From 420f78b2caeaaddc6fe484565b2d0e49c66888e5 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sun, 27 Jul 2014 10:02:38 +0200 Subject: Imported Upstream version 8.4pl4dfsg --- pretyping/arguments_renaming.ml | 2 +- pretyping/arguments_renaming.mli | 2 +- pretyping/cases.ml | 6 +++--- pretyping/cases.mli | 2 +- pretyping/cbv.ml | 2 +- pretyping/cbv.mli | 2 +- pretyping/classops.ml | 2 +- pretyping/classops.mli | 2 +- pretyping/coercion.ml | 24 ++++++++++++---------- pretyping/coercion.mli | 20 +++++++++++-------- pretyping/detyping.ml | 2 +- pretyping/detyping.mli | 2 +- pretyping/evarconv.ml | 20 ++++++++++++++++++- pretyping/evarconv.mli | 2 +- pretyping/evarutil.ml | 37 ++++++++++++++++++++++++---------- pretyping/evarutil.mli | 2 +- pretyping/evd.ml | 2 +- pretyping/evd.mli | 2 +- pretyping/glob_term.ml | 23 +-------------------- pretyping/glob_term.mli | 2 +- pretyping/indrec.ml | 2 +- pretyping/indrec.mli | 2 +- pretyping/inductiveops.ml | 2 +- pretyping/inductiveops.mli | 2 +- pretyping/matching.ml | 2 +- pretyping/matching.mli | 2 +- pretyping/namegen.ml | 2 +- pretyping/namegen.mli | 2 +- pretyping/pattern.ml | 2 +- pretyping/pattern.mli | 2 +- pretyping/pretype_errors.ml | 2 +- pretyping/pretype_errors.mli | 2 +- pretyping/pretyping.ml | 43 ++++++++++++++++++++++------------------ pretyping/pretyping.mli | 6 +++--- pretyping/recordops.ml | 2 +- pretyping/recordops.mli | 2 +- pretyping/reductionops.ml | 2 +- pretyping/reductionops.mli | 2 +- pretyping/retyping.ml | 2 +- pretyping/retyping.mli | 2 +- pretyping/tacred.ml | 2 +- pretyping/tacred.mli | 2 +- pretyping/term_dnet.ml | 2 +- pretyping/term_dnet.mli | 2 +- pretyping/termops.ml | 2 +- pretyping/termops.mli | 2 +- pretyping/typeclasses.ml | 2 +- pretyping/typeclasses.mli | 2 +- pretyping/typeclasses_errors.ml | 2 +- pretyping/typeclasses_errors.mli | 2 +- pretyping/typing.ml | 2 +- pretyping/typing.mli | 2 +- pretyping/unification.ml | 4 ++-- pretyping/unification.mli | 2 +- pretyping/vnorm.ml | 2 +- pretyping/vnorm.mli | 2 +- 56 files changed, 151 insertions(+), 126 deletions(-) (limited to 'pretyping') diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml index 92378837..78290e03 100644 --- a/pretyping/arguments_renaming.ml +++ b/pretyping/arguments_renaming.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* - let (evd',j) = Coercion.inh_conv_coerce_to loc env !evdref j p in + let (evd',j) = Coercion.inh_conv_coerce_to true loc env !evdref j p in evdref := evd'; j | None -> j diff --git a/pretyping/cases.mli b/pretyping/cases.mli index 566c172d..826d68a4 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* evar_map -> unsafe_judgment -> evar_map * unsafe_judgment + bool -> env -> evar_map -> unsafe_judgment -> evar_map * unsafe_judgment (* [inh_coerce_to_sort env evd j] coerces [j] to a type; i.e. it inserts a coercion into [j], if needed, in such a way it gets as @@ -57,10 +57,10 @@ module type S = sig (* [inh_conv_coerce_to loc env evd j t] coerces [j] to an object of type [t]; i.e. it inserts a coercion into [j], if needed, in such a way [t] and [j.uj_type] are convertible; it fails if no coercion is applicable *) - val inh_conv_coerce_to : loc -> + val inh_conv_coerce_to : bool -> loc -> env -> evar_map -> unsafe_judgment -> type_constraint_type -> evar_map * unsafe_judgment - val inh_conv_coerce_rigid_to : loc -> + val inh_conv_coerce_rigid_to : bool -> loc -> env -> evar_map -> unsafe_judgment -> type_constraint_type -> evar_map * unsafe_judgment (* [inh_conv_coerces_to loc env evd t t'] checks if an object of type [t] @@ -140,9 +140,11 @@ module Default = struct lookup_path_to_fun_from env evd j.uj_type in (evd,apply_coercion env evd p j t) - let inh_app_fun env evd j = + let inh_app_fun resolve_tc env evd j = try inh_app_fun env evd j - with Not_found -> + with + | Not_found when not resolve_tc -> (evd, j) + | Not_found -> try inh_app_fun env (saturate_evd env evd) j with Not_found -> (evd, j) @@ -221,13 +223,15 @@ module Default = struct | _ -> raise NoCoercion (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *) - let inh_conv_coerce_to_gen rigidonly loc env evd cj (n, t) = + let inh_conv_coerce_to_gen resolve_tc rigidonly loc env evd cj (n, t) = match n with None -> let (evd', val') = try inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t - with NoCoercion -> + with + | NoCoercion when not resolve_tc -> error_actual_type_loc loc env evd cj t + | NoCoercion -> let evd = saturate_evd env evd in try inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t @@ -238,8 +242,8 @@ module Default = struct (evd',{ uj_val = val'; uj_type = t }) | Some (init, cur) -> (evd, cj) - let inh_conv_coerce_to = inh_conv_coerce_to_gen false - let inh_conv_coerce_rigid_to = inh_conv_coerce_to_gen true + let inh_conv_coerce_to resolve_tc = inh_conv_coerce_to_gen resolve_tc false + let inh_conv_coerce_rigid_to resolve_tc = inh_conv_coerce_to_gen resolve_tc true let inh_conv_coerces_to loc env (evd : evar_map) t (abs, t') = diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli index 4c4725b3..f06f58f4 100644 --- a/pretyping/coercion.mli +++ b/pretyping/coercion.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* evar_map -> unsafe_judgment -> evar_map * unsafe_judgment + bool -> env -> evar_map -> unsafe_judgment -> evar_map * unsafe_judgment (** [inh_coerce_to_sort env isevars j] coerces [j] to a type; i.e. it inserts a coercion into [j], if needed, in such a way it gets as @@ -40,13 +42,15 @@ module type S = sig val inh_coerce_to_prod : loc -> env -> evar_map -> type_constraint_type -> evar_map * type_constraint_type - (** [inh_conv_coerce_to loc env isevars j t] coerces [j] to an object of type + (** [inh_conv_coerce_to resolve_tc loc env isevars j t] coerces [j] to an object of type [t]; i.e. it inserts a coercion into [j], if needed, in such a way [t] and - [j.uj_type] are convertible; it fails if no coercion is applicable *) - val inh_conv_coerce_to : loc -> + [j.uj_type] are convertible; it fails if no coercion is applicable. + resolve_tc=false disables resolving type classes (as the last + resort before failing) *) + val inh_conv_coerce_to : bool -> loc -> env -> evar_map -> unsafe_judgment -> type_constraint_type -> evar_map * unsafe_judgment - val inh_conv_coerce_rigid_to : loc -> + val inh_conv_coerce_rigid_to : bool -> loc -> env -> evar_map -> unsafe_judgment -> type_constraint_type -> evar_map * unsafe_judgment (** [inh_conv_coerces_to loc env isevars t t'] checks if an object of type [t] diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 1065aec9..9e808dd4 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* !debug_unification); + Goptions.optwrite = (fun a -> debug_unification:=a); +} + + type flex_kind_of_term = | Rigid of constr | PseudoRigid of constr (* approximated as rigid but not necessarily so *) @@ -210,6 +221,13 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) in (* Evar must be undefined since we have flushed evars *) + let () = if !debug_unification then + let open Pp in + let pr_state (tm,l) = + h 0 (Termops.print_constr tm ++ str "|" ++ cut () + ++ prlist_with_sep pr_semicolon + (fun x -> hov 1 (Termops.print_constr x)) l) in + pp (v 0 (pr_state appr1 ++ cut () ++ pr_state appr2 ++ cut ()) ++ fnl ()) in match (flex_kind_of_term term1 l1, flex_kind_of_term term2 l2) with | Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) -> let f1 i = diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index dd68f16f..3a352d13 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* candidates + | Some filter -> + let ids = List.map pi1 (list_filter_with filter (evar_context evi)) in + List.filter (fun a -> list_subset (Idset.elements (collect_vars a)) ids) + candidates + +let filter_candidates evd evk filter candidates_update = let evi = Evd.find_undefined evd evk in - let candidates = match candidates with + let candidates = match candidates_update with | None -> evi.evar_candidates - | Some _ -> candidates in - match candidates,filter with - | None,_ | _, None -> candidates - | Some l, Some filter -> - let ids = List.map pi1 (list_filter_with filter (evar_context evi)) in - Some (List.filter (fun a -> - list_subset (Idset.elements (collect_vars a)) ids) l) + | Some _ -> candidates_update + in + match candidates with + | None -> None + | Some l -> + let l' = filter_effective_candidates evi filter l in + if List.length l = List.length l' && candidates_update = None then + None + else + Some l' let closure_of_filter evd evk filter = let evi = Evd.find_undefined evd evk in @@ -1530,6 +1541,7 @@ let solve_candidates conv_algo env evd (evk,argsv as ev) rhs = exception NotInvertibleUsingOurAlgorithm of constr exception NotEnoughInformationToProgress of (identifier * evar_projection) list +exception NotEnoughInformationEvarEvar of constr exception OccurCheckIn of evar_map * constr let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs = @@ -1608,7 +1620,8 @@ let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs = with | EvarSolvedOnTheFly (evd,t) -> evdref:=evd; imitate envk t | CannotProject filter' -> - assert !progress; + if not !progress then + raise (NotEnoughInformationEvarEvar t); (* Make the virtual left evar real *) let ty = get_type_of env' !evdref t in let (evd,evar'',ev'') = @@ -1714,6 +1727,8 @@ and evar_define conv_algo ?(choose=false) env evd (evk,argsv as ev) rhs = with | NotEnoughInformationToProgress sols -> postpone_non_unique_projection env evd ev sols rhs + | NotEnoughInformationEvarEvar t -> + add_conv_pb (Reduction.CONV,env,mkEvar ev,t) evd | NotInvertibleUsingOurAlgorithm t -> error_not_clean env evd evk t (evar_source evk evd) | OccurCheckIn (evd,rhs) -> diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 591a008c..9269f138 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* Anonymous -> - (* Unable to manage the presence of both an alias and a variable *) - raise Not_found - | GVar (loc,id) -> PatVar (loc,Name id) - | GHole (loc,_) -> PatVar (loc,na) - | GRef (loc,ConstructRef cstr) -> - PatCstr (loc,cstr,[],na) - | GApp (loc,GRef (_,ConstructRef (ind,_ as cstr)),args) -> - let mib,_ = Global.lookup_inductive ind in - let nparams = mib.Declarations.mind_nparams in - if nparams > List.length args then - user_err_loc (loc,"",Pp.str "Invalid notation for pattern."); - let params,args = list_chop nparams args in - List.iter (function GHole _ -> () - | _ -> user_err_loc (loc,"",Pp.str"Invalid notation for pattern.")) - params; - let args = List.map (cases_pattern_of_glob_constr Anonymous) args in - PatCstr (loc,cstr,args,na) - | _ -> raise Not_found - let rec cases_pattern_of_glob_constr na = function | GVar (loc,id) when na<>Anonymous -> (* Unable to manage the presence of both an alias and a variable *) diff --git a/pretyping/glob_term.mli b/pretyping/glob_term.mli index 798a960f..09dd9203 100644 --- a/pretyping/glob_term.mli +++ b/pretyping/glob_term.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* env -> evar_map ref -> + bool -> type_constraint -> env -> evar_map ref -> ltac_var_map -> glob_constr -> unsafe_judgment val pretype_type : - val_constraint -> env -> evar_map ref -> + bool -> val_constraint -> env -> evar_map ref -> ltac_var_map -> glob_constr -> unsafe_type_judgment val pretype_gen : @@ -259,9 +259,9 @@ module Pretyping_F (Coercion : Coercion.S) = struct done (* coerce to tycon if any *) - let inh_conv_coerce_to_tycon loc env evdref j = function + let inh_conv_coerce_to_tycon resolve_tc loc env evdref j = function | None -> j - | Some t -> evd_comb2 (Coercion.inh_conv_coerce_to loc env) evdref j t + | Some t -> evd_comb2 (Coercion.inh_conv_coerce_to resolve_tc loc env) evdref j t let push_rels vars env = List.fold_right push_rel vars env @@ -297,18 +297,19 @@ module Pretyping_F (Coercion : Coercion.S) = struct let c = substl subst c in { uj_val = c; uj_type = protected_get_type_of env sigma c } with Not_found -> - (* Check if [id] is a section or goal variable *) - try - let (_,_,typ) = lookup_named id env in - { uj_val = mkVar id; uj_type = typ } - with Not_found -> - (* [id] not found, build nice error message if [id] yet known from ltac *) + (* if [id] an ltac variable not bound to a term *) + (* build a nice error message *) try match List.assoc id unbndltacvars with | None -> user_err_loc (loc,"", str "Variable " ++ pr_id id ++ str " should be bound to a term.") | Some id0 -> Pretype_errors.error_var_not_found_loc loc id0 with Not_found -> + (* Check if [id] is a section or goal variable *) + try + let (_,_,typ) = lookup_named id env in + { uj_val = mkVar id; uj_type = typ } + with Not_found -> (* [id] not found, standard error message *) error_var_not_found_loc loc id @@ -346,7 +347,11 @@ module Pretyping_F (Coercion : Coercion.S) = struct (* [pretype tycon env evdref lvar lmeta cstr] attempts to type [cstr] *) (* in environment [env], with existential variables [evdref] and *) (* the type constraint tycon *) - let rec pretype (tycon : type_constraint) env evdref lvar = function + let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar t = + let pretype = pretype resolve_tc in + let pretype_type = pretype_type resolve_tc in + let inh_conv_coerce_to_tycon = inh_conv_coerce_to_tycon resolve_tc in + match t with | GRef (loc,ref) -> inh_conv_coerce_to_tycon loc env evdref (pretype_ref loc evdref env ref) @@ -459,7 +464,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct | [] -> resj | c::rest -> let argloc = loc_of_glob_constr c in - let resj = evd_comb1 (Coercion.inh_app_fun env) evdref resj in + let resj = evd_comb1 (Coercion.inh_app_fun resolve_tc env) evdref resj in let resty = whd_betadeltaiota env !evdref resj.uj_type in match kind_of_term resty with | Prod (na,c1,c2) -> @@ -696,7 +701,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct in inh_conv_coerce_to_tycon loc env evdref cj tycon (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *) - and pretype_type valcon env evdref lvar = function + and pretype_type resolve_tc valcon env evdref lvar = function | GHole loc -> (match valcon with | Some v -> @@ -716,7 +721,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct { utj_val = e_new_evar evdref env ~src:loc (mkSort s); utj_type = s}) | c -> - let j = pretype empty_tycon env evdref lvar c in + let j = pretype resolve_tc empty_tycon env evdref lvar c in let loc = loc_of_glob_constr c in let tj = evd_comb1 (Coercion.inh_coerce_to_sort loc env) evdref j in match valcon with @@ -731,9 +736,9 @@ module Pretyping_F (Coercion : Coercion.S) = struct let c' = match kind with | OfType exptyp -> let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in - (pretype tycon env evdref lvar c).uj_val + (pretype resolve_classes tycon env evdref lvar c).uj_val | IsType -> - (pretype_type empty_valcon env evdref lvar c).utj_val + (pretype_type resolve_classes empty_valcon env evdref lvar c).utj_val in resolve_evars env evdref fail_evar resolve_classes; let c = if expand_evar then nf_evar !evdref c' else c' in @@ -747,14 +752,14 @@ module Pretyping_F (Coercion : Coercion.S) = struct let understand_judgment sigma env c = let evdref = ref sigma in - let j = pretype empty_tycon env evdref ([],[]) c in + let j = pretype true empty_tycon env evdref ([],[]) c in resolve_evars env evdref true true; let j = j_nf_evar !evdref j in check_evars env sigma !evdref (mkCast(j.uj_val,DEFAULTcast, j.uj_type)); j let understand_judgment_tcc evdref env c = - let j = pretype empty_tycon env evdref ([],[]) c in + let j = pretype true empty_tycon env evdref ([],[]) c in resolve_evars env evdref false true; j_nf_evar !evdref j diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 761e1641..a785b432 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* env -> evar_map ref -> + bool -> type_constraint -> env -> evar_map ref -> ltac_var_map -> glob_constr -> unsafe_judgment val pretype_type : - val_constraint -> env -> evar_map ref -> + bool -> val_constraint -> env -> evar_map ref -> ltac_var_map -> glob_constr -> unsafe_type_judgment val pretype_gen : diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 434fe80c..f9cd3501 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*