[Agda] Termination checking
Francesco Mazzoli
f at mazzo.li
Sun Nov 9 16:41:57 CET 2014
Danke!
Francesco
On 8 November 2014 20:16, Andreas Abel <abela at chalmers.se> wrote:
> Here you go:
>
> https://github.com/agda/agda/commit/bde295096843265fd5386c8bba1b9104ac1e7c22
>
>
> On 08.11.2014 15:05, Andreas Abel wrote:
>>
>> Agda.Termination.TermCheck:
>>
>> -- TODO: isSubTerm should compute a size difference (Order)
>> isSubTerm :: Term -> DeBruijnPat -> Bool
>> isSubTerm t p = equal t p || properSubTerm t p
>>
>> Maybe a good time to address this TODO... ;-)
>>
>> On 08.11.2014 14:57, Andreas Abel wrote:
>>>
>>> The subterm checker of the termination checker is probably not working.
>>>
>>> It works if you use an explicit equality constraint in constructor ⟦_⟫_⟧.
>>>
>>> ⟦_⟫_⟧ : ∀ {d d₁ d₂ ol l nl} {eq : d ≡ d₁ + d₂} → Subst d₁ ol l ->
>>> Subst d₂ l nl -> Subst (suc d) ol nl
>>>
>>> lookup .(suc d) v (⟦_⟫_⟧ {d} {eq = eq} ρ σ) = lookup d v (_⟫_ {eq
>>> = eq} ρ σ)
>>>
>>> Full code attached.
>>>
>>>
>>> On 08.11.2014 14:10, Francesco Mazzoli wrote:
>>>>
>>>> mutual
>>>> data Tm (l : ℕ) : Set where
>>>> var : Fin l -> Tm l
>>>> _·_ : Tm l -> Tm l -> Tm l
>>>> lam : Tm (suc l) -> Tm l
>>>> ⟦_,_⟧ : ∀ {d ol} -> Tm ol -> Subst d ol l -> Tm l
>>>>
>>>> data Subst : (d : ℕ)(ol : ℕ)(nl : ℕ) -> Set where
>>>> id : ∀ {ol} -> Subst 0 ol ol
>>>> _∷_ : ∀ {d ol nl} -> Tm nl -> Subst d ol nl -> Subst d (suc
>>>> ol) nl
>>>> ⟦_⟫_⟧ : ∀ {d₁ d₂ ol l nl} -> Subst d₁ ol l -> Subst d₂ l nl ->
>>>> Subst (suc (d₁ + d₂)) ol nl
>>>>
>>>> _⟫_ : ∀ {d₁ d₂ ol l nl} -> Subst d₁ ol l -> Subst d₂ l nl -> Subst (d₁
>>>> + d₂) ol nl
>>>> id ⟫ σ = σ
>>>> (t ∷ ρ) ⟫ σ = ⟦ t , σ ⟧ ∷ (ρ ⟫ σ)
>>>> _⟫_ .{suc (d₁ + d₂)} {d₃} {ol} {_} {nl} (⟦_⟫_⟧ {d₁} {d₂} ρ σ) γ =
>>>> subst (λ d → Subst d ol nl) (lm d₁ d₂ d₃) (ρ ⟫ ⟦ σ ⟫ γ ⟧)
>>>> where
>>>> lm : ∀ n m k -> n + suc (m + k) ≡ suc (n + m + k)
>>>> lm zero m k = refl
>>>> lm (suc n) m k = cong suc (lm n m k)
>>>>
>>>> lookup : ∀ {ol nl} d -> Fin ol -> Subst d ol nl -> Tm nl
>>>> lookup .0 v id = var v
>>>> lookup d zero (t ∷ ρ) = t
>>>> lookup d (suc v) (t ∷ ρ) = lookup d v ρ
>>>> lookup .(suc (d₁ + d₂)) v (⟦_⟫_⟧ {d₁} {d₂} ρ σ) = lookup (d₁ +
>>>> d₂) v (ρ ⟫ σ)
>>>
>>>
>>>
>>>
>>>
>>>
>>> _______________________________________________
>>> Agda mailing list
>>> Agda at lists.chalmers.se
>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>
>>
>>
>
>
> --
> Andreas Abel <>< Du bist der geliebte Mensch.
>
> Department of Computer Science and Engineering
> Chalmers and Gothenburg University, Sweden
>
> andreas.abel at gu.se
> http://www2.tcs.ifi.lmu.de/~abel/
More information about the Agda
mailing list