Support for naming scrutinee in dependent pattern matching #2464

aseemr · 2022-02-22T09:03:31Z

Dependent pattern matching in F*

PR #2256 added support for dependent pattern matching with returns annotations on match. E.g., from ulib/Steel.ST.EphemeralHashtbl.fst:

let vopt = Seq.index s (U32.v idx) in
match vopt returns STGhostT _ _ _ (fun _ -> tperm a (Map.upd m i c) (Map.remove borrows i)) with ...

However, it comes with a restriction that the scrutinee expression has to be a name in the presence of a returns annotation. As a result, the snippet above has to let-bind the scrutinee expression.

This PR

This PR adds support for naming the scrutinee using as keyword similar to Coq. E.g. the code above can now be written as:

match Seq.index s (U32.v idx) as y returns STGhostT _ _ _ (fun _ -> tperm a (Map.upd m i c) (Map.remove borrows i)) with ...

where y may appear free in the type/computation type after returns.

As an optimization, note that the computation type after returns in the first snippet does not contain vopt, so in this case, we can even write:

match Seq.index s (U32.v idx) returns STGhostT _ _ _ (fun _ -> tperm a (Map.upd m i c) (Map.remove borrows i)) with ...

thereby eliminating the unnecessary naming of the scrutinee.

Code changes

AST, syntax, desugaring, resugaring, reflection

In the parser AST, a returns annotation may now optionally have a ident. Whereas in the core syntax, the returns annotation is of the form (b, asc), where b is a binder and asc is an Syntax.ascription node.

Parser AST returns annotation (x, t) desugars to (x_b, asc), where x_b is a binder for x and t desugars to asc, may be containing the bound variable x_b.

On the other hand, parser AST returns annotation t desugars to (uu___ret_, asc), i.e. we introduce a new binder. One subtlety here is that, it may be the case that source program does not name the scrutinee, but scrutinee is already a name and occurs free in the returns annotation, e.g.:

match x returns Tot (n:int{n > x}) with ...

In this case, when we introduce a new binder uu___ret_, we also substitute x in t with uu___ret_.

That way, core typechecker uniformly works with an explicit binder for the returns annotation.

When resugaring, we check that if the binder name for the returns annotation is the internal name uu___ret_, we do not print it, and appropriately substitute the scrutinee back if necessary. See https://github.com/FStarLang/FStar/blob/aseem_dependent_pattern_matching2/tests/prettyprinting/Match.Returns.fst and https://github.com/FStarLang/FStar/blob/aseem_dependent_pattern_matching2/tests/prettyprinting/Match.Returns.fst.expected for pretty-printing testcases.

Reflection AST, embeddings, and unembeddings are also fixed accordingly.

Typechecker

To typecheck

match e as x returns C with
| P_i -> e_i

We first typecheck G |- e : C_e. Then we typecheck G, x : C_e.t |- C : _, i.e. extend the environment with x:t where t is the type of e and typecheck C. Then we ascribe each branch as e_i <: C[P_i/x], and typecheck the ascribed branch. The final type of the match result is computed as C[e/x] (as usual we later bind it with C_e).

…ation

aseemr · 2022-02-22T09:46:45Z

src/typechecker/FStar.TypeChecker.TcTerm.fs


-        TcUtil.bind_cases env t cases guard_x, g, erasable
+        //c has b free, so substitute it with the scrutinee
+        let c = SS.subst_comp [NT (b.binder_bv, e1)] c in


This is where we compute the type of the match result by substituting binder with e1.

aseemr · 2022-02-22T09:50:34Z

src/typechecker/FStar.TypeChecker.TcTerm.fs

+          let bs, asc = SS.open_ascription [b] asc in
+          let b = List.hd bs in
+          //we set the sort of the binder to be the type of e1
+          {b with binder_bv={b.binder_bv with sort=c1.res_typ}}, asc in


Adding the returns binder with sort as the type of e1, to typecheck the ascription.

aseemr · 2022-02-22T09:51:26Z

src/typechecker/FStar.TypeChecker.TcTerm.fs

+        | Some (b, asc) ->
+          let asc = SS.close_ascription [b] asc in
+          let b = List.hd (SS.close_binders [b]) in
+          let b = {b with binder_bv={b.binder_bv with sort=tun}} in


While packing the returns annotation back, set the sort to _. So we don't have to normalize it, instantiate it, compute its fvs etc. etc.

interesting ... nice trick

aseemr · 2022-02-22T09:52:06Z

src/typechecker/FStar.TypeChecker.TcTerm.fs

        asc
-        |> SS.subst_ascription [NT (scrutinee, norm_pat_exp)]
+        |> SS.subst_ascription [NT (b.binder_bv, norm_pat_exp)]


Ascribe the branches before checking them.

nikswamy · 2022-02-22T18:50:16Z

src/parser/FStar.Parser.Lexhelp.fs

@@ -173,6 +173,7 @@ let keywords =
    ALWAYS, "let"        ,LET(false);
    ALWAYS, "logic"      ,LOGIC;
    ALWAYS, "match"      ,MATCH;
+    ALWAYS, "as"         ,AS;


super tiny nit, sorry. But this list of keywords was originally meant to be in alphabetical order. I see there are some deviations from that already, but may be worth restoring at some point.

nikswamy · 2022-02-22T19:09:03Z

src/parser/FStar.Parser.ToDocument.fs

