cduce issueshttps://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues2017-10-16T08:48:07+02:00https://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>
```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/9Polymorphic typing of record operations2022-03-16T16:21:58+01: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/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/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/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/21Unit tests with dune2022-04-04T15:39:03+02: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?Packaginghttps://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues/22Optional dependencies2022-08-22T10:40:24+02: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.Packaginghttps://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" improvementsPackaginghttps://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues/25Issue in apply that makes it not monotone2022-01-30T14:35:33+01:00Mickael LaurentIssue in apply that makes it not monotoneWhen intersecting an arrow type whose dnf contain several conjunctions,
if this intersection makes one of the conjunctions empty, it will not be simplified in the DNF.
Then, using the operator apply on this arrow type will consider the ...When intersecting an arrow type whose dnf contain several conjunctions,
if this intersection makes one of the conjunctions empty, it will not be simplified in the DNF.
Then, using the operator apply on this arrow type will consider the positive part of this empty conjunction and thus it will not yield the expected type but a larger one.
This can be reproduced with the following code:
```ocaml
module CD = Cduce_types
let cup t1 t2 = CD.Types.cup t1 t2
let cap t1 t2 = CD.Types.cap t1 t2
let diff = CD.Types.diff
let cons = CD.Types.cons
let mk_arrow = CD.Types.arrow
let true_typ = CD.Builtin_defs.true_type
let false_typ = CD.Builtin_defs.false_type
let bool_typ = cup true_typ false_typ
let int_typ = CD.Types.Int.any
let any = CD.Types.any
let empty = CD.Types.empty
let any_node = cons any
let empty_node = cons empty
let subtype = CD.Types.subtype
let pp_typ = CD.Types.Print.print_noname
let apply t args =
let t = CD.Types.Arrow.get t in
CD.Types.Arrow.apply t args
let arrow_any = CD.Types.Function.any
let domain t =
if subtype t arrow_any then
let t = CD.Types.Arrow.get t in
CD.Types.Arrow.domain t
else empty
let _ =
let simple_arrow = mk_arrow (cons int_typ) (cons int_typ) in
let test = simple_arrow in
let test = cup test (mk_arrow (cons bool_typ) any_node) in
let test = diff test (mk_arrow any_node any_node) in
let test = cap test (mk_arrow (cons (diff any bool_typ)) any_node) in
Format.printf "%a@." pp_typ test ;
Format.printf "Subtype of %a ? %b@." pp_typ simple_arrow (subtype test simple_arrow) ;
Format.printf "But when we apply an Int to it: %a@." pp_typ (apply test (domain simple_arrow)) ;
```
It has been tested on the branches dune-switch and polymorphic.Kim NguyễnKim Nguyễnhttps://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues/26Weak polymorphism is not unified nor propagated when used in a function2022-02-01T17:00:39+01:00MattiasWeak polymorphism is not unified nor propagated when used in a functionSome examples here:
```ocaml
# let r = ref ([ 'a* ]) [];;
val r : { get=[ ] -> [ '_weak0* ] set=[ '_weak0* ] -> [ ] } = { get=<fun>
# let f (x : Int) : Int = r := [ x ]; x + 1;;
val f : Int -> Int = <fun>
# r;;
- : { get=[ ] -> [ '_...Some examples here:
```ocaml
# let r = ref ([ 'a* ]) [];;
val r : { get=[ ] -> [ '_weak0* ] set=[ '_weak0* ] -> [ ] } = { get=<fun>
# let f (x : Int) : Int = r := [ x ]; x + 1;;
val f : Int -> Int = <fun>
# r;;
- : { get=[ ] -> [ '_weak0* ] set=[ '_weak0* ] -> [ ] } = { get=<fun>
set=<fun> }
```
```ocaml
# let g (x : 'a) : 'a = r := [ x ]; x;;
val g : 'a -> 'a = <fun>
# g 3;;
- : 3 = 3
# g;;
- : 'a -> 'a = <fun>
# r;;
- : { get=[ ] -> [ '_weak0* ] set=[ '_weak0* ] -> [ ] } = { get=<fun>
set=<fun> }
```Kim NguyễnKim Nguyễnhttps://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues/27Wrong explanation for the merge of the two records2022-03-16T17:18:12+01:00Giuseppe CastagnaWrong explanation for the merge of the two recordsThe current explanation for the merge is not correct:
```
val merge : t -> t -> t
(** [merge t1 t2] discards the non record component of [t1] and [t2] and
returns the type of the [+] operators on records, that is, returns a record...The current explanation for the merge is not correct:
```
val merge : t -> t -> t
(** [merge t1 t2] discards the non record component of [t1] and [t2] and
returns the type of the [+] operators on records, that is, returns a record
type [t] where the type of label [l] is the one of [t2] if it is present in
[t2] and the type of [t1] otherwise.
*)
```
Actually, this does not cover when l is optional in t1. If this is the case then it is the union of the two types
Formally
(t1 + t2)[l] = (t1[l]\undef)|t2[l] for undef < t1[l]https://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues/30RFC: Documentation and website2022-05-02T16:33:40+02:00MattiasRFC: Documentation and websiteSo, I may not understand everything but let's try to summarise what I understand.
The way to produce documentation is to produce the website. This will do the following things:
- Compile `site.cdo` from `site.cd`
- Run `site.cdo` on an ...So, I may not understand everything but let's try to summarise what I understand.
The way to produce documentation is to produce the website. This will do the following things:
- Compile `site.cdo` from `site.cd`
- Run `site.cdo` on an xml file
- When my [MR](https://gitlab.math.univ-paris-diderot.fr/cduce/website/-/merge_requests/1) is merged, run `dune build @doc` to generate the api and copy/paste the files in the html directory
## First issue
### Issue
This is done in [cduce/web/dune](https://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/blob/dev/web/dune) and in [website/Makefile](https://gitlab.math.univ-paris-diderot.fr/cduce/website/-/blob/main/Makefile).
- The former (obtained with `dune build @website`) runs `site.cdo` on [cduce/web/doc.xml](https://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/blob/dev/web/doc.xml) and generate the doc in `./_build/default/web/doc`
- The latter (obtained with `make` in the cduce-website directory) runs `site.cdo` on [website/web/index.xml](https://gitlab.math.univ-paris-diderot.fr/cduce/website/-/blob/main/web/index.xml) and generate the doc in `/tmp/public_html.$(LOGNAME)`
### Solution
Let's get rid of `website/web` and generate all the website like my MR generates the API (see https://gitlab.math.univ-paris-diderot.fr/cduce/website/-/blob/cduce_api/Makefile#L10 and https://gitlab.math.univ-paris-diderot.fr/cduce/website/-/blob/cduce_api/Makefile#L25)
What I do here is create a git submodule containing the cduce repository, call `dune build @doc` inside it and copy/paste it to the proper directory (here `/tmp/public_html.$(LOGNAME)`)
### Why is this my preferred solution?
The reason is simple: when someone makes a MR that changes the behaviour of CDuce (by adding new features, deprecating things etc), they can immediately edit the corresponding part of the documentation in the same MR since everything is in the CDuce repository. From the website repository perspective, we just need to update the submodule (that should always link to the `main` branch of CDuce since this is the production branch)
## Second issue
Let's focus on the website part since this is the one that generates [cduce.org](https://www.cduce.org/) hoping it will be merged in the cduce repository and use it as a submodule.
### Issue
The documentation is split between the API (generated with `dune build @doc`) and the rest (generated from all the xml files). This may make it hard for contributions since you need to edit `.mli` files and `.xml` files if you made some breaking changes.
### Solution
This is not an easy task and I honestly don't think it's useful but just to plant a seed and see how it grows.
Some parts of the documentation could be generated from the `.mli` files by extracting some parts of the comments. The thing I like about this is that we can improve the direct documentation (the `.mli` files) by adding examples in it that can be reused for the website.
What I dislike about it, it's not easy to do, it demands some hardwork in `.mli` files for contributions.
Right now, I'd say don't touch this part.
## Third issue
### Issue
If we want to add more html tags we need to update [cduce/web/siteTypes.cd](https://gitlab.math.univ-paris-diderot.fr/cduce/website/-/blob/main/web/siteTypes.cd).
### Solution
I'm not an expert in XML but would we be able to allow the use of `<![CDATA[ valid html ]]>` in XML files?
## Small issues
- `odoc` produces its own css file that hardly fits other website css so maybe we should create our own css file for the generated api (just remember to delete their odoc.css and replace it with our own)
- The website could go through an update (css, google search bar, site map, night mode etc)
- Inline `cduce.js` in the website for the examples (This reminds me of the "protected functions" in CDuce, if someone could create an issue about it)
Discussion is now opened @kn and @beppehttps://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues/31Add optional parameter to the tally function to specify the order to use2022-08-22T10:25:53+02:00Mickael LaurentAdd optional parameter to the tally function to specify the order to useIt could be useful to be able to specify to the tally function which order to use on the type variables, as this order will determine which variables will be expressed as a function of the others (and which ones will remain unchanged).
T...It could be useful to be able to specify to the tally function which order to use on the type variables, as this order will determine which variables will be expressed as a function of the others (and which ones will remain unchanged).
This order should probably be given as a list of type variables in increasing order. Type variables that do not appear in this list should be considered greater (I think?? or maybe smaller) that all the variables present in the list, so that if we give as order to the tally function the list of our monomophic variables in the context of an inference, then these variables will remain unchanged whenever possible (and variables not present in this list will be expressed in function of our monomorphic variables, except when it is not possible, in which case a monomorphic variable will not remain unchanged).https://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues/32Add positive_vars(t) and negative_vars(t) in the Subst API2022-07-30T21:46:47+02:00Mickael LaurentAdd positive_vars(t) and negative_vars(t) in the Subst APIThere is no way in the current Types.Subst API to determine, given a variable v and a type t, whether v appears only in a covariant position in t, contravariant position, or both.
Adding such a function would be useful, or alternatively ...There is no way in the current Types.Subst API to determine, given a variable v and a type t, whether v appears only in a covariant position in t, contravariant position, or both.
Adding such a function would be useful, or alternatively (depending on the performance), a function positive_vars(t) that returns all the variables appearing in a covariant position in t, and negative_vars(t) that returns all the variables appearing in a contravariant position in t.https://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues/33Issue with min_type and max_type2022-08-25T15:57:39+02:00Mickael LaurentIssue with min_type and max_typeThe description of the functions Type.Subst.min_type and Type.Subst.max_type in the doc is wrong:
the largest subtype of any instance of t is NOT t where all positive occurrences of variables are replaced by 𝟘 and all negative occurrence...The description of the functions Type.Subst.min_type and Type.Subst.max_type in the doc is wrong:
the largest subtype of any instance of t is NOT t where all positive occurrences of variables are replaced by 𝟘 and all negative occurrences of variables not in vars are replaced by 𝟙.
Counterexample:
`t = (Any->Any) & 'a | (Int->Int) & ~'a`
min(t) should be `(Any->Any)&(Int->Int)`, but replacing the occurences of 'a as specified would give Empty,
which is a subtype of any instance of t but not the largest.
Moreover, the result of this computation is not preserved by semantic equivalence, as for any `'a` we have `(Int->Int) = (Int->Int) & 'a | (Int->Int) & ~'a` but `min(Int->Int) = Int->Int` and `min((Int->Int) & 'a | (Int->Int) & ~'a) = Empty`. Also, I am not sure Cduce would always simplify the type `(Int->Int) & 'a | (Int->Int) & ~'a` into `(Int->Int)` as it does not simplify the DNF of functions.
The cases where the functions min_type and max_type are not correct is when a variable appears in both a negative and positive occurence, because then the operation of substituting one of the occurence by something and the other by something else is not preserved by semantic equivalence.
I understand that one of the usecase of this function is to implement the min and max for dynamic types, but as dynamic type variables should always be unique (a given dynamic type variable should not appear twice in a type), the function clean_type should be enough to implement it (as a given dynamic type variable can only be positive or negative but not both). If a dynamic type variable "semantically" appears in both covariant and contravariant positions, it is invalid and thus the fact that clean_type will do nothing is not an issue (assuming that Cduce will simplify trivial partitions of the form `t & 'a | t & ~'a` in order to only keep occurences of variables that have a semantic impact, which I don't think is always true when t is a function for instance).
My suggestion is to remove the min_type and max_type functions as the cases where it is correct (when no variable is both in covariant and contravariant position) can easily be handled with clean_type.https://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues/34Add a lowlevel module to pretty print in UTF-8 and color2022-12-09T16:09:24+01:00Kim NguyễnAdd a lowlevel module to pretty print in UTF-8 and colorA module for pretty printing and color should be added. The right place, imho is in cduce-types, that is in :
[types/misc/](https://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/tree/main/types/misc).
Once this module is available it ...A module for pretty printing and color should be added. The right place, imho is in cduce-types, that is in :
[types/misc/](https://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/tree/main/types/misc).
Once this module is available it could be used for :
- pretty-printing of types (with nice type connectives)
- pretty-printing of error messages or warning in color
- pretty-printing of error messages in tools (configure, dtd2cduce, …)Usabilityhttps://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues/35Improve pretty-printing /parsing of types using UTF-8 Symbols2022-09-29T17:37:04+02:00Kim NguyễnImprove pretty-printing /parsing of types using UTF-8 SymbolsIt would be nice if CDuce was able to pretty-print types with UTF-8 connectives. This would depend on #34. Some requirements :
- It needs to be automatically disabled for terminals that don't support UTF-8
- A user must be able to disabl...It would be nice if CDuce was able to pretty-print types with UTF-8 connectives. This would depend on #34. Some requirements :
- It needs to be automatically disabled for terminals that don't support UTF-8
- A user must be able to disable it with a command-line flag
- This should also work for parsing. A rule of thumb to ensure the correct pretty-printing of types is that CDuce should always be able to parse a type it has pretty-printed (such that both types are equivalent).Usabilityhttps://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues/36Review and sanitize the pretty-printing of errors2022-12-09T16:09:24+01:00Kim NguyễnReview and sanitize the pretty-printing of errorsCDuce's internal code base relies heavily on exceptions for error messages. Due to the various places error can occur, exceptions are not always correctly handled when they should. Some examples :
- Lexing/Parsing errors (static)
- Typin...CDuce's internal code base relies heavily on exceptions for error messages. Due to the various places error can occur, exceptions are not always correctly handled when they should. Some examples :
- Lexing/Parsing errors (static)
- Typing errors (static)
- Compilation errors (static but should be an internal failure, since compilation is not supposed to fail)
- CDuce exceptions (exceptions raised by CDuce code on purpose, dynamic)
- OCaml exceptions (exceptions raised by OCaml code on purpose, dynamic, e.g. if a user calls `OCaml.Stdlib.List.hd []`)
- Runtime exceptions (some corner features of CDuce require dynamic checks, such that pattern-matching against a primitive or polymorphic function)
And there are also warnings. And internal exceptions used for control flow that should never be used.
The use of all these exceptions should be surveyed, sanitized and documented. Most exceptions are caught in
[lang/lib/cduce_driver](https://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/blob/main/lang/lib/cduce_driver.ml#L316)
in a way that is not completely satisfactory (and maybe some are not).
This might require cleaning up the handling of locations first which is its own can of worm ([lang/parser/cduce_loc.ml](https://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/blob/main/lang/parser/cduce_loc.ml)).
In particular, it is still polluted by remnants of the HTML output (CDuce could be run as a CGI script for the online toplevel, which has been replaced by the JavaScript back-end that do not require a server-side component).
Once the surveying is done, a more robust error/warning infrastructure can be put in place.Usabilityhttps://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues/40Displaying unhandled exceptions2024-02-29T14:32:16+01:00Tomaz MascarenhasDisplaying unhandled exceptionsUnhandled exceptions are not shown to the user as the corresponding tag of the constructor of `error_t` is replaced by `_`. There is a failing test that shows this.Unhandled exceptions are not shown to the user as the corresponding tag of the constructor of `error_t` is replaced by `_`. There is a failing test that shows this.Refactor of Exceptions