diff -r 0ad2f3bbd4f0 -r f01ae74f29f2 src/Pure/Tools/codegen_serializer.ML --- a/src/Pure/Tools/codegen_serializer.ML Mon Aug 21 11:02:39 2006 +0200 +++ b/src/Pure/Tools/codegen_serializer.ML Mon Aug 21 11:02:40 2006 +0200 @@ -20,7 +20,11 @@ * OuterParse.token list; val parse_syntax: ('b -> int) -> (string -> 'b -> 'a * 'b) -> OuterParse.token list -> ('b -> 'a pretty_syntax * 'b) * OuterParse.token list; - val pretty_list: string -> string -> int * string -> CodegenThingol.iterm pretty_syntax; + val pretty_list: string -> string -> (Pretty.T list -> Pretty.T) + -> ((string -> string) * (string -> string)) option + -> int * string -> CodegenThingol.iterm pretty_syntax; + val pretty_ml_string: string -> string -> (string -> string) -> (string -> string) + -> string -> CodegenThingol.iterm pretty_syntax; val serializers: { ml: string * (string -> serializer), haskell: string * (string * string list -> serializer) @@ -305,29 +309,56 @@ | _ => SOME) | _ => Scan.fail ()); -(* list serializer *) -fun pretty_list thingol_nil thingol_cons (target_pred, target_cons) = +(* list and string serializers *) + +fun implode_list c_nil c_cons e = let fun dest_cons (IConst (c, _) `$ e1 `$ e2) = - if c = thingol_cons + if c = c_cons then SOME (e1, e2) else NONE | dest_cons _ = NONE; - fun pretty_default fxy pr e1 e2 = - brackify_infix (target_pred, R) fxy [ - pr (INFX (target_pred, X)) e1, + val (es, e') = CodegenThingol.unfoldr dest_cons e; + in case e' + of IConst (c, _) => if c = c_nil then SOME es else NONE + | _ => NONE + end; + +fun implode_string mk_char mk_string es = + if forall (fn IChar _ => true | _ => false) es + then (SOME o str o mk_string o implode o map (fn IChar (c, _) => mk_char c)) es + else NONE; + +fun pretty_ml_string c_nil c_cons mk_char mk_string target_implode = + let + fun pretty fxy pr [e] = + case implode_list c_nil c_cons e + of SOME es => (case implode_string mk_char mk_string es + of SOME p => p + | NONE => Pretty.block [str target_implode, Pretty.brk 1, pr BR e]) + | NONE => Pretty.block [str target_implode, Pretty.brk 1, pr BR e] + in ((1, 1), pretty) end; + +fun pretty_list c_nil c_cons mk_list mk_char_string (target_fxy, target_cons) = + let + fun default fxy pr e1 e2 = + brackify_infix (target_fxy, R) fxy [ + pr (INFX (target_fxy, X)) e1, str target_cons, - pr (INFX (target_pred, R)) e2 + pr (INFX (target_fxy, R)) e2 ]; - fun pretty_compact fxy pr [e1, e2] = - case CodegenThingol.unfoldr dest_cons e2 - of (es, IConst (c, _)) => - if c = thingol_nil - then Pretty.enum "," "[" "]" (map (pr NOBR) (e1::es)) - else pretty_default fxy pr e1 e2 - | _ => pretty_default fxy pr e1 e2; - in ((2, 2), pretty_compact) end; + fun pretty fxy pr [e1, e2] = + case Option.map (cons e1) (implode_list c_nil c_cons e2) + of SOME es => + (case mk_char_string + of SOME (mk_char, mk_string) => + (case implode_string mk_char mk_string es + of SOME p => p + | NONE => mk_list (map (pr NOBR) es)) + | NONE => mk_list (map (pr NOBR) es)) + | NONE => default fxy pr e1 e2; + in ((2, 2), pretty) end; @@ -336,8 +367,9 @@ local val reserved_ml = ThmDatabase.ml_reserved @ [ - "bool", "int", "list", "unit", "option", "true", "false", "not", "None", "Some", "o" -]; (* FIXME None/Some no longer used *) + "bool", "int", "list", "unit", "option", "true", "false", "not", "NONE", "SOME", + "o", "string", "char", "String", "Term" +]; structure NameMangler = NameManglerFun ( type ctxt = string list; @@ -355,17 +387,18 @@ val ml_from_label = str o translate_string (fn "_" => "__" | "." => "_" | c => c) o NameSpace.base o resolv; + fun ml_from_dictvar v = + str (Symbol.to_ascii_upper v ^ "_"); fun ml_from_tyvar (v, []) = str "()" | ml_from_tyvar (v, sort) = let - val w = Symbol.to_ascii_upper v; fun mk_class class = str (prefix "'" v ^ " " ^ resolv class); in Pretty.block [ str "(", - str w, + ml_from_dictvar v, str ":", case sort of [class] => mk_class class @@ -380,17 +413,17 @@ if (is_some o Int.fromString) l then str l else ml_from_label l ]; - fun from_lookup fxy [] v = - v - | from_lookup fxy [l] v = + fun from_lookup fxy [] p = + p + | from_lookup fxy [l] p = brackify fxy [ from_label l, - v + p ] - | from_lookup fxy ls v = + | from_lookup fxy ls p = brackify fxy [ Pretty.enum " o" "(" ")" (map from_label ls), - v + p ]; fun from_classlookup fxy (Instance (inst, lss)) = brackify fxy ( @@ -399,10 +432,10 @@ ) | from_classlookup fxy (Lookup (classes, (v, ~1))) = from_lookup BR classes - ((str o Symbol.to_ascii_upper) v) + (ml_from_dictvar v) | from_classlookup fxy (Lookup (classes, (v, i))) = from_lookup BR (string_of_int (i+1) :: classes) - ((str o Symbol.to_ascii_upper) v) + (ml_from_dictvar v) in case lss of [] => str "()" | [ls] => from_classlookup fxy ls @@ -757,9 +790,16 @@ str ("end; (* struct " ^ name ^ " *)") ]); val is_cons = ml_annotators nsp_dtcon; + fun postproc (shallow, n) = + let + fun ch_first f = String.implode o nth_map 0 f o String.explode; + in if shallow = nsp_dtcon + then ch_first Char.toUpper n + else n + end; in abstract_serializer (target, nspgrp) root_name (ml_from_defs is_cons, ml_from_module, - abstract_validator reserved_ml, snd) end; + abstract_validator reserved_ml, postproc) end; in @@ -786,8 +826,10 @@ let val (val_name, modl') = CodegenThingol.add_eval_def (nsp_eval, e) modl; val struct_name = "EVAL"; + fun output p = if !eval_verbose then (Pretty.writeln p; Pretty.output p) + else Pretty.output p; val serializer = ml_serializer struct_name "ml" nsp_dtcon nspgrp - (fn "" => (fn p => (use_text Context.ml_output (!eval_verbose) (Pretty.output p); NONE)) + (fn "" => (fn p => (use_text Context.ml_output (!eval_verbose) (output p); NONE)) | _ => SOME) (K NONE, syntax_tyco, syntax_const) (hidden, SOME [NameSpace.pack [nsp_eval, val_name]]); val _ = serializer modl'; val val_name_struct = NameSpace.append struct_name val_name; @@ -951,22 +993,19 @@ ] |> SOME else SOME body end | hs_from_def (name, CodegenThingol.Typesyn (sctxt, ty)) = - Pretty.block [ - str "type ", + (Pretty.block o Pretty.breaks) [ + str "type", hs_from_sctxt_tycoexpr (sctxt, (resolv_here name, map (ITyVar o fst) sctxt)), - str " =", - Pretty.brk 1, + str "=", hs_from_sctxt_type ([], ty) ] |> SOME - | hs_from_def (name, CodegenThingol.Datatype (sctxt, [(co, tys)])) = + | hs_from_def (name, CodegenThingol.Datatype (sctxt, [(co, [ty])])) = (Pretty.block o Pretty.breaks) [ str "newtype", hs_from_sctxt_tycoexpr (sctxt, (resolv_here name, map (ITyVar o fst) sctxt)), str "=", - (Pretty.block o Pretty.breaks) ( - (str o resolv_here) co - :: map (hs_from_type BR) tys - ) + (str o resolv_here) co, + hs_from_type BR ty ] |> SOME | hs_from_def (name, CodegenThingol.Datatype (sctxt, constrs)) = let @@ -1036,7 +1075,8 @@ "import", "default", "forall", "let", "in", "class", "qualified", "data", "newtype", "instance", "if", "then", "else", "type", "as", "do", "module" ] @ [ - "Bool", "Integer", "Maybe", "True", "False", "Nothing", "Just", "not", "negate" + "Bool", "Integer", "Maybe", "True", "False", "Nothing", "Just", "not", "negate", + "String", "Char" ]; fun is_cons c = CodegenThingol.has_nsp c nsp_dtcon; fun hs_from_module resolv imps ((_, name), ps) =