summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Inky.idr4
-rw-r--r--src/Inky/Term.idr39
-rw-r--r--src/Inky/Type.idr141
3 files changed, 124 insertions, 60 deletions
diff --git a/src/Inky.idr b/src/Inky.idr
index 40e9286..0c4db56 100644
--- a/src/Inky.idr
+++ b/src/Inky.idr
@@ -54,8 +54,8 @@ parseTerm toks = do
checkType : HasErr String es => Ty [<] -> App es ()
checkType a = do
- let False `Because` wf = illFormed a
- | True `Because` bad => throw "type ill-formed"
+ let True `Because` wf = wellFormed a
+ | False `Because` bad => throw "type ill-formed"
pure ()
checkTerm : (a : Ty [<]) -> (t : Term m [<] [<]) -> HasErr (NotChecks [<] [<] a t) es => App es ()
diff --git a/src/Inky/Term.idr b/src/Inky/Term.idr
index 454c096..1fb50ea 100644
--- a/src/Inky/Term.idr
+++ b/src/Inky/Term.idr
@@ -220,7 +220,7 @@ namespace Branches
data Synths where
AnnotS :
- Not (IllFormed a) ->
+ WellFormed a ->
Checks tyEnv tmEnv (sub tyEnv a) t ->
Synths tyEnv tmEnv (Annot meta t a) (sub tyEnv a)
VarS :
@@ -230,7 +230,7 @@ data Synths where
Synths tyEnv (tmEnv :< (a `Over` Id)) f b ->
Synths tyEnv tmEnv (Let meta e (x ** f)) b
LetTyS :
- Not (IllFormed a) ->
+ WellFormed a ->
Synths (tyEnv :< (sub tyEnv a `Over` Id)) tmEnv e b ->
Synths tyEnv tmEnv (LetTy meta a (x ** e)) b
AppS :
@@ -248,16 +248,16 @@ data Synths where
Synths tyEnv tmEnv e (TFix x a) ->
Synths tyEnv tmEnv (Unroll meta e) (sub [<TFix x a `Over` Id] a)
MapS :
- Not (IllFormed (TFix x a)) ->
- Not (IllFormed b) ->
- Not (IllFormed c) ->
+ WellFormed (TFix x a) ->
+ WellFormed b ->
+ WellFormed c ->
Synths tyEnv tmEnv (Map meta (x ** a) b c)
(TArrow (TArrow (sub tyEnv b) (sub tyEnv c))
(TArrow (sub (tyEnv :< (sub tyEnv b `Over` Id)) a)
(sub (tyEnv :< (sub tyEnv c `Over` Id)) a)))
GetChildrenS :
- Not (IllFormed (TFix x a)) ->
- Not (IllFormed b) ->
+ WellFormed (TFix x a) ->
+ WellFormed b ->
Synths tyEnv tmEnv (GetChildren meta (x ** a) b)
(TArrow (sub (tyEnv :< (sub tyEnv b `Over` Id)) a)
(TProd
@@ -275,7 +275,7 @@ data Checks where
Checks tyEnv (tmEnv :< (a `Over` Id)) b t ->
Checks tyEnv tmEnv b (Let meta e (x ** t))
LetTyC :
- Not (IllFormed a) ->
+ WellFormed a ->
Checks (tyEnv :< (sub tyEnv a `Over` Id)) tmEnv b t ->
Checks tyEnv tmEnv b (LetTy meta a (x ** t))
AbsC :
@@ -600,14 +600,14 @@ allBranchesSplit :
AllBranches tyEnv tmEnv as a ts -> AnyNotBranches tyEnv tmEnv as a ts -> Void
synthsSplit (AnnotS wf prf) (AnnotNS contras) =
- these wf (checksSplit prf) (const $ checksSplit prf) contras
+ these (wellFormedSplit wf) (checksSplit prf) (const $ checksSplit prf) contras
synthsSplit VarS contra = absurd contra
synthsSplit (LetS prf1 prf2) (LetNS1 contra) = synthsSplit prf1 contra
synthsSplit (LetS prf1 prf2) (LetNS2 prf1' contra) =
let contra = rewrite synthsUnique prf1 prf1' in contra in
synthsSplit prf2 contra
synthsSplit (LetTyS wf prf) (LetTyNS contras) =
- these wf (synthsSplit prf) (const $ synthsSplit prf) contras
+ these (wellFormedSplit wf) (synthsSplit prf) (const $ synthsSplit prf) contras
synthsSplit (AppS prf prfs) (AppNS1 contra) = synthsSplit prf contra
synthsSplit (AppS prf prfs) (AppNS2 prf' contras) =
let contras = rewrite synthsUnique prf prf' in contras in
@@ -623,9 +623,12 @@ synthsSplit (UnrollS prf) (UnrollNS1 contra) = synthsSplit prf contra
synthsSplit (UnrollS {x, a} prf) (UnrollNS2 prf' contra) =
void $ contra x a $ synthsUnique prf' prf
synthsSplit (MapS wf1 wf2 wf3) (MapNS contras) =
- these wf1 (these wf2 wf3 (const wf3)) (const $ these wf2 wf3 (const wf3)) contras
+ these (wellFormedSplit wf1)
+ (these (wellFormedSplit wf2) (wellFormedSplit wf3) (const $ wellFormedSplit wf3))
+ (const $ these (wellFormedSplit wf2) (wellFormedSplit wf3) (const $ wellFormedSplit wf3))
+ contras
synthsSplit (GetChildrenS wf1 wf2) (GetChildrenNS contras) =
- these wf1 wf2 (const wf2) contras
+ these (wellFormedSplit wf1) (wellFormedSplit wf2) (const $ wellFormedSplit wf2) contras
checksSplit (EmbedC _ prf1 prf2) (EmbedNC1 _ contra) = synthsSplit prf1 contra
checksSplit (EmbedC _ prf1 prf2) (EmbedNC2 _ prf1' contra) =
@@ -636,7 +639,7 @@ checksSplit (LetC prf1 prf2) (LetNC2 prf1' contra) =
let contra = rewrite synthsUnique prf1 prf1' in contra in
checksSplit prf2 contra
checksSplit (LetTyC wf prf) (LetTyNC contras) =
- these wf (checksSplit prf) (const $ checksSplit prf) contras
+ these (wellFormedSplit wf) (checksSplit prf) (const $ checksSplit prf) contras
checksSplit (AbsC prf1 prf2) (AbsNC1 contra) = isFunctionSplit prf1 contra
checksSplit (AbsC prf1 prf2) (AbsNC2 prf1' contra) =
let (eq1, eq2) = isFunctionUnique prf1 prf1' in
@@ -752,7 +755,7 @@ allBranches :
synths tyEnv tmEnv (Annot _ t a) =
pure (sub tyEnv a) $
map (uncurry AnnotS) AnnotNS $
- all (not $ illFormed a) (checks tyEnv tmEnv (sub tyEnv a) t)
+ all (wellFormed a) (checks tyEnv tmEnv (sub tyEnv a) t)
synths tyEnv tmEnv (Var _ i) = Just (indexAll i.pos tmEnv).extract `Because` VarS
synths tyEnv tmEnv (Let _ e (x ** f)) =
map snd
@@ -761,7 +764,7 @@ synths tyEnv tmEnv (Let _ e (x ** f)) =
(a := synths tyEnv tmEnv e) >=> synths tyEnv (tmEnv :< (a `Over` Id)) f
synths tyEnv tmEnv (LetTy _ a (x ** e)) =
map id (\_, (wf, prf) => LetTyS wf prf) LetTyNS $
- all (not $ illFormed a) (synths (tyEnv :< (sub tyEnv a `Over` Id)) tmEnv e)
+ all (wellFormed a) (synths (tyEnv :< (sub tyEnv a `Over` Id)) tmEnv e)
synths tyEnv tmEnv (Abs _ (bound ** t)) = Nothing `Because` ChecksNS Abs
synths tyEnv tmEnv (App _ e ts) =
map snd
@@ -821,11 +824,11 @@ synths tyEnv tmEnv (Fold _ e (x ** t)) = Nothing `Because` ChecksNS Fold
synths tyEnv tmEnv (Map _ (x ** a) b c) =
pure _ $
map (\(wf1, wf2, wf3) => MapS wf1 wf2 wf3) MapNS $
- all (not $ illFormed (TFix x a)) (all (not $ illFormed b) (not $ illFormed c))
+ all (wellFormed (TFix x a)) (all (wellFormed b) (wellFormed c))
synths tyEnv tmEnv (GetChildren _ (x ** a) b) =
pure _ $
map (uncurry GetChildrenS) GetChildrenNS $
- all (not $ illFormed (TFix x a)) (not $ illFormed b)
+ all (wellFormed (TFix x a)) (wellFormed b)
checks tyEnv tmEnv a (Annot meta t b) = fallbackCheck Annot (synths tyEnv tmEnv $ Annot meta t b) a
checks tyEnv tmEnv a (Var meta i) = fallbackCheck Var (synths tyEnv tmEnv $ Var meta i) a
@@ -836,7 +839,7 @@ checks tyEnv tmEnv a (Let _ e (x ** t)) =
(b := synths tyEnv tmEnv e) >=> checks tyEnv (tmEnv :< (b `Over` Id)) a t
checks tyEnv tmEnv a (LetTy _ b (x ** t)) =
map (uncurry LetTyC) LetTyNC $
- all (not $ illFormed b) (checks (tyEnv :< (sub tyEnv b `Over` Id)) tmEnv a t)
+ all (wellFormed b) (checks (tyEnv :< (sub tyEnv b `Over` Id)) tmEnv a t)
checks tyEnv tmEnv a (Abs meta (bound ** t)) =
map
(\((_, _) ** (prf1, prf2)) => AbsC prf1 prf2)
diff --git a/src/Inky/Type.idr b/src/Inky/Type.idr
index 45645bc..f40ecba 100644
--- a/src/Inky/Type.idr
+++ b/src/Inky/Type.idr
@@ -512,7 +512,7 @@ namespace Occurs
export
Uninhabited (i `OccursInAny` [<]) where
- uninhabited (And prf) impossible
+ uninhabited (And contras) impossible
export
strengthenSplit : Strengthen i a b -> i `OccursIn` a -> Void
@@ -569,7 +569,26 @@ strengthenAll i (as :< (l :- a)) =
-- Not Strictly Positive -----------------------------------------------------------
--- We use negation so we get a cause on failure.
+namespace StrictlyPositive
+ public export
+ data StrictlyPositiveIn : Var ctx -> Ty ctx -> Type
+ public export
+ data StrictlyPositiveInAll : Var ctx -> Context (Ty ctx) -> Type
+
+ data StrictlyPositiveIn where
+ TVar : i `StrictlyPositiveIn` TVar j
+ TArrow : Strengthen i (TArrow a b) c -> i `StrictlyPositiveIn` TArrow a b
+ TProd : i `StrictlyPositiveInAll` as.context -> i `StrictlyPositiveIn` TProd as
+ TSum : i `StrictlyPositiveInAll` as.context -> i `StrictlyPositiveIn` TSum as
+ TFix : ThereVar i `StrictlyPositiveIn` a -> i `StrictlyPositiveIn` TFix x a
+ data StrictlyPositiveInAll where
+ Lin : i `StrictlyPositiveInAll` [<]
+ (:<) :
+ i `StrictlyPositiveInAll` as -> i `StrictlyPositiveIn` a ->
+ i `StrictlyPositiveInAll` (as :< (l :- a))
+
+ %name StrictlyPositiveIn prf
+ %name StrictlyPositiveInAll prfs
namespace NotPositive
public export
@@ -588,48 +607,53 @@ namespace NotPositive
These (i `NotPositiveInAny` as) (i `NotPositiveIn` a) ->
i `NotPositiveInAny` (as :< (n :- a))
- %name NotPositiveIn prf
- %name NotPositiveInAny prf
+ %name NotPositiveIn contra
+ %name NotPositiveInAny contras
export
Uninhabited (i `NotPositiveIn` TVar j) where
- uninhabited (TArrow prf) impossible
+ uninhabited (TArrow contra) impossible
export
Uninhabited (i `NotPositiveInAny` [<]) where
- uninhabited (And prf) impossible
+ uninhabited (And contras) impossible
export
-getOccurs : i `NotPositiveIn` a -> i `OccursIn` a
-export
-getOccursAny : i `NotPositiveInAny` as -> i `OccursInAny` as
+strictlyPositiveSplit : i `StrictlyPositiveIn` a -> i `NotPositiveIn` a -> Void
+strictlyPositiveAllSplit : i `StrictlyPositiveInAll` as -> i `NotPositiveInAny` as -> Void
-getOccurs (TArrow prf) = prf
-getOccurs (TProd prf) = TProd (getOccursAny prf)
-getOccurs (TSum prf) = TSum (getOccursAny prf)
-getOccurs (TFix prf) = TFix (getOccurs prf)
+strictlyPositiveSplit (TArrow prf) (TArrow contra) = strengthenSplit prf contra
+strictlyPositiveSplit (TProd prfs) (TProd contras) = strictlyPositiveAllSplit prfs contras
+strictlyPositiveSplit (TSum prfs) (TSum contras) = strictlyPositiveAllSplit prfs contras
+strictlyPositiveSplit (TFix prf) (TFix contra) = strictlyPositiveSplit prf contra
-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))
+strictlyPositiveAllSplit (prfs :< prf) (And contras) =
+ these
+ (strictlyPositiveAllSplit prfs)
+ (strictlyPositiveSplit prf)
+ (const $ strictlyPositiveSplit prf)
+ contras
export
-notPositiveIn : (i : Var ctx) -> (a : Ty ctx) -> Dec' (i `NotPositiveIn` a)
-notPositiveInAny : (i : Var ctx) -> (as : Context (Ty ctx)) -> Dec' (i `NotPositiveInAny` as)
+strictlyPositiveIn :
+ (i : Var ctx) -> (a : Ty ctx) ->
+ LazyEither (i `StrictlyPositiveIn` a) (i `NotPositiveIn` a)
+strictlyPositiveInAll :
+ (i : Var ctx) -> (as : Context (Ty ctx)) ->
+ LazyEither (i `StrictlyPositiveInAll` as) (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 $
+i `strictlyPositiveIn` TVar j = True `Because` TVar
+i `strictlyPositiveIn` TArrow a b =
+ map (\(_ ** prf) => TArrow prf) TArrow $
(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 `strictlyPositiveIn` TProd (MkRow as _) = map TProd TProd $ i `strictlyPositiveInAll` as
+i `strictlyPositiveIn` TSum (MkRow as _) = map TSum TSum $ i `strictlyPositiveInAll` as
+i `strictlyPositiveIn` TFix x a = map TFix TFix $ ThereVar i `strictlyPositiveIn` 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)
+i `strictlyPositiveInAll` [<] = True `Because` [<]
+i `strictlyPositiveInAll` (as :< (n :- a)) =
+ map (uncurry (:<) . swap) (And . swap) $
+ all (i `strictlyPositiveIn` a) (i `strictlyPositiveInAll` as)
-- Well Formed -----------------------------------------------------------------
@@ -637,6 +661,26 @@ i `notPositiveInAny` (as :< (n :- a)) =
namespace WellFormed
public export
+ data WellFormed : Ty ctx -> Type
+ public export
+ data AllWellFormed : Context (Ty ctx) -> Type
+
+ data WellFormed where
+ TVar : WellFormed (TVar i)
+ TArrow : WellFormed a -> WellFormed b -> WellFormed (TArrow a b)
+ TProd : AllWellFormed as.context -> WellFormed (TProd as)
+ TSum : AllWellFormed as.context -> WellFormed (TSum as)
+ TFix : toVar Here `StrictlyPositiveIn` a -> WellFormed a -> WellFormed (TFix x a)
+
+ data AllWellFormed where
+ Lin : AllWellFormed [<]
+ (:<) : AllWellFormed as -> WellFormed a -> AllWellFormed (as :< (n :- a))
+
+ %name WellFormed wf
+ %name AllWellFormed wfs
+
+namespace IllFormed
+ public export
data IllFormed : Ty ctx -> Type
public export
data AnyIllFormed : Context (Ty ctx) -> Type
@@ -650,6 +694,9 @@ namespace WellFormed
data AnyIllFormed where
And : These (AnyIllFormed as) (IllFormed a) -> AnyIllFormed (as :< (n :- a))
+ %name IllFormed bad
+ %name AnyIllFormed bads
+
export
Uninhabited (IllFormed (TVar i)) where
uninhabited (TArrow prf) impossible
@@ -659,20 +706,34 @@ Uninhabited (AnyIllFormed [<]) where
uninhabited (And prf) impossible
export
-illFormed : (a : Ty ctx) -> Dec' (IllFormed a)
+wellFormedSplit : WellFormed a -> IllFormed a -> Void
+allWellFormedSplit : AllWellFormed as -> AnyIllFormed as -> Void
+
+wellFormedSplit (TArrow wf1 wf2) (TArrow bads) =
+ these (wellFormedSplit wf1) (wellFormedSplit wf2) (const $ wellFormedSplit wf2) bads
+wellFormedSplit (TProd wfs) (TProd bads) = allWellFormedSplit wfs bads
+wellFormedSplit (TSum wfs) (TSum bads) = allWellFormedSplit wfs bads
+wellFormedSplit (TFix prf wf) (TFix bads) =
+ these (strictlyPositiveSplit prf) (wellFormedSplit wf) (const $ wellFormedSplit wf) bads
+
+allWellFormedSplit (wfs :< wf) (And bads) =
+ these (allWellFormedSplit wfs) (wellFormedSplit wf) (const $ wellFormedSplit wf) bads
+
+export
+wellFormed : (a : Ty ctx) -> LazyEither (WellFormed a) (IllFormed a)
export
-anyIllFormed : (as : Context (Ty ctx)) -> Dec' (AnyIllFormed as)
+allWellFormed : (as : Context (Ty ctx)) -> LazyEither (AllWellFormed as) (AnyIllFormed as)
-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)
+wellFormed (TVar j) = True `Because` TVar
+wellFormed (TArrow a b) = map (uncurry TArrow) TArrow $ all (wellFormed a) (wellFormed b)
+wellFormed (TProd (MkRow as _)) = map TProd TProd $ allWellFormed as
+wellFormed (TSum (MkRow as _)) = map TSum TSum $ allWellFormed as
+wellFormed (TFix x a) = map (uncurry TFix) TFix $ all (%% x `strictlyPositiveIn` a) (wellFormed a)
-anyIllFormed [<] = False `Because` absurd
-anyIllFormed (as :< (n :- a)) =
- mapDec (And . swap) (\case And prf => swap prf) $
- orDec (illFormed a) (anyIllFormed as)
+allWellFormed [<] = True `Because` [<]
+allWellFormed (as :< (n :- a)) =
+ map (uncurry (:<) . swap) (And . swap) $
+ all (wellFormed a) (allWellFormed as)
--------------------------------------------------------------------------------
-- Substitution ----------------------------------------------------------------
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-30 07:41:09 +0000