# HG changeset patch
# User haftmann
# Date 1168592311 -3600
# Node ID f4cfc4101c8f9040d7f4816e53b1ca60b29a2f42
# Parent  547b0303f37b5a2d4c0e9133ea904b9decadfeb4
more term inspection

diff -r 547b0303f37b -r f4cfc4101c8f src/Pure/Tools/codegen_thingol.ML
--- a/src/Pure/Tools/codegen_thingol.ML	Fri Jan 12 09:58:30 2007 +0100
+++ b/src/Pure/Tools/codegen_thingol.ML	Fri Jan 12 09:58:31 2007 +0100
@@ -46,7 +46,9 @@
   val unfoldr: ('a -> ('b * 'a) option) -> 'a -> 'b list * 'a;
   val unfold_fun: itype -> itype list * itype;
   val unfold_app: iterm -> iterm * iterm list;
+  val split_abs: iterm -> (((vname * iterm option) * itype) * iterm) option;
   val unfold_abs: iterm -> ((vname * iterm option) * itype) list * iterm;
+  val split_let: iterm -> (((iterm * itype) * iterm) * iterm) option;
   val unfold_let: iterm -> ((iterm * itype) * iterm) list * iterm;
   val unfold_const_app: iterm ->
     ((string * (inst list list * itype)) * iterm list) option;
@@ -106,7 +108,6 @@
         let val (xs', x') = unfoldr dest x2 in (x1::xs', x') end;
 
 
-
 (** language core - types, pattern, expressions **)
 
 (* language representation *)
@@ -169,16 +170,20 @@
   (fn op `$ t => SOME t
     | _ => NONE);
 
-val unfold_abs = unfoldr
+val split_abs =
   (fn (v, ty) `|-> (t as ICase ((IVar w, _), [(p, t')])) =>
         if v = w then SOME (((v, SOME p), ty), t') else SOME (((v, NONE), ty), t)
     | (v, ty) `|-> t => SOME (((v, NONE), ty), t)
-    | _ => NONE)
+    | _ => NONE);
 
-val unfold_let = unfoldr
+val unfold_abs = unfoldr split_abs;
+
+val split_let = 
   (fn ICase ((td, ty), [(p, t)]) => SOME (((p, ty), td), t)
     | _ => NONE);
 
+val unfold_let = unfoldr split_let;
+
 fun unfold_const_app t =
  case unfold_app t
   of (IConst c, ts) => SOME (c, ts)