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
|
open Bwd
open Bwd.Infix
module A = Ast
module S = NbE.Syntax
module D = NbE.Domain
(* TODO: REALLY improve error messages *)
(* invariant: `tps`, `tms` and `names` all have length `size` *)
type env = {
tps : D.env;
tms : D.env;
names : Ident.local bwd;
size : int;
}
module Eff = Algaeff.Reader.Make (struct type nonrec t = env end)
(** General helpers *)
let lookup (id : Ident.t) : D.t * S.t = match Ident.to_local id with
| Some name -> begin
let env = Eff.read() in
match Bwd.find_index ((=) name) env.names with
| Some ix ->
let tp = Bwd.nth env.tps ix in
(tp, S.Var ix)
| None -> Reporter.unbound_variable id
end
| None -> Reporter.unbound_variable id
let bind ~(name : Ident.local) ~(tp : D.t) f =
let arg = D.var (Eff.read()).size in
let update env = {
tps = env.tps <: tp;
tms = env.tms <: arg;
names = env.names <: name;
size = env.size + 1;
} in
Eff.scope update (fun () -> f arg)
(** NbE helpers *)
let eval tm = NbE.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 = NbE.eval ~env:((Eff.read()).tms <: arg)
let quote v = NbE.quote ~size:(Eff.read()).size v
(** Pretty-printing helpers *)
let pp () = let names = (Eff.read()).names in fun fmt tm ->
Pretty.pp ~names fmt tm
(** Main algorithm *)
let rec check ~(tm : A.expr) ~(tp : D.t) : S.t =
Reporter.tracef ?loc:tm.loc "when checking against the type @[%a@]" (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 (name.value, base, fam)
| _ -> Reporter.fatalf Reporter.Message.IllTyped "expected an element of type @[%a@], but found an element of a universe" (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 = NbE.inst_clo fam arg in
check ~tm:body ~tp:fib in
S.Lam (name.value, body)
| _ -> Reporter.fatalf Reporter.Message.IllTyped "expected an element of type @[%a@], but found an element of a Pi type" (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 (name.value, base, fam)
| _ -> Reporter.fatalf Reporter.Message.IllTyped "expected an element of type @[%a@], but found an element of a universe" (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 = NbE.inst_clo fam (eval fst) in
let snd = check ~tm:snd ~tp:fib in
S.Pair (fst, snd)
| _ -> Reporter.fatalf Reporter.Message.IllTyped "expected an element of type @[%a@], but found an element of a Sigma type" (pp()) (quote tp)
end
| A.Type -> begin match tp with (* TODO type-in-type *)
| D.Type -> S.Type
| _ -> Reporter.fatalf Reporter.Message.IllTyped "expected an element of type @[%a@], but found an element of a universe" (pp()) (quote tp)
end
| A.Bool -> begin match tp with
| D.Type -> S.Bool
| _ -> Reporter.fatalf Reporter.Message.IllTyped "expected an element of type @[%a@], but found an element of a universe" (pp()) (quote tp)
end
| A.True -> begin match tp with
| D.Bool -> S.True
| _ -> Reporter.fatalf Reporter.Message.IllTyped "expected an element of type @[%a@], but found an element of type Bool" (pp()) (quote tp)
end
| A.False -> begin match tp with
| D.Bool -> S.False
| _ -> Reporter.fatalf Reporter.Message.IllTyped "expected an element of type @[%a@], but found an element of type Bool" (pp()) (quote tp)
end
| _ -> let (inferred_tp, tm) = infer tm in begin
try NbE.equate ~size:((Eff.read()).size) inferred_tp tp with
| NbE.Unequal ->
Reporter.fatalf Reporter.Message.IllTyped "expected an element of type @[%a@], but found an element of type @[%a@]" (pp()) (quote tp) (pp()) (quote inferred_tp)
end;
tm
and infer (tm : A.expr) : D.t * S.t =
Reporter.tracef ?loc:tm.loc "when inferring the type" @@ fun () ->
match tm.value with
| A.Var name -> lookup 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 = NbE.inst_clo fam (eval arg) in
let tm = S.App (fn, arg) in
(tp, tm)
| _ -> Reporter.fatalf Reporter.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)
| _ -> Reporter.fatalf Reporter.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 = NbE.inst_clo fam (eval (S.Fst p)) in
let tm = S.Snd p in
(tp, tm)
| _ -> Reporter.fatalf Reporter.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_var = motive_var.value; motive; true_case; false_case; scrut } in
(motive_scrut, tm)
| _ -> Reporter.fatalf Reporter.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
|