Add univ type annotation.

src/lang/parser.mly

@@ -293,7 +293,8 @@ time_predicate:
 
 ty:
   | UNDERSCORE                   { `Named "_" }
-  | VAR                          { `Named $1 }
+  | VAR                          { if $1 = "univ" then `Univ None else `Named $1 }
+  | VARLPAR VAR RPAR             { mk_univ_term ~pos:$loc ($1, $2) }
   | ty QUESTION                  { `Nullable $1 }
   | LBRA ty RBRA                 { `List $2 }
   | LBRA ty RBRA VAR VAR DOT VAR { mk_json_assoc_object_ty ~pos:$loc ($2,$4,$5,$7) }

src/lang/parser_helper.ml

@@ -121,8 +121,23 @@ let mk_named_ty ?pos = function
               (Term_base.Parse_error
                  (pos, "Unknown type constructor: " ^ name ^ ".")))
 
+let mk_univ_ty ?pos = function
+  | None -> Type.var ()
+  | Some name ->
+      Type.make ?pos
+        Type_base.(
+          Var
+            (ref
+               (Free
+                  {
+                    name = var_index name;
+                    level = max_int;
+                    constraints = Constraints.empty;
+                  })))
+
 let rec mk_ty ?pos = function
   | `Named s -> mk_named_ty ?pos s
+  | `Univ v -> mk_univ_ty ?pos v
   | `Nullable t -> Type.(make (Nullable (mk_ty ?pos t)))
   | `List t -> Type.(make (List { t = mk_ty ?pos t; json_repr = `Tuple }))
   | `Json_object t ->
@@ -171,6 +186,21 @@ type let_opt_el = string * Term.t
 type meth_term_default = [ `Nullable | `Pattern of Term.pattern | `None ]
 type meth_pattern_el = string * meth_term_default
 
+let mk_univ_term ~pos = function
+  | "univ", v ->
+      String.iter
+        (fun c ->
+          let c = int_of_char c in
+          if c < int_of_char 'a' || int_of_char 'z' < c then
+            raise
+              (Term_base.Parse_error
+                 ( pos,
+                   "universal variable names should only be made of only a-z \
+                    letters" )))
+        v;
+      `Univ (Some v)
+  | _ -> raise (Term_base.Parse_error (pos, "Invalid type constructor"))
+
 let let_decoration_of_lexer_let_decoration = function
   | `Json_parse -> `Json_parse []
   | `Yaml_parse -> `Yaml_parse

src/lang/parser_helper.mli

@@ -39,6 +39,7 @@ type meth_pattern_el = string * meth_term_default
 val clear_comments : unit -> unit
 val append_comment : pos:Pos.t -> string -> unit
 val attach_comments : Term.t -> unit
+val mk_univ_term : pos:Pos.t -> string * string -> Parsed_term.type_annotation
 val mk_ty : ?pos:Pos.t -> Parsed_term.type_annotation -> Type.t
 
 val mk_let :

src/lang/repr.ml

@@ -76,21 +76,6 @@ let excerpt (start, stop) =
 
 let excerpt_opt = function Some pos -> excerpt pos | None -> None
 
-(** Given a strictly positive integer, generate a name in [a-z]+:
-    a, b, ... z, aa, ab, ... az, ba, ... *)
-let name =
-  let base = 26 in
-  let c i = char_of_int (int_of_char 'a' + i - 1) in
-  let add i suffix = Printf.sprintf "%c%s" (c i) suffix in
-  let rec n suffix i =
-    if i <= base then add i suffix
-    else (
-      let head = i mod base in
-      let head = if head = 0 then base else head in
-      n (add head suffix) ((i - head) / base))
-  in
-  n ""
-
 (** Compute the structure that a term represents, given the list of universally
     quantified variables. Also takes care of computing the printing name of
     variables, including constraint symbols, which are removed from constraint
@@ -100,7 +85,7 @@ let make ?(filter_out = fun _ -> false) ?(generalized = []) t : t =
   let uvar g var =
     let rec index n = function
       | v :: tl ->
-          if Var.eq v var then Printf.sprintf "'%s" (name n)
+          if Var.eq v var then Printf.sprintf "univ(%s)" (Type_base.var_name n)
           else index (n + 1) tl
       | [] -> assert false
     in
@@ -119,11 +104,11 @@ let make ?(filter_out = fun _ -> false) ?(generalized = []) t : t =
     let s =
       try Hashtbl.find evars var.name
       with Not_found ->
-        let name = String.uppercase_ascii (name (counter ())) in
+        let name = String.uppercase_ascii (Type_base.var_name (counter ())) in
         Hashtbl.add evars var.name name;
         name
     in
-    `EVar (Printf.sprintf "'%s" s, var.constraints)
+    `EVar (Printf.sprintf "univ(%s)" s, var.constraints)
   in
   let rec repr g t =
     if filter_out t then `Ellipsis

src/lang/term/parsed_term.ml

@@ -54,6 +54,7 @@ and source_annotation = {
 
 and type_annotation =
   [ `Named of string
+  | `Univ of string option
   | `Nullable of type_annotation
   | `List of type_annotation
   | `Json_object of type_annotation

src/lang/types/type_base.ml

@@ -82,6 +82,32 @@ type var = {
   mutable constraints : Constraints.t;
 }
 
+(** Given a strictly positive integer, generate a name in [a-z]+:
+    a, b, ... z, aa, ab, ... az, ba, ... *)
+let var_name =
+  let base = 26 in
+  let c i = char_of_int (int_of_char 'a' + i - 1) in
+  let rec name cur left =
+    let n = left mod base in
+    let cur = Printf.sprintf "%c%s" (c n) cur in
+    let rest = left / base in
+    if rest = 0 then cur else name cur rest
+  in
+  name ""
+
+(** Inverse of the above function *)
+let var_index s =
+  let base = 26 in
+  let s = String.lowercase_ascii s in
+  let chars = List.rev (List.of_seq (String.to_seq s)) in
+  let char_idx c = 1 + int_of_char c - int_of_char 'a' in
+  let _, idx =
+    List.fold_left
+      (fun (lvl, idx) c -> (lvl * base, idx + (lvl * char_idx c)))
+      (1, 0) chars
+  in
+  idx
+
 type invar =
   | Free of var  (** the variable is free *)
   | Link of variance * t  (** the variable has bee substituted *)

src/tooling/parsed_json.ml

@@ -122,6 +122,9 @@ let json_of_annotated_string = function
 
 let rec json_of_type_annotation = function
   | `Named n -> type_node ~typ:"named" (`String n)
+  | `Univ None -> type_node ~typ:"named" (`String "univ")
+  | `Univ (Some name) ->
+      type_node ~typ:"named" (`String (Printf.sprintf "univ(%s)" name))
   | `Nullable t -> type_node ~typ:"nullable" (json_of_type_annotation t)
   | `List t -> type_node ~typ:"list" (json_of_type_annotation t)
   | `Json_object t -> type_node ~typ:"json_object" (json_of_type_annotation t)