Skip to content

Commit

Permalink
feat(sol-driver): fix church encoding tests
Browse files Browse the repository at this point in the history
  • Loading branch information
@aripiprazole
aripiprazole committed May 8, 2024
1 parent 91974b8 commit 19fff4a
Show file tree
Hide file tree
Showing 2 changed files with 167 additions and 27 deletions.
160 changes: 160 additions & 0 deletions sol-driver/suite/church_encoding.expect
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,160 @@
Error: found 1 errors
╭─[unresolved:1:1]
│
1 │
│ │
│ ╰─ resolution error: Empty expression representation is not allowed to be used in any contexts
───╯
Error: found 64 errors
╭─[repl:1:1]
│
2 │ Nat : * = (n : *) -> (n -> n) -> n
│ │┬── ┬──── ┬ ┬ ┬
│ ╰────────────────────────────── parse error: (missing "return")
│ │ │ │ │ │
│ ╰───────────────────────────── resolution error: unresolved `function` `* =`
│ │ │ │ │
│ ╰──────────────────────── parse error: unexpected token(s): n : *
│ │ │ │
│ ╰───────────── resolution error: unresolved `type` `n`
│ │ │
│ ╰──────── resolution error: unresolved `type` `n`
│ │
│ ╰── resolution error: unresolved `type` `n`
│
4 │ Succ (prev : Nat) : Nat = |n succ# zero#|
│ ┬ ┬ ┬ ┬─
│ ╰────────────────── resolution error: unresolved `function` `=`
│ │ │ │
│ ╰─────────────── resolution error: unresolved `constructor` `n`
│ │ │
│ ╰───────── parse error: unexpected token(s): #
│ │
│ ╰─── parse error: unexpected token(s): # |
5 │ succ# (prev n succ# zero#) zero#
│ ┬ ┬─── ┬ ┬ ┬
│ ╰───────────────────────────── parse error: unexpected token(s): #
│ │ │ │ │
│ ╰────────────────────────── resolution error: unresolved `constructor` `prev`
│ │ │ │
│ ╰─────────────── parse error: unexpected token(s): #
│ │ │
│ ╰───────── parse error: unexpected token(s): #
│ │
│ ╰── parse error: unexpected token(s): #
│
7 │ Zero : Nat = |n succ# zero#|
│ ┬ ┬ ┬ ┬─
│ ╰────────────────── resolution error: unresolved `function` `=`
│ │ │ │
│ ╰─────────────── resolution error: unresolved `constructor` `n`
│ │ │
│ ╰───────── parse error: unexpected token(s): #
│ │
│ ╰─── parse error: unexpected token(s): # |
8 │ zero#
│ ┬
│ ╰── parse error: unexpected token(s): #
│
11 │ Maybe (t : *) = (a : *) -> (t -> a) a -> a
│ ┬── ┬ ┬── ┬─ ┬ ┬─ ┬─
│ ╰──────────────────────────────── parse error: unexpected token(s): : *
│ │ │ │ │ │ │
│ ╰─────────────────────────── parse error: unexpected token(s): =
│ │ │ │ │ │
│ ╰────────────────────── parse error: unexpected token(s): : *
│ │ │ │ │
│ ╰───────────────── parse error: unexpected token(s): - >
│ │ │ │
│ ╰───────────── resolution error: unresolved `constructor` `t`
│ │ │
│ ╰─────────── parse error: unexpected token(s): - >
│ │
│ ╰─── parse error: unexpected token(s): - >
│
13 │ Just (value : a) : Maybe a = Just @ |t just# nothing#|
│ ┬──── ┬ ┬──── ┬ ┬ ┬─── ┬ ┬ ┬───┬ ┬──────┬
│ ╰──────────────────────────────────────────────── resolution error: unresolved `constructor` `value`
│ │ │ │ │ │ │ │ │ │ │ │
│ ╰────────────────────────────────────────── parse error: unexpected token(s): :
│ │ │ │ │ │ │ │ │ │ │
│ ╰─────────────────────────────────── resolution error: unresolved `type` `Maybe`
│ │ │ │ │ │ │ │ │ │
│ ╰───────────────────────────── resolution error: unresolved `type` `a`
│ │ │ │ │ │ │ │ │
│ ╰─────────────────────────── resolution error: unresolved `function` `=`
│ │ │ │ │ │ │ │
│ ╰───────────────────────── resolution error: unresolved `type` `Just`
│ │ │ │ │ │ │
│ ╰──────────────────── parse error: unexpected token(s): @
│ │ │ │ │ │
│ ╰───────────────── resolution error: unresolved `type` `t`
│ │ │ │ │
│ ╰─────────────── resolution error: unresolved `type` `just`
│ │ │ │
│ ╰─────────── parse error: unexpected token(s): #
│ │ │
│ ╰───────── resolution error: unresolved `type` `nothing`
│ │
│ ╰── parse error: unexpected token(s): #
14 │ just# value
│ ┬───┬ ┬────
│ ╰──────────── resolution error: unresolved `type` `just`
│ │ │
│ ╰──────── parse error: unexpected token(s): #
│ │
│ ╰────── resolution error: unresolved `type` `value`
│
16 │ Nothing : Maybe a = Nothing @ |t just# nothing#|
│ ┬──── ┬ ┬ ┬────── ┬ ┬┬ ┬───┬ ┬──────┬┬
│ ╰─────────────────────────────────────── resolution error: unresolved `type` `Maybe`
│ │ │ │ │ ││ │ │ │ ││
│ ╰───────────────────────────────── resolution error: unresolved `type` `a`
│ │ │ │ ││ │ │ │ ││
│ ╰─────────────────────────────── resolution error: unresolved `function` `=`
│ │ │ ││ │ │ │ ││
│ ╰───────────────────────────── resolution error: unresolved `type` `Nothing`
│ │ ││ │ │ │ ││
│ ╰───────────────────── parse error: unexpected token(s): @
│ ││ │ │ │ ││
│ ╰─────────────────── resolution error: unresolved `function` `|`
│ │ │ │ │ ││
│ ╰────────────────── resolution error: unresolved `type` `t`
│ │ │ │ ││
│ ╰──────────────── resolution error: unresolved `type` `just`
│ │ │ ││
│ ╰──────────── parse error: unexpected token(s): #
│ │ ││
│ ╰────────── resolution error: unresolved `type` `nothing`
│ ││
│ ╰─── parse error: unexpected token(s): #
│ │
│ ╰── resolution error: unresolved `function` `|`
17 │ nothing#
│ ┬──────┬
│ ╰───────── resolution error: unresolved `type` `nothing`
│ │
│ ╰── parse error: unexpected token(s): #
│
19 │ Maybe.unwrap (maybe : Maybe a) : a =
│ ┬──── ┬ ┬ ┬
│ ╰─────────────── resolution error: unresolved `type` `Maybe`
│ │ │ │
│ ╰───────── resolution error: unresolved `type` `a`
│ │ │
│ ╰──── resolution error: unresolved `type` `a`
│ │
│ ╰── resolution error: unresolved `function` `=`
20 │ maybe // match maybe with
│ ┬──── │
│ ╰─────────────────────────── resolution error: unresolved `type` `maybe`
│ │
│ ╰─ parse error: (missing simple_identifier)
21 │ (|value| value) // Just a => a
│ │ ┬──── ┬────
│ ╰─────────────────── parse error: (missing simple_identifier)
│ │ │
│ ╰───────────── resolution error: unresolved `type` `value`
│ │
│ ╰────── resolution error: unresolved `type` `value`
────╯
34 changes: 7 additions & 27 deletions sol-driver/tests/mod.rs
View file
Original file line number Diff line number Diff line change
@@ -1,12 +1,10 @@
// use sol_diagnostic::Diagnostics;
// use sol_driver::{make_test_suite, suite::*};
// use sol_eval::{hir_eval, stack::Stack};
// use sol_hir_lowering::hir_lower;
// use sol_syntax::parse;
// use sol_tt::Env;
// use sol_typer::table::infer_type_table;
// use sol_vfs::SourceFile;
// use utils::create_package;
use sol_diagnostic::Diagnostics;
use sol_driver::{make_test_suite, suite::*};
use sol_hir_lowering::hir_lower;
use sol_syntax::parse;
use sol_typer::table::infer_type_table;
use sol_vfs::SourceFile;
use utils::create_package;

pub mod utils;

Expand Down Expand Up @@ -37,21 +35,3 @@ make_test_suite! {
Ok(())
}
}

// make_test_suite! {
// tests ("evaluation") {
// eval "eval"
// }
// run |db, source, output| {
// let file = SourceFile::new(&db, "repl".into(), "Repl".into(), source);

// let src = parse(&db, file);
// let local = create_package(&db, src, "local");
// let hir = hir_lower(&db, local, src);
// let value = hir_eval(&db, Stack::default(), Env::default(), hir);

// writeln!(output, "{:#?}", value)?;

// Ok(())
// }
// }

0 comments on commit 19fff4a

Please sign in to comment.