# HG changeset patch
# User haftmann
# Date 1246376010 -7200
# Node ID fb2c8a687529c18f6ab620adcdd305abe077b9a6
# Parent  626c075fd457c7bf5b7b44e2aa4e56bb314e3965
all variable names are optional

diff -r 626c075fd457 -r fb2c8a687529 src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Tue Jun 30 16:43:28 2009 +0200
+++ b/src/Tools/Code/code_haskell.ML	Tue Jun 30 17:33:30 2009 +0200
@@ -23,12 +23,6 @@
 
 (** Haskell serializer **)
 
-fun pr_haskell_bind pr_term =
-  let
-    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
     init_syms deresolve is_cons contr_classparam_typs deriving_show =
   let
@@ -66,12 +60,14 @@
                   pr_term tyvars thm vars NOBR t1,
                   pr_term tyvars thm vars BR t2
                 ])
-      | pr_term tyvars thm vars fxy (IVar v) =
+      | pr_term tyvars thm vars fxy (IVar NONE) =
+          str "_"
+      | pr_term tyvars thm vars fxy (IVar (SOME v)) =
           (str o Code_Printer.lookup_var vars) v
       | pr_term tyvars thm vars fxy (t as _ `|=> _) =
           let
             val (binds, t') = Code_Thingol.unfold_pat_abs t;
-            val (ps, vars') = fold_map (pr_bind tyvars thm BR) binds vars;
+            val (ps, vars') = fold_map (pr_bind tyvars thm BR o fst) 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
@@ -94,13 +90,13 @@
           else (str o deresolve) c :: map (pr_term tyvars thm vars BR) ts
         end
     and pr_app tyvars = gen_pr_app (pr_app' tyvars) (pr_term tyvars) syntax_const
-    and pr_bind tyvars = pr_haskell_bind (pr_term tyvars)
+    and pr_bind tyvars thm fxy p = gen_pr_bind (pr_term tyvars) thm fxy p
     and pr_case tyvars thm vars fxy (cases as ((_, [_]), _)) =
           let
             val (binds, body) = Code_Thingol.unfold_let (ICase cases);
             fun pr ((pat, ty), t) vars =
               vars
-              |> pr_bind tyvars thm BR (SOME pat, ty)
+              |> pr_bind tyvars thm BR pat
               |>> (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 {")
@@ -111,7 +107,7 @@
           let
             fun pr (pat, body) =
               let
-                val (p, vars') = pr_bind tyvars thm NOBR (SOME pat, ty) vars;
+                val (p, vars') = pr_bind tyvars thm NOBR pat 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 "{"])
@@ -251,11 +247,10 @@
                       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) = (apfst o map) fst (Code_Thingol.unfold_abs proto_rhs);
-                    val vs' = map the vs;
                     val vars = init_syms
                       |> Code_Printer.intro_vars (the_list const)
-                      |> Code_Printer.intro_vars vs';
-                    val lhs = IConst (classparam, (([], []), tys)) `$$ map IVar vs';
+                      |> Code_Printer.intro_vars (map_filter I vs);
+                    val lhs = IConst (classparam, (([], []), tys)) `$$ map IVar vs;
                       (*dictionaries are not relevant at this late stage*)
                   in
                     semicolon [
@@ -444,29 +439,29 @@
 fun pretty_haskell_monad c_bind =
   let
     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')
+     of SOME ((pat, ty), t') =>
+          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 ((SOME pat, ty), false), tbind), t')
+              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 =
           (semicolon [pr vars NOBR t], vars)
-      | pr_monad pr_bind pr (SOME (bind, true), t) vars = vars
+      | pr_monad pr_bind pr (SOME ((bind, _), true), t) vars = vars
           |> pr_bind NOBR bind
           |>> (fn p => semicolon [p, str "<-", pr vars NOBR t])
-      | pr_monad pr_bind pr (SOME (bind, false), t) vars = vars
+      | pr_monad pr_bind pr (SOME ((bind, _), false), t) vars = vars
           |> pr_bind NOBR bind
           |>> (fn p => semicolon [str "let", p, str "=", pr vars NOBR t]);
     fun pretty _ [c_bind'] pr thm vars fxy [(t1, _), (t2, _)] = case dest_bind t1 t2
      of SOME (bind, t') => let
           val (binds, t'') = implode_monad c_bind' t'
-          val (ps, vars') = fold_map (pr_monad (pr_haskell_bind (K pr) thm) pr) (bind :: binds) vars;
+          val (ps, vars') = fold_map (pr_monad (gen_pr_bind (K pr) thm) pr) (bind :: binds) vars;
         in (brackify fxy o single o Pretty.enclose "do {" "}" o Pretty.breaks) (ps @| pr vars' NOBR t'') end
       | NONE => brackify_infix (1, L) fxy
           [pr vars (INFX (1, L)) t1, str ">>=", pr vars (INFX (1, X)) t2]
diff -r 626c075fd457 -r fb2c8a687529 src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Tue Jun 30 16:43:28 2009 +0200
+++ b/src/Tools/Code/code_ml.ML	Tue Jun 30 17:33:30 2009 +0200
@@ -85,7 +85,9 @@
       | pr_typ fxy (ITyVar v) = str ("'" ^ v);
     fun pr_term is_closure thm vars fxy (IConst c) =
           pr_app is_closure thm vars fxy (c, [])
-      | pr_term is_closure thm vars fxy (IVar v) =
+      | pr_term is_closure thm vars fxy (IVar NONE) =
+          str "_"
+      | pr_term is_closure thm vars fxy (IVar (SOME v)) =
           str (Code_Printer.lookup_var vars v)
       | pr_term is_closure thm vars fxy (t as t1 `$ t2) =
           (case Code_Thingol.unfold_const_app t
@@ -95,8 +97,8 @@
       | pr_term is_closure thm vars fxy (t as _ `|=> _) =
           let
             val (binds, t') = Code_Thingol.unfold_pat_abs t;
-            fun pr (some_pat, ty) =
-              pr_bind is_closure thm NOBR (some_pat, ty)
+            fun pr (pat, ty) =
+              pr_bind is_closure thm NOBR pat
               #>> (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,15 +124,13 @@
           :: (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, _) = str "_"
-      | pr_bind' (SOME p, _) = p
-    and pr_bind is_closure = gen_pr_bind pr_bind' (pr_term is_closure)
+    and pr_bind is_closure = gen_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 (SOME pat, ty)
+              |> pr_bind is_closure thm NOBR pat
               |>> (fn p => semicolon [str "val", p, str "=", pr_term is_closure thm vars NOBR t])
             val (ps, vars') = fold_map pr binds vars;
           in
@@ -144,7 +144,7 @@
           let
             fun pr delim (pat, body) =
               let
-                val (p, vars') = pr_bind is_closure thm NOBR (SOME pat, ty) vars;
+                val (p, vars') = pr_bind is_closure thm NOBR pat vars;
               in
                 concat [str delim, p, str "=>", pr_term is_closure thm vars' NOBR body]
               end;
@@ -392,7 +392,9 @@
       | pr_typ fxy (ITyVar v) = str ("'" ^ v);
     fun pr_term is_closure thm vars fxy (IConst c) =
           pr_app is_closure thm vars fxy (c, [])
-      | pr_term is_closure thm vars fxy (IVar v) =
+      | pr_term is_closure thm vars fxy (IVar NONE) =
+          str "_"
+      | pr_term is_closure thm vars fxy (IVar (SOME v)) =
           str (Code_Printer.lookup_var vars v)
       | pr_term is_closure thm vars fxy (t as t1 `$ t2) =
           (case Code_Thingol.unfold_const_app t
@@ -402,7 +404,7 @@
       | pr_term is_closure thm vars fxy (t as _ `|=> _) =
           let
             val (binds, t') = Code_Thingol.unfold_pat_abs t;
-            val (ps, vars') = fold_map (pr_bind is_closure thm BR) binds vars;
+            val (ps, vars') = fold_map (pr_bind is_closure thm BR o fst) 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)
@@ -424,15 +426,13 @@
         :: ((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, _) = str "_"
-      | pr_bind' (SOME p, _) = p
-    and pr_bind is_closure = gen_pr_bind pr_bind' (pr_term is_closure)
+    and pr_bind is_closure = gen_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 (SOME pat, ty)
+              |> pr_bind is_closure thm NOBR pat
               |>> (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;
@@ -444,7 +444,7 @@
           let
             fun pr delim (pat, body) =
               let
-                val (p, vars') = pr_bind is_closure thm NOBR (SOME pat, ty) vars;
+                val (p, vars') = pr_bind is_closure thm NOBR pat vars;
               in concat [str delim, p, str "->", pr_term is_closure thm vars' NOBR body] end;
           in
             brackets (
@@ -459,7 +459,7 @@
     fun fish_params vars eqs =
       let
         fun fish_param _ (w as SOME _) = w
-          | fish_param (IVar v) NONE = SOME v
+          | fish_param (IVar (SOME v)) NONE = SOME v
           | fish_param _ NONE = NONE;
         fun fillup_param _ (_, SOME v) = v
           | fillup_param x (i, NONE) = x ^ string_of_int i;
@@ -776,7 +776,7 @@
         val eqs = filter (snd o snd) raw_eqs;
         val (eqs', is_value) = if null (filter_out (null o snd) vs) then case eqs
          of [(([], t), thm)] => if (not o null o fst o Code_Thingol.unfold_fun) ty
-            then ([(([IVar "x"], t `$ IVar "x"), thm)], false)
+            then ([(([IVar (SOME "x")], t `$ IVar (SOME "x")), thm)], false)
             else (eqs, not (Code_Thingol.fold_constnames
               (fn name' => fn b => b orelse name = name') t false))
           | _ => (eqs, false)
diff -r 626c075fd457 -r fb2c8a687529 src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Tue Jun 30 16:43:28 2009 +0200
+++ b/src/Tools/Code/code_printer.ML	Tue Jun 30 17:33:30 2009 +0200
@@ -68,10 +68,9 @@
     -> (thm -> var_ctxt -> fixity -> iterm -> Pretty.T)
     -> (string -> const_syntax option)
     -> thm -> var_ctxt -> fixity -> const * iterm list -> Pretty.T
-  val gen_pr_bind: (Pretty.T option * itype -> Pretty.T)
-    -> (thm -> var_ctxt -> fixity -> iterm -> Pretty.T)
+  val gen_pr_bind: (thm -> var_ctxt -> fixity -> iterm -> Pretty.T)
     -> thm -> fixity
-    -> iterm option * itype -> var_ctxt -> Pretty.T * var_ctxt
+    -> iterm -> var_ctxt -> Pretty.T * var_ctxt
 
   val mk_name_module: Name.context -> string option -> (string -> string option)
     -> 'a Graph.T -> string -> string
@@ -216,14 +215,11 @@
           else pr_term thm vars fxy (Code_Thingol.eta_expand k app)
         end;
 
-fun gen_pr_bind pr_bind pr_term thm (fxy : fixity) (some_pat, ty : itype) vars =
+fun gen_pr_bind pr_term thm (fxy : fixity) pat vars =
   let
-    val vs = case some_pat
-     of SOME pat => Code_Thingol.fold_varnames (insert (op =)) pat []
-      | NONE => [];
+    val vs = Code_Thingol.fold_varnames (insert (op =)) pat [];
     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;
+  in (pr_term thm vars' fxy pat, vars') end;
 
 
 (* mixfix syntax *)
diff -r 626c075fd457 -r fb2c8a687529 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Tue Jun 30 16:43:28 2009 +0200
+++ b/src/Tools/Code/code_thingol.ML	Tue Jun 30 17:33:30 2009 +0200
@@ -23,7 +23,7 @@
   type const = string * ((itype list * dict list list) * itype list (*types of arguments*))
   datatype iterm =
       IConst of const
-    | IVar of vname
+    | IVar of vname option
     | `$ of iterm * iterm
     | `|=> of (vname option * itype) * iterm
     | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
@@ -43,8 +43,8 @@
   val unfold_abs: iterm -> (vname option * 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 split_pat_abs: iterm -> ((iterm * itype) * iterm) option
+  val unfold_pat_abs: iterm -> (iterm * itype) list * iterm
   val unfold_const_app: iterm -> (const * iterm list) option
   val eta_expand: int -> const * iterm list -> iterm
   val contains_dictvar: iterm -> bool
@@ -125,7 +125,7 @@
 
 datatype iterm =
     IConst of const
-  | IVar of vname
+  | IVar of vname option
   | `$ of iterm * iterm
   | `|=> of (vname option * itype) * iterm
   | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
@@ -167,7 +167,7 @@
 
 fun fold_varnames f =
   let
-    fun add (IVar v) = f v
+    fun add (IVar (SOME v)) = f v
       | add ((SOME v, _) `|=> _) = f v
       | add _ = I;
   in fold_aiterms add end;
@@ -175,7 +175,8 @@
 fun fold_unbound_varnames f =
   let
     fun add _ (IConst _) = I
-      | add vs (IVar v) = if not (member (op =) vs v) then f v else I
+      | add vs (IVar (SOME v)) = if not (member (op =) vs v) then f v else I
+      | add _ (IVar NONE) = I
       | add vs (t1 `$ t2) = add vs t1 #> add vs t2
       | add vs ((SOME v, _) `|=> t) = add (insert (op =) v vs) t
       | add vs ((NONE, _) `|=> t) = add vs t
@@ -185,13 +186,13 @@
 
 fun exists_var t v = fold_unbound_varnames (fn w => fn b => v = w orelse b) t false;
 
-fun split_pat_abs ((NONE, ty) `|=> t) = SOME ((NONE, ty), t)
+fun split_pat_abs ((NONE, ty) `|=> t) = SOME ((IVar NONE, ty), t)
   | split_pat_abs ((SOME v, ty) `|=> t) = SOME (case t
-     of ICase (((IVar w, _), [(p, t')]), _) =>
+     of ICase (((IVar (SOME w), _), [(p, t')]), _) =>
           if v = w andalso (exists_var p v orelse not (exists_var t' v))
-          then ((SOME p, ty), t')
-          else ((SOME (IVar v), ty), t)
-      | _ => ((SOME (IVar v), ty), t))
+          then ((p, ty), t')
+          else ((IVar (SOME v), ty), t)
+      | _ => ((IVar (SOME v), ty), t))
   | split_pat_abs _ = NONE;
 
 val unfold_pat_abs = unfoldr split_pat_abs;
@@ -201,8 +202,9 @@
     val j = length ts;
     val l = k - j;
     val ctxt = (fold o fold_varnames) Name.declare ts Name.context;
-    val vs_tys = Name.names ctxt "a" ((curry Library.take l o curry Library.drop j) tys);
-  in (map o apfst) SOME vs_tys `|==> IConst c `$$ ts @ map (IVar o fst) vs_tys end;
+    val vs_tys = (map o apfst) SOME
+      (Name.names ctxt "a" ((curry Library.take l o curry Library.drop j) tys));
+  in vs_tys `|==> IConst c `$$ ts @ map (IVar o fst) vs_tys end;
 
 fun contains_dictvar t =
   let
@@ -572,7 +574,7 @@
 and translate_term thy algbr funcgr thm (Const (c, ty)) =
       translate_app thy algbr funcgr thm ((c, ty), [])
   | translate_term thy algbr funcgr thm (Free (v, _)) =
-      pair (IVar v)
+      pair (IVar (SOME v))
   | translate_term thy algbr funcgr thm (Abs (abs as (_, ty, _))) =
       let
         val (v, t) = Syntax.variant_abs abs;
@@ -635,12 +637,12 @@
       in [(true, (Free v_ty, body))] end
       else map (uncurry mk_clause)
         (AList.make (Code.no_args thy) case_pats ~~ ts_clause);
-    fun retermify ty (_, (IVar x, body)) =
-          (SOME x, ty) `|=> body
+    fun retermify ty (_, (IVar v, body)) =
+          (v, ty) `|=> body
       | retermify _ (_, (pat, body)) =
           let
             val (IConst (_, (_, tys)), ts) = unfold_app pat;
-            val vs = map2 (fn IVar x => fn ty => (SOME x, ty)) ts tys;
+            val vs = map2 (fn IVar v => fn ty => (v, ty)) ts tys;
           in vs `|==> body end;
     fun mk_icase const t ty clauses =
       let
@@ -658,6 +660,39 @@
       #>> pair b) clauses
     #>> (fn (((const, t), ty), ds) => mk_icase const t ty ds)
   end
+
+(*and translate_case' thy algbr funcgr thm case_scheme (c_ty, ts) =
+  let
+    fun casify ts tys =
+      let
+        val t = nth ts t_pos;
+        val ty = nth tys t_pos;
+        val ts_clause = nth_drop t_pos ts;
+        fun strip_abs_eta t [] = t
+          | strip_abs_eta ((`|=>
+
+        fun mk_clause (co, num_co_args) t =
+          let
+            val (vs, body) = Term.strip_abs_eta num_co_args t;
+            val not_undefined = case body
+             of (Const (c, _)) => not (Code.is_undefined thy c)
+              | _ => true;
+            val pat = list_comb (Const (co, map snd vs ---> ty), map Free vs);
+          in (not_undefined, (pat, body)) end;
+
+        val clauses = if null case_pats then let val ([v_ty], body) =
+            Term.strip_abs_eta 1 (the_single ts_clause)
+          in [(true, (Free v_ty, body))] end
+          else map (uncurry mk_clause)
+            (AList.make (Code.no_args thy) case_pats ~~ ts_clause);
+
+      in ((t, ty), map_filter (fn (b, d) => if b then SOME d else NONE) clauses) end;
+  in
+    translate_const thy algbr funcgr thm c_ty
+    ##>> fold_map (translate_term thy algbr funcgr thm) ts
+    #>> (fn (t as IConst (c, (_, tys)), ts) => ICase (casify ts tys, t `$$ ts))
+  end*)
+
 and translate_app_case thy algbr funcgr thm (case_scheme as (num_args, _)) ((c, ty), ts) =
   if length ts < num_args then
     let
diff -r 626c075fd457 -r fb2c8a687529 src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Tue Jun 30 16:43:28 2009 +0200
+++ b/src/Tools/nbe.ML	Tue Jun 30 17:33:30 2009 +0200
@@ -193,7 +193,7 @@
             val (t', ts) = Code_Thingol.unfold_app t
           in of_iapp match_cont t' (fold_rev (cons o of_iterm NONE) ts []) end
         and of_iapp match_cont (IConst (c, ((_, dss), _))) ts = constapp c dss ts
-          | of_iapp match_cont (IVar v) ts = nbe_apps (nbe_bound v) ts
+          | of_iapp match_cont (IVar v) ts = nbe_apps (nbe_bound_optional v) ts
           | of_iapp match_cont ((v, _) `|=> t) ts =
               nbe_apps (nbe_abss 1 (ml_abs (ml_list [nbe_bound_optional v]) (of_iterm NONE t))) ts
           | of_iapp match_cont (ICase (((t, _), cs), t0)) ts =
@@ -214,8 +214,9 @@
           else pair (v, [])) vs names;
         val samepairs = maps (fn (v, vs) => map (pair v) vs) vs_renames;
         fun subst_vars (t as IConst _) samepairs = (t, samepairs)
-          | subst_vars (t as IVar v) samepairs = (case AList.lookup (op =) samepairs v
-             of SOME v' => (IVar v', AList.delete (op =) v samepairs)
+          | subst_vars (t as IVar NONE) samepairs = (t, samepairs)
+          | subst_vars (t as IVar (SOME v)) samepairs = (case AList.lookup (op =) samepairs v
+             of SOME v' => (IVar (SOME v'), AList.delete (op =) v samepairs)
               | NONE => (t, samepairs))
           | subst_vars (t1 `$ t2) samepairs = samepairs
               |> subst_vars t1
@@ -297,7 +298,8 @@
         val params = Name.invent_list [] "d" (length names);
         fun mk (k, name) =
           (name, ([(v, [])],
-            [([IConst (class, (([], []), [])) `$$ map IVar params], IVar (nth params k))]));
+            [([IConst (class, (([], []), [])) `$$ map (IVar o SOME) params],
+              IVar (SOME (nth params k)))]));
       in map_index mk names end
   | eqns_of_stmt (_, Code_Thingol.Classrel _) =
       []