wneuper/isa: src/Pure/Tools/codegen_serializer.ML@19d9b78218fd

     1 (*  Title:      Pure/Tools/codegen_serializer.ML

     2     ID:         $Id$

     3     Author:     Florian Haftmann, TU Muenchen

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

     6 target languages (like SML or Haskell).

     7 *)

     9 signature CODEGEN_SERIALIZER =

    10 sig

    11   include BASIC_CODEGEN_THINGOL;

    13   val add_pretty_list: string -> string -> string -> (Pretty.T list -> Pretty.T)

    14    -> ((string -> string) * (string -> string)) option -> int * string

    15    -> theory -> theory;

    16   val add_pretty_ml_string: string -> string -> string -> string

    17    -> (string -> string) -> (string -> string) -> string -> theory -> theory;

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

    20   type serializer;

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

    22   val ml_from_thingol: serializer;

    23   val hs_from_thingol: serializer;

    24   val get_serializer: theory -> string * Args.T list

    25     -> string list option -> CodegenThingol.code -> unit;

    27   val const_has_serialization: theory -> string list -> string -> bool;

    28   val tyco_has_serialization: theory -> string list -> string -> bool;

    30   val eval_verbose: bool ref;

    31   val eval_term: theory ->

    32     (string * 'a option ref) * CodegenThingol.iterm -> CodegenThingol.code

    33     -> 'a;

    34 end;

    36 structure CodegenSerializer: CODEGEN_SERIALIZER =

    37 struct

    39 open BasicCodegenThingol;

    40 val tracing = CodegenThingol.tracing;

    42 (** syntax **)

    44 (* basics *)

    46 datatype lrx = L | R | X;

    48 datatype fixity =

    49     BR

    50   | NOBR

    51   | INFX of (int * lrx);

    53 type 'a pretty_syntax = int * (fixity -> (fixity -> 'a -> Pretty.T)

    54   -> 'a list -> Pretty.T);

    56 fun eval_lrx L L = false

    57   | eval_lrx R R = false

    58   | eval_lrx _ _ = true;

    60 fun eval_fxy NOBR _ = false

    61   | eval_fxy _ BR = true

    62   | eval_fxy _ NOBR = false

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

    64       pr < pr_ctxt

    65       orelse pr = pr_ctxt

    66         andalso eval_lrx lr lr_ctxt

    67   | eval_fxy _ (INFX _) = false;

    69 fun gen_brackify _ [p] = p

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

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

    73 fun brackify fxy_ctxt ps =

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

    76 fun brackify_infix infx fxy_ctxt ps =

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

    79 fun mk_app mk_app' from_expr const_syntax fxy (const as (c, (_, ty)), es) =

    80   case const_syntax c

    81    of NONE => brackify fxy (mk_app' c es)

    82     | SOME (i, pr) =>

    83         let

    84           val k = if i < 0 then (length o fst o CodegenThingol.unfold_fun) ty else i

    85         in if k <= length es

    86           then case chop i es of (es1, es2) =>

    87             brackify fxy (pr fxy from_expr es1 :: map (from_expr BR) es2)

    88           else from_expr fxy (CodegenThingol.eta_expand (const, es) i)

    89         end;

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

    94 (* user-defined syntax *)

    96 val str = setmp print_mode [] Pretty.str;

    98 val (atomK, infixK, infixlK, infixrK) =

    99   ("target_atom", "infix", "infixl", "infixr");

   100 val _ = OuterSyntax.add_keywords [atomK, infixK, infixlK, infixrK];

   102 datatype 'a mixfix =

   103     Arg of fixity

   104   | Pretty of Pretty.T;

   106 fun fillin_mixfix fxy_this ms fxy_ctxt pr args =

   107   let

   108     fun fillin [] [] =

   109           []

   110       | fillin (Arg fxy :: ms) (a :: args) =

   111           pr fxy a :: fillin ms args

   112       | fillin (Pretty p :: ms) args =

   113           p :: fillin ms args

   114       | fillin [] _ =

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

   116       | fillin _ [] =

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

   118   in gen_brackify (eval_fxy fxy_this fxy_ctxt) (fillin ms args) end;

   120 fun parse_infix (fixity as INFX (i, x)) s =

   121   let

   122     val l = case x of L => fixity

   123                     | _ => INFX (i, X);

   124     val r = case x of R => fixity

   125                     | _ => INFX (i, X);

   126   in

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

   128   end;

   130 fun parse_mixfix s =

   131   let

   132     val sym_any = Scan.one Symbol.not_eof;

   133     val parse = Scan.repeat (

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

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

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

   137       || (Scan.repeat1

   138            (   $$ "'" |-- sym_any

   139             || Scan.unless ($$ "_" || $$ "/")

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

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

   142    of (p, []) => p

   143     | _ => error ("Malformed mixfix annotation: " ^ quote s)

   144   end;

   146 fun parse_syntax num_args =

   147   let

   148     fun is_arg (Arg _) = true

   149       | is_arg _ = false;

   150     fun parse_nonatomic s =

   151       case parse_mixfix s

   152        of [Pretty _] =>

   153             error ("Mixfix contains just one pretty element; either declare as "

   154               ^ quote atomK ^ " or consider adding a break")

   155         | x => x;

   156     fun mk fixity mfx ctxt =

   157       let

   158         val i = (length o List.filter is_arg) mfx;

   159         val _ = if i > num_args ctxt then error "Too many arguments in code syntax" else ();

   160       in (i, fillin_mixfix fixity mfx) end;

   161     val parse = (

   162            OuterParse.$$$ infixK  |-- OuterParse.nat

   163             >> (fn i => (parse_infix (INFX (i, X)), INFX (i, X)))

   164         || OuterParse.$$$ infixlK |-- OuterParse.nat

   165             >> (fn i => (parse_infix (INFX (i, L)), INFX (i, L)))

   166         || OuterParse.$$$ infixrK |-- OuterParse.nat

   167             >> (fn i => (parse_infix (INFX (i, R)), INFX (i, R)))

   168         || OuterParse.$$$ atomK |-- pair (parse_mixfix, NOBR)

   169         || pair (parse_nonatomic, BR)

   170       ) -- OuterParse.string >> (fn ((p, fxy), s) => (p s, fxy));

   171   in

   172     parse #-> (fn (mfx, fixity) => pair (mk fixity mfx))

   173   end;

   176 (* list and string serializer *)

   178 fun implode_list c_nil c_cons e =

   179   let

   180     fun dest_cons (IConst (c, _) `$ e1 `$ e2) =

   181           if c = c_cons

   182           then SOME (e1, e2)

   183           else NONE

   184       | dest_cons  _ = NONE;

   185     val (es, e') = CodegenThingol.unfoldr dest_cons e;

   186   in case e'

   187    of IConst (c, _) => if c = c_nil then SOME es else NONE

   188     | _ => NONE

   189   end;

   191 fun implode_string mk_char mk_string es =

   192   if forall (fn IChar _ => true | _ => false) es

   193   then (SOME o str o mk_string o implode o map (fn IChar (c, _) => mk_char c)) es

   194   else NONE;

   196 fun pretty_ml_string c_nil c_cons mk_char mk_string target_implode =

   197   let

   198     fun pretty fxy pr [e] =

   199       case implode_list c_nil c_cons e

   200        of SOME es => (case implode_string mk_char mk_string es

   201            of SOME p => p

   202             | NONE => Pretty.block [str target_implode, Pretty.brk 1, pr BR e])

   203         | NONE => Pretty.block [str target_implode, Pretty.brk 1, pr BR e]

   204   in (1, pretty) end;

   206 fun pretty_list c_nil c_cons mk_list mk_char_string (target_fxy, target_cons) =

   207   let

   208     fun default fxy pr e1 e2 =

   209       brackify_infix (target_fxy, R) fxy [

   210         pr (INFX (target_fxy, X)) e1,

   211         str target_cons,

   212         pr (INFX (target_fxy, R)) e2

   213       ];

   214     fun pretty fxy pr [e1, e2] =

   215       case Option.map (cons e1) (implode_list c_nil c_cons e2)

   216        of SOME es =>

   217             (case mk_char_string

   218              of SOME (mk_char, mk_string) =>

   219                   (case implode_string mk_char mk_string es

   220                    of SOME p => p

   221                     | NONE => mk_list (map (pr NOBR) es))

   222               | NONE => mk_list (map (pr NOBR) es))

   223         | NONE => default fxy pr e1 e2;

   224   in (2, pretty) end;

   227 (* variable name contexts *)

   229 (*FIXME could name.ML do th whole job?*)

   230 fun make_vars names = (fold (fn name => Symtab.update_new (name, name)) names Symtab.empty,

   231   Name.make_context names);

   233 fun intro_vars names (namemap, namectxt) =

   234   let

   235     val (names', namectxt') = Name.variants names namectxt;

   236     val namemap' = fold2 (curry Symtab.update) names names' namemap;

   237   in (namemap', namectxt') end;

   239 fun lookup_var (namemap, _) name = case Symtab.lookup namemap name

   240  of SOME name' => name'

   241   | NONE => error ("invalid name in context: " ^ quote name);

   243 fun constructive_fun (name, (eqs, ty)) =

   244   let

   245     val is_cons = CodegenNames.has_nsp CodegenNames.nsp_dtco;

   246     fun is_pat (IConst (c, _)) = is_cons c

   247       | is_pat (IVar _) = true

   248       | is_pat (t1 `$ t2) =

   249           is_pat t1 andalso is_pat t2

   250       | is_pat (INum _) = true

   251       | is_pat (IChar _) = true

   252       | is_pat _ = false;

   253     fun check_eq (eq as (lhs, rhs)) =

   254       if forall is_pat lhs

   255       then SOME eq

   256       else (warning ("In function " ^ quote name ^ ", throwing away one "

   257         ^ "non-executable function clause"); NONE)

   258   in case map_filter check_eq eqs

   259    of [] => error ("In function " ^ quote name ^ ", no "

   260         ^ "executable function clauses found")

   261     | eqs => (name, (eqs, ty))

   262   end;

   265 (** SML serializer **)

   267 datatype ml_def =

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

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

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

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

   272         * ((class * (string * inst list list)) list

   273       * (string * iterm) list));

   275 fun pr_sml_def tyco_syntax const_syntax keyword_vars deresolv ml_def =

   276   let

   277     val is_cons = CodegenNames.has_nsp CodegenNames.nsp_dtco;

   278     fun dictvar v =

   279       first_upper v ^ "_";

   280     val label = translate_string (fn "." => "__" | c => c)

   281       o NameSpace.pack o op @ o apsnd single o apfst (fst o split_last) o split_last o NameSpace.unpack;

   282     fun pr_tyvar (v, []) =

   283           str "()"

   284       | pr_tyvar (v, sort) =

   285           let

   286             fun pr_class class =

   287               str ("'" ^ v ^ " " ^ deresolv class);

   288           in

   289             Pretty.block [

   290               str "(",

   291               (str o dictvar) v,

   292               str ":",

   293               case sort

   294                of [class] => pr_class class

   295                 | _ => Pretty.enum " *" "" "" (map pr_class sort),

   296               str ")"

   297             ]

   298           end;

   299     fun pr_insts fxy iys =

   300       let

   301         fun pr_proj s = str ("#" ^ s);

   302         fun pr_lookup [] p =

   303               p

   304           | pr_lookup [p'] p =

   305               brackify BR [p', p]

   306           | pr_lookup (ps as _ :: _) p =

   307               brackify BR [Pretty.enum " o" "(" ")" ps, p];

   308         fun pr_inst fxy (Instance (inst, iss)) =

   309               brackify fxy (

   310                 (str o deresolv) inst

   311                 :: map (pr_insts BR) iss

   312               )

   313           | pr_inst fxy (Context (classes, (v, i))) =

   314               pr_lookup (map (pr_proj o label) classes

   315                 @ (if i = ~1 then [] else [(pr_proj o string_of_int) (i+1)])

   316               ) ((str o dictvar) v);

   317       in case iys

   318        of [] => str "()"

   319         | [iy] => pr_inst fxy iy

   320         | _ :: _ => (Pretty.list "(" ")" o map (pr_inst NOBR)) iys

   321       end;

   322     fun pr_tycoexpr fxy (tyco, tys) =

   323       let

   324         val tyco' = (str o deresolv) tyco

   325       in case map (pr_typ BR) tys

   326        of [] => tyco'

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

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

   329       end

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

   331           (case tyco_syntax tyco

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

   333             | SOME (i, pr) =>

   334                 if not (i = length tys)

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

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

   337                   ^ string_of_int i ^ " expected")

   338                 else pr fxy pr_typ tys)

   339       | pr_typ fxy (t1 `-> t2) =

   340           (gen_brackify (case fxy of BR => false | _ => eval_fxy (INFX (1, R)) fxy)

   341             o Pretty.breaks) [

   342               pr_typ (INFX (1, X)) t1,

   343               str "->",

   344               pr_typ (INFX (1, R)) t2

   345             ]

   346       | pr_typ fxy (ITyVar v) =

   347           str ("'" ^ v);

   348     fun pr_term vars fxy (IConst c) =

   349           pr_app vars fxy (c, [])

   350       | pr_term vars fxy (IVar v) =

   351           str (lookup_var vars v)

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

   353           (case CodegenThingol.unfold_const_app t

   354            of SOME c_ts => pr_app vars fxy c_ts

   355             | NONE =>

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

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

   358           let

   359             val (ts, t') = CodegenThingol.unfold_abs t;

   360             val vs = fold (CodegenThingol.fold_varnames (insert (op =)) o fst) ts [];

   361             val vars' = intro_vars vs vars;

   362             fun mk_abs (t, ty) = (Pretty.block o Pretty.breaks)

   363               [str "fn", pr_term vars' NOBR t, str "=>"];

   364           in brackify BR (map mk_abs ts @ [pr_term vars' NOBR t']) end

   365       | pr_term vars fxy (INum (n, _)) =

   366           brackify BR [(str o IntInf.toString) n, str ":", str "IntInf.int"]

   367       | pr_term vars _ (IChar (c, _)) =

   368           (str o prefix "#" o quote)

   369             (let val i = ord c

   370               in if i < 32

   371                 then prefix "\\" (string_of_int i)

   372                 else c

   373               end)

   374       | pr_term vars fxy (t as ICase ((_, [_]), _)) =

   375           let

   376             val (ts, t) = CodegenThingol.unfold_let t;

   377             fun mk ((p, _), t) vars =

   378               let

   379                 val vs = CodegenThingol.fold_varnames (insert (op =)) p [];

   380                 val vars' = intro_vars vs vars;

   381               in

   382                 (Pretty.block [

   383                   (Pretty.block o Pretty.breaks) [

   384                     str "val",

   385                     pr_term vars' NOBR p,

   386                     str "=",

   387                     pr_term vars NOBR t

   388                   ],

   389                   str ";"

   390                 ], vars')

   391               end

   392             val (binds, vars') = fold_map mk ts vars;

   393           in

   394             Pretty.chunks [

   395               [str ("let"), Pretty.fbrk, binds |> Pretty.chunks] |> Pretty.block,

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

   397               str ("end")

   398             ] end

   399       | pr_term vars fxy (ICase (((td, ty), b::bs), _)) =

   400           let

   401             fun pr definer (p, t) =

   402               let

   403                 val vs = CodegenThingol.fold_varnames (insert (op =)) p [];

   404                 val vars' = intro_vars vs vars;

   405               in

   406                 (Pretty.block o Pretty.breaks) [

   407                   str definer,

   408                   pr_term vars' NOBR p,

   409                   str "=>",

   410                   pr_term vars' NOBR t

   411                 ]

   412               end;

   413           in

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

   415               str "case"

   416               :: pr_term vars NOBR td

   417               :: pr "of" b

   418               :: map (pr "|") bs

   419             )

   420           end

   421     and pr_app' vars c ts =

   422       let

   423         val p = (str o deresolv) c;

   424         val ps = map (pr_term vars BR) ts;

   425       in if is_cons c andalso length ts > 1 then

   426         [p, Pretty.enum "," "(" ")" ps]

   427       else

   428         p :: ps

   429       end

   430     and pr_app vars fxy (app as ((c, (iss, ty)), ts)) =

   431       case if is_cons c then [] else (map (pr_insts BR) o filter_out null) iss

   432        of [] =>

   433             mk_app (pr_app' vars) (pr_term vars) const_syntax fxy app

   434         | ps =>

   435             if (is_none o const_syntax) c then

   436               brackify fxy ((str o deresolv) c :: (ps @ map (pr_term vars BR) ts))

   437             else

   438               error ("Cannot apply user defined serialization for function expecting dictionaries: " ^ quote c)

   439     fun eta_expand_poly_fun (funn as (_, (_::_, _))) =

   440           funn

   441       | eta_expand_poly_fun (funn as (_, ([_], ([], _)))) =

   442           funn

   443       | eta_expand_poly_fun (funn as (_, ([(_::_, _)], _))) =

   444           funn

   445       | eta_expand_poly_fun (funn as (_, ([(_, _ `|-> _)], _))) =

   446           funn

   447       | eta_expand_poly_fun (funn as (name, ([([], t)], tysm as (vs, ty)))) =

   448           if (null o fst o CodegenThingol.unfold_fun) ty

   449               orelse (not o null o filter_out (null o snd)) vs

   450             then funn

   451             else (name, ([([IVar "x"], t `$ IVar "x")], tysm));

   452     fun pr_def (MLFuns raw_funns) =

   453           let

   454             val funns as (funn :: funns') = map (eta_expand_poly_fun o constructive_fun) raw_funns;

   455             val definer =

   456               let

   457                 fun mk [] [] = "val"

   458                   | mk (_::_) _ = "fun"

   459                   | mk [] vs = if (null o filter_out (null o snd)) vs then "val" else "fun";

   460                 fun chk (_, ((ts, _) :: _, (vs, _))) NONE = SOME (mk ts vs)

   461                   | chk (_, ((ts, _) :: _, (vs, _))) (SOME defi) =

   462                       if defi = mk ts vs then SOME defi

   463                       else error ("Mixing simultaneous vals and funs not implemented");

   464               in the (fold chk funns NONE) end;

   465             fun pr_funn definer (name, (eqs as eq::eqs', (raw_vs, ty))) =

   466               let

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

   468                 val shift = if null eqs' then I else

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

   470                 fun pr_eq definer (ts, t) =

   471                   let

   472                     val consts = map_filter

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

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

   475                         ((fold o CodegenThingol.fold_constnames) (insert (op =)) (t :: ts) []);

   476                     val vars = keyword_vars

   477                       |> intro_vars consts

   478                       |> intro_vars ((fold o CodegenThingol.fold_unbound_varnames) (insert (op =)) (t :: ts) []);

   479                   in

   480                     (Pretty.block o Pretty.breaks) (

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

   482                       @ (if null ts andalso null vs

   483                            andalso not (ty = ITyVar "_")(*for evaluation*)

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

   485                          else

   486                            map pr_tyvar vs

   487                            @ map (pr_term vars BR) ts)

   488                    @ [str "=", pr_term vars NOBR t]

   489                     )

   490                   end

   491               in

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

   493                   pr_eq definer eq

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

   495                 )

   496               end;

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

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

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

   500           let

   501             fun pr_co (co, []) =

   502                   str (deresolv co)

   503               | pr_co (co, tys) =

   504                   (Pretty.block o Pretty.breaks) [

   505                     str (deresolv co),

   506                     str "of",

   507                     Pretty.enum " *" "" "" (map (pr_typ (INFX (2, L))) tys)

   508                   ];

   509             fun pr_data definer (tyco, (vs, cos)) =

   510               (Pretty.block o Pretty.breaks) (

   511                 str definer

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

   513                 :: str "="

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

   515               );

   516             val (ps, p) = split_last (pr_data "datatype" data :: map (pr_data "and") datas');

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

   518      | pr_def (MLClass (class, (superclasses, (v, classops)))) =

   519           let

   520             val w = dictvar v;

   521             fun pr_superclass class =

   522               (Pretty.block o Pretty.breaks o map str) [

   523                 label class, ":", "'" ^ v, deresolv class

   524               ];

   525             fun pr_classop (classop, ty) =

   526               (Pretty.block o Pretty.breaks) [

   527                 (str o suffix "_" o NameSpace.base) classop, str ":", pr_typ NOBR ty

   528               ];

   529             fun pr_classop_fun (classop, _) =

   530               (Pretty.block o Pretty.breaks) [

   531                 str "fun",

   532                 (str o deresolv) classop,

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

   534                 str "=",

   535                 str ("#" ^ (suffix "_" o NameSpace.base) classop),

   536                 str (w ^ ";")

   537               ];

   538           in

   539             Pretty.chunks (

   540               (Pretty.block o Pretty.breaks) [

   541                 str ("type '" ^ v),

   542                 (str o deresolv) class,

   543                 str "=",

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

   545                   map pr_superclass superclasses @ map pr_classop classops

   546                 )

   547               ]

   548               :: map pr_classop_fun classops

   549             )

   550           end

   551      | pr_def (MLClassinst (inst, ((class, (tyco, arity)), (superarities, classop_defs)))) =

   552           let

   553             fun pr_superclass (superclass, superinst_iss) =

   554               (Pretty.block o Pretty.breaks) [

   555                 (str o label) superclass,

   556                 str "=",

   557                 pr_insts NOBR [Instance superinst_iss]

   558               ];

   559             fun pr_classop_def (classop, t) =

   560               let

   561                 val consts = map_filter

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

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

   564                     (CodegenThingol.fold_constnames (insert (op =)) t []);

   565                 val vars = keyword_vars

   566                   |> intro_vars consts;

   567               in

   568                 (Pretty.block o Pretty.breaks) [

   569                   (str o suffix "_" o NameSpace.base) classop,

   570                   str "=",

   571                   pr_term vars NOBR t

   572                 ]

   573               end;

   574           in

   575             (Pretty.block o Pretty.breaks) ([

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

   577               (str o deresolv) inst ] @

   578               map pr_tyvar arity @ [

   579               str "=",

   580               Pretty.enum "," "{" "}" (map pr_superclass superarities @ map pr_classop_def classop_defs),

   581               str ":",

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

   583             ])

   584           end;

   585   in pr_def ml_def end;

   589 (** Haskell serializer **)

   591 fun pr_haskell class_syntax tyco_syntax const_syntax keyword_vars deresolv_here deresolv def =

   592   let

   593     val is_cons = CodegenNames.has_nsp CodegenNames.nsp_dtco;

   594     fun class_name class = case class_syntax class

   595      of NONE => deresolv class

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

   597     fun classop_name class classop = case class_syntax class

   598      of NONE => NameSpace.base classop

   599       | SOME (_, classop_syntax) => case classop_syntax classop

   600          of NONE => NameSpace.base classop

   601           | SOME classop => classop

   602     fun pr_typparms tyvars vs =

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

   604        of [] => str ""

   605         | xs => Pretty.block [

   606             Pretty.enum "," "(" ")" (

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

   608                 (class_name class ^ " " ^ lookup_var tyvars v)) xs

   609             ),

   610             str " => "

   611           ];

   612     fun pr_tycoexpr tyvars fxy (tyco, tys) =

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

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

   615           (case tyco_syntax tyco

   616            of NONE =>

   617                 pr_tycoexpr tyvars fxy (deresolv tyco, tys)

   618             | SOME (i, pr) =>

   619                 if not (i = length tys)

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

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

   622                   ^ string_of_int i ^ " expected")

   623                 else pr fxy (pr_typ tyvars) tys)

   624       | pr_typ tyvars fxy (t1 `-> t2) =

   625           brackify_infix (1, R) fxy [

   626             pr_typ tyvars (INFX (1, X)) t1,

   627             str "->",

   628             pr_typ tyvars (INFX (1, R)) t2

   629           ]

   630       | pr_typ tyvars fxy (ITyVar v) =

   631           (str o lookup_var tyvars) v;

   632     fun pr_typscheme_expr tyvars (vs, tycoexpr) =

   633       Pretty.block [pr_typparms tyvars vs, pr_tycoexpr tyvars NOBR tycoexpr];

   634     fun pr_typscheme tyvars (vs, ty) =

   635       Pretty.block [pr_typparms tyvars vs, pr_typ tyvars NOBR ty];

   636     fun pr_term vars fxy (IConst c) =

   637           pr_app vars fxy (c, [])

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

   639           (case CodegenThingol.unfold_const_app t

   640            of SOME app => pr_app vars fxy app

   641             | _ =>

   642                 brackify fxy [

   643                   pr_term vars NOBR t1,

   644                   pr_term vars BR t2

   645                 ])

   646       | pr_term vars fxy (IVar v) =

   647           (str o lookup_var vars) v

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

   649           let

   650             val (ts, t') = CodegenThingol.unfold_abs t;

   651             val vs = fold (CodegenThingol.fold_varnames (insert (op =)) o fst) ts [];

   652             val vars' = intro_vars vs vars;

   653           in

   654             brackify BR (

   655               str "\\"

   656               :: map (pr_term vars' BR o fst) ts @ [

   657               str "->",

   658               pr_term vars' NOBR t'

   659             ])

   660           end

   661       | pr_term vars fxy (INum (n, _)) =

   662           if n > 0 then

   663             (str o IntInf.toString) n

   664           else

   665             brackify BR [(str o Library.prefix "-" o IntInf.toString o IntInf.~) n]

   666       | pr_term vars fxy (IChar (c, _)) =

   667           (str o enclose "'" "'")

   668             (let val i = (Char.ord o the o Char.fromString) c

   669               in if i < 32

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

   671                 else c

   672               end)

   673       | pr_term vars fxy (t as ICase ((_, [_]), _)) =

   674           let

   675             val (ts, t) = CodegenThingol.unfold_let t;

   676             fun pr ((p, _), t) vars =

   677               let

   678                 val vs = CodegenThingol.fold_varnames (insert (op =)) p [];

   679                 val vars' = intro_vars vs vars;

   680               in

   681                 ((Pretty.block o Pretty.breaks) [

   682                   pr_term vars' BR p,

   683                   str "=",

   684                   pr_term vars NOBR t

   685                 ], vars')

   686               end;

   687             val (binds, vars') = fold_map pr ts vars;

   688           in Pretty.chunks [

   689             [str ("let"), Pretty.fbrk, binds |> Pretty.chunks] |> Pretty.block,

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

   691           ] end

   692       | pr_term vars fxy (ICase (((td, _), bs), _)) =

   693           let

   694             fun pr (p, t) =

   695               let

   696                 val vs = CodegenThingol.fold_varnames (insert (op =)) p [];

   697                 val vars' = intro_vars vs vars;

   698               in

   699                 (Pretty.block o Pretty.breaks) [

   700                   pr_term vars' NOBR p,

   701                   str "->",

   702                   pr_term vars' NOBR t

   703                 ]

   704               end

   705           in

   706             (Pretty.enclose "(" ")" o Pretty.breaks) [

   707               str "case",

   708               pr_term vars NOBR td,

   709               str "of",

   710               (Pretty.chunks o map pr) bs

   711             ]

   712           end

   713     and pr_app' vars c ts =

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

   715     and pr_app vars fxy =

   716       mk_app (pr_app' vars) (pr_term vars) const_syntax fxy;

   717     fun pr_def (name, CodegenThingol.Fun (funn as (eqs, (vs, ty)))) =

   718           let

   719             val tyvars = intro_vars (map fst vs) keyword_vars;

   720             fun pr_eq (ts, t) =

   721               let

   722                 val consts = map_filter

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

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

   725                     ((fold o CodegenThingol.fold_constnames) (insert (op =)) (t :: ts) []);

   726                 val vars = keyword_vars

   727                   |> intro_vars consts

   728                   |> intro_vars ((fold o CodegenThingol.fold_unbound_varnames) (insert (op =)) (t :: ts) []);

   729               in

   730                 (Pretty.block o Pretty.breaks) (

   731                   (str o deresolv_here) name

   732                   :: map (pr_term vars BR) ts

   733                   @ [str "=", pr_term vars NOBR t]

   734                 )

   735               end;

   736           in

   737             Pretty.chunks (

   738               Pretty.block [

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

   740                 Pretty.brk 1,

   741                 pr_typscheme tyvars (vs, ty)

   742               ]

   743               :: (map pr_eq o fst o snd o constructive_fun) (name, funn)

   744             )

   745           end |> SOME

   746       | pr_def (name, CodegenThingol.Datatype (vs, [(co, [ty])])) =

   747           let

   748             val tyvars = intro_vars (map fst vs) keyword_vars;

   749           in

   750             (Pretty.block o Pretty.breaks) [

   751               str "newtype",

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

   753               str "=",

   754               (str o deresolv_here) co,

   755               pr_typ tyvars BR ty

   756             ]

   757           end |> SOME

   758       | pr_def (name, CodegenThingol.Datatype (vs, co :: cos)) =

   759           let

   760             val tyvars = intro_vars (map fst vs) keyword_vars;

   761             fun pr_co (co, tys) =

   762               (Pretty.block o Pretty.breaks) (

   763                 (str o deresolv_here) co

   764                 :: map (pr_typ tyvars BR) tys

   765               )

   766           in

   767             (Pretty.block o Pretty.breaks) (

   768               str "data"

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

   770               :: str "="

   771               :: pr_co co

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

   773             )

   774           end |> SOME

   775       | pr_def (_, CodegenThingol.Datatypecons _) =

   776           NONE

   777       | pr_def (name, CodegenThingol.Class (superclasss, (v, classops))) =

   778           let

   779             val tyvars = intro_vars [v] keyword_vars;

   780             fun pr_classop (classop, ty) =

   781               Pretty.block [

   782                 str (deresolv_here classop ^ " ::"),

   783                 Pretty.brk 1,

   784                 pr_typ tyvars NOBR ty

   785               ]

   786           in

   787             Pretty.block [

   788               str "class ",

   789               pr_typparms tyvars [(v, superclasss)],

   790               str (deresolv_here name ^ " " ^ v),

   791               str " where",

   792               Pretty.fbrk,

   793               Pretty.chunks (map pr_classop classops)

   794             ]

   795           end |> SOME

   796       | pr_def (_, CodegenThingol.Classmember _) =

   797           NONE

   798       | pr_def (_, CodegenThingol.Classinst ((class, (tyco, vs)), (_, classop_defs))) =

   799           let

   800             val tyvars = intro_vars (map fst vs) keyword_vars;

   801           in

   802             Pretty.block [

   803               str "instance ",

   804               pr_typparms tyvars vs,

   805               str (class_name class ^ " "),

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

   807               str " where",

   808               Pretty.fbrk,

   809               Pretty.chunks (map (fn (classop, t) =>

   810                 let

   811                   val consts = map_filter

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

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

   814                       (CodegenThingol.fold_constnames (insert (op =)) t []);

   815                   val vars = keyword_vars

   816                     |> intro_vars consts;

   817                 in

   818                   (Pretty.block o Pretty.breaks) [

   819                     (str o classop_name class) classop,

   820                     str "=",

   821                     pr_term vars NOBR t

   822                   ]

   823                 end

   824               ) classop_defs)

   825             ]

   826           end |> SOME

   827   in Pretty.setmp_margin 999999 pr_def def end;

   830 (** generic abstract serializer **)

   832 structure NameMangler = NameManglerFun (

   833   type ctxt = (string * string -> string) * (string -> string option);

   834   type src = string * string;

   835   val ord = prod_ord string_ord string_ord;

   836   fun mk (postprocess, validate) ((shallow, name), 0) =

   837         let

   838           val name' = postprocess (shallow, name);

   839         in case validate name'

   840          of NONE => name'

   841           | _ => mk (postprocess, validate) ((shallow, name), 1)

   842         end

   843     | mk (postprocess, validate) (("", name), i) =

   844         postprocess ("", name ^ replicate_string i "'")

   845         |> perhaps validate

   846     | mk (postprocess, validate) ((shallow, name), 1) =

   847         postprocess (shallow, shallow ^ "_" ^ name)

   848         |> perhaps validate

   849     | mk (postprocess, validate) ((shallow, name), i) =

   850         postprocess (shallow, name ^ replicate_string i "'")

   851         |> perhaps validate;

   852   fun is_valid _ _ = true;

   853   fun maybe_unique _ _ = NONE;

   854   fun re_mangle _ dst = error ("No such definition name: " ^ quote dst);

   855 );

   857 (*FIXME refactor this properly*)

   858 fun code_serialize seri_defs seri_module validate postprocess nsp_conn name_root

   859     (code : CodegenThingol.code) =

   860   let

   861     datatype node = Def of CodegenThingol.def | Module of node Graph.T;

   862     fun dest_modl (Module m) = m;

   863     fun dest_name name =

   864       let

   865         val (names, name_base) = (split_last o NameSpace.unpack) name;

   866         val (names_mod, name_shallow) = split_last names;

   867       in (names_mod, NameSpace.pack [name_shallow, name_base]) end;

   868     fun mk_deresolver module nsp_conn postprocess validate =

   869       let

   870         datatype tabnode = N of string * tabnode Symtab.table option;

   871         fun mk module manglers tab =

   872           let

   873             fun mk_name name =

   874               case NameSpace.unpack name

   875                of [n] => ("", n)

   876                 | [s, n] => (s, n);

   877             fun in_conn (shallow, conn) =

   878               member (op = : string * string -> bool) conn shallow;

   879             fun add_name name =

   880               let

   881                 val n as (shallow, _) = mk_name name;

   882               in

   883                 AList.map_entry_yield in_conn shallow (

   884                   NameMangler.declare (postprocess, validate) n

   885                   #-> (fn n' => pair (name, n'))

   886                 ) #> apfst the

   887               end;

   888             val (renamings, manglers') =

   889               fold_map add_name (Graph.keys module) manglers;

   890             fun extend_tab (n, n') =

   891               if (length o NameSpace.unpack) n = 1

   892               then

   893                 Symtab.update_new

   894                   (n, N (n', SOME (mk ((dest_modl o Graph.get_node module) n) manglers' Symtab.empty)))

   895               else

   896                 Symtab.update_new (n, N (n', NONE));

   897           in fold extend_tab renamings tab end;

   898         fun get_path_name [] tab =

   899               ([], SOME tab)

   900           | get_path_name [p] tab =

   901               let

   902                 val SOME (N (p', tab')) = Symtab.lookup tab p

   903               in ([p'], tab') end

   904           | get_path_name [p1, p2] tab =

   905               (case Symtab.lookup tab p1

   906                of SOME (N (p', SOME tab')) =>

   907                     let

   908                       val (ps', tab'') = get_path_name [p2] tab'

   909                     in (p' :: ps', tab'') end

   910                 | NONE =>

   911                     let

   912                       val SOME (N (p', NONE)) = Symtab.lookup tab (NameSpace.pack [p1, p2])

   913                     in ([p'], NONE) end)

   914           | get_path_name (p::ps) tab =

   915               let

   916                 val SOME (N (p', SOME tab')) = Symtab.lookup tab p

   917                 val (ps', tab'') = get_path_name ps tab'

   918               in (p' :: ps', tab'') end;

   919         fun deresolv tab prefix name =

   920           let

   921             val (common, (_, rem)) = chop_prefix (op =) (prefix, NameSpace.unpack name);

   922             val (_, SOME tab') = get_path_name common tab;

   923             val (name', _) = get_path_name rem tab';

   924           in NameSpace.pack name' end handle BIND => (error ("Missing name: " ^ quote name ^ ", in " ^ quote (NameSpace.pack prefix)));

   925       in deresolv (mk module (AList.make (K NameMangler.empty) nsp_conn) Symtab.empty) end;

   926     fun allimports_of modl =

   927       let

   928         fun imps_of prfx (Module modl) imps tab =

   929               let

   930                 val this = NameSpace.pack prfx;

   931                 val name_con = (rev o Graph.strong_conn) modl;

   932               in

   933                 tab

   934                 |> pair []

   935                 |> fold (fn names => fn (imps', tab) =>

   936                     tab

   937                     |> fold_map (fn name =>

   938                          imps_of (prfx @ [name]) (Graph.get_node modl name) (imps' @ imps)) names

   939                     |-> (fn imps'' => pair (flat imps'' @ imps'))) name_con

   940                 |-> (fn imps' =>

   941                    Symtab.update_new (this, imps' @ imps)

   942                 #> pair (this :: imps'))

   943               end

   944           | imps_of prfx (Def _) imps tab =

   945               ([], tab);

   946       in snd (imps_of [] (Module modl) [] Symtab.empty) end;

   947     fun add_def ((names_mod, name_id), def) =

   948       let

   949         fun add [] =

   950               Graph.new_node (name_id, Def def)

   951           | add (m::ms) =

   952               Graph.default_node (m, Module Graph.empty)

   953               #> Graph.map_node m (Module o add ms o dest_modl)

   954       in add names_mod end;

   955     fun add_dep (name1, name2) =

   956       if name1 = name2 then I

   957       else

   958         let

   959           val m1 = dest_name name1 |> apsnd single |> (op @);

   960           val m2 = dest_name name2 |> apsnd single |> (op @);

   961           val (ms, (r1, r2)) = chop_prefix (op =) (m1, m2);

   962           val (ms, (s1::r1, s2::r2)) = chop_prefix (op =) (m1, m2);

   963           val add_edge =

   964             if null r1 andalso null r2

   965             then Graph.add_edge

   966             else fn edge => fn gr => (Graph.add_edge_acyclic edge gr

   967               handle Graph.CYCLES _ =>

   968                 error ("Module dependency "

   969                   ^ quote name1 ^ " -> " ^ quote name2 ^ " would result in module dependency cycle"))

   970           fun add [] node =

   971                 node

   972                 |> add_edge (s1, s2)

   973             | add (m::ms) node =

   974                 node

   975                 |> Graph.map_node m (Module o add ms o dest_modl);

   976         in add ms end;

   977     val root_module =

   978       Graph.empty

   979       |> Graph.fold (fn (name, (def, _)) => add_def (dest_name name, def)) code

   980       |> Graph.fold (fn (name, (_, (_, deps))) =>

   981           fold (curry add_dep name) deps) code;

   982     val names = map fst (Graph.dest root_module);

   983     val imptab = allimports_of root_module;

   984     val resolver = mk_deresolver root_module nsp_conn postprocess validate;

   985     fun sresolver s = (resolver o NameSpace.unpack) s

   986     fun mk_name prfx name =

   987       let

   988         val name_qual = NameSpace.pack (prfx @ [name])

   989       in (name_qual, resolver prfx name_qual) end;

   990     fun is_bot (_, (Def Bot)) = true

   991       | is_bot _ = false;

   992     fun mk_contents prfx module =

   993       map_filter (seri prfx)

   994         ((map (AList.make (Graph.get_node module)) o rev o Graph.strong_conn) module)

   995     and seri prfx [(name, Module modl)] =

   996           seri_module (resolver []) (map (resolver []) ((the o Symtab.lookup imptab) (NameSpace.pack (prfx @ [name]))))

   997             (mk_name prfx name, mk_contents (prfx @ [name]) modl)

   998       | seri prfx ds =

   999           seri_defs sresolver (NameSpace.pack prfx)

  1000             (map (fn (name, Def def) => (fst (mk_name prfx name), def)) ds)

  1001   in

  1002     seri_module (resolver []) (map (resolver []) ((the o Symtab.lookup imptab) ""))

  1003       (("", name_root), (mk_contents [] root_module))

  1004   end;

  1006 fun abstract_serializer (target, nspgrp) name_root (from_defs, from_module, validator, postproc)

  1007     postprocess (class_syntax, tyco_syntax, const_syntax)

  1008     (drop, select) code =

  1009   let

  1010     fun project NONE code = code

  1011       | project (SOME names) code =

  1012           let

  1013             fun check name = if member (op =) drop name

  1014               then error ("shadowed definition " ^ quote name ^ " selected for serialization")

  1015               else if can (Graph.get_node code) name

  1016               then ()

  1017               else error ("dropped definition " ^ quote name ^ " selected for serialization")

  1018             val names' = (map o tap) check names;

  1019           in CodegenThingol.project_code names code end;

  1020     fun from_module' resolv imps ((name_qual, name), defs) =

  1021       from_module resolv imps ((name_qual, name), defs)

  1022       |> postprocess (resolv name_qual);

  1023   in

  1024     code

  1025     |> tracing (fn _ => "dropping shadowed definitions...")

  1026     |> CodegenThingol.delete_garbage drop

  1027     |> tracing (fn _ => "projecting...")

  1028     |> project select

  1029     |> tracing (fn _ => "serializing...")

  1030     |> code_serialize (from_defs (class_syntax, tyco_syntax, const_syntax))

  1031          from_module' validator postproc nspgrp name_root

  1032     |> K ()

  1033   end;

  1035 fun abstract_validator keywords name =

  1036   let

  1037     fun replace_invalid c = (*FIXME*)

  1038       if Symbol.is_ascii_letter c orelse Symbol.is_ascii_digit c orelse c = "'"

  1039       andalso not (NameSpace.separator = c)

  1040       then c

  1041       else "_"

  1042     fun suffix_it name=

  1043       name

  1044       |> member (op =) keywords ? suffix "'"

  1045       |> (fn name' => if name = name' then name else suffix_it name')

  1046   in

  1047     name

  1048     |> translate_string replace_invalid

  1049     |> suffix_it

  1050     |> (fn name' => if name = name' then NONE else SOME name')

  1051   end;

  1053 fun write_file mkdir path p = (

  1054     if mkdir

  1055       then

  1056         File.mkdir (Path.dir path)

  1057       else ();

  1058       File.write path (Pretty.output p ^ "\n");

  1059       p

  1060   );

  1062 fun mk_module_file postprocess_module ext path name p =

  1063   let

  1064     val prfx = Path.dir path;

  1065     val name' = case name

  1066      of "" => Path.base path

  1067       | _ => (Path.ext ext o Path.unpack o implode o separate "/" o NameSpace.unpack) name;

  1068   in

  1069     p

  1070     |> write_file true (Path.append prfx name')

  1071     |> postprocess_module name

  1072   end;

  1074 fun parse_args f args =

  1075   case f args

  1076    of (x, []) => x

  1077     | (_, _) => error "bad serializer arguments";

  1079 fun parse_single_file serializer =

  1080   parse_args (Args.name

  1081   >> (fn path => serializer

  1082         (fn "" => write_file false (Path.unpack path) #> K NONE

  1083           | _ => SOME)));

  1085 fun parse_multi_file postprocess_module ext serializer =

  1086   parse_args (Args.name

  1087   >> (fn path => (serializer o mk_module_file postprocess_module ext) (Path.unpack path)));

  1089 fun parse_internal serializer =

  1090   parse_args (Args.name

  1091   >> (fn "-" => serializer

  1092         (fn "" => (fn p => (use_text Output.ml_output false (Pretty.output p); NONE))

  1093           | _ => SOME)

  1094        | _ => Scan.fail ()));

  1096 fun parse_stdout serializer =

  1097   parse_args (Args.name

  1098   >> (fn "_" => serializer

  1099         (fn "" => (fn p => (Pretty.writeln p; NONE))

  1100           | _ => SOME)

  1101        | _ => Scan.fail ()));

  1103 val nsp_module = CodegenNames.nsp_module;

  1104 val nsp_class = CodegenNames.nsp_class;

  1105 val nsp_tyco = CodegenNames.nsp_tyco;

  1106 val nsp_inst = CodegenNames.nsp_inst;

  1107 val nsp_fun = CodegenNames.nsp_fun;

  1108 val nsp_classop = CodegenNames.nsp_classop;

  1109 val nsp_dtco = CodegenNames.nsp_dtco;

  1110 val nsp_eval = CodegenNames.nsp_eval;

  1113 (** ML serializer **)

  1115 local

  1117 val reserved_ml' = [

  1118   "bool", "int", "list", "unit", "option", "true", "false", "not",

  1119   "NONE", "SOME", "o", "string", "char", "String", "Term"

  1120 ];

  1122 fun ml_from_defs (_, tyco_syntax, const_syntax) deresolver prefx defs =

  1123   let

  1124     val seri = pr_sml_def tyco_syntax const_syntax

  1125       (make_vars (ThmDatabase.ml_reserved @ reserved_ml'))

  1126       (deresolver prefx) #> SOME;

  1127     val filter_funs =

  1128       map

  1129         (fn (name, CodegenThingol.Fun info) => (name, info)

  1130           | (name, def) => error ("Function block containing illegal def: " ^ quote name)

  1131         )

  1132       #> MLFuns;

  1133     val filter_datatype =

  1134       map_filter

  1135         (fn (name, CodegenThingol.Datatype info) => SOME (name, info)

  1136           | (name, CodegenThingol.Datatypecons _) => NONE

  1137           | (name, def) => error ("Datatype block containing illegal def: " ^ quote name)

  1138         )

  1139       #> MLDatas;

  1140     fun filter_class defs =

  1141       case map_filter

  1142         (fn (name, CodegenThingol.Class info) => SOME (name, info)

  1143           | (name, CodegenThingol.Classmember _) => NONE

  1144           | (name, def) => error ("Class block containing illegal def: " ^ quote name)

  1145         ) defs

  1146        of [class] => MLClass class

  1147         | _ => error ("Class block without class: " ^ (commas o map (quote o fst)) defs)

  1148   in case defs

  1149    of (_, CodegenThingol.Fun _)::_ => (seri o filter_funs) defs

  1150     | (_, CodegenThingol.Datatypecons _)::_ => (seri o filter_datatype) defs

  1151     | (_, CodegenThingol.Datatype _)::_ => (seri o filter_datatype) defs

  1152     | (_, CodegenThingol.Class _)::_ => (seri o filter_class) defs

  1153     | (_, CodegenThingol.Classmember _)::_ => (seri o filter_class) defs

  1154     | [(inst, CodegenThingol.Classinst info)] => seri (MLClassinst (inst, info))

  1155     | defs => error ("Illegal mutual dependencies: " ^ (commas o map fst) defs)

  1156   end;

  1158 fun ml_serializer root_name target nspgrp =

  1159   let

  1160     fun ml_from_module resolv _ ((_, name), ps) =

  1161       Pretty.chunks ([

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

  1163         str "struct",

  1164         str ""

  1165       ] @ separate (str "") ps @ [

  1166         str "",

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

  1168       ]);

  1169     fun postproc (shallow, n) =

  1170       let

  1171         fun ch_first f = String.implode o nth_map 0 f o String.explode;

  1172       in if shallow = CodegenNames.nsp_dtco

  1173         then ch_first Char.toUpper n

  1174         else n

  1175       end;

  1176   in abstract_serializer (target, nspgrp)

  1177     root_name (ml_from_defs, ml_from_module,

  1178      abstract_validator (ThmDatabase.ml_reserved @ reserved_ml'), postproc) end;

  1180 in

  1182 fun ml_from_thingol target args =

  1183   let

  1184     val serializer = ml_serializer "ROOT" target [[nsp_module], [nsp_class, nsp_tyco],

  1185       [nsp_fun, nsp_dtco, nsp_class, nsp_classop, nsp_inst]]

  1186     val parse_multi =

  1187       Args.name

  1188       #-> (fn "dir" =>

  1189                parse_multi_file

  1190                  (K o SOME o str o suffix ";" o prefix "val _ = use "

  1191                   o quote o suffix ".ML" o translate_string (fn "." => "/" | s => s)) "ML" serializer

  1192             | _ => Scan.fail ());

  1193   in

  1194     (parse_multi

  1195     || parse_internal serializer

  1196     || parse_stdout serializer

  1197     || parse_single_file serializer) args

  1198   end;

  1200 val eval_verbose = ref false;

  1202 fun eval_term_proto thy data hidden ((ref_name, reff), e) code =

  1203   let

  1204     val (val_name, code') = CodegenThingol.add_eval_def (nsp_eval, e) code;

  1205     val struct_name = "EVAL";

  1206     fun output p = if !eval_verbose then (Pretty.writeln p; Pretty.output p)

  1207       else Pretty.output p;

  1208     val serializer = ml_serializer struct_name "SML" [[nsp_module], [nsp_class, nsp_tyco],

  1209       [nsp_fun, nsp_dtco, nsp_class, nsp_classop, nsp_inst], [nsp_eval]]

  1210       (fn "" => (fn p => (use_text Output.ml_output (!eval_verbose) (output p); NONE))

  1211         | _ => SOME) data

  1212         (hidden, SOME [NameSpace.pack [nsp_eval, val_name]]);

  1213     val _ = serializer code';

  1214     val val_name_struct = NameSpace.append struct_name val_name;

  1215     val _ = reff := NONE;

  1216     val _ = use_text Output.ml_output (!eval_verbose) ("val _ = (" ^ ref_name ^ " := SOME (" ^ val_name_struct ^ "))");

  1217   in case !reff

  1218    of NONE => error ("Could not retrieve value of ML reference " ^ quote ref_name

  1219         ^ " (reference probably has been shadowed)")

  1220     | SOME value => value

  1221   end;

  1223 structure NameMangler = NameManglerFun (

  1224   type ctxt = string list;

  1225   type src = string;

  1226   val ord = string_ord;

  1227   fun mk reserved_ml (name, i) =

  1228     (Symbol.alphanum o NameSpace.base) name ^ replicate_string i "'";

  1229   fun is_valid (reserved_ml : string list) = not o member (op =) reserved_ml;

  1230   fun maybe_unique _ _ = NONE;

  1231   fun re_mangle _ dst = error ("No such definition name: " ^ quote dst);

  1232 );

  1234 fun mk_flat_ml_resolver names =

  1235   let

  1236     val mangler =

  1237       NameMangler.empty

  1238       |> fold_map (NameMangler.declare (ThmDatabase.ml_reserved @ reserved_ml')) names

  1239       |-> (fn _ => I)

  1240   in NameMangler.get (ThmDatabase.ml_reserved @ reserved_ml') mangler end;

  1242 end; (* local *)

  1245 (** haskell serializer **)

  1247 fun hs_from_thingol target args =

  1248   let

  1249     fun hs_from_defs keyword_vars (class_syntax, tyco_syntax, const_syntax) deresolver prefix defs =

  1250       let

  1251         val deresolv = deresolver "";

  1252         val deresolv_here = deresolver prefix;

  1253         val hs_from_def = pr_haskell class_syntax tyco_syntax const_syntax

  1254           keyword_vars deresolv_here deresolv;

  1255       in case map_filter hs_from_def defs

  1256        of [] => NONE

  1257         | ps => (SOME o Pretty.chunks o separate (str "")) ps

  1258       end;

  1259     val reserved_hs = [

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

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

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

  1263     ] @ [

  1264       "Bool", "Integer", "Maybe", "True", "False", "Nothing", "Just", "not", "negate",

  1265       "String", "Char"

  1266     ];

  1267     fun hs_from_module resolv imps ((_, name), ps) =

  1268       (Pretty.chunks) (

  1269         str ("module " ^ name ^ " where")

  1270         :: map (str o prefix "import qualified ") imps @ (

  1271           str ""

  1272           :: separate (str "") ps

  1273       ));

  1274     fun postproc (shallow, n) =

  1275       let

  1276         fun ch_first f = String.implode o nth_map 0 f o String.explode;

  1277       in if member (op =) [nsp_module, nsp_class, nsp_tyco, nsp_dtco] shallow

  1278         then ch_first Char.toUpper n

  1279         else ch_first Char.toLower n

  1280       end;

  1281     val serializer = abstract_serializer (target, [[nsp_module],

  1282       [nsp_class], [nsp_tyco], [nsp_fun, nsp_classop], [nsp_dtco], [nsp_inst]])

  1283       "Main" (hs_from_defs (make_vars reserved_hs), hs_from_module, abstract_validator reserved_hs, postproc);

  1284   in

  1285     (parse_multi_file ((K o K) NONE) "hs" serializer) args

  1286   end;

  1290 (** theory data **)

  1292 datatype syntax_expr = SyntaxExpr of {

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

  1294   inst: unit Symtab.table,

  1295   tyco: (itype pretty_syntax * serial) Symtab.table,

  1296   const: (iterm pretty_syntax * serial) Symtab.table

  1297 };

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

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

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

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

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

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

  1305   mk_syntax_expr (

  1306     (Symtab.merge (eq_snd (op =)) (class1, class2),

  1307        Symtab.merge (op =) (inst1, inst2)),

  1308     (Symtab.merge (eq_snd (op =)) (tyco1, tyco2),

  1309        Symtab.merge (eq_snd (op =)) (const1, const2))

  1310   );

  1312 datatype syntax_modl = SyntaxModl of {

  1313   merge: string Symtab.table,

  1314   prolog: Pretty.T Symtab.table

  1315 };

  1317 fun mk_syntax_modl (merge, prolog) =

  1318   SyntaxModl { merge = merge, prolog = prolog };

  1319 fun map_syntax_modl f (SyntaxModl { merge, prolog }) =

  1320   mk_syntax_modl (f (merge, prolog));

  1321 fun merge_syntax_modl (SyntaxModl { merge = merge1, prolog = prolog1 },

  1322     SyntaxModl { merge = merge2, prolog = prolog2 }) =

  1323   mk_syntax_modl (

  1324     Symtab.merge (op =) (merge1, merge2),

  1325     Symtab.merge (op =) (prolog1, prolog2)

  1326   );

  1328 type serializer = string -> Args.T list

  1329 -> (string -> (string * (string -> string option)) option)

  1330    * (string

  1331       -> (int

  1332           * (fixity

  1333              -> (fixity

  1334                  -> itype -> Pretty.T)

  1335                 -> itype list -> Pretty.T))

  1336            option)

  1337    * (string

  1338       -> (int

  1339           * (fixity

  1340              -> (fixity

  1341                  -> iterm -> Pretty.T)

  1342                 -> iterm list -> Pretty.T))

  1343            option)

  1344    -> string list * string list option

  1345       -> CodegenThingol.code -> unit;

  1347 datatype target = Target of {

  1348   serial: serial,

  1349   serializer: serializer,

  1350   syntax_expr: syntax_expr,

  1351   syntax_modl: syntax_modl

  1352 };

  1354 fun mk_target (serial, (serializer, (syntax_expr, syntax_modl))) =

  1355   Target { serial = serial, serializer = serializer, syntax_expr = syntax_expr, syntax_modl = syntax_modl };

  1356 fun map_target f ( Target { serial, serializer, syntax_expr, syntax_modl } ) =

  1357   mk_target (f (serial, (serializer, (syntax_expr, syntax_modl))));

  1358 fun merge_target target (Target { serial = serial1, serializer = serializer, syntax_expr = syntax_expr1, syntax_modl = syntax_modl1 },

  1359     Target { serial = serial2, serializer = _, syntax_expr = syntax_expr2, syntax_modl = syntax_modl2 }) =

  1360   if serial1 = serial2 then

  1361     mk_target (serial1, (serializer,

  1362       (merge_syntax_expr (syntax_expr1, syntax_expr2),

  1363         merge_syntax_modl (syntax_modl1, syntax_modl2))

  1364     ))

  1365   else

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

  1368 structure CodegenSerializerData = TheoryDataFun

  1369 (struct

  1370   val name = "Pure/codegen_serializer";

  1371   type T = target Symtab.table;

  1372   val empty = Symtab.empty;

  1373   val copy = I;

  1374   val extend = I;

  1375   fun merge _ = Symtab.join merge_target;

  1376   fun print _ _ = ();

  1377 end);

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

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

  1381 fun the_syntax_modl (Target { syntax_modl = SyntaxModl x, ... }) = x;

  1383 fun add_serializer (target, seri) thy =

  1384   let

  1385     val _ = case Symtab.lookup (CodegenSerializerData.get thy) target

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

  1387       | NONE => ();

  1388   in

  1389     thy

  1390     |> (CodegenSerializerData.map oo Symtab.map_default)

  1391           (target, mk_target (serial (), (seri,

  1392             (mk_syntax_expr ((Symtab.empty, Symtab.empty), (Symtab.empty, Symtab.empty)),

  1393               mk_syntax_modl (Symtab.empty, Symtab.empty)))))

  1394           (map_target (fn (serial, (_, syntax)) => (serial, (seri, syntax))))

  1395   end;

  1397 val _ = Context.add_setup (

  1398   CodegenSerializerData.init

  1399   #> add_serializer ("SML", ml_from_thingol)

  1400   #> add_serializer ("Haskell", hs_from_thingol)

  1401 );

  1403 fun get_serializer thy (target, args) cs =

  1404   let

  1405     val data = case Symtab.lookup (CodegenSerializerData.get thy) target

  1406      of SOME data => data

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

  1408     val seri = the_serializer data;

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

  1410     fun fun_of sys = (Option.map fst oo Symtab.lookup) sys;

  1411   in

  1412     seri target args (fun_of class, fun_of tyco, fun_of const)

  1413       (Symtab.keys class @ Symtab.keys inst @ Symtab.keys tyco @ Symtab.keys const, cs)

  1414   end;

  1416 fun has_serialization f thy targets name =

  1417   forall (

  1418     is_some o (fn tab => Symtab.lookup tab name) o f o the_syntax_expr o the

  1419       o (Symtab.lookup ((CodegenSerializerData.get) thy))

  1420   ) targets;

  1422 val tyco_has_serialization = has_serialization #tyco;

  1423 val const_has_serialization = has_serialization #const;

  1425 fun eval_term thy =

  1426   let

  1427     val target = "SML";

  1428     val data = case Symtab.lookup (CodegenSerializerData.get thy) target

  1429      of SOME data => data

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

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

  1432     fun fun_of sys = (Option.map fst oo Symtab.lookup) sys;

  1433   in

  1434     eval_term_proto thy (fun_of class, fun_of tyco, fun_of const)

  1435       (Symtab.keys class @ Symtab.keys inst @ Symtab.keys tyco @ Symtab.keys const)

  1436   end;

  1440 (** ML and toplevel interface **)

  1442 local

  1444 fun map_syntax_exprs target f thy =

  1445   let

  1446     val _ = if is_some (Symtab.lookup (CodegenSerializerData.get thy) target)

  1447       then ()

  1448       else error ("Unknown code target language: " ^ quote target);

  1449   in

  1450     thy

  1451     |> (CodegenSerializerData.map o Symtab.map_entry target o map_target

  1452           o apsnd o apsnd o apfst o map_syntax_expr) f

  1453   end;

  1455 fun gen_add_syntax_class prep_class prep_const target raw_class (syntax, raw_ops) thy =

  1456   let

  1457     val cls = prep_class thy raw_class

  1458     val class = CodegenNames.class thy cls;

  1459     fun mk_classop (const as (c, _)) = case AxClass.class_of_param thy c

  1460      of SOME class' => if cls = class' then CodegenNames.const thy const

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

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

  1463     val ops = (map o apfst) (mk_classop o prep_const thy) raw_ops;

  1464     val syntax_ops = AList.lookup (op =) ops;

  1465   in

  1466     thy

  1467     |> (map_syntax_exprs target o apfst o apfst)

  1468         (Symtab.update (class, ((syntax, syntax_ops), serial ())))

  1469   end;

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

  1472   let

  1473     val inst = CodegenNames.instance thy (prep_class thy raw_class, prep_tyco thy raw_tyco);

  1474   in

  1475     thy

  1476     |> (map_syntax_exprs target o apfst o apsnd)

  1477         (Symtab.update (inst, ()))

  1478   end;

  1480 fun gen_add_syntax_tyco prep_tyco raw_tyco target syntax thy =

  1481   let

  1482     val tyco = (CodegenNames.tyco thy o prep_tyco thy) raw_tyco;

  1483   in

  1484     thy

  1485     |> (map_syntax_exprs target o apsnd o apfst)

  1486          (Symtab.update (tyco, (syntax, serial ())))

  1487   end;

  1489 fun gen_add_syntax_const prep_const raw_c target syntax thy =

  1490   let

  1491     val c' = prep_const thy raw_c;

  1492     val c'' = CodegenNames.const thy c';

  1493   in

  1494     thy

  1495     |> (map_syntax_exprs target o apsnd o apsnd)

  1496          (Symtab.update (c'', (syntax, serial ())))

  1497   end;

  1499 fun read_type thy raw_tyco =

  1500   let

  1501     val tyco = Sign.intern_type thy raw_tyco;

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

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

  1504   in tyco end;

  1506 fun idfs_of_const_names thy cs =

  1507   let

  1508     val cs' = AList.make (fn c => Sign.the_const_type thy c) cs;

  1509     val cs'' = map (CodegenConsts.norm_of_typ thy) cs';

  1510   in AList.make (CodegenNames.const thy) cs'' end;

  1512 fun parse_quote num_of consts_of target get_init adder =

  1513   parse_syntax num_of #-> (fn mfx => pair (fn thy => adder target (mfx thy) thy));

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

  1516   f x #-> (fn y => fold_map (fn x => g |-- f x >> pair x) xs

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

  1519 structure P = OuterParse

  1520 and K = OuterKeyword

  1522 fun parse_multi_syntax parse_thing parse_syntax =

  1523   P.and_list1 parse_thing

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

  1525       (fn target => zip_list things (parse_syntax target)

  1526         (P.$$$ "and")) --| P.$$$ ")"))

  1528 val add_syntax_class = gen_add_syntax_class ClassPackage.read_class CodegenConsts.read_const;

  1529 val add_syntax_inst = gen_add_syntax_inst ClassPackage.read_class read_type;

  1531 fun parse_syntax_tyco target raw_tyco  =

  1532   let

  1533     fun intern thy = read_type thy raw_tyco;

  1534     fun num_of thy = Sign.arity_number thy (intern thy);

  1535     fun idf_of thy = CodegenNames.tyco thy (intern thy);

  1536     fun read_typ thy =

  1537       Sign.read_typ (thy, K NONE);

  1538   in

  1539     parse_quote num_of ((K o K) ([], [])) target idf_of

  1540       (gen_add_syntax_tyco read_type raw_tyco)

  1541   end;

  1543 fun parse_syntax_const target raw_const =

  1544   let

  1545     fun intern thy = CodegenConsts.read_const thy raw_const;

  1546     fun num_of thy = (length o fst o strip_type o Sign.the_const_type thy o fst o intern) thy;

  1547     fun idf_of thy = (CodegenNames.const thy o intern) thy;

  1548   in

  1549     parse_quote num_of CodegenConsts.consts_of target idf_of

  1550       (gen_add_syntax_const CodegenConsts.read_const raw_const)

  1551   end;

  1553 val (code_classK, code_instanceK, code_typeK, code_constK) =

  1554   ("code_class", "code_instance", "code_type", "code_const");

  1556 in

  1558 val code_classP =

  1559   OuterSyntax.command code_classK "define code syntax for class" K.thy_decl (

  1560     parse_multi_syntax P.xname

  1561       (fn _ => fn _ => P.string -- Scan.optional (P.$$$ "where" |-- Scan.repeat1

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

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

  1564           fold (fn (raw_class, syn) => add_syntax_class target raw_class syn) syns)

  1565   );

  1567 val code_instanceP =

  1568   OuterSyntax.command code_instanceK "define code syntax for instance" K.thy_decl (

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

  1570       (fn _ => fn _ => P.name #->

  1571         (fn "-" => Scan.succeed () | _ => Scan.fail_with (fn _ => "\"-\" expected") ()))

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

  1573           fold (fn (raw_inst, ()) => add_syntax_inst target raw_inst) syns)

  1574   );

  1576 val code_typeP =

  1577   OuterSyntax.command code_typeK "define code syntax for type constructor" K.thy_decl (

  1578     Scan.repeat1 (

  1579       parse_multi_syntax P.xname parse_syntax_tyco

  1580     )

  1581     >> (Toplevel.theory o (fold o fold) (fold snd o snd))

  1582   );

  1584 val code_constP =

  1585   OuterSyntax.command code_constK "define code syntax for constant" K.thy_decl (

  1586     Scan.repeat1 (

  1587       parse_multi_syntax P.term parse_syntax_const

  1588     )

  1589     >> (Toplevel.theory o (fold o fold) (fold snd o snd))

  1590   );

  1592 val _ = OuterSyntax.add_parsers [code_classP, code_instanceP, code_typeP, code_constP];

  1594 fun add_pretty_list target nill cons mk_list mk_char_string target_cons thy =

  1595   let

  1596     val [(_, nil''), (cons', cons'')] = idfs_of_const_names thy [nill, cons];

  1597     val pr = pretty_list nil'' cons'' mk_list mk_char_string target_cons;

  1598   in

  1599     thy

  1600     |> gen_add_syntax_const (K I) cons' target pr

  1601   end;

  1603 fun add_pretty_ml_string target nill cons str mk_char mk_string target_implode thy =

  1604   let

  1605     val [(_, nil''), (_, cons''), (str', _)] = idfs_of_const_names thy [nill, cons, str];

  1606     val pr = pretty_ml_string nil'' cons'' mk_char mk_string target_implode;

  1607   in

  1608     thy

  1609     |> gen_add_syntax_const (K I) str' target pr

  1610   end;

  1612 fun add_undefined target undef target_undefined thy =

  1613   let

  1614     val [(undef', _)] = idfs_of_const_names thy [undef];

  1615     fun pretty _ _ _ = str target_undefined;

  1616   in

  1617     thy

  1618     |> gen_add_syntax_const (K I) undef' target (~1, pretty)

  1619   end;

  1621 end; (*local*)

  1623 end; (* struct *)

author	haftmann
	Tue, 10 Oct 2006 09:17:17 +0200
changeset 20931	19d9b78218fd
parent 20926	b2f67b947200
child 20940	2526ef41a189
permissions	-rw-r--r--