// Simply typed lambda calculus (plus a little extra) in datalog,
// using the "crepe" crate.
// Might even be correct!
use crepe::crepe;
fn typecheck3() {
#[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash, Debug)]
enum PrimType {
I32,
F32,
Bool,
Unit,
}
#[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash, Debug)]
enum BinOp {
Add,
Eq,
}
type Tid = &'static str;
type Eid = &'static str;
type Ident = &'static str;
crepe! {
@input
#[derive(Debug)]
struct ELiteral(Eid, Tid);
@input
#[derive(Debug)]
struct EBinOp(Eid, BinOp, Eid, Eid);
// let x: type = init
@input
#[derive(Debug)]
struct ELet(Eid, Ident, Tid, Eid);
// let x = init (infer type)
@input
#[derive(Debug)]
struct ELetInfer(Eid, Ident, Eid);
@input
#[derive(Debug)]
struct EVarRef(Eid, Ident);
@input
#[derive(Debug)]
struct EMakeRef(Eid, Eid);
// lambda(arg, argtype, rettype, body)
// Currently we have only one arg and the body is one expr, so.
@input
#[derive(Debug)]
struct ELambda(Eid, Ident, Tid, Tid, Eid);
// apply(fn, arg)
@input
#[derive(Debug)]
struct EApply(Eid, Eid, Eid);
@output
#[derive(Debug)]
struct TypeOf(Eid, Tid);
@output
#[derive(Debug)]
struct TypeError(Eid);
struct Expr(Eid);
struct IsNumber(Tid);
struct DefPrim(Tid, PrimType);
struct DefRefType(Tid, Tid);
// Function type id, param type, ret type
struct DefFunType(Tid, Tid, Tid);
struct IsType(Tid);
struct IsUnit(Tid);
struct IsDeclaredVar(Ident);
DefPrim("I32", PrimType::I32);
DefPrim("F32", PrimType::F32);
DefPrim("Bool", PrimType::Bool);
DefPrim("Unit", PrimType::Unit);
// Instantiate the reference types that we use
DefRefType("&I32", "I32");
DefRefType("&&I32", "&I32");
// Instantiate the function types we use
DefFunType("fn(I32) I32", "I32", "I32");
DefFunType("fn(F32) I32", "F32", "I32");
DefFunType("fn(I32) F32", "I32", "F32");
IsNumber(tid) <-
DefPrim(tid, PrimType::I32);
IsNumber(tid) <-
DefPrim(tid, PrimType::F32);
IsUnit(tid) <-
DefPrim(tid, PrimType::Unit);
// Build our type "sum type"
IsType(tid) <-
DefPrim(tid, _);
IsType(tid) <-
DefRefType(tid, pointed_at),
IsType(pointed_at);
IsType(tid) <-
DefFunType(tid, argtype, rettype),
IsType(argtype),
IsType(rettype);
// Build our AST "sum type"
Expr(id) <-
ELiteral(id, _);
Expr(id) <-
EBinOp(id, _, lhs, rhs),
Expr(lhs),
Expr(rhs);
Expr(id) <-
ELet(id, _, _t, init_expr),
Expr(init_expr);
// A var usage is valid iff its name is declared in a let expr or
// function param.
// This requires all variables to have unique names, even function
// args, but that's okay.
IsDeclaredVar(name) <-
ELet(_, name, _, _);
IsDeclaredVar(name) <-
ELetInfer(_, name, _);
IsDeclaredVar(name) <-
ELambda(_eid, name, _argtype, _rettype, _body);
Expr(id) <-
EVarRef(id, name),
IsDeclaredVar(name);
Expr(id) <-
EMakeRef(id, pointed_at),
Expr(pointed_at);
Expr(id) <-
EMakeRef(id, pointed_at),
Expr(pointed_at);
Expr(id) <-
ELambda(id, _argname, argtype, rettype, body),
IsType(argtype),
IsType(rettype),
Expr(body);
// Actually say how to typecheck
// the various pieces of our AST
TypeOf(id, t) <-
EBinOp(id, BinOp::Add, lhs, rhs),
IsNumber(t),
TypeOf(lhs, t),
TypeOf(rhs, t);
TypeOf(id, tid) <-
DefPrim(tid, PrimType::Bool),
EBinOp(id, BinOp::Eq, lhs, rhs),
TypeOf(lhs, x),
TypeOf(rhs, x);
TypeOf(id, t) <-
ELiteral(id, t);
TypeOf(id, tid) <-
IsUnit(tid),
ELet(id, _name, t, init_expr),
TypeOf(init_expr, t);
TypeOf(id, tid) <-
IsUnit(tid),
ELetInfer(id, _name, init_expr),
TypeOf(init_expr, _);
TypeOf(id, t) <-
EVarRef(id, name),
ELet(let_id, name, t, _init_expr),
// Makes sure the let expr typechecks too.
// Maybe unnecessary, depending on what we know
// about our AST already.
TypeOf(let_id, t_output),
IsUnit(t_output);
// Can we do type inference?
TypeOf(id, t) <-
EVarRef(id, name),
ELetInfer(let_id, name, init_expr),
TypeOf(init_expr, t),
TypeOf(let_id, t_output),
IsUnit(t_output);
TypeOf(id, t) <-
EVarRef(id, name),
ELambda(_lambda_id, name, t, _rettype, _body) ;
TypeOf(id, tid) <-
EMakeRef(id, pointed_at),
TypeOf(pointed_at, inner_type),
DefRefType(tid, inner_type);
TypeOf(id, tid) <-
ELambda(id, _argname, argtype, rettype, body),
TypeOf(body, rettype),
DefFunType(tid, argtype, rettype);
TypeOf(id, tid) <-
EApply(id, fnexpr, arg),
TypeOf(fnexpr, fntype), // Get the function's type
DefFunType(fntype, argtype, tid), // what are the function's arg and ret types?
TypeOf(arg, argtype); // arg expr is correct type
TypeError(id) <-
Expr(id),
!TypeOf(id, _);
}
let mut runtime = Crepe::new();
let program1 = vec![
ELiteral("0", "I32"),
ELiteral("1", "I32"),
ELiteral("2.0", "F32"),
ELiteral("3.0", "F32"),
ELiteral("3", "I32"),
];
let program2 = vec![
EBinOp("0+1", BinOp::Add, "0", "1"),
EBinOp("0==1", BinOp::Eq, "0", "1"),
EBinOp("0==2.0", BinOp::Eq, "0", "2.0"),
EBinOp("2.0==3.0", BinOp::Eq, "2.0", "3.0"),
EBinOp("0+3.0", BinOp::Add, "0", "3.0"),
EBinOp("2.0+3.0", BinOp::Add, "2.0", "3.0"),
EBinOp("foo+foo", BinOp::Add, "foo", "foo"),
EBinOp("bar3+foo", BinOp::Add, "bar3", "foo"),
EBinOp("bar4+foo", BinOp::Add, "bar4", "foo"),
];
let program3 = vec![
ELet("let foo: I32 = 0", "foo", "I32", "0"),
ELet("let bar: F32 = 2.0", "bar", "F32", "2.0"),
ELet("let baz: I32 = 2.0", "baz", "I32", "2.0"), // (failure)
];
let program4 = vec![
ELetInfer("let foo2 = 0", "foo2", "0"),
ELetInfer("let bar2 = 2.0", "bar2", "2.0"),
ELetInfer("let baz2 = 0 + 3.0", "baz2", "0+3.0"), // (failure)
ELetInfer(
"let fn1 = fn(bar3 I32) I32 = bar3 + foo",
"fn1",
"fn(bar3 I32) I32 = bar3 + foo",
),
];
let program5 = vec![
EVarRef("foo", "foo"),
EVarRef("bar", "bar"),
EVarRef("baz", "baz"), // (failure, undeclared var)
EVarRef("foo2", "foo2"),
EVarRef("bar2", "bar2"),
EVarRef("baz2", "baz2"), // failure, typecheck fails
EVarRef("bar3", "bar3"),
EVarRef("bar4", "bar4"),
EVarRef("fn1", "fn1"),
];
let program6 = vec![
EMakeRef("&foo", "foo"), // &foo
EMakeRef("&(0+1)", "0+1"), // &(0 + 1)
EMakeRef("&&foo", "&foo"), // &&foo
];
let program7 = vec![
ELambda("fn(_ I32) I32 = foo + foo", "_", "I32", "I32", "foo+foo"),
ELambda("fn(_ I32) I32 = bar", "_", "I32", "I32", "bar"), // failure
ELambda(
"fn(bar3 I32) I32 = bar3 + foo",
"bar3",
"I32",
"I32",
"bar3+foo",
),
ELambda(
"fn(bar4 F32) I32 = bar4 + foo",
"bar4",
"F32",
"I32",
"bar4+foo",
), // failure
];
let program8 = vec![EApply("apply(fn1, 3)", "fn1", "3")];
runtime.extend(program1);
runtime.extend(program2);
runtime.extend(program3);
runtime.extend(program4);
runtime.extend(program5);
runtime.extend(program6);
runtime.extend(program7);
runtime.extend(program8);
let (res1, res2) = runtime.run();
println!("{:<20} : {:>10}", "expr", "type");
let mut successes = 0;
let mut failures = 0;
for TypeOf(name, t) in res1 {
println!("{:<20} : {:>10}", name, t);
successes += 1;
}
println!();
println!("Type errors:");
for TypeError(res) in res2 {
println!("{}", res);
failures += 1;
}
println!("Successes/failures: {}/{}", successes, failures);
}
fn main() {
typecheck3()
}