author | wenzelm |
Tue, 30 Jan 2018 16:12:50 +0100 | |
changeset 67538 | 7747761fa067 |
parent 67536 | f0b2cc2ad464 |
child 67539 | 1b8aad1909b7 |
permissions | -rw-r--r-- |
18 | 1 |
(* Title: Pure/Syntax/parser.ML |
2186 | 2 |
Author: Carsten Clasohm, Sonia Mahjoub, and Markus Wenzel, TU Muenchen |
18 | 3 |
|
15979 | 4 |
General context-free parser for the inner syntax of terms, types, etc. |
18 | 5 |
*) |
6 |
||
7 |
signature PARSER = |
|
15752 | 8 |
sig |
1507 | 9 |
type gram |
10 |
val empty_gram: gram |
|
42288
2074b31650e6
discontinued special treatment of structure Syntax_Ext (formerly Syn_Ext);
wenzelm
parents:
42282
diff
changeset
|
11 |
val extend_gram: Syntax_Ext.xprod list -> gram -> gram |
45632
b23c42b9f78a
prefer Parser.make_gram over Parser.merge_gram, to approximate n-ary merges on theory import;
wenzelm
parents:
44102
diff
changeset
|
12 |
val make_gram: Syntax_Ext.xprod list -> gram |
1507 | 13 |
val pretty_gram: gram -> Pretty.T list |
14 |
datatype parsetree = |
|
15 |
Node of string * parsetree list | |
|
16 |
Tip of Lexicon.token |
|
42374
b9a6b465da25
clarified pretty_parsetree: suppress literal tokens;
wenzelm
parents:
42288
diff
changeset
|
17 |
exception PARSETREE of parsetree |
42205
22f5cc06c419
direct pretty printing of parsetrees -- prevent diagnostic output from crashing due to undeclared entities;
wenzelm
parents:
41378
diff
changeset
|
18 |
val pretty_parsetree: parsetree -> Pretty.T |
45641 | 19 |
val parse: gram -> string -> Lexicon.token list -> parsetree list |
26678 | 20 |
val guess_infix_lr: gram -> string -> (string * bool * bool * int) option |
41378 | 21 |
val branching_level: int Config.T |
15752 | 22 |
end; |
1507 | 23 |
|
15752 | 24 |
structure Parser: PARSER = |
18 | 25 |
struct |
15752 | 26 |
|
18 | 27 |
(** datatype gram **) |
28 |
||
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
29 |
(*production for the NTs are stored in a vector |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
30 |
so we can identify NTs by their index*) |
67533
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
31 |
type nt = int; |
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
32 |
|
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
33 |
type nts = Inttab.set; |
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
34 |
val nts_empty: nts = Inttab.empty; |
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
35 |
val nts_merge: nts * nts -> nts = Inttab.merge (K true); |
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
36 |
fun nts_insert nt : nts -> nts = Inttab.insert_set nt; |
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
37 |
fun nts_member (nts: nts) = Inttab.defined nts; |
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
38 |
fun nts_fold f (nts: nts) = Inttab.fold (f o #1) nts; |
67538 | 39 |
fun nts_subset (nts1: nts, nts2: nts) = Inttab.forall (nts_member nts2 o #1) nts1; |
40 |
fun nts_is_empty (nts: nts) = Inttab.is_empty nts; |
|
41 |
fun nts_is_unique (nts: nts) = nts_is_empty nts orelse Inttab.is_single nts; |
|
1147
57b5f55bf879
removed 'raw' productions from gram datatype; replaced mk_gram by add_prods;
clasohm
parents:
890
diff
changeset
|
42 |
|
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
43 |
datatype symb = |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
44 |
Terminal of Lexicon.token |
67533
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
45 |
| Nonterminal of nt * int; (*(tag, precedence)*) |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
46 |
|
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
47 |
type nt_gram = |
67533
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
48 |
((nts * Lexicon.token list) * |
67535
99c08d541a7a
tuned type: absorb NONE: token option as token_none: token;
wenzelm
parents:
67534
diff
changeset
|
49 |
(Lexicon.token * (symb list * string * int) list) list); |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
50 |
(*(([dependent_nts], [start_tokens]), [(start_token, [(rhs, name, prio)])])*) |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
51 |
(*depent_nts is a list of all NTs whose lookahead depends on this NT's lookahead*) |
1147
57b5f55bf879
removed 'raw' productions from gram datatype; replaced mk_gram by add_prods;
clasohm
parents:
890
diff
changeset
|
52 |
|
67533
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
53 |
val nt_gram_empty: nt_gram = ((nts_empty, []), []); |
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
54 |
|
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
55 |
type tags = nt Symtab.table; |
67531 | 56 |
val tags_empty: tags = Symtab.empty; |
57 |
fun tags_content (tags: tags) = sort_by #1 (Symtab.dest tags); |
|
58 |
fun tags_lookup (tags: tags) = Symtab.lookup tags; |
|
59 |
fun tags_insert tag (tags: tags) = Symtab.update_new tag tags; |
|
60 |
fun tags_name (tags: tags) = the o Inttab.lookup (Inttab.make (map swap (Symtab.dest tags))); |
|
61 |
||
62 |
type chains = unit Int_Graph.T; |
|
63 |
fun chains_preds (chains: chains) = Int_Graph.immediate_preds chains; |
|
64 |
fun chains_all_preds (chains: chains) = Int_Graph.all_preds chains; |
|
65 |
fun chains_all_succs (chains: chains) = Int_Graph.all_succs chains; |
|
66 |
val chains_empty: chains = Int_Graph.empty; |
|
67 |
fun chains_member (chains: chains) = Int_Graph.is_edge chains; |
|
68 |
fun chains_declare nt : chains -> chains = Int_Graph.default_node (nt, ()); |
|
69 |
fun chains_insert (from, to) = |
|
70 |
chains_declare from #> chains_declare to #> Int_Graph.add_edge (from, to); |
|
71 |
||
1147
57b5f55bf879
removed 'raw' productions from gram datatype; replaced mk_gram by add_prods;
clasohm
parents:
890
diff
changeset
|
72 |
datatype gram = |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
73 |
Gram of |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
74 |
{nt_count: int, |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
75 |
prod_count: int, |
67531 | 76 |
tags: tags, |
77 |
chains: chains, |
|
67533
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
78 |
lambdas: nts, |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
79 |
prods: nt_gram Vector.vector}; |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
80 |
(*"tags" is used to map NT names (i.e. strings) to tags; |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
81 |
chain productions are not stored as normal productions |
67517
add9a9f6a290
explicit graph for chains, which contains all nts as nodes;
wenzelm
parents:
67516
diff
changeset
|
82 |
but instead as an entry in "chains": from -> to; |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
83 |
lambda productions are stored as normal productions |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
84 |
and also as an entry in "lambdas"*) |
1147
57b5f55bf879
removed 'raw' productions from gram datatype; replaced mk_gram by add_prods;
clasohm
parents:
890
diff
changeset
|
85 |
|
67532 | 86 |
fun tokens_match toks = |
87 |
(case apply2 Lexicon.kind_of_token toks of |
|
88 |
(Lexicon.Literal, Lexicon.Literal) => op = (apply2 Lexicon.str_of_token toks) |
|
89 |
| kinds => op = kinds); |
|
90 |
||
91 |
val tokens_union = union tokens_match; |
|
92 |
val tokens_subtract = subtract tokens_match; |
|
1147
57b5f55bf879
removed 'raw' productions from gram datatype; replaced mk_gram by add_prods;
clasohm
parents:
890
diff
changeset
|
93 |
|
67535
99c08d541a7a
tuned type: absorb NONE: token option as token_none: token;
wenzelm
parents:
67534
diff
changeset
|
94 |
val token_none = Lexicon.Token (Lexicon.Space, "", Position.no_range); |
99c08d541a7a
tuned type: absorb NONE: token option as token_none: token;
wenzelm
parents:
67534
diff
changeset
|
95 |
|
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
96 |
(*productions for which no starting token is |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
97 |
known yet are associated with this token*) |
38713 | 98 |
val unknown_start = Lexicon.eof; |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
99 |
|
67516 | 100 |
fun get_start (tok :: _) = tok |
101 |
| get_start [] = unknown_start; |
|
102 |
||
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
103 |
(*convert productions to grammar; |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
104 |
prod_count is of type "int option" and is only updated if it is <> NONE*) |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
105 |
fun add_prods _ chains lambdas prod_count [] = (chains, lambdas, prod_count) |
62669 | 106 |
| add_prods prods chains lambdas prod_count ((lhs, new_prod as (rhs, _, pri)) :: ps) = |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
107 |
let |
67517
add9a9f6a290
explicit graph for chains, which contains all nts as nodes;
wenzelm
parents:
67516
diff
changeset
|
108 |
(*store chain if it does not already exist*) |
add9a9f6a290
explicit graph for chains, which contains all nts as nodes;
wenzelm
parents:
67516
diff
changeset
|
109 |
val (chain, new_chain, chains') = |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
110 |
(case (pri, rhs) of |
67517
add9a9f6a290
explicit graph for chains, which contains all nts as nodes;
wenzelm
parents:
67516
diff
changeset
|
111 |
(~1, [Nonterminal (from, ~1)]) => |
67531 | 112 |
if chains_member chains (from, lhs) |
67517
add9a9f6a290
explicit graph for chains, which contains all nts as nodes;
wenzelm
parents:
67516
diff
changeset
|
113 |
then (SOME from, false, chains) |
67531 | 114 |
else (SOME from, true, chains_insert (from, lhs) chains) |
115 |
| _ => (NONE, false, chains_declare lhs chains)); |
|
330
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
258
diff
changeset
|
116 |
|
67530
a7de81d847b0
tuned data structure: potentially more efficient add_prods;
wenzelm
parents:
67518
diff
changeset
|
117 |
(*propagate new chain in lookahead and lambdas; |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
118 |
added_starts is used later to associate existing |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
119 |
productions with new starting tokens*) |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
120 |
val (added_starts, lambdas') = |
67517
add9a9f6a290
explicit graph for chains, which contains all nts as nodes;
wenzelm
parents:
67516
diff
changeset
|
121 |
if not new_chain then ([], lambdas) |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
122 |
else |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
123 |
let (*lookahead of chain's source*) |
67517
add9a9f6a290
explicit graph for chains, which contains all nts as nodes;
wenzelm
parents:
67516
diff
changeset
|
124 |
val ((_, from_tks), _) = Array.sub (prods, the chain); |
1147
57b5f55bf879
removed 'raw' productions from gram datatype; replaced mk_gram by add_prods;
clasohm
parents:
890
diff
changeset
|
125 |
|
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
126 |
(*copy from's lookahead to chain's destinations*) |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
127 |
fun copy_lookahead [] added = added |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
128 |
| copy_lookahead (to :: tos) added = |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
129 |
let |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
130 |
val ((to_nts, to_tks), ps) = Array.sub (prods, to); |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
131 |
|
67536
f0b2cc2ad464
prefer specific tokens_subtract: subtle change of comparison via tokens_match;
wenzelm
parents:
67535
diff
changeset
|
132 |
val new_tks = tokens_subtract to_tks from_tks; (*added lookahead tokens*) |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
133 |
val _ = Array.update (prods, to, ((to_nts, to_tks @ new_tks), ps)); |
1147
57b5f55bf879
removed 'raw' productions from gram datatype; replaced mk_gram by add_prods;
clasohm
parents:
890
diff
changeset
|
134 |
in |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
135 |
copy_lookahead tos (if null new_tks then added else (to, new_tks) :: added) |
1147
57b5f55bf879
removed 'raw' productions from gram datatype; replaced mk_gram by add_prods;
clasohm
parents:
890
diff
changeset
|
136 |
end; |
57b5f55bf879
removed 'raw' productions from gram datatype; replaced mk_gram by add_prods;
clasohm
parents:
890
diff
changeset
|
137 |
|
67531 | 138 |
val tos = chains_all_succs chains' [lhs]; |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
139 |
in |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
140 |
(copy_lookahead tos [], |
67533
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
141 |
lambdas |> nts_member lambdas lhs ? fold nts_insert tos) |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
142 |
end; |
1147
57b5f55bf879
removed 'raw' productions from gram datatype; replaced mk_gram by add_prods;
clasohm
parents:
890
diff
changeset
|
143 |
|
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
144 |
(*test if new production can produce lambda |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
145 |
(rhs must either be empty or only consist of lambda NTs)*) |
67530
a7de81d847b0
tuned data structure: potentially more efficient add_prods;
wenzelm
parents:
67518
diff
changeset
|
146 |
val new_lambdas = |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
147 |
if forall |
67533
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
148 |
(fn Nonterminal (id, _) => nts_member lambdas' id |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
149 |
| Terminal _ => false) rhs |
67533
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
150 |
then SOME (filter_out (nts_member lambdas') (chains_all_succs chains' [lhs])) |
67530
a7de81d847b0
tuned data structure: potentially more efficient add_prods;
wenzelm
parents:
67518
diff
changeset
|
151 |
else NONE; |
67533
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
152 |
val lambdas'' = fold nts_insert (these new_lambdas) lambdas'; |
1147
57b5f55bf879
removed 'raw' productions from gram datatype; replaced mk_gram by add_prods;
clasohm
parents:
890
diff
changeset
|
153 |
|
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
154 |
(*list optional terminal and all nonterminals on which the lookahead |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
155 |
of a production depends*) |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
156 |
fun lookahead_dependency _ [] nts = (NONE, nts) |
42217 | 157 |
| lookahead_dependency _ (Terminal tk :: _) nts = (SOME tk, nts) |
158 |
| lookahead_dependency lambdas (Nonterminal (nt, _) :: symbs) nts = |
|
67533
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
159 |
if nts_member lambdas nt then |
67538 | 160 |
lookahead_dependency lambdas symbs (nts_insert nt nts) |
161 |
else (NONE, nts_insert nt nts); |
|
1147
57b5f55bf879
removed 'raw' productions from gram datatype; replaced mk_gram by add_prods;
clasohm
parents:
890
diff
changeset
|
162 |
|
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
163 |
(*get all known starting tokens for a nonterminal*) |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
164 |
fun starts_for_nt nt = snd (fst (Array.sub (prods, nt))); |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
165 |
|
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
166 |
(*update prods, lookaheads, and lambdas according to new lambda NTs*) |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
167 |
val (added_starts', lambdas') = |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
168 |
let |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
169 |
(*propagate added lambda NT*) |
42217 | 170 |
fun propagate_lambda [] added_starts lambdas = (added_starts, lambdas) |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
171 |
| propagate_lambda (l :: ls) added_starts lambdas = |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
172 |
let |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
173 |
(*get lookahead for lambda NT*) |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
174 |
val ((dependent, l_starts), _) = Array.sub (prods, l); |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
175 |
|
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
176 |
(*check productions whose lookahead may depend on lambda NT*) |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
177 |
fun examine_prods [] add_lambda nt_dependencies added_tks nt_prods = |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
178 |
(add_lambda, nt_dependencies, added_tks, nt_prods) |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
179 |
| examine_prods ((p as (rhs, _, _)) :: ps) add_lambda |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
180 |
nt_dependencies added_tks nt_prods = |
67538 | 181 |
let val (tk, nts) = lookahead_dependency lambdas rhs nts_empty in |
182 |
if nts_member nts l then (*update production's lookahead*) |
|
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
183 |
let |
67530
a7de81d847b0
tuned data structure: potentially more efficient add_prods;
wenzelm
parents:
67518
diff
changeset
|
184 |
val new_lambda = |
67538 | 185 |
is_none tk andalso nts_subset (nts, lambdas); |
1175
1b15a4b1a4f7
added comments; fixed a bug; reduced memory usage slightly
clasohm
parents:
1147
diff
changeset
|
186 |
|
42218
8e0a4d500e5b
streamlined token list operations, assuming that the order of union does not matter;
wenzelm
parents:
42217
diff
changeset
|
187 |
val new_tks = |
67534 | 188 |
the_list tk |
67538 | 189 |
|> nts_fold (tokens_union o starts_for_nt) nts |
67536
f0b2cc2ad464
prefer specific tokens_subtract: subtle change of comparison via tokens_match;
wenzelm
parents:
67535
diff
changeset
|
190 |
|> tokens_subtract l_starts; |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
191 |
|
67532 | 192 |
val added_tks' = tokens_union added_tks new_tks; |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
193 |
|
67538 | 194 |
val nt_dependencies' = nts_merge (nt_dependencies, nts); |
1147
57b5f55bf879
removed 'raw' productions from gram datatype; replaced mk_gram by add_prods;
clasohm
parents:
890
diff
changeset
|
195 |
|
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
196 |
(*associate production with new starting tokens*) |
67535
99c08d541a7a
tuned type: absorb NONE: token option as token_none: token;
wenzelm
parents:
67534
diff
changeset
|
197 |
fun copy ([]: Lexicon.token list) nt_prods = nt_prods |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
198 |
| copy (tk :: tks) nt_prods = |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
199 |
let |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
200 |
val old_prods = these (AList.lookup (op =) nt_prods tk); |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
201 |
val prods' = p :: old_prods; |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
202 |
in |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
203 |
nt_prods |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
204 |
|> AList.update (op =) (tk, prods') |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
205 |
|> copy tks |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
206 |
end; |
1147
57b5f55bf879
removed 'raw' productions from gram datatype; replaced mk_gram by add_prods;
clasohm
parents:
890
diff
changeset
|
207 |
|
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
208 |
val nt_prods' = |
67535
99c08d541a7a
tuned type: absorb NONE: token option as token_none: token;
wenzelm
parents:
67534
diff
changeset
|
209 |
copy (new_tks |> new_lambda ? cons token_none) nt_prods; |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
210 |
in |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
211 |
examine_prods ps (add_lambda orelse new_lambda) |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
212 |
nt_dependencies' added_tks' nt_prods' |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
213 |
end |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
214 |
else (*skip production*) |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
215 |
examine_prods ps add_lambda nt_dependencies added_tks nt_prods |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
216 |
end; |
1175
1b15a4b1a4f7
added comments; fixed a bug; reduced memory usage slightly
clasohm
parents:
1147
diff
changeset
|
217 |
|
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
218 |
(*check each NT whose lookahead depends on new lambda NT*) |
67533
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
219 |
fun process_nts nt (added_lambdas, added_starts) = |
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
220 |
let |
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
221 |
val ((old_nts, old_tks), nt_prods) = Array.sub (prods, nt); |
1147
57b5f55bf879
removed 'raw' productions from gram datatype; replaced mk_gram by add_prods;
clasohm
parents:
890
diff
changeset
|
222 |
|
67533
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
223 |
(*existing productions whose lookahead may depend on l*) |
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
224 |
val tk_prods = |
67535
99c08d541a7a
tuned type: absorb NONE: token option as token_none: token;
wenzelm
parents:
67534
diff
changeset
|
225 |
these (AList.lookup (op =) nt_prods (get_start l_starts)); |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
226 |
|
67533
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
227 |
(*add_lambda is true if an existing production of the nt |
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
228 |
produces lambda due to the new lambda NT l*) |
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
229 |
val (add_lambda, nt_dependencies, added_tks, nt_prods') = |
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
230 |
examine_prods tk_prods false nts_empty [] nt_prods; |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
231 |
|
67533
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
232 |
val new_nts = nts_merge (old_nts, nt_dependencies); |
330
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
258
diff
changeset
|
233 |
|
67533
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
234 |
val added_lambdas' = added_lambdas |> add_lambda ? cons nt; |
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
235 |
val _ = |
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
236 |
Array.update (prods, nt, ((new_nts, old_tks @ added_tks), nt_prods')); |
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
237 |
(*N.B. that because the tks component |
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
238 |
is used to access existing |
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
239 |
productions we have to add new |
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
240 |
tokens at the _end_ of the list*) |
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
241 |
val added_starts' = |
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
242 |
if null added_tks then added_starts |
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
243 |
else ((nt, added_tks) :: added_starts); |
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
244 |
in (added_lambdas', added_starts') end; |
1147
57b5f55bf879
removed 'raw' productions from gram datatype; replaced mk_gram by add_prods;
clasohm
parents:
890
diff
changeset
|
245 |
|
67533
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
246 |
val (added_lambdas, added_starts') = |
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
247 |
nts_fold process_nts dependent ([], added_starts); |
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
248 |
val added_lambdas' = filter_out (nts_member lambdas) added_lambdas; |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
249 |
in |
67530
a7de81d847b0
tuned data structure: potentially more efficient add_prods;
wenzelm
parents:
67518
diff
changeset
|
250 |
propagate_lambda (ls @ added_lambdas') added_starts' |
67533
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
251 |
(fold nts_insert added_lambdas' lambdas) |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
252 |
end; |
67530
a7de81d847b0
tuned data structure: potentially more efficient add_prods;
wenzelm
parents:
67518
diff
changeset
|
253 |
in |
a7de81d847b0
tuned data structure: potentially more efficient add_prods;
wenzelm
parents:
67518
diff
changeset
|
254 |
propagate_lambda |
67533
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
255 |
(nts_fold (fn l => not (nts_member lambdas l) ? cons l) lambdas'' []) |
67530
a7de81d847b0
tuned data structure: potentially more efficient add_prods;
wenzelm
parents:
67518
diff
changeset
|
256 |
added_starts lambdas'' |
a7de81d847b0
tuned data structure: potentially more efficient add_prods;
wenzelm
parents:
67518
diff
changeset
|
257 |
end; |
330
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
258
diff
changeset
|
258 |
|
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
259 |
(*insert production into grammar*) |
62669 | 260 |
val (added_starts', _) = |
67517
add9a9f6a290
explicit graph for chains, which contains all nts as nodes;
wenzelm
parents:
67516
diff
changeset
|
261 |
if is_some chain |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
262 |
then (added_starts', prod_count) (*don't store chain production*) |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
263 |
else |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
264 |
let |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
265 |
(*lookahead tokens of new production and on which |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
266 |
NTs lookahead depends*) |
67538 | 267 |
val (start_tk, start_nts) = lookahead_dependency lambdas' rhs nts_empty; |
1175
1b15a4b1a4f7
added comments; fixed a bug; reduced memory usage slightly
clasohm
parents:
1147
diff
changeset
|
268 |
|
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
269 |
val start_tks = |
67534 | 270 |
the_list start_tk |
67538 | 271 |
|> nts_fold (tokens_union o starts_for_nt) start_nts; |
330
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
258
diff
changeset
|
272 |
|
67535
99c08d541a7a
tuned type: absorb NONE: token option as token_none: token;
wenzelm
parents:
67534
diff
changeset
|
273 |
val start_tks' = |
99c08d541a7a
tuned type: absorb NONE: token option as token_none: token;
wenzelm
parents:
67534
diff
changeset
|
274 |
(if is_some new_lambdas then [token_none] |
99c08d541a7a
tuned type: absorb NONE: token option as token_none: token;
wenzelm
parents:
67534
diff
changeset
|
275 |
else if null start_tks then [unknown_start] |
99c08d541a7a
tuned type: absorb NONE: token option as token_none: token;
wenzelm
parents:
67534
diff
changeset
|
276 |
else []) @ start_tks; |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
277 |
|
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
278 |
(*add lhs NT to list of dependent NTs in lookahead*) |
67538 | 279 |
fun add_nts nt initial = |
280 |
(if initial then |
|
281 |
let val ((old_nts, old_tks), ps) = Array.sub (prods, nt) in |
|
282 |
if nts_member old_nts lhs then () |
|
283 |
else Array.update (prods, nt, ((nts_insert lhs old_nts, old_tks), ps)) |
|
284 |
end |
|
285 |
else (); false); |
|
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
286 |
|
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
287 |
(*add new start tokens to chained NTs' lookahead list; |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
288 |
also store new production for lhs NT*) |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
289 |
fun add_tks [] added prod_count = (added, prod_count) |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
290 |
| add_tks (nt :: nts) added prod_count = |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
291 |
let |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
292 |
val ((old_nts, old_tks), nt_prods) = Array.sub (prods, nt); |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
293 |
|
67532 | 294 |
val new_tks = tokens_subtract old_tks start_tks; |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
295 |
|
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
296 |
(*store new production*) |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
297 |
fun store [] prods is_new = |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
298 |
(prods, |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
299 |
if is_some prod_count andalso is_new then |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
300 |
Option.map (fn x => x + 1) prod_count |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
301 |
else prod_count, is_new) |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
302 |
| store (tk :: tks) prods is_new = |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
303 |
let |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
304 |
val tk_prods = these (AList.lookup (op =) prods tk); |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
305 |
|
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
306 |
(*if prod_count = NONE then we can assume that |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
307 |
grammar does not contain new production already*) |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
308 |
val (tk_prods', is_new') = |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
309 |
if is_some prod_count then |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
310 |
if member (op =) tk_prods new_prod then (tk_prods, false) |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
311 |
else (new_prod :: tk_prods, true) |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
312 |
else (new_prod :: tk_prods, true); |
330
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
258
diff
changeset
|
313 |
|
42218
8e0a4d500e5b
streamlined token list operations, assuming that the order of union does not matter;
wenzelm
parents:
42217
diff
changeset
|
314 |
val prods' = |
8e0a4d500e5b
streamlined token list operations, assuming that the order of union does not matter;
wenzelm
parents:
42217
diff
changeset
|
315 |
if is_new' then |
67535
99c08d541a7a
tuned type: absorb NONE: token option as token_none: token;
wenzelm
parents:
67534
diff
changeset
|
316 |
AList.update (op =) (tk: Lexicon.token, tk_prods') prods |
42218
8e0a4d500e5b
streamlined token list operations, assuming that the order of union does not matter;
wenzelm
parents:
42217
diff
changeset
|
317 |
else prods; |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
318 |
in store tks prods' (is_new orelse is_new') end; |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
319 |
|
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
320 |
val (nt_prods', prod_count', changed) = |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
321 |
if nt = lhs |
67535
99c08d541a7a
tuned type: absorb NONE: token option as token_none: token;
wenzelm
parents:
67534
diff
changeset
|
322 |
then store start_tks' nt_prods false |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
323 |
else (nt_prods, prod_count, false); |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
324 |
val _ = |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
325 |
if not changed andalso null new_tks then () |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
326 |
else Array.update (prods, nt, ((old_nts, old_tks @ new_tks), nt_prods')); |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
327 |
in |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
328 |
add_tks nts |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
329 |
(if null new_tks then added else (nt, new_tks) :: added) prod_count' |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
330 |
end; |
67538 | 331 |
val _ = nts_fold add_nts start_nts true; |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
332 |
in |
67531 | 333 |
add_tks (chains_all_succs chains' [lhs]) [] prod_count |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
334 |
end; |
1175
1b15a4b1a4f7
added comments; fixed a bug; reduced memory usage slightly
clasohm
parents:
1147
diff
changeset
|
335 |
|
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
336 |
(*associate productions with new lookaheads*) |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
337 |
val _ = |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
338 |
let |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
339 |
(*propagate added start tokens*) |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
340 |
fun add_starts [] = () |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
341 |
| add_starts ((changed_nt, new_tks) :: starts) = |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
342 |
let |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
343 |
(*token under which old productions which |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
344 |
depend on changed_nt could be stored*) |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
345 |
val key = |
67535
99c08d541a7a
tuned type: absorb NONE: token option as token_none: token;
wenzelm
parents:
67534
diff
changeset
|
346 |
find_first (not o member (op =) new_tks) (starts_for_nt changed_nt) |
99c08d541a7a
tuned type: absorb NONE: token option as token_none: token;
wenzelm
parents:
67534
diff
changeset
|
347 |
|> the_default unknown_start; |
18 | 348 |
|
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
349 |
(*copy productions whose lookahead depends on changed_nt; |
38713 | 350 |
if key = SOME unknown_start then tk_prods is used to hold |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
351 |
the productions not copied*) |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
352 |
fun update_prods [] result = result |
67533
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
353 |
| update_prods ((p as (rhs, _: string, _: nt)) :: ps) |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
354 |
(tk_prods, nt_prods) = |
1147
57b5f55bf879
removed 'raw' productions from gram datatype; replaced mk_gram by add_prods;
clasohm
parents:
890
diff
changeset
|
355 |
let |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
356 |
(*lookahead dependency for production*) |
67538 | 357 |
val (tk, depends) = lookahead_dependency lambdas' rhs nts_empty; |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
358 |
|
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
359 |
(*test if this production has to be copied*) |
67538 | 360 |
val update = nts_member depends changed_nt; |
330
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
258
diff
changeset
|
361 |
|
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
362 |
(*test if production could already be associated with |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
363 |
a member of new_tks*) |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
364 |
val lambda = |
67538 | 365 |
not (nts_is_unique depends) orelse |
366 |
not (nts_is_empty depends) andalso is_some tk |
|
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
367 |
andalso member (op =) new_tks (the tk); |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
368 |
|
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
369 |
(*associate production with new starting tokens*) |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
370 |
fun copy ([]: Lexicon.token list) nt_prods = nt_prods |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
371 |
| copy (tk :: tks) nt_prods = |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
372 |
let |
67535
99c08d541a7a
tuned type: absorb NONE: token option as token_none: token;
wenzelm
parents:
67534
diff
changeset
|
373 |
val tk_prods = these (AList.lookup (op =) nt_prods tk); |
330
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
258
diff
changeset
|
374 |
|
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
375 |
val tk_prods' = |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
376 |
if not lambda then p :: tk_prods |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
377 |
else insert (op =) p tk_prods; |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
378 |
(*if production depends on lambda NT we |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
379 |
have to look for duplicates*) |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
380 |
in |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
381 |
nt_prods |
67535
99c08d541a7a
tuned type: absorb NONE: token option as token_none: token;
wenzelm
parents:
67534
diff
changeset
|
382 |
|> AList.update (op =) (tk, tk_prods') |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
383 |
|> copy tks |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
384 |
end; |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
385 |
val result = |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
386 |
if update then (tk_prods, copy new_tks nt_prods) |
67535
99c08d541a7a
tuned type: absorb NONE: token option as token_none: token;
wenzelm
parents:
67534
diff
changeset
|
387 |
else if key = unknown_start then (p :: tk_prods, nt_prods) |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
388 |
else (tk_prods, nt_prods); |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
389 |
in update_prods ps result end; |
377
ab8917806779
lookaheads are now computed faster (during the grammar is built)
clasohm
parents:
373
diff
changeset
|
390 |
|
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
391 |
(*copy existing productions for new starting tokens*) |
67533
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
392 |
fun process_nts nt added = |
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
393 |
let |
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
394 |
val (lookahead as (old_nts, old_tks), nt_prods) = Array.sub (prods, nt); |
330
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
258
diff
changeset
|
395 |
|
67533
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
396 |
val tk_prods = these (AList.lookup (op =) nt_prods key); |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
397 |
|
67533
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
398 |
(*associate productions with new lookahead tokens*) |
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
399 |
val (tk_prods', nt_prods') = update_prods tk_prods ([], nt_prods); |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
400 |
|
67533
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
401 |
val nt_prods'' = |
67535
99c08d541a7a
tuned type: absorb NONE: token option as token_none: token;
wenzelm
parents:
67534
diff
changeset
|
402 |
if key = unknown_start then |
67533
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
403 |
AList.update (op =) (key, tk_prods') nt_prods' |
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
404 |
else nt_prods'; |
18 | 405 |
|
67533
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
406 |
val added_tks = tokens_subtract old_tks new_tks; |
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
407 |
in |
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
408 |
if null added_tks then |
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
409 |
(Array.update (prods, nt, (lookahead, nt_prods'')); |
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
410 |
added) |
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
411 |
else |
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
412 |
(Array.update (prods, nt, ((old_nts, added_tks @ old_tks), nt_prods'')); |
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
413 |
((nt, added_tks) :: added)) |
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
414 |
end; |
18 | 415 |
|
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
416 |
val ((dependent, _), _) = Array.sub (prods, changed_nt); |
67533
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
417 |
in add_starts (starts @ nts_fold process_nts dependent []) end; |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
418 |
in add_starts added_starts' end; |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
419 |
in add_prods prods chains' lambdas' prod_count ps end; |
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
46
diff
changeset
|
420 |
|
18 | 421 |
|
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
46
diff
changeset
|
422 |
(* pretty_gram *) |
18 | 423 |
|
1147
57b5f55bf879
removed 'raw' productions from gram datatype; replaced mk_gram by add_prods;
clasohm
parents:
890
diff
changeset
|
424 |
fun pretty_gram (Gram {tags, prods, chains, ...}) = |
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
46
diff
changeset
|
425 |
let |
67531 | 426 |
val print_nt = tags_name tags; |
67518 | 427 |
fun print_pri p = if p < 0 then "" else Symbol.make_sup ("(" ^ string_of_int p ^ ")"); |
1147
57b5f55bf879
removed 'raw' productions from gram datatype; replaced mk_gram by add_prods;
clasohm
parents:
890
diff
changeset
|
428 |
|
67513 | 429 |
fun pretty_symb (Terminal (Lexicon.Token (kind, s, _))) = |
430 |
if kind = Lexicon.Literal then Pretty.quote (Pretty.keyword1 s) else Pretty.str s |
|
431 |
| pretty_symb (Nonterminal (tag, p)) = Pretty.str (print_nt tag ^ print_pri p); |
|
18 | 432 |
|
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
46
diff
changeset
|
433 |
fun pretty_const "" = [] |
67513 | 434 |
| pretty_const c = [Pretty.str ("\<^bold>\<Rightarrow> " ^ quote c)]; |
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
46
diff
changeset
|
435 |
|
67513 | 436 |
fun prod_of_chain from = ([Nonterminal (from, ~1)], "", ~1); |
1147
57b5f55bf879
removed 'raw' productions from gram datatype; replaced mk_gram by add_prods;
clasohm
parents:
890
diff
changeset
|
437 |
|
67513 | 438 |
fun pretty_prod (name, tag) = |
439 |
(fold (union (op =) o #2) (#2 (Vector.sub (prods, tag))) [] @ |
|
67531 | 440 |
map prod_of_chain (chains_preds chains tag)) |
67513 | 441 |
|> map (fn (symbs, const, p) => |
442 |
Pretty.block (Pretty.breaks |
|
443 |
(Pretty.str (name ^ print_pri p ^ " =") :: map pretty_symb symbs @ pretty_const const))); |
|
67531 | 444 |
in maps pretty_prod (tags_content tags) end; |
1147
57b5f55bf879
removed 'raw' productions from gram datatype; replaced mk_gram by add_prods;
clasohm
parents:
890
diff
changeset
|
445 |
|
57b5f55bf879
removed 'raw' productions from gram datatype; replaced mk_gram by add_prods;
clasohm
parents:
890
diff
changeset
|
446 |
|
42217 | 447 |
|
1438 | 448 |
(** Operations on gramars **) |
1147
57b5f55bf879
removed 'raw' productions from gram datatype; replaced mk_gram by add_prods;
clasohm
parents:
890
diff
changeset
|
449 |
|
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
450 |
val empty_gram = |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
451 |
Gram |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
452 |
{nt_count = 0, |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
453 |
prod_count = 0, |
67531 | 454 |
tags = tags_empty, |
455 |
chains = chains_empty, |
|
67533
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
456 |
lambdas = nts_empty, |
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
457 |
prods = Vector.fromList [nt_gram_empty]}; |
1147
57b5f55bf879
removed 'raw' productions from gram datatype; replaced mk_gram by add_prods;
clasohm
parents:
890
diff
changeset
|
458 |
|
1438 | 459 |
|
460 |
(*Add productions to a grammar*) |
|
37684 | 461 |
fun extend_gram [] gram = gram |
462 |
| extend_gram xprods (Gram {nt_count, prod_count, tags, chains, lambdas, prods}) = |
|
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
463 |
let |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
464 |
(*Get tag for existing nonterminal or create a new one*) |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
465 |
fun get_tag nt_count tags nt = |
67531 | 466 |
(case tags_lookup tags nt of |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
467 |
SOME tag => (nt_count, tags, tag) |
67531 | 468 |
| NONE => (nt_count + 1, tags_insert (nt, nt_count) tags, nt_count)); |
1438 | 469 |
|
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
470 |
(*Convert symbols to the form used by the parser; |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
471 |
delimiters and predefined terms are stored as terminals, |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
472 |
nonterminals are converted to integer tags*) |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
473 |
fun symb_of [] nt_count tags result = (nt_count, tags, rev result) |
42288
2074b31650e6
discontinued special treatment of structure Syntax_Ext (formerly Syn_Ext);
wenzelm
parents:
42282
diff
changeset
|
474 |
| symb_of (Syntax_Ext.Delim s :: ss) nt_count tags result = |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
475 |
symb_of ss nt_count tags |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
476 |
(Terminal (Lexicon.Token (Lexicon.Literal, s, Position.no_range)) :: result) |
42288
2074b31650e6
discontinued special treatment of structure Syntax_Ext (formerly Syn_Ext);
wenzelm
parents:
42282
diff
changeset
|
477 |
| symb_of (Syntax_Ext.Argument (s, p) :: ss) nt_count tags result = |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
478 |
let |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
479 |
val (nt_count', tags', new_symb) = |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
480 |
(case Lexicon.predef_term s of |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
481 |
NONE => |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
482 |
let val (nt_count', tags', s_tag) = get_tag nt_count tags s; |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
483 |
in (nt_count', tags', Nonterminal (s_tag, p)) end |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
484 |
| SOME tk => (nt_count, tags, Terminal tk)); |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
485 |
in symb_of ss nt_count' tags' (new_symb :: result) end |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
486 |
| symb_of (_ :: ss) nt_count tags result = symb_of ss nt_count tags result; |
1147
57b5f55bf879
removed 'raw' productions from gram datatype; replaced mk_gram by add_prods;
clasohm
parents:
890
diff
changeset
|
487 |
|
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
488 |
(*Convert list of productions by invoking symb_of for each of them*) |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
489 |
fun prod_of [] nt_count prod_count tags result = |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
490 |
(nt_count, prod_count, tags, result) |
42288
2074b31650e6
discontinued special treatment of structure Syntax_Ext (formerly Syn_Ext);
wenzelm
parents:
42282
diff
changeset
|
491 |
| prod_of (Syntax_Ext.XProd (lhs, xsymbs, const, pri) :: ps) |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
492 |
nt_count prod_count tags result = |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
493 |
let |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
494 |
val (nt_count', tags', lhs_tag) = get_tag nt_count tags lhs; |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
495 |
val (nt_count'', tags'', prods) = symb_of xsymbs nt_count' tags' []; |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
496 |
in |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
497 |
prod_of ps nt_count'' (prod_count + 1) tags'' |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
498 |
((lhs_tag, (prods, const, pri)) :: result) |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
499 |
end; |
1147
57b5f55bf879
removed 'raw' productions from gram datatype; replaced mk_gram by add_prods;
clasohm
parents:
890
diff
changeset
|
500 |
|
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
501 |
val (nt_count', prod_count', tags', xprods') = |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
502 |
prod_of xprods nt_count prod_count tags []; |
1147
57b5f55bf879
removed 'raw' productions from gram datatype; replaced mk_gram by add_prods;
clasohm
parents:
890
diff
changeset
|
503 |
|
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
504 |
(*Copy array containing productions of old grammar; |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
505 |
this has to be done to preserve the old grammar while being able |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
506 |
to change the array's content*) |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
507 |
val prods' = |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
508 |
let |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
509 |
fun get_prod i = |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
510 |
if i < nt_count then Vector.sub (prods, i) |
67533
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
511 |
else nt_gram_empty; |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
512 |
in Array.tabulate (nt_count', get_prod) end; |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
513 |
|
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
514 |
(*Add new productions to old ones*) |
67517
add9a9f6a290
explicit graph for chains, which contains all nts as nodes;
wenzelm
parents:
67516
diff
changeset
|
515 |
val (chains', lambdas', _) = add_prods prods' chains lambdas NONE xprods'; |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
516 |
in |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
517 |
Gram |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
518 |
{nt_count = nt_count', |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
519 |
prod_count = prod_count', |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
520 |
tags = tags', |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
521 |
chains = chains', |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
522 |
lambdas = lambdas', |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
523 |
prods = Array.vector prods'} |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
524 |
end; |
18 | 525 |
|
45632
b23c42b9f78a
prefer Parser.make_gram over Parser.merge_gram, to approximate n-ary merges on theory import;
wenzelm
parents:
44102
diff
changeset
|
526 |
fun make_gram xprods = extend_gram xprods empty_gram; |
1147
57b5f55bf879
removed 'raw' productions from gram datatype; replaced mk_gram by add_prods;
clasohm
parents:
890
diff
changeset
|
527 |
|
18 | 528 |
|
42217 | 529 |
|
42374
b9a6b465da25
clarified pretty_parsetree: suppress literal tokens;
wenzelm
parents:
42288
diff
changeset
|
530 |
(** parser **) |
b9a6b465da25
clarified pretty_parsetree: suppress literal tokens;
wenzelm
parents:
42288
diff
changeset
|
531 |
|
b9a6b465da25
clarified pretty_parsetree: suppress literal tokens;
wenzelm
parents:
42288
diff
changeset
|
532 |
(* parsetree *) |
18 | 533 |
|
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
46
diff
changeset
|
534 |
datatype parsetree = |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
46
diff
changeset
|
535 |
Node of string * parsetree list | |
37683 | 536 |
Tip of Lexicon.token; |
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
46
diff
changeset
|
537 |
|
42374
b9a6b465da25
clarified pretty_parsetree: suppress literal tokens;
wenzelm
parents:
42288
diff
changeset
|
538 |
exception PARSETREE of parsetree; |
b9a6b465da25
clarified pretty_parsetree: suppress literal tokens;
wenzelm
parents:
42288
diff
changeset
|
539 |
|
b9a6b465da25
clarified pretty_parsetree: suppress literal tokens;
wenzelm
parents:
42288
diff
changeset
|
540 |
fun pretty_parsetree parsetree = |
b9a6b465da25
clarified pretty_parsetree: suppress literal tokens;
wenzelm
parents:
42288
diff
changeset
|
541 |
let |
b9a6b465da25
clarified pretty_parsetree: suppress literal tokens;
wenzelm
parents:
42288
diff
changeset
|
542 |
fun pretty (Node (c, pts)) = |
b9a6b465da25
clarified pretty_parsetree: suppress literal tokens;
wenzelm
parents:
42288
diff
changeset
|
543 |
[Pretty.enclose "(" ")" (Pretty.breaks (Pretty.quote (Pretty.str c) :: maps pretty pts))] |
b9a6b465da25
clarified pretty_parsetree: suppress literal tokens;
wenzelm
parents:
42288
diff
changeset
|
544 |
| pretty (Tip tok) = |
b9a6b465da25
clarified pretty_parsetree: suppress literal tokens;
wenzelm
parents:
42288
diff
changeset
|
545 |
if Lexicon.valued_token tok then [Pretty.str (Lexicon.str_of_token tok)] else []; |
b9a6b465da25
clarified pretty_parsetree: suppress literal tokens;
wenzelm
parents:
42288
diff
changeset
|
546 |
in (case pretty parsetree of [prt] => prt | _ => raise PARSETREE parsetree) end; |
b9a6b465da25
clarified pretty_parsetree: suppress literal tokens;
wenzelm
parents:
42288
diff
changeset
|
547 |
|
b9a6b465da25
clarified pretty_parsetree: suppress literal tokens;
wenzelm
parents:
42288
diff
changeset
|
548 |
|
b9a6b465da25
clarified pretty_parsetree: suppress literal tokens;
wenzelm
parents:
42288
diff
changeset
|
549 |
(* parser state *) |
42205
22f5cc06c419
direct pretty printing of parsetrees -- prevent diagnostic output from crashing due to undeclared entities;
wenzelm
parents:
41378
diff
changeset
|
550 |
|
18 | 551 |
type state = |
67533
f253e5eaf995
clarified types and operations: potentially more efficient add_prods;
wenzelm
parents:
67532
diff
changeset
|
552 |
nt * int * (*identification and production precedence*) |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
553 |
parsetree list * (*already parsed nonterminals on rhs*) |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
554 |
symb list * (*rest of rhs*) |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
555 |
string * (*name of production*) |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
556 |
int; (*index for previous state list*) |
18 | 557 |
|
558 |
||
38713 | 559 |
(*Get all rhss with precedence >= min_prec*) |
42217 | 560 |
fun get_RHS min_prec = filter (fn (_, _, prec: int) => prec >= min_prec); |
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
46
diff
changeset
|
561 |
|
38713 | 562 |
(*Get all rhss with precedence >= min_prec and < max_prec*) |
563 |
fun get_RHS' min_prec max_prec = |
|
42217 | 564 |
filter (fn (_, _, prec: int) => prec >= min_prec andalso prec < max_prec); |
18 | 565 |
|
330
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
258
diff
changeset
|
566 |
(*Make states using a list of rhss*) |
62669 | 567 |
fun mk_states i lhs_ID rhss = |
38713 | 568 |
let fun mk_state (rhs, id, prod_prec) = (lhs_ID, prod_prec, [], rhs, id, i); |
569 |
in map mk_state rhss end; |
|
697
40f72ab196f8
changed warning for extremely ambiguous expressions
clasohm
parents:
682
diff
changeset
|
570 |
|
15752 | 571 |
(*Add parse tree to list and eliminate duplicates |
330
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
258
diff
changeset
|
572 |
saving the maximum precedence*) |
42217 | 573 |
fun conc (t: parsetree list, prec: int) [] = (NONE, [(t, prec)]) |
330
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
258
diff
changeset
|
574 |
| conc (t, prec) ((t', prec') :: ts) = |
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
258
diff
changeset
|
575 |
if t = t' then |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
576 |
(SOME prec', |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
577 |
if prec' >= prec then (t', prec') :: ts |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
578 |
else (t, prec) :: ts) |
330
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
258
diff
changeset
|
579 |
else |
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
258
diff
changeset
|
580 |
let val (n, ts') = conc (t, prec) ts |
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
258
diff
changeset
|
581 |
in (n, (t', prec') :: ts') end; |
18 | 582 |
|
330
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
258
diff
changeset
|
583 |
(*Update entry in used*) |
42226
cb650789f2f0
use standard tables with standard argument order;
wenzelm
parents:
42222
diff
changeset
|
584 |
fun update_trees (A, t) used = |
cb650789f2f0
use standard tables with standard argument order;
wenzelm
parents:
42222
diff
changeset
|
585 |
let |
cb650789f2f0
use standard tables with standard argument order;
wenzelm
parents:
42222
diff
changeset
|
586 |
val (i, ts) = the (Inttab.lookup used A); |
cb650789f2f0
use standard tables with standard argument order;
wenzelm
parents:
42222
diff
changeset
|
587 |
val (n, ts') = conc t ts; |
cb650789f2f0
use standard tables with standard argument order;
wenzelm
parents:
42222
diff
changeset
|
588 |
in (n, Inttab.update (A, (i, ts')) used) end; |
18 | 589 |
|
330
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
258
diff
changeset
|
590 |
(*Replace entry in used*) |
42226
cb650789f2f0
use standard tables with standard argument order;
wenzelm
parents:
42222
diff
changeset
|
591 |
fun update_prec (A, prec) = |
cb650789f2f0
use standard tables with standard argument order;
wenzelm
parents:
42222
diff
changeset
|
592 |
Inttab.map_entry A (fn (_, ts) => (prec, ts)); |
18 | 593 |
|
42220 | 594 |
fun getS A max_prec NONE Si = |
595 |
filter |
|
596 |
(fn (_, _, _, Nonterminal (B, prec) :: _, _, _) => A = B andalso prec <= max_prec |
|
597 |
| _ => false) Si |
|
598 |
| getS A max_prec (SOME min_prec) Si = |
|
599 |
filter |
|
600 |
(fn (_, _, _, Nonterminal (B, prec) :: _, _, _) => |
|
601 |
A = B andalso prec > min_prec andalso prec <= max_prec |
|
602 |
| _ => false) Si; |
|
18 | 603 |
|
62669 | 604 |
fun get_states Estate j A max_prec = |
33317 | 605 |
filter |
38713 | 606 |
(fn (_, _, _, Nonterminal (B, prec) :: _, _, _) => A = B andalso prec <= max_prec |
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
46
diff
changeset
|
607 |
| _ => false) |
62669 | 608 |
(Array.sub (Estate, j)); |
18 | 609 |
|
610 |
||
42219 | 611 |
fun movedot_term c (A, j, ts, Terminal a :: sa, id, i) = |
42282
4fa41e068ff0
report literal tokens according to parsetree head;
wenzelm
parents:
42226
diff
changeset
|
612 |
if Lexicon.valued_token c orelse id <> "" |
4fa41e068ff0
report literal tokens according to parsetree head;
wenzelm
parents:
42226
diff
changeset
|
613 |
then (A, j, Tip c :: ts, sa, id, i) |
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
46
diff
changeset
|
614 |
else (A, j, ts, sa, id, i); |
18 | 615 |
|
42219 | 616 |
fun movedot_nonterm tt (A, j, ts, Nonterminal _ :: sa, id, i) = |
42282
4fa41e068ff0
report literal tokens according to parsetree head;
wenzelm
parents:
42226
diff
changeset
|
617 |
(A, j, tt @ ts, sa, id, i); |
18 | 618 |
|
42219 | 619 |
fun movedot_lambda [] _ = [] |
42221 | 620 |
| movedot_lambda ((t, ki) :: ts) (state as (B, j, tss, Nonterminal (A, k) :: sa, id, i)) = |
42282
4fa41e068ff0
report literal tokens according to parsetree head;
wenzelm
parents:
42226
diff
changeset
|
621 |
if k <= ki then (B, j, t @ tss, sa, id, i) :: movedot_lambda ts state |
42221 | 622 |
else movedot_lambda ts state; |
18 | 623 |
|
624 |
||
41378 | 625 |
(*trigger value for warnings*) |
56438 | 626 |
val branching_level = |
64556 | 627 |
Config.int (Config.declare ("syntax_branching_level", \<^here>) (fn _ => Config.Int 600)); |
18 | 628 |
|
1147
57b5f55bf879
removed 'raw' productions from gram datatype; replaced mk_gram by add_prods;
clasohm
parents:
890
diff
changeset
|
629 |
(*get all productions of a NT and NTs chained to it which can |
57b5f55bf879
removed 'raw' productions from gram datatype; replaced mk_gram by add_prods;
clasohm
parents:
890
diff
changeset
|
630 |
be started by specified token*) |
67515 | 631 |
fun prods_for (Gram {prods, chains, ...}) include_none tk nts = |
37683 | 632 |
let |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
633 |
fun token_assoc (list, key) = |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
634 |
let |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
635 |
fun assoc [] result = result |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
636 |
| assoc ((keyi, pi) :: pairs) result = |
67535
99c08d541a7a
tuned type: absorb NONE: token option as token_none: token;
wenzelm
parents:
67534
diff
changeset
|
637 |
if keyi <> token_none andalso tokens_match (keyi, key) |
99c08d541a7a
tuned type: absorb NONE: token option as token_none: token;
wenzelm
parents:
67534
diff
changeset
|
638 |
orelse include_none andalso keyi = token_none then |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
639 |
assoc pairs (pi @ result) |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
640 |
else assoc pairs result; |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
641 |
in assoc list [] end; |
1147
57b5f55bf879
removed 'raw' productions from gram datatype; replaced mk_gram by add_prods;
clasohm
parents:
890
diff
changeset
|
642 |
|
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
643 |
fun get_prods [] result = result |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
644 |
| get_prods (nt :: nts) result = |
38711
79d3cbfb4730
keep persistent production tables as immutable vectors -- potential performance improvement on modern hardware;
wenzelm
parents:
37852
diff
changeset
|
645 |
let val nt_prods = snd (Vector.sub (prods, nt)); |
42217 | 646 |
in get_prods nts (token_assoc (nt_prods, tk) @ result) end; |
67531 | 647 |
in get_prods (chains_all_preds chains nts) [] end; |
1147
57b5f55bf879
removed 'raw' productions from gram datatype; replaced mk_gram by add_prods;
clasohm
parents:
890
diff
changeset
|
648 |
|
57b5f55bf879
removed 'raw' productions from gram datatype; replaced mk_gram by add_prods;
clasohm
parents:
890
diff
changeset
|
649 |
|
67515 | 650 |
fun PROCESSS gram Estate i c states = |
37683 | 651 |
let |
67515 | 652 |
fun all_prods_for nt = prods_for gram true c [nt]; |
330
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
258
diff
changeset
|
653 |
|
62669 | 654 |
fun processS _ [] (Si, Sii) = (Si, Sii) |
37683 | 655 |
| processS used (S :: States) (Si, Sii) = |
656 |
(case S of |
|
38713 | 657 |
(_, _, _, Nonterminal (nt, min_prec) :: _, _, _) => |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
658 |
let (*predictor operation*) |
37683 | 659 |
val (used', new_states) = |
42226
cb650789f2f0
use standard tables with standard argument order;
wenzelm
parents:
42222
diff
changeset
|
660 |
(case Inttab.lookup used nt of |
38713 | 661 |
SOME (used_prec, l) => (*nonterminal has been processed*) |
662 |
if used_prec <= min_prec then |
|
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
663 |
(*wanted precedence has been processed*) |
42219 | 664 |
(used, movedot_lambda l S) |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
665 |
else (*wanted precedence hasn't been parsed yet*) |
37683 | 666 |
let |
667 |
val tk_prods = all_prods_for nt; |
|
42217 | 668 |
val States' = |
62669 | 669 |
mk_states i nt (get_RHS' min_prec used_prec tk_prods); |
42219 | 670 |
in (update_prec (nt, min_prec) used, movedot_lambda l S @ States') end |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
671 |
| NONE => (*nonterminal is parsed for the first time*) |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
672 |
let |
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
673 |
val tk_prods = all_prods_for nt; |
62669 | 674 |
val States' = mk_states i nt (get_RHS min_prec tk_prods); |
42226
cb650789f2f0
use standard tables with standard argument order;
wenzelm
parents:
42222
diff
changeset
|
675 |
in (Inttab.update (nt, (min_prec, [])) used, States') end); |
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
46
diff
changeset
|
676 |
in |
37683 | 677 |
processS used' (new_states @ States) (S :: Si, Sii) |
15752 | 678 |
end |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
679 |
| (_, _, _, Terminal a :: _, _, _) => (*scanner operation*) |
37683 | 680 |
processS used States |
67532 | 681 |
(S :: Si, if tokens_match (a, c) then movedot_term c S :: Sii else Sii) |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
682 |
| (A, prec, ts, [], id, j) => (*completer operation*) |
42222
ff50c436b199
accumulate parsetrees in canonical reverse order;
wenzelm
parents:
42221
diff
changeset
|
683 |
let val tt = if id = "" then ts else [Node (id, rev ts)] in |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
684 |
if j = i then (*lambda production?*) |
37683 | 685 |
let |
42226
cb650789f2f0
use standard tables with standard argument order;
wenzelm
parents:
42222
diff
changeset
|
686 |
val (prec', used') = update_trees (A, (tt, prec)) used; |
42220 | 687 |
val Slist = getS A prec prec' Si; |
688 |
val States' = map (movedot_nonterm tt) Slist; |
|
689 |
in processS used' (States' @ States) (S :: Si, Sii) end |
|
37683 | 690 |
else |
62669 | 691 |
let val Slist = get_states Estate j A prec |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
692 |
in processS used (map (movedot_nonterm tt) Slist @ States) (S :: Si, Sii) end |
37683 | 693 |
end) |
42226
cb650789f2f0
use standard tables with standard argument order;
wenzelm
parents:
42222
diff
changeset
|
694 |
in processS Inttab.empty states ([], []) end; |
18 | 695 |
|
696 |
||
67515 | 697 |
fun produce gram stateset i indata prev_token = |
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
46
diff
changeset
|
698 |
(case Array.sub (stateset, i) of |
25986
26f1e4c172c3
syntax error: reduced spam -- print expected nonterminals instead of terminals;
wenzelm
parents:
24245
diff
changeset
|
699 |
[] => |
26f1e4c172c3
syntax error: reduced spam -- print expected nonterminals instead of terminals;
wenzelm
parents:
24245
diff
changeset
|
700 |
let |
37683 | 701 |
val toks = if Lexicon.is_eof prev_token then indata else prev_token :: indata; |
48992 | 702 |
val pos = Position.here (Lexicon.pos_of_token prev_token); |
27801
0d0adaf0228d
datatype token: maintain range, tuned representation;
wenzelm
parents:
26678
diff
changeset
|
703 |
in |
55624 | 704 |
if null toks then |
705 |
error ("Inner syntax error: unexpected end of input" ^ pos) |
|
706 |
else |
|
707 |
error ("Inner syntax error" ^ pos ^ |
|
708 |
Markup.markup Markup.no_report |
|
709 |
("\n" ^ Pretty.string_of |
|
710 |
(Pretty.block [ |
|
711 |
Pretty.str "at", Pretty.brk 1, |
|
712 |
Pretty.block |
|
713 |
(Pretty.str "\"" :: |
|
714 |
Pretty.breaks (map (Pretty.str o Lexicon.str_of_token) (#1 (split_last toks))) @ |
|
715 |
[Pretty.str "\""])]))) |
|
27801
0d0adaf0228d
datatype token: maintain range, tuned representation;
wenzelm
parents:
26678
diff
changeset
|
716 |
end |
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
46
diff
changeset
|
717 |
| s => |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
718 |
(case indata of |
42218
8e0a4d500e5b
streamlined token list operations, assuming that the order of union does not matter;
wenzelm
parents:
42217
diff
changeset
|
719 |
[] => s |
42217 | 720 |
| c :: cs => |
721 |
let |
|
67515 | 722 |
val (si, sii) = PROCESSS gram stateset i c s; |
42217 | 723 |
val _ = Array.update (stateset, i, si); |
724 |
val _ = Array.update (stateset, i + 1, sii); |
|
67515 | 725 |
in produce gram stateset (i + 1) cs c end)); |
18 | 726 |
|
727 |
||
42217 | 728 |
fun get_trees states = map_filter (fn (_, _, [pt], _, _, _) => SOME pt | _ => NONE) states; |
18 | 729 |
|
67515 | 730 |
fun earley (gram as Gram {tags, ...}) startsymbol indata = |
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
46
diff
changeset
|
731 |
let |
37683 | 732 |
val start_tag = |
67531 | 733 |
(case tags_lookup tags startsymbol of |
37683 | 734 |
SOME tag => tag |
40959 | 735 |
| NONE => error ("Inner syntax: bad grammar root symbol " ^ quote startsymbol)); |
37683 | 736 |
val S0 = [(~1, 0, [], [Nonterminal (start_tag, 0), Terminal Lexicon.eof], "", 0)]; |
330
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
258
diff
changeset
|
737 |
val s = length indata + 1; |
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
46
diff
changeset
|
738 |
val Estate = Array.array (s, []); |
38712
f7688fd819a8
some attempts to recover Isabelle/ML style from the depths of time;
wenzelm
parents:
38711
diff
changeset
|
739 |
val _ = Array.update (Estate, 0, S0); |
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
46
diff
changeset
|
740 |
in |
67515 | 741 |
get_trees (produce gram Estate 0 indata Lexicon.eof) |
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
46
diff
changeset
|
742 |
end; |
18 | 743 |
|
744 |
||
67515 | 745 |
fun parse gram start toks = |
27801
0d0adaf0228d
datatype token: maintain range, tuned representation;
wenzelm
parents:
26678
diff
changeset
|
746 |
let |
0d0adaf0228d
datatype token: maintain range, tuned representation;
wenzelm
parents:
26678
diff
changeset
|
747 |
val end_pos = |
0d0adaf0228d
datatype token: maintain range, tuned representation;
wenzelm
parents:
26678
diff
changeset
|
748 |
(case try List.last toks of |
0d0adaf0228d
datatype token: maintain range, tuned representation;
wenzelm
parents:
26678
diff
changeset
|
749 |
NONE => Position.none |
37683 | 750 |
| SOME (Lexicon.Token (_, _, (_, end_pos))) => end_pos); |
27801
0d0adaf0228d
datatype token: maintain range, tuned representation;
wenzelm
parents:
26678
diff
changeset
|
751 |
val r = |
67515 | 752 |
(case earley gram start (toks @ [Lexicon.mk_eof end_pos]) of |
37852
a902f158b4fc
eliminated old-style sys_error/SYS_ERROR in favour of exception Fail -- after careful checking that there is no overlap with existing handling of that;
wenzelm
parents:
37684
diff
changeset
|
753 |
[] => raise Fail "Inner syntax: no parse trees" |
27801
0d0adaf0228d
datatype token: maintain range, tuned representation;
wenzelm
parents:
26678
diff
changeset
|
754 |
| pts => pts); |
0d0adaf0228d
datatype token: maintain range, tuned representation;
wenzelm
parents:
26678
diff
changeset
|
755 |
in r end; |
26678 | 756 |
|
757 |
||
758 |
fun guess_infix_lr (Gram gram) c = (*based on educated guess*) |
|
759 |
let |
|
38711
79d3cbfb4730
keep persistent production tables as immutable vectors -- potential performance improvement on modern hardware;
wenzelm
parents:
37852
diff
changeset
|
760 |
fun freeze a = map_range (curry Vector.sub a) (Vector.length a); |
27801
0d0adaf0228d
datatype token: maintain range, tuned representation;
wenzelm
parents:
26678
diff
changeset
|
761 |
val prods = maps snd (maps snd (freeze (#prods gram))); |
37683 | 762 |
fun guess (SOME ([Nonterminal (_, k), |
763 |
Terminal (Lexicon.Token (Lexicon.Literal, s, _)), Nonterminal (_, l)], _, j)) = |
|
26678 | 764 |
if k = j andalso l = j + 1 then SOME (s, true, false, j) |
765 |
else if k = j + 1 then if l = j then SOME (s, false, true, j) |
|
766 |
else if l = j + 1 then SOME (s, false, false, j) |
|
767 |
else NONE |
|
768 |
else NONE |
|
769 |
| guess _ = NONE; |
|
770 |
in guess (find_first (fn (_, s, _) => s = c) prods) end; |
|
18 | 771 |
|
772 |
end; |