Hi. Is the following ok, or a bug? <br><br>With line I (with an if-then-else expression) uncommented, module Unif compiles ok (no error detected), but<br>commenting line I and uncommenting lines W1, W2, W3 (using a with-expression instead of if-then-else), <br>
the termination checker complains (mgu1 becomes colored in light salmon).<br><br>I am using <span class="il">agda</span> version 2.3.0.1, on Ubuntu 12.04 LTS.<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>{- ========= was 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>{- =========== was 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>TerminationTriple : Set<br>TerminationTriple = ℕ × ℕ × ℕ<br><br>mgu1 : (List (𝕋 × 𝕋) × TerminationTriple) → Maybe Subs<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><span class="il"></span><br><br>