Disabled external gits
This commit is contained in:
@@ -0,0 +1,363 @@
|
||||
package fos
|
||||
|
||||
import scala.util.parsing.combinator.syntactical.StandardTokenParsers
|
||||
import scala.util.parsing.input._
|
||||
|
||||
/** This object implements a parser and evaluator for the
|
||||
* simply typed lambda calculus found in Chapter 9 of
|
||||
* the TAPL book.
|
||||
*/
|
||||
object SimplyTypedExtended extends StandardTokenParsers {
|
||||
lexical.delimiters ++= List("(", ")", "\\", ".", ":", "=", "->", "{", "}", ",", "*", "+",
|
||||
"=>", "|")
|
||||
lexical.reserved ++= List("Bool", "Nat", "true", "false", "if", "then", "else", "succ",
|
||||
"pred", "iszero", "let", "in", "fst", "snd", "fix", "letrec",
|
||||
"case", "of", "inl", "inr", "as")
|
||||
|
||||
|
||||
/** t ::= "true"
|
||||
* | "false"
|
||||
* | number
|
||||
* | "succ" t
|
||||
* | "pred" t
|
||||
* | "iszero" t
|
||||
* | "if" t "then" t "else" t
|
||||
* | ident
|
||||
* | "\" ident ":" T "." t
|
||||
* | t t
|
||||
* | "(" t ")"
|
||||
* | "let" ident ":" T "=" t "in" t
|
||||
* | "{" t "," t "}"
|
||||
* | "fst" t
|
||||
* | "snd" t
|
||||
* | "inl" t "as" T
|
||||
* | "inr" t "as" T
|
||||
* | "case" t "of" "inl" ident "=>" t "|" "inr" ident "=>" t
|
||||
* | "fix" t
|
||||
* | "letrec" ident ":" T "=" t "in" t
|
||||
*/
|
||||
|
||||
def term: Parser[Term] =
|
||||
rep1(v) ^^ {
|
||||
case x::Nil => x
|
||||
case l => l.reduceLeft(App.apply)
|
||||
}
|
||||
|
||||
|
||||
def v: Parser[Term] =
|
||||
"true" ^^^ True |
|
||||
"false" ^^^ False |
|
||||
numericLit ^^ { case n => numericRec(n.toInt,Zero)._2 } |
|
||||
("succ" ~> term) ^^ { Succ.apply } |
|
||||
("pred" ~> term) ^^ { Pred.apply } |
|
||||
("iszero" ~> term) ^^ { IsZero.apply } |
|
||||
("if" ~> term) ~ ("then" ~> term) ~ ("else" ~> term) ^^ { case cond ~ t1 ~ t2 => If(cond, t1, t2) } |
|
||||
ident ^^ { Var.apply } |
|
||||
("\\" ~> ident) ~ (":" ~> typeTerm) ~ ("." ~> term) ^^ { case id ~ tpe ~ t => Abs(id, tpe, t) } |
|
||||
("(" ~> term <~ ")") |
|
||||
("let" ~> ident) ~ (":" ~> typeTerm) ~ ("=" ~> term) ~ ("in" ~> term) ^^ { case id ~ tpe ~ t1 ~ t2 => App(Abs(id, tpe, t2), t1) } |
|
||||
("{" ~> term <~ ",") ~ (term <~ "}") ^^ { case f ~ s => TermPair(f, s) } |
|
||||
("fst" ~> term) ^^ { First.apply } |
|
||||
("snd" ~> term) ^^ { Second.apply } |
|
||||
("inl" ~> term) ~ ("as" ~> typeTerm) ^^ { case t~tpe => Inl(t,tpe) } |
|
||||
("inr" ~> term) ~ ("as" ~> typeTerm) ^^ { case t~tpe => Inr(t,tpe) } |
|
||||
("case" ~> term) ~ ("of" ~> "inl" ~> ident) ~ ("=>" ~> term) ~
|
||||
("|" ~> "inr" ~> ident) ~ ("=>" ~> term) ^^ { case t~x1~t1~x2~t2 => Case(t,x1,t1,x2,t2) } |
|
||||
("fix" ~> term) ^^ { Fix.apply } |
|
||||
("letrec" ~> ident) ~ (":" ~> typeTerm) ~ ("=" ~> term) ~ ("in" ~> term) ^^ { case id~tpe~t1~t2 => App(Abs(id,tpe,t2),Fix(Abs(id,tpe,t1)))} |
|
||||
failure("Unmatched Term")
|
||||
|
||||
|
||||
def baseTypeTerm: Parser[Type] =
|
||||
"Bool" ^^^ TypeBool |
|
||||
"Nat" ^^^ TypeNat |
|
||||
("(" ~> typeTerm <~ ")")
|
||||
|
||||
def pairTypeTerm: Parser[Type]=
|
||||
rep1sep(baseTypeTerm, "*") ^^ { case p => p.reduceRight(TypePair.apply) }
|
||||
|
||||
def sumTypeTerm: Parser[Type]=
|
||||
rep1sep(baseTypeTerm, "+") ^^ { case p => p.reduceRight(TypeSum.apply) }
|
||||
|
||||
def typeTerm: Parser[Type]=
|
||||
rep1sep(pairTypeTerm|sumTypeTerm, "->") ^^ { case p => p.reduceRight(TypeFun.apply) }
|
||||
|
||||
def numericRec(c:Int,s:Term): (Int,Term) = {
|
||||
if(c<=0) (0,s)
|
||||
else numericRec(c-1,Succ(s))
|
||||
}
|
||||
|
||||
def isNumeric(t: Term): Boolean = t match {
|
||||
case Zero => true
|
||||
case Pred(v) => isNumeric(v)
|
||||
case Succ(v) => isNumeric(v)
|
||||
case _ => false;
|
||||
}
|
||||
|
||||
def isReducible(t: Term): Boolean = try {
|
||||
reduce(t)
|
||||
true
|
||||
} catch { _ =>
|
||||
false
|
||||
}
|
||||
|
||||
var count: Int = 0
|
||||
def alpha(t: Abs): Abs = t match {
|
||||
case Abs(x,tp, t) =>
|
||||
val uid = x.toString()+"_"+count
|
||||
count += 1
|
||||
Abs(uid, tp, recurseUID(x, t, uid))
|
||||
}
|
||||
|
||||
def recurseUID(x: String, t: Term, uid: String): Term = t match {
|
||||
case True | False | Zero => t
|
||||
case Var(v) => if (v == x) Var(uid) else t
|
||||
case Abs(v, tp, t) => if(v==x) Abs(uid, tp, recurseUID(x, t, uid))
|
||||
else Abs(v, tp, recurseUID(x, t, uid))
|
||||
case App(t1, t2) => App(recurseUID(x, t1, uid), recurseUID(x, t2, uid))
|
||||
case Succ(t) => Succ(recurseUID(x, t, uid))
|
||||
case Pred(t) => Pred(recurseUID(x, t, uid))
|
||||
case IsZero(t) => IsZero(recurseUID(x, t,uid))
|
||||
case If(cond, t1, t2) => If(recurseUID(x, cond, uid), recurseUID(x, t1, uid), recurseUID(x, t2, uid))
|
||||
case TermPair(t1, t2) => TermPair(recurseUID(x, t1, uid), recurseUID(x, t2,uid))
|
||||
case First(t) => First(recurseUID(x, t, uid))
|
||||
case Second(t) => Second(recurseUID(x, t, uid))
|
||||
case Inl(t,tp) => Inl(recurseUID(x, t, uid),tp)
|
||||
case Inr(t,tp) => Inr(recurseUID(x, t, uid),tp)
|
||||
case Case(t,x1,t1,x2,t2) =>
|
||||
val nt1 = if (x1==x) t1 else recurseUID(x, t1, uid)
|
||||
val nt2 = if (x2==x) t2 else recurseUID(x, t2, uid)
|
||||
Case(recurseUID(x, t, uid),x1,nt1,x2,nt2)
|
||||
case Fix(t) => Fix(recurseUID(x, t, uid))
|
||||
}
|
||||
|
||||
def FV(t: Term): List[String] = t match {
|
||||
case True | False | Zero => List.empty
|
||||
case Var(v) => List(v)
|
||||
case Abs(v, tp, lt) => FV(lt).filterNot(_==v)
|
||||
case App(lt1, lt2) => FV(lt1):::FV(lt2)
|
||||
case Succ(t) => FV(t)
|
||||
case Pred(t) => FV(t)
|
||||
case IsZero(t) => FV(t)
|
||||
case If(cond,t1,t2) => FV(cond):::FV(t1):::FV(t2)
|
||||
case TermPair(t1,t2) => FV(t1):::FV(t2)
|
||||
case First(t) => FV(t)
|
||||
case Second(t) => FV(t)
|
||||
case Inl(t,_) => FV(t)
|
||||
case Inr(t,_) => FV(t)
|
||||
case Case(t,x1,t1,x2,t2) => FV(t)++: (FV(t1) diff List(x1)) ++: (FV(t2) diff List(x1))
|
||||
case Fix(t) => FV(t)
|
||||
}
|
||||
|
||||
def subst(t: Term, x: String, s: Term): Term = t match {
|
||||
case True | False | Zero => t
|
||||
case Var(v) if (v==x) => s
|
||||
case Var(_) => t
|
||||
|
||||
case If(t1, t2, t3) => If(subst(t1,x,s), subst(t2,x,s), subst(t3,x,s))
|
||||
case Pred(t) => Pred(subst(t,x,s))
|
||||
case Succ(t) => Succ(subst(t,x,s))
|
||||
case IsZero(t) => IsZero(subst(t,x,s))
|
||||
case t@Abs(v, tp, lt) => if (v==x) t
|
||||
else if (FV(s).contains(v)) subst(alpha(t),x,s)
|
||||
else Abs(v,tp,subst(lt,x,s))
|
||||
|
||||
case App(t1, t2) => App(subst(t1,x,s), subst(t2,x,s))
|
||||
case TermPair(t1, t2) => TermPair(subst(t1,x,s), subst(t2,x,s))
|
||||
case First(t) => First(subst(t,x,s))
|
||||
case Second(t) => Second(subst(t,x,s))
|
||||
|
||||
case Inl(t,tp) => Inl(subst(t,x,s),tp)
|
||||
case Inr(t,tp) => Inr(subst(t,x,s),tp)
|
||||
case Case(t,x1,t1,x2,t2) => {
|
||||
var nt1 = if(x1==x) t1 else subst(t1,x,s);
|
||||
var nt2 = if(x2==x) t2 else subst(t2,x,s);
|
||||
Case(subst(t,x,s),x1, nt1, x2, nt2);
|
||||
}
|
||||
case Fix(t) => Fix(subst(t,x,s))
|
||||
}
|
||||
|
||||
/** Call by value reducer. */
|
||||
def reduce(t: Term): Term = t match {
|
||||
|
||||
case If(True, t1, t2) => t1
|
||||
case If(False, t1, t2) => t2
|
||||
case If(cond, t1, t2) => If(reduce(cond), t1, t2)
|
||||
|
||||
case IsZero(Zero) => True
|
||||
case IsZero(Succ(v)) if isNumeric(v) => False
|
||||
case IsZero(t) => IsZero(reduce(t))
|
||||
|
||||
case Pred(Zero) => Zero
|
||||
case Pred(Succ(v)) if isNumeric(v) => v
|
||||
case Pred(v) => Pred(reduce(v))
|
||||
|
||||
case Succ(t) => Succ(reduce(t))
|
||||
|
||||
case App(t1,t2) if isReducible(t1) => App(reduce(t1),t2)
|
||||
case App(t1,t2) if isReducible(t2) => App(t1,reduce(t2))
|
||||
case App(Abs(x, tp, t1), t2) => subst(t1,x,t2)
|
||||
|
||||
case First(TermPair(t,_)) if !isReducible(t) => t
|
||||
case First(t) => First(reduce(t))
|
||||
|
||||
case Second(TermPair(_,t)) if !isReducible(t) => t
|
||||
case Second(t) => Second(reduce(t))
|
||||
|
||||
case TermPair(t1,t2) if isReducible(t1) => TermPair(reduce(t1), t2)
|
||||
case TermPair(t1,t2) if isReducible(t2) => TermPair(t1, reduce(t2))
|
||||
|
||||
case Inl(t,v) => Inl(reduce(t),v)
|
||||
case Inr(t,v) => Inr(reduce(t),v)
|
||||
|
||||
case Case(tt,x1,t1,x2,t2) if !isReducible(tt) => tt match {
|
||||
case Inl(v,_) => subst(t1,x1,v)
|
||||
case Inr(v,_) => subst(t2,x2,v)
|
||||
case _ => throw NoRuleApplies(t)
|
||||
}
|
||||
case Case(t,x1,t1,x2,t2) => Case(reduce(t),x1,t1,x2,t2)
|
||||
|
||||
case Fix(Abs(x,_,t1)) => subst(t1,x,t)
|
||||
case Fix(t) => Fix(reduce(t))
|
||||
|
||||
case _ => throw NoRuleApplies(t)
|
||||
}
|
||||
|
||||
/** Thrown when no reduction rule applies to the given term. */
|
||||
case class NoRuleApplies(t: Term) extends Exception(t.toString)
|
||||
|
||||
/** Print an error message, together with the position where it occured. */
|
||||
case class TypeError(t: Term, msg: String) extends Exception(msg) {
|
||||
override def toString = msg + "\n" + t
|
||||
}
|
||||
|
||||
/** The context is a list of variable names paired with their type. */
|
||||
type Context = List[(String, Type)]
|
||||
|
||||
/** Returns the type of the given term <code>t</code>.
|
||||
*
|
||||
* @param ctx the initial context
|
||||
* @param t the given term
|
||||
* @return the computed type
|
||||
*/
|
||||
def typeof(ctx: Context, term: Term): Type =
|
||||
term match {
|
||||
case True | False => TypeBool
|
||||
case Zero => TypeNat
|
||||
case Succ(t) => {
|
||||
val innerType = typeof(ctx, t)
|
||||
if(innerType == TypeNat) TypeNat
|
||||
else throw TypeError(term, f"Not typeable, Should be Nat, is $innerType")
|
||||
}
|
||||
case Pred(t) => {
|
||||
val innerType = typeof(ctx, t)
|
||||
if(innerType == TypeNat) TypeNat
|
||||
else throw TypeError(term, f"Not typeable, Should be Nat, is $innerType")
|
||||
}
|
||||
case IsZero(t) => {
|
||||
val innerType = typeof(ctx, t)
|
||||
if(innerType == TypeNat) TypeBool
|
||||
else throw TypeError(term, f"Not typeable, Should be Nat, is $innerType")
|
||||
}
|
||||
case If(cond, t1, t2) => {
|
||||
val condType = typeof(ctx, cond)
|
||||
val ifType = typeof(ctx, t1)
|
||||
val elseType = typeof(ctx, t2)
|
||||
if(condType == TypeBool && ifType == elseType) ifType
|
||||
else throw TypeError(term, f"Not typeable, If not consistent: $condType $ifType, $elseType")
|
||||
}
|
||||
case Var(name) => ctx.find { _._1 == name } match {
|
||||
case Some(_, t) => t
|
||||
case None => throw TypeError(term, f"Not typeable, $name not found")
|
||||
}
|
||||
case TermPair(t1, t2) => TypePair(typeof(ctx, t1), typeof(ctx, t2))
|
||||
|
||||
case First(t) => typeof(ctx,t) match {
|
||||
case TypePair(t1, t2) => t1
|
||||
case _ => throw TypeError(term, f"Not typeable. Should be Pair, found ${typeof(ctx, t)}")
|
||||
}
|
||||
|
||||
case Second(t) => typeof(ctx,t) match {
|
||||
case TypePair(t1, t2) => t2
|
||||
case _ => throw TypeError(term, f"Not typeable. Should be Pair, found ${typeof(ctx, t)}")
|
||||
}
|
||||
|
||||
case App(t1, t2) => {
|
||||
val t2type = typeof(ctx, t2)
|
||||
val t1type = typeof(ctx, t1)
|
||||
t1type match {
|
||||
case TypeFun(funt1, funt2) if funt1 == t2type => funt2
|
||||
case TypeFun(funt1, funt2) => throw TypeError(term, f"Not typeable. Should be $funt1, found $t2type")
|
||||
case _ => throw TypeError(term, f"Not typeable. Should be Fun, found $t1type")
|
||||
}
|
||||
}
|
||||
case Abs(x, t1, t) => TypeFun(t1, typeof(ctx.appended((x, t1)), t))
|
||||
|
||||
case Inl(t, tpe) => tpe match {
|
||||
case TypeSum(tp, _) if tp == typeof(ctx, t) => tpe
|
||||
case _ => throw TypeError(term, f"Not typeable. Should be Sum, found ${typeof(ctx, t)}")
|
||||
}
|
||||
|
||||
case Inr(t, tpe) => tpe match {
|
||||
case TypeSum(_, tp) if tp == typeof(ctx, t) => tpe
|
||||
case _ => throw TypeError(term, f"Not typeable. Should be Sum, found ${typeof(ctx, t)}")
|
||||
}
|
||||
|
||||
case Case(t, x1, t1, x2, t2) => typeof(ctx, t) match {
|
||||
case TypeSum(a1, a2) =>
|
||||
val ntp1 = typeof(ctx.appended((x1, a1)), t1)
|
||||
val ntp2 = typeof(ctx.appended((x2, a2)), t2)
|
||||
if (ntp1 == ntp2) ntp1
|
||||
else throw new TypeError(term, f"Not typeable. Should be Sum, found ${typeof(ctx, t)}")
|
||||
case _ => throw new TypeError(term, f"Not typeable. Should be Sum, found ${typeof(ctx, t)}")
|
||||
}
|
||||
|
||||
case Fix(t) => typeof(ctx, t) match {
|
||||
case TypeFun(tp1, tp2) if tp1==tp2 => tp2
|
||||
case _ => throw new TypeError(term, f"Not typeable. Should be Fun, found ${typeof(ctx, t)}")
|
||||
}
|
||||
|
||||
case null => throw TypeError(term, f"Unexpected Type: ${typeof(ctx,term)}")
|
||||
}
|
||||
|
||||
def typeof(t: Term): Type = try {
|
||||
typeof(Nil, t)
|
||||
} catch {
|
||||
case err @ TypeError(_, _) =>
|
||||
Console.println(err)
|
||||
null
|
||||
}
|
||||
|
||||
/** Returns a stream of terms, each being one step of reduction.
|
||||
*
|
||||
* @param t the initial term
|
||||
* @param reduce the evaluation strategy used for reduction.
|
||||
* @return the stream of terms representing the big reduction.
|
||||
*/
|
||||
def path(t: Term, reduce: Term => Term): LazyList[Term] =
|
||||
try {
|
||||
var t1 = reduce(t)
|
||||
LazyList.cons(t, path(t1, reduce))
|
||||
} catch {
|
||||
case NoRuleApplies(_) =>
|
||||
LazyList.cons(t, LazyList.empty)
|
||||
}
|
||||
|
||||
def main(args: Array[String]): Unit = {
|
||||
val stdin = new java.io.BufferedReader(new java.io.InputStreamReader(System.in))
|
||||
val tokens = new lexical.Scanner(stdin.readLine())
|
||||
phrase(term)(tokens) match {
|
||||
case Success(trees, _) =>
|
||||
try {
|
||||
println("parsed: " + trees)
|
||||
println("typed: " + typeof(Nil, trees))
|
||||
for (t <- path(trees, reduce))
|
||||
println(t)
|
||||
} catch {
|
||||
case tperror: Exception => println(tperror.toString)
|
||||
}
|
||||
case e =>
|
||||
println(e)
|
||||
}
|
||||
}
|
||||
}
|
||||
@@ -0,0 +1,84 @@
|
||||
package fos
|
||||
|
||||
import scala.util.parsing.input.Positional
|
||||
|
||||
/** Abstract Syntax Trees for terms. */
|
||||
sealed abstract class Term extends Positional
|
||||
|
||||
case object True extends Term {
|
||||
override def toString() = "true"
|
||||
}
|
||||
case object False extends Term {
|
||||
override def toString() = "false"
|
||||
}
|
||||
case object Zero extends Term {
|
||||
override def toString() = "0"
|
||||
}
|
||||
case class Succ(t: Term) extends Term {
|
||||
override def toString() = s"(succ $t)"
|
||||
}
|
||||
case class Pred(t: Term) extends Term {
|
||||
override def toString() = s"(pred $t)"
|
||||
}
|
||||
case class IsZero(t: Term) extends Term {
|
||||
override def toString() = s"(iszero $t)"
|
||||
}
|
||||
case class If(cond: Term, t1: Term, t2: Term) extends Term {
|
||||
override def toString() = s"if $cond then $t1 else $t2"
|
||||
}
|
||||
|
||||
case class Var(name: String) extends Term {
|
||||
override def toString() = name
|
||||
}
|
||||
case class Abs(v: String, tp: Type, t: Term) extends Term {
|
||||
override def toString() = s"(\\$v: $tp. $t)"
|
||||
}
|
||||
case class App(t1: Term, t2: Term) extends Term {
|
||||
override def toString() = s"($t1 $t2)"
|
||||
}
|
||||
case class TermPair(t1: Term, t2: Term) extends Term {
|
||||
override def toString() = s"{ $t1, $t2 }"
|
||||
}
|
||||
|
||||
case class First(t: Term) extends Term {
|
||||
override def toString() = s"(fst $t)"
|
||||
}
|
||||
|
||||
case class Second(t: Term) extends Term {
|
||||
override def toString() = s"(snd $t)"
|
||||
}
|
||||
|
||||
case class Inl(t: Term, tpe: Type) extends Term {
|
||||
override def toString() = s"(inl $t as $tpe)"
|
||||
}
|
||||
|
||||
case class Inr(t: Term, tpe: Type) extends Term {
|
||||
override def toString() = s"(inr $t as $tpe)"
|
||||
}
|
||||
|
||||
case class Case(t: Term, x1: String, t1: Term, x2: String, t2: Term) extends Term {
|
||||
override def toString() = s"(case $t of inl $x1 => $t1 | inr $x2 => $t2)"
|
||||
}
|
||||
|
||||
case class Fix(t: Term) extends Term {
|
||||
override def toString() = s"(fix $t)"
|
||||
}
|
||||
|
||||
/** Abstract Syntax Trees for types. */
|
||||
abstract class Type extends Positional
|
||||
|
||||
case object TypeBool extends Type {
|
||||
override def toString() = "Bool"
|
||||
}
|
||||
case object TypeNat extends Type {
|
||||
override def toString() = "Nat"
|
||||
}
|
||||
case class TypeFun(t1: Type, t2: Type) extends Type {
|
||||
override def toString() = s"($t1 -> $t2)"
|
||||
}
|
||||
case class TypePair(t1: Type, t2: Type) extends Type {
|
||||
override def toString() = s"($t1 * $t2)"
|
||||
}
|
||||
case class TypeSum(t1: Type, t2: Type) extends Type {
|
||||
override def toString() = s"($t1 + $t2)"
|
||||
}
|
||||
Reference in New Issue
Block a user