diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarconv.ml | 8 | ||||
| -rw-r--r-- | pretyping/evarutil.ml | 98 | ||||
| -rw-r--r-- | pretyping/evarutil.mli | 6 | ||||
| -rw-r--r-- | pretyping/unification.ml | 4 |
4 files changed, 92 insertions, 24 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 6664939fb..18cb9457d 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -210,7 +210,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = | Flexible ev1, MaybeFlexible flex2 -> let f1 i = if - is_unification_pattern_evar env ev1 l1 & + is_unification_pattern_evar env ev1 l1 (applist appr2) & not (occur_evar (fst ev1) (applist appr2)) then (* Miller-Pfenning's patterns unification *) @@ -242,7 +242,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = | MaybeFlexible flex1, Flexible ev2 -> let f1 i = if - is_unification_pattern_evar env ev2 l2 & + is_unification_pattern_evar env ev2 l2 (applist appr1) & not (occur_evar (fst ev2) (applist appr1)) then (* Miller-Pfenning's patterns unification *) @@ -310,7 +310,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = | Flexible ev1, Rigid _ -> if - is_unification_pattern_evar env ev1 l1 & + is_unification_pattern_evar env ev1 l1 (applist appr2) & not (occur_evar (fst ev1) (applist appr2)) then (* Miller-Pfenning's patterns unification *) @@ -325,7 +325,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = | Rigid _, Flexible ev2 -> if - is_unification_pattern_evar env ev2 l2 & + is_unification_pattern_evar env ev2 l2 (applist appr1) & not (occur_evar (fst ev2) (applist appr1)) then (* Miller-Pfenning's patterns unification *) diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 551db4e4f..b23c1cc60 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -490,19 +490,30 @@ let clear_hyps_in_evi evdref hyps concl ids = dependencies in variables are canonically associated to the most ancient variable in its family of aliased variables *) -let rec expand_var env x = match kind_of_term x with +let rec expand_var_at_least_once env x = match kind_of_term x with | Rel n -> - begin try match pi2 (lookup_rel n env) with - | Some t when isRel t -> expand_var env (lift n t) - | _ -> x - with Not_found -> x + begin match pi2 (lookup_rel n env) with + | Some t when isRel t or isVar t -> + let t = lift n t in + (try expand_var_at_least_once env t with Not_found -> t) + | _ -> + raise Not_found end | Var id -> begin match pi2 (lookup_named id env) with - | Some t when isVar t -> expand_var env t - | _ -> x + | Some t when isVar t -> + (try expand_var_at_least_once env t with Not_found -> t) + | _ -> + raise Not_found end - | _ -> x + | _ -> + raise Not_found + +let expand_var env x = + try expand_var_at_least_once env x with Not_found -> x + +let expand_var_opt env x = + try Some (expand_var_at_least_once env x) with Not_found -> None let rec expand_vars_in_term env t = match kind_of_term t with | Rel _ | Var _ -> expand_var env t @@ -967,16 +978,71 @@ let head_evar = that we don't care whether args itself contains Rel's or even Rel's distinct from the ones in l *) -let is_unification_pattern_evar env (_,args) l = - let l' = Array.to_list args @ l in - let l' = List.map (expand_var env) l' in - List.for_all (fun a -> isRel a or isVar a) l' && list_distinct l' -let is_unification_pattern env f l = +let rec expand_and_check_vars env = function + | [] -> [] + | a::l -> + if isRel a or isVar a then + let l = expand_and_check_vars env l in + match expand_var_opt env a with + | None -> a :: l + | Some a' when isRel a' or isVar a' -> list_add_set a' l + | _ -> raise Exit + else + raise Exit + +(* +let is_identity_subst env args l = + let n = Array.length args in + (* Check named context from most recent to oldest declaration *) + let rec aux i = function + | [] -> i = 0 + | (id,_,_)::l -> args.(i) = mkVar id && aux (i-1) l in + (* Check named context from oldest to most recent declaration *) + let rec aux' i = function + | [] -> aux i (named_context env) + | _::l -> args.(i) = mkRel (n-i) && aux' (i-1) l in + List.for_all (fun c -> not (array_exists ((=) (expand_var env c)) args)) l && + aux' (n-1) (rel_context env) +*) + +let is_unification_pattern_evar env (_,args) l t = +(* + (* Optimize the most common case *) + List.for_all (fun x -> isRel x || isVar x) l && is_identity_subst env args l + || +*) + let l' = Array.to_list args @ l in + let l'' = try Some (expand_and_check_vars env l') with Exit -> None in + match l'' with + | Some l -> + let deps = + if occur_meta_or_existential t then + l + else + let fv_rels = free_rels t in + let fv_ids = global_vars env t in + List.filter (fun c -> + match kind_of_term c with + | Var id -> List.mem id fv_ids + | Rel n -> Intset.mem n fv_rels + | _ -> assert false) l in + list_distinct deps + | None -> false + +(* + Pp.ppnl (prlist_with_sep spc (fun c -> match kind_of_term c with Rel _ | Var _ -> print_constr c | _ -> str "..") l'); Pp.flush_all (); +*) + +let is_unification_pattern (env,nb) f l t = match kind_of_term f with - | Meta _ -> array_for_all isRel l && array_distinct l - | Evar ev -> is_unification_pattern_evar env ev (Array.to_list l) - | _ -> false + | Meta _ -> + array_for_all (fun c -> isRel c && destRel c <= nb) l + && array_distinct l + | Evar ev -> + is_unification_pattern_evar env ev (Array.to_list l) t + | _ -> + false (* From a unification problem "?X l1 = term1 l2" such that l1 is made of distinct rel's, build "\x1...xn.(term1 l2)" (patterns unification) *) diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 3ed39fc19..9190d8a97 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -91,8 +91,10 @@ val define_evar_as_product : evar_defs -> existential -> evar_defs * types val define_evar_as_lambda : evar_defs -> existential -> evar_defs * types val define_evar_as_sort : evar_defs -> existential -> evar_defs * sorts -val is_unification_pattern_evar : env -> existential -> constr list -> bool -val is_unification_pattern : env -> constr -> constr array -> bool +val is_unification_pattern_evar : env -> existential -> constr list -> + constr -> bool +val is_unification_pattern : env * int -> constr -> constr array -> + constr -> bool val solve_pattern_eqn : env -> constr list -> constr -> constr val evars_of_term : constr -> Intset.t diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 80d7d34a9..e072af362 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -224,12 +224,12 @@ let unify_0_with_initial_metas subst conv_at_top env sigma cv_pb flags m n = (unirec_rec curenvnb topconv true substn p1 p2) c1 c2) cl1 cl2 | App (f1,l1), _ when - isMeta f1 & is_unification_pattern curenv f1 l1 & + isMeta f1 & is_unification_pattern curenvnb f1 l1 cN & not (dependent f1 cN) -> solve_pattern_eqn_array curenvnb sigma f1 l1 cN substn | _, App (f2,l2) when - isMeta f2 & is_unification_pattern curenv f2 l2 & + isMeta f2 & is_unification_pattern curenvnb f2 l2 cM & not (dependent f2 cM) -> solve_pattern_eqn_array curenvnb sigma f2 l2 cM substn |