fix: eval command

This commit is contained in:
felipegchi 2022-11-16 11:37:11 -03:00
parent 2f14cc1267
commit 16467dedce
6 changed files with 8 additions and 9 deletions

View File

@ -57,6 +57,7 @@ pub fn eval_api(book: &Book) -> Box<Term> {
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)

View File

@ -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));

View File

@ -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,
});

View File

@ -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<Box<Pat>> = Vec::new();

View File

@ -42,9 +42,7 @@ pub fn to_book(session: &mut Session, path: &PathBuf) -> Option<concrete::Book>
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 {

View File

@ -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<desugared::Expr> {