aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/cerrors.ml4
-rw-r--r--toplevel/class.ml101
-rw-r--r--toplevel/class.mli1
-rw-r--r--toplevel/command.ml64
-rw-r--r--toplevel/command.mli12
-rw-r--r--toplevel/coqtop.ml5
-rw-r--r--toplevel/discharge.ml88
-rw-r--r--toplevel/himsg.ml6
-rw-r--r--toplevel/metasyntax.ml69
-rw-r--r--toplevel/metasyntax.mli2
-rw-r--r--toplevel/mltop.ml49
-rw-r--r--toplevel/record.ml18
-rwxr-xr-xtoplevel/recordobj.ml3
-rwxr-xr-xtoplevel/recordobj.mli4
-rw-r--r--toplevel/vernac.ml28
-rw-r--r--toplevel/vernacentries.ml208
-rw-r--r--toplevel/vernacentries.mli2
-rw-r--r--toplevel/vernacexpr.ml12
-rw-r--r--toplevel/vernacinterp.ml1
19 files changed, 421 insertions, 216 deletions
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 1fbc3a90e..9d00e63f4 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -78,12 +78,12 @@ let rec explain_exn_default = function
hov 0 (str "Error:" ++ spc () ++ Himsg.explain_refiner_error e)
| Nametab.GlobalizationError q ->
hov 0 (str "Error:" ++ spc () ++
- str "The reference" ++ spc () ++ Nametab.pr_qualid q ++
+ str "The reference" ++ spc () ++ Libnames.pr_qualid q ++
spc () ++ str "was not found" ++
spc () ++ str "in the current" ++ spc () ++ str "environment")
| Nametab.GlobalizationConstantError q ->
hov 0 (str "Error:" ++ spc () ++
- str "No constant of this name:" ++ spc () ++ Nametab.pr_qualid q)
+ str "No constant of this name:" ++ spc () ++ Libnames.pr_qualid q)
| Refiner.FailError i ->
hov 0 (str "Error: Fail tactic always fails (level " ++
int i ++ str").")
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 8bac0812e..09013d173 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -16,11 +16,13 @@ open Term
open Termops
open Inductive
open Declarations
+open Entries
open Environ
open Inductive
open Lib
open Classops
open Declare
+open Libnames
open Nametab
open Safe_typing
@@ -143,7 +145,7 @@ let uniform_cond nargs lt =
let id_of_cl = function
| CL_FUN -> id_of_string "FUNCLASS"
| CL_SORT -> id_of_string "SORTCLASS"
- | CL_CONST sp -> basename sp
+ | CL_CONST kn -> id_of_label (label kn)
| CL_IND ind ->
let (_,mip) = Global.lookup_inductive ind in
mip.mind_typename
@@ -259,12 +261,12 @@ let build_id_coercion idf_opt source =
(string_of_class (fst (find_class_type t))))
in
let constr_entry = (* Cast is necessary to express [val_f] is identity *)
- ConstantEntry
+ DefinitionEntry
{ const_entry_body = mkCast (val_f, typ_f);
const_entry_type = None;
const_entry_opaque = false } in
- let sp = declare_constant idf (constr_entry,NeverDischarge) in
- ConstRef sp
+ let (_,kn) = declare_constant idf (constr_entry,NeverDischarge) in
+ ConstRef kn
(*
nom de la fonction coercion
@@ -332,7 +334,7 @@ let try_add_new_coercion_with_source ref stre ~source =
let add_coercion_hook stre ref =
try_add_new_coercion ref stre;
Options.if_verbose message
- (string_of_qualid (shortest_qualid_of_global (Global.env()) ref)
+ (string_of_qualid (shortest_qualid_of_global None ref)
^ " is now a coercion")
let add_subclass_hook stre ref =
@@ -374,52 +376,49 @@ let count_extra_abstractions hyps ids_to_discard =
(hyps,0) ids_to_discard
in n
-let defined_in_sec sp sec_sp = dirpath sp = sec_sp
+let defined_in_sec kn olddir =
+ let _,dir,_ = repr_kn kn in
+ dir = olddir
(* This moves the global path one step below *)
-let process_global sec_sp = function
+let process_global olddir = function
| VarRef _ ->
anomaly "process_global only processes global surviving the section"
- | ConstRef sp as x ->
- if defined_in_sec sp sec_sp then
- let (_,spid) = repr_path sp in
- let newsp = Lib.make_path spid in
- ConstRef newsp
+ | ConstRef kn as x ->
+ if defined_in_sec kn olddir then
+ let newkn = Lib.make_kn (id_of_label (label kn)) in
+ ConstRef newkn
else x
- | IndRef (sp,i) as x ->
- if defined_in_sec sp sec_sp then
- let (_,spid) = repr_path sp in
- let newsp = Lib.make_path spid in
- IndRef (newsp,i)
+ | IndRef (kn,i) as x ->
+ if defined_in_sec kn olddir then
+ let newkn = Lib.make_kn (id_of_label (label kn)) in
+ IndRef (newkn,i)
else x
- | ConstructRef ((sp,i),j) as x ->
- if defined_in_sec sp sec_sp then
- let (_,spid) = repr_path sp in
- let newsp = Lib.make_path spid in
- ConstructRef ((newsp,i),j)
+ | ConstructRef ((kn,i),j) as x ->
+ if defined_in_sec kn olddir then
+ let newkn = Lib.make_kn (id_of_label (label kn)) in
+ ConstructRef ((newkn,i),j)
else x
-let process_class sec_sp ids_to_discard x =
+let process_class olddir ids_to_discard x =
let (cl,{cl_strength=stre; cl_param=p}) = x in
(* let env = Global.env () in*)
match cl with
| CL_SECVAR _ -> x
- | CL_CONST sp ->
- if defined_in_sec sp sec_sp then
- let (_,spid) = repr_path sp in
- let newsp = Lib.make_path spid in
- let hyps = (Global.lookup_constant sp).const_hyps in
+ | CL_CONST kn ->
+ if defined_in_sec kn olddir then
+ let newkn = Lib.make_kn (id_of_label (label kn)) in
+ let hyps = (Global.lookup_constant kn).const_hyps in
+ let n = count_extra_abstractions hyps ids_to_discard in
+ (CL_CONST newkn,{cl_strength=stre;cl_param=p+n})
+ else
+ x
+ | CL_IND (kn,i) ->
+ if defined_in_sec kn olddir then
+ let newkn = Lib.make_kn (id_of_label (label kn)) in
+ let hyps = (Global.lookup_mind kn).mind_hyps in
let n = count_extra_abstractions hyps ids_to_discard in
- (CL_CONST newsp,{cl_strength=stre;cl_param=p+n})
- else
- x
- | CL_IND (sp,i) ->
- if defined_in_sec sp sec_sp then
- let (_,spid) = repr_path sp in
- let newsp = Lib.make_path spid in
- let hyps = (Global.lookup_mind sp).mind_hyps in
- let n = count_extra_abstractions hyps ids_to_discard in
- (CL_IND (newsp,i),{cl_strength=stre;cl_param=p+n})
+ (CL_IND (newkn,i),{cl_strength=stre;cl_param=p+n})
else
x
| _ -> anomaly "process_class"
@@ -427,28 +426,26 @@ let process_class sec_sp ids_to_discard x =
let process_cl sec_sp cl =
match cl with
| CL_SECVAR id -> cl
- | CL_CONST sp ->
- if defined_in_sec sp sec_sp then
- let (_,spid) = repr_path sp in
- let newsp = Lib.make_path spid in
- CL_CONST newsp
+ | CL_CONST kn ->
+ if defined_in_sec kn sec_sp then
+ let newkn = Lib.make_kn (id_of_label (label kn)) in
+ CL_CONST newkn
else
cl
- | CL_IND (sp,i) ->
- if defined_in_sec sp sec_sp then
- let (_,spid) = repr_path sp in
- let newsp = Lib.make_path spid in
- CL_IND (newsp,i)
+ | CL_IND (kn,i) ->
+ if defined_in_sec kn sec_sp then
+ let newkn = Lib.make_kn (id_of_label (label kn)) in
+ CL_IND (newkn,i)
else
cl
| _ -> cl
-let process_coercion sec_sp ids_to_discard ((coe,coeinfo),cls,clt) =
+let process_coercion olddir ids_to_discard ((coe,coeinfo),cls,clt) =
let hyps = context_of_global_reference coe in
let nargs = count_extra_abstractions hyps ids_to_discard in
- (process_global sec_sp coe,
+ (process_global olddir coe,
coercion_strength coeinfo,
coercion_identity coeinfo,
- process_cl sec_sp cls,
- process_cl sec_sp clt,
+ process_cl olddir cls,
+ process_cl olddir clt,
nargs + coercion_params coeinfo)
diff --git a/toplevel/class.mli b/toplevel/class.mli
index 388f664e4..8e9bcc3c3 100644
--- a/toplevel/class.mli
+++ b/toplevel/class.mli
@@ -13,6 +13,7 @@ open Names
open Term
open Classops
open Declare
+open Libnames
open Nametab
(*i*)
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 34adc0587..c9becbd3a 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -14,6 +14,7 @@ open Options
open Term
open Termops
open Declarations
+open Entries
open Inductive
open Environ
open Reduction
@@ -21,6 +22,7 @@ open Tacred
open Declare
open Nametab
open Names
+open Libnames
open Nameops
open Coqast
open Ast
@@ -45,6 +47,13 @@ let rec abstract_rawconstr c = function
List.fold_right (fun x b -> mkLambdaC(x,t,b)) idl
(abstract_rawconstr c bl)
+let rec prod_rawconstr c = function
+ | [] -> c
+ | LocalRawDef (x,b)::bl -> mkLetInC(x,b,prod_rawconstr c bl)
+ | LocalRawAssum (idl,t)::bl ->
+ List.fold_right (fun x b -> mkProdC(x,t,b)) idl
+ (prod_rawconstr c bl)
+
let rec destSubCast c = match kind_of_term c with
| Lambda (x,t,c) ->
let (b,u) = destSubCast c in mkLambda (x,t,b), mkProd (x,t,u)
@@ -83,11 +92,11 @@ let red_constant_entry ce = function
reduction_of_redexp red (Global.env()) Evd.empty body }
let declare_global_definition ident ce n local =
- let sp = declare_constant ident (ConstantEntry ce,n) in
+ let (_,kn) = declare_constant ident (DefinitionEntry ce,n) in
if local then
msg_warning (pr_id ident ++ str" is declared as a global definition");
if_verbose message ((string_of_id ident) ^ " is defined");
- ConstRef sp
+ ConstRef kn
let declare_definition ident (local,n) bl red_option c typopt =
let ce = constant_entry_of_com (bl,c,typopt,false) in
@@ -122,13 +131,14 @@ let syntax_definition ident c =
let assumption_message id =
if_verbose message ((string_of_id id) ^ " is assumed")
-let declare_assumption ident n c =
+let declare_assumption ident n bl c =
+ let c = prod_rawconstr c bl in
let c = interp_type Evd.empty (Global.env()) c in
match n with
| NeverDischarge ->
- let r = declare_constant ident (ParameterEntry c, NeverDischarge) in
+ let (_,kn) = declare_constant ident (ParameterEntry c, NeverDischarge) in
assumption_message ident;
- ConstRef r
+ ConstRef kn
| DischargeAt (disch_sp,_) ->
if Lib.is_section_p disch_sp then begin
let r = declare_variable ident (Lib.cwd(),SectionLocalAssum c,n) in
@@ -139,12 +149,12 @@ let declare_assumption ident n c =
VarRef ident
end
else
- let r = declare_constant ident (ParameterEntry c, NeverDischarge) in
+ let (_,kn) = declare_constant ident (ParameterEntry c, NeverDischarge) in
assumption_message ident;
if_verbose
msg_warning (pr_id ident ++ str" is declared as a parameter" ++
str" because it is at a global level");
- ConstRef r
+ ConstRef kn
| NotDeclare ->
anomalylabstrm "Command.hypothesis_def_var"
(str "Strength NotDeclare not for Variable, only for Let")
@@ -230,10 +240,10 @@ let interp_mutual lparams lnamearconstrs finite =
let declare_mutual_with_eliminations mie =
let lrecnames =
List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in
- let sp = declare_mind mie in
+ let (_,kn) = declare_mind mie in
if_verbose ppnl (minductive_message lrecnames);
- Indrec.declare_eliminations sp;
- sp
+ Indrec.declare_eliminations kn;
+ kn
let eq_la (id,ast) (id',ast') = id = id' & alpha_eq(ast,ast')
@@ -351,8 +361,8 @@ let build_recursive lnameargsardef =
recvec));
const_entry_type = None;
const_entry_opaque = false } in
- let sp = declare_constant fi (ConstantEntry ce, n) in
- (ConstRef sp)
+ let (_,kn) = declare_constant fi (DefinitionEntry ce, n) in
+ (ConstRef kn)
in
(* declare the recursive definitions *)
let lrefrec = Array.mapi declare namerec in
@@ -365,7 +375,7 @@ let build_recursive lnameargsardef =
let ce = { const_entry_body = replace_vars subst def;
const_entry_type = Some t;
const_entry_opaque = false } in
- let _ = declare_constant f (ConstantEntry ce,n) in
+ let _ = declare_constant f (DefinitionEntry ce,n) in
warning ((string_of_id f)^" is non-recursively defined");
(var_subst f) :: subst)
(List.map var_subst (Array.to_list namerec))
@@ -415,8 +425,8 @@ let build_corecursive lnameardef =
const_entry_type = None;
const_entry_opaque = false }
in
- let sp = declare_constant fi (ConstantEntry ce,n) in
- (ConstRef sp)
+ let _,kn = declare_constant fi (DefinitionEntry ce,n) in
+ (ConstRef kn)
in
let lrefrec = Array.mapi declare namerec in
if_verbose ppnl (corecursive_message lrefrec);
@@ -427,7 +437,7 @@ let build_corecursive lnameardef =
let ce = { const_entry_body = replace_vars subst def;
const_entry_type = Some t;
const_entry_opaque = false } in
- let _ = declare_constant f (ConstantEntry ce,n) in
+ let _ = declare_constant f (DefinitionEntry ce,n) in
warning ((string_of_id f)^" is non-recursively defined");
(var_subst f) :: subst)
(List.map var_subst (Array.to_list namerec))
@@ -453,8 +463,8 @@ let build_scheme lnamedepindsort =
let ce = { const_entry_body = decl;
const_entry_type = None;
const_entry_opaque = false } in
- let sp = declare_constant fi (ConstantEntry ce,n) in
- ConstRef sp :: lrecref
+ let _,kn = declare_constant fi (DefinitionEntry ce,n) in
+ ConstRef kn :: lrecref
in
let lrecref = List.fold_right2 declare listdecl lrecnames [] in
if_verbose ppnl (recursive_message (Array.of_list lrecref))
@@ -484,17 +494,18 @@ let apply_tac_not_declare id pft = function
Pfedit.delete_current_proof ();
Pfedit.by (Refiner.tclTHENSV cutt [|introduction id;exat|])
-let save id const strength hook =
+let save id const (local,strength) hook =
let {const_entry_body = pft;
const_entry_type = tpo;
const_entry_opaque = opacity } = const in
begin match strength with
- | DischargeAt (disch_sp,_) when Lib.is_section_p disch_sp && not opacity ->
+ | DischargeAt (disch_sp,_) when Lib.is_section_p disch_sp && local ->
let c = SectionLocalDef (pft, tpo) in
let _ = declare_variable id (Lib.cwd(), c, strength) in
hook strength (VarRef id)
| NeverDischarge | DischargeAt _ ->
- let ref = ConstRef (declare_constant id (ConstantEntry const,strength)) in
+ let _,kn = declare_constant id (DefinitionEntry const,strength) in
+ let ref = ConstRef kn in
hook strength ref
| NotDeclare -> apply_tac_not_declare id pft tpo
end;
@@ -505,9 +516,9 @@ let save id const strength hook =
end
let save_named opacity =
- let id,(const,(local,strength),hook) = Pfedit.cook_proof () in
+ let id,(const,persistence,hook) = Pfedit.cook_proof () in
let const = { const with const_entry_opaque = opacity } in
- save id const strength hook
+ save id const persistence hook
let check_anonymity id save_ident =
if atompart_of_id id <> "Unnamed_thm" then
@@ -517,16 +528,17 @@ let check_anonymity id save_ident =
*)
let save_anonymous opacity save_ident =
- let id,(const,(local,strength),hook) = Pfedit.cook_proof () in
+ let id,(const,persistence,hook) = Pfedit.cook_proof () in
let const = { const with const_entry_opaque = opacity } in
check_anonymity id save_ident;
- save save_ident const strength hook
+ save save_ident const persistence hook
let save_anonymous_with_strength strength opacity save_ident =
let id,(const,_,hook) = Pfedit.cook_proof () in
let const = { const with const_entry_opaque = opacity } in
check_anonymity id save_ident;
- save save_ident const strength hook
+ (* we consider that non opaque behaves as local for discharge *)
+ save save_ident const (not opacity,strength) hook
let get_current_context () =
try Pfedit.get_current_goal_context ()
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 1b8cbe49a..23c0db5b4 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -12,9 +12,12 @@
open Util
open Names
open Term
-open Nametab
+open Declare
open Library
+open Libnames
+open Nametab
open Vernacexpr
+
(*i*)
(*s Declaration functions. The following functions take ASTs,
@@ -28,12 +31,13 @@ val declare_definition : identifier -> bool * strength ->
val syntax_definition : identifier -> Coqast.t -> unit
-val declare_assumption : identifier -> strength -> Coqast.t -> global_reference
+val declare_assumption : identifier -> strength ->
+ local_binder list -> Coqast.t -> global_reference
val build_mutual : Vernacexpr.inductive_expr list -> bool -> unit
val declare_mutual_with_eliminations :
- Indtypes.mutual_inductive_entry -> section_path
+ Entries.mutual_inductive_entry -> mutual_inductive
val build_recursive :
(identifier * ((identifier * Coqast.t) list) * Coqast.t * Coqast.t) list
@@ -41,7 +45,7 @@ val build_recursive :
val build_corecursive : (identifier * Coqast.t * Coqast.t) list -> unit
-val build_scheme : (identifier * bool * Nametab.qualid located * Coqast.t) list -> unit
+val build_scheme : (identifier * bool * qualid located * Coqast.t) list -> unit
val start_proof_com : identifier option -> bool * strength -> Coqast.t -> Proof_type.declaration_hook -> unit
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index a62c1fae4..bcee6d0ce 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -13,6 +13,7 @@ open Util
open System
open Options
open Names
+open Libnames
open Nameops
open States
open Toplevel
@@ -62,12 +63,12 @@ let load_vernacular () =
let load_vernacular_obj = ref ([] : string list)
let add_vernac_obj s = load_vernacular_obj := s :: !load_vernacular_obj
let load_vernac_obj () =
- List.iter Library.read_module_from_file (List.rev !load_vernacular_obj)
+ List.iter Library.read_library_from_file (List.rev !load_vernacular_obj)
let require_list = ref ([] : string list)
let add_require s = require_list := s :: !require_list
let require () =
- List.iter (fun s -> Library.require_module_from_file None None s false)
+ List.iter (fun s -> Library.require_library_from_file None None s false)
(List.rev !require_list)
let compile_list = ref ([] : (bool * string) list)
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 14e4feff5..93277300b 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -15,11 +15,13 @@ open Nameops
open Sign
open Term
open Declarations
+open Entries
open Inductive
open Instantiate
open Reduction
open Cooking
open Typeops
+open Libnames
open Libobject
open Lib
open Nametab
@@ -33,7 +35,11 @@ open Indtypes
open Nametab
let recalc_sp dir sp =
- let (_,spid) = repr_path sp in Names.make_path dir spid
+ let (_,spid) = repr_path sp in Libnames.make_path dir spid
+
+let recalc_kn dir kn =
+ let (mp,_,l) = Names.repr_kn kn in
+ Names.make_kn mp dir l
let rec find_var id = function
| [] -> false
@@ -93,8 +99,8 @@ let abstract_inductive ids_to_abs hyps inds =
let params' =
List.map
(function
- | (Name id,None,p) -> id, LocalAssum p
- | (Name id,Some p,_) -> id, LocalDef p
+ | (Name id,None,p) -> id, Entries.LocalAssum p
+ | (Name id,Some p,_) -> id, Entries.LocalDef p
| (Anonymous,_,_) -> anomaly"Unnamed inductive local variable")
params in
{ mind_entry_params = params';
@@ -170,20 +176,21 @@ type opacity = bool
type discharge_operation =
| Variable of identifier * section_variable_entry * strength * bool
- | Constant of section_path * recipe * strength * bool
+ | Constant of identifier * recipe * strength * constant * bool
| Inductive of mutual_inductive_entry * bool
| Class of cl_typ * cl_info_typ
| Struc of inductive * (unit -> struc_typ)
| Objdef of constant
| Coercion of coercion_entry
- | Require of module_reference
+ | Require of library_reference
| Constraints of Univ.constraints
(* Main function to traverse the library segment and compute the various
discharge operations. *)
-let process_object oldenv dir sec_sp
- (ops,ids_to_discard,(constl,indl,cstrl as work_alist)) (sp,lobj) =
+let process_object oldenv olddir full_olddir newdir
+(* {dir -> newdir} {sec_sp -> full_olddir, olddir} *)
+ (ops,ids_to_discard,(constl,indl,cstrl as work_alist)) ((sp,kn),lobj) =
let tag = object_tag lobj in
match tag with
| "VARIABLE" ->
@@ -222,60 +229,63 @@ let process_object oldenv dir sec_sp
(ops, ids_to_discard, (constl,indl,cstrl))
else
*)
- let cb = Environ.lookup_constant sp oldenv in
- let imp = is_implicit_constant sp in
- let newsp = match stre with
- | DischargeAt (d,_) when not (is_dirpath_prefix_of d dir) -> sp
- | _ -> recalc_sp dir sp in
+ let kn = Nametab.locate_constant (qualid_of_sp sp) in
+ let lab = label kn in
+ let cb = Environ.lookup_constant kn oldenv in
+ let imp = is_implicit_constant kn in
+ let newkn = (*match stre with (* this did not work anyway...*)
+ | DischargeAt (d,_) when not (is_dirpath_prefix_of d dir) -> kn
+ | _ -> *)recalc_kn newdir kn in
let mods =
let abs_vars = build_abstract_list cb.const_hyps ids_to_discard in
- [ (sp, DO_ABSTRACT(newsp,abs_vars)) ]
+ [ (kn, DO_ABSTRACT(newkn,abs_vars)) ]
in
let r = { d_from = cb;
d_modlist = work_alist;
d_abstract = ids_to_discard } in
- let op = Constant (newsp,r,stre,imp) in
+ let op = Constant (id_of_label lab, r,stre,newkn,imp) in
(op :: ops, ids_to_discard, (mods@constl, indl, cstrl))
| "INDUCTIVE" ->
- let mib = Environ.lookup_mind sp oldenv in
- let newsp = recalc_sp dir sp in
+ let kn = Nametab.locate_mind (qualid_of_sp sp) in
+ let mib = Environ.lookup_mind kn oldenv in
+ let newkn = recalc_kn newdir kn in
let imp = is_implicit_args() (* CHANGE *) in
let (mie,indmods,cstrmods) =
- process_inductive sp newsp oldenv (ids_to_discard,work_alist) mib in
+ process_inductive kn newkn oldenv (ids_to_discard,work_alist) mib in
((Inductive(mie,imp)) :: ops, ids_to_discard,
(constl,indmods@indl,cstrmods@cstrl))
| "CLASS" ->
let ((cl,clinfo) as x) = outClass lobj in
- if (match clinfo.cl_strength with DischargeAt (sp,_) -> sp = sec_sp | _ -> false) then
+ if (match clinfo.cl_strength with DischargeAt (dp,_) -> dp = full_olddir | _ -> false) then
(ops,ids_to_discard,work_alist)
else
- let (y1,y2) = process_class sec_sp ids_to_discard x in
+ let (y1,y2) = process_class olddir ids_to_discard x in
((Class (y1,y2))::ops, ids_to_discard, work_alist)
| "COERCION" ->
let (((_,coeinfo),_,_)as x) = outCoercion lobj in
- if (match coercion_strength coeinfo with DischargeAt (sp,_) -> sp = sec_sp | _ -> false) then
+ if (match coercion_strength coeinfo with DischargeAt (dp,_) -> dp = full_olddir | _ -> false) then
(ops,ids_to_discard,work_alist)
else
- let y = process_coercion sec_sp ids_to_discard x in
+ let y = process_coercion olddir ids_to_discard x in
((Coercion y)::ops, ids_to_discard, work_alist)
| "STRUCTURE" ->
- let ((sp,i),info) = outStruc lobj in
- let newsp = recalc_sp dir sp in
+ let ((kn,i),info) = outStruc lobj in
+ let newkn = recalc_kn newdir kn in
let strobj () =
- let mib = Environ.lookup_mind newsp (Global.env ()) in
+ let mib = Environ.lookup_mind newkn (Global.env ()) in
{ s_CONST = info.s_CONST;
s_PARAM = mib.mind_packets.(0).mind_nparams;
- s_PROJ = List.map (option_app (recalc_sp dir)) info.s_PROJ } in
- ((Struc ((newsp,i),strobj))::ops, ids_to_discard, work_alist)
+ s_PROJ = List.map (option_app (fun kn -> recalc_kn newdir kn)) info.s_PROJ } in
+ ((Struc ((newkn,i),strobj))::ops, ids_to_discard, work_alist)
| "OBJDEF1" ->
- let sp = outObjDef1 lobj in
- let new_sp = recalc_sp dir sp in
- ((Objdef new_sp)::ops, ids_to_discard, work_alist)
+ let kn = outObjDef1 lobj in
+ let new_kn = recalc_kn newdir kn in
+ ((Objdef new_kn)::ops, ids_to_discard, work_alist)
| "REQUIRE" ->
let c = out_require lobj in
@@ -283,8 +293,9 @@ let process_object oldenv dir sec_sp
| _ -> (ops,ids_to_discard,work_alist)
-let process_item oldenv dir sec_sp acc = function
- | (sp,Leaf lobj) -> process_object oldenv dir sec_sp acc (sp,lobj)
+let process_item oldenv olddir full_olddir newdir acc = function
+ | (sp,Leaf lobj) ->
+ process_object oldenv olddir full_olddir newdir acc (sp,lobj)
| (_,_) -> acc
let process_operation = function
@@ -293,9 +304,9 @@ let process_operation = function
let _ =
with_implicits imp (declare_variable id) (Lib.cwd(),expmod_a,stre) in
()
- | Constant (sp,r,stre,imp) ->
- with_implicits imp (redeclare_constant sp) (r,stre);
- constant_message (basename sp)
+ | Constant (id,r,stre,kn,imp) ->
+ with_implicits imp (redeclare_constant id) (r,stre);
+ constant_message id
| Inductive (mie,imp) ->
let _ = with_implicits imp declare_mind mie in
inductive_message mie.mind_entry_inds
@@ -306,7 +317,7 @@ let process_operation = function
| Objdef newsp ->
begin try Recordobj.objdef_declare (ConstRef newsp) with _ -> () end
| Coercion y -> add_new_coercion y
- | Require y -> reload_module y
+ | Require y -> reload_library y
| Constraints y -> Global.add_constraints y
let catch_not_found f x =
@@ -317,13 +328,14 @@ let catch_not_found f x =
let close_section _ s =
let oldenv = Global.env() in
- let olddir,decls,fs = close_section false s in
+ let prefix,decls,fs = close_section false s in
+ let full_olddir, (_,olddir) = prefix in
let newdir = fst (split_dirpath olddir) in
let (ops,ids,_) =
List.fold_left
- (process_item oldenv newdir olddir) ([],[],([],[],[])) decls
+ (process_item oldenv olddir full_olddir newdir) ([],[],([],[],[])) decls
in
let ids = last_section_hyps olddir in
Summary.unfreeze_lost_summaries fs;
catch_not_found (List.iter process_operation) (List.rev ops);
- Nametab.push_section olddir
+ Nametab.push_dir (Until 1) full_olddir (DirClosedSection full_olddir)
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index c2892a74b..82991495d 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -448,6 +448,11 @@ let error_same_names_constructors id cid =
str "is used twice is the definition of type" ++ spc () ++
pr_id id
+let error_same_names_overlap idl =
+ str "The following names" ++ spc () ++
+ str "are used both as type names and constructor names:" ++ spc () ++
+ prlist_with_sep pr_coma pr_id idl
+
let error_not_an_arity id =
str "The type of" ++ spc () ++ pr_id id ++ spc () ++ str "is not an arity."
@@ -477,6 +482,7 @@ let explain_inductive_error = function
| NonPar (env,c,n,v1,v2) -> error_bad_ind_parameters env c n v1 v2
| SameNamesTypes id -> error_same_names_types id
| SameNamesConstructors (id,cid) -> error_same_names_constructors id cid
+ | SameNamesOverlap idl -> error_same_names_overlap idl
| NotAnArity id -> error_not_an_arity id
| BadEntry -> error_bad_entry ()
(* These are errors related to recursors *)
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index cabdee95c..523b81b41 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -59,13 +59,16 @@ let _ =
(* Pretty-printing objects = syntax_entry *)
let cache_syntax (_,ppobj) = Esyntax.add_ppobject ppobj
+let subst_syntax (_,subst,ppobj) =
+ Extend.subst_syntax_command Ast.subst_astpat subst ppobj
+
let (inPPSyntax,outPPSyntax) =
- declare_object
- ("PPSYNTAX",
- { load_function = (fun _ -> ());
- open_function = cache_syntax;
+ declare_object {(default_object "PPSYNTAX") with
+ open_function = (fun i o -> if i=1 then cache_syntax o);
cache_function = cache_syntax;
- export_function = (fun x -> Some x) })
+ subst_function = subst_syntax;
+ classify_function = (fun (_,o) -> Substitute o);
+ export_function = (fun x -> Some x) }
(* Syntax extension functions (registered in the environnement) *)
@@ -93,25 +96,27 @@ let _ =
let cache_token (_,s) = Pcoq.lexer.Token.using ("", s)
let (inToken, outToken) =
- declare_object
- ("TOKEN",
- { load_function = (fun _ -> ());
- open_function = cache_token;
+ declare_object {(default_object "TOKEN") with
+ open_function = (fun i o -> if i=1 then cache_token o);
cache_function = cache_token;
- export_function = (fun x -> Some x)})
+ subst_function = Libobject.ident_subst_function;
+ classify_function = (fun (_,o) -> Substitute o);
+ export_function = (fun x -> Some x)}
let add_token_obj s = Lib.add_anonymous_leaf (inToken s)
(* Grammar rules *)
let cache_grammar (_,a) = Egrammar.extend_grammar a
+let subst_grammar (_,subst,a) = Egrammar.subst_all_grammar_command subst a
+
let (inGrammar, outGrammar) =
- declare_object
- ("GRAMMAR",
- { load_function = (fun _ -> ());
- open_function = cache_grammar;
+ declare_object {(default_object "GRAMMAR") with
+ open_function = (fun i o -> if i=1 then cache_grammar o);
cache_function = cache_grammar;
- export_function = (fun x -> Some x)})
+ subst_function = subst_grammar;
+ classify_function = (fun (_,o) -> Substitute o);
+ export_function = (fun x -> Some x)}
let gram_define_entry (u,_ as univ) ((ntl,nt),et,assoc,rl) =
let etyp = match et with None -> entry_type_from_name u | Some e -> e in
@@ -164,13 +169,17 @@ let cache_infix (_,(gr,se)) =
Egrammar.extend_grammar gr;
Esyntax.add_ppobject {sc_univ="constr";sc_entries=se}
+let subst_infix (_,subst,(gr,se)) =
+ (Egrammar.subst_all_grammar_command subst gr,
+ list_smartmap (Extend.subst_syntax_entry Ast.subst_astpat subst) se)
+
let (inInfix, outInfix) =
- declare_object
- ("INFIX",
- { load_function = (fun _ -> ());
- open_function = cache_infix;
+ declare_object {(default_object "INFIX") with
+ open_function = (fun i o -> if i=1 then cache_infix o);
cache_function = cache_infix;
- export_function = (fun x -> Some x)})
+ subst_function = subst_infix;
+ classify_function = (fun (_,o) -> Substitute o);
+ export_function = (fun x -> Some x)}
(* Build the syntax and grammar rules *)
@@ -261,27 +270,31 @@ let make_infix_symbols assoc n sl =
NonTerminal ((n,lp),"$a")::(List.map (fun s -> Terminal s) sl)
@[NonTerminal ((n,rp),"$b")]
+let subst_infix2 (_, subst, (ref,inf as node)) =
+ let ref' = Libnames.subst_ext subst ref in
+ if ref' == ref then node else
+ (ref', inf)
let cache_infix2 (_,(ref,inf)) =
let sp = match ref with
- | Nametab.TrueGlobal r -> Nametab.sp_of_global (Global.env()) r
- | Nametab.SyntacticDef sp -> sp in
+ | Libnames.TrueGlobal r -> Nametab.sp_of_global None r
+ | Libnames.SyntacticDef kn -> Nametab.sp_of_syntactic_definition kn in
declare_infix_symbol sp inf
let (inInfix2, outInfix2) =
- declare_object
- ("INFIX2",
- { load_function = (fun _ -> ());
- open_function = cache_infix2;
+ declare_object {(default_object "INFIX2") with
+ open_function = (fun i o -> if i=1 then cache_infix2 o);
cache_function = cache_infix2;
- export_function = (fun x -> Some x)})
+ subst_function = subst_infix2;
+ classify_function = (fun (_,o) -> Substitute o);
+ export_function = (fun x -> Some x)}
let add_infix assoc n inf (loc,qid) =
let ref =
try
Nametab.extended_locate qid
with Not_found ->
- error ("Unknown reference: "^(Nametab.string_of_qualid qid)) in
+ error ("Unknown reference: "^(Libnames.string_of_qualid qid)) in
let pr = Astterm.ast_of_extended_ref_loc loc ref in
(* check the precedence *)
if n<1 or n>10 then
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index 1eeec61b0..839e0fdbe 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -22,7 +22,7 @@ val add_token_obj : string -> unit
val add_tactic_grammar : (string * (string * grammar_production list) * Tacexpr.raw_tactic_expr) list -> unit
val add_infix :
- Gramext.g_assoc option -> int -> string -> Nametab.qualid Util.located -> unit
+ Gramext.g_assoc option -> int -> string -> Libnames.qualid Util.located -> unit
val add_distfix :
Gramext.g_assoc option -> int -> string -> Coqast.t -> unit
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index 0b86c7656..20d87306a 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -41,7 +41,7 @@ open Vernacinterp
put all the needed names into the ML Module object.) *)
(* This path is where we look for .cmo *)
-let coq_mlpath_copy = ref []
+let coq_mlpath_copy = ref ["."]
let keep_copy_mlpath s =
let dir = glob s in
coq_mlpath_copy := dir :: !coq_mlpath_copy
@@ -283,11 +283,10 @@ let cache_ml_module_object (_,{mnames=mnames}) =
let export_ml_module_object x = Some x
let (inMLModule,outMLModule) =
- declare_object ("ML-MODULE",
- { load_function = cache_ml_module_object;
+ declare_object {(default_object "ML-MODULE") with
+ load_function = (fun _ -> cache_ml_module_object);
cache_function = cache_ml_module_object;
- open_function = (fun _ -> ());
- export_function = export_ml_module_object })
+ export_function = export_ml_module_object }
let declare_ml_modules l =
Lib.add_anonymous_leaf (inMLModule {mnames=l})
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 10b9c42da..ab3482c91 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -11,11 +11,13 @@
open Pp
open Util
open Names
+open Libnames
open Nameops
open Term
open Termops
open Environ
open Declarations
+open Entries
open Declare
open Nametab
open Coqast
@@ -49,7 +51,7 @@ let interp_decl sigma env = function
(Name id,Some j.uj_val, j.uj_type)
let build_decl_entry sigma env (id,t) =
- (id,Typeops.LocalAssum (interp_type Evd.empty env t))
+ (id,Entries.LocalAssum (interp_type Evd.empty env t))
let typecheck_params_and_fields ps fs =
let env0 = Global.env () in
@@ -70,8 +72,8 @@ let typecheck_params_and_fields ps fs =
newps, newfs
let degenerate_decl id = function
- (_,None,t) -> (id,Typeops.LocalAssum t)
- | (_,Some c,t) -> (id,Typeops.LocalDef c)
+ (_,None,t) -> (id,Entries.LocalAssum t)
+ | (_,Some c,t) -> (id,Entries.LocalDef c)
type record_error =
| MissingProj of identifier * identifier list
@@ -184,7 +186,7 @@ let declare_projections indsp coers fields =
const_entry_type = None;
const_entry_opaque = false } in
let sp =
- declare_constant fid (ConstantEntry cie,NeverDischarge)
+ declare_constant fid (DefinitionEntry cie,NeverDischarge)
in Some sp
with Type_errors.TypeError (ctx,te) -> begin
warning_or_error coe indsp (BadTypedProj (fid,ctx,te));
@@ -193,9 +195,9 @@ let declare_projections indsp coers fields =
match name with
| None ->
(nfi-1, None::sp_projs, NoProjection fi::subst)
- | Some sp ->
- let refi = ConstRef sp in
- let constr_fi = mkConst sp in
+ | Some (sp,kn) ->
+ let refi = ConstRef kn in
+ let constr_fi = mkConst kn in
if coe then begin
let cl = Class.class_of_ref (IndRef indsp) in
Class.try_add_new_coercion_with_source
@@ -203,7 +205,7 @@ let declare_projections indsp coers fields =
end;
let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in
let constr_fip = applist (constr_fi,proj_args) in
- (nfi-1, name::sp_projs, Projection constr_fip::subst))
+ (nfi-1, (Some kn)::sp_projs, Projection constr_fip::subst))
(List.length fields,[],[]) coers (List.rev fields)
in sp_projs
diff --git a/toplevel/recordobj.ml b/toplevel/recordobj.ml
index 92c8e5524..58fbb9781 100755
--- a/toplevel/recordobj.ml
+++ b/toplevel/recordobj.ml
@@ -11,6 +11,7 @@
open Util
open Pp
open Names
+open Libnames
open Nameops
open Term
open Instantiate
@@ -31,7 +32,7 @@ let typ_lams_of t =
let objdef_err ref =
errorlabstrm "object_declare"
- (pr_id (Termops.id_of_global (Global.env()) ref) ++
+ (pr_id (id_of_global None ref) ++
str" is not a structure object")
let objdef_declare ref =
diff --git a/toplevel/recordobj.mli b/toplevel/recordobj.mli
index 590482653..71dbc6816 100755
--- a/toplevel/recordobj.mli
+++ b/toplevel/recordobj.mli
@@ -8,7 +8,5 @@
(* $Id$ *)
-open Nametab
-
-val objdef_declare : global_reference -> unit
+val objdef_declare : Libnames.global_reference -> unit
val add_object_hook : Proof_type.declaration_hook
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index ed2c3c154..937d05a22 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -156,15 +156,21 @@ let load_vernac verb file =
(* Compile a vernac file (f is assumed without .v suffix) *)
let compile verbosely f =
- let s = Filename.basename f in
- let m = Names.id_of_string s in
- let _,longf = find_file_in_path (Library.get_load_path ()) (f^".v") in
- let ldir0 = Library.find_logical_path (Filename.dirname longf) in
- let ldir = Nameops.extend_dirpath ldir0 m in
- Termops.set_module ldir; (* Just for universe naming *)
- Lib.start_module ldir;
+(*
+ let s = Filename.basename f in
+ let m = Names.id_of_string s in
+ let _,longf = find_file_in_path (Library.get_load_path ()) (f^".v") in
+ let ldir0 = Library.find_logical_path (Filename.dirname longf) in
+ let ldir = Libnames.extend_dirpath ldir0 m in
+ Termops.set_module ldir; (* Just for universe naming *)
+ Lib.start_module ldir;
+ if !dump then dump_string ("F" ^ Names.string_of_dirpath ldir ^ "\n");
+ let _ = load_vernac verbosely longf in
+ let mid = Lib.end_module m in
+ assert (mid = ldir);
+ Library.save_module_to ldir (longf^"o")
+*)
+ let ldir,long_f_dot_v = Library.start_library f in
if !dump then dump_string ("F" ^ Names.string_of_dirpath ldir ^ "\n");
- let _ = load_vernac verbosely longf in
- let mid = Lib.end_module m in
- assert (mid = ldir);
- Library.save_module_to ldir (longf^"o")
+ let _ = load_vernac verbosely long_f_dot_v in
+ Library.save_library_to ldir (long_f_dot_v^"o")
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 3852ba7fe..6e0ba7087 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -14,6 +14,7 @@ open Pp
open Util
open Options
open Names
+open Entries
open Nameops
open Term
open Pfedit
@@ -25,6 +26,8 @@ open Printer
open Tacinterp
open Command
open Goptions
+(*open Declare*)
+open Libnames
open Nametab
open Vernacexpr
@@ -161,8 +164,8 @@ let print_loadpath () =
prlist_with_sep pr_fnl print_path_entry l))
let print_modules () =
- let opened = Library.opened_modules ()
- and loaded = Library.loaded_modules () in
+ let opened = Library.opened_libraries ()
+ and loaded = Library.loaded_libraries () in
let loaded_opened = list_intersect loaded opened
and only_loaded = list_subtract loaded opened in
str"Loaded and imported modules: " ++
@@ -194,14 +197,26 @@ let locate_file f =
let print_located_qualid (_,qid) =
try
- let sp = Nametab.sp_of_global (Global.env()) (Nametab.locate qid) in
+ let sp = Nametab.sp_of_global None (Nametab.locate qid) in
msgnl (pr_sp sp)
with Not_found ->
try
- msgnl (pr_sp (Syntax_def.locate_syntactic_definition qid) ++ fnl ())
+ let kn = Nametab.locate_syntactic_definition qid in
+ let sp = Nametab.sp_of_syntactic_definition kn in
+ msgnl (pr_sp sp)
with Not_found ->
msgnl (pr_qualid qid ++ str " is not a defined object")
+(*let print_path_entry (s,l) =
+ (str s ++ tbrk (0,2) ++ str (string_of_dirpath l))
+
+let print_loadpath () =
+ let l = Library.get_full_load_path () in
+ msgnl (Pp.t (str "Physical path: " ++
+ tab () ++ str "Logical Path:" ++ fnl () ++
+ prlist_with_sep pr_fnl print_path_entry l))
+*)
+
let msg_found_library = function
| Library.LibLoaded, fulldir, file ->
msgnl(pr_dirpath fulldir ++ str " has been loaded from file" ++ fnl () ++
@@ -210,13 +225,13 @@ let msg_found_library = function
msgnl(pr_dirpath fulldir ++ str " is bound to file " ++ str file)
let msg_notfound_library loc qid = function
| Library.LibUnmappedDir ->
- let dir = fst (Nametab.repr_qualid qid) in
+ let dir = fst (repr_qualid qid) in
user_err_loc (loc,"locate_library",
str "Cannot find a physical path bound to logical path " ++
pr_dirpath dir ++ fnl ())
| Library.LibNotFound ->
msgnl (hov 0
- (str"Unable to locate library" ++ spc () ++ Nametab.pr_qualid qid))
+ (str"Unable to locate library" ++ spc () ++ pr_qualid qid))
| e -> assert false
let print_located_library (loc,qid) =
@@ -232,8 +247,8 @@ let vernac_syntax = Metasyntax.add_syntax_obj
let vernac_grammar = Metasyntax.add_grammar_obj
let vernac_infix assoc n inf qid =
- let sp = sp_of_global (Global.env()) (global qid) in
- let dir = repr_dirpath (Nameops.dirpath sp) in
+ let sp = sp_of_global None (global qid) in
+ let dir = repr_dirpath (dirpath sp) in
(*
if dir <> [] then begin
let modname = List.hd dir in
@@ -252,14 +267,14 @@ let vernac_distfix assoc n inf qid =
let interp_assumption = function
| (AssumptionHypothesis | AssumptionVariable) -> Declare.make_strength_0 ()
- | (AssumptionAxiom | AssumptionParameter) -> Nametab.NeverDischarge
+ | (AssumptionAxiom | AssumptionParameter) -> Libnames.NeverDischarge
let interp_definition = function
- | Definition -> (false, Nametab.NeverDischarge)
+ | Definition -> (false, Libnames.NeverDischarge)
| LocalDefinition -> (true, Declare.make_strength_0 ())
let interp_theorem = function
- | (Theorem | Lemma | Decl) -> Nametab.NeverDischarge
+ | (Theorem | Lemma | Decl) -> Libnames.NeverDischarge
| Fact -> Declare.make_strength_1 ()
| Remark -> Declare.make_strength_0 ()
@@ -282,10 +297,14 @@ let rec generalize_rawconstr c = function
let vernac_definition kind id def hook =
let (local,stre as k) = interp_definition kind in
match def with
- | ProveBody (bl,t) ->
- let hook _ _ = () in
- let t = generalize_rawconstr t bl in
- start_proof_and_print (Some id) k t hook
+ | ProveBody (bl,t) -> (* local binders, typ *)
+ if Lib.is_specification () then
+ let ref = declare_assumption id stre bl t in
+ hook stre ref
+ else
+ let hook _ _ = () in
+ let t = generalize_rawconstr t bl in
+ start_proof_and_print (Some id) k t hook
| DefineBody (bl,red_option,c,typ_opt) ->
let red_option = match red_option with
| None -> None
@@ -299,10 +318,16 @@ let vernac_start_proof kind sopt t lettop hook =
if not(refining ()) then
if lettop then
errorlabstrm "Vernacentries.StartProof"
- (str "Let declarations can only be used in proof editing mode")
-(* else if s = None then
- error "repeated Goal not permitted in refining mode"*);
- start_proof_and_print sopt (false, interp_theorem kind) t hook
+ (str "Let declarations can only be used in proof editing mode");
+ let stre = interp_theorem kind in
+ match Lib.is_specification (), sopt with
+ | true, Some id ->
+ let ref = declare_assumption id stre [] t in
+ hook stre ref
+ | _ ->
+ (* an explicit Goal command starts the refining mode
+ even in a specification *)
+ start_proof_and_print sopt (false, stre) t hook
let vernac_end_proof is_opaque idopt =
if_verbose show_script ();
@@ -323,7 +348,7 @@ let vernac_assumption kind l =
let stre = interp_assumption kind in
List.iter
(fun (is_coe,(id,c)) ->
- let r = declare_assumption id stre c in
+ let r = declare_assumption id stre [] c in
if is_coe then Class.try_add_new_coercion r stre) l
let vernac_inductive f indl = build_mutual indl f
@@ -334,6 +359,92 @@ let vernac_cofixpoint = build_corecursive
let vernac_scheme = build_scheme
+(**********************)
+(* Modules *)
+
+let vernac_declare_module id bl mty_ast_o mexpr_ast_o =
+ let evd = Evd.empty in
+ let env = Global.env () in
+ let arglist,base_mty_o,base_mexpr_o =
+ Astmod.interp_module_decl evd env bl mty_ast_o mexpr_ast_o
+ in
+ let argids, args = List.split arglist
+ in (* We check the state of the system (in module, in module type)
+ and what parts are supplied *)
+ match Lib.is_specification (), base_mty_o, base_mexpr_o with
+ | _, None, None
+ | false, _, None ->
+ Declaremods.start_module id argids args base_mty_o;
+ if_verbose message
+ ("Interactive Module "^ string_of_id id ^" started")
+
+ | true, Some _, None
+ | false, _, Some _ ->
+ let mexpr_o =
+ option_app
+ (List.fold_right
+ (fun (mbid,mte) me -> MEfunctor(mbid,mte,me))
+ args)
+ base_mexpr_o
+ in
+ let mty_o =
+ option_app
+ (List.fold_right
+ (fun (arg_id,arg_t) mte -> MTEfunsig(arg_id,arg_t,mte))
+ args)
+ base_mty_o
+ in
+ let mod_entry =
+ {mod_entry_type = mty_o;
+ mod_entry_expr = mexpr_o}
+ in
+ Declaremods.declare_module id mod_entry;
+ if_verbose message
+ ("Module "^ string_of_id id ^" is defined")
+
+ | true, _, Some _ ->
+ error "Module definition not allowed in a Module Type"
+
+
+let vernac_end_module id =
+ Declaremods.end_module id;
+ if_verbose message
+ ("Module "^ string_of_id id ^" is defined")
+
+
+
+let vernac_declare_module_type id bl mty_ast_o =
+ let evd = Evd.empty in
+ let env = Global.env () in
+ let arglist,base_mty_o,_ =
+ Astmod.interp_module_decl evd env bl mty_ast_o None
+ in
+ let argids, args = List.split arglist
+ in (* We check the state of the system (in module, in module type)
+ and what parts are supplied *)
+ match Lib.is_specification (), base_mty_o with
+ | _, None ->
+ Declaremods.start_modtype id argids args;
+ if_verbose message
+ ("Interactive Module "^ string_of_id id ^" started")
+
+ | _, Some base_mty ->
+ let mty =
+ List.fold_right
+ (fun (arg_id,arg_t) mte -> MTEfunsig(arg_id,arg_t,mte))
+ args
+ base_mty
+ in
+ Declaremods.declare_modtype id mty;
+ if_verbose message
+ ("Module Type "^ string_of_id id ^" is defined")
+
+
+let vernac_end_modtype id =
+ Declaremods.end_modtype id;
+ if_verbose message
+ ("Module Type "^ string_of_id id ^" is defined")
+
(**********************)
(* Gallina extensions *)
@@ -350,9 +461,20 @@ let vernac_record struc binders sort nameopt cfs =
let vernac_begin_section id = let _ = Lib.open_section id in ()
let vernac_end_section id =
- check_no_pending_proofs ();
Discharge.close_section (is_verbose ()) id
+
+let vernac_end_segment id =
+ check_no_pending_proofs ();
+ try
+ match Lib.what_is_opened () with
+ | _,Lib.OpenedModule _ -> vernac_end_module id
+ | _,Lib.OpenedModtype _ -> vernac_end_modtype id
+ | _,Lib.OpenedSection _ -> vernac_end_section id
+ | _ -> anomaly "No more opened things"
+ with
+ Not_found -> error "There is nothing to end."
+
let is_obsolete_module (_,qid) =
match repr_qualid qid with
| dir, id when dir = empty_dirpath ->
@@ -367,8 +489,8 @@ let is_obsolete_module (_,qid) =
let vernac_require import _ qidl =
try
match import with
- | None -> List.iter Library.read_module qidl
- | Some b -> Library.require_module None qidl b
+ | None -> List.iter Library.read_library qidl
+ | Some b -> Library.require_library None qidl b
with e ->
(* Compatibility message *)
let qidl' = List.filter is_obsolete_module qidl in
@@ -381,7 +503,20 @@ let vernac_require import _ qidl =
raise e
let vernac_import export qidl =
- List.iter (Library.import_module export) qidl
+ if export then
+ List.iter Library.export_library qidl
+ else
+ let import (loc,qid) =
+ try
+ let mp = Nametab.locate_module qid in
+ Declaremods.import_module mp
+ with Not_found ->
+ user_err_loc
+ (loc,"vernac_import",
+ str ((string_of_qualid qid)^" is not a module"))
+ in
+ List.iter import qidl;
+ Lib.add_frozen_state ()
let vernac_canonical locqid =
Recordobj.objdef_declare (Nametab.global locqid)
@@ -396,7 +531,7 @@ let vernac_coercion stre (loc,qid as locqid) qids qidt =
let source = cl_of_qualid qids in
let ref = Nametab.global locqid in
Class.try_add_new_coercion_with_target ref stre source target;
- if_verbose message ((Nametab.string_of_qualid qid) ^ " is now a coercion")
+ if_verbose message ((string_of_qualid qid) ^ " is now a coercion")
let vernac_identity_coercion stre id qids qidt =
let target = cl_of_qualid qidt in
@@ -431,7 +566,7 @@ let vernac_solve_existential = instantiate_nth_evar_com
(* Auxiliary file management *)
let vernac_require_from export spec id filename =
- Library.require_module_from_file spec (Some id) filename export
+ Library.require_library_from_file spec (Some id) filename export
let vernac_add_loadpath isrec pdir ldiropt =
let alias = match ldiropt with
@@ -595,9 +730,9 @@ let vernac_mem_option key lv =
let vernac_print_option key =
try (get_ref_table key)#print
- with not_found ->
+ with Not_found ->
try (get_string_table key)#print
- with not_found ->
+ with Not_found ->
try print_option_value key
with Not_found -> error_undeclared_key key
@@ -655,7 +790,6 @@ let vernac_print = function
| PrintHintDbName s -> Auto.print_hint_db_by_name s
| PrintHintDb -> Auto.print_searchtable ()
-
let global_loaded_library (loc, qid) =
try Nametab.locate_loaded_library qid
with Not_found ->
@@ -692,7 +826,7 @@ let vernac_goal = function
| None -> ()
| Some c ->
if not (refining()) then begin
- start_proof_com None (false,Nametab.NeverDischarge) c (fun _ _ ->());
+ start_proof_com None (false,Libnames.NeverDischarge) c (fun _ _ ->());
print_subgoals ()
end else
error "repeated Goal not permitted in refining mode"
@@ -844,7 +978,7 @@ let _ =
let ref = Nametab.global (dummy_loc, qid) in
Class.try_add_new_class ref stre;
if_verbose message
- ((Nametab.string_of_qualid qid) ^ " is now a class")
+ ((string_of_qualid qid) ^ " is now a class")
| _ -> bad_vernac_args "CLASS")
(* Meta-syntax commands *)
@@ -893,10 +1027,18 @@ let interp c = match c with
| VernacCoFixpoint l -> vernac_cofixpoint l
| VernacScheme l -> vernac_scheme l
+ (* Modules *)
+ | VernacDeclareModule (id,bl,mtyo,mexpro) ->
+ vernac_declare_module id bl mtyo mexpro
+ | VernacDeclareModuleType (id,bl,mtyo) ->
+ vernac_declare_module_type id bl mtyo
+
(* Gallina extensions *)
- | VernacRecord (id,bl,s,idopt,fs) -> vernac_record id bl s idopt fs
| VernacBeginSection id -> vernac_begin_section id
- | VernacEndSection id -> vernac_end_section id
+
+ | VernacEndSegment id -> vernac_end_segment id
+
+ | VernacRecord (id,bl,s,idopt,fs) -> vernac_record id bl s idopt fs
| VernacRequire (export,spec,qidl) -> vernac_require export spec qidl
| VernacImport (export,qidl) -> vernac_import export qidl
| VernacCanonical qid -> vernac_canonical qid
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli
index 85daf4375..0eca1143f 100644
--- a/toplevel/vernacentries.mli
+++ b/toplevel/vernacentries.mli
@@ -52,7 +52,7 @@ type pcoq_hook = {
solve : int -> unit;
abort : string -> unit;
search : searchable -> dir_path list * bool -> unit;
- print_name : Nametab.qualid Util.located -> unit;
+ print_name : Libnames.qualid Util.located -> unit;
print_check : Environ.unsafe_judgment -> unit;
print_eval : (constr -> constr) -> Environ.env -> Coqast.t -> Environ.unsafe_judgment -> unit;
show_goal : int option -> unit
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index ace11aee3..869760411 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -25,6 +25,7 @@ type def_kind = DEFINITION | LET | LOCAL | THEOREM | LETTOP | DECL | REMARK
| COERCION | LCOERCION | OBJECT | LOBJECT | OBJCOERCION | LOBJCOERCION
| SUBCLASS | LSUBCLASS
+open Libnames
open Nametab
type class_rawexpr = FunClass | SortClass | RefClass of qualid located
@@ -165,6 +166,9 @@ type grammar_entry_ast =
(loc * string) * Ast.entry_type option *
grammar_associativity * raw_grammar_rule list
+type module_ast = Coqast.t
+type module_binder = identifier list * module_ast
+
type vernac_expr =
(* Control *)
| VernacList of located_vernac_expr list
@@ -197,7 +201,7 @@ type vernac_expr =
| VernacRecord of identifier with_coercion * simple_binder list
* sort_expr * identifier option * local_decl_expr with_coercion list
| VernacBeginSection of identifier
- | VernacEndSection of identifier
+ | VernacEndSegment of identifier
| VernacRequire of
export_flag option * specif_flag option * qualid located list
| VernacImport of export_flag * qualid located list
@@ -206,6 +210,12 @@ type vernac_expr =
| VernacIdentityCoercion of strength * identifier *
class_rawexpr * class_rawexpr
+ (* Modules and Module Types *)
+ | VernacDeclareModule of identifier *
+ module_binder list * module_ast option * module_ast option
+ | VernacDeclareModuleType of identifier *
+ module_binder list * module_ast option
+
(* Solving *)
| VernacSolve of int * raw_tactic_expr
| VernacSolveExistential of int * constr_ast
diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml
index 8e4189e2e..da4c56c57 100644
--- a/toplevel/vernacinterp.ml
+++ b/toplevel/vernacinterp.ml
@@ -11,6 +11,7 @@
open Pp
open Util
open Names
+open Libnames
open Himsg
open Proof_type
open Tacinterp
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 00:25:35 +0000