author | wenzelm |
Thu, 07 Aug 2008 19:21:41 +0200 | |
changeset 27779 | 4569003b8813 |
parent 25390 | 8bfa6566ac6b |
child 29606 | fedb8be05f24 |
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 |
20785 | 18 |
val set_mode: Syntax.mode -> T -> T |
19541 | 19 |
val restore_mode: T -> T -> T |
24951
834b8c2b9553
replaced add_modesyntax by general update_modesyntax (add or del);
wenzelm
parents:
20785
diff
changeset
|
20 |
val update_modesyntax: theory -> bool -> Syntax.mode -> |
834b8c2b9553
replaced add_modesyntax by general update_modesyntax (add or del);
wenzelm
parents:
20785
diff
changeset
|
21 |
(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
|
22 |
val extern_term: T -> term -> term |
18997 | 23 |
end; |
24 |
||
19016 | 25 |
structure LocalSyntax: LOCAL_SYNTAX = |
18997 | 26 |
struct |
27 |
||
28 |
(* datatype T *) |
|
29 |
||
19386 | 30 |
type local_mixfix = |
24951
834b8c2b9553
replaced add_modesyntax by general update_modesyntax (add or del);
wenzelm
parents:
20785
diff
changeset
|
31 |
(string * bool) * (*name, fixed?*) |
834b8c2b9553
replaced add_modesyntax by general update_modesyntax (add or del);
wenzelm
parents:
20785
diff
changeset
|
32 |
((bool * Syntax.mode) * (string * typ * mixfix)); (*add?, mode, declaration*) |
19386 | 33 |
|
18997 | 34 |
datatype T = Syntax of |
35 |
{thy_syntax: Syntax.syntax, |
|
36 |
local_syntax: Syntax.syntax, |
|
20785 | 37 |
mode: Syntax.mode, |
19386 | 38 |
mixfixes: local_mixfix list, |
19369
a4374b41c9bf
simplified handling of authentic syntax (cf. early externing in consts.ML);
wenzelm
parents:
19016
diff
changeset
|
39 |
idents: string list * string list}; |
18997 | 40 |
|
19541 | 41 |
fun make_syntax (thy_syntax, local_syntax, mode, mixfixes, idents) = |
18997 | 42 |
Syntax {thy_syntax = thy_syntax, local_syntax = local_syntax, |
19541 | 43 |
mode = mode, mixfixes = mixfixes, idents = idents}; |
18997 | 44 |
|
19541 | 45 |
fun map_syntax f (Syntax {thy_syntax, local_syntax, mode, mixfixes, idents}) = |
46 |
make_syntax (f (thy_syntax, local_syntax, mode, mixfixes, idents)); |
|
18997 | 47 |
|
19369
a4374b41c9bf
simplified handling of authentic syntax (cf. early externing in consts.ML);
wenzelm
parents:
19016
diff
changeset
|
48 |
fun is_consistent thy (Syntax {thy_syntax, ...}) = |
18997 | 49 |
Syntax.eq_syntax (Sign.syn_of thy, thy_syntax); |
50 |
||
51 |
fun syn_of (Syntax {local_syntax, ...}) = local_syntax; |
|
52 |
fun idents_of (Syntax {idents, ...}) = idents; |
|
53 |
val structs_of = #1 o idents_of; |
|
54 |
||
55 |
||
56 |
(* build syntax *) |
|
57 |
||
19541 | 58 |
fun build_syntax thy mode mixfixes (idents as (structs, _)) = |
18997 | 59 |
let |
60 |
val thy_syntax = Sign.syn_of thy; |
|
61 |
val is_logtype = Sign.is_logtype thy; |
|
25385
42df506673ed
update_modesyntax: based on Syntax.update_const_gram (avoids duplicates);
wenzelm
parents:
24960
diff
changeset
|
62 |
fun const_gram ((true, m), decls) = Syntax.update_const_gram is_logtype m decls |
24951
834b8c2b9553
replaced add_modesyntax by general update_modesyntax (add or del);
wenzelm
parents:
20785
diff
changeset
|
63 |
| const_gram ((false, m), decls) = Syntax.remove_const_gram is_logtype m decls; |
18997 | 64 |
val (atrs, trs, trs', atrs') = Syntax.struct_trfuns structs; |
65 |
val local_syntax = thy_syntax |
|
25390
8bfa6566ac6b
syntax operations: turned extend'' into update'' (absorb duplicates);
wenzelm
parents:
25385
diff
changeset
|
66 |
|> Syntax.update_trfuns |
19386 | 67 |
(map Syntax.mk_trfun atrs, map Syntax.mk_trfun trs, |
68 |
map Syntax.mk_trfun trs', map Syntax.mk_trfun atrs') |
|
24951
834b8c2b9553
replaced add_modesyntax by general update_modesyntax (add or del);
wenzelm
parents:
20785
diff
changeset
|
69 |
|> fold const_gram (AList.coalesce (op =) (rev (map snd mixfixes))); |
19541 | 70 |
in make_syntax (thy_syntax, local_syntax, mode, mixfixes, idents) end; |
71 |
||
24960 | 72 |
fun init thy = build_syntax thy Syntax.mode_default [] ([], []); |
18997 | 73 |
|
19541 | 74 |
fun rebuild thy (syntax as Syntax {mode, mixfixes, idents, ...}) = |
75 |
if is_consistent thy syntax then syntax |
|
76 |
else build_syntax thy mode mixfixes idents; |
|
18997 | 77 |
|
19541 | 78 |
|
18997 | 79 |
(* mixfix declarations *) |
80 |
||
81 |
local |
|
82 |
||
24951
834b8c2b9553
replaced add_modesyntax by general update_modesyntax (add or del);
wenzelm
parents:
20785
diff
changeset
|
83 |
fun prep_mixfix _ (_, (_, _, Structure)) = NONE |
834b8c2b9553
replaced add_modesyntax by general update_modesyntax (add or del);
wenzelm
parents:
20785
diff
changeset
|
84 |
| prep_mixfix mode (fixed, (x, T, mx)) = |
834b8c2b9553
replaced add_modesyntax by general update_modesyntax (add or del);
wenzelm
parents:
20785
diff
changeset
|
85 |
let val c = if fixed then Syntax.fixedN ^ x else x |
834b8c2b9553
replaced add_modesyntax by general update_modesyntax (add or del);
wenzelm
parents:
20785
diff
changeset
|
86 |
in SOME ((x, fixed), (mode, (c, T, mx))) end; |
19016 | 87 |
|
88 |
fun prep_struct (fixed, (c, _, Structure)) = |
|
89 |
if fixed then SOME c |
|
24951
834b8c2b9553
replaced add_modesyntax by general update_modesyntax (add or del);
wenzelm
parents:
20785
diff
changeset
|
90 |
else error ("Bad mixfix declaration for constant: " ^ quote c) |
19016 | 91 |
| prep_struct _ = NONE; |
18997 | 92 |
|
93 |
in |
|
94 |
||
24951
834b8c2b9553
replaced add_modesyntax by general update_modesyntax (add or del);
wenzelm
parents:
20785
diff
changeset
|
95 |
fun update_syntax add thy raw_decls |
834b8c2b9553
replaced add_modesyntax by general update_modesyntax (add or del);
wenzelm
parents:
20785
diff
changeset
|
96 |
(syntax as (Syntax {mode, mixfixes, idents = (structs, _), ...})) = |
834b8c2b9553
replaced add_modesyntax by general update_modesyntax (add or del);
wenzelm
parents:
20785
diff
changeset
|
97 |
(case filter_out (fn (_, (_, _, mx)) => mx = NoSyn) raw_decls of |
19016 | 98 |
[] => syntax |
99 |
| decls => |
|
100 |
let |
|
24954
0664f10a4094
update_modesyntax: may delete 'structure' notation as well;
wenzelm
parents:
24951
diff
changeset
|
101 |
val new_mixfixes = map_filter (prep_mixfix (add, mode)) decls; |
0664f10a4094
update_modesyntax: may delete 'structure' notation as well;
wenzelm
parents:
24951
diff
changeset
|
102 |
val new_structs = map_filter prep_struct decls; |
0664f10a4094
update_modesyntax: may delete 'structure' notation as well;
wenzelm
parents:
24951
diff
changeset
|
103 |
val mixfixes' = rev new_mixfixes @ mixfixes; |
0664f10a4094
update_modesyntax: may delete 'structure' notation as well;
wenzelm
parents:
24951
diff
changeset
|
104 |
val structs' = |
0664f10a4094
update_modesyntax: may delete 'structure' notation as well;
wenzelm
parents:
24951
diff
changeset
|
105 |
if add then structs @ new_structs |
0664f10a4094
update_modesyntax: may delete 'structure' notation as well;
wenzelm
parents:
24951
diff
changeset
|
106 |
else subtract (op =) new_structs structs; |
20785 | 107 |
val fixes' = fold (fn ((x, true), _) => cons x | _ => I) mixfixes' []; |
19541 | 108 |
in build_syntax thy mode mixfixes' (structs', fixes') end); |
18997 | 109 |
|
24951
834b8c2b9553
replaced add_modesyntax by general update_modesyntax (add or del);
wenzelm
parents:
20785
diff
changeset
|
110 |
val add_syntax = update_syntax true; |
834b8c2b9553
replaced add_modesyntax by general update_modesyntax (add or del);
wenzelm
parents:
20785
diff
changeset
|
111 |
|
18997 | 112 |
end; |
113 |
||
114 |
||
19660 | 115 |
(* syntax mode *) |
116 |
||
117 |
fun set_mode mode = map_syntax (fn (thy_syntax, local_syntax, _, mixfixes, idents) => |
|
118 |
(thy_syntax, local_syntax, mode, mixfixes, idents)); |
|
119 |
||
120 |
fun restore_mode (Syntax {mode, ...}) = set_mode mode; |
|
121 |
||
24951
834b8c2b9553
replaced add_modesyntax by general update_modesyntax (add or del);
wenzelm
parents:
20785
diff
changeset
|
122 |
fun update_modesyntax thy add mode args syntax = |
834b8c2b9553
replaced add_modesyntax by general update_modesyntax (add or del);
wenzelm
parents:
20785
diff
changeset
|
123 |
syntax |> set_mode mode |> update_syntax add thy args |> restore_mode syntax; |
19660 | 124 |
|
125 |
||
18997 | 126 |
(* extern_term *) |
127 |
||
19369
a4374b41c9bf
simplified handling of authentic syntax (cf. early externing in consts.ML);
wenzelm
parents:
19016
diff
changeset
|
128 |
fun extern_term syntax = |
18997 | 129 |
let |
19369
a4374b41c9bf
simplified handling of authentic syntax (cf. early externing in consts.ML);
wenzelm
parents:
19016
diff
changeset
|
130 |
val (structs, fixes) = idents_of syntax; |
18997 | 131 |
fun map_free (t as Free (x, T)) = |
19618 | 132 |
let val i = find_index (fn s => s = x) structs + 1 in |
18997 | 133 |
if i = 0 andalso member (op =) fixes x then |
134 |
Const (Syntax.fixedN ^ x, T) |
|
135 |
else if i = 1 andalso not (! show_structs) then |
|
136 |
Syntax.const "_struct" $ Syntax.const "_indexdefault" |
|
137 |
else t |
|
138 |
end |
|
139 |
| map_free t = t; |
|
19369
a4374b41c9bf
simplified handling of authentic syntax (cf. early externing in consts.ML);
wenzelm
parents:
19016
diff
changeset
|
140 |
in Term.map_aterms map_free end; |
18997 | 141 |
|
142 |
end; |