Search.Properties

(source)

The content of this module is based on the paper
Applications of Applicative Proof Search
by Liam O'Connor
https://doi.org/10.1145/2976022.2976030

Reexports

import public Data.Stream
import public Data.Colist
import public Data.Colist1
import public Search.Negation
import public Search.HDecidable
import public Search.Generator

Definitions

Product : List Type -> Type

  Take the product of a list of types

Totality: total
Visibility: public export

record Prop : List Type -> Type -> Type

  A property amenable to testing
  @cs is the list of generators we need (inferrable)
  @a  is the type we hope is inhabited
  NB: the longer the list of generators, the bigger the search space!

Totality: total
Visibility: public export
Constructor:

MkProp : (Colist1 (Product cs) -> Fuel -> HDec a) -> Prop cs a

Projection:

.runProp : Prop cs a -> Colist1 (Product cs) -> Fuel -> HDec a

  The function trying to find an `a` provided generators for `cs`.
  Made total by consuming some fuel along the way.

Hint:

AProp (Prop cs)

.runProp : Prop cs a -> Colist1 (Product cs) -> Fuel -> HDec a

  The function trying to find an `a` provided generators for `cs`.
  Made total by consuming some fuel along the way.

Totality: total
Visibility: public export

runProp : Prop cs a -> Colist1 (Product cs) -> Fuel -> HDec a

  The function trying to find an `a` provided generators for `cs`.
  Made total by consuming some fuel along the way.

Totality: total
Visibility: public export

interface AProp : (Type -> Type) -> Type

  A type constructor satisfying the AProp interface is morally a Prop
  It may not make use of all of the powers granted by Prop, hence the
  associated `Constraints` list of types.

Parameters: t
Methods:

0 Constraints : List Type
toProp : t a -> Prop Constraints a

Implementations:

AProp (Prop cs)
AProp HDec
AProp Dec

0 Constraints : AProp t => List Type

Totality: total
Visibility: public export

toProp : {auto __con : AProp t} -> t a -> Prop Constraints a

Totality: total
Visibility: public export

check : {auto gen : Generator (Product cs)} -> (f : Fuel) -> (p : Prop cs a) -> So (isTrue (runProp p generate f)) => a

  We can run an AProp to try to generate a value of type a

Totality: total
Visibility: public export

exists : {auto aPropt : AProp t} -> ((x : a) -> t (p x)) -> Prop (a :: Constraints) (DPair a p)

  Provided that we know how to generate candidates of type `a`, we can look
  for a witness satisfying a given predicate over `a`.

Totality: total
Visibility: public export