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