diff options
| -rw-r--r-- | pretyping/evarconv.ml | 29 | ||||
| -rw-r--r-- | pretyping/evarconv.mli | 3 | ||||
| -rw-r--r-- | pretyping/unification.ml | 7 |
3 files changed, 27 insertions, 12 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 53c659062..ec581eaf1 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -618,7 +618,7 @@ let set_solve_evars f = solve_evars := f * proposition from Dan Grayson] *) -let second_order_matching ts env_rhs evd (evk,args) rhs = +let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = try let args = Array.to_list args in let evi = Evd.find_undefined evd evk in @@ -629,18 +629,26 @@ let second_order_matching ts env_rhs evd (evk,args) rhs = let instance = List.map mkVar (List.map pi1 ctxt) in let rec make_subst = function - | (id,_,t)::ctxt, c::l when isVarId id c -> make_subst (ctxt,l) - | (id,_,t)::ctxt, c::l -> + | (id,_,t)::ctxt, c::l, occs::occsl when isVarId id c -> + if occs<>None then + error "Cannot force abstraction on identity instance." + else + make_subst (ctxt,l,occsl) + | (id,_,t)::ctxt, c::l, occs::occsl -> let evs = ref [] 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 + (id,t,c,ty,evs,filter,occs) :: make_subst (ctxt,l,occsl) + | [], [], [] -> [] + | _ -> anomaly "Signature, instance and occurrences list do not match" in let rec set_holes evdref rhs = function - | (id,_,c,cty,evsref,filter)::subst -> + | (id,_,c,cty,evsref,filter,occs)::subst -> let set_var k = + match occs with + | Some (false,[]) -> mkVar id + | Some _ -> error "Selection of specific occurrences not supported" + | None -> let evty = set_holes evdref cty subst in let instance = snd (list_filter2 (fun b c -> b) (filter,instance)) in let evd,ev = new_evar_instance sign !evdref evty ~filter instance in @@ -650,7 +658,7 @@ let second_order_matching ts env_rhs evd (evk,args) rhs = set_holes evdref (apply_on_subterm set_var c rhs) subst | [] -> rhs in - let subst = make_subst (ctxt,args) in + let subst = make_subst (ctxt,args,argoccs) in let evdref = ref evd in let rhs = set_holes evdref rhs subst in @@ -664,7 +672,7 @@ let second_order_matching ts env_rhs evd (evk,args) rhs = raise Exit in let rec abstract_free_holes evd = function - | (id,idty,c,_,evsref,_)::l -> + | (id,idty,c,_,evsref,_,_)::l -> let rec force_instantiation evd = function | (evk,evty)::evs -> let evd = @@ -695,7 +703,8 @@ let second_order_matching ts env_rhs evd (evk,args) rhs = let second_order_matching_with_args ts env evd ev l t = (* let evd,ev = evar_absorb_arguments env evd ev l in - second_order_matching ts env evd ev t + let argoccs = array_map_to_list (fun _ -> None) (snd ev) in + second_order_matching ts env evd ev argoccs t *) (evd,false) diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index 27a71be24..3e2ca7aed 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -10,6 +10,7 @@ open Names open Term open Sign open Environ +open Termops open Reductionops open Evd @@ -43,4 +44,4 @@ val check_conv_record : constr * types list -> constr * types list -> 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 + existential -> occurrences option list -> constr -> evar_map * bool diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 693ea4395..a66074585 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -64,11 +64,16 @@ 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 set_occurrences_of_last_arg args = + Some all_occurrences :: List.tl (array_map_to_list (fun _ -> None) args) + 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 argoccs = set_occurrences_of_last_arg (snd ev') in let evd,b = - Evarconv.second_order_matching empty_transparent_state env evd ev' c in + Evarconv.second_order_matching empty_transparent_state + env evd ev' argoccs c in if b then nf_evar evd (existential_value evd (destEvar ev)) else error "Cannot find a well-typed abstraction." |