Fix invalid statementHEADmaster

1 files changed, 49 insertions, 35 deletions

diff --git a/src/Data/Term/Unify.idr b/src/Data/Term/Unify.idr
index 9f806fa..113514a 100644
--- a/src/Data/Term/Unify.idr
+++ b/src/Data/Term/Unify.idr
@@ -148,8 +148,8 @@ data AList : Signature -> Nat -> Nat -> Type where
 
 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)
+  (:<) : (k ** AList sig n k) -> (Term sig n, Fin (S n)) -> (k ** AList sig (S n) k)
+  (_ ** sub) :< tx = (_ ** sub :< tx)
 
 export
 eval : {k : Nat} -> AList sig k n -> Fin k -> Term sig n
@@ -198,29 +198,29 @@ flexFlex {n = S n} x y = case thick x y of
   Just z => (_ **[<(Var z, x)])
   Nothing => (_ ** [<])
 
-flexRigid : {n : Nat} -> Fin n -> Term sig n -> Maybe (Exists (AList sig n))
+flexRigid : {n : Nat} -> Fin n -> Term sig n -> Maybe (k ** AList sig n k)
 flexRigid {n = S n} x t = case check x t of
-  Just u => Just (Evidence _ [<(u, x)])
+  Just u => Just (_ ** [<(u, x)])
   Nothing => Nothing
 
 export
 amgu :
   DecOp sig =>
-  {n : Nat} ->
+  {k, n : Nat} ->
   (t, u : Term sig n) ->
   AList sig n k ->
-  Maybe (Exists (AList sig n))
+  Maybe (k ** AList sig n k)
 amguAll :
   DecOp sig =>
-  {n : Nat} ->
+  {k, n : Nat} ->
   (ts, us : Vect j (Term sig n)) ->
   AList sig n k ->
-  Maybe (Exists (AList sig n))
+  Maybe (k ** AList sig n k)
 
 amgu (Op op ts) (Op op' us) acc with (decOp (Evidence _ op) (Evidence _ op'))
   amgu (Op op ts) (Op op us) acc | Yes Refl = amguAll ts us acc
   _ | No neq = Nothing
-amgu (Var x) (Var y) [<] = Just (Evidence _ (flexFlex x y).snd)
+amgu (Var x) (Var y) [<] = Just (flexFlex x y)
 amgu (Var x) (Op op' us) [<] = flexRigid x (Op op' us)
 amgu (Op op ts) (Var y) [<] = flexRigid y (Op op ts)
 amgu t@(Var _) u@(Var _) (sub :< (v, z)) =
@@ -230,13 +230,13 @@ amgu t@(Var _) u@(Op _ _) (sub :< (v, z)) =
 amgu t@(Op _ _) u@(Var _) (sub :< (v, z)) =
   (:< (v, z)) <$> amgu ((v `for` z) <$> t) ((v `for` z) <$> u) sub
 
-amguAll [] [] acc = Just (Evidence _ acc)
+amguAll [] [] acc = Just (_ ** acc)
 amguAll (t :: ts) (u :: us) acc = do
   acc <- amgu t u acc
   amguAll ts us acc.snd
 
 export
-mgu : DecOp sig => {n : Nat} -> (t, u : Term sig n) -> Maybe (Exists (AList sig n))
+mgu : DecOp sig => {n : Nat} -> (t, u : Term sig n) -> Maybe (k ** AList sig n k)
 mgu t u = amgu t u [<]
 
 -- Properties
@@ -258,17 +258,17 @@ flexFlexUnifies {n = S n} x y with (thickProof x y)
     trivialUnify Var (Var x)
   flexFlexUnifies {n = S n} x _ | Thinned y prf =
     rewrite prf in
-    (Max (Unifies (Var x) (Var _))).cong _ _
+    (UniqueMax (Unifies (Var x) (Var _))).cong _ _
       (\i => sym $ subUnit ((Var y `for` x) i))
       (varElim x (Var y))
 
-data FlexRigidProof : Fin n -> Term sig n -> Maybe (Exists (AList sig n)) -> Type where
+data FlexRigidProof : Fin n -> Term sig n -> Maybe (k ** AList sig n k) -> Type where
   NoUnifier : Nothing (Unifies (Var x) t) -> res = Nothing -> FlexRigidProof x t res
   ElimVar :
     {n : Nat} ->
     (sub : AList sig k n) ->
     (mgu : MostGeneral (Unifies (Var x) t) (eval sub)) ->
