summaryrefslogtreecommitdiff
path: root/toplevel/vernacentries.ml
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-04-28 14:59:16 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-04-28 14:59:16 +0000
commit3ef7797ef6fc605dfafb32523261fe1b023aeecb (patch)
treead89c6bb57ceee608fcba2bb3435b74e0f57919e /toplevel/vernacentries.ml
parent018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff)
Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha
Diffstat (limited to 'toplevel/vernacentries.ml')
-rw-r--r--toplevel/vernacentries.ml586
1 files changed, 265 insertions, 321 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 1c6ad9a6..7394bd8f 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,v 1.195.2.1 2004/07/16 19:31:50 herbelin Exp $ i*)
+(*i $Id: vernacentries.ml 8700 2006-04-11 23:14:15Z courtieu $ i*)
(* Concrete syntax of the mathematical vernacular MV V2.6 *)
@@ -23,6 +23,7 @@ open Proof_trees
open Constrintern
open Prettyp
open Printer
+open Tactic_printer
open Tacinterp
open Command
open Goptions
@@ -32,6 +33,7 @@ open Vernacexpr
open Decl_kinds
open Topconstr
open Pretyping
+open Redexpr
(* Pcoq hooks *)
@@ -55,14 +57,13 @@ let set_pcoq_hook f = pcoq := Some f
let cl_of_qualid = function
| FunClass -> Classops.CL_FUN
| SortClass -> Classops.CL_SORT
- | RefClass r -> Class.class_of_ref (Nametab.global r)
+ | RefClass r -> Class.class_of_global (Nametab.global r)
(*******************)
(* "Show" commands *)
let show_proof () =
let pts = get_pftreestate () in
- let pf = proof_of_pftreestate pts in
let cursor = cursor_of_pftreestate pts in
let evc = evc_of_pftreestate pts in
let (pfterm,meta_types) = extract_open_pftreestate pts in
@@ -70,41 +71,41 @@ let show_proof () =
prlist_with_sep pr_spc pr_int (List.rev cursor) ++ fnl () ++
str"Subgoals" ++ fnl () ++
prlist (fun (mv,ty) -> Nameops.pr_meta mv ++ str" -> " ++
- prtype ty ++ fnl ())
+ pr_ltype ty ++ fnl ())
meta_types
- ++ str"Proof: " ++ prterm (Evarutil.nf_evar evc pfterm))
+ ++ str"Proof: " ++ pr_lconstr (Evarutil.nf_evar evc pfterm))
let show_node () =
let pts = get_pftreestate () in
let pf = proof_of_pftreestate pts
and cursor = cursor_of_pftreestate pts in
msgnl (prlist_with_sep pr_spc pr_int (List.rev cursor) ++ fnl () ++
- prgl (goal_of_proof pf) ++ fnl () ++
+ pr_goal (goal_of_proof pf) ++ fnl () ++
(match pf.Proof_type.ref with
| None -> (str"BY <rule>")
| Some(r,spfl) ->
- (str"BY " ++ Refiner.pr_rule r ++ fnl () ++
+ (str"BY " ++ pr_rule r ++ fnl () ++
str" " ++
- hov 0 (prlist_with_sep pr_fnl prgl
+ hov 0 (prlist_with_sep pr_fnl pr_goal
(List.map goal_of_proof spfl)))))
let show_script () =
let pts = get_pftreestate () in
let pf = proof_of_pftreestate pts
and evc = evc_of_pftreestate pts in
- msgnl (Refiner.print_treescript true evc (Global.named_context()) pf)
+ msgnl (print_treescript true evc (Global.named_context()) pf)
let show_top_evars () =
let pfts = get_pftreestate () in
let gls = top_goal_of_pftreestate pfts in
let sigma = project gls in
- msg (pr_evars_int 1 (Evd.non_instantiated sigma))
+ msg (pr_evars_int 1 (Evarutil.non_instantiated sigma))
let show_prooftree () =
let pts = get_pftreestate () in
let pf = proof_of_pftreestate pts
and evc = evc_of_pftreestate pts in
- msg (Refiner.print_proof evc (Global.named_context()) pf)
+ msg (print_proof evc (Global.named_context()) pf)
let print_subgoals () = if_verbose (fun () -> msg (pr_open_subgoals ())) ()
@@ -112,7 +113,7 @@ let print_subgoals () = if_verbose (fun () -> msg (pr_open_subgoals ())) ()
let fresh_id_of_name avoid gl = function
Anonymous -> Tactics.fresh_id avoid (id_of_string "H") gl
- | Name id -> id
+ | Name id -> Tactics.fresh_id avoid id gl
let rec do_renum avoid gl = function
[] -> mt ()
@@ -121,27 +122,83 @@ let rec do_renum avoid gl = function
let id = fresh_id_of_name avoid gl n in
pr_id id ++ spc () ++ do_renum (id :: avoid) gl l
+(* Transforms a product term (x1:T1)..(xn:Tn)T into the pair
+ ([(xn,Tn);...;(x1,T1)],T), where T is not a product nor a letin *)
+let decompose_prod_letins =
+ let rec prodec_rec l c = match kind_of_term c with
+ | Prod (x,t,c) -> prodec_rec ((x,t)::l) c
+ | LetIn (x,b,t,c) -> prodec_rec ((x,t)::l) c
+ | Cast (c,_,_) -> prodec_rec l c
+ | _ -> l,c
+ in
+ prodec_rec []
+
let show_intro all =
let pf = get_pftreestate() in
let gl = nth_goal_of_pftreestate 1 pf in
- let l,_= decompose_prod (strip_outer_cast (pf_concl gl)) in
+ let l,_= decompose_prod_letins (strip_outer_cast (pf_concl gl)) in
let nl = List.rev_map fst l in
- if all then
- msgnl (do_renum [] gl nl)
- else
- try
- let n = List.hd nl in
- msgnl (pr_id (fresh_id_of_name [] gl n))
- with Failure "hd" -> message ""
+ if all then msgnl (hov 0 (do_renum [] gl nl))
+ else try
+ let n = List.hd nl in
+ msgnl (pr_id (fresh_id_of_name [] gl n))
+ with Failure "hd" -> message ""
+
+
+let id_of_name = function
+ | Names.Anonymous -> id_of_string "x"
+ | Names.Name x -> x
+
+
+(* Building of match expression *)
+(* From ide/coq.ml *)
+let make_cases s =
+ let qualified_name = Libnames.qualid_of_string s in
+ let glob_ref = Nametab.locate qualified_name in
+ match glob_ref with
+ | Libnames.IndRef i ->
+ let {Declarations.mind_nparams = np}
+ , {Declarations.mind_consnames = carr ; Declarations.mind_nf_lc = tarr }
+ = Global.lookup_inductive i in
+ Util.array_fold_right2
+ (fun n t l ->
+ let (al,_) = Term.decompose_prod t in
+ let al,_ = Util.list_chop (List.length al - np) al in
+ let rec rename avoid = function
+ | [] -> []
+ | (n,_)::l ->
+ let n' = Termops.next_global_ident_away true (id_of_name n) avoid in
+ string_of_id n' :: rename (n'::avoid) l in
+ let al' = rename [] (List.rev al) in
+ (string_of_id n :: al') :: l)
+ carr tarr []
+ | _ -> raise Not_found
+
+
+let show_match id =
+ try
+ let s = string_of_id (snd id) in
+ let patterns = make_cases s in
+ let cases =
+ List.fold_left
+ (fun acc x ->
+ match x with
+ | [] -> assert false
+ | [x] -> "| "^ x ^ " => \n" ^ acc
+ | x::l ->
+ "| (" ^ List.fold_left (fun acc s -> acc ^ " " ^ s) x l ^ ")"
+ ^ " => \n" ^ acc)
+ "end" patterns in
+ msg (str ("match # with\n" ^ cases))
+ with Not_found -> error "Unknown inductive type"
-(********************)
(* "Print" commands *)
let print_path_entry (s,l) =
(str s ++ str " " ++ tbrk (0,2) ++ str (string_of_dirpath l))
let print_loadpath () =
- let l = Library.get_full_load_path () in
+ let l = Library.get_full_load_paths () in
msgnl (Pp.t (str "Physical path: " ++
tab () ++ str "Logical Path:" ++ fnl () ++
prlist_with_sep pr_fnl print_path_entry l))
@@ -190,8 +247,7 @@ let dump_universes s =
let locate_file f =
try
- let _,file =
- System.where_in_path (Library.get_load_path()) f in
+ let _,file = System.where_in_path (Library.get_load_paths ()) f in
msgnl (str file)
with Not_found ->
msgnl (hov 0 (str"Can't find file" ++ spc () ++ str f ++ spc () ++
@@ -219,13 +275,22 @@ let print_located_library r =
try msg_found_library (Library.locate_qualified_library qid)
with e -> msg_notfound_library loc qid e
+let print_located_module r =
+ let (loc,qid) = qualid_of_reference r in
+ let msg =
+ try
+ let dir = Nametab.full_name_module qid in
+ str "Module " ++ pr_dirpath dir
+ with Not_found ->
+ (if fst (repr_qualid qid) = empty_dirpath then
+ str "No module is referred to by basename "
+ else
+ str "No module is referred to by name ") ++ pr_qualid qid
+ in msgnl msg
+
(**********)
(* Syntax *)
-let vernac_syntax = Metasyntax.add_syntax_obj
-
-let vernac_grammar = Metasyntax.add_grammar_obj
-
let vernac_syntax_extension = Metasyntax.add_syntax_extension
let vernac_delimiters = Metasyntax.add_delimiters
@@ -233,15 +298,13 @@ let vernac_delimiters = Metasyntax.add_delimiters
let vernac_bind_scope sc cll =
List.iter (fun cl -> Metasyntax.add_class_scope sc (cl_of_qualid cl)) cll
-let vernac_open_close_scope = Symbols.open_close_scope
+let vernac_open_close_scope = Notation.open_close_scope
let vernac_arguments_scope qid scl =
- Symbols.declare_arguments_scope (global qid) scl
+ Notation.declare_arguments_scope (global qid) scl
let vernac_infix = Metasyntax.add_infix
-let vernac_distfix = Metasyntax.add_distfix
-
let vernac_notation = Metasyntax.add_notation
(***********)
@@ -252,7 +315,7 @@ let start_proof_and_print idopt k t hook =
print_subgoals ();
if !pcoq <> None then (out_some !pcoq).start_proof ()
-let vernac_definition (local,_ as k) id def hook =
+let vernac_definition (local,_,_ as k) id def hook =
match def with
| ProveBody (bl,t) -> (* local binders, typ *)
if Lib.is_modtype () then
@@ -260,8 +323,7 @@ let vernac_definition (local,_ as k) id def hook =
(str "Proof editing mode not supported in module types")
else
let hook _ _ = () in
- let kind = if local=Local then IsLocal else IsGlobal DefinitionBody in
- start_proof_and_print (Some id) kind (bl,t) hook
+ start_proof_and_print (Some id) (local,DefinitionBody Definition) (bl,t) hook
| DefineBody (bl,red_option,c,typ_opt) ->
let red_option = match red_option with
| None -> None
@@ -278,7 +340,7 @@ let vernac_start_proof kind sopt (bl,t) lettop hook =
if Lib.is_modtype () then
errorlabstrm "Vernacentries.StartProof"
(str "Proof editing mode not supported in module types");
- start_proof_and_print sopt (IsGlobal (Proof kind)) (bl,t) hook
+ start_proof_and_print sopt (Global, Proof kind) (bl,t) hook
let vernac_end_proof = function
| Admitted -> admit ()
@@ -293,9 +355,15 @@ let vernac_end_proof = function
the theories [??] *)
let vernac_exact_proof c =
- by (Tactics.exact_proof c);
- save_named true
-
+ let pfs = top_of_tree (get_pftreestate()) in
+ let pf = proof_of_pftreestate pfs in
+ if (is_leaf_proof pf) then begin
+ by (Tactics.exact_proof c);
+ save_named true end
+ else
+ errorlabstrm "Vernacentries.ExactProof"
+ (str "Command 'Proof ...' can only be used at the beginning of the proof")
+
let vernac_assumption kind l =
List.iter (fun (is_coe,(idl,c)) -> declare_assumption idl is_coe kind [] c) l
@@ -310,107 +378,70 @@ let vernac_scheme = build_scheme
(**********************)
(* Modules *)
-let vernac_declare_module id binders_ast mty_ast_o mexpr_ast_o =
+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 vernac_declare_module export id binders_ast mty_ast_o =
(* We check the state of the system (in section, in module type)
and what module information is supplied *)
if Lib.sections_are_opened () then
error "Modules and Module Types are not allowed inside sections";
-
- if not (Lib.is_modtype ()) then
- error "Declare Module allowed in module types only";
-
- let constrain_mty = match mty_ast_o with
- Some (_,true) -> true
- | _ -> false
- in
-
- match mty_ast_o, constrain_mty, mexpr_ast_o with
- | _, false, None -> (* no ident, no/soft type *)
- Declaremods.start_module Modintern.interp_modtype
- id binders_ast mty_ast_o;
- if_verbose message
- ("Interactive Declaration of Module "^ string_of_id id ^" started")
-
- | Some _, true, None (* no ident, hard type *)
- | _, false, Some (CMEident _) -> (* ident, no/soft type *)
- Declaremods.declare_module
- Modintern.interp_modtype Modintern.interp_modexpr
- id binders_ast mty_ast_o mexpr_ast_o;
- if_verbose message
- ("Module "^ string_of_id id ^" is declared")
-
- | _, true, Some (CMEident _) -> (* ident, hard type *)
- error "You cannot declare an equality and a type in module declaration"
-
- | _, _, Some _ -> (* not ident *)
- error "Only simple modules allowed in module declarations"
-
- | None,true,None -> assert false (* 1st None ==> false *)
-
-let vernac_define_module id binders_ast mty_ast_o mexpr_ast_o =
+ let binders_ast = List.map
+ (fun (export,idl,ty) ->
+ if export <> None then
+ error ("Arguments of a functor declaration cannot be exported. " ^
+ "Remove the \"Export\" and \"Import\" keywords from every functor " ^
+ "argument.")
+ else (idl,ty)) binders_ast in
+ Declaremods.declare_module
+ Modintern.interp_modtype Modintern.interp_modexpr
+ id binders_ast (Some mty_ast_o) None;
+ 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 id binders_ast mty_ast_o mexpr_ast_o =
(* We check the state of the system (in section, in module type)
and what module information is supplied *)
if Lib.sections_are_opened () then
error "Modules and Module Types are not allowed inside sections";
-
- if Lib.is_modtype () then
- error "Module definitions not allowed in module types. Use Declare Module instead";
-
match mexpr_ast_o with
| None ->
- Declaremods.start_module Modintern.interp_modtype
+ let binders_ast,argsexport =
+ List.fold_right
+ (fun (export,idl,ty) (args,argsexport) ->
+ (idl,ty)::args, List.map (fun (_,i) -> export,i) idl) binders_ast
+ ([],[]) in
+ Declaremods.start_module Modintern.interp_modtype export
id binders_ast mty_ast_o;
if_verbose message
- ("Interactive Module "^ string_of_id id ^" started")
-
+ ("Interactive Module "^ string_of_id id ^" started") ;
+ List.iter
+ (fun (export,id) ->
+ option_iter
+ (fun export -> vernac_import export [Ident (dummy_loc,id)]) export
+ ) argsexport
| Some _ ->
+ 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
Declaremods.declare_module
Modintern.interp_modtype Modintern.interp_modexpr
id binders_ast mty_ast_o mexpr_ast_o;
if_verbose message
- ("Module "^ string_of_id id ^" is defined")
-
-(* let vernac_declare_module id binders_ast mty_ast_o mexpr_ast_o = *)
-(* (\* We check the state of the system (in section, in module type) *)
-(* and what module information is supplied *\) *)
-(* if Lib.sections_are_opened () then *)
-(* error "Modules and Module Types are not allowed inside sections"; *)
-
-(* let constrain_mty = match mty_ast_o with *)
-(* Some (_,true) -> true *)
-(* | _ -> false *)
-(* in *)
-
-(* match Lib.is_modtype (), mty_ast_o, constrain_mty, mexpr_ast_o with *)
-(* | _, None, _, None *)
-(* | true, Some _, false, None *)
-(* | false, _, _, None -> *)
-(* Declaremods.start_module Modintern.interp_modtype *)
-(* id binders_ast mty_ast_o; *)
-(* if_verbose message *)
-(* ("Interactive Module "^ string_of_id id ^" started") *)
-
-(* | true, Some _, true, None *)
-(* | true, _, false, Some (CMEident _) *)
-(* | false, _, _, Some _ -> *)
-(* Declaremods.declare_module *)
-(* Modintern.interp_modtype Modintern.interp_modexpr *)
-(* id binders_ast mty_ast_o mexpr_ast_o; *)
-(* if_verbose message *)
-(* ("Module "^ string_of_id id ^" is defined") *)
-
-(* | true, _, _, _ -> *)
-(* error "Module definition not allowed in a Module Type" *)
-
-let vernac_end_module id =
- Declaremods.end_module id;
- if_verbose message
- (if Lib.is_modtype () then
- "Module "^ string_of_id id ^" is declared"
- else
- "Module "^ string_of_id id ^" is defined")
+ ("Module "^ string_of_id id ^" is defined");
+ option_iter (fun export -> vernac_import export [Ident (dummy_loc,id)])
+ export
-
+let vernac_end_module export id =
+ Declaremods.end_module id;
+ 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 id binders_ast mty_ast_o =
@@ -419,11 +450,28 @@ let vernac_declare_module_type id binders_ast mty_ast_o =
match mty_ast_o with
| None ->
+ let binders_ast,argsexport =
+ List.fold_right
+ (fun (export,idl,ty) (args,argsexport) ->
+ (idl,ty)::args, List.map (fun (_,i) -> export,i) idl) binders_ast
+ ([],[]) in
Declaremods.start_modtype Modintern.interp_modtype id binders_ast;
if_verbose message
- ("Interactive Module Type "^ string_of_id id ^" started")
+ ("Interactive Module Type "^ string_of_id id ^" started");
+ List.iter
+ (fun (export,id) ->
+ option_iter
+ (fun export -> vernac_import export [Ident (dummy_loc,id)]) export
+ ) 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
Declaremods.declare_modtype Modintern.interp_modtype
id binders_ast base_mty;
if_verbose message
@@ -455,86 +503,26 @@ let vernac_record struc binders sort nameopt cfs =
(* Sections *)
-let vernac_begin_section id = let _ = Lib.open_section id in ()
-
-let vernac_end_section id =
- Discharge.close_section (is_verbose ()) id
-
+let vernac_begin_section = Lib.open_section
+let vernac_end_section = Lib.close_section
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 ->
- (match string_of_id id with
- | ("Refine" | "Inv" | "Equality" | "EAuto" | "AutoRewrite"
- | "EqDecide" | "Xml" | "Extraction" | "Tauto" | "Setoid_replace"
- | "Elimdep"
- | "DatatypesSyntax" | "LogicSyntax" | "Logic_TypeSyntax"
- | "SpecifSyntax" | "PeanoSyntax" | "TypeSyntax" | "PolyListSyntax")
- -> true
- | _ -> false)
- | _ -> false
-
-let test_renamed_module (_,qid) =
- match repr_qualid qid with
- | dir, id when dir = empty_dirpath ->
- (match string_of_id id with
- | "List" -> warning "List has been renamed into MonoList"
- | "PolyList" -> warning "PolyList has been renamed into List and old List into MonoList"
- | _ -> ())
- | _ -> ()
-
+ let o =
+ try Lib.what_is_opened ()
+ with Not_found -> error "There is nothing to end." in
+ match o with
+ | _,Lib.OpenedModule (export,_,_) -> vernac_end_module export id
+ | _,Lib.OpenedModtype _ -> vernac_end_modtype id
+ | _,Lib.OpenedSection _ -> vernac_end_section id
+ | _ -> anomaly "No more opened things"
+
let vernac_require import _ qidl =
let qidl = List.map qualid_of_reference qidl in
- try
- match import with
- | 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
- if qidl' = qidl then
- List.iter
- (fun (_,qid) ->
- warning ("Module "^(string_of_qualid qid)^
- " is now built-in and shouldn't be required")) qidl
- else
- (if not !Options.v7 then List.iter test_renamed_module qidl;
- raise e)
-
-let vernac_import export refl =
- let import_one ref =
- let qid = qualid_of_reference ref in
- Library.import_library export qid
- in
- List.iter import_one refl;
- Lib.add_frozen_state ()
-
-(* 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;
-*)
+ Library.require_library qidl import
let vernac_canonical locqid =
- Recordobj.objdef_declare (Nametab.global locqid)
+ Recordops.declare_canonical_structure (Nametab.global locqid)
let locate_reference ref =
let (loc,qid) = qualid_of_reference ref in
@@ -591,18 +579,14 @@ let vernac_solve_existential = instantiate_nth_evar_com
let vernac_set_end_tac tac =
if not (refining ()) then
error "Unknown command of the non proof-editing mode";
- if tac <> (Tacexpr.TacId "") then set_end_tac (Tacinterp.interp tac)
-(* TO DO verifier s'il faut pas mettre exist s | TacId s ici*)
-
-
+ if tac <> (Tacexpr.TacId []) then set_end_tac (Tacinterp.interp tac) else ()
+ (* TO DO verifier s'il faut pas mettre exist s | TacId s ici*)
+
(*****************************)
(* Auxiliary file management *)
let vernac_require_from export spec filename =
- match export with
- Some exp ->
- Library.require_library_from_file spec None filename exp
- | None -> Library.read_library_from_file filename
+ Library.require_library_from_file None filename export
let vernac_add_loadpath isrec pdir ldiropt =
let alias = match ldiropt with
@@ -610,7 +594,7 @@ let vernac_add_loadpath isrec pdir ldiropt =
| Some ldir -> ldir in
(if isrec then Mltop.add_rec_path else Mltop.add_path) pdir alias
-let vernac_remove_loadpath = Library.remove_path
+let vernac_remove_loadpath = Library.remove_load_path
(* Coq syntax for ML or system commands *)
@@ -651,7 +635,9 @@ let vernac_reset_initial () = abort_refine Lib.reset_initial ()
let vernac_back n = Lib.back n
+let vernac_backto n = Lib.reset_label n
+(* see also [vernac_backtrack] which combines undoing and resetting *)
(************)
(* Commands *)
@@ -667,7 +653,7 @@ let vernac_declare_implicits locqid = function
let vernac_reserve idl c =
let t = Constrintern.interp_type Evd.empty (Global.env()) c in
- let t = Detyping.detype (false,Global.env()) [] [] t in
+ let t = Detyping.detype false [] [] t in
List.iter (fun id -> Reserve.declare_reserved_type id t) idl
let make_silent_if_not_pcoq b =
@@ -691,13 +677,11 @@ let _ =
optread = Impargs.is_implicit_args;
optwrite = Impargs.make_implicit_args }
-let impargs = if !Options.v7 then "Implicits" else "Implicit"
-
let _ =
declare_bool_option
- { optsync = false; (* synchronisation is in Impargs *)
+ { optsync = true;
optname = "strict implicit arguments";
- optkey = (SecondaryTable ("Strict",impargs));
+ optkey = (SecondaryTable ("Strict","Implicit"));
optread = Impargs.is_strict_implicit_args;
optwrite = Impargs.make_strict_implicit_args }
@@ -705,7 +689,7 @@ let _ =
declare_bool_option
{ optsync = true;
optname = "contextual implicit arguments";
- optkey = (SecondaryTable ("Contextual",impargs));
+ optkey = (SecondaryTable ("Contextual","Implicit"));
optread = Impargs.is_contextual_implicit_args;
optwrite = Impargs.make_contextual_implicit_args }
@@ -721,7 +705,7 @@ let _ =
declare_bool_option
{ optsync = true;
optname = "implicit arguments printing";
- optkey = (SecondaryTable ("Printing",impargs));
+ optkey = (SecondaryTable ("Printing","Implicit"));
optread = (fun () -> !Constrextern.print_implicits);
optwrite = (fun b -> Constrextern.print_implicits := b) }
@@ -737,7 +721,7 @@ let _ =
declare_bool_option
{ optsync = true;
optname = "notations printing";
- optkey = (SecondaryTable ("Printing",if !Options.v7 then "Symbols" else "Notations"));
+ optkey = (SecondaryTable ("Printing","Notations"));
optread = (fun () -> not !Constrextern.print_no_symbol);
optwrite = (fun b -> Constrextern.print_no_symbol := not b) }
@@ -750,6 +734,30 @@ let _ =
optwrite = (fun b -> Options.raw_print := b) }
let _ =
+ declare_bool_option
+ { optsync = true;
+ optname = "use of virtual machine inside the kernel";
+ optkey = (SecondaryTable ("Virtual","Machine"));
+ optread = (fun () -> Vconv.use_vm ());
+ optwrite = (fun b -> Vconv.set_use_vm b) }
+
+let _ =
+ declare_bool_option
+ { optsync = true;
+ optname = "use of boxed definitions";
+ optkey = (SecondaryTable ("Boxed","Definitions"));
+ optread = Options.boxed_definitions;
+ optwrite = (fun b -> Options.set_boxed_definitions b) }
+
+let _ =
+ declare_bool_option
+ { optsync = true;
+ optname = "use of boxed values";
+ optkey = (SecondaryTable ("Boxed","Values"));
+ optread = (fun _ -> not (Vm.transp_values ()));
+ optwrite = (fun b -> Vm.set_transp_values (not b)) }
+
+let _ =
declare_int_option
{ optsync=false;
optkey=PrimaryTable("Undo");
@@ -784,11 +792,11 @@ let _ =
let vernac_set_opacity opaq locqid =
match Nametab.global locqid with
| ConstRef sp ->
- if opaq then Tacred.set_opaque_const sp
- else Tacred.set_transparent_const sp
+ if opaq then set_opaque_const sp
+ else set_transparent_const sp
| VarRef id ->
- if opaq then Tacred.set_opaque_var id
- else Tacred.set_transparent_var id
+ if opaq then set_opaque_var id
+ else set_transparent_var id
| _ -> error "cannot set an inductive type or a constructor as transparent"
let vernac_set_option key = function
@@ -843,7 +851,7 @@ let vernac_check_may_eval redexp glopt rc =
if !pcoq <> None then (out_some !pcoq).print_check j
else msg (print_judgment env j)
| Some r ->
- let redfun = Tacred.reduction_of_redexp (interp_redexp env evmap r) in
+ let redfun = fst (reduction_of_red_expr (interp_redexp env evmap r)) in
if !pcoq <> None
then (out_some !pcoq).print_eval (redfun env evmap) env rc j
else msg (print_eval redfun env j)
@@ -859,7 +867,6 @@ let vernac_global_check c =
let vernac_print = function
| PrintTables -> print_tables ()
- | PrintLocalContext -> msg (print_local_context ())
| PrintFullContext -> msg (print_full_context_typ ())
| PrintSectionContext qid -> msg (print_sec_context_typ qid)
| PrintInspect n -> msg (inspect n)
@@ -876,21 +883,25 @@ let vernac_print = function
| PrintOpaqueName qid -> msg (print_opaque_name qid)
| PrintGraph -> ppnl (Prettyp.print_graph())
| PrintClasses -> ppnl (Prettyp.print_classes())
+ | PrintLtac qid -> ppnl (Tacinterp.print_ltac (snd (qualid_of_reference qid)))
| PrintCoercions -> ppnl (Prettyp.print_coercions())
| PrintCoercionPaths (cls,clt) ->
ppnl (Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt))
+ | PrintCanonicalConversions -> ppnl (Prettyp.print_canonical_projections ())
| PrintUniverses None -> pp (Univ.pr_universes (Global.universes ()))
| PrintUniverses (Some s) -> dump_universes s
| PrintHint qid -> Auto.print_hint_ref (Nametab.global qid)
| PrintHintGoal -> Auto.print_applicable_hint ()
| 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 (Symbols.pr_scopes (Constrextern.without_symbols pr_rawterm))
+ pp (Notation.pr_scopes (Constrextern.without_symbols pr_lrawconstr))
| PrintScope s ->
- pp (Symbols.pr_scope (Constrextern.without_symbols pr_rawterm) s)
+ pp (Notation.pr_scope (Constrextern.without_symbols pr_lrawconstr) s)
| PrintVisibility s ->
- pp (Symbols.pr_visibility (Constrextern.without_symbols pr_rawterm) s)
+ pp (Notation.pr_visibility (Constrextern.without_symbols pr_lrawconstr) s)
| PrintAbout qid -> msgnl (print_about qid)
| PrintImplicit qid -> msg (print_impargs qid)
@@ -929,10 +940,11 @@ let vernac_search s r =
let vernac_locate = function
| LocateTerm qid -> msgnl (print_located_qualid qid)
| LocateLibrary qid -> print_located_library qid
+ | LocateModule qid -> print_located_module qid
| LocateFile f -> locate_file f
| LocateNotation ntn ->
- ppnl (Symbols.locate_notation (Constrextern.without_symbols pr_rawterm)
- (Metasyntax.standardise_locatable_notation ntn))
+ ppnl (Notation.locate_notation (Constrextern.without_symbols pr_lrawconstr)
+ (Metasyntax.standardize_locatable_notation ntn))
(********************)
(* Proof management *)
@@ -942,7 +954,7 @@ let vernac_goal = function
| Some c ->
if not (refining()) then begin
let unnamed_kind = Lemma (* Arbitrary *) in
- start_proof_com None (IsGlobal (Proof unnamed_kind)) c (fun _ _ ->());
+ start_proof_com None (Global, Proof unnamed_kind) c (fun _ _ ->());
print_subgoals ()
end else
error "repeated Goal not permitted in refining mode"
@@ -979,6 +991,17 @@ let vernac_undo n =
undo n;
print_subgoals ()
+(* backtrack with [naborts] abort, then undo_todepth to [pnum], then
+ back-to state number [snum]. This allows to backtrack proofs and
+ state with one command (easier for proofgeneral). *)
+let vernac_backtrack snum pnum naborts =
+ for i = 1 to naborts do vernac_abort None done;
+ undo_todepth pnum;
+ vernac_backto snum;
+ (* there may be no proof in progress, even if no abort *)
+ (try print_subgoals () with UserError _ -> ())
+
+
(* Est-ce normal que "Focus" ne semble pas se comporter comme "Focus 1" ? *)
let vernac_focus = function
| None -> traverse_nth_goal 1; print_subgoals ()
@@ -1005,10 +1028,10 @@ let apply_subproof f occ =
f evc (Global.named_context()) pf
let explain_proof occ =
- msg (apply_subproof (Refiner.print_treescript true) occ)
+ msg (apply_subproof (print_treescript true) occ)
let explain_tree occ =
- msg (apply_subproof Refiner.print_proof occ)
+ msg (apply_subproof print_proof occ)
let vernac_show = function
| ShowGoal nopt ->
@@ -1028,17 +1051,17 @@ let vernac_show = function
| ShowProofNames ->
msgnl (prlist_with_sep pr_spc pr_id (Pfedit.get_all_proof_names()))
| ShowIntros all -> show_intro all
+ | ShowMatch id -> show_match id
| ExplainProof occ -> explain_proof occ
| ExplainTree occ -> explain_tree occ
let vernac_check_guard () =
let pts = get_pftreestate () in
- let pf = proof_of_pftreestate pts
- and cursor = cursor_of_pftreestate pts in
+ let pf = proof_of_pftreestate pts in
let (pfterm,_) = extract_open_pftreestate pts in
let message =
try
- Inductiveops.control_only_guard (Evarutil.evar_env (goal_of_proof pf))
+ Inductiveops.control_only_guard (Evd.evar_env (goal_of_proof pf))
pfterm;
(str "The condition holds up to here")
with UserError(_,s) ->
@@ -1049,100 +1072,19 @@ let vernac_check_guard () =
let vernac_debug b =
set_debug (if b then Tactic_debug.DebugOn 0 else Tactic_debug.DebugOff)
-
-(**************************)
-(* Not supported commands *)
-(***
-let _ =
- add "ResetSection"
- (function
- | [VARG_IDENTIFIER id] ->
- (fun () -> reset_section (string_of_id id))
- | _ -> bad_vernac_args "ResetSection")
-
-(* Modules *)
-
-let _ =
- vinterp_add "BeginModule"
- (function
- | [VARG_IDENTIFIER id] ->
- let s = string_of_id id in
- let lpe,_ = System.find_file_in_path (Library.get_load_path ()) (s^".v") in
- let dir = extend_dirpath (Library.find_logical_path lpe) id in
- fun () ->
- Lib.start_module dir
- | _ -> bad_vernac_args "BeginModule")
-
-let _ =
- vinterp_add "WriteModule"
- (function
- | [VARG_IDENTIFIER id] ->
- let mid = Lib.end_module id in
- fun () -> let m = string_of_id id in Library.save_module_to mid m
- | [VARG_IDENTIFIER id; VARG_STRING f] ->
- let mid = Lib.end_module id in
- fun () -> Library.save_module_to mid f
- | _ -> bad_vernac_args "WriteModule")
-
-let _ =
- vinterp_add "CLASS"
- (function
- | [VARG_STRING kind; VARG_QUALID qid] ->
- let stre =
- if kind = "LOCAL" then
- make_strength_0()
- else
- Nametab.NeverDischarge
- in
- fun () ->
- let ref = Nametab.global (dummy_loc, qid) in
- Class.try_add_new_class ref stre;
- if_verbose message
- ((string_of_qualid qid) ^ " is now a class")
- | _ -> bad_vernac_args "CLASS")
-
-(* Meta-syntax commands *)
-let _ =
- add "TOKEN"
- (function
- | [VARG_STRING s] -> (fun () -> Metasyntax.add_token_obj s)
- | _ -> bad_vernac_args "TOKEN")
-***)
-
-(* Search commands *)
-
-(***
-let _ =
- add "Searchisos"
- (function
- | [VARG_CONSTR com] ->
- (fun () ->
- let env = Global.env() in
- let c = constr_of_com Evd.empty env com in
- let cc = nf_betaiota env Evd.empty c in
- Searchisos.type_search cc)
- | _ -> bad_vernac_args "Searchisos")
-***)
-
let interp c = match c with
(* Control (done in vernac) *)
| (VernacTime _ | VernacVar _ | VernacList _ | VernacLoad _) -> assert false
- | (VernacV7only _ | VernacV8only _) -> assert false
(* Syntax *)
- | VernacSyntax (whatfor,sel) -> vernac_syntax whatfor sel
- | VernacTacticGrammar al -> Metasyntax.add_tactic_grammar al
- | VernacGrammar (univ,al) -> vernac_grammar univ al
- | VernacSyntaxExtension (lcl,sl,l8) -> vernac_syntax_extension lcl sl l8
+ | VernacTacticNotation (n,r,e) -> Metasyntax.add_tactic_notation (n,r,e)
+ | VernacSyntaxExtension (lcl,sl) -> vernac_syntax_extension lcl sl
| VernacDelimiters (sc,lr) -> vernac_delimiters sc lr
| VernacBindScope (sc,rl) -> vernac_bind_scope sc rl
| VernacOpenCloseScope sc -> vernac_open_close_scope sc
| VernacArgumentsScope (qid,scl) -> vernac_arguments_scope qid scl
- | VernacInfix (local,mv,qid,mv8,sc) -> vernac_infix local mv qid mv8 sc
- | VernacDistfix (local,assoc,n,inf,qid,sc) ->
- vernac_distfix local assoc n inf qid sc
- | VernacNotation (local,c,infpl,mv8,sc) ->
- vernac_notation local c infpl mv8 sc
+ | VernacInfix (local,mv,qid,sc) -> vernac_infix local mv qid sc
+ | VernacNotation (local,c,infpl,sc) -> vernac_notation local c infpl sc
(* Gallina *)
| VernacDefinition (k,(_,id),d,f) -> vernac_definition k id d f
@@ -1152,15 +1094,15 @@ let interp c = match c with
| VernacExactProof c -> vernac_exact_proof c
| VernacAssumption (stre,l) -> vernac_assumption stre l
| VernacInductive (finite,l) -> vernac_inductive finite l
- | VernacFixpoint l -> vernac_fixpoint l
- | VernacCoFixpoint l -> vernac_cofixpoint l
+ | VernacFixpoint (l,b) -> vernac_fixpoint l b
+ | VernacCoFixpoint (l,b) -> vernac_cofixpoint l b
| VernacScheme l -> vernac_scheme l
(* Modules *)
- | VernacDeclareModule ((_,id),bl,mtyo,mexpro) ->
- vernac_declare_module id bl mtyo mexpro
- | VernacDefineModule ((_,id),bl,mtyo,mexpro) ->
- vernac_define_module id bl mtyo mexpro
+ | VernacDeclareModule (export,(_,id),bl,mtyo) ->
+ vernac_declare_module export id bl mtyo
+ | VernacDefineModule (export,(_,id),bl,mtyo,mexpro) ->
+ vernac_define_module export id bl mtyo mexpro
| VernacDeclareModuleType ((_,id),bl,mtyo) ->
vernac_declare_module_type id bl mtyo
@@ -1196,6 +1138,7 @@ let interp c = match c with
| VernacResetName id -> vernac_reset_name id
| VernacResetInitial -> vernac_reset_initial ()
| VernacBack n -> vernac_back n
+ | VernacBackTo n -> vernac_backto n
(* Commands *)
| VernacDeclareTacticDefinition (x,l) -> vernac_declare_tactic_definition x l
@@ -1226,6 +1169,7 @@ let interp c = match c with
| VernacSuspend -> vernac_suspend ()
| VernacResume id -> vernac_resume id
| VernacUndo n -> vernac_undo n
+ | VernacBacktrack (snum,pnum,naborts) -> vernac_backtrack snum pnum naborts
| VernacFocus n -> vernac_focus n
| VernacUnfocus -> vernac_unfocus ()
| VernacGo g -> vernac_go g