package alt-ergo-lib

  1. Overview
  2. Docs
On This Page
  1. Parsing

Module type Input.S

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.

Parsing
type parsed

The type of a parsed statement.

val parse_file : content:string -> format:string option -> parsed 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 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 Stack.t -> parsed -> int Typed.atdecl list * env

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