diff options
Diffstat (limited to 'src/Inky/Type.idr')
| -rw-r--r-- | src/Inky/Type.idr | 973 |
1 files changed, 643 insertions, 330 deletions
diff --git a/src/Inky/Type.idr b/src/Inky/Type.idr index 26f3c0f..45645bc 100644 --- a/src/Inky/Type.idr +++ b/src/Inky/Type.idr @@ -1,421 +1,734 @@ module Inky.Type -import Data.Bool.Decidable +import public Inky.Data.Context.Var +import public Inky.Data.Row +import public Inky.Data.SnocList.Var + +import Control.Function import Data.DPair -import Data.Maybe.Decidable import Data.These -import Data.These.Decidable -import Inky.Context -import Inky.Thinning + +import Inky.Data.SnocList.Thinning +import Inky.Data.Thinned +import Inky.Decidable +import Inky.Decidable.Maybe + +%hide Prelude.Ops.infixl.(>=>) -- Definition ------------------------------------------------------------------ public export -data Ty : Context () -> () -> Type where - TVar : Var ctx v -> Ty ctx v - TNat : Ty ctx () - TArrow : Ty ctx () -> Ty ctx () -> Ty ctx () - TProd : Row (Ty ctx ()) -> Ty ctx () - TSum : Row (Ty ctx ()) -> Ty ctx () - TFix : (x : String) -> Ty (ctx :< (x :- ())) () -> Ty ctx () +data Ty : SnocList String -> Type where + TVar : Var ctx -> Ty ctx + TArrow : Ty ctx -> Ty ctx -> Ty ctx + TProd : (as : Row (Ty ctx)) -> Ty ctx + TSum : (as : Row (Ty ctx)) -> Ty ctx + TFix : (x : String) -> Ty (ctx :< x) -> Ty ctx %name Ty a, b, c --------------------------------------------------------------------------------- +export +Injective TProd where + injective Refl = Refl + +export +Injective TSum where + injective Refl = Refl + +export +fixInjective : TFix x t = TFix y u -> the (x ** Ty (ctx :< x)) (x ** t) = (y ** u) +fixInjective Refl = Refl + +-- Decisions ------------------------------------------------------------------- + +export +Uninhabited (TVar i = TArrow a b) where + uninhabited Refl impossible + +export +Uninhabited (TVar i = TProd as) where + uninhabited Refl impossible + +export +Uninhabited (TVar i = TSum as) where + uninhabited Refl impossible + +export +Uninhabited (TVar i = TFix x a) where + uninhabited Refl impossible + +export +Uninhabited (TArrow a b = TProd as) where + uninhabited Refl impossible + +export +Uninhabited (TArrow a b = TSum as) where + uninhabited Refl impossible + +export +Uninhabited (TArrow a b = TFix x c) where + uninhabited Refl impossible + +export +Uninhabited (TProd as = TArrow a b) where + uninhabited Refl impossible + +export +Uninhabited (TProd as = TSum bs) where + uninhabited Refl impossible + +export +Uninhabited (TProd as = TFix x a) where + uninhabited Refl impossible + +export +Uninhabited (TSum as = TArrow a b) where + uninhabited Refl impossible + +export +Uninhabited (TSum as = TProd bs) where + uninhabited Refl impossible + +export +Uninhabited (TSum as = TFix x a) where + uninhabited Refl impossible + +export +Uninhabited (TFix x a = TArrow b c) where + uninhabited Refl impossible + +export +Uninhabited (TFix x a = TProd as) where + uninhabited Refl impossible + +export +Uninhabited (TFix x a = TSum as) where + uninhabited Refl impossible + +public export +isArrow : + (a : Ty ctx) -> + Proof (Ty ctx, Ty ctx) (\bc => a = TArrow (fst bc) (snd bc)) + ((b, c : Ty ctx) -> Not (a = TArrow b c)) +isArrow (TVar i) = Nothing `Because` (\_, _ => absurd) +isArrow (TArrow a b) = Just (a, b) `Because` Refl +isArrow (TProd as) = Nothing `Because` (\_, _ => absurd) +isArrow (TSum as) = Nothing `Because` (\_, _ => absurd) +isArrow (TFix x a) = Nothing `Because` (\_, _ => absurd) + +public export +isProd : (a : Ty ctx) -> DecWhen (Row (Ty ctx)) (\as => a = TProd as) +isProd (TVar i) = Nothing `Because` (\_ => absurd) +isProd (TArrow a b) = Nothing `Because` (\_ => absurd) +isProd (TProd as) = Just as `Because` Refl +isProd (TSum as) = Nothing `Because` (\_ => absurd) +isProd (TFix x a) = Nothing `Because` (\_ => absurd) + +public export +isSum : (a : Ty ctx) -> DecWhen (Row (Ty ctx)) (\as => a = TSum as) +isSum (TVar i) = Nothing `Because` (\_ => absurd) +isSum (TArrow a b) = Nothing `Because` (\_ => absurd) +isSum (TProd as) = Nothing `Because` (\_ => absurd) +isSum (TSum as) = Just as `Because` Refl +isSum (TFix x a) = Nothing `Because` (\_ => absurd) + +public export +isFix : + (a : Ty ctx) -> + Proof (x ** Ty (ctx :< x)) (\xb => a = TFix (fst xb) (snd xb)) + ((x : _) -> (b : _) -> Not (a = TFix x b)) +isFix (TVar i) = Nothing `Because` (\_, _ => absurd) +isFix (TArrow a b) = Nothing `Because` (\_, _ => absurd) +isFix (TProd as) = Nothing `Because` (\_, _ => absurd) +isFix (TSum as) = Nothing `Because` (\_, _ => absurd) +isFix (TFix x a) = Just (x ** a) `Because` Refl + -- Thinning -------------------------------------------------------------------- --------------------------------------------------------------------------------- -thin : ctx1 `Thins` ctx2 -> forall v. Ty ctx1 v -> Ty ctx2 v -thinAll : ctx1 `Thins` ctx2 -> forall v. Row (Ty ctx1 v) -> Row (Ty ctx2 v) -thinAllFresh : - (f : ctx1 `Thins` ctx2) -> (x : String) -> - forall v. (row : Row (Ty ctx1 v)) -> - So (x `freshIn` row) -> So (x `freshIn` thinAll f row) +thin : ctx1 `Thins` ctx2 -> Ty ctx1 -> Ty ctx2 +thinAll : ctx1 `Thins` ctx2 -> Context (Ty ctx1) -> Context (Ty ctx2) +thinAllNames : + (f : ctx1 `Thins` ctx2) -> + (ctx : Context (Ty ctx1)) -> + (thinAll f ctx).names = ctx.names thin f (TVar i) = TVar (index f i) -thin f TNat = TNat thin f (TArrow a b) = TArrow (thin f a) (thin f b) -thin f (TProd as) = TProd (thinAll f as) -thin f (TSum as) = TSum (thinAll f as) +thin f (TProd (MkRow as fresh)) = TProd (MkRow (thinAll f as) (rewrite thinAllNames f as in fresh)) +thin f (TSum (MkRow as fresh)) = TSum (MkRow (thinAll f as) (rewrite thinAllNames f as in fresh)) thin f (TFix x a) = TFix x (thin (Keep f) a) thinAll f [<] = [<] -thinAll f ((:<) as (x :- a) {fresh}) = - (:<) (thinAll f as) (x :- thin f a) {fresh = thinAllFresh f x as fresh} +thinAll f (as :< (n :- a)) = thinAll f as :< (n :- thin f a) -thinAllFresh f x [<] = id -thinAllFresh f x (as :< (y :- a)) = andSo . mapSnd (thinAllFresh f x as) . soAnd +thinAllNames f [<] = Refl +thinAllNames f (as :< (n :- a)) = cong (:< n) $ thinAllNames f as -- Renaming Coalgebra -thinCong : f ~~~ g -> forall v. (a : Ty ctx1 v) -> thin f a = thin g a -thinCongAll : f ~~~ g -> forall v. (as : Row (Ty ctx1 v)) -> thinAll f as = thinAll g as +thinCong : f ~~~ g -> (a : Ty ctx1) -> thin f a = thin g a +thinCongAll : f ~~~ g -> (as : Context (Ty ctx1)) -> thinAll f as = thinAll g as thinCong prf (TVar i) = cong TVar (prf.index i) -thinCong prf TNat = Refl thinCong prf (TArrow a b) = cong2 TArrow (thinCong prf a) (thinCong prf b) -thinCong prf (TProd as) = cong TProd (thinCongAll prf as) -thinCong prf (TSum as) = cong TSum (thinCongAll prf as) +thinCong prf (TProd (MkRow as fresh)) = cong TProd (rowCong $ thinCongAll prf as) +thinCong prf (TSum (MkRow as fresh)) = cong TSum (rowCong $ thinCongAll prf as) thinCong prf (TFix x a) = cong (TFix x) (thinCong (KeepKeep prf) a) thinCongAll prf [<] = Refl -thinCongAll prf (as :< (x :- a)) = - snocCong2 (thinCongAll prf as) (cong (x :-) $ thinCong prf a) +thinCongAll prf (as :< (n :- a)) = + cong2 (:<) (thinCongAll prf as) (cong (n :-) $ thinCong prf a) -thinId : (a : Ty ctx v) -> thin Id a = a -thinIdAll : (as : Row (Ty ctx v)) -> thinAll Id as = as +thinId : (a : Ty ctx) -> thin Id a = a +thinIdAll : (as : Context (Ty ctx)) -> thinAll Id as = as thinId (TVar (%% x)) = Refl -thinId TNat = Refl thinId (TArrow a b) = cong2 TArrow (thinId a) (thinId b) -thinId (TProd as) = cong TProd (thinIdAll as) -thinId (TSum as) = cong TSum (thinIdAll as) +thinId (TProd (MkRow as fresh)) = cong TProd (rowCong $ thinIdAll as) +thinId (TSum (MkRow as fresh)) = cong TSum (rowCong $ thinIdAll as) thinId (TFix x a) = cong (TFix x) (trans (thinCong (KeepId IdId) a) (thinId a)) thinIdAll [<] = Refl -thinIdAll (as :< (x :- a)) = - snocCong2 (thinIdAll as) (cong (x :-) $ thinId a) +thinIdAll (as :< (n :- a)) = cong2 (:<) (thinIdAll as) (cong (n :-) $ thinId a) export -Rename () Ty where - var = TVar +Rename String Ty where rename = thin renameCong = thinCong renameId = thinId --- Equality -------------------------------------------------------------------- - -Preeq : - {ctx2 : Context ()} -> {v : ()} -> - Ty ctx1 v -> Ty ctx2 v -> ctx1 `Thins` ctx2 -> Type -PreeqAll : - {ctx2 : Context ()} -> {v : ()} -> - Row (Ty ctx1 v) -> Row (Ty ctx2 v) -> ctx1 `Thins` ctx2 -> Type - -Preeq (TVar i) (TVar j) f = index f i = j -Preeq (TNat) (TNat) f = () -Preeq (TArrow a b) (TArrow c d) f = (Preeq a c f, Preeq b d f) -Preeq (TProd as) (TProd bs) f = PreeqAll as bs f -Preeq (TSum as) (TSum bs) f = PreeqAll as bs f -Preeq (TFix x a) (TFix y b) f = Preeq a b (Keep f) -Preeq _ _ f = Void - -PreeqAll [<] bs f = (bs = [<]) -PreeqAll (as :< (x :- a)) bs f = - ( b ** cs ** - ( Remove x bs b cs - , Preeq a b f - , PreeqAll as cs f - )) - -preeqAllReorder : - (as : Row (Ty ctx1 v)) -> bs <~> cs -> (f : ctx1 `Thins` ctx2) -> - PreeqAll as bs f -> PreeqAll as cs f -preeqAllReorder [<] [] f Refl = Refl -preeqAllReorder [<] (step :: prf) f Refl impossible -preeqAllReorder (as :< (x :- a)) prf f (b ** bs ** (prf', eq1, eq2)) = - (b ** bs ** (bimap id (trans (sym prf)) prf', eq1, eq2)) - -preeq : Ty ctx1 v -> Ty ctx2 v -> ctx1 `Thins` ctx2 -> Bool -preeqAll : Row (Ty ctx1 v) -> Row (Ty ctx2 v) -> ctx1 `Thins` ctx2 -> Bool - -preeq (TVar i) (TVar j) f = index f i == j -preeq TNat TNat f = True -preeq (TArrow a b) (TArrow c d) f = preeq a c f && preeq b d f -preeq (TProd as) (TProd bs) f = preeqAll as bs f -preeq (TSum as) (TSum bs) f = preeqAll as bs f -preeq (TFix x a) (TFix y b) f = preeq a b (Keep f) -preeq _ _ f = False - -preeqAll [<] bs f = null bs -preeqAll (as :< (x :- a)) bs f = - case remove' x bs of - Just (b, bs) => preeq a b f && preeqAll as bs f - Nothing => False - -export -reflectAnd : a `Reflects` b1 -> b `Reflects` b2 -> (a, b) `Reflects` (b1 && b2) -reflectAnd (RTrue x) (RTrue y) = RTrue (x, y) -reflectAnd (RTrue x) (RFalse f) = RFalse (f . snd) -reflectAnd (RFalse f) _ = RFalse (f . fst) - -0 reflectPreeq : - (a : Ty ctx1 v) -> (b : Ty ctx2 v) -> (f : ctx1 `Thins` ctx2) -> - Preeq a b f `Reflects` preeq a b f -0 reflectPreeqAll : - (as : Row (Ty ctx1 v)) -> (bs : Row (Ty ctx2 v)) -> (f : ctx1 `Thins` ctx2) -> - PreeqAll as bs f `Reflects` preeqAll as bs f - -reflectPreeq (TVar i) (TVar j) f = reflectEq (index f i) j -reflectPreeq (TVar i) TNat f = RFalse id -reflectPreeq (TVar i) (TArrow a b) f = RFalse id -reflectPreeq (TVar i) (TProd as) f = RFalse id -reflectPreeq (TVar i) (TSum as) f = RFalse id -reflectPreeq (TVar i) (TFix x a) f = RFalse id -reflectPreeq TNat (TVar i) f = RFalse id -reflectPreeq TNat TNat f = RTrue () -reflectPreeq TNat (TArrow a b) f = RFalse id -reflectPreeq TNat (TProd as) f = RFalse id -reflectPreeq TNat (TSum as) f = RFalse id -reflectPreeq TNat (TFix x a) f = RFalse id -reflectPreeq (TArrow a c) (TVar i) f = RFalse id -reflectPreeq (TArrow a c) TNat f = RFalse id -reflectPreeq (TArrow a c) (TArrow b d) f = reflectAnd (reflectPreeq a b f) (reflectPreeq c d f) -reflectPreeq (TArrow a c) (TProd as) f = RFalse id -reflectPreeq (TArrow a c) (TSum as) f = RFalse id -reflectPreeq (TArrow a c) (TFix x b) f = RFalse id -reflectPreeq (TProd as) (TVar i) f = RFalse id -reflectPreeq (TProd as) TNat f = RFalse id -reflectPreeq (TProd as) (TArrow a b) f = RFalse id -reflectPreeq (TProd as) (TProd bs) f = reflectPreeqAll as bs f -reflectPreeq (TProd as) (TSum bs) f = RFalse id -reflectPreeq (TProd as) (TFix x a) f = RFalse id -reflectPreeq (TSum as) (TVar i) f = RFalse id -reflectPreeq (TSum as) TNat f = RFalse id -reflectPreeq (TSum as) (TArrow a b) f = RFalse id -reflectPreeq (TSum as) (TProd bs) f = RFalse id -reflectPreeq (TSum as) (TSum bs) f = reflectPreeqAll as bs f -reflectPreeq (TSum as) (TFix x a) f = RFalse id -reflectPreeq (TFix x a) (TVar i) f = RFalse id -reflectPreeq (TFix x a) TNat f = RFalse id -reflectPreeq (TFix x a) (TArrow b c) f = RFalse id -reflectPreeq (TFix x a) (TProd as) f = RFalse id -reflectPreeq (TFix x a) (TSum as) f = RFalse id -reflectPreeq (TFix x a) (TFix y b) f = reflectPreeq a b (Keep f) - -reflectPreeqAll [<] [<] f = RTrue Refl -reflectPreeqAll [<] (_ :< _) f = RFalse (\case Refl impossible) -reflectPreeqAll (as :< (x :- a)) bs f with (reflectRemove x bs) | (remove' x bs) - _ | RJust (Evidence fresh prf) | Just (b, cs) with (reflectAnd (reflectPreeq a b f) (reflectPreeqAll as cs f)) | (preeq a b f && preeqAll as cs f) - _ | RTrue prf' | _ = RTrue (b ** cs ** (Evidence fresh prf, prf')) - _ | RFalse nprf | _ = - RFalse (\(b' ** cs' ** (prf1, prf2)) => - let (eq, reorder) = removeUnique x bs (Evidence fresh prf) prf1 in - nprf $ - bimap - (\x => rewrite eq in x) - (preeqAllReorder as (sym reorder) f) - prf2) - _ | RNothing nprf | _ = RFalse (\(b ** cs ** (prf, _)) => nprf (b, cs) prf) +-- Alpha Equivalence ------------------------------------------------------------ -public export -Eq (Ty ctx v) where - a == b = preeq a b Id +namespace Shape + public export + data SameShape : Ty ctx1 -> Ty ctx2 -> Type where + TVar : SameShape (TVar i) (TVar j) + TArrow : SameShape (TArrow a c) (TArrow b d) + TProd : SameShape (TProd as) (TProd bs) + TSum : SameShape (TSum as) (TSum bs) + TFix : SameShape (TFix x a) (TFix y b) export -Eq : {ctx : Context ()} -> {v : ()} -> Ty ctx v -> Ty ctx v -> Type -Eq a b = Preeq a b Id +Uninhabited (SameShape (TVar i) (TArrow b d)) + where uninhabited TVar impossible export -0 reflectEq : (a, b : Ty ctx v) -> (a `Eq` b) `Reflects` (a == b) -reflectEq a b = reflectPreeq a b Id +Uninhabited (SameShape (TVar i) (TProd bs)) + where uninhabited TVar impossible --- Occurs ---------------------------------------------------------------------- +export +Uninhabited (SameShape (TVar i) (TSum bs)) + where uninhabited TVar impossible -OccursIn : Var ctx v -> Ty ctx w -> Type -OccursInAny : Var ctx v -> Row (Ty ctx w) -> Type +export +Uninhabited (SameShape (TVar i) (TFix y b)) + where uninhabited TVar impossible -i `OccursIn` TVar j = i = j -i `OccursIn` TNat = Void -i `OccursIn` TArrow a b = These (i `OccursIn` a) (i `OccursIn` b) -i `OccursIn` TProd as = i `OccursInAny` as -i `OccursIn` TSum as = i `OccursInAny` as -i `OccursIn` TFix x a = ThereVar i `OccursIn` a +export +Uninhabited (SameShape (TArrow a b) (TVar j)) + where uninhabited TVar impossible -i `OccursInAny` [<] = Void -i `OccursInAny` (as :< (x :- a)) = These (i `OccursIn` a) (i `OccursInAny` as) +export +Uninhabited (SameShape (TArrow a c) (TProd bs)) + where uninhabited TVar impossible --- Decidable +export +Uninhabited (SameShape (TArrow a c) (TSum bs)) + where uninhabited TVar impossible -occursIn : (i : Var ctx v) -> (a : Ty ctx w) -> Bool -occursInAny : (i : Var ctx v) -> (as : Row (Ty ctx w)) -> Bool +export +Uninhabited (SameShape (TArrow a c) (TFix y b)) + where uninhabited TVar impossible -i `occursIn` (TVar j) = i `eq` j -i `occursIn` TNat = False -i `occursIn` (TArrow a b) = (i `occursIn` a) || (i `occursIn` b) -i `occursIn` (TProd as) = i `occursInAny` as -i `occursIn` (TSum as) = i `occursInAny` as -i `occursIn` (TFix x a) = ThereVar i `occursIn` a +export +Uninhabited (SameShape (TProd as) (TVar j)) + where uninhabited TVar impossible -i `occursInAny` [<] = False -i `occursInAny` (as :< (x :- a)) = (i `occursIn` a) || (i `occursInAny` as) +export +Uninhabited (SameShape (TProd as) (TArrow b d)) + where uninhabited TVar impossible -reflectOccursIn : - (i : Var ctx v) -> (a : Ty ctx w) -> - (i `OccursIn` a) `Reflects` (i `occursIn` a) -reflectOccursInAny : - (i : Var ctx v) -> (as : Row (Ty ctx w)) -> - (i `OccursInAny` as) `Reflects` (i `occursInAny` as) +export +Uninhabited (SameShape (TProd as) (TSum bs)) + where uninhabited TVar impossible -reflectOccursIn i (TVar j) = reflectEq i j -reflectOccursIn i TNat = RFalse id -reflectOccursIn i (TArrow a b) = reflectThese (reflectOccursIn i a) (reflectOccursIn i b) -reflectOccursIn i (TProd as) = reflectOccursInAny i as -reflectOccursIn i (TSum as) = reflectOccursInAny i as -reflectOccursIn i (TFix x a) = reflectOccursIn (ThereVar i) a +export +Uninhabited (SameShape (TProd as) (TFix y b)) + where uninhabited TVar impossible + +export +Uninhabited (SameShape (TSum as) (TVar j)) + where uninhabited TVar impossible + +export +Uninhabited (SameShape (TSum as) (TArrow b d)) + where uninhabited TVar impossible + +export +Uninhabited (SameShape (TSum as) (TProd bs)) + where uninhabited TVar impossible + +export +Uninhabited (SameShape (TSum as) (TFix y b)) + where uninhabited TVar impossible + +export +Uninhabited (SameShape (TFix x a) (TVar j)) + where uninhabited TVar impossible + +export +Uninhabited (SameShape (TFix x a) (TArrow b d)) + where uninhabited TVar impossible + +export +Uninhabited (SameShape (TFix x a) (TProd bs)) + where uninhabited TVar impossible + +export +Uninhabited (SameShape (TFix x a) (TSum bs)) + where uninhabited TVar impossible + +namespace Equivalence + public export + data Alpha : Ty ctx1 -> Ty ctx2 -> Type + public export + data AllAlpha : Context (Ty ctx1) -> Context (Ty ctx2) -> Type + + data Alpha where + TVar : elemToNat i.pos = elemToNat j.pos -> Alpha (TVar i) (TVar j) + TArrow : Alpha a b -> Alpha c d -> Alpha (TArrow a c) (TArrow b d) + TProd : AllAlpha as.context bs.context -> Alpha (TProd as) (TProd bs) + TSum : AllAlpha as.context bs.context -> Alpha (TSum as) (TSum bs) + TFix : Alpha a b -> Alpha (TFix x a) (TFix y b) + + data AllAlpha where + Base : AllAlpha [<] [<] + Step : + (i : Elem (n :- b) bs) -> + Alpha a b -> + AllAlpha as (dropElem bs i) -> + AllAlpha (as :< (n :- a)) bs + +namespace Inequivalence + public export + data NotAlpha : Ty ctx1 -> Ty ctx2 -> Type + public export + data AnyNotAlpha : Context (Ty ctx1) -> Context (Ty ctx2) -> Type + + data NotAlpha where + Shape : + Not (SameShape a b) -> + NotAlpha a b + TVar : + Not (elemToNat i.pos = elemToNat j.pos) -> + NotAlpha (TVar i) (TVar j) + TArrow : + These (NotAlpha a b) (NotAlpha c d) -> + NotAlpha (TArrow a c) (TArrow b d) + TProd : + AnyNotAlpha as.context bs.context -> + NotAlpha (TProd as) (TProd bs) + TSum : + AnyNotAlpha as.context bs.context -> + NotAlpha (TSum as) (TSum bs) + TFix : + NotAlpha a b -> + NotAlpha (TFix x a) (TFix y b) + + data AnyNotAlpha where + Base : AnyNotAlpha [<] (bs :< b) + Step1 : + ((b : Ty ctx2) -> Not (Elem (n :- b) bs)) -> + AnyNotAlpha (as :< (n :- a)) bs + Step2 : + (i : Elem (n :- b) bs) -> + These (NotAlpha a b) (AnyNotAlpha as (dropElem bs i)) -> + AnyNotAlpha (as :< (n :- a)) bs + +%name Alpha prf +%name AllAlpha prfs +%name NotAlpha contra +%name AnyNotAlpha contras + +export +alphaShape : Alpha a b -> SameShape a b +alphaShape (TVar prf) = TVar +alphaShape (TArrow prf1 prf2) = TArrow +alphaShape (TProd prfs) = TProd +alphaShape (TSum prfs) = TSum +alphaShape (TFix prf) = TFix + +export +alphaRefl : (a : Ty ctx1) -> (0 b : Ty ctx2) -> a ~=~ b -> Alpha a b +allAlphaRefl : (as : Context (Ty ctx1)) -> (bs : Context (Ty ctx2)) -> as ~=~ bs -> AllAlpha as bs + +alphaRefl (TVar i) .(TVar i) Refl = TVar Refl +alphaRefl (TArrow a b) .(TArrow a b) Refl = TArrow (alphaRefl a a Refl) (alphaRefl b b Refl) +alphaRefl (TProd (MkRow as fresh)) .(TProd (MkRow as fresh)) Refl = TProd (allAlphaRefl as as Refl) +alphaRefl (TSum (MkRow as fresh)) .(TSum (MkRow as fresh)) Refl = TSum (allAlphaRefl as as Refl) +alphaRefl (TFix x a) .(TFix x a) Refl = TFix (alphaRefl a a Refl) + +allAlphaRefl [<] .([<]) Refl = Base +allAlphaRefl (as :< (l :- a)) .(as :< (l :- a)) Refl = + Step Here (alphaRefl a a Refl) (allAlphaRefl as as Refl) + +export +alphaSplit : + {0 a : Ty ctx1} -> {0 b : Ty ctx2} -> + Alpha a b -> NotAlpha a b -> Void +export +allAlphaSplit : + {0 as : Context (Ty ctx1)} -> {0 bs : Context (Ty ctx2)} -> + (0 fresh : AllFresh bs.names) -> + AllAlpha as bs -> AnyNotAlpha as bs -> Void + +alphaSplit prf (Shape contra) = contra (alphaShape prf) +alphaSplit (TVar prf) (TVar contra) = contra prf +alphaSplit (TArrow prf1 prf2) (TArrow contras) = + these (alphaSplit prf1) (alphaSplit prf2) (const $ alphaSplit prf2) contras +alphaSplit (TProd {bs} prfs) (TProd contras) = allAlphaSplit bs.fresh prfs contras +alphaSplit (TSum {bs} prfs) (TSum contras) = allAlphaSplit bs.fresh prfs contras +alphaSplit (TFix prf) (TFix contra) = alphaSplit prf contra + +allAlphaSplit fresh (Step i prf prfs) (Step1 contra) = void $ contra _ i +allAlphaSplit fresh (Step {as, n} i prf prfs) (Step2 j contras) = + let 0 eq = lookupUnique (MkRow bs fresh) i j in + these + (\contra => alphaSplit prf $ rewrite cong fst eq in contra) + (\contras => + allAlphaSplit (dropElemFresh bs fresh i) prfs $ + replace {p = \bi => AnyNotAlpha as (dropElem bs {x = n :- fst bi} $ snd bi)} + (sym eq) + contras) + (\contra, _ => alphaSplit prf $ rewrite cong fst eq in contra) + contras + +export +alpha : (a : Ty ctx1) -> (b : Ty ctx2) -> LazyEither (Alpha a b) (NotAlpha a b) +export +allAlpha : + (as : Context (Ty ctx1)) -> (bs : Context (Ty ctx2)) -> + LazyEither (AllAlpha as bs) (AnyNotAlpha as bs) + +alpha (TVar i) (TVar j) = map TVar TVar $ decEq (elemToNat i.pos) (elemToNat j.pos) +alpha (TVar i) (TArrow a b) = False `Because` Shape absurd +alpha (TVar i) (TProd as) = False `Because` Shape absurd +alpha (TVar i) (TSum as) = False `Because` Shape absurd +alpha (TVar i) (TFix x a) = False `Because` Shape absurd +alpha (TArrow a c) (TVar i) = False `Because` Shape absurd +alpha (TArrow a c) (TArrow b d) = map (uncurry TArrow) TArrow $ all (alpha a b) (alpha c d) +alpha (TArrow a c) (TProd as) = False `Because` Shape absurd +alpha (TArrow a c) (TSum as) = False `Because` Shape absurd +alpha (TArrow a c) (TFix x b) = False `Because` Shape absurd +alpha (TProd as) (TVar i) = False `Because` Shape absurd +alpha (TProd as) (TArrow a b) = False `Because` Shape absurd +alpha (TProd (MkRow as _)) (TProd bs) = map TProd TProd $ allAlpha as bs.context +alpha (TProd as) (TSum bs) = False `Because` Shape absurd +alpha (TProd as) (TFix x a) = False `Because` Shape absurd +alpha (TSum as) (TVar i) = False `Because` Shape absurd +alpha (TSum as) (TArrow a b) = False `Because` Shape absurd +alpha (TSum as) (TProd bs) = False `Because` Shape absurd +alpha (TSum (MkRow as _)) (TSum bs) = map TSum TSum $ allAlpha as bs.context +alpha (TSum as) (TFix x a) = False `Because` Shape absurd +alpha (TFix x a) (TVar i) = False `Because` Shape absurd +alpha (TFix x a) (TArrow b c) = False `Because` Shape absurd +alpha (TFix x a) (TProd as) = False `Because` Shape absurd +alpha (TFix x a) (TSum as) = False `Because` Shape absurd +alpha (TFix x a) (TFix y b) = map TFix TFix $ alpha a b + +allAlpha [<] [<] = True `Because` Base +allAlpha [<] (bs :< nb) = False `Because` Base +allAlpha (as :< (n :- a)) bs = + map + (\((b ** i) ** (prf1, prf2)) => Step i prf1 prf2) + (either Step1 false) $ + (bi := (decLookup n bs).forget) >=> + all (alpha a $ fst bi) (allAlpha as (dropElem bs $ snd bi)) + where + p : (b ** Elem (n :- b) bs) -> Type + p bi = (Alpha a (fst bi), AllAlpha as (dropElem bs $ snd bi)) + + q : (b ** Elem (n :- b) bs) -> Type + q bi = These (NotAlpha a (fst bi)) (AnyNotAlpha as (dropElem bs $ snd bi)) + + false : (bi ** q bi) -> AnyNotAlpha (as :< (n :- a)) bs + false ((b ** i) ** contras) = Step2 i contras + +-- Occurs ---------------------------------------------------------------------- -reflectOccursInAny i [<] = RFalse id -reflectOccursInAny i (as :< (x :- a)) = - reflectThese (reflectOccursIn i a) (reflectOccursInAny i as) +namespace Strengthen + public export + data Strengthen : (i : Var ctx) -> Ty ctx -> Ty (dropElem ctx i.pos) -> Type + public export + data StrengthenAll : + (i : Var ctx) -> (as : Context (Ty ctx)) -> + All (const $ Ty $ dropElem ctx i.pos) as.names -> Type + + data Strengthen where + TVar : (j = index (dropPos i.pos) k) -> Strengthen i (TVar j) (TVar k) + TArrow : Strengthen i a c -> Strengthen i b d -> Strengthen i (TArrow a b) (TArrow c d) + TProd : StrengthenAll i as.context bs -> Strengthen i (TProd as) (TProd $ fromAll as bs) + TSum : StrengthenAll i as.context bs -> Strengthen i (TSum as) (TSum $ fromAll as bs) + TFix : Strengthen (ThereVar i) a b -> Strengthen i (TFix x a) (TFix x b) + + data StrengthenAll where + Lin : StrengthenAll i [<] [<] + (:<) : StrengthenAll i as bs -> Strengthen i a b -> StrengthenAll i (as :< (l :- a)) (bs :< b) + + %name Strengthen prf + %name StrengthenAll prfs + +strengthenEq : Strengthen i a b -> a = thin (dropPos i.pos) b +strengthenAllEq : StrengthenAll i as bs -> as = thinAll (dropPos i.pos) (fromAll as bs) + +strengthenEq (TVar prf) = cong TVar prf +strengthenEq (TArrow prf1 prf2) = cong2 TArrow (strengthenEq prf1) (strengthenEq prf2) +strengthenEq (TProd {as = MkRow _ _} prfs) = cong TProd $ rowCong $ strengthenAllEq prfs +strengthenEq (TSum {as = MkRow _ _} prfs) = cong TSum $ rowCong $ strengthenAllEq prfs +strengthenEq (TFix prf) = cong (TFix _) $ strengthenEq prf + +strengthenAllEq [<] = Refl +strengthenAllEq ((:<) {l} prfs prf) = + cong2 (:<) (strengthenAllEq prfs) (cong (l :-) $ strengthenEq prf) + +namespace Occurs + public export + data OccursIn : Var ctx -> Ty ctx -> Type + public export + data OccursInAny : Var ctx -> Context (Ty ctx) -> Type + + data OccursIn where + TVar : i = j -> i `OccursIn` TVar j + TArrow : These (i `OccursIn` a) (i `OccursIn` b) -> i `OccursIn` TArrow a b + TProd : i `OccursInAny` as.context -> i `OccursIn` TProd as + TSum : i `OccursInAny` as.context -> i `OccursIn` TSum as + TFix : ThereVar i `OccursIn` a -> i `OccursIn` TFix x a + + data OccursInAny where + And : These (i `OccursInAny` as) (i `OccursIn` a) -> i `OccursInAny` (as :< (n :- a)) + + %name OccursIn contra + %name OccursInAny contras + +export +Uninhabited (i `OccursInAny` [<]) where + uninhabited (And prf) impossible + +export +strengthenSplit : Strengthen i a b -> i `OccursIn` a -> Void +strengthenAllSplit : StrengthenAll i as bs -> i `OccursInAny` as -> Void + +strengthenSplit (TVar Refl) (TVar {i = %% n} contra) = void $ lemma _ _ contra + where + lemma : + (i : Elem x sx) -> (j : Elem y (dropElem sx i)) -> + Not (toVar i = toVar (indexPos (dropPos i) j)) + lemma Here j prf = absurd (toVarInjective prf) + lemma (There i) Here prf = absurd (toVarInjective prf) + lemma (There i) (There j) prf = lemma i j $ toVarCong $ thereInjective $ toVarInjective prf +strengthenSplit (TArrow prf1 prf2) (TArrow contras) = + these (strengthenSplit prf1) (strengthenSplit prf2) (const $ strengthenSplit prf2) contras +strengthenSplit (TProd prfs) (TProd contras) = strengthenAllSplit prfs contras +strengthenSplit (TSum prfs) (TSum contras) = strengthenAllSplit prfs contras +strengthenSplit (TFix prf) (TFix contra) = strengthenSplit prf contra + +strengthenAllSplit (prfs :< prf) (And contras) = + these (strengthenAllSplit prfs) (strengthenSplit prf) (const $ strengthenSplit prf) contras + +export +strengthen : + (i : Var ctx) -> (a : Ty ctx) -> + Proof (Ty (dropElem ctx i.pos)) (Strengthen i a) (i `OccursIn` a) +export +strengthenAll : + (i : Var ctx) -> (as : Context (Ty ctx)) -> + Proof (All (const $ Ty $ dropElem ctx i.pos) as.names) (StrengthenAll i as) (i `OccursInAny` as) + +strengthen ((%%) x {pos = i}) (TVar ((%%) y {pos = j})) = + map (TVar . toVar) + (\_, prf => TVar $ toVarCong prf) + (TVar . toVarCong . skipsDropPos i) $ + strengthen (dropPos i) j +strengthen i (TArrow a b) = + map (uncurry TArrow) (\(c, d) => uncurry TArrow) TArrow $ + all (strengthen i a) (strengthen i b) +strengthen i (TProd (MkRow as fresh)) = + map (TProd . fromAll (MkRow as fresh)) (\_ => TProd) TProd $ + strengthenAll i as +strengthen i (TSum (MkRow as fresh)) = + map (TSum . fromAll (MkRow as fresh)) (\_ => TSum) TSum $ + strengthenAll i as +strengthen i (TFix x a) = + map (TFix x) (\_ => TFix) TFix $ + strengthen (ThereVar i) a + +strengthenAll i [<] = Just [<] `Because` [<] +strengthenAll i (as :< (l :- a)) = + map (uncurry (:<) . swap) (\(_, _) => uncurry (:<) . swap) (And . swap) $ + all (strengthen i a) (strengthenAll i as) -- Not Strictly Positive ----------------------------------------------------------- -- We use negation so we get a cause on failure. -NotPositiveIn : Var ctx v -> Ty ctx w -> Type -NotPositiveInAny : Var ctx v -> Row (Ty ctx w) -> Type - -i `NotPositiveIn` TVar j = Void -i `NotPositiveIn` TNat = Void -i `NotPositiveIn` TArrow a b = - -- NOTE: forbid on right side of arrow to prevent infinite breadth. - i `OccursIn` TArrow a b -i `NotPositiveIn` TProd as = i `NotPositiveInAny` as -i `NotPositiveIn` TSum as = i `NotPositiveInAny` as -i `NotPositiveIn` TFix x a = - -- BUG: forbid under fixpoint to prevent unbounded width - -- this is safe to add back with the complex encoding of fixpoints - ThereVar i `OccursIn` a - -i `NotPositiveInAny` [<] = Void -i `NotPositiveInAny` as :< (x :- a) = These (i `NotPositiveIn` a) (i `NotPositiveInAny` as) - --- Not Positive implies Occurs - -notPositiveToOccurs : (a : Ty ctx v) -> i `NotPositiveIn` a -> i `OccursIn` a -notPositiveAnyToOccursAny : (as : Row (Ty ctx v)) -> i `NotPositiveInAny` as -> i `OccursInAny` as - -notPositiveToOccurs (TVar j) = absurd -notPositiveToOccurs TNat = id -notPositiveToOccurs (TArrow a b) = id -notPositiveToOccurs (TProd as) = notPositiveAnyToOccursAny as -notPositiveToOccurs (TSum as) = notPositiveAnyToOccursAny as -notPositiveToOccurs (TFix x a) = id - -notPositiveAnyToOccursAny [<] = id -notPositiveAnyToOccursAny (as :< (x :- a)) = bimap (notPositiveToOccurs a) (notPositiveAnyToOccursAny as) - --- -- Decidable - -notPositiveIn : (i : Var ctx v) -> (a : Ty ctx w) -> Bool -notPositiveInAny : (i : Var ctx v) -> (as : Row (Ty ctx w)) -> Bool - -i `notPositiveIn` (TVar j) = False -i `notPositiveIn` TNat = False -i `notPositiveIn` (TArrow a b) = i `occursIn` TArrow a b -i `notPositiveIn` (TProd as) = i `notPositiveInAny` as -i `notPositiveIn` (TSum as) = i `notPositiveInAny` as -i `notPositiveIn` (TFix x a) = ThereVar i `occursIn` a - -i `notPositiveInAny` [<] = False -i `notPositiveInAny` (as :< (x :- a)) = (i `notPositiveIn` a) || (i `notPositiveInAny` as) - -reflectNotPositiveIn : - (i : Var ctx v) -> (a : Ty ctx w) -> - (i `NotPositiveIn` a) `Reflects` (i `notPositiveIn` a) -reflectNotPositiveInAny : - (i : Var ctx v) -> (as : Row (Ty ctx w)) -> - (i `NotPositiveInAny` as) `Reflects` (i `notPositiveInAny` as) - -reflectNotPositiveIn i (TVar j) = RFalse id -reflectNotPositiveIn i TNat = RFalse id -reflectNotPositiveIn i (TArrow a b) = reflectOccursIn i (TArrow a b) -reflectNotPositiveIn i (TProd as) = reflectNotPositiveInAny i as -reflectNotPositiveIn i (TSum as) = reflectNotPositiveInAny i as -reflectNotPositiveIn i (TFix x a) = reflectOccursIn (ThereVar i) a - -reflectNotPositiveInAny i [<] = RFalse id -reflectNotPositiveInAny i (as :< (x :- a)) = - reflectThese (reflectNotPositiveIn i a) (reflectNotPositiveInAny i as) +namespace NotPositive + public export + data NotPositiveIn : Var ctx -> Ty ctx -> Type + public export + data NotPositiveInAny : Var ctx -> Context (Ty ctx) -> Type --- Well Formed ----------------------------------------------------------------- + data NotPositiveIn where + TArrow : i `OccursIn` TArrow a b -> i `NotPositiveIn` TArrow a b + TProd : i `NotPositiveInAny` as.context -> i `NotPositiveIn` TProd as + TSum : i `NotPositiveInAny` as.context -> i `NotPositiveIn` TSum as + TFix : ThereVar i `NotPositiveIn` a -> i `NotPositiveIn` TFix x a --- Negating decidable properties is fun. + data NotPositiveInAny where + And : + These (i `NotPositiveInAny` as) (i `NotPositiveIn` a) -> + i `NotPositiveInAny` (as :< (n :- a)) + + %name NotPositiveIn prf + %name NotPositiveInAny prf + +export +Uninhabited (i `NotPositiveIn` TVar j) where + uninhabited (TArrow prf) impossible export -IllFormed : Ty ctx v -> Type -AnyIllFormed : Row (Ty ctx v) -> Type +Uninhabited (i `NotPositiveInAny` [<]) where + uninhabited (And prf) impossible -IllFormed (TVar v) = Void -IllFormed TNat = Void -IllFormed (TArrow a b) = These (IllFormed a) (IllFormed b) -IllFormed (TProd as) = AnyIllFormed as -IllFormed (TSum as) = AnyIllFormed as -IllFormed (TFix x a) = These (%% x `NotPositiveIn` a) (IllFormed a) +export +getOccurs : i `NotPositiveIn` a -> i `OccursIn` a +export +getOccursAny : i `NotPositiveInAny` as -> i `OccursInAny` as -AnyIllFormed [<] = Void -AnyIllFormed (as :< (x :- a)) = These (IllFormed a) (AnyIllFormed as) +getOccurs (TArrow prf) = prf +getOccurs (TProd prf) = TProd (getOccursAny prf) +getOccurs (TSum prf) = TSum (getOccursAny prf) +getOccurs (TFix prf) = TFix (getOccurs prf) --- Decidable +getOccursAny (And (This prf)) = And (This (getOccursAny prf)) +getOccursAny (And (That prf)) = And (That (getOccurs prf)) +getOccursAny (And (Both prf1 prf2)) = And (Both (getOccursAny prf1) (getOccurs prf2)) export -illFormed : (a : Ty ctx v) -> Bool -anyIllFormed : (as : Row (Ty ctx v)) -> Bool +notPositiveIn : (i : Var ctx) -> (a : Ty ctx) -> Dec' (i `NotPositiveIn` a) +notPositiveInAny : (i : Var ctx) -> (as : Context (Ty ctx)) -> Dec' (i `NotPositiveInAny` as) + +i `notPositiveIn` TVar j = False `Because` absurd +i `notPositiveIn` TArrow a b = + map TArrow (\(_ ** prf) => \case (TArrow contra) => strengthenSplit prf contra) $ + not $ + (strengthen i $ TArrow a b).forget +i `notPositiveIn` TProd (MkRow as _) = mapDec TProd (\case TProd prf => prf) (i `notPositiveInAny` as) +i `notPositiveIn` TSum (MkRow as _) = mapDec TSum (\case TSum prf => prf) (i `notPositiveInAny` as) +i `notPositiveIn` TFix x a = mapDec TFix (\case TFix prf => prf) $ ThereVar i `notPositiveIn` a + +i `notPositiveInAny` [<] = False `Because` absurd +i `notPositiveInAny` (as :< (n :- a)) = + mapDec (And . swap) (\case And prf => swap prf) $ + orDec (i `notPositiveIn` a) (i `notPositiveInAny` as) -illFormed (TVar j) = False -illFormed TNat = False -illFormed (TArrow a b) = illFormed a || illFormed b -illFormed (TProd as) = anyIllFormed as -illFormed (TSum as) = anyIllFormed as -illFormed (TFix x a) = (%% x `notPositiveIn` a) || illFormed a +-- Well Formed ----------------------------------------------------------------- -anyIllFormed [<] = False -anyIllFormed (as :< (x :- a)) = illFormed a || anyIllFormed as +-- Negating decidable properties is fun. +namespace WellFormed + public export + data IllFormed : Ty ctx -> Type + public export + data AnyIllFormed : Context (Ty ctx) -> Type + + data IllFormed where + TArrow : These (IllFormed a) (IllFormed b) -> IllFormed (TArrow a b) + TProd : AnyIllFormed as.context -> IllFormed (TProd as) + TSum : AnyIllFormed as.context -> IllFormed (TSum as) + TFix : These (toVar Here `NotPositiveIn` a) (IllFormed a) -> IllFormed (TFix x a) + + data AnyIllFormed where + And : These (AnyIllFormed as) (IllFormed a) -> AnyIllFormed (as :< (n :- a)) + +export +Uninhabited (IllFormed (TVar i)) where + uninhabited (TArrow prf) impossible + +export +Uninhabited (AnyIllFormed [<]) where + uninhabited (And prf) impossible + +export +illFormed : (a : Ty ctx) -> Dec' (IllFormed a) export -reflectIllFormed : (a : Ty ctx v) -> IllFormed a `Reflects` illFormed a -reflectAnyIllFormed : (as : Row (Ty ctx v)) -> AnyIllFormed as `Reflects` anyIllFormed as +anyIllFormed : (as : Context (Ty ctx)) -> Dec' (AnyIllFormed as) -reflectIllFormed (TVar j) = RFalse id -reflectIllFormed TNat = RFalse id -reflectIllFormed (TArrow a b) = reflectThese (reflectIllFormed a) (reflectIllFormed b) -reflectIllFormed (TProd as) = reflectAnyIllFormed as -reflectIllFormed (TSum as) = reflectAnyIllFormed as -reflectIllFormed (TFix x a) = reflectThese (reflectNotPositiveIn (%% x) a) (reflectIllFormed a) +illFormed (TVar j) = False `Because` absurd +illFormed (TArrow a b) = mapDec TArrow (\case TArrow prf => prf) $ orDec (illFormed a) (illFormed b) +illFormed (TProd (MkRow as _)) = mapDec TProd (\case TProd prf => prf) (anyIllFormed as) +illFormed (TSum (MkRow as _)) = mapDec TSum (\case TSum prf => prf) (anyIllFormed as) +illFormed (TFix x a) = mapDec TFix (\case TFix prf => prf) $ orDec (%% x `notPositiveIn` a) (illFormed a) -reflectAnyIllFormed [<] = RFalse id -reflectAnyIllFormed (as :< (x :- a)) = - reflectThese (reflectIllFormed a) (reflectAnyIllFormed as) +anyIllFormed [<] = False `Because` absurd +anyIllFormed (as :< (n :- a)) = + mapDec (And . swap) (\case And prf => swap prf) $ + orDec (illFormed a) (anyIllFormed as) -------------------------------------------------------------------------------- -- Substitution ---------------------------------------------------------------- -------------------------------------------------------------------------------- -public export -fromVar : Either (Var ctx v) (Ty ctx v) -> Ty ctx v -fromVar = either TVar id - export -sub : Env ctx1 ctx2 (Ty ctx2) -> Ty ctx1 v -> Ty ctx2 v -subAll : Env ctx1 ctx2 (Ty ctx2) -> Row (Ty ctx1 v) -> Row (Ty ctx2 v) -subAllFresh : - (env : Env ctx1 ctx2 (Ty ctx2)) -> (x : String) -> - (row : Row (Ty ctx1 v)) -> - So (x `freshIn` row) -> So (x `freshIn` subAll env row) - -sub env (TVar i) = fromVar $ lookup env i -sub env TNat = TNat +sub : All (const $ Thinned Ty ctx2) ctx1 -> Ty ctx1 -> Ty ctx2 +subAll : All (const $ Thinned Ty ctx2) ctx1 -> Context (Ty ctx1) -> Context (Ty ctx2) +subAllNames : + (f : All (const $ Thinned Ty ctx2) ctx1) -> + (ctx : Context (Ty ctx1)) -> + (subAll f ctx).names = ctx.names + +sub env (TVar i) = (indexAll i.pos env).extract sub env (TArrow a b) = TArrow (sub env a) (sub env b) -sub env (TProd as) = TProd (subAll env as) -sub env (TSum as) = TSum (subAll env as) -sub env (TFix x a) = TFix x (sub (lift (Drop Id) env :< (x :- TVar (%% x))) a) +sub env (TProd (MkRow as fresh)) = TProd (MkRow (subAll env as) (rewrite subAllNames env as in fresh)) +sub env (TSum (MkRow as fresh)) = TSum (MkRow (subAll env as) (rewrite subAllNames env as in fresh)) +sub env (TFix x a) = TFix x (sub (mapProperty (rename (Drop Id)) env :< (TVar (%% x) `Over` Id)) a) subAll env [<] = [<] -subAll env ((:<) as (x :- a) {fresh}) = - (:<) (subAll env as) (x :- sub env a) {fresh = subAllFresh env x as fresh} +subAll env (as :< (n :- a)) = subAll env as :< (n :- sub env a) -subAllFresh env x [<] = id -subAllFresh env x (as :< (y :- a)) = andSo . mapSnd (subAllFresh env x as) . soAnd +subAllNames env [<] = Refl +subAllNames env (as :< (n :- a)) = cong (:< n) (subAllNames env as) --- Expansion ------------------------------------------------------------------- +-- Special Types --------------------------------------------------------------- -export -expandEnv : DEnv Ty ctx -> Env ctx [<] (Ty [<]) -expandEnv [<] = Base Id -expandEnv {ctx = ctx :< (x :- v)} (env :< (y :- a)) = - let env' = expandEnv env in - expandEnv env :< (x :- sub env' a) +public export +TNat : Ty ctx +TNat = TFix "Nat" (TSum [<"Z" :- TProd [<], "S" :- TVar (%% "Nat")]) -export -expand : DEnv Ty ctx -> Ty ctx v -> Ty [<] v -expand = sub . expandEnv +public export +TList : Ty ctx -> Ty ctx +TList a = + TFix "List" (TSum + [<"N" :- TProd [<] + , "C" :- TProd [<"H" :- thin (Drop Id) a, "T" :- TVar (%% "List")]]) + +-- Testing if we have a list + +-- TODO: prove correct +isList : (a : Ty ctx) -> Maybe (Ty ctx) +isList (TFix x (TSum (MkRow + [<"N" :- TProd (MkRow [<] _) + , "C" :- TProd (MkRow [<"H" :- a, "T" :- TVar ((%%) x {pos = Here})] _)] _))) = + does (strengthen (%% x) a) +isList (TFix x (TSum (MkRow + [<"N" :- TProd (MkRow [<] _) + , "C" :- TProd (MkRow [<"T" :- TVar ((%%) x {pos = Here}), "H" :- a] _)] _))) = + does (strengthen (%% x) a) +isList (TFix x (TSum (MkRow + [<"C" :- TProd (MkRow [<"H" :- a, "T" :- TVar ((%%) x {pos = Here})] _) + , "N" :- TProd (MkRow [<] _)] _))) = + does (strengthen (%% x) a) +isList (TFix x (TSum (MkRow + [<"C" :- TProd (MkRow [<"T" :- TVar ((%%) x {pos = Here}), "H" :- a] _) + , "N" :- TProd (MkRow [<] _)] _))) = + does (strengthen (%% x) a) +isList _ = Nothing |