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

type equality from Elpi to Elpi_parser #277

Closed
cb-wells opened this issue Oct 27, 2024 · 4 comments
Closed

type equality from Elpi to Elpi_parser #277

cb-wells opened this issue Oct 27, 2024 · 4 comments

Comments

@cb-wells
Copy link

Hello, thanks for this great project. Much of the setup is new to me, so this issue might have a simple resolution. I’m trying to add a new REPL command that iterates through the declarations of a parsed program.

List.iter (fun (d : Ast.Program.decl) -> … [[some printing]] … ) p;

But it doesn’t seem to recognize the type equality:
“p has type API.Ast.program, but expected type Ast.Program.decl list”

I assume this is because API is in Elpi, while Ast is in Elpi_parser; somehow the equality is not working across packages. I could clone and build the whole project with my own; but there is probably a simpler solution. Any help is appreciated.

@cb-wells
Copy link
Author

A small test program compiles with dune, with (libraries elpi elpi.parser). This links the modules to the program, but not to each other: within API.ml, there is the error “unbound module Elpi_parser”; and the equality “type program = Ast.Program.t” has a similar error. So, I assume this is probably an issue with the dune build.

Please let me know if I should provide more information. Thank you.

@gares
Copy link
Contributor

gares commented Oct 30, 2024

Hello, there is no API for that. What I suggest is that you temporarily remove the private_modules directive in src/dune then edit src/elpi.ml so to expose all modules in Internal and finally use Elpi.Internal.Whatever you like.

You could also give me a pointer to your code so that I see exactly what you need.

@gares
Copy link
Contributor

gares commented Nov 22, 2024

private_modules directive was removed in #269

@gares gares closed this as completed Nov 22, 2024
@cb-wells
Copy link
Author

Apologies for not replying. Your suggestion worked. Thank you for the help.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants