[710] | 1 | |
---|
[762] | 2 | include "RTLabs/semantics.ma". |
---|
[710] | 3 | |
---|
[1056] | 4 | let rec n_idents (n:nat) (tag:String) (g:universe tag) : Vector (identifier tag) n × (universe tag) ≝ |
---|
[710] | 5 | match n with |
---|
[1056] | 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''〉 |
---|
[710] | 10 | ]. |
---|
| 11 | |
---|
[750] | 12 | definition pre_register ≝ nat. |
---|
[710] | 13 | |
---|
| 14 | record pre_internal_function : Type[0] ≝ |
---|
[898] | 15 | { pf_result : option (pre_register × typ) |
---|
| 16 | ; pf_params : list (pre_register × typ) |
---|
| 17 | ; pf_locals : list (pre_register × typ) |
---|
[710] | 18 | ; pf_stacksize : nat |
---|
[750] | 19 | ; pf_graph : list (nat × ((pre_register → res register) → (nat → res label) → res statement)) |
---|
[710] | 20 | ; pf_entry : nat |
---|
| 21 | ; pf_exit : nat |
---|
| 22 | }. |
---|
| 23 | |
---|
[750] | 24 | definition make_register : |
---|
| 25 | (pre_register → option register) → pre_register → universe RegisterTag → |
---|
[1056] | 26 | (nat → option register) × (universe RegisterTag) × register ≝ |
---|
[750] | 27 | λm,reg,g. |
---|
| 28 | match m reg with |
---|
[1056] | 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'〉 |
---|
[750] | 32 | ] |
---|
| 33 | . |
---|
[710] | 34 | |
---|
| 35 | definition make_registers_list : |
---|
[898] | 36 | (nat → option register) → list (pre_register × typ) → universe RegisterTag → |
---|
[1056] | 37 | (nat → option register) × (universe RegisterTag) × (list (register×typ)) ≝ |
---|
[710] | 38 | λm,lrs,g. |
---|
[1056] | 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. |
---|
[710] | 44 | |
---|
[797] | 45 | axiom MissingRegister : String. |
---|
| 46 | axiom MissingLabel : String. |
---|
| 47 | |
---|
[1056] | 48 | (* Doesn't check for identifier overflow, but don't really need to care here. *) |
---|
[727] | 49 | definition make_internal_function : pre_internal_function → res (fundef internal_function) ≝ |
---|
[710] | 50 | λpre_f. |
---|
[736] | 51 | let rgen0 ≝ new_universe RegisterTag in |
---|
[1056] | 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 |
---|
[710] | 56 | let 〈rmap1, rgen1〉 ≝ rmapgen1 in |
---|
[1056] | 57 | let 〈rmapgen2, params〉 ≝ make_registers_list rmap1 (pf_params pre_f) rgen1 in |
---|
[710] | 58 | let 〈rmap2, rgen2〉 ≝ rmapgen2 in |
---|
[1056] | 59 | let 〈rmapgen3, locals〉 ≝ make_registers_list rmap2 (pf_locals pre_f) rgen2 in |
---|
[710] | 60 | let 〈rmap3, rgen3〉 ≝ rmapgen3 in |
---|
[898] | 61 | let rmap ≝ λn. opt_to_res … (msg MissingRegister) (rmap3 n) in |
---|
[710] | 62 | let max_stmt ≝ foldr ?? (λp,m. max (\fst p) m) 0 (pf_graph pre_f) in |
---|
[1056] | 63 | let 〈labels, gen〉 ≝ n_idents (S max_stmt) ? (new_universe LabelTag) in |
---|
[797] | 64 | let get_label ≝ λn. opt_to_res … (msg MissingLabel) (get_index_weak_v ?? labels n) in |
---|
[882] | 65 | do graph ← foldr ?? (λp:nat × ((pre_register → res register) → (nat → res label) → res statement).λg0. |
---|
| 66 | do g ← g0; |
---|
| 67 | let 〈l,s〉 ≝ p in |
---|
| 68 | do l' ← get_label l; |
---|
| 69 | do s' ← s rmap get_label; |
---|
| 70 | OK ? (add ?? g l' s')) (OK ? (empty_map ??)) (pf_graph pre_f); |
---|
[710] | 71 | do entry ← get_label (pf_entry pre_f); |
---|
| 72 | do exit ← get_label (pf_exit pre_f); |
---|
[1072] | 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 |
---|
[710] | 83 | gen |
---|
[898] | 84 | rgen3 |
---|
[710] | 85 | result |
---|
| 86 | params |
---|
| 87 | locals |
---|
| 88 | (pf_stacksize pre_f) |
---|
| 89 | graph |
---|
[1072] | 90 | (dp ?? entry p) |
---|
| 91 | (dp ?? exit q) |
---|
| 92 | ))) |
---|
| 93 | . |
---|
| 94 | % #E destruct (E) |
---|
| 95 | qed. |
---|
[710] | 96 | |
---|
[750] | 97 | definition make_reg_list : (nat → res register) → list pre_register → res (list register) ≝ |
---|
| 98 | λm,ps. foldr ?? (λp,rs0. do rs ← rs0; do r ← m p; OK ? (r::rs)) (OK ? [ ]) ps. |
---|
[710] | 99 | |
---|
[727] | 100 | (* XXX move somewhere sensible *) |
---|
| 101 | let rec mmap_vec (A:Type[0]) (B:Type[0]) (f:A → res B) (n:nat) (v:Vector A n) on v : res (Vector B n) ≝ |
---|
| 102 | match v with |
---|
| 103 | [ VEmpty ⇒ OK ? (VEmpty …) |
---|
| 104 | | VCons m hd tl ⇒ do hd' ← f hd; |
---|
| 105 | do tl' ← mmap_vec A B f m tl; |
---|
| 106 | OK ? (hd':::tl') |
---|
| 107 | ]. |
---|
| 108 | |
---|
[750] | 109 | definition make_opt_reg : (pre_register → res register) → option pre_register → res (option register) ≝ |
---|
| 110 | λm,o. match o with [ None ⇒ OK ? (None ?) | Some r ⇒ do r' ← m r; OK ? (Some ? r') ]. |
---|
| 111 | |
---|
[710] | 112 | let rec make_St_skip l ≝ λr:nat → res register.λf:nat → res label. do l' ← f l; OK ? (St_skip l'). |
---|
| 113 | let rec make_St_cost cl l ≝ λr:nat → res register.λf:nat → res label. do l' ← f l; OK ? (St_cost cl l'). |
---|
[750] | 114 | let rec make_St_const rs cst l ≝ λr:nat → res register.λf:nat → res label. do rs' ← r rs; do l' ← f l; OK ? (St_const rs' cst l'). |
---|
| 115 | let rec make_St_op1 op dst src l ≝ λr:nat → res register.λf:nat → res label. do dst' ← r dst; do src' ← r src; do l' ← f l; OK ? (St_op1 op dst' src' l'). |
---|
| 116 | let rec make_St_op2 op dst src1 src2 l ≝ λr:nat → res register.λf:nat → res label. do dst' ← r dst; do src1' ← r src1; do src2' ← r src2; do l' ← f l; OK ? (St_op2 op dst' src1' src2' l'). |
---|
[898] | 117 | let rec make_St_load chunk addr dst l ≝ λr:nat → res register.λf:nat → res label. do addr' ← r addr; do dst' ← r dst; do l' ← f l; OK ? (St_load chunk addr' dst' l'). |
---|
| 118 | let rec make_St_store chunk addr src l ≝ λr:nat → res register.λf:nat → res label. do addr' ← r addr; do src' ← r src; do l' ← f l; OK ? (St_store chunk addr' src' l'). |
---|
[816] | 119 | let rec make_St_call_id id args dst l ≝ λr:nat → res register.λf:nat → res label. do args' ← make_reg_list r args; do dst' ← make_opt_reg r dst; do l' ← f l; OK ? (St_call_id id args' dst' l'). |
---|
| 120 | let rec make_St_call_ptr frs args dst l ≝ λr:nat → res register.λf:nat → res label. do frs' ← r frs; do args' ← make_reg_list r args; do dst' ← make_opt_reg r dst; do l' ← f l; OK ? (St_call_ptr frs' args' dst' l'). |
---|
| 121 | let rec make_St_tailcall_id id args ≝ λr:nat → res register.λf:nat → res label. do args' ← make_reg_list r args; OK statement (St_tailcall_id id args'). |
---|
| 122 | let rec make_St_tailcall_ptr frs args ≝ λr:nat → res register.λf:nat → res label. do frs' ← r frs; do args' ← make_reg_list r args; OK statement (St_tailcall_ptr frs' args'). |
---|
[898] | 123 | let rec make_St_cond src ltrue lfalse ≝ λr:nat → res register.λf:nat → res label. do src' ← r src; do ltrue' ← f ltrue; do lfalse' ← f lfalse; OK ? (St_cond src' ltrue' lfalse'). |
---|
[750] | 124 | let rec make_St_jumptable rs ls ≝ λr:nat → res register.λf:nat → res label. do rs' ← r rs; do ls' ← foldr ?? (λl,ls0. do ls ← ls0; do l' ← f l; OK ? (l'::ls)) (OK ? [ ]) ls; OK ? (St_jumptable rs' ls'). |
---|
[765] | 125 | definition make_St_return ≝ λr:nat → res register.λf:nat → res label. OK statement St_return. |
---|
[710] | 126 | |
---|