--- a/doc-src/IsarRef/Thy/Misc.thy Fri Feb 13 23:55:04 2009 +0100
+++ b/doc-src/IsarRef/Thy/Misc.thy Fri Feb 13 23:55:24 2009 +0100
@@ -16,6 +16,7 @@
@{command_def "print_attributes"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@{command_def "print_theorems"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@{command_def "find_theorems"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+ @{command_def "find_consts"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@{command_def "thm_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@{command_def "print_facts"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@{command_def "print_binds"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@@ -25,10 +26,14 @@
'print\_theory' ( '!'?)
;
- 'find\_theorems' (('(' (nat)? ('with\_dups')? ')')?) (criterion *)
+ 'find\_theorems' (('(' (nat)? ('with\_dups')? ')')?) (thmcriterion *)
;
- criterion: ('-'?) ('name' ':' nameref | 'intro' | 'elim' | 'dest' |
- 'simp' ':' term | term)
+ thmcriterion: ('-'?) ('name' ':' nameref | 'intro' | 'elim' | 'dest' |
+ 'solves' | 'simp' ':' term | term)
+ ;
+ 'find\_consts' (constcriterion *)
+ ;
+ constcriterion: ('-'?) ('name' ':' nameref | 'strict' ':' type | type)
;
'thm\_deps' thmrefs
;
@@ -63,11 +68,13 @@
contain ``@{text "*"}'' wildcards. The criteria @{text intro},
@{text elim}, and @{text dest} select theorems that match the
current goal as introduction, elimination or destruction rules,
- respectively. The criterion @{text "simp: t"} selects all rewrite
- rules whose left-hand side matches the given term. The criterion
- term @{text t} selects all theorems that contain the pattern @{text
- t} -- as usual, patterns may contain occurrences of the dummy
- ``@{text _}'', schematic variables, and type constraints.
+ respectively. The criterion @{text "solves"} returns all rules
+ that would directly solve the current goal. The criterion
+ @{text "simp: t"} selects all rewrite rules whose left-hand side
+ matches the given term. The criterion term @{text t} selects all
+ theorems that contain the pattern @{text t} -- as usual, patterns
+ may contain occurrences of the dummy ``@{text _}'', schematic
+ variables, and type constraints.
Criteria can be preceded by ``@{text "-"}'' to select theorems that
do \emph{not} match. Note that giving the empty list of criteria
@@ -75,7 +82,16 @@
number of printed facts may be given; the default is 40. By
default, duplicates are removed from the search result. Use
@{text with_dups} to display duplicates.
-
+
+ \item @{command "find_consts"}~@{text criteria} prints all constants
+ whose type meets all of the given criteria. The criterion @{text
+ "strict: ty"} is met by any type that matches the type pattern
+ @{text ty}. Patterns may contain both the dummy type ``@{text _}''
+ and sort constraints. The criterion @{text ty} is similar, but it
+ also matches against subtypes. The criterion @{text "name: p"} and
+ the prefix ``@{text "-"}'' function as described for @{command
+ "find_theorems"}.
+
\item @{command "thm_deps"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}
visualizes dependencies of facts, using Isabelle's graph browser
tool (see also \cite{isabelle-sys}).
--- a/doc-src/IsarRef/Thy/document/Misc.tex Fri Feb 13 23:55:04 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/Misc.tex Fri Feb 13 23:55:24 2009 +0100
@@ -36,6 +36,7 @@
\indexdef{}{command}{print\_attributes}\hypertarget{command.print-attributes}{\hyperlink{command.print-attributes}{\mbox{\isa{\isacommand{print{\isacharunderscore}attributes}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
\indexdef{}{command}{print\_theorems}\hypertarget{command.print-theorems}{\hyperlink{command.print-theorems}{\mbox{\isa{\isacommand{print{\isacharunderscore}theorems}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
\indexdef{}{command}{find\_theorems}\hypertarget{command.find-theorems}{\hyperlink{command.find-theorems}{\mbox{\isa{\isacommand{find{\isacharunderscore}theorems}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
+ \indexdef{}{command}{find\_consts}\hypertarget{command.find-consts}{\hyperlink{command.find-consts}{\mbox{\isa{\isacommand{find{\isacharunderscore}consts}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
\indexdef{}{command}{thm\_deps}\hypertarget{command.thm-deps}{\hyperlink{command.thm-deps}{\mbox{\isa{\isacommand{thm{\isacharunderscore}deps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
\indexdef{}{command}{print\_facts}\hypertarget{command.print-facts}{\hyperlink{command.print-facts}{\mbox{\isa{\isacommand{print{\isacharunderscore}facts}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
\indexdef{}{command}{print\_binds}\hypertarget{command.print-binds}{\hyperlink{command.print-binds}{\mbox{\isa{\isacommand{print{\isacharunderscore}binds}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
@@ -45,10 +46,14 @@
'print\_theory' ( '!'?)
;
- 'find\_theorems' (('(' (nat)? ('with\_dups')? ')')?) (criterion *)
+ 'find\_theorems' (('(' (nat)? ('with\_dups')? ')')?) (thmcriterion *)
;
- criterion: ('-'?) ('name' ':' nameref | 'intro' | 'elim' | 'dest' |
- 'simp' ':' term | term)
+ thmcriterion: ('-'?) ('name' ':' nameref | 'intro' | 'elim' | 'dest' |
+ 'solves' | 'simp' ':' term | term)
+ ;
+ 'find\_consts' (constcriterion *)
+ ;
+ constcriterion: ('-'?) ('name' ':' nameref | 'strict' ':' type | type)
;
'thm\_deps' thmrefs
;
@@ -83,10 +88,13 @@
contain ``\isa{{\isachardoublequote}{\isacharasterisk}{\isachardoublequote}}'' wildcards. The criteria \isa{intro},
\isa{elim}, and \isa{dest} select theorems that match the
current goal as introduction, elimination or destruction rules,
- respectively. The criterion \isa{{\isachardoublequote}simp{\isacharcolon}\ t{\isachardoublequote}} selects all rewrite
- rules whose left-hand side matches the given term. The criterion
- term \isa{t} selects all theorems that contain the pattern \isa{t} -- as usual, patterns may contain occurrences of the dummy
- ``\isa{{\isacharunderscore}}'', schematic variables, and type constraints.
+ respectively. The criterion \isa{{\isachardoublequote}solves{\isachardoublequote}} returns all rules
+ that would directly solve the current goal. The criterion
+ \isa{{\isachardoublequote}simp{\isacharcolon}\ t{\isachardoublequote}} selects all rewrite rules whose left-hand side
+ matches the given term. The criterion term \isa{t} selects all
+ theorems that contain the pattern \isa{t} -- as usual, patterns
+ may contain occurrences of the dummy ``\isa{{\isacharunderscore}}'', schematic
+ variables, and type constraints.
Criteria can be preceded by ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' to select theorems that
do \emph{not} match. Note that giving the empty list of criteria
@@ -94,7 +102,14 @@
number of printed facts may be given; the default is 40. By
default, duplicates are removed from the search result. Use
\isa{with{\isacharunderscore}dups} to display duplicates.
-
+
+ \item \hyperlink{command.find-consts}{\mbox{\isa{\isacommand{find{\isacharunderscore}consts}}}}~\isa{criteria} prints all constants
+ whose type meets all of the given criteria. The criterion \isa{{\isachardoublequote}strict{\isacharcolon}\ ty{\isachardoublequote}} is met by any type that matches the type pattern
+ \isa{ty}. Patterns may contain both the dummy type ``\isa{{\isacharunderscore}}''
+ and sort constraints. The criterion \isa{ty} is similar, but it
+ also matches against subtypes. The criterion \isa{{\isachardoublequote}name{\isacharcolon}\ p{\isachardoublequote}} and
+ the prefix ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' function as described for \hyperlink{command.find-theorems}{\mbox{\isa{\isacommand{find{\isacharunderscore}theorems}}}}.
+
\item \hyperlink{command.thm-deps}{\mbox{\isa{\isacommand{thm{\isacharunderscore}deps}}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}
visualizes dependencies of facts, using Isabelle's graph browser
tool (see also \cite{isabelle-sys}).
--- a/lib/Tools/codegen Fri Feb 13 23:55:04 2009 +0100
+++ b/lib/Tools/codegen Fri Feb 13 23:55:24 2009 +0100
@@ -36,5 +36,5 @@
THY=$(echo $THY | sed -e 's/\\/\\\\"/g; s/"/\\\"/g')
ISAR="theory Codegen imports \"$THY\" begin export_code $CMD end"
-echo "$ISAR" | "$ISABELLE_PROCESS" -I "$IMAGE" || exit 1
-
+echo "$ISAR" | "$ISABELLE_TOOL" tty -l "$IMAGE"
+exit ${PIPESTATUS[1]}
--- a/src/HOL/Tools/datatype_package.ML Fri Feb 13 23:55:04 2009 +0100
+++ b/src/HOL/Tools/datatype_package.ML Fri Feb 13 23:55:24 2009 +0100
@@ -632,9 +632,8 @@
local
val sym_datatype = Pretty.str "\\isacommand{datatype}";
-val sym_binder = Pretty.str "{\\isacharequal}";
-val sym_of = Pretty.str "of";
-val sym_sep = Pretty.str "{\\isacharbar}";
+val sym_binder = Pretty.str "\\ {\\isacharequal}";
+val sym_sep = Pretty.str "{\\isacharbar}\\ ";
in
@@ -660,17 +659,19 @@
| pretty_constr (co, [ty']) =
(Pretty.block o Pretty.breaks)
[Syntax.pretty_term ctxt (Const (co, ty' --> ty)),
- sym_of, Syntax.pretty_typ ctxt ty']
+ Syntax.pretty_typ ctxt ty']
| pretty_constr (co, tys) =
(Pretty.block o Pretty.breaks)
(Syntax.pretty_term ctxt (Const (co, tys ---> ty)) ::
- sym_of :: map pretty_typ_br tys);
- in (Pretty.block o Pretty.breaks) (
- sym_datatype
- :: Syntax.pretty_typ ctxt ty
- :: sym_binder
- :: separate sym_sep (map pretty_constr cos)
- ) end
+ map pretty_typ_br tys);
+ in
+ Pretty.block
+ (sym_datatype :: Pretty.brk 1 ::
+ Syntax.pretty_typ ctxt ty ::
+ sym_binder :: Pretty.brk 1 ::
+ flat (separate [Pretty.brk 1, sym_sep]
+ (map (single o pretty_constr) cos)))
+ end
end;
--- a/src/Pure/General/seq.ML Fri Feb 13 23:55:04 2009 +0100
+++ b/src/Pure/General/seq.ML Fri Feb 13 23:55:24 2009 +0100
@@ -89,17 +89,17 @@
(*the list of the first n elements, paired with rest of sequence;
if length of list is less than n, then sequence had less than n elements*)
fun chop n xq =
- if n <= (0: int) then ([], xq)
+ if n <= (0 : int) then ([], xq)
else
(case pull xq of
NONE => ([], xq)
| SOME (x, xq') => apfst (Basics.cons x) (chop (n - 1) xq'));
-(* truncate the sequence after n elements *)
-fun take n s = let
- fun f 0 _ () = NONE
- | f n ss () = Option.map (apsnd (make o f (n - 1))) (pull ss);
- in make (f n s) end;
+(*truncate the sequence after n elements*)
+fun take n xq =
+ if n <= (0 : int) then empty
+ else make (fn () =>
+ (Option.map o apsnd) (take (n - 1)) (pull xq));
(*conversion from sequence to list*)
fun list_of xq =
--- a/src/Pure/Isar/find_consts.ML Fri Feb 13 23:55:04 2009 +0100
+++ b/src/Pure/Isar/find_consts.ML Fri Feb 13 23:55:24 2009 +0100
@@ -44,7 +44,31 @@
fun opt_not f (c as (_, (ty, _))) = if is_some (f c)
then NONE else SOME (size_of_typ ty);
+fun filter_const (_, NONE) = NONE
+ | filter_const (f, (SOME (c, r))) = Option.map
+ (pair c o ((curry Int.min) r)) (f c);
+
+fun pretty_criterion (b, c) =
+ let
+ fun prfx s = if b then s else "-" ^ s;
+ in
+ (case c of
+ Strict pat => Pretty.str (prfx "strict: " ^ quote pat)
+ | Loose pat => Pretty.str (prfx (quote pat))
+ | Name name => Pretty.str (prfx "name: " ^ quote name))
+ end;
+
+fun pretty_const ctxt (nm, ty) = let
+ val ty' = Logic.unvarifyT ty;
+ in
+ Pretty.block [Pretty.quote (Pretty.str nm), Pretty.fbrk,
+ Pretty.str "::", Pretty.brk 1,
+ Pretty.quote (Syntax.pretty_typ ctxt ty')]
+ end;
+
fun find_consts ctxt raw_criteria = let
+ val start = start_timing ();
+
val thy = ProofContext.theory_of ctxt;
val low_ranking = 10000;
@@ -68,28 +92,27 @@
val criteria = map make_criterion ((!default_criteria) @ raw_criteria);
val (_, consts) = (#constants o Consts.dest o Sign.consts_of) thy;
-
- fun filter_const (_, NONE) = NONE
- | filter_const (f, (SOME (c, r))) = Option.map
- (pair c o ((curry Int.min) r))
- (f c);
-
fun eval_entry c = foldl filter_const (SOME (c, low_ranking)) criteria;
- fun show (nm, ty) = let
- val ty' = Logic.unvarifyT ty;
- in
- (Pretty.block [Pretty.quote (Pretty.str nm), Pretty.fbrk,
- Pretty.str "::", Pretty.brk 1,
- Pretty.quote (Syntax.pretty_typ ctxt ty')])
- end;
+ val matches = Symtab.fold (cons o eval_entry) consts []
+ |> map_filter I
+ |> sort (rev_order o int_ord o pairself snd)
+ |> map ((apsnd fst) o fst);
+
+ val end_msg = " in " ^
+ (List.nth (String.tokens Char.isSpace (end_timing start), 3))
+ ^ " secs"
in
- Symtab.fold (cons o eval_entry) consts []
- |> map_filter I
- |> sort (rev_order o int_ord o pairself snd)
- |> map ((apsnd fst) o fst)
- |> map show
- |> Pretty.big_list "results:"
+ Pretty.big_list "searched for:" (map pretty_criterion raw_criteria)
+ :: Pretty.str ""
+ :: (Pretty.str o concat)
+ (if null matches
+ then ["nothing found", end_msg]
+ else ["found ", (string_of_int o length) matches,
+ " constants", end_msg, ":"])
+ :: Pretty.str ""
+ :: map (pretty_const ctxt) matches
+ |> Pretty.chunks
|> Pretty.writeln
end handle ERROR s => Output.error_msg s