# HG changeset patch # User haftmann # Date 1138720477 -3600 # Node ID 31aed965135c36a51645ea1b832df94c3d901d36 # Parent a87c0aeae92fd1478eb2f7f049dea9463146508f minor cleanups diff -r a87c0aeae92f -r 31aed965135c src/Pure/Tools/codegen_package.ML --- a/src/Pure/Tools/codegen_package.ML Tue Jan 31 16:12:56 2006 +0100 +++ b/src/Pure/Tools/codegen_package.ML Tue Jan 31 16:14:37 2006 +0100 @@ -19,7 +19,6 @@ val add_appconst: string * ((int * int) * appgen) -> theory -> theory; val add_appconst_i: xstring * ((int * int) * appgen) -> theory -> theory; val add_eqextr: string * eqextr -> theory -> theory; - val add_defgen: string * defgen -> theory -> theory; val add_prim_class: xstring -> string list -> (string * string) -> theory -> theory; val add_prim_tyco: xstring -> string list -> (string * string) @@ -34,6 +33,7 @@ val set_is_datatype: (theory -> string -> bool) -> theory -> theory; val set_get_all_datatype_cons : (theory -> (string * string) list) -> theory -> theory; + val set_defgen_datatype: defgen -> theory -> theory; val set_int_tyco: string -> theory -> theory; val exprgen_type: theory -> auxtab @@ -52,7 +52,7 @@ -> theory -> theory; val add_case_const_i: (theory -> string -> (string * int) list option) -> string -> theory -> theory; - val defgen_datatype: (theory -> string -> ((string * sort) list * string list) option) + val defgen_datatype_proto: (theory -> string -> ((string * sort) list * string list) option) -> (theory -> string * string -> typ list option) -> defgen; @@ -87,8 +87,8 @@ (* auxiliary *) -fun devarify_type ty = (fst o Type.freeze_thaw_type) ty; -fun devarify_term t = (fst o Type.freeze_thaw) t; +fun devarify_type ty = (fst o Type.freeze_thaw_type o Term.zero_var_indexesT) ty; +fun devarify_term t = (fst o Type.freeze_thaw o Term.zero_var_indexes) t; val is_number = is_some o Int.fromString; @@ -175,19 +175,21 @@ ); type auxtab = ((typ * thm) list Symtab.table * string Symtab.table) - * (InstNameMangler.T * ((typ * typ list) Symtab.table * ConstNameMangler.T) * DatatypeconsNameMangler.T); + * (InstNameMangler.T * ((typ * typ list) Symtab.table * ConstNameMangler.T) + * DatatypeconsNameMangler.T); type eqextr = theory -> auxtab -> (string * typ) -> (thm list * typ) option; type defgen = theory -> auxtab -> gen_defgen; -type appgen = theory -> auxtab -> (string * typ) * term list -> transact -> iexpr * transact; +type appgen = theory -> auxtab + -> (string * typ) * term list -> transact -> iexpr * transact; val serializers = ref ( Symtab.empty |> Symtab.update ( #ml CodegenSerializer.serializers |> apsnd (fn seri => seri - (nsp_dtcon, nsp_class, "") - [[nsp_class, nsp_tyco], [nsp_const, nsp_overl, nsp_dtcon, nsp_mem, nsp_inst]] + (nsp_dtcon, nsp_class, K false) + [[nsp_class, nsp_tyco], [nsp_const, nsp_overl, nsp_dtcon, nsp_class, nsp_mem, nsp_inst]] ) ) |> Symtab.update ( @@ -204,68 +206,75 @@ type gens = { appconst: ((int * int) * (appgen * stamp)) Symtab.table, - eqextrs: (string * (eqextr * stamp)) list, - defgens: (string * (defgen * stamp)) list + eqextrs: (string * (eqextr * stamp)) list }; -fun map_gens f { appconst, eqextrs, defgens } = +fun map_gens f { appconst, eqextrs } = let - val (appconst, eqextrs, defgens) = - f (appconst, eqextrs, defgens) - in { appconst = appconst, eqextrs = eqextrs, defgens = defgens } : gens end; + val (appconst, eqextrs) = + f (appconst, eqextrs) + in { appconst = appconst, eqextrs = eqextrs } : gens end; fun merge_gens - ({ appconst = appconst1 , eqextrs = eqextrs1, defgens = defgens1 }, - { appconst = appconst2 , eqextrs = eqextrs2, defgens = defgens2 }) = + ({ appconst = appconst1 , eqextrs = eqextrs1 }, + { appconst = appconst2 , eqextrs = eqextrs2 }) = { appconst = Symtab.merge - (fn ((bounds1, (_, stamp1)), (bounds2, (_, stamp2))) => bounds1 = bounds2 andalso stamp1 = stamp2) + (fn ((bounds1, (_, stamp1)), (bounds2, (_, stamp2))) => bounds1 = bounds2 + andalso stamp1 = stamp2) (appconst1, appconst2), - eqextrs = AList.merge (op =) (eq_snd (op =)) (eqextrs1, eqextrs2), - defgens = AList.merge (op =) (eq_snd (op =)) (defgens1, defgens2) + eqextrs = AList.merge (op =) (eq_snd (op =)) (eqextrs1, eqextrs2) } : gens; type logic_data = { is_datatype: ((theory -> string -> bool) * stamp) option, get_all_datatype_cons: ((theory -> (string * string) list) * stamp) option, + defgen_datatype: (defgen * stamp) option, alias: string Symtab.table * string Symtab.table }; -fun map_logic_data f { is_datatype, get_all_datatype_cons, alias } = +fun map_logic_data f { is_datatype, get_all_datatype_cons, defgen_datatype, alias } = let - val ((is_datatype, get_all_datatype_cons), alias) = - f ((is_datatype, get_all_datatype_cons), alias) + val ((is_datatype, get_all_datatype_cons, defgen_datatype), alias) = + f ((is_datatype, get_all_datatype_cons, defgen_datatype), alias) in { is_datatype = is_datatype, get_all_datatype_cons = get_all_datatype_cons, - alias = alias } : logic_data end; + defgen_datatype = defgen_datatype, alias = alias } : logic_data end; fun merge_logic_data ({ is_datatype = is_datatype1, get_all_datatype_cons = get_all_datatype_cons1, - alias = alias1 }, + defgen_datatype = defgen_datatype1, alias = alias1 }, { is_datatype = is_datatype2, get_all_datatype_cons = get_all_datatype_cons2, - alias = alias2 }) = + defgen_datatype = defgen_datatype2, alias = alias2 }) = let in { is_datatype = merge_opt (eq_snd (op =)) (is_datatype1, is_datatype2), - get_all_datatype_cons = merge_opt (eq_snd (op =)) (get_all_datatype_cons1, get_all_datatype_cons2), + get_all_datatype_cons = merge_opt (eq_snd (op =)) + (get_all_datatype_cons1, get_all_datatype_cons2), + defgen_datatype = merge_opt (eq_snd (op =)) (defgen_datatype1, defgen_datatype2), alias = (Symtab.merge (op =) (fst alias1, fst alias2), Symtab.merge (op =) (snd alias1, snd alias2)) } : logic_data end; type target_data = { + syntax_class: string Symtab.table, syntax_tyco: (itype CodegenSerializer.pretty_syntax * stamp) Symtab.table, syntax_const: (iexpr CodegenSerializer.pretty_syntax * stamp) Symtab.table }; -fun map_target_data f { syntax_tyco, syntax_const } = +fun map_target_data f { syntax_class, syntax_tyco, syntax_const } = let - val (syntax_tyco, syntax_const) = - f (syntax_tyco, syntax_const) - in { syntax_tyco = syntax_tyco, syntax_const = syntax_const } : target_data + val (syntax_class, syntax_tyco, syntax_const) = + f (syntax_class, syntax_tyco, syntax_const) + in { + syntax_class = syntax_class, + syntax_tyco = syntax_tyco, + syntax_const = syntax_const } : target_data end; fun merge_target_data - ({ syntax_tyco = syntax_tyco1, syntax_const = syntax_const1 }, - { syntax_tyco = syntax_tyco2, syntax_const = syntax_const2 }) = - { syntax_tyco = Symtab.merge (eq_snd (op =)) (syntax_tyco1, syntax_tyco2), + ({ syntax_class = syntax_class1, syntax_tyco = syntax_tyco1, syntax_const = syntax_const1 }, + { syntax_class = syntax_class2, syntax_tyco = syntax_tyco2, syntax_const = syntax_const2 }) = + { syntax_class = Symtab.merge (op =) (syntax_class1, syntax_class2), + 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 CodegenData = TheoryDataFun @@ -279,13 +288,15 @@ }; val empty = { modl = empty_module, - gens = { appconst = Symtab.empty, eqextrs = [], defgens = [] } : gens, + gens = { appconst = Symtab.empty, eqextrs = [] } : gens, logic_data = { is_datatype = NONE, get_all_datatype_cons = NONE, + defgen_datatype = NONE, alias = (Symtab.empty, Symtab.empty) } : logic_data, target_data = Symtab.empty |> Symtab.fold (fn (target, _) => - Symtab.update (target, { syntax_tyco = Symtab.empty, syntax_const = Symtab.empty }) + Symtab.update (target, + { syntax_class = Symtab.empty, syntax_tyco = Symtab.empty, syntax_const = Symtab.empty }) ) (! serializers) } : T; val copy = I; @@ -322,58 +333,8 @@ (writeln o Pretty.output o Pretty.chunks) [pretty_module module, pretty_deps module] end; -fun gen_add_appconst prep_const (raw_c, (bounds, ag)) thy = - let - val c = prep_const thy raw_c; - in map_codegen_data - (fn (modl, gens, target_data, logic_data) => - (modl, - gens |> map_gens - (fn (appconst, eqextrs, defgens) => - (appconst - |> Symtab.update (c, (bounds, (ag, stamp ()))), - eqextrs, defgens)), target_data, logic_data)) thy - end; -val add_appconst = gen_add_appconst Sign.intern_const; -val add_appconst_i = gen_add_appconst (K I); - -fun add_defgen (name, dg) = - map_codegen_data - (fn (modl, gens, target_data, logic_data) => - (modl, - gens |> map_gens - (fn (appconst, eqextrs, defgens) => - (appconst, eqextrs, defgens - |> Output.update_warn (op =) ("overwriting existing definition definition generator " ^ name) (name, (dg, stamp ())))), - target_data, logic_data)); - -fun get_defgens thy tabs = - (map (apsnd (fn (dg, _) => dg thy tabs)) o #defgens o #gens o CodegenData.get) thy; - -fun add_eqextr (name, eqx) = - map_codegen_data - (fn (modl, gens, target_data, logic_data) => - (modl, - gens |> map_gens - (fn (appconst, eqextrs, defgens) => - (appconst, eqextrs - |> Output.update_warn (op =) ("overwriting existing equation extractor " ^ name) (name, (eqx, stamp ())), - defgens)), - target_data, logic_data)); - -fun get_eqextrs thy tabs = - (map (fn (_, (eqx, _)) => eqx thy tabs) o #eqextrs o #gens o CodegenData.get) thy; - -fun is_datatype thy = - case (#is_datatype o #logic_data o CodegenData.get) thy - of NONE => K false - | SOME (f, _) => f thy; - -fun get_all_datatype_cons thy = - case (#get_all_datatype_cons o #logic_data o CodegenData.get) thy - of NONE => [] - | SOME (f, _) => f thy; +(* name handling *) fun add_alias (src, dst) = map_codegen_data @@ -384,9 +345,6 @@ (tab |> Symtab.update (src, dst), tab_rev |> Symtab.update (dst, src)))))); - -(* name handling *) - val alias_get = perhaps o Symtab.lookup o fst o #alias o #logic_data o CodegenData.get; val alias_rev = perhaps o Symtab.lookup o snd o #alias o #logic_data o CodegenData.get; @@ -419,69 +377,8 @@ |> dest_nsp shallow |> Option.map (alias_rev thy); -fun set_is_datatype f = - map_codegen_data - (fn (modl, gens, target_data, logic_data) => - (modl, gens, target_data, - logic_data - |> map_logic_data (apfst (fn (is_datatype, get_all_datatype_cons) - => (SOME (f, stamp ()), get_all_datatype_cons))))); - -fun set_get_all_datatype_cons f = - map_codegen_data - (fn (modl, gens, target_data, logic_data) => - (modl, gens, target_data, - logic_data - |> map_logic_data ((apfst (fn (is_datatype, get_all_datatype_cons) - => (is_datatype, SOME (f, stamp ()))))))); - -fun set_int_tyco tyco thy = - (serializers := ( - ! serializers - |> Symtab.update ( - #ml CodegenSerializer.serializers - |> apsnd (fn seri => seri - (nsp_dtcon, nsp_class, idf_of_name thy nsp_tyco tyco) - [[nsp_class, nsp_tyco], [nsp_const, nsp_overl, nsp_dtcon, nsp_mem, nsp_inst]] - ) - ) - ); thy); - - -(* code generator instantiation *) - -fun ensure_def_class thy tabs cls trns = - let - val cls' = idf_of_name thy nsp_class cls; - in - trns - |> debug 4 (fn _ => "generating class " ^ quote cls) - |> gen_ensure_def (get_defgens thy tabs) ("generating class " ^ quote cls) cls' - |> pair cls' - end; - -fun ensure_def_inst thy (tabs as (_, (insttab, _, _))) (cls, tyco) trns = - let - val thyname = (the o AList.lookup (op =) (ClassPackage.the_instances thy cls)) tyco; - val inst = idf_of_name thy nsp_inst (InstNameMangler.get thy insttab (thyname, (cls, tyco))); - in - trns - |> debug 4 (fn _ => "generating instance " ^ quote cls ^ " / " ^ quote tyco) - |> gen_ensure_def (get_defgens thy tabs) ("generating instance " ^ quote cls ^ " / " ^ quote tyco) inst - |> pair inst - end; - -fun ensure_def_tyco thy tabs tyco trns = - let - val tyco' = idf_of_name thy nsp_tyco tyco; - in - trns - |> debug 4 (fn _ => "generating type constructor " ^ quote tyco) - |> gen_ensure_def (get_defgens thy tabs) ("generating type constructor " ^ quote tyco) tyco' - |> pair tyco' - end; - -fun idf_of_const thy (tabs as ((_, clsmemtab), (_, (overltab1, overltab2), dtcontab))) (c, ty) = +fun idf_of_const thy (tabs as ((_, clsmemtab), (_, (overltab1, overltab2), dtcontab))) + (c, ty) = let fun get_overloaded (c, ty) = case Symtab.lookup overltab1 c @@ -519,43 +416,139 @@ | NONE => NONE ); -fun ensure_def_const thy (tabs as ((_, clsmemtab), (_, overltab, dtcontab))) (c, ty) trns = + +(* further theory data accessors *) + +fun gen_add_appconst prep_const (raw_c, (bounds, ag)) thy = let - val c' = idf_of_const thy tabs (c, ty); - in - trns - |> debug 4 (fn _ => "generating constant " ^ quote c) - |> gen_ensure_def (get_defgens thy tabs) ("generating constant " ^ quote c) c' - |> pair c' + val c = prep_const thy raw_c; + in map_codegen_data + (fn (modl, gens, target_data, logic_data) => + (modl, + gens |> map_gens + (fn (appconst, eqextrs) => + (appconst + |> Symtab.update (c, (bounds, (ag, stamp ()))), + eqextrs)), target_data, logic_data)) thy end; -(* fun ensure_def_eq thy tabs (dtco, (eqpred, arity)) trns = +val add_appconst = gen_add_appconst Sign.intern_const; +val add_appconst_i = gen_add_appconst (K I); + +fun add_eqextr (name, eqx) = + map_codegen_data + (fn (modl, gens, target_data, logic_data) => + (modl, + gens |> map_gens + (fn (appconst, eqextrs) => + (appconst, eqextrs + |> Output.update_warn (op =) ("overwriting existing equation extractor " ^ name) + (name, (eqx, stamp ())))), + target_data, logic_data)); + +fun get_eqextrs thy tabs = + (map (fn (_, (eqx, _)) => eqx thy tabs) o #eqextrs o #gens o CodegenData.get) thy; + +fun set_is_datatype f = + map_codegen_data + (fn (modl, gens, target_data, logic_data) => + (modl, gens, target_data, + logic_data + |> map_logic_data (apfst (fn (is_datatype, get_all_datatype_cons, defgen_datatype) + => (SOME (f, stamp ()), get_all_datatype_cons, defgen_datatype))))); + +fun is_datatype thy = + case (#is_datatype o #logic_data o CodegenData.get) thy + of NONE => K false + | SOME (f, _) => f thy; + +fun set_get_all_datatype_cons f = + map_codegen_data + (fn (modl, gens, target_data, logic_data) => + (modl, gens, target_data, + logic_data + |> map_logic_data ((apfst (fn (is_datatype, get_all_datatype_cons, defgen_datatype) + => (is_datatype, SOME (f, stamp ()), defgen_datatype)))))); + +fun get_all_datatype_cons thy = + case (#get_all_datatype_cons o #logic_data o CodegenData.get) thy + of NONE => [] + | SOME (f, _) => f thy; + +fun set_defgen_datatype f = + map_codegen_data + (fn (modl, gens, target_data, logic_data) => + (modl, gens, target_data, + logic_data + |> map_logic_data ((apfst (fn (is_datatype, get_all_datatype_cons, defgen_datatype) + => (is_datatype, get_all_datatype_cons, SOME (f, stamp ()))))))); + +fun defgen_datatype thy tabs dtco trns = + case (#defgen_datatype o #logic_data o CodegenData.get) thy + of NONE => + trns + |> fail ("no datatype definition generator present") + | SOME (f, _) => + trns + |> f thy tabs dtco; + +fun set_int_tyco tyco thy = + (serializers := ( + ! serializers + |> Symtab.update ( + #ml CodegenSerializer.serializers + |> apsnd (fn seri => seri + (nsp_dtcon, nsp_class, fn tyco' => tyco' = idf_of_name thy nsp_tyco tyco ) + [[nsp_class, nsp_tyco], [nsp_const, nsp_overl, nsp_dtcon, nsp_mem, nsp_inst]] + ) + ) + ); thy); + + +(* definition and expression generators *) + +fun ensure_def_class thy tabs cls trns = let - val name_dtco = (the ooo name_of_idf) thy nsp_tyco dtco; - val idf_eqinst = idf_of_name thy nsp_eq_inst name_dtco; - val idf_eqpred = idf_of_name thy nsp_eq_pred name_dtco; - val inst_sortlookup = map (fn (v, _) => [ClassPackage.Lookup ([], (v, 0))]) arity; - fun mk_eq_pred _ trns = - trns - |> succeed (eqpred) - fun mk_eq_inst _ trns = - trns - |> gen_ensure_def [("eqpred", mk_eq_pred)] ("generating equality predicate for " ^ quote dtco) idf_eqpred - |> succeed (Classinst ((class_eq, (dtco, arity)), ([], [(fun_eq, (idf_eqpred, inst_sortlookup))]))); + fun defgen_class thy (tabs as (_, (insttab, _, _))) cls trns = + case name_of_idf thy nsp_class cls + of SOME cls => + let + val cs = (snd o ClassPackage.the_consts_sign thy) cls; + val sortctxts = map (ClassPackage.extract_sortctxt thy o snd) cs; + val idfs = map (idf_of_name thy nsp_mem o fst) cs; + in + trns + |> debug 5 (fn _ => "trying defgen class declaration for " ^ quote cls) + |> fold_map (ensure_def_class thy tabs) (ClassPackage.the_superclasses thy cls) + ||>> fold_map (exprgen_type thy tabs o devarify_type o snd) cs + ||>> (fold_map o fold_map) (exprgen_tyvar_sort thy tabs) sortctxts + |-> (fn ((supcls, memtypes), sortctxts) => succeed + (Class ((supcls, ("a", idfs ~~ (sortctxts ~~ memtypes))), []))) + end + | _ => + trns + |> fail ("no class definition found for " ^ quote cls); + val cls' = idf_of_name thy nsp_class cls; in trns - |> gen_ensure_def [("eqinst", mk_eq_inst)] ("generating equality instance for " ^ quote dtco) idf_eqinst - end; *) - - -(* expression generators *) - -fun exprgen_tyvar_sort thy tabs (v, sort) trns = + |> debug 4 (fn _ => "generating class " ^ quote cls) + |> gen_ensure_def [("class", defgen_class thy tabs)] ("generating class " ^ quote cls) cls' + |> pair cls' + end +and ensure_def_tyco thy tabs tyco trns = + let + val tyco' = idf_of_name thy nsp_tyco tyco; + in + trns + |> debug 4 (fn _ => "generating type constructor " ^ quote tyco) + |> gen_ensure_def [("datatype", defgen_datatype thy tabs)] ("generating type constructor " ^ quote tyco) tyco' + |> pair tyco' + end +and exprgen_tyvar_sort thy tabs (v, sort) trns = trns |> fold_map (ensure_def_class thy tabs) (ClassPackage.syntactic_sort_of thy sort) - |-> (fn sort => pair (unprefix "'" v, sort)); - -fun exprgen_type thy tabs (TVar _) trns = + |-> (fn sort => pair (unprefix "'" v, sort)) +and exprgen_type thy tabs (TVar _) trns = error "TVar encountered during code generation" | exprgen_type thy tabs (TFree v_s) trns = trns @@ -581,60 +574,145 @@ | mk_lookup thy tabs (ClassPackage.Lookup (clss, (v, i))) trns = trns |> fold_map (ensure_def_class thy tabs) clss - |-> (fn clss => pair (ClassPackage.Lookup (clss, (v |> unprefix "'", i)))); - -fun appgen_default thy tabs ((c, ty), ts) trns = - trns - |> ensure_def_const thy tabs (c, ty) - ||>> (fold_map o fold_map) (mk_lookup thy tabs) - (ClassPackage.extract_sortlookup thy (c, ty)) - ||>> exprgen_type thy tabs ty - ||>> fold_map (exprgen_term thy tabs) ts - |-> (fn (((c, ls), ty), es) => - pair (Library.foldl IInst ((IConst (c, ty)), ls) `$$ es)) -and appgen thy tabs ((f, ty), ts) trns = - case Symtab.lookup ((#appconst o #gens o CodegenData.get) thy) f - of SOME ((imin, imax), (ag, _)) => - if length ts < imin then - let - val d = imin - length ts; - val vs = Term.invent_names (add_term_names (Const (f, ty), [])) "x" d; - val tys = Library.take (d, ((fst o strip_type) ty)); - in + |-> (fn clss => pair (ClassPackage.Lookup (clss, (v |> unprefix "'", i)))) +and mk_fun thy tabs (c, ty) trns = + case get_first (fn eqx => eqx (c, ty)) (get_eqextrs thy tabs) + of SOME (eq_thms, ty) => + let + val sortctxt = ClassPackage.extract_sortctxt thy ty; + fun dest_eqthm eq_thm = + let + val ((t, args), rhs) = + (apfst strip_comb o Logic.dest_equals o prop_of o Drule.zero_var_indexes) eq_thm; + in case t + of Const (c', _) => if c' = c then (args, rhs) + else error ("illegal function equation for " ^ quote c + ^ ", actually defining " ^ quote c') + | _ => error ("illegal function equation for " ^ quote c) + end; + fun mk_eq (args, rhs) trns = trns - |> debug 10 (fn _ => "eta-expanding") - |> fold_map (exprgen_type thy tabs) tys - ||>> ag thy tabs ((f, ty), ts @ map2 (curry Free) vs tys) - |-> (fn (tys, e) => pair ((vs ~~ tys) `|--> e)) - end - else if length ts > imax then + |> fold_map (exprgen_term thy tabs o devarify_term) args + ||>> (exprgen_term thy tabs o devarify_term) rhs + |-> (fn (args, rhs) => pair (args, rhs)) + in trns - |> debug 10 (fn _ => "splitting arguments (" ^ string_of_int imax ^ ", " ^ string_of_int (length ts) ^ ")") - |> ag thy tabs ((f, ty), Library.take (imax, ts)) - ||>> fold_map (exprgen_term thy tabs) (Library.drop (imax, ts)) - |-> (fn es => pair (mk_apps es)) - else - trns - |> debug 10 (fn _ => "keeping arguments") - |> ag thy tabs ((f, ty), ts) - | NONE => - trns - |> appgen_default thy tabs ((f, ty), ts) + |> debug 6 (fn _ => "(1) retrieved function equations for " ^ + quote (c ^ "::" ^ Sign.string_of_typ thy ty)) + |> fold_map (mk_eq o dest_eqthm) eq_thms + |> debug 6 (fn _ => "(2) building equations") + ||>> (exprgen_type thy tabs o devarify_type) ty + |> debug 6 (fn _ => "(3) building type") + ||>> fold_map (exprgen_tyvar_sort thy tabs) sortctxt + |> debug 6 (fn _ => "(4) building sort context") + |-> (fn ((eqs, ty), sortctxt) => (pair o SOME) (eqs, (sortctxt, ty))) + end + | NONE => (NONE, trns) +and ensure_def_inst thy (tabs as (_, (insttab, _, _))) (cls, tyco) trns = + let + fun defgen_inst thy (tabs as (_, (insttab, _, _))) inst trns = + case Option.map (InstNameMangler.rev thy insttab) (name_of_idf thy nsp_inst inst) + of SOME (_, (cls, tyco)) => + let + val (arity, memdefs) = ClassPackage.the_inst_sign thy (cls, tyco); + fun gen_suparity supclass trns = + trns + |> ensure_def_inst thy tabs (supclass, tyco) + ||>> (fold_map o fold_map) (mk_lookup thy tabs) + (ClassPackage.extract_sortlookup_inst thy (cls, tyco) supclass) + |-> (fn (inst, ls) => pair (supclass, (inst, ls))); + fun gen_membr (m, ty) trns = + trns + |> mk_fun thy tabs (m, ty) + |-> (fn SOME funn => pair (idf_of_name thy nsp_mem m, funn) + | NONE => error ("could not derive definition for member " ^ quote m)); + in + trns + |> debug 5 (fn _ => "trying defgen class instance for (" ^ quote cls + ^ ", " ^ quote tyco ^ ")") + |> ensure_def_class thy tabs cls + |> debug 5 (fn _ => "(1) got class") + ||>> ensure_def_tyco thy tabs tyco + |> debug 5 (fn _ => "(2) got type") + ||>> fold_map (exprgen_tyvar_sort thy tabs) arity + |> debug 5 (fn _ => "(3) got arity") + ||>> fold_map gen_suparity (ClassPackage.the_superclasses thy cls) + |> debug 5 (fn _ => "(4) got superarities") + ||>> fold_map gen_membr memdefs + |> debug 5 (fn _ => "(5) got members") + |-> (fn ((((cls, tyco), arity), suparities), memdefs) => + succeed (Classinst (((cls, (tyco, arity)), suparities), memdefs))) + end + | _ => + trns |> fail ("no class instance found for " ^ quote inst); + val thyname = (the o AList.lookup (op =) (ClassPackage.the_instances thy cls)) tyco; + val inst = idf_of_name thy nsp_inst (InstNameMangler.get thy insttab (thyname, (cls, tyco))); + in + trns + |> debug 4 (fn _ => "generating instance " ^ quote cls ^ " / " ^ quote tyco) + |> gen_ensure_def [("instance", defgen_inst thy tabs)] + ("generating instance " ^ quote cls ^ " / " ^ quote tyco) inst + |> pair inst + end +and ensure_def_const thy (tabs as ((_, clsmemtab), (_, overltab, dtcontab))) (c, ty) trns = + let + fun defgen_funs thy tabs c trns = + case recconst_of_idf thy tabs c + of SOME (c, ty) => + trns + |> mk_fun thy tabs (c, ty) + |-> (fn (SOME funn) => succeed (Fun funn) + | NONE => fail ("no defining equations found for " ^ quote c)) + | NONE => + trns + |> fail ("not a constant: " ^ quote c); + fun defgen_datatypecons thy (tabs as (_, (_, _, dtcontab))) co trns = + case Option.map (DatatypeconsNameMangler.rev thy dtcontab) (name_of_idf thy nsp_dtcon co) + of SOME (co, dtco) => + trns + |> debug 5 (fn _ => "trying defgen datatype constructor for " ^ quote co) + |> ensure_def_tyco thy tabs dtco + |-> (fn dtco => succeed Undef) + | _ => + trns + |> fail ("not a datatype constructor: " ^ quote co); + fun defgen_clsmem thy tabs m trns = + case name_of_idf thy nsp_mem m + of SOME m => + trns + |> debug 5 (fn _ => "trying defgen class member for " ^ quote m) + |> ensure_def_class thy tabs ((the o ClassPackage.lookup_const_class thy) m) + |-> (fn cls => succeed Undef) + | _ => + trns |> fail ("no class member found for " ^ quote m) + val c' = idf_of_const thy tabs (c, ty); + in + trns + |> debug 4 (fn _ => "generating constant " ^ quote c) + |> gen_ensure_def + [("funs", defgen_funs thy tabs), + ("clsmem", defgen_clsmem thy tabs), + ("datatypecons", defgen_datatypecons thy tabs)] + ("generating constant " ^ quote c) c' + |> pair c' + end and exprgen_term thy tabs (Const (f, ty)) trns = trns |> appgen thy tabs ((f, ty), []) |-> (fn e => pair e) - | exprgen_term thy tabs (Var ((v, i), ty)) trns = + | exprgen_term thy tabs (Var ((v, 0), ty)) trns = trns - |> exprgen_type thy tabs ty - |-> (fn ty => pair (IVarE (if i = 0 then v else v ^ "_" ^ string_of_int i, ty))) + |> (exprgen_type thy tabs o devarify_type) ty + |-> (fn ty => pair (IVarE (v, ty))) + | exprgen_term thy tabs (Var ((_, _), _)) trns = + error "Var with index greater 0 encountered during code generation" | exprgen_term thy tabs (Free (v, ty)) trns = trns - |> exprgen_type thy tabs ty + |> (exprgen_type thy tabs o devarify_type) ty |-> (fn ty => pair (IVarE (v, ty))) | exprgen_term thy tabs (Abs (v, ty, t)) trns = trns - |> exprgen_type thy tabs ty + |> (exprgen_type thy tabs o devarify_type) ty ||>> exprgen_term thy tabs (subst_bound (Free (v, ty), t)) |-> (fn (ty, e) => pair ((v, ty) `|-> e)) | exprgen_term thy tabs (t as t1 $ t2) trns = @@ -650,10 +728,65 @@ |> exprgen_term thy tabs t' ||>> fold_map (exprgen_term thy tabs) ts |-> (fn (e, es) => pair (e `$$ es)) - end; + end +and appgen_default thy tabs ((c, ty), ts) trns = + trns + |> ensure_def_const thy tabs (c, ty) + ||>> (fold_map o fold_map) (mk_lookup thy tabs) + (ClassPackage.extract_sortlookup thy (c, ty)) + ||>> (exprgen_type thy tabs o devarify_type) ty + ||>> fold_map (exprgen_term thy tabs o devarify_term) ts + |-> (fn (((c, ls), ty), es) => + pair (IConst ((c, ty), ls) `$$ es)) +and appgen thy tabs ((f, ty), ts) trns = + case Symtab.lookup ((#appconst o #gens o CodegenData.get) thy) f + of SOME ((imin, imax), (ag, _)) => + if length ts < imin then + let + val d = imin - length ts; + val vs = Term.invent_names (add_term_names (Const (f, ty), [])) "x" d; + val tys = Library.take (d, ((fst o strip_type) ty)); + in + trns + |> debug 10 (fn _ => "eta-expanding") + |> fold_map (exprgen_type thy tabs o devarify_type) tys + ||>> ag thy tabs ((f, ty), ts @ map2 (curry Free) vs tys) + |-> (fn (tys, e) => pair ((vs ~~ tys) `|--> e)) + end + else if length ts > imax then + trns + |> debug 10 (fn _ => "splitting arguments (" ^ string_of_int imax ^ ", " + ^ string_of_int (length ts) ^ ")") + |> ag thy tabs ((f, ty), Library.take (imax, ts)) + ||>> fold_map (exprgen_term thy tabs) (Library.drop (imax, ts)) + |-> (fn es => pair (mk_apps es)) + else + trns + |> debug 10 (fn _ => "keeping arguments") + |> ag thy tabs ((f, ty), ts) + | NONE => + trns + |> appgen_default thy tabs ((f, ty), ts); +(* fun ensure_def_eq thy tabs (dtco, (eqpred, arity)) trns = + let + val name_dtco = (the ooo name_of_idf) thy nsp_tyco dtco; + val idf_eqinst = idf_of_name thy nsp_eq_inst name_dtco; + val idf_eqpred = idf_of_name thy nsp_eq_pred name_dtco; + val inst_sortlookup = map (fn (v, _) => [ClassPackage.Lookup ([], (v, 0))]) arity; + fun mk_eq_pred _ trns = + trns + |> succeed (eqpred) + fun mk_eq_inst _ trns = + trns + |> gen_ensure_def [("eqpred", mk_eq_pred)] ("generating equality predicate for " ^ quote dtco) idf_eqpred + |> succeed (Classinst ((class_eq, (dtco, arity)), ([], [(fun_eq, (idf_eqpred, inst_sortlookup))]))); + in + trns + |> gen_ensure_def [("eqinst", mk_eq_inst)] ("generating equality instance for " ^ quote dtco) idf_eqinst + end; *) -(* application generators *) +(* expression generators *) (* fun appgen_eq thy tabs (("op =", Type ("fun", [ty, _])), [t1, t2]) trns = trns @@ -667,34 +800,6 @@ (* function extractors *) -fun mk_fun thy tabs (c, ty) trns = - case get_first (fn eqx => eqx (c, ty)) (get_eqextrs thy tabs) - of SOME (eq_thms, ty) => - let - val sortctxt = ClassPackage.extract_sortctxt thy ty; - fun dest_eqthm eq_thm = - let - val ((t, args), rhs) = (apfst strip_comb o Logic.dest_equals o prop_of) eq_thm; - in case t - of Const (c', _) => if c' = c then (args, rhs) - else error ("illegal function equation for " ^ quote c - ^ ", actually defining " ^ quote c') - | _ => error ("illegal function equation for " ^ quote c) - end; - fun mk_eq (args, rhs) trns = - trns - |> fold_map (exprgen_term thy tabs o devarify_term) args - ||>> (exprgen_term thy tabs o devarify_term) rhs - |-> (fn (args, rhs) => pair (map ipat_of_iexpr args, rhs)) - in - trns - |> fold_map (mk_eq o dest_eqthm) eq_thms - ||>> exprgen_type thy tabs (devarify_type ty) - ||>> fold_map (exprgen_tyvar_sort thy tabs) sortctxt - |-> (fn ((eqs, ty), sortctxt) => (pair o SOME) (eqs, (sortctxt, ty))) - end - | NONE => (NONE, trns); - fun eqextr_defs thy ((deftab, _), _) (c, ty) = let fun eq_typ (ty1, ty2) = @@ -708,84 +813,6 @@ end; -(* definition generators *) - -fun defgen_clsdecl thy (tabs as (_, (insttab, _, _))) cls trns = - case name_of_idf thy nsp_class cls - of SOME cls => - let - val cs = (snd o ClassPackage.the_consts_sign thy) cls; - val sortctxts = map (ClassPackage.extract_sortctxt thy o snd) cs; - val idfs = map (idf_of_name thy nsp_mem o fst) cs; - in - trns - |> debug 5 (fn _ => "trying defgen class declaration for " ^ quote cls) - |> fold_map (ensure_def_class thy tabs) (ClassPackage.the_superclasses thy cls) - ||>> fold_map (exprgen_type thy tabs o snd) cs - ||>> (fold_map o fold_map) (exprgen_tyvar_sort thy tabs) sortctxts - |-> (fn ((supcls, memtypes), sortctxts) => succeed - (Class ((supcls, ("a", idfs ~~ (sortctxts ~~ memtypes))), []))) - end - | _ => - trns - |> fail ("no class definition found for " ^ quote cls); - -fun defgen_funs thy tabs c trns = - case recconst_of_idf thy tabs c - of SOME (c, ty) => - trns - |> mk_fun thy tabs (c, ty) - |-> (fn (SOME funn) => succeed (Fun funn) - | NONE => fail ("no defining equations found for " ^ quote c)) - | NONE => - trns - |> fail ("not a constant: " ^ quote c); - -fun defgen_datatypecons thy (tabs as (_, (_, _, dtcontab))) co trns = - case Option.map (DatatypeconsNameMangler.rev thy dtcontab) (name_of_idf thy nsp_dtcon co) - of SOME (co, dtco) => - trns - |> debug 5 (fn _ => "trying defgen datatype constructor for " ^ quote co) - |> ensure_def_tyco thy tabs dtco - |-> (fn dtco => succeed Undef) - | _ => - trns - |> fail ("not a datatype constructor: " ^ quote co); - -fun defgen_clsmem thy tabs m trns = - case name_of_idf thy nsp_mem m - of SOME m => - trns - |> debug 5 (fn _ => "trying defgen class member for " ^ quote m) - |> ensure_def_class thy tabs ((the o ClassPackage.lookup_const_class thy) m) - |-> (fn cls => succeed Undef) - | _ => - trns |> fail ("no class member found for " ^ quote m) - -fun defgen_clsinst thy (tabs as (_, (insttab, _, _))) inst trns = - case Option.map (InstNameMangler.rev thy insttab) (name_of_idf thy nsp_inst inst) - of SOME (_, (cls, tyco)) => - let - val (arity, memdefs) = ClassPackage.the_inst_sign thy (cls, tyco); - fun gen_membr (m, ty) trns = - trns - |> mk_fun thy tabs (m, ty) - |-> (fn SOME funn => pair (m, funn) - | NONE => error ("could not derive definition for member " ^ quote m)); - in - trns - |> debug 5 (fn _ => "trying defgen class instance for (" ^ quote cls ^ ", " ^ quote tyco ^ ")") - |> ensure_def_class thy tabs cls - ||>> ensure_def_tyco thy tabs tyco - ||>> fold_map (exprgen_tyvar_sort thy tabs) arity - ||>> fold_map gen_membr memdefs - |-> (fn (((cls, tyco), arity), memdefs) => - succeed (Classinst ((cls, (tyco, arity)), memdefs))) - end - | _ => - trns |> fail ("no class instance found for " ^ quote inst); - - (* parametrized generators, for instantiation in HOL *) fun appgen_let strip_abs thy tabs ((c, ty), [t2, t3]) trns = @@ -801,7 +828,7 @@ trns |> exprgen_term thy tabs l ||>> exprgen_term thy tabs r - |-> (fn (l, r) => pair (r, ipat_of_iexpr l)); + |-> (fn (l, r) => pair (r, l)); val (lets, body) = dest_let (Const (c, ty) $ t2 $ t3) in trns @@ -825,8 +852,8 @@ Type (_, [_, ty as Type (tyco, [])])), [bin]) trns = if tyco = tyco_int then trns - |> exprgen_type thy tabs ty - |-> (fn ty => pair (CodegenThingol.IConst ((IntInf.toString o bin_to_int) bin, ty))) + |> (exprgen_type thy tabs o devarify_type) ty + |-> (fn ty => pair (CodegenThingol.IConst (((IntInf.toString o bin_to_int) bin, ty), []))) else if tyco = tyco_nat then trns |> exprgen_term thy tabs (mk_int_to_nat bin) @@ -849,7 +876,7 @@ trns |> exprgen_term thy tabs (list_comb (Const (cname, tys ---> dty), frees)) ||>> exprgen_term thy tabs t' - |-> (fn (ep, e) => pair (ipat_of_iexpr ep, e)) + |-> (fn (ep, e) => pair (ep, e)) end; in trns @@ -872,7 +899,7 @@ val add_case_const = gen_add_case_const Sign.intern_const; val add_case_const_i = gen_add_case_const (K I); -fun defgen_datatype get_datatype get_datacons thy (tabs as (_, (_, _, dtcontab))) dtco trns = +fun defgen_datatype_proto get_datatype get_datacons thy (tabs as (_, (_, _, dtcontab))) dtco trns = case name_of_idf thy nsp_tyco dtco of SOME dtco => (case get_datatype thy dtco @@ -935,13 +962,15 @@ |> Symtab.fold (fn (c, [_]) => I | (c, tytab) => - (fn (overltab1, overltab2) => ( - overltab1 - |> Symtab.update_new (c, (Sign.the_const_constraint thy c, map fst tytab)), - overltab2 - |> fold (fn (ty, _) => ConstNameMangler.declare thy - (idf_of_name thy nsp_overl c, (Sign.the_const_constraint thy c, ty)) #> snd) tytab - ))) deftab; + if (is_none o ClassPackage.lookup_const_class thy) c + then (fn (overltab1, overltab2) => ( + overltab1 + |> Symtab.update_new (c, (Sign.the_const_constraint thy c, map fst tytab)), + overltab2 + |> fold (fn (ty, _) => ConstNameMangler.declare thy + (idf_of_name thy nsp_overl c, (Sign.the_const_constraint thy c, ty)) #> snd) tytab)) + else I + ) deftab; fun mk_dtcontab thy = DatatypeconsNameMangler.empty |> fold_map @@ -1069,6 +1098,20 @@ (* syntax *) +fun gen_add_syntax_class prep_class class target pretty thy = + thy + |> map_codegen_data + (fn (modl, gens, target_data, logic_data) => + (modl, gens, + target_data |> Symtab.map_entry target + (map_target_data + (fn (syntax_class, syntax_tyco, syntax_const) => + (syntax_class + |> Symtab.update (prep_class thy class, pretty), syntax_tyco, syntax_const))), + logic_data)); + +val add_syntax_class = gen_add_syntax_class Sign.intern_class; + val parse_syntax_tyco = let fun mk reader raw_tyco target thy = @@ -1093,14 +1136,15 @@ (modl, gens, target_data |> Symtab.map_entry target (map_target_data - (fn (syntax_tyco, syntax_const) => - (syntax_tyco |> Symtab.update + (fn (syntax_class, syntax_tyco, syntax_const) => + (syntax_class, syntax_tyco |> Symtab.update (tyco, (pretty, stamp ())), syntax_const))), logic_data))) end; in - CodegenSerializer.parse_syntax (read_quote read_typ exprgen_type) + CodegenSerializer.parse_syntax + (read_quote read_typ (fn thy => fn tabs => exprgen_type thy tabs o devarify_type)) #-> (fn reader => pair (mk reader)) end; @@ -1110,8 +1154,8 @@ (modl, gens, target_data |> Symtab.map_entry target (map_target_data - (fn (syntax_tyco, syntax_const) => - (syntax_tyco, + (fn (syntax_class, syntax_tyco, syntax_const) => + (syntax_class, syntax_tyco, syntax_const |> Symtab.update (c, (pretty, stamp ()))))), @@ -1181,6 +1225,7 @@ |> #target_data |> (fn data => (the oo Symtab.lookup) data target); in (seri ( + (Symtab.lookup o #syntax_class) target_data, (Option.map fst oo Symtab.lookup o #syntax_tyco) target_data, (Option.map fst oo Symtab.lookup o #syntax_const) target_data ) cs module : unit; thy) end; @@ -1197,10 +1242,10 @@ val (generateK, serializeK, primclassK, primtycoK, primconstK, - syntax_tycoK, syntax_constK, aliasK) = + syntax_classK, syntax_tycoK, syntax_constK, aliasK) = ("code_generate", "code_serialize", "code_primclass", "code_primtyco", "code_primconst", - "code_syntax_tyco", "code_syntax_const", "code_alias"); + "code_syntax_class", "code_syntax_tyco", "code_syntax_const", "code_alias"); val dependingK = ("depending_on"); @@ -1260,6 +1305,18 @@ (Toplevel.theory oo fold) (add_prim_const raw_const depends) primdefs) ); +val syntax_classP = + OuterSyntax.command syntax_tycoK "define code syntax for class" K.thy_decl ( + Scan.repeat1 ( + P.xname + -- Scan.repeat1 ( + P.name -- P.string + ) + ) + >> (Toplevel.theory oo fold) (fn (raw_class, syns) => + fold (fn (target, p) => add_syntax_class raw_class target p) syns) + ); + val syntax_tycoP = OuterSyntax.command syntax_tycoK "define code syntax for type constructor" K.thy_decl ( Scan.repeat1 ( @@ -1294,11 +1351,6 @@ val _ = Context.add_setup ( add_eqextr ("defs", eqextr_defs) - #> add_defgen ("funs", defgen_funs) - #> add_defgen ("clsdecl", defgen_clsdecl) - #> add_defgen ("clsmem", defgen_clsmem) - #> add_defgen ("clsinst", defgen_clsinst) - #> add_defgen ("datatypecons", defgen_datatypecons) (* add_appconst_i ("op =", ((2, 2), appgen_eq)) *) ); diff -r a87c0aeae92f -r 31aed965135c src/Pure/Tools/codegen_serializer.ML --- a/src/Pure/Tools/codegen_serializer.ML Tue Jan 31 16:12:56 2006 +0100 +++ b/src/Pure/Tools/codegen_serializer.ML Tue Jan 31 16:14:37 2006 +0100 @@ -12,7 +12,8 @@ type serializer = string list list -> OuterParse.token list -> - ((string -> CodegenThingol.itype pretty_syntax option) + ((string -> string option) + * (string -> CodegenThingol.itype pretty_syntax option) * (string -> CodegenThingol.iexpr pretty_syntax option) -> string list option -> CodegenThingol.module -> unit) @@ -22,7 +23,7 @@ val parse_targetdef: (string -> string) -> string -> string; val pretty_list: string -> string -> int * string -> CodegenThingol.iexpr pretty_syntax; val serializers: { - ml: string * (string * string * string -> serializer), + ml: string * (string * string * (string -> bool) -> serializer), haskell: string * (string -> serializer) } end; @@ -57,7 +58,8 @@ | Pretty of Pretty.T | Quote of 'a; -type 'a pretty_syntax = (int * int) * (fixity -> (fixity -> 'a -> Pretty.T) -> 'a list -> Pretty.T); +type 'a pretty_syntax = (int * int) * (fixity -> (fixity -> 'a -> Pretty.T) + -> 'a list -> Pretty.T); fun eval_lrx L L = false | eval_lrx R R = false @@ -84,17 +86,26 @@ 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 (f, es) = +fun from_app mk_app from_expr const_syntax fxy (c, es) = let fun mk NONE es = - brackify fxy (mk_app f es) + brackify fxy (mk_app c es) | mk (SOME ((i, k), pr)) es = let - val (es1, es2) = splitAt (i, es); + val (es1, es2) = splitAt (k, es); in brackify fxy (pr fxy from_expr es1 :: map (from_expr BR) es2) end; - in mk (const_syntax f) es end; + in mk (const_syntax c) es end; + +val _ : (string -> iexpr list -> Pretty.T list) + -> (fixity -> iexpr -> Pretty.T) + -> (string + -> ((int * int) + * (fixity + -> (fixity -> iexpr -> Pretty.T) + -> iexpr list -> Pretty.T)) option) + -> fixity -> string * iexpr list -> Pretty.T = from_app; fun fillin_mixfix fxy_this ms fxy_ctxt pr args = let @@ -155,13 +166,18 @@ fun parse_nonatomic_mixfix reader s ctxt = case parse_mixfix reader s ctxt - of ([Pretty _], _) => error ("mixfix contains just one pretty element; either declare as " ^ quote atomK ^ " or consider adding a break") + of ([Pretty _], _) => + error ("mixfix contains just one pretty element; either declare as " + ^ quote atomK ^ " or consider adding a break") | x => x; fun parse_syntax_proto reader = OuterParse.$$$ "(" |-- ( - OuterParse.$$$ infixK |-- OuterParse.nat >> (fn i => (parse_infix (INFX (i, X)), INFX (i, X))) - || OuterParse.$$$ infixlK |-- OuterParse.nat >> (fn i => (parse_infix (INFX (i, L)), INFX (i, L))) - || OuterParse.$$$ infixrK |-- OuterParse.nat >> (fn i => (parse_infix (INFX (i, R)), INFX (i, R))) + OuterParse.$$$ infixK |-- OuterParse.nat + >> (fn i => (parse_infix (INFX (i, X)), INFX (i, X))) + || OuterParse.$$$ infixlK |-- OuterParse.nat + >> (fn i => (parse_infix (INFX (i, L)), INFX (i, L))) + || OuterParse.$$$ infixrK |-- OuterParse.nat + >> (fn i => (parse_infix (INFX (i, R)), INFX (i, R))) || OuterParse.$$$ atomK |-- pair (parse_mixfix reader, NOBR) || pair (parse_nonatomic_mixfix reader, BR) ) -- OuterParse.string --| OuterParse.$$$ ")" >> (fn ((p, fxy), s) => (p s, fxy)); @@ -210,7 +226,8 @@ type serializer = string list list -> OuterParse.token list -> - ((string -> CodegenThingol.itype pretty_syntax option) + ((string -> string option) + * (string -> CodegenThingol.itype pretty_syntax option) * (string -> CodegenThingol.iexpr pretty_syntax option) -> string list option -> CodegenThingol.module -> unit) @@ -226,7 +243,8 @@ end; fun abstract_serializer (target, nspgrp) name_root (from_defs, from_module, validator) - postprocess preprocess (tyco_syntax, const_syntax) select module = + postprocess preprocess (class_syntax : string -> string option, tyco_syntax, const_syntax) + select module = let fun from_prim (name, prim) = case AList.lookup (op = : string * string -> bool) prim target @@ -242,7 +260,7 @@ |> debug 3 (fn _ => "preprocessing...") |> preprocess |> debug 3 (fn _ => "serializing...") - |> serialize (from_defs (from_prim, (tyco_syntax, const_syntax))) + |> serialize (from_defs (from_prim, (class_syntax, tyco_syntax, const_syntax))) from_module' validator nspgrp name_root |> K () end; @@ -308,7 +326,7 @@ fun pretty_list thingol_nil thingol_cons (target_pred, target_cons) = let - fun dest_cons (IApp (IApp (IConst (c, _), e1), e2)) = + fun dest_cons (IApp (IApp (IConst ((c, _), _), e1), e2)) = if c = thingol_cons then SOME (e1, e2) else NONE @@ -321,7 +339,7 @@ ]; fun pretty_compact fxy pr [e1, e2] = case unfoldr dest_cons e2 - of (es, IConst (c, _)) => + of (es, IConst ((c, _), _)) => if c = thingol_nil then Pretty.enum "," "[" "]" (map (pr NOBR) (e1::es)) else pretty_default fxy pr e1 e2 @@ -335,21 +353,19 @@ local fun ml_from_defs (is_cons, needs_type) - (from_prim, (tyco_syntax, const_syntax)) resolv defs = + (from_prim, (_, tyco_syntax, const_syntax)) resolv defs = let 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 ml_from_label s = - let - val s' = NameSpace.unpack s; - in - NameSpace.pack (Library.drop (length s' - 2, s')) - |> translate_string (fn "_" => "__" | "." => "_" | c => c) end; + val ml_from_label = + resolv + #> NameSpace.base + #> translate_string (fn "_" => "__" | "." => "_" | c => c) + #> str; fun ml_from_type fxy (IType (tyco, tys)) = (case tyco_syntax tyco of NONE => @@ -363,7 +379,8 @@ | SOME ((i, k), pr) => if not (i <= length tys andalso length tys <= k) then error ("number of argument mismatch in customary serialization: " - ^ (string_of_int o length) tys ^ " given, " ^ string_of_int i ^ " to " ^ string_of_int k + ^ (string_of_int o length) tys ^ " given, " + ^ string_of_int i ^ " to " ^ string_of_int k ^ " expected") else pr fxy ml_from_type tys) | ml_from_type fxy (IFun (t1, t2)) = @@ -379,127 +396,96 @@ ml_from_type (INFX (1, R)) t2 ] end - | ml_from_type _ (IVarT (v, [])) = + | ml_from_type _ (IVarT (v, _)) = str ("'" ^ v) - | ml_from_type _ (IVarT (_, sort)) = - "cannot serialize sort constrained type variable to ML: " ^ commas sort |> error | ml_from_type _ (IDictT fs) = Pretty.enum "," "{" "}" ( map (fn (f, ty) => - Pretty.block [str (ml_from_label f ^ ": "), ml_from_type NOBR ty]) fs + Pretty.block [ml_from_label f, str ": ", ml_from_type NOBR ty]) fs ); - fun ml_from_pat fxy (ICons ((f, ps), ty)) = - (case const_syntax f - of NONE => if length ps <= 1 - then - ps - |> map (ml_from_pat BR) - |> cons ((str o resolv) f) - |> brackify fxy - else - ps - |> map (ml_from_pat BR) - |> Pretty.enum "," "(" ")" - |> single - |> cons ((str o resolv) f) - |> brackify fxy - | SOME ((i, k), pr) => - if not (i <= length ps andalso length ps <= k) - then error ("number of argument mismatch in customary serialization: " - ^ (string_of_int o length) ps ^ " given, " ^ string_of_int i ^ " to " ^ string_of_int k - ^ " expected") - else pr fxy ml_from_expr (map iexpr_of_ipat ps)) - | ml_from_pat fxy (IVarP (v, ty)) = - if needs_type ty - then - brackify fxy [ - str v, - str ":", - ml_from_type NOBR ty - ] - else - str v - and ml_from_expr fxy (e as IApp (e1, e2)) = - (case (unfold_app e) - of (e as (IConst (f, _)), es) => - ml_from_app fxy (f, es) - | _ => + fun ml_from_expr sortctxt fxy (e as IApp (e1, e2)) = + (case unfold_const_app e + of SOME x => ml_from_app sortctxt fxy x + | NONE => brackify fxy [ - ml_from_expr NOBR e1, - ml_from_expr BR e2 + ml_from_expr sortctxt NOBR e1, + ml_from_expr sortctxt BR e2 ]) - | ml_from_expr fxy (e as IConst (f, _)) = - ml_from_app fxy (f, []) - | ml_from_expr fxy (IVarE (v, _)) = + | ml_from_expr sortctxt fxy (e as IConst x) = + ml_from_app sortctxt fxy (x, []) + | ml_from_expr sortctxt fxy (IVarE (v, _)) = str v - | ml_from_expr fxy (IAbs ((v, _), e)) = + | ml_from_expr sortctxt fxy (IAbs ((v, _), e)) = brackify fxy [ str ("fn " ^ v ^ " =>"), - ml_from_expr NOBR e + ml_from_expr sortctxt NOBR e ] - | ml_from_expr fxy (e as ICase (_, [_])) = + | ml_from_expr sortctxt fxy (e as ICase (_, [_])) = let val (ps, e) = unfold_let e; fun mk_val (p, e) = Pretty.block [ str "val ", - ml_from_pat fxy p, + ml_from_expr sortctxt fxy p, str " =", Pretty.brk 1, - ml_from_expr NOBR e, + ml_from_expr sortctxt NOBR e, str ";" ] in Pretty.chunks [ [str ("let"), Pretty.fbrk, map mk_val ps |> Pretty.chunks] |> Pretty.block, - [str ("in"), Pretty.fbrk, ml_from_expr NOBR e] |> Pretty.block, + [str ("in"), Pretty.fbrk, ml_from_expr sortctxt NOBR e] |> Pretty.block, str ("end") ] end - | ml_from_expr fxy (ICase (e, c::cs)) = + | ml_from_expr sortctxt fxy (ICase (e, c::cs)) = let fun mk_clause definer (p, e) = Pretty.block [ str definer, - ml_from_pat NOBR p, + ml_from_expr sortctxt NOBR p, str " =>", Pretty.brk 1, - ml_from_expr NOBR e + ml_from_expr sortctxt NOBR e ] in brackify fxy ( str "case" - :: ml_from_expr NOBR e + :: ml_from_expr sortctxt NOBR e :: mk_clause "of " c :: map (mk_clause "| ") cs ) end - | ml_from_expr fxy (IInst _) = - error "cannot serialize poly instant to ML" - | ml_from_expr fxy (IDictE fs) = + | ml_from_expr sortctxt fxy (IDictE fs) = Pretty.enum "," "{" "}" ( map (fn (f, e) => - Pretty.block [str (ml_from_label f ^ " = "), ml_from_expr NOBR e]) fs + Pretty.block [ml_from_label f, str " = ", ml_from_expr sortctxt NOBR e]) fs ) - | ml_from_expr fxy (ILookup ([], v)) = + | ml_from_expr sortctxt fxy (ILookup ([], v)) = str v - | ml_from_expr fxy (ILookup ([l], v)) = + | ml_from_expr sortctxt fxy (ILookup ([l], v)) = brackify fxy [ - str ("#" ^ (ml_from_label l)), + str "#", + ml_from_label l, str v ] - | ml_from_expr fxy (ILookup (ls, v)) = + (*| ml_from_expr sortctxt fxy (ILookup (ls, v)) = brackify fxy [ str ("(" ^ (ls |> map ((fn s => "#" ^ s) o ml_from_label) |> foldr1 (fn (l, e) => l ^ " o " ^ e)) ^ ")"), str v - ] - | ml_from_expr _ e = + ]*) + | ml_from_expr _ _ e = error ("dubious expression: " ^ (Pretty.output o pretty_iexpr) e) - and ml_mk_app f es = + and ml_mk_app sortctxt f es = if is_cons f andalso length es > 1 then - [(str o resolv) f, Pretty.enum " *" "(" ")" (map (ml_from_expr BR) es)] + [(str o resolv) f, Pretty.enum " *" "(" ")" (map (ml_from_expr sortctxt BR) es)] else - (str o resolv) f :: map (ml_from_expr BR) es - and ml_from_app fxy = - from_app ml_mk_app ml_from_expr const_syntax fxy; + (str o resolv) f :: map (ml_from_expr sortctxt BR) es + and ml_from_app sortctxt fxy (((f, _), ls), es) = + let + val _ = (); + in + from_app (ml_mk_app sortctxt) (ml_from_expr sortctxt) const_syntax fxy (f, es) + end; fun ml_from_funs (ds as d::ds_tl) = let fun mk_definer [] = "val" @@ -513,23 +499,23 @@ | check_args _ _ = error ("function definition block containing other definitions than functions") val definer = the (fold check_args ds NONE); - fun mk_eq definer f ty (pats, expr) = + fun mk_eq definer sortctxt f ty (pats, expr) = let val lhs = [str (definer ^ " " ^ f)] @ (if null pats then [str ":", ml_from_type NOBR ty] - else map (ml_from_pat BR) pats) - val rhs = [str "=", ml_from_expr NOBR expr] + else map (ml_from_expr sortctxt BR) pats) + val rhs = [str "=", ml_from_expr sortctxt NOBR expr] in Pretty.block (separate (Pretty.brk 1) (lhs @ rhs)) end - fun mk_fun definer (f, Fun (eqs as eq::eq_tl, (_, ty))) = + fun mk_fun definer (f, Fun (eqs as eq::eq_tl, (sortctxt , ty))) = let val (pats_hd::pats_tl) = (fst o split_list) eqs; val shift = if null eq_tl then I else map (Pretty.block o single); in (Pretty.block o Pretty.fbreaks o shift) ( - mk_eq definer f ty eq - :: map (mk_eq "|" f ty) eq_tl + mk_eq definer sortctxt f ty eq + :: map (mk_eq "|" sortctxt f ty) eq_tl ) end; in @@ -543,7 +529,8 @@ val defs' = List.mapPartial (fn (name, Datatype info) => SOME (name, info) | (name, Datatypecons _) => NONE - | (name, def) => error ("datatype block containing illegal def: " ^ (Pretty.output o pretty_def) def) + | (name, def) => error ("datatype block containing illegal def: " + ^ (Pretty.output o pretty_def) def) ) defs fun mk_cons (co, []) = str (resolv co) @@ -552,7 +539,8 @@ str (resolv co) :: str " of" :: Pretty.brk 1 - :: separate (Pretty.block [str " *", Pretty.brk 1]) (map (ml_from_type NOBR) tys) + :: separate (Pretty.block [str " *", Pretty.brk 1]) + (map (ml_from_type NOBR) tys) ) fun mk_datatype definer (t, ((vs, cs), _)) = Pretty.block ( @@ -576,7 +564,8 @@ | ml_from_def (name, Prim prim) = from_prim (name, prim) | ml_from_def (name, Typesyn (vs, ty)) = - (map (fn (vname, []) => () | _ => error "can't serialize sort constrained type declaration to ML") vs; + (map (fn (vname, []) => () | _ => + error "can't serialize sort constrained type declaration to ML") vs; Pretty.block [ str "type ", ml_from_type NOBR (name `%% map IVarT vs), @@ -586,12 +575,82 @@ str ";" ] ) |> SOME - | ml_from_def (name, Class _) = - error ("can't serialize class declaration " ^ quote name ^ " to ML") + | ml_from_def (name, Class ((supclasses, (v, membrs)), _)) = + let + val pv = str ("'" ^ v); + fun from_supclass class = + Pretty.block [ + ml_from_label class, + str ":", + Pretty.brk 1, + pv, + Pretty.brk 1, + (str o resolv) class + ] + fun from_membr (m, (_, ty)) = + Pretty.block [ + ml_from_label m, + str ":", + Pretty.brk 1, + ml_from_type NOBR ty + ] + in + Pretty.block [ + str "type", + Pretty.brk 1, + pv, + Pretty.brk 1, + (str o resolv) name, + Pretty.brk 1, + str "=", + Pretty.brk 1, + Pretty.enum "," "{" "};" ( + map from_supclass supclasses @ map from_membr membrs + ) + ] |> SOME + end | ml_from_def (_, Classmember _) = NONE - | ml_from_def (name, Classinst _) = - error ("can't serialize instance declaration " ^ quote name ^ " to ML") + | ml_from_def (name, Classinst (((class, (tyco, arity)), suparities), memdefs)) = + let + val definer = if null arity then "val" else "fun" + fun from_supclass (supclass, (inst, ls)) = str "" + fun from_memdef (m, def) = + ((the o ml_from_funs) [(m, Fun def)], Pretty.block [ + (str o resolv) m, + Pretty.brk 1, + str "=", + Pretty.brk 1, + (str o resolv) m + ]) + fun mk_memdefs supclassexprs [] = + Pretty.enum "," "{" "};" ( + supclassexprs + ) + | mk_memdefs supclassexprs memdefs = + let + val (defs, assigns) = (split_list o map from_memdef) memdefs; + in + Pretty.chunks [ + [str ("let"), Pretty.fbrk, defs |> Pretty.chunks] + |> Pretty.block, + [str ("in "), Pretty.enum "," "{" "};" (supclassexprs @ assigns)] + |> Pretty.block + ] + end; + in + Pretty.block [ + (Pretty.block o Pretty.breaks) ( + str definer + :: str name + :: map (str o fst) arity + ), + Pretty.brk 1, + str "=", + Pretty.brk 1, + mk_memdefs (map from_supclass suparities) memdefs + ] |> SOME + end; in case defs of (_, Fun _)::_ => ml_from_funs defs | (_, Datatypecons _)::_ => ml_from_datatypes defs @@ -601,10 +660,10 @@ in -fun ml_from_thingol target (nsp_dtcon, nsp_class, int_tyco) nspgrp = +fun ml_from_thingol target (nsp_dtcon, nsp_class, is_int_tyco) nspgrp = let val reserved_ml = ThmDatabase.ml_reserved @ [ - "bool", "int", "list", "true", "false" + "bool", "int", "list", "true", "false", "o" ]; fun ml_from_module _ ((_, name), ps) = Pretty.chunks ([ @@ -617,7 +676,7 @@ ]); fun needs_type (IType (tyco, _)) = has_nsp tyco nsp_class - orelse tyco = int_tyco + orelse is_int_tyco tyco | needs_type (IDictT _) = true | needs_type _ = @@ -641,9 +700,7 @@ |> debug 3 (fn _ => "eta-expanding...") |> eta_expand (eta_expander module const_syntax) |> debug 3 (fn _ => "eta-expanding polydefs...") - |> eta_expand_poly - |> debug 3 (fn _ => "eliminating classes...") - |> eliminate_classes; + |> eta_expand_poly; val parse_multi = OuterParse.name #-> (fn "dir" => @@ -655,15 +712,16 @@ (parse_multi || parse_internal serializer || parse_single_file serializer) - >> (fn seri => fn (tyco_syntax, const_syntax) => seri - (preprocess const_syntax) (tyco_syntax, const_syntax)) + >> (fn seri => fn (class_syntax, tyco_syntax, const_syntax) => seri + (preprocess const_syntax) (class_syntax, tyco_syntax, const_syntax)) end; end; (* local *) local -fun hs_from_defs is_cons (from_prim, (tyco_syntax, const_syntax)) resolv defs = +fun hs_from_defs is_cons (from_prim, (class_syntax, tyco_syntax, const_syntax)) + resolv defs = let fun upper_first s = let @@ -691,10 +749,14 @@ f; fun hs_from_sctxt vs = let + fun from_class cls = + case class_syntax cls + of NONE => (upper_first o resolv) cls + | SOME cls => cls fun from_sctxt [] = str "" | from_sctxt vs = vs - |> map (fn (v, cls) => str ((upper_first o resolv) cls ^ " " ^ lower_first v)) + |> map (fn (v, cls) => str (from_class cls ^ " " ^ lower_first v)) |> Pretty.enum "," "(" ")" |> (fn p => Pretty.block [p, str " => "]) in @@ -703,73 +765,39 @@ |> Library.flat |> from_sctxt end; - fun hs_from_type fxy ty = - let - fun from_itype fxy (IType (tyco, tys)) sctxt = - (case tyco_syntax tyco - of NONE => - sctxt - |> fold_map (from_itype BR) tys - |-> (fn tyargs => pair (brackify fxy ((str o upper_first o resolv) tyco :: tyargs))) - | SOME ((i, k), pr) => - if not (i <= length tys andalso length tys <= k) - then error ("number of argument mismatch in customary serialization: " - ^ (string_of_int o length) tys ^ " given, " ^ string_of_int i ^ " to " ^ string_of_int k - ^ " expected") - else (pr fxy hs_from_type tys, sctxt)) - | from_itype fxy (IFun (t1, t2)) sctxt = - sctxt - |> from_itype (INFX (1, X)) t1 - ||>> from_itype (INFX (1, R)) t2 - |-> (fn (p1, p2) => pair ( - brackify_infix (1, R) fxy [ - p1, - str "->", - p2 - ] - )) - | from_itype fxy (IVarT (v, [])) sctxt = - sctxt - |> pair ((str o lower_first) v) - | from_itype fxy (IVarT (v, sort)) sctxt = - sctxt - |> AList.default (op =) (v, []) - |> AList.map_entry (op =) v (fold (insert (op =)) sort) - |> pair ((str o lower_first) v) - | from_itype fxy (IDictT _) _ = - error "cannot serialize dictionary type to hs" - in - [] - |> from_itype fxy ty - ||> hs_from_sctxt - |> (fn (pty, pctxt) => Pretty.block [pctxt, pty]) - end; - fun hs_from_pat fxy (ICons ((f, ps), _)) = - (case const_syntax f + fun hs_from_type fxy (IType (tyco, tys)) = + (case tyco_syntax tyco of NONE => - ps - |> map (hs_from_pat BR) - |> cons ((str o resolv_const) f) - |> brackify fxy + brackify fxy ((str o upper_first o resolv) tyco :: map (hs_from_type BR) tys) | SOME ((i, k), pr) => - if not (i <= length ps andalso length ps <= k) + if not (i <= length tys andalso length tys <= k) then error ("number of argument mismatch in customary serialization: " - ^ (string_of_int o length) ps ^ " given, " ^ string_of_int i ^ " to " ^ string_of_int k + ^ (string_of_int o length) tys ^ " given, " + ^ string_of_int i ^ " to " ^ string_of_int k ^ " expected") - else pr fxy hs_from_expr (map iexpr_of_ipat ps)) - | hs_from_pat fxy (IVarP (v, _)) = + else pr fxy hs_from_type tys) + | hs_from_type fxy (IFun (t1, t2)) = + brackify_infix (1, R) fxy [ + hs_from_type (INFX (1, X)) t1, + str "->", + hs_from_type (INFX (1, R)) t2 + ] + | hs_from_type fxy (IVarT (v, _)) = (str o lower_first) v - and hs_from_expr fxy (e as IApp (e1, e2)) = - (case (unfold_app e) - of (e as (IConst (f, _)), es) => - hs_from_app fxy (f, es) + | hs_from_type fxy (IDictT _) = + error "can't serialize dictionary type to hs"; + fun hs_from_sctxt_type (sctxt, ty) = + Pretty.block [hs_from_sctxt sctxt, hs_from_type NOBR ty] + fun hs_from_expr fxy (e as IApp (e1, e2)) = + (case unfold_const_app e + of SOME x => hs_from_app fxy x | _ => brackify fxy [ hs_from_expr NOBR e1, hs_from_expr BR e2 ]) - | hs_from_expr fxy (e as IConst (f, _)) = - hs_from_app fxy (f, []) + | hs_from_expr fxy (e as IConst x) = + hs_from_app fxy (x, []) | hs_from_expr fxy (IVarE (v, _)) = (str o lower_first) v | hs_from_expr fxy (e as IAbs _) = @@ -787,7 +815,7 @@ let val (ps, body) = unfold_let e; fun mk_bind (p, e) = Pretty.block [ - hs_from_pat BR p, + hs_from_expr BR p, str " =", Pretty.brk 1, hs_from_expr NOBR e @@ -800,7 +828,7 @@ let fun mk_clause (p, e) = Pretty.block [ - hs_from_pat NOBR p, + hs_from_expr NOBR p, str " ->", Pretty.brk 1, hs_from_expr NOBR e @@ -814,26 +842,36 @@ Pretty.fbrk, (Pretty.chunks o map mk_clause) cs ] end - | hs_from_expr fxy (IInst (e, _)) = - hs_from_expr fxy e | hs_from_expr fxy (IDictE _) = - error "cannot serialize dictionary expression to hs" + error "can't serialize dictionary expression to hs" | hs_from_expr fxy (ILookup _) = - error "cannot serialize lookup expression to hs" - and hs_mk_app f es = - (str o resolv_const) f :: map (hs_from_expr BR) es - and hs_from_app fxy = - from_app hs_mk_app hs_from_expr const_syntax fxy; + error "can't serialize lookup expression to hs" + and hs_mk_app c es = + (str o resolv_const) c :: map (hs_from_expr BR) es + and hs_from_app fxy (((c, _), ls), es) = + from_app hs_mk_app hs_from_expr const_syntax fxy (c, es); + fun hs_from_funeqs (name, eqs) = + let + fun from_eq name (args, rhs) = + Pretty.block [ + str (lower_first name), + Pretty.block (map (fn p => Pretty.block [Pretty.brk 1, hs_from_expr BR p]) args), + Pretty.brk 1, + str ("="), + Pretty.brk 1, + hs_from_expr NOBR rhs + ] + in Pretty.chunks (map (from_eq name) eqs) end; fun hs_from_def (name, Undef) = error ("empty statement during serialization: " ^ quote name) | hs_from_def (name, Prim prim) = from_prim (name, prim) - | hs_from_def (name, Fun (eqs, (_, ty))) = + | hs_from_def (name, Fun (eqs, (sctxt, ty))) = let fun from_eq name (args, rhs) = Pretty.block [ str (lower_first name), - Pretty.block (map (fn p => Pretty.block [Pretty.brk 1, hs_from_pat BR p]) args), + Pretty.block (map (fn p => Pretty.block [Pretty.brk 1, hs_from_expr BR p]) args), Pretty.brk 1, str ("="), Pretty.brk 1, @@ -844,22 +882,20 @@ Pretty.block [ str (lower_first name ^ " ::"), Pretty.brk 1, - hs_from_type NOBR ty + hs_from_sctxt_type (sctxt, ty) ], - Pretty.chunks (map (from_eq name) eqs) + hs_from_funeqs (name, eqs) ] |> SOME end | hs_from_def (name, Typesyn (vs, ty)) = Pretty.block [ str "type ", - hs_from_sctxt vs, - str (upper_first name), - Pretty.block (map (fn (v, _) => str (" " ^ (lower_first) v)) vs), + hs_from_sctxt_type (vs, CodegenThingol.IType (name, map CodegenThingol.IVarT vs)), str " =", Pretty.brk 1, - hs_from_type NOBR ty + hs_from_sctxt_type ([], ty) ] |> SOME - | hs_from_def (name, Datatype ((vars, constrs), _)) = + | hs_from_def (name, Datatype ((vs, constrs), _)) = let fun mk_cons (co, tys) = (Pretty.block o Pretty.breaks) ( @@ -867,25 +903,26 @@ :: map (hs_from_type NOBR) tys ) in - Pretty.block ( + Pretty.block (( str "data " - :: hs_from_sctxt vars - :: str (upper_first name) - :: Pretty.block (map (fn (v, _) => str (" " ^ (lower_first) v)) vars) + :: hs_from_sctxt_type (vs, CodegenThingol.IType (name, map CodegenThingol.IVarT vs)) :: str " =" :: Pretty.brk 1 :: separate (Pretty.block [Pretty.brk 1, str "| "]) (map mk_cons constrs) - ) + ) @ [ + Pretty.brk 1, + str "deriving Show" + ]) end |> SOME | hs_from_def (_, Datatypecons _) = NONE | hs_from_def (name, Class ((supclasss, (v, membrs)), _)) = let - fun mk_member (m, (_, ty)) = + fun mk_member (m, (sctxt, ty)) = Pretty.block [ str (resolv m ^ " ::"), Pretty.brk 1, - hs_from_type NOBR ty + hs_from_sctxt_type (sctxt, ty) ] in Pretty.block [ @@ -899,16 +936,15 @@ end | hs_from_def (name, Classmember _) = NONE - | hs_from_def (_, Classinst ((clsname, (tyco, arity)), memdefs)) = + | hs_from_def (_, Classinst (((clsname, (tyco, arity)), _), memdefs)) = Pretty.block [ str "instance ", - hs_from_sctxt arity, - str ((upper_first o resolv) clsname), + hs_from_sctxt_type (arity, IType ((upper_first o resolv) clsname, map (IVarT o rpair [] o fst) arity)), str " ", - hs_from_type NOBR (IType (tyco, (map (IVarT o rpair [] o fst)) arity)), + hs_from_sctxt_type (arity, IType (tyco, map (IVarT o rpair [] o fst) arity)), str " where", Pretty.fbrk, - Pretty.chunks (map (fn (m, funn) => hs_from_def (m, Fun funn) |> the) memdefs) + Pretty.chunks (map (fn (m, (eqs, _)) => hs_from_funeqs (resolv m, eqs)) memdefs) ] |> SOME in case List.mapPartial (fn (name, def) => hs_from_def (name, def)) defs @@ -953,8 +989,8 @@ |> eta_expand (eta_expander const_syntax); in parse_multi_file ((K o K) NONE) "hs" serializer - >> (fn seri => fn (tyco_syntax, const_syntax) => seri - (preprocess const_syntax) (tyco_syntax, const_syntax)) + >> (fn seri => fn (class_syntax, tyco_syntax, const_syntax) => seri + (preprocess const_syntax) (class_syntax, tyco_syntax, const_syntax)) end; end; (* local *) diff -r a87c0aeae92f -r 31aed965135c src/Pure/Tools/codegen_thingol.ML --- a/src/Pure/Tools/codegen_thingol.ML Tue Jan 31 16:12:56 2006 +0100 +++ b/src/Pure/Tools/codegen_thingol.ML Tue Jan 31 16:14:37 2006 +0100 @@ -13,38 +13,31 @@ | IFun of itype * itype | IVarT of vname * sort | IDictT of (string * itype) list; - datatype ipat = - ICons of (string * ipat list) * itype - | IVarP of vname * itype; datatype iexpr = - IConst of string * itype + IConst of (string * itype) * ClassPackage.sortlookup list list | IVarE of vname * itype | IApp of iexpr * iexpr - | IInst of iexpr * ClassPackage.sortlookup list | IAbs of (vname * itype) * iexpr - | ICase of iexpr * (ipat * iexpr) list + | ICase of iexpr * (iexpr * iexpr) list | IDictE of (string * iexpr) list | ILookup of (string list * vname); val mk_funs: itype list * itype -> itype; val mk_apps: iexpr * iexpr list -> iexpr; val mk_abss: (vname * itype) list * iexpr -> iexpr; val pretty_itype: itype -> Pretty.T; - val pretty_ipat: ipat -> Pretty.T; val pretty_iexpr: iexpr -> Pretty.T; val unfoldl: ('a -> ('a * 'b) option) -> 'a -> 'a * 'b list; val unfoldr: ('a -> ('b * 'a) option) -> 'a -> 'b list * 'a; val unfold_fun: itype -> itype list * itype; val unfold_app: iexpr -> iexpr * iexpr list; val unfold_abs: iexpr -> (vname * itype) list * iexpr; - val unfold_let: iexpr -> (ipat * iexpr) list * iexpr; + val unfold_let: iexpr -> (iexpr * iexpr) list * iexpr; + val unfold_const_app: iexpr -> + (((string * itype) * ClassPackage.sortlookup list list) * iexpr list) option; val itype_of_iexpr: iexpr -> itype; - val itype_of_ipat: ipat -> itype; - val ipat_of_iexpr: iexpr -> ipat; - val iexpr_of_ipat: ipat -> iexpr; val eq_itype: itype * itype -> bool; val tvars_of_itypes: itype list -> string list; - val vars_of_ipats: ipat list -> string list; - val vars_of_iexprs: iexpr list -> string list; + val names_of_iexprs: iexpr list -> string list; val `%% : string * itype list -> itype; val `-> : itype * itype -> itype; @@ -54,7 +47,7 @@ val `|-> : (vname * itype) * iexpr -> iexpr; val `|--> : (vname * itype) list * iexpr -> iexpr; - type funn = (ipat list * iexpr) list * (ClassPackage.sortcontext * itype); + type funn = (iexpr list * iexpr) list * (ClassPackage.sortcontext * itype); datatype prim = Pretty of Pretty.T | Name of string; @@ -69,7 +62,9 @@ | Class of (class list * (vname * (string * (ClassPackage.sortcontext * itype)) list)) * string list | Classmember of class - | Classinst of (class * (string * (vname * sort) list)) * (string * funn) list; + | Classinst of ((class * (string * (vname * sort) list)) + * (class * (string * ClassPackage.sortlookup list list)) list) + * (string * funn) list; type module; type transact; type 'dst transact_fin; @@ -90,10 +85,8 @@ -> string -> transact -> transact; val start_transact: (transact -> 'a * transact) -> module -> 'a * module; - val extract_defs: iexpr -> string list; val eta_expand: (string -> int) -> module -> module; val eta_expand_poly: module -> module; - val eliminate_classes: module -> module; val debug_level: int ref; val debug: int -> ('a -> string) -> 'a -> 'a; @@ -164,17 +157,12 @@ (*ML auxiliary*) | IDictT of (string * itype) list; -datatype ipat = - ICons of (string * ipat list) * itype - | IVarP of vname * itype; - datatype iexpr = - IConst of string * itype + IConst of (string * itype) * ClassPackage.sortlookup list list | IVarE of vname * itype | IApp of iexpr * iexpr - | IInst of iexpr * ClassPackage.sortlookup list | IAbs of (vname * itype) * iexpr - | ICase of iexpr * (ipat * iexpr) list + | ICase of iexpr * (iexpr * iexpr) list (*ML auxiliary*) | IDictE of (string * iexpr) list | ILookup of (string list * vname); @@ -231,6 +219,11 @@ (fn ICase (e, [(p, e')]) => SOME ((p, e), e') | _ => NONE); +fun unfold_const_app e = + case unfold_app e + of (IConst x, es) => SOME (x, es) + | _ => NONE; + fun map_itype f_itype (IType (tyco, tys)) = tyco `%% map f_itype tys | map_itype f_itype (IFun (t1, t2)) = @@ -238,27 +231,20 @@ | map_itype _ (ty as IVarT _) = ty; -fun map_ipat f_itype f_ipat (ICons ((c, ps), ty)) = - ICons ((c, map f_ipat ps), f_itype ty) - | map_ipat _ _ (p as IVarP _) = - p; - -fun map_iexpr f_itype f_ipat f_iexpr (IApp (e1, e2)) = +fun map_iexpr f_itype f_iexpr (IApp (e1, e2)) = f_iexpr e1 `$ f_iexpr e2 - | map_iexpr f_itype f_ipat f_iexpr (IInst (e, c)) = - IInst (f_iexpr e, c) - | map_iexpr f_itype f_ipat f_iexpr (IAbs (v, e)) = + | map_iexpr f_itype f_iexpr (IAbs (v, e)) = IAbs (v, f_iexpr e) - | map_iexpr f_itype f_ipat f_iexpr (ICase (e, ps)) = - ICase (f_iexpr e, map (fn (p, e) => (f_ipat p, f_iexpr e)) ps) - | map_iexpr _ _ _ (e as IConst _) = + | map_iexpr f_itype f_iexpr (ICase (e, ps)) = + ICase (f_iexpr e, map (fn (p, e) => (f_iexpr p, f_iexpr e)) ps) + | map_iexpr _ _ (e as IConst _) = e - | map_iexpr _ _ _ (e as IVarE _) = + | map_iexpr _ _ (e as IVarE _) = e - | map_iexpr f_itype f_ipat f_iexpr (IDictE ms) = + | map_iexpr f_itype f_iexpr (IDictE ms) = IDictE (map (apsnd f_iexpr) ms) - | map_iexpr _ _ _ (e as ILookup _) = - e ; + | map_iexpr _ _ (e as ILookup _) = + e; fun fold_itype f_itype (IFun (t1, t2)) = f_itype t1 #> f_itype t2 @@ -267,22 +253,15 @@ | fold_itype _ (ty as IVarT _) = I; -fun fold_ipat f_itype f_ipat (ICons ((_, ps), ty)) = - f_itype ty #> fold f_ipat ps - | fold_ipat f_itype f_ipat (p as IVarP _) = - I; - -fun fold_iexpr f_itype f_ipat f_iexpr (IApp (e1, e2)) = +fun fold_iexpr f_itype f_iexpr (IApp (e1, e2)) = f_iexpr e1 #> f_iexpr e2 - | fold_iexpr f_itype f_ipat f_iexpr (IInst (e, c)) = - f_iexpr e - | fold_iexpr f_itype f_ipat f_iexpr (IAbs (v, e)) = + | fold_iexpr f_itype f_iexpr (IAbs (v, e)) = f_iexpr e - | fold_iexpr f_itype f_ipat f_iexpr (ICase (e, ps)) = - f_iexpr e #> fold (fn (p, e) => f_ipat p #> f_iexpr e) ps - | fold_iexpr _ _ _ (e as IConst _) = + | fold_iexpr f_itype f_iexpr (ICase (e, ps)) = + f_iexpr e #> fold (fn (p, e) => f_iexpr p #> f_iexpr e) ps + | fold_iexpr _ _ (e as IConst _) = I - | fold_iexpr _ _ _ (e as IVarE _) = + | fold_iexpr _ _ (e as IVarE _) = I; @@ -325,20 +304,12 @@ | pretty_itype (IDictT _) = Pretty.str ""; -fun pretty_ipat (ICons ((cons, ps), ty)) = - Pretty.enum " " "(" ")" - (Pretty.str cons :: map pretty_ipat ps @ [Pretty.str ":: ", pretty_itype ty]) - | pretty_ipat (IVarP (v, ty)) = - Pretty.block [Pretty.str ("?" ^ v ^ "::"), pretty_itype ty]; - -fun pretty_iexpr (IConst (f, ty)) = - Pretty.block [Pretty.str (f ^ "::"), pretty_itype ty] +fun pretty_iexpr (IConst ((c, ty), _)) = + Pretty.block [Pretty.str (c ^ "::"), pretty_itype ty] | pretty_iexpr (IVarE (v, ty)) = Pretty.block [Pretty.str ("?" ^ v ^ "::"), pretty_itype ty] | pretty_iexpr (IApp (e1, e2)) = Pretty.enclose "(" ")" [pretty_iexpr e1, Pretty.brk 1, pretty_iexpr e2] - | pretty_iexpr (IInst (e, c)) = - pretty_iexpr e | pretty_iexpr (IAbs ((v, ty), e)) = Pretty.enclose "(" ")" [Pretty.str ("?" ^ v ^ " |->"), Pretty.brk 1, pretty_iexpr e] | pretty_iexpr (ICase (e, cs)) = @@ -347,7 +318,7 @@ pretty_iexpr e, Pretty.enclose "(" ")" (map (fn (p, e) => Pretty.block [ - pretty_ipat p, + pretty_iexpr p, Pretty.str " => ", pretty_iexpr e ] @@ -361,7 +332,18 @@ (* language auxiliary *) -fun itype_of_iexpr (IConst (_, ty)) = ty + +fun instant_itype (v, sty) ty = + let + fun instant (IType (tyco, tys)) = + tyco `%% map instant tys + | instant (IFun (ty1, ty2)) = + instant ty1 `-> instant ty2 + | instant (w as (IVarT (u, _))) = + if v = u then sty else w + in instant ty end; + +fun itype_of_iexpr (IConst ((_, ty), s)) = ty | itype_of_iexpr (IVarE (_, ty)) = ty | itype_of_iexpr (e as IApp (e1, e2)) = (case itype_of_iexpr e1 of (IFun (ty2, ty')) => @@ -371,29 +353,9 @@ ^ ", " ^ (Pretty.output o pretty_itype) ty2 ^ " vs. " ^ (Pretty.output o pretty_itype o itype_of_iexpr) e2) | _ => error ("expression is not a function: " ^ Pretty.output (pretty_iexpr e1))) - | itype_of_iexpr (IInst (e, cs)) = itype_of_iexpr e | itype_of_iexpr (IAbs ((_, ty1), e2)) = ty1 `-> itype_of_iexpr e2 | itype_of_iexpr (ICase ((_, [(_, e)]))) = itype_of_iexpr e; -fun itype_of_ipat (ICons (_, ty)) = ty - | itype_of_ipat (IVarP (_, ty)) = ty; - -fun ipat_of_iexpr (IConst (f, ty)) = ICons ((f, []), ty) - | ipat_of_iexpr (IVarE v) = IVarP v - | ipat_of_iexpr (e as IApp _) = - (case unfold_app e - of (IConst (f, ty), es) => - ICons ((f, map ipat_of_iexpr es), (snd o unfold_fun) ty) - | (IInst (IConst (f, ty), _), es) => - ICons ((f, map ipat_of_iexpr es), (snd o unfold_fun) ty) - | _ => error ("illegal expression for pattern: " ^ (Pretty.output o pretty_iexpr) e)) - | ipat_of_iexpr e = - error ("illegal expression for pattern: " ^ (Pretty.output o pretty_iexpr) e); - -fun iexpr_of_ipat (ICons ((co, ps), ty)) = - IConst (co, map itype_of_ipat ps `--> ty) `$$ map iexpr_of_ipat ps - | iexpr_of_ipat (IVarP v) = IVarE v; - fun tvars_of_itypes tys = let fun vars (IType (_, tys)) = @@ -404,18 +366,10 @@ insert (op =) v in fold vars tys [] end; -fun vars_of_ipats ps = +fun names_of_iexprs es = let - fun vars (ICons ((_, ps), _)) = - fold vars ps - | vars (IVarP (v, _)) = - insert (op =) v - in fold vars ps [] end; - -fun vars_of_iexprs es = - let - fun vars (IConst (f, _)) = - I + fun vars (IConst ((c, _), _)) = + insert (op =) c | vars (IVarE (v, _)) = insert (op =) v | vars (IApp (e1, e2)) = @@ -425,32 +379,19 @@ #> vars e | vars (ICase (e, cs)) = vars e - #> fold (fn (p, e) => fold (insert (op =)) (vars_of_ipats [p]) #> vars e) cs - | vars (IInst (e, lookup)) = - vars e + #> fold (fn (p, e) => vars p #> vars e) cs | vars (IDictE ms) = fold (vars o snd) ms | vars (ILookup (_, v)) = cons v in fold vars es [] end; -fun instant_itype (v, sty) ty = - let - fun instant (IType (tyco, tys)) = - tyco `%% map instant tys - | instant (IFun (ty1, ty2)) = - instant ty1 `-> instant ty2 - | instant (w as (IVarT (u, _))) = - if v = u then sty else w - in instant ty end; - - (** language module system - definitions, modules, transactions **) (* type definitions *) -type funn = (ipat list * iexpr) list * (ClassPackage.sortcontext * itype); +type funn = (iexpr list * iexpr) list * (ClassPackage.sortcontext * itype); datatype prim = Pretty of Pretty.T @@ -467,7 +408,9 @@ | Class of (class list * (vname * (string * (ClassPackage.sortcontext * itype)) list)) * string list | Classmember of class - | Classinst of (class * (string * (vname * sort) list)) * (string * funn) list; + | Classinst of ((class * (string * (vname * sort) list)) + * (class * (string * ClassPackage.sortlookup list list)) list) + * (string * funn) list; datatype node = Def of def | Module of node Graph.T; type module = node Graph.T; @@ -489,7 +432,7 @@ Pretty.enum " |" "" "" ( map (fn (ps, body) => Pretty.block [ - Pretty.enum "," "[" "]" (map pretty_ipat ps), + Pretty.enum "," "[" "]" (map pretty_iexpr ps), Pretty.str " |->", Pretty.brk 1, pretty_iexpr body, @@ -531,7 +474,7 @@ Pretty.str "class member belonging to ", Pretty.str clsname ] - | pretty_def (Classinst ((clsname, (tyco, arity)), _)) = + | pretty_def (Classinst (((clsname, (tyco, arity)), _), _)) = Pretty.block [ Pretty.str "class instance (", Pretty.str clsname, @@ -748,16 +691,16 @@ apfst Module o Graph.fold_map_nodes (foldmap (prfix @ [name])) modl in Graph.fold_map_nodes (foldmap []) end; -fun map_def_fun f_ipat f_iexpr (Fun (eqs, cty)) = - Fun (map (fn (ps, rhs) => (map f_ipat ps, f_iexpr rhs)) eqs, cty) - | map_def_fun _ _ def = def; +fun map_def_fun f_iexpr (Fun (eqs, cty)) = + Fun (map (fn (ps, rhs) => (map f_iexpr ps, f_iexpr rhs)) eqs, cty) + | map_def_fun _ def = def; -fun transform_defs f_def f_ipat f_iexpr s modl = +fun transform_defs f_def f_iexpr s modl = let val (modl', s') = fold_map_defs f_def modl s in modl' - |> map_defs (map_def_fun (f_ipat s') (f_iexpr s')) + |> map_defs (map_def_fun (f_iexpr s')) end; fun merge_module modl12 = @@ -850,7 +793,7 @@ else error "attempted to add class with bare instances" | check_prep_def modl (Classmember _) = error "attempted to add bare class member" - | check_prep_def modl (Classinst ((d as (class, (tyco, arity)), memdefs))) = + | check_prep_def modl (Classinst ((d as ((class, (tyco, arity)), _), memdefs))) = let val Class ((_, (v, membrs)), _) = get_def modl class; val _ = if length memdefs > length memdefs @@ -881,7 +824,7 @@ #> add_dep (name, m) ) membrs ) - | postprocess_def (name, Classinst ((class, (tyco, _)), _)) = + | postprocess_def (name, Classinst (((class, (tyco, _)), _), _)) = map_def class (fn Datatype (d, insts) => Datatype (d, name::insts) | d => d) #> map_def class (fn Class (d, insts) => Class (d, name::insts)) @@ -979,25 +922,9 @@ (** generic transformation **) -fun extract_defs e = - let - fun extr_itype (ty as IType (tyco, _)) = - cons tyco #> fold_itype extr_itype ty - | extr_itype ty = - fold_itype extr_itype ty - fun extr_ipat (p as ICons ((c, _), _)) = - cons c #> fold_ipat extr_itype extr_ipat p - | extr_ipat p = - fold_ipat extr_itype extr_ipat p - fun extr_iexpr (e as IConst (f, _)) = - cons f #> fold_iexpr extr_itype extr_ipat extr_iexpr e - | extr_iexpr e = - fold_iexpr extr_itype extr_ipat extr_iexpr e - in extr_iexpr e [] end; - fun eta_expand query = let - fun eta_app ((f, ty), es) = + fun eta_app (((f, ty), ls), es) = let val delta = query f - length es; val add_n = if delta < 0 then 0 else delta; @@ -1006,20 +933,16 @@ |> curry Library.drop (length es) |> curry Library.take add_n val add_vars = - Term.invent_names (vars_of_iexprs es) "x" add_n ~~ tys; + Term.invent_names (names_of_iexprs es) "x" add_n ~~ tys; in - Library.foldr IAbs (add_vars, IConst (f, ty) `$$ es `$$ (map IVarE add_vars)) + Library.foldr IAbs (add_vars, + IConst ((f, ty), ls) `$$ es `$$ (map IVarE add_vars)) end; - fun eta_iexpr' e = map_iexpr I I eta_iexpr e - and eta_iexpr (IConst (f, ty)) = - eta_app ((f, ty), []) - | eta_iexpr (e as IApp _) = - (case (unfold_app e) - of (IConst (f, ty), es) => - eta_app ((f, ty), map eta_iexpr es) - | _ => eta_iexpr' e) - | eta_iexpr e = eta_iexpr' e; - in map_defs (map_def_fun I eta_iexpr) end; + fun eta_iexpr e = + case unfold_const_app e + of SOME x => eta_app x + | NONE => map_iexpr I eta_iexpr e; + in map_defs (map_def_fun eta_iexpr) end; val eta_expand_poly = let @@ -1029,124 +952,11 @@ then def else let - val add_var = (hd (Term.invent_names (vars_of_iexprs [e]) "x" 1), ty1) - in (Fun ([([IVarP add_var], IAbs (add_var, e))], cty)) end + val add_var = (hd (Term.invent_names (names_of_iexprs [e]) "x" 1), ty1) + in (Fun ([([IVarE add_var], IAbs (add_var, e))], cty)) end | map_def_fun def = def; in map_defs map_def_fun end; -(*fun eliminate_classes module = - let - fun transform_itype (IVarT (v, s)) = - IVarT (v, []) - | transform_itype (ty as IDictT _) = - ty - | transform_itype ty = - map_itype transform_itype ty; - fun transform_ipat p = - map_ipat transform_itype transform_ipat p; - fun transform_iexpr vname_alist (IInst (e, ls)) = - let - fun transform_lookup (ClassPackage.Instance ((cdict, idict), ls)) = - ls - |> transform_lookups - |-> (fn tys => - curry mk_apps (IConst (idict, cdict `%% tys)) - #> pair (cdict `%% tys)) - | transform_lookup (ClassPackage.Lookup (deriv, (v, i))) = - let - val (v', cls) = - (nth o the oo AList.lookup (op =)) vname_alist v i; - fun mk_parm tyco = tyco `%% [IVarT (v, [])]; - in (mk_parm cls, ILookup (deriv, v')) end - and transform_lookups lss = - map_yield (map_yield transform_lookup - #> apfst ** - #> apsnd XXe) lss - in transform_iexpr vname_alist e `$$ (snd o transform_lookups) ls end - | transform_iexpr vname_alist e = - map_iexpr transform_itype transform_ipat (transform_iexpr vname_alist) e; - fun elim_sorts (Fun (eqs, ([], ty))) = - Fun (map (fn (ps, rhs) => (map transform_ipat ps, transform_iexpr [] rhs)) eqs, - ([], transform_itype ty)) - | elim_sorts (Fun (eqs, (sortctxt, ty))) = - let - val varnames_ctxt = - burrow - (Term.invent_names ((vars_of_iexprs o map snd) eqs @ - (vars_of_ipats o Library.flat o map fst) eqs) "d" o length) - (map snd sortctxt); - val vname_alist = map2 (fn (vt, sort) => fn vs => (vt, vs ~~ sort)) - sortctxt varnames_ctxt; - val ty' = map (op ** o (fn (vt, vss) => map (fn (_, cls) => - cls `%% [IVarT (vt, [])]) vss)) vname_alist - `--> transform_itype ty; - val ps_add = map (XXp o (fn (vt, vss) => map (fn (v, cls) => - IVarP (v, cls `%% [IVarT (vt, [])])) vss)) vname_alist; - in Fun (map (fn (ps, rhs) => (ps_add @ map transform_ipat ps, transform_iexpr vname_alist rhs)) eqs, ([], ty')) end - | elim_sorts (Datatype (vars, constrs, insts)) = - Datatype (map (fn (v, _) => (v, [])) vars, map (apsnd (map transform_itype)) constrs, insts) - | elim_sorts (Typesyn (vars, ty)) = - Typesyn (map (fn (v, _) => (v, [])) vars, transform_itype ty) - | elim_sorts d = d; - fun mk_cls_typ_map v (supclss, membrs) ty_inst = - (map (fn class => (class, IType (class, [ty_inst]))) supclss, - map (fn (m, (mctxt, ty)) => - (m, ty |> instant_itype (v, ty_inst))) membrs); - fun extract_members (cls, Class (supclss, v, membrs, _)) = - let - val ty_cls = cls `%% [IVarT (v, [])]; - val w = "d"; - val add_supclss = if null supclss then I else cons (v, supclss); - fun mk_fun (m, (mctxt, ty)) = (m, Fun ([([IVarP (w, ty_cls)], ILookup ([m], w))], - (add_supclss mctxt, ty `-> ty_cls))); - in fold (cons o mk_fun) membrs end - | extract_members _ = I; - fun introduce_dicts (Class (supclss, v, membrs, insts)) = - let - val varname_cls = Term.invent_names (tvars_of_itypes (map (snd o snd) membrs)) "a" 1 |> hd - in - Typesyn ([(varname_cls, supclss)], IDictT ((op @) (mk_cls_typ_map v (supclss, membrs) (IVarT (varname_cls, []))))) - end - | introduce_dicts (Classinst ((clsname, (tyco, arity)), (supinsts, memdefs))) = - let - val Class (supclss, v, members, _) = - if clsname = class_eq - then - Class ([], "a", [(fun_eq, ([], IVarT ("a", []) `-> IVarT ("a", []) `-> Type_bool))], []) - else - get_def module clsname; - val ty = tyco `%% map IVarT arity; - val (supinst_typ_map, mem_typ_map) = mk_cls_typ_map v (supclss, members) ty; - fun mk_meminst (m, ty) = - let - val (instname, instlookup) = (the o AList.lookup (op =) memdefs) m; - in - IInst (IConst (instname, ty), instlookup) - |> pair m - end; - val memdefs_ty = map mk_meminst mem_typ_map; - fun mk_supinst (supcls, dictty) = - let - val (instname, instlookup) = (the o AList.lookup (op =) supinsts) supcls; - in - IInst (IConst (instname, dictty), instlookup) - |> pair supcls - end; - val instdefs_ty = map mk_supinst supinst_typ_map; - in - Fun ([([], IDictE (instdefs_ty @ memdefs_ty))], - (arity, IType (clsname, [ty]))) - end - | introduce_dicts d = d; - in - module - |> `(fn module => fold_defs extract_members module []) - |-> (fn membrs => fold (fn (name, f) => map_def name (K f)) membrs) - |> map_defs introduce_dicts - |> map_defs elim_sorts - end;*) - -fun eliminate_classes module = module; (** generic serialization **)