Fix some bug?

I don't really know. I haven't read this in a long time.

8 files changed, 215 insertions, 105 deletions

diff --git a/src/Encoded/Container.idr b/src/Encoded/Container.idr
index 800623a..a290524 100644
--- a/src/Encoded/Container.idr
+++ b/src/Encoded/Container.idr
@@ -8,36 +8,41 @@ import Encoded.Sum
 import Encoded.Vect
 import Term.Syntax
 
-%ambiguity_depth 4
+%ambiguity_depth 6
 %prefix_record_projections off
 
+-- Utilities -------------------------------------------------------------------
+
+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
+
+-- 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]
+
+-- Cases -----------------------------------------------------------------------
+
 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}
+forgetCase : {c : Case} -> {ty : Ty} -> Term (semCase c ty ~> unitCase c) ctx
+forgetCase {c = (Just tag, k)} = fst
+forgetCase {c = (Nothing, k)} = Arb
 
 dmapCase :
   {c : Case} ->
@@ -46,71 +51,150 @@ dmapCase :
 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
+children : {c : Case} -> {ty : Ty} -> Term (semCase c ty ~> Vect (snd c) ty) ctx
+children {c = (Just tag, k)} = snd
+children {c = (Nothing, k)} = Id
+
+-- Containers ------------------------------------------------------------------
+
+public export
+record Container where
+  constructor Cases
+  constructors : SnocList Case
+  {auto 0 ok : NonEmpty constructors}
 
-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
+%name Container c
+
+public export
+sem : Container -> Ty -> Ty
+sem c ty = Sum (map (flip semCase ty) c.constructors) @{mapNonEmpty c.ok}
+
+unitSem : Container -> Ty
+unitSem c = Sum (map unitCase c.constructors) @{mapNonEmpty c.ok}
+
+-- Fixed Point ----------------------------------------------------------------
 
 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
+W c = (N ~> N * unitSem c * N * N)
+--          ^   ^- data     ^   ^- stride
+--          +- fuel         +- base
 
-fuel : {c : Container} -> Term (W c ~> N) ctx
-fuel = fst . fst
+fuelAt : {c : Container} -> Term (W c ~> N ~> N) ctx
+fuelAt = Abs' (\c => fst . fst . fst . c)
 
-offset : {c : Container} -> Term (W c ~> N ~> N * N) ctx
-offset = snd . fst
+fuel : {c : Container} -> Term (W c ~> N) ctx
+fuel = Abs' (\c => App fuelAt [<c, 0])
 
 vals : {c : Container} -> Term (W c ~> N ~> unitSem c) ctx
-vals = snd
+vals = Abs' (\c => snd . fst . fst . c)
 
