diff options
Diffstat (limited to 'toplevel/vernacentries.ml')
| -rw-r--r-- | toplevel/vernacentries.ml | 2449 |
1 files changed, 766 insertions, 1683 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index a72302458..8d8de77b9 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -10,78 +10,59 @@ (* Concrete syntax of the mathematical vernacular MV V2.6 *) -open Declarations open Pp open Util open Options -open System open Names open Nameops open Term open Pfedit open Tacmach open Proof_trees -open Proof_type -open Evar_refiner -open Tacred -open Environ -open Vernacinterp -open Coqast -open Ast open Astterm open Prettyp open Printer open Tacinterp -open Tactic_debug open Command open Goptions -open Declare open Nametab -open Safe_typing +open Vernacexpr -(* Dans join_binders, s'il y a un "?", on perd l'info qu'il est partagé *) -let join_binders binders = - List.flatten - (List.map (fun (idl,c) -> List.map (fun id -> (id,c)) idl) binders) +(* Pcoq hooks *) -let add = vinterp_add +type pcoq_hook = { + start_proof : unit -> unit; + solve : int -> unit; + abort : string -> unit; + search : searchable -> dir_path list * bool -> unit; + print_name : qualid 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 +} -(* equivalent to pr_subgoals but start from the prooftree and - check for uninstantiated existential variables *) +let pcoq = ref None +let set_pcoq_hook f = pcoq := Some f + +(*******************) +(* "Show" commands *) + + (* equivalent to pr_subgoals but start from the prooftree and + check for uninstantiated existential variables *) let pr_subgoals_of_pfts pfts = - let gls = fst (frontier (proof_of_pftreestate pfts)) in + let gls = fst (Refiner.frontier (proof_of_pftreestate pfts)) in let sigma = project (top_goal_of_pftreestate pfts) in pr_subgoals_existential sigma gls -let show_script () = - let pts = get_pftreestate () in - let pf = proof_of_pftreestate pts - and evc = evc_of_pftreestate pts in - msgnl(Refiner.print_script true evc (Global.named_context()) pf) - -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) - let show_open_subgoals () = let pfts = get_pftreestate () in - msg(pr_subgoals_of_pfts pfts) - -let show_nth_open_subgoal n = - let pf = proof_of_pftreestate (get_pftreestate ()) in - msg(pr_subgoal n (fst(frontier pf))) - -let show_open_subgoals_focused () = - let pfts = get_pftreestate () in match focus() with | 0 -> msg(pr_subgoals_of_pfts pfts) | n -> let pf = proof_of_pftreestate pfts in - let gls = fst(frontier pf) in + let gls = fst(Refiner.frontier pf) in if n > List.length gls then (make_focus 0; msg(pr_subgoals_of_pfts pfts)) else if List.length gls < 2 then @@ -90,26 +71,119 @@ let show_open_subgoals_focused () = msg (v 0 (int(List.length gls) ++ str" subgoals" ++ cut () ++ pr_subgoal n gls)) +let show_nth_open_subgoal n = + let pf = proof_of_pftreestate (get_pftreestate ()) in + msg(pr_subgoal n (fst(Refiner.frontier pf))) + +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 + msgnl (str"LOC: " ++ + prlist_with_sep pr_spc pr_int (List.rev cursor) ++ fnl () ++ + str"Subgoals" ++ fnl () ++ + prlist (fun (mv,ty) -> int mv ++ str" -> " ++ prtype ty ++ fnl ()) + meta_types + ++ str"Proof: " ++ prterm (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 msg (prlist_with_sep pr_spc pr_int (List.rev cursor) ++ fnl () ++ - prgl pf.goal ++ fnl () ++ - (match pf.ref with + prgl (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" " ++ + (str"BY " ++ Refiner.pr_rule r ++ fnl () ++ + str" " ++ hov 0 (prlist_with_sep pr_fnl prgl - (List.map (fun p -> p.goal) spfl)))) ++ + (List.map goal_of_proof spfl)))) ++ fnl ()) +let show_script () = + let pts = get_pftreestate () in + let pf = proof_of_pftreestate pts + and evc = evc_of_pftreestate pts in + msgnl(Refiner.print_script 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)) +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) + +let print_subgoals () = if_verbose show_open_subgoals () + + (* Simulate the Intro(s) tactic *) + +let fresh_id_of_name avoid gl = function + Anonymous -> Tactics.fresh_id avoid (id_of_string "H") gl + | Name id -> id + +let rec do_renum avoid gl = function + [] -> mt () + | [n] -> pr_id (fresh_id_of_name avoid gl n) + | n :: l -> + let id = fresh_id_of_name avoid gl n in + pr_id id ++ spc () ++ do_renum (id :: avoid) gl l + +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 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 "" + +(********************) +(* "Print" commands *) + +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 print_modules () = + let opened = Library.opened_modules () + and loaded = Library.loaded_modules () in + let loaded_opened = list_intersect loaded opened + and only_loaded = list_subtract loaded opened in + str"Loaded and imported modules: " ++ + pr_vertical_list pr_dirpath loaded_opened ++ fnl () ++ + str"Loaded and not imported modules: " ++ + pr_vertical_list pr_dirpath only_loaded + +let dump_universes s = + let output = open_out s in + try + Univ.dump_universes output (Global.universes ()); + close_out output; + msg (str ("Universes written to file \""^s^"\".") ++ fnl ()) + with + e -> close_out output; raise e + + +(*********************) +(* "Locate" commands *) + let locate_file f = try let _,file = @@ -119,7 +193,7 @@ let locate_file f = msg (hov 0 (str"Can't find file" ++ spc () ++ str f ++ spc () ++ str"on loadpath" ++ fnl ())) -let print_located_qualid qid = +let print_located_qualid (_,qid) = try let sp = Nametab.sp_of_global (Global.env()) (Nametab.locate qid) in msg (pr_sp sp ++ fnl ()) @@ -127,33 +201,7 @@ let print_located_qualid qid = try msg (pr_sp (Syntax_def.locate_syntactic_definition qid) ++ fnl ()) with Not_found -> - error ((Nametab.string_of_qualid qid) ^ " 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 get_current_context_of_args = function - | [VARG_NUMBER n] -> get_goal_context n - | [] -> get_current_context () - | _ -> bad_vernac_args "goal_of_args" - -let isfinite = function - | "Inductive" -> true - | "CoInductive" -> false - | _ -> anomaly "Unexpected string" - -(* Locate commands *) -let _ = - add "LocateFile" - (function - | [VARG_STRING f] -> (fun () -> locate_file f) - | _ -> bad_vernac_args "LocateFile") + msg (pr_qualid qid ++ str " is not a defined object") let msg_found_library = function | Library.LibLoaded, fulldir, file -> @@ -161,12 +209,11 @@ let msg_found_library = function str file ++ fnl ()) | Library.LibInPath, fulldir, file -> msg (pr_dirpath fulldir ++ str " is bound to file " ++ str file ++ fnl ()) - -let msg_notfound_library qid = function +let msg_notfound_library loc qid = function | Library.LibUnmappedDir -> let dir = fst (Nametab.repr_qualid qid) in - errorlabstrm "locate_library" - (str "Cannot find a physical path bound to logical path " ++ + user_err_loc (loc,"locate_library", + str "Cannot find a physical path bound to logical path " ++ pr_dirpath dir ++ fnl ()) | Library.LibNotFound -> msg (hov 0 @@ -174,144 +221,566 @@ let msg_notfound_library qid = function spc () ++ Nametab.pr_qualid qid ++ fnl ())) | e -> assert false -let _ = - add "LocateLibrary" - (function - | [VARG_QUALID qid] -> - (fun () -> - try msg_found_library (Library.locate_qualified_library qid) - with e -> msg_notfound_library qid e) - | _ -> bad_vernac_args "LocateLibrary") - -let _ = - add "Locate" - (function - | [VARG_QUALID qid] -> (fun () -> print_located_qualid qid) - | _ -> bad_vernac_args "Locate") - -(* For compatibility *) -let _ = - add "ADDPATH" - (function - | [VARG_STRING dir] -> - (fun () -> Mltop.add_path dir Nameops.default_root_prefix) - | [VARG_STRING dir ; VARG_QUALID alias] -> - let aliasdir,aliasname = Nametab.repr_qualid alias in - (fun () -> Mltop.add_path dir (extend_dirpath aliasdir aliasname)) - | _ -> bad_vernac_args "ADDPATH") - -(* For compatibility *) -let _ = - add "DELPATH" - (function - | [VARG_STRING dir] -> (fun () -> Library.remove_path dir) - | _ -> bad_vernac_args "DELPATH") - -let _ = - add "RECADDPATH" - (function - | [VARG_STRING dir] -> - (fun () -> Mltop.add_rec_path dir Nameops.default_root_prefix) - | [VARG_STRING dir ; VARG_QUALID alias] -> - let aliasdir,aliasname = Nametab.repr_qualid alias in - (fun () ->Mltop.add_rec_path dir (extend_dirpath aliasdir aliasname)) - | _ -> bad_vernac_args "RECADDPATH") - -(* For compatibility *) -let _ = - add "PrintPath" - (function - | [] -> (fun () -> print_loadpath ()) - | _ -> bad_vernac_args "PrintPath") +let print_located_library (loc,qid) = + try msg_found_library (Library.locate_qualified_library qid) + with e -> msg_notfound_library loc qid e -let _ = - add "PWD" - (function - | [] -> (fun () -> print_endline (Sys.getcwd())) - | _ -> bad_vernac_args "PWD") -let _ = - add "DROP" - (function - | [] -> (fun () -> raise Drop) - | _ -> bad_vernac_args "DROP") +(**********) +(* Syntax *) -let _ = - add "PROTECTEDLOOP" - (function - | [] -> (fun () -> raise ProtectedLoop) - | _ -> bad_vernac_args "PROTECTEDLOOP") +let vernac_syntax = Metasyntax.add_syntax_obj -let _ = - add "QUIT" - (function - | [] -> (fun () -> raise Quit) - | _ -> anomaly "To fill the empty holes...") +let vernac_grammar = Metasyntax.add_grammar_obj -let _ = - add "CD" - (function - | [VARG_STRING s] -> - (fun () -> - begin - try Sys.chdir (glob s) - with Sys_error str -> warning ("Cd failed: " ^ str) - end; - if_verbose print_endline (Sys.getcwd())) - | [] -> (fun () -> if_verbose print_endline (Sys.getcwd())) - | _ -> bad_vernac_args "CD") - -(* Managing states *) +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 +(* + if dir <> [] then begin + let modname = List.hd dir in + let long_inf = (string_of_id modname) ^ "." ^ inf in + Metasyntax.add_infix assoc n long_inf qid + end; +*) + Metasyntax.add_infix assoc n inf qid + +let vernac_distfix assoc n inf qid = + Metasyntax.add_distfix assoc n inf (Astterm.globalize_qualid qid) + + +(***********) +(* Gallina *) + +let interp_assumption = function + | (AssumptionHypothesis | AssumptionVariable) -> Declare.make_strength_0 () + | (AssumptionAxiom | AssumptionParameter) -> Nametab.NeverDischarge + +let interp_definition = function + | Definition -> (false, Nametab.NeverDischarge) + | LocalDefinition -> (true, Declare.make_strength_0 ()) + +let interp_theorem = function + | (Theorem | Lemma | Decl) -> Nametab.NeverDischarge + | Fact -> Declare.make_strength_1 () + | Remark -> Declare.make_strength_0 () + +let interp_goal = function + | StartTheoremProof x -> (false, interp_theorem x) + | StartDefinitionBody x -> interp_definition x + +let vernac_definition kind id red_option c typ_opt hook = + 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 + let (local,stre as x) = interp_definition kind in + let ref = declare_definition red_option id x c typ_opt in + hook stre ref + +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_com sopt (interp_goal kind) t hook; + print_subgoals (); + if !pcoq <> None then (out_some !pcoq).start_proof () + +let vernac_end_proof is_opaque idopt = + if_verbose show_script (); + match idopt with + | None -> save_named is_opaque + | Some (id,None) -> save_anonymous is_opaque id + | Some (id,Some kind) -> + save_anonymous_with_strength (interp_theorem kind) is_opaque id + + (* A stupid macro that should be replaced by ``Exact c. Save.'' all along + the theories [??] *) + +let vernac_exact_proof c = + by (Tactics.exact_proof c); + save_named true + +let vernac_assumption kind l = + let stre = interp_assumption kind in + List.iter (fun (id,c) -> declare_assumption id stre c) l + +let vernac_inductive f indl = build_mutual indl f + +let vernac_fixpoint = build_recursive + +let vernac_cofixpoint = build_corecursive + +let vernac_scheme = build_scheme + + +(**********************) +(* Gallina extensions *) + +let vernac_record iscoe struc binders sort nameopt cfs = + let const = match nameopt with + | None -> add_prefix "Build_" struc + | Some id -> id in + let s = Astterm.interp_sort sort in + Record.definition_structure (iscoe,struc,binders,cfs,const,s) + + (* Sections *) + +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 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" ) + -> true + | _ -> false) + | _ -> false + +let vernac_require import _ qidl = + try + match import with + | None -> List.iter Library.read_module qidl + | Some b -> Library.require_module 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 + raise e + +let vernac_import export qidl = + List.iter (Library.import_module export) qidl + +let vernac_canonical locqid = + Recordobj.objdef_declare (Nametab.global locqid) + +let cl_of_qualid = function + | FunClass -> Classops.CL_FUN + | SortClass -> Classops.CL_SORT + | RefClass (loc,qid) -> Class.class_of_ref (Nametab.global (loc, qid)) + +let vernac_coercion stre (loc,qid as locqid) qids qidt = + let target = cl_of_qualid qidt in + 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") + +let vernac_identity_coercion stre id qids qidt = + let target = cl_of_qualid qidt in + let source = cl_of_qualid qids in + Class.try_add_new_identity_coercion id stre source target + + +(***********) +(* Solving *) + +let vernac_solve n tcom = + if not (refining ()) then + error "Unknown command of the non proof-editing mode"; + solve_nth n (Tacinterp.hide_interp tcom); + print_subgoals(); + (* in case a strict subtree was completed, + go back to the top of the prooftree *) + if subtree_solved () then + (reset_top_of_tree (); print_subgoals()); + if !pcoq <> None then (out_some !pcoq).solve n + + (* A command which should be a tactic. It has been + added by Christine to patch an error in the design of the proof + machine, and enables to instantiate existential variables when + there are no more goals to solve. It cannot be a tactic since + all tactics fail if there are no further goals to prove. *) + +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 + +let vernac_add_loadpath isrec pdir ldiropt = + let alias = match ldiropt with + | None -> Nameops.default_root_prefix + | Some ldir -> ldir in + (if isrec then Mltop.add_rec_path else Mltop.add_path) pdir alias + +let vernac_remove_loadpath = Library.remove_path + + (* Coq syntax for ML or system commands *) + +let vernac_add_ml_path isrec s = + (if isrec then Mltop.add_rec_ml_dir else Mltop.add_ml_dir) (System.glob s) + +let vernac_declare_ml_module l = Mltop.declare_ml_modules l + +let vernac_chdir = function + | None -> print_endline (Sys.getcwd()) + | Some s -> + begin + try Sys.chdir (System.glob s) + with Sys_error str -> warning ("Cd failed: " ^ str) + end; + if_verbose print_endline (Sys.getcwd()) + + +(********************) +(* State management *) let abort_refine f x = if Pfedit.refining() then delete_all_proofs (); f x (* used to be: error "Must save or abort current goal first" *) -let _ = - add "WriteState" - (function - | [VARG_STRING file] -> - (fun () -> abort_refine States.extern_state file) - | [VARG_IDENTIFIER id] -> - let file = string_of_id id in - (fun () -> abort_refine States.extern_state file) - | _ -> bad_vernac_args "SaveState") +let vernac_write_state file = abort_refine States.extern_state file -let _ = - add "RestoreState" - (function - | [VARG_STRING file] -> - (fun () -> abort_refine States.intern_state file) - | [VARG_IDENTIFIER id] -> - let file = string_of_id id in - (fun () -> abort_refine States.intern_state file) - | _ -> bad_vernac_args "LoadState") +let vernac_restore_state file = abort_refine States.intern_state file + +(*************) (* Resetting *) -let _ = - add "ResetName" - (function - | [VARG_IDENTIFIER id] -> - (fun () -> abort_refine Lib.reset_name id) - | _ -> bad_vernac_args "ResetName") +let vernac_reset_name id = abort_refine Lib.reset_name id -let _ = - add "ResetInitial" - (function - | [] -> (fun () -> abort_refine Lib.reset_initial ()) - | _ -> bad_vernac_args "ResetInitial") +let vernac_reset_initial () = abort_refine Lib.reset_initial () -let _ = - add "Back" - (function - | [] -> (fun () -> Lib.back 1) - | [VARG_NUMBER n] -> - if n < 1 then error "argument of Back must be positive" - else (fun () -> Lib.back n) - | _ -> bad_vernac_args "Back") +let vernac_back n = Lib.back n + + +(************) +(* Commands *) +let vernac_declare_tactic_definition _ l = Tacinterp.add_tacdef l + +let vernac_hints = Auto.add_hints + +let vernac_syntactic_definition id c = function + | None -> syntax_definition id c + | Some n -> + let l = list_tabulate (fun _ -> Ast.ope("ISEVAR",[])) n in + let c = Ast.ope ("APPLIST",c :: l) in + syntax_definition id c + +let vernac_declare_implicits locqid = function + | Some imps -> Impargs.declare_manual_implicits (Nametab.global locqid) imps + | None -> Impargs.declare_implicits (Nametab.global locqid) + +let make_silent_if_not_pcoq b = + if !pcoq <> None then + error "Turning on/off silent flag is not supported in Centaur mode" + else make_silent b + +let _ = + declare_bool_option + { optsync = false; + optname = "silent"; + optkey = (PrimaryTable "Silent"); + optread = is_silent; + optwrite = make_silent_if_not_pcoq } + +let _ = + declare_bool_option + { optsync = true; + optname = "implicit arguments"; + optkey = (SecondaryTable ("Implicit","Arguments")); + optread = Impargs.is_implicit_args; + optwrite = Impargs.make_implicit_args } + +let _ = + declare_bool_option + { optsync = true; + optname = "coercion printing"; + optkey = (SecondaryTable ("Printing","Coercions")); + optread = (fun () -> !Termast.print_coercions); + optwrite = (fun b -> Termast.print_coercions := b) } + +let _ = + declare_int_option + { optsync=false; + optkey=PrimaryTable("Undo"); + optname="the undo limit"; + optread=Pfedit.get_undo; + optwrite=Pfedit.set_undo } + +let _ = + declare_int_option + { optsync=false; + optkey=SecondaryTable("Hyps","Limit"); + optname="the hypotheses limit"; + optread=Options.print_hyps_limit; + optwrite=Options.set_print_hyps_limit } + +let _ = + declare_int_option + { optsync=true; + optkey=SecondaryTable("Printing","Depth"); + optname="the printing depth"; + optread=Pp_control.get_depth_boxes; + optwrite=Pp_control.set_depth_boxes } + +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 + | VarRef id -> + if opaq then Tacred.set_opaque_var id + else Tacred.set_transparent_var id + | _ -> error "cannot set an inductive type or a constructor as transparent" + +let vernac_set_option key = function + | StringValue s -> set_string_option_value key s + | IntValue n -> set_int_option_value key (Some n) + | BoolValue b -> set_bool_option_value key b + +let vernac_unset_option key = + try set_bool_option_value key false + with _ -> + set_int_option_value key None + +let vernac_add_option key lv = + let f = function + | StringRefValue s -> (get_string_table key)#add s + | QualidRefValue locqid -> (get_ref_table key)#add locqid + in + try List.iter f lv with Not_found -> error_undeclared_key key + +let vernac_remove_option key lv = + let f = function + | StringRefValue s -> (get_string_table key)#remove s + | QualidRefValue locqid -> (get_ref_table key)#remove locqid + in + try List.iter f lv with Not_found -> error_undeclared_key key + +let vernac_mem_option key lv = + let f = function + | StringRefValue s -> (get_string_table key)#mem s + | QualidRefValue locqid -> (get_ref_table key)#mem locqid + in + try List.iter f lv with Not_found -> error_undeclared_key key + +let vernac_print_option key = + try (get_ref_table key)#print + with not_found -> + try (get_string_table key)#print + with not_found -> + try print_option_value key + with Not_found -> error_undeclared_key key + +let get_current_context_of_args = function + | Some n -> get_goal_context n + | None -> get_current_context () + +let vernac_check_may_eval redexp glopt rc = + let (evmap,env) = get_current_context_of_args glopt in + let c = interp_constr evmap env rc in + let j = Typeops.typing env c in + match redexp with + | None -> + 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 + if !pcoq <> None + then (out_some !pcoq).print_eval (redfun env evmap) env rc j + else msg (print_eval redfun env j) + + (* The same but avoiding the current goal context if any *) +let vernac_global_check c = + let evmap = Evd.empty in + let env = Global.env() in + let c = interp_constr evmap env c in + let senv = Global.safe_env() in + let j = Safe_typing.typing senv c in + msg (print_safe_judgment env j) + +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) + | PrintGrammar (uni,ent) -> Metasyntax.print_grammar uni ent + | PrintLoadPath -> (* For compatibility ? *) print_loadpath () + | PrintModules -> msg (print_modules ()) + | PrintMLLoadPath -> Mltop.print_ml_path () + | PrintMLModules -> Mltop.print_ml_modules () + | PrintName qid -> + if !pcoq <> None then (out_some !pcoq).print_name qid + else msg (print_name qid) + | PrintOpaqueName qid -> msg (print_opaque_name qid) + | PrintGraph -> ppnl (Prettyp.print_graph()) + | PrintClasses -> ppnl (Prettyp.print_classes()) + | PrintCoercions -> ppnl (Prettyp.print_coercions()) + | PrintCoercionPaths (cls,clt) -> + ppnl (Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt)) + | 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 + | PrintHintDb -> Auto.print_searchtable () + + +let global_loaded_library (loc, qid) = + try Nametab.locate_loaded_library qid + with Not_found -> + user_err_loc (loc, "global_loaded_library", + str "Module/section " ++ pr_qualid qid ++ str " not found") + +let interp_search_restriction = function + | SearchOutside l -> (List.map global_loaded_library l, true) + | SearchInside l -> (List.map global_loaded_library l, false) + +let vernac_search s r = + let r = interp_search_restriction r in + if !pcoq <> None then (out_some !pcoq).search s r else + match s with + | SearchPattern c -> + let _,pat = interp_constrpattern Evd.empty (Global.env()) c in + Search.search_pattern pat r + | SearchRewrite c -> + let _,pat = interp_constrpattern Evd.empty (Global.env()) c in + Search.search_rewrite pat r + | SearchHead locqid -> + Search.search_by_head (Nametab.global locqid) r + +let vernac_locate = function + | LocateTerm qid -> print_located_qualid qid + | LocateLibrary qid -> print_located_library qid + | LocateFile f -> locate_file f + + +(********************) +(* Proof management *) + +let vernac_goal = function + | None -> () + | Some c -> + if not (refining()) then begin + start_proof_com None (false,Nametab.NeverDischarge) c (fun _ _ ->()); + print_subgoals () + end else + error "repeated Goal not permitted in refining mode" + +let vernac_abort = function + | None -> + delete_current_proof (); + if_verbose message "Current goal aborted"; + if !pcoq <> None then (out_some !pcoq).abort "" + | Some id -> + delete_proof id; + let s = string_of_id id in + if_verbose message ("Goal "^s^" aborted"); + if !pcoq <> None then (out_some !pcoq).abort s + +let vernac_abort_all () = + if refining() then begin + delete_all_proofs (); + message "Current goals aborted" + end else + error "No proof-editing in progress" + +let vernac_restart () = restart_proof(); show_open_subgoals () + + (* Proof switching *) + +let vernac_suspend = suspend_proof + +let vernac_resume = function + | None -> resume_last_proof () + | Some id -> resume_proof id + +let vernac_undo n = + undo n; + show_open_subgoals () + + (* Est-ce normal que "Focus" ne semble pas se comporter comme "Focus 1" ? *) +let vernac_focus = function + | None -> make_focus 1; show_open_subgoals () + | Some n -> traverse_nth_goal n; show_open_subgoals () + + (* Reset the focus to the top of the tree *) +let vernac_unfocus () = + make_focus 0; reset_top_of_tree (); show_open_subgoals () + +let vernac_go = function + | GoTo n -> Pfedit.traverse n;show_node() + | GoTop -> Pfedit.reset_top_of_tree ();show_node() + | GoNext -> Pfedit.traverse_next_unproven ();show_node() + | GoPrev -> Pfedit.traverse_prev_unproven ();show_node() + +let apply_subproof f occ = + let pts = get_pftreestate() in + let evc = evc_of_pftreestate pts in + let rec aux pts = function + | [] -> pts + | (n::l) -> aux (Tacmach.traverse n pts) occ in + let pts = aux pts (occ@[-1]) in + let pf = proof_of_pftreestate pts in + f evc (Global.named_context()) pf + +let explain_proof occ = msg (apply_subproof (Refiner.print_script true) occ) + +let explain_tree occ = msg (apply_subproof Refiner.print_proof occ) + +let vernac_show = function + | ShowGoal nopt -> + if !pcoq <> None then (out_some !pcoq).show_goal nopt + else (match nopt with + | None -> show_open_subgoals () + | (Some n) -> show_nth_open_subgoal n) + | ShowGoalImplicitly None -> Impargs.implicitly show_open_subgoals () + | ShowGoalImplicitly (Some n) -> Impargs.implicitly show_nth_open_subgoal n + | ShowProof -> show_proof () + | ShowNode -> show_node () + | ShowScript -> show_script () + | ShowExistentials -> show_top_evars () + | ShowTree -> show_prooftree () + | ShowProofNames -> + msgnl (prlist_with_sep pr_spc pr_id (Pfedit.get_all_proof_names())) + | ShowIntros all -> show_intro all + | 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 (pfterm,_) = extract_open_pftreestate pts in + let message = + try + Inductiveops.control_only_guard (Evarutil.evar_env (goal_of_proof pf)) + pfterm; + (str "The condition holds up to here") + with UserError(_,s) -> + (str ("Condition violated : ") ++s) + in + msgnl message + +let vernac_debug b = + set_debug (if b then Tactic_debug.DebugOn else Tactic_debug.DebugOff) + + +(**************************) +(* Not supported commands *) (*** let _ = add "ResetSection" @@ -320,12 +789,10 @@ let _ = (fun () -> reset_section (string_of_id id)) | _ -> bad_vernac_args "ResetSection") -***) - (* Modules *) let _ = - add "BeginModule" + vinterp_add "BeginModule" (function | [VARG_IDENTIFIER id] -> let s = string_of_id id in @@ -336,7 +803,7 @@ let _ = | _ -> bad_vernac_args "BeginModule") let _ = - add "WriteModule" + vinterp_add "WriteModule" (function | [VARG_IDENTIFIER id] -> let mid = Lib.end_module id in @@ -347,1103 +814,29 @@ let _ = | _ -> bad_vernac_args "WriteModule") let _ = - add "ReadModule" - (function l -> - let l = - List.map - (function - | VARG_QUALID qid -> qid - | _ -> bad_vernac_args "ReadModule") l in - fun () -> List.iter Library.read_module l) - -let _ = - add "ImportModule" - (function l -> - let l = - List.map - (function - | VARG_QUALID qid -> qid - | _ -> bad_vernac_args "ImportModule") l in - fun () -> List.iter (Library.import_module false) l) - -let _ = - add "ExportModule" - (function l -> - let l = - List.map - (function - | VARG_QUALID qid -> qid - | _ -> bad_vernac_args "ExportModule") l in - fun () -> List.iter (Library.import_module true) l) - -let _ = - add "PrintModules" - (function - | [] -> - (fun () -> - let opened = Library.opened_modules () - and loaded = Library.loaded_modules () in - let loaded_opened = list_intersect loaded opened - and only_loaded = list_subtract loaded opened in - msg (str"Loaded and imported modules: " ++ - pr_vertical_list pr_dirpath loaded_opened ++ fnl () ++ - str"Loaded and not imported modules: " ++ - pr_vertical_list pr_dirpath only_loaded)) - | _ -> bad_vernac_args "PrintModules") - -(* Sections *) - -let _ = - add "BeginSection" - (function - | [VARG_IDENTIFIER id] -> - (fun () -> let _ = Lib.open_section id in ()) - | _ -> bad_vernac_args "BeginSection") - -let _ = - add "EndSection" - (function - | [VARG_IDENTIFIER id] -> - (fun () -> - check_no_pending_proofs (); - Discharge.close_section (is_verbose ()) id) - | _ -> bad_vernac_args "EndSection") - -(* Proof switching *) - -let _ = - add "GOAL" - (function - | [VARG_CONSTR com] -> - (fun () -> - if not (refining()) then begin - start_proof_com None Declare.NeverDischarge com; - if_verbose show_open_subgoals () - end else - error "repeated Goal not permitted in refining mode") - | [] -> (fun () -> ()) - | _ -> bad_vernac_args "GOAL") - -let _ = add "Comments" (function _ -> (fun () -> ())) - -let _ = - add "ABORT" - (function - | [VARG_IDENTIFIER id] -> - (fun () -> - delete_proof id; - message ("Goal "^(string_of_id id)^" aborted")) - | [] -> (fun () -> - delete_current_proof (); - message "Current goal aborted") - | _ -> bad_vernac_args "ABORT") - -let _ = - add "ABORTALL" - (function - | [] -> (fun () -> - if refining() then begin - delete_all_proofs (); - message "Current goals aborted" - end else - error "No proof-editing in progress") - - | _ -> bad_vernac_args "ABORTALL") - -let _ = - add "RESTART" - (function - | [] -> (fun () -> (restart_proof();show_open_subgoals ())) - | _ -> bad_vernac_args "RESTART") - -let _ = - add "SUSPEND" - (function - | [] -> (fun () -> suspend_proof ()) - | _ -> bad_vernac_args "SUSPEND") - -let _ = - add "RESUME" - (function - | [VARG_IDENTIFIER id] -> - (fun () -> resume_proof id) - | [] -> (fun () -> resume_last_proof ()) - | _ -> bad_vernac_args "RESUME") - -let _ = - add "FOCUS" - (function - | [] -> - (fun () -> make_focus 1; show_open_subgoals_focused ()) - | [VARG_NUMBER n] -> - (fun () -> traverse_nth_goal n; show_open_subgoals_focused ()) - | _ -> bad_vernac_args "FOCUS") - -(* Reset the focus to the top of the tree *) - -let _ = - add "UNFOCUS" - (function - | [] -> - (fun () -> - make_focus 0; reset_top_of_tree (); show_open_subgoals ()) - | _ -> bad_vernac_args "UNFOCUS") - -let _ = declare_bool_option - {optsync = true; - optname = "implicit arguments"; - optkey = (SecondaryTable ("Implicit","Arguments")); - optread = Impargs.is_implicit_args; - optwrite = Impargs.make_implicit_args } - -let _ = - add "IMPLICIT_ARGS_ON" - (function - | [] -> (fun () -> set_bool_option_value - (SecondaryTable ("Implicit","Arguments")) true) - | _ -> bad_vernac_args "IMPLICIT_ARGS_ON") - -let _ = - add "IMPLICIT_ARGS_OFF" - (function - | [] -> (fun () -> set_bool_option_value - (SecondaryTable ("Implicit","Arguments")) false) - | _ -> bad_vernac_args "IMPLICIT_ARGS_OFF") - -let _ = - add "TEST_IMPLICIT_ARGS" - (function - | [] -> - (fun () -> - if Impargs.is_implicit_args () then - message "Implicit arguments mode is set" - else - message "Implicit arguments mode is unset") - | _ -> bad_vernac_args "IMPLICIT_ARGS_OFF") - -let coercion_of_qualid loc qid = - let ref = Nametab.global loc qid in - let coe = Classops.coe_of_reference ref in - if not (Classops.coercion_exists coe) then - errorlabstrm "try_add_coercion" - (Printer.pr_global ref ++ str" is not a coercion"); - coe - -let _ = declare_bool_option - {optsync = true; - optname = "coercion printing"; - optkey = (SecondaryTable ("Printing","Coercions")); - optread = (fun () -> !Termast.print_coercions); - optwrite = (fun b -> Termast.print_coercions := b) } - -let number_list = - List.map (function VARG_NUMBER n -> n | _ -> bad_vernac_args "Number list") - -let _ = - add "IMPLICITS" - (function - | (VARG_STRING "") :: (VARG_QUALID qid) :: l -> - (fun () -> - let imps = number_list l in - Impargs.declare_manual_implicits - (Nametab.global dummy_loc qid) imps) - | [VARG_STRING "Auto"; VARG_QUALID qid] -> - (fun () -> - Impargs.declare_implicits (Nametab.global dummy_loc qid)) - | _ -> bad_vernac_args "IMPLICITS") - -let interp_definition_kind = function - | "THEOREM" -> (NeverDischarge, true) - | "LEMMA" -> (NeverDischarge, true) - | "FACT" -> (make_strength_1 (), true) - | "REMARK" -> (make_strength_0 (), true) - | "DEFINITION" -> (NeverDischarge, false) - | "LET" -> (make_strength_1 (), false) - | "LETTOP" -> (NeverDischarge, false) - | "LOCAL" -> (make_strength_0 (), false) - | _ -> anomaly "Unexpected definition kind" - -let _ = - add "SaveNamed" - (function - | [] -> - (fun () -> if_verbose show_script (); save_named true) - | _ -> bad_vernac_args "SaveNamed") - -let _ = - add "DefinedNamed" - (function - | [] -> - (fun () -> if_verbose show_script (); save_named false) - | _ -> bad_vernac_args "DefinedNamed") - -let _ = - add "DefinedAnonymous" - (function - | [VARG_IDENTIFIER id] -> - (fun () -> - if_verbose show_script (); - save_anonymous false id) - | _ -> bad_vernac_args "DefinedAnonymous") - -let _ = - add "SaveAnonymous" - (function - | [VARG_STRING kind; VARG_IDENTIFIER id] -> - (fun () -> - let (strength, opacity) = interp_definition_kind kind in - if_verbose show_script (); - save_anonymous_with_strength strength opacity id) - | [VARG_IDENTIFIER id] -> - (fun () -> - if_verbose show_script (); - save_anonymous true id) - | _ -> bad_vernac_args "SaveAnonymous") - -let _ = - add "TRANSPARENT" - (fun id_list () -> - List.iter - (function - | VARG_QUALID qid -> - (match Nametab.global dummy_loc qid with - | ConstRef sp -> Tacred.set_transparent_const sp - | VarRef id -> Tacred.set_transparent_var id - | _ -> error - "cannot set an inductive type or a constructor as transparent") - | _ -> bad_vernac_args "TRANSPARENT") - id_list) - -let _ = - add "OPAQUE" - (fun id_list () -> - List.iter - (function - | VARG_QUALID qid -> - (match Nametab.global dummy_loc qid with - | ConstRef sp -> Tacred.set_opaque_const sp - | VarRef id -> Tacred.set_opaque_var id - | _ -> error - "cannot set an inductive type or a constructor as opaque") - | _ -> bad_vernac_args "OPAQUE") - id_list) - -let _ = - add "UNDO" - (function - | [VARG_NUMBER n] -> - (fun () -> (undo n;show_open_subgoals_focused())) - | _ -> bad_vernac_args "UNDO") - -let _ = - add "SHOW" - (function - | [] -> (fun () -> show_open_subgoals ()) - | [VARG_NUMBER n] -> (fun () -> show_nth_open_subgoal n) - | _ -> bad_vernac_args "SHOW") - -let _ = - add "SHOWIMPL" - (function - | [] -> (fun () -> Impargs.implicitely show_open_subgoals ()) - | [VARG_NUMBER n] -> - (fun () -> Impargs.implicitely show_nth_open_subgoal n) - | _ -> bad_vernac_args "SHOWIMPL") - -let _ = - add "ShowNode" - (function - | [] -> (fun () -> show_node()) - | _ -> bad_vernac_args "ShowNode") - -let _ = - add "ShowEx" - (function - | [] -> (fun () -> show_top_evars ()) - | _ -> bad_vernac_args "ShowEx") - -let _ = - add "Go" - (function - | [VARG_NUMBER n] -> - (fun () -> (Pfedit.traverse n;show_node())) - | [VARG_STRING"top"] -> - (fun () -> (Pfedit.reset_top_of_tree ();show_node())) - | [VARG_STRING"next"] -> - (fun () -> (Pfedit.traverse_next_unproven ();show_node())) - | [VARG_STRING"prev"] -> - (fun () -> (Pfedit.traverse_prev_unproven ();show_node())) - | _ -> bad_vernac_args "Go") - -let _ = - add "ShowProof" - (function - | [] -> - (fun () -> - 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 - msgnl (str"LOC: " ++ - prlist_with_sep pr_spc pr_int (List.rev cursor) ++ fnl () ++ - str"Subgoals" ++ fnl () ++ - prlist - (fun (mv,ty) -> - (int mv ++ str" -> " ++ prtype ty ++ fnl ())) - meta_types ++ - str"Proof: " ++ prterm (Evarutil.nf_evar evc pfterm))) - | _ -> bad_vernac_args "ShowProof") - -let _ = - add "CheckGuard" - (function - | [] -> - (fun () -> - let pts = get_pftreestate () in - let pf = proof_of_pftreestate pts - and cursor = cursor_of_pftreestate pts in - let (pfterm,_) = extract_open_pftreestate pts in - let message = - try - Inductiveops.control_only_guard (Evarutil.evar_env pf.goal) - pfterm; - (str "The condition holds up to here") - with UserError(_,s) -> - (str ("Condition violated : ") ++s) - in - msgnl message) - | _ -> bad_vernac_args "CheckGuard") - -let _ = - add "ShowTree" - (function - | [] -> (fun () -> show_prooftree()) - | _ -> bad_vernac_args "ShowTree") - -let _ = - add "ShowScript" - (function - | [] -> (fun () -> show_script()) - | _ -> bad_vernac_args "ShowScript") - -let _ = - add "ExplainProof" - (function l -> - let l = number_list l in - fun () -> - let pts = get_pftreestate() in - let evc = evc_of_pftreestate pts in - let rec aux pts = function - | [] -> pts - | (n::l) -> aux (Tacmach.traverse n pts) l in - let pts = aux pts (l@[-1]) in - let pf = proof_of_pftreestate pts in - msg (Refiner.print_script true evc (Global.named_context()) pf)) - -let _ = - add "ExplainProofTree" - (function l -> - let l = number_list l in - fun () -> - let pts = get_pftreestate() in - let evc = evc_of_pftreestate pts in - let rec aux pts = function - | [] -> pts - | (n::l) -> aux (Tacmach.traverse n pts) l in - let pts = aux pts (l@[-1]) in - let pf = proof_of_pftreestate pts in - msg (Refiner.print_proof evc (Global.named_context()) pf)) - -let _ = - add "ShowProofs" - (function [] -> - (fun () -> - let l = Pfedit.get_all_proof_names() in - msgnl (prlist_with_sep pr_spc pr_id l)) - | _ -> bad_vernac_args "ShowProofs") - -let _ = - add "PrintAll" - (function - | [] -> (fun () -> msg(print_full_context_typ ())) - | _ -> bad_vernac_args "PrintAll") - -let _ = - add "PRINT" - (function - | [] -> (fun () -> msg(print_local_context())) - | _ -> bad_vernac_args "PRINT") - -(* Pris en compte dans PrintOption *) - -let _ = - add "PrintId" - (function - | [VARG_QUALID qid] -> (fun () -> msg(print_name qid)) - | _ -> bad_vernac_args "PrintId") - -let _ = - add "PrintOpaqueId" - (function - | [VARG_QUALID qid] -> (fun () -> msg(print_opaque_name qid)) - | _ -> bad_vernac_args "PrintOpaqueId") - -let _ = - add "PrintSec" - (function - | [VARG_QUALID qid] -> (fun () -> msg(print_sec_context_typ qid)) - | _ -> bad_vernac_args "PrintSec") - -let _ = declare_bool_option - {optsync = false; - optname = "silent"; - optkey = (PrimaryTable "Silent"); - optread = is_silent; - optwrite = make_silent } - -let _ = - add "BeginSilent" - (function - | [] -> (fun () -> set_bool_option_value (PrimaryTable "Silent") true) - | _ -> bad_vernac_args "BeginSilent") - -let _ = - add "EndSilent" - (function - | [] -> (fun () -> set_bool_option_value (PrimaryTable "Silent") false) - | _ -> bad_vernac_args "EndSilent") - -let _ = - add "DebugOn" - (function - | [] -> (fun () -> set_debug DebugOn) - | _ -> bad_vernac_args "DebugOn") - -let _ = - add "DebugOff" - (function - | [] -> (fun () -> set_debug DebugOff) - | _ -> bad_vernac_args "DebugOff") - -let _ = - add "StartProof" - (function - | [VARG_STRING kind;VARG_IDENTIFIER s;VARG_CONSTR com] -> - let stre = fst (interp_definition_kind kind) in - fun () -> - begin - if (kind = "LETTOP") && not(refining ()) then - errorlabstrm "Vernacentries.StartProof" (str - "Let declarations can only be used in proof editing mode"); - start_proof_com (Some s) stre com; - if_verbose show_open_subgoals () - end - | _ -> bad_vernac_args "StartProof") - -let _ = - add "TheoremProof" - (function - | [VARG_STRING kind; VARG_IDENTIFIER id; - VARG_CONSTR com; VARG_VARGLIST coml] -> - let calls = List.map - (function - | (VCALL(na,l)) -> (na,l) - | _ -> bad_vernac_args "") - coml - in - let (stre,opacity) = interp_definition_kind kind in - (fun () -> - try - States.with_heavy_rollback - (fun () -> - start_proof_com (Some id) stre com; - if_verbose show_open_subgoals (); - List.iter Vernacinterp.call calls; - if_verbose show_script (); - if not (kind = "LETTOP") then - save_named opacity - else - let csr = interp_type Evd.empty (Global.env ()) com - and (_,({const_entry_body = pft},_)) = cook_proof () in - let cutt = vernac_tactic ("Cut",[Constr csr]) - and exat = vernac_tactic ("Exact",[Constr pft]) in - delete_proof id; - by (tclTHENS cutt [introduction id;exat])) - () - with e -> - if (is_unsafe "proof") && not (kind = "LETTOP") then begin - msgnl (str "Warning: checking of theorem " ++ pr_id id ++ - spc () ++ str "failed" ++ - str "... converting to Axiom"); - delete_proof id; - let _ = parameter_def_var id com in () - end else - errorlabstrm "Vernacentries.TheoremProof" - (str "checking of theorem " ++ pr_id id ++ spc () ++ - str "failed... aborting")) - | _ -> bad_vernac_args "TheoremProof") - -let _ = - add "DEFINITION" - (function - | (VARG_STRING kind :: VARG_IDENTIFIER id :: VARG_CONSTR c :: rest) -> - let typ_opt,red_option = match rest with - | [] -> None, None - | [VARG_CONSTR t] -> Some t, None - | [VARG_TACTIC_ARG (Redexp redexp)] -> - None, Some redexp - | [VARG_CONSTR t; VARG_TACTIC_ARG (Redexp redexp)] -> - Some t, Some redexp - | _ -> bad_vernac_args "DEFINITION" - in - let local,stre,coe,objdef,idcoe = match kind with - | "DEFINITION" -> false,NeverDischarge, false,false,false - | "COERCION" -> false,NeverDischarge, true, false,false - | "LCOERCION" -> true, make_strength_0(),true, false,false - | "LET" -> true, make_strength_2(),false,false,false - | "LOCAL" -> true, make_strength_0(),false,false,false - | "OBJECT" -> false,NeverDischarge, false,true, false - | "LOBJECT" -> true, make_strength_0(),false,true, false - | "OBJCOERCION" -> false,NeverDischarge, true, true, false - | "LOBJCOERCION" -> true,make_strength_0(),true,true, false - | "SUBCLASS" -> false,NeverDischarge, false,false,true - | "LSUBCLASS" -> true, make_strength_0(),false,false,true - | _ -> anomaly "Unexpected string" - in - fun () -> - let ref = - definition_body_red red_option id (local,stre) c typ_opt in - if coe then begin - Class.try_add_new_coercion ref stre; - if_verbose message ((string_of_id id) ^ " is now a coercion") - end; - if idcoe then begin - let cl = Class.class_of_ref ref in - Class.try_add_new_coercion_subclass cl stre - end; - if objdef then Recordobj.objdef_declare ref - | _ -> bad_vernac_args "DEFINITION") - -let _ = - add "CANONICAL" - (function - | [VARG_QUALID qid] -> - fun () -> - let ref = Nametab.global dummy_loc qid in - Recordobj.objdef_declare ref - | _ -> bad_vernac_args "CANONICAL") - -let _ = - add "VARIABLE" - (function - | [VARG_STRING kind; VARG_BINDERLIST slcl] -> - if List.length slcl = 1 & List.length (fst (List.hd slcl)) = 1 then - (match kind with - | "VARIABLES" -> warning "Many variables are expected" - | "HYPOTHESES" -> warning "Many hypotheses are expected" - | "COERCIONS" -> warning "Many hypotheses are expected" - | _ -> ()); - let coe = match kind with - | "COERCION" -> true - | "COERCIONS" -> true - | _ -> false - in - let stre = make_strength_0() in - fun () -> - List.iter - (fun (sl,c) -> - List.iter - (fun id -> - let ref = hypothesis_def_var (refining()) id stre c in - if coe then Class.try_add_new_coercion ref stre) - sl) - slcl - | _ -> bad_vernac_args "VARIABLE") - -let _ = - add "PARAMETER" - (function - | [VARG_STRING kind; VARG_BINDERLIST slcl] -> - if List.length slcl = 1 & List.length (fst (List.hd slcl)) = 1 & - kind = "PARAMETERS" then warning "Many parameters are expected"; - fun () -> - List.iter - (fun (sl,c) -> - List.iter - (fun s -> - let _ = parameter_def_var s c in ()) - sl) - slcl - | _ -> bad_vernac_args "PARAMETER") - -let _ = - add "Eval" - (function - | VARG_TACTIC_ARG (Redexp redexp) :: VARG_CONSTR c :: g -> - let (evmap,sign) = get_current_context_of_args g in - let redfun = print_eval (reduction_of_redexp redexp) sign in - fun () -> msg (redfun (judgment_of_rawconstr evmap sign c)) - | _ -> bad_vernac_args "Eval") - -let _ = - add "Check" - (function - | VARG_STRING "PRINTTYPE" :: VARG_CONSTR c :: _ -> - (fun () -> - let evmap = Evd.empty in - let env = Global.env() in - let c = interp_constr evmap env c in - let senv = Global.safe_env() in - let j = Safe_typing.typing senv c in - msg (print_safe_judgment env j)) - | VARG_STRING "CHECK" :: VARG_CONSTR c :: g -> - (fun () -> - let (evmap, env) = get_current_context_of_args g in - let c = interp_constr evmap env c in - let (j,cst) = Typeops.infer env c in - let _ = Environ.add_constraints cst env in - msg (print_judgment env j)) - | _ -> bad_vernac_args "Check") - - -let extract_qualid = function - | VARG_QUALID qid -> - (try Nametab.locate_loaded_library qid - with Not_found -> - error ("Module/section "^(Nametab.string_of_qualid qid)^" not found")) - | _ -> bad_vernac_args "extract_qualid" - -let inside_outside = function - | (VARG_STRING "outside") :: l -> List.map extract_qualid l, true - | (VARG_STRING "inside") :: l -> List.map extract_qualid l, false - | [] -> [], true - | _ -> bad_vernac_args "inside/outside" - -let _ = - add "SearchRewrite" - (function - | (VARG_CONSTR c) :: l -> - (fun () -> - let _,pat = interp_constrpattern Evd.empty (Global.env()) c in - Search.search_rewrite pat (inside_outside l)) - | _ -> bad_vernac_args "SearchRewrite") - -let _ = - add "SearchPattern" - (function - | (VARG_CONSTR c) :: l -> - (fun () -> - let _,pat = interp_constrpattern Evd.empty (Global.env()) c in - Search.search_pattern pat (inside_outside l)) - | _ -> bad_vernac_args "SearchPattern") - -let _ = - add "SEARCH" - (function - | (VARG_QUALID qid) :: l -> - (fun () -> - let ref = Nametab.global dummy_loc qid in - Search.search_by_head ref (inside_outside l)) - | _ -> bad_vernac_args "SEARCH") - -let _ = - add "INSPECT" - (function - | [VARG_NUMBER n] -> (fun () -> msg(inspect n)) - | _ -> bad_vernac_args "INSPECT") - -let _ = - add "SETUNDO" - (function - | [VARG_NUMBER n] -> (fun () -> set_undo n) - | _ -> bad_vernac_args "SETUNDO") - -let _ = - add "UNSETUNDO" - (function - | [] -> (fun () -> reset_undo ()) - | _ -> bad_vernac_args "UNSETUNDO") - -let _ = - add "SETHYPSLIMIT" - (function - | [VARG_NUMBER n] -> (fun () -> set_print_hyps_limit n) - | _ -> bad_vernac_args "SETHYPSLIMIT") - -let _ = - add "UNSETHYPSLIMIT" - (function - | [] -> (fun () -> unset_print_hyps_limit ()) - | _ -> bad_vernac_args "UNSETHYPSLIMIT") - -let _ = - add "ONEINDUCTIVE" - (function - | [ VARG_STRING f; - VARG_IDENTIFIER s; - VARG_CONSTR c; - VARG_BINDERLIST binders; - VARG_BINDERLIST constructors ] -> - let la = join_binders binders in - let li = List.map - (function - | ([id],c) -> (id,c) - | _ -> bad_vernac_args "ONEINDUCTIVE") - constructors - in - (fun () -> build_mutual la [(s,c,li)] (isfinite f)) - | _ -> bad_vernac_args "ONEINDUCTIVE") - -let eq_la (id,ast) (id',ast') = id = id' & alpha_eq(ast,ast') - -let extract_la_lc = function - | [] -> anomaly "Vernacentries: empty list of inductive types" - | (la,lc)::rest -> - let rec check = function - | [] -> [] - | (la',lc)::rest -> - if (List.length la = List.length la') && - (List.for_all2 eq_la la la') - then - lc::(check rest) - else - error ("Parameters should be syntactically the same "^ - "for each inductive type") - in - (la,lc::(check rest)) - -let _ = - add "MUTUALINDUCTIVE" - (function - | [VARG_STRING f; VARG_VARGLIST indl] -> - let lac = - (List.map - (function - | (VARG_VARGLIST - [VARG_IDENTIFIER arid; - VARG_CONSTR arc; - VARG_BINDERLIST binders; - VARG_BINDERLIST lconstr]) - -> - let la = join_binders binders in - (la, (arid, arc, - List.map - (function - | ([id],c) -> (id,c) - | _ -> bad_vernac_args "") - lconstr)) - | _ -> bad_vernac_args "MUTUALINDUCTIVE") indl) - in - let (la,lnamearconstructs) = extract_la_lc lac in - fun () -> build_mutual la lnamearconstructs (isfinite f) - | _ -> bad_vernac_args "MUTUALINDUCTIVE") - -let _ = - add "OLDMUTUALINDUCTIVE" - (function - | [VARG_BINDERLIST binders; VARG_STRING f; VARG_VARGLIST indl] -> - let la = join_binders binders in - let lnamearconstructs = - (List.map - (function - | (VARG_VARGLIST - [VARG_IDENTIFIER arid; - VARG_CONSTR arc; - VARG_BINDERLIST lconstr]) - -> (arid, - arc, - List.map - (function - | ([id],c) -> (id,c) - | _ -> bad_vernac_args "OLDMUTUALINDUCTIVE") - lconstr) - | _ -> bad_vernac_args "") indl) - in - fun () -> build_mutual la lnamearconstructs (isfinite f) - | _ -> bad_vernac_args "MUTUALINDUCTIVE") - -let _ = - add "RECORD" - (function - | [VARG_STRING coe; - VARG_IDENTIFIER struc; - VARG_BINDERLIST binders; - VARG_CONSTR sort; - VARG_VARGLIST namec; - VARG_VARGLIST cfs] -> - let ps = join_binders binders in - let cfs = - List.map - (function - | (VARG_VARGLIST - [VARG_STRING str; VARG_STRING b; - VARG_IDENTIFIER id; VARG_CONSTR c]) -> - let assum = match b with - | "ASSUM" -> true - | "DEF" -> false - | _ -> bad_vernac_args "RECORD" in - (str = "COERCION", (id, assum, c)) - | _ -> bad_vernac_args "RECORD") - cfs in - let const = match namec with - | [] -> add_prefix "Build_" struc - | [VARG_IDENTIFIER id] -> id - | _ -> bad_vernac_args "RECORD" in - let iscoe = (coe = "COERCION") in - let s = interp_sort sort in - fun () -> Record.definition_structure (iscoe,struc,ps,cfs,const,s) - | _ -> bad_vernac_args "RECORD") - -let _ = - add "MUTUALRECURSIVE" - (function - | [VARG_VARGLIST lmi] -> - (let lnameargsardef = - List.map - (function - | (VARG_VARGLIST - [VARG_IDENTIFIER fid; - VARG_BINDERLIST farg; - VARG_CONSTR arf; - VARG_CONSTR ardef]) - -> (fid,join_binders farg,arf,ardef) - | _ -> bad_vernac_args "MUTUALRECURSIVE") lmi - in - fun () -> build_recursive lnameargsardef) - | _ -> bad_vernac_args "MUTUALRECURSIVE") - -let _ = - add "MUTUALCORECURSIVE" - (function - | [VARG_VARGLIST lmi] -> - let lnameardef = - List.map - (function - | (VARG_VARGLIST - [VARG_IDENTIFIER fid; - VARG_CONSTR arf; - VARG_CONSTR ardef]) - -> (fid,arf,ardef) - | _ -> bad_vernac_args "MUTUALCORECURSIVE") lmi - in - fun () -> build_corecursive lnameardef - | _ -> bad_vernac_args "MUTUALCORECURSIVE") - -let _ = - add "INDUCTIONSCHEME" - (function - | [VARG_VARGLIST lmi] -> - let lnamedepindsort = - List.map - (function - | (VARG_VARGLIST - [VARG_IDENTIFIER fid; - VARG_STRING depstr; - VARG_QUALID indid; - VARG_CONSTR sort]) -> - let dep = match depstr with - | "DEP" -> true - | "NODEP" -> false - | _ -> anomaly "Unexpected string" - in - (fid,dep,indid,sort) - | _ -> bad_vernac_args "INDUCTIONSCHEME") lmi - in - fun () -> build_scheme lnamedepindsort - | _ -> bad_vernac_args "INDUCTIONSCHEME") - -let _ = - add "SyntaxMacro" - (function - | [VARG_IDENTIFIER id;VARG_CONSTR com] -> - (fun () -> syntax_definition id com) - | [VARG_IDENTIFIER id;VARG_CONSTR com; VARG_NUMBER n] -> - (fun () -> - let rec aux t = function - | 0 -> t - | n -> aux (ope("APPLIST",[t;ope("ISEVAR",[])])) (n-1) - in - syntax_definition id (aux com n)) - | _ -> bad_vernac_args "SyntaxMacro") - -let _ = - add "Require" - (function - | VARG_STRING import :: VARG_STRING specif :: l -> - let l = - List.map - (function - | VARG_QUALID qid -> qid - | _ -> bad_vernac_args "Require") l in - let spec = - if specif="UNSPECIFIED" then - None - else - Some (specif="SPECIFICATION") in - let export = (import="EXPORT") in - fun () -> Library.require_module spec l export - | _ -> bad_vernac_args "Require") - -let _ = - add "RequireFrom" - (function - | [VARG_STRING import; VARG_STRING specif; - VARG_QUALID qid; VARG_STRING filename] -> - (fun () -> - Library.require_module_from_file - (if specif="UNSPECIFIED" then - None - else - Some (specif="SPECIFICATION")) - qid filename - (import="EXPORT")) - | _ -> bad_vernac_args "RequireFrom") - -let _ = - add "NOP" - (function - | [] -> (fun () -> ()) - | _ -> bad_vernac_args "NOP") - -let _ = - add "CLASS" + vinterp_add "CLASS" (function | [VARG_STRING kind; VARG_QUALID qid] -> let stre = if kind = "LOCAL" then make_strength_0() else - NeverDischarge + Nametab.NeverDischarge in fun () -> - let ref = Nametab.global dummy_loc qid in + 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") | _ -> bad_vernac_args "CLASS") -let cl_of_qualid qid = - match Nametab.repr_qualid qid with - | d, id when string_of_id id = "FUNCLASS" & repr_dirpath d = [] -> - Classops.CL_FUN - | d, id when string_of_id id = "SORTCLASS" & repr_dirpath d = [] -> - Classops.CL_SORT - | _ -> Class.class_of_ref (Nametab.global dummy_loc qid) - -let _ = - add "COERCION" - (function - | [VARG_STRING kind;VARG_STRING identity; - VARG_QUALID qid;VARG_QUALID qids;VARG_QUALID qidt] -> - let stre = - if (kind = "LOCAL") then - make_strength_0() - else - NeverDischarge - in - let isid = identity = "IDENTITY" in - let target = cl_of_qualid qidt in - let source = cl_of_qualid qids in - fun () -> - if isid then match Nametab.repr_qualid qid with - | d, id when repr_dirpath d = [] -> - Class.try_add_new_identity_coercion id stre source target - | _ -> bad_vernac_args "COERCION" - else - let ref = Nametab.global dummy_loc qid in - Class.try_add_new_coercion_with_target ref stre source target; - if_verbose - message - ((Nametab.string_of_qualid qid) ^ " is now a coercion") - | _ -> bad_vernac_args "COERCION") - -let _ = - add "PrintGRAPH" - (function - | [] -> (fun () -> ppnl (Prettyp.print_graph())) - | _ -> bad_vernac_args "PrintGRAPH") - -let _ = - add "PrintCLASSES" - (function - | [] -> (fun () -> ppnl (Prettyp.print_classes())) - | _ -> bad_vernac_args "PrintCLASSES") - -let _ = - add "PrintCOERCIONS" - (function - | [] -> (fun () -> ppnl (Prettyp.print_coercions())) - | _ -> bad_vernac_args "PrintCOERCIONS") - -let _ = - add "PrintPATH" - (function - | [VARG_QUALID qids;VARG_QUALID qidt] -> - (fun () -> - ppnl (Prettyp.print_path_between - (cl_of_qualid qids) (cl_of_qualid qidt))) - | _ -> bad_vernac_args "PrintPATH") - (* Meta-syntax commands *) - let _ = add "TOKEN" (function | [VARG_STRING s] -> (fun () -> Metasyntax.add_token_obj s) | _ -> bad_vernac_args "TOKEN") - -let _ = - add "GRAMMAR" - (function - | [VARG_STRING univ; VARG_ASTLIST al] -> - (fun () -> Metasyntax.add_grammar_obj univ al) - | _ -> bad_vernac_args "GRAMMAR") - -let _ = - add "SYNTAX" - (function - | [VARG_STRING whatfor; VARG_ASTLIST sel] -> - (fun () -> Metasyntax.add_syntax_obj whatfor sel) - | _ -> bad_vernac_args "SYNTAX") - -let _ = - add "TACDEF" - (let rec tacdef_fun lacc=function - (VARG_IDENTIFIER name)::(VARG_AST tacexp)::tl -> - tacdef_fun ((name,tacexp)::lacc) tl - |[] -> - fun () -> - List.iter (fun (name,ve) -> Tacinterp.add_tacdef name ve) lacc - |_ -> bad_vernac_args "TACDEF" - in - tacdef_fun []) - -let _ = - add "INFIX" - (function - | [VARG_AST assoc; VARG_NUMBER n; VARG_STRING inf; VARG_QUALID pref] -> - let ref = Astterm.globalize_qualid pref in - (fun () -> - Metasyntax.add_infix (Extend.gram_assoc assoc) n inf ref) - | _ -> bad_vernac_args "INFIX") - -let _ = - add "DISTFIX" - (function - | [VARG_AST assoc; VARG_NUMBER n; VARG_STRING s; VARG_QUALID pref] -> - let ref = Astterm.globalize_qualid pref in - (fun () -> - Metasyntax.add_distfix (Extend.gram_assoc assoc) n s ref) - | _ -> bad_vernac_args "DISTFIX") - -let _ = - add "PrintGrammar" - (function - | [VARG_IDENTIFIER uni; VARG_IDENTIFIER ent] -> - (fun () -> - Metasyntax.print_grammar (string_of_id uni) (string_of_id ent)) - | _ -> bad_vernac_args "PrintGrammar") +***) (* Search commands *) @@ -1460,407 +853,97 @@ let _ = | _ -> bad_vernac_args "Searchisos") ***) -open Goptions - -let _ = declare_int_option - { optsync=true; - optkey=SecondaryTable("Printing","Depth"); - optname="the printing depth"; - optread=Pp_control.get_depth_boxes; - optwrite=Pp_control.set_depth_boxes } - -let _ = - add "SetTableField" - (function - (* Hook for Printing Coercions *) - | (VARG_IDENTIFIER t) :: (VARG_IDENTIFIER f) :: l - when t = id_of_string "Printing" && f = id_of_string "Coercion" -> - let ql = - List.map - (function - | VARG_QUALID qid -> qid - | _ -> bad_vernac_args "PRINTING_COERCIONS_ON") l in - (fun () -> - List.iter - (fun qid -> - Classops.set_coercion_visibility true - (coercion_of_qualid dummy_loc qid)) - ql) - | [(VARG_IDENTIFIER t);(VARG_IDENTIFIER f);arg] -> - (fun () -> - let key = - SecondaryTable (string_of_id t,string_of_id f) in - match arg with - | VARG_NUMBER n -> set_int_option_value key n - | VARG_STRING s -> set_string_option_value key s - | _ -> error "No such type of option value") - | [(VARG_IDENTIFIER t);(VARG_IDENTIFIER f)] -> - (fun () -> - let key = - SecondaryTable (string_of_id t,string_of_id f) in - set_bool_option_value key true) - | [(VARG_IDENTIFIER t);arg] -> - (fun () -> - let key = PrimaryTable (string_of_id t) in - match arg with - | VARG_NUMBER n -> set_int_option_value key n - | VARG_STRING s -> set_string_option_value key s - | _ -> error "No such type of option value") - | [(VARG_IDENTIFIER t)] -> - (fun () -> - let key = PrimaryTable (string_of_id t) in - set_bool_option_value key true) - | _ -> bad_vernac_args "VernacOption") - -let _ = - add "UnsetTableField" - (function - | [(VARG_IDENTIFIER t);(VARG_IDENTIFIER f)] -> - (fun () -> - let key = - SecondaryTable (string_of_id t,string_of_id f) in - set_bool_option_value key false) - | [(VARG_IDENTIFIER t)] -> - (fun () -> - let key = PrimaryTable (string_of_id t) in - set_bool_option_value key false) - | _ -> bad_vernac_args "VernacOption") - -let _ = - add "AddTableField" - (function - | [VARG_IDENTIFIER t; VARG_IDENTIFIER f; VARG_QUALID v] -> - (fun () -> - let key = - SecondaryTable (string_of_id t,string_of_id f) in - try - (get_ident_table key)#add (Nametab.global dummy_loc v) - with Not_found -> - error_undeclared_key key) - | [VARG_IDENTIFIER t; VARG_IDENTIFIER f; VARG_STRING s] -> - (fun () -> - let key = - SecondaryTable (string_of_id t,string_of_id f) in - try - (get_string_table key)#add s - with Not_found -> - error_undeclared_key key) - | [VARG_IDENTIFIER t; VARG_QUALID v] -> - (fun () -> - let key = PrimaryTable (string_of_id t) in - try - (get_ident_table key)#add (Nametab.global dummy_loc v) - with Not_found -> - error_undeclared_key key) - | [VARG_IDENTIFIER t; VARG_STRING s] -> - (fun () -> - let key = PrimaryTable (string_of_id t) in - try - (get_string_table key)#add s - with Not_found -> - error_undeclared_key key) - | _ -> bad_vernac_args "TableField") - -let _ = - add "RemoveTableField" - (function - (* Hook for Printing Coercions *) - | (VARG_IDENTIFIER t) :: (VARG_IDENTIFIER f) :: l - when t = id_of_string "Printing" && f = id_of_string "Coercion" -> - let ql = - List.map - (function - | VARG_QUALID qid -> qid - | _ -> bad_vernac_args "PRINTING_COERCIONS_OFF") l in - (fun () -> - List.iter - (fun qid -> - Classops.set_coercion_visibility false - (coercion_of_qualid dummy_loc qid)) - ql) - | [VARG_IDENTIFIER t; VARG_IDENTIFIER f; VARG_QUALID v] -> - (fun () -> - let key = - SecondaryTable (string_of_id t,string_of_id f) in - try - (get_ident_table key)#remove (Nametab.global dummy_loc v) - with Not_found -> - error_undeclared_key key) - | [VARG_IDENTIFIER t; VARG_IDENTIFIER f; VARG_STRING v] -> - (fun () -> - let key = - SecondaryTable (string_of_id t,string_of_id f) in - try - (get_string_table key)#remove v - with Not_found -> - error_undeclared_key key) - | [VARG_IDENTIFIER t; VARG_QUALID v] -> - (fun () -> - let key = PrimaryTable (string_of_id t) in - try - (get_ident_table key)#remove (Nametab.global dummy_loc v) - with Not_found -> - error_undeclared_key key) - | [VARG_IDENTIFIER t; VARG_STRING v] -> - (fun () -> - let key = PrimaryTable (string_of_id t) in - try - (get_string_table key)#remove v - with Not_found -> - error_undeclared_key key) - | _ -> bad_vernac_args "TableField") - -let _ = - add "MemTableField" - (function - (* Hook for Printing Coercions *) - | (VARG_IDENTIFIER t) :: (VARG_IDENTIFIER f) :: l - when t = id_of_string "Printing" && f = id_of_string "Coercion" -> - let ql = - List.map - (function - | VARG_QUALID qid -> qid - | _ -> bad_vernac_args "TEST_PRINTING_COERCIONS") l in - (fun () -> - List.iter - (fun qid -> - let coe = coercion_of_qualid dummy_loc qid in - if Classops.is_coercion_visible coe then - message - ("Printing of coercion "^(Nametab.string_of_qualid qid)^ - " is set") - else - message - ("Printing of coercion "^(Nametab.string_of_qualid qid)^ - " is unset")) - ql) - | [VARG_IDENTIFIER t; VARG_IDENTIFIER f; VARG_QUALID v] -> - (fun () -> - let key = - SecondaryTable (string_of_id t,string_of_id f) in - try - (get_ident_table key)#mem (Nametab.global dummy_loc v) - with Not_found -> - error_undeclared_key key) - | [VARG_IDENTIFIER t; VARG_IDENTIFIER f; VARG_STRING v] -> - (fun () -> - let key = - SecondaryTable (string_of_id t,string_of_id f) in - try - (get_string_table key)#mem v - with Not_found -> - error_undeclared_key key) - | [VARG_IDENTIFIER t; VARG_QUALID v] -> - (fun () -> - let key = PrimaryTable (string_of_id t) in - try - (get_ident_table key)#mem (Nametab.global dummy_loc v) - with Not_found -> - error_undeclared_key key) - | [VARG_IDENTIFIER t; VARG_IDENTIFIER v] -> - (fun () -> - let key = SecondaryTable (string_of_id t, string_of_id v) in - try - (get_ident_table key)#print - with not_found -> - try - (get_string_table key)#print - with not_found -> - try - print_option_value key - with Not_found -> - error_undeclared_key key) - | [VARG_IDENTIFIER t; VARG_STRING v] -> - (fun () -> - let key = PrimaryTable (string_of_id t) in - try - (get_string_table key)#mem v - with Not_found -> - error_undeclared_key key) - | [VARG_IDENTIFIER t] -> - (fun () -> - let key = PrimaryTable (string_of_id t) in - try - (get_ident_table key)#print - with not_found -> - try - (get_string_table key)#print - with not_found -> - try - print_option_value key - with Not_found -> - error_undeclared_key key) - | _ -> bad_vernac_args "TableField") - -let _ = - add "PrintOption" - (function - | [VARG_IDENTIFIER t; VARG_IDENTIFIER f] -> - (fun () -> - let key = SecondaryTable (string_of_id t,string_of_id f) in - try - (get_ident_table key)#print - with not_found -> - try - (get_string_table key)#print - with not_found -> - try - print_option_value key - with Not_found -> - error_undeclared_key key) - | [VARG_IDENTIFIER t] -> - (fun () -> - let key = PrimaryTable (string_of_id t) in - try - (get_ident_table key)#print - with not_found -> - try - (get_string_table key)#print - with not_found -> - try - print_option_value key - with Not_found -> - if (string_of_id t) = "Tables" then - print_tables () - else - msg(print_name (Nametab.make_short_qualid t))) - | _ -> bad_vernac_args "TableField") - - -open Tactics -open Pfedit - -(* - The first one is a command that should be a tactic. It has been - added by Christine to patch an error in the design of the proof - machine, and enables to instantiate existential variables when - there are no more goals to solve. It cannot be a tactic since - all tactics fail if there are no further goals to prove. *) - -let _ = - vinterp_add "EXISTENTIAL" - (function - | [VARG_NUMBER n; VARG_CONSTR c] -> - (fun () -> instantiate_nth_evar_com n c) - | _ -> assert false) - -(* The second is a stupid macro that should be replaced by ``Exact - c. Save.'' all along the theories. *) - -let _ = - vinterp_add "PROOF" - (function - | [VARG_CONSTR c] -> - (fun () -> (* by (tactic_com exact c) *) - (* on experimente la synthese d'ise dans exact *) - by (dyn_exact_check [Command c]); - save_named true) - | _ -> assert false) - -let print_subgoals () = if_verbose show_open_subgoals_focused () - -let _ = - vinterp_add "SOLVE" - (function l -> - let (n,tcom) = match l with - | [VARG_NUMBER n;VARG_TACTIC tcom] -> (n,tcom) - | _ -> invalid_arg "SOLVE" - in - (fun () -> - if not (refining ()) then - error "Unknown command of the non proof-editing mode"; - solve_nth n (Tacinterp.hide_interp tcom); - print_subgoals(); - (* in case a strict subtree was completed, - go back to the top of the prooftree *) - if subtree_solved () then - (reset_top_of_tree (); print_subgoals()) - )) - -(* Coq syntax for ML commands *) - -let _ = vinterp_add "DeclareMLModule" - (fun l -> - let sl = - List.map - (function - | (VARG_STRING s) -> s - | _ -> anomaly "DeclareMLModule : not a string") l - in - fun () -> Mltop.declare_ml_modules sl) - -let _ = vinterp_add "AddMLPath" - (function - | [VARG_STRING s] -> - (fun () -> Mltop.add_ml_dir (glob s)) - | _ -> anomaly "AddMLPath : not a string") - -let _ = vinterp_add "RecAddMLPath" - (function - | [VARG_STRING s] -> - (fun () -> Mltop.add_rec_ml_dir (glob s)) - | _ -> anomaly "RecAddMLPath : not a string") - -let _ = vinterp_add "PrintMLPath" - (function - | [] -> (fun () -> Mltop.print_ml_path ()) - | _ -> anomaly "PrintMLPath : does not expect any argument") - -let _ = vinterp_add "PrintMLModules" - (function - | [] -> (fun () -> Mltop.print_ml_modules ()) - | _ -> anomaly "PrintMLModules : does not expect an argument") - -let _ = vinterp_add "DumpUniverses" - (function - | [] -> (fun () -> pp (Univ.pr_universes (Global.universes ()))) - | [VARG_STRING s] -> - (fun () -> let output = open_out s in - try - Univ.dump_universes output (Global.universes ()); - close_out output; - msg (str ("Universes written to file \""^s^"\".") ++ fnl ()) - with - e -> close_out output; raise e - ) - | _ -> - anomaly "DumpUniverses : expects a filename or nothing as argument") - -(* Simulate the Intro(s) tactic *) - -open Tactics - -let id_of_name = function - Anonymous -> id_of_string "H" - | Name id -> id;; - -let rec do_renum avoid gl = function - [] -> "" - | [n] -> (string_of_id (fresh_id avoid (id_of_name n) gl)) - | n :: l -> let id = fresh_id avoid (id_of_name n) gl in - (string_of_id id)^" "^(do_renum (id :: avoid) gl l) - -let _ = vinterp_add "SHOWINTRO" - (function - | [] -> - (fun () -> - 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 - try - let n = - List.hd (List.rev_map fst l) in - message (string_of_id (fresh_id [] (id_of_name n) gl)) - with Failure "hd" -> message "") - | _ -> bad_vernac_args "Show Intro") - -let _ = vinterp_add "SHOWINTROS" - (function - | [] -> - (fun () -> - 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 = List.rev_map fst l in - message (do_renum [] gl l)) - | _ -> bad_vernac_args "Show Intros") +let interp c = match c with + (* Control (done in vernac) *) + | (VernacTime _ | VernacVar _ | VernacList _ | VernacLoad _) -> assert false + + (* Syntax *) + | VernacSyntax (whatfor,sel) -> vernac_syntax whatfor sel + | VernacTacticGrammar al -> Metasyntax.add_tactic_grammar al + | VernacGrammar (univ,al) -> vernac_grammar univ al + | VernacInfix (assoc,n,inf,qid) -> vernac_infix assoc n inf qid + | VernacDistfix (assoc,n,inf,qid) -> vernac_distfix assoc n inf qid + + (* Gallina *) + | VernacDefinition (k,id,red,t,otyp,f) -> vernac_definition k id red t otyp f + | VernacStartProof (k,id,t,top,f) -> vernac_start_proof k id t top f + | VernacEndProof (opaq,idopt) -> vernac_end_proof opaq idopt + | 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 + | VernacScheme l -> vernac_scheme l + + (* Gallina extensions *) + | VernacRecord (coe,id,bl,s,idopt,fs) -> vernac_record coe id bl s idopt fs + | VernacBeginSection id -> vernac_begin_section id + | VernacEndSection id -> vernac_end_section id + | VernacRequire (export,spec,qidl) -> vernac_require export spec qidl + | VernacImport (export,qidl) -> vernac_import export qidl + | VernacCanonical qid -> vernac_canonical qid + | VernacCoercion (str,r,s,t) -> vernac_coercion str r s t + | VernacIdentityCoercion (str,id,s,t) -> vernac_identity_coercion str id s t + + (* Solving *) + | VernacSolve (n,tac) -> vernac_solve n tac + | VernacSolveExistential (n,c) -> vernac_solve_existential n c + + (* Auxiliary file and library management *) + | VernacRequireFrom (exp,spec,id,f) -> vernac_require_from exp spec id f + | VernacAddLoadPath (isrec,s,alias) -> vernac_add_loadpath isrec s alias + | VernacRemoveLoadPath s -> vernac_remove_loadpath s + | VernacAddMLPath (isrec,s) -> vernac_add_ml_path isrec s + | VernacDeclareMLModule l -> vernac_declare_ml_module l + | VernacChdir s -> vernac_chdir s + + (* State management *) + | VernacWriteState s -> vernac_write_state s + | VernacRestoreState s -> vernac_restore_state s + + (* Resetting *) + | VernacResetName id -> vernac_reset_name id + | VernacResetInitial -> vernac_reset_initial () + | VernacBack n -> vernac_back n + + (* Commands *) + | VernacDeclareTacticDefinition (x,l) -> vernac_declare_tactic_definition x l + | VernacHints (dbnames,hints) -> vernac_hints dbnames hints + | VernacHintDestruct (id,l,p,n,tac) -> Dhyp.add_destructor_hint id l p n tac + | VernacSyntacticDefinition (id,c,n) -> vernac_syntactic_definition id c n + | VernacDeclareImplicits (qid,l) -> vernac_declare_implicits qid l + | VernacSetOpacity (opaq, qidl) -> List.iter (vernac_set_opacity opaq) qidl + | VernacSetOption (key,v) -> vernac_set_option key v + | VernacUnsetOption key -> vernac_unset_option key + | VernacRemoveOption (key,v) -> vernac_remove_option key v + | VernacAddOption (key,v) -> vernac_add_option key v + | VernacMemOption (key,v) -> vernac_mem_option key v + | VernacPrintOption key -> vernac_print_option key + | VernacCheckMayEval (r,g,c) -> vernac_check_may_eval r g c + | VernacGlobalCheck c -> vernac_global_check c + | VernacPrint p -> vernac_print p + | VernacSearch (s,r) -> vernac_search s r + | VernacLocate l -> vernac_locate l + | VernacComments l -> if_verbose message ("Comments ok\n") + | VernacNop -> () + + (* Proof management *) +(* | VernacGoal c -> vernac_goal c*) + | VernacAbort id -> vernac_abort id + | VernacAbortAll -> vernac_abort_all () + | VernacRestart -> vernac_restart () + | VernacSuspend -> vernac_suspend () + | VernacResume id -> vernac_resume id + | VernacUndo n -> vernac_undo n + | VernacFocus n -> vernac_focus n + | VernacUnfocus -> vernac_unfocus () + | VernacGo g -> vernac_go g + | VernacShow s -> vernac_show s + | VernacCheckGuard -> vernac_check_guard () + | VernacDebug b -> vernac_debug b + + (* Toplevel control *) + | VernacToplevelControl e -> raise e + + (* Extensions *) + | VernacExtend (opn,args) -> Vernacinterp.call (opn,args) |