cduce issueshttps://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues2022-01-17T16:54:50+01:00https://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues/24Packaging2022-01-17T16:54:50+01:00MattiasPackagingWhen we're happy with everything, let's have cduce as an opam package, a debian package too and other distros.
I think this will be the first milestone before going further with more "algorithmic" improvementsWhen we're happy with everything, let's have cduce as an opam package, a debian package too and other distros.
I think this will be the first milestone before going further with more "algorithmic" improvementsPackagingMattiasMattiashttps://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues/23Automatic deployment of API documentation2022-01-19T19:15:22+01:00MattiasAutomatic deployment of API documentationIdeally we would like to have two different things:
- Automatic deployment of the API documentation in the project gitlab page (with https://docs.gitlab.com/ee/user/project/pages/)
- Being able to access the documentation of cduce when i...Ideally we would like to have two different things:
- Automatic deployment of the API documentation in the project gitlab page (with https://docs.gitlab.com/ee/user/project/pages/)
- Being able to access the documentation of cduce when installed through opam with [odig](https://erratique.ch/software/odig)PackagingMattiasMattiashttps://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues/22Optional dependencies2022-01-17T16:55:49+01:00MattiasOptional dependenciesOptional dependencies are handled in the libraries stanza of dune files by providing either an empty file if the dependency does not exist or providing the proper file if it does (see https://gitlab.math.univ-paris-diderot.fr/cduce/cduce...Optional dependencies are handled in the libraries stanza of dune files by providing either an empty file if the dependency does not exist or providing the proper file if it does (see https://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/blob/polymorphic/backend/native/dune for example).
Let's see what are other possibilities.PackagingMattiasMattiashttps://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues/21Unit tests with dune2022-01-17T16:56:03+01:00MattiasUnit tests with duneTests are currently done from a generated dune file (see https://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/blob/polymorphic/tests/full/good/dune.auto for example)
Is there a better way of doing it?Tests are currently done from a generated dune file (see https://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/blob/polymorphic/tests/full/good/dune.auto for example)
Is there a better way of doing it?PackagingMattiasMattiashttps://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues/17Unsoundness with record typing2021-05-02T10:41:43+02:00Tommaso PetruccianiUnsoundness with record typingFunctions on records can be given unsound types as in the following:
# let f = fun ({..} -> 'a) x -> x;;
val f : Record -> 'a = <fun>
# f {};;
- : 'a = { }
It seems that this `'a` cannot be instantiated:
# (f {}) + 1;;
Characte...Functions on records can be given unsound types as in the following:
# let f = fun ({..} -> 'a) x -> x;;
val f : Record -> 'a = <fun>
# f {};;
- : 'a = { }
It seems that this `'a` cannot be instantiated:
# (f {}) + 1;;
Characters 1-5:
This expression should have type:
!float | { .. } | Int
but its inferred type is:
'a
which is not a subtype, as shown by the sample:
Atom & 'a
However, here it becomes unsound:
# f (f {});;
- : Empty = { }
Typing of field removal is also unsound:
# let g = fun ({a=Int;b=Bool;..}&'a -> {b=Bool;..}&'a) x -> x\a;;
val g : { a=Int b=Bool .. } & 'a -> { b=Bool .. } & 'a = <fun>
# g {a=2;b=`true};;
- : { a=2 b=`true } = { b=true }
# (g {a=2;b=`true}).a;;
- : 2 = true
# (g {a=2;b=`true}).b;;
- : `true = true
# (g {a=2;b=`true}).a + 2;;
File "runtime/value.ml", line 873, characters 9-15: Assertion failedKim NguyễnKim Nguyễnhttps://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues/16Pretty printing of arrow type could be simplified2017-10-16T08:48:07+02:00Kim NguyễnPretty printing of arrow type could be simplifiedArrows of the form A -> B & A -> C could be printed as a single arrow A -> B|CArrows of the form A -> B & A -> C could be printed as a single arrow A -> B|CKim NguyễnKim Nguyễnhttps://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues/12Solving type equation with recursive types for a variable 'a does not work wh...2017-10-16T08:48:07+02:00Kim NguyễnSolving type equation with recursive types for a variable 'a does not work when 'a occurs below a union/intersection/negationThe problem is in decompose and solve_rectype in Types. The Positive module giving the least fix point solution of a system of equation (aka Courcelle) does not work when variable occurs below type connective.
See for instance:
```
...The problem is in decompose and solve_rectype in Types. The Positive module giving the least fix point solution of a system of equation (aka Courcelle) does not work when variable occurs below type connective.
See for instance:
```
debug tallying [] [ (Int, 'a),'b ; 'b, 'a ] ;;
```
Kim NguyễnKim Nguyễnhttps://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues/9Polymorphic typing of record operations2017-10-16T08:48:07+02:00Kim NguyễnPolymorphic typing of record operationsHow to type the operations on records, concatenation e1 + e2 and field suppression e\ l in the presence of polymorphic variables. For the time being we do a safe but gross approximation. For instance
```
'a & r \ l = r \ l
```
Can ...How to type the operations on records, concatenation e1 + e2 and field suppression e\ l in the presence of polymorphic variables. For the time being we do a safe but gross approximation. For instance
```
'a & r \ l = r \ l
```
Can we do better?
https://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues/6Git subtree merge needed2017-10-16T08:48:07+02:00Kim NguyễnGit subtree merge neededSince the migration to Git the _website_ and cduce are in two distinct repositories. As a consequence the documentation that is in cduce/web and that is distributed with the language is no longer in synchro with the one one the website, ...Since the migration to Git the _website_ and cduce are in two distinct repositories. As a consequence the documentation that is in cduce/web and that is distributed with the language is no longer in synchro with the one one the website, which is the one up-to-date.
Solution: partially reorganize the files so that the directories manual tutorial examples img are directly taken by a subtree merge from the website gitGiuseppe CastagnaGiuseppe Castagnahttps://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues/4Fix pretty printing of Top types2017-10-16T08:48:07+02:00Kim NguyễnFix pretty printing of Top types```
# let max (x: 'a) (y: 'a): 'a = if ( x >> y) then x else y;;
val max : 'a -> 'a -> 'a = <fun>
# max (42 : Int);;
- : (('a \ (Int)) | Int) -> (('a \ (Int)) | Int) = <fun>
# max (42 : 42|AnyXml|Atom|Arrow);;
- : (('a \ ((Arrow | ...```
# let max (x: 'a) (y: 'a): 'a = if ( x >> y) then x else y;;
val max : 'a -> 'a -> 'a = <fun>
# max (42 : Int);;
- : (('a \ (Int)) | Int) -> (('a \ (Int)) | Int) = <fun>
# max (42 : 42|AnyXml|Atom|Arrow);;
- : (('a \ ((Arrow | Atom))) | (Arrow | AnyXml | Atom | 42)) -> (('a \ (
(Arrow |
Atom))) |
(Arrow |
AnyXml |
Atom | 42)) = <fun>
# max (42 : 42|AnyXml|Atom);;
- : (('a \ (Atom)) | (AnyXml | Atom | 42)) -> (('a \ (Atom)) |
(AnyXml | Atom | 42)) = <fun>
```