--- 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]
+base : {c : Container} -> Term (W c ~> N ~> N) ctx
+base = Abs' (\c => snd . fst . c)
+
+stride : {c : Container} -> Term (W c ~> N ~> N) ctx
+stride = Abs' (\c => snd . c)
+
+calcIndex : Term (N ~> N ~> N ~> N) ctx
+calcIndex = AbsAll [<_,_,_] (\[<base, stride, n] => base + stride * n)
+
+reroot : {c : Container} -> Term (W c ~> N ~> W c) ctx
+reroot = AbsAll [<_,_] (\[<x, n] =>
+  App Container.cons
+    [<App pair
+      [<App pair
+      [<App pair
+      [<App fuelAt [<x, n]
+      , App vals [<x, n]]
+      , 1]
+      , 1]
+    , Abs' (\y =>
+        let base' = shift (App base [<x, n]) in
+        let stride' = shift (App stride [<x, n]) in
+        App
+          (Abs' (\z =>
+            App pair
+            [<App pair
+            [<App pair
+            [<App fuelAt [<shift (shift x), z]
+            , App vals [<shift (shift x), z]]
+            , (App base [<shift (shift x), z] `minus` shift base') `div` shift stride']
+            , App stride [<shift (shift x), z] `div` shift stride']))
+          [<App calcIndex [<base', stride', y]])
+    ])
 
--- Calculates total fuel for a new W value.
+-- Introductor -----------------------------------------------------------------
+
+-- Calculates all fuels for a new W value.
 getFuel :
   {cont : Container} ->
   {c : Case} ->
-  Term (semCase c (W cont) ~> N) ctx
-getFuel {c = (tag, k)} = App foldr [<Zero, Op 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 = AbsAll [<_,_,_] (\[<i, f, x] =>
-  App bimap
-    -- Suc is for the initial tag
-    [<Abs' (\n => Suc $ App forget [<shift i] + Op (Lit k) * n)
-    , Abs' (\n => Op (Lit k) * n)
-    , App f [<x]
-    ])
+  Term (semCase c (W cont) ~> N ~> N) ctx
+getFuel {c = (tag, 0)} =
+  -- One tag in total
+  Const (Const 1)
+getFuel {c = (tag, k@(S _))} =
+  Abs' (\x =>
+    App Container.cons
+      [<App (App foldr [<Zero, Op Plus] . App map [<Abs' Suc . fuel] . children) [<x] -- total fuel
+      , Abs'
+        (\n =>
+          -- fuel (1 + i + k z) => fuel_i (z)
+          -- The initial (1 +) is a consequence of the cons.
+          let dm = App (divmod' k) [<n] in
+          let z = App fst [<dm] in
+          let i = App snd [<dm] in
+          let child = App (index . children) [<shift x, i] in
+          App fuelAt [<child, z]
+          )])
+  -- App foldr [<Zero, Op Plus] . App map [<Abs' Suc . fuel] . children
 
 -- Calculates all offsets for a new W value.
-getOffset :
+-- This gives the base and stride for looking up the _children_ of a node.
+
+getBase :
   {cont : Container} ->
   {c : Case} ->
-  Term (semCase c (W cont) ~> N ~> N * N) ctx
-getOffset {c = (tag, 0)} = Const $ Const $ App pair [<1, 0]
-getOffset {c = (tag, k@(S _))} = Abs' (\x =>
-  App Container.cons
-    [<App pair [<1, 0]
-    , 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])
-    ])
+  Term (semCase c (W cont) ~> N ~> N) ctx
+getBase {c = (tag, 0)} =
+  -- No children, so do not care
+  Arb
+getBase {c = (tag, k@(S _))} =
+  Abs' (\x =>
+    App Container.cons
+      [<1 -- Children are 1, 2, ..., k
+      , Abs'
+        (\n =>
+          -- base (1 + i + k z) => 1 + i + k (base_i z)
+          -- The initial (1 +) is a consequence of the cons.
+          let dm = App (divmod' k) [<n] in
+          let z = App fst [<dm] in
+          let i = App snd [<dm] in
+          let child = App (index . children) [<shift x, i] in
+          Suc (App forget [<i] + Op (Lit k) * App base [<child, z]))
+      ])
+
+getStride :
+  {cont : Container} ->
+  {c : Case} ->
+  Term (semCase c (W cont) ~> N ~> N) ctx
+getStride {c = (tag, 0)} =
+  -- No children, so do not care
+  Arb
+getStride {c = (tag, k@(S _))} =
+  Abs' (\x =>
+    App Container.cons
+      [<1 -- Children are 1, 2, ..., k
+      , Abs'
+        (\n =>
+          -- stride (1 + i + k z) => k (stride_i z)
+          -- The initial (1 +) is a consequence of the cons.
+          let dm = App (divmod' k) [<n] in
+          let z = App fst [<dm] in
+          let i = App snd [<dm] in
+          let child = App (index . children) [<shift x, i] in
+          Suc (Op (Lit k) * App base [<child, z]))
+          ])
 
 -- Calculates data map for a new W value.
 getVals :
@@ -119,15 +203,21 @@ getVals :
   (i : Elem c cont.constructors) ->
   Term (semCase c (W cont) ~> N ~> unitSem cont) ctx
 getVals i {c = (tag', 0)} =
+  -- Only the root matters.
   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])
+    [< -- Root is first
+      App (tag @{mapNonEmpty cont.ok} (elemMap unitCase i) . forgetCase) [<x]
+    , Abs'
+      (\n =>
+        -- vals (1 + i + k z) => vals_i (z)
+        -- The initial (1 +) is a consequence of the cons
+        let dm = App (divmod' k) [<n] in
+        let z = App fst [<dm] in
+        let i = App snd [<dm] in
+        let child = App (index . children) [<shift x, i] in
+        App vals [<child, z])
     ])
 
 -- Constructs a value for a specific constructor
@@ -136,12 +226,14 @@ introCase :
   {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
+introCase i = AbsAll [<_,_] (\[<x, n] =>
+  App pair
+  [<App pair
+  [<App pair
+  [<App getFuel [<x, n]
+  , App (getVals i) [<x, n]]
+  , App getBase [<x, n]]
+  , App getStride [<x, n]])
 
 export
 intro : {c : Container} -> Term (sem c (W c) ~> W c) ctx
@@ -150,13 +242,12 @@ intro =
   rewrite mapFusion (~> W c) (flip semCase (W c)) c.constructors in
   gtabulate introCase
 
-calcIndex : Term (N * N ~> N ~> N) ctx
-calcIndex = AbsAll [<_, _] (\[<bs, n] => App fst [<bs] + App snd [<bs] * n)
+-- Case Splitting --------------------------------------------------------------
 
 fillCase :
   {c : Case} ->
-  {ty : Ty} ->
-  Term ((Fin (snd c) ~> ty) ~> (semCase c ty ~> ty) ~> unitCase c ~> ty) ctx
+  {ty, 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
@@ -170,28 +261,38 @@ fillCase {c = (Nothing, k)} =
 
 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
+  {ty, ty' : Ty} ->
+  Term (map (\c => semCase c ty ~> ty') c.constructors ~>* W c ~> (N ~> ty) ~> (N ~> ty')) ctx
+elimStep = AbsAll (_ :< _ :< _ :< _)
+  -- fs: update action for each constructor
+  -- x : fixed point
+  -- f : initial value for each tag
+  -- n : tag to compute at
+  -- ---
+  -- returns updated value for tag
+  (\(fs :< x :< f :< n) =>
+    let val = App vals [<x, n] in
+    let base = App base [<x, n] in
+    let stride = App stride [<x, 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
+        [<f . App calcIndex [<base, stride] . forget
+        , indexAll (elemMap (\c => semCase c ty ~> ty') i) fs
         ]) :<
     val)
 
 export
+inspect :
+  {c : Container} ->
+  {ty : Ty} ->
+  Term (map (\c' => semCase c' (W c) ~> ty) c.constructors ~>* W c ~> ty) ctx
+inspect = AbsAll (_ :< _) (\(fs :< x) => App elimStep (fs :< x :< App reroot [<x] :< 0))
+
+-- Eliminator ------------------------------------------------------------------
+
+export
 elim :
   {c : Container} ->
   {ty : Ty} ->
@@ -201,5 +302,5 @@ elim = AbsAll (_ :< _)
     App
       (Rec (App fuel [<x])
         Arb
-        (App elimStep (fs :< App offset [<x] :< App vals [<x])))
+        (App elimStep (fs :< x)))
       [<Zero])
diff --git a/src/Encoded/Pair.idr b/src/Encoded/Pair.idr
index 5873e40..4b66cfe 100644
--- a/src/Encoded/Pair.idr
+++ b/src/Encoded/Pair.idr
@@ -39,6 +39,11 @@ bimap = Abs $ Abs $ Abs $ Abs $
     ]
 
 export
+mapFst : {ty1, ty1', ty2 : Ty} -> Term ((ty1 ~> ty1') ~> ty1 * ty2 ~> ty1' * ty2) ctx
+mapFst = AbsAll [<_,_] (\[<f, x] =>
+  App pair [<App (f . fst) [<x], App snd [<x]])
+
+export
 mapSnd : {ty1, ty2, ty2' : Ty} -> Term ((ty2 ~> ty2') ~> ty1 * ty2 ~> ty1 * ty2') ctx
 mapSnd = Abs $ Abs $
   let f = Var (There Here) in
diff --git a/src/Encoded/Vect.idr b/src/Encoded/Vect.idr
index 064de5f..e86abdb 100644
--- a/src/Encoded/Vect.idr
+++ b/src/Encoded/Vect.idr
@@ -1,6 +1,7 @@
 module Encoded.Vect
 
 import Data.String
+import Data.Vect
 
 import Encoded.Bool
 import Encoded.Pair
@@ -56,3 +57,13 @@ foldr {k = S k} = Abs $ Abs $ Abs $
   let c = Var (There Here) in
   let xs = Var Here in
   App c [<App xs [<zero], App foldr [<z, c, xs . suc]]
+
+export
+fromVect : {k : Nat} -> {ty : Ty} -> Vect k (Term ty ctx) -> Term (Vect k ty) ctx
+fromVect [] = nil
+fromVect (t :: ts) = App cons [<t, fromVect ts]
+
+export
+toVect : {k : Nat} -> {ty : Ty} -> Term (Vect k ty) ctx -> Vect k (Term ty ctx)
+toVect {k = 0} v = []
+toVect {k = S k} v = App v [<zero] :: toVect (v . suc)
diff --git a/src/Term.idr b/src/Term.idr
index f6fecbb..b6367a1 100644
--- a/src/Term.idr
+++ b/src/Term.idr
@@ -27,7 +27,6 @@ data Operator : List Ty -> Ty -> Type where
   Inr : (ty, ty' : Ty) -> Operator [ty'] (ty <+> ty')
   Prl : (ty, ty' : Ty) -> Operator [ty <+> ty'] ty
   Prr : (ty, ty' : Ty) -> Operator [ty <+> ty'] ty'
-  Arb : (ty : Ty) -> Operator [] ty
 
 %name Operator op
 
diff --git a/src/Term/Compile.idr b/src/Term/Compile.idr
index dd423ae..ba409a8 100644
--- a/src/Term/Compile.idr
+++ b/src/Term/Compile.idr
@@ -35,10 +35,6 @@ lambda = "lambda"
 lit : Nat -> Doc ann
 lit = pretty
 
-compileArb : Ty -> Doc ann
-compileArb N = pretty 0
-compileArb (ty ~> ty') = parens $ group $ "const" <+> softline <+> compileArb ty'
-
 compileOp : Operator tys ty -> Doc ann
 compileOp (Lit n) = lit n
 compileOp Suc = "1+"
@@ -52,7 +48,6 @@ compileOp (Inl _ _) = identity_
 compileOp (Inr _ _) = identity_
 compileOp (Prl _ _) = identity_
 compileOp (Prr _ _) = identity_
-compileOp (Arb ty) = compileArb ty
 
 parameters (names : Stream String)
   compileFullTerm : (len : Len ctx) => FullTerm ty ctx' -> ctx' `Thins` ctx -> Doc ann
diff --git a/src/Term/Pretty.idr b/src/Term/Pretty.idr
index 043d478..1b62dc3 100644
--- a/src/Term/Pretty.idr
+++ b/src/Term/Pretty.idr
@@ -156,7 +156,6 @@ prettyOp (Inl _ _) = keyword "inl"
 prettyOp (Inr _ _) = keyword "inr"
 prettyOp (Prl _ _) = keyword "prl"
 prettyOp (Prr _ _) = keyword "prr"
-prettyOp (Arb _) = keyword "arb"
 
 parameters (names : Stream String)
   prettyTerm' : (len : Len ctx) => Prec -> Term ty ctx -> Doc Syntax
diff --git a/src/Term/Semantics.idr b/src/Term/Semantics.idr
index c31a9e6..eb1c9c5 100644
--- a/src/Term/Semantics.idr
+++ b/src/Term/Semantics.idr
@@ -70,7 +70,6 @@ opSem (Inl ty1 ty2) = inl ty1 ty2
 opSem (Inr ty1 ty2) = swap ty2 ty1 . inl ty2 ty1
 opSem (Prl ty1 ty2) = prl ty1 ty2
 opSem (Prr ty1 ty2) = prl ty2 ty1 . swap ty1 ty2
-opSem (Arb ty) = arb ty
 
 %inline
 sem' : Monad m => Term ty ctx -> m (All TypeOf ctx -> TypeOf ty)
diff --git a/src/Term/Syntax.idr b/src/Term/Syntax.idr
index d403440..5a134a2 100644
--- a/src/Term/Syntax.idr
+++ b/src/Term/Syntax.idr
@@ -43,7 +43,8 @@ t `mod` u = App (App (Op Mod) t) u
 
 export
 Arb : {ty : Ty} -> Term ty ctx
-Arb = Op (Arb ty)
+Arb {ty = N} = Op (Lit 0)
+Arb {ty = ty ~> ty'} = Const Arb
 
 export
 inL : {ty1, ty2 : Ty} -> Term (ty1 ~> (ty1 <+> ty2)) ctx