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