3 ms·

OK, thanks for pointing those out to me. Google leads me here: http://adam.chlipala.net/cpdt/html/Hoas.html http://adam.chlipala.net/cpdt/html/Hoas.html which

• trurl 15y ago
  The best example I have handy is some Scala code a student I worked with wrote in Scala. I'm not sure if this is necessarily compatible with the latest version of their parser combinator library, but is hopefully suggestive: import scala.util.parsing.combinator.syntactical.StandardTokenParsers import scala.util.parsing.input._ import scala.util.parsing.syntax._ object HoasTest extends StandardTokenParsers { lexical.delimiters ++= List("(", ")", "\\", ".", ":", "=", "->", "+", "{", "}", ",", "*") lexical.reserved ++= List("Bool", "Nat", "true", "false", "if", "then", "else", "succ", "pred", "iszero", "let", "in", "fst", "snd") import lexical.NumericLit import lexical.Identifier def Term(base: Parser[Term]): Parser[Term] = positioned( SimpleTerm(base) ~ SimpleTerm(base) ^^ { case fun~arg => Apply(fun,arg) } // should be left-assoc | SimpleTerm(base) ~ ("+" ~> SimpleTerm(base)) ^^ { case a~b => Plus(a,b) } // should be left-assoc | SimpleTerm(base) | failure("illegal start of term")) def SimpleTerm(base: Parser[Term]): Parser[Term] = positioned( (("\\" ~> ident <~ ".") into (x => Parser { in => def body(arg: Term): ParseResult[Term] = Term(Identifier(x) ^^^ arg | base)(in) body(new Term {}) match { case Success(_,rest) => Success(Lambda(x, (arg) => body(arg).get), rest) case f => f } })) | "(" ~> Term(base) <~ ")" | base | failure("illegal start of simple term")) def BaseTerm: Parser[Term] = positioned( numericLit ^^ { case n => Num(n.toInt) } | failure("unrecognized base term")) abstract class Term extends Positional case class Num(n: Int) extends Term case class Plus(a: Term, b: Term) extends Term case class Lambda(x: String, body: Term=>Term) extends Term { override def toString = "\\"+x+".("+body(new Term { override def toString = x }).toString+")" } case class Apply(fun: Term, arg: Term) extends Term }