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