From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 12 Jan 2012 16:02:20 +0100 Subject: Imported Upstream version 8.4~beta --- toplevel/auto_ind_decl.ml | 92 +++---- toplevel/auto_ind_decl.mli | 13 +- toplevel/autoinstance.ml | 21 +- toplevel/autoinstance.mli | 16 +- toplevel/cerrors.ml | 152 ++++-------- toplevel/cerrors.mli | 19 +- toplevel/class.ml | 22 +- toplevel/class.mli | 18 +- toplevel/classes.ml | 131 +++++----- toplevel/classes.mli | 46 ++-- toplevel/command.ml | 90 +++---- toplevel/command.mli | 78 +++--- toplevel/coqinit.ml | 63 ++--- toplevel/coqinit.mli | 7 +- toplevel/coqtop.ml | 114 ++++----- toplevel/coqtop.mli | 15 +- toplevel/discharge.ml | 4 +- toplevel/discharge.mli | 4 +- toplevel/himsg.ml | 285 +++++++++++++++++----- toplevel/himsg.mli | 17 +- toplevel/ide_intf.ml | 434 +++++++++++++++++++++++++++++++++ toplevel/ide_intf.mli | 87 +++++++ toplevel/ide_slave.ml | 579 +++++++++++++++++++++++++++++++++++++++++++++ toplevel/ide_slave.mli | 17 ++ toplevel/ind_tables.ml | 29 ++- toplevel/ind_tables.mli | 16 +- toplevel/indschemes.ml | 27 ++- toplevel/indschemes.mli | 26 +- toplevel/interface.mli | 87 +++++++ toplevel/lemmas.ml | 57 +++-- toplevel/lemmas.mli | 23 +- toplevel/libtypes.ml | 4 +- toplevel/libtypes.mli | 20 +- toplevel/metasyntax.ml | 132 +++++------ toplevel/metasyntax.mli | 22 +- toplevel/mltop.ml4 | 41 ++-- toplevel/mltop.mli | 34 ++- toplevel/record.ml | 110 +++++---- toplevel/record.mli | 24 +- toplevel/search.ml | 45 ++-- toplevel/search.mli | 10 +- toplevel/toplevel.ml | 70 +++--- toplevel/toplevel.mli | 28 +-- toplevel/toplevel.mllib | 2 + toplevel/usage.ml | 141 +++++------ toplevel/usage.mli | 14 +- toplevel/vernac.ml | 78 +++--- toplevel/vernac.mli | 27 +-- toplevel/vernacentries.ml | 578 ++++++++++++++++++++++++++------------------ toplevel/vernacentries.mli | 31 ++- toplevel/vernacexpr.ml | 90 +++---- toplevel/vernacinterp.ml | 8 +- toplevel/vernacinterp.mli | 8 +- toplevel/whelp.ml4 | 52 ++-- toplevel/whelp.mli | 6 +- 55 files changed, 2754 insertions(+), 1410 deletions(-) create mode 100644 toplevel/ide_intf.ml create mode 100644 toplevel/ide_intf.mli create mode 100644 toplevel/ide_slave.ml create mode 100644 toplevel/ide_slave.mli create mode 100644 toplevel/interface.mli (limited to 'toplevel') 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 *) -(* (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 *) -(* 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 *) -(* 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 *) -(* 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 *) -(* - 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 *) -(* 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 *) -(* 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 *) -(* 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 *) -(* + (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 *) -(* 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 *) -(* 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 *) -(* 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 *) -(* () (* 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 *) -(* 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 *) -(* 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 *) -(* 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 *) -(* 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 *) -(* 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 *) +(* 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 *) +(* 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 *) +(* + 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 *) +(* 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 *) -(* (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 *) -(* 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 *) -(* !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 *) -(* 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 *) +(* 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 *) -(* (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 *) -(* 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 *) -(* 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 *) -(* 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 *) -(* 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 *) -(* 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 *) -(* () (* 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 *) -(* 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 *) -(* 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 *) -(* ?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 *) -(* 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 *) -(* 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 *) -(* () -(* 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 "" "" +let emacs_prompt_startstring() = Printer.emacs_str "" -let emacs_prompt_endstring() = Printer.emacs_str (String.make 1 (Char.chr 249)) "" +let emacs_prompt_endstring() = Printer.emacs_str "" (* 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 *) -(* 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 *) -(* \n\n" let print_usage_coqc () = - print_usage "Usage: coqc 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 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 *) -(* '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 *) -(* 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 *) -(* - 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 *) -(* 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 ") - | 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 *) -(* 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 *) -(* "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 *) -(* Date: Mon, 4 Jun 2012 12:07:52 +0200 Subject: Imported Upstream version 8.4~gamma0+really8.4beta2 --- .gitignore | 3 + CHANGES | 56 +- COPYRIGHT | 2 +- CREDITS | 10 +- INSTALL | 6 +- Makefile | 2 +- Makefile.build | 14 +- Makefile.common | 17 +- Makefile.doc | 44 +- README | 6 +- TODO | 53 - checker/mod_checking.ml | 74 +- checker/subtyping.ml | 58 +- configure | 29 +- dev/base_include | 6 +- dev/printers.mllib | 2 +- dev/top_printers.ml | 4 + doc/common/macros.tex | 1 + doc/common/styles/html/coqremote/cover.html | 9 +- doc/common/styles/html/coqremote/footer.html | 45 + doc/common/styles/html/coqremote/header.html | 49 + doc/common/styles/html/simple/cover.html | 10 +- doc/common/styles/html/simple/footer.html | 2 + doc/common/styles/html/simple/header.html | 13 + doc/common/title.tex | 2 +- doc/faq/FAQ.tex | 6 +- doc/refman/Cases.tex | 2 +- doc/refman/RefMan-cic.tex | 77 +- doc/refman/RefMan-coi.tex | 4 +- doc/refman/RefMan-com.tex | 176 +- doc/refman/RefMan-ext.tex | 41 +- doc/refman/RefMan-gal.tex | 4 +- doc/refman/RefMan-ltac.tex | 3 +- doc/refman/RefMan-oth.tex | 138 +- doc/refman/RefMan-pro.tex | 79 +- doc/refman/RefMan-sch.tex | 418 ++ doc/refman/RefMan-syn.tex | 2 +- doc/refman/RefMan-tac.tex | 6168 ++++++++++++------------ doc/refman/RefMan-tacex.tex | 584 --- doc/refman/RefMan-uti.tex | 52 +- doc/refman/Reference-Manual.tex | 7 +- doc/refman/coqdoc.tex | 12 +- doc/stdlib/hidden-files | 0 doc/stdlib/index-list.html.template | 36 +- doc/stdlib/index-trailer.html | 2 - doc/stdlib/make-library-index | 34 +- ide/command_windows.ml | 24 +- ide/command_windows.mli | 2 + ide/coq.ml | 120 +- ide/coq.mli | 14 +- ide/coq_commands.ml | 1 - ide/coq_lex.mll | 28 +- ide/coqide-gtk2rc | 10 - ide/coqide.ml | 231 +- ide/coqide.mli | 3 - ide/coqide_main.ml4 | 24 +- ide/coqide_ui.ml | 28 +- ide/ideproof.ml | 16 +- ide/ideutils.ml | 99 +- ide/ideutils.mli | 13 + ide/minilib.ml | 47 +- ide/preferences.ml | 210 +- ide/preferences.mli | 21 +- ide/tags.ml | 33 +- ide/tags.mli | 50 + ide/utils/configwin.ml | 4 +- ide/utils/configwin_ihm.ml | 6 +- interp/constrextern.ml | 50 +- interp/constrextern.mli | 1 + interp/constrintern.ml | 70 +- interp/constrintern.mli | 3 + interp/genarg.ml | 42 +- interp/genarg.mli | 6 +- interp/notation.ml | 5 + interp/notation.mli | 2 + interp/topconstr.ml | 15 +- interp/topconstr.mli | 4 + kernel/declarations.mli | 4 + kernel/mod_typing.ml | 82 +- kernel/safe_typing.ml | 56 +- kernel/safe_typing.mli | 2 +- kernel/subtyping.ml | 74 +- kernel/term.ml | 1 + kernel/term.mli | 6 +- kernel/univ.ml | 111 +- kernel/univ.mli | 4 + lib/envars.ml | 6 +- lib/explore.ml | 18 +- lib/explore.mli | 2 +- lib/pp.ml4 | 19 +- lib/pp.mli | 3 + lib/util.ml | 25 +- lib/util.mli | 6 + lib/xml_parser.mli | 2 +- library/assumptions.ml | 18 +- library/declare.ml | 2 +- library/global.ml | 2 +- library/global.mli | 2 +- library/goptions.ml | 1 + library/impargs.ml | 13 +- library/lib.ml | 111 +- library/lib.mli | 43 +- man/coqc.1 | 12 + man/coqtop.1 | 8 +- myocamlbuild.ml | 9 + parsing/argextend.ml4 | 74 +- parsing/egrammar.ml | 41 +- parsing/egrammar.mli | 2 + parsing/extrawit.ml | 12 +- parsing/g_constr.ml4 | 24 +- parsing/g_proofs.ml4 | 21 +- parsing/g_tactic.ml4 | 27 +- parsing/g_vernac.ml4 | 4 +- parsing/ppconstr.ml | 72 +- parsing/ppconstr.mli | 6 +- parsing/pptactic.ml | 30 +- parsing/ppvernac.ml | 76 +- parsing/printer.ml | 37 +- parsing/printer.mli | 3 +- parsing/q_coqast.ml4 | 15 +- parsing/tacextend.ml4 | 61 +- plugins/decl_mode/g_decl_mode.ml4 | 5 +- plugins/dp/Dp.v | 118 - plugins/dp/TODO | 24 - plugins/dp/dp.ml | 1133 ----- plugins/dp/dp.mli | 20 - plugins/dp/dp_plugin.mllib | 5 - plugins/dp/dp_why.ml | 185 - plugins/dp/dp_why.mli | 17 - plugins/dp/dp_zenon.mli | 7 - plugins/dp/dp_zenon.mll | 189 - plugins/dp/fol.mli | 58 - plugins/dp/g_dp.ml4 | 77 - plugins/dp/test2.v | 80 - plugins/dp/tests.v | 300 -- plugins/dp/vo.itarget | 1 - plugins/dp/zenon.v | 92 - plugins/extraction/extract_env.ml | 11 +- plugins/extraction/modutil.ml | 11 +- plugins/firstorder/g_ground.ml4 | 2 - plugins/funind/functional_principles_proofs.ml | 3 +- plugins/funind/g_indfun.ml4 | 2 +- plugins/funind/invfun.ml | 55 +- plugins/funind/recdef.ml | 42 +- plugins/micromega/coq_micromega.ml | 19 +- plugins/nsatz/nsatz.ml4 | 2 +- plugins/pluginsbyte.itarget | 1 - plugins/pluginsdyn.itarget | 1 - plugins/pluginsopt.itarget | 1 - plugins/pluginsvo.itarget | 3 +- plugins/rtauto/proof_search.ml | 4 +- plugins/rtauto/proof_search.mli | 2 +- plugins/subtac/eterm.ml | 17 +- plugins/subtac/g_subtac.ml4 | 4 +- plugins/subtac/subtac.ml | 4 +- plugins/subtac/subtac_cases.ml | 2 +- plugins/subtac/subtac_classes.ml | 9 +- plugins/subtac/subtac_coercion.ml | 107 +- plugins/subtac/subtac_command.ml | 2 +- plugins/subtac/subtac_obligations.ml | 25 +- plugins/subtac/subtac_pretyping.ml | 4 +- plugins/subtac/subtac_pretyping_F.ml | 33 +- plugins/subtac/subtac_utils.ml | 11 +- plugins/subtac/subtac_utils.mli | 1 + plugins/xml/dumptree.ml4 | 4 +- pretyping/cases.ml | 5 +- pretyping/coercion.ml | 2 +- pretyping/detyping.ml | 8 +- pretyping/evarconv.ml | 119 +- pretyping/evarutil.ml | 1503 +++--- pretyping/evarutil.mli | 6 +- pretyping/evd.ml | 10 +- pretyping/evd.mli | 2 + pretyping/inductiveops.ml | 19 +- pretyping/namegen.ml | 47 +- pretyping/namegen.mli | 5 +- pretyping/pretyping.ml | 9 +- pretyping/pretyping.mli | 3 +- pretyping/tacred.ml | 12 +- pretyping/typeclasses.ml | 34 +- pretyping/typeclasses.mli | 12 +- pretyping/unification.ml | 2 +- pretyping/vnorm.ml | 9 +- proofs/clenv.ml | 4 +- proofs/evar_refiner.ml | 2 +- proofs/goal.ml | 6 +- proofs/goal.mli | 4 +- proofs/logic.ml | 8 +- proofs/pfedit.ml | 14 +- proofs/pfedit.mli | 22 +- proofs/proof.ml | 134 +- proofs/proof.mli | 14 +- proofs/proof_global.ml | 72 +- proofs/proof_global.mli | 6 - proofs/proofview.ml | 11 + proofs/proofview.mli | 5 + proofs/refiner.ml | 4 - proofs/refiner.mli | 1 - proofs/tacexpr.ml | 11 +- proofs/tacmach.ml | 8 - proofs/tacmach.mli | 3 - proofs/tactic_debug.ml | 103 +- proofs/tactic_debug.mli | 7 + scripts/coqc.ml | 23 +- tactics/auto.ml | 417 +- tactics/auto.mli | 54 +- tactics/class_tactics.ml4 | 37 +- tactics/dhyp.ml | 359 -- tactics/dhyp.mli | 28 - tactics/eauto.ml4 | 146 +- tactics/eauto.mli | 4 +- tactics/extraargs.ml4 | 35 +- tactics/extraargs.mli | 2 + tactics/extratactics.ml4 | 18 +- tactics/refine.ml | 2 +- tactics/rewrite.ml4 | 22 +- tactics/tacinterp.ml | 605 ++- tactics/tacinterp.mli | 14 +- tactics/tacticals.ml | 1 - tactics/tacticals.mli | 1 - tactics/tactics.ml | 10 +- tactics/tactics.mllib | 1 - test-suite/bugs/closed/shouldsucceed/2603.v | 21 +- test-suite/bugs/closed/shouldsucceed/2732.v | 19 + test-suite/bugs/closed/shouldsucceed/2733.v | 26 + test-suite/complexity/autodecomp.v | 11 - test-suite/output/Arguments.out | 8 + test-suite/output/Arguments.v | 12 + test-suite/output/Notations2.out | 6 + test-suite/output/Notations2.v | 15 + test-suite/output/PrintInfos.out | 9 +- test-suite/success/Cases.v | 71 +- test-suite/success/CasesDep.v | 22 +- test-suite/success/Hints.v | 5 - test-suite/success/Mod_params.v | 84 +- test-suite/success/Notations.v | 14 +- test-suite/success/RecTutorial.v | 69 +- test-suite/success/Reset.v | 7 - test-suite/success/apply.v | 17 +- test-suite/success/coercions.v | 42 + test-suite/success/dependentind.v | 31 + test-suite/success/evars.v | 70 + test-suite/success/hyps_inclusion.v | 8 +- test-suite/success/telescope_canonical.v | 70 +- theories/Arith/Div2.v | 26 +- theories/Init/Logic.v | 4 +- theories/Init/Prelude.v | 1 - theories/Init/Specif.v | 2 +- theories/Lists/intro.tex | 2 +- theories/Logic/ChoiceFacts.v | 16 +- theories/MSets/MSetAVL.v | 1377 +----- theories/MSets/MSetGenTree.v | 1145 +++++ theories/MSets/MSetRBT.v | 1931 ++++++++ theories/MSets/vo.itarget | 2 + theories/Program/Equality.v | 26 +- theories/Unicode/Utf8_core.v | 4 +- theories/Vectors/Fin.v | 10 +- theories/Vectors/VectorDef.v | 23 +- theories/Vectors/VectorSpec.v | 6 + theories/Wellfounded/Lexicographic_Product.v | 14 +- theories/ZArith/Int.v | 128 +- theories/ZArith/ZOdiv.v | 88 + theories/ZArith/ZOdiv_def.v | 15 + theories/ZArith/Zeven.v | 6 +- theories/ZArith/vo.itarget | 2 + tools/coq_makefile.ml | 26 +- tools/coqdoc/cpretty.mll | 20 +- tools/coqdoc/index.ml | 6 +- tools/coqdoc/output.ml | 8 +- tools/win32hack.mllib | 1 + tools/win32hack_filename.ml | 4 + toplevel/backtrack.ml | 225 + toplevel/backtrack.mli | 93 + toplevel/class.ml | 2 +- toplevel/classes.ml | 9 +- toplevel/command.ml | 36 +- toplevel/coqtop.ml | 11 +- toplevel/himsg.ml | 16 +- toplevel/ide_intf.ml | 120 +- toplevel/ide_intf.mli | 26 + toplevel/ide_slave.ml | 436 +- toplevel/interface.mli | 47 +- toplevel/metasyntax.ml | 12 + toplevel/metasyntax.mli | 2 + toplevel/mltop.ml4 | 23 +- toplevel/mltop.mli | 10 + toplevel/record.ml | 6 +- toplevel/search.mli | 2 + toplevel/toplevel.ml | 3 - toplevel/toplevel.mllib | 1 + toplevel/vernac.ml | 65 +- toplevel/vernac.mli | 9 +- toplevel/vernacentries.ml | 198 +- toplevel/vernacentries.mli | 31 +- toplevel/vernacexpr.ml | 28 +- 295 files changed, 12968 insertions(+), 11382 deletions(-) delete mode 100644 TODO create mode 100644 doc/common/styles/html/coqremote/footer.html create mode 100644 doc/common/styles/html/coqremote/header.html create mode 100644 doc/common/styles/html/simple/footer.html create mode 100644 doc/common/styles/html/simple/header.html create mode 100644 doc/refman/RefMan-sch.tex create mode 100644 doc/stdlib/hidden-files delete mode 100644 doc/stdlib/index-trailer.html create mode 100644 ide/tags.mli delete mode 100644 plugins/dp/Dp.v delete mode 100644 plugins/dp/TODO delete mode 100644 plugins/dp/dp.ml delete mode 100644 plugins/dp/dp.mli delete mode 100644 plugins/dp/dp_plugin.mllib delete mode 100644 plugins/dp/dp_why.ml delete mode 100644 plugins/dp/dp_why.mli delete mode 100644 plugins/dp/dp_zenon.mli delete mode 100644 plugins/dp/dp_zenon.mll delete mode 100644 plugins/dp/fol.mli delete mode 100644 plugins/dp/g_dp.ml4 delete mode 100644 plugins/dp/test2.v delete mode 100644 plugins/dp/tests.v delete mode 100644 plugins/dp/vo.itarget delete mode 100644 plugins/dp/zenon.v delete mode 100644 tactics/dhyp.ml delete mode 100644 tactics/dhyp.mli create mode 100644 test-suite/bugs/closed/shouldsucceed/2732.v create mode 100644 test-suite/bugs/closed/shouldsucceed/2733.v delete mode 100644 test-suite/complexity/autodecomp.v delete mode 100644 test-suite/success/Reset.v create mode 100644 theories/MSets/MSetGenTree.v create mode 100644 theories/MSets/MSetRBT.v create mode 100644 theories/ZArith/ZOdiv.v create mode 100644 theories/ZArith/ZOdiv_def.v create mode 100644 tools/win32hack.mllib create mode 100644 tools/win32hack_filename.ml create mode 100644 toplevel/backtrack.ml create mode 100644 toplevel/backtrack.mli (limited to 'toplevel') diff --git a/.gitignore b/.gitignore index 7fcd2580..32a40af6 100644 --- a/.gitignore +++ b/.gitignore @@ -79,6 +79,9 @@ doc/stdlib/Library.out doc/stdlib/Library.pdf doc/stdlib/Library.ps doc/stdlib/Library.coqdoc.tex +doc/stdlib/FullLibrary.pdf +doc/stdlib/FullLibrary.ps +doc/stdlib/FullLibrary.coqdoc.tex doc/stdlib/html/ doc/stdlib/index-body.html doc/stdlib/index-list.html diff --git a/CHANGES b/CHANGES index 74aefe49..c245fb25 100644 --- a/CHANGES +++ b/CHANGES @@ -1,5 +1,54 @@ -Changes from V8.3 to V8.4 -========================= +Changes from V8.4beta to V8.4 +============================= + +Vernacular commands + +- Undo and UndoTo are now handling the proof states. They may + perform some extra steps of backtrack to avoid states where + the proof state is unavailable (typically a closed proof). +- The commands Suspend and Resume have been removed. +- A basic Show Script has been reintroduced (no indentation). +- New command "Set Parsing Explicit" for deactivating parsing (and printing) + of implicit arguments (useful for teaching). +- New command "Grab Existential Variables" to transform the unresolved evars at + the end of a proof into goals. + +Tactics + +- Still no general "info" tactical, but new specific tactics + info_auto, info_eauto, info_trivial which provides information + on the proofs found by auto/eauto/trivial. Display of these + details could also be activated by Set Info Auto/Eauto/Trivial. +- Details on everything tried by auto/eauto/trivial during + a proof search could be obtained by "debug auto", "debug eauto", + "debug trivial" or by a global "Set Debug Auto/Eauto/Trivial". +- New command "r string" that interprets "idtac string" as a breakpoint + and jumps to its next use in Ltac debugger. +- Tactics from the Dp plugin (simplify, ergo, yices, cvc3, z3, cvcl, + harvey, zenon, gwhy) have been removed, since Why2 has not been + maintained for the last few years. The Why3 plugin should be a suitable + replacement in most cases. + +Libraries + +- MSetRBT : a new implementation of MSets via Red-Black trees (initial + contribution by Andrew Appel). +- MSetAVL : for maximal sharing with the new MSetRBT, the argument order + of Node has changed (this should be transparent to regular MSets users). + +Module System + +- The names of modules (and module types) are now in a fully separated + namespace from ordinary definitions : "Definition E:=0. Module E. End E." + is now accepted. + +CoqIDE + +- Coqide now supports the Restart command, and Undo (with a warning). + Better support for Abort. + +Changes from V8.3 to V8.4beta +============================= Logic @@ -69,6 +118,8 @@ Tactics - When applying destruct or inversion on a fixpoint hiding an inductive type, recursive calls to the fixpoint now remain folded by default (rare source of incompatibility generally solvable by adding a call to simpl). +- The behavior of the simpl tactic can be tuned using the new "Arguments" + vernacular. Vernacular commands @@ -90,6 +141,7 @@ Vernacular commands to avoid conversion at Qed time to go into a very long computation. - New command "Show Goal ident" to display the statement of a goal, even a closed one (available from Proof General). +- New command "Arguments" subsuming "Implicit Arguments" and "Arguments Scope". Module System diff --git a/COPYRIGHT b/COPYRIGHT index 8d81d8c4..3aa6aae9 100644 --- a/COPYRIGHT +++ b/COPYRIGHT @@ -1,6 +1,6 @@ The Coq proof assistant -Copyright 1999-2010 The Coq development team, INRIA, CNRS, University +Copyright 1999-2012 The Coq development team, INRIA, CNRS, University Paris Sud, University Paris 7, Ecole Polytechnique. This product includes also software developed by diff --git a/CREDITS b/CREDITS index 53bd9e93..543cb3f3 100644 --- a/CREDITS +++ b/CREDITS @@ -106,6 +106,7 @@ The following people have contributed to the development of different versions of the Coq Proof assistant during the indicated time: Bruno Barras (INRIA, 1995-now) + Pierre Boutillier (INRIA-PPS, 2010-now) Jacek Chrzaszcz (LRI, 1998-2003) Thierry Coquand (INRIA, 1985-1989) Pierre Corbineau (LRI, 2003-2005, Nijmegen, 2005-2008, Grenoble 1, 2008-now) @@ -118,10 +119,12 @@ of the Coq Proof assistant during the indicated time: Amy Felty (INRIA, 1993) Jean-Christophe Filliâtre (ENS Lyon, 1994-1997, LRI, 1997-now) Eduardo Giménez (ENS Lyon, 1993-1996, INRIA, 1997-1998) + Stéphane Glondu (INRIA-PPS, 2007-now) Benjamin Grégoire (INRIA, 2003-now) Hugo Herbelin (INRIA, 1996-now) Gérard Huet (INRIA, 1985-1997) - Pierre Letouzey (LRI, 2000-2004 & PPS, 2005-now) + Pierre Letouzey (LRI, 2000-2004, PPS, 2005-2008, INRIA-PPS, 2009-now) + Patrick Loiseleur (Paris Sud, 1997-1999) Evgeny Makarov (INRIA, 2007) Pascal Manoury (INRIA, 1993) Micaela Mayero (INRIA, 1997-2002) @@ -132,9 +135,11 @@ of the Coq Proof assistant during the indicated time: Julien Narboux (INRIA, 2005-2006, Strasbourg, 2007-now) Jean-Marc Notin (CNRS, 2006-now) Catherine Parent-Vigouroux (ENS Lyon, 1992-1995) - Patrick Loiseleur (Paris Sud, 1997-1999) Christine Paulin-Mohring (INRIA, 1985-1989, ENS Lyon, 1989-1997, LRI, 1997-now) + Pierre-Marie Pédrot (INRIA-PPS, 2011-now) + Matthias Puech (INRIA-Bologna, 2008-now) + Yann Régis-Gianas (INRIA-PPS, 2009-now) Clément Renard (INRIA, 2001-2004) Claudio Sacerdoti Coen (INRIA, 2004-2005) Amokrane Saïbi (INRIA, 1993-1998) @@ -142,6 +147,7 @@ of the Coq Proof assistant during the indicated time: Élie Soubiran (INRIA, 2007-now) Matthieu Sozeau (INRIA, 2005-now) Arnaud Spiwack (INRIA, 2006-now) + Enrico Tassi (INRIA, 2011-now) Benjamin Werner (INRIA, 1989-1994) *************************************************************************** diff --git a/INSTALL b/INSTALL index e88dc319..5ee00613 100644 --- a/INSTALL +++ b/INSTALL @@ -39,9 +39,9 @@ WHAT DO YOU NEED ? urpmi coq - Should you need or prefer to compile Coq V8.2 yourself, you need: + Should you need or prefer to compile Coq V8.4 yourself, you need: - - Objective Caml version 3.10.0 or later + - Objective Caml version 3.11.2 or later (available at http://caml.inria.fr/) - Camlp5 (version <= 4.08, or 5.* transitional) @@ -87,7 +87,7 @@ QUICK INSTALLATION PROCEDURE. INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). ================================================= -1- Check that you have the Objective Caml compiler version 3.10.0 (or later) +1- Check that you have the Objective Caml compiler version 3.11.2 (or later) installed on your computer and that "ocamlmktop" and "ocamlc" (or its native code version "ocamlc.opt") lie in a directory which is present in your $PATH environment variable. diff --git a/Makefile b/Makefile index 876ac583..0ff72856 100644 --- a/Makefile +++ b/Makefile @@ -191,6 +191,7 @@ docclean: rm -f doc/common/version.tex rm -f doc/refman/styles.hva doc/refman/cover.html doc/refman/Reference-Manual.html rm -f doc/coq.tex + rm -f doc/refman/styles.hva doc/refman/cover.html archclean: clean-ide optclean voclean rm -rf _build myocamlbuild_config.ml @@ -221,7 +222,6 @@ cleanconfig: rm -f config/Makefile config/coq_config.ml dev/ocamldebug-v7 ide/undo.mli distclean: clean cleanconfig - $(MAKE) -C test-suite distclean voclean: rm -f states/*.coq diff --git a/Makefile.build b/Makefile.build index 59ee457c..41dfabbf 100644 --- a/Makefile.build +++ b/Makefile.build @@ -318,7 +318,7 @@ $(COQIDEOPT): $(LINKIDEOPT) | $(COQTOPOPT) $(STRIP) $@ $(COQIDEBYTE): $(LINKIDE) | $(COQTOPBYTE) - $(SHOW)'OCAMLOPT -o $@' + $(SHOW)'OCAMLC -o $@' $(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -o $@ unix.cma threads.cma lablgtk.cma gtkThread.cmo\ str.cma $(COQRUNBYTEFLAGS) $(LINKIDE) @@ -446,7 +446,7 @@ noreal: logic arith bool zarith qarith lists sets fsets relations \ # 3) plugins ########################################################################### -.PHONY: plugins omega micromega ring setoid_ring nsatz dp xml extraction +.PHONY: plugins omega micromega ring setoid_ring nsatz xml extraction .PHONY: field fourier funind cc subtac rtauto pluginsopt plugins: $(PLUGINSVO) @@ -455,7 +455,6 @@ micromega: $(MICROMEGAVO) $(MICROMEGACMA) $(CSDPCERT) ring: $(RINGVO) $(RINGCMA) setoid_ring: $(NEWRINGVO) $(NEWRINGCMA) nsatz: $(NSATZVO) $(NSATZCMA) -dp: $(DPCMA) xml: $(XMLVO) $(XMLCMA) extraction: $(EXTRACTIONCMA) field: $(FIELDVO) $(FIELDCMA) @@ -623,7 +622,7 @@ INSTALLCMI = $(sort \ install-library: $(MKDIR) $(FULLCOQLIB) - $(INSTALLSH) $(FULLCOQLIB) $(LIBFILES) $(PLUGINS) $(PLUGINSOPT) + $(INSTALLSH) $(FULLCOQLIB) $(LIBFILES) $(PLUGINS) $(MKDIR) $(FULLCOQLIB)/states $(INSTALLLIB) states/*.coq $(FULLCOQLIB)/states $(MKDIR) $(FULLCOQLIB)/user-contrib @@ -632,7 +631,7 @@ install-library: $(INSTALLSH) $(FULLCOQLIB) $(INSTALLCMI) ifeq ($(BEST),opt) $(INSTALLLIB) $(LIBCOQRUN) $(FULLCOQLIB) - $(INSTALLSH) $(FULLCOQLIB) $(CONFIG:.cmo=.cmx) $(CONFIG:.cmo=.o) $(LINKCMO:.cma=.cmxa) $(LINKCMO:.cma=.a) + $(INSTALLSH) $(FULLCOQLIB) $(CONFIG:.cmo=.cmx) $(CONFIG:.cmo=.o) $(LINKCMO:.cma=.cmxa) $(LINKCMO:.cma=.a) $(PLUGINSOPT) endif # csdpcert is not meant to be directly called by the user; we install # it with libraries @@ -643,11 +642,14 @@ endif install-library-light: $(MKDIR) $(FULLCOQLIB) - $(INSTALLSH) $(FULLCOQLIB) $(LIBFILESLIGHT) $(INITPLUGINS) $(INITPLUGINSOPT) + $(INSTALLSH) $(FULLCOQLIB) $(LIBFILESLIGHT) $(INITPLUGINS) $(MKDIR) $(FULLCOQLIB)/states $(INSTALLLIB) states/*.coq $(FULLCOQLIB)/states rm -f $(FULLCOQLIB)/revision -$(INSTALLLIB) revision $(FULLCOQLIB) +ifeq ($(BEST),opt) + $(INSTALLSH) $(FULLCOQLIB) $(INITPLUGINSOPT) +endif install-coq-info: install-coq-manpages install-emacs install-latex diff --git a/Makefile.common b/Makefile.common index b560bae5..3740b52e 100644 --- a/Makefile.common +++ b/Makefile.common @@ -79,7 +79,7 @@ SRCDIRS:=\ pretyping interp toplevel/utils toplevel parsing \ ide/utils ide \ $(addprefix plugins/, \ - omega romega micromega quote ring dp \ + omega romega micromega quote ring \ setoid_ring xml extraction fourier \ cc funind firstorder field subtac \ rtauto nsatz syntax decl_mode) @@ -125,14 +125,15 @@ REFMANCOQTEXFILES:=$(addprefix doc/refman/, \ RefMan-cic.v.tex RefMan-lib.v.tex \ RefMan-tacex.v.tex RefMan-syn.v.tex \ RefMan-oth.v.tex RefMan-ltac.v.tex \ - RefMan-decl.v.tex \ + RefMan-decl.v.tex RefMan-sch.v.tex \ + RefMan-pro.v.tex \ Cases.v.tex Coercion.v.tex Extraction.v.tex \ Program.v.tex Omega.v.tex Micromega.v.tex Polynom.v.tex Nsatz.v.tex \ Setoid.v.tex Helm.tex Classes.v.tex ) REFMANTEXFILES:=$(addprefix doc/refman/, \ headers.sty Reference-Manual.tex \ - RefMan-pre.tex RefMan-int.tex RefMan-pro.tex RefMan-com.tex \ + RefMan-pre.tex RefMan-int.tex RefMan-com.tex \ RefMan-uti.tex RefMan-ide.tex RefMan-add.tex RefMan-modr.tex ) \ $(REFMANCOQTEXFILES) \ @@ -176,7 +177,6 @@ QUOTECMA:=plugins/quote/quote_plugin.cma RINGCMA:=plugins/ring/ring_plugin.cma NEWRINGCMA:=plugins/setoid_ring/newring_plugin.cma NSATZCMA:=plugins/nsatz/nsatz_plugin.cma -DPCMA:=plugins/dp/dp_plugin.cma FIELDCMA:=plugins/field/field_plugin.cma XMLCMA:=plugins/xml/xml_plugin.cma FOURIERCMA:=plugins/fourier/fourier_plugin.cma @@ -196,14 +196,14 @@ OTHERSYNTAXCMA:=$(addprefix plugins/syntax/, \ DECLMODECMA:=plugins/decl_mode/decl_mode_plugin.cma PLUGINSCMA:=$(OMEGACMA) $(ROMEGACMA) $(MICROMEGACMA) $(DECLMODECMA) \ - $(QUOTECMA) $(RINGCMA) $(NEWRINGCMA) $(DPCMA) $(FIELDCMA) \ + $(QUOTECMA) $(RINGCMA) $(NEWRINGCMA) $(FIELDCMA) \ $(FOURIERCMA) $(EXTRACTIONCMA) $(XMLCMA) \ $(CCCMA) $(FOCMA) $(SUBTACCMA) $(RTAUTOCMA) \ $(FUNINDCMA) $(NSATZCMA) $(NATSYNTAXCMA) $(OTHERSYNTAXCMA) ifneq ($(HASNATDYNLINK),false) STATICPLUGINS:= - INITPLUGINS:=$(EXTRACTIONCMA) $(FOCMA) $(CCCMA) $(DPCMA) \ + INITPLUGINS:=$(EXTRACTIONCMA) $(FOCMA) $(CCCMA) \ $(XMLCMA) $(FUNINDCMA) $(SUBTACCMA) $(NATSYNTAXCMA) INITPLUGINSOPT:=$(INITPLUGINS:.cma=.cmxs) PLUGINS:=$(PLUGINSCMA) @@ -314,7 +314,6 @@ NEWRINGVO:=$(call cat_vo_itarget, plugins/setoid_ring) NSATZVO:=$(call cat_vo_itarget, plugins/nsatz) FOURIERVO:=$(call cat_vo_itarget, plugins/fourier) FUNINDVO:=$(call cat_vo_itarget, plugins/funind) -DPVO:=$(call cat_vo_itarget, plugins/dp) RTAUTOVO:=$(call cat_vo_itarget, plugins/rtauto) EXTRACTIONVO:=$(call cat_vo_itarget, plugins/extraction) XMLVO:= @@ -322,7 +321,7 @@ CCVO:= PLUGINSVO:= $(OMEGAVO) $(ROMEGAVO) $(MICROMEGAVO) $(RINGVO) $(FIELDVO) \ $(XMLVO) $(FOURIERVO) $(CCVO) $(FUNINDVO) \ - $(RTAUTOVO) $(NEWRINGVO) $(DPVO) $(QUOTEVO) \ + $(RTAUTOVO) $(NEWRINGVO) $(QUOTEVO) \ $(NSATZVO) $(EXTRACTIONVO) ALLVO:= $(THEORIESVO) $(PLUGINSVO) @@ -347,8 +346,6 @@ MANPAGES:=man/coq-tex.1 man/coqdep.1 man/gallina.1 \ man/coqwc.1 man/coqdoc.1 man/coqide.1 \ man/coq_makefile.1 man/coqmktop.1 man/coqchk.1 -DATE=$(shell LANG=C date +"%B %Y") - ########################################################################### # Source documentation ########################################################################### diff --git a/Makefile.doc b/Makefile.doc index 59eb2fe8..685887f5 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -12,7 +12,7 @@ ###################################################################### .PHONY: doc doc-html doc-pdf doc-ps refman refman-quick tutorial -.PHONY: stdlib full-stdlib faq rectutorial +.PHONY: stdlib full-stdlib faq rectutorial refman-html-dir INDEXURLS:=doc/refman/html/index_urls.txt @@ -126,14 +126,16 @@ doc/refman/styles.hva: doc/common/styles/html/$(HTMLSTYLE)/styles.hva INDEXES:= doc/refman/html/command-index.html doc/refman/html/tactic-index.html ALLINDEXES:= doc/refman/html/index.html $(INDEXES) -$(ALLINDEXES): doc/refman/Reference-Manual.html $(REFMANPNGFILES) \ +$(ALLINDEXES): refman-html-dir + +refman-html-dir: doc/refman/Reference-Manual.html $(REFMANPNGFILES) \ doc/refman/cover.html doc/refman/styles.hva doc/refman/index.html - rm -rf doc/refman/html $(MKDIR) doc/refman/html $(INSTALLLIB) $(REFMANPNGFILES) doc/refman/html (cd doc/refman/html; hacha -nolinks -tocbis -o toc.html ../styles.hva ../Reference-Manual.html) $(INSTALLLIB) doc/refman/cover.html doc/refman/html/index.html - $(INSTALLLIB) doc/common/styles/html/$(HTMLSTYLE)/*.css doc/refman/html + -$(INSTALLLIB) doc/common/styles/html/$(HTMLSTYLE)/*.css doc/refman/html refman-quick: (cd doc/refman;\ @@ -200,40 +202,32 @@ doc/faq/html/index.html: doc/faq/FAQ.v.html ### Standard library (browsable html format) ifdef QUICK -doc/stdlib/index-body.html: - - rm -rf doc/stdlib/html - $(MKDIR) doc/stdlib/html - $(COQDOC) -q -boot -d doc/stdlib/html --multi-index --html -g --utf8 \ - -R theories Coq $(THEORIESVO:.vo=.v) - mv doc/stdlib/html/index.html doc/stdlib/index-body.html +doc/stdlib/html/genindex.html: else -doc/stdlib/index-body.html: $(COQDOC) $(THEORIESVO) +doc/stdlib/html/genindex.html: | $(COQDOC) $(THEORIESVO) +endif - rm -rf doc/stdlib/html $(MKDIR) doc/stdlib/html - $(COQDOC) -q -boot -d doc/stdlib/html --multi-index --html -g --utf8 \ + $(COQDOC) -q -d doc/stdlib/html --with-header doc/common/styles/html/$(HTMLSTYLE)/header.html --with-footer doc/common/styles/html/$(HTMLSTYLE)/footer.html --multi-index --html -g \ -R theories Coq $(THEORIESVO:.vo=.v) - mv doc/stdlib/html/index.html doc/stdlib/index-body.html -endif + mv doc/stdlib/html/index.html doc/stdlib/html/genindex.html doc/stdlib/index-list.html: doc/stdlib/index-list.html.template doc/stdlib/make-library-index - ./doc/stdlib/make-library-index doc/stdlib/index-list.html + ./doc/stdlib/make-library-index doc/stdlib/index-list.html doc/stdlib/hidden-files -doc/stdlib/html/index.html: doc/stdlib/index-list.html doc/stdlib/index-body.html doc/stdlib/index-trailer.html - cat doc/stdlib/index-list.html > $@ - sed -n -e '//,/<\/table>/p' doc/stdlib/index-body.html >> $@ - cat doc/stdlib/index-trailer.html >> $@ +doc/stdlib/html/index.html: doc/stdlib/html/genindex.html doc/stdlib/index-list.html + cat doc/common/styles/html/$(HTMLSTYLE)/header.html doc/stdlib/index-list.html > $@ + cat doc/common/styles/html/$(HTMLSTYLE)/footer.html >> $@ ### Standard library (light version, full version is definitely too big) ifdef QUICK doc/stdlib/Library.coqdoc.tex: - $(COQDOC) -q -boot --gallina --body-only --latex --stdout --utf8 \ - -R theories Coq $(THEORIESLIGHTVO:.vo=.v) > $@ else -doc/stdlib/Library.coqdoc.tex: $(COQDOC) $(THEORIESLIGHTVO) - $(COQDOC) -q -boot --gallina --body-only --latex --stdout --utf8 \ - -R theories Coq $(THEORIESLIGHTVO:.vo=.v) > $@ +doc/stdlib/Library.coqdoc.tex: | $(COQDOC) $(THEORIESLIGHTVO) endif + $(COQDOC) -q -boot --gallina --body-only --latex --stdout \ + -R theories Coq $(THEORIESLIGHTVO:.vo=.v) >> $@ doc/stdlib/Library.dvi: $(DOCCOMMON) doc/stdlib/Library.coqdoc.tex doc/stdlib/Library.tex (cd doc/stdlib;\ @@ -255,12 +249,12 @@ ifdef QUICK doc/stdlib/FullLibrary.coqdoc.tex: $(COQDOC) -q -boot --gallina --body-only --latex --stdout --utf8 \ -R theories Coq $(THEORIESVO:.vo=.v) > $@ - sed -i "" -e 's///g' $@ + sed -i.tmp -e 's///g' $@ && rm $@.tmp else doc/stdlib/FullLibrary.coqdoc.tex: $(COQDOC) $(THEORIESVO) $(COQDOC) -q -boot --gallina --body-only --latex --stdout --utf8 \ -R theories Coq $(THEORIESVO:.vo=.v) > $@ - sed -i "" -e 's///g' $@ + sed -i.tmp -e 's///g' $@ && rm $@.tmp endif doc/stdlib/FullLibrary.dvi: $(DOCCOMMON) doc/stdlib/FullLibrary.coqdoc.tex doc/stdlib/FullLibrary.tex diff --git a/README b/README index 4f4afa5b..9bf63c43 100644 --- a/README +++ b/README @@ -38,7 +38,7 @@ THE COQ CLUB. discuss questions about the Coq system and related topics. The submission address is: - coq-club@coq.inria.fr + coq-club@inria.fr The topics to be discussed in the club should include: @@ -55,7 +55,7 @@ THE COQ CLUB. To be added to, or removed from, the mailing list, please write to: - coq-club-request@coq.inria.fr + coq-club-request@inria.fr Please use also this address for any questions/suggestions about the Coq Club. It might sometimes take a few days before your messages get @@ -67,7 +67,7 @@ BUGS REPORT. Send your bug reports by filling a form at - http://logical.saclay.inria.fr/coq-bugs + http://coq.inria.fr/bugs To be effective, bug reports should mention the Caml version used to compile and run Coq, the Coq version (coqtop -v), the configuration diff --git a/TODO b/TODO deleted file mode 100644 index d6891e5f..00000000 --- a/TODO +++ /dev/null @@ -1,53 +0,0 @@ -Langage: - -Distribution: - -Environnement: - -- Porter SearchIsos - -Noyau: - -Tactic: - -- Que contradiction raisonne a isomorphisme pres de False - -Vernac: - -- Print / Print Proof en fait identiques ; Print ne devrait pas afficher - les constantes opaques (devrait afficher qqchose comme ) - -Theories: - -- Rendre transparent tous les theoremes prouvant {A}+{B} -- Faire demarrer PolyList.nth a` l'indice 0 - Renommer l'actuel nth en nth1 ?? - -Doc: - -- Mettre à jour les messages d'erreurs de Discriminate/Simplify_eq/Injection -- Documenter le filtrage sur les types inductifs avec let-ins (dont la - compatibilite V6) - -- Ajouter let dans les règles du CIC - -> FAIT, mais reste a documenter le let dans les inductifs - et les champs manifestes dans les Record -- revoir le chapitre sur les tactiques utilisateur -- faut-il mieux spécifier la sémantique de Simpl (??) - -- Préciser la clarification syntaxique de IntroPattern -- preciser que Goal vient en dernier dans une clause pattern list et - qu'il doit apparaitre si il y a un "in" - -- Omega Time debranche mais Omega System et Omega Action remarchent ? -- Ajout "Replace in" (mais TODO) -- Syntaxe Conditional tac Rewrite marche, à documenter -- Documenter Dependent Rewrite et CutRewrite ? -- Ajouter les motifs sous-termes de ltac - -- ajouter doc de GenFixpoint (mais avant: changer syntaxe) (J. Forest ou Pierre C.) -- mettre à jour la doc de induction (arguments multiples) (Pierre C.) -- mettre à jour la doc de functional induction/scheme (J. Forest ou Pierre C.) ---> mettre à jour le CHANGES (vers la ligne 72) - - diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 9942816d..e3431fec 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -53,10 +53,14 @@ let path_of_mexpr = function | SEBident mp -> mp | _ -> raise Not_path -let rec list_split_assoc k rev_before = function +let is_modular = function + | SFBmodule _ | SFBmodtype _ -> true + | SFBconst _ | SFBmind _ -> false + +let rec list_split_assoc ((k,m) as km) rev_before = function | [] -> raise Not_found - | (k',b)::after when k=k' -> rev_before,b,after - | h::tail -> list_split_assoc k (h::rev_before) tail + | (k',b)::after when k=k' && is_modular b = m -> rev_before,b,after + | h::tail -> list_split_assoc km (h::rev_before) tail let check_definition_sub env cb1 cb2 = let check_type env t1 t2 = @@ -131,38 +135,35 @@ let lookup_modtype mp env = let rec check_with env mtb with_decl mp= match with_decl with - | With_definition_body _ -> - check_with_aux_def env mtb with_decl mp; + | With_definition_body (idl,c) -> + check_with_def env mtb (idl,c) mp; mtb - | With_module_body _ -> - check_with_aux_mod env mtb with_decl mp; + | With_module_body (idl,mp1) -> + check_with_mod env mtb (idl,mp1) mp; mtb -and check_with_aux_def env mtb with_decl mp = +and check_with_def env mtb (idl,c) mp = let sig_b = match mtb with | SEBstruct(sig_b) -> sig_b | _ -> error_signature_expected mtb in - let id,idl = match with_decl with - | With_definition_body (id::idl,_) | With_module_body (id::idl,_) -> - id,idl - | With_definition_body ([],_) | With_module_body ([],_) -> assert false + let id,idl = match idl with + | [] -> assert false + | id::idl -> id,idl in let l = label_of_id id in try - let rev_before,spec,after = list_split_assoc l [] sig_b in + let rev_before,spec,after = list_split_assoc (l,(idl<>[])) [] sig_b in let before = List.rev rev_before in let env' = Modops.add_signature mp before empty_delta_resolver env in - match with_decl with - | With_definition_body ([],_) -> assert false - | With_definition_body ([id],c) -> + if idl = [] then let cb = match spec with SFBconst cb -> cb | _ -> error_not_a_constant l in check_definition_sub env' c cb - | With_definition_body (_::_,_) -> + else let old = match spec with SFBmodule msb -> msb | _ -> error_not_a_module l @@ -170,49 +171,36 @@ and check_with_aux_def env mtb with_decl mp = begin match old.mod_expr with | None -> - let new_with_decl = match with_decl with - With_definition_body (_,c) -> - With_definition_body (idl,c) - | With_module_body (_,c) -> - With_module_body (idl,c) in - check_with_aux_def env' old.mod_type new_with_decl (MPdot(mp,l)) + check_with_def env' old.mod_type (idl,c) (MPdot(mp,l)) | Some msb -> error_a_generative_module_expected l end - | _ -> anomaly "Modtyping:incorrect use of with" with Not_found -> error_no_such_label l | Reduction.NotConvertible -> error_with_incorrect l -and check_with_aux_mod env mtb with_decl mp = +and check_with_mod env mtb (idl,mp1) mp = let sig_b = match mtb with | SEBstruct(sig_b) -> sig_b | _ -> error_signature_expected mtb in - let id,idl = match with_decl with - | With_definition_body (id::idl,_) | With_module_body (id::idl,_) -> - id,idl - | With_definition_body ([],_) | With_module_body ([],_) -> assert false + let id,idl = match idl with + | [] -> assert false + | id::idl -> id,idl in let l = label_of_id id in try - let rev_before,spec,after = list_split_assoc l [] sig_b in + let rev_before,spec,after = list_split_assoc (l,false) [] sig_b in let before = List.rev rev_before in - let rec mp_rec = function - | [] -> mp - | i::r -> MPdot(mp_rec r,label_of_id i) - in let env' = Modops.add_signature mp before empty_delta_resolver env in - match with_decl with - | With_module_body ([],_) -> assert false - | With_module_body ([id], mp1) -> + if idl = [] then let _ = match spec with SFBmodule msb -> msb | _ -> error_not_a_module l in let (_:module_body) = (lookup_module mp1 env) in () - | With_module_body (_::_,mp) -> + else let old = match spec with SFBmodule msb -> msb | _ -> error_not_a_module l @@ -220,17 +208,11 @@ and check_with_aux_mod env mtb with_decl mp = begin match old.mod_expr with None -> - let new_with_decl = match with_decl with - With_definition_body (_,c) -> - With_definition_body (idl,c) - | With_module_body (_,c) -> - With_module_body (idl,c) in - check_with_aux_mod env' - old.mod_type new_with_decl (MPdot(mp,l)) + check_with_mod env' + old.mod_type (idl,mp1) (MPdot(mp,l)) | Some msb -> error_a_generative_module_expected l end - | _ -> anomaly "Modtyping:incorrect use of with" with Not_found -> error_no_such_label l | Reduction.NotConvertible -> error_with_incorrect l diff --git a/checker/subtyping.ml b/checker/subtyping.ml index 0c97254b..9870ba13 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -28,15 +28,18 @@ type namedobject = | Constant of constant_body | IndType of inductive * mutual_inductive_body | IndConstr of constructor * mutual_inductive_body + +type namedmodule = | Module of module_body | Modtype of module_type_body (* adds above information about one mutual inductive: all types and constructors *) -let add_nameobjects_of_mib ln mib map = - let add_nameobjects_of_one j oib map = - let ip = (ln,j) in +let add_mib_nameobjects mp l mib map = + let ind = make_mind mp empty_dirpath l in + let add_mip_nameobjects j oib map = + let ip = (ind,j) in let map = array_fold_right_i (fun i id map -> @@ -46,22 +49,32 @@ let add_nameobjects_of_mib ln mib map = in Labmap.add (label_of_id oib.mind_typename) (IndType (ip, mib)) map in - array_fold_right_i add_nameobjects_of_one mib.mind_packets map + array_fold_right_i add_mip_nameobjects mib.mind_packets map + + +(* creates (namedobject/namedmodule) map for the whole signature *) +type labmap = { objs : namedobject Labmap.t; mods : namedmodule Labmap.t } -(* creates namedobject map for the whole signature *) +let empty_labmap = { objs = Labmap.empty; mods = Labmap.empty } -let make_label_map mp list = +let get_obj mp map l = + try Labmap.find l map.objs + with Not_found -> error_no_such_label_sub l mp + +let get_mod mp map l = + try Labmap.find l map.mods + with Not_found -> error_no_such_label_sub l mp + +let make_labmap mp list = let add_one (l,e) map = - let add_map obj = Labmap.add l obj map in match e with - | SFBconst cb -> add_map (Constant cb) - | SFBmind mib -> - add_nameobjects_of_mib (make_mind mp empty_dirpath l) mib map - | SFBmodule mb -> add_map (Module mb) - | SFBmodtype mtb -> add_map (Modtype mtb) + | SFBconst cb -> { map with objs = Labmap.add l (Constant cb) map.objs } + | SFBmind mib -> { map with objs = add_mib_nameobjects mp l mib map.objs } + | SFBmodule mb -> { map with mods = Labmap.add l (Module mb) map.mods } + | SFBmodtype mtb -> { map with mods = Labmap.add l (Modtype mtb) map.mods } in - List.fold_right add_one list Labmap.empty + List.fold_right add_one list empty_labmap let check_conv_error error f env a1 a2 = @@ -282,7 +295,6 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 = let ty1 = type_of_constructor cstr (mind1,mind1.mind_packets.(i)) in let ty2 = Typeops.type_of_constant_type env cb2.const_type in check_conv conv env ty1 ty2 - | _ -> error () let rec check_modules env msb1 msb2 subst1 subst2 = let mty1 = module_type_of_module None msb1 in @@ -291,29 +303,25 @@ let rec check_modules env msb1 msb2 subst1 subst2 = and check_signatures env mp1 sig1 sig2 subst1 subst2 = - let map1 = make_label_map mp1 sig1 in + let map1 = make_labmap mp1 sig1 in let check_one_body (l,spec2) = - let info1 = - try - Labmap.find l map1 - with - Not_found -> error_no_such_label_sub l mp1 - in match spec2 with | SFBconst cb2 -> - check_constant env mp1 l info1 cb2 spec2 subst1 subst2 + check_constant env mp1 l (get_obj mp1 map1 l) + cb2 spec2 subst1 subst2 | SFBmind mib2 -> - check_inductive env mp1 l info1 mib2 spec2 subst1 subst2 + check_inductive env mp1 l (get_obj mp1 map1 l) + mib2 spec2 subst1 subst2 | SFBmodule msb2 -> begin - match info1 with + match get_mod mp1 map1 l with | Module msb -> check_modules env msb msb2 subst1 subst2 | _ -> error_not_match l spec2 end | SFBmodtype mtb2 -> let mtb1 = - match info1 with + match get_mod mp1 map1 l with | Modtype mtb -> mtb | _ -> error_not_match l spec2 in diff --git a/configure b/configure index 867ee935..44170b99 100755 --- a/configure +++ b/configure @@ -6,10 +6,10 @@ # ################################## -VERSION=8.4beta +VERSION=8.4beta2 VOMAGIC=08400 STATEMAGIC=58400 -DATE="December 2011" +DATE=`LC_ALL=C LANG=C date +"%B %Y"` # Create the bin/ directory if non-existent test -d bin || mkdir bin @@ -292,7 +292,7 @@ case $DATEPGM in "") echo "I can't find the program \"date\" in your path." echo "Please give me the current date" read COMPILEDATE;; - *) COMPILEDATE=`date +"%h %d %Y %H:%M:%S"`;; + *) COMPILEDATE=`LC_ALL=C LANG=C date +"%h %d %Y %H:%M:%S"`;; esac # Architecture @@ -388,7 +388,7 @@ fi if [ "$browser_spec" = "no" ]; then case $ARCH in - win32) BROWSER='C:\PROGRA~1\INTERN~1\IEXPLORE %s' ;; + win32) BROWSER='start %s' ;; Darwin) BROWSER='open %s' ;; *) BROWSER='firefox -remote "OpenURL(%s,new-tab)" || firefox %s &' ;; esac @@ -445,16 +445,16 @@ esac CAMLVERSION=`"$bytecamlc" -version` case $CAMLVERSION in - 1.*|2.*|3.0*) + 1.*|2.*|3.0*|3.10*|3.11.[01]) echo "Your version of Objective-Caml is $CAMLVERSION." if [ "$force_caml_version" = "yes" ]; then echo "*Warning* You are compiling Coq with an outdated version of Objective-Caml." else - echo " You need Objective-Caml 3.10.0 or later." + echo " You need Objective-Caml 3.11.2 or later." echo " Configuration script failed!" exit 1 fi;; - 3.1*) + 3.11.2|3.12*) CAMLP4COMPAT="-loc loc" echo "You have Objective-Caml $CAMLVERSION. Good!";; *) @@ -742,7 +742,7 @@ case $ARCH$CYGWIN in bindir_def=${W32PREF}bin libdir_def=${W32PREF}lib configdir_def=${W32PREF}config - datadir_def=${W32PREF}data + datadir_def=${W32PREF}share mandir_def=${W32PREF}man docdir_def=${W32PREF}doc emacslib_def=${W32PREF}emacs @@ -795,10 +795,15 @@ case $libdir_spec in *) LIBDIR_OPTION="None";; esac -case $configdir_spec/$local in - yes/*) CONFIGDIR=$configdir;; - */true) CONFIGDIR=$COQTOP/ide - configdir_spec=yes;; +case $configdir_spec/$prefix_spec/$local in + yes/*/*) CONFIGDIR=$configdir;; + */yes/*) configdir_spec=yes + case $ARCH in + win32) CONFIGDIR=$prefix/config;; + *) CONFIGDIR=$prefix/etc/xdg/coq;; + esac;; + */*/true) CONFIGDIR=$COQTOP/ide + configdir_spec=yes;; *) printf "Where should I install the Coqide configuration files [$configdir_def]? " read CONFIGDIR case $CONFIGDIR in diff --git a/dev/base_include b/dev/base_include index d1125965..ad2a3aec 100644 --- a/dev/base_include +++ b/dev/base_include @@ -123,7 +123,6 @@ open Decl_mode open Auto open Autorewrite open Contradiction -open Dhyp open Eauto open Elim open Equality @@ -199,6 +198,11 @@ let current_goal () = get_nth_goal 1;; let pf_e gl s = Constrintern.interp_constr (project gl) (pf_env gl) (parse_constr s);; +(* Set usual printing since the global env is available from the tracer *) +let _ = Constrextern.in_debugger := false +let _ = Constrextern.set_debug_global_reference_printer + (fun loc r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Idset.empty r));; + open Toplevel let go = loop diff --git a/dev/printers.mllib b/dev/printers.mllib index 6a42678e..40a5a822 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -105,12 +105,12 @@ Notation Dumpglob Reserve Impargs -Constrextern Syntax_def Implicit_quantifiers Smartlocate Constrintern Modintern +Constrextern Tacexpr Proof_type Goal diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 3fc90761..3116cbf2 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -487,5 +487,9 @@ let short_string_of_ref loc = function [id_of_label (pi3 (repr_mind kn));id_of_string ("_"^string_of_int i)] (id_of_string ("_"^string_of_int j)) +(* Anticipate that printers can be used from ocamldebug and that + pretty-printer should not make calls to the global env since ocamldebug + runs in a different process and does not have the proper env at hand *) +let _ = Constrextern.in_debugger := true let _ = Constrextern.set_debug_global_reference_printer (if !rawdebug then raw_string_of_ref else short_string_of_ref) diff --git a/doc/common/macros.tex b/doc/common/macros.tex index f0fb0883..ce998a9b 100755 --- a/doc/common/macros.tex +++ b/doc/common/macros.tex @@ -206,6 +206,7 @@ %END LATEX %HEVEA \renewcommand{\proof}{\nterm{proof}} \newcommand{\record}{\nterm{record}} +\newcommand{\recordkw}{\nterm{record\_keyword}} \newcommand{\rewrule}{\nterm{rewriting\_rule}} \newcommand{\sentence}{\nterm{sentence}} \newcommand{\simplepattern}{\nterm{simple\_pattern}} diff --git a/doc/common/styles/html/coqremote/cover.html b/doc/common/styles/html/coqremote/cover.html index f4809a48..62ee00ac 100644 --- a/doc/common/styles/html/coqremote/cover.html +++ b/doc/common/styles/html/coqremote/cover.html @@ -27,7 +27,6 @@