-let rec le_path_uri strict a b =
- if strict then
- List.exists (fun (strict,x,y) -> NUri.eq y b &&
- if strict then le_path_uri false a x else le_path_uri strict a x)
- !le_constraints
- else
- NUri.eq a b ||
- List.exists (fun (_,x,y) -> NUri.eq y b && le_path_uri false a x)
- !le_constraints
+let type0 = []
+
+module F = Format
+
+let rec ppsort f = function
+ | C.Prop -> F.fprintf f "Prop"
+ | (C.Type []) -> F.fprintf f "Type0"
+ | (C.Type [`Type, u]) -> F.fprintf f "%s" (NUri.name_of_uri u)
+ | (C.Type [`Succ, u]) -> F.fprintf f "S(%s)" (NUri.name_of_uri u)
+ | (C.Type [`CProp, u]) -> F.fprintf f "P(%s)" (NUri.name_of_uri u)
+ | (C.Type l) ->
+ F.fprintf f "Max(";
+ ppsort f ((C.Type [List.hd l]));
+ List.iter (fun x -> F.fprintf f ",";ppsort f ((C.Type [x]))) (List.tl l);
+ F.fprintf f ")"
+;;
+
+let string_of_univ u =
+ let b = Buffer.create 100 in
+ let f = Format.formatter_of_buffer b in
+ ppsort f (NCic.Type u);
+ Format.fprintf f "@?";
+ Buffer.contents b
+;;
+
+let eq_univ (b1,u1) (b2,u2) = b1=b2 && NUri.eq u1 u2;;
+
+let max (l1:NCic.universe) (l2:NCic.universe) =
+ match l2 with
+ | x::tl ->
+ let rest = List.filter (fun y -> not (eq_univ x y)) (l1@tl) in
+ x :: HExtlib.list_uniq ~eq:eq_univ
+ (List.sort (fun (b1,u1) (b2,u2) ->
+ let res = compare b1 b2 in
+ if res = 0 then NUri.compare u1 u2 else res)
+ rest)
+ | [] ->
+ match l1 with
+ | [] -> []
+ | ((`Type|`Succ), _)::_ -> l1
+ | (`CProp, u)::tl -> (`Type, u)::tl
+;;
+
+let lt_constraints = ref [] (* a,b := a < b *)
+
+let rec lt_path_uri avoid a b =
+ List.exists
+ (fun (x,y) ->
+ NUri.eq y b &&
+ (NUri.eq a x ||
+ (not (List.exists (NUri.eq x) avoid) &&
+ lt_path_uri (x::avoid) a x))
+ ) !lt_constraints