Crate kind_checker

Source
Expand description

A type checker for the kind2 language. It has some utilities to compile kind2 code into a version that the checker can understand and transform the answer back into a version that the Rust side can manipulate.

Modules§

compiler
This module compiles all of the code to a format that can run on the HVM and inside the checker.hvm file.
report
Transforms a answer from the type checker in a Expr of the kind-tree package.

Constants§

CHECKER

Functions§

eval
eval_api
Runs the type checker but instead of running the check all function we run the “eval_main” that runs the generated version that both HVM and and the checker can understand.
gen_checker
Generates the checker in a string format that can be parsed by HVM.
type_check
Type checks a dessugared book. It spawns an HVM instance in order to run a compiled version of the book