Support for direct tuple member access

As discussed in #549

NOTE: This implements only the direct tuple member access (syntax `foo.N` with N a
number)

- It seems more efficient to wait for the general pattern-matching rewrite to
  handle pattern-matching on tuples
- Until then we keep the (now obsolete) `let (x, y) = pair in x` syntax, to
  leave time for updates, but we won't be documenting it
This commit is contained in:
Louis Gesbert 2024-04-12 11:36:43 +02:00
parent 87b2c4ded2
commit eded54d2b5
10 changed files with 297 additions and 216 deletions

View File

@ -715,6 +715,8 @@ let rec translate_expr
Expr.ematch ~e:(rec_helper e1) ~name:enum_uid ~cases emark
| ArrayLit es -> Expr.earray (List.map rec_helper es) emark
| Tuple es -> Expr.etuple (List.map rec_helper es) emark
| TupleAccess (e, n) ->
Expr.etupleaccess ~e:(rec_helper e) ~index:(Mark.remove n - 1) ~size:0 emark
| CollectionOp (((S.Filter { f } | S.Map { f }) as op), collection) ->
let param_names, predicate = f in
let collection =

View File

@ -117,7 +117,7 @@ let eexternal ~name mark = Mark.add mark (Bindlib.box (EExternal { name }))
let etuple args = Box.appn args @@ fun args -> ETuple args
let etupleaccess ~e ~index ~size =
assert (index < size);
assert (size = 0 || index < size);
Box.app1 e @@ fun e -> ETupleAccess { e; index; size }
let earray args = Box.appn args @@ fun args -> EArray args

View File

@ -799,16 +799,36 @@ and typecheck_expr_top_down :
let es' = List.map2 (typecheck_expr_top_down ctx env) tys es in
Expr.etuple es' mark
| A.ETupleAccess { e = e1; index; size } ->
if index >= size then
Message.error ~pos:(Expr.pos e) "Tuple access out of bounds (%d/%d)" index
size;
let tuple_ty =
TTuple
(List.init size (fun n ->
if n = index then tau else unionfind ~pos:e1 (TAny (Any.fresh ()))))
let out_of_bounds size =
Message.error ~pos:pos_e "Tuple access out of bounds (%d/%d)" index size
in
let e1' = typecheck_expr_top_down ctx env (unionfind ~pos:e1 tuple_ty) e1 in
Expr.etupleaccess ~e:e1' ~index ~size context_mark
let tuple_ty =
if size = 0 then (* Unset yet, we resolve it now *)
TAny (Any.fresh ())
else if index >= size then out_of_bounds size
else
TTuple
(List.init size (fun n ->
if n = index then tau
else unionfind ~pos:e1 (TAny (Any.fresh ()))))
in
let tuple_ty = unionfind ~pos:e1 tuple_ty in
let e1' = typecheck_expr_top_down ctx env tuple_ty e1 in
let size, mark =
if size <> 0 then size, context_mark
else
match typ_to_ast ~flags tuple_ty with
| TTuple l, _ -> (
match List.nth_opt l index with
| None -> out_of_bounds (List.length l)
| Some ty -> List.length l, mark_with_tau_and_unify (ast_to_typ ty))
| TAny, _ -> failwith "Disambiguation failure"
| ty ->
Message.error ~pos:(Expr.pos e1)
"This expression has type@ %a,@ while a tuple was expected"
(Print.typ ctx) ty
in
Expr.etupleaccess ~e:e1' ~index ~size mark
| A.EAbs { binder; tys = t_args } ->
if Bindlib.mbinder_arity binder <> List.length t_args then
Message.error ~pos:(Expr.pos e)

View File

@ -70,6 +70,9 @@ val expr :
- disambiguation of constructors: [EDStructAccess] nodes are translated into
[EStructAccess] with the suitable structure and field idents (this only
concerns [desugared] expressions).
- disambiguation of structure names in [EDStructAmend] nodes ([desugared] as
well)
- resolution of tuple size (when equal to 0) on [ETupleAccess] nodes
- resolution of operator types, which are stored (monomorphised) back in the
[EAppOp] nodes
- resolution of function application input types on the [EApp] nodes, when

View File

@ -194,6 +194,7 @@ and naked_expression =
(* path, ident, state *)
| Dotted of expression * (path * lident Mark.pos) Mark.pos
(** Dotted is for both struct field projection and sub-scope variables *)
| TupleAccess of expression * int Mark.pos
and exception_to =
| NotAnException

File diff suppressed because it is too large Load Diff

View File

@ -191,6 +191,13 @@ let naked_expression ==
}
| e = expression ;
DOT ; i = addpos(qlident) ; <Dotted>
| e = expression ; DOT ; arg = addpos(INT_LITERAL) ; {
let n_str, pos_n = arg in
let n = int_of_string n_str in
if n <= 0 then
Message.error ~pos:pos_n "Tuple indices must be >= 1";
TupleAccess (e, (n, pos_n))
}
| CARDINAL ; {
Builtin Cardinal
}

View File

@ -133,11 +133,12 @@ module ParserAux (LocalisedLexer : Lexer_common.LocalisedLexer) = struct
| msg ->
Format.fprintf ppf "@{<yellow>@<1>»@} @[<hov>%a@]" Format.pp_print_text
(String.trim (String.uncapitalize_ascii msg)));
Format.fprintf ppf "@,@[<hov>Those are valid at this point:@ %a@]"
(Format.pp_print_list
~pp_sep:(fun ppf () -> Format.fprintf ppf ",@ ")
(fun ppf string -> Format.fprintf ppf "@{<yellow>\"%s\"@}" string))
(List.map (fun (s, _) -> s) acceptable_tokens)
if acceptable_tokens <> [] then
Format.fprintf ppf "@,@[<hov>Those are valid at this point:@ %a@]"
(Format.pp_print_list
~pp_sep:(fun ppf () -> Format.fprintf ppf ",@ ")
(fun ppf string -> Format.fprintf ppf "@{<yellow>\"%s\"@}" string))
(List.map (fun (s, _) -> s) acceptable_tokens)
in
raise_parser_error ~suggestion:similar_acceptable_tokens
(Pos.from_lpos (lexing_positions lexbuf))

View File

@ -16,7 +16,7 @@ declaration f2 content decimal
equals
match en with pattern
-- One of str1:
let (a, w) equals str.x1 in
let a equals str.x1.1 in
let (b, w) equals str1.x1 in
a / b
-- Two of z:

View File

@ -37,8 +37,7 @@ scope S:
definition r5 equals (x * y, y / z) for (x, y, z) among (lis1, lis2, lis3)
definition r6 equals
let lis12 equals (x, y) for (x, y) among (lis1, lis2) in
(let (x, y) equals xy in (x * y, y / z))
for (xy, z) among (lis12, lis3)
(xy.1 * xy.2, xy.2 / z) for (xy, z) among (lis12, lis3)
```