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 |
|
|
21 |
structure LocalSyntax (* : LOCAL_SYNTAX *) =
|
|
22 |
struct
|
|
23 |
|
|
24 |
(* datatype T *)
|
|
25 |
|
|
26 |
datatype T = Syntax of
|
|
27 |
{thy_syntax: Syntax.syntax,
|
|
28 |
local_syntax: Syntax.syntax,
|
|
29 |
mixfixes: (string * typ * mixfix) list * (string * typ * mixfix) list,
|
|
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 |
|
|
49 |
fun build_syntax thy (mixfixes as (mxs, mxs_output), idents as (structs, _, _)) =
|
|
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')
|
|
58 |
|> Syntax.extend_const_gram is_logtype ("", false) mxs_output
|
|
59 |
|> Syntax.extend_const_gram is_logtype ("", true) mxs;
|
|
60 |
in make_syntax (thy_syntax, local_syntax, mixfixes, idents) end
|
|
61 |
|
|
62 |
fun init thy = build_syntax thy (([], []), ([], [], []));
|
|
63 |
|
|
64 |
fun rebuild thy (syntax as Syntax {mixfixes, idents, ...}) =
|
|
65 |
if is_consistent thy syntax then syntax
|
|
66 |
else build_syntax thy (mixfixes, idents);
|
|
67 |
|
|
68 |
|
|
69 |
(* mixfix declarations *)
|
|
70 |
|
|
71 |
local
|
|
72 |
|
|
73 |
fun mixfix_conflict (mx1, (_, _, mx2)) = Syntax.mixfix_conflict (mx1, mx2);
|
|
74 |
fun mixfix_proper (_, _, mx) = mx <> NoSyn andalso mx <> Structure;
|
|
75 |
|
|
76 |
fun mixfix_output (c, T, _) =
|
|
77 |
let val c' = unprefix Syntax.fixedN c handle Fail _ => unprefix Syntax.constN c
|
|
78 |
in (c, T, Syntax.literal c') end;
|
|
79 |
|
|
80 |
in
|
|
81 |
|
|
82 |
fun add_syntax thy decls (Syntax {mixfixes = (mxs, _), idents = (structs, _, _), ...}) =
|
|
83 |
let
|
|
84 |
fun add_mx (fixed, (c, T, mx)) =
|
|
85 |
remove mixfix_conflict mx #>
|
|
86 |
cons (if fixed then Syntax.fixedN ^ c else Syntax.constN ^ c, T, mx);
|
|
87 |
val mxs' = mxs |> fold add_mx (filter (mixfix_proper o snd) decls);
|
|
88 |
|
|
89 |
val fixes' = List.mapPartial (try (unprefix Syntax.fixedN) o #1) mxs';
|
|
90 |
val consts' = List.mapPartial (try (unprefix Syntax.constN) o #1) mxs';
|
|
91 |
|
|
92 |
fun prep_struct (fixed, (c, _, Structure)) =
|
|
93 |
if fixed then SOME c
|
|
94 |
else error ("Bad mixfix declaration for const: " ^ quote c)
|
|
95 |
| prep_struct _ = NONE;
|
|
96 |
val structs' = structs @ List.mapPartial prep_struct decls;
|
|
97 |
in build_syntax thy ((mxs', map mixfix_output mxs'), (structs', fixes', consts')) end;
|
|
98 |
|
|
99 |
end;
|
|
100 |
|
|
101 |
|
|
102 |
(* extern_term *)
|
|
103 |
|
|
104 |
fun extern_term extern_const thy syntax =
|
|
105 |
let
|
|
106 |
val (structs, fixes, consts) = idents_of syntax;
|
|
107 |
fun map_const c =
|
|
108 |
if member (op =) consts c then Syntax.constN ^ c else extern_const c;
|
|
109 |
fun map_free (t as Free (x, T)) =
|
|
110 |
let val i = Library.find_index_eq x structs + 1 in
|
|
111 |
if i = 0 andalso member (op =) fixes x then
|
|
112 |
Const (Syntax.fixedN ^ x, T)
|
|
113 |
else if i = 1 andalso not (! show_structs) then
|
|
114 |
Syntax.const "_struct" $ Syntax.const "_indexdefault"
|
|
115 |
else t
|
|
116 |
end
|
|
117 |
| map_free t = t;
|
|
118 |
in Sign.extern_term map_const thy #> Term.map_aterms map_free end;
|
|
119 |
|
|
120 |
|
|
121 |
end;
|