author | wenzelm |
Sat, 01 Mar 2014 22:46:31 +0100 | |
changeset 55828 | 42ac3cfb89f6 |
parent 55550 | bcc643ac071a |
child 55829 | b7bdea5336dd |
permissions | -rw-r--r-- |
42243 | 1 |
(* Title: Pure/Syntax/syntax_phases.ML |
42241
dd8029f71e1c
separate module for standard implementation of inner syntax operations;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
dd8029f71e1c
separate module for standard implementation of inner syntax operations;
wenzelm
parents:
diff
changeset
|
3 |
|
42243 | 4 |
Main phases of inner syntax processing, with standard implementations |
5 |
of parse/unparse operations. |
|
42241
dd8029f71e1c
separate module for standard implementation of inner syntax operations;
wenzelm
parents:
diff
changeset
|
6 |
*) |
dd8029f71e1c
separate module for standard implementation of inner syntax operations;
wenzelm
parents:
diff
changeset
|
7 |
|
42243 | 8 |
signature SYNTAX_PHASES = |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
9 |
sig |
45427
fca432074fb2
sort assignment before simultaneous term_check, not isolated parse_term;
wenzelm
parents:
45423
diff
changeset
|
10 |
val decode_sort: term -> sort |
fca432074fb2
sort assignment before simultaneous term_check, not isolated parse_term;
wenzelm
parents:
45423
diff
changeset
|
11 |
val decode_typ: term -> typ |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
12 |
val decode_term: Proof.context -> |
44736 | 13 |
Position.report list * term Exn.result -> Position.report list * term Exn.result |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
14 |
val parse_ast_pattern: Proof.context -> string * string -> Ast.ast |
42247
12fe41a92cd5
typed_print_translation: discontinued show_sorts argument;
wenzelm
parents:
42245
diff
changeset
|
15 |
val term_of_typ: Proof.context -> typ -> term |
45429 | 16 |
val print_checks: Proof.context -> unit |
17 |
val typ_check: int -> string -> (Proof.context -> typ list -> typ list) -> |
|
18 |
Context.generic -> Context.generic |
|
19 |
val term_check: int -> string -> (Proof.context -> term list -> term list) -> |
|
20 |
Context.generic -> Context.generic |
|
21 |
val typ_uncheck: int -> string -> (Proof.context -> typ list -> typ list) -> |
|
22 |
Context.generic -> Context.generic |
|
23 |
val term_uncheck: int -> string -> (Proof.context -> term list -> term list) -> |
|
24 |
Context.generic -> Context.generic |
|
45444 | 25 |
val typ_check': int -> string -> |
26 |
(typ list -> Proof.context -> (typ list * Proof.context) option) -> |
|
27 |
Context.generic -> Context.generic |
|
28 |
val term_check': int -> string -> |
|
29 |
(term list -> Proof.context -> (term list * Proof.context) option) -> |
|
30 |
Context.generic -> Context.generic |
|
31 |
val typ_uncheck': int -> string -> |
|
32 |
(typ list -> Proof.context -> (typ list * Proof.context) option) -> |
|
33 |
Context.generic -> Context.generic |
|
34 |
val term_uncheck': int -> string -> |
|
35 |
(term list -> Proof.context -> (term list * Proof.context) option) -> |
|
36 |
Context.generic -> Context.generic |
|
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
37 |
end |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
38 |
|
42243 | 39 |
structure Syntax_Phases: SYNTAX_PHASES = |
42241
dd8029f71e1c
separate module for standard implementation of inner syntax operations;
wenzelm
parents:
diff
changeset
|
40 |
struct |
dd8029f71e1c
separate module for standard implementation of inner syntax operations;
wenzelm
parents:
diff
changeset
|
41 |
|
42298
d622145603ee
more accurate markup for syntax consts, notably binders which point back to the original logical entity;
wenzelm
parents:
42296
diff
changeset
|
42 |
(** markup logical entities **) |
d622145603ee
more accurate markup for syntax consts, notably binders which point back to the original logical entity;
wenzelm
parents:
42296
diff
changeset
|
43 |
|
d622145603ee
more accurate markup for syntax consts, notably binders which point back to the original logical entity;
wenzelm
parents:
42296
diff
changeset
|
44 |
fun markup_class ctxt c = |
42379 | 45 |
[Name_Space.markup (Type.class_space (Proof_Context.tsig_of ctxt)) c]; |
42298
d622145603ee
more accurate markup for syntax consts, notably binders which point back to the original logical entity;
wenzelm
parents:
42296
diff
changeset
|
46 |
|
d622145603ee
more accurate markup for syntax consts, notably binders which point back to the original logical entity;
wenzelm
parents:
42296
diff
changeset
|
47 |
fun markup_type ctxt c = |
42379 | 48 |
[Name_Space.markup (Type.type_space (Proof_Context.tsig_of ctxt)) c]; |
42298
d622145603ee
more accurate markup for syntax consts, notably binders which point back to the original logical entity;
wenzelm
parents:
42296
diff
changeset
|
49 |
|
d622145603ee
more accurate markup for syntax consts, notably binders which point back to the original logical entity;
wenzelm
parents:
42296
diff
changeset
|
50 |
fun markup_const ctxt c = |
42379 | 51 |
[Name_Space.markup (Consts.space_of (Proof_Context.consts_of ctxt)) c]; |
42298
d622145603ee
more accurate markup for syntax consts, notably binders which point back to the original logical entity;
wenzelm
parents:
42296
diff
changeset
|
52 |
|
d622145603ee
more accurate markup for syntax consts, notably binders which point back to the original logical entity;
wenzelm
parents:
42296
diff
changeset
|
53 |
fun markup_free ctxt x = |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49690
diff
changeset
|
54 |
[if can Name.dest_skolem x then Markup.skolem else Markup.free] @ |
42493
01430341fc79
more informative markup for fixed variables (via name space entry);
wenzelm
parents:
42488
diff
changeset
|
55 |
(if Variable.is_body ctxt orelse Variable.is_fixed ctxt x |
01430341fc79
more informative markup for fixed variables (via name space entry);
wenzelm
parents:
42488
diff
changeset
|
56 |
then [Variable.markup_fixed ctxt x] |
01430341fc79
more informative markup for fixed variables (via name space entry);
wenzelm
parents:
42488
diff
changeset
|
57 |
else []); |
42298
d622145603ee
more accurate markup for syntax consts, notably binders which point back to the original logical entity;
wenzelm
parents:
42296
diff
changeset
|
58 |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49690
diff
changeset
|
59 |
fun markup_var xi = [Markup.name (Term.string_of_vname xi) Markup.var]; |
42298
d622145603ee
more accurate markup for syntax consts, notably binders which point back to the original logical entity;
wenzelm
parents:
42296
diff
changeset
|
60 |
|
45412 | 61 |
fun markup_bound def ps (name, id) = |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49690
diff
changeset
|
62 |
let val entity = Markup.entity Markup.boundN name in |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49690
diff
changeset
|
63 |
Markup.bound :: |
45412 | 64 |
map (fn pos => Markup.properties (Position.entity_properties_of def id pos) entity) ps |
65 |
end; |
|
42298
d622145603ee
more accurate markup for syntax consts, notably binders which point back to the original logical entity;
wenzelm
parents:
42296
diff
changeset
|
66 |
|
d622145603ee
more accurate markup for syntax consts, notably binders which point back to the original logical entity;
wenzelm
parents:
42296
diff
changeset
|
67 |
fun markup_entity ctxt c = |
42360 | 68 |
(case Syntax.lookup_const (Proof_Context.syn_of ctxt) c of |
42298
d622145603ee
more accurate markup for syntax consts, notably binders which point back to the original logical entity;
wenzelm
parents:
42296
diff
changeset
|
69 |
SOME "" => [] |
d622145603ee
more accurate markup for syntax consts, notably binders which point back to the original logical entity;
wenzelm
parents:
42296
diff
changeset
|
70 |
| SOME b => markup_entity ctxt b |
d622145603ee
more accurate markup for syntax consts, notably binders which point back to the original logical entity;
wenzelm
parents:
42296
diff
changeset
|
71 |
| NONE => c |> Lexicon.unmark |
d622145603ee
more accurate markup for syntax consts, notably binders which point back to the original logical entity;
wenzelm
parents:
42296
diff
changeset
|
72 |
{case_class = markup_class ctxt, |
d622145603ee
more accurate markup for syntax consts, notably binders which point back to the original logical entity;
wenzelm
parents:
42296
diff
changeset
|
73 |
case_type = markup_type ctxt, |
d622145603ee
more accurate markup for syntax consts, notably binders which point back to the original logical entity;
wenzelm
parents:
42296
diff
changeset
|
74 |
case_const = markup_const ctxt, |
d622145603ee
more accurate markup for syntax consts, notably binders which point back to the original logical entity;
wenzelm
parents:
42296
diff
changeset
|
75 |
case_fixed = markup_free ctxt, |
d622145603ee
more accurate markup for syntax consts, notably binders which point back to the original logical entity;
wenzelm
parents:
42296
diff
changeset
|
76 |
case_default = K []}); |
d622145603ee
more accurate markup for syntax consts, notably binders which point back to the original logical entity;
wenzelm
parents:
42296
diff
changeset
|
77 |
|
d622145603ee
more accurate markup for syntax consts, notably binders which point back to the original logical entity;
wenzelm
parents:
42296
diff
changeset
|
78 |
|
d622145603ee
more accurate markup for syntax consts, notably binders which point back to the original logical entity;
wenzelm
parents:
42296
diff
changeset
|
79 |
|
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
80 |
(** decode parse trees **) |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
81 |
|
45427
fca432074fb2
sort assignment before simultaneous term_check, not isolated parse_term;
wenzelm
parents:
45423
diff
changeset
|
82 |
(* decode_sort *) |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
83 |
|
45427
fca432074fb2
sort assignment before simultaneous term_check, not isolated parse_term;
wenzelm
parents:
45423
diff
changeset
|
84 |
fun decode_sort tm = |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
85 |
let |
45427
fca432074fb2
sort assignment before simultaneous term_check, not isolated parse_term;
wenzelm
parents:
45423
diff
changeset
|
86 |
fun err () = raise TERM ("decode_sort: bad encoding of classes", [tm]); |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
87 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
88 |
fun class s = Lexicon.unmark_class s handle Fail _ => err (); |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
89 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
90 |
fun classes (Const (s, _)) = [class s] |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
91 |
| classes (Const ("_classes", _) $ Const (s, _) $ cs) = class s :: classes cs |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
92 |
| classes _ = err (); |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
93 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
94 |
fun sort (Const ("_topsort", _)) = [] |
49674
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
49662
diff
changeset
|
95 |
| sort (Const ("_sort", _) $ cs) = classes cs |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
96 |
| sort (Const (s, _)) = [class s] |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
97 |
| sort _ = err (); |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
98 |
in sort tm end; |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
99 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
100 |
|
45427
fca432074fb2
sort assignment before simultaneous term_check, not isolated parse_term;
wenzelm
parents:
45423
diff
changeset
|
101 |
(* decode_typ *) |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
102 |
|
49685
4341e4d86872
allow position constraints to coexist with 0 or 1 sort constraints;
wenzelm
parents:
49674
diff
changeset
|
103 |
fun decode_pos (Free (s, _)) = |
4341e4d86872
allow position constraints to coexist with 0 or 1 sort constraints;
wenzelm
parents:
49674
diff
changeset
|
104 |
if is_some (Term_Position.decode s) then SOME s else NONE |
4341e4d86872
allow position constraints to coexist with 0 or 1 sort constraints;
wenzelm
parents:
49674
diff
changeset
|
105 |
| decode_pos _ = NONE; |
4341e4d86872
allow position constraints to coexist with 0 or 1 sort constraints;
wenzelm
parents:
49674
diff
changeset
|
106 |
|
45427
fca432074fb2
sort assignment before simultaneous term_check, not isolated parse_term;
wenzelm
parents:
45423
diff
changeset
|
107 |
fun decode_typ tm = |
fca432074fb2
sort assignment before simultaneous term_check, not isolated parse_term;
wenzelm
parents:
45423
diff
changeset
|
108 |
let |
fca432074fb2
sort assignment before simultaneous term_check, not isolated parse_term;
wenzelm
parents:
45423
diff
changeset
|
109 |
fun err () = raise TERM ("decode_typ: bad encoding of type", [tm]); |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
110 |
|
49685
4341e4d86872
allow position constraints to coexist with 0 or 1 sort constraints;
wenzelm
parents:
49674
diff
changeset
|
111 |
fun typ ps sort tm = |
4341e4d86872
allow position constraints to coexist with 0 or 1 sort constraints;
wenzelm
parents:
49674
diff
changeset
|
112 |
(case tm of |
4341e4d86872
allow position constraints to coexist with 0 or 1 sort constraints;
wenzelm
parents:
49674
diff
changeset
|
113 |
Const ("_tfree", _) $ t => typ ps sort t |
4341e4d86872
allow position constraints to coexist with 0 or 1 sort constraints;
wenzelm
parents:
49674
diff
changeset
|
114 |
| Const ("_tvar", _) $ t => typ ps sort t |
4341e4d86872
allow position constraints to coexist with 0 or 1 sort constraints;
wenzelm
parents:
49674
diff
changeset
|
115 |
| Const ("_ofsort", _) $ t $ s => |
4341e4d86872
allow position constraints to coexist with 0 or 1 sort constraints;
wenzelm
parents:
49674
diff
changeset
|
116 |
(case decode_pos s of |
4341e4d86872
allow position constraints to coexist with 0 or 1 sort constraints;
wenzelm
parents:
49674
diff
changeset
|
117 |
SOME p => typ (p :: ps) sort t |
4341e4d86872
allow position constraints to coexist with 0 or 1 sort constraints;
wenzelm
parents:
49674
diff
changeset
|
118 |
| NONE => |
4341e4d86872
allow position constraints to coexist with 0 or 1 sort constraints;
wenzelm
parents:
49674
diff
changeset
|
119 |
if is_none sort then typ ps (SOME (decode_sort s)) t |
4341e4d86872
allow position constraints to coexist with 0 or 1 sort constraints;
wenzelm
parents:
49674
diff
changeset
|
120 |
else err ()) |
4341e4d86872
allow position constraints to coexist with 0 or 1 sort constraints;
wenzelm
parents:
49674
diff
changeset
|
121 |
| Const ("_dummy_ofsort", _) $ s => TFree ("'_dummy_", decode_sort s) |
4341e4d86872
allow position constraints to coexist with 0 or 1 sort constraints;
wenzelm
parents:
49674
diff
changeset
|
122 |
| Free (x, _) => TFree (x, ps @ the_default dummyS sort) |
4341e4d86872
allow position constraints to coexist with 0 or 1 sort constraints;
wenzelm
parents:
49674
diff
changeset
|
123 |
| Var (xi, _) => TVar (xi, ps @ the_default dummyS sort) |
4341e4d86872
allow position constraints to coexist with 0 or 1 sort constraints;
wenzelm
parents:
49674
diff
changeset
|
124 |
| _ => |
4341e4d86872
allow position constraints to coexist with 0 or 1 sort constraints;
wenzelm
parents:
49674
diff
changeset
|
125 |
if null ps andalso is_none sort then |
4341e4d86872
allow position constraints to coexist with 0 or 1 sort constraints;
wenzelm
parents:
49674
diff
changeset
|
126 |
let |
4341e4d86872
allow position constraints to coexist with 0 or 1 sort constraints;
wenzelm
parents:
49674
diff
changeset
|
127 |
val (head, args) = Term.strip_comb tm; |
4341e4d86872
allow position constraints to coexist with 0 or 1 sort constraints;
wenzelm
parents:
49674
diff
changeset
|
128 |
val a = |
4341e4d86872
allow position constraints to coexist with 0 or 1 sort constraints;
wenzelm
parents:
49674
diff
changeset
|
129 |
(case head of |
4341e4d86872
allow position constraints to coexist with 0 or 1 sort constraints;
wenzelm
parents:
49674
diff
changeset
|
130 |
Const (c, _) => (Lexicon.unmark_type c handle Fail _ => err ()) |
4341e4d86872
allow position constraints to coexist with 0 or 1 sort constraints;
wenzelm
parents:
49674
diff
changeset
|
131 |
| _ => err ()); |
4341e4d86872
allow position constraints to coexist with 0 or 1 sort constraints;
wenzelm
parents:
49674
diff
changeset
|
132 |
in Type (a, map (typ [] NONE) args) end |
4341e4d86872
allow position constraints to coexist with 0 or 1 sort constraints;
wenzelm
parents:
49674
diff
changeset
|
133 |
else err ()); |
4341e4d86872
allow position constraints to coexist with 0 or 1 sort constraints;
wenzelm
parents:
49674
diff
changeset
|
134 |
in typ [] NONE tm end; |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
135 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
136 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
137 |
(* parsetree_to_ast *) |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
138 |
|
52188 | 139 |
fun parsetree_to_ast ctxt trf parsetree = |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
140 |
let |
44736 | 141 |
val reports = Unsynchronized.ref ([]: Position.report list); |
44735 | 142 |
fun report pos = Position.store_reports reports [pos]; |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
143 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
144 |
fun trans a args = |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
145 |
(case trf a of |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
146 |
NONE => Ast.mk_appl (Ast.Constant a) args |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
147 |
| SOME f => f ctxt args); |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
148 |
|
49674
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
49662
diff
changeset
|
149 |
fun asts_of_token tok = |
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
49662
diff
changeset
|
150 |
if Lexicon.valued_token tok |
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
49662
diff
changeset
|
151 |
then [Ast.Variable (Lexicon.str_of_token tok)] |
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
49662
diff
changeset
|
152 |
else []; |
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
49662
diff
changeset
|
153 |
|
52162
896ebb4646d8
position constraint for dummy_pattern -- more PIDE markup;
wenzelm
parents:
52160
diff
changeset
|
154 |
fun ast_of_position tok = |
896ebb4646d8
position constraint for dummy_pattern -- more PIDE markup;
wenzelm
parents:
52160
diff
changeset
|
155 |
Ast.Variable (Term_Position.encode (Lexicon.pos_of_token tok)); |
896ebb4646d8
position constraint for dummy_pattern -- more PIDE markup;
wenzelm
parents:
52160
diff
changeset
|
156 |
|
52163
72e83c82c1d4
position constraint for bound dummy -- more PIDE markup;
wenzelm
parents:
52162
diff
changeset
|
157 |
fun ast_of_dummy a tok = |
52188 | 158 |
Ast.Appl [Ast.Constant "_constrain", Ast.Constant a, ast_of_position tok]; |
52163
72e83c82c1d4
position constraint for bound dummy -- more PIDE markup;
wenzelm
parents:
52162
diff
changeset
|
159 |
|
49674
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
49662
diff
changeset
|
160 |
fun asts_of_position c tok = |
52188 | 161 |
[Ast.Appl [Ast.Constant c, ast_of (Parser.Tip tok), ast_of_position tok]] |
49674
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
49662
diff
changeset
|
162 |
|
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
49662
diff
changeset
|
163 |
and asts_of (Parser.Node ("_class_name", [Parser.Tip tok])) = |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
164 |
let |
42470 | 165 |
val pos = Lexicon.pos_of_token tok; |
166 |
val c = Proof_Context.read_class ctxt (Lexicon.str_of_token tok) |
|
48992 | 167 |
handle ERROR msg => error (msg ^ Position.here pos); |
42470 | 168 |
val _ = report pos (markup_class ctxt) c; |
42282
4fa41e068ff0
report literal tokens according to parsetree head;
wenzelm
parents:
42281
diff
changeset
|
169 |
in [Ast.Constant (Lexicon.mark_class c)] end |
4fa41e068ff0
report literal tokens according to parsetree head;
wenzelm
parents:
42281
diff
changeset
|
170 |
| asts_of (Parser.Node ("_type_name", [Parser.Tip tok])) = |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
171 |
let |
42470 | 172 |
val pos = Lexicon.pos_of_token tok; |
173 |
val Type (c, _) = |
|
174 |
Proof_Context.read_type_name_proper ctxt false (Lexicon.str_of_token tok) |
|
48992 | 175 |
handle ERROR msg => error (msg ^ Position.here pos); |
42470 | 176 |
val _ = report pos (markup_type ctxt) c; |
42282
4fa41e068ff0
report literal tokens according to parsetree head;
wenzelm
parents:
42281
diff
changeset
|
177 |
in [Ast.Constant (Lexicon.mark_type c)] end |
49674
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
49662
diff
changeset
|
178 |
| asts_of (Parser.Node ("_position", [Parser.Tip tok])) = asts_of_position "_constrain" tok |
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
49662
diff
changeset
|
179 |
| asts_of (Parser.Node ("_position_sort", [Parser.Tip tok])) = asts_of_position "_ofsort" tok |
52162
896ebb4646d8
position constraint for dummy_pattern -- more PIDE markup;
wenzelm
parents:
52160
diff
changeset
|
180 |
| asts_of (Parser.Node (a as "\\<^const>dummy_pattern", [Parser.Tip tok])) = |
52163
72e83c82c1d4
position constraint for bound dummy -- more PIDE markup;
wenzelm
parents:
52162
diff
changeset
|
181 |
[ast_of_dummy a tok] |
72e83c82c1d4
position constraint for bound dummy -- more PIDE markup;
wenzelm
parents:
52162
diff
changeset
|
182 |
| asts_of (Parser.Node (a as "_idtdummy", [Parser.Tip tok])) = |
72e83c82c1d4
position constraint for bound dummy -- more PIDE markup;
wenzelm
parents:
52162
diff
changeset
|
183 |
[ast_of_dummy a tok] |
72e83c82c1d4
position constraint for bound dummy -- more PIDE markup;
wenzelm
parents:
52162
diff
changeset
|
184 |
| asts_of (Parser.Node ("_idtypdummy", pts as [Parser.Tip tok, _, _])) = |
72e83c82c1d4
position constraint for bound dummy -- more PIDE markup;
wenzelm
parents:
52162
diff
changeset
|
185 |
[Ast.Appl (Ast.Constant "_constrain" :: ast_of_dummy "_idtdummy" tok :: maps asts_of pts)] |
42282
4fa41e068ff0
report literal tokens according to parsetree head;
wenzelm
parents:
42281
diff
changeset
|
186 |
| asts_of (Parser.Node (a, pts)) = |
4fa41e068ff0
report literal tokens according to parsetree head;
wenzelm
parents:
42281
diff
changeset
|
187 |
let |
4fa41e068ff0
report literal tokens according to parsetree head;
wenzelm
parents:
42281
diff
changeset
|
188 |
val _ = pts |> List.app |
4fa41e068ff0
report literal tokens according to parsetree head;
wenzelm
parents:
42281
diff
changeset
|
189 |
(fn Parser.Node _ => () | Parser.Tip tok => |
4fa41e068ff0
report literal tokens according to parsetree head;
wenzelm
parents:
42281
diff
changeset
|
190 |
if Lexicon.valued_token tok then () |
42298
d622145603ee
more accurate markup for syntax consts, notably binders which point back to the original logical entity;
wenzelm
parents:
42296
diff
changeset
|
191 |
else report (Lexicon.pos_of_token tok) (markup_entity ctxt) a); |
42282
4fa41e068ff0
report literal tokens according to parsetree head;
wenzelm
parents:
42281
diff
changeset
|
192 |
in [trans a (maps asts_of pts)] end |
49674
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
49662
diff
changeset
|
193 |
| asts_of (Parser.Tip tok) = asts_of_token tok |
42282
4fa41e068ff0
report literal tokens according to parsetree head;
wenzelm
parents:
42281
diff
changeset
|
194 |
|
4fa41e068ff0
report literal tokens according to parsetree head;
wenzelm
parents:
42281
diff
changeset
|
195 |
and ast_of pt = |
4fa41e068ff0
report literal tokens according to parsetree head;
wenzelm
parents:
42281
diff
changeset
|
196 |
(case asts_of pt of |
4fa41e068ff0
report literal tokens according to parsetree head;
wenzelm
parents:
42281
diff
changeset
|
197 |
[ast] => ast |
4fa41e068ff0
report literal tokens according to parsetree head;
wenzelm
parents:
42281
diff
changeset
|
198 |
| asts => raise Ast.AST ("parsetree_to_ast: malformed parsetree", asts)); |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
199 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
200 |
val ast = Exn.interruptible_capture ast_of parsetree; |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
201 |
in (! reports, ast) end; |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
202 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
203 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
204 |
(* ast_to_term *) |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
205 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
206 |
fun ast_to_term ctxt trf = |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
207 |
let |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
208 |
fun trans a args = |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
209 |
(case trf a of |
42476 | 210 |
NONE => Term.list_comb (Syntax.const a, args) |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
211 |
| SOME f => f ctxt args); |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
212 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
213 |
fun term_of (Ast.Constant a) = trans a [] |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
214 |
| term_of (Ast.Variable x) = Lexicon.read_var x |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
215 |
| term_of (Ast.Appl (Ast.Constant a :: (asts as _ :: _))) = |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
216 |
trans a (map term_of asts) |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
217 |
| term_of (Ast.Appl (ast :: (asts as _ :: _))) = |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
218 |
Term.list_comb (term_of ast, map term_of asts) |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
219 |
| term_of (ast as Ast.Appl _) = raise Ast.AST ("ast_to_term: malformed ast", [ast]); |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
220 |
in term_of end; |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
221 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
222 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
223 |
(* decode_term -- transform parse tree into raw term *) |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
224 |
|
44736 | 225 |
fun decode_term _ (result as (_: Position.report list, Exn.Exn _)) = result |
43761
e72ba84ae58f
tuned signature -- corresponding to Scala version;
wenzelm
parents:
43731
diff
changeset
|
226 |
| decode_term ctxt (reports0, Exn.Res tm) = |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
227 |
let |
42250
cc5ac538f991
eliminated odd object-oriented type_context/term_context;
wenzelm
parents:
42249
diff
changeset
|
228 |
fun get_const a = |
42360 | 229 |
((true, #1 (Term.dest_Const (Proof_Context.read_const_proper ctxt false a))) |
230 |
handle ERROR _ => (false, Consts.intern (Proof_Context.consts_of ctxt) a)); |
|
231 |
val get_free = Proof_Context.intern_skolem ctxt; |
|
42250
cc5ac538f991
eliminated odd object-oriented type_context/term_context;
wenzelm
parents:
42249
diff
changeset
|
232 |
|
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
233 |
val reports = Unsynchronized.ref reports0; |
44735 | 234 |
fun report ps = Position.store_reports reports ps; |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
235 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
236 |
fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) = |
42264 | 237 |
(case Term_Position.decode_position typ of |
45445
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45444
diff
changeset
|
238 |
SOME (p, T) => Type.constraint T (decode (p :: ps) qs bs t) |
45427
fca432074fb2
sort assignment before simultaneous term_check, not isolated parse_term;
wenzelm
parents:
45423
diff
changeset
|
239 |
| NONE => Type.constraint (decode_typ typ) (decode ps qs bs t)) |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
240 |
| decode ps qs bs (Const ("_constrainAbs", _) $ t $ typ) = |
42264 | 241 |
(case Term_Position.decode_position typ of |
45445
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45444
diff
changeset
|
242 |
SOME (q, T) => Type.constraint (T --> dummyT) (decode ps (q :: qs) bs t) |
45427
fca432074fb2
sort assignment before simultaneous term_check, not isolated parse_term;
wenzelm
parents:
45423
diff
changeset
|
243 |
| NONE => Type.constraint (decode_typ typ --> dummyT) (decode ps qs bs t)) |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
244 |
| decode _ qs bs (Abs (x, T, t)) = |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
245 |
let |
45412 | 246 |
val id = serial (); |
247 |
val _ = report qs (markup_bound true qs) (x, id); |
|
248 |
in Abs (x, T, decode [] [] ((qs, (x, id)) :: bs) t) end |
|
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
249 |
| decode _ _ bs (t $ u) = decode [] [] bs t $ decode [] [] bs u |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
250 |
| decode ps _ _ (Const (a, T)) = |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
251 |
(case try Lexicon.unmark_fixed a of |
42282
4fa41e068ff0
report literal tokens according to parsetree head;
wenzelm
parents:
42281
diff
changeset
|
252 |
SOME x => (report ps (markup_free ctxt) x; Free (x, T)) |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
253 |
| NONE => |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
254 |
let |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
255 |
val c = |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
256 |
(case try Lexicon.unmark_const a of |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
257 |
SOME c => c |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
258 |
| NONE => snd (get_const a)); |
42282
4fa41e068ff0
report literal tokens according to parsetree head;
wenzelm
parents:
42281
diff
changeset
|
259 |
val _ = report ps (markup_const ctxt) c; |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
260 |
in Const (c, T) end) |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
261 |
| decode ps _ _ (Free (a, T)) = |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
262 |
(case (get_free a, get_const a) of |
42282
4fa41e068ff0
report literal tokens according to parsetree head;
wenzelm
parents:
42281
diff
changeset
|
263 |
(SOME x, _) => (report ps (markup_free ctxt) x; Free (x, T)) |
4fa41e068ff0
report literal tokens according to parsetree head;
wenzelm
parents:
42281
diff
changeset
|
264 |
| (_, (true, c)) => (report ps (markup_const ctxt) c; Const (c, T)) |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
265 |
| (_, (false, c)) => |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
266 |
if Long_Name.is_qualified c |
42282
4fa41e068ff0
report literal tokens according to parsetree head;
wenzelm
parents:
42281
diff
changeset
|
267 |
then (report ps (markup_const ctxt) c; Const (c, T)) |
4fa41e068ff0
report literal tokens according to parsetree head;
wenzelm
parents:
42281
diff
changeset
|
268 |
else (report ps (markup_free ctxt) c; Free (c, T))) |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
269 |
| decode ps _ _ (Var (xi, T)) = (report ps markup_var xi; Var (xi, T)) |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
270 |
| decode ps _ bs (t as Bound i) = |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
271 |
(case try (nth bs) i of |
45412 | 272 |
SOME (qs, (x, id)) => (report ps (markup_bound false qs) (x, id); t) |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
273 |
| NONE => t); |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
274 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
275 |
val tm' = Exn.interruptible_capture (fn () => decode [] [] [] tm) (); |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
276 |
in (! reports, tm') end; |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
277 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
278 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
279 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
280 |
(** parse **) |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
281 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
282 |
(* results *) |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
283 |
|
43761
e72ba84ae58f
tuned signature -- corresponding to Scala version;
wenzelm
parents:
43731
diff
changeset
|
284 |
fun proper_results results = map_filter (fn (y, Exn.Res x) => SOME (y, x) | _ => NONE) results; |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
285 |
fun failed_results results = map_filter (fn (y, Exn.Exn e) => SOME (y, e) | _ => NONE) results; |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
286 |
|
46512
4f9f61f9b535
simplified configuration options for syntax ambiguity;
wenzelm
parents:
46506
diff
changeset
|
287 |
fun report_result ctxt pos ambig_msgs results = |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
288 |
(case (proper_results results, failed_results results) of |
44736 | 289 |
([], (reports, exn) :: _) => (Context_Position.reports ctxt reports; reraise exn) |
290 |
| ([(reports, x)], _) => (Context_Position.reports ctxt reports; x) |
|
46512
4f9f61f9b535
simplified configuration options for syntax ambiguity;
wenzelm
parents:
46506
diff
changeset
|
291 |
| _ => |
4f9f61f9b535
simplified configuration options for syntax ambiguity;
wenzelm
parents:
46506
diff
changeset
|
292 |
if null ambig_msgs then |
48992 | 293 |
error ("Parse error: ambiguous syntax" ^ Position.here pos) |
46512
4f9f61f9b535
simplified configuration options for syntax ambiguity;
wenzelm
parents:
46506
diff
changeset
|
294 |
else error (cat_lines ambig_msgs)); |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
295 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
296 |
|
42249 | 297 |
(* parse raw asts *) |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
298 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
299 |
fun parse_asts ctxt raw root (syms, pos) = |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
300 |
let |
42360 | 301 |
val syn = Proof_Context.syn_of ctxt; |
42253 | 302 |
val ast_tr = Syntax.parse_ast_translation syn; |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
303 |
|
42251 | 304 |
val toks = Syntax.tokenize syn raw syms; |
44736 | 305 |
val _ = Context_Position.reports ctxt (map Lexicon.report_of_token toks); |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
306 |
|
45641 | 307 |
val pts = Syntax.parse syn root (filter Lexicon.is_proper toks) |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
308 |
handle ERROR msg => |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
309 |
error (msg ^ |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49690
diff
changeset
|
310 |
implode (map (Markup.markup Markup.report o Lexicon.reported_token_range ctxt) toks)); |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
311 |
val len = length pts; |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
312 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
313 |
val limit = Config.get ctxt Syntax.ambiguity_limit; |
46512
4f9f61f9b535
simplified configuration options for syntax ambiguity;
wenzelm
parents:
46506
diff
changeset
|
314 |
val ambig_msgs = |
4f9f61f9b535
simplified configuration options for syntax ambiguity;
wenzelm
parents:
46506
diff
changeset
|
315 |
if len <= 1 then [] |
46506
c7faa011bfa7
simplified configuration options for syntax ambiguity;
wenzelm
parents:
46126
diff
changeset
|
316 |
else |
46512
4f9f61f9b535
simplified configuration options for syntax ambiguity;
wenzelm
parents:
46506
diff
changeset
|
317 |
[cat_lines |
48992 | 318 |
(("Ambiguous input" ^ Position.here (Position.reset_range pos) ^ |
46512
4f9f61f9b535
simplified configuration options for syntax ambiguity;
wenzelm
parents:
46506
diff
changeset
|
319 |
"\nproduces " ^ string_of_int len ^ " parse trees" ^ |
4f9f61f9b535
simplified configuration options for syntax ambiguity;
wenzelm
parents:
46506
diff
changeset
|
320 |
(if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") :: |
52517 | 321 |
map (Pretty.string_of o Pretty.item o single o Parser.pretty_parsetree) |
322 |
(take limit pts))]; |
|
46512
4f9f61f9b535
simplified configuration options for syntax ambiguity;
wenzelm
parents:
46506
diff
changeset
|
323 |
|
52188 | 324 |
in (ambig_msgs, map (parsetree_to_ast ctxt ast_tr) pts) end; |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
325 |
|
46506
c7faa011bfa7
simplified configuration options for syntax ambiguity;
wenzelm
parents:
46126
diff
changeset
|
326 |
fun parse_tree ctxt root input = |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
327 |
let |
42360 | 328 |
val syn = Proof_Context.syn_of ctxt; |
42253 | 329 |
val tr = Syntax.parse_translation syn; |
42255 | 330 |
val parse_rules = Syntax.parse_rules syn; |
46512
4f9f61f9b535
simplified configuration options for syntax ambiguity;
wenzelm
parents:
46506
diff
changeset
|
331 |
val (ambig_msgs, asts) = parse_asts ctxt false root input; |
4f9f61f9b535
simplified configuration options for syntax ambiguity;
wenzelm
parents:
46506
diff
changeset
|
332 |
val results = |
4f9f61f9b535
simplified configuration options for syntax ambiguity;
wenzelm
parents:
46506
diff
changeset
|
333 |
(map o apsnd o Exn.maps_result) |
4f9f61f9b535
simplified configuration options for syntax ambiguity;
wenzelm
parents:
46506
diff
changeset
|
334 |
(Ast.normalize ctxt parse_rules #> Exn.interruptible_capture (ast_to_term ctxt tr)) asts; |
4f9f61f9b535
simplified configuration options for syntax ambiguity;
wenzelm
parents:
46506
diff
changeset
|
335 |
in (ambig_msgs, results) end; |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
336 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
337 |
|
42249 | 338 |
(* parse logical entities *) |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
339 |
|
42241
dd8029f71e1c
separate module for standard implementation of inner syntax operations;
wenzelm
parents:
diff
changeset
|
340 |
fun parse_failed ctxt pos msg kind = |
dd8029f71e1c
separate module for standard implementation of inner syntax operations;
wenzelm
parents:
diff
changeset
|
341 |
cat_error msg ("Failed to parse " ^ kind ^ |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49690
diff
changeset
|
342 |
Markup.markup Markup.report (Context_Position.reported_text ctxt pos Markup.bad "")); |
42241
dd8029f71e1c
separate module for standard implementation of inner syntax operations;
wenzelm
parents:
diff
changeset
|
343 |
|
43731
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
344 |
fun parse_sort ctxt = |
55550 | 345 |
Syntax.parse_token ctxt Term_XML.Decode.sort Markup.language_sort |
43731
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
346 |
(fn (syms, pos) => |
46506
c7faa011bfa7
simplified configuration options for syntax ambiguity;
wenzelm
parents:
46126
diff
changeset
|
347 |
parse_tree ctxt "sort" (syms, pos) |
46512
4f9f61f9b535
simplified configuration options for syntax ambiguity;
wenzelm
parents:
46506
diff
changeset
|
348 |
|> uncurry (report_result ctxt pos) |
45427
fca432074fb2
sort assignment before simultaneous term_check, not isolated parse_term;
wenzelm
parents:
45423
diff
changeset
|
349 |
|> decode_sort |
43731
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
350 |
|> Type.minimize_sort (Proof_Context.tsig_of ctxt) |
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
351 |
handle ERROR msg => parse_failed ctxt pos msg "sort"); |
42241
dd8029f71e1c
separate module for standard implementation of inner syntax operations;
wenzelm
parents:
diff
changeset
|
352 |
|
43731
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
353 |
fun parse_typ ctxt = |
55550 | 354 |
Syntax.parse_token ctxt Term_XML.Decode.typ Markup.language_type |
43731
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
355 |
(fn (syms, pos) => |
46506
c7faa011bfa7
simplified configuration options for syntax ambiguity;
wenzelm
parents:
46126
diff
changeset
|
356 |
parse_tree ctxt "type" (syms, pos) |
46512
4f9f61f9b535
simplified configuration options for syntax ambiguity;
wenzelm
parents:
46506
diff
changeset
|
357 |
|> uncurry (report_result ctxt pos) |
45427
fca432074fb2
sort assignment before simultaneous term_check, not isolated parse_term;
wenzelm
parents:
45423
diff
changeset
|
358 |
|> decode_typ |
43731
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
359 |
handle ERROR msg => parse_failed ctxt pos msg "type"); |
42241
dd8029f71e1c
separate module for standard implementation of inner syntax operations;
wenzelm
parents:
diff
changeset
|
360 |
|
43731
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
361 |
fun parse_term is_prop ctxt = |
42241
dd8029f71e1c
separate module for standard implementation of inner syntax operations;
wenzelm
parents:
diff
changeset
|
362 |
let |
42281 | 363 |
val (markup, kind, root, constrain) = |
364 |
if is_prop |
|
55550 | 365 |
then (Markup.language_prop, "prop", "prop", Type.constraint propT) |
366 |
else (Markup.language_term, "term", Config.get ctxt Syntax.root, I); |
|
43731
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
367 |
val decode = constrain o Term_XML.Decode.term; |
42249 | 368 |
in |
43731
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
369 |
Syntax.parse_token ctxt decode markup |
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
370 |
(fn (syms, pos) => |
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
371 |
let |
46512
4f9f61f9b535
simplified configuration options for syntax ambiguity;
wenzelm
parents:
46506
diff
changeset
|
372 |
val (ambig_msgs, results) = parse_tree ctxt root (syms, pos) ||> map (decode_term ctxt); |
46506
c7faa011bfa7
simplified configuration options for syntax ambiguity;
wenzelm
parents:
46126
diff
changeset
|
373 |
val parsed_len = length (proper_results results); |
42249 | 374 |
|
46512
4f9f61f9b535
simplified configuration options for syntax ambiguity;
wenzelm
parents:
46506
diff
changeset
|
375 |
val ambiguity_warning = Config.get ctxt Syntax.ambiguity_warning; |
43731
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
376 |
val limit = Config.get ctxt Syntax.ambiguity_limit; |
42249 | 377 |
|
43731
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
378 |
(*brute-force disambiguation via type-inference*) |
43761
e72ba84ae58f
tuned signature -- corresponding to Scala version;
wenzelm
parents:
43731
diff
changeset
|
379 |
fun check t = (Syntax.check_term ctxt (constrain t); Exn.Res t) |
43731
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
380 |
handle exn as ERROR _ => Exn.Exn exn; |
42249 | 381 |
|
43731
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
382 |
val results' = |
46506
c7faa011bfa7
simplified configuration options for syntax ambiguity;
wenzelm
parents:
46126
diff
changeset
|
383 |
if parsed_len > 1 then |
46989 | 384 |
(grouped 10 (Par_List.map_name "Syntax_Phases.parse_term") o apsnd o Exn.maps_result) |
43731
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
385 |
check results |
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
386 |
else results; |
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
387 |
val reports' = fst (hd results'); |
42249 | 388 |
|
43731
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
389 |
val errs = map snd (failed_results results'); |
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
390 |
val checked = map snd (proper_results results'); |
46506
c7faa011bfa7
simplified configuration options for syntax ambiguity;
wenzelm
parents:
46126
diff
changeset
|
391 |
val checked_len = length checked; |
42249 | 392 |
|
52517 | 393 |
val pretty_term = Syntax.pretty_term (Config.put Printer.show_brackets true ctxt); |
43731
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
394 |
in |
46506
c7faa011bfa7
simplified configuration options for syntax ambiguity;
wenzelm
parents:
46126
diff
changeset
|
395 |
if checked_len = 0 then |
46512
4f9f61f9b535
simplified configuration options for syntax ambiguity;
wenzelm
parents:
46506
diff
changeset
|
396 |
report_result ctxt pos [] |
4f9f61f9b535
simplified configuration options for syntax ambiguity;
wenzelm
parents:
46506
diff
changeset
|
397 |
[(reports', Exn.Exn (Exn.EXCEPTIONS (map ERROR ambig_msgs @ errs)))] |
46506
c7faa011bfa7
simplified configuration options for syntax ambiguity;
wenzelm
parents:
46126
diff
changeset
|
398 |
else if checked_len = 1 then |
46512
4f9f61f9b535
simplified configuration options for syntax ambiguity;
wenzelm
parents:
46506
diff
changeset
|
399 |
(if parsed_len > 1 andalso ambiguity_warning then |
43731
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
400 |
Context_Position.if_visible ctxt warning |
46512
4f9f61f9b535
simplified configuration options for syntax ambiguity;
wenzelm
parents:
46506
diff
changeset
|
401 |
(cat_lines (ambig_msgs @ |
4f9f61f9b535
simplified configuration options for syntax ambiguity;
wenzelm
parents:
46506
diff
changeset
|
402 |
["Fortunately, only one parse tree is type correct" ^ |
48992 | 403 |
Position.here (Position.reset_range pos) ^ |
46512
4f9f61f9b535
simplified configuration options for syntax ambiguity;
wenzelm
parents:
46506
diff
changeset
|
404 |
",\nbut you may still want to disambiguate your grammar or your input."])) |
4f9f61f9b535
simplified configuration options for syntax ambiguity;
wenzelm
parents:
46506
diff
changeset
|
405 |
else (); report_result ctxt pos [] results') |
43731
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
406 |
else |
46512
4f9f61f9b535
simplified configuration options for syntax ambiguity;
wenzelm
parents:
46506
diff
changeset
|
407 |
report_result ctxt pos [] |
4f9f61f9b535
simplified configuration options for syntax ambiguity;
wenzelm
parents:
46506
diff
changeset
|
408 |
[(reports', Exn.Exn (ERROR (cat_lines (ambig_msgs @ |
4f9f61f9b535
simplified configuration options for syntax ambiguity;
wenzelm
parents:
46506
diff
changeset
|
409 |
(("Ambiguous input\n" ^ string_of_int checked_len ^ " terms are type correct" ^ |
46506
c7faa011bfa7
simplified configuration options for syntax ambiguity;
wenzelm
parents:
46126
diff
changeset
|
410 |
(if checked_len <= limit then "" |
c7faa011bfa7
simplified configuration options for syntax ambiguity;
wenzelm
parents:
46126
diff
changeset
|
411 |
else " (" ^ string_of_int limit ^ " displayed)") ^ ":") :: |
52517 | 412 |
map (Pretty.string_of o Pretty.item o single o pretty_term) |
413 |
(take limit checked))))))] |
|
43731
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
414 |
end handle ERROR msg => parse_failed ctxt pos msg kind) |
42249 | 415 |
end; |
42241
dd8029f71e1c
separate module for standard implementation of inner syntax operations;
wenzelm
parents:
diff
changeset
|
416 |
|
dd8029f71e1c
separate module for standard implementation of inner syntax operations;
wenzelm
parents:
diff
changeset
|
417 |
|
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
418 |
(* parse_ast_pattern *) |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
419 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
420 |
fun parse_ast_pattern ctxt (root, str) = |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
421 |
let |
42360 | 422 |
val syn = Proof_Context.syn_of ctxt; |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
423 |
|
52188 | 424 |
val reports = Unsynchronized.ref ([]: Position.report list); |
425 |
fun report ps = Position.store_reports reports ps; |
|
426 |
||
427 |
fun decode_const ps c = (report ps (markup_entity ctxt) c; Ast.Constant c); |
|
428 |
fun decode_var ps x = (report ps (fn () => [Markup.name x Markup.free]) (); Ast.Variable x); |
|
429 |
fun decode_appl ps asts = Ast.Appl (map (decode ps) asts) |
|
430 |
and decode ps (Ast.Constant c) = decode_const ps c |
|
431 |
| decode ps (Ast.Variable x) = |
|
42298
d622145603ee
more accurate markup for syntax consts, notably binders which point back to the original logical entity;
wenzelm
parents:
42296
diff
changeset
|
432 |
if is_some (Syntax.lookup_const syn x) orelse Long_Name.is_qualified x |
52188 | 433 |
then decode_const ps x |
434 |
else decode_var ps x |
|
435 |
| decode ps (Ast.Appl (asts as (Ast.Constant c :: ast :: Ast.Variable x :: args))) = |
|
436 |
if member (op =) Term_Position.markers c then |
|
437 |
(case Term_Position.decode x of |
|
438 |
SOME p => Ast.mk_appl (decode (p :: ps) ast) (map (decode ps) args) |
|
439 |
| NONE => decode_appl ps asts) |
|
440 |
else decode_appl ps asts |
|
441 |
| decode ps (Ast.Appl asts) = decode_appl ps asts; |
|
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
442 |
|
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55550
diff
changeset
|
443 |
val {text, pos, ...} = Syntax.read_token_source str; |
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55550
diff
changeset
|
444 |
val syms = Symbol_Pos.explode (text, pos); |
52188 | 445 |
val ast = |
446 |
parse_asts ctxt true root (syms, pos) |
|
447 |
|> uncurry (report_result ctxt pos) |
|
448 |
|> decode []; |
|
449 |
val _ = Context_Position.reports ctxt (! reports); |
|
450 |
in ast end; |
|
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
451 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
452 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
453 |
|
42245 | 454 |
(** encode parse trees **) |
455 |
||
456 |
(* term_of_sort *) |
|
457 |
||
458 |
fun term_of_sort S = |
|
459 |
let |
|
42476 | 460 |
val class = Syntax.const o Lexicon.mark_class; |
42245 | 461 |
|
462 |
fun classes [c] = class c |
|
42476 | 463 |
| classes (c :: cs) = Syntax.const "_classes" $ class c $ classes cs; |
42245 | 464 |
in |
465 |
(case S of |
|
42476 | 466 |
[] => Syntax.const "_topsort" |
42245 | 467 |
| [c] => class c |
42476 | 468 |
| cs => Syntax.const "_sort" $ classes cs) |
42245 | 469 |
end; |
470 |
||
471 |
||
472 |
(* term_of_typ *) |
|
473 |
||
42247
12fe41a92cd5
typed_print_translation: discontinued show_sorts argument;
wenzelm
parents:
42245
diff
changeset
|
474 |
fun term_of_typ ctxt ty = |
42245 | 475 |
let |
52210
0226035df99d
more explicit Printer.type_emphasis, depending on show_type_emphasis;
wenzelm
parents:
52188
diff
changeset
|
476 |
val show_sorts = Config.get ctxt show_sorts orelse Config.get ctxt show_markup; |
42247
12fe41a92cd5
typed_print_translation: discontinued show_sorts argument;
wenzelm
parents:
42245
diff
changeset
|
477 |
|
49686
678aa92e921c
printed "_ofsort" is subject to show_markup as well;
wenzelm
parents:
49685
diff
changeset
|
478 |
fun ofsort t raw_S = |
52210
0226035df99d
more explicit Printer.type_emphasis, depending on show_type_emphasis;
wenzelm
parents:
52188
diff
changeset
|
479 |
if show_sorts then |
49686
678aa92e921c
printed "_ofsort" is subject to show_markup as well;
wenzelm
parents:
49685
diff
changeset
|
480 |
let val S = #2 (Term_Position.decode_positionS raw_S) |
678aa92e921c
printed "_ofsort" is subject to show_markup as well;
wenzelm
parents:
49685
diff
changeset
|
481 |
in if S = dummyS then t else Syntax.const "_ofsort" $ t $ term_of_sort S end |
42245 | 482 |
else t; |
483 |
||
484 |
fun term_of (Type (a, Ts)) = |
|
42476 | 485 |
Term.list_comb (Syntax.const (Lexicon.mark_type a), map term_of Ts) |
42245 | 486 |
| term_of (TFree (x, S)) = |
42290
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42289
diff
changeset
|
487 |
if is_some (Term_Position.decode x) then Syntax.free x |
49686
678aa92e921c
printed "_ofsort" is subject to show_markup as well;
wenzelm
parents:
49685
diff
changeset
|
488 |
else ofsort (Syntax.const "_tfree" $ Syntax.free x) S |
678aa92e921c
printed "_ofsort" is subject to show_markup as well;
wenzelm
parents:
49685
diff
changeset
|
489 |
| term_of (TVar (xi, S)) = ofsort (Syntax.const "_tvar" $ Syntax.var xi) S; |
42245 | 490 |
in term_of ty end; |
491 |
||
492 |
||
493 |
(* simple_ast_of *) |
|
494 |
||
495 |
fun simple_ast_of ctxt = |
|
496 |
let |
|
497 |
val tune_var = if Config.get ctxt show_question_marks then I else unprefix "?"; |
|
498 |
fun ast_of (Const (c, _)) = Ast.Constant c |
|
499 |
| ast_of (Free (x, _)) = Ast.Variable x |
|
500 |
| ast_of (Var (xi, _)) = Ast.Variable (tune_var (Term.string_of_vname xi)) |
|
501 |
| ast_of (t as _ $ _) = |
|
502 |
let val (f, args) = strip_comb t |
|
503 |
in Ast.mk_appl (ast_of f) (map ast_of args) end |
|
42408 | 504 |
| ast_of (Bound i) = Ast.Appl [Ast.Constant "_loose", Ast.Variable ("B." ^ string_of_int i)] |
42245 | 505 |
| ast_of (Abs _) = raise Fail "simple_ast_of: Abs"; |
506 |
in ast_of end; |
|
507 |
||
508 |
||
509 |
(* sort_to_ast and typ_to_ast *) |
|
510 |
||
511 |
fun ast_of_termT ctxt trf tm = |
|
512 |
let |
|
513 |
val ctxt' = Config.put show_sorts false ctxt; |
|
514 |
fun ast_of (t as Const ("_tfree", _) $ Free _) = simple_ast_of ctxt t |
|
515 |
| ast_of (t as Const ("_tvar", _) $ Var _) = simple_ast_of ctxt t |
|
516 |
| ast_of (Const (a, _)) = trans a [] |
|
517 |
| ast_of (t as _ $ _) = |
|
518 |
(case strip_comb t of |
|
519 |
(Const (a, _), args) => trans a args |
|
520 |
| (f, args) => Ast.Appl (map ast_of (f :: args))) |
|
521 |
| ast_of t = simple_ast_of ctxt t |
|
42254 | 522 |
and trans a args = ast_of (trf a ctxt' dummyT args) |
523 |
handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args); |
|
42245 | 524 |
in ast_of tm end; |
525 |
||
526 |
fun sort_to_ast ctxt trf S = ast_of_termT ctxt trf (term_of_sort S); |
|
42247
12fe41a92cd5
typed_print_translation: discontinued show_sorts argument;
wenzelm
parents:
42245
diff
changeset
|
527 |
fun typ_to_ast ctxt trf T = ast_of_termT ctxt trf (term_of_typ ctxt T); |
42245 | 528 |
|
529 |
||
530 |
(* term_to_ast *) |
|
531 |
||
52177 | 532 |
local |
533 |
||
534 |
fun mark_aprop tm = |
|
535 |
let |
|
536 |
fun aprop t = Syntax.const "_aprop" $ t; |
|
537 |
||
538 |
fun is_prop Ts t = |
|
52464
36497ee02ed8
clarified printing of type constraints vs. annotations, notably in goal display with its Type_Annotation.ignore_free_types;
wenzelm
parents:
52219
diff
changeset
|
539 |
Type_Annotation.clean (Type_Annotation.fastype_of Ts t) = propT |
36497ee02ed8
clarified printing of type constraints vs. annotations, notably in goal display with its Type_Annotation.ignore_free_types;
wenzelm
parents:
52219
diff
changeset
|
540 |
handle TERM _ => false; |
52177 | 541 |
|
542 |
fun is_term (Const ("Pure.term", _) $ _) = true |
|
543 |
| is_term _ = false; |
|
544 |
||
545 |
fun mark _ (t as Const _) = t |
|
546 |
| mark Ts (t as Const ("_bound", _) $ u) = if is_prop Ts u then aprop t else t |
|
52464
36497ee02ed8
clarified printing of type constraints vs. annotations, notably in goal display with its Type_Annotation.ignore_free_types;
wenzelm
parents:
52219
diff
changeset
|
547 |
| mark Ts (t as Free _) = if is_prop Ts t then aprop t else t |
36497ee02ed8
clarified printing of type constraints vs. annotations, notably in goal display with its Type_Annotation.ignore_free_types;
wenzelm
parents:
52219
diff
changeset
|
548 |
| mark Ts (t as Var _) = if is_prop Ts t then aprop t else t |
52177 | 549 |
| mark Ts (t as Bound _) = if is_prop Ts t then aprop t else t |
550 |
| mark Ts (Abs (x, T, t)) = Abs (x, T, mark (T :: Ts) t) |
|
551 |
| mark Ts (t as t1 $ (t2 as Const ("TYPE", Type ("itself", [T])))) = |
|
552 |
if is_prop Ts t andalso not (is_term t) then Const ("_type_prop", T) $ mark Ts t1 |
|
553 |
else mark Ts t1 $ mark Ts t2 |
|
554 |
| mark Ts (t as t1 $ t2) = |
|
555 |
(if is_Const (Term.head_of t) orelse not (is_prop Ts t) then I else aprop) |
|
556 |
(mark Ts t1 $ mark Ts t2); |
|
557 |
in mark [] tm end; |
|
558 |
||
52186 | 559 |
fun prune_types ctxt tm = |
42245 | 560 |
let |
52211
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
52210
diff
changeset
|
561 |
fun regard t t' seen = |
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
52210
diff
changeset
|
562 |
if Type_Annotation.is_omitted (Type_Annotation.fastype_of [] t) then (t, seen) |
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
52210
diff
changeset
|
563 |
else if member (op aconv) seen t then (t', seen) |
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
52210
diff
changeset
|
564 |
else (t, t :: seen); |
42245 | 565 |
|
52211
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
52210
diff
changeset
|
566 |
fun prune (t as Const _, seen) = (t, seen) |
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
52210
diff
changeset
|
567 |
| prune (t as Free (x, T), seen) = regard t (Free (x, Type_Annotation.ignore_type T)) seen |
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
52210
diff
changeset
|
568 |
| prune (t as Var (xi, T), seen) = regard t (Var (xi, Type_Annotation.ignore_type T)) seen |
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
52210
diff
changeset
|
569 |
| prune (t as Bound _, seen) = (t, seen) |
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
52210
diff
changeset
|
570 |
| prune (Abs (x, T, t), seen) = |
52186 | 571 |
let val (t', seen') = prune (t, seen); |
52211
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
52210
diff
changeset
|
572 |
in (Abs (x, T, t'), seen') end |
52186 | 573 |
| prune (t1 $ t2, seen) = |
52177 | 574 |
let |
52186 | 575 |
val (t1', seen') = prune (t1, seen); |
576 |
val (t2', seen'') = prune (t2, seen'); |
|
52177 | 577 |
in (t1' $ t2', seen'') end; |
52186 | 578 |
in #1 (prune (tm, [])) end; |
52177 | 579 |
|
52186 | 580 |
fun mark_atoms {structs, fixes} is_syntax_const ctxt tm = |
581 |
let |
|
582 |
val show_structs = Config.get ctxt show_structs; |
|
583 |
||
584 |
fun mark ((t as Const (c, _)) $ u) = |
|
52160 | 585 |
if member (op =) Pure_Thy.token_markers c |
52186 | 586 |
then t $ u else mark t $ mark u |
587 |
| mark (t $ u) = mark t $ mark u |
|
588 |
| mark (Abs (x, T, t)) = Abs (x, T, mark t) |
|
589 |
| mark (t as Const (c, T)) = |
|
42252 | 590 |
if is_syntax_const c then t |
42245 | 591 |
else Const (Lexicon.mark_const c, T) |
52186 | 592 |
| mark (t as Free (x, T)) = |
42245 | 593 |
let val i = find_index (fn s => s = x) structs + 1 in |
594 |
if i = 0 andalso member (op =) fixes x then |
|
595 |
Const (Lexicon.mark_fixed x, T) |
|
596 |
else if i = 1 andalso not show_structs then |
|
42476 | 597 |
Syntax.const "_struct" $ Syntax.const "_indexdefault" |
598 |
else Syntax.const "_free" $ t |
|
42245 | 599 |
end |
52186 | 600 |
| mark (t as Var (xi, T)) = |
42288
2074b31650e6
discontinued special treatment of structure Syntax_Ext (formerly Syn_Ext);
wenzelm
parents:
42284
diff
changeset
|
601 |
if xi = Syntax_Ext.dddot_indexname then Const ("_DDDOT", T) |
42476 | 602 |
else Syntax.const "_var" $ t |
52186 | 603 |
| mark a = a; |
604 |
in mark tm end; |
|
605 |
||
606 |
in |
|
607 |
||
608 |
fun term_to_ast idents is_syntax_const ctxt trf tm = |
|
609 |
let |
|
610 |
val show_types = Config.get ctxt show_types orelse Config.get ctxt show_sorts; |
|
611 |
val show_markup = Config.get ctxt show_markup; |
|
42245 | 612 |
|
613 |
fun ast_of tm = |
|
614 |
(case strip_comb tm of |
|
42284 | 615 |
(t as Abs _, ts) => Ast.mk_appl (ast_of (Syntax_Trans.abs_tr' ctxt t)) (map ast_of ts) |
42245 | 616 |
| ((c as Const ("_free", _)), Free (x, T) :: ts) => |
42290
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42289
diff
changeset
|
617 |
Ast.mk_appl (constrain (c $ Syntax.free x) T) (map ast_of ts) |
42245 | 618 |
| ((c as Const ("_var", _)), Var (xi, T) :: ts) => |
42290
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42289
diff
changeset
|
619 |
Ast.mk_appl (constrain (c $ Syntax.var xi) T) (map ast_of ts) |
49660
de49d9b4d7bc
more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
wenzelm
parents:
49659
diff
changeset
|
620 |
| ((c as Const ("_bound", B)), Free (x, T) :: ts) => |
de49d9b4d7bc
more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
wenzelm
parents:
49659
diff
changeset
|
621 |
let |
de49d9b4d7bc
more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
wenzelm
parents:
49659
diff
changeset
|
622 |
val X = |
de49d9b4d7bc
more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
wenzelm
parents:
49659
diff
changeset
|
623 |
if show_markup andalso not show_types orelse B <> dummyT then T |
de49d9b4d7bc
more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
wenzelm
parents:
49659
diff
changeset
|
624 |
else dummyT; |
de49d9b4d7bc
more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
wenzelm
parents:
49659
diff
changeset
|
625 |
in Ast.mk_appl (constrain (c $ Syntax.free x) X) (map ast_of ts) end |
42245 | 626 |
| (Const ("_idtdummy", T), ts) => |
42476 | 627 |
Ast.mk_appl (constrain (Syntax.const "_idtdummy") T) (map ast_of ts) |
52219
c8ee9c0a3a64
observe type annotations in print translations as well, notably type_constraint_tr';
wenzelm
parents:
52211
diff
changeset
|
628 |
| (const as Const (c, T), ts) => trans c (Type_Annotation.smash T) ts |
42245 | 629 |
| (t, ts) => Ast.mk_appl (simple_ast_of ctxt t) (map ast_of ts)) |
630 |
||
42254 | 631 |
and trans a T args = ast_of (trf a ctxt T args) |
632 |
handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args) |
|
42245 | 633 |
|
52211
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
52210
diff
changeset
|
634 |
and constrain t T0 = |
52464
36497ee02ed8
clarified printing of type constraints vs. annotations, notably in goal display with its Type_Annotation.ignore_free_types;
wenzelm
parents:
52219
diff
changeset
|
635 |
let |
36497ee02ed8
clarified printing of type constraints vs. annotations, notably in goal display with its Type_Annotation.ignore_free_types;
wenzelm
parents:
52219
diff
changeset
|
636 |
val T = |
36497ee02ed8
clarified printing of type constraints vs. annotations, notably in goal display with its Type_Annotation.ignore_free_types;
wenzelm
parents:
52219
diff
changeset
|
637 |
if show_markup andalso not show_types |
36497ee02ed8
clarified printing of type constraints vs. annotations, notably in goal display with its Type_Annotation.ignore_free_types;
wenzelm
parents:
52219
diff
changeset
|
638 |
then Type_Annotation.clean T0 |
36497ee02ed8
clarified printing of type constraints vs. annotations, notably in goal display with its Type_Annotation.ignore_free_types;
wenzelm
parents:
52219
diff
changeset
|
639 |
else Type_Annotation.smash T0; |
36497ee02ed8
clarified printing of type constraints vs. annotations, notably in goal display with its Type_Annotation.ignore_free_types;
wenzelm
parents:
52219
diff
changeset
|
640 |
in |
52211
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
52210
diff
changeset
|
641 |
if (show_types orelse show_markup) andalso T <> dummyT then |
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
52210
diff
changeset
|
642 |
Ast.Appl [Ast.Constant "_constrain", simple_ast_of ctxt t, |
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
52210
diff
changeset
|
643 |
ast_of_termT ctxt trf (term_of_typ ctxt T)] |
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
52210
diff
changeset
|
644 |
else simple_ast_of ctxt t |
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
52210
diff
changeset
|
645 |
end; |
42245 | 646 |
in |
647 |
tm |
|
52177 | 648 |
|> mark_aprop |
52186 | 649 |
|> show_types ? prune_types ctxt |
55014
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
53171
diff
changeset
|
650 |
|> Variable.revert_bounds ctxt |
52186 | 651 |
|> mark_atoms idents is_syntax_const ctxt |
42245 | 652 |
|> ast_of |
653 |
end; |
|
654 |
||
52177 | 655 |
end; |
656 |
||
42245 | 657 |
|
658 |
||
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
659 |
(** unparse **) |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
660 |
|
42245 | 661 |
local |
662 |
||
42267
9566078ad905
simplified printer context: uniform externing and static token translations;
wenzelm
parents:
42264
diff
changeset
|
663 |
fun free_or_skolem ctxt x = |
9566078ad905
simplified printer context: uniform externing and static token translations;
wenzelm
parents:
42264
diff
changeset
|
664 |
let |
9566078ad905
simplified printer context: uniform externing and static token translations;
wenzelm
parents:
42264
diff
changeset
|
665 |
val m = |
9566078ad905
simplified printer context: uniform externing and static token translations;
wenzelm
parents:
42264
diff
changeset
|
666 |
if Variable.is_fixed ctxt x orelse Syntax.is_pretty_global ctxt |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49690
diff
changeset
|
667 |
then Markup.fixed x else Markup.intensify; |
42267
9566078ad905
simplified printer context: uniform externing and static token translations;
wenzelm
parents:
42264
diff
changeset
|
668 |
in |
9566078ad905
simplified printer context: uniform externing and static token translations;
wenzelm
parents:
42264
diff
changeset
|
669 |
if can Name.dest_skolem x |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49690
diff
changeset
|
670 |
then ([m, Markup.skolem], Variable.revert_fixed ctxt x) |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49690
diff
changeset
|
671 |
else ([m, Markup.free], x) |
42267
9566078ad905
simplified printer context: uniform externing and static token translations;
wenzelm
parents:
42264
diff
changeset
|
672 |
end; |
9566078ad905
simplified printer context: uniform externing and static token translations;
wenzelm
parents:
42264
diff
changeset
|
673 |
|
9566078ad905
simplified printer context: uniform externing and static token translations;
wenzelm
parents:
42264
diff
changeset
|
674 |
fun var_or_skolem s = |
9566078ad905
simplified printer context: uniform externing and static token translations;
wenzelm
parents:
42264
diff
changeset
|
675 |
(case Lexicon.read_variable s of |
9566078ad905
simplified printer context: uniform externing and static token translations;
wenzelm
parents:
42264
diff
changeset
|
676 |
SOME (x, i) => |
9566078ad905
simplified printer context: uniform externing and static token translations;
wenzelm
parents:
42264
diff
changeset
|
677 |
(case try Name.dest_skolem x of |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49690
diff
changeset
|
678 |
NONE => (Markup.var, s) |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49690
diff
changeset
|
679 |
| SOME x' => (Markup.skolem, Term.string_of_vname (x', i))) |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49690
diff
changeset
|
680 |
| NONE => (Markup.var, s)); |
42267
9566078ad905
simplified printer context: uniform externing and static token translations;
wenzelm
parents:
42264
diff
changeset
|
681 |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49690
diff
changeset
|
682 |
val typing_elem = YXML.output_markup_elem Markup.typing; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49690
diff
changeset
|
683 |
val sorting_elem = YXML.output_markup_elem Markup.sorting; |
49657
40e4feac2921
turn constraints into Isabelle_Markup.typing, depending on show_markup options;
wenzelm
parents:
49655
diff
changeset
|
684 |
|
42267
9566078ad905
simplified printer context: uniform externing and static token translations;
wenzelm
parents:
42264
diff
changeset
|
685 |
fun unparse_t t_to_ast prt_t markup ctxt t = |
42245 | 686 |
let |
49686
678aa92e921c
printed "_ofsort" is subject to show_markup as well;
wenzelm
parents:
49685
diff
changeset
|
687 |
val show_markup = Config.get ctxt show_markup; |
678aa92e921c
printed "_ofsort" is subject to show_markup as well;
wenzelm
parents:
49685
diff
changeset
|
688 |
val show_sorts = Config.get ctxt show_sorts; |
52185 | 689 |
val show_types = Config.get ctxt show_types orelse show_sorts; |
49657
40e4feac2921
turn constraints into Isabelle_Markup.typing, depending on show_markup options;
wenzelm
parents:
49655
diff
changeset
|
690 |
|
42360 | 691 |
val syn = Proof_Context.syn_of ctxt; |
49657
40e4feac2921
turn constraints into Isabelle_Markup.typing, depending on show_markup options;
wenzelm
parents:
49655
diff
changeset
|
692 |
val prtabs = Syntax.prtabs syn; |
40e4feac2921
turn constraints into Isabelle_Markup.typing, depending on show_markup options;
wenzelm
parents:
49655
diff
changeset
|
693 |
val trf = Syntax.print_ast_translation syn; |
40e4feac2921
turn constraints into Isabelle_Markup.typing, depending on show_markup options;
wenzelm
parents:
49655
diff
changeset
|
694 |
|
40e4feac2921
turn constraints into Isabelle_Markup.typing, depending on show_markup options;
wenzelm
parents:
49655
diff
changeset
|
695 |
fun markup_extern c = |
40e4feac2921
turn constraints into Isabelle_Markup.typing, depending on show_markup options;
wenzelm
parents:
49655
diff
changeset
|
696 |
(case Syntax.lookup_const syn c of |
40e4feac2921
turn constraints into Isabelle_Markup.typing, depending on show_markup options;
wenzelm
parents:
49655
diff
changeset
|
697 |
SOME "" => ([], c) |
40e4feac2921
turn constraints into Isabelle_Markup.typing, depending on show_markup options;
wenzelm
parents:
49655
diff
changeset
|
698 |
| SOME b => markup_extern b |
40e4feac2921
turn constraints into Isabelle_Markup.typing, depending on show_markup options;
wenzelm
parents:
49655
diff
changeset
|
699 |
| NONE => c |> Lexicon.unmark |
40e4feac2921
turn constraints into Isabelle_Markup.typing, depending on show_markup options;
wenzelm
parents:
49655
diff
changeset
|
700 |
{case_class = fn x => (markup_class ctxt x, Proof_Context.extern_class ctxt x), |
40e4feac2921
turn constraints into Isabelle_Markup.typing, depending on show_markup options;
wenzelm
parents:
49655
diff
changeset
|
701 |
case_type = fn x => (markup_type ctxt x, Proof_Context.extern_type ctxt x), |
40e4feac2921
turn constraints into Isabelle_Markup.typing, depending on show_markup options;
wenzelm
parents:
49655
diff
changeset
|
702 |
case_const = fn x => (markup_const ctxt x, Proof_Context.extern_const ctxt x), |
40e4feac2921
turn constraints into Isabelle_Markup.typing, depending on show_markup options;
wenzelm
parents:
49655
diff
changeset
|
703 |
case_fixed = fn x => free_or_skolem ctxt x, |
40e4feac2921
turn constraints into Isabelle_Markup.typing, depending on show_markup options;
wenzelm
parents:
49655
diff
changeset
|
704 |
case_default = fn x => ([], x)}); |
42267
9566078ad905
simplified printer context: uniform externing and static token translations;
wenzelm
parents:
42264
diff
changeset
|
705 |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49690
diff
changeset
|
706 |
fun token_trans "_tfree" x = SOME (Pretty.mark_str (Markup.tfree, x)) |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49690
diff
changeset
|
707 |
| token_trans "_tvar" x = SOME (Pretty.mark_str (Markup.tvar, x)) |
42267
9566078ad905
simplified printer context: uniform externing and static token translations;
wenzelm
parents:
42264
diff
changeset
|
708 |
| token_trans "_free" x = SOME (Pretty.marks_str (free_or_skolem ctxt x)) |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49690
diff
changeset
|
709 |
| token_trans "_bound" x = SOME (Pretty.mark_str (Markup.bound, x)) |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49690
diff
changeset
|
710 |
| token_trans "_loose" x = SOME (Pretty.mark_str (Markup.bad, x)) |
42267
9566078ad905
simplified printer context: uniform externing and static token translations;
wenzelm
parents:
42264
diff
changeset
|
711 |
| token_trans "_var" x = SOME (Pretty.mark_str (var_or_skolem x)) |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49690
diff
changeset
|
712 |
| token_trans "_numeral" x = SOME (Pretty.mark_str (Markup.numeral, x)) |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49690
diff
changeset
|
713 |
| token_trans "_inner_string" x = SOME (Pretty.mark_str (Markup.inner_string, x)) |
42267
9566078ad905
simplified printer context: uniform externing and static token translations;
wenzelm
parents:
42264
diff
changeset
|
714 |
| token_trans _ _ = NONE; |
9566078ad905
simplified printer context: uniform externing and static token translations;
wenzelm
parents:
42264
diff
changeset
|
715 |
|
49655 | 716 |
fun markup_trans a [Ast.Variable x] = token_trans a x |
49662
de6be6922c19
proper handling of constraints stemming from idtyp_ast_tr';
wenzelm
parents:
49660
diff
changeset
|
717 |
| markup_trans "_constrain" [t, ty] = constrain_trans t ty |
de6be6922c19
proper handling of constraints stemming from idtyp_ast_tr';
wenzelm
parents:
49660
diff
changeset
|
718 |
| markup_trans "_idtyp" [t, ty] = constrain_trans t ty |
49686
678aa92e921c
printed "_ofsort" is subject to show_markup as well;
wenzelm
parents:
49685
diff
changeset
|
719 |
| markup_trans "_ofsort" [ty, s] = ofsort_trans ty s |
49657
40e4feac2921
turn constraints into Isabelle_Markup.typing, depending on show_markup options;
wenzelm
parents:
49655
diff
changeset
|
720 |
| markup_trans _ _ = NONE |
49655 | 721 |
|
49662
de6be6922c19
proper handling of constraints stemming from idtyp_ast_tr';
wenzelm
parents:
49660
diff
changeset
|
722 |
and constrain_trans t ty = |
49686
678aa92e921c
printed "_ofsort" is subject to show_markup as well;
wenzelm
parents:
49685
diff
changeset
|
723 |
if show_markup andalso not show_types then |
49662
de6be6922c19
proper handling of constraints stemming from idtyp_ast_tr';
wenzelm
parents:
49660
diff
changeset
|
724 |
let |
de6be6922c19
proper handling of constraints stemming from idtyp_ast_tr';
wenzelm
parents:
49660
diff
changeset
|
725 |
val ((bg1, bg2), en) = typing_elem; |
de6be6922c19
proper handling of constraints stemming from idtyp_ast_tr';
wenzelm
parents:
49660
diff
changeset
|
726 |
val bg = bg1 ^ Pretty.symbolic_output (pretty_typ_ast Markup.empty ty) ^ bg2; |
de6be6922c19
proper handling of constraints stemming from idtyp_ast_tr';
wenzelm
parents:
49660
diff
changeset
|
727 |
in SOME (Pretty.raw_markup (bg, en) (0, [pretty_ast Markup.empty t])) end |
de6be6922c19
proper handling of constraints stemming from idtyp_ast_tr';
wenzelm
parents:
49660
diff
changeset
|
728 |
else NONE |
de6be6922c19
proper handling of constraints stemming from idtyp_ast_tr';
wenzelm
parents:
49660
diff
changeset
|
729 |
|
49686
678aa92e921c
printed "_ofsort" is subject to show_markup as well;
wenzelm
parents:
49685
diff
changeset
|
730 |
and ofsort_trans ty s = |
678aa92e921c
printed "_ofsort" is subject to show_markup as well;
wenzelm
parents:
49685
diff
changeset
|
731 |
if show_markup andalso not show_sorts then |
678aa92e921c
printed "_ofsort" is subject to show_markup as well;
wenzelm
parents:
49685
diff
changeset
|
732 |
let |
678aa92e921c
printed "_ofsort" is subject to show_markup as well;
wenzelm
parents:
49685
diff
changeset
|
733 |
val ((bg1, bg2), en) = sorting_elem; |
678aa92e921c
printed "_ofsort" is subject to show_markup as well;
wenzelm
parents:
49685
diff
changeset
|
734 |
val bg = bg1 ^ Pretty.symbolic_output (pretty_typ_ast Markup.empty s) ^ bg2; |
678aa92e921c
printed "_ofsort" is subject to show_markup as well;
wenzelm
parents:
49685
diff
changeset
|
735 |
in SOME (Pretty.raw_markup (bg, en) (0, [pretty_typ_ast Markup.empty ty])) end |
678aa92e921c
printed "_ofsort" is subject to show_markup as well;
wenzelm
parents:
49685
diff
changeset
|
736 |
else NONE |
678aa92e921c
printed "_ofsort" is subject to show_markup as well;
wenzelm
parents:
49685
diff
changeset
|
737 |
|
49657
40e4feac2921
turn constraints into Isabelle_Markup.typing, depending on show_markup options;
wenzelm
parents:
49655
diff
changeset
|
738 |
and pretty_typ_ast m ast = ast |
40e4feac2921
turn constraints into Isabelle_Markup.typing, depending on show_markup options;
wenzelm
parents:
49655
diff
changeset
|
739 |
|> Printer.pretty_typ_ast ctxt prtabs trf markup_trans markup_extern |
40e4feac2921
turn constraints into Isabelle_Markup.typing, depending on show_markup options;
wenzelm
parents:
49655
diff
changeset
|
740 |
|> Pretty.markup m |
40e4feac2921
turn constraints into Isabelle_Markup.typing, depending on show_markup options;
wenzelm
parents:
49655
diff
changeset
|
741 |
|
40e4feac2921
turn constraints into Isabelle_Markup.typing, depending on show_markup options;
wenzelm
parents:
49655
diff
changeset
|
742 |
and pretty_ast m ast = ast |
40e4feac2921
turn constraints into Isabelle_Markup.typing, depending on show_markup options;
wenzelm
parents:
49655
diff
changeset
|
743 |
|> prt_t ctxt prtabs trf markup_trans markup_extern |
40e4feac2921
turn constraints into Isabelle_Markup.typing, depending on show_markup options;
wenzelm
parents:
49655
diff
changeset
|
744 |
|> Pretty.markup m; |
42245 | 745 |
in |
42255 | 746 |
t_to_ast ctxt (Syntax.print_translation syn) t |
747 |
|> Ast.normalize ctxt (Syntax.print_rules syn) |
|
49657
40e4feac2921
turn constraints into Isabelle_Markup.typing, depending on show_markup options;
wenzelm
parents:
49655
diff
changeset
|
748 |
|> pretty_ast markup |
42245 | 749 |
end; |
750 |
||
751 |
in |
|
752 |
||
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55550
diff
changeset
|
753 |
val unparse_sort = unparse_t sort_to_ast Printer.pretty_typ_ast (Markup.language_sort false); |
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55550
diff
changeset
|
754 |
val unparse_typ = unparse_t typ_to_ast Printer.pretty_typ_ast (Markup.language_type false); |
42241
dd8029f71e1c
separate module for standard implementation of inner syntax operations;
wenzelm
parents:
diff
changeset
|
755 |
|
dd8029f71e1c
separate module for standard implementation of inner syntax operations;
wenzelm
parents:
diff
changeset
|
756 |
fun unparse_term ctxt = |
dd8029f71e1c
separate module for standard implementation of inner syntax operations;
wenzelm
parents:
diff
changeset
|
757 |
let |
42360 | 758 |
val thy = Proof_Context.theory_of ctxt; |
759 |
val syn = Proof_Context.syn_of ctxt; |
|
760 |
val idents = Local_Syntax.idents_of (Proof_Context.syntax_of ctxt); |
|
42241
dd8029f71e1c
separate module for standard implementation of inner syntax operations;
wenzelm
parents:
diff
changeset
|
761 |
in |
42298
d622145603ee
more accurate markup for syntax consts, notably binders which point back to the original logical entity;
wenzelm
parents:
42296
diff
changeset
|
762 |
unparse_t (term_to_ast idents (is_some o Syntax.lookup_const syn)) |
42267
9566078ad905
simplified printer context: uniform externing and static token translations;
wenzelm
parents:
42264
diff
changeset
|
763 |
(Printer.pretty_term_ast (not (Pure_Thy.old_appl_syntax thy))) |
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55550
diff
changeset
|
764 |
(Markup.language_term false) ctxt |
42241
dd8029f71e1c
separate module for standard implementation of inner syntax operations;
wenzelm
parents:
diff
changeset
|
765 |
end; |
dd8029f71e1c
separate module for standard implementation of inner syntax operations;
wenzelm
parents:
diff
changeset
|
766 |
|
42249 | 767 |
end; |
768 |
||
42241
dd8029f71e1c
separate module for standard implementation of inner syntax operations;
wenzelm
parents:
diff
changeset
|
769 |
|
42245 | 770 |
|
771 |
(** translations **) |
|
772 |
||
773 |
(* type propositions *) |
|
774 |
||
42247
12fe41a92cd5
typed_print_translation: discontinued show_sorts argument;
wenzelm
parents:
42245
diff
changeset
|
775 |
fun type_prop_tr' ctxt T [Const ("\\<^const>Pure.sort_constraint", _)] = |
42476 | 776 |
Syntax.const "_sort_constraint" $ term_of_typ (Config.put show_sorts true ctxt) T |
42247
12fe41a92cd5
typed_print_translation: discontinued show_sorts argument;
wenzelm
parents:
42245
diff
changeset
|
777 |
| type_prop_tr' ctxt T [t] = |
42476 | 778 |
Syntax.const "_ofclass" $ term_of_typ ctxt T $ t |
42245 | 779 |
| type_prop_tr' _ T ts = raise TYPE ("type_prop_tr'", [T], ts); |
780 |
||
781 |
||
782 |
(* type reflection *) |
|
783 |
||
42247
12fe41a92cd5
typed_print_translation: discontinued show_sorts argument;
wenzelm
parents:
42245
diff
changeset
|
784 |
fun type_tr' ctxt (Type ("itself", [T])) ts = |
42476 | 785 |
Term.list_comb (Syntax.const "_TYPE" $ term_of_typ ctxt T, ts) |
42245 | 786 |
| type_tr' _ _ _ = raise Match; |
787 |
||
788 |
||
789 |
(* type constraints *) |
|
790 |
||
42247
12fe41a92cd5
typed_print_translation: discontinued show_sorts argument;
wenzelm
parents:
42245
diff
changeset
|
791 |
fun type_constraint_tr' ctxt (Type ("fun", [T, _])) (t :: ts) = |
42476 | 792 |
Term.list_comb (Syntax.const "_constrain" $ t $ term_of_typ ctxt T, ts) |
42245 | 793 |
| type_constraint_tr' _ _ _ = raise Match; |
794 |
||
795 |
||
42295
8fdbb3b10beb
moved CONST syntax/translations to their proper place;
wenzelm
parents:
42294
diff
changeset
|
796 |
(* authentic syntax *) |
8fdbb3b10beb
moved CONST syntax/translations to their proper place;
wenzelm
parents:
42294
diff
changeset
|
797 |
|
8fdbb3b10beb
moved CONST syntax/translations to their proper place;
wenzelm
parents:
42294
diff
changeset
|
798 |
fun const_ast_tr intern ctxt [Ast.Variable c] = |
8fdbb3b10beb
moved CONST syntax/translations to their proper place;
wenzelm
parents:
42294
diff
changeset
|
799 |
let |
42360 | 800 |
val Const (c', _) = Proof_Context.read_const_proper ctxt false c; |
42295
8fdbb3b10beb
moved CONST syntax/translations to their proper place;
wenzelm
parents:
42294
diff
changeset
|
801 |
val d = if intern then Lexicon.mark_const c' else c; |
8fdbb3b10beb
moved CONST syntax/translations to their proper place;
wenzelm
parents:
42294
diff
changeset
|
802 |
in Ast.Constant d end |
42470 | 803 |
| const_ast_tr intern ctxt [Ast.Appl [Ast.Constant "_constrain", x, T as Ast.Variable pos]] = |
804 |
(Ast.Appl [Ast.Constant "_constrain", const_ast_tr intern ctxt [x], T] |
|
805 |
handle ERROR msg => |
|
48992 | 806 |
error (msg ^ Position.here (the_default Position.none (Term_Position.decode pos)))) |
42295
8fdbb3b10beb
moved CONST syntax/translations to their proper place;
wenzelm
parents:
42294
diff
changeset
|
807 |
| const_ast_tr _ _ asts = raise Ast.AST ("const_ast_tr", asts); |
8fdbb3b10beb
moved CONST syntax/translations to their proper place;
wenzelm
parents:
42294
diff
changeset
|
808 |
|
8fdbb3b10beb
moved CONST syntax/translations to their proper place;
wenzelm
parents:
42294
diff
changeset
|
809 |
|
42245 | 810 |
(* setup translations *) |
811 |
||
53171 | 812 |
val _ = Theory.setup |
52143 | 813 |
(Sign.parse_ast_translation |
814 |
[("_context_const", const_ast_tr true), |
|
815 |
("_context_xconst", const_ast_tr false)] #> |
|
816 |
Sign.typed_print_translation |
|
42245 | 817 |
[("_type_prop", type_prop_tr'), |
818 |
("\\<^const>TYPE", type_tr'), |
|
53171 | 819 |
("_type_constraint_", type_constraint_tr')]); |
42245 | 820 |
|
821 |
||
822 |
||
42382
dcd983ee2c29
provide structure Syntax early (before structure Type), back-patch check/uncheck later;
wenzelm
parents:
42379
diff
changeset
|
823 |
(** check/uncheck **) |
dcd983ee2c29
provide structure Syntax early (before structure Type), back-patch check/uncheck later;
wenzelm
parents:
42379
diff
changeset
|
824 |
|
45429 | 825 |
(* context-sensitive (un)checking *) |
826 |
||
827 |
type key = int * bool; |
|
828 |
||
829 |
structure Checks = Generic_Data |
|
830 |
( |
|
831 |
type 'a check = 'a list -> Proof.context -> ('a list * Proof.context) option; |
|
832 |
type T = |
|
833 |
((key * ((string * typ check) * stamp) list) list * |
|
834 |
(key * ((string * term check) * stamp) list) list); |
|
835 |
val empty = ([], []); |
|
836 |
val extend = I; |
|
837 |
fun merge ((typ_checks1, term_checks1), (typ_checks2, term_checks2)) : T = |
|
838 |
(AList.join (op =) (K (Library.merge (eq_snd (op =)))) (typ_checks1, typ_checks2), |
|
839 |
AList.join (op =) (K (Library.merge (eq_snd (op =)))) (term_checks1, term_checks2)); |
|
840 |
); |
|
841 |
||
842 |
fun print_checks ctxt = |
|
843 |
let |
|
844 |
fun split_checks checks = |
|
845 |
List.partition (fn ((_, un), _) => not un) checks |
|
846 |
|> pairself (map (fn ((i, _), fs) => (i, map (fst o fst) fs)) |
|
847 |
#> sort (int_ord o pairself fst)); |
|
848 |
fun pretty_checks kind checks = |
|
849 |
checks |> map (fn (i, names) => Pretty.block |
|
850 |
[Pretty.str (kind ^ " (stage " ^ signed_string_of_int i ^ "):"), |
|
851 |
Pretty.brk 1, Pretty.strs names]); |
|
852 |
||
853 |
val (typs, terms) = Checks.get (Context.Proof ctxt); |
|
854 |
val (typ_checks, typ_unchecks) = split_checks typs; |
|
855 |
val (term_checks, term_unchecks) = split_checks terms; |
|
856 |
in |
|
857 |
pretty_checks "typ_checks" typ_checks @ |
|
858 |
pretty_checks "term_checks" term_checks @ |
|
859 |
pretty_checks "typ_unchecks" typ_unchecks @ |
|
860 |
pretty_checks "term_unchecks" term_unchecks |
|
861 |
end |> Pretty.chunks |> Pretty.writeln; |
|
862 |
||
863 |
||
864 |
local |
|
865 |
||
866 |
fun context_check which (key: key) name f = |
|
867 |
Checks.map (which (AList.map_default op = (key, []) (cons ((name, f), stamp ())))); |
|
868 |
||
869 |
fun simple_check eq f xs ctxt = |
|
870 |
let val xs' = f ctxt xs |
|
871 |
in if eq_list eq (xs, xs') then NONE else SOME (xs', ctxt) end; |
|
872 |
||
873 |
in |
|
874 |
||
45444 | 875 |
fun typ_check' stage = context_check apfst (stage, false); |
876 |
fun term_check' stage = context_check apsnd (stage, false); |
|
877 |
fun typ_uncheck' stage = context_check apfst (stage, true); |
|
878 |
fun term_uncheck' stage = context_check apsnd (stage, true); |
|
45429 | 879 |
|
45444 | 880 |
fun typ_check key name f = typ_check' key name (simple_check (op =) f); |
881 |
fun term_check key name f = term_check' key name (simple_check (op aconv) f); |
|
882 |
fun typ_uncheck key name f = typ_uncheck' key name (simple_check (op =) f); |
|
883 |
fun term_uncheck key name f = term_uncheck' key name (simple_check (op aconv) f); |
|
45429 | 884 |
|
885 |
end; |
|
886 |
||
887 |
||
888 |
local |
|
889 |
||
890 |
fun check_stage fs = perhaps_loop (perhaps_apply (map uncurry fs)); |
|
891 |
fun check_all fs = perhaps_apply (map check_stage fs); |
|
892 |
||
893 |
fun check which uncheck ctxt0 xs0 = |
|
894 |
let |
|
895 |
val funs = which (Checks.get (Context.Proof ctxt0)) |
|
896 |
|> map_filter (fn ((i, u), fs) => if uncheck = u then SOME (i, map (snd o fst) fs) else NONE) |
|
897 |
|> Library.sort (int_ord o pairself fst) |> map snd |
|
898 |
|> not uncheck ? map rev; |
|
899 |
in #1 (perhaps (check_all funs) (xs0, ctxt0)) end; |
|
900 |
||
901 |
val apply_typ_check = check fst false; |
|
902 |
val apply_term_check = check snd false; |
|
903 |
val apply_typ_uncheck = check fst true; |
|
904 |
val apply_term_uncheck = check snd true; |
|
905 |
||
906 |
in |
|
907 |
||
49674
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
49662
diff
changeset
|
908 |
fun check_typs ctxt raw_tys = |
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
49662
diff
changeset
|
909 |
let |
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
49662
diff
changeset
|
910 |
val (sorting_report, tys) = Proof_Context.prepare_sortsT ctxt raw_tys; |
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
49662
diff
changeset
|
911 |
val _ = Context_Position.if_visible ctxt Output.report sorting_report; |
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
49662
diff
changeset
|
912 |
in |
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
49662
diff
changeset
|
913 |
tys |
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
49662
diff
changeset
|
914 |
|> apply_typ_check ctxt |
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
49662
diff
changeset
|
915 |
|> Term_Sharing.typs (Proof_Context.theory_of ctxt) |
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
49662
diff
changeset
|
916 |
end; |
45423
92f91f990165
tuned signature -- emphasize internal role of these operations;
wenzelm
parents:
45412
diff
changeset
|
917 |
|
45445
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45444
diff
changeset
|
918 |
fun check_terms ctxt raw_ts = |
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45444
diff
changeset
|
919 |
let |
49674
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
49662
diff
changeset
|
920 |
val (sorting_report, raw_ts') = Proof_Context.prepare_sorts ctxt raw_ts; |
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
49662
diff
changeset
|
921 |
val (ts, ps) = Type_Infer_Context.prepare_positions ctxt raw_ts'; |
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
49662
diff
changeset
|
922 |
|
45445
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45444
diff
changeset
|
923 |
val tys = map (Logic.mk_type o snd) ps; |
45448
018f8959c7a6
more efficient prepare_sorts -- bypass encoded positions;
wenzelm
parents:
45447
diff
changeset
|
924 |
val (ts', tys') = ts @ tys |
45445
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45444
diff
changeset
|
925 |
|> apply_term_check ctxt |
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45444
diff
changeset
|
926 |
|> chop (length ts); |
49674
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
49662
diff
changeset
|
927 |
val typing_report = |
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
49662
diff
changeset
|
928 |
fold2 (fn (pos, _) => fn ty => |
45445
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45444
diff
changeset
|
929 |
if Position.is_reported pos then |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49690
diff
changeset
|
930 |
cons (Position.reported_text pos Markup.typing |
49674
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
49662
diff
changeset
|
931 |
(Syntax.string_of_typ ctxt (Logic.dest_type ty))) |
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
49662
diff
changeset
|
932 |
else I) ps tys' [] |
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
49662
diff
changeset
|
933 |
|> implode; |
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
49662
diff
changeset
|
934 |
|
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
49662
diff
changeset
|
935 |
val _ = Context_Position.if_visible ctxt Output.report (sorting_report ^ typing_report); |
45445
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45444
diff
changeset
|
936 |
in Term_Sharing.terms (Proof_Context.theory_of ctxt) ts' end; |
45423
92f91f990165
tuned signature -- emphasize internal role of these operations;
wenzelm
parents:
45412
diff
changeset
|
937 |
|
42382
dcd983ee2c29
provide structure Syntax early (before structure Type), back-patch check/uncheck later;
wenzelm
parents:
42379
diff
changeset
|
938 |
fun check_props ctxt = map (Type.constraint propT) #> check_terms ctxt; |
dcd983ee2c29
provide structure Syntax early (before structure Type), back-patch check/uncheck later;
wenzelm
parents:
42379
diff
changeset
|
939 |
|
45429 | 940 |
val uncheck_typs = apply_typ_uncheck; |
941 |
val uncheck_terms = apply_term_uncheck; |
|
942 |
||
943 |
end; |
|
944 |
||
945 |
||
946 |
(* standard phases *) |
|
947 |
||
948 |
val _ = Context.>> |
|
949 |
(typ_check 0 "standard" Proof_Context.standard_typ_check #> |
|
950 |
term_check 0 "standard" |
|
951 |
(fn ctxt => Type_Infer_Context.infer_types ctxt #> map (Proof_Context.expand_abbrevs ctxt)) #> |
|
952 |
term_check 100 "standard_finish" Proof_Context.standard_term_check_finish #> |
|
953 |
term_uncheck 0 "standard" Proof_Context.standard_term_uncheck); |
|
42382
dcd983ee2c29
provide structure Syntax early (before structure Type), back-patch check/uncheck later;
wenzelm
parents:
42379
diff
changeset
|
954 |
|
dcd983ee2c29
provide structure Syntax early (before structure Type), back-patch check/uncheck later;
wenzelm
parents:
42379
diff
changeset
|
955 |
|
dcd983ee2c29
provide structure Syntax early (before structure Type), back-patch check/uncheck later;
wenzelm
parents:
42379
diff
changeset
|
956 |
|
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
957 |
(** install operations **) |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
958 |
|
42241
dd8029f71e1c
separate module for standard implementation of inner syntax operations;
wenzelm
parents:
diff
changeset
|
959 |
val _ = Syntax.install_operations |
dd8029f71e1c
separate module for standard implementation of inner syntax operations;
wenzelm
parents:
diff
changeset
|
960 |
{parse_sort = parse_sort, |
dd8029f71e1c
separate module for standard implementation of inner syntax operations;
wenzelm
parents:
diff
changeset
|
961 |
parse_typ = parse_typ, |
42281 | 962 |
parse_term = parse_term false, |
963 |
parse_prop = parse_term true, |
|
42241
dd8029f71e1c
separate module for standard implementation of inner syntax operations;
wenzelm
parents:
diff
changeset
|
964 |
unparse_sort = unparse_sort, |
dd8029f71e1c
separate module for standard implementation of inner syntax operations;
wenzelm
parents:
diff
changeset
|
965 |
unparse_typ = unparse_typ, |
42382
dcd983ee2c29
provide structure Syntax early (before structure Type), back-patch check/uncheck later;
wenzelm
parents:
42379
diff
changeset
|
966 |
unparse_term = unparse_term, |
dcd983ee2c29
provide structure Syntax early (before structure Type), back-patch check/uncheck later;
wenzelm
parents:
42379
diff
changeset
|
967 |
check_typs = check_typs, |
dcd983ee2c29
provide structure Syntax early (before structure Type), back-patch check/uncheck later;
wenzelm
parents:
42379
diff
changeset
|
968 |
check_terms = check_terms, |
dcd983ee2c29
provide structure Syntax early (before structure Type), back-patch check/uncheck later;
wenzelm
parents:
42379
diff
changeset
|
969 |
check_props = check_props, |
dcd983ee2c29
provide structure Syntax early (before structure Type), back-patch check/uncheck later;
wenzelm
parents:
42379
diff
changeset
|
970 |
uncheck_typs = uncheck_typs, |
dcd983ee2c29
provide structure Syntax early (before structure Type), back-patch check/uncheck later;
wenzelm
parents:
42379
diff
changeset
|
971 |
uncheck_terms = uncheck_terms}; |
42241
dd8029f71e1c
separate module for standard implementation of inner syntax operations;
wenzelm
parents:
diff
changeset
|
972 |
|
dd8029f71e1c
separate module for standard implementation of inner syntax operations;
wenzelm
parents:
diff
changeset
|
973 |
end; |