Algebra.Solver.Group

Reexports

Definitions

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

Totality: total
Visibility: public export
Constructors:

Lit : a -> Expr a as

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

Neutral : Expr a as

Neg : Expr a as -> Expr a as

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

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

Totality: total
Visibility: public export
Constructors:

TLit : a -> Term a as

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

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

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

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

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

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

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

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

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

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

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

  Evaluates an expression over the given group.
  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 : (a -> a) -> Term a as -> a

  Evaluates a single term.

Totality: total
Visibility: public export

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

  Evaluates a list of terms over the given monoid.

Totality: total
Visibility: public export

negSng : (a -> a) -> Term a as -> Term a as

  Negates a single term.

Totality: total
Visibility: public export

negate : (a -> a) -> List (Term a as) -> List (Term a as) -> List (Term a as)

  Negates a list of terms using the given inverse function.
  
  This will - according to the usual group laws -
  invert the order of elements.

Totality: total
Visibility: public export
Fixity Declaration: prefix operator, level 10

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

  Flattens an expression into a list of terms, using the given inverse
  function for negation.

Totality: total
Visibility: public export

fuse : (0 _ : Group a z i 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 _ : Group a z i 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 _ : Group a z i p) -> ((v : a) -> Maybe (v = z)) -> List (Term a as) -> List (Term a as)

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

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

Totality: total
Visibility: export