# HG changeset patch
# User wenzelm
# Date 1267459656 -3600
# Node ID b8dead547d9e93d4ab652593e3f66cdae76069dd
# Parent  cafb74a131da7a78ddfd23d9377c91bd48d36c8b
more uniform treatment of syntax for types vs. consts;

diff -r cafb74a131da -r b8dead547d9e src/Pure/Isar/local_syntax.ML
--- a/src/Pure/Isar/local_syntax.ML	Mon Mar 01 09:47:44 2010 +0100
+++ b/src/Pure/Isar/local_syntax.ML	Mon Mar 01 17:07:36 2010 +0100
@@ -13,11 +13,12 @@
   val structs_of: T -> string list
   val init: theory -> T
   val rebuild: theory -> T -> T
-  val add_syntax: theory -> (bool * (string * typ * mixfix)) list -> T -> T
+  datatype kind = Type | Const | Fixed
+  val add_syntax: theory -> (kind * (string * typ * mixfix)) list -> T -> T
   val set_mode: Syntax.mode -> T -> T
   val restore_mode: T -> T -> T
   val update_modesyntax: theory -> bool -> Syntax.mode ->
-    (bool * (string * typ * mixfix)) list -> T -> T
+    (kind * (string * typ * mixfix)) list -> T -> T
   val extern_term: T -> term -> term
 end;
 
@@ -27,8 +28,8 @@
 (* datatype T *)
 
 type local_mixfix =
