different handling of type variable names
authorhaftmann
Wed Dec 27 19:10:06 2006 +0100 (2006-12-27)
changeset 219154e63c55f4cb4
parent 21914 77372f38aa98
child 21916 68c848f636bb
different handling of type variable names
src/Pure/Tools/codegen_funcgr.ML
src/Pure/Tools/codegen_names.ML
     1.1 --- a/src/Pure/Tools/codegen_funcgr.ML	Wed Dec 27 19:10:05 2006 +0100
     1.2 +++ b/src/Pure/Tools/codegen_funcgr.ML	Wed Dec 27 19:10:06 2006 +0100
     1.3 @@ -73,7 +73,7 @@
     1.4    let
     1.5      fun tvars_subst_for thm = (fold_types o fold_atyps)
     1.6        (fn TVar (v_i as (v, _), sort) => let
     1.7 -            val v' = CodegenNames.purify_var v
     1.8 +            val v' = CodegenNames.purify_tvar v
     1.9            in if v = v' then I
    1.10            else insert (op =) (v_i, (v', sort)) end
    1.11          | _ => I) (prop_of thm) [];
     2.1 --- a/src/Pure/Tools/codegen_names.ML	Wed Dec 27 19:10:05 2006 +0100
     2.2 +++ b/src/Pure/Tools/codegen_names.ML	Wed Dec 27 19:10:06 2006 +0100
     2.3 @@ -3,7 +3,7 @@
     2.4      Author:     Florian Haftmann, TU Muenchen
     2.5  
     2.6  Naming policies for code generation: prefixing any name by corresponding theory name,
     2.7 -conversion to alphanumeric representation, shallow name spaces.
     2.8 +conversion to alphanumeric representation, name space identifier.
     2.9  Mappings are incrementally cached.
    2.10  *)
    2.11  
    2.12 @@ -20,13 +20,8 @@
    2.13    val const: theory -> CodegenConsts.const -> const
    2.14    val const_rev: theory -> const -> CodegenConsts.const option
    2.15    val purify_var: string -> string
    2.16 +  val purify_tvar: string -> string
    2.17    val check_modulename: string -> string
    2.18 -  val has_nsp: string -> string -> bool
    2.19 -  val nsp_class: string
    2.20 -  val nsp_tyco: string
    2.21 -  val nsp_inst: string
    2.22 -  val nsp_fun: string
    2.23 -  val nsp_dtco: string
    2.24  end;
    2.25  
    2.26  structure CodegenNames: CODEGEN_NAMES =
    2.27 @@ -225,10 +220,11 @@
    2.28    end
    2.29  
    2.30  fun purify_var "" = "x"
    2.31 -  | purify_var v =
    2.32 -      if nth (explode v) 0 = "'"
    2.33 -      then (unprefix "'" #> purify_name #> purify_lower #> prefix "'") v
    2.34 -      else (purify_name #> purify_lower) v;
    2.35 +  | purify_var v = (purify_name #> purify_lower) v;
    2.36 +
    2.37 +fun purify_tvar "" = "'a"
    2.38 +  | purify_tvar v =
    2.39 +      (unprefix "'" #> explode #> filter Symbol.is_ascii_letter #> cons "'" #> implode) v;
    2.40  
    2.41  val purify_idf = purify_op #> purify_name;
    2.42  val purify_prefix = map (purify_idf #> purify_upper);
    2.43 @@ -274,32 +270,15 @@
    2.44  val nsp_class = "class";
    2.45  val nsp_tyco = "tyco";
    2.46  val nsp_inst = "inst";
    2.47 -val nsp_fun = "fun";
    2.48 -val nsp_dtco = "dtco";
    2.49 +val nsp_const = "const";
    2.50  
    2.51 -fun add_nsp shallow name =
    2.52 -  name
    2.53 -  |> NameSpace.explode
    2.54 -  |> split_last
    2.55 -  |> apsnd (single #> cons shallow)
    2.56 -  |> (op @)
    2.57 -  |> NameSpace.implode;
    2.58 +fun add_nsp nsp name =
    2.59 +  NameSpace.append name nsp
    2.60  
    2.61 -fun dest_nsp nsp nspname =
    2.62 -  let
    2.63 -    val xs = NameSpace.explode nspname;
    2.64 -    val (ys, base) = split_last xs;
    2.65 -    val (module, shallow) = split_last ys;
    2.66 -  in
    2.67 -    if nsp = shallow
    2.68 -   then (SOME o NameSpace.implode) (module @ [base])
    2.69 -    else NONE
    2.70 -  end;
    2.71 -
    2.72 -val has_nsp = is_some oo dest_nsp;
    2.73 -
    2.74 -fun if_nsp nsp f idf =
    2.75 -  Option.map f (dest_nsp nsp idf);
    2.76 +fun dest_nsp nsp name =
    2.77 +  if NameSpace.base name = nsp
    2.78 +  then SOME (NameSpace.qualifier name)
    2.79 +  else NONE;
    2.80  
    2.81  
    2.82  (* external interfaces *)
    2.83 @@ -313,11 +292,10 @@
    2.84  fun instance thy =
    2.85    get thy #instance Insttab.lookup map_inst Insttab.update instance_policy
    2.86    #> add_nsp nsp_inst;
    2.87 -fun const thy c_ty = case CodegenConsts.norm thy c_ty
    2.88 - of (c_tys as (c, tys)) => add_nsp (if (is_some o CodegenData.get_datatype_of_constr thy) c_tys
    2.89 -     then nsp_dtco
    2.90 -   else nsp_fun)
    2.91 -  (get thy #const Consttab.lookup map_const Consttab.update const_policy c_tys);
    2.92 +fun const thy =
    2.93 +  CodegenConsts.norm thy
    2.94 +  #> get thy #const Consttab.lookup map_const Consttab.update const_policy 
    2.95 +  #> add_nsp nsp_const;
    2.96  
    2.97  fun class_rev thy =
    2.98    dest_nsp nsp_class
    2.99 @@ -328,12 +306,8 @@
   2.100  fun instance_rev thy =
   2.101    dest_nsp nsp_inst
   2.102    #> Option.map (rev thy #instance "instance");
   2.103 -fun const_rev thy nspname =
   2.104 -  (case dest_nsp nsp_fun nspname
   2.105 -   of name as SOME _ => name
   2.106 -    | _ => (case dest_nsp nsp_dtco nspname
   2.107 -   of name as SOME _ => name
   2.108 -    | _ => NONE))
   2.109 -  |> Option.map (rev thy #const "constant");
   2.110 +fun const_rev thy =
   2.111 +  dest_nsp nsp_const
   2.112 +  #> Option.map (rev thy #const "constant");
   2.113  
   2.114  end;