UlfNorell
commented
10 years ago From andreas....@gmail.com on October 24, 2013 07:29:04
The loop seems to be triggered by my fix for issue 423 in Unify.hs. However, I do not know if normalization just takes forbiddingly long, or whether it actually loops.
instance UReduce Term where ureduce u = doEtaContractImplicit $ do rho <- onSub makeSubstitution liftTCM $ etaContract =<< normalise (applySubst rho u) -- Andreas, 2011-06-22, fix related to issue 423 -- To make eta contraction work better, I switched reduce to normalise. -- I hope the performance penalty is not big (since we are dealing with -- l.h.s. terms only). -- A systematic solution would make unification type-directed and -- eta-insensitive... -- liftTCM $ etaContract =<< reduce (applySubst rho u)
From andreas....@gmail.com on October 24, 2013 16:26:44
Is was reported by Christoph-Simon Senjak to me that the following program "crashes". When trying it out, I found that there was some never ending normalization.
-- Bug reported by Christoph-Simon Senjak module UnifyConArgsLoops where
open import Level
open import Data.Empty open import Data.Product open import Data.Sum
open import Data.Bool
open import Data.Maybe.Core
import Data.Nat as ℕ open import Data.Nat using (ℕ) import Data.Nat.Divisibility as ℕ import Data.Nat.Properties as ℕ open import Data.Nat.DivMod
import Data.Fin as F open import Data.Fin using (Fin) import Data.Fin.Props as F
import Data.List as L open import Data.List using (List)
open import Data.Vec
open import Relation.Nullary.Core open import Relation.Binary.PropositionalEquality
open import Algebra open import Algebra.Structures
Byte : Set Byte = Fin 256
^ : ℕ → ℕ → ℕ _ ^ 0 = 1 n ^ (ℕ.suc m) = n ℕ.* (n ^ m)
BitVecToNat : {n : ℕ} → Vec Bool n → ℕ BitVecToNat [] = 0 BitVecToNat (true ∷ r) = ℕ.suc (2 ℕ.* (BitVecToNat r)) BitVecToNat (false ∷ r) = (2 ℕ.* (BitVecToNat r))
postulate ≤lem₁ : {a b : ℕ} → (a ℕ.< b) → (2 ℕ.* a) ℕ.< (2 ℕ.* b)
postulate ≤lem₂ : {a b : ℕ} → (a ℕ.< (ℕ.suc b)) → (ℕ.suc (2 ℕ.* a)) ℕ.< (2 ℕ.* (ℕ.suc b)) postulate ≤lem₃ : {a b c : ℕ} → (c ℕ.+ (a ℕ.* 2) ℕ.< (2 ℕ.* b)) → a ℕ.< b
¬0<b∧0≡b : {b : ℕ} → 0 ℕ.< b → 0 ≡ b → ⊥ ¬0<b∧0≡b {0} () 0≡b ¬0<b∧0≡b {ℕ.suc n} 0<b ()
0<a∧0<b→0<ab : (a b : ℕ) → (0 ℕ.< a) → (0 ℕ.< b) → (0 ℕ.< (a ℕ.* b)) 0<a∧0<b→0<ab a b 0<a 0<b with 1 ℕ.≤? (a ℕ.* b) ... | yes y = y ... | no n with (a ℕ.* b) | inspect (λ x → a ℕ.* x) b ... | ℕ.suc ns | _ = ⊥-elim (n (ℕ.s≤s (ℕ.z≤n {ns}))) ... | 0 | [ eq ] with ℕ.i*j≡0⇒i≡0∨j≡0 a {b} eq ... | inj₁ a≡0 = ⊥-elim (¬0<b∧0≡b 0<a (sym a≡0)) ... | inj₂ b≡0 = ⊥-elim (¬0<b∧0≡b 0<b (sym b≡0))
0<s^b : {a b : ℕ} → (0 ℕ.< ((ℕ.suc a) ^ b)) 0<s^b {_} {0} = ℕ.s≤s ℕ.z≤n 0<s^b {m} {ℕ.suc n} = 0<a∧0<b→0<ab (ℕ.suc m) ((ℕ.suc m) ^ n) (ℕ.s≤s ℕ.z≤n) (0<s^b {m} {n})
<-lemma : (b : ℕ) → (0 ℕ.< b) → ∃ λ a → ℕ.suc a ≡ b <-lemma (ℕ.suc b) (ℕ.s≤s (ℕ.z≤n {.b})) = ( b , refl )
2^lem₁ : (a : ℕ) → ∃ λ b → (ℕ.suc b) ≡ (2 ^ a) 2^lem₁ a = <-lemma (2 ^ a) (0<s^b {1} {a})
BitVecToNatLemma : {n : ℕ} → (s : Vec Bool n) → ((BitVecToNat s) ℕ.< (2 ^ n)) BitVecToNatLemma {0} [] = ℕ.s≤s ℕ.z≤n BitVecToNatLemma {ℕ.suc n} (false ∷ r) = ≤lem₁ (BitVecToNatLemma r) BitVecToNatLemma {ℕ.suc n} (true ∷ r) = ret₃ where q = 2^lem₁ n t = proj₁ q s : (ℕ.suc t) ≡ 2 ^ n s = proj₂ q ret₁ : (BitVecToNat r) ℕ.< (ℕ.suc t) ret₁ = subst (λ u → (BitVecToNat r) ℕ.< u) (sym s) (BitVecToNatLemma r) ret₂ : (ℕ.suc (2 ℕ.* (BitVecToNat r))) ℕ.< (2 ℕ.* (ℕ.suc t)) ret₂ = ≤lem₂ ret₁ ret₃ : (ℕ.suc (2 ℕ.* (BitVecToNat r))) ℕ.< (2 ^ (ℕ.suc n)) ret₃ = subst (λ u → (ℕ.suc (2 ℕ.* (BitVecToNat r))) ℕ.< (2 ℕ.* u)) s ret₂
BitVecToFin : {n : ℕ} → Vec Bool n → Fin (2 ^ n) BitVecToFin s = F.fromℕ≤ (BitVecToNatLemma s)
FinToBitVec : {n : ℕ} → (m : Fin (2 ^ n)) → ∃ λ (s : Vec Bool n) → (BitVecToFin s ≡ m) FinToBitVec {0} F.zero = ( [] , refl ) FinToBitVec {0} (F.suc ()) FinToBitVec {ℕ.suc n} k = ret where open CommutativeSemiring hiding (sym; trans; refl) renaming (-comm to sr-comm) -comm : (a b : ℕ) → a ℕ. b ≡ b ℕ.* a -comm = sr-comm ℕ.commutativeSemiring kn = F.toℕ k p2^n' = 2^lem₁ (ℕ.suc n) p2^n = proj₁ p2^n' p2^nl : ℕ.suc p2^n ≡ 2 ^ (ℕ.suc n) p2^nl = proj₂ p2^n' kn<2^n : kn ℕ.< 2 ^ (ℕ.suc n) kn<2^n = subst (λ d → kn ℕ.< d) p2^nl (subst (λ d → kn ℕ.< ℕ.suc (ℕ.pred d)) (sym p2^nl) (ℕ.s≤s (F.prop-toℕ-≤ k))) dm = kn divMod 2 quot = DivMod.quotient dm rem = F.toℕ (DivMod.remainder dm) Fin2toBool : Fin 2 → Bool Fin2toBool F.zero = false Fin2toBool (F.suc F.zero) = true Fin2toBool (F.suc (F.suc ())) zl = 2^lem₁ n lem₀ : rem ℕ.+ quot ℕ.* 2 ℕ.< (2 ^ (ℕ.suc n)) lem₀ = subst (λ d → d ℕ.< (2 ^ (ℕ.suc n))) (DivMod.property dm) kn<2^n lem₁ : (DivMod.quotient dm) ℕ.< (2 ^ n) lem₁ = ≤lem₃ {a = quot} {b = 2 ^ n} {c = rem} lem₀ fQuot : Fin (2 ^ n) fQuot = F.fromℕ≤ lem₁ prevRet : ∃ λ (s : Vec Bool n) → (BitVecToFin s ≡ fQuot) prevRet = FinToBitVec (F.fromℕ≤ lem₁) prevRetEq : (BitVecToFin (proj₁ prevRet) ≡ fQuot) prevRetEq = proj₂ prevRet lem₉ : {n : ℕ} → (r : Vec Bool n) → F.toℕ (BitVecToFin r) ≡ (BitVecToNat r) lem₉ r = trans (cong F.toℕ refl) (F.toℕ-fromℕ≤ (BitVecToNatLemma r)) prevRetEqℕ : quot ≡ BitVecToNat (proj₁ prevRet) prevRetEqℕ = trans (trans (sym (F.toℕ-fromℕ≤ lem₁)) (cong F.toℕ (sym prevRetEq))) (lem₉ (proj₁ prevRet)) ret₁ = (Fin2toBool (DivMod.remainder dm)) ∷ (proj₁ prevRet) lem₃ : (r : Fin 2) → (BitVecToNat ((Fin2toBool r) ∷ (proj₁ prevRet))) ≡ (F.toℕ r) ℕ.+ (2 ℕ.* (BitVecToNat (proj₁ prevRet))) lem₃ F.zero = refl lem₃ (F.suc F.zero) = refl lem₃ (F.suc (F.suc ())) lem₄ : (BitVecToNat ret₁) ≡ rem ℕ.+ (2 ℕ.* (BitVecToNat (proj₁ prevRet))) lem₄ = lem₃ (DivMod.remainder dm) lem₅ : rem ℕ.+ (2 ℕ.* (BitVecToNat (proj₁ prevRet))) ≡ kn lem₅ = subst (λ d → rem ℕ.+ d ≡ kn) (-comm (BitVecToNat (proj₁ prevRet)) 2) (subst (λ d → rem ℕ.+ d ℕ. 2 ≡ kn) prevRetEqℕ (sym (DivMod.property dm))) lem₆ : (BitVecToNat ret₁) ≡ kn lem₆ = trans lem₄ lem₅ lem₈ : kn ≡ F.toℕ (F.fromℕ≤ kn<2^n) lem₈ = sym (cong F.toℕ (F.fromℕ≤-toℕ k kn<2^n)) lem₇ : (BitVecToFin ret₁) ≡ k lem₇ = trans (F.toℕ-injective (trans (lem₉ ret₁) (trans lem₆ lem₈))) (F.fromℕ≤-toℕ k kn<2^n) ret = ( ret₁ , lem₇ )
record ByteStream : Set where constructor bs field cBit : Maybe (∃ λ (c : Fin 8) → Vec Bool (ℕ.suc (F.toℕ c))) str : List Byte property : (cBit ≡ nothing) → (str ≡ L.[])
byteStreamFromList : List Byte → ByteStream byteStreamFromList L.[] = bs nothing L.[](λ _ → refl) byteStreamFromList (a L.∷ x) = bs (just ( (F.fromℕ 7) , (proj₁ (FinToBitVec a)))) x (λ ())
Original issue: http://code.google.com/p/agda/issues/detail?id=924