cduce merge requestshttps://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/merge_requests2024-03-20T00:23:59+01:00https://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/merge_requests/29Tentative fix for the soundness bug in the subtyping algorithm.2024-03-20T00:23:59+01:00Kim NguyễnTentative fix for the soundness bug in the subtyping algorithm.Tentative fix for Issue #37.
Witnesses used to check the non-emptyness of a type are extended
with "polymorphic witnesses".
A polymorphic witness is a triple of a set of positive variable,
a set of negative variables and a plain (monomo...Tentative fix for Issue #37.
Witnesses used to check the non-emptyness of a type are extended
with "polymorphic witnesses".
A polymorphic witness is a triple of a set of positive variable,
a set of negative variables and a plain (monomorphic witness).
Recall that a witness for Any is e.g. 0 (that is,
since Any = Int | Char | ... , then when a witness for Any is
needed, an inhabitant of Int is choosen first and in particular 0).
We used to also return 0 for the type 'a (by wrongly applying the
algorithm of the ICFP'11 Paper which discards toplevel variables).
Here, we return a witness ('a&0). Now, when we check, e.g.
if 'a&0 belongs to Int\'a, we answer no (while previously we
would answer that 0 belongs to Int).
This seems to fix the problem. This commit also adds a file to host
new tests specifically for subtyping.https://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/merge_requests/28Tidy-up the CI script.2024-03-19T10:13:41+01:00Kim NguyễnTidy-up the CI script.Work-around the insanity of gitlab's artifact vs. cache and handle
our own caching that works with ssh and stays on the host.Work-around the insanity of gitlab's artifact vs. cache and handle
our own caching that works with ssh and stays on the host.https://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/merge_requests/27Refactor of Exceptions2024-03-15T20:11:51+01:00Tomaz MascarenhasRefactor of ExceptionsCentralizing the definition of all exceptions in `Cduce_core` in a single module `lang/lib/cduce_error.ml`, packed as the new type `error_t` together with the location where the exception occurred.Centralizing the definition of all exceptions in `Cduce_core` in a single module `lang/lib/cduce_error.ml`, packed as the new type `error_t` together with the location where the exception occurred.Refactor of ExceptionsTomaz MascarenhasTomaz Mascarenhashttps://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/merge_requests/26Replace `num` library by `zarith`2024-01-26T14:15:43+01:00Tomaz MascarenhasReplace `num` library by `zarith`This MR replaces the usage of `num` as a big integer library by `zarith`. It also adds a new test that checks big int manipulation in CDuce.
Related issue: !26.This MR replaces the usage of `num` as a big integer library by `zarith`. It also adds a new test that checks big int manipulation in CDuce.
Related issue: !26.Tomaz MascarenhasTomaz Mascarenhashttps://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/merge_requests/25Fix `sed` on MacOS and remove --pin and updates on CI2024-01-19T16:56:30+01:00Tomaz MascarenhasFix `sed` on MacOS and remove --pin and updates on CIThis MR implements 5 changes:
- Fix usage of `sed` on MacOS in the script `tools/init_opam_switch.sh`. It is necessary to add the flag `-E` to support [extended](https://en.wikibooks.org/wiki/Regular_Expressions/POSIX-Extended_Regular_E...This MR implements 5 changes:
- Fix usage of `sed` on MacOS in the script `tools/init_opam_switch.sh`. It is necessary to add the flag `-E` to support [extended](https://en.wikibooks.org/wiki/Regular_Expressions/POSIX-Extended_Regular_Expressions) regular expressions and to use pipes without escape. This MR is adding variables to consider this depending on the operating system. Another solution would be to restrict ourselves to [basic](https://en.wikibooks.org/wiki/Regular_Expressions/Basic_Regular_Expressions) regular expressions in `sed` commands, which might keep the script more readable.
- Finish removing support for `--pin`. This feature exists on the main branch but seems to be disabled on dev. This MR is removing one last snippet that is related to it.
- Add conditions for running the Windows pipeline on CI. It will only run if one of the following conditions are met:
+ The name of the branch receiving a push ends with `for-windows-ci`.
+ The push is on a branch with an MR open either to `dev` or to `main`.
- Remove `_nojs` from CI for 5.0.0.
- Add CI pipeline for OCaml 5.1.0. We are using `_nojs` here since compiling cduce-js with 5.1.0 results in the following warning:
```plaintext
There are some missing primitives
Dummy implementations (raising 'Failure' exception) will be used if they are not available at runtime.
You can prevent the generation of dummy implementations with the commandline option '--disable genprim'
Missing primitives:
length_nat
```Tomaz MascarenhasTomaz Mascarenhashttps://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/merge_requests/24Remove support for OCaml version 4.07.1 and older2024-01-05T14:24:06+01:00Tomaz MascarenhasRemove support for OCaml version 4.07.1 and olderThis merge request removes support for compiling with OCaml version 4.07.1 or older. It also adds constraints in the `dune-project` file to prevent the user from using `opam install` without having the correct version of the compiler.
R...This merge request removes support for compiling with OCaml version 4.07.1 or older. It also adds constraints in the `dune-project` file to prevent the user from using `opam install` without having the correct version of the compiler.
Related issue: #38.Tomaz MascarenhasTomaz Mascarenhashttps://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/merge_requests/23Test tallying2023-03-30T14:37:35+02:00Kim NguyễnTest tallyingAdd a function to test if a tallying solution exists without computing all solutions. Also removes some undocumented and unused functions from the API.Add a function to test if a tallying solution exists without computing all solutions. Also removes some undocumented and unused functions from the API.https://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/merge_requests/22CI Improvements and OCaml 5.0.0 compatibility2023-01-14T08:55:14+01:00Kim NguyễnCI Improvements and OCaml 5.0.0 compatibilityThis MR serves several purposes:
- it improves slightly the CI speed by locally caching builds between CI jobs
- it replaces the OCaml 4.14.0 docker image with OCaml 4.14.1
- it replaces the unofficial 4.12.0+domains image (multicore pre...This MR serves several purposes:
- it improves slightly the CI speed by locally caching builds between CI jobs
- it replaces the OCaml 4.14.0 docker image with OCaml 4.14.1
- it replaces the unofficial 4.12.0+domains image (multicore preview) with 5.0.0
- while doing so, it fixes some compatibility problems with 5.0.0
The compatibility problems solved with 5.0.0 are:
- update the OCaml/CDuce interface to the new way OCaml's setup its load paths
- remove references in the OCaml/CDuce interface to 'unsafe strings' (mutable strings) since
these where removed after being deprecated
- make the pretty-printing not subtly depend on a probabilistic data structure, which changed
the output of types when OCaml's PRNG changed (as it did with OCaml 5.0.0).https://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/merge_requests/21Several improvements to types, subtyping and tallying.2023-01-13T14:21:05+01:00Kim NguyễnSeveral improvements to types, subtyping and tallying.This MR improves several aspects of the tallying, subtyping and variable-aware BDD structure, yielding speed improvements in tallying intensive code.This MR improves several aspects of the tallying, subtyping and variable-aware BDD structure, yielding speed improvements in tallying intensive code.https://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/merge_requests/20Compatibility with OCaml 4.072022-12-12T15:24:29+01:00MattiasCompatibility with OCaml 4.07Semantic tags were not handled in this versionSemantic tags were not handled in this versionhttps://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/merge_requests/19Deleted the website from the cduce repo2022-12-09T16:12:56+01:00MattiasDeleted the website from the cduce repoThe website is compiled entirely from the website repo and only depends on cduce to build the files and the api documentation (when available)The website is compiled entirely from the website repo and only depends on cduce to build the files and the api documentation (when available)https://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/merge_requests/18Improve performances of type substitutions.2022-09-30T22:58:39+02:00Kim NguyễnImprove performances of type substitutions.This patch improves the performances of type substitutions and of operations
that needs to translate types back to a syntactic equations. Several
improvements are made:
- Internally, a GADT is used instead of polymorphic variants to
...This patch improves the performances of type substitutions and of operations
that needs to translate types back to a syntactic equations. Several
improvements are made:
- Internally, a GADT is used instead of polymorphic variants to
represent recursive type equations. It helped remove a few
inconsistencies and will allow further optimizations.
- Recursive equations are hashconsed, improving sharing of common
subtrees in the type. This impacts the test suite as it may change
the pretty printing of types with shared subtrees as well as the
order of some unioned elements.
- Specifically for type substitutions, when the variables of a subtree
in the types are disjoints from the domain of the substitution, do
not recurse into it.Kim NguyễnKim Nguyễnhttps://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/merge_requests/17Implement custom order for tallying.2022-09-30T21:43:51+02:00Kim NguyễnImplement custom order for tallying.This commit does three things :
- Add the possibility to pass a custom order (given as an ordered
list of variables) to the tallying procedure.
Whenever a constraint s < a < t is added to a constraint set, we add
s < a < any and ...This commit does three things :
- Add the possibility to pass a custom order (given as an ordered
list of variables) to the tallying procedure.
Whenever a constraint s < a < t is added to a constraint set, we add
s < a < any and empty < a < t in sequence, checking whether s
(resp. t) is a positive or negative variable. If s is a variable b,
then it is checked against a with the custom order to add one of :
~b < a < any or b < a < any (if a is a smaller variable than b) or
empty < b < a or ~a < b < any (if a is a larger variable than b)
Constraint sets are maps from variables to (inf, sup) bounds, using
the custom order as ordering, so when traversing a constraint set,
variables are chosen in increasing order of the custom variable
ordering.
- One can now use the syntax:
```
debug tallying ([ 'a 'c 'b ] [ 'd'] [ ('a -> 'c, 'd -> 'b) ]);;
```
to pass the custom order in the toplevel for the debug tallying
directive. the version without the order is still accepted.
- Fix the tallying of record types. The tallying of record types was
erroneously dropping some constraints too early declaring the
whole constraint set unsatisfiable.https://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/merge_requests/16Remove usage of the now deprecated Stream module.2022-12-12T14:34:41+01:00Kim NguyễnRemove usage of the now deprecated Stream module.We replace it with a char Seq.t in the parser or event Seq.t in the
XMLSchema validator. We only use functions that are in OCaml 4.07.We replace it with a char Seq.t in the parser or event Seq.t in the
XMLSchema validator. We only use functions that are in OCaml 4.07.https://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/merge_requests/15Whole code base formatting2022-09-30T15:49:48+02:00Kim NguyễnWhole code base formattingThis MR is split into two commits.
- [the first one](008ca31b3f13a68349b5481b8f224e20a2006e50) fixes a few options in `.ocamlformat` and fixes the version number.
- [the second one](a4894ded33f78fd5b8830e77e274e09a18d1a380) reformats th...This MR is split into two commits.
- [the first one](008ca31b3f13a68349b5481b8f224e20a2006e50) fixes a few options in `.ocamlformat` and fixes the version number.
- [the second one](a4894ded33f78fd5b8830e77e274e09a18d1a380) reformats the whole code base using `dune build @fmt --auto-promote` using these options.Kim NguyễnKim Nguyễnhttps://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/merge_requests/14Pretty printing of some symbols2022-12-09T19:03:16+01:00MattiasPretty printing of some symbols@kn This is an early work in progress to make sure that's the kind of thing you wanted to fix #35@kn This is an early work in progress to make sure that's the kind of thing you wanted to fix #35Usabilityhttps://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/merge_requests/13Draft: Proper handling of semantic tags for ansi terminals2022-12-09T16:13:27+01:00MattiasDraft: Proper handling of semantic tags for ansi terminalsLook at ansiTerminal.mli for details about how to useLook at ansiTerminal.mli for details about how to useUsabilityhttps://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/merge_requests/12Parameterize the tallying algorithm and datastructre with a custom order.2022-09-30T22:58:39+02:00Kim NguyễnParameterize the tallying algorithm and datastructre with a custom order.The tallying algorithm is put in a functor and parameterized by custom ordering for type variables.The tallying algorithm is put in a functor and parameterized by custom ordering for type variables.Kim NguyễnKim Nguyễnhttps://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/merge_requests/11Updated all the .xml and .cd files2022-12-09T16:13:01+01:00MattiasUpdated all the .xml and .cd filesThese files are the ones that were present in the website repo. Since they don't exist anymore in this repository, we took the most up to date ones for the cduce/web repo
@kn If you can take a look at `make @website`, it's raising a war...These files are the ones that were present in the website repo. Since they don't exist anymore in this repository, we took the most up to date ones for the cduce/web repo
@kn If you can take a look at `make @website`, it's raising a warning:
```
File "site.cd", line 427, characters 5-2453:
Warning: The capture variable right is declared in the pattern but not used in the body of this branch. It might be a misspelled or undeclared type or name (if it isn't, use _ instead).
```https://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/merge_requests/10Update the cduce repo to contain a Makefile and up to date files to create th...2022-05-02T15:55:02+02:00MattiasUpdate the cduce repo to contain a Makefile and up to date files to create the website@kn If you can take a look at `make @website`, it's raising a warning:
```
File "site.cd", line 427, characters 5-2453:
Warning: The capture variable right is declared in the pattern but not used in the body of this branch. It might be ...@kn If you can take a look at `make @website`, it's raising a warning:
```
File "site.cd", line 427, characters 5-2453:
Warning: The capture variable right is declared in the pattern but not used in the body of this branch. It might be a misspelled or undeclared type or name (if it isn't, use _ instead).
```