diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-08 15:45:24 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-08 15:45:24 +0100 |
| commit | 6e8ab4c1135f39d441cdcf54c5a1bc12b7e565be (patch) | |
| tree | 66e2388591def400ef2a75d5b81f07d0e4fc3401 | |
| parent | 1995d5aba2d63e1854d138fda6747a8865a43bcb (diff) | |
| -rw-r--r-- | src/Core/Declarative.idr | 1 | ||||
| -rw-r--r-- | src/Core/Generic.idr | 45 | ||||
| -rw-r--r-- | src/Core/Reduction.idr | 2 |
3 files changed, 48 insertions, 0 deletions
diff --git a/src/Core/Declarative.idr b/src/Core/Declarative.idr index 8704e07..e5aa95a 100644 --- a/src/Core/Declarative.idr +++ b/src/Core/Declarative.idr @@ -287,6 +287,7 @@ wknPresTermWf : EnvWf env2 -> IsExtension thin env2 env1 -> TermWf env2 (wkn t thin) (wkn a thin) +export wknPresTermConv : {0 env1 : Env sx} -> TermConv env1 t u a -> diff --git a/src/Core/Generic.idr b/src/Core/Generic.idr index 37b6b36..bd11fad 100644 --- a/src/Core/Generic.idr +++ b/src/Core/Generic.idr @@ -114,3 +114,48 @@ interface IsGenericEquality (eq : GenericEquality) where eq.TermEq env a b f -> --- eq.NtrlEq {sx} env (App t a) (App u b) (subst g (sub1 a)) + +-- Judgemental Equality -------------------------------------------------------- + +Judgemental : GenericEquality +Judgemental = MkEquality TypeConv TermConv TermConv + +IsGenericEquality Judgemental where + ntrlImpliesTermEq = id + termImpliesTypeEq = LiftConv + eqImpliesTermConv = id + eqImpliesTypeConv = id + + ntrlSym = SymTerm + ntrlTrans = TransTerm + termSym = SymTerm + termTrans = TransTerm + typeSym = SymType + typeTrans = TransType + + ntrlConv = ConvTermConv + termConv = ConvTermConv + + wknPresNtrlEq = wknPresTermConv + wknPresTermEq = wknPresTermConv + wknPresTypeEq = wknPresTypeConv + + typeExpansion steps1 steps2 n m conv = + TransType (typeRedImpliesTypeConv steps1) $ + TransType conv $ + SymType (typeRedImpliesTypeConv steps2) + termExpansion steps1 steps2 steps3 n m k conv = + ConvTermConv + (TransTerm (termRedImpliesTermConv steps2) $ + TransTerm conv $ + SymTerm (termRedImpliesTermConv steps3)) + (SymType $ typeRedImpliesTypeConv steps1) + + typeSet = ReflType . SetType + typePi = PiTypeConv + + termPi = PiTermConv + termPiEta = PiEta + + ntrlVar = ReflTerm + ntrlApp = AppConv diff --git a/src/Core/Reduction.idr b/src/Core/Reduction.idr index eb59446..241669f 100644 --- a/src/Core/Reduction.idr +++ b/src/Core/Reduction.idr @@ -58,6 +58,7 @@ termStepImpliesTermConv (StepConv step conv) = ConvTermConv (termStepImpliesTerm typeStepImpliesTypeConv : TypeStep env a b -> TypeConv env a b typeStepImpliesTypeConv step = LiftConv (termStepImpliesTermConv step) +export typeRedImpliesTypeConv : TypeRed env a b -> TypeConv env a b typeRedImpliesTypeConv (Stay wf) = ReflType wf typeRedImpliesTypeConv (step :: steps) = @@ -65,6 +66,7 @@ typeRedImpliesTypeConv (step :: steps) = (typeStepImpliesTypeConv step) (typeRedImpliesTypeConv steps) +export termRedImpliesTermConv : TermRed env t u a -> TermConv env t u a termRedImpliesTermConv (Stay wf) = ReflTerm wf termRedImpliesTermConv (step :: steps) = |