# HG changeset patch # User haftmann # Date 1160199716 -7200 # Node ID 1484c7af6d6837b7ec3c021f27df2ab03c545bdf # Parent ac772d489fde07950cd33d84d24eeaeb319f3d50 cleaned up interfaces diff -r ac772d489fde -r 1484c7af6d68 src/Pure/Tools/codegen_funcgr.ML --- a/src/Pure/Tools/codegen_funcgr.ML Sat Oct 07 02:47:33 2006 +0200 +++ b/src/Pure/Tools/codegen_funcgr.ML Sat Oct 07 07:41:56 2006 +0200 @@ -50,8 +50,9 @@ let val lhs = (fst o Logic.dest_equals o Drule.plain_prop_of) thm; val tys = (fst o strip_type o fastype_of) lhs; + val ctxt = Name.make_context (map (fst o fst) (Term.add_vars lhs [])); val vs_ct = map (fn (v, ty) => cterm_of thy (Var ((v, 0), ty))) - (Name.names Name.context "a" tys); + (Name.names ctxt "a" tys); in fold (fn ct => fn thm => Thm.combination thm (Thm.reflexive ct)) vs_ct thm end; diff -r ac772d489fde -r 1484c7af6d68 src/Pure/Tools/codegen_package.ML --- 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)) ); diff -r ac772d489fde -r 1484c7af6d68 src/Pure/Tools/codegen_serializer.ML --- 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 "" + | 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 = diff -r ac772d489fde -r 1484c7af6d68 src/Pure/Tools/codegen_thingol.ML --- 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 "" - | 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;