-  (string * bool) *                                    (*name, fixed?*)
-  ((bool * Syntax.mode) * (string * typ * mixfix));    (*add?, mode, declaration*)
+  (string * bool) *  (*name, fixed?*)
+  ((bool * bool * Syntax.mode) * (string * typ * mixfix));  (*type?, add?, mode, declaration*)
 
 datatype T = Syntax of
  {thy_syntax: Syntax.syntax,
@@ -57,15 +58,16 @@
 fun build_syntax thy mode mixfixes (idents as (structs, _)) =
   let
     val thy_syntax = Sign.syn_of thy;
-    val is_logtype = Sign.is_logtype thy;
-    fun const_gram ((true, m), decls) = Syntax.update_const_gram is_logtype m decls
-      | const_gram ((false, m), decls) = Syntax.remove_const_gram is_logtype m decls;
+    fun update_gram ((true, add, m), decls) = Syntax.update_type_gram add m decls
+      | update_gram ((false, add, m), decls) =
+          Syntax.update_const_gram add (Sign.is_logtype thy) m decls;
+
     val (atrs, trs, trs', atrs') = Syntax.struct_trfuns structs;
     val local_syntax = thy_syntax
       |> Syntax.update_trfuns
           (map Syntax.mk_trfun atrs, map Syntax.mk_trfun trs,
            map Syntax.mk_trfun trs', map Syntax.mk_trfun atrs')
-      |> fold const_gram (AList.coalesce (op =) (rev (map snd mixfixes)));
+      |> fold update_gram (AList.coalesce (op =) (rev (map snd mixfixes)));
   in make_syntax (thy_syntax, local_syntax, mode, mixfixes, idents) end;
 
 fun init thy = build_syntax thy Syntax.mode_default [] ([], []);
@@ -77,16 +79,18 @@
 
 (* mixfix declarations *)
 
+datatype kind = Type | Const | Fixed;
+
 local
 
-fun prep_mixfix _ (_, (_, _, Structure)) = NONE
-  | prep_mixfix mode (fixed, (x, T, mx)) =
-      let val c = if fixed then Syntax.fixedN ^ x else x
-      in SOME ((x, fixed), (mode, (c, T, mx))) end;
+fun prep_mixfix _ _ (_, (_, _, Structure)) = NONE
+  | prep_mixfix add mode (Type, decl as (x, _, _)) = SOME ((x, false), ((true, add, mode), decl))
+  | prep_mixfix add mode (Const, decl as (x, _, _)) = SOME ((x, false), ((false, add, mode), decl))
+  | prep_mixfix add mode (Fixed, (x, T, mx)) =
+      SOME ((x, true), ((false, add, mode), (Syntax.mark_fixed x, T, mx)));
 
-fun prep_struct (fixed, (c, _, Structure)) =
-      if fixed then SOME c
-      else error ("Bad mixfix declaration for constant: " ^ quote c)
+fun prep_struct (Fixed, (c, _, Structure)) = SOME c
+  | prep_struct (_, (c, _, Structure)) = error ("Bad mixfix declaration for " ^ quote c)
   | prep_struct _ = NONE;
 
 in
@@ -97,7 +101,7 @@
     [] => syntax
   | decls =>
       let
-        val new_mixfixes = map_filter (prep_mixfix (add, mode)) decls;
+        val new_mixfixes = map_filter (prep_mixfix add mode) decls;
         val new_structs = map_filter prep_struct decls;
         val mixfixes' = rev new_mixfixes @ mixfixes;
         val structs' =
@@ -130,7 +134,7 @@
     fun map_free (t as Free (x, T)) =
           let val i = find_index (fn s => s = x) structs + 1 in
             if i = 0 andalso member (op =) fixes x then
-              Const (Syntax.fixedN ^ x, T)
+              Term.Const (Syntax.mark_fixed x, T)
             else if i = 1 andalso not (! show_structs) then
               Syntax.const "_struct" $ Syntax.const "_indexdefault"
             else t
diff -r cafb74a131da -r b8dead547d9e src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Mon Mar 01 09:47:44 2010 +0100
+++ b/src/Pure/Isar/local_theory.ML	Mon Mar 01 17:07:36 2010 +0100
@@ -42,6 +42,7 @@
   val type_syntax: bool -> declaration -> local_theory -> local_theory
   val term_syntax: bool -> declaration -> local_theory -> local_theory
   val declaration: bool -> declaration -> local_theory -> local_theory
+  val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
   val init: serial option -> string -> operations -> Proof.context -> local_theory
   val restore: local_theory -> local_theory
@@ -198,6 +199,10 @@
 val notes = notes_kind "";
 fun note (a, ths) = notes [(a, [(ths, [])])] #>> the_single;
 
+fun type_notation add mode raw_args lthy =
+  let val args = map (apfst (Morphism.typ (target_morphism lthy))) raw_args
+  in type_syntax false (ProofContext.target_type_notation add mode args) lthy end;
+
 fun notation add mode raw_args lthy =
   let val args = map (apfst (Morphism.term (target_morphism lthy))) raw_args
   in term_syntax false (ProofContext.target_notation add mode args) lthy end;
diff -r cafb74a131da -r b8dead547d9e src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Mar 01 09:47:44 2010 +0100
+++ b/src/Pure/Isar/proof_context.ML	Mon Mar 01 17:07:36 2010 +0100
@@ -115,7 +115,10 @@
   val add_cases: bool -> (string * Rule_Cases.T option) list -> Proof.context -> Proof.context
   val apply_case: Rule_Cases.T -> Proof.context -> (string * term list) list * Proof.context
   val get_case: Proof.context -> string -> string option list -> Rule_Cases.T
+  val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> Proof.context -> Proof.context
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> Proof.context -> Proof.context
+  val target_type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> morphism ->
+    Context.generic -> Context.generic
   val target_notation: bool -> Syntax.mode -> (term * mixfix) list -> morphism ->
     Context.generic -> Context.generic
   val add_const_constraint: string * typ option -> Proof.context -> Proof.context
@@ -1029,18 +1032,34 @@
 
 local
 
-fun const_syntax _ (Free (x, T), mx) = SOME (true, (x, T, mx))
+fun type_syntax (Type (c, args), mx) =  (* FIXME authentic syntax *)
+      SOME (Local_Syntax.Type, (Long_Name.base_name c, Syntax.make_type (length args), mx))
+  | type_syntax _ = NONE;
+
+fun const_syntax _ (Free (x, T), mx) = SOME (Local_Syntax.Fixed, (x, T, mx))
   | const_syntax ctxt (Const (c, _), mx) =
       (case try (Consts.type_scheme (consts_of ctxt)) c of
-        SOME T => SOME (false, (Syntax.mark_const c, T, mx))
+        SOME T => SOME (Local_Syntax.Const, (Syntax.mark_const c, T, mx))
       | NONE => NONE)
   | const_syntax _ _ = NONE;
 
+fun gen_notation syntax add mode args ctxt =
+  ctxt |> map_syntax
+    (Local_Syntax.update_modesyntax (theory_of ctxt) add mode (map_filter (syntax ctxt) args));
+
 in
 
-fun notation add mode args ctxt =
-  ctxt |> map_syntax
-    (Local_Syntax.update_modesyntax (theory_of ctxt) add mode (map_filter (const_syntax ctxt) args));
+val type_notation = gen_notation (K type_syntax);
+val notation = gen_notation const_syntax;
+
+fun target_type_notation add  mode args phi =
+  let
+    val args' = args |> map_filter (fn (T, mx) =>
+      let
+        val T' = Morphism.typ phi T;
+        val similar = (case (T, T') of (Type (c, _), Type (c', _)) => c = c' | _ => false);
+      in if similar then SOME (T', mx) else NONE end);
+  in Context.mapping (Sign.type_notation add mode args') (type_notation add mode args') end;
 
 fun target_notation add mode args phi =
   let
@@ -1049,6 +1068,7 @@
       in if Term.aconv_untyped (t, t') then SOME (t', mx) else NONE end);
   in Context.mapping (Sign.notation add mode args') (notation add mode args') end;
 
+
 end;
 
 
@@ -1086,7 +1106,7 @@
   if mx <> NoSyn andalso mx <> Structure andalso
       (can Name.dest_internal x orelse can Name.dest_skolem x) then
     error ("Illegal mixfix syntax for internal/skolem constant " ^ quote x)
-  else (true, (x, T, mx));
+  else (Local_Syntax.Fixed, (x, T, mx));
 
 in
 
diff -r cafb74a131da -r b8dead547d9e src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Mon Mar 01 09:47:44 2010 +0100
+++ b/src/Pure/Syntax/mixfix.ML	Mon Mar 01 17:07:36 2010 +0100
@@ -25,12 +25,13 @@
   val pretty_mixfix: mixfix -> Pretty.T
   val mixfix_args: mixfix -> int
   val mixfixT: mixfix -> typ
+  val make_type: int -> typ
 end;
 
 signature MIXFIX =
 sig
   include MIXFIX1
-  val syn_ext_types: (string * int * mixfix) list -> SynExt.syn_ext
+  val syn_ext_types: (string * typ * mixfix) list -> SynExt.syn_ext
   val syn_ext_consts: (string -> bool) -> (string * typ * mixfix) list -> SynExt.syn_ext
 end;
 
@@ -96,21 +97,22 @@
 
 (* syn_ext_types *)
 
+fun make_type n = replicate n SynExt.typeT ---> SynExt.typeT;
+
 fun syn_ext_types type_decls =
   let
-    fun mk_type n = replicate n SynExt.typeT ---> SynExt.typeT;
-    fun mk_infix sy n t p1 p2 p3 = SynExt.Mfix ("(_ " ^ sy ^ "/ _)", mk_type n, t, [p1, p2], p3);
+    fun mk_infix sy ty t p1 p2 p3 = SynExt.Mfix ("(_ " ^ sy ^ "/ _)", ty, t, [p1, p2], p3);
 
     fun mfix_of (_, _, NoSyn) = NONE
-      | mfix_of (t, n, Mixfix (sy, ps, p)) = SOME (SynExt.Mfix (sy, mk_type n, t, ps, p))
-      | mfix_of (t, n, Delimfix sy) = SOME (SynExt.Mfix (sy, mk_type n, t, [], SynExt.max_pri))
-      | mfix_of (t, n, Infix (sy, p)) = SOME (mk_infix sy n t (p + 1) (p + 1) p)
-      | mfix_of (t, n, Infixl (sy, p)) = SOME (mk_infix sy n t p (p + 1) p)
-      | mfix_of (t, n, Infixr (sy, p)) = SOME (mk_infix sy n t (p + 1) p p)
+      | mfix_of (t, ty, Mixfix (sy, ps, p)) = SOME (SynExt.Mfix (sy, ty, t, ps, p))
+      | mfix_of (t, ty, Delimfix sy) = SOME (SynExt.Mfix (sy, ty, t, [], SynExt.max_pri))
+      | mfix_of (t, ty, Infix (sy, p)) = SOME (mk_infix sy ty t (p + 1) (p + 1) p)
+      | mfix_of (t, ty, Infixl (sy, p)) = SOME (mk_infix sy ty t p (p + 1) p)
+      | mfix_of (t, ty, Infixr (sy, p)) = SOME (mk_infix sy ty t (p + 1) p p)
       | mfix_of (t, _, _) = error ("Bad mixfix declaration for " ^ quote t);  (* FIXME printable t (!?) *)
 
-    fun check_args (t, n, _) (SOME (mfix as SynExt.Mfix (sy, _, _, _, _))) =
-          if SynExt.mfix_args sy = n then ()
+    fun check_args (_, ty, _) (SOME (mfix as SynExt.Mfix (sy, _, _, _, _))) =
+          if length (Term.binder_types ty) = SynExt.mfix_args sy then ()
           else SynExt.err_in_mfix "Bad number of type constructor arguments" mfix
       | check_args _ NONE = ();
 
diff -r cafb74a131da -r b8dead547d9e src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Mon Mar 01 09:47:44 2010 +0100
+++ b/src/Pure/Syntax/syntax.ML	Mon Mar 01 17:07:36 2010 +0100
@@ -59,7 +59,6 @@
     Proof.context -> syntax -> bool -> term -> Pretty.T
   val standard_unparse_typ: Proof.context -> syntax -> typ -> Pretty.T
   val standard_unparse_sort: Proof.context -> syntax -> sort -> Pretty.T
-  val update_type_gram: (string * int * mixfix) list -> syntax -> syntax
   val update_consts: string list -> syntax -> syntax
   val update_trfuns:
     (string * ((ast list -> ast) * stamp)) list *
@@ -73,9 +72,8 @@
     (string * ((Proof.context -> ast list -> ast) * stamp)) list -> syntax -> syntax
   val extend_tokentrfuns: (string * string * (Proof.context -> string -> Pretty.T)) list ->
     syntax -> syntax
-  val update_const_gram: (string -> bool) ->
-    mode -> (string * typ * mixfix) list -> syntax -> syntax
-  val remove_const_gram: (string -> bool) ->
+  val update_type_gram: bool -> mode -> (string * typ * mixfix) list -> syntax -> syntax
+  val update_const_gram: bool -> (string -> bool) ->
     mode -> (string * typ * mixfix) list -> syntax -> syntax
   val update_trrules: Proof.context -> (string -> bool) -> syntax ->
     (string * string) trrule list -> syntax -> syntax
@@ -669,17 +667,16 @@
 
 fun ext_syntax f decls = update_syntax mode_default (f decls);
 
-val update_type_gram       = ext_syntax Mixfix.syn_ext_types;
-val update_consts          = ext_syntax SynExt.syn_ext_const_names;
-val update_trfuns          = ext_syntax SynExt.syn_ext_trfuns;
+val update_consts = ext_syntax SynExt.syn_ext_const_names;
+val update_trfuns = ext_syntax SynExt.syn_ext_trfuns;
 val update_advanced_trfuns = ext_syntax SynExt.syn_ext_advanced_trfuns;
-val extend_tokentrfuns     = ext_syntax SynExt.syn_ext_tokentrfuns;
+val extend_tokentrfuns = ext_syntax SynExt.syn_ext_tokentrfuns;
 
-fun update_const_gram is_logtype prmode decls =
-  update_syntax prmode (Mixfix.syn_ext_consts is_logtype decls);
+fun update_type_gram add prmode decls =
+  (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_types decls);
 
-fun remove_const_gram is_logtype prmode decls =
-  remove_syntax prmode (Mixfix.syn_ext_consts is_logtype decls);
+fun update_const_gram add is_logtype prmode decls =
+  (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_consts is_logtype decls);
 
 fun update_trrules ctxt is_logtype syn =
   ext_syntax SynExt.syn_ext_rules o read_rules ctxt is_logtype syn;
diff -r cafb74a131da -r b8dead547d9e src/Pure/sign.ML
--- a/src/Pure/sign.ML	Mon Mar 01 09:47:44 2010 +0100
+++ b/src/Pure/sign.ML	Mon Mar 01 17:07:36 2010 +0100
@@ -89,6 +89,7 @@
   val add_modesyntax_i: Syntax.mode -> (string * typ * mixfix) list -> theory -> theory
   val del_modesyntax: Syntax.mode -> (string * string * mixfix) list -> theory -> theory
   val del_modesyntax_i: Syntax.mode -> (string * typ * mixfix) list -> theory -> theory
+  val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> theory -> theory
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> theory -> theory
   val declare_const: (binding * typ) * mixfix -> theory -> term * theory
   val add_consts: (binding * string * mixfix) list -> theory -> theory
@@ -439,7 +440,9 @@
 
 fun add_types types thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
   let
-    val syn' = Syntax.update_type_gram (map (fn (a, n, mx) => (Name.of_binding a, n, mx)) types) syn;
+    val syn' =
+      Syntax.update_type_gram true Syntax.mode_default
+        (map (fn (a, n, mx) => (Name.of_binding a, Syntax.make_type n, mx)) types) syn;
     val decls = map (fn (a, n, _) => (a, n)) types;
     val tsig' = fold (Type.add_type naming) decls tsig;
   in (naming, syn', tsig', consts) end);
