diff --git a/Cargo.toml b/Cargo.toml index ce8c55858..1c0aab9f6 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -23,4 +23,4 @@ lalrpop = "0.13.1" [dev-dependencies] difference = "1.0.0" -pretty_assertions = "0.3.4" +pretty_assertions = "0.4.0" diff --git a/experiments/lean/README.md b/experiments/lean/README.md index a08de5b15..a69b7238f 100644 --- a/experiments/lean/README.md +++ b/experiments/lean/README.md @@ -5,6 +5,8 @@ implementation. Many theorems and lemmas remain to be been proven. It would be very nice to provide more guarentees in the future that our Rust implementation matches this formalisation, but that is out of scope for now! +## Setup + To work with the formalisations, you will need to [install Lean 3.3][install_lean]. Then run the following commands in the shell: @@ -16,7 +18,7 @@ leanpkg build [install_lean]: https://leanprover.github.io/download/ -## Note for VS Code users +### Note for VS Code users Note that the VS Code extension doesn't work correctly with packages in sub-directories at the time of writing, so you'll need to open a new editor diff --git a/src/ast.rs b/src/ast.rs deleted file mode 100644 index 0d9a2b6cd..000000000 --- a/src/ast.rs +++ /dev/null @@ -1,256 +0,0 @@ -//! The syntax of our data description language - -use std::fmt; - -use source::Span; - -#[derive(Debug, Clone, PartialEq, Eq)] -pub enum Kind { - Type, - Binary, -} - -/// A type definition -/// -/// ```plain -/// Point = { -/// x : u16, -/// y : u16, -/// } -/// ``` -#[derive(Debug, Clone, PartialEq, Eq)] -pub struct Definition { - pub span: Span, - pub name: String, - pub ty: Type, -} - -impl Definition { - pub fn new(span: Sp, name: S, ty: Type) -> Definition - where - Sp: Into, - S: Into, - { - let span = span.into(); - let name = name.into(); - - Definition { span, name, ty } - } -} - -#[derive(Copy, Clone, PartialEq, Eq)] -pub enum Const { - /// A boolean constant: eg. `true`, `false` - Bool(bool), - /// An integer constant: eg. `0`, `1`, `2`, ... - Int(i64), -} - -impl fmt::Debug for Const { - fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { - match *self { - Const::Bool(value) => write!(f, "Bool({:?})", value), - Const::Int(value) => write!(f, "Int({:?})", value), - } - } -} - -/// An unary operator -#[derive(Debug, Copy, Clone, PartialEq, Eq)] -pub enum Unop { - /// Not: eg. `!x` - Not, - /// Negation: eg. `-x` - Neg, -} - -/// A binary operator -#[derive(Debug, Copy, Clone, PartialEq, Eq)] -pub enum Binop { - /// Disjunction: eg. `x | y` - Or, - /// Conjunction: eg. `x & y` - And, - /// Equality: eg. `x == y` - Eq, - /// Inequality: eg. `x != y` - Ne, - /// Less than or equal: eg. `x <= y` - Le, - /// Less than: eg. `x < y` - Lt, - /// Greater than: eg. `x > y` - Gt, - /// Greater than or equal: eg. `x >= y` - Ge, - /// Addition: eg. `x + y` - Add, - /// Subtraction: eg. `x - y` - Sub, - /// Multiplication: eg. `x * y` - Mul, - /// Division: eg. `x / y` - Div, -} - -/// An expression -#[derive(Debug, Clone, PartialEq, Eq)] -pub enum Expr { - /// A constant value - Const(Span, Const), - /// A variable, referring to an integer that exists in the current - /// context: eg. `len`, `num_tables` - Var(Span, String), - /// An unary operator expression - Unop(Span, Unop, Box), - /// A binary operator expression - Binop(Span, Binop, Box, Box), -} - -impl Expr { - /// A boolean constant: eg. `true`, `false` - pub fn bool(span: Sp, value: bool) -> Expr - where - Sp: Into, - { - Expr::Const(span.into(), Const::Bool(value)) - } - - /// An integer constant: eg. `0`, `1`, `2`, ... - pub fn int(span: Sp, value: i64) -> Expr - where - Sp: Into, - { - Expr::Const(span.into(), Const::Int(value)) - } - - /// A variable, referring to an integer that exists in the current context: - /// eg. `len`, `num_tables` - pub fn var(span: Sp, name: S) -> Expr - where - Sp: Into, - S: Into, - { - Expr::Var(span.into(), name.into()) - } - - /// An unary operator expression - pub fn unop(span: Sp, op: Unop, x: T) -> Expr - where - Sp: Into, - T: Into>, - { - Expr::Unop(span.into(), op, x.into()) - } - - /// A binary operator expression - pub fn binop(span: Sp, op: Binop, x: T, y: U) -> Expr - where - Sp: Into, - T: Into>, - U: Into>, - { - Expr::Binop(span.into(), op, x.into(), y.into()) - } -} - -#[derive(Debug, Copy, Clone, PartialEq, Eq)] -pub enum Endianness { - Little, - Big, - Target, -} - -#[derive(Debug, Clone, PartialEq, Eq)] -pub enum Type { - /// A type variable: eg. `T` - Var(Span, String), - - /// Boolean - Bool, - - /// A ranged integer - matches a range of integers - RangedInt(i64, i64), - /// Unsigned integer - UInt(usize, Endianness), - /// Signed integer - SInt(usize, Endianness), - /// IEEE 754 floating point - Float(usize, Endianness), - - /// An array of the specified type, with a size: eg. `[T; n]` - Array(Span, Box, Expr), - /// A union of types: eg. `union { T, ... }` - Union(Span, Vec), - /// A struct type, with fields: eg. `struct { field : T, ... }` - Struct(Span, Vec), - /// A type constrained by a predicate: eg. `T where x => x == 3` - Where(Span, Box, String, Expr), -} - -impl Type { - /// A type variable: eg. `T` - pub fn var(span: Sp, name: S) -> Type - where - Sp: Into, - S: Into, - { - Type::Var(span.into(), name.into()) - } - - /// An array of the specified type, with a size: eg. `[T; n]` - pub fn array(span: Sp, ty: T, size: Expr) -> Type - where - Sp: Into, - T: Into>, - { - Type::Array(span.into(), ty.into(), size) - } - - /// A union of types: eg. `union { T, ... }` - pub fn union(span: Sp, tys: Vec) -> Type - where - Sp: Into, - { - Type::Union(span.into(), tys) - } - - /// A struct type, with fields: eg. `struct { field : T, ... }` - pub fn struct_(span: Sp, fields: Vec) -> Type - where - Sp: Into, - { - Type::Struct(span.into(), fields) - } - - /// A type constrained by a predicate: eg. `T where x => x == 3` - pub fn where_(span: Sp, ty: T, param: S, pred: Expr) -> Type - where - Sp: Into, - T: Into>, - S: Into, - { - Type::Where(span.into(), ty.into(), param.into(), pred) - } -} - -/// A field in a struct type -#[derive(Debug, Clone, PartialEq, Eq)] -pub struct Field { - pub span: Span, - pub name: String, - pub ty: Type, -} - -impl Field { - pub fn new(span: Sp, name: S, ty: Type) -> Field - where - Sp: Into, - S: Into, - { - let span = span.into(); - let name = name.into(); - - Field { span, name, ty } - } -} diff --git a/src/check.rs b/src/check.rs deleted file mode 100644 index c6d5b7355..000000000 --- a/src/check.rs +++ /dev/null @@ -1,711 +0,0 @@ -//! Typechecking -//! -//! # Syntax -//! -//! ## Expressions -//! -//! ```plain -//! e ::= -//! x variables -//! -//! n natural number -//! true true value -//! false false value -//! -//! -e negation -//! ¬e not -//! op(Rel, e₁, e₂) relational binary operation -//! op(Cmp, e₁, e₂) comparison binary operation -//! op(Arith, e₁, e₂) arithmetic binary operation -//! -//! Rel ::= -//! ∨ disjunction operator -//! ∧ conjunction operator -//! -//! Cmp ::= -//! = equality operator -//! ≠ inequality operator -//! < less than operator -//! ≤ less than or equal operator -//! > greater than operator -//! ≥ greater than or equal operator -//! -//! Arith ::= -//! + addition operator -//! - subtraction operator -//! * multiplication operator -//! / division operator -//! ``` -//! -//! ## Types -//! -//! ```plain -//! E ::= -//! Le little endian -//! Be big endian -//! -//! τ ::= -//! α type variables -//! -//! Bool booleans -//! -//! UInt(n, E) unsigned integer with byte size and endianness -//! SInt(n, E) two's complement signed integer with byte size and endianness -//! SingletonInt(n) matches a single integer -//! RangedInt(n₁, n₂) matches a ranged integer -//! -//! τ₁ + τ₂ sum -//! Σ x:τ₁ .τ₂ dependent pair -//! [τ; e] array -//! { x:τ | e } constrained type -//! ``` -//! -//! ## Kinds -//! -//! ```plain -//! κ ::= -//! Type kind of types -//! Binary kind of binary types -//! ``` -//! -//! # Types in the AST -//! -//! In the `ast`, we represent the above as the following: -//! -//! - `Type::Var`: variables -//! - `Type::Union`: series of unions -//! - `Type::Struct`: nested dependent pairs -//! -//! For example, the struct: -//! -//! ```plain -//! struct { len : u16, reserved : u16, data : [u16; len] } -//! ``` -//! -//! Would be desugared into: -//! -//! ```plain -//! Σ len:u16 . Σ reserved:u16 . [u16; len] -//! ``` -//! -//! Note how later fields have access to the data in previous fields. -//! -//! - `Type::Array`: TODO -//! - `Type::Where`: constrained type - -use ast::{Binop, Const, Definition, Expr, Kind, Type, Unop}; -use env::Env; -use source::Span; - -#[derive(Debug, Clone, PartialEq, Eq)] -pub enum KindError { - Type(TypeError), - UnboundType(Span, String), - ArraySizeExpectedUInt(Span, Type), - WherePredicateExpectedBool(Span, Type), -} - -impl From for KindError { - fn from(src: TypeError) -> KindError { - KindError::Type(src) - } -} - -#[derive(Debug, Clone, PartialEq, Eq)] -pub enum TypeError { - UnboundVariable(Span, String), - UnexpectedUnaryOperand(Span, Unop, Type), - UnexpectedBinaryLhs(Span, Type), - UnexpectedBinaryRhs(Span, Type), - ExpectedNumericOperands(Span, Type, Type), -} - -/// The subtyping relation: `τ₁ <: τ₂` -/// -/// # Rules -/// -/// ```plain -/// ―――――――――――――――――――― (S-REFL) -/// τ <: τ -/// -/// -/// n₃ ≤ n₁ n₂ ≤ n₄ -/// ―――――――――――――――――――――――――――――――――――――――――― (S-RANGED-INT) -/// RangedInt(n₁, n₂) <: RangedInt(n₃, n₄) -/// -/// -/// 0 ≤ n₁ n₂ ≤ 2^n₃ - 1 -/// ――――――――――――――――――――――――――――――――――――――――――――――― (S-RANGED-INT-UINT) -/// RangedInt(n₁, n₂) <: UInt(n₃, E) -/// -/// -/// -2^(n₂ - 1) ≤ n₁ n₂ ≤ 2^(n₃ - 1) - 1 -/// ――――――――――――――――――――――――――――――――――――――――――――――― (S-RANGED-INT-SINT) -/// RangedInt(n₁, n₂) <: SInt(n₃, E) -/// ``` -pub fn is_subtype(sty: &Type, ty: &Type) -> bool { - match (sty, ty) { - // S-REFL - (sty, ty) if sty == ty => true, - - // S-RANGED-INT - (&Type::RangedInt(slo, shi), &Type::RangedInt(lo, hi)) if lo <= slo && shi <= hi => true, - - // S-RANGED-INT-UINT - // FIXME: check size - (&Type::RangedInt(_, _), &Type::UInt(_, _)) => true, - - // S-RANGED-INT-SINT - // FIXME: check size - (&Type::RangedInt(_, _), &Type::SInt(_, _)) => true, - - (_, _) => false, - } -} - -pub fn is_numeric(ty: &Type) -> bool { - match *ty { - Type::RangedInt(_, _) | - Type::UInt(_, _) | - Type::SInt(_, _) => true, - // Ignore floats for now... - _ => false, - } -} - -impl<'parent> Env<'parent> { - pub fn check_defs(&mut self, defs: I) -> Result<(), KindError> - where - I: IntoIterator, - { - for def in defs { - match kind_of(self, &def.ty)? { - Kind::Type => unimplemented!(), // FIXME: Better errors - Kind::Binary => self.add_ty(def.name, def.ty), - } - } - Ok(()) - } -} - -/// The kinding relation: `Γ ⊢ τ : κ` -/// -/// # Rules -/// -/// ```plain -/// ――――――――――――――――――――――― (K-BOOL) -/// Γ ⊢ Bool : Type -/// -/// -/// n₁ ≤ n₂ -/// ――――――――――――――――――――――――――――――――――― (K-RANGED-INT) -/// Γ ⊢ RangedInt(n₁, n₂) : Binary -/// -/// -/// n > 0 -/// ――――――――――――――――――――――――――――――――――― (K-UINT) -/// Γ ⊢ UInt(n, E) : Binary -/// -/// -/// n > 0 -/// ――――――――――――――――――――――――――――――――――― (K-SINT) -/// Γ ⊢ SInt(n, E) : Binary -/// -/// -/// α ∈ Γ -/// ―――――――――――――――――――― (K-VAR) -/// Γ ⊢ α : Binary -/// -/// -/// Γ ⊢ τ₁ : Binary Γ ⊢ τ₂ : Binary -/// ―――――――――――――――――――――――――――――――――――――――――― (K-SUM) -/// Γ ⊢ τ₁ + τ₂ : Binary -/// -/// -/// Γ ⊢ τ₁ : Binary Γ, x:τ₁ ⊢ τ₂ : Binary -/// ―――――――――――――――――――――――――――――――――――――――――――――――――――――― (K-DEPENDENT-PAIR) -/// Γ ⊢ Σ x:τ₁ .τ₂ : Binary -/// -/// -/// Γ ⊢ τ : Binary Γ ⊢ e : UInt(n, E) -/// ―――――――――――――――――――――――――――――――――――――――――――――― (K-ARRAY-UINT) -/// Γ ⊢ [τ; e] : Binary -/// -/// -/// Γ ⊢ τ : Binary Γ ⊢ e : RangedInt(n₁, n₂) n₁ ≥ 0 -/// ―――――――――――――――――――――――――――――――――――――――――――――――――――――――――――― (K-ARRAY-RANGED-INT) -/// Γ ⊢ [τ; e] : Binary -/// -/// -/// Γ ⊢ τ : Binary Γ, x:τ ⊢ e : Bool -/// ―――――――――――――――――――――――――――――――――――――――――― (K-CON) -/// Γ ⊢ { x:τ | e } : Binary -/// ``` -pub fn kind_of(env: &Env, ty: &Type) -> Result { - match *ty { - // K-BOOL - Type::Bool => Ok(Kind::Type), - - // K-RANGED-INT - Type::RangedInt(lo, hi) if lo <= hi => Ok(Kind::Binary), - Type::RangedInt(_, _) => unimplemented!(), // FIXME: Better errors - - // K-UINT - Type::UInt(size, _) if size > 0 => Ok(Kind::Binary), - Type::UInt(_, _) => unimplemented!(), // FIXME: Better errors - - // K-SINT - Type::SInt(size, _) if size > 0 => Ok(Kind::Binary), - Type::SInt(_, _) => unimplemented!(), // FIXME: Better errors - - // K-??? - Type::Float(_, _) => Ok(Kind::Binary), - - // K-VAR - Type::Var(span, ref name) => { - // TODO: kind of var? - expecting only binary types in the context - match env.lookup_ty(name) { - Some(_) => Ok(Kind::Binary), - None => Err(KindError::UnboundType(span, name.clone())), - } - } - - // K-SUM - Type::Union(_, ref tys) => { - for ty in tys { - match kind_of(env, &ty)? { - Kind::Type => unimplemented!(), // FIXME: Better errors - Kind::Binary => {} - } - } - Ok(Kind::Binary) - } - - // K-DEPENDENT-PAIR - Type::Struct(_, ref fields) => { - // TODO: prevent name shadowing? - let mut inner_env = env.extend(); - for field in fields { - match kind_of(&inner_env, &field.ty)? { - Kind::Type => unimplemented!(), // FIXME: Better errors - Kind::Binary => inner_env.add_binding(field.name.clone(), field.ty.clone()), - } - } - Ok(Kind::Binary) - } - - // K-ARRAY-... - Type::Array(span, ref ty, ref size) => { - match kind_of(env, ty)? { - Kind::Type => unimplemented!(), // FIXME: Better errors - Kind::Binary => { - let expr_ty = type_of(env, size)?; - - match expr_ty { - // K-ARRAY-RANGED-INT - Type::RangedInt(lo, _) if lo >= 0 => Ok(Kind::Binary), - Type::RangedInt(_, _) => unimplemented!(), // FIXME: Better errors - - // K-ARRAY-UINT - Type::UInt(_, _) => Ok(Kind::Binary), - ty => Err(KindError::ArraySizeExpectedUInt(span, ty)), - } - } - } - } - - // K-CON - Type::Where(span, ref ty, ref param, ref pred) => { - match kind_of(env, ty)? { - Kind::Type => unimplemented!(), // FIXME: Better errors - Kind::Binary => { - let mut inner_env = env.extend(); - // TODO: prevent name shadowing? - inner_env.add_binding(param.clone(), (**ty).clone()); - match type_of(env, pred)? { - Type::Bool => Ok(Kind::Binary), - pred_ty => Err(KindError::WherePredicateExpectedBool(span, pred_ty)), - } - } - } - } - } -} - -/// The typing relation: `Γ ⊢ e : τ` -/// -/// # Rules -/// -/// ```plain -/// ―――――――――――――――――――――――――――― (T-TRUE) -/// Γ ⊢ true : Bool -/// -/// -/// ―――――――――――――――――――――――――――― (T-FALSE) -/// Γ ⊢ false : Bool -/// -/// -/// ―――――――――――――――――――――――――――― (T-RANGED-INT) -/// Γ ⊢ n : RangedInt(n, n) -/// -/// -/// x : τ ∈ Γ -/// ―――――――――――――――――――――――――――― (T-VAR) -/// Γ ⊢ x : τ -/// -/// -/// Γ ⊢ e : Bool -/// ―――――――――――――――――――――――――――― (T-NOT) -/// Γ ⊢ ¬e : Bool -/// -/// -/// Γ ⊢ e : τ isNumeric(τ) -/// ――――――――――――――――――――――――――――――――――― (T-NEG) -/// Γ ⊢ -e : τ -/// -/// -/// Γ ⊢ e₁ : Bool Γ ⊢ e₂ : Bool -/// ――――――――――――――――――――――――――――――――――――――――― (T-REL) -/// Γ ⊢ op(Rel, e₁, e₂) : Bool -/// -/// -/// Γ ⊢ e₁ : τ₁ Γ ⊢ e₂ : τ₂ τ₁ <: τ₂ isNumeric(τ₂) -/// ――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――― (T-CMP-LHS) -/// Γ ⊢ op(Cmp, e₁, e₂) : Bool -/// -/// -/// Γ ⊢ e₁ : τ₁ Γ ⊢ e₂ : τ₂ τ₂ <: τ₁ isNumeric(τ₁) -/// ――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――― (T-CMP-RHS) -/// Γ ⊢ op(Cmp, e₁, e₂) : Bool -/// -/// -/// Γ ⊢ e₁ : τ₁ Γ ⊢ e₂ : τ₂ τ₁ <: τ₂ isNumeric(τ₂) -/// ―――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――― (T-ARITH-LHS) -/// Γ ⊢ op(Arith, e₁, e₂) : τ₂ -/// -/// -/// Γ ⊢ e₁ : τ₁ Γ ⊢ e₂ : τ₂ τ₂ <: τ₁ isNumeric(τ₁) -/// ―――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――― (T-ARITH-RHS) -/// Γ ⊢ op(Arith, e₁, e₂) : τ₁ -/// ``` -pub fn type_of(env: &Env, expr: &Expr) -> Result { - match *expr { - // T-TRUE, T-FALSE - Expr::Const(_, Const::Bool(_)) => Ok(Type::Bool), - - // T-RANGED-INT - Expr::Const(_, Const::Int(value)) => Ok(Type::RangedInt(value, value)), - - // T-VAR - Expr::Var(span, ref name) => { - match env.lookup_binding(name) { - Some(ty) => Ok(ty.clone()), - None => Err(TypeError::UnboundVariable(span, name.clone())), - } - } - - Expr::Unop(span, op, ref value) => { - let value_ty = type_of(env, value)?; - - match op { - // T-NOT - Unop::Not => { - if value_ty == Type::Bool { - Ok(Type::Bool) - } else { - Err(TypeError::UnexpectedUnaryOperand(span, op, value_ty)) - } - } - // T-NEG - Unop::Neg => { - if is_numeric(&value_ty) { - Ok(value_ty) - } else { - Err(TypeError::UnexpectedUnaryOperand(span, op, value_ty)) - } - } - } - } - - Expr::Binop(span, op, ref lhs, ref rhs) => { - let lhs_ty = type_of(env, lhs)?; - let rhs_ty = type_of(env, rhs)?; - - match op { - // T-REL - Binop::Or | Binop::And => { - if lhs_ty != Type::Bool { - Err(TypeError::UnexpectedBinaryLhs(span, lhs_ty)) - } else if rhs_ty != Type::Bool { - Err(TypeError::UnexpectedBinaryRhs(span, rhs_ty)) - } else { - Ok(Type::Bool) - } - } - // T-CMP-... - Binop::Eq | Binop::Ne | Binop::Le | Binop::Lt | Binop::Gt | Binop::Ge => { - // T-CMP-LHS - if is_subtype(&lhs_ty, &rhs_ty) && is_numeric(&rhs_ty) { - Ok(Type::Bool) - // T-CMP-RHS - } else if is_subtype(&rhs_ty, &lhs_ty) && is_numeric(&lhs_ty) { - Ok(Type::Bool) - } else { - Err(TypeError::ExpectedNumericOperands(span, lhs_ty, rhs_ty)) - } - } - // T-ARITH-... - // FIXME: These rules are incompatible with the way we formulated S-SINGLETON-INT - Binop::Add | Binop::Sub | Binop::Mul | Binop::Div => { - // T-ARITH-LHS - if is_subtype(&lhs_ty, &rhs_ty) && is_numeric(&rhs_ty) { - Ok(rhs_ty) - // T-ARITH-RHS - } else if is_subtype(&rhs_ty, &lhs_ty) && is_numeric(&lhs_ty) { - Ok(lhs_ty) - } else { - Err(TypeError::ExpectedNumericOperands(span, lhs_ty, rhs_ty)) - } - } - } - } - } -} - -#[cfg(test)] -pub mod tests { - use ast::Endianness; - use parser; - use source::BytePos as B; - use super::*; - - mod type_of { - use super::*; - - mod add_expr { - use super::*; - - #[test] - fn uint_with_uint() { - let mut env = Env::default(); - let len_ty = Type::UInt(32, Endianness::Target); - env.add_binding("len", len_ty.clone()); - - let expr = parser::parse_expr(&env, "len + len").unwrap(); - assert_eq!(type_of(&env, &expr), Ok(len_ty)); - } - - #[test] - fn unknown_with_uint() { - let mut env = Env::default(); - let len_ty = Type::UInt(32, Endianness::Target); - env.add_binding("len", len_ty.clone()); - - let expr = parser::parse_expr(&env, "1 + len").unwrap(); - assert_eq!(type_of(&env, &expr), Ok(len_ty.clone())); - } - - #[test] - fn uint_with_unknown() { - let mut env = Env::default(); - let len_ty = Type::UInt(32, Endianness::Target); - env.add_binding("len", len_ty.clone()); - - let expr = parser::parse_expr(&env, "len + 1").unwrap(); - assert_eq!(type_of(&env, &expr), Ok(len_ty.clone())); - } - - #[test] - fn unknown_with_unknown() { - let env = Env::default(); - let expr = parser::parse_expr(&env, "1 + 1").unwrap(); - - assert_eq!(type_of(&env, &expr), Ok(Type::RangedInt(1, 1))); - } - } - - mod mul_expr { - use super::*; - - #[test] - fn uint_with_uint() { - let mut env = Env::default(); - let len_ty = Type::UInt(32, Endianness::Target); - env.add_binding("len", len_ty.clone()); - - let expr = parser::parse_expr(&env, "len * len").unwrap(); - assert_eq!(type_of(&env, &expr), Ok(len_ty)); - } - - #[test] - fn unknown_with_uint() { - let mut env = Env::default(); - let len_ty = Type::UInt(32, Endianness::Target); - env.add_binding("len", len_ty.clone()); - - let expr = parser::parse_expr(&env, "1 * len").unwrap(); - assert_eq!(type_of(&env, &expr), Ok(len_ty.clone())); - } - - #[test] - fn uint_with_unknown() { - let mut env = Env::default(); - let len_ty = Type::UInt(32, Endianness::Target); - env.add_binding("len", len_ty.clone()); - - let expr = parser::parse_expr(&env, "len * 1").unwrap(); - assert_eq!(type_of(&env, &expr), Ok(len_ty.clone())); - } - - #[test] - fn unknown_with_unknown() { - let env = Env::default(); - let expr = parser::parse_expr(&env, "1 * 1").unwrap(); - - assert_eq!(type_of(&env, &expr), Ok(Type::RangedInt(1, 1))); - } - } - } - - mod kind_of { - use super::*; - - mod const_ty { - use super::*; - - #[test] - fn ty_const() { - let env = Env::default(); - let ty = Type::SInt(16, Endianness::Target); - - assert_eq!(kind_of(&env, &ty), Ok(Kind::Binary)); - } - } - - mod var_ty { - use super::*; - - #[test] - fn defined() { - let env = Env::default(); - let ty = parser::parse_ty(&env, "u8").unwrap(); - - assert_eq!(kind_of(&env, &ty), Ok(Kind::Binary)); - } - - #[test] - fn undefined() { - let env = Env::default(); - let ty = parser::parse_ty(&env, "Foo").unwrap(); - - assert_eq!( - kind_of(&env, &ty), - Err(KindError::UnboundType( - Span::new(B(0), B(3)), - "Foo".to_owned(), - )) - ); - } - } - - mod union_ty { - use super::*; - - #[test] - fn simple() { - let env = Env::default(); - let ty = parser::parse_ty(&env, "union { u8, u16, i32 }").unwrap(); - - assert_eq!(kind_of(&env, &ty), Ok(Kind::Binary)); - } - - #[test] - fn undefined_element() { - let env = Env::default(); - let ty = parser::parse_ty(&env, "union { u8, Foo, i32 }").unwrap(); - - assert_eq!( - kind_of(&env, &ty), - Err(KindError::UnboundType( - Span::new(B(12), B(15)), - "Foo".to_owned(), - )) - ); - } - } - - mod struct_ty { - use super::*; - - #[test] - fn simple() { - let env = Env::default(); - let ty = parser::parse_ty(&env, "struct { x: u8, y: u8 }").unwrap(); - - assert_eq!(kind_of(&env, &ty), Ok(Kind::Binary)); - } - - #[test] - fn dependent() { - let env = Env::default(); - let ty = parser::parse_ty(&env, "struct { len: u8, data: [u8; len] }").unwrap(); - - assert_eq!(kind_of(&env, &ty), Ok(Kind::Binary)); - } - } - - mod array_ty { - use super::*; - - #[test] - fn constant_size() { - let env = Env::default(); - let ty = parser::parse_ty(&env, "[u8; 16]").unwrap(); - - assert_eq!(kind_of(&env, &ty), Ok(Kind::Binary)); - } - - #[test] - fn constant_variable_size() { - let mut env = Env::default(); - let len_ty = Type::UInt(32, Endianness::Target); - env.add_binding("len", len_ty); - let ty = parser::parse_ty(&env, "[u8; len]").unwrap(); - - assert_eq!(kind_of(&env, &ty), Ok(Kind::Binary)); - } - - #[test] - fn signed_int_size() { - let mut env = Env::default(); - let len_ty = parser::parse_ty(&env, "i8").unwrap(); - env.add_binding("len", len_ty.clone()); - let ty = parser::parse_ty(&env, "[u8; len]").unwrap(); - - assert_eq!( - kind_of(&env, &ty), - Err(KindError::ArraySizeExpectedUInt( - Span::new(B(0), B(9)), - len_ty, - )) - ); - } - - #[test] - fn struct_size() { - let mut env = Env::default(); - let len_ty = parser::parse_ty(&env, "struct {}").unwrap(); - env.add_binding("len", len_ty.clone()); - let ty = parser::parse_ty(&env, "[u8; len]").unwrap(); - - assert_eq!( - kind_of(&env, &ty), - Err(KindError::ArraySizeExpectedUInt( - Span::new(B(0), B(9)), - len_ty, - )) - ); - } - } - } -} diff --git a/src/check/mod.rs b/src/check/mod.rs new file mode 100644 index 000000000..1e412bb47 --- /dev/null +++ b/src/check/mod.rs @@ -0,0 +1,408 @@ +//! Type and kind-checking for our DDL + +use syntax::{binary, host}; +use syntax::{Binding, Ctx, Definition, Name, Named, Var}; + +#[cfg(test)] +mod tests; + +// Typing + +/// An error that was encountered during type checking +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum TypeError { + /// A variable of the requested name was not bound in this scope + UnboundVariable { expr: host::Expr, name: N }, + /// Variable bound in the context was not at the value level + ExprBindingExpected { + expr: host::Expr, + found: Named>, + }, + /// One type was expected, but another was found + Mismatch { + expr: host::Expr, + found: host::Type, + expected: host::Type, + }, + /// Unexpected operand types in a binary operator expression + BinopOperands { + expr: host::Expr, + lhs_ty: host::Type, + rhs_ty: host::Type, + }, + /// A field was missing when projecting on a record + MissingField { + struct_expr: host::Expr, + struct_ty: host::Type, + field_name: N, + }, +} + +/// Returns the type of a host expression, checking that it is properly formed +/// in the environment +pub fn ty_of(ctx: &Ctx, expr: &host::Expr) -> Result, TypeError> { + use syntax::host::{Binop, Const, Expr, Type, TypeConst, Unop}; + + match *expr { + // Constants are easy! + Expr::Const(Const::Bit(_)) => Ok(Type::bit()), + Expr::Const(Const::Bool(_)) => Ok(Type::bool()), + Expr::Const(Const::Int(_)) => Ok(Type::int()), + + // Variables + Expr::Var(Var::Free(ref x)) => Err(TypeError::UnboundVariable { + expr: expr.clone(), + name: x.clone(), + }), + Expr::Var(Var::Bound(Named(_, i))) => match ctx.lookup_ty(i) { + Ok(Named(_, ty)) => Ok(ty.clone()), + Err(Named(name, binding)) => Err(TypeError::ExprBindingExpected { + expr: expr.clone(), + found: Named(name.clone(), binding.clone()), + }), + }, + + // Primitive expressions + Expr::Prim(_, ref repr_ty) => Ok((**repr_ty).clone()), + + // Unary operators + Expr::Unop(op, ref expr) => match op { + Unop::Neg => match ty_of(ctx, &**expr)? { + Type::Const(TypeConst::Int) => Ok(Type::int()), + expr_ty => Err(TypeError::Mismatch { + expr: (**expr).clone(), + found: expr_ty, + expected: Type::int(), + }), + }, + Unop::Not => match ty_of(ctx, &**expr)? { + Type::Const(TypeConst::Bool) => Ok(Type::bool()), + expr_ty => Err(TypeError::Mismatch { + expr: (**expr).clone(), + found: expr_ty, + expected: Type::bool(), + }), + }, + }, + + // Binary operators + Expr::Binop(op, ref lhs_expr, ref rhs_expr) => { + let lhs_ty = ty_of(ctx, &**lhs_expr)?; + let rhs_ty = ty_of(ctx, &**rhs_expr)?; + + match op { + // Relational operators + Binop::Or | Binop::And => match (lhs_ty, rhs_ty) { + (Type::Const(TypeConst::Bool), Type::Const(TypeConst::Bool)) => { + Ok(Type::bool()) + } + (lhs_ty, rhs_ty) => Err(TypeError::BinopOperands { + expr: expr.clone(), + lhs_ty, + rhs_ty, + }), + }, + + // Comparison operators + Binop::Eq | Binop::Ne | Binop::Le | Binop::Lt | Binop::Gt | Binop::Ge => match ( + lhs_ty, + rhs_ty, + ) { + (Type::Const(TypeConst::Bit), Type::Const(TypeConst::Bit)) | + (Type::Const(TypeConst::Bool), Type::Const(TypeConst::Bool)) | + (Type::Const(TypeConst::Int), Type::Const(TypeConst::Int)) => Ok(Type::bool()), + (lhs_ty, rhs_ty) => Err(TypeError::BinopOperands { + expr: expr.clone(), + lhs_ty, + rhs_ty, + }), + }, + + // Arithmetic operators + Binop::Add | Binop::Sub | Binop::Mul | Binop::Div => match (lhs_ty, rhs_ty) { + (Type::Const(TypeConst::Int), Type::Const(TypeConst::Int)) => Ok(Type::int()), + (lhs_ty, rhs_ty) => Err(TypeError::BinopOperands { + expr: expr.clone(), + lhs_ty, + rhs_ty, + }), + }, + } + } + + // Field projection + Expr::Proj(ref struct_expr, ref field_name) => { + let struct_ty = ty_of(ctx, &**struct_expr)?; + + match struct_ty.lookup_field(field_name).cloned() { + Some(field_ty) => Ok(field_ty), + None => Err(TypeError::MissingField { + struct_expr: (**struct_expr).clone(), + struct_ty: struct_ty.clone(), + field_name: field_name.clone(), + }), + } + } + + // Abstraction + Expr::Abs(Named(ref param_name, ref param_ty), ref body_expr) => { + // FIXME: avoid cloning the environment + let mut ctx = ctx.clone(); + ctx.extend(param_name.clone(), Binding::Expr((**param_ty).clone())); + Ok(Type::arrow( + (**param_ty).clone(), + ty_of(&ctx, &**body_expr)?, + )) + } + } +} + +// Kinding + +pub fn simplify_ty(ctx: &Ctx, ty: &binary::Type) -> binary::Type { + use syntax::binary::Type; + + fn compute_ty(ctx: &Ctx, ty: &binary::Type) -> Option> { + match *ty { + Type::Var(Var::Bound(Named(_, i))) => match ctx.lookup_ty_def(i) { + Ok(Named(_, def_ty)) => Some(def_ty.clone()), + Err(_) => None, + }, + Type::App(ref fn_ty, ref arg_ty) => match **fn_ty { + Type::Abs(_, ref body_ty) => { + // FIXME: Avoid clone + let mut body = (**body_ty).clone(); + body.instantiate(arg_ty); + Some(body) + } + _ => None, + }, + _ => None, + } + } + + let ty = match *ty { + Type::App(ref fn_ty, _) => simplify_ty(ctx, &**fn_ty), + // FIXME: Avoid clone + _ => ty.clone(), + }; + + match compute_ty(ctx, &ty) { + Some(ty) => simplify_ty(ctx, &ty), + None => ty, + } +} + +/// An error that was encountered during kind checking +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum KindError { + /// A variable of the requested name was not bound in this scope + UnboundVariable { ty: binary::Type, name: N }, + /// Variable bound in the context was not at the type level + TypeBindingExpected { + ty: binary::Type, + found: Named>, + }, + /// One kind was expected, but another was found + Mismatch { + ty: binary::Type, + expected: binary::Kind, + found: binary::Kind, + }, + /// No host representation was found for this type + NoReprForType { ty: binary::Type }, + /// A type error + Type(TypeError), +} + +impl From> for KindError { + fn from(src: TypeError) -> KindError { + KindError::Type(src) + } +} + +/// Returns the kind of a binary type, checking that it is properly formed in +/// the environment +pub fn kind_of(ctx: &Ctx, ty: &binary::Type) -> Result> { + use syntax::binary::{Kind, Type, TypeConst}; + + match *ty { + // Variables + Type::Var(Var::Free(ref x)) => Err(KindError::UnboundVariable { + ty: ty.clone(), + name: x.clone(), + }), + Type::Var(Var::Bound(Named(_, i))) => match ctx.lookup_kind(i) { + Ok(Named(_, kind)) => Ok(kind.clone()), + Err(Named(name, binding)) => Err(KindError::TypeBindingExpected { + ty: ty.clone(), + found: Named(name.clone(), binding.clone()), + }), + }, + + // Bit type + Type::Const(TypeConst::Bit) => Ok(Kind::Type), + + // Array types + Type::Array(ref elem_ty, ref size_expr) => { + expect_ty_kind(ctx, &**elem_ty)?; + expect_ty(ctx, &**size_expr, host::Type::int())?; + + Ok(Kind::Type) + } + + // Conditional types + Type::Cond(ref ty, ref pred_expr) => { + expect_ty_kind(ctx, &**ty)?; + expect_ty( + ctx, + &**pred_expr, + host::Type::arrow(ty.repr().unwrap(), host::Type::bool()), + )?; + + Ok(Kind::Type) + } + + // Interpreted types + Type::Interp(ref ty, ref conv_expr, ref host_ty) => { + expect_ty_kind(ctx, &**ty)?; + expect_ty( + ctx, + &**conv_expr, + host::Type::arrow(ty.repr().unwrap(), host_ty.clone()), + )?; + + Ok(Kind::Type) + } + + // Type abstraction + Type::Abs(Named(ref name, ref param_kind), ref body_ty) => { + // FIXME: avoid cloning the environment + let mut ctx = ctx.clone(); + ctx.extend(name.clone(), Binding::Type(param_kind.clone())); + Ok(Kind::arrow(param_kind.clone(), kind_of(&ctx, &**body_ty)?)) + } + + // Union types + Type::Union(ref tys) => { + for ty in tys { + expect_ty_kind(ctx, ty)?; + } + + Ok(Kind::Type) + } + + // Struct type + Type::Struct(ref fields) => { + // FIXME: avoid cloning the environment + let mut ctx = ctx.clone(); + + for field in fields { + expect_ty_kind(&ctx, &field.value)?; + + let field_ty = simplify_ty(&ctx, &field.value); + let repr_ty = field_ty.repr().map_err(|_| { + KindError::NoReprForType { + ty: field_ty.clone(), + } + })?; + ctx.extend(field.name.clone(), Binding::Expr(repr_ty)); + } + + Ok(Kind::Type) + } + + // Type application + Type::App(ref fn_ty, ref arg_ty) => { + match kind_of(ctx, &**fn_ty)? { + Kind::Type => Err(KindError::Mismatch { + ty: (**fn_ty).clone(), + found: Kind::Type, + // FIXME: Kind of args are unknown at this point - therefore + // they shouldn't be `Kind::Type`! + expected: Kind::arrow(Kind::Type, Kind::Type), + }), + Kind::Arrow(param_kind, ret_kind) => { + expect_kind(ctx, &**arg_ty, *param_kind)?; + Ok(*ret_kind) + } + } + } + } +} + +pub fn check_defs<'a, N: 'a + Name, Defs>(defs: Defs) -> Result<(), KindError> +where + Defs: IntoIterator>, +{ + let mut ctx = Ctx::new(); + // We maintain a list of the seen definition names. This will allow us to + // recover the index of these variables as we abstract later definitions... + let mut seen_names = Vec::new(); + + for def in defs { + let mut def_ty = def.ty.clone(); + + // Kind of ugly and inefficient - can't we just substitute directly? + // Should handle mutually recursive bindings as well... + + for (level, name) in seen_names.iter().rev().enumerate() { + def_ty.abstract_name_at(name, level as u32); + } + + for (i, _) in seen_names.iter().enumerate() { + let Named(_, ty) = ctx.lookup_ty_def(i as u32).unwrap(); + def_ty.instantiate(ty); + } + + let def_kind = kind_of(&ctx, &*def_ty)?; + ctx.extend(def.name.clone(), Binding::TypeDef(*def_ty, def_kind)); + + // Record that the definition has been 'seen' + seen_names.push(def.name.clone()); + } + + Ok(()) +} + +// Expectations + +fn expect_ty( + ctx: &Ctx, + expr: &host::Expr, + expected: host::Type, +) -> Result, TypeError> { + let found = ty_of(ctx, expr)?; + + if found == expected { + Ok(found) + } else { + Err(TypeError::Mismatch { + expr: expr.clone(), + expected, + found, + }) + } +} + +fn expect_kind( + ctx: &Ctx, + ty: &binary::Type, + expected: binary::Kind, +) -> Result> { + let found = kind_of(ctx, ty)?; + + if found == expected { + Ok(found) + } else { + Err(KindError::Mismatch { + ty: ty.clone(), + expected, + found, + }) + } +} + +fn expect_ty_kind(ctx: &Ctx, ty: &binary::Type) -> Result<(), KindError> { + expect_kind(ctx, ty, binary::Kind::Type).map(|_| ()) +} diff --git a/src/check/tests.rs b/src/check/tests.rs new file mode 100644 index 000000000..cdfe9adc9 --- /dev/null +++ b/src/check/tests.rs @@ -0,0 +1,106 @@ +use parser; +use super::*; + +mod ty_of { + use super::*; + use self::host::Type; + + #[test] + fn const_int() { + let ctx = Ctx::new(); + let src = "1"; + let expr = parser::parse_expr(src).unwrap(); + + assert_eq!(ty_of(&ctx, &expr), Ok(Type::int())); + } + + #[test] + fn neg_int() { + let ctx = Ctx::new(); + let src = "-(1 + 2)"; + let expr = parser::parse_expr(src).unwrap(); + + assert_eq!(ty_of(&ctx, &expr), Ok(Type::int())); + } + + #[test] + fn neg_bool() { + let ctx = Ctx::new(); + let src = "-(1 == 2)"; + let expr = parser::parse_expr(src).unwrap(); + + assert!(ty_of(&ctx, &expr).is_err()); + } + + #[test] + fn not_int() { + let ctx = Ctx::new(); + let src = "!(1 + 2)"; + let expr = parser::parse_expr(src).unwrap(); + + assert!(ty_of(&ctx, &expr).is_err()); + } + + #[test] + fn not_bool() { + let ctx = Ctx::new(); + let src = "!(1 == 2)"; + let expr = parser::parse_expr(src).unwrap(); + + assert_eq!(ty_of(&ctx, &expr), Ok(Type::bool())); + } + + #[test] + fn arith_ops() { + let ctx = Ctx::new(); + let src = "1 + (1 * -2)"; + let expr = parser::parse_expr(src).unwrap(); + + assert_eq!(ty_of(&ctx, &expr), Ok(Type::int())); + } + + #[test] + fn cmp_ops_eq_int() { + let ctx = Ctx::new(); + let src = "1 + (1 * 2) == 3"; + let expr = parser::parse_expr(src).unwrap(); + + assert_eq!(ty_of(&ctx, &expr), Ok(Type::bool())); + } + + #[test] + fn cmp_ops_ne_int() { + let ctx = Ctx::new(); + let src = "1 + (1 * 2) != 3"; + let expr = parser::parse_expr(src).unwrap(); + + assert_eq!(ty_of(&ctx, &expr), Ok(Type::bool())); + } + + #[test] + fn cmp_ops_eq_bool() { + let ctx = Ctx::new(); + let src = "(1 == 1) == (3 == 3)"; + let expr = parser::parse_expr(src).unwrap(); + + assert_eq!(ty_of(&ctx, &expr), Ok(Type::bool())); + } + + #[test] + fn cmp_ops_ne_bool() { + let ctx = Ctx::new(); + let src = "(1 == 1) != (3 == 3)"; + let expr = parser::parse_expr(src).unwrap(); + + assert_eq!(ty_of(&ctx, &expr), Ok(Type::bool())); + } + + #[test] + fn rel_ops() { + let ctx = Ctx::new(); + let src = "(1 == 3) & (2 == 2) | (1 == 2)"; + let expr = parser::parse_expr(src).unwrap(); + + assert_eq!(ty_of(&ctx, &expr), Ok(Type::bool())); + } +} diff --git a/src/compilers/mod.rs b/src/compilers/mod.rs index 3a6986436..c0b4420db 100644 --- a/src/compilers/mod.rs +++ b/src/compilers/mod.rs @@ -1,2 +1,2 @@ pub mod dot; -pub mod rust; +// pub mod rust; diff --git a/src/compilers/rust.rs b/src/compilers/rust.rs index e1cb0463f..fc6a9f517 100644 --- a/src/compilers/rust.rs +++ b/src/compilers/rust.rs @@ -4,7 +4,7 @@ use std::collections::{HashSet, VecDeque}; use std::io::Write; use Env; -use ast::{Endianness, Field, Type}; +use syntax::{Endianness, Field, Type}; /// Compile the symbols in the environment to a Rust parser #[allow(unused_variables)] @@ -22,7 +22,10 @@ enum NameHint { } enum CompileJob { - Struct { name: String, fields: Vec }, + Struct { + name: String, + fields: Vec>, + }, Union { name: String, elems: Vec }, } @@ -233,9 +236,9 @@ impl CompilerEnv { Type::Float(4, Endianness::Target) => quote! { f32 }, Type::Float(8, Endianness::Target) => quote! { f64 }, - Type::UInt(_, _) | - Type::SInt(_, _) | - Type::Float(_, _) => unimplemented!("{:?} not yet handled outside of structs", ty), + Type::UInt(_, _) | Type::SInt(_, _) | Type::Float(_, _) => { + unimplemented!("{:?} not yet handled outside of structs", ty) + } Type::RangedInt(_, _) => { // Sould never happen! diff --git a/src/env.rs b/src/env.rs deleted file mode 100644 index 6252b3ba3..000000000 --- a/src/env.rs +++ /dev/null @@ -1,113 +0,0 @@ -use std::collections::HashMap; -use std::collections::hash_map::Iter; - -use ast::{Endianness, Type}; - -/// An environment of bindings and types -/// -/// ```plain -/// Γ ::= -/// · empty environment -/// Γ, x:σ environment extension -/// ``` -#[derive(Debug)] -pub struct Env<'parent> { - parent: Option<&'parent Env<'parent>>, - tys: HashMap, - bindings: HashMap, -} - -impl<'parent> Env<'parent> { - pub fn new() -> Env<'static> { - Env { - parent: None, - tys: HashMap::new(), - bindings: HashMap::new(), - } - } - - pub fn extend(&self) -> Env { - Env { - parent: Some(self), - tys: HashMap::new(), - bindings: HashMap::new(), - } - } - - pub fn add_ty(&mut self, name: S, ty: Type) - where - S: Into, - { - self.tys.insert(name.into(), ty); - } - - pub fn add_binding(&mut self, name: S, ty: Type) - where - S: Into, - { - self.bindings.insert(name.into(), ty); - } - - pub fn lookup_ty(&self, name: &str) -> Option<&Type> { - self.tys.get(name).or_else(|| { - self.parent.and_then(|env| env.lookup_ty(name)) - }) - } - - pub fn lookup_binding(&self, name: &str) -> Option<&Type> { - self.bindings.get(name).or_else(|| { - self.parent.and_then(|env| env.lookup_binding(name)) - }) - } - - pub fn tys(&self) -> Iter { - self.tys.iter() - } -} - -const BUILT_INS: [(&str, Type); 30] = [ - ("u8", Type::UInt(1, Endianness::Target)), - ("u16", Type::UInt(2, Endianness::Target)), - ("u32", Type::UInt(4, Endianness::Target)), - ("u64", Type::UInt(8, Endianness::Target)), - ("i8", Type::SInt(1, Endianness::Target)), - ("i16", Type::SInt(2, Endianness::Target)), - ("i32", Type::SInt(4, Endianness::Target)), - ("i64", Type::SInt(8, Endianness::Target)), - ("f32", Type::Float(4, Endianness::Target)), - ("f64", Type::Float(8, Endianness::Target)), - - ("u8le", Type::UInt(1, Endianness::Little)), - ("u16le", Type::UInt(2, Endianness::Little)), - ("u32le", Type::UInt(4, Endianness::Little)), - ("u64le", Type::UInt(8, Endianness::Little)), - ("i8le", Type::SInt(1, Endianness::Little)), - ("i16le", Type::SInt(2, Endianness::Little)), - ("i32le", Type::SInt(4, Endianness::Little)), - ("i64le", Type::SInt(8, Endianness::Little)), - ("f32le", Type::Float(4, Endianness::Little)), - ("f64le", Type::Float(8, Endianness::Little)), - - ("u8be", Type::UInt(1, Endianness::Big)), - ("u16be", Type::UInt(2, Endianness::Big)), - ("u32be", Type::UInt(4, Endianness::Big)), - ("u64be", Type::UInt(8, Endianness::Big)), - ("i8be", Type::SInt(1, Endianness::Big)), - ("i16be", Type::SInt(2, Endianness::Big)), - ("i32be", Type::SInt(4, Endianness::Big)), - ("i64be", Type::SInt(8, Endianness::Big)), - ("f32be", Type::Float(4, Endianness::Big)), - ("f64be", Type::Float(8, Endianness::Big)), -]; - -impl Default for Env<'static> { - fn default() -> Env<'static> { - let mut env = Env::new(); - - for &(ident, ref ty) in &BUILT_INS { - env.add_ty(ident, ty.clone()); - } - - env - } -} diff --git a/src/lib.rs b/src/lib.rs index a2dbf64fe..06454b7c1 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -1,23 +1,20 @@ #[cfg(test)] extern crate difference; -extern crate inflector; +// extern crate inflector; extern crate lalrpop_util; #[cfg(test)] #[macro_use] extern crate pretty_assertions; -#[macro_use] -extern crate quote; +// #[macro_use] +// extern crate quote; extern crate unicode_xid; #[cfg(test)] #[macro_use] mod test; -pub mod ast; -pub mod compilers; +pub mod syntax; +// pub mod compilers; pub mod check; -mod env; pub mod parser; pub mod source; - -pub use env::Env; diff --git a/src/parser/grammar.lalrpop b/src/parser/grammar.lalrpop index cac3bc70f..ec4ff0a99 100644 --- a/src/parser/grammar.lalrpop +++ b/src/parser/grammar.lalrpop @@ -1,9 +1,14 @@ -use ast::{Binop, Definition, Field, Expr, Type, Unop}; -use env::Env; +use syntax::{Definition, Field}; +use syntax::binary::Type; +use syntax::host::{Binop, Expr, Unop}; use parser::lexer::{Token, Error as LexerError}; use source::BytePos; -grammar<'input, 'env>(env: &'env Env); + +grammar<'input>(); + + +// Tokens extern { type Location = BytePos; @@ -51,133 +56,143 @@ extern { } } -pub Definitions: Vec = { + +pub Definitions: Vec> = { Definition*, }; -Definition: Definition = { - "=" ";" => { - Definition::new((lo, hi), name, ty) +Definition: Definition = { + "=" ";" => { + Definition::new(name, ty) + }, +}; + +Field: Field> = { + ":" => { + Field::new(name, ty) + }, +}; + + +// Types + +pub Type: Type = { + => ty, +}; + +PrimaryType: Type = { + AtomicType, + "where" "=>" => { + // FIXME: unwrap + let repr_ty = Box::new(ty.repr().unwrap()); + Type::cond(ty, Expr::abs((param, repr_ty), pred)) }, }; -AtomicType: Type = { - => { - match env.lookup_ty(&name) { - Some(ty) => ty.clone(), - None => Type::var((lo, hi), name), - } +AtomicType: Type = { + => { + Type::fvar(name) }, - "(" ")", - "struct" "{" ",")*> "}" => { + "(" ")" => ty, + "struct" "{" ",")*> "}" => { let mut fields = fields; fields.extend(last); - Type::struct_((lo, hi), fields) + Type::struct_(fields) }, - "union" "{" ",")+> "}" => { + "union" "{" ",")+> "}" => { let mut tys = tys; tys.extend(last); - Type::union((lo, hi), tys) + Type::union(tys) }, - "[" ";" "]" => { - Type::array((lo, hi), elem, size) + "[" ";" "]" => { + Type::array(elem, size) }, }; -pub Type: Type = { - AtomicType, - "where" "=>" => { - Type::where_((lo, hi), ty, param, pred) - }, + +// Expressions + +pub Expr: Expr = { + => expr, }; // Use precedence climbing to define the operators // https://en.wikipedia.org/wiki/Operator-precedence_parser#Precedence_climbing_method -pub Expr: Expr = { +PrimaryExpr: Expr = { EqExpr, - "|" => { - Expr::binop((lo, hi), Binop::Or, lhs, rhs) + "|" => { + Expr::binop(Binop::Or, lhs, rhs) }, - "&" => { - Expr::binop((lo, hi), Binop::And, lhs, rhs) + "&" => { + Expr::binop(Binop::And, lhs, rhs) }, }; -EqExpr: Expr = { +EqExpr: Expr = { CmpExpr, - "==" => { - Expr::binop((lo, hi), Binop::Eq, lhs, rhs) + "==" => { + Expr::binop(Binop::Eq, lhs, rhs) }, - "!=" => { - Expr::binop((lo, hi), Binop::Ne, lhs, rhs) + "!=" => { + Expr::binop(Binop::Ne, lhs, rhs) }, }; -CmpExpr: Expr = { +CmpExpr: Expr = { AddExpr, - "<=" => { - Expr::binop((lo, hi), Binop::Le, lhs, rhs) + "<=" => { + Expr::binop(Binop::Le, lhs, rhs) }, - "<" => { - Expr::binop((lo, hi), Binop::Lt, lhs, rhs) + "<" => { + Expr::binop(Binop::Lt, lhs, rhs) }, - ">" => { - Expr::binop((lo, hi), Binop::Gt, lhs, rhs) + ">" => { + Expr::binop(Binop::Gt, lhs, rhs) }, - ">=" => { - Expr::binop((lo, hi), Binop::Ge, lhs, rhs) + ">=" => { + Expr::binop(Binop::Ge, lhs, rhs) }, }; -AddExpr : Expr = { +AddExpr: Expr = { MulExpr, - "+" => { - Expr::binop((lo, hi), Binop::Add, lhs, rhs) + "+" => { + Expr::binop(Binop::Add, lhs, rhs) }, - "-" => { - Expr::binop((lo, hi), Binop::Sub, lhs, rhs) + "-" => { + Expr::binop(Binop::Sub, lhs, rhs) }, }; -MulExpr : Expr = { +MulExpr: Expr = { AtomicExpr, - "*" => { - Expr::binop((lo, hi), Binop::Mul, lhs, rhs) + "*" => { + Expr::binop(Binop::Mul, lhs, rhs) }, - "/" => { - Expr::binop((lo, hi), Binop::Div, lhs, rhs) + "/" => { + Expr::binop(Binop::Div, lhs, rhs) }, }; -AtomicExpr : Expr = { - "(" ")" => expr, - => { - Expr::int((lo, hi), value) - }, - => { - Expr::int((lo, hi), value) +AtomicExpr: Expr = { + "(" ")" => expr, + => { + Expr::int(value) }, - => { - Expr::int((lo, hi), value) + => { + Expr::int(value) }, - => { - match name { - "true" => Expr::bool((lo, hi), true), - "false" => Expr::bool((lo, hi), false), - name => Expr::var((lo, hi), name), - } + => { + Expr::int(value) }, - "-" => { - Expr::unop((lo, hi), Unop::Neg, expr) + => { + Expr::fvar(name) }, - "!" => { - Expr::unop((lo, hi), Unop::Not, value) + "-" => { + Expr::unop(Unop::Neg, expr) }, -}; - -Field: Field = { - ":" => { - Field::new((lo, hi), name, ty) + "!" => { + Expr::unop(Unop::Not, value) }, }; diff --git a/src/parser/lexer.rs b/src/parser/lexer.rs index 3fb5c5601..4c04867d6 100644 --- a/src/parser/lexer.rs +++ b/src/parser/lexer.rs @@ -68,30 +68,30 @@ pub enum Token<'input> { Where, // Symbols - Ampersand, // & - Bang, // ! - BangEqual, // != - Colon, // : - Comma, // , - Equal, // = - EqualEqual, // == + Ampersand, // & + Bang, // ! + BangEqual, // != + Colon, // : + Comma, // , + Equal, // = + EqualEqual, // == EqualGreater, // => ForwardSlash, // / - Greater, // > + Greater, // > GreaterEqual, // >= - Less, // < - LessEqual, // <= - Minus, // - - Pipe, // | - Plus, // + - Semi, // ; - Star, // * + Less, // < + LessEqual, // <= + Minus, // - + Pipe, // | + Plus, // + + Semi, // ; + Star, // * // Delimiters - LParen, // ( - RParen, // ) - LBrace, // { - RBrace, // } + LParen, // ( + RParen, // ) + LBrace, // { + RBrace, // } LBracket, // [ RBracket, // ] } diff --git a/src/parser/mod.rs b/src/parser/mod.rs index ddc6380e7..96c26e1ba 100644 --- a/src/parser/mod.rs +++ b/src/parser/mod.rs @@ -1,57 +1,39 @@ use lalrpop_util; -use ast::{Definition, Expr, Type}; -use env::Env; +use syntax::{binary, host, Definition}; use source::BytePos; mod lexer; #[allow(unused_extern_crates)] mod grammar; -use self::lexer::{Lexer, Error as LexerError, Token}; +use self::lexer::{Error as LexerError, Lexer, Token}; pub type ParseError<'input> = lalrpop_util::ParseError, LexerError>; -// pub enum ParseError { -// InvalidToken { -// location: L, -// }, -// UnrecognizedToken { -// token: Option<(L, T, L)>, -// expected: Vec, -// }, -// ExtraToken { -// token: (L, T, L), -// }, -// User { -// error: E, -// }, -// } - -pub fn parse<'input, 'env>( - env: &'env Env, +pub fn parse<'input>( src: &'input str, -) -> Result, ParseError<'input>> { - grammar::parse_Definitions(env, Lexer::new(src)) +) -> Result< + Vec>, + ParseError<'input>, +> { + grammar::parse_Definitions(Lexer::new(src)) } -pub fn parse_expr<'input, 'env>( - env: &'env Env, +pub fn parse_expr<'input>( src: &'input str, -) -> Result> { - grammar::parse_Expr(env, Lexer::new(src)) +) -> Result, ParseError<'input>> { + grammar::parse_Expr(Lexer::new(src)) } -pub fn parse_ty<'input, 'env>( - env: &'env Env, +pub fn parse_ty<'input>( src: &'input str, -) -> Result> { - grammar::parse_Type(env, Lexer::new(src)) +) -> Result, ParseError<'input>> { + grammar::parse_Type(Lexer::new(src)) } #[cfg(test)] mod tests { - use env::Env; use super::*; #[test] @@ -60,10 +42,7 @@ mod tests { !((true | (false))) "; - assert_snapshot!( - parse_expr_bool_atomic, - parse_expr(&Env::default(), src).unwrap() - ); + assert_snapshot!(parse_expr_bool_atomic, parse_expr(src).unwrap()); } #[test] @@ -72,68 +51,56 @@ mod tests { (true & false) | (true | false) "; - assert_snapshot!( - parse_expr_bool_operators, - parse_expr(&Env::default(), src).unwrap() - ); + assert_snapshot!(parse_expr_bool_operators, parse_expr(src).unwrap()); } #[test] fn parse_add_expr() { let src = "x + y + z"; - assert_snapshot!(parse_add_expr, parse_expr(&Env::default(), src).unwrap()); + assert_snapshot!(parse_add_expr, parse_expr(src).unwrap()); } #[test] fn parse_sub_expr() { let src = "x - y - z"; - assert_snapshot!(parse_sub_expr, parse_expr(&Env::default(), src).unwrap()); + assert_snapshot!(parse_sub_expr, parse_expr(src).unwrap()); } #[test] fn parse_add_expr_mixed() { let src = "x + y + z - z + x"; - assert_snapshot!( - parse_add_expr_mixed, - parse_expr(&Env::default(), src).unwrap() - ); + assert_snapshot!(parse_add_expr_mixed, parse_expr(src).unwrap()); } #[test] fn parse_mul_expr() { let src = "x * y * z"; - assert_snapshot!(parse_mul_expr, parse_expr(&Env::default(), src).unwrap()); + assert_snapshot!(parse_mul_expr, parse_expr(src).unwrap()); } #[test] fn parse_div_expr() { let src = "x / y / z"; - assert_snapshot!(parse_div_expr, parse_expr(&Env::default(), src).unwrap()); + assert_snapshot!(parse_div_expr, parse_expr(src).unwrap()); } #[test] fn parse_mul_expr_mixed() { let src = "x * y * z / z * x"; - assert_snapshot!( - parse_mul_expr_mixed, - parse_expr(&Env::default(), src).unwrap() - ); + assert_snapshot!(parse_mul_expr_mixed, parse_expr(src).unwrap()); } #[test] fn parse_mixed_arithmetic_expr() { let src = "x + y * z / z - x * a"; - assert_snapshot!( - parse_mixed_arithmetic_expr, - parse_expr(&Env::default(), src).unwrap() - ); + assert_snapshot!(parse_mixed_arithmetic_expr, parse_expr(src).unwrap()); } #[test] @@ -142,7 +109,7 @@ mod tests { assert_snapshot!( parse_mixed_arithmetic_expr_parenthesized, - parse_expr(&Env::default(), src).unwrap() + parse_expr(src).unwrap() ); } @@ -152,30 +119,46 @@ mod tests { Point "; - assert_snapshot!(parse_ty_var, parse_ty(&Env::default(), src).unwrap()); + assert_snapshot!(parse_ty_var, parse_ty(src).unwrap()); } #[test] fn parse_ty_empty_struct() { let src = "struct {}"; - assert_snapshot!( - parse_ty_empty_struct, - parse_ty(&Env::default(), src).unwrap() - ); + assert_snapshot!(parse_ty_empty_struct, parse_ty(src).unwrap()); } #[test] fn parse_ty_where() { let src = " struct { - x: u32 where x => true, + x: u32 where x => x == 3, } - where x => true - where x => false + where x => x == 2 + where x => x == 1 "; - assert_snapshot!(parse_ty_where, parse_ty(&Env::default(), src).unwrap()); + assert_snapshot!(parse_ty_where, parse_ty(src).unwrap()); + } + + #[test] + fn parse_ty_array_dependent() { + let src = " + struct { + len: u32, + data1: [f32; len], + data2: struct { + data1: [f32; len], + len: u32, + padding1: u8, + padding2: u8, + data2: [f32; len], + }, + } + "; + + assert_snapshot!(parse_ty_array_dependent, parse_ty(src).unwrap()); } #[test] @@ -184,10 +167,7 @@ mod tests { Offset32 = u32; "; - assert_snapshot!( - parse_simple_definition, - parse(&Env::default(), src).unwrap() - ); + assert_snapshot!(parse_simple_definition, parse(src).unwrap()); } #[test] @@ -196,10 +176,7 @@ mod tests { Point = [f32; 3]; "; - assert_snapshot!( - parse_array_with_constant_size, - parse(&Env::default(), src).unwrap() - ); + assert_snapshot!(parse_array_with_constant_size, parse(src).unwrap()); } #[test] @@ -222,6 +199,6 @@ mod tests { }; "; - assert_snapshot!(parse_definition, parse(&Env::default(), src).unwrap()); + assert_snapshot!(parse_definition, parse(src).unwrap()); } } diff --git a/src/parser/snapshots/mod.parse_add_expr.snap b/src/parser/snapshots/mod.parse_add_expr.snap index d5bc8696b..dcae63d44 100644 --- a/src/parser/snapshots/mod.parse_add_expr.snap +++ b/src/parser/snapshots/mod.parse_add_expr.snap @@ -1,35 +1,15 @@ Binop( - Span { - lo: BytePos(0), - hi: BytePos(9) - }, Add, Var( - Span { - lo: BytePos(0), - hi: BytePos(1) - }, - "x" + Free("x") ), Binop( - Span { - lo: BytePos(4), - hi: BytePos(9) - }, Add, Var( - Span { - lo: BytePos(4), - hi: BytePos(5) - }, - "y" + Free("y") ), Var( - Span { - lo: BytePos(8), - hi: BytePos(9) - }, - "z" + Free("z") ) ) ) diff --git a/src/parser/snapshots/mod.parse_add_expr_mixed.snap b/src/parser/snapshots/mod.parse_add_expr_mixed.snap index 5fa6a738d..149c7895a 100644 --- a/src/parser/snapshots/mod.parse_add_expr_mixed.snap +++ b/src/parser/snapshots/mod.parse_add_expr_mixed.snap @@ -1,61 +1,25 @@ Binop( - Span { - lo: BytePos(0), - hi: BytePos(17) - }, Add, Var( - Span { - lo: BytePos(0), - hi: BytePos(1) - }, - "x" + Free("x") ), Binop( - Span { - lo: BytePos(4), - hi: BytePos(17) - }, Add, Var( - Span { - lo: BytePos(4), - hi: BytePos(5) - }, - "y" + Free("y") ), Binop( - Span { - lo: BytePos(8), - hi: BytePos(17) - }, Sub, Var( - Span { - lo: BytePos(8), - hi: BytePos(9) - }, - "z" + Free("z") ), Binop( - Span { - lo: BytePos(12), - hi: BytePos(17) - }, Add, Var( - Span { - lo: BytePos(12), - hi: BytePos(13) - }, - "z" + Free("z") ), Var( - Span { - lo: BytePos(16), - hi: BytePos(17) - }, - "x" + Free("x") ) ) ) diff --git a/src/parser/snapshots/mod.parse_array_with_constant_size.snap b/src/parser/snapshots/mod.parse_array_with_constant_size.snap index bc13c7a6c..9b2656a9a 100644 --- a/src/parser/snapshots/mod.parse_array_with_constant_size.snap +++ b/src/parser/snapshots/mod.parse_array_with_constant_size.snap @@ -1,24 +1,11 @@ [ Definition { - span: Span { - lo: BytePos(13), - hi: BytePos(30) - }, name: "Point", ty: Array( - Span { - lo: BytePos(21), - hi: BytePos(29) - }, - Float( - 4, - Target + Var( + Free("f32") ), Const( - Span { - lo: BytePos(27), - hi: BytePos(28) - }, Int(3) ) ) diff --git a/src/parser/snapshots/mod.parse_definition.snap b/src/parser/snapshots/mod.parse_definition.snap index e44c42162..44baf81b4 100644 --- a/src/parser/snapshots/mod.parse_definition.snap +++ b/src/parser/snapshots/mod.parse_definition.snap @@ -1,88 +1,41 @@ [ Definition { - span: Span { - lo: BytePos(13), - hi: BytePos(98) - }, name: "Point", ty: Struct( - Span { - lo: BytePos(21), - hi: BytePos(97) - }, [ Field { - span: Span { - lo: BytePos(46), - hi: BytePos(55) - }, name: "x", - ty: UInt( - 4, - Big + value: Var( + Free("u32be") ) }, Field { - span: Span { - lo: BytePos(73), - hi: BytePos(82) - }, name: "y", - ty: UInt( - 4, - Big + value: Var( + Free("u32be") ) } ] ) }, Definition { - span: Span { - lo: BytePos(112), - hi: BytePos(209) - }, name: "Array", ty: Struct( - Span { - lo: BytePos(120), - hi: BytePos(208) - }, [ Field { - span: Span { - lo: BytePos(145), - hi: BytePos(156) - }, name: "len", - ty: UInt( - 2, - Little + value: Var( + Free("u16le") ) }, Field { - span: Span { - lo: BytePos(174), - hi: BytePos(193) - }, name: "data", - ty: Array( - Span { - lo: BytePos(181), - hi: BytePos(193) - }, + value: Array( Var( - Span { - lo: BytePos(182), - hi: BytePos(187) - }, - "Point" + Free("Point") ), Var( - Span { - lo: BytePos(189), - hi: BytePos(192) - }, - "len" + Bound(Named("len", 0)) ) ) } @@ -90,109 +43,53 @@ ) }, Definition { - span: Span { - lo: BytePos(223), - hi: BytePos(417) - }, name: "Formats", ty: Union( - Span { - lo: BytePos(233), - hi: BytePos(416) - }, [ Struct( - Span { - lo: BytePos(257), - hi: BytePos(291) - }, [ Field { - span: Span { - lo: BytePos(266), - hi: BytePos(278) - }, name: "format", - ty: UInt( - 2, - Target + value: Var( + Free("u16") ) }, Field { - span: Span { - lo: BytePos(280), - hi: BytePos(289) - }, name: "data", - ty: UInt( - 2, - Target + value: Var( + Free("u16") ) } ] ), Struct( - Span { - lo: BytePos(309), - hi: BytePos(346) - }, [ Field { - span: Span { - lo: BytePos(318), - hi: BytePos(330) - }, name: "format", - ty: UInt( - 2, - Target + value: Var( + Free("u16") ) }, Field { - span: Span { - lo: BytePos(332), - hi: BytePos(344) - }, name: "point", - ty: Var( - Span { - lo: BytePos(339), - hi: BytePos(344) - }, - "Point" + value: Var( + Free("Point") ) } ] ), Struct( - Span { - lo: BytePos(364), - hi: BytePos(401) - }, [ Field { - span: Span { - lo: BytePos(373), - hi: BytePos(385) - }, name: "format", - ty: UInt( - 2, - Target + value: Var( + Free("u16") ) }, Field { - span: Span { - lo: BytePos(387), - hi: BytePos(399) - }, name: "array", - ty: Var( - Span { - lo: BytePos(394), - hi: BytePos(399) - }, - "Array" + value: Var( + Free("Array") ) } ] diff --git a/src/parser/snapshots/mod.parse_div_expr.snap b/src/parser/snapshots/mod.parse_div_expr.snap index 2e355e6af..1e2f64056 100644 --- a/src/parser/snapshots/mod.parse_div_expr.snap +++ b/src/parser/snapshots/mod.parse_div_expr.snap @@ -1,35 +1,15 @@ Binop( - Span { - lo: BytePos(0), - hi: BytePos(9) - }, Div, Var( - Span { - lo: BytePos(0), - hi: BytePos(1) - }, - "x" + Free("x") ), Binop( - Span { - lo: BytePos(4), - hi: BytePos(9) - }, Div, Var( - Span { - lo: BytePos(4), - hi: BytePos(5) - }, - "y" + Free("y") ), Var( - Span { - lo: BytePos(8), - hi: BytePos(9) - }, - "z" + Free("z") ) ) ) diff --git a/src/parser/snapshots/mod.parse_expr_bool_atomic.snap b/src/parser/snapshots/mod.parse_expr_bool_atomic.snap index 844833f8e..55207e74d 100644 --- a/src/parser/snapshots/mod.parse_expr_bool_atomic.snap +++ b/src/parser/snapshots/mod.parse_expr_bool_atomic.snap @@ -1,28 +1,12 @@ Unop( - Span { - lo: BytePos(13), - hi: BytePos(32) - }, Not, Binop( - Span { - lo: BytePos(16), - hi: BytePos(30) - }, Or, - Const( - Span { - lo: BytePos(16), - hi: BytePos(20) - }, - Bool(true) + Var( + Free("true") ), - Const( - Span { - lo: BytePos(24), - hi: BytePos(29) - }, - Bool(false) + Var( + Free("false") ) ) ) diff --git a/src/parser/snapshots/mod.parse_expr_bool_operators.snap b/src/parser/snapshots/mod.parse_expr_bool_operators.snap index 0593b91f3..8a960098f 100644 --- a/src/parser/snapshots/mod.parse_expr_bool_operators.snap +++ b/src/parser/snapshots/mod.parse_expr_bool_operators.snap @@ -1,49 +1,21 @@ Binop( - Span { - lo: BytePos(13), - hi: BytePos(44) - }, Or, Binop( - Span { - lo: BytePos(14), - hi: BytePos(26) - }, And, - Const( - Span { - lo: BytePos(14), - hi: BytePos(18) - }, - Bool(true) + Var( + Free("true") ), - Const( - Span { - lo: BytePos(21), - hi: BytePos(26) - }, - Bool(false) + Var( + Free("false") ) ), Binop( - Span { - lo: BytePos(31), - hi: BytePos(43) - }, Or, - Const( - Span { - lo: BytePos(31), - hi: BytePos(35) - }, - Bool(true) + Var( + Free("true") ), - Const( - Span { - lo: BytePos(38), - hi: BytePos(43) - }, - Bool(false) + Var( + Free("false") ) ) ) diff --git a/src/parser/snapshots/mod.parse_mixed_arithmetic_expr.snap b/src/parser/snapshots/mod.parse_mixed_arithmetic_expr.snap index b7b6af40d..5294618be 100644 --- a/src/parser/snapshots/mod.parse_mixed_arithmetic_expr.snap +++ b/src/parser/snapshots/mod.parse_mixed_arithmetic_expr.snap @@ -1,76 +1,32 @@ Binop( - Span { - lo: BytePos(0), - hi: BytePos(21) - }, Add, Var( - Span { - lo: BytePos(0), - hi: BytePos(1) - }, - "x" + Free("x") ), Binop( - Span { - lo: BytePos(4), - hi: BytePos(21) - }, Sub, Binop( - Span { - lo: BytePos(4), - hi: BytePos(13) - }, Mul, Var( - Span { - lo: BytePos(4), - hi: BytePos(5) - }, - "y" + Free("y") ), Binop( - Span { - lo: BytePos(8), - hi: BytePos(13) - }, Div, Var( - Span { - lo: BytePos(8), - hi: BytePos(9) - }, - "z" + Free("z") ), Var( - Span { - lo: BytePos(12), - hi: BytePos(13) - }, - "z" + Free("z") ) ) ), Binop( - Span { - lo: BytePos(16), - hi: BytePos(21) - }, Mul, Var( - Span { - lo: BytePos(16), - hi: BytePos(17) - }, - "x" + Free("x") ), Var( - Span { - lo: BytePos(20), - hi: BytePos(21) - }, - "a" + Free("a") ) ) ) diff --git a/src/parser/snapshots/mod.parse_mixed_arithmetic_expr_parenthesized.snap b/src/parser/snapshots/mod.parse_mixed_arithmetic_expr_parenthesized.snap index 30b2b0337..49f8dd2aa 100644 --- a/src/parser/snapshots/mod.parse_mixed_arithmetic_expr_parenthesized.snap +++ b/src/parser/snapshots/mod.parse_mixed_arithmetic_expr_parenthesized.snap @@ -1,76 +1,32 @@ Binop( - Span { - lo: BytePos(0), - hi: BytePos(25) - }, Mul, Binop( - Span { - lo: BytePos(1), - hi: BytePos(6) - }, Add, Var( - Span { - lo: BytePos(1), - hi: BytePos(2) - }, - "x" + Free("x") ), Var( - Span { - lo: BytePos(5), - hi: BytePos(6) - }, - "y" + Free("y") ) ), Binop( - Span { - lo: BytePos(10), - hi: BytePos(25) - }, Div, Var( - Span { - lo: BytePos(10), - hi: BytePos(11) - }, - "z" + Free("z") ), Binop( - Span { - lo: BytePos(14), - hi: BytePos(25) - }, Mul, Binop( - Span { - lo: BytePos(15), - hi: BytePos(20) - }, Sub, Var( - Span { - lo: BytePos(15), - hi: BytePos(16) - }, - "z" + Free("z") ), Var( - Span { - lo: BytePos(19), - hi: BytePos(20) - }, - "x" + Free("x") ) ), Var( - Span { - lo: BytePos(24), - hi: BytePos(25) - }, - "a" + Free("a") ) ) ) diff --git a/src/parser/snapshots/mod.parse_mul_expr.snap b/src/parser/snapshots/mod.parse_mul_expr.snap index 932f5e8c9..8070c4960 100644 --- a/src/parser/snapshots/mod.parse_mul_expr.snap +++ b/src/parser/snapshots/mod.parse_mul_expr.snap @@ -1,35 +1,15 @@ Binop( - Span { - lo: BytePos(0), - hi: BytePos(9) - }, Mul, Var( - Span { - lo: BytePos(0), - hi: BytePos(1) - }, - "x" + Free("x") ), Binop( - Span { - lo: BytePos(4), - hi: BytePos(9) - }, Mul, Var( - Span { - lo: BytePos(4), - hi: BytePos(5) - }, - "y" + Free("y") ), Var( - Span { - lo: BytePos(8), - hi: BytePos(9) - }, - "z" + Free("z") ) ) ) diff --git a/src/parser/snapshots/mod.parse_mul_expr_mixed.snap b/src/parser/snapshots/mod.parse_mul_expr_mixed.snap index 01df895bf..534fe4d1f 100644 --- a/src/parser/snapshots/mod.parse_mul_expr_mixed.snap +++ b/src/parser/snapshots/mod.parse_mul_expr_mixed.snap @@ -1,61 +1,25 @@ Binop( - Span { - lo: BytePos(0), - hi: BytePos(17) - }, Mul, Var( - Span { - lo: BytePos(0), - hi: BytePos(1) - }, - "x" + Free("x") ), Binop( - Span { - lo: BytePos(4), - hi: BytePos(17) - }, Mul, Var( - Span { - lo: BytePos(4), - hi: BytePos(5) - }, - "y" + Free("y") ), Binop( - Span { - lo: BytePos(8), - hi: BytePos(17) - }, Div, Var( - Span { - lo: BytePos(8), - hi: BytePos(9) - }, - "z" + Free("z") ), Binop( - Span { - lo: BytePos(12), - hi: BytePos(17) - }, Mul, Var( - Span { - lo: BytePos(12), - hi: BytePos(13) - }, - "z" + Free("z") ), Var( - Span { - lo: BytePos(16), - hi: BytePos(17) - }, - "x" + Free("x") ) ) ) diff --git a/src/parser/snapshots/mod.parse_simple_definition.snap b/src/parser/snapshots/mod.parse_simple_definition.snap index 959bb4bd5..1ff9a9dc2 100644 --- a/src/parser/snapshots/mod.parse_simple_definition.snap +++ b/src/parser/snapshots/mod.parse_simple_definition.snap @@ -1,13 +1,8 @@ [ Definition { - span: Span { - lo: BytePos(13), - hi: BytePos(28) - }, name: "Offset32", - ty: UInt( - 4, - Target + ty: Var( + Free("u32") ) } ] diff --git a/src/parser/snapshots/mod.parse_sub_expr.snap b/src/parser/snapshots/mod.parse_sub_expr.snap index 2c11ff1cf..18154ae06 100644 --- a/src/parser/snapshots/mod.parse_sub_expr.snap +++ b/src/parser/snapshots/mod.parse_sub_expr.snap @@ -1,35 +1,15 @@ Binop( - Span { - lo: BytePos(0), - hi: BytePos(9) - }, Sub, Var( - Span { - lo: BytePos(0), - hi: BytePos(1) - }, - "x" + Free("x") ), Binop( - Span { - lo: BytePos(4), - hi: BytePos(9) - }, Sub, Var( - Span { - lo: BytePos(4), - hi: BytePos(5) - }, - "y" + Free("y") ), Var( - Span { - lo: BytePos(8), - hi: BytePos(9) - }, - "z" + Free("z") ) ) ) diff --git a/src/parser/snapshots/mod.parse_ty_array_dependent.snap b/src/parser/snapshots/mod.parse_ty_array_dependent.snap new file mode 100644 index 000000000..2d1cf0207 --- /dev/null +++ b/src/parser/snapshots/mod.parse_ty_array_dependent.snap @@ -0,0 +1,68 @@ +Struct( + [ + Field { + name: "len", + value: Var( + Free("u32") + ) + }, + Field { + name: "data1", + value: Array( + Var( + Free("f32") + ), + Var( + Bound(Named("len", 0)) + ) + ) + }, + Field { + name: "data2", + value: Struct( + [ + Field { + name: "data1", + value: Array( + Var( + Free("f32") + ), + Var( + Bound(Named("len", 1)) + ) + ) + }, + Field { + name: "len", + value: Var( + Free("u32") + ) + }, + Field { + name: "padding1", + value: Var( + Free("u8") + ) + }, + Field { + name: "padding2", + value: Var( + Free("u8") + ) + }, + Field { + name: "data2", + value: Array( + Var( + Free("f32") + ), + Var( + Bound(Named("len", 2)) + ) + ) + } + ] + ) + } + ] +) diff --git a/src/parser/snapshots/mod.parse_ty_empty_struct.snap b/src/parser/snapshots/mod.parse_ty_empty_struct.snap index 428f601ca..056f541fa 100644 --- a/src/parser/snapshots/mod.parse_ty_empty_struct.snap +++ b/src/parser/snapshots/mod.parse_ty_empty_struct.snap @@ -1,7 +1,3 @@ Struct( - Span { - lo: BytePos(0), - hi: BytePos(9) - }, [] ) diff --git a/src/parser/snapshots/mod.parse_ty_var.snap b/src/parser/snapshots/mod.parse_ty_var.snap index d2550f317..8809310da 100644 --- a/src/parser/snapshots/mod.parse_ty_var.snap +++ b/src/parser/snapshots/mod.parse_ty_var.snap @@ -1,7 +1,3 @@ Var( - Span { - lo: BytePos(13), - hi: BytePos(18) - }, - "Point" + Free("Point") ) diff --git a/src/parser/snapshots/mod.parse_ty_where.snap b/src/parser/snapshots/mod.parse_ty_where.snap index b690f18e4..ddcfae303 100644 --- a/src/parser/snapshots/mod.parse_ty_where.snap +++ b/src/parser/snapshots/mod.parse_ty_where.snap @@ -1,61 +1,72 @@ -Where( - Span { - lo: BytePos(13), - hi: BytePos(132) - }, - Where( - Span { - lo: BytePos(13), - hi: BytePos(103) - }, +Cond( + Cond( Struct( - Span { - lo: BytePos(13), - hi: BytePos(75) - }, [ Field { - span: Span { - lo: BytePos(38), - hi: BytePos(60) - }, name: "x", - ty: Where( - Span { - lo: BytePos(41), - hi: BytePos(60) - }, - UInt( - 4, - Target + value: Cond( + Var( + Free("u32") ), - "x", - Const( - Span { - lo: BytePos(56), - hi: BytePos(60) - }, - Bool(true) + Abs( + Named("x", Var( + Free("u32") + )), + Binop( + Eq, + Var( + Bound(Named("x", 0)) + ), + Const( + Int(3) + ) + ) ) ) } ] ), - "x", - Const( - Span { - lo: BytePos(99), - hi: BytePos(103) - }, - Bool(true) + Abs( + Named("x", Struct( + [ + Field { + name: "x", + value: Var( + Free("u32") + ) + } + ] + )), + Binop( + Eq, + Var( + Bound(Named("x", 0)) + ), + Const( + Int(2) + ) + ) ) ), - "x", - Const( - Span { - lo: BytePos(127), - hi: BytePos(132) - }, - Bool(false) + Abs( + Named("x", Struct( + [ + Field { + name: "x", + value: Var( + Free("u32") + ) + } + ] + )), + Binop( + Eq, + Var( + Bound(Named("x", 0)) + ), + Const( + Int(1) + ) + ) ) ) diff --git a/src/source.rs b/src/source.rs index 01d5b3509..0fa5d1e98 100644 --- a/src/source.rs +++ b/src/source.rs @@ -377,28 +377,6 @@ impl Span { pub fn until(self, end: Span) -> Span { Span::new(self.lo(), end.lo()) } - - /// Wrap a value in the span - /// - /// ```rust - /// use ddl::source::{BytePos, Span, Spanned}; - /// - /// enum Expr { - /// Var(String), - /// Abs(String, Spanned>), - /// App(Spanned>, Spanned>), - /// } - /// - /// let span = Span::new(BytePos(2), BytePos(5)); - /// let expr = Expr::Var("x".to_owned()); - /// let x: Spanned> = span.with(expr); - /// ``` - pub fn with, U>(self, value: T) -> Spanned { - Spanned { - span: self, - value: value.into(), - } - } } impl From<(BytePos, BytePos)> for Span { @@ -407,25 +385,6 @@ impl From<(BytePos, BytePos)> for Span { } } -/// A value with an associated `Span` -/// -/// Construct a `Spanned` in a fluent way using `Span::with`. -#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)] -pub struct Spanned { - pub span: Span, - pub value: T, -} - -impl Spanned { - /// Apply the function `f` to the underlying value and return the wrapped result - pub fn map U>(self, mut f: F) -> Spanned { - Spanned { - span: self.span, - value: f(self.value), - } - } -} - /// Some source code pub struct Source { /// The name of the file that the source came from diff --git a/src/syntax/binary.rs b/src/syntax/binary.rs new file mode 100644 index 000000000..87e9faefb --- /dev/null +++ b/src/syntax/binary.rs @@ -0,0 +1,329 @@ +//! The syntax of our data description language + +use syntax::{self, host, Field, Name, Named, Var}; + +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum Kind { + /// Kind of types + Type, + /// Kind of type functions + Arrow(Box, Box), +} + +impl Kind { + /// Kind of type functions + pub fn arrow>, K2: Into>>(lhs: K1, rhs: K2) -> Kind { + Kind::Arrow(lhs.into(), rhs.into()) + } +} + +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum TypeConst { + Bit, +} + +/// A binary type +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum Type { + /// A type variable: eg. `T` + Var(Var), + /// Type constant + Const(TypeConst), + /// An array of the specified type, with a size: eg. `[T; n]` + Array(Box>, Box>), + /// A union of types: eg. `union { T, ... }` + Union(Vec>), + /// A struct type, with fields: eg. `struct { field : T, ... }` + Struct(Vec>>), + /// A type constrained by a predicate: eg. `T where x => x == 3` + Cond(Box>, Box>), + /// An interpreted type + Interp(Box>, Box>, Box>), + /// Type abstraction: eg. `\(a : Type) -> T` + Abs(Named, Box>), + /// Type application: eg. `T U V` + App(Box>, Box>), +} + +impl Type { + /// A free type variable: eg. `T` + pub fn fvar>(x: N1) -> Type { + Type::Var(Var::Free(x.into())) + } + + /// A bound type variable + pub fn bvar>(x: N1, i: u32) -> Type { + Type::Var(Var::Bound(Named(x.into(), i))) + } + + /// Bit type constant + pub fn bit() -> Type { + Type::Const(TypeConst::Bit) + } + + /// An array of the specified type, with a size: eg. `[T; n]` + pub fn array>>, E1: Into>>>( + elem_ty: T1, + size_expr: E1, + ) -> Type { + Type::Array(elem_ty.into(), size_expr.into()) + } + + /// A union of types: eg. `union { T, ... }` + pub fn union(tys: Vec>) -> Type { + Type::Union(tys) + } + + /// Type application: eg. `T U V` + pub fn app>>, T2: Into>>>(ty1: T1, ty2: T2) -> Type { + Type::App(ty1.into(), ty2.into()) + } + + /// A struct type, with fields: eg. `struct { field : T, ... }` + pub fn struct_(mut fields: Vec>>) -> Type { + // We maintain a list of the seen field names. This will allow us to + // recover the index of these variables as we abstract later fields... + let mut seen_names = Vec::with_capacity(fields.len()); + + for field in &mut fields { + for (level, name) in seen_names.iter().rev().enumerate() { + field.value.abstract_name_at(name, level as u32); + } + + // Record that the field has been 'seen' + seen_names.push(field.name.clone()); + } + + Type::Struct(fields) + } + + /// A type constrained by a predicate: eg. `T where x => x == 3` + pub fn cond(ty: T1, pred: E1) -> Type + where + T1: Into>>, + E1: Into>>, + { + Type::Cond(ty.into(), pred.into()) + } + + /// An interpreted type + pub fn interp(ty: T1, conv: E1, repr_ty: T2) -> Type + where + T1: Into>>, + E1: Into>>, + T2: Into>>, + { + Type::Interp(ty.into(), conv.into(), repr_ty.into()) + } + + /// Type abstraction: eg. `\(a : Type) -> T` + pub fn abs((param_name, param_kind): (N1, Kind), body_ty: T1) -> Type + where + N1: Into, + T1: Into>>, + { + let param_name = param_name.into(); + let mut body_ty = body_ty.into(); + body_ty.abstract_name(¶m_name); + Type::Abs(Named(param_name, param_kind), body_ty) + } + + pub fn lookup_field(&self, name: &N) -> Option<&Type> { + match *self { + Type::Struct(ref fields) => syntax::lookup_field(fields, name), + _ => None, + } + } + + pub fn abstract_name_at(&mut self, name: &N, level: u32) { + match *self { + Type::Var(ref mut var) => var.abstract_name_at(name, level), + Type::Const(_) => {} + Type::Array(ref mut elem_ty, ref mut size_expr) => { + elem_ty.abstract_name_at(name, level); + size_expr.abstract_name_at(name, level); + } + Type::Union(ref mut tys) => for ty in tys { + ty.abstract_name_at(name, level); + }, + Type::Struct(ref mut fields) => for (i, field) in fields.iter_mut().enumerate() { + field.value.abstract_name_at(name, level + i as u32); + }, + Type::Cond(ref mut ty, ref mut pred) => { + ty.abstract_name_at(name, level); + pred.abstract_name_at(name, level + 1); + } + Type::Interp(ref mut ty, ref mut conv, ref mut repr_ty) => { + ty.abstract_name_at(name, level); + conv.abstract_name_at(name, level + 1); + repr_ty.abstract_name_at(name, level); + } + Type::Abs(_, ref mut body_ty) => { + body_ty.abstract_name_at(name, level + 1); + } + Type::App(ref mut fn_ty, ref mut arg_ty) => { + fn_ty.abstract_name_at(name, level); + arg_ty.abstract_name_at(name, level); + } + } + } + + pub fn abstract_name(&mut self, name: &N) { + self.abstract_name_at(name, 0); + } + + fn instantiate_at(&mut self, level: u32, src: &Type) { + // Bleh: Running into non-lexical liftetime problems here! + // Just so you know that I'm not going completely insane.... + // FIXME: ensure that expressions are not bound at the same level + *self = match *self { + Type::Var(Var::Bound(ref i)) => if *i == level { + src.clone() + } else { + return; + }, + Type::Var(Var::Free(_)) | Type::Const(_) => return, + Type::Array(ref mut elem_ty, _) => { + elem_ty.instantiate_at(level, src); + return; + } + Type::Cond(ref mut ty, _) => { + ty.instantiate_at(level + 1, src); + return; + } + Type::Interp(ref mut ty, _, _) => { + ty.instantiate_at(level + 1, src); + return; + } + Type::Union(ref mut tys) => { + for ty in tys { + ty.instantiate_at(level, src); + } + return; + } + Type::Struct(ref mut fields) => { + for (i, field) in fields.iter_mut().enumerate() { + field.value.instantiate_at(level + i as u32, src); + } + return; + } + Type::Abs(_, ref mut ty) => { + ty.instantiate_at(level + 1, src); + return; + } + Type::App(ref mut ty, ref mut arg_ty) => { + ty.instantiate_at(level, src); + arg_ty.instantiate_at(level, src); + return; + } + }; + } + + pub fn instantiate(&mut self, ty: &Type) { + self.instantiate_at(0, ty); + } + + pub fn repr(&self) -> Result, ()> { + match *self { + Type::Var(ref v) => Ok(host::Type::Var(v.clone()).into()), + Type::Const(TypeConst::Bit) => Ok(host::Type::Const(host::TypeConst::Bit).into()), + Type::Array(ref elem_ty, ref size_expr) => { + let elem_repr_ty = Box::new(elem_ty.repr()?); + let size_expr = size_expr.clone(); + + Ok(host::Type::Array(elem_repr_ty, size_expr).into()) + } + Type::Cond(ref ty, _) => ty.repr(), + Type::Interp(_, _, ref repr_ty) => Ok((**repr_ty).clone()), + Type::Union(ref tys) => { + let repr_tys = tys.iter().map(Type::repr).collect::>()?; + + Ok(host::Type::Union(repr_tys).into()) + } + Type::Struct(ref fields) => { + let repr_fields = fields + .iter() + .map(|f| f.value.repr().map(|ty| Field::new(f.name.clone(), ty))) + .collect::>()?; + + Ok(host::Type::Struct(repr_fields).into()) + } + Type::Abs(_, _) | Type::App(_, _) => Err(()), + } + } +} + +#[cfg(test)] +mod tests { + use super::*; + + mod ty { + use super::*; + + mod abs { + use super::*; + use self::Kind as K; + + type T = Type<&'static str>; + + #[test] + fn id() { + // λx.λy. x + // λ λ 1 + let ty = T::abs(("x", K::Type), T::fvar("x")); + + assert_snapshot!(ty_abs_id, ty); + } + + // Examples from https://en.wikipedia.org/wiki/De_Bruijn_index + + #[test] + fn k_combinator() { + // λx.λy. x + // λ λ 1 + let ty = T::abs(("x", K::Type), T::abs(("y", K::Type), T::fvar("x"))); + + assert_snapshot!(ty_abs_k_combinator, ty); + } + + #[test] + fn s_combinator() { + // λx.λy.λz. x z (y z) + // λ λ λ 2 0 (1 0) + let ty = T::abs( + ("x", K::Type), + T::abs( + ("y", K::Type), + T::abs( + ("z", K::Type), + T::app( + T::app(T::fvar("x"), T::fvar("z")), + T::app(T::fvar("y"), T::fvar("z")), + ), + ), + ), + ); + + assert_snapshot!(ty_abs_s_combinator, ty); + } + + #[test] + fn complex() { + // λz.(λy. y (λx. x)) (λx. z x) + // λ (λ 0 (λ 0)) (λ 1 0) + let ty = T::abs( + ("z", K::Type), + T::app( + T::abs( + ("y", K::Type), + T::app(T::fvar("y"), T::abs(("x", K::Type), T::fvar("x"))), + ), + T::abs(("x", K::Type), T::app(T::fvar("z"), T::fvar("x"))), + ), + ); + + assert_snapshot!(ty_abs_complex, ty); + } + } + } +} diff --git a/src/syntax/host.rs b/src/syntax/host.rs new file mode 100644 index 000000000..3f1c1279f --- /dev/null +++ b/src/syntax/host.rs @@ -0,0 +1,334 @@ +//! The syntax of our data description language + +use std::fmt; + +use syntax::{self, Field, Name, Named, Var}; + +#[derive(Copy, Clone, PartialEq, Eq)] +pub enum Const { + /// A single bit + Bit(bool), + /// A boolean constant: eg. `true`, `false` + Bool(bool), + /// An integer constant: eg. `0`, `1`, `2`, ... + Int(i64), +} + +impl fmt::Debug for Const { + fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { + match *self { + Const::Bit(value) => write!(f, "Bit({:?})", value), + Const::Bool(value) => write!(f, "Bool({:?})", value), + Const::Int(value) => write!(f, "Int({:?})", value), + } + } +} + +/// An unary operator +#[derive(Debug, Copy, Clone, PartialEq, Eq)] +pub enum Unop { + /// Not: eg. `!x` + Not, + /// Negation: eg. `-x` + Neg, +} + +/// A binary operator +#[derive(Debug, Copy, Clone, PartialEq, Eq)] +pub enum Binop { + /// Disjunction: eg. `x | y` + Or, + /// Conjunction: eg. `x & y` + And, + /// Equality: eg. `x == y` + Eq, + /// Inequality: eg. `x != y` + Ne, + /// Less than or equal: eg. `x <= y` + Le, + /// Less than: eg. `x < y` + Lt, + /// Greater than: eg. `x > y` + Gt, + /// Greater than or equal: eg. `x >= y` + Ge, + /// Addition: eg. `x + y` + Add, + /// Subtraction: eg. `x - y` + Sub, + /// Multiplication: eg. `x * y` + Mul, + /// Division: eg. `x / y` + Div, +} + +/// A host expression +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum Expr { + /// A constant value + Const(Const), + /// Primitive expressions + Prim(&'static str, Box>), + /// A variable, referring to an integer that exists in the current + /// context: eg. `len`, `num_tables` + Var(Var), + /// An unary operator expression + Unop(Unop, Box>), + /// A binary operator expression + Binop(Binop, Box>, Box>), + /// Field projection, eg: `x.field` + Proj(Box>, N), + /// Abstraction, eg: `\(x : T) -> x` + Abs(Named>>, Box>), +} + +impl Expr { + /// A bit constant: eg. `0b`, `01` + pub fn bit(value: bool) -> Expr { + Expr::Const(Const::Bit(value)) + } + + /// A boolean constant: eg. `true`, `false` + pub fn bool(value: bool) -> Expr { + Expr::Const(Const::Bool(value)) + } + + /// An integer constant: eg. `0`, `1`, `2`, ... + pub fn int(value: i64) -> Expr { + Expr::Const(Const::Int(value)) + } + + /// Primitive expressions + pub fn prim>>>(name: &'static str, repr_ty: T1) -> Expr { + Expr::Prim(name, repr_ty.into()) + } + + /// A free variable, referring to an integer that exists in the current + /// context: eg. `len`, `num_tables` + pub fn fvar>(x: N1) -> Expr { + Expr::Var(Var::Free(x.into())) + } + + /// A bound variable + pub fn bvar>(x: N1, i: u32) -> Expr { + Expr::Var(Var::Bound(Named(x.into(), i))) + } + + /// An unary operator expression + pub fn unop>>>(op: Unop, x: E1) -> Expr { + Expr::Unop(op, x.into()) + } + + /// A binary operator expression + pub fn binop>>, E2: Into>>>( + op: Binop, + x: E1, + y: E2, + ) -> Expr { + Expr::Binop(op, x.into(), y.into()) + } + + /// Field projection, eg: `x.field` + pub fn proj>>, M: Into>(e: E1, field: M) -> Expr { + Expr::Proj(e.into(), field.into()) + } + + /// Abstraction, eg: `\(x : T) -> x` + pub fn abs((param_name, param_ty): (N1, T1), body_expr: E1) -> Expr + where + N1: Into, + T1: Into>>, + E1: Into>>, + { + let param_name = param_name.into(); + let mut body_expr = body_expr.into(); + body_expr.abstract_name(¶m_name); + Expr::Abs(Named(param_name, param_ty.into()), body_expr) + } + + pub fn abstract_name_at(&mut self, name: &N, level: u32) { + match *self { + Expr::Var(ref mut var) => var.abstract_name_at(name, level), + Expr::Const(_) => {} + Expr::Prim(_, ref mut repr_ty) => repr_ty.abstract_name_at(name, level), + Expr::Unop(_, ref mut expr) | Expr::Proj(ref mut expr, _) => { + expr.abstract_name_at(name, level); + } + Expr::Binop(_, ref mut lhs_expr, ref mut rhs_expr) => { + lhs_expr.abstract_name_at(name, level); + rhs_expr.abstract_name_at(name, level); + } + Expr::Abs(_, ref mut body_expr) => { + body_expr.abstract_name_at(name, level + 1); + } + } + } + + pub fn abstract_name(&mut self, name: &N) { + self.abstract_name_at(name, 0); + } +} + +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum TypeConst { + /// Bit + Bit, + /// Boolean + Bool, + /// Integer + Int, +} + +/// A host type +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum Type { + /// A type variable: eg. `T` + Var(Var), + /// A type constant + Const(TypeConst), + /// Arrow type: eg. `T -> U` + Arrow(Box>, Box>), + /// An array of the specified type, with a size: eg. `[T; n]` + Array(Box>, Box>), + /// A union of types: eg. `union { T, ... }` + Union(Vec>), + /// A struct type, with fields: eg. `struct { field : T, ... }` + Struct(Vec>>), +} + +impl Type { + /// A free type variable: eg. `T` + pub fn fvar>(x: N1) -> Type { + Type::Var(Var::Free(x.into())) + } + + /// A bound type variable + pub fn bvar>(x: N, i: u32) -> Type { + Type::Var(Var::Bound(Named(x.into(), i))) + } + + /// Bit type constant + pub fn bit() -> Type { + Type::Const(TypeConst::Bit) + } + + /// Boolean type constant + pub fn bool() -> Type { + Type::Const(TypeConst::Bool) + } + + /// Integer type constant + pub fn int() -> Type { + Type::Const(TypeConst::Int) + } + + /// Arrow type: eg. `T -> U` + pub fn arrow>>, E1: Into>>>( + lhs_ty: T1, + rhs_ty: E1, + ) -> Type { + Type::Arrow(lhs_ty.into(), rhs_ty.into()) + } + + /// An array of the specified type, with a size: eg. `[T; n]` + pub fn array>>, E1: Into>>>( + elem_ty: T1, + size_expr: E1, + ) -> Type { + Type::Array(elem_ty.into(), size_expr.into()) + } + + /// A union of types: eg. `union { T, ... }` + pub fn union(tys: Vec>) -> Type { + Type::Union(tys) + } + + /// A struct type, with fields: eg. `struct { field : T, ... }` + pub fn struct_(mut fields: Vec>>) -> Type { + // We maintain a list of the seen field names. This will allow us to + // recover the index of these variables as we abstract later fields... + let mut seen_names = Vec::with_capacity(fields.len()); + + for field in &mut fields { + for (level, name) in seen_names.iter().rev().enumerate() { + field.value.abstract_name_at(name, level as u32); + } + + // Record that the field has been 'seen' + seen_names.push(field.name.clone()); + } + + Type::Struct(fields) + } + + pub fn lookup_field(&self, name: &N) -> Option<&Type> { + match *self { + Type::Struct(ref fields) => syntax::lookup_field(fields, name), + _ => None, + } + } + + pub fn abstract_name_at(&mut self, name: &N, level: u32) { + match *self { + Type::Var(ref mut var) => var.abstract_name_at(name, level), + Type::Const(_) => {} + Type::Arrow(ref mut lhs_ty, ref mut rhs_ty) => { + lhs_ty.abstract_name_at(name, level); + rhs_ty.abstract_name_at(name, level); + } + Type::Array(ref mut elem_ty, ref mut size_expr) => { + elem_ty.abstract_name_at(name, level); + size_expr.abstract_name_at(name, level); + } + Type::Union(ref mut tys) => for ty in tys { + ty.abstract_name_at(name, level); + }, + Type::Struct(ref mut fields) => for (i, field) in fields.iter_mut().enumerate() { + field.value.abstract_name_at(name, level + i as u32); + }, + } + } + + pub fn abstract_name(&mut self, name: &N) { + self.abstract_name_at(name, 0) + } + + fn instantiate_at(&mut self, level: u32, src: &Type) { + // Bleh: Running into non-lexical liftetime problems here! + // Just so you know that I'm not going completely insane.... + // FIXME: ensure that expressions are not bound at the same level + *self = match *self { + Type::Var(Var::Bound(ref i)) => if *i == level { + src.clone() + } else { + return; + }, + Type::Var(Var::Free(_)) | Type::Const(_) => return, + Type::Arrow(ref mut lhs_ty, ref mut rhs_ty) => { + lhs_ty.instantiate_at(level, src); + rhs_ty.instantiate_at(level, src); + return; + } + Type::Array(ref mut elem_ty, _) => { + elem_ty.instantiate_at(level, src); + return; + } + Type::Union(ref mut tys) => { + for ty in tys { + ty.instantiate_at(level, src); + } + return; + } + Type::Struct(ref mut fields) => { + for (i, field) in fields.iter_mut().enumerate() { + field.value.instantiate_at(level + i as u32, src); + } + return; + } + }; + } + + pub fn instantiate(&mut self, ty: &Type) { + self.instantiate_at(0, ty); + } +} diff --git a/src/syntax/mod.rs b/src/syntax/mod.rs new file mode 100644 index 000000000..d220cdacf --- /dev/null +++ b/src/syntax/mod.rs @@ -0,0 +1,293 @@ +//! The syntax of our data description language + +use std::fmt; + +pub mod binary; +pub mod host; + +/// A type definition +/// +/// ```plain +/// Point = { +/// x : u16, +/// y : u16, +/// } +/// ``` +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct Definition { + pub name: N, + pub ty: Box>, +} + +impl Definition { + pub fn new, T1: Into>>>(name: N1, ty: T1) -> Definition { + Definition { + name: name.into(), + ty: ty.into(), + } + } +} + +/// A variable that can either be free or bound +/// +/// We use a locally nameless representation for variable binding. +/// +/// # References +/// +/// - [How I learned to stop worrying and love de Bruijn indices] +/// (http://disciple-devel.blogspot.com.au/2011/08/how-i-learned-to-stop-worrying-and-love.html) +/// - [The Locally Nameless Representation] +/// (https://www.chargueraud.org/research/2009/ln/main.pdf) +/// - [Locally nameless representation with cofinite quantification] +/// (http://www.chargueraud.org/softs/ln/) +/// - [A Locally-nameless Backend for Ott] +/// (http://www.di.ens.fr/~zappa/projects/ln_ott/) +/// - [Library STLC_Tutorial] +/// (https://www.cis.upenn.edu/~plclub/popl08-tutorial/code/coqdoc/STLC_Tutorial.html) +/// +/// ## Libraries +/// +/// There are a number of libraries out there for other languages that abstract +/// away handling locally nameless representations, but I've not yet figured out +/// how to port them to Rust yet: +/// +/// - DBLib: Facilities for working with de Bruijn indices in Coq +/// - [Blog Post](http://gallium.inria.fr/blog/announcing-dblib/) +/// - [Github](https://github.com/coq-contribs/dblib) +/// - Bound: Bruijn indices for Haskell +/// - [Blog Post](https://www.schoolofhaskell.com/user/edwardk/bound) +/// - [Github](https://github.com/ekmett/bound/) +/// - [Hackage](https://hackage.haskell.org/package/bound) +/// - The Penn Locally Nameless Metatheory Library +/// - [Github](https://github.com/plclub/metalib) +#[derive(Clone, PartialEq, Eq)] +pub enum Var { + /// A free, unbound variable + Free(N), + /// A bound variable + Bound(Named), +} + +impl Var { + pub fn abstract_name_at(&mut self, name: &N, level: B) { + *self = match *self { + Var::Free(ref n) if n == name => Var::Bound(Named(n.clone(), level)), + Var::Free(_) | Var::Bound(_) => return, + } + } +} + +impl fmt::Debug for Var { + fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { + match *self { + Var::Free(ref x) => { + write!(f, "Free(")?; + x.fmt(f)?; + } + Var::Bound(ref i) => { + write!(f, "Bound(")?; + i.fmt(f)?; + } + } + write!(f, ")") + } +} + +/// Trait alias for types that work well as names in the AST +pub trait Name: Clone + PartialEq + fmt::Debug + fmt::Display {} + +impl Name for T {} + +/// A variable with a name that is ignored for comparisons. This is useful for +/// improving error reporting when converting free varables to a named form. +/// +/// # Type parameters +/// +/// - `N`: The name that will be ignored for comparison purposes +/// - `T`: The type of the variable +#[derive(Clone, Eq, PartialOrd, Ord)] +pub struct Named(pub N, pub T); + +impl PartialEq for Named { + fn eq(&self, other: &Named) -> bool { + self.1 == other.1 + } +} + +impl PartialEq for Named { + fn eq(&self, other: &T) -> bool { + &self.1 == other + } +} + +impl From<(N, T)> for Named { + fn from(src: (N, T)) -> Named { + Named(src.0, src.1) + } +} + +impl fmt::Debug for Named { + fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { + write!(f, "Named(")?; + self.0.fmt(f)?; + write!(f, ", ")?; + self.1.fmt(f)?; + write!(f, ")") + } +} + +/// A field in a struct type +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct Field { + pub name: N, + pub value: T, +} + +impl Field { + pub fn new, U: Into>(name: M, value: U) -> Field { + Field { + name: name.into(), + value: value.into(), + } + } + + /// Apply the function `f` to the field name and return the wrapped result + pub fn map_name M>(self, mut f: F) -> Field { + Field { + name: f(self.name), + value: self.value, + } + } + + /// Apply the function `f` to the field value and return the wrapped result + pub fn map_value U>(self, mut f: F) -> Field { + Field { + name: self.name, + value: f(self.value), + } + } +} + +fn lookup_field<'a, N, T>(fields: &'a [Field], name: &N) -> Option<&'a T> +where + N: PartialEq, +{ + fields + .iter() + .find(|field| &field.name == name) + .map(|field| &field.value) +} + +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum Binding { + Expr(host::Type), + Type(binary::Kind), + TypeDef(binary::Type, binary::Kind), +} + +#[derive(Debug, Clone)] +pub struct Ctx { + bindings: Vec>>, +} + +impl Ctx { + pub fn new() -> Ctx { + Ctx { + bindings: Vec::new(), + } + } + + pub fn extend(&mut self, name: N, binding: Binding) { + self.bindings.push(Named(name, binding)); + } + + pub fn lookup(&self, i: u32) -> Named<&N, &Binding> { + assert!(self.bindings.len() > i as usize, "ICE: Binder out of range"); + + let Named(ref name, ref binding) = self.bindings[self.bindings.len() - i as usize - 1]; + + Named(name, binding) + } + + pub fn lookup_ty(&self, i: u32) -> Result>, Named<&N, &Binding>> { + let Named(name, binding) = self.lookup(i); + + match *binding { + Binding::Expr(ref ty) => Ok(Named(name, ty)), + _ => Err(Named(name, binding)), + } + } + + pub fn lookup_ty_def( + &self, + i: u32, + ) -> Result>, Named<&N, &Binding>> { + let Named(name, binding) = self.lookup(i); + + match *binding { + Binding::TypeDef(ref ty, _) => Ok(Named(name, ty)), + _ => Err(Named(name, binding)), + } + } + + pub fn lookup_kind(&self, i: u32) -> Result, Named<&N, &Binding>> { + let Named(name, binding) = self.lookup(i); + + match *binding { + Binding::Type(ref kind) => Ok(Named(name, kind)), + Binding::TypeDef(_, ref kind) => Ok(Named(name, kind)), + _ => Err(Named(name, binding)), + } + } +} + +pub fn base_defs From<&'a str>>() -> Vec> { + fn prim_array_ty(size: i64, conv_name: &'static str) -> binary::Type { + use self::binary::Type; + use self::host::Expr; + + let array_ty = Type::array(Type::bit(), Expr::int(size)); + let conv_ty = host::Type::arrow(array_ty.repr().unwrap(), host::Type::int()); + + Type::interp(array_ty, Expr::prim(conv_name, conv_ty), host::Type::int()) + } + + vec![ + // TODO: "true" = Expr::bool(true) + // TODO: "false" = Expr::bool(false) + + // Native endian primitives (Do we need these?) + Definition::new("u8", prim_array_ty(8, "from_u8")), + Definition::new("u16", prim_array_ty(16, "from_u16")), + Definition::new("u32", prim_array_ty(32, "from_u32")), + Definition::new("u64", prim_array_ty(64, "from_u64")), + Definition::new("i8", prim_array_ty(8, "from_i8")), + Definition::new("i16", prim_array_ty(16, "from_i16")), + Definition::new("i32", prim_array_ty(32, "from_i32")), + Definition::new("i64", prim_array_ty(64, "from_i64")), + Definition::new("f32", prim_array_ty(32, "from_f32")), + Definition::new("f64", prim_array_ty(64, "from_f64")), + // Little endian primitives + Definition::new("u8le", prim_array_ty(8, "from_u8le")), + Definition::new("u16le", prim_array_ty(16, "from_u16le")), + Definition::new("u32le", prim_array_ty(32, "from_u32le")), + Definition::new("u64le", prim_array_ty(64, "from_u64le")), + Definition::new("i8le", prim_array_ty(8, "from_i8le")), + Definition::new("i16le", prim_array_ty(16, "from_i16le")), + Definition::new("i32le", prim_array_ty(32, "from_i32le")), + Definition::new("i64le", prim_array_ty(64, "from_i64le")), + Definition::new("f32le", prim_array_ty(32, "from_f32le")), + Definition::new("f64le", prim_array_ty(64, "from_f64le")), + // Big endian primitives + Definition::new("u8be", prim_array_ty(8, "from_u8be")), + Definition::new("u16be", prim_array_ty(16, "from_u16be")), + Definition::new("u32be", prim_array_ty(32, "from_u32be")), + Definition::new("u64be", prim_array_ty(64, "from_u64be")), + Definition::new("i8be", prim_array_ty(8, "from_i8be")), + Definition::new("i16be", prim_array_ty(16, "from_i16be")), + Definition::new("i32be", prim_array_ty(32, "from_i32be")), + Definition::new("i64be", prim_array_ty(64, "from_i64be")), + Definition::new("f32be", prim_array_ty(32, "from_f32be")), + Definition::new("f64be", prim_array_ty(64, "from_f64be")), + ] +} diff --git a/src/syntax/snapshots/binary.ty_abs_complex.snap b/src/syntax/snapshots/binary.ty_abs_complex.snap new file mode 100644 index 000000000..0fe59b337 --- /dev/null +++ b/src/syntax/snapshots/binary.ty_abs_complex.snap @@ -0,0 +1,30 @@ +Abs( + Named("z", Type), + App( + Abs( + Named("y", Type), + App( + Var( + Bound(Named("y", 0)) + ), + Abs( + Named("x", Type), + Var( + Bound(Named("x", 0)) + ) + ) + ) + ), + Abs( + Named("x", Type), + App( + Var( + Bound(Named("z", 1)) + ), + Var( + Bound(Named("x", 0)) + ) + ) + ) + ) +) diff --git a/src/syntax/snapshots/binary.ty_abs_id.snap b/src/syntax/snapshots/binary.ty_abs_id.snap new file mode 100644 index 000000000..de4ab2057 --- /dev/null +++ b/src/syntax/snapshots/binary.ty_abs_id.snap @@ -0,0 +1,6 @@ +Abs( + Named("x", Type), + Var( + Bound(Named("x", 0)) + ) +) diff --git a/src/syntax/snapshots/binary.ty_abs_k_combinator.snap b/src/syntax/snapshots/binary.ty_abs_k_combinator.snap new file mode 100644 index 000000000..251a24aed --- /dev/null +++ b/src/syntax/snapshots/binary.ty_abs_k_combinator.snap @@ -0,0 +1,9 @@ +Abs( + Named("x", Type), + Abs( + Named("y", Type), + Var( + Bound(Named("x", 1)) + ) + ) +) diff --git a/src/syntax/snapshots/binary.ty_abs_s_combinator.snap b/src/syntax/snapshots/binary.ty_abs_s_combinator.snap new file mode 100644 index 000000000..8444d9e50 --- /dev/null +++ b/src/syntax/snapshots/binary.ty_abs_s_combinator.snap @@ -0,0 +1,27 @@ +Abs( + Named("x", Type), + Abs( + Named("y", Type), + Abs( + Named("z", Type), + App( + App( + Var( + Bound(Named("x", 2)) + ), + Var( + Bound(Named("z", 0)) + ) + ), + App( + Var( + Bound(Named("y", 1)) + ), + Var( + Bound(Named("z", 0)) + ) + ) + ) + ) + ) +) diff --git a/src/test.rs b/src/test.rs index efba38073..1718f181a 100644 --- a/src/test.rs +++ b/src/test.rs @@ -73,14 +73,17 @@ macro_rules! assert_snapshot { println!("{}", changes); println!("In file {:?}", file_name); println!(); - println!("Rerun the failing test with REGENERATE_SNAPSHOTS=1 regenerate the saved snapshot"); + println!("Rerun the failing test with REGENERATE_SNAPSHOTS=1 \ + regenerate the saved snapshot"); println!(); panic!(); } } Err(err) => { match err.kind() { - ErrorKind::NotFound => $crate::test::regenerate_snapshot(&file_name, value).unwrap(), + ErrorKind::NotFound => { + $crate::test::regenerate_snapshot(&file_name, value).unwrap() + } _ => panic!("{}", err), } } diff --git a/tests/examples.rs b/tests/examples.rs index 485e56151..a4518b8ee 100644 --- a/tests/examples.rs +++ b/tests/examples.rs @@ -1,49 +1,44 @@ extern crate ddl; -use ddl::Env; +use ddl::{check, parser, syntax}; #[test] #[ignore] fn cmap() { const SRC: &str = include_str!("../examples/ddl/cmap.ddl"); - let mut env = Env::default(); - let defs = ddl::parser::parse(&env, SRC).unwrap(); - env.check_defs(defs).unwrap(); + let defs = parser::parse(SRC).unwrap(); + check::check_defs(syntax::base_defs().iter().chain(&defs)).unwrap(); } #[test] fn edid() { const SRC: &str = include_str!("../examples/ddl/edid.ddl"); - let mut env = Env::default(); - let defs = ddl::parser::parse(&env, SRC).unwrap(); - env.check_defs(defs).unwrap(); + let defs = parser::parse(SRC).unwrap(); + check::check_defs(syntax::base_defs().iter().chain(&defs)).unwrap(); } #[test] fn heroes_of_might_and_magic_bmp() { const SRC: &str = include_str!("../examples/ddl/heroes_of_might_and_magic_bmp.ddl"); - let mut env = Env::default(); - let defs = ddl::parser::parse(&env, SRC).unwrap(); - env.check_defs(defs).unwrap(); + let defs = parser::parse(SRC).unwrap(); + check::check_defs(syntax::base_defs().iter().chain(&defs)).unwrap(); } #[test] fn object_id() { const SRC: &str = include_str!("../examples/ddl/object_id.ddl"); - let mut env = Env::default(); - let defs = ddl::parser::parse(&env, SRC).unwrap(); - env.check_defs(defs).unwrap(); + let defs = parser::parse(SRC).unwrap(); + check::check_defs(syntax::base_defs().iter().chain(&defs)).unwrap(); } #[test] fn stl() { const SRC: &str = include_str!("../examples/ddl/stl.ddl"); - let mut env = Env::default(); - let defs = ddl::parser::parse(&env, SRC).unwrap(); - env.check_defs(defs).unwrap(); + let defs = parser::parse(SRC).unwrap(); + check::check_defs(syntax::base_defs().iter().chain(&defs)).unwrap(); }