+                             ((p_noSeqTermAndComment false false e) ^/+^
+                              (match as_opt with
+                               | None -> empty
+                               | Some as_ident -> str " as" ^/+^ (p_ident as_ident)) ^/+^


do we need the preceding " " in as?

Thanks for noticing! I removed these extra spaces and updated the pretty printing tests.

nikswamy · 2022-02-22T19:09:29Z

src/parser/FStar.Parser.ToDocument.fs

-                (str "ret" ^/+^ p_tmIff ret) ^/^
+                ((match as_opt with
+                  | None -> empty
+                  | Some as_ident -> str " as " ^/^ p_ident as_ident ^/^ str " ")


same as below ... do we need the spaces around it?

nikswamy · 2022-02-22T19:10:13Z

tests/prettyprinting/Match.Returns.fst.expected

@@ -1,22 +1,32 @@
 module Match.Returns

 let test (n: nat) =
-  match n returns nat with
+  match n  returns nat with


I wonder if this extra space will disappear with some tuning in ToDocument

nikswamy · 2022-02-22T19:11:41Z

ulib/FStar.Tactics.Print.fst

+  match ret_opt with
+  | None -> ""
+  | Some (b, asc) ->
+    (binder_to_string b ^ " ")


missing an as here?

This is simply printing the AST, e.g. Tm_match is already printed as (scrutinee, branches), so I followed the same style (e.g. no returns as well).

nikswamy · 2022-02-22T19:12:19Z

ulib/LowStar.BufferView.Down.fst

@@ -78,12 +78,12 @@ let indexing' (#a #b: _) (v:view a b) (len_as:nat) (i:nat{i < len_as * View?.n v
 let indexing #b vb i = indexing' (get_view vb) (B.length (as_buffer vb)) i

 let sel' (#a #b: _) (v:view a b)
-         (as:Seq.seq a)
-         (i:nat{i / View?.n v < Seq.length as})
+         (es:Seq.seq a)


thanks for all the fixes in this file!

nikswamy · 2022-02-22T19:13:20Z

ulib/experimental/Steel.ST.EphemeralHashtbl.fst

-                              _
-                              _
-                              (fun _ -> tperm a (Map.upd m i c) (Map.remove borrows i)) with
+  match Seq.index s (U32.v idx)


nikswamy · 2022-02-22T19:20:15Z

Thanks Aseem.. This looks great! Thanks for all the explanations and code comments in TcTerm too.

I left a few minor nit-picky comments.

aseemr · 2022-02-23T05:09:02Z

Thanks for the review Nik! I incorporated the comments, except the alphabetical sorting of keywords in the lexer(s). I will raise an enhancement issue for that.

aseemr added 23 commits February 22, 2022 05:27

AST support for optionally naming scrutinee in returns annotation

c34fc48

Parsing and lexing the returns name

f172de9

syntax changes for returns name

3568c17

substitution for match returns annotations

b206901

propagating syntax change to syntax/

d677617

resugar match returns, trying to maintain source code closeness

8028726

propagating AST changes in parser/

380cc25

claiming the as keyword from its existing uses in ulib

c575180

reflection: reflecting syntax change

0f4dd61

changes in reflection embeddings for match returns

027a14b

reflection changes for match returns ascription in ulib/

40036ce

desugar match returns annotation

8a067b3

normalization of the match returns ascription

c4a02be

nbe term syntax changes for match returns

0e6b213

NBE normalization for match returns with name

981d0a6

revising typechecking of Tm_match to account for named returned annot…

ba7cd18

…ation

using named returns annotation support

7819463

as is a keyword now

d788aaf

snap

c6261e7

Merge branch 'master' of github.com:FStarLang/FStar

e0e9764

a couple of pretty printing tests

50a6799

checked file version

29e982d

CHANGES.md

5b1a71b

aseemr mentioned this pull request Feb 22, 2022

Renaming variables named as hacl-star/hacl-star#530

Merged

F#?

fbde336

aseemr commented Feb 22, 2022

View reviewed changes

error if returns annotation is present, and the scrutinee is impure

b99f3a9

aseemr added 3 commits February 22, 2022 11:23

snap

703bc46

tests

de2cf53

nit

7dedc5a

nikswamy reviewed Feb 22, 2022

View reviewed changes

aseemr added 5 commits February 23, 2022 04:11

Merge branch 'master' into aseem_dependent_pattern_matching2

9673ea6

comment

95c5969

removing a few unnecessary spaces

029d1f0

a test of returns annotation with if

84e69b1

snap

8be114d

aseemr merged commit c231357 into master Feb 23, 2022

aseemr mentioned this pull request Mar 13, 2022

Adding returns annotation to projectors #2466

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Support for naming scrutinee in dependent pattern matching #2464

Support for naming scrutinee in dependent pattern matching #2464

aseemr commented Feb 22, 2022 •

edited

Loading

aseemr Feb 22, 2022

aseemr Feb 22, 2022

aseemr Feb 22, 2022

nikswamy Feb 22, 2022

aseemr Feb 22, 2022

nikswamy Feb 22, 2022

nikswamy Feb 22, 2022

aseemr Feb 23, 2022

nikswamy Feb 22, 2022

nikswamy Feb 22, 2022

nikswamy Feb 22, 2022

aseemr Feb 23, 2022

nikswamy Feb 22, 2022

nikswamy Feb 22, 2022

nikswamy commented Feb 22, 2022

aseemr commented Feb 23, 2022

Support for naming scrutinee in dependent pattern matching #2464

Support for naming scrutinee in dependent pattern matching #2464

Conversation

aseemr commented Feb 22, 2022 • edited Loading

Dependent pattern matching in F*

This PR

Code changes

AST, syntax, desugaring, resugaring, reflection

Typechecker

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

nikswamy commented Feb 22, 2022

aseemr commented Feb 23, 2022

aseemr commented Feb 22, 2022 •

edited

Loading