RefOf [WIP]

rust/crates/yanais-syntax/src/error.rs

@@ -139,6 +139,7 @@ pub enum ErrorCtx {
     Parentheses,
     Pattern,
     Record,
+    RefOf,
     Select,
     String,
     Ident,

rust/crates/yanais-syntax/src/expr.rs

@@ -34,6 +34,7 @@ pub enum Expr {
     Literal(Literal),
 
     Use(SelIdent),
+    RefUse(SelIdent),
 
     Lambda(Lambda),
     TyLambda {
@@ -68,6 +69,29 @@ fn parse_minexpr(env: &mut ParseEnv<'_>) -> Result<Expr> {
             }
         }
 
+        Tok::RefOf => {
+            let Token { span, kind } = env.lxr.next_in_noeof(Ectx::RefOf)?;
+            match kind {
+                Tok::Ident(i) => {
+                    if let Some(x) = env.lookup(&i) {
+                        Ok(Expr::Use(SelIdent {
+                            span,
+                            dbidx: x,
+                        }))
+                    } else {
+                        Err(Error {
+                            span,
+                            kind: Pek::UnknownIdent(i),
+                        })
+                    }
+                }
+                _ => Err(Error {
+                    span,
+                    kind: Pek::UnexpectedToken(Ectx::RefOf, kind),
+                }),
+            }
+        }
+
         Tok::Kw(Kw::Infer) => Ok(Expr::Infer),
         Tok::Kw(Kw::Literal(lit)) => Ok(Expr::Literal(lit)),
         Tok::Kw(Kw::Lambda) => Lambda::parse(env).map(Expr::Lambda),

rust/crates/yanais-syntax/src/lex.rs

@@ -73,6 +73,7 @@ pub enum TokenKind<KwT> {
     LArr,
     RArr,
     Dot,
+    RefOf,
     DubColon,
     SemiColon,
     Assign,
@@ -222,6 +223,7 @@ impl<Kw: core::str::FromStr> Iterator for Lexer<'_, Kw> {
                     Ok(match c {
                             '.' => Tk::DotIdent(try_consume_ident(slb).unwrap_or_else(|| Arc::from(""))),
                             '$' => Tk::PatOut(try_consume_ident(slb).unwrap_or_else(|| Arc::from(""))),
+                            '&' => Tk::RefOf,
                             ';' => Tk::SemiColon,
                             '^' => Tk::Caret,
                             '←' => Tk::LArr,

rust/crates/yanais-typeck/src/egraph.rs

@@ -127,6 +127,11 @@ fn subst_prune_csr<'a>(hsvars: &'a HashMap<Expr>, csr: &Rc<Var>) -> Cow<'a, Hash
 }
 
 impl Expr {
+    #[inline]
+    pub fn new(k: ExprKind) -> Self {
+        Self(Rc::new(RefCell::new(k)))
+    }
+
     fn deep_clone_intern(
         &self,
         hmexpr: &mut HashMap<Rc<RefCell<ExprKind>>>,

rust/crates/yanais-typeck/src/lib.rs

@@ -4,11 +4,18 @@ pub use egraph::Expr;
 use Expr as Type;
 
 #[derive(Clone, Debug, thiserror::Error)]
-pub enum Error {}
+pub enum Error {
+    #[error("unable to infer type")]
+    UnableToInfer,
+
+    #[error("unable to use value multiple times")]
+    UsedTooOften,
+}
 
 #[derive(Clone, Debug)]
 pub enum BinderState {
     Unknown,
+    PersistResolved(Expr),
     Resolved(Expr),
     Used,
 }
@@ -23,3 +30,46 @@ pub type Result<T> = core::result::Result<T, Error>;
 pub trait TypeCheckPattern {
     fn type_check_pat(&self, ctx: &mut TyContext) -> Result<()>;
 }
+
+pub trait TypeCheckExt {
+    fn type_check(&self, other: Type, ctx: &mut TyContext) -> Result<()>;
+}
+
+pub trait TypeInferExt {
+    fn type_infer(&self, ctx: &mut TyContext) -> Result<Type>;
+}
+
+impl TypeInferExt for yanais_syntax::expr::Expr {
+    fn type_infer(&self, ctx: &mut TyContext) -> Result<Type> {
+        use yanais_syntax::expr::Expr as Ex;
+        match self {
+            Ex::Infer => Err(Error::UnableToInfer),
+            Ex::Literal(lit) => {
+                use yanais_literal::{Literal, TyLit, IntSize};
+                Ok(Expr::new(egraph::ExprKind::Literal(match lit {
+                    Literal::Ty(_) => Literal::Ty(TyLit::Type),
+                    Literal::IntSize(_) => Literal::Ty(TyLit::IntSize),
+                    Literal::Natural(_) => Literal::IntSize(IntSize::Isize),
+                })))
+            }
+            Ex::Use(i) => {
+                use core::mem::replace;
+                match ctx.binders.len().checked_sub(i.dbidx + 1) {
+                    Some(n) => {
+                        let x = &mut ctx.binders[n];
+                        match replace(x, BinderState::Used) {
+                            BinderState::PersistResolved(y) => {
+                                *x = BinderState::PersistResolved(y.clone());
+                                Ok(y)
+                            }
+                            BinderState::Resolved(y) => Ok(y),
+                            BinderState::Unknown => Err(Error::UnableToInfer),
+                            BinderState::Used => Err(Error::UsedTooOften),
+                        }
+                    }
+                    None => panic!("tried to type-infer variable which is out of scope"),
+                }
+            }
+        }
+    }
+}