src/Tools/Metis/src/Parse.sml
author desharna
Thu, 09 Jul 2020 11:39:16 +0200
changeset 72004 913162a47d9f
parent 45778 df6e210fb44c
permissions -rw-r--r--
Update Metis to 2.4
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     1
(* ========================================================================= *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     2
(* PARSING                                                                   *)
72004
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
     3
(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License     *)
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     4
(* ========================================================================= *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     5
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     6
structure Parse :> Parse =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     7
struct
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     8
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     9
open Useful;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    10
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    11
infixr 9 >>++
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    12
infixr 8 ++
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    13
infixr 7 >>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    14
infixr 6 ||
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    15
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    16
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    17
(* A "cannot parse" exception.                                               *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    18
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    19
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    20
exception NoParse;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    21
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    22
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    23
(* Recursive descent parsing combinators.                                    *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    24
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    25
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    26
val error : 'a -> 'b * 'a = fn _ => raise NoParse;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    27
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    28
fun op ++ (parser1,parser2) input =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    29
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    30
      val (result1,input) = parser1 input
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    31
      val (result2,input) = parser2 input
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    32
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    33
      ((result1,result2),input)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    34
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    35
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    36
fun op >> (parser : 'a -> 'b * 'a, treatment) input =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    37
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    38
      val (result,input) = parser input
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    39
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    40
      (treatment result, input)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    41
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    42
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    43
fun op >>++ (parser,treatment) input =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    44
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    45
      val (result,input) = parser input
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    46
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    47
      treatment result input
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    48
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    49
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    50
fun op || (parser1,parser2) input =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    51
    parser1 input handle NoParse => parser2 input;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    52
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    53
fun first [] _ = raise NoParse
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    54
  | first (parser :: parsers) input = (parser || first parsers) input;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    55
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    56
fun mmany parser state input =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    57
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    58
      val (state,input) = parser state input
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    59
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    60
      mmany parser state input
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    61
    end
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    62
    handle NoParse => (state,input);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    63
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    64
fun many parser =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    65
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    66
      fun sparser l = parser >> (fn x => x :: l)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    67
    in
45778
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 39502
diff changeset
    68
      mmany sparser [] >> List.rev
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    69
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    70
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    71
fun atLeastOne p = (p ++ many p) >> op::;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    72
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    73
fun nothing input = ((),input);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    74
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    75
fun optional p = (p >> SOME) || (nothing >> K NONE);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    76
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    77
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    78
(* Stream-based parsers.                                                     *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    79
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    80
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    81
type ('a,'b) parser = 'a Stream.stream -> 'b * 'a Stream.stream
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    82
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    83
fun maybe p Stream.Nil = raise NoParse
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    84
  | maybe p (Stream.Cons (h,t)) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    85
    case p h of SOME r => (r, t ()) | NONE => raise NoParse;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    86
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    87
fun finished Stream.Nil = ((), Stream.Nil)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    88
  | finished (Stream.Cons _) = raise NoParse;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    89
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    90
fun some p = maybe (fn x => if p x then SOME x else NONE);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    91
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    92
fun any input = some (K true) input;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    93
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    94
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    95
(* Parsing whole streams.                                                    *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    96
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    97
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    98
fun fromStream parser input =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    99
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   100
      val (res,_) = (parser ++ finished >> fst) input
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   101
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   102
      res
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   103
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   104
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   105
fun fromList parser l = fromStream parser (Stream.fromList l);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   106
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   107
fun everything parser =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   108
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   109
      fun parserOption input =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   110
          SOME (parser input)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   111
          handle e as NoParse => if Stream.null input then NONE else raise e
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   112
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   113
      fun parserList input =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   114
          case parserOption input of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   115
            NONE => Stream.Nil
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   116
          | SOME (result,input) =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   117
            Stream.append (Stream.fromList result) (fn () => parserList input)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   118
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   119
      parserList
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   120
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   121
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   122
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   123
(* Parsing lines of text.                                                    *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   124
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   125
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   126
fun initialize {lines} =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   127
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   128
      val lastLine = ref (~1,"","","")
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   129
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   130
      val chars =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   131
          let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   132
            fun saveLast line =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   133
                let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   134
                  val ref (n,_,l2,l3) = lastLine
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   135
                  val () = lastLine := (n + 1, l2, l3, line)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   136
                in
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
   137
                  String.explode line
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   138
                end
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   139
          in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   140
            Stream.memoize (Stream.map saveLast lines)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   141
          end
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   142
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   143
      fun parseErrorLocation () =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   144
          let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   145
            val ref (n,l1,l2,l3) = lastLine
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   146
          in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   147
            (if n <= 0 then "at start"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   148
             else "around line " ^ Int.toString n) ^
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   149
            chomp (":\n" ^ l1 ^ l2 ^ l3)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   150
          end
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   151
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   152
      {chars = chars,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   153
       parseErrorLocation = parseErrorLocation}
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   154
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   155
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   156
fun exactChar (c : char) = some (equal c) >> K ();
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   157
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   158
fun exactCharList cs =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   159
    case cs of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   160
      [] => nothing
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   161
    | c :: cs => (exactChar c ++ exactCharList cs) >> snd;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   162
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
   163
fun exactString s = exactCharList (String.explode s);
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   164
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   165
fun escapeString {escape} =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   166
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   167
      fun isEscape c = mem c escape
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   168
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   169
      fun isNormal c =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   170
          case c of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   171
            #"\\" => false
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   172
          | #"\n" => false
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   173
          | #"\t" => false
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   174
          | _ => not (isEscape c)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   175
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   176
      val escapeParser =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   177
          (exactChar #"\\" >> K #"\\") ||
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   178
          (exactChar #"n" >> K #"\n") ||
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   179
          (exactChar #"t" >> K #"\t") ||
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   180
          some isEscape
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   181
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   182
      val charParser =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   183
          ((exactChar #"\\" ++ escapeParser) >> snd) ||
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   184
          some isNormal
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   185
    in
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
   186
      many charParser >> String.implode
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   187
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   188
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   189
local
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   190
  val isSpace = Char.isSpace;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   191
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   192
  val space = some isSpace;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   193
in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   194
  val manySpace = many space >> K ();
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   195
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   196
  val atLeastOneSpace = atLeastOne space >> K ();
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   197
end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   198
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
   199
fun fromString parser s = fromList parser (String.explode s);
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   200
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   201
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   202
(* Infix operators.                                                          *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   203
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   204
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
   205
fun parseLayeredInfixes {tokens,assoc} mk tokParser subParser =
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   206
    let
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
   207
      fun layerTokParser inp =
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
   208
          let
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
   209
            val tok_rest as (tok,_) = tokParser inp
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
   210
          in
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
   211
            if StringSet.member tok tokens then tok_rest
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
   212
            else raise NoParse
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
   213
          end
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   214
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
   215
      fun layerMk (x,txs) =
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
   216
          case assoc of
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
   217
            Print.LeftAssoc =>
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
   218
            let
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
   219
              fun inc ((t,y),z) = mk (t,z,y)
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
   220
            in
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
   221
              List.foldl inc x txs
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
   222
            end
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
   223
          | Print.NonAssoc =>
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
   224
            (case txs of
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
   225
               [] => x
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
   226
             | [(t,y)] => mk (t,x,y)
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
   227
             | _ => raise NoParse)
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
   228
          | Print.RightAssoc =>
45778
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 39502
diff changeset
   229
            (case List.rev txs of
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
   230
               [] => x
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
   231
             | tx :: txs =>
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
   232
               let
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
   233
                 fun inc ((t,y),(u,z)) = (t, mk (u,y,z))
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   234
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
   235
                 val (t,y) = List.foldl inc tx txs
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
   236
               in
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
   237
                 mk (t,x,y)
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
   238
               end)
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
   239
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
   240
      val layerParser = subParser ++ many (layerTokParser ++ subParser)
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
   241
    in
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
   242
      layerParser >> layerMk
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
   243
    end;
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   244
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   245
fun parseInfixes ops =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   246
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   247
      val layeredOps = Print.layerInfixes ops
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   248
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   249
      val iparsers = List.map parseLayeredInfixes layeredOps
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   250
    in
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
   251
      fn mk => fn tokParser => fn subParser =>
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
   252
         List.foldr (fn (p,sp) => p mk tokParser sp) subParser iparsers
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   253
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   254
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   255
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   256
(* Quotations.                                                               *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   257
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   258
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   259
type 'a quotation = 'a frag list;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   260
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   261
fun parseQuotation printer parser quote =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   262
  let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   263
    fun expand (QUOTE q, s) = s ^ q
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   264
      | expand (ANTIQUOTE a, s) = s ^ printer a
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   265
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
   266
    val string = List.foldl expand "" quote
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   267
  in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   268
    parser string
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   269
  end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   270
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   271
end