-
Notifications
You must be signed in to change notification settings - Fork 3
/
Compile.v
173 lines (146 loc) · 7.02 KB
/
Compile.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
From Coq Require Import List String Arith Lia.
Import ListNotations.
From Equations Require Import Equations.
From MetaCoq.PCUIC Require Import PCUICAstUtils.
From MetaCoq.Utils Require Import MCList bytestring.
From MetaCoq.Erasure Require Import EAst ESpineView EEtaExpanded EInduction ERemoveParams Erasure EGlobalEnv.
From Malfunction Require Import utils_array Malfunction.
Open Scope bs.
Section MapiInP.
Context {A B : Type}.
Equations mapi_InP (l : list A) (n : nat) (f : nat -> forall x : A, In x l -> B) : list B :=
mapi_InP nil n _ := nil;
mapi_InP (cons x xs) n f := cons (f n x _) (mapi_InP xs (S n) (fun n x inx => f n x _)).
End MapiInP.
Lemma mapi_InP_spec' {A B : Type} (f : nat -> A -> B) (l : list A) n :
mapi_InP l n (fun n (x : A) _ => f n x) = mapi_rec f l n.
Proof.
remember (fun n (x : A) _ => f n x) as g.
funelim (mapi_InP l n g); simpl. reflexivity.
simp mapi_InP.
f_equal.
now rewrite (H f0).
Qed.
Lemma mapi_InP_spec {A B : Type} (f : nat -> A -> B) (l : list A) :
mapi_InP l 0 (fun n (x : A) _ => f n x) = mapi f l.
Proof.
eapply mapi_InP_spec'.
Qed.
Definition Mapply_ '(e, l) :=
match l with [] => e | _ => Mapply (e, l) end.
Definition Mlambda_ '(e, l) :=
match e with [] => l | _ => Mlambda (e, l) end.
Definition blocks_until i (num_args : list nat) :=
#| filter (fun x => match x with 0 => false | _ => true end) (firstn i num_args)|.
Definition nonblocks_until i num_args :=
#| filter (fun x => match x with 0 => true | _ => false end) (firstn i num_args)|.
Definition Mcase : list nat * t * list (list Ident.t * t) -> t :=
fun '(num_args, discr, brs) =>
Mswitch (discr, mapi (fun i '(nms, b) =>
(match nth_error num_args i with
| Some 0 => [Malfunction.Intrange (int_of_nat (nonblocks_until i num_args), int_of_nat (nonblocks_until i num_args))]
| _hasargs => [Malfunction.Tag (int_of_nat (blocks_until i num_args))]
end,
Mapply_ (Mlambda_ (nms, b), mapi (fun i _ => Mfield (int_of_nat i, discr)) (nms)))) brs).
From MetaCoq Require Import EAst.
Section Compile.
Context (Σ : global_declarations).
Definition lookup_record_projs (e : global_declarations) (ind : Kernames.inductive) : option (list Kernames.ident) :=
match lookup_inductive e ind with
| Some (mdecl, idecl) => Some (map proj_name idecl.(ind_projs))
| None => None
end.
Definition lookup_constructor_args (e : global_declarations) (ind : Kernames.inductive) : option (list nat) :=
match lookup_inductive e ind with
| Some (mdecl, idecl) => Some (map cstr_nargs idecl.(ind_ctors))
| None => None
end.
Definition Mapply_u t a :=
match t with Mapply (fn, args) => Mapply (fn, List.app args [a]) | _ => Mapply (t, [a]) end.
Obligation Tactic := idtac.
Definition num_of_nat n := Mnum (numconst_Int (int_of_nat n)).
Definition compile_array (values : list Malfunction.t) (default : Malfunction.t) : Malfunction.t :=
let init := Mvecnew (Array, num_of_nat (List.length values), default) in
fold_left_i (fun v idx arr => Mvecset (Array, arr, num_of_nat idx, v)) values init.
(* Definition to_primitive (compile : term -> Malfunction.t)
(v : EPrimitive.prim_val EAst.term) : Malfunction.t := *)
Fixpoint is_wf_rec_body (t : Malfunction.t) : bool :=
match t with
| Mlambda _ => true
| Mlazy _ => true
| Mlet (_bindings, t) => is_wf_rec_body t
| _ => false
end.
Definition force_lambda (t : Malfunction.t) :=
if is_wf_rec_body t then t
else Mlambda (["__expanded"], Mapply_u t (Mvar "__expanded")).
Equations? compile (t: term) : Malfunction.t
by wf t (fun x y : EAst.term => size x < size y) :=
| tVar na => Mvar na
| tLambda nm bod => Mlambda ([(BasicAst.string_of_name nm)], compile bod)
| tLetIn nm dfn bod => Mlet ([Named ((BasicAst.string_of_name nm), compile dfn)], compile bod)
| tApp fn arg =>
Mapply_u (compile fn) (compile arg)
| tConst nm => Mglobal (Kernames.string_of_kername nm)
| tConstruct i m [] =>
match lookup_constructor_args Σ i with
| Some num_args => Mnum (numconst_Int (int_of_nat (nonblocks_until m num_args)))
| None => Mstring "error: inductive not found"
end
| tConstruct i m args =>
match lookup_constructor_args Σ i with
| Some num_args => Mblock (int_of_nat (blocks_until m num_args), map_InP args (fun x H => compile x))
| None => Mstring "error: inductive not found"
end
| tCase i mch [] => Mlambda (["empty_match"], Mvar "empty_match")
| tCase i mch brs =>
match lookup_constructor_args Σ (fst i) with
| Some num_args =>
Mcase (num_args, compile mch, map_InP brs (fun br H => (rev_map (fun nm => (BasicAst.string_of_name nm)) (fst br), compile (snd br))))
| None => Mstring "error: inductive not found"
end
| tFix mfix idx =>
let bodies := map_InP mfix (fun d H => ((BasicAst.string_of_name (d.(dname))), force_lambda (compile d.(dbody)))) in
Mlet ([Recursive bodies], Mvar (fst (nth (idx) bodies ("", Mstring ""))))
| tProj (Kernames.mkProjection ind _ nargs) bod with lookup_record_projs Σ ind :=
{ | Some args =>
let len := List.length args in
Mfield (int_of_nat (len - 1 - nargs), compile bod)
| None => Mstring "inductive not found" }
| tPrim (existT (EPrimitive.primIntModel i)) => Mnum (numconst_Int i)
| tPrim (existT (EPrimitive.primFloatModel f)) => Mnum (numconst_Float64 f)
| tPrim (existT (EPrimitive.primArrayModel a)) =>
let default := compile (EPrimitive.array_default a) in
let values := map_InP (EPrimitive.array_value a) (fun v H => compile v) in
let arr := compile_array values default in
Mapply (Mglobal "PArray.of_array", [ arr ; default ])
| tLazy t => Mlazy (compile t)
| tForce t => Mforce (compile t)
| tRel n => Mstring "error: tRel has been translated away"
| tBox => Mstring "error: tBox has been translated away"
| tCoFix mfix idx => Mstring "error: tCofix not supported"
| tEvar _ _ => Mstring "error: tEvar not supported"
.
Proof.
all: try (cbn; lia).
- subst args. eapply (In_size id size) in H. cbn in *.
unfold id in H. change (fun x => size x) with size in H. lia.
- eapply (In_size snd size) in H. cbn in *.
lia.
- eapply (In_size dbody size) in H. cbn in *. lia.
- eapply (In_size id size) in H. unfold id in *; cbn in *.
change (fun x => size x) with size in H. lia.
Qed.
End Compile.
Definition compile_constant_decl Σ cb :=
option_map (compile Σ) cb.(cst_body).
Fixpoint compile_env Σ : list (string * option t) :=
match Σ with
| [] => []
| (x,d) :: Σ => match d with
ConstantDecl cb => (Kernames.string_of_kername x, compile_constant_decl Σ cb) :: compile_env Σ
| _ => compile_env Σ
end
end.
Definition compile_program (p : EProgram.eprogram) : Malfunction.program :=
(compile_env (fst p), compile (fst p) (snd p)).