Add compilation to scheme.

Extract parser as an independent project.

4 files changed, 0 insertions, 478 deletions

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