dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
--- a/src/Tools/Code/code_haskell.ML Tue Oct 13 14:57:53 2009 +0200
+++ b/src/Tools/Code/code_haskell.ML Wed Oct 14 11:56:44 2009 +0200
@@ -24,7 +24,7 @@
(** Haskell serializer **)
fun pr_haskell_stmt labelled_name syntax_class syntax_tyco syntax_const
- init_syms deresolve contr_classparam_typs deriving_show =
+ reserved deresolve contr_classparam_typs deriving_show =
let
val deresolve_base = Long_Name.base_name o deresolve;
fun class_name class = case syntax_class class
@@ -34,18 +34,18 @@
of [] => []
| classbinds => Pretty.enum "," "(" ")" (
map (fn (v, class) =>
- str (class_name class ^ " " ^ Code_Printer.lookup_var tyvars v)) classbinds)
+ str (class_name class ^ " " ^ lookup_var tyvars v)) classbinds)
@@ str " => ";
fun pr_typforall tyvars vs = case map fst vs
of [] => []
| vnames => str "forall " :: Pretty.breaks
- (map (str o Code_Printer.lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1;
+ (map (str o lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1;
fun pr_tycoexpr tyvars fxy (tyco, tys) =
brackify fxy (str tyco :: map (pr_typ tyvars BR) tys)
and pr_typ tyvars fxy (tycoexpr as tyco `%% tys) = (case syntax_tyco tyco
of NONE => pr_tycoexpr tyvars fxy (deresolve tyco, tys)
| SOME (i, pr) => pr (pr_typ tyvars) fxy tys)
- | pr_typ tyvars fxy (ITyVar v) = (str o Code_Printer.lookup_var tyvars) v;
+ | pr_typ tyvars fxy (ITyVar v) = (str o lookup_var tyvars) v;
fun pr_typdecl tyvars (vs, tycoexpr) =
Pretty.block (pr_typcontext tyvars vs @| pr_tycoexpr tyvars NOBR tycoexpr);
fun pr_typscheme tyvars (vs, ty) =
@@ -63,7 +63,7 @@
| pr_term tyvars thm vars fxy (IVar NONE) =
str "_"
| pr_term tyvars thm vars fxy (IVar (SOME v)) =
- (str o Code_Printer.lookup_var vars) v
+ (str o lookup_var vars) v
| pr_term tyvars thm vars fxy (t as _ `|=> _) =
let
val (binds, t') = Code_Thingol.unfold_pat_abs t;
@@ -118,7 +118,7 @@
(brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""];
fun pr_stmt (name, Code_Thingol.Fun (_, ((vs, ty), []))) =
let
- val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
+ val tyvars = intro_vars (map fst vs) reserved;
val n = (length o fst o Code_Thingol.unfold_fun) ty;
in
Pretty.chunks [
@@ -141,14 +141,14 @@
| pr_stmt (name, Code_Thingol.Fun (_, ((vs, ty), raw_eqs))) =
let
val eqs = filter (snd o snd) raw_eqs;
- val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
+ val tyvars = intro_vars (map fst vs) reserved;
fun pr_eq ((ts, t), (thm, _)) =
let
val consts = fold Code_Thingol.add_constnames (t :: ts) [];
- val vars = init_syms
- |> Code_Printer.intro_base_names
+ val vars = reserved
+ |> intro_base_names
(is_none o syntax_const) deresolve consts
- |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_varnames)
+ |> intro_vars ((fold o Code_Thingol.fold_varnames)
(insert (op =)) ts []);
in
semicolon (
@@ -171,7 +171,7 @@
end
| pr_stmt (name, Code_Thingol.Datatype (_, (vs, []))) =
let
- val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
+ val tyvars = intro_vars (map fst vs) reserved;
in
semicolon [
str "data",
@@ -180,7 +180,7 @@
end
| pr_stmt (name, Code_Thingol.Datatype (_, (vs, [(co, [ty])]))) =
let
- val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
+ val tyvars = intro_vars (map fst vs) reserved;
in
semicolon (
str "newtype"
@@ -193,7 +193,7 @@
end
| pr_stmt (name, Code_Thingol.Datatype (_, (vs, co :: cos))) =
let
- val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
+ val tyvars = intro_vars (map fst vs) reserved;
fun pr_co (co, tys) =
concat (
(str o deresolve_base) co
@@ -211,7 +211,7 @@
end
| pr_stmt (name, Code_Thingol.Class (_, (v, (superclasses, classparams)))) =
let
- val tyvars = Code_Printer.intro_vars [v] init_syms;
+ val tyvars = intro_vars [v] reserved;
fun pr_classparam (classparam, ty) =
semicolon [
(str o deresolve_base) classparam,
@@ -223,7 +223,7 @@
Pretty.block [
str "class ",
Pretty.block (pr_typcontext tyvars [(v, map fst superclasses)]),
- str (deresolve_base name ^ " " ^ Code_Printer.lookup_var tyvars v),
+ str (deresolve_base name ^ " " ^ lookup_var tyvars v),
str " where {"
],
str "};"
@@ -231,12 +231,12 @@
end
| pr_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, classparam_insts))) =
let
- val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
+ val tyvars = intro_vars (map fst vs) reserved;
fun pr_instdef ((classparam, c_inst), (thm, _)) = case syntax_const classparam
of NONE => semicolon [
(str o deresolve_base) classparam,
str "=",
- pr_app tyvars thm init_syms NOBR (c_inst, [])
+ pr_app tyvars thm reserved NOBR (c_inst, [])
]
| SOME (k, pr) =>
let
@@ -245,9 +245,9 @@
then NONE else (SOME o Long_Name.base_name o deresolve) c_inst_name;
val proto_rhs = Code_Thingol.eta_expand k (c_inst, []);
val (vs, rhs) = (apfst o map) fst (Code_Thingol.unfold_abs proto_rhs);
- val vars = init_syms
- |> Code_Printer.intro_vars (the_list const)
- |> Code_Printer.intro_vars (map_filter I vs);
+ val vars = reserved
+ |> intro_vars (the_list const)
+ |> intro_vars (map_filter I vs);
val lhs = IConst (classparam, (([], []), tys)) `$$ map IVar vs;
(*dictionaries are not relevant at this late stage*)
in
@@ -271,24 +271,24 @@
end;
in pr_stmt end;
-fun haskell_program_of_program labelled_name module_name module_prefix reserved_names raw_module_alias program =
+fun haskell_program_of_program labelled_name module_name module_prefix reserved raw_module_alias program =
let
val module_alias = if is_some module_name then K module_name else raw_module_alias;
- val reserved_names = Name.make_context reserved_names;
- val mk_name_module = Code_Printer.mk_name_module reserved_names module_prefix module_alias program;
+ val reserved = Name.make_context reserved;
+ val mk_name_module = mk_name_module reserved module_prefix module_alias program;
fun add_stmt (name, (stmt, deps)) =
let
- val (module_name, base) = Code_Printer.dest_name name;
+ val (module_name, base) = dest_name name;
val module_name' = mk_name_module module_name;
val mk_name_stmt = yield_singleton Name.variants;
fun add_fun upper (nsp_fun, nsp_typ) =
let
val (base', nsp_fun') =
- mk_name_stmt (if upper then Code_Printer.first_upper base else base) nsp_fun
+ mk_name_stmt (if upper then first_upper base else base) nsp_fun
in (base', (nsp_fun', nsp_typ)) end;
fun add_typ (nsp_fun, nsp_typ) =
let
- val (base', nsp_typ') = mk_name_stmt (Code_Printer.first_upper base) nsp_typ
+ val (base', nsp_typ') = mk_name_stmt (first_upper base) nsp_typ
in (base', (nsp_fun, nsp_typ')) end;
val add_name = case stmt
of Code_Thingol.Fun _ => add_fun false
@@ -306,7 +306,7 @@
cons (name, (Long_Name.append module_name' base', NONE))
| _ => cons (name, (Long_Name.append module_name' base', SOME stmt));
in
- Symtab.map_default (module_name', ([], ([], (reserved_names, reserved_names))))
+ Symtab.map_default (module_name', ([], ([], (reserved, reserved))))
(apfst (fold (insert (op = : string * string -> bool)) deps))
#> `(fn program => add_name ((snd o snd o the o Symtab.lookup program) module_name'))
#-> (fn (base', names) =>
@@ -317,19 +317,19 @@
(Graph.get_node program name, Graph.imm_succs program name))
(Graph.strong_conn program |> flat)) Symtab.empty;
fun deresolver name = (fst o the o AList.lookup (op =) ((fst o snd o the
- o Symtab.lookup hs_program) ((mk_name_module o fst o Code_Printer.dest_name) name))) name
+ o Symtab.lookup hs_program) ((mk_name_module o fst o dest_name) name))) name
handle Option => error ("Unknown statement name: " ^ labelled_name name);
in (deresolver, hs_program) end;
fun serialize_haskell module_prefix raw_module_name string_classes labelled_name
- raw_reserved_names includes raw_module_alias
+ raw_reserved includes raw_module_alias
syntax_class syntax_tyco syntax_const program cs destination =
let
val stmt_names = Code_Target.stmt_names_of_destination destination;
val module_name = if null stmt_names then raw_module_name else SOME "Code";
- val reserved_names = fold (insert (op =) o fst) includes raw_reserved_names;
+ val reserved = fold (insert (op =) o fst) includes raw_reserved;
val (deresolver, hs_program) = haskell_program_of_program labelled_name
- module_name module_prefix reserved_names raw_module_alias program;
+ module_name module_prefix reserved raw_module_alias program;
val contr_classparam_typs = Code_Thingol.contr_classparam_typs program;
fun deriving_show tyco =
let
@@ -343,9 +343,9 @@
andalso forall (deriv' tycos) tys
| deriv' _ (ITyVar _) = true
in deriv [] tyco end;
- val reserved_names = Code_Printer.make_vars reserved_names;
+ val reserved = make_vars reserved;
fun pr_stmt qualified = pr_haskell_stmt labelled_name
- syntax_class syntax_tyco syntax_const reserved_names
+ syntax_class syntax_tyco syntax_const reserved
(if qualified then deresolver else Long_Name.base_name o deresolver)
contr_classparam_typs
(if string_classes then deriving_show else K false);
--- a/src/Tools/Code/code_ml.ML Tue Oct 13 14:57:53 2009 +0200
+++ b/src/Tools/Code/code_ml.ML Wed Oct 14 11:56:44 2009 +0200
@@ -45,12 +45,12 @@
(** SML serailizer **)
-fun pr_sml_stmt labelled_name syntax_tyco syntax_const reserved_names deresolve is_cons =
+fun pr_sml_stmt labelled_name syntax_tyco syntax_const reserved deresolve is_cons =
let
fun pr_dicts fxy ds =
let
- fun pr_dictvar (v, (_, 1)) = Code_Printer.first_upper v ^ "_"
- | pr_dictvar (v, (i, _)) = Code_Printer.first_upper v ^ string_of_int (i+1) ^ "_";
+ 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_proj [p'] p =
@@ -88,7 +88,7 @@
| pr_term is_closure thm vars fxy (IVar NONE) =
str "_"
| pr_term is_closure thm vars fxy (IVar (SOME v)) =
- str (Code_Printer.lookup_var vars v)
+ str (lookup_var vars v)
| pr_term is_closure thm vars fxy (t as t1 `$ t2) =
(case Code_Thingol.unfold_const_app t
of SOME c_ts => pr_app is_closure thm vars fxy c_ts
@@ -176,8 +176,8 @@
| pr_stmt (MLVal (name, (((vs, ty), t), (thm, _)))) =
let
val consts = Code_Thingol.add_constnames t [];
- val vars = reserved_names
- |> Code_Printer.intro_base_names
+ val vars = reserved
+ |> intro_base_names
(is_none o syntax_const) deresolve consts;
in
concat [
@@ -199,10 +199,10 @@
fun pr_eq definer ((ts, t), (thm, _)) =
let
val consts = fold Code_Thingol.add_constnames (t :: ts) [];
- val vars = reserved_names
- |> Code_Printer.intro_base_names
+ val vars = reserved
+ |> intro_base_names
(is_none o syntax_const) deresolve consts
- |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_varnames)
+ |> intro_vars ((fold o Code_Thingol.fold_varnames)
(insert (op =)) ts []);
in
concat (
@@ -260,7 +260,7 @@
in Pretty.chunks (ps @| Pretty.block ([p, str ";"])) end
| pr_stmt (MLClass (class, (v, (superclasses, classparams)))) =
let
- val w = Code_Printer.first_upper v ^ "_";
+ val w = first_upper v ^ "_";
fun pr_superclass_field (class, classrel) =
(concat o map str) [
deresolve classrel, ":", "'" ^ v, deresolve class
@@ -313,7 +313,7 @@
concat [
(str o Long_Name.base_name o deresolve) classparam,
str "=",
- pr_app (K false) thm reserved_names NOBR (c_inst, [])
+ pr_app (K false) thm reserved NOBR (c_inst, [])
];
in
semicolon ([
@@ -352,12 +352,12 @@
(** OCaml serializer **)
-fun pr_ocaml_stmt labelled_name syntax_tyco syntax_const reserved_names deresolve is_cons =
+fun pr_ocaml_stmt labelled_name syntax_tyco syntax_const reserved deresolve is_cons =
let
fun pr_dicts fxy ds =
let
- fun pr_dictvar (v, (_, 1)) = "_" ^ Code_Printer.first_upper v
- | pr_dictvar (v, (i, _)) = "_" ^ Code_Printer.first_upper v ^ string_of_int (i+1);
+ 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_dict fxy (DictConst (inst, dss)) =
@@ -391,7 +391,7 @@
| pr_term is_closure thm vars fxy (IVar NONE) =
str "_"
| pr_term is_closure thm vars fxy (IVar (SOME v)) =
- str (Code_Printer.lookup_var vars v)
+ str (lookup_var vars v)
| pr_term is_closure thm vars fxy (t as t1 `$ t2) =
(case Code_Thingol.unfold_const_app t
of SOME c_ts => pr_app is_closure thm vars fxy c_ts
@@ -469,8 +469,8 @@
| pr_stmt (MLVal (name, (((vs, ty), t), (thm, _)))) =
let
val consts = Code_Thingol.add_constnames t [];
- val vars = reserved_names
- |> Code_Printer.intro_base_names
+ val vars = reserved
+ |> intro_base_names
(is_none o syntax_const) deresolve consts;
in
concat [
@@ -487,10 +487,10 @@
fun pr_eq ((ts, t), (thm, _)) =
let
val consts = fold Code_Thingol.add_constnames (t :: ts) [];
- val vars = reserved_names
- |> Code_Printer.intro_base_names
+ val vars = reserved
+ |> intro_base_names
(is_none o syntax_const) deresolve consts
- |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_varnames)
+ |> intro_vars ((fold o Code_Thingol.fold_varnames)
(insert (op =)) ts []);
in concat [
(Pretty.block o Pretty.commas)
@@ -501,10 +501,10 @@
fun pr_eqs is_pseudo [((ts, t), (thm, _))] =
let
val consts = fold Code_Thingol.add_constnames (t :: ts) [];
- val vars = reserved_names
- |> Code_Printer.intro_base_names
+ val vars = reserved
+ |> intro_base_names
(is_none o syntax_const) deresolve consts
- |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_varnames)
+ |> intro_vars ((fold o Code_Thingol.fold_varnames)
(insert (op =)) ts []);
in
concat (
@@ -527,10 +527,10 @@
| pr_eqs _ (eqs as eq :: eqs') =
let
val consts = fold Code_Thingol.add_constnames (map (snd o fst) eqs) [];
- val vars = reserved_names
- |> Code_Printer.intro_base_names
+ val vars = reserved
+ |> intro_base_names
(is_none o syntax_const) deresolve consts;
- val dummy_parms = (map str o Code_Printer.aux_params vars o map (fst o fst)) eqs;
+ val dummy_parms = (map str o aux_params vars o map (fst o fst)) eqs;
in
Pretty.block (
Pretty.breaks dummy_parms
@@ -595,7 +595,7 @@
in Pretty.chunks (ps @| Pretty.block ([p, str ";;"])) end
| pr_stmt (MLClass (class, (v, (superclasses, classparams)))) =
let
- val w = "_" ^ Code_Printer.first_upper v;
+ val w = "_" ^ first_upper v;
fun pr_superclass_field (class, classrel) =
(concat o map str) [
deresolve classrel, ":", "'" ^ v, deresolve class
@@ -636,7 +636,7 @@
concat [
(str o deresolve) classparam,
str "=",
- pr_app (K false) thm reserved_names NOBR (c_inst, [])
+ pr_app (K false) thm reserved NOBR (c_inst, [])
];
in
concat (
@@ -705,11 +705,11 @@
in
-fun ml_node_of_program labelled_name module_name reserved_names raw_module_alias program =
+fun ml_node_of_program labelled_name module_name reserved raw_module_alias program =
let
val module_alias = if is_some module_name then K module_name else raw_module_alias;
- val reserved_names = Name.make_context reserved_names;
- val empty_module = ((reserved_names, reserved_names), Graph.empty);
+ val reserved = Name.make_context reserved;
+ val empty_module = ((reserved, reserved), Graph.empty);
fun map_node [] f = f
| map_node (m::ms) f =
Graph.default_node (m, Module (m, empty_module))
@@ -737,11 +737,11 @@
let
val (x, nsp_typ') = f nsp_typ
in (x, (nsp_fun, nsp_typ')) end;
- val mk_name_module = Code_Printer.mk_name_module reserved_names NONE module_alias program;
+ val mk_name_module = mk_name_module reserved NONE module_alias program;
fun mk_name_stmt upper name nsp =
let
- val (_, base) = Code_Printer.dest_name name;
- val base' = if upper then Code_Printer.first_upper base else base;
+ val (_, base) = dest_name name;
+ val base' = if upper then first_upper base else base;
val ([base''], nsp') = Name.variants [base'] nsp;
in (base'', nsp') end;
fun rearrange_fun name (tysm as (vs, ty), raw_eqs) =
@@ -824,7 +824,7 @@
[]
|> fold (fold (insert (op =)) o Graph.imm_succs program) names
|> subtract (op =) names;
- val (module_names, _) = (split_list o map Code_Printer.dest_name) names;
+ val (module_names, _) = (split_list o map dest_name) names;
val module_name = (the_single o distinct (op =) o map mk_name_module) module_names
handle Empty =>
error ("Different namespace prefixes for mutual dependencies:\n"
@@ -834,7 +834,7 @@
val module_name_path = Long_Name.explode module_name;
fun add_dep name name' =
let
- val module_name' = (mk_name_module o fst o Code_Printer.dest_name) name';
+ val module_name' = (mk_name_module o fst o dest_name) name';
in if module_name = module_name' then
map_node module_name_path (Graph.add_edge (name, name'))
else let
@@ -862,7 +862,7 @@
(rev (Graph.strong_conn program)));
fun deresolver prefix name =
let
- val module_name = (fst o Code_Printer.dest_name) name;
+ val module_name = (fst o dest_name) name;
val module_name' = (Long_Name.explode o mk_name_module) module_name;
val (_, (_, remainder)) = chop_prefix (op =) (prefix, module_name');
val stmt_name =
@@ -877,7 +877,7 @@
error ("Unknown statement name: " ^ labelled_name name);
in (deresolver, nodes) end;
-fun serialize_ml target compile pr_module pr_stmt raw_module_name labelled_name reserved_names includes raw_module_alias
+fun serialize_ml target compile pr_module pr_stmt raw_module_name labelled_name reserved includes raw_module_alias
_ syntax_tyco syntax_const program stmt_names destination =
let
val is_cons = Code_Thingol.is_cons program;
@@ -885,15 +885,15 @@
val is_present = not (null present_stmt_names);
val module_name = if is_present then SOME "Code" else raw_module_name;
val (deresolver, nodes) = ml_node_of_program labelled_name module_name
- reserved_names raw_module_alias program;
- val reserved_names = Code_Printer.make_vars reserved_names;
+ reserved raw_module_alias program;
+ val reserved = make_vars reserved;
fun pr_node prefix (Dummy _) =
NONE
| pr_node prefix (Stmt (_, stmt)) = if is_present andalso
(null o filter (member (op =) present_stmt_names) o stmt_names_of) stmt
then NONE
else SOME
- (pr_stmt labelled_name syntax_tyco syntax_const reserved_names
+ (pr_stmt labelled_name syntax_tyco syntax_const reserved
(deresolver prefix) is_cons stmt)
| pr_node prefix (Module (module_name, (_, nodes))) =
separate (str "")
--- a/src/Tools/Code/code_printer.ML Tue Oct 13 14:57:53 2009 +0200
+++ b/src/Tools/Code/code_printer.ML Wed Oct 14 11:56:44 2009 +0200
@@ -316,13 +316,13 @@
val dest_name =
apfst Long_Name.implode o split_last o fst o split_last o Long_Name.explode;
-fun mk_name_module reserved_names module_prefix module_alias program =
+fun mk_name_module reserved module_prefix module_alias program =
let
fun mk_alias name = case module_alias name
of SOME name' => name'
| NONE => name
|> Long_Name.explode
- |> map (fn name => (the_single o fst) (Name.variants [name] reserved_names))
+ |> map (fn name => (the_single o fst) (Name.variants [name] reserved))
|> Long_Name.implode;
fun mk_prefix name = case module_prefix
of SOME module_prefix => Long_Name.append module_prefix name