package universo

  1. Overview
  2. Docs
package universo
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct