| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Mikan.TypeChecking.Free.Base
Synopsis
- newtype MetaSet = MetaSet {}
- insertMetaSet :: MetaId -> MetaSet -> MetaSet
- foldrMetaSet :: (MetaId -> a -> a) -> a -> MetaSet -> a
- metaSetToBlocker :: MetaSet -> Blocker
- data FlexRig' a
- = Flexible !a
- | WeaklyRigid
- | Unguarded
- | StronglyRigid
- type FlexRig = FlexRig' MetaSet
- class LensFlexRig o a | o -> a where
- lensFlexRig :: Lens' o (FlexRig' a)
- isFlexible :: LensFlexRig o a => o -> Bool
- isUnguarded :: LensFlexRig o a => o -> Bool
- isWeaklyRigid :: LensFlexRig o a => o -> Bool
- isStronglyRigid :: LensFlexRig o a => o -> Bool
- addFlexRig :: Semigroup a => FlexRig' a -> FlexRig' a -> FlexRig' a
- zeroFlexRig :: Monoid a => FlexRig' a
- omegaFlexRig :: FlexRig' a
- composeFlexRig :: Semigroup a => FlexRig' a -> FlexRig' a -> FlexRig' a
- oneFlexRig :: FlexRig' a
- flexRigToBlocker :: FlexRig -> Blocker
- data VarOcc' a = VarOcc {
- varFlexRig :: !(FlexRig' a)
- type VarOcc = VarOcc' MetaSet
- topVarOcc :: VarOcc' a
- composeVarOcc :: Semigroup a => VarOcc' a -> VarOcc' a -> VarOcc' a
- oneVarOcc :: VarOcc' a
- constructorFlexRig :: ConHead -> Elims -> FlexRig' a
- type TheVarMap' a = IntMap (VarOcc' a)
- newtype VarMap' a = VarMap {
- theVarMap :: TheVarMap' a
- type TheVarMap = TheVarMap' MetaSet
- type VarMap = VarMap' MetaSet
- mapVarMap :: (TheVarMap' a -> TheVarMap' b) -> VarMap' a -> VarMap' b
- lookupVarMap :: Variable -> VarMap' a -> Maybe (VarOcc' a)
- newtype VarCounts = VarCounts {}
- data IgnoreSorts
- type Variable = Int
- type SingleVar c = Variable -> c
Set of meta variables.
A set of meta variables. Forms a monoid under union.
Constructors
| MetaSet | |
Fields | |
foldrMetaSet :: (MetaId -> a -> a) -> a -> MetaSet -> a Source #
metaSetToBlocker :: MetaSet -> Blocker Source #
Flexible and rigid occurrences (semigroup)
Depending on the surrounding context of a variable, it's occurrence can be classified as flexible or rigid, with finer distinctions.
The constructors are listed in increasing order (wrt. information content).
Constructors
| Flexible !a | In arguments of metas.
The set of metas is used by ' |
| WeaklyRigid | In arguments to variables and definitions. |
| Unguarded | In top position, or only under inductive record constructors (unit). |
| StronglyRigid | Under at least one and only inductive constructors. |
Instances
| Functor FlexRig' Source # | |
| Foldable FlexRig' Source # | |
Defined in Mikan.TypeChecking.Free.Base Methods fold :: Monoid m => FlexRig' m -> m # foldMap :: Monoid m => (a -> m) -> FlexRig' a -> m # foldMap' :: Monoid m => (a -> m) -> FlexRig' a -> m # foldr :: (a -> b -> b) -> b -> FlexRig' a -> b # foldr' :: (a -> b -> b) -> b -> FlexRig' a -> b # foldl :: (b -> a -> b) -> b -> FlexRig' a -> b # foldl' :: (b -> a -> b) -> b -> FlexRig' a -> b # foldr1 :: (a -> a -> a) -> FlexRig' a -> a # foldl1 :: (a -> a -> a) -> FlexRig' a -> a # elem :: Eq a => a -> FlexRig' a -> Bool # maximum :: Ord a => FlexRig' a -> a # minimum :: Ord a => FlexRig' a -> a # | |
| Pretty a => Pretty (FlexRig' a) Source # | |
| PrettyTCM a => PrettyTCM (FlexRig' a) Source # | |
Defined in Mikan.TypeChecking.Pretty | |
| Show a => Show (FlexRig' a) Source # | |
| Eq a => Eq (FlexRig' a) Source # | |
| LensFlexRig (FlexRig' a) a Source # | |
Defined in Mikan.TypeChecking.Free.Base | |
class LensFlexRig o a | o -> a where Source #
Methods
lensFlexRig :: Lens' o (FlexRig' a) Source #
Instances
| LensFlexRig (FlexRig' a) a Source # | |
Defined in Mikan.TypeChecking.Free.Base | |
| LensFlexRig (VarOcc' a) a Source # | Access to |
Defined in Mikan.TypeChecking.Free.Base | |
isFlexible :: LensFlexRig o a => o -> Bool Source #
isUnguarded :: LensFlexRig o a => o -> Bool Source #
isWeaklyRigid :: LensFlexRig o a => o -> Bool Source #
isStronglyRigid :: LensFlexRig o a => o -> Bool Source #
addFlexRig :: Semigroup a => FlexRig' a -> FlexRig' a -> FlexRig' a Source #
FlexRig aggregation (additive operation of the semiring).
For combining occurrences of the same variable in subterms.
This is a refinement of the max operation for FlexRig
which would work if Flexible did not have the MetaSet as an argument.
Now, to aggregate two Flexible occurrences, we union the involved MetaSets.
zeroFlexRig :: Monoid a => FlexRig' a Source #
Unit for addFlexRig.
omegaFlexRig :: FlexRig' a Source #
Absorptive for addFlexRig.
composeFlexRig :: Semigroup a => FlexRig' a -> FlexRig' a -> FlexRig' a Source #
FlexRig composition (multiplicative operation of the semiring).
For accumulating the context of a variable.
Flexible is dominant. Once we are under a meta, we are flexible
regardless what else comes. We taint all variable occurrences
under a meta by this meta.
WeaklyRigid is next in strength. Destroys strong rigidity.
StronglyRigid is still dominant over Unguarded.
Unguarded is the unit. It is the top (identity) context.
oneFlexRig :: FlexRig' a Source #
Unit for composeFlexRig.
flexRigToBlocker :: FlexRig -> Blocker Source #
Extract a blocker from an occurrence
Variable occurrence (semigroup)
Occurrence of free variables is classified by a FlexRig.
Constructors
| VarOcc | |
Fields
| |
Instances
| Pretty a => Pretty (VarOcc' a) Source # | |
| PrettyTCM a => PrettyTCM (VarOcc' a) Source # | |
Defined in Mikan.TypeChecking.Pretty | |
| Monoid a => Monoid (VarOcc' a) Source # | The neutral element for variable occurrence aggregation is least serious
occurrence: flexible.
This is also the absorptive element for |
| Semigroup a => Semigroup (VarOcc' a) Source # | The default way of aggregating free variable info from subterms is by adding
the variable occurrences. For instance, if we have a pair From counting
|
| Show a => Show (VarOcc' a) Source # | |
| Eq a => Eq (VarOcc' a) Source # | Equality up to origin. |
| LensFlexRig (VarOcc' a) a Source # | Access to |
Defined in Mikan.TypeChecking.Free.Base | |
topVarOcc :: VarOcc' a Source #
The absorptive element of variable occurrence under aggregation: strongly rigid.
composeVarOcc :: Semigroup a => VarOcc' a -> VarOcc' a -> VarOcc' a Source #
First argument is the outer occurrence (context) and second is the inner. This multiplicative operation is to modify an occurrence under a context.
Storing variable occurrences (semimodule).
type TheVarMap' a = IntMap (VarOcc' a) Source #
Representation of a variable set as map from de Bruijn indices
to VarOcc.
Constructors
| VarMap | |
Fields
| |
Instances
| Singleton Variable (VarMap' a) Source # | A "set"-style |
| PrettyTCM a => PrettyTCM (VarMap' a) Source # | |
Defined in Mikan.TypeChecking.Pretty | |
| Semigroup a => Monoid (VarMap' a) Source # | |
| Semigroup a => Semigroup (VarMap' a) Source # | Proper monoid instance for |
| Show a => Show (VarMap' a) Source # | |
| Eq a => Eq (VarMap' a) Source # | |
type TheVarMap = TheVarMap' MetaSet Source #
mapVarMap :: (TheVarMap' a -> TheVarMap' b) -> VarMap' a -> VarMap' b Source #
Plain variable occurrence counting.
Environment for collecting free variables.
data IgnoreSorts Source #
Where should we skip sorts in free variable analysis?
Constructors
| IgnoreNot | Do not skip. |
| IgnoreInAnnotations | Skip when annotation to a type. |
| IgnoreAll | Skip unconditionally. |
Instances
| Show IgnoreSorts Source # | |
Defined in Mikan.TypeChecking.Free.Base Methods showsPrec :: Int -> IgnoreSorts -> ShowS # show :: IgnoreSorts -> String # showList :: [IgnoreSorts] -> ShowS # | |
| Eq IgnoreSorts Source # | |
Defined in Mikan.TypeChecking.Free.Base | |