maintain theory name via name space, not tags;
authorwenzelm
Sun Oct 25 20:54:21 2009 +0100 (2009-10-25 ago)
changeset 3317261ee96bc9895
parent 33171 292970b42770
child 33173 b8ca12f6681a
maintain theory name via name space, not tags;
AxClass.thynames_of_arity: explicit theory name, not tags;
src/Pure/General/markup.ML
src/Pure/axclass.ML
src/Pure/codegen.ML
src/Pure/sign.ML
src/Tools/Code/code_thingol.ML
     1.1 --- a/src/Pure/General/markup.ML	Sun Oct 25 19:21:34 2009 +0100
     1.2 +++ b/src/Pure/General/markup.ML	Sun Oct 25 20:54:21 2009 +0100
     1.3 @@ -13,7 +13,6 @@
     1.4    val nameN: string
     1.5    val name: string -> T -> T
     1.6    val bindingN: string val binding: string -> T
     1.7 -  val theory_nameN: string
     1.8    val kindN: string
     1.9    val internalK: string
    1.10    val entityN: string val entity: string -> T
    1.11 @@ -150,8 +149,6 @@
    1.12  
    1.13  val (bindingN, binding) = markup_string "binding" nameN;
    1.14  
    1.15 -val theory_nameN = "theory_name";
    1.16 -
    1.17  
    1.18  (* kind *)
    1.19  
     2.1 --- a/src/Pure/axclass.ML	Sun Oct 25 19:21:34 2009 +0100
     2.2 +++ b/src/Pure/axclass.ML	Sun Oct 25 20:54:21 2009 +0100
     2.3 @@ -36,7 +36,7 @@
     2.4    val lookup_inst_param: Consts.T -> ((string * string) * 'a) list -> string * typ -> 'a option
     2.5    val param_of_inst: theory -> string * string -> string
     2.6    val inst_of_param: theory -> string -> (string * string) option
     2.7 -  val arity_property: theory -> class * string -> string -> string list
     2.8 +  val thynames_of_arity: theory -> class * string -> string list
     2.9    type cache
    2.10    val of_sort: theory -> typ * sort -> cache -> thm list * cache  (*exception Sorts.CLASS_ERROR*)
    2.11    val cache: cache
    2.12 @@ -92,8 +92,8 @@
    2.13  val arity_prefix = "arity_";
    2.14  
    2.15  type instances =
    2.16 -  ((class * class) * thm) list *
    2.17 -  ((class * sort list) * thm) list Symtab.table;
    2.18 +  ((class * class) * thm) list *  (*classrel theorems*)
    2.19 +  ((class * sort list) * (thm * string)) list Symtab.table;  (*arity theorems with theory name*)
    2.20  
    2.21  fun merge_instances ((classrel1, arities1): instances, (classrel2, arities2)) =
    2.22   (merge (eq_fst op =) (classrel1, classrel2),
    2.23 @@ -175,35 +175,32 @@
    2.24  
    2.25  fun the_arity thy a (c, Ss) =
    2.26    (case AList.lookup (op =) (Symtab.lookup_list (#2 (get_instances thy)) a) (c, Ss) of
    2.27 -    SOME th => Thm.transfer thy th
    2.28 +    SOME (th, _) => Thm.transfer thy th
    2.29    | NONE => error ("Unproven type arity " ^
    2.30        Syntax.string_of_arity (ProofContext.init thy) (a, Ss, [c])));
    2.31  
    2.32 -fun arity_property thy (c, a) x =
    2.33 -  Symtab.lookup_list (snd (get_instances thy)) a
    2.34 -  |> map_filter (fn ((c', _), th) => if c = c'
    2.35 -      then AList.lookup (op =) (Thm.get_tags th) x else NONE)
    2.36 +fun thynames_of_arity thy (c, a) =
    2.37 +  Symtab.lookup_list (#2 (get_instances thy)) a
    2.38 +  |> map_filter (fn ((c', _), (_, name)) => if c = c' then SOME name else NONE)
    2.39    |> rev;
    2.40  
    2.41 -fun insert_arity_completions thy (t, ((c, Ss), th)) arities =
    2.42 +fun insert_arity_completions thy (t, ((c, Ss), (th, thy_name))) arities =
    2.43    let
    2.44      val algebra = Sign.classes_of thy;
    2.45 -    val super_class_completions = Sign.super_classes thy c
    2.46 +    val super_class_completions =
    2.47 +      Sign.super_classes thy c
    2.48        |> filter_out (fn c1 => exists (fn ((c2, Ss2), _) => c1 = c2
    2.49 -          andalso Sorts.sorts_le algebra (Ss2, Ss)) (Symtab.lookup_list arities t))
    2.50 -    val tags = Thm.get_tags th;
    2.51 +          andalso Sorts.sorts_le algebra (Ss2, Ss)) (Symtab.lookup_list arities t));
    2.52      val completions = map (fn c1 => (Sorts.weaken algebra
    2.53        (fn (th, c2) => fn c3 => th RS the_classrel thy (c2, c3)) (th, c) c1
    2.54 -        |> Thm.map_tags (K tags) |> Thm.close_derivation, c1)) super_class_completions;
    2.55 -    val arities' = fold (fn (th1, c1) => Symtab.cons_list (t, ((c1, Ss), th1)))
    2.56 +        |> Thm.close_derivation, c1)) super_class_completions;
    2.57 +    val arities' = fold (fn (th1, c1) => Symtab.cons_list (t, ((c1, Ss), (th1, thy_name))))
    2.58        completions arities;
    2.59 -  in (completions, arities') end;
    2.60 +  in (null completions, arities') end;
    2.61  
    2.62  fun put_arity ((t, Ss, c), th) thy =
    2.63    let
    2.64 -    val th' = (Thm.map_tags o AList.default (op =))
    2.65 -      (Markup.theory_nameN, Context.theory_name thy) th;
    2.66 -    val arity' = (t, ((c, Ss), th'));
    2.67 +    val arity' = (t, ((c, Ss), (th, Context.theory_name thy)));
    2.68    in
    2.69      thy
    2.70      |> map_instances (fn (classrel, arities) => (classrel,
    2.71 @@ -216,11 +213,10 @@
    2.72  fun complete_arities thy =
    2.73    let
    2.74      val arities = snd (get_instances thy);
    2.75 -    val (completions, arities') = arities
    2.76 -      |> fold_map (insert_arity_completions thy) (Symtab.dest_list arities)
    2.77 -      |>> flat;
    2.78 -  in if null completions
    2.79 -    then NONE
    2.80 +    val (finished, arities') = arities
    2.81 +      |> fold_map (insert_arity_completions thy) (Symtab.dest_list arities);
    2.82 +  in
    2.83 +    if forall I finished then NONE
    2.84      else SOME (thy |> map_instances (fn (classrel, _) => (classrel, arities')))
    2.85    end;
    2.86  
     3.1 --- a/src/Pure/codegen.ML	Sun Oct 25 19:21:34 2009 +0100
     3.2 +++ b/src/Pure/codegen.ML	Sun Oct 25 20:54:21 2009 +0100
     3.3 @@ -446,13 +446,8 @@
     3.4  fun map_node k f (gr, x) = (Graph.map_node k f gr, x);
     3.5  fun new_node p (gr, x) = (Graph.new_node p gr, x);
     3.6  
     3.7 -fun thyname_of thy f x = the (AList.lookup (op =) (f x) Markup.theory_nameN);
     3.8 -
     3.9 -fun thyname_of_type thy =
    3.10 -  thyname_of thy (Type.the_tags (Sign.tsig_of thy));
    3.11 -
    3.12 -fun thyname_of_const thy =
    3.13 -  thyname_of thy (Consts.the_tags (Sign.consts_of thy));
    3.14 +fun thyname_of_type thy = #theory_name o Name_Space.the_entry (Sign.type_space thy);
    3.15 +fun thyname_of_const thy = #theory_name o Name_Space.the_entry (Sign.const_space thy);
    3.16  
    3.17  fun rename_terms ts =
    3.18    let
     4.1 --- a/src/Pure/sign.ML	Sun Oct 25 19:21:34 2009 +0100
     4.2 +++ b/src/Pure/sign.ML	Sun Oct 25 20:54:21 2009 +0100
     4.3 @@ -434,8 +434,7 @@
     4.4    let
     4.5      val syn' = Syntax.update_type_gram (map (fn (a, n, mx) => (Name.of_binding a, n, mx)) types) syn;
     4.6      val decls = map (fn (a, n, mx) => (Binding.map_name (Syntax.type_name mx) a, n)) types;
     4.7 -    val tags = [(Markup.theory_nameN, Context.theory_name thy)];
     4.8 -    val tsig' = fold (Type.add_type naming tags) decls tsig;
     4.9 +    val tsig' = fold (Type.add_type naming []) decls tsig;
    4.10    in (naming, syn', tsig', consts) end);
    4.11  
    4.12  
    4.13 @@ -511,10 +510,9 @@
    4.14          val T' = Logic.varifyT T;
    4.15        in ((b, T'), (c_syn, T', mx), Const (c, T)) end;
    4.16      val args = map prep raw_args;
    4.17 -    val tags' = tags |> Properties.put (Markup.theory_nameN, Context.theory_name thy);
    4.18    in
    4.19      thy
    4.20 -    |> map_consts (fold (Consts.declare authentic (naming_of thy) tags' o #1) args)
    4.21 +    |> map_consts (fold (Consts.declare authentic (naming_of thy) tags o #1) args)
    4.22      |> add_syntax_i (map #2 args)
    4.23      |> pair (map #3 args)
    4.24    end;
     5.1 --- a/src/Tools/Code/code_thingol.ML	Sun Oct 25 19:21:34 2009 +0100
     5.2 +++ b/src/Tools/Code/code_thingol.ML	Sun Oct 25 20:54:21 2009 +0100
     5.3 @@ -252,19 +252,15 @@
     5.4  (* policies *)
     5.5  
     5.6  local
     5.7 -  fun thyname_of thy f x = the (AList.lookup (op =) (f x) Markup.theory_nameN);
     5.8 -  fun thyname_of_class thy =
     5.9 -    thyname_of thy (ProofContext.query_class (ProofContext.init thy));
    5.10 -  fun thyname_of_tyco thy =
    5.11 -    thyname_of thy (Type.the_tags (Sign.tsig_of thy));
    5.12 -  fun thyname_of_instance thy inst = case AxClass.arity_property thy inst Markup.theory_nameN
    5.13 -   of [] => error ("no such instance: " ^ quote (snd inst ^ " :: " ^ fst inst))
    5.14 +  fun thyname_of_class thy = #theory_name o Name_Space.the_entry (Sign.class_space thy);
    5.15 +  fun thyname_of_instance thy inst = case AxClass.thynames_of_arity thy inst
    5.16 +   of [] => error ("No such instance: " ^ quote (snd inst ^ " :: " ^ fst inst))
    5.17      | thyname :: _ => thyname;
    5.18    fun thyname_of_const thy c = case AxClass.class_of_param thy c
    5.19     of SOME class => thyname_of_class thy class
    5.20      | NONE => (case Code.get_datatype_of_constr thy c
    5.21 -       of SOME dtco => thyname_of_tyco thy dtco
    5.22 -        | NONE => thyname_of thy (Consts.the_tags (Sign.consts_of thy)) c);
    5.23 +       of SOME dtco => Codegen.thyname_of_type thy dtco
    5.24 +        | NONE => Codegen.thyname_of_const thy c);
    5.25    fun purify_base "op &" = "and"
    5.26      | purify_base "op |" = "or"
    5.27      | purify_base "op -->" = "implies"
    5.28 @@ -282,10 +278,11 @@
    5.29  
    5.30  fun namify_class thy = namify thy Long_Name.base_name thyname_of_class;
    5.31  fun namify_classrel thy = namify thy (fn (class1, class2) => 
    5.32 -  Long_Name.base_name class2 ^ "_" ^ Long_Name.base_name class1) (fn thy => thyname_of_class thy o fst);
    5.33 +    Long_Name.base_name class2 ^ "_" ^ Long_Name.base_name class1)
    5.34 +  (fn thy => thyname_of_class thy o fst);
    5.35    (*order fits nicely with composed projections*)
    5.36  fun namify_tyco thy "fun" = "Pure.fun"
    5.37 -  | namify_tyco thy tyco = namify thy Long_Name.base_name thyname_of_tyco tyco;
    5.38 +  | namify_tyco thy tyco = namify thy Long_Name.base_name Codegen.thyname_of_type tyco;
    5.39  fun namify_instance thy = namify thy (fn (class, tyco) => 
    5.40    Long_Name.base_name class ^ "_" ^ Long_Name.base_name tyco) thyname_of_instance;
    5.41  fun namify_const thy = namify thy Long_Name.base_name thyname_of_const;