From 1806f98894ed2bac070e42654e15f17dd606c3be Mon Sep 17 00:00:00 2001 From: Romain Beauxis Date: Sun, 12 Nov 2023 16:56:36 -0600 Subject: [PATCH] Add univ type annotation. --- src/lang/parser.mly | 3 ++- src/lang/parser_helper.ml | 30 ++++++++++++++++++++++++++++++ src/lang/parser_helper.mli | 1 + src/lang/repr.ml | 21 +++------------------ src/lang/term/parsed_term.ml | 1 + src/lang/types/type_base.ml | 26 ++++++++++++++++++++++++++ src/tooling/parsed_json.ml | 3 +++ 7 files changed, 66 insertions(+), 19 deletions(-) diff --git a/src/lang/parser.mly b/src/lang/parser.mly index 56e8b9ce98..6aad13e44c 100644 --- a/src/lang/parser.mly +++ b/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) } diff --git a/src/lang/parser_helper.ml b/src/lang/parser_helper.ml index 0002389e40..a4844fb884 100644 --- a/src/lang/parser_helper.ml +++ b/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 diff --git a/src/lang/parser_helper.mli b/src/lang/parser_helper.mli index c9f0a8ce46..c2aeee2ce1 100644 --- a/src/lang/parser_helper.mli +++ b/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 : diff --git a/src/lang/repr.ml b/src/lang/repr.ml index 8694648c7e..1a93e27b71 100644 --- a/src/lang/repr.ml +++ b/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 diff --git a/src/lang/term/parsed_term.ml b/src/lang/term/parsed_term.ml index ef4b7a2146..fbbfa22386 100644 --- a/src/lang/term/parsed_term.ml +++ b/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 diff --git a/src/lang/types/type_base.ml b/src/lang/types/type_base.ml index af2b898793..c9b1e9c004 100644 --- a/src/lang/types/type_base.ml +++ b/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 *) diff --git a/src/tooling/parsed_json.ml b/src/tooling/parsed_json.ml index 0efc3178f4..722fe464ac 100644 --- a/src/tooling/parsed_json.ml +++ b/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)