Source file gamma_algo.ml
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
open Fmlib
module type GAMMA =
sig
type t
val count: t -> int
val push_local: string -> Term.typ -> t -> t
val type_of_literal: Term.Value.t -> t -> Term.typ
val type_of_variable: int -> t -> Term.typ
val definition_term: int -> t -> Term.t option
end
module Make (Gamma: GAMMA) =
struct
include Gamma
let key_split
(t: Term.t)
(args: (Term.t * Term.Application_info.t) list)
(c: t)
: Term.t * (Term.t * Term.Application_info.t) list
=
let rec split t args =
match t with
| Term.Variable i ->
(match definition_term i c with
| None ->
t, args
| Some def ->
split def args)
| Lambda (_, exp, _) ->
(
match args with
| [] ->
t, args
| (arg, _) :: args ->
split Term.(apply exp arg) args
)
| Term.Appl (f, arg, mode) ->
split f ((arg, mode) :: args)
| Term.Typed (term, _) ->
term, args
| _ ->
t, args
in
split t args
let key_normal (t: Term.t) (c: t): Term.t =
let key, args = key_split t [] c in
List.fold_left
(fun res (arg, mode) ->
Term.Appl (res, arg, mode))
key
args
let type_of_term (t:Term.t) (c:t): Term.typ =
let rec typ t c =
let open Term in
match t with
| Sort s ->
type_of_sort s
| Value v ->
type_of_literal v c
| Variable i ->
type_of_variable i c
| Typed (_, tp) ->
tp
| Appl (f, a, _) ->
(match key_normal (typ f c) c with
| Pi (_, rt, _) ->
apply rt a
| _ ->
assert false
)
| Lambda (tp, exp, info) ->
let c_inner = push_local (Lambda_info.name info) tp c in
let rt = typ exp c_inner
in
let info =
if has_variable 0 rt then
Pi_info.typed (Lambda_info.name info)
else
Pi_info.arrow
in
Pi (tp, rt, info)
| Pi (tp, rt, info) ->
let name = Pi_info.name info in
(match
typ tp c, typ rt (push_local name tp c)
with
| Sort s1, Sort s2 ->
let open Sort in
(match s1, s2 with
| Proposition, Any i ->
Sort (Any i)
| Any i, Any j ->
Sort (Any (max i j))
| _, Proposition ->
Sort Proposition
)
| _, _ ->
assert false
)
| Where (name, tp, exp, def) ->
typ (expand_where name tp exp def) c
in
typ t c
let rec sort_of_kind (k: Term.typ) (c:t): Term.Sort.t option =
let open Term
in
match key_normal k c with
| Sort s ->
Some s
| Pi (arg_tp, res_tp, _) ->
sort_of_kind res_tp (push_local "_" arg_tp c)
| _ ->
None
let is_kind (k: Term.typ) (c: t): bool =
Option.has (sort_of_kind k c)
end