src/Tools/code/code_haskell.ML
changeset 31665 a1f4d3b3f6c8
parent 31376 4356b52b03f7
child 31724 9b5a128cdb5c
equal deleted inserted replaced
31643:b040f1679f77 31665:a1f4d3b3f6c8
   104             fun pr ((pat, ty), t) vars =
   104             fun pr ((pat, ty), t) vars =
   105               vars
   105               vars
   106               |> pr_bind tyvars thm BR ((NONE, SOME pat), ty)
   106               |> pr_bind tyvars thm BR ((NONE, SOME pat), ty)
   107               |>> (fn p => semicolon [p, str "=", pr_term tyvars thm vars NOBR t])
   107               |>> (fn p => semicolon [p, str "=", pr_term tyvars thm vars NOBR t])
   108             val (ps, vars') = fold_map pr binds vars;
   108             val (ps, vars') = fold_map pr binds vars;
   109           in 
   109           in brackify_block fxy (str "let {")
   110             Pretty.block_enclose (
   110             ps
   111               str "(let {",
   111             (concat [str "}", str "in", pr_term tyvars thm vars' NOBR body])
   112               concat [str "}", str "in", pr_term tyvars thm vars' NOBR body, str ")"]
       
   113             ) ps
       
   114           end
   112           end
   115       | pr_case tyvars thm vars fxy (((t, ty), clauses as _ :: _), _) =
   113       | pr_case tyvars thm vars fxy (((t, ty), clauses as _ :: _), _) =
   116           let
   114           let
   117             fun pr (pat, body) =
   115             fun pr (pat, body) =
   118               let
   116               let
   119                 val (p, vars') = pr_bind tyvars thm NOBR ((NONE, SOME pat), ty) vars;
   117                 val (p, vars') = pr_bind tyvars thm NOBR ((NONE, SOME pat), ty) vars;
   120               in semicolon [p, str "->", pr_term tyvars thm vars' NOBR body] end;
   118               in semicolon [p, str "->", pr_term tyvars thm vars' NOBR body] end;
   121           in
   119           in brackify_block fxy
   122             Pretty.block_enclose (
   120             (concat [str "case", pr_term tyvars thm vars NOBR t, str "of", str "{"])
   123               concat [str "(case", pr_term tyvars thm vars NOBR t, str "of", str "{"],
   121             (map pr clauses)
   124               str "})"
   122             (str "}") 
   125             ) (map pr clauses)
       
   126           end
   123           end
   127       | pr_case tyvars thm vars fxy ((_, []), _) =
   124       | pr_case tyvars thm vars fxy ((_, []), _) =
   128           (brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""];
   125           (brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""];
   129     fun pr_stmt (name, Code_Thingol.Fun (_, ((vs, ty), []))) =
   126     fun pr_stmt (name, Code_Thingol.Fun (_, ((vs, ty), []))) =
   130           let
   127           let