H.set_log_callback no_log;
let u0 = mk_type_universe "0" in
let u1 = mk_type_universe "1" in
- E.add_lt_constraint u0 u1
+ E.add_lt_constraint ~acyclic:true u0 u1
-let fst_var = 1
+let fst_var = 1 (* first variable *)
-let snd_var = 2
+let snd_var = 2 (* second variable *)
+
+let fst_con = 1 (* first constructor *)
+
+let appl ts = C.Appl ts
+
+let prod s w t = C.Prod (s, w, t)
let lambda s w t = C.Lambda (s, w, t)
let typeof c t =
K.typeof G.status [] [] c t
+let whd_typeof c t = whd c (typeof c t)
+
+let not_prop1 c u = match whd_typeof c u with
+ | C.Sort (C.Prop) -> false
+ | _ -> true
+
+let not_prop2 c t = not_prop1 c (typeof c t)
+
+let does_not_occur i c t =
+ K.does_not_occur G.status ~subst:[] c 0 i t
+
let segments_of_uri u =
let s = U.string_of_uri u in
let s = F.chop_extension s in
let s = S.sub s (i+2) (l-i-2) in
X.segments_of_string [] (l-i-2) s
-let name_of_reference ss = function
+let names_of_reference ss = function
| C.Constant (_, name, _, _, _), R.Decl ->
ss, name
| C.Constant (_, name, _, _, _), R.Def _ ->
(name :: ss), name
| _ ->
failwith "name_of_reference"
+
+let resolve_reference = function
+ | R.Ref (u, r) ->
+ let ss = segments_of_uri u in
+ let _, _, _, _, obj = E.get_checked_obj G.status u in
+ let ss, name = names_of_reference ss (obj, r) in
+ X.rev_map_concat X.id "." "type" ss, name