observe basic Isabelle/ML coding conventions;
authorwenzelm
Fri Feb 27 16:05:40 2009 +0100 (2009-02-27)
changeset 3014398a986b02022
parent 30142 8d6145694bb5
child 30144 56ae4893e8ae
child 30155 f65dc19cd5f0
child 30191 e3e3d28fe5bc
observe basic Isabelle/ML coding conventions;
src/Pure/Tools/find_consts.ML
src/Pure/Tools/find_theorems.ML
     1.1 --- a/src/Pure/Tools/find_consts.ML	Fri Feb 27 15:46:22 2009 +0100
     1.2 +++ b/src/Pure/Tools/find_consts.ML	Fri Feb 27 16:05:40 2009 +0100
     1.3 @@ -1,15 +1,16 @@
     1.4 -(*  Title:      find_consts.ML
     1.5 +(*  Title:      Pure/Tools/find_consts.ML
     1.6      Author:     Timothy Bourke and Gerwin Klein, NICTA
     1.7  
     1.8 -  Hoogle-like (http://www-users.cs.york.ac.uk/~ndm/hoogle) searching by type
     1.9 -  over constants, but matching is not fuzzy
    1.10 +Hoogle-like (http://www-users.cs.york.ac.uk/~ndm/hoogle) searching by
    1.11 +type over constants, but matching is not fuzzy.
    1.12  *)
    1.13  
    1.14  signature FIND_CONSTS =
    1.15  sig
    1.16 -  datatype criterion = Strict of string
    1.17 -                     | Loose of string
    1.18 -                     | Name of string
    1.19 +  datatype criterion =
    1.20 +      Strict of string
    1.21 +    | Loose of string
    1.22 +    | Name of string
    1.23  
    1.24    val default_criteria : (bool * criterion) list ref
    1.25  
    1.26 @@ -19,34 +20,46 @@
    1.27  structure FindConsts : FIND_CONSTS =
    1.28  struct
    1.29  
    1.30 -datatype criterion = Strict of string
    1.31 -                   | Loose of string
    1.32 -                   | Name of string;
    1.33 +(* search criteria *)
    1.34 +
    1.35 +datatype criterion =
    1.36 +    Strict of string
    1.37 +  | Loose of string
    1.38 +  | Name of string;
    1.39  
    1.40  val default_criteria = ref [(false, Name ".sko_")];
    1.41  
    1.42 -fun add_tye (_, (_, t)) n = size_of_typ t + n;
    1.43 +
    1.44 +(* matching types/consts *)
    1.45  
    1.46 -fun matches_subtype thy typat = let
    1.47 +fun add_tye (_, (_, t)) n = Term.size_of_typ t + n;
    1.48 +
    1.49 +fun matches_subtype thy typat =
    1.50 +  let
    1.51      val p = can (fn ty => Sign.typ_match thy (typat, ty) Vartab.empty);
    1.52  
    1.53      fun fs [] = false
    1.54 -      | fs (t::ts) = f t orelse fs ts
    1.55 +      | fs (t :: ts) = f t orelse fs ts
    1.56  
    1.57      and f (t as Type (_, ars)) = p t orelse fs ars
    1.58        | f t = p t;
    1.59    in f end;
    1.60  
    1.61 -fun check_const p (nm, (ty, _)) = if p (nm, ty)
    1.62 -                                  then SOME (size_of_typ ty)
    1.63 -                                  else NONE;
    1.64 +fun check_const p (nm, (ty, _)) =
    1.65 +  if p (nm, ty)
    1.66 +  then SOME (Term.size_of_typ ty)
    1.67 +  else NONE;
    1.68  
    1.69 -fun opt_not f (c as (_, (ty, _))) = if is_some (f c)
    1.70 -                                    then NONE else SOME (size_of_typ ty);
    1.71 +fun opt_not f (c as (_, (ty, _))) =
    1.72 +  if is_some (f c)
    1.73 +  then NONE else SOME (Term.size_of_typ ty);
    1.74  
    1.75  fun filter_const (_, NONE) = NONE
    1.76 -  | filter_const (f, (SOME (c, r))) = Option.map
    1.77 -                                        (pair c o ((curry Int.min) r)) (f c);
    1.78 +  | filter_const (f, (SOME (c, r))) =
    1.79 +      Option.map (pair c o (curry Int.min r)) (f c);
    1.80 +
    1.81 +
    1.82 +(* pretty results *)
    1.83  
    1.84  fun pretty_criterion (b, c) =
    1.85    let
    1.86 @@ -58,26 +71,32 @@
    1.87      | Name name => Pretty.str (prfx "name: " ^ quote name))
    1.88    end;
    1.89  
    1.90 -fun pretty_const ctxt (nm, ty) = let
    1.91 +fun pretty_const ctxt (nm, ty) =
    1.92 +  let
    1.93      val ty' = Logic.unvarifyT ty;
    1.94    in
    1.95 -    Pretty.block [Pretty.quote (Pretty.str nm), Pretty.fbrk,
    1.96 -                  Pretty.str "::", Pretty.brk 1,
    1.97 -                  Pretty.quote (Syntax.pretty_typ ctxt ty')]
    1.98 +    Pretty.block
    1.99 +     [Pretty.quote (Pretty.str nm), Pretty.fbrk,
   1.100 +      Pretty.str "::", Pretty.brk 1,
   1.101 +      Pretty.quote (Syntax.pretty_typ ctxt ty')]
   1.102    end;
   1.103  
   1.104 -fun find_consts ctxt raw_criteria = let
   1.105 +
   1.106 +(* find_consts *)
   1.107 +
   1.108 +fun find_consts ctxt raw_criteria =
   1.109 +  let
   1.110      val start = start_timing ();
   1.111  
   1.112      val thy = ProofContext.theory_of ctxt;
   1.113      val low_ranking = 10000;
   1.114  
   1.115 -    fun make_pattern crit = ProofContext.read_term_pattern ctxt ("_::" ^ crit)
   1.116 -                            |> type_of;
   1.117 +    fun make_pattern crit = ProofContext.read_term_pattern ctxt ("_::" ^ crit) |> Term.type_of;
   1.118  
   1.119      fun make_match (Strict arg) =
   1.120            let val qty = make_pattern arg; in
   1.121 -            fn (_, (ty, _)) => let
   1.122 +            fn (_, (ty, _)) =>
   1.123 +              let
   1.124                  val tye = Sign.typ_match thy (qty, ty) Vartab.empty;
   1.125                  val sub_size = Vartab.fold add_tye tye 0;
   1.126                in SOME sub_size end handle MATCH => NONE
   1.127 @@ -89,15 +108,16 @@
   1.128        | make_match (Name arg) = check_const (match_string arg o fst);
   1.129  
   1.130      fun make_criterion (b, crit) = (if b then I else opt_not) (make_match crit);
   1.131 -    val criteria = map make_criterion ((!default_criteria) @ raw_criteria);
   1.132 +    val criteria = map make_criterion (! default_criteria @ raw_criteria);
   1.133  
   1.134      val (_, consts) = (#constants o Consts.dest o Sign.consts_of) thy;
   1.135      fun eval_entry c = foldl filter_const (SOME (c, low_ranking)) criteria;
   1.136  
   1.137 -    val matches = Symtab.fold (cons o eval_entry) consts []
   1.138 -                  |> map_filter I
   1.139 -                  |> sort (rev_order o int_ord o pairself snd)
   1.140 -                  |> map ((apsnd fst) o fst);
   1.141 +    val matches =
   1.142 +      Symtab.fold (cons o eval_entry) consts []
   1.143 +      |> map_filter I
   1.144 +      |> sort (rev_order o int_ord o pairself snd)
   1.145 +      |> map ((apsnd fst) o fst);
   1.146  
   1.147      val end_msg = " in " ^
   1.148                    (List.nth (String.tokens Char.isSpace (end_timing start), 3))
   1.149 @@ -114,11 +134,10 @@
   1.150        :: map (pretty_const ctxt) matches
   1.151      |> Pretty.chunks
   1.152      |> Pretty.writeln
   1.153 -  end handle ERROR s => Output.error_msg s
   1.154 +  end handle ERROR s => Output.error_msg s;
   1.155  
   1.156  
   1.157 -
   1.158 -(** command syntax **)
   1.159 +(* command syntax *)
   1.160  
   1.161  fun find_consts_cmd spec =
   1.162    Toplevel.unknown_theory o Toplevel.keep (fn state =>
     2.1 --- a/src/Pure/Tools/find_theorems.ML	Fri Feb 27 15:46:22 2009 +0100
     2.2 +++ b/src/Pure/Tools/find_theorems.ML	Fri Feb 27 16:05:40 2009 +0100
     2.3 @@ -1,4 +1,4 @@
     2.4 -(*  Title:      Pure/Isar/find_theorems.ML
     2.5 +(*  Title:      Pure/Tools/find_theorems.ML
     2.6      Author:     Rafal Kolanski and Gerwin Klein, NICTA
     2.7  
     2.8  Retrieve theorems from proof context.
     2.9 @@ -163,17 +163,20 @@
    2.10  
    2.11  val tac_limit = ref 5;
    2.12  
    2.13 -fun filter_solves ctxt goal = let
    2.14 -    val baregoal = Logic.get_goal (prop_of goal) 1;
    2.15 +fun filter_solves ctxt goal =
    2.16 +  let
    2.17 +    val baregoal = Logic.get_goal (Thm.prop_of goal) 1;
    2.18  
    2.19 -    fun etacn thm i = Seq.take (!tac_limit) o etac thm i;
    2.20 -    fun try_thm thm = if Thm.no_prems thm then rtac thm 1 goal
    2.21 -                      else (etacn thm THEN_ALL_NEW
    2.22 -                             (Goal.norm_hhf_tac THEN'
    2.23 -                               Method.assumption_tac ctxt)) 1 goal;
    2.24 +    fun etacn thm i = Seq.take (! tac_limit) o etac thm i;
    2.25 +    fun try_thm thm =
    2.26 +      if Thm.no_prems thm then rtac thm 1 goal
    2.27 +      else (etacn thm THEN_ALL_NEW
    2.28 +             (Goal.norm_hhf_tac THEN'
    2.29 +               Method.assumption_tac ctxt)) 1 goal;
    2.30    in
    2.31 -    fn (_, thm) => if (is_some o Seq.pull o try_thm) thm
    2.32 -                   then SOME (Thm.nprems_of thm, 0) else NONE
    2.33 +    fn (_, thm) =>
    2.34 +      if (is_some o Seq.pull o try_thm) thm
    2.35 +      then SOME (Thm.nprems_of thm, 0) else NONE
    2.36    end;
    2.37  
    2.38  
    2.39 @@ -195,18 +198,20 @@
    2.40  
    2.41  fun get_names t = (Term.add_const_names t []) union (Term.add_free_names t []);
    2.42  fun get_thm_names (_, thm) = get_names (Thm.full_prop_of thm);
    2.43 -  (* Including all constants and frees is only sound because
    2.44 -     matching uses higher-order patterns. If full matching
    2.45 -     were used, then constants that may be subject to
    2.46 -     beta-reduction after substitution of frees should
    2.47 -     not be included for LHS set because they could be
    2.48 -     thrown away by the substituted function.
    2.49 -     e.g. for (?F 1 2) do not include 1 or 2, if it were
    2.50 -          possible for ?F to be (% x y. 3)
    2.51 -     The largest possible set should always be included on
    2.52 -     the RHS. *)
    2.53  
    2.54 -fun filter_pattern ctxt pat = let
    2.55 +(*Including all constants and frees is only sound because
    2.56 +  matching uses higher-order patterns. If full matching
    2.57 +  were used, then constants that may be subject to
    2.58 +  beta-reduction after substitution of frees should
    2.59 +  not be included for LHS set because they could be
    2.60 +  thrown away by the substituted function.
    2.61 +  e.g. for (?F 1 2) do not include 1 or 2, if it were
    2.62 +       possible for ?F to be (% x y. 3)
    2.63 +  The largest possible set should always be included on
    2.64 +  the RHS.*)
    2.65 +
    2.66 +fun filter_pattern ctxt pat =
    2.67 +  let
    2.68      val pat_consts = get_names pat;
    2.69  
    2.70      fun check (t, NONE) = check (t, SOME (get_thm_names t))
    2.71 @@ -233,12 +238,9 @@
    2.72    | filter_crit _ NONE Elim = err_no_goal "elim"
    2.73    | filter_crit _ NONE Dest = err_no_goal "dest"
    2.74    | filter_crit _ NONE Solves = err_no_goal "solves"
    2.75 -  | filter_crit ctxt (SOME goal) Intro = apfst (filter_intro ctxt
    2.76 -                                                  (fix_goal goal))
    2.77 -  | filter_crit ctxt (SOME goal) Elim = apfst (filter_elim ctxt 
    2.78 -                                                  (fix_goal goal))
    2.79 -  | filter_crit ctxt (SOME goal) Dest = apfst (filter_dest ctxt
    2.80 -                                                  (fix_goal goal))
    2.81 +  | filter_crit ctxt (SOME goal) Intro = apfst (filter_intro ctxt (fix_goal goal))
    2.82 +  | filter_crit ctxt (SOME goal) Elim = apfst (filter_elim ctxt (fix_goal goal))
    2.83 +  | filter_crit ctxt (SOME goal) Dest = apfst (filter_dest ctxt (fix_goal goal))
    2.84    | filter_crit ctxt (SOME goal) Solves = apfst (filter_solves ctxt goal)
    2.85    | filter_crit ctxt _ (Simp pat) = apfst (filter_simp ctxt pat)
    2.86    | filter_crit ctxt _ (Pattern pat) = filter_pattern ctxt pat;
    2.87 @@ -248,11 +250,13 @@
    2.88  fun opt_add (SOME (a, x)) (SOME (b, y)) = SOME (Int.max (a, b), x + y : int)
    2.89    | opt_add _ _ = NONE;
    2.90  
    2.91 -fun app_filters thm = let
    2.92 +fun app_filters thm =
    2.93 +  let
    2.94      fun app (NONE, _, _) = NONE
    2.95        | app (SOME v, consts, []) = SOME (v, thm)
    2.96 -      | app (r, consts, f::fs) = let val (r', consts') = f (thm, consts)
    2.97 -                                 in app (opt_add r r', consts', fs) end;
    2.98 +      | app (r, consts, f :: fs) =
    2.99 +          let val (r', consts') = f (thm, consts)
   2.100 +          in app (opt_add r r', consts', fs) end;
   2.101    in app end;
   2.102  
   2.103  in
   2.104 @@ -302,7 +306,8 @@
   2.105  
   2.106  in
   2.107  
   2.108 -fun nicer_shortest ctxt = let
   2.109 +fun nicer_shortest ctxt =
   2.110 +  let
   2.111      val ns = ProofContext.theory_of ctxt
   2.112               |> PureThy.facts_of
   2.113               |> Facts.space_of;
   2.114 @@ -354,7 +359,8 @@
   2.115        else raw_matches;
   2.116    in matches end;
   2.117  
   2.118 -fun print_theorems ctxt opt_goal opt_limit rem_dups raw_criteria = let
   2.119 +fun print_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
   2.120 +  let
   2.121      val start = start_timing ();
   2.122  
   2.123      val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;