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
open Fmlib
module Algo = Gamma_algo.Make (Gamma_holes)
module Uni = Unifier.Make (Gamma_holes)
include Gamma_holes
let string_of_term term gh =
Term_printer.string_of_term term (Gamma_holes.context gh)
let _ = string_of_term
let is_subtype (sub: Term.typ) (typ: Term.typ) (gh: t) : bool
=
Option.has (Uni.unify sub typ true gh)
let rec check (term: Term.t) (c: t): Term.typ option =
let open Term in
let open Option in
match term with
| Sort s ->
Some (type_of_sort s)
| Value v ->
Some (type_of_literal v c)
| Variable i ->
if i < count c then
Some (type_of_variable i c)
else
None
| Appl (f, arg, _ ) ->
check f c >>= fun f_type ->
check arg c >>= fun arg_type ->
(
match Algo.key_normal f_type c with
| Pi (tp, rt, _ ) when is_subtype arg_type tp c ->
Some (apply rt arg)
| _ ->
None
)
| Typed (exp, tp) ->
check exp c >>=
fun exp_type ->
check tp c >>=
fun tp_tp ->
( match tp_tp with
| Sort _ when is_subtype exp_type tp c ->
Some tp
| _ ->
None
)
| Lambda (arg, exp, info ) ->
check arg c >>= fun sort ->
if Term.is_sort sort then
let name = Lambda_info.name info in
check exp (push_local name arg c)
>>= fun res ->
Some (
Pi (arg, res, Pi_info.typed name)
)
else
None
| Pi (arg, res, info) ->
check arg c >>=
(
function
| Sort arg_sort ->
check res (push_local (Pi_info.name info) arg c)
>>=
(
function
| Sort res_sort ->
Some (Sort (Sort.pi_sort arg_sort res_sort))
| _ ->
None
)
| _ ->
None
)
let check (term: Term.t) (gamma: Gamma.t): Term.typ option =
check term (make gamma)
let is_valid_context (gamma: Gamma.t): bool =
let cnt = Gamma.count gamma in
let rec check_entry i =
if i = cnt then
true
else
let typ = Gamma.type_at_level i gamma in
match Term.down (cnt - i) typ with
| None ->
false
| Some _ ->
match check typ gamma with
| None ->
false
| Some _ ->
let idx = Gamma.index_of_level i gamma in
match Gamma.definition_term idx gamma with
| None ->
check_entry (i + 1)
| Some def ->
match Term.down (cnt - i) def with
| None ->
false
| Some _ ->
match check def gamma with
| None ->
false
| Some def_typ ->
let gh = Gamma_holes.make gamma in
is_subtype def_typ typ gh
&& check_entry (i + 1)
in
check_entry 0
let%test _ =
is_valid_context (Gamma.standard ())