--- a/src/Tools/Code/code_haskell.ML Fri May 25 17:14:14 2012 +0200
+++ b/src/Tools/Code/code_haskell.ML Mon May 28 13:38:07 2012 +0200
@@ -56,8 +56,8 @@
of NONE => print_tyco_expr tyvars fxy (deresolve tyco, tys)
| SOME (_, print) => print (print_typ tyvars) fxy tys)
| print_typ tyvars fxy (ITyVar v) = (str o lookup_var tyvars) v;
- fun print_typdecl tyvars (vs, tycoexpr) =
- Pretty.block (print_typcontext tyvars vs @| print_tyco_expr tyvars NOBR tycoexpr);
+ fun print_typdecl tyvars (tyco, vs) =
+ print_tyco_expr tyvars NOBR (tyco, map ITyVar vs);
fun print_typscheme tyvars (vs, ty) =
Pretty.block (print_typforall tyvars vs @ print_typcontext tyvars vs @| print_typ tyvars NOBR ty);
fun print_term tyvars some_thm vars fxy (IConst c) =
@@ -163,20 +163,20 @@
end
| print_stmt (name, Code_Thingol.Datatype (_, (vs, []))) =
let
- val tyvars = intro_vars (map fst vs) reserved;
+ val tyvars = intro_vars vs reserved;
in
semicolon [
str "data",
- print_typdecl tyvars (vs, (deresolve name, map (ITyVar o fst) vs))
+ print_typdecl tyvars (deresolve name, vs)
]
end
| print_stmt (name, Code_Thingol.Datatype (_, (vs, [((co, _), [ty])]))) =
let
- val tyvars = intro_vars (map fst vs) reserved;
+ val tyvars = intro_vars vs reserved;
in
semicolon (
str "newtype"
- :: print_typdecl tyvars (vs, (deresolve name, map (ITyVar o fst) vs))
+ :: print_typdecl tyvars (deresolve name, vs)
:: str "="
:: (str o deresolve) co
:: print_typ tyvars BR ty
@@ -185,7 +185,7 @@
end
| print_stmt (name, Code_Thingol.Datatype (_, (vs, co :: cos))) =
let
- val tyvars = intro_vars (map fst vs) reserved;
+ val tyvars = intro_vars vs reserved;
fun print_co ((co, _), tys) =
concat (
(str o deresolve) co
@@ -194,7 +194,7 @@
in
semicolon (
str "data"
- :: print_typdecl tyvars (vs, (deresolve name, map (ITyVar o fst) vs))
+ :: print_typdecl tyvars (deresolve name, vs)
:: str "="
:: print_co co
:: map ((fn p => Pretty.block [str "| ", p]) o print_co) cos
--- a/src/Tools/Code/code_ml.ML Fri May 25 17:14:14 2012 +0200
+++ b/src/Tools/Code/code_ml.ML Mon May 28 13:38:07 2012 +0200
@@ -36,7 +36,7 @@
ML_Exc of string * (typscheme * int)
| ML_Val of ml_binding
| ML_Funs of ml_binding list * string list
- | ML_Datas of (string * ((vname * sort) list * ((string * vname list) * itype list) list)) list
+ | ML_Datas of (string * (vname list * ((string * vname list) * itype list) list)) list
| ML_Class of string * (vname * ((class * string) list * (string * itype) list));
fun print_product _ [] = NONE
@@ -167,7 +167,7 @@
in
concat (
str definer
- :: print_tyco_expr (tyco, map (ITyVar o fst) vs)
+ :: print_tyco_expr (tyco, map ITyVar vs)
:: str "="
:: separate (str "|") (map print_co cos)
)
@@ -273,7 +273,7 @@
end
| print_stmt (ML_Datas [(tyco, (vs, []))]) =
let
- val ty_p = print_tyco_expr (tyco, map (ITyVar o fst) vs);
+ val ty_p = print_tyco_expr (tyco, map ITyVar vs);
in
pair
[concat [str "type", ty_p]]
@@ -462,7 +462,7 @@
in
concat (
str definer
- :: print_tyco_expr (tyco, map (ITyVar o fst) vs)
+ :: print_tyco_expr (tyco, map ITyVar vs)
:: str "="
:: separate (str "|") (map print_co cos)
)
@@ -613,7 +613,7 @@
end
| print_stmt (ML_Datas [(tyco, (vs, []))]) =
let
- val ty_p = print_tyco_expr (tyco, map (ITyVar o fst) vs);
+ val ty_p = print_tyco_expr (tyco, map ITyVar vs);
in
pair
[concat [str "type", ty_p]]
--- a/src/Tools/Code/code_scala.ML Fri May 25 17:14:14 2012 +0200
+++ b/src/Tools/Code/code_scala.ML Mon May 28 13:38:07 2012 +0200
@@ -205,7 +205,7 @@
print_def name (vs, ty) (filter (snd o snd) raw_eqs)
| print_stmt (name, Code_Thingol.Datatype (_, (vs, cos))) =
let
- val tyvars = intro_tyvars vs reserved;
+ val tyvars = intro_tyvars (map (rpair []) vs) reserved;
fun print_co ((co, _), []) =
concat [str "final", str "case", str "object", (str o deresolve) co,
str "extends", applify "[" "]" I NOBR ((str o deresolve) name)
@@ -217,11 +217,11 @@
["final", "case", "class", deresolve co]) vs_args)
(Name.invent_names (snd reserved) "a" tys),
str "extends",
- applify "[" "]" (str o lookup_tyvar tyvars o fst) NOBR
+ applify "[" "]" (str o lookup_tyvar tyvars) NOBR
((str o deresolve) name) vs
];
in
- Pretty.chunks (applify "[" "]" (str o prefix "+" o lookup_tyvar tyvars o fst)
+ Pretty.chunks (applify "[" "]" (str o prefix "+" o lookup_tyvar tyvars)
NOBR ((concat o map str) ["abstract", "sealed", "class", deresolve name]) vs
:: map print_co cos)
end
--- a/src/Tools/Code/code_thingol.ML Fri May 25 17:14:14 2012 +0200
+++ b/src/Tools/Code/code_thingol.ML Mon May 28 13:38:07 2012 +0200
@@ -71,7 +71,7 @@
datatype stmt =
NoStmt
| Fun of string * ((typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option)
- | Datatype of string * ((vname * sort) list *
+ | Datatype of string * (vname list *
((string * vname list (*type argument wrt. canonical order*)) * itype list) list)
| Datatypecons of string * string
| Class of class * (vname * ((class * string) list * (string * itype) list))
@@ -422,7 +422,7 @@
datatype stmt =
NoStmt
| Fun of string * ((typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option)
- | Datatype of string * ((vname * sort) list * ((string * vname list) * itype list) list)
+ | Datatype of string * (vname list * ((string * vname list) * itype list) list)
| Datatypecons of string * string
| Class of class * (vname * ((class * string) list * (string * itype) list))
| Classrel of class * class
@@ -625,6 +625,7 @@
val ((vs, cos), _) = Code.get_type thy tyco;
val stmt_datatype =
fold_map (translate_tyvar_sort thy algbr eqngr permissive) vs
+ #>> map fst
##>> fold_map (fn (c, (vs, tys)) =>
ensure_const thy algbr eqngr permissive c
##>> pair (map (unprefix "'" o fst) vs)