Skip to content

Commit

Permalink
Add pol compile and ir phase to test runner (#433)
Browse files Browse the repository at this point in the history
* Add pol compile and ir phase to test runner

* Improve pretty-printing of let in ir

* Document Failure
  • Loading branch information
timsueberkrueb authored Jan 4, 2025
1 parent f63e288 commit e83eaae
Show file tree
Hide file tree
Showing 59 changed files with 1,322 additions and 43 deletions.
1 change: 1 addition & 0 deletions Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

35 changes: 35 additions & 0 deletions app/src/cli/compile.rs
Original file line number Diff line number Diff line change
@@ -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
}
4 changes: 4 additions & 0 deletions app/src/cli/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@ use clap::{Parser, Subcommand};

mod check;
mod clean;
mod compile;
mod doc;
mod format;
mod gen_completions;
Expand Down Expand Up @@ -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,
}
};

Expand Down Expand Up @@ -82,4 +84,6 @@ enum Command {
Clean,
/// Generate completion scripts for various shells
GenerateCompletion(gen_completions::Args),
/// Compile an executable
Compile(compile::Args),
}
8 changes: 7 additions & 1 deletion lang/backend/src/ir/decls.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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)
}
Expand Down
1 change: 1 addition & 0 deletions lang/driver/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -33,3 +33,4 @@ elaborator = { path = "../elaborator" }
printer = { path = "../printer" }
parser = { path = "../parser" }
transformations = { path = "../transformations" }
backend = { path = "../backend" }
41 changes: 37 additions & 4 deletions lang/driver/src/database.rs
Original file line number Diff line number Diff line change
@@ -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;

Expand All @@ -35,6 +38,8 @@ pub struct Database {
pub ust: Cache<Result<Arc<ast::Module>, Error>>,
/// The typechecked AST of a module
pub ast: Cache<Result<Arc<ast::Module>, Error>>,
/// The IR of a module
pub ir: Cache<Result<Arc<ir::Module>, Error>>,
/// The type info table constructed during typechecking
pub module_type_info_table: Cache<elaborator::ModuleTypeInfoTable>,
/// Hover information for spans
Expand Down Expand Up @@ -247,6 +252,33 @@ impl Database {
ast
}

// Core API: ir
//
//

pub async fn ir(&mut self, uri: &Url) -> Result<Arc<ir::Module>, 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<Arc<ir::Module>, 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
//
//
Expand Down Expand Up @@ -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(),
Expand Down
2 changes: 2 additions & 0 deletions lang/driver/src/paths.rs
Original file line number Diff line number Diff line change
@@ -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";
Expand Down
3 changes: 3 additions & 0 deletions lang/driver/src/result.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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)]
Expand All @@ -13,6 +15,7 @@ pub enum Error {
Type(#[from] Box<elaborator::result::TypeError>),
Xfunc(#[from] transformations::result::XfuncError),
Driver(#[from] DriverError),
Backend(#[from] BackendError),
}

#[derive(Error, Debug, Diagnostic, Clone)]
Expand Down
1 change: 1 addition & 0 deletions test/suites/success/001.ir.expected
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
codef Id(a) { .ap(a0, b, x) => x }
1 change: 1 addition & 0 deletions test/suites/success/002.ir.expected
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
codef Compose(a, b, c, f, g) { .ap(a', c', x) => g.ap(b, c, f.ap(a, b, x)) }
Empty file.
Empty file.
6 changes: 6 additions & 0 deletions test/suites/success/005.ir.expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
def .not {
True => False,
False => True
}

def .false { Unit => True.not }
1 change: 1 addition & 0 deletions test/suites/success/006.ir.expected
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
def .foo(a, d) { Unit => d.match { MkD(a0) => MkD(a).match { MkD(x) => MkD(a) } } }
4 changes: 4 additions & 0 deletions test/suites/success/007.ir.expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
def .foo {
CTrue => Z,
CFalse absurd
}
1 change: 1 addition & 0 deletions test/suites/success/008.ir.expected
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
def .id(a) { Unit => comatch { .ap(_, _, x1) => x1 } }
6 changes: 6 additions & 0 deletions test/suites/success/009.ir.expected
Original file line number Diff line number Diff line change
@@ -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") } }
}
6 changes: 6 additions & 0 deletions test/suites/success/010.ir.expected
Original file line number Diff line number Diff line change
@@ -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") } }
}
6 changes: 6 additions & 0 deletions test/suites/success/011.ir.expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
def .foo {
Foo1 => True,
Foo2 absurd,
Foo3 absurd,
Foo4 absurd
}
6 changes: 6 additions & 0 deletions test/suites/success/012.ir.expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
codef MyFoo {
.foo1 => True,
.foo2 absurd,
.foo3 absurd,
.foo4 absurd
}
6 changes: 6 additions & 0 deletions test/suites/success/013.ir.expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
let add(x, y) {
x.match {
Z => y,
S(x') => panic!("not yet implemented")
}
}
11 changes: 11 additions & 0 deletions test/suites/success/014.ir.expected
Original file line number Diff line number Diff line change
@@ -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) }
3 changes: 3 additions & 0 deletions test/suites/success/015.ir.expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
let transparentTwo { S(S(Z)) }

let p2 { Refl(<ZST>, S(S(Z))) }
10 changes: 10 additions & 0 deletions test/suites/success/016-named-args.ir.expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
def .and(other) {
True => other,
False => False
}

let example1 { Cons(True, Nil) }

let example2 { True.and(False) }

let example3 { None(<ZST>) }
1 change: 1 addition & 0 deletions test/suites/success/017.ir.expected
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
let example1 { MkPair(<ZST>, <ZST>, True, False) }
1 change: 1 addition & 0 deletions test/suites/success/018.ir.expected
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
let example { None(panic!("not yet implemented")) }
6 changes: 6 additions & 0 deletions test/suites/success/019-absurd.ir.expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
def .elim_zero(a) { SNotZero(n) absurd }

def .elim(a) {
Ok(a0, x) => x,
Absurd(x) => x.elim_zero(<ZST>)
}
12 changes: 12 additions & 0 deletions test/suites/success/020-motive.ir.expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
def self.rep {
T => TrueRep,
F => FalseRep
}

def .example(b) {
Unit =>
b.match {
T => TrueRep,
F => FalseRep
}
}
7 changes: 7 additions & 0 deletions test/suites/success/021-evalorder.ir.expected
Original file line number Diff line number Diff line change
@@ -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 }
1 change: 1 addition & 0 deletions test/suites/success/022-implicit-list.ir.expected
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
let example { Cons(<ZST>, Unit, Nil(<ZST>)) }
14 changes: 14 additions & 0 deletions test/suites/success/023-comatches.ir.expected
Original file line number Diff line number Diff line change
@@ -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) => <ZST> }
4 changes: 4 additions & 0 deletions test/suites/success/024-gadt.ir.expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
def .unwrap(a) {
WrapFoo(x) => x,
WrapBar(x) => x
}
11 changes: 11 additions & 0 deletions test/suites/success/025-imports.ir.expected
Original file line number Diff line number Diff line change
@@ -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 }
17 changes: 17 additions & 0 deletions test/suites/success/026-refinement.ir.expected
Original file line number Diff line number Diff line change
@@ -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(<ZST>, True),
False => Refl(<ZST>, False)
}
Loading

0 comments on commit e83eaae

Please sign in to comment.