source: src/RTLabs/import.ma @ 1288

Last change on this file since 1288 was 1072, checked in by campbell, 8 years ago

Use not equals form of showing entry/exit labels.

File size: 6.9 KB
Line 
1
2include "RTLabs/semantics.ma".
3
4let rec n_idents (n:nat) (tag:String) (g:universe tag) : Vector (identifier tag) n × (universe tag) ≝
5match n with
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''〉
10].
11
12definition pre_register ≝ nat.
13
14record pre_internal_function : Type[0] ≝
15{ pf_result    : option (pre_register × typ)
16; pf_params    : list (pre_register × typ)
17; pf_locals    : list (pre_register × typ)
18; pf_stacksize : nat
19; pf_graph     : list (nat × ((pre_register → res register) → (nat → res label) → res statement))
20; pf_entry     : nat
21; pf_exit      : nat
22}.
23
24definition make_register :
25  (pre_register → option register) → pre_register → universe RegisterTag →
26  (nat → option register) × (universe RegisterTag) × register ≝
27λm,reg,g.
28  match m reg with
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'〉
32  ]
33.
34
35definition make_registers_list :
36  (nat → option register) → list (pre_register × typ) → universe RegisterTag →
37    (nat → option register) × (universe RegisterTag) × (list (register×typ)) ≝
38λm,lrs,g.
39foldr ?? (λ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.
44
45axiom MissingRegister : String.
46axiom MissingLabel : String.
47
48(* Doesn't check for identifier overflow, but don't really need to care here. *)
49definition make_internal_function : pre_internal_function → res (fundef internal_function) ≝
50λpre_f.
51  let rgen0 ≝ new_universe RegisterTag in
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
56  let 〈rmap1, rgen1〉 ≝ rmapgen1 in
57  let 〈rmapgen2, params〉 ≝ make_registers_list rmap1 (pf_params pre_f) rgen1 in
58  let 〈rmap2, rgen2〉 ≝ rmapgen2 in
59  let 〈rmapgen3, locals〉 ≝ make_registers_list rmap2 (pf_locals pre_f) rgen2 in
60  let 〈rmap3, rgen3〉 ≝ rmapgen3 in
61  let rmap ≝ λn. opt_to_res … (msg MissingRegister) (rmap3 n) in
62  let max_stmt ≝ foldr ?? (λp,m. max (\fst p) m) 0 (pf_graph pre_f) in
63  let 〈labels, gen〉 ≝ n_idents (S max_stmt) ? (new_universe LabelTag) in
64  let get_label ≝ λn. opt_to_res … (msg MissingLabel) (get_index_weak_v ?? labels n) in
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);
71  do entry ← get_label (pf_entry pre_f);
72  do exit ← get_label (pf_exit pre_f);
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
83         gen
84         rgen3
85         result
86         params
87         locals
88         (pf_stacksize pre_f)
89         graph
90         (dp ?? entry p)
91         (dp ?? exit q)
92         )))
93   .
94% #E destruct (E)
95qed.
96
97definition 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.
99
100(* XXX move somewhere sensible *)
101let 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) ≝
102match 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
109definition 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
112let rec make_St_skip l ≝ λr:nat → res register.λf:nat → res label. do l' ← f l; OK ? (St_skip l').
113let rec make_St_cost cl l ≝ λr:nat → res register.λf:nat → res label. do l' ← f l; OK ? (St_cost cl l').
114let 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').
115let 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').
116let 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').
117let 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').
118let 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').
119let 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').
120let 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').
121let 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').
122let 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').
123let 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').
124let 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').
125definition make_St_return ≝ λr:nat → res register.λf:nat → res label. OK statement St_return.
126
Note: See TracBrowser for help on using the repository browser.