@@ -460,7 +463,9 @@
   thy |> map_sign (fn (naming, syn, tsig, consts) =>
     let
       val ctxt = ProofContext.init thy;
-      val syn' = Syntax.update_type_gram [(Name.of_binding b, length vs, mx)] syn;
+      val syn' =
+        Syntax.update_type_gram true Syntax.mode_default
+          [(Name.of_binding b, Syntax.make_type (length vs), mx)] syn;
       val abbr = (b, vs, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt rhs))
         handle ERROR msg => cat_error msg ("in type abbreviation " ^ quote (Binding.str_of b));
       val tsig' = Type.add_abbrev naming abbr tsig;
@@ -479,24 +484,30 @@
       handle ERROR msg => cat_error msg ("in syntax declaration " ^ quote c);
   in thy |> map_syn (change_gram (is_logtype thy) mode (map prep args)) end;
 
-fun gen_add_syntax x = gen_syntax Syntax.update_const_gram x;
+fun gen_add_syntax x = gen_syntax (Syntax.update_const_gram true) x;
 
 val add_modesyntax = gen_add_syntax Syntax.parse_typ;
 val add_modesyntax_i = gen_add_syntax (K I);
 val add_syntax = add_modesyntax Syntax.mode_default;
 val add_syntax_i = add_modesyntax_i Syntax.mode_default;
