gillian » Gillian » Symbolic » FO_logic » Reduction

Module FO_logic.Reduction

exceptionReductionException of Gil_syntax.Expr.t * string

ReductionException (e, msg) denotes an exception raised due to an expression e being malformed with explanation msg

val resolve_expr_to_location :
  Pure_context.t ->
  Type_env.t ->
  Gil_syntax.Expr.t ->
  string option

resolve_to_location pfs e attempts to resolve the expression denoted by e to a location given the pure formulae pfs. If successful, it returns that location, together with any bindings learned during the resolution.

val get_equal_expressions :
  Pure_context.t ->
  Gil_syntax.Expr.t ->
  Gil_syntax.Expr.t list

get_equal_expressions pfs e returns a list of expressions that equal e under the pure formulae pfs.

val understand_lstcat :
  Pure_context.t ->
  Type_env.t ->
  Gil_syntax.Expr.t list ->
  Gil_syntax.Expr.t list ->
  (Gil_syntax.Expr.t * Utils.Containers.SS.t) option

val reduce_lexpr :
  ?matching:bool ->
  ?reduce_lvars:bool ->
  ?pfs:Pure_context.t ->
  ?gamma:Type_env.t ->
  Gil_syntax.Expr.t ->
  Gil_syntax.Expr.t

reduce_lexpr ?matching ?reduce_lvars ?pfs ?gamma e reduces the expression e given (optional) pure formulae pfs and typing environment gamma. The reduce_lvars and matching flags should not be used by Gillian instantiation developers.

val reduce_assertion :
  ?matching:bool ->
  ?pfs:Pure_context.t ->
  ?gamma:Type_env.t ->
  Gil_syntax.Asrt.t ->
  Gil_syntax.Asrt.t

reduce_assertion ?matching ?pfs ?gamma a reduces the assertion a given (optional) pure formulae pfs and typing environment gamma. The matching flag should not be used by Gillian instantiation developers.

val is_tautology :
  ?pfs:Pure_context.t ->
  ?gamma:Type_env.t ->
  Gil_syntax.Expr.t ->
  bool