summaryrefslogtreecommitdiff
path: root/toplevel/vernacentries.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/vernacentries.ml')
-rw-r--r--toplevel/vernacentries.ml289
1 files changed, 158 insertions, 131 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 3f474239..c95c89d3 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: vernacentries.ml 11313 2008-08-07 11:15:03Z barras $ i*)
+(*i $Id: vernacentries.ml 11809 2009-01-20 11:39:55Z aspiwack $ i*)
(* Concrete syntax of the mathematical vernacular MV V2.6 *)
@@ -182,8 +182,11 @@ let show_match id =
let print_path_entry (s,l) =
(str (string_of_dirpath l) ++ str " " ++ tbrk (0,0) ++ str s)
-let print_loadpath () =
+let print_loadpath dir =
let l = Library.get_full_load_paths () in
+ let l = match dir with
+ | None -> l
+ | Some dir -> List.filter (fun (s,l) -> is_dirpath_prefix_of dir l) l in
msgnl (Pp.t (str "Logical Path: " ++
tab () ++ str "Physical path:" ++ fnl () ++
prlist_with_sep pr_fnl print_path_entry l))
@@ -232,7 +235,7 @@ let dump_universes s =
let locate_file f =
try
- let _,file = System.where_in_path false (Library.get_load_paths ()) f in
+ let _,file = System.where_in_path ~warn:false (Library.get_load_paths ()) f in
msgnl (str file)
with Not_found ->
msgnl (hov 0 (str"Can't find file" ++ spc () ++ str f ++ spc () ++
@@ -277,7 +280,7 @@ let print_located_module r =
let global_with_alias r =
let gr = global_with_alias r in
- if !Flags.dump then Constrintern.add_glob (loc_of_reference r) gr;
+ Dumpglob.add_glob (loc_of_reference r) gr;
gr
(**********)
@@ -307,49 +310,31 @@ let start_proof_and_print k l hook =
print_subgoals ();
if !pcoq <> None then (Option.get !pcoq).start_proof ()
-let current_dirpath sec =
- drop_dirpath_prefix (Lib.library_dp ())
- (if sec then Lib.cwd ()
- else extract_dirpath_prefix (Lib.sections_depth ()) (Lib.cwd ()))
-
-let dump_definition (loc, id) sec s =
- Flags.dump_string (Printf.sprintf "%s %d %s %s\n" s (fst (unloc loc))
- (string_of_dirpath (current_dirpath sec)) (string_of_id id))
-
-let dump_reference loc modpath ident ty =
- dump_string (Printf.sprintf "R%d %s %s %s %s\n"
- (fst (unloc loc)) (string_of_dirpath (Lib.library_dp ())) modpath ident ty)
-
-let dump_constraint ((loc, n), _, _) sec ty =
- match n with
- | Name id -> dump_definition (loc, id) sec ty
- | Anonymous -> ()
-
-let vernac_definition (local,_,_ as k) (_,id as lid) def hook =
- if !Flags.dump then dump_definition lid false "def";
- match def with
- | ProveBody (bl,t) -> (* local binders, typ *)
- if Lib.is_modtype () then
- errorlabstrm "Vernacentries.VernacDefinition"
- (str "Proof editing mode not supported in module types.")
- else
- let hook _ _ = () in
- start_proof_and_print (local,DefinitionBody Definition)
- [Some lid,(bl,t)] hook
- | DefineBody (bl,red_option,c,typ_opt) ->
- let red_option = match red_option with
- | None -> None
- | Some r ->
- let (evc,env)= Command.get_current_context () in
- Some (interp_redexp env evc r) in
- declare_definition id k bl red_option c typ_opt hook
-
+let vernac_definition (local,_,_ as k) (loc,id as lid) def hook =
+ Dumpglob.dump_definition lid false "def";
+ (match def with
+ | ProveBody (bl,t) -> (* local binders, typ *)
+ if Lib.is_modtype () then
+ errorlabstrm "Vernacentries.VernacDefinition"
+ (str "Proof editing mode not supported in module types")
+ else
+ let hook _ _ = () in
+ start_proof_and_print (local,DefinitionBody Definition)
+ [Some lid, (bl,t)] hook
+ | DefineBody (bl,red_option,c,typ_opt) ->
+ let red_option = match red_option with
+ | None -> None
+ | Some r ->
+ let (evc,env)= Command.get_current_context () in
+ Some (interp_redexp env evc r) in
+ declare_definition id k bl red_option c typ_opt hook)
+
let vernac_start_proof kind l lettop hook =
- if !Flags.dump then
+ if Dumpglob.dump () then
List.iter (fun (id, _) ->
match id with
- | Some lid -> dump_definition lid false "prf"
- | None -> ()) l;
+ | Some lid -> Dumpglob.dump_definition lid false "prf"
+ | None -> ()) l;
if not(refining ()) then
if lettop then
errorlabstrm "Vernacentries.StartProof"
@@ -383,28 +368,75 @@ let vernac_exact_proof c =
let vernac_assumption kind l nl=
let global = fst kind = Global in
- List.iter (fun (is_coe,(idl,c)) ->
- if !dump then
- List.iter (fun lid ->
- if global then dump_definition lid false "ax"
- else dump_definition lid true "var") idl;
- declare_assumption idl is_coe kind [] c false false nl) l
-
-let vernac_inductive f indl =
- if !dump then
- List.iter (fun ((lid, _, _, cstrs), _) ->
- dump_definition lid false"ind";
- List.iter (fun (_, (lid, _)) ->
- dump_definition lid false "constr") cstrs)
- indl;
- build_mutual indl f
+ List.iter (fun (is_coe,(idl,c)) ->
+ if Dumpglob.dump () then
+ List.iter (fun lid ->
+ if global then Dumpglob.dump_definition lid false "ax"
+ else Dumpglob.dump_definition lid true "var") idl;
+ declare_assumption idl is_coe kind [] c false false nl) l
+
+let vernac_record k finite struc binders sort nameopt cfs =
+ let const = match nameopt with
+ | None -> add_prefix "Build_" (snd (snd struc))
+ | Some (_,id as lid) ->
+ Dumpglob.dump_definition lid false "constr"; id in
+ let sigma = Evd.empty in
+ let env = Global.env() in
+ let s = Option.map (fun x ->
+ let s = Reductionops.whd_betadeltaiota env sigma (interp_constr sigma env x) in
+ match kind_of_term s with
+ | Sort s -> s
+ | _ -> user_err_loc
+ (constr_loc x,"definition_structure", str "Sort expected.")) sort
+ in
+ if Dumpglob.dump () then (
+ Dumpglob.dump_definition (snd struc) false "rec";
+ List.iter (fun ((_, x), _) ->
+ match x with
+ | Vernacexpr.AssumExpr ((loc, Name id), _) -> Dumpglob.dump_definition (loc,id) false "proj"
+ | _ -> ()) cfs);
+ ignore(Record.definition_structure (k,finite,struc,binders,cfs,const,s))
+
+let vernac_inductive finite indl =
+ if Dumpglob.dump () then
+ List.iter (fun (((coe,lid), _, _, _, cstrs), _) ->
+ match cstrs with
+ | Constructors cstrs ->
+ Dumpglob.dump_definition lid false "ind";
+ List.iter (fun (_, (lid, _)) ->
+ Dumpglob.dump_definition lid false "constr") cstrs
+ | _ -> () (* dumping is done by vernac_record (called below) *) )
+ indl;
+ match indl with
+ | [ ( id , bl , c , b, RecordDecl (oc,fs) ), None ] ->
+ vernac_record (match b with Class true -> Class false | _ -> b)
+ finite id bl c oc fs
+ | [ ( id , bl , c , Class true, Constructors [l]), _ ] ->
+ let f =
+ let (coe, ((loc, id), ce)) = l in
+ ((coe, AssumExpr ((loc, Name id), ce)), None)
+ in vernac_record (Class true) finite id bl c None [f]
+ | [ ( id , bl , c , Class true, _), _ ] ->
+ Util.error "Definitional classes must have a single method"
+ | [ ( id , bl , c , Class false, Constructors _), _ ] ->
+ Util.error "Inductive classes not supported"
+ | [ ( _ , _ , _ , _, RecordDecl _ ) , _ ] ->
+ Util.error "where clause not supported for (co)inductive records"
+ | _ -> let unpack = function
+ | ( (_, id) , bl , c , _ , Constructors l ) , ntn -> ( id , bl , c , l ) , ntn
+ | _ -> Util.error "Cannot handle mutually (co)inductive records."
+ in
+ let indl = List.map unpack indl in
+ Command.build_mutual indl (recursivity_flag_of_kind finite)
let vernac_fixpoint l b =
- List.iter (fun ((lid, _, _, _, _), _) -> dump_definition lid false "def") l;
+ if Dumpglob.dump () then
+ List.iter (fun ((lid, _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
build_recursive l b
let vernac_cofixpoint l b =
- List.iter (fun ((lid, _, _, _), _) -> dump_definition lid false "def") l;
+ if Dumpglob.dump () then
+ List.iter (fun ((lid, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
build_corecursive l b
let vernac_scheme = build_scheme
@@ -415,9 +447,11 @@ let vernac_combined_scheme = build_combined_scheme
(* Modules *)
let vernac_import export refl =
- let import ref = Library.import_module export (qualid_of_reference ref) in
- List.iter import refl;
- Lib.add_frozen_state ()
+ let import ref =
+ Library.import_module export (qualid_of_reference ref)
+ in
+ List.iter import refl;
+ Lib.add_frozen_state ()
let vernac_declare_module export (loc, id) binders_ast mty_ast_o =
(* We check the state of the system (in section, in module type)
@@ -435,9 +469,9 @@ let vernac_declare_module export (loc, id) binders_ast mty_ast_o =
Modintern.interp_modtype Modintern.interp_modexpr
id binders_ast (Some mty_ast_o) None
in
- Modintern.dump_moddef loc mp "mod";
- if_verbose message ("Module "^ string_of_id id ^" is declared");
- Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export
+ Dumpglob.dump_moddef loc mp "mod";
+ if_verbose message ("Module "^ string_of_id id ^" is declared");
+ Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export
let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_o =
(* We check the state of the system (in section, in module type)
@@ -455,7 +489,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_o =
let mp = Declaremods.start_module Modintern.interp_modtype export
id binders_ast mty_ast_o
in
- Modintern.dump_moddef loc mp "mod";
+ Dumpglob.dump_moddef loc mp "mod";
if_verbose message
("Interactive Module "^ string_of_id id ^" started") ;
List.iter
@@ -475,7 +509,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_o =
Modintern.interp_modtype Modintern.interp_modexpr
id binders_ast mty_ast_o mexpr_ast_o
in
- Modintern.dump_moddef loc mp "mod";
+ Dumpglob.dump_moddef loc mp "mod";
if_verbose message
("Module "^ string_of_id id ^" is defined");
Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)])
@@ -483,9 +517,9 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_o =
let vernac_end_module export (loc,id) =
let mp = Declaremods.end_module id in
- Modintern.dump_modref loc mp "mod";
- if_verbose message ("Module "^ string_of_id id ^" is defined") ;
- Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export
+ Dumpglob.dump_modref loc mp "mod";
+ if_verbose message ("Module "^ string_of_id id ^" is defined") ;
+ Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export
let vernac_declare_module_type (loc,id) binders_ast mty_ast_o =
@@ -501,7 +535,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_ast_o =
(idl,ty)::args, List.map (fun (_,i) -> export,i) idl) binders_ast
([],[]) in
let mp = Declaremods.start_modtype Modintern.interp_modtype id binders_ast in
- Modintern.dump_moddef loc mp "modtype";
+ Dumpglob.dump_moddef loc mp "modtype";
if_verbose message
("Interactive Module Type "^ string_of_id id ^" started");
List.iter
@@ -511,25 +545,25 @@ let vernac_declare_module_type (loc,id) binders_ast mty_ast_o =
) argsexport
| Some base_mty ->
- let binders_ast = List.map
- (fun (export,idl,ty) ->
- if export <> None then
- error ("Arguments of a functor definition can be imported only if" ^
- " the definition is interactive. Remove the \"Export\" " ^
- "and \"Import\" keywords from every functor argument.")
- else (idl,ty)) binders_ast in
- let mp = Declaremods.declare_modtype Modintern.interp_modtype
+ let binders_ast = List.map
+ (fun (export,idl,ty) ->
+ if export <> None then
+ error ("Arguments of a functor definition can be imported only if" ^
+ " the definition is interactive. Remove the \"Export\" " ^
+ "and \"Import\" keywords from every functor argument.")
+ else (idl,ty)) binders_ast in
+ let mp = Declaremods.declare_modtype Modintern.interp_modtype
id binders_ast base_mty in
- Modintern.dump_moddef loc mp "modtype";
- if_verbose message
- ("Module Type "^ string_of_id id ^" is defined")
+ Dumpglob.dump_moddef loc mp "modtype";
+ if_verbose message
+ ("Module Type "^ string_of_id id ^" is defined")
let vernac_end_modtype (loc,id) =
let mp = Declaremods.end_modtype id in
- Modintern.dump_modref loc mp "modtype";
- if_verbose message
- ("Module Type "^ string_of_id id ^" is defined")
+ Dumpglob.dump_modref loc mp "modtype";
+ if_verbose message
+ ("Module Type "^ string_of_id id ^" is defined")
let vernac_include = function
| CIMTE mty_ast ->
@@ -541,39 +575,18 @@ let vernac_include = function
(**********************)
(* Gallina extensions *)
-
-let vernac_record struc binders sort nameopt cfs =
- let const = match nameopt with
- | None -> add_prefix "Build_" (snd (snd struc))
- | Some (_,id as lid) ->
- if !dump then dump_definition lid false "constr"; id in
- let sigma = Evd.empty in
- let env = Global.env() in
- let s = interp_constr sigma env sort in
- let s = Reductionops.whd_betadeltaiota env sigma s in
- let s = match kind_of_term s with
- | Sort s -> s
- | _ -> user_err_loc
- (constr_loc sort,"definition_structure", str "Sort expected.") in
- if !dump then (
- dump_definition (snd struc) false "rec";
- List.iter (fun (_, x) ->
- match x with
- | AssumExpr ((loc, Name id), _) -> dump_definition (loc,id) false "proj"
- | _ -> ()) cfs);
- ignore(Record.definition_structure (struc,binders,cfs,const,s))
(* Sections *)
let vernac_begin_section (_, id as lid) =
check_no_pending_proofs ();
- if !Flags.dump then dump_definition lid true "sec";
+ Dumpglob.dump_definition lid true "sec";
Lib.open_section id
let vernac_end_section (loc, id) =
- if !Flags.dump then
- dump_reference loc
- (string_of_dirpath (current_dirpath true)) "<>" "sec";
+
+ Dumpglob.dump_reference loc
+ (string_of_dirpath (Lib.current_dirpath true)) "<>" "sec";
Lib.close_section id
let vernac_end_segment lid =
@@ -588,6 +601,10 @@ let vernac_end_segment lid =
let vernac_require import _ qidl =
let qidl = List.map qualid_of_reference qidl in
+ if Dumpglob.dump () then begin
+ let modrefl = Flags.silently (List.map Library.try_locate_qualified_library) qidl in
+ List.iter2 (fun (loc, _) dp -> Dumpglob.dump_libref loc dp "lib") qidl (List.map fst modrefl)
+ end;
Library.require_library qidl import
let vernac_canonical r =
@@ -606,21 +623,17 @@ let vernac_identity_coercion stre id qids qidt =
Class.try_add_new_identity_coercion id stre source target
(* Type classes *)
-let vernac_class id par ar sup props =
- if !dump then (
- dump_definition id false "class";
- List.iter (fun (lid, _, _) -> dump_definition lid false "meth") props);
- Classes.new_class id par ar sup props
let vernac_instance glob sup inst props pri =
- if !dump then dump_constraint inst false "inst";
+ Dumpglob.dump_constraint inst false "inst";
ignore(Classes.new_instance ~global:glob sup inst props pri)
let vernac_context l =
+ List.iter (fun x -> Dumpglob.dump_local_binder x true "var") l;
Classes.context l
let vernac_declare_instance id =
- if !dump then dump_definition id false "inst";
+ Dumpglob.dump_definition id false "inst";
Classes.declare_instance false id
(***********)
@@ -752,15 +765,18 @@ let vernac_backto n = Lib.reset_label n
let vernac_declare_tactic_definition = Tacinterp.add_tacdef
+let vernac_create_hintdb local id b =
+ Auto.create_hint_db local id full_transparent_state b
+
let vernac_hints = Auto.add_hints
let vernac_syntactic_definition lid =
- dump_definition lid false "syndef";
+ Dumpglob.dump_definition lid false "syndef";
Command.syntax_definition (snd lid)
let vernac_declare_implicits local r = function
| Some imps ->
- Impargs.declare_manual_implicits local (global_with_alias r) false
+ Impargs.declare_manual_implicits local (global_with_alias r) ~enriching:false
(List.map (fun (ex,b,f) -> ex, (b,f)) imps)
| None ->
Impargs.declare_implicits local (global_with_alias r)
@@ -1059,7 +1075,7 @@ let vernac_print = function
| PrintSectionContext qid -> msg (print_sec_context_typ qid)
| PrintInspect n -> msg (inspect n)
| PrintGrammar ent -> Metasyntax.print_grammar ent
- | PrintLoadPath -> (* For compatibility ? *) print_loadpath ()
+ | PrintLoadPath dir -> (* For compatibility ? *) print_loadpath dir
| PrintModules -> msg (print_modules ())
| PrintModule qid -> print_module qid
| PrintModuleType qid -> print_modtype qid
@@ -1085,7 +1101,6 @@ let vernac_print = function
| PrintHintDbName s -> Auto.print_hint_db_by_name s
| PrintRewriteHintDbName s -> Autorewrite.print_rewrite_hintdb s
| PrintHintDb -> Auto.print_searchtable ()
- | PrintSetoids -> Setoid_replace.print_setoids()
| PrintScopes ->
pp (Notation.pr_scopes (Constrextern.without_symbols pr_lrawconstr))
| PrintScope s ->
@@ -1113,24 +1128,38 @@ let interp_search_restriction = function
open Search
+let is_ident s = try ignore (check_ident s); true with UserError _ -> false
+
let interp_search_about_item = function
- | SearchRef r -> GlobSearchRef (global_with_alias r)
- | SearchString s -> GlobSearchString s
+ | SearchSubPattern pat ->
+ let _,pat = intern_constr_pattern Evd.empty (Global.env()) pat in
+ GlobSearchSubPattern pat
+ | SearchString (s,None) when is_ident s ->
+ GlobSearchString s
+ | SearchString (s,sc) ->
+ try
+ let ref =
+ Notation.interp_notation_as_global_reference dummy_loc
+ (fun _ -> true) s sc in
+ GlobSearchSubPattern (Pattern.PRef ref)
+ with UserError _ ->
+ error ("Unable to interp \""^s^"\" either as a reference or
+ as an identifier component")
let vernac_search s r =
let r = interp_search_restriction r in
if !pcoq <> None then (Option.get !pcoq).search s r else
match s with
| SearchPattern c ->
- let _,pat = interp_constrpattern Evd.empty (Global.env()) c in
+ let _,pat = intern_constr_pattern Evd.empty (Global.env()) c in
Search.search_pattern pat r
| SearchRewrite c ->
- let _,pat = interp_constrpattern Evd.empty (Global.env()) c in
+ let _,pat = intern_constr_pattern Evd.empty (Global.env()) c in
Search.search_rewrite pat r
| SearchHead ref ->
Search.search_by_head (global_with_alias ref) r
| SearchAbout sl ->
- Search.search_about (List.map interp_search_about_item sl) r
+ Search.search_about (List.map (on_snd interp_search_about_item) sl) r
let vernac_locate = function
| LocateTerm qid -> msgnl (print_located_qualid qid)
@@ -1309,7 +1338,6 @@ let interp c = match c with
| VernacEndSegment lid -> vernac_end_segment lid
- | 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
@@ -1317,8 +1345,6 @@ let interp c = match c with
| VernacIdentityCoercion (str,(_,id),s,t) -> vernac_identity_coercion str id s t
(* Type classes *)
- | VernacClass (id, par, ar, sup, props) -> vernac_class id par ar sup props
-
| VernacInstance (glob, sup, inst, props, pri) -> vernac_instance glob sup inst props pri
| VernacContext sup -> vernac_context sup
| VernacDeclareInstance id -> vernac_declare_instance id
@@ -1356,6 +1382,7 @@ let interp c = match c with
(* Commands *)
| VernacDeclareTacticDefinition (x,l) -> vernac_declare_tactic_definition x l
+ | VernacCreateHintDb (local,dbname,b) -> vernac_create_hintdb local dbname b
| VernacHints (local,dbnames,hints) -> vernac_hints local dbnames hints
| VernacSyntacticDefinition (id,c,l,b) ->vernac_syntactic_definition id c l b
| VernacDeclareImplicits (local,qid,l) ->vernac_declare_implicits local qid l
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 01:55:27 +0000