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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Univ
type contents = Pos | Null
type family = InProp | InSet | InType
type t =
| Prop of contents (* proposition types *)
| Type of universe
let prop = Prop Null
let set = Prop Pos
let type1 = Type type1_univ
let univ_of_sort = function
| Type u -> u
| Prop Pos -> Universe.type0
| Prop Null -> Universe.type0m
let sort_of_univ u =
if is_type0m_univ u then prop
else if is_type0_univ u then set
else Type u
let compare s1 s2 =
if s1 == s2 then 0 else
match s1, s2 with
| Prop c1, Prop c2 ->
begin match c1, c2 with
| Pos, Pos | Null, Null -> 0
| Pos, Null -> -1
| Null, Pos -> 1
end
| Type u1, Type u2 -> Universe.compare u1 u2
| Prop _, Type _ -> -1
| Type _, Prop _ -> 1
let equal s1 s2 = Int.equal (compare s1 s2) 0
let is_prop = function
| Prop Null -> true
| Type u when Universe.equal Universe.type0m u -> true
| _ -> false
let is_set = function
| Prop Pos -> true
| Type u when Universe.equal Universe.type0 u -> true
| _ -> false
let is_small = function
| Prop _ -> true
| Type u -> is_small_univ u
let family = function
| Prop Null -> InProp
| Prop Pos -> InSet
| Type u when is_type0m_univ u -> InProp
| Type u when is_type0_univ u -> InSet
| Type _ -> InType
let family_equal = (==)
open Hashset.Combine
let hash = function
| Prop p ->
let h = match p with
| Pos -> 0
| Null -> 1
in
combinesmall 1 h
| Type u ->
let h = Univ.Universe.hash u in
combinesmall 2 h
module List = struct
let mem = List.memq
let intersect l l' = CList.intersect family_equal l l'
end
module Hsorts =
Hashcons.Make(
struct
type _t = t
type t = _t
type u = universe -> universe
let hashcons huniv = function
| Type u as c ->
let u' = huniv u in
if u' == u then c else Type u'
| s -> s
let eq s1 s2 = match (s1,s2) with
| (Prop c1, Prop c2) -> c1 == c2
| (Type u1, Type u2) -> u1 == u2
|_ -> false
let hash = hash
end)
let hcons = Hashcons.simple_hcons Hsorts.generate Hsorts.hcons hcons_univ
|
