Add encodings for containers.

Remove useless junk.

10 files changed, 269 insertions, 71 deletions

diff --git a/church-eval.ipkg b/church-eval.ipkg
index c2a0fbb..242470b 100644
--- a/church-eval.ipkg
+++ b/church-eval.ipkg
@@ -9,6 +9,7 @@ depends = contrib
 modules
   = Encoded.Arith
   , Encoded.Bool
+  , Encoded.Container
   , Encoded.Fin
   , Encoded.Pair
   , Encoded.Sum
diff --git a/src/Encoded/Arith.idr b/src/Encoded/Arith.idr
index d2f83bc..fe9bc68 100644
--- a/src/Encoded/Arith.idr
+++ b/src/Encoded/Arith.idr
@@ -32,10 +32,15 @@ pred = Abs'
   (\n => App
     (Rec n
       (Const Zero)
-      (Abs' (\f =>
-        Rec (App f [<Zero])
-          (Abs' (\k => Rec k (Suc Zero) (Const Zero)))
-          (Const $ Abs' (\k => Rec k (Suc Zero) (Abs' Suc . shift f))))))
+      (Abs $ Abs $
+        let f = Var (There Here) in
+        let k = Var Here in
+        Rec k
+          (Lit 1)
+          (Const $
+            Rec (App f [<Zero])
+              Zero
+              (Const $ Suc $ App f [<Lit 1]))))
     [<Lit 1])
 
 export
