Initial commit

crates/typing/Cargo.toml

@@ -0,0 +1,7 @@
+[package]
+name = "shiny-typing"
+version = "0.1.0"
+edition = "2021"
+
+[dependencies]
+shiny-std.workspace = true

crates/typing/src/bin.rs

@@ -0,0 +1,33 @@
+//! # Binary types
+
+use shiny_std::arena::make_comb;
+
+use crate::ptr;
+
+make_comb! {
+    /// Type with additionally equipped ID.
+    pub struct Field {
+        pub ty: ptr::Ty,
+        pub id: ptr::Id,
+    }
+
+    /// Product type. Pretty much just `lhs_ty * rhs_ty`.
+    /// The following properties must be upheld:
+    ///
+    /// 1. lhs * rhs = rhs * lhs          <- commutativity
+    /// 2. (a * b) * c = a * (b * c)      <- associativity
+    pub struct Prod {
+        pub lhs: ptr::Ty,
+        pub rhs: ptr::Ty,
+    }
+
+    /// Sum type. Pretty much just `lhs_ty + rhs_ty`.
+    /// The following properties must be upheld:
+    ///
+    /// 1. lhs + rhs = rhs + rhs          <- commutativity
+    /// 2. (a + b) + c = a + (b + c)      <- associativity
+    pub struct Sum {
+        pub lhs: ptr::Ty,
+        pub rhs: ptr::Ty,
+    }
+}

crates/typing/src/check/ctx.rs

@@ -0,0 +1 @@
+pub struct Ctx {}

crates/typing/src/check/mod.rs

@@ -0,0 +1,4 @@
+//! # Type checking.
+
+pub mod ctx;
+pub mod shape;

crates/typing/src/check/shape.rs

@@ -0,0 +1,7 @@
+use crate::ptr;
+
+use super::ctx::Ctx;
+
+pub fn fits(lhs: ptr::Ty, rhs: ptr::Ty) -> bool {
+    todo!()
+}

crates/typing/src/infer/ctx.rs

@@ -0,0 +1,15 @@
+use shiny_std::arena::intern;
+
+use crate::{bin, int, ptr};
+
+enum Ty {
+    Prod(bin::Prod),
+    Sum(bin::Sum),
+    Field(bin::Field),
+    Int(int::Int),
+}
+
+/// Inference context.
+pub struct Ctx {
+    tys: intern::Arena<Ty, ptr::Ty>,
+}

crates/typing/src/infer/mod.rs

@@ -0,0 +1,3 @@
+//! # Type inference.
+
+mod ctx;

crates/typing/src/int.rs

@@ -0,0 +1,14 @@
+//! # Integer types.
+
+/// Sign of the integer.
+#[derive(Debug, Clone, Copy)]
+pub enum Signedness {
+    /// The number has sign.
+    Signed,
+    /// The number has no sign.
+    Unsigned,
+}
+
+/// Integer.
+#[derive(Debug, Clone, Copy)]
+pub struct Int(pub Signedness);

crates/typing/src/lib.rs

@@ -0,0 +1,10 @@
+pub mod bin;
+pub mod un;
+
+pub mod int;
+pub mod pat;
+
+pub mod ptr;
+
+pub mod check;
+pub mod infer;

crates/typing/src/pat.rs

@@ -0,0 +1,32 @@
+use shiny_arena::make_comb;
+
+use crate::ptr;
+
+make_comb! {
+    /// Product type pattern.
+    pub struct Prod {
+        pub lhs: ptr::Pat,
+        pub rhs: ptr::Pat,
+    }
+
+    /// Sum type pattern.
+    pub struct Sum {
+        pub lhs: ptr::Pat,
+        pub rhs: ptr::Pat,
+    }
+
+    /// Exact type. Matches only if matched type
+    /// equals to specified.
+    pub struct ExactTy(pub ptr::Ty);
+
+    /// Field type. matches `{ name : ty_pat }`
+    pub struct Field {
+        pub name: ptr::Id,
+        pub ty: ptr::Pat,
+    }
+
+    /// "Value" pattern. Works like [`ExactTy`], but
+    /// additionally checks whether value of that type is equal
+    /// to specified value.
+    pub struct Value(pub ptr::Value);
+}

crates/typing/src/ptr.rs

@@ -0,0 +1,21 @@
+//! # Pointers to needed information.
+//!
+//! If values are equal, then their pointers are equal.
+//! This means that there's unambiguous mapping from id to value and
+//! back.
+
+use shiny_std::arena::ptr::define;
+
+define! {
+    /// Pointer to a type.
+    pub struct Ty;
+
+    /// Pointer to ID.
+    pub struct Id;
+
+    /// Pointer to a pattern.
+    pub struct Pat;
+
+    /// Pointer to a *complete* value.
+    pub struct Value;
+}

crates/typing/src/un.rs

@@ -0,0 +1 @@
+//! # Unary types