diff options
Diffstat (limited to 'src/Obs/NormalForm.idr')
| -rw-r--r-- | src/Obs/NormalForm.idr | 49 |
1 files changed, 49 insertions, 0 deletions
diff --git a/src/Obs/NormalForm.idr b/src/Obs/NormalForm.idr index 4b4fded..2caf733 100644 --- a/src/Obs/NormalForm.idr +++ b/src/Obs/NormalForm.idr @@ -32,6 +32,13 @@ data Neutral : Nat -> Type where Fst : Neutral n -> Neutral n Snd : Neutral n -> Neutral n Absurd : Neutral n + Equal : Neutral n -> NormalForm n -> NormalForm n -> Neutral n + EqualL : Nat -> Neutral n -> NormalForm n -> Neutral n + EqualR : Nat -> Constructor n -> Neutral n -> Neutral n + EqualU : Nat -> Constructor n -> Constructor n -> Neutral n + CastL : Neutral n -> NormalForm n -> NormalForm n -> Neutral n + CastR : Constructor n -> Neutral n -> NormalForm n -> Neutral n + CastU : Constructor n -> Constructor n -> NormalForm n -> Neutral n public export data NormalForm : Nat -> Type where @@ -73,6 +80,13 @@ eqNtrl (App t u) (App t' u') = eqNtrl t t' && eqWhnf u u' eqNtrl (Fst t) (Fst t') = eqNtrl t t' eqNtrl (Snd t) (Snd t') = eqNtrl t t' eqNtrl Absurd Absurd = True +eqNtrl (Equal a t u) (Equal a' t' u') = eqNtrl a a' && eqWhnf t t' && eqWhnf u u' +eqNtrl (EqualL i t u) (EqualL j t' u') = i == j && eqNtrl t t' && eqWhnf u u' +eqNtrl (EqualR i t u) (EqualR j t' u') = i == j && eqCnstr t t' && eqNtrl u u' +eqNtrl (EqualU i t u) (EqualU j t' u') = i == j && eqCnstr t t' && eqCnstr u u' +eqNtrl (CastL a b t) (CastL a' b' t') = eqNtrl a a' && eqWhnf b b' && eqWhnf t t' +eqNtrl (CastR a b t) (CastR a' b' t') = eqCnstr a a' && eqNtrl b b' && eqWhnf t t' +eqNtrl (CastU a b t) (CastU a' b' t') = eqCnstr a a' && eqCnstr b b' && eqWhnf t t' eqNtrl _ _ = False eqWhnf (Ntrl t) (Ntrl u) = eqNtrl t u @@ -146,6 +160,34 @@ prettyPrecNtrl d (Snd t) = group $ fillSep [pretty "snd", prettyPrecNtrl App t] prettyPrecNtrl d Absurd = pretty "absurd" +prettyPrecNtrl d (Equal _ t u) = + parenthesise (d >= Equal) $ + group $ + prettyPrecWhnf Equal t <++> pretty "~" <+> softline <+> prettyPrecWhnf Equal u +prettyPrecNtrl d (EqualL _ t u) = + parenthesise (d >= Equal) $ + group $ + prettyPrecNtrl Equal t <++> pretty "~" <+> softline <+> prettyPrecWhnf Equal u +prettyPrecNtrl d (EqualR _ t u) = + parenthesise (d >= Equal) $ + group $ + prettyPrecCnstr Equal t <++> pretty "~" <+> softline <+> prettyPrecNtrl Equal u +prettyPrecNtrl d (EqualU _ t u) = + parenthesise (d >= Equal) $ + group $ + prettyPrecCnstr Equal t <++> pretty "~" <+> softline <+> prettyPrecCnstr Equal u +prettyPrecNtrl d (CastL a b t) = + parenthesise (d >= App) $ + group $ + fillSep [pretty "cast", prettyPrecNtrl App a, prettyPrecWhnf App b, prettyPrecWhnf App t] +prettyPrecNtrl d (CastR a b t) = + parenthesise (d >= App) $ + group $ + fillSep [pretty "cast", prettyPrecCnstr App a, prettyPrecNtrl App b, prettyPrecWhnf App t] +prettyPrecNtrl d (CastU a b t) = + parenthesise (d >= App) $ + group $ + fillSep [pretty "cast", prettyPrecCnstr App a, prettyPrecCnstr App b, prettyPrecWhnf App t] prettyPrecWhnf d (Ntrl t) = prettyPrecNtrl d t prettyPrecWhnf d (Cnstr t) = prettyPrecCnstr d t @@ -196,6 +238,13 @@ renameNtrl (App t u) f = App (renameNtrl t f) (renameWhnf u f) renameNtrl (Fst t) f = Fst (renameNtrl t f) renameNtrl (Snd t) f = Snd (renameNtrl t f) renameNtrl Absurd f = Absurd +renameNtrl (Equal a t u) f = Equal (renameNtrl a f) (renameWhnf t f) (renameWhnf u f) +renameNtrl (EqualL i t u) f = EqualL i (renameNtrl t f) (renameWhnf u f) +renameNtrl (EqualR i t u) f = EqualR i (renameCnstr t f) (renameNtrl u f) +renameNtrl (EqualU i t u) f = EqualU i (renameCnstr t f) (renameCnstr u f) +renameNtrl (CastL a b t) f = CastL (renameNtrl a f) (renameWhnf b f) (renameWhnf t f) +renameNtrl (CastR a b t) f = CastR (renameCnstr a f) (renameNtrl b f) (renameWhnf t f) +renameNtrl (CastU a b t) f = CastU (renameCnstr a f) (renameCnstr b f) (renameWhnf t f) renameWhnf (Ntrl t) f = Ntrl $ renameNtrl t f renameWhnf (Cnstr t) f = Cnstr $ renameCnstr t f |