From e978da8c41d8a3c19a29036d9c569fbe2a4616b0 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 16 Jun 2006 14:41:51 +0000 Subject: Imported Upstream version 8.0pl3+8.1beta --- toplevel/command.ml | 27 +++++++++++++++++++++----- toplevel/coqtop.ml | 30 +++++++++++++++++------------ toplevel/discharge.ml | 4 ++-- toplevel/himsg.ml | 23 ++++++++++------------- toplevel/minicoq.ml | 4 ++-- toplevel/record.ml | 4 ++-- toplevel/toplevel.ml | 8 +++++--- toplevel/usage.ml | 3 ++- toplevel/vernac.ml | 47 ++++++++++++++++++++++++---------------------- toplevel/vernacentries.ml | 4 ++-- toplevel/vernacentries.mli | 4 +++- 11 files changed, 93 insertions(+), 65 deletions(-) (limited to 'toplevel') diff --git a/toplevel/command.ml b/toplevel/command.ml index 7ff1b1b5..56a32f04 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: command.ml 8689 2006-04-07 20:20:16Z herbelin $ *) +(* $Id: command.ml 8875 2006-05-29 19:59:11Z msozeau $ *) open Pp open Util @@ -112,7 +112,7 @@ let constant_entry_of_com (bl,com,comtypopt,opacity,boxed) = | Some comtyp -> (* We use a cast to avoid troubles with evars in comtyp *) (* that can only be resolved knowing com *) - let b = abstract_constr_expr (mkCastC (com,DEFAULTcast,comtyp)) bl in + let b = abstract_constr_expr (mkCastC (com, Rawterm.CastConv DEFAULTcast,comtyp)) bl in let (body,typ) = destSubCast (interp_constr sigma env b) in { const_entry_body = body; const_entry_type = Some typ; @@ -219,7 +219,7 @@ let declare_one_elimination ind = let elim_scheme = Indrec.build_indrec env sigma ind in let npars = mib.mind_nparams_rec in let make_elim s = Indrec.instantiate_indrec_scheme s npars elim_scheme in - let kelim = mip.mind_kelim in + let kelim = elim_sorts (mib,mip) in (* in case the inductive has a type elimination, generates only one induction scheme, the other ones share the same code with the apropriate type *) @@ -457,7 +457,9 @@ let build_recursive (lnameargsardef:(fixpoint_expr *decl_notation) list) let lrecnames = List.map (fun ((f,_,_,_,_),_) -> f) lnameargsardef and sigma = Evd.empty and env0 = Global.env() - and nv = Array.of_list (List.map (fun ((_,n,_,_,_),_) -> n) lnameargsardef) in + and nv = Array.of_list (List.map (fun ((_,n,_,_,_),_) -> n) lnameargsardef) + and bl = Array.of_list (List.map (fun ((_,_,bl,_,_),_) -> bl) lnameargsardef) + in (* Build the recursive context and notations for the recursive types *) let (rec_sign,rec_impls,arityl) = List.fold_left @@ -502,9 +504,24 @@ let build_recursive (lnameargsardef:(fixpoint_expr *decl_notation) list) let recvec = Array.map (subst_vars (List.rev (Array.to_list namerec))) defrec in let recdecls = (Array.map (fun id -> Name id) namerec, arrec, recvec) in + let nvrec = Array.mapi + (fun i (n,_) -> match n with + | Some n -> n + | None -> + (* Recursive argument was not given by the user : + We check that there is only one inductive argument *) + let ctx = snd (interp_context sigma env0 bl.(i)) in + let isIndApp t = isInd (fst (decompose_app (strip_head_cast t))) in + (* This could be more precise (e.g. do some delta) *) + let lb = List.rev_map (fun (_,_,t) -> isIndApp t) ctx in + try (list_unique_index true lb) - 1 + with Not_found -> + error "the recursive argument needs to be specified") + nvrec + in let rec declare i fi = let ce = - { const_entry_body = mkFix ((Array.map fst nvrec,i),recdecls); (* ignore rec order *) + { const_entry_body = mkFix ((nvrec,i),recdecls); (* ignore rec order *) const_entry_type = Some arrec.(i); const_entry_opaque = false; const_entry_boxed = boxed} in diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index c3f79e0a..6d65ccc2 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqtop.ml 7740 2005-12-26 20:07:21Z herbelin $ *) +(* $Id: coqtop.ml 8932 2006-06-09 09:29:03Z notin $ *) open Pp open Util @@ -108,14 +108,16 @@ let add_compile verbose s = compile_list := (verbose,s) :: !compile_list let compile_files () = let init_state = States.freeze() in - List.iter - (fun (v,f) -> - States.unfreeze init_state; - if Options.do_translate () then - with_option translate_file (Vernac.compile v) f - else - Vernac.compile v f) - (List.rev !compile_list) + let coqdoc_init_state = Constrintern.coqdoc_freeze () in + List.iter + (fun (v,f) -> + States.unfreeze init_state; + Constrintern.coqdoc_unfreeze coqdoc_init_state; + if Options.do_translate () then + with_option translate_file (Vernac.compile v) f + else + Vernac.compile v f) + (List.rev !compile_list) let re_exec_version = ref "" let set_byte () = re_exec_version := "byte" @@ -172,7 +174,11 @@ let ide_args = ref [] let parse_args is_ide = 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 + else usage (); + parse rem | "-impredicative-set" :: rem -> set_engagement Declarations.ImpredicativeSet; parse rem @@ -242,9 +248,9 @@ let parse_args is_ide = | "-debug" :: rem -> set_debug (); parse rem | "-vm" :: rem -> use_vm := true; parse rem - | "-emacs" :: rem -> Options.print_emacs := true; parse rem + | "-emacs" :: rem -> Options.print_emacs := true; Pp.make_pp_emacs(); parse rem - | "-where" :: _ -> print_endline Coq_config.coqlib; exit 0 + | "-where" :: _ -> print_endline (getenv_else "COQLIB" Coq_config.coqlib); exit 0 | ("-quiet"|"-silent") :: rem -> Options.make_silent true; parse rem diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 6c543079..c011ba52 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: discharge.ml 7493 2005-11-02 22:12:16Z mohring $ *) +(* $Id: discharge.ml 8845 2006-05-23 07:41:58Z herbelin $ *) open Names open Util @@ -73,7 +73,7 @@ let process_inductive sechyps modlist mib = let inds = array_map_to_list (fun mip -> - let arity = expmod_constr modlist mip.mind_user_arity in + let arity = expmod_constr modlist (Termops.refresh_universes (Inductive.type_of_inductive (mib,mip))) in let lc = Array.map (expmod_constr modlist) mip.mind_user_lc in (mip.mind_typename, arity, diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 3fe51b5a..73aaef30 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: himsg.ml 8005 2006-02-07 22:50:35Z herbelin $ *) +(* $Id: himsg.ml 8845 2006-05-23 07:41:58Z herbelin $ *) open Pp open Util @@ -81,14 +81,14 @@ let rec pr_disjunction pr = function | a::l -> pr a ++ str "," ++ spc () ++ pr_disjunction pr l | [] -> assert false -let explain_elim_arity ctx ind aritylst c pj okinds = +let explain_elim_arity ctx ind sorts c pj okinds = let ctx = make_all_name_different ctx in let pi = pr_inductive ctx ind in let pc = pr_lconstr_env ctx c in let msg = match okinds with | Some(kp,ki,explanation) -> - let pki = pr_lconstr_env ctx ki in - let pkp = pr_lconstr_env ctx kp in + let pki = pr_sort_family ki in + let pkp = pr_sort_family kp in let explanation = match explanation with | NonInformativeToInformative -> "proofs can be eliminated only to build proofs" @@ -107,13 +107,10 @@ let explain_elim_arity ctx ind aritylst c pj okinds = hov 0 ( str "Incorrect elimination of" ++ spc() ++ pc ++ spc () ++ str "in the inductive type " ++ spc() ++ quote pi ++ - (let sorts = List.map (fun x -> mkSort (new_sort_in_family x)) - (list_uniquize (List.map (fun ar -> - family_of_sort (destSort (snd (decompose_prod_assum ar)))) aritylst)) in - let ppar = pr_disjunction (pr_lconstr_env ctx) sorts in - let ppt = pr_lconstr_env ctx (snd (decompose_prod_assum pj.uj_type)) in - str "," ++ spc() ++ str "the return type has sort" ++ spc() ++ ppt ++ - spc () ++ str "while it should be " ++ ppar)) + (let ppar = pr_disjunction (fun s -> quote (pr_sort_family s)) sorts in + let ppt = pr_lconstr_env ctx (snd (decompose_prod_assum pj.uj_type)) in + str "," ++ spc() ++ str "the return type has sort" ++ spc() ++ ppt ++ + spc () ++ str "while it should be " ++ ppar)) ++ fnl () ++ msg let explain_case_not_inductive ctx cj = @@ -565,14 +562,14 @@ let error_bad_entry () = let error_not_allowed_case_analysis dep kind i = str (if dep then "Dependent" else "Non Dependent") ++ - str " case analysis on sort: " ++ print_sort kind ++ fnl () ++ + str " case analysis on sort: " ++ pr_sort kind ++ fnl () ++ str "is not allowed for inductive definition: " ++ pr_inductive (Global.env()) i let error_bad_induction dep indid kind = str (if dep then "Dependent" else "Non dependent") ++ str " induction for type " ++ pr_id indid ++ - str " and sort " ++ print_sort kind ++ spc () ++ + str " and sort " ++ pr_sort kind ++ spc () ++ str "is not allowed" let error_not_mutual_in_scheme () = diff --git a/toplevel/minicoq.ml b/toplevel/minicoq.ml index 490765a4..a3b51a11 100644 --- a/toplevel/minicoq.ml +++ b/toplevel/minicoq.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: minicoq.ml 5920 2004-07-16 20:01:26Z herbelin $ *) +(* $Id: minicoq.ml 8752 2006-04-27 19:37:33Z herbelin $ *) open Pp open Util @@ -54,7 +54,7 @@ let check c = let definition id ty c = let c = globalize [] c in - let ty = option_app (globalize []) ty in + let ty = option_map (globalize []) ty in let ce = { const_entry_body = c; const_entry_type = ty } in let sp = make_path [] id CCI in env := add_constant sp ce (locals()) !env; diff --git a/toplevel/record.ml b/toplevel/record.ml index b24e85da..9eeeb51e 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: record.ml 7941 2006-01-28 23:07:59Z herbelin $ *) +(* $Id: record.ml 8875 2006-05-29 19:59:11Z msozeau $ *) open Pp open Util @@ -36,7 +36,7 @@ let interp_decl sigma env = function | Vernacexpr.DefExpr((_,id),c,t) -> let c = match t with | None -> c - | Some t -> mkCastC (c,DEFAULTcast,t) + | Some t -> mkCastC (c, Rawterm.CastConv DEFAULTcast,t) in let j = interp_constr_judgment Evd.empty env c in (id,Some j.uj_val, j.uj_type) diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index a5c2564c..95c1b7d9 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: toplevel.ml 6947 2005-04-20 16:18:41Z coq $ *) +(* $Id: toplevel.ml 8748 2006-04-27 16:01:26Z courtieu $ *) open Pp open Util @@ -47,9 +47,12 @@ let resynch_buffer ibuf = ibuf.start <- ibuf.start + ll | _ -> () + (* Read a char in an input channel, displaying a prompt at every beginning of line. *) +let emacs_prompt_endstring = String.make 1 (Char.chr 249) + let prompt_char ic ibuf count = let bol = match ibuf.bols with | ll::_ -> ibuf.len == ll @@ -204,7 +207,6 @@ let make_prompt () = *) let make_emacs_prompt() = let statnum = string_of_int (Lib.current_command_label ()) in - let endchar = String.make 1 (Char.chr 249) in let dpth = Pfedit.current_proof_depth() in let pending = Pfedit.get_all_proof_names() in let pendingprompt = @@ -212,7 +214,7 @@ let make_emacs_prompt() = (fun acc x -> acc ^ (if acc <> "" then "|" else "") ^ Names.string_of_id x) "" pending in let proof_info = if dpth >= 0 then string_of_int dpth else "0" in - statnum ^ " |" ^ pendingprompt ^ "| " ^ proof_info ^ " < " ^ endchar + statnum ^ " |" ^ pendingprompt ^ "| " ^ proof_info ^ " < " ^ emacs_prompt_endstring (* A buffer to store the current command read on stdin. It is * initialized when a vernac command is immediately followed by "\n", diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 354aff0b..782fdc80 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: usage.ml 6053 2004-09-03 14:33:35Z herbelin $ *) +(* $Id: usage.ml 8932 2006-06-09 09:29:03Z notin $ *) let version () = Printf.printf "The Coq Proof Assistant, version %s (%s)\n" @@ -54,6 +54,7 @@ let print_usage_channel co command = -boot boot mode (implies -q and -batch) -emacs tells Coq it is executed under Emacs -dump-glob f dump globalizations in file f (to be used by coqdoc) + -with-geoproof (yes|no) to (de)activate special functions for Geoproof within Coqide (default is yes) -impredicative-set set sort Set impredicative -dont-load-proofs don't load opaque proofs in memory -xml export XML files either to the hierarchy rooted in diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 64d77b74..afe72f0f 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: vernac.ml 7744 2005-12-27 09:16:06Z herbelin $ *) +(* $Id: vernac.ml 8924 2006-06-08 17:49:01Z notin $ *) (* Parsing of vernacular. *) @@ -126,27 +126,30 @@ let rec vernac_com interpfun (loc,com) = (* end translator state *) (* coqdoc state *) let cds = Constrintern.coqdoc_freeze() in - if !Options.translate_file then begin - let _,f = find_file_in_path (Library.get_load_paths ()) - (make_suffix fname ".v") in - chan_translate := open_out (f^"8"); - Pp.comments := [] - end; - begin try - read_vernac_file verbosely (make_suffix fname ".v"); - if !Options.translate_file then close_out !chan_translate; - chan_translate := ch; - Lexer.restore_com_state cs; - Pp.comments := cl; - Constrintern.coqdoc_unfreeze cds; - with e -> - if !Options.translate_file then close_out !chan_translate; - chan_translate := ch; - Lexer.restore_com_state cs; - Pp.comments := cl; - Constrintern.coqdoc_unfreeze cds; - raise e end; - + if !Options.translate_file then + begin + let _,f = find_file_in_path (Library.get_load_paths ()) + (make_suffix fname ".v") in + chan_translate := open_out (f^"8"); + Pp.comments := [] + end; + begin + try + read_vernac_file verbosely (make_suffix fname ".v"); + if !Options.translate_file then close_out !chan_translate; + chan_translate := ch; + Lexer.restore_com_state cs; + Pp.comments := cl; + Constrintern.coqdoc_unfreeze cds + with e -> + if !Options.translate_file then close_out !chan_translate; + chan_translate := ch; + Lexer.restore_com_state cs; + Pp.comments := cl; + Constrintern.coqdoc_unfreeze cds; + raise e + end + | VernacList l -> List.iter (fun (_,v) -> interp v) l | VernacTime v -> diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 7394bd8f..033fb0e6 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: vernacentries.ml 8700 2006-04-11 23:14:15Z courtieu $ i*) +(*i $Id: vernacentries.ml 8751 2006-04-27 16:17:51Z courtieu $ i*) (* Concrete syntax of the mathematical vernacular MV V2.6 *) @@ -345,7 +345,7 @@ let vernac_start_proof kind sopt (bl,t) lettop hook = let vernac_end_proof = function | Admitted -> admit () | Proved (is_opaque,idopt) -> - if_verbose show_script (); + if not !Options.print_emacs then if_verbose show_script (); match idopt with | None -> save_named is_opaque | Some ((_,id),None) -> save_anonymous is_opaque id diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli index a2bcd990..bcd89490 100644 --- a/toplevel/vernacentries.mli +++ b/toplevel/vernacentries.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: vernacentries.mli 6616 2005-01-21 17:18:23Z herbelin $ i*) +(*i $Id: vernacentries.mli 8781 2006-05-03 10:15:05Z jforest $ i*) (*i*) open Names @@ -52,3 +52,5 @@ val set_pcoq_hook : pcoq_hook -> unit val abort_refine : ('a -> unit) -> 'a -> unit;; val interp : Vernacexpr.vernac_expr -> unit + +val vernac_reset_name : identifier Util.located -> unit -- cgit v1.2.3