wneuper/isa: src/Tools/code/code_target.ML@58e8ba3b792b

     1 (*  Title:      Tools/code/code_target.ML

     2     ID:         $Id$

     3     Author:     Florian Haftmann, TU Muenchen

     5 Serializer from intermediate language ("Thin-gol")

     6 to target languages (like SML or Haskell).

     7 *)

     9 signature CODE_TARGET =

    10 sig

    11   include BASIC_CODE_THINGOL;

    13   val add_syntax_class: string -> class

    14     -> (string * (string * string) list) option -> theory -> theory;

    15   val add_syntax_inst: string -> string * class -> bool -> theory -> theory;

    16   val add_syntax_tycoP: string -> string -> OuterParse.token list

    17     -> (theory -> theory) * OuterParse.token list;

    18   val add_syntax_constP: string -> string -> OuterParse.token list

    19     -> (theory -> theory) * OuterParse.token list;

    21   val add_undefined: string -> string -> string -> theory -> theory;

    22   val add_pretty_list: string -> string -> string -> theory -> theory;

    23   val add_pretty_list_string: string -> string -> string

    24     -> string -> string list -> theory -> theory;

    25   val add_pretty_char: string -> string -> string list -> theory -> theory

    26   val add_pretty_numeral: string -> bool -> string -> string -> string -> string

    27     -> string -> string -> theory -> theory;

    28   val add_pretty_message: string -> string -> string list -> string

    29     -> string -> string -> theory -> theory;

    31   val allow_exception: string -> theory -> theory;

    33   type serializer;

    34   val add_serializer: string * serializer -> theory -> theory;

    35   val get_serializer: theory -> string -> bool -> string option

    36     -> string option -> Args.T list

    37     -> string list option -> CodeThingol.code -> unit;

    38   val assert_serializer: theory -> string -> string;

    40   val eval_verbose: bool ref;

    41   val eval_invoke: theory -> (string * (unit -> 'a) option ref)

    42     -> CodeThingol.code -> CodeThingol.iterm * CodeThingol.itype -> string list -> 'a;

    43   val code_width: int ref;

    45   val setup: theory -> theory;

    46 end;

    48 structure CodeTarget : CODE_TARGET =

    49 struct

    51 open BasicCodeThingol;

    53 (** basics **)

    55 infixr 5 @@;

    56 infixr 5 @|;

    57 fun x @@ y = [x, y];

    58 fun xs @| y = xs @ [y];

    59 val str = PrintMode.setmp [] Pretty.str;

    60 val concat = Pretty.block o Pretty.breaks;

    61 val brackets = Pretty.enclose "(" ")" o Pretty.breaks;

    62 fun semicolon ps = Pretty.block [concat ps, str ";"];

    65 (** syntax **)

    67 datatype lrx = L | R | X;

    69 datatype fixity =

    70     BR

    71   | NOBR

    72   | INFX of (int * lrx);

    74 val APP = INFX (~1, L);

    76 fun eval_lrx L L = false

    77   | eval_lrx R R = false

    78   | eval_lrx _ _ = true;

    80 fun eval_fxy NOBR NOBR = false

    81   | eval_fxy BR NOBR = false

    82   | eval_fxy NOBR BR = false

    83   | eval_fxy (INFX (pr, lr)) (INFX (pr_ctxt, lr_ctxt)) =

    84       pr < pr_ctxt

    85       orelse pr = pr_ctxt

    86         andalso eval_lrx lr lr_ctxt

    87       orelse pr_ctxt = ~1

    88   | eval_fxy _ (INFX _) = false

    89   | eval_fxy (INFX _) NOBR = false

    90   | eval_fxy _ _ = true;

    92 fun gen_brackify _ [p] = p

    93   | gen_brackify true (ps as _::_) = Pretty.enclose "(" ")" ps

    94   | gen_brackify false (ps as _::_) = Pretty.block ps;

    96 fun brackify fxy_ctxt ps =

    97   gen_brackify (eval_fxy BR fxy_ctxt) (Pretty.breaks ps);

    99 fun brackify_infix infx fxy_ctxt ps =

   100   gen_brackify (eval_fxy (INFX infx) fxy_ctxt) (Pretty.breaks ps);

   102 type class_syntax = string * (string -> string option);

   103 type typ_syntax = int * ((fixity -> itype -> Pretty.T)

   104   -> fixity -> itype list -> Pretty.T);

   105 type term_syntax = int * ((CodeName.var_ctxt -> fixity -> iterm -> Pretty.T)

   106   -> CodeName.var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);

   109 (* user-defined syntax *)

   111 datatype 'a mixfix =

   112     Arg of fixity

   113   | Pretty of Pretty.T;

   115 fun mk_mixfix prep_arg (fixity_this, mfx) =

   116   let

   117     fun is_arg (Arg _) = true

   118       | is_arg _ = false;

   119     val i = (length o filter is_arg) mfx;

   120     fun fillin _ [] [] =

   121           []

   122       | fillin pr (Arg fxy :: mfx) (a :: args) =

   123           (pr fxy o prep_arg) a :: fillin pr mfx args

   124       | fillin pr (Pretty p :: mfx) args =

   125           p :: fillin pr mfx args

   126       | fillin _ [] _ =

   127           error ("Inconsistent mixfix: too many arguments")

   128       | fillin _ _ [] =

   129           error ("Inconsistent mixfix: too less arguments");

   130   in

   131     (i, fn pr => fn fixity_ctxt => fn args =>

   132       gen_brackify (eval_fxy fixity_this fixity_ctxt) (fillin pr mfx args))

   133   end;

   135 fun parse_infix prep_arg (x, i) s =

   136   let

   137     val l = case x of L => INFX (i, L) | _ => INFX (i, X);

   138     val r = case x of R => INFX (i, R) | _ => INFX (i, X);

   139   in

   140     mk_mixfix prep_arg (INFX (i, x),

   141       [Arg l, (Pretty o Pretty.brk) 1, (Pretty o str) s, (Pretty o Pretty.brk) 1, Arg r])

   142   end;

   144 fun parse_mixfix prep_arg s =

   145   let

   146     val sym_any = Scan.one Symbol.is_regular;

   147     val parse = Scan.optional ($$ "!" >> K true) false -- Scan.repeat (

   148          ($$ "(" -- $$ "_" -- $$ ")" >> K (Arg NOBR))

   149       || ($$ "_" >> K (Arg BR))

   150       || ($$ "/" |-- Scan.repeat ($$ " ") >> (Pretty o Pretty.brk o length))

   151       || (Scan.repeat1

   152            (   $$ "'" |-- sym_any

   153             || Scan.unless ($$ "_" || $$ "/" || $$ "(" |-- $$ "_" |-- $$ ")")

   154                  sym_any) >> (Pretty o str o implode)));

   155   in case Scan.finite Symbol.stopper parse (Symbol.explode s)

   156    of ((_, p as [_]), []) => mk_mixfix prep_arg (NOBR, p)

   157     | ((b, p as _ :: _ :: _), []) => mk_mixfix prep_arg (if b then NOBR else BR, p)

   158     | _ => Scan.!!

   159         (the_default ("malformed mixfix annotation: " ^ quote s) o snd) Scan.fail ()

   160   end;

   162 fun parse_args f args =

   163   case Scan.read Args.stopper f args

   164    of SOME x => x

   165     | NONE => error "Bad serializer arguments";

   168 (* generic serializer combinators *)

   170 fun gen_pr_app pr_app' pr_term const_syntax labelled_name is_cons

   171       lhs vars fxy (app as ((c, (_, tys)), ts)) =

   172   case const_syntax c

   173    of NONE => if lhs andalso not (is_cons c) then

   174           error ("non-constructor on left hand side of equation: " ^ labelled_name c)

   175         else brackify fxy (pr_app' lhs vars app)

   176     | SOME (i, pr) =>

   177         let

   178           val k = if i < 0 then length tys else i;

   179           fun pr' fxy ts = pr (pr_term lhs) vars fxy (ts ~~ curry Library.take k tys);

   180         in if k = length ts

   181           then pr' fxy ts

   182         else if k < length ts

   183           then case chop k ts of (ts1, ts2) =>

   184             brackify fxy (pr' APP ts1 :: map (pr_term lhs vars BR) ts2)

   185           else pr_term lhs vars fxy (CodeThingol.eta_expand app k)

   186         end;

   188 fun gen_pr_bind pr_bind' pr_term fxy ((v, pat), ty) vars =

   189   let

   190     val vs = case pat

   191      of SOME pat => CodeThingol.fold_varnames (insert (op =)) pat []

   192       | NONE => [];

   193     val vars' = CodeName.intro_vars (the_list v) vars;

   194     val vars'' = CodeName.intro_vars vs vars';

   195     val v' = Option.map (CodeName.lookup_var vars') v;

   196     val pat' = Option.map (pr_term true vars'' fxy) pat;

   197   in (pr_bind' ((v', pat'), ty), vars'') end;

   200 (* list, char, string, numeral and monad abstract syntax transformations *)

   202 fun implode_list c_nil c_cons t =

   203   let

   204     fun dest_cons (IConst (c, _) `$ t1 `$ t2) =

   205           if c = c_cons

   206           then SOME (t1, t2)

   207           else NONE

   208       | dest_cons _ = NONE;

   209     val (ts, t') = CodeThingol.unfoldr dest_cons t;

   210   in case t'

   211    of IConst (c, _) => if c = c_nil then SOME ts else NONE

   212     | _ => NONE

   213   end;

   215 fun decode_char c_nibbles (IConst (c1, _), IConst (c2, _)) =

   216       let

   217         fun idx c = find_index (curry (op =) c) c_nibbles;

   218         fun decode ~1 _ = NONE

   219           | decode _ ~1 = NONE

   220           | decode n m = SOME (chr (n * 16 + m));

   221       in decode (idx c1) (idx c2) end

   222   | decode_char _ _ = NONE;

   224 fun implode_string c_char c_nibbles mk_char mk_string ts =

   225   let

   226     fun implode_char (IConst (c, _) `$ t1 `$ t2) =

   227           if c = c_char then decode_char c_nibbles (t1, t2) else NONE

   228       | implode_char _ = NONE;

   229     val ts' = map implode_char ts;

   230   in if forall is_some ts'

   231     then (SOME o str o mk_string o implode o map_filter I) ts'

   232     else NONE

   233   end;

   235 fun implode_numeral c_bit0 c_bit1 c_pls c_min c_bit =

   236   let

   237     fun dest_bit (IConst (c, _)) = if c = c_bit0 then SOME 0

   238           else if c = c_bit1 then SOME 1

   239           else NONE

   240       | dest_bit _ = NONE;

   241     fun dest_numeral (IConst (c, _)) = if c = c_pls then SOME 0

   242           else if c = c_min then SOME ~1

   243           else NONE

   244       | dest_numeral (IConst (c, _) `$ t1 `$ t2) =

   245           if c = c_bit then case (dest_numeral t1, dest_bit t2)

   246            of (SOME n, SOME b) => SOME (2 * n + b)

   247             | _ => NONE

   248           else NONE

   249       | dest_numeral _ = NONE;

   250   in dest_numeral end;

   252 fun implode_monad c_bind t =

   253   let

   254     fun dest_monad (IConst (c, _) `$ t1 `$ t2) =

   255           if c = c_bind

   256             then case CodeThingol.split_abs t2

   257              of SOME (((v, pat), ty), t') =>

   258                   SOME ((SOME (((SOME v, pat), ty), true), t1), t')

   259               | NONE => NONE

   260             else NONE

   261       | dest_monad t = case CodeThingol.split_let t

   262            of SOME (((pat, ty), tbind), t') =>

   263                 SOME ((SOME (((NONE, SOME pat), ty), false), tbind), t')

   264             | NONE => NONE;

   265   in CodeThingol.unfoldr dest_monad t end;

   268 (** name auxiliary **)

   270 val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode;

   271 val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode;

   273 val dest_name =

   274   apfst NameSpace.implode o split_last o fst o split_last o NameSpace.explode;

   276 fun mk_modl_name_tab init_names prefix module_alias code =

   277   let

   278     fun nsp_map f = NameSpace.explode #> map f #> NameSpace.implode;

   279     fun mk_alias name =

   280      case module_alias name

   281       of SOME name' => name'

   282        | NONE => nsp_map (fn name => (the_single o fst)

   283             (Name.variants [name] init_names)) name;

   284     fun mk_prefix name =

   285       case prefix

   286        of SOME prefix => NameSpace.append prefix name

   287         | NONE => name;

   288     val tab =

   289       Symtab.empty

   290       |> Graph.fold ((fn name => Symtab.default (name, (mk_alias #> mk_prefix) name))

   291            o fst o dest_name o fst)

   292              code

   293   in fn name => (the o Symtab.lookup tab) name end;

   297 (** SML/OCaml serializer **)

   299 datatype ml_def =

   300     MLFuns of (string * (typscheme * (iterm list * iterm) list)) list

   301   | MLDatas of (string * ((vname * sort) list * (string * itype list) list)) list

   302   | MLClass of string * (vname * ((class * string) list * (string * itype) list))

   303   | MLClassinst of string * ((class * (string * (vname * sort) list))

   304         * ((class * (string * (string * dict list list))) list

   305       * (string * const) list));

   307 fun pr_sml tyco_syntax const_syntax labelled_name init_syms deresolv is_cons ml_def =

   308   let

   309     val pr_label_classrel = translate_string (fn "." => "__" | c => c)

   310       o NameSpace.qualifier;

   311     val pr_label_classparam = NameSpace.base o NameSpace.qualifier;

   312     fun pr_dicts fxy ds =

   313       let

   314         fun pr_dictvar (v, (_, 1)) = first_upper v ^ "_"

   315           | pr_dictvar (v, (i, _)) = first_upper v ^ string_of_int (i+1) ^ "_";

   316         fun pr_proj [] p =

   317               p

   318           | pr_proj [p'] p =

   319               brackets [p', p]

   320           | pr_proj (ps as _ :: _) p =

   321               brackets [Pretty.enum " o" "(" ")" ps, p];

   322         fun pr_dictc fxy (DictConst (inst, dss)) =

   323               brackify fxy ((str o deresolv) inst :: map (pr_dicts BR) dss)

   324           | pr_dictc fxy (DictVar (classrels, v)) =

   325               pr_proj (map (str o deresolv) classrels) ((str o pr_dictvar) v)

   326       in case ds

   327        of [] => str "()"

   328         | [d] => pr_dictc fxy d

   329         | _ :: _ => (Pretty.list "(" ")" o map (pr_dictc NOBR)) ds

   330       end;

   331     fun pr_tyvars vs =

   332       vs

   333       |> map (fn (v, sort) => map_index (fn (i, _) =>

   334            DictVar ([], (v, (i, length sort)))) sort)

   335       |> map (pr_dicts BR);

   336     fun pr_tycoexpr fxy (tyco, tys) =

   337       let

   338         val tyco' = (str o deresolv) tyco

   339       in case map (pr_typ BR) tys

   340        of [] => tyco'

   341         | [p] => Pretty.block [p, Pretty.brk 1, tyco']

   342         | (ps as _::_) => Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, tyco']

   343       end

   344     and pr_typ fxy (tyco `%% tys) =

   345           (case tyco_syntax tyco

   346            of NONE => pr_tycoexpr fxy (tyco, tys)

   347             | SOME (i, pr) =>

   348                 if not (i = length tys)

   349                 then error ("Number of argument mismatch in customary serialization: "

   350                   ^ (string_of_int o length) tys ^ " given, "

   351                   ^ string_of_int i ^ " expected")

   352                 else pr pr_typ fxy tys)

   353       | pr_typ fxy (ITyVar v) =

   354           str ("'" ^ v);

   355     fun pr_term lhs vars fxy (IConst c) =

   356           pr_app lhs vars fxy (c, [])

   357       | pr_term lhs vars fxy (IVar v) =

   358           str (CodeName.lookup_var vars v)

   359       | pr_term lhs vars fxy (t as t1 `$ t2) =

   360           (case CodeThingol.unfold_const_app t

   361            of SOME c_ts => pr_app lhs vars fxy c_ts

   362             | NONE =>

   363                 brackify fxy [pr_term lhs vars NOBR t1, pr_term lhs vars BR t2])

   364       | pr_term lhs vars fxy (t as _ `|-> _) =

   365           let

   366             val (binds, t') = CodeThingol.unfold_abs t;

   367             fun pr ((v, pat), ty) =

   368               pr_bind NOBR ((SOME v, pat), ty)

   369               #>> (fn p => concat [str "fn", p, str "=>"]);

   370             val (ps, vars') = fold_map pr binds vars;

   371           in brackets (ps @ [pr_term lhs vars' NOBR t']) end

   372       | pr_term lhs vars fxy (ICase (cases as (_, t0))) =

   373           (case CodeThingol.unfold_const_app t0

   374            of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)

   375                 then pr_case vars fxy cases

   376                 else pr_app lhs vars fxy c_ts

   377             | NONE => pr_case vars fxy cases)

   378     and pr_app' lhs vars (app as ((c, (iss, tys)), ts)) =

   379       if is_cons c then let

   380         val k = length tys

   381       in if k < 2 then

   382         (str o deresolv) c :: map (pr_term lhs vars BR) ts

   383       else if k = length ts then

   384         [(str o deresolv) c, Pretty.enum "," "(" ")" (map (pr_term lhs vars NOBR) ts)]

   385       else [pr_term lhs vars BR (CodeThingol.eta_expand app k)] end else

   386         (str o deresolv) c

   387           :: (map (pr_dicts BR) o filter_out null) iss @ map (pr_term lhs vars BR) ts

   388     and pr_app lhs vars = gen_pr_app pr_app' pr_term const_syntax

   389       labelled_name is_cons lhs vars

   390     and pr_bind' ((NONE, NONE), _) = str "_"

   391       | pr_bind' ((SOME v, NONE), _) = str v

   392       | pr_bind' ((NONE, SOME p), _) = p

   393       | pr_bind' ((SOME v, SOME p), _) = concat [str v, str "as", p]

   394     and pr_bind fxy = gen_pr_bind pr_bind' pr_term fxy

   395     and pr_case vars fxy (cases as ((_, [_]), _)) =

   396           let

   397             val (binds, t') = CodeThingol.unfold_let (ICase cases);

   398             fun pr ((pat, ty), t) vars =

   399               vars

   400               |> pr_bind NOBR ((NONE, SOME pat), ty)

   401               |>> (fn p => semicolon [str "val", p, str "=", pr_term false vars NOBR t])

   402             val (ps, vars') = fold_map pr binds vars;

   403           in

   404             Pretty.chunks [

   405               [str ("let"), Pretty.fbrk, Pretty.chunks ps] |> Pretty.block,

   406               [str ("in"), Pretty.fbrk, pr_term false vars' NOBR t'] |> Pretty.block,

   407               str ("end")

   408             ]

   409           end

   410       | pr_case vars fxy (((td, ty), b::bs), _) =

   411           let

   412             fun pr delim (pat, t) =

   413               let

   414                 val (p, vars') = pr_bind NOBR ((NONE, SOME pat), ty) vars;

   415               in

   416                 concat [str delim, p, str "=>", pr_term false vars' NOBR t]

   417               end;

   418           in

   419             (Pretty.enclose "(" ")" o single o brackify fxy) (

   420               str "case"

   421               :: pr_term false vars NOBR td

   422               :: pr "of" b

   423               :: map (pr "|") bs

   424             )

   425           end

   426       | pr_case vars fxy ((_, []), _) = str "raise Fail \"empty case\""

   427     fun pr_def (MLFuns (funns as (funn :: funns'))) =

   428           let

   429             val definer =

   430               let

   431                 fun no_args _ ((ts, _) :: _) = length ts

   432                   | no_args ty [] = (length o fst o CodeThingol.unfold_fun) ty;

   433                 fun mk 0 [] = "val"

   434                   | mk 0 vs = if (null o filter_out (null o snd)) vs

   435                       then "val" else "fun"

   436                   | mk k _ = "fun";

   437                 fun chk (_, ((vs, ty), eqs)) NONE = SOME (mk (no_args ty eqs) vs)

   438                   | chk (_, ((vs, ty), eqs)) (SOME defi) =

   439                       if defi = mk (no_args ty eqs) vs then SOME defi

   440                       else error ("Mixing simultaneous vals and funs not implemented: "

   441                         ^ commas (map (labelled_name o fst) funns));

   442               in the (fold chk funns NONE) end;

   443             fun pr_funn definer (name, ((raw_vs, ty), [])) =

   444                   let

   445                     val vs = filter_out (null o snd) raw_vs;

   446                     val n = length vs + (length o fst o CodeThingol.unfold_fun) ty;

   447                     val exc_str =

   448                       (ML_Syntax.print_string o NameSpace.base o NameSpace.qualifier) name;

   449                   in

   450                     concat (

   451                       str definer

   452                       :: (str o deresolv) name

   453                       :: map str (replicate n "_")

   454                       @ str "="

   455                       :: str "raise"

   456                       :: str "(Fail"

   457                       :: str exc_str

   458                       @@ str ")"

   459                     )

   460                   end

   461               | pr_funn definer (name, ((raw_vs, ty), eqs as eq :: eqs')) =

   462                   let

   463                     val vs = filter_out (null o snd) raw_vs;

   464                     val shift = if null eqs' then I else

   465                       map (Pretty.block o single o Pretty.block o single);

   466                     fun pr_eq definer (ts, t) =

   467                       let

   468                         val consts = map_filter

   469                           (fn c => if (is_some o const_syntax) c

   470                             then NONE else (SOME o NameSpace.base o deresolv) c)

   471                             ((fold o CodeThingol.fold_constnames) (insert (op =)) (t :: ts) []);

   472                         val vars = init_syms

   473                           |> CodeName.intro_vars consts

   474                           |> CodeName.intro_vars ((fold o CodeThingol.fold_unbound_varnames)

   475                                (insert (op =)) ts []);

   476                       in

   477                         concat (

   478                           [str definer, (str o deresolv) name]

   479                           @ (if null ts andalso null vs

   480                              then [str ":", pr_typ NOBR ty]

   481                              else

   482                                pr_tyvars vs

   483                                @ map (pr_term true vars BR) ts)

   484                        @ [str "=", pr_term false vars NOBR t]

   485                         )

   486                       end

   487                   in

   488                     (Pretty.block o Pretty.fbreaks o shift) (

   489                       pr_eq definer eq

   490                       :: map (pr_eq "|") eqs'

   491                     )

   492                   end;

   493             val (ps, p) = split_last (pr_funn definer funn :: map (pr_funn "and") funns');

   494           in Pretty.chunks (ps @ [Pretty.block ([p, str ";"])]) end

   495      | pr_def (MLDatas (datas as (data :: datas'))) =

   496           let

   497             fun pr_co (co, []) =

   498                   str (deresolv co)

   499               | pr_co (co, tys) =

   500                   concat [

   501                     str (deresolv co),

   502                     str "of",

   503                     Pretty.enum " *" "" "" (map (pr_typ (INFX (2, X))) tys)

   504                   ];

   505             fun pr_data definer (tyco, (vs, [])) =

   506                   concat (

   507                     str definer

   508                     :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)

   509                     :: str "="

   510                     @@ str "EMPTY__"

   511                   )

   512               | pr_data definer (tyco, (vs, cos)) =

   513                   concat (

   514                     str definer

   515                     :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)

   516                     :: str "="

   517                     :: separate (str "|") (map pr_co cos)

   518                   );

   519             val (ps, p) = split_last

   520               (pr_data "datatype" data :: map (pr_data "and") datas');

   521           in Pretty.chunks (ps @ [Pretty.block ([p, str ";"])]) end

   522      | pr_def (MLClass (class, (v, (superclasses, classparams)))) =

   523           let

   524             val w = first_upper v ^ "_";

   525             fun pr_superclass_field (class, classrel) =

   526               (concat o map str) [

   527                 pr_label_classrel classrel, ":", "'" ^ v, deresolv class

   528               ];

   529             fun pr_classparam_field (classparam, ty) =

   530               concat [

   531                 (str o pr_label_classparam) classparam, str ":", pr_typ NOBR ty

   532               ];

   533             fun pr_classparam_proj (classparam, _) =

   534               semicolon [

   535                 str "fun",

   536                 (str o deresolv) classparam,

   537                 Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ deresolv class)],

   538                 str "=",

   539                 str ("#" ^ pr_label_classparam classparam),

   540                 str w

   541               ];

   542             fun pr_superclass_proj (_, classrel) =

   543               semicolon [

   544                 str "fun",

   545                 (str o deresolv) classrel,

   546                 Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ deresolv class)],

   547                 str "=",

   548                 str ("#" ^ pr_label_classrel classrel),

   549                 str w

   550               ];

   551           in

   552             Pretty.chunks (

   553               concat [

   554                 str ("type '" ^ v),

   555                 (str o deresolv) class,

   556                 str "=",

   557                 Pretty.enum "," "{" "};" (

   558                   map pr_superclass_field superclasses @ map pr_classparam_field classparams

   559                 )

   560               ]

   561               :: map pr_superclass_proj superclasses

   562               @ map pr_classparam_proj classparams

   563             )

   564           end

   565      | pr_def (MLClassinst (inst, ((class, (tyco, arity)), (superarities, classparam_insts)))) =

   566           let

   567             fun pr_superclass (_, (classrel, dss)) =

   568               concat [

   569                 (str o pr_label_classrel) classrel,

   570                 str "=",

   571                 pr_dicts NOBR [DictConst dss]

   572               ];

   573             fun pr_classparam (classparam, c_inst) =

   574               concat [

   575                 (str o pr_label_classparam) classparam,

   576                 str "=",

   577                 pr_app false init_syms NOBR (c_inst, [])

   578               ];

   579           in

   580             semicolon ([

   581               str (if null arity then "val" else "fun"),

   582               (str o deresolv) inst ] @

   583               pr_tyvars arity @ [

   584               str "=",

   585               Pretty.enum "," "{" "}"

   586                 (map pr_superclass superarities @ map pr_classparam classparam_insts),

   587               str ":",

   588               pr_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity])

   589             ])

   590           end;

   591   in pr_def ml_def end;

   593 fun pr_sml_modl name content =

   594   Pretty.chunks ([

   595     str ("structure " ^ name ^ " = "),

   596     str "struct",

   597     str ""

   598   ] @ content @ [

   599     str "",

   600     str ("end; (*struct " ^ name ^ "*)")

   601   ]);

   603 fun pr_ocaml tyco_syntax const_syntax labelled_name

   604     init_syms deresolv is_cons ml_def =

   605   let

   606     fun pr_dicts fxy ds =

   607       let

   608         fun pr_dictvar (v, (_, 1)) = "_" ^ first_upper v

   609           | pr_dictvar (v, (i, _)) = "_" ^ first_upper v ^ string_of_int (i+1);

   610         fun pr_proj ps p =

   611           fold_rev (fn p2 => fn p1 => Pretty.block [p1, str ".", str p2]) ps p

   612         fun pr_dictc fxy (DictConst (inst, dss)) =

   613               brackify fxy ((str o deresolv) inst :: map (pr_dicts BR) dss)

   614           | pr_dictc fxy (DictVar (classrels, v)) =

   615               pr_proj (map deresolv classrels) ((str o pr_dictvar) v)

   616       in case ds

   617        of [] => str "()"

   618         | [d] => pr_dictc fxy d

   619         | _ :: _ => (Pretty.list "(" ")" o map (pr_dictc NOBR)) ds

   620       end;

   621     fun pr_tyvars vs =

   622       vs

   623       |> map (fn (v, sort) => map_index (fn (i, _) =>

   624            DictVar ([], (v, (i, length sort)))) sort)

   625       |> map (pr_dicts BR);

   626     fun pr_tycoexpr fxy (tyco, tys) =

   627       let

   628         val tyco' = (str o deresolv) tyco

   629       in case map (pr_typ BR) tys

   630        of [] => tyco'

   631         | [p] => Pretty.block [p, Pretty.brk 1, tyco']

   632         | (ps as _::_) => Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, tyco']

   633       end

   634     and pr_typ fxy (tyco `%% tys) =

   635           (case tyco_syntax tyco

   636            of NONE => pr_tycoexpr fxy (tyco, tys)

   637             | SOME (i, pr) =>

   638                 if not (i = length tys)

   639                 then error ("Number of argument mismatch in customary serialization: "

   640                   ^ (string_of_int o length) tys ^ " given, "

   641                   ^ string_of_int i ^ " expected")

   642                 else pr pr_typ fxy tys)

   643       | pr_typ fxy (ITyVar v) =

   644           str ("'" ^ v);

   645     fun pr_term lhs vars fxy (IConst c) =

   646           pr_app lhs vars fxy (c, [])

   647       | pr_term lhs vars fxy (IVar v) =

   648           str (CodeName.lookup_var vars v)

   649       | pr_term lhs vars fxy (t as t1 `$ t2) =

   650           (case CodeThingol.unfold_const_app t

   651            of SOME c_ts => pr_app lhs vars fxy c_ts

   652             | NONE =>

   653                 brackify fxy [pr_term lhs vars NOBR t1, pr_term lhs vars BR t2])

   654       | pr_term lhs vars fxy (t as _ `|-> _) =

   655           let

   656             val (binds, t') = CodeThingol.unfold_abs t;

   657             fun pr ((v, pat), ty) = pr_bind BR ((SOME v, pat), ty);

   658             val (ps, vars') = fold_map pr binds vars;

   659           in brackets (str "fun" :: ps @ str "->" @@ pr_term lhs vars' NOBR t') end

   660       | pr_term lhs vars fxy (ICase (cases as (_, t0))) = (case CodeThingol.unfold_const_app t0

   661            of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)

   662                 then pr_case vars fxy cases

   663                 else pr_app lhs vars fxy c_ts

   664             | NONE => pr_case vars fxy cases)

   665     and pr_app' lhs vars (app as ((c, (iss, tys)), ts)) =

   666       if is_cons c then

   667         if length tys = length ts

   668         then case ts

   669          of [] => [(str o deresolv) c]

   670           | [t] => [(str o deresolv) c, pr_term lhs vars BR t]

   671           | _ => [(str o deresolv) c, Pretty.enum "," "(" ")"

   672                     (map (pr_term lhs vars NOBR) ts)]

   673         else [pr_term lhs vars BR (CodeThingol.eta_expand app (length tys))]

   674       else (str o deresolv) c

   675         :: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term lhs vars BR) ts)

   676     and pr_app lhs vars = gen_pr_app pr_app' pr_term const_syntax

   677       labelled_name is_cons lhs vars

   678     and pr_bind' ((NONE, NONE), _) = str "_"

   679       | pr_bind' ((SOME v, NONE), _) = str v

   680       | pr_bind' ((NONE, SOME p), _) = p

   681       | pr_bind' ((SOME v, SOME p), _) = brackets [p, str "as", str v]

   682     and pr_bind fxy = gen_pr_bind pr_bind' pr_term fxy

   683     and pr_case vars fxy (cases as ((_, [_]), _)) =

   684           let

   685             val (binds, t') = CodeThingol.unfold_let (ICase cases);

   686             fun pr ((pat, ty), t) vars =

   687               vars

   688               |> pr_bind NOBR ((NONE, SOME pat), ty)

   689               |>> (fn p => concat

   690                   [str "let", p, str "=", pr_term false vars NOBR t, str "in"])

   691             val (ps, vars') = fold_map pr binds vars;

   692           in Pretty.chunks (ps @| pr_term false vars' NOBR t') end

   693       | pr_case vars fxy (((td, ty), b::bs), _) =

   694           let

   695             fun pr delim (pat, t) =

   696               let

   697                 val (p, vars') = pr_bind NOBR ((NONE, SOME pat), ty) vars;

   698               in concat [str delim, p, str "->", pr_term false vars' NOBR t] end;

   699           in

   700             (Pretty.enclose "(" ")" o single o brackify fxy) (

   701               str "match"

   702               :: pr_term false vars NOBR td

   703               :: pr "with" b

   704               :: map (pr "|") bs

   705             )

   706           end

   707       | pr_case vars fxy ((_, []), _) = str "failwith \"empty case\"";

   708     fun pr_def (MLFuns (funns as funn :: funns')) =

   709           let

   710             fun fish_parm _ (w as SOME _) = w

   711               | fish_parm (IVar v) NONE = SOME v

   712               | fish_parm _ NONE = NONE;

   713             fun fillup_parm _ (_, SOME v) = v

   714               | fillup_parm x (i, NONE) = x ^ string_of_int i;

   715             fun fish_parms vars eqs =

   716               let

   717                 val fished1 = fold (map2 fish_parm) eqs (replicate (length (hd eqs)) NONE);

   718                 val x = Name.variant (map_filter I fished1) "x";

   719                 val fished2 = map_index (fillup_parm x) fished1;

   720                 val (fished3, _) = Name.variants fished2 Name.context;

   721                 val vars' = CodeName.intro_vars fished3 vars;

   722               in map (CodeName.lookup_var vars') fished3 end;

   723             fun pr_eq (ts, t) =

   724               let

   725                 val consts = map_filter

   726                   (fn c => if (is_some o const_syntax) c

   727                     then NONE else (SOME o NameSpace.base o deresolv) c)

   728                     ((fold o CodeThingol.fold_constnames) (insert (op =)) (t :: ts) []);

   729                 val vars = init_syms

   730                   |> CodeName.intro_vars consts

   731                   |> CodeName.intro_vars ((fold o CodeThingol.fold_unbound_varnames)

   732                       (insert (op =)) ts []);

   733               in concat [

   734                 (Pretty.block o Pretty.commas) (map (pr_term true vars NOBR) ts),

   735                 str "->",

   736                 pr_term false vars NOBR t

   737               ] end;

   738             fun pr_eqs name ty [] =

   739                   let

   740                     val n = (length o fst o CodeThingol.unfold_fun) ty;

   741                     val exc_str =

   742                       (ML_Syntax.print_string o NameSpace.base o NameSpace.qualifier) name;

   743                   in

   744                     concat (

   745                       map str (replicate n "_")

   746                       @ str "="

   747                       :: str "failwith"

   748                       @@ str exc_str

   749                     )

   750                   end

   751               | pr_eqs _ _ [(ts, t)] =

   752                   let

   753                     val consts = map_filter

   754                       (fn c => if (is_some o const_syntax) c

   755                         then NONE else (SOME o NameSpace.base o deresolv) c)

   756                         ((fold o CodeThingol.fold_constnames) (insert (op =)) (t :: ts) []);

   757                     val vars = init_syms

   758                       |> CodeName.intro_vars consts

   759                       |> CodeName.intro_vars ((fold o CodeThingol.fold_unbound_varnames)

   760                           (insert (op =)) ts []);

   761                   in

   762                     concat (

   763                       map (pr_term true vars BR) ts

   764                       @ str "="

   765                       @@ pr_term false vars NOBR t

   766                     )

   767                   end

   768               | pr_eqs _ _ (eqs as (eq as ([_], _)) :: eqs') =

   769                   Pretty.block (

   770                     str "="

   771                     :: Pretty.brk 1

   772                     :: str "function"

   773                     :: Pretty.brk 1

   774                     :: pr_eq eq

   775                     :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1]

   776                           o single o pr_eq) eqs'

   777                   )

   778               | pr_eqs _ _ (eqs as eq :: eqs') =

   779                   let

   780                     val consts = map_filter

   781                       (fn c => if (is_some o const_syntax) c

   782                         then NONE else (SOME o NameSpace.base o deresolv) c)

   783                         ((fold o CodeThingol.fold_constnames)

   784                           (insert (op =)) (map snd eqs) []);

   785                     val vars = init_syms

   786                       |> CodeName.intro_vars consts;

   787                     val dummy_parms = (map str o fish_parms vars o map fst) eqs;

   788                   in

   789                     Pretty.block (

   790                       Pretty.breaks dummy_parms

   791                       @ Pretty.brk 1

   792                       :: str "="

   793                       :: Pretty.brk 1

   794                       :: str "match"

   795                       :: Pretty.brk 1

   796                       :: (Pretty.block o Pretty.commas) dummy_parms

   797                       :: Pretty.brk 1

   798                       :: str "with"

   799                       :: Pretty.brk 1

   800                       :: pr_eq eq

   801                       :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1]

   802                            o single o pr_eq) eqs'

   803                     )

   804                   end;

   805             fun pr_funn definer (name, ((vs, ty), eqs)) =

   806               concat (

   807                 str definer

   808                 :: (str o deresolv) name

   809                 :: pr_tyvars (filter_out (null o snd) vs)

   810                 @| pr_eqs name ty eqs

   811               );

   812             val (ps, p) = split_last

   813               (pr_funn "let rec" funn :: map (pr_funn "and") funns');

   814           in Pretty.chunks (ps @ [Pretty.block ([p, str ";;"])]) end

   815      | pr_def (MLDatas (datas as (data :: datas'))) =

   816           let

   817             fun pr_co (co, []) =

   818                   str (deresolv co)

   819               | pr_co (co, tys) =

   820                   concat [

   821                     str (deresolv co),

   822                     str "of",

   823                     Pretty.enum " *" "" "" (map (pr_typ (INFX (2, X))) tys)

   824                   ];

   825             fun pr_data definer (tyco, (vs, [])) =

   826                   concat (

   827                     str definer

   828                     :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)

   829                     :: str "="

   830                     @@ str "EMPTY_"

   831                   )

   832               | pr_data definer (tyco, (vs, cos)) =

   833                   concat (

   834                     str definer

   835                     :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)

   836                     :: str "="

   837                     :: separate (str "|") (map pr_co cos)

   838                   );

   839             val (ps, p) = split_last

   840               (pr_data "type" data :: map (pr_data "and") datas');

   841           in Pretty.chunks (ps @ [Pretty.block ([p, str ";;"])]) end

   842      | pr_def (MLClass (class, (v, (superclasses, classparams)))) =

   843           let

   844             val w = "_" ^ first_upper v;

   845             fun pr_superclass_field (class, classrel) =

   846               (concat o map str) [

   847                 deresolv classrel, ":", "'" ^ v, deresolv class

   848               ];

   849             fun pr_classparam_field (classparam, ty) =

   850               concat [

   851                 (str o deresolv) classparam, str ":", pr_typ NOBR ty

   852               ];

   853             fun pr_classparam_proj (classparam, _) =

   854               concat [

   855                 str "let",

   856                 (str o deresolv) classparam,

   857                 str w,

   858                 str "=",

   859                 str (w ^ "." ^ deresolv classparam ^ ";;")

   860               ];

   861           in Pretty.chunks (

   862             concat [

   863               str ("type '" ^ v),

   864               (str o deresolv) class,

   865               str "=",

   866               Pretty.enum ";" "{" "};;" (

   867                 map pr_superclass_field superclasses

   868                 @ map pr_classparam_field classparams

   869               )

   870             ]

   871             :: map pr_classparam_proj classparams

   872           ) end

   873      | pr_def (MLClassinst (inst, ((class, (tyco, arity)), (superarities, classparam_insts)))) =

   874           let

   875             fun pr_superclass (_, (classrel, dss)) =

   876               concat [

   877                 (str o deresolv) classrel,

   878                 str "=",

   879                 pr_dicts NOBR [DictConst dss]

   880               ];

   881             fun pr_classparam_inst (classparam, c_inst) =

   882               concat [

   883                 (str o deresolv) classparam,

   884                 str "=",

   885                 pr_app false init_syms NOBR (c_inst, [])

   886               ];

   887           in

   888             concat (

   889               str "let"

   890               :: (str o deresolv) inst

   891               :: pr_tyvars arity

   892               @ str "="

   893               @@ (Pretty.enclose "(" ");;" o Pretty.breaks) [

   894                 Pretty.enum ";" "{" "}" (map pr_superclass superarities

   895                   @ map pr_classparam_inst classparam_insts),

   896                 str ":",

   897                 pr_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity])

   898               ]

   899             )

   900           end;

   901   in pr_def ml_def end;

   903 fun pr_ocaml_modl name content =

   904   Pretty.chunks ([

   905     str ("module " ^ name ^ " = "),

   906     str "struct",

   907     str ""

   908   ] @ content @ [

   909     str "",

   910     str ("end;; (*struct " ^ name ^ "*)")

   911   ]);

   913 val code_width = ref 80;

   914 fun code_output p = Pretty.setmp_margin (!code_width) Pretty.output p ^ "\n";

   916 fun seri_ml pr_def pr_modl module output labelled_name reserved_syms includes raw_module_alias

   917   (_ : string -> class_syntax option) tyco_syntax const_syntax code =

   918   let

   919     val module_alias = if is_some module then K module else raw_module_alias;

   920     val is_cons = CodeThingol.is_cons code;

   921     datatype node =

   922         Def of string * ml_def option

   923       | Module of string * ((Name.context * Name.context) * node Graph.T);

   924     val init_names = Name.make_context reserved_syms;

   925     val init_module = ((init_names, init_names), Graph.empty);

   926     fun map_node [] f = f

   927       | map_node (m::ms) f =

   928           Graph.default_node (m, Module (m, init_module))

   929           #> Graph.map_node m (fn (Module (dmodlname, (nsp, nodes))) =>

   930                Module (dmodlname, (nsp, map_node ms f nodes)));

   931     fun map_nsp_yield [] f (nsp, nodes) =

   932           let

   933             val (x, nsp') = f nsp

   934           in (x, (nsp', nodes)) end

   935       | map_nsp_yield (m::ms) f (nsp, nodes) =

   936           let

   937             val (x, nodes') =

   938               nodes

   939               |> Graph.default_node (m, Module (m, init_module))

   940               |> Graph.map_node_yield m (fn Module (dmodlname, nsp_nodes) =>

   941                   let

   942                     val (x, nsp_nodes') = map_nsp_yield ms f nsp_nodes

   943                   in (x, Module (dmodlname, nsp_nodes')) end)

   944           in (x, (nsp, nodes')) end;

   945     val init_syms = CodeName.make_vars reserved_syms;

   946     val name_modl = mk_modl_name_tab init_names NONE module_alias code;

   947     fun name_def upper name nsp =

   948       let

   949         val (_, base) = dest_name name;

   950         val base' = if upper then first_upper base else base;

   951         val ([base''], nsp') = Name.variants [base'] nsp;

   952       in (base'', nsp') end;

   953     fun map_nsp_fun f (nsp_fun, nsp_typ) =

   954       let

   955         val (x, nsp_fun') = f nsp_fun

   956       in (x, (nsp_fun', nsp_typ)) end;

   957     fun map_nsp_typ f (nsp_fun, nsp_typ) =

   958       let

   959         val (x, nsp_typ') = f nsp_typ

   960       in (x, (nsp_fun, nsp_typ')) end;

   961     fun mk_funs defs =

   962       fold_map

   963         (fn (name, CodeThingol.Fun info) =>

   964               map_nsp_fun (name_def false name) >>

   965                 (fn base => (base, (name, (apsnd o map) fst info)))

   966           | (name, def) =>

   967               error ("Function block containing illegal definition: " ^ labelled_name name)

   968         ) defs

   969       >> (split_list #> apsnd MLFuns);

   970     fun mk_datatype defs =

   971       fold_map

   972         (fn (name, CodeThingol.Datatype info) =>

   973               map_nsp_typ (name_def false name) >> (fn base => (base, SOME (name, info)))

   974           | (name, CodeThingol.Datatypecons _) =>

   975               map_nsp_fun (name_def true name) >> (fn base => (base, NONE))

   976           | (name, def) =>

   977               error ("Datatype block containing illegal definition: " ^ labelled_name name)

   978         ) defs

   979       >> (split_list #> apsnd (map_filter I

   980         #> (fn [] => error ("Datatype block without data definition: "

   981                   ^ (commas o map (labelled_name o fst)) defs)

   982              | infos => MLDatas infos)));

   983     fun mk_class defs =

   984       fold_map

   985         (fn (name, CodeThingol.Class info) =>

   986               map_nsp_typ (name_def false name) >> (fn base => (base, SOME (name, info)))

   987           | (name, CodeThingol.Classrel _) =>

   988               map_nsp_fun (name_def false name) >> (fn base => (base, NONE))

   989           | (name, CodeThingol.Classparam _) =>

   990               map_nsp_fun (name_def false name) >> (fn base => (base, NONE))

   991           | (name, def) =>

   992               error ("Class block containing illegal definition: " ^ labelled_name name)

   993         ) defs

   994       >> (split_list #> apsnd (map_filter I

   995         #> (fn [] => error ("Class block without class definition: "

   996                   ^ (commas o map (labelled_name o fst)) defs)

   997              | [info] => MLClass info)));

   998     fun mk_inst [(name, CodeThingol.Classinst info)] =

   999       map_nsp_fun (name_def false name)

  1000       >> (fn base => ([base], MLClassinst (name, (apsnd o apsnd o map) fst info)));

  1001     fun add_group mk defs nsp_nodes =

  1002       let

  1003         val names as (name :: names') = map fst defs;

  1004         val deps =

  1005           []

  1006           |> fold (fold (insert (op =)) o Graph.imm_succs code) names

  1007           |> subtract (op =) names;

  1008         val (modls, _) = (split_list o map dest_name) names;

  1009         val modl' = (the_single o distinct (op =) o map name_modl) modls

  1010           handle Empty =>

  1011             error ("Different namespace prefixes for mutual dependencies:\n"

  1012               ^ commas (map labelled_name names)

  1013               ^ "\n"

  1014               ^ commas (map (NameSpace.qualifier o NameSpace.qualifier) names));

  1015         val modl_explode = NameSpace.explode modl';

  1016         fun add_dep name name'' =

  1017           let

  1018             val modl'' = (name_modl o fst o dest_name) name'';

  1019           in if modl' = modl'' then

  1020             map_node modl_explode

  1021               (Graph.add_edge (name, name''))

  1022           else let

  1023             val (common, (diff1::_, diff2::_)) = chop_prefix (op =)

  1024               (modl_explode, NameSpace.explode modl'');

  1025           in

  1026             map_node common

  1027               (fn gr => Graph.add_edge_acyclic (diff1, diff2) gr

  1028                 handle Graph.CYCLES _ => error ("Dependency "

  1029                   ^ quote name ^ " -> " ^ quote name''

  1030                   ^ " would result in module dependency cycle"))

  1031           end end;

  1032       in

  1033         nsp_nodes

  1034         |> map_nsp_yield modl_explode (mk defs)

  1035         |-> (fn (base' :: bases', def') =>

  1036            apsnd (map_node modl_explode (Graph.new_node (name, (Def (base', SOME def')))

  1037               #> fold2 (fn name' => fn base' =>

  1038                    Graph.new_node (name', (Def (base', NONE)))) names' bases')))

  1039         |> apsnd (fold (fn name => fold (add_dep name) deps) names)

  1040         |> apsnd (fold_product (curry (map_node modl_explode o Graph.add_edge)) names names)

  1041       end;

  1042     fun group_defs [(_, CodeThingol.Bot)] =

  1043           I

  1044       | group_defs ((defs as (_, CodeThingol.Fun _)::_)) =

  1045           add_group mk_funs defs

  1046       | group_defs ((defs as (_, CodeThingol.Datatypecons _)::_)) =

  1047           add_group mk_datatype defs

  1048       | group_defs ((defs as (_, CodeThingol.Datatype _)::_)) =

  1049           add_group mk_datatype defs

  1050       | group_defs ((defs as (_, CodeThingol.Class _)::_)) =

  1051           add_group mk_class defs

  1052       | group_defs ((defs as (_, CodeThingol.Classrel _)::_)) =

  1053           add_group mk_class defs

  1054       | group_defs ((defs as (_, CodeThingol.Classparam _)::_)) =

  1055           add_group mk_class defs

  1056       | group_defs ((defs as [(_, CodeThingol.Classinst _)])) =

  1057           add_group mk_inst defs

  1058       | group_defs defs = error ("Illegal mutual dependencies: " ^

  1059           (commas o map (labelled_name o fst)) defs)

  1060     val (_, nodes) =

  1061       init_module

  1062       |> fold group_defs (map (AList.make (Graph.get_node code))

  1063           (rev (Graph.strong_conn code)))

  1064     fun deresolver prefix name =

  1065       let

  1066         val modl = (fst o dest_name) name;

  1067         val modl' = (NameSpace.explode o name_modl) modl;

  1068         val (_, (_, remainder)) = chop_prefix (op =) (prefix, modl');

  1069         val defname' =

  1070           nodes

  1071           |> fold (fn m => fn g => case Graph.get_node g m

  1072               of Module (_, (_, g)) => g) modl'

  1073           |> (fn g => case Graph.get_node g name of Def (defname, _) => defname);

  1074       in

  1075         NameSpace.implode (remainder @ [defname'])

  1076       end handle Graph.UNDEF _ =>

  1077         error ("Unknown definition name: " ^ labelled_name name);

  1078     fun pr_node prefix (Def (_, NONE)) =

  1079           NONE

  1080       | pr_node prefix (Def (_, SOME def)) =

  1081           SOME (pr_def tyco_syntax const_syntax labelled_name init_syms

  1082             (deresolver prefix) is_cons def)

  1083       | pr_node prefix (Module (dmodlname, (_, nodes))) =

  1084           SOME (pr_modl dmodlname (

  1085             separate (str "")

  1086                 ((map_filter (pr_node (prefix @ [dmodlname]) o Graph.get_node nodes)

  1087                 o rev o flat o Graph.strong_conn) nodes)));

  1088     val p = Pretty.chunks (separate (str "") (map snd includes @ (map_filter

  1089       (pr_node [] o Graph.get_node nodes) o rev o flat o Graph.strong_conn) nodes))

  1090   in output p end;

  1092 val eval_verbose = ref false;

  1094 fun isar_seri_sml module file =

  1095   let

  1096     val output = case file

  1097      of NONE => use_text "generated code" Output.ml_output (!eval_verbose) o code_output

  1098       | SOME "-" => PrintMode.setmp [] writeln o code_output

  1099       | SOME file => File.write (Path.explode file) o code_output;

  1100   in

  1101     parse_args (Scan.succeed ())

  1102     #> (fn () => seri_ml pr_sml pr_sml_modl module output)

  1103   end;

  1105 fun isar_seri_ocaml module file =

  1106   let

  1107     val output = case file

  1108      of NONE => error "OCaml: no internal compilation"

  1109       | SOME "-" => PrintMode.setmp [] writeln o code_output

  1110       | SOME file => File.write (Path.explode file) o code_output;

  1111     fun output_file file = File.write (Path.explode file) o code_output;

  1112     val output_diag = PrintMode.setmp [] writeln o code_output;

  1113   in

  1114     parse_args (Scan.succeed ())

  1115     #> (fn () => seri_ml pr_ocaml pr_ocaml_modl module output)

  1116   end;

  1119 (** Haskell serializer **)

  1121 local

  1123 fun pr_bind' ((NONE, NONE), _) = str "_"

  1124   | pr_bind' ((SOME v, NONE), _) = str v

  1125   | pr_bind' ((NONE, SOME p), _) = p

  1126   | pr_bind' ((SOME v, SOME p), _) = brackets [str v, str "@", p]

  1128 val pr_bind_haskell = gen_pr_bind pr_bind';

  1130 in

  1132 fun pr_haskell class_syntax tyco_syntax const_syntax labelled_name

  1133     init_syms deresolv_here deresolv is_cons deriving_show def =

  1134   let

  1135     fun class_name class = case class_syntax class

  1136      of NONE => deresolv class

  1137       | SOME (class, _) => class;

  1138     fun classparam_name class classparam = case class_syntax class

  1139      of NONE => deresolv_here classparam

  1140       | SOME (_, classparam_syntax) => case classparam_syntax classparam

  1141          of NONE => (snd o dest_name) classparam

  1142           | SOME classparam => classparam

  1143     fun pr_typparms tyvars vs =

  1144       case maps (fn (v, sort) => map (pair v) sort) vs

  1145        of [] => str ""

  1146         | xs => Pretty.block [

  1147             Pretty.enum "," "(" ")" (

  1148               map (fn (v, class) => str

  1149                 (class_name class ^ " " ^ CodeName.lookup_var tyvars v)) xs

  1150             ),

  1151             str " => "

  1152           ];

  1153     fun pr_tycoexpr tyvars fxy (tyco, tys) =

  1154       brackify fxy (str tyco :: map (pr_typ tyvars BR) tys)

  1155     and pr_typ tyvars fxy (tycoexpr as tyco `%% tys) =

  1156           (case tyco_syntax tyco

  1157            of NONE =>

  1158                 pr_tycoexpr tyvars fxy (deresolv tyco, tys)

  1159             | SOME (i, pr) =>

  1160                 if not (i = length tys)

  1161                 then error ("Number of argument mismatch in customary serialization: "

  1162                   ^ (string_of_int o length) tys ^ " given, "

  1163                   ^ string_of_int i ^ " expected")

  1164                 else pr (pr_typ tyvars) fxy tys)

  1165       | pr_typ tyvars fxy (ITyVar v) =

  1166           (str o CodeName.lookup_var tyvars) v;

  1167     fun pr_typscheme_expr tyvars (vs, tycoexpr) =

  1168       Pretty.block (pr_typparms tyvars vs @@ pr_tycoexpr tyvars NOBR tycoexpr);

  1169     fun pr_typscheme tyvars (vs, ty) =

  1170       Pretty.block (pr_typparms tyvars vs @@ pr_typ tyvars NOBR ty);

  1171     fun pr_term lhs vars fxy (IConst c) =

  1172           pr_app lhs vars fxy (c, [])

  1173       | pr_term lhs vars fxy (t as (t1 `$ t2)) =

  1174           (case CodeThingol.unfold_const_app t

  1175            of SOME app => pr_app lhs vars fxy app

  1176             | _ =>

  1177                 brackify fxy [

  1178                   pr_term lhs vars NOBR t1,

  1179                   pr_term lhs vars BR t2

  1180                 ])

  1181       | pr_term lhs vars fxy (IVar v) =

  1182           (str o CodeName.lookup_var vars) v

  1183       | pr_term lhs vars fxy (t as _ `|-> _) =

  1184           let

  1185             val (binds, t') = CodeThingol.unfold_abs t;

  1186             fun pr ((v, pat), ty) = pr_bind BR ((SOME v, pat), ty);

  1187             val (ps, vars') = fold_map pr binds vars;

  1188           in brackets (str "\\" :: ps @ str "->" @@ pr_term lhs vars' NOBR t') end

  1189       | pr_term lhs vars fxy (ICase (cases as (_, t0))) =

  1190           (case CodeThingol.unfold_const_app t0

  1191            of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)

  1192                 then pr_case vars fxy cases

  1193                 else pr_app lhs vars fxy c_ts

  1194             | NONE => pr_case vars fxy cases)

  1195     and pr_app' lhs vars ((c, _), ts) =

  1196       (str o deresolv) c :: map (pr_term lhs vars BR) ts

  1197     and pr_app lhs vars = gen_pr_app pr_app' pr_term const_syntax

  1198       labelled_name is_cons lhs vars

  1199     and pr_bind fxy = pr_bind_haskell pr_term fxy

  1200     and pr_case vars fxy (cases as ((_, [_]), _)) =

  1201           let

  1202             val (binds, t) = CodeThingol.unfold_let (ICase cases);

  1203             fun pr ((pat, ty), t) vars =

  1204               vars

  1205               |> pr_bind BR ((NONE, SOME pat), ty)

  1206               |>> (fn p => semicolon [p, str "=", pr_term false vars NOBR t])

  1207             val (ps, vars') = fold_map pr binds vars;

  1208           in

  1209             Pretty.block_enclose (

  1210               str "let {",

  1211               concat [str "}", str "in", pr_term false vars' NOBR t]

  1212             ) ps

  1213           end

  1214       | pr_case vars fxy (((td, ty), bs as _ :: _), _) =

  1215           let

  1216             fun pr (pat, t) =

  1217               let

  1218                 val (p, vars') = pr_bind NOBR ((NONE, SOME pat), ty) vars;

  1219               in semicolon [p, str "->", pr_term false vars' NOBR t] end;

  1220           in

  1221             Pretty.block_enclose (

  1222               concat [str "(case", pr_term false vars NOBR td, str "of", str "{"],

  1223               str "})"

  1224             ) (map pr bs)

  1225           end

  1226       | pr_case vars fxy ((_, []), _) = str "error \"empty case\"";

  1227     fun pr_def (name, CodeThingol.Fun ((vs, ty), [])) =

  1228           let

  1229             val tyvars = CodeName.intro_vars (map fst vs) init_syms;

  1230             val n = (length o fst o CodeThingol.unfold_fun) ty;

  1231           in

  1232             Pretty.chunks [

  1233               Pretty.block [

  1234                 (str o suffix " ::" o deresolv_here) name,

  1235                 Pretty.brk 1,

  1236                 pr_typscheme tyvars (vs, ty),

  1237                 str ";"

  1238               ],

  1239               concat (

  1240                 (str o deresolv_here) name

  1241                 :: map str (replicate n "_")

  1242                 @ str "="

  1243                 :: str "error"

  1244                 @@ (str o (fn s => s ^ ";") o ML_Syntax.print_string

  1245                     o NameSpace.base o NameSpace.qualifier) name

  1246               )

  1247             ]

  1248           end

  1249       | pr_def (name, CodeThingol.Fun ((vs, ty), eqs)) =

  1250           let

  1251             val tyvars = CodeName.intro_vars (map fst vs) init_syms;

  1252             fun pr_eq ((ts, t), _) =

  1253               let

  1254                 val consts = map_filter

  1255                   (fn c => if (is_some o const_syntax) c

  1256                     then NONE else (SOME o NameSpace.base o deresolv) c)

  1257                     ((fold o CodeThingol.fold_constnames) (insert (op =)) (t :: ts) []);

  1258                 val vars = init_syms

  1259                   |> CodeName.intro_vars consts

  1260                   |> CodeName.intro_vars ((fold o CodeThingol.fold_unbound_varnames)

  1261                        (insert (op =)) ts []);

  1262               in

  1263                 semicolon (

  1264                   (str o deresolv_here) name

  1265                   :: map (pr_term true vars BR) ts

  1266                   @ str "="

  1267                   @@ pr_term false vars NOBR t

  1268                 )

  1269               end;

  1270           in

  1271             Pretty.chunks (

  1272               Pretty.block [

  1273                 (str o suffix " ::" o deresolv_here) name,

  1274                 Pretty.brk 1,

  1275                 pr_typscheme tyvars (vs, ty),

  1276                 str ";"

  1277               ]

  1278               :: map pr_eq eqs

  1279             )

  1280           end

  1281       | pr_def (name, CodeThingol.Datatype (vs, [])) =

  1282           let

  1283             val tyvars = CodeName.intro_vars (map fst vs) init_syms;

  1284           in

  1285             semicolon [

  1286               str "data",

  1287               pr_typscheme_expr tyvars (vs, (deresolv_here name, map (ITyVar o fst) vs))

  1288             ]

  1289           end

  1290       | pr_def (name, CodeThingol.Datatype (vs, [(co, [ty])])) =

  1291           let

  1292             val tyvars = CodeName.intro_vars (map fst vs) init_syms;

  1293           in

  1294             semicolon (

  1295               str "newtype"

  1296               :: pr_typscheme_expr tyvars (vs, (deresolv_here name, map (ITyVar o fst) vs))

  1297               :: str "="

  1298               :: (str o deresolv_here) co

  1299               :: pr_typ tyvars BR ty

  1300               :: (if deriving_show name then [str "deriving (Read, Show)"] else [])

  1301             )

  1302           end

  1303       | pr_def (name, CodeThingol.Datatype (vs, co :: cos)) =

  1304           let

  1305             val tyvars = CodeName.intro_vars (map fst vs) init_syms;

  1306             fun pr_co (co, tys) =

  1307               concat (

  1308                 (str o deresolv_here) co

  1309                 :: map (pr_typ tyvars BR) tys

  1310               )

  1311           in

  1312             semicolon (

  1313               str "data"

  1314               :: pr_typscheme_expr tyvars (vs, (deresolv_here name, map (ITyVar o fst) vs))

  1315               :: str "="

  1316               :: pr_co co

  1317               :: map ((fn p => Pretty.block [str "| ", p]) o pr_co) cos

  1318               @ (if deriving_show name then [str "deriving (Read, Show)"] else [])

  1319             )

  1320           end

  1321       | pr_def (name, CodeThingol.Class (v, (superclasses, classparams))) =

  1322           let

  1323             val tyvars = CodeName.intro_vars [v] init_syms;

  1324             fun pr_classparam (classparam, ty) =

  1325               semicolon [

  1326                 (str o classparam_name name) classparam,

  1327                 str "::",

  1328                 pr_typ tyvars NOBR ty

  1329               ]

  1330           in

  1331             Pretty.block_enclose (

  1332               Pretty.block [

  1333                 str "class ",

  1334                 pr_typparms tyvars [(v, map fst superclasses)],

  1335                 str (deresolv_here name ^ " " ^ CodeName.lookup_var tyvars v),

  1336                 str " where {"

  1337               ],

  1338               str "};"

  1339             ) (map pr_classparam classparams)

  1340           end

  1341       | pr_def (_, CodeThingol.Classinst ((class, (tyco, vs)), (_, classparam_insts))) =

  1342           let

  1343             val tyvars = CodeName.intro_vars (map fst vs) init_syms;

  1344             fun pr_instdef ((classparam, c_inst), _) =

  1345               semicolon [

  1346                 (str o classparam_name class) classparam,

  1347                 str "=",

  1348                 pr_app false init_syms NOBR (c_inst, [])

  1349               ];

  1350           in

  1351             Pretty.block_enclose (

  1352               Pretty.block [

  1353                 str "instance ",

  1354                 pr_typparms tyvars vs,

  1355                 str (class_name class ^ " "),

  1356                 pr_typ tyvars BR (tyco `%% map (ITyVar o fst) vs),

  1357                 str " where {"

  1358               ],

  1359               str "};"

  1360             ) (map pr_instdef classparam_insts)

  1361           end;

  1362   in pr_def def end;

  1364 fun pretty_haskell_monad c_bind =

  1365   let

  1366     fun pretty pr vars fxy [(t, _)] =

  1367       let

  1368         val pr_bind = pr_bind_haskell (K pr);

  1369         fun pr_monad (NONE, t) vars =

  1370               (semicolon [pr vars NOBR t], vars)

  1371           | pr_monad (SOME (bind, true), t) vars = vars

  1372               |> pr_bind NOBR bind

  1373               |>> (fn p => semicolon [p, str "<-", pr vars NOBR t])

  1374           | pr_monad (SOME (bind, false), t) vars = vars

  1375               |> pr_bind NOBR bind

  1376               |>> (fn p => semicolon [str "let", p, str "=", pr vars NOBR t]);

  1377         val (binds, t) = implode_monad c_bind t;

  1378         val (ps, vars') = fold_map pr_monad binds vars;

  1379         fun brack p = if eval_fxy BR fxy then Pretty.block [str "(", p, str ")"] else p;

  1380       in (brack o Pretty.block_enclose (str "do {", str "}")) (ps @| pr vars' NOBR t) end;

  1381   in (1, pretty) end;

  1383 end; (*local*)

  1385 fun seri_haskell module_prefix module destination string_classes labelled_name

  1386     reserved_syms includes raw_module_alias

  1387     class_syntax tyco_syntax const_syntax code =

  1388   let

  1389     val _ = Option.map File.check destination;

  1390     val is_cons = CodeThingol.is_cons code;

  1391     val module_alias = if is_some module then K module else raw_module_alias;

  1392     val init_names = Name.make_context reserved_syms;

  1393     val name_modl = mk_modl_name_tab init_names module_prefix module_alias code;

  1394     fun add_def (name, (def, deps)) =

  1395       let

  1396         val (modl, base) = dest_name name;

  1397         val name_def = yield_singleton Name.variants;

  1398         fun add_fun upper (nsp_fun, nsp_typ) =

  1399           let

  1400             val (base', nsp_fun') =

  1401               name_def (if upper then first_upper base else base) nsp_fun

  1402           in (base', (nsp_fun', nsp_typ)) end;

  1403         fun add_typ (nsp_fun, nsp_typ) =

  1404           let

  1405             val (base', nsp_typ') = name_def (first_upper base) nsp_typ

  1406           in (base', (nsp_fun, nsp_typ')) end;

  1407         val add_name =

  1408           case def

  1409            of CodeThingol.Bot => pair base

  1410             | CodeThingol.Fun _ => add_fun false

  1411             | CodeThingol.Datatype _ => add_typ

  1412             | CodeThingol.Datatypecons _ => add_fun true

  1413             | CodeThingol.Class _ => add_typ

  1414             | CodeThingol.Classrel _ => pair base

  1415             | CodeThingol.Classparam _ => add_fun false

  1416             | CodeThingol.Classinst _ => pair base;

  1417         val modlname' = name_modl modl;

  1418         fun add_def base' =

  1419           case def

  1420            of CodeThingol.Bot => I

  1421             | CodeThingol.Datatypecons _ =>

  1422                 cons (name, ((NameSpace.append modlname' base', base'), NONE))

  1423             | CodeThingol.Classrel _ => I

  1424             | CodeThingol.Classparam _ =>

  1425                 cons (name, ((NameSpace.append modlname' base', base'), NONE))

  1426             | _ => cons (name, ((NameSpace.append modlname' base', base'), SOME def));

  1427       in

  1428         Symtab.map_default (modlname', ([], ([], (init_names, init_names))))

  1429               (apfst (fold (insert (op = : string * string -> bool)) deps))

  1430         #> `(fn code => add_name ((snd o snd o the o Symtab.lookup code) modlname'))

  1431         #-> (fn (base', names) =>

  1432               (Symtab.map_entry modlname' o apsnd) (fn (defs, _) =>

  1433               (add_def base' defs, names)))

  1434       end;

  1435     val code' =

  1436       fold add_def (AList.make (fn name =>

  1437         (Graph.get_node code name, Graph.imm_succs code name))

  1438         (Graph.strong_conn code |> flat)) Symtab.empty;

  1439     val init_syms = CodeName.make_vars reserved_syms;

  1440     fun deresolv name =

  1441       (fst o fst o the o AList.lookup (op =) ((fst o snd o the

  1442         o Symtab.lookup code') ((name_modl o fst o dest_name) name))) name

  1443         handle Option => error ("Unknown definition name: " ^ labelled_name name);

  1444     fun deresolv_here name =

  1445       (snd o fst o the o AList.lookup (op =) ((fst o snd o the

  1446         o Symtab.lookup code') ((name_modl o fst o dest_name) name))) name

  1447         handle Option => error ("Unknown definition name: " ^ labelled_name name);

  1448     fun deriving_show tyco =

  1449       let

  1450         fun deriv _ "fun" = false

  1451           | deriv tycos tyco = member (op =) tycos tyco orelse

  1452               case the_default CodeThingol.Bot (try (Graph.get_node code) tyco)

  1453                of CodeThingol.Bot => true

  1454                 | CodeThingol.Datatype (_, cs) => forall (deriv' (tyco :: tycos))

  1455                     (maps snd cs)

  1456         and deriv' tycos (tyco `%% tys) = deriv tycos tyco

  1457               andalso forall (deriv' tycos) tys

  1458           | deriv' _ (ITyVar _) = true

  1459       in deriv [] tyco end;

  1460     fun seri_def qualified = pr_haskell class_syntax tyco_syntax

  1461       const_syntax labelled_name init_syms

  1462       deresolv_here (if qualified then deresolv else deresolv_here) is_cons

  1463       (if string_classes then deriving_show else K false);

  1464     fun write_modulefile (SOME destination) modlname =

  1465           let

  1466             val filename = case modlname

  1467              of "" => Path.explode "Main.hs"

  1468               | _ => (Path.ext "hs" o Path.explode o implode o separate "/"

  1469                     o NameSpace.explode) modlname;

  1470             val pathname = Path.append destination filename;

  1471             val _ = File.mkdir (Path.dir pathname);

  1472           in File.write pathname end

  1473       | write_modulefile NONE _ = PrintMode.setmp [] writeln;

  1474     fun write_module destination (modulename, content) =

  1475       Pretty.chunks [

  1476         str ("module " ^ modulename ^ " where {"),

  1477         str "",

  1478         content,

  1479         str "",

  1480         str "}"

  1481       ]

  1482       |> code_output

  1483       |> write_modulefile destination modulename;

  1484     fun seri_module (modlname', (imports, (defs, _))) =

  1485       let

  1486         val imports' =

  1487           imports

  1488           |> map (name_modl o fst o dest_name)

  1489           |> distinct (op =)

  1490           |> remove (op =) modlname';

  1491         val qualified =

  1492           imports @ map fst defs

  1493           |> distinct (op =)

  1494           |> map_filter (try deresolv)

  1495           |> map NameSpace.base

  1496           |> has_duplicates (op =);

  1497         val mk_import = str o (if qualified

  1498           then prefix "import qualified "

  1499           else prefix "import ") o suffix ";";

  1500         fun import_include (name, _) = str ("import " ^ name ^ ";");

  1501         val content = Pretty.chunks (

  1502             map mk_import imports'

  1503             @ map import_include includes

  1504             @ str ""

  1505             :: separate (str "") (map_filter

  1506               (fn (name, (_, SOME def)) => SOME (seri_def qualified (name, def))

  1507                 | (_, (_, NONE)) => NONE) defs)

  1508           )

  1509       in

  1510         write_module destination (modlname', content)

  1511       end;

  1512   in (

  1513     map (write_module destination) includes;

  1514     Symtab.fold (fn modl => fn () => seri_module modl) code' ()

  1515   ) end;

  1517 fun isar_seri_haskell module file =

  1518   let

  1519     val destination = case file

  1520      of NONE => error ("Haskell: no internal compilation")

  1521       | SOME "-" => NONE

  1522       | SOME file => SOME (Path.explode file)

  1523   in

  1524     parse_args (Scan.option (Args.$$$ "root" -- Args.colon |-- Args.name)

  1525       -- Scan.optional (Args.$$$ "string_classes" >> K true) false

  1526       >> (fn (module_prefix, string_classes) =>

  1527         seri_haskell module_prefix module destination string_classes))

  1528   end;

  1531 (** diagnosis serializer **)

  1533 fun seri_diagnosis labelled_name _ _ _ _ _ _ code =

  1534   let

  1535     val init_names = CodeName.make_vars [];

  1536     fun pr_fun "fun" = SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>

  1537           brackify_infix (1, R) fxy [

  1538             pr_typ (INFX (1, X)) ty1,

  1539             str "->",

  1540             pr_typ (INFX (1, R)) ty2

  1541           ])

  1542       | pr_fun _ = NONE

  1543     val pr = pr_haskell (K NONE) pr_fun (K NONE) labelled_name init_names

  1544       I I (K false) (K false);

  1545   in

  1546     []

  1547     |> Graph.fold (fn (name, (def, _)) =>

  1548           case try pr (name, def) of SOME p => cons p | NONE => I) code

  1549     |> Pretty.chunks2

  1550     |> code_output

  1551     |> PrintMode.setmp [] writeln

  1552   end;

  1556 (** theory data **)

  1558 datatype syntax_expr = SyntaxExpr of {

  1559   class: (string * (string -> string option)) Symtab.table,

  1560   inst: unit Symtab.table,

  1561   tyco: typ_syntax Symtab.table,

  1562   const: term_syntax Symtab.table

  1563 };

  1565 fun mk_syntax_expr ((class, inst), (tyco, const)) =

  1566   SyntaxExpr { class = class, inst = inst, tyco = tyco, const = const };

  1567 fun map_syntax_expr f (SyntaxExpr { class, inst, tyco, const }) =

  1568   mk_syntax_expr (f ((class, inst), (tyco, const)));

  1569 fun merge_syntax_expr (SyntaxExpr { class = class1, inst = inst1, tyco = tyco1, const = const1 },

  1570     SyntaxExpr { class = class2, inst = inst2, tyco = tyco2, const = const2 }) =

  1571   mk_syntax_expr (

  1572     (Symtab.join (K snd) (class1, class2),

  1573        Symtab.join (K snd) (inst1, inst2)),

  1574     (Symtab.join (K snd) (tyco1, tyco2),

  1575        Symtab.join (K snd) (const1, const2))

  1576   );

  1578 type serializer =

  1579   string option

  1580   -> string option

  1581   -> Args.T list

  1582   -> (string -> string)

  1583   -> string list

  1584   -> (string * Pretty.T) list

  1585   -> (string -> string option)

  1586   -> (string -> class_syntax option)

  1587   -> (string -> typ_syntax option)

  1588   -> (string -> term_syntax option)

  1589   -> CodeThingol.code -> unit;

  1591 datatype target = Target of {

  1592   serial: serial,

  1593   serializer: serializer,

  1594   reserved: string list,

  1595   includes: Pretty.T Symtab.table,

  1596   syntax_expr: syntax_expr,

  1597   module_alias: string Symtab.table

  1598 };

  1600 fun mk_target ((serial, serializer), ((reserved, includes), (syntax_expr, module_alias))) =

  1601   Target { serial = serial, serializer = serializer, reserved = reserved,

  1602     includes = includes, syntax_expr = syntax_expr, module_alias = module_alias };

  1603 fun map_target f ( Target { serial, serializer, reserved, includes, syntax_expr, module_alias } ) =

  1604   mk_target (f ((serial, serializer), ((reserved, includes), (syntax_expr, module_alias))));

  1605 fun merge_target target (Target { serial = serial1, serializer = serializer,

  1606   reserved = reserved1, includes = includes1,

  1607   syntax_expr = syntax_expr1, module_alias = module_alias1 },

  1608     Target { serial = serial2, serializer = _,

  1609       reserved = reserved2, includes = includes2,

  1610       syntax_expr = syntax_expr2, module_alias = module_alias2 }) =

  1611   if serial1 = serial2 then

  1612     mk_target ((serial1, serializer),

  1613       ((merge (op =) (reserved1, reserved2), Symtab.merge (op =) (includes1, includes2)),

  1614         (merge_syntax_expr (syntax_expr1, syntax_expr2),

  1615           Symtab.join (K snd) (module_alias1, module_alias2))

  1616     ))

  1617   else

  1618     error ("Incompatible serializers: " ^ quote target);

  1620 structure CodeTargetData = TheoryDataFun

  1621 (

  1622   type T = target Symtab.table * string list;

  1623   val empty = (Symtab.empty, []);

  1624   val copy = I;

  1625   val extend = I;

  1626   fun merge _ ((target1, exc1) : T, (target2, exc2)) =

  1627     (Symtab.join merge_target (target1, target2), Library.merge (op =) (exc1, exc2));

  1628 );

  1630 val target_SML = "SML";

  1631 val target_OCaml = "OCaml";

  1632 val target_Haskell = "Haskell";

  1633 val target_diag = "diag";

  1635 fun the_serializer (Target { serializer, ... }) = serializer;

  1636 fun the_reserved (Target { reserved, ... }) = reserved;

  1637 fun the_includes (Target { includes, ... }) = includes;

  1638 fun the_syntax_expr (Target { syntax_expr = SyntaxExpr x, ... }) = x;

  1639 fun the_module_alias (Target { module_alias , ... }) = module_alias;

  1641 fun assert_serializer thy target =

  1642   case Symtab.lookup (fst (CodeTargetData.get thy)) target

  1643    of SOME data => target

  1644     | NONE => error ("Unknown code target language: " ^ quote target);

  1646 fun add_serializer (target, seri) thy =

  1647   let

  1648     val _ = case Symtab.lookup (fst (CodeTargetData.get thy)) target

  1649      of SOME _ => warning ("overwriting existing serializer " ^ quote target)

  1650       | NONE => ();

  1651   in

  1652     thy

  1653     |> (CodeTargetData.map o apfst oo Symtab.map_default)

  1654           (target, mk_target ((serial (), seri), (([], Symtab.empty),

  1655             (mk_syntax_expr ((Symtab.empty, Symtab.empty), (Symtab.empty, Symtab.empty)),

  1656               Symtab.empty))))

  1657           ((map_target o apfst o apsnd o K) seri)

  1658   end;

  1660 fun map_seri_data target f thy =

  1661   let

  1662     val _ = assert_serializer thy target;

  1663   in

  1664     thy

  1665     |> (CodeTargetData.map o apfst o Symtab.map_entry target o map_target) f

  1666   end;

  1668 fun map_adaptions target =

  1669   map_seri_data target o apsnd o apfst;

  1670 fun map_syntax_exprs target =

  1671   map_seri_data target o apsnd o apsnd o apfst o map_syntax_expr;

  1672 fun map_module_alias target =

  1673   map_seri_data target o apsnd o apsnd o apsnd;

  1675 fun get_serializer thy target permissive module file args

  1676     = fn cs =>

  1677   let

  1678     val (seris, exc) = CodeTargetData.get thy;

  1679     val data = case Symtab.lookup seris target

  1680      of SOME data => data

  1681       | NONE => error ("Unknown code target language: " ^ quote target);

  1682     val seri = the_serializer data;

  1683     val reserved = the_reserved data;

  1684     val includes = Symtab.dest (the_includes data);

  1685     val alias = the_module_alias data;

  1686     val { class, inst, tyco, const } = the_syntax_expr data;

  1687     val project = if target = target_diag then I

  1688       else CodeThingol.project_code permissive

  1689         (Symtab.keys class @ Symtab.keys inst @ Symtab.keys tyco @ Symtab.keys const) cs;

  1690     fun check_empty_funs code = case (filter_out (member (op =) exc)

  1691         (CodeThingol.empty_funs code))

  1692      of [] => code

  1693       | names => error ("No defining equations for "

  1694           ^ commas (map (CodeName.labelled_name thy) names));

  1695   in

  1696     project

  1697     #> check_empty_funs

  1698     #> seri module file args (CodeName.labelled_name thy) reserved includes

  1699         (Symtab.lookup alias) (Symtab.lookup class) (Symtab.lookup tyco) (Symtab.lookup const)

  1700   end;

  1702 fun eval_invoke thy (ref_name, reff) code (t, ty) args =

  1703   let

  1704     val _ = if CodeThingol.contains_dictvar t then

  1705       error "Term to be evaluated constains free dictionaries" else ();

  1706     val val_args = space_implode " "

  1707       (NameSpace.qualifier CodeName.value_name :: map (enclose "(" ")") args);

  1708     val seri = get_serializer thy "SML" false (SOME "Isabelle_Eval") NONE [];

  1709     val code' = CodeThingol.add_value_stmt (t, ty) code;

  1710     val label = "evaluation in SML";

  1711     fun eval () = (seri (SOME [CodeName.value_name]) code';

  1712       ML_Context.evaluate Output.ml_output (!eval_verbose) (ref_name, reff) val_args);

  1713   in NAMED_CRITICAL label eval end;

  1717 (** optional pretty serialization **)

  1719 local

  1721 val pretty : (string * {

  1722     pretty_char: string -> string,

  1723     pretty_string: string -> string,

  1724     pretty_numeral: bool -> int -> string,

  1725     pretty_list: Pretty.T list -> Pretty.T,

  1726     infix_cons: int * string

  1727   }) list = [

  1728   ("SML", { pretty_char = prefix "#" o quote o ML_Syntax.print_char,

  1729       pretty_string = ML_Syntax.print_string,

  1730       pretty_numeral = fn unbounded => fn k =>

  1731         if unbounded then "(" ^ string_of_int k ^ " : IntInf.int)"

  1732         else string_of_int k,

  1733       pretty_list = Pretty.enum "," "[" "]",

  1734       infix_cons = (7, "::")}),

  1735   ("OCaml", { pretty_char = fn c => enclose "'" "'"

  1736         (let val i = ord c

  1737           in if i < 32 orelse i = 39 orelse i = 92

  1738             then prefix "\\" (string_of_int i)

  1739             else c

  1740           end),

  1741       pretty_string = ML_Syntax.print_string,

  1742       pretty_numeral = fn unbounded => fn k => if k >= 0 then

  1743             if unbounded then

  1744               "(Big_int.big_int_of_int " ^ string_of_int k ^ ")"

  1745             else string_of_int k

  1746           else

  1747             if unbounded then

  1748               "(Big_int.big_int_of_int " ^ (enclose "(" ")" o prefix "-"

  1749                 o string_of_int o op ~) k ^ ")"

  1750             else (enclose "(" ")" o prefix "-" o string_of_int o op ~) k,

  1751       pretty_list = Pretty.enum ";" "[" "]",

  1752       infix_cons = (6, "::")}),

  1753   ("Haskell", { pretty_char = fn c => enclose "'" "'"

  1754         (let val i = ord c

  1755           in if i < 32 orelse i = 39 orelse i = 92

  1756             then Library.prefix "\\" (string_of_int i)

  1757             else c

  1758           end),

  1759       pretty_string = ML_Syntax.print_string,

  1760       pretty_numeral = fn unbounded => fn k => if k >= 0 then string_of_int k

  1761           else enclose "(" ")" (signed_string_of_int k),

  1762       pretty_list = Pretty.enum "," "[" "]",

  1763       infix_cons = (5, ":")})

  1764 ];

  1766 in

  1768 fun pr_pretty target = case AList.lookup (op =) pretty target

  1769  of SOME x => x

  1770   | NONE => error ("Unknown code target language: " ^ quote target);

  1772 fun default_list (target_fxy, target_cons) pr fxy t1 t2 =

  1773   brackify_infix (target_fxy, R) fxy [

  1774     pr (INFX (target_fxy, X)) t1,

  1775     str target_cons,

  1776     pr (INFX (target_fxy, R)) t2

  1777   ];

  1779 fun pretty_list c_nil c_cons target =

  1780   let

  1781     val pretty_ops = pr_pretty target;

  1782     val mk_list = #pretty_list pretty_ops;

  1783     fun pretty pr vars fxy [(t1, _), (t2, _)] =

  1784       case Option.map (cons t1) (implode_list c_nil c_cons t2)

  1785        of SOME ts => mk_list (map (pr vars NOBR) ts)

  1786         | NONE => default_list (#infix_cons pretty_ops) (pr vars) fxy t1 t2;

  1787   in (2, pretty) end;

  1789 fun pretty_list_string c_nil c_cons c_char c_nibbles target =

  1790   let

  1791     val pretty_ops = pr_pretty target;

  1792     val mk_list = #pretty_list pretty_ops;

  1793     val mk_char = #pretty_char pretty_ops;

  1794     val mk_string = #pretty_string pretty_ops;

  1795     fun pretty pr vars fxy [(t1, _), (t2, _)] =

  1796       case Option.map (cons t1) (implode_list c_nil c_cons t2)

  1797        of SOME ts => case implode_string c_char c_nibbles mk_char mk_string ts

  1798            of SOME p => p

  1799             | NONE => mk_list (map (pr vars NOBR) ts)

  1800         | NONE => default_list (#infix_cons pretty_ops) (pr vars) fxy t1 t2;

  1801   in (2, pretty) end;

  1803 fun pretty_char c_char c_nibbles target =

  1804   let

  1805     val mk_char = #pretty_char (pr_pretty target);

  1806     fun pretty _ _ _ [(t1, _), (t2, _)] =

  1807       case decode_char c_nibbles (t1, t2)

  1808        of SOME c => (str o mk_char) c

  1809         | NONE => error "Illegal character expression";

  1810   in (2, pretty) end;

  1812 fun pretty_numeral unbounded c_bit0 c_bit1 c_pls c_min c_bit target =

  1813   let

  1814     val mk_numeral = #pretty_numeral (pr_pretty target);

  1815     fun pretty _ _ _ [(t, _)] =

  1816       case implode_numeral c_bit0 c_bit1 c_pls c_min c_bit t

  1817        of SOME k => (str o mk_numeral unbounded) k

  1818         | NONE => error "Illegal numeral expression";

  1819   in (1, pretty) end;

  1821 fun pretty_message c_char c_nibbles c_nil c_cons target =

  1822   let

  1823     val pretty_ops = pr_pretty target;

  1824     val mk_char = #pretty_char pretty_ops;

  1825     val mk_string = #pretty_string pretty_ops;

  1826     fun pretty pr vars fxy [(t, _)] =

  1827       case implode_list c_nil c_cons t

  1828        of SOME ts => (case implode_string c_char c_nibbles mk_char mk_string ts

  1829            of SOME p => p

  1830             | NONE => error "Illegal message expression")

  1831         | NONE => error "Illegal message expression";

  1832   in (1, pretty) end;

  1834 fun pretty_imperative_monad_bind bind' =

  1835   let

  1836     fun dest_abs ((v, ty) `|-> t, _) = ((v, ty), t)

  1837       | dest_abs (t, ty) =

  1838           let

  1839             val vs = CodeThingol.fold_varnames cons t [];

  1840             val v = Name.variant vs "x";

  1841             val ty' = (hd o fst o CodeThingol.unfold_fun) ty;

  1842           in ((v, ty'), t `$ IVar v) end;

  1843     fun tr_bind [(t1, _), (t2, ty2)] =

  1844       let

  1845         val ((v, ty), t) = dest_abs (t2, ty2);

  1846       in ICase (((t1, ty), [(IVar v, tr_bind' t)]), IVar "") end

  1847     and tr_bind' (t as _ `$ _) = (case CodeThingol.unfold_app t

  1848          of (IConst (c, (_, ty1 :: ty2 :: _)), [x1, x2]) => if c = bind'

  1849               then tr_bind [(x1, ty1), (x2, ty2)]

  1850               else t

  1851           | _ => t)

  1852       | tr_bind' t = t;

  1853     fun pretty pr vars fxy ts = pr vars fxy (tr_bind ts);

  1854   in (2, pretty) end;

  1856 fun no_bindings x = (Option.map o apsnd)

  1857   (fn pretty => fn pr => fn vars => pretty (pr vars)) x;

  1859 end; (*local*)

  1861 (** ML and Isar interface **)

  1863 local

  1865 fun cert_class thy class =

  1866   let

  1867     val _ = AxClass.get_info thy class;

  1868   in class end;

  1870 fun read_class thy raw_class =

  1871   let

  1872     val class = Sign.intern_class thy raw_class;

  1873     val _ = AxClass.get_info thy class;

  1874   in class end;

  1876 fun cert_tyco thy tyco =

  1877   let

  1878     val _ = if Sign.declared_tyname thy tyco then ()

  1879       else error ("No such type constructor: " ^ quote tyco);

  1880   in tyco end;

  1882 fun read_tyco thy raw_tyco =

  1883   let

  1884     val tyco = Sign.intern_type thy raw_tyco;

  1885     val _ = if Sign.declared_tyname thy tyco then ()

  1886       else error ("No such type constructor: " ^ quote raw_tyco);

  1887   in tyco end;

  1889 fun gen_add_syntax_class prep_class prep_const target raw_class raw_syn thy =

  1890   let

  1891     val class = prep_class thy raw_class;

  1892     val class' = CodeName.class thy class;

  1893     fun mk_classparam c = case AxClass.class_of_param thy c

  1894      of SOME class'' => if class = class'' then CodeName.const thy c

  1895           else error ("Not a class operation for class " ^ quote class ^ ": " ^ quote c)

  1896       | NONE => error ("Not a class operation: " ^ quote c);

  1897     fun mk_syntax_params raw_params = AList.lookup (op =)

  1898       ((map o apfst) (mk_classparam o prep_const thy) raw_params);

  1899   in case raw_syn

  1900    of SOME (syntax, raw_params) =>

  1901       thy

  1902       |> (map_syntax_exprs target o apfst o apfst)

  1903            (Symtab.update (class', (syntax, mk_syntax_params raw_params)))

  1904     | NONE =>

  1905       thy

  1906       |> (map_syntax_exprs target o apfst o apfst)

  1907            (Symtab.delete_safe class')

  1908   end;

  1910 fun gen_add_syntax_inst prep_class prep_tyco target (raw_tyco, raw_class) add_del thy =

  1911   let

  1912     val inst = CodeName.instance thy (prep_class thy raw_class, prep_tyco thy raw_tyco);

  1913   in if add_del then

  1914     thy

  1915     |> (map_syntax_exprs target o apfst o apsnd)

  1916         (Symtab.update (inst, ()))

  1917   else

  1918     thy

  1919     |> (map_syntax_exprs target o apfst o apsnd)

  1920         (Symtab.delete_safe inst)

  1921   end;

  1923 fun gen_add_syntax_tyco prep_tyco target raw_tyco raw_syn thy =

  1924   let

  1925     val tyco = prep_tyco thy raw_tyco;

  1926     val tyco' = if tyco = "fun" then "fun" else CodeName.tyco thy tyco;

  1927     fun check_args (syntax as (n, _)) = if n <> Sign.arity_number thy tyco

  1928       then error ("Number of arguments mismatch in syntax for type constructor " ^ quote tyco)

  1929       else syntax

  1930   in case raw_syn

  1931    of SOME syntax =>

  1932       thy

  1933       |> (map_syntax_exprs target o apsnd o apfst)

  1934            (Symtab.update (tyco', check_args syntax))

  1935    | NONE =>

  1936       thy

  1937       |> (map_syntax_exprs target o apsnd o apfst)

  1938            (Symtab.delete_safe tyco')

  1939   end;

  1941 fun gen_add_syntax_const prep_const target raw_c raw_syn thy =

  1942   let

  1943     val c = prep_const thy raw_c;

  1944     val c' = CodeName.const thy c;

  1945     fun check_args (syntax as (n, _)) = if n > CodeUnit.no_args thy c

  1946       then error ("Too many arguments in syntax for constant " ^ quote c)

  1947       else syntax;

  1948   in case raw_syn

  1949    of SOME syntax =>

  1950       thy

  1951       |> (map_syntax_exprs target o apsnd o apsnd)

  1952            (Symtab.update (c', check_args syntax))

  1953    | NONE =>

  1954       thy

  1955       |> (map_syntax_exprs target o apsnd o apsnd)

  1956            (Symtab.delete_safe c')

  1957   end;

  1959 fun add_reserved target =

  1960   let

  1961     fun add sym syms = if member (op =) syms sym

  1962       then error ("Reserved symbol " ^ quote sym ^ " already declared")

  1963       else insert (op =) sym syms

  1964   in map_adaptions target o apfst o add end;

  1966 fun add_include target =

  1967   let

  1968     fun add (name, SOME content) incls =

  1969           let

  1970             val _ = if Symtab.defined incls name

  1971               then warning ("Overwriting existing include " ^ name)

  1972               else ();

  1973           in Symtab.update (name, str content) incls end

  1974       | add (name, NONE) incls =

  1975           Symtab.delete name incls;

  1976   in map_adaptions target o apsnd o add end;

  1978 fun add_modl_alias target =

  1979   map_module_alias target o Symtab.update o apsnd CodeName.check_modulename;

  1981 fun add_monad target c_run c_bind thy =

  1982   let

  1983     val c_run' = CodeUnit.read_const thy c_run;

  1984     val c_bind' = CodeUnit.read_const thy c_bind;

  1985     val c_bind'' = CodeName.const thy c_bind';

  1986   in if target = target_Haskell then

  1987     thy

  1988     |> gen_add_syntax_const (K I) target_Haskell c_run'

  1989           (SOME (pretty_haskell_monad c_bind''))

  1990     |> gen_add_syntax_const (K I) target_Haskell c_bind'

  1991           (no_bindings (SOME (parse_infix fst (L, 1) ">>=")))

  1992   else

  1993     thy

  1994     |> gen_add_syntax_const (K I) target c_bind'

  1995           (SOME (pretty_imperative_monad_bind c_bind''))

  1996   end;

  1998 fun gen_allow_exception prep_cs raw_c thy =

  1999   let

  2000     val c = prep_cs thy raw_c;

  2001     val c' = CodeName.const thy c;

  2002   in thy |> (CodeTargetData.map o apsnd) (insert (op =) c') end;

  2004 fun zip_list (x::xs) f g =

  2005   f

  2006   #-> (fn y =>

  2007     fold_map (fn x => g |-- f >> pair x) xs

  2008     #-> (fn xys => pair ((x, y) :: xys)));

  2010 structure P = OuterParse

  2011 and K = OuterKeyword

  2013 fun parse_multi_syntax parse_thing parse_syntax =

  2014   P.and_list1 parse_thing

  2015   #-> (fn things => Scan.repeat1 (P.$$$ "(" |-- P.name --

  2016         (zip_list things parse_syntax (P.$$$ "and")) --| P.$$$ ")"));

  2018 val (infixK, infixlK, infixrK) = ("infix", "infixl", "infixr");

  2020 fun parse_syntax prep_arg xs =

  2021   Scan.option ((

  2022       ((P.$$$ infixK  >> K X)

  2023         || (P.$$$ infixlK >> K L)

  2024         || (P.$$$ infixrK >> K R))

  2025         -- P.nat >> parse_infix prep_arg

  2026       || Scan.succeed (parse_mixfix prep_arg))

  2027       -- P.string

  2028       >> (fn (parse, s) => parse s)) xs;

  2030 in

  2032 val parse_syntax = parse_syntax;

  2034 val add_syntax_class = gen_add_syntax_class cert_class (K I);

  2035 val add_syntax_inst = gen_add_syntax_inst cert_class cert_tyco;

  2036 val add_syntax_tyco = gen_add_syntax_tyco cert_tyco;

  2037 val add_syntax_const = gen_add_syntax_const (K I);

  2038 val allow_exception = gen_allow_exception (K I);

  2040 val add_syntax_class_cmd = gen_add_syntax_class read_class CodeUnit.read_const;

  2041 val add_syntax_inst_cmd = gen_add_syntax_inst read_class read_tyco;

  2042 val add_syntax_tyco_cmd = gen_add_syntax_tyco read_tyco;

  2043 val add_syntax_const_cmd = gen_add_syntax_const CodeUnit.read_const;

  2044 val allow_exception_cmd = gen_allow_exception CodeUnit.read_const;

  2046 fun add_syntax_tycoP target tyco = parse_syntax I >> add_syntax_tyco_cmd target tyco;

  2047 fun add_syntax_constP target c = parse_syntax fst >> (add_syntax_const_cmd target c o no_bindings);

  2049 fun add_undefined target undef target_undefined thy =

  2050   let

  2051     fun pr _ _ _ _ = str target_undefined;

  2052   in

  2053     thy

  2054     |> add_syntax_const target undef (SOME (~1, pr))

  2055   end;

  2057 fun add_pretty_list target nill cons thy =

  2058   let

  2059     val nil' = CodeName.const thy nill;

  2060     val cons' = CodeName.const thy cons;

  2061     val pr = pretty_list nil' cons' target;

  2062   in

  2063     thy

  2064     |> add_syntax_const target cons (SOME pr)

  2065   end;

  2067 fun add_pretty_list_string target nill cons charr nibbles thy =

  2068   let

  2069     val nil' = CodeName.const thy nill;

  2070     val cons' = CodeName.const thy cons;

  2071     val charr' = CodeName.const thy charr;

  2072     val nibbles' = map (CodeName.const thy) nibbles;

  2073     val pr = pretty_list_string nil' cons' charr' nibbles' target;

  2074   in

  2075     thy

  2076     |> add_syntax_const target cons (SOME pr)

  2077   end;

  2079 fun add_pretty_char target charr nibbles thy =

  2080   let

  2081     val charr' = CodeName.const thy charr;

  2082     val nibbles' = map (CodeName.const thy) nibbles;

  2083     val pr = pretty_char charr' nibbles' target;

  2084   in

  2085     thy

  2086     |> add_syntax_const target charr (SOME pr)

  2087   end;

  2089 fun add_pretty_numeral target unbounded number_of b0 b1 pls min bit thy =

  2090   let

  2091     val b0' = CodeName.const thy b0;

  2092     val b1' = CodeName.const thy b1;

  2093     val pls' = CodeName.const thy pls;

  2094     val min' = CodeName.const thy min;

  2095     val bit' = CodeName.const thy bit;

  2096     val pr = pretty_numeral unbounded b0' b1' pls' min' bit' target;

  2097   in

  2098     thy

  2099     |> add_syntax_const target number_of (SOME pr)

  2100   end;

  2102 fun add_pretty_message target charr nibbles nill cons str thy =

  2103   let

  2104     val charr' = CodeName.const thy charr;

  2105     val nibbles' = map (CodeName.const thy) nibbles;

  2106     val nil' = CodeName.const thy nill;

  2107     val cons' = CodeName.const thy cons;

  2108     val pr = pretty_message charr' nibbles' nil' cons' target;

  2109   in

  2110     thy

  2111     |> add_syntax_const target str (SOME pr)

  2112   end;

  2115 val _ = OuterSyntax.keywords [infixK, infixlK, infixrK];

  2117 val _ =

  2118   OuterSyntax.command "code_class" "define code syntax for class" K.thy_decl (

  2119     parse_multi_syntax P.xname

  2120       (Scan.option (P.string -- Scan.optional (P.$$$ "where" |-- Scan.repeat1

  2121         (P.term --| (P.$$$ "\\<equiv>" || P.$$$ "==") -- P.string)) []))

  2122     >> (Toplevel.theory oo fold) (fn (target, syns) =>

  2123           fold (fn (raw_class, syn) => add_syntax_class_cmd target raw_class syn) syns)

  2124   );

  2126 val _ =

  2127   OuterSyntax.command "code_instance" "define code syntax for instance" K.thy_decl (

  2128     parse_multi_syntax (P.xname --| P.$$$ "::" -- P.xname)

  2129       ((P.minus >> K true) || Scan.succeed false)

  2130     >> (Toplevel.theory oo fold) (fn (target, syns) =>

  2131           fold (fn (raw_inst, add_del) => add_syntax_inst_cmd target raw_inst add_del) syns)

  2132   );

  2134 val _ =

  2135   OuterSyntax.command "code_type" "define code syntax for type constructor" K.thy_decl (

  2136     parse_multi_syntax P.xname (parse_syntax I)

  2137     >> (Toplevel.theory oo fold) (fn (target, syns) =>

  2138           fold (fn (raw_tyco, syn) => add_syntax_tyco_cmd target raw_tyco syn) syns)

  2139   );

  2141 val _ =

  2142   OuterSyntax.command "code_const" "define code syntax for constant" K.thy_decl (

  2143     parse_multi_syntax P.term (parse_syntax fst)

  2144     >> (Toplevel.theory oo fold) (fn (target, syns) =>

  2145           fold (fn (raw_const, syn) => add_syntax_const_cmd target raw_const (no_bindings syn)) syns)

  2146   );

  2148 val _ =

  2149   OuterSyntax.command "code_monad" "define code syntax for monads" K.thy_decl (

  2150     P.term -- P.term -- Scan.repeat1 P.name

  2151     >> (fn ((raw_run, raw_bind), targets) => Toplevel.theory

  2152           (fold (fn target => add_monad target raw_run raw_bind) targets))

  2153   );

  2155 val _ =

  2156   OuterSyntax.command "code_reserved" "declare words as reserved for target language" K.thy_decl (

  2157     P.name -- Scan.repeat1 P.name

  2158     >> (fn (target, reserveds) => (Toplevel.theory o fold (add_reserved target)) reserveds)

  2159   );

  2161 val _ =

  2162   OuterSyntax.command "code_include" "declare piece of code to be included in generated code" K.thy_decl (

  2163     P.name -- P.name -- (P.text >> (fn "-" => NONE | s => SOME s))

  2164     >> (fn ((target, name), content) => (Toplevel.theory o add_include target)

  2165       (name, content))

  2166   );

  2168 val _ =

  2169   OuterSyntax.command "code_modulename" "alias module to other name" K.thy_decl (

  2170     P.name -- Scan.repeat1 (P.name -- P.name)

  2171     >> (fn (target, modlnames) => (Toplevel.theory o fold (add_modl_alias target)) modlnames)

  2172   );

  2174 val _ =

  2175   OuterSyntax.command "code_exception" "permit exceptions for constant" K.thy_decl (

  2176     Scan.repeat1 P.term >> (Toplevel.theory o fold allow_exception_cmd)

  2177   );

  2180 (*including serializer defaults*)

  2181 val setup =

  2182   add_serializer (target_SML, isar_seri_sml)

  2183   #> add_serializer (target_OCaml, isar_seri_ocaml)

  2184   #> add_serializer (target_Haskell, isar_seri_haskell)

  2185   #> add_serializer (target_diag, fn _ => fn _=> fn _ => seri_diagnosis)

  2186   #> add_syntax_tyco "SML" "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>

  2187       (gen_brackify (case fxy of NOBR => false | _ => eval_fxy (INFX (1, R)) fxy) o Pretty.breaks) [

  2188         pr_typ (INFX (1, X)) ty1,

  2189         str "->",

  2190         pr_typ (INFX (1, R)) ty2

  2191       ]))

  2192   #> add_syntax_tyco "OCaml" "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>

  2193       (gen_brackify (case fxy of NOBR => false | _ => eval_fxy (INFX (1, R)) fxy) o Pretty.breaks) [

  2194         pr_typ (INFX (1, X)) ty1,

  2195         str "->",

  2196         pr_typ (INFX (1, R)) ty2

  2197       ]))

  2198   #> add_syntax_tyco "Haskell" "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>

  2199       brackify_infix (1, R) fxy [

  2200         pr_typ (INFX (1, X)) ty1,

  2201         str "->",

  2202         pr_typ (INFX (1, R)) ty2

  2203       ]))

  2204   #> fold (add_reserved "SML") ML_Syntax.reserved_names

  2205   #> fold (add_reserved "SML")

  2206       ["o" (*dictionary projections use it already*), "Fail", "div", "mod" (*standard infixes*)]

  2207   #> fold (add_reserved "OCaml") [

  2208       "and", "as", "assert", "begin", "class",

  2209       "constraint", "do", "done", "downto", "else", "end", "exception",

  2210       "external", "false", "for", "fun", "function", "functor", "if",

  2211       "in", "include", "inherit", "initializer", "lazy", "let", "match", "method",

  2212       "module", "mutable", "new", "object", "of", "open", "or", "private", "rec",

  2213       "sig", "struct", "then", "to", "true", "try", "type", "val",

  2214       "virtual", "when", "while", "with"

  2215     ]

  2216   #> fold (add_reserved "OCaml") ["failwith", "mod"]

  2217   #> fold (add_reserved "Haskell") [

  2218       "hiding", "deriving", "where", "case", "of", "infix", "infixl", "infixr",

  2219       "import", "default", "forall", "let", "in", "class", "qualified", "data",

  2220       "newtype", "instance", "if", "then", "else", "type", "as", "do", "module"

  2221     ]

  2222   #> fold (add_reserved "Haskell") [

  2223       "Prelude", "Main", "Bool", "Maybe", "Either", "Ordering", "Char", "String", "Int",

  2224       "Integer", "Float", "Double", "Rational", "IO", "Eq", "Ord", "Enum", "Bounded",

  2225       "Num", "Real", "Integral", "Fractional", "Floating", "RealFloat", "Monad", "Functor",

  2226       "AlreadyExists", "ArithException", "ArrayException", "AssertionFailed", "AsyncException",

  2227       "BlockedOnDeadMVar", "Deadlock", "Denormal", "DivideByZero", "DotNetException", "DynException",

  2228       "Dynamic", "EOF", "EQ", "EmptyRec", "ErrorCall", "ExitException", "ExitFailure",

  2229       "ExitSuccess", "False", "GT", "HeapOverflow",

  2230       "IOError", "IOException", "IllegalOperation",

  2231       "IndexOutOfBounds", "Just", "Key", "LT", "Left", "LossOfPrecision", "NoMethodError",

  2232       "NoSuchThing", "NonTermination", "Nothing", "Obj", "OtherError", "Overflow",

  2233       "PatternMatchFail", "PermissionDenied", "ProtocolError", "RecConError", "RecSelError",

  2234       "RecUpdError", "ResourceBusy", "ResourceExhausted", "Right", "StackOverflow",

  2235       "ThreadKilled", "True", "TyCon", "TypeRep", "UndefinedElement", "Underflow",

  2236       "UnsupportedOperation", "UserError", "abs", "absReal", "acos", "acosh", "all",

  2237       "and", "any", "appendFile", "asTypeOf", "asciiTab", "asin", "asinh", "atan",

  2238       "atan2", "atanh", "basicIORun", "blockIO", "boundedEnumFrom", "boundedEnumFromThen",

  2239       "boundedEnumFromThenTo", "boundedEnumFromTo", "boundedPred", "boundedSucc", "break",

  2240       "catch", "catchException", "ceiling", "compare", "concat", "concatMap", "const",

  2241       "cos", "cosh", "curry", "cycle", "decodeFloat", "denominator", "div", "divMod",

  2242       "doubleToRatio", "doubleToRational", "drop", "dropWhile", "either", "elem",

  2243       "emptyRec", "encodeFloat", "enumFrom", "enumFromThen", "enumFromThenTo",

  2244       "enumFromTo", "error", "even", "exp", "exponent", "fail", "filter", "flip",

  2245       "floatDigits", "floatProperFraction", "floatRadix", "floatRange", "floatToRational",

  2246       "floor", "fmap", "foldl", "foldl'", "foldl1", "foldr", "foldr1", "fromDouble",

  2247       "fromEnum", "fromEnum_0", "fromInt", "fromInteger", "fromIntegral", "fromObj",

  2248       "fromRational", "fst", "gcd", "getChar", "getContents", "getLine", "head",

  2249       "id", "inRange", "index", "init", "intToRatio", "interact", "ioError", "isAlpha",

  2250       "isAlphaNum", "isDenormalized", "isDigit", "isHexDigit", "isIEEE", "isInfinite",

  2251       "isLower", "isNaN", "isNegativeZero", "isOctDigit", "isSpace", "isUpper", "iterate", "iterate'",

  2252       "last", "lcm", "length", "lex", "lexDigits", "lexLitChar", "lexmatch", "lines", "log",

  2253       "logBase", "lookup", "loop", "map", "mapM", "mapM_", "max", "maxBound", "maximum",

  2254       "maybe", "min", "minBound", "minimum", "mod", "negate", "nonnull", "not", "notElem",

  2255       "null", "numerator", "numericEnumFrom", "numericEnumFromThen", "numericEnumFromThenTo",

  2256       "numericEnumFromTo", "odd", "or", "otherwise", "pi", "pred",

  2257       "print", "product", "properFraction", "protectEsc", "putChar", "putStr", "putStrLn",

  2258       "quot", "quotRem", "range", "rangeSize", "rationalToDouble", "rationalToFloat",

  2259       "rationalToRealFloat", "read", "readDec", "readField", "readFieldName", "readFile",

  2260       "readFloat", "readHex", "readIO", "readInt", "readList", "readLitChar", "readLn",

  2261       "readOct", "readParen", "readSigned", "reads", "readsPrec", "realFloatToRational",

  2262       "realToFrac", "recip", "reduce", "rem", "repeat", "replicate", "return", "reverse",

  2263       "round", "scaleFloat", "scanl", "scanl1", "scanr", "scanr1", "seq", "sequence",

  2264       "sequence_", "show", "showChar", "showException", "showField", "showList",

  2265       "showLitChar", "showParen", "showString", "shows", "showsPrec", "significand",

  2266       "signum", "signumReal", "sin", "sinh", "snd", "span", "splitAt", "sqrt", "subtract",

  2267       "succ", "sum", "tail", "take", "takeWhile", "takeWhile1", "tan", "tanh", "threadToIOResult",

  2268       "throw", "toEnum", "toInt", "toInteger", "toObj", "toRational", "truncate", "uncurry",

  2269       "undefined", "unlines", "unsafeCoerce", "unsafeIndex", "unsafeRangeSize", "until", "unwords",

  2270       "unzip", "unzip3", "userError", "words", "writeFile", "zip", "zip3", "zipWith", "zipWith3"

  2271     ] (*due to weird handling of ':', we can't do anything else than to import *all* prelude symbols*);

  2273 end; (*local*)

  2275 end; (*struct*)

author	haftmann
	Wed, 05 Dec 2007 14:16:05 +0100
changeset 25538	58e8ba3b792b
parent 25204	36cf92f63a44
child 25621	97ebdbdb0299
permissions	-rw-r--r--