let history = ref [];;
let frozen_list = ref [];;
-let get_obj = ref (fun _ -> assert false);;
-let set_get_obj f = get_obj := f;;
+let get_obj = ref (fun _ _ -> assert false);;
+let set_get_obj = (:=) get_obj;;
module F = Format
| C.Prop -> (C.Type [])
;;
-let add_lt_constraint a b =
+let add_lt_constraint ~acyclic a b =
match a,b with
| [`Type,a2],[`Type,b2] ->
if not (lt_path_uri [] a2 b2) then (
- if lt_path_uri [] b2 a2 || NUri.eq a2 b2 then
+ if acyclic && (lt_path_uri [] b2 a2 || NUri.eq a2 b2) then
(raise(BadConstraint(lazy("universe inconsistency adding "^
pp_constraint a2 b2
^ " to:\n" ^ pp_constraints ()))));
| C.Prop, C.Type _ -> `UnitOnly
;;
-let typecheck_obj,already_set = ref (fun _ -> assert false), ref false;;
+let typecheck_obj,already_set = ref (fun _ _ -> assert false), ref false;;
let set_typecheck_obj f =
if !already_set then
assert false
end
;;
+(* CSC: old code that performs recursive invalidation; to be removed
+ * once we understand what we really want. Once we removed it, we can
+ * also remove the !history
let invalidate_item item =
let item_eq a b =
match a, b with
| `Constr _ -> assert false
) to_be_deleted
;;
+*)
+
+let invalidate_item =
+ function
+ `Obj (uri,_) -> NUri.UriHash.remove cache uri
+ | `Constr ([_,u1],[_,u2]) ->
+ let w = u1,u2 in
+ lt_constraints := List.filter ((<>) w) !lt_constraints;
+ | `Constr _ -> assert false
+;;
exception Propagate of NUri.uri * exn;;
| `Exn e -> raise e
;;
-let check_and_add_obj ((u,_,_,_,_) as obj) =
+let check_and_add_obj (status:#NCic.status) ((u,_,_,_,_) as obj) =
let saved_frozen_list = !frozen_list in
try
frozen_list := (u,obj)::saved_frozen_list;
- !typecheck_obj obj;
+ HLog.warn ("Typechecking of " ^ NUri.string_of_uri u);
+ !typecheck_obj (status :> NCic.status) obj;
frozen_list := saved_frozen_list;
let obj' = `WellTyped obj in
NUri.UriHash.add cache u obj';
| e ->
frozen_list := saved_frozen_list;
let exn = `Exn e in
- NUri.UriHash.add cache u exn;
history := (`Obj (u,obj))::!history;
if saved_frozen_list = [] then
exn
else
- raise (Propagate (u,e))
+ begin
+ NUri.UriHash.add cache u exn;
+ raise (Propagate (u,e))
+ end
;;
-let get_checked_obj u =
+let get_checked_obj status u =
if List.exists (fun (k,_) -> NUri.eq u k) !frozen_list
then
raise (CircularDependency (lazy (NUri.string_of_uri u)))
else
try NUri.UriHash.find cache u
- with Not_found -> check_and_add_obj (!get_obj u)
+ with Not_found -> check_and_add_obj status (!get_obj (status :> NCic.status) u)
;;
-let get_checked_obj u = to_exn get_checked_obj u;;
+let get_checked_obj (status:#NCic.status) u = to_exn (get_checked_obj status) u;;
-let check_and_add_obj ((u,_,_,_,_) as obj) =
+let check_and_add_obj status ((u,_,_,_,_) as obj) =
if NUri.UriHash.mem cache u then
raise (AlreadyDefined (lazy (NUri.string_of_uri u)))
else
- ignore (to_exn check_and_add_obj obj)
+ ignore (to_exn (check_and_add_obj status) obj)
;;
-let get_checked_decl = function
+let get_checked_decl status = function
| Ref.Ref (uri, Ref.Decl) ->
- (match get_checked_obj uri with
+ (match get_checked_obj status uri with
| _,height,_,_, C.Constant (rlv,name,None,ty,att) ->
rlv,name,ty,att,height
| _,_,_,_, C.Constant (_,_,Some _,_,_) ->
| _ -> prerr_endline "get_checked_decl on a non decl"; assert false
;;
-let get_checked_def = function
+let get_checked_def status = function
| Ref.Ref (uri, Ref.Def _) ->
- (match get_checked_obj uri with
+ (match get_checked_obj status uri with
| _,height,_,_, C.Constant (rlv,name,Some bo,ty,att) ->
rlv,name,bo,ty,att,height
| _,_,_,_, C.Constant (_,_,None,_,_) ->
| _ -> prerr_endline "get_checked_def on a non def"; assert false
;;
-let get_checked_indtys = function
+let get_checked_indtys status = function
| Ref.Ref (uri, (Ref.Ind (_,n,_)|Ref.Con (n,_,_))) ->
- (match get_checked_obj uri with
+ (match get_checked_obj status uri with
| _,_,_,_, C.Inductive (inductive,leftno,tys,att) ->
inductive,leftno,tys,att,n
| _ -> prerr_endline "get_checked_indtys on a non ind 2"; assert false)
| _ -> prerr_endline "get_checked_indtys on a non ind"; assert false
;;
-let get_checked_fixes_or_cofixes = function
+let get_checked_fixes_or_cofixes status = function
| Ref.Ref (uri, (Ref.Fix _|Ref.CoFix _))->
- (match get_checked_obj uri with
+ (match get_checked_obj status uri with
| _,height,_,_, C.Fixpoint (_,funcs,att) ->
funcs, att, height
| _ ->prerr_endline "get_checked_(co)fix on a non (co)fix 2";assert false)
| _ -> prerr_endline "get_checked_(co)fix on a non (co)fix"; assert false
;;
-let get_relevance (Ref.Ref (_, infos) as r) =
+let get_relevance status (Ref.Ref (_, infos) as r) =
match infos with
- Ref.Def _ -> let res,_,_,_,_,_ = get_checked_def r in res
- | Ref.Decl -> let res,_,_,_,_ = get_checked_decl r in res
+ Ref.Def _ -> let res,_,_,_,_,_ = get_checked_def status r in res
+ | Ref.Decl -> let res,_,_,_,_ = get_checked_decl status r in res
| Ref.Ind _ ->
- let _,_,tl,_,n = get_checked_indtys r in
+ let _,_,tl,_,n = get_checked_indtys status r in
let res,_,_,_ = List.nth tl n in
res
| Ref.Con (_,i,_) ->
- let _,_,tl,_,n = get_checked_indtys r in
+ let _,_,tl,_,n = get_checked_indtys status r in
let _,_,_,cl = List.nth tl n in
let res,_,_ = List.nth cl (i - 1) in
res
| Ref.Fix (fixno,_,_)
| Ref.CoFix fixno ->
- let fl,_,_ = get_checked_fixes_or_cofixes r in
+ let fl,_,_ = get_checked_fixes_or_cofixes status r in
let res,_,_,_,_ = List.nth fl fixno in
res
;;