more uniform treatment of syntax for types vs. consts;
authorwenzelm
Mon Mar 01 17:07:36 2010 +0100 (2010-03-01)
changeset 35412b8dead547d9e
parent 35411 cafb74a131da
child 35413 4c7cba1f7ce9
more uniform treatment of syntax for types vs. consts;
src/Pure/Isar/local_syntax.ML
src/Pure/Isar/local_theory.ML
src/Pure/Isar/proof_context.ML
src/Pure/Syntax/mixfix.ML
src/Pure/Syntax/syntax.ML
src/Pure/sign.ML
     1.1 --- a/src/Pure/Isar/local_syntax.ML	Mon Mar 01 09:47:44 2010 +0100
     1.2 +++ b/src/Pure/Isar/local_syntax.ML	Mon Mar 01 17:07:36 2010 +0100
     1.3 @@ -13,11 +13,12 @@
     1.4    val structs_of: T -> string list
     1.5    val init: theory -> T
     1.6    val rebuild: theory -> T -> T
     1.7 -  val add_syntax: theory -> (bool * (string * typ * mixfix)) list -> T -> T
     1.8 +  datatype kind = Type | Const | Fixed
     1.9 +  val add_syntax: theory -> (kind * (string * typ * mixfix)) list -> T -> T
    1.10    val set_mode: Syntax.mode -> T -> T
    1.11    val restore_mode: T -> T -> T
    1.12    val update_modesyntax: theory -> bool -> Syntax.mode ->
    1.13 -    (bool * (string * typ * mixfix)) list -> T -> T
    1.14 +    (kind * (string * typ * mixfix)) list -> T -> T
    1.15    val extern_term: T -> term -> term
    1.16  end;
    1.17  
    1.18 @@ -27,8 +28,8 @@
    1.19  (* datatype T *)
    1.20  
    1.21  type local_mixfix =
    1.22 -  (string * bool) *                                    (*name, fixed?*)
    1.23 -  ((bool * Syntax.mode) * (string * typ * mixfix));    (*add?, mode, declaration*)
    1.24 +  (string * bool) *  (*name, fixed?*)
    1.25 +  ((bool * bool * Syntax.mode) * (string * typ * mixfix));  (*type?, add?, mode, declaration*)
    1.26  
    1.27  datatype T = Syntax of
    1.28   {thy_syntax: Syntax.syntax,
    1.29 @@ -57,15 +58,16 @@
    1.30  fun build_syntax thy mode mixfixes (idents as (structs, _)) =
    1.31    let
    1.32      val thy_syntax = Sign.syn_of thy;
    1.33 -    val is_logtype = Sign.is_logtype thy;
    1.34 -    fun const_gram ((true, m), decls) = Syntax.update_const_gram is_logtype m decls
    1.35 -      | const_gram ((false, m), decls) = Syntax.remove_const_gram is_logtype m decls;
    1.36 +    fun update_gram ((true, add, m), decls) = Syntax.update_type_gram add m decls
    1.37 +      | update_gram ((false, add, m), decls) =
    1.38 +          Syntax.update_const_gram add (Sign.is_logtype thy) m decls;
    1.39 +
    1.40      val (atrs, trs, trs', atrs') = Syntax.struct_trfuns structs;
    1.41      val local_syntax = thy_syntax
    1.42        |> Syntax.update_trfuns
    1.43            (map Syntax.mk_trfun atrs, map Syntax.mk_trfun trs,
    1.44             map Syntax.mk_trfun trs', map Syntax.mk_trfun atrs')
    1.45 -      |> fold const_gram (AList.coalesce (op =) (rev (map snd mixfixes)));
    1.46 +      |> fold update_gram (AList.coalesce (op =) (rev (map snd mixfixes)));
    1.47    in make_syntax (thy_syntax, local_syntax, mode, mixfixes, idents) end;
    1.48  
    1.49  fun init thy = build_syntax thy Syntax.mode_default [] ([], []);
    1.50 @@ -77,16 +79,18 @@
    1.51  
    1.52  (* mixfix declarations *)
    1.53  
    1.54 +datatype kind = Type | Const | Fixed;
    1.55 +
    1.56  local
    1.57  
    1.58 -fun prep_mixfix _ (_, (_, _, Structure)) = NONE
    1.59 -  | prep_mixfix mode (fixed, (x, T, mx)) =
    1.60 -      let val c = if fixed then Syntax.fixedN ^ x else x
    1.61 -      in SOME ((x, fixed), (mode, (c, T, mx))) end;
    1.62 +fun prep_mixfix _ _ (_, (_, _, Structure)) = NONE
    1.63 +  | prep_mixfix add mode (Type, decl as (x, _, _)) = SOME ((x, false), ((true, add, mode), decl))
    1.64 +  | prep_mixfix add mode (Const, decl as (x, _, _)) = SOME ((x, false), ((false, add, mode), decl))
    1.65 +  | prep_mixfix add mode (Fixed, (x, T, mx)) =
    1.66 +      SOME ((x, true), ((false, add, mode), (Syntax.mark_fixed x, T, mx)));
    1.67  
    1.68 -fun prep_struct (fixed, (c, _, Structure)) =
    1.69 -      if fixed then SOME c
    1.70 -      else error ("Bad mixfix declaration for constant: " ^ quote c)
    1.71 +fun prep_struct (Fixed, (c, _, Structure)) = SOME c
    1.72 +  | prep_struct (_, (c, _, Structure)) = error ("Bad mixfix declaration for " ^ quote c)
    1.73    | prep_struct _ = NONE;
    1.74  
    1.75  in
    1.76 @@ -97,7 +101,7 @@
    1.77      [] => syntax
    1.78    | decls =>
    1.79        let
    1.80 -        val new_mixfixes = map_filter (prep_mixfix (add, mode)) decls;
    1.81 +        val new_mixfixes = map_filter (prep_mixfix add mode) decls;
    1.82          val new_structs = map_filter prep_struct decls;
    1.83          val mixfixes' = rev new_mixfixes @ mixfixes;
    1.84          val structs' =
    1.85 @@ -130,7 +134,7 @@
    1.86      fun map_free (t as Free (x, T)) =
    1.87            let val i = find_index (fn s => s = x) structs + 1 in
    1.88              if i = 0 andalso member (op =) fixes x then
    1.89 -              Const (Syntax.fixedN ^ x, T)
    1.90 +              Term.Const (Syntax.mark_fixed x, T)
    1.91              else if i = 1 andalso not (! show_structs) then
    1.92                Syntax.const "_struct" $ Syntax.const "_indexdefault"
    1.93              else t
     2.1 --- a/src/Pure/Isar/local_theory.ML	Mon Mar 01 09:47:44 2010 +0100
     2.2 +++ b/src/Pure/Isar/local_theory.ML	Mon Mar 01 17:07:36 2010 +0100
     2.3 @@ -42,6 +42,7 @@
     2.4    val type_syntax: bool -> declaration -> local_theory -> local_theory
     2.5    val term_syntax: bool -> declaration -> local_theory -> local_theory
     2.6    val declaration: bool -> declaration -> local_theory -> local_theory
     2.7 +  val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory
     2.8    val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
     2.9    val init: serial option -> string -> operations -> Proof.context -> local_theory
    2.10    val restore: local_theory -> local_theory
    2.11 @@ -198,6 +199,10 @@
    2.12  val notes = notes_kind "";
    2.13  fun note (a, ths) = notes [(a, [(ths, [])])] #>> the_single;
    2.14  
    2.15 +fun type_notation add mode raw_args lthy =
    2.16 +  let val args = map (apfst (Morphism.typ (target_morphism lthy))) raw_args
    2.17 +  in type_syntax false (ProofContext.target_type_notation add mode args) lthy end;
    2.18 +
    2.19  fun notation add mode raw_args lthy =
    2.20    let val args = map (apfst (Morphism.term (target_morphism lthy))) raw_args
    2.21    in term_syntax false (ProofContext.target_notation add mode args) lthy end;
     3.1 --- a/src/Pure/Isar/proof_context.ML	Mon Mar 01 09:47:44 2010 +0100
     3.2 +++ b/src/Pure/Isar/proof_context.ML	Mon Mar 01 17:07:36 2010 +0100
     3.3 @@ -115,7 +115,10 @@
     3.4    val add_cases: bool -> (string * Rule_Cases.T option) list -> Proof.context -> Proof.context
     3.5    val apply_case: Rule_Cases.T -> Proof.context -> (string * term list) list * Proof.context
     3.6    val get_case: Proof.context -> string -> string option list -> Rule_Cases.T
     3.7 +  val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> Proof.context -> Proof.context
     3.8    val notation: bool -> Syntax.mode -> (term * mixfix) list -> Proof.context -> Proof.context
     3.9 +  val target_type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> morphism ->
    3.10 +    Context.generic -> Context.generic
    3.11    val target_notation: bool -> Syntax.mode -> (term * mixfix) list -> morphism ->
    3.12      Context.generic -> Context.generic
    3.13    val add_const_constraint: string * typ option -> Proof.context -> Proof.context
    3.14 @@ -1029,18 +1032,34 @@
    3.15  
    3.16  local
    3.17  
    3.18 -fun const_syntax _ (Free (x, T), mx) = SOME (true, (x, T, mx))
    3.19 +fun type_syntax (Type (c, args), mx) =  (* FIXME authentic syntax *)
    3.20 +      SOME (Local_Syntax.Type, (Long_Name.base_name c, Syntax.make_type (length args), mx))
    3.21 +  | type_syntax _ = NONE;
    3.22 +
    3.23 +fun const_syntax _ (Free (x, T), mx) = SOME (Local_Syntax.Fixed, (x, T, mx))
    3.24    | const_syntax ctxt (Const (c, _), mx) =
    3.25        (case try (Consts.type_scheme (consts_of ctxt)) c of
    3.26 -        SOME T => SOME (false, (Syntax.mark_const c, T, mx))
    3.27 +        SOME T => SOME (Local_Syntax.Const, (Syntax.mark_const c, T, mx))
    3.28        | NONE => NONE)
    3.29    | const_syntax _ _ = NONE;
    3.30  
    3.31 +fun gen_notation syntax add mode args ctxt =
    3.32 +  ctxt |> map_syntax
    3.33 +    (Local_Syntax.update_modesyntax (theory_of ctxt) add mode (map_filter (syntax ctxt) args));
    3.34 +
    3.35  in
    3.36  
    3.37 -fun notation add mode args ctxt =
    3.38 -  ctxt |> map_syntax
    3.39 -    (Local_Syntax.update_modesyntax (theory_of ctxt) add mode (map_filter (const_syntax ctxt) args));
    3.40 +val type_notation = gen_notation (K type_syntax);
    3.41 +val notation = gen_notation const_syntax;
    3.42 +
    3.43 +fun target_type_notation add  mode args phi =
    3.44 +  let
    3.45 +    val args' = args |> map_filter (fn (T, mx) =>
    3.46 +      let
    3.47 +        val T' = Morphism.typ phi T;
    3.48 +        val similar = (case (T, T') of (Type (c, _), Type (c', _)) => c = c' | _ => false);
    3.49 +      in if similar then SOME (T', mx) else NONE end);
    3.50 +  in Context.mapping (Sign.type_notation add mode args') (type_notation add mode args') end;
    3.51  
    3.52  fun target_notation add mode args phi =
    3.53    let
    3.54 @@ -1049,6 +1068,7 @@
    3.55        in if Term.aconv_untyped (t, t') then SOME (t', mx) else NONE end);
    3.56    in Context.mapping (Sign.notation add mode args') (notation add mode args') end;
    3.57  
    3.58 +
    3.59  end;
    3.60  
    3.61  
    3.62 @@ -1086,7 +1106,7 @@
    3.63    if mx <> NoSyn andalso mx <> Structure andalso
    3.64        (can Name.dest_internal x orelse can Name.dest_skolem x) then
    3.65      error ("Illegal mixfix syntax for internal/skolem constant " ^ quote x)
    3.66 -  else (true, (x, T, mx));
    3.67 +  else (Local_Syntax.Fixed, (x, T, mx));
    3.68  
    3.69  in
    3.70  
     4.1 --- a/src/Pure/Syntax/mixfix.ML	Mon Mar 01 09:47:44 2010 +0100
     4.2 +++ b/src/Pure/Syntax/mixfix.ML	Mon Mar 01 17:07:36 2010 +0100
     4.3 @@ -25,12 +25,13 @@
     4.4    val pretty_mixfix: mixfix -> Pretty.T
     4.5    val mixfix_args: mixfix -> int
     4.6    val mixfixT: mixfix -> typ
     4.7 +  val make_type: int -> typ
     4.8  end;
     4.9  
    4.10  signature MIXFIX =
    4.11  sig
    4.12    include MIXFIX1
    4.13 -  val syn_ext_types: (string * int * mixfix) list -> SynExt.syn_ext
    4.14 +  val syn_ext_types: (string * typ * mixfix) list -> SynExt.syn_ext
    4.15    val syn_ext_consts: (string -> bool) -> (string * typ * mixfix) list -> SynExt.syn_ext
    4.16  end;
    4.17  
    4.18 @@ -96,21 +97,22 @@
    4.19  
    4.20  (* syn_ext_types *)
    4.21  
    4.22 +fun make_type n = replicate n SynExt.typeT ---> SynExt.typeT;
    4.23 +
    4.24  fun syn_ext_types type_decls =
    4.25    let
    4.26 -    fun mk_type n = replicate n SynExt.typeT ---> SynExt.typeT;
    4.27 -    fun mk_infix sy n t p1 p2 p3 = SynExt.Mfix ("(_ " ^ sy ^ "/ _)", mk_type n, t, [p1, p2], p3);
    4.28 +    fun mk_infix sy ty t p1 p2 p3 = SynExt.Mfix ("(_ " ^ sy ^ "/ _)", ty, t, [p1, p2], p3);
    4.29  
    4.30      fun mfix_of (_, _, NoSyn) = NONE
    4.31 -      | mfix_of (t, n, Mixfix (sy, ps, p)) = SOME (SynExt.Mfix (sy, mk_type n, t, ps, p))
    4.32 -      | mfix_of (t, n, Delimfix sy) = SOME (SynExt.Mfix (sy, mk_type n, t, [], SynExt.max_pri))
    4.33 -      | mfix_of (t, n, Infix (sy, p)) = SOME (mk_infix sy n t (p + 1) (p + 1) p)
    4.34 -      | mfix_of (t, n, Infixl (sy, p)) = SOME (mk_infix sy n t p (p + 1) p)
    4.35 -      | mfix_of (t, n, Infixr (sy, p)) = SOME (mk_infix sy n t (p + 1) p p)
    4.36 +      | mfix_of (t, ty, Mixfix (sy, ps, p)) = SOME (SynExt.Mfix (sy, ty, t, ps, p))
    4.37 +      | mfix_of (t, ty, Delimfix sy) = SOME (SynExt.Mfix (sy, ty, t, [], SynExt.max_pri))
    4.38 +      | mfix_of (t, ty, Infix (sy, p)) = SOME (mk_infix sy ty t (p + 1) (p + 1) p)
    4.39 +      | mfix_of (t, ty, Infixl (sy, p)) = SOME (mk_infix sy ty t p (p + 1) p)
    4.40 +      | mfix_of (t, ty, Infixr (sy, p)) = SOME (mk_infix sy ty t (p + 1) p p)
    4.41        | mfix_of (t, _, _) = error ("Bad mixfix declaration for " ^ quote t);  (* FIXME printable t (!?) *)
    4.42  
    4.43 -    fun check_args (t, n, _) (SOME (mfix as SynExt.Mfix (sy, _, _, _, _))) =
    4.44 -          if SynExt.mfix_args sy = n then ()
    4.45 +    fun check_args (_, ty, _) (SOME (mfix as SynExt.Mfix (sy, _, _, _, _))) =
    4.46 +          if length (Term.binder_types ty) = SynExt.mfix_args sy then ()
    4.47            else SynExt.err_in_mfix "Bad number of type constructor arguments" mfix
    4.48        | check_args _ NONE = ();
    4.49  
     5.1 --- a/src/Pure/Syntax/syntax.ML	Mon Mar 01 09:47:44 2010 +0100
     5.2 +++ b/src/Pure/Syntax/syntax.ML	Mon Mar 01 17:07:36 2010 +0100
     5.3 @@ -59,7 +59,6 @@
     5.4      Proof.context -> syntax -> bool -> term -> Pretty.T
     5.5    val standard_unparse_typ: Proof.context -> syntax -> typ -> Pretty.T
     5.6    val standard_unparse_sort: Proof.context -> syntax -> sort -> Pretty.T
     5.7 -  val update_type_gram: (string * int * mixfix) list -> syntax -> syntax
     5.8    val update_consts: string list -> syntax -> syntax
     5.9    val update_trfuns:
    5.10      (string * ((ast list -> ast) * stamp)) list *
    5.11 @@ -73,9 +72,8 @@
    5.12      (string * ((Proof.context -> ast list -> ast) * stamp)) list -> syntax -> syntax
    5.13    val extend_tokentrfuns: (string * string * (Proof.context -> string -> Pretty.T)) list ->
    5.14      syntax -> syntax
    5.15 -  val update_const_gram: (string -> bool) ->
    5.16 -    mode -> (string * typ * mixfix) list -> syntax -> syntax
    5.17 -  val remove_const_gram: (string -> bool) ->
    5.18 +  val update_type_gram: bool -> mode -> (string * typ * mixfix) list -> syntax -> syntax
    5.19 +  val update_const_gram: bool -> (string -> bool) ->
    5.20      mode -> (string * typ * mixfix) list -> syntax -> syntax
    5.21    val update_trrules: Proof.context -> (string -> bool) -> syntax ->
    5.22      (string * string) trrule list -> syntax -> syntax
    5.23 @@ -669,17 +667,16 @@
    5.24  
    5.25  fun ext_syntax f decls = update_syntax mode_default (f decls);
    5.26  
    5.27 -val update_type_gram       = ext_syntax Mixfix.syn_ext_types;
    5.28 -val update_consts          = ext_syntax SynExt.syn_ext_const_names;
    5.29 -val update_trfuns          = ext_syntax SynExt.syn_ext_trfuns;
    5.30 +val update_consts = ext_syntax SynExt.syn_ext_const_names;
    5.31 +val update_trfuns = ext_syntax SynExt.syn_ext_trfuns;
    5.32  val update_advanced_trfuns = ext_syntax SynExt.syn_ext_advanced_trfuns;
    5.33 -val extend_tokentrfuns     = ext_syntax SynExt.syn_ext_tokentrfuns;
    5.34 +val extend_tokentrfuns = ext_syntax SynExt.syn_ext_tokentrfuns;
    5.35  
    5.36 -fun update_const_gram is_logtype prmode decls =
    5.37 -  update_syntax prmode (Mixfix.syn_ext_consts is_logtype decls);
    5.38 +fun update_type_gram add prmode decls =
    5.39 +  (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_types decls);
    5.40  
    5.41 -fun remove_const_gram is_logtype prmode decls =
    5.42 -  remove_syntax prmode (Mixfix.syn_ext_consts is_logtype decls);
    5.43 +fun update_const_gram add is_logtype prmode decls =
    5.44 +  (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_consts is_logtype decls);
    5.45  
    5.46  fun update_trrules ctxt is_logtype syn =
    5.47    ext_syntax SynExt.syn_ext_rules o read_rules ctxt is_logtype syn;
     6.1 --- a/src/Pure/sign.ML	Mon Mar 01 09:47:44 2010 +0100
     6.2 +++ b/src/Pure/sign.ML	Mon Mar 01 17:07:36 2010 +0100
     6.3 @@ -89,6 +89,7 @@
     6.4    val add_modesyntax_i: Syntax.mode -> (string * typ * mixfix) list -> theory -> theory
     6.5    val del_modesyntax: Syntax.mode -> (string * string * mixfix) list -> theory -> theory
     6.6    val del_modesyntax_i: Syntax.mode -> (string * typ * mixfix) list -> theory -> theory
     6.7 +  val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> theory -> theory
     6.8    val notation: bool -> Syntax.mode -> (term * mixfix) list -> theory -> theory
     6.9    val declare_const: (binding * typ) * mixfix -> theory -> term * theory
    6.10    val add_consts: (binding * string * mixfix) list -> theory -> theory
    6.11 @@ -439,7 +440,9 @@
    6.12  
    6.13  fun add_types types thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
    6.14    let
    6.15 -    val syn' = Syntax.update_type_gram (map (fn (a, n, mx) => (Name.of_binding a, n, mx)) types) syn;
    6.16 +    val syn' =
    6.17 +      Syntax.update_type_gram true Syntax.mode_default
    6.18 +        (map (fn (a, n, mx) => (Name.of_binding a, Syntax.make_type n, mx)) types) syn;
    6.19      val decls = map (fn (a, n, _) => (a, n)) types;
    6.20      val tsig' = fold (Type.add_type naming) decls tsig;
    6.21    in (naming, syn', tsig', consts) end);
    6.22 @@ -460,7 +463,9 @@
    6.23    thy |> map_sign (fn (naming, syn, tsig, consts) =>
    6.24      let
    6.25        val ctxt = ProofContext.init thy;
    6.26 -      val syn' = Syntax.update_type_gram [(Name.of_binding b, length vs, mx)] syn;
    6.27 +      val syn' =
    6.28 +        Syntax.update_type_gram true Syntax.mode_default
    6.29 +          [(Name.of_binding b, Syntax.make_type (length vs), mx)] syn;
    6.30        val abbr = (b, vs, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt rhs))
    6.31          handle ERROR msg => cat_error msg ("in type abbreviation " ^ quote (Binding.str_of b));
    6.32        val tsig' = Type.add_abbrev naming abbr tsig;
    6.33 @@ -479,24 +484,30 @@
    6.34        handle ERROR msg => cat_error msg ("in syntax declaration " ^ quote c);
    6.35    in thy |> map_syn (change_gram (is_logtype thy) mode (map prep args)) end;
    6.36  
    6.37 -fun gen_add_syntax x = gen_syntax Syntax.update_const_gram x;
    6.38 +fun gen_add_syntax x = gen_syntax (Syntax.update_const_gram true) x;
    6.39  
    6.40  val add_modesyntax = gen_add_syntax Syntax.parse_typ;
    6.41  val add_modesyntax_i = gen_add_syntax (K I);
    6.42  val add_syntax = add_modesyntax Syntax.mode_default;
    6.43  val add_syntax_i = add_modesyntax_i Syntax.mode_default;
    6.44 -val del_modesyntax = gen_syntax Syntax.remove_const_gram Syntax.parse_typ;
    6.45 -val del_modesyntax_i = gen_syntax Syntax.remove_const_gram (K I);
    6.46 +val del_modesyntax = gen_syntax (Syntax.update_const_gram false) Syntax.parse_typ;
    6.47 +val del_modesyntax_i = gen_syntax (Syntax.update_const_gram false) (K I);
    6.48 +
    6.49 +fun type_notation add mode args =
    6.50 +  let
    6.51 +    fun type_syntax (Type (c, args), mx) =  (* FIXME authentic syntax *)
    6.52 +          SOME (Long_Name.base_name c, Syntax.make_type (length args), mx)
    6.53 +      | type_syntax _ = NONE;
    6.54 +  in map_syn (Syntax.update_type_gram add mode (map_filter type_syntax args)) end;
    6.55  
    6.56  fun notation add mode args thy =
    6.57    let
    6.58 -    val change_gram = if add then Syntax.update_const_gram else Syntax.remove_const_gram;
    6.59      fun const_syntax (Const (c, _), mx) =
    6.60            (case try (Consts.type_scheme (consts_of thy)) c of
    6.61              SOME T => SOME (Syntax.mark_const c, T, mx)
    6.62            | NONE => NONE)
    6.63        | const_syntax _ = NONE;
    6.64 -  in gen_syntax change_gram (K I) mode (map_filter const_syntax args) thy end;
    6.65 +  in gen_syntax (Syntax.update_const_gram add) (K I) mode (map_filter const_syntax args) thy end;
    6.66  
    6.67  
    6.68  (* add constants *)