src/Pure/Isar/local_syntax.ML
author wenzelm
Mon Mar 01 17:07:36 2010 +0100 (2010-03-01)
changeset 35412 b8dead547d9e
parent 33387 acea2f336721
child 35429 afa8cf9e63d8
permissions -rw-r--r--
more uniform treatment of syntax for types vs. consts;
     1 (*  Title:      Pure/Isar/local_syntax.ML
     2     Author:     Makarius
     3 
     4 Local syntax depending on theory syntax.
     5 *)
     6 
     7 val show_structs = Unsynchronized.ref false;
     8 
     9 signature LOCAL_SYNTAX =
    10 sig
    11   type T
    12   val syn_of: T -> Syntax.syntax
    13   val structs_of: T -> string list
    14   val init: theory -> T
    15   val rebuild: theory -> T -> T
    16   datatype kind = Type | Const | Fixed
    17   val add_syntax: theory -> (kind * (string * typ * mixfix)) list -> T -> T
    18   val set_mode: Syntax.mode -> T -> T
    19   val restore_mode: T -> T -> T
    20   val update_modesyntax: theory -> bool -> Syntax.mode ->
    21     (kind * (string * typ * mixfix)) list -> T -> T
    22   val extern_term: T -> term -> term
    23 end;
    24 
    25 structure Local_Syntax: LOCAL_SYNTAX =
    26 struct
    27 
    28 (* datatype T *)
    29 
    30 type local_mixfix =
    31   (string * bool) *  (*name, fixed?*)
    32   ((bool * bool * Syntax.mode) * (string * typ * mixfix));  (*type?, add?, mode, declaration*)
    33 
    34 datatype T = Syntax of
    35  {thy_syntax: Syntax.syntax,
    36   local_syntax: Syntax.syntax,
    37   mode: Syntax.mode,
    38   mixfixes: local_mixfix list,
    39   idents: string list * string list};
    40 
    41 fun make_syntax (thy_syntax, local_syntax, mode, mixfixes, idents) =
    42   Syntax {thy_syntax = thy_syntax, local_syntax = local_syntax,
    43     mode = mode, mixfixes = mixfixes, idents = idents};
    44 
    45 fun map_syntax f (Syntax {thy_syntax, local_syntax, mode, mixfixes, idents}) =
    46   make_syntax (f (thy_syntax, local_syntax, mode, mixfixes, idents));
    47 
    48 fun is_consistent thy (Syntax {thy_syntax, ...}) =
    49   Syntax.eq_syntax (Sign.syn_of thy, thy_syntax);
    50 
    51 fun syn_of (Syntax {local_syntax, ...}) = local_syntax;
    52 fun idents_of (Syntax {idents, ...}) = idents;
    53 val structs_of = #1 o idents_of;
    54 
    55 
    56 (* build syntax *)
    57 
    58 fun build_syntax thy mode mixfixes (idents as (structs, _)) =
    59   let
    60     val thy_syntax = Sign.syn_of thy;
    61     fun update_gram ((true, add, m), decls) = Syntax.update_type_gram add m decls
    62       | update_gram ((false, add, m), decls) =
    63           Syntax.update_const_gram add (Sign.is_logtype thy) m decls;
    64 
    65     val (atrs, trs, trs', atrs') = Syntax.struct_trfuns structs;
    66     val local_syntax = thy_syntax
    67       |> Syntax.update_trfuns
    68           (map Syntax.mk_trfun atrs, map Syntax.mk_trfun trs,
    69            map Syntax.mk_trfun trs', map Syntax.mk_trfun atrs')
    70       |> fold update_gram (AList.coalesce (op =) (rev (map snd mixfixes)));
    71   in make_syntax (thy_syntax, local_syntax, mode, mixfixes, idents) end;
    72 
    73 fun init thy = build_syntax thy Syntax.mode_default [] ([], []);
    74 
    75 fun rebuild thy (syntax as Syntax {mode, mixfixes, idents, ...}) =
    76   if is_consistent thy syntax then syntax
    77   else build_syntax thy mode mixfixes idents;
    78 
    79 
    80 (* mixfix declarations *)
    81 
    82 datatype kind = Type | Const | Fixed;
    83 
    84 local
    85 
    86 fun prep_mixfix _ _ (_, (_, _, Structure)) = NONE
    87   | prep_mixfix add mode (Type, decl as (x, _, _)) = SOME ((x, false), ((true, add, mode), decl))
    88   | prep_mixfix add mode (Const, decl as (x, _, _)) = SOME ((x, false), ((false, add, mode), decl))
    89   | prep_mixfix add mode (Fixed, (x, T, mx)) =
    90       SOME ((x, true), ((false, add, mode), (Syntax.mark_fixed x, T, mx)));
    91 
    92 fun prep_struct (Fixed, (c, _, Structure)) = SOME c
    93   | prep_struct (_, (c, _, Structure)) = error ("Bad mixfix declaration for " ^ quote c)
    94   | prep_struct _ = NONE;
    95 
    96 in
    97 
    98 fun update_syntax add thy raw_decls
    99     (syntax as (Syntax {mode, mixfixes, idents = (structs, _), ...})) =
   100   (case filter_out (fn (_, (_, _, mx)) => mx = NoSyn) raw_decls of
   101     [] => syntax
   102   | decls =>
   103       let
   104         val new_mixfixes = map_filter (prep_mixfix add mode) decls;
   105         val new_structs = map_filter prep_struct decls;
   106         val mixfixes' = rev new_mixfixes @ mixfixes;
   107         val structs' =
   108           if add then structs @ new_structs
   109           else subtract (op =) new_structs structs;
   110         val fixes' = fold (fn ((x, true), _) => cons x | _ => I) mixfixes' [];
   111       in build_syntax thy mode mixfixes' (structs', fixes') end);
   112 
   113 val add_syntax = update_syntax true;
   114 
   115 end;
   116 
   117 
   118 (* syntax mode *)
   119 
   120 fun set_mode mode = map_syntax (fn (thy_syntax, local_syntax, _, mixfixes, idents) =>
   121   (thy_syntax, local_syntax, mode, mixfixes, idents));
   122 
   123 fun restore_mode (Syntax {mode, ...}) = set_mode mode;
   124 
   125 fun update_modesyntax thy add mode args syntax =
   126   syntax |> set_mode mode |> update_syntax add thy args |> restore_mode syntax;
   127 
   128 
   129 (* extern_term *)
   130 
   131 fun extern_term syntax =
   132   let
   133     val (structs, fixes) = idents_of syntax;
   134     fun map_free (t as Free (x, T)) =
   135           let val i = find_index (fn s => s = x) structs + 1 in
   136             if i = 0 andalso member (op =) fixes x then
   137               Term.Const (Syntax.mark_fixed x, T)
   138             else if i = 1 andalso not (! show_structs) then
   139               Syntax.const "_struct" $ Syntax.const "_indexdefault"
   140             else t
   141           end
   142       | map_free t = t;
   143   in Term.map_aterms map_free end;
   144 
   145 end;