added generalize/instantiate_option;
authorwenzelm
Tue Jul 04 19:49:52 2006 +0200 (2006-07-04)
changeset 20001392e39bd1811
parent 20000 2fa767ab91aa
child 20002 09ac655904a9
added generalize/instantiate_option;
src/Pure/term.ML
     1.1 --- a/src/Pure/term.ML	Tue Jul 04 19:49:51 2006 +0200
     1.2 +++ b/src/Pure/term.ML	Tue Jul 04 19:49:52 2006 +0200
     1.3 @@ -192,9 +192,14 @@
     1.4    val dest_skolem: string -> string
     1.5    val generalize: string list * string list -> int -> term -> term
     1.6    val generalizeT: string list -> int -> typ -> typ
     1.7 +  val generalize_option: string list * string list -> int -> term -> term option
     1.8 +  val generalizeT_option: string list -> int -> typ -> typ option
     1.9    val instantiate: ((indexname * sort) * typ) list * ((indexname * typ) * term) list
    1.10      -> term -> term
    1.11    val instantiateT: ((indexname * sort) * typ) list -> typ -> typ
    1.12 +  val instantiate_option: ((indexname * sort) * typ) list * ((indexname * typ) * term) list
    1.13 +    -> term -> term option
    1.14 +  val instantiateT_option: ((indexname * sort) * typ) list -> typ -> typ option
    1.15    val maxidx_typ: typ -> int -> int
    1.16    val maxidx_typs: typ list -> int -> int
    1.17    val maxidx_term: term -> int -> int
    1.18 @@ -1008,8 +1013,8 @@
    1.19            | gen_typs [] = raise SAME;
    1.20        in gen_typ ty end;
    1.21  
    1.22 -fun generalize ([], []) _ tm = tm
    1.23 -  | generalize (tfrees, frees) idx tm =
    1.24 +fun generalize_same ([], []) _ _ = raise SAME
    1.25 +  | generalize_same (tfrees, frees) idx tm =
    1.26        let
    1.27          fun var ((x, i), T) =
    1.28            (case try dest_internal x of
    1.29 @@ -1027,10 +1032,13 @@
    1.30                (Abs (x, genT T, gen t handle SAME => t)
    1.31                  handle SAME => Abs (x, T, gen t))
    1.32            | gen (t $ u) = (gen t $ (gen u handle SAME => u) handle SAME => t $ gen u);
    1.33 -      in gen tm handle SAME => tm end;
    1.34 +      in gen tm end;
    1.35  
    1.36 -fun generalizeT tfrees i ty =
    1.37 -  generalizeT_same tfrees i ty handle SAME => ty;
    1.38 +fun generalize names i tm = generalize_same names i tm handle SAME => tm;
    1.39 +fun generalizeT names i ty = generalizeT_same names i ty handle SAME => ty;
    1.40 +
    1.41 +fun generalize_option names i tm = SOME (generalize_same names i tm) handle SAME => NONE;
    1.42 +fun generalizeT_option names i ty = SOME (generalizeT_same names i ty) handle SAME => NONE;
    1.43  
    1.44  end;
    1.45  
    1.46 @@ -1054,8 +1062,8 @@
    1.47            | subst_typs [] = raise SAME;
    1.48        in subst_typ ty end;
    1.49  
    1.50 -fun instantiate ([], []) tm = tm
    1.51 -  | instantiate (instT, inst) tm =
    1.52 +fun instantiate_same ([], []) _ = raise SAME
    1.53 +  | instantiate_same (instT, inst) tm =
    1.54        let
    1.55          val substT = instantiateT_same instT;
    1.56          fun subst (Const (c, T)) = Const (c, substT T)
    1.57 @@ -1071,10 +1079,13 @@
    1.58                (Abs (x, substT T, subst t handle SAME => t)
    1.59                  handle SAME => Abs (x, T, subst t))
    1.60            | subst (t $ u) = (subst t $ (subst u handle SAME => u) handle SAME => t $ subst u);
    1.61 -      in subst tm handle SAME => tm end;
    1.62 +      in subst tm end;
    1.63  
    1.64 -fun instantiateT instT ty =
    1.65 -  instantiateT_same instT ty handle SAME => ty;
    1.66 +fun instantiate insts tm = instantiate_same insts tm handle SAME => tm;
    1.67 +fun instantiateT insts ty = instantiateT_same insts ty handle SAME => ty;
    1.68 +
    1.69 +fun instantiate_option insts tm = SOME (instantiate_same insts tm) handle SAME => NONE;
    1.70 +fun instantiateT_option insts ty = SOME (instantiateT_same insts ty) handle SAME => NONE;
    1.71  
    1.72  end;
    1.73