gleamunison/verify
Values
pub fn eval_file(path: String) -> Result(String, String)Evaluate a file and return the last form’s rendered value. Use this when the caller needs the RESULT (test harnesses, datalog queries), not just proof the file evaluates.
pub fn get_init_defs() -> List(#(String, elab_types.SurfaceDef))pub fn load_defs_file(
path: String,
) -> Result(
#(types.TypeCache, List(#(String, elab_types.SurfaceDef))),
String,
)pub fn load_defs_file_scoped(
path: String,
) -> Result(
#(
types.TypeCache,
List(#(String, elab_types.SurfaceDef)),
List(String),
),
String,
)Load a file’s definitions without evaluating anything: parse, bootstrap,
and fold define forms through handle_define (each is compiled and
loaded). Stray expressions are rejected — evaluating them at load time
would fire real handlers outside whatever frame the caller is about to
install (replay, recording, test). Returns the advanced cache and the
full def list (bootstrap + file).
Load a file’s definitions with bootstrap context. Returns the cache,
the full def list (bootstrap + file), and the file-local def names —
callers that gate on definitions (publish) must not gate the bootstrap.
pub fn parse_all_sexprs(
tokens: List(lexer.TokenInfo),
acc: List(parser.SExpr),
) -> Result(List(parser.SExpr), lexer.ParseError)pub fn terms_from_sexprs(
exprs: List(parser.SExpr),
acc: List(elab_types.SurfaceTerm),
) -> Result(List(elab_types.SurfaceTerm), lexer.ParseError)pub fn verify_file(path: String) -> Result(String, String)