src/Pure/Isar/local_syntax.ML
author wenzelm
Wed Oct 10 17:31:59 2007 +0200 (2007-10-10)
changeset 24951 834b8c2b9553
parent 20785 d60f81c56fd4
child 24954 0664f10a4094
permissions -rw-r--r--
replaced add_modesyntax by general update_modesyntax (add or del);
tuned;
wenzelm@18997
     1
(*  Title:      Pure/Isar/local_syntax.ML
wenzelm@18997
     2
    ID:         $Id$
wenzelm@18997
     3
    Author:     Makarius
wenzelm@18997
     4
wenzelm@18997
     5
Local syntax depending on theory syntax.
wenzelm@18997
     6
*)
wenzelm@18997
     7
wenzelm@18997
     8
val show_structs = ref false;
wenzelm@18997
     9
wenzelm@18997
    10
signature LOCAL_SYNTAX =
wenzelm@18997
    11
sig
wenzelm@18997
    12
  type T
wenzelm@18997
    13
  val syn_of: T -> Syntax.syntax
wenzelm@18997
    14
  val structs_of: T -> string list
wenzelm@18997
    15
  val init: theory -> T
wenzelm@18997
    16
  val rebuild: theory -> T -> T
wenzelm@19660
    17
  val add_syntax: theory -> (bool * (string * typ * mixfix)) list -> T -> T
wenzelm@20785
    18
  val set_mode: Syntax.mode -> T -> T
wenzelm@19541
    19
  val restore_mode: T -> T -> T
wenzelm@24951
    20
  val update_modesyntax: theory -> bool -> Syntax.mode ->
wenzelm@24951
    21
    (bool * (string * typ * mixfix)) list -> T -> T
wenzelm@19369
    22
  val extern_term: T -> term -> term
wenzelm@18997
    23
end;
wenzelm@18997
    24
wenzelm@19016
    25
structure LocalSyntax: LOCAL_SYNTAX =
wenzelm@18997
    26
struct
wenzelm@18997
    27
wenzelm@18997
    28
(* datatype T *)
wenzelm@18997
    29
wenzelm@19386
    30
type local_mixfix =
wenzelm@24951
    31
  (string * bool) *                                    (*name, fixed?*)
wenzelm@24951
    32
  ((bool * Syntax.mode) * (string * typ * mixfix));    (*add?, mode, declaration*)
wenzelm@19386
    33
wenzelm@18997
    34
datatype T = Syntax of
wenzelm@18997
    35
 {thy_syntax: Syntax.syntax,
wenzelm@18997
    36
  local_syntax: Syntax.syntax,
wenzelm@20785
    37
  mode: Syntax.mode,
wenzelm@19386
    38
  mixfixes: local_mixfix list,
wenzelm@19369
    39
  idents: string list * string list};
wenzelm@18997
    40
wenzelm@19541
    41
fun make_syntax (thy_syntax, local_syntax, mode, mixfixes, idents) =
wenzelm@18997
    42
  Syntax {thy_syntax = thy_syntax, local_syntax = local_syntax,
wenzelm@19541
    43
    mode = mode, mixfixes = mixfixes, idents = idents};
wenzelm@18997
    44
wenzelm@19541
    45
fun map_syntax f (Syntax {thy_syntax, local_syntax, mode, mixfixes, idents}) =
wenzelm@19541
    46
  make_syntax (f (thy_syntax, local_syntax, mode, mixfixes, idents));
wenzelm@18997
    47
wenzelm@19369
    48
fun is_consistent thy (Syntax {thy_syntax, ...}) =
wenzelm@18997
    49
  Syntax.eq_syntax (Sign.syn_of thy, thy_syntax);
wenzelm@18997
    50
wenzelm@18997
    51
fun syn_of (Syntax {local_syntax, ...}) = local_syntax;
wenzelm@18997
    52
fun idents_of (Syntax {idents, ...}) = idents;
wenzelm@18997
    53
val structs_of = #1 o idents_of;
wenzelm@18997
    54
wenzelm@18997
    55
wenzelm@18997
    56
(* build syntax *)
wenzelm@18997
    57
wenzelm@19541
    58
fun build_syntax thy mode mixfixes (idents as (structs, _)) =
wenzelm@18997
    59
  let
wenzelm@18997
    60
    val thy_syntax = Sign.syn_of thy;
wenzelm@18997
    61
    val is_logtype = Sign.is_logtype thy;
wenzelm@24951
    62
    fun const_gram ((true, m), decls) = Syntax.extend_const_gram is_logtype m decls
wenzelm@24951
    63
      | const_gram ((false, m), decls) = Syntax.remove_const_gram is_logtype m decls;
wenzelm@18997
    64
    val (atrs, trs, trs', atrs') = Syntax.struct_trfuns structs;
wenzelm@18997
    65
    val local_syntax = thy_syntax
wenzelm@18997
    66
      |> Syntax.extend_trfuns
