Ajout du parsing de type de fonction polymorph.
Merge request reports
Activity
added 1 commit
- 273a9c3f - Move a test from sat to unknown it shouldn't have been in sat
enabled an automatic merge when the pipeline for 273a9c3f succeeds
@kanig it should fix in a satisfying way #17 (closed) . The branch in why3 has been updated.
Thanks! Currently it doesn't compile in our setup though. One reason is the use of
dprintf(recall that we use ocaml 4.07.1, which can be easily fixed, but there are other errors (one possible a cascading error?):_File "parser.ml", line 9, characters 7-8: _Error: Multiple definition of the type name t. _ Names must be unique in a given structure or signature.and
_File "dolmen/src/loop/typer.ml", line 192, characters 6-34: _Error: This pattern matches values of type Dolmen_std.Term.t T.warn _ but a pattern was expected which matches values of type _ $Warning_'a T.warn _ Type Dolmen_std.Term.t is not compatible with type $Warning_'aMaybe the first error is related to menhir version, we use
menhir, version 20181113. I will look more into this.Edited by Johannes KanigI was able to remove the first error by using the commented include in
parser.mlinstead, but I still have the second error and don't know how to solve it ... It could actually be related to how I replaced dprintf - I replaced it by functions of the form(fun fmt -> Format.fprintf fmt ...). Maybe that breaks typing.Edited by Johannes KanigLast comment - when removing some of the offending code just to make colibri compile, I can confirm that #17 (closed) is proved now. So this looks like a very good way forward indeed!
added 1 commit
- f6597dc6 - Import from Bin:a1af7a0 Src:242d6cf6a farith:a93db57
Hello François, I confirm that this version compiles here, and with the changes in Why3, this solves #17 (closed). Thanks! So this can go into the master branch I think?
Edited by Johannes Kanigmentioned in issue #17 (closed)
mentioned in commit 1bcd2375
