diff --git a/src/fun/builtins.bend b/src/fun/builtins.bend index 973f7835..4e7dd8d2 100644 --- a/src/fun/builtins.bend +++ b/src/fun/builtins.bend @@ -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) diff --git a/src/fun/transform/resolve_type_ctrs.rs b/src/fun/transform/resolve_type_ctrs.rs index 2c1a57fe..9829f751 100644 --- a/src/fun/transform/resolve_type_ctrs.rs +++ b/src/fun/transform/resolve_type_ctrs.rs @@ -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(); diff --git a/src/fun/transform/type_check.rs b/src/fun/transform/type_check.rs index 1d14b267..12f63dbc 100644 --- a/src/fun/transform/type_check.rs +++ b/src/fun/transform/type_check.rs @@ -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) } } diff --git a/src/lib.rs b/src/lib.rs index 8dfc79b3..ff34c8ec 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -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, } } diff --git a/src/main.rs b/src/main.rs index 7acf47c3..1a2882bf 100644 --- a/src/main.rs +++ b/src/main.rs @@ -188,6 +188,8 @@ pub enum OptArgs { NoCheckNetSize, AdtScott, AdtNumScott, + TypeCheck, + NoTypeCheck, } fn compile_opts_from_cli(args: &Vec) -> CompileOpts { @@ -210,6 +212,8 @@ fn compile_opts_from_cli(args: &Vec) -> 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,