Add infrastructure to parse polymorphic variables

For the moment are identied as `$X and interpreted as atoms

parser/ast.ml

@@ -46,6 +46,7 @@ and pexpr =
 
   (* CDuce is a Lambda-calculus ... *)
   | Var of U.t
+  | TVar of U.t
   | Apply of pexpr * pexpr
   | Abstraction of abstr
       

parser/parser.ml

@@ -404,6 +404,7 @@ EXTEND Gram
 
   tag_type: [
     [ "_" ->  mk _loc (Internal (Types.atom Atoms.any))
+    | "$"; a = ident_or_keyword -> mk _loc (Cst (TVar (ident a)))
     | a = ident_or_keyword -> mk _loc (Cst (Atom (ident a)))
     | t = ANY_IN_NS -> mk _loc (NsT (ident t)) 
     ]

parser/ulexer.ml

@@ -202,7 +202,7 @@ let rec token = lexer
      return lexbuf (ANY_IN_NS "")
  | '-'? ['0'-'9']+ ->
      return lexbuf (INT (L.utf8_lexeme lexbuf))
- | [ "<>=.,:;+-*/@&{}[]()|?`!" ]
+ | [ "<>=.,:;+-*/@&{}[]()|?`!$" ]
  | "->" | "::" | ";;" | "--" | "//" | "/@" | ":=" | "\\" | "++"
  | "<=" | ">=" | "<<" | ">>" | "||" | "&&" | "**" | "_"
  | ".."

tests/libtest/tests.ml

@@ -56,6 +56,7 @@ let subtype_tests = [
   "1--5" , "1--4", false ;
   "Int" , "0--*", false ;
 
+  "`$X" , "Any", true;
 ];;
 
 let test_subtype =

types/types.ml

@@ -19,6 +19,7 @@ let compare = 1
 type const = 
   | Integer of Intervals.V.t
   | Atom of Atoms.V.t
+  | Var of Atoms.V.t
   | Char of Chars.V.t
   | Pair of const * const
   | Xml of const * const
@@ -62,6 +63,10 @@ module Const = struct
     | Atom x, Atom y -> Atoms.V.compare x y
     | Atom _, _ -> -1
     | _, Atom _ -> 1
+    | Var x, Var y -> Atoms.V.compare x y
+    | Var _, _ -> -1
+    | _, Var _ -> 1
+
     | Char x, Char y -> Chars.V.compare x y
     | Char _, _ -> -1
     | _, Char _ -> 1
@@ -94,6 +99,7 @@ module Const = struct
     | Xml (x,y) -> 5 + 17 * (hash x) + 257 * (hash y)
     | Record x -> 6 + 17 * (LabelMap.hash hash x)
     | String (i,j,s,r) -> 7 + 17 * (U.hash s) + 257 * hash r
+    | Var x -> 7 + 17 * (Atoms.V.hash x)
       (* Note: improve hash for String *)
 
   let equal c1 c2 = compare c1 c2 = 0
