src/Pure/Isar/local_syntax.ML
author wenzelm
Mon May 03 14:25:56 2010 +0200 (2010-05-03)
changeset 36610 bafd82950e24
parent 35429 afa8cf9e63d8
permissions -rw-r--r--
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
     1 (*  Title:      Pure/Isar/local_syntax.ML
     2     Author:     Makarius
     3 
     4 Local syntax depending on theory syntax.
     5 *)
     6 
     7 signature LOCAL_SYNTAX =
     8 sig
     9   type T
    10   val syn_of: T -> Syntax.syntax
    11   val idents_of: T -> {structs: string list, fixes: string list}
    12   val init: theory -> T
    13   val rebuild: theory -> T -> T
    14   datatype kind = Type | Const | Fixed
    15   val add_syntax: theory -> (kind * (string * typ * mixfix)) list -> T -> T
    16   val set_mode: Syntax.mode -> T -> T
    17   val restore_mode: T -> T -> T
    18   val update_modesyntax: theory -> bool -> Syntax.mode ->
    19     (kind * (string * typ * mixfix)) list -> T -> T
    20 end;
    21 
    22 structure Local_Syntax: LOCAL_SYNTAX =
    23 struct
    24 
    25 (* datatype T *)
    26 
    27 type local_mixfix =
    28   (string * bool) *  (*name, fixed?*)
    29   ((bool * bool * Syntax.mode) * (string * typ * mixfix));  (*type?, add?, mode, declaration*)
    30 
    31 datatype T = Syntax of
    32  {thy_syntax: Syntax.syntax,
    33   local_syntax: Syntax.syntax,
    34   mode: Syntax.mode,
    35   mixfixes: local_mixfix list,
    36   idents: string list * string list};
    37 
    38 fun make_syntax (thy_syntax, local_syntax, mode, mixfixes, idents) =
    39   Syntax {thy_syntax = thy_syntax, local_syntax = local_syntax,
    40     mode = mode, mixfixes = mixfixes, idents = idents};
    41 
    42 fun map_syntax f (Syntax {thy_syntax, local_syntax, mode, mixfixes, idents}) =
    43   make_syntax (f (thy_syntax, local_syntax, mode, mixfixes, idents));
    44 
    45 fun is_consistent thy (Syntax {thy_syntax, ...}) =
    46   Syntax.eq_syntax (Sign.syn_of thy, thy_syntax);
    47 
    48 fun syn_of (Syntax {local_syntax, ...}) = local_syntax;
    49 fun idents_of (Syntax {idents = (structs, fixes), ...}) = {structs = structs, fixes = fixes};
    50 
    51 
    52 (* build syntax *)
    53 
    54 fun build_syntax thy mode mixfixes (idents as (structs, _)) =
    55   let
    56     val thy_syntax = Sign.syn_of thy;
    57     fun update_gram ((true, add, m), decls) = Syntax.update_type_gram add m decls
    58       | update_gram ((false, add, m), decls) =
    59           Syntax.update_const_gram add (Sign.is_logtype thy) m decls;
    60 
    61     val (atrs, trs, trs', atrs') = Syntax.struct_trfuns structs;
    62     val local_syntax = thy_syntax
    63       |> Syntax.update_trfuns
    64           (map Syntax.mk_trfun atrs, map Syntax.mk_trfun trs,
    65            map Syntax.mk_trfun trs', map Syntax.mk_trfun atrs')
    66       |> fold update_gram (AList.coalesce (op =) (rev (map snd mixfixes)));
    67   in make_syntax (thy_syntax, local_syntax, mode, mixfixes, idents) end;
    68 
    69 fun init thy = build_syntax thy Syntax.mode_default [] ([], []);
    70 
    71 fun rebuild thy (syntax as Syntax {mode, mixfixes, idents, ...}) =
    72   if is_consistent thy syntax then syntax
    73   else build_syntax thy mode mixfixes idents;
    74 
    75 
    76 (* mixfix declarations *)
    77 
    78 datatype kind = Type | Const | Fixed;
    79 
    80 local
    81 
    82 fun prep_mixfix _ _ (_, (_, _, Structure)) = NONE
    83   | prep_mixfix add mode (Type, decl as (x, _, _)) = SOME ((x, false), ((true, add, mode), decl))
    84   | prep_mixfix add mode (Const, decl as (x, _, _)) = SOME ((x, false), ((false, add, mode), decl))
    85   | prep_mixfix add mode (Fixed, (x, T, mx)) =
    86       SOME ((x, true), ((false, add, mode), (Syntax.mark_fixed x, T, mx)));
    87 
    88 fun prep_struct (Fixed, (c, _, Structure)) = SOME c
    89   | prep_struct (_, (c, _, Structure)) = error ("Bad mixfix declaration for " ^ quote c)
    90   | prep_struct _ = NONE;
    91 
    92 in
    93 
    94 fun update_syntax add thy raw_decls
    95     (syntax as (Syntax {mode, mixfixes, idents = (structs, _), ...})) =
    96   (case filter_out (fn (_, (_, _, mx)) => mx = NoSyn) raw_decls of
    97     [] => syntax
    98   | decls =>
    99       let
   100         val new_mixfixes = map_filter (prep_mixfix add mode) decls;
   101         val new_structs = map_filter prep_struct decls;
   102         val mixfixes' = rev new_mixfixes @ mixfixes;
   103         val structs' =
   104           if add then structs @ new_structs
   105           else subtract (op =) new_structs structs;
   106         val fixes' = fold (fn ((x, true), _) => cons x | _ => I) mixfixes' [];
   107       in build_syntax thy mode mixfixes' (structs', fixes') end);
   108 
   109 val add_syntax = update_syntax true;
   110 
   111 end;
   112 
   113 
   114 (* syntax mode *)
   115 
   116 fun set_mode mode = map_syntax (fn (thy_syntax, local_syntax, _, mixfixes, idents) =>
   117   (thy_syntax, local_syntax, mode, mixfixes, idents));
   118 
   119 fun restore_mode (Syntax {mode, ...}) = set_mode mode;
   120 
   121 fun update_modesyntax thy add mode args syntax =
   122   syntax |> set_mode mode |> update_syntax add thy args |> restore_mode syntax;
   123 
   124 end;