really honor pattern depth, and use 2 by default
authorblanchet
Mon Dec 17 22:06:28 2012 +0100 (2012-12-17)
changeset 50583681edd111e9b
parent 50582 001a0e12d7f1
child 50584 4fff0898cc0e
really honor pattern depth, and use 2 by default
src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Dec 17 22:06:28 2012 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Dec 17 22:06:28 2012 +0100
     1.3 @@ -542,7 +542,7 @@
     1.4        | do_add_type (TFree (_, S)) = add_classes S
     1.5        | do_add_type (TVar (_, S)) = add_classes S
     1.6      fun add_type T = type_max_depth >= 0 ? do_add_type T
     1.7 -    fun patternify_term _ ~1 _ = []
     1.8 +    fun patternify_term _ 0 _ = []
     1.9        | patternify_term args _ (Const (x as (s, _))) =
    1.10          if is_bad_const x args then [] else [s]
    1.11        | patternify_term _ depth (Free (s, _)) =
    1.12 @@ -550,7 +550,6 @@
    1.13            [thy_name ^ Long_Name.separator ^ s]
    1.14          else
    1.15            []
    1.16 -      | patternify_term _ 0 _ = []
    1.17        | patternify_term args depth (t $ u) =
    1.18          let
    1.19            val ps = patternify_term (u :: args) depth t
    1.20 @@ -559,7 +558,7 @@
    1.21        | patternify_term _ _ _ = []
    1.22      fun add_term_pattern feature_of =
    1.23        union (op = o pairself fst) o map feature_of oo patternify_term []
    1.24 -    fun add_term_patterns _ ~1 _ = I
    1.25 +    fun add_term_patterns _ 0 _ = I
    1.26        | add_term_patterns feature_of depth t =
    1.27          add_term_pattern feature_of depth t
    1.28          #> add_term_patterns feature_of (depth - 1) t
    1.29 @@ -578,8 +577,8 @@
    1.30  
    1.31  fun is_exists (s, _) = (s = @{const_name Ex} orelse s = @{const_name Ex1})
    1.32  
    1.33 -val term_max_depth = 1
    1.34 -val type_max_depth = 1
    1.35 +val term_max_depth = 2
    1.36 +val type_max_depth = 2
    1.37  
    1.38  (* TODO: Generate type classes for types? *)
    1.39  fun features_of ctxt prover thy (scope, status) ts =