new way
This commit is contained in:
parent
0f0f39e1c7
commit
4113b2df36
7 changed files with 91 additions and 126 deletions
|
@ -1,5 +1,32 @@
|
||||||
use std::{hash::Hash, num::NonZeroU32};
|
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]
|
#[macro_export]
|
||||||
#[doc(hidden)]
|
#[doc(hidden)]
|
||||||
macro_rules! _ptrs {
|
macro_rules! _ptrs {
|
||||||
|
@ -57,3 +84,4 @@ pub trait Ptr: Copy + Eq + Into<NonZeroU32> + From<NonZeroU32> + Hash {
|
||||||
}
|
}
|
||||||
|
|
||||||
pub use crate::_ptrs as define;
|
pub use crate::_ptrs as define;
|
||||||
|
pub use crate::_tags as tags;
|
||||||
|
|
1
crates/typing/src/check/check.rs
Normal file
1
crates/typing/src/check/check.rs
Normal file
|
@ -0,0 +1 @@
|
||||||
|
|
|
@ -1,21 +1,47 @@
|
||||||
use shiny_std::arena::intern;
|
use shiny_std::arena::intern;
|
||||||
|
|
||||||
use crate::ptr::{self, TaggedTy};
|
use crate::{
|
||||||
|
bin, int,
|
||||||
pub type Ts = intern::Arena<TaggedTy, ptr::Ty>;
|
ptr::{self, TyTag as Tag},
|
||||||
|
};
|
||||||
|
|
||||||
|
#[derive(Clone)]
|
||||||
pub struct Ctx {
|
pub struct Ctx {
|
||||||
ts: Ts,
|
/// Product types.
|
||||||
|
prod: intern::Arena<bin::Prod, ptr::RawTy>,
|
||||||
|
/// Sum types.
|
||||||
|
sum: intern::Arena<bin::Sum, ptr::RawTy>,
|
||||||
|
/// Integers.
|
||||||
|
ints: intern::Arena<int::Int, ptr::RawTy>,
|
||||||
}
|
}
|
||||||
|
|
||||||
impl Ctx {
|
impl Ctx {
|
||||||
pub fn new(ts: Ts) -> Self {
|
pub fn int(&self, ptr: ptr::RawTy) -> Option<int::Int> {
|
||||||
Self { ts }
|
self.ints.get(ptr).cloned()
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn prod(&self, ptr: ptr::RawTy) -> Option<bin::Prod> {
|
||||||
|
self.prod.get(ptr).cloned()
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn sum(&self, ptr: ptr::RawTy) -> Option<bin::Sum> {
|
||||||
|
self.sum.get(ptr).cloned()
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
impl Ctx {
|
impl Ctx {
|
||||||
pub fn get_type(&self, ptr: ptr::Ty) -> Option<TaggedTy> {
|
pub fn mk_int(&mut self, signedness: int::Signedness) -> ptr::Ty {
|
||||||
self.ts.get(ptr).cloned()
|
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)
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
|
@ -1,4 +1,4 @@
|
||||||
//! # Type checking.
|
mod check;
|
||||||
|
mod ctx;
|
||||||
|
|
||||||
pub mod ctx;
|
pub use self::ctx::Ctx;
|
||||||
pub mod shape;
|
|
||||||
|
|
|
@ -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<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,7 +1,7 @@
|
||||||
//! # Integer types.
|
//! # Integer types.
|
||||||
|
|
||||||
/// Sign of the integer.
|
/// Sign of the integer.
|
||||||
#[derive(Debug, Clone, Copy)]
|
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
|
||||||
pub enum Signedness {
|
pub enum Signedness {
|
||||||
/// The number has sign.
|
/// The number has sign.
|
||||||
Signed,
|
Signed,
|
||||||
|
@ -10,5 +10,5 @@ pub enum Signedness {
|
||||||
}
|
}
|
||||||
|
|
||||||
/// Integer.
|
/// Integer.
|
||||||
#[derive(Debug, Clone, Copy)]
|
#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)]
|
||||||
pub struct Int(pub Signedness);
|
pub struct Int(pub Signedness);
|
||||||
|
|
|
@ -4,21 +4,35 @@
|
||||||
//! 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, tags};
|
||||||
|
|
||||||
use shiny_std::arena::ptr::define;
|
/// Type.
|
||||||
|
pub type Ty = Tagged<TyTag, RawTy>;
|
||||||
|
|
||||||
#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)]
|
#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)]
|
||||||
pub enum TaggedTy {
|
pub struct Tagged<T, P> {
|
||||||
Prod(bin::Prod),
|
pub tag: T,
|
||||||
Sum(bin::Sum),
|
pub ptr: P,
|
||||||
Number,
|
}
|
||||||
Str,
|
|
||||||
|
impl<T, P> Tagged<T, P> {
|
||||||
|
pub const fn new(tag: T, ptr: P) -> Self {
|
||||||
|
Self { tag, ptr }
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
tags! {
|
||||||
|
pub enum TyTag {
|
||||||
|
Prod,
|
||||||
|
Sum,
|
||||||
|
Int,
|
||||||
|
Str,
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
define! {
|
define! {
|
||||||
/// Pointer to a type.
|
/// Untagged pointer to the type.
|
||||||
pub struct Ty;
|
pub struct RawTy;
|
||||||
|
|
||||||
/// Pointer to ID.
|
/// Pointer to ID.
|
||||||
pub struct Id;
|
pub struct Id;
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue