Changeset 2252 for src/Cminor


Ignore:
Timestamp:
Jul 24, 2012, 7:40:21 PM (7 years ago)
Author:
campbell
Message:

Use the return statement invariant. Restructure the invariants for Cminor
a bit to make them more understandable.

Location:
src/Cminor
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/initialisation.ma

    r2251 r2252  
    3838    ]
    3939].
    40 % /2/
     40% /3/
    4141cases init in p; [ 7: | 8: #a #b | *: #a ] #p normalize in p;
    42 destruct;/3/
     42destruct;/4 by stmt_labels_mp, conj/
    4343qed.
    4444
     
    5050     〈off + (size_init_data datum), St_seq (init_datum id r datum off) s〉)
    5151  〈0, mk_Sig ? (λx.stmt_inv x) St_skip ?〉 init).
    52 [ % /2/
     52[ % /3/
    5353| elim init
    54   [ % /2/
    55   | #h #t #IH whd in ⊢ (?(???%)); @breakup_pair whd in ⊢ (?%);
    56     % [ % [ % /2/ | @(pi2 … (init_datum …)) ] | @IH ]
     54  [ % /3/
     55  | #h #t #IH whd in ⊢ (?(???%)); @breakup_pair
     56    %
     57    [ /3/
     58    | % [ @(pi2 … (init_datum …)) | @IH ]
     59    ]
    5760] qed.
    5861
    5962definition init_vars : list (ident × region × (list init_data)) → Σs:stmt. stmt_inv s ≝
    6063λvars. foldr ? (Σs:stmt. stmt_inv s)
    61   (λvar,s. mk_Sig ? (λx.stmt_inv x ) (St_seq s (init_var (\fst (\fst var)) (\snd (\fst var)) (\snd var))) ?) (mk_Sig ? (λx.stmt_inv x ) St_skip (conj ?? (conj ?? I I) I)) vars.
    62 % [ % [ % /2/ | @(pi2 … s) ] | @(pi2 … (init_var …)) ]
    63 qed.
     64  (λvar,s. mk_Sig ? (λx.stmt_inv x ) (St_seq s (init_var (\fst (\fst var)) (\snd (\fst var)) (\snd var))) ?) (mk_Sig ? (λx.stmt_inv x ) St_skip ?) vars.
     65[ % [ /3/ | % [ @(pi2 … s) | @(pi2 … (init_var …)) ] ]
     66| /4/
     67] qed.
    6468
    6569lemma no_labels : ∀s. stmt_inv s → labels_of s = [ ].
    6670#s elim s //
    67 [ #s1 #s2 #IH1 #IH2 * * * * #_ #_ #_ #H1 #H2 whd in ⊢ (??%?);
     71[ #s1 #s2 #IH1 #IH2 * #_ * #H1 #H2 whd in ⊢ (??%?);
    6872  >(IH1 H1) >(IH2 H2) @refl
    69 | #sz #sg #e #s1 #s2 #IH1 #IH2 * * * #_ #_ #H1 #H2 whd in ⊢ (??%?);
     73| #sz #sg #e #s1 #s2 #IH1 #IH2 * #_ * #H1 #H2 whd in ⊢ (??%?);
    7074  >(IH1 H1) >(IH2 H2) @refl
    7175| #l #s #IH * * * #_ *
    72 | #l #s #IH * * #_ #_ #H @(IH H)
     76| #l #s #IH * #_ #H @(IH H)
    7377] qed.
    7478
     
    9599      | inr _ ⇒ 〈id',f'〉 ]) ].
    96100%
    97 [ % [ % // |
    98   @(stmt_P_mp … H) #s * * #V #L #R %
    99   [ @(stmt_vars_mp … V) #i #t *
    100   | @(stmt_labels_mp … L) #l *
    101   | cases s in R ⊢ %; // #x *
     101[ % //
     102| %
     103  [ @(stmt_P_mp … H) #s * * #V #L #R %
     104    [ @(stmt_vars_mp … V) #i #t *
     105    | @(stmt_labels_mp … L) #l *
     106    | cases s in R ⊢ %; // #x *
     107    ]
     108  | whd in match (labels_of ?); >(no_labels … H) @(f_inv f)
    102109  ]
    103   ]
    104 | whd in match (labels_of ?); >(no_labels … H) @(f_inv f)
    105110] qed.
    106111
  • src/Cminor/syntax.ma

    r2251 r2252  
    5151| St_cost : costlabel → stmt → stmt.
    5252
     53(* Apply a predicate to every statement.  Be careful with grouping so that the
     54   local application is the first conjunct, and substatements the second. *)
     55
    5356let rec stmt_P (P:stmt → Prop) (s:stmt) on s : Prop ≝
    5457match s with
    55 [ St_seq s1 s2 ⇒ P s ∧ stmt_P P s1 ∧ stmt_P P s2
    56 | St_ifthenelse _ _ _ s1 s2 ⇒ P s ∧ stmt_P P s1 ∧ stmt_P P s2
     58[ St_seq s1 s2 ⇒ P s ∧ (stmt_P P s1 ∧ stmt_P P s2)
     59| St_ifthenelse _ _ _ s1 s2 ⇒ P s ∧ (stmt_P P s1 ∧ stmt_P P s2)
    5760| St_label _ s' ⇒ P s ∧ stmt_P P s'
    5861| St_cost _ s' ⇒ P s ∧ stmt_P P s'
    59 | _ ⇒ P s
     62| _ ⇒ P s ∧ True
    6063].
    6164
    6265lemma stmt_P_P : ∀P,s. stmt_P P s → P s.
    63 #P * normalize /2/
    64 [ #s1 #s2 * * /2/
    65 | #sz #sg #e #s1 #s2 * * /2/
    66 | *: #i #s normalize * /2/
    67 ] qed.
     66#P * normalize * /3 by proj1/
     67qed.
    6868
    6969(* Assert a predicate on every variable or parameter identifier. *)
     
    9191
    9292lemma stmt_P_mp : ∀P,Q. (∀s. P s → Q s) → ∀s. stmt_P P s → stmt_P Q s.
    93 #P #Q #H #s elim s /2/
    94 [ #s1 #s2 #H1 #H2 normalize * * /4/
    95 | #sz #sg #e #s1 #s2 #H1 #H2 * * /5/
    96 | #l #s #H * /5/
    97 | #l #s #H * /5/
    98 ] qed.
     93#P #Q #H #s elim s /6 by proj1, proj2, conj/
     94qed.
    9995
    10096lemma stmt_vars_mp : ∀P,Q. (∀i,t. P i t → Q i t) → ∀s. stmt_vars P s → stmt_vars Q s.
  • src/Cminor/toRTLabs.ma

    r2251 r2252  
    192192 λe,g. forall_nodes ? (labels_P (λl. present ?? g l ∨ lpresent e l)) g.
    193193
     194(* Some data structures for the transformation that remain fixed throughout. *)
     195record fixed : Type[0] ≝ {
     196  fx_lenv   : label_env;
     197  fx_env    : env;
     198  fx_rettyp : option typ
     199}.
     200
     201definition resultok : option typ → list (register × typ) → Type[0] ≝
     202λty,env.
     203  match ty with [ Some t ⇒ Σr:register. env_has env r t | _ ⇒ True ].
     204
    194205(* I'd use a single parametrised definition along with internal_function, but
    195206   it's a pain without implicit parameters. *)
    196 record partial_fn (lenv:label_env) (env:env) : Type[0] ≝
     207record partial_fn (fx:fixed) : Type[0] ≝
    197208{ pf_labgen    : universe LabelTag
    198209; pf_reggen    : universe RegisterTag
    199210; pf_params    : list (register × typ)
    200211; pf_locals    : list (register × typ)
    201 ; pf_result    : option (Σrt:register × typ. env_has (pf_locals @ pf_params) (\fst rt) (\snd rt))
    202 ; pf_envok     : ∀id,ty,r,H. lookup_reg env id ty H = r → env_has (pf_locals @ pf_params) r ty
     212; pf_result    : resultok (fx_rettyp … fx) (pf_locals @ pf_params)
     213; pf_envok     : ∀id,ty,r,H. lookup_reg (fx_env … fx) id ty H = r → env_has (pf_locals @ pf_params) r ty
    203214; pf_stacksize : nat
    204215; pf_graph     : graph statement
    205 ; pf_closed    : partially_closed lenv pf_graph
     216; pf_closed    : partially_closed (fx_lenv … fx) pf_graph
    206217; pf_typed     : graph_typed (pf_locals @ pf_params) pf_graph
    207218; pf_entry     : Σl:label. present ?? pf_graph l
     
    210221
    211222definition fn_env_has ≝
    212   λle,env,f. env_has (pf_locals le env f @ pf_params le env f).
    213 
    214 record fn_contains (le:label_env) (env:env) (f1:partial_fn le env) (f2:partial_fn le env) : Prop ≝
     223  λfx,f. env_has (pf_locals fx f @ pf_params fx f).
     224
     225record fn_contains (fx:fixed) (f1:partial_fn fx) (f2:partial_fn fx) : Prop ≝
    215226{ fn_con_graph : graph_included (pf_graph … f1) (pf_graph … f2)
    216 ; fn_con_env : ∀r,ty. fn_env_has le env f1 r ty → fn_env_has le env f2 r ty
     227; fn_con_env : ∀r,ty. fn_env_has … f1 r ty → fn_env_has … f2 r ty
    217228}.
    218229
    219 lemma fn_con_trans : ∀le,env,f1,f2,f3.
    220   fn_contains le env f1 f2 → fn_contains le env f2 f3 → fn_contains le env f1 f3.
    221 #le #env #f1 #f2 #f3 #H1 #H2 %
     230lemma fn_con_trans : ∀fx,f1,f2,f3.
     231  fn_contains fx f1 f2 → fn_contains … f2 f3 → fn_contains … f1 f3.
     232#fx #f1 #f2 #f3 #H1 #H2 %
    222233[ @(graph_inc_trans … (fn_con_graph … H1) (fn_con_graph … H2))
    223234| #r #ty #H @(fn_con_env … H2) @(fn_con_env … H1) @H
    224235] qed.
    225236
    226 lemma fn_con_refl : ∀label_env,env,f.
    227   fn_contains label_env env f f.
    228 #le #env #f % #l // qed.
    229 
    230 lemma fn_con_sig : ∀label_env,env,f,f0.
    231   ∀f':Σf':partial_fn label_env env. fn_contains … f0 f'.
    232   fn_contains label_env env f f0 →
    233   fn_contains label_env env f f'.
    234 #le #env #f #f0 * #f' #H1 #H2 @(fn_con_trans … H2 H1)
    235 qed.
    236 
    237 lemma add_statement_inv : ∀le,env,l,s.∀f.
    238   labels_present (pf_graph le env f) s →
    239   partially_closed le (add … (pf_graph … f) l s).
    240 #le #env #l #s #f #p
     237lemma fn_con_refl : ∀fx,f.
     238  fn_contains fx f f.
     239#fx #f % #l // qed.
     240
     241lemma fn_con_sig : ∀fx,f,f0.
     242  ∀f':Σf':partial_fn fx. fn_contains … f0 f'.
     243  fn_contains fx f f0 →
     244  fn_contains fx f f'.
     245#fx #f #f0 * #f' #H1 #H2 @(fn_con_trans … H2 H1)
     246qed.
     247
     248lemma add_statement_inv : ∀fx,l,s.∀f.
     249  labels_present (pf_graph fx f) s →
     250  partially_closed (fx_lenv … fx) (add … (pf_graph … f) l s).
     251#fx #l #s #f #p
    241252#l' #s' #H cases (identifier_eq … l l')
    242253[ #E >E in H; >lookup_add_hit #E' <(?:s = s') [2:destruct //]
     
    249260
    250261definition statement_typed_in ≝
    251 λle,env,f,s. statement_typed (pf_locals le env f @ pf_params le env f) s.
     262λfx,f,s. statement_typed (pf_locals fx f @ pf_params fx f) s.
    252263
    253264lemma forall_nodes_add : ∀A,P,l,a,g.
     
    261272
    262273(* Add a statement to the graph, *without* updating the entry label. *)
    263 definition fill_in_statement : ∀le,env. label → ∀s:statement. ∀f:partial_fn le env.
     274definition fill_in_statement : ∀fx. label → ∀s:statement. ∀f:partial_fn fx.
    264275  labels_present (pf_graph … f) s →
    265   statement_typed_in le env f s →
    266   Σf':partial_fn le env. fn_contains … f f' ≝
    267 λle,env,l,s,f,p,tp.
    268   mk_partial_fn le env (pf_labgen … f) (pf_reggen … f)
     276  statement_typed_in f s →
     277  Σf':partial_fn fx. fn_contains … f f' ≝
     278λfx,l,s,f,p,tp.
     279  mk_partial_fn fx (pf_labgen … f) (pf_reggen … f)
    269280                (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
    270281                (pf_stacksize … f) (add ?? (pf_graph … f) l s) ? ?
     
    277288
    278289(* Add a statement to the graph, making it the entry label. *)
    279 definition add_to_graph : ∀le,env. label → ∀s:statement. ∀f:partial_fn le env.
     290definition add_to_graph : ∀fx. label → ∀s:statement. ∀f:partial_fn fx.
    280291  labels_present (pf_graph … f) s →
    281292  statement_typed_in … f s →
    282   Σf':partial_fn le env. fn_contains … f f' ≝
    283 λle,env,l,s,f,p,tl.
    284   mk_partial_fn le env (pf_labgen … f) (pf_reggen … f)
     293  Σf':partial_fn fx. fn_contains … f f' ≝
     294λfx,l,s,f,p,tl.
     295  mk_partial_fn fx (pf_labgen … f) (pf_reggen … f)
    285296                (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
    286297                (pf_stacksize … f) (add ?? (pf_graph … f) l s) ? ?
     
    295306(* Add a statement with a fresh label to the start of the function.  The
    296307   statement is parametrised by the *next* instruction's label. *)
    297 definition add_fresh_to_graph : ∀le,env. ∀s:(label → statement). ∀f:partial_fn le env.
     308definition add_fresh_to_graph : ∀fx. ∀s:(label → statement). ∀f:partial_fn fx.
    298309  (∀l. present ?? (pf_graph … f) l → labels_present (pf_graph … f) (s l)) →
    299310  (∀l. statement_typed_in … f (s l)) →
    300   Σf':partial_fn le env. fn_contains … f f' ≝
    301 λle,env,s,f,p,tp.
     311  Σf':partial_fn fx. fn_contains … f f' ≝
     312λfx,s,f,p,tp.
    302313  let 〈l,g〉 ≝ fresh … (pf_labgen … f) in
    303314  let s' ≝ s (pf_entry … f) in
    304     (mk_partial_fn le env g (pf_reggen … f)
     315    (mk_partial_fn fx g (pf_reggen … f)
    305316                   (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
    306317                   (pf_stacksize … f) (add ?? (pf_graph … f) l s') ? ?
     
    315326(* Variants for labels which are (goto) labels *)
    316327
    317 lemma add_statement_inv' : ∀le,env,l,s.∀f.
    318   labels_P (λl. present ?? (pf_graph le env f) l ∨ lpresent le l) s →
    319   partially_closed le (add … (pf_graph … f) l s).
    320 #le #env #l #s #f #p
     328lemma add_statement_inv' : ∀fx,l,s.∀f.
     329  labels_P (λl. present ?? (pf_graph fx f) l ∨ lpresent (fx_lenv … fx) l) s →
     330  partially_closed (fx_lenv … fx) (add … (pf_graph … f) l s).
     331#fx #l #s #f #p
    321332#l' #s' #H cases (identifier_eq … l l')
    322333[ #E >E in H; >lookup_add_hit #E' <(?:s = s') [2:destruct //]
     
    328339] qed.
    329340
    330 definition add_fresh_to_graph' : ∀le,env. ∀s:(label → statement). ∀f:partial_fn le env.
    331   (∀l. present ?? (pf_graph … f) l → labels_P (λl.present ?? (pf_graph … f) l ∨ lpresent le l) (s l)) →
     341definition add_fresh_to_graph' : ∀fx. ∀s:(label → statement). ∀f:partial_fn fx.
     342  (∀l. present ?? (pf_graph … f) l → labels_P (λl.present ?? (pf_graph … f) l ∨ lpresent (fx_lenv … fx) l) (s l)) →
    332343  (∀l. statement_typed_in … f (s l)) →
    333   Σf':partial_fn le env. fn_contains … f f' ≝
    334 λle,env,s,f,p,tp.
     344  Σf':partial_fn fx. fn_contains … f f' ≝
     345λfx,s,f,p,tp.
    335346  let 〈l,g〉 ≝ fresh … (pf_labgen … f) in
    336347  let s' ≝ s (pf_entry … f) in
    337     (mk_partial_fn le env g (pf_reggen … f)
     348    (mk_partial_fn fx g (pf_reggen … f)
    338349                   (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
    339350                   (pf_stacksize … f) (add ?? (pf_graph … f) l s') ? ?
     
    362373(* A little more nesting in the result type than I'd like, but it keeps the
    363374   function closely paired with the proof that it contains f. *)
    364 definition fresh_reg : ∀le,env. ∀f:partial_fn le env. ∀ty:typ.
    365   𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σr:register. fn_env_has le env f' r ty) ≝
    366 λle,env,f,ty.
     375definition fresh_reg : ∀fx. ∀f:partial_fn fx. ∀ty:typ.
     376  𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σr:register. fn_env_has … f' r ty) ≝
     377λfx,f,ty.
    367378  let 〈r,g〉 ≝ fresh … (pf_reggen … f) in
    368379  let f' ≝
    369     «mk_partial_fn le env
    370        (pf_labgen … f) g (pf_params … f) (〈r,ty〉::(pf_locals … f))
    371        (match pf_result … f with [ None ⇒ None ? | Some rt ⇒ Some ? «pi1 … rt, ?»]) ?
     380    «mk_partial_fn fx
     381       (pf_labgen … f) g (pf_params … f) (〈r,ty〉::(pf_locals … f)) ? ?
    372382       (pf_stacksize … f) (pf_graph … f) (pf_closed … f) ? (pf_entry … f) (pf_exit … f), ?»
    373383  in
     
    376386| #l #s #L @stmt_extend_typ_env @(pf_typed … L)
    377387| #i #t #r1 #H #L %2 @(pf_envok … f … L)
    378 | %2 @(pi2 … rt)
     388| lapply (pf_result fx f) cases (fx_rettyp fx) // #t * #r' #H %{r'} @extend_typ_env //
    379389| % [ #l // | #r' #ty' #H @extend_typ_env @H ]
    380390] qed.
     
    382392axiom UnknownVariable : String.
    383393
    384 definition choose_reg : ∀le. ∀env:env.∀ty.∀e:expr ty. ∀f:partial_fn le env. expr_vars ty e (Env_has env) →
    385   𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σr:register. fn_env_has le env f' r ty) ≝
    386 λle,env,ty,e,f.
    387   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
    388   [ Id t i ⇒ λEnv. ❬«f, ?», «lookup_reg env i t Env, ?»❭
    389   | _ ⇒ λ_.fresh_reg le env f ?
     394definition choose_reg : ∀fx.∀ty.∀e:expr ty. ∀f:partial_fn fx. expr_vars ty e (Env_has (fx_env fx)) →
     395  𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σr:register. fn_env_has … f' r ty) ≝
     396λfx,ty,e,f.
     397  match e return λty,e. expr_vars ty e (Env_has (fx_env fx)) → 𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σr:register. fn_env_has … f' r ty) with
     398  [ Id t i ⇒ λEnv. ❬«f, ?», «lookup_reg (fx_env fx) i t Env, ?»❭
     399  | _ ⇒ λ_.fresh_reg f ?
    390400  ].
    391401[ % //
     
    404414λA,P,x. match x with [ mk_DPair a _ ⇒ a].
    405415
    406 definition choose_regs : ∀le. ∀env:env. ∀es:list (𝚺t:typ.expr t).
    407                          ∀f:partial_fn le env. All ? (exprtyp_present env) es →
    408                          𝚺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) ≝
    409 λle,env,es,f,Env.
    410   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))
     416definition choose_regs : ∀fx. ∀es:list (𝚺t:typ.expr t).
     417                         ∀f:partial_fn fx. All ? (exprtyp_present (fx_env fx)) es →
     418                         𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has … f' r (eject' typ expr e)) rs es) ≝
     419λfx,es,f,Env.
     420  foldr_all' (𝚺t:typ.expr t) ? (λes. 𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has … f' r (eject' typ expr e)) rs es))
    411421    (λe,p,tl,acc.
    412       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 ⇒
    413         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.
    414           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 ⇒
     422      match acc return λ_.𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has … f' r (eject' typ expr e)) rs (e::tl)) with [ mk_DPair f1 rs ⇒
     423        match e return λe.exprtyp_present (fx_env fx) e → 𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has … f' r (eject' typ expr e)) rs (e::tl)) with [ mk_DPair t e ⇒ λp.
     424          match choose_reg fx t e (pi1 … f1) ? return λ_.𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has … f' r (eject' typ expr e)) rs (❬t,e❭::tl)) with [ mk_DPair f' r ⇒
    415425            ❬«pi1 … f', ?»,«(pi1 … r)::(pi1 … rs), ?»❭
    416426          ]
     
    419429[ @p
    420430| cases r #r' #Hr' cases rs #rs' #Hrs'
    421   % [ whd in ⊢ (???%%%); @Hr' | @(All2_mp … Hrs') #r1 * #t1 #e1 #H1 @(fn_con_env … f1) [ @(pi2 … f') | @H1 ] ]
     431  % [ whd in ⊢ (??%%%); @Hr' | @(All2_mp … Hrs') #r1 * #t1 #e1 #H1 @(fn_con_env … f1) [ @(pi2 … f') | @H1 ] ]
    422432| @fn_con_trans [ 3: @(pi2 … f') | skip | @(pi2 … f1) ]
    423433| @fn_con_refl
     
    430440
    431441
    432 lemma choose_regs_length : ∀le,env,es,f,p,f',rs.
    433   choose_regs le env es f p = ❬f',rs❭ → |es| = length … rs.
    434 #le #env #es #f #p #f' * #rs #H #_ @sym_eq @(All2_length … H)
    435 qed.
    436 
    437 lemma present_included : ∀le,env,f,f',l.
    438   fn_contains le env f f' →
     442lemma choose_regs_length : ∀fx,es,f,p,f',rs.
     443  choose_regs fx es f p = ❬f',rs❭ → |es| = length … rs.
     444#fx #es #f #p #f' * #rs #H #_ @sym_eq @(All2_length … H)
     445qed.
     446
     447lemma present_included : ∀fx,f,f',l.
     448  fn_contains fx f f' →
    439449  present ?? (pf_graph … f) l →
    440450  present ?? (pf_graph … f') l.
    441 #le #env #f #f' #l * #H1 #H2 @H1 qed.
     451#fx #f #f' #l * #H1 #H2 @H1 qed.
    442452
    443453(* Some definitions for the add_stmt function later, which we introduce now so
     
    446456(* We need to show that the graph only grows, and that Cminor labels will end
    447457   up in the graph. *)
    448 definition Cminor_labels_added ≝ λle,env,s,f'.
     458definition Cminor_labels_added ≝ λfx,s,f'.
    449459∀l. Exists ? (λl'.l=l') (labels_of s) →
    450 ∃l'. lookup ?? le l = Some ? l' ∧ present ?? (pf_graph le env f') l'.
    451 
    452 record add_stmt_inv (le:label_env) (env:env) (s:stmt) (f:partial_fn le env) (f':partial_fn le env) : Prop ≝
     460∃l'. lookup ?? (fx_lenv fx) l = Some ? l' ∧ present ?? (pf_graph fx f') l'.
     461
     462record add_stmt_inv (fx:fixed) (s:stmt) (f:partial_fn fx) (f':partial_fn fx) : Prop ≝
    453463{ stmt_graph_con : fn_contains … f f'
    454464; stmt_labels_added : Cminor_labels_added … s f'
     
    458468
    459469(* A datatype saying how we intend to prove a step. *)
    460 inductive fn_con_because (le:label_env) (env:env) : partial_fn le env → Type[0] ≝
    461 | fn_con_eq : ∀f. fn_con_because le env f
    462 | fn_con_sig : ∀f1,f2:partial_fn le env. fn_contains … f1 f2 →
    463     ∀f3:(Σf3:partial_fn le env.fn_contains … f2 f3). fn_con_because le env f3
    464 | fn_con_addinv : ∀f1,f2:partial_fn le env. fn_contains … f1 f2 →
    465     ∀s.∀f3:(Σf3:partial_fn le env.add_stmt_inv … s f2 f3). fn_con_because le env f3
     470inductive fn_con_because (fx:fixed) : partial_fn fx → Type[0] ≝
     471| fn_con_eq : ∀f. fn_con_because fx f
     472| fn_con_sig : ∀f1,f2:partial_fn fx. fn_contains … f1 f2 →
     473    ∀f3:(Σf3:partial_fn fx.fn_contains … f2 f3). fn_con_because fx f3
     474| fn_con_addinv : ∀f1,f2:partial_fn fx. fn_contains … f1 f2 →
     475    ∀s.∀f3:(Σf3:partial_fn fx.add_stmt_inv … s f2 f3). fn_con_because fx f3
    466476.
    467477
    468478(* Extract the starting function for a step. *)
    469 let rec fn_con_because_left le env f0  (b:fn_con_because ?? f0) on b : partial_fn le env
     479let rec fn_con_because_left fx f0  (b:fn_con_because ? f0) on b : partial_fn fx
    470480  match b with [ fn_con_eq f ⇒ f | fn_con_sig f _ _ _ ⇒ f | fn_con_addinv f _ _ _ _ ⇒ f ].
    471481
     
    475485   have reached the desired starting point. *)
    476486
    477 unification hint 0 ≔ le:label_env, env:env, f:partial_fn le env, dummy:True;
     487unification hint 0 ≔ fx:fixed, f:partial_fn fx, dummy:True;
    478488  f' ≟ f,
    479   b  ≟ fn_con_eq le env f
     489  b  ≟ fn_con_eq fx f
    480490
    481   fn_contains le env f f' ≡ fn_contains le env (fn_con_because_left le env f' b) f'
     491  fn_contains fx f f' ≡ fn_contains fx (fn_con_because_left fx f' b) f'
    482492.
    483493
    484 unification 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);
    485   b ≟ fn_con_sig le env f1 f2 H12 f3
     494unification hint 1 ≔ fx:fixed, f1:partial_fn fx, f2:partial_fn fx, H12 : fn_contains fx f1 f2, f3:(Σf3:partial_fn fx. fn_contains fx f2 f3);
     495  b ≟ fn_con_sig fx f1 f2 H12 f3
    486496
    487   fn_contains le env f1 f3 ≡ fn_contains le env (fn_con_because_left le env f3 b) f3
     497  fn_contains fx f1 f3 ≡ fn_contains fx (fn_con_because_left fx f3 b) f3
    488498.
    489499
    490 unification 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);
    491   b ≟ fn_con_addinv le env f1 f2 H12 s f3
     500unification hint 1 ≔ fx:fixed, f1:partial_fn fx, f2:partial_fn fx, H12 : fn_contains fx f1 f2, s:stmt, f3:(Σf3:partial_fn fx. add_stmt_inv fx s f2 f3);
     501  b ≟ fn_con_addinv fx f1 f2 H12 s f3
    492502
    493   fn_contains le env f1 f3 ≡ fn_contains le env (fn_con_because_left le env f3 b) f3
     503  fn_contains fx f1 f3 ≡ fn_contains fx (fn_con_because_left fx f3 b) f3
    494504.
    495505
    496506(* A lemma to perform a step of the proof.  We can repeat this to do the whole
    497507   proof. *) 
    498 lemma fn_contains_step : ∀le,env,f. ∀b:fn_con_because le env f. fn_contains … (fn_con_because_left … f b) f.
    499 #le #env #f *
     508lemma fn_contains_step : ∀fx,f. ∀b:fn_con_because fx f. fn_contains … (fn_con_because_left … f b) f.
     509#fx #f *
    500510[ #f @fn_con_refl
    501511| #f1 #f2 #H12 * #f3 #H23 @(fn_con_trans … H12 H23)
     
    505515axiom BadCminorProgram : String.
    506516
    507 let rec add_expr (le:label_env) (env:env) (ty:typ) (e:expr ty)
    508   (Env:expr_vars ty e (Env_has env)) (f:partial_fn le env)
     517let rec add_expr (fx:fixed) (ty:typ) (e:expr ty)
     518  (Env:expr_vars ty e (Env_has (fx_env fx))) (f:partial_fn fx)
    509519  (dst:Σdst. fn_env_has … f dst ty)
    510   on e: Σf':partial_fn le env. fn_contains … f f' ≝
    511 match 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
     520  on e: Σf':partial_fn fx. fn_contains … f f' ≝
     521match e return λty,e.expr_vars ty e (Env_has ?) → (Σdst. fn_env_has … f dst ty) → Σf':partial_fn fx. fn_contains … f f' with
    512522[ Id t i ⇒ λEnv,dst.
    513     let r ≝ lookup_reg env i t Env in
     523    let r ≝ lookup_reg (fx_env fx) i t Env in
    514524    match register_eq r dst with
    515525    [ inl _ ⇒ «f, ?»
     
    520530    let ❬f,r❭ ≝ choose_reg … e' f Env in
    521531    let f ≝ add_fresh_to_graph … (St_op1 t' t op dst r) f ?? in
    522     let f ≝ add_expr … env ? e' Env f «r, ?» in
     532    let f ≝ add_expr … ? e' Env f «r, ?» in
    523533      «pi1 … f, ?»
    524534| Op2 _ _ _ op e1 e2 ⇒ λEnv,dst.
     
    526536    let ❬f,r2❭ ≝ choose_reg … e2 f (proj2 … Env) in
    527537    let f ≝ add_fresh_to_graph … (St_op2 ??? op dst r1 r2) f ?? in
    528     let f ≝ add_expr … env ? e2 (proj2 … Env) f «r2, ?» in
    529     let f ≝ add_expr … env ? e1 (proj1 … Env) f «r1, ?» in
     538    let f ≝ add_expr … ? e2 (proj2 … Env) f «r2, ?» in
     539    let f ≝ add_expr … ? e1 (proj1 … Env) f «r1, ?» in
    530540      «pi1 … f, ?»
    531541| Mem t e' ⇒ λEnv,dst.
    532542    let ❬f,r❭ ≝ choose_reg … e' f Env in
    533543    let f ≝ add_fresh_to_graph … (St_load t r dst) f ?? in
    534     let f ≝ add_expr … env ? e' Env f «r,?» in
     544    let f ≝ add_expr … ? e' Env f «r,?» in
    535545      «pi1 … f, ?»
    536546| Cond _ _ _ e' e1 e2 ⇒ λEnv,dst.
    537547    let resume_at ≝ pf_entry … f in
    538     let f ≝ add_expr … env ? e2 (proj2 … Env) f dst in
     548    let f ≝ add_expr … ? e2 (proj2 … Env) f dst in
    539549    let lfalse ≝ pf_entry … f in
    540550    let f ≝ add_fresh_to_graph … (λ_.St_skip resume_at) f ?? in
    541     let f ≝ add_expr … env ? e1 (proj2 … (proj1 … Env)) f «dst, ?» in
     551    let f ≝ add_expr … ? e1 (proj2 … (proj1 … Env)) f «dst, ?» in
    542552    let ❬f,r❭ ≝ choose_reg … e' f ? in
    543553    let f ≝ add_fresh_to_graph … (λltrue. St_cond r ltrue lfalse) f ?? in
    544     let f ≝ add_expr … env ? e' (proj1 … (proj1 … Env)) f «r, ?» in
     554    let f ≝ add_expr … ? e' (proj1 … (proj1 … Env)) f «r, ?» in
    545555      «pi1 … f, ?»
    546556| Ecost _ l e' ⇒ λEnv,dst.
    547     let f ≝ add_expr … env ? e' Env f dst in
     557    let f ≝ add_expr … ? e' Env f dst in
    548558    let f ≝ add_fresh_to_graph … (St_cost l) f ?? in
    549559      «f, ?»
     
    560570| @(fn_con_env … (pi2 ?? r1)) repeat @fn_contains_step @I
    561571| @(fn_con_env … (pi2 ?? r2)) repeat @fn_contains_step @I
    562 | #l % [ % [ @(fn_con_env ??????? (pi2 ?? r1)) | @(pi2 ?? r2) ] | @(fn_con_env … (pi2 ?? dst)) ] repeat @fn_contains_step @I
     572| #l % [ % [ @(fn_con_env (pi2 ?? r1)) | @(pi2 ?? r2) ] | @(fn_con_env … (pi2 ?? dst)) ] repeat @fn_contains_step @I
    563573| #l #H whd % [ @H | @(fn_con_graph … (pi2 ?? lfalse)) repeat @fn_contains_step @I ]
    564574| @(π1 (π1 Env))
     
    567577] qed.
    568578
    569 let rec add_exprs (le:label_env) (env:env) (es:list (𝚺t:typ.expr t)) (Env:All ? (exprtyp_present env) es)
    570                   (dsts:list register) (pf:length … es = length … dsts) (f:partial_fn le env)
    571                   (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' ≝
     579let rec add_exprs (fx:fixed) (es:list (𝚺t:typ.expr t)) (Env:All ? (exprtyp_present (fx_env fx)) es)
     580                  (dsts:list register) (pf:length … es = length … dsts) (f:partial_fn fx)
     581                  (Hdsts:All2 ?? (λr,e. fn_env_has … f r (eject' typ expr e)) dsts es) on es: Σf':partial_fn fx. fn_contains … f f' ≝
    572582match es return λes.All ?? es → All2 ???? es → |es|=|dsts| → ? with
    573 [ nil ⇒ λ_.λ_. match dsts return λx. ?=|x| → Σf':partial_fn le env. fn_contains le env f f' with [ nil ⇒ λ_. «f, ?» | cons _ _ ⇒ λpf.⊥ ]
     583[ nil ⇒ λ_.λ_. match dsts return λx. ?=|x| → Σf':partial_fn fx. fn_contains … f f' with [ nil ⇒ λ_. «f, ?» | cons _ _ ⇒ λpf.⊥ ]
    574584| cons e et ⇒ λEnv.
    575     match dsts return λx. All2 ?? (λr,e. fn_env_has le env f r (eject' typ expr e)) x (e::et) → ?=|x| → ? with
     585    match dsts return λx. All2 ?? (λr,e. fn_env_has f r (eject' typ expr e)) x (e::et) → ?=|x| → ? with
    576586    [ nil ⇒ λ_.λpf.⊥
    577587    | cons r rt ⇒ λHdsts,pf.
    578         let f' ≝ add_exprs ? env et ? rt ? f ? in
    579         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.
    580           let f'' ≝ add_expr ? env ty e ? f' r in
     588        let f' ≝ add_exprs et ? rt ? f ? in
     589        match e return λe.exprtyp_present ? e → fn_env_has f r (eject' typ expr e) → ? with [ mk_DPair ty e ⇒ λEnv,Hr.
     590          let f'' ≝ add_expr ty e ? f' r in
    581591            «pi1 … f'', ?»
    582592        ] (proj1 ?? Env) (π1 Hdsts)
     
    595605axiom ReturnMismatch : String.
    596606
    597 definition stmt_inv : env → label_env → stmt → Prop ≝
    598 λenv,lenv. stmt_P (λs. stmt_vars (Env_has env) s ∧ stmt_labels (present ?? lenv) s).
     607definition return_ok ≝
     608λt,s. match s with [ St_return oe ⇒ rettyp_match t oe | _ ⇒ True ].
     609
     610record stmt_inv (fx:fixed) (s:stmt) : Prop ≝ {
     611  si_vars : stmt_vars (Env_has (fx_env fx)) s;
     612  si_labels : stmt_labels (present ?? (fx_lenv fx)) s;
     613  si_return : return_ok (fx_rettyp fx) s
     614}.
     615
     616definition stmts_inv : fixed → stmt → Prop ≝
     617λfx. stmt_P (stmt_inv fx).
    599618
    600619(* Trick to avoid multiplying the proof obligations for the non-Id cases. *)
     
    631650qed.
    632651
    633 lemma empty_Cminor_labels_added : ∀le,env,s,f'.
    634   labels_of s = [ ] → Cminor_labels_added le env s f'.
    635 #le #env #s #f' #E whd >E #l *;
    636 qed.
    637 
    638 lemma equal_Cminor_labels_added : ∀le,env,s,s',f.
     652lemma empty_Cminor_labels_added : ∀fx,s,f'.
     653  labels_of s = [ ] → Cminor_labels_added fx s f'.
     654#fx #s #f' #E whd >E #l *;
     655qed.
     656
     657lemma equal_Cminor_labels_added : ∀fx,s,s',f.
    639658  labels_of s = labels_of s' → Cminor_labels_added … s' f →
    640   Cminor_labels_added le env s f.
    641 #le #env #s #s' #f #E whd in ⊢ (% → %); > E #H @H
    642 qed.
    643 
    644 lemma Cminor_labels_con : ∀le,env,s,f,f'.
    645   fn_contains le env f f' →
     659  Cminor_labels_added fx s f.
     660#fx #s #s' #f #E whd in ⊢ (% → %); > E #H @H
     661qed.
     662
     663lemma Cminor_labels_con : ∀fx,s,f,f'.
     664  fn_contains fx f f' →
    646665  Cminor_labels_added … s f →
    647666  Cminor_labels_added … s f'.
    648 #le #env #s #f #f' #INC #ADDED
     667#fx #s #f #f' #INC #ADDED
    649668#l #E cases (ADDED l E) #l' * #L #P
    650669%{l'} % [ @L | @(present_included … P) @INC ]
    651670qed.
    652671
    653 lemma Cminor_labels_inv : ∀le,env,s,s',f.
    654   ∀f':Σf':partial_fn le env. add_stmt_inv le env s' f f'.
    655   Cminor_labels_added le env s f →
    656   Cminor_labels_added le env s f'.
    657 #le #env #s #s' #f * #f' * #H1 #H2 #H3
     672lemma Cminor_labels_inv : ∀fx,s,s',f.
     673  ∀f':Σf':partial_fn fx. add_stmt_inv fx s' f f'.
     674  Cminor_labels_added fx s f →
     675  Cminor_labels_added fx s f'.
     676#fx #s #s' #f * #f' * #H1 #H2 #H3
    658677#l #E cases (H3 l E) #l' * #L #P
    659678%{l'} % [ @L | @(present_included … P) @H1 ]
    660679qed.
    661680
    662 lemma Cminor_labels_sig : ∀le,env,s,f.
    663   ∀f':Σf':partial_fn le env. fn_contains … f f'.
     681lemma Cminor_labels_sig : ∀fx,s,f.
     682  ∀f':Σf':partial_fn fx. fn_contains … f f'.
    664683  Cminor_labels_added … s f →
    665684  Cminor_labels_added … s f'.
    666 #le #env #s #f * #f' #H1 #H2
     685#fx #s #f * #f' #H1 #H2
    667686#l #E cases (H2 l E) #l' * #L #P
    668687%{l'} % [ @L | @(present_included … P) @H1 ]
    669688qed.
    670689
    671 let rec add_stmt (env:env) (label_env:label_env) (s:stmt) (Env:stmt_inv env label_env s) (f:partial_fn label_env env) on s : res (Σf':partial_fn label_env env. add_stmt_inv label_env env s f f') ≝
    672 match s return λs.stmt_inv env label_env s → res (Σf':partial_fn label_env env. add_stmt_inv … s f f') with
     690discriminator option.
     691discriminator DPair.
     692
     693(* Return statements need a little careful treatment to avoid errors using the
     694   invariant about the return type. *)
     695
     696definition add_return : ∀fx,opt_e. ∀f:partial_fn fx. ∀Env:stmts_inv fx (St_return opt_e).
     697  Σf':partial_fn fx. add_stmt_inv fx (St_return opt_e) f f' ≝
     698λfx,opt_e,f.
     699  let f0 ≝ f in
     700  let f ≝ add_fresh_to_graph … (λ_. R_return) f ?? in
     701  match opt_e return λo. stmts_inv ? (St_return o) → Σf':partial_fn fx.add_stmt_inv … (St_return o) f0 f' with
     702  [ None ⇒ λEnv. «pi1 … f, ?»
     703  | Some et ⇒
     704    match et return λe.stmts_inv fx (St_return (Some ? e)) → Σf':partial_fn fx.add_stmt_inv … (St_return (Some ? e)) f0 f' with
     705    [ mk_DPair ty e ⇒ λEnv.
     706      match fx_rettyp fx return λX. rettyp_match X ? → match X with [ Some t ⇒ Σr:register. env_has ?? t | None ⇒ ? ] → ? with
     707      [ None ⇒ λH. ⊥
     708      | Some t ⇒ λH,R.
     709        match R with
     710        [ mk_Sig r Hr ⇒
     711            let f ≝ add_expr fx ty e ? f «r, ?» in
     712            «pi1 … f, ?»
     713        ]
     714      ] (si_return … (π1 Env)) (pf_result fx f)
     715    ]
     716  ].
     717[ @mk_add_stmt_inv /2/
     718| inversion H #A #B #C destruct
     719| @mk_add_stmt_inv
     720  [ repeat @fn_contains_step @I
     721  | @empty_Cminor_labels_added //
     722  ]
     723| @(si_vars … (π1 Env))
     724| inversion H [ #E destruct ] #ty' #e' #E1 #E2 #_ destruct @Hr
     725| #l #H @I
     726| #l //
     727] qed.
     728
     729
     730let rec add_stmt (fx:fixed) (s:stmt) (Env:stmts_inv fx s) (f:partial_fn fx) on s : res (Σf':partial_fn fx. add_stmt_inv fx s f f') ≝
     731match s return λs.stmts_inv fx s → res (Σf':partial_fn fx. add_stmt_inv … s f f') with
    673732[ St_skip ⇒ λ_. OK ? «f, ?»
    674733| St_assign t x e ⇒ λEnv.
    675     let dst ≝ lookup_reg env x t (π1 (π1 Env)) in
    676     OK ? «pi1 … (add_expr ? env ? e (π2 (π1 Env)) f dst), ?»
     734    let dst ≝ lookup_reg (fx_env fx) x t (π1 (si_vars … (π1 Env))) in
     735    OK ? «pi1 … (add_expr … e (π2 (si_vars … (π1 Env))) f dst), ?»
    677736| St_store t e1 e2 ⇒ λEnv.
    678     let ❬f, val_reg❭ ≝ choose_reg … e2 f (π2 (π1 Env)) in
    679     let ❬f, addr_reg❭ ≝ choose_reg … e1 f (π1 (π1 Env)) in
     737    let ❬f, val_reg❭ ≝ choose_reg … e2 f (π2 (si_vars … (π1 Env))) in
     738    let ❬f, addr_reg❭ ≝ choose_reg … e1 f (π1 (si_vars … (π1 Env))) in
    680739    let f ≝ add_fresh_to_graph … (St_store t addr_reg val_reg) f ?? in
    681     let f ≝ add_expr ? env ? e1 (π1 (π1 Env)) f «addr_reg, ?» in
    682     OK ? «pi1 … (add_expr ? env ? e2 (π2 (π1 Env)) f «val_reg, ?»), ?»
     740    let f ≝ add_expr … e1 (π1 (si_vars … (π1 Env))) f «addr_reg, ?» in
     741    OK ? «pi1 … (add_expr … ? e2 (π2 (si_vars … (π1 Env))) f «val_reg, ?»), ?»
    683742| St_call return_opt_id e args ⇒ λEnv.
    684743    let return_opt_reg ≝
    685744      match return_opt_id return λo. ? → ? with
    686745      [ None ⇒ λ_. None ?
    687       | Some idty ⇒ λEnv. Some ? (lookup_reg env (\fst idty) (\snd idty) ?)
     746      | Some idty ⇒ λEnv. Some ? (lookup_reg (fx_env fx) (\fst idty) (\snd idty) ?)
    688747      ] Env in
    689     let ❬f, args_regs❭ ≝ choose_regs ? env args f (π2 (π1 Env)) in
     748    let ❬f, args_regs❭ ≝ choose_regs ? args f (π2 (si_vars ?? (π1 Env))) in
    690749    let f ≝
    691750      match expr_is_Id ? e with
    692751      [ Some id ⇒ add_fresh_to_graph … (St_call_id id args_regs return_opt_reg) f ??
    693752      | None ⇒
    694         let ❬f, fnr❭ ≝ choose_reg … e f (π2 (π1 (π1 Env))) in
     753        let ❬f, fnr❭ ≝ choose_reg … e f (π2 (π1 (si_vars … (π1 Env)))) in
    695754        let f ≝ add_fresh_to_graph … (St_call_ptr fnr args_regs return_opt_reg) f ?? in
    696         «pi1 … (add_expr ? env ? e (π2 (π1 (π1 Env))) f «fnr, ?»), ?»
     755        «pi1 … (add_expr … ? e (π2 (π1 (si_vars … (π1 Env)))) f «fnr, ?»), ?»
    697756      ] in
    698     OK ? «pi1 … (add_exprs ? env args (π2 (π1 Env)) args_regs ? f ?), ?»
     757    OK ? «pi1 … (add_exprs … args (π2 (si_vars … (π1 Env))) args_regs ? f ?), ?»
    699758(*
    700759| St_tailcall e args ⇒ λEnv.
     
    711770*)
    712771| St_seq s1 s2 ⇒ λEnv.
    713     do f2 ← add_stmt env label_env s2 ? f;
    714     do f1 ← add_stmt env label_env s1 ? f2;
     772    do f2 ← add_stmt s2 ? f;
     773    do f1 ← add_stmt s1 ? f2;
    715774      OK ? «pi1 … f1, ?»
    716775| St_ifthenelse _ _ e s1 s2 ⇒ λEnv.
    717776    let l_next ≝ pf_entry … f in
    718     do f2 ← add_stmt env label_env s2 (π2 Env) f;
     777    do f2 ← add_stmt … s2 (π2 (π2 Env)) f;
    719778    let l2 ≝ pf_entry … f2 in
    720779    let f ≝ add_fresh_to_graph … (λ_. R_skip l_next) f2 ?? in
    721     do f1 ← add_stmt env label_env s1 (π2 (π1 Env)) f;
    722     let ❬f,r❭ ≝ choose_reg … e f1 (π1 (π1 (π1 Env))) in
     780    do f1 ← add_stmt … s1 (π1 (π2 Env)) f;
     781    let ❬f,r❭ ≝ choose_reg … e f1 (si_vars … (π1 Env)) in
    723782    let f ≝ add_fresh_to_graph … (λl1. St_cond r l1 l2) f ?? in
    724     OK ? «pi1 … (add_expr ? env ? e (π1 (π1 (π1 Env))) f «r, ?»), ?»
    725 | St_return opt_e ⇒ let f0 ≝ f in
     783    OK ? «pi1 … (add_expr … ? e (si_vars … (π1 Env)) f «r, ?»), ?»
     784| St_return opt_e ⇒ λEnv. OK ? (add_return fx opt_e f Env)
     785(*let f0 ≝ f in
    726786    let f ≝ add_fresh_to_graph … (λ_. R_return) f ?? in
    727     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
     787    match opt_e return λo. stmt_inv ? (St_return o) → res (Σf':partial_fn fx.add_stmt_inv … (St_return o) f0 f') with
    728788    [ None ⇒ λEnv. OK ? «pi1 … f, ?»
    729789    | Some e ⇒
    730         match pf_result … f with
     790        match fx_rettyp … f with
    731791        [ None ⇒ λEnv. Error ? (msg ReturnMismatch)
    732792        | Some r ⇒
    733             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
     793            match e return λe.stmt_inv fx (St_return (Some ? e)) → res (Σf':partial_fn fx.add_stmt_inv … (St_return (Some ? e)) f0 f') with
    734794            [ mk_DPair ty e ⇒ λEnv.
    735795                match typ_eq (\snd r) ty with
    736                 [ 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
     796                [ inl E ⇒ let f ≝ add_expr ty e ? f «\fst r, ? E (* XXX E goes missing if I don't use it! *)» in
    737797                          OK ? «pi1 … f, ?»
    738798                | inr _ ⇒ Error ? (msg ReturnMismatch)
     
    740800            ]
    741801        ]
    742     ]
     802    ]*)
    743803| St_label l s' ⇒ λEnv.
    744     do f ← add_stmt env label_env s' (π2 Env) f;
    745     let l' ≝ lookup_label label_env l ? in
     804    do f ← add_stmt s' (π2 Env) f;
     805    let l' ≝ lookup_label (fx_lenv fx) l ? in
    746806    OK ? «pi1 … (add_to_graph … l' (R_skip (pf_entry … f)) f ??), ?»
    747807| St_goto l ⇒ λEnv.
    748     let l' ≝ lookup_label label_env l ? in
     808    let l' ≝ lookup_label (fx_lenv fx) l ? in
    749809    OK ? «pi1 … (add_fresh_to_graph' … (λ_.R_skip l') f ??), ?»
    750810| St_cost l s' ⇒ λEnv.
    751     do f ← add_stmt env label_env s' (π2 Env) f;
     811    do f ← add_stmt s' (π2 Env) f;
    752812    OK ? «pi1 … (add_fresh_to_graph … (St_cost l) f ??), ?»
    753813] Env.
    754 try @(π1 Env)
    755814try @(π2 Env)
    756 try @(π1 (π1 Env))
    757 try @(π2 (π1 Env))
     815try @(π1 (π2 Env))
     816try @(π2 (π2 Env))
    758817try @mk_add_stmt_inv
    759818try (repeat @fn_contains_step @I)
     
    762821try (#l #H @H)
    763822try (#l @I)
    764 [ @(pf_envok … (π1 (π1 Env))) @refl
     823[ @(pf_envok … (π1 (si_vars … (π1 Env)))) @refl
    765824| @(fn_con_env … (pi2 ?? val_reg)) repeat @fn_contains_step @I
    766825| @(fn_con_env … (pi2 ?? addr_reg)) repeat @fn_contains_step @I
     
    768827| @sym_eq @(All2_length … (pi2 ?? args_regs))
    769828| @(fn_con_env … (pi2 ?? fnr)) repeat @fn_contains_step @I
    770 | @(π1 (π1 (π1 Env)))
     829| @(π1 (π1 (si_vars … (π1 Env))))
    771830| #l #H cases (Exists_append … H)
    772   [ #H1 @(stmt_labels_added ????? (pi2 ?? f1) ? H1)
    773   | #H2 @(Cminor_labels_inv … H2) @(stmt_labels_added ????? (pi2 ?? f2))
     831  [ #H1 @(stmt_labels_added ???? (pi2 ?? f1) ? H1)
     832  | #H2 @(Cminor_labels_inv … H2) @(stmt_labels_added ???? (pi2 ?? f2))
    774833  ]
    775834| #l #H @(fn_con_graph … (pi2 ?? l_next)) repeat @fn_contains_step @I
    776835| #l #H cases (Exists_append … H)
    777   [ #H1 @(Cminor_labels_sig … H1) @Cminor_labels_sig @Cminor_labels_sig @(stmt_labels_added ????? (pi2 ?? f1))
    778   | #H2 @(Cminor_labels_sig … H2) @Cminor_labels_sig @Cminor_labels_sig @Cminor_labels_inv @Cminor_labels_sig @(stmt_labels_added ????? (pi2 ?? f2))
     836  [ #H1 @(Cminor_labels_sig … H1) @Cminor_labels_sig @Cminor_labels_sig @(stmt_labels_added ???? (pi2 ?? f1))
     837  | #H2 @(Cminor_labels_sig … H2) @Cminor_labels_sig @Cminor_labels_sig @Cminor_labels_inv @Cminor_labels_sig @(stmt_labels_added ???? (pi2 ?? f2))
    779838  ]
    780839| @(fn_con_env … (pi2 ?? r)) repeat @fn_contains_step @I
    781840| #l #H % [ @H | @(fn_con_graph … (pi2 ?? l2)) repeat @fn_contains_step @I ]
    782 | #_ (* see above *) <E @(pi2 ?? r)
     841| @(si_labels … (π1 Env))
    783842| @(pi2 … (pf_entry …))
    784843| #l1 * [ #E >E %{l'} % [ @lookup_label_rev' | whd >lookup_add_hit % #E' destruct (E') ]
    785         | @Cminor_labels_sig @(stmt_labels_added ????? (pi2 … f))
     844        | @Cminor_labels_sig @(stmt_labels_added ???? (pi2 … f))
    786845        ]
    787846| #l1 #H whd %2 @lookup_label_lpresent
    788 | @(equal_Cminor_labels_added ??? s') [ @refl | @Cminor_labels_sig @(stmt_labels_added ????? (pi2 … f)) ]
     847| @(si_labels … (π1 Env))
     848| @(equal_Cminor_labels_added ?? s') [ @refl | @Cminor_labels_sig @(stmt_labels_added ???? (pi2 … f)) ]
    789849] qed.
    790850
     
    797857let 〈locals0, env, reggen2〉 as E2 ≝ populate_env env1 reggen1 (f_vars f) in
    798858let ❬locals_reggen, result❭ as E3 ≝
    799   match f_return f return λ_.𝚺lr. option (Σrt. env_has ((\fst lr)@params) (\fst rt) (\snd rt)) with
    800   [ None ⇒ ❬〈locals0, reggen2〉, None ?
     859  match f_return f return λt.𝚺lr. resultok t ((\fst lr)@params) with
     860  [ None ⇒ ❬〈locals0, reggen2〉, I
    801861  | Some ty ⇒
    802862      let 〈r,gen〉 ≝ fresh … reggen2 in
    803         mk_DPair ? (λlr.option (Σrt. env_has ((\fst lr)@params) (\fst rt) (\snd rt))) 〈〈r,ty〉::locals0, gen〉 (Some ? «〈r,ty〉, ?») ] in
     863        mk_DPair ? (λlr.Σr. env_has ((\fst lr)@params) r ty) 〈〈r,ty〉::locals0, gen〉 «r, ?» ] in
    804864let locals ≝ \fst locals_reggen in
    805865let reggen ≝ \snd locals_reggen in
    806866let 〈label_env, labgen1〉 as El ≝ populate_label_env (empty_map …) labgen0 cminor_labels in
    807867let 〈l,labgen〉 ≝ fresh … labgen1 in
     868let fixed ≝ mk_fixed label_env env (f_return f) in
    808869let emptyfn ≝
    809   mk_partial_fn
    810     label_env
    811     env
     870  mk_partial_fn fixed
    812871    labgen
    813872    reggen
     
    822881    l
    823882    l in
    824 do f ← add_stmt env label_env (f_body f) ? emptyfn;
     883do f ← add_stmt fixed (f_body f) ? emptyfn;
    825884OK ? (mk_internal_function
    826885    (pf_labgen … f)
    827886    (pf_reggen … f)
    828     (match pf_result … f with [ None ⇒ None ? | Some rt ⇒ Some ? (pi1 … rt) ])
     887    (match fx_rettyp fixed return λt. match t with [ Some t ⇒ Σr:register. env_has ? r t | _ ⇒ True ] → ? with [ None ⇒ λ_. None ? | Some t ⇒ λR. Some ? 〈(pi1 … R),t〉 ] (pf_result … f))
    829888    (pf_params … f)
    830889    (pf_locals … f)
     
    849908  | @(stmt_labels_mp … L)
    850909    #l #H @(populates_label_env … (sym_eq … El)) @H
     910  | cases s in R ⊢ %; //
    851911  ]
    852912| #l #s #E @(labels_P_mp … (pf_closed … f l s E))
     
    864924  [ * #H1 #L1 cases (populate_env_list … (sym_eq … E1) … H1 L1)
    865925    [ * * | normalize @Exists_append_r ]
    866   | cases (f_return f) in E3;
    867     [ whd in ⊢ (??%% → ?); #E3 whd in match locals; destruct
     926  | (* gave up with     cases (f_return f) in result E3; *)
     927    @(match f_return f return λx.∀R:resultok x ((\fst locals_reggen)@params). ❬locals_reggen,R❭ = match x with [None ⇒ ?|Some _ ⇒ ?] → ? with [ None ⇒ λres1.? | Some rty ⇒ λres1.?] result E3)
     928    [ whd in ⊢ (??%% → ?); #E3' whd in match locals; destruct
    868929      @Exists_append_l
    869     | #rt cases (fresh ? reggen2) #rr #ru whd in ⊢ (??%% → ?); #E3 whd in match locals; destruct
     930    | cases (fresh ? reggen2) #rr #ru whd in ⊢ (??%% → ?); #E3' whd in match locals; destruct
    870931      #H' @Exists_append_l %2 @H'
    871932    ]
Note: See TracChangeset for help on using the changeset viewer.