From e4282ea99c664d8d58067bee199cbbcf881b60d5 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sat, 4 Jul 2009 13:28:35 +0200 Subject: Imported Upstream version 8.2.pl1+dfsg --- toplevel/classes.ml | 26 +++++++++++++++++++++++--- toplevel/command.ml | 26 ++++++++++++++------------ toplevel/command.mli | 6 +++--- toplevel/himsg.ml | 6 +++--- toplevel/record.ml | 4 ++-- toplevel/vernacentries.ml | 17 +++++------------ toplevel/vernacexpr.ml | 4 ++-- 7 files changed, 52 insertions(+), 37 deletions(-) (limited to 'toplevel') diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 04945040..1a1640a4 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: classes.ml 11800 2009-01-18 18:34:15Z msozeau $ i*) +(*i $Id: classes.ml 12187 2009-06-13 19:36:59Z msozeau $ i*) (*i*) open Names @@ -264,6 +264,14 @@ 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 env = Global.env() in let evars = ref (Evd.create_evar_defs Evd.empty) in @@ -273,6 +281,14 @@ let context ?(hook=fun _ -> ()) l = List.iter (fun (n, b, t) -> Option.iter ce b; ce t) fullctx; let ctx = try named_of_rel_context fullctx with _ -> error "Anonymous variables not allowed in contexts." + in + let env = push_named_context ctx env in + let keeps = + List.fold_left (fun acc (id,_,t) -> + match class_of_constr t with + | None -> acc + | Some _ -> List.map pi1 (keep_hyps env (Idset.singleton id)) :: acc) + [] ctx in List.iter (function (id,_,t) -> if Lib.is_modtype () then @@ -285,10 +301,14 @@ let context ?(hook=fun _ -> ()) l = hook (ConstRef cst) | None -> () else ( - let impl = List.exists (fun (x,_) -> match x with ExplByPos (_, Some id') -> id = id' | _ -> false) impls + let impl = List.exists (fun (x,_) -> + match x with ExplByPos (_, Some id') -> id = id' | _ -> false) impls + and keep = + let l = list_filter_map (fun ids -> if List.mem id ids then Some ids else None) keeps in + List.concat l in Command.declare_one_assumption false (Local (* global *), Definitional) t - [] impl (* implicit *) true (* always kept *) false (* inline *) (dummy_loc, id); + [] impl (* implicit *) keep (* always kept *) false (* inline *) (dummy_loc, id); match class_of_constr t with | None -> () | Some tc -> hook (VarRef id))) diff --git a/toplevel/command.ml b/toplevel/command.ml index b50c9bbd..05a22829 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: command.ml 11745 2009-01-04 18:43:08Z herbelin $ *) +(* $Id: command.ml 12187 2009-06-13 19:36:59Z msozeau $ *) open Pp open Util @@ -546,7 +546,7 @@ let interp_mutual paramsl indl notations finite = let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in let constructors = - States.with_heavy_rollback (fun () -> + States.with_state_protection (fun () -> (* Temporary declaration of notations and scopes *) List.iter (declare_interning_data impls) notations; (* Interpret the constructor types *) @@ -851,7 +851,7 @@ let interp_recursive fixkind l boxed = (* Interp bodies with rollback because temp use of notations/implicit *) let fixdefs = - States.with_heavy_rollback (fun () -> + States.with_state_protection (fun () -> List.iter (declare_interning_data impls) notations; list_map3 (interp_fix_body evdref env_rec impls) fixctxs fixl fixccls) () in @@ -1012,16 +1012,18 @@ let build_combined_scheme name schemes = let (ctx, arity) = decompose_prod ty in let (_, last) = List.hd ctx in match kind_of_term last with - | App (ind, args) -> ctx, destInd ind, Array.length args + | App (ind, args) -> + let ind = destInd ind in + let (_,spec) = Inductive.lookup_mind_specif env ind in + ctx, ind, spec.mind_nrealargs | _ -> ctx, destInd last, 0 in let defs = List.map (fun x -> let refe = Ident x in let qualid = qualid_of_reference refe in - let cst = try - Nametab.locate_constant (snd qualid) - with Not_found -> error ((string_of_qualid (snd qualid))^" is not declared.") + let cst = try Nametab.locate_constant (snd qualid) + with Not_found -> error ((string_of_qualid (snd qualid))^" is not declared.") in let ty = Typeops.type_of_constant env cst in qualid, cst, ty) @@ -1087,9 +1089,9 @@ let save_remaining_recthms (local,kind) body opaq i (id,(t_i,imps)) = | None -> (match local with | Local -> - let impl=false and keep=false in (* copy values from Vernacentries *) + let impl=false in (* copy values from Vernacentries *) let k = IsAssumption Conjectural in - let c = SectionLocalAssum (t_i,impl,keep) in + let c = SectionLocalAssum (t_i,impl,[]) in let _ = declare_variable id (Lib.cwd(),c,k) in (Local,VarRef id,imps) | Global -> @@ -1123,9 +1125,9 @@ let look_for_mutual_statements thms = let n = List.length thms in let inds = List.map (fun (id,(t,_) as x) -> let (hyps,ccl) = Sign.decompose_prod_assum t in - let whnf_hyp_hds = map_rel_context_with_binders - (fun i c -> fst (whd_betadeltaiota_stack (Global.env()) Evd.empty (lift i c))) - hyps in + let whnf_hyp_hds = fold_map_rel_context + (fun env c -> fst (whd_betadeltaiota_stack env Evd.empty c)) + (Global.env()) hyps in let ind_hyps = List.flatten (list_map_i (fun i (_,b,t) -> match kind_of_term t with diff --git a/toplevel/command.mli b/toplevel/command.mli index b42fafd0..36399029 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 11745 2009-01-04 18:43:08Z herbelin $ i*) +(*i $Id: command.mli 12187 2009-06-13 19:36:59Z msozeau $ i*) (*i*) open Util @@ -45,13 +45,13 @@ val syntax_definition : identifier -> identifier list * constr_expr -> val declare_one_assumption : coercion_flag -> assumption_kind -> Term.types -> Impargs.manual_explicitation list -> - bool (* implicit *) -> bool (* keep *) -> bool (* inline *) -> Names.variable located -> unit + bool (* implicit *) -> identifier list (* keep *) -> bool (* inline *) -> Names.variable located -> unit val set_declare_assumption_hook : (types -> unit) -> unit val declare_assumption : identifier located list -> coercion_flag -> assumption_kind -> local_binder list -> constr_expr -> - bool -> bool -> bool -> unit + bool -> identifier list -> bool -> unit val declare_interning_data : 'a * Constrintern.implicits_env -> string * Topconstr.constr_expr * Topconstr.scope_name option -> unit diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index f733a3d5..0cda7c71 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: himsg.ml 11784 2009-01-14 11:36:32Z herbelin $ *) +(* $Id: himsg.ml 11986 2009-03-17 11:44:20Z herbelin $ *) open Pp open Util @@ -814,8 +814,8 @@ let explain_ltac_call_trace (last,trace,loc) = (if unboundvars <> [] or vars <> [] then strbrk " (with " ++ prlist_with_sep pr_coma (fun (id,c) -> pr_id id ++ str ":=" ++ Printer.pr_lconstr c) - (List.rev vars @ unboundvars) - else mt()) ++ str ")" in + (List.rev vars @ unboundvars) ++ str ")" + else mt()) in if calls <> [] then let kind_of_last_call = match list_last calls with | Proof_type.LtacConstrInterp _ -> ", last term evaluation failed." diff --git a/toplevel/record.ml b/toplevel/record.ml index 4a2ef7db..4c0e34cd 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: record.ml 11809 2009-01-20 11:39:55Z aspiwack $ *) +(* $Id: record.ml 12080 2009-04-11 16:56:20Z herbelin $ *) open Pp open Util @@ -366,7 +366,7 @@ let definition_structure (kind,finite,(is_coe,(loc,idstruc)),ps,cfs,idbuild,s) = (* Now, younger decl in params and fields is on top *) let sc = Option.map mkSort s in let implpars, params, implfs, fields = - States.with_heavy_rollback (fun () -> + States.with_state_protection (fun () -> typecheck_params_and_fields idstruc sc ps notations fs) () in match kind with diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index c95c89d3..6a0acb52 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 11809 2009-01-20 11:39:55Z aspiwack $ i*) +(*i $Id: vernacentries.ml 12187 2009-06-13 19:36:59Z msozeau $ i*) (* Concrete syntax of the mathematical vernacular MV V2.6 *) @@ -373,7 +373,7 @@ let vernac_assumption kind l nl= List.iter (fun lid -> if global then Dumpglob.dump_definition lid false "ax" else Dumpglob.dump_definition lid true "var") idl; - declare_assumption idl is_coe kind [] c false false nl) l + declare_assumption idl is_coe kind [] c false [] nl) l let vernac_record k finite struc binders sort nameopt cfs = let const = match nameopt with @@ -807,14 +807,6 @@ let _ = optread = Impargs.is_implicit_args; optwrite = Impargs.make_implicit_args } -let _ = - declare_bool_option - { optsync = true; - optname = "manual implicit arguments"; - optkey = (TertiaryTable ("Manual","Implicit","Arguments")); - optread = Impargs.is_manual_implicit_args; - optwrite = Impargs.make_manual_implicit_args } - let _ = declare_bool_option { optsync = true; @@ -1110,9 +1102,10 @@ let vernac_print = function | PrintAbout qid -> msgnl (print_about qid) | PrintImplicit qid -> msg (print_impargs qid) (*spiwack: prints all the axioms and section variables used by a term *) - | PrintAssumptions r -> + | PrintAssumptions (o,r) -> let cstr = constr_of_global (global_with_alias r) in - let nassumptions = Environ.assumptions cstr (Global.env ()) in + let nassumptions = Environ.assumptions (Conv_oracle.get_transp_state ()) + ~add_opaque:o cstr (Global.env ()) in msg (Printer.pr_assumptionset (Global.env ()) nassumptions) let global_module r = diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 3e9dfb25..4da16ea7 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 11809 2009-01-20 11:39:55Z aspiwack $ i*) +(*i $Id: vernacexpr.ml 12187 2009-06-13 19:36:59Z msozeau $ i*) open Util open Names @@ -65,7 +65,7 @@ type printable = | PrintVisibility of string option | PrintAbout of reference | PrintImplicit of reference - | PrintAssumptions of reference + | PrintAssumptions of bool * reference type search_about_item = | SearchSubPattern of constr_pattern_expr -- cgit v1.2.3