Kim Nguyễn (25e454b3) at 28 Mar 09:30
Convert exceptions to new types.
Kim Nguyễn (3453423d) at 27 Mar 14:26
WIP.
Kim Nguyễn (78d48ce4) at 27 Mar 10:54
Add forgotten file.
Kim Nguyễn (761cc260) at 26 Mar 20:38
Small refactoring of exception handling code.
Kim Nguyễn (b0d9bbad) at 20 Mar 21:18
Add a lazy interface based on sequences for BDD.
Kim Nguyễn (ade3495b) at 20 Mar 20:35
Convert the singleton extraction function to option like result.
Kim Nguyễn (684565a1) at 20 Mar 20:22
Convert more cduce-types API functions to using options rather than
... and 204 more commits
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:
[Empty]
is not displaying some variables that should be there (it appended before)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>
Fixed in !29 (merged)
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.
Kim Nguyễn (35e8d73e) at 20 Mar 00:22
Merge branch 'subtyping-debug' into 'dev'
... and 1 more commit
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.
Kim Nguyễn (e4bb62b5) at 19 Mar 23:57
Add some more tests for the new subtyping with polymorphic witnesses.
So the solution (which seems to work) is to add a new kind of witness, dubbed polymorphic witness. It adds
a constructor to the witness type, WPoly (Pos, Neg, w)
where Pos
and Neg
are sets of positive
and negative variables and w
is a regular witness.
Now, an inhabitant of Int&'a\'b
will not be WInt(0)
as before but rather WPoly({'a},{'b},WInt(0))
.
Previously, with a witness WInt(0)
when asked if it belonged to the type Int\'a
the subtyping algorithm would say yes, since the \'a
part would be stripped (according to the wrong interpretation of "ignore toplevel variables") and indeed, WInt(0)
is a witness for Int
.
Now we check that WInt(0)
is a witness for Int
(that is we check the regular part of the witness against the monomorphic part of the type) BUT we also check that the variables are compatible. Here, the with the witness WPoly({'a},{'b},WInt(0))
would not belong to Int\'a
since 'a
occurs negatively in the type and positively in the witness.
More generally when checking WPoly(WP, WN, w)
against P & N & T
(where type without toplevel variables),
we check that:
the last two conditions check that the witness has more variables intersected and is therefore more precise that the type we are testing against.
Kim Nguyễn (6ddb7822) at 19 Mar 23:31
Fix a bug in the check of negative variables of polymorphic witnesses.
Kim Nguyễn (00862ed4) at 19 Mar 22:42
Tentative fix for the soundness bug in the subtyping algorithm.
Kim Nguyễn (7f24defc) at 19 Mar 17:13
Add a reproducer for the subyping bug.
... and 202 more commits
Kim Nguyễn (8de429da) at 19 Mar 10:40
Fix a syntax error in yaml file.
Kim Nguyễn (df5769c4) at 19 Mar 10:36
Allow a pipline to run if started manually.