GitLab

Fix a pretty printing error for ground types (the negative part was not shown due to "worth_complement" being called twice).

when a constraint 'a < t or t < 'a with 'a being monomorphic occurs during constraint generation, we check whether
it holds for all 'a, that is we use plain subtyping.
(It generalizes the fact that 'a < Any or Empty < 'a hold for monomorphic variables, but also accounts for constraints such as 'a < 'a | t and so on).

- Change the precedence of the XML constructor to be stronger than the set-theoretic operations (compatibility with previous CDuce)
- Pretty-printing of regular expressions. When the input type contains a sequence type, print the sequence as a regular expression. Do not print empty sequences unless the rest of the atom components is finite:
     `a |`b | `nil
will be printed as
     [] | `a | `b
but
     Atom \ 'a
will be printed as
     Atom \'a
and not
     Atom \ ('a | `nil) | []
- Remove Arrow from positive arrow part (unless it is the only component)
- Fix a bug where records would be printed instead of attributes

- Simplify the pretty-printing descriptor type
- Fix a bug where some unions were shown as intersections
- Correctly display parentheses where needed (issue: #17)
- Prevent sharing for "small" subtrees (AST less than 6 nodes), so:
  (Int -> Int) -> Int -> Int
  is not shown as:
  X1 -> X1 where X1 = Int -> Int
  (but bigger types are).

Partial fix for issue #20. In the Value.t type, the Concat _ value and the Pair value must have the same underlying representation (since their tag is mutated).
This actually also corrects a bug: Concat _ nodes acts as constructor (like pairs, xml, records, …) and should also be decorated with a sigma. Adding a sigma component to Concat make the segfault disapear. However, for the moment substitutions in Concat are never used.

distribute it (redudantly) under all variables to simplify their pretty-printing.

Hence, instead of having e.g. :

('a \ (Int)) | Char | Int | Atom)

we have
('a | Char | Int | Atom)

* 'master' of https://git.cduce.org/cduce:
  [MINOR] Remove dependence with Str module in parser
  Add syntactic sugar for if_then:
  Bugfix in parser: syntactic sugar if_then_else

Refresh the type of variables in the environement to avoid clash with variables of the interface of the function being typed.

	if cond then expr <=> if cond then expr else []

Note that in case of ambiguity the "else" statement is part of the last "if"
statement:

	if a then if b then c else d <=> if a then (if b then c else d)

Only use the old typing of applications for ground types (not types with only monomorphic variables)

Remove commented code in clean_type. Restore cleaning of variables that are in covariant position in the result type, to avoid having strange types such as: [] -> [ ('b) * ]

Given a type for which each kind is i DNF :

ints: \/ /\a /\v /\~b /\~w
chars: \/ /\a /\v /\~b /\~w
...

where a, b are atoms and v w toplevel variables, index the type by
pairs of variables, for each kind, which gives a matrix of 8 lines.
                    ...   (v, w) ...   (x,y) ...
ints:                      t1           t1
chars:                     ...         ...
atoms:
times:
xml:
arrow:
record:
abstract:                  t8           t8

let T = t1 | ... | t8,
we can write ((v & w) | (x & y)) & T
we now try to factor according to variables (intersection of v x and w y)
to have a type of the form: ('a | ... | 'd) & 'e ... & (Any \ 'f) & T

cases like this:

	type t = ['b '@' 'a]

We have a syntax error because CDuce thinks 'b ' as a string, to fix that,
implicitly write:

	type t = [('b) '@' 'a]

variables in brackets. However, we can't write ';;' in strings in brackets in
toplevel now:

	# type t = ['a];;
	# type t = ['a'];;
	# type t = ['a 'a'];;
	# type t = [';;'];;
	Characters 10-11:
	Illegal character

We still have to print a better error message.

* 'master' of https://git.cduce.org/cduce:
  Preliminary work-around to only substitute by any/empty variables that were introduced by the tallying.
  [TESTS] Progress in stdlib/list

Preliminary work-around to only substitute by any/empty variables that were introduced by the tallying.

precise = false returns the constraint itself as output type (which is not sound when it is a variable).

for each component (int, atoms, pairs...) we optimize the case where the component is like

  T1&'a | T2 | T3&'a

we split it into
- T2
- T1 &'a | T3 &'a
we retrieve { 'a } as the set of top level vars in the second type
we compute T2 &'a | T1 &'a | T3 &'a
then remove 'a from that type and return finally :

T2 | ('a & (T1 | T2 | T3))

We special case if (T1 | T2 | T3) is top, then we just display
T2 | 'a

of sequence|non_variable|(toplevelvar ^ rest)
with special cases when non_variable or sequence are empty and toplevelvar or rest are any
(or any combination of thoses).

Add the examples of the part2 paper in a test file.

not propely propagate in case the left component was a 1 element intersection or union
containing an arrow)
Note: we should not have been generating such types in the first place.

Fix typing of application. Apply the polymorphic code when either the function or its argument have variables.

This reverts commit 045a8519.