src/Pure/Isar/local_syntax.ML
author wenzelm
Tue May 02 20:42:37 2006 +0200 (2006-05-02)
changeset 19541 1bb8e26a26ee
parent 19482 9f11af8f7ef9
child 19618 9050a3b01e62
permissions -rw-r--r--
maintain implicit syntax mode;
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@19541
    17
  val set_mode: string * bool -> T -> T
wenzelm@19541
    18
  val restore_mode: T -> T -> T
wenzelm@19541
    19
  val add_syntax: theory -> (bool * (string * typ * mixfix)) list -> T -> T
wenzelm@19369
    20
  val extern_term: T -> term -> term
wenzelm@18997
    21
end;
wenzelm@18997
    22
wenzelm@19016
    23
structure LocalSyntax: LOCAL_SYNTAX =
wenzelm@18997
    24
struct
wenzelm@18997
    25
wenzelm@18997
    26
(* datatype T *)
wenzelm@18997
    27
wenzelm@19386
    28
type local_mixfix =
wenzelm@19386
    29
  ((string * bool) * string list list) *          (*name, fixed?, mixfix content*)
wenzelm@19541
    30
  ((string * bool) * (string * typ * mixfix));    (*mode, mixfix syntax*)
wenzelm@19386
    31
wenzelm@18997
    32
datatype T = Syntax of
wenzelm@18997
    33
 {thy_syntax: Syntax.syntax,
wenzelm@18997
    34
  local_syntax: Syntax.syntax,
wenzelm@19541
    35
  mode: string * bool,
wenzelm@19386
    36
  mixfixes: local_mixfix list,
wenzelm@19369
    37
  idents: string list * string list};
wenzelm@18997
    38
wenzelm@19541
    39
fun make_syntax (thy_syntax, local_syntax, mode, mixfixes, idents) =
wenzelm@18997
    40
  Syntax {thy_syntax = thy_syntax, local_syntax = local_syntax,
wenzelm@19541
    41
    mode = mode, mixfixes = mixfixes, idents = idents};
wenzelm@18997
    42
wenzelm@19541
    43
fun map_syntax f (Syntax {thy_syntax, local_syntax, mode, mixfixes, idents}) =
wenzelm@19541
    44
  make_syntax (f (thy_syntax, local_syntax, mode, mixfixes, idents));
wenzelm@18997
    45
wenzelm@19369
    46
fun is_consistent thy (Syntax {thy_syntax, ...}) =
wenzelm@18997
    47
  Syntax.eq_syntax (Sign.syn_of thy, thy_syntax);
wenzelm@18997
    48
wenzelm@18997
    49
fun syn_of (Syntax {local_syntax, ...}) = local_syntax;
wenzelm@18997
    50
fun idents_of (Syntax {idents, ...}) = idents;
wenzelm@18997
    51
val structs_of = #1 o idents_of;
wenzelm@18997
    52
wenzelm@18997
    53
wenzelm@18997
    54
(* build syntax *)
wenzelm@18997
    55
wenzelm@19541
    56
fun build_syntax thy mode mixfixes (idents as (structs, _)) =
wenzelm@18997
    57
  let
wenzelm@18997
    58
    val thy_syntax = Sign.syn_of thy;
wenzelm@18997
    59
    val is_logtype = Sign.is_logtype thy;
wenzelm@18997
    60
    val (atrs, trs, trs', atrs') = Syntax.struct_trfuns structs;
wenzelm@18997
    61
    val local_syntax = thy_syntax
wenzelm@18997
    62
      |> Syntax.extend_trfuns
wenzelm@19386
    63
          (map Syntax.mk_trfun atrs, map Syntax.mk_trfun trs,
wenzelm@19386
    64
           map Syntax.mk_trfun trs', map Syntax.mk_trfun atrs')
wenzelm@19386
    65
      |> fold (uncurry (Syntax.extend_const_gram is_logtype))
