author | wenzelm |
Wed, 09 Aug 2006 00:12:38 +0200 | |
changeset 20366 | 867696dc64fc |
parent 19660 | e3ec6839c631 |
child 20785 | d60f81c56fd4 |
permissions | -rw-r--r-- |
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 |
|
19660 | 17 |
val add_syntax: theory -> (bool * (string * typ * mixfix)) list -> T -> T |
19541 | 18 |
val set_mode: string * bool -> T -> T |
19 |
val restore_mode: T -> T -> T |
|
19660 | 20 |
val add_modesyntax: theory -> string * bool -> (bool * (string * typ * mixfix)) list -> T -> T |
19369
a4374b41c9bf
simplified handling of authentic syntax (cf. early externing in consts.ML);
wenzelm
parents:
19016
diff
changeset
|
21 |
val extern_term: T -> term -> term |
18997 | 22 |
end; |
23 |
||
19016 | 24 |
structure LocalSyntax: LOCAL_SYNTAX = |
18997 | 25 |
struct |
26 |
||
27 |
(* datatype T *) |
|
28 |
||
19386 | 29 |
type local_mixfix = |
30 |
((string * bool) * string list list) * (*name, fixed?, mixfix content*) |
|
19541 | 31 |
((string * bool) * (string * typ * mixfix)); (*mode, mixfix syntax*) |
19386 | 32 |
|
18997 | 33 |
datatype T = Syntax of |
34 |
{thy_syntax: Syntax.syntax, |
|
35 |
local_syntax: Syntax.syntax, |
|
19541 | 36 |
mode: string * bool, |
19386 | 37 |
mixfixes: local_mixfix list, |
19369
a4374b41c9bf
simplified handling of authentic syntax (cf. early externing in consts.ML);
wenzelm
parents:
19016
diff
changeset
|
38 |
idents: string list * string list}; |
18997 | 39 |
|
19541 | 40 |
fun make_syntax (thy_syntax, local_syntax, mode, mixfixes, idents) = |
18997 | 41 |
Syntax {thy_syntax = thy_syntax, local_syntax = local_syntax, |
19541 | 42 |
mode = mode, mixfixes = mixfixes, idents = idents}; |
18997 | 43 |
|
19541 | 44 |
fun map_syntax f (Syntax {thy_syntax, local_syntax, mode, mixfixes, idents}) = |
45 |
make_syntax (f (thy_syntax, local_syntax, mode, mixfixes, idents)); |
|
18997 | 46 |
|
19369
a4374b41c9bf
simplified handling of authentic syntax (cf. early externing in consts.ML);
wenzelm
parents:
19016
diff
changeset
|
47 |
fun is_consistent thy (Syntax {thy_syntax, ...}) = |
18997 | 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 |
||
19541 | 57 |
fun build_syntax thy mode mixfixes (idents as (structs, _)) = |
18997 | 58 |
let |
59 |
val thy_syntax = Sign.syn_of thy; |
|
60 |
val is_logtype = Sign.is_logtype thy; |
|
61 |
val (atrs, trs, trs', atrs') = Syntax.struct_trfuns structs; |
|
62 |
val local_syntax = thy_syntax |
|
63 |
|> Syntax.extend_trfuns |
|
19386 | 64 |
(map Syntax.mk_trfun atrs, map Syntax.mk_trfun trs, |
65 |
map Syntax.mk_trfun trs', map Syntax.mk_trfun atrs') |
|
66 |
|> fold (uncurry (Syntax.extend_const_gram is_logtype)) |
|
19454
46a7e133f802
moved coalesce to AList, added equality predicates to library
haftmann
parents:
19386
diff
changeset
|
67 |
(AList.coalesce (op =) (rev (map snd mixfixes))); |
19541 | 68 |
in make_syntax (thy_syntax, local_syntax, mode, mixfixes, idents) end; |
69 |
||
70 |
fun init thy = build_syntax thy Syntax.default_mode [] ([], []); |
|
18997 | 71 |
|
19541 | 72 |
fun rebuild thy (syntax as Syntax {mode, mixfixes, idents, ...}) = |
73 |
if is_consistent thy syntax then syntax |
|
74 |
else build_syntax thy mode mixfixes idents; |
|
18997 | 75 |
|
19541 | 76 |
|
18997 | 77 |
(* mixfix declarations *) |
78 |
||
79 |
local |
|
80 |
||
19016 | 81 |
fun mixfix_nosyn (_, (_, _, mx)) = mx = NoSyn; |
82 |
fun mixfix_struct (_, (_, _, mx)) = mx = Structure; |
|
83 |
||
19386 | 84 |
fun mixfix_conflict ((content1: string list list, inout1), ((_, content2), ((_, inout2), _))) = |
85 |
inout1 andalso inout2 andalso exists (fn x => exists (fn y => x = y) content2) content1; |
|
18997 | 86 |
|
19386 | 87 |
fun add_mixfix (mode, inout) (fixed, (x, T, mx)) = |
19016 | 88 |
let |
89 |
val content = Syntax.mixfix_content mx; |
|
19369
a4374b41c9bf
simplified handling of authentic syntax (cf. early externing in consts.ML);
wenzelm
parents:
19016
diff
changeset
|
90 |
val c = if fixed then Syntax.fixedN ^ x else x; |
19386 | 91 |
in |
92 |
remove mixfix_conflict (content, inout) #> |
|
93 |
cons (((x, fixed), content), ((mode, inout), (c, T, mx))) |
|
94 |
end; |
|
19016 | 95 |
|
96 |
fun prep_struct (fixed, (c, _, Structure)) = |
|
97 |
if fixed then SOME c |
|
98 |
else error ("Bad mixfix declaration for const: " ^ quote c) |
|
99 |
| prep_struct _ = NONE; |
|
18997 | 100 |
|
101 |
in |
|
102 |
||
19541 | 103 |
fun add_syntax thy raw_decls (syntax as (Syntax {mode, mixfixes, idents = (structs, _), ...})) = |
19016 | 104 |
(case filter_out mixfix_nosyn raw_decls of |
105 |
[] => syntax |
|
106 |
| decls => |
|
107 |
let |
|
19541 | 108 |
val mixfixes' = mixfixes |> fold (add_mixfix mode) (filter_out mixfix_struct decls); |
19016 | 109 |
val fixes' = fold (fn (((x, true), _), _) => cons x | _ => I) mixfixes' []; |
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19454
diff
changeset
|
110 |
val structs' = structs @ map_filter prep_struct decls; |
19541 | 111 |
in build_syntax thy mode mixfixes' (structs', fixes') end); |
18997 | 112 |
|
113 |
end; |
|
114 |
||
115 |
||
19660 | 116 |
(* syntax mode *) |
117 |
||
118 |
fun set_mode mode = map_syntax (fn (thy_syntax, local_syntax, _, mixfixes, idents) => |
|
119 |
(thy_syntax, local_syntax, mode, mixfixes, idents)); |
|
120 |
||
121 |
fun restore_mode (Syntax {mode, ...}) = set_mode mode; |
|
122 |
||
123 |
fun add_modesyntax thy mode args syntax = |
|
124 |
syntax |> set_mode mode |> add_syntax thy args |> restore_mode syntax; |
|
125 |
||
126 |
||
18997 | 127 |
(* extern_term *) |
128 |
||
19369
a4374b41c9bf
simplified handling of authentic syntax (cf. early externing in consts.ML);
wenzelm
parents:
19016
diff
changeset
|
129 |
fun extern_term syntax = |
18997 | 130 |
let |
19369
a4374b41c9bf
simplified handling of authentic syntax (cf. early externing in consts.ML);
wenzelm
parents:
19016
diff
changeset
|
131 |
val (structs, fixes) = idents_of syntax; |
18997 | 132 |
fun map_free (t as Free (x, T)) = |
19618 | 133 |
let val i = find_index (fn s => s = x) structs + 1 in |
18997 | 134 |
if i = 0 andalso member (op =) fixes x then |
135 |
Const (Syntax.fixedN ^ x, T) |
|
136 |
else if i = 1 andalso not (! show_structs) then |
|
137 |
Syntax.const "_struct" $ Syntax.const "_indexdefault" |
|
138 |
else t |
|
139 |
end |
|
140 |
| map_free t = t; |
|
19369
a4374b41c9bf
simplified handling of authentic syntax (cf. early externing in consts.ML);
wenzelm
parents:
19016
diff
changeset
|
141 |
in Term.map_aterms map_free end; |
18997 | 142 |
|
143 |
end; |