View Source cure_guard_optimizer (cure v0.7.0)
Summary
Functions
Check if Guard1 implies Guard2 (i.e., Guard1 => Guard2) Uses SMT to prove: ∀vars. Guard1 => Guard2
Optimize a list of guards by removing redundant ones
Types
-type expr() :: #literal_expr{value :: term(), location :: term()} | #identifier_expr{name :: term(), location :: term()} | #function_call_expr{function :: term(), args :: term(), location :: term()} | #match_expr{expr :: term(), patterns :: term(), location :: term()} | #let_expr{bindings :: term(), body :: term(), location :: term()} | #binary_op_expr{op :: term(), left :: term(), right :: term(), location :: term()} | #unary_op_expr{op :: term(), operand :: term(), location :: term()} | #list_expr{elements :: term(), location :: term()} | #vector_expr{elements :: term(), location :: term()} | #tuple_expr{elements :: term(), location :: term()} | #record_expr{name :: term(), fields :: term(), location :: term()} | #field_access_expr{record :: term(), field :: term(), location :: term()} | #record_update_expr{name :: term(), base :: term(), fields :: term(), location :: term()} | #lambda_expr{params :: term(), body :: term(), location :: term()} | #forall_expr{variables :: term(), body :: term(), location :: term()} | #exists_expr{variables :: term(), body :: term(), location :: term()} | #fsm_spawn_expr{fsm_name :: term(), init_args :: term(), init_state :: term(), location :: term()} | #fsm_send_expr{target :: term(), message :: term(), location :: term()} | #fsm_receive_expr{patterns :: term(), timeout :: term(), location :: term()} | #fsm_state_expr{location :: term()} | #melquiades_send_expr{message :: term(), target :: term(), location :: term()} | #qualified_call_expr{trait_name :: term(), type_args :: term(), method_name :: term(), receiver :: term(), args :: term(), location :: term()}.
Functions
-spec check_guard_implication(Guard1 :: guard_expr(), Guard2 :: guard_expr()) -> boolean().
Check if Guard1 implies Guard2 (i.e., Guard1 => Guard2) Uses SMT to prove: ∀vars. Guard1 => Guard2
-spec optimize_guards(Guards :: [guard_expr()]) -> [{guard_expr(), optimization_result()}].
Optimize a list of guards by removing redundant ones