src/Pure/Isar/local_syntax.ML
author wenzelm
Mon May 03 14:25:56 2010 +0200 (2010-05-03)
changeset 36610 bafd82950e24
parent 35429 afa8cf9e63d8
permissions -rw-r--r--
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
wenzelm@18997
     1
(*  Title:      Pure/Isar/local_syntax.ML
wenzelm@18997
     2
    Author:     Makarius
wenzelm@18997
     3
wenzelm@18997
     4
Local syntax depending on theory syntax.
wenzelm@18997
     5
*)
wenzelm@18997
     6
wenzelm@18997
     7
signature LOCAL_SYNTAX =
wenzelm@18997
     8
sig
wenzelm@18997
     9
  type T
wenzelm@18997
    10
  val syn_of: T -> Syntax.syntax
wenzelm@35429
    11
  val idents_of: T -> {structs: string list, fixes: string list}
wenzelm@18997
    12
  val init: theory -> T
wenzelm@18997
    13
  val rebuild: theory -> T -> T
wenzelm@35412
    14
  datatype kind = Type | Const | Fixed
wenzelm@35412
    15
  val add_syntax: theory -> (kind * (string * typ * mixfix)) list -> T -> T
wenzelm@20785
    16
  val set_mode: Syntax.mode -> T -> T
wenzelm@19541
    17
  val restore_mode: T -> T -> T
wenzelm@24951
    18
  val update_modesyntax: theory -> bool -> Syntax.mode ->
wenzelm@35412
    19
    (kind * (string * typ * mixfix)) list -> T -> T
wenzelm@18997
    20
end;
wenzelm@18997
    21
wenzelm@33387
    22
structure Local_Syntax: LOCAL_SYNTAX =
wenzelm@18997
    23
struct
wenzelm@18997
    24
wenzelm@18997
    25
(* datatype T *)
wenzelm@18997
    26
wenzelm@19386
    27
type local_mixfix =
wenzelm@35412
    28
  (string * bool) *  (*name, fixed?*)
wenzelm@35412
    29
  ((bool * bool * Syntax.mode) * (string * typ * mixfix));  (*type?, add?, mode, declaration*)
wenzelm@19386
    30
wenzelm@18997
    31
datatype T = Syntax of
wenzelm@18997
    32
 {thy_syntax: Syntax.syntax,
wenzelm@18997
    33
  local_syntax: Syntax.syntax,
wenzelm@20785
    34
  mode: Syntax.mode,
wenzelm@19386
    35
  mixfixes: local_mixfix list,
wenzelm@19369
    36
  idents: string list * string list};
wenzelm@18997
    37
wenzelm@19541
    38
fun make_syntax (thy_syntax, local_syntax, mode, mixfixes, idents) =
wenzelm@18997
    39
  Syntax {thy_syntax = thy_syntax, local_syntax = local_syntax,
wenzelm@19541
    40
    mode = mode, mixfixes = mixfixes, idents = idents};
wenzelm@18997
    41
wenzelm@19541
    42
fun map_syntax f (Syntax {thy_syntax, local_syntax, mode, mixfixes, idents}) =
wenzelm@19541
    43
  make_syntax (f (thy_syntax, local_syntax, mode, mixfixes, idents));
wenzelm@18997
    44
wenzelm@19369
    45
fun is_consistent thy (Syntax {thy_syntax, ...}) =
wenzelm@18997
    46
  Syntax.eq_syntax (Sign.syn_of thy, thy_syntax);
wenzelm@18997
    47
wenzelm@18997
    48
fun syn_of (Syntax {local_syntax, ...}) = local_syntax;
wenzelm@35429
    49
fun idents_of (Syntax {idents = (structs, fixes), ...}) = {structs = structs, fixes = fixes};
wenzelm@18997
    50
wenzelm@18997
    51
wenzelm@18997
    52
(* build syntax *)
wenzelm@18997
    53
wenzelm@19541
    54
fun build_syntax thy mode mixfixes (idents as (structs, _)) =
wenzelm@18997
    55
  let
wenzelm@18997
    56
    val thy_syntax = Sign.syn_of thy;
wenzelm@35412
    57
    fun update_gram ((true, add, m), decls) = Syntax.update_type_gram add m decls
wenzelm@35412
    58
      | update_gram ((false, add, m), decls) =
wenzelm@35412
    59
          Syntax.update_const_gram add (Sign.is_logtype thy) m decls;
wenzelm@35412
    60
wenzelm@18997
    61
    val (atrs, trs, trs', atrs') = Syntax.struct_trfuns structs;