@@ -76,6 +81,6 @@ divmod = Abs $ Abs $
     (App pair [<Zero, Zero])
     (Abs' (\p =>
       App if'
-        [<App lte [<shift d, App snd [<p]]
+        [<App lte [<shift d, Suc (App snd [<p])]
         , App pair [<Suc (App fst [<p]), Zero]
         , App mapSnd [<Abs' Suc, p]]))
diff --git a/src/Encoded/Bool.idr b/src/Encoded/Bool.idr
index 11bb894..778f65d 100644
--- a/src/Encoded/Bool.idr
+++ b/src/Encoded/Bool.idr
@@ -1,6 +1,5 @@
 module Encoded.Bool
 
-import Term.Semantics
 import Term.Syntax
 
 export
@@ -8,15 +7,6 @@ B : Ty
 B = N
 
 export
-Show (TypeOf B) where
-  show 0 = "true"
-  show (S k) = "false"
-
-export
-toBool : TypeOf B -> Bool
-toBool = (== 0)
-
-export
 True : Term B ctx
 True = Lit 0
   
diff --git a/src/Encoded/Container.idr b/src/Encoded/Container.idr
new file mode 100644
index 0000000..1334bc2
--- /dev/null
+++ b/src/Encoded/Container.idr
@@ -0,0 +1,208 @@
+module Encoded.Container
+
+import Encoded.Arith
+import Encoded.Bool
+import Encoded.Fin
+import Encoded.Pair
+import Encoded.Sum
+import Encoded.Vect
+import Term.Syntax
+
+%ambiguity_depth 4
+%prefix_record_projections off
+
+public export
+Case : Type
+Case = (Maybe Ty, Nat)
+
+public export
+record Container where
+  constructor Cases
+  constructors : SnocList Case
+  {auto 0 ok : NonEmpty constructors}
+
+%name Container c
+
+public export
+semCase : Case -> Ty -> Ty
+semCase (Just tag, k) ty = tag * Vect k ty
+semCase (Nothing, k) ty = Vect k ty
+
+public export
+sem : Container -> Ty -> Ty
+sem c ty = Sum (map (flip semCase ty) c.constructors) @{mapNonEmpty c.ok}
+
+unitCase : Case -> Ty
+unitCase (Just tag, k) = tag
+unitCase (Nothing, k) = N
+
+unitSem : Container -> Ty
+unitSem c = Sum (map unitCase c.constructors) @{mapNonEmpty c.ok}
+
+dmapCase :
+  {c : Case} ->
+  {ty, ty' : Ty} ->
+  Term ((Fin (snd c) ~> ty ~> ty') ~> semCase c ty ~> semCase c ty') ctx
+dmapCase {c = (Just tag, k)} = Abs' (\f => App (mapSnd . dmap) [<f])
+dmapCase {c = (Nothing, k)} = dmap
+
+forgetCase : {c : Case} -> {ty : Ty} -> Term (semCase c ty ~> unitCase c) ctx
+forgetCase {c = (Just tag, k)} = fst
+forgetCase {c = (Nothing, k)} = Arb
+
+recurse : {c : Case} -> {ty : Ty} -> Term (semCase c ty ~> Vect (snd c) ty) ctx
+recurse {c = (Just tag, k)} = snd
+recurse {c = (Nothing, k)} = Id
+
+export
+W : Container -> Ty
+W c = N * (N ~> N * N) * (N ~> unitSem c)
+--    ^   ^              ^- data
+--    |   + index mapping function: each index has a different base and stride
+--    +- pred(fuel) for induction
+
+fuel : {c : Container} -> Term (W c ~> N) ctx
+fuel = fst . fst
+
+offset : {c : Container} -> Term (W c ~> N ~> N * N) ctx
+offset = snd . fst
+
+vals : {c : Container} -> Term (W c ~> N ~> unitSem c) ctx
+vals = snd
+
+-- Adds a value to the start of a stream
+cons : {ty : Ty} -> Term (ty ~> (N ~> ty) ~> (N ~> ty)) ctx
+cons = Abs $ Abs $ Abs $
+  let x = Var (There $ There Here) in
+  let xs = Var (There Here) in
+  let n = Var Here in
+  App rec [<n, x, xs . fst]
+
+-- Calculates total fuel for a new W value.
+getFuel :
+  {cont : Container} ->
+  {c : Case} ->
+  Term (semCase c (W cont) ~> N) ctx
+getFuel {c = (tag, k)} = App foldr [<Zero, plus] . App map [<Abs' Suc . fuel] . recurse
+
+-- Updates the base and stride for a single recursive position.
+-- These are multiplexed later.
+stepOffset : {k : Nat} -> Term (Fin k ~> (N ~> N * N) ~> (N ~> N * N)) ctx
+stepOffset = Abs $ Abs $ Abs $
+  let i = Var (There $ There Here) in
+  let f = Var (There Here) in
+  let x = Var Here in
+  App bimap
+    -- Suc is for the initial tag
+    [<App (plus . forget . suc) [<i] . App mult [<Lit k]
+    , App mult [<Lit k]
+    , App f [<x]
+    ]
+
+-- Calculates all offsets for a new W value.
+getOffset :
+  {cont : Container} ->
+  {c : Case} ->
+  Term (semCase c (W cont) ~> N ~> N * N) ctx
+getOffset {c = (tag, 0)} = Const $ Const $ App pair [<Lit 1, Zero]
+getOffset {c = (tag, k@(S _))} = Abs' (\x =>
+  App cons
+    [<App pair [<Lit 1, Zero]
+    , Abs' (\n =>
+      let dm = App (divmod' k) [<n] in
+      let div = App fst [<dm] in
+      let mod = App snd [<dm] in
+      App stepOffset [<mod, App offset [<App (index . recurse) [<shift x, mod]], div])
+    ])
+
+-- Calculates data map for a new W value.
+getVals :
+  {cont : Container} ->
+  {c : Case} ->
+  (i : Elem c cont.constructors) ->
+  Term (semCase c (W cont) ~> N ~> unitSem cont) ctx
+getVals i {c = (tag', 0)} =
+  Abs' (\x => Const $ App (tag @{mapNonEmpty cont.ok} (elemMap unitCase i) . forgetCase) [<x])
+getVals i {c = (tag', k@(S _))} = Abs' (\x =>
+  App Container.cons
+    [<App (tag @{mapNonEmpty cont.ok} (elemMap unitCase i) . forgetCase) [<x]
+    , Abs' (\n =>
+      let dm = App (divmod' k) [<n] in
+      let div = App fst [<dm] in
+      let mod = App snd [<dm] in
+      App vals [<App (index . recurse) [<shift x, mod], div])
+    ])
+
+-- Constructs a value for a specific constructor
+introCase :
+  {cont : Container} ->
+  {c : Case} ->
+  (i : Elem c cont.constructors) ->
+  Term (semCase c (W cont) ~> W cont) ctx
+introCase i = Abs' (\x =>
+  App pair [<App pair [<App getFuel [<x], App getOffset [<x]], App (getVals i) [<x]])
+
+gtabulate : {sx : SnocList a} -> ({x : a} -> Elem x sx -> p (f x)) -> All p (map f sx)
+gtabulate {sx = [<]} g = [<]
+gtabulate {sx = sx :< x} g = gtabulate (g . There) :< g Here
+
+export
+intro : {c : Container} -> Term (sem c (W c) ~> W c) ctx
+intro =
+  App (any @{mapNonEmpty c.ok}) {sty = map (~> W c) $ map (flip semCase (W c)) c.constructors} $
+  rewrite mapFusion (~> W c) (flip semCase (W c)) c.constructors in
+  gtabulate introCase
+
+calcIndex : Term (N * N ~> N ~> N) ctx
+calcIndex = Abs' (\bs => App (plus . fst) [<bs] . App (mult . snd) [<bs])
+
+fillCase :
+  {c : Case} ->
+  {ty : Ty} ->
+  Term ((Fin (snd c) ~> ty) ~> (semCase c ty ~> ty) ~> unitCase c ~> ty) ctx
+fillCase {c = (Just tag, k)} = Abs $ Abs $ Abs $
+  let f = Var (There $ There Here) in
+  let sem = Var (There Here) in
+  let val = Var Here in
+  App sem [<App pair [<val, App tabulate [<f]]]
+fillCase {c = (Nothing, k)} =
+  Abs $ Abs $ Const $
+  let f = Var (There Here) in
+  let sem = Var Here in
+  App (sem . tabulate) [<f]
+
+elimStep :
+  {c : Container} ->
+  {ty : Ty} ->
+  Term
+    (map (\c => semCase c ty ~> ty) c.constructors ~>*
+     (N ~> N * N) ~>
+     (N ~> unitSem c) ~>
+     (N ~> ty) ~>
+     (N ~> ty))
+    ctx
+elimStep = AbsAll (_ :< _ :< _ :< _ :< _)
+  (\(fs :< offsets :< vals :< rec :< n) =>
+    let val = App vals [<n] in
+    let offset = App offsets [<n] in
+    App (any @{mapNonEmpty c.ok}) {sty = map (~> ty) (map unitCase c.constructors) :< unitSem c} $
+    rewrite mapFusion (~> ty) unitCase c.constructors in
+    gtabulate (\i =>
+      Syntax.App fillCase
+        [<rec . App calcIndex [<offset] . forget
+        , indexAll (elemMap (\c => semCase c ty ~> ty) i) fs
+        ]) :<
+    val)
+
+export
+elim :
+  {c : Container} ->
+  {ty : Ty} ->
+  Term (map (\c => semCase c ty ~> ty) c.constructors ~>* W c ~> ty) ctx
+elim = AbsAll (_ :< _)
+  (\(fs :< x) =>
+    App
+      (Rec (App fuel [<x])
+        Arb
+        (App elimStep (fs :< App offset [<x] :< App vals [<x])))
+      [<Zero])
diff --git a/src/Encoded/Fin.idr b/src/Encoded/Fin.idr
index 901c612..0029760 100644
--- a/src/Encoded/Fin.idr
+++ b/src/Encoded/Fin.idr
@@ -5,7 +5,6 @@ import public Data.Nat
 import Data.Stream
 import Encoded.Arith
 import Encoded.Pair
-import Term.Semantics
 import Term.Syntax
 
 export
@@ -40,9 +39,5 @@ forget : Term (Fin k ~> N) ctx
 forget = Id
 
 export
-allSem : (k : Nat) -> List (TypeOf (Fin k))
-allSem k = take k nats
-
-export
 divmod' : (k : Nat) -> {auto 0 ok : NonZero k} -> Term (N ~> N * Fin k) ctx
 divmod' k = Abs' (\n => App divmod [<n, Lit k])
diff --git a/src/Encoded/Pair.idr b/src/Encoded/Pair.idr
index 32bb06c..42adde5 100644
--- a/src/Encoded/Pair.idr
+++ b/src/Encoded/Pair.idr
@@ -2,7 +2,6 @@ module Encoded.Pair
 
 import Encoded.Bool
 import Encoded.Union
-import Term.Semantics
 import Term.Syntax
 
 export
@@ -10,17 +9,6 @@ export
 ty1 * ty2 = B ~> (ty1 <+> ty2)
 
 export
-[ShowPair]
-{ty1, ty2 : Ty} ->
-Show (TypeOf ty1) =>
-Show (TypeOf ty2) =>
-Show (TypeOf (ty1 * ty2)) where
-  show f = fastConcat
-    [ "(", show (sem prL [<] (f $ sem True [<]))
-    , ", ", show (sem prR [<] (f $ sem False [<]))
-    , ")"]
-
-export
 pair : {ty1, ty2 : Ty} -> Term (ty1 ~> ty2 ~> (ty1 * ty2)) ctx
 pair = Abs $ Abs $ Abs $
   let t = Var (There $ There Here) in
diff --git a/src/Encoded/Sum.idr b/src/Encoded/Sum.idr
index e3729f9..6c6da6a 100644
--- a/src/Encoded/Sum.idr
+++ b/src/Encoded/Sum.idr
@@ -1,13 +1,10 @@
 module Encoded.Sum
 
-import public Data.List
-import public Data.List.Elem
-import public Data.List.Quantifiers
+import public Data.SnocList.Operations
 
 import Encoded.Bool
 import Encoded.Pair
 import Encoded.Union
-import Term.Semantics
 import Term.Syntax
 
 -- Binary Sums -----------------------------------------------------------------
@@ -17,13 +14,6 @@ export
 ty1 + ty2 = B * (ty1 <+> ty2)
 
 export
-{ty1, ty2 : Ty} -> Show (TypeOf ty1) => Show (TypeOf ty2) => Show (TypeOf (ty1 + ty2)) where
-  show p =
-    if toBool (sem fst [<] p)
-    then fastConcat ["Left (", show (sem (prL . snd) [<] p), ")"]
-    else fastConcat ["Right (", show (sem (prR . snd) [<] p), ")"]
-
-export
 left : {ty1, ty2 : Ty} -> Term (ty1 ~> (ty1 + ty2)) ctx
 left = Abs' (\t => App pair [<True, App inL [<t]])
 
@@ -51,30 +41,36 @@ either = Abs $ Abs $ Abs $
 -- N-ary Sums ------------------------------------------------------------------
 
 public export
-mapNonEmpty : NonEmpty xs -> NonEmpty (map f xs)
-mapNonEmpty IsNonEmpty = IsNonEmpty
+mapNonEmpty : NonEmpty sx -> NonEmpty (map f sx)
+mapNonEmpty IsSnoc = IsSnoc
 
 export
-Sum : (tys : List Ty) -> {auto 0 ok : NonEmpty tys} -> Ty
-Sum = foldr1 (+)
+Sum : (sty : SnocList Ty) -> {auto 0 ok : NonEmpty sty} -> Ty
+Sum [<ty] = ty
+Sum (sty@(_ :< _) :< ty) = Sum sty + ty
 
 export
 any :
-  {tys : List Ty} ->
+  {sty : SnocList Ty} ->
   {ty : Ty} ->
-  {auto 0 ok : NonEmpty tys} ->
-  All (\ty' => Term (ty' ~> ty) ctx) tys ->
-  Term (Sum tys ~> ty) ctx
-any [f] = f
-any (f :: fs@(_ :: _)) = App either [<f, any fs]
+  {auto 0 ok : NonEmpty sty} ->
+  Term (map (~> ty) sty ~>* Sum sty ~> ty) ctx
+any {sty = [<ty']} = Id
+any {sty = sty :< ty'' :< ty'} =
+  Abs (Abs $ Abs $
+    let rec = Var (There $ There Here) in
+    let f = Var (There Here) in
+    let g = Var Here in
+    App either [<App rec [<f], g]) .:
+  any {sty = sty :< ty''}
 
 export
 tag :
-  {tys : List Ty} ->
+  {sty : SnocList Ty} ->
   {ty : Ty} ->
-  {auto 0 ok : NonEmpty tys} ->
-  Elem ty tys ->
-  Term (ty ~> Sum tys) ctx
-tag {tys = [_]} Here = Id
-tag {tys = _ :: _ :: _} Here = left
-tag {tys = _ :: _ :: _} (There i) = right . tag i
+  {auto 0 ok : NonEmpty sty} ->
+  Elem ty sty ->
+  Term (ty ~> Sum sty) ctx
+tag {sty = [<ty]} Here = Id
+tag {sty = sty :< ty' :< ty} Here = right
+tag {sty = sty :< ty'' :< ty'} (There i) = left . tag i
diff --git a/src/Encoded/Vect.idr b/src/Encoded/Vect.idr
index a427196..064de5f 100644
--- a/src/Encoded/Vect.idr
+++ b/src/Encoded/Vect.idr
@@ -6,7 +6,6 @@ import Encoded.Bool
 import Encoded.Pair
 import Encoded.Fin
 
-import Term.Semantics
 import Term.Syntax
 
 export
@@ -14,13 +13,6 @@ Vect : Nat -> Ty -> Ty
 Vect k ty = Fin k ~> ty
 
 export
-[ShowVect]
-{k : Nat} ->
-Show (TypeOf ty) =>
-Show (TypeOf (Vect k ty)) where
-  show f = "[" ++ joinBy ", " (map (show . f) $ allSem k) ++ "]"
-
-export
 nil : {ty : Ty} -> Term (Vect 0 ty) ctx
 nil = absurd
 
diff --git a/src/Term/Pretty.idr b/src/Term/Pretty.idr
index ed2dd45..ffa88bd 100644
--- a/src/Term/Pretty.idr
+++ b/src/Term/Pretty.idr
@@ -51,6 +51,10 @@ interface Renderable (0 a : Type) where
   fromSyntax : Syntax -> a
 
 export
+Renderable () where
+  fromSyntax _ = ()
+
+export
 Renderable AnsiStyle where
   fromSyntax Bound = italic
   fromSyntax Keyword  = color Blue
@@ -150,7 +154,6 @@ parameters (names : Stream String)
   prettyFullTerm : (len : Len ctx) => Prec -> FullTerm ty ctx' -> ctx' `Thins` ctx -> Doc Syntax
   prettyBinding : (len : Len ctx) => Prec -> Binding ty ctx' -> ctx' `Thins` ctx -> Doc Syntax
   prettySpline : (len : Len ctx) => Prec -> Spline ty ctx -> Doc Syntax
-  prettyArg : (len : Len ctx) => Term ty ctx' -> Doc Syntax
 
   prettyTerm' d (t `Over` thin) = prettyFullTerm d t thin
 
@@ -239,7 +242,7 @@ name k =
 
 export
 canonicalNames : Stream String
-canonicalNames = map (fastPack . name) nats
+canonicalNames = map (fastPack . reverse . name) nats
 
 export
 prettyTerm : Renderable ann => (len : Len ctx) => Term ty ctx -> Doc ann
diff --git a/src/Term/Syntax.idr b/src/Term/Syntax.idr
index 6a05271..211e039 100644
--- a/src/Term/Syntax.idr
+++ b/src/Term/Syntax.idr
@@ -23,7 +23,7 @@ Lit (S k) = Suc (Lit k)
 
 -- HOAS
 
-infix 4 ~>*
+infixr 4 ~>*
 
 public export
 (~>*) : SnocList Ty -> Ty -> Ty
@@ -39,9 +39,27 @@ App t [<] = t
 App t (us :< u) = App (App t us) u
 
 export
+AbsAll :
+  (sty : SnocList Ty) ->
+  (All (flip Term (ctx ++ sty)) sty -> Term ty (ctx ++ sty)) ->
+  Term (sty ~>* ty) ctx
+AbsAll [<] f = f [<]
+AbsAll (sty :< ty') f = AbsAll sty (\vars => Abs' (\x => f (mapProperty shift vars :< x)))
+
+export
 (.) : {ty, ty' : Ty} -> Term (ty' ~> ty'') ctx -> Term (ty ~> ty') ctx -> Term (ty ~> ty'') ctx
 t . u = Abs (App (shift t) [<App (shift u) [<Var Here]])
 
+export
+(.:) :
+  {sty : SnocList Ty} ->
+  {ty : Ty} ->
+  Term (ty ~> ty') ctx ->
+  Term (sty ~>* ty) ctx ->
+  Term (sty ~>* ty') ctx
+(t .: u) {sty = [<]} = App t u
+(t .: u) {sty = sty :< ty''} = Abs' (\f => shift t . f) .: u
+
 -- Incomplete Evaluation
 
 data IsFunc : FullTerm (ty ~> ty') ctx -> Type where
@@ -112,6 +130,8 @@ Rec' Zero thin u v = Just u
 Rec' (Suc t) thin u v =
   let rec = maybe (Rec (t `Over` thin) u v) id (Rec' t thin u v) in
   Just $ maybe (App v rec) id $ (App' 1 v rec)
+Rec' t thin (Zero `Over` thin1) (Const Zero `Over` thin2) =
+  Just (Zero `Over` Empty)
 Rec' t thin u v = Nothing
 
 eval' : {ty : Ty} -> (fuel : Nat) -> (ratio : Double) -> Term ty ctx -> (Nat, Term ty ctx)