Skip to content

Instantly share code, notes, and snippets.

@WheretIB

WheretIB/typed_lambda_ch16.nc

Created June 11, 2021 09:49
Show Gist options
  • Save WheretIB/3cd9dc2330a2606af4d569fadd9fade3 to your computer and use it in GitHub Desktop.
Save WheretIB/3cd9dc2330a2606af4d569fadd9fade3 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
typed_lambda_ch16.nc
import std.string;
import std.io;
import std.hashmap;
import std.typeinfo;
import std.vector;
// Standard library extensions (stuff that should have been in stdlib but isn't there for some reason)
int int(string str){ return int(str.data); }
int hash_value(string str){ return hash_value(str.data); }
StdOut operator<<(StdOut out, string str){ Print(str.data); return out; }
auto vector:find(generic ref(T) f){ for(i in this) if(f(i)) return i; return nullptr; }
void hashmap:insert(Key k, Value v){ this[k] = v; }
auto hashmap:start()
{
return coroutine auto(){
for(int i = 0; i < entries.size; i++) for(auto node = entries[i]; node; node = node.next) yield node;
return nullptr;
};
}
// Types
class Type extendable{}
class TopType: Type{}
class UnitType: Type{}
class BoolType: Type{}
class NatType: Type{}
class StringType: Type{}
class FloatType: Type{}
class FunctionType: Type{ Type ref arg, res; }
class TupleType: Type{ vector<Type ref> elements; }
class TaggedType: Type{ string name; Type ref type; }
class RecordType: Type{ vector<TaggedType ref> elements; } // almost like it can be interchanged with Tuple
class SumType: Type{ Type ref left, right; }
class VariantType: Type{ vector<TaggedType ref> elements; }
class ListType: Type{ Type ref element; }
class RefType: Type{ Type ref target; }
class SourceType: Type{ Type ref target; }
class SinkType: Type{ Type ref target; }
// Type constructors
void FunctionType:FunctionType(Type ref arg, Type ref res){ this.arg = arg; this.res = res; }
void TupleType:TupleType(vector<Type ref> elements){ this.elements = elements; }
void TaggedType:TaggedType(string name, Type ref type){ this.name = name; this.type = type; }
void RecordType:RecordType(vector<TaggedType ref> elements){ this.elements = elements; }
void SumType:SumType(Type ref left, right){ this.left = left; this.right = right; }
void VariantType:VariantType(vector<TaggedType ref> elements){ this.elements = elements; }
void ListType:ListType(Type ref element){ this.element = element; }
void RefType:RefType(Type ref target){ this.target = target; }
void SourceType:SourceType(Type ref target){ this.target = target; }
void SinkType:SinkType(Type ref target){ this.target = target; }
bool isEqual(Type ref a, Type ref b)
{
if (!a || !b)
return !!a == !!b;
if (typeid(a) != typeid(b))
return false;
switch (typeid(a))
{
case TopType:
case UnitType:
case BoolType:
case NatType:
case StringType:
case FloatType:
return true;
case FunctionType:
FunctionType ref funcA = a;
FunctionType ref funcB = b;
return isEqual(funcA.arg, funcB.arg) && isEqual(funcA.res, funcB.res);
case TupleType:
TupleType ref tupA = a;
TupleType ref tupB = b;
if (tupA.elements.size() != tupB.elements.size()) return false;
for (i in tupA.elements, j in tupB.elements) if (!isEqual(i, j)) return false;
return true;
case TaggedType:
TaggedType ref tagA = a;
TaggedType ref tagB = b;
return tagA.name == tagB.name && isEqual(tagA.type, tagB.type);
case RecordType:
RecordType ref recA = a;
RecordType ref recB = b;
if (recA.elements.size() != recB.elements.size()) return false;
for (i in recA.elements, j in recB.elements) if (!isEqual(i, j)) return false;
return true;
case SumType:
SumType ref sumA = a;
SumType ref sumB = b;
return isEqual(sumA.left, sumB.left) && isEqual(sumA.right, sumB.right);
case VariantType:
VariantType ref varA = a;
VariantType ref varB = b;
if (varA.elements.size() != varB.elements.size()) return false;
for (i in varA.elements, j in varB.elements) if (!isEqual(i, j)) return false;
return true;
case ListType:
ListType ref listA = a;
ListType ref listB = b;
return isEqual(listA.element, listB.element);
case RefType:
RefType ref refA = a;
RefType ref refB = b;
return isEqual(refA.target, refB.target);
case SourceType:
SourceType ref sourceA = a;
SourceType ref sourceB = b;
return isEqual(sourceA.target, sourceB.target);
case SinkType:
SinkType ref sinkA = a;
SinkType ref sinkB = b;
return isEqual(sinkA.target, sinkB.target);
}
}
bool subsumes(Type ref super, Type ref sub)
{
if (isEqual(super, sub))
return true;
if (typeid(super) == TopType)
return true;
switch (typeid(sub))
{
case RecordType:
if (RecordType ref s = sub)
{
if (typeid(super) == RecordType)
{
RecordType ref t = super;
// for each element of 'super' we need an element of 'sub' that subsumes it
// this covers width, depth and permutation at the same time
for (i in t.elements)
{
if (!s.elements.find(<j> i.name == j.name && subsumes(i.type, j.type)))
return false;
}
return true;
}
}
break;
case FunctionType:
if (FunctionType ref s = sub)
{
if (typeid(super) == FunctionType)
{
FunctionType ref t = super;
return subsumes(s.arg, t.arg) && subsumes(t.res, s.res);
}
}
break;
case VariantType:
if (VariantType ref s = sub)
{
if (typeid(super) == VariantType)
{
VariantType ref t = super;
// for each element of 'sub' we need an element of 'super' that subsumes it
for (i in s.elements)
{
if (!t.elements.find(<j> i.name == j.name && subsumes(j.type, i.type))) // reverse order for inner type as well (compared to records)
return false;
}
return true;
}
}
break;
case ListType:
if (ListType ref s = sub)
{
if (typeid(super) == ListType)
{
ListType ref t = super;
return subsumes(t.element, s.element);
}
}
break;
case RefType:
if (RefType ref s = sub)
{
if (typeid(super) == RefType)
{
RefType ref t = super;
return subsumes(s.target, t.target) && subsumes(t.target, s.target);
}
if (typeid(super) == SourceType)
{
SourceType ref t = super;
return subsumes(t.target, s.target);
}
if (typeid(super) == SinkType)
{
SinkType ref t = super;
return subsumes(s.target, t.target);
}
}
break;
case SourceType:
if (SourceType ref s = sub)
{
if (typeid(super) == SourceType)
{
SourceType ref t = super;
return subsumes(t.target, s.target);
}
}
break;
case SinkType:
if (SinkType ref s = sub)
{
if (typeid(super) == SinkType)
{
SinkType ref t = super;
return subsumes(s.target, t.target);
}
}
break;
}
return false;
}
Type ref join(Type ref a, Type ref b)
{
if (isEqual(a, b))
return a;
// * | Top == Top
if (typeid(a) == TopType)
return a;
// Top | * == Top
if (typeid(b) == TopType)
return b;
// variants wihtout intersections compose into bigger variants
if (typeid(a) == VariantType && typeid(b) == VariantType)
{
VariantType ref l = a;
VariantType ref r = b;
// create a variant if there are no conflicting labels!
vector<TaggedType ref> elements;
// take elements from first variant
for(i in l.elements)
elements.push_back(i);
for(i in r.elements)
{
// if there is the same label with different type, fail
if (l.elements.find(<j> i.name == j.name && !isEqual(i.type, j.type)))
return nullptr;
// do not att duplicate element
if (!l.elements.find(<j> i.name == j.name))
elements.push_back(i);
}
return new VariantType(elements);
}
// records compose into a record with fields that are present in both
if (typeid(a) == RecordType && typeid(b) == RecordType)
{
RecordType ref l = a;
RecordType ref r = b;
// create a record with common labels
vector<TaggedType ref> elements;
for(i in l.elements)
{
if (TaggedType ref match = r.elements.find(<j> i.name == j.name))
{
if (auto elJoin = join(i.type, match.type))
elements.push_back(new TaggedType(i.name, elJoin));
else
return nullptr;
}
}
// a choice: do not return {} when no labels match
if (elements.size() == 0)
return nullptr;
return new RecordType(elements);
}
// a choice: do not return Top when no other join is found
return nullptr;
}
// Output
hashmap<string, Type ref> aliases; // global state, eww
string getName(Type ref a)
{
if (!a)
return string("-");
for (i in aliases)
{
if (isEqual(a, i.value))
return i.key;
}
switch (typeid(a))
{
case TopType: return string("Top");
case UnitType: return string("Unit");
case BoolType: return string("Bool");
case NatType: return string("Nat");
case StringType: return string("String");
case FloatType: return string("Float");
case FunctionType:
FunctionType ref func = a;
if (typeid(func.arg) == FunctionType)
return "(" + getName(func.arg) + ")->" + getName(func.res);
return getName(func.arg) + "->" + getName(func.res);
case TupleType:
TupleType ref tup = a;
string tupStr = getName(tup.elements[0]);
for (int i = 1; i < tup.elements.size(); i++)
tupStr = tupStr + " * " + getName(tup.elements[i]);
return tupStr;
case TaggedType:
TaggedType ref rpair = a;
return rpair.name + ":" + getName(rpair.type);
case RecordType:
RecordType ref rec = a;
string recStr = "{" + getName(rec.elements[0]);
for (int i = 1; i < rec.elements.size(); i++)
recStr = recStr + "," + getName(rec.elements[i]);
return recStr + "}";
case SumType:
SumType ref sum = a;
return getName(sum.left) + "+" + getName(sum.right);
case VariantType:
VariantType ref var = a;
string varStr = "<" + getName(var.elements[0]);
for (int i = 1; i < var.elements.size(); i++)
varStr = varStr + "," + getName(var.elements[i]);
return varStr + ">";
case ListType:
ListType ref list = a;
return "[" + getName(list.element) + "]";
case RefType:
RefType ref r = a;
return "Ref " + getName(r.target);
case SourceType:
SourceType ref source = a;
return "Source " + getName(source.target);
case SinkType:
SinkType ref sink = a;
return "Sink " + getName(sink.target);
}
}
StdOut operator<<(StdOut out, Type ref t){ out << getName(t); return out; }
// Terms
class Term extendable{ Type ref type; }
class Unit : Term{}
class Boolean : Term{ bool value; }
class Natural : Term{ int value; }
class String : Term{ string value; }
class Float : Term{ float value; }
class Variable: Term{ string x; }
class Abstraction: Term{ string x; Type ref xType; Term ref t; }
class Application: Term{ Term ref t1, t2; }
class Conditional: Term{ Term ref cond, tru, fls; }
class TypeAlias: Term{ string name; Type ref value; } // TODO: if we allow type name to be a stand-alone term, we can use regular assignment
class Assignment: Term{ string name; Term ref value; }
class Ascription: Term{ Term ref t; Type ref expected; }
class Let: Term{ string name; Term ref t, expr; }
class Match: Term{ vector<string> names; Term ref t, expr; }
class Tuple: Term{ vector<Term ref> elements; }
class TupleAccess: Term{ Term ref t; int index; }
class TaggedPair: Term{ string name; Term ref t; }
class Record: Term{ vector<TaggedPair ref> elements; }
class RecordAccess: Term{ Term ref t; string name; }
class Variant: Term{ string label; Term ref t; }
class CaseOption: Term{ string label; string name; Term ref t; } // cannot be typechecked by itself
class Case: Term{ Term ref t; vector<CaseOption ref> options; }
class List: Term{ Term ref head, tail; }
class Ref: Term{ Term ref ref l; }
class Deref: Term{ Term ref t; }
class Store: Term{ Term ref l, r; }
// Term constructors
void Boolean:Boolean(bool value){ this.value = value; }
void Natural:Natural(int value){ this.value = value; }
void String:String(string value){ this.value = value; }
void Float:Float(float value){ this.value = value; }
void Variable:Variable(string x){ this.x = x; }
void Variable:Variable(string x, Type ref type){ this.x = x; this.type = type; assert(type != nullptr); }
void Abstraction:Abstraction(string x, Type ref xType, Term ref t){ this.x = x; this.xType = xType; this.t = t; assert(xType != nullptr); }
void Application:Application(Term ref t1, t2){ this.t1 = t1; this.t2 = t2; }
void Conditional:Conditional(Term ref cond, tru, fls){ this.cond = cond; this.tru = tru; this.fls = fls; }
void Let:Let(string name, Term ref t, expr){ this.name = name; this.t = t; this.expr = expr; }
void Match:Match(vector<string> names, Term ref t, expr){ this.names = names; this.t = t; this.expr = expr; }
void TypeAlias:TypeAlias(string name, Type ref value){ this.name = name; this.value = value; assert(value != nullptr); }
void Assignment:Assignment(string name, Term ref value){ this.name = name; this.value = value; }
void Ascription:Ascription(Term ref t, Type ref expected){ this.t = t; this.expected = expected; assert(expected != nullptr); }
void Tuple:Tuple(vector<Term ref> elements){ this.elements = elements; }
void TupleAccess:TupleAccess(Term ref t, int index){ this.t = t; this.index = index; }
void TaggedPair:TaggedPair(string name, Term ref t){ this.name = name; this.t = t; }
void Record:Record(vector<TaggedPair ref> elements){ this.elements = elements; }
void RecordAccess:RecordAccess(Term ref t, string name){ this.t = t; this.name = name; }
void Variant:Variant(string label, Term ref t){ this.label = label; this.t = t; }
void CaseOption:CaseOption(string label, string name, Term ref t){ this.label = label; this.name = name; this.t = t; }
void Case:Case(Term ref t, vector<CaseOption ref> options){ this.t = t; this.options = options; }
void List:List(Term ref head, tail, Type ref type){ this.head = head; this.tail = tail; this.type = type; assert(type != nullptr); }
void Ref:Ref(Term ref ref l){ this.l = l; this.type = new RefType(l.type); }
void Deref:Deref(Term ref t){ this.t = t; }
void Store:Store(Term ref l, r){ this.l = l; this.r = r; }
// Optional equality (for testing)
bool isEqual(Term ref a, Term ref b)
{
if (typeid(a) != typeid(b))
return false;
if (!isEqual(a.type, b.type))
return false;
switch (typeid(a))
{
case Unit:
return true;
case Boolean:
Boolean ref boolA = a;
Boolean ref boolB = b;
return boolA.value == boolB.value;
case Natural:
Natural ref natA = a;
Natural ref natB = b;
return natA.value == natB.value;
case String:
String ref strA = a;
String ref strB = b;
return strA.value == strB.value;
case Float:
Float ref floatA = a;
Float ref floatB = b;
return floatA.value == floatB.value;
case Variable:
Variable ref varA = a;
Variable ref varB = b;
return varA.x == varB.x;
case Abstraction:
Abstraction ref absA = a;
Abstraction ref absB = b;
return absA.x == absB.x && isEqual(absA.t, absB.t);
case Application:
Application ref appA = a;
Application ref appB = b;
return isEqual(appA.t1, appB.t1) && isEqual(appA.t2, appB.t2);
case Conditional:
Conditional ref condA = a;
Conditional ref condB = b;
return isEqual(condA.cond, condB.cond) && isEqual(condA.tru, condB.tru) && isEqual(condA.fls, condB.fls);
case TypeAlias:
TypeAlias ref aliasA = a;
TypeAlias ref aliasB = b;
return aliasA.name == aliasB.name && isEqual(aliasA.value, aliasB.value);
case Assignment:
Assignment ref setA = a;
Assignment ref setB = b;
return setA.name == setB.name && isEqual(setA.value, setB.value);
case Ascription:
Ascription ref ascA = a;
Ascription ref ascB = b;
return isEqual(ascA.t, ascB.t) && isEqual(ascA.expected, ascB.expected);
case Let:
Let ref letA = a;
Let ref letB = b;
return letA.name == letB.name && isEqual(letA.t, letB.t) && isEqual(letA.expr, letB.expr);
case Match:
Match ref matchA = a;
Match ref matchB = b;
if (matchA.names.size() != matchB.names.size()) return false;
for (i in matchA.names, j in matchB.names) if (i != j) return false;
return isEqual(matchA.t, matchB.t) && isEqual(matchA.expr, matchB.expr);
case Tuple:
Tuple ref tupA = a;
Tuple ref tupB = b;
if (tupA.elements.size() != tupB.elements.size()) return false;
for (i in tupA.elements, j in tupB.elements) if (!isEqual(i, j)) return false;
return true;
case TupleAccess:
TupleAccess ref tupaccA = a;
TupleAccess ref tupaccB = b;
return isEqual(tupaccA.t, tupaccB.t) && tupaccA.index == tupaccB.index;
case TaggedPair:
TaggedPair ref tagA = a;
TaggedPair ref tagB = b;
return tagA.name == tagB.name && isEqual(tagA.t, tagB.t);
case Record:
Record ref recA = a;
Record ref recB = b;
if (recA.elements.size() != recB.elements.size()) return false;
for (i in recA.elements, j in recB.elements) if (!isEqual(i, j)) return false;
return true;
case RecordAccess:
RecordAccess ref recaccA = a;
RecordAccess ref recaccB = b;
return isEqual(recaccA.t, recaccB.t) && recaccA.name == recaccB.name;
case Variant:
Variant ref variantA = a;
Variant ref variantB = b;
return variantA.label == variantB.label && isEqual(variantA.t, variantB.t);
case CaseOption:
CaseOption ref caseoptA = a;
CaseOption ref caseoptB = b;
return caseoptA.label == caseoptB.label && caseoptA.name == caseoptB.name && isEqual(caseoptA.t, caseoptB.t);
case Case:
Case ref caseA = a;
Case ref caseB = b;
if (caseA.options.size() != caseB.options.size()) return false;
for (i in caseA.options, j in caseB.options) if (!isEqual(i, j)) return false;
return isEqual(caseA.t, caseB.t);
case List:
List ref listA = a;
List ref listB = b;
if (!!listA.head != !!listB.head) return false;
if (!!listA.tail != !!listB.tail) return false;
return isEqual(listA.head, listB.head) && isEqual(listA.tail, listB.tail);
case Ref:
Ref ref refA = a;
Ref ref refB = b;
return refA.l == refB.l;
case Deref:
Deref ref derefA = a;
Deref ref derefB = b;
return isEqual(derefA.t, derefB.t);
case Store:
Store ref storeA = a;
Store ref storeB = b;
return isEqual(storeA.l, storeB.l) && isEqual(storeA.r, storeB.r);
}
}
// Term output
void output(Term ref a);
StdOut operator<<(StdOut out, Term ref t){ output(t); return out; }
void output(Term ref a)
{
switch (typeid(a))
{
case Unit:
io.out << "unit";
break;
case Boolean:
if (Boolean ref t = a)
io.out << (t.value ? "true" : "false");
break;
case Natural:
if (Natural ref t = a)
io.out << t.value;
break;
case String:
if (String ref t = a)
io.out << "'" << t.value << "'";
break;
case Float:
if (Float ref t = a)
io.out << t.value;
break;
case Variable:
if (Variable ref t = a)
io.out << t.x;
break;
case Abstraction:
if (Abstraction ref t = a)
{
if (t.xType)
io.out << "/" << t.x << ":" << t.xType << ". " << t.t;
else
io.out << "/" << t.x << ". " << t.t;
}
break;
case Application:
if (Application ref t = a)
{
if (typeid(t.t2) == Application)
io.out << t.t1 << " (" << t.t2 << ")";
else
io.out << t.t1 << " " << t.t2;
}
break;
case Conditional:
if (Conditional ref t = a)
io.out << "if " << t.cond << " then " << t.tru << " else " << t.fls;
break;
case TypeAlias:
if (TypeAlias ref t = a)
io.out << "type " << t.name << " = " << t.value;
break;
case Assignment:
if (Assignment ref t = a)
io.out << "local " << t.name << " = " << t.value;
break;
case Ascription:
if (Ascription ref t = a)
io.out << t.t << " as " << t.expected;
break;
case Let:
if (Let ref t = a)
io.out << "let " << t.name << "=" << t.t << " in " << t.expr;
break;
case Match:
if (Match ref t = a)
{
io.out << "let {" << t.names[0];
for (int i = 1; i < t.names.size(); i++)
io.out << "," << t.names[i];
io.out << "}=" << t.t << " in " << t.expr;
}
break;
case Tuple:
if (Tuple ref t = a)
{
io.out << "{" << t.elements[0];
for (int i = 1; i < t.elements.size(); i++)
io.out << "," << t.elements[i];
io.out << "}";
}
break;
case TupleAccess:
if (TupleAccess ref t = a)
io.out << t.t << "." << t.index;
break;
case TaggedPair:
if (TaggedPair ref t = a)
io.out << t.name << "=" << t.t;
break;
case Record:
if (Record ref t = a)
{
io.out << "{" << t.elements[0];
for (int i = 1; i < t.elements.size(); i++)
io.out << "," << t.elements[i];
io.out << "}";
}
break;
case RecordAccess:
if (RecordAccess ref t = a)
io.out << t.t << "." << t.name;
break;
case Variant:
if (Variant ref t = a)
io.out << "<" << t.label << "=" << t.t << ">";
break;
case CaseOption:
if (CaseOption ref t = a)
io.out << "<" << t.label << "=" << t.name << "> -> " << t.t;
break;
case Case:
if (Case ref t = a)
{
io.out << "case " << t.t << " of" << io.endl;
io.out << t.options[0] << io.endl;
for (int i = 1; i < t.options.size(); i++)
io.out << "| " << t.options[i];
}
break;
case List:
if (List ref t = a)
{
if (!t.head)
io.out << "nil" << t.type;
else
io.out << "cons" << t.type << " " << t.head << " " << t.tail;
}
break;
case Ref:
if (Ref ref t = a)
io.out << "&" << hash_value(auto ref(t.l));
break;
case Deref:
if (Deref ref t = a)
io.out << "!" << t.t;
break;
case Store:
if (Store ref t = a)
io.out << t.l << " := " << t.r;
break;
}
}
void outputln(Term ref t){ io.out << t << io.endl; }
// Lexer
enum LexemeType
{
Lambda,
Number,
Rational,
Str,
QuotedStr,
Oparen,
Cparen,
Ofigure,
Cfigure,
Obracket,
Cbracket,
Less,
Greater,
Point,
Comma,
Colon,
Semicolon,
Pipe,
Arrow,
Add,
Mult,
Equal,
Not,
Assign,
If,
Then,
Else,
Let_,
Letrec,
In,
Case_,
Of,
Nil,
Unknown,
Eof
}
class Lexeme
{
void Lexeme(LexemeType type, string str){ this.type = type; this.str = str; }
void Lexeme(LexemeType type, char[] str){ this.type = type; this.str = str; }
LexemeType type = LexemeType.Eof;
string str;
}
class Lexer
{
void Lexer(string str){ this.str = str; }
void skipSpaces()
{
while (pos < str.length() && str[pos] <= ' ')
pos++;
}
auto peek()
{
skipSpaces();
int pos = this.pos;
if (pos == str.length())
return Lexeme();
auto start = pos;
if (str[pos] == '-' && str[pos + 1] == '>') return Lexeme(LexemeType.Arrow, "->");
if (str[pos] == ':' && str[pos + 1] == '=') return Lexeme(LexemeType.Assign, ":=");
if (str[pos] == '/') return Lexeme(LexemeType.Lambda, str.substr(start, 1));
if (str[pos] == '(') return Lexeme(LexemeType.Oparen, str.substr(start, 1));
if (str[pos] == ')') return Lexeme(LexemeType.Cparen, str.substr(start, 1));
if (str[pos] == '{') return Lexeme(LexemeType.Ofigure, str.substr(start, 1));
if (str[pos] == '}') return Lexeme(LexemeType.Cfigure, str.substr(start, 1));
if (str[pos] == '[') return Lexeme(LexemeType.Obracket, str.substr(start, 1));
if (str[pos] == ']') return Lexeme(LexemeType.Cbracket, str.substr(start, 1));
if (str[pos] == '<') return Lexeme(LexemeType.Less, str.substr(start, 1));
if (str[pos] == '>') return Lexeme(LexemeType.Greater, str.substr(start, 1));
if (str[pos] == '.') return Lexeme(LexemeType.Point, str.substr(start, 1));
if (str[pos] == ',') return Lexeme(LexemeType.Comma, str.substr(start, 1));
if (str[pos] == ':') return Lexeme(LexemeType.Colon, str.substr(start, 1));
if (str[pos] == ';') return Lexeme(LexemeType.Semicolon, str.substr(start, 1));
if (str[pos] == '|') return Lexeme(LexemeType.Pipe, str.substr(start, 1));
if (str[pos] == '+') return Lexeme(LexemeType.Add, str.substr(start, 1));
if (str[pos] == '*') return Lexeme(LexemeType.Mult, str.substr(start, 1));
if (str[pos] == '=') return Lexeme(LexemeType.Equal, str.substr(start, 1));
if (str[pos] == '!') return Lexeme(LexemeType.Not, str.substr(start, 1));
if (str[pos] == '\'')
{
pos++;
while (pos < str.length() && str[pos] != '\'')
pos++;
pos++;
return Lexeme(LexemeType.QuotedStr, str.substr(start, pos - start));
}
// Lex identifier or a number
auto isAlnum = <char x> ((x | 32) >= 'a' && (x | 32) <= 'z') || x < 0 || x == '_';
auto isDigit = <char x> x >= '0' && x <= '9';
if (isAlnum(str[pos]))
{
pos++;
while (pos < str.length() && (isAlnum(str[pos]) || isDigit(str[pos])))
pos++;
}
else if (isDigit(str[pos]))
{
pos++;
while (pos < str.length() && isDigit(str[pos]))
pos++;
if (str[pos] == '.')
{
pos++;
while (pos < str.length() && isDigit(str[pos]))
pos++;
return Lexeme(LexemeType.Rational, str.substr(start, pos - start));
}
return Lexeme(LexemeType.Number, str.substr(start, pos - start));
}
string result = str.substr(start, pos - start);
if (result == "if") return Lexeme(LexemeType.If, result);
if (result == "then") return Lexeme(LexemeType.Then, result);
if (result == "else") return Lexeme(LexemeType.Else, result);
if (result == "let") return Lexeme(LexemeType.Let_, result);
if (result == "letrec") return Lexeme(LexemeType.Letrec, result);
if (result == "in") return Lexeme(LexemeType.In, result);
if (result == "case") return Lexeme(LexemeType.Case_, result);
if (result == "of") return Lexeme(LexemeType.Of, result);
if (result == "nil") return Lexeme(LexemeType.Nil, result);
if (result.empty()) return Lexeme(LexemeType.Unknown, "");
return Lexeme(LexemeType.Str, str.substr(start, pos - start));
}
auto consume()
{
skipSpaces();
auto next = peek();
pos += next.str.length();
return next;
}
string str;
int pos;
}
class Parser
{
Term ref parseExpr();
Term ref parseSeq();
Type ref parseType();
Type ref parseSimpleType()
{
assert(lexer.peek().type == LexemeType.Str, "type name expected");
auto name = lexer.consume().str;
switch (name)
{
case "Top": return new TopType();
case "Unit": return new UnitType();
case "Bool": return new BoolType();
case "Nat": return new NatType();
case "String": return new StringType();
case "Float": return new FloatType();
}
if (auto t = aliases.find(name))
return *t;
assert(false, "unknown type name " + name.data);
}
TaggedType ref parseTaggedType()
{
assert(lexer.peek().type == LexemeType.Str, "name expected");
auto name = lexer.consume().str;
if (lexer.peek().type == LexemeType.Colon)
{
lexer.consume();
auto type = parseType();
return new TaggedType(name, type);
}
return new TaggedType(name, new UnitType());
}
Type ref parseAtomType()
{
if (lexer.peek().type == LexemeType.Ofigure)
{
lexer.consume();
vector<TaggedType ref> elements;
elements.push_back(parseTaggedType());
while (lexer.peek().type == LexemeType.Comma)
{
lexer.consume();
elements.push_back(parseTaggedType());
}
assert(lexer.peek().type == LexemeType.Cfigure, "'}' expected after type");
lexer.consume();
return new RecordType(elements);
}
if (lexer.peek().type == LexemeType.Obracket)
{
lexer.consume();
auto element = parseType();
assert(lexer.peek().type == LexemeType.Cbracket, "']' expected after type");
lexer.consume();
return new ListType(element);
}
if (lexer.peek().type == LexemeType.Less)
{
lexer.consume();
vector<TaggedType ref> elements;
elements.push_back(parseTaggedType());
while (lexer.peek().type == LexemeType.Comma)
{
lexer.consume();
elements.push_back(parseTaggedType());
}
assert(lexer.peek().type == LexemeType.Greater, "'>' expected after type");
lexer.consume();
return new VariantType(elements);
}
if (lexer.peek().str == "Ref")
{
lexer.consume();
auto element = parseType();
return new RefType(element);
}
if (lexer.peek().str == "Source")
{
lexer.consume();
auto element = parseType();
return new SourceType(element);
}
if (lexer.peek().str == "Sink")
{
lexer.consume();
auto element = parseType();
return new SinkType(element);
}
if (lexer.peek().type == LexemeType.Oparen)
{
lexer.consume();
auto element = parseType();
assert(lexer.peek().type == LexemeType.Cparen, "')' expected after type");
lexer.consume();
return element;
}
return parseSimpleType();
}
Type ref parseTupleType()
{
vector<Type ref> elements;
elements.push_back(parseAtomType());
while (lexer.peek().type == LexemeType.Mult)
{
lexer.consume();
elements.push_back(parseAtomType());
}
if (elements.size() == 1)
return elements[0];
return new TupleType(elements);
}
Type ref parseSumType()
{
vector<Type ref> elements;
elements.push_back(parseTupleType());
while (lexer.peek().type == LexemeType.Add)
{
lexer.consume();
elements.push_back(parseTupleType());
}
if (elements.size() == 1)
return elements[0];
return new TupleType(elements);
}
Type ref parseFunctionType()
{
Type ref t = parseSumType();
if (lexer.peek().type == LexemeType.Arrow)
{
lexer.consume();
t = new FunctionType(t, parseFunctionType());
}
return t;
}
Type ref parseType()
{
return parseFunctionType();
}
CaseOption ref parseCaseOption()
{
assert(lexer.peek().type == LexemeType.Less, "'<' expected");
lexer.consume();
assert(lexer.peek().type == LexemeType.Str, "label expected after '<'");
string label = lexer.consume().str;
assert(lexer.peek().type == LexemeType.Equal, "'=' expected after label");
lexer.consume();
assert(lexer.peek().type == LexemeType.Str, "name expected after '='");
string name = lexer.consume().str;
assert(lexer.peek().type == LexemeType.Greater, "'>' expected after name");
lexer.consume();
assert(lexer.peek().type == LexemeType.Arrow, "'->' expected after '>");
lexer.consume();
auto t = parseExpr();
assert(t != nullptr, "term expected after '->'");
return new CaseOption(label, name, t);
}
Term ref parseTerm()
{
switch (lexer.peek().type)
{
case LexemeType.Lambda:
lexer.consume();
assert(lexer.peek().type == LexemeType.Str, "abstraction name expected after '/'");
string x = lexer.consume().str;
assert(lexer.peek().type == LexemeType.Colon, "type expected after abstraction name");
lexer.consume();
Type ref type = parseType();
assert(lexer.peek().type == LexemeType.Point, "'.' not found after abstracton name");
lexer.consume();
return new Abstraction(x, type, parseExpr());
case LexemeType.Number:
return new Natural(int(lexer.consume().str.data));
case LexemeType.Rational:
return new Float(float(lexer.consume().str.data));
case LexemeType.Str:
auto str = lexer.consume().str;
if (str == "unit")
return new Unit();
if (str == "true")
return new Boolean(true);
if (str == "false")
return new Boolean(false);
return new Variable(str);
case LexemeType.QuotedStr:
auto qstr = lexer.consume().str;
return new String(qstr.substr(1, qstr.length() - 2));
case LexemeType.Oparen:
lexer.consume();
auto t = parseSeq();
assert(t != nullptr, "term expected after '('");
assert(lexer.peek().type == LexemeType.Cparen, "')' not found after '('");
lexer.consume();
return t;
case LexemeType.Ofigure:
lexer.consume();
auto first = parseExpr();
assert(first != nullptr, "term expected after '{'");
// Looks like a record instead of a tuple
if (typeid(first) == Variable && lexer.peek().type == LexemeType.Equal)
{
lexer.consume();
auto name = Variable ref(first).x;
auto value = parseExpr();
assert(value != nullptr, "term expected after '='");
vector<TaggedPair ref> elements;
elements.push_back(new TaggedPair(name, value));
while (lexer.peek().type == LexemeType.Comma)
{
lexer.consume();
assert(lexer.peek().type == LexemeType.Str, "name expected after ','");
name = lexer.consume().str;
assert(lexer.peek().type == LexemeType.Equal, "'=' expected after name");
lexer.consume();
value = parseExpr();
assert(value != nullptr, "term expected after '='");
elements.push_back(new TaggedPair(name, value));
}
assert(lexer.peek().type == LexemeType.Cfigure, "'}' not found after term");
lexer.consume();
return new Record(elements);
}
vector<Term ref> elements;
elements.push_back(first);
while (lexer.peek().type == LexemeType.Comma)
{
lexer.consume();
elements.push_back(parseExpr());
assert(*elements.back() != nullptr, "term expected after ','");
}
assert(lexer.peek().type == LexemeType.Cfigure, "'}' not found after term");
lexer.consume();
return new Tuple(elements);
case LexemeType.Less:
lexer.consume();
assert(lexer.peek().type == LexemeType.Str, "label expected after '<'");
auto label = lexer.consume().str;
Term ref value = new Unit();
if (lexer.peek().type == LexemeType.Equal)
{
assert(lexer.peek().type == LexemeType.Equal, "'=' expected after label");
lexer.consume();
value = parseExpr();
assert(value != nullptr, "term expected after '='");
}
assert(lexer.peek().type == LexemeType.Greater, "'>' not found after term");
lexer.consume();
return new Variant(label, value);
case LexemeType.If:
lexer.consume();
auto cond = parseExpr();
assert(cond != nullptr, "condition expected after 'if'");
assert(lexer.peek().type == LexemeType.Then, "'then' not found after term");
lexer.consume();
auto tru = parseExpr();
assert(tru != nullptr, "term expected after 'then'");
assert(lexer.peek().type == LexemeType.Else, "'else' not found after term");
lexer.consume();
auto fls = parseExpr();
assert(fls != nullptr, "term expected after 'else'");
return new Conditional(cond, tru, fls);
case LexemeType.Let_:
lexer.consume();
vector<string> names;
switch(lexer.peek().type)
{
case LexemeType.Str:
names.push_back(lexer.consume().str);
break;
case LexemeType.Ofigure:
lexer.consume();
assert(lexer.peek().type == LexemeType.Str, "name expected after '{'");
names.push_back(lexer.consume().str);
while (lexer.peek().type == LexemeType.Comma)
{
lexer.consume();
assert(lexer.peek().type == LexemeType.Str, "name expected after ','");
names.push_back(lexer.consume().str);
}
assert(lexer.peek().type == LexemeType.Cfigure, "'}' not found after name");
lexer.consume();
break;
default:
assert(false, "name or '{' expected after 'let'");
}
assert(lexer.peek().type == LexemeType.Equal, "'=' not found after name");
lexer.consume();
auto term = parseExpr();
assert(term != nullptr, "term expected after '='");
assert(lexer.peek().type == LexemeType.In, "'in' not found after term");
lexer.consume();
auto expr = parseExpr();
assert(expr != nullptr, "term expected after 'in'");
if (names.size() == 1)
return new Let(names[0], term, expr);
return new Match(names, term, expr);
case LexemeType.Case_:
lexer.consume();
auto caseExpr = parseExpr();
assert(caseExpr != nullptr, "term expected after 'case'");
assert(lexer.peek().type == LexemeType.Of, "'of' not found after term");
lexer.consume();
vector<CaseOption ref> options;
options.push_back(parseCaseOption());
while (lexer.peek().type == LexemeType.Pipe)
{
lexer.consume();
options.push_back(parseCaseOption());
}
return new Case(caseExpr, options);
case LexemeType.Letrec:
{
lexer.consume();
assert(lexer.peek().type == LexemeType.Str, "label expected after '<'");
auto x = lexer.consume().str;
assert(lexer.peek().type == LexemeType.Colon, "':' not found after label");
lexer.consume();
auto xType = parseType();
assert(xType != nullptr, "type expected after name");
assert(lexer.peek().type == LexemeType.Equal, "'=' not found after name");
lexer.consume();
auto t1 = parseExpr();
assert(t1 != nullptr, "expression expected after '='");
assert(lexer.peek().type == LexemeType.In, "'in' not found after expression");
lexer.consume();
auto t2 = parseExpr();
assert(t2 != nullptr, "expression expected after 'in'");
return new Let(x, new Application(new Variable(string("fix")), new Abstraction(x, xType, t1)), t2);
}
case LexemeType.Nil:
lexer.consume();
assert(lexer.peek().type == LexemeType.Obracket, "'[' not found after 'nil'");
lexer.consume();
auto nilType = parseType();
assert(nilType != nullptr, "type expected after '['");
assert(lexer.peek().type == LexemeType.Cbracket, "']' not found after type");
lexer.consume();
return new List(nullptr, nullptr, new ListType(nilType));
case LexemeType.Not:
{
lexer.consume();
auto t = parseExpr();
assert(t != nullptr, "expression expected after '!'");
return new Deref(t);
}
case LexemeType.Unknown:
assert(false, "unknown lexeme at " + lexer.pos.str());
}
return nullptr;
}
Term ref parseAccess()
{
auto t = parseTerm();
while (lexer.peek().str == ".")
{
lexer.consume();
switch(lexer.peek().type)
{
case LexemeType.Number:
int index = int(lexer.consume().str);
assert(index > 0, "index has to start at '1'");
t = new TupleAccess(t, index);
break;
case LexemeType.Str:
string name = lexer.consume().str;
t = new RecordAccess(t, name);
break;
}
}
return t;
}
Term ref parseAs()
{
auto t = parseAccess();
while (lexer.peek().str == "as")
{
lexer.consume();
auto type = parseType();
t = new Ascription(t, type);
}
return t;
}
Term ref parseStore()
{
auto l = parseAs();
if (lexer.peek().type == LexemeType.Assign)
{
lexer.consume();
auto r = parseAs();
return new Store(l, r);
}
return l;
}
Term ref parseTerms()
{
auto t = parseStore();
auto t2 = parseStore();
while (t2)
{
t = new Application(t, t2);
t2 = parseStore();
}
return t;
}
Term ref parseSeq()
{
auto t = parseTerms();
while (lexer.peek().type == LexemeType.Semicolon)
{
lexer.consume();
auto t2 = parseTerms();
assert(t2 != nullptr, "term expected after ';'");
t = new Application(new Abstraction(string("_"), new UnitType(), t2), t);
}
return t;
}
Term ref parseExpr()
{
return parseTerms();
}
Term ref parseStatement()
{
if (lexer.peek().str == "type")
{
lexer.consume();
assert(lexer.peek().type == LexemeType.Str, "name expected after 'type'");
string name = lexer.consume().str;
assert(lexer.peek().type == LexemeType.Equal, "'=' expected after name");
lexer.consume();
Type ref rhs = parseType();
assert(rhs != nullptr, "type name expected after '='");
aliases[name] = rhs;
return new TypeAlias(name, rhs);
}
if (lexer.peek().str == "local")
{
lexer.consume();
assert(lexer.peek().type == LexemeType.Str, "name expected after 'local'");
string name = lexer.consume().str;
assert(lexer.peek().type == LexemeType.Equal, "'=' expected after name");
lexer.consume();
auto value = parseExpr();
assert(value != nullptr, "term expected after '='");
return new Assignment(name, value);
}
return parseSeq();
}
Term ref parseStatements()
{
auto t = parseStatement();
while (lexer.peek().type == LexemeType.Semicolon)
{
lexer.consume();
auto t2 = parseStatement();
assert(t2 != nullptr, "statement expected after ','");
t = new Application(new Abstraction(string("_"), new UnitType(), t2), t);
}
return t;
}
Term ref parse(char[] code)
{
lexer = Lexer(string(code));
auto t = parseStatements();
assert(lexer.pos == lexer.str.length(), "unknown symbol " + {lexer.str[lexer.pos]});
return t;
}
Lexer lexer;
}
class Interpreter
{
Parser p;
hashmap<string, Type ref> bindings;
hashmap<string, Term ref> globals; // optional
}
Type ref Interpreter:typecheck(Term ref a)
{
switch (typeid(a))
{
case Unit:
if (Unit ref t = a)
t.type = new UnitType();
break;
case Boolean:
if (Boolean ref t = a)
t.type = new BoolType();
break;
case Natural:
if (Natural ref t = a)
t.type = new NatType();
break;
case String:
if (String ref t = a)
t.type = new StringType();
break;
case Float:
if (Float ref t = a)
t.type = new FloatType();
break;
case Variable:
if (Variable ref t = a)
{
if (auto type = bindings.find(t.x))
t.type = *type;
else if (auto global = globals.find(t.x))
t.type = global.type;
else
io.out << "ERROR: Unknown variable " << t.x << io.endl;
}
break;
case Abstraction:
if (Abstraction ref t = a)
{
auto lastType = bindings[t.x];
if (t.x != "_")
bindings[t.x] = t.xType;
if (auto tType = typecheck(t.t))
t.type = new FunctionType(t.xType, tType);
bindings[t.x] = lastType;
}
break;
case Application:
if (Application ref t = a)
{
auto t2Type = typecheck(t.t2);
if (t2Type && typeid(t.t1) == Variable)
{
Variable ref v = t.t1;
switch(v.x)
{
case "succ":
if (typeid(t2Type) == NatType)
t.type = new NatType();
else
io.out << v.x << " expects Nat as an argument, got " << t2Type << io.endl;
break;
case "pred":
if (typeid(t2Type) == NatType)
t.type = new NatType();
else
io.out << v.x << " expects expects Nat as an argument, got " << t2Type << io.endl;
break;
case "iszero":
if (typeid(t2Type) == NatType)
t.type = new BoolType();
else
io.out << v.x << " expects expects Nat as an argument, got " << t2Type << io.endl;
break;
case "print":
if (typeid(t2Type) == UnitType || typeid(t2Type) == BoolType || typeid(t2Type) == NatType || typeid(t2Type) == StringType || typeid(t2Type) == FloatType)
t.type = new UnitType();
else
io.out << v.x << " expects expects base type as an argument, got " << t2Type << io.endl;
break;
case "fix":
if (typeid(t2Type) == FunctionType)
{
FunctionType ref funcType = t2Type;
if (isEqual(funcType.arg, funcType.res))
t.type = funcType.res;
else
io.out << v.x << " expects expects T->T function type as an argument, got " << t2Type << io.endl;
}
else
{
io.out << v.x << " expects expects function type as an argument, got " << t2Type << io.endl;
}
break;
case "eq":
if (typeid(t2Type) == NatType)
t.type = new FunctionType(new NatType(), new BoolType());
else
io.out << v.x << " expects expects Nat as an argument, got " << t2Type << io.endl;
break;
case "add":
if (typeid(t2Type) == NatType)
t.type = new FunctionType(new NatType(), new NatType());
else
io.out << v.x << " expects expects Nat as an argument, got " << t2Type << io.endl;
break;
case "mul":
if (typeid(t2Type) == NatType)
t.type = new FunctionType(new NatType(), new NatType());
else
io.out << v.x << " expects expects Nat as an argument, got " << t2Type << io.endl;
break;
case "addf":
if (typeid(t2Type) == FloatType)
t.type = new FunctionType(new FloatType(), new FloatType());
else
io.out << v.x << " expects expects Nat as an argument, got " << t2Type << io.endl;
break;
case "mulf":
if (typeid(t2Type) == FloatType)
t.type = new FunctionType(new FloatType(), new FloatType());
else
io.out << v.x << " expects expects Nat as an argument, got " << t2Type << io.endl;
break;
case "cons":
t.type = new FunctionType(new ListType(t2Type), new ListType(t2Type));
break;
case "isnil":
if (typeid(t2Type) == ListType)
t.type = new BoolType();
else
io.out << v.x << " expects expects List[T] as an argument, got " << t2Type << io.endl;
break;
case "head":
if (typeid(t2Type) == ListType)
t.type = ListType ref(t2Type).element;
else
io.out << v.x << " expects expects List[T] as an argument, got " << t2Type << io.endl;
break;
case "tail":
if (typeid(t2Type) == ListType)
t.type = t2Type;
else
io.out << v.x << " expects expects List[T] as an argument, got " << t2Type << io.endl;
break;
case "ref":
t.type = new RefType(t2Type);
break;
}
if (t.type)
break;
}
auto t1Type = typecheck(t.t1);
if (t1Type && t2Type)
{
if (typeid(t1Type) == FunctionType)
{
FunctionType ref t1FuncType = t1Type;
if (subsumes(t1FuncType.arg, t2Type))
t.type = t1FuncType.res;
else
io.out << "ERROR: Application rhs type " << t2Type << " has to match function argument type " << t1FuncType.arg << io.endl;
}
else
{
io.out << "ERROR: Application lhs type has to be function got " << t1Type << io.endl;
}
}
}
break;
case Conditional:
if (Conditional ref t = a)
{
auto condType = typecheck(t.cond);
auto truType = typecheck(t.tru);
auto flsType = typecheck(t.fls);
if (condType && truType && flsType)
{
if (typeid(condType) == BoolType)
{
t.type = join(truType, flsType);
if (!t.type)
{
io.out << "ERROR: Condition branch types have to join " << truType << " !^ " << flsType << io.endl;
}
}
else
{
io.out << "ERROR: Condition type has to be Bool got " << condType << io.endl;
}
}
}
break;
case TypeAlias:
if (TypeAlias ref t = a)
{
t.type = new UnitType();
}
break;
case Assignment:
if (Assignment ref t = a)
{
auto tType = typecheck(t.value);
if (tType)
{
bindings[t.name] = tType;
t.type = new UnitType();
}
}
break;
case Ascription:
if (Ascription ref t = a)
{
auto tType = typecheck(t.t);
if (tType)
{
if (isEqual(t.expected, tType))
t.type = tType;
else
io.out << "ERROR: Ascription failed to match " << tType << " to " << t.expected << io.endl;
}
}
break;
case Let:
if (Let ref t = a)
{
auto tType = typecheck(t.t);
if (tType)
{
auto lastType = bindings[t.name];
if (t.name != "_")
bindings[t.name] = tType;
if (auto exprType = typecheck(t.expr))
t.type = exprType;
bindings[t.name] = lastType;
}
}
break;
case Match:
if (Match ref t = a)
{
auto tType = typecheck(t.t);
if (tType)
{
if (typeid(tType) == TupleType)
{
TupleType ref matchTupleType = tType;
if (t.names.size() == matchTupleType.elements.size())
{
hashmap<string, Type ref> saved;
for (name in t.names, type in matchTupleType.elements)
{
saved[name] = bindings[name];
if (name != "_")
bindings[name] = type;
}
if (auto exprType = typecheck(t.expr))
t.type = exprType;
for (el in saved)
bindings[el.key] = el.value;
}
else
{
io.out << "ERROR: Mismatch between let pattern " << t << " and tuple type " << tType << io.endl;
}
}
else
{
io.out << "ERROR: Cannot match let pattern to " << tType << io.endl;
}
}
}
break;
case Tuple:
if (Tuple ref t = a)
{
vector<Type ref> elements;
for (i in t.elements)
{
if (auto type = typecheck(i))
elements.push_back(type);
else
break 2;
}
t.type = new TupleType(elements);
}
break;
case TupleAccess:
if (TupleAccess ref t = a)
{
auto tType = typecheck(t.t);
if (tType)
{
if (typeid(tType) == TupleType)
{
TupleType ref tupType = tType;
if (t.index - 1 < tupType.elements.size())
t.type = tupType.elements[t.index - 1];
else
io.out << "ERROR: Index " << t.index << " is out of bounds of type " << tupType << io.endl;
}
else
{
io.out << "ERROR: Cannot index type that is not a Tuple " << tType << io.endl;
}
}
}
break;
case TaggedPair:
if (TaggedPair ref t = a)
{
if (auto tType = typecheck(t.t))
t.type = new TaggedType(t.name, tType);
}
break;
case Record:
if (Record ref t = a)
{
vector<TaggedType ref> elements;
for (i in t.elements)
{
if (auto type = typecheck(i))
{
if (typeid(type) == TaggedType)
{
TaggedType ref recPairType = type;
if (elements.count_if(<x> x.name == recPairType.name) != 0)
io.out << "ERROR: record already has field named " << recPairType.name << io.endl;
else
elements.push_back(type);
}
else
{
io.out << "ERROR: Record element type is not a TaggedPair: " << type << io.endl;
}
}
else
{
break 2;
}
}
t.type = new RecordType(elements);
}
break;
case RecordAccess:
if (RecordAccess ref t = a)
{
auto tType = typecheck(t.t);
if (tType)
{
if (typeid(tType) == RecordType)
{
RecordType ref recType = tType;
if (recType.elements.count_if(<x> x.name == t.name) == 0)
{
io.out << "ERROR: record has no field named " << t.name << " in " << recType;
}
else
{
for (i in recType.elements)
{
if (i.name == t.name)
t.type = i.type;
}
}
}
else
{
io.out << "ERROR: Cannot index type that is not a Record: " << tType << io.endl;
}
}
}
break;
case Variant:
if (Variant ref t = a)
{
auto tType = typecheck(t.t);
if (tType)
{
vector<TaggedType ref> elements;
elements.push_back(new TaggedType(t.label, tType));
VariantType ref varType = new VariantType(elements);
t.type = new VariantType(elements);
}
}
break;
case Case:
if (Case ref t = a)
{
auto tType = typecheck(t.t);
if (!tType)
break;
if (typeid(tType) != VariantType)
{
io.out << "ERROR: " << t.t << " is not a VariantType" << io.endl;
break;
}
VariantType ref varType = tType;
if (varType.elements.size() != t.options.size())
{
io.out << "ERROR: case does cover all options" << io.endl;
break;
}
Type ref result;
for (option in t.options)
{
auto varOption = varType.elements.find(<x> x.name == option.label);
if (!varOption)
{
io.out << "ERROR: label " << option.label << " not found in " << varType << io.endl;
break 2;
}
if (t.options.count_if(<x> x.label == option.label) > 1)
{
io.out << "ERROR: duplicate case labels" << io.endl;
break 2;
}
auto lastType = bindings[option.name];
if (option.name != "_")
bindings[option.name] = varOption.type;
auto exprType = typecheck(option.t);
if (result)
{
result = join(result, exprType);
if(!result)
{
io.out << "ERROR: label " << option.label << " result " << exprType << " doesn't match " << result << io.endl;
break 2;
}
}
else
{
result = exprType;
}
bindings[option.name] = lastType;
}
t.type = result;
}
break;
case List:
if (List ref t = a)
assert(t.type != nullptr, "list must be typed internally");
break;
case Ref:
if (Ref ref t = a)
assert(t.type != nullptr, "ref must be typed internally");
break;
case Deref:
if (Deref ref t = a)
{
auto tType = typecheck(t.t);
if (!tType)
break;
if (typeid(tType) == RefType)
{
RefType ref refType = tType;
t.type = refType.target;
}
else if (typeid(tType) == SourceType)
{
SourceType ref sourceType = tType;
t.type = sourceType.target;
}
else
{
io.out << "ERROR: " << t.t << " is not a Ref or Source" << io.endl;
break;
}
}
break;
case Store:
if (Store ref t = a)
{
auto lType = typecheck(t.l);
auto rType = typecheck(t.r);
if (!lType || !rType)
break;
if (typeid(lType) == RefType)
{
RefType ref refType = lType;
if (!(subsumes(refType.target, rType) && subsumes(rType, refType.target)))
{
io.out << "ERROR: cannot store '" << rType << "'' into " << lType << io.endl;
break;
}
t.type = new UnitType();
}
else if(typeid(lType) == SinkType)
{
SinkType ref refType = lType;
if (!(subsumes(refType.target, rType) && subsumes(rType, refType.target)))
{
io.out << "ERROR: cannot store '" << rType << "'' into " << lType << io.endl;
break;
}
t.type = new UnitType();
}
else
{
io.out << "ERROR: store lhs '" << t.l << "'' is not a Ref" << io.endl;
break;
}
}
break;
}
if (!a.type)
io.out << "ERROR: Failed to typecheck " << typeid(a).name << " '" << a << "'" << io.endl;
return a.type;
}
void Interpreter:free(char[] name, char[] code)
{
p.lexer = Lexer(string(code));
auto t = p.parseType();
assert(t != nullptr, "failed to parse type");
auto var = new Variable(string(name));
var.type = t;
globals[string(name)] = var;
}
void Interpreter:global(char[] name, char[] code)
{
auto t = p.parse(code);
assert(t != nullptr, "failed to parse");
typecheck(t);
assert(t.type != nullptr, "failed to typecheck");
globals[string(name)] = t;
}
Term ref Interpreter:substitute(Term ref a, string x, Term ref rhs)
{
switch (typeid(a))
{
case Unit:
case Boolean:
case Natural:
case String:
case Float:
case Ref:
break;
case Variable:
if (Variable ref t = a)
{
if (t.x == x)
return rhs;
}
break;
case Abstraction:
if (Abstraction ref t = a)
{
// Do not step into the abstractions that have a binding over same name
if (t.x != "_" && t.x == x)
return a;
return new Abstraction(t.x, t.xType, substitute(t.t, x, rhs));
}
break;
case Application:
if (Application ref t = a)
{
// built-in 'binary' ops
if (x == "eq'")
return new Boolean(Natural ref(t.t1).value == Natural ref(rhs).value);
if (x == "add'")
return new Natural(Natural ref(t.t1).value + Natural ref(rhs).value);
if (x == "mul'")
return new Natural(Natural ref(t.t1).value * Natural ref(rhs).value);
if (x == "addf'")
return new Float(Float ref(t.t1).value + Float ref(rhs).value);
if (x == "mulf'")
return new Float(Float ref(t.t1).value * Float ref(rhs).value);
if (x == "cons'")
return new List(t.t1, rhs, new ListType(t.t1.type));
return new Application(substitute(t.t1, x, rhs), substitute(t.t2, x, rhs));
}
break;
case Conditional:
if (Conditional ref t = a)
return new Conditional(substitute(t.cond, x, rhs), substitute(t.tru, x, rhs), substitute(t.fls, x, rhs));
break;
case Ascription:
if (Ascription ref t = a)
return new Ascription(substitute(t.t, x, rhs), t.expected);
break;
case Let:
if (Let ref t = a)
{
auto value = substitute(t.t, x, rhs);
auto expr = t.name == x ? t.expr : substitute(t.expr, x, rhs);
return new Let(t.name, value, expr);
}
break;
case Match:
if (Match ref t = a)
{
auto value = substitute(t.t, x, rhs);
auto expr = t.names.count_if(<name> name == x) != 0 ? t.expr : substitute(t.expr, x, rhs);
return new Match(t.names, value, expr);
}
break;
case Tuple:
if (Tuple ref t = a)
{
vector<Term ref> elements;
for (i in t.elements)
elements.push_back(substitute(i, x, rhs));
return new Tuple(elements);
}
break;
case TupleAccess:
if (TupleAccess ref t = a)
return new TupleAccess(substitute(t.t, x, rhs), t.index);
break;
case Record:
if (Record ref t = a)
{
vector<TaggedPair ref> elements;
for (i in t.elements)
elements.push_back(new TaggedPair(i.name, substitute(i.t, x, rhs)));
return new Record(elements);
}
break;
case RecordAccess:
if (RecordAccess ref t = a)
return new RecordAccess(substitute(t.t, x, rhs), t.name);
break;
case Variant:
if (Variant ref t = a)
return new Variant(t.label, substitute(t.t, x, rhs));
break;
case CaseOption:
if (CaseOption ref t = a)
{
if (t.name != "_" && t.name == x)
return a;
return new CaseOption(t.label, t.name, substitute(t.t, x, rhs));
}
break;
case Case:
if (Case ref t = a)
{
auto value = substitute(t.t, x, rhs);
vector<CaseOption ref> options;
for (i in t.options)
options.push_back(substitute(i, x, rhs));
return new Case(value, options);
}
break;
case Deref:
if (Deref ref t = a)
{
auto value = substitute(t.t, x, rhs);
return new Deref(value);
}
break;
case Store:
if (Store ref t = a)
{
auto l = substitute(t.l, x, rhs);
auto r = substitute(t.r, x, rhs);
return new Store(l, r);
}
break;
default:
assert(false, "can't substitute in " + typeid(a).name);
}
return a;
}
Term ref Interpreter:eval(Term ref t);
Term ref Interpreter:evalBuiltin(Variable ref v, Term ref t)
{
t = eval(t);
switch(v.x)
{
case "succ":
if (Natural ref a = t)
return new Natural(a.value + 1);
break;
case "pred":
if (Natural ref a = t)
{
if (a.value != 0)
return new Natural(a.value - 1);
}
break;
case "iszero":
if (Natural ref a = t)
return new Boolean(a.value == 0);
break;
case "print":
switch (typeid(t))
{
case Unit: io.out << "STDOUT: " << io.endl; break;
case Boolean: io.out << "STDOUT: " << Boolean ref(t).value << io.endl; break;
case Natural: io.out << "STDOUT: " << Natural ref(t).value << io.endl; break;
case String: io.out << "STDOUT: " << String ref(t).value << io.endl; break;
case Float: io.out << "STDOUT: " << Float ref(t).value << io.endl; break;
}
return new Unit();
case "fix":
if (Abstraction ref tabs = eval(t))
{
auto s = new Application(new Variable(string("fix")), t);
return substitute(tabs.t, tabs.x, s);
}
assert(false, "fix must receive a function");
case "eq":
return new Abstraction(string("eq'"), new FunctionType(new NatType(), new BoolType()), new Application(t, new Variable(string("eq'"), new NatType())));
case "add":
return new Abstraction(string("add'"), new FunctionType(new NatType(), new NatType()), new Application(t, new Variable(string("add'"), new NatType())));
case "mul":
return new Abstraction(string("mul'"), new FunctionType(new NatType(), new NatType()), new Application(t, new Variable(string("mul'"), new NatType())));
case "addf":
return new Abstraction(string("addf'"), new FunctionType(new FloatType(), new FloatType()), new Application(t, new Variable(string("addf'"), new FloatType())));
case "mulf":
return new Abstraction(string("mulf'"), new FunctionType(new FloatType(), new FloatType()), new Application(t, new Variable(string("mulf'"), new FloatType())));
case "cons":
return new Abstraction(string("cons'"), new FunctionType(new ListType(t.type), new ListType(t.type)), new Application(t, new Variable(string("cons'"), new ListType(t.type))));
case "isnil":
if (List ref a = t)
return new Boolean(a.head == nullptr);
break;
case "head":
if (List ref a = t)
{
if (a.tail)
return a.head;
}
break;
case "tail":
if (List ref a = t)
{
if (a.tail)
return a.tail;
}
break;
case "ref":
Term ref ref l = new Term ref;
*l = t;
return new Ref(l);
}
return nullptr;
}
Term ref Interpreter:eval(Term ref t)
{
switch (typeid(t))
{
case Unit:
case Boolean:
case Natural:
case String:
case Float:
case Abstraction:
case List:
case Ref:
return t;
case Application:
if (Application ref application = t)
{
auto t1 = eval(application.t1);
if (typeid(t1) == Variable)
{
if (auto r = evalBuiltin(t1, application.t2))
return r;
}
if (typeid(t1) != Abstraction)
io.out << "expected abstraction for t1, got: (" << typeid(t1).name << ") " << t1 << io.endl;
Abstraction ref lhs = t1;
auto value = eval(application.t2);
return lhs.x == "_" ? eval(lhs.t) : eval(substitute(lhs.t, lhs.x, value));
}
break;
case Variable:
if (Variable ref variable = t)
{
if (auto t = globals.find(variable.x))
return eval(*t);
}
break;
case Conditional:
if (Conditional ref conditional = t)
{
auto cond = eval(conditional.cond);
if (Boolean ref(cond).value)
return eval(conditional.tru);
else
return eval(conditional.fls);
}
break;
case TypeAlias:
return new Unit();
case Assignment:
if (Assignment ref a = t)
{
globals[a.name] = eval(a.value);
return new Unit();
}
break;
case Ascription:
if (Ascription ref a = t)
{
return eval(a.t);
}
break;
case Let:
if (Let ref a = t)
{
auto value = eval(a.t);
return a.name == "_" ? eval(a.expr) : eval(substitute(a.expr, a.name, value));
}
break;
case Match:
if (Match ref a = t)
{
Tuple ref value = eval(a.t);
auto expr = a.expr;
for (i in a.names, j in value.elements)
expr = i == "_" ? expr : substitute(expr, i, j);
return eval(expr);
}
break;
case Tuple:
if (Tuple ref a = t)
{
vector<Term ref> elements;
for (i in a.elements)
elements.push_back(eval(i));
return new Tuple(elements);
}
break;
case TupleAccess:
if (TupleAccess ref a = t)
{
Tuple ref value = eval(a.t);
return eval(value.elements[a.index - 1]); // should be typechecked already
}
break;
case Record:
if (Record ref a = t)
{
vector<TaggedPair ref> elements;
for (i in a.elements)
elements.push_back(new TaggedPair(i.name, eval(i.t)));
return new Record(elements);
}
break;
case RecordAccess:
if (RecordAccess ref a = t)
{
Record ref value = eval(a.t);
for (i in value.elements)
{
if (i.name == a.name)
return i.t;
}
assert(false, "failed to access record element");
}
break;
case Variant:
if (Variant ref a = t)
{
return new Variant(a.label, eval(a.t));
}
break;
case Case:
if (Case ref a = t)
{
Variant ref value = eval(a.t);
for (option in a.options)
{
if (value.label == option.label)
{
auto tmp = substitute(option.t, option.name, value.t);
io.out << tmp << io.endl;
return eval(tmp);
}
}
}
break;
case Deref:
if (Deref ref a = t)
{
Ref ref value = eval(a.t);
return *value.l;
}
break;
case Store:
if (Store ref a = t)
{
Ref ref target = eval(a.l);
Term ref value = eval(a.r);
*target.l = value;
return new Unit();
}
break;
default:
assert(false, "can't evaluate " + typeid(t).name);
}
return t;
}
auto Interpreter:eval(char[] code)
{
auto t = p.parse(code);
assert(t != nullptr, "failed to parse");
typecheck(t);
assert(t.type != nullptr, "failed to typecheck");
return eval(t);
}
void Interpreter:printeval(char[] code)
{
io.out << code << io.endl;
auto t = eval(code);
typecheck(t);
io.out << "> " << t << " : " << getName(t.type) << io.endl;
}
void Interpreter:printtest(char[] code, char[] result)
{
io.out << code << io.endl;
auto t = eval(code);
typecheck(t);
io.out << "> " << t << " : " << getName(t.type) << io.endl;
auto r = eval(result);
typecheck(r);
if (!isEqual(t, r))
assert(false, "result mismatch");
}
void Interpreter:printtypecheck(char[] code)
{
auto t = p.parse(code);
assert(t != nullptr, "failed to parse");
typecheck(t);
assert(t.type != nullptr, "failed to typecheck");
io.out << "> " << t << " : " << getName(t.type) << io.endl;
}
Interpreter i;
i.global("not", "/x:Bool. if x then false else true");
i.printeval("if true then (/x:Bool. x) else (/x:Bool. not x)");
i.free("f", "Bool -> Bool");
i.printtypecheck("f");
i.printtypecheck("f (if false then true else false)");
i.printtypecheck("/x:Bool. f (if x then false else x)");
// 11.1 Base types, Type Aliases
i.printeval("true");
i.printeval("1");
i.printeval("'hello'");
i.printeval("1.3");
i.printeval(@"
type UU = Unit->Unit;
(/f:UU. f unit) (/x:Unit. x)
");
// 11.2 Unit type
i.printeval("unit");
// 11.3 Sequencing
i.printeval("unit;2");
// 11.4 Ascription
i.printeval("2 as Nat");
// 11.5 Let Bindings
// 11.5.1
i.printeval("let a = {2, 3} in a.2");
// 11.6, 11.7 Pairs, Tuples
i.free("tupTest", "Bool * Bool -> Bool * Nat");
i.printtypecheck("tupTest");
i.printeval("{2, 'hello', false}");
i.printtest("{2, 'hello', false}.2", "'hello'");
i.printtest("pred 3", "2");
i.printeval("{pred 4, pred 5}");
i.printtest("{pred 4, if true then false else false}.1", "3");
i.printtest("(/x:Nat*Nat. x.2) {pred 4, pred 5}", "4");
// some substitution tests
i.printeval("(/x:Nat. x as Nat) 2");
i.printeval("(/x:Nat. let a=x in a) 2");
i.printeval("(/x:Nat. let x={x, x} in x.1) 2");
i.printeval("(/x:Nat. {x, x}) 2");
i.printeval("(/x:Nat*Nat. x.2) {2, 3}");
i.printeval("print 'hello world'; 2");
i.printeval("{x=5}");
i.printeval("{x=pred 10}");
// 11.8 Records
i.printeval("{partno=5524,cost=30.27}");
i.printeval("{x=pred 4} as {x:Nat}");
i.printeval("{x=5} as {x:Nat}");
i.printeval("{partno=5524,cost=30.27} as {partno:Nat,cost:Float}");
// 11.8.2
i.printeval("let {a,b} = {2, 3} in (print b;a)");
i.printtest("(/_:Nat. 2) (print 'test';3)", "2");
i.printeval(@"
local a = 4;
a
");
i.free("tupTest", "Bool * Bool -> Bool * Nat");
i.printeval("type PhysicalAddr = {firstlast:String, addr:String}");
i.printeval("type VirtualAddr = {name:String, email:String}");
// 11.10 Variants
i.printeval(@"
type Addr = <physical:PhysicalAddr, virtual:VirtualAddr>;
local pa = {firstlast='ve', addr='none'};
local a = <physical=pa>;
a
");
i.printeval(@"
local getName = /a:Addr.
case a of
<physical=x> -> x.firstlast
| <virtual=y> -> y.name;
getName
");
i.printeval(@"
getName a
");
// Options (with Unit skip)
i.printeval("type OptionalNat = <none, some:Nat>");
i.printeval("type Table = Nat -> OptionalNat");
i.printeval("local emptyTable = /n:Nat. <none>");
i.printeval("emptyTable 1");
i.printeval("eq 4 5");
i.printeval("eq 4 4");
i.printeval("add 4 5");
i.printeval("mulf 4.2 5.2");
i.printeval(@"
local extendTable =
/t:Table./m:Nat./v:Nat.
/n:Nat.
if eq n m then <some=v>
else t n
");
i.printeval("extendTable emptyTable 1 10");
// Enumerations (with Unit skip)
i.printeval("type Weekday = <monday, tuesday, wednesday, thursday, friday>");
i.printeval(@"
local nextBusinessDay = /w:Weekday.
case w of
<monday=x> -> <tuesday>
| <tuesday=x> -> <wednesday>
| <wednesday=x> -> <friday>
| <thursday=x> -> <friday>
| <friday=x> -> <monday>
");
i.printeval("nextBusinessDay <tuesday>");
// Single-field variants
i.printeval("type DollarAmount = <dollars:Float>");
i.printeval("type EuroAmount = <euros:Float>");
i.printeval(@"
local dollars2euros = /d:DollarAmount.
case d of
<dollars=x> -> <euros = mulf x 1.1325>
");
i.printeval(@"
local euros2dollars = /d:EuroAmount.
case d of
<euros=x> -> <dollars = mulf x 0.883>
");
i.printeval("local mybankballance = <dollars=39.50>");
i.printeval("euros2dollars (dollars2euros mybankballance)");
// TODO: Dynamic?
// 11.11 General Recursion
i.printeval(@"
local ff = /ie:Nat->Bool.
/x:Nat.
if iszero x then true
else if iszero (pred x) then false
else ie (pred (pred x))
");
i.printeval("local iseven = fix ff");
i.printeval("iseven 7");
i.printeval("iseven 8");
// 11.11.1
i.printeval(@"
local equalrec = fix /self:Nat->Nat->Bool.
/x:Nat./y:Nat.
if iszero x then (if iszero y then true else false)
else if iszero y then (if iszero x then true else false)
else self (pred x) (pred y)
");
i.printeval("equalrec 8 7");
i.printeval("equalrec 14 14");
i.printeval(@"
local plusrec = fix /self:Nat->Nat->Nat.
/x:Nat./y:Nat.
if iszero x then y
else if iszero (pred x) then succ y
else self (pred x) (succ y)
");
i.printeval("plusrec 8 7");
i.printeval(@"
local timesrec = fix /self:Nat->Nat->Nat.
/x:Nat./y:Nat.
if iszero x then 0
else plusrec y (self (pred x) y)
");
i.printeval("timesrec 4 8");
i.printeval(@"
local factrec = fix /self:Nat->Nat.
/x:Nat.
if iszero x then 1
else if iszero (pred x) then 1
else timesrec x (self (pred x))
");
i.printeval("factrec 5");
i.printeval(@"
local ff = /ieio:{iseven:Nat->Bool, isodd:Nat->Bool}.
{
iseven = /x:Nat.
if iszero x then true
else ieio.isodd (pred x),
isodd = /x:Nat.
if iszero x then false
else ieio.iseven (pred x)
};
ff
");
i.printeval("local r = fix ff");
i.printtypecheck("r");
i.printeval("local iseven = r.iseven");
i.printeval("iseven 7");
i.printeval(@"
letrec iseven: Nat->Bool =
/x:Nat.
if iszero x then true
else if iszero (pred x) then false
else iseven (pred (pred x))
in
iseven 7
");
// 11.11.2
i.printeval(@"
letrec equalrec: Nat->Nat->Bool =
/x:Nat./y:Nat.
if iszero x then (if iszero y then true else false)
else if iszero y then (if iszero x then true else false)
else equalrec (pred x) (pred y)
in
equalrec 8 7
");
i.printeval(@"
letrec plusrec: Nat->Nat->Nat =
/x:Nat./y:Nat.
if iszero x then y
else if iszero (pred x) then succ y
else plusrec (pred x) (succ y)
in
plusrec 8 7
");
i.printeval("plusrec 8 7");
i.printeval(@"
letrec timesrec: Nat->Nat->Nat =
/x:Nat./y:Nat.
if iszero x then 0
else plusrec y (timesrec (pred x) y)
in
timesrec 4 8
");
i.printeval("timesrec 4 8");
i.printeval(@"
letrec factrec: Nat->Nat =
/x:Nat.
if iszero x then 1
else if iszero (pred x) then 1
else timesrec x (factrec (pred x))
in
factrec 5
");
// 11.13 Lists
i.free("listTest", "[Nat]");
i.printtypecheck("listTest");
i.printeval("nil[Nat]");
i.printeval("isnil nil[Nat]");
i.printeval("local l1 = cons 1 nil[Nat]");
i.printeval("l1");
i.printeval("head l1");
i.printeval("tail l1");
i.printeval("isnil l1");
i.printeval("local l2 = cons 1 (cons 2 nil[Nat])");
i.printeval("l2");
i.printeval("head l2");
i.printeval("head (tail l2)");
// 13.1 References
i.printeval("local r = ref 5; r");
i.printeval("!r");
i.printeval("r := 7");
i.printeval("!r");
i.printeval("r := (succ !r); !r");
i.printeval("(/_:Unit. !r) (r := (succ !r))");
i.printeval("r := (succ !r); r := (succ !r); r := (succ !r); r := (succ !r); !r");
i.printeval("local s = r; s");
i.printeval("s := 82");
i.printeval("!r");
i.printeval("local c = ref 0");
i.printeval("local incc = /x:Unit. (c := (succ !c); !c)");
i.printeval("local decc = /x:Unit. (c := (pred !c); !c)");
i.printeval("incc unit");
i.printeval("decc unit");
i.printeval("local o = { i = incc, d = decc }");
i.printeval("o.i unit");
i.printeval("type NatArray = Ref (Nat -> Nat)");
i.printeval("local newarray = /_:Unit. ref (/n:Nat. 0)");
i.printeval("newarray");
i.printeval("local lookup = /a:NatArray. /n:Nat. (!a) n");
i.printeval("lookup");
i.printeval(@"
local update = /a:NatArray./m:Nat./v:Nat.
let oldf = !a in
a := (/n:Nat. if eq m n then v else oldf n)
");
i.printeval("update");
i.printeval("local arr = newarray unit");
i.printeval("update arr 1 10");
i.printeval("update arr 2 20");
i.printeval("lookup arr 1");
i.printeval("lookup arr 2");
// 15.2
// records
i.printeval("(/x:{x:Nat}. succ x.x) {x=2}");
i.printeval("(/x:{x:Nat}. succ x.x) {x=2,y=3}");
i.printeval("(/x:{x:Nat,y:Nat}. succ x.x) {y=4,x=2}");
i.printeval("(/x:{x:{a:Nat}}. succ x.x.a) {x={a=4,b=8}}");
// functions
i.printeval("(/a:{x:Nat}->{x:Nat}. a {x=5}) (/b:{x:Nat}. {x=succ b.x})");
i.printeval("(/a:{x:Nat}->{x:Nat}. a {x=5}) (/b:{x:Nat}. {x=succ b.x,y=10})");
i.printeval("(/a:{x:Nat,y:Nat}->{x:Nat}. a {x=5,y=10}) (/b:{x:Nat}. {x=succ b.x})");
// top
i.printeval("(/x:Top. 2) {x=4}");
i.printeval("(/x:Top. 2) 5");
i.printeval("(/x:Top. 2) (/x:Nat. x)");
i.printeval("local id = /x:Top. x");
i.printeval("id 2");
// variants
i.printeval(@"
local getSomeOrZero = /a:<none, some:Nat>.
case a of
<none=x> -> 0
| <some=y> -> y;
getSomeOrZero <some=5>
");
i.printeval(@"
local depthtest = /a:<none,test:{x:Nat}>.
case a of
<none=x> -> 0
| <test=x> -> x.x;
depthtest <test={x=2,y=3}>
");
// lists
i.printeval("local l3 = cons {x=4,y=5} (cons {x=2,y=3} nil[{x:Nat,y:Nat}])");
i.printeval("(/l:[{x:Nat}]. head l) l3");
// ref
i.printeval("local r2 = ref {x=2,y=3}");
i.printeval("r2 := {y=4,x=5}");
i.printeval("!r2");
i.printeval("local r3 = ref {y=2,x=3}");
i.printeval("(/l:Ref {x:Nat,y:Nat}. (!l).x) r3");
// source
i.printeval("local r4 = ref {x=3,y=2}");
i.printeval("(/l:Source {x:Nat}. (!l).x) r4");
i.printeval("local r4f = /l:Source {x:Nat}. (!l).x");
i.printeval("(/l:Source {x:Nat,y:Nat}. (r4f l)) r4");
// sink
i.printeval("local r5 = ref {x=5}");
i.printeval("(/l:Sink {x:Nat,y:Nat}. l := {x=3,y=4}) r5");
i.printeval("!r5");
i.printeval("local r5f = /l:Sink {x:Nat,y:Nat}. l := {x=3,y=4}");
i.printeval("(/l:Sink {x:Nat}. (r5f l)) r5");
i.printeval("!r5");
// 16.3
i.printtypecheck("if true then {x=true,y=false} else {x=false,z=true}");
i.printtypecheck("if true then {x={a=1,b=3},y=false} else {x={a=3},z=true}");
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment