X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fcomponents%2Fng_kernel%2FnCicEnvironment.ml;h=991a88f6406a120b9066d9c28e062ce7ff1aa13b;hb=d51f9674886d1e609a6ea792b65871dcde4f6503;hp=738329689988176b57ecc0b7243f021792cc5c20;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git

diff --git a/matita/components/ng_kernel/nCicEnvironment.ml b/matita/components/ng_kernel/nCicEnvironment.ml
index 738329689..991a88f64 100644
--- a/matita/components/ng_kernel/nCicEnvironment.ml
+++ b/matita/components/ng_kernel/nCicEnvironment.ml
@@ -24,8 +24,8 @@ let cache = NUri.UriHash.create 313;;
 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 
 
@@ -155,11 +155,11 @@ let typeof_sort = function
   | 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 ()))));
@@ -243,7 +243,7 @@ let allowed_sort_elimination s1 s2 =
   | 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
@@ -254,6 +254,9 @@ let set_typecheck_obj f =
   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
@@ -279,6 +282,16 @@ let invalidate_item item =
      | `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;;
 
@@ -288,11 +301,12 @@ let to_exn f x =
   | `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';
@@ -317,35 +331,37 @@ let check_and_add_obj ((u,_,_,_,_) as 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 _,_,_) ->
@@ -354,9 +370,9 @@ let get_checked_decl = function
   | _ -> 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,_,_) ->
@@ -365,40 +381,40 @@ let get_checked_def = function
   | _ -> 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
 ;;