# HG changeset patch # User haftmann # Date 1338205087 -7200 # Node ID 1d11af40b106fe5dde11c29112a17d8926635cbb # Parent 6de952f4069f54a342fa986411816028f9c4b276 dropped sort constraints on datatype specifications diff -r 6de952f4069f -r 1d11af40b106 src/Tools/Code/code_haskell.ML --- 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 diff -r 6de952f4069f -r 1d11af40b106 src/Tools/Code/code_ml.ML --- 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]] diff -r 6de952f4069f -r 1d11af40b106 src/Tools/Code/code_scala.ML --- 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 diff -r 6de952f4069f -r 1d11af40b106 src/Tools/Code/code_thingol.ML --- 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)