Add occurs check for terms.

5 files changed, 234 insertions, 33 deletions

diff --git a/src/Data/Fin/Occurs.idr b/src/Data/Fin/Occurs.idr
index 899e2a1..58c8faa 100644
--- a/src/Data/Fin/Occurs.idr
+++ b/src/Data/Fin/Occurs.idr
@@ -45,23 +45,24 @@ export
 thinSkips : (x : Fin n) -> (y : Fin (pred n)) -> Not (thin x y = x)
 thinSkips (FS x) (FS y) prf = thinSkips x y (injective prf)
 
+%inline
 thinSucZero : (x : Fin n) -> thin (FS x) (zero x) = FZ
-thinSucZero FZ = Refl
-thinSucZero (FS x) = Refl
+thinSucZero x = rewrite snd (indexIsSuc x) in Refl
 
+%inline
 thinSucSuc : (x : Fin n) -> (z : Fin (pred n)) -> thin (FS x) (suc z) = FS (thin x z)
 thinSucSuc FZ FZ = Refl
-thinSucSuc FZ (FS x) = Refl
+thinSucSuc FZ (FS z) = Refl
 thinSucSuc (FS x) FZ = Refl
-thinSucSuc (FS x) (FS y) = Refl
+thinSucSuc (FS x) (FS z) = Refl
 
 export
-thinInverse : (x, y : Fin n) -> Not (x = y) -> (z ** thin x z = y)
+thinInverse : (x, y : Fin n) -> (0 _ : Not (x = y)) -> (z ** thin x z = y)
 thinInverse FZ FZ neq = void (neq Refl)
 thinInverse FZ (FS y) neq = (y ** Refl)
 thinInverse (FS x) FZ neq = (zero x ** thinSucZero x)
 thinInverse (FS x) (FS y) neq =
-  let (z ** prf) = thinInverse x y (\eq => neq $ cong FS eq) in
+  let (z ** prf) = thinInverse x y (neq . cong FS) in
   (suc z ** trans (thinSucSuc x z) (cong FS prf))
 
 -- Thickening ------------------------------------------------------------------
@@ -71,31 +72,32 @@ thick : Fin n -> Fin n -> Maybe (Fin (pred n))
 thick FZ FZ = Nothing
 thick FZ (FS y) = Just y
 thick (FS x) FZ = Just (zero x)
-thick (FS x) (FS y) = [| suc (thick x y) |]
+thick (FS x) (FS y) = suc <$> thick x y
 
 export
-thickIsNothing : (x, y : Fin n) -> (x = y) <=> (thick x y = Nothing)
-thickIsNothing FZ FZ = MkEquivalence (const Refl) (const Refl)
-thickIsNothing FZ (FS y) = MkEquivalence absurd absurd
-thickIsNothing (FS x) FZ = MkEquivalence absurd absurd
-thickIsNothing (FS x) (FS y) =
-  let rec = thickIsNothing x y in
-  MkEquivalence
-    (cong (Just suc <*>) . rec.leftToRight . injective)
-    (cong FS . rec.rightToLeft . appNothingRight suc (thick x y))
+thickRefl : (x : Fin n) -> IsNothing (thick x x)
+thickRefl FZ = ItIsNothing
+thickRefl (FS x) = mapNothing suc (thickRefl x)
 
 export
-thickIsJust : (x, y : Fin n) -> Not (x = y) <=> (z ** (thick x y = Just z, thin x z = y))
-thickIsJust FZ FZ = MkEquivalence (\f => absurd $ f Refl) (\p => absurd $ fst $ snd p)
-thickIsJust FZ (FS y) = MkEquivalence (const (y ** (Refl, Refl))) (const absurd)
-thickIsJust (FS x) FZ =
-  MkEquivalence
-    (const (zero x ** (Refl, thinSucZero x)))
-    (const absurd)
-thickIsJust (FS x) (FS y) =
-  let rec = thickIsJust x y in
-  MkEquivalence
-    (\neq =>
-      let (z ** (prf1, prf2)) = rec.leftToRight (neq . cong FS) in
-      (suc z ** (rewrite prf1 in Refl, trans (thinSucSuc x z) (cong FS prf2))))
-    (\(z ** (prf1, prf2)), prf => thinSkips (FS x) z $ trans prf2 (sym prf))
+thickNeq : (x, y : Fin n) -> (0 _ : Not (x = y)) -> IsJust (thick x y)
+thickNeq FZ FZ neq = void (neq Refl)
+thickNeq FZ (FS y) neq = ItIsJust
+thickNeq (FS x) FZ neq = ItIsJust
+thickNeq (FS x) (FS y) neq = mapIsJust suc (thickNeq x y (neq . cong FS))
+
+export
+thickNothing : (x, y : Fin n) -> (0 _ : IsNothing (thick x y)) -> x = y
+thickNothing FZ FZ prf = Refl
+thickNothing (FS x) (FS y) prf =
+  rewrite thickNothing x y (mapNothingInverse suc (thick x y) prf) in
+  Refl
+
+export
+thickJust : (x, y : Fin n) -> (0 _ : thick x y = Just z) -> thin x z = y
+thickJust FZ (FS y) Refl = Refl
+thickJust (FS x) FZ Refl = thinSucZero x
+thickJust (FS x) (FS y) prf =
+  let 0 z = mapJustInverse suc (thick x y) prf in
+  rewrite snd $ z.snd in
+  trans (thinSucSuc x z.fst) (cong FS $ thickJust x y (fst $ z.snd))
diff --git a/src/Data/Maybe/Properties.idr b/src/Data/Maybe/Properties.idr
index 495256e..99a3507 100644
--- a/src/Data/Maybe/Properties.idr
+++ b/src/Data/Maybe/Properties.idr
@@ -1,10 +1,82 @@
 module Data.Maybe.Properties
 
