From bb4e7c82b7ecd93b7241be5fcc547cfd282a8908 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Sun, 16 Jul 2023 15:19:15 +0100
Subject: Minor changes for use by other projects.

---
 src/Data/Term/Unify.idr | 31 ++++++++++++++++---------------
 1 file changed, 16 insertions(+), 15 deletions(-)

(limited to 'src/Data/Term')

diff --git a/src/Data/Term/Unify.idr b/src/Data/Term/Unify.idr
index f75a61a..b87ab21 100644
--- a/src/Data/Term/Unify.idr
+++ b/src/Data/Term/Unify.idr
@@ -4,6 +4,7 @@ import Data.DPair
 import Data.Fin.Occurs
 import Data.Fin.Strong
 import Data.Maybe.Properties
+import Data.Singleton
 import Data.Term
 import Data.Term.Property
 import Data.Term.Zipper
@@ -197,6 +198,11 @@ sub ++ sub1 :< tx = (sub ++ sub1) :< tx
 
 -- Properties
 
+export
+recover : Singleton k -> AList sig k n -> Singleton n
+recover x [<] = x
+recover x (sub :< _) = recover (pure pred <*> x) sub
+
 export
 evalHomo :
   (0 sub2 : AList sig k n) ->
@@ -239,17 +245,17 @@ flexRigid x t = case check x t of
 
 export
 amgu :
-  DecEq sig.Op =>
+  DecOp sig =>
   (t, u : Term sig n) ->
   Exists (AList sig n) ->
   Maybe (Exists (AList sig n))
 amguAll :
-  DecEq sig.Op =>
+  DecOp sig =>
   (ts, us : Vect k (Term sig n)) ->
   Exists (AList sig n) ->
   Maybe (Exists (AList sig n))
 
-amgu (Op op ts) (Op op' us) acc with (decEq {t = sig.Op} (Evidence _ op) (Evidence _ op'))
+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) (Evidence _ [<]) = Just (flexFlex x y)
@@ -268,7 +274,7 @@ amguAll (t :: ts) (u :: us) acc = do
   amguAll ts us acc
 
 export
-mgu : DecEq sig.Op => (t, u : Term sig n) -> Maybe (Exists (AList sig n))
+mgu : DecOp sig => (t, u : Term sig n) -> Maybe (Exists (AList sig n))
 mgu t u = amgu t u (Evidence _ [<])
 
 -- Properties
@@ -364,7 +370,7 @@ stepEquiv :
   Extension (Unifies ((v `for` x) <$> t) ((v `for` x) <$> u)) (eval sub)
 stepEquiv t u sub v x = extendUnify t u (v `for` x) (eval sub)
 
-parameters {auto _ : DecEq sig.Op}
+parameters {auto _ : DecOp sig}
   public export
   data AmguProof : (t, u : Term sig k) -> Exists (AList sig k) -> Type where
     Success :
@@ -394,20 +400,15 @@ parameters {auto _ : DecEq sig.Op}
       AmguAllProof ts us sub
 
 export
-amguProof :
-  DecEq sig.Op =>
-  (t, u : Term sig n) ->
-  (sub : Exists (AList sig n)) ->
-  AmguProof t u sub
+amguProof : DecOp sig => (t, u : Term sig n) -> (sub : Exists (AList sig n)) -> AmguProof t u sub
 export
 amguAllProof :
-  DecEq sig.Op =>
+  DecOp sig =>
   (ts, us : Vect k (Term sig n)) ->
   (sub : Exists (AList sig n)) ->
   AmguAllProof ts us sub
 
-amguProof (Op op ts) (Op op' us) sub
-  with (decEq {t = sig.Op} (Evidence _ op) (Evidence _ op')) proof prf
+amguProof (Op op ts) (Op op' us) sub with (decOp (Evidence _ op) (Evidence _ op')) proof prf
   amguProof (Op op ts) (Op op us) sub | Yes Refl
     with (amguAllProof ts us sub)
     _ | SuccessAll sub' val prf' =
@@ -541,7 +542,7 @@ amguAllProof (t :: ts) (u :: us) sub with (amguProof t u sub)
       (failHead absurd)
       (bindNothing prf (amguAll ts us))
 
-parameters {auto _ : DecEq sig.Op}
+parameters {auto _ : DecOp sig}
   namespace MguProof
     public export
     data MguProof : (t, u : Term sig k) -> Type where
@@ -556,7 +557,7 @@ parameters {auto _ : DecEq sig.Op}
         MguProof t u
 
 export
-mguProof : DecEq sig.Op => (t, u : Term sig k) -> MguProof t u
+mguProof : DecOp sig => (t, u : Term sig k) -> MguProof t u
 mguProof t u with (amguProof t u (Evidence _ [<]))
   _ | Success (Evidence _ sub) val prf = Success (Evidence _ sub) val prf
   _ | Failure absurd prf = Failure absurd prf
-- 
cgit v1.2.3