package alt-ergo-lib

  1. Overview
  2. Docs
type env

The type of global environment of the typechecker.

val empty_env : env

The empty/initial environment

val type_expr : env -> (Symbols.t * Ty.t) list -> Parsed.lexpr -> int Typed.atterm

Typecheck an input expression (i.e. term (or formula ?)), given a local environment and a list of local types used to extend the initial environment.

val type_parsed : env -> env Stdlib.Stack.t -> Parsed.decl -> int Typed.atdecl list * env

Type a single declaration.

val type_file : Parsed.file -> (int Typed.atdecl * env) list * env

Type an input file. Returns the successive global environments obtained after typing each declaration.

val split_goals : (int Typed.atdecl * 'a) list -> ((int Typed.atdecl * 'a) list * string) list
val split_goals_and_cnf : (int Typed.atdecl * 'a) list -> (Commands.sat_tdecl list * string) list