From 80297f53a4a43aff327426a08ffd58236ec4d56d Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 26 Apr 2000 09:50:56 +0000 Subject: Nettoyage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@367 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tactics/btermdn.ml | 25 ++++++++----------------- tactics/dn.ml | 36 +++++++++++++++--------------------- tactics/dn.mli | 36 ++++++++++++++++++++++-------------- tactics/termdn.ml | 8 +++++--- tactics/termdn.mli | 30 +++++++++++++++++++++++++----- 5 files changed, 75 insertions(+), 60 deletions(-) (limited to 'tactics') diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml index 3015e651b..e6a4b43dd 100644 --- a/tactics/btermdn.ml +++ b/tactics/btermdn.ml @@ -26,27 +26,18 @@ let bounded_constr_val_discr (t,depth) = | None -> None | Some (c,l) -> Some(c,List.map (fun c -> (c,depth-1)) l) -type 'a t = (lbl,constr * int,'a) Dn.under_t +type 'a t = (lbl,constr * int,'a) Dn.t -let newdn () = Dn.create bounded_constr_pat_discr +let create = Dn.create -let ex_termdn = newdn() +let add dn (c,v) = Dn.add dn bounded_constr_pat_discr ((c,!dnet_depth),v) -let inDN tdn = { - Dn.args = ex_termdn.Dn.args; - Dn.tm = tdn } +let rmv dn (c,v) = Dn.rmv dn bounded_constr_pat_discr ((c,!dnet_depth),v) -let outDN dn = dn.Dn.tm - -let create () = outDN (newdn()) - -let add dn (c,v) = outDN (Dn.add (inDN dn) ((c,!dnet_depth),v)) - -let rmv dn (c,v) = outDN (Dn.rmv (inDN dn) ((c,!dnet_depth),v)) - -let lookup dn t = +let lookup dn t = List.map (fun ((c,_),v) -> (c,v)) - (Dn.lookup (inDN dn) bounded_constr_val_discr (t,!dnet_depth)) + (Dn.lookup dn bounded_constr_val_discr (t,!dnet_depth)) + +let app f dn = Dn.app (fun ((c,_),v) -> f(c,v)) dn -let app f dn = Dn.app (fun ((c,_),v) -> f(c,v)) (inDN dn) diff --git a/tactics/dn.ml b/tactics/dn.ml index 33ce0df5d..b53fb2661 100644 --- a/tactics/dn.ml +++ b/tactics/dn.ml @@ -2,7 +2,7 @@ (* $Id$ *) (* This file implements the basic structure of what Chet called - ``discrimination nets''. If my understanding is wright, it serves + ``discrimination nets''. If my understanding is right, it serves to associate actions (for example, tactics) with a priority to term patterns, so that if a hypothesis matches a pattern in the net, then the associated tactic is applied. Discrimination nets are used @@ -23,15 +23,14 @@ (* Definition of the basic structure *) -type ('lbl,'pat) dn_args = 'pat -> ('lbl * 'pat list) option +type ('lbl,'pat) decompose_fun = 'pat -> ('lbl * 'pat list) option -type ('lbl,'pat,'inf) under_t = (('lbl * int) option,'pat * 'inf) Tlm.t +type ('lbl,'pat,'inf) t = (('lbl * int) option,'pat * 'inf) Tlm.t -type ('lbl,'pat,'inf) t = { - tm : ('lbl,'pat,'inf) under_t; - args : ('lbl,'pat) dn_args } +let create () = Tlm.empty -let create dna = { tm = Tlm.empty; args = dna } +(* [path_of dna pat] returns the list of nodes of the pattern [pat] read in +prefix ordering, [dna] is the function returning the main node of a pattern *) let path_of dna = let rec path_of_deferred = function @@ -52,28 +51,23 @@ let path_of dna = let tm_of tm lbl = try [Tlm.map tm lbl] with Not_found -> [] -let lookup dnm dna' t = +let lookup tm dna t = let rec lookrec t tm = (tm_of tm None)@ - (match dna' t with + (match dna t with | None -> [] | Some(lbl,v) -> List.fold_left (fun l c -> List.flatten(List.map (lookrec c) l)) (tm_of tm (Some(lbl,List.length v))) v) in - List.flatten(List.map Tlm.xtract (lookrec t dnm.tm)) + List.flatten(List.map Tlm.xtract (lookrec t tm)) -let upd dnm f = { args = dnm.args; tm = f dnm.args dnm.tm } - -let add dnm (pat,inf) = - upd dnm - (fun dna tm -> - let p = path_of dna pat in Tlm.add tm (p,(pat,inf))) +let add tm dna (pat,inf) = + let p = path_of dna pat in Tlm.add tm (p,(pat,inf)) -let rmv dnm (pat,inf) = - upd dnm - (fun dna tm -> - let p = path_of dna pat in Tlm.rmv tm (p,(pat,inf))) +let rmv tm dna (pat,inf) = + let p = path_of dna pat in Tlm.rmv tm (p,(pat,inf)) -let app f dnm = Tlm.app (fun (_,p) -> f p) dnm.tm +let app f tm = Tlm.app (fun (_,p) -> f p) tm + diff --git a/tactics/dn.mli b/tactics/dn.mli index 211b75a36..42c6303a0 100644 --- a/tactics/dn.mli +++ b/tactics/dn.mli @@ -3,23 +3,31 @@ (* Discrimination nets. *) -type ('lbl,'pat) dn_args = 'pat -> ('lbl * 'pat list) option +type ('lbl,'tree) decompose_fun = 'tree -> ('lbl * 'tree list) option -type ('lbl,'pat,'inf) t = { - tm : (('lbl * int) option,'pat * 'inf) Tlm.t; - args : ('lbl,'pat) dn_args } +type ('lbl,'pat,'inf) t (* = (('lbl * int) option,'pat * 'inf) Tlm.t *) -type ('lbl,'pat,'inf) under_t = (('lbl * int) option,'pat * 'inf) Tlm.t - -val create : ('lbl,'pat) dn_args -> ('lbl,'pat,'inf) t - -val add : ('lbl,'pat,'inf) t -> 'pat * 'inf -> ('lbl,'pat,'inf) t +val create : unit -> ('lbl,'pat,'inf) t -val rmv : ('lbl,'pat,'inf) t -> 'pat * 'inf -> ('lbl,'pat,'inf) t +(* [add t f (tree,inf)] adds a structured object [tree] together with + the associated information [inf] to the table [t]; the function + [f] is used to translated [tree] into its prefix decomposition: [f] + must decompose any tree into a label characterizing its root node and + the list of its subtree *) -val path_of : ('lbl,'pat) dn_args -> 'pat -> ('lbl * int) option list - -val lookup : - ('lbl,'pat,'inf) t -> ('lbl,'term) dn_args -> 'term -> ('pat * 'inf) list +val add : ('lbl,'pat,'inf) t -> ('lbl,'pat) decompose_fun -> 'pat * 'inf + -> ('lbl,'pat,'inf) t + +val rmv : ('lbl,'pat,'inf) t -> ('lbl,'pat) decompose_fun -> 'pat * 'inf + -> ('lbl,'pat,'inf) t + +(* [lookup t f tree] looks for trees (and their associated + information) in table [t] such that the structured object [tree] + matches against them; [f] is used to translated [tree] into its + prefix decomposition: [f] must decompose any tree into a label + characterizing its root node and the list of its subtree *) + +val lookup : ('lbl,'pat,'inf) t -> ('lbl,'term) decompose_fun -> 'term + -> ('pat * 'inf) list val app : (('pat * 'inf) -> unit) -> ('lbl,'pat,'inf) t -> unit diff --git a/tactics/termdn.ml b/tactics/termdn.ml index f1f8374c9..fda033f26 100644 --- a/tactics/termdn.ml +++ b/tactics/termdn.ml @@ -26,6 +26,7 @@ let decomp = in decrec [] + let constr_pat_discr t = if not(occur_meta t) then None @@ -58,10 +59,11 @@ let constr_val_discr_nil t = | None -> None | Some (c,_) -> Some(c,[]) -let create () = Dn.create constr_pat_discr +let create = Dn.create + +let add dn = Dn.add dn constr_pat_discr -let add = Dn.add -let rmv = Dn.rmv +let rmv dn = Dn.rmv dn constr_pat_discr let lookup dn t = Dn.lookup dn constr_val_discr t diff --git a/tactics/termdn.mli b/tactics/termdn.mli index 95cfc6243..62066f604 100644 --- a/tactics/termdn.mli +++ b/tactics/termdn.mli @@ -8,20 +8,40 @@ open Term (* Discrimination nets of terms. *) -type lbl = - | TERM of constr - | DOPER of sorts oper - | DLAMBDA +(* This module registers actions (typically tactics) mapped to patterns *) + +(* Patterns are stocked linearly as the list of its node in prefix +order in such a way patterns having the same prefix have this common +prefix shared and the seek for the action associated to the patterns +that a term matches are found in time proportional to the maximal +number of nodes of the patterns matching the term *) -type 'a t = (lbl,constr,'a) Dn.t +type 'a t val create : unit -> 'a t +(* [add t (c,a)] adds to table [t] pattern [c] associated to action [act] *) + val add : 'a t -> (constr * 'a) -> 'a t + val rmv : 'a t -> (constr * 'a) -> 'a t +(* [lookup t c] looks for patterns (with their action) matching term [c] *) + val lookup : 'a t -> constr -> (constr * 'a) list + val app : ((constr * 'a) -> unit) -> 'a t -> unit + +(*i*) +(* These are for Nbtermdn *) + +type lbl = + | TERM of constr + | DOPER of sorts oper + | DLAMBDA + val constr_pat_discr : constr -> (lbl * constr list) option val constr_val_discr : constr -> (lbl * constr list) option + +(*i*) -- cgit v1.2.3