package TCSLib

  1. Overview
  2. Docs
package TCSLib
Legend:
Library
Module
Module type
Parameter
Class
Class type
type arithm_expr =
  1. | AConst of int
  2. | ASum of arithm_expr * arithm_expr
  3. | ANeg of arithm_expr
  4. | AProd of arithm_expr * arithm_expr
  5. | ADiv of arithm_expr * arithm_expr
  6. | AMod of arithm_expr * arithm_expr
  7. | AArithmVar of string
type indentifier =
  1. | IDefault of string
  2. | IIndexed of string * arithm_expr
type formal_param =
  1. | PFormulaVar of string
  2. | PArithmVar of string
type actual_param =
  1. | PFormula of formula_expr
  2. | PArithmExpr of arithm_expr
and formula_expr =
  1. | FProp of indentifier
  2. | FVariable of indentifier
  3. | Ftt
  4. | Fff
  5. | FNeg of formula_expr
  6. | FOr of formula_expr * formula_expr
  7. | FAnd of formula_expr * formula_expr
  8. | FQuantor of string * indentifier * formula_expr
  9. | FUnaryOp of string * formula_expr
  10. | FBinaryOp of string * formula_expr * formula_expr
  11. | FLabelledOp of string * formula_expr * formula_expr
  12. | FFormulaIdent of string * actual_param list
type condition =
  1. | CondTT
  2. | CondFF
  3. | CondNot of condition
  4. | CondAnd of condition * condition
  5. | CondOr of condition * condition
  6. | CondEq of arithm_expr * arithm_expr
  7. | CondGreater of arithm_expr * arithm_expr
type cond_expression = condition * formula_expr
type formula_def = string * formal_param list * cond_expression list
type environment = formula_def list
val eval_formula : formula_expr -> (string * formal_param list * (condition * formula_expr) list) list -> formula_expr
val identifier_to_str : indentifier -> string
val as_identifier_to_str : formula_expr -> string