kind_checker/
lib.rs

1//! A type checker for the kind2 language. It has some utilities
2//! to [compile kind2 code][compiler] into a version that the checker
3//! can understand and [transform the answer back][report] into a
4//! version that the Rust side can manipulate.
5
6pub mod compiler;
7mod diagnostic;
8pub mod report;
9
10use std::sync::mpsc::Sender;
11
12use hvm::{language, get_cost};
13use hvm::{runtime, syntax::Term};
14use kind_report::data::Diagnostic;
15use kind_tree::desugared::Book;
16use report::parse_report;
17
18pub const CHECKER: &str = include_str!("checker.hvm");
19
20pub fn eval(file: &str, term: &str, dbug: bool, tids: Option<usize>) -> Result<(Box<Term>, u64), String> {
21    let file = language::syntax::read_file(&format!("{}\nHVM_MAIN_CALL = {}", file, term))?;
22
23    let book = language::rulebook::gen_rulebook(&file);
24    let mut prog = runtime::Program::new();
25    prog.add_book(&book);
26    let size = runtime::default_heap_size();
27
28    let tids = tids.unwrap_or(1);
29
30    let heap = runtime::new_heap(size, tids);
31    let tids = runtime::new_tids(tids);
32
33    runtime::link(
34        &heap,
35        0,
36        runtime::Fun(*book.name_to_id.get("HVM_MAIN_CALL").unwrap(), 0),
37    );
38
39    let host = 0;
40    runtime::normalize(&heap, &prog, &tids, host, dbug);
41    let code = language::readback::as_term(&heap, &prog, host);
42    runtime::collect(&heap, &prog.aris, tids[0], runtime::load_ptr(&heap, host));
43    runtime::free(&heap, 0, 0, 1);
44    Ok((code, get_cost(&heap)))
45
46}
47
48/// Generates the checker in a string format that can be
49/// parsed by HVM.
50pub fn gen_checker(book: &Book, check_coverage: bool, functions_to_check: Vec<String>) -> String {
51    let mut checker = CHECKER.to_string();
52    checker.push_str(&compiler::codegen_book(book, check_coverage, functions_to_check).to_string());
53    checker
54}
55
56/// Type checks a dessugared book. It spawns an HVM instance in order
57/// to run a compiled version of the book
58pub fn type_check(
59    book: &Book,
60    tx: Sender<Box<dyn Diagnostic>>,
61    functions_to_check: Vec<String>,
62    check_coverage: bool,
63    tids: Option<usize>
64) -> Option<u64> {
65    let file = gen_checker(book, check_coverage, functions_to_check);
66
67    match eval(&file, "Main", false, tids) {
68        Ok((term, rewrites)) => {
69            let errs = parse_report(&term).unwrap_or_else(|_| {
70                panic!(
71                    "Internal Error: Cannot parse the report message from the type checker: {}",
72                    term
73                )
74            });
75
76            let succeeded = errs.is_empty();
77
78            for err in errs {
79                tx.send(Box::new(err)).unwrap()
80            }
81
82            if succeeded {
83                Some(rewrites)
84            } else {
85                None
86            }
87        }
88        Err(res) => panic!("{}", res),
89    }
90}
91
92/// Runs the type checker but instead of running the check all function
93/// we run the "eval_main" that runs the generated version that both HVM and
94/// and the checker can understand.
95pub fn eval_api(book: &Book) -> (String, u64) {
96
97    let file = gen_checker(book, false, Vec::new());
98
99    let file = language::syntax::read_file(&file).unwrap();
100
101    let book = language::rulebook::gen_rulebook(&file);
102
103    let mut prog = runtime::Program::new();
104    prog.add_book(&book);
105
106    let heap = runtime::new_heap(runtime::default_heap_size(), runtime::default_heap_tids());
107    let tids = runtime::new_tids(runtime::default_heap_tids());
108
109    // Allocates the main term
110    runtime::link(
111        &heap,
112        0,
113        runtime::Fun(*book.name_to_id.get("Apps.Kind.API.eval_main").unwrap(), 0),
114    );
115    let host = 0;
116
117    // Normalizes it
118    runtime::normalize(&heap, &prog, &tids, host, false);
119
120    // Reads it back to a string
121    let term = language::readback::as_string(&heap, &prog, &tids, host).unwrap();
122
123    // Frees used memory
124    runtime::collect(&heap, &prog.aris, tids[0], runtime::load_ptr(&heap, host));
125    runtime::free(&heap, 0, 0, 1);
126
127    (term, get_cost(&heap))
128}
kind_checker/lib.rs

kind_checker/
lib.rs
