--- a/src/Tools/Code/code_haskell.ML Mon Oct 12 14:22:54 2009 +0200
+++ b/src/Tools/Code/code_haskell.ML Mon Oct 12 15:46:38 2009 +0200
@@ -144,12 +144,10 @@
val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
fun pr_eq ((ts, t), (thm, _)) =
let
- val consts = map_filter
- (fn c => if (is_some o syntax_const) c
- then NONE else (SOME o Long_Name.base_name o deresolve) c)
- (fold Code_Thingol.add_constnames (t :: ts) []);
+ val consts = fold Code_Thingol.add_constnames (t :: ts) [];
val vars = init_syms
- |> Code_Printer.intro_vars consts
+ |> Code_Printer.intro_base_names
+ (is_none o syntax_const) deresolve consts
|> Code_Printer.intro_vars ((fold o Code_Thingol.fold_varnames)
(insert (op =)) ts []);
in
--- a/src/Tools/Code/code_ml.ML Mon Oct 12 14:22:54 2009 +0200
+++ b/src/Tools/Code/code_ml.ML Mon Oct 12 15:46:38 2009 +0200
@@ -175,12 +175,10 @@
end
| pr_stmt (MLVal (name, (((vs, ty), t), (thm, _)))) =
let
- val consts = map_filter
- (fn c => if (is_some o syntax_const) c
- then NONE else (SOME o Long_Name.base_name o deresolve) c)
- (Code_Thingol.add_constnames t []);
+ val consts = Code_Thingol.add_constnames t [];
val vars = reserved_names
- |> Code_Printer.intro_vars consts;
+ |> Code_Printer.intro_base_names
+ (is_none o syntax_const) deresolve consts;
in
concat [
str "val",
@@ -200,12 +198,10 @@
map (Pretty.block o single o Pretty.block o single);
fun pr_eq definer ((ts, t), (thm, _)) =
let
- val consts = map_filter
- (fn c => if (is_some o syntax_const) c
- then NONE else (SOME o Long_Name.base_name o deresolve) c)
- (fold Code_Thingol.add_constnames (t :: ts) []);
+ val consts = fold Code_Thingol.add_constnames (t :: ts) [];
val vars = reserved_names
- |> Code_Printer.intro_vars consts
+ |> Code_Printer.intro_base_names
+ (is_none o syntax_const) deresolve consts
|> Code_Printer.intro_vars ((fold o Code_Thingol.fold_varnames)
(insert (op =)) ts []);
in
@@ -472,12 +468,10 @@
end
| pr_stmt (MLVal (name, (((vs, ty), t), (thm, _)))) =
let
- val consts = map_filter
- (fn c => if (is_some o syntax_const) c
- then NONE else (SOME o Long_Name.base_name o deresolve) c)
- (Code_Thingol.add_constnames t []);
+ val consts = Code_Thingol.add_constnames t [];
val vars = reserved_names
- |> Code_Printer.intro_vars consts;
+ |> Code_Printer.intro_base_names
+ (is_none o syntax_const) deresolve consts;
in
concat [
str "let",
@@ -492,12 +486,10 @@
let
fun pr_eq ((ts, t), (thm, _)) =
let
- val consts = map_filter
- (fn c => if (is_some o syntax_const) c
- then NONE else (SOME o Long_Name.base_name o deresolve) c)
- (fold Code_Thingol.add_constnames (t :: ts) []);
+ val consts = fold Code_Thingol.add_constnames (t :: ts) [];
val vars = reserved_names
- |> Code_Printer.intro_vars consts
+ |> Code_Printer.intro_base_names
+ (is_none o syntax_const) deresolve consts
|> Code_Printer.intro_vars ((fold o Code_Thingol.fold_varnames)
(insert (op =)) ts []);
in concat [
@@ -508,12 +500,10 @@
] end;
fun pr_eqs is_pseudo [((ts, t), (thm, _))] =
let
- val consts = map_filter
- (fn c => if (is_some o syntax_const) c
- then NONE else (SOME o Long_Name.base_name o deresolve) c)
- (fold Code_Thingol.add_constnames (t :: ts) []);
+ val consts = fold Code_Thingol.add_constnames (t :: ts) [];
val vars = reserved_names
- |> Code_Printer.intro_vars consts
+ |> Code_Printer.intro_base_names
+ (is_none o syntax_const) deresolve consts
|> Code_Printer.intro_vars ((fold o Code_Thingol.fold_varnames)
(insert (op =)) ts []);
in
@@ -536,12 +526,10 @@
)
| pr_eqs _ (eqs as eq :: eqs') =
let
- val consts = map_filter
- (fn c => if (is_some o syntax_const) c
- then NONE else (SOME o Long_Name.base_name o deresolve) c)
- (fold Code_Thingol.add_constnames (map (snd o fst) eqs) []);
+ val consts = fold Code_Thingol.add_constnames (map (snd o fst) eqs) [];
val vars = reserved_names
- |> Code_Printer.intro_vars consts;
+ |> Code_Printer.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;
in
Pretty.block (
--- a/src/Tools/Code/code_printer.ML Mon Oct 12 14:22:54 2009 +0200
+++ b/src/Tools/Code/code_printer.ML Mon Oct 12 15:46:38 2009 +0200
@@ -27,6 +27,8 @@
val make_vars: string list -> var_ctxt
val intro_vars: string list -> var_ctxt -> var_ctxt
val lookup_var: var_ctxt -> string -> string
+ val intro_base_names: (string -> bool) -> (string -> string)
+ -> string list -> var_ctxt -> var_ctxt
val aux_params: var_ctxt -> iterm list list -> string list
type literals
@@ -134,6 +136,13 @@
val vars' = intro_vars fished3 vars;
in map (lookup_var vars') fished3 end;
+fun intro_base_names no_syntax deresolve names = names
+ |> map_filter (fn name => if no_syntax name then
+ let val name' = deresolve name in
+ if Long_Name.is_qualified name' then NONE else SOME name'
+ end else NONE)
+ |> intro_vars;
+
(** pretty literals **)