new serializer interface
authorhaftmann
Wed May 28 12:06:49 2008 +0200 (2008-05-28)
changeset 27000e8a40d8b7897
parent 26999 284c871d3acb
child 27001 d21bb9f73364
new serializer interface
src/Tools/code/code_package.ML
src/Tools/code/code_target.ML
     1.1 --- a/src/Tools/code/code_package.ML	Wed May 28 11:05:47 2008 +0200
     1.2 +++ b/src/Tools/code/code_package.ML	Wed May 28 12:06:49 2008 +0200
     1.3 @@ -97,9 +97,13 @@
     1.4  fun code thy permissive cs seris =
     1.5    let
     1.6      val code = Program.get thy;
     1.7 -    val seris' = map (fn (((target, module), file), args) =>
     1.8 -      CodeTarget.get_serializer thy target permissive module file args cs) seris;
     1.9 -  in (map (fn f => f code) seris' : unit list; ()) end;
    1.10 +    fun mk_seri_dest file = case file
    1.11 +     of NONE => CodeTarget.compile
    1.12 +      | SOME "-" => writeln o CodeTarget.string
    1.13 +      | SOME f => CodeTarget.file (Path.explode f)
    1.14 +    val _ = map (fn (((target, module), file), args) =>
    1.15 +      (mk_seri_dest file (CodeTarget.serialize thy target permissive module args code cs))) seris;
    1.16 +  in () end;
    1.17  
    1.18  (* evaluation machinery *)
    1.19  
    1.20 @@ -145,7 +149,7 @@
    1.21      val cs = map (CodeUnit.check_const thy) ts;
    1.22      val (cs', code') = generate thy (CodeFuncgr.make thy cs)
    1.23        (fold_map ooo ensure_const) cs;
    1.24 -    val code'' = CodeTarget.sml_of thy cs' code' ^ " ()";
    1.25 +    val code'' = CodeTarget.sml_of thy code' cs' ^ " ()";
    1.26    in (("codevals", code''), (ctxt', args')) end;
    1.27  
    1.28  
     2.1 --- a/src/Tools/code/code_target.ML	Wed May 28 11:05:47 2008 +0200
     2.2 +++ b/src/Tools/code/code_target.ML	Wed May 28 12:06:49 2008 +0200
     2.3 @@ -30,13 +30,16 @@
     2.4  
     2.5    val allow_exception: string -> theory -> theory;
     2.6  
     2.7 +  type serialization;
     2.8    type serializer;
     2.9    val add_serializer: string * serializer -> theory -> theory;
    2.10    val assert_serializer: theory -> string -> string;
    2.11 -  val get_serializer: theory -> string -> bool -> string option
    2.12 -    -> string option -> Args.T list
    2.13 -    -> string list option -> CodeThingol.code -> unit;
    2.14 -  val sml_of: theory -> string list -> CodeThingol.code -> string;
    2.15 +  val serialize: theory -> string -> bool -> string option -> Args.T list
    2.16 +    -> CodeThingol.code -> string list option -> serialization;
    2.17 +  val compile: serialization -> unit;
    2.18 +  val file: Path.T -> serialization -> unit;
    2.19 +  val string: serialization -> string;
    2.20 +  val sml_of: theory -> CodeThingol.code -> string list -> string;
    2.21    val eval: theory -> (string * (unit -> 'a) option ref)
    2.22      -> CodeThingol.code -> CodeThingol.iterm * CodeThingol.itype -> string list -> 'a;
    2.23    val code_width: int ref;
    2.24 @@ -64,10 +67,9 @@
    2.25  
    2.26  val code_width = ref 80;
    2.27  fun code_source p = Pretty.setmp_margin (!code_width) Pretty.string_of p ^ "\n";
    2.28 -fun code_writeln p = Pretty.setmp_margin (!code_width) Pretty.writeln p;
    2.29  
    2.30  
    2.31 -(** syntax **)
    2.32 +(** generic syntax **)
    2.33  
    2.34  datatype lrx = L | R | X;
    2.35  
    2.36 @@ -111,66 +113,168 @@
    2.37    -> CodeName.var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
    2.38  
    2.39  
    2.40 -(* user-defined syntax *)
    2.41 +(** theory data **)
    2.42 +
    2.43 +val target_diag = "diag";
    2.44 +val target_SML = "SML";
    2.45 +val target_OCaml = "OCaml";
    2.46 +val target_Haskell = "Haskell";
    2.47 +
    2.48 +datatype syntax_expr = SyntaxExpr of {
    2.49 +  class: (string * (string -> string option)) Symtab.table,
    2.50 +  inst: unit Symtab.table,
    2.51 +  tyco: typ_syntax Symtab.table,
    2.52 +  const: term_syntax Symtab.table
    2.53 +};
    2.54 +
    2.55 +fun mk_syntax_expr ((class, inst), (tyco, const)) =
    2.56 +  SyntaxExpr { class = class, inst = inst, tyco = tyco, const = const };
    2.57 +fun map_syntax_expr f (SyntaxExpr { class, inst, tyco, const }) =
    2.58 +  mk_syntax_expr (f ((class, inst), (tyco, const)));
    2.59 +fun merge_syntax_expr (SyntaxExpr { class = class1, inst = inst1, tyco = tyco1, const = const1 },
    2.60 +    SyntaxExpr { class = class2, inst = inst2, tyco = tyco2, const = const2 }) =
    2.61 +  mk_syntax_expr (
    2.62 +    (Symtab.join (K snd) (class1, class2),
    2.63 +       Symtab.join (K snd) (inst1, inst2)),
    2.64 +    (Symtab.join (K snd) (tyco1, tyco2),
    2.65 +       Symtab.join (K snd) (const1, const2))
    2.66 +  );
    2.67 +
    2.68 +datatype serialization_dest = Compile | File of Path.T | String;
    2.69 +type serialization = serialization_dest -> string option;
    2.70 +
    2.71 +fun compile f = (f Compile; ());
    2.72 +fun file p f = (f (File p); ());
    2.73 +fun string f = the (f String);
    2.74 +
    2.75 +type serializer =
    2.76 +  string option
    2.77 +  -> Args.T list
    2.78 +  -> (string -> string)
    2.79 +  -> string list
    2.80 +  -> (string * Pretty.T) list
    2.81 +  -> (string -> string option)
    2.82 +  -> (string -> class_syntax option)
    2.83 +  -> (string -> typ_syntax option)
    2.84 +  -> (string -> term_syntax option)
    2.85 +  -> CodeThingol.code -> string list -> serialization;
    2.86  
    2.87 -datatype 'a mixfix =
    2.88 -    Arg of fixity
    2.89 -  | Pretty of Pretty.T;
    2.90 +datatype target = Target of {
    2.91 +  serial: serial,
    2.92 +  serializer: serializer,
    2.93 +  reserved: string list,
    2.94 +  includes: Pretty.T Symtab.table,
    2.95 +  syntax_expr: syntax_expr,
    2.96 +  module_alias: string Symtab.table
    2.97 +};
    2.98  
    2.99 -fun mk_mixfix prep_arg (fixity_this, mfx) =
   2.100 +fun mk_target ((serial, serializer), ((reserved, includes), (syntax_expr, module_alias))) =
   2.101 +  Target { serial = serial, serializer = serializer, reserved = reserved, 
   2.102 +    includes = includes, syntax_expr = syntax_expr, module_alias = module_alias };
   2.103 +fun map_target f ( Target { serial, serializer, reserved, includes, syntax_expr, module_alias } ) =
   2.104 +  mk_target (f ((serial, serializer), ((reserved, includes), (syntax_expr, module_alias))));
   2.105 +fun merge_target target (Target { serial = serial1, serializer = serializer,
   2.106 +  reserved = reserved1, includes = includes1,
   2.107 +  syntax_expr = syntax_expr1, module_alias = module_alias1 },
   2.108 +    Target { serial = serial2, serializer = _,
   2.109 +      reserved = reserved2, includes = includes2,
   2.110 +      syntax_expr = syntax_expr2, module_alias = module_alias2 }) =
   2.111 +  if serial1 = serial2 then
   2.112 +    mk_target ((serial1, serializer),
   2.113 +      ((merge (op =) (reserved1, reserved2), Symtab.merge (op =) (includes1, includes2)),
   2.114 +        (merge_syntax_expr (syntax_expr1, syntax_expr2),
   2.115 +          Symtab.join (K snd) (module_alias1, module_alias2))
   2.116 +    ))
   2.117 +  else
   2.118 +    error ("Incompatible serializers: " ^ quote target);
   2.119 +
   2.120 +structure CodeTargetData = TheoryDataFun
   2.121 +(
   2.122 +  type T = target Symtab.table * string list;
   2.123 +  val empty = (Symtab.empty, []);
   2.124 +  val copy = I;
   2.125 +  val extend = I;
   2.126 +  fun merge _ ((target1, exc1) : T, (target2, exc2)) =
   2.127 +    (Symtab.join merge_target (target1, target2), Library.merge (op =) (exc1, exc2));
   2.128 +);
   2.129 +
   2.130 +fun the_serializer (Target { serializer, ... }) = serializer;
   2.131 +fun the_reserved (Target { reserved, ... }) = reserved;
   2.132 +fun the_includes (Target { includes, ... }) = includes;
   2.133 +fun the_syntax_expr (Target { syntax_expr = SyntaxExpr x, ... }) = x;
   2.134 +fun the_module_alias (Target { module_alias , ... }) = module_alias;
   2.135 +
   2.136 +fun assert_serializer thy target =
   2.137 +  case Symtab.lookup (fst (CodeTargetData.get thy)) target
   2.138 +   of SOME data => target
   2.139 +    | NONE => error ("Unknown code target language: " ^ quote target);
   2.140 +
   2.141 +fun add_serializer (target, seri) thy =
   2.142    let
   2.143 -    fun is_arg (Arg _) = true
   2.144 -      | is_arg _ = false;
   2.145 -    val i = (length o filter is_arg) mfx;
   2.146 -    fun fillin _ [] [] =
   2.147 -          []
   2.148 -      | fillin pr (Arg fxy :: mfx) (a :: args) =
   2.149 -          (pr fxy o prep_arg) a :: fillin pr mfx args
   2.150 -      | fillin pr (Pretty p :: mfx) args =
   2.151 -          p :: fillin pr mfx args
   2.152 -      | fillin _ [] _ =
   2.153 -          error ("Inconsistent mixfix: too many arguments")
   2.154 -      | fillin _ _ [] =
   2.155 -          error ("Inconsistent mixfix: too less arguments");
   2.156 +    val _ = case Symtab.lookup (fst (CodeTargetData.get thy)) target
   2.157 +     of SOME _ => warning ("overwriting existing serializer " ^ quote target)
   2.158 +      | NONE => ();
   2.159    in
   2.160 -    (i, fn pr => fn fixity_ctxt => fn args =>
   2.161 -      gen_brackify (fixity fixity_this fixity_ctxt) (fillin pr mfx args))
   2.162 +    thy
   2.163 +    |> (CodeTargetData.map o apfst oo Symtab.map_default)
   2.164 +          (target, mk_target ((serial (), seri), (([], Symtab.empty),
   2.165 +            (mk_syntax_expr ((Symtab.empty, Symtab.empty), (Symtab.empty, Symtab.empty)),
   2.166 +              Symtab.empty))))
   2.167 +          ((map_target o apfst o apsnd o K) seri)
   2.168    end;
   2.169  
   2.170 -fun parse_infix prep_arg (x, i) s =
   2.171 +fun map_seri_data target f thy =
   2.172    let
   2.173 -    val l = case x of L => INFX (i, L) | _ => INFX (i, X);
   2.174 -    val r = case x of R => INFX (i, R) | _ => INFX (i, X);
   2.175 +    val _ = assert_serializer thy target;
   2.176    in
   2.177 -    mk_mixfix prep_arg (INFX (i, x),
   2.178 -      [Arg l, (Pretty o Pretty.brk) 1, (Pretty o str) s, (Pretty o Pretty.brk) 1, Arg r])
   2.179 +    thy
   2.180 +    |> (CodeTargetData.map o apfst o Symtab.map_entry target o map_target) f
   2.181    end;
   2.182  
   2.183 -fun parse_mixfix prep_arg s =
   2.184 +fun map_adaptions target =
   2.185 +  map_seri_data target o apsnd o apfst;
   2.186 +fun map_syntax_exprs target =
   2.187 +  map_seri_data target o apsnd o apsnd o apfst o map_syntax_expr;
   2.188 +fun map_module_alias target =
   2.189 +  map_seri_data target o apsnd o apsnd o apsnd;
   2.190 +
   2.191 +fun get_serializer get_seri thy target permissive =
   2.192    let
   2.193 -    val sym_any = Scan.one Symbol.is_regular;
   2.194 -    val parse = Scan.optional ($$ "!" >> K true) false -- Scan.repeat (
   2.195 -         ($$ "(" -- $$ "_" -- $$ ")" >> K (Arg NOBR))
   2.196 -      || ($$ "_" >> K (Arg BR))
   2.197 -      || ($$ "/" |-- Scan.repeat ($$ " ") >> (Pretty o Pretty.brk o length))
   2.198 -      || (Scan.repeat1
   2.199 -           (   $$ "'" |-- sym_any
   2.200 -            || Scan.unless ($$ "_" || $$ "/" || $$ "(" |-- $$ "_" |-- $$ ")")
   2.201 -                 sym_any) >> (Pretty o str o implode)));
   2.202 -  in case Scan.finite Symbol.stopper parse (Symbol.explode s)
   2.203 -   of ((_, p as [_]), []) => mk_mixfix prep_arg (NOBR, p)
   2.204 -    | ((b, p as _ :: _ :: _), []) => mk_mixfix prep_arg (if b then NOBR else BR, p)
   2.205 -    | _ => Scan.!!
   2.206 -        (the_default ("malformed mixfix annotation: " ^ quote s) o snd) Scan.fail ()
   2.207 +    val (seris, exc) = CodeTargetData.get thy;
   2.208 +    val data = case Symtab.lookup seris target
   2.209 +     of SOME data => data
   2.210 +      | NONE => error ("Unknown code target language: " ^ quote target);
   2.211 +    val seri = get_seri data;
   2.212 +    val reserved = the_reserved data;
   2.213 +    val includes = Symtab.dest (the_includes data);
   2.214 +    val alias = the_module_alias data;
   2.215 +    val { class, inst, tyco, const } = the_syntax_expr data;
   2.216 +    val project = if target = target_diag then K I
   2.217 +      else CodeThingol.project_code permissive
   2.218 +        (Symtab.keys class @ Symtab.keys inst @ Symtab.keys tyco @ Symtab.keys const);
   2.219 +    fun check_empty_funs code = case filter_out (member (op =) exc)
   2.220 +        (CodeThingol.empty_funs code)
   2.221 +     of [] => code
   2.222 +      | names => error ("No defining equations for "
   2.223 +          ^ commas (map (CodeName.labelled_name thy) names));
   2.224 +  in fn module => fn args => fn code => fn cs =>
   2.225 +    seri module args (CodeName.labelled_name thy) reserved includes
   2.226 +      (Symtab.lookup alias) (Symtab.lookup class)
   2.227 +      (Symtab.lookup tyco) (Symtab.lookup const)
   2.228 +        ((check_empty_funs o project cs) code) (these cs)
   2.229    end;
   2.230  
   2.231 +val serialize = get_serializer the_serializer;
   2.232 +
   2.233  fun parse_args f args =
   2.234    case Scan.read Args.stopper f args
   2.235     of SOME x => x
   2.236      | NONE => error "Bad serializer arguments";
   2.237  
   2.238  
   2.239 -(* generic serializer combinators *)
   2.240 +(** generic output combinators **)
   2.241 +
   2.242 +(* applications and bindings *)
   2.243  
   2.244  fun gen_pr_app pr_app' pr_term const_syntax labelled_name is_cons
   2.245        lhs vars fxy (app as ((c, (_, tys)), ts)) =
   2.246 @@ -269,7 +373,7 @@
   2.247    in CodeThingol.unfoldr dest_monad t end;
   2.248  
   2.249  
   2.250 -(** name auxiliary **)
   2.251 +(* name auxiliary *)
   2.252  
   2.253  val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode;
   2.254  val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode;
   2.255 @@ -914,8 +1018,8 @@
   2.256      str ("end;; (*struct " ^ name ^ "*)")
   2.257    ]);
   2.258  
   2.259 -fun seri_ml pr_def pr_modl module output labelled_name reserved_syms includes raw_module_alias
   2.260 -  (_ : string -> class_syntax option) tyco_syntax const_syntax cs code =
   2.261 +fun seri_ml internal output_cont pr_def pr_modl module labelled_name reserved_syms includes raw_module_alias
   2.262 +  (_ : string -> class_syntax option) tyco_syntax const_syntax code cs seri_dest =
   2.263    let
   2.264      val module_alias = if is_some module then K module else raw_module_alias;
   2.265      val is_cons = CodeThingol.is_cons code;
   2.266 @@ -1089,33 +1193,19 @@
   2.267      val p = Pretty.chunks (separate (str "") (map snd includes @ (map_filter
   2.268        (pr_node [] o Graph.get_node nodes) o rev o flat o Graph.strong_conn) nodes));
   2.269      val deresolv = try (deresolver (if is_some module then the_list module else []));
   2.270 -  in output (map_filter deresolv cs, p) end;
   2.271 -
   2.272 -fun isar_seri_sml module file =
   2.273 -  let
   2.274 -    val output = case file
   2.275 -     of NONE => use_text (1, "generated code") Output.ml_output false o code_source
   2.276 -      | SOME "-" => code_writeln
   2.277 -      | SOME file => File.write (Path.explode file) o code_source;
   2.278 -  in
   2.279 -    parse_args (Scan.succeed ())
   2.280 -    #> (fn () => seri_ml pr_sml pr_sml_modl module (output o snd))
   2.281 -  end;
   2.282 +    val output = case seri_dest
   2.283 +     of Compile => K NONE o internal o code_source
   2.284 +      | File file => K NONE o File.write file o code_source
   2.285 +      | String => SOME o code_source;
   2.286 +  in output_cont (map_filter deresolv cs, output p) end;
   2.287  
   2.288 -fun eval_seri module file args =
   2.289 -  seri_ml pr_sml (K Pretty.chunks) (SOME "Isabelle_Eval")
   2.290 -    (fn (cs, p) => "let\n" ^ code_source p ^ "\nin fn () => " ^ enclose "(" ")" (commas cs) ^ " end");
   2.291 +fun isar_seri_sml module =
   2.292 +  parse_args (Scan.succeed ())
   2.293 +  #> (fn () => seri_ml (use_text (1, "generated code") Output.ml_output false) snd pr_sml pr_sml_modl module);
   2.294  
   2.295 -fun isar_seri_ocaml module file =
   2.296 -  let
   2.297 -    val output = case file
   2.298 -     of NONE => error "OCaml: no internal compilation"
   2.299 -      | SOME "-" => code_writeln
   2.300 -      | SOME file => File.write (Path.explode file) o code_source;
   2.301 -  in
   2.302 -    parse_args (Scan.succeed ())
   2.303 -    #> (fn () => seri_ml pr_ocaml pr_ocaml_modl module (output o snd))
   2.304 -  end;
   2.305 +fun isar_seri_ocaml module =
   2.306 +  parse_args (Scan.succeed ())
   2.307 +  #> (fn () => seri_ml (fn _ => error "OCaml: no internal compilation") snd pr_ocaml pr_ocaml_modl module)
   2.308  
   2.309  
   2.310  (** Haskell serializer **)
   2.311 @@ -1396,11 +1486,10 @@
   2.312  
   2.313  end; (*local*)
   2.314  
   2.315 -fun seri_haskell module_prefix module destination string_classes labelled_name
   2.316 +fun seri_haskell module_prefix module string_classes labelled_name
   2.317      reserved_syms includes raw_module_alias
   2.318 -    class_syntax tyco_syntax const_syntax cs code =
   2.319 +    class_syntax tyco_syntax const_syntax code cs seri_dest =
   2.320    let
   2.321 -    val _ = Option.map File.check destination;
   2.322      val is_cons = CodeThingol.is_cons code;
   2.323      val contr_classparam_typs = CodeThingol.contr_classparam_typs code;
   2.324      val module_alias = if is_some module then K module else raw_module_alias;
   2.325 @@ -1477,25 +1566,14 @@
   2.326        deresolv_here (if qualified then deresolv else deresolv_here) is_cons
   2.327        contr_classparam_typs
   2.328        (if string_classes then deriving_show else K false);
   2.329 -    fun write_modulefile (SOME destination) modlname =
   2.330 -          let
   2.331 -            val filename = case modlname
   2.332 -             of "" => Path.explode "Main.hs"
   2.333 -              | _ => (Path.ext "hs" o Path.explode o implode o separate "/"
   2.334 -                    o NameSpace.explode) modlname;
   2.335 -            val pathname = Path.append destination filename;
   2.336 -            val _ = File.mkdir (Path.dir pathname);
   2.337 -          in File.write pathname o code_source end
   2.338 -      | write_modulefile NONE _ = code_writeln;
   2.339 -    fun write_module destination (modulename, content) =
   2.340 -      Pretty.chunks [
   2.341 +    fun assemble_module (modulename, content) =
   2.342 +      (modulename, code_source (Pretty.chunks [
   2.343          str ("module " ^ modulename ^ " where {"),
   2.344          str "",
   2.345          content,
   2.346          str "",
   2.347          str "}"
   2.348 -      ]
   2.349 -      |> write_modulefile destination modulename;
   2.350 +      ]));
   2.351      fun seri_module (modlname', (imports, (defs, _))) =
   2.352        let
   2.353          val imports' =
   2.354 @@ -1521,31 +1599,34 @@
   2.355                (fn (name, (_, SOME def)) => SOME (seri_def qualified (name, def))
   2.356                  | (_, (_, NONE)) => NONE) defs)
   2.357            )
   2.358 -      in
   2.359 -        write_module destination (modlname', content)
   2.360 -      end;
   2.361 -  in (
   2.362 -    map (write_module destination) includes;
   2.363 -    Symtab.fold (fn modl => fn () => seri_module modl) code' ()
   2.364 -  ) end;
   2.365 +      in assemble_module (modlname', content) end;
   2.366 +    fun write_module destination (modlname, content) =
   2.367 +      let
   2.368 +        val filename = case modlname
   2.369 +         of "" => Path.explode "Main.hs"
   2.370 +          | _ => (Path.ext "hs" o Path.explode o implode o separate "/"
   2.371 +                o NameSpace.explode) modlname;
   2.372 +        val pathname = Path.append destination filename;
   2.373 +        val _ = File.mkdir (Path.dir pathname);
   2.374 +      in File.write pathname content end
   2.375 +    val output = case seri_dest
   2.376 +     of Compile => error ("Haskell: no internal compilation")
   2.377 +      | File destination => K NONE o map (write_module destination)
   2.378 +      | String => SOME o cat_lines o map snd;
   2.379 +  in output (map assemble_module includes
   2.380 +    @ map seri_module (Symtab.dest code'))
   2.381 +  end;
   2.382  
   2.383 -fun isar_seri_haskell module file =
   2.384 -  let
   2.385 -    val destination = case file
   2.386 -     of NONE => error ("Haskell: no internal compilation")
   2.387 -      | SOME "-" => NONE
   2.388 -      | SOME file => SOME (Path.explode file)
   2.389 -  in
   2.390 -    parse_args (Scan.option (Args.$$$ "root" -- Args.colon |-- Args.name)
   2.391 -      -- Scan.optional (Args.$$$ "string_classes" >> K true) false
   2.392 -      >> (fn (module_prefix, string_classes) =>
   2.393 -        seri_haskell module_prefix module destination string_classes))
   2.394 -  end;
   2.395 +fun isar_seri_haskell module =
   2.396 +  parse_args (Scan.option (Args.$$$ "root" -- Args.colon |-- Args.name)
   2.397 +    -- Scan.optional (Args.$$$ "string_classes" >> K true) false
   2.398 +    >> (fn (module_prefix, string_classes) =>
   2.399 +      seri_haskell module_prefix module string_classes));
   2.400  
   2.401  
   2.402  (** diagnosis serializer **)
   2.403  
   2.404 -fun seri_diagnosis labelled_name _ _ _ _ _ _ _ code =
   2.405 +fun seri_diagnosis labelled_name _ _ _ _ _ _ code _ _ =
   2.406    let
   2.407      val init_names = CodeName.make_vars [];
   2.408      fun pr_fun "fun" = SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
   2.409 @@ -1562,174 +1643,12 @@
   2.410      |> Graph.fold (fn (name, (def, _)) =>
   2.411            case try pr (name, def) of SOME p => cons p | NONE => I) code
   2.412      |> Pretty.chunks2
   2.413 -    |> code_writeln
   2.414 +    |> code_source
   2.415 +    |> writeln
   2.416 +    |> K NONE
   2.417    end;
   2.418  
   2.419  
   2.420 -
   2.421 -(** theory data **)
   2.422 -
   2.423 -datatype syntax_expr = SyntaxExpr of {
   2.424 -  class: (string * (string -> string option)) Symtab.table,
   2.425 -  inst: unit Symtab.table,
   2.426 -  tyco: typ_syntax Symtab.table,
   2.427 -  const: term_syntax Symtab.table
   2.428 -};
   2.429 -
   2.430 -fun mk_syntax_expr ((class, inst), (tyco, const)) =
   2.431 -  SyntaxExpr { class = class, inst = inst, tyco = tyco, const = const };
   2.432 -fun map_syntax_expr f (SyntaxExpr { class, inst, tyco, const }) =
   2.433 -  mk_syntax_expr (f ((class, inst), (tyco, const)));
   2.434 -fun merge_syntax_expr (SyntaxExpr { class = class1, inst = inst1, tyco = tyco1, const = const1 },
   2.435 -    SyntaxExpr { class = class2, inst = inst2, tyco = tyco2, const = const2 }) =
   2.436 -  mk_syntax_expr (
   2.437 -    (Symtab.join (K snd) (class1, class2),
   2.438 -       Symtab.join (K snd) (inst1, inst2)),
   2.439 -    (Symtab.join (K snd) (tyco1, tyco2),
   2.440 -       Symtab.join (K snd) (const1, const2))
   2.441 -  );
   2.442 -
   2.443 -type 'a gen_serializer =
   2.444 -  string option
   2.445 -  -> string option
   2.446 -  -> Args.T list
   2.447 -  -> (string -> string)
   2.448 -  -> string list
   2.449 -  -> (string * Pretty.T) list
   2.450 -  -> (string -> string option)
   2.451 -  -> (string -> class_syntax option)
   2.452 -  -> (string -> typ_syntax option)
   2.453 -  -> (string -> term_syntax option)
   2.454 -  -> string list -> CodeThingol.code -> 'a;
   2.455 -
   2.456 -type serializer = unit gen_serializer;
   2.457 -
   2.458 -datatype target = Target of {
   2.459 -  serial: serial,
   2.460 -  serializer: serializer,
   2.461 -  reserved: string list,
   2.462 -  includes: Pretty.T Symtab.table,
   2.463 -  syntax_expr: syntax_expr,
   2.464 -  module_alias: string Symtab.table
   2.465 -};
   2.466 -
   2.467 -fun mk_target ((serial, serializer), ((reserved, includes), (syntax_expr, module_alias))) =
   2.468 -  Target { serial = serial, serializer = serializer, reserved = reserved, 
   2.469 -    includes = includes, syntax_expr = syntax_expr, module_alias = module_alias };
   2.470 -fun map_target f ( Target { serial, serializer, reserved, includes, syntax_expr, module_alias } ) =
   2.471 -  mk_target (f ((serial, serializer), ((reserved, includes), (syntax_expr, module_alias))));
   2.472 -fun merge_target target (Target { serial = serial1, serializer = serializer,
   2.473 -  reserved = reserved1, includes = includes1,
   2.474 -  syntax_expr = syntax_expr1, module_alias = module_alias1 },
   2.475 -    Target { serial = serial2, serializer = _,
   2.476 -      reserved = reserved2, includes = includes2,
   2.477 -      syntax_expr = syntax_expr2, module_alias = module_alias2 }) =
   2.478 -  if serial1 = serial2 then
   2.479 -    mk_target ((serial1, serializer),
   2.480 -      ((merge (op =) (reserved1, reserved2), Symtab.merge (op =) (includes1, includes2)),
   2.481 -        (merge_syntax_expr (syntax_expr1, syntax_expr2),
   2.482 -          Symtab.join (K snd) (module_alias1, module_alias2))
   2.483 -    ))
   2.484 -  else
   2.485 -    error ("Incompatible serializers: " ^ quote target);
   2.486 -
   2.487 -structure CodeTargetData = TheoryDataFun
   2.488 -(
   2.489 -  type T = target Symtab.table * string list;
   2.490 -  val empty = (Symtab.empty, []);
   2.491 -  val copy = I;
   2.492 -  val extend = I;
   2.493 -  fun merge _ ((target1, exc1) : T, (target2, exc2)) =
   2.494 -    (Symtab.join merge_target (target1, target2), Library.merge (op =) (exc1, exc2));
   2.495 -);
   2.496 -
   2.497 -val target_SML = "SML";
   2.498 -val target_OCaml = "OCaml";
   2.499 -val target_Haskell = "Haskell";
   2.500 -val target_diag = "diag";
   2.501 -
   2.502 -fun the_serializer (Target { serializer, ... }) = serializer;
   2.503 -fun the_reserved (Target { reserved, ... }) = reserved;
   2.504 -fun the_includes (Target { includes, ... }) = includes;
   2.505 -fun the_syntax_expr (Target { syntax_expr = SyntaxExpr x, ... }) = x;
   2.506 -fun the_module_alias (Target { module_alias , ... }) = module_alias;
   2.507 -
   2.508 -fun assert_serializer thy target =
   2.509 -  case Symtab.lookup (fst (CodeTargetData.get thy)) target
   2.510 -   of SOME data => target
   2.511 -    | NONE => error ("Unknown code target language: " ^ quote target);
   2.512 -
   2.513 -fun add_serializer (target, seri) thy =
   2.514 -  let
   2.515 -    val _ = case Symtab.lookup (fst (CodeTargetData.get thy)) target
   2.516 -     of SOME _ => warning ("overwriting existing serializer " ^ quote target)
   2.517 -      | NONE => ();
   2.518 -  in
   2.519 -    thy
   2.520 -    |> (CodeTargetData.map o apfst oo Symtab.map_default)
   2.521 -          (target, mk_target ((serial (), seri), (([], Symtab.empty),
   2.522 -            (mk_syntax_expr ((Symtab.empty, Symtab.empty), (Symtab.empty, Symtab.empty)),
   2.523 -              Symtab.empty))))
   2.524 -          ((map_target o apfst o apsnd o K) seri)
   2.525 -  end;
   2.526 -
   2.527 -fun map_seri_data target f thy =
   2.528 -  let
   2.529 -    val _ = assert_serializer thy target;
   2.530 -  in
   2.531 -    thy
   2.532 -    |> (CodeTargetData.map o apfst o Symtab.map_entry target o map_target) f
   2.533 -  end;
   2.534 -
   2.535 -fun map_adaptions target =
   2.536 -  map_seri_data target o apsnd o apfst;
   2.537 -fun map_syntax_exprs target =
   2.538 -  map_seri_data target o apsnd o apsnd o apfst o map_syntax_expr;
   2.539 -fun map_module_alias target =
   2.540 -  map_seri_data target o apsnd o apsnd o apsnd;
   2.541 -
   2.542 -fun gen_get_serializer get_seri thy target permissive =
   2.543 -  let
   2.544 -    val (seris, exc) = CodeTargetData.get thy;
   2.545 -    val data = case Symtab.lookup seris target
   2.546 -     of SOME data => data
   2.547 -      | NONE => error ("Unknown code target language: " ^ quote target);
   2.548 -    val seri = get_seri data;
   2.549 -    val reserved = the_reserved data;
   2.550 -    val includes = Symtab.dest (the_includes data);
   2.551 -    val alias = the_module_alias data;
   2.552 -    val { class, inst, tyco, const } = the_syntax_expr data;
   2.553 -    val project = if target = target_diag then K I
   2.554 -      else CodeThingol.project_code permissive
   2.555 -        (Symtab.keys class @ Symtab.keys inst @ Symtab.keys tyco @ Symtab.keys const);
   2.556 -    fun check_empty_funs code = case filter_out (member (op =) exc)
   2.557 -        (CodeThingol.empty_funs code)
   2.558 -     of [] => code
   2.559 -      | names => error ("No defining equations for "
   2.560 -          ^ commas (map (CodeName.labelled_name thy) names));
   2.561 -  in fn module => fn file => fn args => fn cs => fn code =>
   2.562 -    code
   2.563 -    |> project cs
   2.564 -    |> check_empty_funs
   2.565 -    |> seri module file args (CodeName.labelled_name thy) reserved includes
   2.566 -        (Symtab.lookup alias) (Symtab.lookup class)
   2.567 -        (Symtab.lookup tyco) (Symtab.lookup const) (these cs)
   2.568 -  end;
   2.569 -
   2.570 -val get_serializer = gen_get_serializer the_serializer;
   2.571 -fun sml_of thy cs = gen_get_serializer (K eval_seri) thy target_SML false NONE NONE [] (SOME cs);
   2.572 -
   2.573 -fun eval thy (ref_name, reff) code (t, ty) args =
   2.574 -  let
   2.575 -    val _ = if CodeThingol.contains_dictvar t then
   2.576 -      error "Term to be evaluated constains free dictionaries" else ();
   2.577 -    val code' = CodeThingol.add_value_stmt (t, ty) code;
   2.578 -    val value_code = sml_of thy [CodeName.value_name] code';
   2.579 -    val sml_code = space_implode " " (value_code :: "()" :: map (enclose "(" ")") args);
   2.580 -  in ML_Context.evaluate Output.ml_output false (ref_name, reff) sml_code end;
   2.581 -
   2.582 -
   2.583 -
   2.584  (** optional pretty serialization **)
   2.585  
   2.586  local
   2.587 @@ -1888,7 +1807,65 @@
   2.588  
   2.589  end; (*local*)
   2.590  
   2.591 -(** ML and Isar interface **)
   2.592 +
   2.593 +(** user interfaces **)
   2.594 +
   2.595 +(* evaluation *)
   2.596 +
   2.597 +fun eval_seri module args =
   2.598 +  seri_ml (use_text (1, "generated code") Output.ml_output false)
   2.599 +    (fn (cs, SOME s) => "let\n" ^ s ^ "\nin fn () => " ^ enclose "(" ")" (commas cs) ^ " end")
   2.600 +    pr_sml (K Pretty.chunks) (SOME "Isabelle_Eval");
   2.601 +
   2.602 +fun sml_of thy code cs = get_serializer (K eval_seri) thy target_SML false NONE [] code (SOME cs) String;
   2.603 +
   2.604 +fun eval thy (ref_name, reff) code (t, ty) args =
   2.605 +  let
   2.606 +    val _ = if CodeThingol.contains_dictvar t then
   2.607 +      error "Term to be evaluated constains free dictionaries" else ();
   2.608 +    val code' = CodeThingol.add_value_stmt (t, ty) code;
   2.609 +    val value_code = sml_of thy code' [CodeName.value_name] ;
   2.610 +    val sml_code = space_implode " " (value_code :: "()" :: map (enclose "(" ")") args);
   2.611 +  in ML_Context.evaluate Output.ml_output false (ref_name, reff) sml_code end;
   2.612 +
   2.613 +
   2.614 +(* infix syntax *)
   2.615 +
   2.616 +datatype 'a mixfix =
   2.617 +    Arg of fixity
   2.618 +  | Pretty of Pretty.T;
   2.619 +
   2.620 +fun mk_mixfix prep_arg (fixity_this, mfx) =
   2.621 +  let
   2.622 +    fun is_arg (Arg _) = true
   2.623 +      | is_arg _ = false;
   2.624 +    val i = (length o filter is_arg) mfx;
   2.625 +    fun fillin _ [] [] =
   2.626 +          []
   2.627 +      | fillin pr (Arg fxy :: mfx) (a :: args) =
   2.628 +          (pr fxy o prep_arg) a :: fillin pr mfx args
   2.629 +      | fillin pr (Pretty p :: mfx) args =
   2.630 +          p :: fillin pr mfx args
   2.631 +      | fillin _ [] _ =
   2.632 +          error ("Inconsistent mixfix: too many arguments")
   2.633 +      | fillin _ _ [] =
   2.634 +          error ("Inconsistent mixfix: too less arguments");
   2.635 +  in
   2.636 +    (i, fn pr => fn fixity_ctxt => fn args =>
   2.637 +      gen_brackify (fixity fixity_this fixity_ctxt) (fillin pr mfx args))
   2.638 +  end;
   2.639 +
   2.640 +fun parse_infix prep_arg (x, i) s =
   2.641 +  let
   2.642 +    val l = case x of L => INFX (i, L) | _ => INFX (i, X);
   2.643 +    val r = case x of R => INFX (i, R) | _ => INFX (i, X);
   2.644 +  in
   2.645 +    mk_mixfix prep_arg (INFX (i, x),
   2.646 +      [Arg l, (Pretty o Pretty.brk) 1, (Pretty o str) s, (Pretty o Pretty.brk) 1, Arg r])
   2.647 +  end;
   2.648 +
   2.649 +
   2.650 +(* data access *)
   2.651  
   2.652  local
   2.653  
   2.654 @@ -2047,6 +2024,9 @@
   2.655      fold_map (fn x => g |-- f >> pair x) xs
   2.656      #-> (fn xys => pair ((x, y) :: xys)));
   2.657  
   2.658 +
   2.659 +(* conrete syntax *)
   2.660 +
   2.661  structure P = OuterParse
   2.662  and K = OuterKeyword
   2.663  
   2.664 @@ -2057,6 +2037,24 @@
   2.665  
   2.666  val (infixK, infixlK, infixrK) = ("infix", "infixl", "infixr");
   2.667  
   2.668 +fun parse_mixfix prep_arg s =
   2.669 +  let
   2.670 +    val sym_any = Scan.one Symbol.is_regular;
   2.671 +    val parse = Scan.optional ($$ "!" >> K true) false -- Scan.repeat (
   2.672 +         ($$ "(" -- $$ "_" -- $$ ")" >> K (Arg NOBR))
   2.673 +      || ($$ "_" >> K (Arg BR))
   2.674 +      || ($$ "/" |-- Scan.repeat ($$ " ") >> (Pretty o Pretty.brk o length))
   2.675 +      || (Scan.repeat1
   2.676 +           (   $$ "'" |-- sym_any
   2.677 +            || Scan.unless ($$ "_" || $$ "/" || $$ "(" |-- $$ "_" |-- $$ ")")
   2.678 +                 sym_any) >> (Pretty o str o implode)));
   2.679 +  in case Scan.finite Symbol.stopper parse (Symbol.explode s)
   2.680 +   of ((_, p as [_]), []) => mk_mixfix prep_arg (NOBR, p)
   2.681 +    | ((b, p as _ :: _ :: _), []) => mk_mixfix prep_arg (if b then NOBR else BR, p)
   2.682 +    | _ => Scan.!!
   2.683 +        (the_default ("malformed mixfix annotation: " ^ quote s) o snd) Scan.fail ()
   2.684 +  end;
   2.685 +
   2.686  fun parse_syntax prep_arg xs =
   2.687    Scan.option ((
   2.688        ((P.$$$ infixK  >> K X)
   2.689 @@ -2151,6 +2149,8 @@
   2.690    end;
   2.691  
   2.692  
   2.693 +(* Isar commands *)
   2.694 +
   2.695  val _ = OuterSyntax.keywords [infixK, infixlK, infixrK];
   2.696  
   2.697  val _ =
   2.698 @@ -2217,12 +2217,13 @@
   2.699    );
   2.700  
   2.701  
   2.702 -(*including serializer defaults*)
   2.703 +(* serializer setup, including serializer defaults *)
   2.704 +
   2.705  val setup =
   2.706    add_serializer (target_SML, isar_seri_sml)
   2.707    #> add_serializer (target_OCaml, isar_seri_ocaml)
   2.708    #> add_serializer (target_Haskell, isar_seri_haskell)
   2.709 -  #> add_serializer (target_diag, fn _ => fn _=> fn _ => seri_diagnosis)
   2.710 +  #> add_serializer (target_diag, fn _ => fn _=> seri_diagnosis)
   2.711    #> add_syntax_tyco "SML" "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
   2.712        (gen_brackify (case fxy of NOBR => false | _ => fixity (INFX (1, R)) fxy) o Pretty.breaks) [
   2.713          pr_typ (INFX (1, X)) ty1,