[Agda] Generic programming and pointfree stuff.

[Andreas Abel]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

I fixed the bug 1094 which you reported.

On 06.04.2014 03:11, flicky frans wrote:
>> you could try the development version of Agda (get from the darcs
>> repo) which has some performance improvements.  (Might be worth 
>> trying.)
> I tried, but got this error:
> 
> C:\Documents and Settings\ 4<8=8AB at 0B>@\Application 
> Data\cabal\Agda-2.3.3\lib\prim\Agda\Primitive.agda: openFile: 
> invalid argument (Invalid argument)
> 
> Locale problems. I searched for a way to unhardcode the path, but 
> didn't find it. Is there any?

Agda gets these pathes from Cabal, since they depend on the install
location, see e.g.


http://hackage.haskell.org/package/Cabal-1.18.1.1/docs/Distribution-Simple-InstallDirs.html#v:absoluteInstallDirs

You can check them in

  dist/build/Agda/autogen/Paths_Agda.hs

after 'cabal install' in wherever cabal has compiled Agda.

>> Conversion checking for Level is certainly incomplete.  Levels
>> are not meant for complicated computations.
> Previous version of this code typechecks. Last definition in this 
> messy module: http://lpaste.net/8416145096918958080 It's more
> complicated however. Just for the statistics: how many such a bugs
> with levels have you seen?

Don't know.  Half a dozen?!

>> You could file a bug report (google for "agda issues") with a
>> file that reproduces the problematic behavior.
> 
> I have no idea how to reproduce this bug with a smaller amount of
> code.

Then please report the problem using the full code (should be
self-contained except for std-lib, should trigger the error).

Cheers,
Andreas

- -- 
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/
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.11 (GNU/Linux)
Comment: Using GnuPG with Thunderbird - http://www.enigmail.net/

iEYEARECAAYFAlNBV3AACgkQPMHaDxpUpLOO5wCeM8nV6X5mryCSyFEVO9SlONOo
eyUAoPVZCQF9RsdN1utOQMtATeMHzWbB
=cv9I
-----END PGP SIGNATURE-----