package nuscr

  1. Overview
  2. Docs

Module Nuscrlib.Expr

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

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 =
  1. | PTInt
    (*

    A type for integers

    *)
  2. | PTBool
    (*

    A type for booleans

    *)
  3. | PTString
    (*

    A type for strings

    *)
  4. | PTUnit
    (*

    A type for units

    *)
  5. | PTAbstract of Names.PayloadTypeName.t
    (*

    A type for other un-modelled payloads, e.g. custom types

    *)
  6. | 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

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