diff options
| -rw-r--r-- | obs.ipkg | 1 | ||||
| -rw-r--r-- | src/Core/Generic.idr | 178 | ||||
| -rw-r--r-- | src/Core/Term/NormalForm.idr | 23 |
3 files changed, 202 insertions, 0 deletions
@@ -10,6 +10,7 @@ modules = Core.Declarative , Core.Environment , Core.Environment.Extension + , Core.Generic , Core.Reduction , Core.Term , Core.Term.NormalForm diff --git a/src/Core/Generic.idr b/src/Core/Generic.idr new file mode 100644 index 0000000..c2bd1f4 --- /dev/null +++ b/src/Core/Generic.idr @@ -0,0 +1,178 @@ +module Core.Generic + +import Core.Declarative +import Core.Environment +import Core.Reduction +import Core.Term +import Core.Term.NormalForm +import Core.Term.Substitution +import Core.Term.Thinned +import Core.Thinning + +%prefix_record_projections off + +-- Definition ------------------------------------------------------------------ + +public export +record Equality where + constructor MkEquality + TypeEq : forall n. Env n -> Term n -> Term n -> Type + TermEq : forall n. Env n -> Term n -> Term n -> Term n -> Type + NtrlEq : forall n. Env n -> NeutralTerm n -> NeutralTerm n -> Term n -> Type + +public export +interface IsEq (0 eq : Equality) where + -- Subsumption + ntrlEqImpliesTermEq : + {0 n, m : NeutralTerm k} -> + eq.NtrlEq env n m a -> + eq.TermEq env n.fst m.fst a + termEqImpliesTypeEq : eq.TermEq {n} env a b Set -> eq.TypeEq env a b + termEqImpliesConv : eq.TermEq {n} env t u a -> TermConv env t u a + typeEqImpliesConv : eq.TypeEq {n} env a b -> TypeConv env a b + + -- Partial Equivalence + ntrlSym : eq.NtrlEq {n = k} env n m a -> eq.NtrlEq env m n a + ntrlTrans : eq.NtrlEq {n = k} env n1 n2 a -> eq.NtrlEq env n2 n3 a -> eq.NtrlEq env n1 n3 a + termSym : eq.TermEq {n} env t u a -> eq.TermEq env u t a + termTrans : eq.TermEq {n} env t u a -> eq.TermEq env u v a -> eq.TermEq env t v a + typeSym : eq.TypeEq {n} env a b -> eq.TypeEq env b a + typeTrans : eq.TypeEq {n} env a b -> eq.TypeEq env b c -> eq.TypeEq env a c + + -- Conversion + ntrlConv : eq.NtrlEq {n = k} env n m a -> TypeConv env a b -> eq.NtrlEq env n m b + termConv : eq.TermEq {n} env t u a -> TypeConv env a b -> eq.TermEq env t u b + + -- Weakening + wknNtrl : + eq.NtrlEq {n = j} env1 n m a -> + ExtendsWf thin env2 env1 -> + eq.NtrlEq {n = k} env2 (wkn n thin) (wkn m thin) (wkn a thin) + wknTerm : + eq.TermEq {n = m} env1 t u a -> + ExtendsWf thin env2 env1 -> + eq.TermEq {n} env2 (wkn t thin) (wkn u thin) (wkn a thin) + wknType : + eq.TypeEq {n = m} env1 a b -> + ExtendsWf thin env2 env1 -> + eq.TypeEq {n} env2 (wkn a thin) (wkn b thin) + + -- Weak Head Expansion + expandTerm : + TermReduce env t t' a -> + TermReduce env u u' a -> + Whnf t' -> + Whnf u' -> + eq.TermEq {n} env t' u' a -> + eq.TermEq env t u a + expandType : + TypeReduce env a a' -> + TypeReduce env b b' -> + Whnf a' -> + Whnf b' -> + eq.TypeEq {n} env a' b' -> + eq.TypeEq env a b + + -- Neutral Congruence + ntrlVar : + TermWf env (Var i) a -> + --- + eq.NtrlEq {n} env (Element (Var i) Var) (Element (Var i) Var) a + ntrlApp : + {0 n, m : NeutralTerm k} -> + eq.NtrlEq env n m (Pi a b) -> + eq.TermEq env t u a -> + --- + eq.NtrlEq env + (Element (App n.fst t) (App n.snd)) + (Element (App m.fst u) (App m.snd)) + (subst1 b t) + + -- Term Congurence + termPi : + TypeWf env a -> + eq.TermEq env a c Set -> + eq.TermEq (env :< pure a) b d Set -> + --- + eq.TermEq {n} env (Pi a b) (Pi c d) Set + termPiEta : + TypeWf env a -> + TermWf env t (Pi a b) -> + TermWf env u (Pi a b) -> + eq.TermEq (env :< pure a) + (App (wkn t $ drop $ id _) (Var FZ)) + (App (wkn u $ drop $ id _) (Var FZ)) + b -> + --- + eq.TermEq {n} env t u (Pi a b) + + -- Type Congruence + typeSet : + EnvWf env -> + --- + eq.TypeEq {n} env Set Set + typePi : + TypeWf env a -> + eq.TypeEq env a c -> + eq.TypeEq (env :< pure a) b d -> + --- + eq.TypeEq {n} env (Pi a b) (Pi c d) + +-- Instance 1 ------------------------------------------------------------------ + +public export +Judgemental : Equality +Judgemental = MkEquality TypeConv TermConv (\env, n, m, a => TermConv env n.fst m.fst a) + +judgeWknNtrl : + (Judgemental .NtrlEq) {n = j} env1 n m a -> + ExtendsWf thin env2 env1 -> + (Judgemental .NtrlEq) {n = k} env2 (wkn n thin) (wkn m thin) (wkn a thin) +judgeWknNtrl {n = Element t n, m = Element u m} = weakenTermConv + +export +IsEq Judgemental where + -- Subsumption + ntrlEqImpliesTermEq = id + termEqImpliesTypeEq = LiftConv + termEqImpliesConv = id + typeEqImpliesConv = id + + -- Partial Equivalence + ntrlSym = SymTm + ntrlTrans = TransTm + termSym = SymTm + termTrans = TransTm + typeSym = SymTy + typeTrans = TransTy + + -- Conversion + ntrlConv = ConvConv + termConv = ConvConv + + -- Weakening + wknNtrl = judgeWknNtrl + wknTerm = weakenTermConv + wknType = weakenTypeConv + + -- Weak Head Expansion + expandTerm = \steps1, steps2, n, m, eq => + TransTm (termRedImpliesConv steps1) $ + TransTm eq $ + SymTm (termRedImpliesConv steps2) + expandType = \steps1, steps2, n, m, eq => + TransTy (typeRedImpliesConv steps1) $ + TransTy eq $ + SymTy (typeRedImpliesConv steps2) + + -- Neutral Congruence + ntrlVar = ReflTm + ntrlApp = AppConv + + -- Term Congurence + termPi = PiTmConv + termPiEta = PiEta + + -- Type Congruence + typeSet = ReflTy . SetTyWf + typePi = PiConv diff --git a/src/Core/Term/NormalForm.idr b/src/Core/Term/NormalForm.idr index 9984bee..2cd16a1 100644 --- a/src/Core/Term/NormalForm.idr +++ b/src/Core/Term/NormalForm.idr @@ -1,6 +1,9 @@ module Core.Term.NormalForm import Core.Term +import Core.Thinning + +import public Data.DPair -- Definition ------------------------------------------------------------------ @@ -20,3 +23,23 @@ data Whnf : Term n -> Type where %name Neutral n, m %name Whnf n, m + +public export +NeutralTerm : Nat -> Type +NeutralTerm n = Subset (Term n) Neutral + +-- Inversion ------------------------------------------------------------------- + +invertNtrlApp : Neutral (App t u) -> Neutral t +invertNtrlApp (App n) = n + +-- Weakening ------------------------------------------------------------------- + +export +wknPresNtrl : Neutral t -> (thin : m `Thins` n) -> Neutral (wkn t thin) +wknPresNtrl Var thin = Var +wknPresNtrl (App n) thin = App (wknPresNtrl n thin) + +public export +wkn : NeutralTerm m -> m `Thins` n -> NeutralTerm n +wkn (Element t n) thin = Element (wkn t thin) (wknPresNtrl n thin) |