diff options
Diffstat (limited to 'tactics/dn.ml')
| -rw-r--r-- | tactics/dn.ml | 54 |
1 files changed, 37 insertions, 17 deletions
diff --git a/tactics/dn.ml b/tactics/dn.ml index ab908ff9..2a8166dc 100644 --- a/tactics/dn.ml +++ b/tactics/dn.ml @@ -1,3 +1,4 @@ +(* -*- compile-command: "make -C .. bin/coqtop.byte" -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -6,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: dn.ml 5920 2004-07-16 20:01:26Z herbelin $ *) +(* $Id: dn.ml 11282 2008-07-28 11:51:53Z msozeau $ *) (* This file implements the basic structure of what Chet called ``discrimination nets''. If my understanding is right, it serves @@ -32,6 +33,10 @@ type ('lbl,'pat) decompose_fun = 'pat -> ('lbl * 'pat list) option +type 'res lookup_res = Label of 'res | Nothing | Everything + +type ('lbl,'tree) lookup_fun = 'tree -> ('lbl * 'tree list) lookup_res + type ('lbl,'pat,'inf) t = (('lbl * int) option,'pat * 'inf) Tlm.t let create () = Tlm.empty @@ -46,29 +51,44 @@ let path_of dna = and pathrec deferred t = match dna t with - | None -> - None :: (path_of_deferred deferred) - | Some (lbl,[]) -> - (Some (lbl,0))::(path_of_deferred deferred) - | Some (lbl,(h::def_subl as v)) -> - (Some (lbl,List.length v))::(pathrec (def_subl@deferred) h) + | None -> + None :: (path_of_deferred deferred) + | Some (lbl,[]) -> + (Some (lbl,0))::(path_of_deferred deferred) + | Some (lbl,(h::def_subl as v)) -> + (Some (lbl,List.length v))::(pathrec (def_subl@deferred) h) in pathrec [] let tm_of tm lbl = - try [Tlm.map tm lbl] with Not_found -> [] - + try [Tlm.map tm lbl, true] with Not_found -> [] + +let rec skip_arg n tm = + if n = 0 then [tm,true] + else + List.flatten + (List.map + (fun a -> match a with + | None -> skip_arg (pred n) (Tlm.map tm a) + | Some (lbl,m) -> + skip_arg (pred n + m) (Tlm.map tm a)) + (Tlm.dom tm)) + let lookup tm dna t = let rec lookrec t tm = - (tm_of tm None)@ - (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) + match dna t with + | Nothing -> tm_of tm None + | Label(lbl,v) -> + tm_of tm None@ + (List.fold_left + (fun l c -> + List.flatten(List.map (fun (tm, b) -> + if b then lookrec c tm + else [tm,b]) l)) + (tm_of tm (Some(lbl,List.length v))) v) + | Everything -> skip_arg 1 tm in - List.flatten(List.map Tlm.xtract (lookrec t tm)) + List.flatten (List.map (fun (tm,b) -> Tlm.xtract tm) (lookrec t tm)) let add tm dna (pat,inf) = let p = path_of dna pat in Tlm.add tm (p,(pat,inf)) |