removed code_name module
authorhaftmann
Mon May 04 14:49:51 2009 +0200 (2009-05-04)
changeset 3103664ff53fc0c0c
parent 31035 de0a20a030fd
child 31037 ac8669134e7a
removed code_name module
src/HOL/IsaMakefile
src/HOL/Tools/recfun_codegen.ML
src/Pure/Isar/code_unit.ML
src/Tools/Code_Generator.thy
src/Tools/code/code_name.ML
src/Tools/code/code_target.ML
src/Tools/code/code_thingol.ML
src/Tools/code/code_wellsorted.ML
     1.1 --- a/src/HOL/IsaMakefile	Mon May 04 14:49:50 2009 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Mon May 04 14:49:51 2009 +0200
     1.3 @@ -92,7 +92,6 @@
     1.4    $(SRC)/Tools/auto_solve.ML \
     1.5    $(SRC)/Tools/code/code_haskell.ML \
     1.6    $(SRC)/Tools/code/code_ml.ML \
     1.7 -  $(SRC)/Tools/code/code_name.ML \
     1.8    $(SRC)/Tools/code/code_printer.ML \
     1.9    $(SRC)/Tools/code/code_target.ML \
    1.10    $(SRC)/Tools/code/code_thingol.ML \
     2.1 --- a/src/HOL/Tools/recfun_codegen.ML	Mon May 04 14:49:50 2009 +0200
     2.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Mon May 04 14:49:51 2009 +0200
     2.3 @@ -59,7 +59,7 @@
     2.4        |> expand_eta thy
     2.5        |> map (AxClass.overload thy)
     2.6        |> map_filter (meta_eq_to_obj_eq thy)
     2.7 -      |> Code_Unit.norm_varnames thy Code_Name.purify_tvar Code_Name.purify_var
     2.8 +      |> Code_Unit.norm_varnames thy
     2.9        |> map (rpair opt_name)
    2.10    in if null thms then NONE else SOME thms end;
    2.11  
     3.1 --- a/src/Pure/Isar/code_unit.ML	Mon May 04 14:49:50 2009 +0200
     3.2 +++ b/src/Pure/Isar/code_unit.ML	Mon May 04 14:49:51 2009 +0200
     3.3 @@ -45,7 +45,7 @@
     3.4    val rewrite_eqn: simpset -> thm -> thm
     3.5    val rewrite_head: thm list -> thm -> thm
     3.6    val norm_args: theory -> thm list -> thm list 
     3.7 -  val norm_varnames: theory -> (string -> string) -> (string -> string) -> thm list -> thm list
     3.8 +  val norm_varnames: theory -> thm list -> thm list
     3.9  
    3.10    (*case certificates*)
    3.11    val case_cert: thm -> string * (int * string list)
    3.12 @@ -161,9 +161,10 @@
    3.13      |> map (Conv.fconv_rule Drule.beta_eta_conversion)
    3.14    end;
    3.15  
    3.16 -fun canonical_tvars thy purify_tvar thm =
    3.17 +fun canonical_tvars thy thm =
    3.18    let
    3.19      val ctyp = Thm.ctyp_of thy;
    3.20 +    val purify_tvar = unprefix "'" #> Name.desymbolize false #> prefix "'";
    3.21      fun tvars_subst_for thm = (fold_types o fold_atyps)
    3.22        (fn TVar (v_i as (v, _), sort) => let
    3.23              val v' = purify_tvar v
    3.24 @@ -180,9 +181,10 @@
    3.25      val (_, inst) = fold mk_inst (tvars_subst_for thm) (maxidx + 1, []);
    3.26    in Thm.instantiate (inst, []) thm end;
    3.27  
    3.28 -fun canonical_vars thy purify_var thm =
    3.29 +fun canonical_vars thy thm =
    3.30    let
    3.31      val cterm = Thm.cterm_of thy;
    3.32 +    val purify_var = Name.desymbolize false;
    3.33      fun vars_subst_for thm = fold_aterms
    3.34        (fn Var (v_i as (v, _), ty) => let
    3.35              val v' = purify_var v
    3.36 @@ -199,13 +201,14 @@
    3.37      val (_, inst) = fold mk_inst (vars_subst_for thm) (maxidx + 1, []);
    3.38    in Thm.instantiate ([], inst) thm end;
    3.39  
    3.40 -fun canonical_absvars purify_var thm =
    3.41 +fun canonical_absvars thm =
    3.42    let
    3.43      val t = Thm.plain_prop_of thm;
    3.44 +    val purify_var = Name.desymbolize false;
    3.45      val t' = Term.map_abs_vars purify_var t;
    3.46    in Thm.rename_boundvars t t' thm end;
    3.47  
    3.48 -fun norm_varnames thy purify_tvar purify_var thms =
    3.49 +fun norm_varnames thy thms =
    3.50    let
    3.51      fun burrow_thms f [] = []
    3.52        | burrow_thms f thms =
    3.53 @@ -215,10 +218,10 @@
    3.54            |> Conjunction.elim_balanced (length thms)
    3.55    in
    3.56      thms
    3.57 -    |> map (canonical_vars thy purify_var)
    3.58 -    |> map (canonical_absvars purify_var)
    3.59 +    |> map (canonical_vars thy)
    3.60 +    |> map canonical_absvars
    3.61      |> map Drule.zero_var_indexes
    3.62 -    |> burrow_thms (canonical_tvars thy purify_tvar)
    3.63 +    |> burrow_thms (canonical_tvars thy)
    3.64      |> Drule.zero_var_indexes_list
    3.65    end;
    3.66  
     4.1 --- a/src/Tools/Code_Generator.thy	Mon May 04 14:49:50 2009 +0200
     4.2 +++ b/src/Tools/Code_Generator.thy	Mon May 04 14:49:51 2009 +0200
     4.3 @@ -9,7 +9,6 @@
     4.4  uses
     4.5    "~~/src/Tools/value.ML"
     4.6    "~~/src/Tools/quickcheck.ML"
     4.7 -  "~~/src/Tools/code/code_name.ML"
     4.8    "~~/src/Tools/code/code_wellsorted.ML" 
     4.9    "~~/src/Tools/code/code_thingol.ML"
    4.10    "~~/src/Tools/code/code_printer.ML"
     5.1 --- a/src/Tools/code/code_name.ML	Mon May 04 14:49:50 2009 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,74 +0,0 @@
     5.4 -(*  Title:      Tools/code/code_name.ML
     5.5 -    Author:     Florian Haftmann, TU Muenchen
     5.6 -
     5.7 -Some code generator infrastructure concerning names.
     5.8 -*)
     5.9 -
    5.10 -signature CODE_NAME =
    5.11 -sig
    5.12 -  val purify_name: bool -> string -> string
    5.13 -  val purify_var: string -> string
    5.14 -  val purify_tvar: string -> string
    5.15 -  val purify_base: string -> string
    5.16 -
    5.17 -  val read_const_exprs: theory -> string list -> string list * string list
    5.18 -end;
    5.19 -
    5.20 -structure Code_Name: CODE_NAME =
    5.21 -struct
    5.22 -
    5.23 -(** purification **)
    5.24 -
    5.25 -fun purify_name upper = 
    5.26 -  let
    5.27 -    fun upper_lower cs = if upper then nth_map 0 Symbol.to_ascii_upper cs
    5.28 -      else (if forall Symbol.is_ascii_upper cs
    5.29 -        then map else nth_map 0) Symbol.to_ascii_lower cs;
    5.30 -  in
    5.31 -    Name.desymbolize
    5.32 -    #> explode
    5.33 -    #> upper_lower
    5.34 -    #> implode
    5.35 -  end;
    5.36 -
    5.37 -val purify_var = purify_name false;
    5.38 -
    5.39 -fun purify_tvar "" = "'a"
    5.40 -  | purify_tvar v =
    5.41 -      (unprefix "'" #> purify_name false #> prefix "'") v;
    5.42 -
    5.43 -(*FIMXE non-canonical function treating non-canonical names*)
    5.44 -fun purify_base "op &" = "and"
    5.45 -  | purify_base "op |" = "or"
    5.46 -  | purify_base "op -->" = "implies"
    5.47 -  | purify_base "op :" = "member"
    5.48 -  | purify_base "op =" = "eq"
    5.49 -  | purify_base "*" = "product"
    5.50 -  | purify_base "+" = "sum"
    5.51 -  | purify_base s = purify_name false s;
    5.52 -
    5.53 -
    5.54 -(** misc **)
    5.55 -
    5.56 -fun read_const_exprs thy =
    5.57 -  let
    5.58 -    fun consts_of some_thyname =
    5.59 -      let
    5.60 -        val thy' = case some_thyname
    5.61 -         of SOME thyname => ThyInfo.the_theory thyname thy
    5.62 -          | NONE => thy;
    5.63 -        val cs = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I)
    5.64 -          ((snd o #constants o Consts.dest o #consts o Sign.rep_sg) thy') [];
    5.65 -        fun belongs_here c =
    5.66 -          not (exists (fn thy'' => Sign.declared_const thy'' c) (Theory.parents_of thy'))
    5.67 -      in case some_thyname
    5.68 -       of NONE => cs
    5.69 -        | SOME thyname => filter belongs_here cs
    5.70 -      end;
    5.71 -    fun read_const_expr "*" = ([], consts_of NONE)
    5.72 -      | read_const_expr s = if String.isSuffix ".*" s
    5.73 -          then ([], consts_of (SOME (unsuffix ".*" s)))
    5.74 -          else ([Code_Unit.read_const thy s], []);
    5.75 -  in pairself flat o split_list o map read_const_expr end;
    5.76 -
    5.77 -end;
     6.1 --- a/src/Tools/code/code_target.ML	Mon May 04 14:49:50 2009 +0200
     6.2 +++ b/src/Tools/code/code_target.ML	Mon May 04 14:49:51 2009 +0200
     6.3 @@ -326,7 +326,7 @@
     6.4  fun add_module_alias target (thyname, modlname) =
     6.5    let
     6.6      val xs = Long_Name.explode modlname;
     6.7 -    val xs' = map (Code_Name.purify_name true) xs;
     6.8 +    val xs' = map (Name.desymbolize true) xs;
     6.9    in if xs' = xs
    6.10      then map_module_alias target (Symtab.update (thyname, modlname))
    6.11      else error ("Invalid module name: " ^ quote modlname ^ "\n"
    6.12 @@ -502,7 +502,7 @@
    6.13  
    6.14  fun read_const_exprs thy cs =
    6.15    let
    6.16 -    val (cs1, cs2) = Code_Name.read_const_exprs thy cs;
    6.17 +    val (cs1, cs2) = Code_Thingol.read_const_exprs thy cs;
    6.18      val (names3, (naming, program)) = Code_Thingol.consts_program thy cs2;
    6.19      val names4 = transitivly_non_empty_funs thy naming program;
    6.20      val cs5 = map_filter
     7.1 --- a/src/Tools/code/code_thingol.ML	Mon May 04 14:49:50 2009 +0200
     7.2 +++ b/src/Tools/code/code_thingol.ML	Mon May 04 14:49:51 2009 +0200
     7.3 @@ -81,6 +81,7 @@
     7.4    val is_cons: program -> string -> bool
     7.5    val contr_classparam_typs: program -> string -> itype option list
     7.6  
     7.7 +  val read_const_exprs: theory -> string list -> string list * string list
     7.8    val consts_program: theory -> string list -> string list * (naming * program)
     7.9    val cached_program: theory -> naming * program
    7.10    val eval_conv: theory -> (sort -> sort)
    7.11 @@ -239,10 +240,18 @@
    7.12      | NONE => (case Code.get_datatype_of_constr thy c
    7.13         of SOME dtco => thyname_of_tyco thy dtco
    7.14          | NONE => thyname_of thy (Consts.the_tags (Sign.consts_of thy)) c);
    7.15 +  fun purify_base "op &" = "and"
    7.16 +    | purify_base "op |" = "or"
    7.17 +    | purify_base "op -->" = "implies"
    7.18 +    | purify_base "op :" = "member"
    7.19 +    | purify_base "op =" = "eq"
    7.20 +    | purify_base "*" = "product"
    7.21 +    | purify_base "+" = "sum"
    7.22 +    | purify_base s = Name.desymbolize false s;
    7.23    fun namify thy get_basename get_thyname name =
    7.24      let
    7.25        val prefix = get_thyname thy name;
    7.26 -      val base = (Code_Name.purify_base o get_basename) name;
    7.27 +      val base = (purify_base o get_basename) name;
    7.28      in Long_Name.append prefix base end;
    7.29  in
    7.30  
    7.31 @@ -782,6 +791,27 @@
    7.32  
    7.33  (** diagnostic commands **)
    7.34  
    7.35 +fun read_const_exprs thy =
    7.36 +  let
    7.37 +    fun consts_of some_thyname =
    7.38 +      let
    7.39 +        val thy' = case some_thyname
    7.40 +         of SOME thyname => ThyInfo.the_theory thyname thy
    7.41 +          | NONE => thy;
    7.42 +        val cs = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I)
    7.43 +          ((snd o #constants o Consts.dest o #consts o Sign.rep_sg) thy') [];
    7.44 +        fun belongs_here c =
    7.45 +          not (exists (fn thy'' => Sign.declared_const thy'' c) (Theory.parents_of thy'))
    7.46 +      in case some_thyname
    7.47 +       of NONE => cs
    7.48 +        | SOME thyname => filter belongs_here cs
    7.49 +      end;
    7.50 +    fun read_const_expr "*" = ([], consts_of NONE)
    7.51 +      | read_const_expr s = if String.isSuffix ".*" s
    7.52 +          then ([], consts_of (SOME (unsuffix ".*" s)))
    7.53 +          else ([Code_Unit.read_const thy s], []);
    7.54 +  in pairself flat o split_list o map read_const_expr end;
    7.55 +
    7.56  fun code_depgr thy consts =
    7.57    let
    7.58      val (_, eqngr) = Code_Wellsorted.obtain thy consts [];
    7.59 @@ -818,8 +848,8 @@
    7.60  structure P = OuterParse
    7.61  and K = OuterKeyword
    7.62  
    7.63 -fun code_thms_cmd thy = code_thms thy o op @ o Code_Name.read_const_exprs thy;
    7.64 -fun code_deps_cmd thy = code_deps thy o op @ o Code_Name.read_const_exprs thy;
    7.65 +fun code_thms_cmd thy = code_thms thy o op @ o read_const_exprs thy;
    7.66 +fun code_deps_cmd thy = code_deps thy o op @ o read_const_exprs thy;
    7.67  
    7.68  in
    7.69  
     8.1 --- a/src/Tools/code/code_wellsorted.ML	Mon May 04 14:49:50 2009 +0200
     8.2 +++ b/src/Tools/code/code_wellsorted.ML	Mon May 04 14:49:51 2009 +0200
     8.3 @@ -107,7 +107,7 @@
     8.4      | NONE => let
     8.5          val eqns = Code.these_eqns thy c
     8.6            |> burrow_fst (Code_Unit.norm_args thy)
     8.7 -          |> burrow_fst (Code_Unit.norm_varnames thy Code_Name.purify_tvar Code_Name.purify_var);
     8.8 +          |> burrow_fst (Code_Unit.norm_varnames thy);
     8.9          val ((lhs, _), rhss) = tyscm_rhss_of thy c eqns;
    8.10        in ((lhs, rhss), eqns) end;
    8.11