package alt-ergo-lib

  1. Overview
  2. Docs

This modules defines an input method. Input methods are responsible for two things: parsing and typechceking either an input file (possibly with some preludes files), or arbitrary terms. This last functionality is currently only used in the GUI.

type parsed

The type of a parsed statement.

val parse_file : content:string -> format:string option -> parsed Stdlib.Seq.t

Parse a file as a string with the given format or the input_format set

val parse_files : filename:string -> preludes:string list -> parsed Stdlib.Seq.t

Parse a file (and some preludes).

type env

Global typing environment

val empty_env : env

The empty/initial environment

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

Parse and typecheck some input file, together with some prelude files.