Changeset 1072 for src/RTLabs/import.ma


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

Use not equals form of showing entry/exit labels.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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) ≝
Note: See TracChangeset for help on using the changeset viewer.