package libzipperposition

  1. Overview
  2. Docs
package libzipperposition
Legend:
Library
Module
Module type
Parameter
Class
Class type

Inference and simplification rules for "Enum Types"

type term = Logtk.Term.t

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:

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 = x -> f(x1...xk)

exception Error of string
module type S = sig ... end
module Make (E : Libzipperposition.Env.S) : S with module Env = E

As Extension

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct