# HG changeset patch
# Parent  65a2474441004d3db26b0c4343f023d131a00c94
for generated Haskell code, never use let-binds with pattern matching: irrefutable patterns destroy partial correctness

diff -r 65a247444100 src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Wed Jan 11 16:43:31 2017 +0100
+++ b/src/Tools/Code/code_haskell.ML	Wed Jan 11 20:51:37 2017 +0100
@@ -103,14 +103,14 @@
     and print_bind tyvars some_thm fxy p = gen_print_bind (print_term tyvars) some_thm fxy p
     and print_case tyvars some_thm vars fxy { clauses = [], ... } =
           (brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""]
-      | print_case tyvars some_thm vars fxy (case_expr as { clauses = [_], ... }) =
+      | print_case tyvars some_thm vars fxy (case_expr as { clauses = [(IVar _, _)], ... }) =
           let
-            val (binds, body) = Code_Thingol.unfold_let (ICase case_expr);
-            fun print_match ((pat, _), t) vars =
+            val (vs, body) = Code_Thingol.unfold_let_no_pat (ICase case_expr);
+            fun print_assignment ((some_v, _), t) vars =
               vars
-              |> print_bind tyvars some_thm BR pat
+              |> print_bind tyvars some_thm BR (IVar some_v)
               |>> (fn p => semicolon [p, str "=", print_term tyvars some_thm vars NOBR t])
-            val (ps, vars') = fold_map print_match binds vars;
+            val (ps, vars') = fold_map print_assignment vs vars;
           in brackify_block fxy (str "let {")
             ps
             (concat [str "}", str "in", print_term tyvars some_thm vars' NOBR body])
@@ -451,9 +451,9 @@
     fun dest_monad (IConst { sym = Constant c, ... } `$ t1 `$ t2) =
           if c = c_bind then dest_bind t1 t2
           else NONE
-      | dest_monad t = case Code_Thingol.split_let t
-         of SOME (((pat, ty), tbind), t') =>
-              SOME ((SOME ((pat, ty), false), tbind), t')
+      | dest_monad t = case Code_Thingol.split_let_no_pat t
+         of SOME (((some_v, ty), tbind), t') =>
+              SOME ((SOME ((IVar some_v, ty), false), tbind), t')
           | NONE => NONE;
     val implode_monad = Code_Thingol.unfoldr dest_monad;
     fun print_monad print_bind print_term (NONE, t) vars =
diff -r 65a247444100 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Wed Jan 11 16:43:31 2017 +0100
+++ b/src/Tools/Code/code_thingol.ML	Wed Jan 11 20:51:37 2017 +0100
@@ -47,7 +47,9 @@
   val unfold_app: iterm -> iterm * iterm list
   val unfold_abs: iterm -> (vname option * itype) list * iterm
   val split_let: iterm -> (((iterm * itype) * iterm) * iterm) option
+  val split_let_no_pat: iterm -> (((string option * itype) * iterm) * iterm) option
   val unfold_let: iterm -> ((iterm * itype) * iterm) list * iterm
+  val unfold_let_no_pat: iterm -> ((string option * itype) * iterm) 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
@@ -184,8 +186,14 @@
   (fn ICase { term = t, typ = ty, clauses = [(p, body)], ... } => SOME (((p, ty), t), body)
     | _ => NONE);
 
+val split_let_no_pat = 
+  (fn ICase { term = t, typ = ty, clauses = [(IVar v, body)], ... } => SOME (((v, ty), t), body)
+    | _ => NONE);
+
 val unfold_let = unfoldr split_let;
 
+val unfold_let_no_pat = unfoldr split_let_no_pat;
+
 fun unfold_const_app t =
  case unfold_app t
   of (IConst c, ts) => SOME (c, ts)