Ignore:
Timestamp:
Jul 15, 2011, 4:56:04 PM (9 years ago)
Author:
campbell
Message:

Use not equals form of showing entry/exit labels.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/toRTLabs.ma

    r1070 r1072  
    2121     〈add ?? en id r, gen'〉) 〈en, gen〉.
    2222
     23lemma lookup_sigma : ∀tag,A,m. ∀i:(Σl:identifier tag. lookup tag A m l ≠ None ?).
     24  lookup tag A m i ≠ None ?.
     25#tag #A #m * #i #H @H
     26qed.
     27
    2328(* Add a statement to the graph, *without* updating the entry label. *)
    2429definition fill_in_statement : label → statement → internal_function → internal_function ≝
     
    2833                       (f_stacksize f) (add ?? (f_graph f) l s)
    2934                       (dp ?? (f_entry f) ?) (dp ?? (f_exit f) ?).
    30 @lookup_add_oblivious [ cases (f_entry f) | cases (f_exit f) ] //
     35@lookup_add_oblivious @lookup_sigma
    3136qed.
    3237
     
    3843                       (f_stacksize f) (add ?? (f_graph f) l s)
    3944                       (dp ?? l ?) (dp ?? (f_exit f) ?).
    40 [ %{s} @lookup_add_hit
    41 | @lookup_add_oblivious cases (f_exit f) //
     45[ >lookup_add_hit % #E destruct
     46| @lookup_add_oblivious @lookup_sigma
    4247] qed.
    4348
     
    5257                       (f_stacksize f) (add ?? (f_graph f) l s')
    5358                       (dp ?? l ?) (dp ?? (f_exit f) ?)).
    54 [ %{s'} @lookup_add_hit
    55 | @lookup_add_oblivious cases (f_exit f) //
     59[ >lookup_add_hit % #E destruct
     60| @lookup_add_oblivious @lookup_sigma
    5661] qed.
    57 (*
    58 (* Generate a fresh label and use it as a dangling entry point, to be filled in
    59    later with the loop head. *)
    60 definition add_loop_label_to_graph : internal_function → internal_function ≝
    61 λf.
    62   let 〈l,g〉 ≝ fresh … (f_labgen f) in
    63     (mk_internal_function g (f_reggen f)
    64                        (f_result f) (f_params f) (f_locals f)
    65                        (f_stacksize f) (f_graph f) l (f_exit f)).
    66 *)
     62
    6763definition fresh_reg : internal_function → typ → register × internal_function ≝
    6864λf,ty.
     
    296292OK ? f
    297293.
    298 % [2,4: @lookup_add_hit | *: skip ]
     294>lookup_add_hit % #E destruct
    299295qed.
    300296
Note: See TracChangeset for help on using the changeset viewer.