source: src/RTLabs/import.ma @ 750

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

Track some of the changes to the prototype in RTLabs.

Just one register in each place now, f_ptrs is present but not checked.
The changes to memory quantities have been glossed over for now.
A new difference from the prototype: return registers are optional.

File size: 7.3 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_register ≝ nat.
13
14record pre_internal_function : Type[0] ≝
15{ pf_sig       : signature
16; pf_result    : option pre_register
17; pf_params    : list pre_register
18; pf_locals    : list pre_register
19; pf_ptrs      : list pre_register
20; pf_stacksize : nat
21; pf_graph     : list (nat × ((pre_register → res register) → (nat → res label) → res statement))
22; pf_entry     : nat
23; pf_exit      : nat
24}.
25(* XXX projection generation with nat broken *)
26definition pf_stacksize ≝ λp.match p with [ mk_pre_internal_function _ _ _ _ _ s _ _ _ ⇒ s ].
27definition pf_graph ≝ λp.match p with [ mk_pre_internal_function _ _ _ _ _ _ g _ _ ⇒ g ].
28definition pf_entry ≝ λp.match p with [ mk_pre_internal_function _ _ _ _ _ _ _ e _ ⇒ e ].
29definition pf_exit ≝ λp.match p with [ mk_pre_internal_function _ _ _ _ _ _ _ _ e ⇒ e ].
30
31definition make_register :
32  (pre_register → option register) → pre_register → universe RegisterTag →
33  res ((nat → option register) × (universe RegisterTag) × register) ≝
34λm,reg,g.
35  match m reg with
36  [ Some r' ⇒ OK ? 〈〈m,g〉,r'〉
37  | None ⇒ do 〈r',g'〉 ← fresh ? g;
38           OK ? 〈〈λn. if eqb reg n then Some ? r' else m n,g'〉,r'〉
39  ]
40.
41
42definition make_registers_list :
43  (nat → option register) → list pre_register → universe RegisterTag →
44  res ((nat → option register) × (universe RegisterTag) × (list register)) ≝
45λm,lrs,g.
46foldr ?? (λrs,acc. do 〈acc',l〉 ← acc;
47                   let 〈m,g〉 ≝ acc' in
48                   do 〈mg,rs'〉 ← make_register m rs g;
49                   OK ? 〈mg,rs'::l〉) (OK ? 〈〈m,g〉,[ ]〉) lrs.
50
51definition make_internal_function : pre_internal_function → res (fundef internal_function) ≝
52λpre_f.
53  let rgen0 ≝ new_universe RegisterTag in
54  do 〈rmapgen1, result〉 ← match pf_result pre_f with
55                          [ None ⇒ OK ? 〈〈λ_.None ?, rgen0〉, None ?〉
56                          | Some r ⇒ do 〈x,y〉 ← make_register (λ_.None ?) r rgen0; OK ? 〈x,Some ? y〉
57                          ];
58  let 〈rmap1, rgen1〉 ≝ rmapgen1 in
59  do 〈rmapgen2, params〉 ← make_registers_list rmap1 (pf_params pre_f) rgen1;
60  let 〈rmap2, rgen2〉 ≝ rmapgen2 in
61  do 〈rmapgen3, locals〉 ← make_registers_list rmap2 (pf_locals pre_f) rgen2;
62  let 〈rmap3, rgen3〉 ≝ rmapgen3 in
63  do 〈rmapgen4, ptrs〉 ← make_registers_list rmap3 (pf_ptrs pre_f) rgen3;
64  let 〈rmap4, rgen4〉 ≝ rmapgen4 in
65  let rmap ≝ λn. opt_to_res … (rmap4 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         rgen4
79         (pf_sig pre_f)
80         result
81         params
82         locals
83         ptrs
84         (pf_stacksize pre_f)
85         graph
86         entry
87         exit
88         )).
89
90definition make_reg_list : (nat → res register) → list pre_register → res (list register) ≝
91λm,ps. foldr ?? (λp,rs0. do rs ← rs0; do r ← m p; OK ? (r::rs)) (OK ? [ ]) ps.
92
93(* XXX move somewhere sensible *)
94let 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) ≝
95match v with
96[ VEmpty ⇒ OK ? (VEmpty …)
97| VCons m hd tl ⇒ do hd' ← f hd;
98                  do tl' ← mmap_vec A B f m tl;
99                  OK ? (hd':::tl')
100].
101
102definition make_addr : (nat → res register) → ∀m:addressing. Vector pre_register (addr_mode_args m) → res (addr m) ≝
103λmp,m. mmap_vec ?? mp ?.
104
105definition make_opt_reg : (pre_register → res register) → option pre_register → res (option register) ≝
106λm,o. match o with [ None ⇒ OK ? (None ?) | Some r ⇒ do r' ← m r; OK ? (Some ? r') ].
107
108let rec make_St_skip l ≝ λr:nat → res register.λf:nat → res label. do l' ← f l; OK ? (St_skip l').
109let rec make_St_cost cl l ≝ λr:nat → res register.λf:nat → res label. do l' ← f l; OK ? (St_cost cl l').
110let 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').
111let 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').
112let 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').
113let rec make_St_load chunk mode args dst l ≝ λr:nat → res register.λf:nat → res label. do dst' ← r dst; do l' ← f l; do args' ← make_addr r ? args; OK ? (St_load chunk mode args' dst' l').
114let rec make_St_store chunk mode args src l ≝ λr:nat → res register.λf:nat → res label. do src' ← r src; do l' ← f l; do args' ← make_addr r ? args; OK ? (St_store chunk mode args' src' l').
115let rec make_St_call_id id args dst sig 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' sig l').
116let rec make_St_call_ptr frs args dst sig 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' sig l').
117let rec make_St_tailcall_id id args sig ≝ λr:nat → res register.λf:nat → res label.  do args' ← make_reg_list r args; OK statement (St_tailcall_id id args' sig).
118let rec make_St_tailcall_ptr frs args sig ≝ λ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' sig).
119let 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').
120let rec make_St_cond1 op 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_cond1 op src' ltrue' lfalse').
121let rec make_St_cond2 op src1 src2 ltrue lfalse ≝ λr:nat → res register.λf:nat → res label. do src1' ← r src1; do src2' ← r src2; do ltrue' ← f ltrue; do lfalse' ← f lfalse; OK ? (St_cond2 op src1' src2' ltrue' lfalse').
122let 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').
123let rec make_St_return src ≝ λr:nat → res register.λf:nat → res label. do src' ← r src; OK statement (St_return src').
124
Note: See TracBrowser for help on using the repository browser.