--- a/src/Pure/Tools/codegen_serializer.ML Mon Nov 21 11:14:11 2005 +0100
+++ b/src/Pure/Tools/codegen_serializer.ML Mon Nov 21 15:15:32 2005 +0100
@@ -3,17 +3,574 @@
Author: Florian Haftmann, TU Muenchen
Serializer from intermediate language ("Thin-gol") to
-target languages (like ML or Haskell)
+target languages (like ML or Haskell).
*)
signature CODEGEN_SERIALIZER =
sig
- val bot: unit;
+ type primitives;
+ val empty_prims: primitives;
+ val add_prim: string * (string * string list) -> primitives -> primitives;
+ val merge_prims: primitives * primitives -> primitives;
+ val has_prim: primitives -> string -> bool;
+ val mk_prims: primitives -> string;
+
+ type 'a pretty_syntax = string -> Pretty.T list -> ('a -> Pretty.T)
+ -> (string list * Pretty.T) option;
+ type serializer = CodegenThingol.itype pretty_syntax -> CodegenThingol.iexpr pretty_syntax
+ -> primitives -> CodegenThingol.module -> Pretty.T;
+
+ val ml_from_thingol: string list list -> string -> serializer;
end;
structure CodegenSerializer: CODEGEN_SERIALIZER =
struct
-val bot = ();
+open CodegenThingol;
+
+
+(** target language primitives **)
+
+type primitives = string Graph.T;
+
+val empty_prims = Graph.empty;
+
+fun add_prim (f, (def, deps)) prims =
+ prims
+ |> Graph.new_node (f, def)
+ |> fold (fn dep => Graph.add_edge (f, dep)) deps;
+
+val merge_prims = Graph.merge (op =) : primitives * primitives -> primitives;
+
+val has_prim : primitives -> string -> bool = can o Graph.get_node;
+
+fun get_prims prims defs =
+ defs
+ |> filter (can (Graph.get_node prims))
+ |> `I
+ ||> Graph.all_succs prims
+ ||> (fn gr => Graph.subgraph gr prims)
+ ||> Graph.strong_conn
+ ||> rev
+ ||> Library.flat
+ ||> map (Graph.get_node prims)
+ ||> separate ""
+ ||> cat_lines
+ ||> suffix "\n";
+
+fun mk_prims prims = get_prims prims (Graph.keys prims) |> snd;
+
+
+(** generic serialization **)
+
+type 'a pretty_syntax = string -> Pretty.T list -> ('a -> Pretty.T)
+ -> (string list * Pretty.T) option;
+type serializer = CodegenThingol.itype pretty_syntax -> CodegenThingol.iexpr pretty_syntax
+ -> primitives -> CodegenThingol.module -> Pretty.T;
+
+datatype lrx = L | R | X;
+
+datatype brack =
+ BR
+ | NOBR
+ | INFX of (int * lrx);
+
+fun eval_lrx L L = false
+ | eval_lrx R R = false
+ | eval_lrx _ _ = true;
+
+fun eval_br BR _ = true
+ | eval_br NOBR _ = false
+ | eval_br (INFX (pr1, lr1)) (INFX (pr2, lr2)) =
+ pr1 > pr2
+ orelse pr1 = pr2
+ andalso eval_lrx lr1 lr2
+ | eval_br (INFX _) _ = false;
+
+fun eval_br_postfix BR _ = false
+ | eval_br_postfix NOBR _ = false
+ | eval_br_postfix (INFX (pr1, lr1)) (INFX (pr2, lr2)) =
+ pr1 > pr2
+ orelse pr1 = pr2
+ andalso eval_lrx lr1 lr2
+ | eval_br_postfix (INFX _) _ = false;
+
+fun brackify _ [p] = p
+ | brackify true (ps as _::_) = Pretty.enclose "(" ")" (Pretty.breaks ps)
+ | brackify false (ps as _::_) = Pretty.block (Pretty.breaks ps);
+
+fun postify [] f = [f]
+ | postify [p] f = [p, Pretty.brk 1, f]
+ | postify (ps as _::_) f = [Pretty.list "(" ")" ps, Pretty.brk 1, f];
+
+fun praetify [] f = [f]
+ | praetify [p] f = [f, Pretty.str " of ", p]
+
+
+(** ML serializer **)
+
+local
+
+fun ml_validator prims name =
+ let
+ fun replace_invalid c =
+ if (Char.isAlphaNum o the o Char.fromString) c orelse c = "'"
+ andalso not (NameSpace.separator = c)
+ then c
+ else "_"
+ fun suffix_it name =
+ name
+ |> member (op =) ThmDatabase.ml_reserved ? suffix "'"
+ |> member (op =) CodegenThingol.prims ? suffix "'"
+ |> has_prim prims ? suffix "'"
+ |> (fn name' => if name = name' then name else suffix_it name')
+ in
+ name
+ |> translate_string replace_invalid
+ |> suffix_it
+ |> (fn name' => if name = name' then NONE else SOME name')
+ end;
+
+val ml_label_uniq = translate_string (fn "'" => "''" | "." => "'" | c => c);
-end; (* structure *)
+fun ml_from_defs styco sconst resolv ds =
+ let
+ fun chunk_defs ps =
+ let
+ val (p_init, p_last) = split_last ps
+ in
+ Pretty.chunks (p_init @ [Pretty.block ([p_last, Pretty.str ";"])])
+ end;
+ fun ml_from_typ br (IType ("Pair", [t1, t2])) =
+ brackify (eval_br_postfix br (INFX (2, L))) [
+ ml_from_typ (INFX (2, X)) t1,
+ Pretty.str "*",
+ ml_from_typ (INFX (2, X)) t2
+ ]
+ | ml_from_typ br (IType ("Bool", [])) =
+ Pretty.str "bool"
+ | ml_from_typ br (IType ("Integer", [])) =
+ Pretty.str "IntInf.int"
+ | ml_from_typ br (IType ("List", [ty])) =
+ postify ([ml_from_typ BR ty]) (Pretty.str "list")
+ |> Pretty.block
+ | ml_from_typ br (IType (tyco, typs)) =
+ let
+ val tyargs = (map (ml_from_typ BR) typs)
+ in
+ case styco tyco tyargs (ml_from_typ BR)
+ of NONE =>
+ postify tyargs ((Pretty.str o resolv) tyco)
+ |> Pretty.block
+ | SOME ([], p) =>
+ p
+ | SOME (_, p) =>
+ error ("cannot serialize partial type application to ML, while serializing "
+ ^ quote (tyco ^ " " ^ Pretty.output (Pretty.list "(" ")" tyargs)))
+ end
+ | ml_from_typ br (IFun (t1, t2)) =
+ brackify (eval_br_postfix br (INFX (1, R))) [
+ ml_from_typ (INFX (1, X)) t1,
+ Pretty.str "->",
+ ml_from_typ (INFX (1, R)) t2
+ ]
+ | ml_from_typ _ (IVarT (v, [])) =
+ Pretty.str ("'" ^ v)
+ | ml_from_typ _ (IVarT (_, sort)) =
+ "cannot serialize sort constrained type variable to ML: " ^ commas sort |> error
+ | ml_from_typ _ (IDictT fs) =
+ (Pretty.enclose "{" "}" o Pretty.breaks) (
+ map (fn (f, ty) =>
+ Pretty.block [Pretty.str (ml_label_uniq f ^ ": "), ml_from_typ NOBR ty]) fs
+ );
+ fun ml_from_pat br (ICons (("True", []), _)) =
+ Pretty.str "true"
+ | ml_from_pat br (ICons (("False", []), _)) =
+ Pretty.str "false"
+ | ml_from_pat br (ICons (("Pair", ps), _)) =
+ ps
+ |> map (ml_from_pat NOBR)
+ |> Pretty.list "(" ")"
+ | ml_from_pat br (ICons (("Nil", []), _)) =
+ Pretty.str "[]"
+ | ml_from_pat br (p as ICons (("Cons", _), _)) =
+ let
+ fun dest_cons (ICons (("Cons", [ICons (("Pair", [p1, p2]), _)]), _)) = SOME (p1, p2)
+ | dest_cons p = NONE
+ in
+ case unfoldr dest_cons p
+ of (ps, (ICons (("Nil", []), _))) =>
+ ps
+ |> map (ml_from_pat NOBR)
+ |> Pretty.list "[" "]"
+ | (ps, p) =>
+ (ps @ [p])
+ |> map (ml_from_pat (INFX (5, X)))
+ |> separate (Pretty.str "::")
+ |> brackify (eval_br br (INFX (5, R)))
+ end
+ | ml_from_pat br (ICons ((f, ps), ty)) =
+ ps
+ |> map (ml_from_pat BR)
+ |> cons ((Pretty.str o resolv) f)
+ |> brackify (eval_br br BR)
+ | ml_from_pat br (IVarP (v, IType ("Integer", []))) =
+ Pretty.str ("(" ^ v ^ ":IntInf.int)")
+ | ml_from_pat br (IVarP (v, _)) =
+ Pretty.str v;
+ fun ml_from_iexpr br (e as (IApp (IConst ("Cons", _), _))) =
+ let
+ fun dest_cons (IApp (IConst ("Cons", _),
+ IApp (IApp (IConst ("Pair", _), e1), e2))) = SOME (e1, e2)
+ | dest_cons p = NONE
+ in
+ case unfoldr dest_cons e
+ of (es, (IConst ("Nil", _))) =>
+ es
+ |> map (ml_from_iexpr NOBR)
+ |> Pretty.list "[" "]"
+ | (es, e) =>
+ (es @ [e])
+ |> map (ml_from_iexpr (INFX (5, X)))
+ |> separate (Pretty.str "::")
+ |> brackify (eval_br br (INFX (5, R)))
+ end
+ | ml_from_iexpr br (e as IApp (e1, e2)) =
+ (case (unfold_app e)
+ of (e as (IConst (f, _)), es) =>
+ ml_from_app br (f, es)
+ | _ =>
+ brackify (eval_br br BR) [
+ ml_from_iexpr NOBR e1,
+ ml_from_iexpr BR e2
+ ])
+ | ml_from_iexpr br (e as IConst (f, _)) =
+ ml_from_app br (f, [])
+ | ml_from_iexpr br (IVarE (v, _)) =
+ Pretty.str v
+ | ml_from_iexpr br (IAbs ((v, _), e)) =
+ brackify (eval_br br BR) [
+ Pretty.str ("fn " ^ v ^ " =>"),
+ ml_from_iexpr BR e
+ ]
+ | ml_from_iexpr br (e as ICase (_, [_])) =
+ let
+ val (ps, e) = unfold_let e;
+ fun mk_val (p, e) = Pretty.block [
+ Pretty.str "val ",
+ ml_from_pat BR p,
+ Pretty.str " =",
+ Pretty.brk 1,
+ ml_from_iexpr NOBR e,
+ Pretty.str ";"
+ ]
+ in Pretty.chunks [
+ [Pretty.str ("let"), Pretty.fbrk, map mk_val ps |> Pretty.chunks] |> Pretty.block,
+ [Pretty.str ("in"), Pretty.fbrk, ml_from_iexpr NOBR e] |> Pretty.block,
+ Pretty.str ("end")
+ ] end
+ | ml_from_iexpr br (ICase (e, c::cs)) =
+ let
+ fun mk_clause definer (p, e) =
+ Pretty.block [
+ Pretty.str definer,
+ ml_from_pat NOBR p,
+ Pretty.str " =>",
+ Pretty.brk 1,
+ ml_from_iexpr NOBR e
+ ]
+ in brackify (eval_br br BR) (
+ Pretty.str "case "
+ :: ml_from_iexpr NOBR e
+ :: mk_clause "of " c
+ :: map (mk_clause "|") cs
+ ) end
+ | ml_from_iexpr br (IInst _) =
+ error "cannot serialize poly instant to ML"
+ | ml_from_iexpr br (IDictE fs) =
+ (Pretty.enclose "{" "}" o Pretty.breaks) (
+ map (fn (f, e) =>
+ Pretty.block [Pretty.str (ml_label_uniq f ^ " = "), ml_from_iexpr NOBR e]) fs
+ )
+ | ml_from_iexpr br (ILookup (ls, v)) =
+ brackify (eval_br br BR) [
+ Pretty.str "(",
+ ls |> map ((fn s => "#" ^ s) o ml_label_uniq) |> foldr1 (fn (l, e) => l ^ " o " ^ e) |> Pretty.str,
+ Pretty.str ")",
+ Pretty.str " ",
+ Pretty.str v
+ ]
+ and mk_app_p br p args =
+ brackify (eval_br br BR)
+ (p :: map (ml_from_iexpr BR) args)
+ and ml_from_app br ("Nil", []) =
+ Pretty.str "[]"
+ | ml_from_app br ("True", []) =
+ Pretty.str "true"
+ | ml_from_app br ("False", []) =
+ Pretty.str "false"
+ | ml_from_app br ("primeq", [e1, e2]) =
+ brackify (eval_br br (INFX (4, L))) [
+ ml_from_iexpr (INFX (4, L)) e1,
+ Pretty.str "=",
+ ml_from_iexpr (INFX (4, X)) e2
+ ]
+ | ml_from_app br ("Pair", [e1, e2]) =
+ Pretty.list "(" ")" [
+ ml_from_iexpr NOBR e1,
+ ml_from_iexpr NOBR e2
+ ]
+ | ml_from_app br ("and", [e1, e2]) =
+ brackify (eval_br br (INFX (~1, L))) [
+ ml_from_iexpr (INFX (~1, L)) e1,
+ Pretty.str "andalso",
+ ml_from_iexpr (INFX (~1, X)) e2
+ ]
+ | ml_from_app br ("or", [e1, e2]) =
+ brackify (eval_br br (INFX (~2, L))) [
+ ml_from_iexpr (INFX (~2, L)) e1,
+ Pretty.str "orelse",
+ ml_from_iexpr (INFX (~2, X)) e2
+ ]
+ | ml_from_app br ("if", [b, e1, e2]) =
+ brackify (eval_br br BR) [
+ Pretty.str "if",
+ ml_from_iexpr BR b,
+ Pretty.str "then",
+ ml_from_iexpr BR e1,
+ Pretty.str "else",
+ ml_from_iexpr BR e2
+ ]
+ | ml_from_app br ("add", [e1, e2]) =
+ brackify (eval_br br (INFX (6, L))) [
+ ml_from_iexpr (INFX (6, L)) e1,
+ Pretty.str "+",
+ ml_from_iexpr (INFX (6, X)) e2
+ ]
+ | ml_from_app br ("mult", [e1, e2]) =
+ brackify (eval_br br (INFX (7, L))) [
+ ml_from_iexpr (INFX (7, L)) e1,
+ Pretty.str "+",
+ ml_from_iexpr (INFX (7, X)) e2
+ ]
+ | ml_from_app br ("lt", [e1, e2]) =
+ brackify (eval_br br (INFX (4, L))) [
+ ml_from_iexpr (INFX (4, L)) e1,
+ Pretty.str "<",
+ ml_from_iexpr (INFX (4, X)) e2
+ ]
+ | ml_from_app br ("le", [e1, e2]) =
+ brackify (eval_br br (INFX (7, L))) [
+ ml_from_iexpr (INFX (4, L)) e1,
+ Pretty.str "<=",
+ ml_from_iexpr (INFX (4, X)) e2
+ ]
+ | ml_from_app br ("minus", es) =
+ mk_app_p br (Pretty.str "~") es
+ | ml_from_app br ("wfrec", es) =
+ mk_app_p br (Pretty.str "wfrec") es
+ | ml_from_app br (f, es) =
+ let
+ val args = map (ml_from_iexpr BR) es
+ val brackify' = K (eval_br br BR) ? (single #> Pretty.enclose "(" ")")
+ fun prepend_abs v body =
+ Pretty.block [Pretty.str ("fn " ^ v ^ " =>"), Pretty.brk 1, body]
+ in
+ case sconst f args (ml_from_iexpr BR)
+ of NONE =>
+ brackify (eval_br br BR) (Pretty.str (resolv f) :: args)
+ | SOME ([], p) =>
+ brackify' p
+ | SOME (vars, p) =>
+ p
+ |> fold_rev prepend_abs vars
+ |> brackify'
+ end;
+ fun ml_from_funs (ds as d::ds_tl) =
+ let
+ fun mk_definer [] = "val"
+ | mk_definer _ = "fun"
+ fun check_args (_, Fun ((pats, _)::_, _)) NONE =
+ SOME (mk_definer pats)
+ | check_args (_, Fun ((pats, _)::_, _)) (SOME definer) =
+ if mk_definer pats = definer
+ then SOME definer
+ else error ("Mixing simultaneous vals and funs not implemented")
+ | check_args _ _ =
+ error ("Function definition block containing other definitions than functions")
+ val definer = the (fold check_args ds NONE);
+ fun mk_eq definer f' ty (pats, expr) =
+ let
+ val lhs = [Pretty.str (definer ^ " " ^ f')]
+ @ (if null pats
+ then [Pretty.str ":", ml_from_typ NOBR ty]
+ else map (ml_from_pat BR) pats)
+ val rhs = [Pretty.str "=", ml_from_iexpr NOBR expr]
+ in
+ Pretty.block (separate (Pretty.brk 1) (lhs @ rhs))
+ end
+ fun mk_fun definer (f, Fun (eqs as eq::eq_tl, (_, ty))) =
+ let
+ val (pats_hd::pats_tl) = (fst o split_list) eqs
+ val _ = fold (fn x => fn y => (x ~~ y; y)) pats_tl pats_hd
+ (*check for equal length of argument lists*)
+ in (Pretty.block o Pretty.fbreaks) (
+ (*Pretty.block [
+ Pretty.brk 1,
+ Pretty.str ": ",
+ ml_from_typ NOBR ty
+ ]*)
+ mk_eq definer f ty eq
+ :: map (mk_eq "|" f ty) eq_tl
+ )
+ end
+ in
+ chunk_defs (
+ mk_fun definer d
+ :: map (mk_fun "and") ds_tl
+ )
+ end;
+ fun ml_from_datatypes ds =
+ let
+ val _ = debug 9 (fn _ => map (pretty_def o snd) ds |> Pretty.chunks |> Pretty.output) ();
+ fun check_typ_dup ty xs =
+ if AList.defined (op =) xs ty
+ then error ("double datatype definition: " ^ quote ty)
+ else xs
+ fun check_typ_miss ty xs =
+ if AList.defined (op =) xs ty
+ then xs
+ else error ("missing datatype definition: " ^ quote ty)
+ fun group (name, Datatype (vs, _, _)) ts =
+ (map (fn (_, []) => () | _ => error "can't serialize sort constrained datatype declaration to ML") vs;
+ ts
+ |> apsnd (check_typ_dup name)
+ |> apsnd (AList.update (op =) (name, (vs, []))))
+ | group (_, Datatypecons (_, _::_::_)) _ =
+ error ("Datatype constructor containing more than one parameter")
+ | group (name, Datatypecons (ty, tys)) ts =
+ ts
+ |> apfst (AList.default (op =) (resolv ty, []))
+ |> apfst (AList.map_entry (op =) (resolv ty) (cons (name, tys)))
+ | group _ _ =
+ error ("Datatype block containing other statements than datatype or constructor definitions")
+ fun group_cons (ty, co) ts =
+ ts
+ |> check_typ_miss ty
+ |> AList.map_entry (op =) ty (rpair co o fst)
+ fun mk_datatypes (ds as d::ds_tl) =
+ let
+ fun mk_cons (co, typs) =
+ (Pretty.block oo praetify)
+ (map (ml_from_typ NOBR) typs)
+ (Pretty.str (resolv co))
+ fun mk_datatype definer (t, (vs, cs)) =
+ Pretty.block (
+ [Pretty.str definer]
+ @ postify (map (ml_from_typ BR o IVarT) vs)
+ (Pretty.str t)
+ @ [Pretty.str " =",
+ Pretty.brk 1]
+ @ separate (Pretty.block [Pretty.brk 1, Pretty.str "| "]) (map mk_cons cs)
+ )
+ in
+ chunk_defs (
+ mk_datatype "datatype " d
+ :: map (mk_datatype "and ") ds_tl
+ )
+ end;
+ in
+ ([], [])
+ |> fold group ds
+ |-> (fn cons => fold group_cons cons)
+ |> mk_datatypes
+ end;
+ fun ml_from_def (name, Typesyn (vs, ty)) =
+ (map (fn (vname, []) => () | _ => error "can't serialize sort constrained type declaration to ML") vs;
+ Pretty.block (
+ Pretty.str "type "
+ :: postify (map (Pretty.str o fst) vs) (Pretty.str name)
+ @ [Pretty.str " =",
+ Pretty.brk 1,
+ ml_from_typ NOBR ty,
+ Pretty.str ";"
+ ]))
+ | ml_from_def (name, Nop) =
+ if exists (fn query => (is_some o query) name)
+ [(fn name => styco name [] (ml_from_typ NOBR)),
+ (fn name => sconst name [] (ml_from_iexpr NOBR))]
+ then Pretty.str ""
+ else error ("empty statement during serialization: " ^ quote name)
+ | ml_from_def (name, Class _) =
+ error ("can't serialize class declaration " ^ quote name ^ " to ML")
+ | ml_from_def (name, Classinst _) =
+ error ("can't serialize instance declaration " ^ quote name ^ " to ML")
+ in case (snd o hd) ds
+ of Fun _ => ml_from_funs ds
+ | Datatypecons _ => ml_from_datatypes ds
+ | Datatype _ => ml_from_datatypes ds
+ | _ => (case ds of [d] => ml_from_def d)
+ end;
+
+in
+
+fun ml_from_thingol nspgrp name_root styco sconst prims module =
+ let
+ fun ml_from_module (name, ps) =
+ Pretty.chunks ([
+ Pretty.str ("structure " ^ name ^ " = "),
+ Pretty.str "struct",
+ Pretty.str ""
+ ] @ ps @ [
+ Pretty.str "",
+ Pretty.str ("end; (* struct " ^ name ^ " *)")
+ ]);
+ fun eta_expander "Pair" = 2
+ | eta_expander "Cons" = 2
+ | eta_expander "primeq" = 2
+ | eta_expander "and" = 2
+ | eta_expander "or" = 2
+ | eta_expander "if" = 3
+ | eta_expander "add" = 2
+ | eta_expander "mult" = 2
+ | eta_expander "lt" = 2
+ | eta_expander "le" = 2
+ | eta_expander s =
+ if NameSpace.is_qualified s
+ then case get_def module s
+ of Datatypecons (_ , tys) =>
+ if length tys >= 2 then length tys else 0
+ | _ =>
+ (case sconst s [] (K (Pretty.str ""))
+ of NONE => 0
+ | SOME (xs, _) => length xs)
+ else 0
+ in
+ module
+ |> debug 5 (Pretty.output o pretty_module)
+ |> debug 3 (fn _ => "connecting datatypes and classdecls...")
+ |> connect_datatypes_clsdecls
+ |> debug 3 (fn _ => "selecting submodule...")
+ |> I (*! HIER SOLLTE DAS TATSÄCHLICH STATTFINDEN !*)
+ |> debug 3 (fn _ => "eta-expanding...")
+ |> eta_expand eta_expander
+ |> debug 5 (Pretty.output o pretty_module)
+ |> debug 3 (fn _ => "tupelizing datatypes...")
+ |> tupelize_cons
+ |> debug 3 (fn _ => "eliminating classes...")
+ |> eliminate_classes
+ |> debug 3 (fn _ => "generating...")
+ |> serialize (ml_from_defs styco sconst) ml_from_module (ml_validator prims) nspgrp name_root
+ end;
+
+(* ML infix precedence
+ 7 / * div mod
+ 6 + - ^
+ 5 :: @
+ 4 = <> < > <= >=
+ 3 := o *)
+
+end; (* local *)
+
+end; (* struct *)
+
--- a/src/Pure/Tools/codegen_thingol.ML Mon Nov 21 11:14:11 2005 +0100
+++ b/src/Pure/Tools/codegen_thingol.ML Mon Nov 21 15:15:32 2005 +0100
@@ -33,14 +33,13 @@
val pretty_itype: itype -> Pretty.T;
val pretty_ipat: ipat -> Pretty.T;
val pretty_iexpr: iexpr -> Pretty.T;
+ val unfoldl: ('a -> ('a * 'b) option) -> 'a -> 'a * 'b list;
+ val unfoldr: ('a -> ('b * 'a) option) -> 'a -> 'b list * 'a;
val unfold_fun: itype -> itype list * itype;
val unfold_app: iexpr -> iexpr * iexpr list;
val unfold_let: iexpr -> (ipat * iexpr) list * iexpr;
val itype_of_iexpr: iexpr -> itype;
- val itype_of_ipat: ipat -> itype;
val ipat_of_iexpr: iexpr -> ipat;
- val vars_of_ipats: ipat list -> vname list;
- val instant_itype: vname * itype -> itype -> itype;
val invent_var_t_names: itype list -> int -> vname list -> vname -> vname list;
val invent_var_e_names: iexpr list -> int -> vname list -> vname -> vname list;
@@ -71,17 +70,54 @@
-> 'src -> transact -> 'dst * transact;
val gen_ensure_def: (string * gen_defgen) list -> string
-> string -> transact -> transact;
+ val start_transact: (transact -> 'a * transact) -> module -> 'a * module;
+
+ val class_eq: string;
+ val type_bool: string;
+ val type_pair: string;
+ val type_list: string;
+ val type_integer: string;
+ val cons_pair: string;
+ val fun_fst: string;
+ val fun_snd: string;
+ val Type_integer: itype;
+ val Cons_true: iexpr;
+ val Cons_false: iexpr;
+ val Cons_pair: iexpr;
+ val Cons_nil: iexpr;
+ val Cons_cons: iexpr;
+ val Fun_eq: iexpr;
+ val Fun_not: iexpr;
+ val Fun_and: iexpr;
+ val Fun_or: iexpr;
+ val Fun_if: iexpr;
+ val Fun_fst: iexpr;
+ val Fun_snd: iexpr;
+ val Fun_0: iexpr;
+ val Fun_1: iexpr;
+ val Fun_add: iexpr;
+ val Fun_mult: iexpr;
+ val Fun_minus: iexpr;
+ val Fun_lt: iexpr;
+ val Fun_le: iexpr;
+ val Fun_wfrec: iexpr;
val prims: string list;
val extract_defs: iexpr -> string list;
val eta_expand: (string -> int) -> module -> module;
+ val eta_expand_poly: module -> module;
val connect_datatypes_clsdecls: module -> module;
val tupelize_cons: module -> module;
- val eliminate_dtconstr: module -> module;
val eliminate_classes: module -> module;
val debug_level : int ref;
val debug : int -> ('a -> string) -> 'a -> 'a;
+
+ val serialize:
+ ((string -> string) -> (string * def) list -> Pretty.T)
+ -> (string * Pretty.T list -> Pretty.T)
+ -> (string -> string option)
+ -> string list list -> string -> module -> Pretty.T
end;
signature CODEGEN_THINGOL_OP =
@@ -318,6 +354,13 @@
case unfold_app e of (IConst (f, ty), es) =>
ICons ((f, map ipat_of_iexpr es), (snd o unfold_fun) ty);
+fun vars_of_itype ty =
+ let
+ fun vars (IType (_, tys)) = fold vars tys
+ | vars (IFun (ty1, ty2)) = vars ty1 #> vars ty2
+ | vars (IVarT (v, _)) = cons v
+ in vars ty [] end;
+
fun vars_of_ipats ps =
let
fun vars (ICons ((_, ps), _)) = fold vars ps
@@ -701,6 +744,10 @@
|-> (fn names => pair (names@deps))
end;
+fun start_transact f module =
+ ([], module)
+ |> f
+ |-> (fn x => fn (_, module) => (x, module));
(** primitive language constructs **)
@@ -830,6 +877,19 @@
| eta_iexpr e = eta_iexpr' e;
in map_defs (map_def_fun I eta_iexpr) end;
+val eta_expand_poly =
+ let
+ fun map_def_fun (def as Fun ([([], e)], cty as (sortctxt, (ty as IFun (ty1, ty2))))) =
+ if (not o null) sortctxt
+ orelse (null o vars_of_itype) ty
+ then def
+ else
+ let
+ val add_var = (hd (invent_var_e_names [e] 1 [] "x"), ty1)
+ in (Fun ([([IVarP add_var], IAbs (add_var, e))], cty)) end
+ | map_def_fun def = def;
+ in map_defs map_def_fun end;
+
fun connect_datatypes_clsdecls module =
let
fun extract_dep (name, Datatypecons (dtname, _)) =
@@ -872,28 +932,6 @@
transform_defs replace_def replace_ipat replace_iexpr [cons_cons] module
end;
-fun eliminate_dtconstr module =
- let
- fun replace_def (name, (Datatype (vs, cs, is))) acc =
- (Datatype (map (fn (v, _) => (v, [])) vs, cs, is), (name, vs)::acc)
- | replace_def (_, def) acc = (def, acc);
- fun constrain (ty as IType _, _) =
- ty
- | constrain (IVarT (v, sort1), (_, sort2)) =
- IVarT (v, gen_union (op =) (sort1, sort2));
- fun replace_ty tycos (ty as (IType (tyco, tys))) =
- (case AList.lookup (op =) tycos tyco
- of NONE => ty
- | SOME vs => IType (tyco, map2 constrain (tys, vs)))
- | replace_ty tycos ty =
- map_itype (replace_ty tycos) ty;
- in
- transform_defs replace_def
- (*! HIER FEHLT NOCH: ÄNDERN VON TYP UND SORTCTXT BEI FUNS !*)
- (fn tycos => map_ipat (replace_ty tycos) I)
- (fn tycos => map_iexpr (replace_ty tycos) (map_ipat (replace_ty tycos) I) I) [] module
- end;
-
fun eliminate_classes module =
let
fun mk_cls_typ_map memberdecls ty_inst =
@@ -972,6 +1010,104 @@
|> map_defs transform_defs
end;
+
+(** generic serialization **)
+
+(* resolving *)
+
+fun mk_resolvtab nspgrp validate module =
+ let
+ fun ensure_unique prfix prfix' name name' (locals, tab) =
+ let
+ fun uniquify name n =
+ let
+ val name' = if n = 0 then name else name ^ "_" ^ string_of_int n
+ in
+ if member (op =) locals name'
+ then uniquify name (n+1)
+ else case validate name
+ of NONE => name'
+ | SOME name' => uniquify name' n
+ end;
+ val name'' = uniquify name' 0;
+ in
+ (locals, tab)
+ |> apsnd (Symtab.update_new
+ (NameSpace.pack (prfix @ [name]), NameSpace.pack (prfix' @ [name''])))
+ |> apfst (cons name'')
+ |> pair name''
+ end;
+ fun fill_in prfix prfix' node tab =
+ let
+ val keys = Graph.keys node;
+ val nodes = AList.make (Graph.get_node node) keys;
+ val (mods, defs) =
+ nodes
+ |> List.partition (fn (_, Module _) => true | _ => false)
+ |> apfst (map (fn (name, Module m) => (name, m)))
+ |> apsnd (map fst)
+ fun modl_validate (name, modl) (locals, tab) =
+ (locals, tab)
+ |> ensure_unique prfix prfix' name name
+ |-> (fn name' => apsnd (fill_in (prfix @ [name]) (prfix @ [name']) modl))
+ fun ensure_unique_sidf sidf =
+ let
+ val [shallow, name] = NameSpace.unpack sidf;
+ in
+ nspgrp
+ |> get_first
+ (fn grp => if member (op =) grp shallow
+ then grp |> remove (op =) shallow |> SOME else NONE)
+ |> these
+ |> map (fn s => NameSpace.pack [s, name])
+ |> exists (member (op =) defs)
+ |> (fn b => if b then sidf else name)
+ end;
+ fun def_validate sidf (locals, tab) =
+ (locals, tab)
+ |> ensure_unique prfix prfix' sidf (ensure_unique_sidf sidf)
+ |> snd
+ in
+ ([], tab)
+ |> fold modl_validate mods
+ |> fold def_validate defs
+ |> snd
+ end;
+ in
+ Symtab.empty
+ |> fill_in [] [] module
+ end;
+
+fun mk_resolv tab =
+ let
+ fun resolver modl name =
+ if NameSpace.is_qualified name then
+ let
+ val modl' = if null modl then [] else (NameSpace.unpack o the o Symtab.lookup tab o NameSpace.pack) modl;
+ val name' = (NameSpace.unpack o the o Symtab.lookup tab) name
+ in
+ (NameSpace.pack o #3 o get_prefix (op =)) (modl', name')
+ end
+ else name
+ in resolver end;
+
+
+(* serialization *)
+
+fun serialize s_def s_module validate nspgrp name_root module =
+ let
+ val resolvtab = mk_resolvtab nspgrp validate module;
+ val resolver = mk_resolv resolvtab;
+ fun seri prfx ([(name, Module module)]) =
+ s_module (name,
+ (map (seri (prfx @ [name]))
+ ((map (AList.make (Graph.get_node module)) o rev o Graph.strong_conn) module)))
+ | seri prfx ds =
+ s_def (resolver prfx) (map (fn (name, Def def) => (name, def)) ds)
+ in
+ seri [] [(name_root, Module module)]
+ end;
+
end; (* struct *)