src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
changeset 36555 8ff45c2076da
parent 36496 8b2dc9b4bf4c
child 36960 01594f816e3a
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Thu Apr 29 01:11:06 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Thu Apr 29 01:17:14 2010 +0200
     1.3 @@ -18,6 +18,8 @@
     1.4    val nat_subscript : int -> string
     1.5    val unyxml : string -> string
     1.6    val maybe_quote : string -> string
     1.7 +  val monomorphic_term : Type.tyenv -> term -> term
     1.8 +  val specialize_type : theory -> (string * typ) -> term -> term
     1.9  end;
    1.10   
    1.11  structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
    1.12 @@ -103,4 +105,30 @@
    1.13             OuterKeyword.is_keyword s) ? quote
    1.14    end
    1.15  
    1.16 +fun monomorphic_term subst t =
    1.17 +  map_types (map_type_tvar (fn v =>
    1.18 +      case Type.lookup subst v of
    1.19 +        SOME typ => typ
    1.20 +      | NONE => raise TERM ("monomorphic_term: uninstanitated schematic type \
    1.21 +                            \variable", [t]))) t
    1.22 +
    1.23 +fun specialize_type thy (s, T) t =
    1.24 +  let
    1.25 +    fun subst_for (Const (s', T')) =
    1.26 +      if s = s' then
    1.27 +        SOME (Sign.typ_match thy (T', T) Vartab.empty)
    1.28 +        handle Type.TYPE_MATCH => NONE
    1.29 +      else
    1.30 +        NONE
    1.31 +    | subst_for (t1 $ t2) =
    1.32 +      (case subst_for t1 of SOME x => SOME x | NONE => subst_for t2)
    1.33 +    | subst_for (Abs (_, _, t')) = subst_for t'
    1.34 +    | subst_for _ = NONE
    1.35 +  in
    1.36 +    case subst_for t of
    1.37 +      SOME subst => monomorphic_term subst t
    1.38 +    | NONE => raise Type.TYPE_MATCH
    1.39 +  end
    1.40 +
    1.41 +
    1.42  end;