From 0db1d850b940a5f2351c1ec6e26d1f8087064d40 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 8 May 2014 16:40:48 +0200 Subject: Moving Dnet-related code to tactics/. --- dev/printers.mllib | 2 - lib/dnet.ml | 291 ---------------------------------- lib/dnet.mli | 124 --------------- lib/lib.mllib | 1 - pretyping/pretyping.mllib | 1 - pretyping/term_dnet.ml | 388 ---------------------------------------------- pretyping/term_dnet.mli | 88 ----------- tactics/dnet.ml | 291 ++++++++++++++++++++++++++++++++++ tactics/dnet.mli | 124 +++++++++++++++ tactics/tactics.mllib | 2 + tactics/term_dnet.ml | 388 ++++++++++++++++++++++++++++++++++++++++++++++ tactics/term_dnet.mli | 88 +++++++++++ 12 files changed, 893 insertions(+), 895 deletions(-) delete mode 100644 lib/dnet.ml delete mode 100644 lib/dnet.mli delete mode 100644 pretyping/term_dnet.ml delete mode 100644 pretyping/term_dnet.mli create mode 100644 tactics/dnet.ml create mode 100644 tactics/dnet.mli create mode 100644 tactics/term_dnet.ml create mode 100644 tactics/term_dnet.mli diff --git a/dev/printers.mllib b/dev/printers.mllib index fb8d4c73e0..5a9acb6dd4 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -39,7 +39,6 @@ Explore Predicate Rtree Heap -Dnet Genarg Stateid Ephemeron @@ -121,7 +120,6 @@ Cbv Pretype_errors Evarutil Evarsolve -Term_dnet Recordops Evarconv Arguments_renaming diff --git a/lib/dnet.ml b/lib/dnet.ml deleted file mode 100644 index 22ca7e78d1..0000000000 --- a/lib/dnet.ml +++ /dev/null @@ -1,291 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 'b) -> 'a t -> 'b t - val map2 : ('a -> 'b -> 'c) -> 'a t -> 'b t -> 'c t - val fold : ('a -> 'b -> 'a) -> 'a -> 'b t -> 'a - val fold2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b t -> 'c t -> 'a - val compare : unit t -> unit t -> int - val terminal : 'a t -> bool - val choose : ('a -> 'b) -> 'a t -> 'b -end - -module type S = -sig - type t - type ident - type meta - type 'a structure - module Idset : Set.S with type elt=ident - type term_pattern = - | Term of term_pattern structure - | Meta of meta - val empty : t - val add : t -> term_pattern -> ident -> t - val find_all : t -> Idset.t - val fold_pattern : - ('a -> (Idset.t * meta * t) -> 'a) -> 'a -> term_pattern -> t -> Idset.t option * 'a - val find_match : term_pattern -> t -> Idset.t - val inter : t -> t -> t - val union : t -> t -> t - val map : (ident -> ident) -> (unit structure -> unit structure) -> t -> t -end - -module Make = - functor (T:Datatype) -> - functor (Ident:Set.OrderedType) -> - functor (Meta:Set.OrderedType) -> -struct - - type ident = Ident.t - type meta = Meta.t - - type 'a structure = 'a T.t - - type term_pattern = - | Term of term_pattern structure - | Meta of meta - - module Idset = Set.Make(Ident) - module Mmap = Map.Make(Meta) - module Tmap = Map.Make(struct type t = unit structure - let compare = T.compare end) - - type idset = Idset.t - - - - (* we store identifiers at the leaf of the dnet *) - type node = - | Node of t structure - | Terminal of t structure * idset - - (* at each node, we have a bunch of nodes (actually a map between - the bare node and a subnet) and a bunch of metavariables *) - and t = Nodes of node Tmap.t * idset Mmap.t - - let empty : t = Nodes (Tmap.empty, Mmap.empty) - - (* the head of a data is of type unit structure *) - let head w = T.map (fun c -> ()) w - - (* given a node of the net and a word, returns the subnet with the - same head as the word (with the rest of the nodes) *) - let split l (w:'a structure) : node * node Tmap.t = - let elt : node = Tmap.find (head w) l in - (elt, Tmap.remove (head w) l) - - let select l w = Tmap.find (head w) l - - let rec add (Nodes (t,m):t) (w:term_pattern) (id:ident) : t = - match w with Term w -> - ( try - let (n,tl) = split t w in - let new_node = match n with - | Terminal (e,is) -> Terminal (e,Idset.add id is) - | Node e -> Node (T.map2 (fun t p -> add t p id) e w) in - Nodes ((Tmap.add (head w) new_node tl), m) - with Not_found -> - let new_content = T.map (fun p -> add empty p id) w in - let new_node = - if T.terminal w then - Terminal (new_content, Idset.singleton id) - else Node new_content in - Nodes ((Tmap.add (head w) new_node t), m) ) - | Meta i -> - let m = - try Mmap.add i (Idset.add id (Mmap.find i m)) m - with Not_found -> Mmap.add i (Idset.singleton id) m in - Nodes (t, m) - - let add t w id = add t w id - - let rec find_all (Nodes (t,m)) : idset = - Idset.union - (Mmap.fold (fun _ -> Idset.union) m Idset.empty) - (Tmap.fold - ( fun _ n acc -> - let s2 = match n with - | Terminal (_,is) -> is - | Node e -> T.choose find_all e in - Idset.union acc s2 - ) t Idset.empty) - -(* (\* optimization hack: Not_found is catched in fold_pattern *\) *) -(* let fast_inter s1 s2 = *) -(* if Idset.is_empty s1 || Idset.is_empty s2 then raise Not_found *) -(* else Idset.inter s1 s2 *) - -(* let option_any2 f s1 s2 = match s1,s2 with *) -(* | Some s1, Some s2 -> f s1 s2 *) -(* | (Some s, _ | _, Some s) -> s *) -(* | _ -> raise Not_found *) - -(* let fold_pattern ?(complete=true) f acc pat dn = *) -(* let deferred = ref [] in *) -(* let leafs,metas = ref None, ref None in *) -(* let leaf s = leafs := match !leafs with *) -(* | None -> Some s *) -(* | Some s' -> Some (fast_inter s s') in *) -(* let meta s = metas := match !metas with *) -(* | None -> Some s *) -(* | Some s' -> Some (Idset.union s s') in *) -(* let defer c = deferred := c::!deferred in *) -(* let rec fp_rec (p:term_pattern) (Nodes(t,m) as dn:t) = *) -(* Mmap.iter (fun _ -> meta) m; (\* TODO: gérer patterns nonlin ici *\) *) -(* match p with *) -(* | Meta m -> defer (m,dn) *) -(* | Term w -> *) -(* try match select t w with *) -(* | Terminal (_,is) -> leaf is *) -(* | Node e -> *) -(* if complete then T.fold2 (fun _ -> fp_rec) () w e else *) -(* if T.fold2 *) -(* (fun b p dn -> match p with *) -(* | Term _ -> fp_rec p dn; false *) -(* | Meta _ -> b *) -(* ) true w e *) -(* then T.choose (T.choose fp_rec w) e *) -(* with Not_found -> *) -(* if Mmap.is_empty m then raise Not_found else () *) -(* in try *) -(* fp_rec pat dn; *) -(* (try Some (option_any2 Idset.union !leafs !metas) with Not_found -> None), *) -(* List.fold_left (fun acc (m,dn) -> f m dn acc) acc !deferred *) -(* with Not_found -> None,acc *) - - (* Sets with a neutral element for inter *) - module OSet (S:Set.S) = struct - type t = S.t option - let union s1 s2 : t = match s1,s2 with - | (None, _ | _, None) -> None - | Some a, Some b -> Some (S.union a b) - let inter s1 s2 : t = match s1,s2 with - | (None, a | a, None) -> a - | Some a, Some b -> Some (S.inter a b) - let is_empty : t -> bool = function - | None -> false - | Some s -> S.is_empty s - (* optimization hack: Not_found is catched in fold_pattern *) - let fast_inter s1 s2 = - if is_empty s1 || is_empty s2 then raise Not_found - else let r = inter s1 s2 in - if is_empty r then raise Not_found else r - let full = None - let empty = Some S.empty - end - - module OIdset = OSet(Idset) - - let fold_pattern ?(complete=true) f acc pat dn = - let deferred = ref [] in - let defer c = deferred := c::!deferred in - - let rec fp_rec metas p (Nodes(t,m) as dn:t) = - (* TODO gérer les dnets non-linéaires *) - let metas = Mmap.fold (fun _ -> Idset.union) m metas in - match p with - | Meta m -> defer (metas,m,dn); OIdset.full - | Term w -> - let curm = Mmap.fold (fun _ -> Idset.union) m Idset.empty in - try match select t w with - | Terminal (_,is) -> Some (Idset.union curm is) - | Node e -> - let ids = if complete then T.fold2 - (fun acc w e -> - OIdset.fast_inter acc (fp_rec metas w e) - ) OIdset.full w e - else - let (all_metas, res) = T.fold2 - (fun (b,acc) w e -> match w with - | Term _ -> false, OIdset.fast_inter acc (fp_rec metas w e) - | Meta _ -> b, acc - ) (true,OIdset.full) w e in - if all_metas then T.choose (T.choose (fp_rec metas) w) e - else res in - OIdset.union ids (Some curm) - with Not_found -> - if Idset.is_empty metas then raise Not_found else Some curm in - let cand = - try fp_rec Idset.empty pat dn - with Not_found -> OIdset.empty in - let res = List.fold_left f acc !deferred in - cand, res - - (* intersection of two dnets. keep only the common pairs *) - let rec inter (t1:t) (t2:t) : t = - let inter_map f (Nodes (t1,m1):t) (Nodes (t2,m2):t) : t = - Nodes - (Tmap.fold - ( fun k e acc -> - try Tmap.add k (f e (Tmap.find k t2)) acc - with Not_found -> acc - ) t1 Tmap.empty, - Mmap.fold - ( fun m s acc -> - try Mmap.add m (Idset.inter s (Mmap.find m m2)) acc - with Not_found -> acc - ) m1 Mmap.empty - ) in - inter_map - (fun n1 n2 -> match n1,n2 with - | Terminal (e1,s1), Terminal (_,s2) -> Terminal (e1,Idset.inter s1 s2) - | Node e1, Node e2 -> Node (T.map2 inter e1 e2) - | _ -> assert false - ) t1 t2 - - let rec union (t1:t) (t2:t) : t = - let union_map f (Nodes (t1,m1):t) (Nodes (t2,m2):t) : t = - Nodes - (Tmap.fold - ( fun k e acc -> - try Tmap.add k (f e (Tmap.find k acc)) acc - with Not_found -> Tmap.add k e acc - ) t1 t2, - Mmap.fold - ( fun m s acc -> - try Mmap.add m (Idset.inter s (Mmap.find m acc)) acc - with Not_found -> Mmap.add m s acc - ) m1 m2 - ) in - union_map - (fun n1 n2 -> match n1,n2 with - | Terminal (e1,s1), Terminal (_,s2) -> Terminal (e1,Idset.union s1 s2) - | Node e1, Node e2 -> Node (T.map2 union e1 e2) - | _ -> assert false - ) t1 t2 - - let find_match (p:term_pattern) (t:t) : idset = - let metas = ref Mmap.empty in - let (mset,lset) = fold_pattern ~complete:false - (fun acc (mset,m,t) -> - let all = OIdset.fast_inter acc - (Some(let t = try inter t (Mmap.find m !metas) with Not_found -> t in - metas := Mmap.add m t !metas; - find_all t)) in - OIdset.union (Some mset) all - ) None p t in - Option.get (OIdset.inter mset lset) - - let fold_pattern f acc p dn = fold_pattern ~complete:true f acc p dn - - let idset_map f is = Idset.fold (fun e acc -> Idset.add (f e) acc) is Idset.empty - let tmap_map f g m = Tmap.fold (fun k e acc -> Tmap.add (f k) (g e) acc) m Tmap.empty - - let rec map sidset sterm (Nodes (t,m)) : t = - let snode = function - | Terminal (e,is) -> Terminal (e,idset_map sidset is) - | Node e -> Node (T.map (map sidset sterm) e) in - Nodes (tmap_map sterm snode t, Mmap.map (idset_map sidset) m) - -end diff --git a/lib/dnet.mli b/lib/dnet.mli deleted file mode 100644 index d2373a0d68..0000000000 --- a/lib/dnet.mli +++ /dev/null @@ -1,124 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* | Leaf - | Node of btree * btree | Node of 'a * 'a - -*) - -(** datatype you want to build a dnet on *) -module type Datatype = -sig - (** parametric datatype. ['a] is morally the recursive argument *) - type 'a t - - (** non-recursive mapping of subterms *) - val map : ('a -> 'b) -> 'a t -> 'b t - val map2 : ('a -> 'b -> 'c) -> 'a t -> 'b t -> 'c t - - (** non-recursive folding of subterms *) - val fold : ('a -> 'b -> 'a) -> 'a -> 'b t -> 'a - val fold2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b t -> 'c t -> 'a - - (** comparison of constructors *) - val compare : unit t -> unit t -> int - - (** for each constructor, is it not-parametric on 'a? *) - val terminal : 'a t -> bool - - (** [choose f w] applies f on ONE of the subterms of w *) - val choose : ('a -> 'b) -> 'a t -> 'b -end - -module type S = -sig - type t - - (** provided identifier type *) - type ident - - (** provided metavariable type *) - type meta - - (** provided parametrized datastructure *) - type 'a structure - - (** returned sets of solutions *) - module Idset : Set.S with type elt=ident - - (** a pattern is a term where each node can be a unification - variable *) - type term_pattern = - | Term of term_pattern structure - | Meta of meta - - val empty : t - - (** [add t w i] adds a new association (w,i) in t. *) - val add : t -> term_pattern -> ident -> t - - (** [find_all t] returns all identifiers contained in t. *) - val find_all : t -> Idset.t - - (** [fold_pattern f acc p dn] folds f on each meta of p, passing the - meta and the sub-dnet under it. The result includes: - - Some set if identifiers were gathered on the leafs of the term - - None if the pattern contains no leaf (only Metas at the leafs). - *) - val fold_pattern : - ('a -> (Idset.t * meta * t) -> 'a) -> 'a -> term_pattern -> t -> Idset.t option * 'a - - (** [find_match p t] returns identifiers of all terms matching p in - t. *) - val find_match : term_pattern -> t -> Idset.t - - (** set operations on dnets *) - val inter : t -> t -> t - val union : t -> t -> t - - (** apply a function on each identifier and node of terms in a dnet *) - val map : (ident -> ident) -> (unit structure -> unit structure) -> t -> t -end - -module Make : - functor (T:Datatype) -> - functor (Ident:Set.OrderedType) -> - functor (Meta:Set.OrderedType) -> - S with type ident = Ident.t - and type meta = Meta.t - and type 'a structure = 'a T.t diff --git a/lib/lib.mllib b/lib/lib.mllib index edef3da037..b5421a8c89 100644 --- a/lib/lib.mllib +++ b/lib/lib.mllib @@ -16,7 +16,6 @@ Explore Predicate Rtree Heap -Dnet Unionfind Genarg Ephemeron diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index 469be6d9ea..a4c72f4828 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -11,7 +11,6 @@ Cbv Pretype_errors Evarutil Evarsolve -Term_dnet Recordops Evarconv Arguments_renaming diff --git a/pretyping/term_dnet.ml b/pretyping/term_dnet.ml deleted file mode 100644 index e05f4bcfe8..0000000000 --- a/pretyping/term_dnet.ml +++ /dev/null @@ -1,388 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 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_ci ci1 ci2 = - let c = ind_ord ci1.ci_ind ci2.ci_ind in - if c = 0 then - let c = Int.compare ci1.ci_npar ci2.ci_npar in - if c = 0 then - let c = Array.compare Int.compare ci1.ci_cstr_ndecls ci2.ci_cstr_ndecls in - if c = 0 then - Array.compare Int.compare ci1.ci_cstr_nargs ci2.ci_cstr_nargs - else c - else c - else c - - let compare cmp t1 t2 = match t1, t2 with - | DRel, DRel -> 0 - | DSort, DSort -> 0 - | DRef gr1, DRef gr2 -> RefOrdered.compare gr1 gr2 - | DCtx (tl1, tr1), DCtx (tl2, tr2) - | DLambda (tl1, tr1), DCtx (tl2, tr2) - | DApp (tl1, tr1), DCtx (tl2, tr2) -> - let c = cmp tl1 tl2 in - if c = 0 then cmp tr1 tr2 else c - - | DCase (ci1, c1, t1, p1), DCase (ci2, c2, t2, p2) -> - let c = cmp c1 c2 in - if c = 0 then - let c = cmp t1 t2 in - if c = 0 then - let c = Array.compare cmp p1 p2 in - if c = 0 then compare_ci ci1 ci2 - else c - else c - else c - - | DFix (i1, j1, tl1, pl1), DFix (i2, j2, tl2, pl2) -> - let c = Int.compare j1 j2 in - if c = 0 then - let c = Array.compare Int.compare i1 i2 in - if c = 0 then - let c = Array.compare cmp tl1 tl2 in - if c = 0 then Array.compare cmp pl1 pl2 - else c - else c - else c - | DCoFix (i1, tl1, pl1), DCoFix (i2, tl2, pl2) -> - let c = Int.compare i1 i2 in - if c = 0 then - let c = Array.compare cmp tl1 tl2 in - if c = 0 then Array.compare cmp pl1 pl2 - else c - else c - | _ -> Pervasives.compare t1 t2 (** OK **) - - 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 dummy_cmp () () = 0 - - let fold2 (f:'a -> 'b -> 'c -> 'a) (acc:'a) (c1:'b t) (c2:'c t) : 'a = - let head w = map (fun _ -> ()) w in - if not (Int.equal (compare dummy_cmp (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 not (Int.equal (compare dummy_cmp (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 - - let compare t1 t2 = compare dummy_cmp t1 t2 - -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 = int - = Dnet.Make(DTerm)(Ident)(Int) - - type t = TDnet.t - - type ident = TDnet.ident - - (** We will freshen metas on the fly, to cope with the implementation defect - of Term_dnet which requires metas to be all distinct. *) - let fresh_meta = - let index = ref 0 in - fun () -> - let ans = !index in - let () = index := succ ans in - ans - - open DTerm - open TDnet - - let pat_of_constr c : term_pattern = - (** To each evar we associate a unique identifier. *) - let metas = ref Evar.Map.empty in - let rec pat_of_constr c = match kind_of_term c with - | Rel _ -> Term DRel - | Sort _ -> Term DSort - | Var i -> Term (DRef (VarRef i)) - | Const (c,u) -> Term (DRef (ConstRef c)) - | Ind (i,u) -> Term (DRef (IndRef i)) - | Construct (c,u)-> Term (DRef (ConstructRef c)) - | Term.Meta _ -> assert false - | Evar (i,_) -> - let meta = - try Evar.Map.find i !metas - with Not_found -> - let meta = fresh_meta () in - let () = metas := Evar.Map.add i meta !metas in - meta - in - Meta meta - | 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) - | Proj (p,c) -> - Term (DApp (Term (DRef (ConstRef p)), pat_of_constr c)) - - and ctx_of_constr ctx c = 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 - in - 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 () = Meta (fresh_meta ()) - - let rec remove_cap : term_pattern -> term_pattern = function - | Term (DCons (t,u)) -> Term (DCons (t,remove_cap u)) - | Term DNil -> new_meta() - | Meta _ as m -> m - | _ -> 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 - - (* debug *) - let rec pr_term_pattern p = - (fun pr_t -> function - | Term t -> pr_t t - | Meta m -> str"["++Pp.int (Obj.magic m)++str"]" - ) (pr_dconstr pr_term_pattern) p - - let search_pat cpat dpat dn = - let whole_c = cpat in - (* if we are at the root, add an empty context *) - let dpat = under_prod (empty_ctx dpat) 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 wc,whole_c = if Opt.direction then whole_c,wc else wc,whole_c in - try - let _ = Termops.filtering ctx Reduction.CUMUL wc whole_c in - id :: acc - with Termops.CannotFilter -> (* msgnl(str"recon "++Termops.print_constr_env (Global.env()) wc); *) acc - ) (TDnet.find_match dpat dn) [] - - (* - * 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 - - let find_all dn = Idset.elements (TDnet.find_all dn) - - let map f dn = TDnet.map f (fun x -> x) dn -end - -module type S = -sig - type t - type ident - - val empty : t - val add : constr -> ident -> t -> t - val union : t -> t -> t - val subst : substitution -> t -> t - val search_pattern : t -> constr -> ident list - val find_all : t -> ident list - val map : (ident -> ident) -> t -> t -end diff --git a/pretyping/term_dnet.mli b/pretyping/term_dnet.mli deleted file mode 100644 index 7825ebdf1a..0000000000 --- a/pretyping/term_dnet.mli +++ /dev/null @@ -1,88 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 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 - - 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 -> ident list - - (** [find_all dn] returns all idents contained in dn *) - val find_all : t -> ident list - - val map : (ident -> ident) -> t -> t -end - -module Make : - functor (Ident : IDENT) -> - functor (Opt : OPT) -> - S with type ident = Ident.t diff --git a/tactics/dnet.ml b/tactics/dnet.ml new file mode 100644 index 0000000000..22ca7e78d1 --- /dev/null +++ b/tactics/dnet.ml @@ -0,0 +1,291 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 'b) -> 'a t -> 'b t + val map2 : ('a -> 'b -> 'c) -> 'a t -> 'b t -> 'c t + val fold : ('a -> 'b -> 'a) -> 'a -> 'b t -> 'a + val fold2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b t -> 'c t -> 'a + val compare : unit t -> unit t -> int + val terminal : 'a t -> bool + val choose : ('a -> 'b) -> 'a t -> 'b +end + +module type S = +sig + type t + type ident + type meta + type 'a structure + module Idset : Set.S with type elt=ident + type term_pattern = + | Term of term_pattern structure + | Meta of meta + val empty : t + val add : t -> term_pattern -> ident -> t + val find_all : t -> Idset.t + val fold_pattern : + ('a -> (Idset.t * meta * t) -> 'a) -> 'a -> term_pattern -> t -> Idset.t option * 'a + val find_match : term_pattern -> t -> Idset.t + val inter : t -> t -> t + val union : t -> t -> t + val map : (ident -> ident) -> (unit structure -> unit structure) -> t -> t +end + +module Make = + functor (T:Datatype) -> + functor (Ident:Set.OrderedType) -> + functor (Meta:Set.OrderedType) -> +struct + + type ident = Ident.t + type meta = Meta.t + + type 'a structure = 'a T.t + + type term_pattern = + | Term of term_pattern structure + | Meta of meta + + module Idset = Set.Make(Ident) + module Mmap = Map.Make(Meta) + module Tmap = Map.Make(struct type t = unit structure + let compare = T.compare end) + + type idset = Idset.t + + + + (* we store identifiers at the leaf of the dnet *) + type node = + | Node of t structure + | Terminal of t structure * idset + + (* at each node, we have a bunch of nodes (actually a map between + the bare node and a subnet) and a bunch of metavariables *) + and t = Nodes of node Tmap.t * idset Mmap.t + + let empty : t = Nodes (Tmap.empty, Mmap.empty) + + (* the head of a data is of type unit structure *) + let head w = T.map (fun c -> ()) w + + (* given a node of the net and a word, returns the subnet with the + same head as the word (with the rest of the nodes) *) + let split l (w:'a structure) : node * node Tmap.t = + let elt : node = Tmap.find (head w) l in + (elt, Tmap.remove (head w) l) + + let select l w = Tmap.find (head w) l + + let rec add (Nodes (t,m):t) (w:term_pattern) (id:ident) : t = + match w with Term w -> + ( try + let (n,tl) = split t w in + let new_node = match n with + | Terminal (e,is) -> Terminal (e,Idset.add id is) + | Node e -> Node (T.map2 (fun t p -> add t p id) e w) in + Nodes ((Tmap.add (head w) new_node tl), m) + with Not_found -> + let new_content = T.map (fun p -> add empty p id) w in + let new_node = + if T.terminal w then + Terminal (new_content, Idset.singleton id) + else Node new_content in + Nodes ((Tmap.add (head w) new_node t), m) ) + | Meta i -> + let m = + try Mmap.add i (Idset.add id (Mmap.find i m)) m + with Not_found -> Mmap.add i (Idset.singleton id) m in + Nodes (t, m) + + let add t w id = add t w id + + let rec find_all (Nodes (t,m)) : idset = + Idset.union + (Mmap.fold (fun _ -> Idset.union) m Idset.empty) + (Tmap.fold + ( fun _ n acc -> + let s2 = match n with + | Terminal (_,is) -> is + | Node e -> T.choose find_all e in + Idset.union acc s2 + ) t Idset.empty) + +(* (\* optimization hack: Not_found is catched in fold_pattern *\) *) +(* let fast_inter s1 s2 = *) +(* if Idset.is_empty s1 || Idset.is_empty s2 then raise Not_found *) +(* else Idset.inter s1 s2 *) + +(* let option_any2 f s1 s2 = match s1,s2 with *) +(* | Some s1, Some s2 -> f s1 s2 *) +(* | (Some s, _ | _, Some s) -> s *) +(* | _ -> raise Not_found *) + +(* let fold_pattern ?(complete=true) f acc pat dn = *) +(* let deferred = ref [] in *) +(* let leafs,metas = ref None, ref None in *) +(* let leaf s = leafs := match !leafs with *) +(* | None -> Some s *) +(* | Some s' -> Some (fast_inter s s') in *) +(* let meta s = metas := match !metas with *) +(* | None -> Some s *) +(* | Some s' -> Some (Idset.union s s') in *) +(* let defer c = deferred := c::!deferred in *) +(* let rec fp_rec (p:term_pattern) (Nodes(t,m) as dn:t) = *) +(* Mmap.iter (fun _ -> meta) m; (\* TODO: gérer patterns nonlin ici *\) *) +(* match p with *) +(* | Meta m -> defer (m,dn) *) +(* | Term w -> *) +(* try match select t w with *) +(* | Terminal (_,is) -> leaf is *) +(* | Node e -> *) +(* if complete then T.fold2 (fun _ -> fp_rec) () w e else *) +(* if T.fold2 *) +(* (fun b p dn -> match p with *) +(* | Term _ -> fp_rec p dn; false *) +(* | Meta _ -> b *) +(* ) true w e *) +(* then T.choose (T.choose fp_rec w) e *) +(* with Not_found -> *) +(* if Mmap.is_empty m then raise Not_found else () *) +(* in try *) +(* fp_rec pat dn; *) +(* (try Some (option_any2 Idset.union !leafs !metas) with Not_found -> None), *) +(* List.fold_left (fun acc (m,dn) -> f m dn acc) acc !deferred *) +(* with Not_found -> None,acc *) + + (* Sets with a neutral element for inter *) + module OSet (S:Set.S) = struct + type t = S.t option + let union s1 s2 : t = match s1,s2 with + | (None, _ | _, None) -> None + | Some a, Some b -> Some (S.union a b) + let inter s1 s2 : t = match s1,s2 with + | (None, a | a, None) -> a + | Some a, Some b -> Some (S.inter a b) + let is_empty : t -> bool = function + | None -> false + | Some s -> S.is_empty s + (* optimization hack: Not_found is catched in fold_pattern *) + let fast_inter s1 s2 = + if is_empty s1 || is_empty s2 then raise Not_found + else let r = inter s1 s2 in + if is_empty r then raise Not_found else r + let full = None + let empty = Some S.empty + end + + module OIdset = OSet(Idset) + + let fold_pattern ?(complete=true) f acc pat dn = + let deferred = ref [] in + let defer c = deferred := c::!deferred in + + let rec fp_rec metas p (Nodes(t,m) as dn:t) = + (* TODO gérer les dnets non-linéaires *) + let metas = Mmap.fold (fun _ -> Idset.union) m metas in + match p with + | Meta m -> defer (metas,m,dn); OIdset.full + | Term w -> + let curm = Mmap.fold (fun _ -> Idset.union) m Idset.empty in + try match select t w with + | Terminal (_,is) -> Some (Idset.union curm is) + | Node e -> + let ids = if complete then T.fold2 + (fun acc w e -> + OIdset.fast_inter acc (fp_rec metas w e) + ) OIdset.full w e + else + let (all_metas, res) = T.fold2 + (fun (b,acc) w e -> match w with + | Term _ -> false, OIdset.fast_inter acc (fp_rec metas w e) + | Meta _ -> b, acc + ) (true,OIdset.full) w e in + if all_metas then T.choose (T.choose (fp_rec metas) w) e + else res in + OIdset.union ids (Some curm) + with Not_found -> + if Idset.is_empty metas then raise Not_found else Some curm in + let cand = + try fp_rec Idset.empty pat dn + with Not_found -> OIdset.empty in + let res = List.fold_left f acc !deferred in + cand, res + + (* intersection of two dnets. keep only the common pairs *) + let rec inter (t1:t) (t2:t) : t = + let inter_map f (Nodes (t1,m1):t) (Nodes (t2,m2):t) : t = + Nodes + (Tmap.fold + ( fun k e acc -> + try Tmap.add k (f e (Tmap.find k t2)) acc + with Not_found -> acc + ) t1 Tmap.empty, + Mmap.fold + ( fun m s acc -> + try Mmap.add m (Idset.inter s (Mmap.find m m2)) acc + with Not_found -> acc + ) m1 Mmap.empty + ) in + inter_map + (fun n1 n2 -> match n1,n2 with + | Terminal (e1,s1), Terminal (_,s2) -> Terminal (e1,Idset.inter s1 s2) + | Node e1, Node e2 -> Node (T.map2 inter e1 e2) + | _ -> assert false + ) t1 t2 + + let rec union (t1:t) (t2:t) : t = + let union_map f (Nodes (t1,m1):t) (Nodes (t2,m2):t) : t = + Nodes + (Tmap.fold + ( fun k e acc -> + try Tmap.add k (f e (Tmap.find k acc)) acc + with Not_found -> Tmap.add k e acc + ) t1 t2, + Mmap.fold + ( fun m s acc -> + try Mmap.add m (Idset.inter s (Mmap.find m acc)) acc + with Not_found -> Mmap.add m s acc + ) m1 m2 + ) in + union_map + (fun n1 n2 -> match n1,n2 with + | Terminal (e1,s1), Terminal (_,s2) -> Terminal (e1,Idset.union s1 s2) + | Node e1, Node e2 -> Node (T.map2 union e1 e2) + | _ -> assert false + ) t1 t2 + + let find_match (p:term_pattern) (t:t) : idset = + let metas = ref Mmap.empty in + let (mset,lset) = fold_pattern ~complete:false + (fun acc (mset,m,t) -> + let all = OIdset.fast_inter acc + (Some(let t = try inter t (Mmap.find m !metas) with Not_found -> t in + metas := Mmap.add m t !metas; + find_all t)) in + OIdset.union (Some mset) all + ) None p t in + Option.get (OIdset.inter mset lset) + + let fold_pattern f acc p dn = fold_pattern ~complete:true f acc p dn + + let idset_map f is = Idset.fold (fun e acc -> Idset.add (f e) acc) is Idset.empty + let tmap_map f g m = Tmap.fold (fun k e acc -> Tmap.add (f k) (g e) acc) m Tmap.empty + + let rec map sidset sterm (Nodes (t,m)) : t = + let snode = function + | Terminal (e,is) -> Terminal (e,idset_map sidset is) + | Node e -> Node (T.map (map sidset sterm) e) in + Nodes (tmap_map sterm snode t, Mmap.map (idset_map sidset) m) + +end diff --git a/tactics/dnet.mli b/tactics/dnet.mli new file mode 100644 index 0000000000..d2373a0d68 --- /dev/null +++ b/tactics/dnet.mli @@ -0,0 +1,124 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* | Leaf + | Node of btree * btree | Node of 'a * 'a + +*) + +(** datatype you want to build a dnet on *) +module type Datatype = +sig + (** parametric datatype. ['a] is morally the recursive argument *) + type 'a t + + (** non-recursive mapping of subterms *) + val map : ('a -> 'b) -> 'a t -> 'b t + val map2 : ('a -> 'b -> 'c) -> 'a t -> 'b t -> 'c t + + (** non-recursive folding of subterms *) + val fold : ('a -> 'b -> 'a) -> 'a -> 'b t -> 'a + val fold2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b t -> 'c t -> 'a + + (** comparison of constructors *) + val compare : unit t -> unit t -> int + + (** for each constructor, is it not-parametric on 'a? *) + val terminal : 'a t -> bool + + (** [choose f w] applies f on ONE of the subterms of w *) + val choose : ('a -> 'b) -> 'a t -> 'b +end + +module type S = +sig + type t + + (** provided identifier type *) + type ident + + (** provided metavariable type *) + type meta + + (** provided parametrized datastructure *) + type 'a structure + + (** returned sets of solutions *) + module Idset : Set.S with type elt=ident + + (** a pattern is a term where each node can be a unification + variable *) + type term_pattern = + | Term of term_pattern structure + | Meta of meta + + val empty : t + + (** [add t w i] adds a new association (w,i) in t. *) + val add : t -> term_pattern -> ident -> t + + (** [find_all t] returns all identifiers contained in t. *) + val find_all : t -> Idset.t + + (** [fold_pattern f acc p dn] folds f on each meta of p, passing the + meta and the sub-dnet under it. The result includes: + - Some set if identifiers were gathered on the leafs of the term + - None if the pattern contains no leaf (only Metas at the leafs). + *) + val fold_pattern : + ('a -> (Idset.t * meta * t) -> 'a) -> 'a -> term_pattern -> t -> Idset.t option * 'a + + (** [find_match p t] returns identifiers of all terms matching p in + t. *) + val find_match : term_pattern -> t -> Idset.t + + (** set operations on dnets *) + val inter : t -> t -> t + val union : t -> t -> t + + (** apply a function on each identifier and node of terms in a dnet *) + val map : (ident -> ident) -> (unit structure -> unit structure) -> t -> t +end + +module Make : + functor (T:Datatype) -> + functor (Ident:Set.OrderedType) -> + functor (Meta:Set.OrderedType) -> + S with type ident = Ident.t + and type meta = Meta.t + and type 'a structure = 'a T.t diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib index 27ded23573..4eb4318ee4 100644 --- a/tactics/tactics.mllib +++ b/tactics/tactics.mllib @@ -1,4 +1,5 @@ Geninterp +Dnet Dn Btermdn Tacticals @@ -20,5 +21,6 @@ Tacenv TacticMatching Tacinterp Evar_tactics +Term_dnet Autorewrite Tactic_option diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml new file mode 100644 index 0000000000..e05f4bcfe8 --- /dev/null +++ b/tactics/term_dnet.ml @@ -0,0 +1,388 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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_ci ci1 ci2 = + let c = ind_ord ci1.ci_ind ci2.ci_ind in + if c = 0 then + let c = Int.compare ci1.ci_npar ci2.ci_npar in + if c = 0 then + let c = Array.compare Int.compare ci1.ci_cstr_ndecls ci2.ci_cstr_ndecls in + if c = 0 then + Array.compare Int.compare ci1.ci_cstr_nargs ci2.ci_cstr_nargs + else c + else c + else c + + let compare cmp t1 t2 = match t1, t2 with + | DRel, DRel -> 0 + | DSort, DSort -> 0 + | DRef gr1, DRef gr2 -> RefOrdered.compare gr1 gr2 + | DCtx (tl1, tr1), DCtx (tl2, tr2) + | DLambda (tl1, tr1), DCtx (tl2, tr2) + | DApp (tl1, tr1), DCtx (tl2, tr2) -> + let c = cmp tl1 tl2 in + if c = 0 then cmp tr1 tr2 else c + + | DCase (ci1, c1, t1, p1), DCase (ci2, c2, t2, p2) -> + let c = cmp c1 c2 in + if c = 0 then + let c = cmp t1 t2 in + if c = 0 then + let c = Array.compare cmp p1 p2 in + if c = 0 then compare_ci ci1 ci2 + else c + else c + else c + + | DFix (i1, j1, tl1, pl1), DFix (i2, j2, tl2, pl2) -> + let c = Int.compare j1 j2 in + if c = 0 then + let c = Array.compare Int.compare i1 i2 in + if c = 0 then + let c = Array.compare cmp tl1 tl2 in + if c = 0 then Array.compare cmp pl1 pl2 + else c + else c + else c + | DCoFix (i1, tl1, pl1), DCoFix (i2, tl2, pl2) -> + let c = Int.compare i1 i2 in + if c = 0 then + let c = Array.compare cmp tl1 tl2 in + if c = 0 then Array.compare cmp pl1 pl2 + else c + else c + | _ -> Pervasives.compare t1 t2 (** OK **) + + 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 dummy_cmp () () = 0 + + let fold2 (f:'a -> 'b -> 'c -> 'a) (acc:'a) (c1:'b t) (c2:'c t) : 'a = + let head w = map (fun _ -> ()) w in + if not (Int.equal (compare dummy_cmp (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 not (Int.equal (compare dummy_cmp (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 + + let compare t1 t2 = compare dummy_cmp t1 t2 + +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 = int + = Dnet.Make(DTerm)(Ident)(Int) + + type t = TDnet.t + + type ident = TDnet.ident + + (** We will freshen metas on the fly, to cope with the implementation defect + of Term_dnet which requires metas to be all distinct. *) + let fresh_meta = + let index = ref 0 in + fun () -> + let ans = !index in + let () = index := succ ans in + ans + + open DTerm + open TDnet + + let pat_of_constr c : term_pattern = + (** To each evar we associate a unique identifier. *) + let metas = ref Evar.Map.empty in + let rec pat_of_constr c = match kind_of_term c with + | Rel _ -> Term DRel + | Sort _ -> Term DSort + | Var i -> Term (DRef (VarRef i)) + | Const (c,u) -> Term (DRef (ConstRef c)) + | Ind (i,u) -> Term (DRef (IndRef i)) + | Construct (c,u)-> Term (DRef (ConstructRef c)) + | Term.Meta _ -> assert false + | Evar (i,_) -> + let meta = + try Evar.Map.find i !metas + with Not_found -> + let meta = fresh_meta () in + let () = metas := Evar.Map.add i meta !metas in + meta + in + Meta meta + | 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) + | Proj (p,c) -> + Term (DApp (Term (DRef (ConstRef p)), pat_of_constr c)) + + and ctx_of_constr ctx c = 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 + in + 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 () = Meta (fresh_meta ()) + + let rec remove_cap : term_pattern -> term_pattern = function + | Term (DCons (t,u)) -> Term (DCons (t,remove_cap u)) + | Term DNil -> new_meta() + | Meta _ as m -> m + | _ -> 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 + + (* debug *) + let rec pr_term_pattern p = + (fun pr_t -> function + | Term t -> pr_t t + | Meta m -> str"["++Pp.int (Obj.magic m)++str"]" + ) (pr_dconstr pr_term_pattern) p + + let search_pat cpat dpat dn = + let whole_c = cpat in + (* if we are at the root, add an empty context *) + let dpat = under_prod (empty_ctx dpat) 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 wc,whole_c = if Opt.direction then whole_c,wc else wc,whole_c in + try + let _ = Termops.filtering ctx Reduction.CUMUL wc whole_c in + id :: acc + with Termops.CannotFilter -> (* msgnl(str"recon "++Termops.print_constr_env (Global.env()) wc); *) acc + ) (TDnet.find_match dpat dn) [] + + (* + * 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 + + let find_all dn = Idset.elements (TDnet.find_all dn) + + let map f dn = TDnet.map f (fun x -> x) dn +end + +module type S = +sig + type t + type ident + + val empty : t + val add : constr -> ident -> t -> t + val union : t -> t -> t + val subst : substitution -> t -> t + val search_pattern : t -> constr -> ident list + val find_all : t -> ident list + val map : (ident -> ident) -> t -> t +end diff --git a/tactics/term_dnet.mli b/tactics/term_dnet.mli new file mode 100644 index 0000000000..7825ebdf1a --- /dev/null +++ b/tactics/term_dnet.mli @@ -0,0 +1,88 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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 + + 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 -> ident list + + (** [find_all dn] returns all idents contained in dn *) + val find_all : t -> ident list + + val map : (ident -> ident) -> t -> t +end + +module Make : + functor (Ident : IDENT) -> + functor (Opt : OPT) -> + S with type ident = Ident.t -- cgit v1.2.3