This commit is contained in:
Nicolas Abril 2024-08-07 18:40:13 +02:00
parent d13d303385
commit 6f979e805e
5 changed files with 20 additions and 8 deletions

View File

@ -180,7 +180,7 @@ def IO/MAGIC -> (u24, u24):
def IO/wrap(x: T) -> IO(T):
return IO/Done(IO/MAGIC, x)
def IO/bind(a: IO(A), b: A -> IO(B)) -> IO(B):
def IO/bind(a: IO(A), b: (id -> id) -> A -> IO(B)) -> IO(B):
match a:
case IO/Done:
b = undefer(b)

View File

@ -7,7 +7,7 @@ use crate::{
};
impl Ctx<'_> {
/// Resolves type constructors in the book and adds for alls for the free type vars.
/// Resolves type constructors in the book and adds for-alls for the free type vars.
pub fn resolve_type_ctrs(&mut self) -> Result<(), Diagnostics> {
for def in self.book.defs.values_mut() {
let mut free_vars = Default::default();

View File

@ -374,7 +374,7 @@ fn ctr_to_kindc(ctr_nam: &Name, adt: &Adt, counter: &mut u64, book: &mut KindCBo
typ: Box::new(KT::Set),
bod: Box::new(typ),
});
let term = KT::Ann { chk: true, bod: Box::new(term), typ: Box::new(typ) };
let term = KT::Ann { chk: false, bod: Box::new(term), typ: Box::new(typ) };
book.insert(src, (ctr_nam.to_string(), term));
}
@ -425,7 +425,7 @@ fn adt_to_kindc(adt: &Adt, counter: &mut u64, book: &mut KindCBook) {
bod: Box::new(typ),
});
let term = KT::Ann { chk: true, bod: Box::new(term), typ: Box::new(typ) };
let term = KT::Ann { chk: false, bod: Box::new(term), typ: Box::new(typ) };
book.insert(src, (adt.name.to_string(), term));
}
@ -695,7 +695,7 @@ impl Type {
Type::Tup(els) => els.iter().fold(KT::Ref { nam: format!("kindc__tup{}", els.len()) }, |typ, el| {
KT::App { fun: Box::new(typ), arg: Box::new(el.to_kindc(counter, src)) }
}),
Type::None => KT::Ref { nam: "None".to_string() },
Type::None => KT::Ref { nam: "kindc__none".to_string() },
});
KT::Src { src, bod: Box::new(kt) }
}

View File

@ -103,7 +103,6 @@ pub fn desugar_book(
ctx.book.encode_builtins();
ctx.resolve_refs()?;
ctx.resolve_type_ctrs()?;
ctx.desugar_match_defs()?;
@ -128,7 +127,9 @@ pub fn desugar_book(
// Manual match linearization
ctx.book.linearize_match_with();
type_check_book(&mut ctx)?;
if opts.type_check {
type_check_book(&mut ctx)?;
}
ctx.book.encode_matches(opts.adt_encoding);
@ -172,6 +173,7 @@ pub fn type_check_book(ctx: &mut Ctx) -> Result<(), Diagnostics> {
let old_book = std::mem::replace(ctx.book, ctx.book.clone());
ctx.make_native_defs();
ctx.book.encode_adts(AdtEncoding::Scott);
ctx.resolve_type_ctrs()?;
let res = ctx.type_check();
*ctx.book = old_book;
res?;
@ -365,6 +367,9 @@ pub struct CompileOpts {
/// Enables [hvm::check_net_size].
pub check_net_size: bool,
/// Enables [type_check_book].
pub type_check: bool,
/// Determines the encoding of constructors and matches.
pub adt_encoding: AdtEncoding,
}
@ -378,8 +383,9 @@ impl CompileOpts {
prune: true,
float_combinators: true,
merge: true,
inline: true,
linearize_matches: OptLevel::Enabled,
type_check: true,
inline: self.inline,
check_net_size: self.check_net_size,
adt_encoding: self.adt_encoding,
}
@ -395,6 +401,7 @@ impl CompileOpts {
float_combinators: false,
merge: false,
inline: false,
type_check: self.type_check,
check_net_size: self.check_net_size,
adt_encoding: self.adt_encoding,
}
@ -426,6 +433,7 @@ impl Default for CompileOpts {
merge: false,
inline: false,
check_net_size: false,
type_check: true,
adt_encoding: AdtEncoding::NumScott,
}
}

View File

@ -188,6 +188,8 @@ pub enum OptArgs {
NoCheckNetSize,
AdtScott,
AdtNumScott,
TypeCheck,
NoTypeCheck,
}
fn compile_opts_from_cli(args: &Vec<OptArgs>) -> CompileOpts {
@ -210,6 +212,8 @@ fn compile_opts_from_cli(args: &Vec<OptArgs>) -> CompileOpts {
NoInline => opts.inline = false,
CheckNetSize => opts.check_net_size = true,
NoCheckNetSize => opts.check_net_size = false,
TypeCheck => opts.type_check = true,
NoTypeCheck => opts.type_check = false,
LinearizeMatches => opts.linearize_matches = OptLevel::Enabled,
LinearizeMatchesAlt => opts.linearize_matches = OptLevel::Alt,