-    res = Just (Evidence _ sub) ->
+    res = Just (_ ** sub) ->
     FlexRigidProof x t res
 
 flexRigidProof :
@@ -301,7 +301,7 @@ flexRigidProof {n = S n} x op ts with (checkProof x (Op op ts))
     rewrite prf in
     ElimVar
       [<(Op op us, x)]
-      ((Max (Unifies (Var x) (Op op _))).cong _ _
+      ((UniqueMax (Unifies (Var x) (Op op _))).cong _ _
         (\i => sym $ subUnit ((Op op us `for` x) i))
         (varElim x (Op op us)))
       Refl
@@ -322,7 +322,7 @@ parameters {auto _ : DecOp sig}
     Term sig k ->
     Term sig k ->
     AList sig k n ->
-    Maybe (Exists (AList sig k)) ->
+    Maybe (n ** AList sig k n) ->
     Type
     where
     Failure :
@@ -334,7 +334,7 @@ parameters {auto _ : DecOp sig}
       {0 sub : AList sig k n} ->
       (sub' : AList sig n j) ->
       MostGeneral (Extension (Unifies t u) (eval sub)) (eval sub') ->
-      res = Just (Evidence _ (sub' ++ sub)) ->
+      res = Just (_ ** sub' ++ sub) ->
       AmguProof t u sub res
 
   public export
@@ -342,7 +342,7 @@ parameters {auto _ : DecOp sig}
     Vect j (Term sig k) ->
     Vect j (Term sig k) ->
     AList sig k n ->
-    Maybe (Exists (AList sig k)) ->
+    Maybe (n ** AList sig k n) ->
     Type
     where
     FailureAll :
@@ -354,7 +354,7 @@ parameters {auto _ : DecOp sig}
       {0 sub : AList sig k n} ->
       (sub' : AList sig n j) ->
       MostGeneral (Extension (UnifiesAll ts us) (eval sub)) (eval sub') ->
-      res = Just (Evidence _ (sub' ++ sub)) ->
+      res = Just (_ ** sub' ++ sub) ->
       AmguAllProof ts us sub res
 
 export
@@ -378,8 +378,8 @@ amguProof (Op op ts) (Op op' us) sub with (decOp (Evidence _ op) (Evidence _ op'
     _ | SuccessAll sub' val prf' =
       let
         cong :
-          Max (Extension (Unifies (Op op ts) (Op op us)) (eval sub)) <=>
-          Max (Extension (UnifiesAll ts us) (eval sub))
+          UniqueMax (Extension (Unifies (Op op ts) (Op op us)) (eval sub)) <=>
+          UniqueMax (Extension (UnifiesAll ts us) (eval sub))
         cong = maxCong $ extendCong (eval sub) $ unifiesOp op ts us
       in
       Success sub'
@@ -397,7 +397,10 @@ amguProof (Var x) (Var y) [<] =
   Success
     (flexFlex x y).snd
     (flexFlexUnifies x y)
-    Refl
+    (cong Just $ ext _ (flexFlex x y))
+  where
+  ext : (0 b : a -> Type) -> (v : (x : a ** b x)) -> v = (v.fst ** v.snd)
+  ext b (fst ** snd) = Refl
 amguProof (Var x) (Op op' us) [<] with (flexRigidProof x op' us)
   _ | NoUnifier absurd prf = Failure absurd prf
   _ | ElimVar sub val prf = Success sub val prf
@@ -413,8 +416,8 @@ amguProof (Op op ts) (Var y) [<] with (flexRigidProof y op ts)
   _ | ElimVar sub val prf =
     let
       cong :
-        Max (Extension (Unifies (Var y) (Op op ts)) Var) <=>
-        Max (Extension (Unifies (Op op ts) (Var y)) Var)
+        UniqueMax (Extension (Unifies (Var y) (Op op ts)) Var) <=>
+        UniqueMax (Extension (Unifies (Op op ts) (Var y)) Var)
       cong = maxCong $ extendCong Var $ unifiesSym (Var y) (Op op ts)
     in
     Success sub (cong.leftToRight _ val) prf
@@ -423,8 +426,8 @@ amguProof (Var x) (Var y) (sub :< (v, z))
   _ | Success sub' val prf =
     let
       cong' :
-        Max (Extension (Unifies (Var x) (Var y)) (eval sub . (v `for` z))) <=>
-        Max (Extension (Unifies ((v `for` z) x) ((v `for` z) y)) (eval sub))
+        UniqueMax (Extension (Unifies (Var x) (Var y)) (eval sub . (v `for` z))) <=>
+        UniqueMax (Extension (Unifies ((v `for` z) x) ((v `for` z) y)) (eval sub))
       cong' = maxCong $ stepEquiv (Var x) (Var y) sub v z
     in
     Success sub'
@@ -439,8 +442,8 @@ amguProof (Var x) (Op op' us) (sub :< (v, z))
   _ | Success sub' val prf =
     let
       cong' :
-        Max (Extension (Unifies (Var x) (Op op' us)) (eval sub . (v `for` z))) <=>
-        Max (Extension (Unifies ((v `for` z) x) ((v `for` z) <$> Op op' us)) (eval sub))
+        UniqueMax (Extension (Unifies (Var x) (Op op' us)) (eval sub . (v `for` z))) <=>
+        UniqueMax (Extension (Unifies ((v `for` z) x) ((v `for` z) <$> Op op' us)) (eval sub))
       cong' = maxCong $ stepEquiv (Var x) (Op op' us) sub v z
     in
     Success sub'
@@ -455,8 +458,8 @@ amguProof (Op op ts) (Var y) (sub :< (v, z))
   _ | Success sub' val prf =
     let
       cong' :
-        Max (Extension (Unifies (Op op ts) (Var y)) (eval sub . (v `for` z))) <=>
-        Max (Extension (Unifies ((v `for` z) <$> Op op ts) ((v `for` z) y)) (eval sub))
+        UniqueMax (Extension (Unifies (Op op ts) (Var y)) (eval sub . (v `for` z))) <=>
+        UniqueMax (Extension (Unifies ((v `for` z) <$> Op op ts) ((v `for` z) y)) (eval sub))
       cong' = maxCong $ stepEquiv (Op op ts) (Var y) sub v z
     in
     Success sub'
@@ -470,7 +473,7 @@ amguProof (Op op ts) (Var y) (sub :< (v, z))
 amguAllProof [] [] sub =
   SuccessAll [<]
     (varMostGeneral [])
-    (sym $ cong (\sub => Just (Evidence _ sub)) $ appendUnitLeft sub)
+    (sym $ cong (\sub => Just (_ ** sub)) $ appendUnitLeft sub)
 amguAllProof (t :: ts) (u :: us) sub with (amguProof t u sub)
   _ | Success sub' val prf with (amguAllProof ts us (sub' ++ sub))
     _ | SuccessAll sub'' val' prf' =
@@ -483,11 +486,11 @@ amguAllProof (t :: ts) (u :: us) sub with (amguProof t u sub)
           cong'.leftToRight (eval sub'') val'
       in
       SuccessAll (sub'' ++ sub')
-        ((Max (Extension (UnifiesAll (t :: ts) (u :: us)) (eval sub))).cong _ _
+        ((UniqueMax (Extension (UnifiesAll (t :: ts) (u :: us)) (eval sub))).cong _ _
           (\i => sym $ evalHomo sub'' sub' i)
           opt)
         (rewrite prf in rewrite prf' in
-          cong (\sub => Just (Evidence _ sub)) $
+          cong (\sub => Just (_ ** sub)) $
           appendAssoc sub'' sub' sub)
     _ | FailureAll absurd prf' =
       let
@@ -504,11 +507,12 @@ amguAllProof (t :: ts) (u :: us) sub with (amguProof t u sub)
 parameters {auto _ : DecOp sig}
   namespace MguProof
     public export
-    data MguProof : (t, u : Term sig k) -> Maybe (Exists (AList sig k)) -> Type where
+    data MguProof : (t, u : Term sig k) -> Maybe (n ** AList sig k n) -> Type where
       Success :
+        {n : Nat} ->
         (sub : AList sig k n) ->
         MostGeneral (Unifies t u) (eval sub) ->
-        res = Just (Evidence _ sub) ->
+        res = Just (_ ** sub) ->
         MguProof t u res
       Failure :
         Nothing (Unifies t u) ->
@@ -520,3 +524,13 @@ mguProof : DecOp sig => {k : Nat} -> (t, u : Term sig k) -> MguProof t u (mgu t
 mguProof t u with (amguProof t u [<])
   _ | Success sub val prf = Success sub val prf
   _ | Failure absurd prf = Failure absurd prf
+
+export
+invertMgu :
+  DecOp sig =>
+  {0 t, u : Term sig k} ->
+  MguProof t u res ->
+  res = Just (_ ** sub) ->
+  MostGeneral (Unifies t u) (eval sub)
+invertMgu (Success sub mg Refl) Refl = mg
+invertMgu (Failure _ prf) Refl = absurd prf