simplified binding concept

--- a/src/Tools/Code/code_haskell.ML	Tue Jun 30 14:53:59 2009 +0200
+++ b/src/Tools/Code/code_haskell.ML	Tue Jun 30 14:54:00 2009 +0200
@@ -25,10 +25,8 @@
 
 fun pr_haskell_bind pr_term =
   let
-    fun pr_bind ((NONE, NONE), _) = str "_"
-      | pr_bind ((SOME v, NONE), _) = str v
-      | pr_bind ((NONE, SOME p), _) = p
-      | pr_bind ((SOME v, SOME p), _) = brackets [str v, str "@", p];
+    fun pr_bind (NONE, _) = str "_"
+      | pr_bind (SOME p, _) = p;
   in gen_pr_bind pr_bind pr_term end;
 
 fun pr_haskell_stmt labelled_name syntax_class syntax_tyco syntax_const
@@ -72,9 +70,8 @@
           (str o Code_Printer.lookup_var vars) v
       | pr_term tyvars thm vars fxy (t as _ `|=> _) =
           let
-            val (binds, t') = Code_Thingol.unfold_abs t;
-            fun pr ((v, pat), ty) = pr_bind tyvars thm BR ((SOME v, pat), ty);
-            val (ps, vars') = fold_map pr binds vars;
+            val (binds, t') = Code_Thingol.unfold_pat_abs t;
+            val (ps, vars') = fold_map (pr_bind tyvars thm BR) binds vars;
           in brackets (str "\\" :: ps @ str "->" @@ pr_term tyvars thm vars' NOBR t') end
       | pr_term tyvars thm vars fxy (ICase (cases as (_, t0))) =
           (case Code_Thingol.unfold_const_app t0
@@ -103,7 +100,7 @@
             val (binds, body) = Code_Thingol.unfold_let (ICase cases);
             fun pr ((pat, ty), t) vars =
               vars
-              |> pr_bind tyvars thm BR ((NONE, SOME pat), ty)
+              |> pr_bind tyvars thm BR (SOME pat, ty)
               |>> (fn p => semicolon [p, str "=", pr_term tyvars thm vars NOBR t])
             val (ps, vars') = fold_map pr binds vars;
           in brackify_block fxy (str "let {")
@@ -114,7 +111,7 @@
           let
             fun pr (pat, body) =
               let
-                val (p, vars') = pr_bind tyvars thm NOBR ((NONE, SOME pat), ty) vars;
+                val (p, vars') = pr_bind tyvars thm NOBR (SOME pat, ty) vars;
               in semicolon [p, str "->", pr_term tyvars thm vars' NOBR body] end;
           in brackify_block fxy
             (concat [str "case", pr_term tyvars thm vars NOBR t, str "of", str "{"])
@@ -240,8 +237,6 @@
           end
       | pr_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, classparam_insts))) =
           let
-            val split_abs_pure = (fn (v, _) `|=> t => SOME (v, t) | _ => NONE);
-            val unfold_abs_pure = Code_Thingol.unfoldr split_abs_pure;
             val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
             fun pr_instdef ((classparam, c_inst), (thm, _)) = case syntax_const classparam
              of NONE => semicolon [
@@ -255,7 +250,7 @@
                     val const = if (is_some o syntax_const) c_inst_name
                       then NONE else (SOME o Long_Name.base_name o deresolve) c_inst_name;
                     val proto_rhs = Code_Thingol.eta_expand k (c_inst, []);
-                    val (vs, rhs) = unfold_abs_pure proto_rhs;
+                    val (vs, rhs) = (apfst o map) fst (Code_Thingol.unfold_abs proto_rhs);
                     val vars = init_syms
                       |> Code_Printer.intro_vars (the_list const)
                       |> Code_Printer.intro_vars vs;
@@ -447,16 +442,16 @@
 
 fun pretty_haskell_monad c_bind =
   let
-    fun dest_bind t1 t2 = case Code_Thingol.split_abs t2
-     of SOME (((v, pat), ty), t') =>
-          SOME ((SOME (((SOME v, pat), ty), true), t1), t')
+    fun dest_bind t1 t2 = case Code_Thingol.split_pat_abs t2
+     of SOME ((some_pat, ty), t') =>
+          SOME ((SOME ((some_pat, ty), true), t1), t')
       | NONE => NONE;
     fun dest_monad c_bind_name (IConst (c, _) `$ t1 `$ t2) =
           if c = c_bind_name then dest_bind t1 t2
           else NONE
       | dest_monad _ t = case Code_Thingol.split_let t
          of SOME (((pat, ty), tbind), t') =>
-              SOME ((SOME (((NONE, SOME pat), ty), false), tbind), t')
+              SOME ((SOME ((SOME pat, ty), false), tbind), t')
           | NONE => NONE;
     fun implode_monad c_bind_name = Code_Thingol.unfoldr (dest_monad c_bind_name);
     fun pr_monad pr_bind pr (NONE, t) vars =

--- a/src/Tools/Code/code_ml.ML	Tue Jun 30 14:53:59 2009 +0200
+++ b/src/Tools/Code/code_ml.ML	Tue Jun 30 14:54:00 2009 +0200
@@ -94,9 +94,9 @@
                [pr_term is_closure thm vars NOBR t1, pr_term is_closure thm vars BR t2])
       | pr_term is_closure thm vars fxy (t as _ `|=> _) =
           let
-            val (binds, t') = Code_Thingol.unfold_abs t;
-            fun pr ((v, pat), ty) =
-              pr_bind is_closure thm NOBR ((SOME v, pat), ty)
+            val (binds, t') = Code_Thingol.unfold_pat_abs t;
+            fun pr (some_pat, ty) =
+              pr_bind is_closure thm NOBR (some_pat, ty)
               #>> (fn p => concat [str "fn", p, str "=>"]);
             val (ps, vars') = fold_map pr binds vars;
           in brackets (ps @ [pr_term is_closure thm vars' NOBR t']) end
@@ -122,17 +122,15 @@
           :: (map (pr_dicts BR) o filter_out null) iss @ map (pr_term is_closure thm vars BR) ts
     and pr_app is_closure thm vars = gen_pr_app (pr_app' is_closure) (pr_term is_closure)
       syntax_const thm vars
-    and pr_bind' ((NONE, NONE), _) = str "_"
-      | pr_bind' ((SOME v, NONE), _) = str v
-      | pr_bind' ((NONE, SOME p), _) = p
-      | pr_bind' ((SOME v, SOME p), _) = concat [str v, str "as", p]
+    and pr_bind' (NONE, _) = str "_"
+      | pr_bind' (SOME p, _) = p
     and pr_bind is_closure = gen_pr_bind pr_bind' (pr_term is_closure)
     and pr_case is_closure thm vars fxy (cases as ((_, [_]), _)) =
           let
             val (binds, body) = Code_Thingol.unfold_let (ICase cases);
             fun pr ((pat, ty), t) vars =
               vars
-              |> pr_bind is_closure thm NOBR ((NONE, SOME pat), ty)
+              |> pr_bind is_closure thm NOBR (SOME pat, ty)
               |>> (fn p => semicolon [str "val", p, str "=", pr_term is_closure thm vars NOBR t])
             val (ps, vars') = fold_map pr binds vars;
           in
@@ -146,7 +144,7 @@
           let
             fun pr delim (pat, body) =
               let
-                val (p, vars') = pr_bind is_closure thm NOBR ((NONE, SOME pat), ty) vars;
+                val (p, vars') = pr_bind is_closure thm NOBR (SOME pat, ty) vars;
               in
                 concat [str delim, p, str "=>", pr_term is_closure thm vars' NOBR body]
               end;
@@ -403,9 +401,8 @@
                 brackify fxy [pr_term is_closure thm vars NOBR t1, pr_term is_closure thm vars BR t2])
       | pr_term is_closure thm vars fxy (t as _ `|=> _) =
           let
-            val (binds, t') = Code_Thingol.unfold_abs t;
-            fun pr ((v, pat), ty) = pr_bind is_closure thm BR ((SOME v, pat), ty);
-            val (ps, vars') = fold_map pr binds vars;
+            val (binds, t') = Code_Thingol.unfold_pat_abs t;
+            val (ps, vars') = fold_map (pr_bind is_closure thm BR) binds vars;
           in brackets (str "fun" :: ps @ str "->" @@ pr_term is_closure thm vars' NOBR t') end
       | pr_term is_closure thm vars fxy (ICase (cases as (_, t0))) = (case Code_Thingol.unfold_const_app t0
            of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
@@ -427,17 +424,15 @@
         :: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term is_closure thm vars BR) ts)
     and pr_app is_closure = gen_pr_app (pr_app' is_closure) (pr_term is_closure)
       syntax_const
-    and pr_bind' ((NONE, NONE), _) = str "_"
-      | pr_bind' ((SOME v, NONE), _) = str v
-      | pr_bind' ((NONE, SOME p), _) = p
-      | pr_bind' ((SOME v, SOME p), _) = brackets [p, str "as", str v]
+    and pr_bind' (NONE, _) = str "_"
+      | pr_bind' (SOME p, _) = p
     and pr_bind is_closure = gen_pr_bind pr_bind' (pr_term is_closure)
     and pr_case is_closure thm vars fxy (cases as ((_, [_]), _)) =
           let
             val (binds, body) = Code_Thingol.unfold_let (ICase cases);
             fun pr ((pat, ty), t) vars =
               vars
-              |> pr_bind is_closure thm NOBR ((NONE, SOME pat), ty)
+              |> pr_bind is_closure thm NOBR (SOME pat, ty)
               |>> (fn p => concat
                   [str "let", p, str "=", pr_term is_closure thm vars NOBR t, str "in"])
             val (ps, vars') = fold_map pr binds vars;
@@ -449,7 +444,7 @@
           let
             fun pr delim (pat, body) =
               let
-                val (p, vars') = pr_bind is_closure thm NOBR ((NONE, SOME pat), ty) vars;
+                val (p, vars') = pr_bind is_closure thm NOBR (SOME pat, ty) vars;
               in concat [str delim, p, str "->", pr_term is_closure thm vars' NOBR body] end;
           in
             brackets (

--- a/src/Tools/Code/code_printer.ML	Tue Jun 30 14:53:59 2009 +0200
+++ b/src/Tools/Code/code_printer.ML	Tue Jun 30 14:54:00 2009 +0200
@@ -68,10 +68,10 @@
     -> (thm -> var_ctxt -> fixity -> iterm -> Pretty.T)
     -> (string -> const_syntax option)
     -> thm -> var_ctxt -> fixity -> const * iterm list -> Pretty.T
-  val gen_pr_bind: ((string option * Pretty.T option) * itype -> Pretty.T)
+  val gen_pr_bind: (Pretty.T option * itype -> Pretty.T)
     -> (thm -> var_ctxt -> fixity -> iterm -> Pretty.T)
     -> thm -> fixity
-    -> (string option * iterm option) * itype -> var_ctxt -> Pretty.T * var_ctxt
+    -> iterm option * itype -> var_ctxt -> Pretty.T * var_ctxt
 
   val mk_name_module: Name.context -> string option -> (string -> string option)
     -> 'a Graph.T -> string -> string
@@ -216,16 +216,14 @@
           else pr_term thm vars fxy (Code_Thingol.eta_expand k app)
         end;
 
-fun gen_pr_bind pr_bind pr_term thm (fxy : fixity) ((v, pat), ty : itype) vars =
+fun gen_pr_bind pr_bind pr_term thm (fxy : fixity) (some_pat, ty : itype) vars =
   let
-    val vs = case pat
+    val vs = case some_pat
      of SOME pat => Code_Thingol.fold_varnames (insert (op =)) pat []
       | NONE => [];
-    val vars' = intro_vars (the_list v) vars;
-    val vars'' = intro_vars vs vars';
-    val v' = Option.map (lookup_var vars') v;
-    val pat' = Option.map (pr_term thm vars'' fxy) pat;
-  in (pr_bind ((v', pat'), ty), vars'') end;
+    val vars' = intro_vars vs vars;
+    val some_pat' = Option.map (pr_term thm vars' fxy) some_pat;
+  in (pr_bind (some_pat', ty), vars') end;
 
 
 (* mixfix syntax *)

--- a/src/Tools/Code/code_thingol.ML	Tue Jun 30 14:53:59 2009 +0200
+++ b/src/Tools/Code/code_thingol.ML	Tue Jun 30 14:54:00 2009 +0200
@@ -40,13 +40,12 @@
   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 unfold_abs: iterm -> (vname * itype) list * iterm
   val split_let: iterm -> (((iterm * itype) * iterm) * iterm) option
   val unfold_let: iterm -> ((iterm * itype) * iterm) list * iterm
+  val split_pat_abs: iterm -> ((iterm option * itype) * iterm) option
+  val unfold_pat_abs: iterm -> (iterm option * itype) list * iterm
   val unfold_const_app: iterm -> (const * iterm list) option
-  val collapse_let: ((vname * itype) * iterm) * iterm
-    -> (iterm * itype) * (iterm * iterm) list
   val eta_expand: int -> const * iterm list -> iterm
   val contains_dictvar: iterm -> bool
   val locally_monomorphic: iterm -> bool
@@ -139,14 +138,10 @@
   (fn op `$ t => SOME t
     | _ => NONE);
 
-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)
+val unfold_abs = unfoldr
+  (fn op `|=> t => SOME t
     | _ => NONE);
 
-val unfold_abs = unfoldr split_abs;
-
 val split_let = 
   (fn ICase (((td, ty), [(p, t)]), _) => SOME (((p, ty), td), t)
     | _ => NONE);
@@ -186,17 +181,17 @@
       | add vs (ICase (_, t)) = add vs t;
   in add [] end;
 
-fun collapse_let (((v, ty), se), be as ICase (((IVar w, _), ds), _)) =
-      let
-        fun exists_v t = fold_unbound_varnames (fn w => fn b =>
-          b orelse v = w) t false;
-      in if v = w andalso forall (fn (t1, t2) =>
-        exists_v t1 orelse not (exists_v t2)) ds
-        then ((se, ty), ds)
-        else ((se, ty), [(IVar v, be)])
-      end
-  | collapse_let (((v, ty), se), be) =
-      ((se, ty), [(IVar v, be)])
+fun exists_var t v = fold_unbound_varnames (fn w => fn b => v = w orelse b) t false;
+
+val split_pat_abs = (fn (v, ty) `|=> t => (case t
+   of ICase (((IVar w, _), [(p, t')]), _) =>
+        if v = w andalso (exists_var p v orelse not (exists_var t' v))
+        then SOME ((SOME p, ty), t')
+        else SOME ((SOME (IVar v), ty), t)
+    | _ => SOME ((if exists_var t v then SOME (IVar v) else NONE, ty), t))
+  | _ => NONE);
+
+val unfold_pat_abs = unfoldr split_pat_abs;
 
 fun eta_expand k (c as (_, (_, tys)), ts) =
   let