diff options
| -rw-r--r-- | pretyping/evarutil.ml | 97 | ||||
| -rw-r--r-- | pretyping/evarutil.mli | 6 | ||||
| -rw-r--r-- | pretyping/evd.ml | 2 | ||||
| -rw-r--r-- | pretyping/evd.mli | 2 | ||||
| -rw-r--r-- | test-suite/success/evars.v | 40 |
5 files changed, 94 insertions, 53 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index ab3e655a1..cb64fcb56 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -139,7 +139,7 @@ let new_untyped_evar = * functional operations on evar sets * *------------------------------------*) -let new_evar_instance sign evd typ ?(src=(dummy_loc,InternalHole)) ?(filter=None) instance = +let new_evar_instance sign evd typ ?(src=(dummy_loc,InternalHole)) ?filter instance = let instance = match filter with | None -> instance @@ -148,7 +148,7 @@ let new_evar_instance sign evd typ ?(src=(dummy_loc,InternalHole)) ?(filter=None (let ctxt = named_context_of_val sign in list_distinct (ids_of_named_context ctxt)); let newevk = new_untyped_evar() in - let evd = evar_declare sign newevk typ ~src:src ~filter:filter evd in + let evd = evar_declare sign newevk typ ~src:src ?filter evd in (evd,mkEvar (newevk,Array.of_list instance)) (* Knowing that [Gamma |- ev : T] and that [ev] is applied to [args], @@ -234,13 +234,13 @@ let push_rel_context_to_named_context env typ = (* [new_evar] declares a new existential in an env env with type typ *) (* Converting the env into the sign of the evar to define *) -let new_evar evd env ?(src=(dummy_loc,InternalHole)) ?(filter=None) typ = +let new_evar evd env ?(src=(dummy_loc,InternalHole)) ?filter typ = let sign,typ',instance = push_rel_context_to_named_context env typ in - new_evar_instance sign evd typ' ~src:src ~filter:filter instance + new_evar_instance sign evd typ' ~src:src ?filter instance (* The same using side-effect *) -let e_new_evar evdref env ?(src=(dummy_loc,InternalHole)) ?(filter=None) ty = - let (evd',ev) = new_evar !evdref env ~src:src ~filter:filter ty in +let e_new_evar evdref env ?(src=(dummy_loc,InternalHole)) ?filter ty = + let (evd',ev) = new_evar !evdref env ~src:src ?filter ty in evdref := evd'; ev @@ -339,31 +339,32 @@ let is_defined_equation env evd (ev,inst) rhs = * making the z1..zm unavailable. *) -let shrink_context env' subst ty = - let named_sign' = List.rev (named_context env') in - let rel_sign' = rel_context env' in +let shrink_context env subst ty = + let rev_named_sign = List.rev (named_context env) in + let rel_sign = rel_context env in (* We merge the contexts (optimization) *) - let rec shrink_rel i subst rel_subst rel_sign' = - match subst,rel_sign' with - | (id,c)::subst,_::rel_sign' when c = mkRel i -> - shrink_rel (i-1) subst (mkVar id::rel_subst) rel_sign' + let rec shrink_rel i subst rel_subst rev_rel_sign = + match subst,rev_rel_sign with + | (id,c)::subst,_::rev_rel_sign when c = mkRel i -> + shrink_rel (i-1) subst (mkVar id::rel_subst) rev_rel_sign | _ -> - substl_rel_context rel_subst (List.rev rel_sign'), substl rel_subst ty + substl_rel_context rel_subst (List.rev rev_rel_sign), + substl rel_subst ty in - let rec shrink_named subst named_subst named_sign' = - match subst,named_sign' with - | (id,c)::subst,(id',b',t')::named_sign' when c = mkVar id' -> - shrink_named subst ((id',mkVar id)::named_subst) named_sign' + let rec shrink_named subst named_subst rev_named_sign = + match subst,rev_named_sign with + | (id,c)::subst,(id',b',t')::rev_named_sign when c = mkVar id' -> + shrink_named subst ((id',mkVar id)::named_subst) rev_named_sign | _::_, [] -> - let nrel = List.length rel_sign' in - let rel_sign', ty = shrink_rel nrel subst [] (List.rev rel_sign') in - [], map_rel_context (replace_vars named_subst) rel_sign', + let nrel = List.length rel_sign in + let rel_sign, ty = shrink_rel nrel subst [] (List.rev rel_sign) in + [], map_rel_context (replace_vars named_subst) rel_sign, replace_vars named_subst ty | _ -> - map_named_context (replace_vars named_subst) (List.rev named_sign'), - rel_sign', ty + map_named_context (replace_vars named_subst) (List.rev rev_named_sign), + rel_sign, ty in - shrink_named subst [] named_sign' + shrink_named subst [] rev_named_sign let extend_evar env evdref k (evk1,args1) c = let ty = Retyping.get_type_of env (evars_of !evdref) c in @@ -383,8 +384,7 @@ let extend_evar env evdref k (evk1,args1) c = let rel_filter = list_map_i (fun i _ -> i > nb_to_hide) 1 rel_sign' in let named_filter1 = List.map (fun _ -> true) (named_context (evar_env evi1)) in let named_filter2 = List.map (fun _ -> false) named_sign' in - let filter = named_filter1@named_filter2@rel_filter in - let filter = if List.for_all (fun x -> x) filter then None else Some filter in + let filter = rel_filter@named_filter2@named_filter1 in let evar1' = e_new_evar evdref extenv ~filter:filter ty in let evk1',args1'_in_env = destEvar evar1' in let args1'_in_extenv = Array.map (lift k) (overwrite_first args1'_in_env args1) in @@ -405,7 +405,7 @@ let restrict_upon_filter evd evi evk p args = let newfilter,newargs = subfilter p filter args in if newfilter <> filter then let (evd,newev) = new_evar evd (evar_env evi) ~src:(evar_source evk evd) - ~filter:(Some newfilter) evi.evar_concl in + ~filter:newfilter evi.evar_concl in let evd = Evd.evar_define evk newev evd in evd,fst (destEvar newev),newargs else @@ -436,7 +436,7 @@ let do_restrict_hyps evd evk filter = if oldb then List.hd filter::l,List.tl filter else (false::l,filter)) oldfilter ([],List.rev filter) in let evd,nc = new_evar evd env ~src:(evar_source evk evd) - ~filter:(Some filter) evi.evar_concl in + ~filter:filter evi.evar_concl in let evd = Evd.evar_define evk nc evd in let evk',_ = destEvar nc in evd,evk' @@ -627,15 +627,15 @@ let rec do_projection_effects define_fun env t evd = function let evd = do_projection_effects define_fun env t evd p in let ty = Retyping.get_type_of env (evars_of evd) t in let ty = whd_betadeltaiota env (evars_of evd) ty in - if not (isSort ty) & isEvar evi.evar_concl then + if not (isSort ty) then (* Don't try to instantiate if a sort because if evar_concl is an evar it may commit to a univ level which is not the right one (however, regarding coercions, because t is obtained by unif, we know that no coercion can be inserted) *) let subst = make_pure_subst evi argsv in let ty' = replace_vars subst evi.evar_concl in - let evd = define_fun env (destEvar ty') ty evd in - evd + let ty' = whd_evar (evars_of evd) ty' in + if isEvar ty' then define_fun env (destEvar ty') ty evd else evd else evd @@ -661,19 +661,20 @@ type projectibility_status = | CannotOccur | Projectible of projectibility_kind -let invert_subst env sigma subst t = +let invert_subst env k sigma subst_in_env t_in_env_extended_with_k_binders = let effects = ref [] in let rec aux k t = let t = whd_evar sigma t in match kind_of_term t with | Rel i when i>k -> - project_with_effects env sigma effects (mkRel (i-k)) subst + project_with_effects env sigma effects (mkRel (i-k)) subst_in_env | Var id -> - project_with_effects env sigma effects t subst + project_with_effects env sigma effects t subst_in_env | _ -> map_constr_with_binders succ aux k t in try - let c = aux 0 t in Projectible (UniqueProjection (c,!effects)) + let c = aux k t_in_env_extended_with_k_binders in + Projectible (UniqueProjection (c,!effects)) with | NotUnique -> Projectible NoUniqueProjection | Not_found -> CannotOccur @@ -704,7 +705,7 @@ let solve_evar_evar_l2r f env evd (evk1,args1) (evk2,args2) t = let evi2 = Evd.find (evars_of evd) evk2 in let subst2 = make_projectable_subst (evars_of evd) evi2 args2 in let proj1 = - array_map_to_list (invert_subst env (evars_of evd) subst2) args1 in + array_map_to_list (invert_subst env 0 (evars_of evd) subst2) args1 in let filter1 = List.map filter_of_projection proj1 in try (* Instantiate ev2 with (a restriction of) ev1 if uniquely projectable *) @@ -724,6 +725,15 @@ let solve_evar_evar f env evd ev1 ev2 = with CannotProject filter2 -> postpone_evar_evar env evd filter1 ev1 filter2 ev2 +let add_evar_constraint env evd (evk,argsv) rhs = + let evi = Evd.find (evars_of evd) evk in + let evd,evk,args = + restrict_upon_filter evd evi evk + (fun a -> not (isRel a || isVar a) || dependent a rhs) + (Array.to_list argsv) in + let evar = mkEvar (evk,Array.of_list args) in + Evd.add_conv_pb (Reduction.CONV,env,evar,rhs) evd + (* We try to instantiate the evar assuming the body won't depend * on arguments that are not Rels or Vars, or appearing several times * (i.e. we tackle a generalization of Miller-Pfenning patterns unification) @@ -776,16 +786,16 @@ let rec invert_instance env evd (evk,_ as ev) subst rhs = | Var id -> project_variable env' t k t | Evar (evk',args' as ev') -> (* Evar/Evar problem (but left evar is virtual) *) - let subst = List.map (fun (id,(idc,c)) -> (id,(idc,lift k c))) subst in +(* let subst = List.map (fun (id,(idc,c)) -> (id,(idc,lift k c))) subst in*) let projs' = - array_map_to_list (invert_subst env (evars_of !evdref) subst) args' + array_map_to_list (invert_subst env k (evars_of !evdref) subst) args' in let filter' = List.map filter_of_projection projs' in (try (* Try to project (a restriction of) the right evar *) let projs' = effective_projections projs' in let evd,args' = - list_fold_map (instance_of_projection evar_define env t) + list_fold_map (instance_of_projection evar_define env' t) !evdref projs' in let evd,evk' = do_restrict_hyps !evdref evk' filter' in @@ -850,12 +860,7 @@ and evar_define env (evk,argsv as ev) rhs evd = Evd.evar_define evk body evd' with | NotYetSolvable -> - let evd,evk,args = - restrict_upon_filter evd evi evk - (fun a -> (isRel a or isVar a) & not (dependent a rhs)) - (Array.to_list argsv) in - let evar = mkEvar (evk,Array.of_list args) in - Evd.add_conv_pb (Reduction.CONV,env,evar,rhs) evd + add_evar_constraint env evd ev rhs | NotClean t -> error_not_clean env (evars_of evd) evk t (evar_source evk evd) @@ -967,7 +972,7 @@ let solve_refl conv_algo env evd evk argsv1 argsv2 = (* Rq: uncomplete algorithm if pbty = CONV_X_LEQ ! *) let solve_simple_eqn conv_algo env evd (pbty,(evk1,args1 as ev1),t2) = try - let t2 = nf_evar (evars_of evd) t2 in + let t2 = whd_evar (evars_of evd) t2 in let evd = match kind_of_term t2 with | Evar (evk2,args2 as ev2) -> if evk1 = evk2 then diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index a3c3267e1..36b674fe5 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -34,10 +34,10 @@ val new_untyped_evar : unit -> existential_key (***********************************************************) (* Creating a fresh evar given their type and context *) val new_evar : - evar_defs -> env -> ?src:loc * hole_kind -> ?filter:bool list option -> types -> evar_defs * constr + evar_defs -> env -> ?src:loc * hole_kind -> ?filter:bool list -> types -> evar_defs * constr (* the same with side-effects *) val e_new_evar : - evar_defs ref -> env -> ?src:loc * hole_kind -> ?filter:bool list option -> types -> constr + evar_defs ref -> env -> ?src:loc * hole_kind -> ?filter:bool list -> types -> constr (* Create a fresh evar in a context different from its definition context: [new_evar_instance sign evd ty inst] creates a new evar of context @@ -46,7 +46,7 @@ val e_new_evar : of [inst] are typed in the occurrence context and their type (seen as a telescope) is [sign] *) val new_evar_instance : - named_context_val -> evar_defs -> types -> ?src:loc * hole_kind -> ?filter:bool list option -> constr list -> evar_defs * constr + named_context_val -> evar_defs -> types -> ?src:loc * hole_kind -> ?filter:bool list -> constr list -> evar_defs * constr (***********************************************************) (* Instantiate evars *) diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 06b3a542d..300b4c8e6 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -425,7 +425,7 @@ let evar_define evk body evd = evars = define evd.evars evk body; last_mods = evk :: evd.last_mods } -let evar_declare hyps evk ty ?(src=(dummy_loc,InternalHole)) ?(filter=None) evd = +let evar_declare hyps evk ty ?(src=(dummy_loc,InternalHole)) ?filter evd = let filter = if filter = None then List.map (fun _ -> true) (named_context_of_val hyps) diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 1bf737609..b5a36c1f3 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -158,7 +158,7 @@ val is_undefined_evar : evar_defs -> constr -> bool val undefined_evars : evar_defs -> evar_defs val evar_declare : named_context_val -> evar -> types -> ?src:loc * hole_kind -> - ?filter:bool list option -> evar_defs -> evar_defs + ?filter:bool list -> evar_defs -> evar_defs val evar_define : evar -> constr -> evar_defs -> evar_defs val evar_source : existential_key -> evar_defs -> loc * hole_kind diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v index 27470730d..e117bf62f 100644 --- a/test-suite/success/evars.v +++ b/test-suite/success/evars.v @@ -88,6 +88,14 @@ Parameter Out : STATE -> Output. Check fun (s : STATE) (reg : Input) => reg = Out s. End A. +(* The return predicate found should be: "in _=U return U" *) +(* (feature already available in V8.0) *) + +Definition g (T1 T2:Type) (x:T1) (e:T1=T2) : T2 := + match e with + | refl_equal => x + end. + (* An example extracted from FMapAVL which (may) test restriction on evars problems of the form ?n[args1]=?n[args2] with distinct args1 and args2 *) @@ -121,9 +129,9 @@ Check (fun (A:Set) (a b x:A) (l:list A) (* An example from NMake (simplified), that uses restriction in solve_refl *) -Parameter g:(nat->nat)->(nat->nat). +Parameter h:(nat->nat)->(nat->nat). Fixpoint G p cont {struct p} := - g (fun n => match p with O => cont | S p => G p cont end n). + h (fun n => match p with O => cont | S p => G p cont end n). (* An example from Bordeaux/Cantor that applies evar restriction below a binder *) @@ -150,3 +158,31 @@ Axiom merge_correct : match merge eqA eqB l1 l2 with _ => True end. Unset Implicit Arguments. +(* An example from Bordeaux/Additions that tests restriction below binders *) + +Section Additions_while. + +Variable A : Set. +Variables P Q : A -> Prop. +Variable le : A -> A -> Prop. +Hypothesis Q_dec : forall s : A, P s -> {Q s} + {~ Q s}. +Hypothesis le_step : forall s : A, ~ Q s -> P s -> {s' | P s' /\ le s' s}. +Hypothesis le_wf : well_founded le. + +Lemma loopexec : forall s : A, P s -> {s' : A | P s' /\ Q s'}. +refine + (well_founded_induction_type le_wf (fun s => _ -> {s' : A | _ /\ _}) + (fun s hr i => + match Q_dec s i with + | left _ => _ + | right _ => + match le_step s _ _ with + | exist s' h' => + match hr s' _ _ with + | exist s'' _ => exist _ s'' _ + end + end + end)). +Abort. + +End Additions_while. |