Typechecker (alt-ergo-lib.AltErgoLib.Typechecker)

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