wenzelm@18997
    62
    val local_syntax = thy_syntax
wenzelm@25390
    63
      |> Syntax.update_trfuns
wenzelm@19386
    64
          (map Syntax.mk_trfun atrs, map Syntax.mk_trfun trs,
wenzelm@19386
    65
           map Syntax.mk_trfun trs', map Syntax.mk_trfun atrs')
wenzelm@35412
    66
      |> fold update_gram (AList.coalesce (op =) (rev (map snd mixfixes)));
wenzelm@19541
    67
  in make_syntax (thy_syntax, local_syntax, mode, mixfixes, idents) end;
wenzelm@19541
    68
wenzelm@24960
    69
fun init thy = build_syntax thy Syntax.mode_default [] ([], []);
wenzelm@18997
    70
wenzelm@19541
    71
fun rebuild thy (syntax as Syntax {mode, mixfixes, idents, ...}) =
wenzelm@19541
    72
  if is_consistent thy syntax then syntax
wenzelm@19541
    73
  else build_syntax thy mode mixfixes idents;
wenzelm@18997
    74
wenzelm@19541
    75
wenzelm@18997
    76
(* mixfix declarations *)
wenzelm@18997
    77
wenzelm@35412
    78
datatype kind = Type | Const | Fixed;
wenzelm@35412
    79
wenzelm@18997
    80
local
wenzelm@18997
    81
wenzelm@35412
    82
fun prep_mixfix _ _ (_, (_, _, Structure)) = NONE
wenzelm@35412
    83
  | prep_mixfix add mode (Type, decl as (x, _, _)) = SOME ((x, false), ((true, add, mode), decl))
wenzelm@35412
    84
  | prep_mixfix add mode (Const, decl as (x, _, _)) = SOME ((x, false), ((false, add, mode), decl))
wenzelm@35412
    85
  | prep_mixfix add mode (Fixed, (x, T, mx)) =
wenzelm@35412
    86
      SOME ((x, true), ((false, add, mode), (Syntax.mark_fixed x, T, mx)));
wenzelm@19016
    87
wenzelm@35412
    88
fun prep_struct (Fixed, (c, _, Structure)) = SOME c
wenzelm@35412
    89
  | prep_struct (_, (c, _, Structure)) = error ("Bad mixfix declaration for " ^ quote c)
wenzelm@19016
    90
  | prep_struct _ = NONE;
wenzelm@18997
    91
wenzelm@18997
    92
in
wenzelm@18997
    93
wenzelm@24951
    94
fun update_syntax add thy raw_decls
wenzelm@24951
    95
    (syntax as (Syntax {mode, mixfixes, idents = (structs, _), ...})) =
wenzelm@24951
    96
  (case filter_out (fn (_, (_, _, mx)) => mx = NoSyn) raw_decls of
wenzelm@19016
    97
    [] => syntax
wenzelm@19016
    98
  | decls =>
wenzelm@19016
    99
      let
wenzelm@35412
   100
        val new_mixfixes = map_filter (prep_mixfix add mode) decls;
wenzelm@24954
   101
        val new_structs = map_filter prep_struct decls;
wenzelm@24954
   102
        val mixfixes' = rev new_mixfixes @ mixfixes;
wenzelm@24954
   103
        val structs' =
wenzelm@24954
   104
          if add then structs @ new_structs
wenzelm@24954
   105
          else subtract (op =) new_structs structs;
wenzelm@20785
   106
        val fixes' = fold (fn ((x, true), _) => cons x | _ => I) mixfixes' [];
wenzelm@19541
   107
      in build_syntax thy mode mixfixes' (structs', fixes') end);
wenzelm@18997
   108
wenzelm@24951
   109
val add_syntax = update_syntax true;
wenzelm@24951
   110
wenzelm@18997
   111
end;
wenzelm@18997
   112
wenzelm@18997
   113
wenzelm@19660
   114
(* syntax mode *)
wenzelm@19660
   115
wenzelm@19660
   116
fun set_mode mode = map_syntax (fn (thy_syntax, local_syntax, _, mixfixes, idents) =>
wenzelm@19660
   117
  (thy_syntax, local_syntax, mode, mixfixes, idents));
wenzelm@19660
   118
wenzelm@19660
   119
fun restore_mode (Syntax {mode, ...}) = set_mode mode;
wenzelm@19660
   120
wenzelm@24951
   121
fun update_modesyntax thy add mode args syntax =
wenzelm@24951
   122
  syntax |> set_mode mode |> update_syntax add thy args |> restore_mode syntax;
wenzelm@19660
   123
wenzelm@18997
   124
end;