universo 2.7 (latest) · OCaml Package

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 =

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

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

| `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

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 +=

| FilterSignature : Api.Env.t Processor.t

val export : path -> step -> unit

package universo