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

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.TypeChecking.Rewriting.NonLinMatch

Description

Non-linear matching of the lhs of a rewrite rule against a neutral term.

Given a lhs

Δ ⊢ lhs : B

and a candidate term

Γ ⊢ t : A

we seek a substitution Γ ⊢ σ : Δ such that

Γ ⊢ B[σ] = A and Γ ⊢ lhs[σ] = t : A

Synopsis

- newtype NLM a = NLM {
  - unNLM :: ExceptT Blocked_ (StateT NLMState ReduceM) a
  }
- data NLMState = NLMState {
  - _nlmSub :: Sub
  - _nlmEqs :: PostponedEquations
  }
- nlmSub :: Lens' Sub NLMState
- nlmEqs :: Lens' PostponedEquations NLMState
- runNLM :: MonadReduce m => NLM () -> m (Either Blocked_ NLMState)
- matchingBlocked :: Blocked_ -> NLM ()
- tellSub :: Relevance -> Int -> Type -> Term -> NLM ()
- tellEq :: Telescope -> Telescope -> Type -> Term -> Term -> NLM ()
- type Sub = IntMap (Relevance, Term)
- data PostponedEquation = PostponedEquation {
  - eqFreeVars :: Telescope
  - eqType :: Type
  - eqLhs :: Term
  - eqRhs :: Term
  }
- type PostponedEquations = [PostponedEquation]
- class Match t a b where
  - match :: Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
- reallyFree :: (MonadReduce m, Reduce a, ForceNotFree a) => IntSet -> a -> m (Either Blocked_ (Maybe a))
- makeSubstitution :: Telescope -> Sub -> Substitution
- checkPostponedEquations :: PureTCM m => Substitution -> PostponedEquations -> m (Maybe Blocked_)
- nonLinMatch :: (PureTCM m, Match t a b) => Telescope -> t -> a -> b -> m (Either Blocked_ Substitution)
- equal :: PureTCM m => Type -> Term -> Term -> m (Maybe Blocked_)
- getTypedHead :: PureTCM m => Term -> m (Maybe (QName, Type))

# Documentation

newtype NLM a Source #

Monad for non-linear matching.

Constructors

NLM |

Fields

- unNLM :: ExceptT Blocked_ (StateT NLMState ReduceM) a

#### Instances

Instances details

HasOptions NLM Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods pragmaOptions :: NLM PragmaOptions Source # commandLineOptions :: NLM CommandLineOptions Source #
MonadBlock NLM Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods patternViolation :: Blocker -> NLM a Source # catchPatternErr :: (Blocker -> NLM a) -> NLM a -> NLM a Source #
MonadReduce NLM Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods liftReduce :: ReduceM a -> NLM a Source #
MonadTCEnv NLM Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods askTC :: NLM TCEnv Source # localTC :: (TCEnv -> TCEnv) -> NLM a -> NLM a Source #
ReadTCState NLM Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods getTCState :: NLM TCState Source # locallyTCState :: Lens' a TCState -> (a -> a) -> NLM b -> NLM b Source # withTCState :: (TCState -> TCState) -> NLM a -> NLM a Source #
HasBuiltins NLM Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods getBuiltinThing :: String -> NLM (Maybe (Builtin PrimFun)) Source #
MonadAddContext NLM Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods addCtx :: Name -> Dom Type -> NLM a -> NLM a Source # addLetBinding' :: Name -> Term -> Dom Type -> NLM a -> NLM a Source # updateContext :: Substitution -> (Context -> Context) -> NLM a -> NLM a Source # withFreshName :: Range -> ArgName -> (Name -> NLM a) -> NLM a Source #
MonadDebug NLM Source # |

Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> NLM String Source #

traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> NLM a -> NLM a Source #

verboseBracket :: VerboseKey -> VerboseLevel -> String -> NLM a -> NLM a Source #

getVerbosity :: NLM Verbosity Source #

isDebugPrinting :: NLM Bool Source #

nowDebugPrinting :: NLM a -> NLM a Source #

