18997
|
1 |
(* Title: Pure/Isar/local_syntax.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Makarius
|
|
4 |
|
|
5 |
Local syntax depending on theory syntax.
|
|
6 |
*)
|
|
7 |
|
|
8 |
val show_structs = ref false;
|
|
9 |
|
|
10 |
signature LOCAL_SYNTAX =
|
|
11 |
sig
|
|
12 |
type T
|
|
13 |
val syn_of: T -> Syntax.syntax
|
|
14 |
val structs_of: T -> string list
|
|
15 |
val init: theory -> T
|
|
16 |
val rebuild: theory -> T -> T
|
|
17 |
val add_syntax: theory -> (bool * (string * typ * mixfix)) list -> T -> T
|
|
18 |
val extern_term: (string -> xstring) -> theory -> T -> term -> term
|
|
19 |
end;
|
|
20 |
|
19016
|
21 |
structure LocalSyntax: LOCAL_SYNTAX =
|
18997
|
22 |
struct
|
|
23 |
|
|
24 |
(* datatype T *)
|
|
25 |
|
|
26 |
datatype T = Syntax of
|
|
27 |
{thy_syntax: Syntax.syntax,
|
|
28 |
local_syntax: Syntax.syntax,
|
19016
|
29 |
mixfixes: (((string * bool) * string list list) * (string * typ * mixfix)) list,
|
18997
|
30 |
idents: string list * string list * string list};
|
|
31 |
|
|
32 |
fun make_syntax (thy_syntax, local_syntax, mixfixes, idents) =
|
|
33 |
Syntax {thy_syntax = thy_syntax, local_syntax = local_syntax,
|
|
34 |
mixfixes = mixfixes, idents = idents};
|
|
35 |
|
|
36 |
fun map_syntax f (Syntax {thy_syntax, local_syntax, mixfixes, idents}) =
|
|
37 |
make_syntax (f (thy_syntax, local_syntax, mixfixes, idents));
|
|
38 |
|
|
39 |
fun is_consistent thy (syntax as Syntax {thy_syntax, ...}) =
|
|
40 |
Syntax.eq_syntax (Sign.syn_of thy, thy_syntax);
|
|
41 |
|
|
42 |
fun syn_of (Syntax {local_syntax, ...}) = local_syntax;
|
|
43 |
fun idents_of (Syntax {idents, ...}) = idents;
|
|
44 |
val structs_of = #1 o idents_of;
|
|
45 |
|
|
46 |
|
|
47 |
(* build syntax *)
|
|
48 |
|
19016
|
49 |
fun build_syntax thy (mixfixes, idents as (structs, _, _)) =
|
18997
|
50 |
let
|
|
51 |
val thy_syntax = Sign.syn_of thy;
|
|
52 |
val is_logtype = Sign.is_logtype thy;
|
|
53 |
val (atrs, trs, trs', atrs') = Syntax.struct_trfuns structs;
|
|
54 |
val local_syntax = thy_syntax
|
|
55 |
|> Syntax.extend_trfuns
|
|
56 |
(map Syntax.mk_trfun atrs, map Syntax.mk_trfun trs,
|
|
57 |
map Syntax.mk_trfun trs', map Syntax.mk_trfun atrs')
|
19016
|
58 |
|> Syntax.extend_const_gram is_logtype ("", false)
|
|
59 |
(map (fn (((x, _), _), (c, T, _)) => (c, T, Syntax.literal x)) mixfixes)
|
|
60 |
|> Syntax.extend_const_gram is_logtype ("", true) (map snd mixfixes)
|
18997
|
61 |
in make_syntax (thy_syntax, local_syntax, mixfixes, idents) end
|
|
62 |
|
19016
|
63 |
fun init thy = build_syntax thy ([], ([], [], []));
|
18997
|
64 |
|
|
65 |
fun rebuild thy (syntax as Syntax {mixfixes, idents, ...}) =
|
|
66 |
if is_consistent thy syntax then syntax
|
|
67 |
else build_syntax thy (mixfixes, idents);
|
|
68 |
|
|
69 |
|
|
70 |
(* mixfix declarations *)
|
|
71 |
|
|
72 |
local
|
|
73 |
|
19016
|
74 |
fun mixfix_nosyn (_, (_, _, mx)) = mx = NoSyn;
|
|
75 |
fun mixfix_struct (_, (_, _, mx)) = mx = Structure;
|
|
76 |
|
|
77 |
fun mixfix_conflict (content1: string list list, ((_, content2), _)) =
|
|
78 |
exists (fn x => exists (fn y => x = y) content2) content1;
|
18997
|
79 |
|
19016
|
80 |
fun add_mixfix (fixed, (x, T, mx)) =
|
|
81 |
let
|
|
82 |
val content = Syntax.mixfix_content mx;
|
|
83 |
val c = if fixed then Syntax.fixedN ^ x else Syntax.constN ^ x;
|
|
84 |
in remove mixfix_conflict content #> cons (((x, fixed), content), (c, T, mx)) end;
|
|
85 |
|
|
86 |
fun prep_struct (fixed, (c, _, Structure)) =
|
|
87 |
if fixed then SOME c
|
|
88 |
else error ("Bad mixfix declaration for const: " ^ quote c)
|
|
89 |
| prep_struct _ = NONE;
|
18997
|
90 |
|
|
91 |
in
|
|
92 |
|
19016
|
93 |
fun add_syntax thy raw_decls (syntax as (Syntax {mixfixes, idents = (structs, _, _), ...})) =
|
|
94 |
(case filter_out mixfix_nosyn raw_decls of
|
|
95 |
[] => syntax
|
|
96 |
| decls =>
|
|
97 |
let
|
|
98 |
val mixfixes' = mixfixes |> fold add_mixfix (filter_out mixfix_struct decls);
|
|
99 |
val fixes' = fold (fn (((x, true), _), _) => cons x | _ => I) mixfixes' [];
|
|
100 |
val consts' = fold (fn (((x, false), _), _) => cons x | _ => I) mixfixes' [];
|
|
101 |
val structs' = structs @ List.mapPartial prep_struct decls;
|
|
102 |
in build_syntax thy (mixfixes', (structs', fixes', consts')) end);
|
18997
|
103 |
|
|
104 |
end;
|
|
105 |
|
|
106 |
|
|
107 |
(* extern_term *)
|
|
108 |
|
|
109 |
fun extern_term extern_const thy syntax =
|
|
110 |
let
|
|
111 |
val (structs, fixes, consts) = idents_of syntax;
|
|
112 |
fun map_const c =
|
|
113 |
if member (op =) consts c then Syntax.constN ^ c else extern_const c;
|
|
114 |
fun map_free (t as Free (x, T)) =
|
|
115 |
let val i = Library.find_index_eq x structs + 1 in
|
|
116 |
if i = 0 andalso member (op =) fixes x then
|
|
117 |
Const (Syntax.fixedN ^ x, T)
|
|
118 |
else if i = 1 andalso not (! show_structs) then
|
|
119 |
Syntax.const "_struct" $ Syntax.const "_indexdefault"
|
|
120 |
else t
|
|
121 |
end
|
|
122 |
| map_free t = t;
|
|
123 |
in Sign.extern_term map_const thy #> Term.map_aterms map_free end;
|
|
124 |
|
|
125 |
|
|
126 |
end;
|