[Agda] Termination checking

[Andreas Abel]

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/