Changeset 1626 for src/Cminor


Ignore:
Timestamp:
Dec 19, 2011, 2:48:33 PM (8 years ago)
Author:
campbell
Message:

Add extra type safety in front end. NB: critical freshness parts
axiomatised for now.

Location:
src/Cminor
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/initialisation.ma

    r1610 r1626  
    2121(* None of the additional code introduces locals or labels. *)
    2222definition stmt_inv : stmt → Prop ≝
    23   stmt_P (λs. stmt_vars (λ_.False) s ∧ stmt_labels (λ_.False) s).
     23  stmt_P (λs. stmt_vars (λ_.λ_.False) s ∧ stmt_labels (λ_.False) s).
    2424 
    2525discriminator option.
     
    9797[ % [ % // |
    9898  @(stmt_P_mp … H) #s * #V #L %
    99   [ @(stmt_vars_mp … V) #i *
     99  [ @(stmt_vars_mp … V) #i #t *
    100100  | @(stmt_labels_mp … L) #l *
    101101  ]
  • src/Cminor/semantics.ma

    r1605 r1626  
    1212
    1313definition stmt_inv : internal_function → env → stmt → Prop ≝ λf,en,s.
    14   stmt_P (λs.stmt_vars (present ?? en) s ∧
     14  stmt_P (λs.stmt_vars (λid,ty. present ?? en id) s ∧
    1515             stmt_labels (λl.Exists ? (λl'.l' = l) (labels_of (f_body f))) s) s.
    1616
     
    2323#s * #H1 #H2 %
    2424[ @(stmt_vars_mp … H1)
    25   #l #H @update_still_present @H
     25  #l #ty #H @update_still_present @H
    2626| @H2
    2727] qed.
     
    5353inductive stack : Type[0] ≝
    5454| 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.
     55| Scall : ∀dest:option (ident×typ). ∀f:internal_function. block (* sp *) → ∀en:env. match dest with [ None ⇒ True | Some idty ⇒ present ?? en (\fst idty)] → stmt_inv f en (f_body f) → ∀k:cont. cont_inv f en k → stack → stack.
    5656
    5757inductive state : Type[0] ≝
     
    9292axiom FailedLoad : String.
    9393
    94 let 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) ≝
    95 match e return λt,e.expr_vars t e (present ?? en) → res (trace × val) with
     94let rec eval_expr (ge:genv) (ty0:typ) (e:expr ty0) (en:env) (Env:expr_vars ty0 e (λid,ty. present ?? en id)) (sp:block) (m:mem) on e : res (trace × val) ≝
     95match e return λt,e.expr_vars t e (λid,ty. present ?? en id) → res (trace × val) with
    9696[ Id _ i ⇒ λEnv.
    9797    let r ≝ lookup_present ?? en i ? in
     
    383383        | Some v ⇒ match dst return λdst. match dst with [ None ⇒ ? | Some _ ⇒ ?] → ? with
    384384                   [ None ⇒ λ_. Wrong ??? (msg ReturnMismatch)
    385                    | Some id ⇒ λdstP. ret ? 〈E0, State f St_skip (update_present ?? en id dstP v) ? ? m sp k ? st'〉
     385                   | Some idty ⇒ λdstP. ret ? 〈E0, State f St_skip (update_present ?? en (\fst idty) dstP v) ? ? m sp k ? st'〉
    386386                   ] dstP
    387387        ]
     
    414414  @(stmt_P_mp … (f_inv f))
    415415  #s * #V #L %
    416   [ 1,3: @(stmt_vars_mp … V) #id #EX cases (Exists_append … EX)
     416  [ 1,3: @(stmt_vars_mp … V) #id #ty #EX cases (Exists_append … EX)
    417417    [ 1,3: #H @init_locals_preserves cases (Exists_All … H (pi2 … en))
    418       * #id' #ty * #E1 #H <E1 @H
     418      * #id' #ty * #E1 destruct #H @H
    419419    | *: #H cases (Exists_All … H (init_locals_env … en …))
    420       * #id' #ty * #E1 #H <E1 @H
     420      * #id' #ty * #E1 destruct #H @H
    421421    ]
    422422  | 2,4: @L
  • src/Cminor/syntax.ma

    r1605 r1626  
    1616
    1717(* Assert a predicate on every variable or parameter identifier. *)
    18 let rec expr_vars (t:typ) (e:expr t) (P:ident → Prop) on e : Prop ≝
     18let rec expr_vars (t:typ) (e:expr t) (P:ident → typ → Prop) on e : Prop ≝
    1919match e with
    20 [ Id _ i ⇒ P i
     20[ Id t i ⇒ P i t
    2121| Cst _ _ ⇒ True
    2222| Op1 _ _ _ e ⇒ expr_vars ? e P
     
    2828
    2929lemma expr_vars_mp : ∀t,e,P,Q.
    30   (∀i. P i → Q i) → expr_vars t e P → expr_vars t e Q.
     30  (∀i,t. P i t → Q i t) → expr_vars t e P → expr_vars t e Q.
    3131#t0 #e elim e normalize /3/
    3232[ #t1 #t2 #t #op #e1 #e2 #IH1 #IH2 #P #Q #H * #H1 #H2
     
    4242| St_store : ∀t,r. memory_chunk → expr (ASTptr r) → expr t → stmt
    4343(* ident for returned value, expression to identify fn, args. *)
    44 | St_call : option ident → expr (ASTptr Code) → list (𝚺t. expr t) → stmt
     44| St_call : option (ident × typ) → expr (ASTptr Code) → list (𝚺t. expr t) → stmt
    4545| St_tailcall : expr (ASTptr Code) → list (𝚺t. expr t) → stmt
    4646| St_seq : stmt → stmt → stmt
     
    7676
    7777(* Assert a predicate on every variable or parameter identifier. *)
    78 definition stmt_vars : (ident → Prop) → stmt → Prop ≝
     78definition stmt_vars : (ident → typ → Prop) → stmt → Prop ≝
    7979λP,s.
    8080match s with
    81 [ St_assign _ i e ⇒ P i ∧ expr_vars ? e P
     81[ St_assign t i e ⇒ P i t ∧ expr_vars ? e P
    8282| St_store _ _ _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P
    83 | St_call oi e es ⇒ match oi with [ None ⇒ True | Some i ⇒ P i ] ∧ expr_vars ? e P ∧ All ? (λe.match e with [ mk_DPair _ e ⇒ expr_vars ? e P ]) es
     83| St_call oi e es ⇒ match oi with [ None ⇒ True | Some i ⇒ P (\fst i) (\snd i) ] ∧ expr_vars ? e P ∧ All ? (λe.match e with [ mk_DPair _ e ⇒ expr_vars ? e P ]) es
    8484| St_tailcall e es ⇒ expr_vars ? e P ∧ All ? (λe.match e with [ mk_DPair _ e ⇒ expr_vars ? e P ]) es
    8585| St_ifthenelse _ _ e _ _ ⇒ expr_vars ? e P
     
    107107] qed.
    108108
    109 lemma stmt_vars_mp : ∀P,Q. (∀i. P i → Q i) → ∀s. stmt_vars P s → stmt_vars Q s.
     109lemma stmt_vars_mp : ∀P,Q. (∀i,t. P i t → Q i t) → ∀s. stmt_vars P s → stmt_vars Q s.
    110110#P #Q #H #s elim s normalize
    111111[ //
     
    146146; f_stacksize : nat
    147147; f_body      : stmt
    148 ; f_inv       : stmt_P (λs.stmt_vars (λi.Exists ? (λx.\fst x = i) (f_params @ f_vars)) s ∧
     148     (* Ensure that variables appear in the params and vars list with the
     149        correct typ; and that all goto labels used are declared. *)
     150; f_inv       : stmt_P (λs.stmt_vars (λi,t.Exists ? (λx. x = 〈i,t〉) (f_params @ f_vars)) s ∧
    149151                           stmt_labels (λl.Exists ? (λl'.l' = l) (labels_of f_body)) s) f_body
    150152}.
  • src/Cminor/toRTLabs.ma

    r1611 r1626  
    1 include "basics/lists/list.ma".
     1include "utilities/lists.ma".
    22include "common/Globalenvs.ma".
    33include "Cminor/syntax.ma".
    44include "RTLabs/syntax.ma".
    55
    6 definition env ≝ identifier_map SymbolTag register.
     6definition env ≝ identifier_map SymbolTag (register × typ).
    77definition label_env ≝ identifier_map Label label.
    88definition populate_env : env → universe RegisterTag → list (ident × typ) → list (register×typ) × env × (universe RegisterTag) ≝
     
    1212   let 〈rs,en,gen〉 ≝ rsengen in
    1313   let 〈r,gen'〉 ≝ fresh … gen in
    14      〈〈r,ty〉::rs, add ?? en id r, gen'〉) 〈[ ], en, gen〉.
    15 
     14     〈〈r,ty〉::rs, add ?? en id 〈r,ty〉, gen'〉) 〈[ ], en, gen〉.
     15(*
    1616lemma populates_env : ∀l,e,u,l',e',u'.
    1717  populate_env e u l = 〈l',e',u'〉 →
     
    4949  #i #H @lookup_add_oblivious @(IH … E0) @H
    5050] qed.
    51 
     51*)
    5252definition  populate_label_env : label_env → universe LabelTag → list (identifier Label) → label_env × (universe LabelTag) ≝
    5353λen,gen. foldr ??
     
    9292] qed.
    9393
    94 definition lookup_reg : ∀e:env. ∀id. present ?? e id → register ≝ lookup_present ??.
     94definition Env_has : env → ident → typ → Prop ≝
     95λe,i,t. match lookup ?? e i with [ Some x ⇒ \snd x = t | None ⇒ False ].
     96
     97lemma Env_has_present : ∀e,i,t. Env_has e i t → present … e i.
     98#e #i #t whd in ⊢ (% → %); cases (lookup ?? e i)
     99[ * | * #r #t' #E % #E' destruct ]
     100qed.
     101
     102definition lookup_reg : ∀e:env. ∀id,ty. Env_has e id ty → register ≝ λe,id,ty,H. \fst (lookup_present ?? e id ?).
     103/2/ qed.
    95104definition lookup_label : ∀e:label_env. ∀id. present ?? e id → label ≝ lookup_present ??.
    96105
     
    107116
    108117definition partially_closed : label_env → graph statement → Prop ≝
    109  λe,g. ∀l,s. lookup ?? g l = Some ? s → labels_P (λl. present ?? g l ∨ lpresent e l) s.
     118 λe,g. forall_nodes ? (labels_P (λl. present ?? g l ∨ lpresent e l)) g.
    110119
    111120(* I'd use a single parametrised definition along with internal_function, but
    112121   it's a pain without implicit parameters. *)
    113 record partial_fn (lenv:label_env) : Type[0] ≝
     122record partial_fn (lenv:label_env) (env:env) : Type[0] ≝
    114123{ pf_labgen    : universe LabelTag
    115124; pf_reggen    : universe RegisterTag
    116 ; pf_result    : option (register × typ)
    117125; pf_params    : list (register × typ)
    118126; pf_locals    : list (register × typ)
     127; pf_result    : option (Σrt:register × typ. env_has (pf_locals @ pf_params) (\fst rt) (\snd rt))
     128; pf_envok     : ∀id,ty,r,H. lookup_reg env id ty H = r → env_has (pf_locals @ pf_params) r ty
    119129; pf_stacksize : nat
    120130; pf_graph     : graph statement
    121131; pf_closed    : partially_closed lenv pf_graph
     132; pf_typed     : graph_typed (pf_locals @ pf_params) pf_graph
    122133; pf_entry     : Σl:label. present ?? pf_graph l
    123134; pf_exit      : Σl:label. present ?? pf_graph l
    124135}.
    125136
    126 inductive fn_graph_included (le:label_env) (f1:partial_fn le) (f2:partial_fn le) : Prop ≝
    127 | fn_graph_inc : graph_included (pf_graph ? f1) (pf_graph ? f2) → fn_graph_included le f1 f2.
    128 
    129 lemma fn_graph_inc_trans : ∀le,f1,f2,f3.
    130   fn_graph_included le f1 f2 → fn_graph_included le f2 f3 → fn_graph_included le f1 f3.
    131 #le #f1 #f2 #f3 * #H1 * #H2 % @(graph_inc_trans … H1 H2) qed.
    132 
    133 lemma fn_graph_included_refl : ∀label_env,f.
    134   fn_graph_included label_env f f.
    135 #le #f % #l #H @H qed.
    136 
    137 lemma fn_graph_included_sig : ∀label_env,f,f0.
    138   ∀f':Σf':partial_fn label_env. fn_graph_included ? f0 f'.
    139   fn_graph_included label_env f f0 →
    140   fn_graph_included label_env f f'.
    141 #le #f #f0 * #f' #H1 #H2 @(fn_graph_inc_trans … H2 H1)
    142 qed.
    143 
    144 lemma add_statement_inv : ∀le,l,s.∀f.
    145   labels_present (pf_graph le f) s →
    146   partially_closed le (add … (pf_graph ? f) l s).
    147 #le #l #s #f #p
     137definition fn_env_has ≝
     138  λle,env,f. env_has (pf_locals le env f @ pf_params le env f).
     139
     140record fn_contains (le:label_env) (env:env) (f1:partial_fn le env) (f2:partial_fn le env) : Prop ≝
     141{ fn_con_graph : graph_included (pf_graph … f1) (pf_graph … f2)
     142; fn_con_env : ∀r,ty. fn_env_has le env f1 r ty → fn_env_has le env f2 r ty
     143}.
     144
     145lemma fn_con_trans : ∀le,env,f1,f2,f3.
     146  fn_contains le env f1 f2 → fn_contains le env f2 f3 → fn_contains le env f1 f3.
     147#le #env #f1 #f2 #f3 #H1 #H2 %
     148[ @(graph_inc_trans … (fn_con_graph … H1) (fn_con_graph … H2))
     149| #r #ty #H @(fn_con_env … H2) @(fn_con_env … H1) @H
     150] qed.
     151
     152lemma fn_con_refl : ∀label_env,env,f.
     153  fn_contains label_env env f f.
     154#le #env #f % #l // qed.
     155
     156lemma fn_con_sig : ∀label_env,env,f,f0.
     157  ∀f':Σf':partial_fn label_env env. fn_contains … f0 f'.
     158  fn_contains label_env env f f0 →
     159  fn_contains label_env env f f'.
     160#le #env #f #f0 * #f' #H1 #H2 @(fn_con_trans … H2 H1)
     161qed.
     162
     163lemma add_statement_inv : ∀le,env,l,s.∀f.
     164  labels_present (pf_graph le env f) s →
     165  partially_closed le (add … (pf_graph … f) l s).
     166#le #env #l #s #f #p
    148167#l' #s' #H cases (identifier_eq … l l')
    149168[ #E >E in H; >lookup_add_hit #E' <(?:s = s') [2:destruct //]
    150169  @(labels_P_mp … p) #l0 #H %1 @lookup_add_oblivious @H
    151 | #NE @(labels_P_mp … (pf_closed ? f l' s' ?))
     170| #NE @(labels_P_mp … (pf_closed f l' s' ?))
    152171  [ #lx * [ #H %1 @lookup_add_oblivious @H | #H %2 @H ]
    153172  | >lookup_add_miss in H; /2/
     
    155174] qed.
    156175
     176definition statement_typed_in ≝
     177λle,env,f,s. statement_typed (pf_locals le env f @ pf_params le env f) s.
     178
     179lemma forall_nodes_add : ∀A,P,l,a,g.
     180  forall_nodes A P g → P a → forall_nodes A P (add ?? g l a).
     181#A #P #l #a #g #ALL #NEW
     182#l' #a'
     183cases (identifier_eq … l' l)
     184[ #E destruct >lookup_add_hit #E destruct @NEW
     185| #ne >lookup_add_miss /2/
     186] qed.
     187
    157188(* Add a statement to the graph, *without* updating the entry label. *)
    158 definition 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' ≝
    159 λle,l,s,f,p.
    160   mk_partial_fn le (pf_labgen ? f) (pf_reggen ? f)
    161                 (pf_result ? f) (pf_params ? f) (pf_locals ? f)
    162                 (pf_stacksize ? f) (add ?? (pf_graph ? f) l s) ?
    163                 «pf_entry ? f, ?» «pf_exit ? f, ?».
     189definition fill_in_statement : ∀le,env. label → ∀s:statement. ∀f:partial_fn le env.
     190  labels_present (pf_graph … f) s →
     191  statement_typed_in le env f s →
     192  Σf':partial_fn le env. fn_contains … f f' ≝
     193λle,env,l,s,f,p,tp.
     194  mk_partial_fn le env (pf_labgen … f) (pf_reggen … f)
     195                (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
     196                (pf_stacksize … f) (add ?? (pf_graph … f) l s) ? ?
     197                «pf_entry … f, ?» «pf_exit … f, ?».
    164198[ @add_statement_inv @p
    165 | 2,3: @lookup_add_oblivious [ @(pi2 … (pf_entry le f)) | @(pi2 … (pf_exit le f)) ]
    166 | % #l' @lookup_add_oblivious
     199| @forall_nodes_add //
     200| 3,4: @lookup_add_oblivious [ @(pi2 … (pf_entry … f)) | @(pi2 … (pf_exit … f)) ]
     201| % [ #l' @lookup_add_oblivious | // ]
    167202] qed.
    168203
    169204(* Add a statement to the graph, making it the entry label. *)
    170 definition 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' ≝
    171 λle,l,s,f,p.
    172   mk_partial_fn le (pf_labgen ? f) (pf_reggen ? f)
    173                 (pf_result ? f) (pf_params ? f) (pf_locals ? f)
    174                 (pf_stacksize ? f) (add ?? (pf_graph ? f) l s) ?
    175                 «l, ?» «pf_exit ? f, ?».
     205definition add_to_graph : ∀le,env. label → ∀s:statement. ∀f:partial_fn le env.
     206  labels_present (pf_graph … f) s →
     207  statement_typed_in … f s →
     208  Σf':partial_fn le env. fn_contains … f f' ≝
     209λle,env,l,s,f,p,tl.
     210  mk_partial_fn le env (pf_labgen … f) (pf_reggen … f)
     211                (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
     212                (pf_stacksize … f) (add ?? (pf_graph … f) l s) ? ?
     213                «l, ?» «pf_exit … f, ?».
    176214[ @add_statement_inv @p
     215| @forall_nodes_add //
    177216| whd >lookup_add_hit % #E destruct
    178 | @lookup_add_oblivious @(pi2 … (pf_exit le f))
    179 | % #l' @lookup_add_oblivious
     217| @lookup_add_oblivious @(pi2 … (pf_exit f))
     218| % [ #l' @lookup_add_oblivious | // ]
    180219] qed.
    181220
    182221(* Add a statement with a fresh label to the start of the function.  The
    183222   statement is parametrised by the *next* instruction's label. *)
    184 definition 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' ≝
    185 λle,s,f,p.
    186   let 〈l,g〉 ≝ fresh … (pf_labgen ? f) in
    187   let s' ≝ s (pf_entry ? f) in
    188     (mk_partial_fn le g (pf_reggen ? f)
    189                    (pf_result ? f) (pf_params ? f) (pf_locals ? f)
    190                    (pf_stacksize ? f) (add ?? (pf_graph ? f) l s') ?
    191                    «l, ?» «pf_exit ? f, ?»).
    192 [ % #l' @lookup_add_oblivious
     223definition add_fresh_to_graph : ∀le,env. ∀s:(label → statement). ∀f:partial_fn le env.
     224  (∀l. present ?? (pf_graph … f) l → labels_present (pf_graph … f) (s l)) →
     225  (∀l. statement_typed_in … f (s l)) →
     226  Σf':partial_fn le env. fn_contains … f f' ≝
     227λle,env,s,f,p,tp.
     228  let 〈l,g〉 ≝ fresh … (pf_labgen … f) in
     229  let s' ≝ s (pf_entry … f) in
     230    (mk_partial_fn le env g (pf_reggen … f)
     231                   (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
     232                   (pf_stacksize … f) (add ?? (pf_graph … f) l s') ? ?
     233                   «l, ?» «pf_exit … f, ?»).
     234[ % [ #l' @lookup_add_oblivious | // ]
    193235| @add_statement_inv @p @(pi2 … (pf_entry …))
     236| @forall_nodes_add //
    194237| whd >lookup_add_hit % #E destruct
    195238| @lookup_add_oblivious @(pi2 … (pf_exit …))
     
    198241(* Variants for labels which are (goto) labels *)
    199242
    200 lemma add_statement_inv' : ∀le,l,s.∀f.
    201   labels_P (λl. present ?? (pf_graph le f) l ∨ lpresent le l) s →
    202   partially_closed le (add … (pf_graph ? f) l s).
    203 #le #l #s #f #p
     243lemma add_statement_inv' : ∀le,env,l,s.∀f.
     244  labels_P (λl. present ?? (pf_graph le env f) l ∨ lpresent le l) s →
     245  partially_closed le (add … (pf_graph f) l s).
     246#le #env #l #s #f #p
    204247#l' #s' #H cases (identifier_eq … l l')
    205248[ #E >E in H; >lookup_add_hit #E' <(?:s = s') [2:destruct //]
    206249  @(labels_P_mp … p) #l0 * [ #H %1 @lookup_add_oblivious @H | #H %2 @H ]
    207 | #NE @(labels_P_mp … (pf_closed ? f l' s' ?))
     250| #NE @(labels_P_mp … (pf_closed f l' s' ?))
    208251  [ #lx * [ #H %1 @lookup_add_oblivious @H | #H %2 @H ]
    209252  | >lookup_add_miss in H; /2/
     
    211254] qed.
    212255
    213 definition 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' ≝
    214 λle,s,f,p.
    215   let 〈l,g〉 ≝ fresh … (pf_labgen ? f) in
    216   let s' ≝ s (pf_entry ? f) in
    217     (mk_partial_fn le g (pf_reggen ? f)
    218                    (pf_result ? f) (pf_params ? f) (pf_locals ? f)
    219                    (pf_stacksize ? f) (add ?? (pf_graph ? f) l s') ?
    220                    «l, ?» «pf_exit ? f, ?»).
    221 [ % #l' @lookup_add_oblivious
     256definition add_fresh_to_graph' : ∀le,env. ∀s:(label → statement). ∀f:partial_fn le env.
     257  (∀l. present ?? (pf_graph … f) l → labels_P (λl.present ?? (pf_graph … f) l ∨ lpresent le l) (s l)) →
     258  (∀l. statement_typed_in … f (s l)) →
     259  Σf':partial_fn le env. fn_contains … f f' ≝
     260λle,env,s,f,p,tp.
     261  let 〈l,g〉 ≝ fresh … (pf_labgen … f) in
     262  let s' ≝ s (pf_entry … f) in
     263    (mk_partial_fn le env g (pf_reggen … f)
     264                   (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
     265                   (pf_stacksize … f) (add ?? (pf_graph … f) l s') ? ?
     266                   «l, ?» «pf_exit … f, ?»).
     267[ % [ #l' @lookup_add_oblivious | // ]
    222268| @add_statement_inv' @p @(pi2 … (pf_entry …))
     269| @forall_nodes_add //
    223270| whd >lookup_add_hit % #E destruct
    224271| @lookup_add_oblivious @(pi2 … (pf_exit …))
    225272] qed.
    226273
    227 definition fresh_reg : ∀le. ∀f:partial_fn le. typ → register × (Σf':partial_fn le. fn_graph_included le f f') ≝
    228 λle,f,ty.
    229   let 〈r,g〉 ≝ fresh … (pf_reggen ? f) in
    230     〈r, «mk_partial_fn le (pf_labgen ? f) g
    231                        (pf_result ? f) (pf_params ? f) (〈r,ty〉::(pf_locals ? f))
    232                        (pf_stacksize ? f) (pf_graph ? f) (pf_closed ? f) (pf_entry ? f) (pf_exit ? f), ?»〉.
    233 % #l // qed.
     274lemma extend_typ_env : ∀te,r,t,r',t'.
     275  env_has te r t → env_has (〈r',t'〉::te) r t.
     276#tw #r #t #r' #t' #H %2 @H
     277qed.
     278
     279lemma stmt_extend_typ_env : ∀te,r,t,s.
     280  statement_typed te s → statement_typed (〈r,t〉::te) s.
     281#tw #r #t *
     282[ 4: #t1 #t2 #op #dst #src #l * #H1 #H2 % /2/
     283| *: //
     284] qed.
     285
     286(* A little more nesting in the result type than I'd like, but it keeps the
     287   function closely paired with the proof that it contains f. *)
     288definition fresh_reg : ∀le,env. ∀f:partial_fn le env. ∀ty:typ.
     289  𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σr:register. fn_env_has le env f' r ty) ≝
     290λle,env,f,ty.
     291  let 〈r,g〉 ≝ fresh … (pf_reggen … f) in
     292  let f' ≝
     293    «mk_partial_fn le env
     294       (pf_labgen … f) g (pf_params … f) (〈r,ty〉::(pf_locals … f))
     295       (match pf_result … f with [ None ⇒ None ? | Some rt ⇒ Some ? «pi1 … rt, ?»]) ?
     296       (pf_stacksize … f) (pf_graph … f) (pf_closed … f) ? (pf_entry … f) (pf_exit … f), ?»
     297  in
     298    ❬f' , ?(*«r, ?»*)❭.
     299[ @(«r, ?») % @refl
     300| #l #s #L @stmt_extend_typ_env @(pf_typed … L)
     301| #i #t #r1 #H #L %2 @(pf_envok … f … L)
     302| %2 @(pi2 … rt)
     303| % [ #l // | #r' #ty' #H @extend_typ_env @H ]
     304] qed.
    234305
    235306axiom UnknownVariable : String.
    236307
    237 definition 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') ≝
     308definition choose_reg : ∀le. ∀env:env.∀ty.∀e:expr ty. ∀f:partial_fn le env. expr_vars ty e (Env_has env) →
     309  𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σr:register. fn_env_has le env f' r ty) ≝
    238310λle,env,ty,e,f.
    239   match e return λty,e. expr_vars ty e (present ?? env) → register × (Σf':partial_fn le. fn_graph_included le f f') with
    240   [ Id _ i ⇒ λEnv. 〈lookup_reg env i Env, «f, ?»〉
    241   | _ ⇒ λ_.fresh_reg le f ty
     311  match e return λty,e. expr_vars ty e (Env_has env) → 𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σr:register. fn_env_has le env f' r ty) with
     312  [ Id t i ⇒ λEnv. ❬«f, ?», «lookup_reg env i t Env, ?»❭
     313  | _ ⇒ λ_.fresh_reg le env f ?
    242314  ].
    243 % // qed.
     315[ % //
     316| @(pf_envok … Env) @refl
     317] qed.
    244318 
    245319let 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 ≝ 
    246320 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.
    247 
    248 definition exprtyp_present ≝ λenv:env.λe:𝚺t:typ.expr t.match e with [ mk_DPair ty e ⇒ expr_vars ty e (present ?? env) ].
     321 
     322let rec foldr_all' (A:Type[0]) (P:A → Prop) (B:list A → Type[0]) (f:∀a:A. P a → ∀l. B l → B (a::l)) (b:B [ ]) (l:list A) (H:All ? P l) on l :B l ≝ 
     323 match l return λx.All ? P x → B x with [ nil ⇒ λ_. b | cons a l ⇒ λH. f a (proj1 … H) l (foldr_all' A P B f b l (proj2 … H))] H.
     324
     325definition exprtyp_present ≝ λenv:env.λe:𝚺t:typ.expr t.match e with [ mk_DPair ty e ⇒ expr_vars ty e (Env_has env) ].
     326
     327definition eject' : ∀A. ∀P:A → Type[0]. (𝚺a.P a) → A ≝
     328λA,P,x. match x with [ mk_DPair a _ ⇒ a].
    249329
    250330definition choose_regs : ∀le. ∀env:env. ∀es:list (𝚺t:typ.expr t).
    251                          ∀f:partial_fn le. All ? (exprtyp_present env) es →
    252                          list register × (Σf':partial_fn le. fn_graph_included le f f') ≝
     331                         ∀f:partial_fn le env. All ? (exprtyp_present env) es →
     332                         𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has le env f' r (eject' typ expr e)) rs es) ≝
    253333λle,env,es,f,Env.
    254   foldr_all (𝚺t:typ.expr t) ??
    255     (λe,p,acc. let 〈rs,f〉 ≝ acc in
    256              let 〈r,f'〉 ≝ match e return λe.? → ? with [ mk_DPair t e ⇒ λp.choose_reg le env t e (pi1 ?? f) ? ] p in
    257              〈r::rs,«pi1 ?? f', ?»〉) 〈[ ], «f, ?»〉 es Env.
     334  foldr_all' (𝚺t:typ.expr t) ? (λes. 𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has le env f' r (eject' typ expr e)) rs es))
     335    (λe,p,tl,acc.
     336      match acc return λ_.𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has le env f' r (eject' typ expr e)) rs (e::tl)) with [ mk_DPair f1 rs ⇒
     337        match e return λe.exprtyp_present env e → 𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has le env f' r (eject' typ expr e)) rs (e::tl)) with [ mk_DPair t e ⇒ λp.
     338          match choose_reg le env t e (pi1 … f1) ? return λ_.𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has le env f' r (eject' typ expr e)) rs (❬t,e❭::tl)) with [ mk_DPair f' r ⇒
     339            ❬«pi1 … f', ?»,«(pi1 … r)::(pi1 … rs), ?»❭
     340          ]
     341        ] p
     342      ]) ❬«f, ?», «[ ], I»❭ es Env.
    258343[ @p
    259 | @fn_graph_inc_trans [ 3: @(pi2 ?? f') | skip | @(pi2 ?? f) ]
    260 | % //
     344| cases r #r' #Hr' cases rs #rs' #Hrs'
     345  % [ whd in ⊢ (???%%%); @Hr' | @(All2_mp … Hrs') #r1 * #t1 #e1 #H1 @(fn_con_env … f1) [ @(pi2 … f') | @H1 ] ]
     346| @fn_con_trans [ 3: @(pi2 … f') | skip | @(pi2 … f1) ]
     347| @fn_con_refl
    261348]  qed.
    262349
     
    267354
    268355
    269 lemma choose_regs_length : ∀le,env,es,f,p,rs,f'.
    270   choose_regs le env es f p = 〈rs,f'〉 → |es| = |rs|.
    271 #le #env #es #f elim es
    272 [ #p #rs #f normalize #E destruct @refl
    273 | * #ty #e #t #IH #p #rs #f' whd in ⊢ (??%? → ??%?); #E
    274   cases (extract_pair ???????? E) #rs' * #f'' * #E1 #E2 -E;
    275   cases (extract_pair ???????? E2) #r * #f3 * #E3 #E4 -E2;
    276   destruct (E4) skip (E1 E3) @eq_f @IH
    277   [ @(proj2 … p)
    278   | 3: @sym_eq @E1
    279   | 2: skip
    280   ]
    281 ] qed.
    282 
    283 lemma present_included : ∀le,f,f',l.
    284   fn_graph_included le f f' →
    285   present ?? (pf_graph le f) l →
    286   present ?? (pf_graph le f') l.
    287 #le #f #f' #l * #H1 #H2 @H1 @H2 qed.
     356lemma choose_regs_length : ∀le,env,es,f,p,f',rs.
     357  choose_regs le env es f p = ❬f',rs❭ → |es| = |rs|.
     358#le #env #es #f #p #f' * #rs #H #_ @sym_eq @(All2_length … H)
     359qed.
     360
     361lemma present_included : ∀le,env,f,f',l.
     362  fn_contains le env f f' →
     363  present ?? (pf_graph … f) l →
     364  present ?? (pf_graph … f') l.
     365#le #env #f #f' #l * #H1 #H2 @H1 qed.
    288366
    289367(* Some definitions for the add_stmt function later, which we introduce now so
     
    292370(* We need to show that the graph only grows, and that Cminor labels will end
    293371   up in the graph. *)
    294 definition Cminor_labels_added ≝ λle,s,f'.
     372definition Cminor_labels_added ≝ λle,env,s,f'.
    295373∀l. Exists ? (λl'.l=l') (labels_of s) →
    296 ∃l'. lookup ?? le l = Some ? l' ∧ present ?? (pf_graph le f') l'.
    297 
    298 record add_stmt_inv (le:label_env) (s:stmt) (f:partial_fn le) (f':partial_fn le) : Prop ≝
    299 { stmt_graph_inc : fn_graph_included ? f f'
    300 ; stmt_labels_added : Cminor_labels_added le s f'
     374∃l'. lookup ?? le l = Some ? l' ∧ present ?? (pf_graph le env f') l'.
     375
     376record add_stmt_inv (le:label_env) (env:env) (s:stmt) (f:partial_fn le env) (f':partial_fn le env) : Prop ≝
     377{ stmt_graph_con : fn_contains … f f'
     378; stmt_labels_added : Cminor_labels_added s f'
    301379}.
    302380
    303 (* Build some machinery to solve fn_graph_included goals. *)
     381(* Build some machinery to solve fn_contains goals. *)
    304382
    305383(* A datatype saying how we intend to prove a step. *)
    306 inductive fn_inc_because (le:label_env) : partial_fn le → Type[0] ≝
    307 | fn_inc_eq : ∀f. fn_inc_because le f
    308 | fn_inc_sig : ∀f1,f2:partial_fn le. fn_graph_included le f1 f2 →
    309     ∀f3:(Σf3:partial_fn le.fn_graph_included le f2 f3). fn_inc_because le f3
    310 | fn_inc_addinv : ∀f1,f2:partial_fn le. fn_graph_included le f1 f2 →
    311     ∀s.∀f3:(Σf3:partial_fn le.add_stmt_inv le s f2 f3). fn_inc_because le f3
     384inductive fn_con_because (le:label_env) (env:env) : partial_fn le env → Type[0] ≝
     385| fn_con_eq : ∀f. fn_con_because le env f
     386| fn_con_sig : ∀f1,f2:partial_fn le env. fn_contains … f1 f2 →
     387    ∀f3:(Σf3:partial_fn le env.fn_contains … f2 f3). fn_con_because le env f3
     388| fn_con_addinv : ∀f1,f2:partial_fn le env. fn_contains … f1 f2 →
     389    ∀s.∀f3:(Σf3:partial_fn le env.add_stmt_inv … s f2 f3). fn_con_because le env f3
    312390.
    313391
    314392(* Extract the starting function for a step. *)
    315 let rec fn_inc_because_left le f0  (b:fn_inc_because le f0) on b : partial_fn le
    316   match b with [ fn_inc_eq f ⇒ f | fn_inc_sig f _ _ _ ⇒ f | fn_inc_addinv f _ _ _ _ ⇒ f ].
     393let rec fn_con_because_left le env f0  (b:fn_con_because ?? f0) on b : partial_fn le env
     394  match b with [ fn_con_eq f ⇒ f | fn_con_sig f _ _ _ ⇒ f | fn_con_addinv f _ _ _ _ ⇒ f ].
    317395
    318396(* Some unification hints to pick the right step to apply.  The dummy variable
     
    321399   have reached the desired starting point. *)
    322400
    323 unification hint 0 ≔ le:label_env, f:partial_fn le, dummy:True;
     401unification hint 0 ≔ le:label_env, env:env, f:partial_fn le env, dummy:True;
    324402  f' ≟ f,
    325   b  ≟ fn_inc_eq le f
     403  b  ≟ fn_con_eq le env f
    326404
    327   fn_graph_included le f f' ≡ fn_graph_included le (fn_inc_because_left le f' b) f'
     405  fn_contains le env f f' ≡ fn_contains le env (fn_con_because_left le env f' b) f'
    328406.
    329407
    330 unification hint 1 ≔ le:label_env, f1:partial_fn le, f2:partial_fn le, H12 : fn_graph_included le f1 f2, f3:(Σf3:partial_fn le. fn_graph_included le f2 f3);
    331   b ≟ fn_inc_sig le f1 f2 H12 f3
     408unification hint 1 ≔ le:label_env, env:env, f1:partial_fn le env, f2:partial_fn le env, H12 : fn_contains le env f1 f2, f3:(Σf3:partial_fn le env. fn_contains le env f2 f3);
     409  b ≟ fn_con_sig le env f1 f2 H12 f3
    332410
    333   fn_graph_included le f1 f3 ≡ fn_graph_included le (fn_inc_because_left le f3 b) f3
     411  fn_contains le env f1 f3 ≡ fn_contains le env (fn_con_because_left le env f3 b) f3
    334412.
    335413
    336 unification hint 1 ≔ le:label_env, f1:partial_fn le, f2:partial_fn le, H12 : fn_graph_included le f1 f2, s:stmt, f3:(Σf3:partial_fn le. add_stmt_inv le s f2 f3);
    337   b ≟ fn_inc_addinv le f1 f2 H12 s f3
     414unification hint 1 ≔ le:label_env, env:env, f1:partial_fn le env, f2:partial_fn le env, H12 : fn_contains le env f1 f2, s:stmt, f3:(Σf3:partial_fn le env. add_stmt_inv le env s f2 f3);
     415  b ≟ fn_con_addinv le env f1 f2 H12 s f3
    338416
    339   fn_graph_included le f1 f3 ≡ fn_graph_included le (fn_inc_because_left le f3 b) f3
     417  fn_contains le env f1 f3 ≡ fn_contains le env (fn_con_because_left le env f3 b) f3
    340418.
    341419
    342420(* A lemma to perform a step of the proof.  We can repeat this to do the whole
    343421   proof. *) 
    344 lemma fn_includes_step : ∀le,f. ∀b:fn_inc_because le f. fn_graph_included le (fn_inc_because_left le f b) f.
    345 #le #f *
    346 [ #f @fn_graph_included_refl
    347 | #f1 #f2 #H12 * #f2 #H23 @(fn_graph_inc_trans … H12 H23)
    348 | #f1 #f2 #H12 #s * #f2 * #H23 #X @(fn_graph_inc_trans … H12 H23)
    349 ] qed.
    350 
     422lemma fn_contains_step : ∀le,env,f. ∀b:fn_con_because le env f. fn_contains … (fn_con_because_left … f b) f.
     423#le #env #f *
     424[ #f @fn_con_refl
     425| #f1 #f2 #H12 * #f3 #H23 @(fn_con_trans … H12 H23)
     426| #f1 #f2 #H12 #s * #f3 * #H23 #X @(fn_con_trans … H12 H23)
     427] qed.
     428
     429notation > "vbox('let' ❬ ident v , ident p ❭ ≝ e 'in' break e')" with precedence 10
     430  for @{ match ${e} with [ mk_DPair ${ident v} ${ident p} ⇒ ${e'} ] }.
    351431
    352432axiom BadCminorProgram : String.
    353433
    354 let 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' ≝
    355 match e return λty,e.expr_vars ty e (present ?? env) → Σf':partial_fn le. fn_graph_included le f f' with
    356 [ Id t i ⇒ λEnv.
    357     let r ≝ lookup_reg env i Env in
     434let rec add_expr (le:label_env) (env:env) (ty:typ) (e:expr ty)
     435  (Env:expr_vars ty e (Env_has env)) (f:partial_fn le env)
     436  (dst:Σdst. fn_env_has … f dst ty)
     437  on e: Σf':partial_fn le env. fn_contains … f f' ≝
     438match e return λty,e.expr_vars ty e (Env_has env) → (Σdst. fn_env_has … f dst ty) → Σf':partial_fn le env. fn_contains … f f' with
     439[ Id t i ⇒ λEnv,dst.
     440    let r ≝ lookup_reg env i t Env in
    358441    match register_eq r dst with
    359442    [ inl _ ⇒ «f, ?»
    360     | inr _ ⇒ «pi1 … (add_fresh_to_graph ? (St_op1 t t (Oid t) dst r) f ?), ?»
     443    | inr _ ⇒ «pi1 … (add_fresh_to_graph … (St_op1 t t (Oid t) dst r) f ??), ?»
    361444    ]
    362 | Cst _ c ⇒ λ_. «add_fresh_to_graph ? (St_const dst c) f ?, ?»
    363 | Op1 t t' op e' ⇒ λEnv.
    364     let 〈r,f〉 ≝ choose_reg ? env ? e' f Env in
    365     let f ≝ add_fresh_to_graph ? (St_op1 t t' op dst r) f ? in
    366     let f ≝ add_expr ? env ? e' Env r f in
     445| Cst _ c ⇒ λ_.λdst. «add_fresh_to_graph … (St_const dst c) f ??, ?»
     446| Op1 t t' op e' ⇒ λEnv,dst.
     447    let ❬f,r❭ ≝ choose_reg … e' f Env in
     448    let f ≝ add_fresh_to_graph … (St_op1 t' t op dst r) f ?? in
     449    let f ≝ add_expr … env ? e' Env f «r, ?» in
    367450      «pi1 … f, ?»
    368 | Op2 _ _ _ op e1 e2 ⇒ λEnv.
    369     let 〈r1,f〉 ≝ choose_reg ? env ? e1 f (proj1 … Env) in
    370     let 〈r2,f〉 ≝ choose_reg ? env ? e2 f (proj2 … Env) in
    371     let f ≝ add_fresh_to_graph ? (St_op2 op dst r1 r2) f ? in
    372     let f ≝ add_expr ? env ? e2 (proj2 … Env) r2 f in
    373     let f ≝ add_expr ? env ? e1 (proj1 … Env) r1 f in
     451| Op2 _ _ _ op e1 e2 ⇒ λEnv,dst.
     452    let ❬f,r1❭ ≝ choose_reg … e1 f (proj1 … Env) in
     453    let ❬f,r2❭ ≝ choose_reg … e2 f (proj2 … Env) in
     454    let f ≝ add_fresh_to_graph … (St_op2 op dst r1 r2) f ?? in
     455    let f ≝ add_expr … env ? e2 (proj2 … Env) f «r2, ?» in
     456    let f ≝ add_expr … env ? e1 (proj1 … Env) f «r1, ?» in
    374457      «pi1 … f, ?»
    375 | Mem _ _ q e' ⇒ λEnv.
    376     let 〈r,f〉 ≝ choose_reg ? env ? e' f Env in
    377     let f ≝ add_fresh_to_graph ? (St_load q r dst) f ? in
    378     let f ≝ add_expr ? env ? e' Env r f in
     458| Mem _ _ q e' ⇒ λEnv,dst.
     459    let ❬f,r❭ ≝ choose_reg … e' f Env in
     460    let f ≝ add_fresh_to_graph … (St_load q r dst) f ?? in
     461    let f ≝ add_expr … env ? e' Env f «r,?» in
    379462      «pi1 … f, ?»
    380 | Cond _ _ _ e' e1 e2 ⇒ λEnv.
    381     let resume_at ≝ pf_entry ? f in
    382     let f ≝ add_expr ? env ? e2 (proj2 … Env) dst f in
    383     let lfalse ≝ pf_entry ? f in
    384     let f ≝ add_fresh_to_graph ? (λ_.St_skip resume_at) f ? in
    385     let f ≝ add_expr ? env ? e1 (proj2 … (proj1 … Env)) dst f in
    386     let 〈r,f〉 as E ≝ choose_reg ? env ? e' f (proj1 … (proj1 … Env)) in
    387     let f ≝ add_fresh_to_graph ? (λltrue. St_cond r ltrue lfalse) f ? in
    388     let f ≝ add_expr ? env ? e' (proj1 … (proj1 … Env)) r f in
     463| Cond _ _ _ e' e1 e2 ⇒ λEnv,dst.
     464    let resume_at ≝ pf_entry f in
     465    let f ≝ add_expr … env ? e2 (proj2 … Env) f dst in
     466    let lfalse ≝ pf_entry f in
     467    let f ≝ add_fresh_to_graph … (λ_.St_skip resume_at) f ?? in
     468    let f ≝ add_expr … env ? e1 (proj2 … (proj1 … Env)) f «dst, ?» in
     469    let ❬f,r❭ ≝ choose_reg … e' f ? in
     470    let f ≝ add_fresh_to_graph … (λltrue. St_cond r ltrue lfalse) f ?? in
     471    let f ≝ add_expr … env ? e' (proj1 … (proj1 … Env)) f «r, ?» in
    389472      «pi1 … f, ?»
    390 | Ecost _ l e' ⇒ λEnv.
    391     let f ≝ add_expr ? env ? e' Env dst f in
    392     let f ≝ add_fresh_to_graph ? (St_cost l) f ? in
     473| Ecost _ l e' ⇒ λEnv,dst.
     474    let f ≝ add_expr … env ? e' Env f dst in
     475    let f ≝ add_fresh_to_graph … (St_cost l) f ?? in
    393476      «f, ?»
    394 ] Env.
     477] Env dst.
    395478(* For new labels, we need to step back through the definitions of f until we
    396479   hit the point that it was added. *)
    397 try (repeat @fn_includes_step @I)
     480try (repeat @fn_contains_step @I)
    398481try (#l #H @H)
    399 [ #l #H whd % [ @H | @(present_included … (pi2 … lfalse)) repeat @fn_includes_step @I ]
    400 | #l #H @(present_included … (pi2 ?? resume_at)) repeat @fn_includes_step @I
     482try (#l @I)
     483[ #l % [ @(pi2 … dst) | @(pf_envok … f … Env) @refl ]
     484| 2,6,7: @(fn_con_env … (pi2 ?? r)) repeat @fn_contains_step @I
     485| #l % [ @(fn_con_env … (pi2 ?? dst)) repeat @fn_contains_step @I | @(pi2 ?? r) ]
     486| @(fn_con_env … (pi2 ?? r1)) repeat @fn_contains_step @I
     487| @(fn_con_env … (pi2 ?? r2)) repeat @fn_contains_step @I
     488| #l #H whd % [ @H | @(fn_con_graph … (pi2 ?? lfalse)) repeat @fn_contains_step @I ]
     489| @(π1 (π1 Env))
     490| @(fn_con_env … (pi2 ?? dst)) repeat @fn_contains_step @I
     491| #l #H @(fn_con_graph … (pi2 ?? resume_at)) repeat @fn_contains_step @I
    401492] qed.
    402493
    403494let rec add_exprs (le:label_env) (env:env) (es:list (𝚺t:typ.expr t)) (Env:All ? (exprtyp_present env) es)
    404                   (dsts:list register) (pf:|es|=|dsts|) (f:partial_fn le) on es: Σf':partial_fn le. fn_graph_included le f f' ≝
    405 match es return λes.All ?? es → |es|=|dsts| → ? with
    406 [ nil ⇒ λ_. match dsts return λx. ?=|x| → Σf':partial_fn le. fn_graph_included le f f' with [ nil ⇒ λ_. «f, ?» | cons _ _ ⇒ λpf.⊥ ]
     495                  (dsts:list register) (pf:|es|=|dsts|) (f:partial_fn le env)
     496                  (Hdsts:All2 ?? (λr,e. fn_env_has le env f r (eject' typ expr e)) dsts es) on es: Σf':partial_fn le env. fn_contains le env f f' ≝
     497match es return λes.All ?? es → All2 ???? es → |es|=|dsts| → ? with
     498[ nil ⇒ λ_.λ_. match dsts return λx. ?=|x| → Σf':partial_fn le env. fn_contains le env f f' with [ nil ⇒ λ_. «f, ?» | cons _ _ ⇒ λpf.⊥ ]
    407499| cons e et ⇒ λEnv.
    408     match dsts return λx. ?=|x| → ? with
    409     [ nil ⇒ λpf.⊥
    410     | cons r rt ⇒ λpf.
    411         let f ≝ add_exprs ? env et ? rt ? f in
    412         match e return λe.exprtyp_present ? e → ? with [ mk_DPair ty e ⇒ λEnv.
    413           let f ≝ add_expr ? env ty e ? r f in
    414             «pi1 … f, ?» ] (proj1 ?? Env)
     500    match dsts return λx. All2 ?? (λr,e. fn_env_has le env f r (eject' typ expr e)) x (e::et) → ?=|x| → ? with
     501    [ nil ⇒ λ_.λpf.⊥
     502    | cons r rt ⇒ λHdsts,pf.
     503        let f' ≝ add_exprs ? env et ? rt ? f ? in
     504        match e return λe.exprtyp_present ? e → fn_env_has le env f r (eject' typ expr e) → ? with [ mk_DPair ty e ⇒ λEnv,Hr.
     505          let f'' ≝ add_expr ? env ty e ? f' r in
     506            «pi1 … f'', ?»
     507        ] (proj1 ?? Env) (π1 Hdsts)
    415508    ]
    416 ] Env pf.
    417 try (repeat @fn_includes_step @I)
     509] Env Hdsts pf.
     510try (repeat @fn_contains_step @I)
    418511[ 1,2: normalize in pf; destruct
    419512| @Env
     513| @(fn_con_env … Hr) repeat @fn_contains_step @I
    420514| @(proj2 … Env)
    421515| normalize in pf; destruct @e0
     516| @(π2 Hdsts)
    422517] qed.
    423518
     
    426521
    427522definition stmt_inv : env → label_env → stmt → Prop ≝
    428 λenv,lenv. stmt_P (λs. stmt_vars (present ?? env) s ∧ stmt_labels (present ?? lenv) s).
     523λenv,lenv. stmt_P (λs. stmt_vars (Env_has env) s ∧ stmt_labels (present ?? lenv) s).
    429524
    430525(* Trick to avoid multiplying the proof obligations for the non-Id cases. *)
     
    468563qed.
    469564
    470 lemma empty_Cminor_labels_added : ∀le,s,f'.
    471   labels_of s = [ ] → Cminor_labels_added le s f'.
    472 #le #s #f' #E whd >E #l *;
    473 qed.
    474 
    475 lemma equal_Cminor_labels_added : ∀le,s,s',f.
    476   labels_of s = labels_of s' → Cminor_labels_added le s' f →
    477   Cminor_labels_added le s f.
    478 #le #s #s' #f #E whd in ⊢ (% → %); > E #H @H
    479 qed.
    480 
    481 lemma Cminor_labels_inc : ∀le,s,f,f'.
    482   fn_graph_included le f f' →
    483   Cminor_labels_added le s f →
    484   Cminor_labels_added le s f'.
    485 #le #s #f #f' #INC #ADDED
     565lemma empty_Cminor_labels_added : ∀le,env,s,f'.
     566  labels_of s = [ ] → Cminor_labels_added le env s f'.
     567#le #env #s #f' #E whd >E #l *;
     568qed.
     569
     570lemma equal_Cminor_labels_added : ∀le,env,s,s',f.
     571  labels_of s = labels_of s' → Cminor_labels_added s' f →
     572  Cminor_labels_added le env s f.
     573#le #env #s #s' #f #E whd in ⊢ (% → %); > E #H @H
     574qed.
     575
     576lemma Cminor_labels_con : ∀le,env,s,f,f'.
     577  fn_contains le env f f' →
     578  Cminor_labels_added s f →
     579  Cminor_labels_added s f'.
     580#le #env #s #f #f' #INC #ADDED
    486581#l #E cases (ADDED l E) #l' * #L #P
    487582%{l'} % [ @L | @(present_included … P) @INC ]
    488583qed.
    489584
    490 lemma Cminor_labels_inv : ∀le,s,s',f.
    491   ∀f':Σf':partial_fn le. add_stmt_inv le s' f f'.
    492   Cminor_labels_added le s f →
    493   Cminor_labels_added le s f'.
    494 #le #s #s' #f * #f' * #H1 #H2 #H3
     585lemma Cminor_labels_inv : ∀le,env,s,s',f.
     586  ∀f':Σf':partial_fn le env. add_stmt_inv le env s' f f'.
     587  Cminor_labels_added le env s f →
     588  Cminor_labels_added le env s f'.
     589#le #env #s #s' #f * #f' * #H1 #H2 #H3
    495590#l #E cases (H3 l E) #l' * #L #P
    496591%{l'} % [ @L | @(present_included … P) @H1 ]
    497592qed.
    498593
    499 lemma Cminor_labels_sig : ∀le,s,f.
    500   ∀f':Σf':partial_fn le. fn_graph_included le f f'.
    501   Cminor_labels_added le s f →
    502   Cminor_labels_added le s f'.
    503 #le #s #f * #f' #H1 #H2
     594lemma Cminor_labels_sig : ∀le,env,s,f.
     595  ∀f':Σf':partial_fn le env. fn_contains … f f'.
     596  Cminor_labels_added s f →
     597  Cminor_labels_added s f'.
     598#le #env #s #f * #f' #H1 #H2
    504599#l #E cases (H2 l E) #l' * #L #P
    505600%{l'} % [ @L | @(present_included … P) @H1 ]
    506601qed.
    507602
    508 let 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') ≝
    509 match s return λs.stmt_inv env label_env s → res (Σf':partial_fn label_env. add_stmt_inv ? s f f') with
     603let rec add_stmt (env:env) (label_env:label_env) (s:stmt) (Env:stmt_inv env label_env s) (f:partial_fn label_env env) (exits:Σls:list label. All ? (present ?? (pf_graph … f)) ls) on s : res (Σf':partial_fn label_env env. add_stmt_inv label_env env s f f') ≝
     604match s return λs.stmt_inv env label_env s → res (Σf':partial_fn label_env env. add_stmt_inv … s f f') with
    510605[ St_skip ⇒ λ_. OK ? «f, ?»
    511 | St_assign _ x e ⇒ λEnv.
    512     let dst ≝ lookup_reg env x (π1 (π1 Env)) in
    513     OK ? «pi1 … (add_expr ? env ? e (π2 (π1 Env)) dst f), ?»
     606| St_assign t x e ⇒ λEnv.
     607    let dst ≝ lookup_reg env x t (π1 (π1 Env)) in
     608    OK ? «pi1 … (add_expr ? env ? e (π2 (π1 Env)) f dst), ?»
    514609| St_store _ _ q e1 e2 ⇒ λEnv.
    515     let 〈val_reg, f〉 ≝ choose_reg ? env ? e2 f (π2 (π1 Env)) in
    516     let 〈addr_reg, f〉 ≝ choose_reg ? env ? e1 f (π1 (π1 Env)) in
    517     let f ≝ add_fresh_to_graph ? (St_store q addr_reg val_reg) f ? in
    518     let f ≝ add_expr ? env ? e1 (π1 (π1 Env)) addr_reg f in
    519     OK ? «pi1 … (add_expr ? env ? e2 (π2 (π1 Env)) val_reg f), ?»
     610    let ❬f, val_reg❭ ≝ choose_reg … e2 f (π2 (π1 Env)) in
     611    let ❬f, addr_reg❭ ≝ choose_reg … e1 f (π1 (π1 Env)) in
     612    let f ≝ add_fresh_to_graph … (St_store q addr_reg val_reg) f ?? in
     613    let f ≝ add_expr ? env ? e1 (π1 (π1 Env)) f «addr_reg, ?» in
     614    OK ? «pi1 … (add_expr ? env ? e2 (π2 (π1 Env)) f «val_reg, ?»), ?»
    520615| St_call return_opt_id e args ⇒ λEnv.
    521616    let return_opt_reg ≝
    522617      match return_opt_id return λo. ? → ? with
    523618      [ None ⇒ λ_. None ?
    524       | Some id ⇒ λEnv. Some ? (lookup_reg env id ?)
     619      | Some idty ⇒ λEnv. Some ? (lookup_reg env (\fst idty) (\snd idty) ?)
    525620      ] Env in
    526     let 〈args_regs, f〉 as Eregs ≝ choose_regs ? env args f (π2 (π1 Env)) in
     621    let ❬f, args_regs❭ ≝ choose_regs ? env args f (π2 (π1 Env)) in
    527622    let f ≝
    528623      match expr_is_Id ? e with
    529       [ Some id ⇒ add_fresh_to_graph ? (St_call_id id args_regs return_opt_reg) f ?
     624      [ Some id ⇒ add_fresh_to_graph … (St_call_id id args_regs return_opt_reg) f ??
    530625      | None ⇒
    531         let 〈fnr, f〉 ≝ choose_reg ? env ? e f (π2 (π1 (π1 Env))) in
    532         let f ≝ add_fresh_to_graph ? (St_call_ptr fnr args_regs return_opt_reg) f ? in
    533         «pi1 … (add_expr ? env ? e (π2 (π1 (π1 Env))) fnr f), ?»
     626        let ❬f, fnr❭ ≝ choose_reg … e f (π2 (π1 (π1 Env))) in
     627        let f ≝ add_fresh_to_graph … (St_call_ptr fnr args_regs return_opt_reg) f ?? in
     628        «pi1 … (add_expr ? env ? e (π2 (π1 (π1 Env))) f «fnr, ?»), ?»
    534629      ] in
    535     OK ? «pi1 … (add_exprs ? env args (π2 (π1 Env)) args_regs ? f), ?»
     630    OK ? «pi1 … (add_exprs ? env args (π2 (π1 Env)) args_regs ? f ?), ?»
    536631| St_tailcall e args ⇒ λEnv.
    537     let 〈args_regs, f〉 as Eregs ≝ choose_regs ? env args f (π2 (π1 Env)) in
     632    let ❬f, args_regs❭ ≝ choose_regs ? env args f (π2 (π1 Env)) in
    538633    let f ≝
    539634      match expr_is_Id ? e with
    540       [ Some id ⇒ add_fresh_to_graph ? (λ_. St_tailcall_id id args_regs) f ?
     635      [ Some id ⇒ add_fresh_to_graph … (λ_. St_tailcall_id id args_regs) f ??
    541636      | None ⇒
    542         let 〈fnr, f〉 ≝ choose_reg ? env ? e f (π1 (π1 Env)) in
    543         let f ≝ add_fresh_to_graph ? (λ_. St_tailcall_ptr fnr args_regs) f ? in
    544         «pi1 … (add_expr ? env ? e (π1 (π1 Env)) fnr f), ?»
     637        let ❬f,fnr❭ ≝ choose_reg … e f (π1 (π1 Env)) in
     638        let f ≝ add_fresh_to_graph … (λ_. St_tailcall_ptr fnr args_regs) f ?? in
     639        «pi1 … (add_expr ? env ? e (π1 (π1 Env)) f «fnr, ?»), ?»
    545640      ] in
    546     OK ? «pi1 … (add_exprs ? env args (π2 (π1 Env)) args_regs ? f), ?»
     641    OK ? «pi1 … (add_exprs ? env args (π2 (π1 Env)) args_regs ? f ?), ?»
    547642| St_seq s1 s2 ⇒ λEnv.
    548643    do f2 ← add_stmt env label_env s2 ? f «exits, ?»;
     
    550645      OK ? «pi1 … f1, ?»
    551646| St_ifthenelse _ _ e s1 s2 ⇒ λEnv.
    552     let l_next ≝ pf_entry ? f in
     647    let l_next ≝ pf_entry f in
    553648    do f2 ← add_stmt env label_env s2 (π2 Env) f «exits, ?»;
    554     let l2 ≝ pf_entry ? f2 in
    555     let f ≝ add_fresh_to_graph ? (λ_. R_skip l_next) f2 ? in
     649    let l2 ≝ pf_entry f2 in
     650    let f ≝ add_fresh_to_graph … (λ_. R_skip l_next) f2 ?? in
    556651    do f1 ← add_stmt env label_env s1 (π2 (π1 Env)) f «exits, ?»;
    557     let 〈r,f〉 ≝ choose_reg ? env ? e f1 (π1 (π1 (π1 Env))) in
    558     let f ≝ add_fresh_to_graph ? (λl1. St_cond r l1 l2) f ? in
    559     OK ? «pi1 … (add_expr ? env ? e (π1 (π1 (π1 Env))) r f), ?»
     652    let ❬f,r❭ ≝ choose_reg … e f1 (π1 (π1 (π1 Env))) in
     653    let f ≝ add_fresh_to_graph … (λl1. St_cond r l1 l2) f ?? in
     654    OK ? «pi1 … (add_expr ? env ? e (π1 (π1 (π1 Env))) f «r, ?»), ?»
    560655| St_loop s ⇒ λEnv.
    561     let f ≝ add_fresh_to_graph ? R_skip f ? in (* dummy statement, fill in afterwards *)
    562     let l_loop ≝ pf_entry ? f in
     656    let f ≝ add_fresh_to_graph … R_skip f ?? in (* dummy statement, fill in afterwards *)
     657    let l_loop ≝ pf_entry f in
    563658    do f ← add_stmt env label_env s (π2 Env) f «exits, ?»;
    564     OK ? «pi1 … (fill_in_statement ? l_loop (R_skip (pf_entry ? f)) f ?), ?»
     659    OK ? «pi1 … (fill_in_statement … l_loop (R_skip (pf_entry … f)) f ??), ?»
    565660| St_block s ⇒ λEnv.
    566     do f ← add_stmt env label_env s (π2 Env) f («pf_entry ? f::exits, ?»);
     661    do f ← add_stmt env label_env s (π2 Env) f («pf_entry f::exits, ?»);
    567662    OK ? «pi1 … f, ?»
    568663| St_exit n ⇒ λEnv.
    569664    do l ← nth_sig ?? (msg BadCminorProgram) exits n;
    570     OK ? «pi1 … (add_fresh_to_graph ? (λ_. R_skip l) f ?), ?»
     665    OK ? «pi1 … (add_fresh_to_graph … (λ_. R_skip l) f ??), ?»
    571666| St_switch sz sg e tab n ⇒ λEnv.
    572     let 〈r,f〉 ≝ choose_reg ? env ? e f ? in
     667    let ❬f,r❭ ≝ choose_reg … e f ? in
    573668    do l_default ← nth_sig ?? (msg BadCminorProgram) exits n;
    574     let f ≝ add_fresh_to_graph ? (λ_. R_skip l_default) f ? in
    575     do f ← foldr ? (res (Σf':partial_fn ?. ?)) (λcs,f.
     669    let f ≝ add_fresh_to_graph … (λ_. R_skip l_default) f ?? in
     670    do f ← foldr ? (res (Σf':partial_fn ??. ?)) (λcs,f.
    576671      do f ← f;
    577672      let 〈i,n〉 ≝ cs in
    578       let 〈cr,f〉 ≝ fresh_reg … f (ASTint sz sg) in
    579       let 〈br,f〉 ≝ fresh_reg … f (ASTint I8 Unsigned) in
     673      let ❬f,cr❭ ≝ fresh_reg … f (ASTint sz sg) in
     674      let ❬f,br❭ ≝ fresh_reg … f (ASTint I8 Unsigned) in
    580675      do l_case ← nth_sig ?? (msg BadCminorProgram) exits n;
    581       let f ≝ add_fresh_to_graph ? (St_cond br l_case) f ? in
    582       let f ≝ add_fresh_to_graph ? (St_op2 (Ocmpu Ceq) (* signed? *) br r cr) f ? in
    583       let f ≝ add_fresh_to_graph ? (St_const cr (Ointconst ? i)) f ? in
     676      let f ≝ add_fresh_to_graph … (St_cond br l_case) f ?? in
     677      let f ≝ add_fresh_to_graph … (St_op2 (Ocmpu Ceq) (* signed? *) br r cr) f ?? in
     678      let f ≝ add_fresh_to_graph … (St_const cr (Ointconst ? i)) f ?? in
    584679        OK ? «pi1 … f, ?») (OK ? f) tab;
    585     OK ? «pi1 … (add_expr ? env ? e (π1 Env) r f), ?»
     680    OK ? «pi1 … (add_expr ? env ? e (π1 Env) f «r, ?»), ?»
    586681| St_return opt_e ⇒ let f0 ≝ f in
    587     let f ≝ add_fresh_to_graph ? (λ_. R_return) f ? in
    588     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
     682    let f ≝ add_fresh_to_graph … (λ_. R_return) f ?? in
     683    match opt_e return λo. stmt_inv ?? (St_return o) → res (Σf':partial_fn label_env env.add_stmt_inv … (St_return o) f0 f') with
    589684    [ None ⇒ λEnv. OK ? «pi1 … f, ?»
    590685    | Some e ⇒
    591         match pf_result ? f with
     686        match pf_result f with
    592687        [ None ⇒ λEnv. Error ? (msg ReturnMismatch)
    593688        | Some r ⇒
    594             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
    595             [ mk_DPair ty e ⇒ λEnv. let f ≝ add_expr label_env env ty e ? (\fst r) f in
    596                               OK ? «pi1 … f, ?» ]
     689            match e return λe.stmt_inv env label_env (St_return (Some ? e)) → res (Σf':partial_fn label_env env.add_stmt_inv … (St_return (Some ? e)) f0 f') with
     690            [ mk_DPair ty e ⇒ λEnv.
     691                match typ_eq (\snd r) ty with
     692                [ inl E ⇒ let f ≝ add_expr label_env env ty e ? f «\fst r, ? E (* XXX E goes missing if I don't use it! *)» in
     693                          OK ? «pi1 … f, ?»
     694                | inr _ ⇒ Error ? (msg ReturnMismatch)
     695                ]
     696            ]
    597697        ]
    598698    ]
     
    600700    do f ← add_stmt env label_env s' (π2 Env) f exits;
    601701    let l' ≝ lookup_label label_env l ? in
    602     OK ? «pi1 … (add_to_graph ? l' (R_skip (pf_entry ? f)) f ?), ?»
     702    OK ? «pi1 … (add_to_graph … l' (R_skip (pf_entry … f)) f ??), ?»
    603703| St_goto l ⇒ λEnv.
    604704    let l' ≝ lookup_label label_env l ? in
    605     OK ? «pi1 … (add_fresh_to_graph' ? (λ_.R_skip l') f ?), ?»
     705    OK ? «pi1 … (add_fresh_to_graph' … (λ_.R_skip l') f ??), ?»
    606706| St_cost l s' ⇒ λEnv.
    607707    do f ← add_stmt env label_env s' (π2 Env) f exits;
    608     OK ? «pi1 … (add_fresh_to_graph ? (St_cost l) f ?), ?»
     708    OK ? «pi1 … (add_fresh_to_graph … (St_cost l) f ??), ?»
    609709] Env.
    610710try @(π1 Env)
     
    613713try @(π2 (π1 Env))
    614714try @mk_add_stmt_inv
    615 try (repeat @fn_includes_step @I)
     715try (repeat @fn_contains_step @I)
    616716try (@empty_Cminor_labels_added @refl)
    617 try (@(All_mp … (pi2 ?? exits)))
    618717try (#l #H @I)
    619718try (#l #H @H)
    620 [ -f @(choose_regs_length … (sym_eq … Eregs))
    621 | whd in Env; @(π1 (π1 (π1 Env)))
    622 | -f @(choose_regs_length … (sym_eq … Eregs))
     719try (#l @I)
     720[ @(pf_envok … (π1 (π1 Env))) @refl
     721| @(fn_con_env … (pi2 ?? val_reg)) repeat @fn_contains_step @I
     722| @(fn_con_env … (pi2 ?? addr_reg)) repeat @fn_contains_step @I
     723| 4,8: @(All2_mp … (pi2 ?? args_regs)) #a * #b #c #H @(fn_con_env … H) repeat @fn_contains_step @I
     724| 5,9: @sym_eq @(All2_length … (pi2 ?? args_regs))
     725| 6,10: @(fn_con_env … (pi2 ?? fnr)) repeat @fn_contains_step @I
     726| @(π1 (π1 (π1 Env)))
     727| 11,13,14,19,20: (@(All_mp … (pi2 ?? exits))) #i #H @(fn_con_graph … H) repeat @fn_contains_step @I
    623728| #l #H cases (Exists_append … H)
    624   [ #H1 @(stmt_labels_added ???? (pi2 ?? f1) ? H1)
    625   | @(Cminor_labels_inc ?? f2 f1 ???) [ repeat @fn_includes_step @I | @(stmt_labels_added ???? (pi2 ?? f2)) ]
    626   ]
    627 | #l #H @(present_included … H) repeat @fn_includes_step @I
    628 | #l #H @(present_included … (pi2 ?? l_next)) repeat @fn_includes_step @I
     729  [ #H1 @(stmt_labels_added ????? (pi2 ?? f1) ? H1)
     730  | #H2 @(Cminor_labels_inv … H2) @(stmt_labels_added ????? (pi2 ?? f2))
     731  ]
     732| #l #H @(fn_con_graph … (pi2 ?? l_next)) repeat @fn_contains_step @I
    629733| #l #H cases (Exists_append … H)
    630   [ @(Cminor_labels_inc … (stmt_labels_added ???? (pi2 ?? f1))) repeat @fn_includes_step @I
    631   | @(Cminor_labels_inc … (stmt_labels_added ???? (pi2 ?? f2))) repeat @fn_includes_step @I
    632   ]
    633 | #l #H % [ @H | @(present_included … (pi2 ?? l2)) repeat @fn_includes_step @I ]
    634 | 9,10: #l #H @(present_included … H) repeat @fn_includes_step @I
    635 | @(pi2 ?? (pf_entry ??))
    636 | @Cminor_labels_sig @(equal_Cminor_labels_added ?? s) [ @refl | @(stmt_labels_added … (pi2 … f)) ]
     734  [ #H1 @(Cminor_labels_sig … H1) @Cminor_labels_sig @Cminor_labels_sig @(stmt_labels_added ????? (pi2 ?? f1))
     735  | #H2 @(Cminor_labels_sig … H2) @Cminor_labels_sig @Cminor_labels_sig @Cminor_labels_inv @Cminor_labels_sig @(stmt_labels_added ????? (pi2 ?? f2))
     736  ]
     737| @(fn_con_env … (pi2 ?? r)) repeat @fn_contains_step @I
     738| #l #H % [ @H | @(fn_con_graph … (pi2 ?? l2)) repeat @fn_contains_step @I ]
     739| @(pi2 … (pf_entry …))
     740| @Cminor_labels_sig @(equal_Cminor_labels_added ??? s) [ @refl | @(stmt_labels_added ????? (pi2 ?? f)) ]
    637741| % [ @pi2 | @(pi2 ?? exits) ]
    638 | @(equal_Cminor_labels_added ?? s) [ @refl | @(stmt_labels_added … (pi2 … f)) ]
    639 | #l' #H @(pi2 ?? l)
    640 | #l #H @(present_included … (pi2 ?? l_default)) repeat @fn_includes_step @I
    641 | #l #H % [ @(present_included … (pi2 ?? l_case)) repeat @fn_includes_step @I | @H ]
     742| @(equal_Cminor_labels_added ??? s) [ @refl | @(stmt_labels_added ????? (pi2 ?? f)) ]
     743| #l' #H @(pi2 … l)
     744| #l #H @(fn_con_graph … (pi2 ?? l_default)) repeat @fn_contains_step @I
     745| @(fn_con_env … (pi2 ?? r)) repeat @fn_contains_step @I
     746| #l #H % [ @(fn_con_graph … (pi2 ?? l_case)) repeat @fn_contains_step @I | @H ]
     747| #_ (* see above *) <E @(pi2 ?? r)
    642748| @(pi2 … (pf_entry …))
    643749| #l1 * [ #E >E %{l'} % [ @lookup_label_rev' | whd >lookup_add_hit % #E' destruct (E') ]
    644         |@Cminor_labels_sig @(stmt_labels_added … (pi2 … f))
     750        | @Cminor_labels_sig @(stmt_labels_added ????? (pi2 … f))
    645751        ]
    646752| #l1 #H whd %2 @lookup_label_lpresent
    647 | @(equal_Cminor_labels_added ?? s') [ @refl | @Cminor_labels_sig @(stmt_labels_added … (pi2 … f)) ]
    648 ] qed.
     753| @(equal_Cminor_labels_added ??? s') [ @refl | @Cminor_labels_sig @(stmt_labels_added ????? (pi2 … f)) ]
     754] qed.
     755
    649756
    650757definition c2ra_function (*: internal_function → internal_function*) ≝
     
    655762let 〈params, env1, reggen1〉 as E1 ≝ populate_env (empty_map …) reggen0 (f_params f) in
    656763let 〈locals0, env, reggen2〉 as E2 ≝ populate_env env1 reggen1 (f_vars f) in
    657 let 〈result, locals, reggen〉
    658   match f_return f with
    659   [ None ⇒ 〈None ?, locals0, reggen2〉
     764let ❬locals_reggen, result❭
     765  match f_return f return λ_.𝚺lr. option (Σrt. env_has ((\fst lr)@params) (\fst rt) (\snd rt)) with
     766  [ None ⇒ ❬〈locals0, reggen2〉, None ?❭
    660767  | Some ty ⇒
    661768      let 〈r,gen〉 ≝ fresh … reggen2 in
    662         〈Some ? 〈r,ty〉, 〈r,ty〉::locals0, gen〉 ] in
     769        mk_DPair ? (λlr.option (Σrt. env_has ((\fst lr)@params) (\fst rt) (\snd rt))) 〈〈r,ty〉::locals0, gen〉 (Some ? «〈r,ty〉, ?») ] in
     770let locals ≝ \fst locals_reggen in
     771let reggen ≝ \snd locals_reggen in
    663772let 〈label_env, labgen1〉 as El ≝ populate_label_env (empty_map …) labgen0 cminor_labels in
    664773let 〈l,labgen〉 ≝ fresh … labgen1 in
     
    666775  mk_partial_fn
    667776    label_env
     777    env
    668778    labgen
    669779    reggen
    670     result
    671780    params
    672781    locals
     782    result
     783    ?
    673784    (f_stacksize f)
    674785    (add ?? (empty_map …) l St_return)
     786    ?
    675787    ?
    676788    l
     
    678790do f ← add_stmt env label_env (f_body f) ? emptyfn [ ];
    679791OK ? (mk_internal_function
    680     (pf_labgen ? f)
    681     (pf_reggen ? f)
    682     (pf_result ? f)
    683     (pf_params ? f)
    684     (pf_locals ? f)
    685     (pf_stacksize ? f)
    686     (pf_graph ? f)
     792    (pf_labgen f)
     793    (pf_reggen f)
     794    (match pf_result … f with [ None ⇒ None ? | Some rt ⇒ Some ? (pi1 … rt) ])
     795    (pf_params f)
     796    (pf_locals f)
     797    (pf_stacksize f)
     798    (pf_graph f)
    687799    ?
    688     (pf_entry ? f)
    689     (pf_exit ? f)
     800    (pf_typed … f)
     801    (pf_entry … f)
     802    (pf_exit … f)
    690803  ).
    691804[ @I
     
    693806  #s * #V #L %
    694807  [ @(stmt_vars_mp … V)
    695     #i #H cases (Exists_append … H)
     808    #i #t #H cases (Exists_append … H)
     809    cases daemon (* XXX needs populates_env
    696810    [ #H1 @(populate_extends ?????? (sym_eq … E2))
    697811          @(populates_env … (sym_eq … E1)) @H1
    698812    | #H1 @(populates_env … (sym_eq … E2)) @H1
    699     ]
     813    ]*)
    700814  | @(stmt_labels_mp … L)
    701815    #l #H @(populates_label_env … (sym_eq … El)) @H
    702816  ]
    703 | #l #s #E @(labels_P_mp … (pf_closed ? f l s E))
     817| #l #s #E @(labels_P_mp … (pf_closed f l s E))
    704818  #l' * [ // | * #l #H cases f #f' * #L #P cases (P l ?)
    705819  [ #lx >H * #Ex >(?:lx = l') [ 2: destruct (Ex) @refl ]
     
    712826  ]
    713827  ]
     828| cases daemon (* XXX need information about env *)
    714829| #l1 #s #LOOKUP cases (lookup_add_cases ??????? LOOKUP)
    715830  [ * #E1 #E2 >E2 @I
    716831  | whd in ⊢ (??%? → ?); #E' destruct (E')
    717832  ]
    718 | *: whd >lookup_add_hit % #E destruct
     833| #l #s #LOOKUP cases (lookup_add_cases ??????? LOOKUP)
     834  [ * #E1 #E2 >E2 @I
     835  | whd in ⊢ (??%? → ?); #E' destruct (E')
     836  ]
     837| 7,8: whd >lookup_add_hit % #E destruct
     838| % @refl
    719839]
    720840qed.
Note: See TracChangeset for help on using the changeset viewer.