Frex.Signature

Definitions and functions dealing with single-sorted finitary signatures

Definitions

record Signature : Type

  A single-sorted finitary signature

Totality: total
Visibility: public export
Constructor: 

MkSignature : (Nat -> Type) -> Signature

Projection: 

.OpWithArity : Signature -> Nat -> Type

  Type family of operators indexed by their arity.

Hints:

Applicative (Term sig)

sig1 ~> sig2 => Cast (Equation sig1) (Equation sig2)

Cast (SetoidAlgebra sig) Setoid

Cast (Algebra sig) (SetoidAlgebra sig)

Cast (a <~> b) (a ~> b)

Cast (SetoidAlgebra sig) (PresetoidAlgebra sig)

(DecEq (Op sig), DecEq a) => DecEq (Op (EvaluationSig sig a))

(DecEq (Op sig), DecEq a) => DecEq (Term sig a)

(Eq (Op sig), Eq a) => Eq (Op (EvaluationSig sig a))

(Eq (Op sig), Eq a) => Eq (Term sig a)

Functor (Term sig)

Monad (Term sig)

(Ord (Op sig), Ord a) => Ord (Op (EvaluationSig sig a))

(Ord (Op sig), Ord a) => Ord (Term sig a)

pres .signature = sig => Semantic (a <~.~> b) (Op sig)

pres .signature = sig => Semantic (a <~.~> b) (Term sig y)

pres .signature = sig => Semantic (Coproduct a b) (Op sig)

pres .signature = sig => Semantic (Coproduct a b) (Term sig y)

pres .signature = sig => Semantic (Extension a x) (Op sig)

pres .signature = sig => Semantic (Extension a x) (Term sig y)

pres .signature = sig => Semantic (Frex a x) (Op sig)

pres .signature = sig => Semantic (Frex a x) (Term sig y)

pres .signature = sig => Semantic (Model pres) (Op sig)

pres .signature = sig => Semantic (Model pres) (Term sig x)

pres .signature = sig => Semantic (ModelOver pres x) (Op sig)

pres .signature = sig => Semantic (ModelOver pres x) (Term sig y)

pres .signature = sig => Semantic (Free pres x) (Op sig)

pres .signature = sig => Semantic (Free pres x) (Term sig y)

Semantic (Algebra sig) (Op sig)

Semantic (Algebra sig) (Term sig x)

Semantic (SetoidAlgebra sig) (Op sig)

Semantic (SetoidAlgebra sig) (Term sig x)

Show (FreePresetoid sig x u v)

Presentation -> Signature

Uninhabited (Done x = Call f xs)

Uninhabited (Call f xs = Done x)

.OpWithArity : Signature -> Nat -> Type

  Type family of operators indexed by their arity.

Totality: total
Visibility: public export

OpWithArity : Signature -> Nat -> Type

  Type family of operators indexed by their arity.

Totality: total
Visibility: public export

record Op : Signature -> Type

Totality: total
Visibility: public export
Constructor: 

MkOp : sig .OpWithArity arity -> Op sig

Projections:

.arity : Op sig -> Nat

.snd : ({rec:0} : Op sig) -> sig .OpWithArity (arity {rec:0})

Hints:

(DecEq (Op sig), DecEq a) => DecEq (Op (EvaluationSig sig a))

(DecEq (Op sig), DecEq a) => DecEq (Term sig a)

(Eq (Op sig), Eq a) => Eq (Op (EvaluationSig sig a))

(Eq (Op sig), Eq a) => Eq (Term sig a)

(Ord (Op sig), Ord a) => Ord (Op (EvaluationSig sig a))

(Ord (Op sig), Ord a) => Ord (Term sig a)

pres .signature = sig => Semantic (a <~.~> b) (Op sig)

pres .signature = sig => Semantic (Coproduct a b) (Op sig)

pres .signature = sig => Semantic (Extension a x) (Op sig)

pres .signature = sig => Semantic (Frex a x) (Op sig)

pres .signature = sig => Semantic (Model pres) (Op sig)

pres .signature = sig => Semantic (ModelOver pres x) (Op sig)

pres .signature = sig => Semantic (Free pres x) (Op sig)

Semantic (Algebra sig) (Op sig)

Semantic (SetoidAlgebra sig) (Op sig)

Uninhabited (Done x = Call f xs)

