1(* Title: Tools/Code/code_haskell.ML 2 Author: Florian Haftmann, TU Muenchen 3 4Serializer for Haskell. 5*) 6 7signature CODE_HASKELL = 8sig 9 val language_params: string 10 val target: string 11 val print_numeral: string -> int -> string 12end; 13 14structure Code_Haskell : CODE_HASKELL = 15struct 16 17val target = "Haskell"; 18 19val language_extensions = 20 ["EmptyDataDecls", "RankNTypes", "ScopedTypeVariables"]; 21 22val language_pragma = 23 "{-# LANGUAGE " ^ commas language_extensions ^ " #-}"; 24 25val language_params = 26 space_implode " " (map (prefix "-X") language_extensions); 27 28open Basic_Code_Symbol; 29open Basic_Code_Thingol; 30open Code_Printer; 31 32infixr 5 @@; 33infixr 5 @|; 34 35 36(** Haskell serializer **) 37 38val print_haskell_string = 39 quote o translate_string (fn c => 40 if Symbol.is_ascii c then GHC.print_codepoint (ord c) 41 else error "non-ASCII byte in Haskell string literal"); 42 43fun print_haskell_stmt class_syntax tyco_syntax const_syntax 44 reserved deresolve deriving_show = 45 let 46 val deresolve_const = deresolve o Constant; 47 val deresolve_tyco = deresolve o Type_Constructor; 48 val deresolve_class = deresolve o Type_Class; 49 fun class_name class = case class_syntax class 50 of NONE => deresolve_class class 51 | SOME class => class; 52 fun print_typcontext tyvars vs = case maps (fn (v, sort) => map (pair v) sort) vs 53 of [] => [] 54 | constraints => enum "," "(" ")" ( 55 map (fn (v, class) => 56 str (class_name class ^ " " ^ lookup_var tyvars v)) constraints) 57 @@ str " => "; 58 fun print_typforall tyvars vs = case map fst vs 59 of [] => [] 60 | vnames => str "forall " :: Pretty.breaks 61 (map (str o lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1; 62 fun print_tyco_expr tyvars fxy (tyco, tys) = 63 brackify fxy (str tyco :: map (print_typ tyvars BR) tys) 64 and print_typ tyvars fxy (tyco `%% tys) = (case tyco_syntax tyco 65 of NONE => print_tyco_expr tyvars fxy (deresolve_tyco tyco, tys) 66 | SOME (_, print) => print (print_typ tyvars) fxy tys) 67 | print_typ tyvars fxy (ITyVar v) = (str o lookup_var tyvars) v; 68 fun print_typdecl tyvars (tyco, vs) = 69 print_tyco_expr tyvars NOBR (tyco, map ITyVar vs); 70 fun print_typscheme tyvars (vs, ty) = 71 Pretty.block (print_typforall tyvars vs @ print_typcontext tyvars vs @| print_typ tyvars NOBR ty); 72 fun print_term tyvars some_thm vars fxy (IConst const) = 73 print_app tyvars some_thm vars fxy (const, []) 74 | print_term tyvars some_thm vars fxy (t as (t1 `$ t2)) = 75 (case Code_Thingol.unfold_const_app t 76 of SOME app => print_app tyvars some_thm vars fxy app 77 | _ => 78 brackify fxy [ 79 print_term tyvars some_thm vars NOBR t1, 80 print_term tyvars some_thm vars BR t2 81 ]) 82 | print_term tyvars some_thm vars fxy (IVar NONE) = 83 str "_" 84 | print_term tyvars some_thm vars fxy (IVar (SOME v)) = 85 (str o lookup_var vars) v 86 | print_term tyvars some_thm vars fxy (t as _ `|=> _) = 87 let 88 val (binds, t') = Code_Thingol.unfold_pat_abs t; 89 val (ps, vars') = fold_map (print_bind tyvars some_thm BR o fst) binds vars; 90 in brackets (str "\\" :: ps @ str "->" @@ print_term tyvars some_thm vars' NOBR t') end 91 | print_term tyvars some_thm vars fxy (ICase case_expr) = 92 (case Code_Thingol.unfold_const_app (#primitive case_expr) 93 of SOME (app as ({ sym = Constant const, ... }, _)) => 94 if is_none (const_syntax const) 95 then print_case tyvars some_thm vars fxy case_expr 96 else print_app tyvars some_thm vars fxy app 97 | NONE => print_case tyvars some_thm vars fxy case_expr) 98 and print_app_expr tyvars some_thm vars ({ sym, annotation, ... }, ts) = 99 let 100 val printed_const = 101 case annotation of 102 SOME ty => brackets [(str o deresolve) sym, str "::", print_typ tyvars NOBR ty] 103 | NONE => (str o deresolve) sym 104 in 105 printed_const :: map (print_term tyvars some_thm vars BR) ts 106 end 107 and print_app tyvars = gen_print_app (print_app_expr tyvars) (print_term tyvars) const_syntax 108 and print_bind tyvars some_thm fxy p = gen_print_bind (print_term tyvars) some_thm fxy p 109 and print_case tyvars some_thm vars fxy { clauses = [], ... } = 110 (brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""] 111 | print_case tyvars some_thm vars fxy (case_expr as { clauses = [(IVar _, _)], ... }) = 112 let 113 val (vs, body) = Code_Thingol.unfold_let_no_pat (ICase case_expr); 114 fun print_assignment ((some_v, _), t) vars = 115 vars 116 |> print_bind tyvars some_thm BR (IVar some_v) 117 |>> (fn p => semicolon [p, str "=", print_term tyvars some_thm vars NOBR t]) 118 val (ps, vars') = fold_map print_assignment vs vars; 119 in brackify_block fxy (str "let {") 120 ps 121 (concat [str "}", str "in", print_term tyvars some_thm vars' NOBR body]) 122 end 123 | print_case tyvars some_thm vars fxy { term = t, typ = ty, clauses = clauses as _ :: _, ... } = 124 let 125 fun print_select (pat, body) = 126 let 127 val (p, vars') = print_bind tyvars some_thm NOBR pat vars; 128 in semicolon [p, str "->", print_term tyvars some_thm vars' NOBR body] end; 129 in Pretty.block_enclose 130 (concat [str "(case", print_term tyvars some_thm vars NOBR t, str "of", str "{"], str "})") 131 (map print_select clauses) 132 end; 133 fun print_stmt (Constant const, Code_Thingol.Fun (((vs, ty), raw_eqs), _)) = 134 let 135 val tyvars = intro_vars (map fst vs) reserved; 136 fun print_err n = 137 (semicolon o map str) ( 138 deresolve_const const 139 :: replicate n "_" 140 @ "=" 141 :: "error" 142 @@ print_haskell_string const 143 ); 144 fun print_eqn ((ts, t), (some_thm, _)) = 145 let 146 val vars = reserved 147 |> intro_base_names_for (is_none o const_syntax) 148 deresolve (t :: ts) 149 |> intro_vars ((fold o Code_Thingol.fold_varnames) 150 (insert (op =)) ts []); 151 in 152 semicolon ( 153 (str o deresolve_const) const 154 :: map (print_term tyvars some_thm vars BR) ts 155 @ str "=" 156 @@ print_term tyvars some_thm vars NOBR t 157 ) 158 end; 159 in 160 Pretty.chunks ( 161 semicolon [ 162 (str o suffix " ::" o deresolve_const) const, 163 print_typscheme tyvars (vs, ty) 164 ] 165 :: (case filter (snd o snd) raw_eqs 166 of [] => [print_err ((length o fst o Code_Thingol.unfold_fun) ty)] 167 | eqs => map print_eqn eqs) 168 ) 169 end 170 | print_stmt (Type_Constructor tyco, Code_Thingol.Datatype (vs, [])) = 171 let 172 val tyvars = intro_vars vs reserved; 173 in 174 semicolon [ 175 str "data", 176 print_typdecl tyvars (deresolve_tyco tyco, vs) 177 ] 178 end 179 | print_stmt (Type_Constructor tyco, Code_Thingol.Datatype (vs, [((co, _), [ty])])) = 180 let 181 val tyvars = intro_vars vs reserved; 182 in 183 semicolon ( 184 str "newtype" 185 :: print_typdecl tyvars (deresolve_tyco tyco, vs) 186 :: str "=" 187 :: (str o deresolve_const) co 188 :: print_typ tyvars BR ty 189 :: (if deriving_show tyco then [str "deriving (Prelude.Read, Prelude.Show)"] else []) 190 ) 191 end 192 | print_stmt (Type_Constructor tyco, Code_Thingol.Datatype (vs, co :: cos)) = 193 let 194 val tyvars = intro_vars vs reserved; 195 fun print_co ((co, _), tys) = 196 concat ( 197 (str o deresolve_const) co 198 :: map (print_typ tyvars BR) tys 199 ) 200 in 201 semicolon ( 202 str "data" 203 :: print_typdecl tyvars (deresolve_tyco tyco, vs) 204 :: str "=" 205 :: print_co co 206 :: map ((fn p => Pretty.block [str "| ", p]) o print_co) cos 207 @ (if deriving_show tyco then [str "deriving (Prelude.Read, Prelude.Show)"] else []) 208 ) 209 end 210 | print_stmt (Type_Class class, Code_Thingol.Class (v, (classrels, classparams))) = 211 let 212 val tyvars = intro_vars [v] reserved; 213 fun print_classparam (classparam, ty) = 214 semicolon [ 215 (str o deresolve_const) classparam, 216 str "::", 217 print_typ tyvars NOBR ty 218 ] 219 in 220 Pretty.block_enclose ( 221 Pretty.block [ 222 str "class ", 223 Pretty.block (print_typcontext tyvars [(v, map snd classrels)]), 224 str (deresolve_class class ^ " " ^ lookup_var tyvars v), 225 str " where {" 226 ], 227 str "};" 228 ) (map print_classparam classparams) 229 end 230 | print_stmt (_, Code_Thingol.Classinst { class, tyco, vs, inst_params, ... }) = 231 let 232 val tyvars = intro_vars (map fst vs) reserved; 233 fun print_classparam_instance ((classparam, (const, _)), (thm, _)) = 234 case const_syntax classparam of 235 NONE => semicolon [ 236 (str o Long_Name.base_name o deresolve_const) classparam, 237 str "=", 238 print_app tyvars (SOME thm) reserved NOBR (const, []) 239 ] 240 | SOME (_, Code_Printer.Plain_printer s) => semicolon [ 241 (str o Long_Name.base_name) s, 242 str "=", 243 print_app tyvars (SOME thm) reserved NOBR (const, []) 244 ] 245 | SOME (k, Code_Printer.Complex_printer _) => 246 let 247 val { sym = Constant c, dom, ... } = const; 248 val (vs, rhs) = (apfst o map) fst 249 (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, []))); 250 val s = if (is_some o const_syntax) c 251 then NONE else (SOME o Long_Name.base_name o deresolve_const) c; 252 val vars = reserved 253 |> intro_vars (map_filter I (s :: vs)); 254 val lhs = IConst { sym = Constant classparam, typargs = [], 255 dicts = [], dom = dom, annotation = NONE } `$$ map IVar vs; 256 (*dictionaries are not relevant at this late stage, 257 and these consts never need type annotations for disambiguation *) 258 in 259 semicolon [ 260 print_term tyvars (SOME thm) vars NOBR lhs, 261 str "=", 262 print_term tyvars (SOME thm) vars NOBR rhs 263 ] 264 end; 265 in 266 Pretty.block_enclose ( 267 Pretty.block [ 268 str "instance ", 269 Pretty.block (print_typcontext tyvars vs), 270 str (class_name class ^ " "), 271 print_typ tyvars BR (tyco `%% map (ITyVar o fst) vs), 272 str " where {" 273 ], 274 str "};" 275 ) (map print_classparam_instance inst_params) 276 end; 277 in print_stmt end; 278 279fun haskell_program_of_program ctxt module_prefix module_name reserved identifiers = 280 let 281 fun namify_fun upper base (nsp_fun, nsp_typ) = 282 let 283 val (base', nsp_fun') = Name.variant (Name.enforce_case upper base) nsp_fun; 284 in (base', (nsp_fun', nsp_typ)) end; 285 fun namify_typ base (nsp_fun, nsp_typ) = 286 let 287 val (base', nsp_typ') = Name.variant (Name.enforce_case true base) nsp_typ; 288 in (base', (nsp_fun, nsp_typ')) end; 289 fun namify_stmt (Code_Thingol.Fun (_, SOME _)) = pair 290 | namify_stmt (Code_Thingol.Fun _) = namify_fun false 291 | namify_stmt (Code_Thingol.Datatype _) = namify_typ 292 | namify_stmt (Code_Thingol.Datatypecons _) = namify_fun true 293 | namify_stmt (Code_Thingol.Class _) = namify_typ 294 | namify_stmt (Code_Thingol.Classrel _) = pair 295 | namify_stmt (Code_Thingol.Classparam _) = namify_fun false 296 | namify_stmt (Code_Thingol.Classinst _) = pair; 297 fun select_stmt (Code_Thingol.Fun (_, SOME _)) = false 298 | select_stmt (Code_Thingol.Fun _) = true 299 | select_stmt (Code_Thingol.Datatype _) = true 300 | select_stmt (Code_Thingol.Datatypecons _) = false 301 | select_stmt (Code_Thingol.Class _) = true 302 | select_stmt (Code_Thingol.Classrel _) = false 303 | select_stmt (Code_Thingol.Classparam _) = false 304 | select_stmt (Code_Thingol.Classinst _) = true; 305 in 306 Code_Namespace.flat_program ctxt 307 { module_prefix = module_prefix, module_name = module_name, reserved = reserved, 308 identifiers = identifiers, empty_nsp = (reserved, reserved), namify_stmt = namify_stmt, 309 modify_stmt = fn stmt => if select_stmt stmt then SOME stmt else NONE } 310 end; 311 312val prelude_import_operators = [ 313 "==", "/=", "<", "<=", ">=", ">", "+", "-", "*", "/", "**", ">>=", ">>", "=<<", "&&", "||", "^", "^^", ".", "$", "$!", "++", "!!" 314]; 315 316val prelude_import_unqualified = [ 317 "Eq", 318 "error", 319 "id", 320 "return", 321 "not", 322 "fst", "snd", 323 "map", "filter", "concat", "concatMap", "reverse", "zip", "null", "takeWhile", "dropWhile", "all", "any", 324 "Integer", "negate", "abs", "divMod", 325 "String" 326]; 327 328val prelude_import_unqualified_constr = [ 329 ("Bool", ["True", "False"]), 330 ("Maybe", ["Nothing", "Just"]) 331]; 332 333fun serialize_haskell module_prefix string_classes ctxt { module_name, 334 reserved_syms, identifiers, includes, class_syntax, tyco_syntax, const_syntax } program exports = 335 let 336 337 (* build program *) 338 val reserved = fold (insert (op =) o fst) includes reserved_syms; 339 val { deresolver, flat_program = haskell_program } = haskell_program_of_program 340 ctxt module_prefix module_name (Name.make_context reserved) identifiers exports program; 341 342 (* print statements *) 343 fun deriving_show tyco = 344 let 345 fun deriv _ "fun" = false 346 | deriv tycos tyco = member (op =) tycos tyco 347 orelse case try (Code_Symbol.Graph.get_node program) (Type_Constructor tyco) 348 of SOME (Code_Thingol.Datatype (_, cs)) => forall (deriv' (tyco :: tycos)) 349 (maps snd cs) 350 | NONE => true 351 and deriv' tycos (tyco `%% tys) = deriv tycos tyco 352 andalso forall (deriv' tycos) tys 353 | deriv' _ (ITyVar _) = true 354 in deriv [] tyco end; 355 fun print_stmt deresolve = print_haskell_stmt 356 class_syntax tyco_syntax const_syntax (make_vars reserved) 357 deresolve (if string_classes then deriving_show else K false); 358 359 (* print modules *) 360 fun module_names module_name = 361 let 362 val (xs, x) = split_last (Long_Name.explode module_name) 363 in xs @ [x ^ ".hs"] end 364 fun print_module_frame module_name header exports ps = 365 (module_names module_name, Pretty.chunks2 ( 366 header 367 @ concat [str "module", 368 case exports of 369 SOME ps => Pretty.block [str module_name, enclose "(" ")" (commas ps)] 370 | NONE => str module_name, 371 str "where {" 372 ] 373 :: ps 374 @| str "}" 375 )); 376 fun print_qualified_import module_name = 377 semicolon [str "import qualified", str module_name]; 378 val import_common_ps = 379 enclose "import Prelude (" ");" (commas (map str 380 (map (Library.enclose "(" ")") prelude_import_operators @ prelude_import_unqualified) 381 @ map (fn (tyco, constrs) => (enclose (tyco ^ "(") ")" o commas o map str) constrs) prelude_import_unqualified_constr)) 382 :: print_qualified_import "Prelude" 383 :: map (print_qualified_import o fst) includes; 384 fun print_module module_name (gr, imports) = 385 let 386 val deresolve = deresolver module_name; 387 val deresolve_import = SOME o str o deresolve; 388 val deresolve_import_attached = SOME o str o suffix "(..)" o deresolve; 389 fun print_import (sym, (_, Code_Thingol.Fun _)) = deresolve_import sym 390 | print_import (sym, (Code_Namespace.Public, Code_Thingol.Datatype _)) = deresolve_import_attached sym 391 | print_import (sym, (Code_Namespace.Opaque, Code_Thingol.Datatype _)) = deresolve_import sym 392 | print_import (sym, (Code_Namespace.Public, Code_Thingol.Class _)) = deresolve_import_attached sym 393 | print_import (sym, (Code_Namespace.Opaque, Code_Thingol.Class _)) = deresolve_import sym 394 | print_import (sym, (_, Code_Thingol.Classinst _)) = NONE; 395 val import_ps = import_common_ps @ map (print_qualified_import o fst) imports; 396 fun print_stmt' sym = case Code_Symbol.Graph.get_node gr sym 397 of (_, NONE) => NONE 398 | (_, SOME (export, stmt)) => 399 SOME (if Code_Namespace.not_private export then print_import (sym, (export, stmt)) else NONE, markup_stmt sym (print_stmt deresolve (sym, stmt))); 400 val (export_ps, body_ps) = (flat o rev o Code_Symbol.Graph.strong_conn) gr 401 |> map_filter print_stmt' 402 |> split_list 403 |> apfst (map_filter I); 404 in 405 print_module_frame module_name [str language_pragma] (SOME export_ps) 406 ((if null import_ps then [] else [Pretty.chunks import_ps]) @ body_ps) 407 end; 408 409 in 410 (Code_Target.Hierarchy (map (fn (module_name, content) => ([module_name ^ ".hs"], content)) includes 411 @ map (fn module_name => print_module module_name (Graph.get_node haskell_program module_name)) 412 ((flat o rev o Graph.strong_conn) haskell_program)), try (deresolver "")) 413 end; 414 415val serializer : Code_Target.serializer = 416 Code_Target.parse_args (Scan.optional (Args.$$$ "root" -- Args.colon |-- Args.name) "" 417 -- Scan.optional (Args.$$$ "string_classes" >> K true) false 418 >> (fn (module_prefix, string_classes) => 419 serialize_haskell module_prefix string_classes)); 420 421fun print_numeral typ = Library.enclose "(" (" :: " ^ typ ^ ")") o signed_string_of_int; 422 423val literals = Literals { 424 literal_string = print_haskell_string, 425 literal_numeral = print_numeral "Integer", 426 literal_list = enum "," "[" "]", 427 infix_cons = (5, ":") 428}; 429 430 431(** optional monad syntax **) 432 433fun pretty_haskell_monad c_bind = 434 let 435 fun dest_bind t1 t2 = case Code_Thingol.split_pat_abs t2 436 of SOME ((pat, ty), t') => 437 SOME ((SOME ((pat, ty), true), t1), t') 438 | NONE => NONE; 439 fun dest_monad (IConst { sym = Constant c, ... } `$ t1 `$ t2) = 440 if c = c_bind then dest_bind t1 t2 441 else NONE 442 | dest_monad t = case Code_Thingol.split_let_no_pat t 443 of SOME (((some_v, ty), tbind), t') => 444 SOME ((SOME ((IVar some_v, ty), false), tbind), t') 445 | NONE => NONE; 446 val implode_monad = Code_Thingol.unfoldr dest_monad; 447 fun print_monad print_bind print_term (NONE, t) vars = 448 (semicolon [print_term vars NOBR t], vars) 449 | print_monad print_bind print_term (SOME ((bind, _), true), t) vars = vars 450 |> print_bind NOBR bind 451 |>> (fn p => semicolon [p, str "<-", print_term vars NOBR t]) 452 | print_monad print_bind print_term (SOME ((bind, _), false), t) vars = vars 453 |> print_bind NOBR bind 454 |>> (fn p => semicolon [str "let", str "{", p, str "=", print_term vars NOBR t, str "}"]); 455 fun pretty _ print_term thm vars fxy [(t1, _), (t2, _)] = case dest_bind t1 t2 456 of SOME (bind, t') => let 457 val (binds, t'') = implode_monad t' 458 val (ps, vars') = fold_map (print_monad (gen_print_bind (K print_term) thm) print_term) 459 (bind :: binds) vars; 460 in 461 brackify_block fxy (str "do { ") 462 (ps @| print_term vars' NOBR t'') 463 (str " }") 464 end 465 | NONE => brackify_infix (1, L) fxy 466 (print_term vars (INFX (1, L)) t1, str ">>=", print_term vars (INFX (1, X)) t2) 467 in (2, pretty) end; 468 469fun add_monad target' raw_c_bind thy = 470 let 471 val c_bind = Code.read_const thy raw_c_bind; 472 in 473 if target = target' then 474 thy 475 |> Code_Target.set_printings (Constant (c_bind, [(target, 476 SOME (Code_Printer.complex_const_syntax (pretty_haskell_monad c_bind)))])) 477 else error "Only Haskell target allows for monad syntax" 478 end; 479 480 481(** Isar setup **) 482 483val _ = Theory.setup 484 (Code_Target.add_language 485 (target, {serializer = serializer, literals = literals, 486 check = { env_var = "ISABELLE_GHC", make_destination = I, 487 make_command = fn module_name => 488 "\"$ISABELLE_GHC\" " ^ language_params ^ " -odir build -hidir build -stubdir build -e \"\" " ^ 489 module_name ^ ".hs"}, 490 evaluation_args = []}) 491 #> Code_Target.set_printings (Type_Constructor ("fun", 492 [(target, SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] => 493 brackify_infix (1, R) fxy ( 494 print_typ (INFX (1, X)) ty1, 495 str "->", 496 print_typ (INFX (1, R)) ty2 497 )))])) 498 #> fold (Code_Target.add_reserved target) [ 499 "hiding", "deriving", "where", "case", "of", "infix", "infixl", "infixr", 500 "import", "default", "forall", "let", "in", "class", "qualified", "data", 501 "newtype", "instance", "if", "then", "else", "type", "as", "do", "module" 502 ] 503 #> fold (Code_Target.add_reserved target) prelude_import_unqualified 504 #> fold (Code_Target.add_reserved target o fst) prelude_import_unqualified_constr 505 #> fold (fold (Code_Target.add_reserved target) o snd) prelude_import_unqualified_constr); 506 507val _ = 508 Outer_Syntax.command \<^command_keyword>\<open>code_monad\<close> "define code syntax for monads" 509 (Parse.term -- Parse.name >> (fn (raw_bind, target) => 510 Toplevel.theory (add_monad target raw_bind))); 511 512end; (*struct*) 513