HigherOrderCO/Kind1
1
1
Fork 0
mirror of https://github.com/HigherOrderCO/Kind1.git synced 2024-10-26 16:58:48 +03:00
Code Issues Packages Projects Releases Wiki Activity

Add bootstrap script and removed the need for the inject comment

Browse Source
This commit is contained in:
Felipe g 2022-08-23 09:20:30 -03:00
parent a8662bb93f
commit 4167d3f590
3 changed files with 636 additions and 613 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
bootstrap.sh Executable file
View File

@ -0,0 +1,4 @@
cargo build --release
# Probably we should just use git clone in Wikind?
cd ../Wikind
../Kind2/target/release/kind2 to-hvm Kind/TypeChecker.kind2 >> ../Kind2/src/checker.hvm

1243
src/checker.hvm
View File

File diff suppressed because it is too large Load Diff

2
src/main.rs
View File

@ -287,7 +287,7 @@ pub fn readback_string(rt: &hvm::Runtime, host: u64) -> String {
fn gen_checker(book: &Book) -> String {
// Compile the Kind2 file to HVM checker
let base_check_code = compile_book(&book);
let mut check_code = (&CHECKER_HVM[0 .. CHECKER_HVM.find("////INJECT////").unwrap()]).to_string();
let mut check_code = CHECKER_HVM.to_string();
check_code.push_str(&base_check_code);
return check_code;
}