examples_in_progress/mini-compiler-backward/imp.why

   1 theory Imp
   2
   3   use state.State
   4   use bool.Bool
   5   use int.Int
   6
   7
   8   (* ************************ SYNTAX ************************ *)
   9   type aexpr =
  10     | Anum int
  11     | Avar id
  12     | Aadd aexpr aexpr
  13     | Asub aexpr aexpr
  14     | Amul aexpr aexpr
  15
  16   type bexpr =
  17     | Btrue
  18     | Bfalse
  19     | Band bexpr bexpr
  20     | Bnot bexpr
  21     | Beq aexpr aexpr
  22     | Ble aexpr aexpr
  23
  24   type com =
  25     | Cskip
  26     | Cassign id aexpr
  27     | Cseq com com
  28     | Cif bexpr com com
  29     | Cwhile bexpr com
  30
  31
  32   (* ************************  SEMANTICS ************************ *)
  33   function aeval  (st:state) (e:aexpr) : int =
  34     match e with
  35       | Anum n      -> n
  36       | Avar x      -> st[x]
  37       | Aadd e1 e2  -> aeval st e1 + aeval st e2
  38       | Asub e1 e2  -> aeval st e1 - aeval st e2
  39       | Amul e1 e2  -> aeval st e1 * aeval st e2
  40     end
  41
  42   function beval (st:state) (b:bexpr) : bool =
  43     match b with
  44       | Btrue      -> true
  45       | Bfalse     -> false
  46       | Bnot b'    -> notb (beval st b')
  47       | Band b1 b2 -> andb (beval st b1) (beval st b2)
  48       | Beq a1 a2  -> aeval st a1 = aeval st a2
  49       | Ble a1 a2  -> aeval st a1 <= aeval st a2
  50     end
  51
  52   inductive ceval state com state =
  53     (* skip *)
  54     | E_Skip : forall m. ceval m Cskip m
  55
  56     (* assignement *)
  57     | E_Ass  : forall m a x. ceval m (Cassign x a) m[x <- aeval m a]
  58
  59     (* sequence *)
  60     | E_Seq : forall cmd1 cmd2 m0 m1 m2.
  61         ceval m0 cmd1 m1 -> ceval m1 cmd2 m2 -> ceval m0 (Cseq cmd1 cmd2) m2
  62
  63     (* if then else *)
  64     | E_IfTrue : forall m0 m1 cond cmd1 cmd2. beval m0 cond ->
  65         ceval m0 cmd1 m1 -> ceval m0 (Cif cond cmd1 cmd2) m1
  66
  67     | E_IfFalse : forall m0 m1 cond cmd1 cmd2. not beval m0 cond ->
  68         ceval m0 cmd2 m1 -> ceval m0 (Cif cond cmd1 cmd2) m1
  69
  70     (* while *)
  71     | E_WhileEnd : forall cond m body. not beval m cond ->
  72         ceval m (Cwhile cond body) m
  73
  74     | E_WhileLoop : forall mi mj mf cond body. beval mi cond ->
  75         ceval mi body mj -> ceval mj (Cwhile cond body) mf ->
  76           ceval mi (Cwhile cond body) mf
  77
  78
  79   lemma ceval_deterministic_aux : forall c mi mf1. ceval mi c mf1 ->
  80       forall mf2. ("inversion" ceval mi c mf2) -> mf1 = mf2
  81
  82   lemma ceval_deterministic : forall c mi mf1 mf2.
  83       ceval mi c mf1 ->  ceval mi c mf2 -> mf1 = mf2
  84
  85 end
  86