Source file universes.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
148
149
150
151
152
153
154
155
module B = Kernel.Basic
module T = Kernel.Term

type univ = Sinf | Var of B.name | Enum of int

type pred =
  | Axiom of univ * univ
  | Cumul of univ * univ
  | Rule of univ * univ * univ

type cstr = Pred of pred | EqVar of B.name * B.name

module C = Set.Make (struct
  type t = cstr

  let compare = compare
end)

let md_theory = ref @@ B.mk_mident ""

let md_univ = ref (B.mk_mident "")

let pvar () = B.mk_name !md_theory (B.mk_ident "var")

let sort () = B.mk_name !md_theory (B.mk_ident "Sort")

let typ () = B.mk_name !md_theory (B.mk_ident "type")

let set () = B.mk_name !md_theory (B.mk_ident "set")

let prop () = B.mk_name !md_theory (B.mk_ident "prop")

let univ () = B.mk_name !md_theory (B.mk_ident "Univ")

let cast' () = B.mk_name !md_theory (B.mk_ident "cast'")

let axiom () = B.mk_name !md_theory (B.mk_ident "Axiom")

let rule () = B.mk_name !md_theory (B.mk_ident "Rule")

let cumul () = B.mk_name !md_theory (B.mk_ident "Cumul")

let enum () = B.mk_name !md_theory (B.mk_ident "enum")

let uzero () = B.mk_name !md_theory (B.mk_ident "uzero")

let usucc () = B.mk_name !md_theory (B.mk_ident "usucc")

let subtype () = B.mk_name !md_theory (B.mk_ident "SubType")

let forall () = B.mk_name !md_theory (B.mk_ident "forall")

let sinf () = B.mk_name !md_theory (B.mk_ident "sinf")

let true_ () = T.mk_Const B.dloc (B.mk_name !md_theory (B.mk_ident "true"))

let rec term_of_level i =
  assert (i >= 0);
  if i = 0 then T.mk_Const B.dloc (uzero ())
  else T.mk_App (T.mk_Const B.dloc (usucc ())) (term_of_level (i - 1)) []

let term_of_univ u =
  let lc = B.dloc in
  match u with
  | Sinf -> T.mk_Const lc (sinf ())
  | Var n -> T.mk_Const lc n
  | Enum i -> T.mk_App (T.mk_Const B.dloc (enum ())) (term_of_level i) []

let term_of_pred p =
  let lc = B.dloc in
  match p with
  | Axiom (s, s') ->
      T.mk_App2 (T.mk_Const lc (axiom ())) [term_of_univ s; term_of_univ s']
  | Cumul (s, s') ->
      T.mk_App2 (T.mk_Const lc (cumul ())) [term_of_univ s; term_of_univ s']
  | Rule (s, s', s'') ->
      T.mk_App2
        (T.mk_Const lc (rule ()))
        [term_of_univ s; term_of_univ s'; term_of_univ s'']

let pattern_of_level _ = failwith "todo pattern of level"

let is_const cst t =
  match t with T.Const (_, n) -> B.name_eq cst n | _ -> false

let is_var md_elab t =
  match t with T.Const (_, n) -> B.md n = md_elab | _ -> false

let is_enum t =
  match t with T.App (f, _, []) when is_const (enum ()) f -> true | _ -> false

let is_subtype t =
  match t with
  | T.App (f, _, [_; _; _]) when is_const (subtype ()) f -> true
  | _ -> false

let extract_subtype t =
  match t with
  | T.App (f, _, [_; _; _]) as s when is_const (subtype ()) f -> s
  | _ -> assert false

let is_forall t =
  match t with
  | T.App (f, _, [_; _]) when is_const (forall ()) f -> true
  | _ -> false

let extract_forall t =
  match t with
  | T.App (f, _, [_; T.Lam (_, _, _, t)]) when is_const (forall ()) f -> t
  | _ -> assert false

let is_cast' t =
  match t with T.App (f, _, _) when is_const (cast' ()) f -> true | _ -> false

let extract_cast' t =
  match t with
  | T.App (f, s1, [s2; a; b; t]) when is_const (cast' ()) f -> (s1, s2, a, b, t)
  | T.App (f, s1, s2 :: a :: b :: m :: n) when is_const (cast' ()) f ->
      (s1, s2, a, b, T.mk_App2 m n)
  | _ ->
      Format.eprintf "%a@." Api.Pp.Default.print_term t;
      assert false

let rec extract_level : T.term -> int =
 fun t ->
  match t with
  | T.Const (_, n) when B.name_eq n (uzero ()) -> 0
  | T.App (T.Const (_, n), l, []) when B.name_eq n (usucc ()) ->
      1 + extract_level l
  | _ -> assert false

exception Not_univ

exception Not_pred

let extract_univ : T.term -> univ =
 fun t ->
  match t with
  | T.Const (_, n) when n = sinf () -> Sinf
  | T.Const (_, n) -> Var n
  | T.App (T.Const (_, c), n, []) when B.name_eq c (enum ()) ->
      Enum (extract_level n)
  | _ ->
      Format.eprintf "%a@." Api.Pp.Default.print_term t;
      assert false

let extract_pred t =
  match t with
  | T.App (f, s, [s']) when is_const (axiom ()) f ->
      Axiom (extract_univ s, extract_univ s')
  | T.App (f, s, [s']) when is_const (cumul ()) f ->
      Cumul (extract_univ s, extract_univ s')
  | T.App (f, s, [s'; s'']) when is_const (rule ()) f ->
      Rule (extract_univ s, extract_univ s', extract_univ s'')
  | _ -> raise Not_pred