1.1 --- a/src/Pure/Tools/codegen_serializer.ML Mon Oct 09 20:12:45 2006 +0200
1.2 +++ b/src/Pure/Tools/codegen_serializer.ML Tue Oct 10 09:17:17 2006 +0200
1.3 @@ -9,35 +9,7 @@
1.4 signature CODEGEN_SERIALIZER =
1.5 sig
1.6 include BASIC_CODEGEN_THINGOL;
1.7 - val get_serializer: theory -> string * Args.T list
1.8 - -> string list option -> CodegenThingol.code -> unit;
1.9 - val eval_verbose: bool ref;
1.10 - val eval_term: theory ->
1.11 - (string * 'a option ref) * CodegenThingol.iterm -> CodegenThingol.code
1.12 - -> 'a;
1.13 - val const_has_serialization: theory -> string list -> string -> bool;
1.14 - val tyco_has_serialization: theory -> string list -> string -> bool;
1.15 - val add_syntax_class:
1.16 - string -> string -> string * (string * string) list -> theory -> theory;
1.17 - val add_syntax_inst: string -> (string * string) -> theory -> theory;
1.18 - val parse_syntax_tyco: (theory
1.19 - -> CodegenConsts.const list * (string * typ) list
1.20 - -> string
1.21 - -> CodegenNames.tyco
1.22 - -> typ list -> CodegenThingol.itype list)
1.23 - -> Symtab.key
1.24 - -> xstring
1.25 - -> OuterParse.token list
1.26 - -> (theory -> theory) * OuterParse.token list;
1.27 - val parse_syntax_const: (theory
1.28 - -> CodegenConsts.const list * (string * typ) list
1.29 - -> string
1.30 - -> CodegenNames.const
1.31 - -> term list -> CodegenThingol.iterm list)
1.32 - -> Symtab.key
1.33 - -> string
1.34 - -> OuterParse.token list
1.35 - -> (theory -> theory) * OuterParse.token list;
1.36 +
1.37 val add_pretty_list: string -> string -> string -> (Pretty.T list -> Pretty.T)
1.38 -> ((string -> string) * (string -> string)) option -> int * string
1.39 -> theory -> theory;
1.40 @@ -45,11 +17,20 @@
1.41 -> (string -> string) -> (string -> string) -> string -> theory -> theory;
1.42 val add_undefined: string -> string -> string -> theory -> theory;
1.43
1.44 - type fixity;
1.45 type serializer;
1.46 val add_serializer : string * serializer -> theory -> theory;
1.47 val ml_from_thingol: serializer;
1.48 val hs_from_thingol: serializer;
1.49 + val get_serializer: theory -> string * Args.T list
1.50 + -> string list option -> CodegenThingol.code -> unit;
1.51 +
1.52 + val const_has_serialization: theory -> string list -> string -> bool;
1.53 + val tyco_has_serialization: theory -> string list -> string -> bool;
1.54 +
1.55 + val eval_verbose: bool ref;
1.56 + val eval_term: theory ->
1.57 + (string * 'a option ref) * CodegenThingol.iterm -> CodegenThingol.code
1.58 + -> 'a;
1.59 end;
1.60
1.61 structure CodegenSerializer: CODEGEN_SERIALIZER =
1.62 @@ -120,8 +101,7 @@
1.63
1.64 datatype 'a mixfix =
1.65 Arg of fixity
1.66 - | Pretty of Pretty.T
1.67 - | Quote of 'a;
1.68 + | Pretty of Pretty.T;
1.69
1.70 fun fillin_mixfix fxy_this ms fxy_ctxt pr args =
1.71 let
1.72 @@ -131,8 +111,6 @@
1.73 pr fxy a :: fillin ms args
1.74 | fillin (Pretty p :: ms) args =
1.75 p :: fillin ms args
1.76 - | fillin (Quote q :: ms) args =
1.77 - pr BR q :: fillin ms args
1.78 | fillin [] _ =
1.79 error ("Inconsistent mixfix: too many arguments")
1.80 | fillin _ [] =
1.81 @@ -146,44 +124,40 @@
1.82 val r = case x of R => fixity
1.83 | _ => INFX (i, X);
1.84 in
1.85 - pair [Arg l, (Pretty o Pretty.brk) 1, (Pretty o str) s, (Pretty o Pretty.brk) 1, Arg r]
1.86 + [Arg l, (Pretty o Pretty.brk) 1, (Pretty o str) s, (Pretty o Pretty.brk) 1, Arg r]
1.87 end;
1.88
1.89 -fun parse_mixfix reader s ctxt =
1.90 +fun parse_mixfix s =
1.91 let
1.92 - fun sym s = Scan.lift ($$ s);
1.93 - fun lift_reader ctxt s =
1.94 - ctxt
1.95 - |> reader s
1.96 - |-> (fn x => pair (Quote x));
1.97 - val sym_any = Scan.lift (Scan.one Symbol.not_eof);
1.98 + val sym_any = Scan.one Symbol.not_eof;
1.99 val parse = Scan.repeat (
1.100 - (sym "_" -- sym "_" >> K (Arg NOBR))
1.101 - || (sym "_" >> K (Arg BR))
1.102 - || (sym "/" |-- Scan.repeat (sym " ") >> (Pretty o Pretty.brk o length))
1.103 - || Scan.depend (fn ctxt => $$ "{" |-- $$ "*" |-- Scan.repeat1
1.104 - ( $$ "'" |-- Scan.one Symbol.not_eof
1.105 - || Scan.unless ($$ "*" -- $$ "}") (Scan.one Symbol.not_eof)) --|
1.106 - $$ "*" --| $$ "}" >> (implode #> lift_reader ctxt #> swap))
1.107 + ($$ "_" -- $$ "_" >> K (Arg NOBR))
1.108 + || ($$ "_" >> K (Arg BR))
1.109 + || ($$ "/" |-- Scan.repeat ($$ " ") >> (Pretty o Pretty.brk o length))
1.110 || (Scan.repeat1
1.111 - ( sym "'" |-- sym_any
1.112 - || Scan.unless (sym "_" || sym "?" || sym "/" || sym "{" |-- sym "*")
1.113 + ( $$ "'" |-- sym_any
1.114 + || Scan.unless ($$ "_" || $$ "/")
1.115 sym_any) >> (Pretty o str o implode)));
1.116 - in case Scan.finite' Symbol.stopper parse (ctxt, Symbol.explode s)
1.117 - of (p, (ctxt, [])) => (p, ctxt)
1.118 + in case Scan.finite Symbol.stopper parse (Symbol.explode s)
1.119 + of (p, []) => p
1.120 | _ => error ("Malformed mixfix annotation: " ^ quote s)
1.121 end;
1.122
1.123 -fun parse_syntax num_args reader =
1.124 +fun parse_syntax num_args =
1.125 let
1.126 fun is_arg (Arg _) = true
1.127 | is_arg _ = false;
1.128 - fun parse_nonatomic s ctxt =
1.129 - case parse_mixfix reader s ctxt
1.130 - of ([Pretty _], _) =>
1.131 + fun parse_nonatomic s =
1.132 + case parse_mixfix s
1.133 + of [Pretty _] =>
1.134 error ("Mixfix contains just one pretty element; either declare as "
1.135 ^ quote atomK ^ " or consider adding a break")
1.136 | x => x;
1.137 + fun mk fixity mfx ctxt =
1.138 + let
1.139 + val i = (length o List.filter is_arg) mfx;
1.140 + val _ = if i > num_args ctxt then error "Too many arguments in code syntax" else ();
1.141 + in (i, fillin_mixfix fixity mfx) end;
1.142 val parse = (
1.143 OuterParse.$$$ infixK |-- OuterParse.nat
1.144 >> (fn i => (parse_infix (INFX (i, X)), INFX (i, X)))
1.145 @@ -191,19 +165,11 @@
1.146 >> (fn i => (parse_infix (INFX (i, L)), INFX (i, L)))
1.147 || OuterParse.$$$ infixrK |-- OuterParse.nat
1.148 >> (fn i => (parse_infix (INFX (i, R)), INFX (i, R)))
1.149 - || OuterParse.$$$ atomK |-- pair (parse_mixfix reader, NOBR)
1.150 + || OuterParse.$$$ atomK |-- pair (parse_mixfix, NOBR)
1.151 || pair (parse_nonatomic, BR)
1.152 ) -- OuterParse.string >> (fn ((p, fxy), s) => (p s, fxy));
1.153 - fun mk fixity mfx ctxt =
1.154 - let
1.155 - val i = (length o List.filter is_arg) mfx;
1.156 - val _ = if i > num_args ctxt then error "Too many arguments in code syntax" else ();
1.157 - in ((i, fillin_mixfix fixity mfx), ctxt) end;
1.158 in
1.159 - parse
1.160 - #-> (fn (mfx_reader, fixity) =>
1.161 - pair (mfx_reader #-> (fn mfx => (mk fixity mfx)))
1.162 - )
1.163 + parse #-> (fn (mfx, fixity) => pair (mk fixity mfx))
1.164 end;
1.165
1.166
1.167 @@ -858,7 +824,7 @@
1.168 ) classop_defs)
1.169 ]
1.170 end |> SOME
1.171 - in pr_def def end;
1.172 + in Pretty.setmp_margin 999999 pr_def def end;
1.173
1.174
1.175 (** generic abstract serializer **)
1.176 @@ -1320,138 +1286,6 @@
1.177 end;
1.178
1.179
1.180 -(** LEGACY DIAGNOSIS **)
1.181 -
1.182 -local
1.183 -
1.184 -open CodegenThingol;
1.185 -
1.186 -in
1.187 -
1.188 -val pretty_typparms =
1.189 - Pretty.list "(" ")" o Pretty.commas o map (fn (v, sort) => (Pretty.block o Pretty.breaks)
1.190 - [Pretty.str v, Pretty.str "::", Pretty.enum "&" "" "" (map Pretty.str sort)]);
1.191 -
1.192 -fun pretty_itype (tyco `%% tys) =
1.193 - Pretty.enum "" "(" ")" (Pretty.str tyco :: map pretty_itype tys)
1.194 - | pretty_itype (ty1 `-> ty2) =
1.195 - Pretty.enum "" "(" ")" [pretty_itype ty1, Pretty.str "->", pretty_itype ty2]
1.196 - | pretty_itype (ITyVar v) =
1.197 - Pretty.str v;
1.198 -
1.199 -fun pretty_iterm (IConst (c, _)) =
1.200 - Pretty.str c
1.201 - | pretty_iterm (IVar v) =
1.202 - Pretty.str ("?" ^ v)
1.203 - | pretty_iterm (t1 `$ t2) =
1.204 - (Pretty.enclose "(" ")" o Pretty.breaks)
1.205 - [pretty_iterm t1, pretty_iterm t2]
1.206 - | pretty_iterm ((v, ty) `|-> t) =
1.207 - (Pretty.enclose "(" ")" o Pretty.breaks)
1.208 - [Pretty.str v, Pretty.str "::", pretty_itype ty, Pretty.str "|->", pretty_iterm t]
1.209 - | pretty_iterm (INum (n, _)) =
1.210 - (Pretty.str o IntInf.toString) n
1.211 - | pretty_iterm (IChar (h, _)) =
1.212 - (Pretty.str o quote) h
1.213 - | pretty_iterm (ICase (((t, _), bs), _)) =
1.214 - (Pretty.enclose "(" ")" o Pretty.breaks) [
1.215 - Pretty.str "case",
1.216 - pretty_iterm t,
1.217 - Pretty.enclose "(" ")" (map (fn (p, t) =>
1.218 - (Pretty.block o Pretty.breaks) [
1.219 - pretty_iterm p,
1.220 - Pretty.str "=>",
1.221 - pretty_iterm t
1.222 - ]
1.223 - ) bs)
1.224 - ];
1.225 -
1.226 -fun pretty_def Bot =
1.227 - Pretty.str "<Bot>"
1.228 - | pretty_def (Fun (eqs, (vs, ty))) =
1.229 - Pretty.enum " |" "" "" (
1.230 - map (fn (ps, body) =>
1.231 - Pretty.block [
1.232 - Pretty.enum "," "[" "]" (map pretty_iterm ps),
1.233 - Pretty.str " |->",
1.234 - Pretty.brk 1,
1.235 - pretty_iterm body,
1.236 - Pretty.str "::",
1.237 - pretty_typparms vs,
1.238 - Pretty.str "/",
1.239 - pretty_itype ty
1.240 - ]) eqs
1.241 - )
1.242 - | pretty_def (Datatype (vs, cs)) =
1.243 - Pretty.block [
1.244 - pretty_typparms vs,
1.245 - Pretty.str " |=> ",
1.246 - Pretty.enum " |" "" ""
1.247 - (map (fn (c, tys) => (Pretty.block o Pretty.breaks)
1.248 - (Pretty.str c :: map pretty_itype tys)) cs)
1.249 - ]
1.250 - | pretty_def (Datatypecons dtname) =
1.251 - Pretty.str ("cons " ^ dtname)
1.252 - | pretty_def (Class (supcls, (v, mems))) =
1.253 - Pretty.block [
1.254 - Pretty.str ("class var " ^ v ^ " extending "),
1.255 - Pretty.enum "," "[" "]" (map Pretty.str supcls),
1.256 - Pretty.str " with ",
1.257 - Pretty.enum "," "[" "]"
1.258 - (map (fn (m, ty) => Pretty.block
1.259 - [Pretty.str (m ^ "::"), pretty_itype ty]) mems)
1.260 - ]
1.261 - | pretty_def (Classmember clsname) =
1.262 - Pretty.block [
1.263 - Pretty.str "class member belonging to ",
1.264 - Pretty.str clsname
1.265 - ]
1.266 - | pretty_def (Classinst ((clsname, (tyco, arity)), _)) =
1.267 - Pretty.block [
1.268 - Pretty.str "class instance (",
1.269 - Pretty.str clsname,
1.270 - Pretty.str ", (",
1.271 - Pretty.str tyco,
1.272 - Pretty.str ", ",
1.273 - Pretty.enum "," "[" "]" (map (Pretty.enum "," "{" "}" o
1.274 - map Pretty.str o snd) arity),
1.275 - Pretty.str "))"
1.276 - ];
1.277 -
1.278 -fun pretty_module code =
1.279 - Pretty.chunks (map (fn (name, def) => Pretty.block
1.280 - [Pretty.str name, Pretty.str " :=", Pretty.brk 1, pretty_def def])
1.281 - (AList.make (Graph.get_node code) (Graph.strong_conn code |> flat |> rev)));
1.282 -
1.283 -fun pretty_deps code =
1.284 - let
1.285 - fun one_node key =
1.286 - let
1.287 - val preds_ = Graph.imm_preds code key;
1.288 - val succs_ = Graph.imm_succs code key;
1.289 - val mutbs = gen_inter (op =) (preds_, succs_);
1.290 - val preds = subtract (op =) mutbs preds_;
1.291 - val succs = subtract (op =) mutbs succs_;
1.292 - in
1.293 - (Pretty.block o Pretty.fbreaks) (
1.294 - Pretty.str key
1.295 - :: map (fn s => Pretty.str ("<-> " ^ s)) mutbs
1.296 - @ map (fn s => Pretty.str ("<-- " ^ s)) preds
1.297 - @ map (fn s => Pretty.str ("--> " ^ s)) succs
1.298 - )
1.299 - end
1.300 - in
1.301 - code
1.302 - |> Graph.strong_conn
1.303 - |> flat
1.304 - |> rev
1.305 - |> map one_node
1.306 - |> Pretty.chunks
1.307 - end;
1.308 -
1.309 -end; (*local*)
1.310 -
1.311 -
1.312
1.313 (** theory data **)
1.314
1.315 @@ -1603,7 +1437,7 @@
1.316
1.317
1.318
1.319 -(** target syntax interfaces **)
1.320 +(** ML and toplevel interface **)
1.321
1.322 local
1.323
1.324 @@ -1675,26 +1509,26 @@
1.325 val cs'' = map (CodegenConsts.norm_of_typ thy) cs';
1.326 in AList.make (CodegenNames.const thy) cs'' end;
1.327
1.328 -fun read_quote reader consts_of target get_init gen raw_it thy =
1.329 - let
1.330 - val it = reader thy raw_it;
1.331 - val cs = consts_of thy it;
1.332 - in
1.333 - gen thy cs target (get_init thy) [it]
1.334 - |> (fn [it'] => (it', thy))
1.335 - end;
1.336 +fun parse_quote num_of consts_of target get_init adder =
1.337 + parse_syntax num_of #-> (fn mfx => pair (fn thy => adder target (mfx thy) thy));
1.338
1.339 -fun parse_quote num_of reader consts_of target get_init gen adder =
1.340 - parse_syntax num_of
1.341 - (read_quote reader consts_of target get_init gen)
1.342 - #-> (fn modifier => pair (modifier #-> adder target));
1.343 +fun zip_list (x::xs) f g =
1.344 + f x #-> (fn y => fold_map (fn x => g |-- f x >> pair x) xs
1.345 + #-> (fn xys => pair ((x, y) :: xys)));
1.346
1.347 -in
1.348 +structure P = OuterParse
1.349 +and K = OuterKeyword
1.350 +
1.351 +fun parse_multi_syntax parse_thing parse_syntax =
1.352 + P.and_list1 parse_thing
1.353 + #-> (fn things => Scan.repeat1 (P.$$$ "(" |-- P.name :--
1.354 + (fn target => zip_list things (parse_syntax target)
1.355 + (P.$$$ "and")) --| P.$$$ ")"))
1.356
1.357 val add_syntax_class = gen_add_syntax_class ClassPackage.read_class CodegenConsts.read_const;
1.358 val add_syntax_inst = gen_add_syntax_inst ClassPackage.read_class read_type;
1.359
1.360 -fun parse_syntax_tyco generate target raw_tyco =
1.361 +fun parse_syntax_tyco target raw_tyco =
1.362 let
1.363 fun intern thy = read_type thy raw_tyco;
1.364 fun num_of thy = Sign.arity_number thy (intern thy);
1.365 @@ -1702,20 +1536,61 @@
1.366 fun read_typ thy =
1.367 Sign.read_typ (thy, K NONE);
1.368 in
1.369 - parse_quote num_of read_typ ((K o K) ([], [])) target idf_of generate
1.370 + parse_quote num_of ((K o K) ([], [])) target idf_of
1.371 (gen_add_syntax_tyco read_type raw_tyco)
1.372 end;
1.373
1.374 -fun parse_syntax_const generate target raw_const =
1.375 +fun parse_syntax_const target raw_const =
1.376 let
1.377 fun intern thy = CodegenConsts.read_const thy raw_const;
1.378 fun num_of thy = (length o fst o strip_type o Sign.the_const_type thy o fst o intern) thy;
1.379 fun idf_of thy = (CodegenNames.const thy o intern) thy;
1.380 in
1.381 - parse_quote num_of Sign.read_term CodegenConsts.consts_of target idf_of generate
1.382 + parse_quote num_of CodegenConsts.consts_of target idf_of
1.383 (gen_add_syntax_const CodegenConsts.read_const raw_const)
1.384 end;
1.385
1.386 +val (code_classK, code_instanceK, code_typeK, code_constK) =
1.387 + ("code_class", "code_instance", "code_type", "code_const");
1.388 +
1.389 +in
1.390 +
1.391 +val code_classP =
1.392 + OuterSyntax.command code_classK "define code syntax for class" K.thy_decl (
1.393 + parse_multi_syntax P.xname
1.394 + (fn _ => fn _ => P.string -- Scan.optional (P.$$$ "where" |-- Scan.repeat1
1.395 + (P.term --| (P.$$$ "\\<equiv>" || P.$$$ "==") -- P.string)) [])
1.396 + >> (Toplevel.theory oo fold) (fn (target, syns) =>
1.397 + fold (fn (raw_class, syn) => add_syntax_class target raw_class syn) syns)
1.398 + );
1.399 +
1.400 +val code_instanceP =
1.401 + OuterSyntax.command code_instanceK "define code syntax for instance" K.thy_decl (
1.402 + parse_multi_syntax (P.xname --| P.$$$ "::" -- P.xname)
1.403 + (fn _ => fn _ => P.name #->
1.404 + (fn "-" => Scan.succeed () | _ => Scan.fail_with (fn _ => "\"-\" expected") ()))
1.405 + >> (Toplevel.theory oo fold) (fn (target, syns) =>
1.406 + fold (fn (raw_inst, ()) => add_syntax_inst target raw_inst) syns)
1.407 + );
1.408 +
1.409 +val code_typeP =
1.410 + OuterSyntax.command code_typeK "define code syntax for type constructor" K.thy_decl (
1.411 + Scan.repeat1 (
1.412 + parse_multi_syntax P.xname parse_syntax_tyco
1.413 + )
1.414 + >> (Toplevel.theory o (fold o fold) (fold snd o snd))
1.415 + );
1.416 +
1.417 +val code_constP =
1.418 + OuterSyntax.command code_constK "define code syntax for constant" K.thy_decl (
1.419 + Scan.repeat1 (
1.420 + parse_multi_syntax P.term parse_syntax_const
1.421 + )
1.422 + >> (Toplevel.theory o (fold o fold) (fold snd o snd))
1.423 + );
1.424 +
1.425 +val _ = OuterSyntax.add_parsers [code_classP, code_instanceP, code_typeP, code_constP];
1.426 +
1.427 fun add_pretty_list target nill cons mk_list mk_char_string target_cons thy =
1.428 let
1.429 val [(_, nil''), (cons', cons'')] = idfs_of_const_names thy [nill, cons];