Module AltErgoLib.Translate

val clear_cache : unit -> unit

Empties the internal cache of the module.

val dty_to_ty : ?update:bool -> ?is_var:bool -> AltErgoLib.D_loop.DStd.Expr.ty -> Ty.t

dty_to_ty update is_var subst tyv_substs dty

Converts a Dolmen type to an Alt-Ergo type.

  • If update is true then for each type variable of type DE.Ty.Var.t, if it was not encountered before, a new type variable of type Ty.t is created and added to the cache.
  • If dty is a type application, or an arrow type, only its return type is converted since those have no counterpart in AE's Ty module. The function arguments' types or the type paramters ought to be converted individually.
val make_form : string -> AltErgoLib.D_loop.DStd.Expr.term -> Dolmen.Std.Loc.loc -> decl_kind:Expr.decl_kind -> Expr.t
val make : AltErgoLib.D_loop.DStd.Loc.file -> Commands.sat_tdecl list -> [< D_loop.Typer_Pipe.typechecked | `Optimize of Dolmen.Std.Expr.term * bool | `Goal of Dolmen.Std.Expr.term | `Check of Dolmen.Std.Expr.term list Hyp ] D_loop.Typer_Pipe.stmt -> Commands.sat_tdecl list

make acc stmt Makes one or more Commands.sat_tdecl from the type-checked statement stmt and appends them to acc.

val builtins : Dolmen_loop.State.t -> D_loop.Typer.lang -> Dolmen_loop.Typer.T.builtin_symbols