--- a/src/HOL/IsaMakefile Mon May 04 14:49:50 2009 +0200
+++ b/src/HOL/IsaMakefile Mon May 04 14:49:51 2009 +0200
@@ -92,7 +92,6 @@
$(SRC)/Tools/auto_solve.ML \
$(SRC)/Tools/code/code_haskell.ML \
$(SRC)/Tools/code/code_ml.ML \
- $(SRC)/Tools/code/code_name.ML \
$(SRC)/Tools/code/code_printer.ML \
$(SRC)/Tools/code/code_target.ML \
$(SRC)/Tools/code/code_thingol.ML \
--- a/src/HOL/Tools/recfun_codegen.ML Mon May 04 14:49:50 2009 +0200
+++ b/src/HOL/Tools/recfun_codegen.ML Mon May 04 14:49:51 2009 +0200
@@ -59,7 +59,7 @@
|> expand_eta thy
|> map (AxClass.overload thy)
|> map_filter (meta_eq_to_obj_eq thy)
- |> Code_Unit.norm_varnames thy Code_Name.purify_tvar Code_Name.purify_var
+ |> Code_Unit.norm_varnames thy
|> map (rpair opt_name)
in if null thms then NONE else SOME thms end;
--- a/src/Pure/Isar/code_unit.ML Mon May 04 14:49:50 2009 +0200
+++ b/src/Pure/Isar/code_unit.ML Mon May 04 14:49:51 2009 +0200
@@ -45,7 +45,7 @@
val rewrite_eqn: simpset -> thm -> thm
val rewrite_head: thm list -> thm -> thm
val norm_args: theory -> thm list -> thm list
- val norm_varnames: theory -> (string -> string) -> (string -> string) -> thm list -> thm list
+ val norm_varnames: theory -> thm list -> thm list
(*case certificates*)
val case_cert: thm -> string * (int * string list)
@@ -161,9 +161,10 @@
|> map (Conv.fconv_rule Drule.beta_eta_conversion)
end;
-fun canonical_tvars thy purify_tvar thm =
+fun canonical_tvars thy thm =
let
val ctyp = Thm.ctyp_of thy;
+ val purify_tvar = unprefix "'" #> Name.desymbolize false #> prefix "'";
fun tvars_subst_for thm = (fold_types o fold_atyps)
(fn TVar (v_i as (v, _), sort) => let
val v' = purify_tvar v
@@ -180,9 +181,10 @@
val (_, inst) = fold mk_inst (tvars_subst_for thm) (maxidx + 1, []);
in Thm.instantiate (inst, []) thm end;
-fun canonical_vars thy purify_var thm =
+fun canonical_vars thy thm =
let
val cterm = Thm.cterm_of thy;
+ val purify_var = Name.desymbolize false;
fun vars_subst_for thm = fold_aterms
(fn Var (v_i as (v, _), ty) => let
val v' = purify_var v
@@ -199,13 +201,14 @@
val (_, inst) = fold mk_inst (vars_subst_for thm) (maxidx + 1, []);
in Thm.instantiate ([], inst) thm end;
-fun canonical_absvars purify_var thm =
+fun canonical_absvars thm =
let
val t = Thm.plain_prop_of thm;
+ val purify_var = Name.desymbolize false;
val t' = Term.map_abs_vars purify_var t;
in Thm.rename_boundvars t t' thm end;
-fun norm_varnames thy purify_tvar purify_var thms =
+fun norm_varnames thy thms =
let
fun burrow_thms f [] = []
| burrow_thms f thms =
@@ -215,10 +218,10 @@
|> Conjunction.elim_balanced (length thms)
in
thms
- |> map (canonical_vars thy purify_var)
- |> map (canonical_absvars purify_var)
+ |> map (canonical_vars thy)
+ |> map canonical_absvars
|> map Drule.zero_var_indexes
- |> burrow_thms (canonical_tvars thy purify_tvar)
+ |> burrow_thms (canonical_tvars thy)
|> Drule.zero_var_indexes_list
end;
--- a/src/Tools/Code_Generator.thy Mon May 04 14:49:50 2009 +0200
+++ b/src/Tools/Code_Generator.thy Mon May 04 14:49:51 2009 +0200
@@ -9,7 +9,6 @@
uses
"~~/src/Tools/value.ML"
"~~/src/Tools/quickcheck.ML"
- "~~/src/Tools/code/code_name.ML"
"~~/src/Tools/code/code_wellsorted.ML"
"~~/src/Tools/code/code_thingol.ML"
"~~/src/Tools/code/code_printer.ML"
--- a/src/Tools/code/code_name.ML Mon May 04 14:49:50 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,74 +0,0 @@
-(* Title: Tools/code/code_name.ML
- Author: Florian Haftmann, TU Muenchen
-
-Some code generator infrastructure concerning names.
-*)
-
-signature CODE_NAME =
-sig
- val purify_name: bool -> string -> string
- val purify_var: string -> string
- val purify_tvar: string -> string
- val purify_base: string -> string
-
- val read_const_exprs: theory -> string list -> string list * string list
-end;
-
-structure Code_Name: CODE_NAME =
-struct
-
-(** purification **)
-
-fun purify_name upper =
- let
- fun upper_lower cs = if upper then nth_map 0 Symbol.to_ascii_upper cs
- else (if forall Symbol.is_ascii_upper cs
- then map else nth_map 0) Symbol.to_ascii_lower cs;
- in
- Name.desymbolize
- #> explode
- #> upper_lower
- #> implode
- end;
-
-val purify_var = purify_name false;
-
-fun purify_tvar "" = "'a"
- | purify_tvar v =
- (unprefix "'" #> purify_name false #> prefix "'") v;
-
-(*FIMXE non-canonical function treating non-canonical names*)
-fun purify_base "op &" = "and"
- | purify_base "op |" = "or"
- | purify_base "op -->" = "implies"
- | purify_base "op :" = "member"
- | purify_base "op =" = "eq"
- | purify_base "*" = "product"
- | purify_base "+" = "sum"
- | purify_base s = purify_name false s;
-
-
-(** misc **)
-
-fun read_const_exprs thy =
- let
- fun consts_of some_thyname =
- let
- val thy' = case some_thyname
- of SOME thyname => ThyInfo.the_theory thyname thy
- | NONE => thy;
- val cs = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I)
- ((snd o #constants o Consts.dest o #consts o Sign.rep_sg) thy') [];
- fun belongs_here c =
- not (exists (fn thy'' => Sign.declared_const thy'' c) (Theory.parents_of thy'))
- in case some_thyname
- of NONE => cs
- | SOME thyname => filter belongs_here cs
- end;
- fun read_const_expr "*" = ([], consts_of NONE)
- | read_const_expr s = if String.isSuffix ".*" s
- then ([], consts_of (SOME (unsuffix ".*" s)))
- else ([Code_Unit.read_const thy s], []);
- in pairself flat o split_list o map read_const_expr end;
-
-end;
--- a/src/Tools/code/code_target.ML Mon May 04 14:49:50 2009 +0200
+++ b/src/Tools/code/code_target.ML Mon May 04 14:49:51 2009 +0200
@@ -326,7 +326,7 @@
fun add_module_alias target (thyname, modlname) =
let
val xs = Long_Name.explode modlname;
- val xs' = map (Code_Name.purify_name true) xs;
+ val xs' = map (Name.desymbolize true) xs;
in if xs' = xs
then map_module_alias target (Symtab.update (thyname, modlname))
else error ("Invalid module name: " ^ quote modlname ^ "\n"
@@ -502,7 +502,7 @@
fun read_const_exprs thy cs =
let
- val (cs1, cs2) = Code_Name.read_const_exprs thy cs;
+ val (cs1, cs2) = Code_Thingol.read_const_exprs thy cs;
val (names3, (naming, program)) = Code_Thingol.consts_program thy cs2;
val names4 = transitivly_non_empty_funs thy naming program;
val cs5 = map_filter
--- a/src/Tools/code/code_thingol.ML Mon May 04 14:49:50 2009 +0200
+++ b/src/Tools/code/code_thingol.ML Mon May 04 14:49:51 2009 +0200
@@ -81,6 +81,7 @@
val is_cons: program -> string -> bool
val contr_classparam_typs: program -> string -> itype option list
+ val read_const_exprs: theory -> string list -> string list * string list
val consts_program: theory -> string list -> string list * (naming * program)
val cached_program: theory -> naming * program
val eval_conv: theory -> (sort -> sort)
@@ -239,10 +240,18 @@
| NONE => (case Code.get_datatype_of_constr thy c
of SOME dtco => thyname_of_tyco thy dtco
| NONE => thyname_of thy (Consts.the_tags (Sign.consts_of thy)) c);
+ fun purify_base "op &" = "and"
+ | purify_base "op |" = "or"
+ | purify_base "op -->" = "implies"
+ | purify_base "op :" = "member"
+ | purify_base "op =" = "eq"
+ | purify_base "*" = "product"
+ | purify_base "+" = "sum"
+ | purify_base s = Name.desymbolize false s;
fun namify thy get_basename get_thyname name =
let
val prefix = get_thyname thy name;
- val base = (Code_Name.purify_base o get_basename) name;
+ val base = (purify_base o get_basename) name;
in Long_Name.append prefix base end;
in
@@ -782,6 +791,27 @@
(** diagnostic commands **)
+fun read_const_exprs thy =
+ let
+ fun consts_of some_thyname =
+ let
+ val thy' = case some_thyname
+ of SOME thyname => ThyInfo.the_theory thyname thy
+ | NONE => thy;
+ val cs = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I)
+ ((snd o #constants o Consts.dest o #consts o Sign.rep_sg) thy') [];
+ fun belongs_here c =
+ not (exists (fn thy'' => Sign.declared_const thy'' c) (Theory.parents_of thy'))
+ in case some_thyname
+ of NONE => cs
+ | SOME thyname => filter belongs_here cs
+ end;
+ fun read_const_expr "*" = ([], consts_of NONE)
+ | read_const_expr s = if String.isSuffix ".*" s
+ then ([], consts_of (SOME (unsuffix ".*" s)))
+ else ([Code_Unit.read_const thy s], []);
+ in pairself flat o split_list o map read_const_expr end;
+
fun code_depgr thy consts =
let
val (_, eqngr) = Code_Wellsorted.obtain thy consts [];
@@ -818,8 +848,8 @@
structure P = OuterParse
and K = OuterKeyword
-fun code_thms_cmd thy = code_thms thy o op @ o Code_Name.read_const_exprs thy;
-fun code_deps_cmd thy = code_deps thy o op @ o Code_Name.read_const_exprs thy;
+fun code_thms_cmd thy = code_thms thy o op @ o read_const_exprs thy;
+fun code_deps_cmd thy = code_deps thy o op @ o read_const_exprs thy;
in
--- a/src/Tools/code/code_wellsorted.ML Mon May 04 14:49:50 2009 +0200
+++ b/src/Tools/code/code_wellsorted.ML Mon May 04 14:49:51 2009 +0200
@@ -107,7 +107,7 @@
| NONE => let
val eqns = Code.these_eqns thy c
|> burrow_fst (Code_Unit.norm_args thy)
- |> burrow_fst (Code_Unit.norm_varnames thy Code_Name.purify_tvar Code_Name.purify_var);
+ |> burrow_fst (Code_Unit.norm_varnames thy);
val ((lhs, _), rhss) = tyscm_rhss_of thy c eqns;
in ((lhs, rhss), eqns) end;