Skip to content

Add support for patterns in top-level declarations

Rémi requested to merge keep_pattern into dev

Motivation and Context

The main goal is to propagate the patterns in both let ... in ...s and top-level lets LHS until after the typed AST.
The main benefit of that:

  • it simplifies the "abstractors" implementation,
  • it solves a really silly bug occurring because of the destructuring of top-level let's:
let (a,a) =
  let () = Test.log "hello" in
  (1,2)

let test_x = a + a

incorrectly outputs:

"hello"
"hello"
Everything at the top-level was executed.
- test_x exited with value 4.

Description

Changes in AST

For Ast_imperative to Ast_aggregated:

  • Added D_pattern for the let <pattern> = <expr> construct (top-level).
  • Changed E_let_in/E_let_mut_in from let <binder> = <expr> in <expr> to let <pattern> = <expr> in <expr>.

For Ast_expanded to Mini_c:

  • E_let_in/E_let_mut_in denotes the let <binder> = <expr> in <expr> construct.
  • E_matching are decompiled to case expressions (as done before in Self_ast_aggregated)

Abstractors

The old D_value (let <binder> = <expr>) is still used but is now only used for functional values (i.e. function declaration with at least one parameter or one type parameter):

let foo (type a) = <..> (* will emit D_value *)
let foo x = <..> (* will emit D_value *)
let foo (type a) (x:a) = <..> (* will emit D_value *)
let x = <..> (* will emit D_pattern *)
let x = fun x -> <...> (* will emit D_pattern *)
let (a,b) = <...> (* will emit D_pattern *)

(same goes for E_let_mut_in)

In addition to that lhs type annotations on pattern bindings are now propagated to the rhs:

let foo : t = x 

~>

D_pattern { pattern = P_var "foo"; expr = E_ascription { anno_expr = x, type_expression = ty } }

Typing rule

The type system is extended with an additional rule in infer_expression to handle pattern bindings:

\G |- e1 => B  \G |- p <= B  \G, (binders in p) |- e2 => A 
----------------------------------------------------------
         \G |- let p : B = e1 in e2 => A

An equivalent rule is added for let muts and top-level lets.

Decompilation of patterns

Decompilation of patterns (currently in Self_ast_aggregated) was moved to a new pass Expansion.

The only difference from before here is the destructuring of mutable let-patterns, where 'mutable pattern bindings' are first "expanded" as a case expression and then re-bound using let muts, with case bodies vars being replaced by dereferences:

let mut (a, (b, Foo x)) = matchee in 
let () = x := !x + 1 in
!x

~>

match matchee with
| ( a , gen#1 ) ->
  match gen#1 with
  | ( gen#2 , y ) ->
  match gen#2 with
    | Foo x ->
      (* mutables re-bindings *)
      let mut a = a in
      let mut y = y in
      let mut x = x in
      (* end *)
      let () = x := (!x + 1) in
      !x

A side effect of that is the proxy_ticket.jsligo example where we need to change let to consts to help inlining of Mini_c.

Interpreter

As a side effect of pattern decompilation, we now interpret patterns in interpreter.ml. For now, the simplest solution has been chosen (no parallel interpretation). I doubt any performance issues will be raised because of this.

Types of changes

  • Bug fix (non-breaking change which fixes an issue)
  • New feature (non-breaking change which adds functionality)
  • Breaking change (fix or feature that would cause existing functionality to not work as expected)
  • Performance improvement (non-breaking change that improves performance)
  • None (change with no changelog)

Changelog

  • Fix a bug where top-level let destructuring were causing code to be executed multiple time, as in:
let (a,a) =
  let () = Test.log "hello" in
  (1,2)

Checklist:

  • Changes follow the existing coding style (use dune @fmt to check).
  • Tests for the changes have been added (for bug fixes / feature).
  • Documentation has been updated.
  • Changelog description has been added (if appropriate).
  • Examples in changed behaviour have been added to the changelog (for breaking change / feature).
Edited by Rémi

Merge request reports

Loading