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

[Carlos Camarao]

On Wed, Jul 3, 2013 at 12:09 PM, Carlos Camarao <carlos.camarao at gmail.com>wrote:

> >Unfortunately, the termination checker cannot deal well with tuples.
> Please try a curried version of mgu1 instead:
> >  mgu1 : List (T * T) -> N -> N -> N -> Maybe Subs
> >Cheers,
> >Andreas
>
> 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).
>
> 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).  ...
>

Unfortunately, the problem "with-expression versus if-then-else" appears
again, in the following curried version of mgu1: the code below compiles ok
but mgu1 becomes colored in light salmon if if-then-else is replaced by a
with-expression (i.e. if lines I1 to I4 are commented and lines W1 to W5
are uncommented).

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)

{- ===================== 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 ========================================== -}

{- ===========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)

mgu1 : List (𝕋 × 𝕋) → ℕ → ℕ → ℕ → Maybe Subs
--   v = number of variables
--   c = number of constructors
--   k = sum of number of pairs (t,v) where v is (and t is not) a variable;
-- k is the decreasing measure in rec. calls where t1 is not and t2 is a
var, first arg = ((t1,t2) ∷ _).
mgu1 [] _ _ _
   = just emptySubs
mgu1 ((Con _ , _) ∷ _) _ 0 _                                           =
nothing -- impossible
mgu1 ((Con n1 , Con n2) ∷ pairs_t)   v (suc c) k  with n1 ≟ n2
mgu1 ((Con n1 , Con .n1) ∷ pairs_t)  v (suc c) k  | yes refl = mgu1
pairs_t  v c k
mgu1 ((Con n1 , Con n2) ∷ pairs_t)   v (suc c) k  | no _     =
nothing
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        -- line I1

pairs_t' = applyL s pairs_t                          -- line I2

in if ⌊ v1 ≟ v2 ⌋ then mgu1 pairs_t (suc v) c k -- line I3

else mgu1 pairs_t v c k                             -- line I4
{-
mgu1 ((Var v1 , Var v2) ∷ pairs_t)   (suc v) c k with v1 ≟
v2                                                             -- line W1
mgu1 ((Var v1 , Var .v1) ∷ pairs_t)   (suc v) c k | yes refl = mgu1 pairs_t
(suc v) c k                          -- line W2
mgu1 ((Var v1 , Var v2) ∷ pairs_t)   (suc v) c k  | no _      = let
s        = insert v1 (Var v2) emptySubs -- line W3

pairs_t' = applyL s pairs_t                    -- line W4

in mgu1 pairs_t v c k                              -- line W5
-}
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/20130703/df157b80/attachment.html