tweag/nickel
1
1
Fork 0
mirror of https://github.com/tweag/nickel.git synced 2024-09-19 07:28:22 +03:00
Code Issues Projects Releases Wiki Activity

Working implementation of enums.

Browse Source
This commit is contained in:
Teodoro Freund 2020-01-21 11:30:21 +01:00
parent 7c61e1a4ae
commit 8b5549f2db
9 changed files with 423 additions and 43 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Cargo.lock generated
View File

@ -249,6 +249,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
name = "nickel"
version = "0.1.0"
dependencies = [
"either 1.5.3 (registry+https://github.com/rust-lang/crates.io-index)",
"lalrpop 0.16.3 (registry+https://github.com/rust-lang/crates.io-index)",
"lalrpop-util 0.16.3 (registry+https://github.com/rust-lang/crates.io-index)",
"pretty_assertions 0.5.1 (registry+https://github.com/rust-lang/crates.io-index)",

1
Cargo.toml
View File

@ -13,6 +13,7 @@ lalrpop = "0.16.2"
[dependencies]
lalrpop-util = "0.16.2"
regex = "0.2.1"
either = "1.5.3"
[dev-dependencies]
pretty_assertions = "0.5.1"

26
src/grammar.lalrpop
View File

@ -3,6 +3,7 @@ use crate::label::{Label, TyPath};
use crate::term::{BinaryOp, RichTerm, Term, UnaryOp};
use crate::types::{Types, AbsType};
use std::str::FromStr;
use either::*;
grammar;
@ -45,6 +46,7 @@ Atom: RichTerm = {
Bool => RichTerm::new(Term::Bool(<>)),
Str => RichTerm::new(Term::Str(<>)),
Ident => RichTerm::new(Term::Var(<>)),
"`" <Ident> => RichTerm::new(Term::Enum(<>)),
};
Pattern: Ident = {
@ -77,8 +79,22 @@ UOp: UnaryOp = {
"goCodom" => UnaryOp::GoCodom(),
"tag[" <DbgStr> "]" => UnaryOp::Tag(<>),
"wrap" => UnaryOp::Wrap(),
"embed" <Ident> => UnaryOp::Embed(<>),
"switch" "{" <ds: (switch_def ",")*> "}" =>
UnaryOp::Switch(
ds.clone().into_iter().map(|x| x.0).filter_map(
|x| match x {Left(y) => Some(y), Right(_) => None}
).collect(),
ds.into_iter().map(|x| x.0).find_map(
|x| match x {Left(_) => None, Right(y) => Some(y)})
),
};
switch_def: Either<(Ident, RichTerm), RichTerm> = {
<id: Ident> "=>" <t: SpTerm<Atom> > => Left((id, t)),
"_" "=>" <SpTerm<Atom>> => Right(<>),
}
BOpIn: BinaryOp = {
"+" => BinaryOp::Plus(),
"++" => BinaryOp::PlusStr(),
@ -107,6 +123,16 @@ subType : Types = {
<Ident> => Types(AbsType::Var(<>)),
"#" <SpTerm<RichTerm>> => Types(AbsType::Flat(<>)),
"(" <Types> ")" => <>,
"(|" <r:(<Ident> ",")*> "|" <rest: Ident?> ")" =>
r.iter().fold(
Types(
match rest {
Some(id) => AbsType::Var(id),
None => AbsType::RowEmpty(),
}
),
|t, i| Types(AbsType::RowExtend(i.clone(), Box::new(t)))),
"<" <subType> ">" => Types(AbsType::Enum(Box::new(<>))),
};
DbgStr: String = r"[[:alpha:]_][[:word:]-]*" => <>.to_string();

2
src/main.rs
View File

@ -11,6 +11,8 @@ mod types;
use crate::program::Program;
extern crate either;
fn main() {
let mut p = Program::new_from_stdin();
match p.eval() {

28
src/operation.rs
View File

@ -38,7 +38,7 @@ fn process_unary_operation(
) -> Result<Closure, EvalError> {
let Closure {
body: RichTerm { term: t, .. },
env: _env,
env,
} = clos;
match u_op {
UnaryOp::Ite() => {
@ -101,6 +101,32 @@ fn process_unary_operation(
)))
}
}
UnaryOp::Embed(_id) => {
if let en @ Term::Enum(_) = *t {
Ok(Closure::atomic_closure(en.into()))
} else {
Err(EvalError::TypeError(format!("Expected Enum, got {:?}", *t)))
}
}
UnaryOp::Switch(mut m, d) => {
if let Term::Enum(en) = *t {
match m.remove(&en) {
Some(ex) => Ok(Closure { body: ex, env: env }),
None => match d {
Some(ex) => Ok(Closure { body: ex, env: env }),
None => Err(EvalError::TypeError(format!(
"Expected Enum in {:?}, got {:?}",
m, en
))),
},
}
} else {
match d {
Some(ex) => Ok(Closure { body: ex, env: env }),
None => Err(EvalError::TypeError(format!("Expected Enum, got {:?}", *t))),
}
}
}
UnaryOp::ChangePolarity() => {
if let Term::Lbl(mut l) = *t {
l.polarity = !l.polarity;

21
src/program.rs
View File

@ -194,17 +194,28 @@ impl<T: Read> Program<T> {
fn contracts() -> String {
"let dyn = fun l => fun t => t in
let num = fun l => fun t => if isNum t then t else blame (tag[num] l) in
let bool = fun l => fun t => if isBool t then t else blame (tag[bool] l) in
let string = fun l => fun t => if isStr t then t else blame (tag[str] l) in
let func = fun s => fun t => fun l => fun e =>
let num = fun l => fun t => if isNum t then t else blame (tag[num] l) in
let bool = fun l => fun t => if isBool t then t else blame (tag[bool] l) in
let string = fun l => fun t => if isStr t then t else blame (tag[str] l) in
let func = fun s => fun t => fun l => fun e =>
let l = tag[func] l in if isFun e then (fun x => t (goCodom l) (e (s (chngPol (goDom l)) x))) else blame l in
let forall_var = fun sy => fun pol => fun l => fun t => let lPol = polarity l in
let forall_var = fun sy => fun pol => fun l => fun t => let lPol = polarity l in
if pol =b lPol then
unwrap sy t (blame (tag[unwrp] l))
else
wrap sy t
in
let fail = fun l => fun t => blame (tag[fail] l) in
let row_extend = fun contr => fun case => fun l => fun t =>
if (case t) then t else contr (tag[NotRowExt] l) t
in
".to_string()
}
}

8
src/term.rs
View File

@ -1,6 +1,7 @@
use crate::identifier::Ident;
use crate::label::Label;
use crate::types::Types;
use std::collections::HashMap;
#[derive(Debug, PartialEq, Clone)]
pub enum Term {
@ -14,6 +15,8 @@ pub enum Term {
Let(Ident, RichTerm, RichTerm),
App(RichTerm, RichTerm),
Var(Ident),
// Enums
Enum(Ident),
// Primitives
Op1(UnaryOp, RichTerm),
Op2(BinaryOp, RichTerm, RichTerm),
@ -31,7 +34,7 @@ impl Term {
{
use self::Term::*;
match self {
Bool(_) | Num(_) | Str(_) | Lbl(_) | Var(_) | Sym(_) => {}
Bool(_) | Num(_) | Str(_) | Lbl(_) | Var(_) | Sym(_) | Enum(_) => {}
Fun(_, ref mut t)
| Op1(_, ref mut t)
| Promise(_, _, ref mut t)
@ -62,6 +65,9 @@ pub enum UnaryOp {
Blame(),
Embed(Ident),
Switch(HashMap<Ident, RichTerm>, Option<RichTerm>),
ChangePolarity(),
Pol(),
GoDom(),

331
src/typecheck.rs
View File

@ -1,26 +1,30 @@
use crate::identifier::Ident;
use crate::term::{BinaryOp, Term, UnaryOp};
use crate::types::{AbsType, Types};
use std::collections::HashMap;
use std::collections::{HashMap, HashSet};
// Type checking
pub fn type_check(t: &Term) -> Result<(), String> {
pub fn type_check(t: &Term) -> Result<Types, String> {
let mut s = GTypes::new();
let mut c = GConstr::new();
let ty = TypeWrapper::Ptr(new_var(&mut s));
type_check_(HashMap::new(), &mut s, t, ty, false)
type_check_(HashMap::new(), &mut s, &mut c, t, ty.clone(), false)?;
Ok(to_type(&s, ty)?)
}
fn type_check_(
mut typed_vars: HashMap<Ident, TypeWrapper>,
s: &mut GTypes,
c: &mut GConstr,
t: &Term,
ty: TypeWrapper,
strict: bool,
) -> Result<(), String> {
match t {
Term::Bool(_) => unify(s, ty, TypeWrapper::Concrete(AbsType::Bool()), strict),
Term::Num(_) => unify(s, ty, TypeWrapper::Concrete(AbsType::Num()), strict),
Term::Str(_) => unify(s, ty, TypeWrapper::Concrete(AbsType::Str()), strict),
Term::Bool(_) => unify(s, c, ty, TypeWrapper::Concrete(AbsType::Bool()), strict),
Term::Num(_) => unify(s, c, ty, TypeWrapper::Concrete(AbsType::Num()), strict),
Term::Str(_) => unify(s, c, ty, TypeWrapper::Concrete(AbsType::Str()), strict),
Term::Fun(x, rt) => {
let src = TypeWrapper::Ptr(new_var(s));
// TODO what to do here, this makes more sense to me, but it means let x = foo in bar
@ -30,14 +34,14 @@ fn type_check_(
let arr =
TypeWrapper::Concrete(AbsType::arrow(Box::new(src.clone()), Box::new(trg.clone())));
unify(s, ty, arr, strict)?;
unify(s, c, ty, arr, strict)?;
typed_vars.insert(x.clone(), src);
type_check_(typed_vars, s, rt.as_ref(), trg, strict)
type_check_(typed_vars, s, c, rt.as_ref(), trg, strict)
}
Term::Lbl(_) => {
// TODO implement lbl type
unify(s, ty, TypeWrapper::Concrete(AbsType::Dyn()), strict)
unify(s, c, ty, TypeWrapper::Concrete(AbsType::Dyn()), strict)
}
Term::Let(x, re, rt) => {
let e = re.as_ref();
@ -50,18 +54,18 @@ fn type_check_(
};
let instantiated = instantiate_foralls_with(s, exp.clone(), TypeWrapper::Constant)?;
type_check_(typed_vars.clone(), s, e, instantiated, strict)?;
type_check_(typed_vars.clone(), s, c, e, instantiated, strict)?;
// TODO move this up once lets are rec
typed_vars.insert(x.clone(), exp);
type_check_(typed_vars, s, rt.as_ref(), ty, strict)
type_check_(typed_vars, s, c, rt.as_ref(), ty, strict)
}
Term::App(re, rt) => {
let src = TypeWrapper::Ptr(new_var(s));
let arr = TypeWrapper::Concrete(AbsType::arrow(Box::new(src.clone()), Box::new(ty)));
type_check_(typed_vars.clone(), s, re.as_ref(), arr, strict)?;
type_check_(typed_vars, s, rt.as_ref(), src, strict)
type_check_(typed_vars.clone(), s, c, re.as_ref(), arr, strict)?;
type_check_(typed_vars, s, c, rt.as_ref(), src, strict)
}
Term::Var(x) => {
let x_ty = typed_vars
@ -69,16 +73,31 @@ fn type_check_(
.ok_or_else(|| format!("Found an unbound var {:?}", x))?;
let instantiated = instantiate_foralls_with(s, x_ty.clone(), TypeWrapper::Ptr)?;
unify(s, ty, instantiated, strict)
unify(s, c, ty, instantiated, strict)
}
Term::Enum(id) => {
let row = TypeWrapper::Ptr(new_var(s));
// Do we really need to constraint on enums?
// What's the meaning of this?
constraint(s, c, row.clone(), id.clone())?;
unify(
s,
c,
ty,
TypeWrapper::Concrete(AbsType::Enum(Box::new(TypeWrapper::Concrete(
AbsType::RowExtend(id.clone(), Box::new(row)),
)))),
strict,
)
}
Term::Op1(op, rt) => {
let ty_op = get_uop_type(s, op);
let ty_op = get_uop_type(typed_vars.clone(), s, c, op, strict)?;
let src = TypeWrapper::Ptr(new_var(s));
let arr = TypeWrapper::Concrete(AbsType::arrow(Box::new(src.clone()), Box::new(ty)));
unify(s, arr, ty_op, strict)?;
type_check_(typed_vars, s, rt.as_ref(), src, strict)
unify(s, c, arr, ty_op, strict)?;
type_check_(typed_vars, s, c, rt.as_ref(), src, strict)
}
Term::Op2(op, re, rt) => {
let ty_op = get_bop_type(s, op);
@ -93,31 +112,30 @@ fn type_check_(
))),
));
unify(s, arr, ty_op, strict)?;
type_check_(typed_vars.clone(), s, re.as_ref(), src1, strict)?;
type_check_(typed_vars, s, rt.as_ref(), src2, strict)
unify(s, c, arr, ty_op, strict)?;
type_check_(typed_vars.clone(), s, c, re.as_ref(), src1, strict)?;
type_check_(typed_vars, s, c, rt.as_ref(), src2, strict)
}
Term::Promise(ty2, _, rt) => {
let tyw2 = to_typewrapper(ty2.clone());
let instantiated = instantiate_foralls_with(s, tyw2, TypeWrapper::Constant)?;
unify(s, ty.clone(), to_typewrapper(ty2.clone()), strict)?;
type_check_(typed_vars, s, rt.as_ref(), instantiated, true)
unify(s, c, ty.clone(), to_typewrapper(ty2.clone()), strict)?;
type_check_(typed_vars, s, c, rt.as_ref(), instantiated, true)
}
Term::Assume(ty2, _, rt) => {
unify(s, ty.clone(), to_typewrapper(ty2.clone()), strict)?;
unify(s, c, ty.clone(), to_typewrapper(ty2.clone()), strict)?;
let new_ty = TypeWrapper::Ptr(new_var(s));
type_check_(typed_vars, s, rt.as_ref(), new_ty, false)
type_check_(typed_vars, s, c, rt.as_ref(), new_ty, false)
}
Term::Sym(_) => unify(s, ty, TypeWrapper::Concrete(AbsType::Sym()), strict),
Term::Wrapped(_, rt) => type_check_(typed_vars, s, rt.as_ref(), ty, strict),
Term::Sym(_) => unify(s, c, ty, TypeWrapper::Concrete(AbsType::Sym()), strict),
Term::Wrapped(_, rt) => type_check_(typed_vars, s, c, rt.as_ref(), ty, strict),
}
}
// TypeWrapper
// A type can be a concrete type, or a type variable
// A type can be a concrete type, a constant or a type variable
#[derive(Clone, PartialEq, Debug)]
pub enum TypeWrapper {
Concrete(AbsType<Box<TypeWrapper>>),
@ -131,6 +149,7 @@ impl TypeWrapper {
match self {
Concrete(AbsType::Var(ref i)) if *i == id => to,
Concrete(AbsType::Var(i)) => Concrete(AbsType::Var(i)),
Concrete(AbsType::Forall(i, t)) => {
if i == id {
Concrete(AbsType::Forall(i, t))
@ -152,14 +171,75 @@ impl TypeWrapper {
Concrete(AbsType::Arrow(Box::new(fs), Box::new(ft)))
}
Concrete(AbsType::RowEmpty()) => Concrete(AbsType::RowEmpty()),
Concrete(AbsType::RowExtend(tag, rest)) => {
Concrete(AbsType::RowExtend(tag, Box::new(rest.subst(id, to))))
}
Concrete(AbsType::Enum(row)) => Concrete(AbsType::Enum(Box::new(row.subst(id, to)))),
Constant(x) => Constant(x),
Ptr(x) => Ptr(x),
}
}
}
/// Add an identifier to a row.
///
/// If the id is not there, and the row is open, it will add it.
///
/// # Returns
///
/// The row without the added id.
fn row_add(
state: &mut GTypes,
c: &mut GConstr,
id: Ident,
mut r: TypeWrapper,
) -> Result<TypeWrapper, String> {
if let TypeWrapper::Ptr(p) = r {
r = get_root(state, p)?;
}
match r {
TypeWrapper::Concrete(AbsType::RowEmpty()) => Err("The row didn't have the id".to_string()),
TypeWrapper::Concrete(AbsType::RowExtend(id2, r2)) => {
if id == id2 {
Ok(*r2)
} else {
let subrow = row_add(state, c, id, *r2)?;
Ok(TypeWrapper::Concrete(AbsType::RowExtend(
id2,
Box::new(subrow),
)))
}
}
TypeWrapper::Concrete(not_row) => Err(format!("Expected a row, got {:?}", not_row)),
TypeWrapper::Ptr(root) => {
if let Some(set) = c.get(&root) {
if set.contains(&id) {
return Err(format!(
"Tried to add {:?} to the row, but it was constrained.",
id
));
}
}
let new_row = TypeWrapper::Ptr(new_var(state));
constraint(state, c, new_row.clone(), id.clone())?;
state.insert(
root,
Some(TypeWrapper::Concrete(AbsType::RowExtend(
id,
Box::new(new_row.clone()),
))),
);
Ok(new_row)
}
TypeWrapper::Constant(_) => Err("Expected a row, got a constant".to_string()),
}
}
pub fn unify(
state: &mut GTypes,
c: &mut GConstr,
mut t1: TypeWrapper,
mut t2: TypeWrapper,
strict: bool,
@ -183,6 +263,10 @@ pub fn unify(
(AbsType::Bool(), AbsType::Bool()) => Ok(()),
(AbsType::Str(), AbsType::Str()) => Ok(()),
(AbsType::Sym(), AbsType::Sym()) => Ok(()),
(AbsType::Arrow(s1s, s1t), AbsType::Arrow(s2s, s2t)) => {
unify(state, c, *s1s, *s2s, strict)?;
unify(state, c, *s1t, *s2t, strict)
}
(AbsType::Flat(s), AbsType::Flat(t)) => {
if let Term::Var(s) = s.clone().into() {
if let Term::Var(t) = t.clone().into() {
@ -193,10 +277,12 @@ pub fn unify(
}
Err(format!("Two expressions didn't match {:?} - {:?}", s, t))
} // Right now it only unifies equally named variables
(AbsType::Arrow(s1s, s1t), AbsType::Arrow(s2s, s2t)) => {
unify(state, *s1s, *s2s, strict)?;
unify(state, *s1t, *s2t, strict)
(AbsType::RowEmpty(), AbsType::RowEmpty()) => Ok(()),
(AbsType::RowExtend(id, t), r2 @ AbsType::RowExtend(_, _)) => {
let r2 = row_add(state, c, id, TypeWrapper::Concrete(r2))?;
unify(state, c, *t, r2, strict)
}
(AbsType::Enum(r), AbsType::Enum(r2)) => unify(state, c, *r, *r2, strict),
(AbsType::Var(ref i1), AbsType::Var(ref i2)) if i1 == i2 => Ok(()),
(AbsType::Forall(i1, t1t), AbsType::Forall(i2, t2t)) => {
// Very stupid (slow) implementation
@ -204,6 +290,7 @@ pub fn unify(
unify(
state,
c,
t1t.subst(i1, constant_type.clone()),
t2t.subst(i2, constant_type),
strict,
@ -238,6 +325,20 @@ fn to_typewrapper(t: Types) -> TypeWrapper {
TypeWrapper::Concrete(t3)
}
fn to_type(s: &GTypes, ty: TypeWrapper) -> Result<Types, String> {
Ok(match ty {
TypeWrapper::Ptr(p) => match get_root(s, p)? {
t @ TypeWrapper::Concrete(_) => to_type(s, t)?,
_ => Types(AbsType::Dyn()),
},
TypeWrapper::Constant(_) => Types(AbsType::Dyn()),
TypeWrapper::Concrete(t) => {
let mapped = t.map(|btyp| Box::new(to_type(s, *btyp).unwrap()));
Types(mapped)
}
})
}
fn instantiate_foralls_with<F>(
s: &mut GTypes,
mut ty: TypeWrapper,
@ -257,8 +358,14 @@ where
Ok(ty)
}
pub fn get_uop_type(s: &mut GTypes, op: &UnaryOp) -> TypeWrapper {
match op {
pub fn get_uop_type(
typed_vars: HashMap<Ident, TypeWrapper>,
s: &mut GTypes,
c: &mut GConstr,
op: &UnaryOp,
strict: bool,
) -> Result<TypeWrapper, String> {
Ok(match op {
UnaryOp::Ite() => {
let branches = TypeWrapper::Ptr(new_var(s));
@ -297,6 +404,50 @@ pub fn get_uop_type(s: &mut GTypes, op: &UnaryOp) -> TypeWrapper {
Box::new(TypeWrapper::Concrete(AbsType::Dyn())),
Box::new(TypeWrapper::Concrete(AbsType::Bool())),
)),
UnaryOp::Embed(id) => {
let row = TypeWrapper::Ptr(new_var(s));
constraint(s, c, row.clone(), id.clone())?;
TypeWrapper::Concrete(AbsType::Arrow(
Box::new(TypeWrapper::Concrete(AbsType::Enum(Box::new(row.clone())))),
Box::new(TypeWrapper::Concrete(AbsType::Enum(Box::new(
TypeWrapper::Concrete(AbsType::RowExtend(id.clone(), Box::new(row))),
)))),
))
}
UnaryOp::Switch(l, d) => {
// Currently, if it has a default value, we typecheck the whole thing as
// taking ANY enum, since it's more permissive and there's not a loss of information
let res = TypeWrapper::Ptr(new_var(s));
for (_, exp) in l {
type_check_(typed_vars.clone(), s, c, exp.as_ref(), res.clone(), strict)?;
}
let row = match d {
Some(e) => {
type_check_(typed_vars.clone(), s, c, e.as_ref(), res.clone(), strict)?;
TypeWrapper::Ptr(new_var(s))
}
None => l.into_iter().try_fold(
TypeWrapper::Concrete(AbsType::RowEmpty()),
|acc, x| -> Result<TypeWrapper, String> {
constraint(s, c, acc.clone(), x.0.clone())?;
Ok(TypeWrapper::Concrete(AbsType::RowExtend(
x.0.clone(),
Box::new(acc),
)))
},
)?,
};
TypeWrapper::Concrete(AbsType::Arrow(
Box::new(TypeWrapper::Concrete(AbsType::Enum(Box::new(row)))),
Box::new(res),
))
}
UnaryOp::ChangePolarity() | UnaryOp::GoDom() | UnaryOp::GoCodom() | UnaryOp::Tag(_) => {
TypeWrapper::Concrete(AbsType::arrow(
Box::new(TypeWrapper::Concrete(AbsType::Dyn())),
@ -310,7 +461,7 @@ pub fn get_uop_type(s: &mut GTypes, op: &UnaryOp) -> TypeWrapper {
Box::new(TypeWrapper::Concrete(AbsType::Dyn())),
))),
)),
}
})
}
pub fn get_bop_type(_s: &mut GTypes, op: &BinaryOp) -> TypeWrapper {
@ -352,6 +503,7 @@ pub fn get_bop_type(_s: &mut GTypes, op: &BinaryOp) -> TypeWrapper {
// Global types, where unification happens
pub type GTypes = HashMap<usize, Option<TypeWrapper>>;
pub type GConstr = HashMap<usize, HashSet<Ident>>;
fn new_var(state: &mut GTypes) -> usize {
let nxt = state.len();
@ -359,6 +511,35 @@ fn new_var(state: &mut GTypes) -> usize {
nxt
}
fn constraint(s: &mut GTypes, cons: &mut GConstr, x: TypeWrapper, id: Ident) -> Result<(), String> {
match x {
TypeWrapper::Ptr(p) => {
let ty = get_root(s, p)?;
match ty {
ty @ TypeWrapper::Concrete(_) => constraint(s, cons, ty, id),
TypeWrapper::Ptr(root) => {
if let Some(v) = cons.get_mut(&root) {
v.insert(id);
} else {
cons.insert(root, vec![id].into_iter().collect());
}
Ok(())
}
TypeWrapper::Constant(_) => Err("Can't constraint a constant".to_string()),
}
}
TypeWrapper::Concrete(AbsType::RowEmpty()) => Ok(()),
TypeWrapper::Concrete(AbsType::RowExtend(id2, t)) => {
if id2 == id {
Err(format!("The id {:?} was present on the row", id))
} else {
constraint(s, cons, *t, id)
}
}
_ => Err(format!("Can't constraint a {:?}", x)),
}
}
// TODO This should be a union find like algorithm
pub fn get_root(s: &GTypes, x: usize) -> Result<TypeWrapper, String> {
match s
@ -380,7 +561,7 @@ mod tests {
use crate::parser;
fn parse_and_typecheck(s: &str) -> Result<(), String> {
fn parse_and_typecheck(s: &str) -> Result<Types, String> {
if let Ok(p) = parser::grammar::TermParser::new().parse(s) {
type_check(p.as_ref())
} else {
@ -551,4 +732,84 @@ mod tests {
)
.unwrap_err();
}
#[test]
fn enum_simple() {
parse_and_typecheck("Promise(< (| bla, |) >, `bla)").unwrap();
parse_and_typecheck("Promise(< (| bla, |) >, `blo)").unwrap_err();
parse_and_typecheck("Promise(< (| bla, blo, |) >, `blo)").unwrap();
parse_and_typecheck("Promise(forall r. < (| bla, | r ) >, `bla)").unwrap();
parse_and_typecheck("Promise(forall r. < (| bla, blo, | r ) >, `bla)").unwrap();
parse_and_typecheck("Promise(Num, switch { bla => 3, } `bla)").unwrap();
parse_and_typecheck("Promise(Num, switch { bla => 3, } `blo)").unwrap_err();
parse_and_typecheck("Promise(Num, switch { bla => 3, _ => 2, } `blo)").unwrap();
parse_and_typecheck("Promise(Num, switch { bla => 3, ble => true, } `bla)").unwrap_err();
}
#[test]
fn enum_complex() {
parse_and_typecheck(
"Promise(< (| bla, ble, |) > -> Num, fun x => switch {bla => 1, ble => 2,} x)",
)
.unwrap();
parse_and_typecheck(
"Promise(< (| bla, ble, |) > -> Num,
fun x => switch {bla => 1, ble => 2, bli => 4,} x)",
)
.unwrap_err();
parse_and_typecheck(
"Promise(< (| bla, ble, |) > -> Num,
fun x => switch {bla => 1, ble => 2, bli => 4,} (embed bli x))",
)
.unwrap();
parse_and_typecheck(
"Promise(Num,
(fun x =>
(switch {bla => 3, bli => 2,} x) +
(switch {bli => 6, bla => 20,} x) ) `bla)",
)
.unwrap();
// TODO typecheck this, I'm not sure how to do it with row variables
parse_and_typecheck(
"Promise(Num,
(fun x =>
(switch {bla => 3, bli => 2,} x) +
(switch {bla => 6, blo => 20,} x) ) `bla)",
)
.unwrap_err();
parse_and_typecheck(
"let f = Promise(
forall r. < (| blo, ble, | r )> -> Num,
fun x => (switch {blo => 1, ble => 2, _ => 3, } x ) ) in
Promise(Num, f `bli)",
)
.unwrap();
parse_and_typecheck(
"let f = Promise(
forall r. < (| blo, ble, | r )> -> Num,
fun x => (switch {blo => 1, ble => 2, bli => 3, } x ) ) in
f",
)
.unwrap_err();
parse_and_typecheck(
"let f = Promise(
forall r. (forall p. < (| blo, ble, | r )> -> < (| bla, bli, | p) > ),
fun x => (switch {blo => `bla, ble => `bli, _ => `bla, } x ) ) in
f `bli",
)
.unwrap();
parse_and_typecheck(
"let f = Promise(
forall r. (forall p. < (| blo, ble, | r )> -> < (| bla, bli, | p) > ),
fun x => (switch {blo => `bla, ble => `bli, _ => `blo, } x ) ) in
f `bli",
)
.unwrap_err();
}
}

48
src/types.rs
View File

@ -1,5 +1,5 @@
use crate::identifier::Ident;
use crate::term::{RichTerm, Term};
use crate::term::{RichTerm, Term, UnaryOp};
use std::collections::HashMap;
#[derive(Clone, PartialEq, Debug)]
@ -13,6 +13,11 @@ pub enum AbsType<Ty> {
Arrow(Ty, Ty),
Var(Ident),
Forall(Ident, Ty),
// A kind system would be nice
RowEmpty(),
RowExtend(Ident, Ty /* Row */),
Enum(Ty /* Row */),
}
impl<Ty> AbsType<Ty> {
@ -36,6 +41,9 @@ impl<Ty> AbsType<Ty> {
AbsType::Forall(i, ft)
}
AbsType::RowEmpty() => AbsType::RowEmpty(),
AbsType::RowExtend(id, t) => AbsType::RowExtend(id, f(t)),
AbsType::Enum(t) => AbsType::Enum(f(t)),
}
}
@ -90,6 +98,44 @@ impl Types {
*sy += 1;
t.contract_open(h, pol, sy)
}
AbsType::RowEmpty() | AbsType::RowExtend(_, _) => {
panic!("These types should not be checked at runtime!")
}
AbsType::Enum(ref r) => {
fn form(ty: Types, h: HashMap<Ident, RichTerm>) -> RichTerm {
match ty.0 {
AbsType::RowEmpty() => RichTerm::var("fail".to_string()),
AbsType::RowExtend(id, rest) => {
let rest_contract = form(*rest, h);
let mut map = HashMap::new();
map.insert(id, Term::Bool(true).into());
RichTerm::app(
RichTerm::app(
RichTerm::var("row_extend".to_string()),
rest_contract,
),
Term::Fun(
Ident("x".to_string()),
Term::Op1(
UnaryOp::Switch(map, Some(Term::Bool(false).into())),
Term::Var(Ident("x".to_string())).into(),
)
.into(),
)
.into(),
)
}
AbsType::Var(ref i) => {
let rt = h.get(i).expect(&format!("Unbound type variable {:?}", i));
rt.clone()
}
not_row => panic!("It should be a row!! {:?}", not_row),
}
}
form(*r.clone(), h)
}
}
}
}