FO_logic.Reductionexception ReductionException of Gil_syntax.Expr.t * stringReductionException (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 optionresolve_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 listget_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.Formula.t * Utils.Containers.SS.t) optionval reduce_lexpr :
?matching:bool ->
?reduce_lvars:bool ->
?pfs:Pure_context.t ->
?gamma:Type_env.t ->
Gil_syntax.Expr.t ->
Gil_syntax.Expr.treduce_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_formula :
?matching:bool ->
?rpfs:bool ->
?time:string ->
?pfs:Pure_context.t ->
?gamma:Type_env.t ->
Gil_syntax.Formula.t ->
Gil_syntax.Formula.treduce_formula ?matching ?pfs ?gamma pf reduces the formula pf given (optional) pure formulae pfs and typing environment gamma. The matching flag 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.treduce_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.Formula.t ->
bool