diff options
author | Jason Zaugg <jzaugg@gmail.com> | 2013-12-11 19:56:22 +0100 |
---|---|---|
committer | Jason Zaugg <jzaugg@gmail.com> | 2013-12-11 19:56:22 +0100 |
commit | 3bfd83971ec48102fd1e711236f5a313c6a1ce3e (patch) | |
tree | a75d929d7fc7e2c0ac4b5e620a4019a4936abeeb /docs/examples/typeinf.scala | |
parent | e1c6dd965aa4249f715bbb2832df182cc5505853 (diff) | |
parent | 9cdbe28c00b39c51ae9afe3066c8b44a6e5f6f96 (diff) | |
download | scala-3bfd83971ec48102fd1e711236f5a313c6a1ce3e.tar.gz scala-3bfd83971ec48102fd1e711236f5a313c6a1ce3e.tar.bz2 scala-3bfd83971ec48102fd1e711236f5a313c6a1ce3e.zip |
Merge commit '9cdbe28' into merge/2.10.x-to-master
Conflicts:
build.examples.xml
build.xml
docs/examples/actors/pingpong.scala
docs/examples/fors.scala
docs/examples/iterators.scala
docs/examples/jolib/Ref.scala
docs/examples/jolib/parallelOr.scala
docs/examples/monads/callccInterpreter.scala
docs/examples/monads/directInterpreter.scala
docs/examples/monads/errorInterpreter.scala
docs/examples/monads/simpleInterpreter.scala
docs/examples/monads/stateInterpreter.scala
docs/examples/parsing/ArithmeticParser.scala
docs/examples/patterns.scala
docs/examples/pilib/elasticBuffer.scala
docs/examples/pilib/handover.scala
docs/examples/pilib/piNat.scala
docs/examples/typeinf.scala
src/build/pack.xml
Diffstat (limited to 'docs/examples/typeinf.scala')
-rw-r--r-- | docs/examples/typeinf.scala | 253 |
1 files changed, 0 insertions, 253 deletions
diff --git a/docs/examples/typeinf.scala b/docs/examples/typeinf.scala deleted file mode 100644 index ac6cc35f6b..0000000000 --- a/docs/examples/typeinf.scala +++ /dev/null @@ -1,253 +0,0 @@ -package examples - -object typeinf { - -trait Term {} - -case class Var(x: String) extends Term { - override def toString() = x -} -case class Lam(x: String, e: Term) extends Term { - override def toString() = "(\\" + x + "." + e + ")" -} -case class App(f: Term, e: Term) extends Term { - override def toString() = "(" + f + " " + e + ")" -} -case class Let(x: String, e: Term, f: Term) extends Term { - override def toString() = "let " + x + " = " + e + " in " + f -} - -sealed trait Type {} -case class Tyvar(a: String) extends Type { - override def toString() = a -} -case class Arrow(t1: Type, t2: Type) extends Type { - override def toString() = "(" + t1 + "->" + t2 + ")" -} -case class Tycon(k: String, ts: List[Type]) extends Type { - override def toString() = - k + (if (ts.isEmpty) "" else ts.mkString("[", ",", "]")) -} - -object typeInfer { - - private var n: Int = 0 - def newTyvar(): Type = { n += 1; Tyvar("a" + n) } - - trait Subst extends Function1[Type, Type] { - def lookup(x: Tyvar): Type - def apply(t: Type): Type = t match { - case tv @ Tyvar(a) => val u = lookup(tv); if (t == u) t else apply(u) - case Arrow(t1, t2) => Arrow(apply(t1), apply(t2)) - case Tycon(k, ts) => Tycon(k, ts map apply) - } - def extend(x: Tyvar, t: Type) = new Subst { - def lookup(y: Tyvar): Type = if (x == y) t else Subst.this.lookup(y) - } - } - - val emptySubst = new Subst { def lookup(t: Tyvar): Type = t } - - case class TypeScheme(tyvars: List[Tyvar], tpe: Type) { - def newInstance: Type = - (emptySubst /: tyvars) ((s, tv) => s.extend(tv, newTyvar())) (tpe) - } - - type Env = List[Tuple2[String, TypeScheme]] - - def lookup(env: Env, x: String): TypeScheme = env match { - case List() => null - case (y, t) :: env1 => if (x == y) t else lookup(env1, x) - } - - def gen(env: Env, t: Type): TypeScheme = - TypeScheme(tyvars(t) diff tyvars(env), t) - - def tyvars(t: Type): List[Tyvar] = t match { - case tv @ Tyvar(a) => List(tv) - case Arrow(t1, t2) => tyvars(t1) union tyvars(t2) - case Tycon(k, ts) => (List[Tyvar]() /: ts) ((tvs, t) => tvs union tyvars(t)) - } - - def tyvars(ts: TypeScheme): List[Tyvar] = - tyvars(ts.tpe) diff ts.tyvars; - - def tyvars(env: Env): List[Tyvar] = - (List[Tyvar]() /: env) ((tvs, nt) => tvs union tyvars(nt._2)) - - def mgu(t: Type, u: Type, s: Subst): Subst = (s(t), s(u)) match { - case (Tyvar(a), Tyvar(b)) if (a == b) => - s - case (Tyvar(a), _) if !(tyvars(u) contains a) => - s.extend(Tyvar(a), u) - case (_, Tyvar(a)) => - mgu(u, t, s) - case (Arrow(t1, t2), Arrow(u1, u2)) => - mgu(t1, u1, mgu(t2, u2, s)) - case (Tycon(k1, ts), Tycon(k2, us)) if (k1 == k2) => - (s /: (ts zip us)) ((s, tu) => mgu(tu._1, tu._2, s)) - case _ => - throw new TypeError("cannot unify " + s(t) + " with " + s(u)) - } - - case class TypeError(s: String) extends Exception(s) {} - - def tp(env: Env, e: Term, t: Type, s: Subst): Subst = { - current = e - e match { - case Var(x) => - val u = lookup(env, x) - if (u == null) throw new TypeError("undefined: " + x) - else mgu(u.newInstance, t, s) - - case Lam(x, e1) => - val a, b = newTyvar() - val s1 = mgu(t, Arrow(a, b), s) - val env1 = (x, TypeScheme(List(), a)) :: env - tp(env1, e1, b, s1) - - case App(e1, e2) => - val a = newTyvar() - val s1 = tp(env, e1, Arrow(a, t), s) - tp(env, e2, a, s1) - - case Let(x, e1, e2) => - val a = newTyvar() - val s1 = tp(env, e1, a, s) - tp((x, gen(env, s1(a))) :: env, e2, t, s1) - } - } - var current: Term = null - - def typeOf(env: Env, e: Term): Type = { - val a = newTyvar() - tp(env, e, a, emptySubst)(a) - } -} - - object predefined { - val booleanType = Tycon("Boolean", List()) - val intType = Tycon("Int", List()) - def listType(t: Type) = Tycon("List", List(t)) - - private def gen(t: Type): typeInfer.TypeScheme = typeInfer.gen(List(), t) - private val a = typeInfer.newTyvar() - val env = List( -/* - ("true", gen(booleanType)), - ("false", gen(booleanType)), - ("if", gen(Arrow(booleanType, Arrow(a, Arrow(a, a))))), - ("zero", gen(intType)), - ("succ", gen(Arrow(intType, intType))), - ("nil", gen(listType(a))), - ("cons", gen(Arrow(a, Arrow(listType(a), listType(a))))), - ("isEmpty", gen(Arrow(listType(a), booleanType))), - ("head", gen(Arrow(listType(a), a))), - ("tail", gen(Arrow(listType(a), listType(a)))), -*/ - ("fix", gen(Arrow(Arrow(a, a), a))) - ) - } - - trait MiniMLParsers extends CharParsers { - - /** whitespace */ - def whitespace = rep{chr(' ') ||| chr('\t') ||| chr('\n')} - - /** A given character, possible preceded by whitespace */ - def wschr(ch: char) = whitespace &&& chr(ch) - - def isLetter = (c: char) => Character.isLetter(c) - def isLetterOrDigit: char => boolean = Character.isLetterOrDigit - - /** identifiers or keywords */ - def id: Parser[String] = - for ( - c: char <- rep(chr(' ')) &&& chr(isLetter); - cs: List[char] <- rep(chr(isLetterOrDigit)) - ) yield (c :: cs).mkString("", "", "") - - /** Non-keyword identifiers */ - def ident: Parser[String] = - for (s <- id if s != "let" && s != "in") yield s - - /** term = '\' ident '.' term | term1 {term1} | let ident "=" term in term */ - def term: Parser[Term] = ( - ( for ( - _ <- wschr('\\'); - x <- ident; - _ <- wschr('.'); - t <- term) - yield Lam(x, t): Term ) - ||| - ( for ( - letid <- id if letid == "let"; - x <- ident; - _ <- wschr('='); - t <- term; - inid <- id; if inid == "in"; - c <- term) - yield Let(x, t, c) ) - ||| - ( for ( - t <- term1; - ts <- rep(term1)) - yield (t /: ts)((f, arg) => App(f, arg)) ) - ) - - /** term1 = ident | '(' term ')' */ - def term1: Parser[Term] = ( - ( for (s <- ident) - yield Var(s): Term ) - ||| - ( for ( - _ <- wschr('('); - t <- term; - _ <- wschr(')')) - yield t ) - ) - - /** all = term ';' */ - def all: Parser[Term] = - for ( - t <- term; - _ <- wschr(';')) - yield t - } - - class ParseString(s: String) extends Parsers { - type inputType = int - val input = 0 - def any = new Parser[char] { - def apply(in: int): Parser[char]#Result = - if (in < s.length()) Some((s charAt in, in + 1)) else None - } - } - - def showType(e: Term): String = - try { - typeInfer.typeOf(predefined.env, e).toString() - } - catch { - case typeInfer.TypeError(msg) => - "\n cannot type: " + typeInfer.current + - "\n reason: " + msg - } - - def main(args: Array[String]) { - Console.println( - if (args.length == 1) { - val ps = new ParseString(args(0)) with MiniMLParsers - ps.all(ps.input) match { - case Some((term, _)) => - "" + term + ": " + showType(term) - case None => - "syntax error" - } - } - else - "usage: java examples.typeinf <expr-string>" - ) - } - -} |