From 4113b2df365abe3dd1e971dccacf31c89eb83908 Mon Sep 17 00:00:00 2001 From: Aleksandr Date: Tue, 22 Oct 2024 01:11:03 +0300 Subject: [PATCH] new way --- crates/std/src/arena/ptr.rs | 28 +++++++++ crates/typing/src/check/check.rs | 1 + crates/typing/src/check/ctx.rs | 42 ++++++++++--- crates/typing/src/check/mod.rs | 6 +- crates/typing/src/check/shape.rs | 104 ------------------------------- crates/typing/src/int.rs | 4 +- crates/typing/src/ptr.rs | 32 +++++++--- 7 files changed, 91 insertions(+), 126 deletions(-) create mode 100644 crates/typing/src/check/check.rs delete mode 100644 crates/typing/src/check/shape.rs diff --git a/crates/std/src/arena/ptr.rs b/crates/std/src/arena/ptr.rs index f137771..53ee203 100644 --- a/crates/std/src/arena/ptr.rs +++ b/crates/std/src/arena/ptr.rs @@ -1,5 +1,32 @@ use std::{hash::Hash, num::NonZeroU32}; +#[macro_export] +#[doc(hidden)] +macro_rules! _tags { + ($( + $(#[$outer:meta])* + $vis:vis enum $name:ident { + $($tag:ident),* + $(,)? + } + )*) => {$( + #[derive( + Debug, + Clone, + Copy, + PartialEq, + Eq, + PartialOrd, + Ord, + Hash, + )] + $(#[$outer])* + $vis enum $name { + $($tag),* + } + )*}; +} + #[macro_export] #[doc(hidden)] macro_rules! _ptrs { @@ -57,3 +84,4 @@ pub trait Ptr: Copy + Eq + Into + From + Hash { } pub use crate::_ptrs as define; +pub use crate::_tags as tags; diff --git a/crates/typing/src/check/check.rs b/crates/typing/src/check/check.rs new file mode 100644 index 0000000..8b13789 --- /dev/null +++ b/crates/typing/src/check/check.rs @@ -0,0 +1 @@ + diff --git a/crates/typing/src/check/ctx.rs b/crates/typing/src/check/ctx.rs index 5aa46ef..4c0d2bd 100644 --- a/crates/typing/src/check/ctx.rs +++ b/crates/typing/src/check/ctx.rs @@ -1,21 +1,47 @@ use shiny_std::arena::intern; -use crate::ptr::{self, TaggedTy}; - -pub type Ts = intern::Arena; +use crate::{ + bin, int, + ptr::{self, TyTag as Tag}, +}; +#[derive(Clone)] pub struct Ctx { - ts: Ts, + /// Product types. + prod: intern::Arena, + /// Sum types. + sum: intern::Arena, + /// Integers. + ints: intern::Arena, } impl Ctx { - pub fn new(ts: Ts) -> Self { - Self { ts } + pub fn int(&self, ptr: ptr::RawTy) -> Option { + self.ints.get(ptr).cloned() + } + + pub fn prod(&self, ptr: ptr::RawTy) -> Option { + self.prod.get(ptr).cloned() + } + + pub fn sum(&self, ptr: ptr::RawTy) -> Option { + self.sum.get(ptr).cloned() } } impl Ctx { - pub fn get_type(&self, ptr: ptr::Ty) -> Option { - self.ts.get(ptr).cloned() + pub fn mk_int(&mut self, signedness: int::Signedness) -> ptr::Ty { + let ptr = self.ints.insert(int::Int(signedness)); + ptr::Ty::new(Tag::Int, ptr) + } + + pub fn mk_sum(&mut self, lhs: ptr::Ty, rhs: ptr::Ty) -> ptr::Ty { + let ptr = self.sum.insert(bin::Sum { lhs, rhs }); + ptr::Ty::new(Tag::Sum, ptr) + } + + pub fn mk_prod(&mut self, lhs: ptr::Ty, rhs: ptr::Ty) -> ptr::Ty { + let ptr = self.prod.insert(bin::Prod { lhs, rhs }); + ptr::Ty::new(Tag::Prod, ptr) } } diff --git a/crates/typing/src/check/mod.rs b/crates/typing/src/check/mod.rs index 7a50591..8590a9b 100644 --- a/crates/typing/src/check/mod.rs +++ b/crates/typing/src/check/mod.rs @@ -1,4 +1,4 @@ -//! # Type checking. +mod check; +mod ctx; -pub mod ctx; -pub mod shape; +pub use self::ctx::Ctx; diff --git a/crates/typing/src/check/shape.rs b/crates/typing/src/check/shape.rs deleted file mode 100644 index 82fd722..0000000 --- a/crates/typing/src/check/shape.rs +++ /dev/null @@ -1,104 +0,0 @@ -use crate::{ - bin, - ptr::{self, TaggedTy}, -}; - -use super::ctx::Ctx; - -pub fn fits(ctx: &Ctx, lptr: ptr::Ty, rptr: ptr::Ty) -> bool { - use TaggedTy as TT; - if lptr == rptr { - return true; - } - - let lhs = ctx.get_type(lptr).unwrap(); - let rhs = ctx.get_type(rptr).unwrap(); - - match (lhs, rhs) { - (TT::Prod(lhs), TT::Prod(rhs)) => { - let bin::Prod { - lhs: lhs_lhs, - rhs: lhs_rhs, - } = lhs; - let bin::Prod { - lhs: rhs_lhs, - rhs: rhs_rhs, - } = rhs; - - // (lhs_lhs * lhs_rhs) @ (rhs_lhs * rhs_rhs) - // -^^^^^^^---------------^^^^^^^----------- - // If they fit, it's time to advance and - // check lhs_rhs and rhs_rhs. - if fits(ctx, lhs_lhs, rhs_lhs) { - fits(ctx, lhs_rhs, rhs_rhs) - } else { - // Otherwise, the type is probably somewhere - // in tail. - fits(ctx, lptr, rhs_rhs) - } - } - - (_, TT::Prod(rhs)) => { - // lhs @ (rhs_lhs * rhs_rhs) - // ^^^----^^^^^^^~~~^^^^^^^ - // lhs should be either in rhs_lhs - // or in rhs_rhs. - fits(ctx, lptr, rhs.lhs) || fits(ctx, lptr, rhs.rhs) - } - - (TT::Sum(lhs), TT::Sum(rhs)) => { - todo!() - } - - _ => false, - } -} - -#[cfg(test)] -mod tests { - use crate::check::ctx; - - use super::*; - - fn case(fill: impl FnOnce(ctx::Ts) -> (T, ctx::Ts), check: impl FnOnce(T, Ctx)) { - let (arg, arena) = fill(ctx::Ts::new()); - let ctx = Ctx::new(arena); - - check(arg, ctx); - } - - #[test] - fn shape_matching() { - // (int * int) @ (int * int * int) - case( - |mut ts| { - let int = ts.insert(TaggedTy::Number); - let lhs = ts.insert(TaggedTy::Prod(bin::Prod { lhs: int, rhs: int })); - let rhs = ts.insert(TaggedTy::Prod(bin::Prod { lhs: int, rhs: lhs })); - - ((lhs, rhs), ts) - }, - |(lhs, rhs), ctx| assert!(fits(&ctx, lhs, rhs)), - ); - - // Associativity - // (int * int) @ ((int * str) * int) - case( - |mut ts| { - let int = ts.insert(TaggedTy::Number); - let str = ts.insert(TaggedTy::Str); - - let lhs = ts.insert(TaggedTy::Prod(bin::Prod { lhs: int, rhs: int })); - - let rhs_lhs = ts.insert(TaggedTy::Prod(bin::Prod { lhs: int, rhs: str })); - let rhs = ts.insert(TaggedTy::Prod(bin::Prod { - lhs: rhs_lhs, - rhs: int, - })); - - ((lhs, rhs), ts) - }, - |(lhs, rhs), ctx| assert!(fits(&ctx, lhs, rhs)), - ); - } -} diff --git a/crates/typing/src/int.rs b/crates/typing/src/int.rs index dd50a90..38e0beb 100644 --- a/crates/typing/src/int.rs +++ b/crates/typing/src/int.rs @@ -1,7 +1,7 @@ //! # Integer types. /// Sign of the integer. -#[derive(Debug, Clone, Copy)] +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)] pub enum Signedness { /// The number has sign. Signed, @@ -10,5 +10,5 @@ pub enum Signedness { } /// Integer. -#[derive(Debug, Clone, Copy)] +#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)] pub struct Int(pub Signedness); diff --git a/crates/typing/src/ptr.rs b/crates/typing/src/ptr.rs index 4e26a0f..37383ff 100644 --- a/crates/typing/src/ptr.rs +++ b/crates/typing/src/ptr.rs @@ -4,21 +4,35 @@ //! This means that there's unambiguous mapping from id to value and //! back. -use crate::bin; +use shiny_std::arena::ptr::{define, tags}; -use shiny_std::arena::ptr::define; +/// Type. +pub type Ty = Tagged; #[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)] -pub enum TaggedTy { - Prod(bin::Prod), - Sum(bin::Sum), - Number, - Str, +pub struct Tagged { + pub tag: T, + pub ptr: P, +} + +impl Tagged { + pub const fn new(tag: T, ptr: P) -> Self { + Self { tag, ptr } + } +} + +tags! { + pub enum TyTag { + Prod, + Sum, + Int, + Str, + } } define! { - /// Pointer to a type. - pub struct Ty; + /// Untagged pointer to the type. + pub struct RawTy; /// Pointer to ID. pub struct Id;