--- a/src/Pure/Tools/codegen_package.ML Fri Dec 02 16:05:12 2005 +0100
+++ b/src/Pure/Tools/codegen_package.ML Fri Dec 02 16:05:31 2005 +0100
@@ -12,11 +12,10 @@
signature CODEGEN_PACKAGE =
sig
type deftab;
- type exprgen_type;
type exprgen_term;
+ type appgen;
type defgen;
- val add_codegen_type: string * exprgen_type -> theory -> theory;
- val add_codegen_expr: string * exprgen_term -> theory -> theory;
+ val add_appgen: string * appgen -> theory -> theory;
val add_defgen: string * defgen -> theory -> theory;
val add_lookup_tyco: string * string -> theory -> theory;
val add_lookup_const: (string * typ) * CodegenThingol.iexpr -> theory -> theory;
@@ -53,18 +52,23 @@
val ensure_def_const: theory -> deftab
-> string -> CodegenThingol.transact -> string * CodegenThingol.transact;
- val codegen_let: (int -> term -> term list * term)
- -> exprgen_term;
- val codegen_split: (int -> term -> term list * term)
- -> exprgen_term;
- val codegen_number_of: (term -> IntInf.int) -> (term -> term)
- -> exprgen_term;
- val codegen_case: (theory -> string -> (string * int) list option)
- -> exprgen_term;
+ val appgen_let: (int -> term -> term list * term)
+ -> appgen;
+ val appgen_split: (int -> term -> term list * term)
+ -> appgen;
+ val appgen_number_of: (term -> IntInf.int) -> (term -> term)
+ -> appgen;
+ val appgen_case: (theory -> string -> (string * int) list option)
+ -> appgen;
val defgen_datatype: (theory -> string -> (string list * string list) option)
+ -> (theory -> string * string -> typ list option)
-> defgen;
val defgen_datacons: (theory -> string * string -> typ list option)
-> defgen;
+ val defgen_datatype_eq: (theory -> string -> (string list * string list) option)
+ -> defgen;
+ val defgen_datatype_eqinst: (theory -> string -> (string list * string list) option)
+ -> defgen;
val defgen_recfun: (theory -> string * typ -> (term list * term) list * typ)
-> defgen;
@@ -81,7 +85,8 @@
(* auxiliary *)
-fun perhaps f x = f x |> the_default x;
+fun devarify_term t = (fst o Type.freeze_thaw) t;
+fun devarify_type ty = (fst o Type.freeze_thaw_type) ty;
(* code generator instantiation, part 1 *)
@@ -101,6 +106,7 @@
type exprgen_sort = theory -> deftab -> (sort, sort) gen_exprgen;
type exprgen_type = theory -> deftab -> (typ, itype) gen_exprgen;
type exprgen_term = theory -> deftab -> (term, iexpr) gen_exprgen;
+type appgen = theory -> deftab -> ((string * typ) * term list, iexpr) gen_exprgen;
type defgen = theory -> deftab -> gen_defgen;
@@ -140,29 +146,31 @@
exprgens_sort: (string * (exprgen_sort * stamp)) list,
exprgens_type: (string * (exprgen_type * stamp)) list,
exprgens_term: (string * (exprgen_term * stamp)) list,
+ appgens: (string * (appgen * stamp)) list,
defgens: (string * (defgen * stamp)) list
};
val empty_gens = {
exprgens_sort = Symtab.empty, exprgens_type = Symtab.empty,
- exprgens_term = Symtab.empty, defgens = Symtab.empty
+ exprgens_term = Symtab.empty, defgens = Symtab.empty, appgens = Symtab.empty
};
-fun map_gens f { exprgens_sort, exprgens_type, exprgens_term, defgens } =
+fun map_gens f { exprgens_sort, exprgens_type, exprgens_term, appgens, defgens } =
let
- val (exprgens_sort, exprgens_type, exprgens_term, defgens) =
- f (exprgens_sort, exprgens_type, exprgens_term, defgens)
+ val (exprgens_sort, exprgens_type, exprgens_term, appgens, defgens) =
+ f (exprgens_sort, exprgens_type, exprgens_term, appgens, defgens)
in { exprgens_sort = exprgens_sort, exprgens_type = exprgens_type,
- exprgens_term = exprgens_term, defgens = defgens } end;
+ exprgens_term = exprgens_term, appgens = appgens, defgens = defgens } end;
fun merge_gens
({ exprgens_sort = exprgens_sort1, exprgens_type = exprgens_type1,
- exprgens_term = exprgens_term1, defgens = defgens1 },
+ exprgens_term = exprgens_term1, appgens = appgens1, defgens = defgens1 },
{ exprgens_sort = exprgens_sort2, exprgens_type = exprgens_type2,
- exprgens_term = exprgens_term2, defgens = defgens2 }) =
+ exprgens_term = exprgens_term2, appgens = appgens2, defgens = defgens2 }) =
{ exprgens_sort = AList.merge (op =) (eq_snd (op =)) (exprgens_sort1, exprgens_sort2),
exprgens_type = AList.merge (op =) (eq_snd (op =)) (exprgens_type1, exprgens_type2),
exprgens_term = AList.merge (op =) (eq_snd (op =)) (exprgens_term1, exprgens_term2),
+ appgens = AList.merge (op =) (eq_snd (op =)) (appgens1, appgens2),
defgens = AList.merge (op =) (eq_snd (op =)) (defgens1, defgens2) } : gens;
type lookups = {
@@ -247,7 +255,7 @@
};
val empty = {
modl = empty_module,
- gens = { exprgens_sort = [], exprgens_type = [], exprgens_term = [], defgens = [] } : gens,
+ gens = { exprgens_sort = [], exprgens_type = [], exprgens_term = [], appgens = [], defgens = [] } : gens,
lookups = { lookups_tyco = Symtab.empty, lookups_const = Symtab.empty } : lookups,
logic_data = { is_datatype = NONE, alias = (Symtab.empty, Symtab.empty) } : logic_data,
serialize_data =
@@ -261,7 +269,10 @@
|> CodegenSerializer.add_prim ("wfrec", ("fun wfrec f x = f (wfrec f) x;", [])),
syntax_tyco = Symtab.empty, syntax_const = Symtab.empty })
|> Symtab.update ("haskell",
- { serializer = serializer_hs : CodegenSerializer.serializer, primitives = CodegenSerializer.empty_prims,
+ { serializer = serializer_hs : CodegenSerializer.serializer,
+ primitives =
+ CodegenSerializer.empty_prims
+ |> CodegenSerializer.add_prim ("wfrec", ("wfrec f x = f (wfrec f) x", [])),
syntax_tyco = Symtab.empty, syntax_const = Symtab.empty })
} : T;
val copy = I;
@@ -297,43 +308,54 @@
(fn (modl, gens, lookups, serialize_data, logic_data) =>
(modl,
gens |> map_gens
- (fn (exprgens_sort, exprgens_type, exprgens_term, defgens) =>
+ (fn (exprgens_sort, exprgens_type, exprgens_term, appgens, defgens) =>
(exprgens_sort
|> Output.update_warn (op =) ("overwriting existing class code generator " ^ name) (name, (cg, stamp ())),
- exprgens_type, exprgens_term, defgens)), lookups, serialize_data, logic_data));
+ exprgens_type, exprgens_term, appgens, defgens)), lookups, serialize_data, logic_data));
fun add_codegen_type (name, cg) =
map_codegen_data
(fn (modl, gens, lookups, serialize_data, logic_data) =>
(modl,
gens |> map_gens
- (fn (exprgens_sort, exprgens_type, exprgens_term, defgens) =>
+ (fn (exprgens_sort, exprgens_type, exprgens_term, appgens, defgens) =>
(exprgens_sort,
exprgens_type
|> Output.update_warn (op =) ("overwriting existing type code generator " ^ name) (name, (cg, stamp ())),
- exprgens_term, defgens)), lookups, serialize_data, logic_data));
+ exprgens_term, appgens, defgens)), lookups, serialize_data, logic_data));
fun add_codegen_expr (name, cg) =
map_codegen_data
(fn (modl, gens, lookups, serialize_data, logic_data) =>
(modl,
gens |> map_gens
- (fn (exprgens_sort, exprgens_type, exprgens_term, defgens) =>
+ (fn (exprgens_sort, exprgens_type, exprgens_term, appgens, defgens) =>
(exprgens_sort, exprgens_type,
exprgens_term
|> Output.update_warn (op =) ("overwriting existing expression code generator " ^ name) (name, (cg, stamp ())),
- defgens)),
+ appgens, defgens)),
lookups, serialize_data, logic_data));
+fun add_appgen (name, ag) =
+ map_codegen_data
+ (fn (modl, gens, lookups, serialize_data, logic_data) =>
+ (modl,
+ gens |> map_gens
+ (fn (exprgens_sort, exprgens_type, exprgens_term, appgens, defgens) =>
+ (exprgens_sort, exprgens_type, exprgens_term,
+ appgens
+ |> Output.update_warn (op =) ("overwriting existing definition application generator " ^ name) (name, (ag, stamp ())),
+ defgens)), lookups, serialize_data, logic_data));
+
fun add_defgen (name, dg) =
map_codegen_data
(fn (modl, gens, lookups, serialize_data, logic_data) =>
(modl,
gens |> map_gens
- (fn (exprgens_sort, exprgens_type, exprgens_term, defgens) =>
+ (fn (exprgens_sort, exprgens_type, exprgens_term, appgens, defgens) =>
(exprgens_sort, exprgens_type, exprgens_term,
- defgens
- |> Output.update_warn (op =) ("overwriting existing definition code generator " ^ name) (name, (dg, stamp ())))),
+ appgens, defgens
+ |> Output.update_warn (op =) ("overwriting existing definition definition generator " ^ name) (name, (dg, stamp ())))),
lookups, serialize_data, logic_data));
val get_lookups_tyco = #lookups_tyco o #lookups o CodegenData.get;
@@ -450,17 +472,6 @@
| s => s;
-(* auxiliary *)
-
-fun find_lookup_expr thy (f, ty) =
- Symtab.lookup_multi ((#lookups_const o #lookups o CodegenData.get) thy) f
- |> (fn tab => AList.lookup (Sign.typ_instance thy) tab ty)
-
-fun name_of_tvar (TFree (v, _)) = v |> unprefix "'"
- | name_of_tvar (TVar ((v, i), _)) =
- (if i=0 then v else v ^ string_of_int i) |> unprefix "'"
-
-
(* code generator instantiation, part 2 *)
fun invoke_cg_sort thy defs sort trns =
@@ -478,14 +489,30 @@
((map (apsnd (fn (cg, _) => cg thy defs)) o #exprgens_term o #gens o CodegenData.get) thy)
("generating expression " ^ (quote o Sign.string_of_term thy) t) t trns;
+fun invoke_appgen thy defs (app as ((f, ty), ts)) trns =
+ gen_invoke
+ ((map (apsnd (fn (ag, _) => ag thy defs)) o #appgens o #gens o CodegenData.get) thy)
+ ("generating application " ^ f ^ "::" ^ (Sign.string_of_typ thy) ty
+ ^ " " ^ enclose "(" ")" (commas (map (Sign.string_of_term thy) ts))) app trns;
+
+fun find_lookup_expr thy (f, ty) =
+ Symtab.lookup_multi ((#lookups_const o #lookups o CodegenData.get) thy) f
+ |> (fn tab => AList.lookup (Sign.typ_instance thy) tab ty);
+
fun get_defgens thy defs =
(map (apsnd (fn (dg, _) => dg thy defs)) o #defgens o #gens o CodegenData.get) thy;
-fun ensure_def_class thy defs cls_or_inst trns =
+fun ensure_def_class thy defs cls trns =
trns
- |> debug 4 (fn _ => "generating class or instance " ^ quote cls_or_inst)
- |> gen_ensure_def (get_defgens thy defs) ("generating class/instance " ^ quote cls_or_inst) cls_or_inst
- |> pair cls_or_inst;
+ |> debug 4 (fn _ => "generating class " ^ quote cls)
+ |> gen_ensure_def (get_defgens thy defs) ("generating class " ^ quote cls) cls
+ |> pair cls;
+
+fun ensure_def_instance thy defs inst trns =
+ trns
+ |> debug 4 (fn _ => "generating instance " ^ quote inst)
+ |> gen_ensure_def (get_defgens thy defs) ("generating instance " ^ quote inst) inst
+ |> pair inst;
fun ensure_def_tyco thy defs tyco trns =
if NameSpace.is_qualified tyco
@@ -506,9 +533,9 @@
of NONE =>
trns
|> debug 4 (fn _ => "generating constant " ^ quote f)
- |> invoke_cg_type thy defs (cname_of_idf thy defs f |> the |> snd)
+ |> invoke_cg_type thy defs (cname_of_idf thy defs f |> the |> snd |> devarify_type)
||> gen_ensure_def (get_defgens thy defs) ("generating constant " ^ quote f) f
- |-> (fn ty' => pair f)
+ |-> (fn _ => pair f)
| SOME (IConst (f, ty)) =>
trns
|> pair f
@@ -523,29 +550,34 @@
|-> (fn sort => pair (unprefix "'" v, sort))
fun mk_eq (args, rhs) trns =
trns
- |> fold_map (invoke_cg_expr thy defs) args
- ||>> invoke_cg_expr thy defs rhs
+ |> fold_map (invoke_cg_expr thy defs o devarify_term) args
+ ||>> (invoke_cg_expr thy defs o devarify_term) rhs
|-> (fn (args, rhs) => pair (map ipat_of_iexpr args, rhs))
in
trns
|> fold_map mk_eq eqs
- ||>> invoke_cg_type thy defs ty
+ ||>> invoke_cg_type thy defs (devarify_type ty)
||>> fold_map mk_sortvar sortctxt
|-> (fn ((eqs, ty), sortctxt) => pair (Fun (eqs, (sortctxt, ty))))
end;
-fun fix_nargs thy defs gen i (t, ts) trns =
- if length ts < i
- then
+fun fix_nargs thy defs gen (imin, imax) (t, ts) trns =
+ if length ts < imin then
trns
|> debug 10 (fn _ => "eta-expanding")
- |> gen (strip_comb (Codegen.eta_expand t ts i))
+ |> gen (strip_comb (Codegen.eta_expand t ts imin))
+ |-> succeed
+ else if length ts > imax then
+ trns
+ |> debug 10 (fn _ => "splitting arguments (" ^ string_of_int imax ^ ", " ^ string_of_int (length ts) ^ ")")
+ |> gen (t, Library.take (imax, ts))
+ ||>> fold_map (invoke_cg_expr thy defs) (Library.drop (imax, ts))
+ |-> succeed o mk_apps
else
trns
- |> debug 10 (fn _ => "splitting arguments (" ^ string_of_int i ^ ", " ^ string_of_int (length ts) ^ ")")
- |> gen (t, Library.take (i, ts))
- ||>> fold_map (invoke_cg_expr thy defs) (Library.drop (i, ts))
- |-> pair o mk_apps;
+ |> debug 10 (fn _ => "keeping arguments")
+ |> gen (t, ts)
+ |-> succeed;
local
open CodegenThingolOp;
@@ -566,14 +598,12 @@
(sort |> filter (ClassPackage.is_class thy) |> map (idf_of_name thy nsp_class))
|-> (fn sort => succeed sort)
-fun exprgen_type_default thy defs(v as TVar (_, sort)) trns =
+fun exprgen_type_default thy defs (TVar _) trns =
+ error "TVar encountered during code generation"
+ | exprgen_type_default thy defs (TFree (v, sort)) trns =
trns
|> invoke_cg_sort thy defs sort
- |-> (fn sort => succeed (IVarT (name_of_tvar v, sort)))
- | exprgen_type_default thy defs (v as TFree (_, sort)) trns =
- trns
- |> invoke_cg_sort thy defs sort
- |-> (fn sort => succeed (IVarT (name_of_tvar v, sort)))
+ |-> (fn sort => succeed (IVarT (v |> unprefix "'", sort)))
| exprgen_type_default thy defs (Type ("fun", [t1, t2])) trns =
trns
|> invoke_cg_type thy defs t1
@@ -586,53 +616,85 @@
|-> (fn (tyco, tys) => succeed (tyco `%% tys))
fun exprgen_term_default thy defs (Const (f, ty)) trns =
- let
- val _ = debug 5 (fn _ => "making application of " ^ quote f) ();
- val ty_def = Sign.the_const_constraint thy f;
- val _ = debug 10 (fn _ => "making application (2)") ();
- fun mk_lookup (ClassPackage.Instance (i, ls)) trns =
- trns
- |> ensure_def_class thy defs ((idf_of_name thy nsp_class o fst) i)
- ||>> ensure_def_class thy defs (idf_of_inst thy defs i)
- ||>> (fold_map o fold_map) mk_lookup ls
- |-> (fn ((cls, i), ls) => pair (ClassPackage.Instance ((cls, i), ls)))
- | mk_lookup (ClassPackage.Lookup (clss, (v, i))) trns =
- trns
- |> fold_map (ensure_def_class thy defs) (map (idf_of_name thy nsp_class) clss)
- |-> (fn clss => pair (ClassPackage.Lookup (clss, (name_of_tvar (TFree (v, [])), i))));
- val _ = debug 10 (fn _ => "making application (3)") ();
- fun mk_itapp e [] = e
- | mk_itapp e lookup = IInst (e, lookup);
- in
- trns
- |> debug 10 (fn _ => "making application (4): " ^ f ^ "::" ^ Sign.string_of_typ thy ty ^ " <~> " ^ Sign.string_of_typ thy ty_def)
- |> ensure_def_const thy defs (idf_of_cname thy defs (f, ty))
- |> debug 10 (fn _ => "making application (5)")
- ||>> (fold_map o fold_map) mk_lookup (ClassPackage.extract_sortlookup thy (ty_def, ty))
- |> debug 10 (fn _ => "making application (6)")
- ||>> invoke_cg_type thy defs ty
- |> debug 10 (fn _ => "making application (7)")
- |-> (fn ((f, lookup), ty) =>
- succeed (mk_itapp (IConst (f, ty)) lookup))
- end
+ trns
+ |> invoke_appgen thy defs ((f, ty), [])
+ |-> (fn e => succeed e)
+ | exprgen_term_default thy defs (Var ((v, i), ty)) trns =
+ trns
+ |> invoke_cg_type thy defs ty
+ |-> (fn ty => succeed (IVarE (if i = 0 then v else v ^ "_" ^ string_of_int i, ty)))
| exprgen_term_default thy defs (Free (v, ty)) trns =
trns
|> invoke_cg_type thy defs ty
|-> (fn ty => succeed (IVarE (v, ty)))
- | exprgen_term_default thy defs (Var ((v, i), ty)) trns =
- trns
- |> invoke_cg_type thy defs ty
- |-> (fn ty => succeed (IVarE (if i=0 then v else v ^ string_of_int i, ty)))
| exprgen_term_default thy defs (Abs (v, ty, t)) trns =
trns
|> invoke_cg_type thy defs ty
||>> invoke_cg_expr thy defs (subst_bound (Free (v, ty), t))
|-> (fn (ty, e) => succeed ((v, ty) `|-> e))
- | exprgen_term_default thy defs (t1 $ t2) trns =
+ | exprgen_term_default thy defs (t as t1 $ t2) trns =
+ let
+ val (t', ts) = strip_comb t
+ in case t'
+ of Const (f, ty) =>
+ trns
+ |> invoke_appgen thy defs ((f, ty), ts)
+ |-> (fn e => succeed e)
+ | _ =>
+ trns
+ |> invoke_cg_expr thy defs t'
+ ||>> fold_map (invoke_cg_expr thy defs) ts
+ |-> (fn (e, es) => succeed (e `$$ es))
+ end;
+
+fun appgen_default thy defs ((f, ty), ts) trns =
+ let
+ val _ = debug 5 (fn _ => "making application of " ^ quote f) ();
+ val ty_def = Sign.the_const_constraint thy f;
+ val _ = debug 10 (fn _ => "making application (2)") ();
+ fun mk_lookup (ClassPackage.Instance (i, ls)) trns =
+ trns
+ |> ensure_def_class thy defs ((idf_of_name thy nsp_class o fst) i)
+ ||>> ensure_def_instance thy defs (idf_of_inst thy defs i)
+ ||>> (fold_map o fold_map) mk_lookup ls
+ |-> (fn ((cls, i), ls) => pair (ClassPackage.Instance ((cls, i), ls)))
+ | mk_lookup (ClassPackage.Lookup (clss, (v, i))) trns =
+ trns
+ |> fold_map (ensure_def_class thy defs) (map (idf_of_name thy nsp_class) clss)
+ |-> (fn clss => pair (ClassPackage.Lookup (clss, (v |> unprefix "'", i))));
+ val _ = debug 10 (fn _ => "making application (3)") ();
+ fun mk_itapp e [] = e
+ | mk_itapp e lookup = IInst (e, lookup);
+ in
+ trns
+ |> debug 10 (fn _ => "making application (4): " ^ f ^ "::" ^ Sign.string_of_typ thy ty ^ " <~> " ^ Sign.string_of_typ thy ty_def)
+ |> ensure_def_const thy defs (idf_of_cname thy defs (f, ty))
+ ||> debug 10 (fn _ => "making application (5)")
+ ||>> (fold_map o fold_map) mk_lookup (ClassPackage.extract_sortlookup thy (ty_def, ty))
+ ||> debug 10 (fn _ => "making application (6)")
+ ||>> invoke_cg_type thy defs ty
+ ||> debug 10 (fn _ => "making application (7)")
+ ||>> fold_map (invoke_cg_expr thy defs) ts
+ ||> debug 10 (fn _ => "making application (8)")
+ |-> (fn (((f, lookup), ty), es) =>
+ succeed (mk_itapp (IConst (f, ty)) lookup `$$ es))
+ end
+
+fun appgen_neg thy defs (f as ("neg", Type ("fun", [ty, _])), ts) trns =
+ let
+ fun gen_neg _ trns =
+ trns
+ |> invoke_cg_expr thy defs (Const ("op >", ty --> ty --> Type ("bool", [])) $ Const ("0", ty))
+ in
+ trns
+ |> fix_nargs thy defs gen_neg (0, 0) (Const f, ts)
+ end
+ | appgen_neg thy defs ((f, _), _) trns =
trns
- |> invoke_cg_expr thy defs t1
- ||>> invoke_cg_expr thy defs t2
- |-> (fn (e1, e2) => succeed (e1 `$ e2));
+ |> fail ("not a negation: " ^ quote f);
+
+fun exprgen_term_eq thy defs (Const ("op =", Type ("fun", [ty, _]))) trns =
+ trns
(*fun codegen_eq thy defs t trns =
let
@@ -650,18 +712,6 @@
|> fail ("no equality: " ^ Sign.string_of_term thy t)
in cg_eq (strip_comb t) end;*)
-fun codegen_neg thy defs t trns =
- let
- val (u, ts) = strip_comb t;
- fun cg_neg (Const ("neg", _)) =
- trns
- |> invoke_cg_expr thy defs (hd ts)
- |-> (fn e => succeed (Fun_lt `$ e `$ IConst ("0", Type_integer)))
- | cg_neg _ =
- trns
- |> fail ("no negation: " ^ Sign.string_of_term thy t)
- in cg_neg u end;
-
(* definition generators *)
@@ -692,7 +742,7 @@
of SOME (args, rhs, ty) =>
trns
|> debug 5 (fn _ => "trying defgen def for " ^ quote f)
- |> mk_fun thy defs [(args, rhs)] ty
+ |> mk_fun thy defs [(args, rhs)] (devarify_type ty)
|-> (fn def => succeed (def, []))
| _ => trns |> fail ("no definition found for " ^ quote f);
@@ -721,7 +771,7 @@
in
trns
|> debug 5 (fn _ => "trying defgen class member for " ^ quote f)
- |> invoke_cg_type thy defs ty
+ |> (invoke_cg_type thy defs o devarify_type) ty
|-> (fn ty => succeed (Classmember (cls, "a", ty), []))
end
| _ =>
@@ -731,16 +781,22 @@
case inst_of_idf thy defs clsinst
of SOME (cls, tyco) =>
let
+ val _ = debug 10 (fn _ => "(1) CLSINST " ^ cls ^ " - " ^ tyco) ()
val arity = (map o map) (idf_of_name thy nsp_class)
(ClassPackage.get_arities thy [cls] tyco);
+ val _ = debug 10 (fn _ => "(2) CLSINST " ^ cls ^ " - " ^ tyco) ()
val clsmems = map (idf_of_name thy nsp_mem)
(ClassPackage.the_consts thy cls);
+ val _ = debug 10 (fn _ => "(3) CLSINST " ^ cls ^ " - " ^ tyco) ()
+ val _ = debug 10 (fn _ => AList.string_of_alist I (Sign.string_of_typ thy) (ClassPackage.get_inst_consts_sign thy (tyco, cls))) ()
val instmem_idfs = map (idf_of_cname thy defs)
(ClassPackage.get_inst_consts_sign thy (tyco, cls));
- fun add_vars arity clsmems (trns as (_, univ)) =
+ val _ = debug 10 (fn _ => "(4) CLSINST " ^ cls ^ " - " ^ tyco) ()
+ fun add_vars arity clsmems (trns as (_, modl)) =
((Term.invent_names
- (map ((fn Classmember (_, _, ty) => ty) o get_def univ)
+ (map ((fn Classmember (_, _, ty) => ty) o get_def modl)
clsmems |> tvars_of_itypes) "a" (length arity) ~~ arity, clsmems), trns)
+ val _ = debug 10 (fn _ => "(5) CLSINST " ^ cls ^ " - " ^ tyco) ()
in
trns
|> debug 5 (fn _ => "trying defgen class instance for (" ^ quote cls ^ ", " ^ quote tyco ^ ")")
@@ -759,69 +815,82 @@
(* parametrized generators, for instantiation in HOL *)
-fun codegen_let strip_abs thy defs t trns =
- let
- fun dest_let (l as Const ("Let", _) $ t $ u) =
- (case strip_abs 1 u
- of ([p], u') => apfst (cons (p, t)) (dest_let u')
- | _ => ([], l))
- | dest_let t = ([], t);
- fun mk_let (l, r) trns =
- trns
- |> invoke_cg_expr thy defs l
- ||>> invoke_cg_expr thy defs r
- |-> (fn (l, r) => pair (r, ipat_of_iexpr l));
- fun cg_let' ([], _) _ =
+fun appgen_let strip_abs thy defs (f as ("Let", _), ts) trns =
+ let
+ fun dest_let (l as Const ("Let", _) $ t $ u) =
+ (case strip_abs 1 u
+ of ([p], u') => apfst (cons (p, t)) (dest_let u')
+ | _ => ([], l))
+ | dest_let t = ([], t);
+ fun mk_let (l, r) trns =
trns
- |> fail ("no let expression: " ^ Sign.string_of_term thy t)
- | cg_let' (lets, body) args =
- trns
- |> fold_map mk_let lets
- ||>> invoke_cg_expr thy defs body
- ||>> fold_map (invoke_cg_expr thy defs) args
- |-> (fn ((lets, body), args) =>
- succeed (Library.foldr (fn ((e, p), body) => ICase (e, [(p, body)])) (lets, body) `$$ args))
- fun cg_let (t1 as Const ("Let", _), t2 :: t3 :: ts) =
- cg_let' (dest_let (t1 $ t2 $ t3)) ts
- | cg_let _ =
- trns
- |> fail ("no let expression: " ^ Sign.string_of_term thy t);
- in cg_let (strip_comb t) end;
+ |> invoke_cg_expr thy defs l
+ ||>> invoke_cg_expr thy defs r
+ |-> (fn (l, r) => pair (r, ipat_of_iexpr l));
+ fun gen_let (t1, [t2, t3]) trns =
+ let
+ val (lets, body) = dest_let (t1 $ t2 $ t3)
+ in
+ trns
+ |> fold_map mk_let lets
+ ||>> invoke_cg_expr thy defs body
+ |-> (fn (lets, body) =>
+ pair (Library.foldr (fn ((e, p), body) => ICase (e, [(p, body)])) (lets, body)))
+ end;
+ in
+ trns
+ |> fix_nargs thy defs gen_let (2, 2) (Const f, ts)
+ end
+ | appgen_let strip_abs thy defs ((f, _), _) trns =
+ trns
+ |> fail ("not a let: " ^ quote f);
-fun codegen_split strip_abs thy defs t trns =
- let
- fun cg_split' ([p], body) args =
- trns
- |> invoke_cg_expr thy defs p
- ||>> invoke_cg_expr thy defs body
- ||>> fold_map (invoke_cg_expr thy defs) args
- |-> (fn (((IVarE v), body), args) => succeed (IAbs (v, body) `$$ args))
- | cg_split' _ _ =
- trns
- |> fail ("no split expression: " ^ Sign.string_of_term thy t);
- fun cg_split (t1 as Const ("split", _), t2 :: ts) =
- cg_split' (strip_abs 1 (t1 $ t2)) ts
- | cg_split _ =
+fun appgen_split strip_abs thy defs (f as ("split", _), ts) trns =
+ let
+ fun gen_split (t1, [t2]) trns =
+ let
+ val ([p], body) = strip_abs 1 (t1 $ t2)
+ in
+ trns
+ |> invoke_cg_expr thy defs p
+ ||>> invoke_cg_expr thy defs body
+ |-> (fn (IVarE v, body) => pair (IAbs (v, body)))
+ end
+ in
+ trns
+ |> fix_nargs thy defs gen_split (1, 1) (Const f, ts)
+ end
+ | appgen_split strip_abs thy defs ((f, _), _) trns =
+ trns
+ |> fail ("not a split: " ^ quote f);
+
+fun appgen_number_of dest_binum mk_int_to_nat thy defs (f as ("Numeral.number_of",
+ Type ("fun", [_, Type ("IntDef.int", [])])), ts) trns =
+ let
+ fun gen_num (_, [bin]) trns =
trns
- |> fail ("no split expression: " ^ Sign.string_of_term thy t);
- in cg_split (strip_comb t) end;
-
-fun codegen_number_of dest_binum mk_int_to_nat thy defs (Const ("Numeral.number_of",
- Type ("fun", [_, Type ("IntDef.int", [])])) $ bin) trns =
+ |> (pair (IConst ((IntInf.toString o dest_binum) bin, Type_integer))
+ handle TERM _
+ => error ("not a number: " ^ Sign.string_of_term thy bin))
+ in
+ trns
+ |> fix_nargs thy defs gen_num (1, 1) (Const f, ts)
+ end
+ | appgen_number_of dest_binum mk_int_to_nat thy defs (f as ("Numeral.number_of",
+ Type ("fun", [_, Type ("nat", [])])), ts) trns =
+ let
+ fun gen_num (_, [bin]) trns =
+ trns
+ |> invoke_cg_expr thy defs (mk_int_to_nat bin)
+ in
+ trns
+ |> fix_nargs thy defs gen_num (1, 1) (Const f, ts)
+ end
+ | appgen_number_of dest_binum mk_int_to_nat thy defs ((f, _), _) trns =
trns
- |> (succeed (IConst ((IntInf.toString o dest_binum) bin, Type_integer))
- handle TERM _
- => fail ("not a number: " ^ Sign.string_of_term thy bin))
- | codegen_number_of dest_binum mk_int_to_nat thy defs (Const ("Numeral.number_of",
- Type ("fun", [_, Type ("nat", [])])) $ bin) trns =
- trns
- |> invoke_cg_expr thy defs (mk_int_to_nat bin)
- |-> (fn expr => succeed expr)
- | codegen_number_of dest_binum mk_int_to_nat thy defs t trns =
- trns
- |> fail ("not a number: " ^ Sign.string_of_term thy t);
+ |> fail ("not a number_of: " ^ quote f);
-fun codegen_case get_case_const_data thy defs t trns =
+fun appgen_case get_case_const_data thy defs ((f, ty), ts) trns =
let
fun cg_case_d gen_names dty (((cname, i), ty), t) trns =
let
@@ -849,42 +918,47 @@
||>> fold_map (cg_case_d gen_names dty) (cs ~~ ts')
|-> (fn (t, ds) => pair (ICase (t, ds)))
end;
- in case strip_comb t
- of (t as Const (f, ty), ts) =>
- (case get_case_const_data thy f
- of NONE =>
- trns
- |> fail ("not a case constant: " ^ quote f)
- | SOME cs =>
- let
- val (tys, dty) = (split_last o fst o strip_type) ty;
- in
- trns
- |> debug 9 (fn _ => "for case const " ^ f ^ "::"
- ^ Sign.string_of_typ thy ty ^ ",\n with " ^ AList.string_of_alist I string_of_int cs
- ^ ",\n given as args " ^ (commas o map (Sign.string_of_term thy)) ts
- ^ ",\n with significant length " ^ string_of_int (length cs + 1))
- |> fix_nargs thy defs (cg_case dty (cs ~~ tys))
- (length cs + 1) (t, ts)
- |-> succeed
- end
- )
- | _ =>
- trns
- |> fail ("not a caseconstant expression: " ^ Sign.string_of_term thy t)
+ in
+ case get_case_const_data thy f
+ of NONE =>
+ trns
+ |> fail ("not a case constant: " ^ quote f)
+ | SOME cs =>
+ let
+ val (tys, dty) = (split_last o fst o strip_type) ty;
+ in
+ trns
+ |> debug 9 (fn _ => "for case const " ^ f ^ "::"
+ ^ Sign.string_of_typ thy ty ^ ",\n with " ^ AList.string_of_alist I string_of_int cs
+ ^ ",\n given as args " ^ (commas o map (Sign.string_of_term thy)) ts
+ ^ ",\n with significant length " ^ string_of_int (length cs + 1))
+ |> fix_nargs thy defs (cg_case dty (cs ~~ tys))
+ (length cs + 1, length cs + 1) (Const (f, ty), ts)
+ end
end;
-fun defgen_datatype get_datatype thy defs tyco trns =
+local
+
+fun add_eqinst get_datacons thy modl dtname cnames =
+ if forall (is_eqtype modl)
+ (Library.flat (map (fn cname => get_datacons thy (cname, dtname)) cnames))
+ then append [idf_of_name thy nsp_eq_class dtname]
+ else I
+
+in
+
+fun defgen_datatype get_datatype get_datacons thy defs tyco trns =
case tname_of_idf thy tyco
of SOME dtname =>
- (case get_datatype thy tyco
+ (case get_datatype thy dtname
of SOME (vs, cnames) =>
trns
|> debug 5 (fn _ => "trying defgen datatype for " ^ quote dtname)
|> succeed (Datatype (map (rpair [] o unprefix "'") vs, [], []),
cnames
|> map (idf_of_name thy nsp_const)
- |> map (fn "0" => "const.Zero" | c => c))
+ |> map (fn "0" => "const.Zero" | c => c)
+ (* |> add_eqinst get_datacons thy (snd trns) dtname cnames *))
(*! VARIABLEN, EQTYPE !*)
| NONE =>
trns
@@ -894,6 +968,8 @@
|> fail ("not a type constructor: " ^ quote tyco)
end;
+end; (* local *)
+
fun defgen_datacons get_datacons thy defs f trns =
let
fun the_type "0" = SOME "nat"
@@ -911,7 +987,7 @@
trns
|> debug 5 (fn _ => "trying defgen datatype constructor for " ^ quote c)
|> ensure_def_tyco thy defs (idf_of_tname thy dtname)
- ||>> fold_map (invoke_cg_type thy defs) tyargs
+ ||>> fold_map (invoke_cg_type thy defs o devarify_type) tyargs
|-> (fn (dtname, tys) => succeed (Datatypecons (dtname, tys), []))
| NONE =>
trns
@@ -924,6 +1000,42 @@
|> fail ("not a constant: " ^ quote f)
end;
+fun defgen_datatype_eq get_datatype thy defs f trns =
+ case name_of_idf thy nsp_eq f
+ of SOME dtname =>
+ (case get_datatype thy dtname
+ of SOME (_, cnames) =>
+ trns
+ |> debug 5 (fn _ => "trying defgen datatype_eq for " ^ quote dtname)
+ |> ensure_def_tyco thy defs (idf_of_tname thy dtname)
+ ||>> fold_map (ensure_def_const thy defs) (cnames
+ |> map (idf_of_name thy nsp_const)
+ |> map (fn "0" => "const.Zero" | c => c))
+ ||>> `(fn (_, modl) => build_eqpred modl dtname)
+ |-> (fn (_, eqpred) => succeed (eqpred, []))
+ | NONE =>
+ trns
+ |> fail ("no datatype found for " ^ quote dtname))
+ | NONE =>
+ trns
+ |> fail ("not an equality predicate: " ^ quote f)
+
+fun defgen_datatype_eqinst get_datatype thy defs f trns =
+ case name_of_idf thy nsp_eq_class f
+ of SOME dtname =>
+ (case get_datatype thy dtname
+ of SOME (vs, _) =>
+ trns
+ |> debug 5 (fn _ => "trying defgen datatype_eqinst for " ^ quote dtname)
+ |> ensure_def_const thy defs (idf_of_name thy nsp_eq dtname)
+ |-> (fn pred_eq => succeed (Classinst (class_eq, (dtname, vs ~~ replicate (length vs) [class_eq]), [(fun_eq, pred_eq)]), []))
+ | NONE =>
+ trns
+ |> fail ("no datatype found for " ^ quote dtname))
+ | NONE =>
+ trns
+ |> fail ("not an equality instance: " ^ quote f)
+
fun defgen_recfun get_equations thy defs f trns =
case cname_of_idf thy defs f
of SOME (f, ty) =>
@@ -934,7 +1046,7 @@
of (_::_) =>
trns
|> debug 5 (fn _ => "trying defgen recfun for " ^ quote f)
- |> mk_fun thy defs eqs ty
+ |> mk_fun thy defs eqs (devarify_type ty)
|-> (fn def => succeed (def, []))
| _ =>
trns
@@ -1033,6 +1145,11 @@
|> fold add_def (Codegen.mk_deftab thy |> Symtab.dest)
end;
+fun check_for_serializer serial_name serialize_data =
+ if Symtab.defined serialize_data serial_name
+ then serialize_data
+ else error ("unknown code serializer: " ^ quote serial_name);
+
fun expand_module defs gen thy =
let
fun put_module modl =
@@ -1063,7 +1180,7 @@
|-> (fn mfx => map_codegen_data
(fn (modl, gens, lookups, serialize_data, logic_data) =>
(modl, gens, lookups,
- serialize_data |> Symtab.map_entry serial_name
+ serialize_data |> check_for_serializer serial_name |> Symtab.map_entry serial_name
(map_serialize_data
(fn (primitives, syntax_tyco, syntax_const) =>
(primitives |> add_primdef primdef,
@@ -1088,7 +1205,7 @@
let
val proto_mfx = Codegen.parse_mixfix
(typ_of o read_ctyp thy) mfx;
- fun generate thy defs = fold_map (invoke_cg_type thy defs)
+ fun generate thy defs = fold_map (invoke_cg_type thy defs o devarify_type)
(Codegen.quotes_of proto_mfx);
in
thy
@@ -1115,7 +1232,7 @@
|-> (fn mfx => map_codegen_data
(fn (modl, gens, lookups, serialize_data, logic_data) =>
(modl, gens, lookups,
- serialize_data |> Symtab.map_entry serial_name
+ serialize_data |> check_for_serializer serial_name |> Symtab.map_entry serial_name
(map_serialize_data
(fn (primitives, syntax_tyco, syntax_const) =>
(primitives |> add_primdef primdef,
@@ -1149,7 +1266,7 @@
let
val proto_mfx = Codegen.parse_mixfix
(term_of o read_cterm thy o rpair TypeInfer.logicT) mfx;
- fun generate thy defs = fold_map (invoke_cg_expr thy defs)
+ fun generate thy defs = fold_map (invoke_cg_expr thy defs o devarify_term)
(Codegen.quotes_of proto_mfx);
in
thy
@@ -1198,6 +1315,7 @@
thy
|> CodegenData.get
|> #serialize_data
+ |> check_for_serializer serial_name
|> (fn data => (the oo Symtab.lookup) data serial_name)
val serializer' = (get_serializer thy serial_name)
((mk_sfun o #syntax_tyco) serialize_data)
@@ -1227,8 +1345,18 @@
in
-val (generateK, serializeK, extractingK, aliasK, definedK, dependingK, syntax_tycoK, syntax_constK) =
- ("code_generate", "code_serialize", "extracting", "defined_by", "depending_on", "code_alias", "code_syntax_tyco", "code_syntax_const");
+val (classK, generateK, serializeK, syntax_tycoK, syntax_constK, aliasK) =
+ ("code_class", "code_generate", "code_serialize", "code_syntax_tyco", "code_syntax_const", "code_alias");
+val (extractingK, definedK, dependingK) =
+ ("extracting", "defined_by", "depending_on");
+
+val classP =
+ OuterSyntax.command classK "codegen data for classes" K.thy_decl (
+ P.xname
+ -- ((P.$$$ "\\<Rightarrow>" || P.$$$ "=>") |-- (P.list1 P.name))
+ -- (Scan.optional ((P.$$$ "\\<Rightarrow>" || P.$$$ "=>") |-- (P.list1 P.name)) [])
+ >> (fn ((name, tycos), consts) => (Toplevel.theory (ClassPackage.add_classentry name consts tycos)))
+ )
val generateP =
OuterSyntax.command generateK "generate executable code for constants" K.thy_decl (
@@ -1258,13 +1386,13 @@
val syntax_tycoP =
OuterSyntax.command syntax_tycoK "define code syntax for type constructor" K.thy_decl (
- P.string
+ P.name
-- Scan.repeat1 (
P.xname -- (P.$$$ "(" |-- P.string --| P.$$$ ")")
-- Scan.option (
P.$$$ definedK
|-- Scan.option (P.$$$ "(" |-- P.string --| P.$$$ ")")
- -- (P.string -- Scan.optional (P.$$$ dependingK |-- P.list1 P.string) [])
+ -- (P.text -- Scan.optional (P.$$$ dependingK |-- P.list1 P.string) [])
)
)
>> (fn (serial_name, xs) =>
@@ -1275,13 +1403,13 @@
val syntax_constP =
OuterSyntax.command syntax_constK "define code syntax for constant" K.thy_decl (
- P.string
+ P.name
-- Scan.repeat1 (
(P.xname -- Scan.option (P.$$$ "::" |-- P.typ)) -- (P.$$$ "(" |-- P.string --| P.$$$ ")")
-- Scan.option (
P.$$$ definedK
|-- Scan.option (P.$$$ "(" |-- P.string --| P.$$$ ")")
- -- (P.string -- Scan.optional (P.$$$ dependingK |-- P.list1 P.string) [])
+ -- (P.text -- Scan.optional (P.$$$ dependingK |-- P.list1 P.string) [])
)
)
>> (fn (serial_name, xs) =>
@@ -1290,8 +1418,8 @@
add_syntax_const serial_name ((f, raw_mfx), raw_def)) xs)
);
-val _ = OuterSyntax.add_parsers [generateP, serializeP, aliasP, syntax_tycoP, syntax_constP];
-val _ = OuterSyntax.add_keywords [extractingK, definedK, dependingK];
+val _ = OuterSyntax.add_parsers [classP, generateP, serializeP, aliasP, syntax_tycoP, syntax_constP];
+val _ = OuterSyntax.add_keywords ["\\<Rightarrow>", "=>", extractingK, definedK, dependingK];
(* setup *)
@@ -1309,8 +1437,9 @@
add_codegen_sort ("default", exprgen_sort_default),
add_codegen_type ("default", exprgen_type_default),
add_codegen_expr ("default", exprgen_term_default),
+ add_appgen ("default", appgen_default),
(* add_codegen_expr ("eq", codegen_eq), *)
- add_codegen_expr ("neg", codegen_neg),
+ add_appgen ("neg", appgen_neg),
add_defgen ("clsdecl", defgen_clsdecl),
add_defgen ("tyco_fallback", defgen_tyco_fallback),
add_defgen ("const_fallback", defgen_const_fallback),
--- a/src/Pure/Tools/codegen_serializer.ML Fri Dec 02 16:05:12 2005 +0100
+++ b/src/Pure/Tools/codegen_serializer.ML Fri Dec 02 16:05:31 2005 +0100
@@ -13,7 +13,6 @@
val add_prim: string * (string * string list) -> primitives -> primitives;
val merge_prims: primitives * primitives -> primitives;
val has_prim: primitives -> string -> bool;
- val mk_prims: primitives -> string;
type 'a pretty_syntax = string
-> (int * (Pretty.T list -> ('a -> Pretty.T) -> Pretty.T)) option;
@@ -127,12 +126,16 @@
| postify (ps as _::_) f = [Pretty.list "(" ")" ps, Pretty.brk 1, f];
fun upper_first s =
- let val (c :: cs) = String.explode s
- in String.implode (Char.toUpper c :: cs) end;
+ let
+ val (pr, b) = split_last (NameSpace.unpack s);
+ val (c::cs) = String.explode b;
+ in NameSpace.pack (pr @ [String.implode (Char.toUpper c :: cs)]) end;
fun lower_first s =
- let val (c :: cs) = String.explode s
- in String.implode (Char.toLower c :: cs) end;
+ let
+ val (pr, b) = split_last (NameSpace.unpack s);
+ val (c::cs) = String.explode b;
+ in NameSpace.pack (pr @ [String.implode (Char.toLower c :: cs)]) end;
(** grouping functions **)
@@ -289,10 +292,18 @@
|> brackify (eval_br br (INFX (5, R)))
end
| ml_from_pat br (ICons ((f, ps), ty)) =
- ps
- |> map (ml_from_pat BR)
- |> cons ((Pretty.str o resolv) f)
- |> brackify (eval_br br BR)
+ (case const_syntax f
+ of NONE =>
+ ps
+ |> map (ml_from_pat BR)
+ |> cons ((Pretty.str o resolv) f)
+ |> brackify (eval_br br BR)
+ | SOME (i, pr) =>
+ if i = length ps
+ then
+ pr (map (ml_from_pat BR) ps) (ml_from_expr BR)
+ else
+ error "number of argument mismatch in customary serialization")
| ml_from_pat br (IVarP (v, IType ("Integer", []))) =
brackify (eval_br br BR) [
Pretty.str v,
@@ -300,8 +311,8 @@
Pretty.str "IntInf.int"
]
| ml_from_pat br (IVarP (v, _)) =
- Pretty.str v;
- fun ml_from_expr br (e as (IApp (IConst ("Cons", _), _))) =
+ Pretty.str v
+ and ml_from_expr br (e as (IApp (IConst ("Cons", _), _))) =
let
fun dest_cons (IApp (IConst ("Cons", _),
IApp (IApp (IConst ("Pair", _), e1), e2))) = SOME (e1, e2)
@@ -396,7 +407,9 @@
brackify (eval_br br (INFX (4, L))) [
ml_from_expr (INFX (4, L)) e1,
Pretty.str "=",
- ml_from_expr (INFX (4, X)) e2
+ ml_from_expr (INFX (4, X)) e2,
+ Pretty.str ":",
+ ml_from_type NOBR (itype_of_iexpr e2)
]
| ml_from_app br ("Pair", [e1, e2]) =
Pretty.list "(" ")" [
@@ -452,14 +465,15 @@
mk_app_p br (Pretty.str "~") es
| ml_from_app br ("wfrec", es) =
mk_app_p br (Pretty.str "wfrec") es
- | ml_from_app br (f, []) =
- Pretty.str (resolv f)
| ml_from_app br (f, es) =
case const_syntax f
of NONE =>
- let
- val (es', e) = split_last es;
- in mk_app_p br (ml_from_app NOBR (f, es')) [e] end
+ (case es
+ of [] => Pretty.str (resolv f)
+ | es =>
+ let
+ val (es', e) = split_last es;
+ in mk_app_p br (ml_from_app NOBR (f, es')) [e] end)
| SOME (i, pr) =>
let
val (es1, es2) = splitAt (i, es);
@@ -552,7 +566,7 @@
error ("can't serialize class declaration " ^ quote name ^ " to ML")
| ml_from_def (name, Classinst _) =
error ("can't serialize instance declaration " ^ quote name ^ " to ML")
- in (writeln "******************"; (*map (writeln o Pretty.o)*)
+ in (debug 10 (fn _ => "******************") (); (*map (writeln o Pretty.o)*)
case (snd o hd) ds
of Fun _ => ml_from_funs ds
| Datatypecons _ => ml_from_datatypes ds
@@ -630,6 +644,7 @@
|> eliminate_classes
|> debug 3 (fn _ => "generating...")
|> serialize (ml_from_defs tyco_syntax const_syntax) ml_from_module ml_validator nspgrp name_root
+ |> (fn p => Pretty.chunks [(Pretty.str o mk_prims) prims, p])
end;
fun ml_from_thingol' nspgrp name_root =
@@ -660,9 +675,13 @@
NameSpace.pack (map upper_first prfix @ [base])
end;
fun resolv_const f =
- if is_cons f
- then (upper_first o resolv) f
- else (lower_first o resolv) f
+ if NameSpace.is_qualified f
+ then
+ if is_cons f
+ then (upper_first o resolv) f
+ else (lower_first o resolv) f
+ else
+ f;
fun haskell_from_sctxt vs =
let
fun from_sctxt [] = Pretty.str ""
@@ -755,13 +774,21 @@
|> brackify (eval_br br (INFX (5, R)))
end
| haskell_from_pat br (ICons ((f, ps), _)) =
- ps
- |> map (haskell_from_pat BR)
- |> cons ((Pretty.str o upper_first o resolv) f)
- |> brackify (eval_br br BR)
+ (case const_syntax f
+ of NONE =>
+ ps
+ |> map (haskell_from_pat BR)
+ |> cons ((Pretty.str o resolv_const) f)
+ |> brackify (eval_br br BR)
+ | SOME (i, pr) =>
+ if i = length ps
+ then
+ pr (map (haskell_from_pat BR) ps) (haskell_from_expr BR)
+ else
+ error "number of argument mismatch in customary serialization")
| haskell_from_pat br (IVarP (v, _)) =
- (Pretty.str o lower_first) v;
- fun haskell_from_expr br (e as (IApp (IApp (IConst ("Cons", _), _), _))) =
+ (Pretty.str o lower_first) v
+ and haskell_from_expr br (e as (IApp (IApp (IConst ("Cons", _), _), _))) =
let
fun dest_cons (IApp (IApp (IConst ("Cons", _), e1), e2)) = SOME (e1, e2)
| dest_cons p = NONE
@@ -846,23 +873,17 @@
Pretty.str "==",
haskell_from_expr (INFX (4, X)) e2
]
+ | haskell_from_app br ("eq", [e1, e2]) =
+ brackify (eval_br br (INFX (4, L))) [
+ haskell_from_expr (INFX (4, L)) e1,
+ Pretty.str "==",
+ haskell_from_expr (INFX (4, X)) e2
+ ]
| haskell_from_app br ("Pair", [e1, e2]) =
Pretty.list "(" ")" [
haskell_from_expr NOBR e1,
haskell_from_expr NOBR e2
]
- | haskell_from_app br ("and", [e1, e2]) =
- brackify (eval_br br (INFX (3, R))) [
- haskell_from_expr (INFX (3, X)) e1,
- Pretty.str "&&",
- haskell_from_expr (INFX (3, R)) e2
- ]
- | haskell_from_app br ("or", [e1, e2]) =
- brackify (eval_br br (INFX (2, L))) [
- haskell_from_expr (INFX (2, L)) e1,
- Pretty.str "||",
- haskell_from_expr (INFX (2, X)) e2
- ]
| haskell_from_app br ("if", [b, e1, e2]) =
brackify (eval_br br BR) [
Pretty.str "if",
@@ -872,46 +893,49 @@
Pretty.str "else",
haskell_from_expr NOBR e2
]
- | haskell_from_app br ("add", [e1, e2]) =
- brackify (eval_br br (INFX (6, L))) [
- haskell_from_expr (INFX (6, L)) e1,
- Pretty.str "+",
- haskell_from_expr (INFX (6, X)) e2
- ]
- | haskell_from_app br ("mult", [e1, e2]) =
- brackify (eval_br br (INFX (7, L))) [
- haskell_from_expr (INFX (7, L)) e1,
- Pretty.str "*",
- haskell_from_expr (INFX (7, X)) e2
- ]
- | haskell_from_app br ("lt", [e1, e2]) =
- brackify (eval_br br (INFX (4, L))) [
- haskell_from_expr (INFX (4, L)) e1,
- Pretty.str "<",
- haskell_from_expr (INFX (4, X)) e2
- ]
- | haskell_from_app br ("le", [e1, e2]) =
- brackify (eval_br br (INFX (7, L))) [
- haskell_from_expr (INFX (4, L)) e1,
- Pretty.str "<=",
- haskell_from_expr (INFX (4, X)) e2
- ]
+ | haskell_from_app br ("and", es) =
+ haskell_from_binop br 3 R "&&" es
+ | haskell_from_app br ("or", es) =
+ haskell_from_binop br 2 R "||" es
+ | haskell_from_app br ("add", es) =
+ haskell_from_binop br 6 L "+" es
+ | haskell_from_app br ("mult", es) =
+ haskell_from_binop br 7 L "*" es
+ | haskell_from_app br ("lt", es) =
+ haskell_from_binop br 4 L "<" es
+ | haskell_from_app br ("le", es) =
+ haskell_from_binop br 4 L "<=" es
| haskell_from_app br ("minus", es) =
mk_app_p br (Pretty.str "negate") es
| haskell_from_app br ("wfrec", es) =
mk_app_p br (Pretty.str "wfrec") es
- | haskell_from_app br (f, []) =
- Pretty.str (resolv_const f)
| haskell_from_app br (f, es) =
case const_syntax f
of NONE =>
- let
- val (es', e) = split_last es;
- in mk_app_p br (haskell_from_app NOBR (f, es')) [e] end
+ (case es
+ of [] => Pretty.str (resolv_const f)
+ | es =>
+ let
+ val (es', e) = split_last es;
+ in mk_app_p br (haskell_from_app NOBR (f, es')) [e] end)
| SOME (i, pr) =>
let
val (es1, es2) = splitAt (i, es);
- in mk_app_p br (pr (map (haskell_from_expr BR) es1) (haskell_from_expr BR)) es2 end;
+ in mk_app_p br (pr (map (haskell_from_expr BR) es1) (haskell_from_expr BR)) es2 end
+ and haskell_from_binop br pr L f [e1, e2] =
+ brackify (eval_br br (INFX (pr, L))) [
+ haskell_from_expr (INFX (pr, L)) e1,
+ Pretty.str f,
+ haskell_from_expr (INFX (pr, X)) e2
+ ]
+ | haskell_from_binop br pr R f [e1, e2] =
+ brackify (eval_br br (INFX (pr, R))) [
+ haskell_from_expr (INFX (pr, X)) e1,
+ Pretty.str f,
+ haskell_from_expr (INFX (pr, R)) e2
+ ]
+ | haskell_from_binop br pr ass f args =
+ mk_app_p br (Pretty.str ("(" ^ f ^ ")")) args
fun haskell_from_datatypes defs =
let
fun mk_cons (co, typs) =
@@ -1050,6 +1074,7 @@
|> eta_expand eta_expander
|> debug 3 (fn _ => "generating...")
|> serialize (haskell_from_defs tyco_syntax const_syntax is_cons) haskell_from_module haskell_validator nspgrp name_root
+ |> (fn p => Pretty.chunks [(Pretty.str o mk_prims) prims, p])
end;
end; (* local *)
--- a/src/Pure/Tools/codegen_thingol.ML Fri Dec 02 16:05:12 2005 +0100
+++ b/src/Pure/Tools/codegen_thingol.ML Fri Dec 02 16:05:31 2005 +0100
@@ -1,4 +1,4 @@
-(* Title: Pure/Tools/codegen_thingol.ML
+ (* Title: Pure/Tools/codegen_thingol.ML
ID: $Id$
Author: Florian Haftmann, TU Muenchen
@@ -48,7 +48,7 @@
Nop
| Fun of (ipat list * iexpr) list * (ClassPackage.sortcontext * itype)
| Typesyn of (vname * string list) list * itype
- | Datatype of (vname * string list) list * string list * class list
+ | Datatype of (vname * string list) list * string list * string list
| Datatypecons of string * itype list
| Class of class list * vname * string list * string list
| Classmember of class * vname * itype
@@ -78,6 +78,7 @@
val type_list: string;
val type_integer: string;
val cons_pair: string;
+ val fun_eq: string;
val fun_fst: string;
val fun_snd: string;
val Type_integer: itype;
@@ -103,7 +104,9 @@
val Fun_wfrec: iexpr;
val prims: string list;
+ val get_eqpred: module -> string -> string option;
val is_eqtype: module -> itype -> bool;
+ val build_eqpred: module -> string -> def;
val extract_defs: iexpr -> string list;
val eta_expand: (string -> int) -> module -> module;
val eta_expand_poly: module -> module;
@@ -484,13 +487,13 @@
Pretty.str " |=> ",
pretty_itype ty
]
- | pretty_def (Datatype (vs, cs, clss)) =
+ | pretty_def (Datatype (vs, cs, insts)) =
Pretty.block [
Pretty.list "(" ")" (map (pretty_itype o IVarT) vs),
Pretty.str " |=> ",
Pretty.gen_list " |" "" "" (map Pretty.str cs),
- Pretty.str ", instance of ",
- Pretty.gen_list "," "[" "]" (map Pretty.str clss)
+ Pretty.str ", instances ",
+ Pretty.gen_list "," "[" "]" (map Pretty.str insts)
]
| pretty_def (Datatypecons (dtname, tys)) =
Pretty.block [
@@ -655,25 +658,25 @@
in Graph.join (K join_module) modl12 end;
fun partof names modl =
- let
- datatype pathnode = PN of (string list * (string * pathnode) list);
- fun mk_ipath ([], base) (PN (defs, modls)) =
- PN (base :: defs, modls)
- | mk_ipath (n::ns, base) (PN (defs, modls)) =
- modls
- |> AList.default (op =) (n, PN ([], []))
- |> AList.map_entry (op =) n (mk_ipath (ns, base))
- |> (pair defs #> PN);
- fun select (PN (defs, modls)) (Module module) =
- module
- |> Graph.subgraph (Graph.all_succs module (defs @ map fst modls))
- |> fold (fn (name, modls) => Graph.map_node name (select modls)) modls
- |> Module;
- in
- Module modl
- |> select (fold (mk_ipath o dest_name) (filter NameSpace.is_qualified names) (PN ([], [])))
- |> dest_modl
- end;
+ let
+ datatype pathnode = PN of (string list * (string * pathnode) list);
+ fun mk_ipath ([], base) (PN (defs, modls)) =
+ PN (base :: defs, modls)
+ | mk_ipath (n::ns, base) (PN (defs, modls)) =
+ modls
+ |> AList.default (op =) (n, PN ([], []))
+ |> AList.map_entry (op =) n (mk_ipath (ns, base))
+ |> (pair defs #> PN);
+ fun select (PN (defs, modls)) (Module module) =
+ module
+ |> Graph.subgraph (Graph.all_succs module (defs @ map fst modls))
+ |> fold (fn (name, modls) => Graph.map_node name (select modls)) modls
+ |> Module;
+ in
+ Module modl
+ |> select (fold (mk_ipath o dest_name) (filter NameSpace.is_qualified names) (PN ([], [])))
+ |> dest_modl
+ end;
fun add_check_transform (name, (Datatypecons (dtname, _))) =
(debug 7 (fn _ => "transformation for datatype constructor " ^ quote name
@@ -682,7 +685,7 @@
fn [Datatype (_, _, [])] => NONE
| _ => "attempted to add constructor to already instantiating datatype" |> SOME)],
[(dtname,
- fn Datatype (vs, cs, clss) => Datatype (vs, name::cs, clss)
+ fn Datatype (vs, cs, insts) => Datatype (vs, name::cs, insts)
| def => "attempted to add datatype constructor to non-datatype: "
^ (Pretty.output o pretty_def) def |> error)])
)
@@ -734,7 +737,7 @@
| def => "attempted to add class instance to non-class"
^ (Pretty.output o pretty_def) def |> error),
(tyco,
- fn Datatype (vs, cs, clss) => Datatype (vs, cs, clsname::clss)
+ fn Datatype (vs, cs, insts) => Datatype (vs, cs, name::insts)
| Nop => Nop
| def => "attempted to instantiate non-type to class instance"
^ (Pretty.output o pretty_def) def |> error)])
@@ -945,32 +948,68 @@
cons_true, cons_false, cons_pair, cons_nil, cons_cons, fun_primeq, fun_eq, fun_not, fun_and,
fun_or, fun_if, fun_fst, fun_snd, fun_add, fun_mult, fun_minus, fun_lt, fun_le, fun_wfrec];
-fun is_superclass_of modl class_sub class_sup =
- if class_sub = class_sup
- then true
- else
- if NameSpace.is_qualified class_sub
- then
- case get_def modl class_sub
- of Class (supclsnames, _, _, _)
- => exists (fn class => is_superclass_of modl class class_sup) supclsnames
- else
- false;
+
+(** equality handling **)
+
+fun get_eqpred modl tyco =
+ if NameSpace.is_qualified tyco
+ then
+ case get_def modl tyco
+ of Datatype (_, _, insts) =>
+ get_first (fn inst =>
+ case get_def modl inst
+ of Classinst (cls, _, memdefs) =>
+ if cls = class_eq
+ then (SOME o snd o hd) memdefs
+ else NONE) insts
+ else SOME fun_primeq;
fun is_eqtype modl (IType (tyco, tys)) =
forall (is_eqtype modl) tys
- andalso
- if NameSpace.is_qualified tyco
- then
+ andalso (
+ NameSpace.is_qualified tyco
+ orelse
case get_def modl tyco
of Typesyn (vs, ty) => is_eqtype modl ty
- | Datatype (_, _, classes) => exists (is_superclass_of modl class_eq) classes
- else
- true
+ | Datatype (_, _, insts) =>
+ exists (fn inst => case get_def modl inst of Classinst (cls, _, _) => cls = class_eq) insts
+ )
| is_eqtype modl (IFun _) =
false
| is_eqtype modl (IVarT (_, sort)) =
- exists (is_superclass_of modl class_eq) sort
+ member (op =) sort class_eq;
+
+fun build_eqpred modl dtname =
+ let
+ val cons =
+ map ((fn Datatypecons c => c) o get_def modl)
+ (case get_def modl dtname of Datatype (_, cs, _) => cs);
+ val sortctxt =
+ map (rpair [class_eq])
+ (case get_def modl dtname of Datatype (_, vs, _) => vs);
+ val ty = IType (dtname, map IVarT sortctxt);
+ fun mk_eq (c, []) =
+ ([ICons ((c, []), ty), ICons ((c, []), ty)], Cons_true)
+ | mk_eq (c, tys) =
+ let
+ val vars1 = Term.invent_names [] "a" (length tys);
+ val vars2 = Term.invent_names vars1 "b" (length tys);
+ fun mk_eq_cons ty' (v1, v2) =
+ IConst (fun_eq, ty' `-> ty' `-> Type_bool) `$ IVarE (v1, ty) `$ IVarE (v2, ty)
+ fun mk_conj (e1, e2) =
+ Fun_and `$ e1 `$ e2;
+ in
+ ([ICons ((c, map2 (curry IVarP) vars1 tys), ty),
+ ICons ((c, map2 (curry IVarP) vars2 tys), ty)],
+ foldr1 mk_conj (map2 mk_eq_cons tys (vars1 ~~ vars2)))
+ end;
+ val eqs = map mk_eq cons @ [([IVarP ("_", ty), IVarP ("_", ty)], Cons_false)];
+ in
+ Fun (eqs, (sortctxt, ty `-> ty `-> Type_bool))
+ end;
+
+
+(** generic transformation **)
fun extract_defs e =
let
@@ -988,10 +1027,6 @@
fold_iexpr extr_itype extr_ipat extr_iexpr e
in extr_iexpr e [] end;
-
-
-(** generic transformation **)
-
fun eta_expand query =
let
fun eta_app ((f, ty), es) =