GitLab

* 'master' of https://git.cduce.org/cduce:
  added code for patricia trees
  Added few twisted examples

* debug-typechecking-issue-27-for-merge:
  Remove debugging code.
  Add patricia.cd file from Issue #21
  Check constraints on monomorphic variables at the right place.
  Fix a pretty printing error for ground types (the negative part was not shown due to "worth_complement" being called twice).
  Rework the type variable infrastructure. Remove it from the type structure and have the auxiliary function cache the results as needed.
  Debugging annotations.

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

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

* new-variables-issue-26:
  Rework the type variable infrastructure. Remove it from the type structure and have the auxiliary function cache the results as needed.
  Properly check constraints on monomprhic variable during constraint generation: 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).

Conflicts:
	types/types.ml

Rework the type variable infrastructure. Remove it from the type structure and have the auxiliary function cache the results as needed.

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.