symbol

Documentation

Index

• Constants
• Variables
• type AnalysedExpr
• type BinaryOp
• type BinaryOpExpr
  • func (b BinaryOpExpr) Analyse(tbl Table) (*AnalysedExpr, error)
  • func (b BinaryOpExpr) String() string
• type BracketedExpr
  • func (br BracketedExpr) Analyse(tbl Table) (*AnalysedExpr, error)
  • func (br BracketedExpr) String() string
• type ConstantExpr
  • func (c ConstantExpr) Analyse(tbl Table) (*AnalysedExpr, error)
  • func (c ConstantExpr) String() string
• type Expr
• type Function
  • func (f Function) IsInvocation(params []Parameter) error
  • func (f Function) String() string
  • func (f Function) Table() (Table, error)
• type FunctionSignature
  • func (f FunctionSignature) Table() (Table, error)
• type JustifiableBinaryOpExpr
  • func (b JustifiableBinaryOpExpr) Analyse(tbl Table) (*AnalysedExpr, error)
  • func (b JustifiableBinaryOpExpr) Quantise() RelationChain
  • func (b JustifiableBinaryOpExpr) String() string
• type LabelledChain
  • func (c LabelledChain) Label() string
• type LambdaExpr
  • func (λ LambdaExpr) Analyse(tbl Table) (*AnalysedExpr, error)
  • func (λ LambdaExpr) String() string
  • func (λ LambdaExpr) Table() (Table, error)
• type LambdaProof
  • func (prf LambdaProof) Burden() (Expr, error)
  • func (prf LambdaProof) Chain() RelationChain
  • func (prf LambdaProof) Label() string
• type LocalProof
  • func (lp LocalProof) Table() (Table, error)
• type NegatedExpr
  • func (n NegatedExpr) Analyse(tbl Table) (*AnalysedExpr, error)
  • func (n NegatedExpr) String() string
• type Operator
  • func (op Operator) SimpleTruthOp() BinaryOp
• type Parameter
• type PostfixExpr
  • func (p PostfixExpr) Analyse(tbl Table) (*AnalysedExpr, error)
  • func (p PostfixExpr) String() string
• type Proof
• type ProofChain
• type RelationChain
  • func (rel RelationChain) Burden() (Expr, error)
  • func (rel RelationChain) Chain() RelationChain
  • func (rel RelationChain) GCFOperator() (Operator, error)
  • func (rel RelationChain) Label() string
• type Scope
• type SimpleExpr
  • func (p SimpleExpr) Analyse(tbl Table) (*AnalysedExpr, error)
  • func (p SimpleExpr) String() string
• type Table
  • func (T Table) Nest(Parent Table) Table
• type Template
  • func (t Template) IsInvocation(params []Parameter) error
  • func (t Template) String() string
  • func (t Template) Table() (Table, error)
• type Type
  • func (p Type) Table() (Table, error)

Constants

const (
	And  Operator = "&&"
	Or            = "||"
	Eqv           = "==="
	Impl          = "==>"
	Fllw          = "<=="
)

Variables

var ErrNoCommonOperator = errors.New("no common operator")

Types

type AnalysedExpr

type AnalysedExpr struct {
	P truth.Proposition
	// contains filtered or unexported fields
}

type BinaryOp

type BinaryOp func(truth.Proposition, truth.Proposition) truth.Proposition

type BinaryOpExpr

type BinaryOpExpr struct {
	Op     Operator
	E1, E2 Expr
}

func (BinaryOpExpr) Analyse

func (b BinaryOpExpr) Analyse(tbl Table) (*AnalysedExpr, error)

func (BinaryOpExpr) String

func (b BinaryOpExpr) String() string

type BracketedExpr

type BracketedExpr struct {
	Expr
}

func (BracketedExpr) Analyse

func (br BracketedExpr) Analyse(tbl Table) (*AnalysedExpr, error)

func (BracketedExpr) String

func (br BracketedExpr) String() string

type ConstantExpr

type ConstantExpr bool

func (ConstantExpr) Analyse

func (c ConstantExpr) Analyse(tbl Table) (*AnalysedExpr, error)

func (ConstantExpr) String

func (c ConstantExpr) String() string

type Expr

type Expr interface {
	Analyse(Table) (*AnalysedExpr, error)
	String() string
	// contains filtered or unexported methods
}

Expr is the interface describing the AST nodes that are processed into "pure" first-order logic expressions evaluated by the truth package.

type Function

type Function struct {
	IsAxiom bool
	Sig     FunctionSignature
	Name    string
}

func (Function) IsInvocation

