[Agda] Termination checking, if-then-else X with

[Carlos Camarao]

Hi. Is the following ok, or a bug?

With line I (with an if-then-else expression) uncommented, module Unif
compiles ok (no error detected), but
commenting line I and uncommenting lines W1, W2, W3 (using a
with-expression instead of if-then-else),
the termination checker complains (mgu1 becomes colored in light salmon).

I am using agda version 2.3.0.1, on Ubuntu 12.04 LTS.

Cheers,

Carlos

===============================================
module Unif where

open import Relation.Nullary.Decidable using (⌊_⌋)
open import Data.Bool                  using (Bool; false; _∨_;
if_then_else_)
open import Data.Nat                   using (ℕ; suc; _+_; _≟_; zero)
open import Data.Maybe.Core       using (Maybe; nothing; just)
open import Data.Product             using (_×_; _,_; proj₁)
open import Data.List                   using (List; []; [_]; _∷_; map;
sum; length; concat; filter)
open import Function                   using (_∘_)
open import Relation.Nullary.Core using (yes; no)
open import Relation.Binary.Core  using (Decidable; _≡_; refl)

{- ========= was Ty.agda ==============-}

𝕍ar  : Set
𝕍ar = ℕ

𝕍ars : Set
𝕍ars = List ℕ

mem : ℕ → 𝕍ars → Bool
mem _ []      = false
mem a (b ∷ x) = ⌊ a ≟ b ⌋ ∨ mem a x

union : 𝕍ars → 𝕍ars → 𝕍ars
union []      y = y
union (a ∷ x) y = if mem a y then union x y else a ∷ union x y

data 𝕋 : Set where
 Con : ℕ → 𝕋     {- type constructor -}
 Var : ℕ → 𝕋     {- type variable -}
 _⇒_ : 𝕋 → 𝕋 → 𝕋 {- function type -}

vars : 𝕋 → 𝕍ars
vars (Con _)   = []
vars (Var v)   = [ v ]
vars (ta ⇒ tb) = union (vars ta) (vars tb)

varsP : 𝕋 × 𝕋 → 𝕍ars
varsP (t , t') = union (vars t) (vars t')

numVarsL : List (𝕋 × 𝕋) → ℕ
numVarsL = length ∘ concat ∘ map varsP

numVars : 𝕋 → ℕ
numVars = length ∘ vars

numConstructors : 𝕋 → ℕ
numConstructors (Con _)   = 1
numConstructors (Var _)   = 0
numConstructors (ta ⇒ tb) = 1 + numConstructors ta + numConstructors tb

