1open HOLsexp_dtype
2%%
3%name HOLsexp
4
5%nonterm sexp of HOLsexp_dtype.t
6       | sexp_seq of HOLsexp_dtype.t list * HOLsexp_dtype.t option
7       | dotfree_sexp_seq of HOLsexp_dtype.t list
8       | start of HOLsexp_dtype.t
9
10%term EOF
11    | SYMBOL of string
12    | STRING of string
13    | NUMBER of int
14    | LPAREN
15    | RPAREN
16    | DOT
17    | QUOTE
18%pos int
19%eop EOF
20%noshift EOF
21%verbose
22%pure
23%arg (stringbuffer) : string list ref
24%start start
25
26
27%%
28start : sexp (sexp)
29
30sexp : NUMBER (Integer NUMBER)
31     | SYMBOL (Symbol SYMBOL)
32     | STRING (String STRING)
33     | LPAREN sexp_seq RPAREN
34          (let val (sexps, lastopt) = sexp_seq
35           in
36             List.foldr (fn (t,A) => Cons(t,A))
37                        (case lastopt of
38                             NONE => Symbol "nil"
39                           | SOME t => t)
40                        sexps
41           end)
42     | QUOTE sexp
43          (Cons (Symbol "quote", Cons(sexp, Symbol "nil")))
44
45sexp_seq : dotfree_sexp_seq DOT sexp ((dotfree_sexp_seq, SOME sexp))
46         | dotfree_sexp_seq ((dotfree_sexp_seq, NONE))
47
48dotfree_sexp_seq :  ([]) | sexp dotfree_sexp_seq (sexp::dotfree_sexp_seq)
49