1.1 --- a/etc/isar-keywords-HOL-Nominal.el	Sun Sep 24 08:22:21 2006 +0200
     1.2 +++ b/etc/isar-keywords-HOL-Nominal.el	Mon Sep 25 17:04:12 2006 +0200
     1.3 @@ -48,6 +48,7 @@
     1.4      "code_constname"
     1.5      "code_gen"
     1.6      "code_instance"
     1.7 +    "code_instname"
     1.8      "code_library"
     1.9      "code_module"
    1.10      "code_simtype"
    1.11 @@ -375,6 +376,7 @@
    1.12      "code_const"
    1.13      "code_constname"
    1.14      "code_instance"
    1.15 +    "code_instname"
    1.16      "code_library"
    1.17      "code_module"
    1.18      "code_type"

     2.1 --- a/etc/isar-keywords-ZF.el	Sun Sep 24 08:22:21 2006 +0200
     2.2 +++ b/etc/isar-keywords-ZF.el	Mon Sep 25 17:04:12 2006 +0200
     2.3 @@ -46,6 +46,7 @@
     2.4      "code_constname"
     2.5      "code_gen"
     2.6      "code_instance"
     2.7 +    "code_instname"
     2.8      "code_library"
     2.9      "code_module"
    2.10      "code_simtype"
    2.11 @@ -360,6 +361,7 @@
    2.12      "code_const"
    2.13      "code_constname"
    2.14      "code_instance"
    2.15 +    "code_instname"
    2.16      "code_library"
    2.17      "code_module"
    2.18      "code_type"

     3.1 --- a/etc/isar-keywords.el	Sun Sep 24 08:22:21 2006 +0200
     3.2 +++ b/etc/isar-keywords.el	Mon Sep 25 17:04:12 2006 +0200
     3.3 @@ -48,6 +48,7 @@
     3.4      "code_constname"
     3.5      "code_gen"
     3.6      "code_instance"
     3.7 +    "code_instname"
     3.8      "code_library"
     3.9      "code_module"
    3.10      "code_simtype"
    3.11 @@ -396,6 +397,7 @@
    3.12      "code_const"
    3.13      "code_constname"
    3.14      "code_instance"
    3.15 +    "code_instname"
    3.16      "code_library"
    3.17      "code_module"
    3.18      "code_type"

     4.1 --- a/src/Pure/Tools/codegen_names.ML	Sun Sep 24 08:22:21 2006 +0200
     4.2 +++ b/src/Pure/Tools/codegen_names.ML	Mon Sep 25 17:04:12 2006 +0200
     4.3 @@ -11,16 +11,26 @@
     4.4    type tyco = string
     4.5    type const = string
     4.6    val class: theory -> class -> class
     4.7 -  val class_rev: theory -> class -> class
     4.8 +  val class_rev: theory -> class -> class option
     4.9    val tyco: theory -> tyco -> tyco
    4.10 -  val tyco_rev: theory -> tyco -> tyco
    4.11 +  val tyco_rev: theory -> tyco -> tyco option
    4.12    val tyco_force: tyco * string -> theory -> theory
    4.13    val instance: theory -> class * tyco -> string
    4.14 -  val instance_rev: theory -> string -> class * tyco
    4.15 +  val instance_rev: theory -> string -> (class * tyco) option
    4.16 +  val instance_force: (class * tyco) * string -> theory -> theory
    4.17    val const: theory -> CodegenConsts.const -> const
    4.18 -  val const_rev: theory -> const -> CodegenConsts.const
    4.19 +  val const_rev: theory -> const -> CodegenConsts.const option
    4.20    val const_force: CodegenConsts.const * const -> theory -> theory
    4.21    val purify_var: string -> string
    4.22 +  val has_nsp: string -> string -> bool
    4.23 +  val nsp_module: string
    4.24 +  val nsp_class: string
    4.25 +  val nsp_tyco: string
    4.26 +  val nsp_inst: string
    4.27 +  val nsp_fun: string
    4.28 +  val nsp_classop: string
    4.29 +  val nsp_dtco: string
    4.30 +  val nsp_eval: string
    4.31  end;
    4.32  
    4.33  structure CodegenNames: CODEGEN_NAMES =
    4.34 @@ -278,6 +288,32 @@
    4.35      thy
    4.36    end;
    4.37  
    4.38 +fun instance_force (instance, name) thy =
    4.39 +  let
    4.40 +    val names = NameSpace.unpack name;
    4.41 +    val (prefix, base) = split_last (NameSpace.unpack name);
    4.42 +    val prefix' = purify_prefix prefix;
    4.43 +    val base' = purify_base base;
    4.44 +    val _ = if (base' = base) andalso forall (op =) (prefix' ~~ prefix)
    4.45 +      then ()
    4.46 +      else
    4.47 +        error ("Name violates naming conventions: " ^ quote name
    4.48 +          ^ "; perhaps try with " ^ quote (NameSpace.pack (prefix' @ [base'])))
    4.49 +    val names_ref = CodeName.get thy;
    4.50 +    val (Names names) = ! names_ref;
    4.51 +    val (inst, instrev) = #instance names;
    4.52 +    val _ = if Insttab.defined inst instance
    4.53 +      then error ("Instance already named: " ^ quote (fst instance) ^ ", " ^ quote (snd instance))
    4.54 +      else ();
    4.55 +    val _ = if Symtab.defined instrev name
    4.56 +      then error ("Name already given to instance: " ^ quote name)
    4.57 +      else ();
    4.58 +    val _ = names_ref := map_inst (K (Insttab.update_new (instance, name) inst,
    4.59 +          Symtab.update_new (name, instance) instrev)) (Names names);
    4.60 +  in
    4.61 +    thy
    4.62 +  end;
    4.63 +
    4.64  
    4.65  (* naming policies *)
    4.66  
    4.67 @@ -311,22 +347,80 @@
    4.68        in NameSpace.pack (prefix @ [space_implode "_" base]) end;
    4.69  
    4.70  
    4.71 +(* shallow name spaces *)
    4.72 +
    4.73 +val nsp_module = ""; (*a dummy by convention*)
    4.74 +val nsp_class = "class";
    4.75 +val nsp_tyco = "tyco";
    4.76 +val nsp_inst = "inst";
    4.77 +val nsp_fun = "fun";
    4.78 +val nsp_classop = "classop";
    4.79 +val nsp_dtco = "dtco";
    4.80 +val nsp_eval = "EVAL"; (*only for evaluation*)
    4.81 +
    4.82 +fun add_nsp shallow name =
    4.83 +  name
    4.84 +  |> NameSpace.unpack
    4.85 +  |> split_last
    4.86 +  |> apsnd (single #> cons shallow)
    4.87 +  |> (op @)
    4.88 +  |> NameSpace.pack;
    4.89 +
    4.90 +fun dest_nsp nsp nspname =
    4.91 +  let
    4.92 +    val xs = NameSpace.unpack nspname;
    4.93 +    val (ys, base) = split_last xs;
    4.94 +    val (module, shallow) = split_last ys;
    4.95 +  in
    4.96 +    if nsp = shallow
    4.97 +   then (SOME o NameSpace.pack) (module @ [base])
    4.98 +    else NONE
    4.99 +  end;
   4.100 +
   4.101 +val has_nsp = is_some oo dest_nsp;
   4.102 +
   4.103 +fun if_nsp nsp f idf =
   4.104 +  Option.map f (dest_nsp nsp idf);
   4.105 +
   4.106 +
   4.107  (* external interfaces *)
   4.108  
   4.109  fun class thy =
   4.110 -  get thy #class Symtab.lookup map_class Symtab.update class_policy;
   4.111 +  get thy #class Symtab.lookup map_class Symtab.update class_policy
   4.112 +  #> add_nsp nsp_class;
   4.113  fun tyco thy =
   4.114 -  get thy #tyco Symtab.lookup map_tyco Symtab.update tyco_policy;
   4.115 +  get thy #tyco Symtab.lookup map_tyco Symtab.update tyco_policy
   4.116 +  #> add_nsp nsp_tyco;
   4.117  fun instance thy =
   4.118 -  get thy #instance Insttab.lookup map_inst Insttab.update instance_policy;
   4.119 -fun const thy =
   4.120 -  get thy #const Consttab.lookup map_const Consttab.update const_policy
   4.121 -    o CodegenConsts.norm thy;
   4.122 +  get thy #instance Insttab.lookup map_inst Insttab.update instance_policy
   4.123 +  #> add_nsp nsp_inst;
   4.124 +fun const thy c_ty = case CodegenConsts.norm thy c_ty
   4.125 + of (c_tys as (c, tys)) => add_nsp (if (is_some o CodegenData.get_datatype_of_constr thy) c_tys
   4.126 +     then nsp_dtco
   4.127 +   else if (is_some o AxClass.class_of_param thy) c andalso
   4.128 +    case tys of [TFree _] => true | [TVar _] => true | _ => false
   4.129 +     then nsp_classop
   4.130 +   else nsp_fun)
   4.131 +  (get thy #const Consttab.lookup map_const Consttab.update const_policy c_tys);
   4.132  
   4.133 -fun class_rev thy = rev thy #class "class";
   4.134 -fun tyco_rev thy = rev thy #tyco "type constructor";
   4.135 -fun instance_rev thy = rev thy #instance "instance";
   4.136 -fun const_rev thy = rev thy #const "constant";
   4.137 +fun class_rev thy =
   4.138 +  dest_nsp nsp_class
   4.139 +  #> Option.map (rev thy #class "class");
   4.140 +fun tyco_rev thy =
   4.141 +  dest_nsp nsp_tyco
   4.142 +  #> Option.map (rev thy #tyco "type constructor");
   4.143 +fun instance_rev thy =
   4.144 +  dest_nsp nsp_inst
   4.145 +  #> Option.map (rev thy #instance "instance");
   4.146 +fun const_rev thy nspname =
   4.147 +  (case dest_nsp nsp_fun nspname
   4.148 +   of name as SOME _ => name
   4.149 +    | _ => (case dest_nsp nsp_dtco nspname
   4.150 +   of name as SOME _ => name
   4.151 +    | _ => (case dest_nsp nsp_classop nspname
   4.152 +   of name as SOME _ => name
   4.153 +    | _ => NONE)))
   4.154 +  |> Option.map (rev thy #const "constant");
   4.155  
   4.156  
   4.157  (* outer syntax *)
   4.158 @@ -342,7 +436,10 @@
   4.159  fun tyco_force_e (raw_tyco, name) thy =
   4.160    tyco_force (Sign.intern_type thy raw_tyco, name) thy;
   4.161  
   4.162 -val (constnameK, typenameK) = ("code_constname", "code_typename");
   4.163 +fun instance_force_e ((raw_tyco, raw_class), name) thy =
   4.164 +  instance_force ((Sign.intern_class thy raw_class, Sign.intern_type thy raw_tyco), name) thy;
   4.165 +
   4.166 +val (constnameK, typenameK, instnameK) = ("code_constname", "code_typename", "code_instname");
   4.167  
   4.168  val constnameP =
   4.169    OuterSyntax.command constnameK "declare code name for constant" K.thy_decl (
   4.170 @@ -353,14 +450,21 @@
   4.171  
   4.172  val typenameP =
   4.173    OuterSyntax.command typenameK "declare code name for type constructor" K.thy_decl (
   4.174 -    Scan.repeat1 (P.name -- P.name)
   4.175 +    Scan.repeat1 (P.xname -- P.name)
   4.176      >> (fn aliasses =>
   4.177            Toplevel.theory (fold tyco_force_e aliasses))
   4.178    );
   4.179  
   4.180 +val instnameP =
   4.181 +  OuterSyntax.command instnameK "declare code name for instance relation" K.thy_decl (
   4.182 +    Scan.repeat1 ((P.xname --| P.$$$ "::" -- P.xname) -- P.name)
   4.183 +    >> (fn aliasses =>
   4.184 +          Toplevel.theory (fold instance_force_e aliasses))
   4.185 +  );
   4.186 +
   4.187  in
   4.188  
   4.189 -val _ = OuterSyntax.add_parsers [constnameP, typenameP];
   4.190 +val _ = OuterSyntax.add_parsers [constnameP, typenameP, instnameP];
   4.191  
   4.192  
   4.193  end; (*local*)