aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/evarutil.ml5
-rw-r--r--pretyping/evd.ml21
-rw-r--r--pretyping/evd.mli3
-rw-r--r--pretyping/recordops.ml52
-rwxr-xr-xpretyping/recordops.mli9
-rw-r--r--pretyping/reductionops.ml18
-rw-r--r--pretyping/reductionops.mli1
-rw-r--r--pretyping/term_dnet.ml388
-rw-r--r--pretyping/term_dnet.mli110
-rw-r--r--pretyping/termops.ml69
-rw-r--r--pretyping/termops.mli16
11 files changed, 684 insertions, 8 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 6ac857d5c8..dab5c79873 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -71,7 +71,10 @@ let nf_env_evar sigma env =
let nf_evar_info evc info =
{ info with
evar_concl = Reductionops.nf_evar evc info.evar_concl;
- evar_hyps = map_named_val (Reductionops.nf_evar evc) info.evar_hyps}
+ evar_hyps = map_named_val (Reductionops.nf_evar evc) info.evar_hyps;
+ evar_body = match info.evar_body with
+ | Evar_empty -> Evar_empty
+ | Evar_defined c -> Evar_defined (Reductionops.nf_evar evc c) }
let nf_evars evm = Evd.fold (fun ev evi evm' -> Evd.add evm' ev (nf_evar_info evm evi))
evm Evd.empty
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index b29afc0cb3..a76df2dfb9 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -421,11 +421,27 @@ type evar_defs =
history : (existential_key * (loc * hole_kind)) list;
metas : clbinding Metamap.t }
+let subst_named_context_val s = map_named_val (subst_mps s)
+
+let subst_evar_info s evi =
+ let subst_evb = function Evar_empty -> Evar_empty
+ | Evar_defined c -> Evar_defined (subst_mps s c) in
+ { evi with
+ evar_concl = subst_mps s evi.evar_concl;
+ evar_hyps = subst_named_context_val s evi.evar_hyps;
+ evar_body = subst_evb evi.evar_body }
+
+let subst_evar_map sub evm =
+ assert (snd evm = UniverseMap.empty);
+ Evarmap.map (subst_evar_info sub) (fst evm), snd evm
+
let subst_evar_defs_light sub evd =
- assert (evd.evars = (Evarmap.empty,UniverseMap.empty));
+ assert (snd evd.evars = UniverseMap.empty);
assert (evd.conv_pbs = []);
{ evd with
- metas = Metamap.map (map_clb (subst_mps sub)) evd.metas }
+ metas = Metamap.map (map_clb (subst_mps sub)) evd.metas;
+ evars = Evarmap.map (subst_evar_info sub) (fst evd.evars), snd evd.evars
+ }
let create_evar_defs sigma =
{ evars=sigma; conv_pbs=[]; last_mods = []; history=[]; metas=Metamap.empty }
@@ -715,6 +731,7 @@ let pr_evar_defs evd =
if evd.evars = empty then mt() else
str"EVARS:"++brk(0,1)++pr_evar_map evd.evars++fnl() in
let cstrs =
+ if evd.conv_pbs = [] then mt() else
str"CONSTRAINTS:"++brk(0,1)++pr_constraints evd.conv_pbs++fnl() in
let pp_met =
if evd.metas = Metamap.empty then mt() else
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 825096acca..0e3212813d 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -156,7 +156,8 @@ val map_clb : (constr -> constr) -> clbinding -> clbinding
(* Unification state *)
type evar_defs
-(* Assume empty [evar_map] and [conv_pbs] *)
+val subst_evar_map : substitution -> evar_map -> evar_map
+(* Assume empty universe constraints in [evar_map] and [conv_pbs] *)
val subst_evar_defs_light : substitution -> evar_defs -> evar_defs
(* create an [evar_defs] with empty meta map: *)
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index e8860c065c..b6749db198 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -93,6 +93,58 @@ let find_projection = function
| ConstRef cst -> Cmap.find cst !projection_table
| _ -> raise Not_found
+(* Management of a field store : each field + argument of the inferred
+ * records are stored in a discrimination tree *)
+
+let subst_id s (gr,ev,evm) =
+ (fst(subst_global s gr),ev,Evd.subst_evar_map s evm)
+
+module MethodsDnet : Term_dnet.S
+ with type ident = global_reference * Evd.evar * Evd.evar_map
+ = Term_dnet.Make
+ (struct
+ type t = global_reference * Evd.evar * Evd.evar_map
+ let compare = Pervasives.compare
+ let subst = subst_id
+ let constr_of (_,ev,evm) = Evd.evar_concl (Evd.find evm ev)
+ end)
+ (struct
+ let reduce c = Reductionops.head_unfold_under_prod
+ Names.full_transparent_state (Global.env()) Evd.empty c
+ let direction = true
+ end)
+
+let meth_dnet = ref MethodsDnet.empty
+
+open Summary
+
+let _ =
+ declare_summary "record-methods-state"
+ { freeze_function = (fun () -> !meth_dnet);
+ unfreeze_function = (fun m -> meth_dnet := m);
+ init_function = (fun () -> meth_dnet := MethodsDnet.empty);
+ survive_module = false;
+ survive_section = false }
+
+open Libobject
+
+let load_method (_,(ty,id)) =
+ meth_dnet := MethodsDnet.add ty id !meth_dnet
+
+let (in_method,out_method) =
+ declare_object
+ { (default_object "RECMETHODS") with
+ load_function = (fun _ -> load_method);
+ cache_function = load_method;
+ subst_function = (fun (_,s,(ty,id)) -> Mod_subst.subst_mps s ty,subst_id s id);
+ export_function = (fun x -> Some x);
+ classify_function = (fun (_,x) -> Substitute x)
+ }
+
+let methods_matching c = MethodsDnet.search_pattern !meth_dnet c
+
+let declare_method cons ev sign =
+ Lib.add_anonymous_leaf (in_method ((Evd.evar_concl (Evd.find sign ev)),(cons,ev,sign)))
(************************************************************************)
(*s A canonical structure declares "canonical" conversion hints between *)
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 638cc4304e..4d28ee55b1 100755
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -41,6 +41,15 @@ val find_projection_nparams : global_reference -> int
(* raise [Not_found] if not a projection *)
val find_projection : global_reference -> struc_typ
+(* we keep an index (dnet) of record's arguments + fields
+ (=methods). Here is how to declare them: *)
+val declare_method :
+ global_reference -> Evd.evar -> Evd.evar_map -> unit
+ (* and here is how to search for methods matched by a given term: *)
+val methods_matching : constr ->
+ ((global_reference*Evd.evar*Evd.evar_map) *
+ (constr*existential_key)*Termops.subst) list
+
(*s A canonical structure declares "canonical" conversion hints between *)
(* the effective components of a structure and the projections of the *)
(* structure *)
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index f51820bf62..aadb36396a 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -970,3 +970,21 @@ let meta_reducible_instance evd b =
| _ -> map_constr irec u
in
if fm = [] then (* nf_betaiota? *) b.rebus else irec b.rebus
+
+
+let head_unfold_under_prod ts env _ c =
+ let unfold cst =
+ if Cpred.mem cst (snd ts) then
+ match constant_opt_value env cst with
+ | Some c -> c
+ | None -> mkConst cst
+ else mkConst cst in
+ let rec aux c =
+ match kind_of_term c with
+ | Prod (n,t,c) -> mkProd (n,aux t, aux c)
+ | _ ->
+ let (h,l) = decompose_app c in
+ match kind_of_term h with
+ | Const cst -> beta_applist (unfold cst,l)
+ | _ -> c in
+ aux c
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index edbb4f90ca..171967583e 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -215,6 +215,7 @@ val is_trans_fconv : conv_pb -> transparent_state -> env -> evar_map -> constr
val whd_meta : (metavariable * constr) list -> constr -> constr
val plain_instance : (metavariable * constr) list -> constr -> constr
val instance : (metavariable * constr) list -> constr -> constr
+val head_unfold_under_prod : transparent_state -> reduction_function
(*s Heuristic for Conversion with Evar *)
diff --git a/pretyping/term_dnet.ml b/pretyping/term_dnet.ml
new file mode 100644
index 0000000000..656a90c704
--- /dev/null
+++ b/pretyping/term_dnet.ml
@@ -0,0 +1,388 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(* $Id:$ *)
+
+(*i*)
+open Util
+open Term
+open Sign
+open Names
+open Libnames
+open Mod_subst
+open Pp (* debug *)
+(*i*)
+
+
+(* Representation/approximation of terms to use in the dnet:
+ *
+ * - no meta or evar (use ['a pattern] for that)
+ *
+ * - [Rel]s and [Sort]s are not taken into account (that's why we need
+ * a second pass of linear filterin on the results - it's not a perfect
+ * term indexing structure)
+
+ * - Foralls and LetIns are represented by a context DCtx (a list of
+ * generalization, similar to rel_context, and coded with DCons and
+ * DNil). This allows for matching under an unfinished context
+ *)
+
+module DTerm =
+struct
+
+ type 't t =
+ | DRel
+ | DSort
+ | DRef of global_reference
+ | DCtx of 't * 't (* (binding list, subterm) = Prods and LetIns *)
+ | DLambda of 't * 't
+ | DApp of 't * 't (* binary app *)
+ | DCase of case_info * 't * 't * 't array
+ | DFix of int array * int * 't array * 't array
+ | DCoFix of int * 't array * 't array
+
+ (* special constructors only inside the left-hand side of DCtx or
+ DApp. Used to encode lists of foralls/letins/apps as contexts *)
+ | DCons of ('t * 't option) * 't
+ | DNil
+
+ type dconstr = dconstr t
+
+ (* debug *)
+ let rec pr_dconstr f : 'a t -> std_ppcmds = function
+ | DRel -> str "*"
+ | DSort -> str "Sort"
+ | DRef _ -> str "Ref"
+ | DCtx (ctx,t) -> f ctx ++ spc() ++ str "|-" ++ spc () ++ f t
+ | DLambda (t1,t2) -> str "fun"++ spc() ++ f t1 ++ spc() ++ str"->" ++ spc() ++ f t2
+ | DApp (t1,t2) -> f t1 ++ spc() ++ f t2
+ | DCase (_,t1,t2,ta) -> str "case"
+ | DFix _ -> str "fix"
+ | DCoFix _ -> str "cofix"
+ | DCons ((t,dopt),tl) -> f t ++ (match dopt with
+ Some t' -> str ":=" ++ f t'
+ | None -> str "") ++ spc() ++ str "::" ++ spc() ++ f tl
+ | DNil -> str "[]"
+
+ (*
+ * Functional iterators for the t datatype
+ * a.k.a boring and error-prone boilerplate code
+ *)
+
+ let map f = function
+ | (DRel | DSort | DNil | DRef _) as c -> c
+ | DCtx (ctx,c) -> DCtx (f ctx, f c)
+ | DLambda (t,c) -> DLambda (f t, f c)
+ | DApp (t,u) -> DApp (f t,f u)
+ | DCase (ci,p,c,bl) -> DCase (ci, f p, f c, Array.map f bl)
+ | DFix (ia,i,ta,ca) ->
+ DFix (ia,i,Array.map f ta,Array.map f ca)
+ | DCoFix(i,ta,ca) ->
+ DCoFix (i,Array.map f ta,Array.map f ca)
+ | DCons ((t,topt),u) -> DCons ((f t,Option.map f topt), f u)
+
+ let compare = Pervasives.compare
+
+ let fold f acc = function
+ | (DRel | DNil | DSort | DRef _) -> acc
+ | DCtx (ctx,c) -> f (f acc ctx) c
+ | DLambda (t,c) -> f (f acc t) c
+ | DApp (t,u) -> f (f acc t) u
+ | DCase (ci,p,c,bl) -> Array.fold_left f (f (f acc p) c) bl
+ | DFix (ia,i,ta,ca) ->
+ Array.fold_left f (Array.fold_left f acc ta) ca
+ | DCoFix(i,ta,ca) ->
+ Array.fold_left f (Array.fold_left f acc ta) ca
+ | DCons ((t,topt),u) -> f (Option.fold_left f (f acc t) topt) u
+
+ let choose f = function
+ | (DRel | DSort | DNil | DRef _) -> invalid_arg "choose"
+ | DCtx (ctx,c) -> f ctx
+ | DLambda (t,c) -> f t
+ | DApp (t,u) -> f u
+ | DCase (ci,p,c,bl) -> f c
+ | DFix (ia,i,ta,ca) -> f ta.(0)
+ | DCoFix (i,ta,ca) -> f ta.(0)
+ | DCons ((t,topt),u) -> f u
+
+ let fold2 (f:'a -> 'b -> 'c -> 'a) (acc:'a) (c1:'b t) (c2:'c t) : 'a =
+ let head w = map (fun _ -> ()) w in
+ if compare (head c1) (head c2) <> 0
+ then invalid_arg "fold2:compare" else
+ match c1,c2 with
+ | (DRel, DRel | DNil, DNil | DSort, DSort | DRef _, DRef _) -> acc
+ | (DCtx (c1,t1), DCtx (c2,t2)
+ | DApp (c1,t1), DApp (c2,t2)
+ | DLambda (c1,t1), DLambda (c2,t2)) -> f (f acc c1 c2) t1 t2
+ | DCase (ci,p1,c1,bl1),DCase (_,p2,c2,bl2) ->
+ array_fold_left2 f (f (f acc p1 p2) c1 c2) bl1 bl2
+ | DFix (ia,i,ta1,ca1), DFix (_,_,ta2,ca2) ->
+ array_fold_left2 f (array_fold_left2 f acc ta1 ta2) ca1 ca2
+ | DCoFix(i,ta1,ca1), DCoFix(_,ta2,ca2) ->
+ array_fold_left2 f (array_fold_left2 f acc ta1 ta2) ca1 ca2
+ | DCons ((t1,topt1),u1), DCons ((t2,topt2),u2) ->
+ f (Option.fold_left2 f (f acc t1 t2) topt1 topt2) u1 u2
+ | _ -> assert false
+
+ let map2 (f:'a -> 'b -> 'c) (c1:'a t) (c2:'b t) : 'c t =
+ let head w = map (fun _ -> ()) w in
+ if compare (head c1) (head c2) <> 0
+ then invalid_arg "map2_t:compare" else
+ match c1,c2 with
+ | (DRel, DRel | DSort, DSort | DNil, DNil | DRef _, DRef _) as cc ->
+ let (c,_) = cc in c
+ | DCtx (c1,t1), DCtx (c2,t2) -> DCtx (f c1 c2, f t1 t2)
+ | DLambda (t1,c1), DLambda (t2,c2) -> DLambda (f t1 t2, f c1 c2)
+ | DApp (t1,u1), DApp (t2,u2) -> DApp (f t1 t2,f u1 u2)
+ | DCase (ci,p1,c1,bl1), DCase (_,p2,c2,bl2) ->
+ DCase (ci, f p1 p2, f c1 c2, array_map2 f bl1 bl2)
+ | DFix (ia,i,ta1,ca1), DFix (_,_,ta2,ca2) ->
+ DFix (ia,i,array_map2 f ta1 ta2,array_map2 f ca1 ca2)
+ | DCoFix (i,ta1,ca1), DCoFix (_,ta2,ca2) ->
+ DCoFix (i,array_map2 f ta1 ta2,array_map2 f ca1 ca2)
+ | DCons ((t1,topt1),u1), DCons ((t2,topt2),u2) ->
+ DCons ((f t1 t2,Option.lift2 f topt1 topt2), f u1 u2)
+ | _ -> assert false
+
+ let terminal = function
+ | (DRel | DSort | DNil | DRef _) -> true
+ | _ -> false
+end
+
+(*
+ * Terms discrimination nets
+ * Uses the general dnet datatype on DTerm.t
+ * (here you can restart reading)
+ *)
+
+(*
+ * Construction of the module
+ *)
+
+module type IDENT =
+sig
+ type t
+ val compare : t -> t -> int
+ val subst : substitution -> t -> t
+ val constr_of : t -> constr
+end
+
+module type OPT =
+sig
+ val reduce : constr -> constr
+ val direction : bool
+end
+
+module Make =
+ functor (Ident : IDENT) ->
+ functor (Opt : OPT) ->
+struct
+
+ module TDnet : Dnet.S with type ident=Ident.t
+ and type 'a structure = 'a DTerm.t
+ and type meta = metavariable
+ = Dnet.Make(DTerm)(Ident)
+ (struct
+ type t = metavariable
+ let compare = Pervasives.compare
+ end)
+
+ type t = TDnet.t
+
+ type ident = TDnet.ident
+
+ type 'a pattern = 'a TDnet.pattern
+ type term_pattern = term_pattern DTerm.t pattern
+
+ type idset = TDnet.Idset.t
+
+ type result = ident * (constr*existential_key) * Termops.subst
+
+ open DTerm
+ open TDnet
+
+ let rec pat_of_constr c : term_pattern =
+ match kind_of_term c with
+ | Rel _ -> Term DRel
+ | Sort _ -> Term DSort
+ | Var i -> Term (DRef (VarRef i))
+ | Const c -> Term (DRef (ConstRef c))
+ | Ind i -> Term (DRef (IndRef i))
+ | Construct c -> Term (DRef (ConstructRef c))
+ | Term.Meta _ -> assert false
+ | Evar (i,_) -> Meta i
+ | Case (ci,c1,c2,ca) ->
+ Term(DCase(ci,pat_of_constr c1,pat_of_constr c2,Array.map pat_of_constr ca))
+ | Fix ((ia,i),(_,ta,ca)) ->
+ Term(DFix(ia,i,Array.map pat_of_constr ta, Array.map pat_of_constr ca))
+ | CoFix (i,(_,ta,ca)) ->
+ Term(DCoFix(i,Array.map pat_of_constr ta,Array.map pat_of_constr ca))
+ | Cast (c,_,_) -> pat_of_constr c
+ | Lambda (_,t,c) -> Term(DLambda (pat_of_constr t, pat_of_constr c))
+ | (Prod (_,_,_) | LetIn(_,_,_,_)) ->
+ let (ctx,c) = ctx_of_constr (Term DNil) c in Term (DCtx (ctx,c))
+ | App (f,ca) ->
+ Array.fold_left (fun c a -> Term (DApp (c,a)))
+ (pat_of_constr f) (Array.map pat_of_constr ca)
+
+ and ctx_of_constr ctx c : term_pattern * term_pattern =
+ match kind_of_term c with
+ | Prod (_,t,c) -> ctx_of_constr (Term(DCons((pat_of_constr t,None),ctx))) c
+ | LetIn(_,d,t,c) -> ctx_of_constr (Term(DCons((pat_of_constr t, Some (pat_of_constr d)),ctx))) c
+ | _ -> ctx,pat_of_constr c
+
+ let empty_ctx : term_pattern -> term_pattern = function
+ | Meta _ as c -> c
+ | Term (DCtx(_,_)) as c -> c
+ | c -> Term (DCtx (Term DNil, c))
+
+ (*
+ * Basic primitives
+ *)
+
+ let empty = TDnet.empty
+
+ let subst s t =
+ let sleaf id = Ident.subst s id in
+ let snode = function
+ | DTerm.DRef gr -> DTerm.DRef (fst (subst_global s gr))
+ | n -> n in
+ TDnet.map sleaf snode t
+
+ let union = TDnet.union
+
+ let add (c:constr) (id:Ident.t) (dn:t) =
+ let c = Opt.reduce c in
+ let c = empty_ctx (pat_of_constr c) in
+ TDnet.add dn c id
+
+ let new_meta_no =
+ let ctr = ref 0 in
+ fun () -> decr ctr; !ctr
+
+ let new_meta_no = Evarutil.new_untyped_evar
+
+ let neutral_meta = new_meta_no()
+
+ let new_meta () = Meta (new_meta_no())
+ let new_evar () = mkEvar(new_meta_no(),[||])
+
+ let rec remove_cap : term_pattern -> term_pattern = function
+ | Term (DCons (t,u)) -> Term (DCons (t,remove_cap u))
+ | Term DNil -> new_meta()
+ | _ -> assert false
+
+ let under_prod : term_pattern -> term_pattern = function
+ | Term (DCtx (t,u)) -> Term (DCtx (remove_cap t,u))
+ | Meta m -> Term (DCtx(new_meta(), Meta m))
+ | _ -> assert false
+
+ let init = let e = new_meta_no() in (mkEvar (e,[||]),e)
+
+ let rec e_subst_evar i (t:unit->constr) c =
+ match kind_of_term c with
+ | Evar (j,_) when i=j -> t()
+ | _ -> map_constr (e_subst_evar i t) c
+
+ let subst_evar i c = e_subst_evar i (fun _ -> c)
+
+ (* debug *)
+ let rec pr_term_pattern p =
+ (fun pr_t -> function
+ | Term t -> pr_t t
+ | Meta m -> str"["++Util.pr_int (Obj.magic m)++str"]"
+ ) (pr_dconstr pr_term_pattern) p
+
+ let search_pat cpat dpat dn (up,plug) =
+ let whole_c = subst_evar plug cpat up in
+ TDnet.Idset.fold
+ (fun id acc ->
+ let c_id = Opt.reduce (Ident.constr_of id) in
+ let (ctx,wc) =
+ try Termops.align_prod_letin whole_c c_id
+ with Invalid_argument _ -> [],c_id in
+ let up = it_mkProd_or_LetIn up ctx in
+ let wc,whole_c = if Opt.direction then whole_c,wc else wc,whole_c in
+ try (id,(up,plug),Termops.filtering ctx Reduction.CUMUL wc whole_c)::acc
+ with Termops.CannotFilter -> acc
+ ) (TDnet.find_match dpat dn) []
+
+ let fold_pattern_neutral f =
+ fold_pattern (fun m dn acc -> if m=neutral_meta then acc else f m dn acc)
+
+ let fold_pattern_nonlin f =
+ let defined = ref Gmap.empty in
+ fold_pattern_neutral
+ ( fun m dn acc ->
+ let dn = try TDnet.inter dn (Gmap.find m !defined) with Not_found -> dn in
+ defined := Gmap.add m dn !defined;
+ f m dn acc )
+
+ let fold_pattern_up f acc dpat cpat dn (up,plug) =
+ fold_pattern_nonlin
+ ( fun m dn acc ->
+ f dn (subst_evar plug (e_subst_evar neutral_meta new_evar cpat) up, m) acc
+ ) acc dpat dn
+
+ let possibly_under pat k dn (up,plug) =
+ let rec aux fst dn (up,plug) acc =
+ let cpat = pat() in
+ let dpat = pat_of_constr cpat in
+ let dpat = if fst then empty_ctx dpat else dpat in
+ snd (fold_pattern_up (aux false) acc dpat cpat dn (up,plug)) @
+ (k dn (up,plug)) in
+ aux true dn (up,plug) []
+
+ let eq_pat eq () = mkApp(eq,[|mkEvar(neutral_meta,[||]);new_evar();new_evar()|])
+ let app_pat () = mkApp(new_evar(),[|mkEvar(neutral_meta,[||])|])
+
+ (*
+ * High-level primitives describing specific search problems
+ *)
+
+ let search_pattern dn pat =
+ let pat = Opt.reduce pat in
+ search_pat pat (empty_ctx (pat_of_constr pat)) dn init
+
+ let search_concl dn pat =
+ let pat = Opt.reduce pat in
+ search_pat pat (under_prod (empty_ctx (pat_of_constr pat))) dn init
+
+ let search_eq_concl dn eq pat =
+ let pat = Opt.reduce pat in
+ let eq_pat = eq_pat eq () in
+ let eq_dpat = under_prod (empty_ctx (pat_of_constr eq_pat)) in
+ snd (fold_pattern_up
+ (fun dn up acc ->
+ search_pat pat (pat_of_constr pat) dn up @ acc
+ ) [] eq_dpat eq_pat dn init)
+
+ let search_head_concl dn pat =
+ let pat = Opt.reduce pat in
+ possibly_under app_pat (search_pat pat (pat_of_constr pat)) dn init
+
+ let find_all dn = Idset.elements (TDnet.find_all dn)
+end
+
+module type S =
+sig
+ type t
+ type ident
+
+ type result = ident * (constr*existential_key) * Termops.subst
+
+ val empty : t
+ val add : constr -> ident -> t -> t
+ val union : t -> t -> t
+ val subst : substitution -> t -> t
+ val search_pattern : t -> constr -> result list
+ val search_concl : t -> constr -> result list
+ val search_head_concl : t -> constr -> result list
+ val search_eq_concl : t -> constr -> constr -> result list
+ val find_all : t -> ident list
+end
diff --git a/pretyping/term_dnet.mli b/pretyping/term_dnet.mli
new file mode 100644
index 0000000000..ccf9624814
--- /dev/null
+++ b/pretyping/term_dnet.mli
@@ -0,0 +1,110 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(* $Id:$ *)
+
+(*i*)
+open Term
+open Sign
+open Libnames
+open Mod_subst
+(*i*)
+
+(* Dnets on constr terms.
+
+ An instantiation of Dnet on (an approximation of) constr. It
+ associates a term (possibly with Evar) with an
+ identifier. Identifiers must be unique (no two terms sharing the
+ same ident), and there must be a way to recover the full term from
+ the identifier (function constr_of).
+
+ Optionally, a pre-treatment on terms can be performed before adding
+ or searching (reduce). Practically, it is used to do some kind of
+ delta-reduction on terms before indexing them.
+
+ The results returned here are perfect, since post-filtering is done
+ inside here.
+
+ See lib/dnet.mli for more details.
+*)
+
+(* Identifiers to store (right hand side of the association) *)
+module type IDENT = sig
+ type t
+ val compare : t -> t -> int
+
+ (* how to substitute them for storage *)
+ val subst : substitution -> t -> t
+
+ (* how to recover the term from the identifier *)
+ val constr_of : t -> constr
+end
+
+(* Options : *)
+module type OPT = sig
+
+ (* pre-treatment to terms before adding or searching *)
+ val reduce : constr -> constr
+
+ (* direction of post-filtering w.r.t sort subtyping :
+ - true means query <= terms in the structure
+ - false means terms <= query
+ *)
+ val direction : bool
+end
+
+module type S =
+sig
+ type t
+ type ident
+
+ (* results of filtering : identifier, a context (term with Evar
+ hole) and the substitution in that context*)
+ type result = ident * (constr*existential_key) * Termops.subst
+
+ val empty : t
+
+ (* [add c i dn] adds the binding [(c,i)] to [dn]. [c] can be a
+ closed term or a pattern (with untyped Evars). No Metas accepted *)
+ val add : constr -> ident -> t -> t
+
+ (* merge of dnets. Faster than re-adding all terms *)
+ val union : t -> t -> t
+
+ val subst : substitution -> t -> t
+
+ (*
+ * High-level primitives describing specific search problems
+ *)
+
+ (* [search_pattern dn c] returns all terms/patterns in dn
+ matching/matched by c *)
+ val search_pattern : t -> constr -> result list
+
+ (* [search_concl dn c] returns all matches under products and
+ letins, i.e. it finds subterms whose conclusion matches c. The
+ complexity depends only on c ! *)
+ val search_concl : t -> constr -> result list
+
+ (* [search_head_concl dn c] matches under products and applications
+ heads. Finds terms of the form [forall H_1...H_n, C t_1...t_n]
+ where C matches c *)
+ val search_head_concl : t -> constr -> result list
+
+ (* [search_eq_concl dn eq c] searches terms of the form [forall
+ H1...Hn, eq _ X1 X2] where either X1 or X2 matches c *)
+ val search_eq_concl : t -> constr -> constr -> result list
+
+ (* [find_all dn] returns all idents contained in dn *)
+ val find_all : t -> ident list
+end
+
+module Make :
+ functor (Ident : IDENT) ->
+ functor (Opt : OPT) ->
+ S with type ident = Ident.t
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 987db88b18..e3b8a166c7 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -951,16 +951,77 @@ let base_sort_cmp pb s0 s1 =
| _ -> false
(* eq_constr extended with universe erasure *)
-let rec constr_cmp cv_pb t1 t2 =
+let compare_constr_univ f cv_pb t1 t2 =
match kind_of_term t1, kind_of_term t2 with
Sort s1, Sort s2 -> base_sort_cmp cv_pb s1 s2
| Prod (_,t1,c1), Prod (_,t2,c2) ->
- constr_cmp Reduction.CONV t1 t2 &
- constr_cmp cv_pb c1 c2
- | _ -> compare_constr (constr_cmp Reduction.CONV) t1 t2
+ f Reduction.CONV t1 t2 & f cv_pb c1 c2
+ | _ -> compare_constr (f Reduction.CONV) t1 t2
+
+let rec constr_cmp cv_pb t1 t2 = compare_constr_univ constr_cmp cv_pb t1 t2
let eq_constr = constr_cmp Reduction.CONV
+(* App(c,[t1,...tn]) -> ([c,t1,...,tn-1],tn)
+ App(c,[||]) -> ([],c) *)
+let split_app c = match kind_of_term c with
+ App(c,l) ->
+ let len = Array.length l in
+ if len=0 then ([],c) else
+ let last = Array.get l (len-1) in
+ let prev = Array.sub l 0 (len-1) in
+ c::(Array.to_list prev), last
+ | _ -> assert false
+
+let hdtl l = List.hd l, List.tl l
+
+type subst = (rel_context*constr) Intmap.t
+
+exception CannotFilter
+
+let filtering env cv_pb c1 c2 =
+ let evm = ref Intmap.empty in
+ let define cv_pb e1 ev c1 =
+ try let (e2,c2) = Intmap.find ev !evm in
+ let shift = List.length e1 - List.length e2 in
+ if constr_cmp cv_pb c1 (lift shift c2) then () else raise CannotFilter
+ with Not_found ->
+ evm := Intmap.add ev (e1,c1) !evm
+ in
+ let rec aux env cv_pb c1 c2 =
+ match kind_of_term c1, kind_of_term c2 with
+ | App _, App _ ->
+ let ((p1,l1),(p2,l2)) = (split_app c1),(split_app c2) in
+ aux env cv_pb l1 l2; if p1=[] & p2=[] then () else
+ aux env cv_pb (applist (hdtl p1)) (applist (hdtl p2))
+ | Prod (n,t1,c1), Prod (_,t2,c2) ->
+ aux env cv_pb t1 t2;
+ aux ((n,None,t1)::env) cv_pb c1 c2
+ | _, Evar (ev,_) -> define cv_pb env ev c1
+ | Evar (ev,_), _ -> define cv_pb env ev c2
+ | _ ->
+ if compare_constr_univ
+ (fun pb c1 c2 -> aux env pb c1 c2; true) cv_pb c1 c2 then ()
+ else raise CannotFilter
+ (* TODO: le reste des binders *)
+ in
+ aux env cv_pb c1 c2; !evm
+
+let decompose_prod_letin : constr -> int * rel_context * constr =
+ let rec prodec_rec i l c = match kind_of_term c with
+ | Prod (n,t,c) -> prodec_rec (succ i) ((n,None,t)::l) c
+ | LetIn (n,d,t,c) -> prodec_rec (succ i) ((n,Some d,t)::l) c
+ | Cast (c,_,_) -> prodec_rec i l c
+ | _ -> i,l,c in
+ prodec_rec 0 []
+
+let align_prod_letin c a : rel_context * constr =
+ let (lc,_,_) = decompose_prod_letin c in
+ let (la,l,a) = decompose_prod_letin a in
+ if not (la >= lc) then invalid_arg "align_prod_letin";
+ let (l1,l2) = Util.list_chop lc l in
+ l2,it_mkProd_or_LetIn a l1
+
(* On reduit une serie d'eta-redex de tete ou rien du tout *)
(* [x1:c1;...;xn:cn]@(f;a1...an;x1;...;xn) --> @(f;a1...an) *)
(* Remplace 2 versions précédentes buggées *)
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 9163a1d9e5..79fe908d7a 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -170,12 +170,28 @@ val error_invalid_occurrence : int list -> 'a
(* Alternative term equalities *)
val base_sort_cmp : Reduction.conv_pb -> sorts -> sorts -> bool
+val compare_constr_univ : (Reduction.conv_pb -> constr -> constr -> bool) ->
+ Reduction.conv_pb -> constr -> constr -> bool
val constr_cmp : Reduction.conv_pb -> constr -> constr -> bool
val eq_constr : constr -> constr -> bool
val eta_reduce_head : constr -> constr
val eta_eq_constr : constr -> constr -> bool
+exception CannotFilter
+
+(* Lightweight first-order filtering procedure. Unification
+ variables ar represented by (untyped) Evars.
+ [filtering c1 c2] returns the substitution n'th evar ->
+ (context,term), or raises [CannotFilter].
+ Warning: Outer-kernel sort subtyping are taken into account: c1 has
+ to be smaller than c2 wrt. sorts. *)
+type subst = (rel_context*constr) Intmap.t
+val filtering : rel_context -> Reduction.conv_pb -> constr -> constr -> subst
+
+val decompose_prod_letin : constr -> int * rel_context * constr
+val align_prod_letin : constr -> constr -> rel_context * constr
+
(* finding "intuitive" names to hypotheses *)
val lowercase_first_char : identifier -> string
val sort_hdchar : sorts -> string
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-09 08:48:20 +0000