Describe unification.

1 files changed, 0 insertions, 125 deletions

diff --git a/src/Data/Term/Occurs.idr b/src/Data/Term/Occurs.idr
deleted file mode 100644
index 4caa089..0000000
--- a/src/Data/Term/Occurs.idr
+++ /dev/null
@@ -1,125 +0,0 @@
-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)