Module Libzipperposition_calculi.EnumTypes

Inference and simplification rules for "Enum Types"

Inference rules

An Enum Type is a possibly parametrized type c : type -> type -> ... -> type with an exhaustiveness axiom forall a1....an:type, forall x:(c a1...an), x = t_1 or x = t_2 or ... or x = t_m where the t_i are non-variable terms that contain only x as a variable.

This calculus is designed to remove the axiom (which is very prolific in superposition) and do its job more efficiently.

Inductive types (algebraic types) belong to this category of types, and have additional axioms that are dealt with elsewhere.

We require that the type is as general as possible: either a constant, or a polymorphic type that has only type variables as arguments. Enum types for things like list(int) would be dangerous because if we remove the axiom, because instantiation is a simplification, we won't deal properly with list(rat) (no unification whatsoever)

The rules are:

instantiation of variables:

   C[x] where x:tau unshielded     enum(tau, x in t1....tm)
-----------------------------------------------------------
               C[t_1] or ... or C[tm]

specialization of exhaustiveness for f:

   f : a1 -> ... -> ak -> tau      enum(tau, x in t1....tm)
------------------------------------------------------------
    forall x1:a1, ... xk:ak,
       f(x1...xk)=t1\sigma or .... or f(x1...xk) = tm\sigma
where sigma = {x -> f(x1...xk)}

As Extension