[Agda] Parameterized modules

[Bruno Bianchi]

Thank you!

2015-05-31 21:39 GMT+08:00 Andreas Abel <abela at chalmers.se>:

> Thanks for reporting this issue.  I fixed the problem:
>
>   https://code.google.com/p/agda/issues/detail?id=1530
>
>
> On 30.05.2015 17:15, Bruno Bianchi wrote:
>
>> Hi,
>> I'm trying to compile the following two modules in 2.4.2.3, but for some
>> reason the second one does not pass the termination checker due to the
>> recursive call in olist-sorted. If I include the content of the first
>> module instead of importing it, then it does pass the termination
>> checker. If I remove the parameters from both modules and I postulate
>> them in a third one (which would be imported by both modules), then I'm
>> also able to pass the termination checker.
>> Is there any way to make such parameterized modules pass the termination
>> checker in 2.4.2.3? It used to work in 2.3.2.2.
>> Thanks in advance,
>> Bruno
>> Bound.agda
>> ----------------
>> module Bound {A : Set}(_<=_ : A -> A -> Set) where
>> data Bound : Set where
>>    bot : Bound
>>    val : A -> Bound
>> data LeB : Bound -> Bound -> Set where
>>    lebx : {b : Bound} -> LeB bot b
>>    lexy : {a b : A} -> a <= b -> LeB (val a) (val b)
>> OList.agda
>> ---------------
>> module OList {A : Set}(_<=_ : A -> A -> Set) where
>> open import Data.List
>> open import Bound _<=_
>> data OList : Bound -> Set where
>>    nil : {b : Bound} -> OList b
>>    cons : {b : Bound}{x : A} -> LeB b (val x) -> OList (val x) -> OList b
>> forget : {b : Bound} -> OList b -> List A
>> forget nil = []
>> forget (cons {x = x} _ xs) = x :: forget xs
>> data Sorted : List A -> Set where
>>    empty : Sorted []
>>    single : (x : A) -> Sorted (x :: [])
>>    step : {x y : A}{ys : List A} -> x <= y -> Sorted (y :: ys) -> Sorted
>> (x :: y :: ys)
>> olist-sorted : {b : Bound}(xs : OList b) -> Sorted (forget xs)
>> olist-sorted nil = empty
>> olist-sorted (cons {x = x} _ nil) = single x
>> olist-sorted (cons b<=x (cons (lexy x<=y) ys)) = step x<=y (olist-sorted
>> (cons (lexy x<=y) ys))
>>
>
>
> --
> 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/
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150602/afe2dada/attachment.html