From e83eaae6c346212139123ab33cd18d41ce3615d8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tim=20S=C3=BCberkr=C3=BCb?= Date: Sun, 5 Jan 2025 00:58:30 +0100 Subject: [PATCH] Add pol compile and ir phase to test runner (#433) * Add pol compile and ir phase to test runner * Improve pretty-printing of let in ir * Document Failure --- Cargo.lock | 1 + app/src/cli/compile.rs | 35 + app/src/cli/mod.rs | 4 + lang/backend/src/ir/decls.rs | 8 +- lang/driver/Cargo.toml | 1 + lang/driver/src/database.rs | 41 +- lang/driver/src/paths.rs | 2 + lang/driver/src/result.rs | 3 + test/suites/success/001.ir.expected | 1 + test/suites/success/002.ir.expected | 1 + test/suites/success/003.ir.expected | 0 test/suites/success/004.ir.expected | 0 test/suites/success/005.ir.expected | 6 + test/suites/success/006.ir.expected | 1 + test/suites/success/007.ir.expected | 4 + test/suites/success/008.ir.expected | 1 + test/suites/success/009.ir.expected | 6 + test/suites/success/010.ir.expected | 6 + test/suites/success/011.ir.expected | 6 + test/suites/success/012.ir.expected | 6 + test/suites/success/013.ir.expected | 6 + test/suites/success/014.ir.expected | 11 + test/suites/success/015.ir.expected | 3 + .../suites/success/016-named-args.ir.expected | 10 + test/suites/success/017.ir.expected | 1 + test/suites/success/018.ir.expected | 1 + test/suites/success/019-absurd.ir.expected | 6 + test/suites/success/020-motive.ir.expected | 12 + test/suites/success/021-evalorder.ir.expected | 7 + .../success/022-implicit-list.ir.expected | 1 + test/suites/success/023-comatches.ir.expected | 14 + test/suites/success/024-gadt.ir.expected | 4 + test/suites/success/025-imports.ir.expected | 11 + .../suites/success/026-refinement.ir.expected | 17 + test/suites/success/026-typedhole.ir.expected | 48 ++ test/suites/success/027-colist.ir.expected | 15 + test/suites/success/028-boolrep.ir.expected | 16 + test/suites/success/029-arith.ir.expected | 28 + test/suites/success/030-buffer.ir.expected | 19 + .../success/031-classical-logic.ir.expected | 15 + .../032-expressions-case-study.ir.expected | 25 + test/suites/success/033-setoid.ir.expected | 0 .../success/034-local-matches.ir.expected | 9 + test/suites/success/035-stlc-bool.ir.expected | 712 ++++++++++++++++++ test/suites/success/036-webserver.ir.expected | 47 ++ test/suites/success/037-vect.ir.expected | 23 + test/suites/success/Regr-137.ir.expected | 4 + test/suites/success/Regr-230.ir.expected | 8 + test/suites/success/Regr-230b.ir.expected | 8 + test/suites/success/Regr-250.ir.expected | 4 + test/suites/success/Regr-271.ir.expected | 5 + test/suites/success/Regr-297.ir.expected | 3 + test/suites/success/Regr-341a.ir.expected | 8 + test/suites/success/Regr-341b.ir.expected | 4 + test/suites/success/Regr-341c.ir.expected | 8 + test/suites/success/Regr-403.ir.expected | 7 + test/test-runner/src/phases.rs | 87 ++- test/test-runner/src/runner.rs | 5 +- test/test-runner/src/suites.rs | 20 +- 59 files changed, 1322 insertions(+), 43 deletions(-) create mode 100644 app/src/cli/compile.rs create mode 100644 test/suites/success/001.ir.expected create mode 100644 test/suites/success/002.ir.expected create mode 100644 test/suites/success/003.ir.expected create mode 100644 test/suites/success/004.ir.expected create mode 100644 test/suites/success/005.ir.expected create mode 100644 test/suites/success/006.ir.expected create mode 100644 test/suites/success/007.ir.expected create mode 100644 test/suites/success/008.ir.expected create mode 100644 test/suites/success/009.ir.expected create mode 100644 test/suites/success/010.ir.expected create mode 100644 test/suites/success/011.ir.expected create mode 100644 test/suites/success/012.ir.expected create mode 100644 test/suites/success/013.ir.expected create mode 100644 test/suites/success/014.ir.expected create mode 100644 test/suites/success/015.ir.expected create mode 100644 test/suites/success/016-named-args.ir.expected create mode 100644 test/suites/success/017.ir.expected create mode 100644 test/suites/success/018.ir.expected create mode 100644 test/suites/success/019-absurd.ir.expected create mode 100644 test/suites/success/020-motive.ir.expected create mode 100644 test/suites/success/021-evalorder.ir.expected create mode 100644 test/suites/success/022-implicit-list.ir.expected create mode 100644 test/suites/success/023-comatches.ir.expected create mode 100644 test/suites/success/024-gadt.ir.expected create mode 100644 test/suites/success/025-imports.ir.expected create mode 100644 test/suites/success/026-refinement.ir.expected create mode 100644 test/suites/success/026-typedhole.ir.expected create mode 100644 test/suites/success/027-colist.ir.expected create mode 100644 test/suites/success/028-boolrep.ir.expected create mode 100644 test/suites/success/029-arith.ir.expected create mode 100644 test/suites/success/030-buffer.ir.expected create mode 100644 test/suites/success/031-classical-logic.ir.expected create mode 100644 test/suites/success/032-expressions-case-study.ir.expected create mode 100644 test/suites/success/033-setoid.ir.expected create mode 100644 test/suites/success/034-local-matches.ir.expected create mode 100644 test/suites/success/035-stlc-bool.ir.expected create mode 100644 test/suites/success/036-webserver.ir.expected create mode 100644 test/suites/success/037-vect.ir.expected create mode 100644 test/suites/success/Regr-137.ir.expected create mode 100644 test/suites/success/Regr-230.ir.expected create mode 100644 test/suites/success/Regr-230b.ir.expected create mode 100644 test/suites/success/Regr-250.ir.expected create mode 100644 test/suites/success/Regr-271.ir.expected create mode 100644 test/suites/success/Regr-297.ir.expected create mode 100644 test/suites/success/Regr-341a.ir.expected create mode 100644 test/suites/success/Regr-341b.ir.expected create mode 100644 test/suites/success/Regr-341c.ir.expected create mode 100644 test/suites/success/Regr-403.ir.expected diff --git a/Cargo.lock b/Cargo.lock index ca53ffb766..bdcd45c62e 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -781,6 +781,7 @@ version = "0.1.0" dependencies = [ "ast", "async-trait", + "backend", "codespan", "elaborator", "log", diff --git a/app/src/cli/compile.rs b/app/src/cli/compile.rs new file mode 100644 index 0000000000..fe93a7a9d8 --- /dev/null +++ b/app/src/cli/compile.rs @@ -0,0 +1,35 @@ +use std::fs; +use std::path::{Path, PathBuf}; + +use driver::{Database, IR_PATH}; +use printer::{Print, PrintCfg}; + +#[derive(clap::Args)] +pub struct Args { + #[clap(value_parser, value_name = "FILE")] + filepath: PathBuf, +} + +pub async fn exec(cmd: Args) -> miette::Result<()> { + let mut db = Database::from_path(&cmd.filepath); + let uri = db.resolve_path(&cmd.filepath)?; + let ir = db.ir(&uri).await.map_err(|err| db.pretty_error(&uri, err))?; + + if !Path::new(IR_PATH).exists() { + fs::create_dir_all(IR_PATH).expect("Failed to create IR directory"); + } + + let ir_path = target_path(&cmd.filepath); + let mut file = fs::File::create(&ir_path).expect("Failed to create file"); + let cfg = PrintCfg::default(); + ir.print_io(&cfg, &mut file).expect("Failed to print to file"); + + Ok(()) +} + +fn target_path(filepath: &Path) -> PathBuf { + let mut path = + Path::new(IR_PATH).join(filepath.file_name().unwrap().to_string_lossy().as_ref()); + path.set_extension("ir"); + path +} diff --git a/app/src/cli/mod.rs b/app/src/cli/mod.rs index 91b3d9aec6..0d89e1748b 100644 --- a/app/src/cli/mod.rs +++ b/app/src/cli/mod.rs @@ -2,6 +2,7 @@ use clap::{Parser, Subcommand}; mod check; mod clean; +mod compile; mod doc; mod format; mod gen_completions; @@ -40,6 +41,7 @@ pub fn exec() -> miette::Result<()> { Doc(args) => doc::exec(args).await, Clean => clean::exec().await, GenerateCompletion(args) => gen_completions::exec(args).await, + Compile(args) => compile::exec(args).await, } }; @@ -82,4 +84,6 @@ enum Command { Clean, /// Generate completion scripts for various shells GenerateCompletion(gen_completions::Args), + /// Compile an executable + Compile(compile::Args), } diff --git a/lang/backend/src/ir/decls.rs b/lang/backend/src/ir/decls.rs index f6773526ce..c350a0a992 100644 --- a/lang/backend/src/ir/decls.rs +++ b/lang/backend/src/ir/decls.rs @@ -128,7 +128,13 @@ impl Print for Let { .append(print_params(params, alloc)) .group(); - let body = body.print(cfg, alloc).braces_anno(); + let body = alloc + .line() + .append(body.print(cfg, alloc)) + .nest(cfg.indent) + .append(alloc.line()) + .braces_anno() + .group(); head.append(alloc.space()).append(body) } diff --git a/lang/driver/Cargo.toml b/lang/driver/Cargo.toml index 755d49a2f7..e2c3b6b67e 100644 --- a/lang/driver/Cargo.toml +++ b/lang/driver/Cargo.toml @@ -33,3 +33,4 @@ elaborator = { path = "../elaborator" } printer = { path = "../printer" } parser = { path = "../parser" } transformations = { path = "../transformations" } +backend = { path = "../backend" } diff --git a/lang/driver/src/database.rs b/lang/driver/src/database.rs index be2202806c..bf2369a48e 100644 --- a/lang/driver/src/database.rs +++ b/lang/driver/src/database.rs @@ -1,21 +1,24 @@ -use crate::result::DriverError; -use crate::{cache::*, Error, FileSource}; use std::rc::Rc; use std::sync::Arc; -use crate::dependency_graph::DependencyGraph; +use url::Url; + use ast::Exp; use ast::HashSet; +use backend::ast2ir::traits::ToIR; +use backend::ir; use elaborator::normalizer::normalize::Normalize; use elaborator::{build_type_info_table, ModuleTypeInfoTable, TypeInfoTable}; use lowering::{ModuleSymbolTable, SymbolTable}; use parser::cst; use parser::cst::decls::UseDecl; use transformations::Rename; -use url::Url; +use crate::dependency_graph::DependencyGraph; use crate::fs::*; use crate::info::*; +use crate::result::DriverError; +use crate::{cache::*, Error, FileSource}; use rust_lapper::Lapper; @@ -35,6 +38,8 @@ pub struct Database { pub ust: Cache, Error>>, /// The typechecked AST of a module pub ast: Cache, Error>>, + /// The IR of a module + pub ir: Cache, Error>>, /// The type info table constructed during typechecking pub module_type_info_table: Cache, /// Hover information for spans @@ -247,6 +252,33 @@ impl Database { ast } + // Core API: ir + // + // + + pub async fn ir(&mut self, uri: &Url) -> Result, Error> { + match self.ir.get_unless_stale(uri) { + Some(module) => { + log::debug!("Found ir in cache: {}", uri); + module.clone() + } + None => self.recompute_ir(uri).await, + } + } + + pub async fn recompute_ir(&mut self, uri: &Url) -> Result, Error> { + log::debug!("Recomputing ir for: {}", uri); + + let module = self.ast(uri).await?; + + // Convert to intermediate representation (IR) + let ir = module.to_ir().map(Arc::new).map_err(Error::Backend); + + self.ir.insert(uri.clone(), ir.clone()); + + ir + } + // Core API: info_by_id // // @@ -329,6 +361,7 @@ impl Database { symbol_table: Cache::default(), ust: Cache::default(), ast: Cache::default(), + ir: Cache::default(), module_type_info_table: Cache::default(), info_by_id: Cache::default(), item_by_id: Cache::default(), diff --git a/lang/driver/src/paths.rs b/lang/driver/src/paths.rs index 52035105ca..f4a1fea857 100644 --- a/lang/driver/src/paths.rs +++ b/lang/driver/src/paths.rs @@ -1,5 +1,7 @@ pub const TARGET_PATH: &str = "target_pol/"; +pub const IR_PATH: &str = "target_pol/ir/"; + pub const DOCS_PATH: &str = "target_pol/docs/"; pub const CSS_PATH: &str = "target_pol/docs/style.css"; diff --git a/lang/driver/src/result.rs b/lang/driver/src/result.rs index 55ad0a8ffb..b9b0d5c32e 100644 --- a/lang/driver/src/result.rs +++ b/lang/driver/src/result.rs @@ -4,6 +4,8 @@ use miette::Diagnostic; use thiserror::Error; use url::Url; +use backend::result::BackendError; + #[derive(Error, Diagnostic, Debug, Clone)] #[diagnostic(transparent)] #[error(transparent)] @@ -13,6 +15,7 @@ pub enum Error { Type(#[from] Box), Xfunc(#[from] transformations::result::XfuncError), Driver(#[from] DriverError), + Backend(#[from] BackendError), } #[derive(Error, Debug, Diagnostic, Clone)] diff --git a/test/suites/success/001.ir.expected b/test/suites/success/001.ir.expected new file mode 100644 index 0000000000..b12ccbc92d --- /dev/null +++ b/test/suites/success/001.ir.expected @@ -0,0 +1 @@ +codef Id(a) { .ap(a0, b, x) => x } diff --git a/test/suites/success/002.ir.expected b/test/suites/success/002.ir.expected new file mode 100644 index 0000000000..436cab1a9a --- /dev/null +++ b/test/suites/success/002.ir.expected @@ -0,0 +1 @@ +codef Compose(a, b, c, f, g) { .ap(a', c', x) => g.ap(b, c, f.ap(a, b, x)) } diff --git a/test/suites/success/003.ir.expected b/test/suites/success/003.ir.expected new file mode 100644 index 0000000000..e69de29bb2 diff --git a/test/suites/success/004.ir.expected b/test/suites/success/004.ir.expected new file mode 100644 index 0000000000..e69de29bb2 diff --git a/test/suites/success/005.ir.expected b/test/suites/success/005.ir.expected new file mode 100644 index 0000000000..cedf0d73a6 --- /dev/null +++ b/test/suites/success/005.ir.expected @@ -0,0 +1,6 @@ +def .not { + True => False, + False => True +} + +def .false { Unit => True.not } diff --git a/test/suites/success/006.ir.expected b/test/suites/success/006.ir.expected new file mode 100644 index 0000000000..caf3fa8f61 --- /dev/null +++ b/test/suites/success/006.ir.expected @@ -0,0 +1 @@ +def .foo(a, d) { Unit => d.match { MkD(a0) => MkD(a).match { MkD(x) => MkD(a) } } } diff --git a/test/suites/success/007.ir.expected b/test/suites/success/007.ir.expected new file mode 100644 index 0000000000..6342592cab --- /dev/null +++ b/test/suites/success/007.ir.expected @@ -0,0 +1,4 @@ +def .foo { + CTrue => Z, + CFalse absurd +} diff --git a/test/suites/success/008.ir.expected b/test/suites/success/008.ir.expected new file mode 100644 index 0000000000..1d912eb8e1 --- /dev/null +++ b/test/suites/success/008.ir.expected @@ -0,0 +1 @@ +def .id(a) { Unit => comatch { .ap(_, _, x1) => x1 } } diff --git a/test/suites/success/009.ir.expected b/test/suites/success/009.ir.expected new file mode 100644 index 0000000000..25577c4db7 --- /dev/null +++ b/test/suites/success/009.ir.expected @@ -0,0 +1,6 @@ +def .id { App(e) => App(e) } + +def self.preservation(e2) { + App(e) => + comatch { .ap(_, _, h_eval) => h_eval.match { EBeta(f) => panic!("not yet implemented") } } +} diff --git a/test/suites/success/010.ir.expected b/test/suites/success/010.ir.expected new file mode 100644 index 0000000000..25577c4db7 --- /dev/null +++ b/test/suites/success/010.ir.expected @@ -0,0 +1,6 @@ +def .id { App(e) => App(e) } + +def self.preservation(e2) { + App(e) => + comatch { .ap(_, _, h_eval) => h_eval.match { EBeta(f) => panic!("not yet implemented") } } +} diff --git a/test/suites/success/011.ir.expected b/test/suites/success/011.ir.expected new file mode 100644 index 0000000000..83b6c874f6 --- /dev/null +++ b/test/suites/success/011.ir.expected @@ -0,0 +1,6 @@ +def .foo { + Foo1 => True, + Foo2 absurd, + Foo3 absurd, + Foo4 absurd +} diff --git a/test/suites/success/012.ir.expected b/test/suites/success/012.ir.expected new file mode 100644 index 0000000000..c8f861c2be --- /dev/null +++ b/test/suites/success/012.ir.expected @@ -0,0 +1,6 @@ +codef MyFoo { + .foo1 => True, + .foo2 absurd, + .foo3 absurd, + .foo4 absurd +} diff --git a/test/suites/success/013.ir.expected b/test/suites/success/013.ir.expected new file mode 100644 index 0000000000..53cd60a133 --- /dev/null +++ b/test/suites/success/013.ir.expected @@ -0,0 +1,6 @@ +let add(x, y) { + x.match { + Z => y, + S(x') => panic!("not yet implemented") + } +} diff --git a/test/suites/success/014.ir.expected b/test/suites/success/014.ir.expected new file mode 100644 index 0000000000..556f8e7a80 --- /dev/null +++ b/test/suites/success/014.ir.expected @@ -0,0 +1,11 @@ +def .add(y) { + Z => y, + S(x') => S(x'.add(y)) +} + +def .append'(n, m, ys) { + Cons(n', x, xs) => Cons(n'.add(m), x, xs.append'(n', m, ys)), + Nil => ys +} + +let append(n, m, xs, ys) { xs.append'(n, m, ys) } diff --git a/test/suites/success/015.ir.expected b/test/suites/success/015.ir.expected new file mode 100644 index 0000000000..f1682b6e4b --- /dev/null +++ b/test/suites/success/015.ir.expected @@ -0,0 +1,3 @@ +let transparentTwo { S(S(Z)) } + +let p2 { Refl(, S(S(Z))) } diff --git a/test/suites/success/016-named-args.ir.expected b/test/suites/success/016-named-args.ir.expected new file mode 100644 index 0000000000..94b76276b0 --- /dev/null +++ b/test/suites/success/016-named-args.ir.expected @@ -0,0 +1,10 @@ +def .and(other) { + True => other, + False => False +} + +let example1 { Cons(True, Nil) } + +let example2 { True.and(False) } + +let example3 { None() } diff --git a/test/suites/success/017.ir.expected b/test/suites/success/017.ir.expected new file mode 100644 index 0000000000..cc0eef6632 --- /dev/null +++ b/test/suites/success/017.ir.expected @@ -0,0 +1 @@ +let example1 { MkPair(, , True, False) } diff --git a/test/suites/success/018.ir.expected b/test/suites/success/018.ir.expected new file mode 100644 index 0000000000..b02dfb529a --- /dev/null +++ b/test/suites/success/018.ir.expected @@ -0,0 +1 @@ +let example { None(panic!("not yet implemented")) } diff --git a/test/suites/success/019-absurd.ir.expected b/test/suites/success/019-absurd.ir.expected new file mode 100644 index 0000000000..e4fded6383 --- /dev/null +++ b/test/suites/success/019-absurd.ir.expected @@ -0,0 +1,6 @@ +def .elim_zero(a) { SNotZero(n) absurd } + +def .elim(a) { + Ok(a0, x) => x, + Absurd(x) => x.elim_zero() +} diff --git a/test/suites/success/020-motive.ir.expected b/test/suites/success/020-motive.ir.expected new file mode 100644 index 0000000000..3950709879 --- /dev/null +++ b/test/suites/success/020-motive.ir.expected @@ -0,0 +1,12 @@ +def self.rep { + T => TrueRep, + F => FalseRep +} + +def .example(b) { + Unit => + b.match { + T => TrueRep, + F => FalseRep + } +} diff --git a/test/suites/success/021-evalorder.ir.expected b/test/suites/success/021-evalorder.ir.expected new file mode 100644 index 0000000000..0c1b24ab70 --- /dev/null +++ b/test/suites/success/021-evalorder.ir.expected @@ -0,0 +1,7 @@ +def .diverge { Unit => Unit.diverge } + +def .before { Unit => Ignore(Unit.diverge) } + +def .after { Unit => comatch { .ap(a, b, x) => x } } + +codef Ignore(y) { .ap(a, b, x) => x } diff --git a/test/suites/success/022-implicit-list.ir.expected b/test/suites/success/022-implicit-list.ir.expected new file mode 100644 index 0000000000..a3dc7941fd --- /dev/null +++ b/test/suites/success/022-implicit-list.ir.expected @@ -0,0 +1 @@ +let example { Cons(, Unit, Nil()) } diff --git a/test/suites/success/023-comatches.ir.expected b/test/suites/success/023-comatches.ir.expected new file mode 100644 index 0000000000..f51df9a9c0 --- /dev/null +++ b/test/suites/success/023-comatches.ir.expected @@ -0,0 +1,14 @@ +def .id { Unit => comatch { .pi_elim(x, x0, a) => comatch { .ap(x1, x2, x3) => x3 } } } + +def .const { + Unit => + comatch { + .pi_elim(x, x0, a) => + comatch { + .pi_elim(x1, x2, b) => + comatch { .ap(x3, x4, x5) => comatch { .ap(x6, x7, y) => x5 } } + } + } +} + +codef IdType { .ap(x, x0, a) => } diff --git a/test/suites/success/024-gadt.ir.expected b/test/suites/success/024-gadt.ir.expected new file mode 100644 index 0000000000..92559cd242 --- /dev/null +++ b/test/suites/success/024-gadt.ir.expected @@ -0,0 +1,4 @@ +def .unwrap(a) { + WrapFoo(x) => x, + WrapBar(x) => x +} diff --git a/test/suites/success/025-imports.ir.expected b/test/suites/success/025-imports.ir.expected new file mode 100644 index 0000000000..52e7e11cbd --- /dev/null +++ b/test/suites/success/025-imports.ir.expected @@ -0,0 +1,11 @@ +use "../../../std/data/nat.pol" +use "../../../std/data/bool.pol" + +def .iNeg { + T => F, + F => T +} + +let one { S(Z) } + +let true { T } diff --git a/test/suites/success/026-refinement.ir.expected b/test/suites/success/026-refinement.ir.expected new file mode 100644 index 0000000000..83e76c991c --- /dev/null +++ b/test/suites/success/026-refinement.ir.expected @@ -0,0 +1,17 @@ +def .sym(a, x, y) { Refl(a0, x0) => Refl(a, y) } + +def .subst(a, x, y, p) { Refl(a0, x0) => p } + +def .trans(a, x, y, z, h) { Refl(a0, x0) => h } + +def .cong(a, b, x, y, f) { Refl(a0, x0) => Refl(b, f.ap(a, b, y)) } + +def .not { + True => False, + False => True +} + +def self.not_inverse { + True => Refl(, True), + False => Refl(, False) +} diff --git a/test/suites/success/026-typedhole.ir.expected b/test/suites/success/026-typedhole.ir.expected new file mode 100644 index 0000000000..b53d0f65f6 --- /dev/null +++ b/test/suites/success/026-typedhole.ir.expected @@ -0,0 +1,48 @@ +def .add(y) { + Z => y, + S(x') => S(x'.add(y)) +} + +def .head(n) { + Cons(n', x, xs) => panic!("not yet implemented"), + Nil absurd +} + +def .tail(n) { + Cons(n', x, xs) => panic!("not yet implemented"), + Nil absurd +} + +def .append(n, m, ys) { + Nil => ys, + Cons(n', x, xs) => Cons(n'.add(m), x, xs.append(n', m, ys)) +} + +def .example1 { Unit => Cons(S(Z), Z, Cons(Z, Z, Nil)) } + +def .example2 { Unit => Unit.example1.append(S(S(Z)), S(S(Z)), Unit.example1) } + +def .not { + T => F, + F => T +} + +def .if_then_else(a, then, else) { + T => then, + F => else +} + +codef Zeroes { + .sHead => Z, + .sTail => Zeroes +} + +codef Ones { + .sHead => S(Z), + .sTail => panic!("not yet implemented") +} + +codef Alternate(choose) { + .sHead => choose.if_then_else(, S(panic!("not yet implemented")), Z), + .sTail => Alternate(choose.not) +} diff --git a/test/suites/success/027-colist.ir.expected b/test/suites/success/027-colist.ir.expected new file mode 100644 index 0000000000..06edcf9aff --- /dev/null +++ b/test/suites/success/027-colist.ir.expected @@ -0,0 +1,15 @@ +def .pred { + Z => Z, + S(n) => n, + Omega => Omega +} + +codef CountUp(from) { + .head(n, p) => from, + .tail(n) => CountUp(S(from)) +} + +codef TakeN(n, s) { + .head(n', p) => s.head(Omega, OmegaNotZero), + .tail(n') => TakeN(n.pred, s.tail(Omega)) +} diff --git a/test/suites/success/028-boolrep.ir.expected b/test/suites/success/028-boolrep.ir.expected new file mode 100644 index 0000000000..e86d92f2de --- /dev/null +++ b/test/suites/success/028-boolrep.ir.expected @@ -0,0 +1,16 @@ +use "../../../std/data/bool.pol" + +def .extract(x) { + TrueRep => T, + FalseRep => F +} + +def .flipRep(x, rep) { + Unit => + rep.match { + TrueRep => FalseRep, + FalseRep => TrueRep + } +} + +def .example { Unit => Unit.flipRep(T, TrueRep).extract(F) } diff --git a/test/suites/success/029-arith.ir.expected b/test/suites/success/029-arith.ir.expected new file mode 100644 index 0000000000..bd6d58d03a --- /dev/null +++ b/test/suites/success/029-arith.ir.expected @@ -0,0 +1,28 @@ +def .add(y) { + Z => y, + S(x') => S(x'.add(y)) +} + +def .and(y) { + T => y, + F => F +} + +def .preserves(e1, e2, t, h1) { + EAddCongL(lhs, lhs', rhs, h_lhs) => panic!("not yet implemented"), + EAddCongR(lhs, rhs, rhs', h_rhs) => panic!("not yet implemented"), + EAddRed(n1, n2) => panic!("not yet implemented"), + EIsZeroCong(e, e', h_e) => panic!("not yet implemented"), + EAndCongL(lhs, lhs', rhs, h_lhs) => panic!("not yet implemented"), + EAndCongR(lhs, rhs, rhs', h_rhs) => panic!("not yet implemented"), + EAndRed(b1, b2) => panic!("not yet implemented") +} + +let example { And(IsZero(Add(Num(Z), Num(Z))), Boo(T)) } + +let example_has_type { + TAnd(IsZero(Add(Num(Z), Num(Z))), + Boo(T), + TIsZero(Add(Num(Z), Num(Z)), TAdd(Num(Z), Num(Z), TNum(Z), TNum(Z))), + TBoo(T)) +} diff --git a/test/suites/success/030-buffer.ir.expected b/test/suites/success/030-buffer.ir.expected new file mode 100644 index 0000000000..91d0f3d7b9 --- /dev/null +++ b/test/suites/success/030-buffer.ir.expected @@ -0,0 +1,19 @@ +def .head(n) { + Cons(n', x, xs) => x, + Nil absurd +} + +def .tail(n) { + Cons(n', x, xs) => xs, + Nil absurd +} + +codef Empty { .read(n) absurd } + +codef FromVec(n, xs) { + .read(n') => + comatch { + .proj1(x, x0) => xs.head(n'), + .proj2(x, x0) => FromVec(n', xs.tail(n')) + } +} diff --git a/test/suites/success/031-classical-logic.ir.expected b/test/suites/success/031-classical-logic.ir.expected new file mode 100644 index 0000000000..fda8d791dc --- /dev/null +++ b/test/suites/success/031-classical-logic.ir.expected @@ -0,0 +1,15 @@ +def .contra(a, prf, ref) { Unit => ref.ret(a, prf) } + +def .lem(a) { + Unit => + comatch { + .given(x, k) => + Unit.contra(, + Right(a, + , + comatch { + .ret(x0, x1) => Unit.contra(, Left(a, , x1), k) + }), + k) + } +} diff --git a/test/suites/success/032-expressions-case-study.ir.expected b/test/suites/success/032-expressions-case-study.ir.expected new file mode 100644 index 0000000000..3b54d7b366 --- /dev/null +++ b/test/suites/success/032-expressions-case-study.ir.expected @@ -0,0 +1,25 @@ +def .pres(e, ty) { + TTrue => comatch { .preservationStep(e1, e2, ty0, s) => s.d_step1(e2) }, + TFalse => comatch { .preservationStep(e1, e2, ty0, s) => s.d_step3(e2) }, + TIte(e1, e2, e3, ty0, t1, t2, t3) => + comatch { .preservationStep(e4, e5, ty1, s) => s.d_step5(e1, e2, e3, e5, ty, t1, t2, t3) } +} + +codef StIteT(e1, e2) { + .d_step3(e3) absurd, + .d_step1(e3) absurd, + .d_step5(e3, e4, e5, e6, ty, t1, t2, t3) => t2 +} + +codef StIteF(e1, e2) { + .d_step3(e3) absurd, + .d_step1(e3) absurd, + .d_step5(e3, e4, e5, e6, ty, t1, t2, t3) => t3 +} + +codef StIte(e1, e2, e3, e4, s) { + .d_step1(e5) absurd, + .d_step3(e5) absurd, + .d_step5(e1', e2', e3', e5', ty, t1, t2, t3) => + TIte(e2, e3, e4, ty, t1.pres(e1, TyBool).preservationStep(e1, e2, TyBool, s), t2, t3) +} diff --git a/test/suites/success/033-setoid.ir.expected b/test/suites/success/033-setoid.ir.expected new file mode 100644 index 0000000000..e69de29bb2 diff --git a/test/suites/success/034-local-matches.ir.expected b/test/suites/success/034-local-matches.ir.expected new file mode 100644 index 0000000000..45c7976793 --- /dev/null +++ b/test/suites/success/034-local-matches.ir.expected @@ -0,0 +1,9 @@ +def .top_is_zero(n) { + Unit => + n.match { + Z => T, + S(n0) => F + } +} + +def .top_id(a) { Unit => comatch { .ap(a0, b, x) => x } } diff --git a/test/suites/success/035-stlc-bool.ir.expected b/test/suites/success/035-stlc-bool.ir.expected new file mode 100644 index 0000000000..ad7248fa51 --- /dev/null +++ b/test/suites/success/035-stlc-bool.ir.expected @@ -0,0 +1,712 @@ +def .append(other) { + Nil => other, + Cons(t, ts) => Cons(t, ts.append(other)) +} + +def .len { + Nil => Z, + Cons(x, ts) => S(ts.len) +} + +def .subst(v, by) { + Var(x) => x.cmp(v).subst_result(x, by), + Lam(e) => Lam(e.subst(S(v), by)), + App(e1, e2) => App(e1.subst(v, by), e2.subst(v, by)), + Lit(b) => Lit(b), + If(cond, then, else) => If(cond.subst(v, by), then.subst(v, by), else.subst(v, by)) +} + +def .subst_result(x, by) { + LT => Var(x), + EQ => by, + GT => Var(x.pred) +} + +def e.progress(t) { + Var(x) => + comatch { + .ap(_, _, h_t) => + h_t.match { + TVar(x2, x3, x4, elem) => elem.empty_absurd(x, t).elim_bot(), + TLam(x2, x3, x4, x5, x6) absurd, + TApp(x2, x3, x4, x5, x6, x7, x8) absurd, + TLit(x2, x3) absurd, + TIf(x2, x3, x4, x5, x6, x7, x8, x9) absurd + } + }, + Lam(e) => comatch { .ap(_, _, x1) => PVal(Lam(e), VLam(e)) }, + App(e1, e2) => + comatch { + .ap(_, _, h_t) => + h_t.match { + TVar(x1, x2, x3, x4) absurd, + TLam(x1, x2, x3, x4, x5) absurd, + TLit(x1, x2) absurd, + TIf(x1, x2, x3, x4, x5, x6, x7, x8) absurd, + TApp(x1, t1, t2, x2, x3, e1_t, e2_t) => + e1.progress(FunT(t1, t)).ap(, , e1_t).match { + PStep(x4, e1', e1_eval_e1') => + PStep(App(e1, e2), + App(e1', e2), + ECongApp1(e1, e1', e1_eval_e1', e2)), + PVal(x4, is_val) => + is_val.match { + VLit(x5) => + e1_t.match { + TVar(x6, x7, x8, x9) absurd, + TLam(x6, x7, x8, x9, x10) absurd, + TApp(x6, x7, x8, x9, x10, x11, x12) absurd, + TIf(x6, x7, x8, x9, x10, x11, x12, x13) absurd, + TLit(x6, x7) absurd + }, + VLam(e) => PStep(App(Lam(e), e2), e.subst(Z, e2), EBeta(e, e2)) + } + } + } + }, + Lit(b) => comatch { .ap(_, _, x1) => PVal(Lit(b), VLit(b)) }, + If(cond, then, else) => + comatch { + .ap(_, _, h_e) => + h_e.match { + TVar(x1, x2, x3, x4) absurd, + TLam(x1, x2, x3, x4, x5) absurd, + TApp(x1, x2, x3, x4, x5, x6, x7) absurd, + TLit(x1, x2) absurd, + TIf(x1, x2, x3, x4, x5, h_cond, h_then, h_else) => + cond.progress(BooT).ap(, , h_cond).match { + PVal(x6, h_val) => + h_val.match { + VLam(x7) => + h_cond.match { + TVar(x8, x9, x10, x11) absurd, + TLam(x8, x9, x10, x11, x12) absurd, + TApp(x8, x9, x10, x11, x12, x13, x14) absurd, + TIf(x8, x9, x10, x11, x12, x13, x14, x15) absurd, + TLit(x8, x9) absurd + }, + VLit(b) => + b.match { + True => + PStep(If(Lit(True), then, else), + then, + EIfTrue(then, else)), + False => + PStep(If(Lit(False), then, else), + else, + EIfFalse(then, else)) + } + }, + PStep(x6, cond', h_eval) => + PStep(If(cond, then, else), + If(cond', then, else), + ECongIf(cond, cond', then, else, h_eval)) + } + } + } +} + +def e1.preservation(e2, t) { + Var(x) => + comatch { + .ap(_, _, h_t) => + comatch { + .ap(_, _, h_eval) => + h_eval.match { + EBeta(x4, x5) absurd, + ECongApp1(x4, x5, x6, x7) absurd, + ECongApp2(x4, x5, x6, x7) absurd, + ECongIf(x4, x5, x6, x7, x8) absurd, + EIfTrue(x4, x5) absurd, + EIfFalse(x4, x5) absurd + } + } + }, + Lam(x) => + comatch { + .ap(_, _, h_t) => + comatch { + .ap(_, _, h_eval) => + h_eval.match { + EBeta(x4, x5) absurd, + ECongApp1(x4, x5, x6, x7) absurd, + ECongApp2(x4, x5, x6, x7) absurd, + ECongIf(x4, x5, x6, x7, x8) absurd, + EIfTrue(x4, x5) absurd, + EIfFalse(x4, x5) absurd + } + } + }, + App(e1, e3) => + comatch { + .ap(_, _, h_t) => + h_t.match { + TVar(x1, x2, x3, x4) absurd, + TLam(x1, x2, x3, x4, x5) absurd, + TLit(x1, x2) absurd, + TIf(x1, x2, x3, x4, x5, x6, x7, x8) absurd, + TApp(x1, t1, t2, x2, x3, h_lam, h_e2) => + comatch { + .ap(_, _, h_eval) => + h_eval.match { + ECongIf(x6, x7, x8, x9, x10) absurd, + EIfTrue(x6, x7) absurd, + EIfFalse(x6, x7) absurd, + ECongApp1(x6, e1', h, x7) => + TApp(Nil, + t1, + t, + e1', + e3, + e1.preservation(e1', FunT(t1, t)) + .ap(, , h_lam) + .ap(, , h), + h_e2), + ECongApp2(x6, x7, e2', h) => + TApp(Nil, + t1, + t, + e1, + e2', + h_lam, + e3.preservation(e2', t1) + .ap(, , h_e2) + .ap(, , h)), + EBeta(e4, x6) => + h_lam.match { + TVar(x7, x8, x9, x10) absurd, + TApp(x7, x8, x9, x10, x11, x12, x13) absurd, + TLit(x7, x8) absurd, + TIf(x7, x8, x9, x10, x11, x12, x13, x14) absurd, + TLam(x7, x8, x9, x10, h_e1) => + e4.subst_lemma(Nil, Nil, t1, t, e3) + .ap(, , h_e1) + .ap(, , h_e2) + } + } + } + } + }, + Lit(b) => + comatch { + .ap(_, _, h_t) => + comatch { + .ap(_, _, h_eval) => + h_eval.match { + EBeta(x3, x4) absurd, + ECongApp1(x3, x4, x5, x6) absurd, + ECongApp2(x3, x4, x5, x6) absurd, + ECongIf(x3, x4, x5, x6, x7) absurd, + EIfTrue(x3, x4) absurd, + EIfFalse(x3, x4) absurd + } + } + }, + If(cond, then, else) => + comatch { + .ap(_, _, h_t) => + comatch { + .ap(_, _, h_eval) => + h_t.match { + TVar(x3, x4, x5, x6) absurd, + TApp(x3, x4, x5, x6, x7, x8, x9) absurd, + TLit(x3, x4) absurd, + TLam(x3, x4, x5, x6, x7) absurd, + TIf(x3, x4, x5, x6, t0, h_cond, h_then, h_else) => + h_eval.match { + EBeta(x7, x8) absurd, + ECongApp1(x7, x8, x9, x10) absurd, + ECongApp2(x7, x8, x9, x10) absurd, + ECongIf(x7, cond', x8, x9, h_eval_cond) => + TIf(Nil, + cond', + then, + else, + t, + cond.preservation(cond', BooT) + .ap(, , h_cond) + .ap(, , h_eval_cond), + h_then, + h_else), + EIfTrue(x7, x8) => h_then, + EIfFalse(x7, x8) => h_else + } + } + } + } +} + +def e.subst_lemma(ctx1, ctx2, t1, t2, by_e) { + Var(x) => + comatch { + .ap(_, _, h_e) => + comatch { + .ap(_, _, h_by) => + h_e.match { + TLam(x4, x5, x6, x7, x8) absurd, + TApp(x4, x5, x6, x7, x8, x9, x10) absurd, + TLit(x4, x5) absurd, + TIf(x4, x5, x6, x7, x8, x9, x10, x11) absurd, + TVar(x4, x5, x6, h_elem) => + x.cmp_reflect(ctx1.len).match { + IsLT(x7, x8, h_eq_lt, h_lt) => + h_eq_lt.transport(, + LT, + x.cmp(ctx1.len), + comatch { .ap(x9, x10, cmp) => }, + ctx2.weaken_append(ctx1, Var(x), t2) + .ap(, + , + TVar(ctx1, + x, + t2, + ctx1.elem_append_first(Cons(t1, + ctx2), + t2, + x) + .ap(, , h_lt) + .ap(, + , + h_elem)))), + IsEQ(x7, x8, h_eq_eq, h_eq) => + h_eq_eq.transport(, + EQ, + x.cmp(ctx1.len), + comatch { .ap(x9, x10, cmp) => }, + ctx1.append(ctx2) + .weaken_append(Nil, by_e, t2) + .ap(, + , + ctx1.ctx_lookup(ctx2, t2, t1) + .ap(, + , + h_eq.transport(, + x, + ctx1.len, + comatch { + .ap(x9, x10, x11) => + + }, + h_elem)) + .transport(, + t1, + t2, + comatch { + .ap(x9, x10, t) => + + }, + h_by))), + IsGT(x7, x8, h_eq_gt, h_gt) => + h_eq_gt.transport(, + GT, + x.cmp(ctx1.len), + comatch { .ap(x9, x10, cmp) => }, + TVar(ctx1.append(ctx2), + x.pred, + t2, + ctx1.elem_append_pred(ctx2, + t2, + t1, + x) + .ap(, , h_gt) + .ap(, , h_elem))) + } + } + } + }, + Lam(body) => + comatch { + .ap(_, _, h_e) => + comatch { + .ap(_, _, h_by) => + h_e.match { + TVar(x3, x4, x5, x6) absurd, + TApp(x3, x4, x5, x6, x7, x8, x9) absurd, + TLit(x3, x4) absurd, + TIf(x3, x4, x5, x6, x7, x8, x9, x10) absurd, + TLam(x3, a, b, x4, h_body) => + TLam(ctx1.append(ctx2), + a, + b, + body.subst(S(ctx1.len), by_e), + body.subst_lemma(Cons(a, ctx1), ctx2, t1, b, by_e) + .ap(, , h_body) + .ap(, , h_by)) + } + } + }, + App(e1, e2) => + comatch { + .ap(_, _, h_e) => + comatch { + .ap(_, _, h_by) => + h_e.match { + TVar(x3, x4, x5, x6) absurd, + TLam(x3, x4, x5, x6, x7) absurd, + TLit(x3, x4) absurd, + TIf(x3, x4, x5, x6, x7, x8, x9, x10) absurd, + TApp(x3, a, b, x4, x5, h_e1, h_e2) => + TApp(ctx1.append(ctx2), + a, + t2, + e1.subst(ctx1.len, by_e), + e2.subst(ctx1.len, by_e), + e1.subst_lemma(ctx1, ctx2, t1, FunT(a, t2), by_e) + .ap(, , h_e1) + .ap(, , h_by), + e2.subst_lemma(ctx1, ctx2, t1, a, by_e) + .ap(, , h_e2) + .ap(, , h_by)) + } + } + }, + Lit(b) => + comatch { + .ap(_, _, h_e) => + comatch { + .ap(_, _, h_by) => + h_e.match { + TVar(x3, x4, x5, x6) absurd, + TLam(x3, x4, x5, x6, x7) absurd, + TApp(x3, x4, x5, x6, x7, x8, x9) absurd, + TIf(x3, x4, x5, x6, x7, x8, x9, x10) absurd, + TLit(x3, x4) => TLit(ctx1.append(ctx2), b) + } + } + }, + If(cond, then, else) => + comatch { + .ap(_, _, h_e) => + comatch { + .ap(_, _, h_by) => + h_e.match { + TVar(x3, x4, x5, x6) absurd, + TLam(x3, x4, x5, x6, x7) absurd, + TApp(x3, x4, x5, x6, x7, x8, x9) absurd, + TLit(x3, x4) absurd, + TIf(x3, x4, x5, x6, t, h_cond, h_then, h_else) => + TIf(ctx1.append(ctx2), + cond.subst(ctx1.len, by_e), + then.subst(ctx1.len, by_e), + else.subst(ctx1.len, by_e), + t2, + cond.subst_lemma(ctx1, ctx2, t1, BooT, by_e) + .ap(, , h_cond) + .ap(, , h_by), + then.subst_lemma(ctx1, ctx2, t1, t2, by_e) + .ap(, , h_then) + .ap(, , h_by), + else.subst_lemma(ctx1, ctx2, t1, t2, by_e) + .ap(, , h_else) + .ap(, , h_by)) + } + } + } +} + +def ctx2.weaken_append(ctx1, e, t) { + Nil => + comatch { + .ap(_, _, h_e) => + ctx1.append_nil + .transport(, + ctx1, + ctx1.append(Nil), + comatch { .ap(x1, x2, ctx) => }, + h_e) + }, + Cons(t', ts) => + comatch { + .ap(_, _, h_e) => + ctx1.append_assoc(Cons(t', Nil), ts) + .transport(, + ctx1.append(Cons(t', Nil)).append(ts), + ctx1.append(Cons(t', ts)), + comatch { .ap(x1, x2, ctx) => }, + ts.weaken_append(ctx1.append(Cons(t', Nil)), e, t) + .ap(, + , + e.weaken_cons(ctx1, t', t).ap(, , h_e))) + } +} + +def e.weaken_cons(ctx, t1, t2) { + Var(x) => + comatch { + .ap(_, _, h_e) => + h_e.match { + TLam(x2, x3, x4, x5, x6) absurd, + TApp(x2, x3, x4, x5, x6, x7, x8) absurd, + TLit(x2, x3) absurd, + TIf(x2, x3, x4, x5, x6, x7, x8, x9) absurd, + TVar(x2, x3, x4, h_elem) => + TVar(ctx.append(Cons(t1, Nil)), x, t2, h_elem.elem_append(x, t1, t2, ctx)) + } + }, + Lam(e) => + comatch { + .ap(_, _, h_e) => + h_e.match { + TVar(x1, x2, x3, x4) absurd, + TApp(x1, x2, x3, x4, x5, x6, x7) absurd, + TLit(x1, x2) absurd, + TIf(x1, x2, x3, x4, x5, x6, x7, x8) absurd, + TLam(x1, a, b, x2, h_e0) => + TLam(ctx.append(Cons(t1, Nil)), + a, + b, + e, + e.weaken_cons(Cons(a, ctx), t1, b).ap(, , h_e0)) + } + }, + App(e1, e2) => + comatch { + .ap(_, _, h_e) => + h_e.match { + TVar(x1, x2, x3, x4) absurd, + TLam(x1, x2, x3, x4, x5) absurd, + TLit(x1, x2) absurd, + TIf(x1, x2, x3, x4, x5, x6, x7, x8) absurd, + TApp(x1, a, b, x2, x3, h_e1, h_e2) => + TApp(ctx.append(Cons(t1, Nil)), + a, + t2, + e1, + e2, + e1.weaken_cons(ctx, t1, FunT(a, t2)).ap(, , h_e1), + e2.weaken_cons(ctx, t1, a).ap(, , h_e2)) + } + }, + Lit(b) => + comatch { + .ap(_, _, h_e) => + h_e.match { + TVar(x1, x2, x3, x4) absurd, + TLam(x1, x2, x3, x4, x5) absurd, + TApp(x1, x2, x3, x4, x5, x6, x7) absurd, + TIf(x1, x2, x3, x4, x5, x6, x7, x8) absurd, + TLit(x1, x2) => TLit(ctx.append(Cons(t1, Nil)), b) + } + }, + If(cond, then, else) => + comatch { + .ap(_, _, h_e) => + h_e.match { + TVar(x1, x2, x3, x4) absurd, + TLam(x1, x2, x3, x4, x5) absurd, + TApp(x1, x2, x3, x4, x5, x6, x7) absurd, + TLit(x1, x2) absurd, + TIf(x1, x2, x3, x4, t, h_cond, h_then, h_else) => + TIf(ctx.append(Cons(t1, Nil)), + cond, + then, + else, + t2, + cond.weaken_cons(ctx, t1, BooT).ap(, , h_cond), + then.weaken_cons(ctx, t1, t2).ap(, , h_then), + else.weaken_cons(ctx, t1, t2).ap(, , h_else)) + } + } +} + +def .elem_append(n, t1, t2, ctx) { + Here(t, ts) => Here(t2, ts.append(Cons(t1, Nil))), + There(n0, x, t', ts, h) => + There(n0, t2, t', ts.append(Cons(t1, Nil)), h.elem_append(n0, t1, t2, ts)) +} + +def ctx1.append_assoc(ctx2, ctx3) { + Nil => Refl(, ctx2.append(ctx3)), + Cons(x, xs) => + xs.append_assoc(ctx2, ctx3) + .cong(, + , + xs.append(ctx2).append(ctx3), + xs.append(ctx2.append(ctx3)), + comatch { .ap(x0, x1, xs0) => Cons(x, xs0) }) +} + +def ctx.append_nil { + Nil => Refl(, Nil), + Cons(t, ts) => ts.append_nil.eq_cons(ts, ts.append(Nil), t) +} + +def .empty_absurd(x, t) { + Here(x0, x1) absurd, + There(x0, x1, x2, x3, x4) absurd +} + +def .elem_unique(ctx, t1, t2) { + Here(x, x0) => Refl(, t2), + There(x, x0, x1, x2, x3) absurd +} + +def ctx1.ctx_lookup(ctx2, t1, t2) { + Nil => comatch { .ap(_, _, h) => h.elem_unique(ctx2, t1, t2) }, + Cons(t, ts) => + comatch { + .ap(_, _, h) => + h.match { + Here(x1, x2) absurd, + There(x1, x2, x3, x4, h0) => ts.ctx_lookup(ctx2, t1, t2).ap(, , h0) + } + } +} + +def ctx1.elem_append_first(ctx2, t, x) { + Nil => + comatch { + .ap(_, _, h_lt) => + comatch { + .ap(_, _, h_elem) => + h_lt.match { + LERefl(x4) absurd, + LESucc(x4, x5, x6) absurd + } + } + }, + Cons(t', ts) => + comatch { + .ap(_, _, h_lt) => + comatch { + .ap(_, _, h_elem) => + h_elem.match { + Here(x4, x5) => Here(t', ts), + There(x', x4, x5, x6, h) => + There(x', + t, + t', + ts, + ts.elem_append_first(ctx2, t, x') + .ap(, , h_lt.le_unsucc(S(), ts.len)) + .ap(, , h)) + } + } + } +} + +def ctx1.elem_append_pred(ctx2, t1, t2, x) { + Nil => + comatch { + .ap(_, _, h_gt) => + comatch { + .ap(_, _, h_elem) => + h_elem.match { + Here(x4, x5) => + h_gt.match { + LERefl(x6) absurd, + LESucc(x6, x7, x8) absurd + }, + There(x4, x5, x6, x7, h) => h + } + } + }, + Cons(t, ts) => + comatch { + .ap(_, _, h_gt) => + comatch { + .ap(_, _, h_elem) => + h_elem.match { + Here(x4, x5) => + h_gt.match { + LERefl(x6) absurd, + LESucc(x6, x7, x8) absurd + }, + There(x', x4, x5, x6, h) => + h_gt.le_unsucc(S(ts.len), x') + .s_pred(ts.len, x') + .transport(, + S(x'.pred), + x', + comatch { .ap(x7, x8, x9) => }, + There(x'.pred, + t1, + t, + ts.append(ctx2), + ts.elem_append_pred(ctx2, t1, t2, x') + .ap(, + , + h_gt.le_unsucc(S(ts.len), x')) + .ap(, , h))) + } + } + } +} + +def .elim_bot(a) { } + +def .sym(a, x, y) { Refl(a0, x0) => Refl(a, y) } + +def .transport(a, x, y, p, prf) { Refl(a0, x0) => prf } + +def .cong(a, b, x, y, f) { Refl(a0, x0) => Refl(b, f.ap(a, b, y)) } + +def .eq_s(x, y) { Refl(x0, x1) => Refl(, S(y)) } + +def .eq_cons(xs, ys, t) { Refl(x, x0) => Refl(, Cons(t, ys)) } + +def .pred { + Z => Z, + S(x) => x +} + +def .cmp(y) { + Z => + y.match { + Z => EQ, + S(x) => LT + }, + S(x) => + y.match { + Z => GT, + S(y0) => x.cmp(y0) + } +} + +def x.cmp_reflect(y) { + Z => + y.match { + Z => IsEQ(Z, Z, Refl(, EQ), Refl(, Z)), + S(y0) => IsLT(Z, S(y0), Refl(, LT), y0.z_le.le_succ(Z, y0)) + }, + S(x) => + y.match { + Z => IsGT(S(x), Z, Refl(, GT), x.z_le.le_succ(Z, x)), + S(y0) => + x.cmp_reflect(y0).match { + IsLT(x0, x1, h1, h2) => IsLT(S(x), S(y0), h1, h2.le_succ(S(x), y0)), + IsEQ(x0, x1, h1, h2) => IsEQ(S(x), S(y0), h1, h2.eq_s(x, y0)), + IsGT(x0, x1, h1, h2) => IsGT(S(x), S(y0), h1, h2.le_succ(S(y0), x)) + } + } +} + +def x.z_le { + Z => LERefl(Z), + S(x) => LESucc(Z, x, x.z_le) +} + +def .le_succ(x, y) { + LERefl(x0) => LERefl(S(y)), + LESucc(x0, y0, h) => LESucc(S(x), S(y0), h.le_succ(x, y0)) +} + +def .le_unsucc(x, y) { + LERefl(x0) => LERefl(y), + LESucc(x0, x1, h) => h.s_le(x, y) +} + +def .s_le(x, y) { + LERefl(x0) => LESucc(x, x, LERefl(x)), + LESucc(x0, y', h) => LESucc(x, y', h.s_le(x, y')) +} + +def .s_pred(x, y) { + LERefl(x0) => Refl(, S(x)), + LESucc(x0, y', x1) => Refl(, S()) +} + +def .not { + True => False, + False => True +} diff --git a/test/suites/success/036-webserver.ir.expected b/test/suites/success/036-webserver.ir.expected new file mode 100644 index 0000000000..b0940af3a5 --- /dev/null +++ b/test/suites/success/036-webserver.ir.expected @@ -0,0 +1,47 @@ +def .cong_pair(t1, t2, a, b, c) { Refl(x, x0) => Refl(, Pair(t1, t2, b, c)) } + +codef Pair(a, b, x, y) { + .fst(a0, b0) => x, + .snd(a0, b0) => y +} + +codef MkUtils { + .put_twice(n, route, state) => + route.put(n).ap(, , route.put(n).ap(, , state).fst(, )) +} + +codef Index { + .requiresLogin => F, + .post => + comatch { + .ap(_, _, state) => + comatch { + .fst(a, b) => state, + .snd(a, b) => Forbidden + } + }, + .get => comatch { .ap(_, _, state) => Return(state.counter(F)) }, + .put(n) => comatch { .ap(_, _, state) => Pair(, , state, Forbidden) }, + .put_idempotent(n) => + comatch { .dap(x, x0, state) => Refl(, Pair(, , state, Forbidden)) } +} + +codef Admin { + .requiresLogin => T, + .post => + comatch { + .ap(_, _, state) => + comatch { + .fst(a, b) => state.increment, + .snd(a, b) => Return(state.increment.counter(T)) + } + }, + .get => comatch { .ap(_, _, state) => Return(state.counter(T)) }, + .put(n) => comatch { .ap(_, _, state) => Pair(, , state.set(n), Return(n)) }, + .put_idempotent(n) => + comatch { + .dap(x, x0, state) => + state.set_idempotent(T, n) + .cong_pair(, , state.set(n), state.set(n).set(n), Return(n)) + } +} diff --git a/test/suites/success/037-vect.ir.expected b/test/suites/success/037-vect.ir.expected new file mode 100644 index 0000000000..186fb07ca5 --- /dev/null +++ b/test/suites/success/037-vect.ir.expected @@ -0,0 +1,23 @@ +def .add(y) { + Z => y, + S(x') => S(x'.add(y)) +} + +def .head(n) { + Cons(n', x, xs) => x, + Nil absurd +} + +def .tail(n) { + Cons(n', x, xs) => xs, + Nil absurd +} + +def .append(n, m, ys) { + Nil => ys, + Cons(n', x, xs) => Cons(n'.add(m), x, xs.append(n', m, ys)) +} + +def .example1 { Unit => Cons(S(Z), Z, Cons(Z, Z, Nil)) } + +let main { Unit.example1.append(S(S(Z)), S(S(Z)), Unit.example1) } diff --git a/test/suites/success/Regr-137.ir.expected b/test/suites/success/Regr-137.ir.expected new file mode 100644 index 0000000000..9728b08932 --- /dev/null +++ b/test/suites/success/Regr-137.ir.expected @@ -0,0 +1,4 @@ +def .ind(P, step) { + True => panic!("not yet implemented"), + False => panic!("not yet implemented") +} diff --git a/test/suites/success/Regr-230.ir.expected b/test/suites/success/Regr-230.ir.expected new file mode 100644 index 0000000000..8e9e79f6d0 --- /dev/null +++ b/test/suites/success/Regr-230.ir.expected @@ -0,0 +1,8 @@ +def .add(m) { + Z => m, + S(n) => S(n.add(m)) +} + +let two { S(S(Z)) } + +let foo { Refl(, two.add(S(S(Z)))) } diff --git a/test/suites/success/Regr-230b.ir.expected b/test/suites/success/Regr-230b.ir.expected new file mode 100644 index 0000000000..8e9e79f6d0 --- /dev/null +++ b/test/suites/success/Regr-230b.ir.expected @@ -0,0 +1,8 @@ +def .add(m) { + Z => m, + S(n) => S(n.add(m)) +} + +let two { S(S(Z)) } + +let foo { Refl(, two.add(S(S(Z)))) } diff --git a/test/suites/success/Regr-250.ir.expected b/test/suites/success/Regr-250.ir.expected new file mode 100644 index 0000000000..6b2a568627 --- /dev/null +++ b/test/suites/success/Regr-250.ir.expected @@ -0,0 +1,4 @@ +codef Unit₋ { + .typeAt₋(x, x0) absurd, + .dataAt₋(x, x0) absurd +} diff --git a/test/suites/success/Regr-271.ir.expected b/test/suites/success/Regr-271.ir.expected new file mode 100644 index 0000000000..c6902935e7 --- /dev/null +++ b/test/suites/success/Regr-271.ir.expected @@ -0,0 +1,5 @@ +codef S(n) { .add(m) => n.add(S(m)) } + +codef Z { .add(m) => m } + +let test { Refl(, S(S(S(S(Z))))) } diff --git a/test/suites/success/Regr-297.ir.expected b/test/suites/success/Regr-297.ir.expected new file mode 100644 index 0000000000..3490c6a3c8 --- /dev/null +++ b/test/suites/success/Regr-297.ir.expected @@ -0,0 +1,3 @@ +codef Id(a) { .ap(x, x0, x1) => x1 } + +let example { Id().ap(, , Unit) } diff --git a/test/suites/success/Regr-341a.ir.expected b/test/suites/success/Regr-341a.ir.expected new file mode 100644 index 0000000000..40e67d7b84 --- /dev/null +++ b/test/suites/success/Regr-341a.ir.expected @@ -0,0 +1,8 @@ +codef F { .ap(x, x0, x1) => } + +let foo(t, x) { panic!("not yet implemented") } + +let T { + foo(F.ap(, , panic!("not yet implemented")), + comatch { .ap(_, _, x1) => F.ap(, , x1) }) +} diff --git a/test/suites/success/Regr-341b.ir.expected b/test/suites/success/Regr-341b.ir.expected new file mode 100644 index 0000000000..87e36846bb --- /dev/null +++ b/test/suites/success/Regr-341b.ir.expected @@ -0,0 +1,4 @@ +def .foo { + Bar => T, + Baz absurd +} diff --git a/test/suites/success/Regr-341c.ir.expected b/test/suites/success/Regr-341c.ir.expected new file mode 100644 index 0000000000..d993ff3be7 --- /dev/null +++ b/test/suites/success/Regr-341c.ir.expected @@ -0,0 +1,8 @@ +def .neg { + T => F, + F => T +} + +let foo { comatch { .ap(x) => x.neg } } + +let bar { Refl(F) } diff --git a/test/suites/success/Regr-403.ir.expected b/test/suites/success/Regr-403.ir.expected new file mode 100644 index 0000000000..d206f82de4 --- /dev/null +++ b/test/suites/success/Regr-403.ir.expected @@ -0,0 +1,7 @@ +use "../../../std/data/eq.pol" +use "../../../std/data/bool.pol" +use "../../../std/codata/fun.pol" + +let foo { comatch { .ap(_, _, x1) => x1 } } + +let proof { Refl(, foo) } diff --git a/test/test-runner/src/phases.rs b/test/test-runner/src/phases.rs index d0b69ae488..8e2003a48b 100644 --- a/test/test-runner/src/phases.rs +++ b/test/test-runner/src/phases.rs @@ -4,6 +4,7 @@ use std::panic::{catch_unwind, AssertUnwindSafe}; use std::sync::Arc; use driver::{Database, FileSource, FileSystemSource, InMemorySource}; +use printer::Print as _; use url::Url; use parser::cst; @@ -67,15 +68,11 @@ where // Whether we expect a success in this phase. let expect_success = config.fail.as_ref().map(|fail| fail != phase.name()).unwrap_or(true); - // If we are in the phase that is expected to fail, we check - // whether there is an expected error output. - let output = config.fail.as_ref().and_then(|fail| { - if fail == phase.name() { - self.case.expected() - } else { - None - } - }); + let expected_output = match config.fail.as_deref() { + Some(fail) if fail == phase.name() => self.case.expected(phase.name()), + None => self.case.expected(phase.name()), + _ => None, + }; // Run the phase and handle the result let result = @@ -100,10 +97,14 @@ where if !expect_success { return Err(PhasesError::ExpectedFailure { got: out2.test_output() }); } - if let Some(expected) = output { + if let Some(expected) = expected_output { let actual = out2.test_output(); if actual != expected { - return Err(PhasesError::Mismatch { expected, actual }); + return Err(PhasesError::Mismatch { + phase: phase.name(), + expected, + actual, + }); } } Ok(out2) @@ -118,10 +119,14 @@ where if expect_success { return Err(PhasesError::ExpectedSuccess { got: report }); } - if let Some(expected) = output { + if let Some(expected) = expected_output { let actual = render_report(&report, false); if actual != expected { - return Err(PhasesError::Mismatch { expected, actual }); + return Err(PhasesError::Mismatch { + phase: phase.name(), + expected, + actual, + }); } } Err(PhasesError::AsExpected) @@ -149,8 +154,8 @@ where let result = match self.result { Ok(_) => Ok(()), Err(PhasesError::AsExpected { .. }) => Ok(()), - Err(PhasesError::Mismatch { expected, actual }) => { - Err(Failure::Mismatch { expected, actual }) + Err(PhasesError::Mismatch { phase, expected, actual }) => { + Err(Failure::Mismatch { phase, expected, actual }) } Err(PhasesError::ExpectedFailure { got }) => Err(Failure::ExpectedFailure { got }), Err(PhasesError::ExpectedSuccess { got }) => Err(Failure::ExpectedSuccess { got }), @@ -161,22 +166,18 @@ where } } +/// A test case failed. #[derive(Debug)] pub enum Failure { - Mismatch { - expected: String, - actual: String, - }, + /// The output of a phase did not match the expected output. + Mismatch { phase: &'static str, expected: String, actual: String }, + /// The test was expected to fail, but it succeeded. #[allow(clippy::enum_variant_names)] - ExpectedFailure { - got: String, - }, - ExpectedSuccess { - got: miette::Report, - }, - Panic { - msg: String, - }, + ExpectedFailure { got: String }, + /// The test was expected to succeed, but it failed. + ExpectedSuccess { got: miette::Report }, + /// The test panicked during execution. + Panic { msg: String }, } impl Error for Failure {} @@ -184,7 +185,7 @@ impl Error for Failure {} impl fmt::Display for Failure { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { - Failure::Mismatch { expected, actual } => { + Failure::Mismatch { phase: _, expected, actual } => { write!(f, "\n Expected : {expected}\n Got : {actual}") } Failure::ExpectedFailure { got } => write!(f, "Expected failure, got {got}"), @@ -201,7 +202,7 @@ impl fmt::Display for Failure { enum PhasesError { AsExpected, Panic { msg: String }, - Mismatch { expected: String, actual: String }, + Mismatch { phase: &'static str, expected: String, actual: String }, ExpectedFailure { got: String }, ExpectedSuccess { got: miette::Report }, } @@ -381,6 +382,32 @@ impl Phase for Xfunc { } } +// IR Phase +// +// This phase generates the intermediate representation of the module. + +pub struct IR { + name: &'static str, +} + +impl Phase for IR { + type Out = String; + + fn new(name: &'static str) -> Self { + Self { name } + } + + fn name(&self) -> &'static str { + self.name + } + + async fn run(db: &mut Database, uri: &Url) -> Result { + let ir = db.ir(uri).await?; + let pretty_ir = ir.print_to_string(None); + Ok(pretty_ir) + } +} + // TestOutput pub trait TestOutput { diff --git a/test/test-runner/src/runner.rs b/test/test-runner/src/runner.rs index 43100d3cf5..d3b74e3e16 100644 --- a/test/test-runner/src/runner.rs +++ b/test/test-runner/src/runner.rs @@ -113,6 +113,7 @@ impl Runner { .then(config, Lower::new("relower")) .then(config, Check::new("recheck")) .then(config, Xfunc::new("xfunc")) + .then(config, IR::new("ir")) .report() } } @@ -138,8 +139,8 @@ impl RunResult { pub fn update_expected(&self) { for CaseResult { case, result } in self.case_results() { - if let Err(Failure::Mismatch { ref actual, .. }) = result { - case.set_expected(actual); + if let Err(Failure::Mismatch { phase, ref actual, .. }) = result { + case.set_expected(phase, actual); } } } diff --git a/test/test-runner/src/suites.rs b/test/test-runner/src/suites.rs index 29a83c6541..79fe29e53e 100644 --- a/test/test-runner/src/suites.rs +++ b/test/test-runner/src/suites.rs @@ -44,19 +44,27 @@ impl Case { Url::from_file_path(canonicalized_path).unwrap() } - pub fn expected(&self) -> Option { - let path = self.expected_path(); + pub fn expected(&self, phase_name: &str) -> Option { + let path = self.expected_path(phase_name); // Depending on how git is configured on Windows, it may check-out Unix line endings (\n) as Windows line endings (\r\n). // If this is the case, we need to replace these by Unix line endings for comparision. path.is_file().then(|| fs::read_to_string(path).unwrap().replace("\r\n", "\n")) } - pub fn set_expected(&self, s: &str) { - fs::write(self.expected_path(), s).unwrap(); + pub fn set_expected(&self, phase_name: &str, s: &str) { + fs::write(self.expected_path(phase_name), s).unwrap(); } - fn expected_path(&self) -> PathBuf { - self.path.parent().unwrap().join(format!("{}.expected", self.name)) + fn expected_path(&self, phase_name: &str) -> PathBuf { + let file_extension = phase_name.to_lowercase(); + let path = + self.path.parent().unwrap().join(format!("{}.{}.expected", self.name, file_extension)); + if path.exists() { + path + } else { + // Fallback: Tests that expect failure have a single expected file for the error message. + self.path.parent().unwrap().join(format!("{}.expected", self.name)) + } } }