Module Kat.Optimize

Constants

val ctrue : 'test Ast.bexp
val cfalse : 'test Ast.bexp
val skip : ('act, 'test) Ast.exp
val abort : ('act, 'test) Ast.exp

(Optimizing) smart constructors

val test : 'test -> 'test Ast.bexp
val disj : 'test Ast.bexp -> 'test Ast.bexp -> 'test Ast.bexp
val conj : 'test Ast.bexp -> 'test Ast.bexp -> 'test Ast.bexp
val neg : 'test Ast.bexp -> 'test Ast.bexp
val assrt : 'test Ast.bexp -> ('act, 'test) Ast.exp
val action : 'act -> ('act, 'test) Ast.exp
val union : ('act, 'test) Ast.exp -> ('act, 'test) Ast.exp -> ('act, 'test) Ast.exp
val seq : ('act, 'test) Ast.exp -> ('act, 'test) Ast.exp -> ('act, 'test) Ast.exp
val star : ('act, 'test) Ast.exp -> ('act, 'test) Ast.exp
val ite : 'test Ast.bexp -> ('act, 'test) Ast.exp -> ('act, 'test) Ast.exp -> ('act, 'test) Ast.exp

N-ary constructors

val big_disj : 'test Ast.bexp list -> 'test Ast.bexp
val big_conj : 'test Ast.bexp list -> 'test Ast.bexp
val big_union : ('act, 'test) Ast.exp list -> ('act, 'test) Ast.exp
val big_seq : ('act, 'test) Ast.exp list -> ('act, 'test) Ast.exp

Algebraic optimization

val optimize_bexp : ?⁠negate:bool -> ?⁠neg_test:('test -> 'test) -> 'test Ast.bexp -> 'test Ast.bexp
val optimize_exp : ?⁠neg_test:('test -> 'test) -> ('act, 'test) Ast.exp -> ('act, 'test) Ast.exp
val normalize_rassoc_exp : ('act, 'test) Ast.exp -> ('act, 'test) Ast.exp

Given an e: exp in which union and seq associate strictly to the right, returns normalized expression normalize_rassoc_exp e such that:

  • union and seq associative strictly to the left
  • boolean expressions expand as far as possible in the following sense:
  • assert b1; assert b2 ~> assert (b1; b2)
  • assert b1 + assert b2 ~> assert (b1 + b2)
raises Invalid_argument

if input expression is not strictly right-associative.