--- Log closed Thu Jun 15 01:48:52 2017
--- Log opened Thu Jun 15 01:49:02 2017
-!- Irssi: #agda: Total of 119 nicks [0 ops, 0 halfops, 0 voices, 119 normal]15/06 01:49
-!- Irssi: Join to #agda was synced in 424 secs15/06 01:56
mietekI wish {-# REWRITE ... #-} rules respected module scoping15/06 12:51
* mietek but… this is hard? https://github.com/agda/agda/issues/233515/06 12:51
arjen-jonathanHi all15/06 15:47
arjen-jonathanAgain I got Agda looping; again by splitting 2 mutually defined functions over 2 modules.15/06 16:05
arjen-jonathanIt terminated previously when they were defined together in one module.15/06 16:05
dolioI'm surprised it's even possible to do that.15/06 16:08
mietekme too15/06 16:13
arjen-jonathanWell, you have to use {-# NO_TERMINATION_CHECK #-}15/06 16:15
arjen-jonathanUgh {-# NON_TERMINATING #-} tbp15/06 16:15
arjen-jonathanHmm, there is more weird stuff going on15/06 16:29
dolioI'm still a little surprised that you can write mutually recursive modules, even with those options.15/06 16:33
arjen-jonathanIf I evaluate the expression using C-c C-n, I get some result like:15/06 16:34
arjen-jonathanproj1 x, proj1 (proj2 x)), etc where x is some large product 15/06 16:34
arjen-jonathanInstead of it fully reducing15/06 16:34
arjen-jonathanCan I force that in emacs?15/06 16:34
arjen-jonathanThe modules aren't15/06 16:37
arjen-jonathanI'm making the definitions mutually recursive by making one definition take an argument of type of the second definition15/06 16:38
dolioOh, I see.15/06 16:39
dolioAnd then tying them together later or something?15/06 16:39
arjen-jonathanx : Y -> Z = ... ; y : Y = ... x y ...  15/06 16:41
arjen-jonathanAnd they take other arguments ofc that reduce in size during evaluation.15/06 16:42
arjen-jonathanI think a problem might be that I'm using C-c C-n 15/06 16:42
arjen-jonathanAnd it doesn't fully reduce the result15/06 16:43
arjen-jonathanThat it prints.15/06 16:43
arjen-jonathanCan I force full-evaluation in emacs?15/06 16:43
dolioYeah, okay.15/06 16:46
dolioThere are two C-c C-n type commands, I think. I forget which one C-c C-n is.15/06 16:47
dolioYou can probably try calling them manually with M-x agda-mode-...15/06 16:48
dolioSomething with 'normalize' in the name.15/06 16:48
arjen-jonathanI'm already calling the one with normalize-top-level15/06 16:48
arjen-jonathanThis is super weird15/06 16:56
arjen-jonathanIt doesn't seem to reduce my mutually defined function anymore at all15/06 16:56
arjen-jonathanI've now made it {-# TERMINATING #-}15/06 16:57
arjen-jonathanIt does actually terminate15/06 16:57
arjen-jonathanBut I just a huge projection; from an expression that contains calls to "eval" <- my function15/06 16:58
mietekwhy is there no definition of Category in the stdlib?15/06 17:07
mietekarjen-jonathan: I think you’re asking for trouble15/06 17:07
mietekarjen-jonathan: there are bugs with things that happen between modules15/06 17:07
arjen-jonathanmietek: I think you're right; but now I've re-inlined my function parts into one-module;15/06 17:08
arjen-jonathanAnd I still have the problem that parts are just not reducing15/06 17:08
mietekwell — do you still have module parameters?15/06 17:09
arjen-jonathanYes15/06 17:09
mietekI don’t expect them to reduce15/06 17:09
mietekthey are like buggy postulates15/06 17:09
arjen-jonathanWhy is that?15/06 17:09
arjen-jonathanAh.. that I didn't know15/06 17:09
mietekwell, I may be wrong; this is pure observation15/06 17:09
arjen-jonathanI didn't have too much trouble with them before15/06 17:10
arjen-jonathanAre there open issues about this that you know of?15/06 17:17
arjen-jonathanI looked around ,but nothing stood out to me15/06 17:17
mietekI don’t; I’ve just had poor experiences15/06 17:22
mietekI think I reported some bugs about module parames15/06 17:22
mietekparameters*15/06 17:22
mietekthey may be fixed now15/06 17:22
mietekok, wow15/06 17:28
mietekoops, wrong #15/06 17:28
arjen-jonathanOkay; thanks15/06 17:33

Generated by irclog2html.py 2.7 by Marius Gedminas - find it at mg.pov.lt!