# HG changeset patch # User haftmann # Date 1156150960 -7200 # Node ID f01ae74f29f23f5d513486830d7202792266a9bb # Parent 0ad2f3bbd4f0383251763e52bc85f9fea911ebcc more concise string serialization diff -r 0ad2f3bbd4f0 -r f01ae74f29f2 src/HOL/List.thy --- a/src/HOL/List.thy Mon Aug 21 11:02:39 2006 +0200 +++ b/src/HOL/List.thy Mon Aug 21 11:02:40 2006 +0200 @@ -2721,16 +2721,28 @@ else NONE | NONE => NONE; +val print_list = Pretty.enum "," "[" "]"; + +fun print_char c = + let + val i = ord c + in if i < 32 + then prefix "\\" (string_of_int i) + else c + end; + +val print_string = quote; + in val list_codegen_setup = Codegen.add_codegen "list_codegen" list_codegen #> Codegen.add_codegen "char_codegen" char_codegen - #> fold (CodegenPackage.add_pretty_list "Nil" "Cons") [ - ("ml", (7, "::")), - ("haskell", (5, ":")) - ] - #> CodegenPackage.add_appconst + #> CodegenPackage.add_pretty_list "ml" "Nil" "Cons" + print_list NONE (7, "::") + #> CodegenPackage.add_pretty_list "haskell" "Nil" "Cons" + print_list (SOME (print_char, print_string)) (5, ":") + #> CodegenPackage.add_appconst_i ("List.char.Char", CodegenPackage.appgen_char dest_char); end; @@ -2776,8 +2788,10 @@ ml (target_atom "char") haskell (target_atom "Char") -code_constapp Char - ml (target_atom "(__,/ __)") +code_constapp + Char + ml (target_atom "(__,/ __)") + haskell (target_atom "(__,/ __)") setup list_codegen_setup diff -r 0ad2f3bbd4f0 -r f01ae74f29f2 src/Pure/Tools/codegen_package.ML --- a/src/Pure/Tools/codegen_package.ML Mon Aug 21 11:02:39 2006 +0200 +++ b/src/Pure/Tools/codegen_package.ML Mon Aug 21 11:02:40 2006 +0200 @@ -19,8 +19,11 @@ -> ((string * CodegenThingol.funn) list -> Pretty.T) * ((string * CodegenThingol.datatyp) list -> Pretty.T); - val add_pretty_list: string -> string -> string * (int * string) - -> theory -> theory; + val add_pretty_list: string -> string -> string -> (Pretty.T list -> Pretty.T) + -> ((string -> string) * (string -> string)) option -> int * string + -> theory -> theory; + val add_pretty_ml_string: string -> string -> string -> string + -> (string -> string) -> (string -> string) -> string -> theory -> theory; val purge_code: theory -> theory; type appgen; @@ -708,6 +711,9 @@ fun eval_term (ref_spec, t) thy = let + val _ = Term.fold_atyps (fn _ => + error ("Term" ^ Sign.string_of_term thy t ^ "is polymorhpic")) + (Term.fastype_of t); fun preprocess_term t = let val x = Free (Name.variant (add_term_names (t, [])) "x", fastype_of t); @@ -845,7 +851,7 @@ #-> (fn reader => pair (mk reader)) end; -fun add_pretty_list raw_nil raw_cons (target, seri) thy = +fun add_pretty_list target raw_nil raw_cons mk_list mk_char_string target_cons thy = let val _ = get_serializer target; fun prep_const raw = @@ -859,12 +865,30 @@ idf_of_const thy (snd tabs) c_ty; val nil'' = mk_const nil'; val cons'' = mk_const cons'; - val pr = CodegenSerializer.pretty_list nil'' cons'' seri; + val pr = CodegenSerializer.pretty_list nil'' cons'' mk_list mk_char_string target_cons; in thy |> add_pretty_syntax_const cons'' target pr end; +fun add_pretty_ml_string target raw_nil raw_cons raw_str mk_char mk_string target_implode thy = + let + val _ = get_serializer target; + fun prep_const raw = + let + val c = Sign.intern_const thy raw + in (c, Sign.the_const_type thy c) end; + val cs' = map prep_const [raw_nil, raw_cons, raw_str]; + val tabs = mk_tabs thy NONE cs'; + fun mk_const c_ty = + idf_of_const thy (snd tabs) c_ty; + val [nil', cons', str'] = map mk_const cs'; + val pr = CodegenSerializer.pretty_ml_string nil' cons' mk_char mk_string target_implode; + in + thy + |> add_pretty_syntax_const str' target pr + end; + (** code basis change notifications **) 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) =