Add Container types.

1 files changed, 130 insertions, 2 deletions

diff --git a/src/Obs/NormalForm/Normalise.idr b/src/Obs/NormalForm/Normalise.idr
index 919067e..b50b520 100644
--- a/src/Obs/NormalForm/Normalise.idr
+++ b/src/Obs/NormalForm/Normalise.idr
@@ -7,7 +7,7 @@ import Obs.NormalForm
 import Obs.Sort
 import Obs.Substitution
 
--- Substitution ----------------------------------------------------------------
+-- Utilities -------------------------------------------------------------------
 
 mergeName : String -> String -> String
 mergeName "" s' = s'
@@ -22,6 +22,38 @@ wkn (var :: vars) f =
     (pure $ Ntrl $ Var var FZ)
     (\i => pure $ rename !(wkn vars f i) FS)
 
+export
+expandContainerTy : Sort -> NormalForm n -> Sort -> Sort -> Constructor n
+expandContainerTy s a s' s'' =
+  let tagTy : Constructor n
+      tagTy = Pi s (suc s') "i" a (cast s')
+  in
+  let posTy : Constructor (S n)
+      posTy =
+        Pi s (s' ~> suc s'') "i"
+          (weaken 1 a)
+          (Cnstr $ Pi s' (suc s'') "t"
+            (Ntrl $ App (Var "tag" 1) (Ntrl $ Var "i" 0))
+            (cast s''))
+  in
+  let nextTy : Constructor (2 + n)
+      nextTy =
+        Pi s (s' ~> suc s'' ~> s) "i"
+          (weaken 2 a)
+          (Cnstr $ Pi s' (suc s'' ~> s) "t"
+            (Ntrl $ App (Var "tag" 2) (Ntrl $ Var "i" 0))
+            (Cnstr $ Pi (suc s'') s "p"
+              (Ntrl $ App (App (Var "pos" 2) (Ntrl $ Var "i" 1)) (Ntrl $ Var "p" 0))
+              (weaken 5 a)))
+  in
+  Sigma (s ~> suc s') (lub (s ~> s' ~> suc s'') (s ~> s' ~> s'' ~> s)) "tag"
+    (Cnstr tagTy) $
+  Cnstr $ Sigma (s ~> s' ~> suc s'') (s ~> s' ~> s'' ~> s) "pos"
+    (Cnstr posTy)
+    (Cnstr nextTy)
+
+-- Substitution ----------------------------------------------------------------
+
 partial
 substCnstr : Constructor n -> (Fin n -> Logging ann (NormalForm m)) -> Logging ann (Constructor m)
 partial
@@ -39,6 +71,12 @@ doSnd      : NormalForm n -> Logging ann (NormalForm n)
 partial export
 doCase     : NormalForm n -> NormalForm n -> NormalForm n -> Logging ann (NormalForm n)
 partial export
+doTag      : NormalForm n -> Logging ann (NormalForm n)
+partial export
+doPosition : NormalForm n -> Logging ann (NormalForm n)
+partial export
+doNext     : NormalForm n -> Logging ann (NormalForm n)
+partial export
 doEqual    : NormalForm n -> NormalForm n -> NormalForm n -> Logging ann (NormalForm n)
 partial
 doEqualL   : Nat -> NormalForm n -> NormalForm n -> Logging ann (NormalForm n)
@@ -52,6 +90,10 @@ partial
 doCastR    : Constructor n -> NormalForm n -> NormalForm n -> Logging ann (NormalForm n)
 partial
 doCastU    : Constructor n -> Constructor n -> NormalForm n -> Logging ann (NormalForm n)
+partial export
+expandContainer : NormalForm n -> Logging ann (Constructor n)
+partial export
+contractContainer : NormalForm n -> Logging ann (Constructor n)
 
 substCnstr (Sort s) f = pure $ Sort s
 substCnstr (Pi s s' var a b) f = do
@@ -79,6 +121,14 @@ substCnstr (Left t) f = do
 substCnstr (Right t) f = do
   t <- subst t f
   pure (Right t)
+substCnstr (Container s a s' s'') f = do
+  a <- subst a f
+  pure (Container s a s' s'')
+substCnstr (MkContainer t p u) f = do
+  t <- subst t f
+  p <- subst p f
+  u <- subst u f
+  pure (MkContainer t p u)
 substCnstr Top f = pure $ Top
 substCnstr Bottom  f = pure $ Bottom
 
@@ -101,6 +151,15 @@ substNtrl (Case t u t') f = do
   u <- subst u f
   t' <- subst t' f
   doCase t u t'
+substNtrl (Tag t) f = do
+  t <- substNtrl t f
+  doTag t
+substNtrl (Position t) f = do
+  t <- substNtrl t f
+  doPosition t
+substNtrl (Next t) f = do
+  t <- substNtrl t f
+  doNext t
 substNtrl Absurd f = pure $ Ntrl Absurd
 substNtrl (Equal a t u) f = do
   a <- substNtrl a f
@@ -162,6 +221,21 @@ doCase (Cnstr (Left t)) f g = doApp f t
 doCase (Cnstr (Right t)) f g = doApp g t
 doCase (Cnstr t) f g = inScope "bug" $ inScope "wrong constructor in case" $ fatal t
 
+doTag (Ntrl t) = pure $ Ntrl (Tag t)
+doTag Irrel = pure $ Irrel
+doTag (Cnstr (MkContainer t p f)) = pure t
+doTag (Cnstr t) = inScope "bug" $ inScope "wrong constructor in tag" $ fatal t
+
+doPosition (Ntrl t) = pure $ Ntrl (Position t)
+doPosition Irrel = pure $ Irrel
+doPosition (Cnstr (MkContainer t p f)) = pure p
+doPosition (Cnstr t) = inScope "bug" $ inScope "wrong constructor in position" $ fatal t
+
+doNext (Ntrl t) = pure $ Ntrl (Next t)
+doNext Irrel = pure $ Irrel
+doNext (Cnstr (MkContainer t p f)) = pure f
+doNext (Cnstr t) = inScope "bug" $ inScope "wrong constructor in next" $ fatal t
+
 doEqual (Ntrl a) t u = pure $ Ntrl (Equal a t u)
 doEqual Irrel t u = inScope "bug" $ inScope "wrong type over equal" $ fatal "Irrel"
 doEqual (Cnstr (Sort Prop)) t u =
@@ -201,8 +275,14 @@ doEqual (Cnstr (Sum s s' a b)) t u = do
   fBody <- doCase (weaken 1 u) (Cnstr (Lambda "y" ll)) (Cnstr (Lambda "y" lr))
   gBody <- doCase (weaken 1 u) (Cnstr (Lambda "y" rl)) (Cnstr (Lambda "y" rr))
   doCase t (Cnstr (Lambda "x" fBody)) (Cnstr (Lambda "x" gBody))
+doEqual (Cnstr (Container s a s' s'')) t u = do
+  let containerTy = expandContainerTy s a s' s''
+  t <- expandContainer t
+  u <- expandContainer u
+  doEqual (Cnstr containerTy) (Cnstr t) (Cnstr u)
 doEqual (Cnstr Top) t u = pure $ Cnstr Top
 doEqual (Cnstr Bottom) t u = pure $ Cnstr Top
+doEqual (Cnstr a) t u = inScope "bug" $ inScope "wrong type under equal" $ fatal a
 
 doEqualL i (Ntrl t) u = pure $ Ntrl (EqualL i t u)
 doEqualL i Irrel u = inScope "bug" $ inScope "wrong type under equalL" $ fatal "Irrel"
@@ -229,12 +309,15 @@ doEqualU i (Sigma s s' _ a b) (Sigma l l' var a' b') = case (s == s' && l == l')
     b <- subst b (add (Logging ann . NormalForm) (doCastL (weaken 1 a') (weaken 1 a) x) (pure . Ntrl . Var "" . FS))
     eqRhs <- doEqual (cast s') b b'
     pure $ Cnstr (Sigma Prop Prop "" eqLhs $ weaken 1 $ Cnstr (Pi s Prop var a' eqRhs))
-doEqualU i (Sum s s' a b) (Sum l l' a' b') = case (s == s' && l == l') of
+doEqualU i (Sum s s' a b) (Sum l l' a' b') = case (s == l && s' == l') of
   False => pure $ Cnstr Bottom
   True => do
     eqLhs <- doEqual (cast s) a a'
     eqRhs <- doEqual (cast s) b b'
     pure $ Cnstr (Sigma Prop Prop "" eqLhs (weaken 1 eqRhs))
+doEqualU i (Container s a s' s'') (Container l a' l' l'') = case (s == l && s' == l' && s'' == l'') of
+  False => pure $ Cnstr Bottom
+  True => doEqual (cast s) a a'
 doEqualU i t u = pure $ Ntrl (EqualU i t u) -- assumption: only logical values reach this far
 
 doCastL (Ntrl a) b t = pure $ Ntrl (CastL a b t)
@@ -267,6 +350,51 @@ doCastU (Sum s s' a b) (Sum l l' a' b') t = do
   castL <- doCastL (weaken 1 a) (weaken 1 a') x
   castR <- doCastL (weaken 1 b) (weaken 1 b') x
   doCase t (Cnstr (Lambda "x" (Cnstr (Left castL)))) (Cnstr (Lambda "x" (Cnstr (Right castR))))
+doCastU (Container s a s' s'') (Container l b l' l'') t = do
+  t <- expandContainer t
+  let a = expandContainerTy s a s' s''
+  let b = expandContainerTy l b l' l''
+  t <- doCastU a b (Cnstr t)
+  t <- contractContainer t
+  pure $ Cnstr t
 doCastU Top Top t = pure Irrel
 doCastU Bottom Bottom t = pure Irrel
 doCastU a b t = pure $ Ntrl (CastU a b t)
+
+expandContainer t = do
+  tag <- doTag t
+  pos <- doPosition t
+  next <- doNext t
+  pure $ Pair tag (Cnstr $ Pair pos next)
+
+contractContainer t = do
+  tag <- doFst t
+  t <- doSnd t
+  pos <- doFst t
+  next <- doSnd t
+  pure $ MkContainer tag pos next
+
+-- More utilities --------------------------------------------------------------
+
+export
+tagTy : Sort -> NormalForm n -> Sort -> Constructor n
+tagTy s a s' = Pi s (suc s') "i" a (cast s')
+
+export
+positionTy : Sort -> NormalForm n -> Sort -> NormalForm n -> Sort -> Logging ann (Constructor n)
+positionTy s a s' tag s'' = do
+  let i = Var "i" 0
+  tagI <- doApp (weaken 1 tag) (Ntrl i)
+  pure $ Pi s (s' ~> suc s'') "i" a (Cnstr $ Pi s' (suc s'') "t" tagI (cast s''))
+
+export
+nextTy : Sort -> NormalForm n -> Sort -> NormalForm n -> Sort -> NormalForm n -> Logging ann (Constructor n)
+nextTy s a s' tag s'' pos = do
+  let i = Var "i" 0
+  tagI <- doApp (weaken 1 tag) (Ntrl i)
+  let t = Var "t" 0
+  posI <- doApp (weaken 1 pos) (Ntrl i)
+  posIT <- doApp (weaken 1 posI) (Ntrl t)
+  pure $ Pi s (s' ~> s'' ~> s) "i" a $
+  Cnstr $ Pi s' (s'' ~> s) "t" tagI $
+  Cnstr $ Pi s'' s "p" posIT (weaken 3 a)