diff options
| -rw-r--r-- | CHANGES | 5 | ||||
| -rw-r--r-- | pretyping/evarconv.ml | 65 | ||||
| -rw-r--r-- | pretyping/evarconv.mli | 3 | ||||
| -rw-r--r-- | pretyping/unification.ml | 33 | ||||
| -rw-r--r-- | test-suite/success/unification.v | 39 |
5 files changed, 111 insertions, 34 deletions
@@ -50,6 +50,11 @@ Tactics This pseudo-database "nocore" can also be used with trivial and eauto. - Tactics "set", "destruct" and "induction" accepts incomplete terms and use the goal to complete the pattern assuming it is no ambiguous. +- When used on arguments with a dependent type, tactics such as + "destruct", "induction", "case", "elim", etc. now try to abstract + automatically the dependencies over the arguments of the types + (based on initial ideas from Chung-Kil Hur, extension to nested + dependencies suggested by Dan Grayson) Vernacular commands diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index ac6a574fc..283363f37 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -594,13 +594,14 @@ let initial_evar_data evi = let solve_evars = ref (fun _ -> failwith "solve_evars not installed") let set_solve_evars f = solve_evars := f -(* We solve the problem env_rhs |- ?e[u1..un] = rhs knowing env_ev |- ev : ty +(* We solve the problem env_rhs |- ?e[u1..un] = rhs knowing + * x1:T1 .. xn:Tn |- ev : ty * by looking for a maximal well-typed abtraction over u1..un in rhs * - * We first build \x1..\xn.C[e11..e1p1,..,en1..enpn] where all occurrences of - * u1..un have been replaced by evars eij (in practice, this is a bit more - * complicated as shown above since each eij depends on x1..xi-1 and because - * occurrences of u1..ui can occur in the types of xi+1..xn). + * We first build C[e11..e1p1,..,en1..enpn] obtained from rhs by replacing + * all occurrences of u1..un by evars eij of type Ti' where itself Ti' has + * been obtained from the type of ui by also replacing all occurrences of + * u1..ui-1 by evars. * * Then, we use typing to infer the relations between the different * occurrences. If some occurrence is still unconstrained after typing, @@ -614,53 +615,61 @@ let second_order_matching ts env_rhs evd (evk,args) rhs = try let args = Array.to_list args in let evi = Evd.find_undefined evd evk in - let sign = evar_hyps evi in + let env_evar = evar_env evi in + let sign = named_context_val env_evar in let ctxt = named_context_of_val sign in let filter = evar_filter evi in let instance = List.map mkVar (List.map pi1 ctxt) in - let rec set_holes evd subst rhs = function + + let rec make_subst = function + | (id,_,t)::ctxt, c::l when isVarId id c -> make_subst (ctxt,l) | (id,_,t)::ctxt, c::l -> - let ty = Retyping.get_type_of env_rhs evd c in - let evd,b = evar_conv_x ts env_rhs evd CUMUL ty (replace_vars subst t) in - if not b then raise Exit; - let subst = (id,c)::subst in - let evd,evoccs,rhs = set_holes evd subst rhs (ctxt,l) in let evs = ref [] in - let evdref = ref evd in let filter = List.map2 (&&) filter (filter_possible_projections c args) in + let ty = Retyping.get_type_of env_rhs evd c in + (id,t,c,ty,evs,filter) :: make_subst (ctxt,l) + | [], [] -> [] + | _ -> anomaly "Signature and instance do not match" in + + let rec set_holes evdref rhs = function + | (id,_,c,cty,evsref,filter)::subst -> let set_var k = - let evd,ev = new_evar_instance sign !evdref t ~filter instance in + let evty = set_holes evdref cty subst in + let evd,ev = new_evar_instance sign !evdref evty ~filter instance in evdref := evd; - evs := fst (destEvar ev)::!evs; + evsref := (fst (destEvar ev),evty)::!evsref; ev in - let rhs = apply_on_subterm set_var c rhs in - (!evdref, (id,c,!evs)::evoccs, rhs) - | [],[] -> - (evd, [], rhs) - | _ -> - anomaly "Signature and instance do not match" in + set_holes evdref (apply_on_subterm set_var c rhs) subst + | [] -> rhs in + + let subst = make_subst (ctxt,args) in - let evd,evoccs,rhs = set_holes evd [] rhs (ctxt,args) in + let evdref = ref evd in + let rhs = set_holes evdref rhs subst in + let evd = !evdref in (* We instantiate the evars of which the value is forced by typing *) let evd,rhs = - try !solve_evars env_rhs evd rhs + try !solve_evars env_evar evd rhs with e when Pretype_errors.precatchable_exception e -> (* Could not revert all subterms *) raise Exit in let rec abstract_free_holes evd = function - | (id,c,evs)::l -> + | (id,idty,c,_,evsref,_)::l -> let rec force_instantiation evd = function - | evk::evs -> + | (evk,evty)::evs -> let evd = if is_undefined evd evk then (* We force abstraction over this unconstrained occurrence *) (* and we use typing to propagate this instantiation *) (* This is an arbitrary choice *) let evd = Evd.define evk (mkVar id) evd in + let evd,b = evar_conv_x ts env_evar evd CUMUL idty evty in + if not b then error "Cannot find an instance"; let evd,b = reconsider_conv_pbs (evar_conv_x ts) evd in - if b then evd else error "Cannot find an instance for ..." + if not b then error "Cannot find an instance"; + evd else evd in @@ -668,11 +677,11 @@ let second_order_matching ts env_rhs evd (evk,args) rhs = | [] -> abstract_free_holes evd l in - force_instantiation evd evs + force_instantiation evd !evsref | [] -> Evd.define evk rhs evd in - abstract_free_holes evd evoccs, true + abstract_free_holes evd subst, true with Exit -> evd, false let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index 270d3f1e6..27a71be24 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -41,3 +41,6 @@ val check_conv_record : constr * types list -> constr * types list -> (int * constr) val set_solve_evars : (env -> evar_map -> constr -> evar_map * constr) -> unit + +val second_order_matching : transparent_state -> env -> evar_map -> + existential -> constr -> evar_map * bool diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 01d75233b..250d83cc4 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -64,6 +64,14 @@ let abstract_list_all env evd typ c l = with UserError _ | Type_errors.TypeError _ -> error_cannot_find_well_typed_abstraction env evd p l +let abstract_list_all_with_dependencies env evd typ c l = + let evd,ev = new_evar evd env typ in + let evd,ev' = evar_absorb_arguments env evd (destEvar ev) l in + let evd,b = + Evarconv.second_order_matching empty_transparent_state env evd ev' c in + if b then nf_evar evd (existential_value evd (destEvar ev)) + else error "Cannot find a well-typed abstraction." + (**) (* A refinement of [conv_pb]: the integers tells how many arguments @@ -1124,16 +1132,24 @@ let secondOrderAbstraction env evd flags typ (p, oplist) = let pred = abstract_list_all env evd' typp typ cllist in w_merge env false flags (evd',[p,pred,(Conv,TypeProcessed)],[]) -let w_unify2 env evd flags cv_pb ty1 ty2 = +let secondOrderDependentAbstraction env evd flags typ (p, oplist) = + let typp = Typing.meta_type evd p in + let pred = abstract_list_all_with_dependencies env evd typp typ oplist in + w_merge env false flags (evd,[p,pred,(Conv,TypeProcessed)],[]) + +let secondOrderAbstractionAlgo dep = + if dep then secondOrderDependentAbstraction else secondOrderAbstraction + +let w_unify2 env evd flags dep cv_pb ty1 ty2 = let c1, oplist1 = whd_stack evd ty1 in let c2, oplist2 = whd_stack evd ty2 in match kind_of_term c1, kind_of_term c2 with | Meta p1, _ -> (* Find the predicate *) - secondOrderAbstraction env evd flags ty2 (p1,oplist1) + secondOrderAbstractionAlgo dep env evd flags ty2 (p1,oplist1) | _, Meta p2 -> (* Find the predicate *) - secondOrderAbstraction env evd flags ty1 (p2, oplist2) + secondOrderAbstractionAlgo dep env evd flags ty1 (p2, oplist2) | _ -> error "w_unify2" (* The unique unification algorithm works like this: If the pattern is @@ -1167,19 +1183,24 @@ let w_unify env evd cv_pb ?(flags=default_unify_flags) ty1 ty2 = w_typed_unify_list env evd flags hd1 l1 hd2 l2 with ex when precatchable_exception ex -> try - w_unify2 env evd flags cv_pb ty1 ty2 + w_unify2 env evd flags false cv_pb ty1 ty2 with PretypeError (env,_,NoOccurrenceFound _) as e -> raise e) (* Second order case *) | (Meta _, true, _, _ | _, _, Meta _, true) -> (try - w_unify2 env evd flags cv_pb ty1 ty2 + w_unify2 env evd flags false cv_pb ty1 ty2 with PretypeError (env,_,NoOccurrenceFound _) as e -> raise e | ex when precatchable_exception ex -> try w_typed_unify_list env evd flags hd1 l1 hd2 l2 with ex' when precatchable_exception ex' -> - raise ex) + (* Last chance, use pattern-matching with typed + dependencies (done late for compatibility) *) + try + w_unify2 env evd flags true cv_pb ty1 ty2 + with ex' when precatchable_exception ex' -> + raise ex) (* General case: try first order *) | _ -> w_typed_unify env evd cv_pb flags ty1 ty2 diff --git a/test-suite/success/unification.v b/test-suite/success/unification.v index fdc7c7222..997dceb4d 100644 --- a/test-suite/success/unification.v +++ b/test-suite/success/unification.v @@ -145,3 +145,42 @@ Proof. intros. rewrite H with (f:=f0). Abort. + +(* Three tests provided by Dan Grayson as part of a custom patch he + made for a more powerful "destruct" for handling Voevodsky's + Univalent Foundations. The test checks if second-order matching in + tactic unification is able to guess by itself on which dependent + terms to abstract so that the elimination predicate is well-typed *) + +Definition test1 (X : Type) (x : X) (fxe : forall x1 : X, identity x1 x1) : + identity (fxe x) (fxe x). +Proof. destruct (fxe x). apply identity_refl. Defined. + +(* a harder example *) + +Definition UU := Type . +Inductive paths {T:Type}(t:T): T -> UU := idpath: paths t t. +Inductive foo (X0:UU) (x0:X0) : forall (X:UU)(x:X), UU := newfoo : foo x0 x0. +Definition idonfoo {X0:UU} {x0:X0} {X1:UU} {x1:X1} : foo x0 x1 -> foo x0 x1. +Proof. intros t. exact t. Defined. + +Lemma test2 (T:UU) (t:T) (k : foo t t) : paths k (idonfoo k). +Proof. + destruct k. + apply idpath. +Defined. + +(* an example with two constructors *) + +Inductive foo' (X0:UU) (x0:X0) : forall (X:UU)(x:X), UU := +| newfoo1 : foo' x0 x0 +| newfoo2 : foo' x0 x0 . +Definition idonfoo' {X0:UU} {x0:X0} {X1:UU} {x1:X1} : + foo' x0 x1 -> foo' x0 x1. +Proof. intros t. exact t. Defined. +Lemma test3 (T:UU) (t:T) (k : foo' t t) : paths k (idonfoo' k). +Proof. + destruct k. + apply idpath. + apply idpath. +Defined. |