1.1 --- a/src/Pure/Tools/codegen_serializer.ML Tue Jan 17 10:26:50 2006 +0100
1.2 +++ b/src/Pure/Tools/codegen_serializer.ML Tue Jan 17 16:36:57 2006 +0100
1.3 @@ -8,24 +8,40 @@
1.4
1.5 signature CODEGEN_SERIALIZER =
1.6 sig
1.7 - type fixity;
1.8 - type 'a pretty_syntax = (int * fixity) * (Pretty.T list -> ('a -> Pretty.T) -> Pretty.T);
1.9 - type serializer = string -> (string -> CodegenThingol.itype pretty_syntax option)
1.10 - -> (string -> CodegenThingol.iexpr pretty_syntax option)
1.11 - -> string list option -> CodegenThingol.module -> Pretty.T;
1.12 - val parse_fixity: OuterParse.token list -> fixity * OuterParse.token list;
1.13 -
1.14 - val ml_from_thingol: string list list -> string -> string -> serializer;
1.15 - val haskell_from_thingol: string list list -> string -> string -> serializer;
1.16 + type 'a pretty_syntax;
1.17 + type serializer =
1.18 + string list list
1.19 + -> (string -> CodegenThingol.itype pretty_syntax option)
1.20 + * (string -> CodegenThingol.iexpr pretty_syntax option)
1.21 + -> string
1.22 + -> string list option
1.23 + -> CodegenThingol.module
1.24 + -> unit -> Pretty.T * unit;
1.25 + val parse_syntax: (string -> 'b -> 'a * 'b) -> OuterParse.token list ->
1.26 + ('b -> 'a pretty_syntax * 'b) * OuterParse.token list;
1.27 + val parse_targetdef: (string -> string) -> string -> string;
1.28 + val serializers: {
1.29 + ml: string * (string * string * string -> serializer),
1.30 + haskell: string * (string -> serializer)
1.31 + }
1.32 end;
1.33
1.34 structure CodegenSerializer: CODEGEN_SERIALIZER =
1.35 struct
1.36
1.37 -open CodegenThingol;
1.38 +open CodegenThingolOp;
1.39 +infix 8 `%%;
1.40 +infixr 6 `->;
1.41 +infixr 6 `-->;
1.42 +infix 4 `$;
1.43 +infix 4 `$$;
1.44 +infixr 5 `|->;
1.45 +infixr 5 `|-->;
1.46
1.47 (** generic serialization **)
1.48
1.49 +(* precedences *)
1.50 +
1.51 datatype lrx = L | R | X;
1.52
1.53 datatype fixity =
1.54 @@ -33,87 +49,219 @@
1.55 | NOBR
1.56 | INFX of (int * lrx);
1.57
1.58 -type 'a pretty_syntax = (int * fixity)
1.59 - * (Pretty.T list -> ('a -> Pretty.T) -> Pretty.T);
1.60 -type serializer = string -> (string -> CodegenThingol.itype pretty_syntax option)
1.61 - -> (string -> CodegenThingol.iexpr pretty_syntax option)
1.62 - -> string list option -> CodegenThingol.module -> Pretty.T;
1.63 +datatype 'a mixfix =
1.64 + Arg of fixity
1.65 + | Ignore
1.66 + | Pretty of Pretty.T
1.67 + | Quote of 'a;
1.68
1.69 -local
1.70 -
1.71 -open Scan;
1.72 -open OuterParse;
1.73 -
1.74 -in
1.75 -
1.76 -val parse_fixity = optional (
1.77 - $$$ "(" |-- (
1.78 - $$$ "atom" |-- pair NOBR
1.79 - || $$$ "infix" |-- nat >> (fn pr => INFX (pr, X))
1.80 - || $$$ "infixl" |-- nat >> (fn pr => INFX (pr, L))
1.81 - || $$$ "infixr" |-- nat >> (fn pr => INFX (pr, R))
1.82 - ) --| $$$ ")"
1.83 - ) BR;
1.84 -
1.85 -end; (* local *)
1.86 +type 'a pretty_syntax = (int * int) * (fixity -> (fixity -> 'a -> Pretty.T) -> 'a list -> Pretty.T);
1.87
1.88 fun eval_lrx L L = false
1.89 | eval_lrx R R = false
1.90 | eval_lrx _ _ = true;
1.91
1.92 -fun eval_br BR _ = true
1.93 - | eval_br NOBR _ = false
1.94 - | eval_br (INFX (pr1, lr1)) (INFX (pr2, lr2)) =
1.95 +fun eval_fxy BR _ = true
1.96 + | eval_fxy NOBR _ = false
1.97 + | eval_fxy (INFX (pr1, lr1)) (INFX (pr2, lr2)) =
1.98 pr1 > pr2
1.99 orelse pr1 = pr2
1.100 andalso eval_lrx lr1 lr2
1.101 - | eval_br (INFX _) _ = false;
1.102 + | eval_fxy (INFX _) _ = false;
1.103
1.104 -fun eval_br_postfix BR _ = false
1.105 - | eval_br_postfix NOBR _ = false
1.106 - | eval_br_postfix (INFX (pr1, lr1)) (INFX (pr2, lr2)) =
1.107 - pr1 > pr2
1.108 - orelse pr1 = pr2
1.109 - andalso eval_lrx lr1 lr2
1.110 - | eval_br_postfix (INFX _) _ = false;
1.111 +val str = setmp print_mode [] Pretty.str;
1.112
1.113 fun brackify _ [p] = p
1.114 | brackify true (ps as _::_) = Pretty.enclose "(" ")" (Pretty.breaks ps)
1.115 | brackify false (ps as _::_) = Pretty.block (Pretty.breaks ps);
1.116
1.117 -fun postify [] f = [f]
1.118 - | postify [p] f = [p, Pretty.brk 1, f]
1.119 - | postify (ps as _::_) f = [Pretty.list "(" ")" ps, Pretty.brk 1, f];
1.120 +fun from_app mk_app from_expr const_syntax fxy (f, es) =
1.121 + let
1.122 + fun mk NONE es =
1.123 + brackify (eval_fxy fxy BR) (mk_app f es)
1.124 + | mk (SOME ((i, k), pr)) es =
1.125 + let
1.126 + val (es1, es2) = splitAt (i, es);
1.127 + in
1.128 + brackify (eval_fxy fxy BR) (pr fxy from_expr es1 :: map (from_expr BR) es2)
1.129 + end;
1.130 + in mk (const_syntax f) es end;
1.131
1.132 -fun upper_first s =
1.133 +fun fillin_mixfix fxy_this ms fxy pr args =
1.134 let
1.135 - val (pr, b) = split_last (NameSpace.unpack s);
1.136 - val (c::cs) = String.explode b;
1.137 - in NameSpace.pack (pr @ [String.implode (Char.toUpper c :: cs)]) end;
1.138 + fun brackify true = Pretty.enclose "(" ")"
1.139 + | brackify false = Pretty.block;
1.140 + fun fillin [] [] =
1.141 + []
1.142 + | fillin (Arg fxy :: ms) (a :: args) =
1.143 + pr fxy a :: fillin ms args
1.144 + | fillin (Ignore :: ms) args =
1.145 + fillin ms args
1.146 + | fillin (Pretty p :: ms) args =
1.147 + p :: fillin ms args
1.148 + | fillin (Quote q :: ms) args =
1.149 + pr BR q :: fillin ms args;
1.150 + in brackify true (fillin ms args) (* (eval_fxy fxy_this fxy) *) end;
1.151
1.152 -fun lower_first s =
1.153 +
1.154 +(* user-defined syntax *)
1.155 +
1.156 +val (atomK, infixK, infixlK, infixrK) =
1.157 + ("atom", "infix", "infixl", "infixr");
1.158 +val _ = OuterSyntax.add_keywords ["atom", "infix", "infixl", "infixr"];
1.159 +
1.160 +fun parse_infix (fixity as INFX (i, x)) s =
1.161 let
1.162 - val (pr, b) = split_last (NameSpace.unpack s);
1.163 - val (c::cs) = String.explode b;
1.164 - in NameSpace.pack (pr @ [String.implode (Char.toLower c :: cs)]) end;
1.165 + val l = case x of L => fixity
1.166 + | _ => INFX (i, X);
1.167 + val r = case x of R => fixity
1.168 + | _ => INFX (i, X);
1.169 + in
1.170 + pair [Arg l, (Pretty o Pretty.brk) 1, (Pretty o str) s, (Pretty o Pretty.brk) 1, Arg r]
1.171 + end;
1.172
1.173 -fun code_from_primitive serializer_name (name, prim) =
1.174 - case AList.lookup (op =) prim serializer_name
1.175 - of NONE => error ("no primitive definition for " ^ quote name)
1.176 - | p => p;
1.177 +fun parse_mixfix reader s ctxt =
1.178 + let
1.179 + fun sym s = Scan.lift ($$ s);
1.180 + fun lift_reader ctxt s =
1.181 + ctxt
1.182 + |> reader s
1.183 + |-> (fn x => pair (Quote x));
1.184 + val sym_any = Scan.lift (Scan.one Symbol.not_eof);
1.185 + val parse = Scan.repeat (
1.186 + (sym "_" -- sym "_" >> K (Arg NOBR))
1.187 + || (sym "_" >> K (Arg BR))
1.188 + || (sym "?" >> K Ignore)
1.189 + || (sym "/" |-- Scan.repeat (sym " ") >> (Pretty o Pretty.brk o length))
1.190 + || Scan.depend (fn ctxt => $$ "{" |-- $$ "*" |-- Scan.repeat1
1.191 + ( $$ "'" |-- Scan.one Symbol.not_eof
1.192 + || Scan.unless ($$ "*" -- $$ "}") (Scan.one Symbol.not_eof)) --|
1.193 + $$ "*" --| $$ "}" >> (implode #> lift_reader ctxt #> swap))
1.194 + || (Scan.repeat1
1.195 + ( sym "'" |-- sym_any
1.196 + || Scan.unless (sym "_" || sym "?" || sym "/" || sym "{" |-- sym "*")
1.197 + sym_any) >> (Pretty o str o implode)));
1.198 + in case Scan.finite' Symbol.stopper parse (ctxt, Symbol.explode s)
1.199 + of (p, (ctxt, [])) => (p, ctxt)
1.200 + | _ => error ("Malformed mixfix annotation: " ^ quote s)
1.201 + end;
1.202 +
1.203 +fun parse_syntax_proto reader = OuterParse.$$$ "(" |-- (
1.204 + OuterParse.$$$ infixK |-- OuterParse.nat >> (fn i => (parse_infix (INFX (i, X)), INFX (i, X)))
1.205 + || OuterParse.$$$ infixlK |-- OuterParse.nat >> (fn i => (parse_infix (INFX (i, L)), INFX (i, L)))
1.206 + || OuterParse.$$$ infixrK |-- OuterParse.nat >> (fn i => (parse_infix (INFX (i, R)), INFX (i, R)))
1.207 + || OuterParse.$$$ atomK |-- pair (parse_mixfix reader, NOBR)
1.208 + || pair (parse_mixfix reader, BR)
1.209 + ) -- OuterParse.string --| OuterParse.$$$ ")" >> (fn ((p, fxy), s) => (p s, fxy));
1.210 +
1.211 +fun parse_syntax reader =
1.212 + let
1.213 + fun is_arg (Arg _) = true
1.214 + | is_arg Ignore = true
1.215 + | is_arg _ = false;
1.216 + fun mk fixity mfx =
1.217 + let
1.218 + val i = length (List.filter is_arg mfx)
1.219 + in ((i, i), fillin_mixfix fixity mfx) end;
1.220 + in
1.221 + parse_syntax_proto reader
1.222 + #-> (fn (mfx_reader, fixity) : ('Z -> 'Y mixfix list * 'Z) * fixity =>
1.223 + pair (mfx_reader #-> (fn mfx => pair (mk fixity mfx)))
1.224 + )
1.225 + end;
1.226 +
1.227 +fun newline_correct s =
1.228 + s
1.229 + |> Symbol.strip_blanks
1.230 + |> space_explode "\n"
1.231 + |> map (implode o (fn [] => []
1.232 + | (" "::xs) => xs
1.233 + | xs => xs) o explode)
1.234 + |> space_implode "\n";
1.235 +
1.236 +fun parse_named_quote resolv s =
1.237 + case Scan.finite Symbol.stopper (Scan.repeat (
1.238 + ($$ "`" |-- $$ "`")
1.239 + || ($$ "`" |-- Scan.repeat1 (Scan.unless ($$ "`") (Scan.one Symbol.not_eof))
1.240 + --| $$ "`" >> (resolv o implode))
1.241 + || Scan.repeat1
1.242 + (Scan.unless ($$ "`") (Scan.one Symbol.not_eof)) >> implode
1.243 + ) >> implode) (Symbol.explode s)
1.244 + of (p, []) => p
1.245 + | (p, ss) => error ("Malformed definition: " ^ quote p ^ " - " ^ commas ss);
1.246 +
1.247 +fun parse_targetdef resolv = parse_named_quote resolv o newline_correct;
1.248 +
1.249 +
1.250 +(* abstract serializer *)
1.251 +
1.252 +type serializer =
1.253 + string list list
1.254 + -> (string -> CodegenThingol.itype pretty_syntax option)
1.255 + * (string -> CodegenThingol.iexpr pretty_syntax option)
1.256 + -> string
1.257 + -> string list option
1.258 + -> CodegenThingol.module
1.259 + -> unit -> Pretty.T * unit;
1.260 +
1.261 +fun abstract_serializer preprocess (from_defs, from_module, validator)
1.262 + (target, (tyco_syntax, const_syntax)) (name_root, nspgrp) postprocess select module =
1.263 + let
1.264 + fun from_prim (name, prim) =
1.265 + case AList.lookup (op =) prim target
1.266 + of NONE => error ("no primitive definition for " ^ quote name)
1.267 + | SOME p => p;
1.268 + in
1.269 + module
1.270 + |> debug 3 (fn _ => "selecting submodule...")
1.271 + |> (if is_some select then (partof o the) select else I)
1.272 + |> tap (Pretty.writeln o pretty_deps)
1.273 + |> debug 3 (fn _ => "preprocessing...")
1.274 + |> preprocess
1.275 + |> debug 3 (fn _ => "serializing...")
1.276 + |> serialize (from_defs (from_prim, (tyco_syntax, const_syntax)))
1.277 + from_module validator nspgrp name_root
1.278 + |> postprocess
1.279 + end;
1.280 +
1.281 +fun abstract_validator keywords name =
1.282 + let
1.283 + fun replace_invalid c =
1.284 + if (Char.isAlphaNum o the o Char.fromString) c orelse c = "'"
1.285 + andalso not (NameSpace.separator = c)
1.286 + then c
1.287 + else "_"
1.288 + fun suffix_it name =
1.289 + name
1.290 + |> member (op =) keywords ? suffix "'"
1.291 + |> (fn name' => if name = name' then name else suffix_it name')
1.292 + in
1.293 + name
1.294 + |> translate_string replace_invalid
1.295 + |> suffix_it
1.296 + |> (fn name' => if name = name' then NONE else SOME name')
1.297 + end;
1.298 +
1.299 +fun postprocess_single_file path p =
1.300 + File.write (Path.unpack path) (Pretty.output p ^ "\n");
1.301 +
1.302 +fun parse_single_file serializer =
1.303 + OuterParse.name >> (fn path => serializer (postprocess_single_file path));
1.304 +
1.305
1.306
1.307 (** ML serializer **)
1.308
1.309 local
1.310
1.311 -fun ml_from_defs serializer_name tyco_syntax const_syntax is_dicttype resolv ds =
1.312 +fun ml_from_defs (is_cons, needs_type)
1.313 + (from_prim, (tyco_syntax, const_syntax)) resolv defs =
1.314 let
1.315 fun chunk_defs ps =
1.316 let
1.317 val (p_init, p_last) = split_last ps
1.318 in
1.319 - Pretty.chunks (p_init @ [Pretty.block ([p_last, Pretty.str ";"])])
1.320 + Pretty.chunks (p_init @ [Pretty.block ([p_last, str ";"])])
1.321 end;
1.322 fun ml_from_label s =
1.323 let
1.324 @@ -122,281 +270,160 @@
1.325 NameSpace.pack (Library.drop (length s' - 2, s'))
1.326 |> translate_string (fn "_" => "__" | "." => "_" | c => c)
1.327 end;
1.328 - fun ml_from_type br (IType ("Pair", [t1, t2])) =
1.329 - brackify (eval_br_postfix br (INFX (2, L))) [
1.330 - ml_from_type (INFX (2, X)) t1,
1.331 - Pretty.str "*",
1.332 - ml_from_type (INFX (2, X)) t2
1.333 - ]
1.334 - | ml_from_type br (IType ("Bool", [])) =
1.335 - Pretty.str "bool"
1.336 - | ml_from_type br (IType ("Integer", [])) =
1.337 - Pretty.str "IntInf.int"
1.338 - | ml_from_type br (IType ("List", [ty])) =
1.339 - postify ([ml_from_type BR ty]) (Pretty.str "list")
1.340 - |> Pretty.block
1.341 - | ml_from_type br (IType (tyco, typs)) =
1.342 + fun postify [] f = f
1.343 + | postify [p] f = Pretty.block [p, Pretty.brk 1, f]
1.344 + | postify (ps as _::_) f = Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, f];
1.345 + fun ml_from_type fxy (IType (tyco, tys)) =
1.346 + (case tyco_syntax tyco
1.347 + of NONE =>
1.348 + postify (map (ml_from_type BR) tys) ((str o resolv) tyco)
1.349 + | SOME ((i, k), pr) =>
1.350 + if not (i <= length tys andalso length tys <= k)
1.351 + then error ("number of argument mismatch in customary serialization: "
1.352 + ^ (string_of_int o length) tys ^ " given, " ^ string_of_int i ^ " to " ^ string_of_int k
1.353 + ^ " expected")
1.354 + else pr fxy ml_from_type tys)
1.355 + | ml_from_type fxy (IFun (t1, t2)) =
1.356 let
1.357 - val tyargs = (map (ml_from_type BR) typs)
1.358 + fun eval_fxy_postfix BR _ = false
1.359 + | eval_fxy_postfix NOBR _ = false
1.360 + | eval_fxy_postfix (INFX (pr1, lr1)) (INFX (pr2, lr2)) =
1.361 + pr1 > pr2
1.362 + orelse pr1 = pr2
1.363 + andalso eval_lrx lr1 lr2
1.364 + | eval_fxy_postfix (INFX _) _ = false;
1.365 in
1.366 - case tyco_syntax tyco
1.367 - of NONE =>
1.368 - postify tyargs ((Pretty.str o resolv) tyco)
1.369 - |> Pretty.block
1.370 - | SOME ((i, fix), pr) =>
1.371 - if i <> length (typs)
1.372 - then error "can only serialize strictly complete type applications to ML"
1.373 - else
1.374 - pr tyargs (ml_from_type fix)
1.375 - |> (if eval_br br fix then Pretty.enclose "(" ")" o single else I)
1.376 + brackify (eval_fxy_postfix fxy (INFX (1, R))) [
1.377 + ml_from_type (INFX (1, X)) t1,
1.378 + str "->",
1.379 + ml_from_type (INFX (1, R)) t2
1.380 + ]
1.381 end
1.382 - | ml_from_type br (IFun (t1, t2)) =
1.383 - brackify (eval_br_postfix br (INFX (1, R))) [
1.384 - ml_from_type (INFX (1, X)) t1,
1.385 - Pretty.str "->",
1.386 - ml_from_type (INFX (1, R)) t2
1.387 - ]
1.388 | ml_from_type _ (IVarT (v, [])) =
1.389 - Pretty.str ("'" ^ v)
1.390 + str ("'" ^ v)
1.391 | ml_from_type _ (IVarT (_, sort)) =
1.392 "cannot serialize sort constrained type variable to ML: " ^ commas sort |> error
1.393 | ml_from_type _ (IDictT fs) =
1.394 Pretty.gen_list "," "{" "}" (
1.395 map (fn (f, ty) =>
1.396 - Pretty.block [Pretty.str (ml_from_label f ^ ": "), ml_from_type NOBR ty]) fs
1.397 + Pretty.block [str (ml_from_label f ^ ": "), ml_from_type NOBR ty]) fs
1.398 );
1.399 - fun ml_from_pat br (ICons (("True", []), _)) =
1.400 - Pretty.str "true"
1.401 - | ml_from_pat br (ICons (("False", []), _)) =
1.402 - Pretty.str "false"
1.403 - | ml_from_pat br (ICons (("Pair", [p1, p2]), _)) =
1.404 - Pretty.list "(" ")" [
1.405 - ml_from_pat NOBR p1,
1.406 - ml_from_pat NOBR p2
1.407 - ]
1.408 - | ml_from_pat br (ICons (("Nil", []), _)) =
1.409 - Pretty.str "[]"
1.410 - | ml_from_pat br (p as ICons (("Cons", _), _)) =
1.411 - let
1.412 - fun dest_cons (ICons (("Cons", [ICons (("Pair", [p1, p2]), _)]), _)) = SOME (p1, p2)
1.413 - | dest_cons p = NONE
1.414 - in
1.415 - case unfoldr dest_cons p
1.416 - of (ps, (ICons (("Nil", []), _))) =>
1.417 + fun ml_from_pat fxy (ICons ((f, ps), ty)) =
1.418 + (case const_syntax f
1.419 + of NONE => if length ps <= 1
1.420 + then
1.421 ps
1.422 - |> map (ml_from_pat NOBR)
1.423 - |> Pretty.list "[" "]"
1.424 - | (ps, p) =>
1.425 - (ps @ [p])
1.426 - |> map (ml_from_pat (INFX (5, X)))
1.427 - |> separate (Pretty.str "::")
1.428 - |> brackify (eval_br br (INFX (5, R)))
1.429 - end
1.430 - | ml_from_pat br (ICons ((f, ps), ty)) =
1.431 - (case const_syntax f
1.432 - of NONE =>
1.433 - ps
1.434 - |> map (ml_from_pat BR)
1.435 - |> cons ((Pretty.str o resolv) f)
1.436 - |> brackify (eval_br br BR)
1.437 - | SOME ((i, fix), pr) =>
1.438 - if i = length ps
1.439 - then
1.440 - pr (map (ml_from_pat fix) ps) (ml_from_expr fix)
1.441 - |> (if eval_br br fix then Pretty.enclose "(" ")" o single else I)
1.442 + |> map (ml_from_pat BR)
1.443 + |> cons ((str o resolv) f)
1.444 + |> brackify (eval_fxy fxy BR)
1.445 else
1.446 - error "number of argument mismatch in customary serialization")
1.447 - | ml_from_pat br (IVarP (v, IType ("Integer", []))) =
1.448 - brackify (eval_br br BR) [
1.449 - Pretty.str v,
1.450 - Pretty.str ":",
1.451 - Pretty.str "IntInf.int"
1.452 - ]
1.453 - | ml_from_pat br (IVarP (v, ty)) =
1.454 - if is_dicttype ty
1.455 + ps
1.456 + |> map (ml_from_pat BR)
1.457 + |> Pretty.gen_list "," "(" ")"
1.458 + |> single
1.459 + |> cons ((str o resolv) f)
1.460 + |> brackify (eval_fxy fxy BR)
1.461 + | SOME ((i, k), pr) =>
1.462 + if not (i <= length ps andalso length ps <= k)
1.463 + then error ("number of argument mismatch in customary serialization: "
1.464 + ^ (string_of_int o length) ps ^ " given, " ^ string_of_int i ^ " to " ^ string_of_int k
1.465 + ^ " expected")
1.466 + else pr fxy ml_from_expr (map iexpr_of_ipat ps))
1.467 + | ml_from_pat fxy (IVarP (v, ty)) =
1.468 + if needs_type ty
1.469 then
1.470 - brackify (eval_br br BR) [
1.471 - Pretty.str v,
1.472 - Pretty.str ":",
1.473 + brackify (eval_fxy fxy BR) [
1.474 + str v,
1.475 + str ":",
1.476 ml_from_type NOBR ty
1.477 ]
1.478 else
1.479 - Pretty.str v
1.480 - and ml_from_expr br (e as (IApp (IConst ("Cons", _), _))) =
1.481 - let
1.482 - fun dest_cons (IApp (IConst ("Cons", _),
1.483 - IApp (IApp (IConst ("Pair", _), e1), e2))) = SOME (e1, e2)
1.484 - | dest_cons p = NONE
1.485 - in
1.486 - case unfoldr dest_cons e
1.487 - of (es, (IConst ("Nil", _))) =>
1.488 - es
1.489 - |> map (ml_from_expr NOBR)
1.490 - |> Pretty.list "[" "]"
1.491 - | (es, e) =>
1.492 - (es @ [e])
1.493 - |> map (ml_from_expr (INFX (5, X)))
1.494 - |> separate (Pretty.str "::")
1.495 - |> brackify (eval_br br (INFX (5, R)))
1.496 - end
1.497 - | ml_from_expr br (e as IApp (e1, e2)) =
1.498 + str v
1.499 + and ml_from_expr fxy (e as IApp (e1, e2)) =
1.500 (case (unfold_app e)
1.501 of (e as (IConst (f, _)), es) =>
1.502 - ml_from_app br (f, es)
1.503 + ml_from_app fxy (f, es)
1.504 | _ =>
1.505 - brackify (eval_br br BR) [
1.506 + brackify (eval_fxy fxy BR) [
1.507 ml_from_expr NOBR e1,
1.508 ml_from_expr BR e2
1.509 ])
1.510 - | ml_from_expr br (e as IConst (f, _)) =
1.511 - ml_from_app br (f, [])
1.512 - | ml_from_expr br (IVarE (v, _)) =
1.513 - Pretty.str v
1.514 - | ml_from_expr br (IAbs ((v, _), e)) =
1.515 - brackify (eval_br br BR) [
1.516 - Pretty.str ("fn " ^ v ^ " =>"),
1.517 + | ml_from_expr fxy (e as IConst (f, _)) =
1.518 + ml_from_app fxy (f, [])
1.519 + | ml_from_expr fxy (IVarE (v, _)) =
1.520 + str v
1.521 + | ml_from_expr fxy (IAbs ((v, _), e)) =
1.522 + brackify (eval_fxy fxy BR) [
1.523 + str ("fn " ^ v ^ " =>"),
1.524 ml_from_expr NOBR e
1.525 ]
1.526 - | ml_from_expr br (e as ICase (_, [_])) =
1.527 + | ml_from_expr fxy (e as ICase (_, [_])) =
1.528 let
1.529 val (ps, e) = unfold_let e;
1.530 fun mk_val (p, e) = Pretty.block [
1.531 - Pretty.str "val ",
1.532 - ml_from_pat BR p,
1.533 - Pretty.str " =",
1.534 + str "val ",
1.535 + ml_from_pat fxy p,
1.536 + str " =",
1.537 Pretty.brk 1,
1.538 ml_from_expr NOBR e,
1.539 - Pretty.str ";"
1.540 + str ";"
1.541 ]
1.542 in Pretty.chunks [
1.543 - [Pretty.str ("let"), Pretty.fbrk, map mk_val ps |> Pretty.chunks] |> Pretty.block,
1.544 - [Pretty.str ("in"), Pretty.fbrk, ml_from_expr NOBR e] |> Pretty.block,
1.545 - Pretty.str ("end")
1.546 + [str ("let"), Pretty.fbrk, map mk_val ps |> Pretty.chunks] |> Pretty.block,
1.547 + [str ("in"), Pretty.fbrk, ml_from_expr NOBR e] |> Pretty.block,
1.548 + str ("end")
1.549 ] end
1.550 - | ml_from_expr br (ICase (e, c::cs)) =
1.551 + | ml_from_expr fxy (ICase (e, c::cs)) =
1.552 let
1.553 fun mk_clause definer (p, e) =
1.554 Pretty.block [
1.555 - Pretty.str definer,
1.556 + str definer,
1.557 ml_from_pat NOBR p,
1.558 - Pretty.str " =>",
1.559 + str " =>",
1.560 Pretty.brk 1,
1.561 ml_from_expr NOBR e
1.562 ]
1.563 - in brackify (eval_br br BR) (
1.564 - Pretty.str "case"
1.565 + in brackify (eval_fxy fxy BR) (
1.566 + str "case"
1.567 :: ml_from_expr NOBR e
1.568 :: mk_clause "of " c
1.569 :: map (mk_clause "| ") cs
1.570 ) end
1.571 - | ml_from_expr br (IInst _) =
1.572 + | ml_from_expr fxy (IInst _) =
1.573 error "cannot serialize poly instant to ML"
1.574 - | ml_from_expr br (IDictE fs) =
1.575 + | ml_from_expr fxy (IDictE fs) =
1.576 Pretty.gen_list "," "{" "}" (
1.577 map (fn (f, e) =>
1.578 - Pretty.block [Pretty.str (ml_from_label f ^ " = "), ml_from_expr NOBR e]) fs
1.579 + Pretty.block [str (ml_from_label f ^ " = "), ml_from_expr NOBR e]) fs
1.580 )
1.581 - | ml_from_expr br (ILookup ([], v)) =
1.582 - Pretty.str v
1.583 - | ml_from_expr br (ILookup ([l], v)) =
1.584 - brackify (eval_br br BR) [
1.585 - Pretty.str ("#" ^ (ml_from_label l)),
1.586 - Pretty.str v
1.587 + | ml_from_expr fxy (ILookup ([], v)) =
1.588 + str v
1.589 + | ml_from_expr fxy (ILookup ([l], v)) =
1.590 + brackify (eval_fxy fxy BR) [
1.591 + str ("#" ^ (ml_from_label l)),
1.592 + str v
1.593 ]
1.594 - | ml_from_expr br (ILookup (ls, v)) =
1.595 - brackify (eval_br br BR) [
1.596 - Pretty.str ("("
1.597 + | ml_from_expr fxy (ILookup (ls, v)) =
1.598 + brackify (eval_fxy fxy BR) [
1.599 + str ("("
1.600 ^ (ls |> map ((fn s => "#" ^ s) o ml_from_label) |> foldr1 (fn (l, e) => l ^ " o " ^ e))
1.601 ^ ")"),
1.602 - Pretty.str v
1.603 + str v
1.604 ]
1.605 | ml_from_expr _ e =
1.606 error ("dubious expression: " ^ (Pretty.output o pretty_iexpr) e)
1.607 - and mk_app_p br p args =
1.608 - brackify (eval_br br BR)
1.609 - (p :: map (ml_from_expr BR) args)
1.610 - and ml_from_app br ("Nil", []) =
1.611 - Pretty.str "[]"
1.612 - | ml_from_app br ("True", []) =
1.613 - Pretty.str "true"
1.614 - | ml_from_app br ("False", []) =
1.615 - Pretty.str "false"
1.616 - | ml_from_app br ("Pair", [e1, e2]) =
1.617 - Pretty.list "(" ")" [
1.618 - ml_from_expr NOBR e1,
1.619 - ml_from_expr NOBR e2
1.620 - ]
1.621 - | ml_from_app br ("and", [e1, e2]) =
1.622 - brackify (eval_br br (INFX (~1, L))) [
1.623 - ml_from_expr (INFX (~1, L)) e1,
1.624 - Pretty.str "andalso",
1.625 - ml_from_expr (INFX (~1, X)) e2
1.626 - ]
1.627 - | ml_from_app br ("or", [e1, e2]) =
1.628 - brackify (eval_br br (INFX (~2, L))) [
1.629 - ml_from_expr (INFX (~2, L)) e1,
1.630 - Pretty.str "orelse",
1.631 - ml_from_expr (INFX (~2, X)) e2
1.632 - ]
1.633 - | ml_from_app br ("if", [b, e1, e2]) =
1.634 - brackify (eval_br br BR) [
1.635 - Pretty.str "if",
1.636 - ml_from_expr NOBR b,
1.637 - Pretty.str "then",
1.638 - ml_from_expr NOBR e1,
1.639 - Pretty.str "else",
1.640 - ml_from_expr NOBR e2
1.641 - ]
1.642 - | ml_from_app br ("add", [e1, e2]) =
1.643 - brackify (eval_br br (INFX (6, L))) [
1.644 - ml_from_expr (INFX (6, L)) e1,
1.645 - Pretty.str "+",
1.646 - ml_from_expr (INFX (6, X)) e2
1.647 - ]
1.648 - | ml_from_app br ("mult", [e1, e2]) =
1.649 - brackify (eval_br br (INFX (7, L))) [
1.650 - ml_from_expr (INFX (7, L)) e1,
1.651 - Pretty.str "+",
1.652 - ml_from_expr (INFX (7, X)) e2
1.653 - ]
1.654 - | ml_from_app br ("lt", [e1, e2]) =
1.655 - brackify (eval_br br (INFX (4, L))) [
1.656 - ml_from_expr (INFX (4, L)) e1,
1.657 - Pretty.str "<",
1.658 - ml_from_expr (INFX (4, X)) e2
1.659 - ]
1.660 - | ml_from_app br ("le", [e1, e2]) =
1.661 - brackify (eval_br br (INFX (7, L))) [
1.662 - ml_from_expr (INFX (4, L)) e1,
1.663 - Pretty.str "<=",
1.664 - ml_from_expr (INFX (4, X)) e2
1.665 - ]
1.666 - | ml_from_app br ("minus", es) =
1.667 - mk_app_p br (Pretty.str "~") es
1.668 - | ml_from_app br ("wfrec", es) =
1.669 - mk_app_p br (Pretty.str "wfrec") es
1.670 - | ml_from_app br (f, es) =
1.671 - case const_syntax f
1.672 - of NONE =>
1.673 - (case es
1.674 - of [] => Pretty.str (resolv f)
1.675 - | es =>
1.676 - let
1.677 - val (es', e) = split_last es;
1.678 - in mk_app_p br (ml_from_app NOBR (f, es')) [e] end)
1.679 - | SOME ((i, fix), pr) =>
1.680 - let
1.681 - val (es1, es2) = splitAt (i, es);
1.682 - in
1.683 - mk_app_p br (
1.684 - pr (map (ml_from_expr fix) es1) (ml_from_expr fix)
1.685 - |> (if eval_br br fix then Pretty.enclose "(" ")" o single else I)
1.686 - ) es2
1.687 - end;
1.688 + and ml_mk_app f es =
1.689 + if is_cons f andalso length es > 1
1.690 + then
1.691 + [(str o resolv) f, Pretty.gen_list " *" "(" ")" (map (ml_from_expr BR) es)]
1.692 + else
1.693 + (str o resolv) f :: map (ml_from_expr BR) es
1.694 + and ml_from_app fxy =
1.695 + from_app ml_mk_app ml_from_expr const_syntax fxy;
1.696 fun ml_from_funs (ds as d::ds_tl) =
1.697 let
1.698 fun mk_definer [] = "val"
1.699 - | mk_definer _ = "fun"
1.700 + | mk_definer _ = "fun";
1.701 fun check_args (_, Fun ((pats, _)::_, _)) NONE =
1.702 SOME (mk_definer pats)
1.703 | check_args (_, Fun ((pats, _)::_, _)) (SOME definer) =
1.704 @@ -408,11 +435,11 @@
1.705 val definer = the (fold check_args ds NONE);
1.706 fun mk_eq definer f ty (pats, expr) =
1.707 let
1.708 - val lhs = [Pretty.str (definer ^ " " ^ f)]
1.709 + val lhs = [str (definer ^ " " ^ f)]
1.710 @ (if null pats
1.711 - then [Pretty.str ":", ml_from_type NOBR ty]
1.712 + then [str ":", ml_from_type NOBR ty]
1.713 else map (ml_from_pat BR) pats)
1.714 - val rhs = [Pretty.str "=", ml_from_expr NOBR expr]
1.715 + val rhs = [str "=", ml_from_expr NOBR expr]
1.716 in
1.717 Pretty.block (separate (Pretty.brk 1) (lhs @ rhs))
1.718 end
1.719 @@ -437,21 +464,23 @@
1.720 (fn (name, Datatype info) => SOME (name, info)
1.721 | (name, Datatypecons _) => NONE
1.722 | (name, def) => error ("datatype block containing illegal def: " ^ (Pretty.output o pretty_def) def)
1.723 - ) ds
1.724 - fun praetify [] f = [f]
1.725 - | praetify [p] f = [f, Pretty.str " of ", p]
1.726 - fun mk_cons (co, typs) =
1.727 - (Pretty.block oo praetify)
1.728 - (map (ml_from_type NOBR) typs)
1.729 - (Pretty.str (resolv co))
1.730 - fun mk_datatype definer (t, (vs, cs, _)) =
1.731 + ) defs
1.732 + fun mk_cons (co, []) =
1.733 + str (resolv co)
1.734 + | mk_cons (co, tys) =
1.735 + Pretty.block (
1.736 + str (resolv co)
1.737 + :: str " of"
1.738 + :: Pretty.brk 1
1.739 + :: separate (Pretty.block [str " *", Pretty.brk 1]) (map (ml_from_type NOBR) tys)
1.740 + )
1.741 + fun mk_datatype definer (t, ((vs, cs), _)) =
1.742 Pretty.block (
1.743 - [Pretty.str definer]
1.744 - @ postify (map (ml_from_type BR o IVarT) vs)
1.745 - (Pretty.str (resolv t))
1.746 - @ [Pretty.str " =",
1.747 - Pretty.brk 1]
1.748 - @ separate (Pretty.block [Pretty.brk 1, Pretty.str "| "]) (map mk_cons cs)
1.749 + str definer
1.750 + :: ml_from_type NOBR (t `%% map IVarT vs)
1.751 + :: str " ="
1.752 + :: Pretty.brk 1
1.753 + :: separate (Pretty.block [Pretty.brk 1, str "| "]) (map mk_cons cs)
1.754 )
1.755 in
1.756 case defs'
1.757 @@ -461,134 +490,100 @@
1.758 :: map (mk_datatype "and ") ds_tl
1.759 ) |> SOME
1.760 | _ => NONE
1.761 - end;
1.762 - fun ml_from_def (name, Nop) =
1.763 - if exists (fn query => query name)
1.764 - [(fn name => (is_some o tyco_syntax) name),
1.765 - (fn name => (is_some o const_syntax) name)]
1.766 - then NONE
1.767 - else error ("empty definition during serialization: " ^ quote name)
1.768 + end
1.769 + fun ml_from_def (name, Undef) =
1.770 + error ("empty definition during serialization: " ^ quote name)
1.771 | ml_from_def (name, Prim prim) =
1.772 - code_from_primitive serializer_name (name, prim)
1.773 + from_prim (name, prim)
1.774 | ml_from_def (name, Typesyn (vs, ty)) =
1.775 (map (fn (vname, []) => () | _ => error "can't serialize sort constrained type declaration to ML") vs;
1.776 - Pretty.block (
1.777 - Pretty.str "type "
1.778 - :: postify (map (ml_from_type BR o IVarT) vs) (Pretty.str name)
1.779 - @ [Pretty.str " =",
1.780 + Pretty.block [
1.781 + str "type ",
1.782 + ml_from_type NOBR (name `%% map IVarT vs),
1.783 + str " =",
1.784 Pretty.brk 1,
1.785 ml_from_type NOBR ty,
1.786 - Pretty.str ";"
1.787 + str ";"
1.788 ]
1.789 - )) |> SOME
1.790 + ) |> SOME
1.791 | ml_from_def (name, Class _) =
1.792 error ("can't serialize class declaration " ^ quote name ^ " to ML")
1.793 | ml_from_def (_, Classmember _) =
1.794 NONE
1.795 | ml_from_def (name, Classinst _) =
1.796 error ("can't serialize instance declaration " ^ quote name ^ " to ML")
1.797 - in case ds
1.798 - of (_, Fun _)::_ => ml_from_funs ds
1.799 - | (_, Datatypecons _)::_ => ml_from_datatypes ds
1.800 - | (_, Datatype _)::_ => ml_from_datatypes ds
1.801 - | [d] => ml_from_def d
1.802 + in (writeln ("ML defs " ^ (commas o map fst) defs); case defs
1.803 + of (_, Fun _)::_ => ml_from_funs defs
1.804 + | (_, Datatypecons _)::_ => ml_from_datatypes defs
1.805 + | (_, Datatype _)::_ => ml_from_datatypes defs
1.806 + | [def] => ml_from_def def)
1.807 end;
1.808
1.809 in
1.810
1.811 -fun ml_from_thingol nspgrp nsp_class name_root serializer_name tyco_syntax const_syntax select module =
1.812 +fun ml_from_thingol target (nsp_dtcon, nsp_class, int_tyco)
1.813 + nspgrp (tyco_syntax, const_syntax) name_root select module =
1.814 let
1.815 - fun ml_validator name =
1.816 - let
1.817 - fun replace_invalid c =
1.818 - if (Char.isAlphaNum o the o Char.fromString) c orelse c = "'"
1.819 - andalso not (NameSpace.separator = c)
1.820 - then c
1.821 - else "_"
1.822 - fun suffix_it name =
1.823 - name
1.824 - |> member (op =) ThmDatabase.ml_reserved ? suffix "'"
1.825 - |> member (op =) CodegenThingol.prims ? suffix "'"
1.826 - |> (fn name' => if name = name' then name else suffix_it name')
1.827 - in
1.828 - name
1.829 - |> translate_string replace_invalid
1.830 - |> suffix_it
1.831 - |> (fn name' => if name = name' then NONE else SOME name')
1.832 - end;
1.833 - fun ml_from_module (name, ps) =
1.834 - Pretty.chunks ([
1.835 - Pretty.str ("structure " ^ name ^ " = "),
1.836 - Pretty.str "struct",
1.837 - Pretty.str ""
1.838 - ] @ separate (Pretty.str "") ps @ [
1.839 - Pretty.str "",
1.840 - Pretty.str ("end; (* struct " ^ name ^ " *)")
1.841 - ]);
1.842 - fun is_dicttype (IType (tyco, _)) =
1.843 + val reserved_ml = ThmDatabase.ml_reserved @ [
1.844 + "bool", "int", "list", "true", "false"
1.845 + ];
1.846 + fun ml_from_module _ (name, ps) () =
1.847 + (Pretty.chunks ([
1.848 + str ("structure " ^ name ^ " = "),
1.849 + str "struct",
1.850 + str ""
1.851 + ] @ separate (str "") ps @ [
1.852 + str "",
1.853 + str ("end; (* struct " ^ name ^ " *)")
1.854 + ]), ());
1.855 + fun needs_type (IType (tyco, _)) =
1.856 has_nsp tyco nsp_class
1.857 - | is_dicttype (IDictT _) =
1.858 + orelse tyco = int_tyco
1.859 + | needs_type (IDictT _) =
1.860 true
1.861 - | is_dicttype _ =
1.862 + | needs_type _ =
1.863 false;
1.864 - fun eta_expander "Pair" = 2
1.865 - | eta_expander "Cons" = 2
1.866 - | eta_expander "and" = 2
1.867 - | eta_expander "or" = 2
1.868 - | eta_expander "if" = 3
1.869 - | eta_expander "add" = 2
1.870 - | eta_expander "mult" = 2
1.871 - | eta_expander "lt" = 2
1.872 - | eta_expander "le" = 2
1.873 - | eta_expander s =
1.874 - if NameSpace.is_qualified s
1.875 - then case get_def module s
1.876 - of Datatypecons dtname =>
1.877 - (case get_def module dtname
1.878 - of Datatype (_, cs, _) =>
1.879 - let val l = AList.lookup (op =) cs s |> the |> length
1.880 - in if l >= 2 then l else 0 end)
1.881 - | _ =>
1.882 - const_syntax s
1.883 - |> Option.map (fst o fst)
1.884 - |> the_default 0
1.885 - else 0;
1.886 + fun is_cons c = has_nsp c nsp_dtcon;
1.887 + fun eta_expander s =
1.888 + case const_syntax s
1.889 + of SOME ((i, _), _) => i
1.890 + | _ => if has_nsp s nsp_dtcon
1.891 + then case get_def module s
1.892 + of Datatypecons dtname => case get_def module dtname
1.893 + of Datatype ((_, cs), _) =>
1.894 + let val l = AList.lookup (op =) cs s |> the |> length
1.895 + in if l >= 2 then l else 0 end
1.896 + else 0;
1.897 + fun preprocess module =
1.898 + module
1.899 + |> tap (Pretty.writeln o pretty_deps)
1.900 + |> debug 3 (fn _ => "eta-expanding...")
1.901 + |> eta_expand eta_expander
1.902 + |> debug 3 (fn _ => "eta-expanding polydefs...")
1.903 + |> eta_expand_poly
1.904 + |> debug 3 (fn _ => "eliminating classes...")
1.905 + |> eliminate_classes
1.906 in
1.907 - module
1.908 - |> debug 3 (fn _ => "selecting submodule...")
1.909 - |> (if is_some select then (partof o the) select else I)
1.910 - |> tap (Pretty.writeln o pretty_deps)
1.911 - |> debug 3 (fn _ => "eta-expanding...")
1.912 - |> eta_expand eta_expander
1.913 - |> debug 3 (fn _ => "eta-expanding polydefs...")
1.914 - |> eta_expand_poly
1.915 - |> debug 3 (fn _ => "tupelizing datatypes...")
1.916 - |> tupelize_cons
1.917 - |> debug 3 (fn _ => "eliminating classes...")
1.918 - |> eliminate_classes
1.919 - |> debug 3 (fn _ => "serializing...")
1.920 - |> serialize (ml_from_defs serializer_name tyco_syntax const_syntax is_dicttype) ml_from_module ml_validator nspgrp name_root
1.921 + abstract_serializer preprocess (ml_from_defs (is_cons, needs_type), ml_from_module, abstract_validator reserved_ml)
1.922 + (target, (tyco_syntax, const_syntax)) (name_root, nspgrp) I select module
1.923 end;
1.924
1.925 -fun ml_from_thingol' nspgrp name_root =
1.926 - Scan.optional (
1.927 - OuterParse.$$$ "(" |-- OuterParse.list1 OuterParse.text --| OuterParse.$$$ ")"
1.928 - ) []
1.929 - >> (fn _ => ml_from_thingol nspgrp name_root);
1.930 -
1.931 -(* ML infix precedence
1.932 - 7 / * div mod
1.933 - 6 + - ^
1.934 - 5 :: @
1.935 - 4 = <> < > <= >=
1.936 - 3 := o *)
1.937 -
1.938 end; (* local *)
1.939
1.940 local
1.941
1.942 -fun haskell_from_defs serializer_name tyco_syntax const_syntax is_cons resolv defs =
1.943 +fun haskell_from_defs is_cons (from_prim, (tyco_syntax, const_syntax)) resolv defs =
1.944 let
1.945 + fun upper_first s =
1.946 + let
1.947 + val (pr, b) = split_last (NameSpace.unpack s);
1.948 + val (c::cs) = String.explode b;
1.949 + in NameSpace.pack (pr @ [String.implode (Char.toUpper c :: cs)]) end;
1.950 + fun lower_first s =
1.951 + let
1.952 + val (pr, b) = split_last (NameSpace.unpack s);
1.953 + val (c::cs) = String.explode b;
1.954 + in NameSpace.pack (pr @ [String.implode (Char.toLower c :: cs)]) end;
1.955 val resolv = fn s =>
1.956 let
1.957 val (prfix, base) = (split_last o NameSpace.unpack o resolv) s
1.958 @@ -605,283 +600,156 @@
1.959 f;
1.960 fun haskell_from_sctxt vs =
1.961 let
1.962 - fun from_sctxt [] = Pretty.str ""
1.963 + fun from_sctxt [] = str ""
1.964 | from_sctxt vs =
1.965 vs
1.966 - |> map (fn (v, cls) => Pretty.str ((upper_first o resolv) cls ^ " " ^ lower_first v))
1.967 + |> map (fn (v, cls) => str ((upper_first o resolv) cls ^ " " ^ lower_first v))
1.968 |> Pretty.gen_list "," "(" ")"
1.969 - |> (fn p => Pretty.block [p, Pretty.str " => "])
1.970 + |> (fn p => Pretty.block [p, str " => "])
1.971 in
1.972 vs
1.973 |> map (fn (v, sort) => map (pair v) sort)
1.974 |> Library.flat
1.975 |> from_sctxt
1.976 end;
1.977 - fun haskell_from_type br ty =
1.978 + fun haskell_from_type fxy ty =
1.979 let
1.980 - fun from_itype br (IType ("Pair", [t1, t2])) sctxt =
1.981 - sctxt
1.982 - |> from_itype NOBR t1
1.983 - ||>> from_itype NOBR t2
1.984 - |-> (fn (p1, p2) => pair (Pretty.gen_list "," "(" ")" [p1, p2]))
1.985 - | from_itype br (IType ("List", [ty])) sctxt =
1.986 - sctxt
1.987 - |> from_itype NOBR ty
1.988 - |-> (fn p => pair (Pretty.enclose "[" "]" [p]))
1.989 - | from_itype br (IType (tyco, tys)) sctxt =
1.990 - let
1.991 - fun mk_itype NONE tyargs sctxt =
1.992 - sctxt
1.993 - |> pair (brackify (eval_br br BR) ((Pretty.str o upper_first o resolv) tyco :: tyargs))
1.994 - | mk_itype (SOME ((i, fix), pr)) tyargs sctxt =
1.995 - if i <> length (tys)
1.996 - then error "can only serialize strictly complete type applications to haskell"
1.997 - else
1.998 - sctxt
1.999 - |> pair (pr tyargs (haskell_from_type fix)
1.1000 - |> (if eval_br br fix then Pretty.enclose "(" ")" o single else I)
1.1001 - )
1.1002 - in
1.1003 - sctxt
1.1004 - |> fold_map (from_itype BR) tys
1.1005 - |-> mk_itype (tyco_syntax tyco)
1.1006 - end
1.1007 - | from_itype br (IFun (t1, t2)) sctxt =
1.1008 + fun from_itype fxy (IType (tyco, tys)) sctxt =
1.1009 + (case tyco_syntax tyco
1.1010 + of NONE =>
1.1011 + sctxt
1.1012 + |> fold_map (from_itype BR) tys
1.1013 + |-> (fn tyargs => pair (brackify (eval_fxy fxy BR) ((str o upper_first o resolv) tyco :: tyargs)))
1.1014 + | SOME ((i, k), pr) =>
1.1015 + if not (i <= length tys andalso length tys <= k)
1.1016 + then error ("number of argument mismatch in customary serialization: "
1.1017 + ^ (string_of_int o length) tys ^ " given, " ^ string_of_int i ^ " to " ^ string_of_int k
1.1018 + ^ " expected")
1.1019 + else (pr fxy haskell_from_type tys, sctxt))
1.1020 + | from_itype fxy (IFun (t1, t2)) sctxt =
1.1021 sctxt
1.1022 |> from_itype (INFX (1, X)) t1
1.1023 ||>> from_itype (INFX (1, R)) t2
1.1024 |-> (fn (p1, p2) => pair (
1.1025 - brackify (eval_br br (INFX (1, R))) [
1.1026 + brackify (eval_fxy fxy (INFX (1, R))) [
1.1027 p1,
1.1028 - Pretty.str "->",
1.1029 + str "->",
1.1030 p2
1.1031 ]
1.1032 ))
1.1033 - | from_itype br (IVarT (v, [])) sctxt =
1.1034 + | from_itype fxy (IVarT (v, [])) sctxt =
1.1035 sctxt
1.1036 - |> pair ((Pretty.str o lower_first) v)
1.1037 - | from_itype br (IVarT (v, sort)) sctxt =
1.1038 + |> pair ((str o lower_first) v)
1.1039 + | from_itype fxy (IVarT (v, sort)) sctxt =
1.1040 sctxt
1.1041 |> AList.default (op =) (v, [])
1.1042 |> AList.map_entry (op =) v (fold (insert (op =)) sort)
1.1043 - |> pair ((Pretty.str o lower_first) v)
1.1044 - | from_itype br (IDictT _) _ =
1.1045 + |> pair ((str o lower_first) v)
1.1046 + | from_itype fxy (IDictT _) _ =
1.1047 error "cannot serialize dictionary type to haskell"
1.1048 in
1.1049 []
1.1050 - |> from_itype br ty
1.1051 + |> from_itype fxy ty
1.1052 ||> haskell_from_sctxt
1.1053 |> (fn (pty, pctxt) => Pretty.block [pctxt, pty])
1.1054 end;
1.1055 - fun haskell_from_pat br (ICons (("Pair", [p1, p2]), _)) =
1.1056 - Pretty.list "(" ")" [
1.1057 - haskell_from_pat NOBR p1,
1.1058 - haskell_from_pat NOBR p2
1.1059 - ]
1.1060 - | haskell_from_pat br (ICons (("Nil", []), _)) =
1.1061 - Pretty.str "[]"
1.1062 - | haskell_from_pat br (p as ICons (("Cons", _), _)) =
1.1063 - let
1.1064 - fun dest_cons (ICons (("Cons", [p1, p2]), ty)) = SOME (p1, p2)
1.1065 - | dest_cons p = NONE
1.1066 - in
1.1067 - case unfoldr dest_cons p
1.1068 - of (ps, (ICons (("Nil", []), _))) =>
1.1069 - ps
1.1070 - |> map (haskell_from_pat NOBR)
1.1071 - |> Pretty.list "[" "]"
1.1072 - | (ps, p) =>
1.1073 - (ps @ [p])
1.1074 - |> map (haskell_from_pat (INFX (5, X)))
1.1075 - |> separate (Pretty.str ":")
1.1076 - |> brackify (eval_br br (INFX (5, R)))
1.1077 - end
1.1078 - | haskell_from_pat br (ICons ((f, ps), _)) =
1.1079 + fun haskell_from_pat fxy (ICons ((f, ps), _)) =
1.1080 (case const_syntax f
1.1081 of NONE =>
1.1082 - ps
1.1083 - |> map (haskell_from_pat BR)
1.1084 - |> cons ((Pretty.str o resolv_const) f)
1.1085 - |> brackify (eval_br br BR)
1.1086 - | SOME ((i, fix), pr) =>
1.1087 - if i = length ps
1.1088 - then
1.1089 - pr (map (haskell_from_pat fix) ps) (haskell_from_expr fix)
1.1090 - |> (if eval_br br fix then Pretty.enclose "(" ")" o single else I)
1.1091 - else
1.1092 - error "number of argument mismatch in customary serialization")
1.1093 - | haskell_from_pat br (IVarP (v, _)) =
1.1094 - (Pretty.str o lower_first) v
1.1095 - and haskell_from_expr br (e as (IApp (IApp (IConst ("Cons", _), _), _))) =
1.1096 - let
1.1097 - fun dest_cons (IApp (IApp (IConst ("Cons", _), e1), e2)) = SOME (e1, e2)
1.1098 - | dest_cons p = NONE
1.1099 - in
1.1100 - case unfoldr dest_cons e
1.1101 - of (es, (IConst ("Nil", _))) =>
1.1102 - es
1.1103 - |> map (haskell_from_expr NOBR)
1.1104 - |> Pretty.list "[" "]"
1.1105 - | (es, e) =>
1.1106 - (es @ [e])
1.1107 - |> map (haskell_from_expr (INFX (5, X)))
1.1108 - |> separate (Pretty.str ":")
1.1109 - |> brackify (eval_br br (INFX (5, R)))
1.1110 - end
1.1111 - | haskell_from_expr br (e as IApp (e1, e2)) =
1.1112 + ps
1.1113 + |> map (haskell_from_pat BR)
1.1114 + |> cons ((str o resolv_const) f)
1.1115 + |> brackify (eval_fxy fxy BR)
1.1116 + | SOME ((i, k), pr) =>
1.1117 + if not (i <= length ps andalso length ps <= k)
1.1118 + then error ("number of argument mismatch in customary serialization: "
1.1119 + ^ (string_of_int o length) ps ^ " given, " ^ string_of_int i ^ " to " ^ string_of_int k
1.1120 + ^ " expected")
1.1121 + else pr fxy haskell_from_expr (map iexpr_of_ipat ps))
1.1122 + | haskell_from_pat fxy (IVarP (v, _)) =
1.1123 + (str o lower_first) v
1.1124 + and haskell_from_expr fxy (e as IApp (e1, e2)) =
1.1125 (case (unfold_app e)
1.1126 of (e as (IConst (f, _)), es) =>
1.1127 - haskell_from_app br (f, es)
1.1128 + haskell_from_app fxy (f, es)
1.1129 | _ =>
1.1130 - brackify (eval_br br BR) [
1.1131 + brackify (eval_fxy fxy BR) [
1.1132 haskell_from_expr NOBR e1,
1.1133 haskell_from_expr BR e2
1.1134 ])
1.1135 - | haskell_from_expr br (e as IConst (f, _)) =
1.1136 - haskell_from_app br (f, [])
1.1137 - | haskell_from_expr br (IVarE (v, _)) =
1.1138 - (Pretty.str o lower_first) v
1.1139 - | haskell_from_expr br (e as IAbs _) =
1.1140 + | haskell_from_expr fxy (e as IConst (f, _)) =
1.1141 + haskell_from_app fxy (f, [])
1.1142 + | haskell_from_expr fxy (IVarE (v, _)) =
1.1143 + (str o lower_first) v
1.1144 + | haskell_from_expr fxy (e as IAbs _) =
1.1145 let
1.1146 val (vs, body) = unfold_abs e
1.1147 in
1.1148 - brackify (eval_br br BR) (
1.1149 - Pretty.str "\\"
1.1150 - :: map (Pretty.str o lower_first o fst) vs @ [
1.1151 - Pretty.str "->",
1.1152 + brackify (eval_fxy fxy BR) (
1.1153 + str "\\"
1.1154 + :: map (str o lower_first o fst) vs @ [
1.1155 + str "->",
1.1156 haskell_from_expr NOBR body
1.1157 ])
1.1158 end
1.1159 - | haskell_from_expr br (e as ICase (_, [_])) =
1.1160 + | haskell_from_expr fxy (e as ICase (_, [_])) =
1.1161 let
1.1162 val (ps, body) = unfold_let e;
1.1163 fun mk_bind (p, e) = Pretty.block [
1.1164 haskell_from_pat BR p,
1.1165 - Pretty.str " =",
1.1166 + str " =",
1.1167 Pretty.brk 1,
1.1168 haskell_from_expr NOBR e
1.1169 ];
1.1170 in Pretty.chunks [
1.1171 - [Pretty.str ("let"), Pretty.fbrk, map mk_bind ps |> Pretty.chunks] |> Pretty.block,
1.1172 - [Pretty.str ("in "), haskell_from_expr NOBR body] |> Pretty.block
1.1173 + [str ("let"), Pretty.fbrk, map mk_bind ps |> Pretty.chunks] |> Pretty.block,
1.1174 + [str ("in "), haskell_from_expr NOBR body] |> Pretty.block
1.1175 ] end
1.1176 - | haskell_from_expr br (ICase (e, c::cs)) =
1.1177 + | haskell_from_expr fxy (ICase (e, c::cs)) =
1.1178 let
1.1179 - fun mk_clause (p, e) =
1.1180 + fun mk_clause definer (p, e) =
1.1181 Pretty.block [
1.1182 + str definer,
1.1183 haskell_from_pat NOBR p,
1.1184 - Pretty.str " ->",
1.1185 + str " ->",
1.1186 Pretty.brk 1,
1.1187 haskell_from_expr NOBR e
1.1188 ]
1.1189 - in (Pretty.block o Pretty.fbreaks) (
1.1190 - Pretty.block [Pretty.str "case ", haskell_from_expr NOBR e, Pretty.str " of"]
1.1191 - :: map (mk_clause) cs
1.1192 - )end
1.1193 - | haskell_from_expr br (IInst (e, _)) =
1.1194 - haskell_from_expr br e
1.1195 - | haskell_from_expr br (IDictE _) =
1.1196 + in brackify (eval_fxy fxy BR) (
1.1197 + str "case"
1.1198 + :: haskell_from_expr NOBR e
1.1199 + :: mk_clause "of " c
1.1200 + :: map (mk_clause "| ") cs
1.1201 + ) end
1.1202 + | haskell_from_expr fxy (IInst (e, _)) =
1.1203 + haskell_from_expr fxy e
1.1204 + | haskell_from_expr fxy (IDictE _) =
1.1205 error "cannot serialize dictionary expression to haskell"
1.1206 - | haskell_from_expr br (ILookup _) =
1.1207 + | haskell_from_expr fxy (ILookup _) =
1.1208 error "cannot serialize lookup expression to haskell"
1.1209 - and mk_app_p br p args =
1.1210 - brackify (eval_br br BR)
1.1211 - (p :: map (haskell_from_expr BR) args)
1.1212 - and haskell_from_app br ("Nil", []) =
1.1213 - Pretty.str "[]"
1.1214 - | haskell_from_app br ("Cons", es) =
1.1215 - mk_app_p br (Pretty.str "(:)") es
1.1216 - | haskell_from_app br ("eq", [e1, e2]) =
1.1217 - brackify (eval_br br (INFX (4, L))) [
1.1218 - haskell_from_expr (INFX (4, L)) e1,
1.1219 - Pretty.str "==",
1.1220 - haskell_from_expr (INFX (4, X)) e2
1.1221 - ]
1.1222 - | haskell_from_app br ("Pair", [e1, e2]) =
1.1223 - Pretty.list "(" ")" [
1.1224 - haskell_from_expr NOBR e1,
1.1225 - haskell_from_expr NOBR e2
1.1226 - ]
1.1227 - | haskell_from_app br ("if", [b, e1, e2]) =
1.1228 - brackify (eval_br br BR) [
1.1229 - Pretty.str "if",
1.1230 - haskell_from_expr NOBR b,
1.1231 - Pretty.str "then",
1.1232 - haskell_from_expr NOBR e1,
1.1233 - Pretty.str "else",
1.1234 - haskell_from_expr NOBR e2
1.1235 - ]
1.1236 - | haskell_from_app br ("and", es) =
1.1237 - haskell_from_binop br 3 R "&&" es
1.1238 - | haskell_from_app br ("or", es) =
1.1239 - haskell_from_binop br 2 R "||" es
1.1240 - | haskell_from_app br ("add", es) =
1.1241 - haskell_from_binop br 6 L "+" es
1.1242 - | haskell_from_app br ("mult", es) =
1.1243 - haskell_from_binop br 7 L "*" es
1.1244 - | haskell_from_app br ("lt", es) =
1.1245 - haskell_from_binop br 4 L "<" es
1.1246 - | haskell_from_app br ("le", es) =
1.1247 - haskell_from_binop br 4 L "<=" es
1.1248 - | haskell_from_app br ("minus", es) =
1.1249 - mk_app_p br (Pretty.str "negate") es
1.1250 - | haskell_from_app br ("wfrec", es) =
1.1251 - mk_app_p br (Pretty.str "wfrec") es
1.1252 - | haskell_from_app br (f, es) =
1.1253 - case const_syntax f
1.1254 - of NONE =>
1.1255 - (case es
1.1256 - of [] => Pretty.str (resolv_const f)
1.1257 - | es =>
1.1258 - let
1.1259 - val (es', e) = split_last es;
1.1260 - in mk_app_p br (haskell_from_app NOBR (f, es')) [e] end)
1.1261 - | SOME ((i, fix), pr) =>
1.1262 - let
1.1263 - val (es1, es2) = splitAt (i, es);
1.1264 - in
1.1265 - mk_app_p br (
1.1266 - pr (map (haskell_from_expr fix) es1) (haskell_from_expr fix)
1.1267 - |> (if eval_br br fix then Pretty.enclose "(" ")" o single else I)
1.1268 - ) es2
1.1269 - end
1.1270 - and haskell_from_binop br pr L f [e1, e2] =
1.1271 - brackify (eval_br br (INFX (pr, L))) [
1.1272 - haskell_from_expr (INFX (pr, L)) e1,
1.1273 - Pretty.str f,
1.1274 - haskell_from_expr (INFX (pr, X)) e2
1.1275 - ]
1.1276 - | haskell_from_binop br pr R f [e1, e2] =
1.1277 - brackify (eval_br br (INFX (pr, R))) [
1.1278 - haskell_from_expr (INFX (pr, X)) e1,
1.1279 - Pretty.str f,
1.1280 - haskell_from_expr (INFX (pr, R)) e2
1.1281 - ]
1.1282 - | haskell_from_binop br pr ass f args =
1.1283 - mk_app_p br (Pretty.str ("(" ^ f ^ ")")) args
1.1284 - fun haskell_from_def (name, Nop) =
1.1285 - if exists (fn query => query name)
1.1286 - [(fn name => (is_some o tyco_syntax) name),
1.1287 - (fn name => (is_some o const_syntax) name)]
1.1288 - then NONE
1.1289 - else error ("empty statement during serialization: " ^ quote name)
1.1290 + and haskell_mk_app f es =
1.1291 + (str o resolv_const) f :: map (haskell_from_expr BR) es
1.1292 + and haskell_from_app fxy =
1.1293 + from_app haskell_mk_app haskell_from_expr const_syntax fxy;
1.1294 + fun haskell_from_def (name, Undef) =
1.1295 + error ("empty statement during serialization: " ^ quote name)
1.1296 | haskell_from_def (name, Prim prim) =
1.1297 - code_from_primitive serializer_name (name, prim)
1.1298 + from_prim (name, prim)
1.1299 | haskell_from_def (name, Fun (eqs, (_, ty))) =
1.1300 let
1.1301 fun from_eq name (args, rhs) =
1.1302 Pretty.block [
1.1303 - Pretty.str (lower_first name),
1.1304 + str (lower_first name),
1.1305 Pretty.block (map (fn p => Pretty.block [Pretty.brk 1, haskell_from_pat BR p]) args),
1.1306 Pretty.brk 1,
1.1307 - Pretty.str ("="),
1.1308 + str ("="),
1.1309 Pretty.brk 1,
1.1310 haskell_from_expr NOBR rhs
1.1311 ]
1.1312 in
1.1313 Pretty.chunks [
1.1314 Pretty.block [
1.1315 - Pretty.str (name ^ " ::"),
1.1316 + str (lower_first name ^ " ::"),
1.1317 Pretty.brk 1,
1.1318 haskell_from_type NOBR ty
1.1319 ],
1.1320 @@ -890,138 +758,121 @@
1.1321 end
1.1322 | haskell_from_def (name, Typesyn (vs, ty)) =
1.1323 Pretty.block [
1.1324 - Pretty.str "type ",
1.1325 + str "type ",
1.1326 haskell_from_sctxt vs,
1.1327 - Pretty.str (upper_first name),
1.1328 - Pretty.block (map (fn (v, _) => Pretty.str (" " ^ (lower_first) v)) vs),
1.1329 - Pretty.str " =",
1.1330 + str (upper_first name),
1.1331 + Pretty.block (map (fn (v, _) => str (" " ^ (lower_first) v)) vs),
1.1332 + str " =",
1.1333 Pretty.brk 1,
1.1334 haskell_from_type NOBR ty
1.1335 ] |> SOME
1.1336 - | haskell_from_def (name, Datatype (vars, constrs, _)) =
1.1337 + | haskell_from_def (name, Datatype ((vars, constrs), _)) =
1.1338 let
1.1339 fun mk_cons (co, tys) =
1.1340 (Pretty.block o Pretty.breaks) (
1.1341 - Pretty.str ((upper_first o resolv) co)
1.1342 + str ((upper_first o resolv) co)
1.1343 :: map (haskell_from_type NOBR) tys
1.1344 )
1.1345 in
1.1346 Pretty.block (
1.1347 - Pretty.str "data "
1.1348 + str "data "
1.1349 :: haskell_from_sctxt vars
1.1350 - :: Pretty.str (upper_first name)
1.1351 - :: Pretty.block (map (fn (v, _) => Pretty.str (" " ^ (lower_first) v)) vars)
1.1352 - :: Pretty.str " ="
1.1353 + :: str (upper_first name)
1.1354 + :: Pretty.block (map (fn (v, _) => str (" " ^ (lower_first) v)) vars)
1.1355 + :: str " ="
1.1356 :: Pretty.brk 1
1.1357 - :: separate (Pretty.block [Pretty.brk 1, Pretty.str "| "]) (map mk_cons constrs)
1.1358 + :: separate (Pretty.block [Pretty.brk 1, str "| "]) (map mk_cons constrs)
1.1359 )
1.1360 end |> SOME
1.1361 | haskell_from_def (_, Datatypecons _) =
1.1362 NONE
1.1363 - | haskell_from_def (name, Class (supclasss, v, membrs, _)) =
1.1364 + | haskell_from_def (name, Class ((supclasss, (v, membrs)), _)) =
1.1365 let
1.1366 fun mk_member (m, (_, ty)) =
1.1367 Pretty.block [
1.1368 - Pretty.str (resolv m ^ " ::"),
1.1369 + str (resolv m ^ " ::"),
1.1370 Pretty.brk 1,
1.1371 haskell_from_type NOBR ty
1.1372 ]
1.1373 in
1.1374 Pretty.block [
1.1375 - Pretty.str "class ",
1.1376 + str "class ",
1.1377 haskell_from_sctxt (map (fn class => (v, [class])) supclasss),
1.1378 - Pretty.str ((upper_first name) ^ " " ^ v),
1.1379 - Pretty.str " where",
1.1380 + str ((upper_first name) ^ " " ^ v),
1.1381 + str " where",
1.1382 Pretty.fbrk,
1.1383 Pretty.chunks (map mk_member membrs)
1.1384 ] |> SOME
1.1385 end
1.1386 | haskell_from_def (name, Classmember _) =
1.1387 NONE
1.1388 - | haskell_from_def (_, Classinst (("Eq", (tyco, arity)), (_, [(_, (eqpred, _))]))) =
1.1389 + | haskell_from_def (_, Classinst ((clsname, (tyco, arity)), memdefs)) =
1.1390 Pretty.block [
1.1391 - Pretty.str "instance ",
1.1392 + str "instance ",
1.1393 haskell_from_sctxt arity,
1.1394 - Pretty.str "Eq",
1.1395 - Pretty.str " ",
1.1396 + str ((upper_first o resolv) clsname),
1.1397 + str " ",
1.1398 haskell_from_type NOBR (IType (tyco, (map (IVarT o rpair [] o fst)) arity)),
1.1399 - Pretty.str " where",
1.1400 + str " where",
1.1401 Pretty.fbrk,
1.1402 - Pretty.str ("(==) = " ^ (lower_first o resolv) eqpred)
1.1403 - ] |> SOME
1.1404 - | haskell_from_def (_, Classinst ((clsname, (tyco, arity)), (_, instmems))) =
1.1405 - Pretty.block [
1.1406 - Pretty.str "instance ",
1.1407 - haskell_from_sctxt arity,
1.1408 - Pretty.str ((upper_first o resolv) clsname),
1.1409 - Pretty.str " ",
1.1410 - haskell_from_type NOBR (IType (tyco, (map (IVarT o rpair [] o fst)) arity)),
1.1411 - Pretty.str " where",
1.1412 - Pretty.fbrk,
1.1413 - Pretty.chunks (map (fn (member, (const, _)) =>
1.1414 - Pretty.str ((lower_first o resolv) member ^ " = " ^ (lower_first o resolv) const)
1.1415 - ) instmems)
1.1416 + Pretty.chunks (map (fn (m, funn) => haskell_from_def (m, Fun funn) |> the) memdefs)
1.1417 ] |> SOME
1.1418 in
1.1419 case List.mapPartial (fn (name, def) => haskell_from_def (name, def)) defs
1.1420 of [] => NONE
1.1421 - | l => (SOME o Pretty.chunks o separate (Pretty.str "")) l
1.1422 + | l => (SOME o Pretty.chunks o separate (str "")) l
1.1423 end;
1.1424
1.1425 in
1.1426
1.1427 -fun haskell_from_thingol nspgrp nsp_cons name_root serializer_name tyco_syntax const_syntax select module =
1.1428 +fun haskell_from_thingol target nsp_dtcon
1.1429 + nspgrp (tyco_syntax, const_syntax) name_root select module =
1.1430 let
1.1431 - fun haskell_from_module (name, ps) =
1.1432 - Pretty.block [
1.1433 - Pretty.str ("module " ^ (upper_first name) ^ " where"),
1.1434 + val reserved_haskell = [
1.1435 + "hiding", "deriving", "where", "case", "of", "infix", "infixl", "infixr",
1.1436 + "import", "default", "forall", "let", "in", "class", "qualified", "data",
1.1437 + "newtype", "instance", "if", "then", "else", "type", "as", "do", "module"
1.1438 + ] @ [
1.1439 + "Bool", "fst", "snd", "Integer", "True", "False", "negate"
1.1440 + ];
1.1441 + fun upper_first s =
1.1442 + let
1.1443 + val (pr, b) = split_last (NameSpace.unpack s);
1.1444 + val (c::cs) = String.explode b;
1.1445 + in NameSpace.pack (pr @ [String.implode (Char.toUpper c :: cs)]) end;
1.1446 + fun haskell_from_module _ (name, ps) () =
1.1447 + (Pretty.block [
1.1448 + str ("module " ^ (upper_first name) ^ " where"),
1.1449 Pretty.fbrk,
1.1450 Pretty.fbrk,
1.1451 - Pretty.chunks (separate (Pretty.str "") ps)
1.1452 - ];
1.1453 - fun haskell_validator name =
1.1454 - let
1.1455 - fun replace_invalid c =
1.1456 - if (Char.isAlphaNum o the o Char.fromString) c orelse c = "'"
1.1457 - andalso not (NameSpace.separator = c)
1.1458 - then c
1.1459 - else "_"
1.1460 - fun suffix_it name =
1.1461 - name
1.1462 - |> member (op =) CodegenThingol.prims ? suffix "'"
1.1463 - |> (fn name' => if name = name' then name else suffix_it name')
1.1464 - in
1.1465 - name
1.1466 - |> translate_string replace_invalid
1.1467 - |> suffix_it
1.1468 - |> (fn name' => if name = name' then NONE else SOME name')
1.1469 - end;
1.1470 - fun eta_expander "Pair" = 2
1.1471 - | eta_expander "if" = 3
1.1472 - | eta_expander s =
1.1473 - if NameSpace.is_qualified s
1.1474 - then case get_def module s
1.1475 - of Datatypecons dtname =>
1.1476 - (case get_def module dtname
1.1477 - of Datatype (_, cs, _) =>
1.1478 - let val l = AList.lookup (op =) cs s |> the |> length
1.1479 - in if l >= 2 then l else 0 end)
1.1480 - | _ =>
1.1481 - const_syntax s
1.1482 - |> Option.map (fst o fst)
1.1483 - |> the_default 0
1.1484 - else 0;
1.1485 + Pretty.chunks (separate (str "") ps)
1.1486 + ], ());
1.1487 + fun is_cons c = has_nsp c nsp_dtcon;
1.1488 + fun eta_expander c =
1.1489 + const_syntax c
1.1490 + |> Option.map (fst o fst)
1.1491 + |> the_default 0;
1.1492 + fun preprocess module =
1.1493 + module
1.1494 + |> tap (Pretty.writeln o pretty_deps)
1.1495 + |> debug 3 (fn _ => "eta-expanding...")
1.1496 + |> eta_expand eta_expander
1.1497 in
1.1498 - module
1.1499 - |> debug 3 (fn _ => "selecting submodule...")
1.1500 - |> (if is_some select then (partof o the) select else I)
1.1501 - |> debug 3 (fn _ => "eta-expanding...")
1.1502 - |> eta_expand eta_expander
1.1503 - |> debug 3 (fn _ => "serializing...")
1.1504 - |> serialize (haskell_from_defs serializer_name tyco_syntax const_syntax (fn c => has_nsp c nsp_cons)) haskell_from_module haskell_validator nspgrp name_root
1.1505 + abstract_serializer preprocess (haskell_from_defs is_cons, haskell_from_module, abstract_validator reserved_haskell)
1.1506 + (target, (tyco_syntax, const_syntax)) (name_root, nspgrp) I select module
1.1507 end;
1.1508
1.1509 end; (* local *)
1.1510
1.1511 +
1.1512 +(** lookup record **)
1.1513 +
1.1514 +val serializers =
1.1515 + let
1.1516 + fun seri s f = (s, f s);
1.1517 + in {
1.1518 + ml = seri "ml" ml_from_thingol,
1.1519 + haskell = seri "haskell" haskell_from_thingol
1.1520 + } end;
1.1521 +
1.1522 end; (* struct *)
1.1523 -