From e79c8b830f9f6b0c3f4d577909e32e1bb4032cdf Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Fri, 16 Sep 2011 14:14:15 +0000 Subject: [PATCH] This commit patches the environment and the library so that their status is contained in the global status of Matita. This allows several users to execute concurrently in the same instance of Matita, since they are now using independent statuses. --- .../grafite_engine/grafiteEngine.ml | 17 +- .../components/grafite_engine/grafiteTypes.ml | 2 +- .../grafite_engine/nCicCoercDeclaration.ml | 6 +- .../ng_cic_content/ncic2astMatcher.mli | 2 +- .../ng_disambiguation/grafiteDisambiguate.ml | 15 +- .../ng_disambiguation/grafiteDisambiguate.mli | 5 +- .../ng_disambiguation/nCicDisambiguate.mli | 2 +- matitaB/components/ng_kernel/Makefile | 2 +- .../components/ng_kernel/nCicEnvironment.ml | 222 +++++++++++------- .../components/ng_kernel/nCicEnvironment.mli | 65 +++-- matitaB/components/ng_kernel/nCicPp.ml | 9 +- matitaB/components/ng_kernel/nCicPp.mli | 10 +- matitaB/components/ng_kernel/nCicReduction.ml | 10 +- .../components/ng_kernel/nCicReduction.mli | 16 +- .../components/ng_kernel/nCicSubstitution.mli | 10 +- .../components/ng_kernel/nCicTypeChecker.ml | 8 +- .../components/ng_kernel/nCicTypeChecker.mli | 16 +- .../components/ng_kernel/nCicUntrusted.mli | 14 +- matitaB/components/ng_kernel/nCicUtils.ml | 4 +- matitaB/components/ng_kernel/nCicUtils.mli | 4 +- matitaB/components/ng_library/nCicLibrary.ml | 102 +++++--- matitaB/components/ng_library/nCicLibrary.mli | 26 +- .../ng_paramodulation/nCicParamod.mli | 4 +- .../ng_paramodulation/nCicProof.mli | 2 +- .../components/ng_refiner/nCicMetaSubst.mli | 8 +- .../components/ng_refiner/nCicRefineUtil.mli | 4 +- matitaB/components/ng_refiner/nCicRefiner.ml | 6 +- matitaB/components/ng_refiner/nCicUnifHint.ml | 2 +- .../components/ng_refiner/nCicUnifHint.mli | 2 +- .../components/ng_refiner/nCicUnification.ml | 16 +- .../components/ng_refiner/nCicUnification.mli | 4 +- matitaB/components/ng_tactics/nCicElim.ml | 2 +- matitaB/components/ng_tactics/nCicElim.mli | 4 +- .../ng_tactics/nCicTacReduction.mli | 2 +- matitaB/components/ng_tactics/nnAuto.ml | 2 +- 35 files changed, 379 insertions(+), 246 deletions(-) diff --git a/matitaB/components/grafite_engine/grafiteEngine.ml b/matitaB/components/grafite_engine/grafiteEngine.ml index a0b00150f..cbaa4d93a 100644 --- a/matitaB/components/grafite_engine/grafiteEngine.ml +++ b/matitaB/components/grafite_engine/grafiteEngine.ml @@ -44,7 +44,7 @@ let inject_unification_hint = ~alias_only status = if not alias_only then - let t = refresh_uri_in_term (status :> NCic.status) t in + let t = refresh_uri_in_term (status :> NCicEnvironment.status) t in basic_eval_unification_hint (t,n) status else status @@ -152,10 +152,10 @@ let inject_input_notation = if not alias_only then let l1 = CicNotationParser.refresh_uri_in_checked_l1_pattern - ~refresh_uri_in_term:(refresh_uri_in_term (status:>NCic.status)) + ~refresh_uri_in_term:(refresh_uri_in_term (status:>NCicEnvironment.status)) ~refresh_uri_in_reference l1 in let l2 = NotationUtil.refresh_uri_in_term - ~refresh_uri_in_term:(refresh_uri_in_term (status:>NCic.status)) + ~refresh_uri_in_term:(refresh_uri_in_term (status:>NCicEnvironment.status)) ~refresh_uri_in_reference l2 in basic_eval_input_notation (l1,l2) status @@ -183,10 +183,10 @@ let inject_output_notation = if not alias_only then let l1 = CicNotationParser.refresh_uri_in_checked_l1_pattern - ~refresh_uri_in_term:(refresh_uri_in_term (status:>NCic.status)) + ~refresh_uri_in_term:(refresh_uri_in_term (status:>NCicEnvironment.status)) ~refresh_uri_in_reference l1 in let l2 = NotationUtil.refresh_uri_in_term - ~refresh_uri_in_term:(refresh_uri_in_term (status:>NCic.status)) + ~refresh_uri_in_term:(refresh_uri_in_term (status:>NCicEnvironment.status)) ~refresh_uri_in_reference l2 in basic_eval_output_notation (l1,l2) status @@ -206,7 +206,7 @@ let record_index_obj = let aux l ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference ~alias_only status = - let refresh_uri_in_term = refresh_uri_in_term (status:>NCic.status) in + let refresh_uri_in_term = refresh_uri_in_term (status:>NCicEnvironment.status) in if not alias_only then basic_index_obj (List.map @@ -322,7 +322,7 @@ let inject_constraint = (* NCicLibrary.add_constraint adds the constraint to the NCicEnvironment * and also to the storage (for undo/redo). During inclusion of compiled * files the storage must not be touched. *) - NCicEnvironment.add_lt_constraint u1 u2; + NCicEnvironment.add_lt_constraint status u1 u2; status else status @@ -607,7 +607,8 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = let status = status#set_ng_mode `CommandMode in status) status (NCic.Prop:: - List.map (fun s -> NCic.Type s) (NCicEnvironment.get_universes ())) + List.map (fun s -> NCic.Type s) + (NCicEnvironment.get_universes status)) | _ -> status in let coercions = diff --git a/matitaB/components/grafite_engine/grafiteTypes.ml b/matitaB/components/grafite_engine/grafiteTypes.ml index 5b34158c4..f4ec3309c 100644 --- a/matitaB/components/grafite_engine/grafiteTypes.ml +++ b/matitaB/components/grafite_engine/grafiteTypes.ml @@ -39,7 +39,7 @@ class virtual status = fun (uid : string option) (b : string) -> object (* Warning: #stack and #obj are meaningful iff #ng_mode is `ProofMode *) inherit ([Continuationals.Stack.t] NTacStatus.status uid fake_obj (Continuationals.Stack.empty)) - inherit NCicLibrary.dumpable_status + inherit NCicLibrary.dumpable_status uid inherit NCicLibrary.status uid inherit GrafiteDisambiguate.status uid inherit GrafiteParser.status uid diff --git a/matitaB/components/grafite_engine/nCicCoercDeclaration.ml b/matitaB/components/grafite_engine/nCicCoercDeclaration.ml index a26d5ec7c..cf3c127b9 100644 --- a/matitaB/components/grafite_engine/nCicCoercDeclaration.ml +++ b/matitaB/components/grafite_engine/nCicCoercDeclaration.ml @@ -174,7 +174,7 @@ let src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt = let fresh_uri status prefix suffix = let mk x = NUri.uri_of_string (status#baseuri ^ "/" ^ prefix ^ x ^ suffix) in let rec diverge u i = - if NCicLibrary.aliases_of u = [] then u + if NCicLibrary.aliases_of status u = [] then u else diverge (mk ("__" ^ string_of_int i)) (i+1) in diverge (mk "") 0 @@ -295,7 +295,9 @@ let record_ncoercion = ~refresh_uri_in_reference ~alias_only status = if not alias_only then - List.fold_right (aux ~refresh_uri_in_term:(refresh_uri_in_term (status:>NCic.status))) l status + List.fold_right + (aux ~refresh_uri_in_term:(refresh_uri_in_term + (status:>NCicEnvironment.status))) l status else status in diff --git a/matitaB/components/ng_cic_content/ncic2astMatcher.mli b/matitaB/components/ng_cic_content/ncic2astMatcher.mli index 47721cf4e..50c5e4467 100644 --- a/matitaB/components/ng_cic_content/ncic2astMatcher.mli +++ b/matitaB/components/ng_cic_content/ncic2astMatcher.mli @@ -27,7 +27,7 @@ module Matcher32: sig (** @param l3_patterns level 3 (CIC) patterns (AKA cic_appl_pattern) *) val compiler : - #NCic.status -> + #NCicEnvironment.status -> (NotationPt.cic_appl_pattern * int) list -> (NCic.term -> ((string * NCic.term) list * NCic.term list * int) option) diff --git a/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml b/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml index 4b1bdfcc8..3bede228d 100644 --- a/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml +++ b/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml @@ -54,6 +54,7 @@ class type g_status = class virtual status uid = object (self) inherit Interpretations.status uid + inherit NCicLibrary.status uid val disambiguate_db = initial_status method disambiguate_db = disambiguate_db method set_disambiguate_db v = {< disambiguate_db = v >} @@ -158,13 +159,13 @@ let mk_implicit b = GrafiteAst.Symbol_alias (__Closed_Implicit,None,"Fake Closed Implicit") ;; -let nlookup_in_library +let nlookup_in_library status interactive_user_uri_choice input_or_locate_uri item = match item with | DisambiguateTypes.Id id -> (try - let references = NCicLibrary.resolve id in + let references = NCicLibrary.resolve status id in List.map (fun u -> GrafiteAst.Ident_alias (id,NReference.string_of_reference u) @@ -295,7 +296,7 @@ let diff_obj loc o1 o2 = match o1,o2 with ;; let disambiguate_nterm status expty context metasenv subst thing -= += let newast, metasenv, subst, cic = singleton "first" (NCicDisambiguate.disambiguate_term @@ -303,7 +304,7 @@ let disambiguate_nterm status expty context metasenv subst thing ~aliases:status#disambiguate_db.interpr ~expty ~universe:(status#disambiguate_db.multi_aliases) - ~lookup_in_library:nlookup_in_library + ~lookup_in_library:(nlookup_in_library status) ~mk_choice:(ncic_mk_choice status) ~mk_implicit ~fix_instance ~description_of_alias:GrafiteAst.description_of_alias @@ -311,7 +312,7 @@ let disambiguate_nterm status expty context metasenv subst thing in let _,_,thing' = thing in let diff = diff_term Stdpp.dummy_loc thing' newast in - let status = add_to_interpr status diff + let status = add_to_interpr status diff in metasenv, subst, status, cic ;; @@ -382,7 +383,7 @@ let disambiguate_nobj status ?baseuri (text,prefix_len,obj) = singleton "third" (NCicDisambiguate.disambiguate_obj status - ~lookup_in_library:nlookup_in_library + ~lookup_in_library:(nlookup_in_library status) ~description_of_alias:GrafiteAst.description_of_alias ~mk_choice:(ncic_mk_choice status) ~mk_implicit ~fix_instance ~uri @@ -435,7 +436,7 @@ let aliases_for_objs status refs = List.concat (List.map (fun nref -> - let references = NCicLibrary.aliases_of nref in + let references = NCicLibrary.aliases_of status nref in List.map (fun u -> let name = NCicPp.r2s status true u in diff --git a/matitaB/components/ng_disambiguation/grafiteDisambiguate.mli b/matitaB/components/ng_disambiguation/grafiteDisambiguate.mli index fcea29e43..640f29270 100644 --- a/matitaB/components/ng_disambiguation/grafiteDisambiguate.mli +++ b/matitaB/components/ng_disambiguation/grafiteDisambiguate.mli @@ -36,6 +36,7 @@ class virtual status : object ('self) inherit g_status inherit Interpretations.status + inherit NCicLibrary.status method set_disambiguate_db: db -> 'self method reset_disambiguate_db: unit -> 'self method set_disambiguate_status: #g_status -> 'self @@ -57,7 +58,7 @@ val add_to_disambiguation_univ: (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list -> 'status val aliases_for_objs: - #NCic.status -> NUri.uri list -> + #NCicLibrary.status -> NUri.uri list -> (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list (* args: print function, message (may be empty), status *) @@ -81,7 +82,7 @@ type pattern = (string * NCic.term) list * NCic.term option val disambiguate_npattern: - #NCic.status -> GrafiteAst.npattern Disambiguate.disambiguator_input -> pattern + #NCicEnvironment.status -> GrafiteAst.npattern Disambiguate.disambiguator_input -> pattern val disambiguate_cic_appl_pattern: #status -> diff --git a/matitaB/components/ng_disambiguation/nCicDisambiguate.mli b/matitaB/components/ng_disambiguation/nCicDisambiguate.mli index 6f6bbd1a1..b63f8afaa 100644 --- a/matitaB/components/ng_disambiguation/nCicDisambiguate.mli +++ b/matitaB/components/ng_disambiguation/nCicDisambiguate.mli @@ -55,4 +55,4 @@ val disambiguate_obj : NCic.substitution * NCic.obj) list * bool -val disambiguate_path: #NCic.status -> NotationPt.term -> NCic.term +val disambiguate_path: #NCicEnvironment.status -> NotationPt.term -> NCic.term diff --git a/matitaB/components/ng_kernel/Makefile b/matitaB/components/ng_kernel/Makefile index 35b89f3b1..acf7c9728 100644 --- a/matitaB/components/ng_kernel/Makefile +++ b/matitaB/components/ng_kernel/Makefile @@ -4,9 +4,9 @@ PREDICATES = INTERFACE_FILES = \ nUri.mli \ nReference.mli \ + nCicEnvironment.mli \ nCicUtils.mli \ nCicSubstitution.mli \ - nCicEnvironment.mli \ nCicReduction.mli \ nCicTypeChecker.mli \ nCicUntrusted.mli \ diff --git a/matitaB/components/ng_kernel/nCicEnvironment.ml b/matitaB/components/ng_kernel/nCicEnvironment.ml index 1b155a030..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 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 ;; diff --git a/matitaB/components/ng_kernel/nCicEnvironment.mli b/matitaB/components/ng_kernel/nCicEnvironment.mli index 80fcd2b68..790d72abe 100644 --- a/matitaB/components/ng_kernel/nCicEnvironment.mli +++ b/matitaB/components/ng_kernel/nCicEnvironment.mli @@ -16,41 +16,66 @@ exception ObjectNotFound of string Lazy.t;; exception BadDependency of string Lazy.t * exn;; exception AlreadyDefined of string Lazy.t;; -val set_get_obj: (NCic.status -> NUri.uri -> NCic.obj) -> unit +type item = + [ `Obj of NUri.uri * NCic.obj + | `Constr of NCic.universe * NCic.universe ] +;; -val get_checked_obj: #NCic.status -> NUri.uri -> NCic.obj +type obj_exn = + [ `WellTyped of NCic.obj + | `Exn of exn ] +;; -val check_and_add_obj: #NCic.status -> NCic.obj -> unit +type db -val get_relevance: #NCic.status -> NReference.reference -> bool list +class type g_status = + object + method env_db : db + end + +class virtual status : string option -> + object('self) + inherit NCic.status + inherit g_status + method set_env_db : db -> 'self + method set_env_status : #g_status -> 'self + end + +val set_get_obj : (status -> NUri.uri -> NCic.obj) -> unit +val set_typecheck_obj : (status -> NCic.obj -> unit) -> unit + +val get_checked_obj: #status -> NUri.uri -> NCic.obj + +val check_and_add_obj: #status -> NCic.obj -> unit + +val get_relevance: #status -> NReference.reference -> bool list val get_checked_def: - #NCic.status -> NReference.reference -> + #status -> NReference.reference -> NCic.relevance * string * NCic.term * NCic.term * NCic.c_attr * int (* the last integer is the index of the inductive type in the reference *) val get_checked_indtys: - #NCic.status -> NReference.reference -> + #status -> NReference.reference -> bool * int * NCic.inductiveType list * NCic.i_attr * int val get_checked_fixes_or_cofixes: - #NCic.status -> NReference.reference -> + #status -> NReference.reference -> NCic.inductiveFun list * NCic.f_attr * int -val invalidate_item: +val invalidate_item: + #status -> [ `Obj of NUri.uri * NCic.obj | `Constr of NCic.universe * NCic.universe ] -> unit -val invalidate: unit -> unit - -val set_typecheck_obj: (NCic.status -> NCic.obj -> unit) -> unit +val invalidate: #status -> unit (* =========== universes ============= *) (* utils *) val ppsort : Format.formatter -> NCic.sort -> unit -val pp_constraints: unit -> string -val get_universes: unit -> NCic.universe list +val pp_constraints: #status -> string +val get_universes: #status -> NCic.universe list (* use to type products *) val max: NCic.universe -> NCic.universe -> NCic.universe @@ -58,13 +83,13 @@ val max: NCic.universe -> NCic.universe -> NCic.universe (* raise BadConstraints if the second arg. is an inferred universe or * if the added constraint gives circularity *) exception BadConstraint of string Lazy.t;; -val add_lt_constraint: NCic.universe -> NCic.universe -> unit +val add_lt_constraint: #status -> NCic.universe -> NCic.universe -> unit val universe_eq: NCic.universe -> NCic.universe -> bool -val universe_leq: NCic.universe -> NCic.universe -> bool -val universe_lt: NCic.universe -> NCic.universe -> bool +val universe_leq: #status -> NCic.universe -> NCic.universe -> bool +val universe_lt: #status -> NCic.universe -> NCic.universe -> bool (* checks if s1 <= s2 *) -val are_sorts_convertible: test_eq_only:bool -> NCic.sort -> NCic.sort -> bool +val are_sorts_convertible: #status -> test_eq_only:bool -> NCic.sort -> NCic.sort -> bool (* to type a Match *) val allowed_sort_elimination: NCic.sort -> NCic.sort -> [ `Yes | `UnitOnly ] @@ -72,11 +97,11 @@ val allowed_sort_elimination: NCic.sort -> NCic.sort -> [ `Yes | `UnitOnly ] (* algebraic successor function *) exception UntypableSort of string Lazy.t exception AssertFailure of string Lazy.t -val typeof_sort: NCic.sort -> NCic.sort +val typeof_sort: #status -> NCic.sort -> NCic.sort (* looks for a declared universe that is the least one above the input *) -val sup : NCic.universe -> NCic.universe option -val inf : strict:bool -> NCic.universe -> NCic.universe option +val sup : #status -> NCic.universe -> NCic.universe option +val inf : #status -> strict:bool -> NCic.universe -> NCic.universe option val family_of : NCic.universe -> [ `CProp | `Type ] (* =========== /universes ============= *) diff --git a/matitaB/components/ng_kernel/nCicPp.ml b/matitaB/components/ng_kernel/nCicPp.ml index 84c95f45a..80eb372ae 100644 --- a/matitaB/components/ng_kernel/nCicPp.ml +++ b/matitaB/components/ng_kernel/nCicPp.ml @@ -141,7 +141,7 @@ let ppterm status ~formatter:f ~context ~subst ~metasenv:_ ?(inside_fix=false) t let _,_,t,_ = List.assoc n subst in let hd = NCicSubstitution.subst_meta status lc t in aux ctx - (NCicReduction.head_beta_reduce (status :> NCic.status) ~upto:(List.length args) + (NCicReduction.head_beta_reduce (status :> NCicEnvironment.status) ~upto:(List.length args) (match hd with | NCic.Appl l -> NCic.Appl (l@args) | _ -> NCic.Appl (hd :: args))) @@ -359,8 +359,15 @@ let ppsubst status ~metasenv ?use_subst subst = let ppobj status obj = on_buffer (ppobj status) obj;; +class type cstatus = + object + inherit NCicEnvironment.status + inherit NCic.cstatus + end + class status (uid : string option) = object(self) + inherit NCicEnvironment.status uid (* this method is meant to be overridden in ApplyTransformation *) method user = uid method ppterm = ppterm self diff --git a/matitaB/components/ng_kernel/nCicPp.mli b/matitaB/components/ng_kernel/nCicPp.mli index 06be5b261..fcaa9d199 100644 --- a/matitaB/components/ng_kernel/nCicPp.mli +++ b/matitaB/components/ng_kernel/nCicPp.mli @@ -11,13 +11,19 @@ (* $Id$ *) -val r2s: #NCic.status -> bool -> NReference.reference -> string +val r2s: #NCicEnvironment.status -> bool -> NReference.reference -> string val string_of_flavour: NCic.def_flavour -> string +class type cstatus = + object + inherit NCicEnvironment.status + inherit NCic.cstatus + end + (* low-level pretty printer; all methods are meant to be overridden in ApplyTransformation *) -class status: string option -> NCic.cstatus +class status: string option -> cstatus (* variants that use a formatter module Format : sig diff --git a/matitaB/components/ng_kernel/nCicReduction.ml b/matitaB/components/ng_kernel/nCicReduction.ml index 8a84810a3..4fd42aa28 100644 --- a/matitaB/components/ng_kernel/nCicReduction.ml +++ b/matitaB/components/ng_kernel/nCicReduction.ml @@ -208,18 +208,18 @@ let whd = R.whd let (===) x y = Pervasives.compare x y = 0 ;; -let get_relevance = ref (fun _ ~metasenv:_ ~subst:_ _ _ -> assert false);; +let get_relevance = ref (fun (_:#NCicEnvironment.status) ~metasenv:_ ~subst:_ _ _ -> assert false);; let set_get_relevance = (:=) get_relevance;; -let alpha_eq (status:#NCic.status) ~test_lambda_source aux test_eq_only metasenv subst context +let alpha_eq (status:#NCicEnvironment.status) ~test_lambda_source aux test_eq_only metasenv subst context t1 t2 = if t1 === t2 then true else match (t1,t2) with | C.Sort s1, C.Sort s2 -> - NCicEnvironment.are_sorts_convertible ~test_eq_only s1 s2 + NCicEnvironment.are_sorts_convertible status ~test_eq_only s1 s2 | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) -> aux true context s1 s2 && @@ -285,7 +285,7 @@ let alpha_eq (status:#NCic.status) ~test_lambda_source aux test_eq_only metasenv with Invalid_argument _ -> false | HExtlib.FailureAt fail -> let relevance = - !get_relevance (status :> NCic.status) ~metasenv ~subst context hd1 tl1 in + !get_relevance (status :> NCicEnvironment.status) ~metasenv ~subst context hd1 tl1 in let _,relevance = HExtlib.split_nth fail relevance in let b,relevance = (match relevance with | [] -> assert false @@ -302,7 +302,7 @@ let alpha_eq (status:#NCic.status) ~test_lambda_source aux test_eq_only metasenv | (C.Appl (hd1::tl1), C.Appl (hd2::tl2)) -> aux test_eq_only context hd1 hd2 && - let relevance = !get_relevance (status :> NCic.status) ~metasenv ~subst context hd1 tl1 in + let relevance = !get_relevance (status :> NCicEnvironment.status) ~metasenv ~subst context hd1 tl1 in (try HExtlib.list_forall_default3 (fun t1 t2 b -> not b || aux true context t1 t2) diff --git a/matitaB/components/ng_kernel/nCicReduction.mli b/matitaB/components/ng_kernel/nCicReduction.mli index f53cb5dc8..afe09ddae 100644 --- a/matitaB/components/ng_kernel/nCicReduction.mli +++ b/matitaB/components/ng_kernel/nCicReduction.mli @@ -16,15 +16,15 @@ exception AssertFailure of string Lazy.t;; val debug: bool ref val whd : - #NCic.status -> ?delta:int -> subst:NCic.substitution -> + #NCicEnvironment.status -> ?delta:int -> subst:NCic.substitution -> NCic.context -> NCic.term -> NCic.term val set_get_relevance : - (NCic.status -> metasenv:NCic.metasenv -> subst:NCic.substitution -> + (NCicEnvironment.status -> metasenv:NCic.metasenv -> subst:NCic.substitution -> NCic.context -> NCic.term -> NCic.term list -> bool list) -> unit val are_convertible : - #NCic.status -> metasenv:NCic.metasenv -> subst:NCic.substitution -> + #NCicEnvironment.status -> metasenv:NCic.metasenv -> subst:NCic.substitution -> NCic.context -> NCic.term -> NCic.term -> bool @@ -32,7 +32,7 @@ val are_convertible : delta reduction; if provided, ~upto is the maximum number of beta redexes reduced *) val head_beta_reduce: - #NCic.status -> ?delta:int -> ?upto:int -> ?subst:NCic.substitution -> + #NCicEnvironment.status -> ?delta:int -> ?upto:int -> ?subst:NCic.substitution -> NCic.term -> NCic.term type stack_item @@ -41,17 +41,17 @@ type environment_item type machine = int * environment_item list * NCic.term * stack_item list val reduce_machine : - #NCic.status -> delta:int -> ?subst:NCic.substitution -> NCic.context -> + #NCicEnvironment.status -> delta:int -> ?subst:NCic.substitution -> NCic.context -> machine -> machine * bool val from_stack : delta:int -> stack_item -> machine val from_env : delta:int -> environment_item -> machine -val unwind : #NCic.status -> machine -> NCic.term +val unwind : #NCicEnvironment.status -> machine -> NCic.term val split_prods: - #NCic.status -> subst:NCic.substitution -> NCic.context -> int -> NCic.term -> + #NCicEnvironment.status -> subst:NCic.substitution -> NCic.context -> int -> NCic.term -> NCic.context * NCic.term (* to be used outside the kernel *) val alpha_eq: - #NCic.status -> NCic.metasenv -> NCic.substitution -> NCic.context -> + #NCicEnvironment.status -> NCic.metasenv -> NCic.substitution -> NCic.context -> NCic.term -> NCic.term -> bool diff --git a/matitaB/components/ng_kernel/nCicSubstitution.mli b/matitaB/components/ng_kernel/nCicSubstitution.mli index 9ba2d11fa..8db93d0c0 100644 --- a/matitaB/components/ng_kernel/nCicSubstitution.mli +++ b/matitaB/components/ng_kernel/nCicSubstitution.mli @@ -11,14 +11,14 @@ (* $Id$ *) -val lift_from : #NCic.status -> ?no_implicit:bool -> int -> int -> NCic.term -> NCic.term +val lift_from : #NCicEnvironment.status -> ?no_implicit:bool -> int -> int -> NCic.term -> NCic.term (* lift n t *) (* lifts [t] of [n] *) (* [from] default 1, lifts only indexes >= [from] *) (* NOTE: the opposite function (delift_rels) is defined in CicMetaSubst *) (* since it needs to restrict the metavariables in case of failure *) -val lift : #NCic.status -> ?from:int -> ?no_implicit:bool -> int -> NCic.term -> NCic.term +val lift : #NCicEnvironment.status -> ?from:int -> ?no_implicit:bool -> int -> NCic.term -> NCic.term (* subst t1 t2 *) (* substitutes [t1] for [Rel 1] in [t2] *) @@ -26,7 +26,7 @@ val lift : #NCic.status -> ?from:int -> ?no_implicit:bool -> int -> NCic.term -> (* are generated. WARNING: the substitution can diverge when t2 is not *) (* well typed and avoid_beta_redexes is true. *) val subst : - #NCic.status -> ?avoid_beta_redexes:bool -> ?no_implicit:bool -> + #NCicEnvironment.status -> ?avoid_beta_redexes:bool -> ?no_implicit:bool -> NCic.term -> NCic.term -> NCic.term (* psubst [avoid] [map_arg] [args] [t] @@ -37,7 +37,7 @@ val subst : * the function is ReductionStrategy.from_env_for_unwind when psubst is * used to implement nCicReduction.unwind' *) val psubst : - #NCic.status -> ?avoid_beta_redexes:bool -> ?no_implicit:bool -> + #NCicEnvironment.status -> ?avoid_beta_redexes:bool -> ?no_implicit:bool -> ('a -> NCic.term) -> 'a list -> NCic.term -> NCic.term @@ -45,5 +45,5 @@ val psubst : (* returns the term [t] where [Rel i] is substituted with [t_i] lifted by n *) (* [t_i] is lifted as usual when it crosses an abstraction *) (* subst_meta (n, Irl _) t -> lift n t *) -val subst_meta : #NCic.status -> NCic.local_context -> NCic.term -> NCic.term +val subst_meta : #NCicEnvironment.status -> NCic.local_context -> NCic.term -> NCic.term diff --git a/matitaB/components/ng_kernel/nCicTypeChecker.ml b/matitaB/components/ng_kernel/nCicTypeChecker.ml index 0a73358e0..489b89287 100644 --- a/matitaB/components/ng_kernel/nCicTypeChecker.ml +++ b/matitaB/components/ng_kernel/nCicTypeChecker.ml @@ -382,7 +382,7 @@ let type_of_branch (status:#NCic.status) ~subst context leftno outty cons tycons ;; -let rec typeof (status:#NCic.status) ~subst ~metasenv context term = +let rec typeof (status:#NCicEnvironment.status) ~subst ~metasenv context term = let rec typeof_aux context = fun t -> (*prerr_endline (status#ppterm ~metasenv ~subst ~context t);*) match t with @@ -395,7 +395,7 @@ let rec typeof (status:#NCic.status) ~subst ~metasenv context term = raise (TypeCheckerFailure (lazy ("unbound variable " ^ string_of_int n ^" under: " ^ status#ppcontext ~metasenv ~subst context)))) | C.Sort s -> - (try C.Sort (NCicEnvironment.typeof_sort s) + (try C.Sort (NCicEnvironment.typeof_sort status s) with | NCicEnvironment.UntypableSort msg -> raise (TypeCheckerFailure msg) | NCicEnvironment.AssertFailure msg -> raise (AssertFailure msg)) @@ -793,7 +793,7 @@ and check_mutual_inductive_defs status uri ~metasenv ~subst leftno tyl = let con_sort = typeof status ~subst ~metasenv context te in (match R.whd status ~subst context con_sort, R.whd status ~subst [] ty_sort with (C.Sort (C.Type u1) as s1), (C.Sort (C.Type u2) as s2) -> - if not (E.universe_leq u1 u2) then + if not (E.universe_leq status u1 u2) then raise (TypeCheckerFailure (lazy ("The type " ^ status#ppterm ~metasenv ~subst ~context s1^ @@ -1114,7 +1114,7 @@ and type_of_constant status ((Ref.Ref (uri,_)) as ref) = (lazy ("type_of_constant: environment/reference: " ^ Ref.string_of_reference ref))) -and get_relevance status ~metasenv ~subst context t args = +and get_relevance (status:#NCicEnvironment.status) ~metasenv ~subst context t args = let ty = typeof status ~subst ~metasenv context t in let rec aux context ty = function | [] -> [] diff --git a/matitaB/components/ng_kernel/nCicTypeChecker.mli b/matitaB/components/ng_kernel/nCicTypeChecker.mli index 6ca329fbf..cbbc770f0 100644 --- a/matitaB/components/ng_kernel/nCicTypeChecker.mli +++ b/matitaB/components/ng_kernel/nCicTypeChecker.mli @@ -26,21 +26,21 @@ val set_logger: val set_trust : (NCic.obj -> bool) -> unit val typeof: - #NCic.status -> subst:NCic.substitution -> metasenv:NCic.metasenv -> + #NCicEnvironment.status -> subst:NCic.substitution -> metasenv:NCic.metasenv -> NCic.context -> NCic.term -> NCic.term val height_of_obj_kind: - #NCic.status -> NUri.uri -> subst:NCic.substitution -> NCic.obj_kind -> int + #NCicEnvironment.status -> NUri.uri -> subst:NCic.substitution -> NCic.obj_kind -> int val get_relevance : - #NCic.status -> + #NCicEnvironment.status -> metasenv:NCic.metasenv -> subst:NCic.substitution -> NCic.context -> NCic.term -> NCic.term list -> bool list (* type_of_branch subst context leftno outtype * (constr @ lefts) (ty_constr @ lefts) *) val type_of_branch : - #NCic.status -> + #NCicEnvironment.status -> subst:NCic.substitution -> NCic.context -> int -> NCic.term -> NCic.term -> NCic.term -> NCic.term @@ -49,7 +49,7 @@ val type_of_branch : * arity1 = constructor type @ lefts * arity2 = outtype *) val check_allowed_sort_elimination : - #NCic.status -> + #NCicEnvironment.status -> subst:NCic.substitution -> metasenv:NCic.metasenv -> NReference.reference -> NCic.context -> @@ -57,13 +57,13 @@ val check_allowed_sort_elimination : (* Functions to be used by the refiner *) val debruijn: - #NCic.status -> NUri.uri -> int -> subst:NCic.substitution -> NCic.context -> + #NCicEnvironment.status -> NUri.uri -> int -> subst:NCic.substitution -> NCic.context -> NCic.term -> NCic.term val are_all_occurrences_positive: - #NCic.status -> subst:NCic.substitution -> NCic.context -> NUri.uri -> int -> + #NCicEnvironment.status -> subst:NCic.substitution -> NCic.context -> NUri.uri -> int -> int -> int -> int -> NCic.term -> bool val does_not_occur : - #NCic.status -> subst:NCic.substitution -> NCic.context -> int -> int -> + #NCicEnvironment.status -> subst:NCic.substitution -> NCic.context -> int -> int -> NCic.term -> bool diff --git a/matitaB/components/ng_kernel/nCicUntrusted.mli b/matitaB/components/ng_kernel/nCicUntrusted.mli index 7967936e3..b085be307 100644 --- a/matitaB/components/ng_kernel/nCicUntrusted.mli +++ b/matitaB/components/ng_kernel/nCicUntrusted.mli @@ -12,7 +12,7 @@ (* $Id$ *) val map_term_fold_a: - #NCic.status -> + #NCicEnvironment.status -> (NCic.hypothesis -> 'k -> 'k) -> 'k -> ('k -> 'a -> NCic.term -> 'a * NCic.term) -> 'a -> NCic.term -> 'a * NCic.term @@ -20,9 +20,9 @@ val map_obj_kind: ?skip_body:bool -> (NCic.term -> NCic.term) -> NCic.obj_kind -> NCic.obj_kind val metas_of_term : - #NCic.status -> NCic.substitution -> NCic.context -> NCic.term -> int list + #NCicEnvironment.status -> NCic.substitution -> NCic.context -> NCic.term -> int list val sort_metasenv: - #NCic.status -> NCic.substitution -> NCic.metasenv -> NCic.metasenv + #NCicEnvironment.status -> NCic.substitution -> NCic.metasenv -> NCic.metasenv type meta_kind = [ `IsSort | `IsType | `IsTerm ] val kind_of_meta: NCic.meta_attrs -> meta_kind @@ -40,14 +40,14 @@ val mk_appl : NCic.term -> NCic.term list -> NCic.term (* the context is needed only to honour Barendregt's naming convention *) val apply_subst : - #NCic.status -> NCic.substitution -> NCic.context -> NCic.term -> NCic.term + #NCicEnvironment.status -> NCic.substitution -> NCic.context -> NCic.term -> NCic.term val apply_subst_context : - #NCic.status -> fix_projections:bool -> + #NCicEnvironment.status -> fix_projections:bool -> NCic.substitution -> NCic.context -> NCic.context val apply_subst_metasenv : - #NCic.status -> NCic.substitution -> NCic.metasenv -> NCic.metasenv + #NCicEnvironment.status -> NCic.substitution -> NCic.metasenv -> NCic.metasenv val count_occurrences : - #NCic.status -> subst:NCic.substitution -> int -> NCic.term -> int + #NCicEnvironment.status -> subst:NCic.substitution -> int -> NCic.term -> int (* quick, but with false negatives (since no ~subst), check for closed terms *) val looks_closed : NCic.term -> bool diff --git a/matitaB/components/ng_kernel/nCicUtils.ml b/matitaB/components/ng_kernel/nCicUtils.ml index f22e02a7e..400d69363 100644 --- a/matitaB/components/ng_kernel/nCicUtils.ml +++ b/matitaB/components/ng_kernel/nCicUtils.ml @@ -17,7 +17,7 @@ module Ref = NReference exception Subst_not_found of int exception Meta_not_found of int -let head_beta_reduce = ref (fun _ ~upto:_ _ -> assert false);; +let head_beta_reduce = ref (fun (_:NCicEnvironment.status) ~upto:_ _ -> assert false);; let set_head_beta_reduce = (:=) head_beta_reduce;; let expand_local_context = function @@ -74,7 +74,7 @@ let map status g k f = function | C.Appl l :: tl -> C.Appl (l@tl) | l1 -> C.Appl l1 in - if fire_beta then !head_beta_reduce (status :> NCic.status) ~upto t + if fire_beta then !head_beta_reduce (status :> NCicEnvironment.status) ~upto t else t | C.Prod (n,s,t) as orig -> let s1 = f k s in let t1 = f (g (n,C.Decl s) k) t in diff --git a/matitaB/components/ng_kernel/nCicUtils.mli b/matitaB/components/ng_kernel/nCicUtils.mli index 6697e31b5..de56c4e1f 100644 --- a/matitaB/components/ng_kernel/nCicUtils.mli +++ b/matitaB/components/ng_kernel/nCicUtils.mli @@ -25,9 +25,9 @@ val fold: (NCic.hypothesis -> 'k -> 'k) -> 'k -> ('k -> 'a -> NCic.term -> 'a) -> 'a -> NCic.term -> 'a val map: - #NCic.status -> + #NCicEnvironment.status -> (NCic.hypothesis -> 'k -> 'k) -> 'k -> ('k -> NCic.term -> NCic.term) -> NCic.term -> NCic.term -val set_head_beta_reduce: (NCic.status -> upto:int -> NCic.term -> NCic.term) -> unit +val set_head_beta_reduce: (NCicEnvironment.status -> upto:int -> NCic.term -> NCic.term) -> unit diff --git a/matitaB/components/ng_library/nCicLibrary.ml b/matitaB/components/ng_library/nCicLibrary.ml index 6cb4029cf..b775bff00 100644 --- a/matitaB/components/ng_library/nCicLibrary.ml +++ b/matitaB/components/ng_library/nCicLibrary.ml @@ -88,8 +88,6 @@ type timestamp = ;; let time0 = [],[];; -let storage = ref [];; -let local_aliases = ref [];; let load_db,set_global_aliases,get_global_aliases,add_deps,get_deps,remove_deps= let global_aliases = ref [] in @@ -148,23 +146,52 @@ let load_db,set_global_aliases,get_global_aliases,add_deps,get_deps,remove_deps= let init = load_db;; +type db = { + storage : + [ `Obj of NUri.uri * NCic.obj + | `Constr of NCic.universe * NCic.universe] list ref; + local_aliases : + (NUri.uri * string * NReference.reference) list ref +} + +class type g_status = + object + method lib_db : db + end + class virtual status uid = object - inherit NCic.status uid + inherit NCicEnvironment.status uid + + val lib_db = { + storage = ref []; + local_aliases = ref [] + } + method lib_db = lib_db + val timestamp = (time0 : timestamp) method timestamp = timestamp + method set_timestamp v = {< timestamp = v >} + method set_lib_db v = {< lib_db = v >} + method set_lib_status : 's.#g_status as 's -> 'self + = fun o -> {< lib_db = o#lib_db >} end -let time_travel0 (sto,ali) = - let diff_len = List.length !storage - List.length sto in - let to_be_deleted,_ = HExtlib.split_nth diff_len !storage in +let reset_timestamp st = + st#lib_db.storage := []; + st#lib_db.local_aliases := [] +;; + +let time_travel0 st (sto,ali) = + let diff_len = List.length !(st#lib_db.storage) - List.length sto in + let to_be_deleted,_ = HExtlib.split_nth diff_len !(st#lib_db.storage) in if List.length to_be_deleted > 0 then - List.iter NCicEnvironment.invalidate_item to_be_deleted; - storage := sto; local_aliases := ali + List.iter (NCicEnvironment.invalidate_item st) to_be_deleted; + st#lib_db.storage := sto; st#lib_db.local_aliases := ali ;; -let time_travel status = time_travel0 status#timestamp;; +let time_travel status = time_travel0 status status#timestamp;; type obj = string * Obj.t (* includes are transitively closed; dependencies are only immediate *) @@ -177,8 +204,11 @@ class type g_dumpable_status = end (* uid = None --> single user mode *) -class dumpable_status = +class dumpable_status uid = object + inherit NCicPp.status uid + inherit status uid + val db = { objs = []; includes = []; dependencies = [] } method dump = db method set_dump v = {< db = v >} @@ -202,7 +232,7 @@ module type SerializerType = type 'a register_type = 'a -> refresh_uri_in_universe:(NCic.universe -> NCic.universe) -> - refresh_uri_in_term:(NCic.status -> NCic.term -> NCic.term) -> + refresh_uri_in_term:(NCicEnvironment.status -> NCic.term -> NCic.term) -> refresh_uri_in_reference:(NReference.reference -> NReference.reference) -> alias_only:bool -> dumpable_status -> dumpable_status @@ -216,14 +246,14 @@ module type SerializerType = end module Serializer(D: sig type dumpable_s val get: dumpable_s -> dumpable_status - val set: dumpable_s -> dumpable_status -> dumpable_s val user : dumpable_s -> - string option end) = + val set: dumpable_s -> dumpable_status -> dumpable_s (*val user : dumpable_s -> + string option*) end) = struct type dumpable_status = D.dumpable_s type 'a register_type = 'a -> refresh_uri_in_universe:(NCic.universe -> NCic.universe) -> - refresh_uri_in_term:(NCic.status -> NCic.term -> NCic.term) -> + refresh_uri_in_term:(NCicEnvironment.status -> NCic.term -> NCic.term) -> refresh_uri_in_reference:(NReference.reference -> NReference.reference) -> alias_only:bool -> dumpable_status -> dumpable_status @@ -252,7 +282,7 @@ module Serializer(D: sig type dumpable_s val get: dumpable_s -> dumpable_status end let serialize ~baseuri status = - let ch = open_out (ng_path_of_baseuri (D.user status) baseuri) in + let ch = open_out (ng_path_of_baseuri (D.get status)#user baseuri) in Marshal.to_channel ch (magic,((D.get status)#dump.dependencies,(D.get status)#dump.objs)) []; close_out ch; let deps = String.concat ", " ((D.get status)#dump.dependencies) in @@ -260,14 +290,14 @@ module Serializer(D: sig type dumpable_s val get: dumpable_s -> dumpable_status List.iter (function | `Obj (uri,obj) -> - let ch = open_out (ng_path_of_baseuri (D.user status) uri) in + let ch = open_out (ng_path_of_baseuri (D.get status)#user uri) in Marshal.to_channel ch (magic,obj) []; close_out ch | `Constr _ -> () - ) !storage; - set_global_aliases (!local_aliases @ get_global_aliases ()); + ) !((D.get status)#lib_db.storage); + set_global_aliases (!((D.get status)#lib_db.local_aliases) @ get_global_aliases ()); List.iter (fun u -> add_deps u [baseuri]) (D.get status)#dump.includes; - time_travel0 time0 + reset_timestamp (D.get status) let require2 ~baseuri ~alias_only status = try @@ -277,11 +307,11 @@ module Serializer(D: sig type dumpable_s val get: dumpable_s -> dumpable_status (s#set_dump {s#dump with includes = baseuri::List.filter ((<>) baseuri) s#dump.includes}) in - let _dependencies,dump = require0 (D.user status) ~baseuri in + let _dependencies,dump = require0 (D.get status)#user ~baseuri in List.fold_right (!require1 ~alias_only) dump status with Sys_error _ -> - raise (IncludedFileNotCompiled(ng_path_of_baseuri (D.user status) baseuri,NUri.string_of_uri baseuri)) + raise (IncludedFileNotCompiled(ng_path_of_baseuri (D.get status)#user baseuri,NUri.string_of_uri baseuri)) let dependencies_of user ~baseuri = fst (require0 user ~baseuri) @@ -324,24 +354,24 @@ let fetch_obj user status uri = refresh_uri_in_obj status obj ;; -let resolve name = +let resolve st name = try HExtlib.filter_map (fun (_,name',nref) -> if name'=name then Some nref else None) - (!local_aliases @ get_global_aliases ()) + (!(st#lib_db.local_aliases) @ get_global_aliases ()) with Not_found -> raise (NCicEnvironment.ObjectNotFound (lazy name)) ;; -let aliases_of uri = +let aliases_of st uri = HExtlib.filter_map (fun (uri',_,nref) -> - if NUri.eq uri' uri then Some nref else None) !local_aliases + if NUri.eq uri' uri then Some nref else None) !(st#lib_db.local_aliases) ;; let add_obj status ((u,_,_,_,_) as obj) = NCicEnvironment.check_and_add_obj status obj; - storage := (`Obj (u,obj))::!storage; + status#lib_db.storage := (`Obj (u,obj))::!(status#lib_db.storage); let _,height,_,_,obj = obj in let references = match obj with @@ -370,33 +400,35 @@ let add_obj status ((u,_,_,_,_) as obj) = (NReference.Ind (inductive,i,leftno))] ) il) in - local_aliases := references @ !local_aliases; - status#set_timestamp (!storage,!local_aliases) + status#lib_db.local_aliases := references @ !(status#lib_db.local_aliases); + status#set_timestamp (!(status#lib_db.storage),!(status#lib_db.local_aliases)) ;; let add_constraint status u1 u2 = if List.exists (function `Constr (u1',u2') when u1=u1' && u2=u2' -> true | _ -> false) - !storage + !(status#lib_db.storage) then (*CSC: raise an exception here! *) (prerr_endline "CANNOT ADD A CONSTRAINT TWICE"; assert false); - NCicEnvironment.add_lt_constraint u1 u2; - storage := (`Constr (u1,u2)) :: !storage; - status#set_timestamp (!storage,!local_aliases) + NCicEnvironment.add_lt_constraint status u1 u2; + status#lib_db.storage := (`Constr (u1,u2)) :: !(status#lib_db.storage); + status#set_timestamp (!(status#lib_db.storage),!(status#lib_db.local_aliases)) ;; let get_obj status u = +(* try List.assq u (HExtlib.filter_map (function `Obj (u,o) -> Some (u,o) | _ -> None ) - !storage) - with Not_found -> + !(status#lib_db.storage)) + with Not_found ->*) try fetch_obj (status#user) status u with Sys_error _ -> raise (NCicEnvironment.ObjectNotFound (lazy (NUri.string_of_uri u))) ;; -NCicEnvironment.set_get_obj get_obj;; +NCicEnvironment.set_get_obj + (get_obj :> NCicEnvironment.status -> NUri.uri -> NCic.obj);; diff --git a/matitaB/components/ng_library/nCicLibrary.mli b/matitaB/components/ng_library/nCicLibrary.mli index 89e701fc1..cba90c30c 100644 --- a/matitaB/components/ng_library/nCicLibrary.mli +++ b/matitaB/components/ng_library/nCicLibrary.mli @@ -16,22 +16,35 @@ exception IncludedFileNotCompiled of string * string type timestamp +type db + +class type g_status = + object + method lib_db : db + end + class virtual status : string option -> object ('self) - inherit NCic.status + inherit NCicEnvironment.status + inherit g_status + method lib_db: db method timestamp: timestamp method set_timestamp: timestamp -> 'self + method set_lib_db: db -> 'self + method set_lib_status: #g_status -> 'self end (* it also checks it and add it to the environment *) val add_obj: #status as 'status -> NCic.obj -> 'status val add_constraint: #status as 'status -> NCic.universe -> NCic.universe -> 'status -val aliases_of: NUri.uri -> NReference.reference list -val resolve: string -> NReference.reference list +val aliases_of: #status -> NUri.uri -> NReference.reference list +val resolve: #status -> string -> NReference.reference list +(* (* warning: get_obj may raise (NCicEnvironment.ObjectNotFoud l) *) val get_obj: #NCic.status -> NUri.uri -> NCic.obj (* changes the current timestamp *) +*) val time_travel: #status -> unit @@ -45,9 +58,12 @@ class type g_dumpable_status = method dump: dump end -class dumpable_status : +class dumpable_status : + string option -> object ('self) inherit g_dumpable_status + inherit NCicPp.status + inherit status method set_dump: dump -> 'self method set_dumpable_status: #g_dumpable_status -> 'self end @@ -62,7 +78,7 @@ module type SerializerType = type 'a register_type = 'a -> refresh_uri_in_universe:(NCic.universe -> NCic.universe) -> - refresh_uri_in_term:(NCic.status -> NCic.term -> NCic.term) -> + refresh_uri_in_term:(NCicEnvironment.status -> NCic.term -> NCic.term) -> refresh_uri_in_reference:(NReference.reference -> NReference.reference) -> alias_only:bool -> dumpable_status -> dumpable_status diff --git a/matitaB/components/ng_paramodulation/nCicParamod.mli b/matitaB/components/ng_paramodulation/nCicParamod.mli index 36c5a7cab..2856ebac9 100644 --- a/matitaB/components/ng_paramodulation/nCicParamod.mli +++ b/matitaB/components/ng_paramodulation/nCicParamod.mli @@ -20,9 +20,9 @@ val nparamod : type state val empty_state: state val forward_infer_step: state -> NCic.term -> NCic.term -> state -val index_obj: #NCic.status -> state -> NUri.uri -> state +val index_obj: #NCicEnvironment.status -> state -> NUri.uri -> state val is_equation: - #NCic.status -> NCic.metasenv -> NCic.substitution -> NCic.context -> + #NCicEnvironment.status -> NCic.metasenv -> NCic.substitution -> NCic.context -> NCic.term -> bool val paramod : #NCicCoercion.status -> diff --git a/matitaB/components/ng_paramodulation/nCicProof.mli b/matitaB/components/ng_paramodulation/nCicProof.mli index 5baa10535..78023c0a6 100644 --- a/matitaB/components/ng_paramodulation/nCicProof.mli +++ b/matitaB/components/ng_paramodulation/nCicProof.mli @@ -17,7 +17,7 @@ val set_default_sig: unit -> unit val get_sig: eq_sig_type -> NCic.term val mk_proof: - #NCic.status -> + #NCicEnvironment.status -> ?demod:bool -> NCic.term Terms.bag -> Terms.M.key diff --git a/matitaB/components/ng_refiner/nCicMetaSubst.mli b/matitaB/components/ng_refiner/nCicMetaSubst.mli index c9530d42d..6894129c8 100644 --- a/matitaB/components/ng_refiner/nCicMetaSubst.mli +++ b/matitaB/components/ng_refiner/nCicMetaSubst.mli @@ -35,7 +35,7 @@ val maxmeta: unit -> int * in the term (for occur check). *) val delift : - #NCic.status -> + #NCicEnvironment.status -> unify:(NCic.metasenv -> NCic.substitution -> NCic.context -> NCic.term -> NCic.term -> (NCic.metasenv * NCic.substitution) option) -> NCic.metasenv -> NCic.substitution -> NCic.context -> @@ -47,7 +47,7 @@ val delift : additional (i.e. l' does not intersects l) positions whose restriction was forced because of type dependencies *) val restrict: - #NCic.status -> + #NCicEnvironment.status -> NCic.metasenv -> NCic.substitution -> int -> int list -> @@ -65,7 +65,7 @@ val extend_meta: NCic.metasenv -> int -> NCic.metasenv * NCic.term (* returns the resulting type, the metasenv and the arguments *) val saturate: - #NCic.status -> + #NCicEnvironment.status -> ?delta:int -> NCic.metasenv -> NCic.substitution -> NCic.context -> NCic.term -> int -> NCic.term * NCic.metasenv * NCic.term list @@ -76,4 +76,4 @@ val is_out_scope_tag : NCic.meta_attrs -> bool val int_of_out_scope_tag : NCic.meta_attrs -> int val is_flexible: - #NCic.status -> NCic.context -> subst:NCic.substitution -> NCic.term -> bool + #NCicEnvironment.status -> NCic.context -> subst:NCic.substitution -> NCic.term -> bool diff --git a/matitaB/components/ng_refiner/nCicRefineUtil.mli b/matitaB/components/ng_refiner/nCicRefineUtil.mli index 228342378..f87c927d6 100644 --- a/matitaB/components/ng_refiner/nCicRefineUtil.mli +++ b/matitaB/components/ng_refiner/nCicRefineUtil.mli @@ -11,10 +11,10 @@ (* $Id: nCicRefiner.ml 9802 2009-05-25 15:39:26Z tassi $ *) -val alpha_equivalence : #NCic.status -> NCic.term -> NCic.term -> bool +val alpha_equivalence : #NCicEnvironment.status -> NCic.term -> NCic.term -> bool val replace_lifting : - #NCic.status -> + #NCicEnvironment.status -> equality:((string * NCic.context_entry) list -> NCic.term -> NCic.term -> bool) -> context:(string * NCic.context_entry) list -> diff --git a/matitaB/components/ng_refiner/nCicRefiner.ml b/matitaB/components/ng_refiner/nCicRefiner.ml index 4645e6f6e..8deb72797 100644 --- a/matitaB/components/ng_refiner/nCicRefiner.ml +++ b/matitaB/components/ng_refiner/nCicRefiner.ml @@ -189,7 +189,7 @@ let rec typeof (status:#NCicCoercion.status) in metasenv, subst, t, infty | C.Sort s -> - (try metasenv, subst, t, C.Sort (NCicEnvironment.typeof_sort s) + (try metasenv, subst, t, C.Sort (NCicEnvironment.typeof_sort status s) with | NCicEnvironment.UntypableSort msg -> raise (RefineFailure (lazy (localise t, Lazy.force msg))) @@ -855,7 +855,7 @@ and force_to_sort status metasenv subst context t orig_t localise ty = let ty = NCicReduction.whd status ~subst context ty in try_coercions status ~localise metasenv subst context t orig_t ty (NCic.Sort (NCic.Type - (match NCicEnvironment.get_universes () with + (match NCicEnvironment.get_universes status with | x::_ -> x | _ -> assert false))) false (Uncertain (lazy (localise orig_t, @@ -1204,7 +1204,7 @@ let typeof_obj NCicReduction.whd status ~subst [] ty_sort with (C.Sort (C.Type u1) as s1), (C.Sort (C.Type u2) as s2) -> - if not (NCicEnvironment.universe_leq u1 u2) then + if not (NCicEnvironment.universe_leq status u1 u2) then raise (RefineFailure (lazy(localise te, "The type " ^ diff --git a/matitaB/components/ng_refiner/nCicUnifHint.ml b/matitaB/components/ng_refiner/nCicUnifHint.ml index 960ead117..d228db7b6 100644 --- a/matitaB/components/ng_refiner/nCicUnifHint.ml +++ b/matitaB/components/ng_refiner/nCicUnifHint.ml @@ -53,7 +53,7 @@ class type g_status = class virtual status (uid : string option) = object - inherit NCic.status uid + inherit NCicEnvironment.status uid val db = HDB.empty, EQDB.empty method uhint_db = db method set_uhint_db v = {< db = v >} diff --git a/matitaB/components/ng_refiner/nCicUnifHint.mli b/matitaB/components/ng_refiner/nCicUnifHint.mli index 77600663a..fafc4a6f8 100644 --- a/matitaB/components/ng_refiner/nCicUnifHint.mli +++ b/matitaB/components/ng_refiner/nCicUnifHint.mli @@ -24,7 +24,7 @@ class virtual status : string option -> object ('self) inherit g_status - inherit NCic.status + inherit NCicEnvironment.status method set_uhint_db: db -> 'self method set_unifhint_status: #g_status -> 'self end diff --git a/matitaB/components/ng_refiner/nCicUnification.ml b/matitaB/components/ng_refiner/nCicUnification.ml index 1e37ff797..cd5c89dd3 100644 --- a/matitaB/components/ng_refiner/nCicUnification.ml +++ b/matitaB/components/ng_refiner/nCicUnification.ml @@ -164,7 +164,7 @@ let rec lambda_intros status metasenv subst context argsno ty = let unopt exc = function None -> raise exc | Some x -> x ;; -let fix (status:#NCic.status) metasenv subst is_sup test_eq_only exc t = +let fix (status:#NCicEnvironment.status) metasenv subst is_sup test_eq_only exc t = (*D*) inside 'f'; try let rc = pp (lazy (status#ppterm ~metasenv ~subst ~context:[] t)); let rec aux test_eq_only metasenv = function @@ -176,10 +176,10 @@ let fix (status:#NCic.status) metasenv subst is_sup test_eq_only exc t = metasenv,orig | NCic.Sort (NCic.Type _) when test_eq_only -> raise exc | NCic.Sort (NCic.Type u) when is_sup -> - metasenv, NCic.Sort (NCic.Type (unopt exc (NCicEnvironment.sup u))) + metasenv, NCic.Sort (NCic.Type (unopt exc (NCicEnvironment.sup status u))) | NCic.Sort (NCic.Type u) -> metasenv, NCic.Sort (NCic.Type - (unopt exc (NCicEnvironment.inf ~strict:false u))) + (unopt exc (NCicEnvironment.inf status ~strict:false u))) | NCic.Meta (n,_) as orig -> (try let _,_,_,_ = NCicUtils.lookup_subst n subst in metasenv,orig @@ -335,10 +335,10 @@ let rec instantiate status test_eq_only metasenv subst context n lc t swap = match s,swap with NCic.Type u2, false -> NCic.Sort (NCic.Type - (unopt exc (NCicEnvironment.inf ~strict:false - (unopt exc (NCicEnvironment.inf ~strict:true u1) @ u2)))) + (unopt exc (NCicEnvironment.inf status ~strict:false + (unopt exc (NCicEnvironment.inf status ~strict:true u1) @ u2)))) | NCic.Type u2, true -> - if NCicEnvironment.universe_lt u2 u1 then + if NCicEnvironment.universe_lt status u2 u1 then NCic.Sort (NCic.Type u2) else (raise exc) | NCic.Prop,_ -> NCic.Sort NCic.Prop @@ -425,7 +425,7 @@ and unify status test_eq_only metasenv subst context t1 t2 swap = assert false | (C.Sort (C.Type a), C.Sort (C.Type b)) when not test_eq_only -> let a, b = if swap then b,a else a,b in - if NCicEnvironment.universe_leq a b then metasenv, subst + if NCicEnvironment.universe_leq status a b then metasenv, subst else raise (UnificationFailure (mk_msg status metasenv subst context t1 t2)) | (C.Sort (C.Type a), C.Sort (C.Type b)) -> if NCicEnvironment.universe_eq a b then metasenv, subst @@ -566,7 +566,7 @@ and unify status test_eq_only metasenv subst context t1 t2 swap = let tym = NCicSubstitution.subst_meta status lc tym in match tyn,tym with NCic.Sort NCic.Type u1, NCic.Sort NCic.Type u2 -> - NCicEnvironment.universe_lt u1 u2 + NCicEnvironment.universe_lt status u1 u2 | _,_ -> false -> instantiate status test_eq_only metasenv subst context m lc' (NCicReduction.head_beta_reduce status ~subst t1) (not swap) diff --git a/matitaB/components/ng_refiner/nCicUnification.mli b/matitaB/components/ng_refiner/nCicUnification.mli index ec21d6643..d0a539c6a 100644 --- a/matitaB/components/ng_refiner/nCicUnification.mli +++ b/matitaB/components/ng_refiner/nCicUnification.mli @@ -25,7 +25,7 @@ val unify : (* this should be moved elsewhere *) val fix_sorts: - #NCic.status -> NCic.metasenv -> NCic.substitution -> + #NCicEnvironment.status -> NCic.metasenv -> NCic.substitution -> NCic.term -> NCic.metasenv * NCic.term (* delift_type_wrt_terms st m s c t args @@ -39,7 +39,7 @@ val delift_type_wrt_terms: NCic.metasenv * NCic.substitution * NCic.term val sortfy :# - NCic.status -> exn -> NCic.metasenv -> NCic.substitution -> NCic.context -> + NCicEnvironment.status -> exn -> NCic.metasenv -> NCic.substitution -> NCic.context -> NCic.term -> NCic.metasenv * NCic.substitution * NCic.term val debug : bool ref diff --git a/matitaB/components/ng_tactics/nCicElim.ml b/matitaB/components/ng_tactics/nCicElim.ml index c2543711a..fd20de1dc 100644 --- a/matitaB/components/ng_tactics/nCicElim.ml +++ b/matitaB/components/ng_tactics/nCicElim.ml @@ -197,7 +197,7 @@ let mk_elims status (uri,_,_,_,obj) = NCic.Inductive (true,leftno,[itl],_) -> List.map (fun s-> mk_elim status uri leftno itl (ast_of_sort s) (`Elim s)) (NCic.Prop:: - List.map (fun s -> NCic.Type s) (NCicEnvironment.get_universes ())) + List.map (fun s -> NCic.Type s) (NCicEnvironment.get_universes status)) | _ -> [] ;; diff --git a/matitaB/components/ng_tactics/nCicElim.mli b/matitaB/components/ng_tactics/nCicElim.mli index 826374fab..0d547347d 100644 --- a/matitaB/components/ng_tactics/nCicElim.mli +++ b/matitaB/components/ng_tactics/nCicElim.mli @@ -11,8 +11,8 @@ (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) -val mk_elims: #NCic.status -> NCic.obj -> NotationPt.term NotationPt.obj list +val mk_elims: #NCicEnvironment.status -> NCic.obj -> NotationPt.term NotationPt.obj list val mk_projections: - #NCic.status -> NCic.obj -> NotationPt.term NotationPt.obj list + #NCicEnvironment.status -> NCic.obj -> NotationPt.term NotationPt.obj list val ast_of_sort : NCic.sort -> [> `NCProp of string | `NType of string | `Prop ] * string diff --git a/matitaB/components/ng_tactics/nCicTacReduction.mli b/matitaB/components/ng_tactics/nCicTacReduction.mli index b19e57478..c73133f60 100644 --- a/matitaB/components/ng_tactics/nCicTacReduction.mli +++ b/matitaB/components/ng_tactics/nCicTacReduction.mli @@ -12,5 +12,5 @@ (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) val normalize: - #NCic.status -> ?delta:int -> subst:NCic.substitution -> NCic.context -> + #NCicEnvironment.status -> ?delta:int -> subst:NCic.substitution -> NCic.context -> NCic.term -> NCic.term diff --git a/matitaB/components/ng_tactics/nnAuto.ml b/matitaB/components/ng_tactics/nnAuto.ml index 9ef663ee1..f3cd17caf 100644 --- a/matitaB/components/ng_tactics/nnAuto.ml +++ b/matitaB/components/ng_tactics/nnAuto.ml @@ -450,7 +450,7 @@ let ground_instances status gl = debug_print (lazy (status#ppterm ctx [] [] t)); List.iter (fun (uri,_,_,_,_) as obj -> - NCicEnvironment.invalidate_item (`Obj (uri, obj))) + NCicEnvironment.invalidate_item status (`Obj (uri, obj))) objs; ()) gl -- 2.39.2