diff options
| -rw-r--r-- | .depend | 3 | ||||
| -rw-r--r-- | Makefile | 14 | ||||
| -rw-r--r-- | doc/tactics.dep.ps | 158 | ||||
| -rw-r--r-- | lib/tlm.mli | 22 | ||||
| -rw-r--r-- | tactics/dn.ml | 79 | ||||
| -rw-r--r-- | tactics/dn.mli | 25 | ||||
| -rw-r--r-- | tactics/doc.tex | 11 |
7 files changed, 308 insertions, 4 deletions
@@ -74,6 +74,7 @@ proofs/tacmach.cmi: kernel/environ.cmi proofs/evar_refiner.cmi \ proofs/tacred.cmi: kernel/closure.cmi kernel/environ.cmi kernel/evd.cmi \ kernel/names.cmi kernel/reduction.cmi kernel/term.cmi proofs/typing_ev.cmi: kernel/environ.cmi kernel/evd.cmi kernel/term.cmi +tactics/dn.cmi: lib/tlm.cmi toplevel/errors.cmi: parsing/coqast.cmi lib/pp.cmi toplevel/himsg.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \ kernel/sign.cmi kernel/term.cmi kernel/type_errors.cmi @@ -343,6 +344,8 @@ proofs/typing_ev.cmo: kernel/environ.cmi kernel/generic.cmi kernel/names.cmi \ proofs/typing_ev.cmx: kernel/environ.cmx kernel/generic.cmx kernel/names.cmx \ kernel/reduction.cmx kernel/term.cmx kernel/type_errors.cmx \ kernel/typeops.cmx lib/util.cmx proofs/typing_ev.cmi +tactics/dn.cmo: lib/tlm.cmi tactics/dn.cmi +tactics/dn.cmx: lib/tlm.cmi tactics/dn.cmi toplevel/errors.cmo: parsing/ast.cmi lib/options.cmi lib/pp.cmi lib/util.cmi \ toplevel/errors.cmi toplevel/errors.cmx: parsing/ast.cmx lib/options.cmx lib/pp.cmx lib/util.cmx \ @@ -11,7 +11,7 @@ noargument: @echo or make archclean LOCALINCLUDES=-I config -I lib -I kernel -I library \ - -I proofs -I parsing -I toplevel + -I proofs -I tactics -I parsing -I toplevel INCLUDES=$(LOCALINCLUDES) -I $(CAMLP4LIB) BYTEFLAGS=$(INCLUDES) $(CAMLDEBUG) @@ -51,7 +51,9 @@ LIBRARY=library/libobject.cmo library/summary.cmo library/lib.cmo \ PROOFS=proofs/typing_ev.cmo proofs/tacred.cmo \ proofs/proof_trees.cmo proofs/logic.cmo \ proofs/refiner.cmo proofs/evar_refiner.cmo \ - proofs/macros.cmo proofs/tacinterp.cmo proofs/clenv.cmo + proofs/macros.cmo proofs/tacinterp.cmo # proofs/clenv.cmo + +TACTICS=tactics/dn.cmo PARSING=parsing/lexer.cmo parsing/coqast.cmo parsing/pcoq.cmo parsing/ast.cmo \ parsing/g_prim.cmo parsing/g_basevernac.cmo parsing/g_vernac.cmo \ @@ -63,7 +65,8 @@ TOPLEVEL=toplevel/himsg.cmo toplevel/errors.cmo toplevel/vernac.cmo \ CMA=$(CLIBS) $(CAMLP4OBJS) CMXA=$(CMA:.cma=.cmxa) -CMO=$(CONFIG) $(LIB) $(KERNEL) $(LIBRARY) $(PROOFS) $(PARSING) $(TOPLEVEL) +CMO=$(CONFIG) $(LIB) $(KERNEL) $(LIBRARY) $(PROOFS) $(TACTICS) \ + $(PARSING) $(TOPLEVEL) CMX=$(CMO:.cmo=.cmx) # Targets @@ -102,9 +105,10 @@ LPLIB = lib/doc.tex $(LIB:.cmo=.mli) LPKERNEL = kernel/doc.tex $(KERNEL:.cmo=.mli) LPLIBRARY = library/doc.tex $(LIBRARY:.cmo=.mli) LPPROOFS = proofs/doc.tex $(PROOFS:.cmo=.mli) +LPTACTICS = tactics/doc.tex $(TCATICS:.cmo=.mli) LPTOPLEVEL = toplevel/doc.tex $(TOPLEVEL:.cmo=.mli) LPFILES = doc/macros.tex doc/intro.tex $(LPLIB) $(LPKERNEL) $(LPLIBRARY) \ - $(LPPROOFS) $(LPTOPLEVEL) + $(LPPROOFS) $(LPTACTICS) $(LPTOPLEVEL) doc/coq.tex: doc/preamble.tex $(LPFILES) cat doc/preamble.tex > doc/coq.tex @@ -195,6 +199,7 @@ archclean:: rm -f kernel/*.cmx kernel/*.[so] rm -f library/*.cmx library/*.[so] rm -f proofs/*.cmx proofs/*.[so] + rm -f tactics/*.cmx tactics/*.[so] rm -f parsing/*.cmx parsing/*.[so] cleanall:: archclean @@ -205,6 +210,7 @@ cleanall:: archclean rm -f kernel/*.cm[io] kernel/*~ rm -f library/*.cm[io] library/*~ rm -f proofs/*.cm[io] proofs/*~ + rm -f tactics/*.cm[io] tactics/*~ rm -f parsing/*.cm[io] parsing/*.ppo parsing/*~ cleanconfig:: diff --git a/doc/tactics.dep.ps b/doc/tactics.dep.ps new file mode 100644 index 000000000..61da11e4f --- /dev/null +++ b/doc/tactics.dep.ps @@ -0,0 +1,158 @@ +%!PS-Adobe-2.0 +%%Creator: dot version uwin98 (01-26-98) +%%For: Bill Gates +%%Title: G +%%Pages: (atend) +%%BoundingBox: 36 36 37 37 +%%EndComments +%%BeginProlog +save +/DotDict 200 dict def +DotDict begin + +%%BeginResource: procset +/coord-font-family /Times-Roman def +/default-font-family /Times-Roman def +/coordfont coord-font-family findfont 8 scalefont def + +/InvScaleFactor 1.0 def +/set_scale { + dup 1 exch div /InvScaleFactor exch def + dup scale +} bind def + +% styles +/solid { } bind def +/dashed { [9 InvScaleFactor mul dup ] 0 setdash } bind def +/dotted { [1 InvScaleFactor mul 6 InvScaleFactor mul] 0 setdash } bind def +/invis {/fill {newpath} def /stroke {newpath} def /show {pop newpath} def} bind def +/bold { 2 setlinewidth } bind def +/filled { } bind def +/unfilled { } bind def +/rounded { } bind def +/diagonals { } bind def + +% hooks for setting color +/nodecolor { sethsbcolor } bind def +/edgecolor { sethsbcolor } bind def +/graphcolor { sethsbcolor } bind def +/nopcolor {pop pop pop} bind def + +/beginpage { % i j npages + /npages exch def + /j exch def + /i exch def + /str 10 string def + npages 1 gt { + gsave + coordfont setfont + 0 0 moveto + (() show i str cvs show (,) show j str cvs show ()) show + grestore + } if +} bind def + +/set_font { + findfont exch + scalefont setfont +} def + +% draw aligned label in bounding box aligned to current point +% alignfactor tells what fraction to place on the left. +% -.5 is centered. +/alignedtext { % text labelwidth fontsz alignfactor + /alignfactor exch def + /fontsz exch def + /width exch def + /text exch def + gsave + % even if node or edge is dashed, don't paint text with dashes + [] 0 setdash + currentpoint newpath moveto + text stringwidth pop + alignfactor mul fontsz -.3 mul rmoveto + text show + grestore +} def + +/boxprim { % xcorner ycorner xsize ysize + 4 2 roll + moveto + 2 copy + exch 0 rlineto + 0 exch rlineto + pop neg 0 rlineto + closepath +} bind def + +/ellipse_path { + /ry exch def + /rx exch def + /y exch def + /x exch def + matrix currentmatrix + newpath + x y translate + rx ry scale + 0 0 1 0 360 arc + setmatrix +} bind def + +/endpage { showpage } bind def + +/layercolorseq + [ % layer color sequence - darkest to lightest + [0 0 0] + [.2 .8 .8] + [.4 .8 .8] + [.6 .8 .8] + [.8 .8 .8] + ] +def + +/setlayer {/maxlayer exch def /curlayer exch def + layercolorseq curlayer get + aload pop sethsbcolor + /nodecolor {nopcolor} def + /edgecolor {nopcolor} def + /graphcolor {nopcolor} def +} bind def + +/onlayer { curlayer ne {invis} if } def + +/onlayers { + /myupper exch def + /mylower exch def + curlayer mylower lt + curlayer myupper gt + or + {invis} if +} def + +/curlayer 0 def + +%%EndResource +%%EndProlog +%%BeginSetup +14 default-font-family set_font +% /arrowlength 10 def +% /arrowwidth 5 def +%%EndSetup +%%Page: 1 1 +%%PageBoundingBox: 36 36 37 37 +gsave +35 35 2 2 boxprim clip newpath +36 36 translate +0 0 1 beginpage +0 0 translate 0 rotate +0.000 0.000 0.000 graphcolor +14.00 /Times-Roman set_font +endpage +grestore +%%PageTrailer +%%EndPage: 1 +%%Trailer +%%Pages: 1 +end +restore +%%EOF diff --git a/lib/tlm.mli b/lib/tlm.mli new file mode 100644 index 000000000..abf1efc67 --- /dev/null +++ b/lib/tlm.mli @@ -0,0 +1,22 @@ + +(* $Id$ *) + +type ('a,'b) t + +val create : unit -> ('a,'b) t + +(* Work on labels, not on paths *) + +val map : ('a,'b) t -> 'a -> ('a,'b) t +val xtract : ('a,'b) t -> 'b list +val dom : ('a,'b) t -> 'a list +val in_dom : ('a,'b) t -> 'a -> bool + +(* Work on paths, not labels *) + +val add : ('a,'b) t -> 'a list * 'b -> ('a,'b) t +val rmv : ('a,'b) t -> ('a list * 'b) -> ('a,'b) t + +val app : (('a list * 'c) -> unit) -> ('a,'c) t -> unit +val to_list : ('a,'b) t -> ('a list * 'b) list + diff --git a/tactics/dn.ml b/tactics/dn.ml new file mode 100644 index 000000000..cc811735a --- /dev/null +++ b/tactics/dn.ml @@ -0,0 +1,79 @@ + +(* $Id$ *) + +(* This file implements the basic structure of what Chet called + ``discrimination nets''. If my understanding is wright, 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 + (only) to implement the tactics Auto, DHyp and Point. + + A discrimination net is a tries structure, that is, a tree structure + specially conceived for searching patterns, like for example strings + --see the file Tlm.ml in the directory lib/util--. Here the tries + structure are used for looking for term patterns. + + This module is then used in : + - termdn.ml (discrimination nets of terms); + - btermdn.ml (discrimination nets of terms with bounded depth, + used in the tactic auto); + - nbtermdn.ml (named discrimination nets with bounded depth, used + in the tactics Dhyp and Point). + Eduardo (4/8/97) *) + +(* Definition of the basic structure *) + +type ('lbl,'pat) dn_args = 'pat -> ('lbl * 'pat list) option + +type ('lbl,'pat,'inf) under_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 dna = {tm = Tlm.create(); args = dna} + +let path_of dna = + let rec path_of_deferred = function + | [] -> [] + | h::tl -> pathrec tl h + + 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) + in + pathrec [] + +let tm_of tm lbl = + try [Tlm.map tm lbl] with Not_found -> [] + +let lookup dnm 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) + in + List.flatten(List.map Tlm.xtract (lookrec t dnm.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 rmv dnm (pat,inf) = + upd dnm + (fun dna tm -> + 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 diff --git a/tactics/dn.mli b/tactics/dn.mli new file mode 100644 index 000000000..211b75a36 --- /dev/null +++ b/tactics/dn.mli @@ -0,0 +1,25 @@ + +(* $Id$ *) + +(* Discrimination nets. *) + +type ('lbl,'pat) dn_args = 'pat -> ('lbl * 'pat list) option + +type ('lbl,'pat,'inf) t = { + tm : (('lbl * int) option,'pat * 'inf) Tlm.t; + args : ('lbl,'pat) dn_args } + +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 rmv : ('lbl,'pat,'inf) t -> 'pat * 'inf -> ('lbl,'pat,'inf) t + +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 app : (('pat * 'inf) -> unit) -> ('lbl,'pat,'inf) t -> unit diff --git a/tactics/doc.tex b/tactics/doc.tex new file mode 100644 index 000000000..d44cc14a5 --- /dev/null +++ b/tactics/doc.tex @@ -0,0 +1,11 @@ + +\newpage +\section*{The Tactics} + +\ocwsection \label{tactics} +This chapter describes the \Coq\ main tactics. +The modules of that chapter are organized as follows. + +\bigskip +\begin{center}\epsfig{file=tactics.dep.ps,width=\linewidth}\end{center} + |