source: src/RTLabs/import.ma @ 748

Last change on this file since 748 was 738, checked in by campbell, 10 years ago

Use lower case names for identifiers for consistency with CompCert? derived code
and to prevent confusion with the back-end equivalents until they're all merged.

File size: 7.6 KB
Line 
1
2include "RTLabs/RTLabs-sem.ma".
3
4let rec n_idents (n:nat) (tag:String) (g:universe tag) : res (Vector (identifier tag) n × (universe tag)) ≝
5match 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''〉
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
20; pf_graph     : list (nat × ((nat → res register) → (nat → res label) → res statement))
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 :
31  (nat → option register) → pre_registers → universe RegisterTag →
32  res ((nat → option register) × (universe RegisterTag) × registers) ≝
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〉〉
40                  | None ⇒ do 〈r',g'〉 ← fresh ? g;
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 :
48  (nat → option register) → list pre_registers → universe RegisterTag →
49  res ((nat → option register) × (universe RegisterTag) × (list registers)) ≝
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
56definition make_internal_function : pre_internal_function → res (fundef internal_function) ≝
57λpre_f.
58  let rgen0 ≝ new_universe RegisterTag in
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
67  do 〈labels, gen〉 ← n_idents (S max_stmt) ? (new_universe LabelTag);
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;
73                              OK ? (add ?? g l' s')) (OK ? (empty_map ??)) (pf_graph pre_f);
74  do entry ← get_label (pf_entry pre_f);
75  do exit ← get_label (pf_exit pre_f);
76  OK ? (Internal ? (mk_internal_function
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
87         )).
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
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
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').
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').
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.