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.

Parsing
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.