# HG changeset patch
# User nipkow
# Date 1234565724 -3600
# Node ID 445320b620ef5efa291cfee544e5a14eee827897
# Parent  333cbcad74c3dda842b4ae74f8447a42b0a9f08a# Parent  f4b3f8fbf599f81bd2c5cd66f3856714ac334cc9
merged

diff -r f4b3f8fbf599 -r 445320b620ef doc-src/IsarRef/Thy/Misc.thy
--- 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}).
diff -r f4b3f8fbf599 -r 445320b620ef doc-src/IsarRef/Thy/document/Misc.tex
--- 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}).
diff -r f4b3f8fbf599 -r 445320b620ef lib/Tools/codegen
--- 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]}
diff -r f4b3f8fbf599 -r 445320b620ef src/HOL/Library/Formal_Power_Series.thy
diff -r f4b3f8fbf599 -r 445320b620ef src/HOL/Tools/datatype_package.ML
--- 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;
 
diff -r f4b3f8fbf599 -r 445320b620ef src/Pure/General/seq.ML
--- 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 =
diff -r f4b3f8fbf599 -r 445320b620ef src/Pure/Isar/find_consts.ML
--- 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