package universo

  1. Overview
  2. Docs
module B = Kernel.Basic
module S = Kernel.Signature
module P = Parsers.Parser
module Processor = Api.Processor
type path = string

path to a file

type cin
type cout
type _ channel =
  1. | In : Stdlib.in_channel -> cin channel
  2. | Out : Stdlib.out_channel * Stdlib.Format.formatter -> cout channel

Gather out_channel and in_channel in a GADT for input and output files. In the case of an output file, we store also the formatter associated with.

type 'a t = {
  1. path : path;
    (*

    Path to the current file

    *)
  2. md : B.mident;
    (*

    Md of this file

    *)
  3. channel : 'a channel;
    (*

    OCaml channel to this file

    *)
}
val output_directory : string option Stdlib.ref

Output directory where output files are created

val simplify_directory : string option Stdlib.ref

Simplify directory where simplified files are created.

val elaboration_suffix : string

Suffix used for files containing universe declarations

val checking_suffix : string

Suffix used for files containing universe constraints

val solution_suffix : string

Suffix used for files containing universe solution

val normal_suffix : string

Suffix used for elaborated file where sorts are replaced by fresh variables

type step = [
  1. | `Input
    (*

    Input module

    *)
  2. | `Output
    (*

    Output module

    *)
  3. | `Elaboration
    (*

    File with universe declarations

    *)
  4. | `Checking
    (*

    File with constraints

    *)
  5. | `Solution
    (*

    File containing the solution

    *)
  6. | `Simplify
    (*

    Output file where the variables are replaced by the solution

    *)
]

The steps used to refer the files used by Universo

val add_suffix : path -> string -> string

add_sufix file suffix returns the string file' where suffix is_added at then end of file

val add_dir : string -> string -> string

add_dir dir file prefix the filename file with the directory dir

val mk_dir : string option Stdlib.ref -> string -> unit
val suffix_of_step : step -> string

return the suffix according to the step s

val theory : string option Stdlib.ref
val mk_theory : path -> unit
val get_theory : unit -> string
val get_out_path : path -> step -> path

get_out_path p s returns the path that corresponds to the step s for path p

val out_from_string : path -> step -> cout t

from_string f s returns the filename that corresponds to the step s for file f

val in_from_string : path -> step -> cin t

from_string f s returns the filename that corresponds to the step s for file f

val fmt_of_file : cout t -> Stdlib.Format.formatter

fmt_of_file out_file returns the formatter associated to an out_file

val in_channel_of_file : cin t -> Stdlib.in_channel

in_channel_of_file in_file returns the channel associated to an in_file

val close : 'a. 'a t -> unit

close file closes file

val md_of : path -> step -> B.mident

md_of path step returns the mident associated to the Universo file file for step step.

val add_requires : Stdlib.Format.formatter -> B.mident list -> unit
type Processor.t +=
  1. | FilterSignature : Api.Env.t Processor.t
val export : path -> step -> unit