--- 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)) *)
);
--- 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 "<DUMMY>"
+ 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 *)
--- 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 "<DictT>";
-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 **)