X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fng_kernel%2FnCicEnvironment.ml;h=d3b6a327cab286c42c717876e77530a0cfe2762e;hb=48c011f52853dd106dbf9cbbd1b9da61277fba3b;hp=c7389f16761b4d64579a9a3afb013378b3f790e7;hpb=cacbe3c6493ddce76c4c13379ade271d8dd172e8;p=helm.git

diff --git a/matitaB/components/ng_kernel/nCicEnvironment.ml b/matitaB/components/ng_kernel/nCicEnvironment.ml
index c7389f167..d3b6a327c 100644
--- a/matitaB/components/ng_kernel/nCicEnvironment.ml
+++ b/matitaB/components/ng_kernel/nCicEnvironment.ml
@@ -20,13 +20,66 @@ exception BadDependency of string Lazy.t * exn;;
 exception BadConstraint of string Lazy.t;;
 exception AlreadyDefined of string Lazy.t;;
 
-let cache = NUri.UriHash.create 313;;
-let history = ref [];;
-let frozen_list = ref [];;
+type item = 
+  [ `Obj of NUri.uri * NCic.obj 
+  | `Constr of NCic.universe * NCic.universe ]
+;;
+
+type obj_exn =
+  [ `WellTyped of NCic.obj
+  | `Exn of exn ]
+;;
+
+type db = {
+        cache : obj_exn NUri.UriHash.t;
+        history : item list ref;
+        frozen_list : (NUri.uri * NCic.obj) list ref;
+        lt_constraints : (NUri.uri * NUri.uri) list ref;
+        universes : NUri.uri list ref
+}
+
+class type g_status = 
+  object
+  method env_db : db
+  end
+
+
+class virtual status uid =
+ object
+  inherit NCic.status uid
+
+  val db = { 
+    cache = NUri.UriHash.create 313;
+    history = ref [];
+    frozen_list = ref [];
+    lt_constraints = ref []; (* a,b := a < b *)
+    universes = ref []
+  }
+
+  method env_db = db
+
+  method set_env_db v = {< db = v >}
+  method set_env_status : 's.#g_status as 's -> 'self
+   = fun o -> {< db = o#env_db >}
+ end
+;;
 
 let get_obj = ref (fun _ _ -> assert false);;
+
 let set_get_obj = (:=) get_obj;;
 
+let typechk_already_set = ref false;;  
+let typecheck_obj = ref (fun _ _ -> assert false);;
+
+let set_typecheck_obj f = 
+  if !typechk_already_set then
+   assert false
+  else
+   begin
+    typecheck_obj := f;
+    typechk_already_set := true
+   end
+
 module F = Format 
 
 let rec ppsort f = function
@@ -68,19 +121,17 @@ let max (l1:NCic.universe) (l2:NCic.universe) =
      | (`CProp, u)::tl -> (`Type, u)::tl
 ;;
 
-let lt_constraints = ref [] (* a,b := a < b *)
-
-let rec lt_path_uri avoid a b = 
+let rec lt_path_uri s 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
+        lt_path_uri s (x::avoid) a x))
+  ) !(s#env_db.lt_constraints)
 ;;
 
-let lt_path a b = lt_path_uri [b] a b;;
+let lt_path s a b = lt_path_uri s [b] a b;;
 
 let universe_eq a b = 
   match a,b with 
@@ -93,23 +144,23 @@ let universe_eq a b =
       (lazy "trying to check if two inferred universes are equal"))
 ;;
 
-let universe_leq a b = 
+let universe_leq s a b = 
   match a, b with
   | (((`Type|`Succ),_)::_ | []) , [`CProp,_] -> false
   | l, [((`Type|`CProp),b)] -> 
        List.for_all 
          (function 
-         | `Succ,a -> lt_path a b 
-         | _, a -> NUri.eq a b || lt_path a b) l
+         | `Succ,a -> lt_path s a b 
+         | _, a -> NUri.eq a b || lt_path s a b) l
   | _, ([] | [`Succ,_] | _::_::_) -> 
      raise (BadConstraint (lazy (
        "trying to check if "^string_of_univ a^
        " is leq than the inferred universe " ^ string_of_univ b)))
 ;;
 
-let are_sorts_convertible ~test_eq_only s1 s2 =
+let are_sorts_convertible st ~test_eq_only s1 s2 =
    match s1,s2 with
-   | C.Type a, C.Type b when not test_eq_only -> universe_leq a b
+   | C.Type a, C.Type b when not test_eq_only -> universe_leq st a b
    | C.Type a, C.Type b -> universe_eq a b
    | C.Prop,C.Type _ -> (not test_eq_only)
    | C.Prop, C.Prop -> true
@@ -120,31 +171,30 @@ let pp_constraint x y =
   NUri.name_of_uri x ^ " < " ^ NUri.name_of_uri y
 ;;
 
