module EnumTypes:sig
..end
typeterm =
Libzipperposition.FOTerm.t
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:
Cx
where x:tau unshielded enum(tau, x in t1....tm)
-----------------------------------------------------------
Ct_1
or ... or Ctm
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 =
exception Error of string
module type S =sig
..end
module Make:
val extension : Extensions.t