gleamunison/verify

eval_file

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.

get_init_defs

</>

pub fn get_init_defs() -> List(#(String, elab_types.SurfaceDef))

load_defs_file

</>

pub fn load_defs_file(
  path: String,
) -> Result(
  #(types.TypeCache, List(#(String, elab_types.SurfaceDef))),
  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).

parse_all_sexprs

</>

pub fn parse_all_sexprs(
  tokens: List(lexer.TokenInfo),
  acc: List(parser.SExpr),
) -> Result(List(parser.SExpr), lexer.ParseError)

terms_from_sexprs

</>

pub fn terms_from_sexprs(
  exprs: List(parser.SExpr),
  acc: List(elab_types.SurfaceTerm),
) -> Result(List(elab_types.SurfaceTerm), lexer.ParseError)

verify_file

</>

pub fn verify_file(path: String) -> Result(String, String)