# HG changeset patch # User haftmann # Date 1211969209 -7200 # Node ID e8a40d8b7897db7d9beb9f92e40d46410e13b2f8 # Parent 284c871d3acb126f54b19e9ecff391c771f15dfe new serializer interface diff -r 284c871d3acb -r e8a40d8b7897 src/Tools/code/code_package.ML --- a/src/Tools/code/code_package.ML Wed May 28 11:05:47 2008 +0200 +++ b/src/Tools/code/code_package.ML Wed May 28 12:06:49 2008 +0200 @@ -97,9 +97,13 @@ fun code thy permissive cs seris = let val code = Program.get thy; - val seris' = map (fn (((target, module), file), args) => - CodeTarget.get_serializer thy target permissive module file args cs) seris; - in (map (fn f => f code) seris' : unit list; ()) end; + fun mk_seri_dest file = case file + of NONE => CodeTarget.compile + | SOME "-" => writeln o CodeTarget.string + | SOME f => CodeTarget.file (Path.explode f) + val _ = map (fn (((target, module), file), args) => + (mk_seri_dest file (CodeTarget.serialize thy target permissive module args code cs))) seris; + in () end; (* evaluation machinery *) @@ -145,7 +149,7 @@ val cs = map (CodeUnit.check_const thy) ts; val (cs', code') = generate thy (CodeFuncgr.make thy cs) (fold_map ooo ensure_const) cs; - val code'' = CodeTarget.sml_of thy cs' code' ^ " ()"; + val code'' = CodeTarget.sml_of thy code' cs' ^ " ()"; in (("codevals", code''), (ctxt', args')) end; diff -r 284c871d3acb -r e8a40d8b7897 src/Tools/code/code_target.ML --- a/src/Tools/code/code_target.ML Wed May 28 11:05:47 2008 +0200 +++ b/src/Tools/code/code_target.ML Wed May 28 12:06:49 2008 +0200 @@ -30,13 +30,16 @@ val allow_exception: string -> theory -> theory; + type serialization; type serializer; val add_serializer: string * serializer -> theory -> theory; val assert_serializer: theory -> string -> string; - val get_serializer: theory -> string -> bool -> string option - -> string option -> Args.T list - -> string list option -> CodeThingol.code -> unit; - val sml_of: theory -> string list -> CodeThingol.code -> string; + val serialize: theory -> string -> bool -> string option -> Args.T list + -> CodeThingol.code -> string list option -> serialization; + val compile: serialization -> unit; + val file: Path.T -> serialization -> unit; + val string: serialization -> string; + val sml_of: theory -> CodeThingol.code -> string list -> string; val eval: theory -> (string * (unit -> 'a) option ref) -> CodeThingol.code -> CodeThingol.iterm * CodeThingol.itype -> string list -> 'a; val code_width: int ref; @@ -64,10 +67,9 @@ val code_width = ref 80; fun code_source p = Pretty.setmp_margin (!code_width) Pretty.string_of p ^ "\n"; -fun code_writeln p = Pretty.setmp_margin (!code_width) Pretty.writeln p; -(** syntax **) +(** generic syntax **) datatype lrx = L | R | X; @@ -111,66 +113,168 @@ -> CodeName.var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T); -(* user-defined syntax *) +(** theory data **) + +val target_diag = "diag"; +val target_SML = "SML"; +val target_OCaml = "OCaml"; +val target_Haskell = "Haskell"; + +datatype syntax_expr = SyntaxExpr of { + class: (string * (string -> string option)) Symtab.table, + inst: unit Symtab.table, + tyco: typ_syntax Symtab.table, + const: term_syntax Symtab.table +}; + +fun mk_syntax_expr ((class, inst), (tyco, const)) = + SyntaxExpr { class = class, inst = inst, tyco = tyco, const = const }; +fun map_syntax_expr f (SyntaxExpr { class, inst, tyco, const }) = + mk_syntax_expr (f ((class, inst), (tyco, const))); +fun merge_syntax_expr (SyntaxExpr { class = class1, inst = inst1, tyco = tyco1, const = const1 }, + SyntaxExpr { class = class2, inst = inst2, tyco = tyco2, const = const2 }) = + mk_syntax_expr ( + (Symtab.join (K snd) (class1, class2), + Symtab.join (K snd) (inst1, inst2)), + (Symtab.join (K snd) (tyco1, tyco2), + Symtab.join (K snd) (const1, const2)) + ); + +datatype serialization_dest = Compile | File of Path.T | String; +type serialization = serialization_dest -> string option; + +fun compile f = (f Compile; ()); +fun file p f = (f (File p); ()); +fun string f = the (f String); + +type serializer = + string option + -> Args.T list + -> (string -> string) + -> string list + -> (string * Pretty.T) list + -> (string -> string option) + -> (string -> class_syntax option) + -> (string -> typ_syntax option) + -> (string -> term_syntax option) + -> CodeThingol.code -> string list -> serialization; -datatype 'a mixfix = - Arg of fixity - | Pretty of Pretty.T; +datatype target = Target of { + serial: serial, + serializer: serializer, + reserved: string list, + includes: Pretty.T Symtab.table, + syntax_expr: syntax_expr, + module_alias: string Symtab.table +}; -fun mk_mixfix prep_arg (fixity_this, mfx) = +fun mk_target ((serial, serializer), ((reserved, includes), (syntax_expr, module_alias))) = + Target { serial = serial, serializer = serializer, reserved = reserved, + includes = includes, syntax_expr = syntax_expr, module_alias = module_alias }; +fun map_target f ( Target { serial, serializer, reserved, includes, syntax_expr, module_alias } ) = + mk_target (f ((serial, serializer), ((reserved, includes), (syntax_expr, module_alias)))); +fun merge_target target (Target { serial = serial1, serializer = serializer, + reserved = reserved1, includes = includes1, + syntax_expr = syntax_expr1, module_alias = module_alias1 }, + Target { serial = serial2, serializer = _, + reserved = reserved2, includes = includes2, + syntax_expr = syntax_expr2, module_alias = module_alias2 }) = + if serial1 = serial2 then + mk_target ((serial1, serializer), + ((merge (op =) (reserved1, reserved2), Symtab.merge (op =) (includes1, includes2)), + (merge_syntax_expr (syntax_expr1, syntax_expr2), + Symtab.join (K snd) (module_alias1, module_alias2)) + )) + else + error ("Incompatible serializers: " ^ quote target); + +structure CodeTargetData = TheoryDataFun +( + type T = target Symtab.table * string list; + val empty = (Symtab.empty, []); + val copy = I; + val extend = I; + fun merge _ ((target1, exc1) : T, (target2, exc2)) = + (Symtab.join merge_target (target1, target2), Library.merge (op =) (exc1, exc2)); +); + +fun the_serializer (Target { serializer, ... }) = serializer; +fun the_reserved (Target { reserved, ... }) = reserved; +fun the_includes (Target { includes, ... }) = includes; +fun the_syntax_expr (Target { syntax_expr = SyntaxExpr x, ... }) = x; +fun the_module_alias (Target { module_alias , ... }) = module_alias; + +fun assert_serializer thy target = + case Symtab.lookup (fst (CodeTargetData.get thy)) target + of SOME data => target + | NONE => error ("Unknown code target language: " ^ quote target); + +fun add_serializer (target, seri) thy = let - fun is_arg (Arg _) = true - | is_arg _ = false; - val i = (length o filter is_arg) mfx; - fun fillin _ [] [] = - [] - | fillin pr (Arg fxy :: mfx) (a :: args) = - (pr fxy o prep_arg) a :: fillin pr mfx args - | fillin pr (Pretty p :: mfx) args = - p :: fillin pr mfx args - | fillin _ [] _ = - error ("Inconsistent mixfix: too many arguments") - | fillin _ _ [] = - error ("Inconsistent mixfix: too less arguments"); + val _ = case Symtab.lookup (fst (CodeTargetData.get thy)) target + of SOME _ => warning ("overwriting existing serializer " ^ quote target) + | NONE => (); in - (i, fn pr => fn fixity_ctxt => fn args => - gen_brackify (fixity fixity_this fixity_ctxt) (fillin pr mfx args)) + thy + |> (CodeTargetData.map o apfst oo Symtab.map_default) + (target, mk_target ((serial (), seri), (([], Symtab.empty), + (mk_syntax_expr ((Symtab.empty, Symtab.empty), (Symtab.empty, Symtab.empty)), + Symtab.empty)))) + ((map_target o apfst o apsnd o K) seri) end; -fun parse_infix prep_arg (x, i) s = +fun map_seri_data target f thy = let - val l = case x of L => INFX (i, L) | _ => INFX (i, X); - val r = case x of R => INFX (i, R) | _ => INFX (i, X); + val _ = assert_serializer thy target; in - mk_mixfix prep_arg (INFX (i, x), - [Arg l, (Pretty o Pretty.brk) 1, (Pretty o str) s, (Pretty o Pretty.brk) 1, Arg r]) + thy + |> (CodeTargetData.map o apfst o Symtab.map_entry target o map_target) f end; -fun parse_mixfix prep_arg s = +fun map_adaptions target = + map_seri_data target o apsnd o apfst; +fun map_syntax_exprs target = + map_seri_data target o apsnd o apsnd o apfst o map_syntax_expr; +fun map_module_alias target = + map_seri_data target o apsnd o apsnd o apsnd; + +fun get_serializer get_seri thy target permissive = let - val sym_any = Scan.one Symbol.is_regular; - val parse = Scan.optional ($$ "!" >> K true) false -- Scan.repeat ( - ($$ "(" -- $$ "_" -- $$ ")" >> K (Arg NOBR)) - || ($$ "_" >> K (Arg BR)) - || ($$ "/" |-- Scan.repeat ($$ " ") >> (Pretty o Pretty.brk o length)) - || (Scan.repeat1 - ( $$ "'" |-- sym_any - || Scan.unless ($$ "_" || $$ "/" || $$ "(" |-- $$ "_" |-- $$ ")") - sym_any) >> (Pretty o str o implode))); - in case Scan.finite Symbol.stopper parse (Symbol.explode s) - of ((_, p as [_]), []) => mk_mixfix prep_arg (NOBR, p) - | ((b, p as _ :: _ :: _), []) => mk_mixfix prep_arg (if b then NOBR else BR, p) - | _ => Scan.!! - (the_default ("malformed mixfix annotation: " ^ quote s) o snd) Scan.fail () + val (seris, exc) = CodeTargetData.get thy; + val data = case Symtab.lookup seris target + of SOME data => data + | NONE => error ("Unknown code target language: " ^ quote target); + val seri = get_seri data; + val reserved = the_reserved data; + val includes = Symtab.dest (the_includes data); + val alias = the_module_alias data; + val { class, inst, tyco, const } = the_syntax_expr data; + val project = if target = target_diag then K I + else CodeThingol.project_code permissive + (Symtab.keys class @ Symtab.keys inst @ Symtab.keys tyco @ Symtab.keys const); + fun check_empty_funs code = case filter_out (member (op =) exc) + (CodeThingol.empty_funs code) + of [] => code + | names => error ("No defining equations for " + ^ commas (map (CodeName.labelled_name thy) names)); + in fn module => fn args => fn code => fn cs => + seri module args (CodeName.labelled_name thy) reserved includes + (Symtab.lookup alias) (Symtab.lookup class) + (Symtab.lookup tyco) (Symtab.lookup const) + ((check_empty_funs o project cs) code) (these cs) end; +val serialize = get_serializer the_serializer; + fun parse_args f args = case Scan.read Args.stopper f args of SOME x => x | NONE => error "Bad serializer arguments"; -(* generic serializer combinators *) +(** generic output combinators **) + +(* applications and bindings *) fun gen_pr_app pr_app' pr_term const_syntax labelled_name is_cons lhs vars fxy (app as ((c, (_, tys)), ts)) = @@ -269,7 +373,7 @@ in CodeThingol.unfoldr dest_monad t end; -(** name auxiliary **) +(* name auxiliary *) val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode; val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode; @@ -914,8 +1018,8 @@ str ("end;; (*struct " ^ name ^ "*)") ]); -fun seri_ml pr_def pr_modl module output labelled_name reserved_syms includes raw_module_alias - (_ : string -> class_syntax option) tyco_syntax const_syntax cs code = +fun seri_ml internal output_cont pr_def pr_modl module labelled_name reserved_syms includes raw_module_alias + (_ : string -> class_syntax option) tyco_syntax const_syntax code cs seri_dest = let val module_alias = if is_some module then K module else raw_module_alias; val is_cons = CodeThingol.is_cons code; @@ -1089,33 +1193,19 @@ val p = Pretty.chunks (separate (str "") (map snd includes @ (map_filter (pr_node [] o Graph.get_node nodes) o rev o flat o Graph.strong_conn) nodes)); val deresolv = try (deresolver (if is_some module then the_list module else [])); - in output (map_filter deresolv cs, p) end; - -fun isar_seri_sml module file = - let - val output = case file - of NONE => use_text (1, "generated code") Output.ml_output false o code_source - | SOME "-" => code_writeln - | SOME file => File.write (Path.explode file) o code_source; - in - parse_args (Scan.succeed ()) - #> (fn () => seri_ml pr_sml pr_sml_modl module (output o snd)) - end; + val output = case seri_dest + of Compile => K NONE o internal o code_source + | File file => K NONE o File.write file o code_source + | String => SOME o code_source; + in output_cont (map_filter deresolv cs, output p) end; -fun eval_seri module file args = - seri_ml pr_sml (K Pretty.chunks) (SOME "Isabelle_Eval") - (fn (cs, p) => "let\n" ^ code_source p ^ "\nin fn () => " ^ enclose "(" ")" (commas cs) ^ " end"); +fun isar_seri_sml module = + parse_args (Scan.succeed ()) + #> (fn () => seri_ml (use_text (1, "generated code") Output.ml_output false) snd pr_sml pr_sml_modl module); -fun isar_seri_ocaml module file = - let - val output = case file - of NONE => error "OCaml: no internal compilation" - | SOME "-" => code_writeln - | SOME file => File.write (Path.explode file) o code_source; - in - parse_args (Scan.succeed ()) - #> (fn () => seri_ml pr_ocaml pr_ocaml_modl module (output o snd)) - end; +fun isar_seri_ocaml module = + parse_args (Scan.succeed ()) + #> (fn () => seri_ml (fn _ => error "OCaml: no internal compilation") snd pr_ocaml pr_ocaml_modl module) (** Haskell serializer **) @@ -1396,11 +1486,10 @@ end; (*local*) -fun seri_haskell module_prefix module destination string_classes labelled_name +fun seri_haskell module_prefix module string_classes labelled_name reserved_syms includes raw_module_alias - class_syntax tyco_syntax const_syntax cs code = + class_syntax tyco_syntax const_syntax code cs seri_dest = let - val _ = Option.map File.check destination; val is_cons = CodeThingol.is_cons code; val contr_classparam_typs = CodeThingol.contr_classparam_typs code; val module_alias = if is_some module then K module else raw_module_alias; @@ -1477,25 +1566,14 @@ deresolv_here (if qualified then deresolv else deresolv_here) is_cons contr_classparam_typs (if string_classes then deriving_show else K false); - fun write_modulefile (SOME destination) modlname = - let - val filename = case modlname - of "" => Path.explode "Main.hs" - | _ => (Path.ext "hs" o Path.explode o implode o separate "/" - o NameSpace.explode) modlname; - val pathname = Path.append destination filename; - val _ = File.mkdir (Path.dir pathname); - in File.write pathname o code_source end - | write_modulefile NONE _ = code_writeln; - fun write_module destination (modulename, content) = - Pretty.chunks [ + fun assemble_module (modulename, content) = + (modulename, code_source (Pretty.chunks [ str ("module " ^ modulename ^ " where {"), str "", content, str "", str "}" - ] - |> write_modulefile destination modulename; + ])); fun seri_module (modlname', (imports, (defs, _))) = let val imports' = @@ -1521,31 +1599,34 @@ (fn (name, (_, SOME def)) => SOME (seri_def qualified (name, def)) | (_, (_, NONE)) => NONE) defs) ) - in - write_module destination (modlname', content) - end; - in ( - map (write_module destination) includes; - Symtab.fold (fn modl => fn () => seri_module modl) code' () - ) end; + in assemble_module (modlname', content) end; + fun write_module destination (modlname, content) = + let + val filename = case modlname + of "" => Path.explode "Main.hs" + | _ => (Path.ext "hs" o Path.explode o implode o separate "/" + o NameSpace.explode) modlname; + val pathname = Path.append destination filename; + val _ = File.mkdir (Path.dir pathname); + in File.write pathname content end + val output = case seri_dest + of Compile => error ("Haskell: no internal compilation") + | File destination => K NONE o map (write_module destination) + | String => SOME o cat_lines o map snd; + in output (map assemble_module includes + @ map seri_module (Symtab.dest code')) + end; -fun isar_seri_haskell module file = - let - val destination = case file - of NONE => error ("Haskell: no internal compilation") - | SOME "-" => NONE - | SOME file => SOME (Path.explode file) - in - parse_args (Scan.option (Args.$$$ "root" -- Args.colon |-- Args.name) - -- Scan.optional (Args.$$$ "string_classes" >> K true) false - >> (fn (module_prefix, string_classes) => - seri_haskell module_prefix module destination string_classes)) - end; +fun isar_seri_haskell module = + parse_args (Scan.option (Args.$$$ "root" -- Args.colon |-- Args.name) + -- Scan.optional (Args.$$$ "string_classes" >> K true) false + >> (fn (module_prefix, string_classes) => + seri_haskell module_prefix module string_classes)); (** diagnosis serializer **) -fun seri_diagnosis labelled_name _ _ _ _ _ _ _ code = +fun seri_diagnosis labelled_name _ _ _ _ _ _ code _ _ = let val init_names = CodeName.make_vars []; fun pr_fun "fun" = SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] => @@ -1562,174 +1643,12 @@ |> Graph.fold (fn (name, (def, _)) => case try pr (name, def) of SOME p => cons p | NONE => I) code |> Pretty.chunks2 - |> code_writeln + |> code_source + |> writeln + |> K NONE end; - -(** theory data **) - -datatype syntax_expr = SyntaxExpr of { - class: (string * (string -> string option)) Symtab.table, - inst: unit Symtab.table, - tyco: typ_syntax Symtab.table, - const: term_syntax Symtab.table -}; - -fun mk_syntax_expr ((class, inst), (tyco, const)) = - SyntaxExpr { class = class, inst = inst, tyco = tyco, const = const }; -fun map_syntax_expr f (SyntaxExpr { class, inst, tyco, const }) = - mk_syntax_expr (f ((class, inst), (tyco, const))); -fun merge_syntax_expr (SyntaxExpr { class = class1, inst = inst1, tyco = tyco1, const = const1 }, - SyntaxExpr { class = class2, inst = inst2, tyco = tyco2, const = const2 }) = - mk_syntax_expr ( - (Symtab.join (K snd) (class1, class2), - Symtab.join (K snd) (inst1, inst2)), - (Symtab.join (K snd) (tyco1, tyco2), - Symtab.join (K snd) (const1, const2)) - ); - -type 'a gen_serializer = - string option - -> string option - -> Args.T list - -> (string -> string) - -> string list - -> (string * Pretty.T) list - -> (string -> string option) - -> (string -> class_syntax option) - -> (string -> typ_syntax option) - -> (string -> term_syntax option) - -> string list -> CodeThingol.code -> 'a; - -type serializer = unit gen_serializer; - -datatype target = Target of { - serial: serial, - serializer: serializer, - reserved: string list, - includes: Pretty.T Symtab.table, - syntax_expr: syntax_expr, - module_alias: string Symtab.table -}; - -fun mk_target ((serial, serializer), ((reserved, includes), (syntax_expr, module_alias))) = - Target { serial = serial, serializer = serializer, reserved = reserved, - includes = includes, syntax_expr = syntax_expr, module_alias = module_alias }; -fun map_target f ( Target { serial, serializer, reserved, includes, syntax_expr, module_alias } ) = - mk_target (f ((serial, serializer), ((reserved, includes), (syntax_expr, module_alias)))); -fun merge_target target (Target { serial = serial1, serializer = serializer, - reserved = reserved1, includes = includes1, - syntax_expr = syntax_expr1, module_alias = module_alias1 }, - Target { serial = serial2, serializer = _, - reserved = reserved2, includes = includes2, - syntax_expr = syntax_expr2, module_alias = module_alias2 }) = - if serial1 = serial2 then - mk_target ((serial1, serializer), - ((merge (op =) (reserved1, reserved2), Symtab.merge (op =) (includes1, includes2)), - (merge_syntax_expr (syntax_expr1, syntax_expr2), - Symtab.join (K snd) (module_alias1, module_alias2)) - )) - else - error ("Incompatible serializers: " ^ quote target); - -structure CodeTargetData = TheoryDataFun -( - type T = target Symtab.table * string list; - val empty = (Symtab.empty, []); - val copy = I; - val extend = I; - fun merge _ ((target1, exc1) : T, (target2, exc2)) = - (Symtab.join merge_target (target1, target2), Library.merge (op =) (exc1, exc2)); -); - -val target_SML = "SML"; -val target_OCaml = "OCaml"; -val target_Haskell = "Haskell"; -val target_diag = "diag"; - -fun the_serializer (Target { serializer, ... }) = serializer; -fun the_reserved (Target { reserved, ... }) = reserved; -fun the_includes (Target { includes, ... }) = includes; -fun the_syntax_expr (Target { syntax_expr = SyntaxExpr x, ... }) = x; -fun the_module_alias (Target { module_alias , ... }) = module_alias; - -fun assert_serializer thy target = - case Symtab.lookup (fst (CodeTargetData.get thy)) target - of SOME data => target - | NONE => error ("Unknown code target language: " ^ quote target); - -fun add_serializer (target, seri) thy = - let - val _ = case Symtab.lookup (fst (CodeTargetData.get thy)) target - of SOME _ => warning ("overwriting existing serializer " ^ quote target) - | NONE => (); - in - thy - |> (CodeTargetData.map o apfst oo Symtab.map_default) - (target, mk_target ((serial (), seri), (([], Symtab.empty), - (mk_syntax_expr ((Symtab.empty, Symtab.empty), (Symtab.empty, Symtab.empty)), - Symtab.empty)))) - ((map_target o apfst o apsnd o K) seri) - end; - -fun map_seri_data target f thy = - let - val _ = assert_serializer thy target; - in - thy - |> (CodeTargetData.map o apfst o Symtab.map_entry target o map_target) f - end; - -fun map_adaptions target = - map_seri_data target o apsnd o apfst; -fun map_syntax_exprs target = - map_seri_data target o apsnd o apsnd o apfst o map_syntax_expr; -fun map_module_alias target = - map_seri_data target o apsnd o apsnd o apsnd; - -fun gen_get_serializer get_seri thy target permissive = - let - val (seris, exc) = CodeTargetData.get thy; - val data = case Symtab.lookup seris target - of SOME data => data - | NONE => error ("Unknown code target language: " ^ quote target); - val seri = get_seri data; - val reserved = the_reserved data; - val includes = Symtab.dest (the_includes data); - val alias = the_module_alias data; - val { class, inst, tyco, const } = the_syntax_expr data; - val project = if target = target_diag then K I - else CodeThingol.project_code permissive - (Symtab.keys class @ Symtab.keys inst @ Symtab.keys tyco @ Symtab.keys const); - fun check_empty_funs code = case filter_out (member (op =) exc) - (CodeThingol.empty_funs code) - of [] => code - | names => error ("No defining equations for " - ^ commas (map (CodeName.labelled_name thy) names)); - in fn module => fn file => fn args => fn cs => fn code => - code - |> project cs - |> check_empty_funs - |> seri module file args (CodeName.labelled_name thy) reserved includes - (Symtab.lookup alias) (Symtab.lookup class) - (Symtab.lookup tyco) (Symtab.lookup const) (these cs) - end; - -val get_serializer = gen_get_serializer the_serializer; -fun sml_of thy cs = gen_get_serializer (K eval_seri) thy target_SML false NONE NONE [] (SOME cs); - -fun eval thy (ref_name, reff) code (t, ty) args = - let - val _ = if CodeThingol.contains_dictvar t then - error "Term to be evaluated constains free dictionaries" else (); - val code' = CodeThingol.add_value_stmt (t, ty) code; - val value_code = sml_of thy [CodeName.value_name] code'; - val sml_code = space_implode " " (value_code :: "()" :: map (enclose "(" ")") args); - in ML_Context.evaluate Output.ml_output false (ref_name, reff) sml_code end; - - - (** optional pretty serialization **) local @@ -1888,7 +1807,65 @@ end; (*local*) -(** ML and Isar interface **) + +(** user interfaces **) + +(* evaluation *) + +fun eval_seri module args = + seri_ml (use_text (1, "generated code") Output.ml_output false) + (fn (cs, SOME s) => "let\n" ^ s ^ "\nin fn () => " ^ enclose "(" ")" (commas cs) ^ " end") + pr_sml (K Pretty.chunks) (SOME "Isabelle_Eval"); + +fun sml_of thy code cs = get_serializer (K eval_seri) thy target_SML false NONE [] code (SOME cs) String; + +fun eval thy (ref_name, reff) code (t, ty) args = + let + val _ = if CodeThingol.contains_dictvar t then + error "Term to be evaluated constains free dictionaries" else (); + val code' = CodeThingol.add_value_stmt (t, ty) code; + val value_code = sml_of thy code' [CodeName.value_name] ; + val sml_code = space_implode " " (value_code :: "()" :: map (enclose "(" ")") args); + in ML_Context.evaluate Output.ml_output false (ref_name, reff) sml_code end; + + +(* infix syntax *) + +datatype 'a mixfix = + Arg of fixity + | Pretty of Pretty.T; + +fun mk_mixfix prep_arg (fixity_this, mfx) = + let + fun is_arg (Arg _) = true + | is_arg _ = false; + val i = (length o filter is_arg) mfx; + fun fillin _ [] [] = + [] + | fillin pr (Arg fxy :: mfx) (a :: args) = + (pr fxy o prep_arg) a :: fillin pr mfx args + | fillin pr (Pretty p :: mfx) args = + p :: fillin pr mfx args + | fillin _ [] _ = + error ("Inconsistent mixfix: too many arguments") + | fillin _ _ [] = + error ("Inconsistent mixfix: too less arguments"); + in + (i, fn pr => fn fixity_ctxt => fn args => + gen_brackify (fixity fixity_this fixity_ctxt) (fillin pr mfx args)) + end; + +fun parse_infix prep_arg (x, i) s = + let + val l = case x of L => INFX (i, L) | _ => INFX (i, X); + val r = case x of R => INFX (i, R) | _ => INFX (i, X); + in + mk_mixfix prep_arg (INFX (i, x), + [Arg l, (Pretty o Pretty.brk) 1, (Pretty o str) s, (Pretty o Pretty.brk) 1, Arg r]) + end; + + +(* data access *) local @@ -2047,6 +2024,9 @@ fold_map (fn x => g |-- f >> pair x) xs #-> (fn xys => pair ((x, y) :: xys))); + +(* conrete syntax *) + structure P = OuterParse and K = OuterKeyword @@ -2057,6 +2037,24 @@ val (infixK, infixlK, infixrK) = ("infix", "infixl", "infixr"); +fun parse_mixfix prep_arg s = + let + val sym_any = Scan.one Symbol.is_regular; + val parse = Scan.optional ($$ "!" >> K true) false -- Scan.repeat ( + ($$ "(" -- $$ "_" -- $$ ")" >> K (Arg NOBR)) + || ($$ "_" >> K (Arg BR)) + || ($$ "/" |-- Scan.repeat ($$ " ") >> (Pretty o Pretty.brk o length)) + || (Scan.repeat1 + ( $$ "'" |-- sym_any + || Scan.unless ($$ "_" || $$ "/" || $$ "(" |-- $$ "_" |-- $$ ")") + sym_any) >> (Pretty o str o implode))); + in case Scan.finite Symbol.stopper parse (Symbol.explode s) + of ((_, p as [_]), []) => mk_mixfix prep_arg (NOBR, p) + | ((b, p as _ :: _ :: _), []) => mk_mixfix prep_arg (if b then NOBR else BR, p) + | _ => Scan.!! + (the_default ("malformed mixfix annotation: " ^ quote s) o snd) Scan.fail () + end; + fun parse_syntax prep_arg xs = Scan.option (( ((P.$$$ infixK >> K X) @@ -2151,6 +2149,8 @@ end; +(* Isar commands *) + val _ = OuterSyntax.keywords [infixK, infixlK, infixrK]; val _ = @@ -2217,12 +2217,13 @@ ); -(*including serializer defaults*) +(* serializer setup, including serializer defaults *) + val setup = add_serializer (target_SML, isar_seri_sml) #> add_serializer (target_OCaml, isar_seri_ocaml) #> add_serializer (target_Haskell, isar_seri_haskell) - #> add_serializer (target_diag, fn _ => fn _=> fn _ => seri_diagnosis) + #> add_serializer (target_diag, fn _ => fn _=> seri_diagnosis) #> add_syntax_tyco "SML" "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] => (gen_brackify (case fxy of NOBR => false | _ => fixity (INFX (1, R)) fxy) o Pretty.breaks) [ pr_typ (INFX (1, X)) ty1,