let get_obj = ref (fun _ -> assert false);;
let set_get_obj f = get_obj := f;;
-let type0 = []
-
module F = Format
let rec ppsort f = function
| C.Type ([(`Type|`CProp),u] as univ) ->
if is_declared univ then (C.Type [`Succ, u])
else
+ let universes = !universes in
raise (UntypableSort (lazy ("undeclared universe " ^
NUri.string_of_uri u ^ "\ndeclared ones are: " ^
- String.concat ", " (List.map NUri.string_of_uri !universes)
+ String.concat ", " (List.map NUri.string_of_uri universes)
)))
| C.Type t ->
raise (AssertFailure (lazy (
"Cannot type an inferred type: "^ string_of_univ t)))
- | C.Prop -> (C.Type type0)
+ | C.Prop -> (C.Type [])
;;
let add_lt_constraint a b =
| _ -> raise (BadConstraint
(lazy "trying to add a constraint on an inferred universe"))
;;
+
+let family_of = function (`CProp,_)::_ -> `CProp | _ -> `Type ;;
-let sup l =
+let sup fam l =
match l with
| [(`Type|`CProp),_] -> Some l
| l ->
(fun x -> lt_path_uri [] n1 x || (s1 <> `Succ && NUri.eq n1 x)) acc
in
let solutions = List.fold_left bigger_than !universes l in
- let fam = match l with (`CProp,_)::_ -> `CProp | _ -> `Type in
let rec aux = function
| [] -> None
| u :: tl ->
aux solutions
;;
+let sup l = sup (family_of l) l;;
+
+let inf ~strict fam l =
+ match l with
+ | [(`Type|`CProp),_] -> Some l
+ | [] -> None
+ | l ->
+ let smaller_than acc (_s1,n1) =
+ List.filter
+ (fun x -> lt_path_uri [] x n1 || (not strict && NUri.eq n1 x)) acc
+ in
+ let solutions = List.fold_left smaller_than !universes l in
+ let rec aux = function
+ | [] -> None
+ | u :: tl ->
+ if List.exists (lt_path_uri [] u) solutions then aux tl
+ else Some [fam,u]
+ in
+ aux solutions
+;;
+
+let inf ~strict l = inf ~strict (family_of l) l;;
+
+let rec universe_lt a b =
+ match a, b with
+ | (((`Type|`Succ),_)::_ | []) , [`CProp,_] -> false
+ | l, ([((`Type|`CProp),b)] as orig_b) ->
+ List.for_all
+ (function
+ | `Succ,_ as a ->
+ (match sup [a] with
+ | None -> false
+ | Some x -> universe_lt x orig_b)
+ | _, a -> lt_path a b) l
+ | _, ([] | [`Succ,_] | _::_::_) ->
+ raise (BadConstraint (lazy (
+ "trying to check if "^string_of_univ a^
+ " is lt than the inferred universe " ^ string_of_univ b)))
+;;
+
+
let allowed_sort_elimination s1 s2 =
match s1, s2 with
| C.Type (((`Type|`Succ),_)::_ | []), C.Type (((`Type|`Succ),_)::_ | [])