-let pp_constraints () =
-  String.concat "\n" (List.map (fun (x,y) -> pp_constraint x y) !lt_constraints)
+let pp_constraints s =
+  String.concat "\n" (List.map (fun (x,y) -> pp_constraint x y)
+   !(s#env_db.lt_constraints))
 ;;
 
-let universes = ref [];;
-
-let get_universes () = 
-  List.map (fun x -> [`Type,x]) !universes @
-  List.map (fun x -> [`CProp,x]) !universes
+let get_universes s = 
+  List.map (fun x -> [`Type,x]) !(s#env_db.universes) @
+  List.map (fun x -> [`CProp,x]) !(s#env_db.universes)
 ;;
 
-let is_declared u =
+let is_declared s u =
  match u with
- | [(`CProp|`Type),x] -> List.exists (fun y -> NUri.eq x y) !universes
+ | [(`CProp|`Type),x] -> List.exists (fun y -> NUri.eq x y) !(s#env_db.universes)
  | _ -> assert false
 ;;
 
 exception UntypableSort of string Lazy.t
 exception AssertFailure of string Lazy.t
 
-let typeof_sort = function
+let typeof_sort s = function
   | C.Type ([(`Type|`CProp),u] as univ) ->
-     if is_declared univ then (C.Type [`Succ, u])
+     if is_declared s univ then (C.Type [`Succ, u])
      else 
-      let universes = !universes in
+      let universes = !(s#env_db.universes) in
        raise (UntypableSort (lazy ("undeclared universe " ^
          NUri.string_of_uri u ^ "\ndeclared ones are: " ^ 
          String.concat ", " (List.map NUri.string_of_uri universes)
@@ -155,76 +205,77 @@ let typeof_sort = function
   | C.Prop -> (C.Type [])
 ;;
 
-let add_lt_constraint a b = 
+let add_lt_constraint s 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 not (lt_path_uri s [] a2 b2) then (
+        if lt_path_uri s [] b2 a2 || NUri.eq a2 b2 then
          (raise(BadConstraint(lazy("universe inconsistency adding "^
                     pp_constraint a2 b2
-           ^ " to:\n" ^ pp_constraints ()))));
-        universes := a2 :: b2 :: 
-          List.filter (fun x -> not (NUri.eq x a2 || NUri.eq x b2)) !universes;
-        lt_constraints := (a2,b2) :: !lt_constraints);
-      history := (`Constr (a,b))::!history;
+           ^ " to:\n" ^ pp_constraints s))));
+        s#env_db.universes := a2 :: b2 :: 
+          List.filter (fun x -> not (NUri.eq x a2 || NUri.eq x b2))
+          !(s#env_db.universes);
+        s#env_db.lt_constraints := (a2,b2) :: !(s#env_db.lt_constraints));
+        s#env_db.history := (`Constr (a,b))::!(s#env_db.history);
   | _ -> raise (BadConstraint
-          (lazy "trying to add a constraint on an inferred universe"))
+          (lazy "trying to add a constraint on an inferred universe"));
 ;;
    
 let family_of = function (`CProp,_)::_ -> `CProp | _ -> `Type ;;
 
-let sup fam l =
+let sup s fam l =
   match l with
   | [(`Type|`CProp),_] -> Some l
   | l ->
    let bigger_than acc (s1,n1) = 
     List.filter
-     (fun x -> lt_path_uri [] n1 x || (s1 <> `Succ && NUri.eq n1 x)) acc 
+     (fun x -> lt_path_uri s [] n1 x || (s1 <> `Succ && NUri.eq n1 x)) acc 
    in
-   let solutions = List.fold_left bigger_than !universes l in
+   let solutions = List.fold_left bigger_than !(s#env_db.universes) l in
    let rec aux = function
      | [] -> None
      | u :: tl ->
-         if List.exists (fun x -> lt_path_uri [] x u) solutions then aux tl
+         if List.exists (fun x -> lt_path_uri s [] x u) solutions then aux tl
          else Some [fam,u]
    in
     aux solutions
 ;;
 
-let sup l = sup (family_of l) l;;
+let sup s l = sup s (family_of l) l;;
 
-let inf ~strict fam l =
+let inf s ~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 
+     (fun x -> lt_path_uri s [] x n1 || (not strict && NUri.eq n1 x)) acc 
    in
-   let solutions = List.fold_left smaller_than !universes l in
+   let solutions = List.fold_left smaller_than !(s#env_db.universes) l in
    let rec aux = function
      | [] -> None
      | u :: tl ->
-         if List.exists (lt_path_uri [] u) solutions then aux tl
+         if List.exists (lt_path_uri s [] u) solutions then aux tl
          else Some [fam,u]
    in
     aux solutions
 ;;
 
-let inf ~strict l = inf ~strict (family_of l) l;;
+let inf s ~strict l = inf s ~strict (family_of l) l;;
 
-let rec universe_lt a b = 
+let rec universe_lt s 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
+             (match sup s [a] with
              | None -> false
-             | Some x -> universe_lt x orig_b) 
-         | _, a -> lt_path a b) l
+             | Some x -> universe_lt s x orig_b) 
+         | _, a -> lt_path s a b) l
   | _, ([] | [`Succ,_] | _::_::_) -> 
      raise (BadConstraint (lazy (
        "trying to check if "^string_of_univ a^
@@ -243,17 +294,6 @@ let allowed_sort_elimination s1 s2 =
   | C.Prop, C.Type _ -> `UnitOnly
 ;;
 
-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
-;;
-
 (* 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
@@ -284,13 +324,13 @@ let invalidate_item item =
 ;;
 *)
 
-let invalidate_item =
- function
-    `Obj (uri,_) -> NUri.UriHash.remove cache uri
+let invalidate_item s o =
+  match o with
+  | `Obj (uri,_) -> NUri.UriHash.remove s#env_db.cache uri
   | `Constr ([_,u1],[_,u2]) -> 
       let w = u1,u2 in
-      lt_constraints := List.filter ((<>) w) !lt_constraints;
-  | `Constr _ -> assert false
+      s#env_db.lt_constraints := List.filter ((<>) w) !(s#env_db.lt_constraints);
+  | `Constr _ -> assert false;
 ;;
 
 exception Propagate of NUri.uri * exn;;
@@ -301,57 +341,59 @@ let to_exn f x =
   | `Exn e -> raise e
 ;;
 
-let check_and_add_obj (status:#NCic.status) ((u,_,_,_,_) as obj) =
- let saved_frozen_list = !frozen_list in
+let check_and_add_obj (status:#status) ((u,_,_,_,_) as obj) =
+ let saved_frozen_list = !(status#env_db.frozen_list) in
  try
-   frozen_list := (u,obj)::saved_frozen_list;
-   HLog.warn ("Typechecking of " ^ NUri.string_of_uri u); 
-   !typecheck_obj (status :> NCic.status) obj;
-   frozen_list := saved_frozen_list;
+   status#env_db.frozen_list := (u,obj)::saved_frozen_list;
+   HLog.warn ("Typechecking of " ^ NUri.string_of_uri u);
+   !typecheck_obj (status :> status) obj;
+   status#env_db.frozen_list := saved_frozen_list;
    let obj' = `WellTyped obj in
-   NUri.UriHash.add cache u obj';
-   history := (`Obj (u,obj))::!history;
+   NUri.UriHash.add status#env_db.cache u obj';
+   status#env_db.history := (`Obj (u,obj))::!(status#env_db.history);
    obj'
  with
     Sys.Break as e ->
-     frozen_list := saved_frozen_list;
+     status#env_db.frozen_list := saved_frozen_list;
      raise e
   | Propagate (u',old_exn) as e' ->
-     frozen_list := saved_frozen_list;
+     status#env_db.frozen_list := saved_frozen_list;
      let exn = `Exn (BadDependency (lazy (NUri.string_of_uri u ^
        " depends (recursively) on " ^ NUri.string_of_uri u' ^
        " which is not well-typed"), 
        match old_exn with BadDependency (_,e) -> e | _ -> old_exn)) in
-     NUri.UriHash.add cache u exn;
-     history := (`Obj (u,obj))::!history;
+     NUri.UriHash.add status#env_db.cache u exn;
+     status#env_db.history := (`Obj (u,obj))::!(status#env_db.history);
      if saved_frozen_list = [] then
       exn
      else
       raise e'
   | e ->
-     frozen_list := saved_frozen_list;
+     status#env_db.frozen_list := saved_frozen_list;
      let exn = `Exn e in
-     NUri.UriHash.add cache u exn;
-     history := (`Obj (u,obj))::!history;
+     NUri.UriHash.add status#env_db.cache u exn;
+     status#env_db.history := (`Obj (u,obj))::!(status#env_db.history);
      if saved_frozen_list = [] then
       exn
      else
       raise (Propagate (u,e))
 ;;
 
-let get_checked_obj status u =
- if List.exists (fun (k,_) -> NUri.eq u k) !frozen_list
+let get_checked_obj (status:#status) u =
+ if List.exists (fun (k,_) -> NUri.eq u k) !(status#env_db.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 status (!get_obj (status :> NCic.status) u)
+  try NUri.UriHash.find status#env_db.cache u
+  with Not_found -> 
+    (* XXX: to be checked carefully *)
+    check_and_add_obj status (!get_obj (status :> status) u)
 ;;
 
-let get_checked_obj (status:#NCic.status) u = to_exn (get_checked_obj status) u;;
+let get_checked_obj status u = to_exn (get_checked_obj status) u;;
 
 let check_and_add_obj status ((u,_,_,_,_) as obj) =
- if NUri.UriHash.mem cache u then
+ if NUri.UriHash.mem status#env_db.cache u then
   raise (AlreadyDefined (lazy (NUri.string_of_uri u)))
  else
   ignore (to_exn (check_and_add_obj status) obj)
@@ -418,7 +460,7 @@ let get_relevance status (Ref.Ref (_, infos) as r) =
 ;;
 
 
-let invalidate _ = 
-  assert (!frozen_list = []);
-  NUri.UriHash.clear cache
+let invalidate s = 
+  assert (!(s#env_db.frozen_list) = []);
+  NUri.UriHash.clear s#env_db.cache
 ;;