Changeset 1316 for src/Clight


Ignore:
Timestamp:
Oct 7, 2011, 12:26:39 PM (9 years ago)
Author:
campbell
Message:

Merge in id-lookup-branch to trunk.

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src

  • src/Clight/toCminor.ma

    r1224 r1316  
    33include "Clight/TypeComparison.ma".
    44include "utilities/lists.ma".
     5include "utilities/deppair.ma".
    56
    67(* Identify local variables that must be allocated memory. *)
     
    8485definition var_types ≝ identifier_map SymbolTag var_type.
    8586
     87axiom UndeclaredIdentifier : String.
     88
     89definition lookup' ≝
     90λvars:var_types.λid. opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id).
     91
     92definition local_id : var_types → ident → Prop ≝
     93λvars,id. match lookup' vars id with [ OK t ⇒ match t with [ Global _ ⇒ False | _ ⇒ True ] | _ ⇒ False ].
     94
    8695(* Note that the semantics allows locals to shadow globals.
    8796   Parameters start out as locals, but get stack allocated if their address
     
    99108definition characterise_vars : list (ident×region) → function → var_types × nat ≝
    100109λglobals, f.
    101   let m ≝ foldl ?? (λm,idr. add ?? m (\fst idr) (Global (\snd idr))) (empty_map ??) globals in
    102   let m ≝ foldl ?? (λm,v. add ?? m (\fst v) Local) m (fn_params f) in
     110  let m ≝ foldr ?? (λidr,m. add ?? m (\fst idr) (Global (\snd idr))) (empty_map ??) globals in
    103111  let mem_vars ≝ gather_mem_vars_stmt (fn_body f) in
    104   let 〈m,stacksize〉 ≝ foldl ?? (λms,v.
     112  let 〈m,stacksize〉 ≝ foldr ?? (λv,ms.
    105113    let 〈m,stack_high〉 ≝ ms in
    106114    let 〈id,ty〉 ≝ v in
     
    111119  〈m,stacksize〉.
    112120
     121lemma local_id_add_global : ∀vars,id,r,id'.
     122  local_id (add ?? vars id (Global r)) id' → local_id vars id'.
     123#var #id #r #id'
     124whd in ⊢ (% → ?) whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?] → ?)
     125cases (identifier_eq ? id id')
     126[ #E >E >lookup_add_hit whd in ⊢ (% → ?) *
     127| #NE >lookup_add_miss // @eq_identifier_elim // #E >E in NE * /2/
     128] qed.
     129
     130lemma local_id_add_miss : ∀vars,id,t,id'.
     131  id ≠ id' → local_id (add ?? vars id t) id' → local_id vars id'.
     132#vars #id #t #id' #NE
     133whd in ⊢ (% → %)
     134whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ] → match % with [ _ ⇒ ? | _ ⇒ ? ])
     135>lookup_add_miss
     136[ #H @H | @eq_identifier_elim // #E >E in NE * /2/ ]
     137qed.
     138
     139include "utilities/extralib.ma". (* for pair_eq1 to work around destruct's excessive normalisation *)
     140
     141lemma characterise_vars_all : ∀l,f,vars,n.
     142  characterise_vars l f = 〈vars,n〉 →
     143  ∀i. local_id vars i →
     144      Exists ? (λx.\fst x = i) (fn_params f @ fn_vars f).
     145#globals #f
     146whd in ⊢ (∀_.∀_.??%? → ?)
     147elim (fn_params f @ fn_vars f)
     148[ #vars #n whd in ⊢ (??%? → ?) #E <(pair_eq1 ?????? E) -E; #i #H @False_ind
     149  elim globals in H
     150  [ normalize //
     151  | * #id #rg #t #IH whd in ⊢ (?%? → ?) #H @IH @(local_id_add_global ???? H)
     152  ]
     153| * #id #ty #tl #IH #vars #n whd in ⊢ (??(match % with [ _ ⇒ ? ])? → ?) #E #i
     154  cases (identifier_eq ? id i)
     155  [ #E' <E' #H % @refl
     156  | #NE #H whd %2 >(contract_pair var_types nat ?) in E;
     157    whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?)
     158    cases (always_alloc ty ∨ mem_set ?? id) whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?)
     159    #H' lapply (extract_pair ???????? H') -H' * #m0 * #n0 * #EQ #EQ2
     160    @(IH m0 n0)
     161    [ 1,3: @sym_eq whd in ⊢ (???(match ?????% with [ _ ⇒ ? ])) >contract_pair @EQ
     162    | 2,4: <(pair_eq1 ?????? EQ2) in H #H' @(local_id_add_miss … H') @NE
     163    ]
     164  ]
     165] qed.
    113166
    114167include "Cminor/syntax.ma".
     
    117170alias id "CMexpr" = "cic:/matita/cerco/Cminor/syntax/expr.ind(1,0,0)".
    118171
    119 axiom UndeclaredIdentifier : String.
    120172axiom BadlyTypedAccess : String.
    121173axiom BadLvalue : String.
     
    255307].
    256308
     309lemma translate_binop_vars : ∀P,op,ty1,e1,ty2,e2,ty,e.
     310  expr_vars ? e1 P →
     311  expr_vars ? e2 P →
     312  translate_binop op ty1 e1 ty2 e2 ty = OK ? e →
     313  expr_vars ? e P.
     314#P * #ty1 #e1 #ty2 #e2 #ty #e #H1 #H2
     315whd in ⊢ (??%? → ?)
     316[ cases (classify_add ty1 ty2)
     317  [ 3,4: #z ] whd in ⊢ (??%? → ?)
     318  [ generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?)
     319    * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b))
     320    whd in c:(??%?); destruct % [ @H1 | % // @H2 ]
     321  | generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?)
     322    * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b))
     323    whd in c:(??%?); destruct % [ @H2 | % // @H1 ]
     324  | *: #E destruct (E) % try @H1 @H2
     325  ]
     326| cases (classify_sub ty1 ty2)
     327  [ 3,4: #z] whd in ⊢ (??%? → ?)
     328  [ 2: generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?)
     329    * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b))
     330    whd in c:(??%?); destruct % [ % try @H1 @H2 ] @I
     331  | *: #E destruct (E) % try @H1 try @H2 % // @H2
     332  ]
     333| cases (classify_mul ty1 ty2) #E whd in E:(??%?); destruct
     334    % try @H1 @H2
     335| cases (classify_div ty1 ty2) #E whd in E:(??%?); destruct
     336    % try @H1 @H2
     337| cases (classify_mod ty1 ty2) #E whd in E:(??%?); destruct
     338    % try @H1 @H2
     339| 6,7,8,9: #E destruct % try @H1 @H2
     340| cases (classify_shr ty1 ty2) #E whd in E:(??%?); destruct % try @H1 @H2
     341| 11,12,13,14,15,16: cases (classify_cmp ty1 ty2) #E whd in E:(??%?); destruct % try @H1 @H2
     342] qed.
    257343
    258344(* We'll need to implement proper translation of pointers if we really do memory
     
    269355  ].
    270356
    271 definition translate_ptr : ∀r1,r2. CMexpr (ASTptr r1) → res (CMexpr (ASTptr r2)) ≝
    272 λr1,r2,e. check_region r1 r2 ? e.
    273 
    274 definition translate_cast : type → ∀ty2:type. CMexpr ? → res (CMexpr (typ_of_type ty2)) ≝
    275 λty1,ty2.
    276 match ty1 return λx.CMexpr (typ_of_type x) → ? with
     357definition translate_ptr : ∀P,r1,r2. (Σe:CMexpr (ASTptr r1). expr_vars ? e P) → res (Σe':CMexpr (ASTptr r2).expr_vars ? e' P) ≝
     358λP,r1,r2,e. check_region r1 r2 (λr.Σe:CMexpr (ASTptr r).expr_vars ? e P) e.
     359
     360definition translate_cast : ∀P.type → ∀ty2:type. (Σe:CMexpr ?. expr_vars ? e P) → res (Σe':CMexpr (typ_of_type ty2). expr_vars ? e' P) ≝
     361λP,ty1,ty2.
     362match ty1 return λx.(Σe:CMexpr (typ_of_type x). expr_vars ? e P) → ? with
    277363[ Tint sz1 sg1 ⇒ λe.
    278     match ty2 return λx.res (CMexpr (typ_of_type x)) with
     364    match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with
    279365    [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? (Ocastint sg1 sz2) e)
    280366    | Tfloat sz2 ⇒ OK ? (Op1 ?? (match sg1 with [ Unsigned ⇒ Ofloatofintu | _ ⇒ Ofloatofint]) e)
     
    284370    ]
    285371| Tfloat sz1 ⇒ λe.
    286     match ty2 return λx.res (CMexpr (typ_of_type x)) with
    287     [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? (match sg2 with [ Unsigned ⇒ Ointuoffloat sz2 | _ ⇒ Ointoffloat sz2 ]) e)
    288     | Tfloat sz2 ⇒ OK ? (Op1 ?? Oid e) (* FIXME *)
     372    match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with
     373    [ Tint sz2 sg2 ⇒ OK ? «Op1 ?? (match sg2 with [ Unsigned ⇒ Ointuoffloat sz2 | _ ⇒ Ointoffloat sz2 ]) e, ?»
     374    | Tfloat sz2 ⇒ OK ? «Op1 ?? Oid e, ?» (* FIXME *)
    289375    | _ ⇒ Error ? (msg TypeMismatch)
    290376    ]
    291377| Tpointer r1 _ ⇒ λe. (* will need changed for memory regions *)
    292     match ty2 return λx.res (CMexpr (typ_of_type x)) with
    293     [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? (Ointofptr sz2) e)
    294     | Tarray r2 _ _ ⇒ translate_ptr r1 r2 e
    295     | Tpointer r2 _ ⇒ translate_ptr r1 r2 e
     378    match ty2 return λx.res (Σe':CMexpr (typ_of_type x). expr_vars ? e' P) with
     379    [ Tint sz2 sg2 ⇒ OK ? «Op1 ?? (Ointofptr sz2) e, ?»
     380    | Tarray r2 _ _ ⇒ translate_ptr ? r1 r2 e
     381    | Tpointer r2 _ ⇒ translate_ptr ? r1 r2 e
    296382    | _ ⇒ Error ? (msg TypeMismatch)
    297383    ]
    298384| Tarray r1 _ _ ⇒ λe. (* will need changed for memory regions *)
    299     match ty2 return λx.res (CMexpr (typ_of_type x)) with
    300     [ Tint sz2 sg2 ⇒ OK ? (Op1 (ASTptr r1) (ASTint sz2 sg2) (Ointofptr sz2) e)
    301     | Tarray r2 _ _ ⇒ translate_ptr r1 r2 e
    302     | Tpointer r2 _ ⇒ translate_ptr r1 r2 e
     385    match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with
     386    [ Tint sz2 sg2 ⇒ OK ? «Op1 (ASTptr r1) (ASTint sz2 sg2) (Ointofptr sz2) e, ?»
     387    | Tarray r2 _ _ ⇒ translate_ptr ? r1 r2 e
     388    | Tpointer r2 _ ⇒ translate_ptr ? r1 r2 e
    303389    | _ ⇒ Error ? (msg TypeMismatch)
    304390    ]
    305391| _ ⇒ λ_. Error ? (msg TypeMismatch)
    306 ].
     392]. whd @use_sig qed.
    307393
    308394definition type_should_eq : ∀ty1,ty2. ∀P:type → Type[0]. P ty1 → res (P ty2) ≝
     
    335421] qed.
    336422
    337 let rec translate_expr (vars:var_types) (e:expr) on e : res (CMexpr (typ_of_type (typeof e))) ≝
    338 match e return λe. res (CMexpr (typ_of_type (typeof e))) with
     423let rec translate_expr (vars:var_types) (e:expr) on e : res (Σe':CMexpr (typ_of_type (typeof e)). expr_vars ? e' (local_id vars)) ≝
     424match e return λe. res (Σe':CMexpr (typ_of_type (typeof e)). expr_vars ? e' (local_id vars)) with
    339425[ Expr ed ty ⇒
    340426  match ed with
    341   [ Econst_int sz i ⇒ OK ? (Cst ? (Ointconst sz i))
    342   | Econst_float f ⇒ OK ? (Cst ? (Ofloatconst f))
     427  [ Econst_int sz i ⇒ OK ? «Cst ? (Ointconst sz i), ?»
     428  | Econst_float f ⇒ OK ? «Cst ? (Ofloatconst f), ?»
    343429  | Evar id ⇒
    344       do c ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id);
    345       match c with
    346       [ Global r ⇒
     430      do c as E ← lookup' vars id;
     431      match c return λx.? = ? → res (Σe':CMexpr ?. ?) with
     432      [ Global r ⇒ λ_.
    347433          match access_mode ty with
    348           [ By_value q ⇒ OK ? (Mem ? r q (Cst ? (Oaddrsymbol id 0)))
    349           | By_reference _ ⇒ OK ? (Cst ? (Oaddrsymbol id 0))
     434          [ By_value q ⇒ OK ? «Mem ? r q (Cst ? (Oaddrsymbol id 0)), ?»
     435          | By_reference _ ⇒ OK ? «Cst ? (Oaddrsymbol id 0), ?»
    350436          | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
    351437          ]
    352       | Stack n ⇒
     438      | Stack n ⇒ λE.
    353439          match access_mode ty with
    354           [ By_value q ⇒ OK ? (Mem ? Any q (Cst ? (Oaddrstack n)))
    355           | By_reference _ ⇒ OK ? (Cst ? (Oaddrstack n))
     440          [ By_value q ⇒ OK ? «Mem ? Any q (Cst ? (Oaddrstack n)), ?»
     441          | By_reference _ ⇒ OK ? «Cst ? (Oaddrstack n), ?»
    356442          | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
    357443          ]
    358       | Local ⇒ OK ? (Id ? id)
    359       ]
     444      | Local ⇒ λE. OK ? «Id ? id, ?»
     445      ] E
    360446  | Ederef e1 ⇒
    361447      do e1' ← translate_expr vars e1;
    362       match typ_of_type (typeof e1) return λx.CMexpr x → ? with
     448      match typ_of_type (typeof e1) return λx.(Σz:CMexpr x.expr_vars ? z (local_id vars)) → ? with
    363449      [ ASTptr r ⇒ λe1'.
    364           match access_mode ty return λx.access_mode ty = x → res (CMexpr (typ_of_type ty)) with
    365           [ By_value q ⇒ λ_.OK ? (Mem (typ_of_type ty) ? q e1')
    366           | By_reference r' ⇒ λE. (region_should_eq r r' ? e1')⌈CMexpr (ASTptr r') ↦ CMexpr (typ_of_type ty)⌉
     450          match access_mode ty return λx.? → res (Σe':CMexpr (typ_of_type ty). expr_vars ? e' (local_id vars)) with
     451          [ By_value q ⇒ λ_.OK ? «Mem (typ_of_type ty) ? q (eject … e1'), ?»
     452          | By_reference r' ⇒ λE. do e1' ← region_should_eq r r' ? e1';
     453                                  OK ? e1'⌈Σe':CMexpr ?. expr_vars ? e' (local_id vars) ↦ Σe':CMexpr (typ_of_type ty). expr_vars ? e' (local_id vars)⌉
    367454          | By_nothing ⇒ λ_. Error ? (msg BadlyTypedAccess)
    368           ] (refl ? (access_mode ty))
     455          ] (access_mode_typ ty)
    369456      | _ ⇒ λ_. Error ? (msg TypeMismatch)
    370457      ] e1'
    371458  | Eaddrof e1 ⇒
    372459      do e1' ← translate_addr vars e1;
    373       match typ_of_type ty return λx.res (CMexpr x) with
     460      match typ_of_type ty return λx.res (Σz:CMexpr x.?) with
    374461      [ ASTptr r ⇒
    375462          match e1' with
     
    381468      do op' ← translate_unop ty op;
    382469      do e1' ← translate_expr vars e1;
    383       OK ? (Op1 ?? op' e1')
     470      OK ? «Op1 ?? op' e1', ?»
    384471  | Ebinop op e1 e2 ⇒
    385472      do e1' ← translate_expr vars e1;
    386473      do e2' ← translate_expr vars e2;
    387       translate_binop op (typeof e1) e1' (typeof e2) e2' ty
     474      do e' as E ← translate_binop op (typeof e1) e1' (typeof e2) e2' ty;
     475      OK ? «e', ?»
    388476  | Ecast ty1 e1 ⇒
    389477      do e1' ← translate_expr vars e1;
    390       do e' ← translate_cast (typeof e1) ty1 e1';
    391       typ_should_eq ? (typ_of_type ty) ? e'
     478      do e' ← translate_cast ? (typeof e1) ty1 e1';
     479      do e' ← typ_should_eq (typ_of_type ty1) (typ_of_type ty) ? e';
     480      OK ? e'
    392481  | Econdition e1 e2 e3 ⇒
    393482      do e1' ← translate_expr vars e1;
    394483      do e2' ← translate_expr vars e2;
    395       do e2' ← type_should_eq ? ty (λx.CMexpr (typ_of_type x)) e2';
     484      do e2' ← type_should_eq ? ty (λx.Σe:CMexpr (typ_of_type x).?) e2';
    396485      do e3' ← translate_expr vars e3;
    397       do e3' ← type_should_eq ? ty (λx.CMexpr (typ_of_type x)) e3';
    398       match typ_of_type (typeof e1) return λx.CMexpr x → ? with
    399       [ ASTint _ _ ⇒ λe1'. OK ? (Cond ??? e1' e2' e3')
     486      do e3' ← type_should_eq ? ty (λx.Σe:CMexpr (typ_of_type x).?) e3';
     487      match typ_of_type (typeof e1) return λx.(Σe1':CMexpr x. expr_vars ? e1' (local_id vars)) → ? with
     488      [ ASTint _ _ ⇒ λe1'. OK ? «Cond ??? e1' e2' e3', ?»
    400489      | _ ⇒ λ_.Error ? (msg TypeMismatch)
    401490      ] e1'
     
    405494      match ty with
    406495      [ Tint sz _ ⇒
    407         do e2' ← type_should_eq ? ty (λx.CMexpr (typ_of_type x)) e2';
    408         match typ_of_type (typeof e1) return λx.CMexpr x → res (CMexpr (typ_of_type ty)) with
    409         [ ASTint _ _ ⇒ λe1'. OK ? (Cond ??? e1' e2' (Cst ? (Ointconst sz (zero ?))))
     496        do e2' ← type_should_eq ? ty (λx.Σe:CMexpr (typ_of_type x).?) e2';
     497        match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e (local_id vars)) → res ? with
     498        [ ASTint _ _ ⇒ λe1'. OK ? «Cond ??? e1' e2' (Cst ? (Ointconst sz (zero ?))), ?»
    410499        | _ ⇒ λ_.Error ? (msg TypeMismatch)
    411500        ] e1'
     
    417506      match ty with
    418507      [ Tint sz _ ⇒
    419         do e2' ← type_should_eq ? ty (λx.CMexpr (typ_of_type x)) e2';
    420         match typ_of_type (typeof e1) return λx.CMexpr x → res (CMexpr (typ_of_type ty)) with
    421         [ ASTint _ _ ⇒ λe1'. OK ? (Cond ??? e1' (Cst ? (Ointconst sz (repr ? 1))) e2')
     508        do e2' ← type_should_eq ? ty (λx.Σe:CMexpr (typ_of_type x).?) e2';
     509        match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e (local_id vars)) → ? with
     510        [ ASTint _ _ ⇒ λe1'. OK ? «Cond ??? e1' (Cst ? (Ointconst sz (repr ? 1))) e2', ?»
    422511        | _ ⇒ λ_.Error ? (msg TypeMismatch)
    423512        ] e1'
     
    426515  | Esizeof ty1 ⇒
    427516      match ty with
    428       [ Tint sz _ ⇒ OK ? (Cst ? (Ointconst sz (repr ? (sizeof ty1))))
     517      [ Tint sz _ ⇒ OK ? «Cst ? (Ointconst sz (repr ? (sizeof ty1))), ?»
    429518      | _ ⇒ Error ? (msg TypeMismatch)
    430519      ]
    431520  | Efield e1 id ⇒
    432       do e' ← match typeof e1 with
     521      match typeof e1 with
    433522      [ Tstruct _ fl ⇒
    434523          do e1' ← translate_addr vars e1;
     
    437526            do off ← field_offset id fl;
    438527            match access_mode ty with
    439             [ By_value q ⇒ OK ? (Mem ? r q (Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst I32 (repr ? off)))))
    440             | By_reference _ ⇒ OK ? (Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst I32 (repr ? off))))
     528            [ By_value q ⇒ OK ? «Mem ? r q (Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst I32 (repr ? off)))),?»
     529            | By_reference _ ⇒ OK ? «Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst I32 (repr ? off))),?»
    441530            | By_nothing ⇒ Error ? (msg BadlyTypedAccess)
    442531            ]
     
    446535          match e1' with
    447536          [ dp r e1' ⇒
    448             match access_mode ty return λx. access_mode ty = x → res (CMexpr (typ_of_type ty)) with
    449             [ By_value q ⇒ λ_. OK ? (Mem ?? q e1')
    450             | By_reference r' ⇒ λE. (region_should_eq r r' ? e1')⌈res (CMexpr (ASTptr r')) ↦ res (CMexpr (typ_of_type ty))⌉
     537            match access_mode ty return λx. access_mode ty = x → res ? with
     538            [ By_value q ⇒ λ_. OK ? «Mem ?? q e1', ?»
     539            | By_reference r' ⇒  λE. do e1' ← region_should_eq r r' ? e1';
     540                                OK ? e1'⌈Σz:CMexpr (ASTptr r').? ↦ Σz:CMexpr (typ_of_type ty).?⌉
    451541            | By_nothing ⇒ λ_. Error ? (msg BadlyTypedAccess)
    452542            ] (refl ? (access_mode ty))
    453543          ]
    454544      | _ ⇒ Error ? (msg BadlyTypedAccess)
    455       ];
    456       typ_should_eq ? (typ_of_type ty) ? e'
     545      ]
    457546  | Ecost l e1 ⇒
    458547      do e1' ← translate_expr vars e1;
    459       do e' ← OK ? (Ecost ? l e1');
    460       typ_should_eq ? (typ_of_type ty) ? e'
    461   ]
    462 ] and translate_addr (vars:var_types) (e:expr) on e : res (Σr.CMexpr (ASTptr r)) ≝
     548      do e' ← OK ? «Ecost ? l e1',?»;
     549      typ_should_eq (typ_of_type (typeof e1)) (typ_of_type ty) (λx.Σe:CMexpr x.?) e'
     550  ]
     551] and translate_addr (vars:var_types) (e:expr) on e : res (Σr. Σe':CMexpr (ASTptr r). expr_vars ? e' (local_id vars)) ≝
    463552match e with
    464553[ Expr ed _ ⇒
     
    466555  [ Evar id ⇒
    467556      do c ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id);
    468       match c return λ_. res (Σr.CMexpr (ASTptr r)) with
    469       [ Global r ⇒ OK ? (dp ?? r (Cst ? (Oaddrsymbol id 0)))
    470       | Stack n ⇒ OK ? (dp ?? Any (Cst ? (Oaddrstack n)))
     557      match c return λ_. res (Σr.Σz:CMexpr (ASTptr r).?) with
     558      [ Global r ⇒ OK ? «r, «Cst ? (Oaddrsymbol id 0), ?»»
     559      | Stack n ⇒ OK ? «Any, «Cst ? (Oaddrstack n), ?»»
    471560      | Local ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id] (* TODO: could rule out? *)
    472561      ]
    473562  | Ederef e1 ⇒
    474563      do e1' ← translate_expr vars e1;
    475       match typ_of_type (typeof e1) return λx. CMexpr x → res (Σr. CMexpr (ASTptr r)) with
    476       [ ASTptr r ⇒ λe1'.OK ? (dp ?? r e1')
     564      match typ_of_type (typeof e1) return λx. (Σz:CMexpr x.expr_vars ? z (local_id vars)) → res (Σr. Σz:CMexpr (ASTptr r). ?) with
     565      [ ASTptr r ⇒ λe1'.OK ? «r, e1'»
    477566      | _ ⇒ λ_.Error ? (msg BadlyTypedAccess)
    478567      ] e1'
     
    483572          do off ← field_offset id fl;
    484573          match e1' with
    485           [ dp r e1' ⇒ OK ? (dp ?? r (Op2 (ASTptr r) (ASTint I32 Unsigned (* FIXME inefficient?*)) (ASTptr r) Oaddp e1' (Cst ? (Ointconst I32 (repr ? off)))))
     574          [ dp r e1'' ⇒ OK (Σr:region.Σe:CMexpr (ASTptr r).?) («r, «Op2 (ASTptr r) (ASTint I32 Unsigned (* FIXME inefficient?*)) (ASTptr r) Oaddp e1'' (Cst ? (Ointconst I32 (repr ? off))), ?» »)
    486575          ]
    487576      | Tunion _ _ ⇒ translate_addr vars e1
     
    491580  ]
    492581].
    493 >(access_mode_typ … E) @refl
    494 qed.
    495 
    496 inductive destination : Type[0] ≝
    497 | IdDest : ident → destination
    498 | MemDest : ∀r:region. memory_chunk → CMexpr (ASTptr r) → destination.
     582whd try @I
     583[ >E @I
     584| >(E ? (refl ??)) @refl
     585| 3,4: @use_sig
     586| @(translate_binop_vars … E) @use_sig
     587| % [ % ] @use_sig
     588| % [ % @use_sig ] whd @I
     589| % [ % [ @use_sig | @I ] | @use_sig ]
     590| % [ @use_sig | @I ]
     591| % [ @use_sig | @I ]
     592| >(access_mode_typ … E) @refl
     593| @use_sig
     594| @use_sig
     595| % [ @use_sig | @I ]
     596] qed.
     597
     598inductive destination (vars:var_types) : Type[0] ≝
     599| IdDest : ∀id:ident. local_id vars id → destination vars
     600| MemDest : ∀r:region. memory_chunk → (Σe:CMexpr (ASTptr r).expr_vars ? e (local_id vars)) → destination vars.
    499601
    500602definition translate_dest ≝
     
    509611        match ed1 with
    510612        [ Evar id ⇒
    511             do c ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id);
    512             match c with
    513             [ Local ⇒ OK ? (IdDest id)
    514             | Global r ⇒ OK ? (MemDest r q (Cst ? (Oaddrsymbol id 0)))
    515             | Stack n ⇒ OK ? (MemDest Any q (Cst ? (Oaddrstack n)))
    516             ]
     613            do c as E ← lookup' vars id;
     614            match c return λx.? → ? with
     615            [ Local ⇒ λE. OK ? (IdDest vars id ?)
     616            | Global r ⇒ λE. OK ? (MemDest ? r q (Cst ? (Oaddrsymbol id 0)))
     617            | Stack n ⇒ λE. OK ? (MemDest ? Any q (Cst ? (Oaddrstack n)))
     618            ] E
    517619        | _ ⇒
    518620            do e1' ← translate_addr vars e1;
    519             match e1' with [ dp r e1' ⇒ OK ? (MemDest r q e1') ]
     621            match e1' with [ dp r e1' ⇒ OK ? (MemDest ? r q e1') ]
    520622        ]
    521623    ].
    522 
    523 definition translate_assign ≝
     624whd // >E @I
     625qed.
     626
     627definition lenv ≝ identifier_map SymbolTag (identifier Label).
     628
     629axiom MissingLabel : String.
     630
     631definition lookup_label ≝
     632λlbls:lenv.λl. opt_to_res … [MSG MissingLabel; CTX ? l] (lookup ?? lbls l).
     633
     634definition lpresent ≝ λlbls:lenv. λl. ∃l'. lookup_label lbls l' = OK ? l.
     635
     636let rec labels_defined (s:statement) : list ident ≝
     637match s with
     638[ Ssequence s1 s2 ⇒ labels_defined s1 @ labels_defined s2
     639| Sifthenelse _ s1 s2 ⇒ labels_defined s1 @ labels_defined s2
     640| Swhile _ s ⇒ labels_defined s
     641| Sdowhile _ s ⇒ labels_defined s
     642| Sfor s1 _ s2 s3 ⇒ labels_defined s1 @ labels_defined s2 @ labels_defined s3
     643| Sswitch _ ls ⇒ labels_defined_switch ls
     644| Slabel l s ⇒ l::(labels_defined s)
     645| Scost _ s ⇒ labels_defined s
     646| _ ⇒ [ ]
     647]
     648and labels_defined_switch (ls:labeled_statements) : list ident ≝
     649match ls with
     650[ LSdefault s ⇒ labels_defined s
     651| LScase _ _ s ls ⇒ labels_defined s @ labels_defined_switch ls
     652].
     653
     654definition ldefined ≝ λs.λl.Exists ? (λl'.l' = l) (labels_of s).
     655
     656definition labels_translated : lenv → statement → stmt → Prop ≝
     657λlbls,s,s'.  ∀l.
     658  (Exists ? (λl'.l' = l) (labels_defined s)) →
     659  ∃l'. lookup_label lbls l = OK ? l' ∧ ldefined s' l'.
     660
     661definition stmt_inv ≝
     662λvars. λlbls:lenv.
     663  stmt_P (λs.stmt_vars (local_id vars) s ∧ stmt_labels (lpresent lbls) s).
     664
     665definition translate_assign : ∀vars:var_types. expr → expr → res (Σs:stmt.∀ls. stmt_inv vars ls s) ≝
    524666λvars,e1,e2.
    525667do e2' ← translate_expr vars e2;
    526668do dest ← translate_dest vars e1 (typeof e2);
    527669match dest with
    528 [ IdDest id ⇒ OK ? (St_assign ? id e2')
    529 | MemDest r q e1' ⇒ OK ? (St_store ? r q e1' e2')
    530 ].
     670[ IdDest id p ⇒ OK ? «St_assign ? id e2', ?»
     671| MemDest r q e1' ⇒ OK ? «St_store ? r q e1' e2', ?»
     672].
     673#ls whd %
     674[ % // @use_sig
     675| @I
     676| % @use_sig
     677| @I
     678] qed.
    531679
    532680definition m_option_map : ∀A,B:Type[0]. (A → res B) → option A → res (option B) ≝
     
    537685].
    538686
    539 definition translate_expr_sigma : var_types → expr → res (Σt:typ.CMexpr t) ≝
     687definition translate_expr_sigma : ∀vars:var_types. expr → res (Σe:(Σt:typ.CMexpr t). match e with [ dp t e ⇒ expr_vars t e (local_id vars) ]) ≝
    540688λv,e.
    541689  do e' ← translate_expr v e;
    542   OK ? (dp ? (λt:typ.CMexpr t) ? e').
     690  OK (Σe:(Σt:typ.CMexpr t).?) ««?, e'», ?».
     691whd @use_sig
     692qed.
    543693
    544694axiom FIXME : String.
     
    554704  〈tmp, mk_tmpgen u (〈tmp, typ_of_memory_chunk c〉::(tmp_env g))〉.
    555705
    556 let rec translate_statement (vars:var_types) (u:tmpgen) (s:statement) on s : res (stmt×tmpgen) ≝
    557 match s with
    558 [ Sskip ⇒ OK ? 〈St_skip, u〉
    559 | Sassign e1 e2 ⇒ do s' ← translate_assign vars e1 e2; OK ? 〈s',u〉
     706lemma lookup_label_hit : ∀lbls,l,l'.
     707  lookup_label lbls l = OK ? l' →
     708  lpresent lbls l'.
     709#lbls #l #l' #E whd %{l} @E
     710qed.
     711
     712definition add_tmps : var_types → tmpgen → var_types ≝
     713λvs,g.
     714  foldr ?? (λidty,vs. add ?? vs (\fst idty) Local) vs (tmp_env g).
     715
     716definition tmps_preserved : var_types → tmpgen → tmpgen → Prop ≝
     717λvars,u1,u2.
     718  ∀id. local_id (add_tmps vars u1) id → local_id (add_tmps vars u2) id.
     719
     720lemma alloc_tmp_preserves : ∀tmp,u,u',vars,q.
     721  〈tmp,u'〉 = alloc_tmp q u → tmps_preserved vars u u'.
     722#tmp #g #g' #vars #q
     723whd in ⊢ (???% → ?)
     724generalize in ⊢ (???(match % with [ _ ⇒ ? ]) → ?)
     725* #tmp' #u whd in ⊢ (???% → ?) #E
     726>(pair_eq2 ?????? E)
     727#id #H
     728whd in ⊢ (?%?) whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ]
     729cases (identifier_eq ? id tmp')
     730[ #E1 >E1 >lookup_add_hit @I
     731| * #NE >lookup_add_miss [ @H | @eq_identifier_elim // #E1 cases (NE E1)
     732] qed.
     733
     734definition trans_inv : var_types → lenv → statement → tmpgen → (stmt×tmpgen) → Prop ≝
     735λvars,lbls,s,u,su'.
     736  let 〈s',u'〉 ≝ su' in
     737  stmt_inv (add_tmps vars u') lbls s' ∧
     738  labels_translated lbls s s' ∧
     739  tmps_preserved vars u u'.
     740
     741lemma trans_inv_stmt_inv : ∀vars,lbls,s,u,su.
     742  trans_inv vars lbls s u su → stmt_inv (add_tmps vars (\snd su)) lbls (\fst su).
     743#var #lbls #s #u * #s' #u' * * #H1 #H2 #H3 @H1
     744qed.
     745
     746lemma trans_inv_labels : ∀vars,lbls,s,u,su.
     747  trans_inv vars lbls s u su → labels_translated lbls s (\fst su).
     748#vars #lbls #s #u * #s' #u' * * #_ #H #_ @H
     749qed.
     750
     751lemma local_id_add_local_oblivious : ∀vars,id,id'.
     752  local_id vars id → local_id (add ?? vars id' Local) id.
     753#vars #id #id' #H whd whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
     754cases (identifier_eq ? id id')
     755[ #E >E >lookup_add_hit @I
     756| * #NE >lookup_add_miss [ @H | @eq_identifier_elim // #E cases (NE E)
     757] qed.
     758
     759lemma local_id_add_tmps_oblivious : ∀vars,id,u.
     760  local_id vars id → local_id (add_tmps vars u) id.
     761#vars #id * #u #l #H elim l
     762[ //
     763| * #id' #ty #tl @local_id_add_local_oblivious
     764] qed.
     765
     766lemma add_tmps_oblivious : ∀vars,lbls,s,u.
     767  stmt_inv vars lbls s → stmt_inv (add_tmps vars u) lbls s.
     768#vars #lbls #s #u #H
     769@(stmt_P_mp … H)
     770#s' * #H1 #H2 %
     771[ @(stmt_vars_mp … H1)
     772  #id @local_id_add_tmps_oblivious
     773| @H2
     774] qed.
     775
     776lemma local_id_fresh_tmp : ∀tmp,u,q,u0,vars.
     777  〈tmp,u〉 = alloc_tmp q u0 → local_id (add_tmps vars u) tmp.
     778#tmp #u #q #u0 #vars
     779whd in ⊢ (???% → ?)
     780generalize in ⊢ (???(match % with [ _ ⇒ ? ]) → ?)
     781* #tmp' #u' whd in ⊢ (???% → ?) #E
     782>(pair_eq1 ?????? E) >(pair_eq2 ?????? E)
     783whd in ⊢ (?%?) whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ] >lookup_add_hit
     784@I
     785qed.
     786
     787lemma use_sig' : ∀A.∀P,P':A → Prop. (∀x.P x → P' x) → ∀x:Σx:A.P x. P' x.
     788#A #P #P' #H1 * #x #H2 @H1 @H2
     789qed.
     790
     791definition sigbind2 : ∀A,B,C:Type[0]. ∀P:A×B → Prop. res (Σx:A×B.P x) → (∀a,b. P 〈a,b〉 → res C) → res C ≝
     792λA,B,C,P,e,f.
     793  match e with
     794  [ OK v ⇒ match v with [ dp v' p ⇒ match v' return λv'. P v' → res C with [ pair a b ⇒ f a b ] p ]
     795  | Error msg ⇒ Error ? msg
     796  ].
     797
     798notation > "vbox('do' 〈ident v1, ident v2〉 'with' ident H ← e; break e')" with precedence 40 for @{'sigbind2 ${e} (λ${ident v1}.λ${ident v2}.λ${ident H}.${e'})}.
     799(*
     800notation > "vbox('do' 〈ident v1 : ty1, ident v2 : ty2〉 ← e; break e')" with precedence 40 for @{'bind2 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.${e'})}.
     801notation < "vbox('do' \nbsp 〈ident v1, ident v2〉 ← e; break e')" with precedence 40 for @{'bind2 ${e} (λ${ident v1}.λ${ident v2}.${e'})}.
     802notation < "vbox('do' \nbsp 〈ident v1 : ty1, ident v2 : ty2〉 ← e; break e')" with precedence 40 for @{'bind2 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.${e'})}.
     803*)
     804interpretation "error monad sig Prod bind" 'sigbind2 e f = (sigbind2 ???? e f).
     805
     806let rec translate_statement (vars:var_types) (lbls:lenv) (u:tmpgen) (s:statement) on s : res (Σsu:stmt×tmpgen.trans_inv vars lbls s u su) ≝
     807match s return λs.res (Σsu:stmt×tmpgen.trans_inv vars lbls s u su) with
     808[ Sskip ⇒ OK ? «〈St_skip, u〉, ?»
     809| Sassign e1 e2 ⇒
     810    do s' ← translate_assign vars e1 e2;
     811    OK ? «〈eject ?? s', u〉, ?»
    560812| Scall ret ef args ⇒
    561813    do ef' ← translate_expr vars ef;
    562     do ef' ← typ_should_eq ? (ASTptr Code) ? ef';
    563     do args' ← mmap … (translate_expr_sigma vars) args;
     814    do ef' ← typ_should_eq (typ_of_type (typeof ef)) (ASTptr Code) ? ef';
     815    do args' ← mmap_sigma … (translate_expr_sigma vars) args;
    564816    match ret with
    565     [ None ⇒ OK ? 〈St_call (None ?) ef' args', u〉
     817    [ None ⇒ OK ? «〈St_call (None ?) ef' args', u〉, ?»
    566818    | Some e1 ⇒
    567819        do dest ← translate_dest vars e1 (typeof e1); (* TODO: check if it's sane to use e1's type rather than the return type *)
    568820        match dest with
    569         [ IdDest id ⇒ OK ? 〈St_call (Some ? id) ef' args', u〉
     821        [ IdDest id p ⇒ OK ? «〈St_call (Some ? id) ef' args', u〉, ?»
    570822        | MemDest r q e1' ⇒
    571             let 〈tmp, u〉 ≝ alloc_tmp q u in
    572             OK ? 〈St_seq (St_call (Some ? tmp) ef' args') (St_store (typ_of_memory_chunk q) r q e1' (Id ? tmp)), u〉
     823            let 〈tmp, u〉 as Etmp ≝ alloc_tmp q u in
     824            OK ? «〈St_seq (St_call (Some ? tmp) ef' args') (St_store (typ_of_memory_chunk q) r q e1' (Id ? tmp)), u〉, ?»
    573825        ]
    574826    ]
    575827| Ssequence s1 s2 ⇒
    576     do 〈s1', u〉 ← translate_statement vars u s1;
    577     do 〈s2', u〉 ← translate_statement vars u s2;
    578     OK ? 〈St_seq s1' s2', u〉
     828    do 〈s1', u1〉 with H1 ← translate_statement vars lbls u s1;
     829    do 〈s2', u2〉 with H2 ← translate_statement vars lbls u1 s2;
     830    OK ? «〈St_seq s1' s2', u2〉, ?»
    579831| Sifthenelse e1 s1 s2 ⇒
    580832    do e1' ← translate_expr vars e1;
    581     match typ_of_type (typeof e1) return λx.CMexpr x → ? with
     833    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with
    582834    [ ASTint _ _ ⇒ λe1'.
    583         do 〈s1', u〉 ← translate_statement vars u s1;
    584         do 〈s2', u〉 ← translate_statement vars u s2;
    585         OK ? 〈St_ifthenelse ?? e1' s1' s2', u〉
     835        do 〈s1', u〉 with H1 ← translate_statement vars lbls u s1;
     836        do 〈s2', u〉 with H2 ← translate_statement vars lbls u s2;
     837        OK ? «〈St_ifthenelse ?? e1' s1' s2', u〉, ?»
    586838    | _ ⇒ λ_.Error ? (msg TypeMismatch)
    587839    ] e1'
    588840| Swhile e1 s1 ⇒
    589841    do e1' ← translate_expr vars e1;
    590     match typ_of_type (typeof e1) return λx.CMexpr x → ? with
     842    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with
    591843    [ ASTint _ _ ⇒ λe1'.
    592         do 〈s1', u〉 ← translate_statement vars u s1;
     844        do 〈s1', u〉 with H1 ← translate_statement vars lbls u s1;
    593845        (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
    594         OK ? 〈St_block
     846        OK ? «〈St_block
    595847               (St_loop
    596                  (St_ifthenelse ?? e1' (St_block s1') (St_exit 0))), u〉
     848                 (St_ifthenelse ?? e1' (St_block s1') (St_exit 0))), u〉, ?»
    597849    | _ ⇒ λ_.Error ? (msg TypeMismatch)
    598850    ] e1'
    599851| Sdowhile e1 s1 ⇒
    600852    do e1' ← translate_expr vars e1;
    601     match typ_of_type (typeof e1) return λx.CMexpr x → ? with
     853    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → ? with
    602854    [ ASTint _ _ ⇒ λe1'.
    603         do 〈s1',u〉 ← translate_statement vars u s1;
     855        do 〈s1',u〉 with H1 ← translate_statement vars lbls u s1;
    604856        (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
    605         OK ? 〈St_block
     857        OK ? «〈St_block
    606858               (St_loop
    607                  (St_seq (St_block s1') (St_ifthenelse ?? e1' St_skip (St_exit 0)))), u〉
     859                 (St_seq (St_block s1') (St_ifthenelse ?? e1' St_skip (St_exit 0)))), u〉, ?»
    608860    | _ ⇒ λ_.Error ? (msg TypeMismatch)
    609861    ] e1'
    610862| Sfor s1 e1 s2 s3 ⇒
    611863    do e1' ← translate_expr vars e1;
    612     match typ_of_type (typeof e1) return λx.CMexpr x → ? with
     864    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → ? with
    613865    [ ASTint _ _ ⇒ λe1'.
    614         do 〈s1', u〉 ← translate_statement vars u s1;
    615         do 〈s2', u〉 ← translate_statement vars u s2;
    616         do 〈s3', u〉 ← translate_statement vars u s3;
     866        do 〈s1', u〉 with H1 ← translate_statement vars lbls u s1;
     867        do 〈s2', u〉 with H2 ← translate_statement vars lbls u s2;
     868        do 〈s3', u〉 with H3 ← translate_statement vars lbls u s3;
    617869        (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
    618         OK ? 〈St_seq s1'
     870        OK ? «〈St_seq s1'
    619871             (St_block
    620872               (St_loop
    621                  (St_ifthenelse ?? e1' (St_seq (St_block s3') s2') (St_exit 0)))), u〉
     873                 (St_ifthenelse ?? e1' (St_seq (St_block s3') s2') (St_exit 0)))), u〉, ?»
    622874    | _ ⇒ λ_.Error ? (msg TypeMismatch)
    623875    ] e1'
    624 | Sbreak ⇒ OK ? 〈St_exit 1, u〉
    625 | Scontinue ⇒ OK ? 〈St_exit 0, u〉
     876| Sbreak ⇒ OK ? «〈St_exit 1, u〉, ?»
     877| Scontinue ⇒ OK ? «〈St_exit 0, u〉, ?»
    626878| Sreturn ret ⇒
    627879    match ret with
    628     [ None ⇒ OK ? 〈St_return (None ?), u〉
     880    [ None ⇒ OK ? «〈St_return (None ?), u〉, ?»
    629881    | Some e1 ⇒
    630882        do e1' ← translate_expr vars e1;
    631         OK ? 〈St_return (Some ? (dp … e1')), u〉
     883        OK ? «〈St_return (Some ? (dp … e1')), u〉, ?»
    632884    ]
    633885| Sswitch e1 ls ⇒ Error ? (msg FIXME)
    634886| Slabel l s1 ⇒
    635     do 〈s1', u〉 ← translate_statement vars u s1;
    636     OK ? 〈St_label l s1', u〉
    637 | Sgoto l ⇒ OK ? 〈St_goto l, u〉
     887    do l' as E ← lookup_label lbls l;
     888    do 〈s1', u〉 with H1 ← translate_statement vars lbls u s1;
     889    OK ? «〈St_label l' s1', u〉, ?»
     890| Sgoto l ⇒
     891    do l' as E ← lookup_label lbls l;
     892    OK ? «〈St_goto l', u〉, ?»
    638893| Scost l s1 ⇒
    639     do 〈s1', u〉 ← translate_statement vars u s1;
    640     OK ? 〈St_cost l s1', u〉
    641 ].
     894    do 〈s1', u〉 with H1 ← translate_statement vars lbls u s1;
     895    OK ? «〈St_cost l s1', u〉, ?»
     896].
     897try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj
     898try @I
     899try (#l #H @(match H in False with [ ]))
     900try (#id #H @H)
     901[ @add_tmps_oblivious @(use_sig ?? s')
     902| @local_id_add_tmps_oblivious @p
     903]
     904try (@use_sig' #x @expr_vars_mp #i @local_id_add_tmps_oblivious)
     905[ 1,3,6: @use_sig' #x @All_mp * #ty #e @expr_vars_mp #i @local_id_add_tmps_oblivious
     906| 2,4: @(local_id_fresh_tmp … Etmp)
     907| @(alloc_tmp_preserves … Etmp)
     908| 7,11: @(stmt_P_mp … (π1 (π1 H1))) #s * #H3 #H4 % [ 1,3: @(stmt_vars_mp … H3) cases H2 #_ #H @H | *: @H4 ]
     909| 8,12: @(trans_inv_stmt_inv … H2)
     910| 9,13: #l #H cases (Exists_append … H)
     911  [ 1,3: #H3 cases H1 * #S1 #L1 #T1 cases (L1 l H3) #l' * #E1 #D1
     912    %{l'} % [ 1,3: @E1 | *: @Exists_append_l @D1 ]
     913  | *: #H3 cases H2 * #S2 #L2 #T2 cases (L2 l H3) #l' * #E2 #D2
     914    %{l'} % [ 1,3: @E2 | *: @Exists_append_r @D2 ]
     915  ]
     916| 10,14: cases H2 #_ #TP2 #id #L @TP2 cases H1 #_ #TP1 @TP1 @L
     917| 15,18: @(π1 (π1 H1))
     918| 16,19: cases H1 * #_ #L1 #_ #l #H cases (L1 l H) #l' * #E1 #D1
     919  %{l'} % [ 1,3: @E1 | *: @Exists_append_l @D1 ]
     920| 17,20: @(π2 H1)
     921(* Sfor *)
     922| @(stmt_P_mp … (π1 (π1 H1))) #s * #H4 #H5 % [ @(stmt_vars_mp … H4) #id #H @(π2 H3) @(π2 H2) @H | @H5 ]
     923| @(π1 (π1 H3))
     924| @(stmt_P_mp … (π1 (π1 H2))) #s * #H4 #H5 % [ @(stmt_vars_mp … H4) #id #H @(π2 H3) @H | @H5 ]
     925| #l #H cases (Exists_append … H)
     926  [ #EX1 cases H1 * #S1 #L1 #_ cases (L1 l EX1) #l' * #E1 #D1
     927    %{l'} % [ @E1 | @Exists_append_l @D1 ]
     928  | #EX cases (Exists_append … EX)
     929    [ #EX2 cases H2 * #S2 #L2 #_ cases (L2 l EX2) #l' * #E2 #D2
     930      %{l'} % [ @E2 | @Exists_append_r @Exists_append_l @Exists_append_r @D2 ]
     931    | #EX3 cases H3 * #S3 #L3 #_ cases (L3 l EX3) #l' * #E3 #D3
     932      %{l'} % [ @E3 | @Exists_append_r @Exists_append_l @Exists_append_l @D3 ]
     933    ]
     934  ]
     935| #id #H @(π2 H3) @(π2 H2) @(π2 H1) @H
     936(* Slabel *)
     937| %{l} @E
     938| @(π1 (π1 H1))
     939| #l'' * [ #E <E %{l'} % // %1 @refl | #EX cases (π2 (π1 H1) l'' EX) #l4 * #LK #LD %{l4} % // %2 @LD ]
     940| @(π2 H1)
     941(* Sgoto *)
     942| %{l} @E
     943| @(π1 (π1 H1))
     944(* Scost *)
     945| @(π2 (π1 H1))
     946| @(π2 H1)
     947] qed.
     948
    642949
    643950axiom ParamGlobalMixup : String.
    644951
    645 definition alloc_params : var_types → list (ident×type) → stmt → res stmt ≝
    646 λvars,params,s. foldl ?? (λs,it.
     952(* ls and s0 aren't real parameters, they're just there for giving the invariant. *)
     953definition alloc_params : ∀vars:var_types.∀ls,s0,u. list (ident×type) → (Σsu:stmt×tmpgen. trans_inv vars ls s0 u su) → res (Σsu:stmt×tmpgen.trans_inv vars ls s0 u su) ≝
     954λvars,ls,s0,u,params,s. foldl ?? (λsu,it.
    647955  let 〈id,ty〉 ≝ it in
    648   do s ← s;
    649   do t ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id);
    650   match t with
    651   [ Local ⇒ OK ? s
    652   | Stack n ⇒
     956  do 〈s,u〉 with Is ← su;
     957  do t as E ← lookup' vars id;
     958  match t return λx.? → ? with
     959  [ Local ⇒ λE. OK (Σs:stmt×tmpgen.?) «〈s,u〉,Is»
     960  | Stack n ⇒ λE.
    653961      do q ← match access_mode ty with
    654962      [ By_value q ⇒ OK ? q
     
    656964      | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
    657965      ];
    658       OK ? (St_seq (St_store ? Any q (Cst ? (Oaddrstack n)) (Id (typ_of_type ty) id)) s)
    659   | Global _ ⇒ Error ? [MSG ParamGlobalMixup; CTX ? id]
    660   ]) (OK ? s) params.
     966      OK ? «〈St_seq (St_store ? Any q (Cst ? (Oaddrstack n)) (Id (typ_of_type ty) id)) s, u〉, ?»
     967  | Global _ ⇒ λE. Error ? [MSG ParamGlobalMixup; CTX ? id]
     968  ] E) (OK ? s) params.
     969try @conj try @conj try @conj try @conj try @conj try @conj
     970try @I
     971[ @(expr_vars_mp … (λid. local_id_add_tmps_oblivious vars id u)) whd >E @I
     972| @(π1 (π1 Is))
     973| @(π2 (π1 Is))
     974| @(π2 Is)
     975] qed.
     976
     977(*
     978lemma local_id_add_local : ∀vars,id,id'.
     979  local_id vars id →
     980  local_id (add ?? vars id' Local) id.
     981#vars #id #id' #H
     982whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ?] cases (identifier_eq ? id id')
     983[ #E < E >lookup_add_hit //
     984| #NE >lookup_add_miss // @eq_identifier_elim // #E cases NE >E /2/
     985] qed.
     986*)
     987axiom DuplicateLabel : String.
     988
     989definition lenv_list_inv : lenv → lenv → list ident → Prop ≝
     990λlbls0,lbls,ls.
     991 ∀l,l'. lookup_label lbls l = OK ? l' →
     992 Exists ? (λl'. l' = l) ls ∨ lookup_label lbls0 l = OK ? l'.
     993
     994lemma lookup_label_add : ∀lbls,l,l'.
     995  lookup_label (add … lbls l l') l = OK ? l'.
     996#lbls #l #l' whd in ⊢ (??%?) >lookup_add_hit @refl
     997qed.
     998
     999lemma lookup_label_miss : ∀lbls,l,l',l0.
     1000  l0 ≠ l →
     1001  lookup_label (add … lbls l l') l0 = lookup_label lbls l0.
     1002#lbls #l #l' #l0 * #NE
     1003whd in ⊢ (??%%)
     1004>lookup_add_miss
     1005[ @refl | @(eq_identifier_elim ?? l0 l)
     1006  [ #E cases (NE E)
     1007  | #_ @I
     1008  ]
     1009]
     1010qed. 
     1011
     1012let rec populate_lenv (ls:list ident) (lbls:lenv) (u:universe ?) : res (Σlbls':lenv. lenv_list_inv lbls lbls' ls) ≝
     1013match ls return λls. res (Σlbls':lenv. lenv_list_inv lbls lbls' ls) with
     1014[ nil ⇒ OK ? «lbls, ?»
     1015| cons l t ⇒
     1016    match lookup_label lbls l return λx.lookup_label lbls l = x → ? with
     1017    [ OK _ ⇒ λ_. Error ? (msg DuplicateLabel)
     1018    | Error _ ⇒ λLOOK.
     1019        let 〈l',u1〉 ≝ fresh … u in
     1020        do lbls1 ← populate_lenv t (add … lbls l l') u1;
     1021        OK ? «eject … lbls1, ?»
     1022    ] (refl ? (lookup_label lbls l))
     1023].
     1024[ #l #l' #H %2 @H
     1025| cases lbls1 #lbls' #I whd in ⊢ (??%?)
     1026  #l1 #l1' #E1 @(eq_identifier_elim … l l1)
     1027  [ #E %1 %1 @E
     1028  | #NE cases (I l1 l1' E1)
     1029    [ #H %1 %2 @H
     1030    | #LOOK' %2 >lookup_label_miss in LOOK' /2/ #H @H
     1031    ]
     1032  ]
     1033] qed.
     1034
     1035definition build_label_env : ∀body:statement. res (Σlbls:lenv. ∀l,l'.lookup_label lbls l = OK ? l' → Exists ? (λl'.l' = l) (labels_defined body)) ≝
     1036λbody.
     1037  do «lbls, H» ← populate_lenv (labels_defined body) (empty_map ??) (new_universe ?);
     1038  OK ? «lbls, ?».
     1039#l #l' #E cases (H l l' E) //
     1040whd in ⊢ (??%? → ?) #H destruct
     1041qed.
     1042
     1043lemma local_id_split : ∀vars,tmpgen,i.
     1044  local_id (add_tmps vars tmpgen) i →
     1045  local_id vars i ∨ Exists ? (λx.\fst x = i) (tmp_env tmpgen).
     1046#vars #tmpgen #i
     1047whd in ⊢ (?%? → ?)
     1048elim (tmp_env tmpgen)
     1049[ #H %1 @H
     1050| * #id #ty #tl #IH
     1051  cases (identifier_eq ? i id)
     1052  [ #E >E #H %2 whd %1 @refl
     1053  | * #NE #H cases (IH ?)
     1054    [ #H' %1 @H'
     1055    | #H' %2 %2 @H'
     1056    | whd in H; whd in H:(match % with [ _ ⇒ ? | _ ⇒ ? ]);
     1057      >lookup_add_miss in H; [ #H @H | @eq_identifier_elim // #E cases (NE E) ]
     1058    ]
     1059  ]
     1060] qed.
     1061
     1062lemma Exists_squeeze : ∀A,P,l1,l2,l3.
     1063  Exists A P (l1@l3) → Exists A P (l1@l2@l3).
     1064#A #P #l1 #l2 #l3 #EX
     1065cases (Exists_append … EX)
     1066[ #EX1 @Exists_append_l @EX1
     1067| #EX3 @Exists_append_r @Exists_append_r @EX3
     1068] qed.
    6611069
    6621070definition translate_function : universe SymbolTag → list (ident×region) → function → res internal_function ≝
    6631071λtmpuniverse, globals, f.
    664   let 〈vartypes, stacksize〉 ≝ characterise_vars globals f in
     1072  do «lbls, Ilbls» ← build_label_env (fn_body f);
     1073  let 〈vartypes, stacksize〉 as E ≝ characterise_vars globals f in
    6651074  let tmp ≝ mk_tmpgen tmpuniverse [ ] in
    666   do 〈s,tmp〉 ← translate_statement vartypes tmp (fn_body f);
    667   do s ← alloc_params vartypes (fn_params f) s;
     1075  do s ← translate_statement vartypes lbls tmp (fn_body f);
     1076  do 〈s,tmp〉 with Is ← alloc_params vartypes lbls ?? (fn_params f) s;
    6681077  OK ? (mk_internal_function
    6691078    (opttyp_of_type (fn_return f))
     
    6711080    ((tmp_env tmp)@(map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_vars f)))
    6721081    stacksize
    673     s).
     1082    s ?).
     1083cases Is * #S #L #TP
     1084@(stmt_P_mp ???? S)
     1085#s1 * #H1 #H2 %
     1086[ @(stmt_vars_mp … H1)
     1087  #i #H
     1088  cases (local_id_split … H)
     1089  [ #H' @Exists_squeeze >map_append
     1090    @Exists_map [ 2: @(characterise_vars_all … (sym_eq ??? E) i) @H'
     1091                | skip
     1092                | * #id #ty #E1 <E1 @refl
     1093                ]
     1094  | #EX @Exists_append_r @Exists_append_l @EX
     1095  ]
     1096| @(stmt_labels_mp … H2)
     1097  #l * #l' #LOOKUP
     1098  lapply (Ilbls l' l LOOKUP) #DEFINED
     1099  cases (L … DEFINED) #lx * #LOOKUPx >LOOKUPx in LOOKUP #Ex destruct (Ex)
     1100  #H @H
     1101] qed.
    6741102
    6751103definition translate_fundef : universe SymbolTag → list (ident×region) → clight_fundef → res (fundef internal_function) ≝
Note: See TracChangeset for help on using the changeset viewer.