src/Pure/sign.ML
changeset 30343 79f022df8527
parent 30280 eb98b49ef835
child 30364 577edc39b501
     1.1 --- a/src/Pure/sign.ML	Sat Mar 07 22:04:59 2009 +0100
     1.2 +++ b/src/Pure/sign.ML	Sat Mar 07 22:12:07 2009 +0100
     1.3 @@ -14,6 +14,7 @@
     1.4      consts: Consts.T}
     1.5    val naming_of: theory -> NameSpace.naming
     1.6    val full_name: theory -> binding -> string
     1.7 +  val full_name_path: theory -> string -> binding -> string
     1.8    val full_bname: theory -> bstring -> string
     1.9    val full_bname_path: theory -> string -> bstring -> string
    1.10    val syn_of: theory -> Syntax.syntax
    1.11 @@ -78,24 +79,24 @@
    1.12    val cert_arity: theory -> arity -> arity
    1.13    val add_defsort: string -> theory -> theory
    1.14    val add_defsort_i: sort -> theory -> theory
    1.15 -  val add_types: (bstring * int * mixfix) list -> theory -> theory
    1.16 -  val add_nonterminals: bstring list -> theory -> theory
    1.17 -  val add_tyabbrs: (bstring * string list * string * mixfix) list -> theory -> theory
    1.18 -  val add_tyabbrs_i: (bstring * string list * typ * mixfix) list -> theory -> theory
    1.19 -  val add_syntax: (bstring * string * mixfix) list -> theory -> theory
    1.20 -  val add_syntax_i: (bstring * typ * mixfix) list -> theory -> theory
    1.21 -  val add_modesyntax: Syntax.mode -> (bstring * string * mixfix) list -> theory -> theory
    1.22 -  val add_modesyntax_i: Syntax.mode -> (bstring * typ * mixfix) list -> theory -> theory
    1.23 -  val del_modesyntax: Syntax.mode -> (bstring * string * mixfix) list -> theory -> theory
    1.24 -  val del_modesyntax_i: Syntax.mode -> (bstring * typ * mixfix) list -> theory -> theory
    1.25 +  val add_types: (binding * int * mixfix) list -> theory -> theory
    1.26 +  val add_nonterminals: binding list -> theory -> theory
    1.27 +  val add_tyabbrs: (binding * string list * string * mixfix) list -> theory -> theory
    1.28 +  val add_tyabbrs_i: (binding * string list * typ * mixfix) list -> theory -> theory
    1.29 +  val add_syntax: (string * string * mixfix) list -> theory -> theory
    1.30 +  val add_syntax_i: (string * typ * mixfix) list -> theory -> theory
    1.31 +  val add_modesyntax: Syntax.mode -> (string * string * mixfix) list -> theory -> theory
    1.32 +  val add_modesyntax_i: Syntax.mode -> (string * typ * mixfix) list -> theory -> theory
    1.33 +  val del_modesyntax: Syntax.mode -> (string * string * mixfix) list -> theory -> theory
    1.34 +  val del_modesyntax_i: Syntax.mode -> (string * typ * mixfix) list -> theory -> theory
    1.35    val notation: bool -> Syntax.mode -> (term * mixfix) list -> theory -> theory
    1.36    val declare_const: Properties.T -> (binding * typ) * mixfix -> theory -> term * theory
    1.37 -  val add_consts: (bstring * string * mixfix) list -> theory -> theory
    1.38 -  val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory
    1.39 +  val add_consts: (binding * string * mixfix) list -> theory -> theory
    1.40 +  val add_consts_i: (binding * typ * mixfix) list -> theory -> theory
    1.41    val add_abbrev: string -> Properties.T -> binding * term -> theory -> (term * term) * theory
    1.42    val revert_abbrev: string -> string -> theory -> theory
    1.43    val add_const_constraint: string * typ option -> theory -> theory
    1.44 -  val primitive_class: string * class list -> theory -> theory
    1.45 +  val primitive_class: binding * class list -> theory -> theory
    1.46    val primitive_classrel: class * class -> theory -> theory
    1.47    val primitive_arity: arity -> theory -> theory
    1.48    val add_trfuns:
    1.49 @@ -186,9 +187,10 @@
    1.50  val naming_of = #naming o rep_sg;
    1.51  
    1.52  val full_name = NameSpace.full_name o naming_of;
    1.53 +fun full_name_path thy path = NameSpace.full_name (NameSpace.add_path path (naming_of thy));
    1.54 +
    1.55  fun full_bname thy = NameSpace.full_name (naming_of thy) o Binding.name;
    1.56 -fun full_bname_path thy elems =
    1.57 -  NameSpace.full_name (NameSpace.add_path elems (naming_of thy)) o Binding.name;
    1.58 +fun full_bname_path thy path = full_name_path thy path o Binding.name;
    1.59  
    1.60  
    1.61  (* syntax *)
    1.62 @@ -435,8 +437,8 @@
    1.63  
    1.64  fun add_types types thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
    1.65    let
    1.66 -    val syn' = Syntax.update_type_gram types syn;
    1.67 -    val decls = map (fn (a, n, mx) => (Syntax.type_name a mx, n)) types;
    1.68 +    val syn' = Syntax.update_type_gram (map (fn (a, n, mx) => (Binding.name_of a, n, mx)) types) syn;
    1.69 +    val decls = map (fn (a, n, mx) => (Binding.map_name (Syntax.type_name mx) a, n)) types;
    1.70      val tags = [(Markup.theory_nameN, Context.theory_name thy)];
    1.71      val tsig' = fold (Type.add_type naming tags) decls tsig;
    1.72    in (naming, syn', tsig', consts) end);
    1.73 @@ -446,7 +448,7 @@
    1.74  
    1.75  fun add_nonterminals ns thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
    1.76    let
    1.77 -    val syn' = Syntax.update_consts ns syn;
    1.78 +    val syn' = Syntax.update_consts (map Binding.name_of ns) syn;
    1.79      val tsig' = fold (Type.add_nonterminal naming []) ns tsig;
    1.80    in (naming, syn', tsig', consts) end);
    1.81  
    1.82 @@ -457,10 +459,10 @@
    1.83    thy |> map_sign (fn (naming, syn, tsig, consts) =>
    1.84      let
    1.85        val ctxt = ProofContext.init thy;
    1.86 -      val syn' = Syntax.update_type_gram [(a, length vs, mx)] syn;
    1.87 -      val a' = Syntax.type_name a mx;
    1.88 -      val abbr = (a', vs, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt rhs))
    1.89 -        handle ERROR msg => cat_error msg ("in type abbreviation " ^ quote a');
    1.90 +      val syn' = Syntax.update_type_gram [(Binding.name_of a, length vs, mx)] syn;
    1.91 +      val b = Binding.map_name (Syntax.type_name mx) a;
    1.92 +      val abbr = (b, vs, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt rhs))
    1.93 +        handle ERROR msg => cat_error msg ("in type abbreviation " ^ quote (Binding.str_of b));
    1.94        val tsig' = Type.add_abbrev naming [] abbr tsig;
    1.95      in (naming, syn', tsig', consts) end);
    1.96  
    1.97 @@ -475,7 +477,7 @@
    1.98      val ctxt = ProofContext.init thy;
    1.99      fun prep (c, T, mx) = (c, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt T), mx)
   1.100        handle ERROR msg =>
   1.101 -        cat_error msg ("in syntax declaration " ^ quote (Syntax.const_name c mx));
   1.102 +        cat_error msg ("in syntax declaration " ^ quote (Syntax.const_name mx c));
   1.103    in thy |> map_syn (change_gram (is_logtype thy) mode (map prep args)) end;
   1.104  
   1.105  fun gen_add_syntax x = gen_syntax Syntax.update_const_gram x;
   1.106 @@ -522,12 +524,10 @@
   1.107      |> pair (map #3 args)
   1.108    end;
   1.109  
   1.110 -fun bindify (name, T, mx) = (Binding.name name, T, mx);
   1.111 -
   1.112  in
   1.113  
   1.114 -fun add_consts args = snd o gen_add_consts Syntax.parse_typ false [] (map bindify args);
   1.115 -fun add_consts_i args = snd o gen_add_consts (K I) false [] (map bindify args);
   1.116 +fun add_consts args = snd o gen_add_consts Syntax.parse_typ false [] args;
   1.117 +fun add_consts_i args = snd o gen_add_consts (K I) false [] args;
   1.118  
   1.119  fun declare_const tags ((b, T), mx) thy =
   1.120    let
   1.121 @@ -571,10 +571,10 @@
   1.122  fun primitive_class (bclass, classes) thy =
   1.123    thy |> map_sign (fn (naming, syn, tsig, consts) =>
   1.124      let
   1.125 -      val syn' = Syntax.update_consts [bclass] syn;
   1.126 +      val syn' = Syntax.update_consts [Binding.name_of bclass] syn;
   1.127        val tsig' = Type.add_class (Syntax.pp_global thy) naming (bclass, classes) tsig;
   1.128      in (naming, syn', tsig', consts) end)
   1.129 -  |> add_consts_i [(Logic.const_of_class bclass, Term.a_itselfT --> propT, NoSyn)];
   1.130 +  |> add_consts_i [(Binding.map_name Logic.const_of_class bclass, Term.a_itselfT --> propT, NoSyn)];
   1.131  
   1.132  fun primitive_classrel arg thy = thy |> map_tsig (Type.add_classrel (Syntax.pp_global thy) arg);
   1.133  fun primitive_arity arg thy = thy |> map_tsig (Type.add_arity (Syntax.pp_global thy) arg);