Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.DiscrimTree.Types

Synopsis

- data Key
  - = RigidK !QName !Int
  - | LocalK !Int !Int
  - | PiK Hiding
  - | ConstK
  - | SortK
  - | FlexK
- data DiscrimTree a
  - = EmptyDT
  - | DoneDT (Set a)
  - | CaseDT !Int (Map Key (DiscrimTree a)) (DiscrimTree a)
- mergeDT :: Ord a => DiscrimTree a -> DiscrimTree a -> DiscrimTree a
- singletonDT :: [Key] -> a -> DiscrimTree a

# Documentation

data Key Source #

Constructors

RigidK !QName !Int | Rigid symbols (constructors, data types, record types, postulates) identified by a QName.
LocalK !Int !Int | Local variables.
PiK Hiding | Dependent function types. The domain will be represented accurately, for the case of a genuine dependent function type, the codomain will be a dummy.
ConstK | Constant lambdas.
SortK | Universes.
FlexK | Anything else.

#### Instances

Instances details

PrettyTCM Key Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Key -> m Doc Source #
EmbPrj Key Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Key -> S Word32 Source # icod_ :: Key -> S Word32 Source # value :: Word32 -> R Key Source #
NFData Key Source # |
Instance details Defined in Agda.TypeChecking.DiscrimTree.Types Methods rnf :: Key -> () Source #
Generic Key Source # |

Instance details

Defined in Agda.TypeChecking.DiscrimTree.Types

Associated Types

type Rep Key |

Instance details

Defined in Agda.TypeChecking.DiscrimTree.Types

type Rep Key = D1 ('MetaData "Key" "Agda.TypeChecking.DiscrimTree.Types" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) ((C1 ('MetaCons "RigidK" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 Int)) :+: (C1 ('MetaCons "LocalK" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 Int)) :+: C1 ('MetaCons "PiK" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Hiding)))) :+: (C1 ('MetaCons "ConstK" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "SortK" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FlexK" 'PrefixI 'False) (U1 :: Type -> Type))))

Methods

from :: Key -> Rep Key x Source #

to :: Rep Key x -> Key Source #

Show Key Source # |
Instance details Defined in Agda.TypeChecking.DiscrimTree.Types Methods showsPrec :: Int -> Key -> ShowS Source # show :: Key -> String Source # showList :: [Key] -> ShowS Source #
Eq Key Source # |
Instance details Defined in Agda.TypeChecking.DiscrimTree.Types Methods (==) :: Key -> Key -> Bool Source # (/=) :: Key -> Key -> Bool Source #
Ord Key Source # |
Instance details Defined in Agda.TypeChecking.DiscrimTree.Types Methods compare :: Key -> Key -> Ordering Source # (<) :: Key -> Key -> Bool Source # (<=) :: Key -> Key -> Bool Source # (>) :: Key -> Key -> Bool Source # (>=) :: Key -> Key -> Bool Source # max :: Key -> Key -> Key Source # min :: Key -> Key -> Key Source #
type Rep Key Source # |

Instance details

Defined in Agda.TypeChecking.DiscrimTree.Types

type Rep Key = D1 ('MetaData "Key" "Agda.TypeChecking.DiscrimTree.Types" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) ((C1 ('MetaCons "RigidK" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 Int)) :+: (C1 ('MetaCons "LocalK" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 Int)) :+: C1 ('MetaCons "PiK" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Hiding)))) :+: (C1 ('MetaCons "ConstK" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "SortK" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FlexK" 'PrefixI 'False) (U1 :: Type -> Type))))

data DiscrimTree a Source #

A `Term`-indexed associative data structure supporting approximate (conservative) lookup. Rather than using a `Trie` keyed by `Key` directly, a `DiscrimTree` is instead represented more like a case tree.

This allows us to exploit the fact that instance selection often focuses on a small part of the term: Only that critical chain is represented in the tree. As an example, level parameters are unlikely to contribute to narrowing a search problem, so it would be wasteful to have an indirection in the tree for every `FlexK` standing for a level parameter.

Constructors

EmptyDT | The empty discrimination tree.
DoneDT (Set a) | Succeed with a given set of values.
CaseDT | Do case analysis on a term. `CaseDT` is scoped in the same way as fast case trees for the abstract machine: When matching actually succeeds, the variable that was matched gets replaced by its arguments directly in the context.

Fields

- !Int

  The variable to case on.

- (Map Key (DiscrimTree a))

  The proper branches.

- (DiscrimTree a)

  A further tree, which should always be explored.

#### Instances

Instances details

(KillRange a, Ord a) => KillRange (DiscrimTree a) Source # |
Instance details Defined in Agda.TypeChecking.DiscrimTree.Types Methods killRange :: KillRangeT (DiscrimTree a) Source #
PrettyTCM a => PrettyTCM (DiscrimTree a) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => DiscrimTree a -> m Doc Source #
(EmbPrj a, Ord a) => EmbPrj (DiscrimTree a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: DiscrimTree a -> S Word32 Source # icod_ :: DiscrimTree a -> S Word32 Source # value :: Word32 -> R (DiscrimTree a) Source #
Null (DiscrimTree a) Source # |
Instance details Defined in Agda.TypeChecking.DiscrimTree.Types Methods empty :: DiscrimTree a Source # null :: DiscrimTree a -> Bool Source #
NFData a => NFData (DiscrimTree a) Source # |
Instance details Defined in Agda.TypeChecking.DiscrimTree.Types Methods rnf :: DiscrimTree a -> () Source #
Ord a => Monoid (DiscrimTree a) Source # |
Instance details Defined in Agda.TypeChecking.DiscrimTree.Types Methods mempty :: DiscrimTree a Source # mappend :: DiscrimTree a -> DiscrimTree a -> DiscrimTree a Source # mconcat :: [DiscrimTree a] -> DiscrimTree a Source #
Ord a => Semigroup (DiscrimTree a) Source # |
Instance details Defined in Agda.TypeChecking.DiscrimTree.Types Methods (<>) :: DiscrimTree a -> DiscrimTree a -> DiscrimTree a Source # sconcat :: NonEmpty (DiscrimTree a) -> DiscrimTree a Source # stimes :: Integral b => b -> DiscrimTree a -> DiscrimTree a Source #
Generic (DiscrimTree a) Source # |

Instance details

Defined in Agda.TypeChecking.DiscrimTree.Types

Associated Types

type Rep (DiscrimTree a) |

Instance details

Defined in Agda.TypeChecking.DiscrimTree.Types

type Rep (DiscrimTree a) = D1 ('MetaData "DiscrimTree" "Agda.TypeChecking.DiscrimTree.Types" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "EmptyDT" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "DoneDT" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set a))) :+: C1 ('MetaCons "CaseDT" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Key (DiscrimTree a))) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (DiscrimTree a))))))

