[Agda] Parameterized modules

[Andreas Abel]

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/