--- a/src/Tools/code/code_haskell.ML Sun Mar 22 11:56:22 2009 +0100
+++ b/src/Tools/code/code_haskell.ML Sun Mar 22 11:56:32 2009 +0100
@@ -42,18 +42,18 @@
of [] => []
| classbinds => Pretty.enum "," "(" ")" (
map (fn (v, class) =>
- str (class_name class ^ " " ^ Code_Name.lookup_var tyvars v)) classbinds)
+ str (class_name class ^ " " ^ Code_Printer.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_Name.lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1;
+ (map (str o Code_Printer.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_Name.lookup_var tyvars) v;
+ | pr_typ tyvars fxy (ITyVar v) = (str o Code_Printer.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) =
@@ -69,7 +69,7 @@
pr_term tyvars thm vars BR t2
])
| pr_term tyvars thm vars fxy (IVar v) =
- (str o Code_Name.lookup_var vars) v
+ (str o Code_Printer.lookup_var vars) v
| pr_term tyvars thm vars fxy (t as _ `|-> _) =
let
val (binds, t') = Code_Thingol.unfold_abs t;
@@ -127,7 +127,7 @@
| pr_case tyvars thm vars fxy ((_, []), _) = str "error \"empty case\"";
fun pr_stmt (name, Code_Thingol.Fun (_, ((vs, ty), []))) =
let
- val tyvars = Code_Name.intro_vars (map fst vs) init_syms;
+ val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
val n = (length o fst o Code_Thingol.unfold_fun) ty;
in
Pretty.chunks [
@@ -150,7 +150,7 @@
| pr_stmt (name, Code_Thingol.Fun (_, ((vs, ty), raw_eqs))) =
let
val eqs = filter (snd o snd) raw_eqs;
- val tyvars = Code_Name.intro_vars (map fst vs) init_syms;
+ val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
fun pr_eq ((ts, t), (thm, _)) =
let
val consts = map_filter
@@ -158,8 +158,8 @@
then NONE else (SOME o Long_Name.base_name o deresolve) c)
((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
val vars = init_syms
- |> Code_Name.intro_vars consts
- |> Code_Name.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
+ |> Code_Printer.intro_vars consts
+ |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
(insert (op =)) ts []);
in
semicolon (
@@ -182,7 +182,7 @@
end
| pr_stmt (name, Code_Thingol.Datatype (_, (vs, []))) =
let
- val tyvars = Code_Name.intro_vars (map fst vs) init_syms;
+ val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
in
semicolon [
str "data",
@@ -191,7 +191,7 @@
end
| pr_stmt (name, Code_Thingol.Datatype (_, (vs, [(co, [ty])]))) =
let
- val tyvars = Code_Name.intro_vars (map fst vs) init_syms;
+ val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
in
semicolon (
str "newtype"
@@ -204,7 +204,7 @@
end
| pr_stmt (name, Code_Thingol.Datatype (_, (vs, co :: cos))) =
let
- val tyvars = Code_Name.intro_vars (map fst vs) init_syms;
+ val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
fun pr_co (co, tys) =
concat (
(str o deresolve_base) co
@@ -222,7 +222,7 @@
end
| pr_stmt (name, Code_Thingol.Class (_, (v, (superclasses, classparams)))) =
let
- val tyvars = Code_Name.intro_vars [v] init_syms;
+ val tyvars = Code_Printer.intro_vars [v] init_syms;
fun pr_classparam (classparam, ty) =
semicolon [
(str o deresolve_base) classparam,
@@ -234,7 +234,7 @@
Pretty.block [
str "class ",
Pretty.block (pr_typcontext tyvars [(v, map fst superclasses)]),
- str (deresolve_base name ^ " " ^ Code_Name.lookup_var tyvars v),
+ str (deresolve_base name ^ " " ^ Code_Printer.lookup_var tyvars v),
str " where {"
],
str "};"
@@ -244,7 +244,7 @@
let
val split_abs_pure = (fn (v, _) `|-> t => SOME (v, t) | _ => NONE);
val unfold_abs_pure = Code_Thingol.unfoldr split_abs_pure;
- val tyvars = Code_Name.intro_vars (map fst vs) init_syms;
+ val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
fun pr_instdef ((classparam, c_inst), (thm, _)) = case syntax_const classparam
of NONE => semicolon [
(str o deresolve_base) classparam,
@@ -259,8 +259,8 @@
val proto_rhs = Code_Thingol.eta_expand k (c_inst, []);
val (vs, rhs) = unfold_abs_pure proto_rhs;
val vars = init_syms
- |> Code_Name.intro_vars (the_list const)
- |> Code_Name.intro_vars vs;
+ |> Code_Printer.intro_vars (the_list const)
+ |> Code_Printer.intro_vars vs;
val lhs = IConst (classparam, ([], tys)) `$$ map IVar vs;
(*dictionaries are not relevant at this late stage*)
in
@@ -288,20 +288,20 @@
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_Name.mk_name_module reserved_names module_prefix module_alias program;
+ val mk_name_module = Code_Printer.mk_name_module reserved_names module_prefix module_alias program;
fun add_stmt (name, (stmt, deps)) =
let
- val (module_name, base) = Code_Name.dest_name name;
+ val (module_name, base) = Code_Printer.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_Name.first_upper base else base) nsp_fun
+ mk_name_stmt (if upper then Code_Printer.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_Name.first_upper base) nsp_typ
+ val (base', nsp_typ') = mk_name_stmt (Code_Printer.first_upper base) nsp_typ
in (base', (nsp_fun, nsp_typ')) end;
val add_name = case stmt
of Code_Thingol.Fun _ => add_fun false
@@ -330,7 +330,7 @@
(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_Name.dest_name) name))) name
+ o Symtab.lookup hs_program) ((mk_name_module o fst o Code_Printer.dest_name) name))) name
handle Option => error ("Unknown statement name: " ^ labelled_name name);
in (deresolver, hs_program) end;
@@ -357,7 +357,7 @@
andalso forall (deriv' tycos) tys
| deriv' _ (ITyVar _) = true
in deriv [] tyco end;
- val reserved_names = Code_Name.make_vars reserved_names;
+ val reserved_names = Code_Printer.make_vars reserved_names;
fun pr_stmt qualified = pr_haskell_stmt naming labelled_name
syntax_class syntax_tyco syntax_const reserved_names
(if qualified then deresolver else Long_Name.base_name o deresolver)
--- a/src/Tools/code/code_ml.ML Sun Mar 22 11:56:22 2009 +0100
+++ b/src/Tools/code/code_ml.ML Sun Mar 22 11:56:32 2009 +0100
@@ -50,8 +50,8 @@
val pr_label_classparam = Long_Name.base_name o Long_Name.qualifier;
fun pr_dicts fxy ds =
let
- fun pr_dictvar (v, (_, 1)) = Code_Name.first_upper v ^ "_"
- | pr_dictvar (v, (i, _)) = Code_Name.first_upper v ^ string_of_int (i+1) ^ "_";
+ 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_proj [] p =
p
| pr_proj [p'] p =
@@ -87,7 +87,7 @@
fun pr_term is_closure thm vars fxy (IConst c) =
pr_app is_closure thm vars fxy (c, [])
| pr_term is_closure thm vars fxy (IVar v) =
- str (Code_Name.lookup_var vars v)
+ str (Code_Printer.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
@@ -182,7 +182,7 @@
then NONE else (SOME o Long_Name.base_name o deresolve) c)
(Code_Thingol.fold_constnames (insert (op =)) t []);
val vars = reserved_names
- |> Code_Name.intro_vars consts;
+ |> Code_Printer.intro_vars consts;
in
concat [
str "val",
@@ -207,8 +207,8 @@
then NONE else (SOME o Long_Name.base_name o deresolve) c)
((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
val vars = reserved_names
- |> Code_Name.intro_vars consts
- |> Code_Name.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
+ |> Code_Printer.intro_vars consts
+ |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
(insert (op =)) ts []);
in
concat (
@@ -266,7 +266,7 @@
in Pretty.chunks (ps @| Pretty.block ([p, str ";"])) end
| pr_stmt (MLClass (class, (v, (superclasses, classparams)))) =
let
- val w = Code_Name.first_upper v ^ "_";
+ val w = Code_Printer.first_upper v ^ "_";
fun pr_superclass_field (class, classrel) =
(concat o map str) [
pr_label_classrel classrel, ":", "'" ^ v, deresolve class
@@ -362,8 +362,8 @@
let
fun pr_dicts fxy ds =
let
- fun pr_dictvar (v, (_, 1)) = "_" ^ Code_Name.first_upper v
- | pr_dictvar (v, (i, _)) = "_" ^ Code_Name.first_upper v ^ string_of_int (i+1);
+ 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_proj ps p =
fold_rev (fn p2 => fn p1 => Pretty.block [p1, str ".", str p2]) ps p
fun pr_dict fxy (DictConst (inst, dss)) =
@@ -395,7 +395,7 @@
fun pr_term is_closure thm vars fxy (IConst c) =
pr_app is_closure thm vars fxy (c, [])
| pr_term is_closure thm vars fxy (IVar v) =
- str (Code_Name.lookup_var vars v)
+ str (Code_Printer.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
@@ -468,8 +468,8 @@
val x = Name.variant (map_filter I fished1) "x";
val fished2 = map_index (fillup_param x) fished1;
val (fished3, _) = Name.variants fished2 Name.context;
- val vars' = Code_Name.intro_vars fished3 vars;
- in map (Code_Name.lookup_var vars') fished3 end;
+ val vars' = Code_Printer.intro_vars fished3 vars;
+ in map (Code_Printer.lookup_var vars') fished3 end;
fun pr_stmt (MLExc (name, n)) =
let
val exc_str =
@@ -491,7 +491,7 @@
then NONE else (SOME o Long_Name.base_name o deresolve) c)
(Code_Thingol.fold_constnames (insert (op =)) t []);
val vars = reserved_names
- |> Code_Name.intro_vars consts;
+ |> Code_Printer.intro_vars consts;
in
concat [
str "let",
@@ -511,8 +511,8 @@
then NONE else (SOME o Long_Name.base_name o deresolve) c)
((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
val vars = reserved_names
- |> Code_Name.intro_vars consts
- |> Code_Name.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
+ |> Code_Printer.intro_vars consts
+ |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
(insert (op =)) ts []);
in concat [
(Pretty.block o Pretty.commas)
@@ -527,8 +527,8 @@
then NONE else (SOME o Long_Name.base_name o deresolve) c)
((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
val vars = reserved_names
- |> Code_Name.intro_vars consts
- |> Code_Name.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
+ |> Code_Printer.intro_vars consts
+ |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
(insert (op =)) ts []);
in
concat (
@@ -556,7 +556,7 @@
((fold o Code_Thingol.fold_constnames)
(insert (op =)) (map (snd o fst) eqs) []);
val vars = reserved_names
- |> Code_Name.intro_vars consts;
+ |> Code_Printer.intro_vars consts;
val dummy_parms = (map str o fish_params vars o map (fst o fst)) eqs;
in
Pretty.block (
@@ -623,7 +623,7 @@
in Pretty.chunks (ps @| Pretty.block ([p, str ";;"])) end
| pr_stmt (MLClass (class, (v, (superclasses, classparams)))) =
let
- val w = "_" ^ Code_Name.first_upper v;
+ val w = "_" ^ Code_Printer.first_upper v;
fun pr_superclass_field (class, classrel) =
(concat o map str) [
deresolve classrel, ":", "'" ^ v, deresolve class
@@ -765,11 +765,11 @@
let
val (x, nsp_typ') = f nsp_typ
in (x, (nsp_fun, nsp_typ')) end;
- val mk_name_module = Code_Name.mk_name_module reserved_names NONE module_alias program;
+ val mk_name_module = Code_Printer.mk_name_module reserved_names NONE module_alias program;
fun mk_name_stmt upper name nsp =
let
- val (_, base) = Code_Name.dest_name name;
- val base' = if upper then Code_Name.first_upper base else base;
+ val (_, base) = Code_Printer.dest_name name;
+ val base' = if upper then Code_Printer.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) =
@@ -853,7 +853,7 @@
[]
|> fold (fold (insert (op =)) o Graph.imm_succs program) names
|> subtract (op =) names;
- val (module_names, _) = (split_list o map Code_Name.dest_name) names;
+ val (module_names, _) = (split_list o map Code_Printer.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"
@@ -863,7 +863,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_Name.dest_name) name';
+ val module_name' = (mk_name_module o fst o Code_Printer.dest_name) name';
in if module_name = module_name' then
map_node module_name_path (Graph.add_edge (name, name'))
else let
@@ -891,7 +891,7 @@
(rev (Graph.strong_conn program)));
fun deresolver prefix name =
let
- val module_name = (fst o Code_Name.dest_name) name;
+ val module_name = (fst o Code_Printer.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 =
@@ -914,7 +914,7 @@
val module_name = if null stmt_names then raw_module_name else SOME "Code";
val (deresolver, nodes) = ml_node_of_program labelled_name module_name
reserved_names raw_module_alias program;
- val reserved_names = Code_Name.make_vars reserved_names;
+ val reserved_names = Code_Printer.make_vars reserved_names;
fun pr_node prefix (Dummy _) =
NONE
| pr_node prefix (Stmt (_, stmt)) = if null stmt_names orelse
--- a/src/Tools/code/code_name.ML Sun Mar 22 11:56:22 2009 +0100
+++ b/src/Tools/code/code_name.ML Sun Mar 22 11:56:32 2009 +0100
@@ -6,45 +6,20 @@
signature CODE_NAME =
sig
- structure StringPairTab: TABLE
- val first_upper: string -> string
- val first_lower: string -> string
- val dest_name: string -> string * string
-
val purify_var: string -> string
val purify_tvar: string -> string
- val purify_sym: string -> string
- val purify_base: bool -> string -> string
+ val purify_base: string -> string
val check_modulename: string -> string
- type var_ctxt
- val make_vars: string list -> var_ctxt
- val intro_vars: string list -> var_ctxt -> var_ctxt
- val lookup_var: var_ctxt -> string -> string
-
val read_const_exprs: theory -> string list -> string list * string list
- val mk_name_module: Name.context -> string option -> (string -> string option)
- -> 'a Graph.T -> string -> string
end;
structure Code_Name: CODE_NAME =
struct
-(** auxiliary **)
-
-structure StringPairTab =
- TableFun(type key = string * string val ord = prod_ord fast_string_ord fast_string_ord);
-
-val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode;
-val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode;
-
-val dest_name =
- apfst Long_Name.implode o split_last o fst o split_last o Long_Name.explode;
-
-
(** purification **)
-fun purify_name upper lower =
+fun purify_name upper =
let
fun is_valid s = Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s orelse s = "'";
val is_junk = not o is_valid andf Symbol.is_regular;
@@ -55,9 +30,8 @@
--| junk))
::: Scan.repeat ((Scan.many1 is_valid >> implode) --| junk));
fun upper_lower cs = if upper then nth_map 0 Symbol.to_ascii_upper cs
- else if lower then (if forall Symbol.is_ascii_upper cs
- then map else nth_map 0) Symbol.to_ascii_lower cs
- else cs;
+ else (if forall Symbol.is_ascii_upper cs
+ then map else nth_map 0) Symbol.to_ascii_lower cs;
in
explode
#> scan_valids
@@ -68,7 +42,7 @@
end;
fun purify_var "" = "x"
- | purify_var v = purify_name false true v;
+ | purify_var v = purify_name false v;
fun purify_tvar "" = "'a"
| purify_tvar v =
@@ -81,52 +55,29 @@
(Scan.repeat ($$ "_" |-- $$ "_" >> (fn _ => ".") || Scan.one Symbol.is_regular))
#> implode
#> Long_Name.explode
- #> map (purify_name true false);
+ #> map (purify_name true);
(*FIMXE non-canonical function treating non-canonical names*)
-fun purify_base _ "op &" = "and"
- | purify_base _ "op |" = "or"
- | purify_base _ "op -->" = "implies"
- | purify_base _ "{}" = "empty"
- | purify_base _ "op :" = "member"
- | purify_base _ "op Int" = "intersect"
- | purify_base _ "op Un" = "union"
- | purify_base _ "*" = "product"
- | purify_base _ "+" = "sum"
- | purify_base lower s = if String.isPrefix "op =" s
- then "eq" ^ purify_name false lower s
- else purify_name false lower s;
-
-val purify_sym = purify_base false;
+fun purify_base "op &" = "and"
+ | purify_base "op |" = "or"
+ | purify_base "op -->" = "implies"
+ | purify_base "op :" = "member"
+ | purify_base "*" = "product"
+ | purify_base "+" = "sum"
+ | purify_base s = if String.isPrefix "op =" s
+ then "eq" ^ purify_name false s
+ else purify_name false s;
fun check_modulename mn =
let
val mns = Long_Name.explode mn;
- val mns' = map (purify_name true false) mns;
+ val mns' = map (purify_name true) mns;
in
if mns' = mns then mn else error ("Invalid module name: " ^ quote mn ^ "\n"
^ "perhaps try " ^ quote (Long_Name.implode mns'))
end;
-(** variable name contexts **)
-
-type var_ctxt = string Symtab.table * Name.context;
-
-fun make_vars names = (fold (fn name => Symtab.update_new (name, name)) names Symtab.empty,
- Name.make_context names);
-
-fun intro_vars names (namemap, namectxt) =
- let
- val (names', namectxt') = Name.variants names namectxt;
- val namemap' = fold2 (curry Symtab.update) names names' namemap;
- in (namemap', namectxt') end;
-
-fun lookup_var (namemap, _) name = case Symtab.lookup namemap name
- of SOME name' => name'
- | NONE => error ("Invalid name in context: " ^ quote name);
-
-
(** misc **)
fun read_const_exprs thy =
@@ -150,22 +101,4 @@
else ([Code_Unit.read_const thy s], []);
in pairself flat o split_list o map read_const_expr end;
-fun mk_name_module reserved_names 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))
- |> Long_Name.implode;
- fun mk_prefix name = case module_prefix
- of SOME module_prefix => Long_Name.append module_prefix name
- | NONE => name;
- val tab =
- Symtab.empty
- |> Graph.fold ((fn name => Symtab.default (name, (mk_alias #> mk_prefix) name))
- o fst o dest_name o fst)
- program
- in the o Symtab.lookup tab end;
-
end;
--- a/src/Tools/code/code_printer.ML Sun Mar 22 11:56:22 2009 +0100
+++ b/src/Tools/code/code_printer.ML Sun Mar 22 11:56:32 2009 +0100
@@ -16,6 +16,13 @@
val semicolon: Pretty.T list -> Pretty.T
val enum_default: string -> string -> string -> string -> Pretty.T list -> Pretty.T
+ val first_upper: string -> string
+ val first_lower: string -> string
+ type var_ctxt
+ val make_vars: string list -> var_ctxt
+ val intro_vars: string list -> var_ctxt -> var_ctxt
+ val lookup_var: var_ctxt -> string -> string
+
type lrx
val L: lrx
val R: lrx
@@ -42,14 +49,14 @@
-> fixity -> 'a list -> Pretty.T)) option * OuterParse.token list
val simple_const_syntax: (int * ((fixity -> iterm -> Pretty.T)
-> fixity -> (iterm * itype) list -> Pretty.T)) option -> const_syntax option
- val gen_pr_app: (thm -> Code_Name.var_ctxt -> const * iterm list -> Pretty.T list)
- -> (thm -> Code_Name.var_ctxt -> fixity -> iterm -> Pretty.T)
+ val gen_pr_app: (thm -> var_ctxt -> const * iterm list -> Pretty.T list)
+ -> (thm -> var_ctxt -> fixity -> iterm -> Pretty.T)
-> (string -> const_syntax option) -> Code_Thingol.naming
- -> thm -> Code_Name.var_ctxt -> fixity -> const * iterm list -> Pretty.T
+ -> thm -> var_ctxt -> fixity -> const * iterm list -> Pretty.T
val gen_pr_bind: ((string option * Pretty.T option) * itype -> Pretty.T)
- -> (thm -> Code_Name.var_ctxt -> fixity -> iterm -> Pretty.T)
+ -> (thm -> var_ctxt -> fixity -> iterm -> Pretty.T)
-> thm -> fixity
- -> (string option * iterm option) * itype -> Code_Name.var_ctxt -> Pretty.T * Code_Name.var_ctxt
+ -> (string option * iterm option) * itype -> var_ctxt -> Pretty.T * var_ctxt
type literals
val Literals: { literal_char: string -> string, literal_string: string -> string,
@@ -60,6 +67,10 @@
val literal_numeral: literals -> bool -> int -> string
val literal_list: literals -> Pretty.T list -> Pretty.T
val infix_cons: literals -> int * string
+
+ val mk_name_module: Name.context -> string option -> (string -> string option)
+ -> 'a Graph.T -> string -> string
+ val dest_name: string -> string * string
end;
structure Code_Printer : CODE_PRINTER =
@@ -83,6 +94,27 @@
| enum_default default sep opn cls xs = Pretty.enum sep opn cls xs;
+(** names and variable name contexts **)
+
+type var_ctxt = string Symtab.table * Name.context;
+
+fun make_vars names = (fold (fn name => Symtab.update_new (name, name)) names Symtab.empty,
+ Name.make_context names);
+
+fun intro_vars names (namemap, namectxt) =
+ let
+ val (names', namectxt') = Name.variants names namectxt;
+ val namemap' = fold2 (curry Symtab.update) names names' namemap;
+ in (namemap', namectxt') end;
+
+fun lookup_var (namemap, _) name = case Symtab.lookup namemap name
+ of SOME name' => name'
+ | NONE => error ("Invalid name in context: " ^ quote name);
+
+val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode;
+val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode;
+
+
(** syntax printer **)
(* binding priorities *)
@@ -125,8 +157,8 @@
type tyco_syntax = int * ((fixity -> itype -> Pretty.T)
-> fixity -> itype list -> Pretty.T);
-type const_syntax = int * ((Code_Name.var_ctxt -> fixity -> iterm -> Pretty.T)
- -> Code_Thingol.naming -> thm -> Code_Name.var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
+type const_syntax = int * ((var_ctxt -> fixity -> iterm -> Pretty.T)
+ -> Code_Thingol.naming -> thm -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
fun simple_const_syntax x = (Option.map o apsnd)
(fn pretty => fn pr => fn naming => fn thm => fn vars => pretty (pr vars)) x;
@@ -150,9 +182,9 @@
val vs = case pat
of SOME pat => Code_Thingol.fold_varnames (insert (op =)) pat []
| NONE => [];
- val vars' = Code_Name.intro_vars (the_list v) vars;
- val vars'' = Code_Name.intro_vars vs vars';
- val v' = Option.map (Code_Name.lookup_var vars') v;
+ val vars' = intro_vars (the_list v) vars;
+ val vars'' = intro_vars vs vars';
+ val v' = Option.map (lookup_var vars') v;
val pat' = Option.map (pr_term thm vars'' fxy) pat;
in (pr_bind ((v', pat'), ty), vars'') end;
@@ -239,4 +271,28 @@
val literal_list = #literal_list o dest_Literals;
val infix_cons = #infix_cons o dest_Literals;
+
+(** module name spaces **)
+
+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 =
+ 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))
+ |> Long_Name.implode;
+ fun mk_prefix name = case module_prefix
+ of SOME module_prefix => Long_Name.append module_prefix name
+ | NONE => name;
+ val tab =
+ Symtab.empty
+ |> Graph.fold ((fn name => Symtab.default (name, (mk_alias #> mk_prefix) name))
+ o fst o dest_name o fst)
+ program
+ in the o Symtab.lookup tab end;
+
end; (*struct*)
--- a/src/Tools/code/code_target.ML Sun Mar 22 11:56:22 2009 +0100
+++ b/src/Tools/code/code_target.ML Sun Mar 22 11:56:32 2009 +0100
@@ -82,11 +82,9 @@
(** theory data **)
-structure StringPairTab = Code_Name.StringPairTab;
-
datatype name_syntax_table = NameSyntaxTable of {
class: string Symtab.table,
- instance: unit StringPairTab.table,
+ instance: unit Symreltab.table,
tyco: tyco_syntax Symtab.table,
const: const_syntax Symtab.table
};
@@ -99,7 +97,7 @@
NameSyntaxTable { class = class2, instance = instance2, tyco = tyco2, const = const2 }) =
mk_name_syntax_table (
(Symtab.join (K snd) (class1, class2),
- StringPairTab.join (K snd) (instance1, instance2)),
+ Symreltab.join (K snd) (instance1, instance2)),
(Symtab.join (K snd) (tyco1, tyco2),
Symtab.join (K snd) (const1, const2))
);
@@ -194,7 +192,7 @@
thy
|> (CodeTargetData.map o apfst oo Symtab.map_default)
(target, mk_target ((serial (), seri), (([], Symtab.empty),
- (mk_name_syntax_table ((Symtab.empty, StringPairTab.empty), (Symtab.empty, Symtab.empty)),
+ (mk_name_syntax_table ((Symtab.empty, Symreltab.empty), (Symtab.empty, Symtab.empty)),
Symtab.empty))))
((map_target o apfst o apsnd o K) seri)
end;
@@ -262,11 +260,11 @@
in if add_del then
thy
|> (map_name_syntax target o apfst o apsnd)
- (StringPairTab.update (inst, ()))
+ (Symreltab.update (inst, ()))
else
thy
|> (map_name_syntax target o apfst o apsnd)
- (StringPairTab.delete_safe inst)
+ (Symreltab.delete_safe inst)
end;
fun gen_add_syntax_tyco prep_tyco target raw_tyco raw_syn thy =
@@ -407,7 +405,7 @@
|>> map_filter I;
val (names_class, class') = distill_names Code_Thingol.lookup_class class;
val names_inst = map_filter (Code_Thingol.lookup_instance naming)
- (StringPairTab.keys instance);
+ (Symreltab.keys instance);
val (names_tyco, tyco') = distill_names Code_Thingol.lookup_tyco tyco;
val (names_const, const') = distill_names Code_Thingol.lookup_const const;
val names_hidden = names_class @ names_inst @ names_tyco @ names_const;
--- a/src/Tools/code/code_thingol.ML Sun Mar 22 11:56:22 2009 +0100
+++ b/src/Tools/code/code_thingol.ML Sun Mar 22 11:56:32 2009 +0100
@@ -242,7 +242,7 @@
fun namify thy get_basename get_thyname name =
let
val prefix = get_thyname thy name;
- val base = (Code_Name.purify_base true o get_basename) name;
+ val base = (Code_Name.purify_base o get_basename) name;
in Long_Name.append prefix base end;
in
@@ -261,13 +261,11 @@
(* data *)
-structure StringPairTab = Code_Name.StringPairTab;
-
datatype naming = Naming of {
class: class Symtab.table * Name.context,
- classrel: string StringPairTab.table * Name.context,
+ classrel: string Symreltab.table * Name.context,
tyco: string Symtab.table * Name.context,
- instance: string StringPairTab.table * Name.context,
+ instance: string Symreltab.table * Name.context,
const: string Symtab.table * Name.context
}
@@ -275,9 +273,9 @@
val empty_naming = Naming {
class = (Symtab.empty, Name.context),
- classrel = (StringPairTab.empty, Name.context),
+ classrel = (Symreltab.empty, Name.context),
tyco = (Symtab.empty, Name.context),
- instance = (StringPairTab.empty, Name.context),
+ instance = (Symreltab.empty, Name.context),
const = (Symtab.empty, Name.context)
};
@@ -334,22 +332,22 @@
val lookup_class = add_suffix suffix_class
oo Symtab.lookup o fst o #class o dest_Naming;
val lookup_classrel = add_suffix suffix_classrel
- oo StringPairTab.lookup o fst o #classrel o dest_Naming;
+ oo Symreltab.lookup o fst o #classrel o dest_Naming;
val lookup_tyco = add_suffix suffix_tyco
oo Symtab.lookup o fst o #tyco o dest_Naming;
val lookup_instance = add_suffix suffix_instance
- oo StringPairTab.lookup o fst o #instance o dest_Naming;
+ oo Symreltab.lookup o fst o #instance o dest_Naming;
val lookup_const = add_suffix suffix_const
oo Symtab.lookup o fst o #const o dest_Naming;
fun declare_class thy = declare thy map_class
lookup_class Symtab.update_new namify_class;
fun declare_classrel thy = declare thy map_classrel
- lookup_classrel StringPairTab.update_new namify_classrel;
+ lookup_classrel Symreltab.update_new namify_classrel;
fun declare_tyco thy = declare thy map_tyco
lookup_tyco Symtab.update_new namify_tyco;
fun declare_instance thy = declare thy map_instance
- lookup_instance StringPairTab.update_new namify_instance;
+ lookup_instance Symreltab.update_new namify_instance;
fun declare_const thy = declare thy map_const
lookup_const Symtab.update_new namify_const;