Apostolis Xekoukoulotakis
2018-09-26 02:51:48 UTC
According to this (1) , let statements that are to be executed in a
specific case branch, could be placed before the case term in the treeless
representation . This is harmless in lazy evaluation, but it can cause
infinite loops in eager evaluation.
Is this still the case? (I am trying at the moment to move all let
statements to their correct place.(2))
1 :
https://gitlab.com/janmasrovira/agda2mlf/blob/master/presentation/report.org
2 :
https://github.com/xekoukou/agda-ocaml/commit/4559af202dc5f8b864ce67087790eb526c1c5672
specific case branch, could be placed before the case term in the treeless
representation . This is harmless in lazy evaluation, but it can cause
infinite loops in eager evaluation.
Is this still the case? (I am trying at the moment to move all let
statements to their correct place.(2))
1 :
https://gitlab.com/janmasrovira/agda2mlf/blob/master/presentation/report.org
2 :
https://github.com/xekoukou/agda-ocaml/commit/4559af202dc5f8b864ce67087790eb526c1c5672