[710] | 1 | |
---|
| 2 | include "RTLabs/RTLabs-sem.ma". |
---|
| 3 | |
---|
[736] | 4 | let rec n_idents (n:nat) (tag:String) (g:Universe tag) : res (Vector (Identifier tag) n × (Universe tag)) ≝ |
---|
[710] | 5 | match n with |
---|
[726] | 6 | [ O ⇒ OK ? 〈[[ ]], g〉 |
---|
[736] | 7 | | S m ⇒ do 〈ls, g'〉 ← n_idents m tag g; |
---|
| 8 | do 〈l, g''〉 ← fresh ? g'; |
---|
[726] | 9 | OK ? 〈l:::ls, g''〉 |
---|
[710] | 10 | ]. |
---|
| 11 | |
---|
| 12 | definition pre_registers ≝ Sig nat (Vector nat). |
---|
| 13 | |
---|
| 14 | record pre_internal_function : Type[0] ≝ |
---|
| 15 | { pf_sig : signature |
---|
| 16 | ; pf_result : pre_registers |
---|
| 17 | ; pf_params : list pre_registers |
---|
| 18 | ; pf_locals : list pre_registers |
---|
| 19 | ; pf_stacksize : nat |
---|
[736] | 20 | ; pf_graph : list (nat × ((nat → res register) → (nat → res label) → res statement)) |
---|
[710] | 21 | ; pf_entry : nat |
---|
| 22 | ; pf_exit : nat |
---|
| 23 | }. |
---|
| 24 | (* XXX projection generation with nat broken *) |
---|
| 25 | definition pf_stacksize ≝ λp.match p with [ mk_pre_internal_function _ _ _ _ s _ _ _ ⇒ s ]. |
---|
| 26 | definition pf_graph ≝ λp.match p with [ mk_pre_internal_function _ _ _ _ _ g _ _ ⇒ g ]. |
---|
| 27 | definition pf_entry ≝ λp.match p with [ mk_pre_internal_function _ _ _ _ _ _ e _ ⇒ e ]. |
---|
| 28 | definition pf_exit ≝ λp.match p with [ mk_pre_internal_function _ _ _ _ _ _ _ e ⇒ e ]. |
---|
| 29 | |
---|
| 30 | definition make_registers : |
---|
[736] | 31 | (nat → option register) → pre_registers → Universe RegisterTag → |
---|
| 32 | res ((nat → option register) × (Universe RegisterTag) × registers) ≝ |
---|
[710] | 33 | λm,rs0,g. |
---|
| 34 | match rs0 with [ dp n rs ⇒ |
---|
| 35 | do 〈m,grs〉 ← fold_right_i ??? (λn,r,mr. |
---|
| 36 | do 〈m,grs〉 ← mr; |
---|
| 37 | let 〈g,rs〉 ≝ grs in |
---|
| 38 | match m r with |
---|
| 39 | [ Some r' ⇒ OK ? 〈m,〈g,r':::rs〉〉 |
---|
[736] | 40 | | None ⇒ do 〈r',g'〉 ← fresh ? g; |
---|
[710] | 41 | OK ? 〈λn. if eqb r n then Some ? r' else m n,〈g',r':::rs〉〉 |
---|
| 42 | ]) (OK ? 〈m,〈g,[[ ]]〉〉) rs; |
---|
| 43 | let 〈g',rs'〉 ≝ grs in |
---|
| 44 | OK ? 〈〈m,g'〉,dp ?? n rs'〉 |
---|
| 45 | ]. |
---|
| 46 | |
---|
| 47 | definition make_registers_list : |
---|
[736] | 48 | (nat → option register) → list pre_registers → Universe RegisterTag → |
---|
| 49 | res ((nat → option register) × (Universe RegisterTag) × (list registers)) ≝ |
---|
[710] | 50 | λm,lrs,g. |
---|
| 51 | foldr ?? (λrs,acc. do 〈acc',l〉 ← acc; |
---|
| 52 | let 〈m,g〉 ≝ acc' in |
---|
| 53 | do 〈mg,rs'〉 ← make_registers m rs g; |
---|
| 54 | OK ? 〈mg,rs'::l〉) (OK ? 〈〈m,g〉,[ ]〉) lrs. |
---|
| 55 | |
---|
[727] | 56 | definition make_internal_function : pre_internal_function → res (fundef internal_function) ≝ |
---|
[710] | 57 | λpre_f. |
---|
[736] | 58 | let rgen0 ≝ new_universe RegisterTag in |
---|
[710] | 59 | do 〈rmapgen1, result〉 ← make_registers (λ_.None ?) (pf_result pre_f) rgen0; |
---|
| 60 | let 〈rmap1, rgen1〉 ≝ rmapgen1 in |
---|
| 61 | do 〈rmapgen2, params〉 ← make_registers_list rmap1 (pf_params pre_f) rgen1; |
---|
| 62 | let 〈rmap2, rgen2〉 ≝ rmapgen2 in |
---|
| 63 | do 〈rmapgen3, locals〉 ← make_registers_list rmap2 (pf_locals pre_f) rgen2; |
---|
| 64 | let 〈rmap3, rgen3〉 ≝ rmapgen3 in |
---|
| 65 | let rmap ≝ λn. opt_to_res … (rmap3 n) in |
---|
| 66 | let max_stmt ≝ foldr ?? (λp,m. max (\fst p) m) 0 (pf_graph pre_f) in |
---|
[736] | 67 | do 〈labels, gen〉 ← n_idents (S max_stmt) ? (new_universe LabelTag); |
---|
[710] | 68 | let get_label ≝ λn. opt_to_res … (get_index_weak_v ?? labels n) in |
---|
| 69 | do graph ← foldr ?? (λp,g0. do g ← g0; |
---|
| 70 | let 〈l,s〉 ≝ p in |
---|
| 71 | do l' ← get_label l; |
---|
| 72 | do s' ← s rmap get_label; |
---|
[736] | 73 | OK ? (add ?? g l' s')) (OK ? (empty_map ??)) (pf_graph pre_f); |
---|
[710] | 74 | do entry ← get_label (pf_entry pre_f); |
---|
| 75 | do exit ← get_label (pf_exit pre_f); |
---|
[727] | 76 | OK ? (Internal ? (mk_internal_function |
---|
[710] | 77 | gen |
---|
| 78 | rgen3 |
---|
| 79 | (pf_sig pre_f) |
---|
| 80 | result |
---|
| 81 | params |
---|
| 82 | locals |
---|
| 83 | (pf_stacksize pre_f) |
---|
| 84 | graph |
---|
| 85 | entry |
---|
| 86 | exit |
---|
[727] | 87 | )). |
---|
[710] | 88 | |
---|
| 89 | definition make_regs : (nat → res register) → pre_registers → res registers ≝ |
---|
| 90 | λm,p. |
---|
| 91 | match p with |
---|
| 92 | [ dp n ps ⇒ |
---|
| 93 | do rs ← fold_right_i ??? (λn,r,rs0. |
---|
| 94 | do rs ← rs0; |
---|
| 95 | do r' ← m r; |
---|
| 96 | OK ? (r':::rs)) (OK ? [[ ]]) ps; |
---|
| 97 | OK ? (dp ?? n rs) |
---|
| 98 | ]. |
---|
| 99 | |
---|
| 100 | definition make_regs_list : (nat → res register) → list pre_registers → res (list registers) ≝ |
---|
| 101 | λm,ps. foldr ?? (λp,rs0. do rs ← rs0; do r ← make_regs m p; OK ? (r::rs)) (OK ? [ ]) ps. |
---|
| 102 | |
---|
[727] | 103 | (* XXX move somewhere sensible *) |
---|
| 104 | 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) ≝ |
---|
| 105 | match v with |
---|
| 106 | [ VEmpty ⇒ OK ? (VEmpty …) |
---|
| 107 | | VCons m hd tl ⇒ do hd' ← f hd; |
---|
| 108 | do tl' ← mmap_vec A B f m tl; |
---|
| 109 | OK ? (hd':::tl') |
---|
| 110 | ]. |
---|
| 111 | |
---|
| 112 | definition make_addr : (nat → res register) → ∀m:addressing. Vector pre_registers (addr_mode_args m) → res (addr m) ≝ |
---|
| 113 | λmp,m. mmap_vec ?? (make_regs mp) ?. |
---|
| 114 | |
---|
[710] | 115 | let rec make_St_skip l ≝ λr:nat → res register.λf:nat → res label. do l' ← f l; OK ? (St_skip l'). |
---|
| 116 | let rec make_St_cost cl l ≝ λr:nat → res register.λf:nat → res label. do l' ← f l; OK ? (St_cost cl l'). |
---|
| 117 | let rec make_St_const rs cst l ≝ λr:nat → res register.λf:nat → res label. do rs' ← make_regs r rs; do l' ← f l; OK ? (St_const rs' cst l'). |
---|
| 118 | let rec make_St_op1 op dst src l ≝ λr:nat → res register.λf:nat → res label. do dst' ← make_regs r dst; do src' ← make_regs r src; do l' ← f l; OK ? (St_op1 op dst' src' l'). |
---|
| 119 | let rec make_St_op2 op dst src1 src2 l ≝ λr:nat → res register.λf:nat → res label. do dst' ← make_regs r dst; do src1' ← make_regs r src1; do src2' ← make_regs r src2; do l' ← f l; OK ? (St_op2 op dst' src1' src2' l'). |
---|
[727] | 120 | let rec make_St_load chunk mode args dst l ≝ λr:nat → res register.λf:nat → res label. do dst' ← make_regs r dst; do l' ← f l; do args' ← make_addr r ? args; OK ? (St_load chunk mode args' dst' l'). |
---|
| 121 | let rec make_St_store chunk mode args src l ≝ λr:nat → res register.λf:nat → res label. do src' ← make_regs r src; do l' ← f l; do args' ← make_addr r ? args; OK ? (St_store chunk mode args' src' l'). |
---|
[710] | 122 | let rec make_St_call_id id args dst sig l ≝ λr:nat → res register.λf:nat → res label. do args' ← make_regs_list r args; do dst' ← make_regs r dst; do l' ← f l; OK ? (St_call_id id args' dst' sig l'). |
---|
| 123 | let rec make_St_call_ptr frs args dst sig l ≝ λr:nat → res register.λf:nat → res label. do frs' ← make_regs r frs; do args' ← make_regs_list r args; do dst' ← make_regs r dst; do l' ← f l; OK ? (St_call_ptr frs' args' dst' sig l'). |
---|
| 124 | let rec make_St_tailcall_id id args sig ≝ λr:nat → res register.λf:nat → res label. do args' ← make_regs_list r args; OK statement (St_tailcall_id id args' sig). |
---|
| 125 | let rec make_St_tailcall_ptr frs args sig ≝ λr:nat → res register.λf:nat → res label. do frs' ← make_regs r frs; do args' ← make_regs_list r args; OK statement (St_tailcall_ptr frs' args' sig). |
---|
| 126 | let rec make_St_condcst cst ltrue lfalse ≝ λr:nat → res register.λf:nat → res label. do ltrue' ← f ltrue; do lfalse' ← f lfalse; OK ? (St_condcst cst ltrue' lfalse'). |
---|
| 127 | let rec make_St_cond1 op src ltrue lfalse ≝ λr:nat → res register.λf:nat → res label. do src' ← make_regs r src; do ltrue' ← f ltrue; do lfalse' ← f lfalse; OK ? (St_cond1 op src' ltrue' lfalse'). |
---|
| 128 | let rec make_St_cond2 op src1 src2 ltrue lfalse ≝ λr:nat → res register.λf:nat → res label. do src1' ← make_regs r src1; do src2' ← make_regs r src2; do ltrue' ← f ltrue; do lfalse' ← f lfalse; OK ? (St_cond2 op src1' src2' ltrue' lfalse'). |
---|
| 129 | let rec make_St_jumptable rs ls ≝ λr:nat → res register.λf:nat → res label. do rs' ← make_regs r rs; do ls' ← foldr ?? (λl,ls0. do ls ← ls0; do l' ← f l; OK ? (l'::ls)) (OK ? [ ]) ls; OK ? (St_jumptable rs' ls'). |
---|
| 130 | let rec make_St_return src ≝ λr:nat → res register.λf:nat → res label. do src' ← make_regs r src; OK statement (St_return src'). |
---|
| 131 | |
---|