Algebra.Solver.Monoid

Reexports

Definitions

data Expr : (a : Type) -> List a -> Type

  Tree representing an algebraic expression in a monoid structure.
  
  The idea here is to represent algebraic expressions as an `Expr a as`,
  where `a` is the type we operate on and `as` is a list of known
  variables. Such an `Expr a as` can then be normalized using function
  `normalize`. We proof in this module, that the result of evaluating an
  expression is not affected by normalization. Hence, if two expressions
  `e1` and `e2` have the same normalized representation, the results
  of evaluating the two (`eval e1` and `eval e2`) are propositionally
  equal. This is, what function `solve` is used for.

Totality: total
Visibility: public export
Constructors:

Lit : a -> Expr a as

  A literal value known at compile time. Use this if you want
  values known at runtime to unify.

Var : (x : a) -> Elem x as -> Expr a as

  A variable from the given list of variables.

Neutral : Expr a as

  Represents the neutral element of the monoid

(<+>) : Expr a as -> Expr a as -> Expr a as

  Represents the binary operation of the monoid

data Term : (a : Type) -> List a -> Type

  An `Expr a as` is normalized to a sequence of terms of type
  `List (Term a as)`.

Totality: total
Visibility: public export
Constructors:

TLit : a -> Term a as

TVar : (x : a) -> Elem x as -> Term a as

var : (x : a) -> Elem x xs => Expr a xs

  Alias for `var` that uses an auto-implicit proof of `Elem x xs`.

Totality: total
Visibility: public export

(.+>) : (x : a) -> Expr a xs -> Elem x xs => Expr a xs

  Alias for `var x <+> y`

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 8

(<+.) : Expr a xs -> (x : a) -> Elem x xs => Expr a xs

  Alias for `x <+> var y`

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 8

(.+.) : (x : a) -> (y : a) -> Elem x xs => Elem y xs => Expr a xs

  Alias for `var x .+. var y`

Totality: total
Visibility: public export
Fixity Declarations:
infixl operator, level 8
infixl operator, level 8

eval : (0 _ : Monoid a z p) -> Expr a as -> a

  Evaluates an expression over the given monoid.
  Note: The idea is to use this function at compile-time to
        convert the expression we evaluate to the corresponding
        Idris expression.

Totality: total
Visibility: public export

eterm : Term a as -> a

  Evaluates a single term.

Totality: total
Visibility: public export

elist : (0 _ : Monoid a z p) -> List (Term a as) -> a

  Evaluates a list of terms over the given monoid.

Totality: total
Visibility: public export

flatten : Expr a as -> List (Term a as)

  Flattens an expression into a list of terms

Totality: total
Visibility: public export

fuse : (0 _ : Monoid a z p) -> ((v : a) -> Maybe (v = z)) -> Term a as -> Term a as -> List (Term a as)

  Tries to fuse two neighbouring terms

Totality: total
Visibility: public export

prepend : (0 _ : Monoid a z p) -> ((v : a) -> Maybe (v = z)) -> List (Term a as) -> Term a as -> List (Term a as)

  Prepends a single term in front of a list of terms.
  This will remove terms that evaluate to zero and
  fuse neighbouring literals.

Totality: total
Visibility: public export

merge : (0 _ : Monoid a z p) -> ((v : a) -> Maybe (v = z)) -> List (Term a as) -> List (Term a as)

Totality: total
Visibility: public export

normalize : (0 _ : Monoid a z p) -> ((v : a) -> Maybe (v = z)) -> Expr a as -> List (Term a as)

Totality: total
Visibility: public export

0 solve : (m : Monoid a z p) -> (isZ : ((x : a) -> Maybe (x = z))) -> (e1 : Expr a as) -> (e2 : Expr a as) -> normalize m isZ e1 = normalize m isZ e2 => eval m e1 = eval m e2

Totality: total
Visibility: export