PureTCM NLM Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch
HasConstInfo NLM Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods getConstInfo :: QName -> NLM Definition Source # getConstInfo' :: QName -> NLM (Either SigError Definition) Source # getRewriteRulesFor :: QName -> NLM RewriteRules Source #
MonadFail NLM Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods fail :: String -> NLM a Source #
Alternative NLM Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods empty :: NLM a Source # (<|>) :: NLM a -> NLM a -> NLM a Source # some :: NLM a -> NLM [a] Source # many :: NLM a -> NLM [a] Source #
Applicative NLM Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods pure :: a -> NLM a Source # (<*>) :: NLM (a -> b) -> NLM a -> NLM b Source # liftA2 :: (a -> b -> c) -> NLM a -> NLM b -> NLM c Source # (*>) :: NLM a -> NLM b -> NLM b Source # (<*) :: NLM a -> NLM b -> NLM a Source #
Functor NLM Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods fmap :: (a -> b) -> NLM a -> NLM b Source # (<$) :: a -> NLM b -> NLM a Source #
Monad NLM Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods (>>=) :: NLM a -> (a -> NLM b) -> NLM b Source # (>>) :: NLM a -> NLM b -> NLM b Source # return :: a -> NLM a Source #
MonadPlus NLM Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods mzero :: NLM a Source # mplus :: NLM a -> NLM a -> NLM a Source #
MonadError Blocked_ NLM Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods throwError :: Blocked_ -> NLM a Source # catchError :: NLM a -> (Blocked_ -> NLM a) -> NLM a Source #
MonadState NLMState NLM Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods get :: NLM NLMState Source # put :: NLMState -> NLM () Source # state :: (NLMState -> (a, NLMState)) -> NLM a Source #

data NLMState Source #

Constructors

NLMState |

Fields

- _nlmSub :: Sub
- _nlmEqs :: PostponedEquations

#### Instances

Instances details

Null NLMState Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods empty :: NLMState Source # null :: NLMState -> Bool Source #
MonadState NLMState NLM Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods get :: NLM NLMState Source # put :: NLMState -> NLM () Source # state :: (NLMState -> (a, NLMState)) -> NLM a Source #

nlmSub :: Lens' Sub NLMState Source #

nlmEqs :: Lens' PostponedEquations NLMState Source #

runNLM :: MonadReduce m => NLM () -> m (Either Blocked_ NLMState) Source #

matchingBlocked :: Blocked_ -> NLM () Source #

tellSub :: Relevance -> Int -> Type -> Term -> NLM () Source #

Add substitution `i |-> v : a` to result of matching.

tellEq :: Telescope -> Telescope -> Type -> Term -> Term -> NLM () Source #

type Sub = IntMap (Relevance, Term) Source #

data PostponedEquation Source #

Matching against a term produces a constraint which we have to verify after applying the substitution computed by matching.

Constructors

PostponedEquation |

Fields

- eqFreeVars :: Telescope

  Telescope of free variables in the equation

- eqType :: Type

  Type of the equation, living in same context as the rhs.

- eqLhs :: Term

  Term from pattern, living in pattern context.

- eqRhs :: Term

  Term from scrutinee, living in context where matching was invoked.

type PostponedEquations = [PostponedEquation] Source #

class Match t a b where Source #

Match a non-linear pattern against a neutral term, returning a substitution.

Methods

match Source #

Arguments

:: Relevance | Are we currently matching in an irrelevant context?
-> Telescope | The telescope of pattern variables
-> Telescope | The telescope of lambda-bound variables
-> t | The type of the pattern
-> a | The pattern to match
-> b | The term to be matched against the pattern
-> NLM () |

#### Instances

Instances details

Match Type NLPat Term Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Telescope -> Type -> NLPat -> Term -> NLM () Source #
Match () NLPSort Sort Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Telescope -> () -> NLPSort -> Sort -> NLM () Source #
Match () NLPType Type Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Telescope -> () -> NLPType -> Type -> NLM () Source #
Match () NLPat Level Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Telescope -> () -> NLPat -> Level -> NLM () Source #
Match t a b => Match t (Dom a) (Dom b) Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Telescope -> t -> Dom a -> Dom b -> NLM () Source #
Match t a b => Match (Dom t) (Arg a) (Arg b) Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Telescope -> Dom t -> Arg a -> Arg b -> NLM () Source #
Match (Type, Elims -> Term) [Elim' NLPat] Elims Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Telescope -> (Type, Elims -> Term) -> [Elim' NLPat] -> Elims -> NLM () Source #

reallyFree :: (MonadReduce m, Reduce a, ForceNotFree a) => IntSet -> a -> m (Either Blocked_ (Maybe a)) Source #

makeSubstitution :: Telescope -> Sub -> Substitution Source #

checkPostponedEquations :: PureTCM m => Substitution -> PostponedEquations -> m (Maybe Blocked_) Source #

nonLinMatch :: (PureTCM m, Match t a b) => Telescope -> t -> a -> b -> m (Either Blocked_ Substitution) Source #

equal :: PureTCM m => Type -> Term -> Term -> m (Maybe Blocked_) Source #

Typed βη-equality, also handles empty record types. Returns `Nothing` if the terms are equal, or `Just b` if the terms are not (where b contains information about possible metas blocking the comparison)

getTypedHead :: PureTCM m => Term -> m (Maybe (QName, Type)) Source #

Utility function for getting the name and type of a head term (i.e. a `Def` or `Con` with no arguments)