src/Pure/Isar/local_syntax.ML
author wenzelm
Sat, 11 Feb 2006 17:17:51 +0100
changeset 19016 f26377a4605a
parent 18997 3229c88bbbdf
child 19369 a4374b41c9bf
permissions -rw-r--r--
tuned mixfixes, mixfix_conflict;
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
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    17
  val add_syntax: theory -> (bool * (string * typ * mixfix)) list -> T -> T
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    18
  val extern_term: (string -> xstring) -> theory -> T -> term -> term
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    19
end;
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    20
19016
f26377a4605a tuned mixfixes, mixfix_conflict;
wenzelm
parents: 18997
diff changeset
    21
structure LocalSyntax: LOCAL_SYNTAX =
18997
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    22
struct
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    23
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    24
(* datatype T *)
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    25
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    26
datatype T = Syntax of
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    27
 {thy_syntax: Syntax.syntax,
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    28
  local_syntax: Syntax.syntax,
19016
f26377a4605a tuned mixfixes, mixfix_conflict;
wenzelm
parents: 18997
diff changeset
    29
  mixfixes: (((string * bool) * string list list) * (string * typ * mixfix)) list,
18997
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    30
  idents: string list * string list * string list};
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    31
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    32
fun make_syntax (thy_syntax, local_syntax, mixfixes, idents) =
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    33
  Syntax {thy_syntax = thy_syntax, local_syntax = local_syntax,
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    34
    mixfixes = mixfixes, idents = idents};
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    35
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    36
fun map_syntax f (Syntax {thy_syntax, local_syntax, mixfixes, idents}) =
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    37
  make_syntax (f (thy_syntax, local_syntax, mixfixes, idents));
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    38
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    39
fun is_consistent thy (syntax as Syntax {thy_syntax, ...}) =
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    40
  Syntax.eq_syntax (Sign.syn_of thy, thy_syntax);
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    41
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    42
fun syn_of (Syntax {local_syntax, ...}) = local_syntax;
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    43
fun idents_of (Syntax {idents, ...}) = idents;
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    44
val structs_of = #1 o idents_of;
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    45
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    46
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    47
(* build syntax *)
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    48
19016
f26377a4605a tuned mixfixes, mixfix_conflict;
wenzelm
parents: 18997
diff changeset
    49
fun build_syntax thy (mixfixes, idents as (structs, _, _)) =
18997
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    50
  let
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    51
    val thy_syntax = Sign.syn_of thy;
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    52
    val is_logtype = Sign.is_logtype thy;
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    53
    val (atrs, trs, trs', atrs') = Syntax.struct_trfuns structs;
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    54
    val local_syntax = thy_syntax
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    55
      |> Syntax.extend_trfuns
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    56
         (map Syntax.mk_trfun atrs, map Syntax.mk_trfun trs,
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    57
          map Syntax.mk_trfun trs', map Syntax.mk_trfun atrs')
19016
f26377a4605a tuned mixfixes, mixfix_conflict;
wenzelm
parents: 18997
diff changeset
    58
      |> Syntax.extend_const_gram is_logtype ("", false)
f26377a4605a tuned mixfixes, mixfix_conflict;
wenzelm
parents: 18997
diff changeset
    59
         (map (fn (((x, _), _), (c, T, _)) => (c, T, Syntax.literal x)) mixfixes)
f26377a4605a tuned mixfixes, mixfix_conflict;
wenzelm
parents: 18997
diff changeset
    60
      |> Syntax.extend_const_gram is_logtype ("", true) (map snd mixfixes)
18997
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    61
  in make_syntax (thy_syntax, local_syntax, mixfixes, idents) end
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    62
19016
f26377a4605a tuned mixfixes, mixfix_conflict;
wenzelm
parents: 18997
diff changeset
    63
fun init thy = build_syntax thy ([], ([], [], []));
18997
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    64
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    65
fun rebuild thy (syntax as Syntax {mixfixes, idents, ...}) =
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    66
  if is_consistent thy syntax then syntax
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    67
  else build_syntax thy (mixfixes, idents);
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    68
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    69
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    70
(* mixfix declarations *)
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    71
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    72
local
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    73
19016
f26377a4605a tuned mixfixes, mixfix_conflict;
wenzelm
parents: 18997
diff changeset
    74
fun mixfix_nosyn (_, (_, _, mx)) = mx = NoSyn;
f26377a4605a tuned mixfixes, mixfix_conflict;
wenzelm
parents: 18997
diff changeset
    75
fun mixfix_struct (_, (_, _, mx)) = mx = Structure;
f26377a4605a tuned mixfixes, mixfix_conflict;
wenzelm
parents: 18997
diff changeset
    76
f26377a4605a tuned mixfixes, mixfix_conflict;
wenzelm
parents: 18997
diff changeset
    77
