diff options
| -rw-r--r-- | pretyping/clenv.ml | 34 | ||||
| -rw-r--r-- | pretyping/evd.ml | 14 | ||||
| -rw-r--r-- | pretyping/evd.mli | 12 | ||||
| -rw-r--r-- | pretyping/reductionops.ml | 22 | ||||
| -rw-r--r-- | pretyping/unification.ml | 123 | ||||
| -rw-r--r-- | pretyping/unification.mli | 2 | ||||
| -rw-r--r-- | tactics/decl_proof_instr.ml | 6 | ||||
| -rw-r--r-- | test-suite/success/apply.v | 51 | ||||
| -rw-r--r-- | toplevel/cerrors.ml | 10 |
9 files changed, 169 insertions, 105 deletions
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml index edf905641..5f4293abf 100644 --- a/pretyping/clenv.ml +++ b/pretyping/clenv.ml @@ -196,7 +196,9 @@ let clenv_assign mv rhs clenv = error_incompatible_inst clenv mv else clenv - else {clenv with evd = meta_assign mv (rhs_fls.rebus,ConvUpToEta 0) clenv.evd} + else + let st = (ConvUpToEta 0,TypeNotProcessed) in + {clenv with evd = meta_assign mv (rhs_fls.rebus,st) clenv.evd} with Not_found -> error "clenv_assign: undefined meta" @@ -241,25 +243,7 @@ let clenv_unify allow_K cv_pb t1 t2 clenv = { clenv with evd = w_unify allow_K clenv.env cv_pb t1 t2 clenv.evd } let clenv_unify_meta_types clenv = - List.fold_left (fun clenv (k,m) -> - match m with - | Cltyp _ -> clenv - | Clval (na,(c,s),k_typ) -> - let k_typ = clenv_hnf_constr clenv k_typ.rebus in - match s with - | Coercible c_typ when not (occur_meta k_typ) -> - let evd,c' = w_coerce (cl_env clenv) c.rebus c_typ k_typ clenv.evd in - {clenv with evd = meta_reassign k (c',ConvUpToEta 0) clenv.evd} - | _ -> - (* nf_betaiota was before in type_of - useful to reduce - types like (x:A)([x]P u) *) - let c_typ = nf_betaiota (clenv_get_type_of clenv c.rebus) in - let c_typ = clenv_hnf_constr clenv c_typ in - (* Try to infer some Meta/Evar from the type of [c] *) - try clenv_unify true CUMUL c_typ k_typ clenv - with e when precatchable_exception e -> clenv) - clenv (meta_list clenv.evd) - + { clenv with evd = w_unify_meta_types clenv.env clenv.evd } let clenv_unique_resolver allow_K clenv gl = if isMeta (fst (whd_stack clenv.templtyp.rebus)) then @@ -398,13 +382,13 @@ let rec similar_type_shapes t u = let clenv_unify_similar_types clenv c t u = if occur_meta u then if similar_type_shapes t u then - try Processed, clenv_unify true CUMUL t u clenv, c - with e when precatchable_exception e -> Coercible t, clenv, c + try TypeProcessed, clenv_unify true CUMUL t u clenv, c + with e when precatchable_exception e -> TypeNotProcessed, clenv, c else - Coercible t, clenv, c + TypeNotProcessed, clenv, c else let evd,c = w_coerce (cl_env clenv) c t u clenv.evd in - Processed, { clenv with evd = evd }, c + TypeProcessed, { clenv with evd = evd }, c let clenv_assign_binding clenv k (sigma,c) = let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in @@ -413,7 +397,7 @@ let clenv_assign_binding clenv k (sigma,c) = let c_typ = clenv_hnf_constr clenv' c_typ in let status,clenv'',c = clenv_unify_similar_types clenv' c c_typ k_typ in (* let evd,c' = w_coerce (cl_env clenv') c c_typ k_typ clenv'.evd in*) - { clenv'' with evd = meta_assign k (c,status) clenv''.evd } + { clenv'' with evd = meta_assign k (c,(UserGiven,status)) clenv''.evd } let clenv_match_args bl clenv = if bl = [] then diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 7b5690e2c..439f46264 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -334,9 +334,13 @@ let map_fl f cfl = { cfl with rebus=f cfl.rebus } (e.g. the solution [P] to [?X u v = P u v] can be eta-expanded twice) *) -type instance_status = - | IsSuperType | IsSubType - | ConvUpToEta of int | Coercible of types | Processed +type instance_constraint = + IsSuperType | IsSubType | ConvUpToEta of int | UserGiven + +type instance_typing_status = + TypeNotProcessed | TypeProcessed + +type instance_status = instance_constraint * instance_typing_status (* Clausal environments *) @@ -543,7 +547,7 @@ let retract_coercible_metas evd = let mc,ml = Metamap.fold (fun n v (mc,ml) -> match v with - | Clval (na,(b,s),typ) when s <> Processed -> + | Clval (na,(b,(UserGiven,TypeNotProcessed as s)),typ) -> (n,b.rebus,s)::mc, Metamap.add n (Cltyp (na,typ)) ml | v -> mc, Metamap.add n v ml) @@ -556,7 +560,7 @@ let rec list_assoc_in_triple x = function let subst_defined_metas bl c = let rec substrec c = match kind_of_term c with - | Meta i -> list_assoc_in_triple i bl + | Meta i -> substrec (list_assoc_in_triple i bl) | _ -> map_constr substrec c in try Some (substrec c) with Not_found -> None diff --git a/pretyping/evd.mli b/pretyping/evd.mli index b6ffd02c1..4375f5471 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -104,16 +104,20 @@ val metavars_of : constr -> Metaset.t val mk_freelisted : constr -> constr freelisted val map_fl : ('a -> 'b) -> 'a freelisted -> 'b freelisted -(* Status of an instance wrt to the meta it solves: +(* Possible constraints over the instance of a metavariable: - a supertype of the meta (e.g. the solution to ?X <= T is a supertype of ?X) - a subtype of the meta (e.g. the solution to T <= ?X is a supertype of ?X) - a term that can be eta-expanded n times while still being a solution (e.g. the solution [P] to [?X u v = P u v] can be eta-expanded twice) *) -type instance_status = - | IsSuperType | IsSubType - | ConvUpToEta of int | Coercible of types | Processed +type instance_constraint = + IsSuperType | IsSubType | ConvUpToEta of int | UserGiven + +type instance_typing_status = + TypeNotProcessed | TypeProcessed + +type instance_status = instance_constraint * instance_typing_status type clbinding = | Cltyp of name * constr freelisted diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 7f05b1cbf..f247f47b6 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -896,8 +896,8 @@ let meta_value evd mv = let meta_reducible_instance evd b = let fm = Metaset.elements b.freemetas in - let s = List.fold_left (fun l mv -> - try let g,s = meta_fvalue evd mv in (mv,(g.rebus,s))::l + let metas = List.fold_left (fun l mv -> + try let g,(_,s) = meta_fvalue evd mv in (mv,(g.rebus,s))::l with Anomaly _ | Not_found -> l) [] fm in let rec irec u = let u = whd_betaiota u in @@ -906,8 +906,8 @@ let meta_reducible_instance evd b = let m = try destMeta c with _ -> destMeta (pi1 (destCast c)) in (match try - let g,s = List.assoc m s in - if isConstruct g or s = Processed then Some g else None + let g,s = List.assoc m metas in + if isConstruct g or s = TypeProcessed then Some g else None with Not_found -> None with | Some g -> irec (mkCase (ci,p,g,bl)) @@ -916,15 +916,15 @@ let meta_reducible_instance evd b = let m = try destMeta f with _ -> destMeta (pi1 (destCast f)) in (match try - let g,s = List.assoc m s in - if isLambda g or s = Processed then Some g else None + let g,s = List.assoc m metas in + if isLambda g or s = TypeProcessed then Some g else None with Not_found -> None - with - | Some g -> irec (mkApp (g,l)) - | None -> mkApp (f,Array.map irec l)) + with + | Some g -> irec (mkApp (g,l)) + | None -> mkApp (f,Array.map irec l)) | Meta m -> - (try let g,s = List.assoc m s in if s = Processed then irec g else u - with Not_found -> u) + (try let g,s = List.assoc m metas in if s=TypeProcessed then irec g else u + with Not_found -> u) | _ -> map_constr irec u in if fm = [] then (* nf_betaiota? *) b.rebus else irec b.rebus diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 372188e8a..4116445e1 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -65,11 +65,13 @@ let prod_pb = function ConvUnderApp _ -> topconv | pb -> pb let opp_status = function | IsSuperType -> IsSubType | IsSubType -> IsSuperType - | ConvUpToEta _ | Coercible _ | Processed as x -> x + | ConvUpToEta _ | UserGiven as x -> x + +let add_type_status (x,y) = ((x,TypeNotProcessed),(y,TypeNotProcessed)) let extract_instance_status = function - | Cumul -> (IsSubType,IsSuperType) - | ConvUnderApp (n1,n2) -> ConvUpToEta n1, ConvUpToEta n2 + | Cumul -> add_type_status (IsSubType, IsSuperType) + | ConvUnderApp (n1,n2) -> add_type_status (ConvUpToEta n1, ConvUpToEta n2) let rec assoc_pair x = function [] -> raise Not_found @@ -83,7 +85,7 @@ let rec subst_meta_instances bl c = let solve_pattern_eqn_array env f l c (metasubst,evarsubst) = match kind_of_term f with | Meta k -> - let pb = ConvUpToEta (Array.length l) in + let pb = (ConvUpToEta (Array.length l),TypeNotProcessed) in (k,solve_pattern_eqn env (Array.to_list l) c,pb)::metasubst,evarsubst | Evar ev -> (* Currently unused: incompatible with eauto/eassumption backtracking *) @@ -183,9 +185,9 @@ let unify_0_with_initial_metas metas env sigma cv_pb mod_delta m n = (if mod_delta then is_fconv (conv_pb_of cv_pb) env sigma m n else eq_constr m n) then - ([],[]) + (metas,[]) else - let (mc,ec) = unirec_rec env cv_pb ([],[]) m n in + let (mc,ec) = unirec_rec env cv_pb (metas,[]) m n in ((*sort_eqns*) mc, (*sort_eqns*) ec) let unify_0 = unify_0_with_initial_metas [] @@ -228,19 +230,25 @@ let rec unify_with_eta keptside mod_delta env sigma k1 k2 c1 c2 = let merge_instances env sigma mod_delta st1 st2 c1 c2 = match (opp_status st1, st2) with + | (UserGiven, ConvUpToEta n2) -> + unify_with_eta left mod_delta env sigma 0 n2 c1 c2 + | (ConvUpToEta n1, UserGiven) -> + unify_with_eta right mod_delta env sigma n1 0 c1 c2 | (ConvUpToEta n1, ConvUpToEta n2) -> let side = left (* arbitrary choice, but agrees with compatibility *) in unify_with_eta side mod_delta env sigma n1 n2 c1 c2 - | ((IsSubType | ConvUpToEta _ | Coercible _ | Processed as oppst1), - (IsSubType | ConvUpToEta _ | Coercible _ | Processed)) -> + | ((IsSubType | ConvUpToEta _ | UserGiven as oppst1), + (IsSubType | ConvUpToEta _ | UserGiven)) -> let res = unify_0 env sigma Cumul mod_delta c2 c1 in if oppst1=st2 then (* arbitrary choice *) (left, st1, res) - else (st2=IsSubType, ConvUpToEta 0, res) - | ((IsSuperType | ConvUpToEta _ | Coercible _ | Processed as oppst1), - (IsSuperType | ConvUpToEta _ | Coercible _ | Processed)) -> + else if st2=IsSubType or st1=UserGiven then (left, st1, res) + else (right, st2, res) + | ((IsSuperType | ConvUpToEta _ | UserGiven as oppst1), + (IsSuperType | ConvUpToEta _ | UserGiven)) -> let res = unify_0 env sigma Cumul mod_delta c1 c2 in if oppst1=st2 then (* arbitrary choice *) (left, st1, res) - else (st2=IsSuperType, ConvUpToEta 0, res) + else if st2=IsSuperType or st1=UserGiven then (left, st1, res) + else (right, st2, res) | (IsSuperType,IsSubType) -> (try (left, IsSubType, unify_0 env sigma Cumul mod_delta c2 c1) with _ -> (right, IsSubType, unify_0 env sigma Cumul mod_delta c1 c2)) @@ -323,7 +331,25 @@ let w_coerce env c ctyp target evd = (evd',j'.uj_val) with e when precatchable_exception e -> evd,c - + +let unify_0_meta_type env evd mod_delta mv c = + let sigma = evars_of evd in + let metamap = metas_of evd in + let mvty = Typing.meta_type evd mv in + let mvty = Tacred.hnf_constr env sigma mvty in + (* nf_betaiota was before in type_of - useful to reduce + types like (x:A)([x]P u) *) + let c = refresh_universes c in + let nty = get_type_of_with_meta env sigma metamap c in + let nty = Tacred.hnf_constr env sigma (nf_betaiota nty) in + if occur_meta mvty then + try (evd,c),(unify_0 env sigma Cumul mod_delta nty mvty) + with e when precatchable_exception e -> (evd,c),([],[]) + else + (* Try to coerce to the type of [k]; cannot merge with the + previous case because Coercion does not handle Meta *) + w_coerce env c nty mvty evd,([],[]) + (* [w_merge env sigma b metas evars] merges common instances in metas or in evars, possibly generating new unification problems; if [b] is true, unification of types of metas is required *) @@ -335,17 +361,19 @@ let w_merge env with_types mod_delta metas evars evd = match (evars,metas) with | [], [] -> evd - | ((evn,_ as ev),rhs)::t, metas -> + | ((evn,_ as ev),rhs)::evars', metas -> (match kind_of_term rhs with - | Meta k -> w_merge_rec evd ((k,mkEvar ev,ConvUpToEta 0)::metas) t + | Meta k -> + w_merge_rec evd ((k,mkEvar ev,(ConvUpToEta 0,TypeNotProcessed))::metas) + evars | krhs -> if is_defined_evar evd ev then let v = Evd.existential_value (evars_of evd) ev in - let (metas',evars') = + let (metas',evars'') = unify_0 env (evars_of evd) topconv mod_delta rhs v in - w_merge_rec evd (metas'@metas) (evars'@t) + w_merge_rec evd (metas'@metas) (evars''@evars') else begin let rhs' = if occur_meta rhs then subst_meta_instances metas rhs @@ -356,56 +384,41 @@ let w_merge env with_types mod_delta metas evars evd = match krhs with | App (f,cl) when is_mimick_head f -> (try - w_merge_rec (fst (evar_define env ev rhs' evd)) metas t + w_merge_rec (fst (evar_define env ev rhs' evd)) + metas evars' with ex when precatchable_exception ex -> let evd' = mimick_evar evd mod_delta f (Array.length cl) evn in w_merge_rec evd' metas evars) | _ -> (* ensure tail recursion in non-mimickable case! *) - w_merge_rec (fst (evar_define env ev rhs' evd)) metas t + w_merge_rec (fst (evar_define env ev rhs' evd)) + metas evars' end) - | ([], (mv,n,status)::t) -> + | ([], (mv,n,(status,to_type))::metas) -> + let evd,n = + if with_types & to_type = TypeNotProcessed then + let evd_n,(mc,ec) = unify_0_meta_type env evd mod_delta mv n in + ty_metas := mc @ !ty_metas; + ty_evars := ec @ !ty_evars; + evd_n + else + evd,n in if meta_defined evd mv then - let n',status' = meta_fvalue evd mv in + let n',(status',_) = meta_fvalue evd mv in let n' = n'.rebus in let (take_left,st,(metas',evars')) = merge_instances env (evars_of evd) mod_delta status' status n' n in - let evd' = if take_left then evd else meta_reassign mv (n,st) evd + let evd' = + if take_left then evd + else meta_reassign mv (n,(st,TypeProcessed)) evd in - w_merge_rec evd' (metas'@t) evars' + w_merge_rec evd' (metas'@metas) evars' else - begin - let evd,n = - if with_types & status <> Processed then - let sigma = evars_of evd in - let metas = metas_of evd in - let mvty = Typing.meta_type evd mv in - let mvty = Tacred.hnf_constr env sigma mvty in - (* nf_betaiota was before in type_of - useful to reduce - types like (x:A)([x]P u) *) - let n = refresh_universes n in - let nty = get_type_of_with_meta env sigma metas n in - let nty = Tacred.hnf_constr env sigma (nf_betaiota nty) in - if occur_meta mvty then - (try - let (mc,ec) = unify_0 env sigma Cumul mod_delta nty mvty - in - ty_metas := mc @ !ty_metas; - ty_evars := ec @ !ty_evars; - evd,n - with e when precatchable_exception e -> evd,n) - else - (* Try to coerce to the type of [k]; cannot merge with the - previous case because Coercion does not handle Meta *) - w_coerce env n nty mvty evd - else - evd,n in - let evd' = meta_assign mv (n,status) evd in - w_merge_rec evd' t [] - end + let evd' = meta_assign mv (n,(status,TypeProcessed)) evd in + w_merge_rec evd' metas [] and mimick_evar evd mod_delta hdc nargs sp = let ev = Evd.find (evars_of evd) sp in @@ -428,6 +441,10 @@ let w_merge env with_types mod_delta metas evars evd = else evd' +let w_unify_meta_types env evd = + let metas,evd = retract_coercible_metas evd in + w_merge env true true metas [] evd + (* [w_unify env evd M N] performs a unification of M and N, generating a bunch of unification constraints in the process. These constraints @@ -442,7 +459,7 @@ let w_unify_core_0 env with_types cv_pb mod_delta m n evd = let (mc1,evd') = retract_coercible_metas evd in let (mc2,ec) = unify_0_with_initial_metas mc1 env (evars_of evd') cv_pb mod_delta m n in - w_merge env with_types mod_delta (mc1@mc2) ec evd' + w_merge env with_types mod_delta mc2 ec evd' let w_unify_0 env = w_unify_core_0 env false let w_typed_unify env = w_unify_core_0 env true diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 441b2e495..f163e95f6 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -24,6 +24,8 @@ val w_unify : val w_unify_to_subterm : env -> ?mod_delta:bool -> constr * constr -> evar_defs -> evar_defs * constr +val w_unify_meta_types : env -> evar_defs -> evar_defs + (*i This should be in another module i*) (* [abstract_list_all env sigma t c l] *) diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml index 99507f56c..28fc640d1 100644 --- a/tactics/decl_proof_instr.ml +++ b/tactics/decl_proof_instr.ml @@ -351,7 +351,8 @@ let enstack_subsubgoals env se stack gls= let (nlast,holes,nmetas) = meta_aux se.se_last_meta [] (List.rev rc) in let refiner = applist (appterm,List.rev holes) in - let evd = meta_assign se.se_meta (refiner,ConvUpToEta 0) se.se_evd in + let evd = meta_assign se.se_meta + (refiner,(ConvUpToEta 0,TypeProcessed (* ? *))) se.se_evd in let ncreated = replace_in_list se.se_meta nmetas se.se_meta_list in let evd0 = List.fold_left @@ -397,7 +398,8 @@ let find_subsubgoal c ctyp skip submetas gls = ctyp se.se_type se.se_evd in if n <= 0 then {se with - se_evd=meta_assign se.se_meta (c,ConvUpToEta 0) unifier; + se_evd=meta_assign se.se_meta + (c,(ConvUpToEta 0,TypeNotProcessed (* ?? *))) unifier; se_meta_list=replace_in_list se.se_meta submetas se.se_meta_list} else diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v index adb55cf2c..014f6ffcd 100644 --- a/test-suite/success/apply.v +++ b/test-suite/success/apply.v @@ -112,3 +112,54 @@ Goal forall p q1 q2, f (f q1 (Zpos p)) (f q2 (Zpos p)) = Z0. intros; rewrite g with (p:=p). reflexivity. Qed. + +(* A funny example where the behavior differs depending on which of a + multiple solution to a unification problem is chosen (an instance + of this case can be found in the proof of Buchberger.BuchRed.nf_divp) *) + +Definition succ x := S x. +Goal forall (I : nat -> Set) (P : nat -> Prop) (Q : forall n:nat, I n -> Prop), + (forall x y, P x -> Q x y) -> + (forall x, P (S x)) -> forall y: I (S 0), Q (succ 0) y. +intros. +apply H with (y:=y). +(* [x] had two possible instances: [S 0], coming from unifying the + type of [y] with [I ?n] and [succ 0] coming from the unification with + the goal; only the first one allows to make the next apply (which + does not work modulo delta) working *) +apply H0. +Qed. + +(* A similar example with a arbitrary long conversion between the two + possible instances *) + +Fixpoint compute_succ x := + match x with O => S 0 | S n => S (compute_succ n) end. + +Goal forall (I : nat -> Set) (P : nat -> Prop) (Q : forall n:nat, I n -> Prop), + (forall x y, P x -> Q x y) -> + (forall x, P (S x)) -> forall y: I (S 100), Q (compute_succ 100) y. +intros. +apply H with (y:=y). +apply H0. +Qed. + +(* Another example with multiple convertible solutions to the same + metavariable (extracted from Algebra.Hom_module.Hom_module, 10th + subgoal which precisely fails) *) + +Definition ID (A:Type) := A. +Goal forall f:Type -> Type, + forall (P : forall A:Type, A -> Prop), + (forall (B:Type) x, P (f B) x -> P (f B) x) -> + (forall (A:Type) x, P (f (f A)) x) -> + forall (A:Type) (x:f (f A)), P (f (ID (f A))) x. +intros. +apply H. +(* The parameter [B] had two possible instances: [ID (f A)] by direct + unification and [f A] by unification of the type of [x]; only the + first choice makes the next command fail, as it was + (unfortunately?) in Hom_module *) +try apply H. +unfold ID; apply H0. +Qed. diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index 9d1d8d184..4c600bc66 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -28,10 +28,6 @@ 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_aux anomaly_string report_fn = function @@ -127,8 +123,12 @@ let rec explain_exn_default_aux anomaly_string report_fn = function hov 0 (anomaly_string () ++ str "Uncaught exception " ++ str (Printexc.to_string reraise) ++ report_fn ()) +let anomaly_string () = str "Anomaly: " + +let report () = (str "." ++ spc () ++ str "Please report.") + let explain_exn_default = - explain_exn_default_aux (fun () -> str "Anomaly: ") report + explain_exn_default_aux anomaly_string report let raise_if_debug e = if !Options.debug then raise e |