Skip to content

Commit 13d9434

Browse files
sysemenovasysemenova
committed
beginning of typechecker
1 parent 75c4168 commit 13d9434

File tree

2 files changed

+252
-0
lines changed

2 files changed

+252
-0
lines changed

‎theories/syntax.v‎

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -104,3 +104,29 @@ Section RepInd.
104104
end.
105105

106106
End RepInd.
107+
108+
Section SizeInd.
109+
110+
Variables (P : size -> Prop)
111+
(HVarS : forall idx, P (VarS idx))
112+
(HSumS : forall σs, Forall P σs -> P (SumS σs))
113+
(HProdS : forall σs, Forall P σs -> P (ProdS σs))
114+
(HRepS : forall ρ, P (RepS ρ))
115+
(HConstS : forall n, P (ConstS n)).
116+
117+
Fixpoint size_ind (σ: size) : P σ :=
118+
let fix sizes_ind σs : Forall P σs :=
119+
match σs with
120+
| [] => ListDef.Forall_nil _
121+
| s :: ss => ListDef.Forall_cons _ (size_ind s) (sizes_ind ss)
122+
end
123+
in
124+
match σ with
125+
| VarS idx => HVarS idx
126+
| SumS σs => HSumS σs (sizes_ind σs)
127+
| ProdS σs => HProdS σs (sizes_ind σs)
128+
| RepS ρ => HRepS ρ
129+
| ConstS n => HConstS n
130+
end.
131+
132+
End SizeInd.

‎theories/typechecker/typechecker.v‎

