[Agda] Parameterized modules

[Andrés Sicard-Ramírez]

For simplifying the testing, I replaced in OList.agda

  open import Data.List

by

  infixr 5 _∷_

  data List (A : Set) : Set where
    []  : List A
    _∷_ : (x : A) (xs : List A) → List A


I confirm that the example type-checks with Agda 2.3.2.2. Moreover,
the example does not pass the termination checker with Agda 2.4.0.


On 30 May 2015 at 10:15, Bruno Bianchi <bgbianchi at gmail.com> 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))
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>



-- 
Andrés