Safe Haskell | None |
---|---|

Language | Haskell98 |

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

- class PatternFrom a b where
- type NLM = ExceptT Blocked_ (StateT NLMState ReduceM)
- type NLMState = (Sub, PostponedEquations)
- liftRed :: ReduceM a -> NLM a
- runNLM :: NLM () -> ReduceM (Either Blocked_ NLMState)
- traceSDocNLM :: VerboseKey -> Int -> TCM Doc -> NLM a -> NLM a
- matchingBlocked :: Blocked_ -> NLM ()
- tellSub :: Int -> Term -> NLM ()
- tellEq :: Telescope -> Telescope -> Term -> Term -> NLM ()
- type Sub = IntMap Term
- data PostponedEquation = PostponedEquation {}
- type PostponedEquations = [PostponedEquation]
- class Match a b where
- makeSubstitution :: Telescope -> Sub -> Substitution
- checkPostponedEquations :: Substitution -> PostponedEquations -> ReduceM Bool
- nonLinMatch :: Match a b => Telescope -> a -> b -> ReduceM (Either Blocked_ Substitution)
- equal :: Term -> Term -> ReduceM Bool
- class RaiseNLP a where

# Documentation

class PatternFrom a b where Source #

Turn a term into a non-linear pattern, treating the free variables as pattern variables. The first argument is the number of bound variables (from pattern lambdas).

patternFrom :: Int -> a -> TCM b Source #

PatternFrom Term NLPat Source # | |

PatternFrom a b => PatternFrom [a] [b] Source # | |

PatternFrom a b => PatternFrom (Dom a) (Dom b) Source # | |

PatternFrom a b => PatternFrom (Arg a) (Arg b) Source # | |

PatternFrom a b => PatternFrom (Type' a) (Type' b) Source # | |

PatternFrom a b => PatternFrom (Abs a) (Abs b) Source # | |

PatternFrom a b => PatternFrom (Elim' a) (Elim' b) Source # | |

type NLMState = (Sub, PostponedEquations) Source #

traceSDocNLM :: VerboseKey -> Int -> TCM Doc -> NLM a -> NLM a Source #

matchingBlocked :: Blocked_ -> NLM () Source #

data PostponedEquation Source #

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

type PostponedEquations = [PostponedEquation] Source #

class Match a b where Source #

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

Match NLPat Term Source # | |

Match a b => Match [a] [b] Source # | |

Match a b => Match (Dom a) (Dom b) Source # | |

Match a b => Match (Arg a) (Arg b) Source # | |

Match a b => Match (Type' a) (Type' b) Source # | |

(Match a b, Subst t1 a, Subst t2 b) => Match (Abs a) (Abs b) Source # | |

Match a b => Match (Elim' a) (Elim' b) Source # | |

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

nonLinMatch :: Match a b => Telescope -> a -> b -> ReduceM (Either Blocked_ Substitution) Source #

equal :: Term -> Term -> ReduceM Bool Source #

Untyped βη-equality, does not handle things like empty record types.