Changeset 726 for src/RTLabs/import.ma
 Timestamp:
 Mar 30, 2011, 6:47:35 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/import.ma
r710 r726 2 2 include "RTLabs/RTLabssem.ma". 3 3 4 definition new_reg : internal_function → re gister × internal_function≝5 λf. let 〈r, g〉 ≝ register_new (f_reggen f) in6 〈r, mk_internal_function (f_labgen f) g (f_sig f) (f_result f) (f_params f)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 7 (f_locals f) (f_stacksize f) (f_graph f) (f_entry f) (f_exit f)〉. 8 8 9 definition new_label : internal_function → label × internal_function≝10 λf. let 〈l, g〉 ≝ label_new (f_labgen f) in11 〈l, mk_internal_function g (f_reggen f) (f_sig f) (f_result f) (f_params f)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 12 (f_locals f) (f_stacksize f) (f_graph f) (f_entry f) (f_exit f)〉. 13 13 … … 17 17 (graph_add ? (f_graph f) l s) (f_entry f) (f_exit f). 18 18 19 let rec n_labels (n:nat) (g:label_generation) : Vector label n × label_generation≝19 let rec n_labels (n:nat) (g:label_generation) : res (Vector label n × label_generation) ≝ 20 20 match n with 21 [ O ⇒ 〈[[ ]], g〉22  S m ⇒ let 〈ls, g'〉 ≝ n_labels m g in23 let 〈l, g''〉 ≝ label_new g in24 〈l:::ls, g''〉21 [ 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 25 ]. 26 26 27 let rec n_regs (n:nat) (g:register_generation) : Vector label n × register_generation≝27 let rec n_regs (n:nat) (g:register_generation) : res (Vector label n × register_generation) ≝ 28 28 match n with 29 [ O ⇒ 〈[[ ]], g〉30  S m ⇒ let 〈ls, g'〉 ≝ n_regs m g in31 let 〈l, g''〉 ≝ register_new g in32 〈l:::ls, g''〉29 [ O ⇒ OK ? 〈[[ ]], g〉 30  S m ⇒ do 〈ls, g'〉 ← n_regs m g; 31 do 〈l, g''〉 ← register_new g; 32 OK ? 〈l:::ls, g''〉 33 33 ]. 34 34 … … 61 61 match m r with 62 62 [ Some r' ⇒ OK ? 〈m,〈g,r':::rs〉〉 63  None ⇒ let 〈r',g'〉 ≝ register_new g in63  None ⇒ do 〈r',g'〉 ← register_new g; 64 64 OK ? 〈λn. if eqb r n then Some ? r' else m n,〈g',r':::rs〉〉 65 65 ]) (OK ? 〈m,〈g,[[ ]]〉〉) rs; … … 88 88 let rmap ≝ λn. opt_to_res … (rmap3 n) in 89 89 let max_stmt ≝ foldr ?? (λp,m. max (\fst p) m) 0 (pf_graph pre_f) in 90 let 〈labels, gen〉 ≝ n_labels max_stmt label_gen_new in90 do 〈labels, gen〉 ← n_labels max_stmt label_gen_new; 91 91 let get_label ≝ λn. opt_to_res … (get_index_weak_v ?? labels n) in 92 92 do graph ← foldr ?? (λp,g0. do g ← g0;
Note: See TracChangeset
for help on using the changeset viewer.