fun mixfix_conflict (content1: string list list, ((_, content2), _)) =
f26377a4605a tuned mixfixes, mixfix_conflict;
wenzelm
parents: 18997
diff changeset
    78
  exists (fn x => exists (fn y => x = y) content2) content1;
18997
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    79
19016
f26377a4605a tuned mixfixes, mixfix_conflict;
wenzelm
parents: 18997
diff changeset
    80
fun add_mixfix (fixed, (x, T, mx)) =
f26377a4605a tuned mixfixes, mixfix_conflict;
wenzelm
parents: 18997
diff changeset
    81
  let
f26377a4605a tuned mixfixes, mixfix_conflict;
wenzelm
parents: 18997
diff changeset
    82
    val content = Syntax.mixfix_content mx;
f26377a4605a tuned mixfixes, mixfix_conflict;
wenzelm
parents: 18997
diff changeset
    83
    val c = if fixed then Syntax.fixedN ^ x else Syntax.constN ^ x;
f26377a4605a tuned mixfixes, mixfix_conflict;
wenzelm
parents: 18997
diff changeset
    84
  in remove mixfix_conflict content #> cons (((x, fixed), content), (c, T, mx)) end;
f26377a4605a tuned mixfixes, mixfix_conflict;
wenzelm
parents: 18997
diff changeset
    85
f26377a4605a tuned mixfixes, mixfix_conflict;
wenzelm
parents: 18997
diff changeset
    86
fun prep_struct (fixed, (c, _, Structure)) =
f26377a4605a tuned mixfixes, mixfix_conflict;
wenzelm
parents: 18997
diff changeset
    87
      if fixed then SOME c
f26377a4605a tuned mixfixes, mixfix_conflict;
wenzelm
parents: 18997
diff changeset
    88
      else error ("Bad mixfix declaration for const: " ^ quote c)
f26377a4605a tuned mixfixes, mixfix_conflict;
wenzelm
parents: 18997
diff changeset
    89
  | prep_struct _ = NONE;
18997
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    90
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    91
in
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    92
19016
f26377a4605a tuned mixfixes, mixfix_conflict;
wenzelm
parents: 18997
diff changeset
    93
fun add_syntax thy raw_decls (syntax as (Syntax {mixfixes, idents = (structs, _, _), ...})) =
f26377a4605a tuned mixfixes, mixfix_conflict;
wenzelm
parents: 18997
diff changeset
    94
  (case filter_out mixfix_nosyn raw_decls of
f26377a4605a tuned mixfixes, mixfix_conflict;
wenzelm
parents: 18997
diff changeset
    95
    [] => syntax
f26377a4605a tuned mixfixes, mixfix_conflict;
wenzelm
parents: 18997
diff changeset
    96
  | decls =>
f26377a4605a tuned mixfixes, mixfix_conflict;
wenzelm
parents: 18997
diff changeset
    97
      let
f26377a4605a tuned mixfixes, mixfix_conflict;
wenzelm
parents: 18997
diff changeset
    98
        val mixfixes' = mixfixes |> fold add_mixfix (filter_out mixfix_struct decls);
f26377a4605a tuned mixfixes, mixfix_conflict;
wenzelm
parents: 18997
diff changeset
    99
        val fixes' = fold (fn (((x, true), _), _) => cons x | _ => I) mixfixes' [];
f26377a4605a tuned mixfixes, mixfix_conflict;
wenzelm
parents: 18997
diff changeset
   100
        val consts' = fold (fn (((x, false), _), _) => cons x | _ => I) mixfixes' [];
f26377a4605a tuned mixfixes, mixfix_conflict;
wenzelm
parents: 18997
diff changeset
   101
        val structs' = structs @ List.mapPartial prep_struct decls;
f26377a4605a tuned mixfixes, mixfix_conflict;
wenzelm
parents: 18997
diff changeset
   102
      in build_syntax thy (mixfixes', (structs', fixes', consts')) end);
18997
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
   103
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
   104
end;
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
   105
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
   106
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
   107
(* extern_term *)
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
   108
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
   109
fun extern_term extern_const thy syntax =
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
   110
  let
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
   111
    val (structs, fixes, consts) = idents_of syntax;
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
   112
    fun map_const c =
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
   113
      if member (op =) consts c then Syntax.constN ^ c else extern_const c;
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
   114
    fun map_free (t as Free (x, T)) =
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
   115
          let val i = Library.find_index_eq x structs + 1 in
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
   116
            if i = 0 andalso member (op =) fixes x then
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
   117
              Const (Syntax.fixedN ^ x, T)
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
   118
            else if i = 1 andalso not (! show_structs) then
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
   119
              Syntax.const "_struct" $ Syntax.const "_indexdefault"
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
   120
            else t
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
   121
          end
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
   122
      | map_free t = t;
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
   123
  in Sign.extern_term map_const thy #> Term.map_aterms map_free end;
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
   124
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
   125
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
   126
end;