Uninhabited (Call f xs = Done x)

.arity : Op sig -> Nat

Totality: total
Visibility: public export

arity : Op sig -> Nat

Totality: total
Visibility: public export

.snd : ({rec:0} : Op sig) -> sig .OpWithArity (arity {rec:0})

Totality: total
Visibility: public export

snd : ({rec:0} : Op sig) -> sig .OpWithArity (arity {rec:0})

Totality: total
Visibility: public export

data Precedence : Nat -> Type

Totality: total
Visibility: public export
Constructors:

Prefix : Nat -> Precedence 1

InfixL : Nat -> Precedence 2

InfixR : Nat -> Precedence 2

Hint: 

Show (Precedence n)

isInfix : Precedence n -> Bool

Totality: total
Visibility: export

level : Precedence n -> Nat

Totality: total
Visibility: export

interface HasPrecedence : Signature -> Type

Parameters: sig
Methods:

OpPrecedence : sig .OpWithArity (S n) -> Maybe (Precedence (S n))

OpPrecedence : HasPrecedence sig => sig .OpWithArity (S n) -> Maybe (Precedence (S n))

Totality: total
Visibility: public export

precedence : HasPrecedence sig => (f : Op sig) -> {auto 0 _ : arity f = S n} -> Maybe (Precedence (S n))

Totality: total
Visibility: export

isInfix : HasPrecedence sig => Op sig -> Bool

Totality: total
Visibility: export

record Printer : Signature -> Type -> Type

Totality: total
Visibility: public export
Constructor: 

MkPrinter : String -> Show a -> Show (Op sig) -> Show (Op sig) -> HasPrecedence sig -> Bool -> Bool -> Printer sig a

Projections:

.carrier : Printer sig a -> String

  Printing the carrier type

.opParens : Printer sig a -> Bool

  Should all infix operators be wrapped in parens

.opPatterns : Printer sig a -> Show (Op sig)

  Patterns for operators

.opPrec : Printer sig a -> HasPrecedence sig

  Operator precedences

.opShow : Printer sig a -> Show (Op sig)

  Operator printing

.topParens : Printer sig a -> Bool

  Should we wrap a term in parens at the toplevel

.varShow : Printer sig a -> Show a

  Variable printing

.carrier : Printer sig a -> String

  Printing the carrier type

Totality: total
Visibility: public export

carrier : Printer sig a -> String

  Printing the carrier type

Totality: total
Visibility: public export

.varShow : Printer sig a -> Show a

  Variable printing

Totality: total
Visibility: public export

varShow : Printer sig a -> Show a

  Variable printing

Totality: total
Visibility: public export

.opPatterns : Printer sig a -> Show (Op sig)

  Patterns for operators

Totality: total
Visibility: public export

opPatterns : Printer sig a -> Show (Op sig)

  Patterns for operators

Totality: total
Visibility: public export

.opShow : Printer sig a -> Show (Op sig)

  Operator printing

Totality: total
Visibility: public export

opShow : Printer sig a -> Show (Op sig)

  Operator printing

Totality: total
Visibility: public export

.opPrec : Printer sig a -> HasPrecedence sig

  Operator precedences

Totality: total
Visibility: public export

opPrec : Printer sig a -> HasPrecedence sig

  Operator precedences

Totality: total
Visibility: public export

.opParens : Printer sig a -> Bool

  Should all infix operators be wrapped in parens

Totality: total
Visibility: public export

opParens : Printer sig a -> Bool

  Should all infix operators be wrapped in parens

Totality: total
Visibility: public export

.topParens : Printer sig a -> Bool

  Should we wrap a term in parens at the toplevel

Totality: total
Visibility: public export

topParens : Printer sig a -> Bool

  Should we wrap a term in parens at the toplevel

Totality: total
Visibility: public export

withQuoted : Printer sig a -> Printer sig a

  The modified names we are using when printing a context rather than
  a term (i.e. a term with an extra variable in scope: the focus).

Totality: total
Visibility: export

display : Printer sig () -> Op sig -> Doc ()

Totality: total
Visibility: export

display : Printer sig () -> Op sig -> Maybe (Doc ())

Totality: total
Visibility: export

display : (sig : Signature) -> Finite (Op sig) => Printer sig () -> Doc ()

Totality: total
Visibility: export