grisette-0.2.0.0: Symbolic evaluation as a library
Copyright(c) Sirui Lu 2021-2023
LicenseBSD-3-Clause (see the LICENSE file)
Maintainersiruilu@cs.washington.edu
StabilityExperimental
PortabilityGHC only
Safe HaskellSafe-Inferred
LanguageHaskell2010

Grisette.Utils

Description

 
Synopsis

Utilities for type-level natural numbers.

Unsafe axiom

unsafeAxiom :: forall a b. a :~: b Source #

Assert a proof of equality between two types. This is unsafe if used improperly, so use this with caution!

Runtime representation of type-level natural numbers

data NatRepr (n :: Nat) Source #

A runtime representation of type-level natural numbers. This can be used for performing dynamic checks on type-level natural numbers.

natValue :: NatRepr n -> Natural Source #

The underlying runtime natural number value of a type-level natural number.

unsafeMkNatRepr :: Natural -> NatRepr n Source #

Construct a runtime representation of a type-level natural number.

Note: This function is unsafe, as it does not check that the runtime representation is consistent with the type-level representation. You should ensure the consistency yourself or the program can crash or generate incorrect results.

natRepr :: forall n. KnownNat n => NatRepr n Source #

Construct a runtime representation of a type-level natural number when its runtime value is known.

decNat :: 1 <= n => NatRepr n -> NatRepr (n - 1) Source #

Decrement a NatRepr by 1.

predNat :: NatRepr (n + 1) -> NatRepr n Source #

Predecessor of a NatRepr

incNat :: NatRepr n -> NatRepr (n + 1) Source #

Increment a NatRepr by 1.

addNat :: NatRepr m -> NatRepr n -> NatRepr (m + n) Source #

Addition of two NatReprs.

subNat :: n <= m => NatRepr m -> NatRepr n -> NatRepr (m - n) Source #

Subtraction of two NatReprs.

divNat :: 1 <= n => NatRepr m -> NatRepr n -> NatRepr (Div m n) Source #

Division of two NatReprs.

halfNat :: NatRepr (n + n) -> NatRepr n Source #

Half of a NatRepr.

Proof of KnownNat

data KnownProof (n :: Nat) where Source #

'KnownProof n' is a type whose values are only inhabited when n has a known runtime value.

Constructors

KnownProof :: KnownNat n => KnownProof n 

hasRepr :: forall n. NatRepr n -> KnownProof n Source #

Construct a KnownProof given the runtime representation.

withKnownProof :: KnownProof n -> (KnownNat n => r) -> r Source #

Introduces the KnownNat constraint when it's proven.

unsafeKnownProof :: Natural -> KnownProof n Source #

Construct a KnownProof given the runtime value.

Note: This function is unsafe, as it does not check that the runtime representation is consistent with the type-level representation. You should ensure the consistency yourself or the program can crash or generate incorrect results.

knownAdd :: forall m n r. KnownProof m -> KnownProof n -> KnownProof (m + n) Source #

Adding two type-level natural numbers with known runtime values gives a type-level natural number with a known runtime value.

Proof of (<=) for type-level natural numbers

data LeqProof (m :: Nat) (n :: Nat) where Source #

'LeqProof m n' is a type whose values are only inhabited when m <= n.

Constructors

LeqProof :: m <= n => LeqProof m n 

withLeqProof :: LeqProof m n -> (m <= n => r) -> r Source #

Introduces the m <= n constraint when it's proven.

unsafeLeqProof :: forall m n. LeqProof m n Source #

Construct a LeqProof.

Note: This function is unsafe, as it does not check that the left-hand side is less than or equal to the right-hand side. You should ensure the consistency yourself or the program can crash or generate incorrect results.

testLeq :: NatRepr m -> NatRepr n -> Maybe (LeqProof m n) Source #

Checks if a NatRepr is less than or equal to another NatRepr.

leqRefl :: f n -> LeqProof n n Source #

Apply reflexivity to LeqProof.

leqSucc :: f n -> LeqProof n (n + 1) Source #

A natural number is less than or equal to its successor.

leqTrans :: LeqProof a b -> LeqProof b c -> LeqProof a c Source #

Apply transitivity to LeqProof.

leqZero :: LeqProof 0 n Source #

Zero is less than or equal to any natural number.

leqAdd2 :: LeqProof xl xh -> LeqProof yl yh -> LeqProof (xl + yl) (xh + yh) Source #

Add both sides of two inequalities.

leqAdd :: LeqProof m n -> f o -> LeqProof m (n + o) Source #

Produce proof that adding a value to the larger element in an LeqProof is larger.

leqAddPos :: (1 <= m, 1 <= n) => p m -> q n -> LeqProof 1 (m + n) Source #

Adding two positive natural numbers is positive.