Skip to content

Commit

Permalink
feat(sol-syntax): fix something
Browse files Browse the repository at this point in the history
  • Loading branch information
@aripiprazole
aripiprazole committed May 9, 2024
1 parent 30cb04f commit cf76f68
Show file tree
Hide file tree
Showing 6 changed files with 245 additions and 35 deletions.
111 changes: 111 additions & 0 deletions sol-driver/suite/church_encoding.expect
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,111 @@
Error: found 44 errors
╭─[repl:1:1]
│
3 │ Nat = (n : U) -> (n -> n) -> n
│ ┬ ┬ ┬
│ ╰───────────── resolution error: unresolved `type` `n`
│ │ │
│ ╰──────── resolution error: unresolved `type` `n`
│ │
│ ╰── resolution error: unresolved `type` `n`
│
6 │ Succ = |prev n succ$ zero$| succ$ (prev n succ$ zero$) zero$
│ ┬─── ┬ ┬──── ┬──── ┬──── ┬─── ┬ ┬──── ┬──── ┬────
│ ╰───────────────────────────────────────────────────── resolution error: unresolved `type` `prev`
│ │ │ │ │ │ │ │ │ │
│ ╰──────────────────────────────────────────────── resolution error: unresolved `type` `n`
│ │ │ │ │ │ │ │ │
│ ╰────────────────────────────────────────────── resolution error: unresolved `type` `succ$`
│ │ │ │ │ │ │ │
│ ╰──────────────────────────────────────── resolution error: unresolved `type` `zero$`
│ │ │ │ │ │ │
│ ╰───────────────────────────────── resolution error: unresolved `function` `succ$`
│ │ │ │ │ │
│ ╰────────────────────────── resolution error: unresolved `function` `prev`
│ │ │ │ │
│ ╰───────────────────── resolution error: unresolved `function` `n`
│ │ │ │
│ ╰─────────────────── resolution error: unresolved `function` `succ$`
│ │ │
│ ╰───────────── resolution error: unresolved `function` `zero$`
│ │
│ ╰────── resolution error: unresolved `function` `zero$`
│
9 │ Zero = |n succ$ zero$| zero$
│ ┬ ┬──── ┬──── ┬────
│ ╰───────────────────── resolution error: unresolved `type` `n`
│ │ │ │
│ ╰─────────────────── resolution error: unresolved `type` `succ$`
│ │ │
│ ╰───────────── resolution error: unresolved `type` `zero$`
│ │
│ ╰────── resolution error: unresolved `function` `zero$`
│
13 │ Maybe = |t| (a : U) -> (t -> a) -> a -> a
│ ┬ ┬ ┬ ┬ ┬
│ ╰───────────────────────────────── resolution error: unresolved `type` `t`
│ │ │ │ │
│ ╰────────────────── resolution error: unresolved `type` `t`
│ │ │ │
│ ╰───────────── resolution error: unresolved `type` `a`
│ │ │
│ ╰─────── resolution error: unresolved `type` `a`
│ │
│ ╰── resolution error: unresolved `type` `a`
│
15 │ Just : 'a -> Maybe 'a
│ ┬─ ┬──── ┬─
│ ╰─────────────── resolution error: unresolved `type` `'a`
│ │ │
│ ╰───────── resolution error: unresolved `type` `Maybe`
│ │
│ ╰─── resolution error: unresolved `type` `'a`
16 │ Just = |value t just$ nothing$| just$ value
│ ┬──── ┬ ┬──── ┬─────── ┬──── ┬────
│ ╰──────────────────────────────────── resolution error: unresolved `type` `value`
│ │ │ │ │ │
│ ╰────────────────────────────── resolution error: unresolved `type` `t`
│ │ │ │ │
│ ╰──────────────────────────── resolution error: unresolved `type` `just$`
│ │ │ │
│ ╰────────────────────── resolution error: unresolved `type` `nothing$`
│ │ │
│ ╰──────────── resolution error: unresolved `function` `just$`
│ │
│ ╰────── resolution error: unresolved `function` `value`
│
18 │ Nothing : Maybe 'a
│ ┬──── ┬─
│ ╰───────── resolution error: unresolved `type` `Maybe`
│ │
│ ╰─── resolution error: unresolved `type` `'a`
19 │ Nothing = |t just$ nothing$| nothing$
│ ┬ ┬──── ┬─────── ┬───────
│ ╰─────────────────────────── resolution error: unresolved `type` `t`
│ │ │ │
│ ╰───────────────────────── resolution error: unresolved `type` `just$`
│ │ │
│ ╰─────────────────── resolution error: unresolved `type` `nothing$`
│ │
│ ╰───────── resolution error: unresolved `function` `nothing$`
│
21 │ Maybe.unwrap : Maybe -> 'a
│ ┬──── ┬─
│ ╰──────────── resolution error: unresolved `type` `Maybe`
│ │
│ ╰─── resolution error: unresolved `type` `'a`
22 │ Maybe.unwrap = |maybe|
│ ┬────
│ ╰────── resolution error: unresolved `type` `maybe`
23 │ maybe $
│ ┬──── ┬
│ ╰──────── resolution error: unresolved `function` `maybe`
│ │
│ ╰── resolution error: unresolved `function` `$`
24 │ (|value| value) $
│ ┬────────────────
│ ╰────────────────── parse error: unexpected token(s): (|value| value) $
25 │ sorry
│ ┬────
│ ╰────── resolution error: unresolved `function` `sorry`
────╯
25 changes: 14 additions & 11 deletions sol-driver/suite/church_encoding.sol
View file
Original file line number Diff line number Diff line change
@@ -1,22 +1,25 @@
// Natural numbers
Nat : U = (n : U) -> (n -> n) -> n
Nat : U
Nat = (n : U) -> (n -> n) -> n

