cduce issueshttps://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues2024-03-20T00:24:15+01:00https://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues/37Unsoundness in polymorphic subtying2024-03-20T00:24:15+01:00Kim NguyễnUnsoundness in polymorphic subtyingCDuce says that the following simingly equal types are not equivalent (while they should be). Computing their differences yields a bogus type `[ Empty]` (which should never be printed, since it is empty).
The problem is twofold:
- I thi...CDuce says that the following simingly equal types are not equivalent (while they should be). Computing their differences yields a bogus type `[ Empty]` (which should never be printed, since it is empty).
The problem is twofold:
- I think the pretty-printer is wrong and `[Empty]` is not displaying some variables that should be there (it appended before)
- If the type really are equivalent (and not wrongly displayed as equivalent) then a bug lurks in the subtyping.
```
SIMPLIFY ERROR
[ [ ('7M_9 & '8M_10) '7M_9* ] '7M_9* ]
[ [ ('7M_9 & '8M_10) '7M_9* ] '7M_9* ]
Initial type:
=========
<types = [ [ ('7M_9 & '8M_10) '7M_9* ] '7M_9* ]
ints(F)
atoms(F)
chars(F)
abstract(F)
times((X458,X46)(+(X919,X46)(F,F,-(X960,X958)(T,F,F)),F,F))
xml(F)
record(F)
arrow(F)
absent=false>
X458=<types = Any \ [ ]
ints(T)
atoms(Cofinite[(->Finite[[ ]])])
chars(T)
abstract(T)
times(T)
xml(T)
record(T)
arrow(T)
absent=false>
X958=<types = [ '7M_9* ]
ints(F)
atoms(Finite[(->Finite[[ ]])])
chars(F)
abstract(F)
times((X959,X958)(T,F,F))
xml(F)
record(F)
arrow(F)
absent=false>
X46=ANY
X919=<types = Any \ (Any \ '7M_9 | '8M_10,Any)
ints(T)
atoms(T)
chars(T)
abstract(T)
times((X910,X46)(F,F,T))
xml(T)
record(T)
arrow(T)
absent=false>
X960=<types = [ '7M_9* ]
ints(F)
atoms(Finite[(->Finite[[ ]])])
chars(F)
abstract(F)
times((X961,X960)(T,F,F))
xml(F)
record(F)
arrow(F)
absent=false>
X910=<types = Any \ '7M_9 | '8M_10
ints(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
atoms(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
chars(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
abstract(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
times(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
xml(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
record(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
arrow(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
absent=false>
X961=<types = '7M_9
ints(VAR(9,7M,`user)(T,F,F))
atoms(VAR(9,7M,`user)(T,F,F))
chars(VAR(9,7M,`user)(T,F,F))
abstract(VAR(9,7M,`user)(T,F,F))
times(VAR(9,7M,`user)(T,F,F))
xml(VAR(9,7M,`user)(T,F,F))
record(VAR(9,7M,`user)(T,F,F))
arrow(VAR(9,7M,`user)(T,F,F))
absent=false>
X959=<types = '7M_9
ints(VAR(9,7M,`user)(T,F,F))
atoms(VAR(9,7M,`user)(T,F,F))
chars(VAR(9,7M,`user)(T,F,F))
abstract(VAR(9,7M,`user)(T,F,F))
times(VAR(9,7M,`user)(T,F,F))
xml(VAR(9,7M,`user)(T,F,F))
record(VAR(9,7M,`user)(T,F,F))
arrow(VAR(9,7M,`user)(T,F,F))
absent=false>Simplified type:
=========
<types = [ [ ('7M_9 & '8M_10) '7M_9* ] '7M_9* ]
ints(F)
atoms(F)
chars(F)
abstract(F)
times((X1148,X1147)(F,F,-(X1152,X1150)(+(X1154,X1147)(T,F,F),F,F)))
xml(F)
record(F)
arrow(F)
absent=false>
X1154=<types = Any \ [ ]
ints(T)
atoms(Cofinite[(->Finite[[ ]])])
chars(T)
abstract(T)
times(T)
xml(T)
record(T)
arrow(T)
absent=false>
X1148=<types = Any \ (Any \ '7M_9 | '8M_10,Any)
ints(T)
atoms(T)
chars(T)
abstract(T)
times((X1149,X1147)(F,F,T))
xml(T)
record(T)
arrow(T)
absent=false>
X1147=ANY
X1152=<types = [ '7M_9* ]
ints(F)
atoms(Finite[(->Finite[[ ]])])
chars(F)
abstract(F)
times((X1153,X1152)(T,F,F))
xml(F)
record(F)
arrow(F)
absent=false>
X1150=<types = [ '7M_9* ]
ints(F)
atoms(Finite[(->Finite[[ ]])])
chars(F)
abstract(F)
times((X1151,X1150)(T,F,F))
xml(F)
record(F)
arrow(F)
absent=false>
X1149=<types = Any \ '7M_9 | '8M_10
ints(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
atoms(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
chars(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
abstract(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
times(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
xml(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
record(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
arrow(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
absent=false>
X1153=<types = '7M_9
ints(VAR(9,7M,`user)(T,F,F))
atoms(VAR(9,7M,`user)(T,F,F))
chars(VAR(9,7M,`user)(T,F,F))
abstract(VAR(9,7M,`user)(T,F,F))
times(VAR(9,7M,`user)(T,F,F))
xml(VAR(9,7M,`user)(T,F,F))
record(VAR(9,7M,`user)(T,F,F))
arrow(VAR(9,7M,`user)(T,F,F))
absent=false>
X1151=<types = '7M_9
ints(VAR(9,7M,`user)(T,F,F))
atoms(VAR(9,7M,`user)(T,F,F))
chars(VAR(9,7M,`user)(T,F,F))
abstract(VAR(9,7M,`user)(T,F,F))
times(VAR(9,7M,`user)(T,F,F))
xml(VAR(9,7M,`user)(T,F,F))
record(VAR(9,7M,`user)(T,F,F))
arrow(VAR(9,7M,`user)(T,F,F))
absent=false>
========
======== Simp\Initial (false):
@<types = [ Empty ]
ints(F)
atoms(F)
chars(F)
abstract(F)
times((X458,X46)(+(X919,X46)(+(X1148,X1147)(F,F,
-(X1152,X1150)(+(X1154,X1147)
(T,F,F),
F,F)),
F,
-(X960,X958)(F,F,
-(X1148,X1147)(F,F,
-(X1152,X1150)
(+(X1154,X1147)
(T,F,F),
F,F)))),
F,
-(X1148,X1147)(F,F,
-(X1152,X1150)(+(X1154,X1147)(T,F,F),F,F))))
xml(F)
record(F)
arrow(F)
absent=false>
X1154=<types = Any \ [ ]
ints(T)
atoms(Cofinite[(->Finite[[ ]])])
chars(T)
abstract(T)
times(T)
xml(T)
record(T)
arrow(T)
absent=false>
X458=<types = Any \ [ ]
ints(T)
atoms(Cofinite[(->Finite[[ ]])])
chars(T)
abstract(T)
times(T)
xml(T)
record(T)
arrow(T)
absent=false>
X958=<types = [ '7M_9* ]
ints(F)
atoms(Finite[(->Finite[[ ]])])
chars(F)
abstract(F)
times((X959,X958)(T,F,F))
xml(F)
record(F)
arrow(F)
absent=false>
X46=ANY
X919=<types = Any \ (Any \ '7M_9 | '8M_10,Any)
ints(T)
atoms(T)
chars(T)
abstract(T)
times((X910,X46)(F,F,T))
xml(T)
record(T)
arrow(T)
absent=false>
X1148=<types = Any \ (Any \ '7M_9 | '8M_10,Any)
ints(T)
atoms(T)
chars(T)
abstract(T)
times((X1149,X1147)(F,F,T))
xml(T)
record(T)
arrow(T)
absent=false>
X1147=ANY
X1152=<types = [ '7M_9* ]
ints(F)
atoms(Finite[(->Finite[[ ]])])
chars(F)
abstract(F)
times((X1153,X1152)(T,F,F))
xml(F)
record(F)
arrow(F)
absent=false>
X1150=<types = [ '7M_9* ]
ints(F)
atoms(Finite[(->Finite[[ ]])])
chars(F)
abstract(F)
times((X1151,X1150)(T,F,F))
xml(F)
record(F)
arrow(F)
absent=false>
X960=<types = [ '7M_9* ]
ints(F)
atoms(Finite[(->Finite[[ ]])])
chars(F)
abstract(F)
times((X961,X960)(T,F,F))
xml(F)
record(F)
arrow(F)
absent=false>
X910=<types = Any \ '7M_9 | '8M_10
ints(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
atoms(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
chars(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
abstract(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
times(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
xml(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
record(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
arrow(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
absent=false>
X961=<types = '7M_9
ints(VAR(9,7M,`user)(T,F,F))
atoms(VAR(9,7M,`user)(T,F,F))
chars(VAR(9,7M,`user)(T,F,F))
abstract(VAR(9,7M,`user)(T,F,F))
times(VAR(9,7M,`user)(T,F,F))
xml(VAR(9,7M,`user)(T,F,F))
record(VAR(9,7M,`user)(T,F,F))
arrow(VAR(9,7M,`user)(T,F,F))
absent=false>
X1149=<types = Any \ '7M_9 | '8M_10
ints(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
atoms(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
chars(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
abstract(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
times(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
xml(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
record(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
arrow(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
absent=false>
X959=<types = '7M_9
ints(VAR(9,7M,`user)(T,F,F))
atoms(VAR(9,7M,`user)(T,F,F))
chars(VAR(9,7M,`user)(T,F,F))
abstract(VAR(9,7M,`user)(T,F,F))
times(VAR(9,7M,`user)(T,F,F))
xml(VAR(9,7M,`user)(T,F,F))
record(VAR(9,7M,`user)(T,F,F))
arrow(VAR(9,7M,`user)(T,F,F))
absent=false>
X1153=<types = '7M_9
ints(VAR(9,7M,`user)(T,F,F))
atoms(VAR(9,7M,`user)(T,F,F))
chars(VAR(9,7M,`user)(T,F,F))
abstract(VAR(9,7M,`user)(T,F,F))
times(VAR(9,7M,`user)(T,F,F))
xml(VAR(9,7M,`user)(T,F,F))
record(VAR(9,7M,`user)(T,F,F))
arrow(VAR(9,7M,`user)(T,F,F))
absent=false>
X1151=<types = '7M_9
ints(VAR(9,7M,`user)(T,F,F))
atoms(VAR(9,7M,`user)(T,F,F))
chars(VAR(9,7M,`user)(T,F,F))
abstract(VAR(9,7M,`user)(T,F,F))
times(VAR(9,7M,`user)(T,F,F))
xml(VAR(9,7M,`user)(T,F,F))
record(VAR(9,7M,`user)(T,F,F))
arrow(VAR(9,7M,`user)(T,F,F))
absent=false>
======== Initial\Simp (false):
@<types = [ Empty ]
ints(F)
atoms(F)
chars(F)
abstract(F)
times((X458,X46)(+(X919,X46)(F,F,
-(X960,X958)(+(X1148,X1147)(T,
=(X1152,X1150)
(F,
=(X1154,X1147)
(F,F,T),T),
F),
F,F)),
F,F))
xml(F)
record(F)
arrow(F)
absent=false>
X1154=<types = Any \ [ ]
ints(T)
atoms(Cofinite[(->Finite[[ ]])])
chars(T)
abstract(T)
times(T)
xml(T)
record(T)
arrow(T)
absent=false>
X458=<types = Any \ [ ]
ints(T)
atoms(Cofinite[(->Finite[[ ]])])
chars(T)
abstract(T)
times(T)
xml(T)
record(T)
arrow(T)
absent=false>
X958=<types = [ '7M_9* ]
ints(F)
atoms(Finite[(->Finite[[ ]])])
chars(F)
abstract(F)
times((X959,X958)(T,F,F))
xml(F)
record(F)
arrow(F)
absent=false>
X46=ANY
X919=<types = Any \ (Any \ '7M_9 | '8M_10,Any)
ints(T)
atoms(T)
chars(T)
abstract(T)
times((X910,X46)(F,F,T))
xml(T)
record(T)
arrow(T)
absent=false>
X1148=<types = Any \ (Any \ '7M_9 | '8M_10,Any)
ints(T)
atoms(T)
chars(T)
abstract(T)
times((X1149,X1147)(F,F,T))
xml(T)
record(T)
arrow(T)
absent=false>
X1147=ANY
X1152=<types = [ '7M_9* ]
ints(F)
atoms(Finite[(->Finite[[ ]])])
chars(F)
abstract(F)
times((X1153,X1152)(T,F,F))
xml(F)
record(F)
arrow(F)
absent=false>
X1150=<types = [ '7M_9* ]
ints(F)
atoms(Finite[(->Finite[[ ]])])
chars(F)
abstract(F)
times((X1151,X1150)(T,F,F))
xml(F)
record(F)
arrow(F)
absent=false>
X960=<types = [ '7M_9* ]
ints(F)
atoms(Finite[(->Finite[[ ]])])
chars(F)
abstract(F)
times((X961,X960)(T,F,F))
xml(F)
record(F)
arrow(F)
absent=false>
X910=<types = Any \ '7M_9 | '8M_10
ints(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
atoms(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
chars(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
abstract(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
times(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
xml(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
record(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
arrow(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
absent=false>
X961=<types = '7M_9
ints(VAR(9,7M,`user)(T,F,F))
atoms(VAR(9,7M,`user)(T,F,F))
chars(VAR(9,7M,`user)(T,F,F))
abstract(VAR(9,7M,`user)(T,F,F))
times(VAR(9,7M,`user)(T,F,F))
xml(VAR(9,7M,`user)(T,F,F))
record(VAR(9,7M,`user)(T,F,F))
arrow(VAR(9,7M,`user)(T,F,F))
absent=false>
X1149=<types = Any \ '7M_9 | '8M_10
ints(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
atoms(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
chars(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
abstract(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
times(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
xml(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
record(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
arrow(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
absent=false>
X959=<types = '7M_9
ints(VAR(9,7M,`user)(T,F,F))
atoms(VAR(9,7M,`user)(T,F,F))
chars(VAR(9,7M,`user)(T,F,F))
abstract(VAR(9,7M,`user)(T,F,F))
times(VAR(9,7M,`user)(T,F,F))
xml(VAR(9,7M,`user)(T,F,F))
record(VAR(9,7M,`user)(T,F,F))
arrow(VAR(9,7M,`user)(T,F,F))
absent=false>
X1153=<types = '7M_9
ints(VAR(9,7M,`user)(T,F,F))
atoms(VAR(9,7M,`user)(T,F,F))
chars(VAR(9,7M,`user)(T,F,F))
abstract(VAR(9,7M,`user)(T,F,F))
times(VAR(9,7M,`user)(T,F,F))
xml(VAR(9,7M,`user)(T,F,F))
record(VAR(9,7M,`user)(T,F,F))
arrow(VAR(9,7M,`user)(T,F,F))
absent=false>
X1151=<types = '7M_9
ints(VAR(9,7M,`user)(T,F,F))
atoms(VAR(9,7M,`user)(T,F,F))
chars(VAR(9,7M,`user)(T,F,F))
abstract(VAR(9,7M,`user)(T,F,F))
times(VAR(9,7M,`user)(T,F,F))
xml(VAR(9,7M,`user)(T,F,F))
record(VAR(9,7M,`user)(T,F,F))
arrow(VAR(9,7M,`user)(T,F,F))
absent=false>
```Kim NguyễnKim Nguyễnhttps://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues/41Remaining `failwith`s in the code2024-02-29T14:34:06+01:00Tomaz MascarenhasRemaining `failwith`s in the codeWe should add new exceptions to the remaining `failwith`s in the code. One example is line 589 of `mlstub.real.ml` (branch exceptions-refactor).We should add new exceptions to the remaining `failwith`s in the code. One example is line 589 of `mlstub.real.ml` (branch exceptions-refactor).Refactor of Exceptionshttps://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 Exceptionshttps://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues/39Replace `Num` by `Zarith`2024-01-29T15:08:05+01:00Tomaz MascarenhasReplace `Num` by `Zarith`Tomaz MascarenhasTomaz Mascarenhashttps://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues/38Remove support for OCaml 4.07.1 and older2024-01-05T17:41:16+01:00Tomaz MascarenhasRemove support for OCaml 4.07.1 and olderThis amounts to removing the branches `OCAML_VERSION < 408` at `ocamliface/mlcompat.cpp.ml` and fixing anything that breaks.
Eventually we will also remove support for other newer versions.This amounts to removing the branches `OCAML_VERSION < 408` at `ocamliface/mlcompat.cpp.ml` and fixing anything that breaks.
Eventually we will also remove support for other newer versions.Tomaz MascarenhasTomaz Mascarenhashttps://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues/19repeated definitions bring bugs in the toplevel2022-12-09T16:12:15+01:00Giuseppe Castagnarepeated definitions bring bugs in the toplevelDefine the following flatten function in the toplevel:
````
type Tree('a) = ('a\[Any*]) | [ (Tree('a))* ]
let flatten ( (Tree('a)) -> ['a*])
| [] -> []
| [h ;t] -> (flatten h)@(flatten t)
| x -> [x];;
# flatten [ 3 'r' [ 4 [...Define the following flatten function in the toplevel:
````
type Tree('a) = ('a\[Any*]) | [ (Tree('a))* ]
let flatten ( (Tree('a)) -> ['a*])
| [] -> []
| [h ;t] -> (flatten h)@(flatten t)
| x -> [x];;
# flatten [ 3 'r' [ 4 [ `true 5 ]] [ "quo" [[ `false ] "stop" ] ] ];;
- : [ (Bool | 3--5 | 'o'--'u')* ] = [ 3 'r' 4 true 5 'quo' false 'stop' ]
````
now define it a second time in the toplevel
````
let flatten ( (Tree('a)) -> ['a*])
| [] -> []
| [h ;t] -> (flatten h)@(flatten t)
| x -> [x];;
# flatten [ 3 'r' [ 4 [ `true 5 ]] [ "quo" [[ `false ] "stop" ] ] ];;
- : [ (Bool | 3--5 | 'o'--'u')* ] = [ [ 3
'r'
[ 4 [ true 5 ] ]
[ "quo" [ [ false ] "stop" ] ]
]
]
````
duh? It has become the identity function and with the wrong type.https://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues/14Tallying: monomorphic variables are not handled correctly2022-12-09T16:10:58+01:00Tommaso PetruccianiTallying: monomorphic variables are not handled correctlyWhen we perform tallying with a non-empty delta and types contain
top-level variables that are in delta, we do not handle them correctly.
See
~~~
debug tallying ['b] [ ('a, Int) , 'b ];;
~~~
(no solution found, while `'a<-Empty` works) ...When we perform tallying with a non-empty delta and types contain
top-level variables that are in delta, we do not handle them correctly.
See
~~~
debug tallying ['b] [ ('a, Int) , 'b ];;
~~~
(no solution found, while `'a<-Empty` works) and
~~~
debug tallying ['b] [ ('a, Int) , 'b | 'c ];;
~~~
(no solution found, while it works if we use `['c]` as delta instead).
The problem is in Type_tallying.toplevel (line 245).
We can probably fix it as follows. Currently, we always pick the first variable (positive or negative) that we find (we give priority to polymorphic ones only in one branch of matching). Instead, as long as there is at least one polymorphic variable, we should prefer it to monomorphic ones.
If all variables are monomorphic, we should basically test for emptiness of the type without these monomorphic variables. Say the smallest variable is `'a` and is positive; thus we have `t & 'a`. For emptiness we need `t <: not('a)`. However, this should be possible only if `t` contains `not('a)` (which maybe never happens because we would have simplified the type?) or if it is empty (which we surely need to check).Kim NguyễnKim Nguyễnhttps://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues/23Automatic deployment of API documentation2022-12-09T16:10:19+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)Packaginghttps://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/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/28Use of Stream.icons2022-09-30T17:46:35+02:00MattiasUse of Stream.icons`Stream.icons` resets the internal count to 0 which is not coherent with what `count` represents, namely:
```
val count : 'a t -> int
Return the current count of the stream elements, i.e. the number of the stream elements discarded.
``...`Stream.icons` resets the internal count to 0 which is not coherent with what `count` represents, namely:
```
val count : 'a t -> int
Return the current count of the stream elements, i.e. the number of the stream elements discarded.
```
We should investigate the uses of `Stream.icons` in CDuce code and see if we could use a non buggy `icons` function, i.e. a function that does not reset count to 0 (ping @kn )https://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/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/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/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/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/29Fragile reliance on OCaml version number2022-04-12T12:21:37+02:00Kim NguyễnFragile reliance on OCaml version numberTo check and select the appropriate compatibility stubs for the CDuce - OCaml interface, [ocamliface/dune](https://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/blob/4c7020d4962321d36ca490380132f37a19647132/ocamliface/dune) clumsily tr...To check and select the appropriate compatibility stubs for the CDuce - OCaml interface, [ocamliface/dune](https://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/blob/4c7020d4962321d36ca490380132f37a19647132/ocamliface/dune) clumsily tries to extract the OCaml version numbers from the version string. The script tries to accounts for `+` in the version number (like 4.12.0+flambda) but failwith e.g. if the version number contains `~` (like 4.14.0~rc2).
At the moment, this results in `dune build` failwith with : `Failure: int_of_string`.
The script should :
- be more robust w.r.t. various versioning schemes (i.e. be able to parse `x.y.zS` where `x`, `y`, `z` are integers and `S` any string)
- never fail but should simply disable the OCaml - CDuce interface if the version number cannot be determined.
tKim 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/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]