uds-psl/autosubst-ocaml

autosubst-ocaml's Issues

Example combining a functor and binders

As far as I can tell, there are no examples in the gallery that combine both a functor and binding. It would be nice to add such an example (I struggled for a while to find the correct syntax to get it accepted by the parser).

My use case is a constructor for pairs, with an optional annotation (option functor) for the codomain, which binds a position:

tPair : term -> (bind term in "option" (term)) -> term -> term ->term

Opam package erroring due to wrong file location

I have just been trying to use the opam package, but when trying to build a simple example, I get the following error:

Fatal error: exception Sys_error("/home/meven/.opam/autosubst-ocaml/share/autosubst/fintype.v: No such file or directory")
Raised by primitive operation at Stdlib.open_in_gen in file "stdlib.ml", line 398, characters 28-54
Called from Stdlib.open_in_bin in file "stdlib.ml" (inlined), line 406, characters 2-47
Called from Autosubst_lib__Program.read_file in file "lib/program.ml", line 74, characters 14-32
Called from Autosubst_lib__Program.copy_file in file "lib/program.ml" (inlined), line 102, characters 33-48
Called from Autosubst_lib__Program.gen_static_files.copy_static_file in file "lib/program.ml", line 130, characters 4-74
Called from Autosubst_lib__Program.gen_static_files in file "lib/program.ml", line 134, characters 20-48
Called from Autosubst_lib__Program.main in file "lib/program.ml", line 177, characters 9-75
Called from Stdlib__result.map in file "result.ml", line 25, characters 32-37
Called from Monadic__Result.MakeT.ResultMonad.bind in file "monadic/library/result.ml", line 31, characters 24-33
Called from Stdlib__result.map in file "result.ml", line 25, characters 32-37
Called from Monadic__Result.MakeT.ResultMonad.bind in file "monadic/library/result.ml", line 31, characters 24-33
Called from Dune__exe__Main.main in file "bin/main.ml", line 6, characters 12-35
Called from Dune__exe__Main in file "bin/main.ml", line 10, characters 9-16

It seems like the culprit is this line, which hardcodes that the files are to be found in the share/subst folder, while the opam installation puts them in share/coq-autosubst-ocaml.

Compilation error with successive binders

The .v file generated by autosubst on a signature file with multiple binders in a single item seems to go wrong when used with the option -allfv.

Example signature file (bug.sig):

term : Type

F : (bind term, term in term) -> term

Autosubst called with:

$ autosubst -s ucoq -v ge813 -allfv bug.sig -o Ast.v

The problem lie in the functions allfvRenL_term and allfvRenR_term in the generated Ast.v. The bug seems easy to fix (add additional helper functions similar to the ones already generated, see full repro attached).
repro.zip