diff options
Diffstat (limited to 'toplevel/vernacentries.ml')
| -rw-r--r-- | toplevel/vernacentries.ml | 586 |
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 |