nuscr 2.1.1 · OCaml Package

Expressions, used in RefinementTypes pragma

Expressions

type t

An expression, used in RefinementType extension

 type t =
   | Var of VariableName.t  (** A variable *)
   | Int of int  (** An integer constant *)
   | Bool of bool  (** An boolean constant *)
   | String of string  (** A string literal *)
   | Binop of binop * t * t  (** A binary operator *)
   | Unop of unop * t  (** An unary operator *)

val sexp_of_t : t -> Sexplib0.Sexp.t

val equal : t -> t -> Ppx_deriving_runtime.bool

val compare : t -> t -> Ppx_deriving_runtime.int

val show : t -> Base.string

val free_var : t -> Base.Set.M(Nuscrlib__.Names.VariableName).t

Get free variables in an expression

val substitute : from:Names.VariableName.t -> replace:t -> t -> t

Perform substitutions on an expression

module Sexp : sig ... end

An modified S-expression library that distinguishes literal strings and * atoms

val sexp_of_expr : t -> Sexp.t

Convert an expression to S-expression

Types

type payload_type =

| PTInt
(*
A type for integers
*)
| PTBool
(*
A type for booleans
*)
| PTString
(*
A type for strings
*)
| PTUnit
(*
A type for units
*)
| PTAbstract of Names.PayloadTypeName.t
(*
A type for other un-modelled payloads, e.g. custom types
*)
| PTRefined of Names.VariableName.t * payload_type * t
(*
A refined types, PTRefined (x, ty, e) stands for the refined type 'x:ty{e}' where e is a predicate on x.
*)

Types for expressions. Integers, booleans and strings are are modelled, and can be thus refined with RefinementTypes extension

val sexp_of_payload_type : payload_type -> Sexplib0.Sexp.t

val equal_payload_type : 
  payload_type ->
  payload_type ->
  Ppx_deriving_runtime.bool

val compare_payload_type : 
  payload_type ->
  payload_type ->
  Ppx_deriving_runtime.int

val show_payload_type : payload_type -> Base.string

val payload_typename_of_payload_type : payload_type -> Names.PayloadTypeName.t

Extract PayloadTypeName from a payload_type

val smt_sort_of_type : payload_type -> Base.string

Get the SMT sort of a payload_type

val default_value : payload_type -> t

Get the default value of a payload type, which may not exist.

val parse_typename : Names.PayloadTypeName.t -> payload_type

Convert a PayloadTypeName to a payload_type

Typing

type typing_env

val new_typing_env : typing_env

val is_well_formed_type : typing_env -> payload_type -> Base.bool

Check whether a payload type is well-formed under the typing context

val ensure_satisfiable : typing_env -> Base.unit

Validate whether the typing context is satisfiable, i.e. it does not contain in consistencies

val env_append : 
  typing_env ->
  Names.VariableName.t ->
  payload_type ->
  typing_env

Append an new entry into typing context

val check_type : typing_env -> t -> payload_type -> Base.bool

Check whether an expression can be assigned a provided type under a typing context

SMT Interfacing

type smt_script

val add_assert_s_expr : Sexp.t -> smt_script -> smt_script

Add an assertion into a SMT script

val encode_env : typing_env -> smt_script

Encode a typing context into a SMT script

val check_sat : smt_script -> [ `Sat | `Unsat | `Unknown ]

Invoke SMT solver on an SMT script

package nuscr

Expressions

Types

Typing

SMT Interfacing