From 3caa95a139538bb07c74847ca3aba2603a03c502 Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Fri, 15 Nov 2024 15:44:30 +0000 Subject: Add compilation to scheme. Extract parser as an independent project. --- src/Inky/Data/Assoc.idr | 38 -- src/Inky/Data/Context.idr | 34 -- src/Inky/Data/Context/Var.idr | 117 ------ src/Inky/Data/Fun.idr | 4 +- src/Inky/Data/List.idr | 13 - src/Inky/Data/Row.idr | 36 +- src/Inky/Data/SnocList.idr | 43 -- src/Inky/Data/SnocList/Elem.idr | 116 ------ src/Inky/Data/SnocList/Quantifiers.idr | 44 -- src/Inky/Data/SnocList/Thinning.idr | 228 ---------- src/Inky/Data/SnocList/Var.idr | 90 ---- src/Inky/Data/Thinned.idr | 13 +- src/Inky/Decidable.idr | 261 ------------ src/Inky/Decidable/Either.idr | 111 ----- src/Inky/Decidable/Maybe.idr | 146 ------- src/Inky/Parser.idr | 733 --------------------------------- src/Inky/Term.idr | 13 +- src/Inky/Term/Checks.idr | 43 +- src/Inky/Term/Compile.idr | 316 ++++++++++++++ src/Inky/Term/Desugar.idr | 4 +- src/Inky/Term/Parser.idr | 15 +- src/Inky/Term/Pretty/Error.idr | 5 +- src/Inky/Term/Recompute.idr | 128 ++++++ src/Inky/Term/Substitution.idr | 2 +- src/Inky/Type.idr | 87 +++- src/Inky/Type/Pretty.idr | 2 +- src/Inky/Type/Substitution.idr | 364 ++++++++++++++++ 27 files changed, 939 insertions(+), 2067 deletions(-) delete mode 100644 src/Inky/Data/Assoc.idr delete mode 100644 src/Inky/Data/Context.idr delete mode 100644 src/Inky/Data/Context/Var.idr delete mode 100644 src/Inky/Data/List.idr delete mode 100644 src/Inky/Data/SnocList.idr delete mode 100644 src/Inky/Data/SnocList/Elem.idr delete mode 100644 src/Inky/Data/SnocList/Quantifiers.idr delete mode 100644 src/Inky/Data/SnocList/Thinning.idr delete mode 100644 src/Inky/Data/SnocList/Var.idr delete mode 100644 src/Inky/Decidable.idr delete mode 100644 src/Inky/Decidable/Either.idr delete mode 100644 src/Inky/Decidable/Maybe.idr delete mode 100644 src/Inky/Parser.idr create mode 100644 src/Inky/Term/Compile.idr create mode 100644 src/Inky/Term/Recompute.idr create mode 100644 src/Inky/Type/Substitution.idr (limited to 'src/Inky') diff --git a/src/Inky/Data/Assoc.idr b/src/Inky/Data/Assoc.idr deleted file mode 100644 index 0818ba3..0000000 --- a/src/Inky/Data/Assoc.idr +++ /dev/null @@ -1,38 +0,0 @@ -module Inky.Data.Assoc - -export -infix 2 :- - -public export -record Assoc (a : Type) where - constructor (:-) - name : String - value : a - -public export -Functor Assoc where - map f x = x.name :- f x.value - -namespace Irrelevant - public export - record Assoc0 (0 a : Type) (n : String) where - constructor (:-) - 0 name : String - {auto 0 prf : n = name} - value : a - - public export - map : (a -> b) -> Assoc0 a n -> Assoc0 b n - map f (n :- x) = n :- f x - -namespace Contexts - public export - record Assoc0 (0 p : a -> Type) (x : Assoc a) where - constructor (:-) - 0 name : String - {auto 0 prf : x.name = name} - value : p x.value - - public export - map : (forall x. p x -> q x) -> forall x. Assoc0 p x -> Assoc0 q x - map f (n :- px) = n :- f px diff --git a/src/Inky/Data/Context.idr b/src/Inky/Data/Context.idr deleted file mode 100644 index 4c5f6cf..0000000 --- a/src/Inky/Data/Context.idr +++ /dev/null @@ -1,34 +0,0 @@ -module Inky.Data.Context - -import public Inky.Data.Assoc -import public Inky.Data.SnocList - -import Inky.Data.SnocList.Quantifiers - --- Contexts -------------------------------------------------------------------- - -public export -Context : Type -> Type -Context a = SnocList (Assoc a) - -public export -(.names) : Context a -> SnocList String -[<].names = [<] -(ctx :< nx).names = ctx.names :< nx.name - -export -mapNames : (0 f : a -> b) -> (ctx : Context a) -> (map (map f) ctx).names = ctx.names -mapNames f [<] = Refl -mapNames f (ctx :< nx) = cong (:< nx.name) $ mapNames f ctx - --- Construction ---------------------------------------------------------------- - -public export -fromAll : {sx : SnocList String} -> All (Assoc0 a) sx -> Context a -fromAll [<] = [<] -fromAll {sx = sx :< n} (ctx :< (_ :- x)) = fromAll ctx :< (n :- x) - -export -fromAllNames : {sx : SnocList String} -> (ctx : All (Assoc0 a) sx) -> (fromAll ctx).names = sx -fromAllNames [<] = Refl -fromAllNames {sx = sx :< n} (ctx :< (k :- x)) = cong (:< n) $ fromAllNames ctx diff --git a/src/Inky/Data/Context/Var.idr b/src/Inky/Data/Context/Var.idr deleted file mode 100644 index 4741580..0000000 --- a/src/Inky/Data/Context/Var.idr +++ /dev/null @@ -1,117 +0,0 @@ -module Inky.Data.Context.Var - -import Data.DPair -import Data.Singleton -import Inky.Data.Context -import Inky.Data.SnocList.Elem -import Inky.Decidable -import Inky.Decidable.Maybe - -export -prefix 2 %%, %%% - -public export -record Var (ctx : Context a) (x : a) where - constructor (%%) - 0 name : String - {auto pos : Elem (name :- x) ctx} - -%name Var i, j, k - -public export -toVar : Elem (n :- x) ctx -> Var ctx x -toVar pos = (%%) n {pos} - -public export -ThereVar : Var ctx x -> Var (ctx :< ny) x -ThereVar i = toVar (There i.pos) - -export -Show (Var ctx x) where - show i = show (elemToNat i.pos) - --- Basic Properties --------------------------------------------------------- - -export -toVarCong : - {0 n, k : String} -> {0 x, y : a} -> - {0 i : Elem (n :- x) ctx} -> {0 j : Elem (k :- y) ctx} -> - i ~=~ j -> toVar i ~=~ toVar j -toVarCong Refl = Refl - -export -posCong : {0 i : Var ctx x} -> {0 j : Var ctx y} -> i = j -> i.pos ~=~ j.pos -posCong Refl = Refl - -export -toVarInjective : - {0 n, k : String} -> {0 x, y : a} -> - {i : Elem (n :- x) ctx} -> {j : Elem (k :- y) ctx} -> - (0 _ : toVar i ~=~ toVar j) -> i ~=~ j -toVarInjective prf = toNatInjective $ toNatCong $ posCong prf - -export -posInjective : {i : Var ctx x} -> {j : Var ctx y} -> (0 _ : i.pos ~=~ j.pos) -> i ~=~ j -posInjective {i = %% x} {j = %% y} prf = irrelevantEq $ toVarCong prf - --- Decidable Equality ---------------------------------------------------------- - -public export -decEq : (i : Var ctx x) -> (j : Var ctx y) -> Dec' (i ~=~ j) -decEq i j = - mapDec (\prf => irrelevantEq $ posInjective prf) posCong $ - decEq i.pos j.pos - --- Weakening ------------------------------------------------------------------- - -public export -wknL : (len : LengthOf ctx2) => Var ctx1 x -> Var (ctx1 ++ ctx2) x -wknL i = toVar $ wknL i.pos len - -public export -wknR : Var ctx1 x -> Var (ctx2 ++ ctx1) x -wknR i = toVar $ wknR i.pos - -public export -split : {auto len : LengthOf ctx2} -> Var (ctx1 ++ ctx2) x -> Either (Var ctx1 x) (Var ctx2 x) -split i = bimap toVar toVar $ split len i.pos - -public export -lift : - {auto len : LengthOf ctx3} -> - (forall x. Var ctx1 x -> Var ctx2 x) -> - Var (ctx1 ++ ctx3) x -> Var (ctx2 ++ ctx3) x -lift f = either (wknL {len} . f) wknR . split {len} - --- Names ----------------------------------------------------------------------- - -export -nameOf : {ctx : Context a} -> (i : Var ctx x) -> Singleton i.name -nameOf i = [| (nameOf i.pos).name |] - --- Search ---------------------------------------------------------------------- - -export -lookup : (n : String) -> (ctx : Context a) -> Maybe (x ** Var ctx x) -lookup n ctx = - case decLookup n ctx of - Just x `Because` pos => Just (x ** toVar pos) - Nothing `Because` _ => Nothing - -namespace Search - public export - data VarPos : String -> a -> (ctx : Context a) -> Type where - [search ctx] - Here : VarPos n x (ctx :< (n :- x)) - There : VarPos n x ctx -> VarPos n x (ctx :< ky) - - %name VarPos pos - - public export - toElem : VarPos n x ctx -> Elem (n :- x) ctx - toElem Here = Here - toElem (There pos) = There (toElem pos) - - public export - (%%%) : (0 n : String) -> {auto pos : VarPos n x ctx} -> Var ctx x - (%%%) n {pos} = toVar $ toElem pos diff --git a/src/Inky/Data/Fun.idr b/src/Inky/Data/Fun.idr index d9acb7d..390745a 100644 --- a/src/Inky/Data/Fun.idr +++ b/src/Inky/Data/Fun.idr @@ -1,7 +1,7 @@ module Inky.Data.Fun -import public Inky.Data.SnocList.Quantifiers -import Inky.Data.SnocList +import public Flap.Data.SnocList.Quantifiers +import Flap.Data.SnocList public export Fun : SnocList Type -> Type -> Type diff --git a/src/Inky/Data/List.idr b/src/Inky/Data/List.idr deleted file mode 100644 index 24cb9c0..0000000 --- a/src/Inky/Data/List.idr +++ /dev/null @@ -1,13 +0,0 @@ -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 42f18da..8362770 100644 --- a/src/Inky/Data/Row.idr +++ b/src/Inky/Data/Row.idr @@ -1,11 +1,12 @@ module Inky.Data.Row import public Data.So -import public Inky.Data.Context -import public Inky.Data.SnocList.Quantifiers +import public Flap.Data.Context +import public Flap.Data.SnocList.Quantifiers -import Inky.Data.SnocList.Elem -import Inky.Decidable +import Data.Singleton +import Flap.Data.SnocList.Elem +import Flap.Decidable public export FreshIn : String -> SnocList String -> Type @@ -154,6 +155,33 @@ lookupUnique : the (x ** Elem (n :- x) row.context) (x ** i) = (y ** j) lookupUnique row i j = doLookupUnique row.context row.fresh i j +notHere : + {0 ctx : Context a} -> + (i : Elem (n :- x) (ctx :< (l :- y))) -> + Not (n = l) -> (j : Elem (n :- x) ctx ** i = There j) +notHere Here neq = void $ neq Refl +notHere (There i) _ = (i ** Refl) + +doLookupRecompute : + (ctx : Context a) -> (0 fresh : AllFresh ctx.names) -> + {n : String} -> (0 i : Elem (n :- x) ctx) -> Singleton i +doLookupRecompute [<] [<] i = void $ absurd i +doLookupRecompute (ctx :< (l :- x)) (fresh :< freshIn) i with (decEq n l) + doLookupRecompute (ctx :< (l :- x)) (fresh :< freshIn) i | True `Because` Refl = + replace {p = \x => Singleton x.snd} + (doLookupUnique (ctx :< (l :- x)) (fresh :< freshIn) Here i) + (Val Here) + _ | False `Because` contra = + let 0 jeq = notHere i contra in + rewrite snd jeq in + [| There $ doLookupRecompute ctx fresh (fst jeq) |] + +export +lookupRecompute : + (row : Row a) -> {n : String} -> + (0 i : Elem (n :- x) row.context) -> Singleton i +lookupRecompute row i = doLookupRecompute row.context row.fresh i + -- Removal --------------------------------------------------------------------- dropElemFreshIn : diff --git a/src/Inky/Data/SnocList.idr b/src/Inky/Data/SnocList.idr deleted file mode 100644 index 494e8cc..0000000 --- a/src/Inky/Data/SnocList.idr +++ /dev/null @@ -1,43 +0,0 @@ -module Inky.Data.SnocList - -import public Data.SnocList -import public Data.SnocList.Operations - -import Inky.Decidable.Maybe - -public export -data LengthOf : SnocList a -> Type where - Z : LengthOf [<] - S : LengthOf sx -> LengthOf (sx :< x) - -%name LengthOf len - -public export -lengthOfAppend : LengthOf sx -> LengthOf sy -> LengthOf (sx ++ sy) -lengthOfAppend len1 Z = len1 -lengthOfAppend len1 (S len2) = S (lengthOfAppend len1 len2) - -public export -lengthOf : (sx : SnocList a) -> LengthOf sx -lengthOf [<] = Z -lengthOf (sx :< x) = S (lengthOf sx) - -export -lengthUnique : (len1, len2 : LengthOf sx) -> len1 = len2 -lengthUnique Z Z = Refl -lengthUnique (S len1) (S len2) = cong S $ lengthUnique len1 len2 - -export -isSnoc : (sx : SnocList a) -> Proof (SnocList a, a) (\syy => sx = fst syy :< snd syy) (sx = [<]) -isSnoc [<] = Nothing `Because` Refl -isSnoc (sx :< x) = Just (sx, x) `Because` Refl - -public export -replicate : Nat -> a -> SnocList a -replicate 0 x = [<] -replicate (S n) x = replicate n x :< x - -public export -lengthOfReplicate : (n : Nat) -> (0 x : a) -> LengthOf (replicate n x) -lengthOfReplicate 0 x = Z -lengthOfReplicate (S k) x = S (lengthOfReplicate k x) diff --git a/src/Inky/Data/SnocList/Elem.idr b/src/Inky/Data/SnocList/Elem.idr deleted file mode 100644 index c1e69f6..0000000 --- a/src/Inky/Data/SnocList/Elem.idr +++ /dev/null @@ -1,116 +0,0 @@ -module Inky.Data.SnocList.Elem - -import public Data.SnocList.Elem - -import Data.DPair -import Data.Nat -import Data.Singleton -import Inky.Decidable -import Inky.Decidable.Maybe -import Inky.Data.Assoc -import Inky.Data.List -import Inky.Data.SnocList - -export -Uninhabited (Here {sx, x} ~=~ There {sx = sy, x = z, y} i) where - uninhabited Refl impossible - -export -Uninhabited (There {sx = sy, x = z, y} i ~=~ Here {sx, x}) where - uninhabited Refl impossible - -export -thereCong : - {0 i : Elem x sx} -> {0 j : Elem y sx} -> i = j -> - There {y = z} i = There {y = z} j -thereCong Refl = Refl - -export -toNatCong : {0 i : Elem x sx} -> {0 j : Elem y sx} -> i = j -> elemToNat i = elemToNat j -toNatCong Refl = Refl - -export -thereInjective : - {0 i : Elem x sx} -> {0 j : Elem y sx} -> There {y = z} i = There {y = z} j -> - i = j -thereInjective Refl = Refl - -export -toNatInjective : {i : Elem x sx} -> {j : Elem y sx} -> (0 _ : elemToNat i = elemToNat j) -> i = j -toNatInjective {i = Here} {j = Here} prf = Refl -toNatInjective {i = There i} {j = There j} prf with (toNatInjective {i} {j} $ injective prf) - toNatInjective {i = There i} {j = There .(i)} prf | Refl = Refl - --- Decidable Equality ----------------------------------------------------------- - -public export -reflectEq : (i : Elem x sx) -> (j : Elem y sx) -> (i = j) `When` (elemToNat i == elemToNat j) -reflectEq Here Here = Refl -reflectEq Here (There j) = absurd -reflectEq (There i) Here = absurd -reflectEq (There i) (There j) = mapWhen thereCong thereInjective $ reflectEq i j - -public export -decEq : (i : Elem x sx) -> (j : Elem y sx) -> Dec' (i = j) -decEq i j = (elemToNat i == elemToNat j) `Because` reflectEq i j - --- Weakening ------------------------------------------------------------------- - -public export -wknL : Elem x sx -> LengthOf sy -> Elem x (sx ++ sy) -wknL pos Z = pos -wknL pos (S len) = There (wknL pos len) - -public export -wknR : Elem x sx -> Elem x (sy ++ sx) -wknR Here = Here -wknR (There pos) = There (wknR pos) - -public export -split : LengthOf sy -> Elem x (sx ++ sy) -> Either (Elem x sx) (Elem x sy) -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 -nameOf : {sx : SnocList a} -> Elem x sx -> Singleton x -nameOf Here = Val x -nameOf (There pos) = nameOf pos - --- Search ---------------------------------------------------------------------- - -export -lookup : DecEq' a => (x : a) -> (sx : SnocList a) -> Maybe (Elem x sx) -lookup x [<] = Nothing -lookup x (sx :< y) = - case decEq x y of - True `Because` Refl => Just Here - False `Because` _ => There <$> lookup x sx - -public export -decLookup : (n : String) -> (sx : SnocList (Assoc a)) -> DecWhen a (\x => Elem (n :- x) sx) -decLookup n [<] = Nothing `Because` (\_ => absurd) -decLookup n (sx :< (k :- x)) = - map (maybe x id) leftToRight rightToLeft $ - first (decEq n k) (decLookup n sx) - where - leftToRight : - forall n. (m : Maybe a) -> - maybe (n = k) (\y => Elem (n :- y) sx) m -> - Elem (n :- maybe x Basics.id m) (sx :< (k :- x)) - leftToRight Nothing Refl = Here - leftToRight (Just _) prf = There prf - - rightToLeft : - forall n. - (Not (n = k), (y : a) -> Not (Elem (n :- y) sx)) -> - (y : a) -> Not (Elem (n :- y) (sx :< (k :- x))) - rightToLeft (neq, contra) _ Here = neq Refl - rightToLeft (neq, contra) y (There i) = contra y i diff --git a/src/Inky/Data/SnocList/Quantifiers.idr b/src/Inky/Data/SnocList/Quantifiers.idr deleted file mode 100644 index 886c4e4..0000000 --- a/src/Inky/Data/SnocList/Quantifiers.idr +++ /dev/null @@ -1,44 +0,0 @@ -module Inky.Data.SnocList.Quantifiers - -import public Data.SnocList.Quantifiers - -import Data.List.Quantifiers -import Inky.Data.SnocList -import Inky.Data.SnocList.Elem -import Inky.Decidable - -public export -(<><) : All p xs -> All p sx -> All p (xs <>< sx) -sxp <>< [] = sxp -sxp <>< (px :: pxs) = (sxp :< px) <>< pxs - -public export -head : All p (sx :< x) -> p x -head (prfs :< px) = px - -public export -tail : All p (sx :< x) -> All p sx -tail (prfs :< px) = prfs - -public export -HSnocList : SnocList Type -> Type -HSnocList = All id - -public export -all : - ((x : a) -> LazyEither (p x) (q x)) -> - (sx : SnocList a) -> LazyEither (All p sx) (Any q sx) -all f [<] = True `Because` [<] -all f (sx :< x) = - map (\prfs => snd prfs :< fst prfs) (either Here There) $ - both (f x) (all f sx) - -public export -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 deleted file mode 100644 index 60666d2..0000000 --- a/src/Inky/Data/SnocList/Thinning.idr +++ /dev/null @@ -1,228 +0,0 @@ -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 -import Inky.Decidable.Maybe - --------------------------------------------------------------------------------- --- Thinnings ------------------------------------------------------------------- --------------------------------------------------------------------------------- - -public export -data Thins : SnocList a -> SnocList a -> Type where - Id : sx `Thins` sx - Drop : sx `Thins` sy -> sx `Thins` sy :< x - Keep : sx `Thins` sy -> sx :< x `Thins` sy :< x - -%name Thins f, g, h - --- Basics - -public export -indexPos : (f : sx `Thins` sy) -> (pos : Elem x sx) -> Elem x sy -indexPos Id pos = pos -indexPos (Drop f) pos = There (indexPos f pos) -indexPos (Keep f) Here = Here -indexPos (Keep f) (There pos) = There (indexPos f pos) - -public export -index : (f : sx `Thins` sy) -> Var sx -> Var sy -index f i = toVar (indexPos f i.pos) - -public export -(.) : sy `Thins` sz -> sx `Thins` sy -> sx `Thins` sz -Id . g = g -Drop f . g = Drop (f . g) -Keep f . Id = Keep f -Keep f . Drop g = Drop (f . g) -Keep f . Keep g = Keep (f . g) - --- Basic properties - -export -indexPosInjective : - (f : sx `Thins` sy) -> {i : Elem x sx} -> {j : Elem y sx} -> - (0 _ : elemToNat (indexPos f i) = elemToNat (indexPos f j)) -> i = j -indexPosInjective Id prf = toNatInjective prf -indexPosInjective (Drop f) prf = indexPosInjective f (injective prf) -indexPosInjective (Keep f) {i = Here} {j = Here} prf = Refl -indexPosInjective (Keep f) {i = There i} {j = There j} prf = - thereCong (indexPosInjective f $ injective prf) - -export -indexPosComp : - (f : sy `Thins` sz) -> (g : sx `Thins` sy) -> (pos : Elem x sx) -> - indexPos (f . g) pos = indexPos f (indexPos g pos) -indexPosComp Id g pos = Refl -indexPosComp (Drop f) g pos = cong There (indexPosComp f g pos) -indexPosComp (Keep f) Id pos = Refl -indexPosComp (Keep f) (Drop g) pos = cong There (indexPosComp f g pos) -indexPosComp (Keep f) (Keep g) Here = Refl -indexPosComp (Keep f) (Keep g) (There pos) = cong There (indexPosComp f g pos) - --- Congruence ------------------------------------------------------------------ - -export -infix 6 ~~~ - -public export -data (~~~) : sx `Thins` sy -> sx `Thins` sz -> Type where - IdId : Id ~~~ Id - IdKeep : Id ~~~ f -> Id ~~~ Keep f - KeepId : f ~~~ Id -> Keep f ~~~ Id - DropDrop : f ~~~ g -> Drop f ~~~ Drop g - KeepKeep : f ~~~ g -> Keep f ~~~ Keep g - -%name Thinning.(~~~) prf - -export -(.indexPos) : f ~~~ g -> (pos : Elem x sx) -> elemToNat (indexPos f pos) = elemToNat (indexPos g pos) -(IdId).indexPos pos = Refl -(IdKeep prf).indexPos Here = Refl -(IdKeep prf).indexPos (There pos) = cong S $ prf.indexPos pos -(KeepId prf).indexPos Here = Refl -(KeepId prf).indexPos (There pos) = cong S $ prf.indexPos pos -(DropDrop prf).indexPos pos = cong S $ prf.indexPos pos -(KeepKeep prf).indexPos Here = Refl -(KeepKeep prf).indexPos (There pos) = cong S $ prf.indexPos pos - -export -(.index) : - {0 f, g : sx `Thins` sy} -> f ~~~ g -> (i : Var sx) -> index f i = index g i -prf.index ((%%) n {pos}) = irrelevantEq $ toVarCong $ toNatInjective $ prf.indexPos pos - --- 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) - -public export -dropAll : LengthOf sy -> sx `Thins` sx ++ sy -dropAll Z = Id -dropAll (S len) = Drop (dropAll len) - -public export -keepAll : LengthOf sz -> sx `Thins` sy -> sx ++ sz `Thins` sy ++ sz -keepAll Z f = f -keepAll (S len) f = Keep (keepAll len f) - -public export -append : - sx `Thins` sz -> sy `Thins` sw -> - {auto len : LengthOf sw} -> - sx ++ sy `Thins` sz ++ sw -append f Id = keepAll len f -append f (Drop g) {len = S len} = Drop (append f g) -append f (Keep g) {len = S len} = Keep (append f g) - -public export -assoc : LengthOf sz -> sx ++ (sy ++ sz) `Thins` (sx ++ sy) ++ sz -assoc Z = Id -assoc (S len) = Keep (assoc len) - -public export -growLengthOf : sx `Thins` sy -> LengthOf sx -> LengthOf sy -growLengthOf Id len = len -growLengthOf (Drop f) len = S (growLengthOf f len) -growLengthOf (Keep f) (S len) = S (growLengthOf f len) - -public export -thinLengthOf : sx `Thins` sy -> LengthOf sy -> LengthOf sx -thinLengthOf Id len = len -thinLengthOf (Drop f) (S len) = thinLengthOf f len -thinLengthOf (Keep f) (S len) = S (thinLengthOf f len) - -public export -thinAll : sx `Thins` sy -> All p sy -> All p sx -thinAll Id env = env -thinAll (Drop f) (env :< px) = thinAll f env -thinAll (Keep f) (env :< px) = thinAll f env :< px - -public export -splitL : - {0 sx, sy, sz : SnocList a} -> - LengthOf sz -> - sx `Thins` sy ++ sz -> - Exists (\sxA => Exists (\sxB => (sx = sxA ++ sxB, sxA `Thins` sy, sxB `Thins` sz))) -splitL Z f = Evidence sx (Evidence [<] (Refl, f, Id)) -splitL (S len) Id = Evidence sy (Evidence sz (Refl, Id, Id)) -splitL (S len) (Drop f) = - let Evidence sxA (Evidence sxB (Refl, g, h)) = splitL len f in - Evidence sxA (Evidence sxB (Refl, g, Drop h)) -splitL (S len) (Keep f) = - let Evidence sxA (Evidence sxB (Refl, g, h)) = splitL len f in - Evidence sxA (Evidence (sxB :< _) (Refl, g, Keep h)) - -public export -splitR : - {0 sx, sy, sz : SnocList a} -> - LengthOf sy -> - sx ++ sy `Thins` sz -> - Exists (\sxA => Exists (\sxB => (sz = sxA ++ sxB, sx `Thins` sxA, sy `Thins` sxB))) -splitR Z f = Evidence sz (Evidence [<] (Refl, f, Id)) -splitR (S len) Id = Evidence sx (Evidence sy (Refl, Id, Id)) -splitR (S len) (Drop f) = - let Evidence sxA (Evidence sxB (Refl, g, h)) = splitR (S len) f in - Evidence sxA (Evidence (sxB :< _) (Refl, g, Drop h)) -splitR (S len) (Keep f) = - let Evidence sxA (Evidence sxB (Refl, g, h)) = splitR len f in - Evidence sxA (Evidence (sxB :< _) (Refl, g, Keep h)) - --- Strengthening --------------------------------------------------------------- - -public export -data Skips : sx `Thins` sy -> Elem y sy -> Type where - Here : Drop f `Skips` Here - Also : f `Skips` i -> Drop f `Skips` There i - There : f `Skips` i -> Keep f `Skips` There i - -%name Skips skips - -public export -strengthen : - (f : sx `Thins` sy) -> (i : Elem y sy) -> - Proof (Elem y sx) (\j => i = indexPos f j) (f `Skips` i) -strengthen Id i = Just i `Because` Refl -strengthen (Drop f) Here = Nothing `Because` Here -strengthen (Drop f) (There i) = - map id (\_, prf => cong There prf) Also $ - strengthen f i -strengthen (Keep f) Here = Just Here `Because` Refl -strengthen (Keep f) (There i) = - map There (\_, prf => cong There prf) There $ - strengthen f i - -export -skipsDropPos : (i : Elem x sx) -> dropPos i `Skips` j -> i ~=~ j -skipsDropPos Here Here = Refl -skipsDropPos (There i) (There skips) = thereCong (skipsDropPos i skips) - ------------------------- ------------------------------------------------------- --- Renaming Coalgebras --------------------------------------------------------- --------------------------------------------------------------------------------- - -public export -interface Rename (0 a : Type) (0 t : SnocList a -> Type) where - rename : - {0 sx, sy : SnocList a} -> sx `Thins` sy -> - t sx -> t sy - 0 renameCong : - {0 sx, sy : SnocList a} -> {0 f, g : sx `Thins` sy} -> f ~~~ g -> - (x : t sx) -> rename f x = rename g x - 0 renameId : {0 sx : SnocList a} -> (x : t sx) -> rename Id x = x diff --git a/src/Inky/Data/SnocList/Var.idr b/src/Inky/Data/SnocList/Var.idr deleted file mode 100644 index cc7c088..0000000 --- a/src/Inky/Data/SnocList/Var.idr +++ /dev/null @@ -1,90 +0,0 @@ -module Inky.Data.SnocList.Var - -import public Inky.Data.SnocList.Elem - -import Data.Singleton -import Inky.Data.SnocList -import Inky.Decidable - -export -prefix 2 %% - -public export -record Var (sx : SnocList a) where - constructor (%%) - 0 name : a - {auto pos : Elem name sx} - -%name Var i, j, k - -public export -toVar : Elem x sx -> Var sx -toVar pos = (%%) x {pos} - -public export -ThereVar : Var sx -> Var (sx :< x) -ThereVar i = toVar (There i.pos) - -export -Show (Var sx) where - show i = show (elemToNat i.pos) - --- Basic Properties --------------------------------------------------------- - -export -toVarCong : {0 i : Elem x sx} -> {0 j : Elem y sx} -> i = j -> toVar i = toVar j -toVarCong Refl = Refl - -export -posCong : {0 i, j : Var sx} -> i = j -> i.pos ~=~ j.pos -posCong Refl = Refl - -export -toVarInjective : {i : Elem x sx} -> {j : Elem y sx} -> (0 _ : toVar i = toVar j) -> i = j -toVarInjective prf = toNatInjective $ toNatCong $ posCong prf - -export -posInjective : {i : Var sx} -> {j : Var sx} -> (0 _ : i.pos ~=~ j.pos) -> i = j -posInjective {i = %% x} {j = %% y} prf = irrelevantEq $ toVarCong prf - --- Decidable Equality ---------------------------------------------------------- - -public export -DecEq' (Var {a} sx) where - does i j = (decEq i.pos j.pos).does - reason i j = - mapWhen (\prf => irrelevantEq $ posInjective prf) posCong $ - (decEq i.pos j.pos).reason - --- Weakening ------------------------------------------------------------------- - -public export -wknL : (len : LengthOf sy) => Var sx -> Var (sx ++ sy) -wknL i = toVar $ wknL i.pos len - -public export -wknR : Var sx -> Var (sy ++ sx) -wknR i = toVar $ wknR i.pos - -public export -split : {auto len : LengthOf sy} -> Var (sx ++ sy) -> Either (Var sx) (Var sy) -split i = bimap toVar toVar $ split len i.pos - -public export -lift1 : - (Var sx -> Var sy) -> - Var (sx :< x) -> Var (sy :< y) -lift1 f ((%%) x {pos = Here}) = %% y -lift1 f ((%%) name {pos = There i}) = ThereVar (f $ %% name) - --- Names ----------------------------------------------------------------------- - -export -nameOf : {sx : SnocList a} -> (i : Var sx) -> Singleton i.name -nameOf i = nameOf i.pos - --- Search ---------------------------------------------------------------------- - -export -lookup : DecEq' a => (x : a) -> (sx : SnocList a) -> Maybe (Var sx) -lookup x sx = toVar <$> lookup x sx diff --git a/src/Inky/Data/Thinned.idr b/src/Inky/Data/Thinned.idr index 6ee0d50..eaf5e7b 100644 --- a/src/Inky/Data/Thinned.idr +++ b/src/Inky/Data/Thinned.idr @@ -1,6 +1,6 @@ module Inky.Data.Thinned -import public Inky.Data.SnocList.Thinning +import public Flap.Data.SnocList.Thinning public export record Thinned (0 p : SnocList a -> Type) (ctx : SnocList a) where @@ -11,8 +11,15 @@ record Thinned (0 p : SnocList a -> Type) (ctx : SnocList a) where public export rename : (ctx1 `Thins` ctx2) -> Thinned p ctx1 -> Thinned p ctx2 -rename f (value `Over` thins) = value `Over` (f . thins) +rename f v = v.value `Over` (f . v.thins) public export (.extract) : Rename a p => Thinned p ctx -> p ctx -(value `Over` thins).extract = rename thins value +v.extract = rename v.thins v.value + +export +0 extractHomo : + Rename a p => + (f : ctx1 `Thins` ctx2) -> (x : Thinned p ctx1) -> + rename f x.extract = (rename f x).extract +extractHomo f x = renameHomo f x.thins x.value diff --git a/src/Inky/Decidable.idr b/src/Inky/Decidable.idr deleted file mode 100644 index 7fba676..0000000 --- a/src/Inky/Decidable.idr +++ /dev/null @@ -1,261 +0,0 @@ -module Inky.Decidable - -import public Inky.Decidable.Either - -import Data.Bool -import Data.Either -import Data.Maybe -import Data.List -import Data.List1 -import Data.List1.Properties -import Data.Nat -import Data.SnocList -import Data.So -import Data.These -import Data.Vect - -import Decidable.Equality - -public export -When : Type -> Bool -> Type -When a = Union a (Not a) - -public export -Dec' : (0 _ : Type) -> Type -Dec' a = LazyEither a (Not a) - --- Operations ------------------------------------------------------------------ - --- Conversion to Dec - -public export -fromDec : Dec a -> Dec' a -fromDec (Yes prf) = True `Because` prf -fromDec (No contra) = False `Because` contra - -public export -toDec : Dec' a -> Dec a -toDec (True `Because` prf) = Yes prf -toDec (False `Because` contra) = No contra - --- Negation - -public export -notWhen : {b : Bool} -> a `When` b -> Not a `When` not b -notWhen = Union.map id (\prf, contra => contra prf) . Union.not - -public export -notDec : Dec' a -> Dec' (Not a) -notDec p = not p.does `Because` notWhen p.reason - --- Maps - -public export -mapWhen : (a -> a') -> (0 _ : a' -> a) -> {b : Bool} -> a `When` b -> a' `When` b -mapWhen f g = Union.map f (\contra, prf => void $ contra $ g prf) - -public export -mapDec : (a -> b) -> (0 _ : b -> a) -> Dec' a -> Dec' b -mapDec f g = map f (\contra, prf => void $ contra $ g prf) - --- Conjunction - -public export -andWhen : {b1, b2 : Bool} -> a1 `When` b1 -> Lazy (a2 `When` b2) -> (a1, a2) `When` (b1 && b2) -andWhen x y = - Union.map {d = Not (a1, a2)} id (\x, (y, z) => either (\f => f y) (\g => g z) x) $ - Union.both x y - -public export -andDec : Dec' a -> Dec' b -> Dec' (a, b) -andDec p q = (p.does && q.does) `Because` andWhen p.reason q.reason - --- Disjunction - -public export -elseWhen : {b1, b2 : Bool} -> a1 `When` b1 -> Lazy (a2 `When` b2) -> Either a1 a2 `When` (b1 || b2) -elseWhen x y = - Union.map {b = (Not a1, Not a2)} id (\(f, g) => either f g) $ - Union.first x y - -public export -elseDec : Dec' a -> Dec' b -> Dec' (Either a b) -elseDec p q = (p.does || q.does) `Because` elseWhen p.reason q.reason - -public export -orWhen : {b1, b2 : Bool} -> a1 `When` b1 -> a2 `When` b2 -> These a1 a2 `When` (b1 || b2) -orWhen x y = - Union.map {b = (Not a1, Not a2)} id (\(f, g) => these f g (const g)) $ - Union.any x y - -public export -orDec : Dec' a -> Dec' b -> Dec' (These a b) -orDec p q = (p.does || q.does) `Because` orWhen p.reason q.reason - --- Dependent Versions - -public export -thenDec : - (0 b : a -> Type) -> - (0 unique : (x, y : a) -> b x -> b y) -> - Dec' a -> ((x : a) -> Dec' (b x)) -> Dec' (x ** b x) -thenDec b unique p f = - map id - (\contra, (x ** prf) => - either - (\contra => contra x) - (\yContra => void $ snd yContra $ unique x (fst yContra) prf) - contra) $ - andThen p f - --- Equality -------------------------------------------------------------------- - -public export -interface DecEq' (0 a : Type) where - does : (x, y : a) -> Bool - reason : (x, y : a) -> (x = y) `When` (does x y) - - decEq : (x, y : a) -> Dec' (x = y) - decEq x y = does x y `Because` reason x y - -public export -whenCong : (0 _ : Injective f) => {b : Bool} -> (x = y) `When` b -> (f x = f y) `When` b -whenCong = mapWhen (\prf => cong f prf) (\prf => inj f prf) - -public export -whenCong2 : - (0 _ : Biinjective f) => - {b1, b2 : Bool} -> - (x = y) `When` b1 -> (z = w) `When` b2 -> - (f x z = f y w) `When` (b1 && b2) -whenCong2 p q = - mapWhen {a = (_, _)} (\prfs => cong2 f (fst prfs) (snd prfs)) (\prf => biinj f prf) $ - andWhen p q - -[ToEq] DecEq' a => Eq a where - x == y = does x y - --- Instances ------------------------------------------------------------------- - -public export -DecEq' () where - does _ _ = True - reason () () = Refl - -public export -DecEq' Bool where - does b1 b2 = b1 == b2 - - reason False False = Refl - reason False True = absurd - reason True False = absurd - reason True True = Refl - -public export -DecEq' Nat where - does k n = k == n - - reason 0 0 = Refl - reason 0 (S n) = absurd - reason (S k) 0 = absurd - reason (S k) (S n) = whenCong (reason k n) - -public export -(d : DecEq' a) => DecEq' (Maybe a) where - does x y = let _ = ToEq @{d} in x == y - - reason Nothing Nothing = Refl - reason Nothing (Just y) = absurd - reason (Just x) Nothing = absurd - reason (Just x) (Just y) = whenCong (reason x y) - -public export -(d1 : DecEq' a) => (d2 : DecEq' b) => DecEq' (Either a b) where - does x y = let _ = ToEq @{d1} in let _ = ToEq @{d2} in x == y - - reason (Left x) (Left y) = whenCong (reason x y) - reason (Left x) (Right y) = absurd - reason (Right x) (Left y) = absurd - reason (Right x) (Right y) = whenCong (reason x y) - - -public export -(d1 : DecEq' a) => (d2 : DecEq' b) => DecEq' (These a b) where - does x y = let _ = ToEq @{d1} in let _ = ToEq @{d2} in x == y - - reason (This x) (This y) = whenCong (reason x y) - reason (That x) (That y) = whenCong (reason x y) - reason (Both x z) (Both y w) = whenCong2 (reason x y) (reason z w) - reason (This x) (That y) = \case Refl impossible - reason (This x) (Both y z) = \case Refl impossible - reason (That x) (This y) = \case Refl impossible - reason (That x) (Both y z) = \case Refl impossible - reason (Both x z) (This y) = \case Refl impossible - reason (Both x z) (That y) = \case Refl impossible - -public export -(d1 : DecEq' a) => (d2 : DecEq' b) => DecEq' (a, b) where - does x y = let _ = ToEq @{d1} in let _ = ToEq @{d2} in x == y - - reason (x, y) (z, w) = whenCong2 (reason x z) (reason y w) - -public export -(d : DecEq' a) => DecEq' (List a) where - does x y = let _ = ToEq @{d} in x == y - - reason [] [] = Refl - reason [] (y :: ys) = absurd - reason (x :: xs) [] = absurd - reason (x :: xs) (y :: ys) = whenCong2 (reason x y) (reason xs ys) - -public export -(d : DecEq' a) => DecEq' (List1 a) where - does x y = let _ = ToEq @{d} in x == y - - reason (x ::: xs) (y ::: ys) = whenCong2 (reason x y) (reason xs ys) - -public export -(d : DecEq' a) => DecEq' (SnocList a) where - does x y = let _ = ToEq @{d} in x == y - - reason [<] [<] = Refl - reason [<] (sy :< y) = absurd - reason (sx :< x) [<] = absurd - reason (sx :< x) (sy :< y) = - rewrite sym $ andCommutative (does sx sy) (does x y) in - whenCong2 (reason sx sy) (reason x y) - --- Other Primitives - -%unsafe -public export -primitiveEq : Eq a => (x, y : a) -> (x = y) `When` (x == y) -primitiveEq x y with (x == y) - _ | True = believe_me (Refl {x}) - _ | False = \prf => believe_me {b = Void} () - -%unsafe -public export -[FromEq] Eq a => DecEq' a where - does x y = x == y - reason x y = primitiveEq x y - -public export -DecEq' Int where - does = does @{FromEq} - reason = reason @{FromEq} - -public export -DecEq' Char where - does = does @{FromEq} - reason = reason @{FromEq} - -public export -DecEq' Integer where - does = does @{FromEq} - reason = reason @{FromEq} - -public export -DecEq' String where - does = does @{FromEq} - reason = reason @{FromEq} diff --git a/src/Inky/Decidable/Either.idr b/src/Inky/Decidable/Either.idr deleted file mode 100644 index bea3364..0000000 --- a/src/Inky/Decidable/Either.idr +++ /dev/null @@ -1,111 +0,0 @@ -module Inky.Decidable.Either - -import Data.So -import Data.These - -public export -Union : Type -> Type -> Bool -> Type -Union a b False = b -Union a b True = a - -public export -record LazyEither (0 a, b : Type) where - constructor Because - does : Bool - reason : Lazy (Union a b does) - -%name LazyEither p, q - -namespace Union - public export - map : {tag : Bool} -> (a -> c) -> (b -> d) -> Union a b tag -> Union c d tag - map {tag = False} f g x = g x - map {tag = True} f g x = f x - - public export - not : {tag : Bool} -> Union a b tag -> Union b a (not tag) - not {tag = False} x = x - not {tag = True} x = x - - public export - both : - {tag1 : Bool} -> {tag2 : Lazy Bool} -> - Union a b tag1 -> Lazy (Union c d tag2) -> - Union (a, c) (Either b d) (tag1 && tag2) - both {tag1 = True, tag2 = True} x y = (x, y) - both {tag1 = True, tag2 = False} x y = Right y - both {tag1 = False} x y = Left x - - public export - first : - {tag1 : Bool} -> {tag2 : Lazy Bool} -> - Union a b tag1 -> Lazy (Union c d tag2) -> - Union (Either a c) (b, d) (tag1 || tag2) - first {tag1 = True} x y = Left x - first {tag1 = False, tag2 = True} x y = Right y - first {tag1 = False, tag2 = False} x y = (x, y) - - public export - all : - {tag1, tag2 : Bool} -> - Union a b tag1 -> Union c d tag2 -> - Union (a, c) (These b d) (tag1 && tag2) - all {tag1 = True, tag2 = True} x y = (x, y) - all {tag1 = True, tag2 = False} x y = That y - all {tag1 = False, tag2 = True} x y = This x - all {tag1 = False, tag2 = False} x y = Both x y - - public export - any : - {tag1, tag2 : Bool} -> - Union a b tag1 -> Union c d tag2 -> - Union (These a c) (b, d) (tag1 || tag2) - any {tag1 = True, tag2 = True} x y = Both x y - any {tag1 = True, tag2 = False} x y = This x - any {tag1 = False, tag2 = True} x y = That y - any {tag1 = False, tag2 = False} x y = (x, y) - -public export -map : (a -> c) -> (b -> d) -> LazyEither a b -> LazyEither c d -map f g p = p.does `Because` Union.map f g p.reason - -public export -not : LazyEither a b -> LazyEither b a -not p = not p.does `Because` Union.not p.reason - -public export -both : LazyEither a b -> Lazy (LazyEither c d) -> LazyEither (a, c) (Either b d) -both p q = p.does && q.does `Because` Union.both p.reason q.reason - -public export -first : LazyEither a b -> Lazy (LazyEither c d) -> LazyEither (Either a c) (b, d) -first p q = p.does || q.does `Because` Union.first p.reason q.reason - -public export -all : LazyEither a b -> Lazy (LazyEither c d) -> LazyEither (a, c) (These b d) -all p q = p.does && q.does `Because` Union.all p.reason q.reason - -public export -any : LazyEither a b -> Lazy (LazyEither c d) -> LazyEither (These a c) (b, d) -any p q = p.does || q.does `Because` Union.any p.reason q.reason - -public export -so : (b : Bool) -> LazyEither (So b) (So $ not b) -so b = b `Because` if b then Oh else Oh - -export autobind infixr 0 >=> - -public export -andThen : - {0 p, q : a -> Type} -> - LazyEither a b -> ((x : a) -> LazyEither (p x) (q x)) -> - LazyEither (x ** p x) (Either b (x ** q x)) -andThen (True `Because` x) f = map (\px => (x ** px)) (\qx => Right (x ** qx)) (f x) -andThen (False `Because` y) f = False `Because` (Left y) - -public export -(>=>) : - {0 p, q : a -> Type} -> - LazyEither a b -> ((x : a) -> LazyEither (p x) (q x)) -> - LazyEither (x ** p x) (Either b (x ** q x)) -(>=>) = andThen diff --git a/src/Inky/Decidable/Maybe.idr b/src/Inky/Decidable/Maybe.idr deleted file mode 100644 index 2f1d83c..0000000 --- a/src/Inky/Decidable/Maybe.idr +++ /dev/null @@ -1,146 +0,0 @@ -module Inky.Decidable.Maybe - -import Data.Maybe -import Data.These -import Inky.Decidable.Either - -public export -WhenJust : (a -> Type) -> Type -> Maybe a -> Type -WhenJust p b (Just x) = p x -WhenJust p b Nothing = b - -public export -record Proof (0 a : Type) (0 p : a -> Type) (0 b : Type) where - constructor Because - does : Maybe a - reason : WhenJust p b does - -%name Proof p, q - -public export -DecWhen : (0 a : Type) -> (0 p : a -> Type) -> Type -DecWhen a p = Proof a p ((x : a) -> Not (p x)) - --- Operations ------------------------------------------------------------------ - -public export -(.forget) : Proof a p b -> LazyEither (x ** p x) b -(Just x `Because` px).forget = True `Because` (x ** px) -(Nothing `Because` y).forget = False `Because` y - -public export -map : - (f : a -> a') -> - ((x : a) -> p x -> q (f x)) -> - (b -> b') -> - Proof a p b -> Proof a' q b' -map f g h (Just x `Because` px) = Just (f x) `Because` g x px -map f g h (Nothing `Because` y) = Nothing `Because` h y - -export autobind infixr 0 >=> - -public export -andThen : - {0 q : a -> a' -> Type} -> - {0 b' : a -> Type} -> - Proof a p b -> - ((x : a) -> Proof a' (q x) (b' x)) -> - Proof (a, a') (\xy => (p (fst xy), uncurry q xy)) (Either b (x ** (p x, b' x))) -andThen (Just x `Because` px) f = map (x,) (\_ => (px,)) (\y => Right (x ** (px, y))) $ f x -andThen (Nothing `Because` y) f = Nothing `Because` Left y - -public export -(>=>) : - {0 q : a -> a' -> Type} -> - {0 b' : a -> Type} -> - Proof a p b -> - ((x : a) -> Proof a' (q x) (b' x)) -> - Proof (a, a') (\xy => (p (fst xy), uncurry q xy)) (Either b (x ** (p x, b' x))) -(>=>) = andThen - -public export -andThen' : - {0 a' : a -> Type} -> - {0 q : (x : a) -> a' x -> Type} -> - {0 b' : a -> Type} -> - Proof a p b -> - ((x : a) -> Proof (a' x) (q x) (b' x)) -> - Proof (x ** a' x) (\xy => (p (fst xy), q (fst xy) (snd xy))) (Either b (x ** (p x, b' x))) -andThen' (Just x `Because` px) f = - map (\y => (x ** y)) (\_ => (px,)) (\y => Right (x ** (px, y))) $ f x -andThen' (Nothing `Because` y) f = Nothing `Because` Left y - -public export -all : - Proof a p b -> - Proof a' q b' -> - Proof (a, a') (\xy => (p (fst xy), q (snd xy))) (These b b') -all (Just x `Because` px) (Just y `Because` py) = Just (x, y) `Because` (px, py) -all (Just x `Because` px) (Nothing `Because` y) = Nothing `Because` That y -all (Nothing `Because` x) q = - Nothing `Because` - case q of - (Just _ `Because` _) => This x - (Nothing `Because` y) => Both x y - -public export -first : - Proof a p b -> - Lazy (Proof c q d) -> - Proof (Either a c) (either p q) (b, d) -first (Just x `Because` px) q = Just (Left x) `Because` px -first (Nothing `Because` x) (Just y `Because` py) = Just (Right y) `Because` py -first (Nothing `Because` x) (Nothing `Because` y) = Nothing `Because` (x, y) - -namespace Either - public export - andThen : - (0 c : a -> Type) -> - (0 p : (x : a) -> c x -> Type) -> - (0 d : a -> Type) -> - LazyEither a b -> ((x : a) -> Proof (c x) (p x) (d x)) -> - Proof (x ** c x) (\xy => p (fst xy) (snd xy)) (Either b (x ** d x)) - andThen _ _ _ (True `Because` x) f = map (\y => (x ** y)) (\_ => id) (\y => Right (x ** y)) (f x) - andThen _ _ _ (False `Because` y) f = Nothing `Because` Left y - - public export - first : - LazyEither a b -> - Lazy (Proof c p d) -> - Proof (Maybe c) (maybe a p) (b, d) - first (True `Because` x) q = Just Nothing `Because` x - first (False `Because` x) (Just y `Because` py) = Just (Just y) `Because` py - first (False `Because` x) (Nothing `Because` y) = Nothing `Because` (x, y) - - public export - all : LazyEither a b -> Lazy (Proof c p d) -> Proof c (\x => (a, p x)) (These b d) - all (True `Because` x) (Just y `Because` py) = Just y `Because` (x, py) - all (True `Because` x) (Nothing `Because` y) = Nothing `Because` That y - all (False `Because` x) q = - Nothing `Because` - case q of - (Just y `Because` _) => This x - (Nothing `Because` y) => Both x y - -namespace Elim - export autobind infixr 0 >=> - - public export - andThen : - {0 q, r : a -> Type} -> - Proof a p b -> ((x : a) -> LazyEither (q x) (r x)) -> - LazyEither (x ** (p x, q x)) (Either b (x ** (p x, r x))) - andThen (Just x `Because` px) f = map (\qx => (x ** (px, qx))) (\rx => Right (x ** (px, rx))) (f x) - andThen (Nothing `Because` y) f = False `Because` Left y - - public export - (>=>) : - {0 q, r : a -> Type} -> - Proof a p b -> ((x : a) -> LazyEither (q x) (r x)) -> - LazyEither (x ** (p x, q x)) (Either b (x ** (p x, r x))) - (>=>) = andThen - -public export -pure : (x : a) -> LazyEither (b x) c -> Proof a b c -pure x (True `Because` y) = Just x `Because` y -pure x (False `Because` y) = Nothing `Because` y diff --git a/src/Inky/Parser.idr b/src/Inky/Parser.idr deleted file mode 100644 index 94d8eb8..0000000 --- a/src/Inky/Parser.idr +++ /dev/null @@ -1,733 +0,0 @@ -module Inky.Parser - -import public Data.List.Quantifiers - -import Control.WellFounded -import Data.Bool -import Data.DPair -import Data.List -import Data.List1 -import Data.Nat -import Data.So -import Data.String.Extra -import Inky.Data.Context -import Inky.Data.Context.Var -import Inky.Data.SnocList.Quantifiers -import Inky.Data.SnocList.Thinning -import Text.Lexer - -export -Interpolation Bounds where - interpolate bounds = "\{show (1 + bounds.startLine)}:\{show bounds.startCol}--\{show (1 + bounds.endLine)}:\{show bounds.endCol}" - --- Parser Expressions ---------------------------------------------------------- - -export infixl 3 <**>, **>, <** -export infixr 2 <||> - -public export -linUnless : Bool -> Context a -> Context a -linUnless False ctx = [<] -linUnless True ctx = ctx - -public export -linUnlessLin : (0 a : Type) -> (b : Bool) -> linUnless {a} b [<] = [<] -linUnlessLin a False = Refl -linUnlessLin a True = Refl - -public export -data Parser : (i : Type) -> (nil : Bool) -> (locked, free : Context (Bool, Type)) -> Type -> Type - -public export -data ParserChain : (i : Type) -> (nil : Bool) -> (locked, free : Context (Bool, Type)) -> List Type -> Type - -data Parser where - Var : Var free (nil, a) -> Parser i nil locked free a - Lit : (text : i) -> Parser i False locked free String - Seq : - ParserChain i nil locked free as -> - Parser i nil locked free (HList as) - OneOf : - {nils : List Bool} -> - All (\nil => Parser i nil locked free a) nils -> - {auto 0 prf : length (filter Basics.id nils) `LTE` 1} -> - Parser i (any Basics.id nils) locked free a - Fix : - (0 x : String) -> - Parser i nil (locked :< (x :- (nil, a))) free a -> - Parser i nil locked free a - Map : (a -> b) -> Parser i nil locked free a -> Parser i nil locked free b - WithBounds : Parser i nil locked free a -> Parser i nil locked free (WithBounds a) - -data ParserChain where - Nil : ParserChain i True locked free [] - (::) : - {nil1, nil2 : Bool} -> - Parser i nil1 locked free a -> - ParserChain i nil2 (linUnless nil1 locked) (free ++ linUnless (not nil1) locked) as -> - ParserChain i (nil1 && nil2) locked free (a :: as) - -%name Parser p, q -%name ParserChain ps, qs - --- Weakening ------------------------------------------------------------------- - -public export -rename : - locked1 `Thins` locked2 -> - free1 `Thins` free2 -> - {auto len : LengthOf locked2} -> - Parser i nil locked1 free1 a -> Parser i nil locked2 free2 a -public export -renameChain : - locked1 `Thins` locked2 -> - free1 `Thins` free2 -> - {auto len : LengthOf locked2} -> - ParserChain i nil locked1 free1 a -> ParserChain i nil locked2 free2 a -public export -renameAll : - locked1 `Thins` locked2 -> - free1 `Thins` free2 -> - {auto len : LengthOf locked2} -> - {0 nils : List Bool} -> - All (\nil => Parser i nil locked1 free1 a) nils -> - All (\nil => Parser i nil locked2 free2 a) nils - -rename f g (Var i) = Var (toVar $ indexPos g i.pos) -rename f g (Lit text) = Lit text -rename f g (Seq ps) = Seq (renameChain f g ps) -rename f g (OneOf ps) = OneOf (renameAll f g ps) -rename f g (Fix x p) = Fix x (rename (Keep f) g p) -rename f g (Map h p) = Map h (rename f g p) -rename f g (WithBounds p) = WithBounds (rename f g p) - -renameChain f g [] = [] -renameChain f g ((::) {nil1 = False} p ps) = rename f g p :: renameChain Id (append g f) ps -renameChain f g ((::) {nil1 = True} p ps) = rename f g p :: renameChain f g ps - -renameAll f g [] = [] -renameAll f g (p :: ps) = rename f g p :: renameAll f g ps - -public export -weaken : - (len1 : LengthOf free2) -> - {auto len2 : LengthOf locked} -> - Parser i nil (free2 ++ locked) free1 a -> Parser i nil locked (free1 ++ free2) a -public export -weakenChain : - (len1 : LengthOf free2) -> - {auto len2 : LengthOf locked} -> - ParserChain i nil (free2 ++ locked) free1 a -> ParserChain i nil locked (free1 ++ free2) a -public export -weakenAll : - (len1 : LengthOf free2) -> - {auto len2 : LengthOf locked} -> - {0 nils : List Bool} -> - All (\nil => Parser i nil (free2 ++ locked) free1 a) nils -> - All (\nil => Parser i nil locked (free1 ++ free2) a) nils - -weaken len1 (Var x) = Var (wknL x) -weaken len1 (Lit text) = Lit text -weaken len1 (Seq ps) = Seq (weakenChain len1 ps) -weaken len1 (OneOf ps) = OneOf (weakenAll len1 ps) -weaken len1 (Fix x p) = Fix x (weaken len1 p) -weaken len1 (Map f p) = Map f (weaken len1 p) -weaken len1 (WithBounds p) = WithBounds (weaken len1 p) - -weakenChain len1 [] = [] -weakenChain len1 ((::) {nil1 = False} p ps) = weaken len1 p :: renameChain Id (assoc len2) ps -weakenChain len1 ((::) {nil1 = True} p ps) = weaken len1 p :: weakenChain len1 ps - -weakenAll len1 [] = [] -weakenAll len1 (p :: ps) = weaken len1 p :: weakenAll len1 ps - --- Substitution ---------------------------------------------------------------- - -public export -sub : - {auto len : LengthOf locked2} -> - (f : All (Assoc0 $ (\nilA => Parser i (fst nilA) [<] (free2 ++ locked2) (snd nilA))) locked1) -> - (g : All (Assoc0 $ (\nilA => Parser i (fst nilA) locked2 free2 (snd nilA))) free1) -> - Parser i nil locked1 free1 a -> Parser i nil locked2 free2 a -public export -subChain : - {auto len : LengthOf locked2} -> - (f : All (Assoc0 $ (\nilA => Parser i (fst nilA) [<] (free2 ++ locked2) (snd nilA))) locked1) -> - (g : All (Assoc0 $ (\nilA => Parser i (fst nilA) locked2 free2 (snd nilA))) free1) -> - ParserChain i nil locked1 free1 a -> ParserChain i nil locked2 free2 a -public export -subAll : - {auto len : LengthOf locked2} -> - (f : All (Assoc0 $ (\nilA => Parser i (fst nilA) [<] (free2 ++ locked2) (snd nilA))) locked1) -> - (g : All (Assoc0 $ (\nilA => Parser i (fst nilA) locked2 free2 (snd nilA))) free1) -> - {0 nils : List Bool} -> - All (\nil => Parser i nil locked1 free1 a) nils -> All (\nil => Parser i nil locked2 free2 a) nils - -sub f g (Var x) = (indexAll x.pos g).value -sub f g (Lit text) = Lit text -sub f g (Seq ps) = Seq (subChain f g ps) -sub f g (OneOf ps) = OneOf (subAll f g ps) -sub f g (Fix x p) = - Fix x $ - sub - (mapProperty (map $ rename Id (Drop Id)) f :< (x :- Var (%%% x))) - (mapProperty (map $ rename (Drop Id) Id) g) - p -sub f g (Map h p) = Map h (sub f g p) -sub f g (WithBounds p) = WithBounds (sub f g p) - -subChain f g [] = [] -subChain f g ((::) {nil1 = False} p ps) = - sub f g p :: - subChain [<] (mapProperty (map $ weaken len) g ++ f) ps -subChain f g ((::) {nil1 = True} p ps) = sub f g p :: subChain f g ps - -subAll f g [] = [] -subAll f g (p :: ps) = sub f g p :: subAll f g ps - --- Typing ---------------------------------------------------------------------- - --- Lists are sufficient, as we assume each symbol appears once. --- TODO: switch to some efficient tree? - -public export -peek : - (env : All (Assoc0 $ const $ List i) free) -> - Parser i nil locked free a -> List i -public export -peekChain : - (env : All (Assoc0 $ const $ List i) free) -> - ParserChain i nil locked free a -> List i -public export -peekAll : - (env : All (Assoc0 $ const $ List i) free) -> - {0 nils : List Bool} -> - All (\nil => Parser i nil locked free a) nils -> - All (const $ List i) nils - -peek env (Var x) = (indexAll x.pos env).value -peek env (Lit text) = [text] -peek env (Seq ps) = peekChain env ps -peek env (OneOf ps) = concat (forget $ peekAll env ps) -peek env (Fix x p) = peek env p -peek env (Map f p) = peek env p -peek env (WithBounds p) = peek env p - -peekChain env [] = [] -peekChain env ((::) {nil1 = False} p ps) = peek env p -peekChain env ((::) {nil1 = True} p ps) = peek env p ++ peekChain env ps - -peekAll env [] = [] -peekAll env (p :: ps) = peek env p :: peekAll env ps - -public export -follow : - (penv1 : All (Assoc0 $ const $ List i) locked) -> - (penv2 : All (Assoc0 $ const $ List i) free) -> - (fenv1 : All (Assoc0 $ const $ List i) locked) -> - (fenv2 : All (Assoc0 $ const $ List i) free) -> - Parser i nil locked free a -> List i -public export -followChain : - (penv1 : All (Assoc0 $ const $ List i) locked) -> - (penv2 : All (Assoc0 $ const $ List i) free) -> - (fenv1 : All (Assoc0 $ const $ List i) locked) -> - (fenv2 : All (Assoc0 $ const $ List i) free) -> - ParserChain i nil locked free a -> List i -public export -followAll : - (penv1 : All (Assoc0 $ const $ List i) locked) -> - (penv2 : All (Assoc0 $ const $ List i) free) -> - (fenv1 : All (Assoc0 $ const $ List i) locked) -> - (fenv2 : All (Assoc0 $ const $ List i) free) -> - {0 nils : List Bool} -> - All (\nil => Parser i nil locked free a) nils -> - List i - -follow penv1 penv2 fenv1 fenv2 (Var x) = (indexAll x.pos fenv2).value -follow penv1 penv2 fenv1 fenv2 (Lit text) = [] -follow penv1 penv2 fenv1 fenv2 (Seq ps) = followChain penv1 penv2 fenv1 fenv2 ps -follow penv1 penv2 fenv1 fenv2 (OneOf ps) = followAll penv1 penv2 fenv1 fenv2 ps -follow penv1 penv2 fenv1 fenv2 (Fix x p) = - -- Conjecture: The fix point converges after one step - -- Proof: - -- - we always add information - -- - no step depends on existing information - follow (penv1 :< (x :- peek penv2 p)) penv2 (fenv1 :< (x :- empty)) fenv2 p -follow penv1 penv2 fenv1 fenv2 (Map f p) = follow penv1 penv2 fenv1 fenv2 p -follow penv1 penv2 fenv1 fenv2 (WithBounds p) = follow penv1 penv2 fenv1 fenv2 p - -followChain penv1 penv2 fenv1 fenv2 [] = [] -followChain penv1 penv2 fenv1 fenv2 ((::) {nil1 = False, nil2} p ps) = - (if nil2 - then peekChain (penv2 ++ penv1) ps ++ follow penv1 penv2 fenv1 fenv2 p - else []) ++ - followChain [<] (penv2 ++ penv1) [<] (fenv2 ++ fenv1) ps -followChain penv1 penv2 fenv1 fenv2 ((::) {nil1 = True, nil2} p ps) = - (if nil2 - then peekChain penv2 ps ++ follow penv1 penv2 fenv1 fenv2 p - else []) ++ - followChain penv1 penv2 fenv1 fenv2 ps - -followAll penv1 penv2 fenv1 fenv2 [] = [] -followAll penv1 penv2 fenv1 fenv2 (p :: ps) = - follow penv1 penv2 fenv1 fenv2 p ++ - followAll penv1 penv2 fenv1 fenv2 ps - -public export -all' : (a -> Bool) -> List a -> Bool -all' f [] = True -all' f (x :: xs) = f x && all' f xs - -allTrue : (xs : List a) -> all' (const True) xs = True -allTrue [] = Refl -allTrue (x :: xs) = allTrue xs - -public export -disjoint : Eq a => List (List a) -> Bool -disjoint [] = True -disjoint (xs :: xss) = all' (\ys => all' (\x => not (x `elem` ys)) xs) xss && disjoint xss - -namespace WellTyped - public export - wellTyped : - (e : Eq i) -> - (penv1 : All (Assoc0 $ const $ List i) locked) -> - (penv2 : All (Assoc0 $ const $ List i) free) -> - (fenv1 : All (Assoc0 $ const $ List i) locked) -> - (fenv2 : All (Assoc0 $ const $ List i) free) -> - Parser i nil locked free a -> - Bool - public export - wellTypedChain : - (e : Eq i) -> - (penv1 : All (Assoc0 $ const $ List i) locked) -> - (penv2 : All (Assoc0 $ const $ List i) free) -> - (fenv1 : All (Assoc0 $ const $ List i) locked) -> - (fenv2 : All (Assoc0 $ const $ List i) free) -> - ParserChain i nil locked free a -> - Bool - public export - allWellTyped : - (e : Eq i) -> - (penv1 : All (Assoc0 $ const $ List i) locked) -> - (penv2 : All (Assoc0 $ const $ List i) free) -> - (fenv1 : All (Assoc0 $ const $ List i) locked) -> - (fenv2 : All (Assoc0 $ const $ List i) free) -> - {0 nils : List Bool} -> - All (\nil => Parser i nil locked free a) nils -> - Bool - - wellTyped e penv1 penv2 fenv1 fenv2 (Var i) = True - wellTyped e penv1 penv2 fenv1 fenv2 (Lit txt) = True - wellTyped e penv1 penv2 fenv1 fenv2 (Seq ps) = wellTypedChain e penv1 penv2 fenv1 fenv2 ps - wellTyped e penv1 penv2 fenv1 fenv2 (OneOf {nils, prf} ps) = - disjoint (forget $ peekAll penv2 ps) && allWellTyped e penv1 penv2 fenv1 fenv2 ps - wellTyped e penv1 penv2 fenv1 fenv2 (Fix x p) = - wellTyped e - (penv1 :< (x :- peek penv2 p)) - penv2 - (fenv1 :< (x :- follow (penv1 :< (x :- peek penv2 p)) penv2 (fenv1 :< (x :- [])) fenv2 p)) - fenv2 - p - wellTyped e penv1 penv2 fenv1 fenv2 (Map f p) = wellTyped e penv1 penv2 fenv1 fenv2 p - wellTyped e penv1 penv2 fenv1 fenv2 (WithBounds p) = wellTyped e penv1 penv2 fenv1 fenv2 p - - wellTypedChain e penv1 penv2 fenv1 fenv2 [] = True - wellTypedChain e penv1 penv2 fenv1 fenv2 ((::) {nil1 = False} p ps) = - disjoint [follow penv1 penv2 fenv1 fenv2 p, peekChain (penv2 ++ penv1) ps] && - wellTyped e penv1 penv2 fenv1 fenv2 p && - wellTypedChain e [<] (penv2 ++ penv1) [<] (fenv2 ++ fenv1) ps - wellTypedChain e penv1 penv2 fenv1 fenv2 ((::) {nil1 = True} p ps) = - disjoint [follow penv1 penv2 fenv1 fenv2 p, peekChain penv2 ps] && - wellTyped e penv1 penv2 fenv1 fenv2 p && - wellTypedChain e penv1 penv2 fenv1 fenv2 ps - - allWellTyped e penv1 penv2 fenv1 fenv2 [] = True - allWellTyped e penv1 penv2 fenv1 fenv2 (p :: ps) = - wellTyped e penv1 penv2 fenv1 fenv2 p && - allWellTyped e penv1 penv2 fenv1 fenv2 ps - --- Parsing Function ------------------------------------------------------------ - --- Utilty for recursion - -public export -data SmallerX : Bool -> List a -> List a -> Type where - Strict : {0 xs, ys : List a} -> xs `Smaller` ys -> SmallerX False xs ys - Lax : {0 xs, ys : List a} -> size xs `LTE` size ys -> SmallerX True xs ys - -transX : - {xs, ys, zs : List a} -> - SmallerX b1 xs ys -> SmallerX b2 ys zs -> SmallerX (b1 && b2) xs zs -transX (Strict prf1) (Strict prf2) = Strict (transitive prf1 (lteSuccLeft prf2)) -transX (Strict prf1) (Lax prf2) = Strict (transitive prf1 prf2) -transX (Lax prf1) (Strict prf2) = Strict (transitive (LTESucc prf1) prf2) -transX (Lax prf1) (Lax prf2) = Lax (transitive prf1 prf2) - -ofSmaller : {b : Bool} -> {0 xs, ys : List a} -> xs `Smaller` ys -> SmallerX b xs ys -ofSmaller {b = False} prf = Strict prf -ofSmaller {b = True} prf = Lax (lteSuccLeft prf) - -wknSmallerL : SmallerX b1 xs ys -> (b2 : Bool) -> SmallerX (b1 || b2) xs ys -wknSmallerL (Strict prf) _ = ofSmaller prf -wknSmallerL (Lax prf) _ = Lax prf - -wknSmallerR : (b1 : Bool) -> SmallerX b2 xs ys -> SmallerX (b1 || b2) xs ys -wknSmallerR b1 (Strict prf) = - if b1 then ofSmaller prf else ofSmaller prf -wknSmallerR b1 (Lax prf) = - if b1 then Lax prf else Lax prf - -forget : SmallerX b xs ys -> SmallerX True xs ys -forget = wknSmallerR True - -toSmaller : {xs, ys : List a} -> (0 _ : SmallerX False xs ys) -> xs `Smaller` ys -toSmaller {xs = []} {ys = []} (Strict prf) impossible -toSmaller {xs = []} {ys = (y :: ys)} (Strict prf) = LTESucc LTEZero -toSmaller {xs = (x :: xs)} {ys = []} (Strict prf) impossible -toSmaller {xs = (x :: xs)} {ys = (y :: ys)} (Strict (LTESucc prf)) = LTESucc (toSmaller (Strict prf)) - -anyCons : (b : Bool) -> (bs : List Bool) -> any Basics.id (b :: bs) = b || any Basics.id bs -anyCons b [] = sym (orFalseNeutral b) -anyCons b (b' :: bs) = - trans (anyCons (b || b') bs) $ - trans (sym $ orAssociative b b' (any id bs)) - (cong (b ||) (sym $ anyCons b' bs)) - -anyTrue : (bs : List Bool) -> any Basics.id (True :: bs) = True -anyTrue = anyCons True - --- Return Type - -namespace M - public export - data M : List a -> Bool -> Type -> Type where - Err : String -> M xs nil b - Ok : (res : b) -> (ys : List a) -> (0 prf : SmallerX nil ys xs) -> M xs nil b - - export - Functor (M xs nil) where - map f (Err msg) = Err msg - map f (Ok res ys prf) = Ok (f res) ys prf - - export - pure : {xs : List a} -> (x : b) -> M xs True b - pure x = Ok x xs (Lax reflexive) - - export - (>>=) : - M xs nil b -> - (b -> {ys : List a} -> {auto 0 prf : SmallerX nil ys xs} -> M ys nil' c) -> - M xs (nil && nil') c - Err str >>= f = Err str - Ok res ys prf >>= f = - case f {ys, prf} res of - Err str => Err str - Ok res' zs prf' => Ok res' zs (rewrite andCommutative nil nil' in transX prf' prf) - - export - take : - Eq a => - Interpolation a => - (toks : List a) -> - (xs : List (WithBounds (Token a))) -> - M xs False String - take [tok] [] = Err "expected \{tok}; got end of input" - take toks [] = Err "expected one of: \{join ", " $ map (\k => "\{k}") toks}; got end of input" - take toks (x :: xs) = - if x.val.kind `elem` toks - then Ok x.val.text xs (Strict reflexive) - else case toks of - [tok] => Err "\{x.bounds}: expected \{tok}; got \{x.val.kind}" - toks => Err "\{x.bounds}: expected one of: \{join ", " $ map (\k => "\{k}") toks}; got \{x.val.kind}" - - export - bounds : (xs : List (WithBounds a)) -> M xs True (Bool, Bounds) - bounds [] = Ok (True, MkBounds (-1) (-1) (-1) (-1)) [] (Lax reflexive) - bounds (x :: xs) = Ok (x.isIrrelevant, x.bounds) (x :: xs) (Lax reflexive) - - export - wknL : M xs b1 a -> (b2 : Bool) -> M xs (b1 || b2) a - wknL (Err msg) b2 = Err msg - wknL (Ok res ys prf) b2 = Ok res ys (wknSmallerL prf b2) - - export - wknR : (b1 : Bool) -> M xs b2 a -> M xs (b1 || b2) a - wknR b1 (Err msg) = Err msg - wknR b1 (Ok res ys prf) = Ok res ys (wknSmallerR b1 prf) - - export - anyL : - (b : Bool) -> {0 bs : List Bool} -> - M xs (any Basics.id bs) a -> M xs (any Basics.id (b :: bs)) a - anyL b m = rewrite anyCons b bs in wknR b m - - export - anyR : (bs : List Bool) -> M xs b a -> M xs (any Basics.id (b :: bs)) a - anyR bs m = rewrite anyCons b bs in wknL m (any id bs) - --- The Big Function - -||| Searches `sets` for the first occurence of `x`. -||| On failure, returns the index for the nil element, if it exists. -||| -||| # Unsafe Invariants -||| * `nils` has at most one `True` element -||| * `sets` are disjoint -lookahead : - Eq a => - (x : Maybe a) -> - (nils : List Bool) -> - (sets : Lazy (All (const $ List a) nils)) -> - Maybe (Any (const ()) nils) -lookahead x [] [] = Nothing -lookahead x (nil :: nils) (set :: sets) = - (do - x <- x - if x `elem` set then Just (Here ()) else Nothing) - <|> There <$> lookahead x nils sets - <|> (if nil then Just (Here ()) else Nothing) - -parser : - (e : Eq i) => Interpolation i => - (p : Parser i nil locked free a) -> - {penv1 : _} -> - {penv2 : _} -> - {0 fenv1 : _} -> - {0 fenv2 : _} -> - (0 wf : So (wellTyped e penv1 penv2 fenv1 fenv2 p)) -> - (xs : List (WithBounds (Token i))) -> - All (Assoc0 (\x => (ys : List (WithBounds (Token i))) -> (0 _ : SmallerX False ys xs) -> uncurry (M ys) x)) locked -> - All (Assoc0 (\x => (ys : List (WithBounds (Token i))) -> (0 _ : SmallerX True ys xs) -> uncurry (M ys) x)) free -> - M xs nil a -parserChain : - (e : Eq i) => Interpolation i => - (ps : ParserChain i nil locked free as) -> - {penv1 : _} -> - {penv2 : _} -> - {0 fenv1 : _} -> - {0 fenv2 : _} -> - (0 wf : So (wellTypedChain e penv1 penv2 fenv1 fenv2 ps)) -> - (xs : List (WithBounds (Token i))) -> - All (Assoc0 (\x => (ys : List (WithBounds (Token i))) -> (0 _ : SmallerX False ys xs) -> uncurry (M ys) x)) locked -> - All (Assoc0 (\x => (ys : List (WithBounds (Token i))) -> (0 _ : SmallerX True ys xs) -> uncurry (M ys) x)) free -> - M xs nil (HList as) -parserOneOf : - (e : Eq i) => Interpolation i => - {nils : List Bool} -> - (at : Any (const ()) nils) -> - (ps : All (\nil => Parser i nil locked free a) nils) -> - {penv1 : _} -> - {penv2 : _} -> - {0 fenv1 : _} -> - {0 fenv2 : _} -> - (0 wf : So (allWellTyped e penv1 penv2 fenv1 fenv2 ps)) -> - (xs : List (WithBounds (Token i))) -> - All (Assoc0 (\x => (ys : List (WithBounds (Token i))) -> (0 _ : SmallerX False ys xs) -> uncurry (M ys) x)) locked -> - All (Assoc0 (\x => (ys : List (WithBounds (Token i))) -> (0 _ : SmallerX True ys xs) -> uncurry (M ys) x)) free -> - M xs (any Basics.id nils) a - -parser (Var x) wf xs env1 env2 = (indexAll x.pos env2).value xs (Lax reflexive) -parser (Lit text) wf xs env1 env2 = take [text] xs -parser (Seq ps) wf xs env1 env2 = - parserChain ps wf xs env1 env2 -parser (OneOf {nils} ps) wf [] env1 env2 = - let 0 wfs = soAnd {a = disjoint (forget $ peekAll penv2 ps)} wf in - let sets = peekAll penv2 ps in - case lookahead Nothing nils sets of - Nothing => Err "unexpected end of input" - Just at => parserOneOf at ps (snd wfs) [] env1 env2 -parser (OneOf {nils} ps) wf (x :: xs) env1 env2 = - let 0 wfs = soAnd {a = disjoint (forget $ peekAll penv2 ps)} wf in - let sets = peekAll penv2 ps in - case lookahead (Just x.val.kind) nils sets of - Nothing => Err "\{x.bounds}: expected one of: \{join ", " $ map (\k => "\{k}") $ concat $ forget sets}; got \{x.val.kind}" - Just at => parserOneOf at ps (snd wfs) (x :: xs) env1 env2 -parser (Fix {a, nil} x p) wf xs env1 env2 = - let f = parser p wf in - sizeInd {P = \ys => (0 prf : SmallerX True ys xs) -> M ys nil a} - (\ys, rec, lte => - f ys - ( mapProperty (map (\f, zs, 0 prf => f zs $ transX prf lte)) env1 - :< (x :- (\zs, prf => rec zs (toSmaller prf) (forget $ transX prf lte))) - ) - (mapProperty (map (\f, zs, prf => f zs $ transX prf lte)) env2)) - xs (Lax reflexive) -parser (Map f p) wf xs env1 env2 = - f <$> parser p wf xs env1 env2 -parser (WithBounds p) wf xs env1 env2 = do - (irrel, bounds) <- bounds xs - rewrite sym $ andTrueNeutral nil - x <- parser p wf _ - (mapProperty (map (\f, zs, 0 prf => f zs $ transX {b2 = True} prf %search)) env1) - (mapProperty (map (\f, zs, 0 prf => f zs $ transX prf %search)) env2) - pure (MkBounded x irrel bounds) - -parserChain [] wf xs env1 env2 = Ok [] xs (Lax reflexive) -parserChain ((::) {nil1 = False, nil2} p ps) wf xs env1 env2 = - let 0 wfs = soAnd wf in - let 0 wfs' = soAnd (snd wfs) in do - x <- parser p (fst wfs') xs env1 env2 - y <- parserChain ps (snd wfs') - _ - [<] - ( mapProperty (map (\f, zs, 0 prf => f zs $ forget $ transX {b2 = False} prf %search)) env2 - ++ mapProperty (map (\f, zs, 0 prf => f zs $ transX prf %search)) env1 - ) - pure (x :: y) -parserChain ((::) {nil1 = True, nil2} p ps) wf xs env1 env2 = - let 0 wfs = soAnd wf in - let 0 wfs' = soAnd (snd wfs) in do - x <- parser p (fst wfs') xs env1 env2 - rewrite sym $ andTrueNeutral nil2 - y <- parserChain ps (snd wfs') - _ - (mapProperty (map (\f, zs, prf => f zs $ transX {b2 = True} prf %search)) env1) - (mapProperty (map (\f, zs, prf => f zs $ transX prf %search)) env2) - pure (x :: y) - -parserOneOf {nils = nil :: nils} (Here ()) (p :: ps) wf xs env1 env2 = - let 0 wfs = soAnd wf in - anyR nils (parser p (fst wfs) xs env1 env2) -parserOneOf {nils = nil :: nils} (There at) (p :: ps) wf xs env1 env2 = - let 0 wfs = soAnd {a = wellTyped e penv1 penv2 fenv1 fenv2 p} wf in - anyL nil (parserOneOf at ps (snd wfs) xs env1 env2) - -export -parse : - (e : Eq i) => Interpolation i => - (p : Parser i nil [<] [<] a) -> - {auto 0 wf : So (wellTyped e [<] [<] [<] [<] p)} -> - (xs : List (WithBounds (Token i))) -> M xs nil a -parse p xs = parser p wf xs [<] [<] - --- Functor --------------------------------------------------------------------- - -public export -(++) : - {nil2 : Bool} -> - ParserChain i nil1 locked free as -> - ParserChain i nil2 (linUnless nil1 locked) (free ++ linUnless (not nil1) locked) bs -> - ParserChain i (nil1 && nil2) locked free (as ++ bs) -[] ++ qs = qs -((::) {nil1 = False, nil2} p ps) ++ qs = - p :: - ( ps - ++ rewrite linUnlessLin (Bool, Type) nil2 in - rewrite linUnlessLin (Bool, Type) (not nil2) in - qs) -((::) {nil1 = True, nil2} p ps) ++ qs = p :: (ps ++ qs) - -public export -(<**>) : - {nil1, nil2 : Bool} -> - Parser i nil1 locked free a -> - Parser i nil2 (linUnless nil1 locked) (free ++ linUnless (not nil1) locked) b -> - Parser i (nil1 && nil2) locked free (a, b) -p <**> Seq ps = Map (\(x :: xs) => (x, xs)) $ Seq (p :: ps) --- HACK: andTrueNeutral isn't public, so do a full case split. -(<**>) {nil1 = True, nil2 = True} p q = Map (\[x, y] => (x, y)) $ Seq [p, q] -(<**>) {nil1 = True, nil2 = False} p q = Map (\[x, y] => (x, y)) $ Seq [p, q] -(<**>) {nil1 = False, nil2 = True} p q = Map (\[x, y] => (x, y)) $ Seq [p, q] -(<**>) {nil1 = False, nil2 = False} p q = Map (\[x, y] => (x, y)) $ Seq [p, q] - -public export -Functor (Parser i nil locked free) where - map f (Map g p) = Map (f . g) p - map f p = Map f p - -public export -Applicative (Parser i True locked free) where - pure x = map (const x) (Seq []) - p <*> q = map (\(f, x) => f x) (p <**> q) - --- Combinator ------------------------------------------------------------------ - -public export -(<|>) : - {nil1, nil2 : Bool} -> - Parser i nil1 locked free a -> - Parser i nil2 locked free a -> - {auto 0 prf : length (filter Basics.id [nil1, nil2]) `LTE` 1} -> - Parser i (nil1 || nil2) locked free a -p <|> q = OneOf [p, q] - -public export -(<||>) : - {nil1, nil2 : Bool} -> - Parser i nil1 locked free a -> - Parser i nil2 locked free b -> - {auto 0 prf : length (filter Basics.id [nil1, nil2]) `LTE` 1} -> - Parser i (nil1 || nil2) locked free (Either a b) -p <||> q = Left <$> p <|> Right <$> q - -public export -(**>) : - {nil1, nil2 : Bool} -> - Parser i nil1 locked free a -> - Parser i nil2 (linUnless nil1 locked) (free ++ linUnless (not nil1) locked) b -> - Parser i (nil1 && nil2) locked free b -p **> q = snd <$> (p <**> q) - -public export -(<**) : - {nil1, nil2 : Bool} -> - Parser i nil1 locked free a -> - Parser i nil2 (linUnless nil1 locked) (free ++ linUnless (not nil1) locked) b -> - Parser i (nil1 && nil2) locked free a -p <** q = fst <$> (p <**> q) - -public export -match : TokenKind i => (kind : i) -> Parser i False locked free (TokType kind) -match kind = Map (tokValue kind) $ Lit kind - -public export -enclose : - {b1, b2, b3 : Bool} -> - (left : Parser i b1 locked free ()) -> - (right : - Parser i b3 - (linUnless b2 (linUnless b1 locked)) - ((free ++ linUnless (not b1) locked) ++ linUnless (not b2) (linUnless b1 locked)) - ()) -> - Parser i b2 (linUnless b1 locked) (free ++ linUnless (not b1) locked) a -> - Parser i (b1 && b2 && b3 && True) locked free a -enclose left right p = (\[_, x, _] => x) <$> Seq {as = [(), a, ()]} [left, p, right] - -public export -option : Parser i False locked free a -> Parser i True locked free (Maybe a) -option p = (Just <$> p) <|> pure Nothing - -public export -plus : - {auto len : LengthOf locked} -> - Parser i False locked free a -> - Parser i False locked free (List1 a) -plus p = - Fix "plus" - ( uncurry (:::) - <$> (rename (Drop Id) Id p <**> maybe [] forget <$> option (Var $ %%% "plus"))) - -public export -star : - {auto len : LengthOf locked} -> - Parser i False locked free a -> - Parser i True locked free (List a) -star p = maybe [] forget <$> option (plus p) - -public export -sepBy1 : - {auto len : LengthOf locked} -> - (sep : Parser i False locked free ()) -> - Parser i False locked free a -> - Parser i False locked free (List1 a) -sepBy1 sep p = uncurry (:::) <$> (p <**> star (weaken len sep **> weaken len p)) - -public export -sepBy : - {auto len : LengthOf locked} -> - (sep : Parser i False locked free ()) -> - Parser i False locked free a -> - Parser i True locked free (List a) -sepBy sep p = maybe [] forget <$> option (sepBy1 sep p) diff --git a/src/Inky/Term.idr b/src/Inky/Term.idr index 3c5d214..884256f 100644 --- a/src/Inky/Term.idr +++ b/src/Inky/Term.idr @@ -5,9 +5,9 @@ import public Inky.Type import Data.List.Quantifiers import Data.Singleton import Data.These -import Inky.Data.SnocList.Quantifiers -import Inky.Decidable -import Inky.Decidable.Maybe +import Flap.Data.SnocList.Quantifiers +import Flap.Decidable +import Flap.Decidable.Maybe %hide Prelude.Ops.infixl.(>=>) @@ -84,13 +84,6 @@ data NotFunction : (bound : List String) -> (a : Ty tyCtx) -> Type %name IsFunction prf %name NotFunction contra -export -isFunctionRecompute : - {a : Ty tyCtx} -> IsFunction bound a dom cod -> (Singleton dom, Singleton cod) -isFunctionRecompute Done = (Val _, Val _) -isFunctionRecompute (Step {a} prf) = - mapFst (\case Val _ => Val _) $ isFunctionRecompute prf - export isFunctionUnique : IsFunction bound a dom cod -> IsFunction bound a dom' cod' -> (dom = dom', cod = cod') diff --git a/src/Inky/Term/Checks.idr b/src/Inky/Term/Checks.idr index 6027d68..8de671c 100644 --- a/src/Inky/Term/Checks.idr +++ b/src/Inky/Term/Checks.idr @@ -5,49 +5,14 @@ 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 Flap.Data.SnocList.Quantifiers +import Flap.Decidable +import Flap.Decidable.Maybe import Inky.Term +import Inky.Term.Recompute %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 diff --git a/src/Inky/Term/Compile.idr b/src/Inky/Term/Compile.idr new file mode 100644 index 0000000..0867cd2 --- /dev/null +++ b/src/Inky/Term/Compile.idr @@ -0,0 +1,316 @@ +module Inky.Term.Compile + +-- For DAll +import public Inky.Type.Substitution + +import Data.Maybe +import Data.List.Quantifiers +import Data.Singleton +import Flap.Decidable +import Flap.Decidable.Maybe +import Inky.Term +import Inky.Term.Recompute +import Text.PrettyPrint.Prettyprinter + +-- Utilities ------------------------------------------------------------------- + +mkLet : (bind, val, body: Doc ann) -> Doc ann +mkLet bind val body = + parens $ align $ hang 1 $ + "let" <++> parens (group $ parens $ align $ bind <++> group val) <++> + group body + +mkAbs : (bind, body: Doc ann) -> Doc ann +mkAbs bind body = + parens $ align $ hang 1 $ + "lambda" <++> parens bind <++> + group body + +mkTup : Context (Doc ann) -> Doc ann +mkTup parts = + let + f = \lx => + group $ parens $ align $ hang 2 $ + pretty lx.name <++> "." <++> "," <+> group lx.value + in + "`" <+> group (parens $ align $ concatWith (<++>) $ map f parts <>> []) + +mkPrj : Doc ann -> String -> Doc ann +mkPrj x l = + parens $ align $ + pretty "assq-ref" <++> + group x <++> + pretty "'" <+> pretty l + +mkInj : String -> Doc ann -> Doc ann +mkInj l x = + parens $ align $ + "cons" <++> + "'" <+> pretty l <++> + group x + +mkCase : Doc ann -> Context (Doc ann, Doc ann) -> Doc ann +mkCase target branches = + let + f = \lxy => + group $ parens $ align $ + parens ("'" <+> pretty lxy.name <++> "." <++> fst lxy.value) <++> + group (snd lxy.value) + in + parens $ align $ hang 2 $ + "match" <++> + group target <++> + concatWith (<++>) (map f branches <>> []) + +-- Create a "unique" name from a type ------------------------------------------ + +hashType : Ty tyCtx -> String +hashTypes : Context (Ty tyCtx) -> List String + +hashType (TVar i) = "V" ++ show i +hashType (TArrow a b) = concat ["A", hashType a, hashType b] +hashType (TProd (MkRow as _)) = concat ("P" :: hashTypes as) +hashType (TSum (MkRow as _)) = concat ("S" :: hashTypes as) +hashType (TFix x a) = concat ["F", hashType a] + +hashTypes [<] = ["N"] +hashTypes (as :< (l :- a)) = ["L", l, hashType a] ++ hashTypes as + +-- Compile map and fold -------------------------------------------------------- + +compileMap : + {a : Ty tyCtx} -> + (0 wf : WellFormed a) -> (i : Var tyCtx) -> + (0 prf : i `StrictlyPositiveIn` a) -> + (f, t : Doc ann) -> Doc ann +eagerCompileMap : + {a : Ty tyCtx} -> + (0 wf : WellFormed a) -> (i : Var tyCtx) -> + (0 prf : i `StrictlyPositiveIn` a) -> + (f, t : Doc ann) -> Doc ann +compileMapTuple : + {as : Context (Ty tyCtx)} -> + (0 wf : AllWellFormed as) -> (i : Var tyCtx) -> + (0 prfs : i `StrictlyPositiveInAll` as) -> + (f, t : Doc ann) -> All (Assoc0 $ Doc ann) as.names +compileMapCase : + {as : Context (Ty tyCtx)} -> + (0 wf : AllWellFormed as) -> (i : Var tyCtx) -> + (0 prfs : i `StrictlyPositiveInAll` as) -> + (fun : Doc ann) -> All (Assoc0 $ (Doc ann, Doc ann)) as.names + +compileFold : + {a : Ty (tyCtx :< x)} -> + (0 wf : WellFormed a) -> + (0 prf : %% x `StrictlyPositiveIn` a) -> + (target, bind, body : Doc ann) -> Doc ann + +compileMap wf i prf f t = + if isJust (does $ strengthen i a) + then t + else eagerCompileMap wf i prf f t + +eagerCompileMap (TVar {i = j}) i TVar f t with (i `decEq` j) + _ | True `Because` _ = parens (f <++> t) + _ | False `Because` _ = t +eagerCompileMap (TArrow _ _) i (TArrow prf) f t = t +eagerCompileMap (TProd wfs) i (TProd prfs) f t = + mkTup $ fromAll $ compileMapTuple wfs i prfs f t +eagerCompileMap (TSum wfs) i (TSum prfs) f t = + mkCase t $ fromAll $ compileMapCase wfs i prfs f +eagerCompileMap (TFix sp wf) i (TFix prf) f t = + compileFold wf sp t (pretty "_eta") $ + eagerCompileMap wf (ThereVar i) prf f (pretty "_eta") + +compileMapTuple [<] i [<] f t = [<] +compileMapTuple ((:<) wfs {n} wf) i (prfs :< prf) f t = + compileMapTuple wfs i prfs f t :< + (n :- compileMap wf i prf f (mkPrj t n)) + +compileMapCase [<] i [<] f = [<] +compileMapCase ((:<) wfs {n} wf) i (prfs :< prf) f = + compileMapCase wfs i prfs f :< + (n :- (pretty "_eta", mkInj n (compileMap wf i prf f $ pretty "_eta"))) + +compileFold {a} wf prf target bind body = + let name = pretty "fold-" <+> pretty (hashType a) in + let + fun = parens $ align $ hang 1 $ + "define" <++> parens (name <++> name <+> "-arg") <++> + group (mkLet bind (compileMap wf (%% x) prf name (name <+> "-arg")) body) + in + parens $ align $ hang 1 $ + "begin" <++> + group fun <++> + parens (name <++> target) + +-- Compile any term ------------------------------------------------------------ + +export +compileSynths : + {tmCtx : SnocList String} -> + {t : Term mode m tyCtx tmCtx} -> + {tyEnv : All (Assoc0 $ Ty [<]) tyCtx} -> + {tmEnv : All (Assoc0 $ Ty [<]) tmCtx} -> + (0 tyWf : DAll WellFormed tyEnv) -> + (0 tmWf : DAll WellFormed tmEnv) -> + (0 _ : Synths tyEnv tmEnv t a) -> + Doc ann +export +compileChecks : + {tmCtx : SnocList String} -> + {t : Term mode m tyCtx tmCtx} -> + {tyEnv : All (Assoc0 $ Ty [<]) tyCtx} -> + {tmEnv : All (Assoc0 $ Ty [<]) tmCtx} -> + (0 tyWf : DAll WellFormed tyEnv) -> + (0 tmWf : DAll WellFormed tmEnv) -> + {a : Ty [<]} -> + (0 wf : WellFormed a) -> + (0 _ : Checks tyEnv tmEnv a t) -> + Doc ann +compileSpine : + {tmCtx : SnocList String} -> + {ts : List (Term mode m tyCtx tmCtx)} -> + {tyEnv : All (Assoc0 $ Ty [<]) tyCtx} -> + {tmEnv : All (Assoc0 $ Ty [<]) tmCtx} -> + (0 tyWf : DAll WellFormed tyEnv) -> + (0 tmWf : DAll WellFormed tmEnv) -> + {a : Ty [<]} -> + (0 wf : WellFormed a) -> + (0 _ : CheckSpine tyEnv tmEnv a ts b) -> + (fun : Doc ann) -> + Doc ann +compileAllSynths : + {tmCtx : SnocList String} -> + {ts : Context (Term mode m tyCtx tmCtx)} -> + {tyEnv : All (Assoc0 $ Ty [<]) tyCtx} -> + {tmEnv : All (Assoc0 $ Ty [<]) tmCtx} -> + (0 tyWf : DAll WellFormed tyEnv) -> + (0 tmWf : DAll WellFormed tmEnv) -> + (0 _ : AllSynths tyEnv tmEnv ts as) -> + All (Assoc0 $ Doc ann) ts.names +compileAllChecks : + {tmCtx : SnocList String} -> + {ts : Context (Term mode m tyCtx tmCtx)} -> + {tyEnv : All (Assoc0 $ Ty [<]) tyCtx} -> + {tmEnv : All (Assoc0 $ Ty [<]) tmCtx} -> + (0 tyWf : DAll WellFormed tyEnv) -> + (0 tmWf : DAll WellFormed tmEnv) -> + {as : Context (Ty [<])} -> + (0 fresh : AllFresh as.names) -> + (0 wfs : AllWellFormed as) -> + (0 _ : AllChecks tyEnv tmEnv as ts) -> + All (Assoc0 $ Doc ann) ts.names +compileAllBranches : + {tmCtx : SnocList String} -> + {ts : Context (x ** Term mode m tyCtx (tmCtx :< x))} -> + {tyEnv : All (Assoc0 $ Ty [<]) tyCtx} -> + {tmEnv : All (Assoc0 $ Ty [<]) tmCtx} -> + (0 tyWf : DAll WellFormed tyEnv) -> + (0 tmWf : DAll WellFormed tmEnv) -> + {as : Context (Ty [<])} -> + {a : Ty [<]} -> + (0 fresh : AllFresh as.names) -> + (0 wfs : AllWellFormed as) -> + (0 wf : WellFormed a) -> + (0 _ : AllBranches tyEnv tmEnv as a ts) -> + All (Assoc0 (Doc ann, Doc ann)) ts.names + +compileSynths tyWf tmWf (AnnotS wf prf) = compileChecks tyWf tmWf (subWf tyWf wf) prf +compileSynths tyWf tmWf (VarS {i}) = pretty (unVal $ nameOf i.pos) +compileSynths tyWf tmWf (LetS {x} prf1 prf2) = + case synthsRecompute prf1 of + Val _ => + mkLet (pretty x) + (compileSynths tyWf tmWf prf1) + (compileSynths tyWf (tmWf :< (x :- synthsWf tyWf tmWf prf1)) prf2) +compileSynths tyWf tmWf (LetTyS {x} wf prf) = + compileSynths (tyWf :< (x :- subWf tyWf wf)) tmWf prf +compileSynths tyWf tmWf (AppS prf prfs) = + case synthsRecompute prf of + Val _ => compileSpine tyWf tmWf (synthsWf tyWf tmWf prf) prfs (compileSynths tyWf tmWf prf) +compileSynths tyWf tmWf (TupS prfs) = mkTup $ fromAll $ compileAllSynths tyWf tmWf prfs +compileSynths tyWf tmWf (PrjS {l} prf i) = mkPrj (compileSynths tyWf tmWf prf) l +compileSynths tyWf tmWf (UnrollS prf) = compileSynths tyWf tmWf prf +compileSynths tyWf tmWf (MapS (TFix {x} sp wf1) wf2 wf3) = + mkAbs (pretty "_fun") $ + mkAbs (pretty "_arg") $ + compileMap wf1 (%% x) sp (pretty "_fun") (pretty "_arg") + +compileChecks tyWf tmWf wf (AnnotC prf1 prf2) = compileSynths tyWf tmWf prf1 +compileChecks tyWf tmWf wf (VarC prf1 prf2) = compileSynths tyWf tmWf prf1 +compileChecks tyWf tmWf wf (LetC {x} prf1 prf2) = + case synthsRecompute prf1 of + Val _ => + mkLet (pretty x) + (compileSynths tyWf tmWf prf1) + (compileChecks tyWf (tmWf :< (x :- synthsWf tyWf tmWf prf1)) wf prf2) +compileChecks tyWf tmWf wf (LetTyC wf' {x} prf) = + compileChecks (tyWf :< (x :- subWf tyWf wf')) tmWf wf prf +compileChecks tyWf tmWf wf (AbsC {bound} prf1 prf2) = + case isFunctionRecompute prf1 of + (Val _, Val _) => + let 0 wfs = isFunctionWf prf1 wf in + foldr + (mkAbs . pretty) + (compileChecks tyWf (tmWf <>< fst wfs) (snd wfs) prf2) + bound +compileChecks tyWf tmWf wf (AppC prf1 prf2) = compileSynths tyWf tmWf prf1 +compileChecks tyWf tmWf (TProd {as = MkRow as fresh} wfs) (TupC prfs) = + mkTup $ fromAll $ compileAllChecks tyWf tmWf fresh wfs prfs +compileChecks tyWf tmWf wf (PrjC prf1 prf2) = compileSynths tyWf tmWf prf1 +compileChecks tyWf tmWf (TSum wfs) (InjC {l, as} i prf) = + case lookupRecompute as i of + Val i => case nameOf i of + Val _ => mkInj l $ compileChecks tyWf tmWf (indexAllWellFormed wfs i) prf +compileChecks tyWf tmWf wf (CaseC {as = MkRow as fresh} prf prfs) = + case synthsRecompute prf of + Val _ => + let + 0 wfs : AllWellFormed as + wfs = case synthsWf tyWf tmWf prf of TSum prfs => prfs + in + mkCase + (compileSynths tyWf tmWf prf) + (fromAll $ compileAllBranches tyWf tmWf fresh wfs wf prfs) +compileChecks tyWf tmWf (TFix {x} sp wf) (RollC prf) = + compileChecks tyWf tmWf (subWf [ + let + 0 spwf : (%% x `StrictlyPositiveIn` a, WellFormed a) + spwf = case synthsWf tyWf tmWf prf1 of TFix sp wf => (sp, wf) + in + compileFold (snd spwf) (fst spwf) + (compileSynths tyWf tmWf prf1) + (pretty y) + (compileChecks tyWf (tmWf :< (y :- (subWf [ group arg + +compileAllSynths tyWf tmWf [<] = [<] +compileAllSynths tyWf tmWf ((:<) prfs {l} prf) = + compileAllSynths tyWf tmWf prfs :< (l :- compileSynths tyWf tmWf prf) + +compileAllChecks tyWf tmWf fresh wfs Base = [<] +compileAllChecks tyWf tmWf fresh wfs (Step {l, as} i prf prfs) = + case lookupRecompute (MkRow as fresh) i of + Val i => case nameOf i of + Val _ => + compileAllChecks tyWf tmWf (dropElemFresh as fresh i) (dropAllWellFormed wfs i) prfs :< + (l :- compileChecks tyWf tmWf (indexAllWellFormed wfs i) prf) + +compileAllBranches tyWf tmWf fresh wfs wf Base = [<] +compileAllBranches tyWf tmWf fresh wfs wf (Step {l, x, as} i prf prfs) = + case lookupRecompute (MkRow as fresh) i of + Val i => case nameOf i of + Val _ => + compileAllBranches tyWf tmWf (dropElemFresh as fresh i) (dropAllWellFormed wfs i) wf prfs :< + (l :- (pretty x, compileChecks tyWf (tmWf :< (x :- indexAllWellFormed wfs i)) wf prf)) diff --git a/src/Inky/Term/Desugar.idr b/src/Inky/Term/Desugar.idr index 7051e4b..4bf8f05 100644 --- a/src/Inky/Term/Desugar.idr +++ b/src/Inky/Term/Desugar.idr @@ -2,8 +2,8 @@ module Inky.Term.Desugar import Data.List.Quantifiers import Data.Maybe -import Inky.Data.List -import Inky.Decidable +import Flap.Data.List +import Flap.Decidable import Inky.Term import Inky.Term.Substitution diff --git a/src/Inky/Term/Parser.idr b/src/Inky/Term/Parser.idr index 1c6eb58..4d68242 100644 --- a/src/Inky/Term/Parser.idr +++ b/src/Inky/Term/Parser.idr @@ -7,14 +7,15 @@ import Data.Nat import Data.List1 import Data.String -import Inky.Data.Context -import Inky.Data.Context.Var +import Flap.Data.Context +import Flap.Data.Context.Var +import Flap.Data.SnocList.Var +import Flap.Data.SnocList.Thinning +import Flap.Decidable +import Flap.Decidable.Maybe +import Flap.Parser + import Inky.Data.Row -import Inky.Data.SnocList.Var -import Inky.Data.SnocList.Thinning -import Inky.Decidable -import Inky.Decidable.Maybe -import Inky.Parser import Inky.Term import Inky.Type diff --git a/src/Inky/Term/Pretty/Error.idr b/src/Inky/Term/Pretty/Error.idr index bb19b2f..651d208 100644 --- a/src/Inky/Term/Pretty/Error.idr +++ b/src/Inky/Term/Pretty/Error.idr @@ -5,9 +5,10 @@ import Data.Singleton import Data.String import Data.These -import Inky.Decidable.Maybe +import Flap.Decidable.Maybe + import Inky.Term -import Inky.Term.Checks +import Inky.Term.Recompute import Inky.Type.Pretty import Text.PrettyPrint.Prettyprinter diff --git a/src/Inky/Term/Recompute.idr b/src/Inky/Term/Recompute.idr new file mode 100644 index 0000000..dd0e809 --- /dev/null +++ b/src/Inky/Term/Recompute.idr @@ -0,0 +1,128 @@ +module Inky.Term.Recompute + +import Data.List.Quantifiers +import Data.Singleton +import Inky.Term +import Inky.Type.Substitution + +%hide Prelude.Ops.infixl.(>=>) + +-- Can recompute arguments and result from function + +export +isFunctionRecompute : + {bound : List String} -> {a : Ty tyCtx} -> + {0 dom : All (Assoc0 $ Ty tyCtx) bound} -> + (0 _ : IsFunction bound a dom cod) -> (Singleton dom, Singleton cod) +isFunctionRecompute Done = (Val _, Val _) +isFunctionRecompute (Step {a} prf) = + mapFst (\case Val _ => Val _) $ isFunctionRecompute prf + +-- Can recompute type from synthesis proof + +export +synthsRecompute : + {tyEnv : _} -> {tmEnv : _} -> {e : _} -> + (0 _ : Synths tyEnv tmEnv e a) -> Singleton a +checkSpineRecompute : + {tyEnv : _} -> {tmEnv : _} -> {a : _} -> {ts : _} -> + (0 _ : CheckSpine tyEnv tmEnv a ts b) -> + Singleton b +allSynthsRecompute : + {tyEnv : _} -> {tmEnv : _} -> {es : Context _} -> + {0 as : Row (Ty [<])} -> + (0 _ : AllSynths tyEnv tmEnv es as) -> Singleton as + +synthsRecompute (AnnotS wf prf) = Val _ +synthsRecompute VarS = Val _ +synthsRecompute (LetS prf1 prf2) = + case synthsRecompute prf1 of + Val _ => synthsRecompute prf2 +synthsRecompute (LetTyS wf prf) = synthsRecompute prf +synthsRecompute (AppS prf prfs) = + case synthsRecompute prf of + Val _ => checkSpineRecompute prfs +synthsRecompute (TupS prfs) = + case allSynthsRecompute prfs of + Val _ => Val _ +synthsRecompute (PrjS {l, as} prf i) = + case synthsRecompute prf of + Val _ => case lookupRecompute as i of + Val i => [| (nameOf i).value |] +synthsRecompute (UnrollS prf) = + case synthsRecompute prf of + Val _ => Val _ +synthsRecompute (MapS f g h) = Val _ + +checkSpineRecompute [] = Val _ +checkSpineRecompute (prf :: prfs) = checkSpineRecompute prfs + +allSynthsRecompute [<] = Val _ +allSynthsRecompute (prfs :< prf) = + case (allSynthsRecompute prfs, synthsRecompute prf) of + (Val _, Val _) => Val _ + +-- Synthesised types are well-formed + +export +indexAllWellFormed : AllWellFormed as -> Elem (l :- a) as -> WellFormed a +indexAllWellFormed (wfs :< wf) Here = wf +indexAllWellFormed (wfs :< wf) (There i) = indexAllWellFormed wfs i + +export +dropAllWellFormed : AllWellFormed as -> (i : Elem (l :- a) as) -> AllWellFormed (dropElem as i) +dropAllWellFormed (wfs :< wf) Here = wfs +dropAllWellFormed (wfs :< wf) (There i) = dropAllWellFormed wfs i :< wf + +export +synthsWf : + {e : Term mode m tyCtx tmCtx} -> + {tyEnv : All (Assoc0 $ Ty [<]) tyCtx} -> + {tmEnv : All (Assoc0 $ Ty [<]) tmCtx} -> + DAll WellFormed tyEnv -> DAll WellFormed tmEnv -> + Synths tyEnv tmEnv e a -> WellFormed a +checkSpineWf : + CheckSpine tyEnv tmEnv a ts b -> + WellFormed a -> WellFormed b +allSynthsWf : + {es : Context (Term mode m tyCtx tmCtx)} -> + {tyEnv : All (Assoc0 $ Ty [<]) tyCtx} -> + {tmEnv : All (Assoc0 $ Ty [<]) tmCtx} -> + DAll WellFormed tyEnv -> DAll WellFormed tmEnv -> + AllSynths tyEnv tmEnv es as -> AllWellFormed as.context + +synthsWf tyWf tmWf (AnnotS wf prf) = subWf tyWf wf +synthsWf tyWf tmWf (VarS {i}) = indexDAll i.pos tmWf +synthsWf tyWf tmWf (LetS {x} prf1 prf2) = + case synthsRecompute prf1 of + Val _ => synthsWf tyWf (tmWf :< (x :- synthsWf tyWf tmWf prf1)) prf2 +synthsWf tyWf tmWf (LetTyS wf {x} prf) = + synthsWf (tyWf :< (x :- subWf tyWf wf)) tmWf prf +synthsWf tyWf tmWf (AppS prf prfs) = checkSpineWf prfs (synthsWf tyWf tmWf prf) +synthsWf tyWf tmWf (TupS prfs) = TProd (allSynthsWf tyWf tmWf prfs) +synthsWf tyWf tmWf (PrjS prf i) = + let TProd wfs = synthsWf tyWf tmWf prf in + indexAllWellFormed wfs i +synthsWf tyWf tmWf (UnrollS {x} prf) = + let TFix sp wf = synthsWf tyWf tmWf prf in + case synthsRecompute prf of + Val _ => subWf [ WellFormed a -> + (DAll WellFormed dom, WellFormed cod) +isFunctionWf Done wf = ([], wf) +isFunctionWf (Step {x} prf) (TArrow wf1 wf2) = mapFst ((x :- wf1) ::) $ isFunctionWf prf wf2 diff --git a/src/Inky/Term/Substitution.idr b/src/Inky/Term/Substitution.idr index 690e38c..c99f5e6 100644 --- a/src/Inky/Term/Substitution.idr +++ b/src/Inky/Term/Substitution.idr @@ -1,7 +1,7 @@ module Inky.Term.Substitution import Data.List.Quantifiers -import Inky.Data.List +import Flap.Data.List import Inky.Term public export diff --git a/src/Inky/Type.idr b/src/Inky/Type.idr index 8c46328..5cd0b03 100644 --- a/src/Inky/Type.idr +++ b/src/Inky/Type.idr @@ -1,17 +1,17 @@ module Inky.Type -import public Inky.Data.Context.Var +import public Flap.Data.Context.Var +import public Flap.Data.SnocList.Var import public Inky.Data.Row -import public Inky.Data.SnocList.Var import public Inky.Data.Thinned import Control.Function import Data.DPair import Data.These -import Inky.Data.SnocList.Thinning -import Inky.Decidable -import Inky.Decidable.Maybe +import Flap.Data.SnocList.Thinning +import Flap.Decidable +import Flap.Decidable.Maybe %hide Prelude.Ops.infixl.(>=>) @@ -191,11 +191,29 @@ thinId (TFix x a) = cong (TFix x) (trans (thinCong (KeepId IdId) a) (thinId a)) thinIdAll [<] = Refl thinIdAll (as :< (n :- a)) = cong2 (:<) (thinIdAll as) (cong (n :-) $ thinId a) -export +thinHomo : + (f : ctx2 `Thins` ctx3) -> (g : ctx1 `Thins` ctx2) -> (a : Ty ctx1) -> + thin f (thin g a) = thin (f . g) a +thinHomoAll : + (f : ctx2 `Thins` ctx3) -> (g : ctx1 `Thins` ctx2) -> (as : Context (Ty ctx1)) -> + thinAll f (thinAll g as) = thinAll (f . g) as + +thinHomo f g (TVar i) = cong (TVar . toVar) $ sym $ indexPosComp f g i.pos +thinHomo f g (TArrow a b) = cong2 TArrow (thinHomo f g a) (thinHomo f g b) +thinHomo f g (TProd (MkRow as fresh)) = cong TProd $ rowCong $ thinHomoAll f g as +thinHomo f g (TSum (MkRow as fresh)) = cong TSum $ rowCong $ thinHomoAll f g as +thinHomo f g (TFix x a) = cong (TFix x) $ thinHomo (Keep f) (Keep g) a + +thinHomoAll f g [<] = Refl +thinHomoAll f g (as :< (n :- a)) = + cong2 (:<) (thinHomoAll f g as) (cong (n :-) $ thinHomo f g a) + +public export Rename String Ty where rename = thin renameCong = thinCong renameId = thinId + renameHomo = thinHomo -- Alpha Equivalence ------------------------------------------------------------ @@ -521,14 +539,13 @@ namespace Strengthen data Strengthen : (i : Var ctx) -> Ty ctx -> Ty (dropElem ctx i.pos) -> Type public export data StrengthenAll : - (i : Var ctx) -> (as : Context (Ty ctx)) -> - All (Assoc0 $ Ty $ dropElem ctx i.pos) as.names -> Type + (i : Var ctx) -> Context (Ty ctx) -> Context (Ty $ dropElem ctx i.pos) -> Type data Strengthen where TVar : (j = index (dropPos i.pos) k) -> Strengthen i (TVar j) (TVar k) TArrow : Strengthen i a c -> Strengthen i b d -> Strengthen i (TArrow a b) (TArrow c d) - TProd : StrengthenAll i as.context bs -> Strengthen i (TProd as) (TProd $ fromAll bs as.fresh) - TSum : StrengthenAll i as.context bs -> Strengthen i (TSum as) (TSum $ fromAll bs as.fresh) + TProd : StrengthenAll i as.context bs.context -> Strengthen i (TProd as) (TProd bs) + TSum : StrengthenAll i as.context bs.context -> Strengthen i (TSum as) (TSum bs) TFix : Strengthen (ThereVar i) a b -> Strengthen i (TFix x a) (TFix x b) data StrengthenAll where @@ -538,13 +555,20 @@ namespace Strengthen %name Strengthen prf %name StrengthenAll prfs +export +strengthenAllNames : StrengthenAll i as bs -> bs.names = as.names +strengthenAllNames [<] = Refl +strengthenAllNames ((:<) prfs {l} prf) = cong (:< l) (strengthenAllNames prfs) + strengthenEq : Strengthen i a b -> a = thin (dropPos i.pos) b -strengthenAllEq : StrengthenAll i as bs -> as = thinAll (dropPos i.pos) (fromAll bs) +strengthenAllEq : StrengthenAll i as bs -> as = thinAll (dropPos i.pos) bs strengthenEq (TVar prf) = cong TVar prf strengthenEq (TArrow prf1 prf2) = cong2 TArrow (strengthenEq prf1) (strengthenEq prf2) -strengthenEq (TProd {as = MkRow _ _} prfs) = cong TProd $ rowCong $ strengthenAllEq prfs -strengthenEq (TSum {as = MkRow _ _} prfs) = cong TSum $ rowCong $ strengthenAllEq prfs +strengthenEq (TProd {as = MkRow _ _, bs = MkRow _ _} prfs) = + cong TProd $ rowCong $ strengthenAllEq prfs +strengthenEq (TSum {as = MkRow _ _, bs = MkRow _ _} prfs) = + cong TSum $ rowCong $ strengthenAllEq prfs strengthenEq (TFix prf) = cong (TFix _) $ strengthenEq prf strengthenAllEq [<] = Refl @@ -583,8 +607,8 @@ strengthenSplit (TVar Refl) (TVar {i = %% n} contra) = void $ lemma _ _ contra lemma : (i : Elem x sx) -> (j : Elem y (dropElem sx i)) -> Not (toVar i = toVar (indexPos (dropPos i) j)) - lemma Here j prf = absurd (toVarInjective prf) - lemma (There i) Here prf = absurd (toVarInjective prf) + lemma Here j prf = absurd @{HereThere} (toVarInjective prf) + lemma (There i) Here prf = absurd @{ThereHere} (toVarInjective prf) lemma (There i) (There j) prf = lemma i j $ toVarCong $ thereInjective $ toVarInjective prf strengthenSplit (TArrow prf1 prf2) (TArrow contras) = these (strengthenSplit prf1) (strengthenSplit prf2) (const $ strengthenSplit prf2) contras @@ -602,7 +626,9 @@ strengthen : export strengthenAll : (i : Var ctx) -> (as : Context (Ty ctx)) -> - Proof (All (Assoc0 $ Ty $ dropElem ctx i.pos) as.names) (StrengthenAll i as) (i `OccursInAny` as) + Proof (Subset (Context (Ty $ dropElem ctx i.pos)) (\bs => bs.names = as.names)) + (StrengthenAll i as . Subset.fst) + (i `OccursInAny` as) strengthen ((%%) x {pos = i}) (TVar ((%%) y {pos = j})) = map (TVar . toVar) @@ -613,18 +639,21 @@ strengthen i (TArrow a b) = map (uncurry TArrow) (\(c, d) => uncurry TArrow) TArrow $ all (strengthen i a) (strengthen i b) strengthen i (TProd (MkRow as fresh)) = - map (\bs => TProd $ fromAll bs fresh) (\_ => TProd) TProd $ + map (\bs => TProd $ MkRow (fst bs) (rewrite snd bs in fresh)) (\_ => TProd) TProd $ strengthenAll i as strengthen i (TSum (MkRow as fresh)) = - map (\bs => TSum $ fromAll bs fresh) (\_ => TSum) TSum $ + map (\bs => TSum $ MkRow (fst bs) (rewrite snd bs in fresh)) (\_ => TSum) TSum $ strengthenAll i as strengthen i (TFix x a) = map (TFix x) (\_ => TFix) TFix $ strengthen (ThereVar i) a -strengthenAll i [<] = Just [<] `Because` [<] +strengthenAll i [<] = Just (Element [<] Refl) `Because` [<] strengthenAll i (as :< (l :- a)) = - map (\x => snd x :< (l :- fst x)) (\(_, _) => uncurry (:<) . swap) (And . swap) $ + map + (\x => Element (fst (snd x) :< (l :- fst x)) (cong (:< l) (snd $ snd x))) + (\(_, _) => uncurry (:<) . swap) + (And . swap) $ all (strengthen i a) (strengthenAll i as) -- Not Strictly Positive ----------------------------------------------------------- @@ -678,6 +707,20 @@ export Uninhabited (i `NotPositiveInAny` [<]) where uninhabited (And contras) impossible +export +strongIsStrictlyPositive : Strengthen i a b -> i `StrictlyPositiveIn` a +allStrongIsAllStrictlyPositive : StrengthenAll i as bs -> i `StrictlyPositiveInAll` as + +strongIsStrictlyPositive (TVar prf) = TVar +strongIsStrictlyPositive (TArrow prf1 prf2) = TArrow (TArrow prf1 prf2) +strongIsStrictlyPositive (TProd prfs) = TProd (allStrongIsAllStrictlyPositive prfs) +strongIsStrictlyPositive (TSum prfs) = TSum (allStrongIsAllStrictlyPositive prfs) +strongIsStrictlyPositive (TFix prf) = TFix (strongIsStrictlyPositive prf) + +allStrongIsAllStrictlyPositive [<] = [<] +allStrongIsAllStrictlyPositive (prfs :< prf) = + allStrongIsAllStrictlyPositive prfs :< strongIsStrictlyPositive prf + export strictlyPositiveSplit : i `StrictlyPositiveIn` a -> i `NotPositiveIn` a -> Void strictlyPositiveAllSplit : i `StrictlyPositiveInAll` as -> i `NotPositiveInAny` as -> Void @@ -806,8 +849,8 @@ subAll : All (Assoc0 $ Thinned Ty ctx2) ctx1 -> Context (Ty ctx1) -> Context (Ty public export subAllNames : (f : All (Assoc0 $ Thinned Ty ctx2) ctx1) -> - (ctx : Context (Ty ctx1)) -> - (subAll f ctx).names = ctx.names + (env : Context (Ty ctx1)) -> + (subAll f env).names = env.names sub' env (TVar i) = (indexAll i.pos env).value.extract sub' env (TArrow a b) = TArrow (sub' env a) (sub' env b) diff --git a/src/Inky/Type/Pretty.idr b/src/Inky/Type/Pretty.idr index 2785b87..91b28ba 100644 --- a/src/Inky/Type/Pretty.idr +++ b/src/Inky/Type/Pretty.idr @@ -1,7 +1,7 @@ module Inky.Type.Pretty import Data.Singleton -import Inky.Decidable +import Flap.Decidable import Inky.Type import Text.PrettyPrint.Prettyprinter diff --git a/src/Inky/Type/Substitution.idr b/src/Inky/Type/Substitution.idr new file mode 100644 index 0000000..2a25d07 --- /dev/null +++ b/src/Inky/Type/Substitution.idr @@ -0,0 +1,364 @@ +module Inky.Type.Substitution + +import Data.List.Quantifiers +import Flap.Decidable.Maybe +import Inky.Type + +namespace SnocList + public export + data DAll : {0 ctx : SnocList String} -> (p : a -> Type) -> All (Assoc0 a) ctx -> Type where + Lin : DAll p [<] + (:<) : DAll p env -> Assoc0 p (n :- a) -> DAll p (env :< (n :- a)) + + %name DAll penv + + export + indexDAll : + {0 p : a -> Type} -> + (i : Elem x ctx) -> {0 env : All (Assoc0 a) ctx} -> + DAll p env -> p (indexAll i env).value + indexDAll Here (penv :< (l :- px)) = px + indexDAll (There i) (penv :< (l :- px)) = indexDAll i penv + + export + mapDProperty : + {0 p : a -> Type} -> + {0 q : b -> Type} -> + {0 f : a -> b} -> + (forall x. p x -> q (f x)) -> + DAll p env -> DAll q (mapProperty (map f) env) + mapDProperty g [<] = [<] + mapDProperty g (penv :< (l :- px)) = mapDProperty g penv :< (l :- g px) + +namespace List + public export + data DAll : {0 ctx : List String} -> (p : a -> Type) -> All (Assoc0 a) ctx -> Type where + Nil : DAll p [] + (::) : Assoc0 p (n :- a) -> List.DAll p env -> DAll p ((n :- a) :: env) + + %name List.DAll penv + +export +(<><) : DAll p env1 -> List.DAll p env2 -> DAll p (env1 <>< env2) +penv1 <>< [] = penv1 +penv1 <>< (px :: penv2) = (penv1 :< px) <>< penv2 + +indexAllMap : + {0 p, q : a -> Type} -> + (0 f : forall x. p x -> q x) -> + (i : Elem x sx) -> (env : All p sx) -> + indexAll i (mapProperty f env) = f (indexAll i env) +indexAllMap f Here (env :< px) = Refl +indexAllMap f (There i) (env :< px) = indexAllMap f i env + +-- Strengthening --------------------------------------------------------------- + +skipsStrengthens : + {f : ctx1 `Thins` ctx2} -> + f `Skips` i.pos -> + (a : Ty ctx1) -> + (b ** Strengthen i (thin f a) b) +skipsStrengthensAll : + {f : ctx1 `Thins` ctx2} -> + f `Skips` i.pos -> + (as : Context (Ty ctx1)) -> + (bs ** (StrengthenAll i (thinAll f as) bs, bs.names = as.names)) + +skipsStrengthens skips (TVar j) = + let (k ** eq) = strong f skips j.pos in + (TVar k ** TVar eq) + where + strong : + forall ctx1, ctx2. + (f : ctx1 `Thins` ctx2) -> {0 i : Elem y ctx2} -> + f `Skips` i -> (j : Elem x ctx1) -> (k ** toVar (indexPos f j) = index (dropPos i) k) + strong (Drop {sx, sy} f) Here j = (toVar (indexPos f j) ** Refl) + strong (Drop f) (Also skips) j = + let (k ** eq) = strong f skips j in + (ThereVar k ** cong ThereVar eq) + strong (Keep f) (There skips) Here = (toVar Here ** Refl) + strong (Keep f) (There skips) (There j) = + let (k ** eq) = strong f skips j in + (ThereVar k ** cong ThereVar eq) +skipsStrengthens skips (TArrow a b) = + let (a ** prf1) = skipsStrengthens skips a in + let (b ** prf2) = skipsStrengthens skips b in + (TArrow a b ** TArrow prf1 prf2) +skipsStrengthens skips (TProd (MkRow as fresh)) = + let (as ** (prfs, eq)) = skipsStrengthensAll skips as in + (TProd (MkRow as (rewrite eq in fresh)) ** TProd prfs) +skipsStrengthens skips (TSum (MkRow as fresh)) = + let (as ** (prfs, eq)) = skipsStrengthensAll skips as in + (TSum (MkRow as (rewrite eq in fresh)) ** TSum prfs) +skipsStrengthens skips (TFix x a) = + let (a ** prf) = skipsStrengthens (There skips) a in + (TFix x a ** TFix prf) + +skipsStrengthensAll skips [<] = ([<] ** ([<], Refl)) +skipsStrengthensAll skips (as :< (l :- a)) = + let (bs ** (prfs, eq)) = skipsStrengthensAll skips as in + let (b ** prf) = skipsStrengthens skips a in + (bs :< (l :- b) ** (prfs :< prf, cong (:< l) eq)) + +thinStrengthen : + (0 f : ctx1 `Thins` ctx2) -> + Strengthen i a b -> Strengthen (index f i) (thin f a) (thin (punchOut f i.pos) b) +thinAllStrengthen : + (0 f : ctx1 `Thins` ctx2) -> + StrengthenAll i as bs -> StrengthenAll (index f i) (thinAll f as) (thinAll (punchOut f i.pos) bs) + +thinStrengthen f (TVar {j, k} prf) = + TVar $ + rewrite sym $ indexPosComp (dropPos (indexPos f i.pos)) (punchOut f i.pos) k.pos in + rewrite (punchOutHomo f i.pos).indexPos k.pos in + rewrite indexPosComp f (dropPos i.pos) k.pos in + cong (index f) prf +thinStrengthen f (TArrow prf1 prf2) = TArrow (thinStrengthen f prf1) (thinStrengthen f prf2) +thinStrengthen f (TProd {as = MkRow _ _, bs = MkRow _ _} prfs) = TProd (thinAllStrengthen f prfs) +thinStrengthen f (TSum {as = MkRow _ _, bs = MkRow _ _} prfs) = TSum (thinAllStrengthen f prfs) +thinStrengthen f (TFix prf) = TFix (thinStrengthen (Keep f) prf) + +thinAllStrengthen f [<] = [<] +thinAllStrengthen f (prfs :< prf) = thinAllStrengthen f prfs :< thinStrengthen f prf + +sub'Strengthen : + {a : Ty ctx1} -> + {env : All (Assoc0 $ Thinned Ty ctx2) ctx1} -> + ((k : Var ctx1) -> + Proof (Ty (dropElem ctx2 j.pos)) + (Strengthen j (indexAll k.pos env).value.extract) + (i = k)) -> + Strengthen i a b -> + (c ** Strengthen j (sub' env a) c) +subAllStrengthen : + {as : Context (Ty ctx1)} -> + {env : All (Assoc0 $ Thinned Ty ctx2) ctx1} -> + ((k : Var ctx1) -> + Proof (Ty (dropElem ctx2 j.pos)) + (Strengthen j (indexAll k.pos env).value.extract) + (i = k)) -> + StrengthenAll i as bs -> + (cs ** (StrengthenAll j (subAll env as) cs, cs.names = as.names)) + +sub'Strengthen envStr (TVar {j = k1, k = k2} eq) = + case envStr k1 of + Just b `Because` prf => (b ** prf) + Nothing `Because` prf => + void $ + skipsSplit (dropPosSkips i.pos) k2.pos $ + replace {p = (\x => i.pos ~=~ x.pos)} + (trans prf eq) + Refl +sub'Strengthen envStr (TArrow prf1 prf2) = + let (a ** prf1) = sub'Strengthen envStr prf1 in + let (b ** prf2) = sub'Strengthen envStr prf2 in + (TArrow a b ** TArrow prf1 prf2) +sub'Strengthen envStr (TProd {as = MkRow as fresh} prfs) = + let (as ** (prfs, eq)) = subAllStrengthen envStr prfs in + (TProd (MkRow as (rewrite eq in fresh)) ** TProd prfs) +sub'Strengthen envStr (TSum {as = MkRow as fresh} prfs) = + let (as ** (prfs, eq)) = subAllStrengthen envStr prfs in + (TSum (MkRow as (rewrite eq in fresh)) ** TSum prfs) +sub'Strengthen envStr (TFix {x} prf) = + let (a ** prf) = sub'Strengthen envStr' prf in + (TFix x a ** TFix prf) + where + Env0 : All (Assoc0 $ Thinned Ty (ctx2 :< x)) ctx1 + Env0 = mapProperty (map $ rename $ Drop Id) env + + getEnv0 : (i : Elem y ctx1) -> indexAll i Env0 = map (rename $ Drop Id) (indexAll i env) + getEnv0 i = indexAllMap (map $ rename $ Drop Id) i env + + Env' : All (Assoc0 $ Thinned Ty (ctx2 :< x)) (ctx1 :< x) + Env' = Env0 :< (x :- (TVar (%% x) `Over` Id)) + + getEnv' : Var (ctx1 :< x) -> Ty (ctx2 :< x) + getEnv' i = (indexAll i.pos Env').value.extract + + envStr' : + (k : Var (ctx1 :< x)) -> + Proof (Ty (dropElem ctx2 j.pos :< x)) + (Strengthen (ThereVar j) (getEnv' k)) + (ThereVar i = k) + envStr' ((%%) _ {pos = Here}) = Just (TVar (%% x)) `Because` TVar Refl + envStr' ((%%) name {pos = There k}) = + map (thin $ Drop Id) + (\b, prf => + rewrite getEnv0 k in + rewrite sym $ extractHomo (Drop {x} Id) (indexAll k env).value in + thinStrengthen (Drop Id) prf) + (\eq => cong ThereVar eq) $ + envStr (%% name) + +subAllStrengthen envStr [<] = ([<] ** ([<], Refl)) +subAllStrengthen envStr ((:<) prfs {l} prf) = + let (cs ** (prfs, eq)) = subAllStrengthen envStr prfs in + let (c ** prf) = sub'Strengthen envStr prf in + (cs :< (l :- c) ** (prfs :< prf, cong (:< l) eq)) + +-- Strict Positivity ----------------------------------------------------------- + +thinStrictlyPositive : + (0 f : ctx1 `Thins` ctx2) -> + i `StrictlyPositiveIn` a -> + index f i `StrictlyPositiveIn` thin f a +thinAllStrictlyPositive : + (0 f : ctx1 `Thins` ctx2) -> + i `StrictlyPositiveInAll` as -> + index f i `StrictlyPositiveInAll` thinAll f as + +thinStrictlyPositive f TVar = TVar +thinStrictlyPositive f (TArrow prf) = TArrow (thinStrengthen f prf) +thinStrictlyPositive f (TProd {as = MkRow _ _} prfs) = TProd (thinAllStrictlyPositive f prfs) +thinStrictlyPositive f (TSum {as = MkRow _ _} prfs) = TSum (thinAllStrictlyPositive f prfs) +thinStrictlyPositive f (TFix prf) = TFix (thinStrictlyPositive (Keep f) prf) + +thinAllStrictlyPositive f [<] = [<] +thinAllStrictlyPositive f (prfs :< prf) = + thinAllStrictlyPositive f prfs :< thinStrictlyPositive f prf + +sub'StrictlyPositive : + {a : Ty ctx1} -> + {env : All (Assoc0 $ Thinned Ty ctx2) ctx1} -> + ((k : Var ctx1) -> + Proof (Ty (dropElem ctx2 j.pos)) + (Strengthen j (indexAll k.pos env).value.extract) + (i = k, j `StrictlyPositiveIn` (indexAll k.pos env).value.extract)) -> + i `StrictlyPositiveIn` a -> + j `StrictlyPositiveIn` sub' env a +subAllStrictlyPositive : + {as : Context (Ty ctx1)} -> + {env : All (Assoc0 $ Thinned Ty ctx2) ctx1} -> + ((k : Var ctx1) -> + Proof (Ty (dropElem ctx2 j.pos)) + (Strengthen j (indexAll k.pos env).value.extract) + (i = k, j `StrictlyPositiveIn` (indexAll k.pos env).value.extract)) -> + i `StrictlyPositiveInAll` as -> + j `StrictlyPositiveInAll` subAll env as + +sub'StrictlyPositive envSp (TVar {j = k}) = + case envSp k of + Just a `Because` prf => strongIsStrictlyPositive prf + Nothing `Because` (Refl, prf) => prf +sub'StrictlyPositive envSp (TArrow (TArrow prf1 prf2)) = + let envStr = \k => map id (\_ => id) fst $ envSp k in + let (_ ** str1) = sub'Strengthen envStr prf1 in + let (_ ** str2) = sub'Strengthen envStr prf2 in + TArrow (TArrow str1 str2) +sub'StrictlyPositive envSp (TProd {as = MkRow _ _} prfs) = TProd (subAllStrictlyPositive envSp prfs) +sub'StrictlyPositive envSp (TSum {as = MkRow _ _} prfs) = TSum (subAllStrictlyPositive envSp prfs) +sub'StrictlyPositive envSp (TFix {x} prf) = + TFix (sub'StrictlyPositive envSp' prf) + where + Env0 : All (Assoc0 $ Thinned Ty (ctx2 :< x)) ctx1 + Env0 = mapProperty (map $ rename $ Drop Id) env + + getEnv0 : (i : Elem y ctx1) -> indexAll i Env0 = map (rename $ Drop Id) (indexAll i env) + getEnv0 i = indexAllMap (map $ rename $ Drop Id) i env + + Env' : All (Assoc0 $ Thinned Ty (ctx2 :< x)) (ctx1 :< x) + Env' = Env0 :< (x :- (TVar (%% x) `Over` Id)) + + getEnv' : Var (ctx1 :< x) -> Ty (ctx2 :< x) + getEnv' i = (indexAll i.pos Env').value.extract + + envSp' : + (k : Var (ctx1 :< x)) -> + Proof (Ty (dropElem ctx2 j.pos :< x)) + (Strengthen (ThereVar j) (getEnv' k)) + (ThereVar i = k, ThereVar j `StrictlyPositiveIn` (getEnv' k)) + envSp' ((%%) _ {pos = Here}) = Just (TVar (%% x)) `Because` TVar Refl + envSp' ((%%) name {pos = There k}) = + map (thin $ Drop Id) + (\b, prf => + rewrite getEnv0 k in + rewrite sym $ extractHomo (Drop {x} Id) (indexAll k env).value in + thinStrengthen (Drop Id) prf) + (\(eq, prf) => + ( cong ThereVar eq + , rewrite getEnv0 k in + rewrite sym $ extractHomo (Drop {x} Id) (indexAll k env).value in + thinStrictlyPositive (Drop Id) prf + )) $ + envSp (%% name) + +subAllStrictlyPositive envSp [<] = [<] +subAllStrictlyPositive envSp (prfs :< prf) = + subAllStrictlyPositive envSp prfs :< sub'StrictlyPositive envSp prf + +-- Well Formedness ------------------------------------------------------------- + +thinWf : (0 f : ctx1 `Thins` ctx2) -> WellFormed a -> WellFormed (thin f a) +thinAllWf : (0 f : ctx1 `Thins` ctx2) -> AllWellFormed as -> AllWellFormed (thinAll f as) + +thinWf f TVar = TVar +thinWf f (TArrow wf1 wf2) = TArrow (thinWf f wf1) (thinWf f wf2) +thinWf f (TProd {as = MkRow _ _} wfs) = TProd (thinAllWf f wfs) +thinWf f (TSum {as = MkRow _ _} wfs) = TSum (thinAllWf f wfs) +thinWf f (TFix prf wf) = TFix (thinStrictlyPositive (Keep f) prf) (thinWf (Keep f) wf) + +thinAllWf f [<] = [<] +thinAllWf f (wfs :< wf) = thinAllWf f wfs :< thinWf f wf + +sub'Wf : + {a : Ty ctx1} -> + {env : All (Assoc0 $ Thinned Ty ctx2) ctx1} -> + DAll (\ty => WellFormed ty.value) env -> + WellFormed a -> + WellFormed (sub' env a) +subAllWf : + {as : Context (Ty ctx1)} -> + {env : All (Assoc0 $ Thinned Ty ctx2) ctx1} -> + DAll (\ty => WellFormed ty.value) env -> + AllWellFormed as -> + AllWellFormed (subAll env as) + +sub'Wf envWf (TVar {i}) = + thinWf (indexAll i.pos env).value.thins (indexDAll i.pos envWf) +sub'Wf envWf (TArrow wf1 wf2) = TArrow (sub'Wf envWf wf1) (sub'Wf envWf wf2) +sub'Wf envWf (TProd {as = MkRow _ _} wfs) = TProd (subAllWf envWf wfs) +sub'Wf envWf (TSum {as = MkRow _ _} wfs) = TSum (subAllWf envWf wfs) +sub'Wf envWf (TFix {x} prf wf) = + TFix + (sub'StrictlyPositive envSp prf) + (sub'Wf (mapDProperty {f = rename (Drop Id)} id envWf :< (x :- TVar)) wf) + where + Env0 : All (Assoc0 $ Thinned Ty (ctx2 :< x)) ctx1 + Env0 = mapProperty (map $ rename $ Drop Id) env + + getEnv0 : (i : Elem y ctx1) -> indexAll i Env0 = map (rename $ Drop Id) (indexAll i env) + getEnv0 i = indexAllMap (map $ rename $ Drop Id) i env + + Env' : All (Assoc0 $ Thinned Ty (ctx2 :< x)) (ctx1 :< x) + Env' = Env0 :< (x :- (TVar (%% x) `Over` Id)) + + getEnv' : Var (ctx1 :< x) -> Ty (ctx2 :< x) + getEnv' i = (indexAll i.pos Env').value.extract + + envSp : + (k : Var (ctx1 :< x)) -> + Proof (Ty ctx2) + (Strengthen (%% x) (getEnv' k)) + ((%% x) = k, (%% x) `StrictlyPositiveIn` (getEnv' k)) + envSp ((%%) _ {pos = Here}) = Nothing `Because` (Refl, TVar) + envSp ((%%) name {pos = There i}) = + let + (b ** prf) = + skipsStrengthens + {f = (indexAll i Env0).value.thins} + (rewrite getEnv0 i in Here) + _ + in + Just b `Because` prf + +subAllWf envWf [<] = [<] +subAllWf envWf (wfs :< wf) = subAllWf envWf wfs :< sub'Wf envWf wf + +export +subWf : + {a : Ty ctx1} -> + {env : All (Assoc0 $ Ty ctx2) ctx1} -> + DAll (\ty => WellFormed ty) env -> + WellFormed a -> + WellFormed (sub env a) +subWf envWf = sub'Wf (mapDProperty id envWf) -- cgit v1.2.3