added expand_term;
authorwenzelm
Thu Dec 07 17:58:45 2006 +0100 (2006-12-07)
changeset 216956c07cc87fe2b
parent 21694 9f65fecb6e10
child 21696 f3c78a133fbb
added expand_term;
src/Pure/envir.ML
     1.1 --- a/src/Pure/envir.ML	Thu Dec 07 17:58:44 2006 +0100
     1.2 +++ b/src/Pure/envir.ML	Thu Dec 07 17:58:45 2006 +0100
     1.3 @@ -39,6 +39,7 @@
     1.4    val subst_Vars: tenv -> term -> term
     1.5    val subst_vars: Type.tyenv * tenv -> term -> term
     1.6    val expand_atom: typ -> typ * term -> term
     1.7 +  val expand_term: (term -> (typ * term) option) -> term -> term
     1.8  end;
     1.9  
    1.10  structure Envir : ENVIR =
    1.11 @@ -295,10 +296,28 @@
    1.12    in subst end;
    1.13  
    1.14  
    1.15 -(* expand_atom *)
    1.16 +(* expand defined atoms *)
    1.17  
    1.18  fun expand_atom T (U, u) =
    1.19    subst_TVars (Type.raw_match (U, T) Vartab.empty) u
    1.20    handle Type.TYPE_MATCH => raise TYPE ("expand_atom: ill-typed replacement", [T, U], [u]);
    1.21  
    1.22 +fun expand_term get_def =
    1.23 +  let
    1.24 +    fun expand tm =
    1.25 +      let
    1.26 +        val (head, args) = Term.strip_comb tm;
    1.27 +        val args' = map expand args;
    1.28 +        fun comb head' = Term.list_comb (head', args');
    1.29 +      in
    1.30 +        (case head of
    1.31 +          Abs (x, T, t) => comb (Abs (x, T, expand t))
    1.32 +        | _ =>
    1.33 +            (case get_def head of
    1.34 +              SOME def => Term.betapplys (expand_atom (Term.fastype_of head) def, args')
    1.35 +            | NONE => comb head)
    1.36 +        | _ => comb head)
    1.37 +      end;
    1.38 +  in expand end;
    1.39 +
    1.40  end;