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

expr/0

-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

check_guard_implication(Guard1, Guard2)

-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

optimize_guards(Guards)

-spec optimize_guards(Guards :: [guard_expr()]) -> [{guard_expr(), optimization_result()}].

Optimize a list of guards by removing redundant ones