source: src/RTLabs/import.ma @ 736

Last change on this file since 736 was 736, checked in by campbell, 9 years ago

Extra type safety for identifiers.

File size: 7.6 KB
RevLine 
[710]1
2include "RTLabs/RTLabs-sem.ma".
3
[736]4let rec n_idents (n:nat) (tag:String) (g:Universe tag) : res (Vector (Identifier tag) n × (Universe tag)) ≝
[710]5match 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
12definition pre_registers ≝ Sig nat (Vector nat).
13
14record 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 *)
25definition pf_stacksize ≝ λp.match p with [ mk_pre_internal_function _ _ _ _ s _ _ _ ⇒ s ].
26definition pf_graph ≝ λp.match p with [ mk_pre_internal_function _ _ _ _ _ g _ _ ⇒ g ].
27definition pf_entry ≝ λp.match p with [ mk_pre_internal_function _ _ _ _ _ _ e _ ⇒ e ].
28definition pf_exit ≝ λp.match p with [ mk_pre_internal_function _ _ _ _ _ _ _ e ⇒ e ].
29
30definition make_registers :
[736]31  (nat → option register) → pre_registers → Universe RegisterTag →
32  res ((nat → option register) × (Universe RegisterTag) × registers) ≝
[710]33λm,rs0,g.
34match 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
47definition 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.
51foldr ?? (λ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]56definition 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
89definition make_regs : (nat → res register) → pre_registers → res registers ≝
90λm,p.
91match 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
100definition 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 *)
104let 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) ≝
105match 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
112definition 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]115let rec make_St_skip l ≝ λr:nat → res register.λf:nat → res label. do l' ← f l; OK ? (St_skip l').
116let rec make_St_cost cl l ≝ λr:nat → res register.λf:nat → res label. do l' ← f l; OK ? (St_cost cl l').
117let 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').
118let 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').
119let 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]120let 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').
121let 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]122let 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').
123let 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').
124let 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).
125let 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).
126let 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').
127let 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').
128let 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').
129let 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').
130let 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
Note: See TracBrowser for help on using the repository browser.