Module Common.FilesSource

module P = Parsers.Parser
Sourcemodule Processor = Api.Processor
Sourcetype path = string

path to a file

Sourcetype cin
Sourcetype cout
Sourcetype _ channel =
  1. | In : in_channel -> cin channel
  2. | Out : out_channel * 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.

Sourcetype '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

    *)
}
Sourceval output_directory : string option ref

Output directory where output files are created

Sourceval simplify_directory : string option ref

Simplify directory where simplified files are created.

Sourceval elaboration_suffix : string

Suffix used for files containing universe declarations

Sourceval checking_suffix : string

Suffix used for files containing universe constraints

Sourceval solution_suffix : string

Suffix used for files containing universe solution

Sourceval normal_suffix : string

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

Sourcetype 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

Sourceval add_suffix : path -> string -> string

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

Sourceval add_dir : string -> string -> string

add_dir dir file prefix the filename file with the directory dir

Sourceval mk_dir : string option ref -> string -> unit
Sourceval suffix_of_step : step -> string

return the suffix according to the step s

Sourceval theory : string option ref
Sourceval mk_theory : path -> unit
Sourceval get_theory : unit -> string
Sourceval get_out_path : path -> step -> path

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

Sourceval out_from_string : path -> step -> cout t

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

Sourceval in_from_string : path -> step -> cin t

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

Sourceval fmt_of_file : cout t -> Format.formatter

fmt_of_file out_file returns the formatter associated to an out_file

Sourceval in_channel_of_file : cin t -> in_channel

in_channel_of_file in_file returns the channel associated to an in_file

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

close file closes file

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

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

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