wenzelm@19386
    67
          (map Syntax.mk_trfun atrs, map Syntax.mk_trfun trs,
wenzelm@19386
    68
           map Syntax.mk_trfun trs', map Syntax.mk_trfun atrs')
wenzelm@24951
    69
      |> fold const_gram (AList.coalesce (op =) (rev (map snd mixfixes)));
wenzelm@19541
    70
  in make_syntax (thy_syntax, local_syntax, mode, mixfixes, idents) end;
wenzelm@19541
    71
wenzelm@19541
    72
fun init thy = build_syntax thy Syntax.default_mode [] ([], []);
wenzelm@18997
    73
wenzelm@19541
    74
fun rebuild thy (syntax as Syntax {mode, mixfixes, idents, ...}) =
wenzelm@19541
    75
  if is_consistent thy syntax then syntax
wenzelm@19541
    76
  else build_syntax thy mode mixfixes idents;
wenzelm@18997
    77
wenzelm@19541
    78
wenzelm@18997
    79
(* mixfix declarations *)
wenzelm@18997
    80
wenzelm@18997
    81
local
wenzelm@18997
    82
wenzelm@24951
    83
fun prep_mixfix _ (_, (_, _, Structure)) = NONE
wenzelm@24951
    84
  | prep_mixfix mode (fixed, (x, T, mx)) =
wenzelm@24951
    85
      let val c = if fixed then Syntax.fixedN ^ x else x
wenzelm@24951
    86
      in SOME ((x, fixed), (mode, (c, T, mx))) end;
wenzelm@19016
    87
wenzelm@19016
    88
fun prep_struct (fixed, (c, _, Structure)) =
wenzelm@19016
    89
      if fixed then SOME c
wenzelm@24951
    90
      else error ("Bad mixfix declaration for constant: " ^ quote c)
wenzelm@19016
    91
  | prep_struct _ = NONE;
wenzelm@18997
    92
wenzelm@18997
    93
in
wenzelm@18997
    94
wenzelm@24951
    95
fun update_syntax add thy raw_decls
wenzelm@24951
    96
    (syntax as (Syntax {mode, mixfixes, idents = (structs, _), ...})) =
wenzelm@24951
    97
  (case filter_out (fn (_, (_, _, mx)) => mx = NoSyn) raw_decls of
wenzelm@19016
    98
    [] => syntax
wenzelm@19016
    99
  | decls =>
wenzelm@19016
   100
      let
wenzelm@24951
   101
        val mixfixes' = rev (map_filter (prep_mixfix (add, mode)) decls) @ mixfixes;
wenzelm@24951
   102
        val structs' = structs @ map_filter prep_struct decls;
wenzelm@20785
   103
        val fixes' = fold (fn ((x, true), _) => cons x | _ => I) mixfixes' [];
wenzelm@19541
   104
      in build_syntax thy mode mixfixes' (structs', fixes') end);
wenzelm@18997
   105
wenzelm@24951
   106
val add_syntax = update_syntax true;
wenzelm@24951
   107
wenzelm@18997
   108
end;
wenzelm@18997
   109
wenzelm@18997
   110
wenzelm@19660
   111
(* syntax mode *)
wenzelm@19660
   112
wenzelm@19660
   113
fun set_mode mode = map_syntax (fn (thy_syntax, local_syntax, _, mixfixes, idents) =>
wenzelm@19660
   114
  (thy_syntax, local_syntax, mode, mixfixes, idents));
wenzelm@19660
   115
wenzelm@19660
   116
fun restore_mode (Syntax {mode, ...}) = set_mode mode;
wenzelm@19660
   117
wenzelm@24951
   118
fun update_modesyntax thy add mode args syntax =
wenzelm@24951
   119
  syntax |> set_mode mode |> update_syntax add thy args |> restore_mode syntax;
wenzelm@19660
   120
wenzelm@19660
   121
wenzelm@18997
   122
(* extern_term *)
wenzelm@18997
   123
wenzelm@19369
   124
fun extern_term syntax =
wenzelm@18997
   125
  let
wenzelm@19369
   126
    val (structs, fixes) = idents_of syntax;
wenzelm@18997
   127
    fun map_free (t as Free (x, T)) =
wenzelm@19618
   128
          let val i = find_index (fn s => s = x) structs + 1 in
wenzelm@18997
   129
            if i = 0 andalso member (op =) fixes x then
wenzelm@18997
   130
              Const (Syntax.fixedN ^ x, T)
wenzelm@18997
   131
            else if i = 1 andalso not (! show_structs) then
wenzelm@18997
   132
              Syntax.const "_struct" $ Syntax.const "_indexdefault"
wenzelm@18997
   133
            else t
wenzelm@18997
   134
          end
wenzelm@18997
   135
      | map_free t = t;
wenzelm@19369
   136
  in Term.map_aterms map_free end;
wenzelm@18997
   137
wenzelm@18997
   138
end;