Changeset 1072


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

Use not equals form of showing entry/exit labels.

Location:
src
Files:
3 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
  • src/RTLabs/import.ma

    r1056 r1072  
    7171  do entry ← get_label (pf_entry pre_f);
    7272  do exit ← get_label (pf_exit pre_f);
    73   OK ? (Internal ? (mk_internal_function
     73  (* We could figure out that entry and exit are in the graph, but why bother
     74     for some testing code? *)
     75  match lookup … graph entry return λx. (x ≠ None ? → ?) → ? with
     76  [ None ⇒ λ_. Error ? (msg MissingLabel)
     77  | Some _ ⇒
     78      match lookup … graph exit return λx. (? → x ≠ None ? → ?) → ? with
     79      [ None ⇒ λ_. Error ? (msg MissingLabel)
     80      | Some _ ⇒ λx. x ??
     81      ]
     82  ] (λp,q. OK ? (Internal ? (mk_internal_function
    7483         gen
    7584         rgen3
     
    7988         (pf_stacksize pre_f)
    8089         graph
    81          entry
    82          exit
    83          )).
     90         (dp ?? entry p)
     91         (dp ?? exit q)
     92         )))
     93   .
     94% #E destruct (E)
     95qed.
    8496
    8597definition make_reg_list : (nat → res register) → list pre_register → res (list register) ≝
  • src/common/Identifiers.ma

    r1070 r1072  
    113113
    114114lemma lookup_add_oblivious : ∀tag,A,m,i,j,a.
    115   (∃v. lookup tag A m i = Some ? v) →
    116   ∃v. lookup tag A (add tag A m j a) i = Some ? v.
    117 #tag #A #m #i #j #a * #v #H
     115  (lookup tag A m i ≠ None ?) →
     116  lookup tag A (add tag A m j a) i ≠ None ?.
     117#tag #A #m #i #j #a #H
    118118lapply (lookup_add_miss … m i j a)
    119119@eq_identifier_elim
    120 [ #E #_ %{a} >E @lookup_add_hit
    121 | #_ #H' %{v} <H @H' %
     120[ #E #_ >E >lookup_add_hit % #N destruct
     121| #_ #H' >H' //
    122122] qed.
    123123
Note: See TracChangeset for help on using the changeset viewer.