# HG changeset patch
# User haftmann
# Date 1186667577 -7200
# Node ID 9e77397eba8ebd25be9d35982b5541c9acac8842
# Parent  a879b30e8e86f3a4efd3bd2a1fdd06dd6d692b4d
explizit checking for pattern discipline

diff -r a879b30e8e86 -r 9e77397eba8e src/Pure/Tools/codegen_serializer.ML
--- a/src/Pure/Tools/codegen_serializer.ML	Thu Aug 09 15:52:56 2007 +0200
+++ b/src/Pure/Tools/codegen_serializer.ML	Thu Aug 09 15:52:57 2007 +0200
@@ -162,18 +162,22 @@
 
 (* generic serializer combinators *)
 
-fun gen_pr_app pr_app' pr_term const_syntax vars fxy (app as ((c, (_, tys)), ts)) =
+fun gen_pr_app pr_app' pr_term const_syntax labelled_name is_cons
+      lhs vars fxy (app as ((c, (_, tys)), ts)) =
   case const_syntax c
-   of NONE => brackify fxy (pr_app' vars app)
+   of NONE => if lhs andalso not (is_cons c) then
+          error ("non-constructor on left hand side of equation: " ^ labelled_name c)
+        else brackify fxy (pr_app' lhs vars app)
     | SOME (i, pr) =>
         let
           val k = if i < 0 then length tys else i;
-          fun pr' fxy ts = pr pr_term vars fxy (ts ~~ curry Library.take k tys);
+          fun pr' fxy ts = pr (pr_term lhs) vars fxy (ts ~~ curry Library.take k tys);
         in if k = length ts
           then pr' fxy ts
         else if k < length ts
-          then case chop k ts of (ts1, ts2) => brackify fxy (pr' APP ts1 :: map (pr_term vars BR) ts2)
-          else pr_term vars fxy (CodegenThingol.eta_expand app k)
+          then case chop k ts of (ts1, ts2) =>
+            brackify fxy (pr' APP ts1 :: map (pr_term lhs vars BR) ts2)
+          else pr_term lhs vars fxy (CodegenThingol.eta_expand app k)
         end;
 
 fun gen_pr_bind pr_bind' pr_term fxy ((v, pat), ty) vars =
@@ -341,56 +345,56 @@
                 else pr pr_typ fxy tys)
       | pr_typ fxy (ITyVar v) =
           str ("'" ^ v);
-    fun pr_term vars fxy (IConst c) =
-          pr_app vars fxy (c, [])
-      | pr_term vars fxy (IVar v) =
+    fun pr_term lhs vars fxy (IConst c) =
+          pr_app lhs vars fxy (c, [])
+      | pr_term lhs vars fxy (IVar v) =
           str (CodegenNames.lookup_var vars v)
-      | pr_term vars fxy (t as t1 `$ t2) =
+      | pr_term lhs vars fxy (t as t1 `$ t2) =
           (case CodegenThingol.unfold_const_app t
-           of SOME c_ts => pr_app vars fxy c_ts
+           of SOME c_ts => pr_app lhs vars fxy c_ts
             | NONE =>
-                brackify fxy [pr_term vars NOBR t1, pr_term vars BR t2])
-      | pr_term vars fxy (t as _ `|-> _) =
+                brackify fxy [pr_term lhs vars NOBR t1, pr_term lhs vars BR t2])
+      | pr_term lhs vars fxy (t as _ `|-> _) =
           let
             val (binds, t') = CodegenThingol.unfold_abs t;
             fun pr ((v, pat), ty) =
               pr_bind NOBR ((SOME v, pat), ty)
               #>> (fn p => concat [str "fn", p, str "=>"]);
             val (ps, vars') = fold_map pr binds vars;
-          in brackets (ps @ [pr_term vars' NOBR t']) end
-      | pr_term vars fxy (ICase (cases as (_, t0))) = (case CodegenThingol.unfold_const_app t0
+          in brackets (ps @ [pr_term lhs vars' NOBR t']) end
+      | pr_term lhs vars fxy (ICase (cases as (_, t0))) = (case CodegenThingol.unfold_const_app t0
            of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
                 then pr_case vars fxy cases
-                else pr_app vars fxy c_ts
+                else pr_app lhs vars fxy c_ts
             | NONE => pr_case vars fxy cases)
-    and pr_app' vars (app as ((c, (iss, tys)), ts)) =
+    and pr_app' lhs vars (app as ((c, (iss, tys)), ts)) =
       if is_cons c then let
         val k = length tys
       in if k < 2 then 
-        (str o deresolv) c :: map (pr_term vars BR) ts
+        (str o deresolv) c :: map (pr_term lhs vars BR) ts
       else if k = length ts then
-        [(str o deresolv) c, Pretty.enum "," "(" ")" (map (pr_term vars NOBR) ts)]
-      else [pr_term vars BR (CodegenThingol.eta_expand app k)] end else
+        [(str o deresolv) c, Pretty.enum "," "(" ")" (map (pr_term lhs vars NOBR) ts)]
+      else [pr_term lhs vars BR (CodegenThingol.eta_expand app k)] end else
         (str o deresolv) c
-          :: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term vars BR) ts)
-    and pr_app vars = gen_pr_app pr_app' pr_term const_syntax vars
+          :: (map (pr_dicts BR) o filter_out null) iss @ map (pr_term lhs vars BR) ts
+    and pr_app lhs vars = gen_pr_app pr_app' pr_term const_syntax labelled_name is_cons lhs 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 fxy = gen_pr_bind pr_bind' pr_term fxy
+    and pr_bind fxy = gen_pr_bind pr_bind' (pr_term false) fxy
     and pr_case vars fxy (cases as ((_, [_]), _)) =
           let
             val (binds, t') = CodegenThingol.unfold_let (ICase cases);
             fun pr ((pat, ty), t) vars =
               vars
               |> pr_bind NOBR ((NONE, SOME pat), ty)
-              |>> (fn p => semicolon [str "val", p, str "=", pr_term vars NOBR t])
+              |>> (fn p => semicolon [str "val", p, str "=", pr_term false vars NOBR t])
             val (ps, vars') = fold_map pr binds vars;
           in
             Pretty.chunks [
               [str ("let"), Pretty.fbrk, Pretty.chunks ps] |> Pretty.block,
-              [str ("in"), Pretty.fbrk, pr_term vars' NOBR t'] |> Pretty.block,
+              [str ("in"), Pretty.fbrk, pr_term false vars' NOBR t'] |> Pretty.block,
               str ("end")
             ]
           end
@@ -400,12 +404,12 @@
               let
                 val (p, vars') = pr_bind NOBR ((NONE, SOME pat), ty) vars;
               in
-                concat [str delim, p, str "=>", pr_term vars' NOBR t]
+                concat [str delim, p, str "=>", pr_term false vars' NOBR t]
               end;
           in
             (Pretty.enclose "(" ")" o single o brackify fxy) (
               str "case"
-              :: pr_term vars NOBR td
+              :: pr_term false vars NOBR td
               :: pr "of" b
               :: map (pr "|") bs
             )
@@ -447,8 +451,8 @@
                          then [str ":", pr_typ NOBR ty]
                          else
                            pr_tyvars vs
-                           @ map (pr_term vars BR) ts)
-                   @ [str "=", pr_term vars NOBR t]
+                           @ map (pr_term true vars BR) ts)
+                   @ [str "=", pr_term false vars NOBR t]
                     )
                   end
               in
@@ -547,7 +551,7 @@
                 concat [
                   (str o pr_label_classop) classop,
                   str "=",
-                  pr_term vars NOBR t
+                  pr_term false vars NOBR t
                 ]
               end;
           in
@@ -613,61 +617,61 @@
                 else pr pr_typ fxy tys)
       | pr_typ fxy (ITyVar v) =
           str ("'" ^ v);
-    fun pr_term vars fxy (IConst c) =
-          pr_app vars fxy (c, [])
-      | pr_term vars fxy (IVar v) =
+    fun pr_term lhs vars fxy (IConst c) =
+          pr_app lhs vars fxy (c, [])
+      | pr_term lhs vars fxy (IVar v) =
           str (CodegenNames.lookup_var vars v)
-      | pr_term vars fxy (t as t1 `$ t2) =
+      | pr_term lhs vars fxy (t as t1 `$ t2) =
           (case CodegenThingol.unfold_const_app t
-           of SOME c_ts => pr_app vars fxy c_ts
+           of SOME c_ts => pr_app lhs vars fxy c_ts
             | NONE =>
-                brackify fxy [pr_term vars NOBR t1, pr_term vars BR t2])
-      | pr_term vars fxy (t as _ `|-> _) =
+                brackify fxy [pr_term lhs vars NOBR t1, pr_term lhs vars BR t2])
+      | pr_term lhs vars fxy (t as _ `|-> _) =
           let
             val (binds, t') = CodegenThingol.unfold_abs t;
             fun pr ((v, pat), ty) = pr_bind BR ((SOME v, pat), ty);
             val (ps, vars') = fold_map pr binds vars;
-          in brackets (str "fun" :: ps @ str "->" @@ pr_term vars' NOBR t') end
-      | pr_term vars fxy (ICase (cases as (_, t0))) = (case CodegenThingol.unfold_const_app t0
+          in brackets (str "fun" :: ps @ str "->" @@ pr_term lhs vars' NOBR t') end
+      | pr_term lhs vars fxy (ICase (cases as (_, t0))) = (case CodegenThingol.unfold_const_app t0
            of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
                 then pr_case vars fxy cases
-                else pr_app vars fxy c_ts
+                else pr_app lhs vars fxy c_ts
             | NONE => pr_case vars fxy cases)
-    and pr_app' vars (app as ((c, (iss, tys)), ts)) =
+    and pr_app' lhs vars (app as ((c, (iss, tys)), ts)) =
       if is_cons c then
         if length tys = length ts
         then case ts
          of [] => [(str o deresolv) c]
-          | [t] => [(str o deresolv) c, pr_term vars BR t]
-          | _ => [(str o deresolv) c, Pretty.enum "," "(" ")" (map (pr_term vars NOBR) ts)]
-        else [pr_term vars BR (CodegenThingol.eta_expand app (length tys))]
+          | [t] => [(str o deresolv) c, pr_term lhs vars BR t]
+          | _ => [(str o deresolv) c, Pretty.enum "," "(" ")" (map (pr_term lhs vars NOBR) ts)]
+        else [pr_term lhs vars BR (CodegenThingol.eta_expand app (length tys))]
       else (str o deresolv) c
-        :: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term vars BR) ts)
-    and pr_app vars = gen_pr_app pr_app' pr_term const_syntax vars
+        :: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term lhs vars BR) ts)
+    and pr_app lhs vars = gen_pr_app pr_app' pr_term const_syntax labelled_name is_cons lhs 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), _) = brackets [p, str "as", str v]
-    and pr_bind fxy = gen_pr_bind pr_bind' pr_term fxy
+    and pr_bind fxy = gen_pr_bind pr_bind' (pr_term false) fxy
     and pr_case vars fxy (cases as ((_, [_]), _)) =
           let
             val (binds, t') = CodegenThingol.unfold_let (ICase cases);
             fun pr ((pat, ty), t) vars =
               vars
               |> pr_bind NOBR ((NONE, SOME pat), ty)
-              |>> (fn p => concat [str "let", p, str "=", pr_term vars NOBR t, str "in"])
+              |>> (fn p => concat [str "let", p, str "=", pr_term false vars NOBR t, str "in"])
             val (ps, vars') = fold_map pr binds vars;
-          in Pretty.chunks (ps @| pr_term vars' NOBR t') end
+          in Pretty.chunks (ps @| pr_term false vars' NOBR t') end
       | pr_case vars fxy (((td, ty), b::bs), _) =
           let
             fun pr delim (pat, t) =
               let
                 val (p, vars') = pr_bind NOBR ((NONE, SOME pat), ty) vars;
-              in concat [str delim, p, str "->", pr_term vars' NOBR t] end;
+              in concat [str delim, p, str "->", pr_term false vars' NOBR t] end;
           in
             (Pretty.enclose "(" ")" o single o brackify fxy) (
               str "match"
-              :: pr_term vars NOBR td
+              :: pr_term false vars NOBR td
               :: pr "with" b
               :: map (pr "|") bs
             )
@@ -698,9 +702,9 @@
                   |> CodegenNames.intro_vars ((fold o CodegenThingol.fold_unbound_varnames)
                       (insert (op =)) ts []);
               in concat [
-                (Pretty.block o Pretty.commas) (map (pr_term vars NOBR) ts),
+                (Pretty.block o Pretty.commas) (map (pr_term true vars NOBR) ts),
                 str "->",
-                pr_term vars NOBR t
+                pr_term false vars NOBR t
               ] end;
             fun pr_eqs [(ts, t)] =
                   let
@@ -714,9 +718,9 @@
                           (insert (op =)) ts []);
                   in
                     concat (
-                      map (pr_term vars BR) ts
+                      map (pr_term true vars BR) ts
                       @ str "="
-                      @@ pr_term vars NOBR t
+                      @@ pr_term false vars NOBR t
                     )
                   end
               | pr_eqs (eqs as (eq as ([_], _)) :: eqs') =
@@ -837,7 +841,7 @@
                 concat [
                   (str o deresolv) classop,
                   str "=",
-                  pr_term vars NOBR t
+                  pr_term false vars NOBR t
                 ]
               end;
           in
@@ -872,9 +876,7 @@
   (_ : string -> class_syntax option) tyco_syntax const_syntax code =
   let
     val module_alias = if is_some module then K module else raw_module_alias;
-    val is_cons = fn node => case CodegenThingol.get_def code node
-     of CodegenThingol.Datatypecons _ => true
-      | _ => false;
+    val is_cons = CodegenThingol.is_cons code;
     datatype node =
         Def of string * ml_def option
       | Module of string * ((Name.context * Name.context) * node Graph.T);
@@ -1077,7 +1079,8 @@
 
 in
 
-fun pr_haskell class_syntax tyco_syntax const_syntax labelled_name init_syms deresolv_here deresolv deriving_show def =
+fun pr_haskell class_syntax tyco_syntax const_syntax labelled_name init_syms
+    deresolv_here deresolv is_cons deriving_show def =
   let
     fun class_name class = case class_syntax class
      of NONE => deresolv class
@@ -1115,45 +1118,45 @@
       Pretty.block (pr_typparms tyvars vs @@ pr_tycoexpr tyvars NOBR tycoexpr);
     fun pr_typscheme tyvars (vs, ty) =
       Pretty.block (pr_typparms tyvars vs @@ pr_typ tyvars NOBR ty);
-    fun pr_term vars fxy (IConst c) =
-          pr_app vars fxy (c, [])
-      | pr_term vars fxy (t as (t1 `$ t2)) =
+    fun pr_term lhs vars fxy (IConst c) =
+          pr_app lhs vars fxy (c, [])
+      | pr_term lhs vars fxy (t as (t1 `$ t2)) =
           (case CodegenThingol.unfold_const_app t
-           of SOME app => pr_app vars fxy app
+           of SOME app => pr_app lhs vars fxy app
             | _ =>
                 brackify fxy [
-                  pr_term vars NOBR t1,
-                  pr_term vars BR t2
+                  pr_term lhs vars NOBR t1,
+                  pr_term lhs vars BR t2
                 ])
-      | pr_term vars fxy (IVar v) =
+      | pr_term lhs vars fxy (IVar v) =
           (str o CodegenNames.lookup_var vars) v
-      | pr_term vars fxy (t as _ `|-> _) =
+      | pr_term lhs vars fxy (t as _ `|-> _) =
           let
             val (binds, t') = CodegenThingol.unfold_abs t;
             fun pr ((v, pat), ty) = pr_bind BR ((SOME v, pat), ty);
             val (ps, vars') = fold_map pr binds vars;
-          in brackets (str "\\" :: ps @ str "->" @@ pr_term vars' NOBR t') end
-      | pr_term vars fxy (ICase (cases as (_, t0))) = (case CodegenThingol.unfold_const_app t0
+          in brackets (str "\\" :: ps @ str "->" @@ pr_term lhs vars' NOBR t') end
+      | pr_term lhs vars fxy (ICase (cases as (_, t0))) = (case CodegenThingol.unfold_const_app t0
            of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
                 then pr_case vars fxy cases
-                else pr_app vars fxy c_ts
+                else pr_app lhs vars fxy c_ts
             | NONE => pr_case vars fxy cases)
-    and pr_app' vars ((c, _), ts) =
-      (str o deresolv) c :: map (pr_term vars BR) ts
-    and pr_app vars = gen_pr_app pr_app' pr_term const_syntax vars
-    and pr_bind fxy = pr_bind_haskell pr_term fxy
+    and pr_app' lhs vars ((c, _), ts) =
+      (str o deresolv) c :: map (pr_term lhs vars BR) ts
+    and pr_app lhs vars = gen_pr_app pr_app' pr_term const_syntax labelled_name is_cons lhs vars
+    and pr_bind fxy = pr_bind_haskell (pr_term false) fxy
     and pr_case vars fxy (cases as ((_, [_]), _)) =
           let
             val (binds, t) = CodegenThingol.unfold_let (ICase cases);
             fun pr ((pat, ty), t) vars =
               vars
               |> pr_bind BR ((NONE, SOME pat), ty)
-              |>> (fn p => semicolon [p, str "=", pr_term vars NOBR t])
+              |>> (fn p => semicolon [p, str "=", pr_term false vars NOBR t])
             val (ps, vars') = fold_map pr binds vars;
           in
             Pretty.block_enclose (
               str "let {",
-              concat [str "}", str "in", pr_term vars' NOBR t]
+              concat [str "}", str "in", pr_term false vars' NOBR t]
             ) ps
           end
       | pr_case vars fxy (((td, ty), bs as _ :: _), _) =
@@ -1161,10 +1164,10 @@
             fun pr (pat, t) =
               let
                 val (p, vars') = pr_bind NOBR ((NONE, SOME pat), ty) vars;
-              in semicolon [p, str "->", pr_term vars' NOBR t] end;
+              in semicolon [p, str "->", pr_term false vars' NOBR t] end;
           in
             Pretty.block_enclose (
-              concat [str "(case", pr_term vars NOBR td, str "of", str "{"],
+              concat [str "(case", pr_term false vars NOBR td, str "of", str "{"],
               str "})"
             ) (map pr bs)
           end
@@ -1185,9 +1188,9 @@
               in
                 semicolon (
                   (str o deresolv_here) name
-                  :: map (pr_term vars BR) ts
+                  :: map (pr_term true vars BR) ts
                   @ str "="
-                  @@ pr_term vars NOBR t
+                  @@ pr_term false vars NOBR t
                 )
               end;
           in
@@ -1276,7 +1279,7 @@
                   semicolon [
                     (str o classop_name class) classop,
                     str "=",
-                    pr_term vars NOBR t
+                    pr_term false vars NOBR t
                   ]
                 end;
           in
@@ -1315,9 +1318,10 @@
 end; (*local*)
 
 fun seri_haskell module_prefix module destination string_classes labelled_name
-  reserved_syms raw_module_alias module_prolog class_syntax tyco_syntax const_syntax code =
+    reserved_syms raw_module_alias module_prolog class_syntax tyco_syntax const_syntax code =
   let
     val _ = Option.map File.check destination;
+    val is_cons = CodegenThingol.is_cons code;
     val module_alias = if is_some module then K module else raw_module_alias;
     val init_names = Name.make_context reserved_syms;
     val name_modl = mk_modl_name_tab init_names module_prefix module_alias code;
@@ -1386,7 +1390,7 @@
           | deriv' _ (ITyVar _) = true
       in deriv [] tyco end;
     fun seri_def qualified = pr_haskell class_syntax tyco_syntax const_syntax labelled_name init_syms
-      deresolv_here (if qualified then deresolv else deresolv_here)
+      deresolv_here (if qualified then deresolv else deresolv_here) is_cons
       (if string_classes then deriving_show else K false);
     fun write_module (SOME destination) modlname =
           let
@@ -1458,7 +1462,7 @@
             pr_typ (INFX (1, R)) ty2
           ])
       | pr_fun _ = NONE
-    val pr = pr_haskell (K NONE) pr_fun (K NONE) labelled_name init_names I I (K false);
+    val pr = pr_haskell (K NONE) pr_fun (K NONE) labelled_name init_names I I (K false) (K false);
   in
     []
     |> Graph.fold (fn (name, (def, _)) => case try pr (name, def) of SOME p => cons p | NONE => I) code