--- a/src/Pure/Tools/codegen_package.ML Sat Oct 07 02:47:33 2006 +0200
+++ b/src/Pure/Tools/codegen_package.ML Sat Oct 07 07:41:56 2006 +0200
@@ -11,7 +11,7 @@
val codegen_term: theory -> term -> thm * iterm;
val eval_term: theory -> (string (*reference name!*) * 'a option ref) * term -> 'a;
val const_of_idf: theory -> string -> string * typ;
- val get_root_module: theory -> CodegenThingol.module;
+ val get_root_module: theory -> CodegenThingol.code;
type appgen;
val add_appconst: string * appgen -> theory -> theory;
@@ -21,30 +21,15 @@
-> ((string * typ) list * ((term * typ) * (term * term) list)) option)
-> appgen;
val appgen_let: appgen;
-
- val print_code: theory -> unit;
- val purge_code: theory -> CodegenThingol.module;
- structure CodegenPackageData: THEORY_DATA;
- structure Code: CODE_DATA;
end;
structure CodegenPackage : CODEGEN_PACKAGE =
struct
-open CodegenThingol;
-
-(** preliminaries **)
-
-val nsp_module = CodegenNames.nsp_module;
-val nsp_class = CodegenNames.nsp_class;
-val nsp_tyco = CodegenNames.nsp_tyco;
-val nsp_inst = CodegenNames.nsp_inst;
-val nsp_fun = CodegenNames.nsp_fun;
-val nsp_classop = CodegenNames.nsp_classop;
-val nsp_dtco = CodegenNames.nsp_dtco;
-val nsp_eval = CodegenNames.nsp_eval;
-
-
+open BasicCodegenThingol;
+val tracing = CodegenThingol.tracing;
+val succeed = CodegenThingol.succeed;
+val fail = CodegenThingol.fail;
(** code extraction **)
@@ -52,7 +37,8 @@
type appgen = theory -> ((sort -> sort) * Sorts.algebra) * Consts.T
-> CodegenFuncgr.T
- -> bool * string list option -> (string * typ) * term list -> transact -> iterm * transact;
+ -> bool * string list option
+ -> (string * typ) * term list -> CodegenThingol.transact -> iterm * CodegenThingol.transact;
type appgens = (int * (appgen * stamp)) Symtab.table;
@@ -63,10 +49,10 @@
structure Code = CodeDataFun
(struct
val name = "Pure/code";
- type T = module;
- val empty = empty_module;
- fun merge _ = merge_module;
- fun purge _ _ = CodegenThingol.empty_module;
+ type T = CodegenThingol.code;
+ val empty = CodegenThingol.empty_code;
+ fun merge _ = CodegenThingol.merge_code;
+ fun purge _ _ = CodegenThingol.empty_code;
end);
structure CodegenPackageData = TheoryDataFun
@@ -82,13 +68,6 @@
val _ = Context.add_setup (Code.init #> CodegenPackageData.init);
-fun print_code thy =
- let
- val code = Code.get thy;
- in (Pretty.writeln o Pretty.chunks) [pretty_module code, pretty_deps code] end;
-
-fun purge_code thy = Code.change thy (K CodegenThingol.empty_module);
-
(* extraction kernel *)
@@ -99,61 +78,48 @@
| check_strict has_seri x (true, _) =
true;
-fun ensure_def_class thy algbr funcgr strct cls trns =
+fun ensure_def_class thy (algbr as ((proj_sort, _), _)) funcgr strct class trns =
let
- fun defgen_class thy (algbr as ((proj_sort, _), _)) funcgr strct cls trns =
- case CodegenNames.class_rev thy cls
- of SOME cls =>
- let
- val (v, cs) = (ClassPackage.the_consts_sign thy) cls;
- val superclasses = (proj_sort o Sign.super_classes thy) cls
- val idfs = map (CodegenNames.const thy o CodegenConsts.norm_of_typ thy) cs;
- in
- trns
- |> tracing (fn _ => "trying defgen class declaration for " ^ quote cls)
- |> fold_map (ensure_def_class thy algbr funcgr strct) superclasses
- ||>> (fold_map (exprgen_type thy algbr funcgr strct) o map snd) cs
- |-> (fn (supcls, memtypes) => succeed
- (Class (supcls, (unprefix "'" v, idfs ~~ memtypes))))
- end
- | _ =>
- trns
- |> fail ("No class definition found for " ^ quote cls);
- val cls' = CodegenNames.class thy cls;
+ val (v, cs) = (ClassPackage.the_consts_sign thy) class;
+ val superclasses = (proj_sort o Sign.super_classes thy) class;
+ val classops' = map (CodegenNames.const thy o CodegenConsts.norm_of_typ thy) cs;
+ val class' = CodegenNames.class thy class;
+ fun defgen_class trns =
+ trns
+ |> fold_map (ensure_def_class thy algbr funcgr strct) superclasses
+ ||>> (fold_map (exprgen_type thy algbr funcgr strct) o map snd) cs
+ |-> (fn (superclasses, classoptyps) => succeed
+ (CodegenThingol.Class (superclasses,
+ (unprefix "'" v, classops' ~~ classoptyps))))
in
trns
- |> tracing (fn _ => "generating class " ^ quote cls)
- |> ensure_def (defgen_class thy algbr funcgr strct) true ("generating class " ^ quote cls) cls'
- |> pair cls'
+ |> tracing (fn _ => "generating class " ^ quote class)
+ |> CodegenThingol.ensure_def defgen_class true
+ ("generating class " ^ quote class) class'
+ |> pair class'
end
and ensure_def_tyco thy algbr funcgr strct tyco trns =
let
+ fun defgen_datatype trns =
+ case CodegenData.get_datatype thy tyco
+ of SOME (vs, cos) =>
+ trns
+ |> fold_map (exprgen_tyvar_sort thy algbr funcgr strct) vs
+ ||>> fold_map (fn (c, tys) =>
+ fold_map (exprgen_type thy algbr funcgr strct) tys
+ #-> (fn tys' =>
+ pair ((CodegenNames.const thy o CodegenConsts.norm_of_typ thy)
+ (c, tys ---> Type (tyco, map TFree vs)), tys'))) cos
+ |-> (fn (vs, cos) => succeed (CodegenThingol.Datatype (vs, cos)))
+ | NONE =>
+ trns
+ |> fail ("No such datatype: " ^ quote tyco)
val tyco' = CodegenNames.tyco thy tyco;
val strict = check_strict (CodegenSerializer.tyco_has_serialization thy) tyco' strct;
- fun defgen_datatype thy algbr funcgr strct dtco trns =
- case CodegenNames.tyco_rev thy dtco
- of SOME dtco =>
- (case CodegenData.get_datatype thy dtco
- of SOME (vs, cos) =>
- trns
- |> tracing (fn _ => "trying defgen datatype for " ^ quote dtco)
- |> fold_map (exprgen_tyvar_sort thy algbr funcgr strct) vs
- ||>> fold_map (fn (c, tys) =>
- fold_map (exprgen_type thy algbr funcgr strct) tys
- #-> (fn tys' =>
- pair ((CodegenNames.const thy o CodegenConsts.norm_of_typ thy)
- (c, tys ---> Type (dtco, map TFree vs)), tys'))) cos
- |-> (fn (vs, cos) => succeed (Datatype (vs, cos)))
- | NONE =>
- trns
- |> fail ("No datatype found for " ^ quote dtco))
- | NONE =>
- trns
- |> fail ("Not a type constructor: " ^ quote dtco)
in
trns
|> tracing (fn _ => "generating type constructor " ^ quote tyco)
- |> ensure_def (defgen_datatype thy algbr funcgr strct) strict
+ |> CodegenThingol.ensure_def defgen_datatype strict
("generating type constructor " ^ quote tyco) tyco'
|> pair tyco'
end
@@ -226,71 +192,54 @@
trns
|> fold_map (exprgen_typinst thy algbr funcgr strct) insts
end
-and ensure_def_inst thy algbr funcgr strct (cls, tyco) trns =
+and ensure_def_inst thy (algbr as ((proj_sort, _), _)) funcgr strct (class, tyco) trns =
let
- fun defgen_inst thy (algbr as ((proj_sort, _), _)) funcgr strct inst trns =
- case CodegenNames.instance_rev thy inst
- of SOME (class, tyco) =>
- let
- val (vs, memdefs) = ClassPackage.the_inst_sign thy (class, tyco);
- val (_, members) = ClassPackage.the_consts_sign thy class;
- val arity_typ = Type (tyco, (map TFree vs));
- val superclasses = (proj_sort o Sign.super_classes thy) class
- fun gen_suparity supclass trns =
- trns
- |> ensure_def_class thy algbr funcgr strct supclass
- ||>> exprgen_typinst thy algbr funcgr strct (arity_typ, [supclass])
- |-> (fn (supclass, [Instance (supints, lss)]) => pair (supclass, (supints, lss)));
- fun gen_membr ((m0, ty0), (m, ty)) trns =
- trns
- |> ensure_def_const thy algbr funcgr strct (CodegenConsts.norm_of_typ thy (m0, ty0))
- ||>> exprgen_term thy algbr funcgr strct (Const (m, ty));
- in
- trns
- |> tracing (fn _ => "trying defgen class instance for (" ^ quote cls
- ^ ", " ^ quote tyco ^ ")")
- |> ensure_def_class thy algbr funcgr strct class
- ||>> ensure_def_tyco thy algbr funcgr strct tyco
- ||>> fold_map (exprgen_tyvar_sort thy algbr funcgr strct) vs
- ||>> fold_map gen_suparity superclasses
- ||>> fold_map gen_membr (members ~~ memdefs)
- |-> (fn ((((class, tyco), arity), suparities), memdefs) =>
- succeed (Classinst ((class, (tyco, arity)), (suparities, memdefs))))
- end
- | _ =>
- trns |> fail ("No class instance found for " ^ quote inst);
- val inst = CodegenNames.instance thy (cls, tyco);
+ val (vs, classop_defs) = ((apsnd o map) Const o ClassPackage.the_inst_sign thy)
+ (class, tyco);
+ val classops = (map (CodegenConsts.norm_of_typ thy) o snd
+ o ClassPackage.the_consts_sign thy) class;
+ val arity_typ = Type (tyco, (map TFree vs));
+ val superclasses = (proj_sort o Sign.super_classes thy) class
+ fun gen_superarity superclass trns =
+ trns
+ |> ensure_def_class thy algbr funcgr strct superclass
+ ||>> exprgen_typinst thy algbr funcgr strct (arity_typ, [superclass])
+ |-> (fn (superclass, [Instance (inst, iss)]) => pair (superclass, (inst, iss)));
+ fun gen_classop_def (classop, t) trns =
+ trns
+ |> ensure_def_const thy algbr funcgr strct classop
+ ||>> exprgen_term thy algbr funcgr strct t;
+ fun defgen_inst trns =
+ trns
+ |> ensure_def_class thy algbr funcgr strct class
+ ||>> ensure_def_tyco thy algbr funcgr strct tyco
+ ||>> fold_map (exprgen_tyvar_sort thy algbr funcgr strct) vs
+ ||>> fold_map gen_superarity superclasses
+ ||>> fold_map gen_classop_def (classops ~~ classop_defs)
+ |-> (fn ((((class, tyco), arity), superarities), classops) =>
+ succeed (CodegenThingol.Classinst ((class, (tyco, arity)), (superarities, classops))));
+ val inst = CodegenNames.instance thy (class, tyco);
in
trns
- |> tracing (fn _ => "generating instance " ^ quote cls ^ " / " ^ quote tyco)
- |> ensure_def (defgen_inst thy algbr funcgr strct) true
- ("generating instance " ^ quote cls ^ " / " ^ quote tyco) inst
+ |> tracing (fn _ => "generating instance " ^ quote class ^ " / " ^ quote tyco)
+ |> CodegenThingol.ensure_def defgen_inst true
+ ("generating instance " ^ quote class ^ " / " ^ quote tyco) inst
|> pair inst
end
-and ensure_def_const thy algbr funcgr strct (c, tys) trns =
+and ensure_def_const thy (algbr as (_, consts)) funcgr strct (c, tys) trns =
let
- fun defgen_datatypecons thy algbr funcgr strct co trns =
- case CodegenData.get_datatype_of_constr thy ((the o CodegenNames.const_rev thy) co)
- of SOME tyco =>
- trns
- |> tracing (fn _ => "trying defgen datatype constructor for " ^ quote co)
- |> ensure_def_tyco thy algbr funcgr strct tyco
- |-> (fn _ => succeed Bot)
- | _ =>
- trns
- |> fail ("Not a datatype constructor: "
- ^ (quote o CodegenConsts.string_of_const thy) (c, tys));
- fun defgen_clsmem thy algbr funcgr strct m trns =
- case AxClass.class_of_param thy ((fst o the o CodegenNames.const_rev thy) m)
- of SOME class =>
- trns
- |> tracing (fn _ => "trying defgen class operation for " ^ quote m)
- |> ensure_def_class thy algbr funcgr strct class
- |-> (fn _ => succeed Bot)
- | _ =>
- trns |> fail ("No class found for " ^ (quote o CodegenConsts.string_of_const thy) (c, tys))
- fun defgen_funs thy (algbr as (_, consts)) funcgr strct c' trns =
- case CodegenFuncgr.get_funcs funcgr ((the o CodegenNames.const_rev thy) c')
+ val c' = CodegenNames.const thy (c, tys);
+ fun defgen_datatypecons trns =
+ trns
+ |> ensure_def_tyco thy algbr funcgr strct
+ ((the o CodegenData.get_datatype_of_constr thy) (c, tys))
+ |-> (fn _ => succeed CodegenThingol.Bot);
+ fun defgen_classop trns =
+ trns
+ |> ensure_def_class thy algbr funcgr strct ((the o AxClass.class_of_param thy) c)
+ |-> (fn _ => succeed CodegenThingol.Bot);
+ fun defgen_fun trns =
+ case CodegenFuncgr.get_funcs funcgr (c, tys)
of eq_thms as eq_thm :: _ =>
let
val msg = cat_lines ("generating code for theorems " :: map string_of_thm eq_thms);
@@ -304,44 +253,42 @@
||>> exprgen_term thy algbr funcgr strct rhs;
in
trns
- |> message msg (fn trns => trns
+ |> CodegenThingol.message msg (fn trns => trns
|> fold_map (exprgen_eq o dest_eqthm) eq_thms
||>> fold_map (exprgen_tyvar_sort thy algbr funcgr strct) vs
||>> exprgen_type thy algbr funcgr strct ty
- |-> (fn ((eqs, vs), ty) => succeed (Fun (eqs, (vs, ty)))))
+ |-> (fn ((eqs, vs), ty) => succeed (CodegenThingol.Fun (eqs, (vs, ty)))))
end
| [] =>
trns
|> fail ("No defining equations found for "
^ (quote o CodegenConsts.string_of_const thy) (c, tys));
- fun get_defgen funcgr strct idf strict =
- if CodegenNames.has_nsp nsp_fun idf
- then defgen_funs thy algbr funcgr strct strict
- else if CodegenNames.has_nsp nsp_classop idf
- then defgen_clsmem thy algbr funcgr strct strict
- else if CodegenNames.has_nsp nsp_dtco idf
- then defgen_datatypecons thy algbr funcgr strct strict
- else error ("Illegal shallow name space for constant: " ^ quote idf);
- val idf = CodegenNames.const thy (c, tys);
- val strict = check_strict (CodegenSerializer.const_has_serialization thy) idf strct;
+ val defgen =
+ if CodegenNames.has_nsp CodegenNames.nsp_fun c'
+ then defgen_fun
+ else if CodegenNames.has_nsp CodegenNames.nsp_classop c'
+ then defgen_classop
+ else if CodegenNames.has_nsp CodegenNames.nsp_dtco c'
+ then defgen_datatypecons
+ else error ("Illegal shallow name space for constant: " ^ quote c');
+ val strict = check_strict (CodegenSerializer.const_has_serialization thy) c' strct;
in
trns
|> tracing (fn _ => "generating constant "
^ (quote o CodegenConsts.string_of_const thy) (c, tys))
- |> ensure_def (get_defgen funcgr strct idf) strict ("generating constant "
- ^ CodegenConsts.string_of_const thy (c, tys)) idf
- |> pair idf
+ |> CodegenThingol.ensure_def defgen strict ("generating constant "
+ ^ CodegenConsts.string_of_const thy (c, tys)) c'
+ |> pair c'
end
-and exprgen_term thy algbr funcgr strct (Const (f, ty)) trns =
+and exprgen_term thy algbr funcgr strct (Const (c, ty)) trns =
trns
- |> appgen thy algbr funcgr strct ((f, ty), [])
- |-> (fn e => pair e)
+ |> select_appgen thy algbr funcgr strct ((c, ty), [])
| exprgen_term thy algbr funcgr strct (Var _) trns =
error "Var encountered in term during code generation"
| exprgen_term thy algbr funcgr strct (Free (v, ty)) trns =
trns
|> exprgen_type thy algbr funcgr strct ty
- |-> (fn ty => pair (IVar v))
+ |-> (fn _ => pair (IVar v))
| exprgen_term thy algbr funcgr strct (Abs (raw_v, ty, raw_t)) trns =
let
val (v, t) = Syntax.variant_abs (CodegenNames.purify_var raw_v, ty, raw_t);
@@ -349,54 +296,51 @@
trns
|> exprgen_type thy algbr funcgr strct ty
||>> exprgen_term thy algbr funcgr strct t
- |-> (fn (ty, e) => pair ((v, ty) `|-> e))
+ |-> (fn (ty, t) => pair ((v, ty) `|-> t))
end
- | exprgen_term thy algbr funcgr strct (t as t1 $ t2) trns =
- let
- val (t', ts) = strip_comb t
- in case t'
- of Const (f, ty) =>
+ | exprgen_term thy algbr funcgr strct (t as _ $ _) trns =
+ case strip_comb t
+ of (Const (c, ty), ts) =>
trns
- |> appgen thy algbr funcgr strct ((f, ty), ts)
- |-> (fn e => pair e)
- | _ =>
+ |> select_appgen thy algbr funcgr strct ((c, ty), ts)
+ |-> (fn t => pair t)
+ | (t', ts) =>
trns
|> exprgen_term thy algbr funcgr strct t'
||>> fold_map (exprgen_term thy algbr funcgr strct) ts
- |-> (fn (e, es) => pair (e `$$ es))
- end
+ |-> (fn (t, ts) => pair (t `$$ ts))
and appgen_default thy algbr funcgr strct ((c, ty), ts) trns =
trns
|> ensure_def_const thy algbr funcgr strct (CodegenConsts.norm_of_typ thy (c, ty))
||>> exprgen_type thy algbr funcgr strct ty
||>> exprgen_typinst_const thy algbr funcgr strct (c, ty)
||>> fold_map (exprgen_term thy algbr funcgr strct) ts
- |-> (fn (((c, ty), ls), es) =>
- pair (IConst (c, (ls, ty)) `$$ es))
-and appgen thy algbr funcgr strct ((f, ty), ts) trns =
- case Symtab.lookup (CodegenPackageData.get thy) f
- of SOME (i, (ag, _)) =>
+ |-> (fn (((c, ty), iss), ts) =>
+ pair (IConst (c, (iss, ty)) `$$ ts))
+and select_appgen thy algbr funcgr strct ((c, ty), ts) trns =
+ case Symtab.lookup (CodegenPackageData.get thy) c
+ of SOME (i, (appgen, _)) =>
if length ts < i then
let
val tys = Library.take (i - length ts, ((fst o strip_type) ty));
- val vs = Name.names (Name.declare f Name.context) "a" tys;
+ val vs = Name.names (Name.declare c Name.context) "a" tys;
in
trns
|> fold_map (exprgen_type thy algbr funcgr strct) tys
- ||>> ag thy algbr funcgr strct ((f, ty), ts @ map Free vs)
- |-> (fn (tys, e) => pair (map2 (fn (v, _) => pair v) vs tys `|--> e))
+ ||>> appgen thy algbr funcgr strct ((c, ty), ts @ map Free vs)
+ |-> (fn (tys, t) => pair (map2 (fn (v, _) => pair v) vs tys `|--> t))
end
else if length ts > i then
trns
- |> ag thy algbr funcgr strct ((f, ty), Library.take (i, ts))
+ |> appgen thy algbr funcgr strct ((c, ty), Library.take (i, ts))
||>> fold_map (exprgen_term thy algbr funcgr strct) (Library.drop (i, ts))
- |-> (fn (e, es) => pair (e `$$ es))
+ |-> (fn (t, ts) => pair (t `$$ ts))
else
trns
- |> ag thy algbr funcgr strct ((f, ty), ts)
+ |> appgen thy algbr funcgr strct ((c, ty), ts)
| NONE =>
trns
- |> appgen_default thy algbr funcgr strct ((f, ty), ts);
+ |> appgen_default thy algbr funcgr strct ((c, ty), ts);
(* entrance points into extraction kernel *)
@@ -425,7 +369,7 @@
of SOME i =>
trns
|> appgen_default thy algbr funcgr strct app
- |-> (fn e => pair (CodegenThingol.INum (i, e)))
+ |-> (fn t => pair (CodegenThingol.INum (i, t)))
| NONE =>
trns
|> appgen_default thy algbr funcgr strct app;
@@ -436,7 +380,7 @@
trns
|> exprgen_type thy algbr funcgr strct ty
||>> appgen_default thy algbr funcgr strct app
- |-> (fn (_, e0) => pair (IChar (chr i, e0)))
+ |-> (fn (_, t0) => pair (IChar (chr i, t0)))
| NONE =>
trns
|> appgen_default thy algbr funcgr strct app;
@@ -489,7 +433,7 @@
(CodegenFuncgr.get_func_typs funcgr)
val algbr = (algebr, consttab);
in
- Code.change_yield thy (start_transact init (gen thy algbr funcgr
+ Code.change_yield thy (CodegenThingol.start_transact init (gen thy algbr funcgr
(true, targets) it))
|> (fn (x, modl) => x)
end;
@@ -544,15 +488,16 @@
val targets = case map fst seris
of [] => NONE
| xs => SOME xs;
- val seris' = map_filter (fn (target, SOME seri) => SOME (target, seri) | _ => NONE) seris;
+ val seris' = map_filter (fn (target, args as _ :: _) =>
+ SOME (CodegenSerializer.get_serializer thy (target, args)) | _ => NONE) seris;
fun generate' thy = case cs
of [] => []
| _ =>
generate thy (cs, []) targets NONE (fold_map oooo ensure_def_const') cs;
- fun serialize' [] code (_, seri) =
- seri thy NONE code
- | serialize' cs code (_, seri) =
- seri thy (SOME cs) code;
+ fun serialize' [] code seri =
+ seri NONE code
+ | serialize' cs code seri =
+ seri (SOME cs) code;
val cs = generate' thy;
val code = Code.get thy;
in
@@ -565,15 +510,13 @@
fun reader_const thy rhss target dep =
generate thy rhss (SOME [target]) (SOME dep) (fold_map oooo exprgen_term');
-val parse_target = P.name >> tap CodegenSerializer.check_serializer;
-
fun zip_list (x::xs) f g =
f x #-> (fn y => fold_map (fn x => g |-- f x >> pair x) xs
#-> (fn xys => pair ((x, y) :: xys)));
fun parse_multi_syntax parse_thing parse_syntax =
P.and_list1 parse_thing
- #-> (fn things => Scan.repeat1 (P.$$$ "(" |-- parse_target :--
+ #-> (fn things => Scan.repeat1 (P.$$$ "(" |-- P.name :--
(fn target => zip_list things (parse_syntax target)
(P.$$$ "and")) --| P.$$$ ")"))
@@ -589,7 +532,7 @@
OuterSyntax.improper_command codeK "generate and serialize executable code for constants" K.diag (
Scan.repeat P.term
-- Scan.repeat (P.$$$ "(" |--
- P.name :-- (fn target => (CodegenSerializer.parse_serializer target >> SOME) || pair NONE)
+ P.name -- P.arguments
--| P.$$$ ")")
>> (fn (raw_cs, seris) => Toplevel.keep (code raw_cs seris o Toplevel.theory_of))
);
--- a/src/Pure/Tools/codegen_serializer.ML Sat Oct 07 02:47:33 2006 +0200
+++ b/src/Pure/Tools/codegen_serializer.ML Sat Oct 07 07:41:56 2006 +0200
@@ -9,22 +9,14 @@
signature CODEGEN_SERIALIZER =
sig
include BASIC_CODEGEN_THINGOL;
- val parse_serializer: string
- -> OuterParse.token list
- -> (theory -> string list option -> CodegenThingol.module -> unit)
- * OuterParse.token list
+ val get_serializer: theory -> string * Args.T list
+ -> string list option -> CodegenThingol.code -> unit;
val eval_verbose: bool ref;
val eval_term: theory ->
- (string * 'a option ref) * CodegenThingol.iterm -> CodegenThingol.module
+ (string * 'a option ref) * CodegenThingol.iterm -> CodegenThingol.code
-> 'a;
- val mk_flat_ml_resolver: string list -> string -> string;
- val ml_fun_datatype:
- theory -> (string -> string)
- -> ((string * ((iterm list * iterm) list * CodegenThingol.typscheme)) list -> Pretty.T)
- * ((string * ((vname * sort) list * (string * itype list) list)) list -> Pretty.T);
val const_has_serialization: theory -> string list -> string -> bool;
val tyco_has_serialization: theory -> string list -> string -> bool;
- val check_serializer: string -> unit;
val add_syntax_class:
string -> string -> string * (string * string) list -> theory -> theory;
val add_syntax_inst: string -> (string * string) -> theory -> theory;
@@ -52,6 +44,12 @@
val add_pretty_ml_string: string -> string -> string -> string
-> (string -> string) -> (string -> string) -> string -> theory -> theory;
val add_undefined: string -> string -> string -> theory -> theory;
+
+ type fixity;
+ type serializer;
+ val add_serializer : string * serializer -> theory -> theory;
+ val ml_from_thingol: serializer;
+ val hs_from_thingol: serializer;
end;
structure CodegenSerializer: CODEGEN_SERIALIZER =
@@ -60,7 +58,9 @@
open BasicCodegenThingol;
val tracing = CodegenThingol.tracing;
-(** precedences **)
+(** syntax **)
+
+(* basics *)
datatype lrx = L | R | X;
@@ -95,9 +95,9 @@
fun brackify_infix infx fxy_ctxt ps =
gen_brackify (eval_fxy (INFX infx) fxy_ctxt) (Pretty.breaks ps);
-fun from_app mk_app from_expr const_syntax fxy (const as (c, (_, ty)), es) =
+fun mk_app mk_app' from_expr const_syntax fxy (const as (c, (_, ty)), es) =
case const_syntax c
- of NONE => brackify fxy (mk_app c es)
+ of NONE => brackify fxy (mk_app' c es)
| SOME (i, pr) =>
let
val k = if i < 0 then (length o fst o CodegenThingol.unfold_fun) ty else i
@@ -107,81 +107,17 @@
else from_expr fxy (CodegenThingol.eta_expand (const, es) i)
end;
-
-(** user-defined syntax **)
-
-(* theory data *)
+val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode;
-type target_data = {
- syntax_class: ((string * (string -> string option)) * stamp) Symtab.table,
- syntax_inst: unit Symtab.table,
- syntax_tyco: (itype pretty_syntax * stamp) Symtab.table,
- syntax_const: (iterm pretty_syntax * stamp) Symtab.table
-};
-
-fun merge_target_data
- ({ syntax_class = syntax_class1, syntax_inst = syntax_inst1,
- syntax_tyco = syntax_tyco1, syntax_const = syntax_const1 },
- { syntax_class = syntax_class2, syntax_inst = syntax_inst2,
- syntax_tyco = syntax_tyco2, syntax_const = syntax_const2 }) =
- { syntax_class = Symtab.merge (eq_snd (op =)) (syntax_class1, syntax_class2),
- syntax_inst = Symtab.merge (op =) (syntax_inst1, syntax_inst2),
- syntax_tyco = Symtab.merge (eq_snd (op =)) (syntax_tyco1, syntax_tyco2),
- syntax_const = Symtab.merge (eq_snd (op =)) (syntax_const1, syntax_const2) } : target_data;
-structure CodegenSerializerData = TheoryDataFun
-(struct
- val name = "Pure/codegen_serializer";
- type T = target_data Symtab.table;
- val empty =
- Symtab.empty
- |> fold (fn target =>
- Symtab.update (target,
- { syntax_class = Symtab.empty, syntax_inst = Symtab.empty,
- syntax_tyco = Symtab.empty, syntax_const = Symtab.empty })
- ) ["SML", "Haskell"] : T;
- val copy = I;
- val extend = I;
- fun merge _ = Symtab.join (K merge_target_data);
- fun print _ _ = ();
-end);
+(* user-defined syntax *)
-fun has_serialization f thy targets name =
- forall (
- is_some o (fn tab => Symtab.lookup tab name) o f o the
- o (Symtab.lookup ((CodegenSerializerData.get) thy))
- ) targets;
-
-val tyco_has_serialization = has_serialization #syntax_tyco;
-val const_has_serialization = has_serialization #syntax_const;
-
-fun serialize thy seri target cs =
- let
- val data = CodegenSerializerData.get thy;
- val target_data =
- (the oo Symtab.lookup) data target;
- val syntax_class = #syntax_class target_data;
- val syntax_inst = #syntax_inst target_data;
- val syntax_tyco = #syntax_tyco target_data;
- val syntax_const = #syntax_const target_data;
- fun fun_of syntax = (Option.map fst oo Symtab.lookup) syntax;
- in
- seri (fun_of syntax_class, fun_of syntax_tyco, fun_of syntax_const)
- (Symtab.keys syntax_class @ Symtab.keys syntax_inst
- @ Symtab.keys syntax_tyco @ Symtab.keys syntax_const, cs)
- end;
-
-val _ = Context.add_setup CodegenSerializerData.init;
+val str = setmp print_mode [] Pretty.str;
val (atomK, infixK, infixlK, infixrK) =
("target_atom", "infix", "infixl", "infixr");
val _ = OuterSyntax.add_keywords [atomK, infixK, infixlK, infixrK];
-
-(* syntax parser *)
-
-val str = setmp print_mode [] Pretty.str;
-
datatype 'a mixfix =
Arg of fixity
| Pretty of Pretty.T
@@ -271,130 +207,7 @@
end;
-
-(** generic abstract serializer **)
-
-val nsp_module = CodegenNames.nsp_module;
-val nsp_class = CodegenNames.nsp_class;
-val nsp_tyco = CodegenNames.nsp_tyco;
-val nsp_inst = CodegenNames.nsp_inst;
-val nsp_fun = CodegenNames.nsp_fun;
-val nsp_classop = CodegenNames.nsp_classop;
-val nsp_dtco = CodegenNames.nsp_dtco;
-val nsp_eval = CodegenNames.nsp_eval;
-
-fun abstract_serializer (target, nspgrp) name_root (from_defs, from_module, validator, postproc)
- postprocess (class_syntax, tyco_syntax, const_syntax)
- (drop: string list, select) code =
- let
- fun from_module' resolv imps ((name_qual, name), defs) =
- from_module resolv imps ((name_qual, name), defs)
- |> postprocess (resolv name_qual);
- in
- code
- |> tracing (fn _ => "dropping shadowed defintions...")
- |> CodegenThingol.delete_garbage drop
- |> tracing (fn _ => "projecting...")
- |> (if is_some select then (CodegenThingol.project_module o the) select else I)
- |> tracing (fn _ => "serializing...")
- |> CodegenThingol.serialize (from_defs (class_syntax, tyco_syntax, const_syntax))
- from_module' validator postproc nspgrp name_root
- |> K ()
- end;
-
-fun abstract_validator keywords name =
- let
- fun replace_invalid c = (*FIXME*)
- if Symbol.is_ascii_letter c orelse Symbol.is_ascii_digit c orelse c = "'"
- andalso not (NameSpace.separator = c)
- then c
- else "_"
- fun suffix_it name=
- name
- |> member (op =) keywords ? 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;
-
-fun write_file mkdir path p = (
- if mkdir
- then
- File.mkdir (Path.dir path)
- else ();
- File.write path (Pretty.output p ^ "\n");
- p
- );
-
-fun mk_module_file postprocess_module ext path name p =
- let
- val prfx = Path.dir path;
- val name' = case name
- of "" => Path.base path
- | _ => (Path.ext ext o Path.unpack o implode o separate "/" o NameSpace.unpack) name;
- in
- p
- |> write_file true (Path.append prfx name')
- |> postprocess_module name
- end;
-
-fun parse_single_file serializer =
- OuterParse.path
- >> (fn path => serializer
- (fn "" => write_file false path #> K NONE
- | _ => SOME));
-
-fun parse_multi_file postprocess_module ext serializer =
- OuterParse.path
- >> (fn path => (serializer o mk_module_file postprocess_module ext) path);
-
-fun parse_internal serializer =
- OuterParse.name
- >> (fn "-" => serializer
- (fn "" => (fn p => (use_text Context.ml_output false (Pretty.output p); NONE))
- | _ => SOME)
- | _ => Scan.fail ());
-
-fun parse_stdout serializer =
- OuterParse.name
- >> (fn "_" => serializer
- (fn "" => (fn p => (Pretty.writeln p; NONE))
- | _ => SOME)
- | _ => Scan.fail ());
-
-fun constructive_fun (name, (eqs, ty)) =
- let
- val is_cons = CodegenNames.has_nsp CodegenNames.nsp_dtco;
- fun check_eq (eq as (lhs, rhs)) =
- if forall (CodegenThingol.is_pat is_cons) lhs
- then SOME eq
- else (warning ("In function " ^ quote name ^ ", throwing away one "
- ^ "non-executable function clause"); NONE)
- in case map_filter check_eq eqs
- of [] => error ("In function " ^ quote name ^ ", no "
- ^ "executable function clauses found")
- | eqs => (name, (eqs, ty))
- end;
-
-fun make_ctxt names = (fold (fn name => Symtab.update_new (name, name)) names Symtab.empty,
- Name.make_context names);
-
-fun intro_ctxt names (namemap, namectxt) =
- let
- val (names', namectxt') = Name.variants names namectxt;
- val namemap' = fold2 (curry Symtab.update) names names' namemap;
- in (namemap', namectxt') end;
-
-fun lookup_ctxt (namemap, _) name = case Symtab.lookup namemap name
- of SOME name' => name'
- | NONE => error ("invalid name in context: " ^ quote name);
-
-
-
-(** generic list and string serializers **)
+(* list and string serializer *)
fun implode_list c_nil c_cons e =
let
@@ -445,441 +258,934 @@
in (2, pretty) end;
+(* variable name contexts *)
-(** ML serializer **)
-
-local
+(*FIXME could name.ML do th whole job?*)
+fun make_vars names = (fold (fn name => Symtab.update_new (name, name)) names Symtab.empty,
+ Name.make_context names);
-val reserved_ml' = [
- "bool", "int", "list", "unit", "option", "true", "false", "not", "NONE", "SOME",
- "o", "string", "char", "String", "Term"
-];
+fun intro_vars names (namemap, namectxt) =
+ let
+ val (names', namectxt') = Name.variants names namectxt;
+ val namemap' = fold2 (curry Symtab.update) names names' namemap;
+ in (namemap', namectxt') end;
-fun ml_expr_seri (tyco_syntax, const_syntax) resolv =
+fun lookup_var (namemap, _) name = case Symtab.lookup namemap name
+ of SOME name' => name'
+ | NONE => error ("invalid name in context: " ^ quote name);
+
+fun constructive_fun (name, (eqs, ty)) =
let
val is_cons = CodegenNames.has_nsp CodegenNames.nsp_dtco;
- fun first_upper s =
- implode (nth_map 0 (Symbol.to_ascii_upper) (explode s));
- fun ml_from_dictvar v =
+ fun is_pat (IConst (c, _)) = is_cons c
+ | is_pat (IVar _) = true
+ | is_pat (t1 `$ t2) =
+ is_pat t1 andalso is_pat t2
+ | is_pat (INum _) = true
+ | is_pat (IChar _) = true
+ | is_pat _ = false;
+ fun check_eq (eq as (lhs, rhs)) =
+ if forall is_pat lhs
+ then SOME eq
+ else (warning ("In function " ^ quote name ^ ", throwing away one "
+ ^ "non-executable function clause"); NONE)
+ in case map_filter check_eq eqs
+ of [] => error ("In function " ^ quote name ^ ", no "
+ ^ "executable function clauses found")
+ | eqs => (name, (eqs, ty))
+ end;
+
+
+(** SML serializer **)
+
+datatype ml_def =
+ MLFuns of (string * ((iterm list * iterm) list * typscheme)) list
+ | MLDatas of (string * ((vname * sort) list * (string * itype list) list)) list
+ | MLClass of string * (class list * (vname * (string * itype) list))
+ | MLClassinst of string * ((class * (string * (vname * sort) list))
+ * ((class * (string * inst list list)) list
+ * (string * iterm) list));
+
+fun pr_sml_def tyco_syntax const_syntax keyword_vars deresolv ml_def =
+ let
+ val is_cons = CodegenNames.has_nsp CodegenNames.nsp_dtco;
+ fun dictvar v =
first_upper v ^ "_";
- val ml_from_label =
- str o translate_string (fn "." => "__" | c => c);
- fun ml_from_tyvar (v, []) =
+ val label = translate_string (fn "." => "__" | c => c)
+ o NameSpace.pack o op @ o apsnd single o apfst (fst o split_last) o split_last o NameSpace.unpack;
+ fun pr_tyvar (v, []) =
str "()"
- | ml_from_tyvar (v, sort) =
+ | pr_tyvar (v, sort) =
let
- fun mk_class class =
- str (prefix "'" v ^ " " ^ resolv class);
+ fun pr_class class =
+ str ("'" ^ v ^ " " ^ deresolv class);
in
Pretty.block [
str "(",
- (str o ml_from_dictvar) v,
+ (str o dictvar) v,
str ":",
case sort
- of [class] => mk_class class
- | _ => Pretty.enum " *" "" "" (map mk_class sort),
- str ")"
+ of [class] => pr_class class
+ | _ => Pretty.enum " *" "" "" (map pr_class sort),
+ str ")"
]
end;
- fun ml_from_insts fxy lss =
+ fun pr_insts fxy iys =
let
- fun from_label l =
- Pretty.block [str "#",
- if (is_some o Int.fromString) l then str l
- else ml_from_label l
- ];
- fun from_lookup fxy [] p =
+ fun pr_proj s = str ("#" ^ s);
+ fun pr_lookup [] p =
p
- | from_lookup fxy [l] p =
- brackify fxy [
- from_label l,
- p
- ]
- | from_lookup fxy ls p =
- brackify fxy [
- Pretty.enum " o" "(" ")" (map from_label ls),
- p
- ];
- fun from_inst fxy (Instance (inst, lss)) =
+ | pr_lookup [p'] p =
+ brackify BR [p', p]
+ | pr_lookup (ps as _ :: _) p =
+ brackify BR [Pretty.enum " o" "(" ")" ps, p];
+ fun pr_inst fxy (Instance (inst, iss)) =
brackify fxy (
- (str o resolv) inst
- :: map (ml_from_insts BR) lss
+ (str o deresolv) inst
+ :: map (pr_insts BR) iss
)
- | from_inst fxy (Context (classes, (v, ~1))) =
- from_lookup BR classes
- ((str o ml_from_dictvar) v)
- | from_inst fxy (Context (classes, (v, i))) =
- from_lookup BR (classes @ [string_of_int (i+1)])
- ((str o ml_from_dictvar) v)
- in case lss
+ | pr_inst fxy (Context (classes, (v, i))) =
+ pr_lookup (map (pr_proj o label) classes
+ @ (if i = ~1 then [] else [(pr_proj o string_of_int) (i+1)])
+ ) ((str o dictvar) v);
+ in case iys
of [] => str "()"
- | [ls] => from_inst fxy ls
- | lss => (Pretty.list "(" ")" o map (from_inst NOBR)) lss
+ | [iy] => pr_inst fxy iy
+ | _ :: _ => (Pretty.list "(" ")" o map (pr_inst NOBR)) iys
end;
- fun ml_from_tycoexpr fxy (tyco, tys) =
+ fun pr_tycoexpr fxy (tyco, tys) =
let
- val tyco' = (str o resolv) tyco
- in case map (ml_from_type BR) tys
+ val tyco' = (str o deresolv) tyco
+ in case map (pr_typ BR) tys
of [] => tyco'
| [p] => Pretty.block [p, Pretty.brk 1, tyco']
| (ps as _::_) => Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, tyco']
end
- and ml_from_type fxy (tycoexpr as tyco `%% tys) =
+ and pr_typ fxy (tyco `%% tys) =
(case tyco_syntax tyco
- of NONE => ml_from_tycoexpr fxy (tyco, tys)
+ of NONE => pr_tycoexpr fxy (tyco, tys)
| SOME (i, pr) =>
if not (i = length tys)
then error ("Number of argument mismatch in customary serialization: "
^ (string_of_int o length) tys ^ " given, "
^ string_of_int i ^ " expected")
- else pr fxy ml_from_type tys)
- | ml_from_type fxy (t1 `-> t2) =
- let
- val brackify = gen_brackify
- (case fxy
- of BR => false
- | _ => eval_fxy (INFX (1, R)) fxy) o Pretty.breaks;
- in
- brackify [
- ml_from_type (INFX (1, X)) t1,
+ else pr fxy pr_typ tys)
+ | pr_typ fxy (t1 `-> t2) =
+ (gen_brackify (case fxy of BR => false | _ => eval_fxy (INFX (1, R)) fxy)
+ o Pretty.breaks) [
+ pr_typ (INFX (1, X)) t1,
str "->",
- ml_from_type (INFX (1, R)) t2
+ pr_typ (INFX (1, R)) t2
]
- end
- | ml_from_type fxy (ITyVar v) =
+ | pr_typ fxy (ITyVar v) =
str ("'" ^ v);
- fun ml_from_expr var_ctxt fxy (e as IConst x) =
- ml_from_app var_ctxt fxy (x, [])
- | ml_from_expr var_ctxt fxy (IVar v) =
- str (lookup_ctxt var_ctxt v)
- | ml_from_expr var_ctxt fxy (e as e1 `$ e2) =
- (case CodegenThingol.unfold_const_app e
- of SOME x => ml_from_app var_ctxt fxy x
+ fun pr_term vars fxy (IConst c) =
+ pr_app vars fxy (c, [])
+ | pr_term vars fxy (IVar v) =
+ str (lookup_var vars v)
+ | pr_term vars fxy (t as t1 `$ t2) =
+ (case CodegenThingol.unfold_const_app t
+ of SOME c_ts => pr_app vars fxy c_ts
| NONE =>
- brackify fxy [
- ml_from_expr var_ctxt NOBR e1,
- ml_from_expr var_ctxt BR e2
- ])
- | ml_from_expr var_ctxt fxy (e as _ `|-> _) =
+ brackify fxy [pr_term vars NOBR t1, pr_term vars BR t2 ])
+ | pr_term vars fxy (t as _ `|-> _) =
let
- val (es, e') = CodegenThingol.unfold_abs e;
- val vs = fold CodegenThingol.add_varnames (map fst es) [];
- val var_ctxt' = intro_ctxt vs var_ctxt;
- fun mk_abs (e, ty) = (Pretty.block o Pretty.breaks) [
- str "fn",
- ml_from_expr var_ctxt' NOBR e,
- str "=>"
- ];
- in brackify BR (map mk_abs es @ [ml_from_expr var_ctxt' NOBR e']) end
- | ml_from_expr var_ctxt fxy (INum (n, _)) =
- brackify BR [
- (str o IntInf.toString) n,
- str ":",
- str "IntInf.int"
- ]
- | ml_from_expr var_ctxt _ (IChar (c, _)) =
+ val (ts, t') = CodegenThingol.unfold_abs t;
+ val vs = fold (CodegenThingol.fold_varnames (insert (op =)) o fst) ts [];
+ val vars' = intro_vars vs vars;
+ fun mk_abs (t, ty) = (Pretty.block o Pretty.breaks)
+ [str "fn", pr_term vars' NOBR t, str "=>"];
+ in brackify BR (map mk_abs ts @ [pr_term vars' NOBR t']) end
+ | pr_term vars fxy (INum (n, _)) =
+ brackify BR [(str o IntInf.toString) n, str ":", str "IntInf.int"]
+ | pr_term vars _ (IChar (c, _)) =
(str o prefix "#" o quote)
(let val i = ord c
in if i < 32
then prefix "\\" (string_of_int i)
else c
end)
- | ml_from_expr var_ctxt fxy (e as ICase ((_, [_]), _)) =
+ | pr_term vars fxy (t as ICase ((_, [_]), _)) =
let
- val (ves, be) = CodegenThingol.unfold_let e;
- fun mk_val ((ve, vty), se) var_ctxt =
+ val (ts, t) = CodegenThingol.unfold_let t;
+ fun mk ((p, _), t) vars =
let
- val vs = CodegenThingol.add_varnames ve [];
- val var_ctxt' = intro_ctxt vs var_ctxt;
+ val vs = CodegenThingol.fold_varnames (insert (op =)) p [];
+ val vars' = intro_vars vs vars;
in
(Pretty.block [
(Pretty.block o Pretty.breaks) [
str "val",
- ml_from_expr var_ctxt' NOBR ve,
+ pr_term vars' NOBR p,
str "=",
- ml_from_expr var_ctxt NOBR se
+ pr_term vars NOBR t
],
str ";"
- ], var_ctxt')
+ ], vars')
end
- val (binds, var_ctxt') = fold_map mk_val ves var_ctxt;
- in Pretty.chunks [
- [str ("let"), Pretty.fbrk, binds |> Pretty.chunks] |> Pretty.block,
- [str ("in"), Pretty.fbrk, ml_from_expr var_ctxt' NOBR be] |> Pretty.block,
- str ("end")
- ] end
- | ml_from_expr var_ctxt fxy (ICase (((de, dty), bse::bses), _)) =
+ val (binds, vars') = fold_map mk ts vars;
+ in
+ Pretty.chunks [
+ [str ("let"), Pretty.fbrk, binds |> Pretty.chunks] |> Pretty.block,
+ [str ("in"), Pretty.fbrk, pr_term vars' NOBR t] |> Pretty.block,
+ str ("end")
+ ] end
+ | pr_term vars fxy (ICase (((td, ty), b::bs), _)) =
let
- fun mk_clause definer (se, be) =
+ fun pr definer (p, t) =
let
- val vs = CodegenThingol.add_varnames se [];
- val var_ctxt' = intro_ctxt vs var_ctxt;
+ val vs = CodegenThingol.fold_varnames (insert (op =)) p [];
+ val vars' = intro_vars vs vars;
in
(Pretty.block o Pretty.breaks) [
str definer,
- ml_from_expr var_ctxt' NOBR se,
+ pr_term vars' NOBR p,
str "=>",
- ml_from_expr var_ctxt' NOBR be
+ pr_term vars' NOBR t
]
- end
- in brackify fxy (
- str "(case"
- :: ml_from_expr var_ctxt NOBR de
- :: mk_clause "of" bse
- :: map (mk_clause "|") bses
- @ [str ")"]
- ) end
- | ml_from_expr var_ctxt _ e =
- error ("Dubious expression: " ^ (Pretty.output o CodegenThingol.pretty_iterm) e)
- and ml_mk_app var_ctxt f es =
- if is_cons f andalso length es > 1 then
- [(str o resolv) f, Pretty.enum "," "(" ")" (map (ml_from_expr var_ctxt BR) es)]
+ end;
+ in
+ (Pretty.enclose "(" ")" o single o brackify fxy) (
+ str "case"
+ :: pr_term vars NOBR td
+ :: pr "of" b
+ :: map (pr "|") bs
+ )
+ end
+ and pr_app' vars c ts =
+ let
+ val p = (str o deresolv) c;
+ val ps = map (pr_term vars BR) ts;
+ in if is_cons c andalso length ts > 1 then
+ [p, Pretty.enum "," "(" ")" ps]
else
- (str o resolv) f :: map (ml_from_expr var_ctxt BR) es
- and ml_from_app var_ctxt fxy (app_expr as ((c, (lss, ty)), es)) =
- case if is_cons c then [] else (map (ml_from_insts BR) o filter_out null) lss
+ p :: ps
+ end
+ and pr_app vars fxy (app as ((c, (iss, ty)), ts)) =
+ case if is_cons c then [] else (map (pr_insts BR) o filter_out null) iss
of [] =>
- from_app (ml_mk_app var_ctxt) (ml_from_expr var_ctxt) const_syntax fxy app_expr
- | lss =>
+ mk_app (pr_app' vars) (pr_term vars) const_syntax fxy app
+ | ps =>
if (is_none o const_syntax) c then
- brackify fxy (
- (str o resolv) c
- :: (lss
- @ map (ml_from_expr var_ctxt BR) es)
- )
- else error ("Can't apply user defined serialization for function expecting dicitonaries: " ^ quote c)
- in (ml_from_dictvar, ml_from_label, ml_from_tyvar, ml_from_insts,
- ml_from_tycoexpr, ml_from_type, ml_from_expr) end;
+ brackify fxy ((str o deresolv) c :: (ps @ map (pr_term vars BR) ts))
+ else
+ error ("Cannot apply user defined serialization for function expecting dictionaries: " ^ quote c)
+ fun eta_expand_poly_fun (funn as (_, (_::_, _))) =
+ funn
+ | eta_expand_poly_fun (funn as (_, ([_], ([], _)))) =
+ funn
+ | eta_expand_poly_fun (funn as (_, ([(_::_, _)], _))) =
+ funn
+ | eta_expand_poly_fun (funn as (_, ([(_, _ `|-> _)], _))) =
+ funn
+ | eta_expand_poly_fun (funn as (name, ([([], t)], tysm as (vs, ty)))) =
+ if (null o fst o CodegenThingol.unfold_fun) ty
+ orelse (not o null o filter_out (null o snd)) vs
+ then funn
+ else (name, ([([IVar "x"], t `$ IVar "x")], tysm));
+ fun pr_def (MLFuns raw_funns) =
+ let
+ val funns as (funn :: funns') = map (eta_expand_poly_fun o constructive_fun) raw_funns;
+ val definer =
+ let
+ fun mk [] [] = "val"
+ | mk (_::_) _ = "fun"
+ | mk [] vs = if (null o filter_out (null o snd)) vs then "val" else "fun";
+ fun chk (_, ((ts, _) :: _, (vs, _))) NONE = SOME (mk ts vs)
+ | chk (_, ((ts, _) :: _, (vs, _))) (SOME defi) =
+ if defi = mk ts vs then SOME defi
+ else error ("Mixing simultaneous vals and funs not implemented");
+ in the (fold chk funns NONE) end;
+ fun pr_funn definer (name, (eqs as eq::eqs', (raw_vs, ty))) =
+ let
+ val vs = filter_out (null o snd) raw_vs;
+ val shift = if null eqs' then I else
+ map (Pretty.block o single o Pretty.block o single);
+ fun pr_eq definer (ts, t) =
+ let
+ val consts = map_filter
+ (fn c => if (is_some o const_syntax) c
+ then NONE else (SOME o NameSpace.base o deresolv) c)
+ ((fold o CodegenThingol.fold_constnames) (insert (op =)) (t :: ts) []);
+ val vars = keyword_vars
+ |> intro_vars consts
+ |> intro_vars ((fold o CodegenThingol.fold_unbound_varnames) (insert (op =)) (t :: ts) []);
+ in
+ (Pretty.block o Pretty.breaks) (
+ [str definer, (str o deresolv) name]
+ @ (if null ts andalso null vs
+ andalso not (ty = ITyVar "_")(*for evaluation*)
+ then [str ":", pr_typ NOBR ty]
+ else
+ map pr_tyvar vs
+ @ map (pr_term vars BR) ts)
+ @ [str "=", pr_term vars NOBR t]
+ )
+ end
+ in
+ (Pretty.block o Pretty.fbreaks o shift) (
+ pr_eq definer eq
+ :: map (pr_eq "|") eqs'
+ )
+ end;
+ val (ps, p) = split_last (pr_funn definer funn :: map (pr_funn "and") funns');
+ in Pretty.chunks (ps @ [Pretty.block ([p, str ";"])]) end
+ | pr_def (MLDatas (datas as (data :: datas'))) =
+ let
+ fun pr_co (co, []) =
+ str (deresolv co)
+ | pr_co (co, tys) =
+ (Pretty.block o Pretty.breaks) [
+ str (deresolv co),
+ str "of",
+ Pretty.enum " *" "" "" (map (pr_typ (INFX (2, L))) tys)
+ ];
+ fun pr_data definer (tyco, (vs, cos)) =
+ (Pretty.block o Pretty.breaks) (
+ str definer
+ :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)
+ :: str "="
+ :: separate (str "|") (map pr_co cos)
+ );
+ val (ps, p) = split_last (pr_data "datatype" data :: map (pr_data "and") datas');
+ in Pretty.chunks (ps @ [Pretty.block ([p, str ";"])]) end
+ | pr_def (MLClass (class, (superclasses, (v, classops)))) =
+ let
+ val w = dictvar v;
+ fun pr_superclass class =
+ (Pretty.block o Pretty.breaks o map str) [
+ label class, ":", "'" ^ v, deresolv class
+ ];
+ fun pr_classop (classop, ty) =
+ (Pretty.block o Pretty.breaks) [
+ (str o suffix "_" o NameSpace.base) classop, str ":", pr_typ NOBR ty
+ ];
+ fun pr_classop_fun (classop, _) =
+ (Pretty.block o Pretty.breaks) [
+ str "fun",
+ (str o deresolv) classop,
+ Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ deresolv class)],
+ str "=",
+ str ("#" ^ (suffix "_" o NameSpace.base) classop),
+ str (w ^ ";")
+ ];
+ in
+ Pretty.chunks (
+ (Pretty.block o Pretty.breaks) [
+ str ("type '" ^ v),
+ (str o deresolv) class,
+ str "=",
+ Pretty.enum "," "{" "};" (
+ map pr_superclass superclasses @ map pr_classop classops
+ )
+ ]
+ :: map pr_classop_fun classops
+ )
+ end
+ | pr_def (MLClassinst (inst, ((class, (tyco, arity)), (superarities, classop_defs)))) =
+ let
+ fun pr_superclass (superclass, superinst_iss) =
+ (Pretty.block o Pretty.breaks) [
+ (str o label) superclass,
+ str "=",
+ pr_insts NOBR [Instance superinst_iss]
+ ];
+ fun pr_classop_def (classop, t) =
+ let
+ val consts = map_filter
+ (fn c => if (is_some o const_syntax) c
+ then NONE else (SOME o NameSpace.base o deresolv) c)
+ (CodegenThingol.fold_constnames (insert (op =)) t []);
+ val vars = keyword_vars
+ |> intro_vars consts;
+ in
+ (Pretty.block o Pretty.breaks) [
+ (str o suffix "_" o NameSpace.base) classop,
+ str "=",
+ pr_term vars NOBR t
+ ]
+ end;
+ in
+ (Pretty.block o Pretty.breaks) ([
+ str (if null arity then "val" else "fun"),
+ (str o deresolv) inst ] @
+ map pr_tyvar arity @ [
+ str "=",
+ Pretty.enum "," "{" "}" (map pr_superclass superarities @ map pr_classop_def classop_defs),
+ str ":",
+ pr_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity])
+ ])
+ end;
+ in pr_def ml_def end;
-fun ml_fun_datatype init_ctxt (tyco_syntax, const_syntax) resolv =
+
+
+(** Haskell serializer **)
+
+fun pr_haskell class_syntax tyco_syntax const_syntax keyword_vars deresolv_here deresolv def =
let
val is_cons = CodegenNames.has_nsp CodegenNames.nsp_dtco;
- val (ml_from_dictvar, ml_from_label, ml_from_tyvar, ml_from_insts, ml_from_tycoexpr, ml_from_type, ml_from_expr) =
- ml_expr_seri (tyco_syntax, const_syntax) resolv;
- fun chunk_defs ps =
- let
- val (p_init, p_last) = split_last ps
- in
- Pretty.chunks (p_init @ [Pretty.block ([p_last, str ";"])])
- end;
- fun eta_expand_poly_fun (funn as (_, (_::_, _))) =
- funn
- | eta_expand_poly_fun (funn as (eqs, tysm as (_, ty))) =
+ fun class_name class = case class_syntax class
+ of NONE => deresolv class
+ | SOME (class, _) => class;
+ fun classop_name class classop = case class_syntax class
+ of NONE => NameSpace.base classop
+ | SOME (_, classop_syntax) => case classop_syntax classop
+ of NONE => NameSpace.base classop
+ | SOME classop => classop
+ fun pr_typparms tyvars vs =
+ case maps (fn (v, sort) => map (pair v) sort) vs
+ of [] => str ""
+ | xs => Pretty.block [
+ Pretty.enum "," "(" ")" (
+ map (fn (v, class) => str
+ (class_name class ^ " " ^ lookup_var tyvars v)) xs
+ ),
+ str " => "
+ ];
+ fun pr_tycoexpr tyvars fxy (tyco, tys) =
+ brackify fxy (str tyco :: map (pr_typ tyvars BR) tys)
+ and pr_typ tyvars fxy (tycoexpr as tyco `%% tys) =
+ (case tyco_syntax tyco
+ of NONE =>
+ pr_tycoexpr tyvars fxy (deresolv tyco, tys)
+ | SOME (i, pr) =>
+ if not (i = length tys)
+ then error ("Number of argument mismatch in customary serialization: "
+ ^ (string_of_int o length) tys ^ " given, "
+ ^ string_of_int i ^ " expected")
+ else pr fxy (pr_typ tyvars) tys)
+ | pr_typ tyvars fxy (t1 `-> t2) =
+ brackify_infix (1, R) fxy [
+ pr_typ tyvars (INFX (1, X)) t1,
+ str "->",
+ pr_typ tyvars (INFX (1, R)) t2
+ ]
+ | pr_typ tyvars fxy (ITyVar v) =
+ (str o lookup_var tyvars) v;
+ fun pr_typscheme_expr tyvars (vs, tycoexpr) =
+ Pretty.block [pr_typparms tyvars vs, pr_tycoexpr tyvars NOBR tycoexpr];
+ fun pr_typscheme tyvars (vs, ty) =
+ Pretty.block [pr_typparms tyvars vs, pr_typ tyvars NOBR ty];
+ fun pr_term vars fxy (IConst c) =
+ pr_app vars fxy (c, [])
+ | pr_term vars fxy (t as (t1 `$ t2)) =
+ (case CodegenThingol.unfold_const_app t
+ of SOME app => pr_app vars fxy app
+ | _ =>
+ brackify fxy [
+ pr_term vars NOBR t1,
+ pr_term vars BR t2
+ ])
+ | pr_term vars fxy (IVar v) =
+ (str o lookup_var vars) v
+ | pr_term vars fxy (t as _ `|-> _) =
let
- fun no_eta (_::_, _) = I
- | no_eta (_, _ `|-> _) = I
- | no_eta ([], e) = K false;
- fun has_tyvars (_ `%% tys) =
- exists has_tyvars tys
- | has_tyvars (ITyVar _) =
- true
- | has_tyvars (ty1 `-> ty2) =
- has_tyvars ty1 orelse has_tyvars ty2;
- in if (null o fst o CodegenThingol.unfold_fun) ty
- orelse (not o has_tyvars) ty
- orelse fold no_eta eqs true
- then funn
- else (map (fn ([], rhs) => ([IVar "x"], rhs `$ IVar "x")) eqs, tysm)
- end;
- fun ml_from_funs (defs as def::defs_tl) =
- let
- fun mk_definer [] [] = "val"
- | mk_definer (_::_) _ = "fun"
- | mk_definer [] vs = if (null o filter_out (null o snd)) vs then "val" else "fun";
- fun check_args (_, ((pats, _)::_, (vs, _))) NONE =
- SOME (mk_definer pats vs)
- | check_args (_, ((pats, _)::_, (vs, _))) (SOME definer) =
- if mk_definer pats vs = definer
- then SOME definer
- else error ("Mixing simultaneous vals and funs not implemented");
- fun mk_fun definer (name, (eqs as eq::eq_tl, (raw_vs, ty))) =
+ val (ts, t') = CodegenThingol.unfold_abs t;
+ val vs = fold (CodegenThingol.fold_varnames (insert (op =)) o fst) ts [];
+ val vars' = intro_vars vs vars;
+ in
+ brackify BR (
+ str "\\"
+ :: map (pr_term vars' BR o fst) ts @ [
+ str "->",
+ pr_term vars' NOBR t'
+ ])
+ end
+ | pr_term vars fxy (INum (n, _)) =
+ if n > 0 then
+ (str o IntInf.toString) n
+ else
+ brackify BR [(str o Library.prefix "-" o IntInf.toString o IntInf.~) n]
+ | pr_term vars fxy (IChar (c, _)) =
+ (str o enclose "'" "'")
+ (let val i = (Char.ord o the o Char.fromString) c
+ in if i < 32
+ then Library.prefix "\\" (string_of_int i)
+ else c
+ end)
+ | pr_term vars fxy (t as ICase ((_, [_]), _)) =
let
- val vs = filter_out (null o snd) raw_vs;
- val shift = if null eq_tl then I else
- map (Pretty.block o single o Pretty.block o single);
- fun mk_eq definer (pats, expr) =
+ val (ts, t) = CodegenThingol.unfold_let t;
+ fun pr ((p, _), t) vars =
+ let
+ val vs = CodegenThingol.fold_varnames (insert (op =)) p [];
+ val vars' = intro_vars vs vars;
+ in
+ ((Pretty.block o Pretty.breaks) [
+ pr_term vars' BR p,
+ str "=",
+ pr_term vars NOBR t
+ ], vars')
+ end;
+ val (binds, vars') = fold_map pr ts vars;
+ in Pretty.chunks [
+ [str ("let"), Pretty.fbrk, binds |> Pretty.chunks] |> Pretty.block,
+ [str ("in "), pr_term vars' NOBR t] |> Pretty.block
+ ] end
+ | pr_term vars fxy (ICase (((td, _), bs), _)) =
+ let
+ fun pr (p, t) =
+ let
+ val vs = CodegenThingol.fold_varnames (insert (op =)) p [];
+ val vars' = intro_vars vs vars;
+ in
+ (Pretty.block o Pretty.breaks) [
+ pr_term vars' NOBR p,
+ str "->",
+ pr_term vars' NOBR t
+ ]
+ end
+ in
+ (Pretty.enclose "(" ")" o Pretty.breaks) [
+ str "case",
+ pr_term vars NOBR td,
+ str "of",
+ (Pretty.chunks o map pr) bs
+ ]
+ end
+ and pr_app' vars c ts =
+ (str o deresolv) c :: map (pr_term vars BR) ts
+ and pr_app vars fxy =
+ mk_app (pr_app' vars) (pr_term vars) const_syntax fxy;
+ fun pr_def (name, CodegenThingol.Fun (funn as (eqs, (vs, ty)))) =
+ let
+ val tyvars = intro_vars (map fst vs) keyword_vars;
+ fun pr_eq (ts, t) =
let
val consts = map_filter
(fn c => if (is_some o const_syntax) c
- then NONE else (SOME o NameSpace.base o resolv) c) (fold CodegenThingol.add_constnames (expr :: pats) []);
- val vars = fold CodegenThingol.add_unbound_varnames (expr :: pats) [];
- val var_ctxt = init_ctxt
- |> intro_ctxt consts
- |> intro_ctxt vars;
+ then NONE else (SOME o NameSpace.base o deresolv) c)
+ ((fold o CodegenThingol.fold_constnames) (insert (op =)) (t :: ts) []);
+ val vars = keyword_vars
+ |> intro_vars consts
+ |> intro_vars ((fold o CodegenThingol.fold_unbound_varnames) (insert (op =)) (t :: ts) []);
in
(Pretty.block o Pretty.breaks) (
- [str definer, (str o resolv) name]
- @ (if null pats andalso null vs
- andalso not (ty = ITyVar "_")(*for evaluation*)
- then [str ":", ml_from_type NOBR ty]
- else
- map ml_from_tyvar vs
- @ map (ml_from_expr var_ctxt BR) pats)
- @ [str "=", ml_from_expr var_ctxt NOBR expr]
+ (str o deresolv_here) name
+ :: map (pr_term vars BR) ts
+ @ [str "=", pr_term vars NOBR t]
)
- end
+ end;
+ in
+ Pretty.chunks (
+ Pretty.block [
+ (str o suffix " ::" o deresolv_here) name,
+ Pretty.brk 1,
+ pr_typscheme tyvars (vs, ty)
+ ]
+ :: (map pr_eq o fst o snd o constructive_fun) (name, funn)
+ )
+ end |> SOME
+ | pr_def (name, CodegenThingol.Datatype (vs, [(co, [ty])])) =
+ let
+ val tyvars = intro_vars (map fst vs) keyword_vars;
in
- (Pretty.block o Pretty.fbreaks o shift) (
- mk_eq definer eq
- :: map (mk_eq "|") eq_tl
+ (Pretty.block o Pretty.breaks) [
+ str "newtype",
+ pr_typscheme_expr tyvars (vs, (deresolv_here name, map (ITyVar o fst) vs)),
+ str "=",
+ (str o deresolv_here) co,
+ pr_typ tyvars BR ty
+ ]
+ end |> SOME
+ | pr_def (name, CodegenThingol.Datatype (vs, co :: cos)) =
+ let
+ val tyvars = intro_vars (map fst vs) keyword_vars;
+ fun pr_co (co, tys) =
+ (Pretty.block o Pretty.breaks) (
+ (str o deresolv_here) co
+ :: map (pr_typ tyvars BR) tys
+ )
+ in
+ (Pretty.block o Pretty.breaks) (
+ str "data"
+ :: pr_typscheme_expr tyvars (vs, (deresolv_here name, map (ITyVar o fst) vs))
+ :: str "="
+ :: pr_co co
+ :: map ((fn p => Pretty.block [str "| ", p]) o pr_co) cos
)
- end;
- val def' :: defs' = map (apsnd eta_expand_poly_fun o constructive_fun) defs
- in
- chunk_defs (
- (mk_fun (the (fold check_args defs NONE))) def'
- :: map (mk_fun "and") defs'
- )
- end;
- fun ml_from_datatypes (defs as (def::defs_tl)) =
- let
- fun mk_cons (co, []) =
- str (resolv co)
- | mk_cons (co, tys) =
+ end |> SOME
+ | pr_def (_, CodegenThingol.Datatypecons _) =
+ NONE
+ | pr_def (name, CodegenThingol.Class (superclasss, (v, classops))) =
+ let
+ val tyvars = intro_vars [v] keyword_vars;
+ fun pr_classop (classop, ty) =
Pretty.block [
- str (resolv co),
- str " of",
+ str (deresolv_here classop ^ " ::"),
Pretty.brk 1,
- Pretty.enum " *" "" "" (map (ml_from_type (INFX (2, L))) tys)
+ pr_typ tyvars NOBR ty
]
- fun mk_datatype definer (t, (vs, cs)) =
- (Pretty.block o Pretty.breaks) (
- str definer
- :: ml_from_tycoexpr NOBR (t, map (ITyVar o fst) vs)
- :: str "="
- :: separate (str "|") (map mk_cons cs)
- )
- in
- chunk_defs (
- mk_datatype "datatype" def
- :: map (mk_datatype "and") defs_tl
+ in
+ Pretty.block [
+ str "class ",
+ pr_typparms tyvars [(v, superclasss)],
+ str (deresolv_here name ^ " " ^ v),
+ str " where",
+ Pretty.fbrk,
+ Pretty.chunks (map pr_classop classops)
+ ]
+ end |> SOME
+ | pr_def (_, CodegenThingol.Classmember _) =
+ NONE
+ | pr_def (_, CodegenThingol.Classinst ((class, (tyco, vs)), (_, classop_defs))) =
+ let
+ val tyvars = intro_vars (map fst vs) keyword_vars;
+ in
+ Pretty.block [
+ str "instance ",
+ pr_typparms tyvars vs,
+ str (class_name class ^ " "),
+ pr_typ tyvars BR (tyco `%% map (ITyVar o fst) vs),
+ str " where",
+ Pretty.fbrk,
+ Pretty.chunks (map (fn (classop, t) =>
+ let
+ val consts = map_filter
+ (fn c => if (is_some o const_syntax) c
+ then NONE else (SOME o NameSpace.base o deresolv) c)
+ (CodegenThingol.fold_constnames (insert (op =)) t []);
+ val vars = keyword_vars
+ |> intro_vars consts;
+ in
+ (Pretty.block o Pretty.breaks) [
+ (str o classop_name class) classop,
+ str "=",
+ pr_term vars NOBR t
+ ]
+ end
+ ) classop_defs)
+ ]
+ end |> SOME
+ in pr_def def end;
+
+
+(** generic abstract serializer **)
+
+structure NameMangler = NameManglerFun (
+ type ctxt = (string * string -> string) * (string -> string option);
+ type src = string * string;
+ val ord = prod_ord string_ord string_ord;
+ fun mk (postprocess, validate) ((shallow, name), 0) =
+ let
+ val name' = postprocess (shallow, name);
+ in case validate name'
+ of NONE => name'
+ | _ => mk (postprocess, validate) ((shallow, name), 1)
+ end
+ | mk (postprocess, validate) (("", name), i) =
+ postprocess ("", name ^ replicate_string i "'")
+ |> perhaps validate
+ | mk (postprocess, validate) ((shallow, name), 1) =
+ postprocess (shallow, shallow ^ "_" ^ name)
+ |> perhaps validate
+ | mk (postprocess, validate) ((shallow, name), i) =
+ postprocess (shallow, name ^ replicate_string i "'")
+ |> perhaps validate;
+ fun is_valid _ _ = true;
+ fun maybe_unique _ _ = NONE;
+ fun re_mangle _ dst = error ("No such definition name: " ^ quote dst);
+);
+
+(*FIXME refactor this properly*)
+fun code_serialize seri_defs seri_module validate postprocess nsp_conn name_root
+ (code : CodegenThingol.code) =
+ let
+ datatype node = Def of CodegenThingol.def | Module of node Graph.T;
+ fun dest_modl (Module m) = m;
+ fun dest_name name =
+ let
+ val (names, name_base) = (split_last o NameSpace.unpack) name;
+ val (names_mod, name_shallow) = split_last names;
+ in (names_mod, NameSpace.pack [name_shallow, name_base]) end;
+ fun mk_deresolver module nsp_conn postprocess validate =
+ let
+ datatype tabnode = N of string * tabnode Symtab.table option;
+ fun mk module manglers tab =
+ let
+ fun mk_name name =
+ case NameSpace.unpack name
+ of [n] => ("", n)
+ | [s, n] => (s, n);
+ fun in_conn (shallow, conn) =
+ member (op = : string * string -> bool) conn shallow;
+ fun add_name name =
+ let
+ val n as (shallow, _) = mk_name name;
+ in
+ AList.map_entry_yield in_conn shallow (
+ NameMangler.declare (postprocess, validate) n
+ #-> (fn n' => pair (name, n'))
+ ) #> apfst the
+ end;
+ val (renamings, manglers') =
+ fold_map add_name (Graph.keys module) manglers;
+ fun extend_tab (n, n') =
+ if (length o NameSpace.unpack) n = 1
+ then
+ Symtab.update_new
+ (n, N (n', SOME (mk ((dest_modl o Graph.get_node module) n) manglers' Symtab.empty)))
+ else
+ Symtab.update_new (n, N (n', NONE));
+ in fold extend_tab renamings tab end;
+ fun get_path_name [] tab =
+ ([], SOME tab)
+ | get_path_name [p] tab =
+ let
+ val SOME (N (p', tab')) = Symtab.lookup tab p
+ in ([p'], tab') end
+ | get_path_name [p1, p2] tab =
+ (case Symtab.lookup tab p1
+ of SOME (N (p', SOME tab')) =>
+ let
+ val (ps', tab'') = get_path_name [p2] tab'
+ in (p' :: ps', tab'') end
+ | NONE =>
+ let
+ val SOME (N (p', NONE)) = Symtab.lookup tab (NameSpace.pack [p1, p2])
+ in ([p'], NONE) end)
+ | get_path_name (p::ps) tab =
+ let
+ val SOME (N (p', SOME tab')) = Symtab.lookup tab p
+ val (ps', tab'') = get_path_name ps tab'
+ in (p' :: ps', tab'') end;
+ fun deresolv tab prefix name =
+ let
+ val (common, (_, rem)) = chop_prefix (op =) (prefix, NameSpace.unpack name);
+ val (_, SOME tab') = get_path_name common tab;
+ val (name', _) = get_path_name rem tab';
+ in NameSpace.pack name' end handle BIND => (error ("Missing name: " ^ quote name ^ ", in " ^ quote (NameSpace.pack prefix)));
+ in deresolv (mk module (AList.make (K NameMangler.empty) nsp_conn) Symtab.empty) end;
+ fun allimports_of modl =
+ let
+ fun imps_of prfx (Module modl) imps tab =
+ let
+ val this = NameSpace.pack prfx;
+ val name_con = (rev o Graph.strong_conn) modl;
+ in
+ tab
+ |> pair []
+ |> fold (fn names => fn (imps', tab) =>
+ tab
+ |> fold_map (fn name =>
+ imps_of (prfx @ [name]) (Graph.get_node modl name) (imps' @ imps)) names
+ |-> (fn imps'' => pair (flat imps'' @ imps'))) name_con
+ |-> (fn imps' =>
+ Symtab.update_new (this, imps' @ imps)
+ #> pair (this :: imps'))
+ end
+ | imps_of prfx (Def _) imps tab =
+ ([], tab);
+ in snd (imps_of [] (Module modl) [] Symtab.empty) end;
+ fun add_def ((names_mod, name_id), def) =
+ let
+ fun add [] =
+ Graph.new_node (name_id, Def def)
+ | add (m::ms) =
+ Graph.default_node (m, Module Graph.empty)
+ #> Graph.map_node m (Module o add ms o dest_modl)
+ in add names_mod end;
+ fun add_dep (name1, name2) =
+ if name1 = name2 then I
+ else
+ let
+ val m1 = dest_name name1 |> apsnd single |> (op @);
+ val m2 = dest_name name2 |> apsnd single |> (op @);
+ val (ms, (r1, r2)) = chop_prefix (op =) (m1, m2);
+ val (ms, (s1::r1, s2::r2)) = chop_prefix (op =) (m1, m2);
+ val add_edge =
+ if null r1 andalso null r2
+ then Graph.add_edge
+ else fn edge => fn gr => (Graph.add_edge_acyclic edge gr
+ handle Graph.CYCLES _ =>
+ error ("Module dependency "
+ ^ quote name1 ^ " -> " ^ quote name2 ^ " would result in module dependency cycle"))
+ fun add [] node =
+ node
+ |> add_edge (s1, s2)
+ | add (m::ms) node =
+ node
+ |> Graph.map_node m (Module o add ms o dest_modl);
+ in add ms end;
+ val root_module =
+ Graph.empty
+ |> Graph.fold (fn (name, (def, _)) => add_def (dest_name name, def)) code
+ |> Graph.fold (fn (name, (_, (_, deps))) =>
+ fold (curry add_dep name) deps) code;
+ val names = map fst (Graph.dest root_module);
+ val imptab = allimports_of root_module;
+ val resolver = mk_deresolver root_module nsp_conn postprocess validate;
+ fun sresolver s = (resolver o NameSpace.unpack) s
+ fun mk_name prfx name =
+ let
+ val name_qual = NameSpace.pack (prfx @ [name])
+ in (name_qual, resolver prfx name_qual) end;
+ fun is_bot (_, (Def Bot)) = true
+ | is_bot _ = false;
+ fun mk_contents prfx module =
+ map_filter (seri prfx)
+ ((map (AList.make (Graph.get_node module)) o rev o Graph.strong_conn) module)
+ and seri prfx [(name, Module modl)] =
+ seri_module (resolver []) (map (resolver []) ((the o Symtab.lookup imptab) (NameSpace.pack (prfx @ [name]))))
+ (mk_name prfx name, mk_contents (prfx @ [name]) modl)
+ | seri prfx ds =
+ seri_defs sresolver (NameSpace.pack prfx)
+ (map (fn (name, Def def) => (fst (mk_name prfx name), def)) ds)
+ in
+ seri_module (resolver []) (map (resolver []) ((the o Symtab.lookup imptab) ""))
+ (("", name_root), (mk_contents [] root_module))
+ end;
+
+fun abstract_serializer (target, nspgrp) name_root (from_defs, from_module, validator, postproc)
+ postprocess (class_syntax, tyco_syntax, const_syntax)
+ (drop, select) code =
+ let
+ fun project NONE code = code
+ | project (SOME names) code =
+ let
+ fun check name = if member (op =) drop name
+ then error ("shadowed definition " ^ quote name ^ " selected for serialization")
+ else if can (Graph.get_node code) name
+ then ()
+ else error ("dropped definition " ^ quote name ^ " selected for serialization")
+ val names' = (map o tap) check names;
+ in CodegenThingol.project_code names code end;
+ fun from_module' resolv imps ((name_qual, name), defs) =
+ from_module resolv imps ((name_qual, name), defs)
+ |> postprocess (resolv name_qual);
+ in
+ code
+ |> tracing (fn _ => "dropping shadowed definitions...")
+ |> CodegenThingol.delete_garbage drop
+ |> tracing (fn _ => "projecting...")
+ |> project select
+ |> tracing (fn _ => "serializing...")
+ |> code_serialize (from_defs (class_syntax, tyco_syntax, const_syntax))
+ from_module' validator postproc nspgrp name_root
+ |> K ()
+ end;
+
+fun abstract_validator keywords name =
+ let
+ fun replace_invalid c = (*FIXME*)
+ if Symbol.is_ascii_letter c orelse Symbol.is_ascii_digit c orelse c = "'"
+ andalso not (NameSpace.separator = c)
+ then c
+ else "_"
+ fun suffix_it name=
+ name
+ |> member (op =) keywords ? 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;
+
+fun write_file mkdir path p = (
+ if mkdir
+ then
+ File.mkdir (Path.dir path)
+ else ();
+ File.write path (Pretty.output p ^ "\n");
+ p
+ );
+
+fun mk_module_file postprocess_module ext path name p =
+ let
+ val prfx = Path.dir path;
+ val name' = case name
+ of "" => Path.base path
+ | _ => (Path.ext ext o Path.unpack o implode o separate "/" o NameSpace.unpack) name;
+ in
+ p
+ |> write_file true (Path.append prfx name')
+ |> postprocess_module name
+ end;
+
+fun parse_args f args =
+ case f args
+ of (x, []) => x
+ | (_, _) => error "bad serializer arguments";
+
+fun parse_single_file serializer =
+ parse_args (Args.name
+ >> (fn path => serializer
+ (fn "" => write_file false (Path.unpack path) #> K NONE
+ | _ => SOME)));
+
+fun parse_multi_file postprocess_module ext serializer =
+ parse_args (Args.name
+ >> (fn path => (serializer o mk_module_file postprocess_module ext) (Path.unpack path)));
+
+fun parse_internal serializer =
+ parse_args (Args.name
+ >> (fn "-" => serializer
+ (fn "" => (fn p => (use_text Context.ml_output false (Pretty.output p); NONE))
+ | _ => SOME)
+ | _ => Scan.fail ()));
+
+fun parse_stdout serializer =
+ parse_args (Args.name
+ >> (fn "_" => serializer
+ (fn "" => (fn p => (Pretty.writeln p; NONE))
+ | _ => SOME)
+ | _ => Scan.fail ()));
+
+val nsp_module = CodegenNames.nsp_module;
+val nsp_class = CodegenNames.nsp_class;
+val nsp_tyco = CodegenNames.nsp_tyco;
+val nsp_inst = CodegenNames.nsp_inst;
+val nsp_fun = CodegenNames.nsp_fun;
+val nsp_classop = CodegenNames.nsp_classop;
+val nsp_dtco = CodegenNames.nsp_dtco;
+val nsp_eval = CodegenNames.nsp_eval;
+
+
+(** ML serializer **)
+
+local
+
+val reserved_ml' = [
+ "bool", "int", "list", "unit", "option", "true", "false", "not",
+ "NONE", "SOME", "o", "string", "char", "String", "Term"
+];
+
+fun ml_from_defs (_, tyco_syntax, const_syntax) deresolver prefx defs =
+ let
+ val seri = pr_sml_def tyco_syntax const_syntax
+ (make_vars (ThmDatabase.ml_reserved @ reserved_ml'))
+ (deresolver prefx) #> SOME;
+ val filter_funs =
+ map
+ (fn (name, CodegenThingol.Fun info) => (name, info)
+ | (name, def) => error ("Function block containing illegal def: " ^ quote name)
)
- end;
- in (ml_from_funs, ml_from_datatypes) end;
-
-fun ml_from_defs init_ctxt
- (_, tyco_syntax, const_syntax) resolver prefx defs =
- let
- val resolv = resolver prefx;
- val (ml_from_dictvar, ml_from_label, ml_from_tyvar, ml_from_insts, ml_from_tycoexpr, ml_from_type, ml_from_expr) =
- ml_expr_seri (tyco_syntax, const_syntax) resolv;
- val (ml_from_funs, ml_from_datatypes) =
- ml_fun_datatype init_ctxt (tyco_syntax, const_syntax) resolv;
+ #> MLFuns;
val filter_datatype =
map_filter
(fn (name, CodegenThingol.Datatype info) => SOME (name, info)
| (name, CodegenThingol.Datatypecons _) => NONE
- | (name, def) => error ("Datatype block containing illegal def: "
- ^ (Pretty.output o CodegenThingol.pretty_def) def));
+ | (name, def) => error ("Datatype block containing illegal def: " ^ quote name)
+ )
+ #> MLDatas;
fun filter_class defs =
case map_filter
(fn (name, CodegenThingol.Class info) => SOME (name, info)
| (name, CodegenThingol.Classmember _) => NONE
- | (name, def) => error ("Class block containing illegal def: "
- ^ (Pretty.output o CodegenThingol.pretty_def) def)) defs
- of [class] => class
+ | (name, def) => error ("Class block containing illegal def: " ^ quote name)
+ ) defs
+ of [class] => MLClass class
| _ => error ("Class block without class: " ^ (commas o map (quote o fst)) defs)
- fun ml_from_class (name, (supclasses, (v, membrs))) =
- let
- val w = ml_from_dictvar v;
- fun from_supclass class =
- Pretty.block [
- ml_from_label class,
- str ":",
- Pretty.brk 1,
- str ("'" ^ v),
- Pretty.brk 1,
- (str o resolv) class
- ];
- fun from_membr (m, ty) =
- Pretty.block [
- (ml_from_label o suffix "_" o NameSpace.base) m,
- str ":",
- Pretty.brk 1,
- ml_from_type NOBR ty
- ];
- fun from_membr_fun (m, _) =
- (Pretty.block o Pretty.breaks) [
- str "fun",
- (str o resolv) m,
- Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ resolv name)],
- str "=",
- Pretty.block [str "#", (ml_from_label o suffix "_" o NameSpace.base) m],
- str (w ^ ";")
- ];
- in
- Pretty.chunks (
- (Pretty.block o Pretty.breaks) [
- str "type",
- str ("'" ^ v),
- (str o resolv) name,
- str "=",
- Pretty.enum "," "{" "};" (
- map from_supclass supclasses @ map from_membr membrs
- )
- ]
- :: map from_membr_fun membrs)
- end
- fun ml_from_def (name, CodegenThingol.Typesyn (vs, ty)) =
- (map (fn (vname, []) => () | _ =>
- error "Can't serialize sort constrained type declaration to ML") vs;
- Pretty.block [
- str "type ",
- ml_from_tycoexpr NOBR (name, map (ITyVar o fst) vs),
- str " =",
- Pretty.brk 1,
- ml_from_type NOBR ty,
- str ";"
- ]
- ) |> SOME
- | ml_from_def (name, CodegenThingol.Classinst ((class, (tyco, arity)), (suparities, memdefs))) =
- let
- val definer = if null arity then "val" else "fun"
- fun from_supclass (supclass, (supinst, lss)) =
- (Pretty.block o Pretty.breaks) [
- ml_from_label supclass,
- str "=",
- ml_from_insts NOBR [Instance (supinst, lss)]
- ];
- fun from_memdef (m, e) =
- let
- val consts = map_filter
- (fn c => if (is_some o const_syntax) c
- then NONE else (SOME o NameSpace.base o resolv) c) (CodegenThingol.add_constnames e []);
- val var_ctxt = init_ctxt
- |> intro_ctxt consts;
- in
- (Pretty.block o Pretty.breaks) [
- (ml_from_label o suffix "_" o NameSpace.base) m,
- str "=",
- ml_from_expr var_ctxt NOBR e
- ]
- end;
- fun mk_corp rhs =
- (Pretty.block o Pretty.breaks) (
- str definer
- :: (str o resolv) name
- :: map ml_from_tyvar arity
- @ [str "=", rhs]
- );
- fun mk_memdefs supclassexprs memdefs =
- (mk_corp o Pretty.block o Pretty.breaks) [
- Pretty.enum "," "{" "}" (supclassexprs @ memdefs),
- str ":",
- ml_from_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity])
- ];
- in
- mk_memdefs (map from_supclass suparities) (map from_memdef memdefs) |> SOME
- end
- | ml_from_def (name, def) = error ("Illegal definition for " ^ quote name ^ ": " ^
- (Pretty.output o CodegenThingol.pretty_def) def);
in case defs
- of (_, CodegenThingol.Fun _)::_ => ((*writeln "FUN";*) (SOME o ml_from_funs o map (fn (name, CodegenThingol.Fun info) => (name, info))) defs)
- | (_, CodegenThingol.Datatypecons _)::_ => ((*writeln "DTCO";*) (SOME o ml_from_datatypes o filter_datatype) defs)
- | (_, CodegenThingol.Datatype _)::_ => ((*writeln "DT";*) (SOME o ml_from_datatypes o filter_datatype) defs)
- | (_, CodegenThingol.Class _)::_ => (SOME o ml_from_class o filter_class) defs
- | (_, CodegenThingol.Classmember _)::_ => (SOME o ml_from_class o filter_class) defs
- | [def] => ml_from_def def
+ of (_, CodegenThingol.Fun _)::_ => (seri o filter_funs) defs
+ | (_, CodegenThingol.Datatypecons _)::_ => (seri o filter_datatype) defs
+ | (_, CodegenThingol.Datatype _)::_ => (seri o filter_datatype) defs
+ | (_, CodegenThingol.Class _)::_ => (seri o filter_class) defs
+ | (_, CodegenThingol.Classmember _)::_ => (seri o filter_class) defs
+ | [(inst, CodegenThingol.Classinst info)] => seri (MLClassinst (inst, info))
| defs => error ("Illegal mutual dependencies: " ^ (commas o map fst) defs)
end;
@@ -902,60 +1208,42 @@
else n
end;
in abstract_serializer (target, nspgrp)
- root_name (ml_from_defs (make_ctxt ((ThmDatabase.ml_reserved @ reserved_ml'))), ml_from_module,
+ root_name (ml_from_defs, ml_from_module,
abstract_validator (ThmDatabase.ml_reserved @ reserved_ml'), postproc) end;
in
-val ml_fun_datatype = fn thy =>
- let
- val target = "SML";
- val data = CodegenSerializerData.get thy;
- val target_data =
- (the oo Symtab.lookup) data target;
- val syntax_tyco = #syntax_tyco target_data;
- val syntax_const = #syntax_const target_data;
- fun fun_of syntax = (Option.map fst oo Symtab.lookup) syntax;
- in ml_fun_datatype (make_ctxt (ThmDatabase.ml_reserved @ reserved_ml')) (fun_of syntax_tyco, fun_of syntax_const) end;
-
-fun ml_from_thingol target =
+fun ml_from_thingol target args =
let
val serializer = ml_serializer "ROOT" target [[nsp_module], [nsp_class, nsp_tyco],
[nsp_fun, nsp_dtco, nsp_class, nsp_classop, nsp_inst]]
val parse_multi =
- OuterParse.name
+ Args.name
#-> (fn "dir" =>
parse_multi_file
(K o SOME o str o suffix ";" o prefix "val _ = use "
o quote o suffix ".ML" o translate_string (fn "." => "/" | s => s)) "ML" serializer
| _ => Scan.fail ());
in
- parse_multi
+ (parse_multi
|| parse_internal serializer
|| parse_stdout serializer
- || parse_single_file serializer
+ || parse_single_file serializer) args
end;
val eval_verbose = ref false;
-fun eval_term thy ((ref_name, reff), e) code =
+fun eval_term_proto thy data hidden ((ref_name, reff), e) code =
let
val (val_name, code') = CodegenThingol.add_eval_def (nsp_eval, e) code;
val struct_name = "EVAL";
fun output p = if !eval_verbose then (Pretty.writeln p; Pretty.output p)
else Pretty.output p;
- val target = "SML";
- val data = CodegenSerializerData.get thy;
- val target_data =
- (the oo Symtab.lookup) data target;
- val syntax_tyco = #syntax_tyco target_data;
- val syntax_const = #syntax_const target_data;
- fun fun_of syntax = (Option.map fst oo Symtab.lookup) syntax;
val serializer = ml_serializer struct_name "SML" [[nsp_module], [nsp_class, nsp_tyco],
[nsp_fun, nsp_dtco, nsp_class, nsp_classop, nsp_inst], [nsp_eval]]
(fn "" => (fn p => (use_text Context.ml_output (!eval_verbose) (output p); NONE))
- | _ => SOME) (K NONE, fun_of syntax_tyco, fun_of syntax_const)
- ((Symtab.keys (#syntax_tyco target_data) @ Symtab.keys (#syntax_const target_data)), SOME [NameSpace.pack [nsp_eval, val_name]]);
+ | _ => SOME) data
+ (hidden, SOME [NameSpace.pack [nsp_eval, val_name]]);
val _ = serializer code';
val val_name_struct = NameSpace.append struct_name val_name;
val _ = reff := NONE;
@@ -990,272 +1278,18 @@
(** haskell serializer **)
-local
-
-fun hs_from_defs init_ctxt (class_syntax, tyco_syntax, const_syntax)
- resolver prefix defs =
+fun hs_from_thingol target args =
let
- val is_cons = CodegenNames.has_nsp CodegenNames.nsp_dtco;
- val resolv = resolver "";
- val resolv_here = resolver prefix;
- fun hs_from_class cls = case class_syntax cls
- of NONE => resolv cls
- | SOME (cls, _) => cls;
- fun hs_from_classop_name cls clsop = case class_syntax cls
- of NONE => NameSpace.base clsop
- | SOME (_, classop_syntax) => case classop_syntax clsop
- of NONE => NameSpace.base clsop
- | SOME clsop => clsop;
- fun hs_from_typparms tyvar_ctxt vs =
+ fun hs_from_defs keyword_vars (class_syntax, tyco_syntax, const_syntax) deresolver prefix defs =
let
- fun from_typparms [] = str ""
- | from_typparms vs =
- vs
- |> map (fn (v, cls) => str
- (hs_from_class cls ^ " " ^ lookup_ctxt tyvar_ctxt v))
- |> Pretty.enum "," "(" ")"
- |> (fn p => Pretty.block [p, str " => "])
- in
- vs
- |> maps (fn (v, sort) => map (pair v) sort)
- |> from_typparms
+ val deresolv = deresolver "";
+ val deresolv_here = deresolver prefix;
+ val hs_from_def = pr_haskell class_syntax tyco_syntax const_syntax
+ keyword_vars deresolv_here deresolv;
+ in case map_filter hs_from_def defs
+ of [] => NONE
+ | ps => (SOME o Pretty.chunks o separate (str "")) ps
end;
- fun hs_from_tycoexpr tyvar_ctxt fxy (tyco, tys) =
- brackify fxy (str tyco :: map (hs_from_type tyvar_ctxt BR) tys)
- and hs_from_type tyvar_ctxt fxy (tycoexpr as tyco `%% tys) =
- (case tyco_syntax tyco
- of NONE =>
- hs_from_tycoexpr tyvar_ctxt fxy (resolv tyco, tys)
- | SOME (i, pr) =>
- if not (i = length tys)
- then error ("Number of argument mismatch in customary serialization: "
- ^ (string_of_int o length) tys ^ " given, "
- ^ string_of_int i ^ " expected")
- else pr fxy (hs_from_type tyvar_ctxt) tys)
- | hs_from_type tyvar_ctxt fxy (t1 `-> t2) =
- brackify_infix (1, R) fxy [
- hs_from_type tyvar_ctxt (INFX (1, X)) t1,
- str "->",
- hs_from_type tyvar_ctxt (INFX (1, R)) t2
- ]
- | hs_from_type tyvar_ctxt fxy (ITyVar v) =
- str (lookup_ctxt tyvar_ctxt v);
- fun hs_from_typparms_tycoexpr tyvar_ctxt (vs, tycoexpr) =
- Pretty.block [hs_from_typparms tyvar_ctxt vs, hs_from_tycoexpr tyvar_ctxt NOBR tycoexpr]
- fun hs_from_typparms_type tyvar_ctxt (vs, ty) =
- Pretty.block [hs_from_typparms tyvar_ctxt vs, hs_from_type tyvar_ctxt NOBR ty]
- fun hs_from_expr var_ctxt fxy (e as IConst x) =
- hs_from_app var_ctxt fxy (x, [])
- | hs_from_expr var_ctxt fxy (e as (e1 `$ e2)) =
- (case CodegenThingol.unfold_const_app e
- of SOME x => hs_from_app var_ctxt fxy x
- | _ =>
- brackify fxy [
- hs_from_expr var_ctxt NOBR e1,
- hs_from_expr var_ctxt BR e2
- ])
- | hs_from_expr var_ctxt fxy (IVar v) =
- str (lookup_ctxt var_ctxt v)
- | hs_from_expr var_ctxt fxy (e as _ `|-> _) =
- let
- val (es, e) = CodegenThingol.unfold_abs e;
- val vs = fold CodegenThingol.add_varnames (map fst es) [];
- val var_ctxt' = intro_ctxt vs var_ctxt;
- in
- brackify BR (
- str "\\"
- :: map (hs_from_expr var_ctxt' BR o fst) es @ [
- str "->",
- hs_from_expr var_ctxt' NOBR e
- ])
- end
- | hs_from_expr var_ctxt fxy (INum (n, _)) =
- if n > 0 then
- (str o IntInf.toString) n
- else
- brackify BR [(str o Library.prefix "-" o IntInf.toString o IntInf.~) n]
- | hs_from_expr var_ctxt fxy (IChar (c, _)) =
- (str o enclose "'" "'")
- (let val i = (Char.ord o the o Char.fromString) c
- in if i < 32
- then Library.prefix "\\" (string_of_int i)
- else c
- end)
- | hs_from_expr var_ctxt fxy (e as ICase ((_, [_]), _)) =
- let
- val (ps, body) = CodegenThingol.unfold_let e;
- fun mk_bind ((p, _), e) var_ctxt =
- let
- val vs = CodegenThingol.add_varnames p [];
- val var_ctxt' = intro_ctxt vs var_ctxt;
- in
- ((Pretty.block o Pretty.breaks) [
- hs_from_expr var_ctxt' BR p,
- str "=",
- hs_from_expr var_ctxt NOBR e
- ], var_ctxt')
- end;
- val (binds, var_ctxt') = fold_map mk_bind ps var_ctxt;
- in Pretty.chunks [
- [str ("let"), Pretty.fbrk, binds |> Pretty.chunks] |> Pretty.block,
- [str ("in "), hs_from_expr var_ctxt' NOBR body] |> Pretty.block
- ] end
- | hs_from_expr var_ctxt fxy (ICase (((de, _), bses), _)) =
- let
- fun mk_clause (se, be) =
- let
- val vs = CodegenThingol.add_varnames se [];
- val var_ctxt' = intro_ctxt vs var_ctxt;
- in
- (Pretty.block o Pretty.breaks) [
- hs_from_expr var_ctxt' NOBR se,
- str "->",
- hs_from_expr var_ctxt' NOBR be
- ]
- end
- in Pretty.enclose "(" ")" [
- str "case",
- Pretty.brk 1,
- hs_from_expr var_ctxt NOBR de,
- Pretty.brk 1,
- str "of",
- Pretty.fbrk,
- (Pretty.chunks o map mk_clause) bses
- ] end
- and hs_mk_app var_ctxt c es =
- (str o resolv) c :: map (hs_from_expr var_ctxt BR) es
- and hs_from_app var_ctxt fxy =
- from_app (hs_mk_app var_ctxt) (hs_from_expr var_ctxt) const_syntax fxy
- fun hs_from_def (name, CodegenThingol.Fun (def as (eqs, (vs, ty)))) =
- let
- fun from_eq (args, rhs) =
- let
- val consts = map_filter
- (fn c => if (is_some o const_syntax) c
- then NONE else (SOME o NameSpace.base o resolv) c) (fold CodegenThingol.add_constnames (rhs :: args) []);
- val vars = fold CodegenThingol.add_unbound_varnames (rhs :: args) [];
- val var_ctxt = init_ctxt
- |> intro_ctxt consts
- |> intro_ctxt vars;
- in
- (Pretty.block o Pretty.breaks) (
- (str o resolv_here) name
- :: map (hs_from_expr var_ctxt BR) args
- @ [str "=", hs_from_expr var_ctxt NOBR rhs]
- )
- end;
- val tyvar_ctxt = intro_ctxt (map fst vs) init_ctxt;
- in
- Pretty.chunks (
- Pretty.block [
- (str o suffix " ::" o resolv_here) name,
- Pretty.brk 1,
- hs_from_typparms_type tyvar_ctxt (vs, ty)
- ]
- :: (map from_eq o fst o snd o constructive_fun) (name, def)
- ) |> SOME
- end
- | hs_from_def (name, CodegenThingol.Typesyn (vs, ty)) =
- let
- val tyvar_ctxt = intro_ctxt (map fst vs) init_ctxt;
- in
- (Pretty.block o Pretty.breaks) [
- str "type",
- hs_from_typparms_tycoexpr tyvar_ctxt (vs, (resolv_here name, map (ITyVar o fst) vs)),
- str "=",
- hs_from_typparms_type tyvar_ctxt ([], ty)
- ] |> SOME
- end
- | hs_from_def (name, CodegenThingol.Datatype (vs, [(co, [ty])])) =
- let
- val tyvar_ctxt = intro_ctxt (map fst vs) init_ctxt;
- in
- (Pretty.block o Pretty.breaks) [
- str "newtype",
- hs_from_typparms_tycoexpr tyvar_ctxt (vs, (resolv_here name, map (ITyVar o fst) vs)),
- str "=",
- (str o resolv_here) co,
- hs_from_type tyvar_ctxt BR ty
- ] |> SOME
- end
- | hs_from_def (name, CodegenThingol.Datatype (vs, constr :: constrs)) =
- let
- val tyvar_ctxt = intro_ctxt (map fst vs) init_ctxt;
- fun mk_cons (co, tys) =
- (Pretty.block o Pretty.breaks) (
- (str o resolv_here) co
- :: map (hs_from_type tyvar_ctxt BR) tys
- )
- in
- (Pretty.block o Pretty.breaks) (
- str "data"
- :: hs_from_typparms_tycoexpr tyvar_ctxt (vs, (resolv_here name, map (ITyVar o fst) vs))
- :: str "="
- :: mk_cons constr
- :: map ((fn p => Pretty.block [str "| ", p]) o mk_cons) constrs
- )
- end |> SOME
- | hs_from_def (_, CodegenThingol.Datatypecons _) =
- NONE
- | hs_from_def (name, CodegenThingol.Class (supclasss, (v, membrs))) =
- let
- val tyvar_ctxt = intro_ctxt [v] init_ctxt;
- fun mk_member (m, ty) =
- Pretty.block [
- str (resolv_here m ^ " ::"),
- Pretty.brk 1,
- hs_from_type tyvar_ctxt NOBR ty
- ]
- in
- Pretty.block [
- str "class ",
- hs_from_typparms tyvar_ctxt [(v, supclasss)],
- str (resolv_here name ^ " " ^ v),
- str " where",
- Pretty.fbrk,
- Pretty.chunks (map mk_member membrs)
- ] |> SOME
- end
- | hs_from_def (_, CodegenThingol.Classmember _) =
- NONE
- | hs_from_def (_, CodegenThingol.Classinst ((clsname, (tyco, vs)), (_, memdefs))) =
- let
- val tyvar_ctxt = intro_ctxt (map fst vs) init_ctxt;
- in
- Pretty.block [
- str "instance ",
- hs_from_typparms tyvar_ctxt vs,
- str (hs_from_class clsname ^ " "),
- hs_from_type tyvar_ctxt BR (tyco `%% map (ITyVar o fst) vs),
- str " where",
- Pretty.fbrk,
- Pretty.chunks (map (fn (m, e) =>
- let
- val consts = map_filter
- (fn c => if (is_some o const_syntax) c
- then NONE else (SOME o NameSpace.base o resolv) c) (CodegenThingol.add_constnames e []);
- val var_ctxt = init_ctxt
- |> intro_ctxt consts;
- in
- (Pretty.block o Pretty.breaks) [
- (str o hs_from_classop_name clsname) m,
- str "=",
- hs_from_expr var_ctxt NOBR e
- ]
- end
- ) memdefs)
- ] |> SOME
- end
- in
- case map_filter (fn (name, def) => hs_from_def (name, def)) defs
- of [] => NONE
- | l => (SOME o Pretty.chunks o separate (str "")) l
- end;
-
-in
-
-fun hs_from_thingol target =
- let
val reserved_hs = [
"hiding", "deriving", "where", "case", "of", "infix", "infixl", "infixr",
"import", "default", "forall", "let", "in", "class", "qualified", "data",
@@ -1280,72 +1314,324 @@
end;
val serializer = abstract_serializer (target, [[nsp_module],
[nsp_class], [nsp_tyco], [nsp_fun, nsp_classop], [nsp_dtco], [nsp_inst]])
- "Main" (hs_from_defs (make_ctxt reserved_hs), hs_from_module, abstract_validator reserved_hs, postproc);
+ "Main" (hs_from_defs (make_vars reserved_hs), hs_from_module, abstract_validator reserved_hs, postproc);
in
- parse_multi_file ((K o K) NONE) "hs" serializer
+ (parse_multi_file ((K o K) NONE) "hs" serializer) args
end;
-end; (* local *)
+
+(** LEGACY DIAGNOSIS **)
+
+local
+
+open CodegenThingol;
+
+in
+
+val pretty_typparms =
+ Pretty.list "(" ")" o Pretty.commas o map (fn (v, sort) => (Pretty.block o Pretty.breaks)
+ [Pretty.str v, Pretty.str "::", Pretty.enum "&" "" "" (map Pretty.str sort)]);
+
+fun pretty_itype (tyco `%% tys) =
+ Pretty.enum "" "(" ")" (Pretty.str tyco :: map pretty_itype tys)
+ | pretty_itype (ty1 `-> ty2) =
+ Pretty.enum "" "(" ")" [pretty_itype ty1, Pretty.str "->", pretty_itype ty2]
+ | pretty_itype (ITyVar v) =
+ Pretty.str v;
+
+fun pretty_iterm (IConst (c, _)) =
+ Pretty.str c
+ | pretty_iterm (IVar v) =
+ Pretty.str ("?" ^ v)
+ | pretty_iterm (t1 `$ t2) =
+ (Pretty.enclose "(" ")" o Pretty.breaks)
+ [pretty_iterm t1, pretty_iterm t2]
+ | pretty_iterm ((v, ty) `|-> t) =
+ (Pretty.enclose "(" ")" o Pretty.breaks)
+ [Pretty.str v, Pretty.str "::", pretty_itype ty, Pretty.str "|->", pretty_iterm t]
+ | pretty_iterm (INum (n, _)) =
+ (Pretty.str o IntInf.toString) n
+ | pretty_iterm (IChar (h, _)) =
+ (Pretty.str o quote) h
+ | pretty_iterm (ICase (((t, _), bs), _)) =
+ (Pretty.enclose "(" ")" o Pretty.breaks) [
+ Pretty.str "case",
+ pretty_iterm t,
+ Pretty.enclose "(" ")" (map (fn (p, t) =>
+ (Pretty.block o Pretty.breaks) [
+ pretty_iterm p,
+ Pretty.str "=>",
+ pretty_iterm t
+ ]
+ ) bs)
+ ];
+
+fun pretty_def Bot =
+ Pretty.str "<Bot>"
+ | pretty_def (Fun (eqs, (vs, ty))) =
+ Pretty.enum " |" "" "" (
+ map (fn (ps, body) =>
+ Pretty.block [
+ Pretty.enum "," "[" "]" (map pretty_iterm ps),
+ Pretty.str " |->",
+ Pretty.brk 1,
+ pretty_iterm body,
+ Pretty.str "::",
+ pretty_typparms vs,
+ Pretty.str "/",
+ pretty_itype ty
+ ]) eqs
+ )
+ | pretty_def (Datatype (vs, cs)) =
+ Pretty.block [
+ pretty_typparms vs,
+ Pretty.str " |=> ",
+ Pretty.enum " |" "" ""
+ (map (fn (c, tys) => (Pretty.block o Pretty.breaks)
+ (Pretty.str c :: map pretty_itype tys)) cs)
+ ]
+ | pretty_def (Datatypecons dtname) =
+ Pretty.str ("cons " ^ dtname)
+ | pretty_def (Class (supcls, (v, mems))) =
+ Pretty.block [
+ Pretty.str ("class var " ^ v ^ " extending "),
+ Pretty.enum "," "[" "]" (map Pretty.str supcls),
+ Pretty.str " with ",
+ Pretty.enum "," "[" "]"
+ (map (fn (m, ty) => Pretty.block
+ [Pretty.str (m ^ "::"), pretty_itype ty]) mems)
+ ]
+ | pretty_def (Classmember clsname) =
+ Pretty.block [
+ Pretty.str "class member belonging to ",
+ Pretty.str clsname
+ ]
+ | pretty_def (Classinst ((clsname, (tyco, arity)), _)) =
+ Pretty.block [
+ Pretty.str "class instance (",
+ Pretty.str clsname,
+ Pretty.str ", (",
+ Pretty.str tyco,
+ Pretty.str ", ",
+ Pretty.enum "," "[" "]" (map (Pretty.enum "," "{" "}" o
+ map Pretty.str o snd) arity),
+ Pretty.str "))"
+ ];
+
+fun pretty_module code =
+ Pretty.chunks (map (fn (name, def) => Pretty.block
+ [Pretty.str name, Pretty.str " :=", Pretty.brk 1, pretty_def def])
+ (AList.make (Graph.get_node code) (Graph.strong_conn code |> flat |> rev)));
+
+fun pretty_deps code =
+ let
+ fun one_node key =
+ let
+ val preds_ = Graph.imm_preds code key;
+ val succs_ = Graph.imm_succs code key;
+ val mutbs = gen_inter (op =) (preds_, succs_);
+ val preds = subtract (op =) mutbs preds_;
+ val succs = subtract (op =) mutbs succs_;
+ in
+ (Pretty.block o Pretty.fbreaks) (
+ Pretty.str key
+ :: map (fn s => Pretty.str ("<-> " ^ s)) mutbs
+ @ map (fn s => Pretty.str ("<-- " ^ s)) preds
+ @ map (fn s => Pretty.str ("--> " ^ s)) succs
+ )
+ end
+ in
+ code
+ |> Graph.strong_conn
+ |> flat
+ |> rev
+ |> map one_node
+ |> Pretty.chunks
+ end;
+
+end; (*local*)
-(** lookup table **)
+(** theory data **)
+
+datatype syntax_expr = SyntaxExpr of {
+ class: ((string * (string -> string option)) * serial) Symtab.table,
+ inst: unit Symtab.table,
+ tyco: (itype pretty_syntax * serial) Symtab.table,
+ const: (iterm pretty_syntax * serial) Symtab.table
+};
-val serializers =
- Symtab.empty
- |> fold (fn (name, f) => Symtab.update_new (name, f name))
- [("SML", ml_from_thingol), ("Haskell", hs_from_thingol)];
+fun mk_syntax_expr ((class, inst), (tyco, const)) =
+ SyntaxExpr { class = class, inst = inst, tyco = tyco, const = const };
+fun map_syntax_expr f (SyntaxExpr { class, inst, tyco, const }) =
+ mk_syntax_expr (f ((class, inst), (tyco, const)));
+fun merge_syntax_expr (SyntaxExpr { class = class1, inst = inst1, tyco = tyco1, const = const1 },
+ SyntaxExpr { class = class2, inst = inst2, tyco = tyco2, const = const2 }) =
+ mk_syntax_expr (
+ (Symtab.merge (eq_snd (op =)) (class1, class2),
+ Symtab.merge (op =) (inst1, inst2)),
+ (Symtab.merge (eq_snd (op =)) (tyco1, tyco2),
+ Symtab.merge (eq_snd (op =)) (const1, const2))
+ );
+
+datatype syntax_modl = SyntaxModl of {
+ merge: string Symtab.table,
+ prolog: Pretty.T Symtab.table
+};
-fun check_serializer target =
- case Symtab.lookup serializers target
- of SOME seri => ()
- | NONE => error ("Unknown code target language: " ^ quote target);
+fun mk_syntax_modl (merge, prolog) =
+ SyntaxModl { merge = merge, prolog = prolog };
+fun map_syntax_modl f (SyntaxModl { merge, prolog }) =
+ mk_syntax_modl (f (merge, prolog));
+fun merge_syntax_modl (SyntaxModl { merge = merge1, prolog = prolog1 },
+ SyntaxModl { merge = merge2, prolog = prolog2 }) =
+ mk_syntax_modl (
+ Symtab.merge (op =) (merge1, merge2),
+ Symtab.merge (op =) (prolog1, prolog2)
+ );
-fun parse_serializer target =
- case Symtab.lookup serializers target
- of SOME seri => seri >> (fn seri' => fn thy => serialize thy seri' target)
- | NONE => Scan.fail_with (fn _ => "Unknown code target language: " ^ quote target) ();
+type serializer = string -> Args.T list
+-> (string -> (string * (string -> string option)) option)
+ * (string
+ -> (int
+ * (fixity
+ -> (fixity
+ -> itype -> Pretty.T)
+ -> itype list -> Pretty.T))
+ option)
+ * (string
+ -> (int
+ * (fixity
+ -> (fixity
+ -> iterm -> Pretty.T)
+ -> iterm list -> Pretty.T))
+ option)
+ -> string list * string list option
+ -> CodegenThingol.code -> unit;
+
+datatype target = Target of {
+ serial: serial,
+ serializer: serializer,
+ syntax_expr: syntax_expr,
+ syntax_modl: syntax_modl
+};
-fun map_target_data target f =
+fun mk_target (serial, (serializer, (syntax_expr, syntax_modl))) =
+ Target { serial = serial, serializer = serializer, syntax_expr = syntax_expr, syntax_modl = syntax_modl };
+fun map_target f ( Target { serial, serializer, syntax_expr, syntax_modl } ) =
+ mk_target (f (serial, (serializer, (syntax_expr, syntax_modl))));
+fun merge_target target (Target { serial = serial1, serializer = serializer, syntax_expr = syntax_expr1, syntax_modl = syntax_modl1 },
+ Target { serial = serial2, serializer = _, syntax_expr = syntax_expr2, syntax_modl = syntax_modl2 }) =
+ if serial1 = serial2 then
+ mk_target (serial1, (serializer,
+ (merge_syntax_expr (syntax_expr1, syntax_expr2),
+ merge_syntax_modl (syntax_modl1, syntax_modl2))
+ ))
+ else
+ error ("Incompatible serializers: " ^ quote target);
+
+structure CodegenSerializerData = TheoryDataFun
+(struct
+ val name = "Pure/codegen_serializer";
+ type T = target Symtab.table;
+ val empty = Symtab.empty;
+ val copy = I;
+ val extend = I;
+ fun merge _ = Symtab.join merge_target;
+ fun print _ _ = ();
+end);
+
+fun the_serializer (Target { serializer, ... }) = serializer;
+fun the_syntax_expr (Target { syntax_expr = SyntaxExpr x, ... }) = x;
+fun the_syntax_modl (Target { syntax_modl = SyntaxModl x, ... }) = x;
+
+fun add_serializer (target, seri) thy =
let
- val _ = check_serializer target;
+ val _ = case Symtab.lookup (CodegenSerializerData.get thy) target
+ of SOME _ => warning ("overwriting existing serializer " ^ quote target)
+ | NONE => ();
in
- CodegenSerializerData.map (
- (Symtab.map_entry target (fn { syntax_class, syntax_inst, syntax_tyco, syntax_const } =>
- let
- val (syntax_class, syntax_inst, syntax_tyco, syntax_const) =
- f (syntax_class, syntax_inst, syntax_tyco, syntax_const)
- in {
- syntax_class = syntax_class,
- syntax_inst = syntax_inst,
- syntax_tyco = syntax_tyco,
- syntax_const = syntax_const } : target_data
- end
- ))
- )
+ thy
+ |> (CodegenSerializerData.map oo Symtab.map_default)
+ (target, mk_target (serial (), (seri,
+ (mk_syntax_expr ((Symtab.empty, Symtab.empty), (Symtab.empty, Symtab.empty)),
+ mk_syntax_modl (Symtab.empty, Symtab.empty)))))
+ (map_target (fn (serial, (_, syntax)) => (serial, (seri, syntax))))
end;
+val _ = Context.add_setup (
+ CodegenSerializerData.init
+ #> add_serializer ("SML", ml_from_thingol)
+ #> add_serializer ("Haskell", hs_from_thingol)
+);
+
+fun get_serializer thy (target, args) cs =
+ let
+ val data = case Symtab.lookup (CodegenSerializerData.get thy) target
+ of SOME data => data
+ | NONE => error ("Unknown code target language: " ^ quote target);
+ val seri = the_serializer data;
+ val { class, inst, tyco, const } = the_syntax_expr data;
+ fun fun_of sys = (Option.map fst oo Symtab.lookup) sys;
+ in
+ seri target args (fun_of class, fun_of tyco, fun_of const)
+ (Symtab.keys class @ Symtab.keys inst @ Symtab.keys tyco @ Symtab.keys const, cs)
+ end;
+
+fun has_serialization f thy targets name =
+ forall (
+ is_some o (fn tab => Symtab.lookup tab name) o f o the_syntax_expr o the
+ o (Symtab.lookup ((CodegenSerializerData.get) thy))
+ ) targets;
+
+val tyco_has_serialization = has_serialization #tyco;
+val const_has_serialization = has_serialization #const;
+
+fun eval_term thy =
+ let
+ val target = "SML";
+ val data = case Symtab.lookup (CodegenSerializerData.get thy) target
+ of SOME data => data
+ | NONE => error ("Unknown code target language: " ^ quote target);
+ val { class, inst, tyco, const } = the_syntax_expr data;
+ fun fun_of sys = (Option.map fst oo Symtab.lookup) sys;
+ in
+ eval_term_proto thy (fun_of class, fun_of tyco, fun_of const)
+ (Symtab.keys class @ Symtab.keys inst @ Symtab.keys tyco @ Symtab.keys const)
+ end;
+
+
(** target syntax interfaces **)
local
+fun map_syntax_exprs target f thy =
+ let
+ val _ = if is_some (Symtab.lookup (CodegenSerializerData.get thy) target)
+ then ()
+ else error ("Unknown code target language: " ^ quote target);
+ in
+ thy
+ |> (CodegenSerializerData.map o Symtab.map_entry target o map_target
+ o apsnd o apsnd o apfst o map_syntax_expr) f
+ end;
+
fun gen_add_syntax_class prep_class prep_const target raw_class (syntax, raw_ops) thy =
let
val cls = prep_class thy raw_class
val class = CodegenNames.class thy cls;
- fun mk_classop (c, _) = case AxClass.class_of_param thy c
- of SOME class' => if cls = class' then c
+ fun mk_classop (const as (c, _)) = case AxClass.class_of_param thy c
+ of SOME class' => if cls = class' then CodegenNames.const thy const
else error ("Not a class operation for class " ^ quote class ^ ": " ^ quote c)
| NONE => error ("Not a class operation: " ^ quote c)
val ops = (map o apfst) (mk_classop o prep_const thy) raw_ops;
val syntax_ops = AList.lookup (op =) ops;
in
thy
- |> map_target_data target (fn (syntax_class, syntax_inst, syntax_tyco, syntax_const) =>
- (syntax_class |> Symtab.update (class,
- ((syntax, syntax_ops), stamp ())),
- syntax_inst, syntax_tyco, syntax_const))
+ |> (map_syntax_exprs target o apfst o apfst)
+ (Symtab.update (class, ((syntax, syntax_ops), serial ())))
end;
fun gen_add_syntax_inst prep_class prep_tyco target (raw_tyco, raw_class) thy =
@@ -1353,9 +1639,8 @@
val inst = CodegenNames.instance thy (prep_class thy raw_class, prep_tyco thy raw_tyco);
in
thy
- |> map_target_data target (fn (syntax_class, syntax_inst, syntax_tyco, syntax_const) =>
- (syntax_class, syntax_inst |> Symtab.update (inst, ()),
- syntax_tyco, syntax_const))
+ |> (map_syntax_exprs target o apfst o apsnd)
+ (Symtab.update (inst, ()))
end;
fun gen_add_syntax_tyco prep_tyco raw_tyco target syntax thy =
@@ -1363,9 +1648,8 @@
val tyco = (CodegenNames.tyco thy o prep_tyco thy) raw_tyco;
in
thy
- |> map_target_data target (fn (syntax_class, syntax_inst, syntax_tyco, syntax_const) =>
- (syntax_class, syntax_inst, syntax_tyco
- |> Symtab.update (tyco, (syntax, stamp ())), syntax_const))
+ |> (map_syntax_exprs target o apsnd o apfst)
+ (Symtab.update (tyco, (syntax, serial ())))
end;
fun gen_add_syntax_const prep_const raw_c target syntax thy =
@@ -1374,9 +1658,8 @@
val c'' = CodegenNames.const thy c';
in
thy
- |> map_target_data target (fn (syntax_class, syntax_inst, syntax_tyco, syntax_const) =>
- (syntax_class, syntax_inst, syntax_tyco, syntax_const
- |> Symtab.update (c'', (syntax, stamp ()))))
+ |> (map_syntax_exprs target o apsnd o apsnd)
+ (Symtab.update (c'', (syntax, serial ())))
end;
fun read_type thy raw_tyco =
--- a/src/Pure/Tools/codegen_thingol.ML Sat Oct 07 02:47:33 2006 +0200
+++ b/src/Pure/Tools/codegen_thingol.ML Sat Oct 07 07:41:56 2006 +0200
@@ -34,16 +34,15 @@
(*((discriminendum term (td), discriminendum type (ty)),
[(selector pattern (p), body term (t))] (bs)),
pure term (t0))*)
+ val `--> : itype list * itype -> itype;
+ val `$$ : iterm * iterm list -> iterm;
+ val `|--> : (vname * itype) list * iterm -> iterm;
+ type typscheme = (vname * sort) list * itype;
end;
signature CODEGEN_THINGOL =
sig
include BASIC_CODEGEN_THINGOL;
- val `--> : itype list * itype -> itype;
- val `$$ : iterm * iterm list -> iterm;
- val `|--> : (vname * itype) list * iterm -> iterm;
- val pretty_itype: itype -> Pretty.T;
- val pretty_iterm: iterm -> 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;
@@ -52,19 +51,15 @@
val unfold_let: iterm -> ((iterm * itype) * iterm) list * iterm;
val unfold_const_app: iterm ->
((string * (inst list list * itype)) * iterm list) option;
- val add_constnames: iterm -> string list -> string list;
- val add_varnames: iterm -> string list -> string list;
- val add_unbound_varnames: iterm -> string list -> string list;
- val is_pat: (string -> bool) -> iterm -> bool;
- val vars_distinct: iterm list -> bool;
val map_pure: (iterm -> 'a) -> iterm -> 'a;
val eta_expand: (string * (inst list list * itype)) * iterm list -> int -> iterm;
+ val fold_constnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;
+ val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;
+ val fold_unbound_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;
- type typscheme = (vname * sort) list * itype;
datatype def =
Bot
| Fun of (iterm list * iterm) list * typscheme
- | Typesyn of typscheme
| Datatype of (vname * sort) list * (string * itype list) list
| Datatypecons of string
| Class of class list * (vname * (string * itype) list)
@@ -72,39 +67,25 @@
| Classinst of (class * (string * (vname * sort) list))
* ((class * (string * inst list list)) list
* (string * iterm) list);
- type module;
+ type code = def Graph.T;
type transact;
- type 'dst transact_fin;
- val pretty_def: def -> Pretty.T;
- val pretty_module: module -> Pretty.T;
- val pretty_deps: module -> Pretty.T;
- val empty_module: module;
- val get_def: module -> string -> def;
- val merge_module: module * module -> module;
- val diff_module: module * module -> (string * def) list;
- val project_module: string list -> module -> module;
- val purge_module: string list -> module -> module;
-(* val flat_funs_datatypes: module -> (string * def) list; *)
- val add_eval_def: string (*shallow name space*) * iterm -> module -> string * module;
- val delete_garbage: string list (*hidden definitions*) -> module -> module;
- val ensure_def: (string -> transact -> def transact_fin) -> bool -> string
+ val empty_code: code;
+ val get_def: code -> string -> def;
+ val merge_code: code * code -> code;
+ val project_code: string list -> code -> code;
+ val add_eval_def: string (*shallow name space*) * iterm -> code -> string * code;
+ val delete_garbage: string list (*hidden definitions*) -> code -> code;
+
+ val ensure_def: (transact -> def * code) -> bool -> string
-> string -> transact -> transact;
- val succeed: 'a -> transact -> 'a transact_fin;
- val fail: string -> transact -> 'a transact_fin;
+ val succeed: 'a -> transact -> 'a * code;
+ val fail: string -> transact -> 'a * code;
val message: string -> (transact -> 'a) -> transact -> 'a;
- val start_transact: string option -> (transact -> 'a * transact) -> module -> 'a * module;
- val elim_classes: module -> (iterm list * iterm) list * typscheme -> (iterm list * iterm) list * itype;
+ val start_transact: string option -> (transact -> 'a * transact) -> code -> 'a * code;
val trace: bool ref;
val tracing: ('a -> string) -> 'a -> 'a;
val soft_exc: bool ref;
-
- val serialize:
- ((string -> string -> string) -> string -> (string * def) list -> 'a option)
- -> ((string -> string) -> string list -> (string * string) * 'a list -> 'a option)
- -> (string -> string option)
- -> (string * string -> string)
- -> string list list -> string -> module -> 'a option;
end;
structure CodegenThingol: CODEGEN_THINGOL =
@@ -168,7 +149,7 @@
class operation names clsop (op)
arbitrary name s
- v, c, co, clsop also annotated with types usw.
+ v, c, co, clsop also annotated with types etc.
constructs:
sort sort
@@ -184,44 +165,6 @@
val op `$$ = Library.foldl (op `$);
val op `|--> = Library.foldr (op `|->);
-val pretty_typparms =
- Pretty.list "(" ")" o Pretty.commas o map (fn (v, sort) => (Pretty.block o Pretty.breaks)
- [Pretty.str v, Pretty.str "::", Pretty.enum "&" "" "" (map Pretty.str sort)]);
-
-fun pretty_itype (tyco `%% tys) =
- Pretty.enum "" "(" ")" (Pretty.str tyco :: map pretty_itype tys)
- | pretty_itype (ty1 `-> ty2) =
- Pretty.enum "" "(" ")" [pretty_itype ty1, Pretty.str "->", pretty_itype ty2]
- | pretty_itype (ITyVar v) =
- Pretty.str v;
-
-fun pretty_iterm (IConst (c, _)) =
- Pretty.str c
- | pretty_iterm (IVar v) =
- Pretty.str ("?" ^ v)
- | pretty_iterm (t1 `$ t2) =
- (Pretty.enclose "(" ")" o Pretty.breaks)
- [pretty_iterm t1, pretty_iterm t2]
- | pretty_iterm ((v, ty) `|-> t) =
- (Pretty.enclose "(" ")" o Pretty.breaks)
- [Pretty.str v, Pretty.str "::", pretty_itype ty, Pretty.str "|->", pretty_iterm t]
- | pretty_iterm (INum (n, _)) =
- (Pretty.str o IntInf.toString) n
- | pretty_iterm (IChar (h, _)) =
- (Pretty.str o quote) h
- | pretty_iterm (ICase (((t, _), bs), _)) =
- (Pretty.enclose "(" ")" o Pretty.breaks) [
- Pretty.str "case",
- pretty_iterm t,
- Pretty.enclose "(" ")" (map (fn (p, t) =>
- (Pretty.block o Pretty.breaks) [
- pretty_iterm p,
- Pretty.str "=>",
- pretty_iterm t
- ]
- ) bs)
- ];
-
val unfold_fun = unfoldr
(fn op `-> ty => SOME ty
| _ => NONE);
@@ -245,55 +188,6 @@
of (IConst c, ts) => SOME (c, ts)
| _ => NONE;
-fun map_itype _ (ty as ITyVar _) =
- ty
- | map_itype f (tyco `%% tys) =
- tyco `%% map f tys
- | map_itype f (ty1 `-> ty2) =
- f ty1 `-> f ty2;
-
-fun eq_ityp ((vs1, ty1), (vs2, ty2)) =
- let
- exception NO_MATCH;
- fun eq_typparms subs vs1 vs2 =
- map (fn (v : string, sort : string list) => case AList.lookup (op =) subs v
- of NONE => raise NO_MATCH
- | SOME (v' : string) => case AList.lookup (op =) vs2 v'
- of NONE => raise NO_MATCH
- | SOME sort' => if sort <> sort' then raise NO_MATCH else ()) vs1
- fun eq (ITyVar v1) (ITyVar v2) subs =
- (case AList.lookup (op =) subs v1
- of NONE => subs |> AList.update (op =) (v1, v2)
- | SOME v1' =>
- if v1' <> v2
- then raise NO_MATCH
- else subs)
- | eq (tyco1 `%% tys1) (tyco2 `%% tys2) subs =
- if tyco1 <> tyco2
- then raise NO_MATCH
- else subs |> fold2 eq tys1 tys2
- | eq (ty11 `-> ty12) (ty21 `-> ty22) subs =
- subs |> eq ty11 ty21 |> eq ty12 ty22
- | eq _ _ _ = raise NO_MATCH;
- in
- (eq_typparms vs1 vs2; eq ty1 ty2 []; true)
- handle NO_MATCH => false
- end;
-
-fun instant_itype f =
- let
- fun instant (ITyVar v) = f v
- | instant ty = map_itype instant ty;
- in instant end;
-
-fun is_pat is_cons (IConst (c, _)) = is_cons c
- | is_pat _ (IVar _) = true
- | is_pat is_cons (t1 `$ t2) =
- is_pat is_cons t1 andalso is_pat is_cons t2
- | is_pat _ (INum _) = true
- | is_pat _ (IChar _) = true
- | is_pat _ _ = false;
-
fun map_pure f (t as IConst _) =
f t
| map_pure f (t as IVar _) =
@@ -309,82 +203,63 @@
| map_pure f (ICase (_, t0)) =
f t0;
-fun add_constnames (IConst (c, _)) =
- insert (op =) c
- | add_constnames (IVar _) =
- I
- | add_constnames (t1 `$ t2) =
- add_constnames t1 #> add_constnames t2
- | add_constnames (_ `|-> t) =
- add_constnames t
- | add_constnames (INum (_, t0)) =
- add_constnames t0
- | add_constnames (IChar (_, t0)) =
- add_constnames t0
- | add_constnames (ICase (_, t0)) =
- add_constnames t0;
+fun fold_aiterms f (t as IConst _) =
+ f t
+ | fold_aiterms f (t as IVar _) =
+ f t
+ | fold_aiterms f (t1 `$ t2) =
+ fold_aiterms f t1 #> fold_aiterms f t2
+ | fold_aiterms f (t as _ `|-> t') =
+ f t #> fold_aiterms f t'
+ | fold_aiterms f (INum (_, t0)) =
+ fold_aiterms f t0
+ | fold_aiterms f (IChar (_, t0)) =
+ fold_aiterms f t0
+ | fold_aiterms f (ICase (_, t0)) =
+ fold_aiterms f t0;
-fun add_varnames (IConst _) =
- I
- | add_varnames (IVar v) =
- insert (op =) v
- | add_varnames (t1 `$ t2) =
- add_varnames t1 #> add_varnames t2
- | add_varnames ((v, _) `|-> t) =
- insert (op =) v #> add_varnames t
- | add_varnames (INum (_, t)) =
- add_varnames t
- | add_varnames (IChar (_, t)) =
- add_varnames t
- | add_varnames (ICase (((td, _), bs), _)) =
- add_varnames td #> fold (fn (p, t) => add_varnames p #> add_varnames t) bs;
+fun fold_constnames f =
+ let
+ fun add (IConst (c, _)) = f c
+ | add _ = I;
+ in fold_aiterms add end;
-fun add_unbound_varnames (IConst _) =
- I
- | add_unbound_varnames (IVar v) =
- insert (op =) v
- | add_unbound_varnames (t1 `$ t2) =
- add_unbound_varnames t1 #> add_unbound_varnames t2
- | add_unbound_varnames ((v, _) `|-> t) =
- I
- | add_unbound_varnames (INum (_, t)) =
- add_unbound_varnames t
- | add_unbound_varnames (IChar (_, t)) =
- add_unbound_varnames t
- | add_unbound_varnames (ICase (((td, _), bs), _)) =
- add_unbound_varnames td #> fold (fn (p, t) => add_unbound_varnames p #> add_unbound_varnames t) bs;
+fun fold_varnames f =
+ let
+ fun add (IVar v) = f v
+ | add ((v, _) `|-> _) = f v
+ | add _ = I;
+ in fold_aiterms add end;
-fun vars_distinct ts =
+fun fold_unbound_varnames f =
let
- fun distinct _ NONE =
- NONE
- | distinct (IConst _) x =
- x
- | distinct (IVar v) (SOME vs) =
- if member (op =) vs v then NONE else SOME (v::vs)
- | distinct (t1 `$ t2) x =
- x |> distinct t1 |> distinct t2
- | distinct (_ `|-> t) x =
- x |> distinct t
- | distinct (INum _) x =
- x
- | distinct (IChar _) x =
- x
- | distinct (ICase (((td, _), bs), _)) x =
- x |> distinct td |> fold (fn (p, t) => distinct p #> distinct t) bs;
- in is_some (fold distinct ts (SOME [])) end;
+ fun add _ (IConst _) =
+ I
+ | add vs (IVar v) =
+ if not (member (op =) vs v) then f v else I
+ | add vs (t1 `$ t2) =
+ add vs t1 #> add vs t2
+ | add vs ((v, _) `|-> t) =
+ add (insert (op =) v vs) t
+ | add vs (INum (_, t)) =
+ add vs t
+ | add vs (IChar (_, t)) =
+ add vs t
+ | add vs (ICase (_, t0)) =
+ add vs t0
+ in add [] end;
fun eta_expand (c as (_, (_, ty)), ts) k =
let
val j = length ts;
val l = k - j;
val tys = (curry Library.take l o curry Library.drop j o fst o unfold_fun) ty;
- val vs_tys = Name.names (fold Name.declare (fold add_varnames ts []) Name.context) "a" tys;
+ val ctxt = (fold o fold_varnames) Name.declare ts Name.context;
+ val vs_tys = Name.names ctxt "a" tys;
in vs_tys `|--> IConst c `$$ ts @ map (fn (v, _) => IVar v) vs_tys end;
-
-(** language module system - definitions, modules, transactions **)
+(** definitions, transactions **)
(* type definitions *)
@@ -392,7 +267,6 @@
datatype def =
Bot
| Fun of (iterm list * iterm) list * typscheme
- | Typesyn of typscheme
| Datatype of (vname * sort) list * (string * itype list) list
| Datatypecons of string
| Class of class list * (vname * (string * itype) list)
@@ -400,589 +274,61 @@
| Classinst of (class * (string * (vname * sort) list))
* ((class * (string * inst list list)) list
* (string * iterm) list);
-
-datatype node = Def of def | Module of node Graph.T;
-type module = node Graph.T;
-type transact = Graph.key option * module;
-type 'dst transact_fin = 'dst * module;
-exception FAIL of string list * exn option;
-
val eq_def = (op =) : def * def -> bool;
-(* simple diagnosis *)
-
-fun pretty_def Bot =
- Pretty.str "<Bot>"
- | pretty_def (Fun (eqs, (vs, ty))) =
- Pretty.enum " |" "" "" (
- map (fn (ps, body) =>
- Pretty.block [
- Pretty.enum "," "[" "]" (map pretty_iterm ps),
- Pretty.str " |->",
- Pretty.brk 1,
- pretty_iterm body,
- Pretty.str "::",
- pretty_typparms vs,
- Pretty.str "/",
- pretty_itype ty
- ]) eqs
- )
- | pretty_def (Typesyn (vs, ty)) =
- Pretty.block [
- pretty_typparms vs,
- Pretty.str " |=> ",
- pretty_itype ty
- ]
- | pretty_def (Datatype (vs, cs)) =
- Pretty.block [
- pretty_typparms vs,
- Pretty.str " |=> ",
- Pretty.enum " |" "" ""
- (map (fn (c, tys) => (Pretty.block o Pretty.breaks)
- (Pretty.str c :: map pretty_itype tys)) cs)
- ]
- | pretty_def (Datatypecons dtname) =
- Pretty.str ("cons " ^ dtname)
- | pretty_def (Class (supcls, (v, mems))) =
- Pretty.block [
- Pretty.str ("class var " ^ v ^ " extending "),
- Pretty.enum "," "[" "]" (map Pretty.str supcls),
- Pretty.str " with ",
- Pretty.enum "," "[" "]"
- (map (fn (m, ty) => Pretty.block
- [Pretty.str (m ^ "::"), pretty_itype ty]) mems)
- ]
- | pretty_def (Classmember clsname) =
- Pretty.block [
- Pretty.str "class member belonging to ",
- Pretty.str clsname
- ]
- | pretty_def (Classinst ((clsname, (tyco, arity)), _)) =
- Pretty.block [
- Pretty.str "class instance (",
- Pretty.str clsname,
- Pretty.str ", (",
- Pretty.str tyco,
- Pretty.str ", ",
- Pretty.enum "," "[" "]" (map (Pretty.enum "," "{" "}" o
- map Pretty.str o snd) arity),
- Pretty.str "))"
- ];
-
-fun pretty_module modl =
- let
- fun pretty (name, Module modl) =
- Pretty.block (
- Pretty.str ("module " ^ name ^ " {")
- :: Pretty.brk 1
- :: Pretty.chunks (map pretty (AList.make (Graph.get_node modl)
- (Graph.strong_conn modl |> flat |> rev)))
- :: Pretty.str "}" :: nil
- )
- | pretty (name, Def def) =
- Pretty.block [Pretty.str name, Pretty.str " :=", Pretty.brk 1, pretty_def def]
- in pretty ("//", Module modl) end;
-
-fun pretty_deps modl =
- let
- fun one_node key =
- let
- val preds_ = Graph.imm_preds modl key;
- val succs_ = Graph.imm_succs modl key;
- val mutbs = gen_inter (op =) (preds_, succs_);
- val preds = subtract (op =) mutbs preds_;
- val succs = subtract (op =) mutbs succs_;
- in
- (Pretty.block o Pretty.fbreaks) (
- Pretty.str key
- :: map (fn s => Pretty.str ("<-> " ^ s)) mutbs
- @ map (fn s => Pretty.str ("<-- " ^ s)) preds
- @ map (fn s => Pretty.str ("--> " ^ s)) succs
- @ (the_list oo Option.mapPartial)
- ((fn Module modl' => SOME (pretty_deps modl')
- | _ => NONE) o Graph.get_node modl) (SOME key)
- )
- end
- in
- modl
- |> Graph.strong_conn
- |> flat
- |> rev
- |> map one_node
- |> Pretty.chunks
- end;
+type code = def Graph.T;
+type transact = Graph.key option * code;
+exception FAIL of string list * exn option;
-(* name handling *)
+(* abstract code *)
-fun dest_name name =
- let
- val name' = NameSpace.unpack name
- val (name'', name_base) = split_last name'
- val (modl, shallow) = split_last name''
- in (modl, NameSpace.pack [shallow, name_base]) end
- handle Empty => error ("Not a qualified name: " ^ quote name);
-
-fun dest_modl (Module m) = m;
-fun dest_def (Def d) = d;
-
-
-(* modules *)
+val empty_code = Graph.empty : code; (*read: "depends on"*)
-val empty_module = Graph.empty; (*read: "depends on"*)
+val get_def = Graph.get_node;
-fun get_def modl name =
- case dest_name name
- of (modlname, base) =>
- let
- fun get (Module node) [] =
- (dest_def o Graph.get_node node) base
- | get (Module node) (m::ms) =
- get (Graph.get_node node m) ms
- in get (Module modl) modlname end;
-
-fun is_def modl name =
- case try (get_def modl) name
- of NONE => false
- | SOME Bot => false
- | _ => true;
+fun ensure_bot name = Graph.default_node (name, Bot);
-fun add_def (name, def) =
- let
- val (modl, base) = dest_name name;
- fun add [] =
- Graph.new_node (base, Def def)
- | add (m::ms) =
- Graph.default_node (m, Module empty_module)
- #> Graph.map_node m (Module o add ms o dest_modl)
- in add modl end;
-
-fun map_def name f =
- let
- val (modl, base) = dest_name name;
- fun mapp [] =
- Graph.map_node base (Def o f o dest_def)
- | mapp (m::ms) =
- Graph.map_node m (Module o mapp ms o dest_modl)
- in mapp modl end;
-
-fun ensure_bot name =
- let
- val (modl, base) = dest_name name;
- fun ensure [] module =
- (case try (Graph.get_node module) base
- of NONE =>
- module
- |> Graph.new_node (base, Def Bot)
- | SOME (Module _) => error ("Module already present: " ^ quote name)
- | _ => module)
- | ensure (m::ms) module =
- module
- |> Graph.default_node (m, Module empty_module)
- |> Graph.map_node m (Module o ensure ms o dest_modl)
- in ensure modl end;
-
-fun add_def_incr strict (name, Bot) module =
- (case try (get_def module) name
- of NONE => if strict then error "Attempted to add Bot to module"
- else map_def name (K Bot) module
- | SOME Bot => if strict then error "Attempted to add Bot to module"
- else map_def name (K Bot) module
- | SOME _ => module)
- | add_def_incr _ (name, def) module =
- (case try (get_def module) name
- of NONE => add_def (name, def) module
- | SOME Bot => map_def name (K def) module
+fun add_def_incr strict (name, Bot) code =
+ (case the_default Bot (try (get_def code) name)
+ of Bot => if strict then error "Attempted to add Bot to code"
+ else Graph.map_node name (K Bot) code
+ | _ => code)
+ | add_def_incr _ (name, def) code =
+ (case try (get_def code) name
+ of NONE => Graph.new_node (name, def) code
+ | SOME Bot => Graph.map_node name (K def) code
| SOME def' => if eq_def (def, def')
- then module
+ then code
else error ("Tried to overwrite definition " ^ quote name));
-fun add_dep (name1, name2) modl =
- if name1 = name2 then modl
- else
- let
- val m1 = dest_name name1 |> apsnd single |> (op @);
- val m2 = dest_name name2 |> apsnd single |> (op @);
- val (ms, (r1, r2)) = chop_prefix (op =) (m1, m2);
- val (ms, (s1::r1, s2::r2)) = chop_prefix (op =) (m1, m2);
- val add_edge =
- if null r1 andalso null r2
- then Graph.add_edge
- else fn edge => fn gr => (Graph.add_edge_acyclic edge gr
- handle Graph.CYCLES _ =>
- error ("Adding dependency "
- ^ quote name1 ^ " -> " ^ quote name2 ^ " would result in module dependency cycle"))
- fun add [] node =
- node
- |> add_edge (s1, s2)
- | add (m::ms) node =
- node
- |> Graph.map_node m (Module o add ms o dest_modl);
- in add ms modl end;
-
-fun merge_module modl12 =
- let
- fun join_module _ (Module m1, Module m2) =
- Module (merge_module (m1, m2))
- | join_module name (Def d1, Def d2) =
- if eq_def (d1, d2) then Def d1 else Def Bot
- | join_module name _ = raise Graph.DUP name
- in Graph.join join_module modl12 end;
+fun add_dep (dep as (name1, name2)) =
+ if name1 = name2 then I else Graph.add_edge dep;
-fun diff_module modl12 =
- let
- fun diff_entry prefix modl2 (name, Def def1) =
- let
- val e2 = try (Graph.get_node modl2) name
- in if is_some e2 andalso eq_def (def1, (dest_def o the) e2)
- then I
- else cons (NameSpace.pack (prefix @ [name]), def1)
- end
- | diff_entry prefix modl2 (name, Module modl1) =
- diff_modl (prefix @ [name]) (modl1,
- (the_default empty_module o Option.map dest_modl o try (Graph.get_node modl2)) name)
- and diff_modl prefix (modl1, modl2) =
- fold (diff_entry prefix modl2)
- ((AList.make (Graph.get_node modl1) o flat o Graph.strong_conn) modl1)
- in diff_modl [] modl12 [] end;
-
-fun project_module names modl =
- let
- datatype pathnode = PN of (string list * (string * pathnode) list);
- fun mk_ipath ([], base) (PN (defs, modls)) =
- PN (base :: defs, modls)
- | mk_ipath (n::ns, base) (PN (defs, modls)) =
- modls
- |> AList.default (op =) (n, PN ([], []))
- |> AList.map_entry (op =) n (mk_ipath (ns, base))
- |> (pair defs #> PN);
- fun select (PN (defs, modls)) (Module module) =
- module
- |> Graph.project (member (op =) ((*!*) Graph.all_succs module (defs @ map fst modls)))
- |> fold (fn (name, modls) => Graph.map_node name (select modls)) modls
- |> Module;
- in
- Module modl
- |> select (fold (mk_ipath o dest_name)
- (filter NameSpace.is_qualified names) (PN ([], [])))
- |> dest_modl
- end;
+val merge_code = Graph.join (fn _ => fn def12 => if eq_def def12 then fst def12 else Bot);
-fun purge_module names modl =
- let
- fun split_names names =
- fold
- (fn ([], name) => apfst (cons name)
- | (m::ms, name) => apsnd (AList.default (op =) (m : string, [])
- #> AList.map_entry (op =) m (cons (ms, name))))
- names ([], []);
- fun purge names (Module modl) =
- let
- val (ndefs, nmodls) = split_names names;
- in
- modl
- |> Graph.del_nodes (Graph.all_preds modl ndefs)
- |> Graph.del_nodes ndefs
- |> Graph.del_nodes (Graph.all_preds modl (map fst nmodls))
- |> fold (fn (nmodl, names') => Graph.map_node nmodl (purge names')) nmodls
- |> Module
- end;
- in
- Module modl
- |> purge (map dest_name names)
- |> dest_modl
- end;
-
-fun flat_module modl =
- maps (
- fn (name, Module modl) => map (apfst (NameSpace.append name)) (flat_module modl)
- | (name, Def def) => [(name, def)]
- ) ((AList.make (Graph.get_node modl) o flat o Graph.strong_conn) modl)
+fun project_code names code =
+ Graph.project (member (op =) (Graph.all_succs code names)) code;
-(*
-(*FIXME: graph-based approach is better.
-* build graph
-* implement flat_classops on sort level, not class level
-* flat_instances bleibt wie es ist
-*)
-fun flat_classops modl =
- let
- fun add_ancestry class anc =
- let
- val SOME (Class (super_classes, (v, ops))) = AList.lookup (op =) modl class
- val super_classees' = filter (not o member (fn (c', (c, _)) => c = c') anc) super_classes;
- in
- [(class, ops)] @ anc
- |> fold add_ancestry super_classees'
- end;
- in
- Symtab.empty
- |> fold (
- fn (class, Class _) =>
- Symtab.update_new (class, maps snd (add_ancestry class []))
- | _ => I
- ) modl
- |> the oo Symtab.lookup
- end;
-
-fun flat_instances modl =
- let
- fun add_ancestry instance instsss anc =
- let
- val SOME (Classinst (_, (super_instances, ops))) = AList.lookup (op =) modl instance;
- val super_instances' = filter (not o member (eq_fst (op =)) anc) super_instances;
- val ops' = map (apsnd (rpair instsss)) ops;
- (*FIXME: build types*)
- in
- [(instance, ops')] @ anc
- |> fold (fn (_, (instance, instss)) => add_ancestry instance (instss :: instsss)) super_instances'
- end;
- in
- Symtab.empty
- |> fold (
- fn (instance, Classinst _) =>
- Symtab.update_new (instance, maps snd (add_ancestry instance [] []))
- | _ => I
- ) modl
- |> the oo Symtab.lookup
- end;
-
-fun flat_fundef classops instdefs is_classop (eqs, (vs, ty)) =
+fun delete_garbage hidden code =
let
- fun fold_map_snd' f (x, ys) = fold_map (f x) ys;
- fun fold_map_snd f (x, ys) = fold_map f ys #-> (fn zs => pair (x, zs));
- val names =
- Name.context
- |> fold Name.declare
- (fold (fn (rhs, lhs) => fold add_varnames rhs #> add_varnames lhs) eqs []);
- val opmap = [] : (string * (string * (string * itype) list) list) list;
- val (params, tys) = (split_list o maps snd o maps snd) opmap;
- (*fun name_ops v' class =
- (fold_map o fold_map_snd')
- (fn (class, v) => fn (c, ty) => Name.variants [c] #-> (fn [p] =>
- pair (class, v') (c, (ty, p))))
- (classops class);
- val (opsmap, _) = (fold_map o fold_map_snd') name_ops vs names;
- (* --> (iterm * itype) list *)*)
- fun flat_inst (Instance (instance, instss)) =
- let
- val xs : (string * (iterm * (itype * inst list list list))) list = instdefs instance
- fun mk_t (t, (ty, instsss)) =
- (Library.foldl (fn (t, instss) => t `$$ map (fst o snd) ((maps o maps) flat_inst instss))
- (t, instss :: instsss), ty)
- in
- map (apsnd mk_t) xs
- end
- | flat_inst (Context (classes, (v, k))) =
- let
- val _ : 'a = classops (hd classes);
- in
- []
- end
- (*
- val parm_map = nth ((the o AList.lookup (op =) octxt) v)
- (if k = ~1 then 0 else k);
- in map (apfst IVar o swap o snd) (case classes
- of class::_ => (the o AList.lookup (op =) parm_map) class
- | _ => (snd o hd) parm_map)*)
- and flat_iterm (e as IConst (c, (lss, ty))) =
- if is_classop c then let
- val tab = (maps o maps) flat_inst lss;
- val SOME (t, _) = AList.lookup (op =) tab c;
- in t end else let
- val (es, tys) = (split_list o map snd) ((maps o maps) flat_inst lss)
- in IConst (c, (replicate (length lss) [], tys `--> ty)) `$$ es end
- | flat_iterm (e as IVar _) =
- e
- | flat_iterm (e1 `$ e2) =
- flat_iterm e1 `$ flat_iterm e2
- | flat_iterm (v_ty `|-> e) =
- v_ty `|-> flat_iterm e
- | flat_iterm (INum (k, e)) =
- INum (k, flat_iterm e)
- | flat_iterm (IChar (s, e)) =
- IChar (s, flat_iterm e)
- | flat_iterm (ICase (((de, dty), es), e)) =
- ICase (((flat_iterm de, dty), map (pairself flat_iterm) es), flat_iterm e);
- fun flat_eq (lhs, rhs) = (map IVar params @ lhs, flat_iterm rhs);
- in (map flat_eq eqs, (map (apsnd (K [])) vs, tys `--> ty)) end;
-
-fun flat_funs_datatypes modl =
- let
- val modl = flat_module modl;
- val classops = flat_classops modl;
- val instdefs = flat_instances modl;
- val is_classop = is_some o AList.lookup (op =) modl;
- in map_filter (
- fn def as (_, Datatype _) => SOME def
- | (name, Fun funn) => SOME (name, (Fun (flat_fundef classops instdefs is_classop funn)))
- | _ => NONE
- ) end;
-*)
-
-val add_deps_of_typparms =
- fold (fn (v : vname, sort : sort) => fold (insert (op =)) sort);
-
-fun add_deps_of_classlookup (Instance (inst, lss)) =
- insert (op =) inst
- #> (fold o fold) add_deps_of_classlookup lss
- | add_deps_of_classlookup (Context (clss, _)) =
- fold (insert (op =)) clss;
-
-fun add_deps_of_type (tyco `%% tys) =
- insert (op =) tyco
- #> fold add_deps_of_type tys
- | add_deps_of_type (ty1 `-> ty2) =
- add_deps_of_type ty1
- #> add_deps_of_type ty2
- | add_deps_of_type (ITyVar v) =
- I;
-
-fun add_deps_of_term (IConst (c, (lss, ty))) =
- insert (op =) c
- #> add_deps_of_type ty
- #> (fold o fold) add_deps_of_classlookup lss
- | add_deps_of_term (IVar _) =
- I
- | add_deps_of_term (e1 `$ e2) =
- add_deps_of_term e1 #> add_deps_of_term e2
- | add_deps_of_term ((_, ty) `|-> e) =
- add_deps_of_type ty
- #> add_deps_of_term e
- | add_deps_of_term (INum _) =
- I
- | add_deps_of_term (IChar (_, e)) =
- add_deps_of_term e
- | add_deps_of_term (ICase (_, e)) =
- add_deps_of_term e;
-
-fun deps_of Bot =
- []
- | deps_of (Fun (eqs, (vs, ty))) =
- []
- |> add_deps_of_typparms vs
- |> add_deps_of_type ty
- |> fold (fn (lhs, rhs) => fold add_deps_of_term lhs #> add_deps_of_term rhs) eqs
- | deps_of (Typesyn (vs, ty)) =
- []
- |> add_deps_of_typparms vs
- |> add_deps_of_type ty
- | deps_of (Datatype (vs, cos)) =
- []
- |> add_deps_of_typparms vs
- |> fold (fn (c, tys) => insert (op =) c #> fold add_deps_of_type tys) cos
- | deps_of (Datatypecons dtco) =
- [dtco]
- | deps_of (Class (supclss, (_, memdecls))) =
- []
- |> fold (insert (op =)) supclss
- |> fold (fn (name, ty) =>
- insert (op =) name
- #> add_deps_of_type ty
- ) memdecls
- | deps_of (Classmember class) =
- [class]
- | deps_of (Classinst ((class, (tyco, vs)), (suparities, memdefs))) =
- []
- |> insert (op =) class
- |> insert (op =) tyco
- |> add_deps_of_typparms vs
- |> fold (fn (supclass, (supinst, lss)) =>
- insert (op =) supclass
- #> insert (op =) supinst
- #> (fold o fold) add_deps_of_classlookup lss
- ) suparities
- |> fold (fn (name, e) =>
- insert (op =) name
- #> add_deps_of_term e
- ) memdefs;
-
-fun delete_garbage hidden modl =
- let
- fun allnames modl =
- let
- val entries = AList.make (Graph.get_node modl) (Graph.keys modl)
- fun is_def (name, Module _) = NONE
- | is_def (name, _) = SOME name;
- fun is_modl (name, Module modl) = SOME (name, modl)
- | is_modl (name, _) = NONE;
- val defs = map_filter is_def entries;
- val modls = map_filter is_modl entries;
- in
- defs
- @ maps (fn (name, modl) => map (NameSpace.append name) (allnames modl)) modls
- end;
- fun alldeps modl =
- let
- val entries = AList.make (Graph.get_node modl) (Graph.keys modl)
- fun is_def (name, Module _) = NONE
- | is_def (name, _) = SOME name;
- fun is_modl (name, Module modl) = SOME (name, modl)
- | is_modl (name, _) = NONE;
- val defs = map_filter is_def entries;
- val modls = map_filter is_modl entries;
- in
- maps (fn name => map (pair (name)) (Graph.imm_succs modl name)) defs
- @ maps (fn (name, modl) => (map o pairself) (NameSpace.append name) (alldeps modl)) modls
- end;
- val names = subtract (op =) hidden (allnames modl);
-(* val _ = writeln "HIDDEN"; *)
-(* val _ = (writeln o commas) hidden; *)
-(* val _ = writeln "NAMES"; *)
-(* val _ = (writeln o commas) names; *)
- fun is_bot name =
- case get_def modl name of Bot => true | _ => false;
- val bots = filter is_bot names;
- val defs = filter (not o is_bot) names;
- val expldeps =
- Graph.empty
- |> fold (fn name => Graph.new_node (name, ())) names
- |> fold (fn name => fold (curry Graph.add_edge name)
- (deps_of (get_def modl name) |> subtract (op =) hidden)) names
- val bots' = fold (insert op =) bots (Graph.all_preds expldeps bots);
- val selected = subtract (op =) bots' names;
-(* val deps = filter (fn (x, y) => member (op =) selected x andalso member (op =) selected y) *)
- val adddeps = maps (fn (n, ns) => map (pair n) ns) (expldeps |> Graph.del_nodes bots' |> Graph.dest);
-(* val _ = writeln "SELECTED";
- val _ = (writeln o commas) selected;
- val _ = writeln "DEPS";
- val _ = (writeln o cat_lines o map (fn (x, y) => x ^ " -> " ^ y)) adddeps; *)
+ fun is_bot name = case get_def code name
+ of Bot => true
+ | _ => false;
+ val names = subtract (op =) hidden (Graph.keys code);
+ val names' = subtract (op =)
+ (Graph.all_preds code (filter is_bot names)) names;
in
- empty_module
- |> fold (fn name => add_def (name, get_def modl name)) selected
-(* |> fold ensure_bot (hidden @ bots') *)
- |> fold (fn (x, y) => ((*writeln ("adding " ^ x ^ " -> " ^ y);*) add_dep (x, y))) adddeps
+ Graph.project (member (op =) names') code
end;
-fun allimports_of modl =
- let
- fun imps_of prfx (Module modl) imps tab =
- let
- val this = NameSpace.pack prfx;
- val name_con = (rev o Graph.strong_conn) modl;
- in
- tab
- |> pair []
- |> fold (fn names => fn (imps', tab) =>
- tab
- |> fold_map (fn name =>
- imps_of (prfx @ [name]) (Graph.get_node modl name) (imps' @ imps)) names
- |-> (fn imps'' => pair (flat imps'' @ imps'))) name_con
- |-> (fn imps' =>
- Symtab.update_new (this, imps' @ imps)
- #> pair (this :: imps'))
- end
- | imps_of prfx (Def _) imps tab =
- ([], tab);
- in snd (imps_of [] (Module modl) [] Symtab.empty) end;
-
fun check_samemodule names =
fold (fn name =>
let
- val modn = (fst o dest_name) name
+ val module_name = (NameSpace.qualifier o NameSpace.qualifier) name
in
- fn NONE => SOME modn
- | SOME mod' => if modn = mod' then SOME modn
+ fn NONE => SOME module_name
+ | SOME module_name' => if module_name = module_name' then SOME module_name
else error ("Inconsistent name prefix for simultanous names: " ^ commas_quote names)
end
) names NONE;
@@ -1002,8 +348,6 @@
Bot
| check_prep_def modl (Fun (eqs, d)) =
Fun (check_funeqs eqs, d)
- | check_prep_def modl (d as Typesyn _) =
- d
| check_prep_def modl (d as Datatype _) =
d
| check_prep_def modl (Datatypecons dtco) =
@@ -1063,13 +407,13 @@
(check_prep_def modl def, modl);
fun invoke_generator name defgen modl =
if ! soft_exc (*that "!" isn't a "not"...*)
- then defgen name (SOME name, modl)
+ then defgen (SOME name, modl)
handle FAIL (msgs, exc) =>
if strict then raise FAIL (msg' :: msgs, exc)
else (Bot, modl)
| e => raise
FAIL (["definition generator for " ^ quote name, msg'], SOME e)
- else defgen name (SOME name, modl)
+ else defgen (SOME name, modl)
handle FAIL (msgs, exc) =>
if strict then raise FAIL (msg' :: msgs, exc)
else (Bot, modl);
@@ -1087,8 +431,7 @@
#> invoke_generator name defgen
#-> (fn def => prep_def def)
#-> (fn def =>
- tracing (fn _ => "addition of " ^ name ^ " := " ^ (Pretty.output o pretty_def) def)
- #> tracing (fn _ => "adding")
+ tracing (fn _ => "adding")
#> add_def_incr strict (name, def)
#> tracing (fn _ => "postprocessing")
#> postprocess_def (name, def)
@@ -1121,143 +464,18 @@
|-> (fn x => fn (_, modl) => (x, modl))
end;
-fun add_eval_def (shallow, e) modl =
+fun add_eval_def (shallow, e) code =
let
val name = "VALUE";
val sname = NameSpace.pack [shallow, name];
in
- modl
- |> add_def (sname, Fun ([([], e)], ([("_", [])], ITyVar "_")))
- |> fold (curry add_dep sname) (add_deps_of_term e [])
+ code
+ |> Graph.new_node (sname, Fun ([([], e)], ([("_", [])], ITyVar "_")))
+ |> fold (curry Graph.add_edge sname) (Graph.keys code) (*FIXME*)
|> pair name
end;
-
-(** eliminating classes in definitions **)
-
-fun elim_classes modl (eqs, (vs, ty)) =
- let
- fun elim_expr _ = ();
- in (error ""; (eqs, ty)) end;
-
-(** generic serialization **)
-
-(* resolving *)
-
-structure NameMangler = NameManglerFun (
- type ctxt = (string * string -> string) * (string -> string option);
- type src = string * string;
- val ord = prod_ord string_ord string_ord;
- fun mk (postprocess, validate) ((shallow, name), 0) =
- let
- val name' = postprocess (shallow, name);
- in case validate name'
- of NONE => name'
- | _ => mk (postprocess, validate) ((shallow, name), 1)
- end
- | mk (postprocess, validate) (("", name), i) =
- postprocess ("", name ^ replicate_string i "'")
- |> perhaps validate
- | mk (postprocess, validate) ((shallow, name), 1) =
- postprocess (shallow, shallow ^ "_" ^ name)
- |> perhaps validate
- | mk (postprocess, validate) ((shallow, name), i) =
- postprocess (shallow, name ^ replicate_string i "'")
- |> perhaps validate;
- fun is_valid _ _ = true;
- fun maybe_unique _ _ = NONE;
- fun re_mangle _ dst = error ("No such definition name: " ^ quote dst);
-);
-
-fun mk_deresolver module nsp_conn postprocess validate =
- let
- datatype tabnode = N of string * tabnode Symtab.table option;
- fun mk module manglers tab =
- let
- fun mk_name name =
- case NameSpace.unpack name
- of [n] => ("", n)
- | [s, n] => (s, n);
- fun in_conn (shallow, conn) =
- member (op = : string * string -> bool) conn shallow;
- fun add_name name =
- let
- val n as (shallow, _) = mk_name name;
- in
- AList.map_entry_yield in_conn shallow (
- NameMangler.declare (postprocess, validate) n
- #-> (fn n' => pair (name, n'))
- ) #> apfst the
- end;
- val (renamings, manglers') =
- fold_map add_name (Graph.keys module) manglers;
- fun extend_tab (n, n') =
- if (length o NameSpace.unpack) n = 1
- then
- Symtab.update_new
- (n, N (n', SOME (mk ((dest_modl o Graph.get_node module) n) manglers' Symtab.empty)))
- else
- Symtab.update_new (n, N (n', NONE));
- in fold extend_tab renamings tab end;
- fun get_path_name [] tab =
- ([], SOME tab)
- | get_path_name [p] tab =
- let
- val SOME (N (p', tab')) = Symtab.lookup tab p
- in ([p'], tab') end
- | get_path_name [p1, p2] tab =
- (case Symtab.lookup tab p1
- of SOME (N (p', SOME tab')) =>
- let
- val (ps', tab'') = get_path_name [p2] tab'
- in (p' :: ps', tab'') end
- | NONE =>
- let
- val SOME (N (p', NONE)) = Symtab.lookup tab (NameSpace.pack [p1, p2])
- in ([p'], NONE) end)
- | get_path_name (p::ps) tab =
- let
- val SOME (N (p', SOME tab')) = Symtab.lookup tab p
- val (ps', tab'') = get_path_name ps tab'
- in (p' :: ps', tab'') end;
- fun deresolv tab prefix name =
- let
- val (common, (_, rem)) = chop_prefix (op =) (prefix, NameSpace.unpack name);
- val (_, SOME tab') = get_path_name common tab;
- val (name', _) = get_path_name rem tab';
- in NameSpace.pack name' end handle BIND => (error ("Missing name: " ^ quote name ^ ", in " ^ quote (NameSpace.pack prefix)));
- in deresolv (mk module (AList.make (K NameMangler.empty) nsp_conn) Symtab.empty) end;
+end; (*struct*)
-(* serialization *)
-
-fun serialize seri_defs seri_module validate postprocess nsp_conn name_root module =
- let
- val imptab = allimports_of module;
- val resolver = mk_deresolver module nsp_conn postprocess validate;
- fun sresolver s = (resolver o NameSpace.unpack) s
- fun mk_name prfx name =
- let
- val name_qual = NameSpace.pack (prfx @ [name])
- in (name_qual, resolver prfx name_qual) end;
- fun is_bot (_, (Def Bot)) = true
- | is_bot _ = false;
- fun mk_contents prfx module =
- map_filter (seri prfx)
- ((map (AList.make (Graph.get_node module)) o rev o Graph.strong_conn) module)
- and seri prfx [(name, Module modl)] =
- seri_module (resolver []) (map (resolver []) ((the o Symtab.lookup imptab) (NameSpace.pack (prfx @ [name]))))
- (mk_name prfx name, mk_contents (prfx @ [name]) modl)
- | seri prfx ds =
- case filter_out is_bot ds
- of [] => NONE
- | ds' => seri_defs sresolver (NameSpace.pack prfx)
- (map (fn (name, Def def) => (fst (mk_name prfx name), def (*|> tap (Pretty.writeln o pretty_def)*))) ds')
- in
- seri_module (resolver []) (map (resolver []) ((the o Symtab.lookup imptab) ""))
- (("", name_root), (mk_contents [] module))
- end;
-
-end; (* struct *)
-
structure BasicCodegenThingol: BASIC_CODEGEN_THINGOL = CodegenThingol;