Describe unification.

4 files changed, 142 insertions, 2 deletions

diff --git a/src/Data/Fin/Occurs.idr b/src/Data/Fin/Occurs.idr
index 58c8faa..d70c8f3 100644
--- a/src/Data/Fin/Occurs.idr
+++ b/src/Data/Fin/Occurs.idr
@@ -101,3 +101,14 @@ 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))
+
+export
+thickThin : (x : Fin n) -> (y : Fin (pred n)) -> thick x (thin x y) = Just y
+thickThin x y =
+  let neq = thinSkips x y in
+  let isJust = thickNeq x (thin x y) (\prf => neq $ sym prf) in
+  let zPrf = extractIsJust isJust in
+  let z = zPrf.fst in
+  let 0 prf1 = zPrf.snd in
+  let 0 prf2 = thickJust x (thin x y) prf1 in
+  trans prf1 (cong Just $ thinInjective x prf2)
diff --git a/src/Data/Maybe/Properties.idr b/src/Data/Maybe/Properties.idr
index 99a3507..459cb8f 100644
--- a/src/Data/Maybe/Properties.idr
+++ b/src/Data/Maybe/Properties.idr
@@ -20,6 +20,11 @@ extractIsJust ItIsJust = (_ ** Refl)
 
 %inline
 export
+extractIsNothing : {x : Maybe a} -> (0 _ : IsNothing x) -> x = Nothing
+extractIsNothing ItIsNothing = Refl
+
+%inline
+export
 mapIsJust : (0 f : a -> b) -> IsJust x -> IsJust (map f x)
 mapIsJust f ItIsJust = ItIsJust
 
diff --git a/src/Data/Term/Occurs.idr b/src/Data/Term/Unify.idr
index 4caa089..2955aa2 100644
--- a/src/Data/Term/Occurs.idr
+++ b/src/Data/Term/Unify.idr
@@ -1,10 +1,13 @@
-module Data.Term.Occurs
+module Data.Term.Unify
 
+import Data.DPair
 import Data.Fin.Occurs
 import Data.Maybe.Properties
 import Data.Term
 import Data.Term.Zipper
 
+import Decidable.Equality
+
 import Syntax.PreorderReasoning
 
 -- Check -----------------------------------------------------------------------
@@ -123,3 +126,124 @@ checkAllJust x (t :: ts) prf =
     ~~ 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)
