Module MoxiTypeChecker

Sort checker for MoXI scripts

Checks a parsed script against the MoXI language definition before it is translated into transition systems: the sorts of the variables are well-formed and belong to the declared logic; every term is well-sorted under the SMT-LIB theories of Core, Ints, Reals, Reals_Ints, FixedSizeBitVectors and ArraysEx, and only uses the symbols of the declared logic (including its linearity restriction); the constants, enumeration sorts and values, and functions are declared once, under names of their own; the :init and :inv conditions are one-state formulas and the :trans condition is a two-state formula; every subsystem instance refers to a defined system and binds its inputs and outputs to variables of the right sorts and kinds; and every check-system renames the variables of its system consistently, primes only inputs in its assumptions, and names declared conditions in its queries.

The checker stops at the first error.

type sort =
  1. | Bool
  2. | Int
  3. | Real
  4. | BitVec of int
  5. | Array of sort * sort
    (*

    Index sort, element sort

    *)
  6. | Enum of string
    (*

    An enumeration sort, by name

    *)

A MoXI sort

val pp_print_sort : Stdlib.Format.formatter -> sort -> unit

Print a sort in SMT-LIB syntax

type error_kind =
  1. | UnknownLogic of string
  2. | LogicAlreadySet
  3. | LogicAfterDefinition
  4. | UnknownSort of string
  5. | MalformedSort of string * string
  6. | SortNotInLogic of sort * string
  7. | NumeralNotInLogic of string
  8. | DecimalNotInLogic of string
  9. | BitvectorNotInLogic of string
  10. | BitvectorOutOfRange of string * int
  11. | SymbolNotInLogic of string * string
  12. | NonlinearTerm of string * string
  13. | UnboundVariable of string
  14. | UnknownFunction of string
  15. | UnknownIndexedIdentifier of string
  16. | PrimedLetVariable of string
  17. | PrimedNonVariable of string
  18. | PrimeNotAllowed of string * string
  19. | PrimedNonInput of string * string
  20. | Arity of string * string * int
  21. | ArgumentSort of string * int * sort * string
  22. | ExpectedBool of string * sort
  23. | AscriptionMismatch of sort * sort
  24. | ConstArrayWithoutSort
  25. | ConstArrayNotArraySort of sort
  26. | DuplicateLetBinding of string
  27. | SystemRedefined of string
  28. | FunctionRedefined of string
  29. | SymbolRedeclared of string
  30. | BuiltinRedefined of string
  31. | SortRedeclared of string
  32. | FunctionBodySort of string * sort * sort
  33. | UnknownSystem of string
  34. | SelfInstantiation of string
  35. | DuplicateInstance of string
  36. | DuplicateVariable of string
  37. | SubsystemArity of string * string * int * int
  38. | SubsystemArgumentSort of string * string * sort * string * sort
  39. | SubsystemOutputToInput of string * string * string
  40. | RenamingArity of string * string * int * int
  41. | RenamingSort of string * sort * string * sort
  42. | DuplicateFormula of string
  43. | DuplicateQuery of string
  44. | UnknownFormula of string * string
  45. | SeveralCurrent of string

What went wrong

type error = Lib.position * error_kind

An error and where it was found

val error_message : error_kind -> string

A message describing an error

val check_script : MoxiAst.script -> (unit, error) Stdlib.result

Check a script, returning the first error found, if any

For the translation

val string_of_indexed_id : string -> MoxiAst.index list -> string

An identifier with its indices as written, (_ f i j), or the bare symbol when it has none

val bv_literal : string -> MoxiAst.index list -> (Numeral.t * Numeral.t) option

The value and width of a bit-vector literal (_ bvN m), given the symbol and indices of an indexed identifier, if it is one. The checker has verified that the value fits the width of every literal of a checked script.

val numerals_are_real : string -> bool

Whether numerals denote reals in the logic of the given name: it has reals and no integers