-val del_modesyntax = gen_syntax Syntax.remove_const_gram Syntax.parse_typ;
-val del_modesyntax_i = gen_syntax Syntax.remove_const_gram (K I);
+val del_modesyntax = gen_syntax (Syntax.update_const_gram false) Syntax.parse_typ;
+val del_modesyntax_i = gen_syntax (Syntax.update_const_gram false) (K I);
+
+fun type_notation add mode args =
+  let
+    fun type_syntax (Type (c, args), mx) =  (* FIXME authentic syntax *)
+          SOME (Long_Name.base_name c, Syntax.make_type (length args), mx)
+      | type_syntax _ = NONE;
+  in map_syn (Syntax.update_type_gram add mode (map_filter type_syntax args)) end;
 
 fun notation add mode args thy =
   let
-    val change_gram = if add then Syntax.update_const_gram else Syntax.remove_const_gram;
     fun const_syntax (Const (c, _), mx) =
           (case try (Consts.type_scheme (consts_of thy)) c of
             SOME T => SOME (Syntax.mark_const c, T, mx)
           | NONE => NONE)
       | const_syntax _ = NONE;
-  in gen_syntax change_gram (K I) mode (map_filter const_syntax args) thy end;
+  in gen_syntax (Syntax.update_const_gram add) (K I) mode (map_filter const_syntax args) thy end;
 
 
 (* add constants *)