diff options
Diffstat (limited to 'src/Obs/NormalForm.idr')
| -rw-r--r-- | src/Obs/NormalForm.idr | 74 |
1 files changed, 42 insertions, 32 deletions
diff --git a/src/Obs/NormalForm.idr b/src/Obs/NormalForm.idr index 08354b4..8ee3b19 100644 --- a/src/Obs/NormalForm.idr +++ b/src/Obs/NormalForm.idr @@ -18,12 +18,15 @@ data NormalForm : Nat -> Type public export data Constructor : Nat -> Type where Sort : Sort -> Constructor n + Pi : Sort -> Sort -> NormalForm n -> NormalForm (S n) -> Constructor n + Lambda : NormalForm (S n) -> Constructor n Top : Constructor n Bottom : Constructor n public export data Neutral : Nat -> Type where Var : Fin n -> Neutral n + App : Neutral n -> NormalForm n -> Neutral n Absurd : Neutral n public export @@ -35,7 +38,7 @@ data NormalForm : Nat -> Type where public export record Definition (n : Nat) where constructor MkDefinition - name : Maybe String + name : String sort : Sort ty : NormalForm n tm : NormalForm n @@ -53,12 +56,15 @@ eqNtrl : Neutral n -> Neutral n -> Bool eqWhnf : NormalForm n -> NormalForm n -> Bool eqCnstr (Sort s) (Sort s') = s == s' -eqCnstr Top Top = True -eqCnstr Bottom Bottom = True +eqCnstr (Pi s s' a b) (Pi l l' a' b') = s == l && s' == l' && eqWhnf a a' && eqWhnf b b' +eqCnstr (Lambda t) (Lambda u) = eqWhnf t u +eqCnstr Top Top = True +eqCnstr Bottom Bottom = True eqCnstr _ _ = False eqNtrl (Var i) (Var j) = i == j -eqNtrl Absurd Absurd = True +eqNtrl (App t u) (App t' u') = eqNtrl t t' && eqWhnf u u' +eqNtrl Absurd Absurd = True eqNtrl _ _ = False eqWhnf (Ntrl t) (Ntrl u) = eqNtrl t u @@ -78,6 +84,14 @@ export Eq (NormalForm n) where t == u = eqWhnf t u +export +Cast Sort (Constructor n) where + cast = Sort + +export +Cast Sort (NormalForm n) where + cast = Cnstr . cast + -- Pretty Print ---------------------------------------------------------------- prettyPrecCnstr : Prec -> Constructor n -> Doc ann @@ -85,10 +99,24 @@ prettyPrecNtrl : Prec -> Neutral n -> Doc ann prettyPrecWhnf : Prec -> NormalForm n -> Doc ann prettyPrecCnstr d (Sort s) = prettyPrec d s +prettyPrecCnstr d (Pi _ _ a b) = + parenthesise (d > Open) $ + group $ + parens (prettyPrecWhnf Open a) <++> + pretty "->" <+> softline <+> + prettyPrecWhnf Open b +prettyPrecCnstr d (Lambda t) = + parenthesise (d > Open) $ + group $ + backslash <+> softline <+> prettyPrecWhnf Open t prettyPrecCnstr d Top = pretty "()" prettyPrecCnstr d Bottom = pretty "Void" prettyPrecNtrl d (Var i) = pretty "$\{show i}" +prettyPrecNtrl d (App t u) = + parenthesise (d >= App) $ + group $ + fillSep [prettyPrecNtrl Open t, prettyPrecWhnf App u] prettyPrecNtrl d Absurd = pretty "absurd" prettyPrecWhnf d (Ntrl t) = prettyPrecNtrl d t @@ -128,11 +156,14 @@ renameNtrl : Neutral n -> (Fin n -> Fin m) -> Neutral m renameWhnf : NormalForm n -> (Fin n -> Fin m) -> NormalForm m renameCnstr (Sort s) f = Sort s -renameCnstr Top f = Top -renameCnstr Bottom f = Bottom +renameCnstr (Pi s s' a b) f = Pi s s' (renameWhnf a f) (renameWhnf b $ lift 1 f) +renameCnstr (Lambda t) f = Lambda (renameWhnf t $ lift 1 f) +renameCnstr Top f = Top +renameCnstr Bottom f = Bottom renameNtrl (Var i) f = Var (f i) -renameNtrl Absurd f = Absurd +renameNtrl (App t u) f = App (renameNtrl t f) (renameWhnf u f) +renameNtrl Absurd f = Absurd renameWhnf (Ntrl t) f = Ntrl $ renameNtrl t f renameWhnf (Cnstr t) f = Cnstr $ renameCnstr t f @@ -150,31 +181,10 @@ export Rename NormalForm where rename = renameWhnf --- Substitution - -substCnstr : Constructor n -> (Fin n -> NormalForm m) -> Constructor m -substNtrl : Neutral n -> (Fin n -> NormalForm m) -> NormalForm m -substWhnf : NormalForm n -> (Fin n -> NormalForm m) -> NormalForm m - -substCnstr (Sort s) f = Sort s -substCnstr Top f = Top -substCnstr Bottom f = Bottom - -substNtrl (Var i) f = f i -substNtrl Absurd f = Ntrl Absurd - -substWhnf (Ntrl t) f = substNtrl t f -substWhnf (Cnstr t) f = Cnstr $ substCnstr t f -substWhnf Irrel f = Irrel - -export -Subst Constructor NormalForm Constructor where - subst = substCnstr - export -Subst Neutral NormalForm NormalForm where - subst = substNtrl +PointedRename Neutral where + point = Var export -Subst NormalForm NormalForm NormalForm where - subst = substWhnf +PointedRename NormalForm where + point = Ntrl . point |