Changeset 1056 for src/RTLabs
- Timestamp:
- Jul 5, 2011, 4:25:41 PM (8 years ago)
- Location:
- src/RTLabs
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTLabs/import.ma
r898 r1056 2 2 include "RTLabs/semantics.ma". 3 3 4 let rec n_idents (n:nat) (tag:String) (g:universe tag) : res (Vector (identifier tag) n × (universe tag)) ≝4 let rec n_idents (n:nat) (tag:String) (g:universe tag) : Vector (identifier tag) n × (universe tag) ≝ 5 5 match n with 6 [ O ⇒ OK ?〈[[ ]], g〉7 | S m ⇒ do 〈ls, g'〉 ← n_idents m tag g;8 do 〈l, g''〉 ← fresh ? g';9 OK ?〈l:::ls, g''〉6 [ O ⇒ 〈[[ ]], g〉 7 | S m ⇒ let 〈ls, g'〉 ≝ n_idents m tag g in 8 let 〈l, g''〉 ≝ fresh ? g' in 9 〈l:::ls, g''〉 10 10 ]. 11 11 … … 24 24 definition make_register : 25 25 (pre_register → option register) → pre_register → universe RegisterTag → 26 res ((nat → option register) × (universe RegisterTag) × register)≝26 (nat → option register) × (universe RegisterTag) × register ≝ 27 27 λm,reg,g. 28 28 match m reg with 29 [ Some r' ⇒ OK ?〈〈m,g〉,r'〉30 | None ⇒ do 〈r',g'〉 ← fresh ? g;31 OK ?〈〈λn. if eqb reg n then Some ? r' else m n,g'〉,r'〉29 [ Some r' ⇒ 〈〈m,g〉,r'〉 30 | None ⇒ let 〈r',g'〉 ≝ fresh ? g in 31 〈〈λn. if eqb reg n then Some ? r' else m n,g'〉,r'〉 32 32 ] 33 33 . … … 35 35 definition make_registers_list : 36 36 (nat → option register) → list (pre_register × typ) → universe RegisterTag → 37 res ((nat → option register) × (universe RegisterTag) × (list (register×typ))) ≝37 (nat → option register) × (universe RegisterTag) × (list (register×typ)) ≝ 38 38 λm,lrs,g. 39 foldr ?? (λrst,acc. do 〈acc',l〉 ← acc;40 let 〈rs,ty〉 ≝ rst in41 let 〈m,g〉 ≝ acc' in42 do 〈mg,rs'〉 ← make_register m rs g;43 OK ? 〈mg,〈rs',ty〉::l〉) (OK ? 〈〈m,g〉,[ ]〉)lrs.39 foldr ?? (λrst,acc. let 〈acc',l〉 ≝ acc in 40 let 〈rs,ty〉 ≝ rst in 41 let 〈m,g〉 ≝ acc' in 42 let 〈mg,rs'〉 ≝ make_register m rs g in 43 〈mg,〈rs',ty〉::l〉) 〈〈m,g〉,[ ]〉 lrs. 44 44 45 45 axiom MissingRegister : String. 46 46 axiom MissingLabel : String. 47 47 48 (* Doesn't check for identifier overflow, but don't really need to care here. *) 48 49 definition make_internal_function : pre_internal_function → res (fundef internal_function) ≝ 49 50 λpre_f. 50 51 let rgen0 ≝ new_universe RegisterTag in 51 do 〈rmapgen1, result〉 ←match pf_result pre_f with52 [ None ⇒ OK ?〈〈λ_.None ?, rgen0〉, None ?〉53 | Some rt ⇒ do 〈x,y〉 ← make_register (λ_.None ?) (\fst rt) rgen0; OK ?〈x,Some ? 〈y,\snd rt〉〉54 ];52 let 〈rmapgen1, result〉 ≝ match pf_result pre_f with 53 [ None ⇒ 〈〈λ_.None ?, rgen0〉, None ?〉 54 | Some rt ⇒ let 〈x,y〉 ≝ make_register (λ_.None ?) (\fst rt) rgen0 in 〈x,Some ? 〈y,\snd rt〉〉 55 ] in 55 56 let 〈rmap1, rgen1〉 ≝ rmapgen1 in 56 do 〈rmapgen2, params〉 ← make_registers_list rmap1 (pf_params pre_f) rgen1;57 let 〈rmapgen2, params〉 ≝ make_registers_list rmap1 (pf_params pre_f) rgen1 in 57 58 let 〈rmap2, rgen2〉 ≝ rmapgen2 in 58 do 〈rmapgen3, locals〉 ← make_registers_list rmap2 (pf_locals pre_f) rgen2;59 let 〈rmapgen3, locals〉 ≝ make_registers_list rmap2 (pf_locals pre_f) rgen2 in 59 60 let 〈rmap3, rgen3〉 ≝ rmapgen3 in 60 61 let rmap ≝ λn. opt_to_res … (msg MissingRegister) (rmap3 n) in 61 62 let max_stmt ≝ foldr ?? (λp,m. max (\fst p) m) 0 (pf_graph pre_f) in 62 do 〈labels, gen〉 ← n_idents (S max_stmt) ? (new_universe LabelTag);63 let 〈labels, gen〉 ≝ n_idents (S max_stmt) ? (new_universe LabelTag) in 63 64 let get_label ≝ λn. opt_to_res … (msg MissingLabel) (get_index_weak_v ?? labels n) in 64 65 do graph ← foldr ?? (λp:nat × ((pre_register → res register) → (nat → res label) → res statement).λg0. -
src/RTLabs/syntax.ma
r1051 r1056 13 13 | St_skip : label → statement 14 14 | St_cost : costlabel → label → statement 15 | St_const : register → c ast → label → statement15 | St_const : register → constant → label → statement 16 16 | St_op1 : unary_operation → register → register → label → statement 17 17 | St_op2 : binary_operation → register → register → register → label → statement
Note: See TracChangeset
for help on using the changeset viewer.