numConstructorsP : (𝕋 × 𝕋) → ℕ
numConstructorsP (t , t') = numConstructors t + numConstructors t'

numConstructorsLP : List (𝕋 × 𝕋) → ℕ
numConstructorsLP = sum ∘ map numConstructorsP

{- ========== end of Ty.agda ================== -}

{- =========== was Subst.agda ================ -}
Mapping : Set
Mapping = 𝕍ar × 𝕋

Subs : Set
Subs = List Mapping

emptySubs : Subs
emptySubs = []

insert : 𝕍ar → 𝕋 → Subs → Subs
insert v st s = (v , st) ∷ s

find : 𝕍ar → Subs → Maybe 𝕋
find v s with filter (λ vt → ⌊ proj₁ vt ≟ v ⌋)  s
... | []          = nothing
... | (_ , t) ∷ _ = just t

apply : Subs → 𝕋 → 𝕋
apply s (Var v) with find v s
... | just t       = t
... | nothing      = Var v
apply s (Con c)    = Con c
apply s (ta ⇒ tb)  = (apply s ta) ⇒ (apply s tb)

applyP : Subs → (𝕋 × 𝕋) → (𝕋 × 𝕋)
applyP s (t , t') = (apply s t , apply s t')

applyL : Subs → List (𝕋 × 𝕋) → List (𝕋 × 𝕋)
applyL s l = map (applyP s) l

{- ============= end of Subst.agda ================ -}

num_pairs_tv : 𝕋 × 𝕋 → ℕ
num_pairs_tv (Var _ , _)         = 0
num_pairs_tv (_ , Var _)         = 1
num_pairs_tv (ta ⇒ tb , tc ⇒ td) = num_pairs_tv (ta , tc) + num_pairs_tv
(tb , td)
num_pairs_tv _                   = 0

num_pairs_tvL : List (𝕋 × 𝕋) → ℕ
num_pairs_tvL = sum ∘ map num_pairs_tv

occurs : 𝕍ar → 𝕋 → Bool
occurs ν (Var ν')  = ⌊ ν' ≟ ν ⌋
occurs _ (Con _)   = false
occurs ν (ta ⇒ tb) = (occurs ν ta) ∨ (occurs ν tb)

TerminationTriple : Set
TerminationTriple = ℕ × ℕ × ℕ

mgu1 : (List (𝕋 × 𝕋) × TerminationTriple) → Maybe Subs
mgu1 ([]                        ,         _         )       = just
emptySubs
mgu1 (((Con _ , _) ∷ _)         ,        (_ , 0 , _))       = nothing --
impossible
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

-- mgu1 (((Con n1 , Con n2) ∷ pairs_t)   ,    (v , suc c , k))   with n1 ≟
n2                                        -- line W1
-- mgu1 (((Con n1 , Con .n1) ∷ pairs_t)  ,    (v , suc c , k))   | yes refl
= mgu1 (pairs_t , (v , c , k) )   -- line W2
-- mgu1 (((Con n1 , Con n2) ∷ pairs_t)   ,    (v , suc c , k))   | no _
= nothing                               -- line W3

mgu1 (((Con _ , _ ⇒ _) ∷ _)           ,  _                ) = nothing
mgu1 (((Con _ , Var _) ∷ pairs_t)     ,    (v , c , 0)    ) = nothing --
impossible
mgu1 (((Con c1 , Var v2) ∷ pairs_t)   ,    (v , c , suc k)) = mgu1 (((Var
v2 , Con c1) ∷ pairs_t) , (v , c , k))

mgu1 (((_ ⇒ _ , _) ∷ pairs_t)         ,    (_ , 0 , _)    ) = nothing --
impossible
mgu1 (((_ ⇒ _ , Con _) ∷ _)           ,  _                ) = nothing
mgu1 (((_ ⇒ _ , Var v2) ∷ pairs_t)    ,  (_ , _ , 0)      ) = nothing --
impossible
mgu1 (((ta ⇒ tb , Var v2) ∷ pairs_t)  ,  (v , c , suc k)  ) = mgu1 (((Var
v2 , ta ⇒ tb) ∷ pairs_t) , (v , c , k))
mgu1 (((_ ⇒ _ , _ ⇒ _) ∷ _)           ,  (_ , suc 0 , _)  ) = nothing --
impossible
mgu1 (((ta ⇒ tb , tc ⇒ td) ∷ pairs_t) , (v , suc (suc c) , k)) = mgu1 (((ta
, tc) ∷ (tb , td) ∷ pairs_t) , (v , c , k))

mgu1 (((Var _ , _)   ∷ _ )            ,   (0 , _ , _)     ) = nothing --
impossible
mgu1 (((Var v1 , Var v2) ∷ pairs_t)   ,   (suc v , c , k) ) = let s
= insert v1 (Var v2) emptySubs
                                                                  pairs_t'
= applyL s pairs_t
                                                               in if ⌊ v1 ≟
v2 ⌋ then mgu1 (pairs_t , (suc v , c , k))

else mgu1 (pairs_t , (v , c , k))
mgu1 (((Var v1 , t2) ∷ pairs_t)       ,   (suc v , c , k) ) = let s
= insert v1 t2 emptySubs
                                                                  pairs_t'
= applyL s pairs_t
                                                                  c'
= numConstructorsLP pairs_t'
                                                                  k'
= num_pairs_tvL pairs_t'
                                                               in if occurs
v t2 then nothing

else mgu1 (pairs_t' , (v , c' , k'))
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130702/a614f125/attachment-0001.html