wenzelm@18997: (* Title: Pure/Isar/local_syntax.ML wenzelm@18997: Author: Makarius wenzelm@18997: wenzelm@18997: Local syntax depending on theory syntax. wenzelm@18997: *) wenzelm@18997: wenzelm@32738: val show_structs = Unsynchronized.ref false; wenzelm@18997: wenzelm@18997: signature LOCAL_SYNTAX = wenzelm@18997: sig wenzelm@18997: type T wenzelm@18997: val syn_of: T -> Syntax.syntax wenzelm@18997: val structs_of: T -> string list wenzelm@18997: val init: theory -> T wenzelm@18997: val rebuild: theory -> T -> T wenzelm@19660: val add_syntax: theory -> (bool * (string * typ * mixfix)) list -> T -> T wenzelm@20785: val set_mode: Syntax.mode -> T -> T wenzelm@19541: val restore_mode: T -> T -> T wenzelm@24951: val update_modesyntax: theory -> bool -> Syntax.mode -> wenzelm@24951: (bool * (string * typ * mixfix)) list -> T -> T wenzelm@19369: val extern_term: T -> term -> term wenzelm@18997: end; wenzelm@18997: wenzelm@33387: structure Local_Syntax: LOCAL_SYNTAX = wenzelm@18997: struct wenzelm@18997: wenzelm@18997: (* datatype T *) wenzelm@18997: wenzelm@19386: type local_mixfix = wenzelm@24951: (string * bool) * (*name, fixed?*) wenzelm@24951: ((bool * Syntax.mode) * (string * typ * mixfix)); (*add?, mode, declaration*) wenzelm@19386: wenzelm@18997: datatype T = Syntax of wenzelm@18997: {thy_syntax: Syntax.syntax, wenzelm@18997: local_syntax: Syntax.syntax, wenzelm@20785: mode: Syntax.mode, wenzelm@19386: mixfixes: local_mixfix list, wenzelm@19369: idents: string list * string list}; wenzelm@18997: wenzelm@19541: fun make_syntax (thy_syntax, local_syntax, mode, mixfixes, idents) = wenzelm@18997: Syntax {thy_syntax = thy_syntax, local_syntax = local_syntax, wenzelm@19541: mode = mode, mixfixes = mixfixes, idents = idents}; wenzelm@18997: wenzelm@19541: fun map_syntax f (Syntax {thy_syntax, local_syntax, mode, mixfixes, idents}) = wenzelm@19541: make_syntax (f (thy_syntax, local_syntax, mode, mixfixes, idents)); wenzelm@18997: wenzelm@19369: fun is_consistent thy (Syntax {thy_syntax, ...}) = wenzelm@18997: Syntax.eq_syntax (Sign.syn_of thy, thy_syntax); wenzelm@18997: wenzelm@18997: fun syn_of (Syntax {local_syntax, ...}) = local_syntax; wenzelm@18997: fun idents_of (Syntax {idents, ...}) = idents; wenzelm@18997: val structs_of = #1 o idents_of; wenzelm@18997: wenzelm@18997: wenzelm@18997: (* build syntax *) wenzelm@18997: wenzelm@19541: fun build_syntax thy mode mixfixes (idents as (structs, _)) = wenzelm@18997: let wenzelm@18997: val thy_syntax = Sign.syn_of thy; wenzelm@18997: val is_logtype = Sign.is_logtype thy; wenzelm@25385: fun const_gram ((true, m), decls) = Syntax.update_const_gram is_logtype m decls wenzelm@24951: | const_gram ((false, m), decls) = Syntax.remove_const_gram is_logtype m decls; wenzelm@18997: val (atrs, trs, trs', atrs') = Syntax.struct_trfuns structs; wenzelm@18997: val local_syntax = thy_syntax wenzelm@25390: |> Syntax.update_trfuns wenzelm@19386: (map Syntax.mk_trfun atrs, map Syntax.mk_trfun trs, wenzelm@19386: map Syntax.mk_trfun trs', map Syntax.mk_trfun atrs') wenzelm@24951: |> fold const_gram (AList.coalesce (op =) (rev (map snd mixfixes))); wenzelm@19541: in make_syntax (thy_syntax, local_syntax, mode, mixfixes, idents) end; wenzelm@19541: wenzelm@24960: fun init thy = build_syntax thy Syntax.mode_default [] ([], []); wenzelm@18997: wenzelm@19541: fun rebuild thy (syntax as Syntax {mode, mixfixes, idents, ...}) = wenzelm@19541: if is_consistent thy syntax then syntax wenzelm@19541: else build_syntax thy mode mixfixes idents; wenzelm@18997: wenzelm@19541: wenzelm@18997: (* mixfix declarations *) wenzelm@18997: wenzelm@18997: local wenzelm@18997: wenzelm@24951: fun prep_mixfix _ (_, (_, _, Structure)) = NONE wenzelm@24951: | prep_mixfix mode (fixed, (x, T, mx)) = wenzelm@24951: let val c = if fixed then Syntax.fixedN ^ x else x wenzelm@24951: in SOME ((x, fixed), (mode, (c, T, mx))) end; wenzelm@19016: wenzelm@19016: fun prep_struct (fixed, (c, _, Structure)) = wenzelm@19016: if fixed then SOME c wenzelm@24951: else error ("Bad mixfix declaration for constant: " ^ quote c) wenzelm@19016: | prep_struct _ = NONE; wenzelm@18997: wenzelm@18997: in wenzelm@18997: wenzelm@24951: fun update_syntax add thy raw_decls wenzelm@24951: (syntax as (Syntax {mode, mixfixes, idents = (structs, _), ...})) = wenzelm@24951: (case filter_out (fn (_, (_, _, mx)) => mx = NoSyn) raw_decls of wenzelm@19016: [] => syntax wenzelm@19016: | decls => wenzelm@19016: let wenzelm@24954: val new_mixfixes = map_filter (prep_mixfix (add, mode)) decls; wenzelm@24954: val new_structs = map_filter prep_struct decls; wenzelm@24954: val mixfixes' = rev new_mixfixes @ mixfixes; wenzelm@24954: val structs' = wenzelm@24954: if add then structs @ new_structs wenzelm@24954: else subtract (op =) new_structs structs; wenzelm@20785: val fixes' = fold (fn ((x, true), _) => cons x | _ => I) mixfixes' []; wenzelm@19541: in build_syntax thy mode mixfixes' (structs', fixes') end); wenzelm@18997: wenzelm@24951: val add_syntax = update_syntax true; wenzelm@24951: wenzelm@18997: end; wenzelm@18997: wenzelm@18997: wenzelm@19660: (* syntax mode *) wenzelm@19660: wenzelm@19660: fun set_mode mode = map_syntax (fn (thy_syntax, local_syntax, _, mixfixes, idents) => wenzelm@19660: (thy_syntax, local_syntax, mode, mixfixes, idents)); wenzelm@19660: wenzelm@19660: fun restore_mode (Syntax {mode, ...}) = set_mode mode; wenzelm@19660: wenzelm@24951: fun update_modesyntax thy add mode args syntax = wenzelm@24951: syntax |> set_mode mode |> update_syntax add thy args |> restore_mode syntax; wenzelm@19660: wenzelm@19660: wenzelm@18997: (* extern_term *) wenzelm@18997: wenzelm@19369: fun extern_term syntax = wenzelm@18997: let wenzelm@19369: val (structs, fixes) = idents_of syntax; wenzelm@18997: fun map_free (t as Free (x, T)) = wenzelm@19618: let val i = find_index (fn s => s = x) structs + 1 in wenzelm@18997: if i = 0 andalso member (op =) fixes x then wenzelm@18997: Const (Syntax.fixedN ^ x, T) wenzelm@18997: else if i = 1 andalso not (! show_structs) then wenzelm@18997: Syntax.const "_struct" $ Syntax.const "_indexdefault" wenzelm@18997: else t wenzelm@18997: end wenzelm@18997: | map_free t = t; wenzelm@19369: in Term.map_aterms map_free end; wenzelm@18997: wenzelm@18997: end;