src/Pure/Isar/local_syntax.ML
author wenzelm
Tue, 16 May 2006 21:33:11 +0200
changeset 19660 e3ec6839c631
parent 19618 9050a3b01e62
child 20785 d60f81c56fd4
permissions -rw-r--r--
added add_modesyntax; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
18997
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Isar/local_syntax.ML
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
     3
    Author:     Makarius
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
     4
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
     5
Local syntax depending on theory syntax.
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
     6
*)
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
     7
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
     8
val show_structs = ref false;
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
     9
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    10
signature LOCAL_SYNTAX =
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    11
sig
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    12
  type T
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    13
  val syn_of: T -> Syntax.syntax
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    14
  val structs_of: T -> string list
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    15
  val init: theory -> T
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    16
  val rebuild: theory -> T -> T
19660
e3ec6839c631 added add_modesyntax;
wenzelm
parents: 19618
diff changeset
    17
  val add_syntax: theory -> (bool * (string * typ * mixfix)) list -> T -> T
19541
1bb8e26a26ee maintain implicit syntax mode;
wenzelm
parents: 19482
diff changeset
    18
  val set_mode: string * bool -> T -> T
1bb8e26a26ee maintain implicit syntax mode;
wenzelm
parents: 19482
diff changeset
    19
  val restore_mode: T -> T -> T
19660
e3ec6839c631 added add_modesyntax;
wenzelm
parents: 19618
diff changeset
    20
  val add_modesyntax: theory -> string * bool -> (bool * (string * typ * mixfix)) list -> T -> T
19369
a4374b41c9bf simplified handling of authentic syntax (cf. early externing in consts.ML);
wenzelm
parents: 19016
diff changeset
    21
  val extern_term: T -> term -> term
18997
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    22
end;
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    23
19016
f26377a4605a tuned mixfixes, mixfix_conflict;
wenzelm
parents: 18997
diff changeset
    24
structure LocalSyntax: LOCAL_SYNTAX =
18997
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    25
struct
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    26
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    27
(* datatype T *)
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    28
19386
38d83ffd6217 add_syntax: actually observe print mode;
wenzelm
parents: 19369
diff changeset
    29
type local_mixfix =
38d83ffd6217 add_syntax: actually observe print mode;
wenzelm
parents: 19369
diff changeset
    30
  ((string * bool) * string list list) *          (*name, fixed?, mixfix content*)
19541
1bb8e26a26ee maintain implicit syntax mode;
wenzelm
parents: 19482
diff changeset
    31
  ((string * bool) * (string * typ * mixfix));    (*mode, mixfix syntax*)
19386
38d83ffd6217 add_syntax: actually observe print mode;
wenzelm
parents: 19369
diff changeset
    32
18997
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    33
datatype T = Syntax of
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    34
 {thy_syntax: Syntax.syntax,
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    35
  local_syntax: Syntax.syntax,
19541
1bb8e26a26ee maintain implicit syntax mode;
wenzelm
parents: 19482
diff changeset
    36
  mode: string * bool,
19386
38d83ffd6217 add_syntax: actually observe print mode;
wenzelm
parents: 19369
diff changeset
    37
  mixfixes: local_mixfix list,
19369
a4374b41c9bf simplified handling of authentic syntax (cf. early externing in consts.ML);
wenzelm
parents: 19016
diff changeset
    38
  idents: string list * string list};
18997
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    39
19541
1bb8e26a26ee maintain implicit syntax mode;
wenzelm
parents: 19482
diff changeset
    40
fun make_syntax (thy_syntax, local_syntax, mode, mixfixes, idents) =
18997
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    41
  Syntax {thy_syntax = thy_syntax, local_syntax = local_syntax,
19541
1bb8e26a26ee maintain implicit syntax mode;
wenzelm
parents: 19482
diff changeset
    42
    mode = mode, mixfixes = mixfixes, idents = idents};
18997
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    43
19541
1bb8e26a26ee maintain implicit syntax mode;
wenzelm
parents: 19482
diff changeset
    44
fun map_syntax f (Syntax {thy_syntax, local_syntax, mode, mixfixes, idents}) =
1bb8e26a26ee maintain implicit syntax mode;
wenzelm
parents: 19482
diff changeset
    45
  make_syntax (f (thy_syntax, local_syntax, mode, mixfixes, idents));
18997
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    46
19369
a4374b41c9bf simplified handling of authentic syntax (cf. early externing in consts.ML);
wenzelm
parents: 19016
diff changeset
    47
fun is_consistent thy (Syntax {thy_syntax, ...}) =
18997
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    48
  Syntax.eq_syntax (Sign.syn_of thy, thy_syntax);
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    49
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    50
fun syn_of (Syntax {local_syntax, ...}) = local_syntax;
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    51
fun idents_of (Syntax {idents, ...}) = idents;
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    52
val structs_of = #1 o idents_of;
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    53
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    54
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    55
(* build syntax *)
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    56
19541
1bb8e26a26ee maintain implicit syntax mode;
wenzelm
parents: 19482
diff changeset
    57
