|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open CErrors
open Pp
open Util
open Names
open Constr
open Context
open Termops
open Environ
open EConstr
open Vars
open Namegen
open Evd
open Reduction
open Reductionops
open Evarutil
open Evardefine
open Evarsolve
open Pretype_errors
open Retyping
open Coercion
open Recordops
open Locus
open Locusops
open Find_subterm
type metabinding = (metavariable * EConstr.constr * (instance_constraint * instance_typing_status))
type subst0 =
(evar_map *
metabinding list *
(Environ.env * EConstr.existential * EConstr.t) list)
module RelDecl = Context.Rel.Declaration
module NamedDecl = Context.Named.Declaration
let keyed_unification = ref (false)
let () = Goptions.(declare_bool_option {
optdepr = false;
optname = "Unification is keyed";
optkey = ["Keyed";"Unification"];
optread = (fun () -> !keyed_unification);
optwrite = (fun a -> keyed_unification:=a);
})
let is_keyed_unification () = !keyed_unification
let debug_unification = ref (false)
let () = Goptions.(declare_bool_option {
optdepr = false;
optname =
"Print states sent to tactic unification";
optkey = ["Debug";"Tactic";"Unification"];
optread = (fun () -> !debug_unification);
optwrite = (fun a -> debug_unification:=a);
})
(** Making this unification algorithm correct w.r.t. the evar-map abstraction
breaks too much stuff. So we redefine incorrect functions here. *)
let unsafe_occur_meta_or_existential c =
let c = EConstr.Unsafe.to_constr c in
let rec occrec c = match Constr.kind c with
| Evar _ -> raise Occur
| Meta _ -> raise Occur
| _ -> Constr.iter occrec c
in try occrec c; false with Occur -> true
let occur_meta_or_undefined_evar evd c =
(* This is performance-critical. Using the evar-insensitive API changes the
resulting heuristic. *)
let c = EConstr.Unsafe.to_constr c in
let rec occrec c = match Constr.kind c with
| Meta _ -> raise Occur
| Evar (ev,args) ->
(match evar_body (Evd.find evd ev) with
| Evar_defined c ->
occrec (EConstr.Unsafe.to_constr c); Array.iter occrec args
| Evar_empty -> raise Occur)
| _ -> Constr.iter occrec c
in try occrec c; false with Occur | Not_found -> true
let occur_meta_evd sigma mv c =
let rec occrec c =
(* Note: evars are not instantiated by terms with metas *)
let c = whd_meta sigma c in
match EConstr.kind sigma c with
| Meta mv' when Int.equal mv mv' -> raise Occur
| _ -> EConstr.iter sigma occrec c
in try occrec c; false with Occur -> true
(* if lname_typ is [xn,An;..;x1,A1] and l is a list of terms,
gives [x1:A1]..[xn:An]c' such that c converts to ([x1:A1]..[xn:An]c' l) *)
let abstract_scheme env evd c l lname_typ =
let mkLambda_name env (n,a,b) =
mkLambda (map_annot (named_hd env evd a) n, a, b)
in
List.fold_left2
(fun (t,evd) (locc,a) decl ->
let na = RelDecl.get_annot decl in
let ta = RelDecl.get_type decl in
let na = match EConstr.kind evd a with Var id -> {na with binder_name=Name id} | _ -> na in
(* [occur_meta ta] test removed for support of eelim/ecase but consequences
are unclear...
if occur_meta ta then error "cannot find a type for the generalisation"
else *)
if occur_meta evd a then mkLambda_name env (na,ta,t), evd
else
let t', evd' = Find_subterm.subst_closed_term_occ env evd locc a t in
mkLambda_name env (na,ta,t'), evd')
(c,evd)
(List.rev l)
lname_typ
(* Precondition: resulting abstraction is expected to be of type [typ] *)
let abstract_list_all env evd typ c l =
let ctxt,_ = splay_prod_n env evd (List.length l) typ in
let l_with_all_occs = List.map (function a -> (LikeFirst,a)) l in
let p,evd = abstract_scheme env evd c l_with_all_occs ctxt in
let evd,typp =
try Typing.type_of env evd p
with
| UserError _ ->
error_cannot_find_well_typed_abstraction env evd p l None
| Type_errors.TypeError (env',x) ->
(* FIXME: plug back the typing information *)
error_cannot_find_well_typed_abstraction env evd p l None
| Pretype_errors.PretypeError (env',evd,TypingError x) ->
error_cannot_find_well_typed_abstraction env evd p l (Some (env',x)) in
evd,(p,typp)
let set_occurrences_of_last_arg args =
Evarconv.AtOccurrences AllOccurrences ::
List.tl (Array.map_to_list (fun _ -> Evarconv.Unspecified Abstraction.Abstract) args)
let occurrence_test _ _ _ env sigma _ c1 c2 =
match EConstr.eq_constr_universes env sigma c1 c2 with
| None -> false, sigma
| Some cstr ->
try true, Evd.add_universe_constraints sigma cstr
with UniversesDiffer -> false, sigma
let abstract_list_all_with_dependencies env evd typ c l =
let (evd, ev) = new_evar env evd typ in
let evd,ev' = evar_absorb_arguments env evd (destEvar evd ev) l in
let n = List.length l in
let argoccs = set_occurrences_of_last_arg (Array.sub (snd ev') 0 n) in
let evd,b =
Evarconv.second_order_matching
(Evarconv.default_flags_of TransparentState.empty)
env evd ev' (occurrence_test, argoccs) c in
if b then
let p = nf_evar evd ev in
evd, p
else error_cannot_find_well_typed_abstraction env evd
c l None
(* A refinement of [conv_pb]: the integers tells how many arguments
were applied in the context of the conversion problem; if the number
is non zero, steps of eta-expansion will be allowed
*)
let opp_status = function
| IsSuperType -> IsSubType
| IsSubType -> IsSuperType
| Conv -> Conv
let add_type_status (x,y) = ((x,TypeNotProcessed),(y,TypeNotProcessed))
let extract_instance_status = function
| CUMUL -> add_type_status (IsSubType, IsSuperType)
| CONV -> add_type_status (Conv, Conv)
let rec subst_meta_instances sigma bl c =
match EConstr.kind sigma c with
| Meta i ->
let select (j,_,_) = Int.equal i j in
(try pi2 (List.find select bl) with Not_found -> c)
| _ -> EConstr.map sigma (subst_meta_instances sigma bl) c
(** [env] should be the context in which the metas live *)
let pose_all_metas_as_evars env evd t =
let evdref = ref evd in
let rec aux t = match EConstr.kind !evdref t with
| Meta mv ->
(match Evd.meta_opt_fvalue !evdref mv with
| Some ({rebus=c},_) -> c
| None ->
let {rebus=ty;freemetas=mvs} = Evd.meta_ftype evd mv in
let ty = if Evd.Metaset.is_empty mvs then ty else aux ty in
let ty = nf_betaiota env evd ty in
let src = Evd.evar_source_of_meta mv !evdref in
let evd, ev = Evarutil.new_evar env !evdref ~src ty in
evdref := meta_assign mv (ev,(Conv,TypeNotProcessed)) evd;
ev)
| _ ->
EConstr.map !evdref aux t in
let c = aux t in
(* side-effect *)
(!evdref, c)
let solve_pattern_eqn_array (env,nb) f l c (sigma,metasubst,evarsubst : subst0) =
match EConstr.kind sigma f with
| Meta k ->
(* We enforce that the Meta does not depend on the [nb]
extra assumptions added by unification to the context *)
let env' = pop_rel_context nb env in
let sigma,c = pose_all_metas_as_evars env' sigma c in
let c = solve_pattern_eqn env sigma l c in
let pb = (Conv,TypeNotProcessed) in
if noccur_between sigma 1 nb c then
sigma,(k,lift (-nb) c,pb)::metasubst,evarsubst
else
let l = List.map of_alias l in
error_cannot_unify_local env sigma (applist (f, l),c,c)
| Evar ev ->
let env' = pop_rel_context nb env in
let sigma,c = pose_all_metas_as_evars env' sigma c in
sigma,metasubst,(env,ev,solve_pattern_eqn env sigma l c)::evarsubst
| _ -> assert false
let push d (env,n) = (push_rel_assum d env,n+1)
(*******************************)
(* Unification à l'ordre 0 de m et n: [unify_0 env sigma cv_pb m n]
renvoie deux listes:
metasubst:(int*constr)list récolte les instances des (Meta k)
evarsubst:(constr*constr)list récolte les instances des (Const "?k")
Attention : pas d'unification entre les différences instances d'une
même meta ou evar, il peut rester des doublons *)
(* Unification order: *)
(* Left to right: unifies first argument and then the other arguments *)
(*let unify_l2r x = List.rev x
(* Right to left: unifies last argument and then the other arguments *)
let unify_r2l x = x
let sort_eqns = unify_r2l
*)
type allowed_evars =
| AllowAll
| AllowFun of (Evar.t -> bool)
type core_unify_flags = {
modulo_conv_on_closed_terms : TransparentState.t option;
(* What this flag controls was activated with all constants transparent, *)
(* even for auto, since Coq V5.10 *)
use_metas_eagerly_in_conv_on_closed_terms : bool;
(* This refinement of the conversion on closed terms is activable *)
(* (and activated for apply, rewrite but not auto since Feb 2008 for 8.2) *)
use_evars_eagerly_in_conv_on_closed_terms : bool;
modulo_delta : TransparentState.t;
(* This controls which constants are unfoldable; this is on for apply *)
(* (but not simple apply) since Feb 2008 for 8.2 *)
modulo_delta_types : TransparentState.t;
check_applied_meta_types : bool;
(* This controls whether meta's applied to arguments have their *)
(* type unified with the type of their instance *)
use_pattern_unification : bool;
(* This solves pattern "?n x1 ... xn = t" when the xi are distinct rels *)
(* This says if pattern unification is tried *)
use_meta_bound_pattern_unification : bool;
(* This is implied by use_pattern_unification; has no particular *)
(* reasons to be set differently than use_pattern_unification *)
(* except for compatibility of "auto". *)
(* This was on for all tactics, including auto, since Sep 2006 for 8.1 *)
(* This allowed for instance to unify "forall x:?A, ?B x" with "A' -> B'" *)
(* when ?B is a Meta. *)
allowed_evars : allowed_evars;
(* Evars that are allowed to be instantiated *)
(* Useful e.g. for autorewrite *)
restrict_conv_on_strict_subterms : bool;
(* No conversion at the root of the term; potentially useful for rewrite *)
modulo_betaiota : bool;
(* Support betaiota in the reduction *)
(* Note that zeta is always used *)
modulo_eta : bool;
(* Support eta in the reduction *)
}
type unify_flags = {
core_unify_flags : core_unify_flags;
(* Governs unification of problems of the form "t(?x) = u(?x)" in apply *)
merge_unify_flags : core_unify_flags;
(* These are the flags to be used when trying to unify *)
(* several instances of the same metavariable *)
(* Typical situation is when we give a pattern to be matched *)
(* syntactically against a subterm but we want the metas of the *)
(* pattern to be modulo convertibility *)
subterm_unify_flags : core_unify_flags;
(* Governs unification of problems of the form "?X a1..an = u" in apply, *)
(* hence in rewrite and elim *)
allow_K_in_toplevel_higher_order_unification : bool;
(* Tells in second-order abstraction over subterms which have not *)
(* been found in term are allowed (used for rewrite, elim, or *)
(* apply with a lemma whose type has the form "?X a1 ... an") *)
resolve_evars : bool
(* This says if type classes instances resolution must be used to infer *)
(* the remaining evars *)
}
(* Default flag for unifying a type against a type (e.g. apply) *)
(* We set all conversion flags (no flag should be modified anymore) *)
let default_core_unify_flags () =
let ts = TransparentState.full in {
modulo_conv_on_closed_terms = Some ts;
use_metas_eagerly_in_conv_on_closed_terms = true;
use_evars_eagerly_in_conv_on_closed_terms = false;
modulo_delta = ts;
modulo_delta_types = ts;
check_applied_meta_types = true;
use_pattern_unification = true;
use_meta_bound_pattern_unification = true;
allowed_evars = AllowAll;
restrict_conv_on_strict_subterms = false;
modulo_betaiota = true;
modulo_eta = true;
}
(* Default flag for first-order or second-order unification of a type *)
(* against another type (e.g. apply) *)
(* We set all conversion flags (no flag should be modified anymore) *)
let default_unify_flags () =
let flags = default_core_unify_flags () in {
core_unify_flags = flags;
merge_unify_flags = flags;
subterm_unify_flags = { flags with modulo_delta = TransparentState.var_full };
allow_K_in_toplevel_higher_order_unification = false; (* Why not? *)
resolve_evars = false
}
let set_no_delta_core_flags flags = { flags with
modulo_conv_on_closed_terms = None;
modulo_delta = TransparentState.empty;
check_applied_meta_types = false;
use_pattern_unification = false;
use_meta_bound_pattern_unification = true;
modulo_betaiota = false
}
let set_no_delta_flags flags = {
core_unify_flags = set_no_delta_core_flags flags.core_unify_flags;
merge_unify_flags = set_no_delta_core_flags flags.merge_unify_flags;
subterm_unify_flags = set_no_delta_core_flags flags.subterm_unify_flags;
allow_K_in_toplevel_higher_order_unification =
flags.allow_K_in_toplevel_higher_order_unification;
resolve_evars = flags.resolve_evars
}
(* For the first phase of keyed unification, restrict
to conversion (including beta-iota) only on closed terms *)
let set_no_delta_open_core_flags flags = { flags with
modulo_delta = TransparentState.empty;
modulo_betaiota = false;
}
let set_no_delta_open_flags flags = {
core_unify_flags = set_no_delta_open_core_flags flags.core_unify_flags;
merge_unify_flags = set_no_delta_open_core_flags flags.merge_unify_flags;
subterm_unify_flags = set_no_delta_open_core_flags flags.subterm_unify_flags;
allow_K_in_toplevel_higher_order_unification =
flags.allow_K_in_toplevel_higher_order_unification;
resolve_evars = flags.resolve_evars
}
(* Default flag for the "simple apply" version of unification of a *)
(* type against a type (e.g. apply) *)
(* We set only the flags available at the time the new "apply" extended *)
(* out of "simple apply" *)
let default_no_delta_core_unify_flags () = { (default_core_unify_flags ()) with
modulo_delta = TransparentState.empty;
check_applied_meta_types = false;
use_pattern_unification = false;
use_meta_bound_pattern_unification = true;
modulo_betaiota = false;
}
let default_no_delta_unify_flags ts =
let flags = default_no_delta_core_unify_flags () in
let flags = { flags with
modulo_conv_on_closed_terms = Some ts;
modulo_delta_types = ts
} in
{
core_unify_flags = flags;
merge_unify_flags = flags;
subterm_unify_flags = flags;
allow_K_in_toplevel_higher_order_unification = false;
resolve_evars = false
}
let allow_new_evars sigma =
let undefined = Evd.undefined_map sigma in
AllowFun (fun evk -> not (Evar.Map.mem evk undefined))
(* Default flags for looking for subterms in elimination tactics *)
(* Not used in practice at the current date, to the exception of *)
(* allow_K) because only closed terms are involved in *)
(* induction/destruct/case/elim and w_unify_to_subterm_list does not *)
(* call w_unify for induction/destruct/case/elim (13/6/2011) *)
let elim_core_flags sigma = { (default_core_unify_flags ()) with
modulo_betaiota = false;
allowed_evars = allow_new_evars sigma;
}
let elim_flags_evars sigma =
let flags = elim_core_flags sigma in {
core_unify_flags = flags;
merge_unify_flags = flags;
subterm_unify_flags = { flags with modulo_delta = TransparentState.empty };
allow_K_in_toplevel_higher_order_unification = true;
resolve_evars = false
}
let elim_flags () = elim_flags_evars Evd.empty
let elim_no_delta_core_flags () = { (elim_core_flags Evd.empty) with
modulo_delta = TransparentState.empty;
check_applied_meta_types = false;
use_pattern_unification = false;
modulo_betaiota = false;
}
let elim_no_delta_flags () =
let flags = elim_no_delta_core_flags () in {
core_unify_flags = flags;
merge_unify_flags = flags;
subterm_unify_flags = flags;
allow_K_in_toplevel_higher_order_unification = true;
resolve_evars = false
}
(* On types, we don't restrict unification, but possibly for delta *)
let set_flags_for_type flags = { flags with
modulo_delta = flags.modulo_delta_types;
modulo_conv_on_closed_terms = Some flags.modulo_delta_types;
use_pattern_unification = true;
modulo_betaiota = true;
modulo_eta = true;
}
let use_evars_pattern_unification flags =
flags.use_pattern_unification
let use_metas_pattern_unification sigma flags nb l =
flags.use_pattern_unification
|| flags.use_meta_bound_pattern_unification &&
Array.for_all (fun c -> isRel sigma c && destRel sigma c <= nb) l
type key =
| IsKey of CClosure.table_key
| IsProj of Projection.t * EConstr.constr
let expand_table_key env = function
| ConstKey cst -> constant_opt_value_in env cst
| VarKey id -> (try named_body id env with Not_found -> None)
| RelKey _ -> None
let unfold_projection env p stk =
let s = Stack.Proj (p, Cst_stack.empty) in
s :: stk
let expand_key ts env sigma = function
| Some (IsKey k) -> Option.map EConstr.of_constr (expand_table_key env k)
| Some (IsProj (p, c)) ->
let red = Stack.zip sigma (fst (whd_betaiota_deltazeta_for_iota_state ts env sigma
Cst_stack.empty (c, unfold_projection env p [])))
in if EConstr.eq_constr sigma (EConstr.mkProj (p, c)) red then None else Some red
| None -> None
let isApp_or_Proj sigma c =
match kind sigma c with
| App _ | Proj _ -> true
| _ -> false
type unirec_flags = {
at_top: bool;
with_types: bool;
with_cs : bool;
}
let subterm_restriction opt flags =
not opt.at_top && flags.restrict_conv_on_strict_subterms
let key_of env sigma b flags f =
if subterm_restriction b flags then None else
match EConstr.kind sigma f with
| Const (cst, u) when is_transparent env (ConstKey cst) &&
(TransparentState.is_transparent_constant flags.modulo_delta cst
|| Recordops.is_primitive_projection cst) ->
let u = EInstance.kind sigma u in
Some (IsKey (ConstKey (cst, u)))
| Var id when is_transparent env (VarKey id) &&
TransparentState.is_transparent_variable flags.modulo_delta id ->
Some (IsKey (VarKey id))
| Proj (p, c) when Projection.unfolded p
|| (is_transparent env (ConstKey (Projection.constant p)) &&
(TransparentState.is_transparent_constant flags.modulo_delta (Projection.constant p))) ->
Some (IsProj (p, c))
| _ -> None
let translate_key = function
| ConstKey (cst,u) -> ConstKey cst
| VarKey id -> VarKey id
| RelKey n -> RelKey n
let translate_key = function
| IsKey k -> translate_key k
| IsProj (c, _) -> ConstKey (Projection.constant c)
let oracle_order env cf1 cf2 =
match cf1 with
| None ->
(match cf2 with
| None -> None
| Some k2 -> Some false)
| Some k1 ->
match cf2 with
| None -> Some true
| Some k2 ->
match k1, k2 with
| IsProj (p, _), IsKey (ConstKey (p',_))
when Constant.equal (Projection.constant p) p' ->
Some (not (Projection.unfolded p))
| IsKey (ConstKey (p,_)), IsProj (p', _)
when Constant.equal p (Projection.constant p') ->
Some (Projection.unfolded p')
| _ ->
Some (Conv_oracle.oracle_order (fun x -> x)
(Environ.oracle env) false (translate_key k1) (translate_key k2))
let is_rigid_head sigma flags t =
match EConstr.kind sigma t with
| Const (cst,u) -> not (TransparentState.is_transparent_constant flags.modulo_delta cst)
| Ind (i,u) -> true
| Construct _ | Int _ -> true
| Fix _ | CoFix _ -> true
| Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Cast (_, _, _) | Prod _
| Lambda _ | LetIn _ | App (_, _) | Case (_, _, _, _)
| Proj (_, _) -> false (* Why aren't Prod, Sort rigid heads ? *)
let force_eqs c =
let open UnivProblem in
Set.fold
(fun c acc ->
let c' = match c with
(* Should we be forcing weak constraints? *)
| ULub (l, r) | UWeak (l, r) -> UEq (Univ.Universe.make l,Univ.Universe.make r)
| ULe _ | UEq _ -> c
in
Set.add c' acc)
c Set.empty
let constr_cmp pb env sigma flags t u =
let cstrs =
if pb == Reduction.CONV then EConstr.eq_constr_universes env sigma t u
else EConstr.leq_constr_universes env sigma t u
in
match cstrs with
| Some cstrs ->
begin try Some (Evd.add_universe_constraints sigma cstrs)
with Univ.UniverseInconsistency _ -> None
| Evd.UniversesDiffer ->
if is_rigid_head sigma flags t then
try Some (Evd.add_universe_constraints sigma (force_eqs cstrs))
with Univ.UniverseInconsistency _ -> None
else None
end
| None ->
None
let do_reduce ts (env, nb) sigma c =
Stack.zip sigma (fst (whd_betaiota_deltazeta_for_iota_state
ts env sigma Cst_stack.empty (c, Stack.empty)))
let is_evar_allowed flags evk = match flags.allowed_evars with
| AllowAll -> true
| AllowFun f -> f evk
let isAllowedEvar sigma flags c = match EConstr.kind sigma c with
| Evar (evk,_) -> is_evar_allowed flags evk
| _ -> false
let subst_defined_metas_evars sigma (bl,el) c =
(* This seems to be performance-critical, and using the
evar-insensitive primitives blow up the time passed in this
function. *)
let c = EConstr.Unsafe.to_constr c in
let rec substrec c = match Constr.kind c with
| Meta i ->
let select (j,_,_) = Int.equal i j in
substrec (EConstr.Unsafe.to_constr (pi2 (List.find select bl)))
| Evar (evk,args) ->
let eq c1 c2 = Constr.equal c1 (EConstr.Unsafe.to_constr c2) in
let select (_,(evk',args'),_) = Evar.equal evk evk' && Array.for_all2 eq args args' in
(try substrec (EConstr.Unsafe.to_constr (pi3 (List.find select el)))
with Not_found -> Constr.map substrec c)
| _ -> Constr.map substrec c
in try Some (EConstr.of_constr (substrec c)) with Not_found -> None
let check_compatibility env pbty flags (sigma,metasubst,evarsubst : subst0) tyM tyN =
match subst_defined_metas_evars sigma (metasubst,[]) tyM with
| None -> sigma
| Some m ->
match subst_defined_metas_evars sigma (metasubst,[]) tyN with
| None -> sigma
| Some n ->
if is_ground_term sigma m && is_ground_term sigma n then
match infer_conv ~pb:pbty ~ts:flags.modulo_delta_types env sigma m n with
| Some sigma -> sigma
| None -> error_cannot_unify env sigma (m,n)
else sigma
let rec is_neutral env sigma ts t =
let (f, l) = decompose_app_vect sigma t in
match EConstr.kind sigma f with
| Const (c, u) ->
not (Environ.evaluable_constant c env) ||
not (is_transparent env (ConstKey c)) ||
not (TransparentState.is_transparent_constant ts c)
| Var id ->
not (Environ.evaluable_named id env) ||
not (is_transparent env (VarKey id)) ||
not (TransparentState.is_transparent_variable ts id)
| Rel n -> true
| Evar _ | Meta _ -> true
| Case (_, p, c, cl) -> is_neutral env sigma ts c
| Proj (p, c) -> is_neutral env sigma ts c
| Lambda _ | LetIn _ | Construct _ | CoFix _ | Int _ -> false
| Sort _ | Cast (_, _, _) | Prod (_, _, _) | Ind _ -> false (* Really? *)
| Fix _ -> false (* This is an approximation *)
| App _ -> assert false
let is_eta_constructor_app env sigma ts f l1 term =
match EConstr.kind sigma f with
| Construct (((_, i as ind), j), u) when j == 1 ->
let open Declarations in
let mib = lookup_mind (fst ind) env in
(match mib.Declarations.mind_record with
| PrimRecord info when mib.Declarations.mind_finite == Declarations.BiFinite &&
let (_, projs, _, _) = info.(i) in
Array.length projs == Array.length l1 - mib.Declarations.mind_nparams ->
(* Check that the other term is neutral *)
is_neutral env sigma ts term
| _ -> false)
| _ -> false
let eta_constructor_app env sigma f l1 term =
match EConstr.kind sigma f with
| Construct (((_, i as ind), j), u) ->
let mib = lookup_mind (fst ind) env in
(match get_projections env ind with
| Some projs ->
let npars = mib.Declarations.mind_nparams in
let pars, l1' = Array.chop npars l1 in
let arg = Array.append pars [|term|] in
let l2 = Array.map (fun p -> mkApp (mkConstU (Projection.Repr.constant p,u), arg)) projs in
l1', l2
| _ -> assert false)
| _ -> assert false
let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top env cv_pb flags m n =
let rec unirec_rec (curenv,nb as curenvnb) pb opt ((sigma,metasubst,evarsubst) as substn : subst0) curm curn =
let cM = Evarutil.whd_head_evar sigma curm
and cN = Evarutil.whd_head_evar sigma curn in
let () =
if !debug_unification then
Feedback.msg_debug (
Termops.Internal.print_constr_env curenv sigma cM ++ str" ~= " ++
Termops.Internal.print_constr_env curenv sigma cN)
in
match (EConstr.kind sigma cM, EConstr.kind sigma cN) with
| Meta k1, Meta k2 ->
if Int.equal k1 k2 then substn else
let stM,stN = extract_instance_status pb in
let sigma =
if opt.with_types && flags.check_applied_meta_types then
let tyM = Typing.meta_type sigma k1 in
let tyN = Typing.meta_type sigma k2 in
let l, r = if k2 < k1 then tyN, tyM else tyM, tyN in
check_compatibility curenv CUMUL flags substn l r
else sigma
in
if k2 < k1 then sigma,(k1,cN,stN)::metasubst,evarsubst
else sigma,(k2,cM,stM)::metasubst,evarsubst
| Meta k, _
when not (occur_metavariable sigma k cN) (* helps early trying alternatives *) ->
let sigma =
if opt.with_types && flags.check_applied_meta_types then
(try
let tyM = Typing.meta_type sigma k in
let tyN = get_type_of curenv ~lax:true sigma cN in
check_compatibility curenv CUMUL flags substn tyN tyM
with RetypeError _ ->
(* Renounce, maybe metas/evars prevents typing *) sigma)
else sigma
in
(* Here we check that [cN] does not contain any local variables *)
if Int.equal nb 0 then
sigma,(k,cN,snd (extract_instance_status pb))::metasubst,evarsubst
else if noccur_between sigma 1 nb cN then
(sigma,
(k,lift (-nb) cN,snd (extract_instance_status pb))::metasubst,
evarsubst)
else error_cannot_unify_local curenv sigma (m,n,cN)
| _, Meta k
when not (occur_metavariable sigma k cM) (* helps early trying alternatives *) ->
let sigma =
if opt.with_types && flags.check_applied_meta_types then
(try
let tyM = get_type_of curenv ~lax:true sigma cM in
let tyN = Typing.meta_type sigma k in
check_compatibility curenv CUMUL flags substn tyM tyN
with RetypeError _ ->
(* Renounce, maybe metas/evars prevents typing *) sigma)
else sigma
in
(* Here we check that [cM] does not contain any local variables *)
if Int.equal nb 0 then
(sigma,(k,cM,fst (extract_instance_status pb))::metasubst,evarsubst)
else if noccur_between sigma 1 nb cM
then
(sigma,(k,lift (-nb) cM,fst (extract_instance_status pb))::metasubst,
evarsubst)
else error_cannot_unify_local curenv sigma (m,n,cM)
| Evar (evk,_ as ev), Evar (evk',_)
when is_evar_allowed flags evk
&& Evar.equal evk evk' ->
begin match constr_cmp cv_pb env sigma flags cM cN with
| Some sigma ->
sigma, metasubst, evarsubst
| None ->
sigma,metasubst,((curenv,ev,cN)::evarsubst)
end
| Evar (evk,_ as ev), _
when is_evar_allowed flags evk
&& not (occur_evar sigma evk cN) ->
let cmvars = free_rels sigma cM and cnvars = free_rels sigma cN in
if Int.Set.subset cnvars cmvars then
sigma,metasubst,((curenv,ev,cN)::evarsubst)
else error_cannot_unify_local curenv sigma (m,n,cN)
| _, Evar (evk,_ as ev)
when is_evar_allowed flags evk
&& not (occur_evar sigma evk cM) ->
let cmvars = free_rels sigma cM and cnvars = free_rels sigma cN in
if Int.Set.subset cmvars cnvars then
sigma,metasubst,((curenv,ev,cM)::evarsubst)
else error_cannot_unify_local curenv sigma (m,n,cN)
| Sort s1, Sort s2 ->
(try
let s1 = ESorts.kind sigma s1 in
let s2 = ESorts.kind sigma s2 in
let sigma' =
if pb == CUMUL
then Evd.set_leq_sort curenv sigma s1 s2
else Evd.set_eq_sort curenv sigma s1 s2
in (sigma', metasubst, evarsubst)
with e when CErrors.noncritical e ->
error_cannot_unify curenv sigma (m,n))
| Lambda (na,t1,c1), Lambda (__,t2,c2) ->
unirec_rec (push (na,t1) curenvnb) CONV {opt with at_top = true}
(unirec_rec curenvnb CONV {opt with at_top = true; with_types = false} substn t1 t2) c1 c2
| Prod (na,t1,c1), Prod (_,t2,c2) ->
unirec_rec (push (na,t1) curenvnb) pb {opt with at_top = true}
(unirec_rec curenvnb CONV {opt with at_top = true; with_types = false} substn t1 t2) c1 c2
| LetIn (_,a,_,c), _ -> unirec_rec curenvnb pb opt substn (subst1 a c) cN
| _, LetIn (_,a,_,c) -> unirec_rec curenvnb pb opt substn cM (subst1 a c)
(* Fast path for projections. *)
| Proj (p1,c1), Proj (p2,c2) when Constant.equal
(Projection.constant p1) (Projection.constant p2) ->
(try unify_same_proj curenvnb cv_pb {opt with at_top = true}
substn c1 c2
with ex when precatchable_exception ex ->
unify_not_same_head curenvnb pb opt substn cM cN)
(* eta-expansion *)
| Lambda (na,t1,c1), _ when flags.modulo_eta ->
unirec_rec (push (na,t1) curenvnb) CONV {opt with at_top = true} substn
c1 (mkApp (lift 1 cN,[|mkRel 1|]))
| _, Lambda (na,t2,c2) when flags.modulo_eta ->
unirec_rec (push (na,t2) curenvnb) CONV {opt with at_top = true} substn
(mkApp (lift 1 cM,[|mkRel 1|])) c2
(* For records *)
| App (f1, l1), _ when flags.modulo_eta &&
(* This ensures cN is an evar, meta or irreducible constant/variable
and not a constructor. *)
is_eta_constructor_app curenv sigma flags.modulo_delta f1 l1 cN ->
(try
let l1', l2' = eta_constructor_app curenv sigma f1 l1 cN in
let opt' = {opt with at_top = true; with_cs = false} in
Array.fold_left2 (unirec_rec curenvnb CONV opt') substn l1' l2'
with ex when precatchable_exception ex ->
match EConstr.kind sigma cN with
| App(f2,l2) when
(isMeta sigma f2 && use_metas_pattern_unification sigma flags nb l2
|| use_evars_pattern_unification flags && isAllowedEvar sigma flags f2) ->
unify_app_pattern false curenvnb pb opt substn cM f1 l1 cN f2 l2
| _ -> raise ex)
| _, App (f2, l2) when flags.modulo_eta &&
is_eta_constructor_app curenv sigma flags.modulo_delta f2 l2 cM ->
(try
let l2', l1' = eta_constructor_app curenv sigma f2 l2 cM in
let opt' = {opt with at_top = true; with_cs = false} in
Array.fold_left2 (unirec_rec curenvnb CONV opt') substn l1' l2'
with ex when precatchable_exception ex ->
match EConstr.kind sigma cM with
| App(f1,l1) when
(isMeta sigma f1 && use_metas_pattern_unification sigma flags nb l1
|| use_evars_pattern_unification flags && isAllowedEvar sigma flags f1) ->
unify_app_pattern true curenvnb pb opt substn cM f1 l1 cN f2 l2
| _ -> raise ex)
| Case (ci1,p1,c1,cl1), Case (ci2,p2,c2,cl2) ->
(try
if not (eq_ind ci1.ci_ind ci2.ci_ind) then error_cannot_unify curenv sigma (cM,cN);
let opt' = {opt with at_top = true; with_types = false} in
Array.fold_left2 (unirec_rec curenvnb CONV {opt with at_top = true})
(unirec_rec curenvnb CONV opt'
(unirec_rec curenvnb CONV opt' substn p1 p2) c1 c2)
cl1 cl2
with ex when precatchable_exception ex ->
reduce curenvnb pb opt substn cM cN)
| Fix ((ln1,i1),(lna1,tl1,bl1)), Fix ((ln2,i2),(_,tl2,bl2)) when
Int.equal i1 i2 && Array.equal Int.equal ln1 ln2 ->
(try
let opt' = {opt with at_top = true; with_types = false} in
let curenvnb' = Array.fold_right2 (fun na t -> push (na,t)) lna1 tl1 curenvnb in
Array.fold_left2 (unirec_rec curenvnb' CONV opt')
(Array.fold_left2 (unirec_rec curenvnb CONV opt') substn tl1 tl2) bl1 bl2
with ex when precatchable_exception ex ->
reduce curenvnb pb opt substn cM cN)
| CoFix (i1,(lna1,tl1,bl1)), CoFix (i2,(_,tl2,bl2)) when
Int.equal i1 i2 ->
(try
let opt' = {opt with at_top = true; with_types = false} in
let curenvnb' = Array.fold_right2 (fun na t -> push (na,t)) lna1 tl1 curenvnb in
Array.fold_left2 (unirec_rec curenvnb' CONV opt')
(Array.fold_left2 (unirec_rec curenvnb CONV opt') substn tl1 tl2) bl1 bl2
with ex when precatchable_exception ex ->
reduce curenvnb pb opt substn cM cN)
| App (f1,l1), _ when
(isMeta sigma f1 && use_metas_pattern_unification sigma flags nb l1
|| use_evars_pattern_unification flags && isAllowedEvar sigma flags f1) ->
unify_app_pattern true curenvnb pb opt substn cM f1 l1 cN cN [||]
| _, App (f2,l2) when
(isMeta sigma f2 && use_metas_pattern_unification sigma flags nb l2
|| use_evars_pattern_unification flags && isAllowedEvar sigma flags f2) ->
unify_app_pattern false curenvnb pb opt substn cM cM [||] cN f2 l2
| App (f1,l1), App (f2,l2) ->
unify_app curenvnb pb opt substn cM f1 l1 cN f2 l2
| App (f1,l1), Proj(p2,c2) ->
unify_app curenvnb pb opt substn cM f1 l1 cN cN [||]
| Proj (p1,c1), App(f2,l2) ->
unify_app curenvnb pb opt substn cM cM [||] cN f2 l2
| _ ->
unify_not_same_head curenvnb pb opt substn cM cN
and unify_app_pattern dir curenvnb pb opt (sigma, _, _ as substn) cM f1 l1 cN f2 l2 =
let f, l, t = if dir then f1, l1, cN else f2, l2, cM in
match is_unification_pattern curenvnb sigma f (Array.to_list l) t with
| None ->
(match EConstr.kind sigma t with
| App (f',l') ->
if dir then unify_app curenvnb pb opt substn cM f1 l1 t f' l'
else unify_app curenvnb pb opt substn t f' l' cN f2 l2
| Proj _ -> unify_app curenvnb pb opt substn cM f1 l1 cN f2 l2
| _ -> unify_not_same_head curenvnb pb opt substn cM cN)
| Some l ->
solve_pattern_eqn_array curenvnb f l t substn
and unify_app (curenv, nb as curenvnb) pb opt (sigma, metas, evars as substn : subst0) cM f1 l1 cN f2 l2 =
try
let needs_expansion p c' =
match EConstr.kind sigma c' with
| Meta _ -> true
| Evar _ -> true
| Const (c, u) -> Constant.equal c (Projection.constant p)
| _ -> false
in
let expand_proj c c' l =
match EConstr.kind sigma c with
| Proj (p, t) when not (Projection.unfolded p) && needs_expansion p c' ->
(try destApp sigma (Retyping.expand_projection curenv sigma p t (Array.to_list l))
with RetypeError _ -> (* Unification can be called on ill-typed terms, due
to FO and eta in particular, fail gracefully in that case *)
(c, l))
| _ -> (c, l)
in
let f1, l1 = expand_proj f1 f2 l1 in
let f2, l2 = expand_proj f2 f1 l2 in
let opta = {opt with at_top = true; with_types = false} in
let optf = {opt with at_top = true; with_types = true} in
let (f1,l1,f2,l2) = adjust_app_array_size f1 l1 f2 l2 in
if Array.length l1 == 0 then error_cannot_unify (fst curenvnb) sigma (cM,cN)
else
Array.fold_left2 (unirec_rec curenvnb CONV opta)
(unirec_rec curenvnb CONV optf substn f1 f2) l1 l2
with ex when precatchable_exception ex ->
try reduce curenvnb pb {opt with with_types = false} substn cM cN
with ex when precatchable_exception ex ->
try canonical_projections curenvnb pb opt cM cN substn
with ex when precatchable_exception ex ->
expand curenvnb pb {opt with with_types = false} substn cM f1 l1 cN f2 l2
and unify_same_proj (curenv, nb as curenvnb) cv_pb opt substn c1 c2 =
let substn = unirec_rec curenvnb CONV opt substn c1 c2 in
try (* Force unification of the types to fill in parameters *)
let ty1 = get_type_of curenv ~lax:true sigma c1 in
let ty2 = get_type_of curenv ~lax:true sigma c2 in
unify_0_with_initial_metas substn true curenv cv_pb
{ flags with modulo_conv_on_closed_terms = Some TransparentState.full;
modulo_delta = TransparentState.full;
modulo_eta = true;
modulo_betaiota = true }
ty1 ty2
with RetypeError _ -> substn
and unify_not_same_head curenvnb pb opt (sigma, metas, evars as substn : subst0) cM cN =
try canonical_projections curenvnb pb opt cM cN substn
with ex when precatchable_exception ex ->
match constr_cmp cv_pb env sigma flags cM cN with
| Some sigma -> (sigma, metas, evars)
| None ->
try reduce curenvnb pb opt substn cM cN
with ex when precatchable_exception ex ->
let (f1,l1) =
match EConstr.kind sigma cM with App (f,l) -> (f,l) | _ -> (cM,[||]) in
let (f2,l2) =
match EConstr.kind sigma cN with App (f,l) -> (f,l) | _ -> (cN,[||]) in
expand curenvnb pb opt substn cM f1 l1 cN f2 l2
and reduce curenvnb pb opt (sigma, metas, evars as substn) cM cN =
if flags.modulo_betaiota && not (subterm_restriction opt flags) then
let cM' = do_reduce flags.modulo_delta curenvnb sigma cM in
if not (EConstr.eq_constr sigma cM cM') then
unirec_rec curenvnb pb opt substn cM' cN
else
let cN' = do_reduce flags.modulo_delta curenvnb sigma cN in
if not (EConstr.eq_constr sigma cN cN') then
unirec_rec curenvnb pb opt substn cM cN'
else error_cannot_unify (fst curenvnb) sigma (cM,cN)
else error_cannot_unify (fst curenvnb) sigma (cM,cN)
and expand (curenv,_ as curenvnb) pb opt (sigma,metasubst,evarsubst as substn : subst0) cM f1 l1 cN f2 l2 =
let res =
(* Try full conversion on meta-free terms. *)
(* Back to 1995 (later on called trivial_unify in 2002), the
heuristic was to apply conversion on meta-free (but not
evar-free!) terms in all cases (i.e. for apply but also for
auto and rewrite, even though auto and rewrite did not use
modulo conversion in the rest of the unification
algorithm). By compatibility we need to support this
separately from the main unification algorithm *)
(* The exploitation of known metas has been added in May 2007
(it is used by apply and rewrite); it might now be redundant
with the support for delta-expansion (which is used
essentially for apply)... *)
if subterm_restriction opt flags then None else
match flags.modulo_conv_on_closed_terms with
| None -> None
| Some convflags ->
let subst = ((if flags.use_metas_eagerly_in_conv_on_closed_terms then metasubst else ms), (if flags.use_evars_eagerly_in_conv_on_closed_terms then evarsubst else es)) in
match subst_defined_metas_evars sigma subst cM with
| None -> (* some undefined Metas in cM *) None
| Some m1 ->
match subst_defined_metas_evars sigma subst cN with
| None -> (* some undefined Metas in cN *) None
| Some n1 ->
(* No subterm restriction there, too much incompatibilities *)
let sigma =
if opt.with_types then
try (* Ensure we call conversion on terms of the same type *)
let tyM = get_type_of curenv ~lax:true sigma m1 in
let tyN = get_type_of curenv ~lax:true sigma n1 in
check_compatibility curenv CUMUL flags substn tyM tyN
with RetypeError _ ->
(* Renounce, maybe metas/evars prevents typing *) sigma
else sigma
in
match infer_conv ~pb ~ts:convflags curenv sigma m1 n1 with
| Some sigma ->
Some (sigma, metasubst, evarsubst)
| None ->
if is_ground_term sigma m1 && is_ground_term sigma n1 then
error_cannot_unify curenv sigma (cM,cN)
else None
in
match res with
| Some substn -> substn
| None ->
let cf1 = key_of curenv sigma opt flags f1 and cf2 = key_of curenv sigma opt flags f2 in
match oracle_order curenv cf1 cf2 with
| None -> error_cannot_unify curenv sigma (cM,cN)
| Some true ->
(match expand_key flags.modulo_delta curenv sigma cf1 with
| Some c ->
unirec_rec curenvnb pb opt substn
(whd_betaiotazeta sigma (mkApp(c,l1))) cN
| None ->
(match expand_key flags.modulo_delta curenv sigma cf2 with
| Some c ->
unirec_rec curenvnb pb opt substn cM
(whd_betaiotazeta sigma (mkApp(c,l2)))
| None ->
error_cannot_unify curenv sigma (cM,cN)))
| Some false ->
(match expand_key flags.modulo_delta curenv sigma cf2 with
| Some c ->
unirec_rec curenvnb pb opt substn cM
(whd_betaiotazeta sigma (mkApp(c,l2)))
| None ->
(match expand_key flags.modulo_delta curenv sigma cf1 with
| Some c ->
unirec_rec curenvnb pb opt substn
(whd_betaiotazeta sigma (mkApp(c,l1))) cN
| None ->
error_cannot_unify curenv sigma (cM,cN)))
and canonical_projections (curenv, _ as curenvnb) pb opt cM cN (sigma,_,_ as substn) =
let f1 () =
if isApp_or_Proj sigma cM then
let f1l1 = whd_nored_state sigma (cM,Stack.empty) in
if is_open_canonical_projection curenv sigma f1l1 then
let f2l2 = whd_nored_state sigma (cN,Stack.empty) in
solve_canonical_projection curenvnb pb opt cM f1l1 cN f2l2 substn
else error_cannot_unify (fst curenvnb) sigma (cM,cN)
else error_cannot_unify (fst curenvnb) sigma (cM,cN)
in
if not opt.with_cs ||
begin match flags.modulo_conv_on_closed_terms with
| None -> true
| Some _ -> subterm_restriction opt flags
end then
error_cannot_unify (fst curenvnb) sigma (cM,cN)
else
try f1 () with e when precatchable_exception e ->
if isApp_or_Proj sigma cN then
let f2l2 = whd_nored_state sigma (cN, Stack.empty) in
if is_open_canonical_projection curenv sigma f2l2 then
let f1l1 = whd_nored_state sigma (cM, Stack.empty) in
solve_canonical_projection curenvnb pb opt cN f2l2 cM f1l1 substn
else error_cannot_unify (fst curenvnb) sigma (cM,cN)
else error_cannot_unify (fst curenvnb) sigma (cM,cN)
and solve_canonical_projection curenvnb pb opt cM f1l1 cN f2l2 (sigma,ms,es) =
let (ctx,t,c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) =
try Evarconv.check_conv_record (fst curenvnb) sigma f1l1 f2l2
with Not_found -> error_cannot_unify (fst curenvnb) sigma (cM,cN)
in
if Reductionops.Stack.compare_shape ts ts1 then
let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in
let (evd,ks,_) =
List.fold_left
(fun (evd,ks,m) b ->
if match n with Some n -> Int.equal m n | None -> false then
(evd,t2::ks, m-1)
else
let mv = new_meta () in
let evd' = meta_declare mv (substl ks b) evd in
(evd', mkMeta mv :: ks, m - 1))
(sigma,[],List.length bs) bs
in
try
let opt' = {opt with with_types = false} in
let substn = Reductionops.Stack.fold2
(fun s u1 u -> unirec_rec curenvnb pb opt' s u1 (substl ks u))
(evd,ms,es) us2 us in
let substn = Reductionops.Stack.fold2
(fun s u1 u -> unirec_rec curenvnb pb opt' s u1 (substl ks u))
substn params1 params in
let substn = Reductionops.Stack.fold2 (fun s u1 u2 -> unirec_rec curenvnb pb opt' s u1 u2) substn ts ts1 in
let app = mkApp (c, Array.rev_of_list ks) in
(* let substn = unirec_rec curenvnb pb b false substn t cN in *)
unirec_rec curenvnb pb opt' substn c1 app
with Reductionops.Stack.IncompatibleFold2 ->
error_cannot_unify (fst curenvnb) sigma (cM,cN)
else error_cannot_unify (fst curenvnb) sigma (cM,cN)
in
if !debug_unification then Feedback.msg_debug (str "Starting unification");
let opt = { at_top = conv_at_top; with_types = false; with_cs = true } in
try
let res =
if subterm_restriction opt flags ||
occur_meta_or_undefined_evar sigma m || occur_meta_or_undefined_evar sigma n
then
None
else
let ans = match flags.modulo_conv_on_closed_terms with
| Some convflags -> infer_conv ~pb:cv_pb ~ts:convflags env sigma m n
| _ -> constr_cmp cv_pb env sigma flags m n in
match ans with
| Some sigma -> ans
| None ->
if (match flags.modulo_conv_on_closed_terms, flags.modulo_delta with
| Some cv, dl ->
let open TransparentState in
Id.Pred.subset dl.tr_var cv.tr_var && Cpred.subset dl.tr_cst cv.tr_cst
| None, dl -> TransparentState.is_empty dl)
then error_cannot_unify env sigma (m, n) else None
in
let a = match res with
| Some sigma -> sigma, ms, es
| None -> unirec_rec (env,0) cv_pb opt subst m n in
if !debug_unification then Feedback.msg_debug (str "Leaving unification with success");
a
with e ->
let e = CErrors.push e in
if !debug_unification then Feedback.msg_debug (str "Leaving unification with failure");
iraise e
let unify_0 env sigma = unify_0_with_initial_metas (sigma,[],[]) true env
let left = true
let right = false
let rec unify_with_eta keptside flags env sigma c1 c2 =
(* Question: try whd_all on ci if not two lambdas? *)
match EConstr.kind sigma c1, EConstr.kind sigma c2 with
| (Lambda (na,t1,c1'), Lambda (_,t2,c2')) ->
let env' = push_rel_assum (na,t1) env in
let sigma,metas,evars = unify_0 env sigma CONV flags t1 t2 in
let side,(sigma,metas',evars') =
unify_with_eta keptside flags env' sigma c1' c2'
in (side,(sigma,metas@metas',evars@evars'))
| (Lambda (na,t,c1'),_)->
let env' = push_rel_assum (na,t) env in
let side = left in (* expansion on the right: we keep the left side *)
unify_with_eta side flags env' sigma
c1' (mkApp (lift 1 c2,[|mkRel 1|]))
| (_,Lambda (na,t,c2')) ->
let env' = push_rel_assum (na,t) env in
let side = right in (* expansion on the left: we keep the right side *)
unify_with_eta side flags env' sigma
(mkApp (lift 1 c1,[|mkRel 1|])) c2'
| _ ->
(keptside,unify_0 env sigma CONV flags c1 c2)
(* We solved problems [?n =_pb u] (i.e. [u =_(opp pb) ?n]) and [?n =_pb' u'],
we now compute the problem on [u =? u'] and decide which of u or u' is kept
Rem: the upper constraint is lost in case u <= ?n <= u' (and symmetrically
in the case u' <= ?n <= u)
*)
let merge_instances env sigma flags st1 st2 c1 c2 =
match (opp_status st1, st2) with
| (Conv, Conv) ->
let side = left (* arbitrary choice, but agrees with compatibility *) in
let (side,res) = unify_with_eta side flags env sigma c1 c2 in
(side,Conv,res)
| ((IsSubType | Conv as oppst1),
(IsSubType | Conv)) ->
let res = unify_0 env sigma CUMUL flags c2 c1 in
if eq_instance_constraint oppst1 st2 then (* arbitrary choice *) (left, st1, res)
else if eq_instance_constraint st2 IsSubType then (left, st1, res)
else (right, st2, res)
| ((IsSuperType | Conv as oppst1),
(IsSuperType | Conv)) ->
let res = unify_0 env sigma CUMUL flags c1 c2 in
if eq_instance_constraint oppst1 st2 then (* arbitrary choice *) (left, st1, res)
else if eq_instance_constraint st2 IsSuperType then (left, st1, res)
else (right, st2, res)
| (IsSuperType,IsSubType) ->
(try (left, IsSubType, unify_0 env sigma CUMUL flags c2 c1)
with e when CErrors.noncritical e ->
(right, IsSubType, unify_0 env sigma CUMUL flags c1 c2))
| (IsSubType,IsSuperType) ->
(try (left, IsSuperType, unify_0 env sigma CUMUL flags c1 c2)
with e when CErrors.noncritical e ->
(right, IsSuperType, unify_0 env sigma CUMUL flags c2 c1))
(* Unification
*
* Procedure:
* (1) The function [unify mc wc M N] produces two lists:
* (a) a list of bindings Meta->RHS
* (b) a list of bindings EVAR->RHS
*
* The Meta->RHS bindings cannot themselves contain
* meta-vars, so they get applied eagerly to the other
* bindings. This may or may not close off all RHSs of
* the EVARs. For each EVAR whose RHS is closed off,
* we can just apply it, and go on. For each which
* is not closed off, we need to do a mimic step -
* in general, we have something like:
*
* ?X == (c e1 e2 ... ei[Meta(k)] ... en)
*
* so we need to do a mimic step, converting ?X
* into
*
* ?X -> (c ?z1 ... ?zn)
*
* of the proper types. Then, we can decompose the
* equation into
*
* ?z1 --> e1
* ...
* ?zi --> ei[Meta(k)]
* ...
* ?zn --> en
*
* and keep on going. Whenever we find that a R.H.S.
* is closed, we can, as before, apply the constraint
* directly. Whenever we find an equation of the form:
*
* ?z -> Meta(n)
*
* we can reverse the equation, put it into our metavar
* substitution, and keep going.
*
* The most efficient mimic possible is, for each
* Meta-var remaining in the term, to declare a
* new EVAR of the same type. This is supposedly
* determinable from the clausale form context -
* we look up the metavar, take its type there,
* and apply the metavar substitution to it, to
* close it off. But this might not always work,
* since other metavars might also need to be resolved. *)
let applyHead env evd n c =
let rec apprec n c cty evd =
if Int.equal n 0 then
(evd, c)
else
match EConstr.kind evd (whd_all env evd cty) with
| Prod (_,c1,c2) ->
let (evd',evar) =
Evarutil.new_evar env evd ~src:(Loc.tag Evar_kinds.GoalEvar) c1 in
apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) evd'
| _ -> user_err Pp.(str "Apply_Head_Then")
in
apprec n c (Typing.unsafe_type_of env evd c) evd
let is_mimick_head sigma ts f =
match EConstr.kind sigma f with
| Const (c,u) -> not (TransparentState.is_transparent_constant ts c)
| Var id -> not (TransparentState.is_transparent_variable ts id)
| (Rel _|Construct _|Ind _) -> true
| _ -> false
let try_to_coerce env evd c cty tycon =
let j = make_judge c cty in
let (evd',j') = inh_conv_coerce_rigid_to ~program_mode:false true env evd j tycon in
let evd' = Evarconv.solve_unif_constraints_with_heuristics env evd' in
let evd' = Evd.map_metas_fvalue (fun c -> nf_evar evd' c) evd' in
(evd',j'.uj_val)
let w_coerce_to_type env evd c cty mvty =
let evd,tycon = pose_all_metas_as_evars env evd mvty in
try try_to_coerce env evd c cty tycon
with e when precatchable_exception e ->
(* inh_conv_coerce_rigid_to should have reasoned modulo reduction
but there are cases where it though it was not rigid (like in
fst (nat,nat)) and stops while it could have seen that it is rigid *)
let cty = Tacred.hnf_constr env evd cty in
try_to_coerce env evd c cty tycon
let w_coerce env evd mv c =
let cty = get_type_of env evd c in
let mvty = Typing.meta_type evd mv in
w_coerce_to_type env evd c cty mvty
let unify_to_type env sigma flags c status u =
let sigma, c = refresh_universes (Some false) env sigma c in
let t = get_type_of env sigma (nf_meta sigma c) in
let t = nf_betaiota env sigma (nf_meta sigma t) in
unify_0 env sigma CUMUL flags t u
let unify_type env sigma flags mv status c =
let mvty = Typing.meta_type sigma mv in
let mvty = nf_meta sigma mvty in
unify_to_type env sigma
(set_flags_for_type flags)
c status mvty
(* Move metas that may need coercion at the end of the list of instances *)
let order_metas metas =
let rec order latemetas = function
| [] -> List.rev latemetas
| (_,_,(_,CoerceToType) as meta)::metas ->
order (meta::latemetas) metas
| (_,_,(_,_) as meta)::metas ->
meta :: order latemetas metas
in order [] metas
(* Solve an equation ?n[x1=u1..xn=un] = t where ?n is an evar *)
let solve_simple_evar_eqn flags env evd ev rhs =
match solve_simple_eqn Evarconv.evar_unify flags env evd (None,ev,rhs) with
| UnifFailure (evd,reason) ->
error_cannot_unify env evd ~reason (mkEvar ev,rhs);
| Success evd -> 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 *)
let w_merge env with_types flags (evd,metas,evars : subst0) =
let eflags = Evarconv.default_flags_of flags.modulo_delta_types in
let rec w_merge_rec evd metas evars eqns =
(* Process evars *)
match evars with
| (curenv,(evk,_ as ev),rhs)::evars' ->
if Evd.is_defined evd evk then
let v = mkEvar ev in
let (evd,metas',evars'') =
unify_0 curenv evd CONV flags rhs v in
w_merge_rec evd (metas'@metas) (evars''@evars') eqns
else begin
(* This can make rhs' ill-typed if metas are *)
let rhs' = subst_meta_instances evd metas rhs in
match EConstr.kind evd rhs with
| App (f,cl) when occur_meta evd rhs' ->
if occur_evar evd evk rhs' then
error_occur_check curenv evd evk rhs';
if is_mimick_head evd flags.modulo_delta f then
let evd' =
mimick_undefined_evar evd flags f (Array.length cl) evk in
w_merge_rec evd' metas evars eqns
else
let evd' =
let evd', rhs'' = pose_all_metas_as_evars curenv evd rhs' in
try solve_simple_evar_eqn eflags curenv evd' ev rhs''
with Retyping.RetypeError _ ->
error_cannot_unify curenv evd' (mkEvar ev,rhs'')
in w_merge_rec evd' metas evars' eqns
| _ ->
let evd', rhs'' = pose_all_metas_as_evars curenv evd rhs' in
let evd' =
try solve_simple_evar_eqn eflags curenv evd' ev rhs''
with Retyping.RetypeError _ -> error_cannot_unify curenv evd' (mkEvar ev, rhs'')
in
w_merge_rec evd' metas evars' eqns
end
| [] ->
(* Process metas *)
match metas with
| (mv,c,(status,to_type))::metas ->
let ((evd,c),(metas'',evars'')),eqns =
if with_types && to_type != TypeProcessed then
begin match to_type with
| CoerceToType ->
(* Some coercion may have to be inserted *)
(w_coerce env evd mv c,([],[])),eqns
| _ ->
(* No coercion needed: delay the unification of types *)
((evd,c),([],[])),(mv,status,c)::eqns
end
else
((evd,c),([],[])),eqns
in
if meta_defined evd mv then
let {rebus=c'},(status',_) = meta_fvalue evd mv in
let (take_left,st,(evd,metas',evars')) =
merge_instances env evd flags status' status c' c
in
let evd' =
if take_left then evd
else meta_reassign mv (c,(st,TypeProcessed)) evd
in
w_merge_rec evd' (metas'@metas@metas'') (evars'@evars'') eqns
else
let evd' =
if occur_meta_evd evd mv c then
if isMetaOf evd mv (whd_all env evd c) then evd
else error_cannot_unify env evd (mkMeta mv,c)
else
meta_assign mv (c,(status,TypeProcessed)) evd in
w_merge_rec evd' (metas''@metas) evars'' eqns
| [] ->
(* Process type eqns *)
let rec process_eqns failures = function
| (mv,status,c)::eqns ->
(match (try Inl (unify_type env evd flags mv status c)
with e when CErrors.noncritical e -> Inr e)
with
| Inr e -> process_eqns (((mv,status,c),e)::failures) eqns
| Inl (evd,metas,evars) ->
w_merge_rec evd metas evars (List.map fst failures @ eqns))
| [] ->
(match failures with
| [] -> evd
| ((mv,status,c),e)::_ -> raise e)
in process_eqns [] eqns
and mimick_undefined_evar evd flags hdc nargs sp =
let ev = Evd.find_undefined evd sp in
let sp_env = reset_with_named_context (evar_filtered_hyps ev) env in
let (evd', c) = applyHead sp_env evd nargs hdc in
let (evd'',mc,ec) =
unify_0 sp_env evd' CUMUL flags
(get_type_of sp_env evd' c) ev.evar_concl in
let evd''' = w_merge_rec evd'' mc ec [] in
if evd' == evd'''
then Evd.define sp c evd'''
else Evd.define sp (Evarutil.nf_evar evd''' c) evd''' in
let check_types evd =
let metas = Evd.meta_list evd in
let eqns = List.fold_left (fun acc (mv, b) ->
match b with
| Clval (n, (t, (c, TypeNotProcessed)), v) -> (mv, c, t.rebus) :: acc
| _ -> acc) [] metas
in w_merge_rec evd [] [] eqns
in
let res = (* merge constraints *)
w_merge_rec evd (order_metas metas)
(* Assign evars in the order of assignments during unification *)
(List.rev evars) []
in
if with_types then check_types res else res
let w_unify_meta_types env ?(flags=default_unify_flags ()) evd =
let metas,evd = retract_coercible_metas evd in
w_merge env true flags.merge_unify_flags (evd,metas,[])
(* [w_unify env evd M N]
performs a unification of M and N, generating a bunch of
unification constraints in the process. These constraints
are processed, one-by-one - they may either generate new
bindings, or, if there is already a binding, new unifications,
which themselves generate new constraints. This continues
until we get failure, or we run out of constraints.
[clenv_typed_unify M N clenv] expects in addition that expected
types of metavars are unifiable with the types of their instances *)
let head_app sigma m =
fst (whd_nored_state sigma (m, Stack.empty))
let isEvar_or_Meta sigma c = match EConstr.kind sigma c with
| Evar _ | Meta _ -> true
| _ -> false
let check_types env flags (sigma,_,_ as subst) m n =
if isEvar_or_Meta sigma (head_app sigma m) then
unify_0_with_initial_metas subst true env CUMUL
flags
(get_type_of env sigma n)
(get_type_of env sigma m)
else if isEvar_or_Meta sigma (head_app sigma n) then
unify_0_with_initial_metas subst true env CUMUL
flags
(get_type_of env sigma m)
(get_type_of env sigma n)
else subst
let try_resolve_typeclasses env evd flag m n =
if flag then
Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~split:false
~fail:true env evd
else evd
let w_unify_core_0 env evd with_types cv_pb flags m n =
let (mc1,evd') = retract_coercible_metas evd in
let (sigma,ms,es) = check_types env (set_flags_for_type flags.core_unify_flags) (evd',mc1,[]) m n in
let subst2 =
unify_0_with_initial_metas (sigma,ms,es) false env cv_pb
flags.core_unify_flags m n
in
let evd = w_merge env with_types flags.merge_unify_flags subst2 in
try_resolve_typeclasses env evd flags.resolve_evars m n
let w_typed_unify env evd = w_unify_core_0 env evd true
let w_typed_unify_array env evd flags f1 l1 f2 l2 =
let f1,l1,f2,l2 = adjust_app_array_size f1 l1 f2 l2 in
let (mc1,evd') = retract_coercible_metas evd in
let fold_subst subst m n = unify_0_with_initial_metas subst true env CONV flags.core_unify_flags m n in
let subst = fold_subst (evd', [], []) f1 f2 in
let subst = Array.fold_left2 fold_subst subst l1 l2 in
let evd = w_merge env true flags.merge_unify_flags subst in
try_resolve_typeclasses env evd flags.resolve_evars
(mkApp(f1,l1)) (mkApp(f2,l2))
(* takes a substitution s, an open term op and a closed term cl
try to find a subterm of cl which matches op, if op is just a Meta
FAIL because we cannot find a binding *)
let iter_fail f a =
let n = Array.length a in
let rec ffail i =
if Int.equal i n then user_err Pp.(str "iter_fail")
else
try f a.(i)
with ex when precatchable_exception ex -> ffail (i+1)
in ffail 0
(* make_abstraction: a variant of w_unify_to_subterm which works on
contexts, with evars, and possibly with occurrences *)
let indirectly_dependent sigma c d decls =
not (isVar sigma c) &&
(* This test is not needed if the original term is a variable, but
it is needed otherwise, as e.g. when abstracting over "2" in
"forall H:0=2, H=H:>(0=1+1) -> 0=2." where there is now obvious
way to see that the second hypothesis depends indirectly over 2 *)
let open Context.Named.Declaration in
List.exists (fun d' -> exists (fun c -> Termops.local_occur_var sigma (NamedDecl.get_id d') c) d) decls
let finish_evar_resolution ?(flags=Pretyping.all_and_fail_flags) env current_sigma (pending,c) =
let sigma = Pretyping.solve_remaining_evars flags env current_sigma ~initial:pending in
(sigma, nf_evar sigma c)
let default_matching_core_flags sigma =
let ts = TransparentState.full in {
modulo_conv_on_closed_terms = Some TransparentState.empty;
use_metas_eagerly_in_conv_on_closed_terms = false;
use_evars_eagerly_in_conv_on_closed_terms = false;
modulo_delta = TransparentState.empty;
modulo_delta_types = ts;
check_applied_meta_types = true;
use_pattern_unification = false;
use_meta_bound_pattern_unification = false;
allowed_evars = allow_new_evars sigma;
restrict_conv_on_strict_subterms = false;
modulo_betaiota = false;
modulo_eta = false;
}
let default_matching_merge_flags sigma =
let ts = TransparentState.full in
let flags = default_matching_core_flags sigma in {
flags with
modulo_conv_on_closed_terms = Some ts;
modulo_delta = ts;
modulo_betaiota = true;
modulo_eta = true;
use_pattern_unification = true;
}
let default_matching_flags sigma =
let flags = default_matching_core_flags sigma in {
core_unify_flags = flags;
merge_unify_flags = default_matching_merge_flags sigma;
subterm_unify_flags = flags; (* does not matter *)
resolve_evars = false;
allow_K_in_toplevel_higher_order_unification = false;
}
(* This supports search of occurrences of term from a pattern *)
(* from_prefix is useful e.g. for subterms in an inductive type: we can say *)
(* "destruct t" and it finds "t u" *)
exception PatternNotFound
let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) =
let flags =
if from_prefix_of_ind then
let flags = default_matching_flags pending in
{ flags with core_unify_flags = { flags.core_unify_flags with
modulo_conv_on_closed_terms = Some TransparentState.full;
restrict_conv_on_strict_subterms = true } }
else default_matching_flags pending in
let n = Array.length (snd (decompose_app_vect sigma c)) in
let matching_fun _ t =
try
let t',l2 =
if from_prefix_of_ind then
(* We check for fully applied subterms of the form "u u1 .. un" *)
(* of inductive type knowing only a prefix "u u1 .. ui" *)
let t,l = decompose_app sigma t in
let l1,l2 =
try List.chop n l with Failure _ -> raise (NotUnifiable None) in
if not (List.for_all (fun c -> Vars.closed0 sigma c) l2) then raise (NotUnifiable None)
else
applist (t,l1), l2
else t, [] in
let sigma = w_typed_unify env sigma Reduction.CONV flags c t' in
let ty = Retyping.get_type_of env sigma t in
if not (is_correct_type ty) then raise (NotUnifiable None);
Some(sigma, t, l2)
with
| PretypeError (_,_,CannotUnify (c1,c2,Some e)) ->
raise (NotUnifiable (Some (c1,c2,e)))
(* MS: This is pretty bad, it catches Not_found for example *)
| e when CErrors.noncritical e -> raise (NotUnifiable None) in
let merge_fun c1 c2 =
match c1, c2 with
| Some (evd,c1,x), Some (_,c2,_) ->
begin match infer_conv ~pb:CONV env evd c1 c2 with
| Some evd -> Some (evd, c1, x)
| None -> raise (NotUnifiable None)
end
| Some _, None -> c1
| None, Some _ -> c2
| None, None -> None in
{ match_fun = matching_fun; merge_fun = merge_fun;
testing_state = None; last_found = None },
(fun test -> match test.testing_state with
| None -> None
| Some (sigma,_,l) ->
let c = applist (local_strong whd_meta sigma c, l) in
Some (sigma, c))
let make_eq_test env evd c =
let out cstr =
match cstr.last_found with None -> None | _ -> Some (cstr.testing_state, c)
in
(make_eq_univs_test env evd c, out)
let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
let id =
let t = match ty with Some t -> t | None -> get_type_of env sigma c in
let x = id_of_name_using_hdchar env sigma t name in
let ids = Environ.ids_of_named_context_val (named_context_val env) in
if name == Anonymous then next_ident_away_in_goal x ids else
if mem_named_context_val x (named_context_val env) then
user_err ~hdr:"Unification.make_abstraction_core"
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.61 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