Lines changed: 226 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,226 @@
1+
Require Import RecordUpdate.RecordUpdate.
2+
From stdpp Require Import base list.
3+
From Stdlib.Strings Require Import String.
4+
5+
From RichWasm Require Import layout syntax typing util.
6+
Set Bullet Behavior "Strict Subproofs".
7+
8+
Definition type_error := string.
9+
Definition ok := unit.
10+
Definition type_checker_res := sum ok type_error.
11+
12+
Definition ok_term : type_checker_res := inl ().
13+
Definition INR (s:string) : type_checker_res := inr s.
14+
15+
16+
17+
(* No matter how type_checker_res changes, this MUST stay the same *)
18+
Definition check_ok In (func: In -> type_checker_res) (i: In) : bool :=
19+
match (func i) with
20+
| inl a => true
21+
| inr a => false
22+
end.
23+
24+
Definition check_ok_output (res: type_checker_res) : bool :=
25+
match res with
26+
| inl a => true
27+
| inr a => false
28+
end.
29+
30+
(* This is only true if ok is kept at unit. Unfortunately most of the proofs
31+
rely on this. *)
32+
Lemma check_ok_true_to_prop In (func: In -> type_checker_res) (i:In) :
33+
check_ok In func i = true -> func i = ok_term.
34+
Proof.
35+
intros. unfold ok_term.
36+
destruct (func i) eqn:H'.
37+
- unfold ok in o.
38+
assert (o = tt) by (by destruct o).
39+
subst; auto.
40+
- unfold check_ok in H.
41+
rewrite H' in H. inversion H.
42+
Qed.
43+
Lemma check_ok_output_true_to_prop (res: type_checker_res) :
44+
check_ok_output res = true -> res = ok_term.
45+
Proof.
46+
intros. unfold ok_term.
47+
destruct (res) eqn:H'.
48+
- unfold ok in o.
49+
assert (o = tt) by (by destruct o).
50+
subst; auto.
51+
- unfold check_ok in H.
52+
simpl in H.
53+
inversion H.
54+
Qed.
55+
56+
(* Helper function for converting between forall inductive hyp and foldr boolean version *)
57+
Lemma Forall_foldr_bool_to_prop A (Pprop : A -> Prop) (Pbool : A -> bool) (l : list A) :
58+
(Forall (λ x:A, (Pbool x = true) -> Pprop x) l) ->
59+
(foldr (λ x:A, andb (Pbool x)) true l) = true ->
60+
Forall Pprop l.
61+
Proof.
62+
intros HForall Hfoldr.
63+
apply Forall_fold_right.
64+
induction l; simpl; auto.
65+
- rewrite foldr_cons in Hfoldr; apply andb_prop in Hfoldr as [a_true l_true].
66+
apply Forall_cons_1 in HForall; destruct HForall as [a_prop l_prop].
67+
split; auto.
68+
Qed.
69+
70+
(* Converting between _ = ok_term to check_ok = true *)
71+
Lemma equal_okterm_to_checkok In (func: In -> type_checker_res) (Pbool : In -> Prop) :
72+
forall i:In,
73+
((func i = ok_term -> Pbool i) ->
74+
(check_ok In func i = true -> Pbool i)).
75+
Proof.
76+
intros. apply H.
77+
by apply check_ok_true_to_prop.
78+
Qed.
79+
80+
81+
82+
83+
(** WE BEGIN **)
84+
85+
86+
(* mem_ok *)
87+
Definition mem_ok_checker (k:kind_ctx) (mem:memory) : type_checker_res :=
88+
match mem with
89+
| BaseM cm => ok_term
90+
| VarM m =>
91+
if m <? k.(kc_mem_vars) then ok_term else INR "mem_ok error"
92+
end.
93+
94+
Lemma mem_ok_checker_correct (k:kind_ctx) (mem:memory) :
95+
(mem_ok_checker k mem = ok_term) -> mem_ok k mem.
96+
Proof.
97+
intros.
98+
destruct mem.
99+
- apply OKVarM.
100+
simpl in H.
101+
destruct (n <? kc_mem_vars k) eqn:H'.
102+
+ apply Nat.ltb_lt in H'. auto.
103+
+ inversion H.
104+
- apply OKBaseM.
105+
Qed.
106+
107+
108+
109+
(* rep_ok *)
110+
Fixpoint rep_ok_checker (k:kind_ctx) (rep:representation) : type_checker_res :=
111+
match rep with
112+
| AtomR ι => ok_term
113+
| VarR r => if r <? k.(kc_rep_vars) then ok_term else INR "rep_ok error"
114+
| ProdR ρs =>
115+
if (foldr (λ i:representation, andb (check_ok representation (rep_ok_checker k) i)) true ρs)
116+
then ok_term else INR "rep_ok error"
117+
| SumR ρs =>
118+
if (foldr (λ i:representation, andb (check_ok representation (rep_ok_checker k) i)) true ρs)
119+
then ok_term else INR "rep_ok error"
120+
end.
121+
122+
Lemma rep_ok_checker_correct (k:kind_ctx) (rep:representation) :
123+
(rep_ok_checker k rep = ok_term) -> rep_ok k rep.
124+
Proof.
125+
intros.
126+
induction rep using rep_ind.
127+
- apply OKVarR.
128+
simpl in H.
129+
destruct (idx <? kc_rep_vars k) eqn:H'.
130+
+ apply Nat.ltb_lt in H'. auto.
131+
+ inversion H.
132+
- apply OKSumR.
133+
simpl in H.
134+
destruct (foldr (λ i:representation, andb (check_ok representation (rep_ok_checker k) i)) true ρs) eqn:H'.
135+
+ clear H.
136+
apply (Forall_impl _ (λ x, check_ok representation (rep_ok_checker k) x = true -> rep_ok k x)) in H0.
137+
* eapply Forall_foldr_bool_to_prop; [apply H0 | apply H'].
138+
* apply equal_okterm_to_checkok.
139+
+ inversion H.
140+
- apply OKProdR.
141+
simpl in H.
142+
destruct (foldr (λ i:representation, andb (check_ok representation (rep_ok_checker k) i)) true ρs) eqn:H'.
143+
+ clear H.
144+
apply (Forall_impl _ (λ x, check_ok representation (rep_ok_checker k) x = true -> rep_ok k x)) in H0.
145+
* eapply Forall_foldr_bool_to_prop; [apply H0 | apply H'].
146+
* apply equal_okterm_to_checkok.
147+
+ inversion H.
148+
- apply OKAtomR.
149+
Qed.
150+
151+
152+
153+
(* size_ok *)
154+
Fixpoint size_ok_checker (k:kind_ctx) (s:size) : type_checker_res :=
155+
match s with
156+
| ConstS n => ok_term
157+
| VarS r => if r <? k.(kc_size_vars) then ok_term else INR "size_ok error"
158+
| RepS ρ => match (rep_ok_checker k ρ) with
159+
| inl _ => ok_term
160+
| err => err (* this allows propagation*)
161+
(* you could also just ret rep_ok_checker. Idk which would be
162+
better for future changeability. I'll do just ret later*)
163+
end
164+
| SumS σs =>
165+
if (foldr (λ i:size, andb (check_ok size (size_ok_checker k) i)) true σs)
166+
then ok_term else INR "size_ok error"
167+
| ProdS σs =>
168+
if (foldr (λ i:size, andb (check_ok size (size_ok_checker k) i)) true σs)
169+
then ok_term else INR "size_ok error"
170+
end.
171+
172+
Lemma size_ok_checker_correct (k:kind_ctx) (s:size) :
173+
(size_ok_checker k s = ok_term) -> size_ok k s.
174+
Proof.
175+
intros.
176+
induction s using size_ind.
177+
- apply OKVarS.
178+
simpl in H.
179+
destruct (idx <? kc_size_vars k) eqn:H'.
180+
+ apply Nat.ltb_lt in H'. auto.
181+
+ inversion H.
182+
- apply OKSumS.
183+
simpl in H.
184+
destruct (foldr (λ i:size, andb (check_ok size (size_ok_checker k) i)) true σs) eqn:H'.
185+
+ clear H.
186+
apply (Forall_impl _ (λ x, check_ok size (size_ok_checker k) x = true -> size_ok k x)) in H0.
187+
* eapply Forall_foldr_bool_to_prop; [apply H0 | apply H'].
188+
* apply equal_okterm_to_checkok.
189+
+ inversion H.
190+
- apply OKProdS.
191+
simpl in H.
192+
destruct (foldr (λ i:size, andb (check_ok size (size_ok_checker k) i)) true σs) eqn:H'.
193+
+ clear H.
194+
apply (Forall_impl _ (λ x, check_ok size (size_ok_checker k) x = true -> size_ok k x)) in H0.
195+
* eapply Forall_foldr_bool_to_prop; [apply H0 | apply H'].
196+
* apply equal_okterm_to_checkok.
197+
+ inversion H.
198+
- apply OKRepS.
199+
simpl in H.
200+
destruct (rep_ok_checker k ρ) eqn:H'.
201+
+ apply rep_ok_checker_correct.
202+
unfold ok in o.
203+
assert (o = tt) by (by destruct o).
204+
subst; auto.
205+
+ inversion H.
206+
- apply OKConstS.
207+
Qed.
208+
209+
210+
(* kind_ok *)
211+
Definition kind_ok_checker (k:kind_ctx) (ki: kind) : type_checker_res :=
212+
match ki with
213+
| (VALTYPE ρ χ δ) => rep_ok_checker k ρ
214+
| MEMTYPE σ δ => size_ok_checker k σ
215+
end.
216+
217+
Lemma kind_ok_checker_correct (k:kind_ctx) (ki:kind) :
218+
(kind_ok_checker k ki = ok_term) -> kind_ok k ki.
219+
Proof.
220+
intros.
221+
destruct ki; simpl in H.
222+
- apply OKVALTYPE.
223+
apply rep_ok_checker_correct; auto.
224+
- apply OKMEMTYPE.
225+
apply size_ok_checker_correct; auto.
226+
Qed.

0 commit comments

Comments
 (0)