func (f Function) IsInvocation(params []Parameter) error

func (Function) String

func (f Function) String() string

func (Function) Table

func (f Function) Table() (Table, error)

type FunctionSignature

type FunctionSignature struct {
	Params []Parameter
	Return Type
}

func (FunctionSignature) Table

func (f FunctionSignature) Table() (Table, error)

type JustifiableBinaryOpExpr

type JustifiableBinaryOpExpr struct {
	BinaryOpExpr
	Just *PostfixExpr
}

func (JustifiableBinaryOpExpr) Analyse

func (b JustifiableBinaryOpExpr) Analyse(tbl Table) (*AnalysedExpr, error)

func (JustifiableBinaryOpExpr) Quantise

func (b JustifiableBinaryOpExpr) Quantise() RelationChain

Quantise takes a JustifiableBinaryOpExpr that is a relation (i.e. has as its operation one of the links) and breaks it into a sequence of relations that can be evaluated one-by-one in order to compute the truth or falsehood of the original relation.

func (JustifiableBinaryOpExpr) String

func (b JustifiableBinaryOpExpr) String() string

type LabelledChain

type LabelledChain struct {
	RelationChain
	L string
}

func (LabelledChain) Label

func (c LabelledChain) Label() string

type LambdaExpr

type LambdaExpr struct {
	Params []Parameter
	Expr   Expr
}

func (LambdaExpr) Analyse

func (λ LambdaExpr) Analyse(tbl Table) (*AnalysedExpr, error)

func (LambdaExpr) String

func (λ LambdaExpr) String() string

func (LambdaExpr) Table

func (λ LambdaExpr) Table() (Table, error)

type LambdaProof

type LambdaProof struct {
	E LambdaExpr
	L string
}

func (LambdaProof) Burden

func (prf LambdaProof) Burden() (Expr, error)

func (LambdaProof) Chain

func (prf LambdaProof) Chain() RelationChain

func (LambdaProof) Label

func (prf LambdaProof) Label() string

type LocalProof

type LocalProof struct {
	Expr Expr
}

func (LocalProof) Table

func (lp LocalProof) Table() (Table, error)

type NegatedExpr

type NegatedExpr struct {
	Expr
}

func (NegatedExpr) Analyse

func (n NegatedExpr) Analyse(tbl Table) (*AnalysedExpr, error)

func (NegatedExpr) String

func (n NegatedExpr) String() string

type Operator

type Operator string

func (Operator) SimpleTruthOp

func (op Operator) SimpleTruthOp() BinaryOp

type Parameter

type Parameter struct {
	Name string
	Type
}

type PostfixExpr

type PostfixExpr struct {
	Name string
	Args []Expr
}

func (PostfixExpr) Analyse

func (p PostfixExpr) Analyse(tbl Table) (*AnalysedExpr, error)

func (PostfixExpr) String

func (p PostfixExpr) String() string

type Proof

type Proof interface {
	Chain() RelationChain
	Burden() (Expr, error)
	Label() string
}

type ProofChain

type ProofChain struct {
	Preamble []Proof
	Proof    Proof
}

type RelationChain

type RelationChain []JustifiableBinaryOpExpr

RelationChain is a series of JustifiableBinaryOpExpr's each with the operation being one of the links, i.e. `==>`, `===`, or `<==`.

func (RelationChain) Burden

func (rel RelationChain) Burden() (Expr, error)

func (RelationChain) Chain

func (rel RelationChain) Chain() RelationChain

func (RelationChain) GCFOperator

func (rel RelationChain) GCFOperator() (Operator, error)

GCF returns the greatest-common-factor-operator, if it exists, or an error otherwise.

func (RelationChain) Label

func (rel RelationChain) Label() string

type Scope

type Scope interface {
	Table() (Table, error)
}

type SimpleExpr

type SimpleExpr string

func (SimpleExpr) Analyse

func (p SimpleExpr) Analyse(tbl Table) (*AnalysedExpr, error)

func (SimpleExpr) String

func (p SimpleExpr) String() string

type Table

type Table map[string]Scope

func (Table) Nest

func (T Table) Nest(Parent Table) Table

type Template

type Template struct {
	IsAxiom bool
	Params  []Parameter
	E       Expr
	Proofs  []ProofChain
	Name    string
}

func (Template) IsInvocation

func (t Template) IsInvocation(params []Parameter) error

func (Template) String

func (t Template) String() string

func (Template) Table

func (t Template) Table() (Table, error)

type Type

type Type string

const (
	Any  Type = "any"
	Bool      = "bool"
)

func (Type) Table

func (p Type) Table() (Table, error)