--- a/src/Tools/Code/code_ml.ML Sat Jan 25 23:50:49 2014 +0100
+++ b/src/Tools/Code/code_ml.ML Sat Jan 25 23:50:49 2014 +0100
@@ -28,17 +28,17 @@
datatype ml_binding =
ML_Function of string * (typscheme * ((iterm list * iterm) * (thm option * bool)) list)
- | ML_Instance of string * { class: string, tyco: string, vs: (vname * sort) list,
- superinsts: (class * (string * (string * dict list list))) list,
+ | ML_Instance of (string * class) * { class: class, tyco: string, vs: (vname * sort) list,
+ superinsts: (class * dict list list) list,
inst_params: ((string * (const * int)) * (thm * bool)) list,
superinst_params: ((string * (const * int)) * (thm * bool)) list };
datatype ml_stmt =
ML_Exc of string * (typscheme * int)
| ML_Val of ml_binding
- | ML_Funs of ml_binding list * string list
+ | ML_Funs of ml_binding list * Code_Symbol.symbol 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));
+ | ML_Class of string * (vname * ((class * class) list * (string * itype) list));
fun print_product _ [] = NONE
| print_product print [x] = SOME (print x)
@@ -53,30 +53,35 @@
fun print_sml_stmt tyco_syntax const_syntax reserved is_constr deresolve =
let
- fun print_tyco_expr (tyco, []) = (str o deresolve) tyco
- | print_tyco_expr (tyco, [ty]) =
- concat [print_typ BR ty, (str o deresolve) tyco]
- | print_tyco_expr (tyco, tys) =
- concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco]
+ 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;
+ val deresolve_classrel = deresolve o Code_Symbol.Class_Relation;
+ val deresolve_inst = deresolve o Code_Symbol.Class_Instance;
+ fun print_tyco_expr (sym, []) = (str o deresolve) sym
+ | print_tyco_expr (sym, [ty]) =
+ concat [print_typ BR ty, (str o deresolve) sym]
+ | print_tyco_expr (sym, tys) =
+ concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) sym]
and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco
- of NONE => print_tyco_expr (tyco, tys)
+ of NONE => print_tyco_expr (Code_Symbol.Type_Constructor tyco, tys)
| SOME (_, print) => print print_typ fxy tys)
| print_typ fxy (ITyVar v) = str ("'" ^ v);
- fun print_dicttyp (class, ty) = print_tyco_expr (class, [ty]);
+ fun print_dicttyp (class, ty) = print_tyco_expr (Code_Symbol.Type_Class class, [ty]);
fun print_typscheme_prefix (vs, p) = enum " ->" "" ""
(map_filter (fn (v, sort) =>
(print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p);
fun print_typscheme (vs, ty) = print_typscheme_prefix (vs, print_typ NOBR ty);
fun print_dicttypscheme (vs, class_ty) = print_typscheme_prefix (vs, print_dicttyp class_ty);
fun print_classrels fxy [] ps = brackify fxy ps
- | print_classrels fxy [classrel] ps = brackify fxy [(str o deresolve) classrel, brackify BR ps]
+ | print_classrels fxy [classrel] ps = brackify fxy [(str o deresolve_classrel) classrel, brackify BR ps]
| print_classrels fxy classrels ps =
- brackify fxy [enum " o" "(" ")" (map (str o deresolve) classrels), brackify BR ps]
+ brackify fxy [enum " o" "(" ")" (map (str o deresolve_classrel) classrels), brackify BR ps]
fun print_dict is_pseudo_fun fxy (Dict (classrels, x)) =
print_classrels fxy classrels (print_plain_dict is_pseudo_fun fxy x)
and print_plain_dict is_pseudo_fun fxy (Dict_Const (inst, dss)) =
- ((str o deresolve) inst ::
- (if is_pseudo_fun inst then [str "()"]
+ ((str o deresolve_inst) inst ::
+ (if is_pseudo_fun (Code_Symbol.Class_Instance inst) then [str "()"]
else map_filter (print_dicts is_pseudo_fun BR) dss))
| print_plain_dict is_pseudo_fun fxy (Dict_Var (v, (i, k))) =
[str (if k = 1 then first_upper v ^ "_"
@@ -105,21 +110,22 @@
in brackets (ps @ [print_term is_pseudo_fun some_thm vars' NOBR t']) end
| print_term is_pseudo_fun 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 is_pseudo_fun some_thm vars fxy case_expr
else print_app is_pseudo_fun some_thm vars fxy app
| NONE => print_case is_pseudo_fun some_thm vars fxy case_expr)
- and print_app_expr is_pseudo_fun some_thm vars (app as ({ name = c, dicts = dss, dom = dom, ... }, ts)) =
- if is_constr c then
+ and print_app_expr is_pseudo_fun some_thm vars (app as ({ sym, dicts = dss, dom = dom, ... }, ts)) =
+ if is_constr sym then
let val k = length dom in
if k < 2 orelse length ts = k
- then (str o deresolve) c
+ then (str o deresolve) sym
:: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts)
else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.eta_expand k app)]
end
- else if is_pseudo_fun c
- then (str o deresolve) c @@ str "()"
- else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) dss
+ else if is_pseudo_fun sym
+ then (str o deresolve) sym @@ str "()"
+ else (str o deresolve) sym :: map_filter (print_dicts is_pseudo_fun BR) dss
@ map (print_term is_pseudo_fun some_thm vars BR) ts
and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun)
(print_term is_pseudo_fun) const_syntax some_thm vars
@@ -158,23 +164,23 @@
:: map (print_select "|") clauses
)
end;
- fun print_val_decl print_typscheme (name, typscheme) = concat
- [str "val", str (deresolve name), str ":", print_typscheme typscheme];
+ fun print_val_decl print_typscheme (sym, typscheme) = concat
+ [str "val", str (deresolve sym), str ":", print_typscheme typscheme];
fun print_datatype_decl definer (tyco, (vs, cos)) =
let
- fun print_co ((co, _), []) = str (deresolve co)
- | print_co ((co, _), tys) = concat [str (deresolve co), str "of",
+ fun print_co ((co, _), []) = str (deresolve_const co)
+ | print_co ((co, _), tys) = concat [str (deresolve_const co), str "of",
enum " *" "" "" (map (print_typ (INFX (2, X))) tys)];
in
concat (
str definer
- :: print_tyco_expr (tyco, map ITyVar vs)
+ :: print_tyco_expr (Code_Symbol.Type_Constructor tyco, map ITyVar vs)
:: str "="
:: separate (str "|") (map print_co cos)
)
end;
fun print_def is_pseudo_fun needs_typ definer
- (ML_Function (name, (vs_ty as (vs, ty), eq :: eqs))) =
+ (ML_Function (const, (vs_ty as (vs, ty), eq :: eqs))) =
let
fun print_eqn definer ((ts, t), (some_thm, _)) =
let
@@ -184,12 +190,12 @@
|> intro_vars ((fold o Code_Thingol.fold_varnames)
(insert (op =)) ts []);
val prolog = if needs_typ then
- concat [str definer, (str o deresolve) name, str ":", print_typ NOBR ty]
- else (concat o map str) [definer, deresolve name];
+ concat [str definer, (str o deresolve_const) const, str ":", print_typ NOBR ty]
+ else (concat o map str) [definer, deresolve_const const];
in
concat (
prolog
- :: (if is_pseudo_fun name then [str "()"]
+ :: (if is_pseudo_fun (Code_Symbol.Constant const) then [str "()"]
else print_dict_args vs
@ map (print_term is_pseudo_fun some_thm vars BR) ts)
@ str "="
@@ -199,53 +205,53 @@
val shift = if null eqs then I else
map (Pretty.block o single o Pretty.block o single);
in pair
- (print_val_decl print_typscheme (name, vs_ty))
+ (print_val_decl print_typscheme (Code_Symbol.Constant const, vs_ty))
((Pretty.block o Pretty.fbreaks o shift) (
print_eqn definer eq
:: map (print_eqn "|") eqs
))
end
| print_def is_pseudo_fun _ definer
- (ML_Instance (inst, { class, tyco, vs, superinsts, inst_params, ... })) =
+ (ML_Instance (inst as (tyco, class), { vs, superinsts, inst_params, ... })) =
let
- fun print_super_instance (_, (classrel, x)) =
+ fun print_super_instance (super_class, x) =
concat [
- (str o Long_Name.base_name o deresolve) classrel,
+ (str o Long_Name.base_name o deresolve_classrel) (class, super_class),
str "=",
- print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const x))
+ print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const ((tyco, super_class), x)))
];
fun print_classparam_instance ((classparam, (const, _)), (thm, _)) =
concat [
- (str o Long_Name.base_name o deresolve) classparam,
+ (str o Long_Name.base_name o deresolve_const) classparam,
str "=",
print_app (K false) (SOME thm) reserved NOBR (const, [])
];
in pair
(print_val_decl print_dicttypscheme
- (inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
+ (Code_Symbol.Class_Instance inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
(concat (
str definer
- :: (str o deresolve) inst
- :: (if is_pseudo_fun inst then [str "()"]
+ :: (str o deresolve_inst) inst
+ :: (if is_pseudo_fun (Code_Symbol.Class_Instance inst) then [str "()"]
else print_dict_args vs)
@ str "="
:: enum "," "{" "}"
(map print_super_instance superinsts
@ map print_classparam_instance inst_params)
:: str ":"
- @@ print_tyco_expr (class, [tyco `%% map (ITyVar o fst) vs])
+ @@ print_dicttyp (class, tyco `%% map (ITyVar o fst) vs)
))
end;
- fun print_stmt (ML_Exc (name, (vs_ty, n))) = pair
- [print_val_decl print_typscheme (name, vs_ty)]
+ fun print_stmt (ML_Exc (const, (vs_ty, n))) = pair
+ [print_val_decl print_typscheme (Code_Symbol.Constant const, vs_ty)]
((semicolon o map str) (
(if n = 0 then "val" else "fun")
- :: deresolve name
+ :: deresolve_const const
:: replicate n "_"
@ "="
:: "raise"
:: "Fail"
- @@ (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name
+ @@ ML_Syntax.print_string const
))
| print_stmt (ML_Val binding) =
let
@@ -257,11 +263,11 @@
| print_stmt (ML_Funs (binding :: bindings, pseudo_funs)) =
let
val print_def' = print_def (member (op =) pseudo_funs) false;
- fun print_pseudo_fun name = concat [
+ fun print_pseudo_fun sym = concat [
str "val",
- (str o deresolve) name,
+ (str o deresolve) sym,
str "=",
- (str o deresolve) name,
+ (str o deresolve) sym,
str "();"
];
val (sig_ps, (ps, p)) = (apsnd split_last o split_list)
@@ -273,7 +279,7 @@
end
| print_stmt (ML_Datas [(tyco, (vs, []))]) =
let
- val ty_p = print_tyco_expr (tyco, map ITyVar vs);
+ val ty_p = print_tyco_expr (Code_Symbol.Type_Constructor tyco, map ITyVar vs);
in
pair
[concat [str "type", ty_p]]
@@ -288,42 +294,42 @@
sig_ps
(Pretty.chunks (ps @| semicolon [p]))
end
- | print_stmt (ML_Class (class, (v, (super_classes, classparams)))) =
+ | print_stmt (ML_Class (class, (v, (classrels, classparams)))) =
let
fun print_field s p = concat [str s, str ":", p];
fun print_proj s p = semicolon
(map str ["val", s, "=", "#" ^ s, ":"] @| p);
- fun print_super_class_decl (super_class, classrel) =
+ fun print_super_class_decl (classrel as (_, super_class)) =
print_val_decl print_dicttypscheme
- (classrel, ([(v, [class])], (super_class, ITyVar v)));
- fun print_super_class_field (super_class, classrel) =
- print_field (deresolve classrel) (print_dicttyp (super_class, ITyVar v));
- fun print_super_class_proj (super_class, classrel) =
- print_proj (deresolve classrel)
+ (Code_Symbol.Class_Relation classrel, ([(v, [class])], (super_class, ITyVar v)));
+ fun print_super_class_field (classrel as (_, super_class)) =
+ print_field (deresolve_classrel classrel) (print_dicttyp (super_class, ITyVar v));
+ fun print_super_class_proj (classrel as (_, super_class)) =
+ print_proj (deresolve_classrel classrel)
(print_dicttypscheme ([(v, [class])], (super_class, ITyVar v)));
fun print_classparam_decl (classparam, ty) =
print_val_decl print_typscheme
- (classparam, ([(v, [class])], ty));
+ (Code_Symbol.Constant classparam, ([(v, [class])], ty));
fun print_classparam_field (classparam, ty) =
- print_field (deresolve classparam) (print_typ NOBR ty);
+ print_field (deresolve_const classparam) (print_typ NOBR ty);
fun print_classparam_proj (classparam, ty) =
- print_proj (deresolve classparam)
+ print_proj (deresolve_const classparam)
(print_typscheme ([(v, [class])], ty));
in pair
(concat [str "type", print_dicttyp (class, ITyVar v)]
- :: map print_super_class_decl super_classes
+ :: map print_super_class_decl classrels
@ map print_classparam_decl classparams)
(Pretty.chunks (
concat [
str ("type '" ^ v),
- (str o deresolve) class,
+ (str o deresolve_class) class,
str "=",
enum "," "{" "};" (
- map print_super_class_field super_classes
+ map print_super_class_field classrels
@ map print_classparam_field classparams
)
]
- :: map print_super_class_proj super_classes
+ :: map print_super_class_proj classrels
@ map print_classparam_proj classparams
))
end;
@@ -353,29 +359,34 @@
fun print_ocaml_stmt tyco_syntax const_syntax reserved is_constr deresolve =
let
- fun print_tyco_expr (tyco, []) = (str o deresolve) tyco
- | print_tyco_expr (tyco, [ty]) =
- concat [print_typ BR ty, (str o deresolve) tyco]
- | print_tyco_expr (tyco, tys) =
- concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco]
+ 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;
+ val deresolve_classrel = deresolve o Code_Symbol.Class_Relation;
+ val deresolve_inst = deresolve o Code_Symbol.Class_Instance;
+ fun print_tyco_expr (sym, []) = (str o deresolve) sym
+ | print_tyco_expr (sym, [ty]) =
+ concat [print_typ BR ty, (str o deresolve) sym]
+ | print_tyco_expr (sym, tys) =
+ concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) sym]
and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco
- of NONE => print_tyco_expr (tyco, tys)
+ of NONE => print_tyco_expr (Code_Symbol.Type_Constructor tyco, tys)
| SOME (_, print) => print print_typ fxy tys)
| print_typ fxy (ITyVar v) = str ("'" ^ v);
- fun print_dicttyp (class, ty) = print_tyco_expr (class, [ty]);
+ fun print_dicttyp (class, ty) = print_tyco_expr (Code_Symbol.Type_Class class, [ty]);
fun print_typscheme_prefix (vs, p) = enum " ->" "" ""
(map_filter (fn (v, sort) =>
(print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p);
fun print_typscheme (vs, ty) = print_typscheme_prefix (vs, print_typ NOBR ty);
fun print_dicttypscheme (vs, class_ty) = print_typscheme_prefix (vs, print_dicttyp class_ty);
val print_classrels =
- fold_rev (fn classrel => fn p => Pretty.block [p, str ".", (str o deresolve) classrel])
+ fold_rev (fn classrel => fn p => Pretty.block [p, str ".", (str o deresolve_classrel) classrel])
fun print_dict is_pseudo_fun fxy (Dict (classrels, x)) =
print_plain_dict is_pseudo_fun fxy x
|> print_classrels classrels
and print_plain_dict is_pseudo_fun fxy (Dict_Const (inst, dss)) =
- brackify BR ((str o deresolve) inst ::
- (if is_pseudo_fun inst then [str "()"]
+ brackify BR ((str o deresolve_inst) inst ::
+ (if is_pseudo_fun (Code_Symbol.Class_Instance inst) then [str "()"]
else map_filter (print_dicts is_pseudo_fun BR) dss))
| print_plain_dict is_pseudo_fun fxy (Dict_Var (v, (i, k))) =
str (if k = 1 then "_" ^ first_upper v
@@ -401,21 +412,22 @@
in brackets (str "fun" :: ps @ str "->" @@ print_term is_pseudo_fun some_thm vars' NOBR t') end
| print_term is_pseudo_fun 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 is_pseudo_fun some_thm vars fxy case_expr
else print_app is_pseudo_fun some_thm vars fxy app
| NONE => print_case is_pseudo_fun some_thm vars fxy case_expr)
- and print_app_expr is_pseudo_fun some_thm vars (app as ({ name = c, dicts = dss, dom = dom, ... }, ts)) =
- if is_constr c then
+ and print_app_expr is_pseudo_fun some_thm vars (app as ({ sym, dicts = dss, dom = dom, ... }, ts)) =
+ if is_constr sym then
let val k = length dom in
if length ts = k
- then (str o deresolve) c
+ then (str o deresolve) sym
:: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts)
else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.eta_expand k app)]
end
- else if is_pseudo_fun c
- then (str o deresolve) c @@ str "()"
- else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) dss
+ else if is_pseudo_fun sym
+ then (str o deresolve) sym @@ str "()"
+ else (str o deresolve) sym :: map_filter (print_dicts is_pseudo_fun BR) dss
@ map (print_term is_pseudo_fun some_thm vars BR) ts
and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun)
(print_term is_pseudo_fun) const_syntax some_thm vars
@@ -449,23 +461,23 @@
:: map (print_select "|") clauses
)
end;
- fun print_val_decl print_typscheme (name, typscheme) = concat
- [str "val", str (deresolve name), str ":", print_typscheme typscheme];
+ fun print_val_decl print_typscheme (sym, typscheme) = concat
+ [str "val", str (deresolve sym), str ":", print_typscheme typscheme];
fun print_datatype_decl definer (tyco, (vs, cos)) =
let
- fun print_co ((co, _), []) = str (deresolve co)
- | print_co ((co, _), tys) = concat [str (deresolve co), str "of",
+ fun print_co ((co, _), []) = str (deresolve_const co)
+ | print_co ((co, _), tys) = concat [str (deresolve_const co), str "of",
enum " *" "" "" (map (print_typ (INFX (2, X))) tys)];
in
concat (
str definer
- :: print_tyco_expr (tyco, map ITyVar vs)
+ :: print_tyco_expr (Code_Symbol.Type_Constructor tyco, map ITyVar vs)
:: str "="
:: separate (str "|") (map print_co cos)
)
end;
fun print_def is_pseudo_fun needs_typ definer
- (ML_Function (name, (vs_ty as (vs, ty), eqs))) =
+ (ML_Function (const, (vs_ty as (vs, ty), eqs))) =
let
fun print_eqn ((ts, t), (some_thm, _)) =
let
@@ -529,57 +541,57 @@
)
end;
val prolog = if needs_typ then
- concat [str definer, (str o deresolve) name, str ":", print_typ NOBR ty]
- else (concat o map str) [definer, deresolve name];
+ concat [str definer, (str o deresolve_const) const, str ":", print_typ NOBR ty]
+ else (concat o map str) [definer, deresolve_const const];
in pair
- (print_val_decl print_typscheme (name, vs_ty))
+ (print_val_decl print_typscheme (Code_Symbol.Constant const, vs_ty))
(concat (
prolog
:: print_dict_args vs
- @| print_eqns (is_pseudo_fun name) eqs
+ @| print_eqns (is_pseudo_fun (Code_Symbol.Constant const)) eqs
))
end
| print_def is_pseudo_fun _ definer
- (ML_Instance (inst, { class, tyco, vs, superinsts, inst_params, ... })) =
+ (ML_Instance (inst as (tyco, class), { vs, superinsts, inst_params, ... })) =
let
- fun print_super_instance (_, (classrel, x)) =
+ fun print_super_instance (super_class, x) =
concat [
- (str o deresolve) classrel,
+ (str o deresolve_classrel) (class, super_class),
str "=",
- print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const x))
+ print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const ((tyco, super_class), x)))
];
fun print_classparam_instance ((classparam, (const, _)), (thm, _)) =
concat [
- (str o deresolve) classparam,
+ (str o deresolve_const) classparam,
str "=",
print_app (K false) (SOME thm) reserved NOBR (const, [])
];
in pair
(print_val_decl print_dicttypscheme
- (inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
+ (Code_Symbol.Class_Instance inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
(concat (
str definer
- :: (str o deresolve) inst
- :: (if is_pseudo_fun inst then [str "()"]
+ :: (str o deresolve_inst) inst
+ :: (if is_pseudo_fun (Code_Symbol.Class_Instance inst) then [str "()"]
else print_dict_args vs)
@ str "="
@@ brackets [
enum_default "()" ";" "{" "}" (map print_super_instance superinsts
@ map print_classparam_instance inst_params),
str ":",
- print_tyco_expr (class, [tyco `%% map (ITyVar o fst) vs])
+ print_dicttyp (class, tyco `%% map (ITyVar o fst) vs)
]
))
end;
- fun print_stmt (ML_Exc (name, (vs_ty, n))) = pair
- [print_val_decl print_typscheme (name, vs_ty)]
+ fun print_stmt (ML_Exc (const, (vs_ty, n))) = pair
+ [print_val_decl print_typscheme (Code_Symbol.Constant const, vs_ty)]
((doublesemicolon o map str) (
"let"
- :: deresolve name
+ :: deresolve_const const
:: replicate n "_"
@ "="
:: "failwith"
- @@ (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name
+ @@ ML_Syntax.print_string const
))
| print_stmt (ML_Val binding) =
let
@@ -591,11 +603,11 @@
| print_stmt (ML_Funs (binding :: bindings, pseudo_funs)) =
let
val print_def' = print_def (member (op =) pseudo_funs) false;
- fun print_pseudo_fun name = concat [
+ fun print_pseudo_fun sym = concat [
str "let",
- (str o deresolve) name,
+ (str o deresolve) sym,
str "=",
- (str o deresolve) name,
+ (str o deresolve) sym,
str "();;"
];
val (sig_ps, (ps, p)) = (apsnd split_last o split_list)
@@ -607,7 +619,7 @@
end
| print_stmt (ML_Datas [(tyco, (vs, []))]) =
let
- val ty_p = print_tyco_expr (tyco, map ITyVar vs);
+ val ty_p = print_tyco_expr (Code_Symbol.Type_Constructor tyco, map ITyVar vs);
in
pair
[concat [str "type", ty_p]]
@@ -622,26 +634,26 @@
sig_ps
(Pretty.chunks (ps @| doublesemicolon [p]))
end
- | print_stmt (ML_Class (class, (v, (super_classes, classparams)))) =
+ | print_stmt (ML_Class (class, (v, (classrels, classparams)))) =
let
fun print_field s p = concat [str s, str ":", p];
- fun print_super_class_field (super_class, classrel) =
- print_field (deresolve classrel) (print_dicttyp (super_class, ITyVar v));
+ fun print_super_class_field (classrel as (_, super_class)) =
+ print_field (deresolve_classrel classrel) (print_dicttyp (super_class, ITyVar v));
fun print_classparam_decl (classparam, ty) =
print_val_decl print_typscheme
- (classparam, ([(v, [class])], ty));
+ (Code_Symbol.Constant classparam, ([(v, [class])], ty));
fun print_classparam_field (classparam, ty) =
- print_field (deresolve classparam) (print_typ NOBR ty);
+ print_field (deresolve_const classparam) (print_typ NOBR ty);
val w = "_" ^ first_upper v;
fun print_classparam_proj (classparam, _) =
- (concat o map str) ["let", deresolve classparam, w, "=",
- w ^ "." ^ deresolve classparam ^ ";;"];
+ (concat o map str) ["let", deresolve_const classparam, w, "=",
+ w ^ "." ^ deresolve_const classparam ^ ";;"];
val type_decl_p = concat [
str ("type '" ^ v),
- (str o deresolve) class,
+ (str o deresolve_class) class,
str "=",
enum_default "unit" ";" "{" "}" (
- map print_super_class_field super_classes
+ map print_super_class_field classrels
@ map print_classparam_field classparams
)
];
@@ -694,7 +706,7 @@
(** SML/OCaml generic part **)
-fun ml_program_of_program ctxt symbol_of module_name reserved identifiers program =
+fun ml_program_of_program ctxt module_name reserved identifiers program =
let
fun namify_const upper base (nsp_const, nsp_type) =
let
@@ -712,76 +724,76 @@
| namify_stmt (Code_Thingol.Classrel _) = namify_const false
| namify_stmt (Code_Thingol.Classparam _) = namify_const false
| namify_stmt (Code_Thingol.Classinst _) = namify_const false;
- fun ml_binding_of_stmt (name, Code_Thingol.Fun (_, ((tysm as (vs, ty), raw_eqs), _))) =
+ fun ml_binding_of_stmt (sym as Code_Symbol.Constant const, Code_Thingol.Fun ((tysm as (vs, ty), raw_eqs), _)) =
let
val eqs = filter (snd o snd) raw_eqs;
- val (eqs', some_value_name) = if null (filter_out (null o snd) vs) then case eqs
+ val (eqs', some_sym) = if null (filter_out (null o snd) vs) then case eqs
of [(([], t), some_thm)] => if (not o null o fst o Code_Thingol.unfold_fun) ty
then ([(([IVar (SOME "x")], t `$ IVar (SOME "x")), some_thm)], NONE)
- else (eqs, SOME (name, member (op =) (Code_Thingol.add_constnames t []) name))
+ else (eqs, SOME (sym, member (op =) (Code_Thingol.add_constsyms t []) sym))
| _ => (eqs, NONE)
else (eqs, NONE)
- in (ML_Function (name, (tysm, eqs')), some_value_name) end
- | ml_binding_of_stmt (name, Code_Thingol.Classinst (stmt as { vs, ... })) =
- (ML_Instance (name, stmt), if forall (null o snd) vs then SOME (name, false) else NONE)
- | ml_binding_of_stmt (name, _) =
+ in (ML_Function (const, (tysm, eqs')), some_sym) end
+ | ml_binding_of_stmt (sym as Code_Symbol.Class_Instance inst, Code_Thingol.Classinst (stmt as { vs, ... })) =
+ (ML_Instance (inst, stmt), if forall (null o snd) vs then SOME (sym, false) else NONE)
+ | ml_binding_of_stmt (sym, _) =
error ("Binding block containing illegal statement: " ^
- (Code_Symbol.quote_symbol ctxt o symbol_of) name)
- fun modify_fun (name, stmt) =
+ Code_Symbol.quote ctxt sym)
+ fun modify_fun (sym, stmt) =
let
- val (binding, some_value_name) = ml_binding_of_stmt (name, stmt);
+ val (binding, some_value_sym) = ml_binding_of_stmt (sym, stmt);
val ml_stmt = case binding
- of ML_Function (name, ((vs, ty), [])) =>
- ML_Exc (name, ((vs, ty),
+ of ML_Function (const, ((vs, ty), [])) =>
+ ML_Exc (const, ((vs, ty),
(length o filter_out (null o snd)) vs + (length o fst o Code_Thingol.unfold_fun) ty))
- | _ => case some_value_name
+ | _ => case some_value_sym
of NONE => ML_Funs ([binding], [])
- | SOME (name, true) => ML_Funs ([binding], [name])
- | SOME (name, false) => ML_Val binding
+ | SOME (sym, true) => ML_Funs ([binding], [sym])
+ | SOME (sym, false) => ML_Val binding
in SOME ml_stmt end;
fun modify_funs stmts = single (SOME
(ML_Funs (map_split ml_binding_of_stmt stmts |> (apsnd o map_filter o Option.map) fst)))
fun modify_datatypes stmts = single (SOME
(ML_Datas (map_filter
- (fn (name, Code_Thingol.Datatype (_, stmt)) => SOME (name, stmt) | _ => NONE) stmts)))
+ (fn (Code_Symbol.Type_Constructor tyco, Code_Thingol.Datatype stmt) => SOME (tyco, stmt) | _ => NONE) stmts)))
fun modify_class stmts = single (SOME
(ML_Class (the_single (map_filter
- (fn (name, Code_Thingol.Class (_, stmt)) => SOME (name, stmt) | _ => NONE) stmts))))
+ (fn (Code_Symbol.Type_Class class, Code_Thingol.Class stmt) => SOME (class, stmt) | _ => NONE) stmts))))
fun modify_stmts ([stmt as (_, stmt' as Code_Thingol.Fun _)]) =
if Code_Thingol.is_case stmt' then [] else [modify_fun stmt]
- | modify_stmts ((stmts as (_, Code_Thingol.Fun _)::_)) =
+ | modify_stmts ((stmts as (_, Code_Thingol.Fun _) :: _)) =
modify_funs (filter_out (Code_Thingol.is_case o snd) stmts)
- | modify_stmts ((stmts as (_, Code_Thingol.Datatypecons _)::_)) =
+ | modify_stmts ((stmts as (_, Code_Thingol.Datatypecons _) :: _)) =
modify_datatypes stmts
- | modify_stmts ((stmts as (_, Code_Thingol.Datatype _)::_)) =
+ | modify_stmts ((stmts as (_, Code_Thingol.Datatype _) :: _)) =
modify_datatypes stmts
- | modify_stmts ((stmts as (_, Code_Thingol.Class _)::_)) =
+ | modify_stmts ((stmts as (_, Code_Thingol.Class _) :: _)) =
modify_class stmts
- | modify_stmts ((stmts as (_, Code_Thingol.Classrel _)::_)) =
+ | modify_stmts ((stmts as (_, Code_Thingol.Classrel _) :: _)) =
modify_class stmts
- | modify_stmts ((stmts as (_, Code_Thingol.Classparam _)::_)) =
+ | modify_stmts ((stmts as (_, Code_Thingol.Classparam _) :: _)) =
modify_class stmts
| modify_stmts ([stmt as (_, Code_Thingol.Classinst _)]) =
[modify_fun stmt]
- | modify_stmts ((stmts as (_, Code_Thingol.Classinst _)::_)) =
+ | modify_stmts ((stmts as (_, Code_Thingol.Classinst _) :: _)) =
modify_funs stmts
| modify_stmts stmts = error ("Illegal mutual dependencies: " ^
- (Library.commas o map (Code_Symbol.quote_symbol ctxt o symbol_of o fst)) stmts);
+ (Library.commas o map (Code_Symbol.quote ctxt o fst)) stmts);
in
- Code_Namespace.hierarchical_program ctxt symbol_of {
+ Code_Namespace.hierarchical_program ctxt {
module_name = module_name, reserved = reserved, identifiers = identifiers,
empty_nsp = (reserved, reserved), namify_module = pair, namify_stmt = namify_stmt,
cyclic_modules = false, empty_data = (), memorize_data = K I, modify_stmts = modify_stmts } program
end;
fun serialize_ml print_ml_module print_ml_stmt with_signatures ctxt
- { symbol_of, module_name, reserved_syms, identifiers, includes,
+ { module_name, reserved_syms, identifiers, includes,
class_syntax, tyco_syntax, const_syntax } program =
let
(* build program *)
val { deresolver, hierarchical_program = ml_program } =
- ml_program_of_program ctxt symbol_of module_name (Name.make_context reserved_syms) identifiers program;
+ ml_program_of_program ctxt module_name (Name.make_context reserved_syms) identifiers program;
(* print statements *)
fun print_stmt prefix_fragments (_, stmt) = print_ml_stmt
@@ -803,7 +815,7 @@
lift_markup = apsnd } ml_program));
fun write width NONE = writeln o format [] width
| write width (SOME p) = File.write p o format [] width;
- fun prepare names width p = ([("", format names width p)], try (deresolver []));
+ fun prepare syms width p = ([("", format syms width p)], try (deresolver []));
in
Code_Target.serialization write prepare p
end;