--- a/src/Tools/Code/code_haskell.ML Sat Jan 25 23:50:49 2014 +0100
+++ b/src/Tools/Code/code_haskell.ML Sat Jan 25 23:50:49 2014 +0100
@@ -37,8 +37,11 @@
fun print_haskell_stmt class_syntax tyco_syntax const_syntax
reserved deresolve deriving_show =
let
+ val deresolve_const = deresolve o Code_Symbol.Constant;
+ val deresolve_tyco = deresolve o Code_Symbol.Type_Constructor;
+ val deresolve_class = deresolve o Code_Symbol.Type_Class;
fun class_name class = case class_syntax class
- of NONE => deresolve class
+ of NONE => deresolve_class class
| SOME class => class;
fun print_typcontext tyvars vs = case maps (fn (v, sort) => map (pair v) sort) vs
of [] => []
@@ -53,7 +56,7 @@
fun print_tyco_expr tyvars fxy (tyco, tys) =
brackify fxy (str tyco :: map (print_typ tyvars BR) tys)
and print_typ tyvars fxy (tyco `%% tys) = (case tyco_syntax tyco
- of NONE => print_tyco_expr tyvars fxy (deresolve tyco, tys)
+ of NONE => print_tyco_expr tyvars fxy (deresolve_tyco 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 (tyco, vs) =
@@ -81,18 +84,19 @@
in brackets (str "\\" :: ps @ str "->" @@ print_term tyvars some_thm vars' NOBR t') end
| print_term tyvars some_thm vars fxy (ICase case_expr) =
(case Code_Thingol.unfold_const_app (#primitive case_expr)
- of SOME (app as ({ name = c, ... }, _)) => if is_none (const_syntax c)
+ of SOME (app as ({ sym = Code_Symbol.Constant const, ... }, _)) =>
+ if is_none (const_syntax const)
then print_case tyvars some_thm vars fxy case_expr
else print_app tyvars some_thm vars fxy app
| NONE => print_case tyvars some_thm vars fxy case_expr)
- and print_app_expr tyvars some_thm vars ({ name = c, dom, range, annotate, ... }, ts) =
+ and print_app_expr tyvars some_thm vars ({ sym, dom, range, annotate, ... }, ts) =
let
- val ty = Library.foldr (fn (ty1, ty2) => Code_Thingol.fun_tyco `%% [ty1, ty2]) (dom, range)
+ val ty = Library.foldr (op `->) (dom, range)
val printed_const =
if annotate then
- brackets [(str o deresolve) c, str "::", print_typ tyvars NOBR ty]
+ brackets [(str o deresolve) sym, str "::", print_typ tyvars NOBR ty]
else
- (str o deresolve) c
+ (str o deresolve) sym
in
printed_const :: map (print_term tyvars some_thm vars BR) ts
end
@@ -122,17 +126,16 @@
(concat [str "(case", print_term tyvars some_thm vars NOBR t, str "of", str "{"], str "})")
(map print_select clauses)
end;
- fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) =
+ fun print_stmt (Code_Symbol.Constant const, Code_Thingol.Fun (((vs, ty), raw_eqs), _)) =
let
val tyvars = intro_vars (map fst vs) reserved;
fun print_err n =
- semicolon (
- (str o deresolve) name
- :: map str (replicate n "_")
- @ str "="
- :: str "error"
- @@ (str o ML_Syntax.print_string
- o Long_Name.base_name o Long_Name.qualifier) name
+ (semicolon o map str) (
+ deresolve_const const
+ :: replicate n "_"
+ @ "="
+ :: "error"
+ @@ ML_Syntax.print_string const
);
fun print_eqn ((ts, t), (some_thm, _)) =
let
@@ -143,7 +146,7 @@
(insert (op =)) ts []);
in
semicolon (
- (str o deresolve) name
+ (str o deresolve_const) const
:: map (print_term tyvars some_thm vars BR) ts
@ str "="
@@ print_term tyvars some_thm vars NOBR t
@@ -152,7 +155,7 @@
in
Pretty.chunks (
semicolon [
- (str o suffix " ::" o deresolve) name,
+ (str o suffix " ::" o deresolve_const) const,
print_typscheme tyvars (vs, ty)
]
:: (case filter (snd o snd) raw_eqs
@@ -160,52 +163,52 @@
| eqs => map print_eqn eqs)
)
end
- | print_stmt (name, Code_Thingol.Datatype (_, (vs, []))) =
+ | print_stmt (Code_Symbol.Type_Constructor tyco, Code_Thingol.Datatype (vs, [])) =
let
val tyvars = intro_vars vs reserved;
in
semicolon [
str "data",
- print_typdecl tyvars (deresolve name, vs)
+ print_typdecl tyvars (deresolve_tyco tyco, vs)
]
end
- | print_stmt (name, Code_Thingol.Datatype (_, (vs, [((co, _), [ty])]))) =
+ | print_stmt (Code_Symbol.Type_Constructor tyco, Code_Thingol.Datatype (vs, [((co, _), [ty])])) =
let
val tyvars = intro_vars vs reserved;
in
semicolon (
str "newtype"
- :: print_typdecl tyvars (deresolve name, vs)
+ :: print_typdecl tyvars (deresolve_tyco tyco, vs)
:: str "="
- :: (str o deresolve) co
+ :: (str o deresolve_const) co
:: print_typ tyvars BR ty
- :: (if deriving_show name then [str "deriving (Read, Show)"] else [])
+ :: (if deriving_show tyco then [str "deriving (Read, Show)"] else [])
)
end
- | print_stmt (name, Code_Thingol.Datatype (_, (vs, co :: cos))) =
+ | print_stmt (Code_Symbol.Type_Constructor tyco, Code_Thingol.Datatype (vs, co :: cos)) =
let
val tyvars = intro_vars vs reserved;
fun print_co ((co, _), tys) =
concat (
- (str o deresolve) co
+ (str o deresolve_const) co
:: map (print_typ tyvars BR) tys
)
in
semicolon (
str "data"
- :: print_typdecl tyvars (deresolve name, vs)
+ :: print_typdecl tyvars (deresolve_tyco tyco, vs)
:: str "="
:: print_co co
:: map ((fn p => Pretty.block [str "| ", p]) o print_co) cos
- @ (if deriving_show name then [str "deriving (Read, Show)"] else [])
+ @ (if deriving_show tyco then [str "deriving (Read, Show)"] else [])
)
end
- | print_stmt (name, Code_Thingol.Class (_, (v, (super_classes, classparams)))) =
+ | print_stmt (Code_Symbol.Type_Class class, Code_Thingol.Class (v, (classrels, classparams))) =
let
val tyvars = intro_vars [v] reserved;
fun print_classparam (classparam, ty) =
semicolon [
- (str o deresolve) classparam,
+ (str o deresolve_const) classparam,
str "::",
print_typ tyvars NOBR ty
]
@@ -213,8 +216,8 @@
Pretty.block_enclose (
Pretty.block [
str "class ",
- Pretty.block (print_typcontext tyvars [(v, map fst super_classes)]),
- str (deresolve name ^ " " ^ lookup_var tyvars v),
+ Pretty.block (print_typcontext tyvars [(v, map snd classrels)]),
+ str (deresolve_class class ^ " " ^ lookup_var tyvars v),
str " where {"
],
str "};"
@@ -230,20 +233,20 @@
fun print_classparam_instance ((classparam, (const, _)), (thm, _)) =
case requires_args classparam
of NONE => semicolon [
- (str o Long_Name.base_name o deresolve) classparam,
+ (str o Long_Name.base_name o deresolve_const) classparam,
str "=",
print_app tyvars (SOME thm) reserved NOBR (const, [])
]
| SOME k =>
let
- val { name = c, dom, range, ... } = const;
+ val { sym = Code_Symbol.Constant c, dom, range, ... } = const;
val (vs, rhs) = (apfst o map) fst
(Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, [])));
val s = if (is_some o const_syntax) c
- then NONE else (SOME o Long_Name.base_name o deresolve) c;
+ then NONE else (SOME o Long_Name.base_name o deresolve_const) c;
val vars = reserved
|> intro_vars (map_filter I (s :: vs));
- val lhs = IConst { name = classparam, typargs = [],
+ val lhs = IConst { sym = Code_Symbol.Constant classparam, typargs = [],
dicts = [], dom = dom, range = range, annotate = false } `$$ map IVar vs;
(*dictionaries are not relevant at this late stage,
and these consts never need type annotations for disambiguation *)
@@ -268,7 +271,7 @@
end;
in print_stmt end;
-fun haskell_program_of_program ctxt symbol_of module_prefix module_name reserved identifiers =
+fun haskell_program_of_program ctxt module_prefix module_name reserved identifiers =
let
fun namify_fun upper base (nsp_fun, nsp_typ) =
let
@@ -279,7 +282,7 @@
let
val (base', nsp_typ') = Name.variant (first_upper base) nsp_typ;
in (base', (nsp_fun, nsp_typ')) end;
- fun namify_stmt (Code_Thingol.Fun (_, (_, SOME _))) = pair
+ fun namify_stmt (Code_Thingol.Fun (_, SOME _)) = pair
| namify_stmt (Code_Thingol.Fun _) = namify_fun false
| namify_stmt (Code_Thingol.Datatype _) = namify_typ
| namify_stmt (Code_Thingol.Datatypecons _) = namify_fun true
@@ -287,7 +290,7 @@
| namify_stmt (Code_Thingol.Classrel _) = pair
| namify_stmt (Code_Thingol.Classparam _) = namify_fun false
| namify_stmt (Code_Thingol.Classinst _) = pair;
- fun select_stmt (Code_Thingol.Fun (_, (_, SOME _))) = false
+ fun select_stmt (Code_Thingol.Fun (_, SOME _)) = false
| select_stmt (Code_Thingol.Fun _) = true
| select_stmt (Code_Thingol.Datatype _) = true
| select_stmt (Code_Thingol.Datatypecons _) = false
@@ -296,7 +299,7 @@
| select_stmt (Code_Thingol.Classparam _) = false
| select_stmt (Code_Thingol.Classinst _) = true;
in
- Code_Namespace.flat_program ctxt symbol_of
+ Code_Namespace.flat_program ctxt
{ module_prefix = module_prefix, module_name = module_name, reserved = reserved,
identifiers = identifiers, empty_nsp = (reserved, reserved), namify_stmt = namify_stmt,
modify_stmt = fn stmt => if select_stmt stmt then SOME stmt else NONE }
@@ -323,25 +326,24 @@
("Maybe", ["Nothing", "Just"])
];
-fun serialize_haskell module_prefix string_classes ctxt { symbol_of, module_name,
+fun serialize_haskell module_prefix string_classes ctxt { module_name,
reserved_syms, identifiers, includes, class_syntax, tyco_syntax, const_syntax } program =
let
(* build program *)
val reserved = fold (insert (op =) o fst) includes reserved_syms;
val { deresolver, flat_program = haskell_program } = haskell_program_of_program
- ctxt symbol_of module_prefix module_name (Name.make_context reserved) identifiers program;
+ ctxt module_prefix module_name (Name.make_context reserved) identifiers program;
(* print statements *)
fun deriving_show tyco =
let
fun deriv _ "fun" = false
- | deriv tycos tyco = not (tyco = Code_Thingol.fun_tyco)
- andalso (member (op =) tycos tyco
- orelse case try (Graph.get_node program) tyco
- of SOME (Code_Thingol.Datatype (_, (_, cs))) => forall (deriv' (tyco :: tycos))
+ | deriv tycos tyco = member (op =) tycos tyco
+ orelse case try (Code_Symbol.Graph.get_node program) (Code_Symbol.Type_Constructor tyco)
+ of SOME (Code_Thingol.Datatype (_, cs)) => forall (deriv' (tyco :: tycos))
(maps snd cs)
- | NONE => true)
+ | NONE => true
and deriv' tycos (tyco `%% tys) = deriv tycos tyco
andalso forall (deriv' tycos) tys
| deriv' _ (ITyVar _) = true
@@ -369,10 +371,10 @@
val deresolve = deresolver module_name;
fun print_import module_name = (semicolon o map str) ["import qualified", module_name];
val import_ps = import_common_ps @ map (print_qualified_import o fst) imports;
- fun print_stmt' name = case Graph.get_node gr name
+ fun print_stmt' sym = case Code_Symbol.Graph.get_node gr sym
of (_, NONE) => NONE
- | (_, SOME stmt) => SOME (markup_stmt name (print_stmt deresolve (name, stmt)));
- val body_ps = map_filter print_stmt' ((flat o rev o Graph.strong_conn) gr);
+ | (_, SOME stmt) => SOME (markup_stmt sym (print_stmt deresolve (sym, stmt)));
+ val body_ps = map_filter print_stmt' ((flat o rev o Code_Symbol.Graph.strong_conn) gr);
in
print_module_frame module_name
((if null import_ps then [] else [Pretty.chunks import_ps]) @ body_ps)
@@ -430,7 +432,7 @@
of SOME ((pat, ty), t') =>
SOME ((SOME ((pat, ty), true), t1), t')
| NONE => NONE;
- fun dest_monad c_bind_name (IConst { name = c, ... } `$ t1 `$ t2) =
+ fun dest_monad c_bind_name (IConst { sym = Code_Symbol.Constant c, ... } `$ t1 `$ t2) =
if c = c_bind_name then dest_bind t1 t2
else NONE
| dest_monad _ t = case Code_Thingol.split_let t