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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \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 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
| _ -> false
let family = function
| Prop Null -> InProp
| Prop Pos -> InSet
| Type _ -> InType
module Hsorts =
Hashcons.Make(
struct
type _t = t
type t = _t
type u = universe -> universe
let hashcons huniv = function
Prop c -> Prop c
| Type u -> Type (huniv u)
let equal s1 s2 =
match (s1,s2) with
(Prop c1, Prop c2) -> c1 == c2
| (Type u1, Type u2) -> u1 == u2
|_ -> false
let hash = Hashtbl.hash
end)
let hcons = Hashcons.simple_hcons Hsorts.generate hcons_univ
|
