--- a/src/Pure/Tools/codegen_package.ML Tue Jan 16 14:10:26 2007 +0100
+++ b/src/Pure/Tools/codegen_package.ML Tue Jan 16 14:10:27 2007 +0100
@@ -114,17 +114,17 @@
fun ensure_def_class thy (algbr as ((proj_sort, _), _)) funcgr strct class trns =
let
+ val superclasses = (proj_sort o Sign.super_classes thy) class;
val (v, cs) = AxClass.params_of_class thy class;
- val superclasses = (proj_sort o Sign.super_classes thy) class;
+ val class' = CodegenNames.class thy class;
+ val classrels' = map (curry (CodegenNames.classrel thy) class) superclasses;
val classops' = map (CodegenNames.const thy o CodegenConsts.norm_of_typ thy) cs;
- val class' = CodegenNames.class thy class;
fun defgen_class trns =
trns
|> fold_map (ensure_def_class thy algbr funcgr strct) superclasses
||>> (fold_map (exprgen_type thy algbr funcgr strct) o map snd) cs
|-> (fn (superclasses, classoptyps) => succeed
- (CodegenThingol.Class (superclasses,
- (unprefix "'" v, classops' ~~ classoptyps))))
+ (CodegenThingol.Class (superclasses ~~ classrels', (unprefix "'" v, classops' ~~ classoptyps))))
in
trns
|> tracing (fn _ => "generating class " ^ quote class)
@@ -132,6 +132,10 @@
("generating class " ^ quote class) class'
|> pair class'
end
+and ensure_def_classrel thy algbr funcgr strct (subclass, superclass) trns =
+ trns
+ |> ensure_def_class thy algbr funcgr strct subclass
+ |-> (fn _ => pair (CodegenNames.classrel thy (subclass, superclass)))
and ensure_def_tyco thy algbr funcgr strct tyco trns =
let
fun defgen_datatype trns =
@@ -186,40 +190,39 @@
exception CONSTRAIN of (string * typ) * typ;
val timing = ref false;
-fun exprgen_typinst thy (algbr as ((proj_sort, algebra), consts)) funcgr strct (ty_ctxt, sort_decl) trns =
+fun exprgen_dicts thy (algbr as ((proj_sort, algebra), consts)) funcgr strct (ty_ctxt, sort_decl) trns =
let
val pp = Sign.pp thy;
- datatype inst =
- Inst of (class * string) * inst list list
- | Contxt of (string * sort) * (class list * int);
- fun classrel (l as Contxt (v_sort, (classes, n)), _) class =
- Contxt (v_sort, (class :: classes, n))
- | classrel (Inst ((_, tyco), lss), _) class =
- Inst ((class, tyco), lss);
- fun constructor tyco iss class =
- Inst ((class, tyco), (map o map) fst iss);
+ datatype typarg =
+ Global of (class * string) * typarg list list
+ | Local of (class * class) list * (string * (int * sort));
+ fun classrel (Global ((_, tyco), yss), _) class =
+ Global ((class, tyco), yss)
+ | classrel (Local (classrels, v), subclass) superclass =
+ Local ((subclass, superclass) :: classrels, v);
+ fun constructor tyco yss class =
+ Global ((class, tyco), (map o map) fst yss);
fun variable (TFree (v, sort)) =
let
val sort' = proj_sort sort;
- in map_index (fn (n, class) => (Contxt ((v, sort'), ([], n)), class)) sort' end;
- val insts = Sorts.of_sort_derivation pp algebra
+ in map_index (fn (n, class) => (Local ([], (v, (n, sort'))), class)) sort' end;
+ val typargs = Sorts.of_sort_derivation pp algebra
{classrel = classrel, constructor = constructor, variable = variable}
(ty_ctxt, proj_sort sort_decl);
- fun mk_dict (Inst (inst, instss)) trns =
+ fun mk_dict (Global (inst, yss)) trns =
trns
|> ensure_def_inst thy algbr funcgr strct inst
- ||>> (fold_map o fold_map) mk_dict instss
- |-> (fn (inst, instss) => pair (Instance (inst, instss)))
- | mk_dict (Contxt ((v, sort), (classes, k))) trns =
+ ||>> (fold_map o fold_map) mk_dict yss
+ |-> (fn (inst, dss) => pair (DictConst (inst, dss)))
+ | mk_dict (Local (classrels, (v, (k, sort)))) trns =
trns
- |> fold_map (ensure_def_class thy algbr funcgr strct) classes
- |-> (fn classes => pair (Context ((classes, k), (unprefix "'" v,
- length sort))))
+ |> fold_map (ensure_def_classrel thy algbr funcgr strct) classrels
+ |-> (fn classrels => pair (DictVar (classrels, (unprefix "'" v, (k, length sort)))))
in
trns
- |> fold_map mk_dict insts
+ |> fold_map mk_dict typargs
end
-and exprgen_typinst_const thy (algbr as (_, consts)) funcgr strct (c, ty_ctxt) trns =
+and exprgen_dict_parms thy (algbr as (_, consts)) funcgr strct (c, ty_ctxt) trns =
let
val c' = CodegenConsts.norm_of_typ thy (c, ty_ctxt)
val idf = CodegenNames.const thy c';
@@ -230,7 +233,7 @@
then raise CONSTRAIN ((c, ty_decl), ty_ctxt) else ();
in
trns
- |> fold_map (exprgen_typinst thy algbr funcgr strct) insts
+ |> fold_map (exprgen_dicts thy algbr funcgr strct) insts
end
and ensure_def_inst thy (algbr as ((proj_sort, _), _)) funcgr strct (class, tyco) trns =
let
@@ -243,8 +246,10 @@
fun gen_superarity superclass trns =
trns
|> ensure_def_class thy algbr funcgr strct superclass
- ||>> exprgen_typinst thy algbr funcgr strct (arity_typ, [superclass])
- |-> (fn (superclass, [Instance (inst, iss)]) => pair (superclass, (inst, iss)));
+ ||>> ensure_def_classrel thy algbr funcgr strct (class, superclass)
+ ||>> exprgen_dicts thy algbr funcgr strct (arity_typ, [superclass])
+ |-> (fn ((superclass, classrel), [DictConst (inst, dss)]) =>
+ pair (superclass, (classrel, (inst, dss))));
fun gen_classop_def (classop, t) trns =
trns
|> ensure_def_const thy algbr funcgr strct classop
@@ -354,7 +359,7 @@
trns
|> ensure_def_const thy algbr funcgr strct (CodegenConsts.norm_of_typ thy (c, ty))
||>> exprgen_type thy algbr funcgr strct ty
- ||>> exprgen_typinst_const thy algbr funcgr strct (c, ty)
+ ||>> exprgen_dict_parms thy algbr funcgr strct (c, ty)
||>> fold_map (exprgen_term thy algbr funcgr strct) ts
|-> (fn (((c, ty), iss), ts) =>
pair (IConst (c, (iss, ty)) `$$ ts))
--- a/src/Pure/Tools/codegen_serializer.ML Tue Jan 16 14:10:26 2007 +0100
+++ b/src/Pure/Tools/codegen_serializer.ML Tue Jan 16 14:10:27 2007 +0100
@@ -288,57 +288,37 @@
datatype ml_def =
MLFuns of (string * ((iterm list * iterm) list * typscheme)) list
| MLDatas of (string * ((vname * sort) list * (string * itype list) list)) list
- | MLClass of string * (class list * (vname * (string * itype) list))
+ | MLClass of string * ((class * string) list * (vname * (string * itype) list))
| MLClassinst of string * ((class * (string * (vname * sort) list))
- * ((class * (string * inst list list)) list
+ * ((class * (string * (string * dict list list))) list
* (string * iterm) list));
fun pr_sml tyco_syntax const_syntax keyword_vars deresolv is_cons ml_def =
let
- fun dictvar v =
- first_upper v ^ "_";
- val label = translate_string (fn "." => "__" | c => c) o NameSpace.qualifier;
- val mk_classop_name = suffix "_" o snd o dest_name;
- fun pr_tyvar (v, []) =
- str "()"
- | pr_tyvar (v, sort) =
- let
- fun pr_class class =
- str ("'" ^ v ^ " " ^ deresolv class);
- in
- Pretty.block [
- str "(",
- (str o dictvar) v,
- str ":",
- case sort
- of [class] => pr_class class
- | _ => Pretty.enum " *" "" "" (map pr_class sort),
- str ")"
- ]
- end;
- fun pr_insts fxy iys =
+ val pr_label = translate_string (fn "." => "__" | c => c) o NameSpace.qualifier;
+ fun pr_dicts fxy ds =
let
- fun pr_proj s = str ("#" ^ s);
- fun pr_lookup [] p =
+ fun pr_dictvar (v, (_, 1)) = first_upper v ^ "_"
+ | pr_dictvar (v, (i, _)) = first_upper v ^ string_of_int (i+1) ^ "_";
+ fun pr_proj [] p =
p
- | pr_lookup [p'] p =
+ | pr_proj [p'] p =
brackets [p', p]
- | pr_lookup (ps as _ :: _) p =
+ | pr_proj (ps as _ :: _) p =
brackets [Pretty.enum " o" "(" ")" ps, p];
- fun pr_inst fxy (Instance (inst, iss)) =
- brackify fxy (
- (str o deresolv) inst
- :: map (pr_insts BR) iss
- )
- | pr_inst fxy (Context ((classes, i), (v, k))) =
- pr_lookup (map (pr_proj o label) classes
- @ (if k = 1 then [] else [(pr_proj o string_of_int) (i+1)])
- ) ((str o dictvar) v);
- in case iys
+ fun pr_dictc fxy (DictConst (inst, dss)) =
+ brackify fxy ((str o deresolv) inst :: map (pr_dicts BR) dss)
+ | pr_dictc fxy (DictVar (classrels, v)) =
+ pr_proj (map (str o deresolv) classrels) ((str o pr_dictvar) v)
+ in case ds
of [] => str "()"
- | [iy] => pr_inst fxy iy
- | _ :: _ => (Pretty.list "(" ")" o map (pr_inst NOBR)) iys
+ | [d] => pr_dictc fxy d
+ | _ :: _ => (Pretty.list "(" ")" o map (pr_dictc NOBR)) ds
end;
+ fun pr_tyvars vs =
+ vs
+ |> map (fn (v, sort) => map_index (fn (i, _) => DictVar ([], (v, (i, length sort)))) sort)
+ |> map (pr_dicts BR);
fun pr_tycoexpr fxy (tyco, tys) =
let
val tyco' = (str o deresolv) tyco
@@ -424,7 +404,7 @@
[(str o deresolv) c, Pretty.enum "," "(" ")" (map (pr_term vars NOBR) ts)]
else [pr_term vars BR (CodegenThingol.eta_expand app k)] end else
(str o deresolv) c
- :: ((map (pr_insts BR) o filter_out null) iss @ map (pr_term vars BR) ts)
+ :: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term vars BR) ts)
and pr_app vars = gen_pr_app pr_app' pr_term const_syntax vars
and pr_bind' ((NONE, NONE), _) = str "_"
| pr_bind' ((SOME v, NONE), _) = str v
@@ -465,7 +445,7 @@
andalso not (ty = ITyVar "_")(*for evaluation*)
then [str ":", pr_typ NOBR ty]
else
- map pr_tyvar vs
+ pr_tyvars vs
@ map (pr_term vars BR) ts)
@ [str "=", pr_term vars NOBR t]
)
@@ -499,24 +479,32 @@
in Pretty.chunks (ps @ [Pretty.block ([p, str ";"])]) end
| pr_def (MLClass (class, (superclasses, (v, classops)))) =
let
- val w = dictvar v;
- fun pr_superclass class =
+ val w = first_upper v ^ "_";
+ fun pr_superclass_field (class, classrel) =
(concat o map str) [
- label class, ":", "'" ^ v, deresolv class
+ pr_label classrel, ":", "'" ^ v, deresolv class
];
- fun pr_classop (classop, ty) =
+ fun pr_classop_field (classop, ty) =
concat [
- (*FIXME?*)
- (str o mk_classop_name) classop, str ":", pr_typ NOBR ty
+ (str o pr_label) classop, str ":", pr_typ NOBR ty
];
- fun pr_classop_fun (classop, _) =
- concat [
+ fun pr_classop_proj (classop, _) =
+ semicolon [
str "fun",
(str o deresolv) classop,
Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ deresolv class)],
str "=",
- str ("#" ^ mk_classop_name classop),
- str (w ^ ";")
+ str ("#" ^ pr_label classop),
+ str w
+ ];
+ fun pr_superclass_proj (_, classrel) =
+ semicolon [
+ str "fun",
+ (str o deresolv) classrel,
+ Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ deresolv class)],
+ str "=",
+ str ("#" ^ pr_label classrel),
+ str w
];
in
Pretty.chunks (
@@ -525,45 +513,44 @@
(str o deresolv) class,
str "=",
Pretty.enum "," "{" "};" (
- map pr_superclass superclasses @ map pr_classop classops
+ map pr_superclass_field superclasses @ map pr_classop_field classops
)
]
- :: map pr_classop_fun classops
+ :: map pr_superclass_proj superclasses
+ @ map pr_classop_proj classops
)
end
| pr_def (MLClassinst (inst, ((class, (tyco, arity)), (superarities, classop_defs)))) =
let
- fun pr_superclass (superclass, superinst_iss) =
+ fun pr_superclass (_, (classrel, dss)) =
concat [
- (str o label) superclass,
+ (str o pr_label) classrel,
str "=",
- pr_insts NOBR [Instance superinst_iss]
+ pr_dicts NOBR [DictConst dss]
];
- fun pr_classop_def (classop, t) =
+ fun pr_classop (classop, t) =
let
val consts = map_filter
(fn c => if (is_some o const_syntax) c
then NONE else (SOME o NameSpace.base o deresolv) c)
(CodegenThingol.fold_constnames (insert (op =)) t []);
- val vars = keyword_vars
- |> CodegenNames.intro_vars consts;
+ val vars = CodegenNames.intro_vars consts keyword_vars;
in
concat [
- (str o mk_classop_name) classop,
+ (str o pr_label) classop,
str "=",
pr_term vars NOBR t
]
end;
in
- concat ([
+ semicolon ([
str (if null arity then "val" else "fun"),
(str o deresolv) inst ] @
- map pr_tyvar arity @ [
+ pr_tyvars arity @ [
str "=",
- Pretty.enum "," "{" "}" (map pr_superclass superarities @ map pr_classop_def classop_defs),
+ Pretty.enum "," "{" "}" (map pr_superclass superarities @ map pr_classop classop_defs),
str ":",
- pr_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity]),
- str ";;"
+ pr_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity])
])
end;
in pr_def ml_def end;
@@ -580,53 +567,25 @@
fun pr_ocaml tyco_syntax const_syntax keyword_vars deresolv is_cons ml_def =
let
- fun dictvar v = "_" ^ first_upper v;
- fun pr_tyvar (v, []) =
- str "()"
- | pr_tyvar (v, sort) =
- let
- fun pr_class class =
- str ("'" ^ v ^ " " ^ deresolv class);
- in
- Pretty.block [
- str "(",
- (str o dictvar) v,
- str ":",
- case sort
- of [class] => pr_class class
- | _ => Pretty.enum " *" "" "" (map pr_class sort),
- str ")"
- ]
- end;
- fun pr_insts fxy iys =
+ fun pr_dicts fxy ds =
let
- fun dot p2 p1 = Pretty.block [p1, str ".", str p2];
- fun proj k i p = (brackets o map str) [
- "match",
- p,
- "with",
- replicate i "_" |> nth_map k (K "d") |> separate (", ") |> implode,
- "-> d"
- ]
- fun pr_lookup [] p =
- p
- | pr_lookup [p'] p =
- dot p' p
- | pr_lookup (ps as _ :: _) p =
- fold_rev dot ps p;
- fun pr_inst fxy (Instance (inst, iss)) =
- brackify fxy (
- (str o deresolv) inst
- :: map (pr_insts BR) iss
- )
- | pr_inst fxy (Context ((classes, k), (v, i))) =
- if i = 1 then pr_lookup (map deresolv classes) ((str o dictvar) v)
- else pr_lookup (map deresolv classes) (proj k i (dictvar v));
- in case iys
+ fun pr_dictvar (v, (_, 1)) = "_" ^ first_upper v
+ | pr_dictvar (v, (i, _)) = "_" ^ first_upper v ^ string_of_int (i+1);
+ fun pr_proj ps p =
+ fold_rev (fn p2 => fn p1 => Pretty.block [p1, str ".", str p2]) ps p
+ fun pr_dictc fxy (DictConst (inst, dss)) =
+ brackify fxy ((str o deresolv) inst :: map (pr_dicts BR) dss)
+ | pr_dictc fxy (DictVar (classrels, v)) =
+ pr_proj (map deresolv classrels) ((str o pr_dictvar) v)
+ in case ds
of [] => str "()"
- | [iy] => pr_inst fxy iy
- | _ :: _ => (Pretty.list "(" ")" o map (pr_inst NOBR)) iys
+ | [d] => pr_dictc fxy d
+ | _ :: _ => (Pretty.list "(" ")" o map (pr_dictc NOBR)) ds
end;
+ fun pr_tyvars vs =
+ vs
+ |> map (fn (v, sort) => map_index (fn (i, _) => DictVar ([], (v, (i, length sort)))) sort)
+ |> map (pr_dicts BR);
fun pr_tycoexpr fxy (tyco, tys) =
let
val tyco' = (str o deresolv) tyco
@@ -702,7 +661,7 @@
| _ => [(str o deresolv) c, Pretty.enum "," "(" ")" (map (pr_term vars NOBR) ts)]
else [pr_term vars BR (CodegenThingol.eta_expand app ((length o fst o CodegenThingol.unfold_fun) ty))]
else (str o deresolv) c
- :: ((map (pr_insts BR) o filter_out null) iss @ map (pr_term vars BR) ts)
+ :: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term vars BR) ts)
and pr_app vars = gen_pr_app pr_app' pr_term const_syntax vars
and pr_bind' ((NONE, NONE), _) = str "_"
| pr_bind' ((SOME v, NONE), _) = str v
@@ -793,7 +752,7 @@
concat (
str definer
:: (str o deresolv) name
- :: map_filter (fn (_, []) => NONE | v => SOME (pr_tyvar v)) vs
+ :: pr_tyvars (filter_out (null o snd) vs)
@| pr_eqs eqs
);
val (ps, p) = split_last (pr_funn "let rec" funn :: map (pr_funn "and") funns');
@@ -819,43 +778,41 @@
in Pretty.chunks (ps @ [Pretty.block ([p, str ";;"])]) end
| pr_def (MLClass (class, (superclasses, (v, classops)))) =
let
- val w = dictvar v;
- fun pr_superclass class =
+ val w = "_" ^ first_upper v;
+ fun pr_superclass_field (class, classrel) =
(concat o map str) [
- deresolv class, ":", "'" ^ v, deresolv class
+ deresolv classrel, ":", "'" ^ v, deresolv class
];
- fun pr_classop (classop, ty) =
+ fun pr_classop_field (classop, ty) =
concat [
(str o deresolv) classop, str ":", pr_typ NOBR ty
];
- fun pr_classop_fun (classop, _) =
+ fun pr_classop_proj (classop, _) =
concat [
str "let",
(str o deresolv) classop,
- Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ deresolv class)],
+ str w,
str "=",
str (w ^ "." ^ deresolv classop ^ ";;")
];
- in
- Pretty.chunks (
- concat [
- str ("type '" ^ v),
- (str o deresolv) class,
- str "=",
- Pretty.enum ";" "{" "};;" (
- map pr_superclass superclasses @ map pr_classop classops
- )
- ]
- :: map pr_classop_fun classops
- )
- end
+ in Pretty.chunks (
+ concat [
+ str ("type '" ^ v),
+ (str o deresolv) class,
+ str "=",
+ Pretty.enum ";" "{" "};;" (
+ map pr_superclass_field superclasses @ map pr_classop_field classops
+ )
+ ]
+ :: map pr_classop_proj classops
+ ) end
| pr_def (MLClassinst (inst, ((class, (tyco, arity)), (superarities, classop_defs)))) =
let
- fun pr_superclass (superclass, superinst_iss) =
+ fun pr_superclass (_, (classrel, dss)) =
concat [
- (str o deresolv) superclass,
+ (str o deresolv) classrel,
str "=",
- pr_insts NOBR [Instance superinst_iss]
+ pr_dicts NOBR [DictConst dss]
];
fun pr_classop_def (classop, t) =
let
@@ -863,8 +820,7 @@
(fn c => if (is_some o const_syntax) c
then NONE else (SOME o NameSpace.base o deresolv) c)
(CodegenThingol.fold_constnames (insert (op =)) t []);
- val vars = keyword_vars
- |> CodegenNames.intro_vars consts;
+ val vars = CodegenNames.intro_vars consts keyword_vars;
in
concat [
(str o deresolv) classop,
@@ -876,7 +832,7 @@
concat (
str "let"
:: (str o deresolv) inst
- :: map pr_tyvar arity
+ :: pr_tyvars arity
@ str "="
@@ (Pretty.enclose "(" ");;" o Pretty.breaks) [
Pretty.enum ";" "{" "}" (map pr_superclass superarities @ map pr_classop_def classop_defs),
@@ -967,6 +923,8 @@
fold_map
(fn (name, CodegenThingol.Class info) =>
map_nsp_typ (name_def false name) >> (fn base => (base, SOME (name, info)))
+ | (name, CodegenThingol.Classrel _) =>
+ map_nsp_fun (name_def false name) >> (fn base => (base, NONE))
| (name, CodegenThingol.Classop _) =>
map_nsp_fun (name_def false name) >> (fn base => (base, NONE))
| (name, def) => error ("Class block containing illegal def: " ^ quote name)
@@ -1024,6 +982,8 @@
add_group mk_datatype defs
| group_defs ((defs as (_, CodegenThingol.Class _)::_)) =
add_group mk_class defs
+ | group_defs ((defs as (_, CodegenThingol.Classrel _)::_)) =
+ add_group mk_class defs
| group_defs ((defs as (_, CodegenThingol.Classop _)::_)) =
add_group mk_class defs
| group_defs ((defs as [(_, CodegenThingol.Classinst _)])) =
@@ -1270,7 +1230,7 @@
Pretty.block_enclose (
Pretty.block [
str "class ",
- pr_typparms tyvars [(v, superclasss)],
+ pr_typparms tyvars [(v, map fst superclasss)],
str (deresolv_here name ^ " " ^ CodegenNames.lookup_var tyvars v),
str " where {"
],
@@ -1361,14 +1321,16 @@
| CodegenThingol.Datatype _ => add_typ
| CodegenThingol.Datatypecons _ => add_fun true
| CodegenThingol.Class _ => add_typ
+ | CodegenThingol.Classrel _ => pair base
| CodegenThingol.Classop _ => add_fun false
| CodegenThingol.Classinst _ => pair base;
val modlname' = name_modl modl;
fun add_def base' =
case def
of CodegenThingol.Bot => I
- | CodegenThingol.Datatypecons _ => I
+ | CodegenThingol.Datatypecons _ =>
cons (name, ((NameSpace.append modlname' base', base'), NONE))
+ | CodegenThingol.Classrel _ => I
| CodegenThingol.Classop _ =>
cons (name, ((NameSpace.append modlname' base', base'), NONE))
| _ => cons (name, ((NameSpace.append modlname' base', base'), SOME def));
@@ -1766,18 +1728,29 @@
val c'' = CodegenConsts.norm_of_typ thy c';
in (c'', CodegenNames.const thy c'') end;
+fun no_bindings x = (Option.map o apsnd)
+ (fn pretty => fn pr => fn vars => pretty (pr vars)) x;
+
fun gen_add_haskell_monad prep_const c_run c_mbind c_kbind thy =
let
val c_run' =
(CodegenConsts.norm thy o prep_const thy) c_run;
+ val c_mbind' =
+ (CodegenConsts.norm thy o prep_const thy) c_mbind;
val c_mbind'' =
- (CodegenNames.const thy o CodegenConsts.norm thy o prep_const thy) c_mbind;
+ CodegenNames.const thy c_mbind';
+ val c_kbind' =
+ (CodegenConsts.norm thy o prep_const thy) c_kbind;
val c_kbind'' =
- (CodegenNames.const thy o CodegenConsts.norm thy o prep_const thy) c_kbind;
+ CodegenNames.const thy c_kbind';
val pr = pretty_haskell_monad c_mbind'' c_kbind''
in
thy
|> gen_add_syntax_const (K I) target_Haskell c_run' (SOME pr)
+ |> gen_add_syntax_const (K I) target_Haskell c_mbind'
+ (no_bindings (SOME (parse_infix (L, 1) ">>=")))
+ |> gen_add_syntax_const (K I) target_Haskell c_kbind'
+ (no_bindings (SOME (parse_infix (L, 1) ">>")))
end;
val add_syntax_class = gen_add_syntax_class read_class CodegenConsts.read_const;
@@ -1810,9 +1783,6 @@
#-> (fn things => Scan.repeat1 (P.$$$ "(" |-- P.name --
(zip_list things parse_syntax (P.$$$ "and")) --| P.$$$ ")"));
-fun no_bindings x = (Option.map o apsnd)
- (fn pretty => fn pr => fn vars => pretty (pr vars)) x;
-
val (infixK, infixlK, infixrK) = ("infix", "infixl", "infixr");
fun parse_syntax xs =
--- a/src/Pure/Tools/codegen_thingol.ML Tue Jan 16 14:10:26 2007 +0100
+++ b/src/Pure/Tools/codegen_thingol.ML Tue Jan 16 14:10:27 2007 +0100
@@ -16,14 +16,14 @@
signature BASIC_CODEGEN_THINGOL =
sig
type vname = string;
- datatype inst =
- Instance of string * inst list list
- | Context of (class list * int) * (vname * int);
+ datatype dict =
+ DictConst of string * dict list list
+ | DictVar of string list * (vname * (int * int));
datatype itype =
`%% of string * itype list
| ITyVar of vname;
datatype iterm =
- IConst of string * (inst list list * itype)
+ IConst of string * (dict list list * itype)
| IVar of vname
| `$ of iterm * iterm
| `|-> of (vname * itype) * iterm
@@ -51,8 +51,8 @@
val split_let: iterm -> (((iterm * itype) * iterm) * iterm) option;
val unfold_let: iterm -> ((iterm * itype) * iterm) list * iterm;
val unfold_const_app: iterm ->
- ((string * (inst list list * itype)) * iterm list) option;
- val eta_expand: (string * (inst list list * itype)) * iterm list -> int -> iterm;
+ ((string * (dict list list * itype)) * iterm list) option;
+ val eta_expand: (string * (dict list list * itype)) * iterm list -> int -> iterm;
val fold_constnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;
val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;
val fold_unbound_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;
@@ -62,10 +62,11 @@
| Fun of (iterm list * iterm) list * typscheme
| Datatype of (vname * sort) list * (string * itype list) list
| Datatypecons of string
- | Class of class list * (vname * (string * itype) list)
+ | Class of (class * string) list * (vname * (string * itype) list)
| Classop of class
+ | Classrel of class * class
| Classinst of (class * (string * (vname * sort) list))
- * ((class * (string * inst list list)) list
+ * ((class * (string * (string * dict list list))) list
* (string * iterm) list);
type code = def Graph.T;
type transact;
@@ -114,16 +115,16 @@
type vname = string;
-datatype inst =
- Instance of string * inst list list
- | Context of (class list * int) * (vname * int);
+datatype dict =
+ DictConst of string * dict list list
+ | DictVar of string list * (vname * (int * int));
datatype itype =
`%% of string * itype list
| ITyVar of vname;
datatype iterm =
- IConst of string * (inst list list * itype)
+ IConst of string * (dict list list * itype)
| IVar of vname
| `$ of iterm * iterm
| `|-> of (vname * itype) * iterm
@@ -255,10 +256,11 @@
| Fun of (iterm list * iterm) list * typscheme
| Datatype of (vname * sort) list * (string * itype list) list
| Datatypecons of string
- | Class of class list * (vname * (string * itype) list)
+ | Class of (class * string) list * (vname * (string * itype) list)
| Classop of class
+ | Classrel of class * class
| Classinst of (class * (string * (vname * sort) list))
- * ((class * (string * inst list list)) list
+ * ((class * (string * (string * dict list list))) list
* (string * iterm) list);
val eq_def = (op =) : def * def -> bool;
@@ -346,37 +348,40 @@
| check_prep_def code (d as Class _) =
d
| check_prep_def code (Classop _) =
- error "Attempted to add bare class member"
- | check_prep_def code (d as Classinst ((class, (tyco, arity)), (_, memdefs))) =
+ error "Attempted to add bare class operation"
+ | check_prep_def code (Classrel _) =
+ error "Attempted to add bare class relation"
+ | check_prep_def code (d as Classinst ((class, (tyco, arity)), (_, inst_classops))) =
let
- val Class (_, (v, membrs)) = get_def code class;
- val _ = if length memdefs > length memdefs
- then error "Too many member definitions given"
+ val Class (_, (_, classops)) = get_def code class;
+ val _ = if length inst_classops > length classops
+ then error "Too many class operations given"
else ();
- fun check_memdef (m, _) =
- if AList.defined (op =) memdefs m
- then () else error ("Missing definition for member " ^ quote m);
- val _ = map check_memdef memdefs;
- in d end
- | check_prep_def code Classinstmember =
- error "Attempted to add bare class instance member";
+ fun check_classop (f, _) =
+ if AList.defined (op =) inst_classops f
+ then () else error ("Missing definition for class operation " ^ quote f);
+ val _ = map check_classop classops;
+ in d end;
fun postprocess_def (name, Datatype (_, constrs)) =
- (check_samemodule (name :: map fst constrs);
- fold (fn (co, _) =>
+ tap (fn _ => check_samemodule (name :: map fst constrs))
+ #> fold (fn (co, _) =>
add_def_incr true (co, Datatypecons name)
#> add_dep (co, name)
#> add_dep (name, co)
) constrs
- )
- | postprocess_def (name, Class (_, (_, membrs))) =
- (check_samemodule (name :: map fst membrs);
- fold (fn (m, _) =>
- add_def_incr true (m, Classop name)
- #> add_dep (m, name)
- #> add_dep (name, m)
- ) membrs
- )
+ | postprocess_def (name, Class (classrels, (_, classops))) =
+ tap (fn _ => check_samemodule (name :: map fst classops @ map snd classrels))
+ #> fold (fn (f, _) =>
+ add_def_incr true (f, Classop name)
+ #> add_dep (f, name)
+ #> add_dep (name, f)
+ ) classops
+ #> fold (fn (superclass, classrel) =>
+ add_def_incr true (classrel, Classrel (name, superclass))
+ #> add_dep (classrel, name)
+ #> add_dep (name, classrel)
+ ) classrels
| postprocess_def _ =
I;