src/Pure/Isar/local_syntax.ML
author wenzelm
Sun Mar 01 23:36:12 2009 +0100 (2009-03-01)
changeset 30190 479806475f3c
parent 29606 fedb8be05f24
child 32738 15bb09ca0378
permissions -rw-r--r--
use long names for old-style fold combinators;
     1 (*  Title:      Pure/Isar/local_syntax.ML
     2     Author:     Makarius
     3 
     4 Local syntax depending on theory syntax.
     5 *)
     6 
     7 val show_structs = 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   val add_syntax: theory -> (bool * (string * typ * mixfix)) list -> T -> T
    17   val set_mode: Syntax.mode -> T -> T
    18   val restore_mode: T -> T -> T
    19   val update_modesyntax: theory -> bool -> Syntax.mode ->
    20     (bool * (string * typ * mixfix)) list -> T -> T
    21   val extern_term: T -> term -> term
    22 end;
    23 
    24 structure LocalSyntax: LOCAL_SYNTAX =
    25 struct
    26 
    27 (* datatype T *)
    28 
    29 type local_mixfix =
    30   (string * bool) *                                    (*name, fixed?*)
    31   ((bool * Syntax.mode) * (string * typ * mixfix));    (*add?, mode, declaration*)
    32 
    33 datatype T = Syntax of
    34  {thy_syntax: Syntax.syntax,
    35   local_syntax: Syntax.syntax,
    36   mode: Syntax.mode,
    37   mixfixes: local_mixfix list,
    38   idents: string list * string list};
    39 
    40 fun make_syntax (thy_syntax, local_syntax, mode, mixfixes, idents) =
    41   Syntax {thy_syntax = thy_syntax, local_syntax = local_syntax,
    42     mode = mode, mixfixes = mixfixes, idents = idents};
    43 
    44 fun map_syntax f (Syntax {thy_syntax, local_syntax, mode, mixfixes, idents}) =
    45   make_syntax (f (thy_syntax, local_syntax, mode, mixfixes, idents));
    46 
    47 fun is_consistent thy (Syntax {thy_syntax, ...}) =
    48   Syntax.eq_syntax (Sign.syn_of thy, thy_syntax);
    49 
    50 fun syn_of (Syntax {local_syntax, ...}) = local_syntax;
    51 fun idents_of (Syntax {idents, ...}) = idents;
    52 val structs_of = #1 o idents_of;
    53 
    54 
    55 (* build syntax *)
    56 
    57 fun build_syntax thy mode mixfixes (idents as (structs, _)) =
    58   let
    59     val thy_syntax = Sign.syn_of thy;
    60     val is_logtype = Sign.is_logtype thy;
    61     fun const_gram ((true, m), decls) = Syntax.update_const_gram is_logtype m decls
    62       | const_gram ((false, m), decls) = Syntax.remove_const_gram is_logtype m decls;
    63     val (atrs, trs, trs', atrs') = Syntax.struct_trfuns structs;
    64     val local_syntax = thy_syntax
    65       |> Syntax.update_trfuns
    66           (map Syntax.mk_trfun atrs, map Syntax.mk_trfun trs,
    67            map Syntax.mk_trfun trs', map Syntax.mk_trfun atrs')
    68       |> fold const_gram (AList.coalesce (op =) (rev (map snd mixfixes)));
    69   in make_syntax (thy_syntax, local_syntax, mode, mixfixes, idents) end;
    70 
    71 fun init thy = build_syntax thy Syntax.mode_default [] ([], []);
    72 
    73 fun rebuild thy (syntax as Syntax {mode, mixfixes, idents, ...}) =
    74   if is_consistent thy syntax then syntax
    75   else build_syntax thy mode mixfixes idents;
    76 
    77 
    78 (* mixfix declarations *)
    79 
    80 local
    81 
    82 fun prep_mixfix _ (_, (_, _, Structure)) = NONE
    83   | prep_mixfix mode (fixed, (x, T, mx)) =
    84       let val c = if fixed then Syntax.fixedN ^ x else x
    85       in SOME ((x, fixed), (mode, (c, T, mx))) end;
    86 
    87 fun prep_struct (fixed, (c, _, Structure)) =
    88       if fixed then SOME c
    89       else error ("Bad mixfix declaration for constant: " ^ 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 
   125 (* extern_term *)
   126 
   127 fun extern_term syntax =
   128   let
   129     val (structs, fixes) = idents_of syntax;
   130     fun map_free (t as Free (x, T)) =
   131           let val i = find_index (fn s => s = x) structs + 1 in
   132             if i = 0 andalso member (op =) fixes x then
   133               Const (Syntax.fixedN ^ x, T)
   134             else if i = 1 andalso not (! show_structs) then
   135               Syntax.const "_struct" $ Syntax.const "_indexdefault"
   136             else t
   137           end
   138       | map_free t = t;
   139   in Term.map_aterms map_free end;
   140 
   141 end;