diff -r fa38cca42913 -r d0071d93978e src/Pure/Tools/codegen_serializer.ML --- a/src/Pure/Tools/codegen_serializer.ML Mon Dec 12 15:36:46 2005 +0100 +++ b/src/Pure/Tools/codegen_serializer.ML Mon Dec 12 15:37:05 2005 +0100 @@ -143,7 +143,7 @@ local -fun ml_from_defs tyco_syntax const_syntax resolv ds = +fun ml_from_defs tyco_syntax const_syntax is_dicttype resolv ds = let fun chunk_defs ps = let @@ -340,14 +340,6 @@ Pretty.str "true" | ml_from_app br ("False", []) = Pretty.str "false" - | ml_from_app br ("primeq", [e1, e2]) = - brackify (eval_br br (INFX (4, L))) [ - ml_from_expr (INFX (4, L)) e1, - Pretty.str "=", - ml_from_expr (INFX (4, X)) e2, - Pretty.str ":", - ml_from_type NOBR (itype_of_iexpr e2) - ] | ml_from_app br ("Pair", [e1, e2]) = Pretty.list "(" ")" [ ml_from_expr NOBR e1, @@ -417,6 +409,7 @@ in mk_app_p br (pr (map (ml_from_expr BR) es1) (ml_from_expr BR)) es2 end; fun ml_from_funs (ds as d::ds_tl) = let + val _ = debug 15 (fn _ => "(1) FUN") (); fun mk_definer [] = "val" | mk_definer _ = "fun" fun check_args (_, Fun ((pats, _)::_, _)) NONE = @@ -427,19 +420,39 @@ else error ("mixing simultaneous vals and funs not implemented") | check_args _ _ = error ("function definition block containing other definitions than functions") + val _ = debug 15 (fn _ => "(2) FUN") (); val definer = the (fold check_args ds NONE); + val _ = debug 15 (fn _ => "(3) FUN") (); fun mk_eq definer f ty (pats, expr) = let + val _ = debug 15 (fn _ => "(5) FUN") (); + fun mk_pat_arg p = + case itype_of_ipat p + of ty as IType (tyco, _) => + if is_dicttype tyco + then Pretty.block [ + Pretty.str "(", + ml_from_pat NOBR p, + Pretty.str ":", + ml_from_type NOBR ty, + Pretty.str ")" + ] + else ml_from_pat BR p + | _ => ml_from_pat BR p; + val _ = debug 15 (fn _ => "(6) FUN") (); val lhs = [Pretty.str (definer ^ " " ^ f)] @ (if null pats then [Pretty.str ":", ml_from_type NOBR ty] - else map (ml_from_pat BR) pats) + else map mk_pat_arg pats) + val _ = debug 15 (fn _ => "(7) FUN") (); val rhs = [Pretty.str "=", ml_from_expr NOBR expr] + val _ = debug 15 (fn _ => "(8) FUN") (); in Pretty.block (separate (Pretty.brk 1) (lhs @ rhs)) end fun mk_fun definer (f, Fun (eqs as eq::eq_tl, (_, ty))) = let + val _ = debug 15 (fn _ => "(4) FUN") (); val (pats_hd::pats_tl) = (fst o split_list) eqs; val shift = if null eq_tl then I else map (Pretty.block o single); in (Pretty.block o Pretty.fbreaks o shift) ( @@ -507,7 +520,7 @@ NONE | ml_from_def (name, Classinst _) = error ("can't serialize instance declaration " ^ quote name ^ " to ML") - in (debug 10 (fn _ => "*** defs " ^ commas (map fst ds)) (); + in (debug 10 (fn _ => "*** defs " ^ commas (map (fn (n, d) => n ^ " = " ^ (Pretty.output o pretty_def) d) ds)) (); case ds of (_, Fun _)::_ => ml_from_funs ds | (_, Datatypecons _)::_ => ml_from_datatypes ds @@ -547,9 +560,12 @@ Pretty.str "", Pretty.str ("end; (* struct " ^ name ^ " *)") ]); + fun is_dicttype tyco = + case get_def module tyco + of Typesyn (_, IDictT _) => true + | _ => false; fun eta_expander "Pair" = 2 | eta_expander "Cons" = 2 - | eta_expander "primeq" = 2 | eta_expander "and" = 2 | eta_expander "or" = 2 | eta_expander "if" = 3 @@ -569,7 +585,7 @@ const_syntax s |> Option.map fst |> the_default 0 - else 0 + else 0; in module |> debug 12 (Pretty.output o pretty_module) @@ -584,8 +600,8 @@ |> debug 3 (fn _ => "eliminating classes...") |> eliminate_classes |> debug 12 (Pretty.output o pretty_module) - |> debug 3 (fn _ => "generating...") - |> serialize (ml_from_defs tyco_syntax const_syntax) ml_from_module ml_validator nspgrp name_root + |> debug 3 (fn _ => "serializing...") + |> serialize (ml_from_defs tyco_syntax const_syntax is_dicttype) ml_from_module ml_validator nspgrp name_root |> (fn p => Pretty.chunks [setmp print_mode [] (Pretty.str o mk_prims) prims, p]) end; @@ -807,12 +823,6 @@ Pretty.str "[]" | haskell_from_app br ("Cons", es) = mk_app_p br (Pretty.str "(:)") es - | haskell_from_app br ("primeq", [e1, e2]) = - brackify (eval_br br (INFX (4, L))) [ - haskell_from_expr (INFX (4, L)) e1, - Pretty.str "==", - haskell_from_expr (INFX (4, X)) e2 - ] | haskell_from_app br ("eq", [e1, e2]) = brackify (eval_br br (INFX (4, L))) [ haskell_from_expr (INFX (4, L)) e1, @@ -884,7 +894,9 @@ else error ("empty statement during serialization: " ^ quote name) | haskell_from_def (name, Fun (eqs, (_, ty))) = let + val _ = print "(1) FUN"; fun from_eq name (args, rhs) = + (print args; print rhs; Pretty.block [ Pretty.str (lower_first name), Pretty.block (map (fn p => Pretty.block [Pretty.brk 1, haskell_from_pat BR p]) args), @@ -892,7 +904,8 @@ Pretty.str ("="), Pretty.brk 1, haskell_from_expr NOBR rhs - ] + ]) + val _ = print "(2) FUN"; in Pretty.chunks [ Pretty.block [ @@ -953,6 +966,17 @@ end | haskell_from_def (name, Classmember _) = NONE + | haskell_from_def (_, Classinst ("Eq", (tyco, arity), [(_, eqpred)])) = + Pretty.block [ + Pretty.str "instance ", + haskell_from_sctxt arity, + Pretty.str "Eq", + Pretty.str " ", + haskell_from_type NOBR (IType (tyco, (map (IVarT o rpair [] o fst)) arity)), + Pretty.str " where", + Pretty.fbrk, + Pretty.str ("(==) = " ^ (lower_first o resolv) eqpred) + ] |> SOME | haskell_from_def (_, Classinst (clsname, (tyco, arity), instmems)) = Pretty.block [ Pretty.str "instance ", @@ -967,7 +991,7 @@ ) instmems) ] |> SOME in - case List.mapPartial (fn (name, def) => haskell_from_def (name, def)) defs + case List.mapPartial (fn (name, def) => (print ("serializing " ^ name); haskell_from_def (name, def))) defs of [] => NONE | l => (SOME o Pretty.block) l end; @@ -1028,7 +1052,7 @@ |> (if is_some select then (partof o the) select else I) |> debug 3 (fn _ => "eta-expanding...") |> eta_expand eta_expander - |> debug 3 (fn _ => "generating...") + |> debug 3 (fn _ => "serializing...") |> serialize (haskell_from_defs tyco_syntax const_syntax is_cons) haskell_from_module haskell_validator nspgrp name_root |> (fn p => Pretty.chunks [setmp print_mode [] (Pretty.str o mk_prims) prims, p]) end;