Changeset 1087 for Deliverables


Ignore:
Timestamp:
Jul 25, 2011, 2:58:10 PM (9 years ago)
Author:
campbell
Message:

Experimental branch where lookups of local variables in Cminor code always
succeed.

Location:
Deliverables/D3.3/id-lookup-branch
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/id-lookup-branch/Clight/toCminor.ma

    r1078 r1087  
    153153definition var_types ≝ identifier_map SymbolTag var_type.
    154154
     155axiom UndeclaredIdentifier : String.
     156
     157definition lookup' ≝
     158λvars:var_types.λid. opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id).
     159
     160definition local_id : var_types → ident → Prop ≝
     161λvars,id. match lookup' vars id with [ OK t ⇒ match t with [ Global _ ⇒ False | _ ⇒ True ] | _ ⇒ False ].
     162
    155163(* Note that the semantics allows locals to shadow globals.
    156164   Parameters start out as locals, but get stack allocated if their address
     
    168176definition characterise_vars : list (ident×region) → function → var_types × nat ≝
    169177λglobals, f.
    170   let m ≝ foldl ?? (λm,idr. add ?? m (\fst idr) (Global (\snd idr))) (empty_map ??) globals in
    171   let m ≝ foldl ?? (λm,v. add ?? m (\fst v) Local) m (fn_params f) in
     178  let m ≝ foldr ?? (λidr,m. add ?? m (\fst idr) (Global (\snd idr))) (empty_map ??) globals in
    172179  let mem_vars ≝ gather_mem_vars_stmt (fn_body f) in
    173   let 〈m,stacksize〉 ≝ foldl ?? (λms,v.
     180  let 〈m,stacksize〉 ≝ foldr ?? (λv,ms.
    174181    let 〈m,stack_high〉 ≝ ms in
    175182    let 〈id,ty〉 ≝ v in
     
    180187  〈m,stacksize〉.
    181188
     189lemma local_id_add_global : ∀vars,id,r,id'.
     190  local_id (add ?? vars id (Global r)) id' → local_id vars id'.
     191#var #id #r #id'
     192whd in ⊢ (% → ?) whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?] → ?)
     193cases (identifier_eq ? id id')
     194[ #E >E >lookup_add_hit whd in ⊢ (% → ?) *
     195| #NE >lookup_add_miss // @eq_identifier_elim // #E >E in NE * /2/
     196] qed.
     197
     198lemma local_id_add_miss : ∀vars,id,t,id'.
     199  id ≠ id' → local_id (add ?? vars id t) id' → local_id vars id'.
     200#vars #id #t #id' #NE
     201whd in ⊢ (% → %)
     202whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ] → match % with [ _ ⇒ ? | _ ⇒ ? ])
     203>lookup_add_miss
     204[ #H @H | @eq_identifier_elim // #E >E in NE * /2/ ]
     205qed.
     206
     207lemma contract_pair : ∀A,B.∀e:A×B. (let 〈a,b〉 ≝ e in 〈a,b〉) = e.
     208#A #B * // qed.
     209
     210lemma extract_pair : ∀A,B,C,D.  ∀u:A×B. ∀Q:A → B → C×D. ∀x,y.
     211((let 〈a,b〉 ≝ u in Q a b) = 〈x,y〉) →
     212∃a,b. 〈a,b〉 = u ∧ Q a b = 〈x,y〉.
     213#A #B #C #D * #a #b #Q #x #y normalize #E1 %{a} %{b} % try @refl @E1 qed.
     214
     215include "utilities/extralib.ma". (* for pair_eq1 to work around destruct's excessive normalisation *)
     216
     217lemma characterise_vars_all : ∀l,f,vars,n.
     218  characterise_vars l f = 〈vars,n〉 →
     219  ∀i. local_id vars i →
     220      Exists ? (λx.\fst x = i) (fn_params f @ fn_vars f).
     221#globals #f
     222whd in ⊢ (∀_.∀_.??%? → ?)
     223elim (fn_params f @ fn_vars f)
     224[ #vars #n whd in ⊢ (??%? → ?) #E <(pair_eq1 ?????? E) -E; #i #H @False_ind
     225  elim globals in H
     226  [ normalize //
     227  | * #id #rg #t #IH whd in ⊢ (?%? → ?) #H @IH @(local_id_add_global ???? H)
     228  ]
     229| * #id #ty #tl #IH #vars #n whd in ⊢ (??(match % with [ _ ⇒ ? ])? → ?) #E #i
     230  cases (identifier_eq ? id i)
     231  [ #E' <E' #H % @refl
     232  | #NE #H whd %2 >(contract_pair var_types nat ?) in E;
     233    whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?)
     234    cases (always_alloc ty ∨ mem_set ?? id) whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?)
     235    #H' lapply (extract_pair ???????? H') -H' * #m0 * #n0 * #EQ #EQ2
     236    @(IH m0 n0)
     237    [ 1,3: @sym_eq whd in ⊢ (???(match ?????% with [ _ ⇒ ? ])) >contract_pair @EQ
     238    | 2,4: <(pair_eq1 ?????? EQ2) in H #H' @(local_id_add_miss … H') @NE
     239    ]
     240  ]
     241] qed.
    182242
    183243include "Cminor/syntax.ma".
     
    186246alias id "CMexpr" = "cic:/matita/cerco/Cminor/syntax/expr.ind(1,0,0)".
    187247
    188 axiom UndeclaredIdentifier : String.
    189248axiom BadlyTypedAccess : String.
    190249axiom BadLvalue : String.
     
    324383].
    325384
     385lemma translate_binop_vars : ∀P,op,ty1,e1,ty2,e2,ty,e.
     386  expr_vars ? e1 P →
     387  expr_vars ? e2 P →
     388  translate_binop op ty1 e1 ty2 e2 ty = OK ? e →
     389  expr_vars ? e P.
     390#P * #ty1 #e1 #ty2 #e2 #ty #e #H1 #H2
     391whd in ⊢ (??%? → ?)
     392[ cases (classify_add ty1 ty2)
     393  [ 3,4: #z ] whd in ⊢ (??%? → ?)
     394  [ generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?)
     395    * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b))
     396    whd in c:(??%?); destruct % [ @H1 | % // @H2 ]
     397  | generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?)
     398    * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b))
     399    whd in c:(??%?); destruct % [ @H2 | % // @H1 ]
     400  | *: #E destruct (E) % try @H1 @H2
     401  ]
     402| cases (classify_sub ty1 ty2)
     403  [ 3,4: #z] whd in ⊢ (??%? → ?)
     404  [ 2: generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?)
     405    * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b))
     406    whd in c:(??%?); destruct % [ % try @H1 @H2 ] @I
     407  | *: #E destruct (E) % try @H1 try @H2 % // @H2
     408  ]
     409| cases (classify_mul ty1 ty2) #E whd in E:(??%?); destruct
     410    % try @H1 @H2
     411| cases (classify_div ty1 ty2) #E whd in E:(??%?); destruct
     412    % try @H1 @H2
     413| cases (classify_mod ty1 ty2) #E whd in E:(??%?); destruct
     414    % try @H1 @H2
     415| 6,7,8,9: #E destruct % try @H1 @H2
     416| cases (classify_shr ty1 ty2) #E whd in E:(??%?); destruct % try @H1 @H2
     417| 11,12,13,14,15,16: cases (classify_cmp ty1 ty2) #E whd in E:(??%?); destruct % try @H1 @H2
     418] qed.
    326419
    327420(* We'll need to implement proper translation of pointers if we really do memory
     
    338431  ].
    339432
    340 definition translate_ptr : ∀r1,r2. CMexpr (ASTptr r1) → res (CMexpr (ASTptr r2)) ≝
    341 λr1,r2,e. check_region r1 r2 ? e.
    342 
    343 definition translate_cast : type → ∀ty2:type. CMexpr ? → res (CMexpr (typ_of_type ty2)) ≝
    344 λty1,ty2.
    345 match ty1 return λx.CMexpr (typ_of_type x) → ? with
     433definition translate_ptr : ∀P,r1,r2. (Σe:CMexpr (ASTptr r1). expr_vars ? e P) → res (Σe':CMexpr (ASTptr r2).expr_vars ? e' P) ≝
     434λP,r1,r2,e. check_region r1 r2 (λr.Σe:CMexpr (ASTptr r).expr_vars ? e P) e.
     435
     436notation "hvbox(« term 19 a, break term 19 b»)"
     437with precedence 90 for @{ (dp ?? $a $b) }.
     438
     439lemma sig_ok : ∀A:Type[0]. ∀P:A → Prop. ∀x:Σx:A.P x.
     440  P x.
     441#A #P * #a #p @p
     442qed.
     443
     444definition translate_cast : ∀P.type → ∀ty2:type. (Σe:CMexpr ?. expr_vars ? e P) → res (Σe':CMexpr (typ_of_type ty2). expr_vars ? e' P) ≝
     445λP,ty1,ty2.
     446match ty1 return λx.(Σe:CMexpr (typ_of_type x). expr_vars ? e P) → ? with
    346447[ Tint sz1 sg1 ⇒ λe.
    347     match ty2 return λx.res (CMexpr (typ_of_type x)) with
     448    match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with
    348449    [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? (Ocastint sg1 sz2) e)
    349450    | Tfloat sz2 ⇒ OK ? (Op1 ?? (match sg1 with [ Unsigned ⇒ Ofloatofintu | _ ⇒ Ofloatofint]) e)
     
    353454    ]
    354455| Tfloat sz1 ⇒ λe.
    355     match ty2 return λx.res (CMexpr (typ_of_type x)) with
    356     [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? (match sg2 with [ Unsigned ⇒ Ointuoffloat sz2 | _ ⇒ Ointoffloat sz2 ]) e)
    357     | Tfloat sz2 ⇒ OK ? (Op1 ?? Oid e) (* FIXME *)
     456    match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with
     457    [ Tint sz2 sg2 ⇒ OK ? «Op1 ?? (match sg2 with [ Unsigned ⇒ Ointuoffloat sz2 | _ ⇒ Ointoffloat sz2 ]) e, ?»
     458    | Tfloat sz2 ⇒ OK ? «Op1 ?? Oid e, ?» (* FIXME *)
    358459    | _ ⇒ Error ? (msg TypeMismatch)
    359460    ]
    360461| Tpointer r1 _ ⇒ λe. (* will need changed for memory regions *)
    361     match ty2 return λx.res (CMexpr (typ_of_type x)) with
    362     [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? (Ointofptr sz2) e)
    363     | Tarray r2 _ _ ⇒ translate_ptr r1 r2 e
    364     | Tpointer r2 _ ⇒ translate_ptr r1 r2 e
     462    match ty2 return λx.res (Σe':CMexpr (typ_of_type x). expr_vars ? e' P) with
     463    [ Tint sz2 sg2 ⇒ OK ? «Op1 ?? (Ointofptr sz2) e, ?»
     464    | Tarray r2 _ _ ⇒ translate_ptr ? r1 r2 e
     465    | Tpointer r2 _ ⇒ translate_ptr ? r1 r2 e
    365466    | _ ⇒ Error ? (msg TypeMismatch)
    366467    ]
    367468| Tarray r1 _ _ ⇒ λe. (* will need changed for memory regions *)
    368     match ty2 return λx.res (CMexpr (typ_of_type x)) with
    369     [ Tint sz2 sg2 ⇒ OK ? (Op1 (ASTptr r1) (ASTint sz2 sg2) (Ointofptr sz2) e)
    370     | Tarray r2 _ _ ⇒ translate_ptr r1 r2 e
    371     | Tpointer r2 _ ⇒ translate_ptr r1 r2 e
     469    match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with
     470    [ Tint sz2 sg2 ⇒ OK ? «Op1 (ASTptr r1) (ASTint sz2 sg2) (Ointofptr sz2) e, ?»
     471    | Tarray r2 _ _ ⇒ translate_ptr ? r1 r2 e
     472    | Tpointer r2 _ ⇒ translate_ptr ? r1 r2 e
    372473    | _ ⇒ Error ? (msg TypeMismatch)
    373474    ]
    374475| _ ⇒ λ_. Error ? (msg TypeMismatch)
    375 ].
     476]. whd @sig_ok qed.
    376477
    377478definition type_should_eq : ∀ty1,ty2. ∀P:type → Type[0]. P ty1 → res (P ty2) ≝
     
    404505] qed.
    405506
    406 let rec translate_expr (vars:var_types) (e:expr) on e : res (CMexpr (typ_of_type (typeof e))) ≝
    407 match e return λe. res (CMexpr (typ_of_type (typeof e))) with
     507definition bind_eq ≝ λA,B:Type[0]. λf: res A. λg: ∀a:A. f = OK ? a → res B.
     508  match f return λx. f = x → ? with
     509  [ OK x ⇒ g x
     510  | Error msg ⇒ λ_. Error ? msg
     511  ] (refl ? f).
     512
     513notation > "vbox('do' ident v 'as' ident E ← e; break e')" with precedence 40 for @{ bind_eq ?? ${e} (λ${ident v}.λ${ident E}.${e'})}.
     514
     515let rec translate_expr (vars:var_types) (e:expr) on e : res (Σe':CMexpr (typ_of_type (typeof e)). expr_vars ? e' (local_id vars)) ≝
     516match e return λe. res (Σe':CMexpr (typ_of_type (typeof e)). expr_vars ? e' (local_id vars)) with
    408517[ Expr ed ty ⇒
    409518  match ed with
    410   [ Econst_int sz i ⇒ OK ? (Cst ? (Ointconst sz i))
    411   | Econst_float f ⇒ OK ? (Cst ? (Ofloatconst f))
     519  [ Econst_int sz i ⇒ OK ? «Cst ? (Ointconst sz i), ?»
     520  | Econst_float f ⇒ OK ? «Cst ? (Ofloatconst f), ?»
    412521  | Evar id ⇒
    413       do c ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id);
    414       match c with
    415       [ Global r ⇒
     522      do c as E ← lookup' vars id;
     523      match c return λx.? = ? → res (Σe':CMexpr ?. ?) with
     524      [ Global r ⇒ λ_.
    416525          match access_mode ty with
    417           [ By_value q ⇒ OK ? (Mem ? r q (Cst ? (Oaddrsymbol id 0)))
    418           | By_reference _ ⇒ OK ? (Cst ? (Oaddrsymbol id 0))
     526          [ By_value q ⇒ OK ? «Mem ? r q (Cst ? (Oaddrsymbol id 0)), ?»
     527          | By_reference _ ⇒ OK ? «Cst ? (Oaddrsymbol id 0), ?»
    419528          | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
    420529          ]
    421       | Stack n ⇒
     530      | Stack n ⇒ λE.
    422531          match access_mode ty with
    423           [ By_value q ⇒ OK ? (Mem ? Any q (Cst ? (Oaddrstack n)))
    424           | By_reference _ ⇒ OK ? (Cst ? (Oaddrstack n))
     532          [ By_value q ⇒ OK ? «Mem ? Any q (Cst ? (Oaddrstack n)), ?»
     533          | By_reference _ ⇒ OK ? «Cst ? (Oaddrstack n), ?»
    425534          | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
    426535          ]
    427       | Local ⇒ OK ? (Id ? id)
    428       ]
     536      | Local ⇒ λE. OK ? «Id ? id, ?»
     537      ] E
    429538  | Ederef e1 ⇒
    430539      do e1' ← translate_expr vars e1;
    431       match typ_of_type (typeof e1) return λx.CMexpr x → ? with
     540      match typ_of_type (typeof e1) return λx.(Σz:CMexpr x.expr_vars ? z (local_id vars)) → ? with
    432541      [ ASTptr r ⇒ λe1'.
    433           match access_mode ty return λx.access_mode ty = x → res (CMexpr (typ_of_type ty)) with
    434           [ By_value q ⇒ λ_.OK ? (Mem (typ_of_type ty) ? q e1')
    435           | By_reference r' ⇒ λE. (region_should_eq r r' ? e1')⌈CMexpr (ASTptr r') ↦ CMexpr (typ_of_type ty)⌉
     542          match access_mode ty return λx.? → res (Σe':CMexpr (typ_of_type ty). expr_vars ? e' (local_id vars)) with
     543          [ By_value q ⇒ λ_.OK ? «Mem (typ_of_type ty) ? q (eject … e1'), ?»
     544          | By_reference r' ⇒ λE. do e1' ← region_should_eq r r' ? e1';
     545                                  OK ? e1'⌈Σe':CMexpr ?. expr_vars ? e' (local_id vars) ↦ Σe':CMexpr (typ_of_type ty). expr_vars ? e' (local_id vars)⌉
    436546          | By_nothing ⇒ λ_. Error ? (msg BadlyTypedAccess)
    437           ] (refl ? (access_mode ty))
     547          ] (access_mode_typ ty)
    438548      | _ ⇒ λ_. Error ? (msg TypeMismatch)
    439549      ] e1'
    440550  | Eaddrof e1 ⇒
    441551      do e1' ← translate_addr vars e1;
    442       match typ_of_type ty return λx.res (CMexpr x) with
     552      match typ_of_type ty return λx.res (Σz:CMexpr x.?) with
    443553      [ ASTptr r ⇒
    444554          match e1' with
     
    450560      do op' ← translate_unop ty op;
    451561      do e1' ← translate_expr vars e1;
    452       OK ? (Op1 ?? op' e1')
     562      OK ? «Op1 ?? op' e1', ?»
    453563  | Ebinop op e1 e2 ⇒
    454564      do e1' ← translate_expr vars e1;
    455565      do e2' ← translate_expr vars e2;
    456       translate_binop op (typeof e1) e1' (typeof e2) e2' ty
     566      do e' as E ← translate_binop op (typeof e1) e1' (typeof e2) e2' ty;
     567      OK ? «e', ?»
    457568  | Ecast ty1 e1 ⇒
    458569      do e1' ← translate_expr vars e1;
    459       do e' ← translate_cast (typeof e1) ty1 e1';
    460       typ_should_eq ? (typ_of_type ty) ? e'
     570      do e' ← translate_cast ? (typeof e1) ty1 e1';
     571      do e' ← typ_should_eq (typ_of_type ty1) (typ_of_type ty) ? e';
     572      OK ? e'
    461573  | Econdition e1 e2 e3 ⇒
    462574      do e1' ← translate_expr vars e1;
    463575      do e2' ← translate_expr vars e2;
    464       do e2' ← type_should_eq ? ty (λx.CMexpr (typ_of_type x)) e2';
     576      do e2' ← type_should_eq ? ty (λx.Σe:CMexpr (typ_of_type x).?) e2';
    465577      do e3' ← translate_expr vars e3;
    466       do e3' ← type_should_eq ? ty (λx.CMexpr (typ_of_type x)) e3';
    467       match typ_of_type (typeof e1) return λx.CMexpr x → ? with
    468       [ ASTint _ _ ⇒ λe1'. OK ? (Cond ??? e1' e2' e3')
     578      do e3' ← type_should_eq ? ty (λx.Σe:CMexpr (typ_of_type x).?) e3';
     579      match typ_of_type (typeof e1) return λx.(Σe1':CMexpr x. expr_vars ? e1' (local_id vars)) → ? with
     580      [ ASTint _ _ ⇒ λe1'. OK ? «Cond ??? e1' e2' e3', ?»
    469581      | _ ⇒ λ_.Error ? (msg TypeMismatch)
    470582      ] e1'
     
    474586      match ty with
    475587      [ Tint sz _ ⇒
    476         do e2' ← type_should_eq ? ty (λx.CMexpr (typ_of_type x)) e2';
    477         match typ_of_type (typeof e1) return λx.CMexpr x → res (CMexpr (typ_of_type ty)) with
    478         [ ASTint _ _ ⇒ λe1'. OK ? (Cond ??? e1' e2' (Cst ? (Ointconst sz (zero ?))))
     588        do e2' ← type_should_eq ? ty (λx.Σe:CMexpr (typ_of_type x).?) e2';
     589        match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e (local_id vars)) → res ? with
     590        [ ASTint _ _ ⇒ λe1'. OK ? «Cond ??? e1' e2' (Cst ? (Ointconst sz (zero ?))), ?»
    479591        | _ ⇒ λ_.Error ? (msg TypeMismatch)
    480592        ] e1'
     
    486598      match ty with
    487599      [ Tint sz _ ⇒
    488         do e2' ← type_should_eq ? ty (λx.CMexpr (typ_of_type x)) e2';
    489         match typ_of_type (typeof e1) return λx.CMexpr x → res (CMexpr (typ_of_type ty)) with
    490         [ ASTint _ _ ⇒ λe1'. OK ? (Cond ??? e1' (Cst ? (Ointconst sz (repr ? 1))) e2')
     600        do e2' ← type_should_eq ? ty (λx.Σe:CMexpr (typ_of_type x).?) e2';
     601        match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e (local_id vars)) → ? with
     602        [ ASTint _ _ ⇒ λe1'. OK ? «Cond ??? e1' (Cst ? (Ointconst sz (repr ? 1))) e2', ?»
    491603        | _ ⇒ λ_.Error ? (msg TypeMismatch)
    492604        ] e1'
     
    495607  | Esizeof ty1 ⇒
    496608      match ty with
    497       [ Tint sz _ ⇒ OK ? (Cst ? (Ointconst sz (repr ? (sizeof ty1))))
     609      [ Tint sz _ ⇒ OK ? «Cst ? (Ointconst sz (repr ? (sizeof ty1))), ?»
    498610      | _ ⇒ Error ? (msg TypeMismatch)
    499611      ]
    500612  | Efield e1 id ⇒
    501       do e' ← match typeof e1 with
     613      match typeof e1 with
    502614      [ Tstruct _ fl ⇒
    503615          do e1' ← translate_addr vars e1;
     
    506618            do off ← field_offset id fl;
    507619            match access_mode ty with
    508             [ By_value q ⇒ OK ? (Mem ? r q (Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst I32 (repr ? off)))))
    509             | By_reference _ ⇒ OK ? (Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst I32 (repr ? off))))
     620            [ By_value q ⇒ OK ? «Mem ? r q (Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst I32 (repr ? off)))),?»
     621            | By_reference _ ⇒ OK ? «Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst I32 (repr ? off))),?»
    510622            | By_nothing ⇒ Error ? (msg BadlyTypedAccess)
    511623            ]
     
    515627          match e1' with
    516628          [ dp r e1' ⇒
    517             match access_mode ty return λx. access_mode ty = x → res (CMexpr (typ_of_type ty)) with
    518             [ By_value q ⇒ λ_. OK ? (Mem ?? q e1')
    519             | By_reference r' ⇒ λE. (region_should_eq r r' ? e1')⌈res (CMexpr (ASTptr r')) ↦ res (CMexpr (typ_of_type ty))⌉
     629            match access_mode ty return λx. access_mode ty = x → res ? with
     630            [ By_value q ⇒ λ_. OK ? «Mem ?? q e1', ?»
     631            | By_reference r' ⇒  λE. do e1' ← region_should_eq r r' ? e1';
     632                                OK ? e1'⌈Σz:CMexpr (ASTptr r').? ↦ Σz:CMexpr (typ_of_type ty).?⌉
    520633            | By_nothing ⇒ λ_. Error ? (msg BadlyTypedAccess)
    521634            ] (refl ? (access_mode ty))
    522635          ]
    523636      | _ ⇒ Error ? (msg BadlyTypedAccess)
    524       ];
    525       typ_should_eq ? (typ_of_type ty) ? e'
     637      ]
    526638  | Ecost l e1 ⇒
    527639      do e1' ← translate_expr vars e1;
    528       do e' ← OK ? (Ecost ? l e1');
    529       typ_should_eq ? (typ_of_type ty) ? e'
     640      do e' ← OK ? «Ecost ? l e1',?»;
     641      typ_should_eq (typ_of_type (typeof e1)) (typ_of_type ty) (λx.Σe:CMexpr x.?) e'
    530642  ]
    531 ] and translate_addr (vars:var_types) (e:expr) on e : res (Σr.CMexpr (ASTptr r)) ≝
     643] and translate_addr (vars:var_types) (e:expr) on e : res (Σr. Σe':CMexpr (ASTptr r). expr_vars ? e' (local_id vars)) ≝
    532644match e with
    533645[ Expr ed _ ⇒
     
    535647  [ Evar id ⇒
    536648      do c ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id);
    537       match c return λ_. res (Σr.CMexpr (ASTptr r)) with
    538       [ Global r ⇒ OK ? (dp ?? r (Cst ? (Oaddrsymbol id 0)))
    539       | Stack n ⇒ OK ? (dp ?? Any (Cst ? (Oaddrstack n)))
     649      match c return λ_. res (Σr.Σz:CMexpr (ASTptr r).?) with
     650      [ Global r ⇒ OK ? «r, «Cst ? (Oaddrsymbol id 0), ?»»
     651      | Stack n ⇒ OK ? «Any, «Cst ? (Oaddrstack n), ?»»
    540652      | Local ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id] (* TODO: could rule out? *)
    541653      ]
    542654  | Ederef e1 ⇒
    543655      do e1' ← translate_expr vars e1;
    544       match typ_of_type (typeof e1) return λx. CMexpr x → res (Σr. CMexpr (ASTptr r)) with
    545       [ ASTptr r ⇒ λe1'.OK ? (dp ?? r e1')
     656      match typ_of_type (typeof e1) return λx. (Σz:CMexpr x.expr_vars ? z (local_id vars)) → res (Σr. Σz:CMexpr (ASTptr r). ?) with
     657      [ ASTptr r ⇒ λe1'.OK ? «r, e1'»
    546658      | _ ⇒ λ_.Error ? (msg BadlyTypedAccess)
    547659      ] e1'
     
    552664          do off ← field_offset id fl;
    553665          match e1' with
    554           [ dp r e1' ⇒ OK ? (dp ?? r (Op2 (ASTptr r) (ASTint I32 Unsigned (* FIXME inefficient?*)) (ASTptr r) Oaddp e1' (Cst ? (Ointconst I32 (repr ? off)))))
     666          [ 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))), ?» »)
    555667          ]
    556668      | Tunion _ _ ⇒ translate_addr vars e1
     
    560672  ]
    561673].
    562 >(access_mode_typ … E) @refl
    563 qed.
    564 
    565 inductive destination : Type[0] ≝
    566 | IdDest : ident → destination
    567 | MemDest : ∀r:region. memory_chunk → CMexpr (ASTptr r) → destination.
     674whd try @I
     675[ >E @I
     676| >(E ? (refl ??)) @refl
     677| 3,4: @sig_ok
     678| @(translate_binop_vars … E) @sig_ok
     679| % [ % ] @sig_ok
     680| % [ % @sig_ok ] whd @I
     681| % [ % [ @sig_ok | @I ] | @sig_ok ]
     682| % [ @sig_ok | @I ]
     683| % [ @sig_ok | @I ]
     684| >(access_mode_typ … E) @refl
     685| @sig_ok
     686| @sig_ok
     687| % [ @sig_ok | @I ]
     688] qed.
     689
     690inductive destination (vars:var_types) : Type[0] ≝
     691| IdDest : ∀id:ident. local_id vars id → destination vars
     692| MemDest : ∀r:region. memory_chunk → (Σe:CMexpr (ASTptr r).expr_vars ? e (local_id vars)) → destination vars.
    568693
    569694definition translate_dest ≝
     
    578703        match ed1 with
    579704        [ Evar id ⇒
    580             do c ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id);
    581             match c with
    582             [ Local ⇒ OK ? (IdDest id)
    583             | Global r ⇒ OK ? (MemDest r q (Cst ? (Oaddrsymbol id 0)))
    584             | Stack n ⇒ OK ? (MemDest Any q (Cst ? (Oaddrstack n)))
    585             ]
     705            do c as E ← lookup' vars id;
     706            match c return λx.? → ? with
     707            [ Local ⇒ λE. OK ? (IdDest vars id ?)
     708            | Global r ⇒ λE. OK ? (MemDest ? r q (Cst ? (Oaddrsymbol id 0)))
     709            | Stack n ⇒ λE. OK ? (MemDest ? Any q (Cst ? (Oaddrstack n)))
     710            ] E
    586711        | _ ⇒
    587712            do e1' ← translate_addr vars e1;
    588             match e1' with [ dp r e1' ⇒ OK ? (MemDest r q e1') ]
     713            match e1' with [ dp r e1' ⇒ OK ? (MemDest ? r q e1') ]
    589714        ]
    590715    ].
     716whd // >E @I
     717qed.
    591718(*
    592719definition translate_assign ≝
     
    614741    ].
    615742*)
    616 definition translate_assign
     743definition translate_assign : ∀vars:var_types. expr → expr → res (Σs:stmt.stmt_vars s (local_id vars))
    617744λvars,e1,e2.
    618745do e2' ← translate_expr vars e2;
    619746do dest ← translate_dest vars e1 (typeof e2);
    620747match dest with
    621 [ IdDest id ⇒ OK ? (St_assign ? id e2')
    622 | MemDest r q e1' ⇒ OK ? (St_store ? r q e1' e2')
    623 ].
     748[ IdDest id p ⇒ OK ? «St_assign ? id e2', ?»
     749| MemDest r q e1' ⇒ OK ? «St_store ? r q e1' e2', ?»
     750].
     751whd
     752[ % // @sig_ok
     753| % @sig_ok
     754] qed.
    624755
    625756definition m_option_map : ∀A,B:Type[0]. (A → res B) → option A → res (option B) ≝
     
    630761].
    631762
    632 definition translate_expr_sigma : var_types → expr → res (Σt:typ.CMexpr t) ≝
     763definition 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) ]) ≝
    633764λv,e.
    634765  do e' ← translate_expr v e;
    635   OK ? (dp ? (λt:typ.CMexpr t) ? e').
     766  OK (Σe:(Σt:typ.CMexpr t).?) ««?, e'», ?».
     767whd @sig_ok
     768qed.
    636769
    637770axiom FIXME : String.
    638771
    639 let rec translate_statement (vars:var_types) (tmp:ident) (tmpp:ident) (s:statement) on s : res stmt ≝
     772let 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') ≝
     773match l with
     774[ nil ⇒ OK ? «nil B, ?»
     775| cons h t ⇒
     776    do h' ← f h;
     777    do t' ← mmap_sigma A B P f t;
     778    OK ? «cons B h' t', ?»
     779].
     780whd // %
     781[ @(sig_ok B P)
     782| cases t' #l' #p @p
     783] qed.
     784
     785let rec translate_statement (vars:var_types) (tmp:Σi:ident.local_id vars i) (tmpp:Σi:ident.local_id vars i) (s:statement) on s : res (Σs:stmt.stmt_vars s (local_id vars)) ≝
    640786match s with
    641 [ Sskip ⇒ OK ? St_skip
     787[ Sskip ⇒ OK ? «St_skip, ?»
    642788| Sassign e1 e2 ⇒ translate_assign vars e1 e2
    643789| Scall ret ef args ⇒
    644790    do ef' ← translate_expr vars ef;
    645     do ef' ← typ_should_eq ? (ASTptr Code) ? ef';
    646     do args' ← mmap … (translate_expr_sigma vars) args;
     791    do ef' ← typ_should_eq (typ_of_type (typeof ef)) (ASTptr Code) ? ef';
     792    do args' ← mmap_sigma … (translate_expr_sigma vars) args;
    647793    match ret with
    648     [ None ⇒ OK ? (St_call (None ?) ef' args')
     794    [ None ⇒ OK ? «St_call (None ?) ef' args', ?»
    649795    | Some e1 ⇒
    650796        do dest ← translate_dest vars e1 (typeof e1); (* TODO: check if it's sane to use e1's type rather than the return type *)
    651797        match dest with
    652         [ IdDest id ⇒ OK ? (St_call (Some ? id) ef' args')
     798        [ IdDest id p ⇒ OK ? «St_call (Some ? id) ef' args', ?»
    653799        | MemDest r q e1' ⇒
    654800            let tmp' ≝ match q with [ Mpointer _ ⇒ tmpp | _ ⇒ tmp ] in
    655             OK ? (St_seq (St_call (Some ? tmp) ef' args') (St_store (typ_of_memory_chunk q) r q e1' (Id ? tmp)))
     801            OK ? «St_seq (St_call (Some ? tmp) ef' args') (St_store (typ_of_memory_chunk q) r q e1' (Id ? tmp)), ?»
    656802        ]
    657803    ]
     
    659805    do s1' ← translate_statement vars tmp tmpp s1;
    660806    do s2' ← translate_statement vars tmp tmpp s2;
    661     OK ? (St_seq s1' s2')
     807    OK ? «St_seq s1' s2', ?»
    662808| Sifthenelse e1 s1 s2 ⇒
    663809    do e1' ← translate_expr vars e1;
    664     match typ_of_type (typeof e1) return λx.CMexpr x → ? with
     810    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with
    665811    [ ASTint _ _ ⇒ λe1'.
    666812        do s1' ← translate_statement vars tmp tmpp s1;
    667813        do s2' ← translate_statement vars tmp tmpp s2;
    668         OK ? (St_ifthenelse ?? e1' s1' s2')
     814        OK ? «St_ifthenelse ?? e1' s1' s2', ?»
    669815    | _ ⇒ λ_.Error ? (msg TypeMismatch)
    670816    ] e1'
    671817| Swhile e1 s1 ⇒
    672818    do e1' ← translate_expr vars e1;
    673     match typ_of_type (typeof e1) return λx.CMexpr x → ? with
     819    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with
    674820    [ ASTint _ _ ⇒ λe1'.
    675821        do s1' ← translate_statement vars tmp tmpp s1;
    676822        (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
    677         OK ? (St_block
     823        OK ? «St_block
    678824               (St_loop
    679                  (St_ifthenelse ?? e1' (St_block s1') (St_exit 0))))
     825                 (St_ifthenelse ?? e1' (St_block s1') (St_exit 0))), ?»
    680826    | _ ⇒ λ_.Error ? (msg TypeMismatch)
    681827    ] e1'
    682828| Sdowhile e1 s1 ⇒
    683829    do e1' ← translate_expr vars e1;
    684     match typ_of_type (typeof e1) return λx.CMexpr x → ? with
     830    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → ? with
    685831    [ ASTint _ _ ⇒ λe1'.
    686832        do s1' ← translate_statement vars tmp tmpp s1;
    687833        (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
    688         OK ? (St_block
     834        OK ? «St_block
    689835               (St_loop
    690                  (St_seq (St_block s1') (St_ifthenelse ?? e1' St_skip (St_exit 0)))))
     836                 (St_seq (St_block s1') (St_ifthenelse ?? e1' St_skip (St_exit 0)))), ?»
    691837    | _ ⇒ λ_.Error ? (msg TypeMismatch)
    692838    ] e1'
    693839| Sfor s1 e1 s2 s3 ⇒
    694840    do e1' ← translate_expr vars e1;
    695     match typ_of_type (typeof e1) return λx.CMexpr x → ? with
     841    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → ? with
    696842    [ ASTint _ _ ⇒ λe1'.
    697843        do s1' ← translate_statement vars tmp tmpp s1;
     
    699845        do s3' ← translate_statement vars tmp tmpp s3;
    700846        (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
    701         OK ? (St_seq s1'
     847        OK ? «St_seq s1'
    702848             (St_block
    703849               (St_loop
    704                  (St_ifthenelse ?? e1' (St_seq (St_block s3') s2') (St_exit 0)))))
     850                 (St_ifthenelse ?? e1' (St_seq (St_block s3') s2') (St_exit 0)))), ?»
    705851    | _ ⇒ λ_.Error ? (msg TypeMismatch)
    706852    ] e1'
    707 | Sbreak ⇒ OK ? (St_exit 1)
    708 | Scontinue ⇒ OK ? (St_exit 0)
     853| Sbreak ⇒ OK ? «St_exit 1, ?»
     854| Scontinue ⇒ OK ? «St_exit 0, ?»
    709855| Sreturn ret ⇒
    710856    match ret with
    711     [ None ⇒ OK ? (St_return (None ?))
     857    [ None ⇒ OK ? «St_return (None ?), ?»
    712858    | Some e1 ⇒
    713859        do e1' ← translate_expr vars e1;
    714         OK ? (St_return (Some ? (dp … e1')))
     860        OK ? «St_return (Some ? (dp … e1')), ?»
    715861    ]
    716862| Sswitch e1 ls ⇒ Error ? (msg FIXME)
    717863| Slabel l s1 ⇒
    718864    do s1' ← translate_statement vars tmp tmpp s1;
    719     OK ? (St_label l s1')
    720 | Sgoto l ⇒ OK ? (St_goto l)
     865    OK ? «St_label l s1', ?»
     866| Sgoto l ⇒ OK ? «St_goto l, ?»
    721867| Scost l s1 ⇒
    722868    do s1' ← translate_statement vars tmp tmpp s1;
    723     OK ? (St_cost l s1')
    724 ].
     869    OK ? «St_cost l s1', ?»
     870].
     871whd try @I
     872[ % [ % [ @p | @sig_ok ] | @(sig_ok ? (All ??)) ]
     873| % [ whd % [ % [ @sig_ok | @sig_ok ] | @(sig_ok ? (All ??)) ] | whd % @sig_ok ]
     874| % [ % [ @I | @sig_ok ] | @(sig_ok ? (All ??)) ]
     875| % @sig_ok
     876| % [ % @sig_ok | @sig_ok ]
     877| % [ % @sig_ok | whd @I ]
     878| % [ @sig_ok | whd % [ % [ @sig_ok | @I ] | @I ] ]
     879| % [ @sig_ok | whd % [ % [ @sig_ok | whd % @sig_ok ] | @I ] ]
     880| @sig_ok
     881| @sig_ok
     882| @sig_ok
     883] qed.
    725884
    726885axiom ParamGlobalMixup : String.
    727886
    728 definition alloc_params : var_types → list (ident×type) → stmt → res stmt
     887definition alloc_params : ∀vars:var_types. list (ident×type) → (Σs:stmt.stmt_vars s (local_id vars)) → res (Σs:stmt.stmt_vars s (local_id vars))
    729888λvars,params,s. foldl ?? (λs,it.
    730889  let 〈id,ty〉 ≝ it in
    731890  do s ← s;
    732   do t ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id);
    733   match t with
    734   [ Local ⇒ OK ? s
    735   | Stack n ⇒
     891  do t as E ← lookup' vars id;
     892  match t return λx.? → ? with
     893  [ Local ⇒ λE. OK (Σs:stmt.?) s
     894  | Stack n ⇒ λE.
    736895      do q ← match access_mode ty with
    737896      [ By_value q ⇒ OK ? q
     
    739898      | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
    740899      ];
    741       OK ? (St_seq (St_store ? Any q (Cst ? (Oaddrstack n)) (Id (typ_of_type ty) id)) s)
    742   | Global _ ⇒ Error ? [MSG ParamGlobalMixup; CTX ? id]
    743   ]) (OK ? s) params.
     900      OK ? «St_seq (St_store ? Any q (Cst ? (Oaddrstack n)) (Id (typ_of_type ty) id)) s, ?»
     901  | Global _ ⇒ λE. Error ? [MSG ParamGlobalMixup; CTX ? id]
     902  ] E) (OK ? s) params.
     903whd % [ whd % [ @I | whd >E @I ] | @sig_ok ]
     904qed.
    744905
    745906definition bigid1 ≝ an_identifier SymbolTag [[
     
    754915false;false;false;true]].
    755916
     917lemma Exists_rm : ∀A,P,l1,x,l2. Exists A P (l1@l2) → Exists A P (l1@x::l2).
     918#A #P #l1 #x #l2 elim l1
     919[ normalize #H %2 @H
     920| #h #t #IH normalize * [ #H %1 @H | #H %2 @IH @H ]
     921qed.
     922
     923lemma Exists_mid : ∀A,P,l1,x,l2. P x → Exists A P (l1@x::l2).
     924#A #P #l1 #x #l2 #H elim l1
     925[ %1 @H
     926| #h #t #IH %2 @IH
     927] qed.
     928
     929lemma Exists_map : ∀A,B,P,Q,f,l.
     930Exists A P l →
     931(∀a.P a → Q (f a)) →
     932Exists B Q (map A B f l).
     933#A #B #P #Q #f #l elim l //
     934#h #t #IH * [ #H #F %1 @F @H | #H #F %2 @IH [ @H | @F ] ] qed.
     935
     936notation > "hvbox('let' 〈ident x,ident y〉 'as' ident E ≝ t 'in' s)"
     937 with precedence 10
     938for @{ match $t return λx.x = $t → ? with [ pair ${ident x} ${ident y} ⇒
     939        λ${ident E}.$s ] (refl ? $t) }.
     940
     941lemma local_id_add_local : ∀vars,id,id'.
     942  local_id vars id →
     943  local_id (add ?? vars id' Local) id.
     944#vars #id #id' #H
     945whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ?] cases (identifier_eq ? id id')
     946[ #E < E >lookup_add_hit //
     947| #NE >lookup_add_miss // @eq_identifier_elim // #E cases NE >E /2/
     948] qed.
     949
    756950(* FIXME: the temporary handling is nonsense, I'm afraid. *)
    757951definition translate_function : list (ident×region) → function → res internal_function ≝
    758952λglobals, f.
    759   let 〈vartypes, stacksize〉 ≝ characterise_vars globals f in
     953  let 〈vartypes0, stacksize〉 as E ≝ characterise_vars globals f in
    760954  let tmp ≝ bigid1 in (* FIXME *)
    761955  let tmpp ≝ bigid2 in (* FIXME *)
     956  let vartypes ≝ add … (add … vartypes0 tmp Local) tmpp Local in
    762957  do s ← translate_statement vartypes tmp tmpp (fn_body f);
    763958  do s ← alloc_params vartypes (fn_params f) s;
     
    767962    (〈tmp,ASTint I32 Unsigned〉::〈tmpp,ASTptr Any〉::(map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_vars f)))
    768963    stacksize
    769     s).
     964    s ?).
     965[ whd whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]) >lookup_add_hit %
     966| whd whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]) >lookup_add_miss [ >lookup_add_hit %| % ]
     967| @stmt_vars_mp [ 3: @sig_ok | skip ]
     968  #i #H cases (identifier_eq ? tmp i)
     969  [ #E <E @Exists_mid @refl
     970  | #NE1 @Exists_rm cases (identifier_eq ? tmpp i)
     971    [ #E <E @Exists_mid @refl
     972    | #NE2 @Exists_rm
     973      >map_append
     974      @Exists_map [ 2: @(characterise_vars_all … (sym_eq ??? E) i)
     975                       @(local_id_add_miss ?? Local ? NE1)
     976                       @(local_id_add_miss ?? Local ? NE2) @H
     977                  | skip
     978                  | * #id #ty #E1 <E1 @refl
     979                  ]
     980    ]
     981  ]
     982] qed.
    770983
    771984definition translate_fundef : list (ident×region) → clight_fundef → res (fundef internal_function) ≝
  • Deliverables/D3.3/id-lookup-branch/Cminor/initialisation.ma

    r961 r1087  
    2222   away. *)
    2323
    24 definition init_datum : ident → region → init_data → nat (*offset*) → stmt
     24definition init_datum : ident → region → init_data → nat (*offset*) → Σs:stmt. stmt_vars s (λ_.False)
    2525λid,r,init,off.
    2626match init_expr init with
     
    3131    ]
    3232].
     33//
     34cases init in p; [ 8: #a #b ] #c #p normalize in p; destruct; /2/
     35qed.
    3336
    34 definition init_var : ident → region → list init_data → stmt ≝
     37lemma unpair : ∀A,B,C,D,x. ∀P:A → B → C. ∀Q:A → B → D.
     38  let 〈a,b〉 ≝ x in 〈P a b, Q a b〉 = 〈P (\fst x) (\snd x), Q (\fst x) (\snd x)〉.
     39#A #B #C #D * // qed.
     40
     41lemma sndredex : ∀A,B,C,D,x. ∀R:D → Prop. ∀P:A → C. ∀Q:A → B → D.
     42  R (Q (\fst x) (\snd x)) → R (\snd (let 〈a,b〉 ≝ x in 〈P a, Q a b〉)).
     43#A #B #C #D *; normalize /2/
     44qed.
     45
     46lemma sig_stmt_vars : ∀P:ident → Prop. ∀s:Σs:stmt.stmt_vars s P.
     47  stmt_vars s P.
     48#P * #s #p whd in ⊢ (?%?) //
     49qed.
     50
     51definition init_var : ident → region → list init_data → Σs:stmt. stmt_vars s (λ_.False) ≝
    3552λid,r,init.
    3653\snd (foldr ??
     
    3855   let 〈off,s〉 ≝ os in
    3956     〈off + (size_init_data datum), St_seq (init_datum id r datum off) s〉)
    40   〈0, St_skip〉 init).
     57  〈0, dp ? (λx.stmt_vars x (λ_.False)) St_skip ?〉 init).
     58[ whd //
     59| elim init whd //
     60  #h #t #IH whd in ⊢ (?(???%)?) @sndredex whd % [ @sig_stmt_vars | @IH ]
     61] qed.
    4162
    42 definition init_vars : list (ident × (list init_data) × region × unit) → stmt ≝
    43 λvars. foldr ??
    44   (λvar,s. St_seq s (init_var (\fst (\fst (\fst var))) (\snd (\fst var)) (\snd (\fst (\fst var))))) St_skip vars.
     63definition init_vars : list (ident × (list init_data) × region × unit) → Σs:stmt. stmt_vars s (λ_.False) ≝
     64λvars. foldr ? (Σs:stmt. stmt_vars s (λ_.False))
     65  (λvar,s. dp ? (λx.stmt_vars x (λ_.False)) (St_seq s (init_var (\fst (\fst (\fst var))) (\snd (\fst var)) (\snd (\fst (\fst var))))) ?) (dp ? (λx.stmt_vars x (λ_.False)) St_skip I) vars.
     66whd % @sig_stmt_vars
     67qed.
    4568
    46 definition add_statement : ident → stmt
     69definition add_statement : ident → (Σs:stmt. stmt_vars s (λ_.False))
    4770                              list (ident × (fundef internal_function)) →
    4871                              list (ident × (fundef internal_function)) ≝
    49 λid,s.
     72λid,s. match s with [ dp s H ⇒
    5073  map ??
    5174    (λidf.
     
    5982                                           (f_vars f)
    6083                                           (f_stacksize f)
    61                                            (St_seq s (f_body f)))〉
     84                                           (St_seq s (f_body f))
     85                                           ?)〉
    6286          | External f ⇒ 〈id, External ? f〉 (* Error ? *)
    6387          ]
    64       | inr _ ⇒ 〈id',f'〉 ]).
     88      | inr _ ⇒ 〈id',f'〉 ]) ].
     89whd %
     90[ @(stmt_vars_mp … H) #i *
     91| //
     92] qed.
    6593
    6694definition empty_vars : list (ident × (list init_data) × region × unit) →
  • Deliverables/D3.3/id-lookup-branch/Cminor/syntax.ma

    r961 r1087  
    22include "common/FrontEndOps.ma".
    33include "common/CostLabel.ma".
     4include "utilities/lists.ma".
     5include "utilities/option.ma".
     6
     7definition present : ∀tag,A. identifier_map tag A → identifier tag → Prop ≝
     8λtag,A,m,i. lookup … m i ≠ None ?.
    49
    510(* TODO: consider making the typing stricter. *)
     
    1318| Cond : ∀sz,sg,t. expr (ASTint sz sg) → expr t → expr t → expr t
    1419| Ecost : ∀t. costlabel → expr t → expr t.
     20
     21(* Assert a predicate on every variable or parameter identifier. *)
     22let rec expr_vars (t:typ) (e:expr t) (P:ident → Prop) on e : Prop ≝
     23match e with
     24[ Id _ i ⇒ P i
     25| Cst _ _ ⇒ True
     26| Op1 _ _ _ e ⇒ expr_vars ? e P
     27| Op2 _ _ _ _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P
     28| Mem _ _ _ e ⇒ expr_vars ? e P
     29| Cond _ _ _ e1 e2 e3 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P ∧ expr_vars ? e3 P
     30| Ecost _ _ e ⇒ expr_vars ? e P
     31].
     32
     33lemma expr_vars_mp : ∀t,e,P,Q.
     34  (∀i. P i → Q i) → expr_vars t e P → expr_vars t e Q.
     35#t0 #e elim e normalize /3/
     36[ #t1 #t2 #t #op #e1 #e2 #IH1 #IH2 #P #Q #H * #H1 #H2
     37  % /3/
     38| #sz #sg #t #e1 #e2 #e3 #IH1 #IH2 #IH3 #P #Q #H * * /5/
     39] qed.
    1540
    1641inductive stmt : Type[0] ≝
     
    3358| St_cost : costlabel → stmt → stmt.
    3459
     60(* Assert a predicate on every variable or parameter identifier. *)
     61let rec stmt_vars (s:stmt) (P:ident → Prop) on s : Prop ≝
     62match s with
     63[ St_skip ⇒ True
     64| St_assign _ i e ⇒ P i ∧ expr_vars ? e P
     65| St_store _ _ _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P
     66| 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
     67| St_tailcall e es ⇒ expr_vars ? e P ∧ All ? (λe.match e with [ dp _ e ⇒ expr_vars ? e P ]) es
     68| St_seq s1 s2 ⇒ stmt_vars s1 P ∧ stmt_vars s2 P
     69| St_ifthenelse _ _ e s1 s2 ⇒ expr_vars ? e P ∧ stmt_vars s1 P ∧ stmt_vars s2 P
     70| St_loop s ⇒ stmt_vars s P
     71| St_block s ⇒ stmt_vars s P
     72| St_exit _ ⇒ True
     73| St_switch _ _ e _ _ ⇒ expr_vars ? e P
     74| St_return oe ⇒ match oe with [ None ⇒ True | Some e ⇒ match e with [ dp _ e ⇒ expr_vars ? e P ] ]
     75| St_label _ s ⇒ stmt_vars s P
     76| St_goto _ ⇒ True
     77| St_cost _ s ⇒ stmt_vars s P
     78].
     79
     80lemma stmt_vars_mp : ∀P,Q. (∀i. P i → Q i) → ∀s. stmt_vars s P → stmt_vars s Q.
     81#P #Q #H #s elim s normalize
     82[ //
     83| #t #id #e * /4/
     84| #t #r #q #e1 #e2 * /4/
     85| * normalize [ 2: #id ] #e #es * * #H1 #H2 #H3 % [ 1,3: % /3/ | *: @(All_mp … H3) * #t #e normalize @expr_vars_mp @H ]
     86| #e #es * #H1 #H2 % [ /3/ | @(All_mp … H2) * /3/ ]
     87| #s1 #s2 #H1 #H2 * /3/
     88| #sz #sg #e #s1 #s2 #H1 #H2 * * /5/
     89| 8,9: #s #H1 #H2 /2/
     90| //
     91| /5/
     92| * normalize [ // | *; normalize /3/ ]
     93| /2/
     94| //
     95| /2/
     96] qed.
     97
    3598record internal_function : Type[0] ≝
    3699{ f_return    : option typ
     
    39102; f_stacksize : nat
    40103; f_body      : stmt
     104; f_bound     : stmt_vars f_body (λi.Exists ? (λx.\fst x = i) (f_params @ f_vars))
    41105}.
    42106
  • Deliverables/D3.3/id-lookup-branch/Cminor/toRTLabs.ma

    r1072 r1087  
    1414     〈〈r,ty〉::rs, add ?? en id r, gen'〉) 〈[ ], en, gen〉.
    1515
    16 definition populate_label_env : label_env → universe LabelTag → list ident → label_env × (universe LabelTag) ≝
     16lemma populates_env : ∀l,e,u,l',e',u'.
     17  populate_env e u l = 〈l',e',u'〉 →
     18  ∀i. Exists ? (λx.\fst x = i) l →
     19      present ?? e' i.
     20#l elim l
     21[ #e #u #l' #e' #u' #E whd in E:(??%?); #i destruct (E) *
     22| * #id #t #tl #IH #e #u #l' #e' #u' #E #i whd in E:(??%?) ⊢ (% → ?);
     23  * [ whd in ⊢ (??%? → ?) #E1 <E1
     24      generalize in E:(??(match % with [ _ ⇒ ? ])?) ⊢ ? * * #x #y #z
     25      whd in ⊢ (??%? → ?) elim (fresh RegisterTag z) #r #gen' #E
     26      whd in E:(??%?);
     27      >(?:e' = add ?? y id r) [ 2: destruct (E) @refl ] (* XXX workaround because destruct overnormalises *)
     28      whd >lookup_add_hit % #A destruct
     29    | #H change in E:(??(match % with [ _ ⇒ ? ])?) with (populate_env e u tl)
     30      lapply (refl ? (populate_env e u tl))
     31      cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?) (* XXX if I do this directly it rewrites both sides of the equality *)
     32      * #rs #e1 #u1 #E1 >E1 in E; whd in ⊢ (??%? → ?) cases (fresh RegisterTag u1) #r #u''
     33      whd in ⊢ (??%? → ?) #E
     34      >(?:e' = add ?? e1 id r) [ 2: destruct (E) @refl ] (* XXX workaround because destruct overnormalises *)
     35      @lookup_add_oblivious
     36      @(IH … E1 ? H)
     37    ]
     38] qed.
     39
     40lemma populate_extends : ∀l,e,u,l',e',u'.
     41  populate_env e u l = 〈l',e',u'〉 →
     42  ∀i. present ?? e i → present ?? e' i.
     43#l elim l
     44[ #e #u #l' #e' #u' #E whd in E:(??%?); destruct //
     45| * #id #t #tl #IH #e #u #l' #e' #u' #E whd in E:(??%?);
     46  change in E:(??(match % with [ _ ⇒ ?])?) with (populate_env e u tl)
     47  lapply (refl ? (populate_env e u tl))
     48  cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?) * #l0 #e0 #u0 #E0
     49  >E0 in E; whd in ⊢ (??%? → ?) cases (fresh RegisterTag u0) #i1 #u1 #E
     50  whd in E:(??%?)
     51  >(?:e' = add ?? e0 id i1) [ 2: destruct (E) @refl ]
     52  #i #H @lookup_add_oblivious @(IH … E0) @H
     53] qed.
     54     
     55definition  populate_label_env : label_env → universe LabelTag → list ident → label_env × (universe LabelTag) ≝
    1756λen,gen. foldr ??
    1857 (λid,engen.
     
    2564#tag #A #m * #i #H @H
    2665qed.
     66
     67definition lookup' : ∀e:env. ∀id. present ?? e id → register ≝
     68λe,id. match lookup ?? e id return λx. x ≠ None ? → ? with [ Some r ⇒ λ_. r | None ⇒ λH.⊥ ].
     69cases H #H'  cases (H' (refl ??)) qed.
     70
    2771
    2872(* Add a statement to the graph, *without* updating the entry label. *)
     
    70114axiom UnknownVariable : String.
    71115
    72 definition choose_reg : env → ∀ty.expr ty → internal_function → res (register × internal_function)
     116definition choose_reg : ∀env:env.∀ty.∀e:expr ty. internal_function → expr_vars ty e (present ?? env) → register × internal_function
    73117λ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)
     118  match e return λty,e. expr_vars ty e (present ?? env) → register × internal_function with
     119  [ Id _ i ⇒ λEnv. 〈lookup' env i Env, f〉
     120  | _ ⇒ λ_.fresh_reg f ty
    80121  ].
    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.
     122 
     123let 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 ≝ 
     124 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.
     125
     126definition exprtyp_present ≝ λenv:env.λe:Σt:typ.expr t.match e with [ dp ty e ⇒ expr_vars ty e (present ?? env) ].
     127
     128definition choose_regs : ∀env:env. ∀es:list (Σt:typ.expr t). internal_function → All ? (exprtyp_present env) es → list register × internal_function ≝
     129λenv,es,f,Env.
     130  foldr_all (Σt:typ.expr t) ??
     131    (λe,p,acc. let 〈rs,f〉 ≝ acc in
     132             let 〈r,f'〉 ≝ match e return λe.? → ? with [ dp t e ⇒ λp.choose_reg env t e f ? ] p in
     133             〈r::rs,f'〉) 〈[ ], f〉 es Env.
     134@p qed.
    88135
    89136axiom BadCminorProgram : String.
    90137
    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);
     138let rec add_expr (env:env) (ty:typ) (e:expr ty) (Env:expr_vars ty e (present ?? env)) (dst:register) (f:internal_function) on e: internal_function ≝
     139match e return λty,e.expr_vars ty e (present ?? env) → internal_function with
     140[ Id _ i ⇒ λEnv.
     141    let r ≝ lookup' env i Env in
    95142    match register_eq r dst with
    96     [ inl _ ⇒ OK ? f
    97     | inr _ ⇒ OK ? (add_fresh_to_graph (St_op1 Oid dst r) f)
     143    [ inl _ ⇒ f
     144    | inr _ ⇒ add_fresh_to_graph (St_op1 Oid dst r) f
    98145    ]
    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;
     146| Cst _ c ⇒ λ_. add_fresh_to_graph (St_const dst c) f
     147| Op1 _ _ op e' ⇒ λEnv.
     148    let 〈r,f〉 ≝ choose_reg env ? e' f Env in
    102149    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;
     150    add_expr env ? e' Env r f
     151| Op2 _ _ _ op e1 e2 ⇒ λEnv.
     152    let 〈r1,f〉 ≝ choose_reg env ? e1 f (proj1 … Env) in
     153    let 〈r2,f〉 ≝ choose_reg env ? e2 f (proj2 … Env) in
    107154    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;
     155    let f ≝ add_expr env ? e2 (proj2 … Env) r2 f in
     156    add_expr env ? e1 (proj1 … Env) r1 f
     157| Mem _ _ q e' ⇒ λEnv.
     158    let 〈r,f〉 ≝ choose_reg env ? e' f Env in
    112159    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 ⇒
     160    add_expr env ? e' Env r f
     161| Cond _ _ _ e' e1 e2 ⇒ λEnv.
    115162    let resume_at ≝ f_entry f in
    116     do f ← add_expr env ? e2 dst f;
     163    let f ≝ add_expr env ? e2 (proj2 … Env) dst f in
    117164    let lfalse ≝ f_entry f in
    118165    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;
     166    let f ≝ add_expr env ? e1 (proj2 … (proj1 … Env)) dst f in
     167    let 〈r,f〉 ≝ choose_reg env ? e' f (proj1 … (proj1 … Env)) in
    121168    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 ].
     169    add_expr env ? e' (proj1 … (proj1 … Env)) r f
     170| Ecost _ l e' ⇒ λEnv.
     171    let f ≝ add_expr env ? e' Env dst f in
     172    add_fresh_to_graph (St_cost l) f
     173] Env.
    127174
    128175(* This shouldn't occur; maybe use vectors? *)
    129176axiom WrongNumberOfArguments : String.
    130177
    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 ⇒
     178let rec add_exprs (env:env) (es:list (Σt:typ.expr t)) (Env:All ? (exprtyp_present env) es) (dsts:list register) (f:internal_function) on es: res internal_function ≝
     179match es return λes.All ?? es → ? with
     180[ nil ⇒ λ_. match dsts with [ nil ⇒ OK ? f | cons _ _ ⇒ Error ? (msg WrongNumberOfArguments) ]
     181| cons e et ⇒ λEnv.
    135182    match dsts with
    136183    [ nil ⇒ Error ? (msg WrongNumberOfArguments)
    137184    | 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 ]
     185        do f ← add_exprs env et ? rt f;
     186        match e return λe.? → ? with [ dp ty e ⇒ λEnv. OK ? (add_expr env ty e ? r f) ] (proj1 ?? Env)
    140187    ]
    141 ].
     188] Env.
     189whd in Env
     190[ @(proj2 … Env) | @Env ] qed.
    142191
    143192axiom UnknownLabel : String.
    144193axiom ReturnMismatch : String.
    145194
    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;
     195let rec add_stmt (env:env) (label_env:label_env) (s:stmt) (Env:stmt_vars s (present ?? env)) (exits:list label) (f:internal_function) on s : res internal_function ≝
     196match s return λs.stmt_vars s (present ?? env) → res internal_function with
     197[ St_skip ⇒ λ_. OK ? f
     198| St_assign _ x e ⇒ λEnv.
     199    let dst ≝ lookup' env x (proj1 … Env) in
     200    OK ? (add_expr env ? e (proj2 … Env) dst f)
     201| St_store _ _ q e1 e2 ⇒ λEnv.
     202    let 〈val_reg, f〉 ≝ choose_reg env ? e2 f (proj2 … Env) in
     203    let 〈addr_reg, f〉 ≝ choose_reg env ? e1 f (proj1 … Env) in
    155204    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 ←
     205    let f ≝ add_expr env ? e1 (proj1 … Env) addr_reg f in
     206    OK ? (add_expr env ? e2 (proj2 … Env) val_reg f)
     207| St_call return_opt_id e args ⇒ λEnv.
     208    let return_opt_reg ≝
     209      match return_opt_id return λo. ? → ? with
     210      [ None ⇒ λ_. None ?
     211      | Some id ⇒ λEnv. Some ? (lookup' env id ?)
     212      ] Env in
     213    let 〈args_regs, f〉 ≝ choose_regs env args f (proj2 … Env) in
     214    let f ≝
    166215      match e with
    167       [ Id _ id ⇒ OK ? (add_fresh_to_graph (St_call_id id args_regs return_opt_reg) f)
     216      [ Id _ id ⇒ add_fresh_to_graph (St_call_id id args_regs return_opt_reg) f
    168217      | _ ⇒
    169         do 〈fnr, f〉 ← choose_reg env ? e f;
     218        let 〈fnr, f〉 ≝ choose_reg env ? e f (proj2 … (proj1 … Env)) in
    170219        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 ←
     220        add_expr env ? e (proj2 … (proj1 … Env)) fnr f
     221      ] in
     222    add_exprs env args (proj2 … Env) args_regs f
     223| St_tailcall e args ⇒ λEnv.
     224    let 〈args_regs, f〉 ≝ choose_regs env args f (proj2 … Env) in
     225    let f ≝
    177226      match e with
    178       [ Id _ id ⇒ OK ? (add_fresh_to_graph (λ_. St_tailcall_id id args_regs) f)
     227      [ Id _ id ⇒ add_fresh_to_graph (λ_. St_tailcall_id id args_regs) f
    179228      | _ ⇒
    180         do 〈fnr, f〉 ← choose_reg env ? e f;
     229        let 〈fnr, f〉 ≝ choose_reg env ? e f (proj1 … Env) in
    181230        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 ⇒
     231        add_expr env ? e (proj1 … Env) fnr f
     232      ] in
     233    add_exprs env args (proj2 … Env) args_regs f
     234| St_seq s1 s2 ⇒ λEnv.
     235    do f ← add_stmt env label_env s2 (proj2 … Env) exits f;
     236    add_stmt env label_env s1 (proj1 … Env) exits f
     237| St_ifthenelse _ _ e s1 s2 ⇒ λEnv.
    189238    let l_next ≝ f_entry f in
    190     do f ← add_stmt env label_env s2 exits f;
     239    do f ← add_stmt env label_env s2 (proj2 … Env) exits f;
    191240    let l2 ≝ f_entry f in
    192241    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;
     242    do f ← add_stmt env label_env s1 (proj2 … (proj1 … Env)) exits f;
     243    let 〈r,f〉 ≝ choose_reg env ? e f (proj1 … (proj1 … Env)) in
    195244    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 ⇒
     245    OK ? (add_expr env ? e (proj1 … (proj1 … Env)) r f)
     246| St_loop s ⇒ λEnv.
    198247    let f ≝ add_fresh_to_graph ? f in (* dummy statement, fill in afterwards *)
    199248    let l_loop ≝ f_entry f in
    200     do f ← add_stmt env label_env s exits f;
     249    do f ← add_stmt env label_env s Env exits f;
    201250    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 ⇒
     251| St_block s ⇒ λEnv.
     252    add_stmt env label_env s Env ((f_entry f)::exits) f
     253| St_exit n ⇒ λEnv.
    205254    do l ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits);
    206255    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;
     256| St_switch sz sg e tab n ⇒ λEnv.
     257    let 〈r,f〉 ≝ choose_reg env ? e f Env in
    209258    do l_default ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits);
    210259    let f ≝ add_fresh_to_graph (* XXX grrrr: λ_. St_skip l_default*)? f in
     
    218267      let f ≝ add_fresh_to_graph (St_op2 (Ocmpu Ceq) (* signed? *) br r cr) f in
    219268        OK ? (add_fresh_to_graph (St_const cr (Ointconst ? i)) f)) (OK ? f) tab;
    220     add_expr env ? e r f
     269    OK ? (add_expr env ? e Env r f)
    221270| St_return opt_e ⇒
    222271    let f ≝ add_fresh_to_graph (λ_. St_return) f in
    223     match opt_e with
    224     [ None ⇒ OK ? f
     272    match opt_e return λo. ? → ? with
     273    [ None ⇒ λEnv. OK ? f
    225274    | Some e ⇒
    226275        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 ]
     276        [ None ⇒ λEnv. Error ? (msg ReturnMismatch)
     277        | Some r ⇒ match e return λe.? → ? with [ dp ty e ⇒ λEnv. OK ? (add_expr env ? e ? (\fst r) f) ]
    229278        ]
    230279    ]
    231 | St_label l s' ⇒
    232     do f ← add_stmt env label_env s' exits f;
     280| St_label l s' ⇒ λEnv.
     281    do f ← add_stmt env label_env s' Env exits f;
    233282    do l' ← opt_to_res … [MSG UnknownLabel; CTX ? l] (lookup ?? label_env l);
    234283    OK ? (add_to_graph l' (* XXX again: St_skip (f_entry f)*)? f)
    235 | St_goto l ⇒
     284| St_goto l ⇒ λEnv.
    236285    do l' ← opt_to_res … [MSG UnknownLabel; CTX ? l] (lookup ?? label_env l);
    237286    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;
     287| St_cost l s' ⇒ λEnv.
     288    do f ← add_stmt env label_env s' Env exits f;
    240289    OK ? (add_fresh_to_graph (St_cost l) f)
    241 ].
    242 [ @(λ_. St_skip l_next)
     290] Env.
     291[ whd in Env @(proj1 … (proj1 … Env))
     292| @(λ_. St_skip l_next)
    243293| @(St_skip (f_entry f))
    244294| @St_skip
    245295| @(λ_. St_skip l)
    246296| @(λ_. St_skip l_default)
     297| whd in Env @Env
    247298| @(St_skip (f_entry f))
    248299| @(λ_.St_skip l')
     
    261312].
    262313
     314notation > "hvbox('let' 〈ident x,ident y,ident z〉 'as' ident E ≝ t 'in' s)"
     315 with precedence 10
     316for @{ match $t return λx.x = $t → ? with [ pair ${fresh xy} ${ident z} ⇒
     317       match ${fresh xy} return λx. ? = $t → ? with [ pair ${ident x} ${ident y} ⇒
     318        λ${ident E}.$s ] ] (refl ? $t) }.
     319
     320
    263321definition c2ra_function (*: internal_function → internal_function*) ≝
    264322λf.
     
    266324let reggen0 ≝ new_universe RegisterTag in
    267325let 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
     326let 〈params, env1, reggen1〉 as E1 ≝ populate_env (empty_map …) reggen0 (f_params f) in
     327let 〈locals0, env, reggen2〉 as E2 ≝ populate_env env1 reggen1 (f_vars f) in
    270328let 〈result, locals, reggen〉 ≝
    271329  match f_return f with
     
    287345    l
    288346    l in
    289 do f ← add_stmt env label_env (f_body f) [ ] emptyfn;
     347do f ← add_stmt env label_env (f_body f) ? [ ] emptyfn;
    290348do u1 ← check_universe_ok ? (f_labgen f);
    291349do u2 ← check_universe_ok ? (f_reggen f);
    292350OK ? f
    293351.
    294 >lookup_add_hit % #E destruct
     352[ @(stmt_vars_mp … (f_bound f))
     353  #i #H cases (Exists_append … H)
     354  [ #H1 @(populate_extends ?????? (sym_eq … E2))
     355        @(populates_env … (sym_eq … E1)) @H1
     356  | #H1 @(populates_env … (sym_eq … E2)) @H1
     357  ]
     358| *: >lookup_add_hit % #E destruct
     359]
    295360qed.
    296361
  • Deliverables/D3.3/id-lookup-branch/utilities/lists.ma

    r816 r1087  
    99let rec All (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝
    1010match l with
    11 [ nil ⇒ False
     11[ nil ⇒ True
    1212| cons h t ⇒ P h ∧ All A P t
    1313].
     14
     15lemma All_mp : ∀A,P,Q. (∀a.P a → Q a) → ∀l. All A P l → All A Q l.
     16#A #P #Q #H #l elim l normalize //
     17#h #t #IH * /3/
     18qed.
    1419
    1520let rec exists (A:Type[0]) (p:A → bool) (l:list A) on l : bool ≝
     
    1823| cons h t ⇒ orb (p h) (exists A p t)
    1924].
     25
     26let rec Exists (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝
     27match l with
     28[ nil ⇒ False
     29| cons h t ⇒ (P h) ∨ (Exists A P t)
     30].
     31
     32lemma Exists_append : ∀A,P,l1,l2.
     33  Exists A P (l1 @ l2) → Exists A P l1 ∨ Exists A P l2.
     34#A #P #l1 elim l1
     35[ normalize /2/
     36| #h #t #IH #l2 *
     37  [ #H /3/
     38  | #H cases (IH l2 H) /3/
     39  ]
     40] qed.
     41
     42lemma map_append : ∀A,B,f,l1,l2.
     43  (map A B f l1) @ (map A B f l2) = map A B f (l1@l2).
     44#A #B #f #l1 elim l1
     45[ #l2 @refl
     46| #h #t #IH #l2 normalize //
     47] qed.
Note: See TracChangeset for help on using the changeset viewer.