From 0f0f39e1c7f49ea4cfd004d2c9f73ef910346fa8 Mon Sep 17 00:00:00 2001
From: Aleksandr <nerodono0@gmail.com>
Date: Mon, 21 Oct 2024 22:43:21 +0300
Subject: [PATCH] add fits check for product types

---
 crates/typing/src/check/ctx.rs   |  22 ++++++-
 crates/typing/src/check/shape.rs | 103 ++++++++++++++++++++++++++++++-
 crates/typing/src/pat.rs         |   2 +-
 crates/typing/src/ptr.rs         |  10 +++
 4 files changed, 132 insertions(+), 5 deletions(-)

diff --git a/crates/typing/src/check/ctx.rs b/crates/typing/src/check/ctx.rs
index 7072c46..5aa46ef 100644
--- a/crates/typing/src/check/ctx.rs
+++ b/crates/typing/src/check/ctx.rs
@@ -1 +1,21 @@
-pub struct Ctx {}
+use shiny_std::arena::intern;
+
+use crate::ptr::{self, TaggedTy};
+
+pub type Ts = intern::Arena<TaggedTy, ptr::Ty>;
+
+pub struct Ctx {
+    ts: Ts,
+}
+
+impl Ctx {
+    pub fn new(ts: Ts) -> Self {
+        Self { ts }
+    }
+}
+
+impl Ctx {
+    pub fn get_type(&self, ptr: ptr::Ty) -> Option<TaggedTy> {
+        self.ts.get(ptr).cloned()
+    }
+}
diff --git a/crates/typing/src/check/shape.rs b/crates/typing/src/check/shape.rs
index 3331c7d..82fd722 100644
--- a/crates/typing/src/check/shape.rs
+++ b/crates/typing/src/check/shape.rs
@@ -1,7 +1,104 @@
-use crate::ptr;
+use crate::{
+    bin,
+    ptr::{self, TaggedTy},
+};
 
 use super::ctx::Ctx;
 
-pub fn fits(lhs: ptr::Ty, rhs: ptr::Ty) -> bool {
-    todo!()
+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<T>(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/pat.rs b/crates/typing/src/pat.rs
index d24f0d1..da54729 100644
--- a/crates/typing/src/pat.rs
+++ b/crates/typing/src/pat.rs
@@ -1,4 +1,4 @@
-use shiny_arena::make_comb;
+use shiny_std::arena::make_comb;
 
 use crate::ptr;
 
diff --git a/crates/typing/src/ptr.rs b/crates/typing/src/ptr.rs
index 6f8d0cd..4e26a0f 100644
--- a/crates/typing/src/ptr.rs
+++ b/crates/typing/src/ptr.rs
@@ -4,8 +4,18 @@
 //! This means that there's unambiguous mapping from id to value and
 //! back.
 
+use crate::bin;
+
 use shiny_std::arena::ptr::define;
 
+#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)]
+pub enum TaggedTy {
+    Prod(bin::Prod),
+    Sum(bin::Sum),
+    Number,
+    Str,
+}
+
 define! {
     /// Pointer to a type.
     pub struct Ty;