add fits check for product types
This commit is contained in:
parent
85b08fe00b
commit
0f0f39e1c7
4 changed files with 132 additions and 5 deletions
|
@ -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()
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
|
@ -1,7 +1,104 @@
|
||||||
use crate::ptr;
|
use crate::{
|
||||||
|
bin,
|
||||||
|
ptr::{self, TaggedTy},
|
||||||
|
};
|
||||||
|
|
||||||
use super::ctx::Ctx;
|
use super::ctx::Ctx;
|
||||||
|
|
||||||
pub fn fits(lhs: ptr::Ty, rhs: ptr::Ty) -> bool {
|
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!()
|
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)),
|
||||||
|
);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
|
@ -1,4 +1,4 @@
|
||||||
use shiny_arena::make_comb;
|
use shiny_std::arena::make_comb;
|
||||||
|
|
||||||
use crate::ptr;
|
use crate::ptr;
|
||||||
|
|
||||||
|
|
|
@ -4,8 +4,18 @@
|
||||||
//! This means that there's unambiguous mapping from id to value and
|
//! This means that there's unambiguous mapping from id to value and
|
||||||
//! back.
|
//! back.
|
||||||
|
|
||||||
|
use crate::bin;
|
||||||
|
|
||||||
use shiny_std::arena::ptr::define;
|
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! {
|
define! {
|
||||||
/// Pointer to a type.
|
/// Pointer to a type.
|
||||||
pub struct Ty;
|
pub struct Ty;
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue