~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
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
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
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
(* 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
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 =
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
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
~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
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)
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 >}
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)
;;
let disambiguate_nterm status expty context metasenv subst thing
-=
+=
let newast, metasenv, subst, cic =
singleton "first"
(NCicDisambiguate.disambiguate_term
~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
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
;;
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
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
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
(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 *)
(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 ->
NCic.substitution * NCic.obj)
list * bool
-val disambiguate_path: #NCic.status -> NotationPt.term -> NCic.term
+val disambiguate_path: #NCicEnvironment.status -> NotationPt.term -> NCic.term
INTERFACE_FILES = \
nUri.mli \
nReference.mli \
+ nCicEnvironment.mli \
nCicUtils.mli \
nCicSubstitution.mli \
- nCicEnvironment.mli \
nCicReduction.mli \
nCicTypeChecker.mli \
nCicUntrusted.mli \
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
| (`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
(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
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)
| 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^
| 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
;;
*)
-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;;
| `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)
;;
-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
;;
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
(* 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 ]
(* 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 ============= *)
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)))
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
(* $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
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 &&
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
| (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)
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
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
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
(* $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] *)
(* 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]
* 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
(* 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
;;
-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
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))
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^
(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
| [] -> []
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
* 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 ->
(* 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
(* $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
?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
(* 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
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
| 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
(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
;;
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
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 *)
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 >}
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
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
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
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
(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)
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
(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);;
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
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
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
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 ->
val get_sig: eq_sig_type -> NCic.term
val mk_proof:
- #NCic.status ->
+ #NCicEnvironment.status ->
?demod:bool
-> NCic.term Terms.bag
-> Terms.M.key
* 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 ->
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 ->
(* 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
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
(* $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 ->
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)))
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,
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 " ^
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 >}
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
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
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
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
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
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)
(* 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
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
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))
| _ -> []
;;
(* $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
(* $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
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
projects / helm.git / commitdiff