source: src/RTLabs/import.ma @ 797

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

Add error messages wherever the error monad is used.
Sticks to CompCert? style strings+identifiers for the moment.
Use axioms for strings as we currently have no representation or literals
for them - still *very* useful for animation in the proof assistant.

File size: 7.4 KB
Line 
1
2include "RTLabs/semantics.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
51axiom MissingRegister : String.
52axiom MissingLabel : String.
53
54definition make_internal_function : pre_internal_function → res (fundef internal_function) ≝
55λpre_f.
56  let rgen0 ≝ new_universe RegisterTag in
57  do 〈rmapgen1, result〉 ← match pf_result pre_f with
58                          [ None ⇒ OK ? 〈〈λ_.None ?, rgen0〉, None ?〉
59                          | Some r ⇒ do 〈x,y〉 ← make_register (λ_.None ?) r rgen0; OK ? 〈x,Some ? y〉
60                          ];
61  let 〈rmap1, rgen1〉 ≝ rmapgen1 in
62  do 〈rmapgen2, params〉 ← make_registers_list rmap1 (pf_params pre_f) rgen1;
63  let 〈rmap2, rgen2〉 ≝ rmapgen2 in
64  do 〈rmapgen3, locals〉 ← make_registers_list rmap2 (pf_locals pre_f) rgen2;
65  let 〈rmap3, rgen3〉 ≝ rmapgen3 in
66  do 〈rmapgen4, ptrs〉 ← make_registers_list rmap3 (pf_ptrs pre_f) rgen3;
67  let 〈rmap4, rgen4〉 ≝ rmapgen4 in
68  let rmap ≝ λn. opt_to_res … (msg MissingRegister) (rmap4 n) in
69  let max_stmt ≝ foldr ?? (λp,m. max (\fst p) m) 0 (pf_graph pre_f) in
70  do 〈labels, gen〉 ← n_idents (S max_stmt) ? (new_universe LabelTag);
71  let get_label ≝ λn. opt_to_res … (msg MissingLabel) (get_index_weak_v ?? labels n) in
72  do graph ← foldr ?? (λp,g0. do g ← g0;
73                              let 〈l,s〉 ≝ p in
74                              do l' ← get_label l;
75                              do s' ← s rmap get_label;
76                              OK ? (add ?? g l' s')) (OK ? (empty_map ??)) (pf_graph pre_f);
77  do entry ← get_label (pf_entry pre_f);
78  do exit ← get_label (pf_exit pre_f);
79  OK ? (Internal ? (mk_internal_function
80         gen
81         rgen4
82         (pf_sig pre_f)
83         result
84         params
85         locals
86         ptrs
87         (pf_stacksize pre_f)
88         graph
89         entry
90         exit
91         )).
92
93definition make_reg_list : (nat → res register) → list pre_register → res (list register) ≝
94λm,ps. foldr ?? (λp,rs0. do rs ← rs0; do r ← m p; OK ? (r::rs)) (OK ? [ ]) ps.
95
96(* XXX move somewhere sensible *)
97let 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) ≝
98match v with
99[ VEmpty ⇒ OK ? (VEmpty …)
100| VCons m hd tl ⇒ do hd' ← f hd;
101                  do tl' ← mmap_vec A B f m tl;
102                  OK ? (hd':::tl')
103].
104
105definition make_addr : (nat → res register) → ∀m:addressing. Vector pre_register (addr_mode_args m) → res (addr m) ≝
106λmp,m. mmap_vec ?? mp ?.
107
108definition make_opt_reg : (pre_register → res register) → option pre_register → res (option register) ≝
109λm,o. match o with [ None ⇒ OK ? (None ?) | Some r ⇒ do r' ← m r; OK ? (Some ? r') ].
110
111let rec make_St_skip l ≝ λr:nat → res register.λf:nat → res label. do l' ← f l; OK ? (St_skip l').
112let rec make_St_cost cl l ≝ λr:nat → res register.λf:nat → res label. do l' ← f l; OK ? (St_cost cl l').
113let 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').
114let 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').
115let 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').
116let 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').
117let 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').
118let 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').
119let 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').
120let 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).
121let 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).
122let 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').
123let 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').
124let 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').
125let 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').
126definition make_St_return ≝ λr:nat → res register.λf:nat → res label. OK statement St_return.
127
Note: See TracBrowser for help on using the repository browser.