From bf9379dc09f413fab73464aaaef32f7d3d6975f2 Mon Sep 17 00:00:00 2001 From: puech Date: Sat, 17 Jan 2009 12:41:35 +0000 Subject: DISCLAIMER ========== This big patch is commited here with a HUGE experimental tag on it. It is probably not a finished job. The aim of committing it now, as agreed with Hugo, is to get some feedback from potential users to identify more clearly the directions the implementation could take. So please feel free to mail me any remarks, bug reports or advices at . Here are the changes induced by it : For the user ============ * Search tools have been reimplemented to be faster and more general. Affected are [SearchPattern], [SearchRewrite] and [Search] (not [SearchAbout] yet). Changes are: - All of them accept general constructions, and previous syntactical limitations are abolished. In particular, one can for example [SearchPattern (nat -> Prop)], which will find [isSucc], but also [le], [gt] etc. - Patterns are typed. This means that you cannot search mistyped expressions anymore. I'm not sure if it's a good or a bad thing though (especially regarding coercions)... * New tool to automatically infer (some) Record/Typeclasses instances. Usage : [Record/Class *Infer* X := ...] flags a record/class as subject to instance search. There is also an option to activate/deactivate the search [Set/Unset Autoinstance]. It works by finding combinations of definitions (actually all kinds of objects) which forms a record instance, possibly parameterized. It is activated at two moments: - A complete search is done when defining a new record, to find all possible instances that could have been formed with past definitions. Example: Require Import List. Record Infer Monoid A (op:A->A->A) e := { assoc : forall x y z, op x (op y z) = op (op x y) z; idl : forall x, x = op x e ; idr : forall x, x = op e x }. new instance Monoid_autoinstance_1 : (Monoid nat plus 0) [...] - At each new declaration (Definition, Axiom, Inductive), a search is made to find instances involving the new object. Example: Parameter app_nil_beg : forall A (l:list A), l = nil ++ l. new instance Build_Monoid_autoinstance_12 : (forall H : Type, Monoid (list H) app nil) := (fun H : Type => Build_Monoid (list H) app nil ass_app (app_nil_beg H) (app_nil_end H)) For the developper ================== * New yet-to-be-named datastructure in [lib/dnet.ml]. Should do efficient one-to-many or many-to-one non-linear first-order filtering, faster than traditional methods like discrimination nets (so yes, the name of the file should probably be changed). * Comes with its application to Coq's terms [pretyping/term_dnet.ml]. Terms are represented so that you can search for patterns under products as fast as you would do not under products, and facilities are provided to express other kind of searches (head of application, under equality, whatever you need that can be expressed as a pattern) * A global repository of all objects defined and imported is maintained [toplevel/libtypes.ml], with all search facilities described before. * A certain kind of proof search in [toplevel/autoinstance.ml]. For the moment it is specialized on finding instances, but it should be generalizable and reusable (more on this in a few months :-). The bad news ============ * Compile time should increase by 0 to 15% (depending on the size of the Requires done). This could be optimized greatly by not performing substitutions on modules which are not functors I think. There may also be some inefficiency sources left in my code though... * Vo's also gain a little bit of weight (20%). That's inevitable if I wanted to store the big datastructure of objects, but could also be optimized some more. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11794 85f007b7-540e-0410-9357-904b9bb8a0f7 --- lib/dnet.ml | 240 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ lib/dnet.mli | 128 +++++++++++++++++++++++++++++++ 2 files changed, 368 insertions(+) create mode 100644 lib/dnet.ml create mode 100644 lib/dnet.mli (limited to 'lib') diff --git a/lib/dnet.ml b/lib/dnet.ml new file mode 100644 index 0000000000..b5a7bb7283 --- /dev/null +++ b/lib/dnet.ml @@ -0,0 +1,240 @@ +(************************************************************************) +(* 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 'a pattern = + | Term of 'a + | Meta of meta + type term_pattern = ('a structure) pattern as 'a + val empty : t + val add : t -> term_pattern -> ident -> t + val find_all : t -> Idset.t + val fold_pattern : + (meta -> t -> 'a -> '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 pattern = + | Term of 'a + | Meta of meta + + type 'a structure = 'a T.t + + 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 term_pattern = term_pattern structure pattern + 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) + + exception 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 Empty + 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 | Empty -> None,acc + + (* 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 m t acc -> +(* Printf.printf "eval pat %d\n" (Obj.magic m:int);*) + Some (option_any2 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))) + ) None p t in + try option_any2 Idset.inter mset lset + with Not_found -> Idset.empty + + 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 new file mode 100644 index 0000000000..a01bbb0e2e --- /dev/null +++ b/lib/dnet.mli @@ -0,0 +1,128 @@ +(************************************************************************) +(* 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 'a pattern = + | Term of 'a + | Meta of meta + + type term_pattern = 'a structure pattern as 'a + + 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 : + (meta -> t -> 'a -> '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 -- cgit v1.2.3