for generated Haskell code, never use let-binds with pattern matching: irrefutable patterns destroy partial correctness
--- a/src/Tools/Code/code_haskell.ML Thu Apr 13 10:10:09 2017 +0200
+++ b/src/Tools/Code/code_haskell.ML Thu Apr 13 10:10:12 2017 +0200
@@ -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 =
--- a/src/Tools/Code/code_thingol.ML Thu Apr 13 10:10:09 2017 +0200
+++ b/src/Tools/Code/code_thingol.ML Thu Apr 13 10:10:12 2017 +0200
@@ -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)