diff options
Diffstat (limited to 'toplevel/vernacentries.ml')
| -rw-r--r-- | toplevel/vernacentries.ml | 419 |
1 files changed, 287 insertions, 132 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index dd6d7e25..402f3b34 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -6,13 +6,13 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: vernacentries.ml 10067 2007-08-09 17:13:16Z msozeau $ i*) +(*i $Id: vernacentries.ml 11065 2008-06-06 22:39:43Z msozeau $ i*) (* Concrete syntax of the mathematical vernacular MV V2.6 *) open Pp open Util -open Options +open Flags open Names open Entries open Nameops @@ -35,6 +35,7 @@ open Decl_kinds open Topconstr open Pretyping open Redexpr +open Syntax_def (* Pcoq hooks *) @@ -44,8 +45,8 @@ type pcoq_hook = { abort : string -> unit; search : searchable -> dir_path list * bool -> unit; print_name : reference -> unit; - print_check : Environ.unsafe_judgment -> unit; - print_eval : (constr -> constr) -> Environ.env -> constr_expr -> + print_check : Environ.env -> Environ.unsafe_judgment -> unit; + print_eval : Reductionops.reduction_function -> Environ.env -> Evd.evar_map -> constr_expr -> Environ.unsafe_judgment -> unit; show_goal : int option -> unit } @@ -58,7 +59,7 @@ 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_global (Nametab.global r) + | RefClass r -> Class.class_of_global (global_with_alias r) (*******************) (* "Show" commands *) @@ -94,7 +95,7 @@ let show_script () = let pts = get_pftreestate () in let pf = proof_of_pftreestate pts and evc = evc_of_pftreestate pts in - msgnl (print_treescript true evc pf) + msgnl_with !Pp_control.deep_ft (print_treescript true evc pf) let show_thesis () = msgnl (anomaly "TODO" ) @@ -272,6 +273,11 @@ let print_located_module r = str "No module is referred to by name ") ++ pr_qualid qid in msgnl msg +let global_with_alias r = + let gr = global_with_alias r in + if !Flags.dump then Constrintern.add_glob (loc_of_reference r) gr; + gr + (**********) (* Syntax *) @@ -284,8 +290,8 @@ let vernac_bind_scope sc cll = let vernac_open_close_scope = Notation.open_close_scope -let vernac_arguments_scope local qid scl = - Notation.declare_arguments_scope local (global qid) scl +let vernac_arguments_scope local r scl = + Notation.declare_arguments_scope local (global_with_alias r) scl let vernac_infix = Metasyntax.add_infix @@ -294,12 +300,31 @@ let vernac_notation = Metasyntax.add_notation (***********) (* Gallina *) -let start_proof_and_print idopt k t hook = - start_proof_com idopt k t hook; +let start_proof_and_print k l hook = + start_proof_com k l hook; print_subgoals (); - if !pcoq <> None then (out_some !pcoq).start_proof () + if !pcoq <> None then (Option.get !pcoq).start_proof () + +let current_dirpath sec = + drop_dirpath_prefix (Lib.library_dp ()) + (if sec then Lib.cwd () + else extract_dirpath_prefix (Lib.sections_depth ()) (Lib.cwd ())) + +let dump_definition (loc, id) sec s = + Flags.dump_string (Printf.sprintf "%s %d %s %s\n" s (fst (unloc loc)) + (string_of_dirpath (current_dirpath sec)) (string_of_id id)) + +let dump_reference loc modpath ident ty = + dump_string (Printf.sprintf "R%d %s %s %s %s\n" + (fst (unloc loc)) (string_of_dirpath (Lib.library_dp ())) modpath ident ty) -let vernac_definition (local,_,_ as k) id def hook = +let dump_constraint ((loc, n), _, _) sec ty = + match n with + | Name id -> dump_definition (loc, id) sec ty + | Anonymous -> () + +let vernac_definition (local,_,_ as k) (_,id as lid) def hook = + if !Flags.dump then dump_definition lid false "def"; match def with | ProveBody (bl,t) -> (* local binders, typ *) if Lib.is_modtype () then @@ -307,7 +332,8 @@ let vernac_definition (local,_,_ as k) id def hook = (str "Proof editing mode not supported in module types") else let hook _ _ = () in - start_proof_and_print (Some id) (local,DefinitionBody Definition) (bl,t) hook + start_proof_and_print (local,DefinitionBody Definition) + [Some lid,(bl,t)] hook | DefineBody (bl,red_option,c,typ_opt) -> let red_option = match red_option with | None -> None @@ -316,7 +342,12 @@ let vernac_definition (local,_,_ as k) id def hook = Some (interp_redexp env evc r) in declare_definition id k bl red_option c typ_opt hook -let vernac_start_proof kind sopt (bl,t) lettop hook = +let vernac_start_proof kind l lettop hook = + if !Flags.dump then + List.iter (fun (id, _) -> + match id with + | Some lid -> dump_definition lid false "prf" + | None -> ()) l; if not(refining ()) then if lettop then errorlabstrm "Vernacentries.StartProof" @@ -324,12 +355,12 @@ 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 (Global, Proof kind) (bl,t) hook + start_proof_and_print (Global, Proof kind) l hook let vernac_end_proof = function | Admitted -> admit () | Proved (is_opaque,idopt) -> - if not !Options.print_emacs then if_verbose show_script (); + if not !Flags.print_emacs then if_verbose show_script (); match idopt with | None -> save_named is_opaque | Some ((_,id),None) -> save_anonymous is_opaque id @@ -348,14 +379,31 @@ let vernac_exact_proof c = 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 - -let vernac_inductive f indl = build_mutual indl f - -let vernac_fixpoint = build_recursive - -let vernac_cofixpoint = build_corecursive +let vernac_assumption kind l nl= + let global = fst kind = Global in + List.iter (fun (is_coe,(idl,c)) -> + if !dump then + List.iter (fun lid -> + if global then dump_definition lid false "ax" + else dump_definition lid true "var") idl; + declare_assumption idl is_coe kind [] c false false nl) l + +let vernac_inductive f indl = + if !dump then + List.iter (fun ((lid, _, _, cstrs), _) -> + dump_definition lid false"ind"; + List.iter (fun (_, (lid, _)) -> + dump_definition lid false "constr") cstrs) + indl; + build_mutual indl f + +let vernac_fixpoint l b = + List.iter (fun ((lid, _, _, _, _), _) -> dump_definition lid false "def") l; + build_recursive l b + +let vernac_cofixpoint l b = + List.iter (fun ((lid, _, _, _), _) -> dump_definition lid false "def") l; + build_corecursive l b let vernac_scheme = build_scheme @@ -369,7 +417,7 @@ let vernac_import export refl = List.iter import refl; Lib.add_frozen_state () -let vernac_declare_module export id binders_ast mty_ast_o = +let vernac_declare_module export (loc, 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 @@ -381,33 +429,38 @@ let vernac_declare_module export id binders_ast mty_ast_o = "Remove the \"Export\" and \"Import\" keywords from every functor " ^ "argument.") else (idl,ty)) binders_ast in - Declaremods.declare_module + let mp = Declaremods.declare_module Modintern.interp_modtype Modintern.interp_modexpr - id binders_ast (Some mty_ast_o) None; + id binders_ast (Some mty_ast_o) None + in + Modintern.dump_moddef loc mp "mod"; if_verbose message ("Module "^ string_of_id id ^" is declared"); - option_iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export + 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 = +let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_o = (* We check the state of the system (in section, in module type) and what module information is supplied *) if Lib.sections_are_opened () then error "Modules and Module Types are not allowed inside sections"; match mexpr_ast_o with | None -> + check_no_pending_proofs (); let binders_ast,argsexport = List.fold_right (fun (export,idl,ty) (args,argsexport) -> (idl,ty)::args, (List.map (fun (_,i) -> export,i)idl)@argsexport) 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") ; - List.iter - (fun (export,id) -> - option_iter - (fun export -> vernac_import export [Ident (dummy_loc,id)]) export - ) argsexport + let mp = Declaremods.start_module Modintern.interp_modtype export + id binders_ast mty_ast_o + in + Modintern.dump_moddef loc mp "mod"; + if_verbose message + ("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) -> @@ -416,37 +469,42 @@ let vernac_define_module export id binders_ast mty_ast_o mexpr_ast_o = " the definition is interactive. Remove the \"Export\" and " ^ "\"Import\" keywords from every functor argument.") else (idl,ty)) binders_ast in - Declaremods.declare_module + let mp = 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"); - option_iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) - export - -let vernac_end_module export id = - Declaremods.end_module id; + id binders_ast mty_ast_o mexpr_ast_o + in + Modintern.dump_moddef loc mp "mod"; + if_verbose message + ("Module "^ string_of_id id ^" is defined"); + Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) + export + +let vernac_end_module export (loc,id) = + let mp = Declaremods.end_module id in + Modintern.dump_modref loc mp "mod"; if_verbose message ("Module "^ string_of_id id ^" is defined") ; - option_iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export + Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export -let vernac_declare_module_type id binders_ast mty_ast_o = +let vernac_declare_module_type (loc,id) binders_ast mty_ast_o = if Lib.sections_are_opened () then error "Modules and Module Types are not allowed inside sections"; match mty_ast_o with | None -> + check_no_pending_proofs (); 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; + let mp = Declaremods.start_modtype Modintern.interp_modtype id binders_ast in + Modintern.dump_moddef loc mp "modtype"; if_verbose message ("Interactive Module Type "^ string_of_id id ^" started"); List.iter (fun (export,id) -> - option_iter + Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export ) argsexport @@ -458,25 +516,35 @@ let vernac_declare_module_type id binders_ast mty_ast_o = " 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; + let mp = Declaremods.declare_modtype Modintern.interp_modtype + id binders_ast base_mty in + Modintern.dump_moddef loc mp "modtype"; if_verbose message ("Module Type "^ string_of_id id ^" is defined") -let vernac_end_modtype id = - Declaremods.end_modtype id; +let vernac_end_modtype (loc,id) = + let mp = Declaremods.end_modtype id in + Modintern.dump_modref loc mp "modtype"; if_verbose message ("Module Type "^ string_of_id id ^" is defined") - +let vernac_include = function + | CIMTE mty_ast -> + Declaremods.declare_include Modintern.interp_modtype mty_ast false + | CIME mexpr_ast -> + Declaremods.declare_include Modintern.interp_modexpr mexpr_ast true + + + (**********************) (* Gallina extensions *) - + let vernac_record struc binders sort nameopt cfs = let const = match nameopt with | None -> add_prefix "Build_" (snd (snd struc)) - | Some (_,id) -> id in + | Some (_,id as lid) -> + if !dump then dump_definition lid false "constr"; id in let sigma = Evd.empty in let env = Global.env() in let s = interp_constr sigma env sort in @@ -485,45 +553,48 @@ let vernac_record struc binders sort nameopt cfs = | Sort s -> s | _ -> user_err_loc (constr_loc sort,"definition_structure", str "Sort expected") in - Record.definition_structure (struc,binders,cfs,const,s) + if !dump then ( + dump_definition (snd struc) false "rec"; + List.iter (fun (_, x) -> + match x with + | AssumExpr ((loc, Name id), _) -> dump_definition (loc,id) false "proj" + | _ -> ()) cfs); + ignore(Record.definition_structure (struc,binders,cfs,const,s)) (* Sections *) -let vernac_begin_section = Lib.open_section -let vernac_end_section = Lib.close_section +let vernac_begin_section (_, id as lid) = + check_no_pending_proofs (); + if !Flags.dump then dump_definition lid true "sec"; + Lib.open_section id + +let vernac_end_section (loc, id) = + if !Flags.dump then + dump_reference loc + (string_of_dirpath (current_dirpath true)) "<>" "sec"; + Lib.close_section id -let vernac_end_segment id = +let vernac_end_segment lid = check_no_pending_proofs (); 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 + | _,Lib.OpenedModule (export,_,_) -> vernac_end_module export lid + | _,Lib.OpenedModtype _ -> vernac_end_modtype lid + | _,Lib.OpenedSection _ -> vernac_end_section lid | _ -> anomaly "No more opened things" let vernac_require import _ qidl = let qidl = List.map qualid_of_reference qidl in Library.require_library qidl import -let vernac_canonical locqid = - Recordops.declare_canonical_structure (Nametab.global locqid) - -let locate_reference ref = - let (loc,qid) = qualid_of_reference ref in - try match Nametab.extended_locate qid with - | TrueGlobal ref -> ref - | SyntacticDef kn -> - match Syntax_def.search_syntactic_definition loc kn with - | Rawterm.RRef (_,ref) -> ref - | _ -> raise Not_found - with Not_found -> - error_global_not_found_loc loc qid +let vernac_canonical r = + Recordops.declare_canonical_structure (global_with_alias r) let vernac_coercion stre ref qids qidt = let target = cl_of_qualid qidt in let source = cl_of_qualid qids in - let ref' = locate_reference ref in + let ref' = global_with_alias ref in Class.try_add_new_coercion_with_target ref' stre source target; if_verbose message ((string_of_reference ref) ^ " is now a coercion") @@ -532,6 +603,24 @@ let vernac_identity_coercion stre id qids qidt = let source = cl_of_qualid qids in Class.try_add_new_identity_coercion id stre source target +(* Type classes *) +let vernac_class id par ar sup props = + if !dump then ( + dump_definition id false "class"; + List.iter (fun (lid, _, _) -> dump_definition lid false "meth") props); + Classes.new_class id par ar sup props + +let vernac_instance glob sup inst props pri = + if !dump then dump_constraint inst false "inst"; + ignore(Classes.new_instance ~global:glob sup inst props pri) + +let vernac_context l = + if !dump then List.iter (fun x -> dump_constraint x true "var") l; + Classes.context l + +let vernac_declare_instance id = + if !dump then dump_definition id false "inst"; + Classes.declare_instance false id (***********) (* Solving *) @@ -547,12 +636,12 @@ let vernac_solve n tcom b = (* in case a strict subtree was completed, go back to the top of the prooftree *) if subtree_solved () then begin - Options.if_verbose msgnl (str "Subgoal proved"); + Flags.if_verbose msgnl (str "Subgoal proved"); make_focus 0; reset_top_of_script () end; print_subgoals(); - if !pcoq <> None then (out_some !pcoq).solve n + if !pcoq <> None then (Option.get !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 @@ -664,13 +753,16 @@ let vernac_declare_tactic_definition = Tacinterp.add_tacdef let vernac_hints = Auto.add_hints -let vernac_syntactic_definition = Command.syntax_definition - -let vernac_declare_implicits local locqid = function +let vernac_syntactic_definition lid = + dump_definition lid false "syndef"; + Command.syntax_definition (snd lid) + +let vernac_declare_implicits local r = function | Some imps -> - Impargs.declare_manual_implicits local (Nametab.global locqid) imps + Impargs.declare_manual_implicits local (global_with_alias r) false + (List.map (fun (ex,b,f) -> ex, (b,f)) imps) | None -> - Impargs.declare_implicits local (Nametab.global locqid) + Impargs.declare_implicits local (global_with_alias r) let vernac_reserve idl c = let t = Constrintern.interp_type Evd.empty (Global.env()) c in @@ -709,11 +801,43 @@ let _ = let _ = declare_bool_option { optsync = true; + optname = "strong strict implicit arguments"; + optkey = (TertiaryTable ("Strongly","Strict","Implicit")); + optread = Impargs.is_strongly_strict_implicit_args; + optwrite = Impargs.make_strongly_strict_implicit_args } + +let _ = + declare_bool_option + { optsync = true; optname = "contextual implicit arguments"; optkey = (SecondaryTable ("Contextual","Implicit")); optread = Impargs.is_contextual_implicit_args; optwrite = Impargs.make_contextual_implicit_args } +(* let _ = *) +(* declare_bool_option *) +(* { optsync = true; *) +(* optname = "forceable implicit arguments"; *) +(* optkey = (SecondaryTable ("Forceable","Implicit")); *) +(* optread = Impargs.is_forceable_implicit_args; *) +(* optwrite = Impargs.make_forceable_implicit_args } *) + +let _ = + declare_bool_option + { optsync = true; + optname = "implicit arguments defensive printing"; + optkey = (TertiaryTable ("Reversible","Pattern","Implicit")); + optread = Impargs.is_reversible_pattern_implicit_args; + optwrite = Impargs.make_reversible_pattern_implicit_args } + +let _ = + declare_bool_option + { optsync = true; + optname = "maximal insertion of implicit"; + optkey = (TertiaryTable ("Maximal","Implicit","Insertion")); + optread = Impargs.is_maximal_implicit_args; + optwrite = Impargs.make_maximal_implicit_args } + let _ = declare_bool_option { optsync = true; @@ -725,6 +849,13 @@ let _ = let _ = declare_bool_option { optsync = true; + optname = "printing of existential variable instances"; + optkey = (TertiaryTable ("Printing","Existential","Instances")); + optread = (fun () -> !Constrextern.print_evar_arguments); + optwrite = (:=) Constrextern.print_evar_arguments } +let _ = + declare_bool_option + { optsync = true; optname = "implicit arguments printing"; optkey = (SecondaryTable ("Printing","Implicit")); optread = (fun () -> !Constrextern.print_implicits); @@ -733,6 +864,14 @@ let _ = let _ = declare_bool_option { optsync = true; + optname = "implicit arguments defensive printing"; + optkey = (TertiaryTable ("Printing","Implicit","Defensive")); + optread = (fun () -> !Constrextern.print_implicits_defensive); + optwrite = (fun b -> Constrextern.print_implicits_defensive := b) } + +let _ = + declare_bool_option + { optsync = true; optname = "projection printing using dot notation"; optkey = (SecondaryTable ("Printing","Projections")); optread = (fun () -> !Constrextern.print_projections); @@ -751,8 +890,8 @@ let _ = { optsync = true; optname = "raw printing"; optkey = (SecondaryTable ("Printing","All")); - optread = (fun () -> !Options.raw_print); - optwrite = (fun b -> Options.raw_print := b) } + optread = (fun () -> !Flags.raw_print); + optwrite = (fun b -> Flags.raw_print := b) } let _ = declare_bool_option @@ -767,8 +906,8 @@ let _ = { optsync = true; optname = "use of boxed definitions"; optkey = (SecondaryTable ("Boxed","Definitions")); - optread = Options.boxed_definitions; - optwrite = (fun b -> Options.set_boxed_definitions b) } + optread = Flags.boxed_definitions; + optwrite = (fun b -> Flags.set_boxed_definitions b) } let _ = declare_bool_option @@ -791,8 +930,8 @@ let _ = { optsync=false; optkey=SecondaryTable("Hyps","Limit"); optname="the hypotheses limit"; - optread=Options.print_hyps_limit; - optwrite=Options.set_print_hyps_limit } + optread=Flags.print_hyps_limit; + optwrite=Flags.set_print_hyps_limit } let _ = declare_int_option @@ -814,7 +953,7 @@ let _ = declare_bool_option { optsync=true; optkey=SecondaryTable("Printing","Universes"); - optname="the printing of universes"; + optname="printing of universes"; optread=(fun () -> !Constrextern.print_universes); optwrite=(fun b -> Constrextern.print_universes:=b) } @@ -829,15 +968,15 @@ let _ = optread=(fun () -> get_debug () <> Tactic_debug.DebugOff); optwrite=vernac_debug } -let vernac_set_opacity opaq locqid = - match Nametab.global locqid with - | ConstRef sp -> - if opaq then set_opaque_const sp - else set_transparent_const sp - | VarRef 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_opacity local str = + let glob_ref r = + match global_with_alias r with + | ConstRef sp -> EvalConstRef sp + | VarRef id -> EvalVarRef id + | _ -> error + "cannot set an inductive type or a constructor as transparent" in + let str = List.map (fun (lev,ql) -> (lev,List.map glob_ref ql)) str in + Redexpr.set_strategy local str let vernac_set_option key = function | StringValue s -> set_string_option_value key s @@ -888,13 +1027,13 @@ let vernac_check_may_eval redexp glopt rc = let j = Typeops.typing env c in match redexp with | None -> - if !pcoq <> None then (out_some !pcoq).print_check j + if !pcoq <> None then (Option.get !pcoq).print_check env j else msg (print_judgment env j) | Some r -> 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) + then (Option.get !pcoq).print_eval redfun env evmap rc j + else msg (print_eval redfun env evmap rc j) (* The same but avoiding the current goal context if any *) let vernac_global_check c = @@ -910,7 +1049,7 @@ let vernac_print = function | 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 + | PrintGrammar ent -> Metasyntax.print_grammar ent | PrintLoadPath -> (* For compatibility ? *) print_loadpath () | PrintModules -> msg (print_modules ()) | PrintModule qid -> print_module qid @@ -918,11 +1057,13 @@ let vernac_print = function | PrintMLLoadPath -> Mltop.print_ml_path () | PrintMLModules -> Mltop.print_ml_modules () | PrintName qid -> - if !pcoq <> None then (out_some !pcoq).print_name qid + if !pcoq <> None then (Option.get !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()) + | PrintTypeClasses -> ppnl (Prettyp.print_typeclasses()) + | PrintInstances c -> ppnl (Prettyp.print_instances (global c)) | PrintLtac qid -> ppnl (Tacinterp.print_ltac (snd (qualid_of_reference qid))) | PrintCoercions -> ppnl (Prettyp.print_coercions()) | PrintCoercionPaths (cls,clt) -> @@ -930,7 +1071,7 @@ let vernac_print = function | 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) + | PrintHint r -> Auto.print_hint_ref (global_with_alias r) | PrintHintGoal -> Auto.print_applicable_hint () | PrintHintDbName s -> Auto.print_hint_db_by_name s | PrintRewriteHintDbName s -> Autorewrite.print_rewrite_hintdb s @@ -944,6 +1085,11 @@ let vernac_print = function pp (Notation.pr_visibility (Constrextern.without_symbols pr_lrawconstr) s) | PrintAbout qid -> msgnl (print_about qid) | PrintImplicit qid -> msg (print_impargs qid) +(*spiwack: prints all the axioms and section variables used by a term *) + | PrintAssumptions r -> + let cstr = constr_of_global (global_with_alias r) in + let nassumptions = Environ.assumptions cstr (Global.env ()) in + msg (Printer.pr_assumptionset (Global.env ()) nassumptions) let global_module r = let (loc,qid) = qualid_of_reference r in @@ -959,12 +1105,12 @@ let interp_search_restriction = function open Search let interp_search_about_item = function - | SearchRef qid -> GlobSearchRef (Nametab.global qid) + | SearchRef r -> GlobSearchRef (global_with_alias r) | SearchString s -> GlobSearchString s let vernac_search s r = let r = interp_search_restriction r in - if !pcoq <> None then (out_some !pcoq).search s r else + if !pcoq <> None then (Option.get !pcoq).search s r else match s with | SearchPattern c -> let _,pat = interp_constrpattern Evd.empty (Global.env()) c in @@ -972,8 +1118,8 @@ let vernac_search s 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 + | SearchHead ref -> + Search.search_by_head (global_with_alias ref) r | SearchAbout sl -> Search.search_about (List.map interp_search_about_item sl) r @@ -994,7 +1140,7 @@ let vernac_goal = function | Some c -> if not (refining()) then begin let unnamed_kind = Lemma (* Arbitrary *) in - start_proof_com None (Global, Proof unnamed_kind) c (fun _ _ ->()); + start_proof_com (Global, Proof unnamed_kind) [None,c] (fun _ _ ->()); print_subgoals () end else error "repeated Goal not permitted in refining mode" @@ -1003,12 +1149,12 @@ let vernac_abort = function | None -> delete_current_proof (); if_verbose message "Current goal aborted"; - if !pcoq <> None then (out_some !pcoq).abort "" + if !pcoq <> None then (Option.get !pcoq).abort "" | Some id -> delete_proof id; let s = string_of_id (snd id) in if_verbose message ("Goal "^s^" aborted"); - if !pcoq <> None then (out_some !pcoq).abort s + if !pcoq <> None then (Option.get !pcoq).abort s let vernac_abort_all () = if refining() then begin @@ -1078,7 +1224,7 @@ let explain_tree occ = let vernac_show = function | ShowGoal nopt -> - if !pcoq <> None then (out_some !pcoq).show_goal nopt + if !pcoq <> None then (Option.get !pcoq).show_goal nopt else msg (match nopt with | None -> pr_open_subgoals () | Some n -> pr_nth_open_subgoal n) @@ -1116,7 +1262,7 @@ let vernac_check_guard () = let interp c = match c with (* Control (done in vernac) *) - | (VernacTime _ | VernacVar _ | VernacList _ | VernacLoad _) -> assert false + | (VernacTime _ | VernacList _ | VernacLoad _) -> assert false (* Syntax *) | VernacTacticNotation (n,r,e) -> Metasyntax.add_tactic_notation (n,r,e) @@ -1129,12 +1275,11 @@ let interp c = match c with | VernacNotation (local,c,infpl,sc) -> vernac_notation local c infpl sc (* Gallina *) - | VernacDefinition (k,(_,id),d,f) -> vernac_definition k id d f - | VernacStartTheoremProof (k,(_,id),t,top,f) -> - vernac_start_proof k (Some id) t top f + | VernacDefinition (k,lid,d,f) -> vernac_definition k lid d f + | VernacStartTheoremProof (k,l,top,f) -> vernac_start_proof k l top f | VernacEndProof e -> vernac_end_proof e | VernacExactProof c -> vernac_exact_proof c - | VernacAssumption (stre,l) -> vernac_assumption stre l + | VernacAssumption (stre,nl,l) -> vernac_assumption stre l nl | VernacInductive (finite,l) -> vernac_inductive finite l | VernacFixpoint (l,b) -> vernac_fixpoint l b | VernacCoFixpoint (l,b) -> vernac_cofixpoint l b @@ -1142,17 +1287,18 @@ let interp c = match c with | VernacCombinedScheme (id, l) -> vernac_combined_scheme id l (* Modules *) - | 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 - + | VernacDeclareModule (export,lid,bl,mtyo) -> + vernac_declare_module export lid bl mtyo + | VernacDefineModule (export,lid,bl,mtyo,mexpro) -> + vernac_define_module export lid bl mtyo mexpro + | VernacDeclareModuleType (lid,bl,mtyo) -> + vernac_declare_module_type lid bl mtyo + | VernacInclude (in_ast) -> + vernac_include in_ast (* Gallina extensions *) - | VernacBeginSection (_,id) -> vernac_begin_section id + | VernacBeginSection lid -> vernac_begin_section lid - | VernacEndSegment (_,id) -> vernac_end_segment id + | VernacEndSegment lid -> vernac_end_segment lid | VernacRecord (_,id,bl,s,idopt,fs) -> vernac_record id bl s idopt fs | VernacRequire (export,spec,qidl) -> vernac_require export spec qidl @@ -1161,6 +1307,13 @@ let interp c = match c with | VernacCoercion (str,r,s,t) -> vernac_coercion str r s t | VernacIdentityCoercion (str,(_,id),s,t) -> vernac_identity_coercion str id s t + (* Type classes *) + | VernacClass (id, par, ar, sup, props) -> vernac_class id par ar sup props + + | VernacInstance (glob, sup, inst, props, pri) -> vernac_instance glob sup inst props pri + | VernacContext sup -> vernac_context sup + | VernacDeclareInstance id -> vernac_declare_instance id + (* Solving *) | VernacSolve (n,tac,b) -> vernac_solve n tac b | VernacSolveExistential (n,c) -> vernac_solve_existential n c @@ -1186,6 +1339,7 @@ let interp c = match c with | VernacRestoreState s -> vernac_restore_state s (* Resetting *) + | VernacRemoveName id -> Lib.remove_name id | VernacResetName id -> vernac_reset_name id | VernacResetInitial -> vernac_reset_initial () | VernacBack n -> vernac_back n @@ -1197,7 +1351,7 @@ let interp c = match c with | VernacSyntacticDefinition (id,c,l,b) ->vernac_syntactic_definition id c l b | VernacDeclareImplicits (local,qid,l) ->vernac_declare_implicits local qid l | VernacReserve (idl,c) -> vernac_reserve idl c - | VernacSetOpacity (opaq, qidl) -> List.iter (vernac_set_opacity opaq) qidl + | VernacSetOpacity (local,qidl) -> vernac_set_opacity local qidl | VernacSetOption (key,v) -> vernac_set_option key v | VernacUnsetOption key -> vernac_unset_option key | VernacRemoveOption (key,v) -> vernac_remove_option key v @@ -1213,13 +1367,14 @@ let interp c = match c with | VernacNop -> () (* Proof management *) - | VernacGoal t -> vernac_start_proof Theorem None ([],t) false (fun _ _ ->()) + | VernacGoal t -> vernac_start_proof Theorem [None,([],t)] false (fun _ _->()) | 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 + | VernacUndoTo n -> undo_todepth n | VernacBacktrack (snum,pnum,naborts) -> vernac_backtrack snum pnum naborts | VernacFocus n -> vernac_focus n | VernacUnfocus -> vernac_unfocus () |