haftmann@19454
    66
          (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@19541
    69
fun init thy = build_syntax thy Syntax.default_mode [] ([], []);
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@19541
    76
(* syntax mode *)
wenzelm@19541
    77
wenzelm@19541
    78
fun set_mode mode = map_syntax (fn (thy_syntax, local_syntax, _, mixfixes, idents) =>
wenzelm@19541
    79
  (thy_syntax, local_syntax, mode, mixfixes, idents));
wenzelm@19541
    80
wenzelm@19541
    81
fun restore_mode (Syntax {mode, ...}) = set_mode mode;
wenzelm@18997
    82
wenzelm@18997
    83
wenzelm@18997
    84
(* mixfix declarations *)
wenzelm@18997
    85
wenzelm@18997
    86
local
wenzelm@18997
    87
wenzelm@19016
    88
fun mixfix_nosyn (_, (_, _, mx)) = mx = NoSyn;
wenzelm@19016
    89
fun mixfix_struct (_, (_, _, mx)) = mx = Structure;
wenzelm@19016
    90
wenzelm@19386
    91
fun mixfix_conflict ((content1: string list list, inout1), ((_, content2), ((_, inout2), _))) =
wenzelm@19386
    92
  inout1 andalso inout2 andalso exists (fn x => exists (fn y => x = y) content2) content1;
wenzelm@18997
    93
wenzelm@19386
    94
fun add_mixfix (mode, inout) (fixed, (x, T, mx)) =
wenzelm@19016
    95
  let
wenzelm@19016
    96
    val content = Syntax.mixfix_content mx;
wenzelm@19369
    97
    val c = if fixed then Syntax.fixedN ^ x else x;
wenzelm@19386
    98
  in
wenzelm@19386
    99
    remove mixfix_conflict (content, inout) #>
wenzelm@19386
   100
    cons (((x, fixed), content), ((mode, inout), (c, T, mx)))
wenzelm@19386
   101
  end;
wenzelm@19016
   102
wenzelm@19016
   103
fun prep_struct (fixed, (c, _, Structure)) =
wenzelm@19016
   104
      if fixed then SOME c
wenzelm@19016
   105
      else error ("Bad mixfix declaration for const: " ^ quote c)
wenzelm@19016
   106
  | prep_struct _ = NONE;
wenzelm@18997
   107
wenzelm@18997
   108
in
wenzelm@18997
   109
wenzelm@19541
   110
fun add_syntax thy raw_decls (syntax as (Syntax {mode, mixfixes, idents = (structs, _), ...})) =
wenzelm@19016
   111
  (case filter_out mixfix_nosyn raw_decls of
wenzelm@19016
   112
    [] => syntax
wenzelm@19016
   113
  | decls =>
wenzelm@19016
   114
      let
wenzelm@19541
   115
        val mixfixes' = mixfixes |> fold (add_mixfix mode) (filter_out mixfix_struct decls);
wenzelm@19016
   116
        val fixes' = fold (fn (((x, true), _), _) => cons x | _ => I) mixfixes' [];
wenzelm@19482
   117
        val structs' = structs @ map_filter prep_struct decls;
wenzelm@19541
   118
      in build_syntax thy mode mixfixes' (structs', fixes') end);
wenzelm@18997
   119
wenzelm@18997
   120
end;
wenzelm@18997
   121
wenzelm@18997
   122
wenzelm@18997
   123
(* extern_term *)
wenzelm@18997
   124
wenzelm@19369
   125
fun extern_term syntax =
wenzelm@18997
   126
  let
wenzelm@19369
   127
    val (structs, fixes) = idents_of syntax;
wenzelm@18997
   128
    fun map_free (t as Free (x, T)) =
wenzelm@18997
   129
          let val i = Library.find_index_eq x structs + 1 in
wenzelm@18997
   130
            if i = 0 andalso member (op =) fixes x then
wenzelm@18997
   131
              Const (Syntax.fixedN ^ x, T)
wenzelm@18997
   132
            else if i = 1 andalso not (! show_structs) then
wenzelm@18997
   133
              Syntax.const "_struct" $ Syntax.const "_indexdefault"
wenzelm@18997
   134
            else t
wenzelm@18997
   135
          end
wenzelm@18997
   136
      | map_free t = t;
wenzelm@19369
   137
  in Term.map_aterms map_free end;
wenzelm@18997
   138
wenzelm@18997
   139
end;