fun build_syntax thy mode mixfixes (idents as (structs, _)) =
18997
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    58
  let
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    59
    val thy_syntax = Sign.syn_of thy;
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    60
    val is_logtype = Sign.is_logtype thy;
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    61
    val (atrs, trs, trs', atrs') = Syntax.struct_trfuns structs;
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    62
    val local_syntax = thy_syntax
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    63
      |> Syntax.extend_trfuns
19386
38d83ffd6217 add_syntax: actually observe print mode;
wenzelm
parents: 19369
diff changeset
    64
          (map Syntax.mk_trfun atrs, map Syntax.mk_trfun trs,
38d83ffd6217 add_syntax: actually observe print mode;
wenzelm
parents: 19369
diff changeset
    65
           map Syntax.mk_trfun trs', map Syntax.mk_trfun atrs')
38d83ffd6217 add_syntax: actually observe print mode;
wenzelm
parents: 19369
diff changeset
    66
      |> fold (uncurry (Syntax.extend_const_gram is_logtype))
19454
46a7e133f802 moved coalesce to AList, added equality predicates to library
haftmann
parents: 19386
diff changeset
    67
          (AList.coalesce (op =) (rev (map snd mixfixes)));
19541
1bb8e26a26ee maintain implicit syntax mode;
wenzelm
parents: 19482
diff changeset
    68
  in make_syntax (thy_syntax, local_syntax, mode, mixfixes, idents) end;
1bb8e26a26ee maintain implicit syntax mode;
wenzelm
parents: 19482
diff changeset
    69
1bb8e26a26ee maintain implicit syntax mode;
wenzelm
parents: 19482
diff changeset
    70
fun init thy = build_syntax thy Syntax.default_mode [] ([], []);
18997
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    71
19541
1bb8e26a26ee maintain implicit syntax mode;
wenzelm
parents: 19482
diff changeset
    72
fun rebuild thy (syntax as Syntax {mode, mixfixes, idents, ...}) =
1bb8e26a26ee maintain implicit syntax mode;
wenzelm
parents: 19482
diff changeset
    73
  if is_consistent thy syntax then syntax
1bb8e26a26ee maintain implicit syntax mode;
wenzelm
parents: 19482
diff changeset
    74
  else build_syntax thy mode mixfixes idents;
18997
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    75
19541
1bb8e26a26ee maintain implicit syntax mode;
wenzelm
parents: 19482
diff changeset
    76
18997
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    77
(* mixfix declarations *)
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    78
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    79
local
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    80
19016
f26377a4605a tuned mixfixes, mixfix_conflict;
wenzelm
parents: 18997
diff changeset
    81
fun mixfix_nosyn (_, (_, _, mx)) = mx = NoSyn;
f26377a4605a tuned mixfixes, mixfix_conflict;
wenzelm
parents: 18997
diff changeset
    82
fun mixfix_struct (_, (_, _, mx)) = mx = Structure;
f26377a4605a tuned mixfixes, mixfix_conflict;
wenzelm
parents: 18997
diff changeset
    83
19386
38d83ffd6217 add_syntax: actually observe print mode;
wenzelm
parents: 19369
diff changeset
    84
fun mixfix_conflict ((content1: string list list, inout1), ((_, content2), ((_, inout2), _))) =
38d83ffd6217 add_syntax: actually observe print mode;
wenzelm
parents: 19369
diff changeset
    85
  inout1 andalso inout2 andalso exists (fn x => exists (fn y => x = y) content2) content1;
18997
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    86
19386
38d83ffd6217 add_syntax: actually observe print mode;
wenzelm
parents: 19369
diff changeset
    87
fun add_mixfix (mode, inout) (fixed, (x, T, mx)) =
19016
f26377a4605a tuned mixfixes, mixfix_conflict;
wenzelm
parents: 18997
diff changeset
    88
  let
f26377a4605a tuned mixfixes, mixfix_conflict;
wenzelm
parents: 18997
diff changeset
    89
    val content = Syntax.mixfix_content mx;
19369
a4374b41c9bf simplified handling of authentic syntax (cf. early externing in consts.ML);
wenzelm
parents: 19016
diff changeset
    90
    val c = if fixed then Syntax.fixedN ^ x else x;
19386
38d83ffd6217 add_syntax: actually observe print mode;
wenzelm
parents: 19369
diff changeset
    91
  in
38d83ffd6217 add_syntax: actually observe print mode;
wenzelm
parents: 19369
diff changeset
    92
    remove mixfix_conflict (content, inout) #>
38d83ffd6217 add_syntax: actually observe print mode;
wenzelm
parents: 19369
diff changeset
    93
    cons (((x, fixed), content), ((mode, inout), (c, T, mx)))
38d83ffd6217 add_syntax: actually observe print mode;
wenzelm
parents: 19369
diff changeset
    94
  end;
19016
f26377a4605a tuned mixfixes, mixfix_conflict;
wenzelm
parents: 18997
diff changeset
    95
f26377a4605a tuned mixfixes, mixfix_conflict;
wenzelm
parents: 18997
diff changeset
    96
