<br><div class="gmail_quote">On Wed, Jul 3, 2013 at 12:09 PM, Carlos Camarao <span dir="ltr"><<a href="mailto:carlos.camarao@gmail.com" target="_blank">carlos.camarao@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div class="im">>Unfortunately, the termination checker cannot deal well with tuples. Please try a curried version of mgu1 instead:<br>>Â mgu1 : List (T * T) -> N -> N -> N -> Maybe Subs<br>
>Cheers,<br>
>Andreas<br><br></div>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></blockquote><div><br>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).<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') = union (vars t) (vars t')<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') = numConstructors t + numConstructors t'<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') = (apply s t , apply s t')<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 ν') = ⌊ ν' ≟ ν ⌋<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 with n1 ≟ n2 <br>
mgu1 ((Con n1 , Con .n1) ∷ pairs_t) v (suc c) k | yes refl = mgu1 pairs_t v c k <br>mgu1 ((Con n1 , Con n2) ∷ pairs_t)  v (suc c) k | no _    = nothing            <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       -- line I1<br>                                                                                          pairs_t' = applyL s pairs_t                -- line I2<br>
                                                                                       in if ⌊ v1 ≟ v2 ⌋ then mgu1 pairs_t (suc v) c k -- line I3<br>                                                                                          else mgu1 pairs_t v c k                -- line I4<br>
{- <br>mgu1 ((Var v1 , Var v2) ∷ pairs_t)  (suc v) c k with v1 ≟ v2                                                          -- line W1<br>mgu1 ((Var v1 , Var .v1) ∷ pairs_t)  (suc v) c k | yes refl = mgu1 pairs_t (suc v) c k                       -- line W2<br>
mgu1 ((Var v1 , Var v2) ∷ pairs_t)  (suc v) c k | no _     = let s       = insert v1 (Var v2) emptySubs -- line W3<br>                                                                                         pairs_t' = applyL s pairs_t                  -- line W4<br>
                                                                                      in mgu1 pairs_t v c k                           -- line W5<br>-}<br>mgu1 ((Var v1 , t2) ∷ pairs_t)      (suc v) c k           = let s       = insert v1 t2 emptySubs<br>
                                                                                    pairs_t' = applyL s pairs_t<br>                                                                                    c'      = numConstructorsLP pairs_t'<br>
                                                                                    k'      = num_pairs_tvL pairs_t'<br>                                                                                in if occurs v t2 then nothing <br>
                                                                                else mgu1 pairs_t' v c' k'<br><br>======================================================================<br></div></div>