&gt;Unfortunately, the termination checker cannot deal well with tuples. Please try a curried version of mgu1 instead:<br>&gt;  mgu1 : List (T * T) -&gt; N -&gt; N -&gt; N -&gt; Maybe Subs<br>
&gt;Cheers,<br>
&gt;Andreas<br><br>Thanks Andreas! Surprisingly (for me), changing to a curried version did work! (Surprising for me because I think making the termination checker work with tuples also should not be difficult). <br><br>
The curried version of mgu1 is below; it compiles ok also with a with-expression (i.e. it also compiles ok by uncommenting lines W1,W2,W3 and commenting line I). <br><br>Cheers, <br><br>Carlos<br><br>======================================================================<br>
module Unif where<br><br>open import Relation.Nullary.Decidable using (⌊_⌋)<br>open import Data.Bool                  using (Bool; false; _∨_; if_then_else_)<br>open import Data.Nat                   using (â„•; suc; _+_; _≟_; zero)<br>
open import Data.Maybe.Core       using (Maybe; nothing; just)<br>open import Data.Product             using (_×_; _,_; proj₁)<br>open import Data.List                   using (List; []; [_]; _∷_; map; sum; length; concat; filter)<br>
open import Function                   using (_∘_)<br>open import Relation.Nullary.Core  using (yes; no)<br>open import Relation.Binary.Core   using (Decidable; _≡_; refl)<br><br>{- ===================== Ty.agda ===================================-} <br>
<br>𝕍ar  : Set <br>𝕍ar = â„•<br><br>𝕍ars : Set<br>𝕍ars = List â„•<br><br>mem : â„• â†’ ð•ars â†’ Bool<br>mem _ []      = false<br>mem a (b âˆ· x) = âŒŠ a â‰Ÿ b âŒ‹ âˆ¨ mem a x<br><br>union : ð•ars â†’ ð•ars â†’ ð•ars<br>union []      y = y<br>
union (a âˆ· x) y = if mem a y then union x y else a âˆ· union x y<br><br>data ð•‹ : Set where<br> Con : â„• â†’ ð•‹Â Â Â Â  {- type constructor -}<br> Var : â„• â†’ ð•‹Â Â Â Â  {- type variable -}<br> _⇒_ : ð•‹ â†’ ð•‹ â†’ ð•‹ {- function type -}<br>
<br>vars : ð•‹ â†’ ð•ars<br>vars (Con _)   = []<br>vars (Var v)   = [ v ]<br>vars (ta â‡’ tb) = union (vars ta) (vars tb)<br><br>varsP : ð•‹ Ã— ð•‹ â†’ ð•ars<br>varsP (t , t&#39;) = union (vars t) (vars t&#39;)<br><br>numVarsL : List (𝕋 Ã— ð•‹) â†’ â„• <br>
numVarsL = length âˆ˜ concat âˆ˜ map varsP <br><br>numVars : ð•‹ â†’ â„•<br>numVars = length âˆ˜ vars<br><br>numConstructors : ð•‹ â†’ â„•<br>numConstructors (Con _)   = 1<br>numConstructors (Var _)   = 0<br>numConstructors (ta â‡’ tb) = 1 + numConstructors ta + numConstructors tb<br>
<br>numConstructorsP : (𝕋 Ã— ð•‹) â†’ â„•<br>numConstructorsP (t , t&#39;) = numConstructors t + numConstructors t&#39;<br><br>numConstructorsLP : List (𝕋 Ã— ð•‹) â†’ â„•<br>numConstructorsLP = sum âˆ˜ map numConstructorsP <br><br>{- ===========end of Ty.agda ========================================== -}<br>
<br>{- ===========Subst.agda ========================================== -}<br>Mapping : Set<br>Mapping = ð•ar Ã— ð•‹<br><br>Subs : Set<br>Subs = List Mapping<br><br>emptySubs : Subs<br>emptySubs = []<br><br>insert : ð•ar â†’ ð•‹ â†’ Subs â†’ Subs<br>
insert v st s = (v , st) âˆ· s<br><br>find : ð•ar â†’ Subs â†’ Maybe ð•‹<br>find v s with filter (λ vt â†’ âŒŠ proj₁ vt â‰Ÿ v âŒ‹)  s<br>... | []          = nothing<br>... | (_ , t) âˆ· _ = just t <br><br>apply : Subs â†’ ð•‹ â†’ ð•‹<br>apply s (Var v) with find v s <br>
... | just t       = t<br>... | nothing      = Var v<br>apply s (Con c)    = Con c<br>apply s (ta â‡’ tb)  = (apply s ta) â‡’ (apply s tb)<br><br>applyP : Subs â†’ (𝕋 Ã— ð•‹) â†’ (𝕋 Ã— ð•‹)<br>applyP s (t , t&#39;) = (apply s t , apply s t&#39;)<br>
<br>applyL : Subs â†’ List (𝕋 Ã— ð•‹) â†’ List (𝕋 Ã— ð•‹)<br>applyL s l = map (applyP s) l <br><br>{- =============end of Subst.agda =============================================== -}<br><br>num_pairs_tv : ð•‹ Ã— ð•‹ â†’ â„•<br>num_pairs_tv (Var _ , _)         = 0<br>
num_pairs_tv (_ , Var _)         = 1<br>num_pairs_tv (ta â‡’ tb , tc â‡’ td) = num_pairs_tv (ta , tc) + num_pairs_tv (tb , td)<br>num_pairs_tv _                   = 0<br><br>num_pairs_tvL : List (𝕋 Ã— ð•‹) â†’ â„•<br>num_pairs_tvL = sum âˆ˜ map num_pairs_tv <br>
<br>occurs : ð•ar â†’ ð•‹ â†’ Bool<br>occurs Î½ (Var Î½&#39;)  = âŒŠ Î½&#39; â‰Ÿ Î½ âŒ‹<br>occurs _ (Con _)   = false<br>occurs Î½ (ta â‡’ tb) = (occurs Î½ ta) âˆ¨ (occurs Î½ tb)<br><br>mgu1 : List (𝕋 Ã— ð•‹) â†’ â„• â†’ â„• â†’ â„• â†’ Maybe Subs<br>--   v = number of variables    <br>
--   c = number of constructors <br>--   k = sum of number of pairs (t,v) where v is (and t is not) a variable;<br>-- k is the decreasing measure in rec. calls where t1 is not and t2 is a var, first arg = ((t1,t2) âˆ· _).<br>
mgu1 [] _ _ _                                                      = just emptySubs <br>mgu1 ((Con _ , _) âˆ· _) _ 0 _                                = nothing -- impossible<br>-- mgu1 ((Con n1 , Con n2) âˆ· pairs_t) v (suc c) k   = if âŒŠ n1 â‰Ÿ n2 âŒ‹ then mgu1 pairs_t v c k else nothing  -- line I<br>
<br>mgu1 ((Con n1 , Con n2) âˆ· pairs_t)   v (suc c) k  with n1 â‰Ÿ n2                     -- line W1<br>mgu1 ((Con n1 , Con .n1) âˆ· pairs_t)  v (suc c) k  | yes refl = mgu1 pairs_t  v c k -- line W2<br>mgu1 ((Con n1 , Con n2) âˆ· pairs_t)   v (suc c) k  | no _     = nothing             -- line W3<br>
<br>mgu1 ((Con _ , _ â‡’ _) âˆ· _)  _ _ _                         = nothing<br>mgu1 ((Con _ , Var _) âˆ· pairs_t)     v  c 0              = nothing -- impossible<br>mgu1 ((Con c1 , Var v2) âˆ· pairs_t)   v  c (suc k)    = mgu1 ((Var v2 , Con c1) âˆ· pairs_t) v c k<br>
<br>mgu1 ((_ â‡’ _ , _) âˆ· pairs_t)         _  0 _                = nothing -- impossible<br>mgu1 ((_ â‡’ _ , Con _) âˆ· _)           _  _ _               = nothing<br>mgu1 ((_ â‡’ _ , Var v2) âˆ· pairs_t)    _ _ 0              = nothing -- impossible<br>
mgu1 ((ta â‡’ tb , Var v2) âˆ· pairs_t)  v c (suc k)      = mgu1 ((Var v2 , ta â‡’ tb) âˆ· pairs_t) v c k<br>mgu1 ((_ â‡’ _ , _ â‡’ _) âˆ· _)           _ (suc 0) _        = nothing -- impossible<br>mgu1 ((ta â‡’ tb , tc â‡’ td) âˆ· pairs_t) v (suc (suc c)) k = mgu1 ((ta , tc) âˆ· (tb , td) âˆ· pairs_t) v c k<br>
<br>mgu1 ((Var _ , _)   âˆ· _ )            0 _ _                    = nothing -- impossible<br>mgu1 ((Var v1 , Var v2) âˆ· pairs_t)   (suc v) c k      = let s      Â Â  = insert v1 (Var v2) emptySubs<br>                                                                                 pairs_t&#39; = applyL s pairs_t<br>
                                                              Â  Â  Â  Â  Â  Â  Â  Â  in if âŒŠ v1 â‰Ÿ v2 âŒ‹ then mgu1 pairs_t (suc v) c k<br>                                                                                 else mgu1 pairs_t v c k<br>
mgu1 ((Var v1 , t2) âˆ· pairs_t)       (suc v) c k         = let s  Â Â  Â Â Â Â  = insert v1 t2 emptySubs<br>                                                                                  pairs_t&#39; = applyL s pairs_t<br>                                                                                  c&#39;   Â Â  Â Â  = numConstructorsLP pairs_t&#39;<br>
                                                                 Â  Â  Â  Â  Â  Â  Â  Â Â  k&#39; Â Â  Â Â Â Â  = num_pairs_tvL pairs_t&#39;<br>                                                                              in if occurs v t2 then nothing <br>
                                                                                 else mgu1 pairs_t&#39; v c&#39; k&#39;<br>============================================================================<br><br><br>