summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--inky.ipkg5
-rw-r--r--src/Inky.idr27
-rw-r--r--src/Inky/Data/List.idr13
-rw-r--r--src/Inky/Data/Row.idr51
-rw-r--r--src/Inky/Data/SnocList/Elem.idr6
-rw-r--r--src/Inky/Data/SnocList/Quantifiers.idr7
-rw-r--r--src/Inky/Data/SnocList/Thinning.idr11
-rw-r--r--src/Inky/Term.idr668
-rw-r--r--src/Inky/Term/Checks.idr538
-rw-r--r--src/Inky/Term/Desugar.idr349
-rw-r--r--src/Inky/Term/Parser.idr27
-rw-r--r--src/Inky/Term/Pretty.idr237
-rw-r--r--src/Inky/Term/Pretty/Error.idr218
-rw-r--r--src/Inky/Term/Substitution.idr197
-rw-r--r--src/Inky/Type.idr64
15 files changed, 1565 insertions, 853 deletions
diff --git a/inky.ipkg b/inky.ipkg
index 43010e3..ec81709 100644
--- a/inky.ipkg
+++ b/inky.ipkg
@@ -16,6 +16,7 @@ modules
, Inky.Data.Context.Var
, Inky.Data.Fun
, Inky.Data.Irrelevant
+ , Inky.Data.List
, Inky.Data.Row
, Inky.Data.SnocList
, Inky.Data.SnocList.Elem
@@ -28,7 +29,11 @@ modules
, Inky.Decidable.Maybe
, Inky.Parser
, Inky.Term
+ , Inky.Term.Checks
+ , Inky.Term.Desugar
, Inky.Term.Parser
, Inky.Term.Pretty
+ , Inky.Term.Pretty.Error
+ , Inky.Term.Substitution
, Inky.Type
, Inky.Type.Pretty
diff --git a/src/Inky.idr b/src/Inky.idr
index 0c4db56..649c620 100644
--- a/src/Inky.idr
+++ b/src/Inky.idr
@@ -10,8 +10,11 @@ import Inky.Decidable
import Inky.Decidable.Maybe
import Inky.Parser
import Inky.Term
+import Inky.Term.Checks
+import Inky.Term.Desugar
import Inky.Term.Parser
import Inky.Term.Pretty
+import Inky.Term.Pretty.Error
import Inky.Type.Pretty
import System.File.Mode
@@ -43,7 +46,7 @@ parseType toks = do
| Left msg => throw msg
pure a
-parseTerm : HasErr String es => List (WithBounds InkyToken) -> App es (Term Bounds [<] [<])
+parseTerm : HasErr String es => List (WithBounds InkyToken) -> App es (Term Sugar Bounds [<] [<])
parseTerm toks = do
let Ok res [] _ = parse @{EqI} OpenTerm toks
| Ok res (x :: _) _ => throw "\{x.bounds}: unexpected token \{x.val.kind}, expected end of input"
@@ -58,7 +61,7 @@ checkType a = do
| False `Because` bad => throw "type ill-formed"
pure ()
-checkTerm : (a : Ty [<]) -> (t : Term m [<] [<]) -> HasErr (NotChecks [<] [<] a t) es => App es ()
+checkTerm : (a : Ty [<]) -> (t : Term mode m [<] [<]) -> HasErr (NotChecks [<] [<] a t) es => App es ()
checkTerm a t = do
let True `Because` prf = checks [<] [<] a t
| False `Because` contra => throw contra
@@ -72,13 +75,13 @@ printType a = do
printTerm :
PrimIO es => {default defaultLayoutOptions opts : LayoutOptions} ->
- Term m [<] [<] -> App es ()
+ Term mode m [<] [<] -> App es ()
printTerm a = do
primIO $ renderIO $ layoutSmart opts $ prettyTerm a Open
printCheckError :
PrimIO es => {default defaultLayoutOptions opts : LayoutOptions} ->
- {a : Ty [<]} -> {t : Term Bounds [<] [<]} ->
+ {a : Ty [<]} -> {t : Term mode Bounds [<] [<]} ->
NotChecks [<] [<] a t -> App es ()
printCheckError contra =
primIO $ renderIO $ layoutSmart opts $
@@ -118,7 +121,12 @@ Inky = MkCommand
"""
, subcommands =
[ "type" ::= basic "print a type" filePath
- , "term" ::= basic "print a term" filePath
+ , "term" ::= MkCommand
+ { description = "print a term"
+ , subcommands = []
+ , modifiers = ["--desugar" ::= flag "desugar the term"]
+ , arguments = filePath
+ }
]
, modifiers = []
, arguments = none
@@ -187,8 +195,13 @@ main = run {l = MayThrow} $ do
txt <- handle {err = IOError} (readFileOrStdin path) pure (abortErr . show)
toks <- handle {err = String} (lexInkyString txt) pure abortErr
t <- handle {err = String} (parseTerm toks) pure abortErr
- printTerm t
- pure ()
+ let [noSugar] = cmd.modifiers.content
+ case noSugar of
+ True => do
+ let Just t = maybeDesugar t
+ | Nothing => abortErr "failed to desugar term"
+ printTerm t
+ False => printTerm t
]
]
, "check" ::=
diff --git a/src/Inky/Data/List.idr b/src/Inky/Data/List.idr
new file mode 100644
index 0000000..24cb9c0
--- /dev/null
+++ b/src/Inky/Data/List.idr
@@ -0,0 +1,13 @@
+module Inky.Data.List
+
+public export
+data LengthOf : List a -> Type where
+ Z : LengthOf []
+ S : LengthOf xs -> LengthOf (x :: xs)
+
+%name LengthOf len
+
+public export
+lengthOf : (xs : List a) -> LengthOf xs
+lengthOf [] = Z
+lengthOf (x :: xs) = S (lengthOf xs)
diff --git a/src/Inky/Data/Row.idr b/src/Inky/Data/Row.idr
index ba0c5f6..05e1fd0 100644
--- a/src/Inky/Data/Row.idr
+++ b/src/Inky/Data/Row.idr
@@ -28,20 +28,6 @@ public export
(.names) : Row a -> SnocList String
row.names = row.context.names
--- Interfaces ------------------------------------------------------------------
-
-public export
-Functor Row where
- map f row = MkRow (map (map f) row.context) (rewrite mapNames f row.context in row.fresh)
-
-public export
-Foldable Row where
- foldr f x row = foldr (\x, y => f x.value y) x row.context
- foldl f x row = foldl (\x, y => f x y.value) x row.context
- null row = null row.context
- foldlM f x row = foldlM (\x, y => f x y.value) x row.context
- foldMap f row = foldMap (f . value) row.context
-
-- Equality --------------------------------------------------------------------
export
@@ -81,10 +67,47 @@ public export
Row a
row :< x = MkRow (row.context :< x) (row.fresh :< fresh)
+export
+snocCong :
+ {0 x, y : Assoc a} ->
+ row1 = row2 -> x = y ->
+ {0 fresh1 : x.name `FreshIn` row1.names} ->
+ {0 fresh2 : y.name `FreshIn` row2.names} ->
+ (:<) row1 x @{fresh1} = (:<) row2 y @{fresh2}
+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)
+-- Interfaces ------------------------------------------------------------------
+
+public export
+mapRow : (a -> b) -> (ctx : Context a) -> (0 fresh : AllFresh ctx.names) -> Row b
+export
+mapRowNames :
+ (0 f : a -> b) -> (ctx : Context a) -> (0 fresh : AllFresh ctx.names) ->
+ (mapRow f ctx fresh).names = ctx.names
+
+mapRow f [<] [<] = [<]
+mapRow f (ctx :< (l :- x)) (prfs :< prf) =
+ (:<) (mapRow f ctx prfs) (l :- f x) @{rewrite mapRowNames f ctx prfs in prf}
+
+mapRowNames f [<] [<] = Refl
+mapRowNames f (ctx :< (l :- x)) (prfs :< prf) = cong (:< l) $ mapRowNames f ctx prfs
+
+public export
+Functor Row where
+ map f row = mapRow f row.context row.fresh
+
+public export
+Foldable Row where
+ foldr f x row = foldr (\x, y => f x.value y) x row.context
+ foldl f x row = foldl (\x, y => f x y.value) x row.context
+ null row = null row.context
+ foldlM f x row = foldlM (\x, y => f x y.value) x row.context
+ foldMap f row = foldMap (f . value) row.context
+
-- Operations ------------------------------------------------------------------
export
diff --git a/src/Inky/Data/SnocList/Elem.idr b/src/Inky/Data/SnocList/Elem.idr
index 465e92c..c1e69f6 100644
--- a/src/Inky/Data/SnocList/Elem.idr
+++ b/src/Inky/Data/SnocList/Elem.idr
@@ -8,6 +8,7 @@ import Data.Singleton
import Inky.Decidable
import Inky.Decidable.Maybe
import Inky.Data.Assoc
+import Inky.Data.List
import Inky.Data.SnocList
export
@@ -71,6 +72,11 @@ split Z pos = Left pos
split (S len) Here = Right Here
split (S len) (There pos) = mapSnd There $ split len pos
+public export
+wknL' : Elem x sx -> LengthOf xs -> Elem x (sx <>< xs)
+wknL' i Z = i
+wknL' i (S len) = wknL' (There i) len
+
-- Lookup ----------------------------------------------------------------------
export
diff --git a/src/Inky/Data/SnocList/Quantifiers.idr b/src/Inky/Data/SnocList/Quantifiers.idr
index 73c6551..ac6287b 100644
--- a/src/Inky/Data/SnocList/Quantifiers.idr
+++ b/src/Inky/Data/SnocList/Quantifiers.idr
@@ -4,6 +4,8 @@ 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
public export
@@ -41,6 +43,11 @@ 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
+
+public export
data Pairwise : (a -> a -> Type) -> SnocList a -> Type where
Lin : Pairwise r [<]
(:<) : Pairwise r sx -> All (flip r x) sx -> Pairwise r (sx :< x)
diff --git a/src/Inky/Data/SnocList/Thinning.idr b/src/Inky/Data/SnocList/Thinning.idr
index f766069..60666d2 100644
--- a/src/Inky/Data/SnocList/Thinning.idr
+++ b/src/Inky/Data/SnocList/Thinning.idr
@@ -2,6 +2,7 @@ module Inky.Data.SnocList.Thinning
import Data.DPair
import Data.Nat
+import Inky.Data.List
import Inky.Data.SnocList
import Inky.Data.SnocList.Var
import Inky.Data.SnocList.Quantifiers
@@ -97,6 +98,16 @@ prf.index ((%%) n {pos}) = irrelevantEq $ toVarCong $ toNatInjective $ prf.index
-- Useful for Parsers ----------------------------------------------------------
public export
+(<><) : ctx1 `Thins` ctx2 -> LengthOf bound -> ctx1 <>< bound `Thins` ctx2 <>< bound
+f <>< Z = f
+f <>< S len = Keep f <>< len
+
+public export
+dropFish : ctx1 `Thins` ctx2 -> LengthOf bound -> ctx1 `Thins` ctx2 <>< bound
+dropFish f Z = f
+dropFish f (S len) = dropFish (Drop f) len
+
+public export
dropPos : (pos : Elem x ctx) -> dropElem ctx pos `Thins` ctx
dropPos Here = Drop Id
dropPos (There pos) = Keep (dropPos pos)
diff --git a/src/Inky/Term.idr b/src/Inky/Term.idr
index 1fb50ea..8ae1223 100644
--- a/src/Inky/Term.idr
+++ b/src/Inky/Term.idr
@@ -3,7 +3,6 @@ module Inky.Term
import public Inky.Data.Thinned
import public Inky.Type
-import Control.Function
import Data.List.Quantifiers
import Data.Singleton
import Data.These
@@ -18,27 +17,29 @@ import Inky.Decidable.Maybe
--------------------------------------------------------------------------------
public export
-data Term : (m : Type) -> (tyCtx, tmCtx : SnocList String) -> Type where
- Annot : (meta : m) -> Term m tyCtx tmCtx -> Ty tyCtx -> Term m tyCtx tmCtx
- Var : (meta : m) -> Var tmCtx -> Term m tyCtx tmCtx
- Let : (meta : m) -> Term m tyCtx tmCtx -> (x ** Term m tyCtx (tmCtx :< x)) -> Term m tyCtx tmCtx
- LetTy : (meta : m) -> Ty tyCtx -> (x ** Term m (tyCtx :< x) tmCtx) -> Term m tyCtx tmCtx
- Abs : (meta : m) -> (bound ** Term m tyCtx (tmCtx <>< bound)) -> Term m tyCtx tmCtx
- App : (meta : m) -> Term m tyCtx tmCtx -> List (Term m tyCtx tmCtx) -> Term m tyCtx tmCtx
- Tup : (meta : m) -> Row (Term m tyCtx tmCtx) -> Term m tyCtx tmCtx
- Prj : (meta : m) -> Term m tyCtx tmCtx -> (l : String) -> Term m tyCtx tmCtx
- Inj : (meta : m) -> (l : String) -> Term m tyCtx tmCtx -> Term m tyCtx tmCtx
- Case : (meta : m) -> Term m tyCtx tmCtx -> Row (x ** Term m tyCtx (tmCtx :< x)) -> Term m tyCtx tmCtx
- Roll : (meta : m) -> Term m tyCtx tmCtx -> Term m tyCtx tmCtx
- Unroll : (meta : m) -> Term m tyCtx tmCtx -> Term m tyCtx tmCtx
- Fold : (meta : m) -> Term m tyCtx tmCtx -> (x ** Term m tyCtx (tmCtx :< x)) -> Term m tyCtx tmCtx
- Map : (meta : m) -> (x ** Ty (tyCtx :< x)) -> Ty tyCtx -> Ty tyCtx -> Term m tyCtx tmCtx
- GetChildren : (meta : m) -> (x ** Ty (tyCtx :< x)) -> Ty tyCtx -> Term m tyCtx tmCtx
+data Mode = Sugar | NoSugar
+
+public export
+data Term : Mode -> (m : Type) -> (tyCtx, tmCtx : SnocList String) -> Type where
+ Annot : (meta : m) -> Term mode m tyCtx tmCtx -> Ty tyCtx -> Term mode m tyCtx tmCtx
+ Var : (meta : m) -> Var tmCtx -> Term mode m tyCtx tmCtx
+ Let : (meta : m) -> Term mode m tyCtx tmCtx -> (x ** Term mode m tyCtx (tmCtx :< x)) -> Term mode m tyCtx tmCtx
+ LetTy : (meta : m) -> Ty tyCtx -> (x ** Term mode m (tyCtx :< x) tmCtx) -> Term mode m tyCtx tmCtx
+ Abs : (meta : m) -> (bound ** Term mode m tyCtx (tmCtx <>< bound)) -> Term mode m tyCtx tmCtx
+ App : (meta : m) -> Term mode m tyCtx tmCtx -> List (Term mode m tyCtx tmCtx) -> Term mode m tyCtx tmCtx
+ Tup : (meta : m) -> Row (Term mode m tyCtx tmCtx) -> Term mode m tyCtx tmCtx
+ Prj : (meta : m) -> Term mode m tyCtx tmCtx -> (l : String) -> Term mode m tyCtx tmCtx
+ Inj : (meta : m) -> (l : String) -> Term mode m tyCtx tmCtx -> Term mode m tyCtx tmCtx
+ Case : (meta : m) -> Term mode m tyCtx tmCtx -> Row (x ** Term mode m tyCtx (tmCtx :< x)) -> Term mode m tyCtx tmCtx
+ Roll : (meta : m) -> Term mode m tyCtx tmCtx -> Term mode m tyCtx tmCtx
+ Unroll : (meta : m) -> Term mode m tyCtx tmCtx -> Term mode m tyCtx tmCtx
+ Fold : (meta : m) -> Term mode m tyCtx tmCtx -> (x ** Term mode m tyCtx (tmCtx :< x)) -> Term mode m tyCtx tmCtx
+ Map : (meta : m) -> (x ** Ty (tyCtx :< x)) -> Ty tyCtx -> Ty tyCtx -> Term Sugar m tyCtx tmCtx
%name Term e, f, t, u
export
-(.meta) : Term m tyCtx tmCtx -> m
+(.meta) : Term mode m tyCtx tmCtx -> m
(Annot meta _ _).meta = meta
(Var meta _).meta = meta
(Let meta _ _).meta = meta
@@ -53,7 +54,6 @@ export
(Unroll meta _).meta = meta
(Fold meta _ _).meta = meta
(Map meta _ _ _).meta = meta
-(GetChildren meta _ _).meta = meta
--------------------------------------------------------------------------------
-- Well Formed -----------------------------------------------------------------
@@ -128,40 +128,42 @@ isFunction (x :: bound) a =
namespace Modes
public export
- data SynthsOnly : Term m tyCtx tmCtx -> Type where
- Annot : SynthsOnly (Annot _ t a)
- Var : SynthsOnly (Var _ i)
- App : SynthsOnly (App _ f ts)
- Prj : SynthsOnly (Prj _ e l)
- Unroll : SynthsOnly (Unroll _ e)
- Map : SynthsOnly (Map _ (x ** a) b c)
- GetChildren : SynthsOnly (GetChildren _ (x ** a) b)
+ data SynthsOnly : Term mode m tyCtx tmCtx -> Type where
+ Annot : SynthsOnly (Annot meta t a)
+ Var : SynthsOnly (Var meta i)
+ App : SynthsOnly (App meta f ts)
+ Prj : SynthsOnly (Prj meta e l)
+ Unroll : SynthsOnly (Unroll meta e)
+ Map : SynthsOnly (Map meta (x ** a) b c)
public export
- data ChecksOnly : Term m tyCtx tmCtx -> Type where
- Abs : ChecksOnly (Abs _ (bounds ** t))
- Inj : ChecksOnly (Inj _ l t)
- Case : ChecksOnly (Case _ e ts)
- Roll : ChecksOnly (Roll _ t)
- Fold : ChecksOnly (Fold _ e (x ** t))
+ data ChecksOnly : Term mode m tyCtx tmCtx -> Type where
+ Abs : ChecksOnly (Abs meta (bounds ** t))
+ Inj : ChecksOnly (Inj meta l t)
+ Case : ChecksOnly (Case meta e ts)
+ Roll : ChecksOnly (Roll meta t)
+ Fold : ChecksOnly (Fold meta e (x ** t))
+
+ %name SynthsOnly shape
+ %name ChecksOnly shape
public export
data Synths :
All (const $ Thinned Ty [<]) tyCtx ->
All (const $ Thinned Ty [<]) tmCtx ->
- Term m tyCtx tmCtx -> Ty [<] -> Type
+ Term mode m tyCtx tmCtx -> Ty [<] -> Type
public export
data Checks :
All (const $ Thinned Ty [<]) tyCtx ->
All (const $ Thinned Ty [<]) tmCtx ->
- Ty [<] -> Term m tyCtx tmCtx -> Type
+ Ty [<] -> Term mode m tyCtx tmCtx -> Type
namespace Spine
public export
data CheckSpine :
All (const $ Thinned Ty [<]) tyCtx ->
All (const $ Thinned Ty [<]) tmCtx ->
- Ty [<] -> List (Term m tyCtx tmCtx) -> Ty [<] -> Type
+ Ty [<] -> List (Term mode m tyCtx tmCtx) -> Ty [<] -> Type
where
Nil : CheckSpine tyEnv tmEnv a [] a
(::) :
@@ -176,13 +178,14 @@ namespace Synths
data AllSynths :
All (const $ Thinned Ty [<]) tyCtx ->
All (const $ Thinned Ty [<]) tmCtx ->
- (ts : Context (Term m tyCtx tmCtx)) -> All (const $ Ty [<]) ts.names -> Type
+ Context (Term mode m tyCtx tmCtx) -> Row (Ty [<]) -> Type
where
Lin : AllSynths tyEnv tmEnv [<] [<]
(:<) :
AllSynths tyEnv tmEnv ts as ->
+ {auto 0 freshIn : l `FreshIn` as.names} ->
Synths tyEnv tmEnv t a ->
- AllSynths tyEnv tmEnv (ts :< (l :- t)) (as :< a)
+ AllSynths tyEnv tmEnv (ts :< (l :- t)) (as :< (l :- a))
%name AllSynths prfs
@@ -191,7 +194,7 @@ namespace Checks
data AllChecks :
All (const $ Thinned Ty [<]) tyCtx ->
All (const $ Thinned Ty [<]) tmCtx ->
- Context (Ty [<]) -> Context (Term m tyCtx tmCtx) -> Type
+ Context (Ty [<]) -> Context (Term mode m tyCtx tmCtx) -> Type
where
Base : AllChecks tyEnv tmEnv [<] [<]
Step :
@@ -207,7 +210,7 @@ namespace Branches
data AllBranches :
All (const $ Thinned Ty [<]) tyCtx ->
All (const $ Thinned Ty [<]) tmCtx ->
- Context (Ty [<]) -> Ty [<] -> Context (x ** Term m tyCtx (tmCtx :< x)) -> Type
+ Context (Ty [<]) -> Ty [<] -> Context (x ** Term mode m tyCtx (tmCtx :< x)) -> Type
where
Base : AllBranches tyEnv tmEnv [<] a [<]
Step :
@@ -239,7 +242,7 @@ data Synths where
Synths tyEnv tmEnv (App meta f ts) b
TupS :
AllSynths tyEnv tmEnv es.context as ->
- Synths tyEnv tmEnv (Tup meta es) (TProd (fromAll es as))
+ Synths tyEnv tmEnv (Tup meta es) (TProd as)
PrjS :
Synths tyEnv tmEnv e (TProd as) ->
Elem (l :- a) as.context ->
@@ -255,21 +258,16 @@ data Synths where
(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 :
- WellFormed (TFix x a) ->
- WellFormed b ->
- Synths tyEnv tmEnv (GetChildren meta (x ** a) b)
- (TArrow (sub (tyEnv :< (sub tyEnv b `Over` Id)) a)
- (TProd
- [<"Children" :- sub tyEnv b
- , "Shape" :- sub (tyEnv :< (TNat `Over` Id)) a]))
data Checks where
- EmbedC :
- SynthsOnly e ->
- Synths tyEnv tmEnv e a ->
+ AnnotC :
+ Synths tyEnv tmEnv (Annot meta t a) b ->
+ Alpha b c ->
+ Checks tyEnv tmEnv c (Annot meta t a)
+ VarC :
+ Synths tyEnv tmEnv (Var {mode} meta i) a ->
Alpha a b ->
- Checks tyEnv tmEnv b e
+ Checks tyEnv tmEnv b (Var {mode} meta i)
LetC :
Synths tyEnv tmEnv e a ->
Checks tyEnv (tmEnv :< (a `Over` Id)) b t ->
@@ -282,9 +280,17 @@ data Checks where
IsFunction bound a dom cod ->
Checks tyEnv (tmEnv <>< mapProperty (`Over` Id) dom) cod t ->
Checks tyEnv tmEnv a (Abs meta (bound ** t))
+ AppC :
+ Synths tyEnv tmEnv (App meta e ts) a ->
+ Alpha a b ->
+ Checks tyEnv tmEnv b (App meta e ts)
TupC :
AllChecks tyEnv tmEnv as.context ts.context ->
Checks tyEnv tmEnv (TProd as) (Tup meta ts)
+ PrjC :
+ Synths tyEnv tmEnv (Prj meta e l) a ->
+ Alpha a b ->
+ Checks tyEnv tmEnv b (Prj meta e l)
InjC :
Elem (l :- a) as.context ->
Checks tyEnv tmEnv a t ->
@@ -296,10 +302,32 @@ data Checks where
RollC :
Checks tyEnv tmEnv (sub [<TFix x a `Over` Id] a) t ->
Checks tyEnv tmEnv (TFix x a) (Roll meta t)
+ UnrollC :
+ Synths tyEnv tmEnv (Unroll meta e) a ->
+ Alpha a b ->
+ 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 b (Fold meta e (y ** t))
+ MapC :
+ Synths tyEnv tmEnv (Map meta (x ** a) b c) d ->
+ Alpha d e ->
+ Checks tyEnv tmEnv e (Map meta (x ** a) b c)
+
+public export
+%inline
+EmbedC :
+ SynthsOnly e ->
+ Synths tyEnv tmEnv e a ->
+ Alpha a b ->
+ Checks tyEnv tmEnv b e
+EmbedC Annot prf1 prf2 = AnnotC prf1 prf2
+EmbedC Var prf1 prf2 = VarC prf1 prf2
+EmbedC App prf1 prf2 = AppC prf1 prf2
+EmbedC Prj prf1 prf2 = PrjC prf1 prf2
+EmbedC Unroll prf1 prf2 = UnrollC prf1 prf2
+EmbedC Map prf1 prf2 = MapC prf1 prf2
%name Synths prf
%name Checks prf
@@ -308,19 +336,19 @@ public export
data NotSynths :
All (const $ Thinned Ty [<]) tyCtx ->
All (const $ Thinned Ty [<]) tmCtx ->
- Term m tyCtx tmCtx -> Type
+ Term mode m tyCtx tmCtx -> Type
public export
data NotChecks :
All (const $ Thinned Ty [<]) tyCtx ->
All (const $ Thinned Ty [<]) tmCtx ->
- Ty [<] -> Term m tyCtx tmCtx -> Type
+ Ty [<] -> Term mode m tyCtx tmCtx -> Type
namespace Spine
public export
data NotCheckSpine :
All (const $ Thinned Ty [<]) tyCtx ->
All (const $ Thinned Ty [<]) tmCtx ->
- Ty [<] -> List (Term m tyCtx tmCtx) -> Type
+ Ty [<] -> List (Term mode m tyCtx tmCtx) -> Type
where
Step1 :
((b, c : Ty [<]) -> Not (a = TArrow b c)) ->
@@ -336,7 +364,7 @@ namespace Synths
data AnyNotSynths :
All (const $ Thinned Ty [<]) tyCtx ->
All (const $ Thinned Ty [<]) tmCtx ->
- (ts : Context (Term m tyCtx tmCtx)) -> Type
+ (ts : Context (Term mode m tyCtx tmCtx)) -> Type
where
Step :
These (NotSynths tyEnv tmEnv t) (AnyNotSynths tyEnv tmEnv ts) ->
@@ -349,7 +377,7 @@ namespace Checks
data AnyNotChecks :
All (const $ Thinned Ty [<]) tyCtx ->
All (const $ Thinned Ty [<]) tmCtx ->
- Context (Ty [<]) -> Context (Term m tyCtx tmCtx) -> Type
+ Context (Ty [<]) -> Context (Term mode m tyCtx tmCtx) -> Type
where
Base1 : AnyNotChecks tyEnv tmEnv (as :< la) [<]
Step1 :
@@ -367,7 +395,7 @@ namespace Branches
data AnyNotBranches :
All (const $ Thinned Ty [<]) tyCtx ->
All (const $ Thinned Ty [<]) tmCtx ->
- Context (Ty [<]) -> Ty [<] -> Context (x ** Term m tyCtx (tmCtx :< x)) -> Type
+ Context (Ty [<]) -> Ty [<] -> Context (x ** Term mode m tyCtx (tmCtx :< x)) -> Type
where
Base1 : AnyNotBranches tyEnv tmEnv (as :< a) b [<]
Step1 :
@@ -430,9 +458,6 @@ data NotSynths where
MapNS :
These (IllFormed (TFix x a)) (These (IllFormed b) (IllFormed c)) ->
NotSynths tyEnv tmEnv (Map meta (x ** a) b c)
- GetChildrenNS :
- These (IllFormed (TFix x a)) (IllFormed b) ->
- NotSynths tyEnv tmEnv (GetChildren meta (x ** a) b)
data NotChecks where
EmbedNC1 :
@@ -516,538 +541,31 @@ Uninhabited (NotSynths tyEnv tmEnv (Var meta i)) where
uninhabited (ChecksNS Roll) impossible
uninhabited (ChecksNS Fold) impossible
--- Can recompute type from synthesis proof
-
-export
-synthsRecompute :
- {tyEnv : _} -> {tmEnv : _} -> {e : _} ->
- Synths tyEnv tmEnv e a -> Singleton a
-checkSpineRecompute :
- {tyEnv : _} -> {tmEnv : _} -> {a : _} ->
- CheckSpine tyEnv tmEnv a ts b -> Singleton b
-allSynthsRecompute :
- {tyEnv : _} -> {tmEnv : _} -> {es : Context _} ->
- {0 as : All (const $ Ty [<]) es.names} ->
- AllSynths tyEnv tmEnv es as -> Singleton as
-
-synthsRecompute (AnnotS wf prf) = Val _
-synthsRecompute VarS = Val _
-synthsRecompute (LetS prf1 prf2) with (synthsRecompute prf1)
- _ | Val _ = synthsRecompute prf2
-synthsRecompute (LetTyS wf prf) = synthsRecompute prf
-synthsRecompute (AppS prf prfs) with (synthsRecompute prf)
- _ | Val _ = checkSpineRecompute prfs
-synthsRecompute (TupS prfs) with (allSynthsRecompute prfs)
- _ | Val _ = Val _
-synthsRecompute (PrjS prf i) with (synthsRecompute prf)
- _ | Val _ = [| (nameOf i).value |]
-synthsRecompute (UnrollS prf) with (synthsRecompute prf)
- _ | Val _ = Val _
-synthsRecompute (MapS f g h) = Val _
-synthsRecompute (GetChildrenS f g) = Val _
-
-checkSpineRecompute [] = Val _
-checkSpineRecompute (prf :: prfs) = checkSpineRecompute prfs
-
-allSynthsRecompute [<] = Val _
-allSynthsRecompute (prfs :< prf) = [| allSynthsRecompute prfs :< synthsRecompute prf |]
-
--- Synthesis gives unique types
-
-synthsUnique : Synths tyEnv tmEnv e a -> Synths tyEnv tmEnv e b -> a = b
-checkSpineUnique : CheckSpine tyEnv tmEnv a ts b -> CheckSpine tyEnv tmEnv a ts c -> b = c
-allSynthsUnique : AllSynths tyEnv tmEnv es as -> AllSynths tyEnv tmEnv es bs -> as = bs
-
-synthsUnique (AnnotS _ _) (AnnotS _ _) = Refl
-synthsUnique VarS VarS = Refl
-synthsUnique (LetS prf1 prf2) (LetS prf1' prf2') =
- let prf2' = rewrite synthsUnique prf1 prf1' in prf2' in
- synthsUnique prf2 prf2'
-synthsUnique (LetTyS _ prf) (LetTyS _ prf') = synthsUnique prf prf'
-synthsUnique (AppS prf prfs) (AppS prf' prfs') =
- let prfs' = rewrite synthsUnique prf prf' in prfs' in
- checkSpineUnique prfs prfs'
-synthsUnique (TupS {es} prfs) (TupS prfs') =
- cong (TProd . fromAll es) $ allSynthsUnique prfs prfs'
-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) $
- fixInjective $
- synthsUnique prf prf'
-synthsUnique (MapS _ _ _) (MapS _ _ _) = Refl
-synthsUnique (GetChildrenS _ _) (GetChildrenS _ _) = Refl
-
-checkSpineUnique [] [] = Refl
-checkSpineUnique (prf :: prfs) (prf' :: prfs') = checkSpineUnique prfs prfs'
-
-allSynthsUnique [<] [<] = Refl
-allSynthsUnique (prfs :< prf) (prfs' :< prf') =
- cong2 (:<) (allSynthsUnique prfs prfs') (synthsUnique prf prf')
-
--- We cannot both succeed and fail
-
-synthsSplit : Synths tyEnv tmEnv e a -> NotSynths tyEnv tmEnv e -> Void
-checksSplit : Checks tyEnv tmEnv a t -> NotChecks tyEnv tmEnv a t -> Void
-checkSpineSplit : CheckSpine tyEnv tmEnv a ts b -> NotCheckSpine tyEnv tmEnv a ts -> Void
-allSynthsSplit : AllSynths tyEnv tmEnv es as -> AnyNotSynths tyEnv tmEnv es -> Void
-allChecksSplit :
- (0 fresh : AllFresh as.names) ->
- AllChecks tyEnv tmEnv as ts -> AnyNotChecks tyEnv tmEnv as ts -> Void
-allBranchesSplit :
- (0 fresh : AllFresh as.names) ->
- AllBranches tyEnv tmEnv as a ts -> AnyNotBranches tyEnv tmEnv as a ts -> Void
-
-synthsSplit (AnnotS wf prf) (AnnotNS 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 (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
- checkSpineSplit prfs contras
-synthsSplit (TupS prfs) (TupNS contras) = allSynthsSplit prfs contras
-synthsSplit (PrjS prf i) (PrjNS1 contra) = synthsSplit prf contra
-synthsSplit (PrjS {as} prf i) (PrjNS2 prf' contra) =
- void $ contra as $ synthsUnique prf' prf
-synthsSplit (PrjS {as, a} prf i) (PrjNS3 {as = bs} prf' contra) =
- let i = rewrite inj TProd $ synthsUnique prf' prf in i in
- void $ contra a i
-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 (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 (wellFormedSplit wf1) (wellFormedSplit wf2) (const $ wellFormedSplit wf2) contras
-
-checksSplit (EmbedC _ prf1 prf2) (EmbedNC1 _ contra) = synthsSplit prf1 contra
-checksSplit (EmbedC _ prf1 prf2) (EmbedNC2 _ prf1' contra) =
- let contra = rewrite synthsUnique prf1 prf1' in contra in
- alphaSplit prf2 contra
-checksSplit (LetC prf1 prf2) (LetNC1 contra) = synthsSplit prf1 contra
-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 (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
- let contra = rewrite eq1 in rewrite eq2 in contra in
- checksSplit prf2 contra
-checksSplit (TupC {as} prfs) (TupNC1 contra) = void $ contra as Refl
-checksSplit (TupC {as} prfs) (TupNC2 contras) = allChecksSplit as.fresh prfs contras
-checksSplit (InjC {as} i prf) (InjNC1 contra) = void $ contra as Refl
-checksSplit (InjC {a} i prf) (InjNC2 contra) = void $ contra a i
-checksSplit (InjC {as} i prf) (InjNC3 j contra) =
- let contra = rewrite cong fst $ lookupUnique as i j in contra in
- checksSplit prf contra
-checksSplit (CaseC prf prfs) (CaseNC1 contra) = synthsSplit prf contra
-checksSplit (CaseC {as} prf prfs) (CaseNC2 prf' contra) =
- void $ contra as $ synthsUnique prf' prf
-checksSplit (CaseC {as} prf prfs) (CaseNC3 prf' contras) =
- let contras = rewrite inj TSum $ synthsUnique prf prf' in contras in
- allBranchesSplit as.fresh prfs contras
-checksSplit (RollC {x, a} prf) (RollNC1 contra) = void $ contra x a Refl
-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) =
- let
- contra =
- replace
- {p = \(x ** a) => NotChecks tyEnv (tmEnv :< (sub [<b `Over` Id] a `Over` Id)) b t}
- (fixInjective $ synthsUnique prf1' prf1)
- contra
- in
- checksSplit prf2 contra
-
-checkSpineSplit (prf :: prfs) (Step1 contra) = void $ contra _ _ Refl
-checkSpineSplit (prf :: prfs) (Step2 contras) =
- these (checksSplit prf) (checkSpineSplit prfs) (const $ checkSpineSplit prfs) contras
-
-allSynthsSplit (prfs :< prf) (Step contras) =
- these (synthsSplit prf) (allSynthsSplit prfs) (const $ allSynthsSplit prfs) contras
-
-allChecksSplit fresh (Step i prf prfs) (Step1 contra) = void $ contra _ i
-allChecksSplit fresh (Step {as, t, ts} i prf prfs) (Step2 j contras) =
- let
- contras =
- replace
- {p = \(a ** i) => These (NotChecks tyEnv tmEnv a t) (AnyNotChecks tyEnv tmEnv (dropElem as i) ts)}
- (lookupUnique (MkRow as fresh) j i)
- contras
- 0 fresh = dropElemFresh as fresh i
- in
- these (checksSplit prf) (allChecksSplit fresh prfs) (const $ allChecksSplit fresh prfs) contras
-
-allBranchesSplit fresh (Step i prf prfs) (Step1 contra) = void $ contra _ i
-allBranchesSplit fresh (Step {as, b, x, t, ts} i prf prfs) (Step2 j contras) =
- let
- contras =
- replace
- {p = \(a ** i) =>
- These
- (NotChecks tyEnv (tmEnv :< (a `Over` Id)) b t)
- (AnyNotBranches tyEnv tmEnv (dropElem as i) b ts)}
- (lookupUnique (MkRow as fresh) j i)
- contras
- 0 fresh = dropElemFresh as fresh i
- in
- these (checksSplit prf) (allBranchesSplit fresh prfs) (const $ allBranchesSplit fresh prfs) contras
-
--- Synthesis and Checking are decidable
-
-fallbackCheck :
- SynthsOnly e ->
- Proof (Ty [<]) (Synths tyEnv tmEnv e) (NotSynths tyEnv tmEnv e) ->
- (a : Ty [<]) ->
- LazyEither (Checks tyEnv tmEnv a e) (NotChecks tyEnv tmEnv a e)
-fallbackCheck prf p a =
- map
- (\xPrf => uncurry (EmbedC prf) $ snd xPrf)
- (either (EmbedNC1 prf) (\xPrf => uncurry (EmbedNC2 prf) $ snd xPrf)) $
- (b := p) >=> alpha b a
-
-synths :
- (tyEnv : All (const $ Thinned Ty [<]) tyCtx) ->
- (tmEnv : All (const $ Thinned Ty [<]) tmCtx) ->
- (e : Term 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) ->
- (a : Ty [<]) -> (t : Term 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) ->
- (a : Ty [<]) -> (ts : List (Term 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) ->
- (es : Context (Term m tyCtx tmCtx)) ->
- Proof (All (const $ Ty [<]) es.names) (AllSynths tyEnv tmEnv es) (AnyNotSynths tyEnv tmEnv es)
-allChecks :
- (tyEnv : All (const $ Thinned Ty [<]) tyCtx) ->
- (tmEnv : All (const $ Thinned Ty [<]) tmCtx) ->
- (as : Context (Ty [<])) -> (ts : Context (Term 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) ->
- (as : Context (Ty [<])) -> (a : Ty [<]) -> (ts : Context (x ** Term m tyCtx (tmCtx :< x))) ->
- LazyEither (AllBranches tyEnv tmEnv as a ts) (AnyNotBranches tyEnv tmEnv as a ts)
-
-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 (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
-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)
-synths tyEnv tmEnv (Abs _ (bound ** t)) = Nothing `Because` ChecksNS Abs
-synths tyEnv tmEnv (App _ e ts) =
- map snd
- (\(_, _), (prf1, prf2) => AppS prf1 prf2)
- (either AppNS1 (\xPrfs => uncurry AppNS2 (snd xPrfs))) $
- (a := synths tyEnv tmEnv e) >=> checkSpine tyEnv tmEnv a ts
-synths tyEnv tmEnv (Tup _ (MkRow es fresh)) =
- map (TProd . fromAll (MkRow es fresh)) (\_ => TupS) TupNS $
- allSynths tyEnv tmEnv es
-synths tyEnv tmEnv (Prj meta e l) =
- map (snd . snd) true false $
- (a := synths tyEnv tmEnv e) >=>
- (as := isProd a) >=>
- decLookup l as.context
- where
- true :
- (x : (Ty [<], Row (Ty [<]), Ty [<])) ->
- (Synths tyEnv tmEnv e (fst x), uncurry (\x, yz => (x = TProd (fst yz), uncurry (\y,z => Elem (l :- z) y.context) yz)) x) ->
- Synths tyEnv tmEnv (Prj meta e l) (snd $ snd x)
- true (.(TProd as), as, a) (prf, Refl, i) = PrjS prf i
-
- false :
- Either
- (NotSynths tyEnv tmEnv e)
- (a : Ty [<] ** (Synths tyEnv tmEnv e a,
- Either
- ((as : Row (Ty [<])) -> Not (a = TProd as))
- (as : Row (Ty [<]) ** (a = TProd as, (b : Ty [<]) -> Not (Elem (l :- b) as.context))))) ->
- NotSynths tyEnv tmEnv (Prj meta e l)
- false (Left contra) = PrjNS1 contra
- false (Right (a ** (prf1, Left contra))) = PrjNS2 prf1 contra
- false (Right (.(TProd as) ** (prf1, Right (as ** (Refl, contra))))) = PrjNS3 prf1 contra
-synths tyEnv tmEnv (Inj _ l t) = Nothing `Because` ChecksNS Inj
-synths tyEnv tmEnv (Case _ e (MkRow ts _)) = Nothing `Because` ChecksNS Case
-synths tyEnv tmEnv (Roll _ t) = Nothing `Because` ChecksNS Roll
-synths tyEnv tmEnv (Unroll _ e) =
- map f true false $
- synths tyEnv tmEnv e `andThen` isFix
- where
- f : (Ty [<], (x ** Ty [<x])) -> Ty [<]
- f (a, (x ** b)) = sub [<TFix x b `Over` Id] b
-
- true :
- (axb : _) ->
- (Synths tyEnv tmEnv e (fst axb), uncurry (\a,xb => a = TFix xb.fst xb.snd) axb) ->
- Synths tyEnv tmEnv (Unroll meta e) (f axb)
- true (.(TFix x a), (x ** a)) (prf, Refl) = UnrollS prf
-
- false :
- Either
- (NotSynths tyEnv tmEnv e)
- (a ** (Synths tyEnv tmEnv e a, (x : _) -> (b : _) -> Not (a = TFix x b))) ->
- NotSynths tyEnv tmEnv (Unroll meta e)
- false (Left contra) = UnrollNS1 contra
- false (Right (a ** (prf, contra))) = UnrollNS2 prf contra
-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 (wellFormed (TFix x a)) (all (wellFormed b) (wellFormed c))
-synths tyEnv tmEnv (GetChildren _ (x ** a) b) =
- pure _ $
- map (uncurry GetChildrenS) GetChildrenNS $
- 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
-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
-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)
-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
- where
- false :
- (x ** (uncurry (IsFunction bound a) x, NotChecks tyEnv (tmEnv <>< mapProperty (`Over` Id) (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
-checks tyEnv tmEnv a (Tup _ (MkRow ts fresh')) =
- map true false $
- (as := isProd a) >=> allChecks tyEnv tmEnv as.context ts
- where
- true :
- forall a.
- (as : Row (Ty [<]) ** (a = TProd as, AllChecks tyEnv tmEnv as.context ts)) ->
- Checks tyEnv tmEnv a (Tup meta (MkRow ts fresh'))
- true (as ** (Refl, prf)) = TupC prf
-
- false :
- forall a.
- Either
- ((as : Row (Ty [<])) -> Not (a = TProd as))
- (as : Row (Ty [<]) ** (a = TProd as, AnyNotChecks tyEnv tmEnv as.context ts)) ->
- NotChecks tyEnv tmEnv a (Tup meta (MkRow ts fresh'))
- false (Left contra) = TupNC1 contra
- false (Right (as ** (Refl, contra))) = TupNC2 contra
-checks tyEnv tmEnv a (Prj meta e l) = fallbackCheck Prj (synths tyEnv tmEnv $ Prj meta e l) a
-checks tyEnv tmEnv a (Inj _ l t) =
- map true false $
- (as := isSum a) >=>
- (b := decLookup l as.context) >=>
- checks tyEnv tmEnv b t
- where
- true :
- forall a.
- (as ** (a = TSum as, (b ** (Elem (l :- b) as.context, Checks tyEnv tmEnv b t)))) ->
- Checks tyEnv tmEnv a (Inj meta l t)
- true (as ** (Refl, (b ** (i, prf)))) = InjC i prf
-
- false :
- forall a.
- Either
- ((as : _) -> Not (a = TSum as))
- (as ** (a = TSum as,
- Either
- ((b : _) -> Not (Elem (l :- b) as.context))
- (b ** (Elem (l :- b) as.context, NotChecks tyEnv tmEnv b t)))) ->
- NotChecks tyEnv tmEnv a (Inj meta l t)
- false (Left contra) = InjNC1 contra
- false (Right (as ** (Refl, Left contra))) = InjNC2 contra
- false (Right (as ** (Refl, Right (b ** (i, contra))))) = InjNC3 i contra
-checks tyEnv tmEnv a (Case _ e (MkRow ts fresh)) =
- map true false $
- (b := synths tyEnv tmEnv e) >=>
- (as := isSum b) >=>
- allBranches tyEnv tmEnv as.context a ts
- where
- true :
- forall fresh.
- (b ** (Synths tyEnv tmEnv e b, (as ** (b = TSum as, AllBranches tyEnv tmEnv as.context a ts)))) ->
- Checks tyEnv tmEnv a (Case meta e (MkRow ts fresh))
- true (.(TSum as) ** (prf, (as ** (Refl, prfs)))) = CaseC prf prfs
-
- false :
- forall fresh.
- Either
- (NotSynths tyEnv tmEnv e)
- (b ** (Synths tyEnv tmEnv e b,
- Either
- ((as : _) -> Not (b = TSum as))
- (as ** (b = TSum as, AnyNotBranches tyEnv tmEnv as.context a ts)))) ->
- NotChecks tyEnv tmEnv a (Case meta e (MkRow ts fresh))
- false (Left contra) = CaseNC1 contra
- false (Right (b ** (prf, Left contra))) = CaseNC2 prf contra
- false (Right (.(TSum as) ** (prf, Right (as ** (Refl, contras))))) = CaseNC3 prf contras
-checks tyEnv tmEnv a (Roll _ t) =
- map true false $
- (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
-
- true :
- forall a.
- (xb : (x ** Ty [<x]) ** (a = TFix (fst xb) (snd xb), Checks tyEnv tmEnv (ty xb) t)) ->
- Checks tyEnv tmEnv a (Roll meta t)
- true ((x ** b) ** (Refl, prf)) = RollC prf
-
- false :
- forall a.
- Either
- ((x : _) -> (b : Ty [<x]) -> Not (a = TFix x b))
- (xb : (x ** Ty [<x]) ** (a = TFix (fst xb) (snd xb), NotChecks tyEnv tmEnv (ty xb) t)) ->
- NotChecks tyEnv tmEnv a (Roll meta t)
- false (Left contra) = RollNC1 contra
- false (Right ((x ** b) ** (Refl, contra))) = RollNC2 contra
-checks tyEnv tmEnv a (Unroll meta e) = fallbackCheck Unroll (synths tyEnv tmEnv $ Unroll meta e) a
-checks tyEnv tmEnv a (Fold _ e (x ** t)) =
- map true false $
- (b := synths tyEnv tmEnv e) >=>
- (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)
-
- true :
- (b ** (Synths tyEnv tmEnv e b,
- (yc ** (b = TFix (fst yc) (snd yc), Checks tyEnv (tmEnv' yc) a t)))) ->
- Checks tyEnv tmEnv a (Fold meta e (x ** t))
- true (.(TFix y b) ** (prf1, ((y ** b) ** (Refl, prf2)))) = FoldC prf1 prf2
-
- false :
- Either
- (NotSynths tyEnv tmEnv e)
- (b ** (Synths tyEnv tmEnv e b,
- Either
- ((y : _) -> (c : Ty [<y]) -> Not (b = TFix y c))
- (yc ** (b = TFix (fst yc) (snd yc), NotChecks tyEnv (tmEnv' yc) a t)))) ->
- NotChecks tyEnv tmEnv a (Fold meta e (x ** t))
- false (Left contra) = FoldNC1 contra
- false (Right (b ** (prf1, Left contra))) = FoldNC2 prf1 contra
- false (Right (.(TFix y b) ** (prf1, Right ((y ** b) ** (Refl, contra))))) = FoldNC3 prf1 contra
-checks tyEnv tmEnv a (Map meta (x ** b) c d) =
- fallbackCheck Map (synths tyEnv tmEnv $ Map meta (x ** b) c d) a
-checks tyEnv tmEnv a (GetChildren meta (x ** b) c) =
- fallbackCheck GetChildren (synths tyEnv tmEnv $ GetChildren meta (x ** b) c) a
-
-checkSpine tyEnv tmEnv a [] = Just a `Because` []
-checkSpine tyEnv tmEnv a (t :: ts) =
- map snd true false $
- (bc := isArrow a) >=>
- all (checks tyEnv tmEnv (fst bc) t) (checkSpine tyEnv tmEnv (snd bc) ts)
- where
- true :
- forall a.
- (bcd : ((Ty [<], Ty [<]), Ty [<])) ->
- ( a = TArrow (fst $ fst bcd) (snd $ fst bcd)
- , uncurry (\bc,d => (Checks tyEnv tmEnv (fst bc) t, CheckSpine tyEnv tmEnv (snd bc) ts d)) bcd) ->
- CheckSpine tyEnv tmEnv a (t :: ts) (snd bcd)
- true ((b, c), d) (Refl, (prf1, prf2)) = prf1 :: prf2
-
- false :
- forall a.
- Either
- ((b, c : Ty [<]) -> Not (a = TArrow b c))
- (bc : (Ty [<], Ty [<]) ** (a = TArrow (fst bc) (snd bc),
- These
- (NotChecks tyEnv tmEnv (fst bc) t)
- (NotCheckSpine tyEnv tmEnv (snd bc) ts))) ->
- NotCheckSpine tyEnv tmEnv a (t :: ts)
- false (Left contra) = Step1 contra
- false (Right ((b, c) ** (Refl, contras))) = Step2 contras
-
-allSynths tyEnv tmEnv [<] = Just [<] `Because` [<]
-allSynths tyEnv tmEnv (es :< (l :- e)) =
- map (uncurry (flip (:<))) (\(a, as), (prf, prfs) => prfs :< prf) Step $
- all (synths tyEnv tmEnv e) (allSynths tyEnv tmEnv es)
-
-allChecks tyEnv tmEnv [<] [<] = True `Because` Base
-allChecks tyEnv tmEnv (as :< la) [<] = False `Because` Base1
-allChecks tyEnv tmEnv as (ts :< (l :- t)) =
- map
- (\((a ** i) ** (prf, prfs)) => Step i prf prfs)
- (either Step1 (\xPrf => Step2 (snd $ fst xPrf) (snd xPrf))) $
- (ai := (decLookup l as).forget) >=>
- all (checks tyEnv tmEnv (fst ai) t) (allChecks tyEnv tmEnv (dropElem as $ snd ai) ts)
-
-allBranches tyEnv tmEnv [<] b [<] = True `Because` Base
-allBranches tyEnv tmEnv (as :< la) b [<] = False `Because` Base1
-allBranches tyEnv tmEnv as b (ts :< (l :- (x ** t))) =
- map
- (\((a ** i) ** (prf, prfs)) => Step i prf prfs)
- (either Step1 (\xPrf => Step2 (snd $ fst xPrf) (snd xPrf))) $
- (ai := (decLookup l as).forget) >=>
- all
- (checks tyEnv (tmEnv :< (fst ai `Over` Id)) b t)
- (allBranches tyEnv tmEnv (dropElem as $ snd ai) b ts)
-
-- Sugar -----------------------------------------------------------------------
public export
-CheckLit : m -> Nat -> Term m tyCtx tmCtx
+CheckLit : m -> Nat -> Term mode m tyCtx tmCtx
CheckLit meta 0 = Roll meta (Inj meta "Z" $ Tup meta [<])
CheckLit meta (S n) = Roll meta (Inj meta "S" $ CheckLit meta n)
public export
-Lit : m -> Nat -> Term m tyCtx tmCtx
+Lit : m -> Nat -> Term mode m tyCtx tmCtx
Lit meta n = Annot meta (CheckLit meta n) TNat
public export
-Suc : m -> Term m tyCtx tmCtx
+Suc : m -> Term mode m tyCtx tmCtx
Suc meta =
Annot meta (Abs meta (["_x"] ** Roll meta (Inj meta "S" $ Var meta (%% "_x"))))
(TArrow TNat TNat)
export
-isCheckLit : Term m tyCtx tmCtx -> Maybe Nat
+isCheckLit : Term mode m tyCtx tmCtx -> Maybe Nat
isCheckLit (Roll _ (Inj _ "Z" (Tup _ (MkRow [<] _)))) = Just 0
isCheckLit (Roll _ (Inj _ "S" t)) = S <$> isCheckLit t
isCheckLit _ = Nothing
export
-isLit : Term m tyCtx tmCtx -> Maybe Nat
+isLit : Term mode m tyCtx tmCtx -> Maybe Nat
isLit (Annot _ t a) =
if (alpha {ctx2 = [<]} a TNat).does
then isCheckLit t
@@ -1055,7 +573,7 @@ isLit (Annot _ t a) =
isLit _ = Nothing
export
-isSuc : Term m tyCtx tmCtx -> Bool
+isSuc : Term mode m tyCtx tmCtx -> Bool
isSuc (Annot _ (Abs _ ([x] ** Roll _ (Inj _ "S" $ Var _ ((%%) x {pos = Here})))) a) =
does (alpha {ctx2 = [<]} a (TArrow TNat TNat))
isSuc _ = False
diff --git a/src/Inky/Term/Checks.idr b/src/Inky/Term/Checks.idr
new file mode 100644
index 0000000..8ddcd8d
--- /dev/null
+++ b/src/Inky/Term/Checks.idr
@@ -0,0 +1,538 @@
+module Inky.Term.Checks
+
+import Control.Function
+import Data.DPair
+import Data.List.Quantifiers
+import Data.Singleton
+import Data.These
+import Inky.Data.SnocList.Quantifiers
+import Inky.Decidable
+import Inky.Decidable.Maybe
+import Inky.Term
+
+%hide Prelude.Ops.infixl.(>=>)
+
+-- Can recompute type from synthesis proof
+
+export
+synthsRecompute :
+ {tyEnv : _} -> {tmEnv : _} -> {e : _} ->
+ Synths tyEnv tmEnv e a -> Singleton a
+checkSpineRecompute :
+ {tyEnv : _} -> {tmEnv : _} -> {a : _} ->
+ CheckSpine tyEnv tmEnv a ts b -> Singleton b
+allSynthsRecompute :
+ {tyEnv : _} -> {tmEnv : _} -> {es : Context _} ->
+ {0 as : Row (Ty [<])} ->
+ AllSynths tyEnv tmEnv es as -> Singleton as
+
+synthsRecompute (AnnotS wf prf) = Val _
+synthsRecompute VarS = Val _
+synthsRecompute (LetS prf1 prf2) with (synthsRecompute prf1)
+ _ | Val _ = synthsRecompute prf2
+synthsRecompute (LetTyS wf prf) = synthsRecompute prf
+synthsRecompute (AppS prf prfs) with (synthsRecompute prf)
+ _ | Val _ = checkSpineRecompute prfs
+synthsRecompute (TupS prfs) with (allSynthsRecompute prfs)
+ _ | Val _ = Val _
+synthsRecompute (PrjS prf i) with (synthsRecompute prf)
+ _ | Val _ = [| (nameOf i).value |]
+synthsRecompute (UnrollS prf) with (synthsRecompute prf)
+ _ | Val _ = Val _
+synthsRecompute (MapS f g h) = Val _
+
+checkSpineRecompute [] = Val _
+checkSpineRecompute (prf :: prfs) = checkSpineRecompute prfs
+
+allSynthsRecompute [<] = Val _
+allSynthsRecompute (prfs :< prf) with (allSynthsRecompute prfs) | (synthsRecompute prf)
+ _ | Val _ | Val _ = Val _
+
+-- Synthesis gives unique types
+
+synthsUnique : Synths tyEnv tmEnv e a -> Synths tyEnv tmEnv e b -> a = b
+checkSpineUnique : CheckSpine tyEnv tmEnv a ts b -> CheckSpine tyEnv tmEnv a ts c -> b = c
+allSynthsUnique : AllSynths tyEnv tmEnv es as -> AllSynths tyEnv tmEnv es bs -> as = bs
+
+synthsUnique (AnnotS _ _) (AnnotS _ _) = Refl
+synthsUnique VarS VarS = Refl
+synthsUnique (LetS prf1 prf2) (LetS prf1' prf2') =
+ let prf2' = rewrite synthsUnique prf1 prf1' in prf2' in
+ synthsUnique prf2 prf2'
+synthsUnique (LetTyS _ prf) (LetTyS _ prf') = synthsUnique prf prf'
+synthsUnique (AppS prf prfs) (AppS prf' prfs') =
+ let prfs' = rewrite synthsUnique prf prf' in prfs' in
+ checkSpineUnique prfs prfs'
+synthsUnique (TupS {es} prfs) (TupS prfs') =
+ cong TProd $ allSynthsUnique prfs prfs'
+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) $
+ fixInjective $
+ synthsUnique prf prf'
+synthsUnique (MapS _ _ _) (MapS _ _ _) = Refl
+
+checkSpineUnique [] [] = Refl
+checkSpineUnique (prf :: prfs) (prf' :: prfs') = checkSpineUnique prfs prfs'
+
+allSynthsUnique [<] [<] = Refl
+allSynthsUnique ((:<) prfs {l} prf) (prfs' :< prf') =
+ snocCong (allSynthsUnique prfs prfs') (cong (l :-) $ synthsUnique prf prf')
+
+-- We cannot both succeed and fail
+
+synthsSplit : Synths tyEnv tmEnv e a -> NotSynths tyEnv tmEnv e -> Void
+checksSplit : Checks tyEnv tmEnv a t -> NotChecks tyEnv tmEnv a t -> Void
+checkSpineSplit : CheckSpine tyEnv tmEnv a ts b -> NotCheckSpine tyEnv tmEnv a ts -> Void
+allSynthsSplit : AllSynths tyEnv tmEnv es as -> AnyNotSynths tyEnv tmEnv es -> Void
+allChecksSplit :
+ (0 fresh : AllFresh as.names) ->
+ AllChecks tyEnv tmEnv as ts -> AnyNotChecks tyEnv tmEnv as ts -> Void
+allBranchesSplit :
+ (0 fresh : AllFresh as.names) ->
+ AllBranches tyEnv tmEnv as a ts -> AnyNotBranches tyEnv tmEnv as a ts -> Void
+
+synthsSplit (AnnotS wf prf) (AnnotNS 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 (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
+ checkSpineSplit prfs contras
+synthsSplit (TupS prfs) (TupNS contras) = allSynthsSplit prfs contras
+synthsSplit (PrjS prf i) (PrjNS1 contra) = synthsSplit prf contra
+synthsSplit (PrjS {as} prf i) (PrjNS2 prf' contra) =
+ void $ contra as $ synthsUnique prf' prf
+synthsSplit (PrjS {as, a} prf i) (PrjNS3 {as = bs} prf' contra) =
+ let i = rewrite inj TProd $ synthsUnique prf' prf in i in
+ void $ contra a i
+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 (wellFormedSplit wf1)
+ (these (wellFormedSplit wf2) (wellFormedSplit wf3) (const $ wellFormedSplit wf3))
+ (const $ these (wellFormedSplit wf2) (wellFormedSplit wf3) (const $ wellFormedSplit wf3))
+ contras
+
+checksSplit (AnnotC prf1 prf2) (EmbedNC1 Annot contra) = synthsSplit prf1 contra
+checksSplit (VarC prf1 prf2) (EmbedNC1 Var contra) = synthsSplit prf1 contra
+checksSplit (AppC prf1 prf2) (EmbedNC1 App contra) = synthsSplit prf1 contra
+checksSplit (PrjC prf1 prf2) (EmbedNC1 Prj contra) = synthsSplit prf1 contra
+checksSplit (UnrollC prf1 prf2) (EmbedNC1 Unroll contra) = synthsSplit prf1 contra
+checksSplit (MapC prf1 prf2) (EmbedNC1 Map contra) = synthsSplit prf1 contra
+checksSplit (AnnotC prf1 prf2) (EmbedNC2 Annot prf1' contra) =
+ let contra = rewrite synthsUnique prf1 prf1' in contra in
+ alphaSplit prf2 contra
+checksSplit (VarC prf1 prf2) (EmbedNC2 Var prf1' contra) =
+ let contra = rewrite synthsUnique prf1 prf1' in contra in
+ alphaSplit prf2 contra
+checksSplit (AppC prf1 prf2) (EmbedNC2 App prf1' contra) =
+ let contra = rewrite synthsUnique prf1 prf1' in contra in
+ alphaSplit prf2 contra
+checksSplit (PrjC prf1 prf2) (EmbedNC2 Prj prf1' contra) =
+ let contra = rewrite synthsUnique prf1 prf1' in contra in
+ alphaSplit prf2 contra
+checksSplit (UnrollC prf1 prf2) (EmbedNC2 Unroll prf1' contra) =
+ let contra = rewrite synthsUnique prf1 prf1' in contra in
+ alphaSplit prf2 contra
+checksSplit (MapC prf1 prf2) (EmbedNC2 Map prf1' contra) =
+ let contra = rewrite synthsUnique prf1 prf1' in contra in
+ alphaSplit prf2 contra
+checksSplit (LetC prf1 prf2) (LetNC1 contra) = synthsSplit prf1 contra
+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 (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
+ let contra = rewrite eq1 in rewrite eq2 in contra in
+ checksSplit prf2 contra
+checksSplit (TupC {as} prfs) (TupNC1 contra) = void $ contra as Refl
+checksSplit (TupC {as} prfs) (TupNC2 contras) = allChecksSplit as.fresh prfs contras
+checksSplit (InjC {as} i prf) (InjNC1 contra) = void $ contra as Refl
+checksSplit (InjC {a} i prf) (InjNC2 contra) = void $ contra a i
+checksSplit (InjC {as} i prf) (InjNC3 j contra) =
+ let contra = rewrite cong fst $ lookupUnique as i j in contra in
+ checksSplit prf contra
+checksSplit (CaseC prf prfs) (CaseNC1 contra) = synthsSplit prf contra
+checksSplit (CaseC {as} prf prfs) (CaseNC2 prf' contra) =
+ void $ contra as $ synthsUnique prf' prf
+checksSplit (CaseC {as} prf prfs) (CaseNC3 prf' contras) =
+ let contras = rewrite inj TSum $ synthsUnique prf prf' in contras in
+ allBranchesSplit as.fresh prfs contras
+checksSplit (RollC {x, a} prf) (RollNC1 contra) = void $ contra x a Refl
+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) =
+ let
+ contra =
+ replace
+ {p = \(x ** a) => NotChecks tyEnv (tmEnv :< (sub [<b `Over` Id] a `Over` Id)) b t}
+ (fixInjective $ synthsUnique prf1' prf1)
+ contra
+ in
+ checksSplit prf2 contra
+
+checkSpineSplit (prf :: prfs) (Step1 contra) = void $ contra _ _ Refl
+checkSpineSplit (prf :: prfs) (Step2 contras) =
+ these (checksSplit prf) (checkSpineSplit prfs) (const $ checkSpineSplit prfs) contras
+
+allSynthsSplit (prfs :< prf) (Step contras) =
+ these (synthsSplit prf) (allSynthsSplit prfs) (const $ allSynthsSplit prfs) contras
+
+allChecksSplit fresh (Step i prf prfs) (Step1 contra) = void $ contra _ i
+allChecksSplit fresh (Step {as, t, ts} i prf prfs) (Step2 j contras) =
+ let
+ contras =
+ replace
+ {p = \(a ** i) => These (NotChecks tyEnv tmEnv a t) (AnyNotChecks tyEnv tmEnv (dropElem as i) ts)}
+ (lookupUnique (MkRow as fresh) j i)
+ contras
+ 0 fresh = dropElemFresh as fresh i
+ in
+ these (checksSplit prf) (allChecksSplit fresh prfs) (const $ allChecksSplit fresh prfs) contras
+
+allBranchesSplit fresh (Step i prf prfs) (Step1 contra) = void $ contra _ i
+allBranchesSplit fresh (Step {as, b, x, t, ts} i prf prfs) (Step2 j contras) =
+ let
+ contras =
+ replace
+ {p = \(a ** i) =>
+ These
+ (NotChecks tyEnv (tmEnv :< (a `Over` Id)) b t)
+ (AnyNotBranches tyEnv tmEnv (dropElem as i) b ts)}
+ (lookupUnique (MkRow as fresh) j i)
+ contras
+ 0 fresh = dropElemFresh as fresh i
+ in
+ these (checksSplit prf) (allBranchesSplit fresh prfs) (const $ allBranchesSplit fresh prfs) contras
+
+-- Synthesis and Checking are decidable
+
+fallbackCheck :
+ SynthsOnly e ->
+ Proof (Ty [<]) (Synths tyEnv tmEnv e) (NotSynths tyEnv tmEnv e) ->
+ (a : Ty [<]) ->
+ LazyEither (Checks tyEnv tmEnv a e) (NotChecks tyEnv tmEnv a e)
+fallbackCheck prf p a =
+ map
+ (\xPrf => uncurry (EmbedC prf) $ snd xPrf)
+ (either (EmbedNC1 prf) (\xPrf => uncurry (EmbedNC2 prf) $ snd xPrf)) $
+ (b := p) >=> alpha b a
+
+synths :
+ (tyEnv : All (const $ Thinned Ty [<]) tyCtx) ->
+ (tmEnv : All (const $ Thinned 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) ->
+ (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) ->
+ (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) ->
+ (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) ->
+ (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) ->
+ (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)
+
+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 (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
+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)
+synths tyEnv tmEnv (Abs _ (bound ** t)) = Nothing `Because` ChecksNS Abs
+synths tyEnv tmEnv (App _ e ts) =
+ map snd
+ (\(_, _), (prf1, prf2) => AppS prf1 prf2)
+ (either AppNS1 (\xPrfs => uncurry AppNS2 (snd xPrfs))) $
+ (a := synths tyEnv tmEnv e) >=> checkSpine tyEnv tmEnv a ts
+synths tyEnv tmEnv (Tup _ (MkRow es fresh)) =
+ map (TProd . fst) (\_ => TupS) TupNS $
+ allSynths tyEnv tmEnv es fresh
+synths tyEnv tmEnv (Prj meta e l) =
+ map (snd . snd) true false $
+ (a := synths tyEnv tmEnv e) >=>
+ (as := isProd a) >=>
+ decLookup l as.context
+ where
+ true :
+ (x : (Ty [<], Row (Ty [<]), Ty [<])) ->
+ (Synths tyEnv tmEnv e (fst x), uncurry (\x, yz => (x = TProd (fst yz), uncurry (\y,z => Elem (l :- z) y.context) yz)) x) ->
+ Synths tyEnv tmEnv (Prj meta e l) (snd $ snd x)
+ true (.(TProd as), as, a) (prf, Refl, i) = PrjS prf i
+
+ false :
+ Either
+ (NotSynths tyEnv tmEnv e)
+ (a : Ty [<] ** (Synths tyEnv tmEnv e a,
+ Either
+ ((as : Row (Ty [<])) -> Not (a = TProd as))
+ (as : Row (Ty [<]) ** (a = TProd as, (b : Ty [<]) -> Not (Elem (l :- b) as.context))))) ->
+ NotSynths tyEnv tmEnv (Prj meta e l)
+ false (Left contra) = PrjNS1 contra
+ false (Right (a ** (prf1, Left contra))) = PrjNS2 prf1 contra
+ false (Right (.(TProd as) ** (prf1, Right (as ** (Refl, contra))))) = PrjNS3 prf1 contra
+synths tyEnv tmEnv (Inj _ l t) = Nothing `Because` ChecksNS Inj
+synths tyEnv tmEnv (Case _ e (MkRow ts _)) = Nothing `Because` ChecksNS Case
+synths tyEnv tmEnv (Roll _ t) = Nothing `Because` ChecksNS Roll
+synths tyEnv tmEnv (Unroll _ e) =
+ map f true false $
+ synths tyEnv tmEnv e `andThen` isFix
+ where
+ f : (Ty [<], (x ** Ty [<x])) -> Ty [<]
+ f (a, (x ** b)) = sub [<TFix x b `Over` Id] b
+
+ true :
+ (axb : _) ->
+ (Synths tyEnv tmEnv e (fst axb), uncurry (\a,xb => a = TFix xb.fst xb.snd) axb) ->
+ Synths tyEnv tmEnv (Unroll meta e) (f axb)
+ true (.(TFix x a), (x ** a)) (prf, Refl) = UnrollS prf
+
+ false :
+ Either
+ (NotSynths tyEnv tmEnv e)
+ (a ** (Synths tyEnv tmEnv e a, (x : _) -> (b : _) -> Not (a = TFix x b))) ->
+ NotSynths tyEnv tmEnv (Unroll meta e)
+ false (Left contra) = UnrollNS1 contra
+ false (Right (a ** (prf, contra))) = UnrollNS2 prf contra
+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 (wellFormed (TFix x a)) (all (wellFormed b) (wellFormed c))
+
+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
+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
+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)
+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
+ where
+ false :
+ (x ** (Prelude.uncurry (IsFunction bound a) x, NotChecks tyEnv (tmEnv <>< mapProperty (`Over` Id) (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
+checks tyEnv tmEnv a (Tup _ (MkRow ts fresh')) =
+ map true false $
+ (as := isProd a) >=> allChecks tyEnv tmEnv as.context ts
+ where
+ true :
+ forall a.
+ (as : Row (Ty [<]) ** (a = TProd as, AllChecks tyEnv tmEnv as.context ts)) ->
+ Checks tyEnv tmEnv a (Tup meta (MkRow ts fresh'))
+ true (as ** (Refl, prf)) = TupC prf
+
+ false :
+ forall a.
+ Either
+ ((as : Row (Ty [<])) -> Not (a = TProd as))
+ (as : Row (Ty [<]) ** (a = TProd as, AnyNotChecks tyEnv tmEnv as.context ts)) ->
+ NotChecks tyEnv tmEnv a (Tup meta (MkRow ts fresh'))
+ false (Left contra) = TupNC1 contra
+ false (Right (as ** (Refl, contra))) = TupNC2 contra
+checks tyEnv tmEnv a (Prj meta e l) = fallbackCheck Prj (synths tyEnv tmEnv $ Prj meta e l) a
+checks tyEnv tmEnv a (Inj _ l t) =
+ map true false $
+ (as := isSum a) >=>
+ (b := decLookup l as.context) >=>
+ checks tyEnv tmEnv b t
+ where
+ true :
+ forall a.
+ (as ** (a = TSum as, (b ** (Elem (l :- b) as.context, Checks tyEnv tmEnv b t)))) ->
+ Checks tyEnv tmEnv a (Inj meta l t)
+ true (as ** (Refl, (b ** (i, prf)))) = InjC i prf
+
+ false :
+ forall a.
+ Either
+ ((as : _) -> Not (a = TSum as))
+ (as ** (a = TSum as,
+ Either
+ ((b : _) -> Not (Elem (l :- b) as.context))
+ (b ** (Elem (l :- b) as.context, NotChecks tyEnv tmEnv b t)))) ->
+ NotChecks tyEnv tmEnv a (Inj meta l t)
+ false (Left contra) = InjNC1 contra
+ false (Right (as ** (Refl, Left contra))) = InjNC2 contra
+ false (Right (as ** (Refl, Right (b ** (i, contra))))) = InjNC3 i contra
+checks tyEnv tmEnv a (Case _ e (MkRow ts fresh)) =
+ map true false $
+ (b := synths tyEnv tmEnv e) >=>
+ (as := isSum b) >=>
+ allBranches tyEnv tmEnv as.context a ts
+ where
+ true :
+ forall fresh.
+ (b ** (Synths tyEnv tmEnv e b, (as ** (b = TSum as, AllBranches tyEnv tmEnv as.context a ts)))) ->
+ Checks tyEnv tmEnv a (Case meta e (MkRow ts fresh))
+ true (.(TSum as) ** (prf, (as ** (Refl, prfs)))) = CaseC prf prfs
+
+ false :
+ forall fresh.
+ Either
+ (NotSynths tyEnv tmEnv e)
+ (b ** (Synths tyEnv tmEnv e b,
+ Either
+ ((as : _) -> Not (b = TSum as))
+ (as ** (b = TSum as, AnyNotBranches tyEnv tmEnv as.context a ts)))) ->
+ NotChecks tyEnv tmEnv a (Case meta e (MkRow ts fresh))
+ false (Left contra) = CaseNC1 contra
+ false (Right (b ** (prf, Left contra))) = CaseNC2 prf contra
+ false (Right (.(TSum as) ** (prf, Right (as ** (Refl, contras))))) = CaseNC3 prf contras
+checks tyEnv tmEnv a (Roll _ t) =
+ map true false $
+ (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
+
+ true :
+ forall a.
+ (xb : (x ** Ty [<x]) ** (a = TFix (fst xb) (snd xb), Checks tyEnv tmEnv (ty xb) t)) ->
+ Checks tyEnv tmEnv a (Roll meta t)
+ true ((x ** b) ** (Refl, prf)) = RollC prf
+
+ false :
+ forall a.
+ Either
+ ((x : _) -> (b : Ty [<x]) -> Not (a = TFix x b))
+ (xb : (x ** Ty [<x]) ** (a = TFix (fst xb) (snd xb), NotChecks tyEnv tmEnv (ty xb) t)) ->
+ NotChecks tyEnv tmEnv a (Roll meta t)
+ false (Left contra) = RollNC1 contra
+ false (Right ((x ** b) ** (Refl, contra))) = RollNC2 contra
+checks tyEnv tmEnv a (Unroll meta e) = fallbackCheck Unroll (synths tyEnv tmEnv $ Unroll meta e) a
+checks tyEnv tmEnv a (Fold _ e (x ** t)) =
+ map true false $
+ (b := synths tyEnv tmEnv e) >=>
+ (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)
+
+ true :
+ (b ** (Synths tyEnv tmEnv e b,
+ (yc ** (b = TFix (fst yc) (snd yc), Checks tyEnv (tmEnv' yc) a t)))) ->
+ Checks tyEnv tmEnv a (Fold meta e (x ** t))
+ true (.(TFix y b) ** (prf1, ((y ** b) ** (Refl, prf2)))) = FoldC prf1 prf2
+
+ false :
+ Either
+ (NotSynths tyEnv tmEnv e)
+ (b ** (Synths tyEnv tmEnv e b,
+ Either
+ ((y : _) -> (c : Ty [<y]) -> Not (b = TFix y c))
+ (yc ** (b = TFix (fst yc) (snd yc), NotChecks tyEnv (tmEnv' yc) a t)))) ->
+ NotChecks tyEnv tmEnv a (Fold meta e (x ** t))
+ false (Left contra) = FoldNC1 contra
+ false (Right (b ** (prf1, Left contra))) = FoldNC2 prf1 contra
+ false (Right (.(TFix y b) ** (prf1, Right ((y ** b) ** (Refl, contra))))) = FoldNC3 prf1 contra
+checks tyEnv tmEnv a (Map meta (x ** b) c d) =
+ fallbackCheck Map (synths tyEnv tmEnv $ Map meta (x ** b) c d) a
+
+checkSpine tyEnv tmEnv a [] = Just a `Because` []
+checkSpine tyEnv tmEnv a (t :: ts) =
+ map snd true false $
+ (bc := isArrow a) >=>
+ all (checks tyEnv tmEnv (fst bc) t) (checkSpine tyEnv tmEnv (snd bc) ts)
+ where
+ true :
+ forall a.
+ (bcd : ((Ty [<], Ty [<]), Ty [<])) ->
+ ( a = TArrow (fst $ fst bcd) (snd $ fst bcd)
+ , uncurry (\bc,d => (Checks tyEnv tmEnv (fst bc) t, CheckSpine tyEnv tmEnv (snd bc) ts d)) bcd) ->
+ CheckSpine tyEnv tmEnv a (t :: ts) (snd bcd)
+ true ((b, c), d) (Refl, (prf1, prf2)) = prf1 :: prf2
+
+ false :
+ forall a.
+ Either
+ ((b, c : Ty [<]) -> Not (a = TArrow b c))
+ (bc : (Ty [<], Ty [<]) ** (a = TArrow (fst bc) (snd bc),
+ These
+ (NotChecks tyEnv tmEnv (fst bc) t)
+ (NotCheckSpine tyEnv tmEnv (snd bc) ts))) ->
+ NotCheckSpine tyEnv tmEnv a (t :: ts)
+ false (Left contra) = Step1 contra
+ false (Right ((b, c) ** (Refl, contras))) = Step2 contras
+
+allSynths tyEnv tmEnv [<] [<] = Just (Element [<] Refl) `Because` [<]
+allSynths tyEnv tmEnv (es :< (l :- e)) (fresh :< freshIn) =
+ map
+ (\(a, Element as eq) =>
+ Element ((:<) as (l :- a) @{rewrite sym eq in freshIn}) (cong (:< l) eq))
+ (\(a, Element as eq), (prf, prfs) => (:<) prfs prf @{rewrite sym eq in freshIn})
+ Step $
+ all (synths tyEnv tmEnv e) (allSynths tyEnv tmEnv es fresh)
+
+allChecks tyEnv tmEnv [<] [<] = True `Because` Base
+allChecks tyEnv tmEnv (as :< la) [<] = False `Because` Base1
+allChecks tyEnv tmEnv as (ts :< (l :- t)) =
+ map
+ (\((a ** i) ** (prf, prfs)) => Step i prf prfs)
+ (either Step1 (\xPrf => Step2 (snd $ fst xPrf) (snd xPrf))) $
+ (ai := (decLookup l as).forget) >=>
+ all (checks tyEnv tmEnv (fst ai) t) (allChecks tyEnv tmEnv (dropElem as $ snd ai) ts)
+
+allBranches tyEnv tmEnv [<] b [<] = True `Because` Base
+allBranches tyEnv tmEnv (as :< la) b [<] = False `Because` Base1
+allBranches tyEnv tmEnv as b (ts :< (l :- (x ** t))) =
+ map
+ (\((a ** i) ** (prf, prfs)) => Step i prf prfs)
+ (either Step1 (\xPrf => Step2 (snd $ fst xPrf) (snd xPrf))) $
+ (ai := (decLookup l as).forget) >=>
+ all
+ (checks tyEnv (tmEnv :< (fst ai `Over` Id)) 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
new file mode 100644
index 0000000..50676ce
--- /dev/null
+++ b/src/Inky/Term/Desugar.idr
@@ -0,0 +1,349 @@
+module Inky.Term.Desugar
+
+import Data.List.Quantifiers
+import Data.Maybe
+import Inky.Data.List
+import Inky.Decidable
+import Inky.Term
+import Inky.Term.Substitution
+
+-- Desugar map -----------------------------------------------------------------
+
+desugarMap :
+ (meta : m) =>
+ (a : Ty tyCtx) -> (i : Var tyCtx) -> (0 prf : i `StrictlyPositiveIn` a) ->
+ (f : Term mode m tyCtx' tmCtx) ->
+ (t : Term mode m tyCtx' tmCtx) ->
+ Term mode m tyCtx' tmCtx
+desugarMapTuple :
+ (meta : m) =>
+ (as : Context (Ty tyCtx)) ->
+ (0 fresh : AllFresh as.names) ->
+ (i : Var tyCtx) -> (0 prfs : i `StrictlyPositiveInAll` as) ->
+ (f : Term mode m tyCtx' tmCtx) ->
+ (t : Term mode m tyCtx' tmCtx) ->
+ Row (Term mode m tyCtx' tmCtx)
+desugarMapTupleNames :
+ (0 meta : m) =>
+ (as : Context (Ty tyCtx)) ->
+ (0 fresh : AllFresh as.names) ->
+ (0 i : Var tyCtx) -> (0 prfs : i `StrictlyPositiveInAll` as) ->
+ (0 f : Term mode m tyCtx' tmCtx) ->
+ (0 t : Term mode m tyCtx' tmCtx) ->
+ (desugarMapTuple as fresh i prfs f t).names = as.names
+desugarMapCase :
+ (meta : m) =>
+ (as : Context (Ty tyCtx)) ->
+ (0 fresh : AllFresh as.names) ->
+ (i : Var tyCtx) -> (0 prfs : i `StrictlyPositiveInAll` as) ->
+ (f : Term mode m tyCtx' tmCtx) ->
+ Row (x ** Term mode m tyCtx' (tmCtx :< x))
+desugarMapCaseNames :
+ (meta : m) =>
+ (as : Context (Ty tyCtx)) ->
+ (0 fresh : AllFresh as.names) ->
+ (i : Var tyCtx) -> (0 prfs : i `StrictlyPositiveInAll` as) ->
+ (f : Term mode m tyCtx' tmCtx) ->
+ (desugarMapCase as fresh i prfs f).names = as.names
+
+desugarMap (TVar j) i TVar f t with (i `decEq` j)
+ _ | True `Because` _ = App meta f [t]
+ _ | False `Because` _ = t
+desugarMap (TArrow a b) i (TArrow prf) f t = t
+desugarMap (TProd (MkRow as fresh)) i (TProd prfs) f t =
+ Tup meta (desugarMapTuple as fresh i prfs f t)
+desugarMap (TSum (MkRow as fresh)) i (TSum prfs) f t =
+ Case meta t (desugarMapCase as fresh i prfs f)
+desugarMap (TFix x a) i (TFix prf) f t =
+ Fold meta t ("_eta" ** Roll meta
+ (desugarMap a (ThereVar i) prf (thin (Drop Id) f) (Var meta (%% "_eta"))))
+
+desugarMapTuple [<] [<] i [<] f t = [<]
+desugarMapTuple (as :< (l :- a)) (fresh :< freshIn) i (prfs :< prf) f t =
+ (:<)
+ (desugarMapTuple as fresh i prfs f t)
+ (l :- desugarMap a i prf f (Prj meta t l))
+ @{rewrite desugarMapTupleNames as fresh i prfs f t in freshIn}
+
+desugarMapTupleNames [<] [<] i [<] f t = Refl
+desugarMapTupleNames (as :< (l :- a)) (fresh :< freshIn) i (prfs :< prf) f t =
+ cong (:< l) $ desugarMapTupleNames as fresh i prfs f t
+
+desugarMapCase [<] [<] i [<] f = [<]
+desugarMapCase (as :< (l :- a)) (fresh :< freshIn) i (prfs :< prf) f =
+ (:<)
+ (desugarMapCase as fresh i prfs f)
+ (l :- ("_eta" ** Inj meta l (desugarMap a i prf (thin (Drop Id) f) (Var meta (%% "_eta")))))
+ @{rewrite desugarMapCaseNames as fresh i prfs f in freshIn}
+
+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 :
+ (len : LengthOf tyCtx) =>
+ {t : Term Sugar m tyCtx tmCtx} ->
+ (0 _ : Synths tyEnv tmEnv t a) ->
+ Term NoSugar m tyCtx tmCtx
+desugarChecks :
+ LengthOf tyCtx =>
+ {t : Term Sugar m tyCtx tmCtx} ->
+ (0 _ : Checks tyEnv tmEnv a t) ->
+ Term NoSugar m tyCtx tmCtx
+desugarCheckSpine :
+ LengthOf tyCtx =>
+ {ts : List (Term Sugar m tyCtx tmCtx)} ->
+ (0 _ : CheckSpine tyEnv tmEnv a ts b) ->
+ List (Term NoSugar m tyCtx tmCtx)
+desugarAllSynths :
+ LengthOf tyCtx =>
+ {ts : Context (Term Sugar m tyCtx tmCtx)} ->
+ (0 _ : AllSynths tyEnv tmEnv ts as) ->
+ Context (Term NoSugar m tyCtx tmCtx)
+desugarAllChecks :
+ LengthOf tyCtx =>
+ {ts : Context (Term Sugar m tyCtx tmCtx)} ->
+ (0 _ : AllChecks tyEnv tmEnv as ts) ->
+ Context (Term NoSugar m tyCtx tmCtx)
+desugarAllBranches :
+ LengthOf tyCtx =>
+ {ts : Context (x ** Term Sugar m tyCtx (tmCtx :< x))} ->
+ (0 _ : AllBranches tyEnv tmEnv as a ts) ->
+ Context (x ** Term NoSugar m tyCtx (tmCtx :< x))
+desugarAllSynthsNames :
+ (0 len : LengthOf tyCtx) =>
+ {ts : Context (Term Sugar m tyCtx tmCtx)} ->
+ (0 prfs : AllSynths tyEnv tmEnv ts as) ->
+ (desugarAllSynths prfs).names = ts.names
+desugarAllChecksNames :
+ (0 len : LengthOf tyCtx) =>
+ {ts : Context (Term Sugar m tyCtx tmCtx)} ->
+ (0 prfs : AllChecks tyEnv tmEnv as ts) ->
+ (desugarAllChecks prfs).names = ts.names
+desugarAllBranchesNames :
+ (0 len : LengthOf tyCtx) =>
+ {ts : Context (x ** Term Sugar m tyCtx (tmCtx :< x))} ->
+ (0 prfs : AllBranches tyEnv tmEnv as a ts) ->
+ (desugarAllBranches prfs).names = ts.names
+
+desugarSynths (AnnotS {meta, a} wf prf) = Annot meta (desugarChecks prf) a
+desugarSynths (VarS {meta, i}) = Var meta i
+desugarSynths (LetS {meta, x} prf1 prf2) = Let meta (desugarSynths prf1) (x ** desugarSynths prf2)
+desugarSynths (LetTyS {meta, a, x} wf prf) = LetTy meta a (x ** desugarSynths prf)
+desugarSynths (AppS {meta} prf prfs) = App meta (desugarSynths prf) (desugarCheckSpine prfs)
+desugarSynths (TupS {meta, es} prfs) =
+ Tup meta (MkRow (desugarAllSynths prfs) (rewrite desugarAllSynthsNames prfs in es.fresh))
+desugarSynths (PrjS {meta, l} prf i) = Prj meta (desugarSynths prf) l
+desugarSynths (UnrollS {meta} prf) = Unroll meta (desugarSynths prf)
+desugarSynths (MapS {meta, x, a, b, c} (TFix prf1 wf1) wf2 wf3) =
+ Annot meta
+ (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))
+
+desugarChecks (AnnotC prf1 prf2) = desugarSynths prf1
+desugarChecks (VarC prf1 prf2) = desugarSynths prf1
+desugarChecks (LetC {meta, x} prf1 prf2) = Let meta (desugarSynths prf1) (x ** desugarChecks prf2)
+desugarChecks (LetTyC {meta, a, x} wf prf) = LetTy meta a (x ** desugarChecks prf)
+desugarChecks (AbsC {meta, bound} prf1 prf2) = Abs meta (bound ** desugarChecks prf2)
+desugarChecks (AppC prf1 prf2) = desugarSynths prf1
+desugarChecks (TupC {meta, ts} prfs) =
+ Tup meta (MkRow (desugarAllChecks prfs) (rewrite desugarAllChecksNames prfs in ts.fresh))
+desugarChecks (PrjC prf1 prf2) = desugarSynths prf1
+desugarChecks (InjC {meta, l} i prf) = Inj meta l (desugarChecks prf)
+desugarChecks (CaseC {meta, ts} prf prfs) =
+ Case meta (desugarSynths prf)
+ (MkRow (desugarAllBranches prfs) (rewrite desugarAllBranchesNames prfs in ts.fresh))
+desugarChecks (RollC {meta} prf) = Roll meta (desugarChecks prf)
+desugarChecks (UnrollC prf1 prf2) = desugarSynths prf1
+desugarChecks (FoldC {meta, y} prf1 prf2) = Fold meta (desugarSynths prf1) (y ** desugarChecks prf2)
+desugarChecks (MapC prf1 prf2) = desugarSynths prf1
+
+desugarCheckSpine [] = []
+desugarCheckSpine (prf :: prfs) = desugarChecks prf :: desugarCheckSpine prfs
+
+desugarAllSynths [<] = [<]
+desugarAllSynths ((:<) {l} prfs prf) = desugarAllSynths prfs :< (l :- desugarSynths prf)
+
+desugarAllChecks Base = [<]
+desugarAllChecks (Step {l} i prf prfs) = desugarAllChecks prfs :< (l :- desugarChecks prf)
+
+desugarAllBranches Base = [<]
+desugarAllBranches (Step {l, x} i prf prfs) = desugarAllBranches prfs :< (l :- (x ** desugarChecks prf))
+
+desugarAllSynthsNames [<] = Refl
+desugarAllSynthsNames ((:<) {l} prfs prf) = cong (:< l) $ desugarAllSynthsNames prfs
+
+desugarAllChecksNames Base = Refl
+desugarAllChecksNames (Step {l} i prf prfs) = cong (:< l) $ desugarAllChecksNames prfs
+
+desugarAllBranchesNames Base = Refl
+desugarAllBranchesNames (Step {l} i prf prfs) = cong (:< l) $ desugarAllBranchesNames prfs
+
+-- Fallibly Desugar Terms ------------------------------------------------------
+
+export
+maybeDesugar : (len : LengthOf tyCtx) => Term Sugar m tyCtx tmCtx -> Maybe (Term NoSugar m tyCtx tmCtx)
+maybeDesugarList :
+ (len : LengthOf tyCtx) =>
+ List (Term Sugar m tyCtx tmCtx) -> Maybe (List $ Term NoSugar m tyCtx tmCtx)
+maybeDesugarAll :
+ (len : LengthOf tyCtx) =>
+ (ts : Context (Term Sugar m tyCtx tmCtx)) ->
+ Maybe (All (const $ 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)
+
+maybeDesugar (Annot meta t a) = do
+ t <- maybeDesugar t
+ pure (Annot meta t a)
+maybeDesugar (Var meta i) = pure (Var meta i)
+maybeDesugar (Let meta e (x ** t)) = do
+ e <- maybeDesugar e
+ t <- maybeDesugar t
+ pure (Let meta e (x ** t))
+maybeDesugar (LetTy meta a (x ** t)) = do
+ t <- maybeDesugar t
+ pure (LetTy meta a (x ** t))
+maybeDesugar (Abs meta (bound ** t)) = do
+ t <- maybeDesugar t
+ pure (Abs meta (bound ** t))
+maybeDesugar (App meta e ts) = do
+ e <- maybeDesugar e
+ 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'))
+maybeDesugar (Prj meta e l) = do
+ e <- maybeDesugar e
+ pure (Prj meta e l)
+maybeDesugar (Inj meta l t) = do
+ t <- maybeDesugar t
+ 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'))
+maybeDesugar (Roll meta t) = do
+ t <- maybeDesugar t
+ pure (Roll meta t)
+maybeDesugar (Unroll meta e) = do
+ e <- maybeDesugar e
+ pure (Unroll meta e)
+maybeDesugar (Fold meta e (x ** t)) = do
+ e <- maybeDesugar e
+ t <- maybeDesugar t
+ pure (Fold meta e (x ** t))
+maybeDesugar (Map meta (x ** a) b c) =
+ case (%% x `strictlyPositiveIn` a) of
+ False `Because` contra => Nothing
+ True `Because` prf =>
+ pure $
+ Annot meta
+ (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))
+
+maybeDesugarList [] = pure []
+maybeDesugarList (t :: ts) = [| maybeDesugar t :: maybeDesugarList ts |]
+
+maybeDesugarAll [<] = pure [<]
+maybeDesugarAll (ts :< (l :- t)) = [| maybeDesugarAll ts :< maybeDesugar t |]
+
+maybeDesugarBranches [<] = pure [<]
+maybeDesugarBranches (ts :< (l :- (x ** t))) = do
+ ts <- maybeDesugarBranches ts
+ t <- maybeDesugar t
+ pure (ts :< (x ** t))
diff --git a/src/Inky/Term/Parser.idr b/src/Inky/Term/Parser.idr
index ee122bb..1c6eb58 100644
--- a/src/Inky/Term/Parser.idr
+++ b/src/Inky/Term/Parser.idr
@@ -38,7 +38,6 @@ data InkyKind
| List
| Suc
| Map
- | GetChildren
| ParenOpen
| ParenClose
| BracketOpen
@@ -75,7 +74,6 @@ export
List == List = True
Suc == Suc = True
Map == Map = True
- GetChildren == GetChildren = True
ParenOpen == ParenOpen = True
ParenClose == ParenClose = True
BracketOpen == BracketOpen = True
@@ -113,7 +111,6 @@ Interpolation InkyKind where
interpolate List = "'List'"
interpolate Suc = "'suc'"
interpolate Map = "'map'"
- interpolate GetChildren = "'getChildren'"
interpolate ParenOpen = "'('"
interpolate ParenClose = "')'"
interpolate BracketOpen = "'['"
@@ -154,7 +151,6 @@ TokenKind InkyKind where
tokValue List = const ()
tokValue Suc = const ()
tokValue Map = const ()
- tokValue GetChildren = const ()
tokValue ParenOpen = const ()
tokValue ParenClose = const ()
tokValue BracketOpen = const ()
@@ -188,7 +184,6 @@ keywords =
, ("List", List)
, ("suc", Suc)
, ("map", Map)
- , ("getChildren", GetChildren)
]
export
@@ -281,7 +276,7 @@ TypeFun = ParseFun 1 Ty
public export
TermFun : Type
-TermFun = ParseFun 2 (Term Bounds)
+TermFun = ParseFun 2 (Term Sugar Bounds)
public export
TypeParser : SnocList String -> SnocList String -> Type
@@ -431,7 +426,7 @@ AppTerm =
, weaken (S Z) SuffixTerm
]
, mkApp <$> Seq
- [ OneOf {nils = [False, False, False]}
+ [ OneOf
[ WithBounds SuffixTerm
, mkMap <$> Seq
[ WithBounds (match Map)
@@ -444,16 +439,6 @@ AppTerm =
, sub [<"openType" :- rename Id (Drop Id) OpenType] [<] AtomType
, sub [<"openType" :- rename Id (Drop Id) OpenType] [<] AtomType
]
- , mkGetChildren <$> Seq
- [ WithBounds (match GetChildren)
- , enclose (match ParenOpen) (match ParenClose) $ Seq
- [ match Backslash
- , match TypeIdent
- , match DoubleArrow
- , rename Id (Drop Id) OpenType
- ]
- , sub [<"openType" :- rename Id (Drop Id) OpenType] [<] AtomType
- ]
]
, star (weaken (S Z) SuffixTerm)
]
@@ -468,12 +453,6 @@ AppTerm =
pure $ Map m.bounds (x ** !(a.try (tyCtx :< x))) !(b.try tyCtx) !(c.try tyCtx))
<$ m
- mkGetChildren : HList [WithBounds (), HList [_, String, _, TypeFun], TypeFun] -> WithBounds TermFun
- mkGetChildren [m, [_, x, _, a], b] =
- MkParseFun (\tyCtx, tmCtx =>
- pure $ GetChildren m.bounds (x ** !(a.try (tyCtx :< x))) !(b.try tyCtx))
- <$ m
-
mkApp : HList [WithBounds TermFun, List TermFun] -> TermFun
mkApp [t, []] = t.val
mkApp [fun, (arg :: args)] =
@@ -600,7 +579,7 @@ CaseTerm =
mkBranch :
HList [String, String, (), TermFun] ->
- Assoc (ParseFun 2 $ \tyCtx, tmCtx => (x ** Term Bounds tyCtx (tmCtx :< x)))
+ Assoc (ParseFun 2 $ \tyCtx, tmCtx => (x ** Term Sugar Bounds tyCtx (tmCtx :< x)))
mkBranch [tag, bound, _, branch] =
tag :- MkParseFun (\tyCtx, tmCtx => pure (bound ** !(branch.try tyCtx (tmCtx :< bound))))
diff --git a/src/Inky/Term/Pretty.idr b/src/Inky/Term/Pretty.idr
index 1ff0de0..a2e6407 100644
--- a/src/Inky/Term/Pretty.idr
+++ b/src/Inky/Term/Pretty.idr
@@ -1,11 +1,8 @@
module Inky.Term.Pretty
-import Data.List.Quantifiers
import Data.Singleton
import Data.String
-import Data.These
-import Inky.Decidable.Maybe
import Inky.Term
import Inky.Type.Pretty
@@ -47,12 +44,12 @@ Ord TermPrec where
compare Open d2 = GT
export
-prettyTerm : {tyCtx, tmCtx : SnocList String} -> Term m tyCtx tmCtx -> TermPrec -> Doc ann
-prettyAllTerm : {tyCtx, tmCtx : SnocList String} -> List (Term m tyCtx tmCtx) -> TermPrec -> List (Doc ann)
-prettyTermCtx : {tyCtx, tmCtx : SnocList String} -> Context (Term m tyCtx tmCtx) -> TermPrec -> SnocList (Doc ann)
-prettyCases : {tyCtx, tmCtx : SnocList String} -> Context (x ** Term m tyCtx (tmCtx :< x)) -> SnocList (Doc ann)
+prettyTerm : {tyCtx, tmCtx : SnocList String} -> Term mode m tyCtx tmCtx -> TermPrec -> Doc ann
+prettyAllTerm : {tyCtx, tmCtx : SnocList String} -> List (Term mode m tyCtx tmCtx) -> TermPrec -> List (Doc ann)
+prettyTermCtx : {tyCtx, tmCtx : SnocList String} -> Context (Term mode m tyCtx tmCtx) -> TermPrec -> SnocList (Doc ann)
+prettyCases : {tyCtx, tmCtx : SnocList String} -> Context (x ** Term mode m tyCtx (tmCtx :< x)) -> SnocList (Doc ann)
prettyLet : Doc ann -> Doc ann -> Doc ann
-lessPrettyTerm : {tyCtx, tmCtx : SnocList String} -> Term m tyCtx tmCtx -> TermPrec -> Doc ann
+lessPrettyTerm : {tyCtx, tmCtx : SnocList String} -> Term mode m tyCtx tmCtx -> TermPrec -> Doc ann
prettyTerm t d =
case isLit t <|> isCheckLit t of
@@ -149,13 +146,6 @@ lessPrettyTerm (App _ (Map _ (x ** a) b c) ts) d =
:: prettyType b Atom
:: prettyType c Atom
:: prettyAllTerm ts Suffix)
-lessPrettyTerm (App _ (GetChildren _ (x ** a) b) ts) d =
- group $ align $ hang 2 $ parenthesise (d < App) $
- concatWith (surround line)
- ( pretty "getChildren"
- :: parens (group $ align $ hang 2 $ "\\" <+> pretty x <++> "=>" <+> line <+> prettyType a Open)
- :: prettyType b Atom
- :: prettyAllTerm ts Suffix)
lessPrettyTerm (App _ f ts) d =
group $ align $ hang 2 $ parenthesise (d < App) $
concatWith (surround line) (prettyTerm f Suffix :: prettyAllTerm ts Suffix)
@@ -205,220 +195,3 @@ lessPrettyTerm (Map _ (x ** a) b c) d =
, prettyType b Atom
, prettyType c Atom
]
-lessPrettyTerm (GetChildren _ (x ** a) b) d =
- group $ align $ hang 2 $ parenthesise (d < App) $
- concatWith (surround line)
- [ pretty "getChildren"
- , group (align $ hang 2 $ parens $ "\\" <+> pretty x <++> "=>" <+> line <+> prettyType a Open)
- , prettyType b Atom
- ]
-
--- Typing Errors ---------------------------------------------------------------
-
-Pretty (ChecksOnly t) where
- pretty Abs = "abstraction"
- pretty Inj = "injection"
- pretty Case = "case split"
- pretty Roll = "rolling"
- pretty Fold = "fold"
-
-prettyNotSynths :
- {tyCtx, tmCtx : SnocList String} ->
- {e : Term m tyCtx tmCtx} ->
- {tyEnv : _} -> {tmEnv : _} ->
- NotSynths tyEnv tmEnv e ->
- List (m, Doc ann)
-export
-prettyNotChecks :
- {tyCtx, tmCtx : SnocList String} ->
- {a : Ty [<]} ->
- {t : Term m tyCtx tmCtx} ->
- {tyEnv : _} -> {tmEnv : _} ->
- NotChecks tyEnv tmEnv a t ->
- List (m, Doc ann)
-prettyNotCheckSpine :
- {tyCtx, tmCtx : SnocList String} ->
- {a : Ty [<]} ->
- {ts : List (Term m tyCtx tmCtx)} ->
- {tyEnv : _} -> {tmEnv : _} ->
- NotCheckSpine tyEnv tmEnv a ts ->
- List (m, Doc ann)
-prettyAnyNotSynths :
- {tyCtx, tmCtx : SnocList String} ->
- {es : Context (Term m tyCtx tmCtx)} ->
- {tyEnv : _} -> {tmEnv : _} ->
- AnyNotSynths tyEnv tmEnv es ->
- List (m, Doc ann)
-prettyAnyNotChecks :
- {tyCtx, tmCtx : SnocList String} ->
- {ts : Context (Term m tyCtx tmCtx)} ->
- {tyEnv : _} -> {tmEnv : _} -> {as : Context _} ->
- (meta : m) ->
- AnyNotChecks tyEnv tmEnv as ts ->
- List (m, Doc ann)
-prettyAnyNotBranches :
- {tyCtx, tmCtx : SnocList String} ->
- {ts : Context (x ** Term m tyCtx (tmCtx :< x))} ->
- {tyEnv : _} -> {tmEnv : _} -> {as : Context _} -> {a : _} ->
- (meta : m) ->
- AnyNotBranches tyEnv tmEnv as a ts ->
- List (m, Doc ann)
-
-prettyNotSynths (ChecksNS shape) =
- [(e.meta, pretty "cannot synthesise type of" <++> pretty shape)]
-prettyNotSynths (AnnotNS {a} (This contra)) =
- [(e.meta, pretty "ill-formed type" <+> line <+> prettyType a Open)]
-prettyNotSynths (AnnotNS (That contra)) = prettyNotChecks contra
-prettyNotSynths (AnnotNS {a} (Both contra1 contra2)) =
- (e.meta, pretty "ill-formed type" <+> line <+> prettyType a Open) ::
- prettyNotChecks contra2
-prettyNotSynths (LetNS1 contra) = prettyNotSynths contra
-prettyNotSynths (LetNS2 prf contra) =
- case synthsRecompute prf of
- Val a => prettyNotSynths contra
-prettyNotSynths (LetTyNS {a} (This contra)) =
- [(e.meta, pretty "ill-formed type" <+> line <+> prettyType a Open)]
-prettyNotSynths (LetTyNS (That contra)) = prettyNotSynths contra
-prettyNotSynths (LetTyNS {a} (Both contra1 contra2)) =
- (e.meta, pretty "ill-formed type" <+> line <+> prettyType a Open)
- :: prettyNotSynths contra2
-prettyNotSynths (AppNS1 contra) = prettyNotSynths contra
-prettyNotSynths (AppNS2 prf contras) =
- case synthsRecompute prf of
- Val a => prettyNotCheckSpine contras
-prettyNotSynths (TupNS contras) = prettyAnyNotSynths contras
-prettyNotSynths (PrjNS1 contra) = prettyNotSynths contra
-prettyNotSynths (PrjNS2 prf f) =
- case synthsRecompute prf of
- Val a =>
- [(e.meta
- , pretty "cannot project non-product type" <+> line <+>
- prettyType a Open
- )]
-prettyNotSynths (PrjNS3 {l, as} prf contra) =
- case synthsRecompute prf of
- Val (TProd as) =>
- [(e.meta
- , pretty "unknown label" <++> enclose "'" "'" (pretty l) <+> line <+>
- pretty "in product type" <+> line <+>
- prettyType (TProd as) Open
- )]
-prettyNotSynths (UnrollNS1 contra) = prettyNotSynths contra
-prettyNotSynths (UnrollNS2 prf contra) =
- case synthsRecompute prf of
- Val a =>
- [(e.meta
- , pretty "cannot unroll non-inductive type" <+> line <+>
- prettyType a Open
- )]
-prettyNotSynths (MapNS {a} {b} {c} contras) =
- bifoldMap
- (const [(e.meta, pretty "ill-formed functor" <+> line <+> prettyType a Open)])
- (bifoldMap
- (const [(e.meta, pretty "ill-formed source" <+> line <+> prettyType b Open)])
- (const [(e.meta, pretty "ill-formed target" <+> line <+> prettyType c Open)]))
- contras
-prettyNotSynths (GetChildrenNS {a} {b} contras) =
- bifoldMap
- (const [(e.meta, pretty "ill-formed functor" <+> line <+> prettyType a Open)])
- (const [(e.meta, pretty "ill-formed contents" <+> line <+> prettyType b Open)])
- contras
-
-prettyNotChecks (EmbedNC1 _ contra) = prettyNotSynths contra
-prettyNotChecks (EmbedNC2 _ prf contra) =
- case synthsRecompute prf of
- Val b =>
- [(t.meta
- , pretty "cannot unify" <+> line <+>
- prettyType a Open <+> line <+>
- pretty "and" <+> line <+>
- prettyType b Open
- )]
-prettyNotChecks (LetNC1 contra) = prettyNotSynths contra
-prettyNotChecks (LetNC2 prf contra) =
- case synthsRecompute prf of
- Val _ => prettyNotChecks contra
-prettyNotChecks (LetTyNC {a} (This contra)) =
- [(t.meta, pretty "ill-formed type" <+> line <+> prettyType a Open)]
-prettyNotChecks (LetTyNC (That contra)) = prettyNotChecks contra
-prettyNotChecks (LetTyNC (Both contra1 contra2)) =
- (t.meta, pretty "ill-formed type" <+> line <+> prettyType a Open) ::
- prettyNotChecks contra2
-prettyNotChecks (AbsNC1 contra) =
- [(t.meta, pretty "cannot abstract to construct type" <+> line <+> prettyType a Open)]
-prettyNotChecks (AbsNC2 prf contra) =
- case isFunctionRecompute prf of
- (Val _, Val _) => prettyNotChecks contra
-prettyNotChecks (TupNC1 contra) =
- [(t.meta, pretty "cannot tuple to construct type" <+> line <+> prettyType a Open)]
-prettyNotChecks (TupNC2 contras) = prettyAnyNotChecks t.meta contras
-prettyNotChecks (InjNC1 contra) =
- [(t.meta, pretty "cannot inject to construct type" <+> line <+> prettyType a Open)]
-prettyNotChecks (InjNC2 {l} contra) =
- [(t.meta
- , pretty "unknown label" <++> enclose "'" "'" (pretty l) <+> line <+>
- pretty "in sum type" <+> line <+>
- prettyType a Open
- )]
-prettyNotChecks (InjNC3 i contra) =
- case [| (nameOf i).value |] of
- Val _ => prettyNotChecks contra
-prettyNotChecks (CaseNC1 contra) = prettyNotSynths contra
-prettyNotChecks (CaseNC2 prf contra) =
- case synthsRecompute prf of
- Val a => [(t.meta, pretty "cannot case split on type" <+> line <+> prettyType a Open)]
-prettyNotChecks (CaseNC3 prf contras) =
- case synthsRecompute prf of
- Val _ => prettyAnyNotBranches t.meta contras
-prettyNotChecks (RollNC1 contra) =
- [(t.meta, pretty "cannot roll to construct type" <+> line <+> prettyType a Open)]
-prettyNotChecks (RollNC2 contra) = prettyNotChecks contra
-prettyNotChecks (FoldNC1 contra) = prettyNotSynths contra
-prettyNotChecks (FoldNC2 prf contra) =
- case synthsRecompute prf of
- Val a => [(t.meta, pretty "cannot fold over type" <+> line <+> prettyType a Open)]
-prettyNotChecks (FoldNC3 prf contra) =
- case synthsRecompute prf of
- Val _ => prettyNotChecks contra
-
-prettyNotCheckSpine (Step1 {t} contra) =
- [(t.meta, pretty "cannot apply non-function type" <+> line <+> prettyType a Open)]
-prettyNotCheckSpine (Step2 (This contra)) = prettyNotChecks contra
-prettyNotCheckSpine (Step2 (That contra)) = prettyNotCheckSpine contra
-prettyNotCheckSpine (Step2 (Both contra1 contra2)) =
- prettyNotChecks contra1 ++ prettyNotCheckSpine contra2
-
-prettyAnyNotSynths (Step (This contra)) = prettyNotSynths contra
-prettyAnyNotSynths (Step (That contra)) = prettyAnyNotSynths contra
-prettyAnyNotSynths (Step (Both contra1 contra2)) =
- prettyNotSynths contra1 ++ prettyAnyNotSynths contra2
-
-prettyAnyNotChecks meta Base1 =
- [(meta
- , pretty "missing components" <+> line <+>
- concatWith (surround $ "," <++> neutral) (map pretty as.names <>> [])
- )]
-prettyAnyNotChecks meta (Step1 {t, l} contra) =
- [(t.meta , pretty "unknown label" <++> enclose "'" "'" (pretty l))]
-prettyAnyNotChecks meta (Step2 i (This contra)) =
- case [| (nameOf i).value |] of
- Val _ => prettyNotChecks contra
-prettyAnyNotChecks meta (Step2 i (That contra)) = prettyAnyNotChecks meta contra
-prettyAnyNotChecks meta (Step2 i (Both contra1 contra2)) =
- case [| (nameOf i).value |] of
- Val _ => prettyNotChecks contra1 ++ prettyAnyNotChecks meta contra2
-
-prettyAnyNotBranches meta Base1 =
- [(meta
- , pretty "missing cases" <+> line <+>
- concatWith (surround $ "," <++> neutral) (map pretty as.names <>> [])
- )]
-prettyAnyNotBranches meta (Step1 {t, l} contra) =
- [(t.meta , pretty "unknown label" <++> enclose "'" "'" (pretty l))]
-prettyAnyNotBranches meta (Step2 i (This contra)) =
- case [| (nameOf i).value |] of
- Val _ => prettyNotChecks contra
-prettyAnyNotBranches meta (Step2 i (That contra)) = prettyAnyNotBranches meta contra
-prettyAnyNotBranches meta (Step2 i (Both contra1 contra2)) =
- case [| (nameOf i).value |] of
- Val _ => prettyNotChecks contra1 ++ prettyAnyNotBranches meta contra2
diff --git a/src/Inky/Term/Pretty/Error.idr b/src/Inky/Term/Pretty/Error.idr
new file mode 100644
index 0000000..bb19b2f
--- /dev/null
+++ b/src/Inky/Term/Pretty/Error.idr
@@ -0,0 +1,218 @@
+module Inky.Term.Pretty.Error
+
+import Data.List.Quantifiers
+import Data.Singleton
+import Data.String
+import Data.These
+
+import Inky.Decidable.Maybe
+import Inky.Term
+import Inky.Term.Checks
+import Inky.Type.Pretty
+
+import Text.PrettyPrint.Prettyprinter
+
+-- Typing Errors ---------------------------------------------------------------
+
+Pretty (ChecksOnly t) where
+ pretty Abs = "abstraction"
+ pretty Inj = "injection"
+ pretty Case = "case split"
+ pretty Roll = "rolling"
+ pretty Fold = "fold"
+
+prettyNotSynths :
+ {tyCtx, tmCtx : SnocList String} ->
+ {e : Term mode m tyCtx tmCtx} ->
+ {tyEnv : _} -> {tmEnv : _} ->
+ NotSynths tyEnv tmEnv e ->
+ List (m, Doc ann)
+export
+prettyNotChecks :
+ {tyCtx, tmCtx : SnocList String} ->
+ {a : Ty [<]} ->
+ {t : Term mode m tyCtx tmCtx} ->
+ {tyEnv : _} -> {tmEnv : _} ->
+ NotChecks tyEnv tmEnv a t ->
+ List (m, Doc ann)
+prettyNotCheckSpine :
+ {tyCtx, tmCtx : SnocList String} ->
+ {a : Ty [<]} ->
+ {ts : List (Term mode m tyCtx tmCtx)} ->
+ {tyEnv : _} -> {tmEnv : _} ->
+ NotCheckSpine tyEnv tmEnv a ts ->
+ List (m, Doc ann)
+prettyAnyNotSynths :
+ {tyCtx, tmCtx : SnocList String} ->
+ {es : Context (Term mode m tyCtx tmCtx)} ->
+ {tyEnv : _} -> {tmEnv : _} ->
+ AnyNotSynths tyEnv tmEnv es ->
+ List (m, Doc ann)
+prettyAnyNotChecks :
+ {tyCtx, tmCtx : SnocList String} ->
+ {ts : Context (Term mode m tyCtx tmCtx)} ->
+ {tyEnv : _} -> {tmEnv : _} -> {as : Context _} ->
+ (meta : m) ->
+ AnyNotChecks tyEnv tmEnv as ts ->
+ List (m, Doc ann)
+prettyAnyNotBranches :
+ {tyCtx, tmCtx : SnocList String} ->
+ {ts : Context (x ** Term mode m tyCtx (tmCtx :< x))} ->
+ {tyEnv : _} -> {tmEnv : _} -> {as : Context _} -> {a : _} ->
+ (meta : m) ->
+ AnyNotBranches tyEnv tmEnv as a ts ->
+ List (m, Doc ann)
+
+prettyNotSynths (ChecksNS shape) =
+ [(e.meta, pretty "cannot synthesise type of" <++> pretty shape)]
+prettyNotSynths (AnnotNS {a} (This contra)) =
+ [(e.meta, pretty "ill-formed type" <+> line <+> prettyType a Open)]
+prettyNotSynths (AnnotNS (That contra)) = prettyNotChecks contra
+prettyNotSynths (AnnotNS {a} (Both contra1 contra2)) =
+ (e.meta, pretty "ill-formed type" <+> line <+> prettyType a Open) ::
+ prettyNotChecks contra2
+prettyNotSynths (LetNS1 contra) = prettyNotSynths contra
+prettyNotSynths (LetNS2 prf contra) =
+ case synthsRecompute prf of
+ Val a => prettyNotSynths contra
+prettyNotSynths (LetTyNS {a} (This contra)) =
+ [(e.meta, pretty "ill-formed type" <+> line <+> prettyType a Open)]
+prettyNotSynths (LetTyNS (That contra)) = prettyNotSynths contra
+prettyNotSynths (LetTyNS {a} (Both contra1 contra2)) =
+ (e.meta, pretty "ill-formed type" <+> line <+> prettyType a Open)
+ :: prettyNotSynths contra2
+prettyNotSynths (AppNS1 contra) = prettyNotSynths contra
+prettyNotSynths (AppNS2 prf contras) =
+ case synthsRecompute prf of
+ Val a => prettyNotCheckSpine contras
+prettyNotSynths (TupNS contras) = prettyAnyNotSynths contras
+prettyNotSynths (PrjNS1 contra) = prettyNotSynths contra
+prettyNotSynths (PrjNS2 prf f) =
+ case synthsRecompute prf of
+ Val a =>
+ [(e.meta
+ , pretty "cannot project non-product type" <+> line <+>
+ prettyType a Open
+ )]
+prettyNotSynths (PrjNS3 {l, as} prf contra) =
+ case synthsRecompute prf of
+ Val (TProd as) =>
+ [(e.meta
+ , pretty "unknown label" <++> enclose "'" "'" (pretty l) <+> line <+>
+ pretty "in product type" <+> line <+>
+ prettyType (TProd as) Open
+ )]
+prettyNotSynths (UnrollNS1 contra) = prettyNotSynths contra
+prettyNotSynths (UnrollNS2 prf contra) =
+ case synthsRecompute prf of
+ Val a =>
+ [(e.meta
+ , pretty "cannot unroll non-inductive type" <+> line <+>
+ prettyType a Open
+ )]
+prettyNotSynths (MapNS {a} {b} {c} contras) =
+ bifoldMap
+ (const [(e.meta, pretty "ill-formed functor" <+> line <+> prettyType a Open)])
+ (bifoldMap
+ (const [(e.meta, pretty "ill-formed source" <+> line <+> prettyType b Open)])
+ (const [(e.meta, pretty "ill-formed target" <+> line <+> prettyType c Open)]))
+ contras
+
+prettyNotChecks (EmbedNC1 _ contra) = prettyNotSynths contra
+prettyNotChecks (EmbedNC2 _ prf contra) =
+ case synthsRecompute prf of
+ Val b =>
+ [(t.meta
+ , pretty "cannot unify" <+> line <+>
+ prettyType a Open <+> line <+>
+ pretty "and" <+> line <+>
+ prettyType b Open
+ )]
+prettyNotChecks (LetNC1 contra) = prettyNotSynths contra
+prettyNotChecks (LetNC2 prf contra) =
+ case synthsRecompute prf of
+ Val _ => prettyNotChecks contra
+prettyNotChecks (LetTyNC {a} (This contra)) =
+ [(t.meta, pretty "ill-formed type" <+> line <+> prettyType a Open)]
+prettyNotChecks (LetTyNC (That contra)) = prettyNotChecks contra
+prettyNotChecks (LetTyNC (Both contra1 contra2)) =
+ (t.meta, pretty "ill-formed type" <+> line <+> prettyType a Open) ::
+ prettyNotChecks contra2
+prettyNotChecks (AbsNC1 contra) =
+ [(t.meta, pretty "cannot abstract to construct type" <+> line <+> prettyType a Open)]
+prettyNotChecks (AbsNC2 prf contra) =
+ case isFunctionRecompute prf of
+ (Val _, Val _) => prettyNotChecks contra
+prettyNotChecks (TupNC1 contra) =
+ [(t.meta, pretty "cannot tuple to construct type" <+> line <+> prettyType a Open)]
+prettyNotChecks (TupNC2 contras) = prettyAnyNotChecks t.meta contras
+prettyNotChecks (InjNC1 contra) =
+ [(t.meta, pretty "cannot inject to construct type" <+> line <+> prettyType a Open)]
+prettyNotChecks (InjNC2 {l} contra) =
+ [(t.meta
+ , pretty "unknown label" <++> enclose "'" "'" (pretty l) <+> line <+>
+ pretty "in sum type" <+> line <+>
+ prettyType a Open
+ )]
+prettyNotChecks (InjNC3 i contra) =
+ case [| (nameOf i).value |] of
+ Val _ => prettyNotChecks contra
+prettyNotChecks (CaseNC1 contra) = prettyNotSynths contra
+prettyNotChecks (CaseNC2 prf contra) =
+ case synthsRecompute prf of
+ Val a => [(t.meta, pretty "cannot case split on type" <+> line <+> prettyType a Open)]
+prettyNotChecks (CaseNC3 prf contras) =
+ case synthsRecompute prf of
+ Val _ => prettyAnyNotBranches t.meta contras
+prettyNotChecks (RollNC1 contra) =
+ [(t.meta, pretty "cannot roll to construct type" <+> line <+> prettyType a Open)]
+prettyNotChecks (RollNC2 contra) = prettyNotChecks contra
+prettyNotChecks (FoldNC1 contra) = prettyNotSynths contra
+prettyNotChecks (FoldNC2 prf contra) =
+ case synthsRecompute prf of
+ Val a => [(t.meta, pretty "cannot fold over type" <+> line <+> prettyType a Open)]
+prettyNotChecks (FoldNC3 prf contra) =
+ case synthsRecompute prf of
+ Val _ => prettyNotChecks contra
+
+prettyNotCheckSpine (Step1 {t} contra) =
+ [(t.meta, pretty "cannot apply non-function type" <+> line <+> prettyType a Open)]
+prettyNotCheckSpine (Step2 (This contra)) = prettyNotChecks contra
+prettyNotCheckSpine (Step2 (That contra)) = prettyNotCheckSpine contra
+prettyNotCheckSpine (Step2 (Both contra1 contra2)) =
+ prettyNotChecks contra1 ++ prettyNotCheckSpine contra2
+
+prettyAnyNotSynths (Step (This contra)) = prettyNotSynths contra
+prettyAnyNotSynths (Step (That contra)) = prettyAnyNotSynths contra
+prettyAnyNotSynths (Step (Both contra1 contra2)) =
+ prettyNotSynths contra1 ++ prettyAnyNotSynths contra2
+
+prettyAnyNotChecks meta Base1 =
+ [(meta
+ , pretty "missing components" <+> line <+>
+ concatWith (surround $ "," <++> neutral) (map pretty as.names <>> [])
+ )]
+prettyAnyNotChecks meta (Step1 {t, l} contra) =
+ [(t.meta , pretty "unknown label" <++> enclose "'" "'" (pretty l))]
+prettyAnyNotChecks meta (Step2 i (This contra)) =
+ case [| (nameOf i).value |] of
+ Val _ => prettyNotChecks contra
+prettyAnyNotChecks meta (Step2 i (That contra)) = prettyAnyNotChecks meta contra
+prettyAnyNotChecks meta (Step2 i (Both contra1 contra2)) =
+ case [| (nameOf i).value |] of
+ Val _ => prettyNotChecks contra1 ++ prettyAnyNotChecks meta contra2
+
+prettyAnyNotBranches meta Base1 =
+ [(meta
+ , pretty "missing cases" <+> line <+>
+ concatWith (surround $ "," <++> neutral) (map pretty as.names <>> [])
+ )]
+prettyAnyNotBranches meta (Step1 {t, l} contra) =
+ [(t.meta , pretty "unknown label" <++> enclose "'" "'" (pretty l))]
+prettyAnyNotBranches meta (Step2 i (This contra)) =
+ case [| (nameOf i).value |] of
+ Val _ => prettyNotChecks contra
+prettyAnyNotBranches meta (Step2 i (That contra)) = prettyAnyNotBranches meta contra
+prettyAnyNotBranches meta (Step2 i (Both contra1 contra2)) =
+ case [| (nameOf i).value |] of
+ Val _ => prettyNotChecks contra1 ++ prettyAnyNotBranches meta contra2
diff --git a/src/Inky/Term/Substitution.idr b/src/Inky/Term/Substitution.idr
new file mode 100644
index 0000000..791014b
--- /dev/null
+++ b/src/Inky/Term/Substitution.idr
@@ -0,0 +1,197 @@
+module Inky.Term.Substitution
+
+import Data.List.Quantifiers
+import Inky.Data.List
+import Inky.Term
+
+public export
+thin : ctx1 `Thins` ctx2 -> Term mode m tyCtx ctx1 -> Term mode m tyCtx ctx2
+public export
+thinList : ctx1 `Thins` ctx2 -> List (Term mode m tyCtx ctx1) -> List (Term mode m tyCtx ctx2)
+public export
+thinAll : ctx1 `Thins` ctx2 -> Context (Term mode m tyCtx ctx1) -> Context (Term mode m tyCtx ctx2)
+public export
+thinAllNames :
+ (f : ctx1 `Thins` ctx2) -> (ts : Context (Term mode m tyCtx ctx1)) ->
+ (thinAll f ts).names = ts.names
+public export
+thinBranches :
+ ctx1 `Thins` ctx2 ->
+ Context (x ** Term mode m tyCtx (ctx1 :< x)) ->
+ Context (x ** Term mode m tyCtx (ctx2 :< x))
+public export
+thinBranchesNames :
+ (f : ctx1 `Thins` ctx2) -> (ts : Context (x ** Term mode m tyCtx (ctx1 :< x))) ->
+ (thinBranches f ts).names = ts.names
+
+thin f (Annot meta t a) = Annot meta (thin f t) a
+thin f (Var meta i) = Var meta (index f i)
+thin f (Let meta e (x ** t)) = Let meta (thin f e) (x ** thin (Keep f) t)
+thin f (LetTy meta a (x ** t)) = LetTy meta a (x ** thin f t)
+thin f (Abs meta (bound ** t)) = Abs meta (bound ** thin (f <>< lengthOf bound) t)
+thin f (App meta e ts) = App meta (thin f e) (thinList f ts)
+thin f (Tup meta (MkRow ts fresh)) =
+ Tup meta (MkRow (thinAll f ts) (rewrite thinAllNames f ts in fresh))
+thin f (Prj meta e l) = Prj meta (thin f e) l
+thin f (Inj meta l t) = Inj meta l (thin f t)
+thin f (Case meta t (MkRow ts fresh)) =
+ Case meta (thin f t) (MkRow (thinBranches f ts) (rewrite thinBranchesNames f ts in fresh))
+thin f (Roll meta t) = Roll meta (thin f t)
+thin f (Unroll meta e) = Unroll meta (thin f e)
+thin f (Fold meta e (x ** t)) = Fold meta (thin f e) (x ** thin (Keep f) t)
+thin f (Map meta (x ** a) b c) = Map meta (x ** a) b c
+
+thinList f [] = []
+thinList f (t :: ts) = thin f t :: thinList f ts
+
+thinAll f [<] = [<]
+thinAll f (ts :< (l :- t)) = thinAll f ts :< (l :- thin f t)
+
+thinAllNames f [<] = Refl
+thinAllNames f (ts :< (l :- t)) = cong (:< l) $ thinAllNames f ts
+
+thinBranches f [<] = [<]
+thinBranches f (ts :< (l :- (x ** t))) = thinBranches f ts :< (l :- (x ** thin (Keep f) t))
+
+thinBranchesNames f [<] = Refl
+thinBranchesNames f (ts :< (l :- (x ** t))) = cong (:< l) $ thinBranchesNames f ts
+
+public export
+thinTy : ctx1 `Thins` ctx2 -> Term mode m ctx1 tmCtx -> Term mode m ctx2 tmCtx
+public export
+thinTyList : ctx1 `Thins` ctx2 -> List (Term mode m ctx1 tmCtx) -> List (Term mode m ctx2 tmCtx)
+public export
+thinTyAll : ctx1 `Thins` ctx2 -> Context (Term mode m ctx1 tmCtx) -> Context (Term mode m ctx2 tmCtx)
+public export
+thinTyAllNames :
+ (f : ctx1 `Thins` ctx2) -> (ts : Context (Term mode m ctx1 tmCtx)) ->
+ (thinTyAll f ts).names = ts.names
+public export
+thinTyBranches :
+ ctx1 `Thins` ctx2 ->
+ Context (x ** Term mode m ctx1 (tmCtx :< x)) ->
+ Context (x ** Term mode m ctx2 (tmCtx :< x))
+public export
+thinTyBranchesNames :
+ (f : ctx1 `Thins` ctx2) -> (ts : Context (x ** Term mode m ctx1 (tmCtx :< x))) ->
+ (thinTyBranches f ts).names = ts.names
+
+thinTy f (Annot meta t a) = Annot meta (thinTy f t) (rename f a)
+thinTy f (Var meta i) = Var meta i
+thinTy f (Let meta e (x ** t)) = Let meta (thinTy f e) (x ** thinTy f t)
+thinTy f (LetTy meta a (x ** t)) = LetTy meta (rename f a) (x ** thinTy (Keep f) t)
+thinTy f (Abs meta (bound ** t)) = Abs meta (bound ** thinTy f t)
+thinTy f (App meta e ts) = App meta (thinTy f e) (thinTyList f ts)
+thinTy f (Tup meta (MkRow ts fresh)) =
+ Tup meta (MkRow (thinTyAll f ts) (rewrite thinTyAllNames f ts in fresh))
+thinTy f (Prj meta e l) = Prj meta (thinTy f e) l
+thinTy f (Inj meta l t) = Inj meta l (thinTy f t)
+thinTy f (Case meta t (MkRow ts fresh)) =
+ Case meta (thinTy f t) (MkRow (thinTyBranches f ts) (rewrite thinTyBranchesNames f ts in fresh))
+thinTy f (Roll meta t) = Roll meta (thinTy f t)
+thinTy f (Unroll meta e) = Unroll meta (thinTy f e)
+thinTy f (Fold meta e (x ** t)) = Fold meta (thinTy f e) (x ** thinTy f t)
+thinTy f (Map meta (x ** a) b c) = Map meta (x ** rename (Keep f) a) (rename f b) (rename f c)
+
+thinTyList f [] = []
+thinTyList f (t :: ts) = thinTy f t :: thinTyList f ts
+
+thinTyAll f [<] = [<]
+thinTyAll f (ts :< (l :- t)) = thinTyAll f ts :< (l :- thinTy f t)
+
+thinTyAllNames f [<] = Refl
+thinTyAllNames f (ts :< (l :- t)) = cong (:< l) $ thinTyAllNames f ts
+
+thinTyBranches f [<] = [<]
+thinTyBranches f (ts :< (l :- (x ** t))) = thinTyBranches f ts :< (l :- (x ** thinTy f t))
+
+thinTyBranchesNames f [<] = Refl
+thinTyBranchesNames f (ts :< (l :- (x ** t))) = cong (:< l) $ thinTyBranchesNames f ts
+
+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
+
+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
+
+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))
+
+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)
+
+public export
+sub :
+ Env mode m tyCtx ctx1 ctx2 ->
+ Term mode m tyCtx ctx1 -> Term mode m tyCtx ctx2
+public export
+subList :
+ Env mode m tyCtx ctx1 ctx2 ->
+ List (Term mode m tyCtx ctx1) -> List (Term mode m tyCtx ctx2)
+public export
+subAll :
+ Env mode m tyCtx ctx1 ctx2 ->
+ Context (Term mode m tyCtx ctx1) -> Context (Term mode m tyCtx ctx2)
+public export
+subAllNames :
+ (f : Env mode m tyCtx ctx1 ctx2) ->
+ (ts : Context (Term mode m tyCtx ctx1)) -> (subAll f ts).names = ts.names
+public export
+subBranches :
+ Env mode m tyCtx ctx1 ctx2 ->
+ Context (x ** Term mode m tyCtx (ctx1 :< x)) ->
+ Context (x ** Term mode m tyCtx (ctx2 :< x))
+public export
+subBranchesNames :
+ (f : Env mode m tyCtx ctx1 ctx2) ->
+ (ts : Context (x ** Term mode m tyCtx (ctx1 :< x))) -> (subBranches f ts).names = ts.names
+
+public export
+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
+
+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 (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 (Abs meta (bound ** t)) =
+ let len = lengthOf bound in
+ Abs meta (bound ** sub (thinEnv (dropFish Id len) f <>< keepBound len) t)
+sub f (App meta e ts) = App meta (sub f e) (subList f ts)
+sub f (Tup meta (MkRow ts fresh)) =
+ Tup meta (MkRow (subAll f ts) (rewrite subAllNames f ts in fresh))
+sub f (Prj meta e l) = Prj meta (sub f e) l
+sub f (Inj meta l t) = Inj meta l (sub f t)
+sub f (Case meta t (MkRow ts fresh)) =
+ Case meta (sub f t) (MkRow (subBranches f ts) (rewrite subBranchesNames f ts in fresh))
+sub f (Roll meta t) = Roll meta (sub f t)
+sub f (Unroll meta e) = Unroll meta (sub f e)
+sub f (Fold meta e (x ** t)) = Fold meta (sub f e) (x ** sub (lift f) t)
+sub f (Map meta (x ** a) b c) = Map meta (x ** a) b c
+
+subList f [] = []
+subList f (t :: ts) = sub f t :: subList f ts
+
+subAll f [<] = [<]
+subAll f (ts :< (l :- t)) = subAll f ts :< (l :- sub f t)
+
+subAllNames f [<] = Refl
+subAllNames f (ts :< (l :- t)) = cong (:< l) $ subAllNames f ts
+
+subBranches f [<] = [<]
+subBranches f (ts :< (l :- (x ** t))) = subBranches f ts :< (l :- (x ** sub (lift f) t))
+
+subBranchesNames f [<] = Refl
+subBranchesNames f (ts :< (l :- (x ** t))) = cong (:< l) $ subBranchesNames f ts
diff --git a/src/Inky/Type.idr b/src/Inky/Type.idr
index f40ecba..72388b6 100644
--- a/src/Inky/Type.idr
+++ b/src/Inky/Type.idr
@@ -372,6 +372,66 @@ allAlphaRefl [<] .([<]) Refl = Base
allAlphaRefl (as :< (l :- a)) .(as :< (l :- a)) Refl =
Step Here (alphaRefl a a Refl) (allAlphaRefl as as Refl)
+namespace Sym
+ data AllAlpha' : Context (Ty ctx1) -> Context (Ty ctx2) -> Type where
+ Base : AllAlpha' [<] [<]
+ Step :
+ {0 as : Context (Ty ctx1)} -> {0 bs : Context (Ty ctx2)} ->
+ (i : Elem (l :- a) as) -> (j : Elem (l :- b) bs) ->
+ Alpha a b ->
+ AllAlpha' (dropElem as i) (dropElem bs j) ->
+ AllAlpha' as bs
+
+ %name AllAlpha' prfs
+
+ pinch :
+ (i : Elem x sx) -> (j : Elem y (dropElem sx i)) ->
+ Elem x (dropElem sx (indexPos (dropPos i) j))
+ pinch Here j = Here
+ pinch (There i) Here = i
+ pinch (There i) (There j) = There (pinch i j)
+
+ dropPinch :
+ (i : Elem x sx) -> (j : Elem y (dropElem sx i)) ->
+ dropElem (dropElem sx i) j = dropElem (dropElem sx $ indexPos (dropPos i) j) (pinch i j)
+ dropPinch Here j = Refl
+ dropPinch (There i) Here = Refl
+ dropPinch {sx = _ :< y} (There i) (There j) = cong (:< y) $ dropPinch i j
+
+ toStep :
+ AllAlpha' (as :< (l :- a)) bs ->
+ Exists (\b => (i : Elem (l :- b) bs ** (Alpha a b, AllAlpha' as (dropElem bs i))))
+ toStep (Step Here j prf prfs) = Evidence _ (j ** (prf, prfs))
+ toStep (Step {b = b'} (There i) j prf prfs) =
+ let Evidence b (k ** (prf', prfs)) = toStep prfs in
+ Evidence b
+ (indexPos (dropPos j) k **
+ (prf', Step i (pinch j k) prf (rewrite sym $ dropPinch j k in prfs)))
+
+ elemIsSnoc : Elem x sx -> NonEmpty sx
+ elemIsSnoc Here = IsSnoc
+ elemIsSnoc (There _) = IsSnoc
+
+ toAll : AllAlpha' as bs -> AllAlpha as bs
+ toAll Base = Base
+ toAll (Step i j prf prfs) with (elemIsSnoc i)
+ toAll {as = as :< (l :- a)} (Step i j prf prfs) | IsSnoc =
+ let Evidence b (k ** (prf, prfs)) = toStep (Step i j prf prfs) in
+ Step k prf (toAll prfs)
+
+ export
+ alphaSym : Alpha a b -> Alpha b a
+ allAlphaSym : AllAlpha as bs -> AllAlpha' bs as
+
+ alphaSym (TVar prf) = TVar (sym prf)
+ alphaSym (TArrow prf1 prf2) = TArrow (alphaSym prf1) (alphaSym prf2)
+ alphaSym (TProd prfs) = TProd (toAll $ allAlphaSym prfs)
+ alphaSym (TSum prfs) = TSum (toAll $ allAlphaSym prfs)
+ alphaSym (TFix prf) = TFix (alphaSym prf)
+
+ allAlphaSym Base = Base
+ allAlphaSym (Step i prf prfs) = Step i Here (alphaSym prf) (allAlphaSym prfs)
+
export
alphaSplit :
{0 a : Ty ctx1} -> {0 b : Ty ctx2} ->
@@ -739,9 +799,11 @@ allWellFormed (as :< (n :- a)) =
-- Substitution ----------------------------------------------------------------
--------------------------------------------------------------------------------
-export
+public export
sub : All (const $ Thinned Ty ctx2) ctx1 -> Ty ctx1 -> Ty ctx2
+public export
subAll : All (const $ Thinned Ty ctx2) ctx1 -> Context (Ty ctx1) -> Context (Ty ctx2)
+public export
subAllNames :
(f : All (const $ Thinned Ty ctx2) ctx1) ->
(ctx : Context (Ty ctx1)) ->
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-30 07:52:32 +0000