added handling for explicit classrel witnesses
authorhaftmann
Fri Dec 29 12:11:04 2006 +0100 (2006-12-29)
changeset 219279677abe5d374
parent 21926 1091904ddb19
child 21928 266c2b1fbd6b
added handling for explicit classrel witnesses
src/Pure/Tools/codegen_names.ML
     1.1 --- a/src/Pure/Tools/codegen_names.ML	Fri Dec 29 12:11:03 2006 +0100
     1.2 +++ b/src/Pure/Tools/codegen_names.ML	Fri Dec 29 12:11:04 2006 +0100
     1.3 @@ -13,6 +13,8 @@
     1.4    type const = string
     1.5    val class: theory -> class -> class
     1.6    val class_rev: theory -> class -> class option
     1.7 +  val classrel: theory -> class * class -> string
     1.8 +  val classrel_rev: theory -> string -> (class * class) option
     1.9    val tyco: theory -> tyco -> tyco
    1.10    val tyco_rev: theory -> tyco -> tyco option
    1.11    val instance: theory -> class * tyco -> string
    1.12 @@ -32,53 +34,60 @@
    1.13  
    1.14  type tyco = string;
    1.15  type const = string;
    1.16 -val inst_ord = prod_ord fast_string_ord fast_string_ord;
    1.17 -val eq_inst = is_equal o inst_ord;
    1.18 +val string_pair_ord = prod_ord fast_string_ord fast_string_ord;
    1.19 +val eq_string_pair = is_equal o string_pair_ord;
    1.20  structure Consttab = CodegenConsts.Consttab;
    1.21  
    1.22 -structure Insttab =
    1.23 +structure StringPairTab =
    1.24    TableFun(
    1.25 -    type key = class * tyco;
    1.26 -    val ord = inst_ord;
    1.27 +    type key = string * string;
    1.28 +    val ord = string_pair_ord;
    1.29    );
    1.30  
    1.31  datatype names = Names of {
    1.32    class: class Symtab.table * class Symtab.table,
    1.33 +  classrel: string StringPairTab.table * (class * class) Symtab.table,
    1.34    tyco: tyco Symtab.table * tyco Symtab.table,
    1.35 -  instance: string Insttab.table * (class * tyco) Symtab.table,
    1.36 +  instance: string StringPairTab.table * (class * tyco) Symtab.table,
    1.37    const: const Consttab.table * (string * typ list) Symtab.table
    1.38  }
    1.39  
    1.40  val empty_names = Names {
    1.41    class = (Symtab.empty, Symtab.empty),
    1.42 +  classrel = (StringPairTab.empty, Symtab.empty),
    1.43    tyco = (Symtab.empty, Symtab.empty),
    1.44 -  instance = (Insttab.empty, Symtab.empty),
    1.45 +  instance = (StringPairTab.empty, Symtab.empty),
    1.46    const = (Consttab.empty, Symtab.empty)
    1.47  };
    1.48  
    1.49  local
    1.50 -  fun mk_names (class, tyco, instance, const) =
    1.51 -    Names { class = class, tyco = tyco, instance = instance, const = const};
    1.52 -  fun map_names f (Names { class, tyco, instance, const }) =
    1.53 -    mk_names (f (class, tyco, instance, const));
    1.54 +  fun mk_names (class, classrel, tyco, instance, const) =
    1.55 +    Names { class = class, classrel = classrel, tyco = tyco, instance = instance, const = const};
    1.56 +  fun map_names f (Names { class, classrel, tyco, instance, const }) =
    1.57 +    mk_names (f (class, classrel, tyco, instance, const));
    1.58    val eq_string = op = : string * string -> bool;
    1.59  in
    1.60 -  fun merge_names (Names { class = (class1, classrev1), tyco = (tyco1, tycorev1),
    1.61 +  fun merge_names (Names { class = (class1, classrev1),
    1.62 +      classrel = (classrel1, classrelrev1), tyco = (tyco1, tycorev1),
    1.63        instance = (instance1, instancerev1), const = (const1, constrev1) },
    1.64 -    Names { class = (class2, classrev2), tyco = (tyco2, tycorev2),
    1.65 +    Names { class = (class2, classrev2),
    1.66 +      classrel = (classrel2, classrelrev2), tyco = (tyco2, tycorev2),
    1.67        instance = (instance2, instancerev2), const = (const2, constrev2) }) =
    1.68      mk_names ((Symtab.merge eq_string (class1, class2), Symtab.merge eq_string (classrev1, classrev2)),
    1.69 +      (StringPairTab.merge eq_string (classrel1, classrel2), Symtab.merge eq_string_pair (classrelrev1, classrelrev2)),
    1.70        (Symtab.merge eq_string (tyco1, tyco2), Symtab.merge eq_string (tycorev1, tycorev2)),
    1.71 -      (Insttab.merge eq_string (instance1, instance2), Symtab.merge eq_inst (instancerev1, instancerev2)),
    1.72 +      (StringPairTab.merge eq_string (instance1, instance2), Symtab.merge eq_string_pair (instancerev1, instancerev2)),
    1.73        (Consttab.merge eq_string (const1, const2), Symtab.merge CodegenConsts.eq_const (constrev1, constrev2)));
    1.74    fun map_class f = map_names
    1.75 -    (fn (class, tyco, inst, const) => (f class, tyco, inst, const));
    1.76 +    (fn (class, classrel, tyco, inst, const) => (f class, classrel, tyco, inst, const));
    1.77 +  fun map_classrel f = map_names
    1.78 +    (fn (class, classrel, tyco, inst, const) => (class, f classrel, tyco, inst, const));
    1.79    fun map_tyco f = map_names
    1.80 -    (fn (class, tyco, inst, const) => (class, f tyco, inst, const));
    1.81 +    (fn (class, classrel, tyco, inst, const) => (class, classrel, f tyco, inst, const));
    1.82    fun map_inst f = map_names
    1.83 -    (fn (class, tyco, inst, const) => (class, tyco, f inst, const));
    1.84 +    (fn (class, classrel, tyco, inst, const) => (class, classrel, tyco, f inst, const));
    1.85    fun map_const f = map_names
    1.86 -    (fn (class, tyco, inst, const) => (class, tyco, inst, f const));
    1.87 +    (fn (class, classrel, tyco, inst, const) => (class, classrel, tyco, inst, f const));
    1.88  
    1.89  end; (*local*)
    1.90  
    1.91 @@ -142,17 +151,16 @@
    1.92        else NONE;
    1.93    in case thy_of thy
    1.94     of SOME thy => Context.theory_name thy
    1.95 -        |> explode
    1.96 -        (*should disappear as soon as hierarchical theory name spaces are available*)
    1.97 -        |> Symbol.scanner "Malformed name"
    1.98 -             (Scan.repeat ($$ "_" |-- $$ "_" >> (fn _ => ".") || Scan.one Symbol.not_eof))
    1.99 -        |> implode
   1.100      | NONE => error (errmsg x) end;
   1.101  
   1.102  fun thyname_of_class thy =
   1.103    thyname_of thy (fn thy => member (op =) (Sign.classes thy))
   1.104      (fn class => "thyname_of_class: no such class: " ^ quote class);
   1.105  
   1.106 +fun thyname_of_classrel thy =
   1.107 +  thyname_of thy (fn thy => fn (class1, class2) => Sign.subsort thy ([class1], [class2]))
   1.108 +    (fn (class1, class2) => "thyname_of_classrel: no such classrel: " ^ quote class1 ^ " in " ^ quote class2);
   1.109 +
   1.110  fun thyname_of_tyco thy =
   1.111    thyname_of thy Sign.declared_tyname
   1.112      (fn tyco => "thyname_of_tyco: no such type constructor: " ^ quote tyco);
   1.113 @@ -230,16 +238,25 @@
   1.114  val purify_prefix = map (purify_idf #> purify_upper);
   1.115  val purify_base = purify_idf #> purify_lower;
   1.116  
   1.117 +val dotify =
   1.118 +  explode
   1.119 +  (*should disappear as soon as hierarchical theory name spaces are available*)
   1.120 +  #> Symbol.scanner "Malformed name"
   1.121 +      (Scan.repeat ($$ "_" |-- $$ "_" >> (fn _ => ".") || Scan.one Symbol.not_eof))
   1.122 +  #> implode;
   1.123 +
   1.124  
   1.125  (* naming policies *)
   1.126  
   1.127  fun policy thy get_basename get_thyname name =
   1.128    let
   1.129 -    val prefix = (purify_prefix o NameSpace.explode o get_thyname thy) name;
   1.130 +    val prefix = (purify_prefix o NameSpace.explode o dotify o get_thyname thy) name;
   1.131      val base = (purify_base o get_basename) name;
   1.132    in NameSpace.implode (prefix @ [base]) end;
   1.133  
   1.134  fun class_policy thy = policy thy NameSpace.base thyname_of_class;
   1.135 +fun classrel_policy thy = policy thy (fn (class1, class2) => 
   1.136 +  NameSpace.base class2 ^ "_" ^ NameSpace.base class1) thyname_of_classrel;
   1.137  fun tyco_policy thy = policy thy NameSpace.base thyname_of_tyco;
   1.138  fun instance_policy thy = policy thy (fn (class, tyco) => 
   1.139    NameSpace.base class ^ "_" ^ NameSpace.base tyco) thyname_of_instance;
   1.140 @@ -259,7 +276,7 @@
   1.141    case force_thyname thy (c, tys)
   1.142     of NONE => policy thy NameSpace.base thyname_of_const c
   1.143      | SOME thyname => let
   1.144 -        val prefix = (purify_prefix o NameSpace.explode) thyname;
   1.145 +        val prefix = (purify_prefix o NameSpace.explode o dotify) thyname;
   1.146          val tycos = map_filter (fn Type (tyco, _) => SOME tyco | _ => NONE) tys;
   1.147          val base = map (purify_base o NameSpace.base) (c :: tycos);
   1.148        in NameSpace.implode (prefix @ [space_implode "_" base]) end;
   1.149 @@ -268,6 +285,7 @@
   1.150  (* shallow name spaces *)
   1.151  
   1.152  val nsp_class = "class";
   1.153 +val nsp_classrel = "clsrel"
   1.154  val nsp_tyco = "tyco";
   1.155  val nsp_inst = "inst";
   1.156  val nsp_const = "const";
   1.157 @@ -286,11 +304,14 @@
   1.158  fun class thy =
   1.159    get thy #class Symtab.lookup map_class Symtab.update class_policy
   1.160    #> add_nsp nsp_class;
   1.161 +fun classrel thy =
   1.162 +  get thy #classrel StringPairTab.lookup map_classrel StringPairTab.update classrel_policy
   1.163 +  #> add_nsp nsp_classrel;
   1.164  fun tyco thy =
   1.165    get thy #tyco Symtab.lookup map_tyco Symtab.update tyco_policy
   1.166    #> add_nsp nsp_tyco;
   1.167  fun instance thy =
   1.168 -  get thy #instance Insttab.lookup map_inst Insttab.update instance_policy
   1.169 +  get thy #instance StringPairTab.lookup map_inst StringPairTab.update instance_policy
   1.170    #> add_nsp nsp_inst;
   1.171  fun const thy =
   1.172    CodegenConsts.norm thy
   1.173 @@ -300,6 +321,9 @@
   1.174  fun class_rev thy =
   1.175    dest_nsp nsp_class
   1.176    #> Option.map (rev thy #class "class");
   1.177 +fun classrel_rev thy =
   1.178 +  dest_nsp nsp_classrel
   1.179 +  #> Option.map (rev thy #classrel "class relation");
   1.180  fun tyco_rev thy =
   1.181    dest_nsp nsp_tyco
   1.182    #> Option.map (rev thy #tyco "type constructor");