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/Cminor
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • 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
Note: See TracChangeset for help on using the changeset viewer.