Changeset 1316


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

Merge in id-lookup-branch to trunk.

Location:
src
Files:
14 edited
2 copied

Legend:

Unmodified
Added
Removed
  • src

  • src/ASM

  • src/ASM/BitVectorTrie.ma

    r1074 r1316  
    524524 ]
    525525qed.   
     526
     527lemma update_fail : ∀A,n,b,a,t.
     528  update A n b a t = None ? →
     529  lookup_opt A n b t = None ?.
     530#A #n elim n
     531[ #b @(vector_inv_n … b) #a #t cases (BitVectorTrie_O … t)
     532  [ * #x #E >E normalize #NE destruct
     533  | #E >E normalize //
     534  ]
     535| #m #IH #b @(vector_inv_n … b) #hd #tl #a #t cases (BitVectorTrie_Sn … t)
     536  [ * #t1 * #t2 #E >E cases hd whd in ⊢ (??%? → ??%?)
     537    #X lapply (option_map_none … X) @IH
     538  | #E >E normalize //
     539  ]
     540] qed.
     541
     542lemma update_lookup_opt_same : ∀A,n,b,a,t,t'.
     543  update A n b a t = Some ? t' →
     544  lookup_opt A n b t' = Some ? a.
     545#A #n elim n
     546[ #b #a #t #t' @(vector_inv_n … b)
     547  cases (BitVectorTrie_O … t)
     548  [ * #x #E >E normalize #E' destruct @refl
     549  | #E >E normalize #E' destruct
     550  ]
     551| #m #IH #b #a #t #t'
     552  @(vector_inv_n … b) #bhd #btl
     553  cases (BitVectorTrie_Sn … t)
     554  [ * #t1 * #t2 #E' >E'
     555    whd in ⊢ (??%? → ??%?) cases bhd #U
     556    cases (option_map_some ????? U)
     557    #tn' * #U' #E'' <E''
     558    whd in ⊢ (??%?) whd in ⊢ (??(???%%)?)
     559    @(IH … U')
     560  | #E >E normalize #E' destruct
     561  ]
     562] qed.
     563
     564lemma update_lookup_opt_other : ∀A,n,b,a,t,t'.
     565  update A n b a t = Some ? t' →
     566  ∀b'. b ≠ b' →
     567  lookup_opt A n b' t = lookup_opt A n b' t'.
     568#A #n elim n
     569[ #b #a #t #t' #E #b'
     570  @(vector_inv_n … b) @(vector_inv_n … b')
     571  * #NE cases (NE (refl ??))
     572| #m #IH #b #a #t #t'
     573  @(vector_inv_n … b) #bhd #btl
     574  cases (BitVectorTrie_Sn … t)
     575  [ * #t1 * #t2 #E >E whd in ⊢ (??%? → ?) cases bhd
     576    #U cases (option_map_some ????? U) #tn' * #U' #E' <E'
     577    #b' @(vector_inv_n … b') #bhd' #btl'
     578    cases bhd'
     579    [ 2,3: #_ @refl
     580    | *: #NE whd in ⊢ (??%%) whd in ⊢ (??(???%%)(???%%))
     581         @(IH … U') % #E'' >E'' in NE * #H @H @refl
     582    ]
     583  | #E >E whd in ⊢ (??%? → ?) #NE destruct
     584  ]
     585] qed.
     586
  • 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) ≝
  • src/Cminor/initialisation.ma

    r1224 r1316  
    44include "Cminor/syntax.ma".
    55include "common/Globalenvs.ma".
     6include "utilities/pair.ma".
     7include "utilities/deppair.ma".
    68
    79(* XXX having to specify the return type in the match is annoying. *)
     
    1921].
    2022
     23(* None of the additional code introduces locals or labels. *)
     24definition stmt_inv : stmt → Prop ≝
     25  stmt_P (λs. stmt_vars (λ_.False) s ∧ stmt_labels (λ_.False) s).
     26
    2127(* Produces a few extra skips - hopefully the compiler will optimise these
    2228   away. *)
    2329
    24 definition init_datum : ident → region → init_data → nat (*offset*) → stmt
     30definition init_datum : ident → region → init_data → nat (*offset*) → Σs:stmt. stmt_inv s
    2531λid,r,init,off.
    2632match init_expr init with
     
    3137    ]
    3238].
     39% //
     40cases init in p; [ 8: #a #b ] #c #p normalize in p; destruct; /2/
     41qed.
    3342
    34 definition init_var : ident → region → list init_data → stmt
     43definition init_var : ident → region → list init_data → Σs:stmt. stmt_inv s
    3544λid,r,init.
    3645\snd (foldr ??
     
    3847   let 〈off,s〉 ≝ os in
    3948     〈off + (size_init_data datum), St_seq (init_datum id r datum off) s〉)
    40   〈0, St_skip〉 init).
     49  〈0, dp ? (λx.stmt_inv x) St_skip ?〉 init).
     50[ % //
     51| elim init
     52  [ % //
     53  | #h #t #IH whd in ⊢ (?(???%)) @breakup_pair whd in ⊢ (?%) % [ % [ % // | @(use_sig ? stmt_inv) ] | @IH ]
     54] qed.
    4155
    42 definition init_vars : list (ident × region × (list init_data)) → stmt ≝
    43 λvars. foldr ??
    44   (λvar,s. St_seq s (init_var (\fst (\fst var)) (\snd (\fst var)) (\snd var))) St_skip vars.
     56definition init_vars : list (ident × region × (list init_data)) → Σs:stmt. stmt_inv s ≝
     57λvars. foldr ? (Σs:stmt. stmt_inv s)
     58  (λvar,s. dp ? (λx.stmt_inv x ) (St_seq s (init_var (\fst (\fst var)) (\snd (\fst var)) (\snd var))) ?) (dp ? (λx.stmt_inv x ) St_skip (conj ?? I I)) vars.
     59% [ % [ % // | @(use_sig ? stmt_inv) ] | @(use_sig ? stmt_inv) ]
     60qed.
    4561
    46 definition add_statement : ident → stmt →
     62lemma no_labels : ∀s. stmt_inv s → labels_of s = [ ].
     63#s elim s //
     64[ #s1 #s2 #IH1 #IH2 * * * #_ #_ #H1 #H2 whd in ⊢ (??%?)
     65  >(IH1 H1) >(IH2 H2) @refl
     66| #sz #sg #e #s1 #s2 #IH1 #IH2 * * * #_ #_ #H1 #H2 whd in ⊢ (??%?)
     67  >(IH1 H1) >(IH2 H2) @refl
     68| #s #IH * * #_ #_ #H @(IH H)
     69| #s #IH * * #_ #_ #H @(IH H)
     70| #l #s #IH * * #_ *
     71| #l #s #IH * * #_ #_ #H @(IH H)
     72] qed.
     73
     74definition add_statement : ident → (Σs:stmt. stmt_inv s) →
    4775                              list (ident × (fundef internal_function)) →
    4876                              list (ident × (fundef internal_function)) ≝
    49 λid,s.
     77λid,s. match s with [ dp s H ⇒
    5078  map ??
    5179    (λidf.
     
    5987                                           (f_vars f)
    6088                                           (f_stacksize f)
    61                                            (St_seq s (f_body f)))〉
     89                                           (St_seq s (f_body f))
     90                                           ?)〉
    6291          | External f ⇒ 〈id, External ? f〉 (* Error ? *)
    6392          ]
    64       | inr _ ⇒ 〈id',f'〉 ]).
     93      | inr _ ⇒ 〈id',f'〉 ]) ].
     94%
     95[ % [ % // |
     96  @(stmt_P_mp … H) #s * #V #L %
     97  [ @(stmt_vars_mp … V) #i *
     98  | @(stmt_labels_mp … L) #l *
     99  ]
     100  ]
     101| whd in ⊢ (?(λ_.??(?(λ_.???%)?))?) >(no_labels … H) @(f_inv f)
     102] qed.
    65103
    66104definition empty_vars : list (ident × region × (list init_data)) →
  • src/Cminor/semantics.ma

    r1238 r1316  
    1111definition genv ≝ (genv_t Genv) (fundef internal_function).
    1212
     13definition stmt_inv : internal_function → env → stmt → Prop ≝ λf,en,s.
     14  stmt_P (λs.stmt_vars (present ?? en) s ∧
     15             stmt_labels (λl.Exists ? (λl'.l' = l) (labels_of (f_body f))) s) s.
     16
     17lemma stmt_inv_update : ∀f,en,s,l,v.
     18  stmt_inv f en s →
     19  ∀H:present ?? en l.
     20  stmt_inv f (update_present ?? en l H v) s.
     21#f #en #s #l #v #Inv #H
     22@(stmt_P_mp … Inv)
     23#s * #H1 #H2 %
     24[ @(stmt_vars_mp … H1)
     25  #l #H @update_still_present @H
     26| @H2
     27] qed.
     28
     29(* continuations within a function. *)
    1330inductive cont : Type[0] ≝
    14 | Kstop : cont
     31| Kend : cont
    1532| Kseq : stmt → cont → cont
    16 | Kblock : cont → cont
    17 | Kcall : option ident → internal_function → block (* sp *) → env → cont → cont.
     33| Kblock : cont → cont.
     34
     35let rec cont_inv (f:internal_function) (en:env) (k:cont) on k : Prop ≝
     36match k with
     37[ Kend ⇒ True
     38| Kseq s k' ⇒ stmt_inv f en s ∧ cont_inv f en k'
     39| Kblock k' ⇒ cont_inv f en k'
     40].
     41
     42lemma cont_inv_update : ∀f,en,k,l,v.
     43  cont_inv f en k →
     44  ∀H:present ?? en l.
     45  cont_inv f (update_present ?? en l H v) k.
     46#f #en #k elim k /2/
     47#s #k #IH #l #v #Inv #H whd %
     48[ @stmt_inv_update @(π1 Inv)
     49| @IH @(π2 Inv)
     50] qed.
     51
     52(* a stack of function calls *)
     53inductive stack : Type[0] ≝
     54| SStop : stack
     55| Scall : ∀dest:option ident. ∀f:internal_function. block (* sp *) → ∀en:env. match dest with [ None ⇒ True | Some id ⇒ present ?? en id] → stmt_inv f en (f_body f) → ∀k:cont. cont_inv f en k → stack → stack.
    1856
    1957inductive state : Type[0] ≝
     
    2260    ∀    s: stmt.
    2361    ∀   en: env.
     62    ∀ fInv: stmt_inv f en (f_body f).
     63    ∀  Inv: stmt_inv f en s.
    2464    ∀    m: mem.
    2565    ∀   sp: block.
    2666    ∀    k: cont.
     67    ∀ kInv: cont_inv f en k.
     68    ∀   st: stack.
    2769            state
    2870| Callstate:
     
    3072    ∀ args: list val.
    3173    ∀    m: mem.
    32     ∀    k: cont.
     74    ∀   st: stack.
    3375            state
    3476| Returnstate:
    3577    ∀    v: option val.
    3678    ∀    m: mem.
    37     ∀    k: cont.
     79    ∀   st: stack.
    3880            state.
    3981
    4082definition mem_of_state : state → mem ≝
    4183λst. match st with
    42 [ State _ _ _ m _ _ ⇒ m
     84[ State _ _ _ _ _ m _ _ _ _ ⇒ m
    4385| Callstate _ _ m _ ⇒ m
    4486| Returnstate _ m _ ⇒ m
     
    5092axiom FailedLoad : String.
    5193
    52 let rec eval_expr (ge:genv) (ty0:typ) (e:expr ty0) (en:env) (sp:block) (m:mem) on e : res (trace × val) ≝
    53 match e with
    54 [ Id _ i ⇒
    55     do r ← opt_to_res … [MSG UnknownLocal; CTX ? i] (lookup ?? en i);
     94let rec eval_expr (ge:genv) (ty0:typ) (e:expr ty0) (en:env) (Env:expr_vars ty0 e (present ?? en)) (sp:block) (m:mem) on e : res (trace × val) ≝
     95match e return λt,e.expr_vars t e (present ?? en) → res (trace × val) with
     96[ Id _ i ⇒ λEnv.
     97    let r ≝ lookup_present ?? en i ? in
    5698    OK ? 〈E0, r〉
    57 | Cst _ c ⇒
     99| Cst _ c ⇒ λEnv.
    58100    do r ← opt_to_res … (msg FailedConstant) (eval_constant (find_symbol … ge) sp c);
    59101    OK ? 〈E0, r〉
    60 | Op1 ty ty' op e' ⇒
    61     do 〈tr,v〉 ← eval_expr ge ? e' en sp m;
     102| Op1 ty ty' op e' ⇒ λEnv.
     103    do 〈tr,v〉 ← eval_expr ge ? e' en ? sp m;
    62104    do r ← opt_to_res … (msg FailedOp) (eval_unop op v);
    63105    OK ? 〈tr, r〉
    64 | Op2 ty1 ty2 ty' op e1 e2 ⇒
    65     do 〈tr1,v1〉 ← eval_expr ge ? e1 en sp m;
    66     do 〈tr2,v2〉 ← eval_expr ge ? e2 en sp m;
     106| Op2 ty1 ty2 ty' op e1 e2 ⇒ λEnv.
     107    do 〈tr1,v1〉 ← eval_expr ge ? e1 en ? sp m;
     108    do 〈tr2,v2〉 ← eval_expr ge ? e2 en ? sp m;
    67109    do r ← opt_to_res … (msg FailedOp) (eval_binop op v1 v2);
    68110    OK ? 〈tr1 ⧺ tr2, r〉
    69 | Mem rg ty chunk e ⇒
    70     do 〈tr,v〉 ← eval_expr ge ? e en sp m;
     111| Mem rg ty chunk e ⇒ λEnv.
     112    do 〈tr,v〉 ← eval_expr ge ? e en ? sp m;
    71113    do r ← opt_to_res … (msg FailedLoad) (loadv chunk m v);
    72114    OK ? 〈tr, r〉
    73 | Cond sz sg ty e' e1 e2 ⇒
    74     do 〈tr,v〉 ← eval_expr ge ? e' en sp m;
     115| Cond sz sg ty e' e1 e2 ⇒ λEnv.
     116    do 〈tr,v〉 ← eval_expr ge ? e' en ? sp m;
    75117    do b ← eval_bool_of_val v;
    76     do 〈tr',r〉 ← eval_expr ge ? (if b then e1 else e2) en sp m;
     118    do 〈tr',r〉 ← eval_expr ge ? (if b then e1 else e2) en ? sp m;
    77119    OK ? 〈tr ⧺ tr', r〉
    78 | Ecost ty l e' ⇒
    79     do 〈tr,r〉 ← eval_expr ge ty e' en sp m;
     120| Ecost ty l e' ⇒ λEnv.
     121    do 〈tr,r〉 ← eval_expr ge ty e' en ? sp m;
    80122    OK ? 〈Echarge l ⧺ tr, r〉
    81 ].
     123] Env.
     124try @Env
     125try @(π1 Env)
     126try @(π2 Env)
     127try @(π1 (π1 Env))
     128cases b
     129try @(π2 (π1 Env))
     130try @(π2 Env)
     131qed.
    82132
    83133axiom BadState : String.
    84134
    85 let rec k_exit (n:nat) (k:cont) on k : res cont ≝
    86 match k with
    87 [ Kstop ⇒ Error ? (msg BadState)
    88 | Kseq _ k' ⇒ k_exit n k'
    89 | Kblock k' ⇒ match n with [ O ⇒ OK ? k' | S m ⇒ k_exit m k' ]
    90 | Kcall _ _ _ _ _ ⇒ Error ? (msg BadState)
    91 ].
     135let rec k_exit (n:nat) (k:cont) f en (kInv:cont_inv f en k) on k : res (Σk':cont. cont_inv f en k') ≝
     136match k return λk.cont_inv f en k → ? with
     137[ Kend ⇒ λ_. Error ? (msg BadState)
     138| Kseq _ k' ⇒ λkInv. k_exit n k' f en ?
     139| Kblock k' ⇒ λkInv. match n with [ O ⇒ OK ? «k',?» | S m ⇒ k_exit m k' f en ? ]
     140] kInv.
     141[ @(π2 kInv) | @kInv | @kInv ]
     142qed.
    92143
    93144let rec find_case (A:Type[0]) (sz:intsize) (i:bvint sz) (cs:list (bvint sz × A)) (default:A) on cs : A ≝
     
    99150].
    100151
    101 let rec call_cont (k:cont) : cont ≝
    102 match k with
    103 [ Kseq _ k' ⇒ call_cont k'
    104 | Kblock k' ⇒ call_cont k'
    105 | _ ⇒ k
    106 ].
    107 
    108 let rec find_label (l:ident) (s:stmt) (k:cont) on s : option (stmt × cont) ≝
    109 match s with
    110 [ St_seq s1 s2 ⇒
    111     match find_label l s1 (Kseq s2 k) with
    112     [ None ⇒ find_label l s2 k
     152let rec find_label (l:identifier Label) (s:stmt) (k:cont) f en (Inv:stmt_inv f en s) (kInv:cont_inv f en k) on s : option (Σsk:(stmt × cont). stmt_inv f en (\fst sk) ∧ cont_inv f en (\snd sk)) ≝
     153match s return λs. stmt_inv f en s → ? with
     154[ St_seq s1 s2 ⇒ λInv.
     155    match find_label l s1 (Kseq s2 k) f en ?? with
     156    [ None ⇒ find_label l s2 k f en ??
    113157    | Some sk ⇒ Some ? sk
    114158    ]
    115 | St_ifthenelse _ _ _ s1 s2 ⇒
    116     match find_label l s1 k with
    117     [ None ⇒ find_label l s2 k
     159| St_ifthenelse _ _ _ s1 s2 ⇒ λInv.
     160    match find_label l s1 k f en ?? with
     161    [ None ⇒ find_label l s2 k f en ??
    118162    | Some sk ⇒ Some ? sk
    119163    ]
    120 | St_loop s' ⇒ find_label l s' (Kseq (St_loop s') k)
    121 | St_block s' ⇒ find_label l s' (Kblock k)
    122 | St_label l' s' ⇒
    123     match ident_eq l l' with
     164| St_loop s' ⇒ λInv. find_label l s' (Kseq (St_loop s') k) f en ??
     165| St_block s' ⇒ λInv. find_label l s' (Kblock k) f en ??
     166| St_label l' s' ⇒ λInv.
     167    match identifier_eq ? l l' with
    124168    [ inl _ ⇒ Some ? 〈s',k〉
    125     | inr _ ⇒ find_label l s' k
    126     ]
    127 | St_cost _ s' ⇒ find_label l s' k
    128 | _ ⇒ None ?
    129 ].
     169    | inr _ ⇒ find_label l s' k f en ??
     170    ]
     171| St_cost _ s' ⇒ λInv. find_label l s' k f en ??
     172| _ ⇒ λ_. None ?
     173] Inv.
     174//
     175try @(π2 Inv)
     176try @(π2 (π1 Inv))
     177[ % [ @(π2 Inv) | @kInv ]
     178| % [ @Inv | @kInv ]
     179| % [ @(π2 Inv) | @kInv ]
     180] qed.
     181
     182lemma find_label_none : ∀l,s,k,f,en,Inv,kInv.
     183  find_label l s k f en Inv kInv = None ? →
     184  ¬Exists ? (λl'.l' = l) (labels_of s).
     185#l #s elim s
     186try (try #a try #b try #c try #d try #e try #f try #g try #h try #i try #j try #m % * (* *) )
     187[ #s1 #s2 #IH1 #IH2 #k #f #en #Inv #kInv whd in ⊢ (??%? → ?(???%))
     188  lapply (IH1 (Kseq s2 k) f en (π2 (π1 Inv)) (conj ?? (π2 Inv) kInv))
     189  cases (find_label l s1 (Kseq s2 k) f en ??)
     190  [ #H1 whd in ⊢ (??%? → ?)
     191    lapply (IH2 k f en (π2 Inv) kInv) cases (find_label l s2 k f en ??)
     192    [ #H2 #_ % #H cases (Exists_append … H)
     193      [ #H' cases (H1 (refl ??)) /2/
     194      | #H' cases (H2 (refl ??)) /2/
     195      ]
     196    | #sk #_ #E destruct
     197    ]
     198  | #sk #_ #E whd in E:(??%?); destruct
     199  ]
     200| #sz #sg #e #s1 #s2 #IH1 #IH2 #k #f #en #Inv #kInv whd in ⊢ (??%? → ?(???%))
     201  lapply (IH1 k f en (π2 (π1 Inv)) kInv)
     202  cases (find_label l s1 k f en ??)
     203  [ #H1 whd in ⊢ (??%? → ?)
     204    lapply (IH2 k f en (π2 Inv) kInv) cases (find_label l s2 k f en ??)
     205    [ #H2 #_ % #H cases (Exists_append … H)
     206      [ #H' cases (H1 (refl ??)) /2/
     207      | #H' cases (H2 (refl ??)) /2/
     208      ]
     209    | #sk #_ #E destruct
     210    ]
     211  | #sk #_ #E whd in E:(??%?); destruct
     212  ]
     213| #s1 #IH #k #f #en #Inv #kInv @IH
     214| #s1 #IH #k #f #en #Inv #kInv @IH
     215| #E whd in i:(??%?); cases (identifier_eq Label l a) in i;
     216  whd in ⊢ (? → ??%? → ?) [ #_ #E2 destruct | *; #H cases (H (sym_eq … E)) ]
     217| whd in i:(??%?); cases (identifier_eq Label l a) in i;
     218  whd in ⊢ (? → ??%? → ?) [ #_ #E2 destruct | #NE #E cases (c d e f ?? E) #H @H ]
     219| #cl #s1 #IH #k #f #en #Inv #kInv @IH
     220] qed.
     221
     222definition find_label_always : ∀l,s,k. Exists ? (λl'.l' = l) (labels_of s) →
     223  ∀f,en. stmt_inv f en s → cont_inv f en k →
     224  Σsk:stmt × cont. stmt_inv f en (\fst sk) ∧ cont_inv f en (\snd sk) ≝
     225λl,s,k,H,f,en,Inv,kInv.
     226  match find_label l s k f en Inv kInv return λx.find_label l s k f en Inv kInv = x → ? with
     227  [ Some sk ⇒ λ_. sk
     228  | None ⇒ λE. ⊥
     229  ] (refl ? (find_label l s k f en Inv kInv)).
     230cases (find_label_none … E)
     231#H1 @(H1 H)
     232qed.
    130233
    131234axiom WrongNumberOfParameters : String.
    132235
    133236(* TODO: perhaps should do a little type checking? *)
    134 let rec bind_params (vs:list val) (ids:list (ident×typ)) : res env
     237let rec bind_params (vs:list val) (ids:list (ident×typ)) : res (Σen:env. All ? (λit. present ?? en (\fst it)) ids)
    135238match vs with
    136 [ nil ⇒ match ids with [ nil ⇒ OK ? (empty_map ??) | _ ⇒ Error ? (msg WrongNumberOfParameters) ]
     239[ nil ⇒ match ids return λids.res (Σen. All ?? ids) with [ nil ⇒ OK ? «empty_map ??, ?» | _ ⇒ Error ? (msg WrongNumberOfParameters) ]
    137240| cons v vt ⇒
    138     match ids with
     241    match ids return λids.res (Σen. All ?? ids) with
    139242    [ nil ⇒ Error ? (msg WrongNumberOfParameters)
    140243    | cons idh idt ⇒
    141244        let 〈id,ty〉 ≝ idh in
    142245        do en ← bind_params vt idt;
    143         OK ? (add ?? en id v)
    144     ]
    145 ].
     246        OK ? «add ?? en (\fst idh) v, ?»
     247    ]
     248].
     249[ @I
     250| % [ whd >lookup_add_hit % #E destruct
     251    | @(All_mp … (use_sig ?? en)) #a #H whd @lookup_add_oblivious @H
     252    ]
     253] qed.
    146254
    147255(* TODO: perhaps should do a little type checking? *)
    148256definition init_locals : env → list (ident×typ) → env ≝
    149257foldr ?? (λidty,en. add ?? en (\fst idty) Vundef).
     258
     259lemma init_locals_preserves : ∀en,vars,l.
     260  present ?? en l →
     261  present ?? (init_locals en vars) l.
     262#en #vars elim vars
     263[ #l #H @H
     264| #idt #tl #IH #l #H whd
     265  @lookup_add_oblivious @IH @H
     266] qed.
     267
     268lemma init_locals_env : ∀en,vars.
     269  All ? (λidt. present ?? (init_locals en vars) (\fst idt)) vars.
     270#en #vars elim vars
     271[ @I
     272| #idt #tl #IH %
     273  [ whd >lookup_add_hit % #E destruct
     274  | @(All_mp … IH) #a #H @lookup_add_oblivious @H
     275  ]
     276] qed.
     277
     278let rec trace_map_inv (A,B:Type[0]) (P:A → Prop) (f:∀a. P a → res (trace × B))
     279                  (l:list A) (p:All A P l) on l : res (trace × (list B)) ≝
     280match l return λl. All A P l → ? with
     281[ nil ⇒ λ_. OK ? 〈E0, [ ]〉
     282| cons h t ⇒ λp.
     283    do 〈tr,h'〉 ← f h ?;
     284    do 〈tr',t'〉 ← trace_map_inv … f t ?;
     285    OK ? 〈tr ⧺ tr',h'::t'〉
     286] p.
     287[ @(π1 p) | @(π2 p) ] qed.
    150288
    151289axiom FailedStore : String.
     
    155293axiom ReturnMismatch : String.
    156294
     295lemma Exists_exists : ∀A,P,l.
     296  Exists A P l →
     297  ∃x. P x.
     298#A #P #l elim l [ * | #hd #tl #IH * [ #H %{hd} @H | @IH ]
     299qed.
     300
     301lemma Exists_All : ∀A,P,Q,l.
     302  Exists A P l →
     303  All A Q l →
     304  ∃x. P x ∧ Q x.
     305#A #P #Q #l elim l [ * | #hd #tl #IH * [ #H1 * #H2 #_ %{hd} /2/ | #H1 * #_ #H2 @IH // ]
     306qed.
     307
    157308definition eval_step : genv → state → IO io_out io_in (trace × state) ≝
    158309λge,st.
    159310match st with
    160 [ State f s en m sp k ⇒
    161     match s with
    162     [ St_skip ⇒
    163         match k with
    164         [ Kstop ⇒ Wrong ??? (msg BadState)
    165         | Kseq s' k' ⇒ ret ? 〈E0, State f s' en m sp k'〉
    166         | Kblock k' ⇒ ret ? 〈E0, State f s en m sp k'〉
     311[ State f s en fInv Inv m sp k kInv st ⇒
     312    match s return λs. stmt_inv f en s → ? with
     313    [ St_skip ⇒ λInv.
     314        match k return λk. cont_inv f en k → ? with
     315        [ Kseq s' k' ⇒ λkInv. ret ? 〈E0, State f s' en fInv ? m sp k' ? st〉
     316        | Kblock k' ⇒ λkInv. ret ? 〈E0, State f St_skip en fInv ? m sp k' ? st〉
    167317          (* cminor allows functions without an explicit return statement *)
    168         | Kcall _ _ _ _ _ ⇒ ret ? 〈E0, Returnstate (None ?) (free m sp) k
    169         ]
    170     | St_assign _ id e ⇒
    171         ! 〈tr,v〉 ← eval_expr ge ? e en sp m;
    172         ! en' ← update ?? en id v;
    173         ret ? 〈tr, State f St_skip en' m sp k
    174     | St_store _ _ chunk edst e ⇒
    175         ! 〈tr,vdst〉 ← eval_expr ge ? edst en sp m;
    176         ! 〈tr',v〉 ← eval_expr ge ? e en sp m;
     318        | Kend ⇒ λkInv. ret ? 〈E0, Returnstate (None ?) (free m sp) st
     319        ] kInv
     320    | St_assign _ id e ⇒ λInv.
     321        ! 〈tr,v〉 ← eval_expr ge ? e en ? sp m;
     322        let en' ≝ update_present ?? en id ? v in
     323        ret ? 〈tr, State f St_skip en' ? ? m sp k ? st
     324    | St_store _ _ chunk edst e ⇒ λInv.
     325        ! 〈tr,vdst〉 ← eval_expr ge ? edst en ? sp m;
     326        ! 〈tr',v〉 ← eval_expr ge ? e en ? sp m;
    177327        ! m' ← opt_to_res … (msg FailedStore) (storev chunk m vdst v);
    178         ret ? 〈tr ⧺ tr', State f St_skip en m' sp k
    179 
    180     | St_call dst ef args ⇒
    181         ! 〈tr,vf〉 ← eval_expr ge ? ef en sp m;
     328        ret ? 〈tr ⧺ tr', State f St_skip en fInv ? m' sp k ? st
     329
     330    | St_call dst ef args ⇒ λInv.
     331        ! 〈tr,vf〉 ← eval_expr ge ? ef en ? sp m;
    182332        ! fd ← opt_to_res … (msg BadFunctionValue) (find_funct ?? ge vf);
    183         ! 〈tr',vargs〉 ← trace_map … (λe. match e with [ dp ty e ⇒ eval_expr ge ? e en sp m ]) args;
    184         ret ? 〈tr ⧺ tr', Callstate fd vargs m (Kcall dst f sp en k)〉
    185     | St_tailcall ef args ⇒
    186         ! 〈tr,vf〉 ← eval_expr ge ? ef en sp m;
     333        ! 〈tr',vargs〉 ← trace_map_inv … (λe. match e return λe.match e with [ dp _ _ ⇒ ? ] → ? with [ dp ty e ⇒ λp. eval_expr ge ? e en p sp m ]) args ?;
     334        ret ? 〈tr ⧺ tr', Callstate fd vargs m (Scall dst f sp en ? fInv k ? st)〉
     335    | St_tailcall ef args ⇒ λInv.
     336        ! 〈tr,vf〉 ← eval_expr ge ? ef en ? sp m;
    187337        ! fd ← opt_to_res … (msg BadFunctionValue) (find_funct ?? ge vf);
    188         ! 〈tr',vargs〉 ← trace_map … (λe. match e with [ dp ty e ⇒ eval_expr ge ? e en sp m ]) args;
    189         ret ? 〈tr ⧺ tr', Callstate fd vargs (free m sp) (call_cont k)
     338        ! 〈tr',vargs〉 ← trace_map_inv … (λe. match e return λe.match e with [ dp _ _ ⇒ ? ] → ? with [ dp ty e ⇒ λp. eval_expr ge ? e en p sp m ]) args ?;
     339        ret ? 〈tr ⧺ tr', Callstate fd vargs (free m sp) st
    190340       
    191     | St_seq s1 s2 ⇒ ret ? 〈E0, State f s1 en m sp (Kseq s2 k)
    192     | St_ifthenelse _ _ e strue sfalse ⇒
    193         ! 〈tr,v〉 ← eval_expr ge ? e en sp m;
     341    | St_seq s1 s2 ⇒ λInv. ret ? 〈E0, State f s1 en fInv ? m sp (Kseq s2 k) ? st
     342    | St_ifthenelse _ _ e strue sfalse ⇒ λInv.
     343        ! 〈tr,v〉 ← eval_expr ge ? e en ? sp m;
    194344        ! b ← eval_bool_of_val v;
    195         ret ? 〈tr, State f (if b then strue else sfalse) en m sp k
    196     | St_loop s ⇒ ret ? 〈E0, State f s en m sp (Kseq (St_loop s) k)
    197     | St_block s ⇒ ret ? 〈E0, State f s en m sp (Kblock k)
    198     | St_exit n ⇒
    199         ! k' ← k_exit n k;
    200         ret ? 〈E0, State f St_skip en m sp k'
    201     | St_switch sz _ e cs default ⇒
    202         ! 〈tr,v〉 ← eval_expr ge ? e en sp m;
     345        ret ? 〈tr, State f (if b then strue else sfalse) en fInv ? m sp k ? st
     346    | St_loop s ⇒ λInv. ret ? 〈E0, State f s en fInv ? m sp (Kseq (St_loop s) k) ? st
     347    | St_block s ⇒ λInv. ret ? 〈E0, State f s en fInv ? m sp (Kblock k) ? st
     348    | St_exit n ⇒ λInv.
     349        ! k' ← k_exit n k ?? kInv;
     350        ret ? 〈E0, State f St_skip en fInv ? m sp k' ? st
     351    | St_switch sz _ e cs default ⇒ λInv.
     352        ! 〈tr,v〉 ← eval_expr ge ? e en ? sp m;
    203353        match v with
    204354        [ Vint sz' i ⇒ intsize_eq_elim ? sz' sz ? i (λi.
    205             ! k' ← k_exit (find_case ?? i cs default) k;
    206             ret ? 〈tr, State f St_skip en m sp k'〉)
     355            ! k' ← k_exit (find_case ?? i cs default) k ?? kInv;
     356            ret ? 〈tr, State f St_skip en fInv ? m sp k' ? st〉)
    207357            (Wrong ??? (msg BadSwitchValue))
    208358        | _ ⇒ Wrong ??? (msg BadSwitchValue)
    209359        ]
    210360    | St_return eo ⇒
    211         match eo with
    212         [ None ⇒ ret ? 〈E0, Returnstate (None ?) (free m sp) (call_cont k)
     361        match eo return λeo. stmt_inv f en (St_return eo) → ? with
     362        [ None ⇒ λInv. ret ? 〈E0, Returnstate (None ?) (free m sp) st
    213363        | Some e ⇒
    214             match e with [ dp ty e ⇒
    215               ! 〈tr,v〉 ← eval_expr ge ? e en sp m;
    216               ret ? 〈tr, Returnstate (Some ? v) (free m sp) (call_cont k)
     364            match e return λe. stmt_inv f en (St_return (Some ? e)) → ? with [ dp ty e ⇒ λInv.
     365              ! 〈tr,v〉 ← eval_expr ge ? e en ? sp m;
     366              ret ? 〈tr, Returnstate (Some ? v) (free m sp) st
    217367            ]
    218368        ]
    219     | St_label l s' ⇒ ret ? 〈E0, State f s' en m sp k〉
    220     | St_goto l ⇒
    221         ! 〈s', k'〉 ← opt_to_res … [MSG UnknownLabel; CTX ? l] (find_label l (f_body f) (call_cont k));
    222         ret ? 〈E0, State f s' en m sp k'〉
    223     | St_cost l s' ⇒
    224         ret ? 〈Echarge l, State f s' en m sp k〉
    225     ]
    226 | Callstate fd args m k ⇒
     369    | St_label l s' ⇒ λInv. ret ? 〈E0, State f s' en fInv ? m sp k ? st〉
     370    | St_goto l ⇒ λInv.
     371        match find_label_always l (f_body f) Kend ? f en ?? with [ dp sk Inv' ⇒
     372          ret ? 〈E0, State f (\fst sk) en fInv ? m sp (\snd sk) ? st〉
     373        ]
     374    | St_cost l s' ⇒ λInv.
     375        ret ? 〈Echarge l, State f s' en fInv ? m sp k ? st〉
     376    ] Inv
     377| Callstate fd args m st ⇒
    227378    match fd with
    228379    [ Internal f ⇒
    229380        let 〈m',sp〉 ≝ alloc m 0 (f_stacksize f) Any in
    230381        ! en ← bind_params args (f_params f);
    231         ret ? 〈E0, State f (f_body f) (init_locals en (f_vars f)) m' sp k
     382        ret ? 〈E0, State f (f_body f) (init_locals en (f_vars f)) ? ? m' sp Kend ? st
    232383    | External fn ⇒
    233384        ! evargs ← check_eventval_list args (sig_args (ef_sig fn));
    234385        ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
    235386        let res ≝ match (sig_res (ef_sig fn)) with [ None ⇒ None ? | Some _ ⇒ Some ? (mk_val ? evres) ] in
    236         ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate res m k〉
    237     ]
    238 | Returnstate res m k ⇒
    239     match k with
    240     [ Kcall dst f sp en k' ⇒
    241         ! en' ← match res with
    242                 [ None ⇒ match dst with [ None ⇒ OK ? en | Some _ ⇒ Error ? (msg ReturnMismatch)]
    243                 | Some v ⇒ match dst with [ None ⇒ Error ? (msg ReturnMismatch)
    244                                           | Some id ⇒ update ?? en id v ]
    245                 ];
    246         ret ? 〈E0, State f St_skip en' m sp k'〉
     387        ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate res m st〉
     388    ]
     389| Returnstate res m st ⇒
     390    match st with
     391    [ Scall dst f sp en dstP fInv k Inv st' ⇒
     392        match res with
     393        [ None ⇒ match dst with
     394                 [ None ⇒ ret ? 〈E0, State f St_skip en ? ? m sp k ? st'〉
     395                 | Some _ ⇒ Wrong ??? (msg ReturnMismatch)]
     396        | Some v ⇒ match dst return λdst. match dst with [ None ⇒ ? | Some _ ⇒ ?] → ? with
     397                   [ None ⇒ λ_. Wrong ??? (msg ReturnMismatch)
     398                   | Some id ⇒ λdstP. ret ? 〈E0, State f St_skip (update_present ?? en id dstP v) ? ? m sp k ? st'〉
     399                   ] dstP
     400        ]
    247401    | _ ⇒ Wrong ??? (msg BadState)
    248402    ]
    249403].
     404try @(π1 kInv)
     405try @(π2 kInv)
     406try @(conj ?? I I)
     407try @kInv
     408try @(π2 (π1 Inv))
     409try @kInv
     410try @(π1 (π1 Inv))
     411try (@cont_inv_update @kInv)
     412try @(π2 (π1 (π1 Inv)))
     413try @(π1 (π1 (π1 Inv)))
     414try @(π1 Inv)
     415try @(π2 Inv)
     416[ @stmt_inv_update @fInv
     417| % [ @(π2 Inv) | @kInv ]
     418| cases b [ @(π2 (π1 Inv)) | @(π2 Inv) ]
     419| % [ @Inv | @kInv ]
     420| @(use_sig … k')
     421| @(use_sig … k')
     422| @(π1 Inv')
     423| @(π2 Inv')
     424| @fInv
     425| @I
     426| 11,12:
     427  @(stmt_P_mp … (f_inv f))
     428  #s * #V #L %
     429  [ 1,3: @(stmt_vars_mp … V) #id #EX cases (Exists_append … EX)
     430    [ 1,3: #H @init_locals_preserves cases (Exists_All … H (use_sig … en))
     431      * #id' #ty * #E1 #H <E1 @H
     432    | *: #H cases (Exists_All … H (init_locals_env … en …))
     433      * #id' #ty * #E1 #H <E1 @H
     434    ]
     435  | 2,4: @L
     436  ]
     437| @fInv
     438| @Inv
     439| @stmt_inv_update @fInv
     440| @cont_inv_update @Inv
     441] qed.
    250442
    251443definition is_final : state → option int ≝
    252444λs. match s with
    253 [ Returnstate res m k
    254     match k with
    255     [ Kstop ⇒
     445[ Returnstate res m st
     446    match st with
     447    [ SStop ⇒
    256448        match res with
    257449        [ None ⇒ None ?
     
    281473  do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p));
    282474  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b);
    283   OK ? (Callstate f (nil ?) m Kstop).
     475  OK ? (Callstate f (nil ?) m SStop).
    284476
    285477definition Cminor_fullexec : fullexec io_out io_in ≝
     
    295487  do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p));
    296488  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b);
    297   OK ? (Callstate f (nil ?) m Kstop).
     489  OK ? (Callstate f (nil ?) m SStop).
    298490
    299491definition Cminor_noinit_fullexec : fullexec io_out io_in ≝
  • src/Cminor/syntax.ma

    r1224 r1316  
    22include "common/FrontEndOps.ma".
    33include "common/CostLabel.ma".
     4include "utilities/lists.ma".
     5include "utilities/option.ma".
    46
    57(* TODO: consider making the typing stricter. *)
     
    1315| Cond : ∀sz,sg,t. expr (ASTint sz sg) → expr t → expr t → expr t
    1416| Ecost : ∀t. costlabel → expr t → expr t.
     17
     18(* Assert a predicate on every variable or parameter identifier. *)
     19let rec expr_vars (t:typ) (e:expr t) (P:ident → Prop) on e : Prop ≝
     20match e with
     21[ Id _ i ⇒ P i
     22| Cst _ _ ⇒ True
     23| Op1 _ _ _ e ⇒ expr_vars ? e P
     24| Op2 _ _ _ _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P
     25| Mem _ _ _ e ⇒ expr_vars ? e P
     26| Cond _ _ _ e1 e2 e3 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P ∧ expr_vars ? e3 P
     27| Ecost _ _ e ⇒ expr_vars ? e P
     28].
     29
     30lemma expr_vars_mp : ∀t,e,P,Q.
     31  (∀i. P i → Q i) → expr_vars t e P → expr_vars t e Q.
     32#t0 #e elim e normalize /3/
     33[ #t1 #t2 #t #op #e1 #e2 #IH1 #IH2 #P #Q #H * #H1 #H2
     34  % /3/
     35| #sz #sg #t #e1 #e2 #e3 #IH1 #IH2 #IH3 #P #Q #H * * /5/
     36] qed.
     37
     38axiom Label : String.
    1539
    1640inductive stmt : Type[0] ≝
     
    2953| St_switch : ∀sz,sg. expr (ASTint sz sg) → list (bvint sz × nat) → nat → stmt
    3054| St_return : option (Σt. expr t) → stmt
    31 | St_label : ident → stmt → stmt
    32 | St_goto : ident → stmt
     55| St_label : identifier Label → stmt → stmt
     56| St_goto : identifier Label → stmt
    3357| St_cost : costlabel → stmt → stmt.
     58
     59let rec stmt_P (P:stmt → Prop) (s:stmt) on s : Prop ≝
     60match s with
     61[ St_seq s1 s2 ⇒ P s ∧ stmt_P P s1 ∧ stmt_P P s2
     62| St_ifthenelse _ _ _ s1 s2 ⇒ P s ∧ stmt_P P s1 ∧ stmt_P P s2
     63| St_loop s' ⇒ P s ∧ stmt_P P s'
     64| St_block s' ⇒ P s ∧ stmt_P P s'
     65| St_label _ s' ⇒ P s ∧ stmt_P P s'
     66| St_cost _ s' ⇒ P s ∧ stmt_P P s'
     67| _ ⇒ P s
     68].
     69
     70lemma stmt_P_P : ∀P,s. stmt_P P s → P s.
     71#P * normalize /2/
     72[ #s1 #s2 * * /2/
     73| #sz #sg #e #s1 #s2 * * /2/
     74| 3,4: #s * /2/
     75| 5,6: #i #s normalize * /2/
     76] qed.
     77
     78(* Assert a predicate on every variable or parameter identifier. *)
     79definition stmt_vars : (ident → Prop) → stmt → Prop ≝
     80λP,s.
     81match s with
     82[ St_assign _ i e ⇒ P i ∧ expr_vars ? e P
     83| St_store _ _ _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P
     84| St_call oi e es ⇒ match oi with [ None ⇒ True | Some i ⇒ P i ] ∧ expr_vars ? e P ∧ All ? (λe.match e with [ dp _ e ⇒ expr_vars ? e P ]) es
     85| St_tailcall e es ⇒ expr_vars ? e P ∧ All ? (λe.match e with [ dp _ e ⇒ expr_vars ? e P ]) es
     86| St_ifthenelse _ _ e _ _ ⇒ expr_vars ? e P
     87| St_switch _ _ e _ _ ⇒ expr_vars ? e P
     88| St_return oe ⇒ match oe with [ None ⇒ True | Some e ⇒ match e with [ dp _ e ⇒ expr_vars ? e P ] ]
     89| _ ⇒ True
     90].
     91
     92definition stmt_labels : (identifier Label → Prop) → stmt → Prop ≝
     93λP,s.
     94match s with
     95[ St_label l _ ⇒ P l
     96| St_goto l ⇒ P l
     97| _ ⇒ True
     98].
     99
     100lemma stmt_P_mp : ∀P,Q. (∀s. P s → Q s) → ∀s. stmt_P P s → stmt_P Q s.
     101#P #Q #H #s elim s /2/
     102[ #s1 #s2 #H1 #H2 normalize * * /4/
     103| #sz #sg #e #s1 #s2 #H1 #H2 * * /5/
     104| #s #H * /5/
     105| #s #H * /5/
     106| #l #s #H * /5/
     107| #l #s #H * /5/
     108] qed.
     109
     110lemma stmt_vars_mp : ∀P,Q. (∀i. P i → Q i) → ∀s. stmt_vars P s → stmt_vars Q s.
     111#P #Q #H #s elim s normalize
     112[ //
     113| #t #id #e * /4/
     114| #t #r #q #e1 #e2 * /4/
     115| * normalize [ 2: #id ] #e #es * * #H1 #H2 #H3 % [ 1,3: % /3/ | *: @(All_mp … H3) * #t #e normalize @expr_vars_mp @H ]
     116| #e #es * #H1 #H2 % [ /3/ | @(All_mp … H2) * /3/ ]
     117| #s1 #s2 #H1 #H2 * /3/
     118| #sz #sg #e #s1 #s2 #H1 #H2 /5/
     119| 8,9: #s #H1 #H2 /2/
     120| //
     121| /5/
     122| * normalize [ // | *; normalize /3/ ]
     123| /2/
     124| //
     125| /2/
     126] qed.
     127
     128lemma stmt_labels_mp : ∀P,Q. (∀l. P l → Q l) → ∀s. stmt_labels P s → stmt_labels Q s.
     129#P #Q #H #s elim s normalize /2/ qed.
     130
     131(* Get labels from a Cminor statement. *)
     132let rec labels_of (s:stmt) : list (identifier Label) ≝
     133match s with
     134[ St_seq s1 s2 ⇒ (labels_of s1) @ (labels_of s2)
     135| St_ifthenelse _ _ _ s1 s2 ⇒ (labels_of s1) @ (labels_of s2)
     136| St_loop s ⇒ labels_of s
     137| St_block s ⇒ labels_of s
     138| St_label l s ⇒ l::(labels_of s)
     139| St_cost _ s ⇒ labels_of s
     140| _ ⇒ [ ]
     141].
    34142
    35143record internal_function : Type[0] ≝
     
    39147; f_stacksize : nat
    40148; f_body      : stmt
     149; f_inv       : stmt_P (λs.stmt_vars (λi.Exists ? (λx.\fst x = i) (f_params @ f_vars)) s ∧
     150                           stmt_labels (λl.Exists ? (λl'.l' = l) (labels_of f_body)) s) f_body
    41151}.
    42152
  • src/Cminor/toRTLabs.ma

    r1224 r1316  
    33include "Cminor/syntax.ma".
    44include "RTLabs/syntax.ma".
     5include "utilities/pair.ma".
     6include "utilities/deppair.ma".
    57
    68definition env ≝ identifier_map SymbolTag register.
    7 definition label_env ≝ identifier_map SymbolTag label.
     9definition label_env ≝ identifier_map Label label.
    810definition populate_env : env → universe RegisterTag → list (ident × typ) → list (register×typ) × env × (universe RegisterTag) ≝
    911λen,gen. foldr ??
     
    1416     〈〈r,ty〉::rs, add ?? en id r, gen'〉) 〈[ ], en, gen〉.
    1517
    16 definition populate_label_env : label_env → universe LabelTag → list ident → label_env × (universe LabelTag) ≝
     18lemma populates_env : ∀l,e,u,l',e',u'.
     19  populate_env e u l = 〈l',e',u'〉 →
     20  ∀i. Exists ? (λx.\fst x = i) l →
     21      present ?? e' i.
     22#l elim l
     23[ #e #u #l' #e' #u' #E whd in E:(??%?); #i destruct (E) *
     24| * #id #t #tl #IH #e #u #l' #e' #u' #E #i whd in E:(??%?) ⊢ (% → ?);
     25  * [ whd in ⊢ (??%? → ?) #E1 <E1
     26      generalize in E:(??(match % with [ _ ⇒ ? ])?) ⊢ ? * * #x #y #z
     27      whd in ⊢ (??%? → ?) elim (fresh RegisterTag z) #r #gen' #E
     28      whd in E:(??%?);
     29      >(?:e' = add ?? y id r) [ 2: destruct (E) @refl ] (* XXX workaround because destruct overnormalises *)
     30      whd >lookup_add_hit % #A destruct
     31    | #H change in E:(??(match % with [ _ ⇒ ? ])?) with (populate_env e u tl)
     32      lapply (refl ? (populate_env e u tl))
     33      cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?) (* XXX if I do this directly it rewrites both sides of the equality *)
     34      * #rs #e1 #u1 #E1 >E1 in E; whd in ⊢ (??%? → ?) cases (fresh RegisterTag u1) #r #u''
     35      whd in ⊢ (??%? → ?) #E
     36      >(?:e' = add ?? e1 id r) [ 2: destruct (E) @refl ] (* XXX workaround because destruct overnormalises *)
     37      @lookup_add_oblivious
     38      @(IH … E1 ? H)
     39    ]
     40] qed.
     41
     42lemma populate_extends : ∀l,e,u,l',e',u'.
     43  populate_env e u l = 〈l',e',u'〉 →
     44  ∀i. present ?? e i → present ?? e' i.
     45#l elim l
     46[ #e #u #l' #e' #u' #E whd in E:(??%?); destruct //
     47| * #id #t #tl #IH #e #u #l' #e' #u' #E whd in E:(??%?);
     48  change in E:(??(match % with [ _ ⇒ ?])?) with (populate_env e u tl)
     49  lapply (refl ? (populate_env e u tl))
     50  cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?) * #l0 #e0 #u0 #E0
     51  >E0 in E; whd in ⊢ (??%? → ?) cases (fresh RegisterTag u0) #i1 #u1 #E
     52  whd in E:(??%?)
     53  >(?:e' = add ?? e0 id i1) [ 2: destruct (E) @refl ]
     54  #i #H @lookup_add_oblivious @(IH … E0) @H
     55] qed.
     56
     57definition  populate_label_env : label_env → universe LabelTag → list (identifier Label) → label_env × (universe LabelTag) ≝
    1758λen,gen. foldr ??
    1859 (λid,engen.
     
    2162     〈add ?? en id r, gen'〉) 〈en, gen〉.
    2263
    23 lemma lookup_sigma : ∀tag,A,m. ∀i:(Σl:identifier tag. lookup tag A m l ≠ None ?).
    24   lookup tag A m i ≠ None ?.
    25 #tag #A #m * #i #H @H
    26 qed.
     64lemma populates_label_env : ∀ls,lbls,u,lbls',u'.
     65  populate_label_env lbls u ls = 〈lbls',u'〉 →
     66  ∀l. Exists ? (λl'.l' = l) ls → present ?? lbls' l.
     67#ls elim ls
     68[ #lbls #u #lbls' #u' #E #l *
     69| #h #t #IH #lbls #u #lbls' #u' whd in ⊢ (??%? → ?)
     70  change in ⊢ (??match % with [ _ ⇒ ? ]? → ?) with (populate_label_env ???)
     71  lapply (refl ? (populate_label_env lbls u t))
     72  cases (populate_label_env lbls u t) in ⊢ (???% → %)
     73  #lbls1 #u1 #E1 whd in ⊢ (??%? → ?) cases (fresh ? u1) #r #gen' whd in ⊢ (??%? → ?)
     74  #E >(?:lbls' = add ?? lbls1 h r) [ 2: destruct (E) @refl ]
     75  #l *
     76  [ #El <El whd >lookup_add_hit % #Er destruct
     77  | #H @lookup_add_oblivious @(IH … E1 ? H)
     78  ]
     79] qed.
     80
     81lemma label_env_contents : ∀ls,lbls,u,lbls',u'.
     82  populate_label_env lbls u ls = 〈lbls',u'〉 →
     83  ∀l. present ?? lbls' l → Exists ? (λl'.l = l') ls ∨ present ?? lbls l.
     84#ls elim ls
     85[ #lbls #u #lbls' #u' #E #l #H %2 whd in E:(??%?); destruct @H
     86| #h #t #IH #lbls #u #lbls' #u' whd in ⊢ (??%? → ?)
     87  change in ⊢ (??match % with [ _ ⇒ ? ]? → ?) with (populate_label_env ???)
     88  lapply (refl ? (populate_label_env lbls u t))
     89  cases (populate_label_env lbls u t) in ⊢ (???% → %)
     90  #lbls1 #u1 #E1 whd in ⊢ (??%? → ?) cases (fresh ? u1) #r #gen' whd in ⊢ (??%? → ?)
     91  #E >(?:lbls' = add ?? lbls1 h r) [ 2: destruct (E) @refl ]
     92  #l #H cases (identifier_eq ? l h)
     93  [ #El %1 %1 @El
     94  | #NE cases (IH … E1 l ?)
     95    [ #H' %1 %2 @H' | #H' %2 @H' | whd in H >lookup_add_miss in H // @eq_identifier_elim // #E cases NE /2/ ]
     96  ]
     97] qed.
     98
     99definition lookup_reg : ∀e:env. ∀id. present ?? e id → register ≝ lookup_present ??.
     100definition lookup_label : ∀e:label_env. ∀id. present ?? e id → label ≝ lookup_present ??.
     101
     102(* Check that the domain of one graph is included in another, for monotonicity
     103   properties.  Note that we don't say anything about the statements. *)
     104definition graph_included : graph statement → graph statement → Prop ≝
     105λg1,g2. ∀l. present ?? g1 l → present ?? g2 l.
     106
     107lemma graph_inc_trans : ∀g1,g2,g3.
     108  graph_included g1 g2 → graph_included g2 g3 → graph_included g1 g3.
     109#g1 #g2 #g3 #H1 #H2 #l #P1 @H2 @H1 @P1 qed.
     110
     111definition lpresent ≝ λlbls:label_env. λl. ∃l'. lookup ?? lbls l' = Some ? l.
     112
     113definition partially_closed : label_env → graph statement → Prop ≝
     114 λe,g. ∀l,s. lookup ?? g l = Some ? s → labels_P (λl. present ?? g l ∨ lpresent e l) s.
     115
     116(* I'd use a single parametrised definition along with internal_function, but
     117   it's a pain without implicit parameters. *)
     118record partial_fn (lenv:label_env) : Type[0] ≝
     119{ pf_labgen    : universe LabelTag
     120; pf_reggen    : universe RegisterTag
     121; pf_result    : option (register × typ)
     122; pf_params    : list (register × typ)
     123; pf_locals    : list (register × typ)
     124; pf_stacksize : nat
     125; pf_graph     : graph statement
     126; pf_closed    : partially_closed lenv pf_graph
     127; pf_entry     : Σl:label. present ?? pf_graph l
     128; pf_exit      : Σl:label. present ?? pf_graph l
     129}.
     130
     131inductive fn_graph_included (le:label_env) (f1:partial_fn le) (f2:partial_fn le) : Prop ≝
     132| fn_graph_inc : graph_included (pf_graph ? f1) (pf_graph ? f2) → fn_graph_included le f1 f2.
     133
     134lemma fn_graph_inc_trans : ∀le,f1,f2,f3.
     135  fn_graph_included le f1 f2 → fn_graph_included le f2 f3 → fn_graph_included le f1 f3.
     136#le #f1 #f2 #f3 * #H1 * #H2 % @(graph_inc_trans … H1 H2) qed.
     137
     138lemma fn_graph_included_refl : ∀label_env,f.
     139  fn_graph_included label_env f f.
     140#le #f % #l #H @H qed.
     141
     142lemma fn_graph_included_sig : ∀label_env,f,f0.
     143  ∀f':Σf':partial_fn label_env. fn_graph_included ? f0 f'.
     144  fn_graph_included label_env f f0 →
     145  fn_graph_included label_env f f'.
     146#le #f #f0 * #f' #H1 #H2 @(fn_graph_inc_trans … H2 H1)
     147qed.
     148
     149lemma add_statement_inv : ∀le,l,s.∀f.
     150  labels_present (pf_graph le f) s →
     151  partially_closed le (add … (pf_graph ? f) l s).
     152#le #l #s #f #p
     153#l' #s' #H cases (identifier_eq … l l')
     154[ #E >E in H >lookup_add_hit #E' <(?:s = s') [2:destruct //]
     155  @(labels_P_mp … p) #l0 #H %1 @lookup_add_oblivious @H
     156| #NE @(labels_P_mp … (pf_closed ? f l' s' ?))
     157  [ #lx * [ #H %1 @lookup_add_oblivious @H | #H %2 @H ]
     158  | >lookup_add_miss in H // @eq_identifier_elim // #E cases NE /2/
     159  ]
     160] qed.
    27161
    28162(* Add a statement to the graph, *without* updating the entry label. *)
    29 definition fill_in_statement : label → statement → internal_function → internal_function ≝
    30 λl,s,f.
    31   mk_internal_function (f_labgen f) (f_reggen f)
    32                        (f_result f) (f_params f) (f_locals f)
    33                        (f_stacksize f) (add ?? (f_graph f) l s)
    34                        (dp ?? (f_entry f) ?) (dp ?? (f_exit f) ?).
    35 @lookup_add_oblivious @lookup_sigma
    36 qed.
     163definition fill_in_statement : ∀le. label → ∀s:statement. ∀f:partial_fn le. labels_present (pf_graph ? f) s → Σf':partial_fn le. fn_graph_included le f f' ≝
     164λle,l,s,f,p.
     165  mk_partial_fn le (pf_labgen ? f) (pf_reggen ? f)
     166                (pf_result ? f) (pf_params ? f) (pf_locals ? f)
     167                (pf_stacksize ? f) (add ?? (pf_graph ? f) l s) ?
     168                «pf_entry ? f, ?» «pf_exit ? f, ?».
     169[ @add_statement_inv @p
     170| 2,3: @lookup_add_oblivious @use_sig
     171| % #l' @lookup_add_oblivious
     172] qed.
    37173
    38174(* Add a statement to the graph, making it the entry label. *)
    39 definition add_to_graph : label → statement → internal_function → internal_function ≝
    40 λl,s,f.
    41   mk_internal_function (f_labgen f) (f_reggen f)
    42                        (f_result f) (f_params f) (f_locals f)
    43                        (f_stacksize f) (add ?? (f_graph f) l s)
    44                        (dp ?? l ?) (dp ?? (f_exit f) ?).
    45 [ >lookup_add_hit % #E destruct
    46 | @lookup_add_oblivious @lookup_sigma
     175definition add_to_graph : ∀le. label → ∀s:statement. ∀f:partial_fn le. labels_present (pf_graph ? f) s → Σf':partial_fn le. fn_graph_included le f f' ≝
     176λle,l,s,f,p.
     177  mk_partial_fn le (pf_labgen ? f) (pf_reggen ? f)
     178                (pf_result ? f) (pf_params ? f) (pf_locals ? f)
     179                (pf_stacksize ? f) (add ?? (pf_graph ? f) l s) ?
     180                «l, ?» «pf_exit ? f, ?».
     181[ @add_statement_inv @p
     182| whd >lookup_add_hit % #E destruct
     183| @lookup_add_oblivious @use_sig
     184| % #l' @lookup_add_oblivious
    47185] qed.
    48186
    49187(* Add a statement with a fresh label to the start of the function.  The
    50188   statement is parametrised by the *next* instruction's label. *)
    51 definition add_fresh_to_graph : (label → statement) → internal_function → internal_function ≝
    52 λs,f.
    53   let 〈l,g〉 ≝ fresh … (f_labgen f) in
    54   let s' ≝ s (f_entry f) in
    55     (mk_internal_function g (f_reggen f)
    56                        (f_result f) (f_params f) (f_locals f)
    57                        (f_stacksize f) (add ?? (f_graph f) l s')
    58                        (dp ?? l ?) (dp ?? (f_exit f) ?)).
    59 [ >lookup_add_hit % #E destruct
    60 | @lookup_add_oblivious @lookup_sigma
    61 ] qed.
    62 
    63 definition fresh_reg : internal_function → typ → register × internal_function ≝
    64 λf,ty.
    65   let 〈r,g〉 ≝ fresh … (f_reggen f) in
    66     〈r, mk_internal_function (f_labgen f) g
    67                        (f_result f) (f_params f) (〈r,ty〉::(f_locals f))
    68                        (f_stacksize f) (f_graph f) (f_entry f) (f_exit f)〉.
     189definition add_fresh_to_graph : ∀le. ∀s:(label → statement). ∀f:partial_fn le. (∀l. present ?? (pf_graph ? f) l → labels_present (pf_graph ? f) (s l)) → Σf':partial_fn le. fn_graph_included le f f' ≝
     190λle,s,f,p.
     191  let 〈l,g〉 ≝ fresh … (pf_labgen ? f) in
     192  let s' ≝ s (pf_entry ? f) in
     193    (mk_partial_fn le g (pf_reggen ? f)
     194                   (pf_result ? f) (pf_params ? f) (pf_locals ? f)
     195                   (pf_stacksize ? f) (add ?? (pf_graph ? f) l s') ?
     196                   «l, ?» «pf_exit ? f, ?»).
     197[ % #l' @lookup_add_oblivious
     198| @add_statement_inv @p @use_sig
     199| whd >lookup_add_hit % #E destruct
     200| @lookup_add_oblivious @use_sig
     201] qed.
     202
     203(* Variants for labels which are (goto) labels *)
     204
     205lemma add_statement_inv' : ∀le,l,s.∀f.
     206  labels_P (λl. present ?? (pf_graph le f) l ∨ lpresent le l) s →
     207  partially_closed le (add … (pf_graph ? f) l s).
     208#le #l #s #f #p
     209#l' #s' #H cases (identifier_eq … l l')
     210[ #E >E in H >lookup_add_hit #E' <(?:s = s') [2:destruct //]
     211  @(labels_P_mp … p) #l0 * [ #H %1 @lookup_add_oblivious @H | #H %2 @H ]
     212| #NE @(labels_P_mp … (pf_closed ? f l' s' ?))
     213  [ #lx * [ #H %1 @lookup_add_oblivious @H | #H %2 @H ]
     214  | >lookup_add_miss in H // @eq_identifier_elim // #E cases NE /2/
     215  ]
     216] qed.
     217
     218definition add_fresh_to_graph' : ∀le. ∀s:(label → statement). ∀f:partial_fn le. (∀l. present ?? (pf_graph ? f) l → labels_P (λl.present ?? (pf_graph ? f) l ∨ lpresent le l) (s l)) → Σf':partial_fn le. fn_graph_included le f f' ≝
     219λle,s,f,p.
     220  let 〈l,g〉 ≝ fresh … (pf_labgen ? f) in
     221  let s' ≝ s (pf_entry ? f) in
     222    (mk_partial_fn le g (pf_reggen ? f)
     223                   (pf_result ? f) (pf_params ? f) (pf_locals ? f)
     224                   (pf_stacksize ? f) (add ?? (pf_graph ? f) l s') ?
     225                   «l, ?» «pf_exit ? f, ?»).
     226[ % #l' @lookup_add_oblivious
     227| @add_statement_inv' @p @use_sig
     228| whd >lookup_add_hit % #E destruct
     229| @lookup_add_oblivious @use_sig
     230] qed.
     231
     232definition fresh_reg : ∀le. ∀f:partial_fn le. typ → register × (Σf':partial_fn le. fn_graph_included le f f') ≝
     233λle,f,ty.
     234  let 〈r,g〉 ≝ fresh … (pf_reggen ? f) in
     235    〈r, «mk_partial_fn le (pf_labgen ? f) g
     236                       (pf_result ? f) (pf_params ? f) (〈r,ty〉::(pf_locals ? f))
     237                       (pf_stacksize ? f) (pf_graph ? f) (pf_closed ? f) (pf_entry ? f) (pf_exit ? f), ?»〉.
     238% #l // qed.
    69239
    70240axiom UnknownVariable : String.
    71241
    72 definition choose_reg : env → ∀ty.expr ty → internal_function → res (register × internal_function) ≝
    73 λenv,ty,e,f.
    74   match e with
    75   [ Id _ i ⇒
    76       do r ← opt_to_res … [MSG UnknownVariable; CTX ? i] (lookup … env i);
    77       OK ? 〈r, f〉
    78   | _ ⇒
    79       OK ? (fresh_reg f ty)
     242definition choose_reg : ∀le. ∀env:env.∀ty.∀e:expr ty. ∀f:partial_fn le. expr_vars ty e (present ?? env) → register × (Σf':partial_fn le. fn_graph_included le f f') ≝
     243λle,env,ty,e,f.
     244  match e return λty,e. expr_vars ty e (present ?? env) → register × (Σf':partial_fn le. fn_graph_included le f f') with
     245  [ Id _ i ⇒ λEnv. 〈lookup_reg env i Env, «f, ?»〉
     246  | _ ⇒ λ_.fresh_reg le f ty
    80247  ].
    81 
    82 definition choose_regs : env → list (Σt:typ.expr t) → internal_function → res (list register × internal_function) ≝
    83 λenv,es,f.
    84   foldr (Σt:typ.expr t) ?
    85     (λe,acc. do 〈rs,f〉 ← acc;
    86              do 〈r,f'〉 ← match e with [ dp t e ⇒ choose_reg env t e f ];
    87              OK ? 〈r::rs,f'〉) (OK ? 〈[ ], f〉) es.
     248% // qed.
     249 
     250let rec foldr_all (A,B:Type[0]) (P:A → Prop) (f:∀a:A. P a → B → B) (b:B) (l:list A) (H:All ? P l) on l :B ≝ 
     251 match l return λx.All ? P x → B with [ nil ⇒ λ_. b | cons a l ⇒ λH. f a (proj1 … H) (foldr_all A B P f b l (proj2 … H))] H.
     252
     253definition exprtyp_present ≝ λenv:env.λe:Σt:typ.expr t.match e with [ dp ty e ⇒ expr_vars ty e (present ?? env) ].
     254
     255definition choose_regs : ∀le. ∀env:env. ∀es:list (Σt:typ.expr t).
     256                         ∀f:partial_fn le. All ? (exprtyp_present env) es →
     257                         list register × (Σf':partial_fn le. fn_graph_included le f f') ≝
     258λle,env,es,f,Env.
     259  foldr_all (Σt:typ.expr t) ??
     260    (λe,p,acc. let 〈rs,f〉 ≝ acc in
     261             let 〈r,f'〉 ≝ match e return λe.? → ? with [ dp t e ⇒ λp.choose_reg le env t e (eject … f) ? ] p in
     262             〈r::rs,«eject … f', ?»〉) 〈[ ], «f, ?»〉 es Env.
     263[ @p
     264| @fn_graph_inc_trans [ 3: @(use_sig ?? f') | skip | @(use_sig ?? f) ]
     265| % //
     266]  qed.
     267
     268lemma extract_pair : ∀A,B,C,D.  ∀u:A×B. ∀Q:A → B → C×D. ∀x,y.
     269((let 〈a,b〉 ≝ u in Q a b) = 〈x,y〉) →
     270∃a,b. 〈a,b〉 = u ∧ Q a b = 〈x,y〉.
     271#A #B #C #D * #a #b #Q #x #y normalize #E1 %{a} %{b} % try @refl @E1 qed.
     272
     273
     274lemma choose_regs_length : ∀le,env,es,f,p,rs,f'.
     275  choose_regs le env es f p = 〈rs,f'〉 → |es| = |rs|.
     276#le #env #es #f elim es
     277[ #p #rs #f normalize #E destruct @refl
     278| * #ty #e #t #IH #p #rs #f' whd in ⊢ (??%? → ??%?) #E
     279  cases (extract_pair ???????? E) #rs' * #f'' * #E1 #E2 -E;
     280  cases (extract_pair ???????? E2) #r * #f3 * #E3 #E4 -E2;
     281  destruct (E4) skip (E1 E3) @eq_f @IH
     282  [ @(proj2 … p)
     283  | 3: @sym_eq @E1
     284  | 2: skip
     285  ]
     286] qed.
     287
     288lemma present_inc : ∀le,f,l.
     289  ∀f':Σf':partial_fn le. fn_graph_included le f f'.
     290  present ?? (pf_graph le f) l →
     291  present ?? (pf_graph le f') l.
     292#le #f #l * #f' * #H1 #H2 @H1 @H2 qed.
    88293
    89294axiom BadCminorProgram : String.
    90295
    91 let rec add_expr (env:env) (ty:typ) (e:expr ty) (dst:register) (f:internal_function) on e: res internal_function
    92 match e with
    93 [ Id _ i ⇒
    94     do r ← opt_to_res … [MSG UnknownVariable; CTX ? i] (lookup ?? env i);
     296let rec add_expr (le:label_env) (env:env) (ty:typ) (e:expr ty) (Env:expr_vars ty e (present ?? env)) (dst:register) (f:partial_fn le) on e: Σf':partial_fn le. fn_graph_included le f f'
     297match e return λty,e.expr_vars ty e (present ?? env) → Σf':partial_fn le. fn_graph_included le f f' with
     298[ Id _ i ⇒ λEnv.
     299    let r ≝ lookup_reg env i Env in
    95300    match register_eq r dst with
    96     [ inl _ ⇒ OK ? f
    97     | inr _ ⇒ OK ? (add_fresh_to_graph (St_op1 Oid dst r) f)
     301    [ inl _ ⇒ «f, ?»
     302    | inr _ ⇒ «eject … (add_fresh_to_graph ? (St_op1 Oid dst r) f ?), ?»
    98303    ]
    99 | Cst _ c ⇒ OK ? (add_fresh_to_graph (St_const dst c) f)
    100 | Op1 _ _ op e' ⇒
    101     do 〈r,f〉 ← choose_reg env ? e' f;
    102     let f ≝ add_fresh_to_graph (St_op1 op dst r) f in
    103     add_expr env ? e' r f
    104 | Op2 _ _ _ op e1 e2 ⇒
    105     do 〈r1,f〉 ← choose_reg env ? e1 f;
    106     do 〈r2,f〉 ← choose_reg env ? e2 f;
    107     let f ≝ add_fresh_to_graph (St_op2 op dst r1 r2) f in
    108     do f ← add_expr env ? e2 r2 f;
    109     add_expr env ? e1 r1 f
    110 | Mem _ _ q e' ⇒
    111     do 〈r,f〉 ← choose_reg env ? e' f;
    112     let f ≝ add_fresh_to_graph (St_load q r dst) f in
    113     add_expr env ? e' r f
    114 | Cond _ _ _ e' e1 e2 ⇒
    115     let resume_at ≝ f_entry f in
    116     do f ← add_expr env ? e2 dst f;
    117     let lfalse ≝ f_entry f in
    118     let f ≝ add_fresh_to_graph (λ_.St_skip resume_at) f in
    119     do f ← add_expr env ? e1 dst f;
    120     do 〈r,f〉 ← choose_reg env ? e' f;
    121     let f ≝ add_fresh_to_graph (λltrue. St_cond r ltrue lfalse) f in
    122     add_expr env ? e' r f
    123 | Ecost _ l e' ⇒
    124     do f ← add_expr env ? e' dst f;
    125     OK ? (add_fresh_to_graph (St_cost l) f)
    126 ].
    127 
    128 (* This shouldn't occur; maybe use vectors? *)
    129 axiom WrongNumberOfArguments : String.
    130 
    131 let rec add_exprs (env:env) (es:list (Σt:typ.expr t)) (dsts:list register) (f:internal_function) on es: res internal_function ≝
    132 match es with
    133 [ nil ⇒ match dsts with [ nil ⇒ OK ? f | cons _ _ ⇒ Error ? (msg WrongNumberOfArguments) ]
    134 | cons e et ⇒
    135     match dsts with
    136     [ nil ⇒ Error ? (msg WrongNumberOfArguments)
    137     | cons r rt ⇒
    138         do f ← add_exprs env et rt f;
    139         match e with [ dp ty e ⇒ add_expr env ty e r f ]
     304| Cst _ c ⇒ λ_. «add_fresh_to_graph ? (St_const dst c) f ?, ?»
     305| Op1 _ _ op e' ⇒ λEnv.
     306    let 〈r,f〉 ≝ choose_reg ? env ? e' f Env in
     307    let f ≝ add_fresh_to_graph ? (St_op1 op dst r) f ? in
     308    let f ≝ add_expr ? env ? e' Env r f in
     309      «eject … f, ?»
     310| Op2 _ _ _ op e1 e2 ⇒ λEnv.
     311    let 〈r1,f〉 ≝ choose_reg ? env ? e1 f (proj1 … Env) in
     312    let 〈r2,f〉 ≝ choose_reg ? env ? e2 f (proj2 … Env) in
     313    let f ≝ add_fresh_to_graph ? (St_op2 op dst r1 r2) f ? in
     314    let f ≝ add_expr ? env ? e2 (proj2 … Env) r2 f in
     315    let f ≝ add_expr ? env ? e1 (proj1 … Env) r1 f in
     316      «eject … f, ?»
     317| Mem _ _ q e' ⇒ λEnv.
     318    let 〈r,f〉 ≝ choose_reg ? env ? e' f Env in
     319    let f ≝ add_fresh_to_graph ? (St_load q r dst) f ? in
     320    let f ≝ add_expr ? env ? e' Env r f in
     321      «eject … f, ?»
     322| Cond _ _ _ e' e1 e2 ⇒ λEnv.
     323    let resume_at ≝ pf_entry ? f in
     324    let f ≝ add_expr ? env ? e2 (proj2 … Env) dst f in
     325    let lfalse ≝ pf_entry ? f in
     326    let f ≝ add_fresh_to_graph ? (λ_.St_skip resume_at) f ? in
     327    let f ≝ add_expr ? env ? e1 (proj2 … (proj1 … Env)) dst f in
     328    let 〈r,f〉 as E ≝ choose_reg ? env ? e' f (proj1 … (proj1 … Env)) in
     329    let f ≝ add_fresh_to_graph ? (λltrue. St_cond r ltrue lfalse) f ? in
     330    let f ≝ add_expr ? env ? e' (proj1 … (proj1 … Env)) r f in
     331      «eject … f, ?»
     332| Ecost _ l e' ⇒ λEnv.
     333    let f ≝ add_expr ? env ? e' Env dst f in
     334    let f ≝ add_fresh_to_graph ? (St_cost l) f ? in
     335      «f, ?»
     336] Env.
     337(* For new labels, we need to step back through the definitions of f until we
     338   hit the point that it was added. *)
     339try @fn_graph_included_refl
     340try (#l #H @H)
     341[ 7: #l #H whd % [ @H |
     342    @present_inc
     343    @present_inc
     344    @present_inc
     345    @(use_sig ? (present ???)) ]
     346| 8: #l #H
     347    @present_inc
     348    @(use_sig ? (present ???))
     349(* For the monotonicity properties, we just keep going back until we're at the
     350   start.  The repeat tactical helps here. *)
     351| *: repeat @fn_graph_included_sig @fn_graph_included_refl
     352] qed.
     353
     354let rec add_exprs (le:label_env) (env:env) (es:list (Σt:typ.expr t)) (Env:All ? (exprtyp_present env) es)
     355                  (dsts:list register) (pf:|es|=|dsts|) (f:partial_fn le) on es: Σf':partial_fn le. fn_graph_included le f f' ≝
     356match es return λes.All ?? es → |es|=|dsts| → ? with
     357[ nil ⇒ λ_. match dsts return λx. ?=|x| → Σf':partial_fn le. fn_graph_included le f f' with [ nil ⇒ λ_. «f, ?» | cons _ _ ⇒ λpf.⊥ ]
     358| cons e et ⇒ λEnv.
     359    match dsts return λx. ?=|x| → ? with
     360    [ nil ⇒ λpf.⊥
     361    | cons r rt ⇒ λpf.
     362        let f ≝ add_exprs ? env et ? rt ? f in
     363        match e return λe.exprtyp_present ? e → ? with [ dp ty e ⇒ λEnv.
     364          let f ≝ add_expr ? env ty e ? r f in
     365            «eject … f, ?» ] (proj1 ?? Env)
    140366    ]
    141 ].
     367] Env pf.
     368[ //
     369| 2,3: normalize in pf; destruct
     370| @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_refl
     371| @Env
     372| @(proj2 … Env)
     373| normalize in pf; destruct @e0 ] qed.
    142374
    143375axiom UnknownLabel : String.
    144376axiom ReturnMismatch : String.
    145377
    146 let rec add_stmt (env:env) (label_env:label_env) (s:stmt) (exits:list label) (f:internal_function) on s : res internal_function ≝
    147 match s with
    148 [ St_skip ⇒ OK ? f
    149 | St_assign _ x e ⇒
    150     do dst ← opt_to_res … [MSG UnknownVariable; CTX ? x] (lookup ?? env x);
    151     add_expr env ? e dst f
    152 | St_store _ _ q e1 e2 ⇒
    153     do 〈val_reg, f〉 ← choose_reg env ? e2 f;
    154     do 〈addr_reg, f〉 ← choose_reg env ? e1 f;
    155     let f ≝ add_fresh_to_graph (St_store q addr_reg val_reg) f in
    156     do f ← add_expr env ? e1 addr_reg f;
    157     add_expr env ? e2 val_reg f
    158 | St_call return_opt_id e args ⇒
    159     do return_opt_reg ←
    160       match return_opt_id with
    161       [ None ⇒ OK ? (None ?)
    162       | Some id ⇒ do r ← opt_to_res … [MSG UnknownVariable; CTX ? id] (lookup ?? env id); OK ? (Some ? r)
    163       ];
    164     do 〈args_regs, f〉 ← choose_regs env args f;
    165     do f ←
    166       match e with
    167       [ Id _ id ⇒ OK ? (add_fresh_to_graph (St_call_id id args_regs return_opt_reg) f)
    168       | _ ⇒
    169         do 〈fnr, f〉 ← choose_reg env ? e f;
    170         let f ≝ add_fresh_to_graph (St_call_ptr fnr args_regs return_opt_reg) f in
    171         add_expr env ? e fnr f
    172       ];
    173     add_exprs env args args_regs f
    174 | St_tailcall e args ⇒
    175     do 〈args_regs, f〉 ← choose_regs env args f;
    176     do f ←
    177       match e with
    178       [ Id _ id ⇒ OK ? (add_fresh_to_graph (λ_. St_tailcall_id id args_regs) f)
    179       | _ ⇒
    180         do 〈fnr, f〉 ← choose_reg env ? e f;
    181         let f ≝ add_fresh_to_graph (λ_. St_tailcall_ptr fnr args_regs) f in
    182         add_expr env ? e fnr f
    183       ];
    184     add_exprs env args args_regs f
    185 | St_seq s1 s2 ⇒
    186     do f ← add_stmt env label_env s2 exits f;
    187     add_stmt env label_env s1 exits f
    188 | St_ifthenelse _ _ e s1 s2 ⇒
    189     let l_next ≝ f_entry f in
    190     do f ← add_stmt env label_env s2 exits f;
    191     let l2 ≝ f_entry f in
    192     let f ≝ add_fresh_to_graph ? (* XXX: fails, but works if applied afterwards: λ_. St_skip l_next*) f in
    193     do f ← add_stmt env label_env s1 exits f;
    194     do 〈r,f〉 ← choose_reg env ? e f;
    195     let f ≝ add_fresh_to_graph (λl1. St_cond r l1 l2) f in
    196     add_expr env ? e r f
    197 | St_loop s ⇒
    198     let f ≝ add_fresh_to_graph ? f in (* dummy statement, fill in afterwards *)
    199     let l_loop ≝ f_entry f in
    200     do f ← add_stmt env label_env s exits f;
    201     OK ? (fill_in_statement l_loop (* XXX another odd failure: St_skip (f_entry f)*)? f)
    202 | St_block s ⇒
    203     add_stmt env label_env s ((f_entry f)::exits) f
    204 | St_exit n ⇒
    205     do l ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits);
    206     OK ? (add_fresh_to_graph (* XXX another: λ_. St_skip l*)? f)
    207 | St_switch sz sg e tab n ⇒
    208     do 〈r,f〉 ← choose_reg env ? e f;
    209     do l_default ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits);
    210     let f ≝ add_fresh_to_graph (* XXX grrrr: λ_. St_skip l_default*)? f in
    211     do f ← foldr ?? (λcs,f.
     378definition stmt_inv : env → label_env → stmt → Prop ≝
     379λenv,lenv. stmt_P (λs. stmt_vars (present ?? env) s ∧ stmt_labels (present ?? lenv) s).
     380
     381(* Trick to avoid multiplying the proof obligations for the non-Id cases. *)
     382definition expr_is_Id : ∀t. expr t → option ident ≝
     383λt,e. match e with
     384[ Id _ id ⇒ Some ? id
     385| _ ⇒ None ?
     386].
     387
     388(* XXX Work around odd disambiguation errors. *)
     389alias id "R_skip" = "cic:/matita/cerco/RTLabs/syntax/statement.con(0,1,0)".
     390alias id "R_return" = "cic:/matita/cerco/RTLabs/syntax/statement.con(0,14,0)".
     391
     392definition nth_sig : ∀A. ∀P:A → Prop. errmsg → (Σl:list A. All A P l) → nat → res (Σa:A. P a) ≝
     393λA,P,m,l,n.
     394  match nth_opt A n l return λx.(∀_.x = ? → ?) → ? with
     395  [ None ⇒ λ_. Error ? m
     396  | Some a ⇒ λH'. OK ? «a, ?»
     397  ] (All_nth A P n l (use_sig … l)).
     398@H' @refl qed.
     399
     400lemma lookup_label_rev : ∀lenv,l,l',p.
     401  lookup_label lenv l p = l' → lookup ?? lenv l = Some ? l'.
     402#lenv #l #l' #p
     403cut (∃lx. lookup ?? lenv l = Some ? lx)
     404[ whd in p; cases (lookup ?? lenv l) in p ⊢ %
     405  [ * #H cases (H (refl ??))
     406  | #lx #_ %{lx} @refl
     407  ]
     408| * #lx #E whd in ⊢ (??%? → ?) cases p >E #q whd in ⊢ (??%? → ?) #E' >E' @refl
     409] qed.
     410
     411lemma lookup_label_rev' : ∀lenv,l,p.
     412  lookup ?? lenv l = Some ? (lookup_label lenv l p).
     413#lenv #l #p @lookup_label_rev [ @p | @refl ]
     414qed.
     415
     416lemma lookup_label_lpresent : ∀lenv,l,p.
     417  lpresent lenv (lookup_label lenv l p).
     418#le #l #p whd %{l} @lookup_label_rev'
     419qed.
     420
     421(* We need to show that the graph only grows, and that Cminor labels will end
     422   up in the graph. *)
     423definition Cminor_labels_added ≝ λle,s,f'.
     424∀l. Exists ? (λl'.l=l') (labels_of s) →
     425∃l'. lookup ?? le l = Some ? l' ∧ present ?? (pf_graph le f') l'.
     426
     427record add_stmt_inv (le:label_env) (s:stmt) (f:partial_fn le) (f':partial_fn le) : Prop ≝
     428{ stmt_graph_inc : fn_graph_included ? f f'
     429; stmt_labels_added : Cminor_labels_added le s f'
     430}.
     431
     432lemma empty_Cminor_labels_added : ∀le,s,f'.
     433  labels_of s = [ ] → Cminor_labels_added le s f'.
     434#le #s #f' #E whd >E #l *;
     435qed.
     436
     437lemma equal_Cminor_labels_added : ∀le,s,s',f.
     438  labels_of s = labels_of s' → Cminor_labels_added le s' f →
     439  Cminor_labels_added le s f.
     440#le #s #s' #f #E whd in ⊢ (% → %) > E #H @H
     441qed.
     442
     443lemma fn_graph_included_inv : ∀label_env,s,f,f0.
     444  ∀f':Σf':partial_fn label_env. add_stmt_inv label_env s f0 f'.
     445  fn_graph_included label_env f f0 →
     446  fn_graph_included label_env f f'.
     447#label_env #s #f #f0 * #f' * #H1 #H2 #H3
     448@(fn_graph_inc_trans … H3 H1)
     449qed.
     450
     451lemma present_inc' : ∀le,s,f,l.
     452  ∀f':(Σf':partial_fn le. add_stmt_inv le s f f').
     453  present ?? (pf_graph le f) l →
     454  present ?? (pf_graph le f') l.
     455#le #s #f #l * #f' * * #H1 #H2 #H3
     456@H1 @H3
     457qed.
     458
     459lemma Cminor_labels_inv : ∀le,s,s',f.
     460  ∀f':Σf':partial_fn le. add_stmt_inv le s' f f'.
     461  Cminor_labels_added le s f →
     462  Cminor_labels_added le s f'.
     463#le #s #s' #f * #f' * #H1 #H2 #H3
     464#l #E cases (H3 l E) #l' * #L #P
     465%{l'} % [ @L | @present_inc' @P ]
     466qed.
     467
     468lemma Cminor_labels_sig : ∀le,s,f.
     469  ∀f':Σf':partial_fn le. fn_graph_included le f f'.
     470  Cminor_labels_added le s f →
     471  Cminor_labels_added le s f'.
     472#le #s #f * #f' #H1 #H2
     473#l #E cases (H2 l E) #l' * #L #P
     474%{l'} % [ @L | @present_inc @P ]
     475qed.
     476
     477let rec add_stmt (env:env) (label_env:label_env) (s:stmt) (Env:stmt_inv env label_env s) (f:partial_fn label_env) (exits:Σls:list label. All ? (present ?? (pf_graph ? f)) ls) on s : res (Σf':partial_fn label_env. add_stmt_inv label_env s f f') ≝
     478match s return λs.stmt_inv env label_env s → res (Σf':partial_fn label_env. add_stmt_inv ? s f f') with
     479[ St_skip ⇒ λ_. OK ? «f, ?»
     480| St_assign _ x e ⇒ λEnv.
     481    let dst ≝ lookup_reg env x (π1 (π1 Env)) in
     482    OK ? «eject … (add_expr ? env ? e (π2 (π1 Env)) dst f), ?»
     483| St_store _ _ q e1 e2 ⇒ λEnv.
     484    let 〈val_reg, f〉 ≝ choose_reg ? env ? e2 f (π2 (π1 Env)) in
     485    let 〈addr_reg, f〉 ≝ choose_reg ? env ? e1 f (π1 (π1 Env)) in
     486    let f ≝ add_fresh_to_graph ? (St_store q addr_reg val_reg) f ? in
     487    let f ≝ add_expr ? env ? e1 (π1 (π1 Env)) addr_reg f in
     488    OK ? «eject … (add_expr ? env ? e2 (π2 (π1 Env)) val_reg f), ?»
     489| St_call return_opt_id e args ⇒ λEnv.
     490    let return_opt_reg ≝
     491      match return_opt_id return λo. ? → ? with
     492      [ None ⇒ λ_. None ?
     493      | Some id ⇒ λEnv. Some ? (lookup_reg env id ?)
     494      ] Env in
     495    let 〈args_regs, f〉 as Eregs ≝ choose_regs ? env args f (π2 (π1 Env)) in
     496    let f ≝
     497      match expr_is_Id ? e with
     498      [ Some id ⇒ add_fresh_to_graph ? (St_call_id id args_regs return_opt_reg) f ?
     499      | None ⇒
     500        let 〈fnr, f〉 ≝ choose_reg ? env ? e f (π2 (π1 (π1 Env))) in
     501        let f ≝ add_fresh_to_graph ? (St_call_ptr fnr args_regs return_opt_reg) f ? in
     502        «eject … (add_expr ? env ? e (π2 (π1 (π1 Env))) fnr f), ?»
     503      ] in
     504    OK ? «eject … (add_exprs ? env args (π2 (π1 Env)) args_regs ? f), ?»
     505| St_tailcall e args ⇒ λEnv.
     506    let 〈args_regs, f〉 as Eregs ≝ choose_regs ? env args f (π2 (π1 Env)) in
     507    let f ≝
     508      match expr_is_Id ? e with
     509      [ Some id ⇒ add_fresh_to_graph ? (λ_. St_tailcall_id id args_regs) f ?
     510      | None ⇒
     511        let 〈fnr, f〉 ≝ choose_reg ? env ? e f (π1 (π1 Env)) in
     512        let f ≝ add_fresh_to_graph ? (λ_. St_tailcall_ptr fnr args_regs) f ? in
     513        «eject … (add_expr ? env ? e (π1 (π1 Env)) fnr f), ?»
     514      ] in
     515    OK ? «eject … (add_exprs ? env args (π2 (π1 Env)) args_regs ? f), ?»
     516| St_seq s1 s2 ⇒ λEnv.
     517    do f2 ← add_stmt env label_env s2 ? f «exits, ?»;
     518    do f1 ← add_stmt env label_env s1 ? f2 «exits, ?»;
     519      OK ? «eject … f1, ?»
     520| St_ifthenelse _ _ e s1 s2 ⇒ λEnv.
     521    let l_next ≝ pf_entry ? f in
     522    do f2 ← add_stmt env label_env s2 (π2 Env) f «exits, ?»;
     523    let l2 ≝ pf_entry ? f2 in
     524    let f ≝ add_fresh_to_graph ? (λ_. R_skip l_next) f2 ? in
     525    do f1 ← add_stmt env label_env s1 (π2 (π1 Env)) f «exits, ?»;
     526    let 〈r,f〉 ≝ choose_reg ? env ? e f1 (π1 (π1 (π1 Env))) in
     527    let f ≝ add_fresh_to_graph ? (λl1. St_cond r l1 l2) f ? in
     528    OK ? «eject … (add_expr ? env ? e (π1 (π1 (π1 Env))) r f), ?»
     529| St_loop s ⇒ λEnv.
     530    let f ≝ add_fresh_to_graph ? R_skip f ? in (* dummy statement, fill in afterwards *)
     531    let l_loop ≝ pf_entry ? f in
     532    do f ← add_stmt env label_env s (π2 Env) f «exits, ?»;
     533    OK ? «eject … (fill_in_statement ? l_loop (R_skip (pf_entry ? f)) f ?), ?»
     534| St_block s ⇒ λEnv.
     535    do f ← add_stmt env label_env s (π2 Env) f («pf_entry ? f::exits, ?»);
     536    OK ? «eject … f, ?»
     537| St_exit n ⇒ λEnv.
     538    do l ← nth_sig ?? (msg BadCminorProgram) exits n;
     539    OK ? «eject … (add_fresh_to_graph ? (λ_. R_skip l) f ?), ?»
     540| St_switch sz sg e tab n ⇒ λEnv.
     541    let 〈r,f〉 ≝ choose_reg ? env ? e f ? in
     542    do l_default ← nth_sig ?? (msg BadCminorProgram) exits n;
     543    let f ≝ add_fresh_to_graph ? (λ_. R_skip l_default) f ? in
     544    do f ← foldr ? (res (Σf':partial_fn ?. ?)) (λcs,f.
    212545      do f ← f;
    213546      let 〈i,n〉 ≝ cs in
    214547      let 〈cr,f〉 ≝ fresh_reg … f (ASTint sz sg) in
    215548      let 〈br,f〉 ≝ fresh_reg … f (ASTint I8 Unsigned) in
    216       do l_case ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits);
    217       let f ≝ add_fresh_to_graph (St_cond br l_case) f in
    218       let f ≝ add_fresh_to_graph (St_op2 (Ocmpu Ceq) (* signed? *) br r cr) f in
    219         OK ? (add_fresh_to_graph (St_const cr (Ointconst ? i)) f)) (OK ? f) tab;
    220     add_expr env ? e r f
    221 | St_return opt_e ⇒
    222     let f ≝ add_fresh_to_graph (λ_. St_return) f in
    223     match opt_e with
    224     [ None ⇒ OK ? f
    225     | Some e ⇒
    226         match f_result f with
    227         [ None ⇒ Error ? (msg ReturnMismatch)
    228         | Some r ⇒ match e with [ dp ty e ⇒ add_expr env ? e (\fst r) f ]
     549      do l_case ← nth_sig ?? (msg BadCminorProgram) exits n;
     550      let f ≝ add_fresh_to_graph ? (St_cond br l_case) f ? in
     551      let f ≝ add_fresh_to_graph ? (St_op2 (Ocmpu Ceq) (* signed? *) br r cr) f ? in
     552      let f ≝ add_fresh_to_graph ? (St_const cr (Ointconst ? i)) f ? in
     553        OK ? «eject … f, ?») (OK ? f) tab;
     554    OK ? «eject … (add_expr ? env ? e (π1 Env) r f), ?»
     555| St_return opt_e ⇒ let f0 ≝ f in
     556    let f ≝ add_fresh_to_graph ? (λ_. R_return) f ? in
     557    match opt_e return λo. stmt_inv ?? (St_return o) → res (Σf':partial_fn label_env.add_stmt_inv ? (St_return o) f0 f') with
     558    [ None ⇒ λEnv. OK ? «eject … f, ?»
     559    | Some e ⇒
     560        match pf_result ? f with
     561        [ None ⇒ λEnv. Error ? (msg ReturnMismatch)
     562        | Some r ⇒
     563            match e return λe.stmt_inv env label_env (St_return (Some ? e)) → res (Σf':partial_fn label_env.add_stmt_inv label_env (St_return (Some ? e)) f0 f') with
     564            [ dp ty e ⇒ λEnv. let f ≝ add_expr label_env env ty e ? (\fst r) f in
     565                              OK ? «eject … f, ?» ]
    229566        ]
    230567    ]
    231 | St_label l s' ⇒
    232     do f ← add_stmt env label_env s' exits f;
    233     do l' ← opt_to_res … [MSG UnknownLabel; CTX ? l] (lookup ?? label_env l);
    234     OK ? (add_to_graph l' (* XXX again: St_skip (f_entry f)*)? f)
    235 | St_goto l ⇒
    236     do l' ← opt_to_res … [MSG UnknownLabel; CTX ? l] (lookup ?? label_env l);
    237     OK ? (add_fresh_to_graph (* XXX again: λ_.St_skip l'*)? f)
    238 | St_cost l s' ⇒
    239     do f ← add_stmt env label_env s' exits f;
    240     OK ? (add_fresh_to_graph (St_cost l) f)
    241 ].
    242 [ @(λ_. St_skip l_next)
    243 | @(St_skip (f_entry f))
    244 | @St_skip
    245 | @(λ_. St_skip l)
    246 | @(λ_. St_skip l_default)
    247 | @(St_skip (f_entry f))
    248 | @(λ_.St_skip l')
    249 ] qed.
    250 
    251 (* Get labels from a Cminor statement. *)
    252 let rec labels_of (s:stmt) : list ident ≝
    253 match s with
    254 [ St_seq s1 s2 ⇒ (labels_of s1) @ (labels_of s2)
    255 | St_ifthenelse _ _ _ s1 s2 ⇒ (labels_of s1) @ (labels_of s2)
    256 | St_loop s ⇒ labels_of s
    257 | St_block s ⇒ labels_of s
    258 | St_label l s ⇒ l::(labels_of s)
    259 | St_cost _ s ⇒ labels_of s
    260 | _ ⇒ [ ]
    261 ].
     568| St_label l s' ⇒ λEnv.
     569    do f ← add_stmt env label_env s' (π2 Env) f exits;
     570    let l' ≝ lookup_label label_env l ? in
     571    OK ? «eject … (add_to_graph ? l' (R_skip (pf_entry ? f)) f ?), ?»
     572| St_goto l ⇒ λEnv.
     573    let l' ≝ lookup_label label_env l ? in
     574    OK ? «eject … (add_fresh_to_graph' ? (λ_.R_skip l') f ?), ?»
     575| St_cost l s' ⇒ λEnv.
     576    do f ← add_stmt env label_env s' (π2 Env) f exits;
     577    OK ? «eject … (add_fresh_to_graph ? (St_cost l) f ?), ?»
     578] Env.
     579try @(π1 Env)
     580try @(π2 Env)
     581try @(π1 (π1 Env))
     582try @(π2 (π1 Env))
     583try @mk_add_stmt_inv
     584try (@empty_Cminor_labels_added @refl)
     585try (@(All_mp … (use_sig ?? exits)))
     586try @fn_graph_included_refl
     587try (repeat @fn_graph_included_inv repeat @fn_graph_included_sig @fn_graph_included_refl)
     588try (#l #H @I)
     589try (#l #H @H)
     590[ -f @(choose_regs_length … (sym_eq … Eregs))
     591| @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_refl
     592| whd in Env @(π1 (π1 (π1 Env)))
     593| -f @(choose_regs_length … (sym_eq … Eregs))
     594| @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_refl
     595| #l #H cases (Exists_append … H)
     596  [ #H1 @(stmt_labels_added ???? (use_sig ?? f1) ? H1)
     597  | #H2 @(Cminor_labels_inv … H2) @(stmt_labels_added ???? (use_sig ?? f2))
     598  ]
     599| #l #H @present_inc' @H
     600| #l #H @present_inc' @use_sig
     601| @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_inv @fn_graph_included_sig @fn_graph_included_inv @fn_graph_included_refl
     602| #l #H cases (Exists_append … H)
     603  [ #H1 @(Cminor_labels_sig … H1) @Cminor_labels_sig @Cminor_labels_sig @(stmt_labels_added ???? (use_sig ?? f1))
     604  | #H2 @(Cminor_labels_sig … H2) @Cminor_labels_sig @Cminor_labels_sig @Cminor_labels_inv @Cminor_labels_sig @(stmt_labels_added ???? (use_sig ?? f2))
     605  ]
     606| #l #H % [ @H | @present_inc @present_inc' @present_inc @(use_sig ?? (pf_entry ? f2)) ]
     607| #l #H @present_inc @present_inc' @H
     608| #l #H @present_inc @H
     609| @(use_sig ?? (pf_entry ??))
     610| @fn_graph_included_sig @fn_graph_included_inv @fn_graph_included_sig @fn_graph_included_refl
     611| @Cminor_labels_sig @(equal_Cminor_labels_added ?? s) [ @refl | @(stmt_labels_added ???? (use_sig ? (add_stmt_inv ???) ?)) ]
     612| % [ @use_sig | @(use_sig ?? exits) ]
     613| @(equal_Cminor_labels_added ?? s) [ @refl | @(stmt_labels_added ???? (use_sig ? (add_stmt_inv ???) ?)) ]
     614| #l #H @use_sig
     615| #l #H @present_inc @use_sig
     616| #l #H % [ @present_inc @present_inc @present_inc @present_inc @use_sig | @H ]
     617| @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_refl
     618| @use_sig
     619| @fn_graph_included_sig @fn_graph_included_inv @fn_graph_included_refl
     620| #l1 * [ #E >E %{l'} % [ @lookup_label_rev' | whd >lookup_add_hit % #E' destruct (E') ]
     621        |@Cminor_labels_sig @(stmt_labels_added ???? (use_sig ? (add_stmt_inv ???) ?))
     622        ]
     623| #l1 #H whd %2 @lookup_label_lpresent
     624| @fn_graph_included_sig @fn_graph_included_inv @fn_graph_included_refl
     625| @(equal_Cminor_labels_added ?? s') [ @refl | @Cminor_labels_sig @(stmt_labels_added ???? (use_sig ? (add_stmt_inv ???) ?)) ]
     626] qed.
     627
     628(*
     629definition mk_fn : ∀le. partial_fn le → internal_function ≝
     630λle, f.
     631  mk_internal_function
     632    (pf_labgen ? f)
     633    (pf_reggen ? f)
     634    (pf_result ? f)
     635    (pf_params ? f)
     636    (pf_locals ? f)
     637    (pf_stacksize ? f)
     638    (pf_graph ? f)
     639    ?
     640    (pf_entry ? f)
     641    (pf_exit ? f).
     642#l #s #E @(labels_P_mp … (pf_closed ? f l s E))
     643#l' * [ // | #H
     644*)
    262645
    263646definition c2ra_function (*: internal_function → internal_function*) ≝
     
    266649let reggen0 ≝ new_universe RegisterTag in
    267650let cminor_labels ≝ labels_of (f_body f) in
    268 let 〈params, env1, reggen1〉 ≝ populate_env (empty_map …) reggen0 (f_params f) in
    269 let 〈locals0, env, reggen2〉 ≝ populate_env env1 reggen1 (f_vars f) in
     651let 〈params, env1, reggen1〉 as E1 ≝ populate_env (empty_map …) reggen0 (f_params f) in
     652let 〈locals0, env, reggen2〉 as E2 ≝ populate_env env1 reggen1 (f_vars f) in
    270653let 〈result, locals, reggen〉 ≝
    271654  match f_return f with
     
    274657      let 〈r,gen〉 ≝ fresh … reggen2 in
    275658        〈Some ? 〈r,ty〉, 〈r,ty〉::locals0, gen〉 ] in
    276 let 〈label_env, labgen1〉 ≝ populate_label_env (empty_map …) labgen0 cminor_labels in
     659let 〈label_env, labgen1〉 as El ≝ populate_label_env (empty_map …) labgen0 cminor_labels in
    277660let 〈l,labgen〉 ≝ fresh … labgen1 in
    278661let emptyfn ≝
    279   mk_internal_function
     662  mk_partial_fn
     663    label_env
    280664    labgen
    281665    reggen
     
    285669    (f_stacksize f)
    286670    (add ?? (empty_map …) l St_return)
     671    ?
    287672    l
    288673    l in
    289 do f ← add_stmt env label_env (f_body f) [ ] emptyfn;
    290 do u1 ← check_universe_ok ? (f_labgen f);
    291 do u2 ← check_universe_ok ? (f_reggen f);
    292 OK ? f
    293 .
    294 >lookup_add_hit % #E destruct
     674do f ← add_stmt env label_env (f_body f) ? emptyfn [ ];
     675do u1 ← check_universe_ok ? (pf_labgen ? f);
     676do u2 ← check_universe_ok ? (pf_reggen ? f);
     677OK ? (mk_internal_function
     678    (pf_labgen ? f)
     679    (pf_reggen ? f)
     680    (pf_result ? f)
     681    (pf_params ? f)
     682    (pf_locals ? f)
     683    (pf_stacksize ? f)
     684    (pf_graph ? f)
     685    ?
     686    (pf_entry ? f)
     687    (pf_exit ? f)
     688  ).
     689[ @I
     690| -emptyfn @(stmt_P_mp … (f_inv f))
     691  #s * #V #L %
     692  [ @(stmt_vars_mp … V)
     693    #i #H cases (Exists_append … H)
     694    [ #H1 @(populate_extends ?????? (sym_eq … E2))
     695          @(populates_env … (sym_eq … E1)) @H1
     696    | #H1 @(populates_env … (sym_eq … E2)) @H1
     697    ]
     698  | @(stmt_labels_mp … L)
     699    #l #H @(populates_label_env … (sym_eq … El)) @H
     700  ]
     701| #l #s #E @(labels_P_mp … (pf_closed ? f l s E))
     702  #l' * [ // | * #l #H cases f #f' * #L #P cases (P l ?)
     703  [ #lx >H * #Ex >(?:lx = l') [ 2: destruct (Ex) @refl ]
     704  #P' @P'
     705  | cases (label_env_contents … (sym_eq ??? El) l ?)
     706    [ #H @H
     707    | whd in ⊢ (% → ?) whd in ⊢ (?(??%?) → ?) * #H cases (H (refl ??))
     708    | whd >H % #E' destruct (E')
     709    ]
     710  ]
     711  ]
     712| #l1 #s #LOOKUP cases (lookup_add_cases ??????? LOOKUP)
     713  [ * #E1 #E2 >E2 @I
     714  | whd in ⊢ (??%? → ?) #E' destruct (E')
     715  ]
     716| *: whd >lookup_add_hit % #E destruct
     717]
    295718qed.
    296719
  • src/RTLabs/syntax.ma

    r1307 r1316  
    2626.
    2727
     28definition labels_P : (label → Prop) → statement → Prop ≝
     29λP,s. match s with
     30[ St_skip l ⇒ P l
     31| St_cost _ l ⇒ P l
     32| St_const _ _ l ⇒ P l
     33| St_op1 _ _ _ l ⇒ P l
     34| St_op2 _ _ _ _ l ⇒ P l
     35| St_load _ _ _ l ⇒ P l
     36| St_store _ _ _ l ⇒ P l
     37| St_call_id _ _ _ l ⇒ P l
     38| St_call_ptr _ _ _ l ⇒ P l
     39| St_tailcall_id _ _ ⇒ True
     40| St_tailcall_ptr _ _ ⇒ True
     41| St_cond _ l1 l2 ⇒ P l1 ∧ P l2
     42| St_jumptable _ ls ⇒ All ? P ls
     43| St_return ⇒ True
     44].
     45
     46lemma labels_P_mp : ∀P,Q. (∀l. P l → Q l) → ∀s.labels_P P s → labels_P Q s.
     47#P #Q #H * /3/
     48#r #l #l' * /3/
     49qed.
     50
     51definition labels_present : graph statement → statement → Prop ≝
     52λg,s. labels_P (present ?? g) s.
     53
     54definition graph_closed : graph statement → Prop ≝
     55λg. ∀l,s. lookup ?? g l = Some ? s → labels_present g s.
     56
    2857record internal_function : Type[0] ≝
    2958{ f_labgen    : universe LabelTag
     
    3463; f_stacksize : nat
    3564; f_graph     : graph statement
    36 ; f_entry     : Σl:label. lookup ?? f_graph l ≠ None ?
    37 ; f_exit      : Σl:label. lookup ?? f_graph l ≠ None ?
     65; f_closed    : graph_closed f_graph
     66; f_entry     : Σl:label. present ?? f_graph l
     67; f_exit      : Σl:label. present ?? f_graph l
    3868}.
    3969
  • src/common/Errors.ma

    r1214 r1316  
    1818include "basics/list.ma".
    1919include "common/PreIdentifiers.ma".
     20include "utilities/lists.ma".
     21include "utilities/deppair.ma".
    2022
    2123(* * Error reporting and the error monad. *)
     
    8789notation "'ret' e" non associative with precedence 45 for @{'ret ${e}}.*)
    8890
     91(* Dependent pair version. *)
     92notation > "vbox('do' « ident v , ident p » ← e; break e')" with precedence 40
     93  for @{ bind ?? ${e} (λ${fresh x}.match ${fresh x} with [ dp ${ident v} ${ident p} ⇒ ${e'} ]) }.
     94
    8995(*
    9096(** The [do] notation, inspired by Haskell's, keeps the code readable. *)
     
    127133  | cons hd tl ⇒ do hd' ← f hd; do tl' ← mmap ?? f tl; OK ? (hd'::tl')
    128134  ].
     135
     136(* And mmap coupled with proofs. *)
     137
     138let rec mmap_sigma (A,B:Type[0]) (P:B → Prop) (f:A → res (Σx:B.P x)) (l:list A) on l : res (Σl':list B.All B P l') ≝
     139match l with
     140[ nil ⇒ OK ? «nil B, ?»
     141| cons h t ⇒
     142    do h' ← f h;
     143    do t' ← mmap_sigma A B P f t;
     144    OK ? «cons B h' t', ?»
     145].
     146whd // %
     147[ @(use_sig B P)
     148| cases t' #l' #p @p
     149] qed.
    129150
    130151(*
     
    239260qed.
    240261
     262(* A variation of bind and its notation that provides an equality proof for
     263   later use. *)
     264
     265definition bind_eq ≝ λA,B:Type[0]. λf: res A. λg: ∀a:A. f = OK ? a → res B.
     266  match f return λx. f = x → ? with
     267  [ OK x ⇒ g x
     268  | Error msg ⇒ λ_. Error ? msg
     269  ] (refl ? f).
     270
     271notation > "vbox('do' ident v 'as' ident E ← e; break e')" with precedence 40 for @{ bind_eq ?? ${e} (λ${ident v}.λ${ident E}.${e'})}.
     272
    241273definition res_to_opt : ∀A:Type[0]. res A → option A ≝
    242274 λA.λv. match v with [ Error _ ⇒ None ? | OK v ⇒ Some … v].
     275
  • src/common/Identifiers.ma

    r1092 r1316  
    33include "ASM/Arithmetic.ma".
    44include "common/Errors.ma".
     5include "utilities/option.ma".
    56
    67(* identifiers and their generators are tagged to differentiate them, and to
     
    122123] qed.
    123124
     125lemma lookup_add_cases : ∀tag,A,m,i,j,a,v.
     126  lookup tag A (add tag A m i a) j = Some ? v →
     127  (i=j ∧ v = a) ∨ lookup tag A m j = Some ? v.
     128#tag #A #m #i #j #a #v
     129cases (identifier_eq ? i j)
     130[ #E >E >lookup_add_hit #H %1 destruct % //
     131| #NE >lookup_add_miss /2/ @eq_identifier_elim /2/
     132] qed.
     133
    124134(* Extract every identifier, value pair from the map. *)
    125135definition elements : ∀tag,A. identifier_map tag A → list (identifier tag × A) ≝
     
    147157  [ an_id_map m' ⇒ fold A B ? (λbv. f (an_identifier ? bv)) m' b ].
    148158
     159(* A predicate that an identifier is in a map, and a failure-avoiding lookup
     160   and update using it. *)
     161
     162definition present : ∀tag,A. identifier_map tag A → identifier tag → Prop ≝
     163λtag,A,m,i. lookup … m i ≠ None ?.
     164
     165definition lookup_present : ∀tag,A. ∀m:identifier_map tag A. ∀id. present ?? m id → A ≝
     166λtag,A,m,id. match lookup ?? m id return λx. x ≠ None ? → ? with [ Some a ⇒ λ_. a | None ⇒ λH.⊥ ].
     167cases H #H'  cases (H' (refl ??)) qed.
     168
     169definition update_present : ∀tag,A. ∀m:identifier_map tag A. ∀id. present ?? m id → A → identifier_map tag A ≝
     170λtag,A,m,l,p,a.
     171  let l' ≝ match l with [ an_identifier l' ⇒ l' ] in
     172  let m' ≝ match m with [ an_id_map m' ⇒ m' ] in
     173  let u' ≝ update A 16 l' a m' in
     174  match u' return λx. update ????? = x → ? with
     175  [ None ⇒ λE.⊥
     176  | Some m' ⇒ λ_. an_id_map tag A m'
     177  ] (refl ? u').
     178whd in p; whd in p:(?(??%?)) E:(??(???%?%)?);
     179cases l in p E; cases m; -l' -m' #m' #l' whd in ⊢ (?(??(???%%)?) → ??(???%?%)? → ?)
     180#NL #U cases NL #H @H @(update_fail … U)
     181qed.
     182
     183lemma update_still_present : ∀tag,A,m,id,a,id'.
     184  ∀H:present tag A m id.
     185  ∀H':present tag A m id'.
     186  present tag A (update_present tag A m id' H' a) id.
     187#tag #A * #m * #id #a * #id' #H #H'
     188whd whd in ⊢ (?(??(???(%??????)?)?)) normalize nodelta
     189cases (identifier_eq ? (an_identifier tag id) (an_identifier tag id'))
     190[ #E >E @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)) >(update_lookup_opt_same ?????? U)
     191  % #E' destruct
     192| #NE @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)) whd in ⊢ (?(??(???%%)?))
     193  <(update_lookup_opt_other ?????? U id) [ @H | % #E cases NE >E #H @H @refl ]
     194] qed.
     195
    149196(* Sets *)
    150197
  • src/utilities/extralib.ma

    r1260 r1316  
    1616include "basics/list.ma".
    1717include "basics/logic.ma".
     18include "utilities/pair.ma".
    1819include "utilities/binary/Z.ma".
    1920include "utilities/binary/positive.ma".
     
    516517lemma p0_plus: ∀n,m:Pos. p0 (n+m) = p0 n + p0 m.
    517518/2/; qed.
    518 
    519 lemma pair_eq1: ∀A,B. ∀a1,a2:A. ∀b1,b2:B. 〈a1,b1〉 = 〈a2,b2〉 → a1 = a2.
    520 #A #B #a1 #a2 #b1 #b2 #H destruct //
    521 qed.
    522 
    523 lemma pair_eq2: ∀A,B. ∀a1,a2:A. ∀b1,b2:B. 〈a1,b1〉 = 〈a2,b2〉 → b1 = b2.
    524 #A #B #a1 #a2 #b1 #b2 #H destruct //
    525 qed.
    526519
    527520theorem divide_ok : ∀m,n,dv,md.
  • src/utilities/lists.ma

    r1195 r1316  
    1717#h #t #IH * /3/
    1818qed.
     19
     20lemma All_nth : ∀A,P,n,l.
     21  All A P l →
     22  ∀a.
     23  nth_opt A n l = Some A a →
     24  P a.
     25#A #P #n elim n
     26[ * [ #_ #a #E whd in E:(??%?); destruct
     27    | #hd #tl * #H #_ #a #E whd in E:(??%?); destruct @H
     28    ]
     29| #m #IH *
     30  [ #_ #a #E whd in E:(??%?); destruct
     31  | #hd #tl * #_ whd in ⊢ (? → ∀_.??%? → ?) @IH
     32  ]
     33] qed.
    1934
    2035let rec exists (A:Type[0]) (p:A → bool) (l:list A) on l : bool ≝
     
    4055] qed.
    4156
     57lemma Exists_append_l : ∀A,P,l1,l2.
     58  Exists A P l1 → Exists A P (l1@l2).
     59#A #P #l1 #l2 elim l1
     60[ *
     61| #h #t #IH *
     62  [ #H %1 @H
     63  | #H %2 @IH @H
     64  ]
     65] qed.
     66
     67lemma Exists_append_r : ∀A,P,l1,l2.
     68  Exists A P l2 → Exists A P (l1@l2).
     69#A #P #l1 #l2 elim l1
     70[ #H @H
     71| #h #t #IH #H %2 @IH @H
     72] qed.
     73
     74lemma Exists_add : ∀A,P,l1,x,l2. Exists A P (l1@l2) → Exists A P (l1@x::l2).
     75#A #P #l1 #x #l2 elim l1
     76[ normalize #H %2 @H
     77| #h #t #IH normalize * [ #H %1 @H | #H %2 @IH @H ]
     78qed.
     79
     80lemma Exists_mid : ∀A,P,l1,x,l2. P x → Exists A P (l1@x::l2).
     81#A #P #l1 #x #l2 #H elim l1
     82[ %1 @H
     83| #h #t #IH %2 @IH
     84] qed.
     85
     86lemma Exists_map : ∀A,B,P,Q,f,l.
     87Exists A P l →
     88(∀a.P a → Q (f a)) →
     89Exists B Q (map A B f l).
     90#A #B #P #Q #f #l elim l //
     91#h #t #IH * [ #H #F %1 @F @H | #H #F %2 @IH [ @H | @F ] ] qed.
     92
    4293lemma map_append : ∀A,B,f,l1,l2.
    4394  (map A B f l1) @ (map A B f l2) = map A B f (l1@l2).
  • src/utilities/option.ma

    r761 r1316  
    33definition option_map : ∀A,B:Type[0]. (A → B) → option A → option B ≝
    44λA,B,f,o. match o with [ None ⇒ None B | Some a ⇒ Some B (f a) ].
     5
     6lemma option_map_none : ∀A,B,f,x.
     7  option_map A B f x = None B → x = None A.
     8#A #B #f * [ // | #a #E whd in E:(??%?); destruct ]
     9qed.
     10
     11lemma option_map_some : ∀A,B,f,x,v.
     12  option_map A B f x = Some B v → ∃y. x = Some ? y ∧ f y = v.
     13#A #B #f *
     14[ #v normalize #E destruct
     15| #y #v normalize #E %{y} destruct % //
     16] qed.
     17
     18lemma refute_none_by_refl : ∀A,B:Type[0]. ∀P:A → B. ∀Q:B → Type[0]. ∀x:option A. ∀H:x = None ? → False.
     19  (∀v. x = Some ? v → Q (P v)) →
     20  Q (match x return λy.x = y → ? with [ Some v ⇒ λ_. P v | None ⇒ λE. match H E in False with [ ] ] (refl ? x)).
     21#A #B #P #Q *
     22[ #H cases (H (refl ??))
     23| #a #H #p normalize @p @refl
     24] qed.
     25
Note: See TracChangeset for help on using the changeset viewer.