Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

The JS backend generates incorrect code for Agda code that uses reflection #5420

Closed
nad opened this issue May 31, 2021 · 2 comments
Closed
Assignees
Labels
backend: js JavaScript generation backend reflection Elaborator reflection, macros, tactic arguments type: bug Issues and pull requests about actual bugs
Milestone

Comments

@nad
Copy link
Contributor

nad commented May 31, 2021

Consider the following code:

open import Agda.Builtin.IO
open import Agda.Builtin.Reflection
open import Agda.Builtin.String
open import Agda.Builtin.Unit

_>>=_ : {A B : Set}  TC A  (A  TC B)  TC B
_>>=_ = λ x f  bindTC x f

postulate
  putStr : String  IO ⊤

{-# COMPILE JS putStr =
    function (x) {
      return function(cb) {
        process.stdout.write(x); cb(0); }; } #-}

main : IO ⊤
main = putStr "Success\n"

If you compile this using the JS backend and run the code using node, then you get an error message:

[…]/jAgda.Bug.js:9
exports["_>>=_"] = z_jAgda_Agda_Builtin_Reflection["bindTC"](null)(null)(null)(null);
                                                            ^

TypeError: z_jAgda_Agda_Builtin_Reflection.bindTC is not a function
    at Object.<anonymous> ([…]/jAgda.Bug.js:9:61)
    at Module._compile (module.js:652:30)
    at Object.Module._extensions..js (module.js:663:10)
    at Module.load (module.js:565:32)
    at tryModuleLoad (module.js:505:12)
    at Function.Module._load (module.js:497:3)
    at Function.Module.runMain (module.js:693:10)
    at startup (bootstrap_node.js:188:16)
    at bootstrap_node.js:609:3

It should be possible to compile and run code that uses reflection, if reflection primitives are only used on the meta-level.

@nad nad added type: bug Issues and pull requests about actual bugs reflection Elaborator reflection, macros, tactic arguments backend: js JavaScript generation backend labels May 31, 2021
@nad nad added this to the 2.6.3 milestone May 31, 2021
@nad nad changed the title The JS backend fails to compile code that uses reflection The JS backend generates incorrect code for Agda code that uses reflection May 31, 2021
@nad nad self-assigned this May 31, 2021
nad added a commit that referenced this issue May 31, 2021
nad added a commit that referenced this issue Jun 2, 2021
nad added a commit that referenced this issue Jun 2, 2021
@nad nad closed this as completed in 35aa048 Jun 7, 2021
@asr
Copy link
Member

asr commented Jun 7, 2021

What about of cherry-picking the fix into release-2.6.2?

@nad
Copy link
Contributor Author

nad commented Jun 8, 2021

I have no strong opinion on this.

@andreasabel andreasabel modified the milestones: 2.6.3, 2.6.2.1 Aug 18, 2021
@andreasabel andreasabel mentioned this issue Aug 25, 2021
5 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
backend: js JavaScript generation backend reflection Elaborator reflection, macros, tactic arguments type: bug Issues and pull requests about actual bugs
Projects
None yet
Development

No branches or pull requests

3 participants