+
+-- Single Variable Substitution ------------------------------------------------
+
+export
+for : Term sig (pred k) -> Fin k -> Fin k -> Term sig (pred k)
+(t `for` x) y = maybe t Var (thick x y)
+
+export
+forThin : (0 t : Term sig (pred k)) -> (x : Fin k) -> (t `for` x) . thin x .=. Var
+forThin t x i = cong (maybe t Var) (thickThin x i)
+
+export
+forUnifies :
+  (x : Fin k) ->
+  (t : Term sig k) ->
+  (0 _ : check x t = Just u) ->
+  (u `for` x) <$> t = (u `for` x) <$> Var x
+forUnifies x t prf = Calc $
+  |~ (u `for` x) <$> t
+  ~~ (u `for` x) <$> pure (thin x) <$> u ...(cong ((u `for` x) <$>) $ checkJust x t prf)
+  ~~ (u `for` x) . thin x <$> u          ...(sym $ subAssoc (u `for` x) (pure (thin x)) u)
+  ~~ Var <$> u                           ...(subCong (forThin u x) u)
+  ~~ u                                   ...(subUnit u)
+  ~~ (u `for` x) <$> Var x               ...(sym $ cong (maybe u Var) $ extractIsNothing $ thickRefl x)
+
+-- Substitution List -----------------------------------------------------------
+
+public export
+data AList : Signature -> Nat -> Nat -> Type where
+  Lin : AList sig n n
+  (:<) : AList sig k n -> (Term sig k, Fin (S k)) -> AList sig (S k) n
+
+%name AList sub
+
+namespace Exists
+  public export
+  (:<) : Exists (AList sig n) -> (Term sig n, Fin (S n)) -> Exists (AList sig (S n))
+  Evidence _ sub :< tx = Evidence _ (sub :< tx)
+
+export
+eval : AList sig k n -> Fin k -> Term sig n
+eval [<] = Var
+eval (sub :< (t, x)) = eval sub . (t `for` x)
+
+export
+(++) : AList sig k n -> AList sig j k -> AList sig j n
+sub ++ [<] = sub
+sub ++ sub1 :< tx = (sub ++ sub1) :< tx
+
+-- Properties
+
+export
+evalHomo :
+  (0 sub2 : AList sig k n) ->
+  (sub1 : AList sig j k) ->
+  eval (sub2 ++ sub1) .=. eval sub2 . eval sub1
+evalHomo sub2 [<] i = Refl
+evalHomo sub2 (sub1 :< (t, x)) i = Calc $
+  |~ eval (sub2 ++ sub1) <$> (t `for` x) i
+  ~~ (eval sub2 . eval sub1) <$> (t `for` x) i ...(subCong (evalHomo sub2 sub1) ((t `for` x) i))
+  ~~ eval sub2 <$> eval sub1 <$> (t `for` x) i ...(subAssoc (eval sub2) (eval sub1) ((t `for` x) i))
+
+-- Unification -----------------------------------------------------------------
+
+flexFlex : (x, y : Fin n) -> Exists (AList sig n)
+flexFlex x y =
+  rewrite (snd $ indexIsSuc x) in
+  case thick x' y' of
+    Just z => Evidence _ [<(Var z, x')]
+    Nothing => Evidence _ [<]
+  where
+  x', y' : Fin (S $ fst $ indexIsSuc x)
+  x' = replace {p = Fin} (snd $ indexIsSuc x) x
+  y' = replace {p = Fin} (snd $ indexIsSuc x) y
+
+flexRigid : Fin n -> Term sig n -> Maybe (Exists (AList sig n))
+flexRigid x t =
+  rewrite (snd $ indexIsSuc x) in
+  case check x' t' of
+    Just u => Just (Evidence _ [<(u, x')])
+    Nothing => Nothing
+  where
+  x' : Fin (S $ fst $ indexIsSuc x)
+  x' = replace {p = Fin} (snd $ indexIsSuc x) x
+  t' : Term sig (S $ fst $ indexIsSuc x)
+  t' = replace {p = Term sig} (snd $ indexIsSuc x) t
+
+export
+amgu :
+  DecEq (Exists sig.Operator) =>
+  (t, u : Term sig n) ->
+  Exists (AList sig n) ->
+  Maybe (Exists (AList sig n))
+amguAll :
+  DecEq (Exists sig.Operator) =>
+  (ts, us : Vect k (Term sig n)) ->
+  Exists (AList sig n) ->
+  Maybe (Exists (AList sig n))
+
+amgu (Op op ts) (Op op' us) acc =
+  case decEq {t = Exists sig.Operator} (Evidence _ op) (Evidence _ op') of
+    Yes prf => amguAll ts (replace {p = \k => Vect k (Term sig n)} (sym $ cong fst prf) us) acc
+    No neq => Nothing
+amgu (Var x) (Var y) (Evidence _ [<]) = Just (flexFlex x y)
+amgu (Var x) (Op op' us) (Evidence _ [<]) = flexRigid x (Op op' us)
+amgu (Op op ts) (Var y) (Evidence _ [<]) = flexRigid y (Op op ts)
+amgu t@(Var _) u@(Var _) (Evidence _ (sub :< (v, z))) =
+  (:< (v, z)) <$> amgu ((v `for` z) <$> t) ((v `for` z) <$> u) (Evidence _ sub)
+amgu t@(Var _) u@(Op _ _) (Evidence _ (sub :< (v, z))) =
+  (:< (v, z)) <$> amgu ((v `for` z) <$> t) ((v `for` z) <$> u) (Evidence _ sub)
+amgu t@(Op _ _) u@(Var _) (Evidence _ (sub :< (v, z))) =
+  (:< (v, z)) <$> amgu ((v `for` z) <$> t) ((v `for` z) <$> u) (Evidence _ sub)
+
+amguAll [] [] acc = Just acc
+amguAll (t :: ts) (u :: us) acc = do
+  acc <- amgu t u acc
+  amguAll ts us acc
+
+export
+mgu : DecEq (Exists sig.Operator) => (t, u : Term sig n) -> Maybe (Exists (AList sig n))
+mgu t u = amgu t u (Evidence _ [<])
diff --git a/unify.ipkg b/unify.ipkg
index 0a8616a..5350848 100644
--- a/unify.ipkg
+++ b/unify.ipkg
@@ -10,8 +10,8 @@ modules
   = Data.Fin.Occurs
   , Data.Maybe.Properties
   , Data.Term
-  , Data.Term.Occurs
   , Data.Term.Property
+  , Data.Term.Unify
   , Data.Term.Zipper
   , Data.Vect.Properties.Insert
   , Data.Vect.Quantifiers.Extra