Core.Case.CaseTree

Definitions

data CaseTree : Scoped

  Case trees in A-normal forms
  i.e. we may only dispatch on variables, not expressions

Totality: total
Visibility: public export
Constructors:

Case : (idx : Nat) -> (0 _ : IsVar name idx vars) -> Term vars -> List (CaseAlt vars) -> CaseTree vars

  case x return scTy of { p1 => e1 ; ... }

STerm : Int -> Term vars -> CaseTree vars

  RHS: no need for further inspection
  The Int is a clause id that allows us to see which of the
  initial clauses are reached in the tree

Unmatched : String -> CaseTree vars

  error from a partial match

Impossible : CaseTree vars

  Absurd context

Hints:

FreelyEmbeddable CaseTree

HasNames (CaseTree vars)

Hashable (CaseTree vars)

Show (CaseTree vars)

StripNamespace (CaseTree vars)

TTC (CaseTree vars)

Weaken CaseTree

data CaseAlt : Scoped

  Case alternatives. Unlike arbitrary patterns, they can be at most
  one constructor deep.

Totality: total
Visibility: public export
Constructors:

ConCase : Name -> Int -> (args : List Name) -> CaseTree (addInner vars args) -> CaseAlt vars

  Constructor for a data type; bind the arguments and subterms.

DelayCase : (ty : Name) -> (arg : Name) -> CaseTree (addInner vars [ty, arg]) -> CaseAlt vars

  Lazy match for the Delay type use for codata types

ConstCase : Constant -> CaseTree vars -> CaseAlt vars

  Match against a literal

DefaultCase : CaseTree vars -> CaseAlt vars

  Catch-all case

Hints:

HasNames (CaseAlt vars)

Hashable (CaseAlt vars)

Show (CaseAlt vars)

StripNamespace (CaseAlt vars)

TTC (CaseAlt vars)

measure : CaseTree vars -> Nat

Visibility: public export

isDefault : CaseAlt vars -> Bool

Visibility: export

data Pat : Type

Totality: total
Visibility: public export
Constructors:

PAs : FC -> Name -> Pat -> Pat

PCon : FC -> Name -> Int -> Nat -> List Pat -> Pat

PTyCon : FC -> Name -> Nat -> List Pat -> Pat

PConst : FC -> Constant -> Pat

PArrow : FC -> Name -> Pat -> Pat -> Pat

PDelay : FC -> LazyReason -> Pat -> Pat -> Pat

PLoc : FC -> Name -> Pat

PUnmatchable : FC -> ClosedTerm -> Pat

Hints:

HasNames Pat

Hashable Pat

Pretty IdrisSyntax Pat

Show Pat

TTC Pat

isPConst : Pat -> Maybe Constant

Visibility: export

0 isConPat : Pat -> Bool

Visibility: public export

0 IsConPat : Pat -> Type

Visibility: public export

eqTree : CaseTree vs -> CaseTree vs' -> Bool

Visibility: export

getRefs : Name -> CaseTree vars -> NameMap Bool

Visibility: export

addRefs : Name -> NameMap Bool -> CaseTree vars -> NameMap Bool

Visibility: export

getMetas : CaseTree vars -> NameMap Bool

Visibility: export

mkTerm : (vars : Scope) -> Pat -> Term vars

Visibility: export