diff options
author | 2006-11-21 21:38:49 +0000 | |
---|---|---|
committer | 2006-11-21 21:38:49 +0000 | |
commit | 70b9be8acc1d1ada178a95c1cd4013506e9d0d1b (patch) | |
tree | f672a286d962cc67c95874b3b60402fc957870b6 /toplevel | |
parent | a5bd4e097a94cc4f863bf4d4bcc5ce592c30ba47 (diff) | |
parent | 208a0f7bfa5249f9795e6e225f309cbe715c0fad (diff) |
Merge commit 'upstream/8.1.gamma' into 8.1
Diffstat (limited to 'toplevel')
-rw-r--r-- | toplevel/cerrors.ml | 42 | ||||
-rw-r--r-- | toplevel/command.ml | 737 | ||||
-rw-r--r-- | toplevel/command.mli | 6 | ||||
-rw-r--r-- | toplevel/coqtop.ml | 22 | ||||
-rw-r--r-- | toplevel/discharge.ml | 4 | ||||
-rw-r--r-- | toplevel/himsg.ml | 11 | ||||
-rw-r--r-- | toplevel/metasyntax.ml | 15 | ||||
-rw-r--r-- | toplevel/record.ml | 5 | ||||
-rw-r--r-- | toplevel/toplevel.ml | 28 | ||||
-rw-r--r-- | toplevel/vernac.ml | 14 | ||||
-rw-r--r-- | toplevel/vernacentries.ml | 134 | ||||
-rw-r--r-- | toplevel/vernacexpr.ml | 18 |
12 files changed, 562 insertions, 474 deletions
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index ab9c4c63..f6c5c3af 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: cerrors.ml 8003 2006-02-07 22:11:50Z herbelin $ *) +(* $Id: cerrors.ml 9306 2006-10-28 18:28:19Z herbelin $ *) open Pp open Util @@ -28,19 +28,21 @@ let guill s = "\""^s^"\"" let where s = if !Options.debug then (str"in " ++ str s ++ str":" ++ spc ()) else (mt ()) +let anomaly_string () = str "Anomaly: " + let report () = (str "." ++ spc () ++ str "Please report.") (* assumption : explain_sys_exn does NOT end with a 'FNL anymore! *) -let rec explain_exn_default = function +let rec explain_exn_default_aux anomaly_string report_fn = function | Stream.Failure -> - hov 0 (str "Anomaly: uncaught Stream.Failure.") + hov 0 (anomaly_string () ++ str "uncaught Stream.Failure.") | Stream.Error txt -> hov 0 (str "Syntax error: " ++ str txt) | Token.Error txt -> hov 0 (str "Syntax error: " ++ str txt) | Sys_error msg -> - hov 0 (str "Anomaly: uncaught exception Sys_error " ++ str (guill msg) ++ report ()) + hov 0 (anomaly_string () ++ str "uncaught exception Sys_error " ++ str (guill msg) ++ report_fn ()) | UserError(s,pps) -> hov 1 (str "User error: " ++ where s ++ pps) | Out_of_memory -> @@ -48,26 +50,26 @@ let rec explain_exn_default = function | Stack_overflow -> hov 0 (str "Stack overflow") | Anomaly (s,pps) -> - hov 1 (str "Anomaly: " ++ where s ++ pps ++ report ()) + hov 1 (anomaly_string () ++ where s ++ pps ++ report_fn ()) | Match_failure(filename,pos1,pos2) -> - hov 1 (str "Anomaly: Match failure in file " ++ str (guill filename) ++ + hov 1 (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 ()) + ++ report_fn ()) | Not_found -> - hov 0 (str "Anomaly: uncaught exception Not_found" ++ report ()) + hov 0 (anomaly_string () ++ str "uncaught exception Not_found" ++ report_fn ()) | Failure s -> - hov 0 (str "Anomaly: uncaught exception Failure " ++ str (guill s) ++ report ()) + hov 0 (anomaly_string () ++ str "uncaught exception Failure " ++ str (guill s) ++ report_fn ()) | Invalid_argument s -> - hov 0 (str "Anomaly: uncaught exception Invalid_argument " ++ str (guill s) ++ report ()) + hov 0 (anomaly_string () ++ str "uncaught exception Invalid_argument " ++ str (guill s) ++ report_fn ()) | Sys.Break -> - hov 0 (fnl () ++ str "User Interrupt.") + hov 0 (fnl () ++ str "User interrupt.") | Univ.UniverseInconsistency -> - hov 0 (str "Error: Universe Inconsistency.") + hov 0 (str "Error: Universe inconsistency.") | TypeError(ctx,te) -> hov 0 (str "Error:" ++ spc () ++ Himsg.explain_type_error ctx te) | PretypeError(ctx,te) -> @@ -97,7 +99,7 @@ let rec explain_exn_default = function | Stdpp.Exc_located (loc,exc) -> hov 0 ((if loc = dummy_loc then (mt ()) else (str"At location " ++ print_loc loc ++ str":" ++ fnl ())) - ++ explain_exn_default exc) + ++ explain_exn_default_aux anomaly_string report_fn exc) | Lexer.Error Illegal_character -> hov 0 (str "Syntax error: Illegal character.") | Lexer.Error Unterminated_comment -> @@ -109,7 +111,7 @@ let rec explain_exn_default = function | Lexer.Error (Bad_token s) -> hov 0 (str "Syntax error: Bad token" ++ spc () ++ str s ++ str ".") | Assert_failure (s,b,e) -> - hov 0 (str "Anomaly: assert failure" ++ spc () ++ + hov 0 (anomaly_string () ++ str "assert failure" ++ spc () ++ (if s <> "" then if Sys.ocaml_version = "3.06" then (str ("(file \"" ^ s ^ "\", characters ") ++ @@ -120,16 +122,22 @@ let rec explain_exn_default = function int (e+6) ++ str ")") else (mt ())) ++ - report ()) + report_fn ()) | reraise -> - hov 0 (str "Anomaly: Uncaught exception " ++ - str (Printexc.to_string reraise) ++ report ()) + hov 0 (anomaly_string () ++ str "Uncaught exception " ++ + str (Printexc.to_string reraise) ++ report_fn ()) + +let explain_exn_default = + explain_exn_default_aux (fun () -> str "Anomaly: ") report let raise_if_debug e = if !Options.debug then raise e let _ = Tactic_debug.explain_logic_error := explain_exn_default +let _ = Tactic_debug.explain_logic_error_no_anomaly := + explain_exn_default_aux (fun () -> mt()) (fun () -> mt()) + let explain_exn_function = ref explain_exn_default let explain_exn e = !explain_exn_function e diff --git a/toplevel/command.ml b/toplevel/command.ml index 56a32f04..d751f70c 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: command.ml 8875 2006-05-29 19:59:11Z msozeau $ *) +(* $Id: command.ml 9310 2006-10-28 19:35:09Z herbelin $ *) open Pp open Util @@ -32,11 +32,15 @@ open Proof_type open Tacmach open Safe_typing open Nametab +open Impargs open Typeops +open Reductionops open Indtypes open Vernacexpr open Decl_kinds open Pretyping +open Evarutil +open Evarconv open Notation let mkLambdaCit = List.fold_right (fun (x,a) b -> mkLambdaC(x,a,b)) @@ -56,11 +60,6 @@ let rec generalize_constr_expr c = function List.fold_right (fun x b -> mkProdC([x],t,b)) idl (generalize_constr_expr c bl) -let rec length_of_raw_binders = function - | [] -> 0 - | LocalRawDef _::bl -> 1 + length_of_raw_binders bl - | LocalRawAssum (idl,_)::bl -> List.length idl + length_of_raw_binders bl - let rec under_binders env f n c = if n = 0 then f env Evd.empty c else match kind_of_term c with @@ -78,12 +77,12 @@ let rec destSubCast c = match kind_of_term c with | Cast (b,_, u) -> (b,u) | _ -> assert false -let rec adjust_conclusion a cs = function - | CProdN (loc,bl,c) -> CProdN (loc,bl,adjust_conclusion a cs c) - | CLetIn (loc,b,t,c) -> CLetIn (loc,b,t,adjust_conclusion a cs c) +let rec complete_conclusion a cs = function + | CProdN (loc,bl,c) -> CProdN (loc,bl,complete_conclusion a cs c) + | CLetIn (loc,b,t,c) -> CLetIn (loc,b,t,complete_conclusion a cs c) | CHole loc -> - let (nar,name,params) = a in - if nar <> 0 then + let (has_no_args,name,params) = a in + if not has_no_args then user_err_loc (loc,"", str "Cannot infer the non constant arguments of the conclusion of " ++ pr_id cs); @@ -106,7 +105,7 @@ let constant_entry_of_com (bl,com,comtypopt,opacity,boxed) = let b = abstract_constr_expr com bl in let j = interp_constr_judgment sigma env b in { const_entry_body = j.uj_val; - const_entry_type = Some (refresh_universes j.uj_type); + const_entry_type = None; const_entry_opaque = opacity; const_entry_boxed = boxed } | Some comtyp -> @@ -125,7 +124,7 @@ let red_constant_entry bl ce = function let body = ce.const_entry_body in { ce with const_entry_body = under_binders (Global.env()) (fst (reduction_of_red_expr red)) - (length_of_raw_binders bl) + (local_binders_length bl) body } let declare_global_definition ident ce local = @@ -226,7 +225,8 @@ let declare_one_elimination ind = if List.mem InType kelim then let elim = make_elim (new_sort_in_family InType) in let cte = declare (mindstr^(Indrec.elimination_suffix InType)) elim None in - let c = mkConst cte and t = constant_type (Global.env()) cte in + let c = mkConst cte in + let t = type_of_constant (Global.env()) cte in List.iter (fun (sort,suff) -> let (t',c') = Indrec.instantiate_type_indrec_scheme (new_sort_in_family sort) @@ -248,371 +248,380 @@ let declare_eliminations sp = declare_one_elimination (sp,i) done -(* 3b| Mutual Inductive definitions *) - -let minductive_message = function +(* 3b| Mutual inductive definitions *) + +let compute_interning_datas env l nal typl = + let mk_interning_data na typ = + let idl, impl = + if is_implicit_args() then + let impl = compute_implicits env typ in + let sub_impl,_ = list_chop (List.length l) impl in + let sub_impl' = List.filter is_status_implicit sub_impl in + (List.map name_of_implicit sub_impl', impl) + else + ([],[]) in + (na, (idl, impl, compute_arguments_scope typ)) in + (l, List.map2 mk_interning_data nal typl) + +let declare_interning_data (_,impls) (df,c,scope) = + silently (Metasyntax.add_notation_interpretation df impls c) scope + +let push_named_types env idl tl = + List.fold_left2 (fun env id t -> Environ.push_named (id,None,t) env) + env idl tl + +let push_types env idl tl = + List.fold_left2 (fun env id t -> Environ.push_rel (Name id,None,t) env) + env idl tl + +type inductive_expr = { + ind_name : identifier; + ind_arity : constr_expr; + ind_lc : (identifier * constr_expr) list +} + +let minductive_message = function | [] -> error "no inductive definition" | [x] -> (pr_id x ++ str " is defined") | l -> hov 0 (prlist_with_sep pr_coma pr_id l ++ spc () ++ str "are defined") -let recursive_message v = - match Array.length v with - | 0 -> error "no recursive definition" - | 1 -> (Printer.pr_global v.(0) ++ str " is recursively defined") - | _ -> hov 0 (prvect_with_sep pr_coma Printer.pr_global v ++ - spc () ++ str "are recursively defined") - -let corecursive_message v = - match Array.length v with - | 0 -> error "no corecursive definition" - | 1 -> (Printer.pr_global v.(0) ++ str " is corecursively defined") - | _ -> hov 0 (prvect_with_sep pr_coma Printer.pr_global v ++ - spc () ++ str "are corecursively defined") +let check_all_names_different indl = + let get_names ind = ind.ind_name::List.map fst ind.ind_lc in + if not (list_distinct (List.flatten (List.map get_names indl))) then + error "Two inductive objects have the same name" + +let mk_mltype_data isevars env assums arity indname = + let is_ml_type = is_sort env (Evd.evars_of !isevars) arity in + (is_ml_type,indname,assums) + +let prepare_param = function + | (na,None,t) -> out_name na, LocalAssum t + | (na,Some b,_) -> out_name na, LocalDef b + +let interp_ind_arity isevars env ind = + interp_type_evars isevars env ind.ind_arity + +let interp_cstrs isevars env impls mldata arity ind = + let cnames,ctyps = List.split ind.ind_lc in + (* Complete conclusions of constructor types if given in ML-style syntax *) + let ctyps' = List.map2 (complete_conclusion mldata) cnames ctyps in + (* Interpret the constructor types *) + let ctyps'' = List.map (interp_type_evars isevars env ~impls) ctyps' in + (cnames, ctyps'') + +let interp_mutual paramsl indl notations finite = + check_all_names_different indl; + let env0 = Global.env() in + let isevars = ref (Evd.create_evar_defs Evd.empty) in + let env_params, ctx_params = interp_context_evars isevars env0 paramsl in + let indnames = List.map (fun ind -> ind.ind_name) indl in -let interp_mutual lparams lnamearconstrs finite = - let allnames = - List.fold_left (fun acc (id,_,_,l) -> id::(List.map fst l)@acc) - [] lnamearconstrs in - if not (list_distinct allnames) then - error "Two inductive objects have the same name"; - let sigma = Evd.empty and env0 = Global.env() in - let env_params, params = interp_context sigma env0 lparams in - - (* Builds the params of the inductive entry *) - let params' = - List.map (fun (na,b,t) -> - let id = match na with - | Name id -> id - | Anonymous -> anomaly "Unnamed inductive variable" in - match b with - | None -> (id, LocalAssum t) - | Some b -> (id, LocalDef b)) params - in - let paramassums = - List.fold_right (fun d l -> match d with - (id,LocalAssum _) -> id::l | (_,LocalDef _) -> l) params' [] in - let nparamassums = List.length paramassums in - let (ind_env,ind_impls,arityl) = - List.fold_left - (fun (env, ind_impls, arl) (recname, _, arityc, _) -> - let arity = interp_type sigma env_params arityc in - let fullarity = it_mkProd_or_LetIn arity params in - let env' = Termops.push_rel_assum (Name recname,fullarity) env in - let argsc = compute_arguments_scope fullarity in - let ind_impls' = - if Impargs.is_implicit_args() then - let impl = Impargs.compute_implicits env_params fullarity in - let paramimpl,_ = list_chop nparamassums impl in - let l = List.fold_right - (fun imp l -> if Impargs.is_status_implicit imp then - Impargs.name_of_implicit imp::l else l) paramimpl [] in - (recname,(l,impl,argsc))::ind_impls - else - (recname,([],[],argsc))::ind_impls in - (env', ind_impls', (arity::arl))) - (env0, [], []) lnamearconstrs - in (* Names of parameters as arguments of the inductive type (defs removed) *) - let lparargs = - List.flatten - (List.map (function (id,LocalAssum _) -> [id] | _ -> []) params') in - let notations = - List.fold_right (fun (_,ntnopt,_,_) l -> option_cons ntnopt l) - lnamearconstrs [] in - let fs = States.freeze() in - (* Declare the notations for the inductive types pushed in local context*) - try - List.iter (fun (df,c,scope) -> - silently (Metasyntax.add_notation_interpretation df ind_impls c) scope) - notations; - let ind_env_params = push_rel_context params ind_env in - - let mispecvec = - List.map2 - (fun ar (name,_,_,lname_constr) -> - let constrnames, bodies = List.split lname_constr in - (* Compute the conclusions of constructor types *) - (* for inductive given in ML syntax *) - let nar = - List.length (fst (Reductionops.splay_arity env_params Evd.empty ar)) - in - let bodies = - List.map2 (adjust_conclusion (nar,name,lparargs)) - constrnames bodies - in - - (* Interpret the constructor types *) - let constrs = - List.map - (interp_type sigma ind_env_params ~impls:(paramassums,ind_impls)) - bodies - in - - (* Build the inductive entry *) - { mind_entry_typename = name; - mind_entry_arity = ar; - mind_entry_consnames = constrnames; - mind_entry_lc = constrs }) - (List.rev arityl) lnamearconstrs - in - States.unfreeze fs; - notations, { mind_entry_params = params'; - mind_entry_record = false; - mind_entry_finite = finite; - mind_entry_inds = mispecvec } - with e -> States.unfreeze fs; raise e + let assums = List.filter(fun (_,b,_) -> b=None) ctx_params in + let params = List.map (fun (na,_,_) -> out_name na) assums in + + (* Interpret the arities *) + let arities = List.map (interp_ind_arity isevars env_params) indl in + let fullarities = List.map (fun c -> it_mkProd_or_LetIn c ctx_params) arities in + let env_ar = push_types env0 indnames fullarities in + let env_ar_params = push_rel_context ctx_params env_ar in + + (* Compute interpretation metadatas *) + let impls = compute_interning_datas env0 params indnames fullarities in + let mldatas = List.map2 (mk_mltype_data isevars env_params params) arities indnames in + + let constructors = + States.with_heavy_rollback (fun () -> + (* Temporary declaration of notations and scopes *) + List.iter (declare_interning_data impls) notations; + (* Interpret the constructor types *) + list_map3 (interp_cstrs isevars env_ar_params impls) mldatas arities indl) + () in + + (* Instantiate evars and check all are resolved *) + let isevars,_ = consider_remaining_unif_problems env_params !isevars in + let sigma = Evd.evars_of isevars in + let constructors = List.map (fun (idl,cl) -> (idl,List.map (nf_evar sigma) cl)) constructors in + let ctx_params = Sign.map_rel_context (nf_evar sigma) ctx_params in + let arities = List.map (nf_evar sigma) arities in + List.iter (check_evars env_params Evd.empty isevars) arities; + Sign.iter_rel_context (check_evars env0 Evd.empty isevars) ctx_params; + List.iter (fun (_,ctyps) -> + List.iter (check_evars env_ar_params Evd.empty isevars) ctyps) + constructors; + + (* Build the inductive entries *) + let entries = list_map3 (fun ind arity (cnames,ctypes) -> { + mind_entry_typename = ind.ind_name; + mind_entry_arity = arity; + mind_entry_consnames = cnames; + mind_entry_lc = ctypes + }) indl arities constructors in + + (* Build the mutual inductive entry *) + { mind_entry_params = List.map prepare_param ctx_params; + mind_entry_record = false; + mind_entry_finite = finite; + mind_entry_inds = entries } + +let eq_constr_expr c1 c2 = + try let _ = Constrextern.check_same_type c1 c2 in true with _ -> false + +(* Very syntactical equality *) +let eq_local_binder d1 d2 = match d1,d2 with + | LocalRawAssum (nal1,c1), LocalRawAssum (nal2,c2) -> + List.length nal1 = List.length nal2 && + List.for_all2 (fun (_,na1) (_,na2) -> na1 = na2) nal1 nal2 && + eq_constr_expr c1 c2 + | LocalRawDef ((_,id1),c1), LocalRawDef ((_,id2),c2) -> + id1 = id2 && eq_constr_expr c1 c2 + | _ -> + false + +let eq_local_binders bl1 bl2 = + List.length bl1 = List.length bl2 && List.for_all2 eq_local_binder bl1 bl2 + +let extract_coercions indl = + let mkqid (_,((_,id),_)) = make_short_qualid id in + let extract lc = List.filter (fun (iscoe,_) -> iscoe) lc in + List.map mkqid (List.flatten(List.map (fun (_,_,_,lc) -> extract lc) indl)) + +let extract_params indl = + let paramsl = List.map (fun (_,params,_,_) -> params) indl in + match paramsl with + | [] -> anomaly "empty list of inductive types" + | params::paramsl -> + if not (List.for_all (eq_local_binders params) paramsl) then error + "Parameters should be syntactically the same for each inductive type"; + params + +let prepare_inductive ntnl indl = + let indl = + List.map (fun ((_,indname),_,ar,lc) -> { + ind_name = indname; + ind_arity = ar; + ind_lc = List.map (fun (_,((_,id),t)) -> (id,t)) lc + }) indl in + List.fold_right option_cons ntnl [], indl let declare_mutual_with_eliminations isrecord mie = - let lrecnames = - List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in + let names = List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in let (_,kn) = declare_mind isrecord mie in - if_verbose ppnl (minductive_message lrecnames); + if_verbose ppnl (minductive_message names); declare_eliminations kn; kn -(* Very syntactical equality *) -let eq_la d1 d2 = match d1,d2 with - | LocalRawAssum (nal,ast), LocalRawAssum (nal',ast') -> - (List.length nal = List.length nal') && - List.for_all2 (fun (_,na) (_,na') -> na = na') nal nal' - & (try let _ = Constrextern.check_same_type ast ast' in true with _ -> false) - | LocalRawDef ((_,id),ast), LocalRawDef ((_,id'),ast') -> - id=id' & (try let _ = Constrextern.check_same_type ast ast' in true with _ -> false) - | _ -> false - -let extract_coe lc = - List.fold_right - (fun (addcoe,((_,(id:identifier)),t)) (l1,l2) -> - ((if addcoe then id::l1 else l1), (id,t)::l2)) lc ([],[]) - -let extract_coe_la_lc = function - | [] -> anomaly "Vernacentries: empty list of inductive types" - | ((_,id),ntn,la,ar,lc)::rest -> - let rec check = function - | [] -> [],[] - | ((_,id),ntn,la',ar,lc)::rest -> - if (List.length la = List.length la') && - (List.for_all2 eq_la la la') - then - let mcoes, mspec = check rest in - let coes, lc' = extract_coe lc in - (coes::mcoes,(id,ntn,ar,lc')::mspec) - else - error ("Parameters should be syntactically the same "^ - "for each inductive type") - in - let mcoes, mspec = check rest in - let coes, lc' = extract_coe lc in - (coes,la,(id,ntn,ar,lc'):: mspec) - -let build_mutual lind finite = - let ((coes:identifier list),lparams,lnamearconstructs) = extract_coe_la_lc lind in - let notations,mie = interp_mutual lparams lnamearconstructs finite in - let _ = declare_mutual_with_eliminations false mie in - (* Declare the notations now bound to the inductive types *) - List.iter (fun (df,c,scope) -> - Metasyntax.add_notation_interpretation df [] c scope) notations; - List.iter - (fun id -> - Class.try_add_new_coercion (locate (make_short_qualid id)) Global) coes - -(* try to find non recursive definitions *) - -let list_chop_hd i l = match list_chop i l with - | (l1,x::l2) -> (l1,x,l2) - | _ -> assert false +let build_mutual l finite = + let indl,ntnl = List.split l in + let paramsl = extract_params indl in + let coes = extract_coercions indl in + let notations,indl = prepare_inductive ntnl indl in + let mie = interp_mutual paramsl indl notations finite in + (* Declare the mutual inductive block with its eliminations *) + ignore (declare_mutual_with_eliminations false mie); + (* Declare the possible notations of inductive types *) + List.iter (declare_interning_data ([],[])) notations; + (* Declare the coercions *) + List.iter (fun qid -> Class.try_add_new_coercion (locate qid) Global) coes + +(* 3c| Fixpoints and co-fixpoints *) + +let recursive_message = function + | [] -> anomaly "no recursive definition" + | [id] -> pr_id id ++ str " is recursively defined" + | l -> hov 0 (prlist_with_sep pr_coma pr_id l ++ + spc () ++ str "are recursively defined") -let collect_non_rec env = - let rec searchrec lnonrec lnamerec ldefrec larrec nrec = - try - let i = - list_try_find_i - (fun i f -> - if List.for_all (fun def -> not (occur_var env f def)) ldefrec - then i else failwith "try_find_i") - 0 lnamerec - in - let (lf1,f,lf2) = list_chop_hd i lnamerec in - let (ldef1,def,ldef2) = list_chop_hd i ldefrec in - let (lar1,ar,lar2) = list_chop_hd i larrec in - let newlnv = - try - match list_chop i nrec with - | (lnv1,_::lnv2) -> (lnv1@lnv2) - | _ -> [] (* nrec=[] for cofixpoints *) - with Failure "list_chop" -> [] - in - searchrec ((f,def,ar)::lnonrec) - (lf1@lf2) (ldef1@ldef2) (lar1@lar2) newlnv - with Failure "try_find_i" -> - (List.rev lnonrec, - (Array.of_list lnamerec, Array.of_list ldefrec, - Array.of_list larrec, Array.of_list nrec)) - in - searchrec [] +let corecursive_message = function + | [] -> error "no corecursive definition" + | [id] -> pr_id id ++ str " is corecursively defined" + | l -> hov 0 (prlist_with_sep pr_coma pr_id l ++ + spc () ++ str "are corecursively defined") -let build_recursive (lnameargsardef:(fixpoint_expr *decl_notation) list) - boxed = - 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) - 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 - (fun (env,impls,arl) ((recname,_,bl,arityc,_),_) -> - let arityc = generalize_constr_expr arityc bl in - let arity = interp_type sigma env0 arityc in - let impl = - if Impargs.is_implicit_args() - then Impargs.compute_implicits env0 arity - else [] in - let impls' =(recname,([],impl,compute_arguments_scope arity))::impls in - (Environ.push_named (recname,None,arity) env, impls', arity::arl)) - (env0,[],[]) lnameargsardef in - let arityl = List.rev arityl in - let notations = - List.fold_right (fun (_,ntnopt) l -> option_cons ntnopt l) - lnameargsardef [] in - - let recdef = - - (* Declare local notations *) - let fs = States.freeze() in - let def = - try - List.iter (fun (df,c,scope) -> - silently - (Metasyntax.add_notation_interpretation df rec_impls c) scope) - notations; - List.map2 - (fun ((_,_,bl,_,def),_) arity -> - let def = abstract_constr_expr def bl in - interp_casted_constr sigma rec_sign ~impls:([],rec_impls) - def arity) - lnameargsardef arityl - with e -> - States.unfreeze fs; raise e in - States.unfreeze fs; def - in +let recursive_message isfix = + if isfix=Fixpoint then recursive_message else corecursive_message - let (lnonrec,(namerec,defrec,arrec,nvrec)) = - collect_non_rec env0 lrecnames recdef arityl (Array.to_list nv) in - 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 ((nvrec,i),recdecls); (* ignore rec order *) - const_entry_type = Some arrec.(i); - const_entry_opaque = false; - const_entry_boxed = boxed} in - let kn = declare_constant fi (DefinitionEntry ce,IsDefinition Fixpoint) - in (ConstRef kn) - in - (* declare the recursive definitions *) - let lrefrec = Array.mapi declare namerec in - if_verbose ppnl (recursive_message lrefrec); - (* The others are declared as normal definitions *) - let var_subst id = (id, global_reference id) in - let _ = - List.fold_left - (fun subst (f,def,t) -> - let ce = { const_entry_body = replace_vars subst def; - const_entry_type = Some t; - const_entry_opaque = false; - const_entry_boxed = boxed } in - let _ = - declare_constant f (DefinitionEntry ce,IsDefinition Definition) - in - warning ((string_of_id f)^" is non-recursively defined"); - (var_subst f) :: subst) - (List.map var_subst (Array.to_list namerec)) - lnonrec - in - List.iter (fun (df,c,scope) -> - Metasyntax.add_notation_interpretation df [] c scope) notations +(* An (unoptimized) function that maps preorders to partial orders... -let build_corecursive lnameardef boxed = - let lrecnames = List.map (fun (f,_,_,_) -> f) lnameardef - and sigma = Evd.empty - and env0 = Global.env() in - let fs = States.freeze() in - let (rec_sign,arityl) = - try - List.fold_left - (fun (env,arl) (recname,bl,arityc,_) -> - let arityc = generalize_constr_expr arityc bl in - let arity = interp_type Evd.empty env0 arityc in - let _ = declare_variable recname - (Lib.cwd(),SectionLocalAssum arity,IsAssumption Definitional) in - (Environ.push_named (recname,None,arity) env, (arity::arl))) - (env0,[]) lnameardef - with e -> - States.unfreeze fs; raise e in - let arityl = List.rev arityl in - let recdef = - try - List.map (fun (_,bl,arityc,def) -> - let arityc = generalize_constr_expr arityc bl in - let def = abstract_constr_expr def bl in - let arity = interp_constr sigma rec_sign arityc in - interp_casted_constr sigma rec_sign def arity) - lnameardef - with e -> - States.unfreeze fs; raise e + Input: a list of associations (x,[y1;...;yn]), all yi distincts + and different of x, meaning x<=y1, ..., x<=yn + + Output: a list of associations (x,Inr [y1;...;yn]), collecting all + distincts yi greater than x, _or_, (x, Inl y) meaning that + x is in the same class as y (in which case, x occurs + nowhere else in the association map) + + partial_order : ('a * 'a list) list -> ('a * ('a,'a list) union) list +*) + +let rec partial_order = function + | [] -> [] + | (x,xge)::rest -> + let rec browse res xge' = function + | [] -> + let res = List.map (function + | (z, Inr zge) when List.mem x zge -> (z, Inr (list_union zge xge')) + | r -> r) res in + (x,Inr xge')::res + | y::xge -> + let rec link y = + try match List.assoc y res with + | Inl z -> link z + | Inr yge -> + if List.mem x yge then + let res = List.remove_assoc y res in + let res = List.map (function + | (z, Inl t) -> + if t = y then (z, Inl x) else (z, Inl t) + | (z, Inr zge) -> + if List.mem y zge then + (z, Inr (list_add_set x (list_remove y zge))) + else + (z, Inr zge)) res in + browse ((y,Inl x)::res) xge' (list_union xge (list_remove x yge)) + else + browse res (list_add_set y (list_union xge' yge)) xge + with Not_found -> browse res (list_add_set y xge') xge + in link y + in browse (partial_order rest) [] xge + +let non_full_mutual_message x xge y yge kind rest = + let reason = + if List.mem x yge then + string_of_id y^" depends on "^string_of_id x^" but not conversely" + else if List.mem y xge then + string_of_id x^" depends on "^string_of_id y^" but not conversely" + else + string_of_id y^" and "^string_of_id x^" are not mutually dependent" in + let e = if rest <> [] then "e.g.: "^reason else reason in + let k = if kind=Fixpoint then "fixpoint" else "cofixpoint" in + let w = + if kind=Fixpoint then "Well-foundedness check may fail unexpectedly.\n" + else "" in + "Not a fully mutually defined "^k^"\n("^e^").\n"^w + +let check_mutuality env kind fixl = + let names = List.map fst fixl in + let preorder = + List.map (fun (id,def) -> + (id, List.filter (fun id' -> id<>id' & occur_var env id' def) names)) + fixl in + let po = partial_order preorder in + match List.filter (function (_,Inr _) -> true | _ -> false) po with + | (x,Inr xge)::(y,Inr yge)::rest -> + if_verbose warning (non_full_mutual_message x xge y yge kind rest) + | _ -> () + +type fixpoint_kind = + | IsFixpoint of (int option * recursion_order_expr) list + | IsCoFixpoint + +type fixpoint_expr = { + fix_name : identifier; + fix_binders : local_binder list; + fix_body : constr_expr; + fix_type : constr_expr +} + +let interp_fix_type isevars env fix = + interp_type_evars isevars env + (generalize_constr_expr fix.fix_type fix.fix_binders) + +let interp_fix_body isevars env impls fix fixtype = + interp_casted_constr_evars isevars env ~impls + (abstract_constr_expr fix.fix_body fix.fix_binders) fixtype + +let declare_fix boxed kind f def t = + let ce = { + const_entry_body = def; + const_entry_type = Some t; + const_entry_opaque = false; + const_entry_boxed = boxed + } in + let kn = declare_constant f (DefinitionEntry ce,IsDefinition kind) in + ConstRef kn + +let prepare_recursive_declaration fixnames fixtypes fixdefs = + let defs = List.map (subst_vars (List.rev fixnames)) fixdefs in + let names = List.map (fun id -> Name id) fixnames in + (Array.of_list names, Array.of_list fixtypes, Array.of_list defs) + +let compute_guardness_evidence (n,_) fixl fixtype = + 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 m = local_binders_length fixl.fix_binders in + let ctx = fst (Sign.decompose_prod_n_assum m fixtype) 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" + +let interp_recursive fixkind l boxed = + let env = Global.env() in + let fixl, ntnl = List.split l in + let kind = if fixkind <> IsCoFixpoint then Fixpoint else CoFixpoint in + let fixnames = List.map (fun fix -> fix.fix_name) fixl in + + (* Interp arities allowing for unresolved types *) + let isevars = ref (Evd.create_evar_defs Evd.empty) in + let fixtypes = List.map (interp_fix_type isevars env) fixl in + let env_rec = push_named_types env fixnames fixtypes in + + (* Get interpretation metadatas *) + let impls = compute_interning_datas env [] fixnames fixtypes in + let notations = List.fold_right option_cons ntnl [] in + + (* Interp bodies with rollback because temp use of notations/implicit *) + let fixdefs = + States.with_heavy_rollback (fun () -> + List.iter (declare_interning_data impls) notations; + List.map2 (interp_fix_body isevars env_rec impls) fixl fixtypes) + () in + + (* Instantiate evars and check all are resolved *) + let isevars,_ = consider_remaining_unif_problems env_rec !isevars in + let fixdefs = List.map (nf_evar (Evd.evars_of isevars)) fixdefs in + let fixtypes = List.map (nf_evar (Evd.evars_of isevars)) fixtypes in + List.iter (check_evars env_rec Evd.empty isevars) fixdefs; + check_mutuality env kind (List.combine fixnames fixdefs); + + (* Build the fix declaration block *) + let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in + let fixdecls = + match fixkind with + | IsFixpoint wfl -> + let fixwf = list_map3 compute_guardness_evidence wfl fixl fixtypes in + list_map_i (fun i _ -> mkFix ((Array.of_list fixwf,i),fixdecls)) 0 l + | IsCoFixpoint -> + list_map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 l in - States.unfreeze fs; - let (lnonrec,(namerec,defrec,arrec,_)) = - collect_non_rec env0 lrecnames recdef arityl [] in - 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 rec declare i fi = - let ce = - { const_entry_body = mkCoFix (i, recdecls); - const_entry_type = Some (arrec.(i)); - const_entry_opaque = false; - const_entry_boxed = boxed } - in - let kn = declare_constant fi (DefinitionEntry ce,IsDefinition CoFixpoint) - in (ConstRef kn) - in - let lrefrec = Array.mapi declare namerec in - if_verbose ppnl (corecursive_message lrefrec); - let var_subst id = (id, global_reference id) in - let _ = - List.fold_left - (fun subst (f,def,t) -> - let ce = { const_entry_body = replace_vars subst def; - const_entry_type = Some t; - const_entry_opaque = false; - const_entry_boxed = boxed } in - let _ = - declare_constant f (DefinitionEntry ce,IsDefinition Definition) in - warning ((string_of_id f)^" is non-recursively defined"); - (var_subst f) :: subst) - (List.map var_subst (Array.to_list namerec)) - lnonrec - in () + + (* Declare the recursive definitions *) + ignore (list_map3 (declare_fix boxed kind) fixnames fixdecls fixtypes); + if_verbose ppnl (recursive_message kind fixnames); + + (* Declare notations *) + List.iter (declare_interning_data ([],[])) notations + +let build_recursive l b = + let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in + let fixl = List.map (fun ((id,_,bl,typ,def),ntn) -> + ({fix_name = id; fix_binders = bl; fix_body = def; fix_type = typ},ntn)) + l in + interp_recursive (IsFixpoint g) fixl b + +let build_corecursive l b = + let fixl = List.map (fun ((id,bl,typ,def),ntn) -> + ({fix_name = id; fix_binders = bl; fix_body = def; fix_type = typ},ntn)) + l in + interp_recursive IsCoFixpoint fixl b + +(* 3d| Schemes *) let build_scheme lnamedepindsort = let lrecnames = List.map (fun ((_,f),_,_,_) -> f) lnamedepindsort @@ -637,8 +646,10 @@ let build_scheme lnamedepindsort = let kn = declare_constant fi (DefinitionEntry ce, IsDefinition Scheme) in ConstRef kn :: lrecref in - let lrecref = List.fold_right2 declare listdecl lrecnames [] in - if_verbose ppnl (recursive_message (Array.of_list lrecref)) + let _ = List.fold_right2 declare listdecl lrecnames [] in + if_verbose ppnl (recursive_message Fixpoint lrecnames) + +(* 4| Goal declaration *) let start_proof id kind c hook = let sign = Global.named_context () in diff --git a/toplevel/command.mli b/toplevel/command.mli index c93f69be..6f9a55c3 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: command.mli 7682 2005-12-21 15:06:11Z herbelin $ i*) +(*i $Id: command.mli 9110 2006-09-01 12:30:52Z herbelin $ i*) (*i*) open Util @@ -39,14 +39,14 @@ val syntax_definition : identifier -> constr_expr -> bool -> bool -> unit val declare_assumption : identifier located list -> coercion_flag -> assumption_kind -> local_binder list -> constr_expr -> unit -val build_mutual : inductive_expr list -> bool -> unit +val build_mutual : (inductive_expr * decl_notation) list -> bool -> unit val declare_mutual_with_eliminations : bool -> Entries.mutual_inductive_entry -> mutual_inductive val build_recursive : (fixpoint_expr * decl_notation) list -> bool -> unit -val build_corecursive : cofixpoint_expr list -> bool -> unit +val build_corecursive : (cofixpoint_expr * decl_notation) list -> bool -> unit val build_scheme : (identifier located * bool * reference * rawsort) list -> unit diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 6d65ccc2..3374b0ee 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqtop.ml 8932 2006-06-09 09:29:03Z notin $ *) +(* $Id: coqtop.ml 9191 2006-09-29 15:45:42Z courtieu $ *) open Pp open Util @@ -21,18 +21,16 @@ open Coqinit let get_version_date () = try - let ch = open_in (Coq_config.coqtop^"/make.result") in - let l = input_line ch in - let i = String.index l ' ' in - let j = String.index_from l (i+1) ' ' in - "checked out on "^(String.sub l (i+1) (j-i-1)) - with _ -> Coq_config.date + let ch = open_in (Coq_config.coqlib^"/revision") in + let ver = input_line ch in + let rev = input_line ch in + (ver,rev) + with _ -> (Coq_config.version,Coq_config.date) let print_header () = - Printf.printf "Welcome to Coq %s (%s)\n" - Coq_config.version - (get_version_date ()); - flush stdout + let (ver,rev) = (get_version_date ()) in + Printf.printf "Welcome to Coq %s (%s)\n" ver rev; + flush stdout let memory_stat = ref false @@ -249,6 +247,8 @@ let parse_args is_ide = | "-vm" :: rem -> use_vm := true; parse rem | "-emacs" :: rem -> Options.print_emacs := true; Pp.make_pp_emacs(); parse rem + | "-emacs-U" :: rem -> Options.print_emacs := true; + Options.print_emacs_safechar := true; Pp.make_pp_emacs(); parse rem | "-where" :: _ -> print_endline (getenv_else "COQLIB" Coq_config.coqlib); exit 0 diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index c011ba52..63a6ad07 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: discharge.ml 8845 2006-05-23 07:41:58Z herbelin $ *) +(* $Id: discharge.ml 9310 2006-10-28 19:35:09Z 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 (Termops.refresh_universes (Inductive.type_of_inductive (mib,mip))) in + let arity = expmod_constr modlist (Termops.refresh_universes (Inductive.type_of_inductive (Global.env()) (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 73aaef30..b8e9eeda 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: himsg.ml 8845 2006-05-23 07:41:58Z herbelin $ *) +(* $Id: himsg.ml 9217 2006-10-05 17:31:23Z notin $ *) open Pp open Util @@ -385,6 +385,14 @@ let explain_cannot_unify m n = str"Impossible to unify" ++ brk(1,1) ++ pm ++ spc () ++ str"with" ++ brk(1,1) ++ pn +let explain_cannot_unify_local env m n subn = + let pm = pr_lconstr m in + let pn = pr_lconstr n in + let psubn = pr_lconstr_env env subn in + str"Impossible to unify" ++ brk(1,1) ++ pm ++ spc () ++ + str"with" ++ brk(1,1) ++ pn ++ spc() ++ str"as" ++ brk(1,1) ++ + psubn ++ str" contains local variables" + let explain_refiner_cannot_generalize ty = str "Cannot find a well-typed generalisation of the goal with type : " ++ pr_lconstr ty @@ -455,6 +463,7 @@ let explain_pretype_error ctx err = | NotProduct c -> explain_not_product ctx c | CannotUnify (m,n) -> explain_cannot_unify m n + | CannotUnifyLocal (e,m,n,sn) -> explain_cannot_unify_local e m n sn | CannotGeneralize ty -> explain_refiner_cannot_generalize ty | NoOccurrenceFound c -> explain_no_occurrence_found c | CannotUnifyBindingType (m,n) -> explain_cannot_unify_binding_type m n diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 92ce6e36..3dcb1f58 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: metasyntax.ml 7822 2006-01-08 17:14:56Z herbelin $ *) +(* $Id: metasyntax.ml 9333 2006-11-02 13:59:14Z barras $ *) open Pp open Util @@ -50,7 +50,7 @@ let make_terminal_status = function let rec make_tags lev = function | VTerm s :: l -> make_tags lev l | VNonTerm (loc, nt, po) :: l -> - let (etyp, _) = Egrammar.interp_entry_name lev "tactic" nt in + let (etyp, _) = Egrammar.interp_entry_name lev nt in etyp :: make_tags lev l | [] -> [] @@ -112,6 +112,8 @@ let print_grammar univ = function | "tactic" -> msgnl (str "Entry tactic_expr is"); Gram.Entry.print Pcoq.Tactic.tactic_expr; + msgnl (str "Entry binder_tactic is"); + Gram.Entry.print Pcoq.Tactic.binder_tactic; msgnl (str "Entry simple_tactic is"); Gram.Entry.print Pcoq.Tactic.simple_tactic; | "vernac" -> @@ -399,6 +401,10 @@ let is_operator s = s.[0] = '-' or s.[0] = '/' or s.[0] = '<' or s.[0] = '>' or s.[0] = '@' or s.[0] = '\\' or s.[0] = '&' or s.[0] = '~') +let is_prod_ident = function + | Terminal s when is_letter s.[0] or s.[0] = '_' -> true + | _ -> false + let rec is_non_terminal = function | NonTerminal _ | SProdList _ -> true | _ -> false @@ -437,10 +443,11 @@ let make_hunks etyps symbols from = else UnpTerminal s :: add_break 1 (make NoBreak prods) else if is_ident_tail s.[String.length s - 1] then + let sep = if is_prod_ident (List.hd prods) then "" else " " in if ws = CanBreak then - add_break 1 (UnpTerminal (s^" ") :: make CanBreak prods) + add_break 1 (UnpTerminal (s^sep) :: make CanBreak prods) else - UnpTerminal (s^" ") :: make CanBreak prods + UnpTerminal (s^sep) :: make CanBreak prods else if ws = CanBreak then add_break 1 (UnpTerminal (s^" ") :: make CanBreak prods) else diff --git a/toplevel/record.ml b/toplevel/record.ml index 9eeeb51e..bf0271d9 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: record.ml 8875 2006-05-29 19:59:11Z msozeau $ *) +(* $Id: record.ml 9082 2006-08-24 17:03:28Z herbelin $ *) open Pp open Util @@ -192,7 +192,6 @@ let declare_projections indsp coers fields = list telling if the corresponding fields must me declared as coercion *) let definition_structure ((is_coe,(_,idstruc)),ps,cfs,idbuild,s) = let coers,fs = List.split cfs in - let nparams = local_binders_length ps in let extract_name acc = function Vernacexpr.AssumExpr((_,Name id),_) -> id::acc | Vernacexpr.DefExpr ((_,Name id),_,_) -> id::acc @@ -219,4 +218,4 @@ let definition_structure ((is_coe,(_,idstruc)),ps,cfs,idbuild,s) = let kinds,sp_projs = declare_projections rsp coers fields in let build = ConstructRef (rsp,1) in (* This is construct path of idbuild *) if is_coe then Class.try_add_new_coercion build Global; - Recordops.declare_structure(rsp,idbuild,nparams,List.rev kinds,List.rev sp_projs) + Recordops.declare_structure(rsp,idbuild,List.rev kinds,List.rev sp_projs) diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index 95c1b7d9..439e9254 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: toplevel.ml 8748 2006-04-27 16:01:26Z courtieu $ *) +(* $Id: toplevel.ml 9252 2006-10-20 14:22:41Z herbelin $ *) open Pp open Util @@ -48,11 +48,19 @@ let resynch_buffer ibuf = | _ -> () -(* Read a char in an input channel, displaying a prompt at every - beginning of line. *) +(* 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. *) + +let emacs_prompt_startstring() = + if !Options.print_emacs_safechar then "<prompt>" else "" -let emacs_prompt_endstring = String.make 1 (Char.chr 249) +let emacs_prompt_endstring() = + if !Options.print_emacs_safechar then "</prompt>" + else String.make 1 (Char.chr 249) +(* Read a char in an input channel, displaying a prompt at every + beginning of line. *) let prompt_char ic ibuf count = let bol = match ibuf.bols with | ll::_ -> ibuf.len == ll @@ -128,6 +136,7 @@ let print_highlight_location ib loc = str sn ++ str dn) in (l1 ++ li ++ ln) in + let loc = make_loc (bp,ep) in (str"Toplevel input, characters " ++ Cerrors.print_loc loc ++ fnl () ++ highlight_lines ++ fnl ()) @@ -214,14 +223,16 @@ 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 ^ " < " ^ emacs_prompt_endstring + 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", * or after a Drop. *) let top_buffer = let pr() = - make_prompt() ^ Printer.emacs_str (make_emacs_prompt()) + Printer.emacs_str (emacs_prompt_startstring()) + ^ make_prompt() + ^ Printer.emacs_str (make_emacs_prompt()) in { prompt = pr; str = ""; @@ -232,7 +243,10 @@ let top_buffer = let set_prompt prompt = top_buffer.prompt - <- (fun () -> (prompt ())^(Printer.emacs_str (String.make 1 (Char.chr 249)))) + <- (fun () -> + Printer.emacs_str (emacs_prompt_startstring()) + ^ prompt () + ^ Printer.emacs_str (emacs_prompt_endstring())) (* Removes and prints the location of the error. The following exceptions need not be located. *) diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index afe72f0f..710b814d 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: vernac.ml 8924 2006-06-08 17:49:01Z notin $ *) +(* $Id: vernac.ml 9133 2006-09-12 14:52:07Z notin $ *) (* Parsing of vernacular. *) @@ -162,12 +162,12 @@ let rec vernac_com interpfun (loc,com) = | v -> if not !just_parsing then interpfun v in - try - if do_translate () then pr_new_syntax loc (Some com); - interp com - with e -> - Format.set_formatter_out_channel stdout; - raise (DuringCommandInterp (loc, e)) + try + if do_translate () then pr_new_syntax loc (Some com); + interp com + with e -> + Format.set_formatter_out_channel stdout; + raise (DuringCommandInterp (loc, e)) and vernac interpfun input = vernac_com interpfun (parse_phrase input) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index d384541f..35d202d9 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 9017 2006-07-05 17:27:34Z herbelin $ i*) +(*i $Id: vernacentries.ml 9304 2006-10-28 09:58:16Z herbelin $ i*) (* Concrete syntax of the mathematical vernacular MV V2.6 *) @@ -20,6 +20,7 @@ open Term open Pfedit open Tacmach open Proof_trees +open Decl_mode open Constrintern open Prettyp open Printer @@ -93,7 +94,10 @@ let show_script () = let pts = get_pftreestate () in let pf = proof_of_pftreestate pts and evc = evc_of_pftreestate pts in - msgnl (print_treescript true evc (Global.named_context()) pf) + msgnl (print_treescript true evc pf) + +let show_thesis () = + msgnl (anomaly "TODO" ) let show_top_evars () = let pfts = get_pftreestate () in @@ -111,39 +115,19 @@ let print_subgoals () = if_verbose (fun () -> msg (pr_open_subgoals ())) () (* Simulate the Intro(s) tactic *) -let fresh_id_of_name avoid gl = function - Anonymous -> Tactics.fresh_id avoid (id_of_string "H") gl - | Name id -> Tactics.fresh_id avoid id gl - -let rec do_renum avoid gl = function - [] -> mt () - | [n] -> pr_id (fresh_id_of_name avoid gl n) - | n :: l -> - let id = fresh_id_of_name avoid gl n in - pr_id id ++ spc () ++ do_renum (id :: avoid) gl l - -(* Transforms a product term (x1:T1)..(xn:Tn)T into the pair - ([(xn,Tn);...;(x1,T1)],T), where T is not a product nor a letin *) -let decompose_prod_letins = - let rec prodec_rec l c = match kind_of_term c with - | Prod (x,t,c) -> prodec_rec ((x,t)::l) c - | LetIn (x,b,t,c) -> prodec_rec ((x,t)::l) c - | Cast (c,_,_) -> prodec_rec l c - | _ -> l,c - in - prodec_rec [] - let show_intro all = let pf = get_pftreestate() in let gl = nth_goal_of_pftreestate 1 pf in - let l,_= decompose_prod_letins (strip_outer_cast (pf_concl gl)) in - let nl = List.rev_map fst l in - if all then msgnl (hov 0 (do_renum [] gl nl)) - else try - let n = List.hd nl in - msgnl (pr_id (fresh_id_of_name [] gl n)) - with Failure "hd" -> message "" - + let l,_= Sign.decompose_prod_assum (strip_outer_cast (pf_concl gl)) in + if all + then + let lid = Tactics.find_intro_names l gl in + msgnl (hov 0 (prlist_with_sep spc pr_id lid)) + else + try + let n = list_last l in + 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" @@ -508,15 +492,14 @@ let vernac_end_section = Lib.close_section let vernac_end_segment id = check_no_pending_proofs (); - let o = - try Lib.what_is_opened () - with Not_found -> error "There is nothing to end." in - match o with - | _,Lib.OpenedModule (export,_,_) -> vernac_end_module export id - | _,Lib.OpenedModtype _ -> vernac_end_modtype id - | _,Lib.OpenedSection _ -> vernac_end_section id - | _ -> anomaly "No more opened things" - + let o = try Lib.what_is_opened () with + Not_found -> error "There is nothing to end." in + match o with + | _,Lib.OpenedModule (export,_,_) -> vernac_end_module export id + | _,Lib.OpenedModtype _ -> vernac_end_modtype id + | _,Lib.OpenedSection _ -> vernac_end_section id + | _ -> anomaly "No more opened things" + let vernac_require import _ qidl = let qidl = List.map qualid_of_reference qidl in Library.require_library qidl import @@ -553,6 +536,7 @@ let vernac_identity_coercion stre id qids qidt = 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 ())) @@ -563,7 +547,7 @@ let vernac_solve n tcom b = if subtree_solved () then begin Options.if_verbose msgnl (str "Subgoal proved"); make_focus 0; - reset_top_of_tree () + reset_top_of_script () end; print_subgoals(); if !pcoq <> None then (out_some !pcoq).solve n @@ -580,8 +564,35 @@ let vernac_set_end_tac tac = if not (refining ()) then error "Unknown command of the non proof-editing mode"; 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*) - + (* 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 () + (*****************************) (* Auxiliary file management *) @@ -789,6 +800,14 @@ let _ = optread=Pp_control.get_margin; optwrite=Pp_control.set_margin } +let _ = + declare_bool_option + { optsync=true; + optkey=SecondaryTable("Printing","Universes"); + optname="the printing of universes"; + optread=(fun () -> !Constrextern.print_universes); + optwrite=(fun b -> Constrextern.print_universes:=b) } + let vernac_debug b = set_debug (if b then Tactic_debug.DebugOn 0 else Tactic_debug.DebugOff) @@ -1009,18 +1028,21 @@ let vernac_backtrack snum pnum naborts = for i = 1 to naborts do vernac_abort None done; undo_todepth pnum; vernac_backto snum; + Pp.flush_all(); (* there may be no proof in progress, even if no abort *) (try print_subgoals () with UserError _ -> ()) - (* Est-ce normal que "Focus" ne semble pas se comporter comme "Focus 1" ? *) -let vernac_focus = function - | None -> traverse_nth_goal 1; print_subgoals () - | Some n -> traverse_nth_goal n; print_subgoals () - +let vernac_focus gln = + check_not_proof_mode "No focussing or Unfocussing in Proof Mode."; + match gln with + | None -> traverse_nth_goal 1; print_subgoals () + | Some n -> traverse_nth_goal n; print_subgoals () + (* Reset the focus to the top of the tree *) let vernac_unfocus () = - make_focus 0; reset_top_of_tree (); print_subgoals () + 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() @@ -1039,7 +1061,7 @@ let apply_subproof f occ = f evc (Global.named_context()) pf let explain_proof occ = - msg (apply_subproof (print_treescript true) occ) + msg (apply_subproof (fun evd _ -> print_treescript true evd) occ) let explain_tree occ = msg (apply_subproof print_proof occ) @@ -1063,9 +1085,11 @@ let vernac_show = function msgnl (prlist_with_sep pr_spc pr_id (Pfedit.get_all_proof_names())) | 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 @@ -1130,6 +1154,14 @@ let interp c = match c with | 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 diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 972d7ed9..9d514622 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: vernacexpr.ml 9017 2006-07-05 17:27:34Z herbelin $ i*) +(*i $Id: vernacexpr.ml 9154 2006-09-20 17:18:18Z corbinea $ i*) open Util open Names @@ -99,6 +99,7 @@ type showable = | ShowProofNames | ShowIntros of bool | ShowMatch of lident + | ShowThesis | ExplainProof of int list | ExplainTree of int list @@ -146,8 +147,7 @@ type simple_binder = lident list * constr_expr type 'a with_coercion = coercion_flag * 'a type constructor_expr = (lident * constr_expr) with_coercion type inductive_expr = - lident * decl_notation * local_binder list * constr_expr - * constructor_expr list + lident * local_binder list * constr_expr * constructor_expr list type definition_expr = | ProveBody of local_binder list * constr_expr | DefineBody of local_binder list * raw_red_expr option * constr_expr @@ -195,9 +195,9 @@ type vernac_expr = | VernacEndProof of proof_end | VernacExactProof of constr_expr | VernacAssumption of assumption_kind * simple_binder with_coercion list - | VernacInductive of inductive_flag * inductive_expr list + | VernacInductive of inductive_flag * (inductive_expr * decl_notation) list | VernacFixpoint of (fixpoint_expr * decl_notation) list * bool - | VernacCoFixpoint of cofixpoint_expr list * bool + | VernacCoFixpoint of (cofixpoint_expr * decl_notation) list * bool | VernacScheme of (lident * bool * lreference * sort_expr) list (* Gallina extensions *) @@ -223,9 +223,17 @@ type vernac_expr = module_binder list * module_type_ast option (* Solving *) + | VernacSolve of int * raw_tactic_expr * bool | VernacSolveExistential of int * constr_expr + (* Proof Mode *) + + | VernacDeclProof + | VernacReturn + | VernacProofInstr of Decl_expr.raw_proof_instr + + (* Auxiliary file and library management *) | VernacRequireFrom of export_flag option * specif_flag option * lstring | VernacAddLoadPath of rec_flag * lstring * dir_path option |