Changeset 736 for src/RTLabs/import.ma
 Timestamp:
 Apr 4, 2011, 5:13:08 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/import.ma
r727 r736 2 2 include "RTLabs/RTLabssem.ma". 3 3 4 definition new_reg : internal_function → res (register × internal_function) ≝ 5 λf. do 〈r, g〉 ← register_new (f_reggen f); 6 OK ? 〈r, mk_internal_function (f_labgen f) g (f_sig f) (f_result f) (f_params f) 7 (f_locals f) (f_stacksize f) (f_graph f) (f_entry f) (f_exit f)〉. 8 9 definition new_label : internal_function → res (label × internal_function) ≝ 10 λf. do 〈l, g〉 ← label_new (f_labgen f); 11 OK ? 〈l, mk_internal_function g (f_reggen f) (f_sig f) (f_result f) (f_params f) 12 (f_locals f) (f_stacksize f) (f_graph f) (f_entry f) (f_exit f)〉. 13 14 definition new_statement : internal_function → label → statement → internal_function ≝ 15 λf,l,s. mk_internal_function (f_labgen f) (f_reggen f) (f_sig f) (f_result f) (f_params f) 16 (f_locals f) (f_stacksize f) 17 (graph_add ? (f_graph f) l s) (f_entry f) (f_exit f). 18 19 let rec n_labels (n:nat) (g:label_generation) : res (Vector label n × label_generation) ≝ 4 let rec n_idents (n:nat) (tag:String) (g:Universe tag) : res (Vector (Identifier tag) n × (Universe tag)) ≝ 20 5 match n with 21 6 [ O ⇒ OK ? 〈[[ ]], g〉 22  S m ⇒ do 〈ls, g'〉 ← n_labels m g; 23 do 〈l, g''〉 ← label_new g'; 24 OK ? 〈l:::ls, g''〉 25 ]. 26 27 let rec n_regs (n:nat) (g:register_generation) : res (Vector label n × register_generation) ≝ 28 match n with 29 [ O ⇒ OK ? 〈[[ ]], g〉 30  S m ⇒ do 〈ls, g'〉 ← n_regs m g; 31 do 〈l, g''〉 ← register_new g'; 7  S m ⇒ do 〈ls, g'〉 ← n_idents m tag g; 8 do 〈l, g''〉 ← fresh ? g'; 32 9 OK ? 〈l:::ls, g''〉 33 10 ]. … … 41 18 ; pf_locals : list pre_registers 42 19 ; pf_stacksize : nat 43 ; pf_graph : list (nat × ((nat → res label) → (nat → res register) → res statement))20 ; pf_graph : list (nat × ((nat → res register) → (nat → res label) → res statement)) 44 21 ; pf_entry : nat 45 22 ; pf_exit : nat … … 52 29 53 30 definition make_registers : 54 (nat → option register) → pre_registers → register_generation→55 res ((nat → option register) × register_generation× registers) ≝31 (nat → option register) → pre_registers → Universe RegisterTag → 32 res ((nat → option register) × (Universe RegisterTag) × registers) ≝ 56 33 λm,rs0,g. 57 34 match rs0 with [ dp n rs ⇒ … … 61 38 match m r with 62 39 [ Some r' ⇒ OK ? 〈m,〈g,r':::rs〉〉 63  None ⇒ do 〈r',g'〉 ← register_newg;40  None ⇒ do 〈r',g'〉 ← fresh ? g; 64 41 OK ? 〈λn. if eqb r n then Some ? r' else m n,〈g',r':::rs〉〉 65 42 ]) (OK ? 〈m,〈g,[[ ]]〉〉) rs; … … 69 46 70 47 definition make_registers_list : 71 (nat → option register) → list pre_registers → register_generation→72 res ((nat → option register) × register_generation× (list registers)) ≝48 (nat → option register) → list pre_registers → Universe RegisterTag → 49 res ((nat → option register) × (Universe RegisterTag) × (list registers)) ≝ 73 50 λm,lrs,g. 74 51 foldr ?? (λrs,acc. do 〈acc',l〉 ← acc; … … 79 56 definition make_internal_function : pre_internal_function → res (fundef internal_function) ≝ 80 57 λpre_f. 81 let rgen0 ≝ register_gen_newin58 let rgen0 ≝ new_universe RegisterTag in 82 59 do 〈rmapgen1, result〉 ← make_registers (λ_.None ?) (pf_result pre_f) rgen0; 83 60 let 〈rmap1, rgen1〉 ≝ rmapgen1 in … … 88 65 let rmap ≝ λn. opt_to_res … (rmap3 n) in 89 66 let max_stmt ≝ foldr ?? (λp,m. max (\fst p) m) 0 (pf_graph pre_f) in 90 do 〈labels, gen〉 ← n_ labels (S max_stmt) label_gen_new;67 do 〈labels, gen〉 ← n_idents (S max_stmt) ? (new_universe LabelTag); 91 68 let get_label ≝ λn. opt_to_res … (get_index_weak_v ?? labels n) in 92 69 do graph ← foldr ?? (λp,g0. do g ← g0; … … 94 71 do l' ← get_label l; 95 72 do s' ← s rmap get_label; 96 OK ? ( graph_add ? g l' s')) (OK ? (empty_graph?)) (pf_graph pre_f);73 OK ? (add ?? g l' s')) (OK ? (empty_map ??)) (pf_graph pre_f); 97 74 do entry ← get_label (pf_entry pre_f); 98 75 do exit ← get_label (pf_exit pre_f);
Note: See TracChangeset
for help on using the changeset viewer.