fun prep_struct (fixed, (c, _, Structure)) =
f26377a4605a tuned mixfixes, mixfix_conflict;
wenzelm
parents: 18997
diff changeset
    97
      if fixed then SOME c
f26377a4605a tuned mixfixes, mixfix_conflict;
wenzelm
parents: 18997
diff changeset
    98
      else error ("Bad mixfix declaration for const: " ^ quote c)
f26377a4605a tuned mixfixes, mixfix_conflict;
wenzelm
parents: 18997
diff changeset
    99
  | prep_struct _ = NONE;
18997
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
   100
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
   101
in
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
   102
19541
1bb8e26a26ee maintain implicit syntax mode;
wenzelm
parents: 19482
diff changeset
   103
fun add_syntax thy raw_decls (syntax as (Syntax {mode, mixfixes, idents = (structs, _), ...})) =
19016
f26377a4605a tuned mixfixes, mixfix_conflict;
wenzelm
parents: 18997
diff changeset
   104
  (case filter_out mixfix_nosyn raw_decls of
f26377a4605a tuned mixfixes, mixfix_conflict;
wenzelm
parents: 18997
diff changeset
   105
    [] => syntax
f26377a4605a tuned mixfixes, mixfix_conflict;
wenzelm
parents: 18997
diff changeset
   106
  | decls =>
f26377a4605a tuned mixfixes, mixfix_conflict;
wenzelm
parents: 18997
diff changeset
   107
      let
19541
1bb8e26a26ee maintain implicit syntax mode;
wenzelm
parents: 19482
diff changeset
   108
        val mixfixes' = mixfixes |> fold (add_mixfix mode) (filter_out mixfix_struct decls);
19016
f26377a4605a tuned mixfixes, mixfix_conflict;
wenzelm
parents: 18997
diff changeset
   109
        val fixes' = fold (fn (((x, true), _), _) => cons x | _ => I) mixfixes' [];
19482
9f11af8f7ef9 tuned basic list operators (flat, maps, map_filter);
wenzelm
parents: 19454
diff changeset
   110
        val structs' = structs @ map_filter prep_struct decls;
19541
1bb8e26a26ee maintain implicit syntax mode;
wenzelm
parents: 19482
diff changeset
   111
      in build_syntax thy mode mixfixes' (structs', fixes') end);
18997
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
   112
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
   113
end;
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
   114
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
   115
19660
e3ec6839c631 added add_modesyntax;
wenzelm
parents: 19618
diff changeset
   116
(* syntax mode *)
e3ec6839c631 added add_modesyntax;
wenzelm
parents: 19618
diff changeset
   117
e3ec6839c631 added add_modesyntax;
wenzelm
parents: 19618
diff changeset
   118
fun set_mode mode = map_syntax (fn (thy_syntax, local_syntax, _, mixfixes, idents) =>
e3ec6839c631 added add_modesyntax;
wenzelm
parents: 19618
diff changeset
   119
  (thy_syntax, local_syntax, mode, mixfixes, idents));
e3ec6839c631 added add_modesyntax;
wenzelm
parents: 19618
diff changeset
   120
e3ec6839c631 added add_modesyntax;
wenzelm
parents: 19618
diff changeset
   121
fun restore_mode (Syntax {mode, ...}) = set_mode mode;
e3ec6839c631 added add_modesyntax;
wenzelm
parents: 19618
diff changeset
   122
e3ec6839c631 added add_modesyntax;
wenzelm
parents: 19618
diff changeset
   123
fun add_modesyntax thy mode args syntax =
e3ec6839c631 added add_modesyntax;
wenzelm
parents: 19618
diff changeset
   124
  syntax |> set_mode mode |> add_syntax thy args |> restore_mode syntax;
e3ec6839c631 added add_modesyntax;
wenzelm
parents: 19618
diff changeset
   125
e3ec6839c631 added add_modesyntax;
wenzelm
parents: 19618
diff changeset
   126
18997
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
   127
(* extern_term *)
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
   128
19369
a4374b41c9bf simplified handling of authentic syntax (cf. early externing in consts.ML);
wenzelm
parents: 19016
diff changeset
   129
fun extern_term syntax =
18997
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
   130
  let
19369
a4374b41c9bf simplified handling of authentic syntax (cf. early externing in consts.ML);
wenzelm
parents: 19016
diff changeset
   131
    val (structs, fixes) = idents_of syntax;
18997
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
   132
    fun map_free (t as Free (x, T)) =
19618
wenzelm
parents: 19541
diff changeset
   133
          let val i = find_index (fn s => s = x) structs + 1 in
18997
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
   134
            if i = 0 andalso member (op =) fixes x then
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
   135
              Const (Syntax.fixedN ^ x, T)
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
   136
            else if i = 1 andalso not (! show_structs) then
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
   137
              Syntax.const "_struct" $ Syntax.const "_indexdefault"
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
   138
            else t
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
   139
          end
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
   140
      | map_free t = t;
19369
a4374b41c9bf simplified handling of authentic syntax (cf. early externing in consts.ML);
wenzelm
parents: 19016
diff changeset
   141
  in Term.map_aterms map_free end;
18997
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
   142
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
   143
end;