less hermetic ML;
authorwenzelm
Thu Oct 29 11:56:02 2009 +0100 (2009-10-29)
changeset 333011fe9fc908ec3
parent 33300 939ca97f5a11
child 33302 a2fa94305254
less hermetic ML;
parse_pattern: apply Consts.intern only once (Why is this done anyway?);
modernized structure names;
src/Pure/Tools/find_consts.ML
src/Pure/Tools/find_theorems.ML
src/Tools/auto_solve.ML
     1.1 --- a/src/Pure/Tools/find_consts.ML	Thu Oct 29 11:26:47 2009 +0100
     1.2 +++ b/src/Pure/Tools/find_consts.ML	Thu Oct 29 11:56:02 2009 +0100
     1.3 @@ -11,11 +11,10 @@
     1.4        Strict of string
     1.5      | Loose of string
     1.6      | Name of string
     1.7 -
     1.8    val find_consts : Proof.context -> (bool * criterion) list -> unit
     1.9  end;
    1.10  
    1.11 -structure FindConsts : FIND_CONSTS =
    1.12 +structure Find_Consts : FIND_CONSTS =
    1.13  struct
    1.14  
    1.15  (* search criteria *)
    1.16 @@ -162,7 +161,7 @@
    1.17  
    1.18  val _ =
    1.19    OuterSyntax.improper_command "find_consts" "search constants by type pattern" K.diag
    1.20 -    (Scan.repeat (((Scan.option P.minus >> is_none) -- criterion))
    1.21 +    (Scan.repeat ((Scan.option P.minus >> is_none) -- criterion)
    1.22        >> (Toplevel.no_timing oo find_consts_cmd));
    1.23  
    1.24  end;
     2.1 --- a/src/Pure/Tools/find_theorems.ML	Thu Oct 29 11:26:47 2009 +0100
     2.2 +++ b/src/Pure/Tools/find_theorems.ML	Thu Oct 29 11:56:02 2009 +0100
     2.3 @@ -18,7 +18,7 @@
     2.4      (bool * string criterion) list -> unit
     2.5  end;
     2.6  
     2.7 -structure FindTheorems: FIND_THEOREMS =
     2.8 +structure Find_Theorems: FIND_THEOREMS =
     2.9  struct
    2.10  
    2.11  (** search criteria **)
    2.12 @@ -28,24 +28,22 @@
    2.13    Pattern of 'term;
    2.14  
    2.15  fun apply_dummies tm =
    2.16 -  strip_abs tm
    2.17 -  |> fst
    2.18 -  |> map (Term.dummy_pattern o snd)
    2.19 -  |> betapplys o pair tm
    2.20 -  |> (fn x => Term.replace_dummy_patterns x 1)
    2.21 -  |> fst;
    2.22 +  let
    2.23 +    val (xs, _) = Term.strip_abs tm;
    2.24 +    val tm' = Term.betapplys (tm, map (Term.dummy_pattern o #2) xs);
    2.25 +  in #1 (Term.replace_dummy_patterns tm' 1) end;
    2.26  
    2.27  fun parse_pattern ctxt nm =
    2.28    let
    2.29 -    val nm' = case Syntax.parse_term ctxt nm of Const (n, _) => n | _ => nm;
    2.30      val consts = ProofContext.consts_of ctxt;
    2.31 +    val nm' =
    2.32 +      (case Syntax.parse_term ctxt nm of
    2.33 +        Const (c, _) => c
    2.34 +      | _ => Consts.intern consts nm);
    2.35    in
    2.36 -    nm'
    2.37 -    |> Consts.intern consts
    2.38 -    |> Consts.the_abbreviation consts
    2.39 -    |> snd
    2.40 -    |> apply_dummies
    2.41 -    handle TYPE _ => ProofContext.read_term_pattern ctxt nm
    2.42 +    (case try (Consts.the_abbreviation consts) nm' of
    2.43 +      SOME (_, rhs) => apply_dummies rhs
    2.44 +    | NONE => ProofContext.read_term_pattern ctxt nm)
    2.45    end;
    2.46  
    2.47  fun read_criterion _ (Name name) = Name name
     3.1 --- a/src/Tools/auto_solve.ML	Thu Oct 29 11:26:47 2009 +0100
     3.2 +++ b/src/Tools/auto_solve.ML	Thu Oct 29 11:56:02 2009 +0100
     3.3 @@ -5,7 +5,7 @@
     3.4  existing theorem.  Duplicate lemmas can be detected in this way.
     3.5  
     3.6  The implementation is based in part on Berghofer and Haftmann's
     3.7 -quickcheck.ML.  It relies critically on the FindTheorems solves
     3.8 +quickcheck.ML.  It relies critically on the Find_Theorems solves
     3.9  feature.
    3.10  *)
    3.11  
    3.12 @@ -45,8 +45,8 @@
    3.13    let
    3.14      val ctxt = Proof.context_of state;
    3.15  
    3.16 -    val crits = [(true, FindTheorems.Solves)];
    3.17 -    fun find g = snd (FindTheorems.find_theorems ctxt (SOME g) (SOME (! limit)) false crits);
    3.18 +    val crits = [(true, Find_Theorems.Solves)];
    3.19 +    fun find g = snd (Find_Theorems.find_theorems ctxt (SOME g) (SOME (! limit)) false crits);
    3.20  
    3.21      fun prt_result (goal, results) =
    3.22        let
    3.23 @@ -57,7 +57,7 @@
    3.24        in
    3.25          Pretty.big_list
    3.26            (msg ^ " could be solved directly with:")
    3.27 -          (map (FindTheorems.pretty_thm ctxt) results)
    3.28 +          (map (Find_Theorems.pretty_thm ctxt) results)
    3.29        end;
    3.30  
    3.31      fun seek_against_goal () =