author | haftmann |
Thu, 08 Nov 2018 09:11:52 +0100 | |
changeset 69260 | 0a9688695a1b |
parent 63185 | 08369e33c185 |
child 74563 | 042041c0ebeb |
permissions | -rw-r--r-- |
60248
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
1 |
(* Title: HOL/Eisbach/parse_tools.ML |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
2 |
Author: Daniel Matichuk, NICTA/UNSW |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
3 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
4 |
Simple tools for deferred stateful token values. |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
5 |
*) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
6 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
7 |
signature PARSE_TOOLS = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
8 |
sig |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
9 |
datatype ('a, 'b) parse_val = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
10 |
Real_Val of 'a |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
11 |
| Parse_Val of 'b * ('a -> unit); |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
12 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
13 |
val is_real_val : ('a, 'b) parse_val -> bool |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
14 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
15 |
val the_real_val : ('a, 'b) parse_val -> 'a |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
16 |
val the_parse_val : ('a, 'b) parse_val -> 'b |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
17 |
val the_parse_fun : ('a, 'b) parse_val -> ('a -> unit) |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
18 |
|
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
19 |
val parse_val_cases: ('b -> 'a) -> ('a, 'b) parse_val -> ('a * ('a -> unit)) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
20 |
|
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
21 |
val parse_term_val : 'b parser -> (term, 'b) parse_val parser |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
22 |
val name_term : (term, string) parse_val parser |
63185
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
63120
diff
changeset
|
23 |
|
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
63120
diff
changeset
|
24 |
val parse_thm_val : 'b parser -> (thm, 'b) parse_val parser |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
25 |
end; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
26 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
27 |
structure Parse_Tools: PARSE_TOOLS = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
28 |
struct |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
29 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
30 |
datatype ('a, 'b) parse_val = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
31 |
Real_Val of 'a |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
32 |
| Parse_Val of 'b * ('a -> unit); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
33 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
34 |
fun parse_term_val scan = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
35 |
Scan.ahead Parse.not_eof -- Scan.ahead (Scan.option Args.internal_term) -- scan >> |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
36 |
(fn ((_, SOME t), _) => Real_Val t |
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
60285
diff
changeset
|
37 |
| ((tok, NONE), v) => Parse_Val (v, fn t => ignore (Token.assign (SOME (Token.Term t)) tok))); |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
38 |
|
63120
629a4c5e953e
embedded content may be delimited via cartouches;
wenzelm
parents:
61814
diff
changeset
|
39 |
val name_term = parse_term_val Args.embedded_inner_syntax; |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
40 |
|
63185
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
63120
diff
changeset
|
41 |
fun parse_thm_val scan = |
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
63120
diff
changeset
|
42 |
Scan.ahead Parse.not_eof -- Scan.ahead (Scan.option (Args.internal_fact >> the_single)) -- scan >> |
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
63120
diff
changeset
|
43 |
(fn ((_, SOME t), _) => Real_Val t |
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
63120
diff
changeset
|
44 |
| ((tok, NONE), v) => Parse_Val (v, fn t => ignore (Token.assign (SOME (Token.Fact (NONE, [t]))) tok))); |
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
63120
diff
changeset
|
45 |
|
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
46 |
fun is_real_val (Real_Val _) = true |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
47 |
| is_real_val _ = false; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
48 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
49 |
fun the_real_val (Real_Val t) = t |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
50 |
| the_real_val _ = raise Fail "Expected close parsed value"; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
51 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
52 |
fun the_parse_val (Parse_Val (b, _)) = b |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
53 |
| the_parse_val _ = raise Fail "Expected open parsed value"; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
54 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
55 |
fun the_parse_fun (Parse_Val (_, f)) = f |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
56 |
| the_parse_fun _ = raise Fail "Expected open parsed value"; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
57 |
|
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
58 |
fun parse_val_cases g (Parse_Val (b, f)) = (g b, f) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
59 |
| parse_val_cases _ (Real_Val v) = (v, K ()); |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
60 |
|
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
61 |
end; |