+import Control.Function
+import Data.Maybe
+
+public export
+data IsNothing : Maybe a -> Type where
+  ItIsNothing : IsNothing Nothing
+
+%inline
 export
 mapFusion : (s : Maybe a) -> (f . g) <$> s = f <$> [| g s |]
 mapFusion Nothing = Refl
 mapFusion (Just x) = Refl
 
+%inline
+export
+extractIsJust : {x : Maybe a} -> (0 _ : IsJust x) -> (y ** x = Just y)
+extractIsJust ItIsJust = (_ ** Refl)
+
+%inline
+export
+mapIsJust : (0 f : a -> b) -> IsJust x -> IsJust (map f x)
+mapIsJust f ItIsJust = ItIsJust
+
+%inline
+export
+mapJustInverse :
+  (0 f : a -> b) ->
+  (x : Maybe a) ->
+  (0 _ : map f x = Just y) ->
+  (z ** (x = Just z, y = f z))
+mapJustInverse f (Just x) prf = (x ** (Refl, sym $ injective prf))
+
+%inline
+export
+mapNothing : (0 f : a -> b) -> IsNothing x -> IsNothing (map f x)
+mapNothing f ItIsNothing = ItIsNothing
+
+%inline
+export
+mapNothingInverse :
+  (0 f : a -> b) ->
+  (x : Maybe a) ->
+  (0 _ : IsNothing (map f x)) ->
+  IsNothing x
+mapNothingInverse f Nothing prf = ItIsNothing
+
+%inline
+export
+appIsJust : IsJust f -> IsJust x -> IsJust (f <*> x)
+appIsJust ItIsJust ItIsJust = ItIsJust
+
+%inline
+export
+appJustInverse :
+  (f : Maybe (a -> b)) ->
+  (x : Maybe a) ->
+  (0 _ : f <*> x = Just y) ->
+  (f' ** x' ** (f = Just f', x = Just x', y = f' x'))
+appJustInverse (Just f) (Just x) prf = (f ** x ** (Refl, Refl, sym $ injective prf))
+
+%inline
+export
+appLeftNothingIsNothing : IsNothing f -> (0 x : Maybe a) -> IsNothing (f <*> x)
+appLeftNothingIsNothing ItIsNothing x = ItIsNothing
+
+%inline
+export
+appRightNothingIsNothing : (f : Maybe (a -> b)) -> IsNothing x -> IsNothing (f <*> x)
+appRightNothingIsNothing Nothing prf = ItIsNothing
+appRightNothingIsNothing (Just f) ItIsNothing = ItIsNothing
+
+%inline
 export
-appNothingRight : (0 f : a -> b) -> (y : Maybe a) -> Just f <*> y = Nothing -> y = Nothing
-appNothingRight f Nothing prf = Refl
+appNothingInverse :
+  (f : Maybe (a -> b)) ->
+  (x : Maybe a) ->
+  (0 _ : IsNothing (f <*> x)) ->
+  Either (IsNothing f) (IsNothing x)
+appNothingInverse Nothing x prf = Left ItIsNothing
+appNothingInverse (Just f) Nothing prf = Right ItIsNothing
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)
diff --git a/src/Data/Term/Zipper.idr b/src/Data/Term/Zipper.idr
index 09ba2c9..3f6668a 100644
--- a/src/Data/Term/Zipper.idr
+++ b/src/Data/Term/Zipper.idr
@@ -41,7 +41,8 @@ assoc (Op op i ts zip1) zip2 zip3 = cong (Op op i ts) (assoc zip1 zip2 zip3)
 
 -- Action ----------------------------------------------------------------------
 
-export
+-- NOTE: should this be public?
+public export
 (+) : Zipper sig n -> Term sig n -> Term sig n
 Top + t = t
 Op op i ts zip + t = Op op (insertAt i (zip + t) ts)
diff --git a/unify.ipkg b/unify.ipkg
index 44ee037..0a8616a 100644
--- a/unify.ipkg
+++ b/unify.ipkg
@@ -10,6 +10,7 @@ modules
   = Data.Fin.Occurs
   , Data.Maybe.Properties
   , Data.Term
+  , Data.Term.Occurs
   , Data.Term.Property
   , Data.Term.Zipper
   , Data.Vect.Properties.Insert