Changeset 1871


Ignore:
Timestamp:
Apr 4, 2012, 1:40:30 PM (8 years ago)
Author:
campbell
Message:

Change Clight to Cminor compilation to use gotos rather than loops, blocks
and exits. (Commit on behalf of Ilias)

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/Clight/toCminor.ma

    r1631 r1871  
    1 
    21include "Clight/Csyntax.ma".
    32include "Clight/TypeComparison.ma".
    … …  
    65
    76(* Identify local variables that must be allocated memory. *)
    8 
     7(* These are the variables whose addresses are taken. *)
    98let rec gather_mem_vars_expr (e:expr) : identifier_set SymbolTag ≝
    109match e with
    … …  
    7776].
    7877
     78(* Defines where a variable should be allocated. *)
    7979inductive var_type : Type[0] ≝
    80 | Global : region → var_type
    81 | Stack  : nat → var_type
    82 | Local  : var_type
     80| Global : region → var_type  (* A global, allocated statically in a given region (which one ???)  *)
     81| Stack  : nat → var_type     (* On the stack, at a given height *)
     82| Local  : var_type           (* Locally (hopefully, in a register) *)
    8383.
    8484
     85(* A map associating each variable identifier to its allocation mode and its type. *)
    8586definition var_types ≝ identifier_map SymbolTag (var_type × type).
    8687
    … …  
    99100 *)
    100101
     102(* Some kind of data is never allocated in registers, even if it fits, typically structured data. *)
    101103definition always_alloc : type → bool ≝
    102104λt. match t with
    … …  
    107109].
    108110
     111(* This builds a [var_types] map characterizing the allocation mode, of variables,
     112 * and it returns a stack usage for the function (in bytes, according to [sizeof]) *)
    109113definition characterise_vars : list (ident×region×type) → function → var_types × nat ≝
    110114λglobals, f.
     115  (* globals are added into a map, with var_type Global, region π_2(idrt) and type π_3(idrt) *)
    111116  let m ≝ foldr ?? (λidrt,m. add ?? m (\fst (\fst idrt)) 〈Global (\snd (\fst idrt)), \snd idrt〉) (empty_map ??) globals in
     117  (* variables in the body of the function are gathered in [mem_vars] *)
    112118  let mem_vars ≝ gather_mem_vars_stmt (fn_body f) in
     119  (* iterate on the parameters and local variables of the function, with a tuple (map, stack_high) as an accumulator *)
    113120  let 〈m,stacksize〉 ≝ foldr ?? (λv,ms.
    114     let 〈m,stack_high〉 ≝ ms in
    115     let 〈id,ty〉 ≝ v in
    116     let 〈c,stack_high〉 ≝ if always_alloc ty ∨ mem_set ? mem_vars id
    117                            then 〈Stack stack_high,stack_high + sizeof ty〉
    118                            else 〈Local, stack_high〉 in
     121    let 〈m,stack_high〉 ≝ ms in
     122    let 〈id,ty〉 ≝ v in         
     123    let 〈c,stack_high〉 ≝
     124      (* if the (local, parameter) variable is of a compound type OR if its adress is taken, we allocate it on the stack. *)
     125      if always_alloc ty ∨ mem_set ? mem_vars id then
     126        〈Stack stack_high,stack_high + sizeof ty〉
     127      else
     128        〈Local, stack_high〉
     129    in
    119130      〈add ?? m id 〈c, ty〉, stack_high〉) 〈m,0〉 (fn_params f @ fn_vars f) in
    120131  〈m,stacksize〉.
    121132
     133(* A local variable id' status is not modified by the removal of a global variable id : id' is still local *)
    122134lemma local_id_add_global : ∀vars,id,r,t,id',t'.
    123135  local_id (add ?? vars id 〈Global r, t〉) id' t' → local_id vars id' t'.
    … …  
    129141] qed.
    130142
     143(* If I add a variable id ≠ id', then id' is still local *)
    131144lemma local_id_add_miss : ∀vars,id,vt,id',t'.
    132145  id ≠ id' → local_id (add ?? vars id vt) id' t' → local_id vars id' t'.
    … …  
    138151qed.
    139152
     153(* After characterise_vars, a variable in the resulting map is either a global or a "local"(register or stack allocated) *)
    140154lemma characterise_vars_src : ∀gl,f,vars,n.
    141155  characterise_vars gl f = 〈vars,n〉 →
    142   ∀id. present ?? vars id →
     156  ∀id. present ?? vars id → 
    143157   (∃r,ty. lookup' vars id = OK ? 〈Global r,ty〉 ∧ Exists ? (λx.x = 〈〈id,r〉,ty〉) gl) ∨
    144158   ∃t.local_id vars id t.
    … …  
    181195] qed.
    182196
    183 
     197(* A local variable in a function is either a parameter or a "local" (:=register or stack alloc'd)
     198 * variable, with the right type *)
    184199lemma characterise_vars_all : ∀l,f,vars,n.
    185200  characterise_vars l f = 〈vars,n〉 →
    … …  
    215230] qed.
    216231
     232(* The map generated by characterise_vars is "correct" wrt the fresh ident generator of tag [u],
     233   i.e. by generating fresh idents with u, we risk no collision with the idents in the map domain. *)
    217234lemma characterise_vars_fresh : ∀gl,f,vars,n,u.
    218   characterise_vars gl f = 〈vars,n〉 →
    219   globals_fresh_for_univ ? gl u →
    220   fn_fresh_for_univ f u →
    221   fresh_map_for_univ … vars u.
     235  characterise_vars gl f = 〈vars,n〉 →              (* If we generate a map ... *)
     236  globals_fresh_for_univ ? gl u →                  (* and the globals are out of the idents generated by u *)
     237  fn_fresh_for_univ f u →                          (* and the variables of the function f are cool with u too ... *)
     238  fresh_map_for_univ … vars u.                     (* then there won't be collisions between the map and idents made from u *)
    222239#gl #f #vars #n #u #CH #GL #FN
    223240#id #H
    … …  
    238255axiom MissingField : String.
    239256
    240 
     257(* type_should_eq enforces that two types are equal and eliminates this equality by
     258   transporting P ty1 to P ty2. If ty1 != ty2, then Error *)
    241259definition type_should_eq : ∀ty1,ty2. ∀P:type → Type[0]. P ty1 → res (P ty2) ≝
    242260λty1,ty2,P,p.
    243261  do E ← assert_type_eq ty1 ty2;
    244   OK ? (match E return λx.λ_. P ty1 → P x with [ refl ⇒ λp.p ] p).
    245 
     262  OK ? (match E return λx.λ_. P ty1 → P x with [ refl ⇒ λp.p ] p). 
     263
     264(* same gig for regions *)
    246265definition region_should_eq : ∀r1,r2. ∀P:region → Type[0]. P r1 → res (P r2).
    247266* * #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
    248267qed.
    249268
     269(* same gig for AST typs *)
    250270definition typ_should_eq : ∀ty1,ty2. ∀P:typ → Type[0]. P ty1 → res (P ty2).
    251271* [ #sz1 #sg1 | #r1 | #sz1 ]
    … …  
    257277] qed.
    258278
    259 
    260279alias id "CLunop" = "cic:/matita/cerco/Clight/Csyntax/unary_operation.ind(1,0,0)".
    261280alias id "CMunop" = "cic:/matita/cerco/common/FrontEndOps/unary_operation.ind(1,0,0)".
    … …  
    264283alias id "CMnotbool" = "cic:/matita/cerco/common/FrontEndOps/unary_operation.con(0,3,0)".
    265284
     285(* Translates a Clight unary operation into a Cminor one, while checking
     286 * that the domain and codomain types are consistent. *)
    266287definition translate_unop : ∀t,t':typ. CLunop → res (CMunop t t') ≝
    267288λt,t'.λop:CLunop.
    … …  
    294315  ]. @I qed.
    295316
     317(* Translates a Clight addition into a Cminor one. Four cases to consider :
     318  - integer/integer add
     319  - fp/fp add
     320  - pointer/integer
     321  - integer/pointer.
     322  Consistency of the type is enforced by explicit checks.
     323*)
    296324definition translate_add ≝
    297325λty1,e1,ty2,e2,ty'.
    … …  
    315343| add_default ⇒ Error ? (msg TypeMismatch)
    316344].
     345
    317346
    318347definition translate_sub ≝
    … …  
    408437].
    409438
     439(* Recall that [expr_vars], defined in Cminor/Syntax.ma, asserts a predicate on
     440  all the variables of a program. [translate_binop_vars], given
     441  a predicate verified for all variables of subexprs e1 and e2, produces
     442  a proof that all variables of [translate_binop op _ e1 _ e2 _] satisfy this
     443  predicate. *)
    410444lemma translate_binop_vars : ∀P,op,ty1,e1,ty2,e2,ty,e.
    411445  expr_vars ? e1 P →
    … …  
    445479(* We'll need to implement proper translation of pointers if we really do memory
    446480   spaces. *)
     481(* This function performs leibniz-style subst if r1 = r2, and fails otherwise. *)
    447482definition check_region : ∀r1:region. ∀r2:region. ∀P:region → Type[0]. P r1 → res (P r2) ≝
    448483λr1,r2,P.
    … …  
    456491  ].
    457492
     493(* Simple application of [check_region] to translate between terms. *)
    458494definition translate_ptr : ∀P,r1,r2. (Σe:CMexpr (ASTptr r1). expr_vars ? e P) → res (Σe':CMexpr (ASTptr r2).expr_vars ? e' P) ≝
    459495λP,r1,r2,e. check_region r1 r2 (λr.Σe:CMexpr (ASTptr r).expr_vars ? e P) e.
    … …  
    461497axiom FIXME : String.
    462498
    463 definition translate_cast : ∀P.type → ∀ty2:type. (Σe:CMexpr ?. expr_vars ? e P) → res (Σe':CMexpr (typ_of_type ty2). expr_vars ? e' P) ≝
     499(* Given a source and target type, translate an expession of type source to type target *)
     500definition translate_cast : ∀P. ∀ty1:type.∀ty2:type. (Σe:CMexpr (typ_of_type ty1). expr_vars ? e P) → res (Σe':CMexpr (typ_of_type ty2). expr_vars ? e' P) ≝
    464501λP,ty1,ty2.
    465502match ty1 return λx.(Σe:CMexpr (typ_of_type x). expr_vars ? e P) → ? with
    … …  
    496533qed.
    497534
     535(* Small inversion lemma : if the access mode of a type is by reference, then it must be a ptr type. *)
    498536lemma access_mode_typ : ∀ty,r. access_mode ty = By_reference r → typ_of_type ty = ASTptr r.
    499537*
    … …  
    506544] qed.
    507545
     546(* Translate Clight exprs into Cminor ones.
     547  Arguments :
     548  - vars:var_types, an environment mapping each variable to a couple (allocation mode, type)
     549  - e:expr, the expression to be converted
     550  Result : res (Σe':CMexpr (typ_of_type (typeof e)). expr_vars ? e' (local_id vars))
     551  that is, either
     552  . an error
     553  . an expression e', matching the type of e, such that e' respect the property that all variables
     554    in it are not global. In effect, [translate_expr] will replace global variables by constant symbols.
     555*)
    508556let rec translate_expr (vars:var_types) (e:expr) on e : res (Σe':CMexpr (typ_of_type (typeof e)). expr_vars ? e' (local_id vars)) ≝
    509557match e return λe. res (Σe':CMexpr (typ_of_type (typeof e)). expr_vars ? e' (local_id vars)) with
    … …  
    513561  | Econst_float f ⇒ OK ? «Cst ? (Ofloatconst f), ?»
    514562  | Evar id ⇒
    515       do 〈c,t〉 as E ← lookup' vars id;
     563      do 〈c,t〉 as E ← lookup' vars id; (* E is an equality proof of the shape "lookup' vars id = Ok <c,t>" *)
    516564      match c return λx.? = ? → res (Σe':CMexpr ?. ?) with
    517       [ Global r ⇒ λ_.
     565      [ Global r ⇒ λ_.
     566          (* We are accessing a global variable in an expression. Its Cminor counterpart also depends on
     567             its access mode:
     568             - By_value q, where q is a memory chunk specification (whitch should match the type of the global)
     569             - By_reference, and we only take the adress of the variable
     570             - By_nothing : error
     571           *)
    518572          match access_mode ty with
    519           [ By_value q ⇒ OK ? «Mem ? r q (Cst ? (Oaddrsymbol id 0)), ?»
     573          [ By_value q ⇒ OK ? «Mem ? r q (Cst ? (Oaddrsymbol id 0)), ?» (* Mem is "load" in compcert *)
    520574          | By_reference _ ⇒ OK ? «Cst ? (Oaddrsymbol id 0), ?»
    521575          | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
    522576          ]
    523577      | Stack n ⇒ λE.
     578          (* We have decided that the variable should be allocated on the stack,
     579           * because its adress was taken somewhere or becauste it's a structured data. *)
    524580          match access_mode ty with
    525581          [ By_value q ⇒ OK ? «Mem ? Any q (Cst ? (Oaddrstack n)), ?»
    … …  
    527583          | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
    528584          ]
     585          (* This is a local variable. Keep it as an identifier in the Cminor code, ensuring that the type of the original expr and of ty match. *)
    529586      | Local ⇒ λE. type_should_eq t ty (λt.Σe':CMexpr (typ_of_type t).expr_vars (typ_of_type t) e' (local_id vars))  («Id (typ_of_type t) id, ?»)
    530587      ] E
    531588  | Ederef e1 ⇒
    532589      do e1' ← translate_expr vars e1;
     590      (* According to the way the data pointed to by e1 is accessed, the generated Cminor code will vary.
     591        - if e1 is a kind of int* ptr, then we load ("Mem") the ptr returned by e1
     592        - if e1 is a struct* or a function ptr, then we acess by reference, in which case we :
     593           1) check the consistency of the regions in the type of e1 and in the access mode of its type
     594           2) return directly the converted CMinor expression "as is" (TODO : what is the strange notation with the ceil function and the mapsto ?)
     595      *)
    533596      match typ_of_type (typeof e1) return λx.(Σz:CMexpr x.expr_vars ? z (local_id vars)) → ? with
    534597      [ ASTptr r ⇒ λe1'.
    … …  
    634697      typ_should_eq (typ_of_type (typeof e1)) (typ_of_type ty) (λx.Σe:CMexpr x.?) e'
    635698  ]
    636 ] and translate_addr (vars:var_types) (e:expr) on e : res (𝚺r. Σe':CMexpr (ASTptr r). expr_vars ? e' (local_id vars)) ≝
     699]
     700
     701(* Translate addr takes an expression e1, and returns a Cminor code computing the address of the result of [e1].   *)
     702and translate_addr (vars:var_types) (e:expr) on e : res (𝚺r. Σe':CMexpr (ASTptr r). expr_vars ? e' (local_id vars)) ≝
    637703match e with
    638704[ Expr ed _ ⇒
    … …  
    685751| MemDest : ∀r:region. memory_chunk → (Σe:CMexpr (ASTptr r).expr_vars ? e (local_id vars)) → destination vars.
    686752
     753(* Let a source Clight expression be assign(e1, e2). First of all, observe that [e1] is a
     754  /Clight/ expression, not converted by translate_expr. We thus have to do part of the work
     755  of [translate_expr] in this function. [translate_dest] will convert e1
     756   into a proper destination for an assignement operation. We proceed by case analysis on e1.
     757   - if e1 is a variable [id], then we proceed by case analysis on its allocation mode:
     758      - if [id] is allocated locally (in a register), then id becomes directly
     759        the target for the assignement, as (IdDest vars id t H), where t is the type
     760        of id, and H asserts that id is indeed a local variable.
     761      - if [id] is a global variable stored in region [r], then we perform [translate_expr]'s
     762        job and return an adress, given as a constant symbol corresponding to [id], with
     763        region r and memory chunk specified by the access mode of the rhs type ty2 of [e2].
     764      - same thing for stack-allocated variables, except that we don't specify any region.
     765   - if e1 is not a variable, we use [translate_addr] to generate a Cminor expression computing
     766    the adres of e1
     767*)
    687768definition translate_dest ≝
    688769λvars,e1,ty2.
    … …  
    710791qed.
    711792
     793(* [lenv] is the type of maps from Clight labels to Cminor labels. *)
    712794definition lenv ≝ identifier_map SymbolTag (identifier Label).
    713795
    714796axiom MissingLabel : String.
    715797
     798(* Find the Cminor label corresponding to [l] or fail. *)
    716799definition lookup_label ≝
    717800λlbls:lenv.λl. opt_to_res … [MSG MissingLabel; CTX ? l] (lookup ?? lbls l).
    718801
     802(* True iff the Cminor label [l] is in the codomain of [lbls] *)
    719803definition lpresent ≝ λlbls:lenv. λl. ∃l'. lookup_label lbls l' = OK ? l.
     804
     805(* True iff The Clight label [l] is in the domain of [lbls] *)
     806definition label_in_domain ≝ λlbls:lenv. λl. present ?? lbls l.
     807
     808let rec fresh_list_for_univ (l:list (identifier Label)) (u:universe Label) ≝
     809match l with
     810[ nil ⇒ True
     811| cons elt tl ⇒ fresh_for_univ ? elt u ∧ fresh_list_for_univ tl u].
     812
     813record labgen : Type[0] ≝ {
     814  labuniverse   : universe Label;
     815  label_genlist    : list (identifier Label);
     816  genlist_is_fresh : fresh_list_for_univ label_genlist labuniverse
     817}.
     818
     819lemma fresh_list_stays_fresh : ∀l,tmp,u,u'. fresh_list_for_univ l u → 〈tmp,u'〉=fresh Label u → fresh_list_for_univ l u'.
     820#l elim l
     821[ 1: normalize //
     822| 2: #hd #tl #Hind #tmp #u #u' #HA #HB
     823  whd
     824  @conj
     825  [ 1: whd in HA ⊢ ?;
     826    elim HA #HAleft #HAright
     827    @(fresh_remains_fresh ? hd tmp u u') assumption
     828  | 2: whd in HA ⊢ ?;
     829    elim HA #HAleft #HAright   
     830    @Hind //
     831  ]
     832]
     833qed.
     834
     835definition In ≝ λelttype.λelt.λl.Exists elttype (λx.x=elt) l.   
     836
     837definition generate_fresh_label :
     838 ∀ul. Σlul:(identifier Label × labgen).
     839               (And (∀lab. In ? lab (label_genlist ul) → In ? lab (label_genlist (snd … lul)))
     840                   (In ? (fst … lul) (label_genlist (snd … lul)))) ≝
     841λul.
     842let 〈tmp,u〉 as E ≝ fresh ? (labuniverse ul) in
     843 «〈tmp, mk_labgen u (tmp::(label_genlist ul)) ?〉, ?».
     844[ 1: normalize @conj
     845  [ 1: @(fresh_is_fresh ? tmp u (labuniverse ul) ?) assumption
     846  | 2: @fresh_list_stays_fresh // ]
     847| @conj /2/
     848]
     849qed.
    720850
    721851let rec labels_defined (s:statement) : list ident ≝
    … …  
    739869definition ldefined ≝ λs.λl.Exists ? (λl'.l' = l) (labels_of s).
    740870
     871(* For each label l in s, there exists a matching label l' = lenv(l) defined in s' *)
    741872definition labels_translated : lenv → statement → stmt → Prop ≝
    742873λlbls,s,s'.  ∀l.
    743874  (Exists ? (λl'.l' = l) (labels_defined s)) →
    744   ∃l'. lookup_label lbls l = OK ? l' ∧ ldefined s' l'.
    745 
    746 definition stmt_inv ≝
    747 λvars. λlbls:lenv.
    748   stmt_P (λs.stmt_vars (local_id vars) s ∧ stmt_labels (lpresent lbls) s).
    749 
    750 definition translate_assign : ∀vars:var_types. expr → expr → res (Σs:stmt.∀ls. stmt_inv vars ls s) ≝
     875  ∃l'. lookup_label lbls l = (OK ? l') ∧ ldefined s' l'.
     876
     877
     878(* Invariant on statements, holds during conversion to Cminor *)
     879definition stmt_inv ≝  λvars. stmt_P (stmt_vars (local_id vars)).
     880
     881(* I (Ilias) decided to inline the following definition, to make explicit the data constructed.
     882 * This was needed to prove some stuff in translate_statement at some point, but it might be
     883 * useless now. If needed, I can revert this change.  *)
     884definition translate_assign : ∀vars:var_types. expr → expr → res (Σs:stmt. stmt_inv vars s) ≝
    751885λvars,e1,e2.
    752 do e2' ← translate_expr vars e2;
     886do e2' ← translate_expr vars e2;             
    753887do dest ← translate_dest vars e1 (typeof e2);
    754888match dest with
    … …  
    758892| MemDest r q e1' ⇒ OK ? «St_store ? r q e1' e2', ?»
    759893].
    760 #ls whd %
    761 [ % // @pi2
    762 | @I
    763 | % @pi2
    764 | @I
    765 ] qed.
     894% try (//)  try (elim e2' //) elim e1' //
     895qed.
    766896
    767897definition m_option_map : ∀A,B:Type[0]. (A → res B) → option A → res (option B) ≝
    … …  
    779909qed.
    780910
     911(* Add the list of typed variables tmpenv to the environment [var_types] with
     912   the allocation mode Local. *)
    781913definition add_tmps : var_types → list (ident × type) → var_types ≝
    782914λvs,tmpenv.
    … …  
    787919  tmp_env : list (ident × type);
    788920  tmp_ok : fresh_map_for_univ … (add_tmps vars tmp_env) tmp_universe;
    789   tmp_preserved : 
     921  tmp_preserved :
    790922    ∀id,ty. local_id vars id ty → local_id (add_tmps vars tmp_env) id ty
    791923}.
    … …  
    814946] qed.
    815947
     948
    816949lemma lookup_label_hit : ∀lbls,l,l'.
    817950  lookup_label lbls l = OK ? l' →
    … …  
    821954
    822955(* TODO: is this really needed now? *)
     956
    823957definition tmps_preserved : ∀vars:var_types. tmpgen vars → tmpgen vars → Prop ≝
    824958λvars,u1,u2.
    … …  
    839973qed.
    840974
    841 definition trans_inv : ∀vars:var_types. lenv → statement → tmpgen vars → (stmt×(tmpgen vars)) → Prop ≝
    842 λvars,lbls,s,u,su'.
    843   let 〈s',u'〉 ≝ su' in
    844   stmt_inv (add_tmps vars (tmp_env … u')) lbls s' ∧
    845   labels_translated lbls s s' ∧
    846   tmps_preserved vars u u'.
    847 
    848 lemma trans_inv_stmt_inv : ∀vars,lbls,s,u,su.
    849   trans_inv vars lbls s u su → stmt_inv (add_tmps vars (tmp_env … (\snd su))) lbls (\fst su).
    850 #var #lbls #s #u * #s' #u' * * #H1 #H2 #H3 @H1
    851 qed.
    852 
    853 lemma trans_inv_labels : ∀vars,lbls,s,u,su.
    854   trans_inv vars lbls s u su → labels_translated lbls s (\fst su).
    855 #vars #lbls #s #u * #s' #u' * * #_ #H #_ @H
    856 qed.
    857 
    858 (* TODO: still needed? *)
    859 lemma local_id_add_local_oblivious : ∀vars,id,ty,id',ty'.
    860   fresh_for_map ?? id' vars →
    861   local_id vars id ty → local_id (add ?? vars id' 〈Local, ty'〉) id ty.
    862 #vars #id #ty #id' #ty' #F #H whd whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]);
    863 cases (identifier_eq ? id id')
    864 [ #E @False_ind >E in H; whd in ⊢ (% → ?);
    865   whd in ⊢ (match % with [_⇒ ?|_⇒ ?] → ?); cases id' in F ⊢ %; #id'
    866   #F whd in F; >F *
    867 | #NE >lookup_add_miss [ @H | // ]
    868 ] qed.
    869 
    870 (*
    871 lemma local_id_add_tmps_oblivious : ∀vars,id,ty,u.
    872   local_id vars id ty → local_id (add_tmps vars (tmp_env vars u)) id ty.
    873 #vars #id #ty * #u #l #F #H elim l
    874 [ //
    875 | * #id' #ty' #tl @local_id_add_local_oblivious @F
    876 ] qed.
    877 *)
    878 
    879 lemma add_tmps_oblivious : ∀vars,lbls,s,u.
    880   stmt_inv vars lbls s → stmt_inv (add_tmps vars (tmp_env vars u)) lbls s.
    881 #vars #lbls #s #u #H
     975lemma add_tmps_oblivious : ∀vars,s,u.
     976  stmt_inv vars s → stmt_inv (add_tmps vars (tmp_env vars u)) s.
     977#vars #s #u #H
    882978@(stmt_P_mp … H)
    883 #s' * #H1 #H2 %
    884 [ @(stmt_vars_mp … H1)
    885   #id #t @(tmp_preserved ? u)
    886 | @H2
    887 ] qed.
     979#s' #H1 @(stmt_vars_mp … H1) #id #t #H @(tmp_preserved ? u ?? H)
     980qed.
    888981
    889982lemma local_id_fresh_tmp : ∀vars,tmp,u,ty,u0.
    … …  
    898991qed.
    899992
    900 let rec translate_statement (vars:var_types) (lbls:lenv) (u:tmpgen vars) (s:statement) on s : res (Σsu:stmt×(tmpgen vars).trans_inv vars lbls s u su) ≝
    901 match s return λs.res (Σsu:stmt×(tmpgen vars).trans_inv vars lbls s u su) with
    902 [ Sskip ⇒ OK ? «〈St_skip, u〉, ?»
     993
     994let rec mklabels (ul:labgen) : (identifier Label) × (identifier Label) × labgen ≝
     995  match generate_fresh_label ul with
     996  [ mk_Sig res1 H1 ⇒
     997     let 〈entry_label, ul1〉 as E1 ≝ res1 in
     998     match generate_fresh_label ul1 with
     999     [ mk_Sig res2 H2 ⇒
     1000        let 〈exit_label, ul2〉 as E2 ≝ res2 in
     1001        〈entry_label, exit_label, ul2〉
     1002     ]
     1003  ].
     1004
     1005(* When converting loops into gotos, and in order to eliminate blocks, we have
     1006 * to convert continues and breaks into goto's, too. We add some "flags" in
     1007 * in argument to [translate_statement], meaning that the next encountered break
     1008 * or continue has to be converted into a goto to some contained label.
     1009 * ConvertTo l1 l2 means "convert continue to goto l1 and convert break to goto l2".
     1010 *)
     1011inductive convert_flag : Type[0] ≝
     1012| DoNotConvert : convert_flag
     1013| ConvertTo    : identifier Label → identifier Label → convert_flag. (* continue, break *)
     1014
     1015let rec labels_of_flag (flag : convert_flag) : list (identifier Label) ≝
     1016match flag with
     1017[ DoNotConvert ⇒ [ ]
     1018| ConvertTo continue break ⇒ continue :: break :: [ ]
     1019].
     1020
     1021(* For a top-level expression, [label-wf] collapses to "all labels are properly declared" *)
     1022definition label_wf ≝
     1023λ (s : statement) .λ (s' : stmt) .λ (lbls : lenv). λ (flag : convert_flag).
     1024    stmt_P (λs1. stmt_labels (λl.ldefined s' l ∨ lpresent lbls l ∨ In ? l (labels_of_flag flag)) s1) s'.
     1025
     1026(* trans_inv is the invariant which is enforced during the translation from Clight to Cminor.
     1027  The involved arguments are the following:
     1028  . vars:var_types, an environment mapping variables to their types and allocation modes
     1029  . lbls:lenv, a mapping from old (Clight) to fresh and new (Cminor) labels,
     1030  . s:statement, a Clight statement,
     1031  . uv, a fresh variable generator (containing itself some invariants)
     1032  . flag, wich maps "break" and "continue" to "gotos"
     1033  . su', a couple of a Cminor statement and fresh variable generator.
     1034*)
     1035definition trans_inv : ∀vars:var_types . ∀lbls:lenv . statement → tmpgen vars → convert_flag → ((tmpgen vars) × labgen × stmt) → Prop ≝
     1036λvars,lbls,s,uv,flag,su'.
     1037  let 〈uv', ul', s'〉 ≝ su' in
     1038  stmt_inv (add_tmps vars (tmp_env … uv')) s' ∧   (* remaining variables in s' are local*)
     1039  labels_translated lbls s s' ∧                   (* all the labels in s are transformed in label of s' using [lbls] as a map *)
     1040  tmps_preserved vars uv uv' ∧                    (* the variables generated are local and grows in a monotonic fashion *)
     1041  label_wf s s' lbls flag.                        (* labels are "properly" declared, as defined in [ŀabel_wf].*)
     1042                                 
     1043let rec translate_statement (vars:var_types) (uv:tmpgen vars) (ul:labgen) (lbls:lenv) (flag:convert_flag) (s:statement) on s
     1044  : res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls s uv flag su) ≝
     1045match s return λs.res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls s uv flag su) with
     1046[ Sskip ⇒ OK ? «〈uv, ul, St_skip〉, ?»
    9031047| Sassign e1 e2 ⇒
    904     do s' ← translate_assign vars e1 e2;
    905     OK ? «〈pi1 ?? s', u〉, ?»
     1048    do e2' ← translate_expr vars e2;              (* rhs *)
     1049    do dest ← translate_dest vars e1 (typeof e2); (* e1 *)
     1050    match dest with
     1051    [ IdDest id ty p ⇒
     1052       do e2' ← type_should_eq (typeof e2) ty ? e2';
     1053       OK ? «〈uv, ul, St_assign ? id e2'〉, ?»
     1054    | MemDest r q e1' ⇒
     1055       OK ? «〈uv, ul, St_store ? r q e1' e2'〉, ?»
     1056    ]
    9061057| Scall ret ef args ⇒
    9071058    do ef' ← translate_expr vars ef;
    … …  
    9091060    do args' ← mmap_sigma ??? (translate_expr_sigma vars) args;
    9101061    match ret with
    911     [ None ⇒ OK ? «〈St_call (None ?) ef' args', u〉, ?»
     1062    [ None ⇒ OK ? «〈uv, ul, St_call (None ?) ef' args'〉, ?»
    9121063    | Some e1 ⇒
    9131064        do dest ← translate_dest vars e1 (typeof e1); (* TODO: check if it's sane to use e1's type rather than the return type *)
    9141065        match dest with
    915         [ IdDest id ty p ⇒ OK ? «〈St_call (Some ? 〈id,typ_of_type ty〉) ef' args', u〉, ?»
     1066        [ IdDest id ty p ⇒ OK ? «〈uv, ul, St_call (Some ? 〈id,typ_of_type ty〉) ef' args'〉, ?»
    9161067        | MemDest r q e1' ⇒
    917             let 〈tmp, u〉 as Etmp ≝ alloc_tmp ? (typeof e1) u in
    918             OK ? «〈St_seq (St_call (Some ? 〈tmp,typ_of_type (typeof e1)〉) ef' args') (St_store (typ_of_type (typeof e1)) r q e1' (Id ? tmp)), u〉, ?»
     1068            let 〈tmp, uv1〉 as Etmp ≝ alloc_tmp ? (typeof e1) uv in
     1069            OK ? «〈uv1, ul, St_seq (St_call (Some ? 〈tmp,typ_of_type (typeof e1)〉) ef' args') (St_store (typ_of_type (typeof e1)) r q e1' (Id ? tmp))〉, ?»
    9191070        ]
    9201071    ]
    9211072| Ssequence s1 s2 ⇒
    922      do «s1', u1, H1» ← translate_statement vars lbls u s1;
    923      do «s2', u2, H2» ← translate_statement vars lbls u1 s2;
    924     OK ? «〈St_seq s1' s2', u2〉, ?»
     1073    do «fgens1, s1', H1» ← translate_statement vars uv ul «lbls,?» flag s1;
     1074    do «fgens2, s2', H2» ← translate_statement vars (fst … fgens1) (snd … fgens1) «lbls,?» flag s2;
     1075    OK ? «〈fgens2, St_seq s1' s2'〉, ?»
    9251076| Sifthenelse e1 s1 s2 ⇒
    9261077    do e1' ← translate_expr vars e1;
    9271078    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with
    9281079    [ ASTint _ _ ⇒ λe1'.
    929          do «s1', u, H1» ← translate_statement vars lbls u s1;
    930          do «s2', u, H2» ← translate_statement vars lbls u s2;
    931         OK ? «〈St_ifthenelse ?? e1' s1' s2', u〉, ?»
     1080         do «fgens1, s1', H1» ← translate_statement vars uv ul «lbls,?» flag s1;
     1081         do «fgens2, s2', H2» ← translate_statement vars (fst … fgens1) (snd … fgens1) «lbls,?» flag s2;
     1082        OK ? «〈fgens2, St_ifthenelse ?? e1' s1' s2'〉, ?»
    9321083    | _ ⇒ λ_.Error ? (msg TypeMismatch)
    9331084    ] e1'
    … …  
    9351086    do e1' ← translate_expr vars e1;
    9361087    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with
    937     [ ASTint _ _ ⇒ λe1'.
    938          do «s1', u, H1» ← translate_statement vars lbls u s1;
    939         (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
    940         OK ? «〈St_block
    941                (St_loop
    942                  (St_ifthenelse ?? e1' (St_block s1') (St_exit 0))), u〉, ?»
     1088    [ ASTint _ _ ⇒ λe1'.         
     1089         (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
     1090         match mklabels ul with
     1091         [ mk_Sig result Hmklabels =>
     1092              let 〈labels, ul1〉 as E1 ≝ result in
     1093              let 〈entry, exit〉 as E2 ≝ labels in
     1094              do «fgens2, s1',H1» ← translate_statement vars uv ul1 «lbls,?» (ConvertTo entry exit) s1;
     1095              let converted_loop ≝
     1096               St_label entry
     1097               (St_seq
     1098                 (St_ifthenelse ?? e1' (St_seq s1' (St_goto entry)) St_skip)
     1099                 (St_label exit St_skip))
     1100              in         
     1101              OK ? «〈fgens2, converted_loop〉, ?»
     1102         ]
    9431103    | _ ⇒ λ_.Error ? (msg TypeMismatch)
    9441104    ] e1'
    … …  
    9471107    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → ? with
    9481108    [ ASTint _ _ ⇒ λe1'.
    949          do «s1',u, H1» ← translate_statement vars lbls u s1;
    950         (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
    951         OK ? «〈St_block
    952                (St_loop
    953                  (St_seq (St_block s1') (St_ifthenelse ?? e1' St_skip (St_exit 0)))), u〉, ?»
     1109         match mklabels ul with
     1110         [ mk_Sig result Hmklabels ⇒
     1111              let 〈labels, ul1〉 as E1 ≝ result in
     1112              let 〈entry, exit〉 as E2 ≝ labels in             
     1113              do «fgens2, s1', H1» ← translate_statement vars uv ul1 «lbls,?» (ConvertTo entry exit) s1;
     1114              let converted_loop ≝
     1115               St_label entry
     1116                 (St_seq
     1117                   (St_seq
     1118                     s1'
     1119                     (St_ifthenelse ?? e1' (St_goto entry) St_skip)
     1120                   )
     1121                   (St_label exit St_skip))
     1122              in
     1123              (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
     1124              OK ? «〈fgens2, converted_loop〉, ?»
     1125         ]
    9541126    | _ ⇒ λ_.Error ? (msg TypeMismatch)
    9551127    ] e1'
    … …  
    9581130    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → ? with
    9591131    [ ASTint _ _ ⇒ λe1'.
    960          do «s1', u, H1» ← translate_statement vars lbls u s1;
    961          do «s2', u, H2» ← translate_statement vars lbls u s2;
    962          do «s3', u, H3» ← translate_statement vars lbls u s3;
    963         (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
    964         OK ? «〈St_seq s1'
    965              (St_block
    966                (St_loop
    967                  (St_ifthenelse ?? e1' (St_seq (St_block s3') s2') (St_exit 0)))), u〉, ?»
     1132         match mklabels ul with
     1133         [ mk_Sig result Hmklabels ⇒
     1134              let 〈labels, ul1〉 as E ≝ result in
     1135              let 〈entry, exit〉 as E2 ≝ labels in                           
     1136              do «fgens2, s1', H1» ← translate_statement vars uv ul1 «lbls,?» flag s1;
     1137              do «fgens3, s2', H2» ← translate_statement vars (fst … fgens2) (snd … fgens2) «lbls, ?» (ConvertTo entry exit) s2;
     1138              do «fgens4, s3', H3» ← translate_statement vars (fst … fgens3) (snd … fgens3) «lbls, ?» (ConvertTo entry exit) s3;
     1139              (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
     1140              let converted_loop ≝
     1141                St_seq
     1142                 s1'
     1143                 (St_label entry
     1144                   (St_seq
     1145                     (St_ifthenelse ?? e1' (St_seq s3' (St_seq s2' (St_goto entry))) St_skip)
     1146                     (St_label exit St_skip)
     1147                    ))
     1148              in
     1149             OK ? «〈fgens4, converted_loop〉, ?»
     1150        ]
    9681151    | _ ⇒ λ_.Error ? (msg TypeMismatch)
    9691152    ] e1'
    970 | Sbreak ⇒ OK ? «〈St_exit 1, u〉, ?»
    971 | Scontinue ⇒ OK ? «〈St_exit 0, u〉, ?»
     1153| Sbreak ⇒
     1154   match flag return λf.flag = f → ? with
     1155   [ DoNotConvert ⇒ λEflag.
     1156     Error ? (msg FIXME)
     1157   | ConvertTo continue_label break_label ⇒ λEflag.
     1158     OK ? «〈uv, ul, St_goto break_label〉, ?»
     1159   ] (refl ? flag)
     1160| Scontinue ⇒
     1161  match flag return λf.flag = f → ? with
     1162  [ DoNotConvert ⇒ λEflag.
     1163    Error ? (msg FIXME)
     1164  | ConvertTo continue_label break_label ⇒ λEflag.
     1165    OK ? «〈uv, ul, St_goto continue_label〉, ?»
     1166  ] (refl ? flag)
    9721167| Sreturn ret ⇒
    9731168    match ret with
    974     [ None ⇒ OK ? «〈St_return (None ?), u〉, ?»
     1169    [ None ⇒ OK ? «〈uv, ul, St_return (None ?)〉, ?»
    9751170    | Some e1 ⇒
    9761171        do e1' ← translate_expr vars e1;
    977         OK ? «〈St_return (Some ? (mk_DPair … e1')), u〉, ?»
     1172        OK ? «〈uv, ul, St_return (Some ? (mk_DPair … e1'))〉, ?»
    9781173    ]
    9791174| Sswitch e1 ls ⇒ Error ? (msg FIXME)
    9801175| Slabel l s1 ⇒
    9811176    do l' as E ← lookup_label lbls l;
    982      do «s1', u, H1» ← translate_statement vars lbls u s1;
    983     OK ? «〈St_label l' s1', u〉, ?»
     1177    do «fgens1, s1', H1» ← translate_statement vars uv ul lbls flag s1;
     1178    OK ? «〈fgens1, St_label l' s1'〉, ?»
    9841179| Sgoto l ⇒
    9851180    do l' as E ← lookup_label lbls l;
    986     OK ? «〈St_goto l', u〉, ?»
     1181    OK ? «〈uv, ul, St_goto l'〉, ?»
    9871182| Scost l s1 ⇒
    988      do «s1', u, H1» ← translate_statement vars lbls u s1;
    989     OK ? «〈St_cost l s1', u〉, ?»
    990 ].
    991 try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj
    992 try @I
    993 try (#l #H @(match H in False with [ ]))
    994 try (#id #ty #H @H)
    995 [ @add_tmps_oblivious @(pi2 ?? s')
    996 | @(tmp_preserved … u) @p
    997 ]
    998 try (@sub_pi2 #x @expr_vars_mp #i #ty @(tmp_preserved … u))
    999 [ 1,3,6: @sub_pi2 #x @All_mp * #ty #e @expr_vars_mp #i #ty' @(tmp_preserved … u)
    1000 | 2,4: @(local_id_fresh_tmp … Etmp)
    1001 | @(alloc_tmp_preserves … Etmp)
    1002 | 7,11: @(stmt_P_mp … (π1 (π1 H1))) #s * #H3 #H4 % [ 1,3: @(stmt_vars_mp … H3) cases H2 #_ #H @H | *: @H4 ]
    1003 | 8,12: @(trans_inv_stmt_inv … H2)
    1004 | 9,13: #l #H cases (Exists_append … H)
    1005   [ 1,3: #H3 cases H1 * #S1 #L1 #T1 cases (L1 l H3) #l' * #E1 #D1
    1006     %{l'} % [ 1,3: @E1 | *: @Exists_append_l @D1 ]
    1007   | *: #H3 cases H2 * #S2 #L2 #T2 cases (L2 l H3) #l' * #E2 #D2
    1008     %{l'} % [ 1,3: @E2 | *: @Exists_append_r @D2 ]
    1009   ]
    1010 | 10,14: cases H2 #_ #TP2 #id #ty #L @TP2 cases H1 #_ #TP1 @TP1 @L
    1011 | 15,18: @(π1 (π1 H1))
    1012 | 16,19: cases H1 * #_ #L1 #_ #l #H cases (L1 l H) #l' * #E1 #D1
    1013   %{l'} % [ 1,3: @E1 | *: @Exists_append_l @D1 ]
    1014 | 17,20: @(π2 H1)
    1015 (* Sfor *)
    1016 | @(stmt_P_mp … (π1 (π1 H1))) #s * #H4 #H5 % [ @(stmt_vars_mp … H4) #id #ty #H @(π2 H3) @(π2 H2) @H | @H5 ]
    1017 | @(π1 (π1 H3))
    1018 | @(stmt_P_mp … (π1 (π1 H2))) #s * #H4 #H5 % [ @(stmt_vars_mp … H4) #id #ty #H @(π2 H3) @H | @H5 ]
    1019 | #l #H cases (Exists_append … H)
    1020   [ #EX1 cases H1 * #S1 #L1 #_ cases (L1 l EX1) #l' * #E1 #D1
    1021     %{l'} % [ @E1 | @Exists_append_l @D1 ]
    1022   | #EX cases (Exists_append … EX)
    1023     [ #EX2 cases H2 * #S2 #L2 #_ cases (L2 l EX2) #l' * #E2 #D2
    1024       %{l'} % [ @E2 | @Exists_append_r @Exists_append_l @Exists_append_r @D2 ]
    1025     | #EX3 cases H3 * #S3 #L3 #_ cases (L3 l EX3) #l' * #E3 #D3
    1026       %{l'} % [ @E3 | @Exists_append_r @Exists_append_l @Exists_append_l @D3 ]
    1027     ]
    1028   ]
    1029 | #id #ty #H @(π2 H3) @(π2 H2) @(π2 H1) @H
    1030 (* Slabel *)
    1031 | %{l} @E
    1032 | @(π1 (π1 H1))
    1033 | #l'' * [ #E <E %{l'} % // %1 @refl | #EX cases (π2 (π1 H1) l'' EX) #l4 * #LK #LD %{l4} % // %2 @LD ]
    1034 | @(π2 H1)
    1035 (* Sgoto *)
    1036 | %{l} @E
    1037 | @(π1 (π1 H1))
    1038 (* Scost *)
    1039 | @(π2 (π1 H1))
    1040 | @(π2 H1)
     1183    do «fgens1, s1', H1» ← translate_statement vars uv ul lbls flag s1;
     1184    OK ? «〈fgens1, St_cost l s1'〉, ?»
     1185].
     1186try @conj try @conj try @conj try @conj try @conj try @conj try @conj
     1187try (@I)
     1188try (#l #H elim H)
     1189try (#size #sign #H assumption)
     1190try (#region #H assumption)
     1191[ 1,5: @(tmp_preserved … p) ]
     1192[ 1,3: elim e2' | 2,9: elim e1' | 4,7,14: elim ef' ]
     1193[ 1,2,3,4,5,6,7 : #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal) ]
     1194[ 1: @All_mp [ 1: @(λe.match e with [ mk_DPair t e0 ⇒ expr_vars t e0 (local_id vars) ])
     1195             | 2: * #t #e #Hev whd in Hev ⊢ %; @(expr_vars_mp … Hev) #i #t #Hp @(tmp_preserved … Hp)
     1196             | 3: elim args' // ]
     1197| 8: (* we should be able to merge this case with the previous ... *)
     1198     @All_mp [ 1: @(λe.match e with [ mk_DPair t e0 ⇒ expr_vars t e0 (local_id vars) ])
     1199             | 2: * #t #e #Hev whd in Hev ⊢ %; @(expr_vars_mp … Hev) #i #t #Hp @(tmp_preserved … Hp)
     1200             | 3: elim args' // ]
     1201| 2: @(local_id_fresh_tmp vars tmp uv1 (typeof e1) uv Etmp)
     1202| 3:  @(All_mp (𝚺 t:typ.expr t) (λe. match e with [ mk_DPair t e0 ⇒ expr_vars t e0 (local_id vars)]))
     1203       [ 1: #a #Ha elim a in Ha ⊢ ?; #ta #a #Ha whd @(expr_vars_mp ?? (local_id vars))
     1204       [ 1: #i0 #t0 #H0 @(tmp_preserved vars uv1 i0 t0 H0)
     1205       | 2: assumption ]
     1206       | 2: elim args' // ]
     1207| 4: @(local_id_fresh_tmp vars tmp uv1 (typeof e1) uv Etmp) ]
     1208[ 1: #size #sign | 2: #reg | 3: #fsize ]
     1209[ 1,2,3: #H @(alloc_tmp_preserves vars tmp uv uv1 … Etmp) @H ]
     1210try @(match fgens1 return λx.x=fgens1 → ? with
     1211     [ mk_Prod uv1 ul1 ⇒ λHfgens1.? ] (refl ? fgens1))
     1212try @(match fgens2 return λx.x=fgens2 → ? with
     1213     [ mk_Prod uv2 ul2 ⇒ λHfgens2.? ] (refl ? fgens2))
     1214try @(match fgens3 return λx.x=fgens3 → ? with
     1215     [ mk_Prod uv3 ul3 ⇒ λHfgens3.? ] (refl ? fgens3))
     1216try @(match fgens4 return λx.x=fgens4 → ? with
     1217     [ mk_Prod uv4 ul4 ⇒ λHfgens4.? ] (refl ? fgens4))
     1218whd in H1 H2 H3 ⊢ ?; destruct whd nodelta in H1 H2 H3;
     1219try (elim H1 -H1 * * #Hstmt_inv1 #Hlabels_tr1 #Htmps_pres1)
     1220try (elim H2 -H2 * * #Hstmt_inv2 #Hlabels_tr2 #Htmps_pres2)
     1221try (elim H3 -H3 * * #Hstmt_inv3 #Hlabels_tr3 #Htmps_pres3)
     1222[ 1,2: #Hind1 #Hind2 | 3,4,9,11: #Hind | 5: #Hind1 #Hind2 #Hind3 ]
     1223try @conj try @conj try @conj try @conj try @conj try (whd @I) try assumption
     1224[ 1,7: @(stmt_P_mp … Hstmt_inv1) #e #Hvars @(stmt_vars_mp … Hvars) #i #t #Hlocal @(Htmps_pres2 … Hlocal)
     1225| 2: #l #H cases (Exists_append ???? H) #Hcase
     1226         [ 1: elim (Hlabels_tr1 l Hcase) #label #Hlabel @(ex_intro … label) @conj
     1227           [ 1: @(proj1 ?? Hlabel)
     1228           | 2: normalize @Exists_append_l @(proj2 … Hlabel) ]
     1229         | 2: elim (Hlabels_tr2 l Hcase) #label #Hlabel @(ex_intro … label) @conj
     1230           [ 1: @(proj1 ?? Hlabel)
     1231           | 2: normalize @Exists_append_r @(proj2 … Hlabel) ]
     1232         ]
     1233| 3,9: #id #ty #H @(Htmps_pres2 … (Htmps_pres1 id ty H)) ]
     1234[ 1: @(stmt_P_mp … Hind2) | 2: @(stmt_P_mp … Hind1) ]
     1235[ 1,2: #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
     1236     #l * try * [ 1,4: #H %1 %1 normalize in H ⊢ %; try (@Exists_append_l @H); try (@Exists_append_r @H)
     1237                | 2,5: #H %1 %2 assumption
     1238                | 3,6: #H %2 assumption ]
     1239(* if/then/else *)
     1240| 3: whd elim e1' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal)
     1241| 4: whd #l #H
     1242       cases (Exists_append ???? H) #Hcase
     1243         [ 1: elim (Hlabels_tr1 l Hcase) #label #Hlabel @(ex_intro … label) @conj
     1244           [ 1: @(proj1 ?? Hlabel)
     1245           | 2: normalize @Exists_append_l @(proj2 … Hlabel) ]
     1246         | 2: elim (Hlabels_tr2 l Hcase) #label #Hlabel @(ex_intro … label) @conj
     1247           [ 1: @(proj1 ?? Hlabel)
     1248           | 2: normalize @Exists_append_r @(proj2 … Hlabel) ]
     1249         ]
     1250]                 
     1251[ 1: 1: @(stmt_P_mp … Hind2) | 2: @(stmt_P_mp … Hind1) ]
     1252[ 1,2: #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
     1253     #l * try * [ 1,4: #H %1 %1 normalize in H ⊢ %; try (@Exists_append_l @H); try (@Exists_append_r @H)
     1254                | 2,5: #H %1 %2 assumption
     1255                | 3,6: #H %2 assumption ] ]
     1256try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @I
     1257[ 1,9,19,32: whd elim e1' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal)
     1258| 2,8: @(stmt_P_mp … Hstmt_inv1) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) //
     1259| 3,10: whd #l #H normalize in H;
     1260         elim (Hlabels_tr1 … H) #label #Hlabel @(ex_intro … label)
     1261         @conj
     1262         [ 1,3: @(proj1 … Hlabel)
     1263         | 2,4: whd @or_intror normalize @Exists_append_l @Exists_append_l try @Exists_append_l
     1264              @(proj2 … Hlabel) ]
     1265| 30: whd %2 %2 whd /2/
     1266| 31: whd %2 whd /2/
     1267| 4,16: whd %1 %1 normalize /2/
     1268| 5,12: @(stmt_P_mp … Hind) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
     1269   #l * try * [ 1,5: #H %1 %1 normalize %2 @Exists_append_l @Exists_append_l try @Exists_append_l @H
     1270              | 2,6: #H %1 %2 assumption
     1271              | 3,7: #H <H %1 %1 normalize /2/
     1272              | 4,8: #H normalize in H; elim H [ 1,3: #E <E %1 %1 normalize %2
     1273                                                 @Exists_append_r normalize /2/
     1274                                               | 2,4: * ]
     1275              ]
     1276| 6: normalize %1 %1 %1 //                                                                                   
     1277| 7,14: normalize %1 %1 %2 @Exists_append_r normalize /2/
     1278| 11,13: whd %1 %1 normalize /2/
     1279| 15: whd #label * [ 1: #Eq @(ex_intro … l') @conj [ 1: destruct // | whd /2/ ]
     1280                   | 2: #H elim (Hlabels_tr1 label H)
     1281                         #lab * #Hlookup #Hdef @(ex_intro … lab) @conj
     1282                         [ 1: // | 2: whd %2 assumption ]
     1283                   ]
     1284| 17: @(stmt_P_mp … Hind) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
     1285   #l * try * [ 1: #H %1 %1 normalize %2 @H
     1286              | 2: #H %1 %2 assumption
     1287              | 3: #H %2 assumption ]
     1288| 18: @(stmt_P_mp … Hstmt_inv1) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) #i #t
     1289   #H @(Htmps_pres3 … (Htmps_pres2 … H))
     1290| 20: @(stmt_P_mp … Hstmt_inv3) //
     1291| 21: @(stmt_P_mp … Hstmt_inv2) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) #i #t
     1292   #H @(Htmps_pres3 … H)
     1293| 22: whd #l #H normalize in H;
     1294      cases (Exists_append … H) #Hcase
     1295      [ 1: elim (Hlabels_tr1 l Hcase) #label #Hlabel @(ex_intro … label) @conj
     1296        [ 1: @(proj1 … Hlabel)
     1297        | 2: normalize @Exists_append_l @(proj2 … Hlabel)
     1298        ]
     1299      | 2: cases (Exists_append … Hcase) #Hcase2
     1300        [ 1: elim (Hlabels_tr2 l Hcase2) #label #Hlabel @(ex_intro … label) @conj
     1301          [ 1: @(proj1 … Hlabel)
     1302          | 2: normalize >append_nil >append_nil >append_cons
     1303               @Exists_append_r @Exists_append_l @Exists_append_r
     1304               @(proj2 … Hlabel)
     1305          ]
     1306        | 2: elim (Hlabels_tr3 l Hcase2) #label #Hlabel @(ex_intro … label) @conj
     1307          [ 1: @(proj1 … Hlabel)
     1308          | 2: normalize >append_nil >append_nil >append_cons
     1309             @Exists_append_r @Exists_append_l @Exists_append_l
     1310             @(proj2 … Hlabel)
     1311          ]
     1312        ]
     1313      ]
     1314| 23: #id #ty #H @(Htmps_pres3 … (Htmps_pres2 … (Htmps_pres1 … H)))
     1315| 24: @(stmt_P_mp … Hind3) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
     1316   #l * try * [ 1: #H %1 %1 normalize @Exists_append_l @H
     1317              | 2: #H %1 %2 assumption
     1318              | 3: #H %2 assumption ]
     1319| 25: whd %1 %1 normalize /2/
     1320| 26: @(stmt_P_mp … Hind1) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
     1321   #l * try * [ 1: #H %1 %1 normalize @Exists_append_r @(Exists_add ?? (nil ?))
     1322                   @Exists_append_r @Exists_append_l @Exists_append_l
     1323                   @Exists_append_l assumption
     1324              | 2: #H %1 %2 assumption
     1325              | 3: #H <H %1 %1 normalize
     1326                   @Exists_append_r whd %1 //
     1327              | 4: * [ 1: #H <H %1 %1 normalize
     1328                       @Exists_append_r @(Exists_add ?? (nil ?))
     1329                       @Exists_append_r @Exists_append_r
     1330                       whd %1 //
     1331                     | 2: * ]
     1332              ]
     1333| 27: @(stmt_P_mp … Hind2) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
     1334   #l * try * [ 1: #H %1 %1 normalize @Exists_append_r @(Exists_add ?? (nil ?))
     1335                   @Exists_append_r @Exists_append_l @Exists_append_l                   
     1336                   @Exists_append_r @Exists_append_l assumption
     1337              | 2: #H %1 %2 assumption
     1338              | 3: #H <H %1 %1 normalize
     1339                   @Exists_append_r whd %1 //
     1340              | 4: * [ 1: #Eq <Eq %1 %1 whd normalize
     1341                       @Exists_append_r @(Exists_add ?? (nil ?)) @Exists_append_r
     1342                       @Exists_append_r whd %1 //
     1343                     | 2: * ]
     1344              ]
     1345| 28: whd %1 %1 normalize /2/
     1346| 29: whd %1 %1 normalize
     1347      @Exists_append_r @(Exists_add ?? (nil ?)) @Exists_append_r @Exists_append_r
     1348      whd %1 //
     1349| 33: whd %1 %2 whd @(ex_intro … l) @E
    10411350] qed.
    10421351
    1043 
    10441352axiom ParamGlobalMixup : String.
    10451353
    1046 (* ls and s0 aren't real parameters, they're just there for giving the invariant. *)
    1047 definition alloc_params : ∀vars:var_types.∀ls,s0,u. list (ident×type) → (Σsu:stmt×(tmpgen vars). trans_inv vars ls s0 u su) → res (Σsu:stmt×(tmpgen vars).trans_inv vars ls s0 u su) ≝
    1048 λvars,ls,s0,u,params,s. foldl ?? (λsu,it.
     1354(* params and statement aren't real parameters, they're just there for giving the invariant. *)
     1355definition alloc_params :
     1356 ∀vars:var_types.∀lbls,statement,uv,flag. list (ident×type) → (Σsu:(tmpgen vars)×labgen×stmt. trans_inv vars lbls statement uv flag su)
     1357   → res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls statement uv flag su) ≝   
     1358λvars,lbls,statement,uv,ul,params,s. foldl ?? (λsu,it.
    10491359  let 〈id,ty〉 ≝ it in
    1050    do «s,u, Is» ← su;
     1360  do «result,Is» ← su;
     1361  let 〈fgens1, s〉 as Eresult ≝ result in
    10511362  do 〈t,ty'〉 as E ← lookup' vars id;
    1052   match t return λx.? → ? with
    1053   [ Local ⇒ λE. OK (Σs:stmt×(tmpgen vars).?) «〈s,u〉,Is»
     1363  match t return λx.? → res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls statement uv ul su) with
     1364  [ Local ⇒ λE. OK (Σs:(tmpgen vars)×labgen×stmt.?) «result,Is»
    10541365  | Stack n ⇒ λE.
    10551366      do q ← match access_mode ty with
    … …  
    10581369      | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
    10591370      ];
    1060       OK ? «〈St_seq (St_store ? Any q (Cst ? (Oaddrstack n)) (Id (typ_of_type ty') id)) s, u〉, ?»
     1371      OK ? «〈fgens1, St_seq (St_store ? Any q (Cst ? (Oaddrstack n)) (Id (typ_of_type ty') id)) s〉, ?»
    10611372  | Global _ ⇒ λE. Error ? [MSG ParamGlobalMixup; CTX ? id]
    10621373  ] E) (OK ? s) params.
    1063 try @conj try @conj try @conj try @conj try @conj try @conj
    1064 try @I
    1065 [ @(expr_vars_mp … (tmp_preserved … u)) whd >E @refl
    1066 | @(π1 (π1 Is))
    1067 | @(π2 (π1 Is))
    1068 | @(π2 Is)
    1069 ] qed.
    1070 
    1071 (*
    1072 lemma local_id_add_local : ∀vars,id,id'.
    1073   local_id vars id →
    1074   local_id (add ?? vars id' Local) id.
    1075 #vars #id #id' #H
    1076 whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ?] cases (identifier_eq ? id id')
    1077 [ #E < E >lookup_add_hit //
    1078 | #NE >lookup_add_miss // @eq_identifier_elim // #E cases NE >E /2/
    1079 ] qed.
    1080 *)
     1374whd
     1375@(match fgens1 return λx.x=fgens1 → ? with
     1376  [ mk_Prod uv1 ul1 ⇒ λHfgens1.? ] (refl ? fgens1))
     1377whd in Is ⊢ %; destruct whd in Is;
     1378try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @I
     1379elim Is * * #Hincl #Hstmt_inv #Hlab_tr #Htmp_pr try assumption
     1380@(expr_vars_mp … (tmp_preserved … uv1)) whd >E @refl
     1381qed.
     1382
    10811383axiom DuplicateLabel : String.
    10821384
    … …  
    10981400>lookup_add_miss
    10991401[ @refl | @NE ]
    1100 qed. 
    1101 
    1102 let rec populate_lenv (ls:list ident) (lbls:lenv) (u:universe ?) : res (Σlbls':lenv. lenv_list_inv lbls lbls' ls) ≝
    1103 match ls return λls. res (Σlbls':lenv. lenv_list_inv lbls lbls' ls) with
    1104 [ nil ⇒ OK ? «lbls, ?»
     1402qed.
     1403
     1404let rec populate_lenv (ls:list ident) (ul:labgen) (lbls:lenv): res ((Σlbls':lenv. lenv_list_inv lbls lbls' ls) × labgen) ≝
     1405match ls return λls.res ((Σlbls':lenv. lenv_list_inv lbls lbls' ls) × labgen) with
     1406[ nil ⇒ OK ? 〈«lbls, ?», ul〉
    11051407| cons l t ⇒
    1106     match lookup_label lbls l return λx.lookup_label lbls l = x → ? with
    1107     [ OK _ ⇒ λ_. Error ? (msg DuplicateLabel)
    1108     | Error _ ⇒ λLOOK.
    1109         let 〈l',u1〉 ≝ fresh … u in
    1110         do lbls1 ← populate_lenv t (add … lbls l l') u1;
    1111         OK ? «pi1 … lbls1, ?»
    1112     ] (refl ? (lookup_label lbls l))
    1113 ].
    1114 [ #l #l' #H %2 @H
    1115 | cases lbls1 #lbls' #I whd in ⊢ (??%?);
    1116   #l1 #l1' #E1 @(eq_identifier_elim … l l1)
    1117   [ #E %1 %1 @E
    1118   | #NE cases (I l1 l1' E1)
    1119     [ #H %1 %2 @H
    1120     | #LOOK' %2 >lookup_label_miss in LOOK'; /2/ #H @H
    1121     ]
    1122   ]
    1123 ] qed.
    1124 
    1125 definition build_label_env : ∀body:statement. res (Σlbls:lenv. ∀l,l'.lookup_label lbls l = OK ? l' → Exists ? (λl'.l' = l) (labels_defined body)) ≝
     1408  match lookup_label lbls l return λlook. lookup_label lbls l = look → ? with
     1409  [ OK _    ⇒ λ_.Error ? (msg DuplicateLabel)
     1410  | Error _ ⇒ λLOOK.
     1411    match generate_fresh_label … ul with
     1412    [ mk_Sig ret H ⇒
     1413       do 〈packed_lbls, ul1〉 ← populate_lenv t (snd ?? ret) (add … lbls l (fst ?? ret));
     1414       match packed_lbls with
     1415       [ mk_Sig lbls' Hinv ⇒ OK ? 〈«lbls', ?», ul1〉 ]
     1416    ]
     1417  ] (refl ? (lookup_label lbls l))
     1418].
     1419[ 1: whd #l #l' #Hlookup %2 assumption
     1420| 2: whd in Hinv; whd #cl_lab #cm_lab #Hlookup
     1421     @(eq_identifier_elim … l cl_lab)
     1422     [ 1: #Heq %1 >Heq whd %1 //
     1423     | 2: #Hneq cases (Hinv cl_lab cm_lab Hlookup)
     1424           [ 1: #H %1 %2 @H
     1425           | 2: #LOOK' %2 >lookup_label_miss in LOOK'; /2/ #H @H ]
     1426     ]
     1427]
     1428qed.
     1429
     1430definition build_label_env :
     1431   ∀body:statement. res ((Σlbls:lenv. ∀l,l'.lookup_label lbls l = OK ? l' → Exists ? (λl'.l' = l) (labels_defined body)) × labgen) ≝
    11261432λbody.
    1127   do «lbls, H» ← populate_lenv (labels_defined body) (empty_map ??) (new_universe ?);
    1128   OK ? «lbls, ?».
    1129 #l #l' #E cases (H l l' E) //
    1130 whd in ⊢ (??%? → ?); #H destruct
     1433  let initial_labgen ≝ mk_labgen (new_universe ?) (nil ?) ?  in
     1434  do 〈label_map, u〉 ← populate_lenv (labels_defined body) initial_labgen (empty_map ??);
     1435  let lbls ≝ pi1 ?? label_map in
     1436  let H    ≝ pi2 ?? label_map in
     1437  OK ? 〈«lbls, ?», u〉.
     1438[ 1: #l #l' #E cases (H l l' E) //
     1439     whd in ⊢ (??%? → ?); #H destruct
     1440| 2: whd @I ]
    11311441qed.
    11321442
    … …  
    11581468] qed.
    11591469
     1470(* This lemma allows to merge two stmt_P in one. Used in the following parts to merge an invariant on variables
     1471   and an invariant on labels. *)
     1472lemma stmt_P_conj : ∀ (P1:stmt → Prop). ∀ (P2:stmt → Prop). ∀ s. stmt_P P1 s → stmt_P P2 s → stmt_P (λs.P1 s ∧ P2 s) s.
     1473#P1 #P2 #s elim s
     1474normalize try @conj try @conj try /3/
     1475[ #z0 #s #Hind1 #Hind2 * * #HA #HB #HC * * #HD #HE #HF try @conj try @conj try @conj try /2/
     1476| #H5 #H6 #H7 #H8 #H9 #H10 #H11 * * #H15 #H16 #H17 * * #H20 #H21 #H22
     1477  try @conj try @conj try @conj try /2/
     1478| 3,4: #H24 #H25 * #H29 #H30 * #H33 #H34 try @conj try @conj try @conj try /2/
     1479| 5,6: #H36 #H37 #H38 * #H42 #H43 * #H46 #H47 try @conj try @conj try @conj try /2/ ]
     1480qed.
     1481
    11601482definition translate_function :
    11611483  ∀tmpuniverse:universe SymbolTag.
    … …  
    11661488  res internal_function ≝
    11671489λtmpuniverse, globals, f, Fglobals, Ffn.
    1168   do «lbls, Ilbls» ← build_label_env (fn_body f);
    1169   let 〈vartypes, stacksize〉 as E ≝ characterise_vars globals f in
    1170   let tmp ≝ mk_tmpgen vartypes tmpuniverse [ ] ?? in
    1171   do s ← translate_statement vartypes lbls tmp (fn_body f);
    1172   do «s,tmp, Is» ← alloc_params vartypes lbls ?? (fn_params f) s;
    1173   let params ≝ map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_params f) in
    1174   let vars ≝ map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (tmp_env ? tmp @ fn_vars f) in
    1175   do D ← check_distinct_env ?? (params @ vars);
    1176   OK ? (mk_internal_function
    1177     (opttyp_of_type (fn_return f))
    1178     params
    1179     vars
    1180     D
    1181     stacksize
    1182     s ?).
    1183 [ //
    1184 | @(characterise_vars_fresh … (sym_eq … E)) //
    1185 | cases Is * #S #L #TP
    1186   @(stmt_P_mp ???? S)
    1187   #s1 * #H1 #H2 %
    1188   [ @(stmt_vars_mp … H1)
    1189     #i #t #H
    1190     cases (local_id_split … H)
    1191     [ #H' >map_append
    1192       @Exists_map [ 2: @Exists_squeeze @(characterise_vars_all … (sym_eq ??? E) i t) @H'
    1193                   | skip
    1194                   | * #id #ty * #E1 #E2 <E1 <E2 @refl
    1195                   ]
    1196     | #EX @Exists_append_r whd in ⊢ (???%); <map_append @Exists_append_l @Exists_map [2: @EX | skip | * #id #ty * #E1 #E2 <E1 <E2 % @refl ]
    1197     ]
    1198   | @(stmt_labels_mp … H2)
    1199     #l * #l' #LOOKUP
    1200     lapply (Ilbls l' l LOOKUP) #DEFINED
    1201     cases (L … DEFINED) #lx * #LOOKUPx >LOOKUPx in LOOKUP; #Ex destruct (Ex)
    1202     #H @H
    1203   ]
    1204 ] qed.
     1490  do 〈env_pack, ul〉 ← build_label_env (fn_body f);
     1491    match env_pack with
     1492    [ mk_Sig lbls Ilbls ⇒
     1493      let 〈vartypes, stacksize〉 as E ≝ characterise_vars globals f in
     1494      let uv ≝ mk_tmpgen vartypes tmpuniverse [ ] ?? in
     1495      do s0 ← translate_statement vartypes uv ul lbls DoNotConvert (fn_body f);
     1496      do «fgens, s1, Is» ← alloc_params vartypes lbls ? uv DoNotConvert (fn_params f) s0;
     1497      let params ≝ map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_params f) in
     1498      let vars ≝ map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (tmp_env ? (fst ?? fgens) @ fn_vars f) in
     1499      do D ← check_distinct_env ?? (params @ vars);
     1500      OK ? (mk_internal_function
     1501        (opttyp_of_type (fn_return f))
     1502        params
     1503        vars
     1504        D
     1505        stacksize
     1506        s1 ?)
     1507  ].
     1508[ 1: #i #t #Hloc whd @Hloc
     1509| 2: whd #id #Hpresent normalize in Hpresent:(???%?); whd in Hpresent;
     1510      @(characterise_vars_fresh … (sym_eq … E)) //
     1511| 3: @(match fgens return λx.x=fgens → ? with
     1512     [ mk_Prod uv' ul' ⇒ λHfgens.? ] (refl ? fgens))
     1513     whd in Is; <Hfgens in Is; #Is whd in Is ⊢ %;
     1514     elim Is * * #Hstmt_inv #Hlab_trans #Htmps_pres #Hlabel_wf
     1515     (* merge Hlabel_wf with Hstmt_inv and eliminate right away *)
     1516     @(stmt_P_mp … (stmt_P_conj … Hstmt_inv Hlabel_wf))
     1517     #s * #Hstmt_vars #Hstmt_labels @conj
     1518     [ 1: (* prove that variables are either parameters or locals *)
     1519        @(stmt_vars_mp … Hstmt_vars) #i #t #H
     1520        (* Case analysis: (i, t) is either in vartypes, or in (tmp_env vartypes uv) *)
     1521        cases (local_id_split … H)
     1522        [ 1: #H' >map_append
     1523          @Exists_map [ 1: #x @(And (\fst x = i) (typ_of_type (\snd x) = t))  (* * #id #ty @(〈id, typ_of_type ty〉=〈i, t〉)*)
     1524                      | 2: whd @Exists_squeeze @(characterise_vars_all globals f ?? (sym_eq ??? E) i t H')
     1525                      | 3: * #id #ty * #E1 #E2 <E1 <E2 @refl
     1526                      ]
     1527        | 2: #EX @Exists_append_r whd in ⊢ (???%); <map_append @Exists_append_l
     1528          @Exists_map [ 1: #x @(And (\fst x = i) (typ_of_type (\snd x) = t))
     1529                      | 2: <Hfgens @EX
     1530                      | 3: * #id #ty * #E1 #E2 <E1 <E2 % @refl
     1531                      ]
     1532        ]
     1533     | 2: (* prove that labels are properly declared. *)
     1534          @(stmt_labels_mp … Hstmt_labels) #l * *
     1535          [ 1: #H assumption
     1536          | 2: * #cl_label #Hlookup lapply (Ilbls cl_label l Hlookup) #Hdefined
     1537                cases (Hlab_trans … Hdefined) #lx * #LOOKUPx >LOOKUPx in Hlookup; #Ex destruct (Ex)
     1538                #H @H
     1539          ]
     1540    ]
     1541] qed.   
    12051542
    12061543definition translate_fundef :
Note: See TracChangeset for help on using the changeset viewer.