src/HOL/Eisbach/parse_tools.ML
author haftmann
Thu, 08 Nov 2018 09:11:52 +0100
changeset 69260 0a9688695a1b
parent 63185 08369e33c185
child 74563 042041c0ebeb
permissions -rw-r--r--
removed relics of ASCII syntax for indexed big operators
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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;