Succ (prev : Nat) : Nat = |n succ$ zero$|
succ$ (prev n succ$ zero$) zero$
Succ : Nat -> Nat
Succ = |prev n succ$ zero$| succ$ (prev n succ$ zero$) zero$

Zero : Nat = |n succ$ zero$|
zero$
Zero : Nat
Zero = |n succ$ zero$| zero$

// Maybe definition
Maybe (t : U) = (a : U) -> (t -> a) a -> a
Maybe : U -> U
Maybe = |t| (a : U) -> (t -> a) -> a -> a

Just (value : a) : Maybe a = |t just$ nothing$|
just$ value
Just : 'a -> Maybe 'a
Just = |value t just$ nothing$| just$ value

Nothing : Maybe a = |t just$ nothing$|
nothing$
Nothing : Maybe 'a
Nothing = |t just$ nothing$| nothing$

Maybe.unwrap (maybe : Maybe a) : a =
Maybe.unwrap : Maybe -> 'a
Maybe.unwrap = |maybe|
maybe $
(|value| value) $
sorry
10 changes: 9 additions & 1 deletion sol-hir-lowering/src/pattern.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -77,7 +77,15 @@ impl HirLowering<'_, '_> {

// If the patterns are empty, it's a binding pattern, otherwise, it's a constructor
// pattern.
if patterns.is_empty() {
if patterns.is_empty()
&& name
.to_string(self.db)
.unwrap()
.chars()
.next()
.unwrap()
.is_lowercase()
{
// Defines the node on the scope
let name = self
.scope
Expand Down
32 changes: 16 additions & 16 deletions sol-hir-lowering/src/stmt.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -72,25 +72,25 @@ impl HirLowering<'_, '_> {
.solve(self, |this, node| this.expr(node, level));

let then = stmt.then().solve(self, |this, node| {
use sol_syntax::anon_unions::AnnExpr_AppExpr_BinaryExpr_Block_ForallExpr_LamExpr_MatchExpr_PiExpr_Primary_SigmaExpr::*;
use sol_syntax::anon_unions::AnnExpr_AppExpr_BinaryExpr_Block_ForallExpr_LamExpr_MatchExpr_PiExpr_Primary_SigmaExpr::*;

node.child().solve(this, |this, node| match node {
Block(block) => Expr::block(this.db, this.block(block, level)),
_ => this.expr(node.into_node().try_into().unwrap(), level),
})
});
node.child().solve(this, |this, node| match node {
Block(block) => Expr::block(this.db, this.block(block, level)),
_ => this.expr(node.into_node().try_into().unwrap(), level),
})
});

let otherwise = stmt.otherwise().map(|then| {
then.solve(self, |this, node| {
use sol_syntax::anon_unions::AnnExpr_AppExpr_BinaryExpr_Block_ForallExpr_LamExpr_MatchExpr_PiExpr_Primary_SigmaExpr::*;

node.value().solve(this, |this, node| match node {
Block(block) => Expr::block(this.db, this.block(block, level)),
_ => this.expr(node.into_node().try_into().unwrap(), level),
})
})
})
.unwrap_or_else(|| Expr::call_unit_expr(Location::CallSite, self.db));
then.solve(self, |this, node| {
use sol_syntax::anon_unions::AnnExpr_AppExpr_BinaryExpr_Block_ForallExpr_LamExpr_MatchExpr_PiExpr_Primary_SigmaExpr::*;

node.value().solve(this, |this, node| match node {
Block(block) => Expr::block(this.db, this.block(block, level)),
_ => this.expr(node.into_node().try_into().unwrap(), level),
})
})
})
.unwrap_or_else(|| Expr::call_unit_expr(Location::CallSite, self.db));

