-let get_checked_obj u =
- try let b, o = NUri.UriHash.find cache u in
- if not b then assert false else o
- with Not_found ->
- let ouri = NUri.ouri_of_nuri u in
- let o,_ =
- CicEnvironment.get_cooked_obj ~trust:false CicUniv.oblivion_ugraph ouri
- in
- (* FIX: add all objects to the environment and give back the last one *)
- let l = OCic2NCic.convert_obj ouri o in
- List.iter (fun (u,_,_,_,_ as o) ->
- prerr_endline ("+"^NUri.string_of_uri u);
- NUri.UriHash.add cache u (false,o)) l;
- HExtlib.list_last l
+(* $Id$ *)
+
+exception CircularDependency of string Lazy.t;;
+exception ObjectNotFound of string Lazy.t;;
+exception BadDependency of string Lazy.t;;
+exception BadConstraint of string Lazy.t;;
+
+let type0 = [false, NUri.uri_of_string ("cic:/matita/pts/Type.univ")]
+
+let le_constraints = ref [] (* strict,a,b *)
+
+let rec le_path_uri avoid strict a b =
+ (not strict && NUri.eq a b) ||
+ List.exists
+ (fun (strict',x,y) ->
+ NUri.eq y b && not (List.exists (NUri.eq x) avoid) &&
+ le_path_uri (x::avoid) (strict && not strict') a x
+ ) !le_constraints
+;;
+
+let leq_path a b = le_path_uri [b] (fst a) (snd a) b;;
+
+let universe_leq a b =
+ match a, b with
+ | a,[(false,b)] -> List.for_all (fun a -> leq_path a b) a
+ | _,_ ->
+ raise (BadConstraint
+ (lazy "trying to check if a universe is less or equal than an inferred universe"))
+
+let universe_eq a b = universe_leq b a && universe_leq a b
+
+let add_constraint strict a b =
+ match a,b with
+ | [false,a2],[false,b2] ->
+ if not (le_path_uri [] strict a2 b2) then (
+ if le_path_uri [] (not strict) b2 a2 then
+ (raise (BadConstraint (lazy "universe inconsistency")));
+ le_constraints := (strict,a2,b2) :: !le_constraints)
+ | _ -> raise (BadConstraint
+ (lazy "trying to add a constraint on an inferred universe"))
+;;
+
+let typecheck_obj,already_set = ref (fun _ -> assert false), ref false;;
+let set_typecheck_obj f =
+ if !already_set then
+ assert false
+ else
+ begin
+ typecheck_obj := f;
+ already_set := true
+ end