# HG changeset patch
# User kleing
# Date 1234472018 -39600
# Node ID 29154e67731d963ede9848a103364b71bfd271ab
# Parent 58f3c48dbbb7dcbb61c88846361701f8898447a5
New command find_consts searching for constants by type (by Timothy Bourke).
diff -r 58f3c48dbbb7 -r 29154e67731d etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el Thu Feb 12 12:35:45 2009 -0800
+++ b/etc/isar-keywords-ZF.el Fri Feb 13 07:53:38 2009 +1100
@@ -73,6 +73,7 @@
"extract_type"
"finalconsts"
"finally"
+ "find_consts"
"find_theorems"
"fix"
"from"
@@ -280,6 +281,7 @@
"disable_pr"
"display_drafts"
"enable_pr"
+ "find_consts"
"find_theorems"
"full_prf"
"header"
diff -r 58f3c48dbbb7 -r 29154e67731d etc/isar-keywords.el
--- a/etc/isar-keywords.el Thu Feb 12 12:35:45 2009 -0800
+++ b/etc/isar-keywords.el Fri Feb 13 07:53:38 2009 +1100
@@ -95,6 +95,7 @@
"extract_type"
"finalconsts"
"finally"
+ "find_consts"
"find_theorems"
"fix"
"fixpat"
@@ -346,6 +347,7 @@
"display_drafts"
"enable_pr"
"export_code"
+ "find_consts"
"find_theorems"
"full_prf"
"header"
diff -r 58f3c48dbbb7 -r 29154e67731d lib/jedit/isabelle.xml
--- a/lib/jedit/isabelle.xml Thu Feb 12 12:35:45 2009 -0800
+++ b/lib/jedit/isabelle.xml Fri Feb 13 07:53:38 2009 +1100
@@ -135,6 +135,7 @@
file
finalconsts
finally
+
fix
fixes
diff -r 58f3c48dbbb7 -r 29154e67731d src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile Thu Feb 12 12:35:45 2009 -0800
+++ b/src/Pure/IsaMakefile Fri Feb 13 07:53:38 2009 +1100
@@ -38,10 +38,10 @@
Isar/attrib.ML Isar/auto_bind.ML Isar/calculation.ML Isar/class.ML \
Isar/class_target.ML Isar/code.ML Isar/code_unit.ML \
Isar/constdefs.ML Isar/context_rules.ML Isar/element.ML \
- Isar/expression.ML Isar/find_theorems.ML Isar/isar.ML \
- Isar/isar_document.ML Isar/isar_cmd.ML Isar/isar_syn.ML \
+ Isar/expression.ML Isar/find_theorems.ML Isar/find_consts.ML \
+ Isar/isar.ML Isar/isar_document.ML Isar/isar_cmd.ML Isar/isar_syn.ML \
Isar/local_defs.ML Isar/local_syntax.ML Isar/local_theory.ML \
- Isar/locale.ML Isar/method.ML Isar/net_rules.ML \
+ Isar/locale.ML Isar/method.ML Isar/net_rules.ML \
Isar/object_logic.ML Isar/obtain.ML Isar/outer_keyword.ML \
Isar/outer_lex.ML Isar/outer_parse.ML Isar/outer_syntax.ML \
Isar/overloading.ML Isar/proof.ML Isar/proof_context.ML \
diff -r 58f3c48dbbb7 -r 29154e67731d src/Pure/Isar/ROOT.ML
--- a/src/Pure/Isar/ROOT.ML Thu Feb 12 12:35:45 2009 -0800
+++ b/src/Pure/Isar/ROOT.ML Fri Feb 13 07:53:38 2009 +1100
@@ -90,5 +90,6 @@
use "rule_insts.ML";
use "../Thy/thm_deps.ML";
use "find_theorems.ML";
+use "find_consts.ML";
use "isar_cmd.ML";
use "isar_syn.ML";
diff -r 58f3c48dbbb7 -r 29154e67731d src/Pure/Isar/find_theorems.ML
--- a/src/Pure/Isar/find_theorems.ML Thu Feb 12 12:35:45 2009 -0800
+++ b/src/Pure/Isar/find_theorems.ML Fri Feb 13 07:53:38 2009 +1100
@@ -103,21 +103,10 @@
(* filter_name *)
-fun match_string pat str =
- let
- fun match [] _ = true
- | match (p :: ps) s =
- size p <= size s andalso
- (case try (unprefix p) s of
- SOME s' => match ps s'
- | NONE => match (p :: ps) (String.substring (s, 1, size s - 1)));
- in match (space_explode "*" pat) str end;
-
fun filter_name str_pat (thmref, _) =
if match_string str_pat (Facts.name_of_ref thmref)
then SOME (0, 0) else NONE;
-
(* filter intro/elim/dest/solves rules *)
fun filter_dest ctxt goal (_, thm) =
diff -r 58f3c48dbbb7 -r 29154e67731d src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML Thu Feb 12 12:35:45 2009 -0800
+++ b/src/Pure/Isar/isar_cmd.ML Fri Feb 13 07:53:38 2009 +1100
@@ -64,6 +64,8 @@
val thm_deps: (Facts.ref * Attrib.src list) list -> Toplevel.transition -> Toplevel.transition
val find_theorems: (int option * bool) * (bool * string FindTheorems.criterion) list
-> Toplevel.transition -> Toplevel.transition
+ val find_consts: (bool * FindConsts.criterion) list ->
+ Toplevel.transition -> Toplevel.transition
val unused_thms: (string list * string list option) option ->
Toplevel.transition -> Toplevel.transition
val print_binds: Toplevel.transition -> Toplevel.transition
@@ -432,6 +434,12 @@
|> map pretty_thm |> Pretty.chunks |> Pretty.writeln
end);
+(* retrieve constants *)
+
+fun find_consts spec =
+ Toplevel.unknown_theory o Toplevel.keep (fn state =>
+ let val ctxt = (Proof.context_of o Toplevel.enter_proof_body) state
+ in FindConsts.find_consts ctxt spec end);
(* print proof context contents *)
diff -r 58f3c48dbbb7 -r 29154e67731d src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML Thu Feb 12 12:35:45 2009 -0800
+++ b/src/Pure/Isar/isar_syn.ML Fri Feb 13 07:53:38 2009 +1100
@@ -878,6 +878,22 @@
end;
+local
+
+val criterion =
+ P.reserved "strict" |-- P.!!! (P.$$$ ":" |-- P.xname) >> FindConsts.Strict ||
+ P.reserved "name" |-- P.!!! (P.$$$ ":" |-- P.xname) >> FindConsts.Name ||
+ P.xname >> FindConsts.Loose;
+
+in
+
+val _ =
+ OuterSyntax.improper_command "find_consts" "search constants by type pattern"
+ K.diag (Scan.repeat (((Scan.option P.minus >> is_none) -- criterion))
+ >> (Toplevel.no_timing oo IsarCmd.find_consts));
+
+end;
+
val _ =
OuterSyntax.improper_command "print_binds" "print term bindings of proof context" K.diag
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_binds));
diff -r 58f3c48dbbb7 -r 29154e67731d src/Pure/library.ML
--- a/src/Pure/library.ML Thu Feb 12 12:35:45 2009 -0800
+++ b/src/Pure/library.ML Fri Feb 13 07:53:38 2009 +1100
@@ -159,6 +159,7 @@
val replicate_string: int -> string -> string
val translate_string: (string -> string) -> string -> string
val multiply: 'a list -> 'a list list -> 'a list list
+ val match_string: string -> string -> bool
(*lists as sets -- see also Pure/General/ord_list.ML*)
val member: ('b * 'a -> bool) -> 'a list -> 'b -> bool
@@ -554,7 +555,6 @@
fun multiply [] _ = []
| multiply (x :: xs) yss = map (cons x) yss @ multiply xs yss;
-
(* direct product *)
fun map_product f _ [] = []
@@ -787,7 +787,16 @@
if k mod 2 = 0 then replicate_string (k div 2) (a ^ a)
else replicate_string (k div 2) (a ^ a) ^ a;
-
+(*crude matching of str against simple glob pat*)
+fun match_string pat str =
+ let
+ fun match [] _ = true
+ | match (p :: ps) s =
+ size p <= size s andalso
+ (case try (unprefix p) s of
+ SOME s' => match ps s'
+ | NONE => match (p :: ps) (String.substring (s, 1, size s - 1)));
+ in match (space_explode "*" pat) str end;
(** lists as sets -- see also Pure/General/ord_list.ML **)
diff -r 58f3c48dbbb7 -r 29154e67731d src/Pure/term.ML
--- a/src/Pure/term.ML Thu Feb 12 12:35:45 2009 -0800
+++ b/src/Pure/term.ML Fri Feb 13 07:53:38 2009 +1100
@@ -64,6 +64,7 @@
val strip_comb: term -> term * term list
val head_of: term -> term
val size_of_term: term -> int
+ val size_of_typ: typ -> int
val map_atyps: (typ -> typ) -> typ -> typ
val map_aterms: (term -> term) -> term -> term
val map_type_tvar: (indexname * sort -> typ) -> typ -> typ
@@ -391,6 +392,13 @@
| add_size (_, n) = n + 1;
in add_size (tm, 0) end;
+(*number of tfrees, tvars, and constructors in a type*)
+fun size_of_typ ty =
+ let
+ fun add_size (Type (_, ars), n) = foldl add_size (n + 1) ars
+ | add_size (_, n) = n + 1;
+ in add_size (ty, 0) end;
+
fun map_atyps f (Type (a, Ts)) = Type (a, map (map_atyps f) Ts)
| map_atyps f T = f T;