let clauses = vec![
MatchArm {
Expand Down
12 changes: 9 additions & 3 deletions sol-hir-lowering/src/term.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,6 @@ use sol_hir::{
HirElement,
},
};
use sol_syntax::anon_unions::Comma_ConsPattern_GroupPattern_Literal_Parameter_RestPattern;

use super::*;

Expand Down Expand Up @@ -99,7 +98,14 @@ impl HirLowering<'_, '_> {
/// into a high-level binary expression.
pub fn binary_expr(&mut self, tree: sol_syntax::BinaryExpr, level: HirLevel) -> Expr {
let lhs = tree.lhs().solve(self, |this, node| this.expr(node, level));
let rhs = tree.rhs().solve(self, |this, node| this.expr(node, level));
let rhs = tree.rhs().solve(self, |this, node| {
use sol_syntax::anon_unions::BinaryExpr_Primary::*;

match node {
BinaryExpr(binary_expr) => this.binary_expr(binary_expr, level),
Primary(primary) => this.primary(primary, level),
}
});
let op = tree.op().solve(self, |this, node| {
let location = this.range(node.range());
let identifier = node
Expand Down Expand Up @@ -262,7 +268,7 @@ impl HirLowering<'_, '_> {
.flatten()
.filter_map(|parameter| parameter.regular())
.map(|parameter| {
use Comma_ConsPattern_GroupPattern_Literal_Parameter_RestPattern::*;
use sol_syntax::anon_unions::Comma_ConsPattern_GroupPattern_Literal_Parameter_RestPattern::*;

match parameter {
Parameter(parameter) => self.parameter(true, true, parameter),
Expand Down
90 changes: 86 additions & 4 deletions sol-syntax/src/generated/node_types.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -388,7 +388,7 @@ impl<'tree> type_sitter_lib::TypedNode<'tree> for Binary<'tree> {
Self(node)
}
}
#[doc = "Typed node `binary_expr`\n\nThis node has these fields:\n- `lhs`: `{ann_expr | app_expr | binary_expr | forall_expr | lam_expr | match_expr | pi_expr | primary | sigma_expr}` ([anon_unions::AnnExpr_AppExpr_BinaryExpr_ForallExpr_LamExpr_MatchExpr_PiExpr_Primary_SigmaExpr])\n- `op`: `infix_op` ([InfixOp])\n- `rhs`: `{ann_expr | app_expr | binary_expr | forall_expr | lam_expr | match_expr | pi_expr | primary | sigma_expr}` ([anon_unions::AnnExpr_AppExpr_BinaryExpr_ForallExpr_LamExpr_MatchExpr_PiExpr_Primary_SigmaExpr])\n"]
#[doc = "Typed node `binary_expr`\n\nThis node has these fields:\n- `lhs`: `{ann_expr | app_expr | binary_expr | forall_expr | lam_expr | match_expr | pi_expr | primary | sigma_expr}` ([anon_unions::AnnExpr_AppExpr_BinaryExpr_ForallExpr_LamExpr_MatchExpr_PiExpr_Primary_SigmaExpr])\n- `op`: `infix_op` ([InfixOp])\n- `rhs`: `{binary_expr | primary}` ([anon_unions::BinaryExpr_Primary])\n"]
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[allow(non_camel_case_types)]
pub struct BinaryExpr<'tree>(tree_sitter::Node<'tree>);
Expand All @@ -407,10 +407,13 @@ impl<'tree> BinaryExpr<'tree> {
self . 0 . child_by_field_name ("op") . map (< InfixOp < 'tree > as TryFrom < _ >> :: try_from) . expect ("tree-sitter node missing its required child, there should at least be a MISSING node in its place")
}

#[doc = "Get the field `rhs` which has kind `{ann_expr | app_expr | binary_expr | forall_expr | lam_expr | match_expr | pi_expr | primary | sigma_expr}` ([anon_unions::AnnExpr_AppExpr_BinaryExpr_ForallExpr_LamExpr_MatchExpr_PiExpr_Primary_SigmaExpr])"]
#[doc = "Get the field `rhs` which has kind `{binary_expr | primary}` ([anon_unions::BinaryExpr_Primary])"]
#[allow(dead_code)]
#[inline] pub fn rhs (& self) -> type_sitter_lib :: NodeResult < 'tree , anon_unions :: AnnExpr_AppExpr_BinaryExpr_ForallExpr_LamExpr_MatchExpr_PiExpr_Primary_SigmaExpr < 'tree > >{
self . 0 . child_by_field_name ("rhs") . map (< anon_unions :: AnnExpr_AppExpr_BinaryExpr_ForallExpr_LamExpr_MatchExpr_PiExpr_Primary_SigmaExpr < 'tree > as TryFrom < _ >> :: try_from) . expect ("tree-sitter node missing its required child, there should at least be a MISSING node in its place")
#[inline]
pub fn rhs(
&self,
) -> type_sitter_lib::NodeResult<'tree, anon_unions::BinaryExpr_Primary<'tree>> {
self . 0 . child_by_field_name ("rhs") . map (< anon_unions :: BinaryExpr_Primary < 'tree > as TryFrom < _ >> :: try_from) . expect ("tree-sitter node missing its required child, there should at least be a MISSING node in its place")
}
}
#[automatically_derived]
Expand Down Expand Up @@ -7987,6 +7990,85 @@ pub mod anon_unions {
}
}
}
#[doc = "one of `{binary_expr | primary}`:\n- [BinaryExpr]\n- [Primary]"]
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[allow(non_camel_case_types)]
pub enum BinaryExpr_Primary<'tree> {
BinaryExpr(BinaryExpr<'tree>),
Primary(Primary<'tree>),
}
#[automatically_derived]
impl<'tree> BinaryExpr_Primary<'tree> {
#[doc = "Returns the node if it is of kind `binary_expr` ([BinaryExpr]), otherwise returns None"]
#[inline]
#[allow(unused, non_snake_case)]
pub fn binary_expr(self) -> Option<BinaryExpr<'tree>> {
match self {
Self::BinaryExpr(x) => Some(x),
_ => None,
}
}

#[doc = "Returns the node if it is of kind `primary` ([Primary]), otherwise returns None"]
#[inline]
#[allow(unused, non_snake_case)]
pub fn primary(self) -> Option<Primary<'tree>> {
match self {
Self::Primary(x) => Some(x),
_ => None,
}
}
}
#[automatically_derived]
impl<'tree> TryFrom<tree_sitter::Node<'tree>> for BinaryExpr_Primary<'tree> {
type Error = type_sitter_lib::IncorrectKind<'tree>;

#[inline]
fn try_from(node: tree_sitter::Node<'tree>) -> Result<Self, Self::Error> {
match node.kind() {
"binary_expr" => Ok(unsafe {
Self :: BinaryExpr (< BinaryExpr < 'tree > as type_sitter_lib :: TypedNode < 'tree >> :: from_node_unchecked (node))
}),
"primary" => {
Ok(unsafe {
Self :: Primary (< Primary < 'tree > as type_sitter_lib :: TypedNode < 'tree >> :: from_node_unchecked (node))
})
}
_ => Err(type_sitter_lib::IncorrectKind {
node,
kind: <Self as type_sitter_lib::TypedNode<'tree>>::KIND,
}),
}
}
}
#[automatically_derived]
impl<'tree> type_sitter_lib::TypedNode<'tree> for BinaryExpr_Primary<'tree> {
const KIND: &'static str = "{binary_expr | primary}";

#[inline]
fn node(&self) -> &tree_sitter::Node<'tree> {
match self {
Self::BinaryExpr(x) => x.node(),
Self::Primary(x) => x.node(),
}
}

#[inline]
fn node_mut(&mut self) -> &mut tree_sitter::Node<'tree> {
match self {
Self::BinaryExpr(x) => x.node_mut(),
Self::Primary(x) => x.node_mut(),
}
}

#[inline]
fn into_node(self) -> tree_sitter::Node<'tree> {
match self {
Self::BinaryExpr(x) => x.into_node(),
Self::Primary(x) => x.into_node(),
}
}
}
#[doc = "one of `{ask_stmt | expr_stmt | if_stmt | let_stmt}`:\n- [AskStmt]\n- [ExprStmt]\n- [IfStmt]\n- [LetStmt]"]
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[allow(non_camel_case_types)]
Expand Down

0 comments on commit cf76f68

Please sign in to comment.