summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Inky/Data/Assoc.idr12
-rw-r--r--src/Inky/Data/Context.idr14
-rw-r--r--src/Inky/Data/Irrelevant.idr19
-rw-r--r--src/Inky/Data/Row.idr17
-rw-r--r--src/Inky/Data/SnocList/Quantifiers.idr15
-rw-r--r--src/Inky/Decidable.idr18
-rw-r--r--src/Inky/Decidable/Either.idr5
-rw-r--r--src/Inky/Term.idr101
-rw-r--r--src/Inky/Term/Checks.idr56
-rw-r--r--src/Inky/Term/Desugar.idr110
-rw-r--r--src/Inky/Term/Substitution.idr14
-rw-r--r--src/Inky/Type.idr43
12 files changed, 157 insertions, 267 deletions
diff --git a/src/Inky/Data/Assoc.idr b/src/Inky/Data/Assoc.idr
index a009515..0818ba3 100644
--- a/src/Inky/Data/Assoc.idr
+++ b/src/Inky/Data/Assoc.idr
@@ -15,6 +15,18 @@ Functor Assoc where
namespace Irrelevant
public export
+ record Assoc0 (0 a : Type) (n : String) where
+ constructor (:-)
+ 0 name : String
+ {auto 0 prf : n = name}
+ value : a
+
+ public export
+ map : (a -> b) -> Assoc0 a n -> Assoc0 b n
+ map f (n :- x) = n :- f x
+
+namespace Contexts
+ public export
record Assoc0 (0 p : a -> Type) (x : Assoc a) where
constructor (:-)
0 name : String
diff --git a/src/Inky/Data/Context.idr b/src/Inky/Data/Context.idr
index 0d3df99..4c5f6cf 100644
--- a/src/Inky/Data/Context.idr
+++ b/src/Inky/Data/Context.idr
@@ -24,13 +24,11 @@ mapNames f (ctx :< nx) = cong (:< nx.name) $ mapNames f ctx
-- Construction ----------------------------------------------------------------
public export
-fromAll : (ctx : Context a) -> All (const b) ctx.names -> Context b
-fromAll [<] [<] = [<]
-fromAll (ctx :< (n :- _)) (sx :< x) = fromAll ctx sx :< (n :- x)
+fromAll : {sx : SnocList String} -> All (Assoc0 a) sx -> Context a
+fromAll [<] = [<]
+fromAll {sx = sx :< n} (ctx :< (_ :- x)) = fromAll ctx :< (n :- x)
export
-fromAllNames :
- (ctx : Context a) -> (sx : All (const b) ctx.names) ->
- (fromAll ctx sx).names = ctx.names
-fromAllNames [<] [<] = Refl
-fromAllNames (ctx :< (n :- _)) (sx :< x) = cong (:< n) $ fromAllNames ctx sx
+fromAllNames : {sx : SnocList String} -> (ctx : All (Assoc0 a) sx) -> (fromAll ctx).names = sx
+fromAllNames [<] = Refl
+fromAllNames {sx = sx :< n} (ctx :< (k :- x)) = cong (:< n) $ fromAllNames ctx
diff --git a/src/Inky/Data/Irrelevant.idr b/src/Inky/Data/Irrelevant.idr
deleted file mode 100644
index ca72470..0000000
--- a/src/Inky/Data/Irrelevant.idr
+++ /dev/null
@@ -1,19 +0,0 @@
-module Inky.Data.Irrelevant
-
-public export
-record Irrelevant (a : Type) where
- constructor Forget
- 0 value : a
-
-public export
-Functor Irrelevant where
- map f x = Forget (f x.value)
-
-public export
-Applicative Irrelevant where
- pure x = Forget x
- f <*> x = Forget (f.value x.value)
-
-public export
-Monad Irrelevant where
- join x = Forget (x.value.value)
diff --git a/src/Inky/Data/Row.idr b/src/Inky/Data/Row.idr
index 05e1fd0..42f18da 100644
--- a/src/Inky/Data/Row.idr
+++ b/src/Inky/Data/Row.idr
@@ -5,7 +5,6 @@ import public Inky.Data.Context
import public Inky.Data.SnocList.Quantifiers
import Inky.Data.SnocList.Elem
-import Inky.Data.Irrelevant
import Inky.Decidable
public export
@@ -77,8 +76,8 @@ snocCong :
snocCong eq1 eq2 = rowCong $ cong2 (\x, y => x.context :< y) eq1 eq2
public export
-fromAll : (row : Row a) -> All (const b) row.names -> Row b
-fromAll row sx = MkRow (fromAll row.context sx) (rewrite fromAllNames row.context sx in row.fresh)
+fromAll : {sx : SnocList String} -> (ctx : All (Assoc0 b) sx) -> (0 fresh : AllFresh sx) -> Row b
+fromAll ctx fresh = MkRow (fromAll ctx) (rewrite fromAllNames ctx in fresh)
-- Interfaces ------------------------------------------------------------------
@@ -114,16 +113,14 @@ export
isFresh :
(names : SnocList String) ->
(name : String) ->
- Dec' (Irrelevant $ name `FreshIn` names)
-isFresh names name =
- map irrelevant (\contra, prfs => anyNegAll contra $ relevant names prfs.value) $
- all (\x => (decSo $ x /= name).forget) names
+ LazyEither (name `FreshIn` names) (Any (\x => So (x == name)) names)
+isFresh names name = all (\x => not (so $ x == name)) names
export
extend : Row a -> Assoc a -> Maybe (Row a)
-extend row x with (isFresh row.names x.name)
- _ | True `Because` Forget prf = Just (row :< x)
- _ | False `Because` _ = Nothing
+extend row x = case (isFresh row.names x.name) of
+ True `Because` prf => Just ((:<) row x @{prf})
+ False `Because` _ => Nothing
-- Search ----------------------------------------------------------------------
diff --git a/src/Inky/Data/SnocList/Quantifiers.idr b/src/Inky/Data/SnocList/Quantifiers.idr
index ac6287b..886c4e4 100644
--- a/src/Inky/Data/SnocList/Quantifiers.idr
+++ b/src/Inky/Data/SnocList/Quantifiers.idr
@@ -3,7 +3,6 @@ module Inky.Data.SnocList.Quantifiers
import public Data.SnocList.Quantifiers
import Data.List.Quantifiers
-import Inky.Data.Irrelevant
import Inky.Data.SnocList
import Inky.Data.SnocList.Elem
import Inky.Decidable
@@ -26,23 +25,15 @@ HSnocList : SnocList Type -> Type
HSnocList = All id
public export
-all : ((x : a) -> Dec' (p x)) -> (sx : SnocList a) -> LazyEither (All p sx) (Any (Not . p) sx)
+all :
+ ((x : a) -> LazyEither (p x) (q x)) ->
+ (sx : SnocList a) -> LazyEither (All p sx) (Any q sx)
all f [<] = True `Because` [<]
all f (sx :< x) =
map (\prfs => snd prfs :< fst prfs) (either Here There) $
both (f x) (all f sx)
public export
-irrelevant : {0 sx : SnocList a} -> All (Irrelevant . p) sx -> Irrelevant (All p sx)
-irrelevant [<] = Forget [<]
-irrelevant (prfs :< px) = [| irrelevant prfs :< px |]
-
-public export
-relevant : (sx : SnocList a) -> (0 prfs : All p sx) -> All (Irrelevant . p) sx
-relevant [<] _ = [<]
-relevant (sx :< x) prfs = relevant sx (tail prfs) :< Forget (head prfs)
-
-public export
tabulate : LengthOf sx -> (forall x. Elem x sx -> p x) -> All p sx
tabulate Z f = [<]
tabulate (S len) f = tabulate len (f . There) :< f Here
diff --git a/src/Inky/Decidable.idr b/src/Inky/Decidable.idr
index 860f9e2..7fba676 100644
--- a/src/Inky/Decidable.idr
+++ b/src/Inky/Decidable.idr
@@ -15,7 +15,6 @@ import Data.These
import Data.Vect
import Decidable.Equality
-import Inky.Data.Irrelevant
public export
When : Type -> Bool -> Type
@@ -39,23 +38,6 @@ toDec : Dec' a -> Dec a
toDec (True `Because` prf) = Yes prf
toDec (False `Because` contra) = No contra
--- So
-
-public export
-decSo : (b : Bool) -> Dec' (So b)
-decSo b = b `Because` (if b then Oh else absurd)
-
--- Irrelevant
-
-public export
-forgetWhen : {b : Bool} -> a `When` b -> Irrelevant a `When` b
-forgetWhen {b = True} prf = Forget prf
-forgetWhen {b = False} contra = \prf => void $ contra $ prf.value
-
-public export
-(.forget) : Dec' a -> Dec' (Irrelevant a)
-p.forget = p.does `Because` forgetWhen p.reason
-
-- Negation
public export
diff --git a/src/Inky/Decidable/Either.idr b/src/Inky/Decidable/Either.idr
index 9da2c72..bea3364 100644
--- a/src/Inky/Decidable/Either.idr
+++ b/src/Inky/Decidable/Either.idr
@@ -1,5 +1,6 @@
module Inky.Decidable.Either
+import Data.So
import Data.These
public export
@@ -88,6 +89,10 @@ public export
any : LazyEither a b -> Lazy (LazyEither c d) -> LazyEither (These a c) (b, d)
any p q = p.does || q.does `Because` Union.any p.reason q.reason
+public export
+so : (b : Bool) -> LazyEither (So b) (So $ not b)
+so b = b `Because` if b then Oh else Oh
+
export autobind infixr 0 >=>
public export
diff --git a/src/Inky/Term.idr b/src/Inky/Term.idr
index 8ae1223..3c5d214 100644
--- a/src/Inky/Term.idr
+++ b/src/Inky/Term.idr
@@ -1,6 +1,5 @@
module Inky.Term
-import public Inky.Data.Thinned
import public Inky.Type
import Data.List.Quantifiers
@@ -64,13 +63,13 @@ export
public export
data IsFunction :
(bound : List String) -> (a : Ty tyCtx) ->
- (dom : All (const $ Ty tyCtx) bound) -> (cod : Ty tyCtx) ->
+ (dom : All (Assoc0 $ Ty tyCtx) bound) -> (cod : Ty tyCtx) ->
Type
where
Done : IsFunction [] a [] a
Step :
IsFunction bound b dom cod ->
- IsFunction (x :: bound) (TArrow a b) (a :: dom) cod
+ IsFunction (x :: bound) (TArrow a b) ((x :- a) :: dom) cod
public export
data NotFunction : (bound : List String) -> (a : Ty tyCtx) -> Type
@@ -96,8 +95,8 @@ export
isFunctionUnique :
IsFunction bound a dom cod -> IsFunction bound a dom' cod' -> (dom = dom', cod = cod')
isFunctionUnique Done Done = (Refl, Refl)
-isFunctionUnique (Step {a} prf) (Step prf') =
- mapFst (\prf => cong (a ::) prf) $ isFunctionUnique prf prf'
+isFunctionUnique (Step {x, a} prf) (Step prf') =
+ mapFst (\prf => cong ((x :- a) ::) prf) $ isFunctionUnique prf prf'
export
isFunctionSplit : IsFunction bound a dom cod -> NotFunction bound a -> Void
@@ -107,13 +106,13 @@ isFunctionSplit (Step prf) (Step2 contra) = isFunctionSplit prf contra
export
isFunction :
(bound : List String) -> (a : Ty tyCtx) ->
- Proof (All (const $ Ty tyCtx) bound, Ty tyCtx)
+ Proof (All (Assoc0 $ Ty tyCtx) bound, Ty tyCtx)
(uncurry $ IsFunction bound a)
(NotFunction bound a)
isFunction [] a = Just ([], a) `Because` Done
isFunction (x :: bound) a =
map
- (\x => (fst (fst x) :: fst (snd x), snd (snd x)))
+ (\y => ((x :- fst (fst y)) :: fst (snd y), snd (snd y)))
(\((a, b), (dom, cod)), (eq, prf) => rewrite eq in Step prf)
(either Step1 false) $
(ab := isArrow a) >=> isFunction bound (snd ab)
@@ -149,20 +148,20 @@ namespace Modes
public export
data Synths :
- All (const $ Thinned Ty [<]) tyCtx ->
- All (const $ Thinned Ty [<]) tmCtx ->
+ All (Assoc0 $ Ty [<]) tyCtx ->
+ All (Assoc0 $ Ty [<]) tmCtx ->
Term mode m tyCtx tmCtx -> Ty [<] -> Type
public export
data Checks :
- All (const $ Thinned Ty [<]) tyCtx ->
- All (const $ Thinned Ty [<]) tmCtx ->
+ All (Assoc0 $ Ty [<]) tyCtx ->
+ All (Assoc0 $ Ty [<]) tmCtx ->
Ty [<] -> Term mode m tyCtx tmCtx -> Type
namespace Spine
public export
data CheckSpine :
- All (const $ Thinned Ty [<]) tyCtx ->
- All (const $ Thinned Ty [<]) tmCtx ->
+ All (Assoc0 $ Ty [<]) tyCtx ->
+ All (Assoc0 $ Ty [<]) tmCtx ->
Ty [<] -> List (Term mode m tyCtx tmCtx) -> Ty [<] -> Type
where
Nil : CheckSpine tyEnv tmEnv a [] a
@@ -176,8 +175,8 @@ namespace Spine
namespace Synths
public export
data AllSynths :
- All (const $ Thinned Ty [<]) tyCtx ->
- All (const $ Thinned Ty [<]) tmCtx ->
+ All (Assoc0 $ Ty [<]) tyCtx ->
+ All (Assoc0 $ Ty [<]) tmCtx ->
Context (Term mode m tyCtx tmCtx) -> Row (Ty [<]) -> Type
where
Lin : AllSynths tyEnv tmEnv [<] [<]
@@ -192,8 +191,8 @@ namespace Synths
namespace Checks
public export
data AllChecks :
- All (const $ Thinned Ty [<]) tyCtx ->
- All (const $ Thinned Ty [<]) tmCtx ->
+ All (Assoc0 $ Ty [<]) tyCtx ->
+ All (Assoc0 $ Ty [<]) tmCtx ->
Context (Ty [<]) -> Context (Term mode m tyCtx tmCtx) -> Type
where
Base : AllChecks tyEnv tmEnv [<] [<]
@@ -208,14 +207,14 @@ namespace Checks
namespace Branches
public export
data AllBranches :
- All (const $ Thinned Ty [<]) tyCtx ->
- All (const $ Thinned Ty [<]) tmCtx ->
+ All (Assoc0 $ Ty [<]) tyCtx ->
+ All (Assoc0 $ Ty [<]) tmCtx ->
Context (Ty [<]) -> Ty [<] -> Context (x ** Term mode m tyCtx (tmCtx :< x)) -> Type
where
Base : AllBranches tyEnv tmEnv [<] a [<]
Step :
(i : Elem (l :- a) as) ->
- Checks tyEnv (tmEnv :< (a `Over` Id)) b t ->
+ Checks tyEnv (tmEnv :< (x :- a)) b t ->
AllBranches tyEnv tmEnv (dropElem as i) b ts ->
AllBranches tyEnv tmEnv as b (ts :< (l :- (x ** t)))
@@ -227,14 +226,14 @@ data Synths where
Checks tyEnv tmEnv (sub tyEnv a) t ->
Synths tyEnv tmEnv (Annot meta t a) (sub tyEnv a)
VarS :
- Synths tyEnv tmEnv (Var meta i) (indexAll i.pos tmEnv).extract
+ Synths tyEnv tmEnv (Var meta i) (indexAll i.pos tmEnv).value
LetS :
Synths tyEnv tmEnv e a ->
- Synths tyEnv (tmEnv :< (a `Over` Id)) f b ->
+ Synths tyEnv (tmEnv :< (x :- a)) f b ->
Synths tyEnv tmEnv (Let meta e (x ** f)) b
LetTyS :
WellFormed a ->
- Synths (tyEnv :< (sub tyEnv a `Over` Id)) tmEnv e b ->
+ Synths (tyEnv :< (x :- sub tyEnv a)) tmEnv e b ->
Synths tyEnv tmEnv (LetTy meta a (x ** e)) b
AppS :
Synths tyEnv tmEnv f a ->
@@ -249,15 +248,15 @@ data Synths where
Synths tyEnv tmEnv (Prj meta e l) a
UnrollS :
Synths tyEnv tmEnv e (TFix x a) ->
- Synths tyEnv tmEnv (Unroll meta e) (sub [<TFix x a `Over` Id] a)
+ Synths tyEnv tmEnv (Unroll meta e) (sub [<x :- TFix x a] a)
MapS :
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)))
+ (TArrow (sub (tyEnv :< (x :- sub tyEnv b)) a)
+ (sub (tyEnv :< (x :- sub tyEnv c)) a)))
data Checks where
AnnotC :
@@ -270,15 +269,15 @@ data Checks where
Checks tyEnv tmEnv b (Var {mode} meta i)
LetC :
Synths tyEnv tmEnv e a ->
- Checks tyEnv (tmEnv :< (a `Over` Id)) b t ->
+ Checks tyEnv (tmEnv :< (x :- a)) b t ->
Checks tyEnv tmEnv b (Let meta e (x ** t))
LetTyC :
WellFormed a ->
- Checks (tyEnv :< (sub tyEnv a `Over` Id)) tmEnv b t ->
+ Checks (tyEnv :< (x :- sub tyEnv a)) tmEnv b t ->
Checks tyEnv tmEnv b (LetTy meta a (x ** t))
AbsC :
IsFunction bound a dom cod ->
- Checks tyEnv (tmEnv <>< mapProperty (`Over` Id) dom) cod t ->
+ Checks tyEnv (tmEnv <>< dom) cod t ->
Checks tyEnv tmEnv a (Abs meta (bound ** t))
AppC :
Synths tyEnv tmEnv (App meta e ts) a ->
@@ -300,7 +299,7 @@ data Checks where
AllBranches tyEnv tmEnv as.context a ts.context ->
Checks tyEnv tmEnv a (Case meta e ts)
RollC :
- Checks tyEnv tmEnv (sub [<TFix x a `Over` Id] a) t ->
+ Checks tyEnv tmEnv (sub [<x :- TFix x a] a) t ->
Checks tyEnv tmEnv (TFix x a) (Roll meta t)
UnrollC :
Synths tyEnv tmEnv (Unroll meta e) a ->
@@ -308,7 +307,7 @@ data Checks where
Checks tyEnv tmEnv b (Unroll meta e)
FoldC :
Synths tyEnv tmEnv e (TFix x a) ->
- Checks tyEnv (tmEnv :< (sub [<b `Over` Id] a `Over` Id)) b t ->
+ Checks tyEnv (tmEnv :< (y :- sub [<x :- b] a)) b t ->
Checks tyEnv tmEnv b (Fold meta e (y ** t))
MapC :
Synths tyEnv tmEnv (Map meta (x ** a) b c) d ->
@@ -334,20 +333,20 @@ EmbedC Map prf1 prf2 = MapC prf1 prf2
public export
data NotSynths :
- All (const $ Thinned Ty [<]) tyCtx ->
- All (const $ Thinned Ty [<]) tmCtx ->
+ All (Assoc0 $ Ty [<]) tyCtx ->
+ All (Assoc0 $ Ty [<]) tmCtx ->
Term mode m tyCtx tmCtx -> Type
public export
data NotChecks :
- All (const $ Thinned Ty [<]) tyCtx ->
- All (const $ Thinned Ty [<]) tmCtx ->
+ All (Assoc0 $ Ty [<]) tyCtx ->
+ All (Assoc0 $ Ty [<]) tmCtx ->
Ty [<] -> Term mode m tyCtx tmCtx -> Type
namespace Spine
public export
data NotCheckSpine :
- All (const $ Thinned Ty [<]) tyCtx ->
- All (const $ Thinned Ty [<]) tmCtx ->
+ All (Assoc0 $ Ty [<]) tyCtx ->
+ All (Assoc0 $ Ty [<]) tmCtx ->
Ty [<] -> List (Term mode m tyCtx tmCtx) -> Type
where
Step1 :
@@ -362,8 +361,8 @@ namespace Spine
namespace Synths
public export
data AnyNotSynths :
- All (const $ Thinned Ty [<]) tyCtx ->
- All (const $ Thinned Ty [<]) tmCtx ->
+ All (Assoc0 $ Ty [<]) tyCtx ->
+ All (Assoc0 $ Ty [<]) tmCtx ->
(ts : Context (Term mode m tyCtx tmCtx)) -> Type
where
Step :
@@ -375,8 +374,8 @@ namespace Synths
namespace Checks
public export
data AnyNotChecks :
- All (const $ Thinned Ty [<]) tyCtx ->
- All (const $ Thinned Ty [<]) tmCtx ->
+ All (Assoc0 $ Ty [<]) tyCtx ->
+ All (Assoc0 $ Ty [<]) tmCtx ->
Context (Ty [<]) -> Context (Term mode m tyCtx tmCtx) -> Type
where
Base1 : AnyNotChecks tyEnv tmEnv (as :< la) [<]
@@ -393,8 +392,8 @@ namespace Checks
namespace Branches
public export
data AnyNotBranches :
- All (const $ Thinned Ty [<]) tyCtx ->
- All (const $ Thinned Ty [<]) tmCtx ->
+ All (Assoc0 $ Ty [<]) tyCtx ->
+ All (Assoc0 $ Ty [<]) tmCtx ->
Context (Ty [<]) -> Ty [<] -> Context (x ** Term mode m tyCtx (tmCtx :< x)) -> Type
where
Base1 : AnyNotBranches tyEnv tmEnv (as :< a) b [<]
@@ -404,7 +403,7 @@ namespace Branches
Step2 :
(i : Elem (l :- a) as) ->
These
- (NotChecks tyEnv (tmEnv :< (a `Over` Id)) b t)
+ (NotChecks tyEnv (tmEnv :< (x :- a)) b t)
(AnyNotBranches tyEnv tmEnv (dropElem as i) b ts) ->
AnyNotBranches tyEnv tmEnv as b (ts :< (l :- (x ** t)))
@@ -422,10 +421,10 @@ data NotSynths where
NotSynths tyEnv tmEnv (Let meta e (x ** f))
LetNS2 :
Synths tyEnv tmEnv e a ->
- NotSynths tyEnv (tmEnv :< (a `Over` Id)) f ->
+ NotSynths tyEnv (tmEnv :< (x :- a)) f ->
NotSynths tyEnv tmEnv (Let meta e (x ** f))
LetTyNS :
- These (IllFormed a) (NotSynths (tyEnv :< (sub tyEnv a `Over` Id)) tmEnv e) ->
+ These (IllFormed a) (NotSynths (tyEnv :< (x :- sub tyEnv a)) tmEnv e) ->
NotSynths tyEnv tmEnv (LetTy meta a (x ** e))
AppNS1 :
NotSynths tyEnv tmEnv f ->
@@ -474,17 +473,17 @@ data NotChecks where
NotChecks tyEnv tmEnv b (Let meta e (x ** t))
LetNC2 :
Synths tyEnv tmEnv e a ->
- NotChecks tyEnv (tmEnv :< (a `Over` Id)) b t ->
+ NotChecks tyEnv (tmEnv :< (x :- a)) b t ->
NotChecks tyEnv tmEnv b (Let meta e (x ** t))
LetTyNC :
- These (IllFormed a) (NotChecks (tyEnv :< (sub tyEnv a `Over` Id)) tmEnv b t) ->
+ These (IllFormed a) (NotChecks (tyEnv :< (x :- sub tyEnv a)) tmEnv b t) ->
NotChecks tyEnv tmEnv b (LetTy meta a (x ** t))
AbsNC1 :
NotFunction bound a ->
NotChecks tyEnv tmEnv a (Abs meta (bound ** t))
AbsNC2 :
IsFunction bound a dom cod ->
- NotChecks tyEnv (tmEnv <>< mapProperty (`Over` Id) dom) cod t ->
+ NotChecks tyEnv (tmEnv <>< dom) cod t ->
NotChecks tyEnv tmEnv a (Abs meta (bound ** t))
TupNC1 :
((as : Row (Ty [<])) -> Not (a = TProd as)) ->
@@ -517,7 +516,7 @@ data NotChecks where
((x : String) -> (b : Ty [<x]) -> Not (a = TFix x b)) ->
NotChecks tyEnv tmEnv a (Roll meta t)
RollNC2 :
- NotChecks tyEnv tmEnv (sub [<TFix x a `Over` Id] a) t ->
+ NotChecks tyEnv tmEnv (sub [<x :- TFix x a] a) t ->
NotChecks tyEnv tmEnv (TFix x a) (Roll meta t)
FoldNC1 :
NotSynths tyEnv tmEnv e ->
@@ -528,7 +527,7 @@ data NotChecks where
NotChecks tyEnv tmEnv b (Fold meta e (y ** t))
FoldNC3 :
Synths tyEnv tmEnv e (TFix x a) ->
- NotChecks tyEnv (tmEnv :< (sub [<b `Over` Id] a `Over` Id)) b t ->
+ NotChecks tyEnv (tmEnv :< (y :- sub [<x :- b] a)) b t ->
NotChecks tyEnv tmEnv b (Fold meta e (y ** t))
%name NotSynths contra
diff --git a/src/Inky/Term/Checks.idr b/src/Inky/Term/Checks.idr
index 8ddcd8d..6027d68 100644
--- a/src/Inky/Term/Checks.idr
+++ b/src/Inky/Term/Checks.idr
@@ -69,7 +69,7 @@ synthsUnique (PrjS {as} prf i) (PrjS {as = bs} prf' j) =
let j = rewrite inj TProd $ synthsUnique prf prf' in j in
cong fst $ lookupUnique as i j
synthsUnique (UnrollS {x, a} prf) (UnrollS {x = y, a = b} prf') =
- cong (\(x ** a) => sub [<TFix x a `Over` Id] a) $
+ cong (\(x ** a) => sub [<x :- TFix x a] a) $
fixInjective $
synthsUnique prf prf'
synthsUnique (MapS _ _ _) (MapS _ _ _) = Refl
@@ -176,11 +176,11 @@ checksSplit (RollC prf) (RollNC2 contra) = checksSplit prf contra
checksSplit (FoldC prf1 prf2) (FoldNC1 contra) = synthsSplit prf1 contra
checksSplit (FoldC {x, a} prf1 prf2) (FoldNC2 prf1' contra) =
void $ contra x a $ synthsUnique prf1' prf1
-checksSplit (FoldC {t, b} prf1 prf2) (FoldNC3 prf1' contra) =
+checksSplit (FoldC {y, t, b} prf1 prf2) (FoldNC3 prf1' contra) =
let
contra =
replace
- {p = \(x ** a) => NotChecks tyEnv (tmEnv :< (sub [<b `Over` Id] a `Over` Id)) b t}
+ {p = \(x ** a) => NotChecks tyEnv (tmEnv :< (y :- sub [<x :- b] a)) b t}
(fixInjective $ synthsUnique prf1' prf1)
contra
in
@@ -212,7 +212,7 @@ allBranchesSplit fresh (Step {as, b, x, t, ts} i prf prfs) (Step2 j contras) =
replace
{p = \(a ** i) =>
These
- (NotChecks tyEnv (tmEnv :< (a `Over` Id)) b t)
+ (NotChecks tyEnv (tmEnv :< (x :- a)) b t)
(AnyNotBranches tyEnv tmEnv (dropElem as i) b ts)}
(lookupUnique (MkRow as fresh) j i)
contras
@@ -234,37 +234,37 @@ fallbackCheck prf p a =
(b := p) >=> alpha b a
synths :
- (tyEnv : All (const $ Thinned Ty [<]) tyCtx) ->
- (tmEnv : All (const $ Thinned Ty [<]) tmCtx) ->
+ (tyEnv : All (Assoc0 $ Ty [<]) tyCtx) ->
+ (tmEnv : All (Assoc0 $ Ty [<]) tmCtx) ->
(e : Term mode m tyCtx tmCtx) ->
Proof (Ty [<]) (Synths tyEnv tmEnv e) (NotSynths tyEnv tmEnv e)
export
checks :
- (tyEnv : All (const $ Thinned Ty [<]) tyCtx) ->
- (tmEnv : All (const $ Thinned Ty [<]) tmCtx) ->
+ (tyEnv : All (Assoc0 $ Ty [<]) tyCtx) ->
+ (tmEnv : All (Assoc0 $ Ty [<]) tmCtx) ->
(a : Ty [<]) -> (t : Term mode m tyCtx tmCtx) ->
LazyEither (Checks tyEnv tmEnv a t) (NotChecks tyEnv tmEnv a t)
checkSpine :
- (tyEnv : All (const $ Thinned Ty [<]) tyCtx) ->
- (tmEnv : All (const $ Thinned Ty [<]) tmCtx) ->
+ (tyEnv : All (Assoc0 $ Ty [<]) tyCtx) ->
+ (tmEnv : All (Assoc0 $ Ty [<]) tmCtx) ->
(a : Ty [<]) -> (ts : List (Term mode m tyCtx tmCtx)) ->
Proof (Ty [<]) (CheckSpine tyEnv tmEnv a ts) (NotCheckSpine tyEnv tmEnv a ts)
allSynths :
- (tyEnv : All (const $ Thinned Ty [<]) tyCtx) ->
- (tmEnv : All (const $ Thinned Ty [<]) tmCtx) ->
+ (tyEnv : All (Assoc0 $ Ty [<]) tyCtx) ->
+ (tmEnv : All (Assoc0 $ Ty [<]) tmCtx) ->
(es : Context (Term mode m tyCtx tmCtx)) ->
(0 fresh : AllFresh es.names) ->
Proof (Subset (Row (Ty [<])) (\as => es.names = as.names))
(AllSynths tyEnv tmEnv es . Subset.fst)
(AnyNotSynths tyEnv tmEnv es)
allChecks :
- (tyEnv : All (const $ Thinned Ty [<]) tyCtx) ->
- (tmEnv : All (const $ Thinned Ty [<]) tmCtx) ->
+ (tyEnv : All (Assoc0 $ Ty [<]) tyCtx) ->
+ (tmEnv : All (Assoc0 $ Ty [<]) tmCtx) ->
(as : Context (Ty [<])) -> (ts : Context (Term mode m tyCtx tmCtx)) ->
LazyEither (AllChecks tyEnv tmEnv as ts) (AnyNotChecks tyEnv tmEnv as ts)
allBranches :
- (tyEnv : All (const $ Thinned Ty [<]) tyCtx) ->
- (tmEnv : All (const $ Thinned Ty [<]) tmCtx) ->
+ (tyEnv : All (Assoc0 $ Ty [<]) tyCtx) ->
+ (tmEnv : All (Assoc0 $ Ty [<]) tmCtx) ->
(as : Context (Ty [<])) -> (a : Ty [<]) -> (ts : Context (x ** Term mode m tyCtx (tmCtx :< x))) ->
LazyEither (AllBranches tyEnv tmEnv as a ts) (AnyNotBranches tyEnv tmEnv as a ts)
@@ -272,15 +272,15 @@ synths tyEnv tmEnv (Annot _ t a) =
pure (sub tyEnv a) $
map (uncurry AnnotS) AnnotNS $
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 (Var _ i) = Just (indexAll i.pos tmEnv).value `Because` VarS
synths tyEnv tmEnv (Let _ e (x ** f)) =
map snd
(\(_, _), (prf1, prf2) => LetS prf1 prf2)
(either LetNS1 (\xPrfs => uncurry LetNS2 (snd xPrfs))) $
- (a := synths tyEnv tmEnv e) >=> synths tyEnv (tmEnv :< (a `Over` Id)) f
+ (a := synths tyEnv tmEnv e) >=> synths tyEnv (tmEnv :< (x :- a)) f
synths tyEnv tmEnv (LetTy _ a (x ** e)) =
map id (\_, (wf, prf) => LetTyS wf prf) LetTyNS $
- all (wellFormed a) (synths (tyEnv :< (sub tyEnv a `Over` Id)) tmEnv e)
+ all (wellFormed a) (synths (tyEnv :< (x :- sub tyEnv a)) tmEnv e)
synths tyEnv tmEnv (Abs _ (bound ** t)) = Nothing `Because` ChecksNS Abs
synths tyEnv tmEnv (App _ e ts) =
map snd
@@ -321,7 +321,7 @@ synths tyEnv tmEnv (Unroll _ e) =
synths tyEnv tmEnv e `andThen` isFix
where
f : (Ty [<], (x ** Ty [<x])) -> Ty [<]
- f (a, (x ** b)) = sub [<TFix x b `Over` Id] b
+ f (a, (x ** b)) = sub [<x :- TFix x b] b
true :
(axb : _) ->
@@ -348,19 +348,19 @@ checks tyEnv tmEnv a (Let _ e (x ** t)) =
map
(\(_ ** (prf1, prf2)) => LetC prf1 prf2)
(either LetNC1 (\xPrfs => uncurry LetNC2 $ snd xPrfs)) $
- (b := synths tyEnv tmEnv e) >=> checks tyEnv (tmEnv :< (b `Over` Id)) a t
+ (b := synths tyEnv tmEnv e) >=> checks tyEnv (tmEnv :< (x :- b)) a t
checks tyEnv tmEnv a (LetTy _ b (x ** t)) =
map (uncurry LetTyC) LetTyNC $
- all (wellFormed b) (checks (tyEnv :< (sub tyEnv b `Over` Id)) tmEnv a t)
+ all (wellFormed b) (checks (tyEnv :< (x :- sub tyEnv b)) tmEnv a t)
checks tyEnv tmEnv a (Abs meta (bound ** t)) =
map
(\((_, _) ** (prf1, prf2)) => AbsC prf1 prf2)
(either AbsNC1 false) $
(domCod := isFunction bound a) >=>
- checks tyEnv (tmEnv <>< mapProperty (`Over` Id) (fst domCod)) (snd domCod) t
+ checks tyEnv (tmEnv <>< fst domCod) (snd domCod) t
where
false :
- (x ** (Prelude.uncurry (IsFunction bound a) x, NotChecks tyEnv (tmEnv <>< mapProperty (`Over` Id) (fst x)) (snd x) t)) ->
+ (x ** (Prelude.uncurry (IsFunction bound a) x, NotChecks tyEnv (tmEnv <>< fst x) (snd x) t)) ->
NotChecks tyEnv tmEnv a (Abs meta (bound ** t))
false ((_,_) ** prf) = uncurry AbsNC2 prf
checks tyEnv tmEnv a (App meta f ts) = fallbackCheck App (synths tyEnv tmEnv $ App meta f ts) a
@@ -436,7 +436,7 @@ checks tyEnv tmEnv a (Roll _ t) =
(xb := isFix a) >=> checks tyEnv tmEnv (ty xb) t
where
ty : (x ** Ty [<x]) -> Ty [<]
- ty (x ** b) = sub [<TFix x b `Over` Id] b
+ ty (x ** b) = sub [<x :- TFix x b] b
true :
forall a.
@@ -459,8 +459,8 @@ checks tyEnv tmEnv a (Fold _ e (x ** t)) =
(yc := isFix b) >=>
checks tyEnv (tmEnv' yc) a t
where
- tmEnv' : (y ** Ty [<y]) -> All (const $ Thinned Ty [<]) (tmCtx :< x)
- tmEnv' (y ** c) = tmEnv :< (sub [<a `Over` Id] c `Over` Id)
+ tmEnv' : (y ** Ty [<y]) -> All (Assoc0 $ Ty [<]) (tmCtx :< x)
+ tmEnv' (y ** c) = tmEnv :< (x :- sub [<y :- a] c)
true :
(b ** (Synths tyEnv tmEnv e b,
@@ -534,5 +534,5 @@ allBranches tyEnv tmEnv as b (ts :< (l :- (x ** t))) =
(either Step1 (\xPrf => Step2 (snd $ fst xPrf) (snd xPrf))) $
(ai := (decLookup l as).forget) >=>
all
- (checks tyEnv (tmEnv :< (fst ai `Over` Id)) b t)
+ (checks tyEnv (tmEnv :< (x :- fst ai)) b t)
(allBranches tyEnv tmEnv (dropElem as $ snd ai) b ts)
diff --git a/src/Inky/Term/Desugar.idr b/src/Inky/Term/Desugar.idr
index 50676ce..1ce0e41 100644
--- a/src/Inky/Term/Desugar.idr
+++ b/src/Inky/Term/Desugar.idr
@@ -80,89 +80,6 @@ desugarMapCaseNames [<] [<] i [<] f = Refl
desugarMapCaseNames (as :< (l :- a)) (fresh :< freshIn) i (prfs :< prf) f =
cong (:< l) $ desugarMapCaseNames as fresh i prfs f
--- -- Well Formed
-
--- desugarMapChecks :
--- (0 meta : m) =>
--- (a : Ty (tyCtx :< arg ++ bound)) -> (len : LengthOf bound) ->
--- (0 prf : index (dropAll len) (toVar {sx = tyCtx :< arg} Here) `StrictlyPositiveIn` a) ->
--- {env1 : All (const $ Thinned Ty [<]) tyCtx} ->
--- {env2 : All (const $ Thinned Ty [<]) bound} ->
--- {b, c : Ty [<]} ->
--- Synths tyEnv tmEnv f (TArrow b c) ->
--- Synths tyEnv tmEnv t (sub (((:<) {x = arg} env1 (b `Over` Id)) ++ env2) a) ->
--- SynthsOnly t ->
--- Checks tyEnv tmEnv
--- (sub (((:<) {x = arg} env1 (c `Over` Id)) ++ env2) a)
--- (desugarMap {m} a (index (dropAll len) (toVar {sx = tyCtx :< arg} Here)) prf f t)
--- desugarMapTupleChecks :
--- (0 meta : m) =>
--- (as : Context (Ty (tyCtx :< arg ++ bound))) -> (len' : LengthOf bs) ->
--- (0 fresh' : AllFresh (as <>< bs).names) ->
--- (0 fresh : AllFresh as.names) ->
--- (len : LengthOf bound) ->
--- (0 prfs : index (dropAll len) (toVar {sx = tyCtx :< arg} Here) `StrictlyPositiveInAll` as) ->
--- {env1 : All (const $ Thinned Ty [<]) tyCtx} ->
--- {env2 : All (const $ Thinned Ty [<]) bound} ->
--- {b, c : Ty [<]} ->
--- Synths tyEnv tmEnv f (TArrow b c) ->
--- Synths tyEnv tmEnv t
--- (sub (((:<) {x = arg} env1 (b `Over` Id)) ++ env2) (TProd (MkRow (as <>< bs) fresh'))) ->
--- SynthsOnly t ->
--- AllChecks tyEnv tmEnv
--- (subAll (((:<) {x = arg} env1 (c `Over` Id)) ++ env2) as)
--- (desugarMapTuple {m} as fresh (index (dropAll len) (toVar {sx = tyCtx :< arg} Here)) prfs f t).context
--- desugarMapCaseBranches :
--- (0 meta : m) =>
--- (as : Context (Ty (tyCtx :< arg ++ bound))) -> (len' : LengthOf bs) ->
--- (0 fresh' : AllFresh (as <>< bs).names) ->
--- (0 fresh : AllFresh as.names) ->
--- (len : LengthOf bound) ->
--- (0 prfs : index (dropAll len) (toVar {sx = tyCtx :< arg} Here) `StrictlyPositiveInAll` as) ->
--- {env1 : All (const $ Thinned Ty [<]) tyCtx} ->
--- {env2 : All (const $ Thinned Ty [<]) bound} ->
--- {b, c : Ty [<]} ->
--- Synths tyEnv tmEnv f (TArrow b c) ->
--- AllBranches tyEnv tmEnv
--- (subAll (((:<) {x = arg} env1 (b `Over` Id)) ++ env2) as)
--- (sub (((:<) {x = arg} env1 (c `Over` Id)) ++ env2) (TSum (MkRow (as <>< bs) fresh')))
--- (desugarMapCase {m} as fresh (index (dropAll len) (toVar {sx = tyCtx :< arg} Here)) prfs f).context
-
--- desugarMapChecks (TVar j) len TVar fun arg argSynOnly
--- with (index (dropAll len) (toVar Here) `decEq` j)
--- desugarMapChecks (TVar _) len TVar fun arg argSynOnly | True `Because` Refl =
--- EmbedC App (AppS fun [EmbedC argSynOnly arg $ alphaSym $ alphaRefl b _ $ ?b]) ?c
--- _ | False `Because` neq =
--- EmbedC argSynOnly arg $ alphaSym $ alphaRefl _ _ ?a
--- desugarMapChecks (TArrow a b) len (TArrow prf) fun arg argSynOnly =
--- EmbedC argSynOnly arg $ ?dmc_2
--- desugarMapChecks (TProd (MkRow as fresh)) len (TProd prfs) fun arg argSynOnly =
--- TupC (desugarMapTupleChecks as Z fresh fresh len prfs fun arg argSynOnly)
--- desugarMapChecks (TSum (MkRow as fresh)) len (TSum prfs) fun arg argSynOnly =
--- CaseC arg (desugarMapCaseBranches as Z fresh fresh len prfs fun)
--- desugarMapChecks (TFix x a) len (TFix prf) fun arg' argSynOnly =
--- let
--- x =
--- -- FoldC arg' (RollC $
--- desugarMapChecks
--- { m
--- , meta
--- , tyCtx
--- , arg
--- , bound = bound :< x
--- , env1
--- , env2 = env2 :< ?dmc_90
--- , b
--- , c
--- , tyEnv
--- , tmEnv = tmEnv :< (?dmc_92 `Over` Id)
--- , f = thin (Drop Id) f
--- , t = Var meta ((%%) "_eta" {pos = Here})
--- }
--- a (S len) prf ?x ?y ?z
--- -- Need assoc. of subst
--- in FoldC arg' (RollC ?dmc_99)
-
-- Desugar Terms ---------------------------------------------------------------
desugarSynths :
@@ -225,8 +142,8 @@ desugarSynths (MapS {meta, x, a, b, c} (TFix prf1 wf1) wf2 wf3) =
(Abs meta
(["_fun", "_arg"] ** desugarMap a (%% x) prf1 (Var meta (%% "_fun")) (Var meta (%% "_arg"))))
(TArrow (TArrow (TArrow b c)
- (sub (tabulate len ((`Over` Id) . TVar . toVar) :< (b `Over` Id)) a))
- (sub (tabulate len ((`Over` Id) . TVar . toVar) :< (c `Over` Id)) a))
+ (sub (tabulate len (\i => _ :- TVar (toVar i)) :< (x :- b)) a))
+ (sub (tabulate len (\i => _ :- TVar (toVar i)) :< (x :- c)) a))
desugarChecks (AnnotC prf1 prf2) = desugarSynths prf1
desugarChecks (VarC prf1 prf2) = desugarSynths prf1
@@ -277,11 +194,11 @@ maybeDesugarList :
maybeDesugarAll :
(len : LengthOf tyCtx) =>
(ts : Context (Term Sugar m tyCtx tmCtx)) ->
- Maybe (All (const $ Term NoSugar m tyCtx tmCtx) ts.names)
+ Maybe (All (Assoc0 $ Term NoSugar m tyCtx tmCtx) ts.names)
maybeDesugarBranches :
(len : LengthOf tyCtx) =>
(ts : Context (x ** Term Sugar m tyCtx (tmCtx :< x))) ->
- Maybe (All (const $ (x ** Term NoSugar m tyCtx (tmCtx :< x))) ts.names)
+ Maybe (All (Assoc0 $ (x ** Term NoSugar m tyCtx (tmCtx :< x))) ts.names)
maybeDesugar (Annot meta t a) = do
t <- maybeDesugar t
@@ -302,8 +219,8 @@ maybeDesugar (App meta e ts) = do
ts <- maybeDesugarList ts
pure (App meta e ts)
maybeDesugar (Tup meta (MkRow ts fresh)) = do
- ts' <- maybeDesugarAll ts
- pure (Tup meta (fromAll (MkRow ts fresh) ts'))
+ ts <- maybeDesugarAll ts
+ pure (Tup meta (fromAll ts fresh))
maybeDesugar (Prj meta e l) = do
e <- maybeDesugar e
pure (Prj meta e l)
@@ -312,8 +229,8 @@ maybeDesugar (Inj meta l t) = do
pure (Inj meta l t)
maybeDesugar (Case meta e (MkRow ts fresh)) = do
e <- maybeDesugar e
- ts' <- maybeDesugarBranches ts
- pure (Case meta e (fromAll (MkRow ts fresh) ts'))
+ ts <- maybeDesugarBranches ts
+ pure (Case meta e (fromAll ts fresh))
maybeDesugar (Roll meta t) = do
t <- maybeDesugar t
pure (Roll meta t)
@@ -333,17 +250,20 @@ maybeDesugar (Map meta (x ** a) b c) =
(Abs meta
(["_fun", "_arg"] ** desugarMap a (%% x) prf (Var meta (%% "_fun")) (Var meta (%% "_arg"))))
(TArrow (TArrow (TArrow b c)
- (sub (tabulate len ((`Over` Id) . TVar . toVar) :< (b `Over` Id)) a))
- (sub (tabulate len ((`Over` Id) . TVar . toVar) :< (c `Over` Id)) a))
+ (sub (tabulate len (\i => _ :- TVar (toVar i)) :< (x :- b)) a))
+ (sub (tabulate len (\i => _ :- TVar (toVar i)) :< (x :- c)) a))
maybeDesugarList [] = pure []
maybeDesugarList (t :: ts) = [| maybeDesugar t :: maybeDesugarList ts |]
maybeDesugarAll [<] = pure [<]
-maybeDesugarAll (ts :< (l :- t)) = [| maybeDesugarAll ts :< maybeDesugar t |]
+maybeDesugarAll (ts :< (l :- t)) = do
+ ts <- maybeDesugarAll ts
+ t <- maybeDesugar t
+ pure (ts :< (l :- t))
maybeDesugarBranches [<] = pure [<]
maybeDesugarBranches (ts :< (l :- (x ** t))) = do
ts <- maybeDesugarBranches ts
t <- maybeDesugar t
- pure (ts :< (x ** t))
+ pure (ts :< (l :- (x ** t)))
diff --git a/src/Inky/Term/Substitution.idr b/src/Inky/Term/Substitution.idr
index 791014b..690e38c 100644
--- a/src/Inky/Term/Substitution.idr
+++ b/src/Inky/Term/Substitution.idr
@@ -110,24 +110,24 @@ thinTyBranchesNames f (ts :< (l :- (x ** t))) = cong (:< l) $ thinTyBranchesName
public export
Env : Mode -> Type -> SnocList String -> SnocList String -> SnocList String -> Type
-Env mode m tyCtx ctx1 ctx2 = All (const $ Either (Var ctx2) (Term mode m tyCtx ctx2)) ctx1
+Env mode m tyCtx ctx1 ctx2 = All (Assoc0 $ Either (Var ctx2) (Term mode m tyCtx ctx2)) ctx1
public export
Env' : Mode -> Type -> SnocList String -> List String -> SnocList String -> Type
-Env' mode m tyCtx ctx1 ctx2 = All (const $ Either (Var ctx2) (Term mode m tyCtx ctx2)) ctx1
+Env' mode m tyCtx ctx1 ctx2 = All (Assoc0 $ Either (Var ctx2) (Term mode m tyCtx ctx2)) ctx1
public export
thinEnv :
ctx2 `Thins` ctx3 ->
Env mode m tyCtx ctx1 ctx2 ->
Env mode m tyCtx ctx1 ctx3
-thinEnv f = mapProperty (bimap (index f) (thin $ f))
+thinEnv f = mapProperty (map $ bimap (index f) (thin $ f))
public export
lift :
Env mode m tyCtx ctx1 ctx2 ->
Env mode m tyCtx (ctx1 :< x) (ctx2 :< x)
-lift f = thinEnv (Drop Id) f :< Left (%% x)
+lift f = thinEnv (Drop Id) f :< (x :- Left (%% x))
public export
sub :
@@ -160,12 +160,12 @@ keepBound :
forall ctx. {0 bound : List String} ->
LengthOf bound -> Env' mode m tyCtx bound (ctx <>< bound)
keepBound Z = []
-keepBound (S len) = Left (index (dropFish Id len) (toVar Here)) :: keepBound len
+keepBound (S len) = (_ :- Left (index (dropFish Id len) (toVar Here))) :: keepBound len
sub f (Annot meta t a) = Annot meta (sub f t) a
-sub f (Var meta i) = either (Var meta) id $ indexAll i.pos f
+sub f (Var meta i) = either (Var meta) id (indexAll i.pos f).value
sub f (Let meta e (x ** t)) = Let meta (sub f e) (x ** sub (lift f) t)
-sub f (LetTy meta a (x ** t)) = LetTy meta a (x ** sub (mapProperty (map $ thinTy (Drop Id)) f) t)
+sub f (LetTy meta a (x ** t)) = LetTy meta a (x ** sub (mapProperty (map $ map $ thinTy (Drop Id)) f) t)
sub f (Abs meta (bound ** t)) =
let len = lengthOf bound in
Abs meta (bound ** sub (thinEnv (dropFish Id len) f <>< keepBound len) t)
diff --git a/src/Inky/Type.idr b/src/Inky/Type.idr
index 72388b6..8c46328 100644
--- a/src/Inky/Type.idr
+++ b/src/Inky/Type.idr
@@ -3,13 +3,13 @@ module Inky.Type
import public Inky.Data.Context.Var
import public Inky.Data.Row
import public Inky.Data.SnocList.Var
+import public Inky.Data.Thinned
import Control.Function
import Data.DPair
import Data.These
import Inky.Data.SnocList.Thinning
-import Inky.Data.Thinned
import Inky.Decidable
import Inky.Decidable.Maybe
@@ -522,24 +522,24 @@ namespace Strengthen
public export
data StrengthenAll :
(i : Var ctx) -> (as : Context (Ty ctx)) ->
- All (const $ Ty $ dropElem ctx i.pos) as.names -> Type
+ All (Assoc0 $ 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)
+ TProd : StrengthenAll i as.context bs -> Strengthen i (TProd as) (TProd $ fromAll bs as.fresh)
+ TSum : StrengthenAll i as.context bs -> Strengthen i (TSum as) (TSum $ fromAll bs as.fresh)
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)
+ (:<) : StrengthenAll i as bs -> Strengthen i a b -> StrengthenAll i (as :< (l :- a)) (bs :< (l :- 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)
+strengthenAllEq : StrengthenAll i as bs -> as = thinAll (dropPos i.pos) (fromAll bs)
strengthenEq (TVar prf) = cong TVar prf
strengthenEq (TArrow prf1 prf2) = cong2 TArrow (strengthenEq prf1) (strengthenEq prf2)
@@ -602,7 +602,7 @@ strengthen :
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)
+ Proof (All (Assoc0 $ Ty $ dropElem ctx i.pos) as.names) (StrengthenAll i as) (i `OccursInAny` as)
strengthen ((%%) x {pos = i}) (TVar ((%%) y {pos = j})) =
map (TVar . toVar)
@@ -613,10 +613,10 @@ 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 $
+ map (\bs => TProd $ fromAll bs fresh) (\_ => TProd) TProd $
strengthenAll i as
strengthen i (TSum (MkRow as fresh)) =
- map (TSum . fromAll (MkRow as fresh)) (\_ => TSum) TSum $
+ map (\bs => TSum $ fromAll bs fresh) (\_ => TSum) TSum $
strengthenAll i as
strengthen i (TFix x a) =
map (TFix x) (\_ => TFix) TFix $
@@ -624,7 +624,7 @@ strengthen i (TFix x a) =
strengthenAll i [<] = Just [<] `Because` [<]
strengthenAll i (as :< (l :- a)) =
- map (uncurry (:<) . swap) (\(_, _) => uncurry (:<) . swap) (And . swap) $
+ map (\x => snd x :< (l :- fst x)) (\(_, _) => uncurry (:<) . swap) (And . swap) $
all (strengthen i a) (strengthenAll i as)
-- Not Strictly Positive -----------------------------------------------------------
@@ -800,27 +800,32 @@ allWellFormed (as :< (n :- a)) =
--------------------------------------------------------------------------------
public export
-sub : All (const $ Thinned Ty ctx2) ctx1 -> Ty ctx1 -> Ty ctx2
+sub' : All (Assoc0 $ Thinned Ty ctx2) ctx1 -> Ty ctx1 -> Ty ctx2
public export
-subAll : All (const $ Thinned Ty ctx2) ctx1 -> Context (Ty ctx1) -> Context (Ty ctx2)
+subAll : All (Assoc0 $ Thinned Ty ctx2) ctx1 -> Context (Ty ctx1) -> Context (Ty ctx2)
public export
subAllNames :
- (f : All (const $ Thinned Ty ctx2) ctx1) ->
+ (f : All (Assoc0 $ 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 (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)
+sub' env (TVar i) = (indexAll i.pos env).value.extract
+sub' env (TArrow a b) = TArrow (sub' env a) (sub' env b)
+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 (map $ rename $ Drop Id) env :< (x :- (TVar (%% x) `Over` Id))) a)
subAll env [<] = [<]
-subAll env (as :< (n :- a)) = subAll env as :< (n :- sub env a)
+subAll env (as :< (n :- a)) = subAll env as :< (n :- sub' env a)
subAllNames env [<] = Refl
subAllNames env (as :< (n :- a)) = cong (:< n) (subAllNames env as)
+public export
+sub : All (Assoc0 $ Ty ctx2) ctx1 -> Ty ctx1 -> Ty ctx2
+sub = sub' . mapProperty (map $ (`Over` Id))
+
-- Special Types ---------------------------------------------------------------
public export
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-30 07:26:54 +0000