diff options
| author |  Stephane Glondu <steph@glondu.net> | 2012-01-12 16:02:20 +0100 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:02:20 +0100 |
| commit | 97fefe1fcca363a1317e066e7f4b99b9c1e9987b (patch) | |
| tree | 97ec6b7d831cc5fb66328b0c63a11db1cbb2f158 /toplevel | |
| parent | 300293c119981054c95182a90c829058530a6b6f (diff) | |
Imported Upstream version 8.4~betaupstream/8.4_beta
Diffstat (limited to 'toplevel')
55 files changed, 2754 insertions, 1410 deletions
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 16ceffed..f4dab15f 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: auto_ind_decl.ml 14641 2011-11-06 11:59:10Z herbelin $ i*) - (* This file is about the automatic generation of schemes about decidable equality, created by Vincent Siles, Oct 2007 *) @@ -79,6 +77,25 @@ let sumbool = Coqlib.build_coq_sumbool let andb = fun _ -> (Coqlib.build_bool_type()).Coqlib.andb +let induct_on c = + new_induct false + [Tacexpr.ElimOnConstr (Evd.empty,(c,Glob_term.NoBindings))] + None (None,None) None + +let destruct_on_using c id = + new_destruct false + [Tacexpr.ElimOnConstr (Evd.empty,(c,Glob_term.NoBindings))] + None + (None,Some (dl,Genarg.IntroOrAndPattern [ + [dl,Genarg.IntroAnonymous]; + [dl,Genarg.IntroIdentifier id]])) + None + +let destruct_on c = + new_destruct false + [Tacexpr.ElimOnConstr (Evd.empty,(c,Glob_term.NoBindings))] + None (None,None) None + (* reconstruct the inductive with the correct deBruijn indexes *) let mkFullInd ind n = let mib = Global.lookup_mind (fst ind) in @@ -329,13 +346,12 @@ let do_replace_lb lb_scheme_key aavoid narg gls p q = with Not_found -> (* spiwack: the format of this error message should probably be improved. *) - let err_msg = msg_with Format.str_formatter + let err_msg = string_of_ppcmds (str "Leibniz->boolean:" ++ str "You have to declare the" ++ str "decidability over " ++ Printer.pr_constr type_of_pq ++ - str " first."); - Format.flush_str_formatter () + str " first.") in error err_msg in let lb_args = Array.append (Array.append @@ -387,13 +403,12 @@ let do_replace_bl bl_scheme_key ind gls aavoid narg lft rgt = with Not_found -> (* spiwack: the format of this error message should probably be improved. *) - let err_msg = msg_with Format.str_formatter + let err_msg = string_of_ppcmds (str "boolean->Leibniz:" ++ str "You have to declare the" ++ str "decidability over " ++ Printer.pr_constr tt1 ++ - str " first."); - Format.flush_str_formatter () + str " first.") in error err_msg in let bl_args = @@ -513,17 +528,9 @@ let compute_bl_tact bl_scheme_key ind lnamesparrec nparrec gsig = avoid := freshz::(!avoid); tclTHENSEQ [ intros_using fresh_first_intros; intro_using freshn ; - new_induct false [ (Tacexpr.ElimOnConstr ((mkVar freshn), - Rawterm.NoBindings))] - None - (None,None) - None; + induct_on (mkVar freshn); intro_using freshm; - new_destruct false [ (Tacexpr.ElimOnConstr ((mkVar freshm), - Rawterm.NoBindings))] - None - (None,None) - None; + destruct_on (mkVar freshm); intro_using freshz; intros; tclTRY ( @@ -541,7 +548,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). in avoid := fresht::(!avoid); (new_destruct false [Tacexpr.ElimOnConstr - ((mkVar freshz,Rawterm.NoBindings))] + (Evd.empty,((mkVar freshz,Glob_term.NoBindings)))] None (None, Some (dl,Genarg.IntroOrAndPattern [[ dl,Genarg.IntroIdentifier fresht; @@ -551,7 +558,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). Ci a1 ... an = Ci b1 ... bn replace bi with ai; auto || replace bi with ai by apply typeofbi_prod ; auto *) - fun gls-> let gl = (gls.Evd.it).Evd.evar_concl in + fun gls-> let gl = pf_concl gls in match (kind_of_term gl) with | App (c,ca) -> ( match (kind_of_term c) with @@ -583,7 +590,7 @@ let make_bl_scheme mind = let nparrec = mib.mind_nparams_rec in let lnonparrec,lnamesparrec = context_chop (nparams-nparrec) mib.mind_params_ctxt in - [|Pfedit.build_by_tactic + [|Pfedit.build_by_tactic (Global.env()) (compute_bl_goal ind lnamesparrec nparrec) (compute_bl_tact (!bl_scheme_kind_aux()) ind lnamesparrec nparrec)|] @@ -651,30 +658,22 @@ let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec gsig = avoid := freshz::(!avoid); tclTHENSEQ [ intros_using fresh_first_intros; intro_using freshn ; - new_induct false [Tacexpr.ElimOnConstr - ((mkVar freshn),Rawterm.NoBindings)] - None - (None,None) - None; + induct_on (mkVar freshn); intro_using freshm; - new_destruct false [Tacexpr.ElimOnConstr - ((mkVar freshm),Rawterm.NoBindings)] - None - (None,None) - None; + destruct_on (mkVar freshm); intro_using freshz; intros; tclTRY ( tclORELSE reflexivity (Equality.discr_tac false None) ); - Equality.inj [] false (mkVar freshz,Rawterm.NoBindings); + Equality.inj [] false (mkVar freshz,Glob_term.NoBindings); intros; simpl_in_concl; Auto.default_auto; tclREPEAT ( tclTHENSEQ [apply (andb_true_intro()); simplest_split ;Auto.default_auto ] ); - fun gls -> let gl = (gls.Evd.it).Evd.evar_concl in + fun gls -> let gl = pf_concl gls in (* assume the goal to be eq (eq_type ...) = true *) match (kind_of_term gl) with | App(c,ca) -> (match (kind_of_term ca.(1)) with @@ -703,7 +702,7 @@ let make_lb_scheme mind = let nparrec = mib.mind_nparams_rec in let lnonparrec,lnamesparrec = context_chop (nparams-nparrec) mib.mind_params_ctxt in - [|Pfedit.build_by_tactic + [|Pfedit.build_by_tactic (Global.env()) (compute_lb_goal ind lnamesparrec nparrec) (compute_lb_tact (!lb_scheme_kind_aux()) ind lnamesparrec nparrec)|] @@ -810,24 +809,11 @@ let compute_dec_tact ind lnamesparrec nparrec gsig = assert_by (Name freshH) ( mkApp(sumbool(),[|eqtrue eqbnm; eqfalse eqbnm|]) ) - (tclTHEN - (new_destruct false [Tacexpr.ElimOnConstr - (eqbnm,Rawterm.NoBindings)] - None - (None,None) - None) - Auto.default_auto); + (tclTHEN (destruct_on eqbnm) Auto.default_auto); (fun gsig -> let freshH2 = fresh_id (!avoid) (id_of_string "H") gsig in avoid := freshH2::(!avoid); - tclTHENS ( - new_destruct false [Tacexpr.ElimOnConstr - ((mkVar freshH),Rawterm.NoBindings)] - None - (None,Some (dl,Genarg.IntroOrAndPattern [ - [dl,Genarg.IntroAnonymous]; - [dl,Genarg.IntroIdentifier freshH2]])) None - ) [ + tclTHENS (destruct_on_using (mkVar freshH) freshH2) [ (* left *) tclTHENSEQ [ simplest_left; @@ -850,10 +836,10 @@ let compute_dec_tact ind lnamesparrec nparrec gsig = Auto.default_auto ]); Equality.general_rewrite_bindings_in true - all_occurrences false + all_occurrences true false (List.hd !avoid) ((mkVar (List.hd (List.tl !avoid))), - Rawterm.NoBindings + Glob_term.NoBindings ) true; Equality.discr_tac false None @@ -870,7 +856,7 @@ let make_eq_decidability mind = let nparrec = mib.mind_nparams_rec in let lnonparrec,lnamesparrec = context_chop (nparams-nparrec) mib.mind_params_ctxt in - [|Pfedit.build_by_tactic + [|Pfedit.build_by_tactic (Global.env()) (compute_dec_goal ind lnamesparrec nparrec) (compute_dec_tact ind lnamesparrec nparrec)|] diff --git a/toplevel/auto_ind_decl.mli b/toplevel/auto_ind_decl.mli index c791da28..076a946a 100644 --- a/toplevel/auto_ind_decl.mli +++ b/toplevel/auto_ind_decl.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -14,7 +14,12 @@ open Sign open Proof_type open Ind_tables -(* Build boolean equality of a block of mutual inductive types *) +(** This file is about the automatic generation of schemes about + decidable equality, + @author Vincent Siles + Oct 2007 *) + +(** {6 Build boolean equality of a block of mutual inductive types } *) exception EqNotFound of inductive * inductive exception EqUnknown of string @@ -27,7 +32,7 @@ exception NonSingletonProp of inductive val beq_scheme_kind : mutual scheme_kind val build_beq_scheme : mutual_inductive -> constr array -(* Build equivalence between boolean equality and Leibniz equality *) +(** {6 Build equivalence between boolean equality and Leibniz equality } *) val lb_scheme_kind : mutual scheme_kind val make_lb_scheme : mutual_inductive -> constr array @@ -35,7 +40,7 @@ val make_lb_scheme : mutual_inductive -> constr array val bl_scheme_kind : mutual scheme_kind val make_bl_scheme : mutual_inductive -> constr array -(* Build decidability of equality *) +(** {6 Build decidability of equality } *) val eq_dec_scheme_kind : mutual scheme_kind val make_eq_decidability : mutual_inductive -> constr array diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml index 4a67ede4..9258a39f 100644 --- a/toplevel/autoinstance.ml +++ b/toplevel/autoinstance.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id:$ *) - (*i*) open Pp open Printer @@ -181,8 +179,10 @@ let declare_record_instance gr ctx params = let ident = make_instance_ident gr in let def = it_mkLambda_or_LetIn (applistc (constr_of_global gr) params) ctx in let def = deep_refresh_universes def in - let ce = { const_entry_body=def; const_entry_type=None; - const_entry_opaque=false; const_entry_boxed=false } in + let ce = { const_entry_body= def; + const_entry_secctx = None; + const_entry_type=None; + const_entry_opaque=false } in let cst = Declare.declare_constant ident (DefinitionEntry ce,Decl_kinds.IsDefinition Decl_kinds.StructureComponent) in new_instance_message ident (Typeops.type_of_constant (Global.env()) cst) def @@ -195,14 +195,16 @@ let declare_class_instance gr ctx params = let def = deep_refresh_universes def in let typ = deep_refresh_universes typ in let ce = Entries.DefinitionEntry - { const_entry_type=Some typ; const_entry_body=def; - const_entry_opaque=false; const_entry_boxed=false } in + { const_entry_type = Some typ; + const_entry_secctx = None; + const_entry_body= def; + const_entry_opaque=false } in try let cst = Declare.declare_constant ident (ce,Decl_kinds.IsDefinition Decl_kinds.Instance) in Typeclasses.add_instance (Typeclasses.new_instance cl (Some 100) true (ConstRef cst)); new_instance_message ident typ def - with e -> msgnl (str"Error defining instance := "++pr_constr def++str" : "++pr_constr typ++str" "++Cerrors.explain_exn e) + with e -> msgnl (str"Error defining instance := "++pr_constr def++str" : "++pr_constr typ++str" "++Errors.print e) let rec iter_under_prod (f:rel_context->constr->unit) (ctx:rel_context) t = f ctx t; match kind_of_term t with @@ -255,7 +257,7 @@ let gen_sort_topo l evm = (* register real typeclass instance given a totally defined evd *) let declare_instance (k:global_reference -> rel_context -> constr list -> unit) (cl,gen,evm:signature) = - let evm = Evarutil.nf_evars evm in + let evm = Evarutil.nf_evar_map evm in let gen = gen_sort_topo gen evm in let (evm,gen) = List.fold_right (fun ev (evm,gen) -> @@ -310,6 +312,7 @@ let end_autoinstance () = let _ = Goptions.declare_bool_option { Goptions.optsync=true; + Goptions.optdepr=false; Goptions.optkey=["Autoinstance"]; Goptions.optname="automatic typeclass instance recognition"; Goptions.optread=(fun () -> !autoinstance_opt); diff --git a/toplevel/autoinstance.mli b/toplevel/autoinstance.mli index b9b1e3c2..dd50cda5 100644 --- a/toplevel/autoinstance.mli +++ b/toplevel/autoinstance.mli @@ -1,38 +1,34 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id:$ *) - -(*i*) open Term open Libnames open Typeclasses open Names open Evd open Sign -(*i*) -(*s Automatic detection of (some) record instances *) +(** {6 Automatic detection of (some) record instances } *) -(* What to do if we find an instance. Passed are : the reference +(** What to do if we find an instance. Passed are : the reference * representing the record/class (definition or constructor) *) type instance_decl_function = global_reference -> rel_context -> constr list -> unit -(* [search_declaration gr] Search in the library if the (new) +(** [search_declaration gr] Search in the library if the (new) * declaration gr can form an instance of a registered record/class *) val search_declaration : global_reference -> unit -(* [search_record declf gr evm] Search the library for instances of +(** [search_record declf gr evm] Search the library for instances of the (new) record/class declaration [gr], and register them using [declf]. [evm] is the signature of the record (to avoid recomputing it) *) val search_record : instance_decl_function -> global_reference -> evar_map -> unit -(* Instance declaration for both scenarios *) +(** Instance declaration for both scenarios *) val declare_record_instance : instance_decl_function val declare_class_instance : instance_decl_function diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index 86057b4b..5f2c3dbb 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -1,20 +1,18 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: cerrors.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - +open Compat open Pp open Util open Indtypes open Type_errors open Pretype_errors open Indrec -open Lexer let print_loc loc = if loc = dummy_loc then @@ -25,86 +23,37 @@ let print_loc loc = let guill s = "\""^s^"\"" -let where s = - if !Flags.debug then (str"in " ++ str s ++ str":" ++ spc ()) else (mt ()) exception EvaluatedError of std_ppcmds * exn option -(* assumption : explain_sys_exn does NOT end with a 'FNL anymore! *) - -let rec explain_exn_default_aux anomaly_string report_fn = function - | Stream.Failure -> - hov 0 (anomaly_string () ++ str "uncaught Stream.Failure.") - | Stream.Error txt -> - hov 0 (str "Syntax error: " ++ str txt ++ str ".") - | Token.Error txt -> - hov 0 (str "Syntax error: " ++ str txt ++ str ".") - | Sys_error msg -> - hov 0 (anomaly_string () ++ str "uncaught exception Sys_error " ++ str (guill msg) ++ report_fn ()) - | UserError(s,pps) -> - hov 0 (str "Error: " ++ where s ++ pps) - | Out_of_memory -> - hov 0 (str "Out of memory.") - | Stack_overflow -> - hov 0 (str "Stack overflow.") - | Timeout -> - hov 0 (str "Timeout!") - | Anomaly (s,pps) -> - hov 0 (anomaly_string () ++ where s ++ pps ++ report_fn ()) - | AnomalyOnError (s,exc) -> - hov 0 (anomaly_string () ++ str s ++ str ". Received exception is:" ++ - fnl() ++ explain_exn_default_aux anomaly_string report_fn exc) - | Match_failure(filename,pos1,pos2) -> - hov 0 (anomaly_string () ++ str "Match failure in file " ++ str (guill filename) ++ - if Sys.ocaml_version = "3.06" then - (str " from character " ++ int pos1 ++ - str " to " ++ int pos2) - else - (str " at line " ++ int pos1 ++ - str " character " ++ int pos2) - ++ report_fn ()) - | Not_found -> - hov 0 (anomaly_string () ++ str "uncaught exception Not_found" ++ report_fn ()) - | Failure s -> - hov 0 (anomaly_string () ++ str "uncaught exception Failure " ++ str (guill s) ++ report_fn ()) - | Invalid_argument s -> - hov 0 (anomaly_string () ++ str "uncaught exception Invalid_argument " ++ str (guill s) ++ report_fn ()) - | Sys.Break -> - hov 0 (fnl () ++ str "User interrupt.") - | Lexer.Error Illegal_character -> - hov 0 (str "Syntax error: Illegal character.") - | Lexer.Error Unterminated_comment -> - hov 0 (str "Syntax error: Unterminated comment.") - | Lexer.Error Unterminated_string -> - hov 0 (str "Syntax error: Unterminated string.") - | Lexer.Error Undefined_token -> - hov 0 (str "Syntax error: Undefined token.") - | Lexer.Error (Bad_token s) -> - hov 0 (str "Syntax error: Bad token" ++ spc () ++ str s ++ str ".") - | Stdpp.Exc_located (loc,exc) -> +(** Registration of generic errors + Nota: explain_exn does NOT end with a newline anymore! +*) + +let explain_exn_default = function + (* Basic interaction exceptions *) + | Stream.Error txt -> hov 0 (str ("Syntax error: " ^ txt ^ ".")) + | Token.Error txt -> hov 0 (str ("Syntax error: " ^ txt ^ ".")) + | Lexer.Error.E err -> hov 0 (str (Lexer.Error.to_string err)) + | Sys_error msg -> hov 0 (str ("System error: " ^ guill msg)) + | Out_of_memory -> hov 0 (str "Out of memory.") + | Stack_overflow -> hov 0 (str "Stack overflow.") + | Timeout -> hov 0 (str "Timeout!") + | Sys.Break -> hov 0 (fnl () ++ str "User interrupt.") + (* Meta-exceptions *) + | Loc.Exc_located (loc,exc) -> hov 0 ((if loc = dummy_loc then (mt ()) else (str"At location " ++ print_loc loc ++ str":" ++ fnl ())) - ++ explain_exn_default_aux anomaly_string report_fn exc) - | Assert_failure (s,b,e) -> - hov 0 (anomaly_string () ++ str "assert failure" ++ spc () ++ - (if s <> "" then - if Sys.ocaml_version = "3.06" then - (str ("(file \"" ^ s ^ "\", characters ") ++ - int b ++ str "-" ++ int e ++ str ")") - else - (str ("(file \"" ^ s ^ "\", line ") ++ int b ++ - str ", characters " ++ int e ++ str "-" ++ - int (e+6) ++ str ")") - else - (mt ())) ++ - report_fn ()) - | EvaluatedError (msg,None) -> - msg - | EvaluatedError (msg,Some reraise) -> - msg ++ explain_exn_default_aux anomaly_string report_fn reraise - | reraise -> - hov 0 (anomaly_string () ++ str "Uncaught exception " ++ - str (Printexc.to_string reraise) ++ report_fn ()) + ++ Errors.print_no_anomaly exc) + | EvaluatedError (msg,None) -> msg + | EvaluatedError (msg,Some reraise) -> msg ++ Errors.print_no_anomaly reraise + (* Otherwise, not handled here *) + | _ -> raise Errors.Unhandled + +let _ = Errors.register_handler explain_exn_default + + +(** Pre-explain a vernac interpretation error *) let wrap_vernac_error strm = EvaluatedError (hov 0 (str "Error:" ++ spc () ++ strm), None) @@ -120,13 +69,17 @@ let rec process_vernac_interp_error = function mt() in wrap_vernac_error (str "Universe inconsistency" ++ msg ++ str ".") | TypeError(ctx,te) -> - wrap_vernac_error (Himsg.explain_type_error ctx te) - | PretypeError(ctx,te) -> - wrap_vernac_error (Himsg.explain_pretype_error ctx te) + wrap_vernac_error (Himsg.explain_type_error ctx Evd.empty te) + | PretypeError(ctx,sigma,te) -> + wrap_vernac_error (Himsg.explain_pretype_error ctx sigma te) | Typeclasses_errors.TypeClassError(env, te) -> wrap_vernac_error (Himsg.explain_typeclass_error env te) | InductiveError e -> wrap_vernac_error (Himsg.explain_inductive_error e) + | Modops.ModuleTypingError e -> + wrap_vernac_error (Himsg.explain_module_error e) + | Modintern.ModuleInternalizationError e -> + wrap_vernac_error (Himsg.explain_module_internalization_error e) | RecursionSchemeError e -> wrap_vernac_error (Himsg.explain_recursion_scheme_error e) | Cases.PatternMatchingError (env,e) -> @@ -145,10 +98,10 @@ let rec process_vernac_interp_error = function (str "No constant of this name:" ++ spc () ++ Libnames.pr_qualid q ++ str ".") | Refiner.FailError (i,s) -> - EvaluatedError (hov 0 (str "Error: Tactic failure" ++ - (if Lazy.force s <> mt() then str ":" ++ Lazy.force s else mt ()) ++ - if i=0 then str "." else str " (level " ++ int i ++ str")."), - None) + wrap_vernac_error + (str "Tactic failure" ++ + (if Lazy.force s <> mt() then str ":" ++ Lazy.force s else mt ()) ++ + if i=0 then str "." else str " (level " ++ int i ++ str").") | AlreadyDeclared msg -> wrap_vernac_error (msg ++ str ".") | Proof_type.LtacLocated (_,(Refiner.FailError (i,s) as exc)) when Lazy.force s <> mt () -> @@ -156,32 +109,13 @@ let rec process_vernac_interp_error = function | Proof_type.LtacLocated (s,exc) -> EvaluatedError (hov 0 (Himsg.explain_ltac_call_trace s ++ fnl()), Some (process_vernac_interp_error exc)) - | Stdpp.Exc_located (loc,exc) -> - Stdpp.Exc_located (loc,process_vernac_interp_error exc) + | Loc.Exc_located (loc,exc) -> + Loc.Exc_located (loc,process_vernac_interp_error exc) | exc -> exc -let anomaly_string () = str "Anomaly: " - -let report () = (str "." ++ spc () ++ str "Please report.") - -let explain_exn_default = - explain_exn_default_aux anomaly_string report - -let raise_if_debug e = - if !Flags.debug then raise e - let _ = Tactic_debug.explain_logic_error := - (fun e -> explain_exn_default (process_vernac_interp_error e)) + (fun e -> Errors.print (process_vernac_interp_error e)) let _ = Tactic_debug.explain_logic_error_no_anomaly := - (fun e -> - explain_exn_default_aux (fun () -> mt()) (fun () -> str ".") - (process_vernac_interp_error e)) - -let explain_exn_function = ref explain_exn_default - -let explain_exn e = !explain_exn_function e - -let explain_exn_no_anomaly e = - explain_exn_default_aux (fun () -> raise e) mt e + (fun e -> Errors.print_no_report (process_vernac_interp_error e)) diff --git a/toplevel/cerrors.mli b/toplevel/cerrors.mli index e1f7c035..da9d3590 100644 --- a/toplevel/cerrors.mli +++ b/toplevel/cerrors.mli @@ -1,35 +1,24 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: cerrors.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(*i*) open Pp open Util -(*i*) -(* Error report. *) +(** Error report. *) val print_loc : loc -> std_ppcmds -val explain_exn : exn -> std_ppcmds - -(** Precompute errors raised during vernac interpretation *) - -val explain_exn_no_anomaly : exn -> std_ppcmds - (** Pre-explain a vernac interpretation error *) val process_vernac_interp_error : exn -> exn -(** For debugging purpose (?), the explain function can be twicked *) +(** General explain function. Should not be used directly now, + see instead function [Errors.print] and variants *) -val explain_exn_function : (exn -> std_ppcmds) ref val explain_exn_default : exn -> std_ppcmds -val raise_if_debug : exn -> unit diff --git a/toplevel/class.ml b/toplevel/class.ml index 09ce84e0..ebaa19b6 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: class.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - open Util open Pp open Names @@ -94,7 +92,9 @@ let check_target clt = function let uniform_cond nargs lt = let rec aux = function | (0,[]) -> true - | (n,t::l) -> (strip_outer_cast t = mkRel n) & (aux ((n-1),l)) + | (n,t::l) -> + let t = strip_outer_cast t in + isRel t && destRel t = n && aux ((n-1),l) | _ -> false in aux (nargs,lt) @@ -126,7 +126,7 @@ let get_source lp source = let (cl1,lv1) = match lp with | [] -> raise Not_found - | t1::_ -> find_class_type (Global.env()) Evd.empty t1 + | t1::_ -> find_class_type Evd.empty t1 in (cl1,lv1,1) | Some cl -> @@ -134,7 +134,7 @@ let get_source lp source = | [] -> raise Not_found | t1::lt -> try - let cl1,lv1 = find_class_type (Global.env()) Evd.empty t1 in + let cl1,lv1 = find_class_type Evd.empty t1 in if cl = cl1 then cl1,lv1,(List.length lt+1) else raise Not_found with Not_found -> aux lt @@ -144,7 +144,7 @@ let get_target t ind = if (ind > 1) then CL_FUN else - fst (find_class_type (Global.env()) Evd.empty t) + fst (find_class_type Evd.empty t) let prods_of t = let rec aux acc d = match kind_of_term d with @@ -212,16 +212,16 @@ let build_id_coercion idf_opt source = match idf_opt with | Some idf -> idf | None -> - let cl,_ = find_class_type (Global.env()) Evd.empty t in + let cl,_ = find_class_type Evd.empty t in id_of_string ("Id_"^(ident_key_of_class source)^"_"^ (ident_key_of_class cl)) in let constr_entry = (* Cast is necessary to express [val_f] is identity *) DefinitionEntry { const_entry_body = mkCast (val_f, DEFAULTcast, typ_f); + const_entry_secctx = None; const_entry_type = Some typ_f; - const_entry_opaque = false; - const_entry_boxed = Flags.boxed_definitions()} in + const_entry_opaque = false } in let kn = declare_constant idf (constr_entry,IsDefinition IdentityCoercion) in ConstRef kn @@ -266,7 +266,7 @@ let add_new_coercion_core coef stre source target isid = check_arity cls; check_arity clt; let stre' = get_strength stre coef cls clt in - declare_coercion coef stre' isid cls clt (List.length lvs) + declare_coercion coef stre' ~isid ~src:cls ~target:clt ~params:(List.length lvs) let try_add_new_coercion_core ref b c d e = try add_new_coercion_core ref b c d e diff --git a/toplevel/class.mli b/toplevel/class.mli index b05f38e7..2cc8c453 100644 --- a/toplevel/class.mli +++ b/toplevel/class.mli @@ -1,14 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: class.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(*i*) open Names open Term open Classops @@ -16,31 +13,30 @@ open Declare open Libnames open Decl_kinds open Nametab -(*i*) -(* Classes and coercions. *) +(** Classes and coercions. *) -(* [try_add_new_coercion_with_target ref s src tg] declares [ref] as a coercion +(** [try_add_new_coercion_with_target ref s src tg] declares [ref] as a coercion from [src] to [tg] *) val try_add_new_coercion_with_target : global_reference -> locality -> source:cl_typ -> target:cl_typ -> unit -(* [try_add_new_coercion ref s] declares [ref], assumed to be of type +(** [try_add_new_coercion ref s] declares [ref], assumed to be of type [(x1:T1)...(xn:Tn)src->tg], as a coercion from [src] to [tg] *) val try_add_new_coercion : global_reference -> locality -> unit -(* [try_add_new_coercion_subclass cst s] expects that [cst] denotes a +(** [try_add_new_coercion_subclass cst s] expects that [cst] denotes a transparent constant which unfolds to some class [tg]; it declares an identity coercion from [cst] to [tg], named something like ["Id_cst_tg"] *) val try_add_new_coercion_subclass : cl_typ -> locality -> unit -(* [try_add_new_coercion_with_source ref s src] declares [ref] as a coercion +(** [try_add_new_coercion_with_source ref s src] declares [ref] as a coercion from [src] to [tg] where the target is inferred from the type of [ref] *) val try_add_new_coercion_with_source : global_reference -> locality -> source:cl_typ -> unit -(* [try_add_new_identity_coercion id s src tg] enriches the +(** [try_add_new_identity_coercion id s src tg] enriches the environment with a new definition of name [id] declared as an identity coercion from [src] to [tg] *) val try_add_new_identity_coercion : identifier -> locality -> diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 28c1ab75..1e83e4b8 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -1,19 +1,15 @@ -(* -*- compile-command: "make -C .. bin/coqtop.byte" -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: classes.ml 14641 2011-11-06 11:59:10Z herbelin $ i*) - (*i*) open Names open Decl_kinds open Term -open Termops open Sign open Entries open Evd @@ -25,7 +21,7 @@ open Typeclasses_errors open Typeclasses open Libnames open Constrintern -open Rawterm +open Glob_term open Topconstr (*i*) @@ -34,18 +30,21 @@ open Entries let typeclasses_db = "typeclass_instances" -let set_typeclass_transparency c b = - Auto.add_hints false [typeclasses_db] +let set_typeclass_transparency c local b = + Auto.add_hints local [typeclasses_db] (Auto.HintsTransparencyEntry ([c], b)) let _ = Typeclasses.register_add_instance_hint - (fun inst pri -> + (fun inst local pri -> + let path = try Auto.PathHints [global_of_constr inst] with _ -> Auto.PathAny in Flags.silently (fun () -> - Auto.add_hints false [typeclasses_db] + Auto.add_hints local [typeclasses_db] (Auto.HintsResolveEntry - [pri, false, constr_of_global inst])) ()); - Typeclasses.register_set_typeclass_transparency set_typeclass_transparency + [pri, false, path, inst])) ()); + Typeclasses.register_set_typeclass_transparency set_typeclass_transparency; + Typeclasses.register_classes_transparent_state + (fun () -> Auto.Hint_db.transparent_state (Auto.searchtable_map typeclasses_db)) let declare_class g = match global g with @@ -54,12 +53,13 @@ let declare_class g = | _ -> user_err_loc (loc_of_reference g, "declare_class", Pp.str"Unsupported class type, only constants and inductives are allowed") -let declare_instance glob g = +(** TODO: add subinstances *) +let existing_instance glob g = let c = global g in let instance = Typing.type_of (Global.env ()) Evd.empty (constr_of_global c) in let _, r = decompose_prod_assum instance in match class_of_constr r with - | Some tc -> add_instance (new_instance tc None glob c) + | Some (_, (tc, _)) -> add_instance (new_instance tc None glob c) | None -> user_err_loc (loc_of_reference g, "declare_instance", Pp.str "Constant does not build instances of a declared type class.") @@ -68,13 +68,6 @@ let mismatched_props env n m = mismatched_ctx_inst env Properties n m type binder_list = (identifier located * bool * constr_expr) list -(* Calls to interpretation functions. *) - -let interp_type_evars evdref env ?(impls=empty_internalization_env) typ = - let typ' = intern_gen true ~impls !evdref env typ in - let imps = Implicit_quantifiers.implicits_of_rawterm typ' in - imps, Pretyping.Default.understand_tcc_evars evdref env Pretyping.IsType typ' - (* Declare everything in the parameters as implicit, and the class instance as well *) open Topconstr @@ -108,19 +101,18 @@ open Pp let ($$) g f = fun x -> g (f x) let instance_hook k pri global imps ?hook cst = - let inst = Typeclasses.new_instance k pri global cst in - Impargs.maybe_declare_manual_implicits false cst ~enriching:false imps; - Typeclasses.add_instance inst; - (match hook with Some h -> h cst | None -> ()) + Impargs.maybe_declare_manual_implicits false cst ~enriching:false imps; + Typeclasses.declare_instance pri (not global) cst; + (match hook with Some h -> h cst | None -> ()) let declare_instance_constant k pri global imps ?hook id term termtype = let cdecl = let kind = IsDefinition Instance in let entry = { const_entry_body = term; + const_entry_secctx = None; const_entry_type = Some termtype; - const_entry_opaque = false; - const_entry_boxed = false } + const_entry_opaque = false } in DefinitionEntry entry, kind in let kn = Declare.declare_constant id cdecl in @@ -148,8 +140,8 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props in let tclass = if generalize then CGeneralization (dummy_loc, Implicit, Some AbsPi, tclass) else tclass in let k, cty, ctx', ctx, len, imps, subst = - let (env', ctx), imps = interp_context_evars evars env ctx in - let c', imps' = interp_type_evars_impls ~evdref:evars ~fail_evar:false env' tclass in + let impls, ((env', ctx), imps) = interp_context_evars evars env ctx in + let c', imps' = interp_type_evars_impls ~impls ~evdref:evars ~fail_evar:false env' tclass in let len = List.length ctx in let imps = imps @ Impargs.lift_implicits len imps' in let ctx', c = decompose_prod_assum c' in @@ -190,26 +182,29 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props Evarutil.nf_evar !evars t in Evarutil.check_evars env Evd.empty !evars termtype; - let cst = Declare.declare_internal_constant id - (Entries.ParameterEntry (termtype,false), Decl_kinds.IsAssumption Decl_kinds.Logical) - in instance_hook k None false imps ?hook (ConstRef cst); id + let cst = Declare.declare_constant ~internal:Declare.KernelSilent id + (Entries.ParameterEntry + (None,termtype,None), Decl_kinds.IsAssumption Decl_kinds.Logical) + in instance_hook k None global imps ?hook (ConstRef cst); id end else begin let props = match props with - | CRecord (loc, _, fs) -> + | Some (CRecord (loc, _, fs)) -> if List.length fs > List.length k.cl_props then mismatched_props env' (List.map snd fs) k.cl_props; - Inl fs - | _ -> Inr props + Some (Inl fs) + | Some t -> Some (Inr t) + | None -> None in let subst = match props with - | Inr term -> + | None -> if k.cl_props = [] then Some (Inl subst) else None + | Some (Inr term) -> let c = interp_casted_constr_evars evars env' term cty in - Inr (c, subst) - | Inl props -> + Some (Inr (c, subst)) + | Some (Inl props) -> let get_id = function | Ident id' -> id' @@ -223,7 +218,10 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props let (loc_mid, c) = List.find (fun (id', _) -> Name (snd (get_id id')) = id) rest in let rest' = List.filter (fun (id', _) -> Name (snd (get_id id')) <> id) rest in let (loc, mid) = get_id loc_mid in - Option.iter (fun x -> Dumpglob.add_glob loc (ConstRef x)) (List.assoc mid k.cl_projs); + List.iter (fun (n, _, x) -> + if n = Name mid then + Option.iter (fun x -> Dumpglob.add_glob loc (ConstRef x)) x) + k.cl_projs; c :: props, rest' with Not_found -> (CHole (Util.dummy_loc, None) :: props), rest @@ -233,12 +231,14 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props if rest <> [] then unbound_method env' k.cl_impl (get_id (fst (List.hd rest))) else - Inl (type_ctx_instance evars (push_rel_context ctx' env') k.cl_props props subst) + Some (Inl (type_ctx_instance evars (push_rel_context ctx' env') k.cl_props props subst)) in evars := Evarutil.nf_evar_map !evars; let term, termtype = match subst with - | Inl subst -> + | None -> let termtype = it_mkProd_or_LetIn cty ctx in + None, termtype + | Some (Inl subst) -> let subst = List.fold_left2 (fun subst' s (_, b, _) -> if b = None then s :: subst' else subst') [] subst (k.cl_props @ snd k.cl_context) @@ -246,26 +246,25 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props let app, ty_constr = instance_constructor k subst in let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in let term = Termops.it_mkLambda_or_LetIn (Option.get app) (ctx' @ ctx) in - term, termtype - | Inr (def, subst) -> + Some term, termtype + | Some (Inr (def, subst)) -> let termtype = it_mkProd_or_LetIn cty ctx in let term = Termops.it_mkLambda_or_LetIn def ctx in - term, termtype + Some term, termtype in let termtype = Evarutil.nf_evar !evars termtype in - let term = Evarutil.nf_evar !evars term in + let term = Option.map (Evarutil.nf_evar !evars) term in let evm = undefined_evars !evars in Evarutil.check_evars env Evd.empty !evars termtype; - if Evd.is_empty evm then - declare_instance_constant k pri global imps ?hook id term termtype + if Evd.is_empty evm && term <> None then + declare_instance_constant k pri global imps ?hook id (Option.get term) termtype else begin evars := Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:true env !evars; let kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Instance in Flags.silently (fun () -> Lemmas.start_proof id kind termtype (fun _ -> instance_hook k pri global imps ?hook); - if props <> Inl [] then - Pfedit.by (* (Refiner.tclTHEN (Refiner.tclEVARS ( !isevars)) *) - (!refine_ref (evm, term)) + if term <> None then + Pfedit.by (!refine_ref (evm, Option.get term)) else if Flags.is_auto_intros () then Pfedit.by (Refiner.tclDO len Tactics.intro); (match tac with Some tac -> Pfedit.by tac | None -> ())) (); @@ -284,18 +283,13 @@ let named_of_rel_context l = l ([], []) in ctx -let push_named_context = List.fold_right push_named - -let rec list_filter_map f = function - | [] -> [] - | hd :: tl -> match f hd with - | None -> list_filter_map f tl - | Some x -> x :: list_filter_map f tl - -let context ?(hook=fun _ -> ()) l = +let string_of_global r = + string_of_qualid (Nametab.shortest_qualid_of_global Idset.empty r) + +let context l = let env = Global.env() in let evars = ref Evd.empty in - let (env', fullctx), impls = interp_context_evars evars env l in + let _, ((env', fullctx), impls) = interp_context_evars evars env l in let fullctx = Evarutil.nf_rel_context_evar !evars fullctx in let ce t = Evarutil.check_evars env Evd.empty !evars t in List.iter (fun (n, b, t) -> Option.iter ce b; ce t) fullctx; @@ -304,13 +298,13 @@ let context ?(hook=fun _ -> ()) l = in let fn (id, _, t) = if Lib.is_modtype () && not (Lib.sections_are_opened ()) then - let cst = Declare.declare_internal_constant id - (ParameterEntry (t,false), IsAssumption Logical) + let cst = Declare.declare_constant ~internal:Declare.KernelSilent id + (ParameterEntry (None,t,None), IsAssumption Logical) in match class_of_constr t with - | Some tc -> - add_instance (Typeclasses.new_instance tc None false (ConstRef cst)); - hook (ConstRef cst) + | Some (rels, (tc, args) as _cl) -> + add_instance (Typeclasses.new_instance tc None false (ConstRef cst)) + (* declare_subclasses (ConstRef cst) cl *) | None -> () else ( let impl = List.exists @@ -318,9 +312,6 @@ let context ?(hook=fun _ -> ()) l = match x with ExplByPos (_, Some id') -> id = id' | _ -> false) impls in Command.declare_assumption false (Local (* global *), Definitional) t - [] impl (* implicit *) false (* inline *) (dummy_loc, id); - match class_of_constr t with - | None -> () - | Some tc -> hook (VarRef id)) + [] impl (* implicit *) None (* inline *) (dummy_loc, id)) in List.iter fn (List.rev ctx) - + diff --git a/toplevel/classes.mli b/toplevel/classes.mli index 69e4dd8b..68a93a74 100644 --- a/toplevel/classes.mli +++ b/toplevel/classes.mli @@ -1,14 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: classes.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(*i*) open Names open Decl_kinds open Term @@ -22,59 +19,56 @@ open Util open Typeclasses open Implicit_quantifiers open Libnames -(*i*) -(* Errors *) +(** Errors *) val mismatched_params : env -> constr_expr list -> rel_context -> 'a val mismatched_props : env -> constr_expr list -> rel_context -> 'a -(* Post-hoc class declaration. *) +(** Post-hoc class declaration. *) val declare_class : reference -> unit -(* Instance declaration *) +(** Instance declaration *) -val declare_instance : bool -> reference -> unit +val existing_instance : bool -> reference -> unit val declare_instance_constant : typeclass -> - int option -> (* priority *) - bool -> (* globality *) - Impargs.manual_explicitation list -> (* implicits *) + int option -> (** priority *) + bool -> (** globality *) + Impargs.manual_explicitation list -> (** implicits *) ?hook:(Libnames.global_reference -> unit) -> - identifier -> (* name *) - Term.constr -> (* body *) - Term.types -> (* type *) + identifier -> (** name *) + Term.constr -> (** body *) + Term.types -> (** type *) Names.identifier val new_instance : - ?abstract:bool -> (* Not abstract by default. *) - ?global:bool -> (* Not global by default. *) + ?abstract:bool -> (** Not abstract by default. *) + ?global:bool -> (** Not global by default. *) local_binder list -> typeclass_constraint -> - constr_expr -> + constr_expr option -> ?generalize:bool -> ?tac:Proof_type.tactic -> ?hook:(Libnames.global_reference -> unit) -> int option -> identifier -(* Setting opacity *) +(** Setting opacity *) -val set_typeclass_transparency : evaluable_global_reference -> bool -> unit +val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> unit -(* For generation on names based on classes only *) +(** For generation on names based on classes only *) val id_of_class : typeclass -> identifier -(* Context command *) +(** Context command *) -val context : ?hook:(Libnames.global_reference -> unit) -> - local_binder list -> unit +val context : local_binder list -> unit -(* Forward ref for refine *) +(** Forward ref for refine *) val refine_ref : (open_constr -> Proof_type.tactic) ref - diff --git a/toplevel/command.ml b/toplevel/command.ml index 1112ac6d..eca53ae7 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: command.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - open Pp open Util open Flags @@ -64,35 +62,36 @@ let red_constant_entry n ce = function | Some red -> let body = ce.const_entry_body in { ce with const_entry_body = - under_binders (Global.env()) (fst (reduction_of_red_expr red)) n body } + under_binders (Global.env()) (fst (reduction_of_red_expr red)) n body } -let interp_definition boxed bl red_option c ctypopt = +let interp_definition bl red_option c ctypopt = let env = Global.env() in let evdref = ref Evd.empty in - let (env_bl, ctx), imps1 = interp_context_evars evdref env bl in + let impls, ((env_bl, ctx), imps1) = interp_context_evars evdref env bl in + let nb_args = List.length ctx in let imps,ce = match ctypopt with None -> - let c, imps2 = interp_constr_evars_impls ~evdref ~fail_evar:false env_bl c in + let c, imps2 = interp_constr_evars_impls ~impls ~evdref ~fail_evar:false env_bl c in let body = nf_evar !evdref (it_mkLambda_or_LetIn c ctx) in check_evars env Evd.empty !evdref body; - imps1@imps2, + imps1@(Impargs.lift_implicits nb_args imps2), { const_entry_body = body; + const_entry_secctx = None; const_entry_type = None; - const_entry_opaque = false; - const_entry_boxed = boxed } + const_entry_opaque = false } | Some ctyp -> - let ty, impls = interp_type_evars_impls ~evdref ~fail_evar:false env_bl ctyp in - let c, imps2 = interp_casted_constr_evars_impls ~evdref ~fail_evar:false env_bl c ty in + let ty, impsty = interp_type_evars_impls ~impls ~evdref ~fail_evar:false env_bl ctyp in + let c, imps2 = interp_casted_constr_evars_impls ~impls ~evdref ~fail_evar:false env_bl c ty in let body = nf_evar !evdref (it_mkLambda_or_LetIn c ctx) in let typ = nf_evar !evdref (it_mkProd_or_LetIn ty ctx) in check_evars env Evd.empty !evdref body; check_evars env Evd.empty !evdref typ; - imps1@imps2, + imps1@(Impargs.lift_implicits nb_args imps2), { const_entry_body = body; + const_entry_secctx = None; const_entry_type = Some typ; - const_entry_opaque = false; - const_entry_boxed = boxed } + const_entry_opaque = false } in red_constant_entry (rel_context_length ctx) ce red_option, imps @@ -115,11 +114,11 @@ let declare_definition ident (local,k) ce imps hook = let r = match local with | Local when Lib.sections_are_opened () -> let c = - SectionLocalDef(ce.const_entry_body,ce.const_entry_type,false) in + SectionLocalDef(ce.const_entry_body ,ce.const_entry_type,false) in let _ = declare_variable ident (Lib.cwd(),c,IsDefinition k) in definition_message ident; if Pfedit.refining () then - Flags.if_verbose msg_warning + Flags.if_warn msg_warning (str"Local definition " ++ pr_id ident ++ str" is not visible from current goals"); VarRef ident @@ -139,10 +138,12 @@ let declare_assumption is_coe (local,kind) c imps impl nl (_,ident) = if is_verbose () & Pfedit.refining () then msgerrnl (str"Warning: Variable " ++ pr_id ident ++ str" is not visible from current goals"); - VarRef ident + let r = VarRef ident in + Typeclasses.declare_instance None true r; r | (Global|Local) -> let kn = - declare_constant ident (ParameterEntry (c,nl), IsAssumption kind) in + declare_constant ident + (ParameterEntry (None,c,nl), IsAssumption kind) in let gr = ConstRef kn in maybe_declare_manual_implicits false gr imps; assumption_message ident; @@ -150,8 +151,10 @@ let declare_assumption is_coe (local,kind) c imps impl nl (_,ident) = msg_warning (pr_id ident ++ str" is declared as a parameter" ++ str" because it is at a global level"); Autoinstance.search_declaration (ConstRef kn); - gr in - if is_coe then Class.try_add_new_coercion r local + Typeclasses.declare_instance None false gr; + gr + in + if is_coe then Class.try_add_new_coercion r local let declare_assumptions_hook = ref ignore let set_declare_assumptions_hook = (:=) declare_assumptions_hook @@ -225,7 +228,7 @@ let interp_mutual_inductive (paramsl,indl) notations finite = check_all_names_different indl; let env0 = Global.env() in let evdref = ref Evd.empty in - let (env_params, ctx_params), userimpls = + let _, ((env_params, ctx_params), userimpls) = interp_context_evars evdref env0 paramsl in let indnames = List.map (fun ind -> ind.ind_name) indl in @@ -321,7 +324,7 @@ let extract_params indl = let extract_inductive indl = List.map (fun ((_,indname),_,ar,lc) -> { ind_name = indname; - ind_arity = Option.cata (fun x -> x) (CSort (dummy_loc, Rawterm.RType None)) ar; + ind_arity = Option.cata (fun x -> x) (CSort (dummy_loc, Glob_term.GType None)) ar; ind_lc = List.map (fun (_,((_,id),t)) -> (id,t)) lc }) indl @@ -335,7 +338,7 @@ let extract_mutual_inductive_declaration_components indl = let declare_mutual_inductive_with_eliminations isrecord mie impls = let names = List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in let (_,kn) = declare_mind isrecord mie in - let mind = Global.mind_of_delta (mind_of_kn kn) in + let mind = Global.mind_of_delta_kn kn in list_iter_i (fun i (indimpls, constrimpls) -> let ind = (mind,i) in Autoinstance.search_declaration (IndRef ind); @@ -442,7 +445,7 @@ let check_mutuality env isfix fixl = let po = partial_order preorder in match List.filter (function (_,Inr _) -> true | _ -> false) po with | (x,Inr xge)::(y,Inr yge)::rest -> - if_verbose msg_warning (non_full_mutual_message x xge y yge isfix rest) + if_warn msg_warning (non_full_mutual_message x xge y yge isfix rest) | _ -> () type structured_fixpoint_expr = { @@ -455,8 +458,8 @@ type structured_fixpoint_expr = { let interp_fix_context evdref env isfix fix = let before, after = if isfix then split_at_annot fix.fix_binders fix.fix_annot else [], fix.fix_binders in - let (env', ctx), imps = interp_context_evars evdref env before in - let (env'', ctx'), imps' = interp_context_evars evdref env' after in + let impl_env, ((env', ctx), imps) = interp_context_evars evdref env before in + let _, ((env'', ctx'), imps') = interp_context_evars ~impl_env evdref env' after in let annot = Option.map (fun _ -> List.length (assums_of_rel_context ctx)) fix.fix_annot in ((env'', ctx' @ ctx), imps @ imps', annot) @@ -471,13 +474,13 @@ let interp_fix_body evdref env_rec impls (_,ctx) fix ccl = let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx -let declare_fix boxed kind f def t imps = +let declare_fix kind f def t imps = let ce = { const_entry_body = def; + const_entry_secctx = None; const_entry_type = Some t; - const_entry_opaque = false; - const_entry_boxed = boxed - } in + const_entry_opaque = false } + in let kn = declare_constant f (DefinitionEntry ce,IsDefinition kind) in let gr = ConstRef kn in Autoinstance.search_declaration (ConstRef kn); @@ -547,7 +550,7 @@ let interp_recursive isfix fixl notations = let interp_fixpoint = interp_recursive true let interp_cofixpoint = interp_recursive false -let declare_fixpoint boxed ((fixnames,fixdefs,fixtypes),fiximps) indexes ntns = +let declare_fixpoint ((fixnames,fixdefs,fixtypes),fiximps) indexes ntns = if List.mem None fixdefs then (* Some bodies to define by proof *) let thms = @@ -565,14 +568,14 @@ let declare_fixpoint boxed ((fixnames,fixdefs,fixtypes),fiximps) indexes ntns = let fiximps = List.map (fun (n,r,p) -> r) fiximps in let fixdecls = list_map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in - ignore (list_map4 (declare_fix boxed Fixpoint) fixnames fixdecls fixtypes fiximps); + ignore (list_map4 (declare_fix Fixpoint) fixnames fixdecls fixtypes fiximps); (* Declare the recursive definitions *) fixpoint_message (Some indexes) fixnames; end; (* Declare notations *) List.iter Metasyntax.add_notation_interpretation ntns -let declare_cofixpoint boxed ((fixnames,fixdefs,fixtypes),fiximps) ntns = +let declare_cofixpoint ((fixnames,fixdefs,fixtypes),fiximps) ntns = if List.mem None fixdefs then (* Some bodies to define by proof *) let thms = @@ -588,22 +591,23 @@ let declare_cofixpoint boxed ((fixnames,fixdefs,fixtypes),fiximps) ntns = let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in let fixdecls = list_map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in - ignore (list_map4 (declare_fix boxed CoFixpoint) fixnames fixdecls fixtypes fiximps); + ignore (list_map4 (declare_fix CoFixpoint) fixnames fixdecls fixtypes fiximps); (* Declare the recursive definitions *) cofixpoint_message fixnames end; (* Declare notations *) List.iter Metasyntax.add_notation_interpretation ntns -let extract_decreasing_argument = function +let extract_decreasing_argument limit = function | (na,CStructRec) -> na + | (na,_) when not limit -> na | _ -> error "Only structural decreasing is supported for a non-Program Fixpoint" -let extract_fixpoint_components l = +let extract_fixpoint_components limit l = let fixl, ntnl = List.split l in let fixl = List.map (fun ((_,id),ann,bl,typ,def) -> - let ann = extract_decreasing_argument ann in + let ann = extract_decreasing_argument limit ann in {fix_name = id; fix_annot = ann; fix_binders = bl; fix_body = def; fix_type = typ}) fixl in fixl, List.flatten ntnl @@ -613,13 +617,13 @@ let extract_cofixpoint_components l = {fix_name = id; fix_annot = None; fix_binders = bl; fix_body = def; fix_type = typ}) fixl, List.flatten ntnl -let do_fixpoint l b = - let fixl,ntns = extract_fixpoint_components l in +let do_fixpoint l = + let fixl,ntns = extract_fixpoint_components true l in let fix = interp_fixpoint fixl ntns in let possible_indexes = List.map compute_possible_guardness_evidences (snd fix) in - declare_fixpoint b fix possible_indexes ntns + declare_fixpoint fix possible_indexes ntns -let do_cofixpoint l b = +let do_cofixpoint l = let fixl,ntns = extract_cofixpoint_components l in - declare_cofixpoint b (interp_cofixpoint fixl ntns) ntns + declare_cofixpoint (interp_cofixpoint fixl ntns) ntns diff --git a/toplevel/command.mli b/toplevel/command.mli index af89b59a..8ffdbdec 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -1,14 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: command.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(*i*) open Util open Names open Term @@ -21,45 +18,41 @@ open Decl_kinds open Redexpr open Constrintern open Pfedit -(*i*) -(*s This file is about the interpretation of raw commands into typed +(** This file is about the interpretation of raw commands into typed ones and top-level declaration of the main Gallina objects *) -(* Hooks for Pcoq *) +(** {6 Hooks for Pcoq} *) val set_declare_definition_hook : (definition_entry -> unit) -> unit val get_declare_definition_hook : unit -> (definition_entry -> unit) val set_declare_assumptions_hook : (types -> unit) -> unit -(*************************************************************************) -(* Definitions/Let *) +(** {6 Definitions/Let} *) val interp_definition : - boxed_flag -> local_binder list -> red_expr option -> constr_expr -> - constr_expr option -> definition_entry * manual_implicits + local_binder list -> red_expr option -> constr_expr -> + constr_expr option -> definition_entry * Impargs.manual_implicits val declare_definition : identifier -> locality * definition_object_kind -> - definition_entry -> manual_implicits -> declaration_hook -> unit + definition_entry -> Impargs.manual_implicits -> declaration_hook -> unit -(*************************************************************************) -(* Parameters/Assumptions *) +(** {6 Parameters/Assumptions} *) val interp_assumption : - local_binder list -> constr_expr -> types * manual_implicits + local_binder list -> constr_expr -> types * Impargs.manual_implicits val declare_assumption : coercion_flag -> assumption_kind -> types -> - manual_implicits -> - bool (* implicit *) -> bool (* inline *) -> variable located -> unit + Impargs.manual_implicits -> + bool (** implicit *) -> Entries.inline -> variable located -> unit val declare_assumptions : variable located list -> - coercion_flag -> assumption_kind -> types -> manual_implicits -> - bool -> bool -> unit + coercion_flag -> assumption_kind -> types -> Impargs.manual_implicits -> + bool -> Entries.inline -> unit -(*************************************************************************) -(* Inductive and coinductive types *) +(** {6 Inductive and coinductive types} *) -(* Extracting the semantical components out of the raw syntax of mutual +(** Extracting the semantical components out of the raw syntax of mutual inductive declarations *) type structured_one_inductive_expr = { @@ -75,30 +68,29 @@ val extract_mutual_inductive_declaration_components : (one_inductive_expr * decl_notation list) list -> structured_inductive_expr * (*coercions:*) qualid list * decl_notation list -(* Typing mutual inductive definitions *) +(** Typing mutual inductive definitions *) type one_inductive_impls = - Impargs.manual_explicitation list (* for inds *)* - Impargs.manual_explicitation list list (* for constrs *) + Impargs.manual_implicits (** for inds *)* + Impargs.manual_implicits list (** for constrs *) val interp_mutual_inductive : structured_inductive_expr -> decl_notation list -> bool -> mutual_inductive_entry * one_inductive_impls list -(* Registering a mutual inductive definition together with its +(** Registering a mutual inductive definition together with its associated schemes *) val declare_mutual_inductive_with_eliminations : Declare.internal_flag -> mutual_inductive_entry -> one_inductive_impls list -> mutual_inductive -(* Entry points for the vernacular commands Inductive and CoInductive *) +(** Entry points for the vernacular commands Inductive and CoInductive *) val do_mutual_inductive : (one_inductive_expr * decl_notation list) list -> bool -> unit -(*************************************************************************) -(* Fixpoints and cofixpoints *) +(** {6 Fixpoints and cofixpoints} *) type structured_fixpoint_expr = { fix_name : identifier; @@ -108,10 +100,10 @@ type structured_fixpoint_expr = { fix_type : constr_expr } -(* Extracting the semantical components out of the raw syntax of +(** Extracting the semantical components out of the raw syntax of (co)fixpoints declarations *) -val extract_fixpoint_components : +val extract_fixpoint_components : bool -> (fixpoint_expr * decl_notation list) list -> structured_fixpoint_expr list * decl_notation list @@ -119,40 +111,40 @@ val extract_cofixpoint_components : (cofixpoint_expr * decl_notation list) list -> structured_fixpoint_expr list * decl_notation list -(* Typing global fixpoints and cofixpoint_expr *) +(** Typing global fixpoints and cofixpoint_expr *) type recursive_preentry = identifier list * constr option list * types list val interp_fixpoint : structured_fixpoint_expr list -> decl_notation list -> - recursive_preentry * (name list * manual_implicits * int option) list + recursive_preentry * (name list * Impargs.manual_implicits * int option) list val interp_cofixpoint : structured_fixpoint_expr list -> decl_notation list -> - recursive_preentry * (name list * manual_implicits * int option) list + recursive_preentry * (name list * Impargs.manual_implicits * int option) list -(* Registering fixpoints and cofixpoints in the environment *) +(** Registering fixpoints and cofixpoints in the environment *) val declare_fixpoint : - bool -> recursive_preentry * (name list * manual_implicits * int option) list -> + recursive_preentry * (name list * Impargs.manual_implicits * int option) list -> lemma_possible_guards -> decl_notation list -> unit val declare_cofixpoint : - bool -> recursive_preentry * (name list * manual_implicits * int option) list -> + recursive_preentry * (name list * Impargs.manual_implicits * int option) list -> decl_notation list -> unit -(* Entry points for the vernacular commands Fixpoint and CoFixpoint *) +(** Entry points for the vernacular commands Fixpoint and CoFixpoint *) val do_fixpoint : - (fixpoint_expr * decl_notation list) list -> bool -> unit + (fixpoint_expr * decl_notation list) list -> unit val do_cofixpoint : - (cofixpoint_expr * decl_notation list) list -> bool -> unit + (cofixpoint_expr * decl_notation list) list -> unit -(* Utils *) +(** Utils *) val check_mutuality : Environ.env -> bool -> (identifier * types) list -> unit -val declare_fix : bool -> definition_object_kind -> identifier -> - constr -> types -> Impargs.manual_explicitation list -> global_reference +val declare_fix : definition_object_kind -> identifier -> + constr -> types -> Impargs.manual_implicits -> global_reference diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 210507e1..e4cfcb3f 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqinit.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - open Pp open System open Toplevel @@ -17,13 +15,13 @@ let (/) = Filename.concat let set_debug () = Flags.debug := true (* Loading of the ressource file. - rcfile is either $HOME/.coqrc.VERSION, or $HOME/.coqrc if the first one + rcfile is either $XDG_CONFIG_HOME/.coqrc.VERSION, or $XDG_CONFIG_HOME/.coqrc if the first one does not exist. *) -let rcfile = ref (home/".coqrc") +let rcdefaultname = "coqrc" +let rcfile = ref "" let rcfile_specified = ref false let set_rcfile s = rcfile := s; rcfile_specified := true -let set_rcuser s = rcfile := ("~"^s)/".coqrc" let load_rc = ref true let no_load_rc () = load_rc := false @@ -35,14 +33,17 @@ let load_rcfile() = if file_readable_p !rcfile then Vernac.load_vernac false !rcfile else raise (Sys_error ("Cannot read rcfile: "^ !rcfile)) - else if file_readable_p (!rcfile^"."^Coq_config.version) then - Vernac.load_vernac false (!rcfile^"."^Coq_config.version) - else if file_readable_p !rcfile then - Vernac.load_vernac false !rcfile - else () + else try let inferedrc = List.find file_readable_p [ + Envars.xdg_config_home/rcdefaultname^"."^Coq_config.version; + Envars.xdg_config_home/rcdefaultname; + System.home/"."^rcdefaultname^"."^Coq_config.version; + System.home/"."^rcdefaultname; + ] in + Vernac.load_vernac false inferedrc + with Not_found -> () (* Flags.if_verbose - mSGNL (str ("No .coqrc or .coqrc."^Coq_config.version^ + mSGNL (str ("No coqrc or coqrc."^Coq_config.version^ " found. Skipping rcfile loading.")) *) with e -> @@ -52,9 +53,9 @@ let load_rcfile() = Flags.if_verbose msgnl (str"Skipping rcfile loading.") (* Puts dir in the path of ML and in the LoadPath *) -let coq_add_path d s = - Mltop.add_path d (Names.make_dirpath [Nameops.coq_root;Names.id_of_string s]) -let coq_add_rec_path s = Mltop.add_rec_path s (Names.make_dirpath [Nameops.coq_root]) +let coq_add_path unix_path s = + Mltop.add_path ~unix_path ~coq_root:(Names.make_dirpath [Nameops.coq_root;Names.id_of_string s]) +let coq_add_rec_path unix_path = Mltop.add_rec_path ~unix_path ~coq_root:(Names.make_dirpath [Nameops.coq_root]) (* By the option -include -I or -R of the command line *) let includes = ref [] @@ -75,10 +76,12 @@ let theories_dirs_map = [ "theories/Sets", "Sets" ; "theories/Structures", "Structures" ; "theories/Lists", "Lists" ; + "theories/Vectors", "Vectors" ; "theories/Wellfounded", "Wellfounded" ; "theories/Relations", "Relations" ; "theories/Numbers", "Numbers" ; "theories/QArith", "QArith" ; + "theories/PArith", "PArith" ; "theories/NArith", "NArith" ; "theories/ZArith", "ZArith" ; "theories/Arith", "Arith" ; @@ -91,24 +94,31 @@ let theories_dirs_map = [ let init_load_path () = let coqlib = Envars.coqlib () in let user_contrib = coqlib/"user-contrib" in + let xdg_dirs = Envars.xdg_dirs in + let coqpath = Envars.coqpath in let dirs = ["states";"plugins"] in - (* first user-contrib *) - if Sys.file_exists user_contrib then - Mltop.add_rec_path user_contrib Nameops.default_root_prefix; - (* then states, theories and dev *) - List.iter (fun s -> coq_add_rec_path (coqlib/s)) dirs; - (* developer specific directory to open *) + (* NOTE: These directories are searched from last to first *) + (* first, developer specific directory to open *) if Coq_config.local then coq_add_path (coqlib/"dev") "dev"; (* then standard library *) List.iter - (fun (s,alias) -> Mltop.add_rec_path (coqlib/s) (Names.make_dirpath [Names.id_of_string alias; Nameops.coq_root])) + (fun (s,alias) -> Mltop.add_rec_path ~unix_path:(coqlib/s) ~coq_root:(Names.make_dirpath [Names.id_of_string alias; Nameops.coq_root])) theories_dirs_map; + (* then states and plugins *) + List.iter (fun s -> coq_add_rec_path (coqlib/s)) dirs; + (* then user-contrib *) + if Sys.file_exists user_contrib then + Mltop.add_rec_path ~unix_path:user_contrib ~coq_root:Nameops.default_root_prefix; + (* then directories in XDG_DATA_DIRS and XDG_DATA_HOME *) + List.iter (fun s -> Mltop.add_rec_path ~unix_path:s ~coq_root:Nameops.default_root_prefix) xdg_dirs; + (* then directories in COQPATH *) + List.iter (fun s -> Mltop.add_rec_path ~unix_path:s ~coq_root:Nameops.default_root_prefix) coqpath; (* then current directory *) - Mltop.add_path "." Nameops.default_root_prefix; + Mltop.add_path ~unix_path:"." ~coq_root:Nameops.default_root_prefix; (* additional loadpath, given with -I -include -R options *) List.iter - (fun (s,alias,reci) -> - if reci then Mltop.add_rec_path s alias else Mltop.add_path s alias) + (fun (unix_path, coq_root, reci) -> + if reci then Mltop.add_rec_path ~unix_path ~coq_root else Mltop.add_path ~unix_path ~coq_root) (List.rev !includes) let init_library_roots () = @@ -117,9 +127,8 @@ let init_library_roots () = (* Initialises the Ocaml toplevel before launching it, so that it can find the "include" file in the *source* directory *) let init_ocaml_path () = - let coqsrc = Coq_config.coqsrc in let add_subdir dl = - Mltop.add_ml_dir (List.fold_left (/) coqsrc dl) + Mltop.add_ml_dir (List.fold_left (/) Envars.coqroot dl) in Mltop.add_ml_dir (Envars.coqlib ()); List.iter add_subdir diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli index c0f59a56..43b1556d 100644 --- a/toplevel/coqinit.mli +++ b/toplevel/coqinit.mli @@ -1,19 +1,16 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: coqinit.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(* Initialization. *) +(** Initialization. *) val set_debug : unit -> unit val set_rcfile : string -> unit -val set_rcuser : string -> unit val no_load_rc : unit -> unit val load_rcfile : unit -> unit diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 7887a060..76e9c2fe 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqtop.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - open Pp open Util open System @@ -122,51 +120,19 @@ let compile_files () = (List.rev !compile_list) let set_compat_version = function + | "8.3" -> compat_version := Some V8_3 | "8.2" -> compat_version := Some V8_2 | "8.1" -> warning "Compatibility with version 8.1 not supported." | "8.0" -> warning "Compatibility with version 8.0 not supported." | s -> error ("Unknown compatibility version \""^s^"\".") -let re_exec_version = ref "" -let set_byte () = re_exec_version := "byte" -let set_opt () = re_exec_version := "opt" - -(* Re-exec Coq in bytecode or native code if necessary. [s] is either - ["byte"] or ["opt"]. Notice that this is possible since the nature of - the toplevel has already been set in [Mltop] by the main file created - by coqmktop (see scripts/coqmktop.ml). *) - -let re_exec is_ide = - let s = !re_exec_version in - let is_native = Mltop.is_native in - (* Unix.readlink is not implemented on Windows architectures :-( - let prog = - try Unix.readlink "/proc/self/exe" - with Unix.Unix_error _ -> Sys.argv.(0) in - *) - let prog = Sys.argv.(0) in - if (is_native && s = "byte") || ((not is_native) && s = "opt") - then begin - let s = if s = "" then if is_native then "opt" else "byte" else s in - let newprog = - let dir = Filename.dirname prog in - let coqtop = if is_ide then "coqide." else "coqtop." in - let com = coqtop ^ s ^ Coq_config.exec_extension in - if dir <> "." then Filename.concat dir com else com - in - Sys.argv.(0) <- newprog; - Unix.handle_unix_error (Unix.execvp newprog) Sys.argv - end - (*s options for the virtual machine *) let boxed_val = ref false -let boxed_def = ref false let use_vm = ref false let set_vm_opt () = Vm.set_transp_values (not !boxed_val); - Flags.set_boxed_definitions !boxed_def; Vconv.set_use_vm !use_vm (*s Parsing of the command line. @@ -183,12 +149,13 @@ let usage () = let warning s = msg_warning (str s) +let ide_slave = ref false +let filter_opts = ref false -let ide_args = ref [] -let parse_args is_ide = +let parse_args arglist = let glob_opt = ref false in let rec parse = function - | [] -> () + | [] -> [] | "-with-geoproof" :: s :: rem -> if s = "yes" then Coq_config.with_geoproof := true else if s = "no" then Coq_config.with_geoproof := false @@ -216,14 +183,15 @@ let parse_args is_ide = | "-notop" :: rem -> unset_toplevel_name (); parse rem | "-q" :: rem -> no_load_rc (); parse rem - | "-opt" :: rem -> set_opt(); parse rem - | "-byte" :: rem -> set_byte(); parse rem + | "-opt" :: rem -> warning "option -opt deprecated, call with .opt suffix\n"; parse rem + | "-byte" :: rem -> warning "option -byte deprecated, call with .byte suffix\n"; parse rem | "-full" :: rem -> warning "option -full deprecated\n"; parse rem | "-batch" :: rem -> set_batch_mode (); parse rem | "-boot" :: rem -> boot := true; no_load_rc (); parse rem | "-quality" :: rem -> term_quality := true; no_load_rc (); parse rem - | "-outputstate" :: s :: rem -> set_outputstate s; parse rem + | "-outputstate" :: s :: rem -> + Flags.load_proofs := Flags.Force; set_outputstate s; parse rem | "-outputstate" :: [] -> usage () | "-nois" :: rem -> set_inputstate ""; parse rem @@ -264,7 +232,9 @@ let parse_args is_ide = | "-compile-verbose" :: f :: rem -> add_compile true f; if not !glob_opt then Dumpglob.dump_to_dotglob (); parse rem | "-compile-verbose" :: [] -> usage () - | "-dont-load-proofs" :: rem -> Flags.dont_load_proofs := true; parse rem + | "-force-load-proofs" :: rem -> Flags.load_proofs := Flags.Force; parse rem + | "-lazy-load-proofs" :: rem -> Flags.load_proofs := Flags.Lazy; parse rem + | "-dont-load-proofs" :: rem -> Flags.load_proofs := Flags.Dont; parse rem | "-beautify" :: rem -> make_beautify true; parse rem @@ -278,30 +248,28 @@ let parse_args is_ide = | "-vm" :: rem -> use_vm := true; parse rem | "-emacs" :: rem -> Flags.print_emacs := true; Pp.make_pp_emacs(); parse rem - | "-emacs-U" :: rem -> Flags.print_emacs := true; - Flags.print_emacs_safechar := true; Pp.make_pp_emacs(); parse rem + | "-emacs-U" :: rem -> + warning "Obsolete option \"-emacs-U\", use -emacs instead."; + Flags.print_emacs := true; Pp.make_pp_emacs(); parse rem | "-unicode" :: rem -> add_require "Utf8_core"; parse rem | "-coqlib" :: d :: rem -> Flags.coqlib_spec:=true; Flags.coqlib:=d; parse rem | "-coqlib" :: [] -> usage () - | "-where" :: _ -> print_endline (Envars.coqlib ()); exit 0 + | "-where" :: _ -> print_endline (Envars.coqlib ()); exit (if !filter_opts then 2 else 0) - | ("-config"|"--config") :: _ -> Usage.print_config (); exit 0 + | ("-config"|"--config") :: _ -> Usage.print_config (); exit (if !filter_opts then 2 else 0) | ("-quiet"|"-silent") :: rem -> Flags.make_silent true; parse rem | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage () - | ("-v"|"--version") :: _ -> Usage.version () + | ("-v"|"--version") :: _ -> Usage.version (if !filter_opts then 2 else 0) | "-init-file" :: f :: rem -> set_rcfile f; parse rem | "-init-file" :: [] -> usage () - | "-user" :: u :: rem -> set_rcuser u; parse rem - | "-user" :: [] -> usage () - | "-notactics" :: rem -> warning "Obsolete option \"-notactics\"."; remove_top_ml (); parse rem @@ -320,32 +288,41 @@ let parse_args is_ide = | "-no-hash-consing" :: rem -> Flags.hash_cons_proofs := false; parse rem + | "-ideslave" :: rem -> ide_slave := true; parse rem + + | "-filteropts" :: rem -> filter_opts := true; parse rem + | s :: rem -> - if is_ide then begin - ide_args := s :: !ide_args; - parse rem - end else begin - prerr_endline ("Don't know what to do with " ^ s); usage () - end + if !filter_opts then + s :: (parse rem) + else + (prerr_endline ("Don't know what to do with " ^ s); usage ()) in try - parse (List.tl (Array.to_list Sys.argv)) + parse arglist with | UserError(_,s) as e -> begin try Stream.empty s; exit 1 with Stream.Failure -> - msgnl (Cerrors.explain_exn e); exit 1 + msgnl (Errors.print e); exit 1 end - | e -> begin msgnl (Cerrors.explain_exn e); exit 1 end + | e -> begin msgnl (Errors.print e); exit 1 end -let init is_ide = +let init arglist = Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *) Lib.init(); + (* Default Proofb Mode starts with an alternative default. *) + Goptions.set_string_option_value ["Default";"Proof";"Mode"] "Classic"; begin try - parse_args is_ide; - re_exec is_ide; + let foreign_args = parse_args arglist in + if !filter_opts then + (print_string (String.concat "\n" foreign_args); exit 0); + if !ide_slave then begin + Flags.make_silent true; + Ide_slave.init_stdout () + end; if_verbose print_header (); init_load_path (); inputstate (); @@ -374,13 +351,14 @@ let init is_ide = exit 0); Lib.declare_initial_state () -let init_toplevel () = init false - -let init_ide () = init true; List.rev !ide_args +let init_toplevel = init let start () = - init_toplevel (); - Toplevel.loop(); + init_toplevel (List.tl (Array.to_list Sys.argv)); + if !ide_slave then + Ide_slave.loop () + else + Toplevel.loop(); (* Initialise and launch the Ocaml toplevel *) Coqinit.init_ocaml_path(); Mltop.ocaml_toploop(); diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli index ef730915..16d2b874 100644 --- a/toplevel/coqtop.mli +++ b/toplevel/coqtop.mli @@ -1,23 +1,16 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: coqtop.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(* The Coq main module. The following function [start] will parse the +(** The Coq main module. The following function [start] will parse the command line, print the banner, initialize the load path, load the input state, load the files given on the command line, load the ressource file, produce the output state if any, and finally will launch [Toplevel.loop]. *) -val start : unit -> unit - -(* [init_ide] is to be used by the Coq IDE. - It does everything [start] does, except launching the toplevel loop. - It returns the list of Coq files given on the command line. *) - -val init_ide : unit -> string list +val init_toplevel : string list -> unit +val start : unit -> unit diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 58122e11..bab711ea 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: discharge.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - open Names open Util open Sign diff --git a/toplevel/discharge.mli b/toplevel/discharge.mli index f881e8a2..f94ed6e3 100644 --- a/toplevel/discharge.mli +++ b/toplevel/discharge.mli @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: discharge.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - open Sign open Cooking open Declarations diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 62d19bea..1bd68014 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: himsg.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - open Pp open Util open Flags @@ -28,7 +26,7 @@ open Reduction open Cases open Logic open Printer -open Rawterm +open Glob_term open Evd let pr_lconstr c = quote (pr_lconstr c) @@ -52,7 +50,8 @@ let explain_unbound_var env v = let var = pr_id v in str "No such section variable or assumption: " ++ var ++ str "." -let explain_not_type env j = +let explain_not_type env sigma j = + let j = j_nf_evar sigma j in let pe = pr_ne_context_of (str "In environment") env in let pc,pt = pr_ljudge_env env j in pe ++ str "The term" ++ brk(1,1) ++ pc ++ spc () ++ @@ -111,7 +110,8 @@ let explain_elim_arity env ind sorts c pj okinds = str "in the inductive type" ++ spc () ++ quote pi ++ str ":") ++ fnl () ++ msg -let explain_case_not_inductive env cj = +let explain_case_not_inductive env sigma cj = + let cj = j_nf_evar sigma cj in let env = make_all_name_different env in let pc = pr_lconstr_env env cj.uj_val in let pct = pr_lconstr_env env cj.uj_type in @@ -123,7 +123,8 @@ let explain_case_not_inductive env cj = str "has type" ++ brk(1,1) ++ pct ++ spc () ++ str "which is not a (co-)inductive type." -let explain_number_branches env cj expn = +let explain_number_branches env sigma cj expn = + let cj = j_nf_evar sigma cj in let env = make_all_name_different env in let pc = pr_lconstr_env env cj.uj_val in let pct = pr_lconstr_env env cj.uj_type in @@ -131,14 +132,17 @@ let explain_number_branches env cj expn = str "of type" ++ brk(1,1) ++ pct ++ spc () ++ str "expects " ++ int expn ++ str " branches." -let explain_ill_formed_branch env c i actty expty = +let explain_ill_formed_branch env sigma c ci actty expty = + let simp t = Reduction.nf_betaiota (nf_evar sigma t) in + let c = nf_evar sigma c in let env = make_all_name_different env in let pc = pr_lconstr_env env c in - let pa = pr_lconstr_env env actty in - let pe = pr_lconstr_env env expty in - str "In pattern-matching on term" ++ brk(1,1) ++ pc ++ - spc () ++ str "the " ++ nth (i+1) ++ str " branch has type" ++ - brk(1,1) ++ pa ++ spc () ++ + let pa = pr_lconstr_env env (simp actty) in + let pe = pr_lconstr_env env (simp expty) in + strbrk "In pattern-matching on term" ++ brk(1,1) ++ pc ++ + spc () ++ strbrk "the branch for constructor" ++ spc () ++ + quote (pr_constructor env ci) ++ + spc () ++ str "has type" ++ brk(1,1) ++ pa ++ spc () ++ str "which should be" ++ brk(1,1) ++ pe ++ str "." let explain_generalization env (name,var) j = @@ -150,7 +154,9 @@ let explain_generalization env (name,var) j = str "it has type" ++ spc () ++ pt ++ spc () ++ str "which should be Set, Prop or Type." -let explain_actual_type env j pt = +let explain_actual_type env sigma j pt = + let j = j_nf_betaiotaevar sigma j in + let pt = Reductionops.nf_betaiota sigma pt in let pe = pr_ne_context_of (str "In environment") env in let (pc,pct) = pr_ljudge_env env j in let pt = pr_lconstr_env env pt in @@ -159,7 +165,11 @@ let explain_actual_type env j pt = str "has type" ++ brk(1,1) ++ pct ++ brk(1,1) ++ str "while it is expected to have type" ++ brk(1,1) ++ pt ++ str "." -let explain_cant_apply_bad_type env (n,exptyp,actualtyp) rator randl = +let explain_cant_apply_bad_type env sigma (n,exptyp,actualtyp) rator randl = + let randl = jv_nf_betaiotaevar sigma randl in + let exptyp = nf_evar sigma exptyp in + let actualtyp = Reductionops.nf_betaiota sigma actualtyp in + let rator = j_nf_evar sigma rator in let env = make_all_name_different env in let nargs = Array.length randl in (* let pe = pr_ne_context_of (str "in environment") env in*) @@ -181,7 +191,9 @@ let explain_cant_apply_bad_type env (n,exptyp,actualtyp) rator randl = str "which should be coercible to" ++ brk(1,1) ++ pr_lconstr_env env exptyp ++ str "." -let explain_cant_apply_not_functional env rator randl = +let explain_cant_apply_not_functional env sigma rator randl = + let randl = jv_nf_evar sigma randl in + let rator = j_nf_evar sigma rator in let env = make_all_name_different env in let nargs = Array.length randl in (* let pe = pr_ne_context_of (str "in environment") env in*) @@ -200,14 +212,16 @@ let explain_cant_apply_not_functional env rator randl = str "cannot be applied to the " ++ str (plural nargs "term") ++ fnl () ++ str " " ++ v 0 appl -let explain_unexpected_type env actual_type expected_type = +let explain_unexpected_type env sigma actual_type expected_type = + let actual_type = nf_evar sigma actual_type in + let expected_type = nf_evar sigma expected_type in let pract = pr_lconstr_env env actual_type in let prexp = pr_lconstr_env env expected_type in - str "This type is" ++ spc () ++ pract ++ spc () ++ - str "but is expected to be" ++ - spc () ++ prexp ++ str "." + str "Found type" ++ spc () ++ pract ++ spc () ++ + str "where" ++ spc () ++ prexp ++ str " was expected." -let explain_not_product env c = +let explain_not_product env sigma c = + let c = nf_evar sigma c in let pr = pr_lconstr_env env c in str "The type of this term is a product" ++ spc () ++ str "while it is expected to be" ++ @@ -229,7 +243,8 @@ let explain_ill_formed_rec_body env err names i fixenv vdefj = | RecursionNotOnInductiveType c -> str "Recursive definition on" ++ spc () ++ pr_lconstr_env env c ++ spc () ++ str "which should be an inductive type" - | RecursionOnIllegalTerm(j,arg,le,lt) -> + | RecursionOnIllegalTerm(j,(arg_env, arg),le,lt) -> + let arg_env = make_all_name_different arg_env in let called = match names.(j) with Name id -> pr_id id @@ -247,7 +262,7 @@ let explain_ill_formed_rec_body env err names i fixenv vdefj = prlist_with_sep pr_spc pr_db lt in str "Recursive call to " ++ called ++ spc () ++ strbrk "has principal argument equal to" ++ spc () ++ - pr_lconstr_env env arg ++ strbrk " instead of " ++ vars + pr_lconstr_env arg_env arg ++ strbrk " instead of " ++ vars | NotEnoughArgumentsForFixCall j -> let called = @@ -274,12 +289,12 @@ let explain_ill_formed_rec_body env err names i fixenv vdefj = str "Recursive call forbidden in the type of a recursive definition" ++ spc () ++ pr_lconstr_env env c | RecCallInCaseFun c -> - str "Recursive call in a branch of" ++ spc () ++ pr_lconstr_env env c + str "Invalid recursive call in a branch of" ++ spc () ++ pr_lconstr_env env c | RecCallInCaseArg c -> - str "Recursive call in the argument of cases in" ++ spc () ++ + str "Invalid recursive call in the argument of \"match\" in" ++ spc () ++ pr_lconstr_env env c | RecCallInCasePred c -> - str "Recursive call in the type of cases in" ++ spc () ++ + str "Invalid recursive call in the \"return\" clause of \"match\" in" ++ spc () ++ pr_lconstr_env env c | NotGuardedForm c -> str "Sub-expression " ++ pr_lconstr_env env c ++ @@ -295,7 +310,9 @@ let explain_ill_formed_rec_body env err names i fixenv vdefj = str"Recursive definition is:" ++ spc () ++ pvd ++ str "." with _ -> mt ()) -let explain_ill_typed_rec_body env i names vdefj vargs = +let explain_ill_typed_rec_body env sigma i names vdefj vargs = + let vdefj = jv_nf_evar sigma vdefj in + let vargs = Array.map (nf_evar sigma) vargs in let env = make_all_name_different env in let pvd,pvdt = pr_ljudge_env env (vdefj.(i)) in let pv = pr_lconstr_env env vargs.(i) in @@ -305,12 +322,14 @@ let explain_ill_typed_rec_body env i names vdefj vargs = str "has type" ++ spc () ++ pvdt ++ spc () ++ str "while it should be" ++ spc () ++ pv ++ str "." -let explain_cant_find_case_type env c = +let explain_cant_find_case_type env sigma c = + let c = nf_evar sigma c in let env = make_all_name_different env in let pe = pr_lconstr_env env c in str "Cannot infer type of pattern-matching on" ++ ws 1 ++ pe ++ str "." -let explain_occur_check env ev rhs = +let explain_occur_check env sigma ev rhs = + let rhs = nf_evar sigma rhs in let env = make_all_name_different env in let id = Evd.string_of_existential ev in let pt = pr_lconstr_env env rhs in @@ -354,7 +373,8 @@ let explain_hole_kind env evi = function | MatchingVar _ -> assert false -let explain_not_clean env ev t k = +let explain_not_clean env sigma ev t k = + let t = nf_evar sigma t in let env = make_all_name_different env in let id = Evd.string_of_existential ev in let var = pr_lconstr_env env t in @@ -401,13 +421,15 @@ let explain_wrong_case_info env ind ci = str "was given to a pattern-matching expression on the inductive type" ++ spc () ++ pc ++ str "." -let explain_cannot_unify env m n = +let explain_cannot_unify env sigma m n = + let m = nf_evar sigma m in + let n = nf_evar sigma n in let pm = pr_lconstr_env env m in let pn = pr_lconstr_env env n in str "Impossible to unify" ++ brk(1,1) ++ pm ++ spc () ++ str "with" ++ brk(1,1) ++ pn ++ str "." -let explain_cannot_unify_local env m n subn = +let explain_cannot_unify_local env sigma m n subn = let pm = pr_lconstr_env env m in let pn = pr_lconstr_env env n in let psubn = pr_lconstr_env env subn in @@ -449,7 +471,7 @@ let explain_non_linear_unification env m t = strbrk " which would require to abstract twice on " ++ pr_lconstr_env env t ++ str "." -let explain_type_error env err = +let explain_type_error env sigma err = let env = make_all_name_different env in match err with | UnboundRel n -> @@ -457,7 +479,7 @@ let explain_type_error env err = | UnboundVar v -> explain_unbound_var env v | NotAType j -> - explain_not_type env j + explain_not_type env sigma j | BadAssumption c -> explain_bad_assumption env c | ReferenceVariables id -> @@ -465,38 +487,39 @@ let explain_type_error env err = | ElimArity (ind, aritylst, c, pj, okinds) -> explain_elim_arity env ind aritylst c pj okinds | CaseNotInductive cj -> - explain_case_not_inductive env cj + explain_case_not_inductive env sigma cj | NumberBranches (cj, n) -> - explain_number_branches env cj n + explain_number_branches env sigma cj n | IllFormedBranch (c, i, actty, expty) -> - explain_ill_formed_branch env c i actty expty + explain_ill_formed_branch env sigma c i actty expty | Generalization (nvar, c) -> explain_generalization env nvar c | ActualType (j, pt) -> - explain_actual_type env j pt + explain_actual_type env sigma j pt | CantApplyBadType (t, rator, randl) -> - explain_cant_apply_bad_type env t rator randl + explain_cant_apply_bad_type env sigma t rator randl | CantApplyNonFunctional (rator, randl) -> - explain_cant_apply_not_functional env rator randl + explain_cant_apply_not_functional env sigma rator randl | IllFormedRecBody (err, lna, i, fixenv, vdefj) -> explain_ill_formed_rec_body env err lna i fixenv vdefj | IllTypedRecBody (i, lna, vdefj, vargs) -> - explain_ill_typed_rec_body env i lna vdefj vargs + explain_ill_typed_rec_body env sigma i lna vdefj vargs | WrongCaseInfo (ind,ci) -> explain_wrong_case_info env ind ci -let explain_pretype_error env err = +let explain_pretype_error env sigma err = + let env = env_nf_betaiotaevar sigma env in let env = make_all_name_different env in match err with - | CantFindCaseType c -> explain_cant_find_case_type env c - | OccurCheck (n,c) -> explain_occur_check env n c - | NotClean (n,c,k) -> explain_not_clean env n c k + | CantFindCaseType c -> explain_cant_find_case_type env sigma c + | OccurCheck (n,c) -> explain_occur_check env sigma n c + | NotClean (n,c,k) -> explain_not_clean env sigma n c k | UnsolvableImplicit (evi,k,exp) -> explain_unsolvable_implicit env evi k exp | VarNotFound id -> explain_var_not_found env id - | UnexpectedType (actual,expect) -> explain_unexpected_type env actual expect - | NotProduct c -> explain_not_product env c - | CannotUnify (m,n) -> explain_cannot_unify env m n - | CannotUnifyLocal (m,n,sn) -> explain_cannot_unify_local env m n sn + | UnexpectedType (actual,expect) -> explain_unexpected_type env sigma actual expect + | NotProduct c -> explain_not_product env sigma c + | CannotUnify (m,n) -> explain_cannot_unify env sigma m n + | CannotUnifyLocal (m,n,sn) -> explain_cannot_unify_local env sigma m n sn | CannotGeneralize ty -> explain_refiner_cannot_generalize env ty | NoOccurrenceFound (c, id) -> explain_no_occurrence_found env c id | CannotUnifyBindingType (m,n) -> explain_cannot_unify_binding_type env m n @@ -504,6 +527,155 @@ let explain_pretype_error env err = explain_cannot_find_well_typed_abstraction env p l | AbstractionOverMeta (m,n) -> explain_abstraction_over_meta env m n | NonLinearUnification (m,c) -> explain_non_linear_unification env m c + | TypingError t -> explain_type_error env sigma t + +(* Module errors *) + +open Modops + +let explain_not_match_error = function + | InductiveFieldExpected _ -> + strbrk "an inductive definition is expected" + | DefinitionFieldExpected -> + strbrk "a definition is expected" + | ModuleFieldExpected -> + strbrk "a module is expected" + | ModuleTypeFieldExpected -> + strbrk "a module type is expected" + | NotConvertibleInductiveField id | NotConvertibleConstructorField id -> + str "types given to " ++ str (string_of_id id) ++ str " differ" + | NotConvertibleBodyField -> + str "the body of definitions differs" + | NotConvertibleTypeField -> + str "types differ" + | NotSameConstructorNamesField -> + str "constructor names differ" + | NotSameInductiveNameInBlockField -> + str "inductive types names differ" + | FiniteInductiveFieldExpected isfinite -> + str "type is expected to be " ++ + str (if isfinite then "coinductive" else "inductive") + | InductiveNumbersFieldExpected n -> + str "number of inductive types differs" + | InductiveParamsNumberField n -> + str "inductive type has not the right number of parameters" + | RecordFieldExpected isrecord -> + str "type is expected " ++ str (if isrecord then "" else "not ") ++ + str "to be a record" + | RecordProjectionsExpected nal -> + (if List.length nal >= 2 then str "expected projection names are " + else str "expected projection name is ") ++ + pr_enum (function Name id -> str (string_of_id id) | _ -> str "_") nal + | NotEqualInductiveAliases -> + str "Aliases to inductive types do not match" + | NoTypeConstraintExpected -> + strbrk "a definition whose type is constrained can only be subtype of a definition whose type is itself constrained" + +let explain_signature_mismatch l spec why = + str "Signature components for label " ++ str (string_of_label l) ++ + str " do not match:" ++ spc () ++ explain_not_match_error why ++ str "." + +let explain_label_already_declared l = + str ("The label "^string_of_label l^" is already declared.") + +let explain_application_to_not_path _ = + str "Application of modules is restricted to paths." + +let explain_not_a_functor mtb = + str "Application of not a functor." + +let explain_incompatible_module_types mexpr1 mexpr2 = + str "Incompatible module types." + +let explain_not_equal_module_paths mp1 mp2 = + str "Non equal modules." + +let explain_no_such_label l = + str "No such label " ++ str (string_of_label l) ++ str "." + +let explain_incompatible_labels l l' = + str "Opening and closing labels are not the same: " ++ + str (string_of_label l) ++ str " <> " ++ str (string_of_label l') ++ str "!" + +let explain_signature_expected mtb = + str "Signature expected." + +let explain_no_module_to_end () = + str "No open module to end." + +let explain_no_module_type_to_end () = + str "No open module type to end." + +let explain_not_a_module s = + quote (str s) ++ str " is not a module." + +let explain_not_a_module_type s = + quote (str s) ++ str " is not a module type." + +let explain_not_a_constant l = + quote (pr_label l) ++ str " is not a constant." + +let explain_incorrect_label_constraint l = + str "Incorrect constraint for label " ++ + quote (pr_label l) ++ str "." + +let explain_generative_module_expected l = + str "The module " ++ str (string_of_label l) ++ + strbrk " is not generative. Only components of generative modules can be changed using the \"with\" construct." + +let explain_non_empty_local_context = function + | None -> str "The local context is not empty." + | Some l -> + str "The local context of the component " ++ + str (string_of_label l) ++ str " is not empty." + +let explain_label_missing l s = + str "The field " ++ str (string_of_label l) ++ str " is missing in " + ++ str s ++ str "." + +let explain_module_error = function + | SignatureMismatch (l,spec,err) -> explain_signature_mismatch l spec err + | LabelAlreadyDeclared l -> explain_label_already_declared l + | ApplicationToNotPath mexpr -> explain_application_to_not_path mexpr + | NotAFunctor mtb -> explain_not_a_functor mtb + | IncompatibleModuleTypes (m1,m2) -> explain_incompatible_module_types m1 m2 + | NotEqualModulePaths (mp1,mp2) -> explain_not_equal_module_paths mp1 mp2 + | NoSuchLabel l -> explain_no_such_label l + | IncompatibleLabels (l1,l2) -> explain_incompatible_labels l1 l2 + | SignatureExpected mtb -> explain_signature_expected mtb + | NoModuleToEnd -> explain_no_module_to_end () + | NoModuleTypeToEnd -> explain_no_module_type_to_end () + | NotAModule s -> explain_not_a_module s + | NotAModuleType s -> explain_not_a_module_type s + | NotAConstant l -> explain_not_a_constant l + | IncorrectWithConstraint l -> explain_incorrect_label_constraint l + | GenerativeModuleExpected l -> explain_generative_module_expected l + | NonEmptyLocalContect lopt -> explain_non_empty_local_context lopt + | LabelMissing (l,s) -> explain_label_missing l s + +(* Module internalization errors *) + +(* +let explain_declaration_not_path _ = + str "Declaration is not a path." + +*) + +let explain_not_module_nor_modtype s = + quote (str s) ++ str " is not a module or module type." + +let explain_incorrect_with_in_module () = + str "The syntax \"with\" is not allowed for modules." + +let explain_incorrect_module_application () = + str "Illegal application to a module type." + +open Modintern + +let explain_module_internalization_error = function + | NotAModuleNorModtype s -> explain_not_module_nor_modtype s + | IncorrectWithInModule -> explain_incorrect_with_in_module () + | IncorrectModuleApplication -> explain_incorrect_module_application () (* Typeclass errors *) @@ -525,6 +697,7 @@ let explain_no_instance env (_,id) l = prlist_with_sep pr_spc (pr_lconstr_env env) l let pr_constraints printenv env evm = + let evm = Evd.undefined_evars (Evarutil.nf_evar_map_undefined evm) in let l = Evd.to_list evm in let (ev, evi) = List.hd l in if List.for_all (fun (ev', evi') -> @@ -534,12 +707,14 @@ let pr_constraints printenv env evm = (reset_with_named_context evi.evar_hyps env) in (if printenv then pe ++ fnl () else mt ()) ++ prlist_with_sep (fun () -> fnl ()) - (fun (ev, evi) -> str(string_of_existential ev)++ str " == " ++ pr_constr evi.evar_concl) l + (fun (ev, evi) -> str(string_of_existential ev) ++ + str " : " ++ pr_lconstr evi.evar_concl) l ++ fnl() ++ + pr_evar_map_constraints evm else - pr_evar_map evm + pr_evar_map None evm let explain_unsatisfiable_constraints env evd constr = - let evm = Evarutil.nf_evars evd in + let evm = Evarutil.nf_evar_map evd in let undef = Evd.undefined_evars evm in match constr with | None -> @@ -684,7 +859,7 @@ let error_not_allowed_case_analysis isrec kind i = let error_not_mutual_in_scheme ind ind' = if ind = ind' then str "The inductive type " ++ pr_inductive (Global.env()) ind ++ - str "occurs twice." + str " occurs twice." else str "The inductive types " ++ pr_inductive (Global.env()) ind ++ spc () ++ str "and" ++ spc () ++ pr_inductive (Global.env()) ind' ++ spc () ++ @@ -805,7 +980,7 @@ let explain_reduction_tactic_error = function | Tacred.InvalidAbstraction (env,c,(env',e)) -> str "The abstracted term" ++ spc () ++ pr_lconstr_env_at_top env c ++ spc () ++ str "is not well typed." ++ fnl () ++ - explain_type_error env' e + explain_type_error env' Evd.empty e let explain_ltac_call_trace (nrep,last,trace,loc) = let calls = @@ -831,7 +1006,7 @@ let explain_ltac_call_trace (nrep,last,trace,loc) = let filter = function (id,None) -> None | (id,Some id') -> Some(id,([],mkVar id')) in let unboundvars = list_map_filter filter unboundvars in - quote (pr_rawconstr_env (Global.env()) c) ++ + quote (pr_glob_constr_env (Global.env()) c) ++ (if unboundvars <> [] or vars <> [] then strbrk " (with " ++ prlist_with_sep pr_comma diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli index e12e445c..a763472b 100644 --- a/toplevel/himsg.mli +++ b/toplevel/himsg.mli @@ -1,14 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: himsg.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(*i*) open Pp open Names open Indtypes @@ -19,13 +16,12 @@ open Typeclasses_errors open Indrec open Cases open Logic -(*i*) -(* This module provides functions to explain the type errors. *) +(** This module provides functions to explain the type errors. *) -val explain_type_error : env -> type_error -> std_ppcmds +val explain_type_error : env -> Evd.evar_map -> type_error -> std_ppcmds -val explain_pretype_error : env -> pretype_error -> std_ppcmds +val explain_pretype_error : env -> Evd.evar_map -> pretype_error -> std_ppcmds val explain_inductive_error : inductive_error -> std_ppcmds @@ -44,3 +40,8 @@ val explain_reduction_tactic_error : val explain_ltac_call_trace : int * Proof_type.ltac_call_kind * Proof_type.ltac_trace * Util.loc -> std_ppcmds + +val explain_module_error : Modops.module_typing_error -> std_ppcmds + +val explain_module_internalization_error : + Modintern.module_internalization_error -> std_ppcmds diff --git a/toplevel/ide_intf.ml b/toplevel/ide_intf.ml new file mode 100644 index 00000000..fc8ffa25 --- /dev/null +++ b/toplevel/ide_intf.ml @@ -0,0 +1,434 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** * Interface of calls to Coq by CoqIde *) + +open Xml_parser +open Interface + +type xml = Xml_parser.xml + +(** We use phantom types and GADT to protect ourselves against wild casts *) + +type 'a call = + | Interp of raw * verbose * string + | Rewind of int + | Goal + | Evars + | Hints + | Status + | GetOptions + | SetOptions of (option_name * option_value) list + | InLoadPath of string + | MkCases of string + +(** The actual calls *) + +let interp (r,b,s) : string call = Interp (r,b,s) +let rewind i : int call = Rewind i +let goals : goals option call = Goal +let evars : evar list option call = Evars +let hints : (hint list * hint) option call = Hints +let status : status call = Status +let get_options : (option_name * option_state) list call = GetOptions +let set_options l : unit call = SetOptions l +let inloadpath s : bool call = InLoadPath s +let mkcases s : string list list call = MkCases s + +(** * Coq answers to CoqIde *) + +let abstract_eval_call handler c = + try + let res = match c with + | Interp (r,b,s) -> Obj.magic (handler.interp (r,b,s) : string) + | Rewind i -> Obj.magic (handler.rewind i : int) + | Goal -> Obj.magic (handler.goals () : goals option) + | Evars -> Obj.magic (handler.evars () : evar list option) + | Hints -> Obj.magic (handler.hints () : (hint list * hint) option) + | Status -> Obj.magic (handler.status () : status) + | GetOptions -> Obj.magic (handler.get_options () : (option_name * option_state) list) + | SetOptions opts -> Obj.magic (handler.set_options opts : unit) + | InLoadPath s -> Obj.magic (handler.inloadpath s : bool) + | MkCases s -> Obj.magic (handler.mkcases s : string list list) + in Good res + with e -> + let (l, str) = handler.handle_exn e in + Fail (l,str) + +(** * XML data marshalling *) + +exception Marshal_error + +(** Utility functions *) + +let massoc x l = + try List.assoc x l + with Not_found -> raise Marshal_error + +let constructor t c args = Element (t, ["val", c], args) + +let do_match constr t mf = match constr with +| Element (s, attrs, args) -> + if s = t then + let c = massoc "val" attrs in + mf c args + else raise Marshal_error +| _ -> raise Marshal_error + +let pcdata = function +| PCData s -> s +| _ -> raise Marshal_error + +let singleton = function +| [x] -> x +| _ -> raise Marshal_error + +let raw_string = function +| [] -> "" +| [PCData s] -> s +| _ -> raise Marshal_error + +let bool_arg tag b = if b then [tag, ""] else [] + +(** Base types *) + +let of_bool b = + if b then constructor "bool" "true" [] + else constructor "bool" "false" [] + +let to_bool xml = do_match xml "bool" + (fun s _ -> match s with + | "true" -> true + | "false" -> false + | _ -> raise Marshal_error) + +let of_list f l = + Element ("list", [], List.map f l) + +let to_list f = function +| Element ("list", [], l) -> + List.map f l +| _ -> raise Marshal_error + +let of_option f = function +| None -> Element ("option", ["val", "none"], []) +| Some x -> Element ("option", ["val", "some"], [f x]) + +let to_option f = function +| Element ("option", ["val", "none"], []) -> None +| Element ("option", ["val", "some"], [x]) -> Some (f x) +| _ -> raise Marshal_error + +let of_string s = Element ("string", [], [PCData s]) + +let to_string = function +| Element ("string", [], l) -> raw_string l +| _ -> raise Marshal_error + +let of_int i = Element ("int", [], [PCData (string_of_int i)]) + +let to_int = function +| Element ("int", [], [PCData s]) -> int_of_string s +| _ -> raise Marshal_error + +let of_pair f g (x, y) = Element ("pair", [], [f x; g y]) + +let to_pair f g = function +| Element ("pair", [], [x; y]) -> (f x, g y) +| _ -> raise Marshal_error + +(** More elaborate types *) + +let of_option_value = function +| IntValue i -> + constructor "option_value" "intvalue" [of_option of_int i] +| BoolValue b -> + constructor "option_value" "boolvalue" [of_bool b] +| StringValue s -> + constructor "option_value" "stringvalue" [of_string s] + +let to_option_value xml = do_match xml "option_value" + (fun s args -> match s with + | "intvalue" -> IntValue (to_option to_int (singleton args)) + | "boolvalue" -> BoolValue (to_bool (singleton args)) + | "stringvalue" -> StringValue (to_string (singleton args)) + | _ -> raise Marshal_error + ) + +let of_option_state s = + Element ("option_state", [], [ + of_bool s.opt_sync; + of_bool s.opt_depr; + of_string s.opt_name; + of_option_value s.opt_value] + ) + +let to_option_state = function +| Element ("option_state", [], [sync; depr; name; value]) -> + { + opt_sync = to_bool sync; + opt_depr = to_bool depr; + opt_name = to_string name; + opt_value = to_option_value value; + } +| _ -> raise Marshal_error + +let of_value f = function +| Good x -> Element ("value", ["val", "good"], [f x]) +| Fail (loc, msg) -> + let loc = match loc with + | None -> [] + | Some (s, e) -> [("loc_s", string_of_int s); ("loc_e", string_of_int e)] + in + Element ("value", ["val", "fail"] @ loc, [PCData msg]) + +let to_value f = function +| Element ("value", attrs, l) -> + let ans = massoc "val" attrs in + if ans = "good" then Good (f (singleton l)) + else if ans = "fail" then + let loc = + try + let loc_s = int_of_string (List.assoc "loc_s" attrs) in + let loc_e = int_of_string (List.assoc "loc_e" attrs) in + Some (loc_s, loc_e) + with _ -> None + in + let msg = raw_string l in + Fail (loc, msg) + else raise Marshal_error +| _ -> raise Marshal_error + +let of_call = function +| Interp (raw, vrb, cmd) -> + let flags = (bool_arg "raw" raw) @ (bool_arg "verbose" vrb) in + Element ("call", ("val", "interp") :: flags, [PCData cmd]) +| Rewind n -> + Element ("call", ("val", "rewind") :: ["steps", string_of_int n], []) +| Goal -> + Element ("call", ["val", "goal"], []) +| Evars -> + Element ("call", ["val", "evars"], []) +| Hints -> + Element ("call", ["val", "hints"], []) +| Status -> + Element ("call", ["val", "status"], []) +| GetOptions -> + Element ("call", ["val", "getoptions"], []) +| SetOptions opts -> + let args = List.map (of_pair (of_list of_string) of_option_value) opts in + Element ("call", ["val", "setoptions"], args) +| InLoadPath file -> + Element ("call", ["val", "inloadpath"], [PCData file]) +| MkCases ind -> + Element ("call", ["val", "mkcases"], [PCData ind]) + +let to_call = function +| Element ("call", attrs, l) -> + let ans = massoc "val" attrs in + begin match ans with + | "interp" -> + let raw = List.mem_assoc "raw" attrs in + let vrb = List.mem_assoc "verbose" attrs in + Interp (raw, vrb, raw_string l) + | "rewind" -> + let steps = int_of_string (massoc "steps" attrs) in + Rewind steps + | "goal" -> Goal + | "evars" -> Evars + | "status" -> Status + | "getoptions" -> GetOptions + | "setoptions" -> + let args = List.map (to_pair (to_list to_string) to_option_value) l in + SetOptions args + | "inloadpath" -> InLoadPath (raw_string l) + | "mkcases" -> MkCases (raw_string l) + | "hints" -> Hints + | _ -> raise Marshal_error + end +| _ -> raise Marshal_error + +let of_status s = + let of_so = of_option of_string in + Element ("status", [], [of_so s.status_path; of_so s.status_proofname]) + +let to_status = function +| Element ("status", [], [path; name]) -> + { + status_path = to_option to_string path; + status_proofname = to_option to_string name; + } +| _ -> raise Marshal_error + +let of_evar s = + Element ("evar", [], [PCData s.evar_info]) + +let to_evar = function +| Element ("evar", [], data) -> { evar_info = raw_string data; } +| _ -> raise Marshal_error + +let of_goal g = + let hyp = of_list of_string g.goal_hyp in + let ccl = of_string g.goal_ccl in + Element ("goal", [], [hyp; ccl]) + +let to_goal = function +| Element ("goal", [], [hyp; ccl]) -> + let hyp = to_list to_string hyp in + let ccl = to_string ccl in + { goal_hyp = hyp; goal_ccl = ccl } +| _ -> raise Marshal_error + +let of_goals g = + let fg = of_list of_goal g.fg_goals in + let bg = of_list of_goal g.bg_goals in + Element ("goals", [], [fg; bg]) + +let to_goals = function +| Element ("goals", [], [fg; bg]) -> + let fg = to_list to_goal fg in + let bg = to_list to_goal bg in + { fg_goals = fg; bg_goals = bg; } +| _ -> raise Marshal_error + +let of_hints = + let of_hint = of_list (of_pair of_string of_string) in + of_option (of_pair (of_list of_hint) of_hint) + +let of_answer (q : 'a call) (r : 'a value) = + let convert = match q with + | Interp _ -> Obj.magic (of_string : string -> xml) + | Rewind _ -> Obj.magic (of_int : int -> xml) + | Goal -> Obj.magic (of_option of_goals : goals option -> xml) + | Evars -> Obj.magic (of_option (of_list of_evar) : evar list option -> xml) + | Hints -> Obj.magic (of_hints : (hint list * hint) option -> xml) + | Status -> Obj.magic (of_status : status -> xml) + | GetOptions -> Obj.magic (of_list (of_pair (of_list of_string) of_option_state) : (option_name * option_state) list -> xml) + | SetOptions _ -> Obj.magic (fun _ -> Element ("unit", [], [])) + | InLoadPath _ -> Obj.magic (of_bool : bool -> xml) + | MkCases _ -> Obj.magic (of_list (of_list of_string) : string list list -> xml) + in + of_value convert r + +let to_answer xml = + let rec convert elt = match elt with + | Element (tpe, attrs, l) -> + begin match tpe with + | "unit" -> Obj.magic () + | "string" -> Obj.magic (to_string elt : string) + | "int" -> Obj.magic (to_int elt : int) + | "status" -> Obj.magic (to_status elt : status) + | "bool" -> Obj.magic (to_bool elt : bool) + | "list" -> Obj.magic (to_list convert elt : 'a list) + | "option" -> Obj.magic (to_option convert elt : 'a option) + | "pair" -> Obj.magic (to_pair convert convert elt : ('a * 'b)) + | "goals" -> Obj.magic (to_goals elt : goals) + | "evar" -> Obj.magic (to_evar elt : evar) + | "option_value" -> Obj.magic (to_option_value elt : option_value) + | "option_state" -> Obj.magic (to_option_state elt : option_state) + | _ -> raise Marshal_error + end + | _ -> raise Marshal_error + in + to_value convert xml + +(** * Debug printing *) + +let pr_option_value = function +| IntValue None -> "none" +| IntValue (Some i) -> string_of_int i +| StringValue s -> s +| BoolValue b -> if b then "true" else "false" + +let rec pr_setoptions opts = + let map (key, v) = + let key = String.concat " " key in + key ^ " := " ^ (pr_option_value v) + in + String.concat "; " (List.map map opts) + +let pr_getoptions opts = + let map (key, s) = + let key = String.concat " " key in + Printf.sprintf "%s: sync := %b; depr := %b; name := %s; value := %s\n" + key s.opt_sync s.opt_depr s.opt_name (pr_option_value s.opt_value) + in + "\n" ^ String.concat "" (List.map map opts) + +let pr_call = function + | Interp (r,b,s) -> + let raw = if r then "RAW" else "" in + let verb = if b then "" else "SILENT" in + "INTERP"^raw^verb^" ["^s^"]" + | Rewind i -> "REWIND "^(string_of_int i) + | Goal -> "GOALS" + | Evars -> "EVARS" + | Hints -> "HINTS" + | Status -> "STATUS" + | GetOptions -> "GETOPTIONS" + | SetOptions l -> "SETOPTIONS" ^ " [" ^ pr_setoptions l ^ "]" + | InLoadPath s -> "INLOADPATH "^s + | MkCases s -> "MKCASES "^s + +let pr_value_gen pr = function + | Good v -> "GOOD " ^ pr v + | Fail (_,str) -> "FAIL ["^str^"]" + +let pr_value v = pr_value_gen (fun _ -> "") v + +let pr_string s = "["^s^"]" +let pr_bool b = if b then "true" else "false" + +let pr_status s = + let path = match s.status_path with + | None -> "no path; " + | Some p -> "path = " ^ p ^ "; " + in + let name = match s.status_proofname with + | None -> "no proof;" + | Some n -> "proof = " ^ n ^ ";" + in + "Status: " ^ path ^ name + +let pr_mkcases l = + let l = List.map (String.concat " ") l in + "[" ^ String.concat " | " l ^ "]" + +let pr_goals_aux g = + if g.fg_goals = [] then + if g.bg_goals = [] then "Proof completed." + else Printf.sprintf "Still %i unfocused goals." (List.length g.bg_goals) + else + let pr_menu s = s in + let pr_goal { goal_hyp = hyps; goal_ccl = goal } = + "[" ^ String.concat "; " (List.map pr_menu hyps) ^ " |- " ^ pr_menu goal ^ "]" + in + String.concat " " (List.map pr_goal g.fg_goals) + +let pr_goals = function +| None -> "No proof in progress." +| Some g -> pr_goals_aux g + +let pr_evar ev = "[" ^ ev.evar_info ^ "]" + +let pr_evars = function +| None -> "No proof in progress." +| Some evars -> String.concat " " (List.map pr_evar evars) + +let pr_full_value call value = + match call with + | Interp _ -> pr_value_gen pr_string (Obj.magic value : string value) + | Rewind i -> pr_value_gen string_of_int (Obj.magic value : int value) + | Goal -> pr_value_gen pr_goals (Obj.magic value : goals option value) + | Evars -> pr_value_gen pr_evars (Obj.magic value : evar list option value) + | Hints -> pr_value value + | Status -> pr_value_gen pr_status (Obj.magic value : status value) + | GetOptions -> pr_value_gen pr_getoptions (Obj.magic value : (option_name * option_state) list value) + | SetOptions _ -> pr_value value + | InLoadPath s -> pr_value_gen pr_bool (Obj.magic value : bool value) + | MkCases s -> pr_value_gen pr_mkcases (Obj.magic value : string list list value) diff --git a/toplevel/ide_intf.mli b/toplevel/ide_intf.mli new file mode 100644 index 00000000..69204da1 --- /dev/null +++ b/toplevel/ide_intf.mli @@ -0,0 +1,87 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** * Applicative part of the interface of CoqIde calls to Coq *) + +open Interface + +type xml = Xml_parser.xml + +type 'a call + +(** Running a command (given as a string). + - The 1st flag indicates whether to use "raw" mode + (less sanity checks, no impact on the undo stack). + Suitable e.g. for queries, or for the Set/Unset + of display options that coqide performs all the time. + - The 2nd flag controls the verbosity. + - The returned string contains the messages produced + by this command, but not the updated goals (they are + to be fetch by a separated [current_goals]). *) +val interp : raw * verbose * string -> string call + +(** Backtracking by at least a certain number of phrases. + No finished proofs will be re-opened. Instead, + we continue backtracking until before these proofs, + and answer the amount of extra backtracking performed. + Backtracking by more than the number of phrases already + interpreted successfully (and not yet undone) will fail. *) +val rewind : int -> int call + +(** Fetching the list of current goals. Return [None] if no proof is in + progress, [Some gl] otherwise. *) +val goals : goals option call + +(** Retrieving the tactics applicable to the current goal. [None] if there is + no proof in progress. *) +val hints : (hint list * hint) option call + +(** The status, for instance "Ready in SomeSection, proving Foo" *) +val status : status call + +(** Is a directory part of Coq's loadpath ? *) +val inloadpath : string -> bool call + +(** Create a "match" template for a given inductive type. + For each branch of the match, we list the constructor name + followed by enough pattern variables. *) +val mkcases : string -> string list list call + +(** Retrieve the list of unintantiated evars in the current proof. [None] if no + proof is in progress. *) +val evars : evar list option call + +(** Retrieve the list of options of the current toplevel, together with their + state. *) +val get_options : (option_name * option_state) list call + +(** Set the options to the given value. Warning: this is not atomic, so whenever + the call fails, the option state can be messed up... This is the caller duty + to check that everything is correct. *) +val set_options : (option_name * option_value) list -> unit call + +val abstract_eval_call : handler -> 'a call -> 'a value + +(** * XML data marshalling *) + +exception Marshal_error + +val of_value : ('a -> xml) -> 'a value -> xml +val to_value : (xml -> 'a) -> xml -> 'a value + +val of_call : 'a call -> xml +val to_call : xml -> 'a call + +val of_answer : 'a call -> 'a value -> xml +val to_answer : xml -> 'a value + +(** * Debug printing *) + +val pr_call : 'a call -> string +val pr_value : 'a value -> string +val pr_full_value : 'a call -> 'a value -> string diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml new file mode 100644 index 00000000..42ecb75b --- /dev/null +++ b/toplevel/ide_slave.ml @@ -0,0 +1,579 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Vernacexpr +open Names +open Compat +open Util +open Pp +open Printer +open Namegen + +(** Ide_slave : an implementation of [Interface], i.e. mainly an interp + function and a rewind function. This specialized loop is triggered + when the -ideslave option is passed to Coqtop. Currently CoqIDE is + the only one using this mode, but we try here to be as generic as + possible, so this may change in the future... *) + + +(** Comment the next line for displaying some more debug messages *) + +let prerr_endline _ = () + + +(** Signal handling: we postpone ^C during input and output phases, + but make it directly raise a Sys.Break during evaluation of the request. *) + +let catch_break = ref false + +let init_signal_handler () = + let f _ = if !catch_break then raise Sys.Break else Util.interrupt := true in + Sys.set_signal Sys.sigint (Sys.Signal_handle f) + + +(** Redirection of standard output to a printable buffer *) + +let orig_stdout = ref stdout + +let init_stdout,read_stdout = + let out_buff = Buffer.create 100 in + let out_ft = Format.formatter_of_buffer out_buff in + let deep_out_ft = Format.formatter_of_buffer out_buff in + let _ = Pp_control.set_gp deep_out_ft Pp_control.deep_gp in + (fun () -> + flush_all (); + orig_stdout := Unix.out_channel_of_descr (Unix.dup Unix.stdout); + Unix.dup2 Unix.stderr Unix.stdout; + Pp_control.std_ft := out_ft; + Pp_control.err_ft := out_ft; + Pp_control.deep_ft := deep_out_ft; + set_binary_mode_out !orig_stdout true; + set_binary_mode_in stdin true; + ), + (fun () -> Format.pp_print_flush out_ft (); + let r = Buffer.contents out_buff in + Buffer.clear out_buff; r) + + +(** Categories of commands *) + +let coqide_known_option table = List.mem table [ + ["Printing";"Implicit"]; + ["Printing";"Coercions"]; + ["Printing";"Matching"]; + ["Printing";"Synth"]; + ["Printing";"Notations"]; + ["Printing";"All"]; + ["Printing";"Records"]; + ["Printing";"Existential";"Instances"]; + ["Printing";"Universes"]] + +type command_attribute = + NavigationCommand | QueryCommand | DebugCommand | KnownOptionCommand + | OtherStatePreservingCommand | GoalStartingCommand | SolveCommand + | ProofEndingCommand + +let rec attribute_of_vernac_command = function + (* Control *) + | VernacTime com -> attribute_of_vernac_command com + | VernacTimeout(_,com) -> attribute_of_vernac_command com + | VernacFail com -> attribute_of_vernac_command com + | VernacList _ -> [] (* unsupported *) + | VernacLoad _ -> [] + + (* Syntax *) + | VernacTacticNotation _ -> [] + | VernacSyntaxExtension _ -> [] + | VernacDelimiters _ -> [] + | VernacBindScope _ -> [] + | VernacOpenCloseScope _ -> [] + | VernacArgumentsScope _ -> [] + | VernacInfix _ -> [] + | VernacNotation _ -> [] + + (* Gallina *) + | VernacDefinition (_,_,DefineBody _,_) -> [] + | VernacDefinition (_,_,ProveBody _,_) -> [GoalStartingCommand] + | VernacStartTheoremProof _ -> [GoalStartingCommand] + | VernacEndProof _ -> [ProofEndingCommand] + | VernacExactProof _ -> [ProofEndingCommand] + + | VernacAssumption _ -> [] + | VernacInductive _ -> [] + | VernacFixpoint _ -> [] + | VernacCoFixpoint _ -> [] + | VernacScheme _ -> [] + | VernacCombinedScheme _ -> [] + + (* Modules *) + | VernacDeclareModule _ -> [] + | VernacDefineModule _ -> [] + | VernacDeclareModuleType _ -> [] + | VernacInclude _ -> [] + + (* Gallina extensions *) + | VernacBeginSection _ -> [] + | VernacEndSegment _ -> [] + | VernacRequire _ -> [] + | VernacImport _ -> [] + | VernacCanonical _ -> [] + | VernacCoercion _ -> [] + | VernacIdentityCoercion _ -> [] + + (* Type classes *) + | VernacInstance _ -> [] + | VernacContext _ -> [] + | VernacDeclareInstances _ -> [] + | VernacDeclareClass _ -> [] + + (* Solving *) + | VernacSolve _ -> [SolveCommand] + | VernacSolveExistential _ -> [SolveCommand] + + (* Auxiliary file and library management *) + | VernacRequireFrom _ -> [] + | VernacAddLoadPath _ -> [] + | VernacRemoveLoadPath _ -> [] + | VernacAddMLPath _ -> [] + | VernacDeclareMLModule _ -> [] + | VernacChdir o -> + (* TODO: [Chdir d] is currently not undo-able (not stored in coq state). + But if we register [Chdir] in the state, loading [initial.coq] will + wrongly cd to the compile-time directory at each coqtop launch. *) + if o = None then [QueryCommand] else [] + + (* State management *) + | VernacWriteState _ -> [] + | VernacRestoreState _ -> [] + + (* Resetting *) + | VernacRemoveName _ -> [NavigationCommand] + | VernacResetName _ -> [NavigationCommand] + | VernacResetInitial -> [NavigationCommand] + | VernacBack _ -> [NavigationCommand] + | VernacBackTo _ -> [NavigationCommand] + + (* Commands *) + | VernacDeclareTacticDefinition _ -> [] + | VernacCreateHintDb _ -> [] + | VernacRemoveHints _ -> [] + | VernacHints _ -> [] + | VernacSyntacticDefinition _ -> [] + | VernacDeclareImplicits _ -> [] + | VernacArguments _ -> [] + | VernacDeclareReduction _ -> [] + | VernacReserve _ -> [] + | VernacGeneralizable _ -> [] + | VernacSetOpacity _ -> [] + | VernacSetOption (_,["Ltac";"Debug"], _) -> [DebugCommand] + | VernacSetOption (_,o,BoolValue true) | VernacUnsetOption (_,o) -> + if coqide_known_option o then [KnownOptionCommand] else [] + | VernacSetOption _ -> [] + | VernacRemoveOption _ -> [] + | VernacAddOption _ -> [] + | VernacMemOption _ -> [QueryCommand] + + | VernacPrintOption _ -> [QueryCommand] + | VernacCheckMayEval _ -> [QueryCommand] + | VernacGlobalCheck _ -> [QueryCommand] + | VernacPrint _ -> [QueryCommand] + | VernacSearch _ -> [QueryCommand] + | VernacLocate _ -> [QueryCommand] + + | VernacComments _ -> [OtherStatePreservingCommand] + | VernacNop -> [OtherStatePreservingCommand] + + (* Proof management *) + | VernacGoal _ -> [GoalStartingCommand] + + | VernacAbort _ -> [] + | VernacAbortAll -> [NavigationCommand] + | VernacRestart -> [NavigationCommand] + | VernacSuspend -> [NavigationCommand] + | VernacResume _ -> [NavigationCommand] + | VernacUndo _ -> [NavigationCommand] + | VernacUndoTo _ -> [NavigationCommand] + | VernacBacktrack _ -> [NavigationCommand] + + | VernacFocus _ -> [SolveCommand] + | VernacUnfocus -> [SolveCommand] + | VernacShow _ -> [OtherStatePreservingCommand] + | VernacCheckGuard -> [OtherStatePreservingCommand] + | VernacProof (None, None) -> [OtherStatePreservingCommand] + | VernacProof _ -> [] + + | VernacProofMode _ -> [] + | VernacBullet _ -> [SolveCommand] + | VernacSubproof _ -> [SolveCommand] + | VernacEndSubproof -> [SolveCommand] + + (* Toplevel control *) + | VernacToplevelControl _ -> [] + + (* Extensions *) + | VernacExtend ("Subtac_Obligations", _) -> [GoalStartingCommand] + | VernacExtend _ -> [] + +let is_vernac_navigation_command com = + List.mem NavigationCommand (attribute_of_vernac_command com) + +let is_vernac_query_command com = + List.mem QueryCommand (attribute_of_vernac_command com) + +let is_vernac_known_option_command com = + List.mem KnownOptionCommand (attribute_of_vernac_command com) + +let is_vernac_debug_command com = + List.mem DebugCommand (attribute_of_vernac_command com) + +let is_vernac_goal_printing_command com = + let attribute = attribute_of_vernac_command com in + List.mem GoalStartingCommand attribute or + List.mem SolveCommand attribute + +let is_vernac_state_preserving_command com = + let attribute = attribute_of_vernac_command com in + List.mem OtherStatePreservingCommand attribute or + List.mem QueryCommand attribute + +let is_vernac_tactic_command com = + List.mem SolveCommand (attribute_of_vernac_command com) + +let is_vernac_proof_ending_command com = + List.mem ProofEndingCommand (attribute_of_vernac_command com) + + +(** Command history stack + + We maintain a stack of the past states of the system. Each + successfully interpreted command adds a [reset_info] element + to this stack, storing what were the (label / open proofs / + current proof depth) just _before_ the interpretation of this + command. A label is just an integer (cf. BackTo and Bactrack + vernac commands). +*) + +type reset_info = { label : int; proofs : identifier list; depth : int } + +let com_stk = Stack.create () + +let compute_reset_info () = + { label = Lib.current_command_label (); + proofs = Pfedit.get_all_proof_names (); + depth = max 0 (Pfedit.current_proof_depth ()) } + + +(** Interpretation (cf. [Ide_intf.interp]) *) + +(** Check whether a command is forbidden by CoqIDE *) + +let coqide_cmd_checks (loc,ast) = + let user_error s = + raise (Loc.Exc_located (loc, Util.UserError ("CoqIde", str s))) + in + if is_vernac_debug_command ast then + user_error "Debug mode not available within CoqIDE"; + if is_vernac_navigation_command ast then + user_error "Use CoqIDE navigation instead"; + if is_vernac_known_option_command ast then + user_error "Use CoqIDE display menu instead"; + if is_vernac_query_command ast then + msgerrnl (str "Warning: query commands should not be inserted in scripts") + +let raw_eval_expr = Vernac.eval_expr + +let eval_expr loc_ast = + let rewind_info = compute_reset_info () in + raw_eval_expr loc_ast; + Stack.push rewind_info com_stk + +let interp (raw,verbosely,s) = + if not raw then (prerr_endline "Starting interp..."; prerr_endline s); + let pa = Pcoq.Gram.parsable (Stream.of_string s) in + let loc_ast = Vernac.parse_sentence (pa,None) in + if not raw then coqide_cmd_checks loc_ast; + (* We run tactics silently, since we will query the goal state later. + Otherwise, we honor the IDE verbosity flag. *) + Flags.make_silent + (is_vernac_goal_printing_command (snd loc_ast) || not verbosely); + if raw then raw_eval_expr loc_ast else eval_expr loc_ast; + Flags.make_silent true; + if not raw then prerr_endline ("...Done with interp of : "^s); + read_stdout () + + +(** Backtracking (cf. [Ide_intf.rewind]). + We now rely on the [Backtrack] command just as ProofGeneral. *) + +let rewind count = + if count = 0 then 0 + else + let current_proofs = Pfedit.get_all_proof_names () + in + (* 1) First, let's pop the history stack exactly [count] times. + NB: Normally, the IDE will not rewind by more than the numbers + of already interpreted commands, hence no risk of [Stack.Empty]. + *) + let initial_target = + for i = 1 to count - 1 do ignore (Stack.pop com_stk) done; + Stack.pop com_stk + in + (* 2) Backtrack by enough additional steps to avoid re-opening proofs. + Typically, when a Qed has been crossed, we backtrack to the proof start. + NB: We cannot reach the empty stack, since the oldest [reset_info] + in the history cannot have opened proofs. + *) + let already_opened p = List.mem p current_proofs in + let rec extra_back n target = + if List.for_all already_opened target.proofs then n,target + else extra_back (n+1) (Stack.pop com_stk) + in + let extra_count, target = extra_back 0 initial_target + in + (* 3) Now that [target.proofs] is a subset of the opened proofs before + the rewind, we simply abort the extra proofs (if any). + NB: It is critical here that proofs are nested in a regular way + (i.e. no Resume or Suspend, as enforced above). This way, we can simply + count the extra proofs to abort instead of taking care of their names. + *) + let naborts = List.length current_proofs - List.length target.proofs + in + (* 4) We are now ready to call [Backtrack] *) + prerr_endline ("Rewind to state "^string_of_int target.label^ + ", proof depth "^string_of_int target.depth^ + ", num of aborts "^string_of_int naborts); + Vernacentries.vernac_backtrack target.label target.depth naborts; + Lib.mark_end_of_command (); (* We've short-circuited Vernac.eval_expr *) + extra_count + + +(** Goal display *) + +let hyp_next_tac sigma env (id,_,ast) = + let id_s = Names.string_of_id id in + let type_s = string_of_ppcmds (pr_ltype_env env ast) in + [ + ("clear "^id_s),("clear "^id_s^".\n"); + ("apply "^id_s),("apply "^id_s^".\n"); + ("exact "^id_s),("exact "^id_s^".\n"); + ("generalize "^id_s),("generalize "^id_s^".\n"); + ("absurd <"^id_s^">"),("absurd "^type_s^".\n") + ] @ (if Hipattern.is_equality_type ast then [ + ("discriminate "^id_s),("discriminate "^id_s^".\n"); + ("injection "^id_s),("injection "^id_s^".\n") + ] else []) @ (if Hipattern.is_equality_type (snd (Reductionops.splay_prod env sigma ast)) then [ + ("rewrite "^id_s),("rewrite "^id_s^".\n"); + ("rewrite <- "^id_s),("rewrite <- "^id_s^".\n") + ] else []) @ [ + ("elim "^id_s), ("elim "^id_s^".\n"); + ("inversion "^id_s), ("inversion "^id_s^".\n"); + ("inversion clear "^id_s), ("inversion_clear "^id_s^".\n") + ] + +let concl_next_tac sigma concl = + let expand s = (s,s^".\n") in + List.map expand ([ + "intro"; + "intros"; + "intuition" + ] @ (if Hipattern.is_equality_type (Goal.V82.concl sigma concl) then [ + "reflexivity"; + "discriminate"; + "symmetry" + ] else []) @ [ + "assumption"; + "omega"; + "ring"; + "auto"; + "eauto"; + "tauto"; + "trivial"; + "decide equality"; + "simpl"; + "subst"; + "red"; + "split"; + "left"; + "right" + ]) + +let process_goal sigma g = + let env = Goal.V82.env sigma g in + let ccl = + let norm_constr = Reductionops.nf_evar sigma (Goal.V82.concl sigma g) in + string_of_ppcmds (pr_ltype_env_at_top env norm_constr) in + let process_hyp h_env d acc = + let d = Term.map_named_declaration (Reductionops.nf_evar sigma) d in + (string_of_ppcmds (pr_var_decl h_env d)) :: acc in +(* (string_of_ppcmds (pr_var_decl h_env d), hyp_next_tac sigma h_env d)::acc in *) + let hyps = + List.rev (Environ.fold_named_context process_hyp env ~init: []) in + { Interface.goal_hyp = hyps; Interface.goal_ccl = ccl } +(* hyps,(ccl,concl_next_tac sigma g)) *) + +let goals () = + try + let pfts = Proof_global.give_me_the_proof () in + let { Evd.it = all_goals ; sigma = sigma } = Proof.V82.subgoals pfts in + let fg = List.map (process_goal sigma) all_goals in + let { Evd.it = bgoals ; sigma = sigma } = Proof.V82.background_subgoals pfts in + let bg = List.map (process_goal sigma) bgoals in + Some { Interface.fg_goals = fg; Interface.bg_goals = bg; } + with Proof_global.NoCurrentProof -> None + +let evars () = + try + let pfts = Proof_global.give_me_the_proof () in + let { Evd.it = all_goals ; sigma = sigma } = Proof.V82.subgoals pfts in + let exl = Evarutil.non_instantiated sigma in + let map_evar ev = { Interface.evar_info = string_of_ppcmds (pr_evar ev); } in + let el = List.map map_evar exl in + Some el + with Proof_global.NoCurrentProof -> None + +let hints () = + try + let pfts = Proof_global.give_me_the_proof () in + let { Evd.it = all_goals ; sigma = sigma } = Proof.V82.subgoals pfts in + match all_goals with + | [] -> None + | g :: _ -> + let env = Goal.V82.env sigma g in + let hint_goal = concl_next_tac sigma g in + let get_hint_hyp env d accu = hyp_next_tac sigma env d :: accu in + let hint_hyps = List.rev (Environ.fold_named_context get_hint_hyp env ~init: []) in + Some (hint_hyps, hint_goal) + with Proof_global.NoCurrentProof -> None + +(** Other API calls *) + +let inloadpath dir = + Library.is_in_load_paths (System.physical_path_of_string dir) + +let status () = + (** We remove the initial part of the current [dir_path] + (usually Top in an interactive session, cf "coqtop -top"), + and display the other parts (opened sections and modules) *) + let path = + let l = Names.repr_dirpath (Lib.cwd ()) in + let l = snd (Util.list_sep_last l) in + if l = [] then None + else Some (Names.string_of_dirpath (Names.make_dirpath l)) + in + let proof = + try + Some (Names.string_of_id (Pfedit.get_current_proof_name ())) + with _ -> None + in + { Interface.status_path = path; Interface.status_proofname = proof } + +let get_options () = + let table = Goptions.get_tables () in + let fold key state accu = (key, state) :: accu in + Goptions.OptionMap.fold fold table [] + +let set_options options = + let iter (name, value) = match value with + | BoolValue b -> Goptions.set_bool_option_value name b + | IntValue i -> Goptions.set_int_option_value name i + | StringValue s -> Goptions.set_string_option_value name s + in + List.iter iter options + +(** Grouping all call handlers together + error handling *) + +let eval_call c = + let rec handle_exn e = + catch_break := false; + let pr_exn e = string_of_ppcmds (Errors.print e) in + match e with + | Vernacexpr.Drop -> None, "Drop is not allowed by coqide!" + | Vernacexpr.Quit -> None, "Quit is not allowed by coqide!" + | Vernac.DuringCommandInterp (_,inner) -> handle_exn inner + | Error_in_file (_,_,inner) -> None, pr_exn inner + | Loc.Exc_located (loc, inner) when loc = dummy_loc -> None, pr_exn inner + | Loc.Exc_located (loc, inner) -> Some (Util.unloc loc), pr_exn inner + | e -> None, pr_exn e + in + let interruptible f x = + catch_break := true; + Util.check_for_interrupt (); + let r = f x in + catch_break := false; + r + in + let handler = { + Interface.interp = interruptible interp; + Interface.rewind = interruptible rewind; + Interface.goals = interruptible goals; + Interface.evars = interruptible evars; + Interface.hints = interruptible hints; + Interface.status = interruptible status; + Interface.inloadpath = interruptible inloadpath; + Interface.get_options = interruptible get_options; + Interface.set_options = interruptible set_options; + Interface.mkcases = interruptible Vernacentries.make_cases; + Interface.handle_exn = handle_exn; } + in + (* If the messages of last command are still there, we remove them *) + ignore (read_stdout ()); + Ide_intf.abstract_eval_call handler c + + +(** The main loop *) + +(** Exceptions during eval_call should be converted into [Interface.Fail] + messages by [handle_exn] above. Otherwise, we die badly, after having + tried to send a last message to the ide: trying to recover from errors + with the current protocol would most probably bring desynchronisation + between coqtop and ide. With marshalling, reading an answer to + a different request could hang the ide... *) + +let pr_debug s = + if !Flags.debug then Printf.eprintf "[pid %d] %s\n%!" (Unix.getpid ()) s + +let fail err = + Ide_intf.of_value (fun _ -> assert false) (Interface.Fail (None, err)) + +let loop () = + let p = Xml_parser.make () in + let () = Xml_parser.check_eof p false in + init_signal_handler (); + catch_break := false; + (* ensure we have a command separator object (DOT) so that the first + command can be reseted. *) + Lib.mark_end_of_command(); + try + while true do + let xml_answer = + try + let xml_query = Xml_parser.parse p (Xml_parser.SChannel stdin) in + let q = Ide_intf.to_call xml_query in + let () = pr_debug ("<-- " ^ Ide_intf.pr_call q) in + let r = eval_call q in + let () = pr_debug ("--> " ^ Ide_intf.pr_full_value q r) in + Ide_intf.of_answer q r + with + | Xml_parser.Error (err, loc) -> + let msg = "Syntax error in query: " ^ Xml_parser.error_msg err in + fail msg + | Ide_intf.Marshal_error -> + fail "Incorrect query." + in + Xml_utils.print_xml !orig_stdout xml_answer; + flush !orig_stdout + done + with e -> + let msg = Printexc.to_string e in + let r = "Fatal exception in coqtop:\n" ^ msg in + pr_debug ("==> " ^ r); + (try + Xml_utils.print_xml !orig_stdout (fail r); + flush !orig_stdout + with _ -> ()); + exit 1 diff --git a/toplevel/ide_slave.mli b/toplevel/ide_slave.mli new file mode 100644 index 00000000..13dff280 --- /dev/null +++ b/toplevel/ide_slave.mli @@ -0,0 +1,17 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** [Ide_slave] : an implementation of [Ide_intf], i.e. mainly an interp + function and a rewind function. This specialized loop is triggered + when the -ideslave option is passed to Coqtop. Currently CoqIDE is + the only one using this mode, but we try here to be as generic as + possible, so this may change in the future... *) + +val init_stdout : unit -> unit + +val loop : unit -> unit diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml index 53c3bcea..de3b62f8 100644 --- a/toplevel/ind_tables.ml +++ b/toplevel/ind_tables.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ind_tables.ml 14641 2011-11-06 11:59:10Z herbelin $ i*) - (* File created by Vincent Siles, Oct 2007, extended into a generic support for generation of inductive schemes by Hugo Herbelin, Nov 2009 *) @@ -53,7 +51,7 @@ let discharge_scheme (_,(kind,l)) = Some (kind,Array.map (fun (ind,const) -> (Lib.discharge_inductive ind,Lib.discharge_con const)) l) -let (inScheme,_) = +let inScheme : string * (inductive * constant) array -> obj = declare_object {(default_object "SCHEME") with cache_function = cache_scheme; load_function = (fun _ -> cache_scheme); @@ -111,21 +109,28 @@ let declare_individual_scheme_object s ?(aux="") f = let declare_scheme kind indcl = Lib.add_anonymous_leaf (inScheme (kind,indcl)) +let is_visible_name id = + try ignore (Nametab.locate (Libnames.qualid_of_ident id)); true + with Not_found -> false + +let compute_name internal id = + match internal with + | KernelVerbose | UserVerbose -> id + | KernelSilent -> + Namegen.next_ident_away_from (add_prefix "internal_" id) is_visible_name + let define internal id c = - (* TODO: specify even more by distinguish between KernelVerbose and - * UserVerbose *) - let fd = match internal with - | KernelSilent -> declare_internal_constant - | _ -> declare_constant in + let fd = declare_constant ~internal in + let id = compute_name internal id in let kn = fd id (DefinitionEntry { const_entry_body = c; + const_entry_secctx = None; const_entry_type = None; - const_entry_opaque = false; - const_entry_boxed = Flags.boxed_definitions() }, + const_entry_opaque = false }, Decl_kinds.IsDefinition Scheme) in (match internal with - | KernelSilent -> () + | KernelSilent -> () | _-> definition_message id); kn diff --git a/toplevel/ind_tables.mli b/toplevel/ind_tables.mli index e6f5e77a..96096d47 100644 --- a/toplevel/ind_tables.mli +++ b/toplevel/ind_tables.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -13,10 +13,10 @@ open Mod_subst open Sign open Declarations -(* This module provides support for registering inductive scheme builders, +(** This module provides support for registering inductive scheme builders, declaring schemes and generating schemes on demand *) -(* A scheme is either a "mutual scheme_kind" or an "individual scheme_kind" *) +(** A scheme is either a "mutual scheme_kind" or an "individual scheme_kind" *) type mutual type individual @@ -25,7 +25,7 @@ type 'a scheme_kind type mutual_scheme_object_function = mutual_inductive -> constr array type individual_scheme_object_function = inductive -> constr -(* Main functions to register a scheme builder *) +(** Main functions to register a scheme builder *) val declare_mutual_scheme_object : string -> ?aux:string -> mutual_scheme_object_function -> mutual scheme_kind @@ -37,16 +37,16 @@ val declare_individual_scheme_object : string -> ?aux:string -> val declare_scheme : 'a scheme_kind -> (inductive * constant) array -> unit *) -(* Force generation of a (mutually) scheme with possibly user-level names *) +(** Force generation of a (mutually) scheme with possibly user-level names *) val define_individual_scheme : individual scheme_kind -> - Declare.internal_flag (* internal *) -> + Declare.internal_flag (** internal *) -> identifier option -> inductive -> constant -val define_mutual_scheme : mutual scheme_kind -> Declare.internal_flag (* internal *) -> +val define_mutual_scheme : mutual scheme_kind -> Declare.internal_flag (** internal *) -> (int * identifier) list -> mutual_inductive -> constant array -(* Main function to retrieve a scheme in the cache or to generate it *) +(** Main function to retrieve a scheme in the cache or to generate it *) val find_scheme : 'a scheme_kind -> inductive -> constant val check_scheme : 'a scheme_kind -> inductive -> bool diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index 3596085f..51eddbae 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: indschemes.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - (* Created by Hugo Herbelin from contents related to inductive schemes initially developed by Christine Paulin (induction schemes), Vincent Siles (decidable equality and boolean equality) and Matthieu Sozeau @@ -49,6 +47,7 @@ let elim_flag = ref true let _ = declare_bool_option { optsync = true; + optdepr = false; optname = "automatic declaration of induction schemes"; optkey = ["Elimination";"Schemes"]; optread = (fun () -> !elim_flag) ; @@ -58,6 +57,7 @@ let case_flag = ref false let _ = declare_bool_option { optsync = true; + optdepr = false; optname = "automatic declaration of case analysis schemes"; optkey = ["Case";"Analysis";"Schemes"]; optread = (fun () -> !case_flag) ; @@ -67,6 +67,7 @@ let eq_flag = ref false let _ = declare_bool_option { optsync = true; + optdepr = false; optname = "automatic declaration of boolean equality"; optkey = ["Boolean";"Equality";"Schemes"]; optread = (fun () -> !eq_flag) ; @@ -74,6 +75,7 @@ let _ = let _ = (* compatibility *) declare_bool_option { optsync = true; + optdepr = true; optname = "automatic declaration of boolean equality"; optkey = ["Equality";"Scheme"]; optread = (fun () -> !eq_flag) ; @@ -81,10 +83,11 @@ let _ = (* compatibility *) let is_eq_flag () = !eq_flag && Flags.version_strictly_greater Flags.V8_2 -let eq_dec_flag = ref false +let eq_dec_flag = ref false let _ = declare_bool_option { optsync = true; + optdepr = false; optname = "automatic declaration of decidable equality"; optkey = ["Decidable";"Equality";"Schemes"]; optread = (fun () -> !eq_dec_flag) ; @@ -94,6 +97,7 @@ let rewriting_flag = ref false let _ = declare_bool_option { optsync = true; + optdepr = false; optname ="automatic declaration of rewriting schemes for equality types"; optkey = ["Rewriting";"Schemes"]; optread = (fun () -> !rewriting_flag) ; @@ -102,16 +106,13 @@ let _ = (* Util *) let define id internal c t = - (* TODO: specify even more by distinguish KernelVerbose and UserVerbose *) - let f = match internal with - | KernelSilent -> declare_internal_constant - | _ -> declare_constant in + let f = declare_constant ~internal in let kn = f id (DefinitionEntry { const_entry_body = c; + const_entry_secctx = None; const_entry_type = t; - const_entry_opaque = false; - const_entry_boxed = Flags.boxed_definitions() }, + const_entry_opaque = false }, Decl_kinds.IsDefinition Scheme) in definition_message id; kn @@ -127,7 +128,7 @@ let alarm what internal msg = | KernelVerbose | KernelSilent -> (if debug then - Flags.if_verbose Pp.msg_warning + Flags.if_warn Pp.msg_warning (hov 0 msg ++ fnl () ++ what ++ str " not defined.")) | _ -> errorlabstrm "" msg @@ -158,7 +159,7 @@ let try_declare_scheme what f internal names kn = (strbrk "Required constant " ++ str s ++ str " undefined.") | AlreadyDeclared msg -> alarm what internal (msg ++ str ".") - | _ -> + | _ -> alarm what internal (str "Unknown exception during scheme creation.") @@ -173,7 +174,7 @@ let declare_beq_scheme_with l kn = try_declare_scheme (beq_scheme_msg kn) declare_beq_scheme_gen UserVerbose l kn let try_declare_beq_scheme kn = - (* TODO: handle Fix, see e.g. TheoryList.In_spec, eventually handle + (* TODO: handle Fix, eventually handle proof-irrelevance; improve decidability by depending on decidability for the parameters rather than on the bl and lb properties *) try_declare_scheme (beq_scheme_msg kn) declare_beq_scheme_gen KernelVerbose [] kn diff --git a/toplevel/indschemes.mli b/toplevel/indschemes.mli index 707b9e00..87aedc7b 100644 --- a/toplevel/indschemes.mli +++ b/toplevel/indschemes.mli @@ -1,56 +1,52 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: indschemes.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(*i*) open Util open Names open Term open Environ open Libnames -open Rawterm +open Glob_term open Genarg open Vernacexpr open Ind_tables -(*i*) -(* See also Auto_ind_decl, Indrec, Eqscheme, Ind_tables, ... *) +(** See also Auto_ind_decl, Indrec, Eqscheme, Ind_tables, ... *) -(* Build and register the boolean equalities associated to an inductive type *) +(** Build and register the boolean equalities associated to an inductive type *) val declare_beq_scheme : mutual_inductive -> unit val declare_eq_decidability : mutual_inductive -> unit -(* Build and register a congruence scheme for an equality-like inductive type *) +(** Build and register a congruence scheme for an equality-like inductive type *) val declare_congr_scheme : inductive -> unit -(* Build and register rewriting schemes for an equality-like inductive type *) +(** Build and register rewriting schemes for an equality-like inductive type *) val declare_rewriting_schemes : inductive -> unit -(* Mutual Minimality/Induction scheme *) +(** Mutual Minimality/Induction scheme *) val do_mutual_induction_scheme : - (identifier located * bool * inductive * rawsort) list -> unit + (identifier located * bool * inductive * glob_sort) list -> unit -(* Main calls to interpret the Scheme command *) +(** Main calls to interpret the Scheme command *) val do_scheme : (identifier located option * scheme) list -> unit -(* Combine a list of schemes into a conjunction of them *) +(** Combine a list of schemes into a conjunction of them *) val build_combined_scheme : env -> constant list -> constr * types val do_combined_scheme : identifier located -> identifier located list -> unit -(* Hook called at each inductive type definition *) +(** Hook called at each inductive type definition *) val declare_default_schemes : mutual_inductive -> unit diff --git a/toplevel/interface.mli b/toplevel/interface.mli new file mode 100644 index 00000000..e1410f5b --- /dev/null +++ b/toplevel/interface.mli @@ -0,0 +1,87 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** * Declarative part of the interface of CoqIde calls to Coq *) + +(** * Generic structures *) + +type raw = bool +type verbose = bool + +(** The type of coqtop goals *) +type goal = { + goal_hyp : string list; + (** List of hypotheses *) + goal_ccl : string; + (** Goal conclusion *) +} + +type evar = { + evar_info : string; + (** A string describing an evar: type, number, environment *) +} + +type status = { + status_path : string option; + (** Module path of the current proof *) + status_proofname : string option; + (** Current proof name. [None] if no proof is in progress *) +} + +type goals = { + fg_goals : goal list; + (** List of the focussed goals *) + bg_goals : goal list; + (** List of the background goals *) +} + +type hint = (string * string) list +(** A list of tactics applicable and their appearance *) + +type option_name = Goptionstyp.option_name + +type option_value = Goptionstyp.option_value = + | BoolValue of bool + | IntValue of int option + | StringValue of string + +(** Summary of an option status *) +type option_state = Goptionstyp.option_state = { + opt_sync : bool; + (** Whether an option is synchronous *) + opt_depr : bool; + (** Wheter an option is deprecated *) + opt_name : string; + (** A short string that is displayed when using [Test] *) + opt_value : option_value; + (** The current value of the option *) +} + +(** * Coq answers to CoqIde *) + +type location = (int * int) option (* start and end of the error *) + +type 'a value = + | Good of 'a + | Fail of (location * string) + +(** * The structure that coqtop should implement *) + +type handler = { + interp : raw * verbose * string -> string; + rewind : int -> int; + goals : unit -> goals option; + evars : unit -> evar list option; + hints : unit -> (hint list * hint) option; + status : unit -> status; + get_options : unit -> (option_name * option_state) list; + set_options : (option_name * option_value) list -> unit; + inloadpath : string -> bool; + mkcases : string -> string list list; + handle_exn : exn -> location * string; +} diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml index 8ef82105..7704449f 100644 --- a/toplevel/lemmas.ml +++ b/toplevel/lemmas.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: lemmas.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - (* Created by Hugo Herbelin from contents related to lemma proofs in file command.ml, Aug 2009 *) @@ -41,8 +39,8 @@ let retrieve_first_recthm = function | VarRef id -> (pi2 (Global.lookup_named id),variable_opacity id) | ConstRef cst -> - let {const_body=body;const_opaque=opaq} = Global.lookup_constant cst in - (Option.map Declarations.force body,opaq) + let cb = Global.lookup_constant cst in + (Option.map Declarations.force (body_of_constant cb), is_opaque cb) | _ -> assert false let adjust_guardness_conditions const = function @@ -126,13 +124,13 @@ let find_mutually_recursive_statements thms = assert (rest=[]); (* One occ. of common coind ccls and no common inductive hyps *) if common_same_indhyp <> [] then - if_verbose warning "Assuming mutual coinductive statements."; + if_verbose msgnl (str "Assuming mutual coinductive statements."); flush_all (); indccl, true, [] | [], _::_ -> if same_indccl <> [] && list_distinct (List.map pi1 (List.hd same_indccl)) then - if_verbose warn (strbrk "Coinductive statements do not follow the order of definition, assume the proof to be by induction."); flush_all (); + if_verbose msgnl (strbrk "Coinductive statements do not follow the order of definition, assuming the proof to be by induction."); flush_all (); let possible_guards = List.map (List.map pi3) inds_hyps in (* assume the largest indices as possible *) list_last common_same_indhyp, false, possible_guards @@ -176,14 +174,6 @@ let save id const do_guard (locality,kind) hook = definition_message id; hook l r -let save_hook = ref ignore -let set_save_hook f = save_hook := f - -let save_named opacity = - let id,(const,do_guard,persistence,hook) = Pfedit.cook_proof !save_hook in - let const = { const with const_entry_opaque = opacity } in - save id const do_guard persistence hook - let default_thm_id = id_of_string "Unnamed_thm" let compute_proof_name locality = function @@ -209,7 +199,7 @@ let save_remaining_recthms (local,kind) body opaq i (id,(t_i,(_,imps))) = (Local,VarRef id,imps) | Global -> let k = IsAssumption Conjectural in - let kn = declare_constant id (ParameterEntry (t_i,false), k) in + let kn = declare_constant id (ParameterEntry (None,t_i,None), k) in (Global,ConstRef kn,imps)) | Some body -> let k = logical_kind_of_goal_kind kind in @@ -225,27 +215,34 @@ let save_remaining_recthms (local,kind) body opaq i (id,(t_i,(_,imps))) = | Global -> let const = { const_entry_body = body_i; + const_entry_secctx = None; const_entry_type = Some t_i; - const_entry_opaque = opaq; - const_entry_boxed = false (* copy of what cook_proof does *)} in + const_entry_opaque = opaq } in let kn = declare_constant id (DefinitionEntry const, k) in (Global,ConstRef kn,imps) -(* 4.2| General support for goals *) +let save_hook = ref ignore +let set_save_hook f = save_hook := f + +let get_proof opacity = + let id,(const,do_guard,persistence,hook) = Pfedit.cook_proof !save_hook in + id,{const with const_entry_opaque = opacity},do_guard,persistence,hook + +let save_named opacity = + let id,const,do_guard,persistence,hook = get_proof opacity in + save id const do_guard persistence hook let check_anonymity id save_ident = - if atompart_of_id id <> "Unnamed_thm" then + if atompart_of_id id <> string_of_id (default_thm_id) then error "This command can only be used for unnamed theorem." let save_anonymous opacity save_ident = - let id,(const,do_guard,persistence,hook) = Pfedit.cook_proof !save_hook in - let const = { const with const_entry_opaque = opacity } in + let id,const,do_guard,persistence,hook = get_proof opacity in check_anonymity id save_ident; save save_ident const do_guard persistence hook let save_anonymous_with_strength kind opacity save_ident = - let id,(const,do_guard,_,hook) = Pfedit.cook_proof !save_hook in - let const = { const with const_entry_opaque = opacity } in + let id,const,do_guard,_,hook = get_proof opacity in check_anonymity id save_ident; (* we consider that non opaque behaves as local for discharge *) save save_ident const do_guard (Global, Proof kind) hook @@ -256,8 +253,7 @@ let start_hook = ref ignore let set_start_hook = (:=) start_hook let start_proof id kind c ?init_tac ?(compute_guard=[]) hook = - let sign = Global.named_context () in - let sign = clear_proofs sign in + let sign = initialize_named_context_for_proof () in !start_hook c; Pfedit.start_proof id kind sign c ?init_tac ~compute_guard hook @@ -314,11 +310,11 @@ let start_proof_with_initialization kind recguard thms snl hook = start_proof id kind t ?init_tac hook ~compute_guard:guard let start_proof_com kind thms hook = - let evdref = ref (create_evar_defs Evd.empty) in + let evdref = ref Evd.empty in let env0 = Global.env () in let thms = List.map (fun (sopt,(bl,t,guard)) -> - let (env, ctx), imps = interp_context_evars evdref env0 bl in - let t', imps' = interp_type_evars_impls ~evdref env t in + let impls, ((env, ctx), imps) = interp_context_evars evdref env0 bl in + let t', imps' = interp_type_evars_impls ~impls ~evdref env t in Sign.iter_rel_context (check_evars env Evd.empty !evdref) ctx; let ids = List.map pi1 ctx in (compute_proof_name (fst kind) sopt, @@ -333,8 +329,9 @@ let start_proof_com kind thms hook = let admit () = let (id,k,typ,hook) = Pfedit.current_proof_statement () in + let e = Pfedit.get_used_variables(), typ, None in let kn = - declare_constant id (ParameterEntry (typ,false),IsAssumption Conjectural) in + declare_constant id (ParameterEntry e,IsAssumption Conjectural) in Pfedit.delete_current_proof (); assumption_message id; hook Global (ConstRef kn) diff --git a/toplevel/lemmas.mli b/toplevel/lemmas.mli index 0e8eaac2..8b496f82 100644 --- a/toplevel/lemmas.mli +++ b/toplevel/lemmas.mli @@ -1,14 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: lemmas.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(*i*) open Names open Term open Decl_kinds @@ -17,9 +14,8 @@ open Tacexpr open Vernacexpr open Proof_type open Pfedit -(*i*) -(* A hook start_proof calls on the type of the definition being started *) +(** A hook start_proof calls on the type of the definition being started *) val set_start_hook : (types -> unit) -> unit val start_proof : identifier -> goal_kind -> types -> @@ -35,31 +31,32 @@ val start_proof_with_initialization : (identifier * (types * (name list * Impargs.manual_explicitation list))) list -> int list option -> declaration_hook -> unit -(* A hook the next three functions pass to cook_proof *) -val set_save_hook : (Refiner.pftreestate -> unit) -> unit +(** A hook the next three functions pass to cook_proof *) +val set_save_hook : (Proof.proof -> unit) -> unit -(*s [save_named b] saves the current completed proof under the name it +(** {6 ... } *) +(** [save_named b] saves the current completed proof under the name it was started; boolean [b] tells if the theorem is declared opaque; it fails if the proof is not completed *) val save_named : bool -> unit -(* [save_anonymous b name] behaves as [save_named] but declares the theorem +(** [save_anonymous b name] behaves as [save_named] but declares the theorem under the name [name] and respects the strength of the declaration *) val save_anonymous : bool -> identifier -> unit -(* [save_anonymous_with_strength s b name] behaves as [save_anonymous] but +(** [save_anonymous_with_strength s b name] behaves as [save_anonymous] but declares the theorem under the name [name] and gives it the strength [strength] *) val save_anonymous_with_strength : theorem_kind -> bool -> identifier -> unit -(* [admit ()] aborts the current goal and save it as an assmumption *) +(** [admit ()] aborts the current goal and save it as an assmumption *) val admit : unit -> unit -(* [get_current_context ()] returns the evar context and env of the +(** [get_current_context ()] returns the evar context and env of the current open proof if any, otherwise returns the empty evar context and the current global env *) diff --git a/toplevel/libtypes.ml b/toplevel/libtypes.ml index 27e19bd8..2f98962c 100644 --- a/toplevel/libtypes.ml +++ b/toplevel/libtypes.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -71,7 +71,7 @@ let subst a b = Profile.profile2 subst_key TypeDnet.subst a b let load_key = Profile.declare_profile "load" let load a = Profile.profile1 load_key load a *) -let (input,output) = +let input : TypeDnet.t -> obj = declare_object { (default_object "LIBTYPES") with load_function = (fun _ -> load); diff --git a/toplevel/libtypes.mli b/toplevel/libtypes.mli index 03329592..a6a95ccf 100644 --- a/toplevel/libtypes.mli +++ b/toplevel/libtypes.mli @@ -1,31 +1,25 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id:$ *) - -(*i*) open Term -(*i*) -(* - * Persistent library of all declared object, - * indexed by their types (uses Dnets) - *) +(** Persistent library of all declared object, indexed by their types + (uses Dnets) *) -(* results are the reference of the object, together with a context +(** results are the reference of the object, together with a context (constr+evar) and a substitution under this context *) type result = Libnames.global_reference * (constr*existential_key) * Termops.subst -(* this is the reduction function used in the indexing process *) +(** this is the reduction function used in the indexing process *) val reduce : types -> types -(* The different types of search available. - * See term_dnet.mli for more explanations *) +(** The different types of search available. + See term_dnet.mli for more explanations *) val search_pattern : types -> result list val search_concl : types -> result list val search_head_concl : types -> result list diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 0adae08a..6a4d7251 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -1,15 +1,14 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: metasyntax.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - open Pp open Flags +open Compat open Util open Names open Topconstr @@ -20,8 +19,9 @@ open Summary open Constrintern open Vernacexpr open Pcoq -open Rawterm +open Glob_term open Libnames +open Tok open Lexer open Egrammar open Notation @@ -30,9 +30,9 @@ open Nameops (**********************************************************************) (* Tokens *) -let cache_token (_,s) = add_token ("", s) +let cache_token (_,s) = add_keyword s -let (inToken, outToken) = +let inToken : string -> obj = declare_object {(default_object "TOKEN") with open_function = (fun i o -> if i=1 then cache_token o); cache_function = cache_token; @@ -70,7 +70,12 @@ let subst_tactic_parule subst (key,n,p,(d,tac)) = let subst_tactic_notation (subst,(pa,pp)) = (subst_tactic_parule subst pa,pp) -let (inTacticGrammar, outTacticGrammar) = +type tactic_grammar_obj = + (string * int * grammar_prod_item list * + (dir_path * Tacexpr.glob_tactic_expr)) + * (string * Genarg.argument_type list * (int * Pptactic.grammar_terminals)) + +let inTacticGrammar : tactic_grammar_obj -> obj = declare_object {(default_object "TacticGrammar") with open_function = (fun i o -> if i=1 then cache_tactic_notation o); cache_function = cache_tactic_notation; @@ -106,33 +111,33 @@ let add_tactic_notation (n,prods,e) = let print_grammar = function | "constr" | "operconstr" | "binder_constr" -> msgnl (str "Entry constr is"); - entry_print Pcoq.Constr.constr; + Gram.entry_print Pcoq.Constr.constr; msgnl (str "and lconstr is"); - entry_print Pcoq.Constr.lconstr; + Gram.entry_print Pcoq.Constr.lconstr; msgnl (str "where binder_constr is"); - entry_print Pcoq.Constr.binder_constr; + Gram.entry_print Pcoq.Constr.binder_constr; msgnl (str "and operconstr is"); - entry_print Pcoq.Constr.operconstr; + Gram.entry_print Pcoq.Constr.operconstr; | "pattern" -> - entry_print Pcoq.Constr.pattern + Gram.entry_print Pcoq.Constr.pattern | "tactic" -> msgnl (str "Entry tactic_expr is"); - entry_print Pcoq.Tactic.tactic_expr; + Gram.entry_print Pcoq.Tactic.tactic_expr; msgnl (str "Entry binder_tactic is"); - entry_print Pcoq.Tactic.binder_tactic; + Gram.entry_print Pcoq.Tactic.binder_tactic; msgnl (str "Entry simple_tactic is"); - entry_print Pcoq.Tactic.simple_tactic; + Gram.entry_print Pcoq.Tactic.simple_tactic; | "vernac" -> msgnl (str "Entry vernac is"); - entry_print Pcoq.Vernac_.vernac; + Gram.entry_print Pcoq.Vernac_.vernac; msgnl (str "Entry command is"); - entry_print Pcoq.Vernac_.command; + Gram.entry_print Pcoq.Vernac_.command; msgnl (str "Entry syntax is"); - entry_print Pcoq.Vernac_.syntax; + Gram.entry_print Pcoq.Vernac_.syntax; msgnl (str "Entry gallina is"); - entry_print Pcoq.Vernac_.gallina; + Gram.entry_print Pcoq.Vernac_.gallina; msgnl (str "Entry gallina_ext is"); - entry_print Pcoq.Vernac_.gallina_ext; + Gram.entry_print Pcoq.Vernac_.gallina_ext; | _ -> error "Unknown or unprintable grammar entry." (**********************************************************************) @@ -233,7 +238,7 @@ let parse_format (loc,str) = else error "Empty format." with e -> - Stdpp.raise_with_loc loc e + Loc.raise loc e (***********************) (* Analyzing notations *) @@ -279,9 +284,9 @@ let rec find_pattern nt xl = function find_pattern nt (x::xl) (l,l') | [], NonTerminal x' :: l' -> (out_nt nt,x',List.rev xl),l' - | [], Terminal s :: _ | Terminal s :: _, _ -> + | _, Terminal s :: _ | Terminal s :: _, _ -> error ("The token \""^s^"\" occurs on one side of \"..\" but not on the other side.") - | [], Break s :: _ | Break s :: _, _ -> + | _, Break s :: _ | Break s :: _, _ -> error ("A break occurs on one side of \"..\" but not on the other side.") | _, [] -> error ("The special symbol \"..\" must occur in a configuration of the form\n\"x symbs .. symbs y\".") @@ -311,13 +316,10 @@ let rec interp_list_parser hd = function (* Find non-terminal tokens of notation *) -let is_normal_token str = - try let _ = Lexer.check_ident str in true with Lexer.Error _ -> false - (* To protect alphabetic tokens and quotes from being seen as variables *) let quote_notation_token x = let n = String.length x in - let norm = is_normal_token x in + let norm = is_ident x in if (n > 0 & norm) or (n > 2 & x.[0] = '\'') then "'"^x^"'" else x @@ -325,11 +327,9 @@ let rec raw_analyze_notation_tokens = function | [] -> [] | String ".." :: sl -> NonTerminal ldots_var :: raw_analyze_notation_tokens sl | String "_" :: _ -> error "_ must be quoted." - | String x :: sl when is_normal_token x -> - Lexer.check_ident x; + | String x :: sl when is_ident x -> NonTerminal (Names.id_of_string x) :: raw_analyze_notation_tokens sl | String s :: sl -> - Lexer.check_keyword s; Terminal (drop_simple_quotes s) :: raw_analyze_notation_tokens sl | WhiteSpace n :: sl -> Break n :: raw_analyze_notation_tokens sl @@ -363,11 +363,6 @@ let error_not_same_scope x y = error ("Variables "^string_of_id x^" and "^string_of_id y^ " must be in the same scope.") -let error_both_bound_and_binding x y = - errorlabstrm "" (strbrk "The recursive variables " ++ pr_id x ++ - strbrk " and " ++ pr_id y ++ strbrk " cannot be used as placeholder - for both terms and binders.") - (**********************************************************************) (* Build pretty-printing rules *) @@ -375,9 +370,9 @@ type printing_precedence = int * parenRelation type parsing_precedence = int option let prec_assoc = function - | Gramext.RightA -> (L,E) - | Gramext.LeftA -> (E,L) - | Gramext.NonA -> (L,L) + | RightA -> (L,E) + | LeftA -> (E,L) + | NonA -> (L,L) let precedence_of_entry_type from = function | ETConstr (NumLevel n,BorderProd (_,None)) -> n, Prec n @@ -403,12 +398,6 @@ let is_right_bracket s = let l = String.length s in l <> 0 & (s.[l-1] = '}' or s.[l-1] = ']' or s.[l-1] = ')') -let is_left_bracket_on_left s = - let l = String.length s in l <> 0 & s.[l-1] = '>' - -let is_right_bracket_on_right s = - let l = String.length s in l <> 0 & s.[0] = '<' - let is_comma s = let l = String.length s in l <> 0 & (s.[0] = ',' or s.[0] = ';') @@ -598,20 +587,20 @@ let is_not_small_constr = function | _ -> false let rec define_keywords_aux = function - | GramConstrNonTerminal(e,Some _) as n1 :: GramConstrTerminal("IDENT",k) :: l + | GramConstrNonTerminal(e,Some _) as n1 :: GramConstrTerminal(IDENT k) :: l when is_not_small_constr e -> - message ("Defining '"^k^"' as keyword"); - Lexer.add_token("",k); - n1 :: GramConstrTerminal("",k) :: define_keywords_aux l + message ("Identifier '"^k^"' now a keyword"); + Lexer.add_keyword k; + n1 :: GramConstrTerminal(KEYWORD k) :: define_keywords_aux l | n :: l -> n :: define_keywords_aux l | [] -> [] (* Ensure that IDENT articulation terminal symbols are keywords *) let define_keywords = function - | GramConstrTerminal("IDENT",k)::l -> - message ("Defining '"^k^"' as keyword"); - Lexer.add_token("",k); - GramConstrTerminal("",k) :: define_keywords_aux l + | GramConstrTerminal(IDENT k)::l -> + message ("Identifier '"^k^"' now a keyword"); + Lexer.add_keyword k; + GramConstrTerminal(KEYWORD k) :: define_keywords_aux l | l -> define_keywords_aux l let distribute a ll = List.map (fun l -> a @ l) ll @@ -673,9 +662,9 @@ let border = function let recompute_assoc typs = match border typs, border (List.rev typs) with - | Some Gramext.LeftA, Some Gramext.RightA -> assert false - | Some Gramext.LeftA, _ -> Some Gramext.LeftA - | _, Some Gramext.RightA -> Some Gramext.RightA + | Some LeftA, Some RightA -> assert false + | Some LeftA, _ -> Some LeftA + | _, Some RightA -> Some RightA | _ -> None (**************************************************************************) @@ -726,7 +715,13 @@ let subst_syntax_extension (subst,(local,sy)) = let classify_syntax_definition (local,_ as o) = if local then Dispose else Substitute o -let (inSyntaxExtension, outSyntaxExtension) = +type syntax_extension_obj = + bool * + (notation_var_internalization_type list * Notation.level * + notation * notation_grammar * unparsing list) + list + +let inSyntaxExtension : syntax_extension_obj -> obj = declare_object {(default_object "SYNTAX-EXTENSION") with open_function = (fun i o -> if i=1 then cache_syntax_extension o); cache_function = cache_syntax_extension; @@ -891,15 +886,17 @@ specially and require that the notation \"{ _ }\" is already reserved." (* Remove patterns of the form "{ _ }", unless it is the "{ _ }" notation *) let remove_curly_brackets l = - let rec next = function - | Break _ :: l -> next l - | l -> l in + let rec skip_break acc = function + | Break _ as br :: l -> skip_break (br::acc) l + | l -> List.rev acc, l in let rec aux deb = function | [] -> [] | Terminal "{" as t1 :: l -> - (match next l with + let br,next = skip_break [] l in + (match next with | NonTerminal _ as x :: l' as l0 -> - (match next l' with + let br',next' = skip_break [] l' in + (match next' with | Terminal "}" as t2 :: l'' as l1 -> if l <> l0 or l' <> l1 then warning "Skipping spaces inside curly brackets"; @@ -907,15 +904,14 @@ let remove_curly_brackets l = check_curly_brackets_notation_exists (); x :: aux false l'' end - | l1 -> t1 :: x :: aux false l1) + | l1 -> t1 :: br @ x :: br' @ aux false l1) | l0 -> t1 :: aux false l0) | x :: l -> x :: aux false l in aux true l let compute_syntax_data (df,modifiers) = let (assoc,n,etyps,onlyparse,fmt) = interp_modifiers modifiers in - (* Notation defaults to NONA *) - let assoc = match assoc with None -> Some Gramext.NonA | a -> a in + let assoc = match assoc with None -> (* default *) Some NonA | a -> a in let toks = split_notation_string df in let (recvars,mainvars,symbols) = analyze_notation_tokens toks in let ntn_for_interp = make_notation_key symbols in @@ -977,7 +973,11 @@ let subst_notation (subst,(lc,scope,pat,b,ndf)) = let classify_notation (local,_,_,_,_ as o) = if local then Dispose else Substitute o -let (inNotation, outNotation) = +type notation_obj = + bool * scope_name option * interpretation * bool * + (notation * notation_location) + +let inNotation : notation_obj -> obj = declare_object {(default_object "NOTATION") with open_function = open_notation; cache_function = cache_notation; @@ -1153,7 +1153,7 @@ let subst_scope_command (subst,(scope,o as x)) = match o with scope, ScopeClasses cl' | _ -> x -let (inScopeCommand,outScopeCommand) = +let inScopeCommand : scope_name * scope_command -> obj = declare_object {(default_object "DELIMITERS") with cache_function = cache_scope_command; open_function = open_scope_command; diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli index 2c4e29bb..4ee1310a 100644 --- a/toplevel/metasyntax.mli +++ b/toplevel/metasyntax.mli @@ -1,14 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: metasyntax.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(*i*) open Util open Names open Libnames @@ -18,16 +15,15 @@ open Tacexpr open Vernacexpr open Notation open Topconstr -(*i*) val add_token_obj : string -> unit -(* Adding a tactic notation in the environment *) +(** Adding a tactic notation in the environment *) val add_tactic_notation : int * grammar_tactic_prod_item_expr list * raw_tactic_expr -> unit -(* Adding a (constr) notation in the environment*) +(** Adding a (constr) notation in the environment*) val add_infix : locality_flag -> (lstring * syntax_modifier list) -> constr_expr -> scope_name option -> unit @@ -35,32 +31,32 @@ val add_infix : locality_flag -> (lstring * syntax_modifier list) -> val add_notation : locality_flag -> constr_expr -> (lstring * syntax_modifier list) -> scope_name option -> unit -(* Declaring delimiter keys and default scopes *) +(** Declaring delimiter keys and default scopes *) val add_delimiters : scope_name -> string -> unit val add_class_scope : scope_name -> Classops.cl_typ -> unit -(* Add only the interpretation of a notation that already has pa/pp rules *) +(** Add only the interpretation of a notation that already has pa/pp rules *) val add_notation_interpretation : (lstring * constr_expr * scope_name option) -> unit -(* Add a notation interpretation for supporting the "where" clause *) +(** Add a notation interpretation for supporting the "where" clause *) val set_notation_for_interpretation : Constrintern.internalization_env -> (lstring * constr_expr * scope_name option) -> unit -(* Add only the parsing/printing rule of a notation *) +(** Add only the parsing/printing rule of a notation *) val add_syntax_extension : locality_flag -> (lstring * syntax_modifier list) -> unit -(* Add a syntactic definition (as in "Notation f := ...") *) +(** Add a syntactic definition (as in "Notation f := ...") *) val add_syntactic_definition : identifier -> identifier list * constr_expr -> bool -> bool -> unit -(* Print the Camlp4 state of a grammar *) +(** Print the Camlp4 state of a grammar *) val print_grammar : string -> unit diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index 59bc01d0..ff3ce8a0 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -1,18 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4use: "pa_macro.cmo" i*) -(* WARNING - * camlp4deps will not work for this file unless Makefile system enhanced. - *) - -(* $Id: mltop.ml4 14641 2011-11-06 11:59:10Z herbelin $ *) - open Util open Pp open Flags @@ -133,8 +126,8 @@ let add_ml_dir s = | _ -> () (* For Rec Add ML Path *) -let add_rec_ml_dir dir = - List.iter (fun (lp,_) -> add_ml_dir lp) (all_subdirs dir) +let add_rec_ml_dir unix_path = + List.iter (fun (lp,_) -> add_ml_dir lp) (all_subdirs ~unix_path) (* Adding files to Coq and ML loadpath *) @@ -150,24 +143,24 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath = let convert_string d = try Names.id_of_string d with _ -> - if_verbose warning - ("Directory "^d^" cannot be used as a Coq identifier (skipped)"); + if_warn msg_warning + (str ("Directory "^d^" cannot be used as a Coq identifier (skipped)")); flush_all (); failwith "caught" -let add_rec_path ~unix_path:dir ~coq_root:coq_dirpath = - if exists_dir dir then - let dirs = all_subdirs dir in - let prefix = Names.repr_dirpath coq_dirpath in +let add_rec_path ~unix_path ~coq_root = + if exists_dir unix_path then + let dirs = all_subdirs ~unix_path in + let prefix = Names.repr_dirpath coq_root in let convert_dirs (lp,cp) = (lp,Names.make_dirpath (List.map convert_string (List.rev cp)@prefix)) in let dirs = map_succeed convert_dirs dirs in List.iter (fun lpe -> add_ml_dir (fst lpe)) dirs; - add_ml_dir dir; + add_ml_dir unix_path; List.iter (Library.add_load_path false) dirs; - Library.add_load_path true (dir,coq_dirpath) + Library.add_load_path true (unix_path, coq_root) else - msg_warning (str ("Cannot open " ^ dir)) + msg_warning (str ("Cannot open " ^ unix_path)) (* convertit un nom quelconque en nom de fichier ou de module *) let mod_of_name name = @@ -224,8 +217,6 @@ let file_of_name name = coqtop could always load plugins, we prefer to have uniformity between bytecode and native versions. *) -let stdlib_use_plugins = Coq_config.has_natdynlink - (* [known_loaded_module] contains the names of the loaded ML modules * (linked or loaded with load_object). It is used not to load a * module twice. It is NOT the list of ML modules Coq knows. *) @@ -244,7 +235,7 @@ let add_known_module mname = let module_is_known mname = Stringset.mem (String.capitalize mname) !known_loaded_modules -let load_object mname fname= +let load_ml_object mname fname= dir_ml_load fname; add_known_module mname @@ -266,7 +257,7 @@ let unfreeze_ml_modules x = if not (module_is_known mname) then if has_dynlink then let fname = file_of_name mname in - load_object mname fname + load_ml_object mname fname else errorlabstrm "Mltop.unfreeze_ml_modules" (str"Loading of ML object file forbidden in a native Coq."); @@ -291,7 +282,7 @@ let cache_ml_module_object (_,{mnames=mnames}) = try if_verbose msg (str"[Loading ML file " ++ str fname ++ str" ..."); - load_object mname fname; + load_ml_object mname fname; if_verbose msgnl (str" done]"); add_loaded_module mname with e -> @@ -305,7 +296,7 @@ let cache_ml_module_object (_,{mnames=mnames}) = let classify_ml_module_object ({mlocal=mlocal} as o) = if mlocal then Dispose else Substitute o -let (inMLModule,outMLModule) = +let inMLModule : ml_module_object -> obj = declare_object {(default_object "ML-MODULE") with load_function = (fun _ -> cache_ml_module_object); cache_function = cache_ml_module_object; diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli index ae562bd2..1e9c3b03 100644 --- a/toplevel/mltop.mli +++ b/toplevel/mltop.mli @@ -1,14 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: mltop.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(* If there is a toplevel under Coq, it is described by the following +(** If there is a toplevel under Coq, it is described by the following record. *) type toplevel = { load_obj : string -> unit; @@ -16,44 +14,44 @@ type toplevel = { add_dir : string -> unit; ml_loop : unit -> unit } -(* Sets and initializes a toplevel (if any) *) +(** Sets and initializes a toplevel (if any) *) val set_top : toplevel -> unit -(* Are we in a native version of Coq? *) +(** Are we in a native version of Coq? *) val is_native : bool -(* Removes the toplevel (if any) *) +(** Removes the toplevel (if any) *) val remove : unit -> unit -(* Tests if an Ocaml toplevel runs under Coq *) +(** Tests if an Ocaml toplevel runs under Coq *) val is_ocaml_top : unit -> bool -(* Tests if we can load ML files *) +(** Tests if we can load ML files *) val has_dynlink : bool -(* Starts the Ocaml toplevel loop *) +(** Starts the Ocaml toplevel loop *) val ocaml_toploop : unit -> unit -(* Dynamic loading of .cmo *) +(** Dynamic loading of .cmo *) val dir_ml_load : string -> unit -(* Dynamic interpretation of .ml *) +(** Dynamic interpretation of .ml *) val dir_ml_use : string -> unit -(* Adds a path to the ML paths *) +(** Adds a path to the ML paths *) val add_ml_dir : string -> unit val add_rec_ml_dir : string -> unit -(* Adds a path to the Coq and ML paths *) +(** Adds a path to the Coq and ML paths *) val add_path : unix_path:string -> coq_root:Names.dir_path -> unit val add_rec_path : unix_path:string -> coq_root:Names.dir_path -> unit -(* List of modules linked to the toplevel *) +(** List of modules linked to the toplevel *) val add_known_module : string -> unit val module_is_known : string -> bool -val load_object : string -> string -> unit +val load_ml_object : string -> string -> unit -(* Summary of Declared ML Modules *) +(** Summary of Declared ML Modules *) val get_loaded_modules : unit -> string list val add_loaded_module : string -> unit val init_ml_modules : unit -> unit @@ -63,8 +61,6 @@ type ml_module_object = { mlocal: Vernacexpr.locality_flag; mnames: string list; } -val inMLModule : ml_module_object -> Libobject.obj -val outMLModule : Libobject.obj -> ml_module_object val declare_ml_modules : Vernacexpr.locality_flag -> string list -> unit diff --git a/toplevel/record.ml b/toplevel/record.ml index ee9b8d66..86849cbb 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -1,20 +1,17 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: record.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - open Pp open Util open Names open Libnames open Nameops open Term -open Termops open Environ open Declarations open Entries @@ -33,10 +30,10 @@ open Topconstr let interp_evars evdref env impls k typ = let typ' = intern_gen true ~impls !evdref env typ in - let imps = Implicit_quantifiers.implicits_of_rawterm typ' in + let imps = Implicit_quantifiers.implicits_of_glob_constr typ' in imps, Pretyping.Default.understand_tcc_evars evdref env k typ' -let interp_fields_evars evars env nots l = +let interp_fields_evars evars env impls_env nots l = List.fold_left2 (fun (env, uimpls, params, impls) no ((loc, i), b, t) -> let impl, t' = interp_evars evars env impls Pretyping.IsType t in @@ -44,12 +41,12 @@ let interp_fields_evars evars env nots l = let impls = match i with | Anonymous -> impls - | Name id -> (id, compute_internalization_data env Constrintern.Method t' impl) :: impls + | Name id -> Idmap.add id (compute_internalization_data env Constrintern.Method t' impl) impls in let d = (i,b',t') in List.iter (Metasyntax.set_notation_for_interpretation impls) no; (push_rel d env, impl :: uimpls, d::params, impls)) - (env, [], [], []) nots l + (env, [], [], impls_env) nots l let binder_of_decl = function | Vernacexpr.AssumExpr(n,t) -> (n,None,t) @@ -60,11 +57,23 @@ let binders_of_decls = List.map binder_of_decl let typecheck_params_and_fields id t ps nots fs = let env0 = Global.env () in let evars = ref Evd.empty in - let (env1,newps), imps = interp_context_evars evars env0 ps in - let fullarity = it_mkProd_or_LetIn (Option.cata (fun x -> x) (new_Type ()) t) newps in + let _ = + let error bk (loc, name) = + match bk with + | Default _ -> + if name = Anonymous then + user_err_loc (loc, "record", str "Record parameters must be named") + | _ -> () + in + List.iter + (function LocalRawDef (b, _) -> error default_binder_kind b + | LocalRawAssum (ls, bk, ce) -> List.iter (error bk) ls) ps + in + let impls_env, ((env1,newps), imps) = interp_context_evars evars env0 ps in + let fullarity = it_mkProd_or_LetIn (Option.cata (fun x -> x) (Termops.new_Type ()) t) newps in let env_ar = push_rel_context newps (push_rel (Name id,None,fullarity) env0) in let env2,impls,newfs,data = - interp_fields_evars evars env_ar nots (binders_of_decls fs) + interp_fields_evars evars env_ar impls_env nots (binders_of_decls fs) in let evars = Evarconv.consider_remaining_unif_problems env_ar !evars in let evars = Typeclasses.resolve_typeclasses env_ar evars in @@ -153,7 +162,7 @@ let subst_projection fid l c = let instantiate_possibly_recursive_type indsp paramdecls fields = let subst = list_map_i (fun i _ -> mkRel i) 1 paramdecls in - substl_rel_context (subst@[mkInd indsp]) fields + Termops.substl_rel_context (subst@[mkInd indsp]) fields (* We build projections *) let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls fields = @@ -161,11 +170,11 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls let (mib,mip) = Global.lookup_inductive indsp in let paramdecls = mib.mind_params_ctxt in let r = mkInd indsp in - let rp = applist (r, extended_rel_list 0 paramdecls) in - let paramargs = extended_rel_list 1 paramdecls in (*def in [[params;x:rp]]*) + let rp = applist (r, Termops.extended_rel_list 0 paramdecls) in + let paramargs = Termops.extended_rel_list 1 paramdecls in (*def in [[params;x:rp]]*) let x = match name with Some n -> Name n | None -> Namegen.named_hd (Global.env()) r Anonymous in let fields = instantiate_possibly_recursive_type indsp paramdecls fields in - let lifted_fields = lift_rel_context 1 fields in + let lifted_fields = Termops.lift_rel_context 1 fields in let (_,kinds,sp_projs,_) = list_fold_left3 (fun (nfi,kinds,sp_projs,subst) coe (fi,optci,ti) impls -> @@ -194,11 +203,11 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls try let cie = { const_entry_body = proj; + const_entry_secctx = None; const_entry_type = Some projtyp; - const_entry_opaque = false; - const_entry_boxed = Flags.boxed_definitions() } in + const_entry_opaque = false } in let k = (DefinitionEntry cie,IsDefinition kind) in - let kn = declare_internal_constant fid k in + let kn = declare_constant ~internal:KernelSilent fid k in Flags.if_verbose message (string_of_id fid ^" is defined"); kn with Type_errors.TypeError (ctx,te) -> @@ -208,7 +217,7 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls Impargs.maybe_declare_manual_implicits false refi impls; if coe then begin let cl = Class.class_of_global (IndRef indsp) in - Class.try_add_new_coercion_with_source refi Global cl + Class.try_add_new_coercion_with_source refi Global ~source:cl end; let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in let constr_fip = applist (constr_fi,proj_args) in @@ -239,7 +248,7 @@ open Typeclasses let declare_structure finite infer id idbuild paramimpls params arity fieldimpls fields ?(kind=StructureComponent) ?name is_coe coers sign = let nparams = List.length params and nfields = List.length fields in - let args = extended_rel_list nfields params in + let args = Termops.extended_rel_list nfields params in let ind = applist (mkRel (1+nparams+nfields), args) in let type_constructor = it_mkProd_or_LetIn ind fields in let mie_ind = @@ -253,7 +262,7 @@ let declare_structure finite infer id idbuild paramimpls params arity fieldimpls (* there is probably a way to push this to "declare_mutual" *) begin match finite with | BiFinite -> - if dependent (mkRel (nparams+1)) (it_mkProd_or_LetIn mkProp fields) then + if Termops.dependent (mkRel (nparams+1)) (it_mkProd_or_LetIn mkProp fields) then error "Records declared with the keyword Record or Structure cannot be recursive. Maybe you meant to define an Inductive or CoInductive record." | _ -> () end; @@ -282,18 +291,15 @@ let implicits_of_context ctx = in ExplByPos (i, explname), (true, true, true)) 1 (List.rev (Anonymous :: (List.map pi1 ctx))) -let qualid_of_con c = - Qualid (dummy_loc, shortest_qualid_of_global Idset.empty (ConstRef c)) - -let declare_instance_cst glob con = +let declare_instance_cst glob con pri = let instance = Typeops.type_of_constant (Global.env ()) con in let _, r = decompose_prod_assum instance in match class_of_constr r with - | Some tc -> add_instance (new_instance tc None glob (ConstRef con)) + | Some (_, (tc, _)) -> add_instance (new_instance tc pri glob (ConstRef con)) | None -> errorlabstrm "" (Pp.strbrk "Constant does not build instances of a declared type class.") let declare_class finite def infer id idbuild paramimpls params arity fieldimpls fields - ?(kind=StructureComponent) ?name is_coe coers sign = + ?(kind=StructureComponent) ?name is_coe coers priorities sign = let fieldimpls = (* Make the class and all params implicits in the projections *) let ctx_impls = implicits_of_context params in @@ -307,21 +313,21 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls let class_type = Option.map (fun ar -> it_mkProd_or_LetIn ar params) arity in let class_entry = { const_entry_body = class_body; + const_entry_secctx = None; const_entry_type = class_type; - const_entry_opaque = false; - const_entry_boxed = false } + const_entry_opaque = false } in let cst = Declare.declare_constant (snd id) (DefinitionEntry class_entry, IsDefinition Definition) in - let inst_type = appvectc (mkConst cst) (rel_vect 0 (List.length params)) in + let inst_type = appvectc (mkConst cst) (Termops.rel_vect 0 (List.length params)) in let proj_type = it_mkProd_or_LetIn (mkProd(Name (snd id), inst_type, lift 1 field)) params in let proj_body = it_mkLambda_or_LetIn (mkLambda (Name (snd id), inst_type, mkRel 1)) params in let proj_entry = { const_entry_body = proj_body; + const_entry_secctx = None; const_entry_type = Some proj_type; - const_entry_opaque = false; - const_entry_boxed = false } + const_entry_opaque = false } in let proj_cst = Declare.declare_constant proj_name (DefinitionEntry proj_entry, IsDefinition Definition) @@ -329,22 +335,27 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls let cref = ConstRef cst in Impargs.declare_manual_implicits false cref [paramimpls]; Impargs.declare_manual_implicits false (ConstRef proj_cst) [List.hd fieldimpls]; - Classes.set_typeclass_transparency (EvalConstRef cst) false; + Classes.set_typeclass_transparency (EvalConstRef cst) false false; if infer then Evd.fold (fun ev evi _ -> Recordops.declare_method (ConstRef cst) ev sign) sign (); - cref, [proj_name, Some proj_cst] + let sub = match List.hd coers with Some b -> Some ((if b then Backward else Forward), List.hd priorities) | None -> None in + cref, [Name proj_name, sub, Some proj_cst] | _ -> - let idarg = Namegen.next_ident_away (snd id) (ids_of_context (Global.env())) in + let idarg = Namegen.next_ident_away (snd id) (Termops.ids_of_context (Global.env())) in let ind = declare_structure BiFinite infer (snd id) idbuild paramimpls - params (Option.cata (fun x -> x) (new_Type ()) arity) fieldimpls fields + params (Option.default (Termops.new_Type ()) arity) fieldimpls fields ~kind:Method ~name:idarg false (List.map (fun _ -> false) fields) sign in - IndRef ind, (List.map2 (fun (id, _, _) y -> (Nameops.out_name id, y)) - (List.rev fields) (Recordops.lookup_projections ind)) + let coers = List.map2 (fun coe pri -> + Option.map (fun b -> if b then Backward, pri else Forward, pri) coe) + coers priorities + in + IndRef ind, (list_map3 (fun (id, _, _) b y -> (id, b, y)) + (List.rev fields) coers (Recordops.lookup_projections ind)) in let ctx_context = List.map (fun (na, b, t) -> match Typeclasses.class_of_constr t with - | Some cl -> Some (cl.cl_impl, true) (*List.exists (fun (_, n) -> n = na) supnames)*) + | Some (_, (cl, _)) -> Some (cl.cl_impl, true) (*List.exists (fun (_, n) -> n = na) supnames)*) | None -> None) params, params in @@ -354,9 +365,9 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls cl_props = fields; cl_projs = projs } in - List.iter2 (fun p sub -> - if sub then match snd p with Some p -> declare_instance_cst true p | None -> ()) - k.cl_projs coers; +(* list_iter3 (fun p sub pri -> *) +(* if sub then match p with (_, _, Some p) -> declare_instance_cst true p pri | _ -> ()) *) +(* k.cl_projs coers priorities; *) add_class k; impl let interp_and_check_sort sort = @@ -369,10 +380,12 @@ let interp_and_check_sort sort = open Vernacexpr open Autoinstance -(* [fs] corresponds to fields and [ps] to parameters; [coers] is a boolean - list telling if the corresponding fields must me declared as coercion *) +(* [fs] corresponds to fields and [ps] to parameters; [coers] is a + list telling if the corresponding fields must me declared as coercions + or subinstances *) let definition_structure (kind,finite,infer,(is_coe,(loc,idstruc)),ps,cfs,idbuild,s) = let cfs,notations = List.split cfs in + let cfs,priorities = List.split cfs in let coers,fs = List.split cfs in let extract_name acc = function Vernacexpr.AssumExpr((_,Name id),_) -> id::acc @@ -380,6 +393,8 @@ let definition_structure (kind,finite,infer,(is_coe,(loc,idstruc)),ps,cfs,idbuil | _ -> acc in let allnames = idstruc::(List.fold_left extract_name [] fs) in if not (list_distinct allnames) then error "Two objects have the same name"; + if not (kind = Class false) && List.exists ((<>) None) priorities then + error "Priorities only allowed for type class substructures"; (* Now, younger decl in params and fields is on top *) let sc = interp_and_check_sort s in let implpars, params, implfs, fields = @@ -389,13 +404,14 @@ let definition_structure (kind,finite,infer,(is_coe,(loc,idstruc)),ps,cfs,idbuil match kind with | Class def -> let gr = declare_class finite def infer (loc,idstruc) idbuild - implpars params sc implfs fields is_coe coers sign in + implpars params sc implfs fields is_coe coers priorities sign in if infer then search_record declare_class_instance gr sign; gr | _ -> - let arity = Option.default (new_Type ()) sc in + let arity = Option.default (Termops.new_Type ()) sc in let implfs = List.map (fun impls -> implpars @ Impargs.lift_implicits (succ (List.length params)) impls) implfs in - let ind = declare_structure finite infer idstruc idbuild implpars params arity implfs fields is_coe coers sign in + let ind = declare_structure finite infer idstruc idbuild implpars params arity implfs + fields is_coe (List.map (fun coe -> coe <> None) coers) sign in if infer then search_record declare_record_instance (ConstructRef (ind,1)) sign; IndRef ind diff --git a/toplevel/record.mli b/toplevel/record.mli index 44b34550..45670f1f 100644 --- a/toplevel/record.mli +++ b/toplevel/record.mli @@ -1,14 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: record.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(*i*) open Names open Term open Sign @@ -16,28 +13,27 @@ open Vernacexpr open Topconstr open Impargs open Libnames -(*i*) -(* [declare_projections ref name coers params fields] declare projections of +(** [declare_projections ref name coers params fields] declare projections of record [ref] (if allowed) using the given [name] as argument, and put them as coercions accordingly to [coers]; it returns the absolute names of projections *) val declare_projections : inductive -> ?kind:Decl_kinds.definition_object_kind -> ?name:identifier -> - bool list -> manual_explicitation list list -> rel_context -> + coercion_flag list -> manual_explicitation list list -> rel_context -> (name * bool) list * constant option list val declare_structure : Decl_kinds.recursivity_kind -> - bool (*infer?*) -> identifier -> identifier -> - manual_explicitation list -> rel_context -> (* params *) constr -> (* arity *) - Impargs.manual_explicitation list list -> rel_context -> (* fields *) + bool (**infer?*) -> identifier -> identifier -> + manual_explicitation list -> rel_context -> (** params *) constr -> (** arity *) + Impargs.manual_explicitation list list -> rel_context -> (** fields *) ?kind:Decl_kinds.definition_object_kind -> ?name:identifier -> - bool -> (* coercion? *) - bool list -> (* field coercions *) + bool -> (** coercion? *) + bool list -> (** field coercions *) Evd.evar_map -> inductive val definition_structure : - inductive_kind * Decl_kinds.recursivity_kind * bool(*infer?*)* lident with_coercion * local_binder list * - (local_decl_expr with_coercion with_notation) list * + inductive_kind * Decl_kinds.recursivity_kind * bool(**infer?*)* lident with_coercion * local_binder list * + (local_decl_expr with_instance with_priority with_notation) list * identifier * constr_expr option -> global_reference diff --git a/toplevel/search.ml b/toplevel/search.ml index fd3024a4..33e8e51d 100644 --- a/toplevel/search.ml +++ b/toplevel/search.ml @@ -1,19 +1,17 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: search.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - open Pp open Util open Names open Nameops open Term -open Rawterm +open Glob_term open Declarations open Libobject open Declare @@ -24,6 +22,16 @@ open Printer open Libnames open Nametab +module SearchBlacklist = + Goptions.MakeStringTable + (struct + let key = ["Search";"Blacklist"] + let title = "Current search blacklist : " + let member_message s b = + str ("Search blacklist does "^(if b then "" else "not ")^"include "^s) + let synchronous = true + end) + (* The functions print_constructors and crible implement the behavior needed for the Coq searching commands. These functions take as first argument the procedure @@ -57,14 +65,14 @@ let gen_crible refopt (fn : global_reference -> env -> constr -> unit) = fn (VarRef id) env typ with Not_found -> (* we are in a section *) ()) | "CONSTANT" -> - let cst = Global.constant_of_delta(constant_of_kn kn) in + let cst = Global.constant_of_delta_kn kn in let typ = Typeops.type_of_constant env cst in if refopt = None || head_const typ = constr_of_global (Option.get refopt) then fn (ConstRef cst) env typ | "INDUCTIVE" -> - let mind = Global.mind_of_delta(mind_of_kn kn) in + let mind = Global.mind_of_delta_kn kn in let mib = Global.lookup_mind mind in (match refopt with | Some (IndRef ((kn',tyi) as ind)) when eq_mind mind kn' -> @@ -95,10 +103,6 @@ let rec head c = | LetIn (_,_,_,c) -> head c | _ -> c -let constr_to_full_path c = match kind_of_term c with - | Const sp -> sp - | _ -> raise No_full_path - let xor a b = (a or b) & (not (a & b)) let plain_display ref a c = @@ -170,6 +174,10 @@ let raw_search_by_head extra_filter display_function pattern = let name_of_reference ref = string_of_id (basename_of_global ref) +let full_name_of_reference ref = + let (dir,id) = repr_path (path_of_global ref) in + string_of_dirpath dir ^ "." ^ string_of_id id + (* * functions to use the new Libtypes facility *) @@ -196,20 +204,21 @@ let filter_by_module_from_list = function | [], _ -> (fun _ _ _ -> true) | l, outside -> filter_by_module l (not outside) -let filter_subproof gr _ _ = - not (string_string_contains (name_of_reference gr) "_subproof") && - not (string_string_contains (name_of_reference gr) "_admitted") +let filter_blacklist gr _ _ = + let name = full_name_of_reference gr in + let l = SearchBlacklist.elements () in + List.for_all (fun str -> not (string_string_contains ~where:name ~what:str)) l let (&&&&&) f g x y z = f x y z && g x y z let search_by_head pat inout = - text_search_by_head (filter_by_module_from_list inout &&&&& filter_subproof) pat + text_search_by_head (filter_by_module_from_list inout &&&&& filter_blacklist) pat let search_rewrite pat inout = - text_search_rewrite (filter_by_module_from_list inout &&&&& filter_subproof) pat + text_search_rewrite (filter_by_module_from_list inout &&&&& filter_blacklist) pat let search_pattern pat inout = - text_pattern_search (filter_by_module_from_list inout &&&&& filter_subproof) pat + text_pattern_search (filter_by_module_from_list inout &&&&& filter_blacklist) pat let gen_filtered_search filter_function display_function = gen_crible None @@ -223,13 +232,13 @@ type glob_search_about_item = let search_about_item (itemref,typ) = function | GlobSearchSubPattern pat -> is_matching_appsubterm ~closed:false pat typ - | GlobSearchString s -> string_string_contains (name_of_reference itemref) s + | GlobSearchString s -> string_string_contains ~where:(name_of_reference itemref) ~what:s let raw_search_about filter_modules display_function l = let filter ref' env typ = filter_modules ref' env typ && List.for_all (fun (b,i) -> b = search_about_item (ref',typ) i) l && - filter_subproof ref' () () + filter_blacklist ref' () () in gen_filtered_search filter display_function diff --git a/toplevel/search.mli b/toplevel/search.mli index 6a85a12f..d2d5c538 100644 --- a/toplevel/search.mli +++ b/toplevel/search.mli @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: search.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - open Pp open Names open Term @@ -16,7 +14,7 @@ open Pattern open Libnames open Nametab -(*s Search facilities. *) +(** {6 Search facilities. } *) type glob_search_about_item = | GlobSearchSubPattern of constr_pattern @@ -28,14 +26,14 @@ val search_pattern : constr -> dir_path list * bool -> unit val search_about : (bool * glob_search_about_item) list -> dir_path list * bool -> unit -(* The filtering function that is by standard search facilities. +(** The filtering function that is by standard search facilities. It can be passed as argument to the raw search functions. It is used in pcoq. *) val filter_by_module_from_list : dir_path list * bool -> global_reference -> env -> 'a -> bool -(* raw search functions can be used for various extensions. +(** raw search functions can be used for various extensions. They are also used for pcoq. *) val gen_filtered_search : (global_reference -> env -> constr -> bool) -> (global_reference -> env -> constr -> unit) -> unit diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index 9954ff56..699fd12f 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: toplevel.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - open Pp open Util open Flags @@ -15,6 +13,7 @@ open Cerrors open Vernac open Vernacexpr open Pcoq +open Compat (* A buffer for the character read from a channel. We store the command * entered to be able to report errors without pretty-printing. *) @@ -48,13 +47,12 @@ let resynch_buffer ibuf = | _ -> () -(* emacs special character for prompt end (fast) detection. Prefer - (Char.chr 6) since it does not interfere with utf8. For - compatibility we let (Char.chr 249) as default for a while. *) +(* emacs special prompt tag for easy detection. No special character, + to avoid interfering with utf8. Compatibility code removed. *) -let emacs_prompt_startstring() = Printer.emacs_str "" "<prompt>" +let emacs_prompt_startstring() = Printer.emacs_str "<prompt>" -let emacs_prompt_endstring() = Printer.emacs_str (String.make 1 (Char.chr 249)) "</prompt>" +let emacs_prompt_endstring() = Printer.emacs_str "</prompt>" (* Read a char in an input channel, displaying a prompt at every beginning of line. *) @@ -165,26 +163,26 @@ let print_location_in_file s inlibrary fname loc = hov 0 (errstrm ++ str"Module " ++ str ("\""^fname^"\"") ++ spc() ++ str"characters " ++ Cerrors.print_loc loc) ++ fnl () else - let (bp,ep) = unloc loc in - let ic = open_in fname in - let rec line_of_pos lin bol cnt = - if cnt < bp then - if input_char ic == '\n' - then line_of_pos (lin + 1) (cnt +1) (cnt+1) - else line_of_pos lin bol (cnt+1) - else (lin, bol) - in - try - let (line, bol) = line_of_pos 1 0 0 in - close_in ic; - hov 0 (* No line break so as to follow emacs error message format *) - (errstrm ++ str"File " ++ str ("\""^fname^"\"") ++ - str", line " ++ int line ++ str", characters " ++ - Cerrors.print_loc (make_loc (bp-bol,ep-bol))) ++ str":" ++ - fnl () - with e -> - (close_in ic; - hov 1 (errstrm ++ spc() ++ str"(invalid location):") ++ fnl ()) + let (bp,ep) = unloc loc in + let ic = open_in fname in + let rec line_of_pos lin bol cnt = + if cnt < bp then + if input_char ic == '\n' + then line_of_pos (lin + 1) (cnt +1) (cnt+1) + else line_of_pos lin bol (cnt+1) + else (lin, bol) + in + try + let (line, bol) = line_of_pos 1 0 0 in + close_in ic; + hov 0 (* No line break so as to follow emacs error message format *) + (errstrm ++ str"File " ++ str ("\""^fname^"\"") ++ + str", line " ++ int line ++ str", characters " ++ + Cerrors.print_loc (make_loc (bp-bol,ep-bol))) ++ str":" ++ + fnl () + with e -> + (close_in ic; + hov 1 (errstrm ++ spc() ++ str"(invalid location):") ++ fnl ()) let print_command_location ib dloc = match dloc with @@ -274,7 +272,7 @@ let set_prompt prompt = let rec is_pervasive_exn = function | Out_of_memory | Stack_overflow | Sys.Break -> true | Error_in_file (_,_,e) -> is_pervasive_exn e - | Stdpp.Exc_located (_,e) -> is_pervasive_exn e + | Loc.Exc_located (_,e) -> is_pervasive_exn e | DuringCommandInterp (_,e) -> is_pervasive_exn e | _ -> false @@ -290,7 +288,7 @@ let print_toplevel_error exc = in let (locstrm,exc) = match exc with - | Stdpp.Exc_located (loc, ie) -> + | Loc.Exc_located (loc, ie) -> if valid_buffer_loc top_buffer dloc loc then (print_highlight_location top_buffer loc, ie) else @@ -310,13 +308,13 @@ let print_toplevel_error exc = raise Vernacexpr.Quit | _ -> (if is_pervasive_exn exc then (mt ()) else locstrm) ++ - Cerrors.explain_exn exc + Errors.print exc (* Read the input stream until a dot is encountered *) let parse_to_dot = - let rec dot st = match Stream.next st with - | ("", ".") -> () - | ("EOI", "") -> raise End_of_input + let rec dot st = match get_tok (Stream.next st) with + | Tok.KEYWORD "." -> () + | Tok.EOI -> raise End_of_input | _ -> dot st in Gram.Entry.of_parser "Coqtoplevel.dot" dot @@ -324,8 +322,8 @@ let parse_to_dot = (* We assume that when a lexer error occurs, at least one char was eaten *) let rec discard_to_dot () = try - Gram.Entry.parse parse_to_dot top_buffer.tokens - with Stdpp.Exc_located(_,(Token.Error _|Lexer.Error _)) -> + Gram.entry_parse parse_to_dot top_buffer.tokens + with Loc.Exc_located(_,(Token.Error _|Lexer.Error.E _)) -> discard_to_dot() diff --git a/toplevel/toplevel.mli b/toplevel/toplevel.mli index 022a6541..757aab1a 100644 --- a/toplevel/toplevel.mli +++ b/toplevel/toplevel.mli @@ -1,46 +1,42 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: toplevel.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(*i*) open Pp open Pcoq -(*i*) -(* The Coq toplevel loop. *) +(** The Coq toplevel loop. *) -(* A buffer for the character read from a channel. We store the command +(** A buffer for the character read from a channel. We store the command * entered to be able to report errors without pretty-printing. *) type input_buffer = { mutable prompt : unit -> string; - mutable str : string; (* buffer of already read characters *) - mutable len : int; (* number of chars in the buffer *) - mutable bols : int list; (* offsets in str of begining of lines *) - mutable tokens : Pcoq.Gram.parsable; (* stream of tokens *) - mutable start : int } (* stream count of the first char of the buffer *) + mutable str : string; (** buffer of already read characters *) + mutable len : int; (** number of chars in the buffer *) + mutable bols : int list; (** offsets in str of begining of lines *) + mutable tokens : Pcoq.Gram.parsable; (** stream of tokens *) + mutable start : int } (** stream count of the first char of the buffer *) -(* The input buffer of stdin. *) +(** The input buffer of stdin. *) val top_buffer : input_buffer val set_prompt : (unit -> string) -> unit -(* Toplevel error explanation, dealing with locations, Drop, Ctrl-D +(** Toplevel error explanation, dealing with locations, Drop, Ctrl-D May raise only the following exceptions: [Drop] and [End_of_input], meaning we get out of the Coq loop. *) val print_toplevel_error : exn -> std_ppcmds -(* Parse and execute a vernac command. *) +(** Parse and execute a vernac command. *) val do_vernac : unit -> unit -(* Main entry point of Coq: read and execute vernac commands. *) +(** Main entry point of Coq: read and execute vernac commands. *) val loop : unit -> unit diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib index 4c229d16..8b03e938 100644 --- a/toplevel/toplevel.mllib +++ b/toplevel/toplevel.mllib @@ -18,6 +18,8 @@ Mltop Vernacentries Whelp Vernac +Ide_intf +Ide_slave Toplevel Usage Coqinit diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 0282f30a..8c9b1078 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -1,18 +1,16 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: usage.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - -let version () = +let version ret = Printf.printf "The Coq Proof Assistant, version %s (%s)\n" Coq_config.version Coq_config.date; Printf.printf "compiled on %s with OCaml %s\n" Coq_config.compile_date Coq_config.caml_version; - exit 0 + exit ret (* print the usage of coqtop (or coqc) on channel co *) @@ -20,57 +18,59 @@ let print_usage_channel co command = output_string co command; output_string co "Coq options are:\n"; output_string co -" -I dir -as coqdir map physical dir to logical coqdir - -I dir map directory dir to the empty logical path - -include dir (idem) - -R dir -as coqdir recursively map physical dir to logical coqdir - -R dir coqdir (idem) - -top coqdir set the toplevel name to be coqdir instead of Top - -notop r set the toplevel name to be the empty logical path - -exclude-dir f exclude subdirectories named f for option -R - - -inputstate f read state from file f.coq - -is f (idem) - -nois start with an empty state - -outputstate f write state in file f.coq - -compat X.Y provides compatibility support for Coq version X.Y - - -load-ml-object f load ML object file f - -load-ml-source f load ML file f - -load-vernac-source f load Coq file f.v (Load f.) - -l f (idem) - -load-vernac-source-verbose f load Coq file f.v (Load Verbose f.) - -lv f (idem) - -load-vernac-object f load Coq object file f.vo - -require f load Coq object file f.vo and import it (Require f.) - -compile f compile Coq file f.v (implies -batch) - -compile-verbose f verbosely compile Coq file f.v (implies -batch) - - -opt run the native-code version of Coq - -byte run the bytecode version of Coq - - -where print Coq's standard library location and exit - -config print Coq's configuration information and exit - -v print Coq version and exit - - -q skip loading of rcfile - -init-file f set the rcfile to f - -user u use the rcfile of user u - -batch batch mode (exits just after arguments parsing) - -boot boot mode (implies -q and -batch) - -emacs tells Coq it is executed under Emacs - -noglob do not dump globalizations - -dump-glob f dump globalizations in file f (to be used by coqdoc) - -with-geoproof (yes|no) to (de)activate special functions for Geoproof within Coqide (default is yes) - -impredicative-set set sort Set impredicative - -dont-load-proofs don't load opaque proofs in memory - -xml export XML files either to the hierarchy rooted in - the directory $COQ_XML_LIBRARY_ROOT (if set) or to - stdout (if unset) - -quality improve the legibility of the proof terms produced by - some tactics - -h, --help print this list of options -" +" -I dir -as coqdir map physical dir to logical coqdir\ +\n -I dir map directory dir to the empty logical path\ +\n -include dir (idem)\ +\n -R dir -as coqdir recursively map physical dir to logical coqdir\ +\n -R dir coqdir (idem)\ +\n -top coqdir set the toplevel name to be coqdir instead of Top\ +\n -notop set the toplevel name to be the empty logical path\ +\n -exclude-dir f exclude subdirectories named f for option -R\ +\n\ +\n -inputstate f read state from file f.coq\ +\n -is f (idem)\ +\n -nois start with an empty state\ +\n -outputstate f write state in file f.coq\ +\n -compat X.Y provides compatibility support for Coq version X.Y\ +\n\ +\n -load-ml-object f load ML object file f\ +\n -load-ml-source f load ML file f\ +\n -load-vernac-source f load Coq file f.v (Load f.)\ +\n -l f (idem)\ +\n -load-vernac-source-verbose f load Coq file f.v (Load Verbose f.)\ +\n -lv f (idem)\ +\n -load-vernac-object f load Coq object file f.vo\ +\n -require f load Coq object file f.vo and import it (Require f.)\ +\n -compile f compile Coq file f.v (implies -batch)\ +\n -compile-verbose f verbosely compile Coq file f.v (implies -batch)\ +\n\ +\n -opt run the native-code version of Coq\ +\n -byte run the bytecode version of Coq\ +\n\ +\n -where print Coq's standard library location and exit\ +\n -config print Coq's configuration information and exit\ +\n -v print Coq version and exit\ +\n\ +\n -q skip loading of rcfile\ +\n -init-file f set the rcfile to f\ +\n -batch batch mode (exits just after arguments parsing)\ +\n -boot boot mode (implies -q and -batch)\ +\n -emacs tells Coq it is executed under Emacs\ +\n -noglob do not dump globalizations\ +\n -dump-glob f dump globalizations in file f (to be used by coqdoc)\ +\n -with-geoproof (yes|no) to (de)activate special functions for Geoproof within Coqide (default is yes)\ +\n -impredicative-set set sort Set impredicative\ +\n -force-load-proofs load opaque proofs in memory initially\ + +\n -lazy-load-proofs load opaque proofs in memory by necessity (default)\ +\n -dont-load-proofs see opaque proofs as axioms instead of loading them\ +\n -xml export XML files either to the hierarchy rooted in\ +\n the directory $COQ_XML_LIBRARY_ROOT (if set) or to\ +\n stdout (if unset)\ +\n -quality improve the legibility of the proof terms produced by\ +\n some tactics\ +\n -h, --help print this list of options\ +\n" (* print the usage on standard error *) @@ -80,22 +80,25 @@ let print_usage_coqtop () = print_usage "Usage: coqtop <options>\n\n" let print_usage_coqc () = - print_usage "Usage: coqc <options> <Coq options> file...\n -options are: - -verbose compile verbosely - -image f specify an alternative executable for Coq - -t keep temporary files\n\n" + print_usage "Usage: coqc <options> <Coq options> file...\n\ +\noptions are:\ +\n -verbose compile verbosely\ +\n -image f specify an alternative executable for Coq\ +\n -t keep temporary files\n\n" (* Print the configuration information *) let print_config () = if Coq_config.local then Printf.printf "LOCAL=1\n" else Printf.printf "LOCAL=0\n"; - Printf.printf "COQLIB=%s/\n" Coq_config.coqlib; - Printf.printf "COQSRC=%s/\n" Coq_config.coqsrc; - Printf.printf "CAMLBIN=%s/\n" Coq_config.camlbin; - Printf.printf "CAMLLIB=%s/\n" Coq_config.camllib; + Printf.printf "COQLIB=%s/\n" (Envars.coqlib ()); + Printf.printf "DOCDIR=%s/\n" (Envars.docdir ()); + Printf.printf "OCAMLDEP=%s\n" Coq_config.ocamldep; + Printf.printf "OCAMLC=%s\n" Coq_config.ocamlc; + Printf.printf "OCAMLOPT=%s\n" Coq_config.ocamlopt; + Printf.printf "OCAMLDOC=%s\n" Coq_config.ocamldoc; + Printf.printf "CAMLBIN=%s/\n" (Envars.camlbin ()); + Printf.printf "CAMLLIB=%s/\n" (Envars.camllib ()); Printf.printf "CAMLP4=%s\n" Coq_config.camlp4; - Printf.printf "CAMLP4BIN=%s\n" Coq_config.camlp4bin; - Printf.printf "CAMLP4LIB=%s\n" Coq_config.camlp4lib - - + Printf.printf "CAMLP4BIN=%s/\n" (Envars.camlp4bin ()); + Printf.printf "CAMLP4LIB=%s\n" (Envars.camlp4lib ()); + Printf.printf "HASNATDYNLINK=%s\n" (if Coq_config.has_natdynlink then "true" else "false") diff --git a/toplevel/usage.mli b/toplevel/usage.mli index 721edccb..0b98f061 100644 --- a/toplevel/usage.mli +++ b/toplevel/usage.mli @@ -1,23 +1,21 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: usage.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) +(** {6 Prints the version number on the standard output and exits (with 0). } *) -(*s Prints the version number on the standard output and exits (with 0). *) +val version : int -> 'a -val version : unit -> 'a - -(*s Prints the usage on the error output, preceeded by a user-provided message. *) +(** {6 Prints the usage on the error output, preceeded by a user-provided message. } *) val print_usage : string -> unit -(*s Prints the usage on the error output. *) +(** {6 Prints the usage on the error output. } *) val print_usage_coqtop : unit -> unit val print_usage_coqc : unit -> unit -(*s Prints the configuration information *) +(** {6 Prints the configuration information } *) val print_config : unit -> unit diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index a7aef93f..84e20f5e 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: vernac.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - (* Parsing of vernacular. *) open Pp @@ -18,6 +16,7 @@ open System open Vernacexpr open Vernacinterp open Ppvernac +open Compat (* The functions in this module may raise (unexplainable!) exceptions. Use the module Coqtoplevel, which catches these exceptions @@ -41,14 +40,14 @@ let raise_with_file file exc = match re with | Error_in_file (_, (b,f,loc), e) when loc <> dummy_loc -> ((b, f, loc), e) - | Stdpp.Exc_located (loc, e) when loc <> dummy_loc -> + | Loc.Exc_located (loc, e) when loc <> dummy_loc -> ((false,file, loc), e) - | Stdpp.Exc_located (_, e) | e -> ((false,file,cmdloc), e) + | Loc.Exc_located (_, e) | e -> ((false,file,cmdloc), e) in raise (Error_in_file (file, inner, disable_drop inex)) let real_error = function - | Stdpp.Exc_located (_, e) -> e + | Loc.Exc_located (_, e) -> e | Error_in_file (_, _, e) -> e | e -> e @@ -62,6 +61,7 @@ let default_timeout = ref None let _ = Goptions.declare_int_option { Goptions.optsync = true; + Goptions.optdepr = false; Goptions.optname = "the default timeout"; Goptions.optkey = ["Default";"Timeout"]; Goptions.optread = (fun () -> !default_timeout); @@ -133,8 +133,8 @@ let verbose_phrase verbch loc = exception End_of_input -let parse_phrase (po, verbch) = - match Pcoq.Gram.Entry.parse Pcoq.main_entry po with +let parse_sentence (po, verbch) = + match Pcoq.Gram.entry_parse Pcoq.main_entry po with | Some (loc,_ as com) -> verbose_phrase verbch loc; com | None -> raise End_of_input @@ -211,10 +211,11 @@ let rec vernac_com interpfun (loc,com) = | HasNotFailed -> errorlabstrm "Fail" (str "The command has not failed !") | e -> - (* if [e] is an anomaly, the next function will re-raise it *) - let msg = Cerrors.explain_exn_no_anomaly e in - if_verbose msgnl (str "The command has indeed failed with message:" ++ - fnl () ++ str "=> " ++ hov 0 msg) + (* Anomalies are re-raised by the next line *) + let msg = Errors.print_no_anomaly e in + if_verbose msgnl + (str "The command has indeed failed with message:" ++ + fnl () ++ str "=> " ++ hov 0 msg) end | VernacTime v -> @@ -249,22 +250,21 @@ let rec vernac_com interpfun (loc,com) = Format.set_formatter_out_channel stdout; raise (DuringCommandInterp (loc, e)) -and vernac interpfun input = - vernac_com interpfun (parse_phrase input) - and read_vernac_file verbosely s = Flags.make_warn verbosely; let interpfun = - if verbosely then - Vernacentries.interp - else - Flags.silently Vernacentries.interp + if verbosely then Vernacentries.interp + else Flags.silently Vernacentries.interp in - let (in_chan, fname, input) = open_file_twice_if verbosely s in + let (in_chan, fname, input) = + open_file_twice_if verbosely s in try (* we go out of the following infinite loop when a End_of_input is * raised, which means that we raised the end of the file being loaded *) - while true do vernac interpfun input; pp_flush () done + while true do + vernac_com interpfun (parse_sentence input); + pp_flush () + done with e -> (* whatever the exception *) Format.set_formatter_out_channel stdout; close_input in_chan input; (* we must close the file first *) @@ -273,17 +273,20 @@ and read_vernac_file verbosely s = if do_beautify () then pr_new_syntax (make_loc (max_int,max_int)) None | _ -> raise_with_file fname e -(* raw_do_vernac : char Stream.t -> unit - * parses and executes one command of the vernacular char stream. - * Marks the end of the command in the lib_stk with a new label to - * make vernac undoing easier. Also freeze state to speed up - * backtracking. *) -let raw_do_vernac po = - vernac Vernacentries.interp (po,None); +(* eval_expr : Util.loc * Vernacexpr.vernac_expr -> unit + * execute one vernacular command. Marks the end of the command in the lib_stk + * with a new label to make vernac undoing easier. Also freeze state to speed up + * backtracking. *) +let eval_expr last = + vernac_com Vernacentries.interp last; Lib.add_frozen_state(); Lib.mark_end_of_command() +(* raw_do_vernac : Pcoq.Gram.parsable -> unit + * vernac_step . parse_sentence *) +let raw_do_vernac po = eval_expr (parse_sentence (po,None)) + (* XML output hooks *) let xml_start_library = ref (fun _ -> ()) let xml_end_library = ref (fun _ -> ()) @@ -305,15 +308,14 @@ let load_vernac verb file = (* Compile a vernac file (f is assumed without .v suffix) *) let compile verbosely f = let ldir,long_f_dot_v = Flags.verbosely Library.start_library f in - if Dumpglob.multi_dump () then - Dumpglob.open_glob_file (f ^ ".glob"); - Dumpglob.dump_string ("F" ^ Names.string_of_dirpath ldir ^ "\n"); - if !Flags.xml_export then !xml_start_library (); - let _ = load_vernac verbosely long_f_dot_v in - if Pfedit.get_all_proof_names () <> [] then - (message "Error: There are pending proofs"; exit 1); - if !Flags.xml_export then !xml_end_library (); - if Dumpglob.multi_dump () then Dumpglob.close_glob_file (); - Library.save_library_to ldir (long_f_dot_v ^ "o") + Dumpglob.start_dump_glob long_f_dot_v; + Dumpglob.dump_string ("F" ^ Names.string_of_dirpath ldir ^ "\n"); + if !Flags.xml_export then !xml_start_library (); + let _ = load_vernac verbosely long_f_dot_v in + if Pfedit.get_all_proof_names () <> [] then + (message "Error: There are pending proofs"; exit 1); + if !Flags.xml_export then !xml_end_library (); + Dumpglob.end_dump_glob (); + Library.save_library_to ldir (long_f_dot_v ^ "o") diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli index 54ce9244..d89e90d0 100644 --- a/toplevel/vernac.mli +++ b/toplevel/vernac.mli @@ -1,46 +1,39 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: vernac.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) +(** Parsing of vernacular. *) -(* Parsing of vernacular. *) - -(* Read a vernac command on the specified input (parse only). +(** Read a vernac command on the specified input (parse only). Raises [End_of_file] if EOF (or Ctrl-D) is reached. *) -val parse_phrase : Pcoq.Gram.parsable * in_channel option -> - Util.loc * Vernacexpr.vernac_expr +val parse_sentence : Pcoq.Gram.parsable * in_channel option -> + Util.loc * Vernacexpr.vernac_expr -(* Reads and executes vernac commands from a stream. +(** Reads and executes vernac commands from a stream. The boolean [just_parsing] disables interpretation of commands. *) exception DuringCommandInterp of Util.loc * exn exception End_of_input val just_parsing : bool ref +val eval_expr : Util.loc * Vernacexpr.vernac_expr -> unit val raw_do_vernac : Pcoq.Gram.parsable -> unit -(* Set XML hooks *) +(** Set XML hooks *) val set_xml_start_library : (unit -> unit) -> unit val set_xml_end_library : (unit -> unit) -> unit -(* Load a vernac file, verbosely or not. Errors are annotated with file +(** Load a vernac file, verbosely or not. Errors are annotated with file and location *) val load_vernac : bool -> string -> unit -(* Compile a vernac file, verbosely or not (f is assumed without .v suffix) *) +(** Compile a vernac file, verbosely or not (f is assumed without .v suffix) *) val compile : bool -> string -> unit - -(* Interpret a vernac AST *) - -val vernac_com : - (Vernacexpr.vernac_expr -> unit) -> - Util.loc * Vernacexpr.vernac_expr -> unit diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 3be3c6db..5787feb0 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: vernacentries.ml 14641 2011-11-06 11:59:10Z herbelin $ i*) - (* Concrete syntax of the mathematical vernacular MV V2.6 *) open Pp @@ -19,12 +17,9 @@ open Nameops open Term open Pfedit open Tacmach -open Proof_trees -open Decl_mode open Constrintern open Prettyp open Printer -open Tactic_printer open Tacinterp open Command open Goptions @@ -37,6 +32,7 @@ open Pretyping open Redexpr open Syntax_def open Lemmas +open Declaremods (* Pcoq hooks *) @@ -49,7 +45,7 @@ type pcoq_hook = { 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 + show_goal : goal_reference -> unit } let pcoq = ref None @@ -66,52 +62,34 @@ let cl_of_qualid = function (* "Show" commands *) let show_proof () = - let pts = get_pftreestate () 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) -> Nameops.pr_meta mv ++ str" -> " ++ - pr_ltype ty ++ fnl ()) - meta_types - ++ str"Proof: " ++ pr_lconstr (Evarutil.nf_evar evc pfterm)) + (* spiwack: this would probably be cooler with a bit of polishing. *) + let p = Proof_global.give_me_the_proof () in + let pprf = Proof.partial_proof p in + msgnl (Util.prlist_with_sep Pp.fnl Printer.pr_constr pprf) let show_node () = - let pts = get_pftreestate () in - let pf = proof_of_pftreestate pts - and cursor = cursor_of_pftreestate pts in - msgnl (prlist_with_sep pr_spc pr_int (List.rev cursor) ++ fnl () ++ - pr_goal (goal_of_proof pf) ++ fnl () ++ - (match pf.Proof_type.ref with - | None -> (str"BY <rule>") - | Some(r,spfl) -> - (str"BY " ++ pr_rule r ++ fnl () ++ - str" " ++ - hov 0 (prlist_with_sep pr_fnl pr_goal - (List.map goal_of_proof spfl))))) + (* spiwack: I'm have little clue what this function used to do. I deactivated it, + could, possibly, be cleaned away. (Feb. 2010) *) + () let show_script () = - let pts = get_pftreestate () in - let pf = proof_of_pftreestate pts - and evc = evc_of_pftreestate pts in - msgnl_with !Pp_control.deep_ft (print_treescript evc pf) + (* spiwack: show_script is currently not working *) + () let show_thesis () = msgnl (anomaly "TODO" ) let show_top_evars () = + (* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *) let pfts = get_pftreestate () in - let gls = top_goal_of_pftreestate pfts in - let sigma = project gls in + let gls = Proof.V82.subgoals pfts in + let sigma = gls.Evd.sigma in msg (pr_evars_int 1 (Evarutil.non_instantiated sigma)) + let show_prooftree () = - let pts = get_pftreestate () in - let pf = proof_of_pftreestate pts - and evc = evc_of_pftreestate pts in - msg (print_proof evc (Global.named_context()) pf) + (* Spiwack: proof tree is currently not working *) + () let print_subgoals () = if_verbose (fun () -> msg (pr_open_subgoals ())) () @@ -119,7 +97,8 @@ let print_subgoals () = if_verbose (fun () -> msg (pr_open_subgoals ())) () let show_intro all = let pf = get_pftreestate() in - let gl = nth_goal_of_pftreestate 1 pf in + let {Evd.it=gls ; sigma=sigma} = Proof.V82.subgoals pf in + let gl = {Evd.it=List.hd gls ; sigma = sigma} in let l,_= decompose_prod_assum (strip_outer_cast (pf_concl gl)) in if all then @@ -131,13 +110,12 @@ let show_intro all = msgnl (pr_id (List.hd (Tactics.find_intro_names [n] gl))) with Failure "list_last" -> message "" -let id_of_name = function - | Names.Anonymous -> id_of_string "x" - | Names.Name x -> x - +(** Prepare a "match" template for a given inductive type. + For each branch of the match, we list the constructor name + followed by enough pattern variables. + [Not_found] is raised if the given string isn't the qualid of + a known inductive type. *) -(* Building of match expression *) -(* From ide/coq.ml *) let make_cases s = let qualified_name = Libnames.qualid_of_string s in let glob_ref = Nametab.locate qualified_name in @@ -147,36 +125,31 @@ let make_cases s = , {Declarations.mind_consnames = carr ; Declarations.mind_nf_lc = tarr } = Global.lookup_inductive i in Util.array_fold_right2 - (fun n t l -> - let (al,_) = Term.decompose_prod t in - let al,_ = Util.list_chop (List.length al - np) al in + (fun consname typ l -> + let al = List.rev (fst (Term.decompose_prod typ)) in + let al = Util.list_skipn np al in let rec rename avoid = function | [] -> [] | (n,_)::l -> - let n' = Namegen.next_ident_away_in_goal (id_of_name n) avoid in + let n' = Namegen.next_name_away_in_cases_pattern n avoid in string_of_id n' :: rename (n'::avoid) l in - let al' = rename [] (List.rev al) in - (string_of_id n :: al') :: l) + let al' = rename [] al in + (string_of_id consname :: al') :: l) carr tarr [] | _ -> raise Not_found +(** Textual display of a generic "match" template *) let show_match id = - try - let s = string_of_id (snd id) in - let patterns = List.rev (make_cases s) in - let cases = - List.fold_left - (fun acc x -> - match x with - | [] -> assert false - | [x] -> "| "^ x ^ " => \n" ^ acc - | x::l -> - "| " ^ List.fold_left (fun acc s -> acc ^ " " ^ s) x l - ^ " => \n" ^ acc) - "end" patterns in - msg (str ("match # with\n" ^ cases)) - with Not_found -> error "Unknown inductive type." + let patterns = + try make_cases (string_of_id (snd id)) + with Not_found -> error "Unknown inductive type." + in + let pr_branch l = + str "| " ++ hov 1 (prlist_with_sep spc str l) ++ str " =>" + in + msg (v 1 (str "match # with" ++ fnl () ++ + prlist_with_sep fnl pr_branch patterns ++ fnl ())) (* "Print" commands *) @@ -220,18 +193,55 @@ let print_modtype r = let (loc,qid) = qualid_of_reference r in try let kn = Nametab.locate_modtype qid in - msgnl (Printmod.print_modtype kn) - with - Not_found -> msgnl (str"Unknown Module Type " ++ pr_qualid qid) + msgnl (Printmod.print_modtype kn) + with Not_found -> + (* Is there a module of this name ? If yes we display its type *) + try + let mp = Nametab.locate_module qid in + msgnl (Printmod.print_module false mp) + with Not_found -> + msgnl (str"Unknown Module Type or Module " ++ pr_qualid qid) -let dump_universes s = +let dump_universes_gen g s = let output = open_out s in + let output_constraint, close = + if Filename.check_suffix s ".dot" || Filename.check_suffix s ".gv" then begin + (* the lazy unit is to handle errors while printing the first line *) + let init = lazy (Printf.fprintf output "digraph universes {\n") in + begin fun kind left right -> + let () = Lazy.force init in + match kind with + | Univ.Lt -> + Printf.fprintf output " \"%s\" -> \"%s\" [style=bold];\n" right left + | Univ.Le -> + Printf.fprintf output " \"%s\" -> \"%s\" [style=solid];\n" right left + | Univ.Eq -> + Printf.fprintf output " \"%s\" -> \"%s\" [style=dashed];\n" left right + end, begin fun () -> + if Lazy.lazy_is_val init then Printf.fprintf output "}\n"; + close_out output + end + end else begin + begin fun kind left right -> + let kind = match kind with + | Univ.Lt -> "<" + | Univ.Le -> "<=" + | Univ.Eq -> "=" + in Printf.fprintf output "%s %s %s ;\n" left kind right + end, (fun () -> close_out output) + end + in try - Univ.dump_universes output (Global.universes ()); - close_out output; + Univ.dump_universes output_constraint g; + close (); msgnl (str ("Universes written to file \""^s^"\".")) with - e -> close_out output; raise e + e -> close (); raise e + +let dump_universes sorted s = + let g = Global.universes () in + let g = if sorted then Univ.sort_universes g else g in + dump_universes_gen g s (*********************) (* "Locate" commands *) @@ -318,7 +328,7 @@ let start_proof_and_print k l hook = print_subgoals (); if !pcoq <> None then (Option.get !pcoq).start_proof () -let vernac_definition (local,boxed,k) (loc,id as lid) def hook = +let vernac_definition (local,k) (loc,id as lid) def hook = if local = Local then Dumpglob.dump_definition lid true "var" else Dumpglob.dump_definition lid false "def"; (match def with @@ -332,7 +342,7 @@ let vernac_definition (local,boxed,k) (loc,id as lid) def hook = | Some r -> let (evc,env)= get_current_context () in Some (interp_redexp env evc r) in - let ce,imps = interp_definition boxed bl red_option c typ_opt in + let ce,imps = interp_definition bl red_option c typ_opt in declare_definition id (local,k) ce imps hook) let vernac_start_proof kind l lettop hook = @@ -360,14 +370,10 @@ let vernac_end_proof = function the theories [??] *) let vernac_exact_proof c = - let pfs = top_of_tree (get_pftreestate()) in - let pf = proof_of_pftreestate pfs in - if (is_leaf_proof pf) then begin - by (Tactics.exact_proof c); - save_named true end - else - errorlabstrm "Vernacentries.ExactProof" - (strbrk "Command 'Proof ...' can only be used at the beginning of the proof.") + (* spiwack: for simplicity I do not enforce that "Proof proof_term" is + called only at the begining of a proof. *) + by (Tactics.exact_proof c); + save_named true let vernac_assumption kind l nl= let global = fst kind = Global in @@ -386,7 +392,7 @@ let vernac_record k finite infer struc binders sort nameopt cfs = Dumpglob.dump_definition lid false "constr"; id in if Dumpglob.dump () then ( Dumpglob.dump_definition (snd struc) false "rec"; - List.iter (fun ((_, x), _) -> + List.iter (fun (((_, x), _), _) -> match x with | Vernacexpr.AssumExpr ((loc, Name id), _) -> Dumpglob.dump_definition (loc,id) false "proj" | _ -> ()) cfs); @@ -409,7 +415,8 @@ let vernac_inductive finite infer indl = | [ ( id , bl , c , Class true, Constructors [l]), _ ] -> let f = let (coe, ((loc, id), ce)) = l in - ((coe, AssumExpr ((loc, Name id), ce)), []) + let coe' = if coe then Some true else None in + (((coe', AssumExpr ((loc, Name id), ce)), None), []) in vernac_record (Class true) finite infer id bl c None [f] | [ ( id , bl , c , Class true, _), _ ] -> Util.error "Definitional classes must have a single method" @@ -424,15 +431,15 @@ let vernac_inductive finite infer indl = let indl = List.map unpack indl in do_mutual_inductive indl (recursivity_flag_of_kind finite) -let vernac_fixpoint l b = +let vernac_fixpoint l = if Dumpglob.dump () then List.iter (fun ((lid, _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l; - do_fixpoint l b + do_fixpoint l -let vernac_cofixpoint l b = +let vernac_cofixpoint l = if Dumpglob.dump () then List.iter (fun ((lid, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l; - do_cofixpoint l b + do_cofixpoint l let vernac_scheme = Indschemes.do_scheme @@ -585,10 +592,10 @@ let vernac_end_section (loc,_) = let vernac_end_segment (_,id as lid) = check_no_pending_proofs (); match Lib.find_opening_node id with - | Lib.OpenedModule (export,_,_) -> vernac_end_module export lid - | Lib.OpenedModtype _ -> vernac_end_modtype lid + | Lib.OpenedModule (false,export,_,_) -> vernac_end_module export lid + | Lib.OpenedModule (true,_,_,_) -> vernac_end_modtype lid | Lib.OpenedSection _ -> vernac_end_section lid - | _ -> anomaly "No more opened things" + | _ -> assert false (* Libraries *) @@ -608,13 +615,13 @@ let vernac_coercion stre ref qids qidt = let target = cl_of_qualid qidt in let source = cl_of_qualid qids in let ref' = smart_global ref in - Class.try_add_new_coercion_with_target ref' stre source target; + Class.try_add_new_coercion_with_target ref' stre ~source ~target; if_verbose msgnl (pr_global ref' ++ str " 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 + Class.try_add_new_identity_coercion id stre ~source ~target (* Type classes *) @@ -625,32 +632,32 @@ let vernac_instance abst glob sup inst props pri = let vernac_context l = Classes.context l -let vernac_declare_instance glob id = - Classes.declare_instance glob id +let vernac_declare_instances glob ids = + List.iter (fun (id) -> Classes.existing_instance glob id) ids let vernac_declare_class id = Classes.declare_class id (***********) (* Solving *) + +let command_focus = Proof.new_focus_kind () +let focus_command_cond = Proof.no_cond command_focus + + let vernac_solve n tcom b = if not (refining ()) then error "Unknown command of the non proof-editing mode."; - Decl_mode.check_not_proof_mode "Unknown proof instruction"; - begin - if b then - solve_nth n (Tacinterp.hide_interp tcom (get_end_tac ())) - else solve_nth n (Tacinterp.hide_interp tcom None) - end; - (* in case a strict subtree was completed, - go back to the top of the prooftree *) - if subtree_solved () then begin - Flags.if_verbose msgnl (str "Subgoal proved"); - make_focus 0; - reset_top_of_script () - end; - print_subgoals(); - if !pcoq <> None then (Option.get !pcoq).solve n + let p = Proof_global.give_me_the_proof () in + Proof.transaction p begin fun () -> + solve_nth n (Tacinterp.hide_interp tcom None) ~with_end_tac:b; + (* in case a strict subtree was completed, + go back to the top of the prooftree *) + Proof_global.maximal_unfocus command_focus p; + print_subgoals(); + if !pcoq <> None then (Option.get !pcoq).solve n + end + (* A command which should be a tactic. It has been added by Christine to patch an error in the design of the proof @@ -666,32 +673,15 @@ let vernac_set_end_tac tac = if tac <> (Tacexpr.TacId []) then set_end_tac (Tacinterp.interp tac) else () (* TO DO verifier s'il faut pas mettre exist s | TacId s ici*) -(***********************) -(* Proof Language Mode *) - -let vernac_decl_proof () = - check_not_proof_mode "Already in Proof Mode"; - if tree_solved () then - error "Nothing left to prove here." - else - begin - Decl_proof_instr.go_to_proof_mode (); - print_subgoals () - end - -let vernac_return () = - match get_current_mode () with - Mode_tactic -> - Decl_proof_instr.return_from_tactic_mode (); - print_subgoals () - | Mode_proof -> - error "\"return\" is only used after \"escape\"." - | Mode_none -> - error "There is no proof to end." - -let vernac_proof_instr instr = - Decl_proof_instr.proof_instr instr; - print_subgoals () +let vernac_set_used_variables l = + let l = List.map snd l in + if not (list_distinct l) then error "Used variables list contains duplicates"; + let vars = Environ.named_context (Global.env ()) in + List.iter (fun id -> + if not (List.exists (fun (id',_,_) -> id = id') vars) then + error ("Unknown variable: " ^ string_of_id id)) + l; + set_used_variables l (*****************************) (* Auxiliary file management *) @@ -706,7 +696,7 @@ 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 + (if isrec then Mltop.add_rec_path else Mltop.add_path) ~unix_path:pdir ~coq_root:alias let vernac_remove_loadpath path = Library.remove_load_path (System.expand_path_macros path) @@ -764,6 +754,9 @@ let vernac_declare_tactic_definition (local,x,def) = let vernac_create_hintdb local id b = Auto.create_hint_db local id full_transparent_state b +let vernac_remove_hints local dbs ids = + Auto.remove_hints local dbs (List.map Smartlocate.global_with_alias ids) + let vernac_hints local lb h = Auto.add_hints local lb (Auto.interp_hints h) @@ -778,11 +771,89 @@ let vernac_declare_implicits local r = function Impargs.declare_manual_implicits local (smart_global r) ~enriching:false (List.map (List.map (fun (ex,b,f) -> ex, (b,true,f))) imps) +let vernac_declare_arguments local r l nargs flags = + let names = List.map (List.map (fun (id, _,_,_,_) -> id)) l in + let names, rest = List.hd names, List.tl names in + if List.exists ((<>) names) rest then + error "All arguments lists must declare the same names."; + if not (Util.list_distinct (List.filter ((<>) Anonymous) names)) then + error "Arguments names must be distinct."; + let sr = smart_global r in + let inf_names = + Impargs.compute_implicits_names (Global.env()) (Global.type_of_global sr) in + let string_of_name = function Anonymous -> "_" | Name id -> string_of_id id in + let rec check li ld = match li, ld with + | [], [] -> () + | [], x::_ -> error ("Extra argument " ^ string_of_name x ^ ".") + | l, [] -> error ("The following arguments are not declared: " ^ + (String.concat ", " (List.map string_of_name l)) ^ ".") + | _::li, _::ld -> check li ld in + if l <> [[]] then + List.iter (fun l -> check inf_names l) (names :: rest); + (* we interpret _ as the inferred names *) + let l = if l = [[]] then l else + let name_anons = function + | (Anonymous, a,b,c,d), Name id -> Name id, a,b,c,d + | x, _ -> x in + List.map (fun ns -> List.map name_anons (List.combine ns inf_names)) l in + let names_decl = List.map (List.map (fun (id, _,_,_,_) -> id)) l in + let some_renaming_specified = + try Arguments_renaming.arguments_names sr <> names_decl + with Not_found -> false in + let some_renaming_specified, implicits = + if l = [[]] then false, [[]] else + Util.list_fold_map (fun sr il -> + let sr', impl = Util.list_fold_map (fun b -> function + | (Anonymous, _,_, true, max), Name id -> assert false + | (Name x, _,_, true, _), Anonymous -> + error ("Argument "^string_of_id x^" cannot be declared implicit.") + | (Name iid, _,_, true, max), Name id -> + b || iid <> id, Some (ExplByName id, max, false) + | (Name iid, _,_, _, _), Name id -> b || iid <> id, None + | _ -> b, None) + sr (List.combine il inf_names) in + sr || sr', Util.list_map_filter (fun x -> x) impl) + some_renaming_specified l in + if some_renaming_specified then + if not (List.mem `Rename flags) then + error "To rename arguments the \"rename\" flag must be specified." + else Arguments_renaming.rename_arguments local sr names_decl; + (* All other infos are in the first item of l *) + let l = List.hd l in + let some_implicits_specified = implicits <> [[]] in + let scopes = List.map (function + | (_,_, None,_,_) -> None + | (_,_, Some (o, k), _,_) -> + try Some(ignore(Notation.find_scope k); k) + with _ -> Some (Notation.find_delimiters_scope o k)) l in + let some_scopes_specified = List.exists ((<>) None) scopes in + let rargs = + Util.list_map_filter (function (n, true) -> Some n | _ -> None) + (Util.list_map_i (fun i (_, b, _,_,_) -> i, b) 0 l) in + if some_scopes_specified || List.mem `ClearScopes flags then + vernac_arguments_scope local r scopes; + if not some_implicits_specified && List.mem `DefaultImplicits flags then + vernac_declare_implicits local r [] + else if some_implicits_specified || List.mem `ClearImplicits flags then + vernac_declare_implicits local r implicits; + if nargs >= 0 && nargs < List.fold_left max 0 rargs then + error "The \"/\" option must be placed after the last \"!\"."; + let rec narrow = function + | #Tacred.simpl_flag as x :: tl -> x :: narrow tl + | [] -> [] | _ :: tl -> narrow tl in + let flags = narrow flags in + if rargs <> [] || nargs >= 0 || flags <> [] then + match sr with + | ConstRef _ as c -> + Tacred.set_simpl_behaviour local c (rargs, nargs, flags) + | _ -> errorlabstrm "" (strbrk "Modifiers of the behavior of the simpl tactic are relevant for constants only.") + let vernac_reserve bl = let sb_decl = (fun (idl,c) -> let t = Constrintern.interp_type Evd.empty (Global.env()) c in - let t = Detyping.detype false [] [] t in - List.iter (fun id -> Reserve.declare_reserved_type id t) idl) + let t = Detyping.detype false [] [] t in + let t = aconstr_of_glob_constr [] [] t in + Reserve.declare_reserved_type idl t) in List.iter sb_decl bl let vernac_generalizable = Implicit_quantifiers.declare_generalizable @@ -795,6 +866,7 @@ let make_silent_if_not_pcoq b = let _ = declare_bool_option { optsync = false; + optdepr = false; optname = "silent"; optkey = ["Silent"]; optread = is_silent; @@ -803,6 +875,7 @@ let _ = let _ = declare_bool_option { optsync = true; + optdepr = false; optname = "implicit arguments"; optkey = ["Implicit";"Arguments"]; optread = Impargs.is_implicit_args; @@ -811,6 +884,7 @@ let _ = let _ = declare_bool_option { optsync = true; + optdepr = false; optname = "strict implicit arguments"; optkey = ["Strict";"Implicit"]; optread = Impargs.is_strict_implicit_args; @@ -819,6 +893,7 @@ let _ = let _ = declare_bool_option { optsync = true; + optdepr = false; optname = "strong strict implicit arguments"; optkey = ["Strongly";"Strict";"Implicit"]; optread = Impargs.is_strongly_strict_implicit_args; @@ -827,22 +902,16 @@ let _ = let _ = declare_bool_option { optsync = true; + optdepr = false; optname = "contextual implicit arguments"; optkey = ["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 = ["Forceable";"Implicit")); *) -(* optread = Impargs.is_forceable_implicit_args; *) -(* optwrite = Impargs.make_forceable_implicit_args } *) - let _ = declare_bool_option { optsync = true; + optdepr = false; optname = "implicit status of reversible patterns"; optkey = ["Reversible";"Pattern";"Implicit"]; optread = Impargs.is_reversible_pattern_implicit_args; @@ -851,6 +920,7 @@ let _ = let _ = declare_bool_option { optsync = true; + optdepr = false; optname = "maximal insertion of implicit"; optkey = ["Maximal";"Implicit";"Insertion"]; optread = Impargs.is_maximal_implicit_args; @@ -859,6 +929,7 @@ let _ = let _ = declare_bool_option { optsync = true; + optdepr = false; optname = "automatic introduction of variables"; optkey = ["Automatic";"Introduction"]; optread = Flags.is_auto_intros; @@ -867,6 +938,7 @@ let _ = let _ = declare_bool_option { optsync = true; + optdepr = false; optname = "coercion printing"; optkey = ["Printing";"Coercions"]; optread = (fun () -> !Constrextern.print_coercions); @@ -875,6 +947,7 @@ let _ = let _ = declare_bool_option { optsync = true; + optdepr = false; optname = "printing of existential variable instances"; optkey = ["Printing";"Existential";"Instances"]; optread = (fun () -> !Constrextern.print_evar_arguments); @@ -882,6 +955,7 @@ let _ = let _ = declare_bool_option { optsync = true; + optdepr = false; optname = "implicit arguments printing"; optkey = ["Printing";"Implicit"]; optread = (fun () -> !Constrextern.print_implicits); @@ -890,6 +964,7 @@ let _ = let _ = declare_bool_option { optsync = true; + optdepr = false; optname = "implicit arguments defensive printing"; optkey = ["Printing";"Implicit";"Defensive"]; optread = (fun () -> !Constrextern.print_implicits_defensive); @@ -898,6 +973,7 @@ let _ = let _ = declare_bool_option { optsync = true; + optdepr = false; optname = "projection printing using dot notation"; optkey = ["Printing";"Projections"]; optread = (fun () -> !Constrextern.print_projections); @@ -906,6 +982,7 @@ let _ = let _ = declare_bool_option { optsync = true; + optdepr = false; optname = "notations printing"; optkey = ["Printing";"Notations"]; optread = (fun () -> not !Constrextern.print_no_symbol); @@ -914,6 +991,7 @@ let _ = let _ = declare_bool_option { optsync = true; + optdepr = false; optname = "raw printing"; optkey = ["Printing";"All"]; optread = (fun () -> !Flags.raw_print); @@ -922,38 +1000,57 @@ let _ = let _ = declare_bool_option { optsync = true; + optdepr = false; + optname = "record printing"; + optkey = ["Printing";"Records"]; + optread = (fun () -> !Flags.record_print); + optwrite = (fun b -> Flags.record_print := b) } + +let _ = + declare_bool_option + { optsync = true; + optdepr = false; optname = "use of virtual machine inside the kernel"; optkey = ["Virtual";"Machine"]; optread = (fun () -> Vconv.use_vm ()); optwrite = (fun b -> Vconv.set_use_vm b) } let _ = - declare_bool_option + declare_int_option { optsync = true; - optname = "use of boxed definitions"; - optkey = ["Boxed";"Definitions"]; - optread = Flags.boxed_definitions; - optwrite = (fun b -> Flags.set_boxed_definitions b) } + optdepr = false; + optname = "the level of inling duging functor application"; + optkey = ["Inline";"Level"]; + optread = (fun () -> Some (Flags.get_inline_level ())); + optwrite = (fun o -> + let lev = Option.default Flags.default_inline_level o in + Flags.set_inline_level lev) } let _ = declare_bool_option { optsync = true; + optdepr = false; optname = "use of boxed values"; optkey = ["Boxed";"Values"]; optread = (fun _ -> not (Vm.transp_values ())); optwrite = (fun b -> Vm.set_transp_values (not b)) } +(* No more undo limit in the new proof engine. + The command still exists for compatibility (e.g. with ProofGeneral) *) + let _ = declare_int_option { optsync = false; - optname = "the undo limit"; + optdepr = true; + optname = "the undo limit (OBSOLETE)"; optkey = ["Undo"]; - optread = Pfedit.get_undo; - optwrite = Pfedit.set_undo } + optread = (fun _ -> None); + optwrite = (fun _ -> ()) } let _ = declare_int_option { optsync = false; + optdepr = false; optname = "the hypotheses limit"; optkey = ["Hyps";"Limit"]; optread = Flags.print_hyps_limit; @@ -962,6 +1059,7 @@ let _ = let _ = declare_int_option { optsync = true; + optdepr = false; optname = "the printing depth"; optkey = ["Printing";"Depth"]; optread = Pp_control.get_depth_boxes; @@ -970,6 +1068,7 @@ let _ = let _ = declare_int_option { optsync = true; + optdepr = false; optname = "the printing width"; optkey = ["Printing";"Width"]; optread = Pp_control.get_margin; @@ -978,6 +1077,7 @@ let _ = let _ = declare_bool_option { optsync = true; + optdepr = false; optname = "printing of universes"; optkey = ["Printing";"Universes"]; optread = (fun () -> !Constrextern.print_universes); @@ -989,6 +1089,7 @@ let vernac_debug b = let _ = declare_bool_option { optsync = false; + optdepr = false; optname = "Ltac debug"; optkey = ["Ltac";"Debug"]; optread = (fun () -> get_debug () <> Tactic_debug.DebugOff); @@ -1006,7 +1107,7 @@ let vernac_set_opacity local str = let vernac_set_option locality key = function | StringValue s -> set_string_option_value_gen locality key s - | IntValue n -> set_int_option_value_gen locality key (Some n) + | IntValue n -> set_int_option_value_gen locality key n | BoolValue b -> set_bool_option_value_gen locality key b let vernac_unset_option locality key = @@ -1046,18 +1147,25 @@ let get_current_context_of_args = function | 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 + let module P = Pretype_errors in + let (sigma, env) = get_current_context_of_args glopt in + let sigma', c = interp_open_constr sigma env rc in + let j = + try + Evarutil.check_evars env sigma sigma' c; + Arguments_renaming.rename_typing env c + with P.PretypeError (_,_,P.UnsolvableImplicit _) + | Compat.Loc.Exc_located (_,P.PretypeError (_,_,P.UnsolvableImplicit _)) -> + Evarutil.j_nf_evar sigma' (Retyping.get_judgment_of env sigma' c) in match redexp with | None -> 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 + let redfun = fst (reduction_of_red_expr (interp_redexp env sigma' r)) in if !pcoq <> None - then (Option.get !pcoq).print_eval redfun env evmap rc j - else msg (print_eval redfun env evmap rc j) + then (Option.get !pcoq).print_eval redfun env sigma' rc j + else msg (print_eval redfun env sigma' rc j) let vernac_declare_reduction locality s r = declare_red_expr locality s (interp_redexp (Global.env()) Evd.empty r) @@ -1095,19 +1203,22 @@ let vernac_print = function | PrintCoercionPaths (cls,clt) -> ppnl (Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt)) | PrintCanonicalConversions -> ppnl (Prettyp.print_canonical_projections ()) - | PrintUniverses None -> pp (Univ.pr_universes (Global.universes ())) - | PrintUniverses (Some s) -> dump_universes s + | PrintUniverses (b, None) -> + let univ = Global.universes () in + let univ = if b then Univ.sort_universes univ else univ in + pp (Univ.pr_universes univ) + | PrintUniverses (b, Some s) -> dump_universes b s | PrintHint r -> Auto.print_hint_ref (smart_global r) | PrintHintGoal -> Auto.print_applicable_hint () | PrintHintDbName s -> Auto.print_hint_db_by_name s | PrintRewriteHintDbName s -> Autorewrite.print_rewrite_hintdb s | PrintHintDb -> Auto.print_searchtable () | PrintScopes -> - pp (Notation.pr_scopes (Constrextern.without_symbols pr_lrawconstr)) + pp (Notation.pr_scopes (Constrextern.without_symbols pr_lglob_constr)) | PrintScope s -> - pp (Notation.pr_scope (Constrextern.without_symbols pr_lrawconstr) s) + pp (Notation.pr_scope (Constrextern.without_symbols pr_lglob_constr) s) | PrintVisibility s -> - pp (Notation.pr_visibility (Constrextern.without_symbols pr_lrawconstr) s) + pp (Notation.pr_visibility (Constrextern.without_symbols pr_lglob_constr) s) | PrintAbout qid -> msg (print_about qid) | PrintImplicit qid -> msg (print_impargs qid) | PrintAssumptions (o,r) -> @@ -1145,7 +1256,7 @@ let interp_search_about_item = function (fun _ -> true) s sc in GlobSearchSubPattern (Pattern.PRef ref) with UserError _ -> - error ("Unable to interp \""^s^"\" either as a reference or + error ("Unable to interp \""^s^"\" either as a reference or \ as an identifier component") let vernac_search s r = @@ -1169,7 +1280,7 @@ let vernac_locate = function | LocateTerm (Genarg.ByNotation (_,ntn,sc)) -> ppnl (Notation.locate_notation - (Constrextern.without_symbols pr_lrawconstr) ntn sc) + (Constrextern.without_symbols pr_lglob_constr) ntn sc) | LocateLibrary qid -> print_located_library qid | LocateModule qid -> print_located_module qid | LocateTactic qid -> print_located_tactic qid @@ -1178,16 +1289,6 @@ let vernac_locate = function (********************) (* Proof management *) -let vernac_goal = function - | None -> () - | Some c -> - if not (refining()) then begin - let unnamed_kind = Lemma (* Arbitrary *) in - start_proof_com (Global, Proof unnamed_kind) [None,c] (fun _ _ ->()); - print_subgoals () - end else - error "repeated Goal not permitted in refining mode." - let vernac_abort = function | None -> delete_current_proof (); @@ -1229,48 +1330,58 @@ let vernac_backtrack snum pnum naborts = vernac_backto snum; Pp.flush_all(); (* there may be no proof in progress, even if no abort *) - (try print_subgoals () with UserError _ -> ()) + (try print_subgoals () with Proof_global.NoCurrentProof | UserError _ -> ()) let vernac_focus gln = - check_not_proof_mode "No focussing or Unfocussing in Proof Mode."; + let p = Proof_global.give_me_the_proof () in match gln with - | None -> traverse_nth_goal 1; print_subgoals () - | Some n -> traverse_nth_goal n; print_subgoals () + | None -> Proof.focus focus_command_cond () 1 p; print_subgoals () + | Some n -> Proof.focus focus_command_cond () n p; print_subgoals () + - (* Reset the focus to the top of the tree *) + (* Unfocuses one step in the focus stack. *) let vernac_unfocus () = - check_not_proof_mode "No focussing or Unfocussing in Proof Mode."; - make_focus 0; reset_top_of_script (); print_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 (fun evd _ -> print_treescript evd) occ) - -let explain_tree occ = - msg (apply_subproof print_proof occ) + let p = Proof_global.give_me_the_proof () in + Proof.unfocus command_focus p; print_subgoals () + +(* BeginSubproof / EndSubproof. + BeginSubproof (vernac_subproof) focuses on the first goal, or the goal + given as argument. + EndSubproof (vernac_end_subproof) unfocuses from a BeginSubproof, provided + that the proof of the goal has been completed. +*) +let subproof_kind = Proof.new_focus_kind () +let subproof_cond = Proof.done_cond subproof_kind + +let vernac_subproof gln = + let p = Proof_global.give_me_the_proof () in + begin match gln with + | None -> Proof.focus subproof_cond () 1 p + | Some n -> Proof.focus subproof_cond () n p + end ; + print_subgoals () + +let vernac_end_subproof () = + let p = Proof_global.give_me_the_proof () in + Proof.unfocus subproof_kind p ; print_subgoals () + + +let vernac_bullet (bullet:Proof_global.Bullet.t) = + let p = Proof_global.give_me_the_proof () in + Proof.transaction p + (fun () -> Proof_global.Bullet.put p bullet); + (* Makes the focus visible in emacs by re-printing the goal. *) + if !Flags.print_emacs then print_subgoals () + let vernac_show = function - | ShowGoal 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) + | ShowGoal goalref -> + if !pcoq <> None then (Option.get !pcoq).show_goal goalref + else msg (match goalref with + | OpenSubgoals -> pr_open_subgoals () + | NthGoal n -> pr_nth_open_subgoal n + | GoalId id -> pr_goal_by_id id) | ShowGoalImplicitly None -> Constrextern.with_implicits msg (pr_open_subgoals ()) | ShowGoalImplicitly (Some n) -> @@ -1285,17 +1396,15 @@ let vernac_show = function | ShowIntros all -> show_intro all | ShowMatch id -> show_match id | ShowThesis -> show_thesis () - | 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 in - let (pfterm,_) = extract_open_pftreestate pts in + let pfterm = List.hd (Proof.partial_proof pts) in let message = try - Inductiveops.control_only_guard (Evd.evar_env (goal_of_proof pf)) + let { Evd.it=gl ; sigma=sigma } = Proof.V82.top_goal pts in + Inductiveops.control_only_guard (Goal.V82.env sigma gl) pfterm; (str "The condition holds up to here") with UserError(_,s) -> @@ -1325,8 +1434,8 @@ let interp c = match c with | VernacExactProof c -> vernac_exact_proof c | VernacAssumption (stre,nl,l) -> vernac_assumption stre l nl | VernacInductive (finite,infer,l) -> vernac_inductive finite infer l - | VernacFixpoint (l,b) -> vernac_fixpoint l b - | VernacCoFixpoint (l,b) -> vernac_cofixpoint l b + | VernacFixpoint l -> vernac_fixpoint l + | VernacCoFixpoint l -> vernac_cofixpoint l | VernacScheme l -> vernac_scheme l | VernacCombinedScheme (id, l) -> vernac_combined_scheme id l @@ -1354,21 +1463,13 @@ let interp c = match c with | VernacInstance (abst, glob, sup, inst, props, pri) -> vernac_instance abst glob sup inst props pri | VernacContext sup -> vernac_context sup - | VernacDeclareInstance (glob, id) -> vernac_declare_instance glob id + | VernacDeclareInstances (glob, ids) -> vernac_declare_instances glob ids | VernacDeclareClass id -> vernac_declare_class id (* Solving *) | VernacSolve (n,tac,b) -> vernac_solve n tac b | VernacSolveExistential (n,c) -> vernac_solve_existential n c - (* MMode *) - - | VernacDeclProof -> vernac_decl_proof () - | VernacReturn -> vernac_return () - | VernacProofInstr stp -> vernac_proof_instr stp - - (* /MMode *) - (* Auxiliary file and library management *) | VernacRequireFrom (exp,spec,f) -> vernac_require_from exp spec f | VernacAddLoadPath (isrec,s,alias) -> vernac_add_loadpath isrec s alias @@ -1391,9 +1492,11 @@ let interp c = match c with (* Commands *) | VernacDeclareTacticDefinition def -> vernac_declare_tactic_definition def | VernacCreateHintDb (local,dbname,b) -> vernac_create_hintdb local dbname b + | VernacRemoveHints (local,dbnames,ids) -> vernac_remove_hints local dbnames ids | VernacHints (local,dbnames,hints) -> vernac_hints local dbnames hints | VernacSyntacticDefinition (id,c,l,b) ->vernac_syntactic_definition id c l b | VernacDeclareImplicits (local,qid,l) ->vernac_declare_implicits local qid l + | VernacArguments (local, qid, l, narg, flags) -> vernac_declare_arguments local qid l narg flags | VernacReserve bl -> vernac_reserve bl | VernacGeneralizable (local,gen) -> vernac_generalizable local gen | VernacSetOpacity (local,qidl) -> vernac_set_opacity local qidl @@ -1424,10 +1527,17 @@ let interp c = match c with | VernacBacktrack (snum,pnum,naborts) -> vernac_backtrack snum pnum naborts | VernacFocus n -> vernac_focus n | VernacUnfocus -> vernac_unfocus () - | VernacGo g -> vernac_go g + | VernacBullet b -> vernac_bullet b + | VernacSubproof n -> vernac_subproof n + | VernacEndSubproof -> vernac_end_subproof () | VernacShow s -> vernac_show s | VernacCheckGuard -> vernac_check_guard () - | VernacProof tac -> vernac_set_end_tac tac + | VernacProof (None, None) -> () + | VernacProof (Some tac, None) -> vernac_set_end_tac tac + | VernacProof (None, Some l) -> vernac_set_used_variables l + | VernacProof (Some tac, Some l) -> + vernac_set_end_tac tac; vernac_set_used_variables l + | VernacProofMode mn -> Proof_global.set_proof_mode mn (* Toplevel control *) | VernacToplevelControl e -> raise e diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli index 1cca3540..8fb6f466 100644 --- a/toplevel/vernacentries.mli +++ b/toplevel/vernacentries.mli @@ -1,34 +1,31 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: vernacentries.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(*i*) open Names open Term open Vernacinterp open Vernacexpr open Topconstr -(*i*) -(* Vernacular entries *) +(** Vernacular entries *) val show_script : unit -> unit val show_prooftree : unit -> unit val show_node : unit -> unit -(* This function can be used by any command that want to observe terms +(** This function can be used by any command that want to observe terms in the context of the current goal, as for instance in pcoq *) val get_current_context_of_args : int option -> Evd.evar_map * Environ.env (*i -(* this function is used to analyse the extra arguments in search commands. + +(** this function is used to analyse the extra arguments in search commands. It is used in pcoq. *) (*i anciennement: inside_outside i*) val interp_search_restriction : search_restriction -> dir_path list * bool i*) @@ -42,12 +39,12 @@ type pcoq_hook = { 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 + show_goal : goal_reference -> unit } val set_pcoq_hook : pcoq_hook -> unit -(* This function makes sure that the function given in argument is preceded +(** This function makes sure that the function given in argument is preceded by a command aborting all proofs if necessary. It is used in pcoq. *) val abort_refine : ('a -> unit) -> 'a -> unit;; @@ -55,3 +52,17 @@ val abort_refine : ('a -> unit) -> 'a -> unit;; val interp : Vernacexpr.vernac_expr -> unit val vernac_reset_name : identifier Util.located -> unit + +val vernac_backtrack : int -> int -> int -> unit + +(* Print subgoals when the verbose flag is on. Meant to be used inside + vernac commands from plugins. *) +val print_subgoals : unit -> unit + +(** Prepare a "match" template for a given inductive type. + For each branch of the match, we list the constructor name + followed by enough pattern variables. + [Not_found] is raised if the given string isn't the qualid of + a known inductive type. *) + +val make_cases : string -> string list list diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 31c46a54..850bc111 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -1,13 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: vernacexpr.ml 14641 2011-11-06 11:59:10Z herbelin $ i*) - +open Compat open Util open Names open Tacexpr @@ -16,6 +15,7 @@ open Genarg open Topconstr open Decl_kinds open Ppextend +open Declaremods (* Toplevel control exceptions *) exception Drop @@ -31,6 +31,13 @@ type lreference = reference type class_rawexpr = FunClass | SortClass | RefClass of reference or_by_notation +type goal_identifier = string + +type goal_reference = + | OpenSubgoals + | NthGoal of int + | GoalId of goal_identifier + type printable = | PrintTables | PrintFullContext @@ -52,7 +59,7 @@ type printable = | PrintCoercions | PrintCoercionPaths of class_rawexpr * class_rawexpr | PrintCanonicalConversions - | PrintUniverses of string option + | PrintUniverses of bool * string option | PrintHint of reference or_by_notation | PrintHintGoal | PrintHintDbName of string @@ -82,14 +89,8 @@ type locatable = | LocateTactic of reference | LocateFile of string -type goable = - | GoTo of int - | GoTop - | GoNext - | GoPrev - type showable = - | ShowGoal of int option + | ShowGoal of goal_reference | ShowGoalImplicitly of int option | ShowProof | ShowNode @@ -100,8 +101,6 @@ type showable = | ShowIntros of bool | ShowMatch of lident | ShowThesis - | ExplainProof of int list - | ExplainTree of int list type comment = | CommentConstr of constr_expr @@ -126,7 +125,8 @@ type rec_flag = bool (* true = Rec; false = NoRec *) type verbose_flag = bool (* true = Verbose; false = Silent *) type opacity_flag = bool (* true = Opaque; false = Transparent *) type locality_flag = bool (* true = Local; false = Global *) -type coercion_flag = bool (* true = AddCoercion; false = NoCoercion *) +type coercion_flag = bool (* true = AddCoercion false = NoCoercion *) +type instance_flag = bool option (* Some true = Backward instance; Some false = Forward instance, None = NoInstance *) type export_flag = bool (* true = Export; false = Import *) type specif_flag = bool (* true = Specification; false = Implementation *) type inductive_flag = Decl_kinds.recursivity_kind @@ -134,16 +134,16 @@ type onlyparsing_flag = bool (* true = Parse only; false = Print also *) type infer_flag = bool (* true = try to Infer record; false = nothing *) type full_locality_flag = bool option (* true = Local; false = Global *) -type option_value = - | StringValue of string - | IntValue of int +type option_value = Goptionstyp.option_value = | BoolValue of bool + | IntValue of int option + | StringValue of string type option_ref_value = | StringRefValue of string | QualidRefValue of reference -type sort_expr = Rawterm.rawsort +type sort_expr = Glob_term.glob_sort type definition_expr = | ProveBody of local_binder list * constr_expr @@ -165,11 +165,13 @@ type decl_notation = lstring * constr_expr * scope_name option type simple_binder = lident list * constr_expr type class_binder = lident * constr_expr list type 'a with_coercion = coercion_flag * 'a +type 'a with_instance = instance_flag * 'a type 'a with_notation = 'a * decl_notation list +type 'a with_priority = 'a * int option type constructor_expr = (lident * constr_expr) with_coercion type constructor_list_or_record_decl_expr = | Constructors of constructor_expr list - | RecordDecl of lident option * local_decl_expr with_coercion with_notation list + | RecordDecl of lident option * local_decl_expr with_instance with_priority with_notation list type inductive_expr = lident with_coercion * local_binder list * constr_expr option * inductive_kind * constructor_list_or_record_decl_expr @@ -177,6 +179,7 @@ type inductive_expr = type one_inductive_expr = lident * local_binder list * constr_expr option * constructor_expr list +type module_ast_inl = module_ast annotated type module_binder = bool option * lident list * module_ast_inl type grammar_tactic_prod_item_expr = @@ -186,7 +189,7 @@ type grammar_tactic_prod_item_expr = type syntax_modifier = | SetItemLevel of string list * production_level | SetLevel of int - | SetAssoc of Gramext.g_assoc + | SetAssoc of gram_assoc | SetEntryType of string * simple_constr_prod_entry_key | SetOnlyParsing | SetFormat of string located @@ -200,6 +203,13 @@ type scheme = | CaseScheme of bool * reference or_by_notation * sort_expr | EqualityScheme of reference or_by_notation +type inline = int option (* inlining level, none for no inlining *) + +type bullet = + | Dash + | Star + | Plus + type vernac_expr = (* Control *) | VernacList of located_vernac_expr list @@ -214,8 +224,6 @@ type vernac_expr = | VernacOpenCloseScope of (locality_flag * bool * scope_name) | VernacDelimiters of scope_name * string | VernacBindScope of scope_name * class_rawexpr list - | VernacArgumentsScope of locality_flag * reference or_by_notation * - scope_name option list | VernacInfix of locality_flag * (lstring * syntax_modifier list) * constr_expr * scope_name option | VernacNotation of @@ -230,10 +238,10 @@ type vernac_expr = bool * declaration_hook | VernacEndProof of proof_end | VernacExactProof of constr_expr - | VernacAssumption of assumption_kind * bool * simple_binder with_coercion list + | VernacAssumption of assumption_kind * inline * simple_binder with_coercion list | VernacInductive of inductive_flag * infer_flag * (inductive_expr * decl_notation list) list - | VernacFixpoint of (fixpoint_expr * decl_notation list) list * bool - | VernacCoFixpoint of (cofixpoint_expr * decl_notation list) list * bool + | VernacFixpoint of (fixpoint_expr * decl_notation list) list + | VernacCoFixpoint of (cofixpoint_expr * decl_notation list) list | VernacScheme of (lident option * scheme) list | VernacCombinedScheme of lident * lident list @@ -255,13 +263,13 @@ type vernac_expr = bool * (* global *) local_binder list * (* super *) typeclass_constraint * (* instance name, class name, params *) - constr_expr * (* props *) + constr_expr option * (* props *) int option (* Priority *) | VernacContext of local_binder list - | VernacDeclareInstance of - bool (* global *) * reference (* instance name *) + | VernacDeclareInstances of + bool (* global *) * reference list (* instance names *) | VernacDeclareClass of reference (* inductive or definition name *) @@ -279,13 +287,6 @@ type vernac_expr = | VernacSolve of int * raw_tactic_expr * bool | VernacSolveExistential of int * constr_expr - (* Proof Mode *) - - | VernacDeclProof - | VernacReturn - | VernacProofInstr of Decl_expr.raw_proof_instr - - (* Auxiliary file and library management *) | VernacRequireFrom of export_flag option * specif_flag option * string | VernacAddLoadPath of rec_flag * string * dir_path option @@ -309,11 +310,18 @@ type vernac_expr = | VernacDeclareTacticDefinition of (locality_flag * rec_flag * (reference * bool * raw_tactic_expr) list) | VernacCreateHintDb of locality_flag * string * bool + | VernacRemoveHints of locality_flag * string list * reference list | VernacHints of locality_flag * string list * hints_expr | VernacSyntacticDefinition of identifier located * (identifier list * constr_expr) * locality_flag * onlyparsing_flag | VernacDeclareImplicits of locality_flag * reference or_by_notation * (explicitation * bool * bool) list list + | VernacArguments of locality_flag * reference or_by_notation * + ((name * bool * (loc * string) option * bool * bool) list) list * + int * [ `SimplDontExposeCase | `SimplNeverUnfold | `Rename + | `ClearImplicits | `ClearScopes | `DefaultImplicits ] list + | VernacArgumentsScope of locality_flag * reference or_by_notation * + scope_name option list | VernacReserve of simple_binder list | VernacGeneralizable of locality_flag * (lident list) option | VernacSetOpacity of @@ -345,10 +353,13 @@ type vernac_expr = | VernacBacktrack of int*int*int | VernacFocus of int option | VernacUnfocus - | VernacGo of goable + | VernacBullet of bullet + | VernacSubproof of int option + | VernacEndSubproof | VernacShow of showable | VernacCheckGuard - | VernacProof of raw_tactic_expr + | VernacProof of raw_tactic_expr option * lident list option + | VernacProofMode of string (* Toplevel control *) | VernacToplevelControl of exn @@ -369,9 +380,6 @@ let locality_flag = ref None let local_of_bool = function true -> Local | false -> Global -let is_true = function Some (_,b) -> b | _ -> false -let is_false = function Some (_,b) -> not b | _ -> false - let check_locality () = match !locality_flag with | Some (loc,true) -> @@ -395,7 +403,7 @@ let enforce_locality_full local = error "Use only prefix \"Local\"." | None -> if local then begin - Flags.if_verbose + Flags.if_warn Pp.msg_warning (Pp.str"Obsolete syntax: use \"Local\" as a prefix."); Some true end else diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml index e6fe9a4f..10c5a00f 100644 --- a/toplevel/vernacinterp.ml +++ b/toplevel/vernacinterp.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: vernacinterp.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - open Pp open Util open Names @@ -66,7 +64,3 @@ let call (opn,converted_args) = if !Flags.debug then msgnl (str"Vernac Interpreter " ++ str !loc); raise e - -let bad_vernac_args s = - anomalylabstrm s - (str"Vernac " ++ str s ++ str" called with bad arguments") diff --git a/toplevel/vernacinterp.mli b/toplevel/vernacinterp.mli index 780e4e28..5fdc2b2c 100644 --- a/toplevel/vernacinterp.mli +++ b/toplevel/vernacinterp.mli @@ -1,18 +1,14 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: vernacinterp.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(*i*) open Tacexpr -(*i*) -(* Interpretation of extended vernac phrases. *) +(** Interpretation of extended vernac phrases. *) val disable_drop : exn -> exn diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4 index e380ae6f..aa38e9e9 100644 --- a/toplevel/whelp.ml4 +++ b/toplevel/whelp.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -8,8 +8,6 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id: whelp.ml4 14641 2011-11-06 11:59:10Z herbelin $ *) - open Flags open Pp open Util @@ -17,10 +15,9 @@ open System open Names open Term open Environ -open Rawterm +open Glob_term open Libnames open Nametab -open Termops open Detyping open Constrintern open Dischargedhypsmap @@ -41,6 +38,7 @@ open Goptions let _ = declare_string_option { optsync = false; + optdepr = false; optname = "Whelp server"; optkey = ["Whelp";"Server"]; optread = (fun () -> !whelp_server_name); @@ -49,6 +47,7 @@ let _ = let _ = declare_string_option { optsync = false; + optdepr = false; optname = "Whelp getter"; optkey = ["Whelp";"Getter"]; optread = (fun () -> !getter_server_name); @@ -94,10 +93,10 @@ let uri_of_repr_kn ref (mp,dir,l) = let url_paren f l = url_char '('; f l; url_char ')' let url_bracket f l = url_char '['; f l; url_char ']' -let whelp_of_rawsort = function - | RProp Null -> "Prop" - | RProp Pos -> "Set" - | RType _ -> "Type" +let whelp_of_glob_sort = function + | GProp Null -> "Prop" + | GProp Pos -> "Set" + | GType _ -> "Type" let uri_int n = Buffer.add_string b (string_of_int n) @@ -130,9 +129,9 @@ let uri_params f = function let get_discharged_hyp_names sp = List.map basename (get_discharged_hyps sp) let section_parameters = function - | RRef (_,(ConstructRef ((induri,_),_) | IndRef (induri,_))) -> + | GRef (_,(ConstructRef ((induri,_),_) | IndRef (induri,_))) -> get_discharged_hyp_names (path_of_global (IndRef(induri,0))) - | RRef (_,(ConstRef cst as ref)) -> + | GRef (_,(ConstRef cst as ref)) -> get_discharged_hyp_names (path_of_global ref) | _ -> [] @@ -144,33 +143,33 @@ let merge vl al = let rec uri_of_constr c = match c with - | RVar (_,id) -> url_id id - | RRef (_,ref) -> uri_of_global ref - | RHole _ | REvar _ -> url_string "?" - | RSort (_,s) -> url_string (whelp_of_rawsort s) + | GVar (_,id) -> url_id id + | GRef (_,ref) -> uri_of_global ref + | GHole _ | GEvar _ -> url_string "?" + | GSort (_,s) -> url_string (whelp_of_glob_sort s) | _ -> url_paren (fun () -> match c with - | RApp (_,f,args) -> + | GApp (_,f,args) -> let inst,rest = merge (section_parameters f) args in uri_of_constr f; url_char ' '; uri_params uri_of_constr inst; url_list_with_sep " " uri_of_constr rest - | RLambda (_,na,k,ty,c) -> + | GLambda (_,na,k,ty,c) -> url_string "\\lambda "; url_of_name na; url_string ":"; uri_of_constr ty; url_string "."; uri_of_constr c - | RProd (_,Anonymous,k,ty,c) -> + | GProd (_,Anonymous,k,ty,c) -> uri_of_constr ty; url_string "\\to "; uri_of_constr c - | RProd (_,Name id,k,ty,c) -> + | GProd (_,Name id,k,ty,c) -> url_string "\\forall "; url_id id; url_string ":"; uri_of_constr ty; url_string "."; uri_of_constr c - | RLetIn (_,na,b,c) -> + | GLetIn (_,na,b,c) -> url_string "let "; url_of_name na; url_string "\\def "; uri_of_constr b; url_string " in "; uri_of_constr c - | RCast (_,c, CastConv (_,t)) -> + | GCast (_,c, CastConv (_,t)) -> uri_of_constr c; url_string ":"; uri_of_constr t - | RRec _ | RIf _ | RLetTuple _ | RCases _ -> + | GRec _ | GIf _ | GLetTuple _ | GCases _ -> error "Whelp does not support pattern-matching and (co-)fixpoint." - | RVar _ | RRef _ | RHole _ | REvar _ | RSort _ | RCast (_,_, CastCoerce) -> + | GVar _ | GRef _ | GHole _ | GEvar _ | GSort _ | GCast (_,_, CastCoerce) -> anomaly "Written w/o parenthesis" - | RPatVar _ | RDynamic _ -> + | GPatVar _ -> anomaly "Found constructors not supported in constr") () let make_string f x = Buffer.reset b; f x; Buffer.contents b @@ -196,8 +195,9 @@ let whelp_elim ind = send_whelp "elim" (make_string uri_of_global (IndRef ind)) let on_goal f = - let gls = nth_goal_of_pftreestate 1 (get_pftreestate ()) in - f (it_mkNamedProd_or_LetIn (pf_concl gls) (pf_hyps gls)) + let { Evd.it=goals ; sigma=sigma } = Proof.V82.subgoals (get_pftreestate ()) in + let gls = { Evd.it=List.hd goals ; sigma = sigma } in + f (Termops.it_mkNamedProd_or_LetIn (pf_concl gls) (pf_hyps gls)) type whelp_request = | Locate of string diff --git a/toplevel/whelp.mli b/toplevel/whelp.mli index 75e9ad49..b0fb5491 100644 --- a/toplevel/whelp.mli +++ b/toplevel/whelp.mli @@ -1,14 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: whelp.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(* Coq interface to the Whelp query engine developed at +(** Coq interface to the Whelp query engine developed at the University of Bologna *) open Names |