Changeset 1105


Ignore:
Timestamp:
Aug 10, 2011, 5:17:58 PM (8 years ago)
Author:
campbell
Message:

Show that RTLabs graphs are closed on branch (i.e., all labels in
instructions are in the graph). Rather time consuming and fiddly.

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

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/id-lookup-branch/Cminor/toRTLabs.ma

    r1104 r1105  
    7979] qed.
    8080
     81lemma label_env_contents : ∀ls,lbls,u,lbls',u'.
     82  populate_label_env lbls u ls = 〈lbls',u'〉 →
     83  ∀l. present ?? lbls' l → Exists ? (λl'.l = l') ls ∨ present ?? lbls l.
     84#ls elim ls
     85[ #lbls #u #lbls' #u' #E #l #H %2 whd in E:(??%?); destruct @H
     86| #h #t #IH #lbls #u #lbls' #u' whd in ⊢ (??%? → ?)
     87  change in ⊢ (??match % with [ _ ⇒ ? ]? → ?) with (populate_label_env ???)
     88  lapply (refl ? (populate_label_env lbls u t))
     89  cases (populate_label_env lbls u t) in ⊢ (???% → %)
     90  #lbls1 #u1 #E1 whd in ⊢ (??%? → ?) cases (fresh ? u1) #r #gen' whd in ⊢ (??%? → ?)
     91  #E >(?:lbls' = add ?? lbls1 h r) [ 2: destruct (E) @refl ]
     92  #l #H cases (identifier_eq ? l h)
     93  [ #El %1 %1 @El
     94  | #NE cases (IH … E1 l ?)
     95    [ #H' %1 %2 @H' | #H' %2 @H' | whd in H >lookup_add_miss in H // @eq_identifier_elim // #E cases NE /2/ ]
     96  ]
     97] qed.
     98
    8199definition lookup_reg : ∀e:env. ∀id. present ?? e id → register ≝ lookup_present ??.
    82100definition lookup_label : ∀e:label_env. ∀id. present ?? e id → label ≝ lookup_present ??.
    83101
     102(* Check that the domain of one graph is included in another, for monotonicity
     103   properties.  Note that we don't say anything about the statements. *)
     104definition graph_included : graph statement → graph statement → Prop ≝
     105λg1,g2. ∀l. present ?? g1 l → present ?? g2 l.
     106
     107lemma graph_inc_trans : ∀g1,g2,g3.
     108  graph_included g1 g2 → graph_included g2 g3 → graph_included g1 g3.
     109#g1 #g2 #g3 #H1 #H2 #l #P1 @H2 @H1 @P1 qed.
     110
     111definition lpresent ≝ λlbls:label_env. λl. ∃l'. lookup ?? lbls l' = Some ? l.
     112
     113definition partially_closed : label_env → graph statement → Prop ≝
     114 λe,g. ∀l,s. lookup ?? g l = Some ? s → labels_P (λl. present ?? g l ∨ lpresent e l) s.
     115
     116(* I'd use a single parametrised definition along with internal_function, but
     117   it's a pain without implicit parameters. *)
     118record partial_fn (lenv:label_env) : Type[0] ≝
     119{ pf_labgen    : universe LabelTag
     120; pf_reggen    : universe RegisterTag
     121; pf_result    : option (register × typ)
     122; pf_params    : list (register × typ)
     123; pf_locals    : list (register × typ)
     124; pf_stacksize : nat
     125; pf_graph     : graph statement
     126; pf_closed    : partially_closed lenv pf_graph
     127; pf_entry     : Σl:label. present ?? pf_graph l
     128; pf_exit      : Σl:label. present ?? pf_graph l
     129}.
     130
     131inductive fn_graph_included (le:label_env) (f1:partial_fn le) (f2:partial_fn le) : Prop ≝
     132| fn_graph_inc : graph_included (pf_graph ? f1) (pf_graph ? f2) → fn_graph_included le f1 f2.
     133
     134lemma fn_graph_inc_trans : ∀le,f1,f2,f3.
     135  fn_graph_included le f1 f2 → fn_graph_included le f2 f3 → fn_graph_included le f1 f3.
     136#le #f1 #f2 #f3 * #H1 * #H2 % @(graph_inc_trans … H1 H2) qed.
     137
     138lemma fn_graph_included_refl : ∀label_env,f.
     139  fn_graph_included label_env f f.
     140#le #f % #l #H @H qed.
     141
     142lemma fn_graph_included_sig : ∀label_env,f,f0.
     143  ∀f':Σf':partial_fn label_env. fn_graph_included ? f0 f'.
     144  fn_graph_included label_env f f0 →
     145  fn_graph_included label_env f f'.
     146#le #f #f0 * #f' #H1 #H2 @(fn_graph_inc_trans … H2 H1)
     147qed.
     148
     149lemma add_statement_inv : ∀le,l,s.∀f.
     150  labels_present (pf_graph le f) s →
     151  partially_closed le (add … (pf_graph ? f) l s).
     152#le #l #s #f #p
     153#l' #s' #H cases (identifier_eq … l l')
     154[ #E >E in H >lookup_add_hit #E' <(?:s = s') [2:destruct //]
     155  @(labels_P_mp … p) #l0 #H %1 @lookup_add_oblivious @H
     156| #NE @(labels_P_mp … (pf_closed ? f l' s' ?))
     157  [ #lx * [ #H %1 @lookup_add_oblivious @H | #H %2 @H ]
     158  | >lookup_add_miss in H // @eq_identifier_elim // #E cases NE /2/
     159  ]
     160] qed.
     161
    84162(* Add a statement to the graph, *without* updating the entry label. *)
    85 definition fill_in_statement : label → statement → internal_function → internal_function ≝
    86 λl,s,f.
    87   mk_internal_function (f_labgen f) (f_reggen f)
    88                        (f_result f) (f_params f) (f_locals f)
    89                        (f_stacksize f) (add ?? (f_graph f) l s)
    90                        (dp ?? (f_entry f) ?) (dp ?? (f_exit f) ?).
    91 @lookup_add_oblivious @use_sig
    92 qed.
     163definition fill_in_statement : ∀le. label → ∀s:statement. ∀f:partial_fn le. labels_present (pf_graph ? f) s → Σf':partial_fn le. fn_graph_included le f f' ≝
     164λle,l,s,f,p.
     165  mk_partial_fn le (pf_labgen ? f) (pf_reggen ? f)
     166                (pf_result ? f) (pf_params ? f) (pf_locals ? f)
     167                (pf_stacksize ? f) (add ?? (pf_graph ? f) l s) ?
     168                «pf_entry ? f, ?» «pf_exit ? f, ?».
     169[ @add_statement_inv @p
     170| 2,3: @lookup_add_oblivious @use_sig
     171| % #l' @lookup_add_oblivious
     172] qed.
    93173
    94174(* Add a statement to the graph, making it the entry label. *)
    95 definition add_to_graph : label → statement → internal_function → internal_function ≝
    96 λl,s,f.
    97   mk_internal_function (f_labgen f) (f_reggen f)
    98                        (f_result f) (f_params f) (f_locals f)
    99                        (f_stacksize f) (add ?? (f_graph f) l s)
    100                        (dp ?? l ?) (dp ?? (f_exit f) ?).
    101 [ >lookup_add_hit % #E destruct
     175definition add_to_graph : ∀le. label → ∀s:statement. ∀f:partial_fn le. labels_present (pf_graph ? f) s → Σf':partial_fn le. fn_graph_included le f f' ≝
     176λle,l,s,f,p.
     177  mk_partial_fn le (pf_labgen ? f) (pf_reggen ? f)
     178                (pf_result ? f) (pf_params ? f) (pf_locals ? f)
     179                (pf_stacksize ? f) (add ?? (pf_graph ? f) l s) ?
     180                «l, ?» «pf_exit ? f, ?».
     181[ @add_statement_inv @p
     182| whd >lookup_add_hit % #E destruct
    102183| @lookup_add_oblivious @use_sig
     184| % #l' @lookup_add_oblivious
    103185] qed.
    104186
    105187(* Add a statement with a fresh label to the start of the function.  The
    106188   statement is parametrised by the *next* instruction's label. *)
    107 definition add_fresh_to_graph : (label → statement) → internal_function → internal_function ≝
    108 λs,f.
    109   let 〈l,g〉 ≝ fresh … (f_labgen f) in
    110   let s' ≝ s (f_entry f) in
    111     (mk_internal_function g (f_reggen f)
    112                        (f_result f) (f_params f) (f_locals f)
    113                        (f_stacksize f) (add ?? (f_graph f) l s')
    114                        (dp ?? l ?) (dp ?? (f_exit f) ?)).
    115 [ >lookup_add_hit % #E destruct
     189definition add_fresh_to_graph : ∀le. ∀s:(label → statement). ∀f:partial_fn le. (∀l. present ?? (pf_graph ? f) l → labels_present (pf_graph ? f) (s l)) → Σf':partial_fn le. fn_graph_included le f f' ≝
     190λle,s,f,p.
     191  let 〈l,g〉 ≝ fresh … (pf_labgen ? f) in
     192  let s' ≝ s (pf_entry ? f) in
     193    (mk_partial_fn le g (pf_reggen ? f)
     194                   (pf_result ? f) (pf_params ? f) (pf_locals ? f)
     195                   (pf_stacksize ? f) (add ?? (pf_graph ? f) l s') ?
     196                   «l, ?» «pf_exit ? f, ?»).
     197[ % #l' @lookup_add_oblivious
     198| @add_statement_inv @p @use_sig
     199| whd >lookup_add_hit % #E destruct
    116200| @lookup_add_oblivious @use_sig
    117201] qed.
    118202
    119 definition fresh_reg : internal_function → typ → register × internal_function ≝
    120 λf,ty.
    121   let 〈r,g〉 ≝ fresh … (f_reggen f) in
    122     〈r, mk_internal_function (f_labgen f) g
    123                        (f_result f) (f_params f) (〈r,ty〉::(f_locals f))
    124                        (f_stacksize f) (f_graph f) (f_entry f) (f_exit f)〉.
     203(* Variants for labels which are (goto) labels *)
     204
     205lemma add_statement_inv' : ∀le,l,s.∀f.
     206  labels_P (λl. present ?? (pf_graph le f) l ∨ lpresent le l) s →
     207  partially_closed le (add … (pf_graph ? f) l s).
     208#le #l #s #f #p
     209#l' #s' #H cases (identifier_eq … l l')
     210[ #E >E in H >lookup_add_hit #E' <(?:s = s') [2:destruct //]
     211  @(labels_P_mp … p) #l0 * [ #H %1 @lookup_add_oblivious @H | #H %2 @H ]
     212| #NE @(labels_P_mp … (pf_closed ? f l' s' ?))
     213  [ #lx * [ #H %1 @lookup_add_oblivious @H | #H %2 @H ]
     214  | >lookup_add_miss in H // @eq_identifier_elim // #E cases NE /2/
     215  ]
     216] qed.
     217
     218definition add_fresh_to_graph' : ∀le. ∀s:(label → statement). ∀f:partial_fn le. (∀l. present ?? (pf_graph ? f) l → labels_P (λl.present ?? (pf_graph ? f) l ∨ lpresent le l) (s l)) → Σf':partial_fn le. fn_graph_included le f f' ≝
     219λle,s,f,p.
     220  let 〈l,g〉 ≝ fresh … (pf_labgen ? f) in
     221  let s' ≝ s (pf_entry ? f) in
     222    (mk_partial_fn le g (pf_reggen ? f)
     223                   (pf_result ? f) (pf_params ? f) (pf_locals ? f)
     224                   (pf_stacksize ? f) (add ?? (pf_graph ? f) l s') ?
     225                   «l, ?» «pf_exit ? f, ?»).
     226[ % #l' @lookup_add_oblivious
     227| @add_statement_inv' @p @use_sig
     228| whd >lookup_add_hit % #E destruct
     229| @lookup_add_oblivious @use_sig
     230] qed.
     231
     232definition fresh_reg : ∀le. ∀f:partial_fn le. typ → register × (Σf':partial_fn le. fn_graph_included le f f') ≝
     233λle,f,ty.
     234  let 〈r,g〉 ≝ fresh … (pf_reggen ? f) in
     235    〈r, «mk_partial_fn le (pf_labgen ? f) g
     236                       (pf_result ? f) (pf_params ? f) (〈r,ty〉::(pf_locals ? f))
     237                       (pf_stacksize ? f) (pf_graph ? f) (pf_closed ? f) (pf_entry ? f) (pf_exit ? f), ?»〉.
     238% #l // qed.
    125239
    126240axiom UnknownVariable : String.
    127241
    128 definition choose_reg : ∀env:env.∀ty.∀e:expr ty. internal_function → expr_vars ty e (present ?? env) → register × internal_function
    129 λenv,ty,e,f.
    130   match e return λty,e. expr_vars ty e (present ?? env) → register × internal_function with
    131   [ Id _ i ⇒ λEnv. 〈lookup_reg env i Env, f
    132   | _ ⇒ λ_.fresh_reg f ty
     242definition choose_reg : ∀le. ∀env:env.∀ty.∀e:expr ty. ∀f:partial_fn le. expr_vars ty e (present ?? env) → register × (Σf':partial_fn le. fn_graph_included le f f')
     243λle,env,ty,e,f.
     244  match e return λty,e. expr_vars ty e (present ?? env) → register × (Σf':partial_fn le. fn_graph_included le f f') with
     245  [ Id _ i ⇒ λEnv. 〈lookup_reg env i Env, «f, ?»
     246  | _ ⇒ λ_.fresh_reg le f ty
    133247  ].
     248% // qed.
    134249 
    135250let 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 ≝ 
     
    138253definition exprtyp_present ≝ λenv:env.λe:Σt:typ.expr t.match e with [ dp ty e ⇒ expr_vars ty e (present ?? env) ].
    139254
    140 definition choose_regs : ∀env:env. ∀es:list (Σt:typ.expr t).
    141                          internal_function → All ? (exprtyp_present env) es →
    142                          list register × internal_function
    143 λenv,es,f,Env.
     255definition choose_regs : ∀le. ∀env:env. ∀es:list (Σt:typ.expr t).
     256                         ∀f:partial_fn le. All ? (exprtyp_present env) es →
     257                         list register × (Σf':partial_fn le. fn_graph_included le f f')
     258λle,env,es,f,Env.
    144259  foldr_all (Σt:typ.expr t) ??
    145260    (λe,p,acc. let 〈rs,f〉 ≝ acc in
    146              let 〈r,f'〉 ≝ match e return λe.? → ? with [ dp t e ⇒ λp.choose_reg env t e f ? ] p in
    147              〈r::rs,f'〉) 〈[ ], f〉 es Env.
    148 @p qed.
     261             let 〈r,f'〉 ≝ match e return λe.? → ? with [ dp t e ⇒ λp.choose_reg le env t e (eject … f) ? ] p in
     262             〈r::rs,«eject … f', ?»〉) 〈[ ], «f, ?»〉 es Env.
     263[ @p
     264| @fn_graph_inc_trans [ 3: @(use_sig ?? f') | skip | @(use_sig ?? f) ]
     265| % //
     266]  qed.
    149267
    150268lemma extract_pair : ∀A,B,C,D.  ∀u:A×B. ∀Q:A → B → C×D. ∀x,y.
     
    154272
    155273
    156 lemma choose_regs_length : ∀env,es,f,p,rs,f'.
    157   choose_regs env es f p = 〈rs,f'〉 → |es| = |rs|.
    158 #env #es #f elim es
     274lemma choose_regs_length : ∀le,env,es,f,p,rs,f'.
     275  choose_regs le env es f p = 〈rs,f'〉 → |es| = |rs|.
     276#le #env #es #f elim es
    159277[ #p #rs #f normalize #E destruct @refl
    160278| * #ty #e #t #IH #p #rs #f' whd in ⊢ (??%? → ??%?) #E
     
    168286] qed.
    169287
     288lemma present_inc : ∀le,f,l.
     289  ∀f':Σf':partial_fn le. fn_graph_included le f f'.
     290  present ?? (pf_graph le f) l →
     291  present ?? (pf_graph le f') l.
     292#le #f #l * #f' * #H1 #H2 @H1 @H2 qed.
     293
    170294axiom BadCminorProgram : String.
    171295
    172 let rec add_expr (env:env) (ty:typ) (e:expr ty) (Env:expr_vars ty e (present ?? env)) (dst:register) (f:internal_function) on e: internal_function
    173 match e return λty,e.expr_vars ty e (present ?? env) → internal_function with
     296let rec add_expr (le:label_env) (env:env) (ty:typ) (e:expr ty) (Env:expr_vars ty e (present ?? env)) (dst:register) (f:partial_fn le) on e: Σf':partial_fn le. fn_graph_included le f f'
     297match e return λty,e.expr_vars ty e (present ?? env) → Σf':partial_fn le. fn_graph_included le f f' with
    174298[ Id _ i ⇒ λEnv.
    175299    let r ≝ lookup_reg env i Env in
    176300    match register_eq r dst with
    177     [ inl _ ⇒ f
    178     | inr _ ⇒ add_fresh_to_graph (St_op1 Oid dst r) f
     301    [ inl _ ⇒ «f, ?»
     302    | inr _ ⇒ «eject … (add_fresh_to_graph ? (St_op1 Oid dst r) f ?), ?»
    179303    ]
    180 | Cst _ c ⇒ λ_. add_fresh_to_graph (St_const dst c) f
     304| Cst _ c ⇒ λ_. «add_fresh_to_graph ? (St_const dst c) f ?, ?»
    181305| Op1 _ _ op e' ⇒ λEnv.
    182     let 〈r,f〉 ≝ choose_reg env ? e' f Env in
    183     let f ≝ add_fresh_to_graph (St_op1 op dst r) f in
    184     add_expr env ? e' Env r f
     306    let 〈r,f〉 ≝ choose_reg ? env ? e' f Env in
     307    let f ≝ add_fresh_to_graph ? (St_op1 op dst r) f ? in
     308    let f ≝ add_expr ? env ? e' Env r f in
     309      «eject … f, ?»
    185310| Op2 _ _ _ op e1 e2 ⇒ λEnv.
    186     let 〈r1,f〉 ≝ choose_reg env ? e1 f (proj1 … Env) in
    187     let 〈r2,f〉 ≝ choose_reg env ? e2 f (proj2 … Env) in
    188     let f ≝ add_fresh_to_graph (St_op2 op dst r1 r2) f in
    189     let f ≝ add_expr env ? e2 (proj2 … Env) r2 f in
    190     add_expr env ? e1 (proj1 … Env) r1 f
     311    let 〈r1,f〉 ≝ choose_reg ? env ? e1 f (proj1 … Env) in
     312    let 〈r2,f〉 ≝ choose_reg ? env ? e2 f (proj2 … Env) in
     313    let f ≝ add_fresh_to_graph ? (St_op2 op dst r1 r2) f ? in
     314    let f ≝ add_expr ? env ? e2 (proj2 … Env) r2 f in
     315    let f ≝ add_expr ? env ? e1 (proj1 … Env) r1 f in
     316      «eject … f, ?»
    191317| Mem _ _ q e' ⇒ λEnv.
    192     let 〈r,f〉 ≝ choose_reg env ? e' f Env in
    193     let f ≝ add_fresh_to_graph (St_load q r dst) f in
    194     add_expr env ? e' Env r f
     318    let 〈r,f〉 ≝ choose_reg ? env ? e' f Env in
     319    let f ≝ add_fresh_to_graph ? (St_load q r dst) f ? in
     320    let f ≝ add_expr ? env ? e' Env r f in
     321      «eject … f, ?»
    195322| Cond _ _ _ e' e1 e2 ⇒ λEnv.
    196     let resume_at ≝ f_entry f in
    197     let f ≝ add_expr env ? e2 (proj2 … Env) dst f in
    198     let lfalse ≝ f_entry f in
    199     let f ≝ add_fresh_to_graph (λ_.St_skip resume_at) f in
    200     let f ≝ add_expr env ? e1 (proj2 … (proj1 … Env)) dst f in
    201     let 〈r,f〉 ≝ choose_reg env ? e' f (proj1 … (proj1 … Env)) in
    202     let f ≝ add_fresh_to_graph (λltrue. St_cond r ltrue lfalse) f in
    203     add_expr env ? e' (proj1 … (proj1 … Env)) r f
     323    let resume_at ≝ pf_entry ? f in
     324    let f ≝ add_expr ? env ? e2 (proj2 … Env) dst f in
     325    let lfalse ≝ pf_entry ? f in
     326    let f ≝ add_fresh_to_graph ? (λ_.St_skip resume_at) f ? in
     327    let f ≝ add_expr ? env ? e1 (proj2 … (proj1 … Env)) dst f in
     328    let 〈r,f〉 as E ≝ choose_reg ? env ? e' f (proj1 … (proj1 … Env)) in
     329    let f ≝ add_fresh_to_graph ? (λltrue. St_cond r ltrue lfalse) f ? in
     330    let f ≝ add_expr ? env ? e' (proj1 … (proj1 … Env)) r f in
     331      «eject … f, ?»
    204332| Ecost _ l e' ⇒ λEnv.
    205     let f ≝ add_expr env ? e' Env dst f in
    206     add_fresh_to_graph (St_cost l) f
     333    let f ≝ add_expr ? env ? e' Env dst f in
     334    let f ≝ add_fresh_to_graph ? (St_cost l) f ? in
     335      «f, ?»
    207336] Env.
    208 
    209 let rec add_exprs (env:env) (es:list (Σt:typ.expr t)) (Env:All ? (exprtyp_present env) es)
    210                   (dsts:list register) (pf:|es|=|dsts|) (f:internal_function) on es: internal_function ≝
     337(* For new labels, we need to step back through the definitions of f until we
     338   hit the point that it was added. *)
     339try @fn_graph_included_refl
     340try (#l #H @H)
     341[ 7: #l #H whd % [ @H |
     342    @present_inc
     343    @present_inc
     344    @present_inc
     345    @(use_sig ? (present ???)) ]
     346| 8: #l #H
     347    @present_inc
     348    @(use_sig ? (present ???))
     349(* For the monotonicity properties, we just keep going back until we're at the
     350   start.  The repeat tactical helps here. *)
     351| *: repeat @fn_graph_included_sig @fn_graph_included_refl
     352] qed.
     353
     354let rec add_exprs (le:label_env) (env:env) (es:list (Σt:typ.expr t)) (Env:All ? (exprtyp_present env) es)
     355                  (dsts:list register) (pf:|es|=|dsts|) (f:partial_fn le) on es: Σf':partial_fn le. fn_graph_included le f f' ≝
    211356match es return λes.All ?? es → |es|=|dsts| → ? with
    212 [ nil ⇒ λ_. match dsts return λx. ?=|x| → ? with [ nil ⇒ λ_. f | cons _ _ ⇒ λpf.⊥ ]
     357[ nil ⇒ λ_. match dsts return λx. ?=|x| → Σf':partial_fn le. fn_graph_included le f f' with [ nil ⇒ λ_. «f, ?» | cons _ _ ⇒ λpf.⊥ ]
    213358| cons e et ⇒ λEnv.
    214359    match dsts return λx. ?=|x| → ? with
    215360    [ nil ⇒ λpf.⊥
    216361    | cons r rt ⇒ λpf.
    217         let f ≝ add_exprs env et ? rt ? f in
    218         match e return λe.? → ? with [ dp ty e ⇒ λEnv. add_expr env ty e ? r f ] (proj1 ?? Env)
     362        let f ≝ add_exprs ? env et ? rt ? f in
     363        match e return λe.exprtyp_present ? e → ? with [ dp ty e ⇒ λEnv.
     364          let f ≝ add_expr ? env ty e ? r f in
     365            «eject … f, ?» ] (proj1 ?? Env)
    219366    ]
    220367] Env pf.
    221 [ 1,2,3: normalize in pf; destruct //
    222 | whd in Env @(proj2 … Env)
     368[ //
     369| 2,3: normalize in pf; destruct
     370| @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_refl
     371| @Env
     372| @(proj2 … Env)
    223373| normalize in pf; destruct @e0 ] qed.
    224374
     
    229379λenv,lenv. stmt_P (λs. stmt_vars (present ?? env) s ∧ stmt_labels (present ?? lenv) s).
    230380
    231 let rec add_stmt (env:env) (label_env:label_env) (s:stmt) (Env:stmt_inv env label_env s) (exits:list label) (f:internal_function) on s : res internal_function ≝
    232 match s return λs.stmt_inv env label_env s → res internal_function with
    233 [ St_skip ⇒ λ_. OK ? f
     381(* Trick to avoid multiplying the proof obligations for the non-Id cases. *)
     382definition expr_is_Id : ∀t. expr t → option ident ≝
     383λt,e. match e with
     384[ Id _ id ⇒ Some ? id
     385| _ ⇒ None ?
     386].
     387
     388(* XXX Work around odd disambiguation errors. *)
     389alias id "R_skip" = "cic:/matita/cerco/RTLabs/syntax/statement.con(0,1,0)".
     390alias id "R_return" = "cic:/matita/cerco/RTLabs/syntax/statement.con(0,14,0)".
     391
     392definition nth_sig : ∀A. ∀P:A → Prop. errmsg → (Σl:list A. All A P l) → nat → res (Σa:A. P a) ≝
     393λA,P,m,l,n.
     394  match nth_opt A n l return λx.(∀_.x = ? → ?) → ? with
     395  [ None ⇒ λ_. Error ? m
     396  | Some a ⇒ λH'. OK ? «a, ?»
     397  ] (All_nth A P n l (use_sig … l)).
     398@H' @refl qed.
     399
     400lemma lookup_label_rev : ∀lenv,l,l',p.
     401  lookup_label lenv l p = l' → lookup ?? lenv l = Some ? l'.
     402#lenv #l #l' #p
     403cut (∃lx. lookup ?? lenv l = Some ? lx)
     404[ whd in p; cases (lookup ?? lenv l) in p ⊢ %
     405  [ * #H cases (H (refl ??))
     406  | #lx #_ %{lx} @refl
     407  ]
     408| * #lx #E whd in ⊢ (??%? → ?) cases p >E #q whd in ⊢ (??%? → ?) #E' >E' @refl
     409] qed.
     410
     411lemma lookup_label_rev' : ∀lenv,l,p.
     412  lookup ?? lenv l = Some ? (lookup_label lenv l p).
     413#lenv #l #p @lookup_label_rev [ @p | @refl ]
     414qed.
     415
     416lemma lookup_label_lpresent : ∀lenv,l,p.
     417  lpresent lenv (lookup_label lenv l p).
     418#le #l #p whd %{l} @lookup_label_rev'
     419qed.
     420
     421(* We need to show that the graph only grows, and that Cminor labels will end
     422   up in the graph. *)
     423definition Cminor_labels_added ≝ λle,s,f'.
     424∀l. Exists ? (λl'.l=l') (labels_of s) →
     425∃l'. lookup ?? le l = Some ? l' ∧ present ?? (pf_graph le f') l'.
     426
     427record add_stmt_inv (le:label_env) (s:stmt) (f:partial_fn le) (f':partial_fn le) : Prop ≝
     428{ stmt_graph_inc : fn_graph_included ? f f'
     429; stmt_labels_added : Cminor_labels_added le s f'
     430}.
     431
     432lemma empty_Cminor_labels_added : ∀le,s,f'.
     433  labels_of s = [ ] → Cminor_labels_added le s f'.
     434#le #s #f' #E whd >E #l *;
     435qed.
     436
     437lemma equal_Cminor_labels_added : ∀le,s,s',f.
     438  labels_of s = labels_of s' → Cminor_labels_added le s' f →
     439  Cminor_labels_added le s f.
     440#le #s #s' #f #E whd in ⊢ (% → %) > E #H @H
     441qed.
     442
     443lemma fn_graph_included_inv : ∀label_env,s,f,f0.
     444  ∀f':Σf':partial_fn label_env. add_stmt_inv label_env s f0 f'.
     445  fn_graph_included label_env f f0 →
     446  fn_graph_included label_env f f'.
     447#label_env #s #f #f0 * #f' * #H1 #H2 #H3
     448@(fn_graph_inc_trans … H3 H1)
     449qed.
     450
     451lemma present_inc' : ∀le,s,f,l.
     452  ∀f':(Σf':partial_fn le. add_stmt_inv le s f f').
     453  present ?? (pf_graph le f) l →
     454  present ?? (pf_graph le f') l.
     455#le #s #f #l * #f' * * #H1 #H2 #H3
     456@H1 @H3
     457qed.
     458
     459lemma Cminor_labels_inv : ∀le,s,s',f.
     460  ∀f':Σf':partial_fn le. add_stmt_inv le s' f f'.
     461  Cminor_labels_added le s f →
     462  Cminor_labels_added le s f'.
     463#le #s #s' #f * #f' * #H1 #H2 #H3
     464#l #E cases (H3 l E) #l' * #L #P
     465%{l'} % [ @L | @present_inc' @P ]
     466qed.
     467
     468lemma Cminor_labels_sig : ∀le,s,f.
     469  ∀f':Σf':partial_fn le. fn_graph_included le f f'.
     470  Cminor_labels_added le s f →
     471  Cminor_labels_added le s f'.
     472#le #s #f * #f' #H1 #H2
     473#l #E cases (H2 l E) #l' * #L #P
     474%{l'} % [ @L | @present_inc @P ]
     475qed.
     476
     477let rec add_stmt (env:env) (label_env:label_env) (s:stmt) (Env:stmt_inv env label_env s) (f:partial_fn label_env) (exits:Σls:list label. All ? (present ?? (pf_graph ? f)) ls) on s : res (Σf':partial_fn label_env. add_stmt_inv label_env s f f') ≝
     478match s return λs.stmt_inv env label_env s → res (Σf':partial_fn label_env. add_stmt_inv ? s f f') with
     479[ St_skip ⇒ λ_. OK ? «f, ?»
    234480| St_assign _ x e ⇒ λEnv.
    235481    let dst ≝ lookup_reg env x (π1 (π1 Env)) in
    236     OK ? (add_expr env ? e (π2 (π1 Env)) dst f)
     482    OK ? «eject … (add_expr ? env ? e (π2 (π1 Env)) dst f), ?»
    237483| St_store _ _ q e1 e2 ⇒ λEnv.
    238     let 〈val_reg, f〉 ≝ choose_reg env ? e2 f (π2 (π1 Env)) in
    239     let 〈addr_reg, f〉 ≝ choose_reg env ? e1 f (π1 (π1 Env)) in
    240     let f ≝ add_fresh_to_graph (St_store q addr_reg val_reg) f in
    241     let f ≝ add_expr env ? e1 (π1 (π1 Env)) addr_reg f in
    242     OK ? (add_expr env ? e2 (π2 (π1 Env)) val_reg f)
     484    let 〈val_reg, f〉 ≝ choose_reg ? env ? e2 f (π2 (π1 Env)) in
     485    let 〈addr_reg, f〉 ≝ choose_reg ? env ? e1 f (π1 (π1 Env)) in
     486    let f ≝ add_fresh_to_graph ? (St_store q addr_reg val_reg) f ? in
     487    let f ≝ add_expr ? env ? e1 (π1 (π1 Env)) addr_reg f in
     488    OK ? «eject … (add_expr ? env ? e2 (π2 (π1 Env)) val_reg f), ?»
    243489| St_call return_opt_id e args ⇒ λEnv.
    244490    let return_opt_reg ≝
     
    247493      | Some id ⇒ λEnv. Some ? (lookup_reg env id ?)
    248494      ] Env in
    249     let 〈args_regs, f〉 as Eregs ≝ choose_regs env args f (π2 (π1 Env)) in
     495    let 〈args_regs, f〉 as Eregs ≝ choose_regs ? env args f (π2 (π1 Env)) in
    250496    let f ≝
    251       match e with
    252       [ Id _ id ⇒ add_fresh_to_graph (St_call_id id args_regs return_opt_reg) f
    253       | _
    254         let 〈fnr, f〉 ≝ choose_reg env ? e f (π2 (π1 (π1 Env))) in
    255         let f ≝ add_fresh_to_graph (St_call_ptr fnr args_regs return_opt_reg) f in
    256         add_expr env ? e (π2 (π1 (π1 Env))) fnr f
     497      match expr_is_Id ? e with
     498      [ Some id ⇒ add_fresh_to_graph ? (St_call_id id args_regs return_opt_reg) f ?
     499      | None
     500        let 〈fnr, f〉 ≝ choose_reg ? env ? e f (π2 (π1 (π1 Env))) in
     501        let f ≝ add_fresh_to_graph ? (St_call_ptr fnr args_regs return_opt_reg) f ? in
     502        «eject … (add_expr ? env ? e (π2 (π1 (π1 Env))) fnr f), ?»
    257503      ] in
    258     OK ? (add_exprs env args (π2 (π1 Env)) args_regs ? f)
     504    OK ? «eject … (add_exprs ? env args (π2 (π1 Env)) args_regs ? f), ?»
    259505| St_tailcall e args ⇒ λEnv.
    260     let 〈args_regs, f〉 as Eregs ≝ choose_regs env args f (π2 (π1 Env)) in
     506    let 〈args_regs, f〉 as Eregs ≝ choose_regs ? env args f (π2 (π1 Env)) in
    261507    let f ≝
    262       match e with
    263       [ Id _ id ⇒ add_fresh_to_graph (λ_. St_tailcall_id id args_regs) f
    264       | _
    265         let 〈fnr, f〉 ≝ choose_reg env ? e f (π1 (π1 Env)) in
    266         let f ≝ add_fresh_to_graph (λ_. St_tailcall_ptr fnr args_regs) f in
    267         add_expr env ? e (π1 (π1 Env)) fnr f
     508      match expr_is_Id ? e with
     509      [ Some id ⇒ add_fresh_to_graph ? (λ_. St_tailcall_id id args_regs) f ?
     510      | None
     511        let 〈fnr, f〉 ≝ choose_reg ? env ? e f (π1 (π1 Env)) in
     512        let f ≝ add_fresh_to_graph ? (λ_. St_tailcall_ptr fnr args_regs) f ? in
     513        «eject … (add_expr ? env ? e (π1 (π1 Env)) fnr f), ?»
    268514      ] in
    269     OK ? (add_exprs env args (π2 (π1 Env)) args_regs ? f)
     515    OK ? «eject … (add_exprs ? env args (π2 (π1 Env)) args_regs ? f), ?»
    270516| St_seq s1 s2 ⇒ λEnv.
    271     do f ← add_stmt env label_env s2 ? exits f;
    272     add_stmt env label_env s1 ? exits f
     517    do f2 ← add_stmt env label_env s2 ? f «exits, ?»;
     518    do f1 ← add_stmt env label_env s1 ? f2 «exits, ?»;
     519      OK ? «eject … f1, ?»
    273520| St_ifthenelse _ _ e s1 s2 ⇒ λEnv.
    274     let l_next ≝ f_entry f in
    275     do f ← add_stmt env label_env s2 (π2 Env) exits f;
    276     let l2 ≝ f_entry f in
    277     let f ≝ add_fresh_to_graph ? (* XXX: fails, but works if applied afterwards: λ_. St_skip l_next*) f in
    278     do f ← add_stmt env label_env s1 (π2 (π1 Env)) exits f;
    279     let 〈r,f〉 ≝ choose_reg env ? e f (π1 (π1 (π1 Env))) in
    280     let f ≝ add_fresh_to_graph (λl1. St_cond r l1 l2) f in
    281     OK ? (add_expr env ? e (π1 (π1 (π1 Env))) r f)
     521    let l_next ≝ pf_entry ? f in
     522    do f2 ← add_stmt env label_env s2 (π2 Env) f «exits, ?»;
     523    let l2 ≝ pf_entry ? f2 in
     524    let f ≝ add_fresh_to_graph ? (λ_. R_skip l_next) f2 ? in
     525    do f1 ← add_stmt env label_env s1 (π2 (π1 Env)) f «exits, ?»;
     526    let 〈r,f〉 ≝ choose_reg ? env ? e f1 (π1 (π1 (π1 Env))) in
     527    let f ≝ add_fresh_to_graph ? (λl1. St_cond r l1 l2) f ? in
     528    OK ? «eject … (add_expr ? env ? e (π1 (π1 (π1 Env))) r f), ?»
    282529| St_loop s ⇒ λEnv.
    283     let f ≝ add_fresh_to_graph ? f in (* dummy statement, fill in afterwards *)
    284     let l_loop ≝ f_entry f in
    285     do f ← add_stmt env label_env s (π2 Env) exits f;
    286     OK ? (fill_in_statement l_loop (* XXX another odd failure: St_skip (f_entry f)*)? f)
     530    let f ≝ add_fresh_to_graph ? R_skip f ? in (* dummy statement, fill in afterwards *)
     531    let l_loop ≝ pf_entry ? f in
     532    do f ← add_stmt env label_env s (π2 Env) f «exits, ?»;
     533    OK ? «eject … (fill_in_statement ? l_loop (R_skip (pf_entry ? f)) f ?), ?»
    287534| St_block s ⇒ λEnv.
    288     add_stmt env label_env s (π2 Env) ((f_entry f)::exits) f
     535    do f ← add_stmt env label_env s (π2 Env) f («pf_entry ? f::exits, ?»);
     536    OK ? «eject … f, ?»
    289537| St_exit n ⇒ λEnv.
    290     do l ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits);
    291     OK ? (add_fresh_to_graph (* XXX another: λ_. St_skip l*)? f)
     538    do l ← nth_sig ?? (msg BadCminorProgram) exits n;
     539    OK ? «eject … (add_fresh_to_graph ? (λ_. R_skip l) f ?), ?»
    292540| St_switch sz sg e tab n ⇒ λEnv.
    293     let 〈r,f〉 ≝ choose_reg env ? e f ? in
    294     do l_default ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits);
    295     let f ≝ add_fresh_to_graph (* XXX grrrr: λ_. St_skip l_default*)? f in
    296     do f ← foldr ?? (λcs,f.
     541    let 〈r,f〉 ≝ choose_reg ? env ? e f ? in
     542    do l_default ← nth_sig ?? (msg BadCminorProgram) exits n;
     543    let f ≝ add_fresh_to_graph ? (λ_. R_skip l_default) f ? in
     544    do f ← foldr ? (res (Σf':partial_fn ?. ?)) (λcs,f.
    297545      do f ← f;
    298546      let 〈i,n〉 ≝ cs in
    299547      let 〈cr,f〉 ≝ fresh_reg … f (ASTint sz sg) in
    300548      let 〈br,f〉 ≝ fresh_reg … f (ASTint I8 Unsigned) in
    301       do l_case ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits);
    302       let f ≝ add_fresh_to_graph (St_cond br l_case) f in
    303       let f ≝ add_fresh_to_graph (St_op2 (Ocmpu Ceq) (* signed? *) br r cr) f in
    304         OK ? (add_fresh_to_graph (St_const cr (Ointconst ? i)) f)) (OK ? f) tab;
    305     OK ? (add_expr env ? e (π1 Env) r f)
    306 | St_return opt_e ⇒
    307     let f ≝ add_fresh_to_graph (λ_. St_return) f in
    308     match opt_e return λo. ? → ? with
    309     [ None ⇒ λEnv. OK ? f
    310     | Some e ⇒
    311         match f_result f with
     549      do l_case ← nth_sig ?? (msg BadCminorProgram) exits n;
     550      let f ≝ add_fresh_to_graph ? (St_cond br l_case) f ? in
     551      let f ≝ add_fresh_to_graph ? (St_op2 (Ocmpu Ceq) (* signed? *) br r cr) f ? in
     552      let f ≝ add_fresh_to_graph ? (St_const cr (Ointconst ? i)) f ? in
     553        OK ? «eject … f, ?») (OK ? f) tab;
     554    OK ? «eject … (add_expr ? env ? e (π1 Env) r f), ?»
     555| St_return opt_e ⇒ let f0 ≝ f in
     556    let f ≝ add_fresh_to_graph ? (λ_. R_return) f ? in
     557    match opt_e return λo. stmt_inv ?? (St_return o) → res (Σf':partial_fn label_env.add_stmt_inv ? (St_return o) f0 f') with
     558    [ None ⇒ λEnv. OK ? «eject … f, ?»
     559    | Some e ⇒
     560        match pf_result ? f with
    312561        [ None ⇒ λEnv. Error ? (msg ReturnMismatch)
    313         | Some r ⇒ match e return λe.? → ? with [ dp ty e ⇒ λEnv. OK ? (add_expr env ? e ? (\fst r) f) ]
     562        | Some r ⇒
     563            match e return λe.stmt_inv env label_env (St_return (Some ? e)) → res (Σf':partial_fn label_env.add_stmt_inv label_env (St_return (Some ? e)) f0 f') with
     564            [ dp ty e ⇒ λEnv. let f ≝ add_expr label_env env ty e ? (\fst r) f in
     565                              OK ? «eject … f, ?» ]
    314566        ]
    315567    ]
    316568| St_label l s' ⇒ λEnv.
    317     do f ← add_stmt env label_env s' (π2 Env) exits f;
     569    do f ← add_stmt env label_env s' (π2 Env) f exits;
    318570    let l' ≝ lookup_label label_env l ? in
    319     OK ? (add_to_graph l' (* XXX again: St_skip (f_entry f)*)? f)
     571    OK ? «eject … (add_to_graph ? l' (R_skip (pf_entry ? f)) f ?), ?»
    320572| St_goto l ⇒ λEnv.
    321573    let l' ≝ lookup_label label_env l ? in
    322     OK ? (add_fresh_to_graph (* XXX again: λ_.St_skip l'*)? f)
     574    OK ? «eject … (add_fresh_to_graph' ? (λ_.R_skip l') f ?), ?»
    323575| St_cost l s' ⇒ λEnv.
    324     do f ← add_stmt env label_env s' (π2 Env) exits f;
    325     OK ? (add_fresh_to_graph (St_cost l) f)
     576    do f ← add_stmt env label_env s' (π2 Env) f exits;
     577    OK ? «eject … (add_fresh_to_graph ? (St_cost l) f ?), ?»
    326578] Env.
    327579try @(π1 Env)
     
    329581try @(π1 (π1 Env))
    330582try @(π2 (π1 Env))
     583try @mk_add_stmt_inv
     584try (@empty_Cminor_labels_added @refl)
     585try (@(All_mp … (use_sig ?? exits)))
     586try @fn_graph_included_refl
     587try (repeat @fn_graph_included_inv repeat @fn_graph_included_sig @fn_graph_included_refl)
     588try (#l #H @I)
     589try (#l #H @H)
    331590[ -f @(choose_regs_length … (sym_eq … Eregs))
     591| @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_refl
    332592| whd in Env @(π1 (π1 (π1 Env)))
    333593| -f @(choose_regs_length … (sym_eq … Eregs))
    334 | @(λ_. St_skip l_next)
    335 | @(St_skip (f_entry f))
    336 | @St_skip
    337 | @(λ_. St_skip l)
    338 | @(λ_. St_skip l_default)
    339 | @(St_skip (f_entry f))
    340 | @(λ_.St_skip l')
    341 ] qed.
    342 
     594| @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_refl
     595| #l #H cases (Exists_append … H)
     596  [ #H1 @(stmt_labels_added ???? (use_sig ?? f1) ? H1)
     597  | #H2 @(Cminor_labels_inv … H2) @(stmt_labels_added ???? (use_sig ?? f2))
     598  ]
     599| #l #H @present_inc' @H
     600| #l #H @present_inc' @use_sig
     601| @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_inv @fn_graph_included_sig @fn_graph_included_inv @fn_graph_included_refl
     602| #l #H cases (Exists_append … H)
     603  [ #H1 @(Cminor_labels_sig … H1) @Cminor_labels_sig @Cminor_labels_sig @(stmt_labels_added ???? (use_sig ?? f1))
     604  | #H2 @(Cminor_labels_sig … H2) @Cminor_labels_sig @Cminor_labels_sig @Cminor_labels_inv @Cminor_labels_sig @(stmt_labels_added ???? (use_sig ?? f2))
     605  ]
     606| #l #H % [ @H | @present_inc @present_inc' @present_inc @(use_sig ?? (pf_entry ? f2)) ]
     607| #l #H @present_inc @present_inc' @H
     608| #l #H @present_inc @H
     609| @(use_sig ?? (pf_entry ??))
     610| @fn_graph_included_sig @fn_graph_included_inv @fn_graph_included_sig @fn_graph_included_refl
     611| @Cminor_labels_sig @(equal_Cminor_labels_added ?? s) [ @refl | @(stmt_labels_added ???? (use_sig ? (add_stmt_inv ???) ?)) ]
     612| % [ @use_sig | @(use_sig ?? exits) ]
     613| @(equal_Cminor_labels_added ?? s) [ @refl | @(stmt_labels_added ???? (use_sig ? (add_stmt_inv ???) ?)) ]
     614| #l #H @use_sig
     615| #l #H @present_inc @use_sig
     616| #l #H % [ @present_inc @present_inc @present_inc @present_inc @use_sig | @H ]
     617| @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_refl
     618| @use_sig
     619| @fn_graph_included_sig @fn_graph_included_inv @fn_graph_included_refl
     620| #l1 * [ #E >E %{l'} % [ @lookup_label_rev' | whd >lookup_add_hit % #E' destruct (E') ]
     621        |@Cminor_labels_sig @(stmt_labels_added ???? (use_sig ? (add_stmt_inv ???) ?))
     622        ]
     623| #l1 #H whd %2 @lookup_label_lpresent
     624| @fn_graph_included_sig @fn_graph_included_inv @fn_graph_included_refl
     625| @(equal_Cminor_labels_added ?? s') [ @refl | @Cminor_labels_sig @(stmt_labels_added ???? (use_sig ? (add_stmt_inv ???) ?)) ]
     626] qed.
     627
     628(*
     629definition mk_fn : ∀le. partial_fn le → internal_function ≝
     630λle, f.
     631  mk_internal_function
     632    (pf_labgen ? f)
     633    (pf_reggen ? f)
     634    (pf_result ? f)
     635    (pf_params ? f)
     636    (pf_locals ? f)
     637    (pf_stacksize ? f)
     638    (pf_graph ? f)
     639    ?
     640    (pf_entry ? f)
     641    (pf_exit ? f).
     642#l #s #E @(labels_P_mp … (pf_closed ? f l s E))
     643#l' * [ // | #H
     644*)
    343645
    344646definition c2ra_function (*: internal_function → internal_function*) ≝
     
    358660let 〈l,labgen〉 ≝ fresh … labgen1 in
    359661let emptyfn ≝
    360   mk_internal_function
     662  mk_partial_fn
     663    label_env
    361664    labgen
    362665    reggen
     
    366669    (f_stacksize f)
    367670    (add ?? (empty_map …) l St_return)
     671    ?
    368672    l
    369673    l in
    370 do f ← add_stmt env label_env (f_body f) ? [ ] emptyfn;
    371 do u1 ← check_universe_ok ? (f_labgen f);
    372 do u2 ← check_universe_ok ? (f_reggen f);
    373 OK ? f
    374 .
    375 [ @(stmt_P_mp … (f_inv f))
     674do f ← add_stmt env label_env (f_body f) ? emptyfn [ ];
     675do u1 ← check_universe_ok ? (pf_labgen ? f);
     676do u2 ← check_universe_ok ? (pf_reggen ? f);
     677OK ? (mk_internal_function
     678    (pf_labgen ? f)
     679    (pf_reggen ? f)
     680    (pf_result ? f)
     681    (pf_params ? f)
     682    (pf_locals ? f)
     683    (pf_stacksize ? f)
     684    (pf_graph ? f)
     685    ?
     686    (pf_entry ? f)
     687    (pf_exit ? f)
     688  ).
     689[ @I
     690| -emptyfn @(stmt_P_mp … (f_inv f))
    376691  #s * #V #L %
    377692  [ @(stmt_vars_mp … V)
     
    384699    #l #H @(populates_label_env … (sym_eq … El)) @H
    385700  ]
    386 | *: >lookup_add_hit % #E destruct
     701| #l #s #E @(labels_P_mp … (pf_closed ? f l s E))
     702  #l' * [ // | * #l #H cases f #f' * #L #P cases (P l ?)
     703  [ #lx >H * #Ex >(?:lx = l') [ 2: destruct (Ex) @refl ]
     704  #P' @P'
     705  | cases (label_env_contents … (sym_eq ??? El) l ?)
     706    [ #H @H
     707    | whd in ⊢ (% → ?) whd in ⊢ (?(??%?) → ?) * #H cases (H (refl ??))
     708    | whd >H % #E' destruct (E')
     709    ]
     710  ]
     711  ]
     712| #l1 #s #LOOKUP cases (lookup_add_cases ??????? LOOKUP)
     713  [ * #E1 #E2 >E2 @I
     714  | whd in ⊢ (??%? → ?) #E' destruct (E')
     715  ]
     716| *: whd >lookup_add_hit % #E destruct
    387717]
    388718qed.
  • Deliverables/D3.3/id-lookup-branch/RTLabs/syntax.ma

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

    r1104 r1105  
    122122] qed.
    123123
     124lemma lookup_add_cases : ∀tag,A,m,i,j,a,v.
     125  lookup tag A (add tag A m i a) j = Some ? v →
     126  (i=j ∧ v = a) ∨ lookup tag A m j = Some ? v.
     127#tag #A #m #i #j #a #v
     128cases (identifier_eq ? i j)
     129[ #E >E >lookup_add_hit #H %1 destruct % //
     130| #NE >lookup_add_miss /2/ @eq_identifier_elim /2/
     131] qed.
     132
    124133(* Extract every identifier, value pair from the map. *)
    125134definition elements : ∀tag,A. identifier_map tag A → list (identifier tag × A) ≝
  • Deliverables/D3.3/id-lookup-branch/utilities/lists.ma

    r1102 r1105  
    1717#h #t #IH * /3/
    1818qed.
     19
     20lemma All_nth : ∀A,P,n,l.
     21  All A P l →
     22  ∀a.
     23  nth_opt A n l = Some A a →
     24  P a.
     25#A #P #n elim n
     26[ * [ #_ #a #E whd in E:(??%?); destruct
     27    | #hd #tl * #H #_ #a #E whd in E:(??%?); destruct @H
     28    ]
     29| #m #IH *
     30  [ #_ #a #E whd in E:(??%?); destruct
     31  | #hd #tl * #_ whd in ⊢ (? → ∀_.??%? → ?) @IH
     32  ]
     33] qed.
    1934
    2035let rec exists (A:Type[0]) (p:A → bool) (l:list A) on l : bool ≝
Note: See TracChangeset for help on using the changeset viewer.