diff options
Diffstat (limited to 'src/Inky')
| -rw-r--r-- | src/Inky/Kind.idr | 50 | ||||
| -rw-r--r-- | src/Inky/OnlyWhen.idr | 44 | ||||
| -rw-r--r-- | src/Inky/Type.idr | 110 |
3 files changed, 204 insertions, 0 deletions
diff --git a/src/Inky/Kind.idr b/src/Inky/Kind.idr new file mode 100644 index 0000000..a09c97d --- /dev/null +++ b/src/Inky/Kind.idr @@ -0,0 +1,50 @@ +module Inky.Kind + +import Control.Function +import Data.Bool.Decidable +import Decidable.Equality.Core + +public export +data Kind : Type where + KStar : Kind + KArrow : Kind -> Kind -> Kind + +export +Eq Kind where + KStar == KStar = True + (t1 `KArrow` u1) == (t2 `KArrow` u2) = t1 == t2 && u1 == u2 + _ == _ = False + +export +Uninhabited (KStar = KArrow t u) where + uninhabited prf impossible + +export +Uninhabited (KArrow t u = KStar) where + uninhabited prf impossible + +export +Biinjective KArrow where + biinjective Refl = (Refl, Refl) + +export +DecEq Kind where + decEq KStar KStar = Yes Refl + decEq KStar (KArrow _ _) = No absurd + decEq (KArrow k1 k2) KStar = No absurd + decEq (KArrow k1 k2) (KArrow j1 j2) = + case (decEq k1 j1, decEq k2 j2) of + (Yes eq1, Yes eq2) => Yes (cong2 KArrow eq1 eq2) + (Yes eq1, No neq2) => No (neq2 . snd . biinjective) + (No neq1, _) => No (neq1 . fst . biinjective) + +export +decEqReflects : (k, j : Kind) -> (k = j) `Reflects` (k == j) +decEqReflects KStar KStar = RTrue Refl +decEqReflects KStar (KArrow _ _) = RFalse absurd +decEqReflects (KArrow k1 k2) KStar = RFalse absurd +decEqReflects (KArrow k1 k2) (KArrow j1 j2) with (decEqReflects k1 j1) | (k1 == j1) + _ | RTrue eq1 | _ with (decEqReflects k2 j2) | (k2 == j2) + _ | RTrue eq2 | _ = RTrue (cong2 KArrow eq1 eq2) + _ | RFalse neq2 | _ = RFalse (neq2 . snd . biinjective) + _ | RFalse neq1 | _ = RFalse (neq1 . fst . biinjective) diff --git a/src/Inky/OnlyWhen.idr b/src/Inky/OnlyWhen.idr new file mode 100644 index 0000000..7bed91a --- /dev/null +++ b/src/Inky/OnlyWhen.idr @@ -0,0 +1,44 @@ +module Inky.OnlyWhen + +import Data.DPair + +public export +data OnlyWhen : Maybe a -> (a -> Type) -> Type where + Yes : forall x. (px : p x) -> Just x `OnlyWhen` p + No : ((x : a) -> Not (p x)) -> Nothing `OnlyWhen` p + +public export +decDPair : (v ** v `OnlyWhen` p) <=> Dec (x : a ** p x) +decDPair = + MkEquivalence + { leftToRight = \case + (Just x ** Yes px) => Yes (x ** px) + (Nothing ** No prf) => No (\(x ** px) => prf x px) + , rightToLeft = \case + Yes (x ** px) => (Just x ** Yes px) + No prf => (Nothing ** No (\x, px => prf (x ** px))) + } + +public export +decExists : Exists (`OnlyWhen` p) <=> Dec (Exists p) +decExists = + MkEquivalence + { leftToRight = \case + Evidence .(Just x) (Yes px) => Yes (Evidence x px) + Evidence .(Nothing) (No prf) => No (\(Evidence x px) => void (prf x px)) + , rightToLeft = \case + Yes (Evidence x px) => Evidence (Just x) (Yes px) + No prf => Evidence Nothing (No (\x, px => prf (Evidence x px))) + } + +public export +decSubset : Subset (Maybe a) (`OnlyWhen` p) <=> Dec (Subset a p) +decSubset = + MkEquivalence + { leftToRight = \case + Element (Just x) prf => Yes (Element x (case prf of Yes px => px)) + Element Nothing prf => No (\(Element x px) => void (case prf of No prf => prf x px)) + , rightToLeft = \case + Yes (Element x px) => Element (Just x) (Yes px) + No prf => Element Nothing (No (\x, px => prf (Element x px))) + } diff --git a/src/Inky/Type.idr b/src/Inky/Type.idr new file mode 100644 index 0000000..8c4285e --- /dev/null +++ b/src/Inky/Type.idr @@ -0,0 +1,110 @@ +module Inky.Type + +import Data.Bool.Decidable +import Data.DPair +import Inky.Binding +import Inky.Env +import Inky.Kind +import Inky.OnlyWhen + +namespace Raw + public export + data RawSTy : World -> Type where + + public export + data RawCTy : World -> Type where + + data RawSTy where + TVar : (x : Name w) -> RawSTy w + TNat : RawSTy w + TArrow : RawCTy w -> RawCTy w -> RawSTy w + TApp : RawSTy w -> RawCTy w -> RawSTy w + TAnnot : RawCTy w -> Kind -> RawSTy w + + data RawCTy where + TFix : (x : Binder) -> RawCTy (w :< x) -> RawCTy w + TEmbed : RawSTy w -> RawCTy w + +public export +data SynthKind : Env Kind w -> RawSTy w -> Kind -> Type where +public export +data CheckKind : Env Kind w -> Kind -> RawCTy w -> Type where + +data SynthKind where + TVar : SynthKind env (TVar x) (lookup env x) + TNat : SynthKind env TNat KStar + TArrow : CheckKind env KStar t -> CheckKind env KStar u -> SynthKind env (t `TArrow` u) KStar + TApp : SynthKind env f (k `KArrow` j) -> CheckKind env k t -> SynthKind env (f `TApp` t) j + TAnnot : CheckKind env k t -> SynthKind env (TAnnot t k) k + +data CheckKind where + TFix : CheckKind (env :< (x :~ k)) k t -> CheckKind env k (TFix x t) + TEmbed : SynthKind env a j -> k = j -> CheckKind env k (TEmbed a) + +export +synthKindUniq : SynthKind env t k -> SynthKind env t j -> k = j +synthKindUniq TVar TVar = Refl +synthKindUniq TNat TNat = Refl +synthKindUniq (TArrow p1 p2) (TArrow p3 p4) = Refl +synthKindUniq (TApp p1 p2) (TApp p3 p4) = case (synthKindUniq p1 p3) of Refl => Refl +synthKindUniq (TAnnot p1) (TAnnot p2) = Refl + +export +synthKind : (env : Env Kind w) -> (a : RawSTy w) -> Maybe Kind +export +checkKind : (env : Env Kind w) -> (k : Kind) -> (t : RawCTy w) -> Bool + +synthKind env (TVar x) = Just (lookup env x) +synthKind env TNat = Just KStar +synthKind env (TArrow t u) = do + guard (checkKind env KStar t) + guard (checkKind env KStar u) + Just KStar +synthKind env (TApp f t) = do + dom `KArrow` cod <- synthKind env f + | _ => Nothing + guard (checkKind env dom t) + Just cod +synthKind env (TAnnot t k) = do + guard (checkKind env k t) + Just k + +checkKind env k (TFix x t) = checkKind (env :< (x :~ k)) k t +checkKind env k (TEmbed a) = + case synthKind env a of + Nothing => False + Just k' => k == k' + +export +synthKindPrf : (env : Env Kind w) -> (a : RawSTy w) -> synthKind env a `OnlyWhen` SynthKind env a +export +checkKindPrf : (env : Env Kind w) -> (k : Kind) -> (t : RawCTy w) -> CheckKind env k t `Reflects` checkKind env k t + +synthKindPrf env (TVar x) = Yes TVar +synthKindPrf env TNat = Yes TNat +synthKindPrf env (TArrow t u) with (checkKindPrf env KStar t) | (checkKind env KStar t) + _ | RTrue tStar | _ with (checkKindPrf env KStar u) | (checkKind env KStar u) + _ | RTrue uStar | _ = Yes (TArrow tStar uStar) + _ | RFalse uUnstar | _ = No (\_ => \case TArrow _ uStar => uUnstar uStar) + _ | RFalse tUnstar | _ = No (\_ => \case TArrow tStar _ => tUnstar tStar) +synthKindPrf env (TApp f t) with (synthKindPrf env f) | (synthKind env f) + _ | Yes fArrow | Just (KArrow dom cod) with (checkKindPrf env dom t) | (checkKind env dom t) + _ | RTrue uDom | _ = Yes (TApp fArrow uDom) + _ | RFalse uUndom | _ = + No (\_ => \case + TApp fKind uDom => case synthKindUniq fArrow fKind of + Refl => uUndom uDom) + _ | Yes fStar | Just KStar = No (\_ => \case TApp fArrow _ => absurd (synthKindUniq fStar fArrow)) + _ | No fUnkind | Nothing = No (\_ => \case TApp fKind _ => void (fUnkind _ fKind)) +synthKindPrf env (TAnnot t k) with (checkKindPrf env k t) | (checkKind env k t) + _ | RTrue tKind | _ = Yes (TAnnot tKind) + _ | RFalse tUnkind | _ = No (\_ => \case TAnnot tKind => tUnkind tKind) + +checkKindPrf env k (TFix x t) with (checkKindPrf (env :< (x :~ k)) k t) | (checkKind (env :< (x :~ k)) k t) + _ | RTrue tKind | _ = RTrue (TFix tKind) + _ | RFalse tUnkind | _ = RFalse (\case TFix tKind => tUnkind tKind) +checkKindPrf env k (TEmbed a) with (synthKindPrf env a) | (synthKind env a) + _ | Yes aKind | Just k' with (decEqReflects k k') | (k == k') + _ | RTrue eq | _ = RTrue (TEmbed aKind eq) + _ | RFalse neq | _ = RFalse (\case TEmbed aKind' eq => neq $ trans eq $ synthKindUniq aKind' aKind) + _ | No aUnkind | _ = RFalse (\case TEmbed aKind Refl => aUnkind _ aKind) |