Module `Common.Files`Source

Sourcemodule B = Kernel.Basic

Sourcemodule S = Kernel.Signature

module P = Parsers.Parser

Sourcemodule Processor = Api.Processor

Sourcetype path = string

path to a file

Sourcetype cin

Sourcetype cout

Sourcetype _ channel =

| In : in_channel -> cin channel
| 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 = {

path : path;
(*
Path to the current file
*)
md : B.mident;
(*
Md of this file
*)
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 = [

| `Input
(*
Input module
*)
| `Output
(*
Output module
*)
| `Elaboration
(*
File with universe declarations
*)
| `Checking
(*
File with constraints
*)
| `Solution
(*
File containing the solution
*)
| `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 +=

| FilterSignature : Api.Env.t Processor.t

Sourceval export : path -> step -> unit

Install

Dune Dependency

Authors

Maintainers

Sources

doc/universo.common/Common/Files/index.html

Module `Common.Files`Source

package universo

Install

Dune Dependency

Authors

Maintainers

Sources

doc/universo.common/Common/Files/index.html

Module Common.FilesSource

Module `Common.Files`Source