--- a/src/Pure/Tools/class_package.ML Wed Nov 30 17:56:08 2005 +0100
+++ b/src/Pure/Tools/class_package.ML Wed Nov 30 18:13:31 2005 +0100
@@ -17,7 +17,7 @@
val is_class: theory -> class -> bool
val get_arities: theory -> sort -> string -> sort list
val get_superclasses: theory -> class -> class list
- val get_const_sign: theory -> string -> string * typ
+ val get_const_sign: theory -> string -> string -> typ
val get_inst_consts_sign: theory -> string * class -> (string * typ) list
val lookup_const_class: theory -> string -> class option
val get_classtab: theory -> (string list * (string * string) list) Symtab.table
@@ -162,32 +162,33 @@
(* instance queries *)
-fun get_const_sign thy const =
+fun get_const_sign thy tvar const =
let
val class = (the o lookup_const_class thy) const;
val ty = (Type.unvarifyT o Sign.the_const_constraint thy) const;
- val tvar = fold_atyps
- (fn TFree (tvar, sort) =>
- if Sorts.sort_eq (Sign.classes_of thy) ([class], sort) then K (SOME tvar) else I | _ => I) ty NONE
- |> the;
- val ty' = map_type_tfree (fn (tvar', sort) =>
- if tvar' = tvar
- then TFree (tvar, [])
- else TFree (tvar', sort)
- ) ty;
- in (tvar, ty') end;
+ val tvars_used = Term.add_tfreesT ty [];
+ val tvar_rename = hd (Term.invent_names (map fst tvars_used) tvar 1);
+ in
+ ty
+ |> map_type_tfree (fn (tvar', sort) =>
+ if Sorts.sort_eq (Sign.classes_of thy) ([class], sort)
+ then TFree (tvar, [])
+ else if tvar' = tvar
+ then TFree (tvar_rename, sort)
+ else TFree (tvar', sort))
+ end;
fun get_inst_consts_sign thy (tyco, class) =
let
val consts = the_consts thy class;
val arities = get_arities thy [class] tyco;
- val const_signs = map (get_const_sign thy) consts;
- val vars_used = fold (fn (tvar, ty) => curry (gen_union (op =))
- (map fst (typ_tfrees ty) |> remove (op =) tvar)) const_signs [];
+ val const_signs = map (get_const_sign thy "'a") consts;
+ val vars_used = fold (fn ty => curry (gen_union (op =))
+ (map fst (typ_tfrees ty) |> remove (op =) "'a")) const_signs [];
val vars_new = Term.invent_names vars_used "'a" (length arities);
val typ_arity = Type (tyco, map2 TFree (vars_new, arities));
val instmem_signs =
- map (fn (tvar, ty) => typ_subst_atomic [(TFree (tvar, []), typ_arity)] ty) const_signs;
+ map (typ_subst_atomic [(TFree ("'a", []), typ_arity)]) const_signs;
in consts ~~ instmem_signs end;
fun get_classtab thy =
--- a/src/Pure/Tools/codegen_package.ML Wed Nov 30 17:56:08 2005 +0100
+++ b/src/Pure/Tools/codegen_package.ML Wed Nov 30 18:13:31 2005 +0100
@@ -12,11 +12,11 @@
signature CODEGEN_PACKAGE =
sig
type deftab;
- type codegen_type;
- type codegen_expr;
+ type exprgen_type;
+ type exprgen_term;
type defgen;
- val add_codegen_type: string * codegen_type -> theory -> theory;
- val add_codegen_expr: string * codegen_expr -> theory -> theory;
+ val add_codegen_type: string * exprgen_type -> theory -> theory;
+ val add_codegen_expr: string * exprgen_term -> 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;
@@ -54,13 +54,13 @@
-> string -> CodegenThingol.transact -> string * CodegenThingol.transact;
val codegen_let: (int -> term -> term list * term)
- -> codegen_expr;
+ -> exprgen_term;
val codegen_split: (int -> term -> term list * term)
- -> codegen_expr;
+ -> exprgen_term;
val codegen_number_of: (term -> IntInf.int) -> (term -> term)
- -> codegen_expr;
+ -> exprgen_term;
val codegen_case: (theory -> string -> (string * int) list option)
- -> codegen_expr;
+ -> exprgen_term;
val defgen_datatype: (theory -> string -> (string list * string list) option)
-> defgen;
val defgen_datacons: (theory -> string * string -> typ list option)
@@ -98,9 +98,9 @@
* (string * string) Symtab.table
* class Symtab.table);
-type codegen_sort = theory -> deftab -> (sort, sort) gen_codegen;
-type codegen_type = theory -> deftab -> (typ, itype) gen_codegen;
-type codegen_expr = theory -> deftab -> (term, iexpr) gen_codegen;
+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 defgen = theory -> deftab -> gen_defgen;
@@ -129,7 +129,7 @@
let
val name_root = "Generated";
val nsp_conn = [
- [nsp_class, nsp_eq_class], [nsp_type], [nsp_const], [nsp_inst], [nsp_mem], [nsp_eq]
+ [nsp_class, nsp_eq_class], [nsp_type], [nsp_const, nsp_eq], [nsp_inst], [nsp_mem]
];
in CodegenSerializer.haskell_from_thingol nsp_conn name_root end;
@@ -137,33 +137,33 @@
(* theory data for codegen *)
type gens = {
- codegens_sort: (string * (codegen_sort * stamp)) list,
- codegens_type: (string * (codegen_type * stamp)) list,
- codegens_expr: (string * (codegen_expr * stamp)) list,
+ exprgens_sort: (string * (exprgen_sort * stamp)) list,
+ exprgens_type: (string * (exprgen_type * stamp)) list,
+ exprgens_term: (string * (exprgen_term * stamp)) list,
defgens: (string * (defgen * stamp)) list
};
val empty_gens = {
- codegens_sort = Symtab.empty, codegens_type = Symtab.empty,
- codegens_expr = Symtab.empty, defgens = Symtab.empty
+ exprgens_sort = Symtab.empty, exprgens_type = Symtab.empty,
+ exprgens_term = Symtab.empty, defgens = Symtab.empty
};
-fun map_gens f { codegens_sort, codegens_type, codegens_expr, defgens } =
+fun map_gens f { exprgens_sort, exprgens_type, exprgens_term, defgens } =
let
- val (codegens_sort, codegens_type, codegens_expr, defgens) =
- f (codegens_sort, codegens_type, codegens_expr, defgens)
- in { codegens_sort = codegens_sort, codegens_type = codegens_type,
- codegens_expr = codegens_expr, defgens = defgens } end;
+ val (exprgens_sort, exprgens_type, exprgens_term, defgens) =
+ f (exprgens_sort, exprgens_type, exprgens_term, defgens)
+ in { exprgens_sort = exprgens_sort, exprgens_type = exprgens_type,
+ exprgens_term = exprgens_term, defgens = defgens } end;
fun merge_gens
- ({ codegens_sort = codegens_sort1, codegens_type = codegens_type1,
- codegens_expr = codegens_expr1, defgens = defgens1 },
- { codegens_sort = codegens_sort2, codegens_type = codegens_type2,
- codegens_expr = codegens_expr2, defgens = defgens2 }) =
- { codegens_sort = AList.merge (op =) (eq_snd (op =)) (codegens_sort1, codegens_sort2),
- codegens_type = AList.merge (op =) (eq_snd (op =)) (codegens_type1, codegens_type2),
- codegens_expr = AList.merge (op =) (eq_snd (op =)) (codegens_expr1, codegens_expr2),
- defgens = AList.merge (op =) (eq_snd (op =)) (defgens1, defgens2) };
+ ({ exprgens_sort = exprgens_sort1, exprgens_type = exprgens_type1,
+ exprgens_term = exprgens_term1, defgens = defgens1 },
+ { exprgens_sort = exprgens_sort2, exprgens_type = exprgens_type2,
+ exprgens_term = exprgens_term2, 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),
+ defgens = AList.merge (op =) (eq_snd (op =)) (defgens1, defgens2) } : gens;
type lookups = {
lookups_tyco: string Symtab.table,
@@ -184,7 +184,7 @@
({ lookups_tyco = lookups_tyco1, lookups_const = lookups_const1 },
{ lookups_tyco = lookups_tyco2, lookups_const = lookups_const2 }) =
{ lookups_tyco = Symtab.merge (op =) (lookups_tyco1, lookups_tyco2),
- lookups_const = Symtab.merge (op =) (lookups_const1, lookups_const2) };
+ lookups_const = Symtab.merge (op =) (lookups_const1, lookups_const2) } : lookups;
type logic_data = {
is_datatype: ((theory -> string -> bool) * stamp) option,
@@ -208,7 +208,7 @@
in
{ is_datatype = merge_opt (eq_snd (op =)) (is_datatype1, is_datatype2),
alias = (Symtab.merge (op =) (fst alias1, fst alias2),
- Symtab.merge (op =) (snd alias1, snd alias2)) }
+ Symtab.merge (op =) (snd alias1, snd alias2)) } : logic_data
end;
type serialize_data = {
@@ -233,7 +233,7 @@
{ serializer = serializer,
primitives = CodegenSerializer.merge_prims (primitives1, primitives2) : CodegenSerializer.primitives,
syntax_tyco = Symtab.merge (op =) (syntax_tyco1, syntax_tyco2),
- syntax_const = Symtab.merge (op =) (syntax_const1, syntax_const2) };
+ syntax_const = Symtab.merge (op =) (syntax_const1, syntax_const2) } : serialize_data;
structure CodegenData = TheoryDataFun
(struct
@@ -247,7 +247,7 @@
};
val empty = {
modl = empty_module,
- gens = { codegens_sort = [], codegens_type = [], codegens_expr = [], defgens = [] } : gens,
+ gens = { exprgens_sort = [], exprgens_type = [], exprgens_term = [], 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 =
@@ -297,30 +297,30 @@
(fn (modl, gens, lookups, serialize_data, logic_data) =>
(modl,
gens |> map_gens
- (fn (codegens_sort, codegens_type, codegens_expr, defgens) =>
- (codegens_sort
+ (fn (exprgens_sort, exprgens_type, exprgens_term, defgens) =>
+ (exprgens_sort
|> Output.update_warn (op =) ("overwriting existing class code generator " ^ name) (name, (cg, stamp ())),
- codegens_type, codegens_expr, defgens)), lookups, serialize_data, logic_data));
+ exprgens_type, exprgens_term, 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 (codegens_sort, codegens_type, codegens_expr, defgens) =>
- (codegens_sort,
- codegens_type
+ (fn (exprgens_sort, exprgens_type, exprgens_term, defgens) =>
+ (exprgens_sort,
+ exprgens_type
|> Output.update_warn (op =) ("overwriting existing type code generator " ^ name) (name, (cg, stamp ())),
- codegens_expr, defgens)), lookups, serialize_data, logic_data));
+ exprgens_term, 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 (codegens_sort, codegens_type, codegens_expr, defgens) =>
- (codegens_sort, codegens_type,
- codegens_expr
+ (fn (exprgens_sort, exprgens_type, exprgens_term, defgens) =>
+ (exprgens_sort, exprgens_type,
+ exprgens_term
|> Output.update_warn (op =) ("overwriting existing expression code generator " ^ name) (name, (cg, stamp ())),
defgens)),
lookups, serialize_data, logic_data));
@@ -330,8 +330,8 @@
(fn (modl, gens, lookups, serialize_data, logic_data) =>
(modl,
gens |> map_gens
- (fn (codegens_sort, codegens_type, codegens_expr, defgens) =>
- (codegens_sort, codegens_type, codegens_expr,
+ (fn (exprgens_sort, exprgens_type, exprgens_term, defgens) =>
+ (exprgens_sort, exprgens_type, exprgens_term,
defgens
|> Output.update_warn (op =) ("overwriting existing definition code generator " ^ name) (name, (dg, stamp ())))),
lookups, serialize_data, logic_data));
@@ -465,17 +465,17 @@
fun invoke_cg_sort thy defs sort trns =
gen_invoke
- ((map (apsnd (fn (cg, _) => cg thy defs)) o #codegens_sort o #gens o CodegenData.get) thy)
+ ((map (apsnd (fn (cg, _) => cg thy defs)) o #exprgens_sort o #gens o CodegenData.get) thy)
("generating sort " ^ (quote o Sign.string_of_sort thy) sort) sort trns;
fun invoke_cg_type thy defs ty trns =
gen_invoke
- ((map (apsnd (fn (cg, _) => cg thy defs)) o #codegens_type o #gens o CodegenData.get) thy)
+ ((map (apsnd (fn (cg, _) => cg thy defs)) o #exprgens_type o #gens o CodegenData.get) thy)
("generating type " ^ (quote o Sign.string_of_typ thy) ty) ty trns;
fun invoke_cg_expr thy defs t trns =
gen_invoke
- ((map (apsnd (fn (cg, _) => cg thy defs)) o #codegens_expr o #gens o CodegenData.get) thy)
+ ((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 get_defgens thy defs =
@@ -560,32 +560,32 @@
(* code generators *)
-fun codegen_sort_default thy defs sort trns =
+fun exprgen_sort_default thy defs sort trns =
trns
|> fold_map (ensure_def_class thy defs)
(sort |> filter (ClassPackage.is_class thy) |> map (idf_of_name thy nsp_class))
|-> (fn sort => succeed sort)
-fun codegen_type_default thy defs(v as TVar (_, sort)) trns =
+fun exprgen_type_default thy defs(v as TVar (_, sort)) trns =
trns
|> invoke_cg_sort thy defs sort
|-> (fn sort => succeed (IVarT (name_of_tvar v, sort)))
- | codegen_type_default thy defs (v as TFree (_, sort)) trns =
+ | 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)))
- | codegen_type_default thy defs (Type ("fun", [t1, t2])) trns =
+ | exprgen_type_default thy defs (Type ("fun", [t1, t2])) trns =
trns
|> invoke_cg_type thy defs t1
||>> invoke_cg_type thy defs t2
|-> (fn (t1', t2') => succeed (t1' `-> t2'))
- | codegen_type_default thy defs (Type (tyco, tys)) trns =
+ | exprgen_type_default thy defs (Type (tyco, tys)) trns =
trns
|> ensure_def_tyco thy defs (idf_of_tname thy tyco)
||>> fold_map (invoke_cg_type thy defs) tys
|-> (fn (tyco, tys) => succeed (tyco `%% tys))
-fun codegen_expr_default thy defs (Const (f, ty)) trns =
+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;
@@ -615,20 +615,20 @@
|-> (fn ((f, lookup), ty) =>
succeed (mk_itapp (IConst (f, ty)) lookup))
end
- | codegen_expr_default thy defs (Free (v, ty)) trns =
+ | exprgen_term_default thy defs (Free (v, ty)) trns =
trns
|> invoke_cg_type thy defs ty
|-> (fn ty => succeed (IVarE (v, ty)))
- | codegen_expr_default thy defs (Var ((v, i), ty)) trns =
+ | 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)))
- | codegen_expr_default thy defs (Abs (v, ty, t)) trns =
+ | 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))
- | codegen_expr_default thy defs (t1 $ t2) trns =
+ | exprgen_term_default thy defs (t1 $ t2) trns =
trns
|> invoke_cg_expr thy defs t1
||>> invoke_cg_expr thy defs t2
@@ -703,7 +703,7 @@
|> debug 5 (fn _ => "trying defgen class declaration for " ^ quote cls)
|> fold_map (ensure_def_class thy defs)
(map (idf_of_name thy nsp_class) (ClassPackage.get_superclasses thy cls))
- |-> (fn supcls => succeed (Class (supcls, [], []),
+ |-> (fn supcls => succeed (Class (supcls, "a", [], []),
map (idf_of_name thy nsp_mem) (ClassPackage.the_consts thy cls)
@ map (curry (idf_of_inst thy defs) cls) ((map fst o ClassPackage.the_tycos thy) cls)))
| _ =>
@@ -717,12 +717,12 @@
val _ = debug 10 (fn _ => "CLSMEM " ^ quote clsmem) ();
val _ = debug 10 (fn _ => (the o ClassPackage.lookup_const_class thy) clsmem) ();
val cls = idf_of_name thy nsp_class ((the o ClassPackage.lookup_const_class thy) clsmem);
- val (tvar, ty) = ClassPackage.get_const_sign thy clsmem;
+ val ty = ClassPackage.get_const_sign thy "'a" clsmem;
in
trns
|> debug 5 (fn _ => "trying defgen class member for " ^ quote f)
|> invoke_cg_type thy defs ty
- |-> (fn ty => succeed (Classmember (cls, name_of_tvar (TFree (tvar, [])), ty), []))
+ |-> (fn ty => succeed (Classmember (cls, "a", ty), []))
end
| _ =>
trns |> fail ("no class member found for " ^ quote f)
@@ -738,9 +738,9 @@
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)) =
- ((invent_var_t_names
+ ((Term.invent_names
(map ((fn Classmember (_, _, ty) => ty) o get_def univ)
- clsmems) (length arity) [] "a" ~~ arity, clsmems), trns)
+ clsmems |> tvars_of_itypes) "a" (length arity) ~~ arity, clsmems), trns)
in
trns
|> debug 5 (fn _ => "trying defgen class instance for (" ^ quote cls ^ ", " ^ quote tyco ^ ")")
@@ -1190,11 +1190,10 @@
let
fun mk_sfun tab =
let
- fun na name =
- Option.map Codegen.num_args_of (Symtab.lookup tab name)
- fun stx name =
- Codegen.fillin_mixfix ((the o Symtab.lookup tab) name)
- in (na, stx) end;
+ fun f name =
+ Symtab.lookup tab name
+ |> Option.map (fn qs => (Codegen.num_args_of qs, Codegen.fillin_mixfix qs))
+ in f end;
val serialize_data =
thy
|> CodegenData.get
@@ -1307,9 +1306,9 @@
val B = TVar (("'b", 0), []);
in Context.add_setup [
CodegenData.init,
- add_codegen_sort ("default", codegen_sort_default),
- add_codegen_type ("default", codegen_type_default),
- add_codegen_expr ("default", codegen_expr_default),
+ add_codegen_sort ("default", exprgen_sort_default),
+ add_codegen_type ("default", exprgen_type_default),
+ add_codegen_expr ("default", exprgen_term_default),
(* add_codegen_expr ("eq", codegen_eq), *)
add_codegen_expr ("neg", codegen_neg),
add_defgen ("clsdecl", defgen_clsdecl),
--- a/src/Pure/Tools/codegen_serializer.ML Wed Nov 30 17:56:08 2005 +0100
+++ b/src/Pure/Tools/codegen_serializer.ML Wed Nov 30 18:13:31 2005 +0100
@@ -15,13 +15,10 @@
val has_prim: primitives -> string -> bool;
val mk_prims: primitives -> string;
- type num_args_syntax = string -> int option;
- type 'a pretty_syntax = string -> Pretty.T list -> ('a -> Pretty.T)
- -> Pretty.T;
- type serializer = num_args_syntax * CodegenThingol.itype pretty_syntax
- -> num_args_syntax * CodegenThingol.iexpr pretty_syntax
+ type 'a pretty_syntax = string
+ -> (int * (Pretty.T list -> ('a -> Pretty.T) -> Pretty.T)) option;
+ type serializer = CodegenThingol.itype pretty_syntax -> CodegenThingol.iexpr pretty_syntax
-> primitives -> string list option -> CodegenThingol.module -> Pretty.T;
- type parm_serializer = OuterParse.token list -> serializer * OuterParse.token list;
val ml_from_thingol: string list list -> string -> serializer;
val haskell_from_thingol: string list list -> string -> serializer;
@@ -65,15 +62,34 @@
fun mk_prims prims = get_prims prims (Graph.keys prims) |> snd;
+(** keyword arguments **)
+
+type kw = (string * string option) list;
+fun kw_make args =
+ let
+ val parse_keyval = ();
+ in
+ Args.!!! (Scan.repeat (
+ Args.name
+ -- Scan.option (Args.$$$ "=" |-- Args.name)
+ ) #> fst) args
+ end;
+fun kw_get k kw =
+ ((the o AList.lookup (op =) kw) k, AList.delete (op =) k kw);
+fun kw_has kw k =
+ AList.defined (op =) kw k;
+fun kw_done x [] = x
+ | kw_done x kw =
+ error ("uninterpreted keyword arguments: " ^ (commas o map (quote o fst)) kw);
+
+
+
(** generic serialization **)
-type num_args_syntax = string -> int option;
-type 'a pretty_syntax = string -> Pretty.T list -> ('a -> Pretty.T)
- -> Pretty.T;
-type serializer = num_args_syntax * CodegenThingol.itype pretty_syntax
- -> num_args_syntax * CodegenThingol.iexpr pretty_syntax
+type 'a pretty_syntax = string
+ -> (int * (Pretty.T list -> ('a -> Pretty.T) -> Pretty.T)) option;
+type serializer = CodegenThingol.itype pretty_syntax -> CodegenThingol.iexpr pretty_syntax
-> primitives -> string list option -> CodegenThingol.module -> Pretty.T;
-type parm_serializer = OuterParse.token list -> serializer * OuterParse.token list;
datatype lrx = L | R | X;
@@ -123,13 +139,13 @@
fun group_datatypes one_arg defs =
let
- fun check_typ_dup dtname xs =
- if AList.defined (op =) xs dtname
+ fun check_typ_dup dtname ts =
+ if AList.defined (op =) ts dtname
then error ("double datatype definition: " ^ quote dtname)
- else xs
- fun check_typ_miss dtname xs =
- if AList.defined (op =) xs dtname
- then xs
+ else ts
+ fun check_typ_miss dtname ts =
+ if AList.defined (op =) ts dtname
+ then ts
else error ("missing datatype definition: " ^ quote dtname)
fun group (name, Datatype (vs, _, _)) ts =
(if one_arg
@@ -161,12 +177,41 @@
|-> (fn cons => fold group_cons cons)
end;
+fun group_classes defs =
+ let
+ fun check_class_dup clsname ts =
+ if AList.defined (op =) ts clsname
+ then error ("double class definition: " ^ quote clsname)
+ else ts
+ fun check_clsname_miss clsname ts =
+ if AList.defined (op =) ts clsname
+ then ts
+ else error ("missing class definition: " ^ quote clsname)
+ fun group (name, Class (supercls, v, _, _)) ts =
+ ts
+ |> apsnd (check_class_dup name)
+ |> apsnd (AList.update (op =) (name, ((supercls, v), [])))
+ | group (name, Classmember (clsname, _, ty)) ts =
+ ts
+ |> apfst (AList.default (op =) (NameSpace.base clsname, []))
+ |> apfst (AList.map_entry (op =) (NameSpace.base clsname) (cons (name, ty)))
+ | group _ _ =
+ error ("Datatype block containing other statements than datatype or constructor definitions")
+ fun group_members (clsname, member) ts =
+ ts
+ |> check_clsname_miss clsname
+ |> AList.map_entry (op =) clsname (rpair member o fst)
+ in
+ ([], [])
+ |> fold group defs
+ |-> (fn members => fold group_members members)
+ end;
(** ML serializer **)
local
-fun ml_from_defs (tyco_na, tyco_stx) (const_na, const_stx) resolv ds =
+fun ml_from_defs tyco_syntax const_syntax resolv ds =
let
fun chunk_defs ps =
let
@@ -192,14 +237,14 @@
let
val tyargs = (map (ml_from_type BR) typs)
in
- case tyco_na tyco
+ case tyco_syntax tyco
of NONE =>
postify tyargs ((Pretty.str o resolv) tyco)
|> Pretty.block
- | SOME i =>
+ | SOME (i, pr) =>
if i <> length (typs)
then error "can only serialize strictly complete type applications to ML"
- else tyco_stx tyco tyargs (ml_from_type BR)
+ else pr tyargs (ml_from_type BR)
end
| ml_from_type br (IFun (t1, t2)) =
brackify (eval_br_postfix br (INFX (1, R))) [
@@ -410,15 +455,15 @@
| ml_from_app br (f, []) =
Pretty.str (resolv f)
| ml_from_app br (f, es) =
- case const_na f
+ 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
- | SOME i =>
+ | SOME (i, pr) =>
let
val (es1, es2) = splitAt (i, es);
- in mk_app_p br (const_stx f (map (ml_from_expr BR) es1) (ml_from_expr BR)) es2 end;
+ in mk_app_p br (pr (map (ml_from_expr BR) es1) (ml_from_expr BR)) es2 end;
fun ml_from_funs (ds as d::ds_tl) =
let
fun mk_definer [] = "val"
@@ -498,9 +543,9 @@
Pretty.str ";"
]))
| ml_from_def (name, Nop) =
- if exists (fn query => (is_some o query) name)
- [(fn name => tyco_na name),
- (fn name => const_na name)]
+ if exists (fn query => query name)
+ [(fn name => (is_some o tyco_syntax) name),
+ (fn name => (is_some o const_syntax) name)]
then Pretty.str ""
else error ("empty statement during serialization: " ^ quote name)
| ml_from_def (name, Class _) =
@@ -517,7 +562,7 @@
in
-fun ml_from_thingol nspgrp name_root (tyco_syntax) (const_syntax as (const_na, _)) prims select module =
+fun ml_from_thingol nspgrp name_root tyco_syntax const_syntax prims select module =
let
fun ml_validator name =
let
@@ -563,7 +608,8 @@
of Datatypecons (_ , tys) =>
if length tys >= 2 then length tys else 0
| _ =>
- const_na s
+ const_syntax s
+ |> Option.map fst
|> the_default 0
else 0
in
@@ -605,7 +651,7 @@
val bslash = "\\";
-fun haskell_from_defs (tyco_na, tyco_stx) (const_na, const_stx) is_cons resolv defs =
+fun haskell_from_defs tyco_syntax const_syntax is_cons resolv defs =
let
val resolv = fn s =>
let
@@ -647,16 +693,16 @@
fun mk_itype NONE tyargs sctxt =
sctxt
|> pair (brackify (eval_br br BR) ((Pretty.str o upper_first o resolv) tyco :: tyargs))
- | mk_itype (SOME i) tyargs sctxt =
+ | mk_itype (SOME (i, pr)) tyargs sctxt =
if i <> length (tys)
then error "can only serialize strictly complete type applications to haskell"
else
sctxt
- |> pair (tyco_stx tyco tyargs (haskell_from_type BR))
+ |> pair (pr tyargs (haskell_from_type BR))
in
sctxt
|> fold_map (from_itype BR) tys
- |-> mk_itype (tyco_na tyco)
+ |-> mk_itype (tyco_syntax tyco)
end
| from_itype br (IFun (t1, t2)) sctxt =
sctxt
@@ -857,15 +903,15 @@
| haskell_from_app br (f, []) =
Pretty.str (resolv_const f)
| haskell_from_app br (f, es) =
- case const_na f
+ 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
- | SOME i =>
+ | SOME (i, pr) =>
let
val (es1, es2) = splitAt (i, es);
- in mk_app_p br (const_stx f (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;
fun haskell_from_datatypes defs =
let
fun mk_cons (co, typs) =
@@ -886,15 +932,30 @@
in
Pretty.chunks ((separate (Pretty.str "") o map mk_datatype o group_datatypes false) defs)
end;
- fun haskell_from_classes defs = Pretty.str "";
-(*
- | haskell_from_def (name, Class (supclsnames, members, insts)) = Pretty.str ""
- | haskell_from_def (name, Classmember (clsname, v, ty)) = Pretty.str ""
-*)
+ fun haskell_from_classes defs =
+ let
+ fun mk_member (f, ty) =
+ Pretty.block [
+ Pretty.str (f ^ " ::"),
+ Pretty.brk 1,
+ haskell_from_type NOBR ty
+ ];
+ fun mk_class (clsname, ((supclsnames, v), members)) =
+ Pretty.block [
+ Pretty.str "class ",
+ haskell_from_sctxt (map (fn class => (v, [class])) supclsnames),
+ Pretty.str ((upper_first clsname) ^ " " ^ v),
+ Pretty.str " where",
+ Pretty.fbrk,
+ Pretty.chunks (map mk_member members)
+ ];
+ in
+ Pretty.chunks ((separate (Pretty.str "") o map mk_class o group_classes) defs)
+ end;
fun haskell_from_def (name, Nop) =
- if exists (fn query => (is_some o query) name)
- [(fn name => tyco_na name),
- (fn name => const_na name)]
+ if exists (fn query => query name)
+ [(fn name => (is_some o tyco_syntax) name),
+ (fn name => (is_some o const_syntax) name)]
then Pretty.str ""
else error ("empty statement during serialization: " ^ quote name)
| haskell_from_def (name, Fun (eqs, (_, ty))) =
@@ -951,7 +1012,7 @@
in
-fun haskell_from_thingol nspgrp name_root tyco_syntax (const_syntax as (const_na, _)) prims select module =
+fun haskell_from_thingol nspgrp name_root tyco_syntax const_syntax prims select module =
let
fun haskell_from_module (name, ps) =
Pretty.block [
@@ -969,7 +1030,8 @@
of Datatypecons (_ , tys) =>
if length tys >= 2 then length tys else 0
| _ =>
- const_na s
+ const_syntax s
+ |> Option.map fst
|> the_default 0
else 0;
fun is_cons f =
--- a/src/Pure/Tools/codegen_thingol.ML Wed Nov 30 17:56:08 2005 +0100
+++ b/src/Pure/Tools/codegen_thingol.ML Wed Nov 30 18:13:31 2005 +0100
@@ -40,22 +40,23 @@
val itype_of_iexpr: iexpr -> itype;
val ipat_of_iexpr: iexpr -> ipat;
val eq_itype: itype * itype -> bool;
- val invent_var_t_names: itype list -> int -> vname list -> vname -> vname list;
- val invent_var_e_names: iexpr list -> int -> vname list -> vname -> vname list;
+ val tvars_of_itypes: itype list -> string list;
+ val vars_of_ipats: ipat list -> string list;
+ val vars_of_iexprs: iexpr list -> string list;
datatype def =
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 * string list
+ | Datatype of (vname * string list) list * string list * class list
| Datatypecons of string * itype list
- | Class of string list * string list * string list
- | Classmember of string * vname * itype
- | Classinst of string * (string * (vname * string list) list) * (string * string) list;
+ | Class of class list * vname * string list * string list
+ | Classmember of class * vname * itype
+ | Classinst of class * (string * (vname * string list) list) * (string * string) list;
type module;
type transact;
type 'dst transact_fin;
- type ('src, 'dst) gen_codegen = 'src -> transact -> 'dst transact_fin;
+ type ('src, 'dst) gen_exprgen = 'src -> transact -> 'dst transact_fin;
type gen_defgen = string -> transact -> (def * string list) transact_fin;
val pretty_def: def -> Pretty.T;
val pretty_module: module -> Pretty.T;
@@ -65,7 +66,7 @@
val partof: string list -> module -> module;
val succeed: 'a -> transact -> 'a transact_fin;
val fail: string -> transact -> 'a transact_fin;
- val gen_invoke: (string * ('src, 'dst) gen_codegen) list -> string
+ val gen_invoke: (string * ('src, 'dst) gen_exprgen) list -> string
-> 'src -> transact -> 'dst * transact;
val gen_ensure_def: (string * gen_defgen) list -> string
-> string -> transact -> transact;
@@ -102,6 +103,7 @@
val Fun_wfrec: iexpr;
val prims: string list;
+ val is_eqtype: module -> itype -> bool;
val extract_defs: iexpr -> string list;
val eta_expand: (string -> int) -> module -> module;
val eta_expand_poly: module -> module;
@@ -142,20 +144,6 @@
fun debug d f x = (if d <= !debug_level then Output.debug (f x) else (); x);
val soft_exc = ref true;
-fun foldl' f (l, []) = the l
- | foldl' f (_, (r::rs)) =
- let
- fun itl (l, []) = l
- | itl (l, r::rs) = itl (f (l, r), rs)
- in itl (r, rs) end;
-
-fun foldr' f ([], r) = the r
- | foldr' f (ls, _) =
- let
- fun itr [l] = l
- | itr (l::ls) = f (l, itr ls)
- in itr ls end;
-
fun unfoldl dest x =
case dest x
of NONE => (x, [])
@@ -399,19 +387,44 @@
case unfold_app e of (IConst (f, ty), es) =>
ICons ((f, map ipat_of_iexpr es), (snd o unfold_fun) ty);
-fun vars_of_itype ty =
+fun tvars_of_itypes tys =
let
- fun vars (IType (_, tys)) = fold vars tys
- | vars (IFun (ty1, ty2)) = vars ty1 #> vars ty2
- | vars (IVarT (v, _)) = cons v
- in vars ty [] end;
+ fun vars (IType (_, tys)) =
+ fold vars tys
+ | vars (IFun (ty1, ty2)) =
+ vars ty1 #> vars ty2
+ | vars (IVarT (v, _)) =
+ insert (op =) v
+ in fold vars tys [] end;
fun vars_of_ipats ps =
let
- fun vars (ICons ((_, ps), _)) = fold vars ps
- | vars (IVarP (v, _)) = cons v
+ 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
+ | vars (IVarE (v, _)) =
+ insert (op =) v
+ | vars (IApp (e1, e2)) =
+ vars e1 #> vars e2
+ | vars (IAbs ((v, _), e)) =
+ insert (op =) v
+ #> 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
+ | vars (IDictE ms) =
+ fold (vars o snd) ms
+ in fold vars es [] end;
+
fun instant_itype (v, sty) ty =
let
fun instant (IType (tyco, tys)) =
@@ -422,36 +435,6 @@
if v = u then sty else w
in instant ty end;
-fun invent_var_t_names tys n used a =
- let
- fun invent (IType (_, tys)) =
- fold invent tys
- | invent (IFun (ty1, ty2)) =
- invent ty1 #> invent ty2
- | invent (IVarT (v, _)) =
- cons v
-in Term.invent_names (fold invent tys used) a n end;
-
-fun invent_var_e_names es n used a =
- let
- fun invent (IConst (f, _)) =
- I
- | invent (IVarE (v, _)) =
- insert (op =) v
- | invent (IApp (e1, e2)) =
- invent e1 #> invent e2
- | invent (IAbs ((v, _), e)) =
- insert (op =) v #> invent e
- | invent (ICase (e, cs)) =
- invent e
- #> fold (fn (p, e) => fold (insert (op =)) (vars_of_ipats [p]) #> invent e) cs
- | invent (IInst (e, lookup)) =
- invent e
- | invent (IDictE ms) =
- fold (invent o snd) ms
- | invent (ILookup (ls, v)) = error "ILOOKUP"
- in Term.invent_names (fold invent es used) a n end;
-
(** language module system - definitions, modules, transactions **)
@@ -464,16 +447,16 @@
| Typesyn of (vname * string list) list * itype
| Datatype of (vname * string list) list * string list * string list
| Datatypecons of string * itype list
- | Class of string list * string list * string list
- | Classmember of string * string * itype
- | Classinst of string * (string * (vname * string list) list) * (string * string) list;
+ | Class of class list * vname * string list * string list
+ | Classmember of class * vname * itype
+ | Classinst of class * (string * (vname * string list) list) * (string * string) list;
datatype node = Def of def | Module of node Graph.T;
type module = node Graph.T;
type transact = Graph.key list * module;
datatype 'dst transact_res = Succeed of 'dst | Fail of string list * exn option;
type 'dst transact_fin = 'dst transact_res * transact;
-type ('src, 'dst) gen_codegen = 'src -> transact -> 'dst transact_fin;
+type ('src, 'dst) gen_exprgen = 'src -> transact -> 'dst transact_fin;
type gen_defgen = string -> transact -> (def * string list) transact_fin;
exception FAIL of string list * exn option;
@@ -514,7 +497,7 @@
Pretty.str "cons ",
Pretty.gen_list " ->" "" "" (map pretty_itype tys @ [Pretty.str dtname])
]
- | pretty_def (Class (supcls, mems, insts)) =
+ | pretty_def (Class (supcls, _, mems, insts)) =
Pretty.block [
Pretty.str "class extending ",
Pretty.gen_list "," "[" "]" (map Pretty.str supcls),
@@ -721,10 +704,10 @@
in
([([], fn [] => check_var ty NONE),
([clsname],
- fn [Class (_, _, [])] => NONE
+ fn [Class (_, _, _, [])] => NONE
| _ => "attempted to add class member to witnessed class" |> SOME)],
[(clsname,
- fn Class (supcs, mems, insts) => Class (supcs, name::mems, insts)
+ fn Class (supcs, v, mems, insts) => Class (supcs, v, name::mems, insts)
| def => "attempted to add class member to non-class"
^ (Pretty.output o pretty_def) def |> error)])
end
@@ -747,7 +730,7 @@
in
(map (fn (memname, memprim) => ([memname, memprim], check)) memdefs,
[(clsname,
- fn Class (supcs, mems, insts) => Class (supcs, mems, name::insts)
+ fn Class (supcs, v, mems, insts) => Class (supcs, v, mems, name::insts)
| def => "attempted to add class instance to non-class"
^ (Pretty.output o pretty_def) def |> error),
(tyco,
@@ -879,7 +862,7 @@
(** primitive language constructs **)
-val class_eq = "Eqtype"; (*defined for all primitve types and extensionally for all datatypes*)
+val class_eq = "Eq"; (*defined for all primitve types and extensionally for all datatypes*)
val type_bool = "Bool";
val type_integer = "Integer"; (*infinite!*)
val type_float = "Float";
@@ -962,6 +945,33 @@
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;
+
+fun is_eqtype modl (IType (tyco, tys)) =
+ forall (is_eqtype modl) tys
+ andalso
+ if NameSpace.is_qualified tyco
+ then
+ 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
+ | is_eqtype modl (IFun _) =
+ false
+ | is_eqtype modl (IVarT (_, sort)) =
+ exists (is_superclass_of modl class_eq) sort
+
fun extract_defs e =
let
fun extr_itype (ty as IType (tyco, _)) =
@@ -993,7 +1003,7 @@
|> curry Library.drop (length es)
|> curry Library.take add_n
val add_vars =
- invent_var_e_names es add_n [] "x" ~~ tys;
+ Term.invent_names (vars_of_iexprs es) "x" add_n ~~ tys;
in
Library.foldr IAbs (add_vars, IConst (f, ty) `$$ es `$$ (map IVarE add_vars))
end;
@@ -1012,11 +1022,11 @@
let
fun map_def_fun (def as Fun ([([], e)], cty as (sortctxt, (ty as IFun (ty1, ty2))))) =
if (not o null) sortctxt
- orelse (null o vars_of_itype) ty
+ orelse (null o tvars_of_itypes) [ty]
then def
else
let
- val add_var = (hd (invent_var_e_names [e] 1 [] "x"), ty1)
+ 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
| map_def_fun def = def;
in map_defs map_def_fun end;
@@ -1038,14 +1048,14 @@
(def, acc)
| replace_def (name, (Datatypecons (tyco, tys))) acc =
(Datatypecons (tyco,
- [foldl' (op xx) (NONE, tys)]), name::acc)
+ [foldr1 (op xx) tys]), name::acc)
| replace_def (_, def) acc = (def, acc);
fun replace_app cs ((f, ty), es) =
if member (op =) cs f
then
let
val (tys, ty') = unfold_fun ty
- in IConst (f, foldr' (op xx) (tys, NONE) `-> ty') `$ foldl' (op **) (NONE, es) end
+ in IConst (f, foldr1 (op xx) tys `-> ty') `$ foldr1 (op **) es end
else IConst (f, ty) `$$ es;
fun replace_iexpr cs (IConst (f, ty)) =
replace_app cs ((f, ty), [])
@@ -1056,7 +1066,7 @@
| replace_iexpr cs e = map_iexpr I I (replace_iexpr cs) e;
fun replace_ipat cs (p as ICons ((c, ps), ty)) =
if member (op =) cs c then
- ICons ((c, [(foldl' (op &&) (NONE, map (replace_ipat cs) ps))]), ty)
+ ICons ((c, [(foldr1 (op &&) (map (replace_ipat cs) ps))]), ty)
else map_ipat I (replace_ipat cs) p
| replace_ipat cs p = map_ipat I (replace_ipat cs) p;
in
@@ -1068,17 +1078,17 @@
fun mk_cls_typ_map memberdecls ty_inst =
map (fn (memname, (v, ty)) =>
(memname, ty |> instant_itype (v, ty_inst))) memberdecls;
- fun transform_dicts (Class (supcls, members, _)) =
+ fun transform_dicts (Class (supcls, v, members, _)) =
let
val memberdecls = AList.make
((fn Classmember (_, v, ty) => (v, ty)) o get_def module) members;
- val varname_cls = invent_var_t_names (map (snd o snd) memberdecls) 1 [] "a" |> hd;
+ val varname_cls = Term.invent_names (tvars_of_itypes (map (snd o snd) memberdecls)) "a" 1 |> hd
in
Typesyn ([(varname_cls, [])], IDictT (mk_cls_typ_map memberdecls (IVarT (varname_cls, []))))
end
| transform_dicts (Classinst (clsname, (tyco, arity), memdefs)) =
let
- val Class (_, members, _) = get_def module clsname;
+ val Class (_, _, members, _) = get_def module clsname;
val memberdecls = AList.make
((fn Classmember (_, v, ty) => (v, ty)) o get_def module) members;
val ty_arity = tyco `%% map IVarT arity;
@@ -1092,22 +1102,21 @@
| transform_dicts d = d
fun transform_defs (Fun (ds, (sortctxt, ty))) =
let
- fun reduce f xs = foldl' f (NONE, xs);
val _ = writeln ("class 1");
val varnames_ctxt =
sortctxt
|> length o Library.flat o map snd
- |> (fn used => invent_var_e_names (map snd ds) used ((vars_of_ipats o fst o hd) ds) "d")
+ |> Term.invent_names ((vars_of_iexprs o map snd) ds @ (vars_of_ipats o Library.flat o map fst) ds) "d"
|> unflat (map snd sortctxt);
val _ = writeln ("class 2");
val vname_alist = map2 (fn ((vt, sort), vs) => (vt, vs ~~ sort)) (sortctxt, varnames_ctxt);
val _ = writeln ("class 3");
fun add_typarms ty =
- map (reduce (op xx) o (fn (vt, vss) => map (fn (_, cls) => cls `%% [IVarT (vt, [])]) vss)) vname_alist
+ map (foldr1 (op xx) o (fn (vt, vss) => map (fn (_, cls) => cls `%% [IVarT (vt, [])]) vss)) vname_alist
`--> ty;
val _ = writeln ("class 4");
fun add_parms ps =
- map (reduce (op &&) o (fn (vt, vss) => map (fn (v, cls) => IVarP (v, cls `%% [IVarT (vt, [])])) vss)) vname_alist
+ map (foldr1 (op &&) o (fn (vt, vss) => map (fn (v, cls) => IVarP (v, cls `%% [IVarT (vt, [])])) vss)) vname_alist
@ ps;
val _ = writeln ("class 5");
fun transform_itype (IVarT (v, s)) =
@@ -1132,8 +1141,8 @@
in (mk_parm cls, ILookup (rev deriv, v')) end
and transform_lookups lss =
map_yield (map_yield transform_lookup
- #> apfst (reduce (op xx))
- #> apsnd (reduce (op **))) lss;
+ #> apfst (foldr1 (op xx))
+ #> apsnd (foldr1 (op **))) lss;
val _ = writeln ("class 8");
fun transform_iexpr (IInst (e, ls)) =
(writeln "A"; transform_iexpr e `$$ (snd o transform_lookups) ls)