source: LTS/imp.ma @ 3582

(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

include "Language.ma".


(* Syntax *)

definition variable ≝ DeqNat.

inductive expr: Type[0] ≝
   Var: variable → expr
 | Const: DeqNat → expr
 | Plus: expr → expr → expr
 | Minus: expr → expr → expr.

inductive condition: Type[0] ≝
   Eq: expr → expr → condition
 | Not: condition → condition.

let rec expr_eq (e1:expr) (e2:expr) on e1 :bool≝
match e1 with [Var v1⇒ match e2 with [Var v2⇒ eqb v1 v2|_⇒ false]
|Const v1⇒ match e2 with [Const v2⇒ eqb v1 v2|_⇒ false]
|Plus le1 re1 ⇒ match e2 with [Plus le2 re2 ⇒ andb (expr_eq le1 le2) (expr_eq re1 re2)|_⇒ false]
|Minus le1 re1 ⇒ match e2 with [Minus le2 re2 ⇒ andb (expr_eq le1 le2) (expr_eq re1 re2)|_⇒ false]
].

lemma expr_eq_elim : ∀P : bool → Prop.∀e1,e2.(e1 = e2 → P true) → (e1 ≠ e2 → P false) → P (expr_eq e1 e2).
#P #e1 lapply P -P elim e1 -e1 
[1,2: #v #P * [1,5: #v' |2,6: #v' |*: #e1 #e2 ] #H1 #H2 normalize try(@H2 % #EQ destruct) @(eqb_elim v v')
  [1,3: #EQ destruct @H1 % |*: * #H @H2 % #EQ destruct @H %]
|*: #e1 #e2 #IH1 #IH2 #P * [1,5: #v' |2,6: #v' |*: #e1' #e2' ] #H1 #H2 try(@H2 % #EQ destruct) normalize
    @IH1
    [1,3: #EQ destruct normalize @IH2 [1,3: #EQ destruct @H1 % |*: * #H @H2 % #EQ destruct @H %]
    |*: * #H @H2 % #EQ destruct @H %
    ]
]
qed.

definition DeqExpr ≝ 
mk_DeqSet expr expr_eq ?.
@hide_prf #e1 #e2 @expr_eq_elim
[ #EQ destruct % // | * #H % #EQ destruct cases H % ]
qed.

unification hint  0 ≔ ; 
    X ≟ DeqExpr
(* ---------------------------------------- *) ⊢ 
    expr ≡ carr X.

(*
unification hint  0 ≔ p1,p2; 
    X ≟ DeqExpr
(* ---------------------------------------- *) ⊢ 
    expr_eq p1 p2 ≡ eqb X p1 p2.
*)
(* for the syntactical record in Language.ma *)


  (* seq_i: type of sequential instructions *)

inductive seq_i:Type[0]≝ |sAss: variable → expr → seq_i.

definition seq_i_eq:seq_i→ seq_i → bool≝λs1,s2:seq_i.
match s1 with [
sAss v e ⇒ match s2 with [sAss v' e' ⇒ (andb (v==v') (expr_eq e e')) ]
].


lemma seq_i_eq_elim : ∀P : bool → Prop.∀s1,s2.(s1 = s2 → P true) → (s1 ≠ s2→ P false) → P (seq_i_eq s1 s2).
#P * #v #e * #v' #e' #H1 #H2 normalize @(eqb_elim v v')
[ #EQ destruct @expr_eq_elim [ #EQ destruct @H1 % | * #H @H2 % #EQ destruct @H %]
| * #H @H2 % #EQ destruct @H %
]
qed.

definition DeqSeqI ≝ mk_DeqSet seq_i seq_i_eq ?.
@hide_prf #e1 #e2 @seq_i_eq_elim
[ #EQ destruct % // | * #H % #EQ destruct cases H % ]
qed.

unification hint  0 ≔ ; 
    X ≟ DeqSeqI
(* ---------------------------------------- *) ⊢ 
    seq_i ≡ carr X.

(* ambigous input! why?
unification hint  0 ≔ p1,p2; 
    X ≟ DeqSeqI
(* ---------------------------------------- *) ⊢ 
    seq_i_eq p1 p2 ≡ eqb X p1 p2.
*)


let rec cond_i_eq (c1:condition) (c2:condition):bool ≝
match c1 with [Eq e1 e2⇒ match c2 with [Eq f1 f2 ⇒ 
(andb (expr_eq e1 f1) (expr_eq e2 f2))|_⇒ false]
|Not e⇒ match c2 with [Not f⇒ cond_i_eq e f|_⇒ false]].

lemma cond_i_eq_elim : ∀P : bool → Prop.∀c1,c2.(c1 = c2 → P true) → (c1 ≠c2 → P false) → P (cond_i_eq c1 c2).
#P #c1 lapply P -P elim c1 -c1
[ #e1 #e2 #P * [ #e1' #e2' | #c' ] #H1 #H2 normalize try (@H2 % #EQ destruct) @expr_eq_elim
  [ #EQ destruct @expr_eq_elim [#EQ destruct @H1 % | * #H @H2 % #EQ destruct @H %]
  | * #H @H2 % #EQ destruct @H %
  ]
| #c #IH #P * [ #e1' #e2' | #c' ] #H1 #H2 normalize try (@H2 % #EQ destruct) @IH
  [#EQ destruct @H1 % | * #H @H2 % #EQ destruct @H %]
]
qed.

definition DeqCondition ≝ mk_DeqSet condition cond_i_eq ?.
@hide_prf #e1 #e2 @cond_i_eq_elim
[ #EQ destruct % // | * #H % #EQ destruct cases H % ]
qed.

unification hint  0 ≔ ; 
    X ≟ DeqCondition
(* ---------------------------------------- *) ⊢ 
    condition ≡ carr X.

(* ambigous input!!!
unification hint  0 ≔ p1,p2; 
    X ≟ DeqCondition
(* ---------------------------------------- *) ⊢ 
    cond_i_eq p1 p2 ≡ eqb X p1 p2.
*)

  (* syntactical record *)

definition imp_instr_params: instr_params ≝ mk_instr_params DeqSeqI DeqFalse 
DeqCondition DeqCondition (DeqProd variable DeqExpr) DeqExpr.

definition environment ≝ DeqSet_List (DeqProd variable DeqNat).


definition default_env: environment ≝ nil ?.
 

let rec assign (env:environment) (v:variable) (n:DeqNat):environment ≝match env with
[nil ⇒ [mk_Prod … v n]
|cons hd tl ⇒ 
    let 〈v',n'〉≝ hd in if (v==v')
                       then 〈v,n〉::tl
                       else hd::(assign tl v n)
].

let rec read (env:environment) (v:variable):(option DeqNat)≝match env with
[nil ⇒ None …
|cons hd tl ⇒ let 〈v',n〉≝ hd in 
  if (v==v')
  then Some … n
  else read tl v
].


lemma assign_hit: ∀env,v,val. read (assign env v val) v = Some … val.
#env elim env
[2: * #v' #val' #env' #IH #v #val whd in match (assign ???);
inversion (v==v')
 [#INV whd in ⊢ (??%?); >(\b (refl …)) %
 |#INV whd in ⊢ (??%?); >INV whd in ⊢ (??%?); @IH ]
|#v #val whd in match (assign [ ] v val); normalize >(eqb_n_n v) %]qed.



lemma assign_miss: ∀env,v1,v2,val. v2 ≠ v1 → (read (assign env v1 val) v2)= (read env v2).
 #env #v1 #v2 #val #E elim env [normalize >(not_eq_to_eqb_false v2 v1) /2 by refl, not_to_not/
|* #v #n #env' #IH inversion(v1==v) #INV [lapply(\P INV)|lapply(\Pf INV)] #K [destruct
whd in match (assign ???); >INV normalize nodelta whd in match (read (〈v,n〉::env') v2);
inversion(v2==v) #INV2 >INV2 normalize nodelta
whd in match (read (〈v,val〉::env') v2); >INV2 normalize nodelta
whd in match (read (〈v,n〉::env') v2); try %
lapply (\P INV2) #ABS cases(absurd ? ABS E)
(*elim E #ABS2 lapply (ABS2 ABS) #F cases F*)
|whd in match (assign ???); >INV normalize nodelta whd in match (read ??);
inversion(v2==v) #INV2 whd in match(if ? then ? else ?);
[whd in match (read ??); >INV2 %
|>IH whd in match (read (〈v,n〉::env') v2);  >INV2 %
qed.

let rec sem_expr (env:environment) (e: expr) on e : (option nat) ≝
 match e with
  [ Var v ⇒ read env v
  | Const n ⇒ Some ? n
  | Plus e1 e2 ⇒ !n1 ← sem_expr env e1;
                 !n2 ← sem_expr env e2;
                 return (n1+n2)
  | Minus e1 e2 ⇒ !n1 ← sem_expr env e1;
                  !n2 ← sem_expr env e2;
                  return (n1-n2)
  ].

let rec sem_condition (env:environment) (c:condition) on c : option bool ≝
  match c with
   [ Eq e1 e2 ⇒ !n ← sem_expr env e1;
                !m ← sem_expr env e2;
                return (eqb n m)
   | Not c ⇒ !b ← sem_condition env c;
             return (notb b)
   ].



(*CERCO*)

definition imp_env_params:env_params≝mk_env_params variable.

definition store_t≝ DeqSet_List (DeqProd environment variable).

definition imp_state_params:state_params≝
mk_state_params imp_instr_params imp_env_params flat_labels store_t (*DeqEnv*).

definition current_env:store_type imp_state_params→ option environment≝λs.!hd ← option_hd … s; return \fst hd.

definition assign_var ≝ λenv:store_t.λv:variable.λn:DeqNat.
match env with
[ nil ⇒ None ?
| cons hd tl ⇒ let 〈e,var〉 ≝ hd in return (〈assign e v n,var〉 :: tl)
].


definition imp_eval_seq:seq_i →store_t→ option store_t
≝λi,s.
match i with
[sAss v e ⇒ match s with
  [nil⇒ None ?
  |cons hd tl⇒ let 〈env,var〉 ≝ hd in
               ! n ← sem_expr env e;
               assign_var s v n
  ]
].


definition imp_eval_io: False → store_t→ option store_t≝?.
// qed.

definition imp_eval_cond_cond:condition → store_t→ option (bool × store_t)≝λc,s.
!env ← current_env s;
!b ← sem_condition env c;
return 〈b,s〉.


definition imp_eval_loop_cond:condition→ store_t → option (bool × store_t)≝
imp_eval_cond_cond.

definition imp_init_store: store_t≝[〈(nil ?),O〉].

definition imp_signature≝signature imp_state_params imp_state_params.

definition imp_eval_call:imp_signature→ (variable × expr) → store_t → (option store_t)≝
λsgn,e,st.
  match sgn with 
  [ mk_signature fun fpt rt ⇒
    let 〈var,act_exp〉 ≝ e in
    match st with
    [nil ⇒ None ?
    |cons hd tl⇒ let 〈env,v〉≝ hd in
                 !n ← sem_expr env act_exp;
                 assign_var (〈(nil ?),var〉::st) fpt n
    ]
  ].

definition imp_return_call:expr→ store_t→ (option store_t)≝
λr,s.match s with 
[nil⇒ None ?
|cons hd tl⇒ let 〈env,v〉≝ hd in
             !n ← sem_expr env r;
             assign_var tl v n
].
 

definition imp_sem_state_params : sem_state_params imp_state_params ≝ mk_sem_state_params imp_state_params imp_eval_seq imp_eval_io
imp_eval_cond_cond imp_eval_loop_cond imp_eval_call imp_return_call imp_init_store.

  (* Abitare tipo Instructions *)
  
definition imp_Instructions≝Instructions imp_state_params flat_labels.

definition imp_envitem≝ (env_item imp_env_params imp_instr_params flat_labels).