author | wenzelm |
Tue, 06 Sep 2011 19:48:57 +0200 | |
changeset 44735 | 66862d02678c |
parent 44564 | 96ba83710946 |
child 44736 | c2a3f1c84179 |
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 |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
10 |
val term_sorts: term -> (indexname * sort) list |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
11 |
val typ_of_term: (indexname -> sort) -> term -> typ |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
12 |
val decode_term: Proof.context -> |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
13 |
Position.reports * term Exn.result -> Position.reports * term Exn.result |
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 |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
16 |
end |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
17 |
|
42243 | 18 |
structure Syntax_Phases: SYNTAX_PHASES = |
42241
dd8029f71e1c
separate module for standard implementation of inner syntax operations;
wenzelm
parents:
diff
changeset
|
19 |
struct |
dd8029f71e1c
separate module for standard implementation of inner syntax operations;
wenzelm
parents:
diff
changeset
|
20 |
|
42298
d622145603ee
more accurate markup for syntax consts, notably binders which point back to the original logical entity;
wenzelm
parents:
42296
diff
changeset
|
21 |
(** 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
|
22 |
|
d622145603ee
more accurate markup for syntax consts, notably binders which point back to the original logical entity;
wenzelm
parents:
42296
diff
changeset
|
23 |
fun markup_class ctxt c = |
42379 | 24 |
[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
|
25 |
|
d622145603ee
more accurate markup for syntax consts, notably binders which point back to the original logical entity;
wenzelm
parents:
42296
diff
changeset
|
26 |
fun markup_type ctxt c = |
42379 | 27 |
[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
|
28 |
|
d622145603ee
more accurate markup for syntax consts, notably binders which point back to the original logical entity;
wenzelm
parents:
42296
diff
changeset
|
29 |
fun markup_const ctxt c = |
42379 | 30 |
[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
|
31 |
|
d622145603ee
more accurate markup for syntax consts, notably binders which point back to the original logical entity;
wenzelm
parents:
42296
diff
changeset
|
32 |
fun markup_free ctxt x = |
d622145603ee
more accurate markup for syntax consts, notably binders which point back to the original logical entity;
wenzelm
parents:
42296
diff
changeset
|
33 |
[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
|
34 |
(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
|
35 |
then [Variable.markup_fixed ctxt x] |
01430341fc79
more informative markup for fixed variables (via name space entry);
wenzelm
parents:
42488
diff
changeset
|
36 |
else []); |
42298
d622145603ee
more accurate markup for syntax consts, notably binders which point back to the original logical entity;
wenzelm
parents:
42296
diff
changeset
|
37 |
|
d622145603ee
more accurate markup for syntax consts, notably binders which point back to the original logical entity;
wenzelm
parents:
42296
diff
changeset
|
38 |
fun markup_var xi = [Markup.name (Term.string_of_vname xi) Markup.var]; |
d622145603ee
more accurate markup for syntax consts, notably binders which point back to the original logical entity;
wenzelm
parents:
42296
diff
changeset
|
39 |
|
d622145603ee
more accurate markup for syntax consts, notably binders which point back to the original logical entity;
wenzelm
parents:
42296
diff
changeset
|
40 |
fun markup_bound def id = |
d622145603ee
more accurate markup for syntax consts, notably binders which point back to the original logical entity;
wenzelm
parents:
42296
diff
changeset
|
41 |
[Markup.properties [(if def then Markup.defN else Markup.refN, id)] Markup.bound]; |
d622145603ee
more accurate markup for syntax consts, notably binders which point back to the original logical entity;
wenzelm
parents:
42296
diff
changeset
|
42 |
|
d622145603ee
more accurate markup for syntax consts, notably binders which point back to the original logical entity;
wenzelm
parents:
42296
diff
changeset
|
43 |
fun markup_entity ctxt c = |
42360 | 44 |
(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
|
45 |
SOME "" => [] |
d622145603ee
more accurate markup for syntax consts, notably binders which point back to the original logical entity;
wenzelm
parents:
42296
diff
changeset
|
46 |
| 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
|
47 |
| 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
|
48 |
{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
|
49 |
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
|
50 |
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
|
51 |
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
|
52 |
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
|
53 |
|
d622145603ee
more accurate markup for syntax consts, notably binders which point back to the original logical entity;
wenzelm
parents:
42296
diff
changeset
|
54 |
|
d622145603ee
more accurate markup for syntax consts, notably binders which point back to the original logical entity;
wenzelm
parents:
42296
diff
changeset
|
55 |
|
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
56 |
(** decode parse trees **) |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
57 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
58 |
(* sort_of_term *) |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
59 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
60 |
fun sort_of_term tm = |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
61 |
let |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
62 |
fun err () = raise TERM ("sort_of_term: bad encoding of classes", [tm]); |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
63 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
64 |
fun class s = Lexicon.unmark_class s handle Fail _ => err (); |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
65 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
66 |
fun classes (Const (s, _)) = [class s] |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
67 |
| classes (Const ("_classes", _) $ Const (s, _) $ cs) = class s :: classes cs |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
68 |
| classes _ = err (); |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
69 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
70 |
fun sort (Const ("_topsort", _)) = [] |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
71 |
| sort (Const (s, _)) = [class s] |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
72 |
| sort (Const ("_sort", _) $ cs) = classes cs |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
73 |
| sort _ = err (); |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
74 |
in sort tm end; |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
75 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
76 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
77 |
(* term_sorts *) |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
78 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
79 |
fun term_sorts tm = |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
80 |
let |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
81 |
val sort_of = sort_of_term; |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
82 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
83 |
fun add_env (Const ("_ofsort", _) $ Free (x, _) $ cs) = |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
84 |
insert (op =) ((x, ~1), sort_of cs) |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
85 |
| add_env (Const ("_ofsort", _) $ (Const ("_tfree", _) $ Free (x, _)) $ cs) = |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
86 |
insert (op =) ((x, ~1), sort_of cs) |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
87 |
| add_env (Const ("_ofsort", _) $ Var (xi, _) $ cs) = |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
88 |
insert (op =) (xi, sort_of cs) |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
89 |
| add_env (Const ("_ofsort", _) $ (Const ("_tvar", _) $ Var (xi, _)) $ cs) = |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
90 |
insert (op =) (xi, sort_of cs) |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
91 |
| add_env (Abs (_, _, t)) = add_env t |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
92 |
| add_env (t1 $ t2) = add_env t1 #> add_env t2 |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
93 |
| add_env _ = I; |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
94 |
in add_env tm [] end; |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
95 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
96 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
97 |
(* typ_of_term *) |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
98 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
99 |
fun typ_of_term get_sort tm = |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
100 |
let |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
101 |
fun err () = raise TERM ("typ_of_term: bad encoding of type", [tm]); |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
102 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
103 |
fun typ_of (Free (x, _)) = TFree (x, get_sort (x, ~1)) |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
104 |
| typ_of (Var (xi, _)) = TVar (xi, get_sort xi) |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
105 |
| typ_of (Const ("_tfree",_) $ (t as Free _)) = typ_of t |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
106 |
| typ_of (Const ("_tvar",_) $ (t as Var _)) = typ_of t |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
107 |
| typ_of (Const ("_ofsort", _) $ Free (x, _) $ _) = TFree (x, get_sort (x, ~1)) |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
108 |
| typ_of (Const ("_ofsort", _) $ (Const ("_tfree",_) $ Free (x, _)) $ _) = |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
109 |
TFree (x, get_sort (x, ~1)) |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
110 |
| typ_of (Const ("_ofsort", _) $ Var (xi, _) $ _) = TVar (xi, get_sort xi) |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
111 |
| typ_of (Const ("_ofsort", _) $ (Const ("_tvar",_) $ Var (xi, _)) $ _) = |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
112 |
TVar (xi, get_sort xi) |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
113 |
| typ_of (Const ("_dummy_ofsort", _) $ t) = TFree ("'_dummy_", sort_of_term t) |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
114 |
| typ_of t = |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
115 |
let |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
116 |
val (head, args) = Term.strip_comb t; |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
117 |
val a = |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
118 |
(case head of |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
119 |
Const (c, _) => (Lexicon.unmark_type c handle Fail _ => err ()) |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
120 |
| _ => err ()); |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
121 |
in Type (a, map typ_of args) end; |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
122 |
in typ_of tm end; |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
123 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
124 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
125 |
(* parsetree_to_ast *) |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
126 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
127 |
fun parsetree_to_ast ctxt constrain_pos trf parsetree = |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
128 |
let |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
129 |
val reports = Unsynchronized.ref ([]: Position.reports); |
44735 | 130 |
fun report pos = Position.store_reports reports [pos]; |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
131 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
132 |
fun trans a args = |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
133 |
(case trf a of |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
134 |
NONE => Ast.mk_appl (Ast.Constant a) args |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
135 |
| SOME f => f ctxt args); |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
136 |
|
42282
4fa41e068ff0
report literal tokens according to parsetree head;
wenzelm
parents:
42281
diff
changeset
|
137 |
fun asts_of (Parser.Node ("_class_name", [Parser.Tip tok])) = |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
138 |
let |
42470 | 139 |
val pos = Lexicon.pos_of_token tok; |
140 |
val c = Proof_Context.read_class ctxt (Lexicon.str_of_token tok) |
|
141 |
handle ERROR msg => error (msg ^ Position.str_of pos); |
|
142 |
val _ = report pos (markup_class ctxt) c; |
|
42282
4fa41e068ff0
report literal tokens according to parsetree head;
wenzelm
parents:
42281
diff
changeset
|
143 |
in [Ast.Constant (Lexicon.mark_class c)] end |
4fa41e068ff0
report literal tokens according to parsetree head;
wenzelm
parents:
42281
diff
changeset
|
144 |
| asts_of (Parser.Node ("_type_name", [Parser.Tip tok])) = |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
145 |
let |
42470 | 146 |
val pos = Lexicon.pos_of_token tok; |
147 |
val Type (c, _) = |
|
148 |
Proof_Context.read_type_name_proper ctxt false (Lexicon.str_of_token tok) |
|
149 |
handle ERROR msg => error (msg ^ Position.str_of pos); |
|
150 |
val _ = report pos (markup_type ctxt) c; |
|
42282
4fa41e068ff0
report literal tokens according to parsetree head;
wenzelm
parents:
42281
diff
changeset
|
151 |
in [Ast.Constant (Lexicon.mark_type c)] end |
42410
16bc5564535f
less bulky "_position", for improved readability of parse trees;
wenzelm
parents:
42408
diff
changeset
|
152 |
| asts_of (Parser.Node ("_position", [pt as Parser.Tip tok])) = |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
153 |
if constrain_pos then |
42282
4fa41e068ff0
report literal tokens according to parsetree head;
wenzelm
parents:
42281
diff
changeset
|
154 |
[Ast.Appl [Ast.Constant "_constrain", ast_of pt, |
4fa41e068ff0
report literal tokens according to parsetree head;
wenzelm
parents:
42281
diff
changeset
|
155 |
Ast.Variable (Term_Position.encode (Lexicon.pos_of_token tok))]] |
4fa41e068ff0
report literal tokens according to parsetree head;
wenzelm
parents:
42281
diff
changeset
|
156 |
else [ast_of pt] |
4fa41e068ff0
report literal tokens according to parsetree head;
wenzelm
parents:
42281
diff
changeset
|
157 |
| asts_of (Parser.Node (a, pts)) = |
4fa41e068ff0
report literal tokens according to parsetree head;
wenzelm
parents:
42281
diff
changeset
|
158 |
let |
4fa41e068ff0
report literal tokens according to parsetree head;
wenzelm
parents:
42281
diff
changeset
|
159 |
val _ = pts |> List.app |
4fa41e068ff0
report literal tokens according to parsetree head;
wenzelm
parents:
42281
diff
changeset
|
160 |
(fn Parser.Node _ => () | Parser.Tip tok => |
4fa41e068ff0
report literal tokens according to parsetree head;
wenzelm
parents:
42281
diff
changeset
|
161 |
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
|
162 |
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
|
163 |
in [trans a (maps asts_of pts)] end |
4fa41e068ff0
report literal tokens according to parsetree head;
wenzelm
parents:
42281
diff
changeset
|
164 |
| asts_of (Parser.Tip tok) = |
4fa41e068ff0
report literal tokens according to parsetree head;
wenzelm
parents:
42281
diff
changeset
|
165 |
if Lexicon.valued_token tok |
4fa41e068ff0
report literal tokens according to parsetree head;
wenzelm
parents:
42281
diff
changeset
|
166 |
then [Ast.Variable (Lexicon.str_of_token tok)] |
4fa41e068ff0
report literal tokens according to parsetree head;
wenzelm
parents:
42281
diff
changeset
|
167 |
else [] |
4fa41e068ff0
report literal tokens according to parsetree head;
wenzelm
parents:
42281
diff
changeset
|
168 |
|
4fa41e068ff0
report literal tokens according to parsetree head;
wenzelm
parents:
42281
diff
changeset
|
169 |
and ast_of pt = |
4fa41e068ff0
report literal tokens according to parsetree head;
wenzelm
parents:
42281
diff
changeset
|
170 |
(case asts_of pt of |
4fa41e068ff0
report literal tokens according to parsetree head;
wenzelm
parents:
42281
diff
changeset
|
171 |
[ast] => ast |
4fa41e068ff0
report literal tokens according to parsetree head;
wenzelm
parents:
42281
diff
changeset
|
172 |
| 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
|
173 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
174 |
val ast = Exn.interruptible_capture ast_of parsetree; |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
175 |
in (! reports, ast) end; |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
176 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
177 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
178 |
(* ast_to_term *) |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
179 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
180 |
fun ast_to_term ctxt trf = |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
181 |
let |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
182 |
fun trans a args = |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
183 |
(case trf a of |
42476 | 184 |
NONE => Term.list_comb (Syntax.const a, args) |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
185 |
| SOME f => f ctxt args); |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
186 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
187 |
fun term_of (Ast.Constant a) = trans a [] |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
188 |
| term_of (Ast.Variable x) = Lexicon.read_var x |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
189 |
| term_of (Ast.Appl (Ast.Constant a :: (asts as _ :: _))) = |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
190 |
trans a (map term_of asts) |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
191 |
| term_of (Ast.Appl (ast :: (asts as _ :: _))) = |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
192 |
Term.list_comb (term_of ast, map term_of asts) |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
193 |
| 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
|
194 |
in term_of end; |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
195 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
196 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
197 |
(* decode_term -- transform parse tree into raw term *) |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
198 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
199 |
fun decode_term _ (result as (_: Position.reports, Exn.Exn _)) = result |
43761
e72ba84ae58f
tuned signature -- corresponding to Scala version;
wenzelm
parents:
43731
diff
changeset
|
200 |
| decode_term ctxt (reports0, Exn.Res tm) = |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
201 |
let |
42250
cc5ac538f991
eliminated odd object-oriented type_context/term_context;
wenzelm
parents:
42249
diff
changeset
|
202 |
fun get_const a = |
42360 | 203 |
((true, #1 (Term.dest_Const (Proof_Context.read_const_proper ctxt false a))) |
204 |
handle ERROR _ => (false, Consts.intern (Proof_Context.consts_of ctxt) a)); |
|
205 |
val get_free = Proof_Context.intern_skolem ctxt; |
|
42250
cc5ac538f991
eliminated odd object-oriented type_context/term_context;
wenzelm
parents:
42249
diff
changeset
|
206 |
|
42360 | 207 |
val decodeT = typ_of_term (Proof_Context.get_sort ctxt (term_sorts tm)); |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
208 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
209 |
val reports = Unsynchronized.ref reports0; |
44735 | 210 |
fun report ps = Position.store_reports reports ps; |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
211 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
212 |
fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) = |
42264 | 213 |
(case Term_Position.decode_position typ of |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
214 |
SOME p => decode (p :: ps) qs bs t |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
215 |
| NONE => Type.constraint (decodeT typ) (decode ps qs bs t)) |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
216 |
| decode ps qs bs (Const ("_constrainAbs", _) $ t $ typ) = |
42264 | 217 |
(case Term_Position.decode_position typ of |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
218 |
SOME q => decode ps (q :: qs) bs t |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
219 |
| NONE => Type.constraint (decodeT typ --> dummyT) (decode ps qs bs t)) |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
220 |
| decode _ qs bs (Abs (x, T, t)) = |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
221 |
let |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
222 |
val id = serial_string (); |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
223 |
val _ = report qs (markup_bound true) id; |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
224 |
in Abs (x, T, decode [] [] (id :: bs) t) end |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
225 |
| decode _ _ bs (t $ u) = decode [] [] bs t $ decode [] [] bs u |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
226 |
| decode ps _ _ (Const (a, T)) = |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
227 |
(case try Lexicon.unmark_fixed a of |
42282
4fa41e068ff0
report literal tokens according to parsetree head;
wenzelm
parents:
42281
diff
changeset
|
228 |
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
|
229 |
| NONE => |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
230 |
let |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
231 |
val c = |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
232 |
(case try Lexicon.unmark_const a of |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
233 |
SOME c => c |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
234 |
| NONE => snd (get_const a)); |
42282
4fa41e068ff0
report literal tokens according to parsetree head;
wenzelm
parents:
42281
diff
changeset
|
235 |
val _ = report ps (markup_const ctxt) c; |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
236 |
in Const (c, T) end) |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
237 |
| decode ps _ _ (Free (a, T)) = |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
238 |
(case (get_free a, get_const a) of |
42282
4fa41e068ff0
report literal tokens according to parsetree head;
wenzelm
parents:
42281
diff
changeset
|
239 |
(SOME x, _) => (report ps (markup_free ctxt) x; Free (x, T)) |
4fa41e068ff0
report literal tokens according to parsetree head;
wenzelm
parents:
42281
diff
changeset
|
240 |
| (_, (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
|
241 |
| (_, (false, c)) => |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
242 |
if Long_Name.is_qualified c |
42282
4fa41e068ff0
report literal tokens according to parsetree head;
wenzelm
parents:
42281
diff
changeset
|
243 |
then (report ps (markup_const ctxt) c; Const (c, T)) |
4fa41e068ff0
report literal tokens according to parsetree head;
wenzelm
parents:
42281
diff
changeset
|
244 |
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
|
245 |
| 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
|
246 |
| decode ps _ bs (t as Bound i) = |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
247 |
(case try (nth bs) i of |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
248 |
SOME id => (report ps (markup_bound false) id; t) |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
249 |
| NONE => t); |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
250 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
251 |
val tm' = Exn.interruptible_capture (fn () => decode [] [] [] tm) (); |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
252 |
in (! reports, tm') end; |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
253 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
254 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
255 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
256 |
(** parse **) |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
257 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
258 |
(* results *) |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
259 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
260 |
fun ambiguity_msg pos = "Parse error: ambiguous syntax" ^ Position.str_of pos; |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
261 |
|
43761
e72ba84ae58f
tuned signature -- corresponding to Scala version;
wenzelm
parents:
43731
diff
changeset
|
262 |
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
|
263 |
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
|
264 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
265 |
fun report ctxt = List.app (fn (pos, m) => Context_Position.report ctxt pos m); |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
266 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
267 |
fun report_result ctxt pos results = |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
268 |
(case (proper_results results, failed_results results) of |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
269 |
([], (reports, exn) :: _) => (report ctxt reports; reraise exn) |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
270 |
| ([(reports, x)], _) => (report ctxt reports; x) |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
271 |
| _ => error (ambiguity_msg pos)); |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
272 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
273 |
|
42249 | 274 |
(* parse raw asts *) |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
275 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
276 |
fun parse_asts ctxt raw root (syms, pos) = |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
277 |
let |
42360 | 278 |
val syn = Proof_Context.syn_of ctxt; |
42253 | 279 |
val ast_tr = Syntax.parse_ast_translation syn; |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
280 |
|
42251 | 281 |
val toks = Syntax.tokenize syn raw syms; |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
282 |
val _ = List.app (Lexicon.report_token ctxt) toks; |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
283 |
|
42251 | 284 |
val pts = Syntax.parse ctxt syn root (filter Lexicon.is_proper toks) |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
285 |
handle ERROR msg => |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
286 |
error (msg ^ |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
287 |
implode (map (Markup.markup Markup.report o Lexicon.reported_token_range ctxt) toks)); |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
288 |
val len = length pts; |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
289 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
290 |
val limit = Config.get ctxt Syntax.ambiguity_limit; |
44069 | 291 |
val warnings = Config.get ctxt Syntax.ambiguity_warnings; |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
292 |
val _ = |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
293 |
if len <= Config.get ctxt Syntax.ambiguity_level then () |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
294 |
else if not (Config.get ctxt Syntax.ambiguity_enabled) then error (ambiguity_msg pos) |
44069 | 295 |
else if warnings then |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
296 |
(Context_Position.if_visible ctxt warning (cat_lines |
44564
96ba83710946
tuned positions of ambiguity messages -- less intrusive in IDE view;
wenzelm
parents:
44069
diff
changeset
|
297 |
(("Ambiguous input" ^ Position.str_of (Position.reset_range pos) ^ |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
298 |
"\nproduces " ^ string_of_int len ^ " parse trees" ^ |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
299 |
(if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") :: |
44069 | 300 |
map (Pretty.string_of o Parser.pretty_parsetree) (take limit pts)))) |
301 |
else (); |
|
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
302 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
303 |
val constrain_pos = not raw andalso Config.get ctxt Syntax.positions; |
42253 | 304 |
val parsetree_to_ast = parsetree_to_ast ctxt constrain_pos ast_tr; |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
305 |
in map parsetree_to_ast pts end; |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
306 |
|
42249 | 307 |
fun parse_raw ctxt root input = |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
308 |
let |
42360 | 309 |
val syn = Proof_Context.syn_of ctxt; |
42253 | 310 |
val tr = Syntax.parse_translation syn; |
42255 | 311 |
val parse_rules = Syntax.parse_rules syn; |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
312 |
in |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
313 |
parse_asts ctxt false root input |
42255 | 314 |
|> (map o apsnd o Exn.maps_result) |
315 |
(Ast.normalize ctxt parse_rules #> Exn.interruptible_capture (ast_to_term ctxt tr)) |
|
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
316 |
end; |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
317 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
318 |
|
42249 | 319 |
(* parse logical entities *) |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
320 |
|
42241
dd8029f71e1c
separate module for standard implementation of inner syntax operations;
wenzelm
parents:
diff
changeset
|
321 |
fun parse_failed ctxt pos msg kind = |
dd8029f71e1c
separate module for standard implementation of inner syntax operations;
wenzelm
parents:
diff
changeset
|
322 |
cat_error msg ("Failed to parse " ^ kind ^ |
dd8029f71e1c
separate module for standard implementation of inner syntax operations;
wenzelm
parents:
diff
changeset
|
323 |
Markup.markup Markup.report (Context_Position.reported_text ctxt pos Markup.bad "")); |
dd8029f71e1c
separate module for standard implementation of inner syntax operations;
wenzelm
parents:
diff
changeset
|
324 |
|
43731
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
325 |
fun parse_sort ctxt = |
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
326 |
Syntax.parse_token ctxt Term_XML.Decode.sort Markup.sort |
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
327 |
(fn (syms, pos) => |
42249 | 328 |
parse_raw ctxt "sort" (syms, pos) |
329 |
|> report_result ctxt pos |
|
330 |
|> sort_of_term |
|
43731
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
331 |
|> 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
|
332 |
handle ERROR msg => parse_failed ctxt pos msg "sort"); |
42241
dd8029f71e1c
separate module for standard implementation of inner syntax operations;
wenzelm
parents:
diff
changeset
|
333 |
|
43731
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
334 |
fun parse_typ ctxt = |
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
335 |
Syntax.parse_token ctxt Term_XML.Decode.typ Markup.typ |
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
336 |
(fn (syms, pos) => |
42249 | 337 |
parse_raw ctxt "type" (syms, pos) |
338 |
|> report_result ctxt pos |
|
42360 | 339 |
|> (fn t => typ_of_term (Proof_Context.get_sort ctxt (term_sorts t)) 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
|
340 |
handle ERROR msg => parse_failed ctxt pos msg "type"); |
42241
dd8029f71e1c
separate module for standard implementation of inner syntax operations;
wenzelm
parents:
diff
changeset
|
341 |
|
43731
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
342 |
fun parse_term is_prop ctxt = |
42241
dd8029f71e1c
separate module for standard implementation of inner syntax operations;
wenzelm
parents:
diff
changeset
|
343 |
let |
42281 | 344 |
val (markup, kind, root, constrain) = |
345 |
if is_prop |
|
346 |
then (Markup.prop, "proposition", "prop", Type.constraint propT) |
|
42288
2074b31650e6
discontinued special treatment of structure Syntax_Ext (formerly Syn_Ext);
wenzelm
parents:
42284
diff
changeset
|
347 |
else (Markup.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
|
348 |
val decode = constrain o Term_XML.Decode.term; |
42249 | 349 |
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
|
350 |
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
|
351 |
(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
|
352 |
let |
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
353 |
val results = parse_raw ctxt root (syms, pos) |> map (decode_term ctxt); |
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
354 |
val ambiguity = length (proper_results results); |
42249 | 355 |
|
43731
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
356 |
val level = Config.get ctxt Syntax.ambiguity_level; |
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
357 |
val limit = Config.get ctxt Syntax.ambiguity_limit; |
44069 | 358 |
val warnings = Config.get ctxt Syntax.ambiguity_warnings; |
42249 | 359 |
|
43731
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
360 |
val ambig_msg = |
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
361 |
if ambiguity > 1 andalso ambiguity <= level then |
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
362 |
["Got more than one parse tree.\n\ |
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
363 |
\Retry with smaller syntax_ambiguity_level for more information."] |
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
364 |
else []; |
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
365 |
|
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
366 |
(*brute-force disambiguation via type-inference*) |
43761
e72ba84ae58f
tuned signature -- corresponding to Scala version;
wenzelm
parents:
43731
diff
changeset
|
367 |
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
|
368 |
handle exn as ERROR _ => Exn.Exn exn; |
42249 | 369 |
|
43731
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
370 |
val results' = |
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
371 |
if ambiguity > 1 then |
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
372 |
(Par_List.map_name "Syntax_Phases.parse_term" o apsnd o Exn.maps_result) |
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
373 |
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
|
374 |
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
|
375 |
val reports' = fst (hd results'); |
42249 | 376 |
|
43731
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
377 |
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
|
378 |
val checked = map snd (proper_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
|
379 |
val len = length checked; |
42249 | 380 |
|
43731
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
381 |
val show_term = Syntax.string_of_term (Config.put Printer.show_brackets true ctxt); |
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
382 |
in |
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
383 |
if len = 0 then |
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
384 |
report_result ctxt pos |
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
385 |
[(reports', Exn.Exn (Exn.EXCEPTIONS (map ERROR ambig_msg @ errs)))] |
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 if len = 1 then |
44069 | 387 |
(if ambiguity > level andalso warnings 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
|
388 |
Context_Position.if_visible ctxt warning |
44564
96ba83710946
tuned positions of ambiguity messages -- less intrusive in IDE view;
wenzelm
parents:
44069
diff
changeset
|
389 |
("Fortunately, only one parse tree is type correct" ^ |
96ba83710946
tuned positions of ambiguity messages -- less intrusive in IDE view;
wenzelm
parents:
44069
diff
changeset
|
390 |
Position.str_of (Position.reset_range pos) ^ |
96ba83710946
tuned positions of ambiguity messages -- less intrusive in IDE view;
wenzelm
parents:
44069
diff
changeset
|
391 |
",\nbut you may still want to disambiguate your grammar or your input.") |
43731
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
392 |
else (); report_result ctxt pos results') |
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
393 |
else |
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
394 |
report_result ctxt pos |
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
395 |
[(reports', Exn.Exn (ERROR (cat_lines (ambig_msg @ |
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
396 |
(("Ambiguous input, " ^ string_of_int len ^ " terms are type correct" ^ |
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
397 |
(if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") :: |
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
398 |
map show_term (take limit checked))))))] |
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43552
diff
changeset
|
399 |
end handle ERROR msg => parse_failed ctxt pos msg kind) |
42249 | 400 |
end; |
42241
dd8029f71e1c
separate module for standard implementation of inner syntax operations;
wenzelm
parents:
diff
changeset
|
401 |
|
dd8029f71e1c
separate module for standard implementation of inner syntax operations;
wenzelm
parents:
diff
changeset
|
402 |
|
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
403 |
(* parse_ast_pattern *) |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
404 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
405 |
fun parse_ast_pattern ctxt (root, str) = |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
406 |
let |
42360 | 407 |
val syn = Proof_Context.syn_of ctxt; |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
408 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
409 |
fun constify (ast as Ast.Constant _) = ast |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
410 |
| constify (ast as 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
|
411 |
if is_some (Syntax.lookup_const syn x) orelse Long_Name.is_qualified x |
d622145603ee
more accurate markup for syntax consts, notably binders which point back to the original logical entity;
wenzelm
parents:
42296
diff
changeset
|
412 |
then Ast.Constant x |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
413 |
else ast |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
414 |
| constify (Ast.Appl asts) = Ast.Appl (map constify asts); |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
415 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
416 |
val (syms, pos) = Syntax.read_token str; |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
417 |
in |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
418 |
parse_asts ctxt true root (syms, pos) |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
419 |
|> report_result ctxt pos |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
420 |
|> constify |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
421 |
end; |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
422 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
423 |
|
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
424 |
|
42245 | 425 |
(** encode parse trees **) |
426 |
||
427 |
(* term_of_sort *) |
|
428 |
||
429 |
fun term_of_sort S = |
|
430 |
let |
|
42476 | 431 |
val class = Syntax.const o Lexicon.mark_class; |
42245 | 432 |
|
433 |
fun classes [c] = class c |
|
42476 | 434 |
| classes (c :: cs) = Syntax.const "_classes" $ class c $ classes cs; |
42245 | 435 |
in |
436 |
(case S of |
|
42476 | 437 |
[] => Syntax.const "_topsort" |
42245 | 438 |
| [c] => class c |
42476 | 439 |
| cs => Syntax.const "_sort" $ classes cs) |
42245 | 440 |
end; |
441 |
||
442 |
||
443 |
(* term_of_typ *) |
|
444 |
||
42247
12fe41a92cd5
typed_print_translation: discontinued show_sorts argument;
wenzelm
parents:
42245
diff
changeset
|
445 |
fun term_of_typ ctxt ty = |
42245 | 446 |
let |
42247
12fe41a92cd5
typed_print_translation: discontinued show_sorts argument;
wenzelm
parents:
42245
diff
changeset
|
447 |
val show_sorts = Config.get ctxt show_sorts; |
12fe41a92cd5
typed_print_translation: discontinued show_sorts argument;
wenzelm
parents:
42245
diff
changeset
|
448 |
|
42245 | 449 |
fun of_sort t S = |
42476 | 450 |
if show_sorts then Syntax.const "_ofsort" $ t $ term_of_sort S |
42245 | 451 |
else t; |
452 |
||
453 |
fun term_of (Type (a, Ts)) = |
|
42476 | 454 |
Term.list_comb (Syntax.const (Lexicon.mark_type a), map term_of Ts) |
42245 | 455 |
| term_of (TFree (x, S)) = |
42290
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42289
diff
changeset
|
456 |
if is_some (Term_Position.decode x) then Syntax.free x |
42476 | 457 |
else of_sort (Syntax.const "_tfree" $ Syntax.free x) S |
458 |
| term_of (TVar (xi, S)) = of_sort (Syntax.const "_tvar" $ Syntax.var xi) S; |
|
42245 | 459 |
in term_of ty end; |
460 |
||
461 |
||
462 |
(* simple_ast_of *) |
|
463 |
||
464 |
fun simple_ast_of ctxt = |
|
465 |
let |
|
466 |
val tune_var = if Config.get ctxt show_question_marks then I else unprefix "?"; |
|
467 |
fun ast_of (Const (c, _)) = Ast.Constant c |
|
468 |
| ast_of (Free (x, _)) = Ast.Variable x |
|
469 |
| ast_of (Var (xi, _)) = Ast.Variable (tune_var (Term.string_of_vname xi)) |
|
470 |
| ast_of (t as _ $ _) = |
|
471 |
let val (f, args) = strip_comb t |
|
472 |
in Ast.mk_appl (ast_of f) (map ast_of args) end |
|
42408 | 473 |
| ast_of (Bound i) = Ast.Appl [Ast.Constant "_loose", Ast.Variable ("B." ^ string_of_int i)] |
42245 | 474 |
| ast_of (Abs _) = raise Fail "simple_ast_of: Abs"; |
475 |
in ast_of end; |
|
476 |
||
477 |
||
478 |
(* sort_to_ast and typ_to_ast *) |
|
479 |
||
480 |
fun ast_of_termT ctxt trf tm = |
|
481 |
let |
|
482 |
val ctxt' = Config.put show_sorts false ctxt; |
|
483 |
fun ast_of (t as Const ("_tfree", _) $ Free _) = simple_ast_of ctxt t |
|
484 |
| ast_of (t as Const ("_tvar", _) $ Var _) = simple_ast_of ctxt t |
|
485 |
| ast_of (Const (a, _)) = trans a [] |
|
486 |
| ast_of (t as _ $ _) = |
|
487 |
(case strip_comb t of |
|
488 |
(Const (a, _), args) => trans a args |
|
489 |
| (f, args) => Ast.Appl (map ast_of (f :: args))) |
|
490 |
| ast_of t = simple_ast_of ctxt t |
|
42254 | 491 |
and trans a args = ast_of (trf a ctxt' dummyT args) |
492 |
handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args); |
|
42245 | 493 |
in ast_of tm end; |
494 |
||
495 |
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
|
496 |
fun typ_to_ast ctxt trf T = ast_of_termT ctxt trf (term_of_typ ctxt T); |
42245 | 497 |
|
498 |
||
499 |
(* term_to_ast *) |
|
500 |
||
42252 | 501 |
fun term_to_ast idents is_syntax_const ctxt trf tm = |
42245 | 502 |
let |
503 |
val show_types = |
|
504 |
Config.get ctxt show_types orelse Config.get ctxt show_sorts orelse |
|
505 |
Config.get ctxt show_all_types; |
|
506 |
val show_structs = Config.get ctxt show_structs; |
|
507 |
val show_free_types = Config.get ctxt show_free_types; |
|
508 |
val show_all_types = Config.get ctxt show_all_types; |
|
509 |
||
510 |
val {structs, fixes} = idents; |
|
511 |
||
42249 | 512 |
fun mark_atoms ((t as Const (c, _)) $ u) = |
42294 | 513 |
if member (op =) Syntax.token_markers c |
42245 | 514 |
then t $ u else mark_atoms t $ mark_atoms u |
515 |
| mark_atoms (t $ u) = mark_atoms t $ mark_atoms u |
|
516 |
| mark_atoms (Abs (x, T, t)) = Abs (x, T, mark_atoms t) |
|
517 |
| mark_atoms (t as Const (c, T)) = |
|
42252 | 518 |
if is_syntax_const c then t |
42245 | 519 |
else Const (Lexicon.mark_const c, T) |
520 |
| mark_atoms (t as Free (x, T)) = |
|
521 |
let val i = find_index (fn s => s = x) structs + 1 in |
|
522 |
if i = 0 andalso member (op =) fixes x then |
|
523 |
Const (Lexicon.mark_fixed x, T) |
|
524 |
else if i = 1 andalso not show_structs then |
|
42476 | 525 |
Syntax.const "_struct" $ Syntax.const "_indexdefault" |
526 |
else Syntax.const "_free" $ t |
|
42245 | 527 |
end |
528 |
| mark_atoms (t as Var (xi, T)) = |
|
42288
2074b31650e6
discontinued special treatment of structure Syntax_Ext (formerly Syn_Ext);
wenzelm
parents:
42284
diff
changeset
|
529 |
if xi = Syntax_Ext.dddot_indexname then Const ("_DDDOT", T) |
42476 | 530 |
else Syntax.const "_var" $ t |
42245 | 531 |
| mark_atoms a = a; |
532 |
||
533 |
fun prune_typs (t_seen as (Const _, _)) = t_seen |
|
534 |
| prune_typs (t as Free (x, ty), seen) = |
|
535 |
if ty = dummyT then (t, seen) |
|
42290
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42289
diff
changeset
|
536 |
else if not show_free_types orelse member (op aconv) seen t then (Syntax.free x, seen) |
42245 | 537 |
else (t, t :: seen) |
538 |
| prune_typs (t as Var (xi, ty), seen) = |
|
539 |
if ty = dummyT then (t, seen) |
|
42290
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42289
diff
changeset
|
540 |
else if not show_free_types orelse member (op aconv) seen t then (Syntax.var xi, seen) |
42245 | 541 |
else (t, t :: seen) |
542 |
| prune_typs (t_seen as (Bound _, _)) = t_seen |
|
543 |
| prune_typs (Abs (x, ty, t), seen) = |
|
544 |
let val (t', seen') = prune_typs (t, seen); |
|
545 |
in (Abs (x, ty, t'), seen') end |
|
546 |
| prune_typs (t1 $ t2, seen) = |
|
547 |
let |
|
548 |
val (t1', seen') = prune_typs (t1, seen); |
|
549 |
val (t2', seen'') = prune_typs (t2, seen'); |
|
550 |
in (t1' $ t2', seen'') end; |
|
551 |
||
552 |
fun ast_of tm = |
|
553 |
(case strip_comb tm of |
|
42284 | 554 |
(t as Abs _, ts) => Ast.mk_appl (ast_of (Syntax_Trans.abs_tr' ctxt t)) (map ast_of ts) |
42245 | 555 |
| ((c as Const ("_free", _)), Free (x, T) :: ts) => |
42290
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42289
diff
changeset
|
556 |
Ast.mk_appl (constrain (c $ Syntax.free x) T) (map ast_of ts) |
42245 | 557 |
| ((c as Const ("_var", _)), Var (xi, T) :: ts) => |
42290
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42289
diff
changeset
|
558 |
Ast.mk_appl (constrain (c $ Syntax.var xi) T) (map ast_of ts) |
42245 | 559 |
| ((c as Const ("_bound", _)), Free (x, T) :: ts) => |
42290
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42289
diff
changeset
|
560 |
Ast.mk_appl (constrain (c $ Syntax.free x) T) (map ast_of ts) |
42245 | 561 |
| (Const ("_idtdummy", T), ts) => |
42476 | 562 |
Ast.mk_appl (constrain (Syntax.const "_idtdummy") T) (map ast_of ts) |
42245 | 563 |
| (const as Const (c, T), ts) => |
564 |
if show_all_types |
|
565 |
then Ast.mk_appl (constrain const T) (map ast_of ts) |
|
566 |
else trans c T ts |
|
567 |
| (t, ts) => Ast.mk_appl (simple_ast_of ctxt t) (map ast_of ts)) |
|
568 |
||
42254 | 569 |
and trans a T args = ast_of (trf a ctxt T args) |
570 |
handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args) |
|
42245 | 571 |
|
572 |
and constrain t T = |
|
573 |
if show_types andalso T <> dummyT then |
|
42248 | 574 |
Ast.Appl [Ast.Constant "_constrain", simple_ast_of ctxt t, |
42247
12fe41a92cd5
typed_print_translation: discontinued show_sorts argument;
wenzelm
parents:
42245
diff
changeset
|
575 |
ast_of_termT ctxt trf (term_of_typ ctxt T)] |
42245 | 576 |
else simple_ast_of ctxt t; |
577 |
in |
|
578 |
tm |
|
42284 | 579 |
|> Syntax_Trans.prop_tr' |
42245 | 580 |
|> show_types ? (#1 o prune_typs o rpair []) |
581 |
|> mark_atoms |
|
582 |
|> ast_of |
|
583 |
end; |
|
584 |
||
585 |
||
586 |
||
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
587 |
(** unparse **) |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
588 |
|
42245 | 589 |
local |
590 |
||
42267
9566078ad905
simplified printer context: uniform externing and static token translations;
wenzelm
parents:
42264
diff
changeset
|
591 |
fun free_or_skolem ctxt x = |
9566078ad905
simplified printer context: uniform externing and static token translations;
wenzelm
parents:
42264
diff
changeset
|
592 |
let |
9566078ad905
simplified printer context: uniform externing and static token translations;
wenzelm
parents:
42264
diff
changeset
|
593 |
val m = |
9566078ad905
simplified printer context: uniform externing and static token translations;
wenzelm
parents:
42264
diff
changeset
|
594 |
if Variable.is_fixed ctxt x orelse Syntax.is_pretty_global ctxt |
9566078ad905
simplified printer context: uniform externing and static token translations;
wenzelm
parents:
42264
diff
changeset
|
595 |
then Markup.fixed x |
9566078ad905
simplified printer context: uniform externing and static token translations;
wenzelm
parents:
42264
diff
changeset
|
596 |
else Markup.hilite; |
9566078ad905
simplified printer context: uniform externing and static token translations;
wenzelm
parents:
42264
diff
changeset
|
597 |
in |
9566078ad905
simplified printer context: uniform externing and static token translations;
wenzelm
parents:
42264
diff
changeset
|
598 |
if can Name.dest_skolem x |
42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42476
diff
changeset
|
599 |
then ([m, Markup.skolem], Variable.revert_fixed ctxt x) |
42267
9566078ad905
simplified printer context: uniform externing and static token translations;
wenzelm
parents:
42264
diff
changeset
|
600 |
else ([m, Markup.free], x) |
9566078ad905
simplified printer context: uniform externing and static token translations;
wenzelm
parents:
42264
diff
changeset
|
601 |
end; |
9566078ad905
simplified printer context: uniform externing and static token translations;
wenzelm
parents:
42264
diff
changeset
|
602 |
|
9566078ad905
simplified printer context: uniform externing and static token translations;
wenzelm
parents:
42264
diff
changeset
|
603 |
fun var_or_skolem s = |
9566078ad905
simplified printer context: uniform externing and static token translations;
wenzelm
parents:
42264
diff
changeset
|
604 |
(case Lexicon.read_variable s of |
9566078ad905
simplified printer context: uniform externing and static token translations;
wenzelm
parents:
42264
diff
changeset
|
605 |
SOME (x, i) => |
9566078ad905
simplified printer context: uniform externing and static token translations;
wenzelm
parents:
42264
diff
changeset
|
606 |
(case try Name.dest_skolem x of |
9566078ad905
simplified printer context: uniform externing and static token translations;
wenzelm
parents:
42264
diff
changeset
|
607 |
NONE => (Markup.var, s) |
9566078ad905
simplified printer context: uniform externing and static token translations;
wenzelm
parents:
42264
diff
changeset
|
608 |
| SOME x' => (Markup.skolem, Term.string_of_vname (x', i))) |
9566078ad905
simplified printer context: uniform externing and static token translations;
wenzelm
parents:
42264
diff
changeset
|
609 |
| NONE => (Markup.var, s)); |
9566078ad905
simplified printer context: uniform externing and static token translations;
wenzelm
parents:
42264
diff
changeset
|
610 |
|
9566078ad905
simplified printer context: uniform externing and static token translations;
wenzelm
parents:
42264
diff
changeset
|
611 |
fun unparse_t t_to_ast prt_t markup ctxt t = |
42245 | 612 |
let |
42360 | 613 |
val syn = Proof_Context.syn_of ctxt; |
42267
9566078ad905
simplified printer context: uniform externing and static token translations;
wenzelm
parents:
42264
diff
changeset
|
614 |
|
9566078ad905
simplified printer context: uniform externing and static token translations;
wenzelm
parents:
42264
diff
changeset
|
615 |
fun token_trans "_tfree" x = SOME (Pretty.mark_str (Markup.tfree, x)) |
9566078ad905
simplified printer context: uniform externing and static token translations;
wenzelm
parents:
42264
diff
changeset
|
616 |
| token_trans "_tvar" x = SOME (Pretty.mark_str (Markup.tvar, x)) |
9566078ad905
simplified printer context: uniform externing and static token translations;
wenzelm
parents:
42264
diff
changeset
|
617 |
| token_trans "_free" x = SOME (Pretty.marks_str (free_or_skolem ctxt x)) |
9566078ad905
simplified printer context: uniform externing and static token translations;
wenzelm
parents:
42264
diff
changeset
|
618 |
| token_trans "_bound" x = SOME (Pretty.mark_str (Markup.bound, x)) |
42408 | 619 |
| token_trans "_loose" x = SOME (Pretty.mark_str (Markup.malformed, x)) |
42267
9566078ad905
simplified printer context: uniform externing and static token translations;
wenzelm
parents:
42264
diff
changeset
|
620 |
| token_trans "_var" x = SOME (Pretty.mark_str (var_or_skolem x)) |
9566078ad905
simplified printer context: uniform externing and static token translations;
wenzelm
parents:
42264
diff
changeset
|
621 |
| token_trans "_numeral" x = SOME (Pretty.mark_str (Markup.numeral, x)) |
9566078ad905
simplified printer context: uniform externing and static token translations;
wenzelm
parents:
42264
diff
changeset
|
622 |
| token_trans "_inner_string" x = SOME (Pretty.mark_str (Markup.inner_string, x)) |
9566078ad905
simplified printer context: uniform externing and static token translations;
wenzelm
parents:
42264
diff
changeset
|
623 |
| token_trans _ _ = NONE; |
9566078ad905
simplified printer context: uniform externing and static token translations;
wenzelm
parents:
42264
diff
changeset
|
624 |
|
42301
d7ca0c03d4ea
unparse: more accurate markup for syntax consts, notably binders;
wenzelm
parents:
42298
diff
changeset
|
625 |
fun markup_extern c = |
d7ca0c03d4ea
unparse: more accurate markup for syntax consts, notably binders;
wenzelm
parents:
42298
diff
changeset
|
626 |
(case Syntax.lookup_const syn c of |
d7ca0c03d4ea
unparse: more accurate markup for syntax consts, notably binders;
wenzelm
parents:
42298
diff
changeset
|
627 |
SOME "" => ([], c) |
d7ca0c03d4ea
unparse: more accurate markup for syntax consts, notably binders;
wenzelm
parents:
42298
diff
changeset
|
628 |
| SOME b => markup_extern b |
d7ca0c03d4ea
unparse: more accurate markup for syntax consts, notably binders;
wenzelm
parents:
42298
diff
changeset
|
629 |
| NONE => c |> Lexicon.unmark |
43548
f231a7594e54
type classes: entity markup instead of old-style token markup;
wenzelm
parents:
42493
diff
changeset
|
630 |
{case_class = fn x => (markup_class ctxt x, Proof_Context.extern_class ctxt x), |
43552 | 631 |
case_type = fn x => (markup_type ctxt x, Proof_Context.extern_type ctxt x), |
632 |
case_const = fn x => (markup_const ctxt x, Proof_Context.extern_const ctxt x), |
|
42301
d7ca0c03d4ea
unparse: more accurate markup for syntax consts, notably binders;
wenzelm
parents:
42298
diff
changeset
|
633 |
case_fixed = fn x => free_or_skolem ctxt x, |
d7ca0c03d4ea
unparse: more accurate markup for syntax consts, notably binders;
wenzelm
parents:
42298
diff
changeset
|
634 |
case_default = fn x => ([], x)}); |
42245 | 635 |
in |
42255 | 636 |
t_to_ast ctxt (Syntax.print_translation syn) t |
637 |
|> Ast.normalize ctxt (Syntax.print_rules syn) |
|
42267
9566078ad905
simplified printer context: uniform externing and static token translations;
wenzelm
parents:
42264
diff
changeset
|
638 |
|> prt_t ctxt (Syntax.prtabs syn) (Syntax.print_ast_translation syn) token_trans markup_extern |
42253 | 639 |
|> Pretty.markup markup |
42245 | 640 |
end; |
641 |
||
642 |
in |
|
643 |
||
42267
9566078ad905
simplified printer context: uniform externing and static token translations;
wenzelm
parents:
42264
diff
changeset
|
644 |
val unparse_sort = unparse_t sort_to_ast Printer.pretty_typ_ast Markup.sort; |
9566078ad905
simplified printer context: uniform externing and static token translations;
wenzelm
parents:
42264
diff
changeset
|
645 |
val unparse_typ = unparse_t typ_to_ast Printer.pretty_typ_ast Markup.typ; |
42241
dd8029f71e1c
separate module for standard implementation of inner syntax operations;
wenzelm
parents:
diff
changeset
|
646 |
|
dd8029f71e1c
separate module for standard implementation of inner syntax operations;
wenzelm
parents:
diff
changeset
|
647 |
fun unparse_term ctxt = |
dd8029f71e1c
separate module for standard implementation of inner syntax operations;
wenzelm
parents:
diff
changeset
|
648 |
let |
42360 | 649 |
val thy = Proof_Context.theory_of ctxt; |
650 |
val syn = Proof_Context.syn_of ctxt; |
|
651 |
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
|
652 |
in |
42298
d622145603ee
more accurate markup for syntax consts, notably binders which point back to the original logical entity;
wenzelm
parents:
42296
diff
changeset
|
653 |
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
|
654 |
(Printer.pretty_term_ast (not (Pure_Thy.old_appl_syntax thy))) |
9566078ad905
simplified printer context: uniform externing and static token translations;
wenzelm
parents:
42264
diff
changeset
|
655 |
Markup.term ctxt |
42241
dd8029f71e1c
separate module for standard implementation of inner syntax operations;
wenzelm
parents:
diff
changeset
|
656 |
end; |
dd8029f71e1c
separate module for standard implementation of inner syntax operations;
wenzelm
parents:
diff
changeset
|
657 |
|
42249 | 658 |
end; |
659 |
||
42241
dd8029f71e1c
separate module for standard implementation of inner syntax operations;
wenzelm
parents:
diff
changeset
|
660 |
|
42245 | 661 |
|
662 |
(** translations **) |
|
663 |
||
664 |
(* type propositions *) |
|
665 |
||
42247
12fe41a92cd5
typed_print_translation: discontinued show_sorts argument;
wenzelm
parents:
42245
diff
changeset
|
666 |
fun type_prop_tr' ctxt T [Const ("\\<^const>Pure.sort_constraint", _)] = |
42476 | 667 |
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
|
668 |
| type_prop_tr' ctxt T [t] = |
42476 | 669 |
Syntax.const "_ofclass" $ term_of_typ ctxt T $ t |
42245 | 670 |
| type_prop_tr' _ T ts = raise TYPE ("type_prop_tr'", [T], ts); |
671 |
||
672 |
||
673 |
(* type reflection *) |
|
674 |
||
42247
12fe41a92cd5
typed_print_translation: discontinued show_sorts argument;
wenzelm
parents:
42245
diff
changeset
|
675 |
fun type_tr' ctxt (Type ("itself", [T])) ts = |
42476 | 676 |
Term.list_comb (Syntax.const "_TYPE" $ term_of_typ ctxt T, ts) |
42245 | 677 |
| type_tr' _ _ _ = raise Match; |
678 |
||
679 |
||
680 |
(* type constraints *) |
|
681 |
||
42247
12fe41a92cd5
typed_print_translation: discontinued show_sorts argument;
wenzelm
parents:
42245
diff
changeset
|
682 |
fun type_constraint_tr' ctxt (Type ("fun", [T, _])) (t :: ts) = |
42476 | 683 |
Term.list_comb (Syntax.const "_constrain" $ t $ term_of_typ ctxt T, ts) |
42245 | 684 |
| type_constraint_tr' _ _ _ = raise Match; |
685 |
||
686 |
||
42295
8fdbb3b10beb
moved CONST syntax/translations to their proper place;
wenzelm
parents:
42294
diff
changeset
|
687 |
(* authentic syntax *) |
8fdbb3b10beb
moved CONST syntax/translations to their proper place;
wenzelm
parents:
42294
diff
changeset
|
688 |
|
8fdbb3b10beb
moved CONST syntax/translations to their proper place;
wenzelm
parents:
42294
diff
changeset
|
689 |
fun const_ast_tr intern ctxt [Ast.Variable c] = |
8fdbb3b10beb
moved CONST syntax/translations to their proper place;
wenzelm
parents:
42294
diff
changeset
|
690 |
let |
42360 | 691 |
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
|
692 |
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
|
693 |
in Ast.Constant d end |
42470 | 694 |
| const_ast_tr intern ctxt [Ast.Appl [Ast.Constant "_constrain", x, T as Ast.Variable pos]] = |
695 |
(Ast.Appl [Ast.Constant "_constrain", const_ast_tr intern ctxt [x], T] |
|
696 |
handle ERROR msg => |
|
697 |
error (msg ^ Position.str_of (the_default Position.none (Term_Position.decode pos)))) |
|
42295
8fdbb3b10beb
moved CONST syntax/translations to their proper place;
wenzelm
parents:
42294
diff
changeset
|
698 |
| 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
|
699 |
|
8fdbb3b10beb
moved CONST syntax/translations to their proper place;
wenzelm
parents:
42294
diff
changeset
|
700 |
|
42245 | 701 |
(* setup translations *) |
702 |
||
703 |
val _ = Context.>> (Context.map_theory |
|
42295
8fdbb3b10beb
moved CONST syntax/translations to their proper place;
wenzelm
parents:
42294
diff
changeset
|
704 |
(Sign.add_advanced_trfuns |
8fdbb3b10beb
moved CONST syntax/translations to their proper place;
wenzelm
parents:
42294
diff
changeset
|
705 |
([("_context_const", const_ast_tr true), |
8fdbb3b10beb
moved CONST syntax/translations to their proper place;
wenzelm
parents:
42294
diff
changeset
|
706 |
("_context_xconst", const_ast_tr false)], [], [], []) #> |
8fdbb3b10beb
moved CONST syntax/translations to their proper place;
wenzelm
parents:
42294
diff
changeset
|
707 |
Sign.add_advanced_trfunsT |
42245 | 708 |
[("_type_prop", type_prop_tr'), |
709 |
("\\<^const>TYPE", type_tr'), |
|
710 |
("_type_constraint_", type_constraint_tr')])); |
|
711 |
||
712 |
||
713 |
||
42382
dcd983ee2c29
provide structure Syntax early (before structure Type), back-patch check/uncheck later;
wenzelm
parents:
42379
diff
changeset
|
714 |
(** check/uncheck **) |
dcd983ee2c29
provide structure Syntax early (before structure Type), back-patch check/uncheck later;
wenzelm
parents:
42379
diff
changeset
|
715 |
|
43794
49cbbe2768a8
sub-structural sharing after Syntax.check phase, with global interning of logical entities (the latter is relevant when bypassing default parsing via YXML);
wenzelm
parents:
43761
diff
changeset
|
716 |
fun check_typs ctxt = Syntax.typ_check ctxt #> Term_Sharing.typs (Proof_Context.theory_of ctxt); |
49cbbe2768a8
sub-structural sharing after Syntax.check phase, with global interning of logical entities (the latter is relevant when bypassing default parsing via YXML);
wenzelm
parents:
43761
diff
changeset
|
717 |
fun check_terms ctxt = Syntax.term_check ctxt #> Term_Sharing.terms (Proof_Context.theory_of ctxt); |
42382
dcd983ee2c29
provide structure Syntax early (before structure Type), back-patch check/uncheck later;
wenzelm
parents:
42379
diff
changeset
|
718 |
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
|
719 |
|
dcd983ee2c29
provide structure Syntax early (before structure Type), back-patch check/uncheck later;
wenzelm
parents:
42379
diff
changeset
|
720 |
val uncheck_typs = Syntax.typ_uncheck; |
dcd983ee2c29
provide structure Syntax early (before structure Type), back-patch check/uncheck later;
wenzelm
parents:
42379
diff
changeset
|
721 |
val uncheck_terms = Syntax.term_uncheck; |
dcd983ee2c29
provide structure Syntax early (before structure Type), back-patch check/uncheck later;
wenzelm
parents:
42379
diff
changeset
|
722 |
|
dcd983ee2c29
provide structure Syntax early (before structure Type), back-patch check/uncheck later;
wenzelm
parents:
42379
diff
changeset
|
723 |
|
dcd983ee2c29
provide structure Syntax early (before structure Type), back-patch check/uncheck later;
wenzelm
parents:
42379
diff
changeset
|
724 |
|
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
725 |
(** install operations **) |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42241
diff
changeset
|
726 |
|
42241
dd8029f71e1c
separate module for standard implementation of inner syntax operations;
wenzelm
parents:
diff
changeset
|
727 |
val _ = Syntax.install_operations |
dd8029f71e1c
separate module for standard implementation of inner syntax operations;
wenzelm
parents:
diff
changeset
|
728 |
{parse_sort = parse_sort, |
dd8029f71e1c
separate module for standard implementation of inner syntax operations;
wenzelm
parents:
diff
changeset
|
729 |
parse_typ = parse_typ, |
42281 | 730 |
parse_term = parse_term false, |
731 |
parse_prop = parse_term true, |
|
42241
dd8029f71e1c
separate module for standard implementation of inner syntax operations;
wenzelm
parents:
diff
changeset
|
732 |
unparse_sort = unparse_sort, |
dd8029f71e1c
separate module for standard implementation of inner syntax operations;
wenzelm
parents:
diff
changeset
|
733 |
unparse_typ = unparse_typ, |
42382
dcd983ee2c29
provide structure Syntax early (before structure Type), back-patch check/uncheck later;
wenzelm
parents:
42379
diff
changeset
|
734 |
unparse_term = unparse_term, |
dcd983ee2c29
provide structure Syntax early (before structure Type), back-patch check/uncheck later;
wenzelm
parents:
42379
diff
changeset
|
735 |
check_typs = check_typs, |
dcd983ee2c29
provide structure Syntax early (before structure Type), back-patch check/uncheck later;
wenzelm
parents:
42379
diff
changeset
|
736 |
check_terms = check_terms, |
dcd983ee2c29
provide structure Syntax early (before structure Type), back-patch check/uncheck later;
wenzelm
parents:
42379
diff
changeset
|
737 |
check_props = check_props, |
dcd983ee2c29
provide structure Syntax early (before structure Type), back-patch check/uncheck later;
wenzelm
parents:
42379
diff
changeset
|
738 |
uncheck_typs = uncheck_typs, |
dcd983ee2c29
provide structure Syntax early (before structure Type), back-patch check/uncheck later;
wenzelm
parents:
42379
diff
changeset
|
739 |
uncheck_terms = uncheck_terms}; |
42241
dd8029f71e1c
separate module for standard implementation of inner syntax operations;
wenzelm
parents:
diff
changeset
|
740 |
|
dd8029f71e1c
separate module for standard implementation of inner syntax operations;
wenzelm
parents:
diff
changeset
|
741 |
end; |