Changeset 882 for src/RTLabs/import.ma
- Timestamp:
- Jun 3, 2011, 5:35:32 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTLabs/import.ma
r878 r882 65 65 do 〈labels, gen〉 ← n_idents (S max_stmt) ? (new_universe LabelTag); 66 66 let get_label ≝ λn. opt_to_res … (msg MissingLabel) (get_index_weak_v ?? labels n) in 67 do graph ← foldr ?? (λp,g0. do g ← g0; 68 let 〈l,s〉 ≝ p in 69 do l' ← get_label l; 70 do s' ← s rmap get_label; 71 OK ? (add ?? g l' s')) (OK ? (empty_map ??)) (pf_graph pre_f); 67 do graph ← foldr ?? (λp:nat × ((pre_register → res register) → (nat → res label) → res statement).λg0. 68 do g ← g0; 69 let 〈l,s〉 ≝ p in 70 do l' ← get_label l; 71 do s' ← s rmap get_label; 72 OK ? (add ?? g l' s')) (OK ? (empty_map ??)) (pf_graph pre_f); 72 73 do entry ← get_label (pf_entry pre_f); 73 74 do exit ← get_label (pf_exit pre_f);
Note: See TracChangeset
for help on using the changeset viewer.