Methods

from :: DiscrimTree a -> Rep (DiscrimTree a) x Source #

to :: Rep (DiscrimTree a) x -> DiscrimTree a Source #

Show a => Show (DiscrimTree a) Source # |
Instance details Defined in Agda.TypeChecking.DiscrimTree.Types Methods showsPrec :: Int -> DiscrimTree a -> ShowS Source # show :: DiscrimTree a -> String Source # showList :: [DiscrimTree a] -> ShowS Source #
Eq a => Eq (DiscrimTree a) Source # |
Instance details Defined in Agda.TypeChecking.DiscrimTree.Types Methods (==) :: DiscrimTree a -> DiscrimTree a -> Bool Source # (/=) :: DiscrimTree a -> DiscrimTree a -> Bool Source #
type Rep (DiscrimTree a) Source # |

Instance details

Defined in Agda.TypeChecking.DiscrimTree.Types

type Rep (DiscrimTree a) = D1 ('MetaData "DiscrimTree" "Agda.TypeChecking.DiscrimTree.Types" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "EmptyDT" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "DoneDT" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set a))) :+: C1 ('MetaCons "CaseDT" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Key (DiscrimTree a))) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (DiscrimTree a))))))

mergeDT :: Ord a => DiscrimTree a -> DiscrimTree a -> DiscrimTree a Source #

Merge a pair of discrimination trees. This function tries to build the minimal discrimination tree that yields the union of the inputs' results, though it does so slightly naïvely, without considerable optimisations (e.g. it does not turn single-alternative `CaseDT`s into `DoneDT`s).

singletonDT :: [Key] -> a -> DiscrimTree a Source #

Construct the case tree corresponding to only performing proper matches on the given key. In this context, a "proper match" is any `Key` that is not `FlexK`.