Skip to content

Instantly share code, notes, and snippets.

@kamiyaowl kamiyaowl/Program.cs
Last active Jun 28, 2016

Embed
What would you like to do?
C# + Sprache Lambda-Expr
using Sprache;
using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
namespace lambda_calc
{
abstract class Statement { }
abstract class Expr : Statement
{
public abstract Expr Conversion(Identifier before, Expr after);
public abstract Expr Reduction(Identifier before = null, Expr after = null);
public abstract Expr Optimize();
public abstract IEnumerable<char> Definitions();
public IEnumerable<char> AnonymousVar()
{
return Enumerable.Range('a', 26).Select(x => (char)x).Except(Definitions());
}
public abstract Expr Substitute(Assign assign);
}
class Identifier : Expr
{
public string Item { get; private set; }
public Identifier(string item)
{
Item = item;
}
public Identifier(char item)
{
Item = item.ToString();
}
public override string ToString()
{
return Item;
}
public override Expr Conversion(Identifier before, Expr after)
{
return new Identifier(Item.Replace(before.Item, after.ToString()));
}
public override Expr Reduction(Identifier before = null, Expr after = null)
{
return (before != null && after != null) ?
LambdaParser.expr.Parse(
(Item.Replace(before.Item, after.ToString()).Split(' ').Aggregate((s, x) => string.Format("({0}) {1}", s, x)))
) :
this;
}
public override Expr Optimize()
{
return this;
}
public IEnumerable<Identifier> Tokens
{
get
{
return Item.Select(x => new Identifier(x.ToString()));
}
}
public override IEnumerable<char> Definitions()
{
return Item.Distinct();
}
public override Expr Substitute(Assign assign)
{
return assign.Name == Item ? assign.Expr : this;
}
}
class Abstraction : Expr
{
public Identifier Left { get; private set; }
public Expr Right { get; private set; }
public Abstraction(Identifier l, Expr r)
{
Left = l;
Right = r;
}
public override string ToString()
{
return string.Format(@"λ{0}.{1}", Left, Right);
}
public override Expr Conversion(Identifier before, Expr after)
{
return new Abstraction(Left.Conversion(before, after) as Identifier, Right.Conversion(before, after));
}
public override Expr Reduction(Identifier before = null, Expr after = null)
{
return (before != null && after != null) ?
Conversion(before, after) :
this;
}
public override Expr Optimize()
{
return Left.Tokens.Reverse().Aggregate(Right, (s, x) => new Abstraction(x, s));
}
public override IEnumerable<char> Definitions()
{
return Left.Definitions().Concat(Right.Definitions()).Distinct();
}
public override Expr Substitute(Assign assign)
{
return new Abstraction(Left, Right.Substitute(assign));
}
}
class Application : Expr
{
public Expr Left { get; private set; }
public Expr Right { get; private set; }
public Application(Expr l, Expr r)
{
Left = l;
Right = r;
}
public override string ToString()
{
return string.Format(@"({0}) {1}", Left, Right);
}
public override Expr Conversion(Identifier before, Expr after)
{
return new Application(Left.Conversion(before, after), Right.Conversion(before, after));
}
public override Expr Reduction(Identifier before = null, Expr after = null)
{
var id = Left as Abstraction;
if (before == null && after == null && id != null && (Right is Abstraction || Right is Identifier))
{
var defined = id.Right.Definitions().Intersect(Right.Definitions()).Where(x => x != ' ');
if (defined.Any())
{
var nr = defined.Aggregate(Right, (s, x) => s.Conversion(new Identifier(x), new Identifier(s.AnonymousVar().Except(id.Right.Definitions()).First())));
var beta = id.Right.Reduction(id.Left, nr);
Console.WriteLine("\tαβ[{0} -> {1}] : {2}", id.Left, nr, beta);
return beta;
}
else
{
var beta = id.Right.Reduction(id.Left, Right);
Console.WriteLine("\tβ[{0} -> {1}] : {2}", id.Left, Right, beta);
return beta;
}
}
else
{
return new Application(Left.Reduction(before, after), Right.Reduction(before, after));
}
}
public override Expr Optimize()
{
return new Application(Left.Optimize(), Right.Optimize());
}
public override IEnumerable<char> Definitions()
{
return Left.Definitions().Concat(Right.Definitions()).Distinct();
}
public override Expr Substitute(Assign assign)
{
return new Application(Left.Substitute(assign), Right.Substitute(assign));
}
}
class Assign : Statement
{
public string Name { get; private set; }
public Expr Expr { get; private set; }
public Assign(string n, Expr e)
{
Name = n;
Expr = e;
}
public override string ToString()
{
return string.Format("<{0} = {1}>", Name, Expr);
}
}
class LambdaParser
{
public static readonly Parser<char> lambda = Parse.Char('\\')
.Or(Parse.Char('λ'));
public static readonly Parser<char> dot = Parse.Char('.');
public static readonly Parser<char> space = Parse.WhiteSpace;
public static readonly Parser<Expr> expr = Parse.Ref(() => application.Or<Expr>(abstraction).Or<Expr>(identifier));
public static readonly Parser<Identifier> identifier = Parse.LetterOrDigit.Or(space).AtLeastOnce().Text().Select(x => new Identifier(x));
public static readonly Parser<Abstraction> abstraction =
from l in lambda
from id in Parse.Letter.Or(space).AtLeastOnce().Text().Select(x => new Identifier(x))
from d in dot
from e in expr.Token().Many().Select(z => z.Aggregate((s, x) => new Application(s, x)))
select new Abstraction(id, e);
public static readonly Parser<Application> application =
from ob in Parse.Char('(')
from l in expr
from cb in Parse.Char(')')
from s in space
from r in expr
select new Application(l, r);
public static readonly Parser<Assign> assign =
from name in Parse.Upper.Or(Parse.Digit).AtLeastOnce().Text()
from eq in Parse.Char('=').Token()
from e in expr.End()
select new Assign(name, e);
public static readonly Parser<Statement> statement = assign.Or<Statement>(expr);
}
class Program
{
static void Main(string[] args)
{
var dic = new SortedDictionary<string, Assign>();
while (true)
{
//input
Console.Write(">");
var src = Console.ReadLine();
var parse = LambdaParser.statement.Parse(src);
Console.WriteLine(parse);
Expr result = (parse is Assign) ? (parse as Assign).Expr : parse as Expr;
//substitute
foreach (var p in dic)
{
result = result.Substitute(p.Value);
Console.WriteLine("\t{0} -> {1}", p.Value, result);
}
//reduction
string beta = "";
while (true)
{
Console.WriteLine("-> {0}", result);
result = result.Reduction();
if (result.ToString() == beta) break;
else beta = result.ToString();
}
//store
var assign = parse as Assign;
if (assign != null)
{
var na = new Assign(assign.Name, result);
dic.Add(na.Name, na);
}
}
}
}
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.