# HG changeset patch # User haftmann # Date 1160751171 -7200 # Node ID 425883e01fe0fb252da9c973f060682d298cd63c # Parent 3b0c2641f740c5cccd324d16b1668e4b2ebff8d3 improved framework diff -r 3b0c2641f740 -r 425883e01fe0 src/Pure/Tools/codegen_serializer.ML --- a/src/Pure/Tools/codegen_serializer.ML Fri Oct 13 16:52:49 2006 +0200 +++ b/src/Pure/Tools/codegen_serializer.ML Fri Oct 13 16:52:51 2006 +0200 @@ -21,7 +21,7 @@ val add_serializer : string * serializer -> theory -> theory; val ml_from_thingol: serializer; val hs_from_thingol: serializer; - val get_serializer: theory -> string * Args.T list + val get_serializer: theory -> string -> Args.T list -> string list option -> CodegenThingol.code -> unit; val const_has_serialization: theory -> string list -> string -> bool; @@ -143,7 +143,7 @@ | _ => error ("Malformed mixfix annotation: " ^ quote s) end; -fun parse_syntax num_args = +fun parse_syntax tokens = let fun is_arg (Arg _) = true | is_arg _ = false; @@ -153,10 +153,9 @@ error ("Mixfix contains just one pretty element; either declare as " ^ quote atomK ^ " or consider adding a break") | x => x; - fun mk fixity mfx ctxt = + fun mk fixity mfx = let val i = (length o List.filter is_arg) mfx; - val _ = if i > num_args ctxt then error "Too many arguments in code syntax" else (); in (i, fillin_mixfix fixity mfx) end; val parse = ( OuterParse.$$$ infixK |-- OuterParse.nat @@ -169,7 +168,7 @@ || pair (parse_nonatomic, BR) ) -- OuterParse.string >> (fn ((p, fxy), s) => (p s, fxy)); in - parse #-> (fn (mfx, fixity) => pair (mk fixity mfx)) + (parse >> (fn (mfx, fixity) => mk fixity mfx)) tokens end; @@ -190,7 +189,7 @@ 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 + 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 = @@ -226,7 +225,6 @@ (* variable name contexts *) -(*FIXME could name.ML do th whole job?*) fun make_vars names = (fold (fn name => Symtab.update_new (name, name)) names Symtab.empty, Name.make_context names); @@ -262,6 +260,7 @@ end; + (** SML serializer **) datatype ml_def = @@ -356,26 +355,33 @@ brackify fxy [pr_term vars NOBR t1, pr_term vars BR t2]) | pr_term vars fxy (t as _ `|-> _) = let - val (ts, t') = CodegenThingol.unfold_abs t; - fun pr (p, _) vars = - let - val vs = CodegenThingol.fold_varnames (insert (op =)) p []; - val vars' = intro_vars vs vars; - in - ((Pretty.block o Pretty.breaks) [str "fn", pr_term vars' NOBR p, str "=>"], vars') - end; - val (ps, vars') = fold_map pr ts vars; - in brackify BR (ps @ [pr_term vars' NOBR t']) end - | pr_term vars fxy (INum (n, _)) = + val (ps, t') = CodegenThingol.unfold_abs t; + fun pr ((v, NONE), _) vars = + let + val vars' = intro_vars [v] vars; + in + ((Pretty.block o Pretty.breaks) [str "fn", str (lookup_var vars' v), str "=>"], vars') + end + | pr ((v, SOME p), _) vars = + let + val vs = CodegenThingol.fold_varnames (insert (op =)) p [v]; + val vars' = intro_vars vs vars; + in + ((Pretty.block o Pretty.breaks) [str "fn", str (lookup_var vars' v), str "as", + pr_term vars' NOBR p, str "=>"], vars') + end; + val (ps', vars') = fold_map pr ps vars; + in brackify BR (ps' @ [pr_term vars' NOBR t']) end + | pr_term vars fxy (INum n) = brackify BR [(str o IntInf.toString) n, str ":", str "IntInf.int"] - | pr_term vars _ (IChar (c, _)) = + | pr_term vars _ (IChar c) = (str o prefix "#" o quote) (let val i = ord c in if i < 32 then prefix "\\" (string_of_int i) else c end) - | pr_term vars fxy (t as ICase ((_, [_]), _)) = + | pr_term vars fxy (t as ICase (_, [_])) = let val (ts, t') = CodegenThingol.unfold_let t; fun mk ((p, _), t'') vars = @@ -400,7 +406,7 @@ [str ("in"), Pretty.fbrk, pr_term vars' NOBR t'] |> Pretty.block, str ("end") ] end - | pr_term vars fxy (ICase (((td, ty), b::bs), _)) = + | pr_term vars fxy (ICase ((td, ty), b::bs)) = let fun pr definer (p, t) = let @@ -651,34 +657,38 @@ (str o lookup_var vars) v | pr_term vars fxy (t as _ `|-> _) = let - val (ts, t') = CodegenThingol.unfold_abs t; - fun pr (p, _) vars = - let - val vs = CodegenThingol.fold_varnames (insert (op =)) p []; - val vars' = intro_vars vs vars; - in (pr_term vars' BR p, vars') end; - val (ps, vars') = fold_map pr ts vars; + val (ps, t') = CodegenThingol.unfold_abs t; + fun pr ((v, SOME p), _) vars = + let + val vs = CodegenThingol.fold_varnames (insert (op =)) p [v]; + val vars' = intro_vars vs vars; + in ((Pretty.block o Pretty.breaks) [str (lookup_var vars' v), str "@", pr_term vars' BR p], vars') end + | pr ((v, NONE), _) vars = + let + val vars' = intro_vars [v] vars; + in (str (lookup_var vars' v), vars') end; + val (ps', vars') = fold_map pr ps vars; in brackify BR ( str "\\" - :: ps @ [ + :: ps' @ [ str "->", pr_term vars' NOBR t' ]) end - | pr_term vars fxy (INum (n, _)) = + | pr_term vars fxy (INum n) = if n > 0 then (str o IntInf.toString) n else brackify BR [(str o Library.prefix "-" o IntInf.toString o IntInf.~) n] - | pr_term vars fxy (IChar (c, _)) = + | pr_term vars fxy (IChar c) = (str o enclose "'" "'") (let val i = (Char.ord o the o Char.fromString) c in if i < 32 then Library.prefix "\\" (string_of_int i) else c end) - | pr_term vars fxy (t as ICase ((_, [_]), _)) = + | pr_term vars fxy (t as ICase (_, [_])) = let val (ts, t) = CodegenThingol.unfold_let t; fun pr ((p, _), t) vars = @@ -697,7 +707,7 @@ [str ("let"), Pretty.fbrk, binds |> Pretty.chunks] |> Pretty.block, [str ("in "), pr_term vars' NOBR t] |> Pretty.block ] end - | pr_term vars fxy (ICase (((td, _), bs), _)) = + | pr_term vars fxy (ICase ((td, _), bs)) = let fun pr (p, t) = let @@ -832,8 +842,40 @@ ) classop_defs) ] end |> SOME + | pr_def (_, CodegenThingol.Bot) = + NONE; in pr_def def end; +val reserved_haskell = [ + "hiding", "deriving", "where", "case", "of", "infix", "infixl", "infixr", + "import", "default", "forall", "let", "in", "class", "qualified", "data", + "newtype", "instance", "if", "then", "else", "type", "as", "do", "module" +]; + +fun seri_haskell module_prefix destination reserved_user module_alias module_prolog + class_syntax tyco_syntax const_syntax code = + let + val init_vars = make_vars (reserved_haskell @ reserved_user); + in () end; + + + +(** diagnosis serializer **) + +fun seri_diagnosis _ _ _ _ _ code = + let + val init_vars = make_vars reserved_haskell; + val pr = pr_haskell (K NONE) (K NONE) (K NONE) init_vars I I; + in + [] + |> Graph.fold (fn (name, (def, _)) => + case pr (name, def) of SOME p => cons p | NONE => I) code + |> separate (Pretty.str "") + |> Pretty.chunks + |> Pretty.writeln + end; + + (** generic abstract serializer **) @@ -1011,32 +1053,17 @@ (("", name_root), (mk_contents [] root_module)) end; -fun abstract_serializer (target, nspgrp) name_root (from_defs, from_module, validator, postproc) - postprocess (class_syntax, tyco_syntax, const_syntax) - (drop, select) code = +fun abstract_serializer nspgrp name_root (from_defs, from_module, validator, postproc) + postprocess + reserved_user module_alias module_prolog class_syntax tyco_syntax const_syntax + code = let - fun project NONE code = code - | project (SOME names) code = - let - fun check name = if member (op =) drop name - then error ("shadowed definition " ^ quote name ^ " selected for serialization") - else if can (Graph.get_node code) name - then () - else error ("dropped definition " ^ quote name ^ " selected for serialization") - val names' = (map o tap) check names; - in CodegenThingol.project_code names code end; fun from_module' resolv imps ((name_qual, name), defs) = from_module resolv imps ((name_qual, name), defs) |> postprocess (resolv name_qual); in - code - |> tracing (fn _ => "dropping shadowed definitions...") - |> CodegenThingol.delete_garbage drop - |> tracing (fn _ => "projecting...") - |> project select - |> tracing (fn _ => "serializing...") - |> code_serialize (from_defs (class_syntax, tyco_syntax, const_syntax)) - from_module' validator postproc nspgrp name_root + code_serialize (from_defs (class_syntax, tyco_syntax, const_syntax)) + from_module' validator postproc nspgrp name_root code |> K () end; @@ -1087,7 +1114,7 @@ fun parse_single_file serializer = parse_args (Args.name >> (fn path => serializer - (fn "" => write_file false (Path.unpack path) #> K NONE + (fn "" => Pretty.setmp_margin 80 (write_file false (Path.unpack path)) #> K NONE | _ => SOME))); fun parse_multi_file postprocess_module ext serializer = @@ -1163,7 +1190,7 @@ | defs => error ("Illegal mutual dependencies: " ^ (commas o map fst) defs) end; -fun ml_serializer root_name target nspgrp = +fun ml_serializer root_name nspgrp = let fun ml_from_module resolv _ ((_, name), ps) = Pretty.chunks ([ @@ -1181,15 +1208,15 @@ then ch_first Char.toUpper n else n end; - in abstract_serializer (target, nspgrp) + in abstract_serializer nspgrp root_name (ml_from_defs, ml_from_module, abstract_validator (ThmDatabase.ml_reserved @ reserved_ml'), postproc) end; in -fun ml_from_thingol target args = +fun ml_from_thingol args = let - val serializer = ml_serializer "ROOT" target [[nsp_module], [nsp_class, nsp_tyco], + val serializer = ml_serializer "ROOT" [[nsp_module], [nsp_class, nsp_tyco], [nsp_fun, nsp_dtco, nsp_class, nsp_classop, nsp_inst]] val parse_multi = Args.name @@ -1207,18 +1234,18 @@ val eval_verbose = ref false; -fun eval_term_proto thy data hidden ((ref_name, reff), e) code = +fun eval_term_proto thy data1 data2 data3 data4 data5 data6 hidden ((ref_name, reff), e) code = let val (val_name, code') = CodegenThingol.add_eval_def (nsp_eval, e) code; + val code'' = CodegenThingol.project_code hidden (SOME [NameSpace.pack [nsp_eval, val_name]]) code'; 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 "SML" [[nsp_module], [nsp_class, nsp_tyco], + val serializer = ml_serializer struct_name [[nsp_module], [nsp_class, nsp_tyco], [nsp_fun, nsp_dtco, nsp_class, nsp_classop, nsp_inst], [nsp_eval]] (fn "" => (fn p => (use_text Output.ml_output (!eval_verbose) (output p); NONE)) - | _ => SOME) data - (hidden, SOME [NameSpace.pack [nsp_eval, val_name]]); - val _ = serializer code'; + | _ => SOME) data1 data2 data3 data4 data5 data6; + val _ = serializer code''; val val_name_struct = NameSpace.append struct_name val_name; val _ = reff := NONE; val _ = use_text Output.ml_output (!eval_verbose) ("val _ = (" ^ ref_name ^ " := SOME (" ^ val_name_struct ^ "))"); @@ -1252,7 +1279,7 @@ (** haskell serializer **) -fun hs_from_thingol target args = +fun hs_from_thingol args = let fun hs_from_defs keyword_vars (class_syntax, tyco_syntax, const_syntax) deresolver prefix defs = let @@ -1286,8 +1313,8 @@ then ch_first Char.toUpper n else ch_first Char.toLower n end; - val serializer = abstract_serializer (target, [[nsp_module], - [nsp_class], [nsp_tyco], [nsp_fun, nsp_classop], [nsp_dtco], [nsp_inst]]) + val serializer = abstract_serializer [[nsp_module], + [nsp_class], [nsp_tyco], [nsp_fun, nsp_classop], [nsp_dtco], [nsp_inst]] "Main" (hs_from_defs (make_vars reserved_hs), hs_from_module, abstract_validator reserved_hs, postproc); in (parse_multi_file ((K o K) NONE) "hs" serializer) args @@ -1318,55 +1345,48 @@ ); datatype syntax_modl = SyntaxModl of { - merge: string Symtab.table, + alias: string Symtab.table, prolog: Pretty.T Symtab.table }; -fun mk_syntax_modl (merge, prolog) = - SyntaxModl { merge = merge, prolog = prolog }; -fun map_syntax_modl f (SyntaxModl { merge, prolog }) = - mk_syntax_modl (f (merge, prolog)); -fun merge_syntax_modl (SyntaxModl { merge = merge1, prolog = prolog1 }, - SyntaxModl { merge = merge2, prolog = prolog2 }) = +fun mk_syntax_modl (alias, prolog) = + SyntaxModl { alias = alias, prolog = prolog }; +fun map_syntax_modl f (SyntaxModl { alias, prolog }) = + mk_syntax_modl (f (alias, prolog)); +fun merge_syntax_modl (SyntaxModl { alias = alias1, prolog = prolog1 }, + SyntaxModl { alias = alias2, prolog = prolog2 }) = mk_syntax_modl ( - Symtab.merge (op =) (merge1, merge2), + Symtab.merge (op =) (alias1, alias2), Symtab.merge (op =) (prolog1, prolog2) ); -type serializer = string -> Args.T list --> (string -> (string * (string -> string option)) option) - * (string - -> (int - * (fixity - -> (fixity - -> itype -> Pretty.T) - -> itype list -> Pretty.T)) - option) - * (string - -> (int - * (fixity - -> (fixity - -> iterm -> Pretty.T) - -> iterm list -> Pretty.T)) - option) - -> string list * string list option - -> CodegenThingol.code -> unit; +type serializer = Args.T list + -> string list + -> (string -> string option) + -> (string -> Pretty.T option) + -> (string -> (string * (string -> string option)) option) + -> (string -> (int * (fixity -> (fixity -> itype -> Pretty.T) -> itype list -> Pretty.T)) option) + -> (string -> (int * (fixity -> (fixity -> iterm -> Pretty.T) -> iterm list -> Pretty.T)) option) + -> CodegenThingol.code -> unit; datatype target = Target of { serial: serial, serializer: serializer, syntax_expr: syntax_expr, - syntax_modl: syntax_modl + syntax_modl: syntax_modl, + reserved: string list }; -fun mk_target (serial, (serializer, (syntax_expr, syntax_modl))) = - Target { serial = serial, serializer = serializer, syntax_expr = syntax_expr, syntax_modl = syntax_modl }; -fun map_target f ( Target { serial, serializer, syntax_expr, syntax_modl } ) = - mk_target (f (serial, (serializer, (syntax_expr, syntax_modl)))); -fun merge_target target (Target { serial = serial1, serializer = serializer, syntax_expr = syntax_expr1, syntax_modl = syntax_modl1 }, - Target { serial = serial2, serializer = _, syntax_expr = syntax_expr2, syntax_modl = syntax_modl2 }) = +fun mk_target (serial, ((serializer, reserved), (syntax_expr, syntax_modl))) = + Target { serial = serial, reserved = reserved, serializer = serializer, syntax_expr = syntax_expr, syntax_modl = syntax_modl }; +fun map_target f ( Target { serial, serializer, reserved, syntax_expr, syntax_modl } ) = + mk_target (f (serial, ((serializer, reserved), (syntax_expr, syntax_modl)))); +fun merge_target target (Target { serial = serial1, serializer = serializer, reserved = reserved1, + syntax_expr = syntax_expr1, syntax_modl = syntax_modl1 }, + Target { serial = serial2, serializer = _, reserved = reserved2, + syntax_expr = syntax_expr2, syntax_modl = syntax_modl2 }) = if serial1 = serial2 then - mk_target (serial1, (serializer, + mk_target (serial1, ((serializer, merge (op =) (reserved1, reserved2)), (merge_syntax_expr (syntax_expr1, syntax_expr2), merge_syntax_modl (syntax_modl1, syntax_modl2)) )) @@ -1385,6 +1405,7 @@ end); fun the_serializer (Target { serializer, ... }) = serializer; +fun the_reserved (Target { reserved, ... }) = reserved; fun the_syntax_expr (Target { syntax_expr = SyntaxExpr x, ... }) = x; fun the_syntax_modl (Target { syntax_modl = SyntaxModl x, ... }) = x; @@ -1396,29 +1417,47 @@ in thy |> (CodegenSerializerData.map oo Symtab.map_default) - (target, mk_target (serial (), (seri, + (target, mk_target (serial (), ((seri, []), (mk_syntax_expr ((Symtab.empty, Symtab.empty), (Symtab.empty, Symtab.empty)), mk_syntax_modl (Symtab.empty, Symtab.empty))))) - (map_target (fn (serial, (_, syntax)) => (serial, (seri, syntax)))) + (map_target (fn (serial, ((_, keywords), syntax)) => (serial, ((seri, keywords), syntax)))) end; +fun map_seri_data target f thy = + let + val _ = if is_some (Symtab.lookup (CodegenSerializerData.get thy) target) + then () + else error ("Unknown code target language: " ^ quote target); + in + thy + |> (CodegenSerializerData.map o Symtab.map_entry target o map_target) f + end; + +val target_diag = "diag"; + val _ = Context.add_setup ( CodegenSerializerData.init #> add_serializer ("SML", ml_from_thingol) #> add_serializer ("Haskell", hs_from_thingol) + #> add_serializer (target_diag, (fn _ => fn _ => seri_diagnosis)) ); -fun get_serializer thy (target, args) cs = +fun get_serializer thy target args cs = let val data = case Symtab.lookup (CodegenSerializerData.get thy) target of SOME data => data | NONE => error ("Unknown code target language: " ^ quote target); val seri = the_serializer data; + val reserved = the_reserved data; + val { alias, prolog } = the_syntax_modl data; val { class, inst, tyco, const } = the_syntax_expr data; fun fun_of sys = (Option.map fst oo Symtab.lookup) sys; + val project = if target = target_diag then I + else CodegenThingol.project_code + (Symtab.keys class @ Symtab.keys inst @ Symtab.keys tyco @ Symtab.keys const) cs; in - seri target args (fun_of class, fun_of tyco, fun_of const) - (Symtab.keys class @ Symtab.keys inst @ Symtab.keys tyco @ Symtab.keys const, cs) + project #> seri args reserved (Symtab.lookup alias) (Symtab.lookup prolog) + (fun_of class) (fun_of tyco) (fun_of const) end; fun has_serialization f thy targets name = @@ -1436,10 +1475,12 @@ val data = case Symtab.lookup (CodegenSerializerData.get thy) target of SOME data => data | NONE => error ("Unknown code target language: " ^ quote target); + val reserved = the_reserved data; + val { alias, prolog } = the_syntax_modl data; val { class, inst, tyco, const } = the_syntax_expr data; fun fun_of sys = (Option.map fst oo Symtab.lookup) sys; in - eval_term_proto thy (fun_of class, fun_of tyco, fun_of const) + eval_term_proto thy reserved (Symtab.lookup alias) (Symtab.lookup prolog) (fun_of class) (fun_of tyco) (fun_of const) (Symtab.keys class @ Symtab.keys inst @ Symtab.keys tyco @ Symtab.keys const) end; @@ -1449,16 +1490,12 @@ local -fun map_syntax_exprs target f thy = - let - val _ = if is_some (Symtab.lookup (CodegenSerializerData.get thy) target) - then () - else error ("Unknown code target language: " ^ quote target); - in - thy - |> (CodegenSerializerData.map o Symtab.map_entry target o map_target - o apsnd o apsnd o apfst o map_syntax_expr) f - end; +fun map_syntax_exprs target = + map_seri_data target o (apsnd o apsnd o apfst o map_syntax_expr); +fun map_syntax_modls target = + map_seri_data target o (apsnd o apsnd o apsnd o map_syntax_modl); +fun map_reserveds target = + map_seri_data target o (apsnd o apfst o apsnd); fun gen_add_syntax_class prep_class prep_const target raw_class (syntax, raw_ops) thy = let @@ -1485,23 +1522,30 @@ (Symtab.update (inst, ())) end; -fun gen_add_syntax_tyco prep_tyco raw_tyco target syntax thy = +fun gen_add_syntax_tyco prep_tyco target raw_tyco (syntax as (n, _)) thy = let - val tyco = (CodegenNames.tyco thy o prep_tyco thy) raw_tyco; + val tyco = prep_tyco thy raw_tyco; + val tyco' = CodegenNames.tyco thy tyco; + val _ = if n > Sign.arity_number thy tyco + then error ("Too many arguments in syntax for type constructor " ^ quote tyco) + else () in thy |> (map_syntax_exprs target o apsnd o apfst) - (Symtab.update (tyco, (syntax, serial ()))) + (Symtab.update (tyco', (syntax, serial ()))) end; -fun gen_add_syntax_const prep_const raw_c target syntax thy = +fun gen_add_syntax_const prep_const target raw_c (syntax as (n, _)) thy = let - val c' = prep_const thy raw_c; - val c'' = CodegenNames.const thy c'; + val c = prep_const thy raw_c; + val c' = CodegenNames.const thy c; + val _ = if n > (length o fst o strip_type o Sign.the_const_type thy o fst) c + then error ("Too many arguments in syntax for constant " ^ (quote o fst) c) + else () in thy |> (map_syntax_exprs target o apsnd o apsnd) - (Symtab.update (c'', (syntax, serial ()))) + (Symtab.update (c', (syntax, serial ()))) end; fun read_type thy raw_tyco = @@ -1517,11 +1561,26 @@ val cs'' = map (CodegenConsts.norm_of_typ thy) cs'; in AList.make (CodegenNames.const thy) cs'' end; -fun parse_quote num_of consts_of target get_init adder = - parse_syntax num_of #-> (fn mfx => pair (fn thy => adder target (mfx thy) thy)); +val add_syntax_class = gen_add_syntax_class ClassPackage.read_class CodegenConsts.read_const; +val add_syntax_inst = gen_add_syntax_inst ClassPackage.read_class read_type; +val add_syntax_tyco = gen_add_syntax_tyco read_type; +val add_syntax_const = gen_add_syntax_const CodegenConsts.read_const; + +fun add_reserved target = + map_reserveds target o insert (op =); + +fun add_modl_alias target = + map_syntax_modls target o apfst o Symtab.update o apsnd CodegenNames.check_modulename; + +fun add_modl_prolog target = + map_syntax_modls target o apsnd o + (fn (modl, NONE) => Symtab.delete modl | (modl, SOME prolog) => + Symtab.update (modl, Pretty.str prolog)); fun zip_list (x::xs) f g = - f x #-> (fn y => fold_map (fn x => g |-- f x >> pair x) xs + f + #-> (fn y => + fold_map (fn x => g |-- f >> pair x) xs #-> (fn xys => pair ((x, y) :: xys))); structure P = OuterParse @@ -1529,44 +1588,47 @@ fun parse_multi_syntax parse_thing parse_syntax = P.and_list1 parse_thing - #-> (fn things => Scan.repeat1 (P.$$$ "(" |-- P.name :-- - (fn target => zip_list things (parse_syntax target) - (P.$$$ "and")) --| P.$$$ ")")) + #-> (fn things => Scan.repeat1 (P.$$$ "(" |-- P.name -- + (zip_list things parse_syntax (P.$$$ "and")) --| P.$$$ ")")); -val add_syntax_class = gen_add_syntax_class ClassPackage.read_class CodegenConsts.read_const; -val add_syntax_inst = gen_add_syntax_inst ClassPackage.read_class read_type; +val (code_classK, code_instanceK, code_typeK, code_constK, + code_reservedK, code_modulenameK, code_moduleprologK) = + ("code_class", "code_instance", "code_type", "code_const", + "code_reserved", "code_modulename", "code_moduleprolog"); -fun parse_syntax_tyco target raw_tyco = +in + +fun add_pretty_list target nill cons mk_list mk_char_string target_cons thy = let - fun intern thy = read_type thy raw_tyco; - fun num_of thy = Sign.arity_number thy (intern thy); - fun idf_of thy = CodegenNames.tyco thy (intern thy); - fun read_typ thy = - Sign.read_typ (thy, K NONE); + val [(_, nil''), (cons', cons'')] = idfs_of_const_names thy [nill, cons]; + val pr = pretty_list nil'' cons'' mk_list mk_char_string target_cons; in - parse_quote num_of ((K o K) ([], [])) target idf_of - (gen_add_syntax_tyco read_type raw_tyco) + thy + |> gen_add_syntax_const (K I) target cons' pr end; -fun parse_syntax_const target raw_const = +fun add_pretty_ml_string target nill cons str mk_char mk_string target_implode thy = let - fun intern thy = CodegenConsts.read_const thy raw_const; - fun num_of thy = (length o fst o strip_type o Sign.the_const_type thy o fst o intern) thy; - fun idf_of thy = (CodegenNames.const thy o intern) thy; + val [(_, nil''), (_, cons''), (str', _)] = idfs_of_const_names thy [nill, cons, str]; + val pr = pretty_ml_string nil'' cons'' mk_char mk_string target_implode; in - parse_quote num_of CodegenConsts.consts_of target idf_of - (gen_add_syntax_const CodegenConsts.read_const raw_const) + thy + |> gen_add_syntax_const (K I) target str' pr end; -val (code_classK, code_instanceK, code_typeK, code_constK) = - ("code_class", "code_instance", "code_type", "code_const"); - -in +fun add_undefined target undef target_undefined thy = + let + val [(undef', _)] = idfs_of_const_names thy [undef]; + fun pretty _ _ _ = str target_undefined; + in + thy + |> gen_add_syntax_const (K I) target undef' (~1, pretty) + end; val code_classP = OuterSyntax.command code_classK "define code syntax for class" K.thy_decl ( parse_multi_syntax P.xname - (fn _ => fn _ => P.string -- Scan.optional (P.$$$ "where" |-- Scan.repeat1 + (P.string -- Scan.optional (P.$$$ "where" |-- Scan.repeat1 (P.term --| (P.$$$ "\\" || P.$$$ "==") -- P.string)) []) >> (Toplevel.theory oo fold) (fn (target, syns) => fold (fn (raw_class, syn) => add_syntax_class target raw_class syn) syns) @@ -1575,7 +1637,7 @@ val code_instanceP = OuterSyntax.command code_instanceK "define code syntax for instance" K.thy_decl ( parse_multi_syntax (P.xname --| P.$$$ "::" -- P.xname) - (fn _ => fn _ => P.name #-> + (P.name #-> (fn "-" => Scan.succeed () | _ => Scan.fail_with (fn _ => "\"-\" expected") ())) >> (Toplevel.theory oo fold) (fn (target, syns) => fold (fn (raw_inst, ()) => add_syntax_inst target raw_inst) syns) @@ -1583,48 +1645,38 @@ val code_typeP = OuterSyntax.command code_typeK "define code syntax for type constructor" K.thy_decl ( - Scan.repeat1 ( - parse_multi_syntax P.xname parse_syntax_tyco - ) - >> (Toplevel.theory o (fold o fold) (fold snd o snd)) + parse_multi_syntax P.xname parse_syntax + >> (Toplevel.theory oo fold) (fn (target, syns) => + fold (fn (raw_tyco, syn) => add_syntax_tyco target raw_tyco syn) syns) ); val code_constP = OuterSyntax.command code_constK "define code syntax for constant" K.thy_decl ( - Scan.repeat1 ( - parse_multi_syntax P.term parse_syntax_const - ) - >> (Toplevel.theory o (fold o fold) (fold snd o snd)) + parse_multi_syntax P.term parse_syntax + >> (Toplevel.theory oo fold) (fn (target, syns) => + fold (fn (raw_const, syn) => add_syntax_const target raw_const syn) syns) ); -val _ = OuterSyntax.add_parsers [code_classP, code_instanceP, code_typeP, code_constP]; - -fun add_pretty_list target nill cons mk_list mk_char_string target_cons thy = - let - val [(_, nil''), (cons', cons'')] = idfs_of_const_names thy [nill, cons]; - val pr = pretty_list nil'' cons'' mk_list mk_char_string target_cons; - in - thy - |> gen_add_syntax_const (K I) cons' target pr - end; +val code_reservedP = + OuterSyntax.command code_reservedK "declare words as reserved for target language" K.thy_decl ( + P.name -- Scan.repeat1 P.name + >> (fn (target, reserveds) => (Toplevel.theory o fold (add_reserved target)) reserveds) + ) -fun add_pretty_ml_string target nill cons str mk_char mk_string target_implode thy = - let - val [(_, nil''), (_, cons''), (str', _)] = idfs_of_const_names thy [nill, cons, str]; - val pr = pretty_ml_string nil'' cons'' mk_char mk_string target_implode; - in - thy - |> gen_add_syntax_const (K I) str' target pr - end; +val code_modulenameP = + OuterSyntax.command code_reservedK "alias module to other name" K.thy_decl ( + P.name -- Scan.repeat1 (P.name -- P.name) + >> (fn (target, modlnames) => (Toplevel.theory o fold (add_modl_alias target)) modlnames) + ) -fun add_undefined target undef target_undefined thy = - let - val [(undef', _)] = idfs_of_const_names thy [undef]; - fun pretty _ _ _ = str target_undefined; - in - thy - |> gen_add_syntax_const (K I) undef' target (~1, pretty) - end; +val code_moduleprologP = + OuterSyntax.command code_reservedK "add prolog to module" K.thy_decl ( + P.name -- Scan.repeat1 (P.name -- (P.string >> (fn "-" => NONE | s => SOME s))) + >> (fn (target, prologs) => (Toplevel.theory o fold (add_modl_prolog target)) prologs) + ) + +val _ = OuterSyntax.add_parsers [code_classP, code_instanceP, code_typeP, code_constP, + code_reservedP, code_modulenameP, code_moduleprologP]; end; (*local*)