haftmann@37744: (* Title: Tools/Code/code_haskell.ML haftmann@28054: Author: Florian Haftmann, TU Muenchen haftmann@28054: haftmann@28054: Serializer for Haskell. haftmann@28054: *) haftmann@28054: haftmann@28054: signature CODE_HASKELL = haftmann@28054: sig haftmann@37744: val target: string haftmann@28054: val setup: theory -> theory haftmann@28054: end; haftmann@28054: haftmann@28054: structure Code_Haskell : CODE_HASKELL = haftmann@28054: struct haftmann@28054: haftmann@28054: val target = "Haskell"; haftmann@28054: haftmann@28054: open Basic_Code_Thingol; haftmann@28054: open Code_Printer; haftmann@28054: haftmann@28054: infixr 5 @@; haftmann@28054: infixr 5 @|; haftmann@28054: haftmann@28054: haftmann@28054: (** Haskell serializer **) haftmann@28054: haftmann@39149: fun print_haskell_stmt labelled_name class_syntax tyco_syntax const_syntax haftmann@32924: reserved deresolve contr_classparam_typs deriving_show = haftmann@28054: let haftmann@39149: fun class_name class = case class_syntax class haftmann@28054: of NONE => deresolve class haftmann@28687: | SOME class => class; haftmann@33988: fun print_typcontext tyvars vs = case maps (fn (v, sort) => map (pair v) sort) vs haftmann@28054: of [] => [] haftmann@37359: | constraints => enum "," "(" ")" ( haftmann@28054: map (fn (v, class) => haftmann@37359: str (class_name class ^ " " ^ lookup_var tyvars v)) constraints) haftmann@28054: @@ str " => "; haftmann@33988: fun print_typforall tyvars vs = case map fst vs haftmann@28054: of [] => [] haftmann@28054: | vnames => str "forall " :: Pretty.breaks haftmann@32924: (map (str o lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1; haftmann@33988: fun print_tyco_expr tyvars fxy (tyco, tys) = haftmann@33988: brackify fxy (str tyco :: map (print_typ tyvars BR) tys) haftmann@39149: and print_typ tyvars fxy (tycoexpr as tyco `%% tys) = (case tyco_syntax tyco haftmann@33988: of NONE => print_tyco_expr tyvars fxy (deresolve tyco, tys) haftmann@33988: | SOME (i, print) => print (print_typ tyvars) fxy tys) haftmann@33988: | print_typ tyvars fxy (ITyVar v) = (str o lookup_var tyvars) v; haftmann@33988: fun print_typdecl tyvars (vs, tycoexpr) = haftmann@33988: Pretty.block (print_typcontext tyvars vs @| print_tyco_expr tyvars NOBR tycoexpr); haftmann@33988: fun print_typscheme tyvars (vs, ty) = haftmann@33988: Pretty.block (print_typforall tyvars vs @ print_typcontext tyvars vs @| print_typ tyvars NOBR ty); haftmann@35228: fun print_term tyvars some_thm vars fxy (IConst c) = haftmann@35228: print_app tyvars some_thm vars fxy (c, []) haftmann@35228: | print_term tyvars some_thm vars fxy (t as (t1 `$ t2)) = haftmann@28054: (case Code_Thingol.unfold_const_app t haftmann@35228: of SOME app => print_app tyvars some_thm vars fxy app haftmann@28054: | _ => haftmann@28054: brackify fxy [ haftmann@35228: print_term tyvars some_thm vars NOBR t1, haftmann@35228: print_term tyvars some_thm vars BR t2 haftmann@28054: ]) haftmann@35228: | print_term tyvars some_thm vars fxy (IVar NONE) = haftmann@31889: str "_" haftmann@35228: | print_term tyvars some_thm vars fxy (IVar (SOME v)) = haftmann@32924: (str o lookup_var vars) v haftmann@35228: | print_term tyvars some_thm vars fxy (t as _ `|=> _) = haftmann@28054: let haftmann@31873: val (binds, t') = Code_Thingol.unfold_pat_abs t; haftmann@35228: val (ps, vars') = fold_map (print_bind tyvars some_thm BR o fst) binds vars; haftmann@35228: in brackets (str "\\" :: ps @ str "->" @@ print_term tyvars some_thm vars' NOBR t') end haftmann@35228: | print_term tyvars some_thm vars fxy (ICase (cases as (_, t0))) = haftmann@28054: (case Code_Thingol.unfold_const_app t0 haftmann@39149: of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c) haftmann@35228: then print_case tyvars some_thm vars fxy cases haftmann@35228: else print_app tyvars some_thm vars fxy c_ts haftmann@35228: | NONE => print_case tyvars some_thm vars fxy cases) bulwahn@45656: and print_app_expr tyvars some_thm vars ((c, ((_, function_typs), _)), ts) = case contr_classparam_typs c haftmann@35228: of [] => (str o deresolve) c :: map (print_term tyvars some_thm vars BR) ts haftmann@28054: | fingerprint => let haftmann@33956: val ts_fingerprint = ts ~~ take (length ts) fingerprint; haftmann@28054: val needs_annotation = forall (fn (_, NONE) => true | (t, SOME _) => haftmann@28054: (not o Code_Thingol.locally_monomorphic) t) ts_fingerprint; haftmann@35228: fun print_term_anno (t, NONE) _ = print_term tyvars some_thm vars BR t haftmann@33988: | print_term_anno (t, SOME _) ty = haftmann@35228: brackets [print_term tyvars some_thm vars NOBR t, str "::", print_typ tyvars NOBR ty]; haftmann@28054: in haftmann@28054: if needs_annotation then haftmann@37424: (str o deresolve) c :: map2 print_term_anno ts_fingerprint (take (length ts) function_typs) haftmann@35228: else (str o deresolve) c :: map (print_term tyvars some_thm vars BR) ts haftmann@28054: end haftmann@39149: and print_app tyvars = gen_print_app (print_app_expr tyvars) (print_term tyvars) const_syntax haftmann@35228: and print_bind tyvars some_thm fxy p = gen_print_bind (print_term tyvars) some_thm fxy p haftmann@35228: and print_case tyvars some_thm vars fxy (cases as ((_, [_]), _)) = haftmann@28054: let haftmann@29889: val (binds, body) = Code_Thingol.unfold_let (ICase cases); haftmann@33988: fun print_match ((pat, ty), t) vars = haftmann@28054: vars haftmann@35228: |> print_bind tyvars some_thm BR pat haftmann@35228: |>> (fn p => semicolon [p, str "=", print_term tyvars some_thm vars NOBR t]) haftmann@33988: val (ps, vars') = fold_map print_match binds vars; haftmann@31665: in brackify_block fxy (str "let {") haftmann@31665: ps haftmann@35228: (concat [str "}", str "in", print_term tyvars some_thm vars' NOBR body]) haftmann@28054: end haftmann@35228: | print_case tyvars some_thm vars fxy (((t, ty), clauses as _ :: _), _) = haftmann@28054: let haftmann@33988: fun print_select (pat, body) = haftmann@28054: let haftmann@35228: val (p, vars') = print_bind tyvars some_thm NOBR pat vars; haftmann@35228: in semicolon [p, str "->", print_term tyvars some_thm vars' NOBR body] end; haftmann@36574: in Pretty.block_enclose haftmann@36574: (concat [str "(case", print_term tyvars some_thm vars NOBR t, str "of", str "{"], str "})") haftmann@33988: (map print_select clauses) haftmann@28054: end haftmann@35228: | print_case tyvars some_thm vars fxy ((_, []), _) = haftmann@31376: (brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""]; haftmann@37412: fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) = haftmann@28054: let haftmann@32924: val tyvars = intro_vars (map fst vs) reserved; haftmann@34262: fun print_err n = haftmann@33988: semicolon ( haftmann@39437: (str o deresolve) name haftmann@28054: :: map str (replicate n "_") haftmann@28054: @ str "=" haftmann@28054: :: str "error" haftmann@33988: @@ (str o ML_Syntax.print_string wenzelm@30364: o Long_Name.base_name o Long_Name.qualifier) name haftmann@34262: ); haftmann@35228: fun print_eqn ((ts, t), (some_thm, _)) = haftmann@28054: let haftmann@32913: val consts = fold Code_Thingol.add_constnames (t :: ts) []; haftmann@32924: val vars = reserved haftmann@32924: |> intro_base_names haftmann@39149: (is_none o const_syntax) deresolve consts haftmann@32924: |> intro_vars ((fold o Code_Thingol.fold_varnames) haftmann@32925: (insert (op =)) ts []); haftmann@28054: in haftmann@28054: semicolon ( haftmann@39437: (str o deresolve) name haftmann@35228: :: map (print_term tyvars some_thm vars BR) ts haftmann@28054: @ str "=" haftmann@35228: @@ print_term tyvars some_thm vars NOBR t haftmann@28054: ) haftmann@28054: end; haftmann@28054: in haftmann@28054: Pretty.chunks ( haftmann@33988: semicolon [ haftmann@39437: (str o suffix " ::" o deresolve) name, haftmann@33988: print_typscheme tyvars (vs, ty) haftmann@28054: ] haftmann@34262: :: (case filter (snd o snd) raw_eqs haftmann@34262: of [] => [print_err ((length o fst o Code_Thingol.unfold_fun) ty)] haftmann@34262: | eqs => map print_eqn eqs) haftmann@28054: ) haftmann@28054: end haftmann@33988: | print_stmt (name, Code_Thingol.Datatype (_, (vs, []))) = haftmann@28054: let haftmann@32924: val tyvars = intro_vars (map fst vs) reserved; haftmann@28054: in haftmann@28054: semicolon [ haftmann@28054: str "data", haftmann@39437: print_typdecl tyvars (vs, (deresolve name, map (ITyVar o fst) vs)) haftmann@28054: ] haftmann@28054: end haftmann@37424: | print_stmt (name, Code_Thingol.Datatype (_, (vs, [((co, _), [ty])]))) = haftmann@28054: let haftmann@32924: val tyvars = intro_vars (map fst vs) reserved; haftmann@28054: in haftmann@28054: semicolon ( haftmann@28054: str "newtype" haftmann@39437: :: print_typdecl tyvars (vs, (deresolve name, map (ITyVar o fst) vs)) haftmann@28054: :: str "=" haftmann@39437: :: (str o deresolve) co haftmann@33988: :: print_typ tyvars BR ty haftmann@28054: :: (if deriving_show name then [str "deriving (Read, Show)"] else []) haftmann@28054: ) haftmann@28054: end haftmann@33988: | print_stmt (name, Code_Thingol.Datatype (_, (vs, co :: cos))) = haftmann@28054: let haftmann@32924: val tyvars = intro_vars (map fst vs) reserved; haftmann@37424: fun print_co ((co, _), tys) = haftmann@28054: concat ( haftmann@39437: (str o deresolve) co haftmann@33988: :: map (print_typ tyvars BR) tys haftmann@28054: ) haftmann@28054: in haftmann@28054: semicolon ( haftmann@28054: str "data" haftmann@39437: :: print_typdecl tyvars (vs, (deresolve name, map (ITyVar o fst) vs)) haftmann@28054: :: str "=" haftmann@33988: :: print_co co haftmann@33988: :: map ((fn p => Pretty.block [str "| ", p]) o print_co) cos haftmann@28054: @ (if deriving_show name then [str "deriving (Read, Show)"] else []) haftmann@28054: ) haftmann@28054: end haftmann@37422: | print_stmt (name, Code_Thingol.Class (_, (v, (super_classes, classparams)))) = haftmann@28054: let haftmann@32924: val tyvars = intro_vars [v] reserved; haftmann@33988: fun print_classparam (classparam, ty) = haftmann@28054: semicolon [ haftmann@39437: (str o deresolve) classparam, haftmann@28054: str "::", haftmann@33988: print_typ tyvars NOBR ty haftmann@28054: ] haftmann@28054: in haftmann@28054: Pretty.block_enclose ( haftmann@28054: Pretty.block [ haftmann@28054: str "class ", haftmann@37359: Pretty.block (print_typcontext tyvars [(v, map fst super_classes)]), haftmann@39437: str (deresolve name ^ " " ^ lookup_var tyvars v), haftmann@28054: str " where {" haftmann@28054: ], haftmann@28054: str "};" haftmann@33988: ) (map print_classparam classparams) haftmann@28054: end haftmann@37424: | print_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, (classparam_instances, _)))) = haftmann@28054: let haftmann@32924: val tyvars = intro_vars (map fst vs) reserved; haftmann@39149: fun requires_args classparam = case const_syntax classparam haftmann@39437: of NONE => NONE haftmann@39437: | SOME (Code_Printer.Plain_const_syntax _) => SOME 0 haftmann@39437: | SOME (Code_Printer.Complex_const_syntax (k,_ )) => SOME k; haftmann@37854: fun print_classparam_instance ((classparam, const), (thm, _)) = haftmann@37854: case requires_args classparam haftmann@39437: of NONE => semicolon [ haftmann@39437: (str o Long_Name.base_name o deresolve) classparam, haftmann@28687: str "=", haftmann@37854: print_app tyvars (SOME thm) reserved NOBR (const, []) haftmann@28687: ] haftmann@39437: | SOME k => haftmann@37854: let bulwahn@45656: val (c, ((_, tys), _)) = const; (* FIXME: pass around the need annotation flag here? *) haftmann@37854: val (vs, rhs) = (apfst o map) fst haftmann@37854: (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, []))); haftmann@39149: val s = if (is_some o const_syntax) c haftmann@37854: then NONE else (SOME o Long_Name.base_name o deresolve) c; haftmann@37854: val vars = reserved haftmann@37854: |> intro_vars (map_filter I (s :: vs)); bulwahn@45656: val lhs = IConst (classparam, ((([], []), tys), false (* FIXME *))) `$$ map IVar vs; haftmann@37854: (*dictionaries are not relevant at this late stage*) haftmann@37854: in haftmann@37854: semicolon [ haftmann@37854: print_term tyvars (SOME thm) vars NOBR lhs, haftmann@37854: str "=", haftmann@37854: print_term tyvars (SOME thm) vars NOBR rhs haftmann@37854: ] haftmann@37854: end; haftmann@28054: in haftmann@28054: Pretty.block_enclose ( haftmann@28054: Pretty.block [ haftmann@28054: str "instance ", haftmann@33988: Pretty.block (print_typcontext tyvars vs), haftmann@28054: str (class_name class ^ " "), haftmann@33988: print_typ tyvars BR (tyco `%% map (ITyVar o fst) vs), haftmann@28054: str " where {" haftmann@28054: ], haftmann@28054: str "};" haftmann@37359: ) (map print_classparam_instance classparam_instances) haftmann@28054: end; haftmann@33988: in print_stmt end; haftmann@28054: haftmann@39432: fun haskell_program_of_program labelled_name module_alias module_prefix reserved = haftmann@39432: let haftmann@39432: fun namify_fun upper base (nsp_fun, nsp_typ) = haftmann@39432: let wenzelm@44208: val (base', nsp_fun') = wenzelm@44208: Name.variant (if upper then first_upper base else base) nsp_fun; haftmann@39432: in (base', (nsp_fun', nsp_typ)) end; haftmann@39432: fun namify_typ base (nsp_fun, nsp_typ) = haftmann@39432: let wenzelm@44208: val (base', nsp_typ') = Name.variant (first_upper base) nsp_typ; haftmann@39432: in (base', (nsp_fun, nsp_typ')) end; haftmann@39432: fun namify_stmt (Code_Thingol.Fun (_, (_, SOME _))) = pair haftmann@39432: | namify_stmt (Code_Thingol.Fun _) = namify_fun false haftmann@39432: | namify_stmt (Code_Thingol.Datatype _) = namify_typ haftmann@39432: | namify_stmt (Code_Thingol.Datatypecons _) = namify_fun true haftmann@39432: | namify_stmt (Code_Thingol.Class _) = namify_typ haftmann@39432: | namify_stmt (Code_Thingol.Classrel _) = pair haftmann@39432: | namify_stmt (Code_Thingol.Classparam _) = namify_fun false haftmann@39432: | namify_stmt (Code_Thingol.Classinst _) = pair; haftmann@39432: fun select_stmt (Code_Thingol.Fun (_, (_, SOME _))) = false haftmann@39432: | select_stmt (Code_Thingol.Fun _) = true haftmann@39432: | select_stmt (Code_Thingol.Datatype _) = true haftmann@39432: | select_stmt (Code_Thingol.Datatypecons _) = false haftmann@39432: | select_stmt (Code_Thingol.Class _) = true haftmann@39432: | select_stmt (Code_Thingol.Classrel _) = false haftmann@39432: | select_stmt (Code_Thingol.Classparam _) = false haftmann@39432: | select_stmt (Code_Thingol.Classinst _) = true; haftmann@39432: in haftmann@39436: Code_Namespace.flat_program labelled_name haftmann@39432: { module_alias = module_alias, module_prefix = module_prefix, haftmann@39432: reserved = reserved, empty_nsp = (reserved, reserved), namify_stmt = namify_stmt, haftmann@39432: modify_stmt = fn stmt => if select_stmt stmt then SOME stmt else NONE } haftmann@39432: end; haftmann@39432: haftmann@39381: fun serialize_haskell module_prefix string_classes { labelled_name, reserved_syms, haftmann@41591: includes, module_alias, class_syntax, tyco_syntax, const_syntax } program = haftmann@28054: let haftmann@39434: haftmann@39434: (* build program *) haftmann@39152: val reserved = fold (insert (op =) o fst) includes reserved_syms; haftmann@39434: val { deresolver, flat_program = haskell_program } = haskell_program_of_program haftmann@39434: labelled_name module_alias module_prefix (Name.make_context reserved) program; haftmann@39434: haftmann@39434: (* print statements *) haftmann@28054: val contr_classparam_typs = Code_Thingol.contr_classparam_typs program; haftmann@28054: fun deriving_show tyco = haftmann@28054: let haftmann@28054: fun deriv _ "fun" = false haftmann@34085: | deriv tycos tyco = not (tyco = Code_Thingol.fun_tyco) haftmann@34085: andalso (member (op =) tycos tyco haftmann@34085: orelse case try (Graph.get_node program) tyco haftmann@28663: of SOME (Code_Thingol.Datatype (_, (_, cs))) => forall (deriv' (tyco :: tycos)) haftmann@28054: (maps snd cs) haftmann@34085: | NONE => true) haftmann@28054: and deriv' tycos (tyco `%% tys) = deriv tycos tyco haftmann@28054: andalso forall (deriv' tycos) tys haftmann@28054: | deriv' _ (ITyVar _) = true haftmann@28054: in deriv [] tyco end; haftmann@39434: fun print_stmt deresolve = print_haskell_stmt labelled_name haftmann@39434: class_syntax tyco_syntax const_syntax (make_vars reserved) haftmann@39434: deresolve contr_classparam_typs haftmann@28054: (if string_classes then deriving_show else K false); haftmann@39434: haftmann@39434: (* print modules *) haftmann@39434: val import_includes_ps = haftmann@39434: map (fn (name, _) => str ("import qualified " ^ name ^ ";")) includes; haftmann@39434: fun print_module_frame module_name ps = haftmann@39434: (module_name, Pretty.chunks2 ( haftmann@39439: str ("module " ^ module_name ^ " where {") haftmann@39434: :: ps haftmann@39434: @| str "}" haftmann@39434: )); haftmann@39434: fun print_module module_name (gr, imports) = haftmann@28054: let haftmann@39434: val deresolve = deresolver module_name haftmann@39434: fun print_import module_name = (semicolon o map str) ["import qualified", module_name]; haftmann@39434: val import_ps = import_includes_ps @ map (print_import o fst) imports; haftmann@39434: fun print_stmt' gr name = case Graph.get_node gr name haftmann@39434: of (_, NONE) => NONE haftmann@39434: | (_, SOME stmt) => SOME (markup_stmt name (print_stmt deresolve (name, stmt))); haftmann@39434: val body_ps = map_filter (print_stmt' gr) ((flat o rev o Graph.strong_conn) gr); haftmann@39434: in haftmann@39434: print_module_frame module_name haftmann@39434: ((if null import_ps then [] else [Pretty.chunks import_ps]) @ body_ps) haftmann@39434: end; haftmann@39434: haftmann@39434: (*serialization*) haftmann@39434: fun write_module width (SOME destination) (module_name, content) = haftmann@39141: let wenzelm@42874: val _ = File.check_dir destination; haftmann@39434: val filepath = (Path.append destination o Path.ext "hs" o Path.explode o implode haftmann@39434: o separate "/" o Long_Name.explode) module_name; haftmann@41487: val _ = Isabelle_System.mkdirs (Path.dir filepath); haftmann@39439: in haftmann@39439: (File.write filepath o format [] width o Pretty.chunks2) haftmann@41050: [str "{-# LANGUAGE ScopedTypeVariables #-}", content] haftmann@39439: end haftmann@39290: | write_module width NONE (_, content) = writeln (format [] width content); haftmann@28054: in haftmann@39142: Code_Target.serialization haftmann@39141: (fn width => fn destination => K () o map (write_module width destination)) haftmann@40953: (fn present => fn width => rpair (try (deresolver "")) haftmann@39434: o format present width o Pretty.chunks o map snd) haftmann@39434: (map (uncurry print_module_frame o apsnd single) includes haftmann@39434: @ map (fn module_name => print_module module_name (Graph.get_node haskell_program module_name)) haftmann@39434: ((flat o rev o Graph.strong_conn) haskell_program)) haftmann@28054: end; haftmann@28054: haftmann@39192: val serializer : Code_Target.serializer = haftmann@39436: Code_Target.parse_args (Scan.optional (Args.$$$ "root" -- Args.colon |-- Args.name) "" haftmann@39192: -- Scan.optional (Args.$$$ "string_classes" >> K true) false haftmann@39192: >> (fn (module_prefix, string_classes) => haftmann@39192: serialize_haskell module_prefix string_classes)); haftmann@39192: haftmann@28064: val literals = let haftmann@28064: fun char_haskell c = haftmann@28064: let haftmann@28064: val s = ML_Syntax.print_char c; haftmann@28064: in if s = "'" then "\\'" else s end; haftmann@34931: fun numeral_haskell k = if k >= 0 then string_of_int k haftmann@34931: else Library.enclose "(" ")" (signed_string_of_int k); haftmann@28064: in Literals { haftmann@34178: literal_char = Library.enclose "'" "'" o char_haskell, haftmann@28064: literal_string = quote o translate_string char_haskell, haftmann@34931: literal_numeral = numeral_haskell, haftmann@34931: literal_positive_numeral = numeral_haskell, haftmann@38195: literal_alternative_numeral = numeral_haskell, haftmann@34931: literal_naive_numeral = numeral_haskell, haftmann@34178: literal_list = enum "," "[" "]", haftmann@28064: infix_cons = (5, ":") haftmann@28064: } end; haftmann@28064: haftmann@28054: haftmann@28054: (** optional monad syntax **) haftmann@28054: haftmann@28054: fun pretty_haskell_monad c_bind = haftmann@28054: let haftmann@31873: fun dest_bind t1 t2 = case Code_Thingol.split_pat_abs t2 haftmann@31889: of SOME ((pat, ty), t') => haftmann@31889: SOME ((SOME ((pat, ty), true), t1), t') haftmann@28145: | NONE => NONE; haftmann@28663: fun dest_monad c_bind_name (IConst (c, _) `$ t1 `$ t2) = haftmann@28663: if c = c_bind_name then dest_bind t1 t2 haftmann@28145: else NONE haftmann@28663: | dest_monad _ t = case Code_Thingol.split_let t haftmann@28145: of SOME (((pat, ty), tbind), t') => haftmann@31889: SOME ((SOME ((pat, ty), false), tbind), t') haftmann@28145: | NONE => NONE; haftmann@28663: fun implode_monad c_bind_name = Code_Thingol.unfoldr (dest_monad c_bind_name); haftmann@33988: fun print_monad print_bind print_term (NONE, t) vars = haftmann@33988: (semicolon [print_term vars NOBR t], vars) haftmann@33988: | print_monad print_bind print_term (SOME ((bind, _), true), t) vars = vars haftmann@33988: |> print_bind NOBR bind haftmann@33988: |>> (fn p => semicolon [p, str "<-", print_term vars NOBR t]) haftmann@33988: | print_monad print_bind print_term (SOME ((bind, _), false), t) vars = vars haftmann@33988: |> print_bind NOBR bind haftmann@37832: |>> (fn p => semicolon [str "let", str "{", p, str "=", print_term vars NOBR t, str "}"]); haftmann@33988: fun pretty _ [c_bind'] print_term thm vars fxy [(t1, _), (t2, _)] = case dest_bind t1 t2 haftmann@28145: of SOME (bind, t') => let haftmann@31054: val (binds, t'') = implode_monad c_bind' t' haftmann@33988: val (ps, vars') = fold_map (print_monad (gen_print_bind (K print_term) thm) print_term) haftmann@33988: (bind :: binds) vars; haftmann@33988: in haftmann@37833: (brackify fxy o single o enclose "do { " " }" o Pretty.breaks) haftmann@33988: (ps @| print_term vars' NOBR t'') haftmann@33988: end haftmann@28145: | NONE => brackify_infix (1, L) fxy haftmann@37239: (print_term vars (INFX (1, L)) t1, str ">>=", print_term vars (INFX (1, X)) t2) haftmann@31054: in (2, ([c_bind], pretty)) end; haftmann@28054: haftmann@28145: fun add_monad target' raw_c_bind thy = haftmann@28054: let haftmann@31156: val c_bind = Code.read_const thy raw_c_bind; haftmann@28054: in if target = target' then haftmann@28054: thy haftmann@39149: |> Code_Target.add_const_syntax target c_bind haftmann@37854: (SOME (Code_Printer.complex_const_syntax (pretty_haskell_monad c_bind))) haftmann@28054: else error "Only Haskell target allows for monad syntax" end; haftmann@28054: haftmann@28054: haftmann@28054: (** Isar setup **) haftmann@28054: haftmann@28054: val _ = wenzelm@36970: Outer_Syntax.command "code_monad" "define code syntax for monads" Keyword.thy_decl ( wenzelm@36970: Parse.term_group -- Parse.name >> (fn (raw_bind, target) => haftmann@28145: Toplevel.theory (add_monad target raw_bind)) haftmann@28054: ); haftmann@28054: haftmann@28054: val setup = haftmann@37821: Code_Target.add_target haftmann@39192: (target, { serializer = serializer, literals = literals, wenzelm@42823: check = { env_var = "ISABELLE_GHC", make_destination = I, wenzelm@42811: make_command = fn module_name => noschinl@45192: "\"$ISABELLE_GHC\" -XRankNTypes -XScopedTypeVariables -odir build -hidir build -stubdir build -e \"\" " ^ wenzelm@42811: module_name ^ ".hs" } }) haftmann@39149: #> Code_Target.add_tyco_syntax target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] => haftmann@37239: brackify_infix (1, R) fxy ( haftmann@33988: print_typ (INFX (1, X)) ty1, haftmann@28054: str "->", haftmann@33988: print_typ (INFX (1, R)) ty2 haftmann@37239: ))) haftmann@28054: #> fold (Code_Target.add_reserved target) [ haftmann@28054: "hiding", "deriving", "where", "case", "of", "infix", "infixl", "infixr", haftmann@28054: "import", "default", "forall", "let", "in", "class", "qualified", "data", haftmann@28054: "newtype", "instance", "if", "then", "else", "type", "as", "do", "module" haftmann@28054: ] haftmann@28054: #> fold (Code_Target.add_reserved target) [ haftmann@28054: "Prelude", "Main", "Bool", "Maybe", "Either", "Ordering", "Char", "String", "Int", haftmann@28054: "Integer", "Float", "Double", "Rational", "IO", "Eq", "Ord", "Enum", "Bounded", haftmann@28054: "Num", "Real", "Integral", "Fractional", "Floating", "RealFloat", "Monad", "Functor", haftmann@28054: "AlreadyExists", "ArithException", "ArrayException", "AssertionFailed", "AsyncException", haftmann@28054: "BlockedOnDeadMVar", "Deadlock", "Denormal", "DivideByZero", "DotNetException", "DynException", haftmann@28054: "Dynamic", "EOF", "EQ", "EmptyRec", "ErrorCall", "ExitException", "ExitFailure", haftmann@28054: "ExitSuccess", "False", "GT", "HeapOverflow", haftmann@28054: "IOError", "IOException", "IllegalOperation", haftmann@28054: "IndexOutOfBounds", "Just", "Key", "LT", "Left", "LossOfPrecision", "NoMethodError", haftmann@28054: "NoSuchThing", "NonTermination", "Nothing", "Obj", "OtherError", "Overflow", haftmann@28054: "PatternMatchFail", "PermissionDenied", "ProtocolError", "RecConError", "RecSelError", haftmann@28054: "RecUpdError", "ResourceBusy", "ResourceExhausted", "Right", "StackOverflow", haftmann@28054: "ThreadKilled", "True", "TyCon", "TypeRep", "UndefinedElement", "Underflow", haftmann@28054: "UnsupportedOperation", "UserError", "abs", "absReal", "acos", "acosh", "all", haftmann@28054: "and", "any", "appendFile", "asTypeOf", "asciiTab", "asin", "asinh", "atan", haftmann@28054: "atan2", "atanh", "basicIORun", "blockIO", "boundedEnumFrom", "boundedEnumFromThen", haftmann@28054: "boundedEnumFromThenTo", "boundedEnumFromTo", "boundedPred", "boundedSucc", "break", haftmann@28054: "catch", "catchException", "ceiling", "compare", "concat", "concatMap", "const", haftmann@28054: "cos", "cosh", "curry", "cycle", "decodeFloat", "denominator", "div", "divMod", haftmann@28054: "doubleToRatio", "doubleToRational", "drop", "dropWhile", "either", "elem", haftmann@28054: "emptyRec", "encodeFloat", "enumFrom", "enumFromThen", "enumFromThenTo", haftmann@28054: "enumFromTo", "error", "even", "exp", "exponent", "fail", "filter", "flip", haftmann@28054: "floatDigits", "floatProperFraction", "floatRadix", "floatRange", "floatToRational", haftmann@28054: "floor", "fmap", "foldl", "foldl'", "foldl1", "foldr", "foldr1", "fromDouble", haftmann@28054: "fromEnum", "fromEnum_0", "fromInt", "fromInteger", "fromIntegral", "fromObj", haftmann@28054: "fromRational", "fst", "gcd", "getChar", "getContents", "getLine", "head", haftmann@28054: "id", "inRange", "index", "init", "intToRatio", "interact", "ioError", "isAlpha", haftmann@28054: "isAlphaNum", "isDenormalized", "isDigit", "isHexDigit", "isIEEE", "isInfinite", haftmann@28054: "isLower", "isNaN", "isNegativeZero", "isOctDigit", "isSpace", "isUpper", "iterate", "iterate'", haftmann@28054: "last", "lcm", "length", "lex", "lexDigits", "lexLitChar", "lexmatch", "lines", "log", haftmann@28054: "logBase", "lookup", "loop", "map", "mapM", "mapM_", "max", "maxBound", "maximum", haftmann@28054: "maybe", "min", "minBound", "minimum", "mod", "negate", "nonnull", "not", "notElem", haftmann@28054: "null", "numerator", "numericEnumFrom", "numericEnumFromThen", "numericEnumFromThenTo", haftmann@28054: "numericEnumFromTo", "odd", "or", "otherwise", "pi", "pred", haftmann@28054: "print", "product", "properFraction", "protectEsc", "putChar", "putStr", "putStrLn", haftmann@28054: "quot", "quotRem", "range", "rangeSize", "rationalToDouble", "rationalToFloat", haftmann@28054: "rationalToRealFloat", "read", "readDec", "readField", "readFieldName", "readFile", haftmann@28054: "readFloat", "readHex", "readIO", "readInt", "readList", "readLitChar", "readLn", haftmann@28054: "readOct", "readParen", "readSigned", "reads", "readsPrec", "realFloatToRational", haftmann@28054: "realToFrac", "recip", "reduce", "rem", "repeat", "replicate", "return", "reverse", haftmann@28054: "round", "scaleFloat", "scanl", "scanl1", "scanr", "scanr1", "seq", "sequence", haftmann@28054: "sequence_", "show", "showChar", "showException", "showField", "showList", haftmann@28054: "showLitChar", "showParen", "showString", "shows", "showsPrec", "significand", haftmann@28054: "signum", "signumReal", "sin", "sinh", "snd", "span", "splitAt", "sqrt", "subtract", haftmann@28054: "succ", "sum", "tail", "take", "takeWhile", "takeWhile1", "tan", "tanh", "threadToIOResult", haftmann@28054: "throw", "toEnum", "toInt", "toInteger", "toObj", "toRational", "truncate", "uncurry", haftmann@28054: "undefined", "unlines", "unsafeCoerce", "unsafeIndex", "unsafeRangeSize", "until", "unwords", haftmann@28054: "unzip", "unzip3", "userError", "words", "writeFile", "zip", "zip3", "zipWith", "zipWith3" haftmann@28054: ] (*due to weird handling of ':', we can't do anything else than to import *all* prelude symbols*); haftmann@28054: haftmann@28054: end; (*struct*)