@@ -134,6 +140,7 @@ module rec Descr :
 sig
   type s = {
     atoms : Atoms.t;
+    vars  : Atoms.t;
     ints  : Intervals.t;
     chars : Chars.t;
     times : BoolPair.t;
@@ -149,6 +156,7 @@ end =
 struct
   type s = {
     atoms : Atoms.t;
+    vars  : Atoms.t;
     ints  : Intervals.t;
     chars : Chars.t;
     times : BoolPair.t;
@@ -177,6 +185,7 @@ struct
     record= BoolRec.empty;
     ints  = Intervals.empty;
     atoms = Atoms.empty;
+    vars = Atoms.empty;
     chars = Chars.empty;
     abstract = Abstract.empty;
     absent= false;
@@ -225,6 +234,7 @@ struct
     Chars.check a.chars;
     Intervals.check a.ints;
     Atoms.check a.atoms;
+    Atoms.check a.vars;
     BoolPair.check a.times;
     BoolPair.check a.xml;
     BoolPair.check a.arrow;
@@ -309,6 +319,7 @@ let any =  {
   record= BoolRec.full; 
   ints  = Intervals.any;
   atoms = Atoms.any;
+  vars = Atoms.any;
   chars = Chars.any;
   abstract = Abstract.any;
   absent= false;
@@ -332,6 +343,7 @@ let record label t =
 let record_fields (x : bool * node Ident.label_map) =
   { empty with record = BoolRec.atom x }
 let atom a = { empty with atoms = a }
+let vars a = { empty with vars = a }
 let char c = { empty with chars = c }
 let abstract a = { empty with abstract = a }
 
@@ -345,6 +357,7 @@ let cup x y =
     record= BoolRec.cup x.record y.record;
     ints  = Intervals.cup x.ints  y.ints;
     atoms = Atoms.cup x.atoms y.atoms;
+    vars = Atoms.cup x.vars y.vars;
     chars = Chars.cup x.chars y.chars;
     abstract = Abstract.cup x.abstract y.abstract;
     absent= x.absent || y.absent;
@@ -358,6 +371,7 @@ let cap x y =
     arrow = BoolPair.cap x.arrow y.arrow;
     ints  = Intervals.cap x.ints  y.ints;
     atoms = Atoms.cap x.atoms y.atoms;
+    vars = Atoms.cap x.vars y.vars;
     chars = Chars.cap x.chars y.chars;
     abstract = Abstract.cap x.abstract y.abstract;
     absent= x.absent && y.absent;
@@ -371,6 +385,7 @@ let diff x y =
     record= BoolRec.diff x.record y.record;
     ints  = Intervals.diff x.ints  y.ints;
     atoms = Atoms.diff x.atoms y.atoms;
+    vars = Atoms.diff x.vars y.vars;
     chars = Chars.diff x.chars y.chars;
     abstract = Abstract.diff x.abstract y.abstract;
     absent= x.absent && not y.absent;
@@ -384,6 +399,7 @@ let trivially_disjoint a b =
   (Chars.disjoint a.chars b.chars) &&
   (Intervals.disjoint a.ints b.ints) &&
   (Atoms.disjoint a.atoms b.atoms) &&
+  (Atoms.disjoint a.vars b.vars) &&
   (BoolPair.trivially_disjoint a.times b.times) &&
   (BoolPair.trivially_disjoint a.xml b.xml) &&
   (BoolPair.trivially_disjoint a.arrow b.arrow) &&
@@ -391,16 +407,14 @@ let trivially_disjoint a b =
   (Abstract.disjoint a.abstract b.abstract) &&
   (not (a.absent && b.absent))
 
-
-
 let descr n = n.Node.descr
 let internalize n = n
 let id n = n.Node.id
 
-
 let rec constant = function
   | Integer i -> interval (Intervals.atom i)
   | Atom a -> atom (Atoms.atom a)
+  | Var a -> vars (Atoms.atom a)
   | Char c -> char (Chars.atom c)
   | Pair (x,y) -> times (const_node x) (const_node y)
   | Xml (x,y) -> xml (const_node x) (const_node y)
@@ -1378,6 +1392,7 @@ struct
   let rec print_const ppf = function
     | Integer i -> Intervals.V.print ppf i
     | Atom a -> Atoms.V.print_quote ppf a
+    | Var a -> Format.fprintf ppf "`$%a" Atoms.V.print_quote a
     | Char c -> Chars.V.print ppf c
     | Pair (x,y) -> Format.fprintf ppf "(%a,%a)" print_const x print_const y
     | Xml (x,y) -> Format.fprintf ppf "XML(%a,%a)" print_const x print_const y

types/types.mli

@@ -3,6 +3,7 @@ open Ident
 type const = 
   | Integer of Intervals.V.t
   | Atom of Atoms.V.t
+  | Var of Atoms.V.t
   | Char of Chars.V.t
   | Pair of const * const
   | Xml of const * const
@@ -106,6 +107,7 @@ type pair_kind = [ `Normal | `XML ]
 
 val interval : Intervals.t -> t
 val atom     : Atoms.t -> t
+val vars     : Atoms.t -> t
 val times    : Node.t -> Node.t -> t
 val xml      : Node.t -> Node.t -> t
 val arrow    : Node.t -> Node.t -> t

typing/typed.ml

@@ -26,6 +26,8 @@ and  texpr' =
   | Check of (Types.t ref) * texpr * ttyp
   (* CDuce is a Lambda-calculus ... *)
   | Var of id
+  (* polymorphic variable *)
+  | TVar of id
   | ExtVar of Compunit.t * id * Types.t
   | Apply of texpr * texpr
   | Abstraction of abstr

typing/typer.ml

@@ -175,6 +175,7 @@ let rec const env loc = function
   | RecordLitt x -> Types.Record (parse_record env loc (const env loc) x)
   | String (i,j,s,c) -> Types.String (i,j,s,const env loc c)
   | Atom t -> Types.Atom (parse_atom env loc t)
+  | TVar t -> Types.Var (parse_atom env loc t)
   | Integer i -> Types.Integer i
   | Char c -> Types.Char c
   | Const c -> c
@@ -514,6 +515,7 @@ let rec expr env loc = function
       let (fv,e) = expr env loc e and t = typ env t in
       exp loc fv (Typed.Check (ref Types.empty,e,t))
   | Var s -> var env loc s
+  | TVar s -> var env loc s
   | Apply (e1,e2) -> 
       let (fv1,e1) = expr env loc e1 and (fv2,e2) = expr env loc e2 in
       let fv = Fv.cup fv1 fv2 in