1 files changed, 125 insertions, 0 deletions
diff --git a/src/Data/Term/Occurs.idr b/src/Data/Term/Occurs.idr
new file mode 100644
index 0000000..4caa089
--- /dev/null
+++ b/src/Data/Term/Occurs.idr
@@ -0,0 +1,125 @@
+module Data.Term.Occurs
+
+import Data.Fin.Occurs
+import Data.Maybe.Properties
+import Data.Term
+import Data.Term.Zipper
+
+import Syntax.PreorderReasoning
+
+-- Check -----------------------------------------------------------------------
+
+export
+check : Fin k -> Term sig k -> Maybe (Term sig (pred k))
+checkAll : Fin k -> Vect n (Term sig k) -> Maybe (Vect n (Term sig (pred k)))
+
+check x (Var y) = Var <$> thick x y
+check x (Op op ts) = Op op <$> checkAll x ts
+
+checkAll x [] = Just []
+checkAll x (t :: ts) = [| check x t :: checkAll x ts |]
+
+-- Properties
+
+export
+checkOccurs : (x : Fin k) -> (zip : Zipper sig k) -> IsNothing (check x (zip + Var x))
+checkAllOccurs :
+  (x : Fin k) ->
+  (i : Fin (S n)) ->
+  (ts : Vect n (Term sig k)) ->
+  (zip : Zipper sig k) ->
+  IsNothing (checkAll x (insertAt i (zip + Var x) ts))
+
+checkOccurs x Top = mapNothing Var (thickRefl x)
+checkOccurs x (Op op i ts zip) = mapNothing (Op op) (checkAllOccurs x i ts zip)
+
+checkAllOccurs x FZ ts zip =
+  appLeftNothingIsNothing
+    (appRightNothingIsNothing (Just (::)) (checkOccurs x zip))
+    (checkAll x ts)
+checkAllOccurs x (FS i) (t :: ts) zip =
+  appRightNothingIsNothing
+    (Just (::) <*> check x t)
+    (checkAllOccurs x i ts zip)
+
+export
+checkNothing :
+  (x : Fin k) ->
+  (t : Term sig k) ->
+  (0 _ : IsNothing (check x t)) ->
+  (zip : Zipper sig k ** t = zip + Var x)
+checkAllNothing :
+  (x : Fin k) ->
+  (t : Term sig k) ->
+  (ts : Vect n (Term sig k)) ->
+  (0 _ : IsNothing (checkAll x (t :: ts))) ->
+  (i ** ts' ** zip : Zipper sig k ** t :: ts = insertAt i (zip + Var x) ts')
+
+checkNothing x (Var y) prf =
+  (Top ** sym (cong Var (thickNothing x y (mapNothingInverse Var (thick x y) prf))))
+checkNothing x (Op op (t :: ts)) prf =
+  let (i ** ts' ** zip ** prf) = checkAllNothing x t ts (mapNothingInverse (Op op) _ prf) in
+  (Op op i ts' zip ** cong (Op op) prf)
+
+checkAllNothing x t ts prf with (appNothingInverse (Just (::) <*> check x t) (checkAll x ts) prf)
+  _ | Left prf' = case appNothingInverse (Just (::)) (check x t) prf' of
+      Right prf =>
+        let (zip ** prf) = checkNothing x t prf in
+        (FZ ** ts ** zip ** cong (:: ts) prf)
+  checkAllNothing x t (t' :: ts) prf | Right prf' =
+    let (i ** ts ** zip ** prf) = checkAllNothing x t' ts prf' in
+    (FS i ** t :: ts ** zip ** cong (t ::) prf)
+
+export
+checkThin : (x : Fin k) -> (t : Term sig (pred k)) -> IsJust (check x (pure (thin x) <$> t))
+checkAllThin :
+  (x : Fin k) ->
+  (ts : Vect n (Term sig (pred k))) ->
+  IsJust (checkAll x (map (pure (thin x) <$>) ts))
+
+checkThin x (Var y) = mapIsJust Var (thickNeq x (thin x y) (\prf => thinSkips x y $ sym prf))
+checkThin x (Op op ts) = mapIsJust (Op op) (checkAllThin x ts)
+
+checkAllThin x [] = ItIsJust
+checkAllThin x (t :: ts) =
+  appIsJust
+    (appIsJust ItIsJust (checkThin x t))
+    (checkAllThin x ts)
+
+export
+checkJust :
+  (x : Fin k) ->
+  (t : Term sig k) ->
+  (0 _ : check x t = Just u) ->
+  t = pure (thin x) <$> u
+checkAllJust :
+  (x : Fin k) ->
+  (ts : Vect n (Term sig k)) ->
+  (0 _ : checkAll x ts = Just us) ->
+  ts = map (pure (thin x) <$>) us
+
+checkJust x (Var y) prf =
+  let 0 z = mapJustInverse Var (thick x y) prf in
+  let 0 prf = thickJust x y (fst z.snd) in
+  sym $ Calc $
+    |~ pure (thin x) <$> u
+    ~~ pure (thin x) <$> Var z.fst ...(cong (pure (thin x) <$>) $ snd z.snd)
+    ~~ Var y                       ...(cong Var prf)
+checkJust x (Op op ts) prf =
+  let 0 z = mapJustInverse (Op op) (checkAll x ts) prf in
+  let 0 prf = checkAllJust x ts (fst z.snd) in
+  Calc $
+    |~ Op op ts
+    ~~ pure (thin x) <$> Op op z.fst ...(cong (Op op) prf)
+    ~~ pure (thin x) <$> u           ...(sym $ cong (pure (thin x) <$>) $ snd z.snd)
+
+checkAllJust x [] Refl = Refl
+checkAllJust x (t :: ts) prf =
+  let 0 z = appJustInverse (Just (::) <*> check x t) (checkAll x ts) prf in
+  let 0 w = appJustInverse (Just (::)) (check x t) (fst z.snd.snd) in
+  Calc $
+    |~ t :: ts
+    ~~ map (pure (thin x) <$>) (w.snd.fst :: z.snd.fst)    ...(cong2 (::) (checkJust x t (fst $ snd w.snd.snd)) (checkAllJust x ts (fst $ snd z.snd.snd)))
+    ~~ map (pure (thin x) <$>) (w.fst w.snd.fst z.snd.fst) ...(cong (\f => map (pure (thin x) <$>) (f w.snd.fst z.snd.fst)) $ injective $ fst w.snd.snd)
+    ~~ map (pure (thin x) <$>) (z.fst z.snd.fst)           ...(sym $ cong (\f => map (pure (thin x) <$>) (f z.snd.fst)) $ snd $ snd w.snd.snd)
+    ~~ map (pure (thin x) <$>) us                          ...(sym $ cong (map (pure (thin x) <$>)) $ snd $ snd z.snd.snd)