diff --git a/src/kind-checker/src/lib.rs b/src/kind-checker/src/lib.rs index 0776494f..940cee7b 100644 --- a/src/kind-checker/src/lib.rs +++ b/src/kind-checker/src/lib.rs @@ -57,6 +57,7 @@ pub fn eval_api(book: &Book) -> Box { let mut runtime = hvm::Runtime::from_code(&check_code).unwrap(); let main = runtime.alloc_code("Kind.API.eval_main").unwrap(); + runtime.run_io(main); runtime.normalize(main); runtime.readback(main) diff --git a/src/kind-cli/src/lib.rs b/src/kind-cli/src/lib.rs index b57c9431..bd2f2166 100644 --- a/src/kind-cli/src/lib.rs +++ b/src/kind-cli/src/lib.rs @@ -185,7 +185,7 @@ pub fn run_cli(config: Cli) { } Command::Eval { file } => { compile_in_session(render_config, root, file.clone(), &mut |session| { - driver::erase_book(session, &PathBuf::from(file.clone()), &["Main".to_string()]) + driver::desugar_book(session, &PathBuf::from(file.clone())) }) .map(|res| { println!("{}", driver::eval_in_checker(&res)); diff --git a/src/kind-derive/src/matching.rs b/src/kind-derive/src/matching.rs index 81182c8c..35e445e1 100644 --- a/src/kind-derive/src/matching.rs +++ b/src/kind-derive/src/matching.rs @@ -170,7 +170,7 @@ pub fn derive_match(range: Range, sum: &SumTypeDecl) -> concrete::Entry { types.push(Argument { hidden: false, erased: false, - name: Ident::new_static(&format!("_{}", cons.name.to_string()), range), + name: Ident::new_static(&format!("{}_", cons.name.to_string()), range), typ: Some(cons_type), range, }); diff --git a/src/kind-derive/src/open.rs b/src/kind-derive/src/open.rs index ca25976a..1d8196d2 100644 --- a/src/kind-derive/src/open.rs +++ b/src/kind-derive/src/open.rs @@ -60,12 +60,12 @@ pub fn derive_open(range: Range, rec: &RecordDecl) -> concrete::Entry { types.push(Argument { hidden: true, erased: true, - name: Ident::generate("_res"), + name: Ident::generate("res_"), typ: None, range, }); - let cons_tipo = mk_var(Ident::generate("_res")); + let cons_tipo = mk_var(Ident::generate("res_")); let cons_type = rec.fields.iter().rfold(cons_tipo, |out, (name, _, typ)| { mk_pi(name.clone(), typ.clone(), out) @@ -91,7 +91,7 @@ pub fn derive_open(range: Range, rec: &RecordDecl) -> concrete::Entry { // Motive with indices - let ret_ty = mk_var(Ident::generate("_res")); + let ret_ty = mk_var(Ident::generate("res_")); let mut pats: Vec> = Vec::new(); diff --git a/src/kind-driver/src/lib.rs b/src/kind-driver/src/lib.rs index 74327854..4c2de12b 100644 --- a/src/kind-driver/src/lib.rs +++ b/src/kind-driver/src/lib.rs @@ -42,9 +42,7 @@ pub fn to_book(session: &mut Session, path: &PathBuf) -> Option let mut concrete_book = resolution::parse_and_store_book(session, path)?; expand::expand_book(&mut concrete_book); - - println!("{}", concrete_book); - + let failed = resolution::check_unbound_top_level(session, &mut concrete_book); if failed { diff --git a/src/kind-pass/src/desugar/mod.rs b/src/kind-pass/src/desugar/mod.rs index 8e0a2937..db13c0d9 100644 --- a/src/kind-pass/src/desugar/mod.rs +++ b/src/kind-pass/src/desugar/mod.rs @@ -61,7 +61,7 @@ impl<'a> DesugarState<'a> { fn gen_name(&mut self, range: Range) -> Ident { self.name_count += 1; - Ident::new(format!("_x{}", self.name_count), range) + Ident::new(format!("x{}_", self.name_count), range) } fn gen_hole_expr(&mut self) -> Box {