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
|
open Bwd
open Bwd.Infix
module A = Ast
module S = Syntax
module D = Domain
module R = Reporter
(* TODO: REALLY improve error messages *)
(* `None` means that an underscore was used in the binder *)
(* TODO: actually implement this *)
type local_name = Yuujinchou.Trie.path option
(* invariant: `tps`, `tms` and `names` all have length `size` *)
type env = {
tps : D.env;
tms : D.env;
names : local_name bwd;
size : int;
}
module Eff = Algaeff.Reader.Make (struct type nonrec t = env end)
(** General helpers *)
let lookup_name name : D.t * S.t =
let env = Eff.read() in
match Bwd.find_index ((=) (Some name)) env.names with
| Some ix ->
let tp = Bwd.nth env.tps ix in
let tm = Quote.quote ~size:env.size (Bwd.nth env.tms ix) in
(tp, tm)
| None -> R.fatalf R.Message.UnboundVariable
"unbound variable @[%a@]" S.Pretty.pp_name name
let define ~(name : A.raw_ident) ~(tp : D.t) ~(tm : D.t) f =
let update env = {
tps = env.tps <: tp;
tms = env.tms <: tm;
names = env.names <: Some name;
size = env.size + 1;
} in
Eff.scope update f
let bind ~(name : A.raw_ident) ~(tp : D.t) f =
let arg = D.var (Eff.read()).size in
define ~name ~tp ~tm:arg (fun () -> f arg)
(** NbE helpers *)
let eval tm = Eval.eval ~env:(Eff.read()).tms tm
(** Evaluate under the current environment augmented by `arg` *)
(* TODO: this is kind of inelegant, can we do better? *)
let eval_at arg = Eval.eval ~env:((Eff.read()).tms <: arg)
let quote v = Quote.quote ~size:(Eff.read()).size v
(** Main algorithm *)
let rec check ~(tm : A.expr) ~(tp : D.t) : S.t =
R.tracef ?loc:tm.loc "when checking against the type @[%a@]" Syntax.Pretty.pp (quote tp) @@ fun () ->
match tm.value with
| A.Pi ((name, base), fam) -> begin match tp with
| D.Type ->
let base = check ~tm:base ~tp in
let fam = bind ~name:name.value ~tp:(eval base) @@ fun _ -> check ~tm:fam ~tp in
S.Pi (base, fam)
| _ -> R.fatalf R.Message.IllTyped "expected an element of type @[%a@], but found an element of a universe" Syntax.Pretty.pp (quote tp) end
| A.Lam (name, body) -> begin match tp with
| D.Pi (base, fam) ->
let body = bind ~name:name.value ~tp:base @@ fun arg ->
let fib = Eval.inst_clo fam arg in
check ~tm:body ~tp:fib in
S.Lam body
| _ -> R.fatalf R.Message.IllTyped "expected an element of type @[%a@], but found an element of a Pi type" Syntax.Pretty.pp (quote tp)
end
| A.Sg ((name, base), fam) -> begin match tp with
| D.Type ->
let base = check ~tm:base ~tp in
let fam = bind ~name:name.value ~tp:(eval base) @@ fun _ -> check ~tm:fam ~tp in
S.Sg (base, fam)
| _ -> R.fatalf R.Message.IllTyped "expected an element of type @[%a@], but found an element of a universe" Syntax.Pretty.pp (quote tp) end
| A.Pair (fst, snd) -> begin match tp with
| D.Sg (base, fam) ->
let fst = check ~tm:fst ~tp:base in
let fib = Eval.inst_clo fam (eval fst) in
let snd = check ~tm:snd ~tp:fib in
S.Pair (fst, snd)
| _ -> R.fatalf R.Message.IllTyped "expected an element of type @[%a@], but found an element of a Sigma type" Syntax.Pretty.pp (quote tp)
end
| A.Type -> begin match tp with (* TODO type-in-type *)
| D.Type -> S.Type
| _ -> R.fatalf R.Message.IllTyped "expected an element of type @[%a@], but found an element of a universe" Syntax.Pretty.pp (quote tp)
end
| A.Bool -> begin match tp with
| D.Type -> S.Bool
| _ -> R.fatalf R.Message.IllTyped "expected an element of type @[%a@], but found an element of a universe" Syntax.Pretty.pp (quote tp)
end
| A.True -> begin match tp with
| D.Bool -> S.True
| _ -> R.fatalf R.Message.IllTyped "expected an element of type @[%a@], but found an element of type Bool" Syntax.Pretty.pp (quote tp)
end
| A.False -> begin match tp with
| D.Bool -> S.False
| _ -> R.fatalf R.Message.IllTyped "expected an element of type @[%a@], but found an element of type Bool" Syntax.Pretty.pp (quote tp)
end
| _ -> let (inferred_tp, tm) = infer tm in begin
try Conversion.equate ~size:((Eff.read()).size) inferred_tp tp with
| Conversion.Unequal ->
R.fatalf R.Message.IllTyped "expected an element of type @[%a@], but found an element of type @[%a@]" Syntax.Pretty.pp (quote tp) Syntax.Pretty.pp (quote inferred_tp)
end;
tm
and infer (tm : A.expr) : D.t * S.t =
R.tracef ?loc:tm.loc "when inferring the type" @@ fun () ->
match tm.value with
| A.Var name -> lookup_name name
| A.Check (tm, tp) ->
let tp = eval @@ check ~tp:D.Type ~tm:tp in
let tm = check ~tp ~tm in
(tp, tm)
| A.App (fn, arg) -> begin match infer fn with
| (D.Pi (base, fam), fn) ->
let arg = check ~tm:arg ~tp:base in
let tp = Eval.inst_clo fam (eval arg) in
let tm = S.App (fn, arg) in
(tp, tm)
| _ -> R.fatalf R.Message.IllTyped "cannot apply this term because it is not a function"
end
| A.Fst p -> begin match infer p with
| (D.Sg (base, _), p) -> (base, S.Fst p)
| _ -> R.fatalf R.Message.IllTyped "cannot apply first projection to this term because it is not of sigma type"
end
| A.Snd p -> begin match infer p with
| (D.Sg (_, fam), p) ->
let tp = Eval.inst_clo fam (eval (S.Fst p)) in
let tm = S.Snd p in
(tp, tm)
| _ -> R.fatalf R.Message.IllTyped "cannot apply second projection to this term because it is of sigma type"
end
| A.BoolElim { motive_var; motive_body; true_case; false_case; scrut } ->
let scrut = check ~tm:scrut ~tp:D.Bool in
let motive = bind ~name:motive_var.value ~tp:D.Bool @@ fun _ ->
check ~tm:motive_body ~tp:D.Type in
let motive_true = eval_at D.True motive in
let motive_false = eval_at D.False motive in
let motive_scrut = eval_at (eval scrut) motive in
let true_case = check ~tm:true_case ~tp:motive_true in
let false_case = check ~tm:false_case ~tp:motive_false in
let tm = S.BoolElim { motive; true_case; false_case; scrut } in
(motive_scrut, tm)
| _ -> R.fatalf R.Message.CannotInferType "cannot infer type"
let empty_env : env = {
tps = Emp;
tms = Emp;
names = Emp;
size = 0;
}
let infer_toplevel (tm : A.expr) = Eff.run ~env:empty_env @@ fun () -> infer tm
|