Implement support for IO Bool tests

This commit is contained in:
Nathan McCarty 2024-12-31 18:12:35 -05:00
parent c089685a2a
commit 09ac7506ee
4 changed files with 49 additions and 11 deletions

View file

@ -1,6 +1,9 @@
#| Utilities for interacting with the idris compiler and package manager
unit module IUtils::Compiler;
# Represents the output of an Expr that we need to run
enum ExprOutput is export <Unit Boolean Either>;
# Utility functions for pack
#| Invoke a pack command
@ -53,7 +56,7 @@ class IdrisError is Exception {
}
#| An error coming from a compiled expression
class ExpressionError is Exception {
class ExpressionError is Exception is export {
has Str $.out;
has Str $.err;
has Int $.exit-code;
@ -81,11 +84,27 @@ sub idris-run(*@cmd) is export {
return $out;
}
# TODO: Special handling for IO Bool to make this eaiser
#| Exec the expression with the given name in the given file
sub idris-exec($expr, $file) is export {
my constant $bool-lambda =
'(\x => if x then exitSuccess else exitFailure)';
# TODO: Implemenent support for the Either case
# TODO: Use the ide protocol to drive this so we can avoid the user needing to
# import anything
# Exec the expression with the given name in the given file
sub idris-exec($expr, $file, $output-type? = Unit) is export {
# Have idris compile an executable for the expression,
idris-run '--find-ipkg', '--client', ":c iutils_out $expr", $file;
given $output-type {
when Unit {
idris-run '--find-ipkg', '--client', ":c iutils_out $expr", $file;
}
when Boolean {
idris-run '--find-ipkg', '--client',
":c iutils_out ($expr >>= $bool-lambda)", $file;
}
default {
die "Unsupported output type encountered: $_";
}
}
# Run the expression
my $proc = run 'build/exec/iutils_out', :out, :err;
my $out = $proc.out.slurp(:close);