Support for dependent pattern matching #2256

aseemr · 2021-03-19T09:05:20Z

Overview

This PR introduces support for dependent pattern matching in F*. With SMT support available in deciding the relations between types, we haven't felt much need for it. However, in Steel like DSLs where typing relations are mostly handled using unification, we have been working around using handwritten cond combinator (that too only for boolean), and using them. For example, Steel.Effect.fsti defines:

val cond (#a:Type)
         (b:bool)
         (p: bool -> slprop)
         (q: bool -> a -> slprop)
         (then_: (unit -> SteelT a (p true) (q true)))
         (else_: (unit -> SteelT a (p false) (q false)))
  : SteelT a (p b) (q b)

which is then used in Steel.Primitive.ForkJoin as follows:

 cond b (pre t) (post p) (join_case_true t) (join_case_false t (join #p))

where join_case_true and join_case_false are hoisted to the top-level to get better unification etc.

With this PR, we can now annotate match and if with a returning annotation that supplies a computation type, and get the same effect. So the code in Steel.Primitive.ForkJoin can now be written as 6b94c39.

How does it work

When typechecking

match x returns C with
| P_i -> e_i

where C is a computation type annotation, we typecheck e_i as:

G, x |- e_i <: C[P_i/x]

I.e. with an expected computation type C where the scrutinee x has been substituted by the pattern P_i. After typechecking the branches, the final computation type for the match expression is C.

In our small example above, we will typecheck the then branch with expected computation type as (St b)[true/b] i.e. St true, and similarly for the else branch. The computed and expected computation types for the branches are then syntactically same, and hence no smt is required.

Syntax etc.

Both match and if can now be optionally annotated with returns C or returns t:

if e returns C then e1 else e2

and

match e returns C with | P-i -> e_i

Enhancements

While the current PR state is enough for examples such as Steel.Primitive.ForkJoin, it can be enhanced on the lines of as and in annotations in Coq.

Right now we enforce that if you are using returning annotation, the scrutinee must be a variable. This restriction can go with an as annotation.
To get more help from inductive type indices, we could also add the support for in annotations.
Syntax discussions

aseemr · 2021-03-29T06:01:49Z

src/typechecker/FStar.TypeChecker.TcTerm.fs

@@ -1004,32 +1004,89 @@ and tc_maybe_toplevel_term env (e:term) : term                  (* type-checked
    check_inner_let_rec env top

 and tc_match (env : Env.env) (top : term) : term * lcomp * guard_t =
+


cc @nikswamy , the main change in the PR

nikswamy · 2021-03-29T18:58:25Z

src/reflection/FStar.Reflection.Basic.fs

@@ -208,7 +208,7 @@ let rec inspect_ln (t:term) : term_view =
        | BU.Inl bv -> Tv_Let (true, lb.lbattrs, bv, lb.lbdef, t2)
        end

-    | Tm_match (t, brs) ->
+    | Tm_match (t, _, brs) ->  //AR: TODO: expose the annotation in the reflection API


Would be great to address this now, otherwise we'll forget and not do it until a user complains about it

nikswamy · 2021-03-29T19:00:02Z

src/syntax/FStar.Syntax.Print.fs

+          (match asc_opt with
+           | None -> ""
+           | Some (asc, tacopt) ->
+             U.format2 "ret %s%s "


Fixed, thanks for the catch!

…n API

…s properly

…e interface

nikswamy · 2021-03-31T20:51:20Z

src/typechecker/FStar.TypeChecker.TcTerm.fs

-        Env.set_expected_typ env res_t, res_t, Env.conj_guard g1 g in
+  | Tm_match(e1, ret_opt, eqns) ->  //ret_opt is the return annotation
+    let e1, c1, g1 = tc_term
+      ({(env |> Env.clear_expected_typ |> fst) with instantiate_imp = true})


May be a bit more abstract to write it as

env |> Env.clear_expected_typ |> fst |> instantiate_both

?

Done, thanks!

nikswamy · 2021-03-31T20:54:59Z

src/typechecker/FStar.TypeChecker.TcTerm.fs

+      | Some (t_or_c, None) ->
+        //typecheck the return annotation and unset expected type in the env if exists
+        //the branch typechecking (tc_eqn) will typecheck the branch with an ascription
+        let env, _ = Env.clear_expected_typ env in


Shouldn't we check that if an expected type is set in the environment, then the type in the returns annotation is compatible with the environment's expected type?

Otherwise, I wonder what would happen if we had something like

(match x returns t with ...) <: t'

We do it at the end of tc_match, I have also added a comment here to that effect.

nikswamy · 2021-03-31T21:06:19Z

src/typechecker/FStar.TypeChecker.TcTerm.fs

+      | Some asc ->
+        asc
+        |> SS.subst_ascription [NT (scrutinee, norm_pat_exp)]
+        |> U.ascribe branch_exp in


Rather than adding an ascription node and then removing it, couldn't we just set the Env.expected_typ?

Some pros/cons:

That would mean we don't disturb the syntax of the term to typecheck it

We don't re-typecheck the annotated returns clause

But, currently, we only support Env.expected_typ rather than Env.expected_effect. Can we add support for Env.expected_comp_type so that we can handle both cases of a returns annotation?

Yes, agreed, would be great to have Env.expected_comp. As we discussed offline, we can take it up separately.

…to aseem_dependent_match

aseemr added 6 commits March 19, 2021 08:21

parser changes for option return annotation on match and if

ef38627

syntax changes for keeping return annotation with match and if

ef26a9c

desugar return annotations

452c43a

typechecking using the match returns

80fcc9e

removing the use of cond combinator in ForkJoin

6b94c39

snap

902cb1e

aseemr requested a review from nikswamy March 19, 2021 09:05

aseemr mentioned this pull request Mar 19, 2021

Steel work items #2243

Open

48 tasks

aseemr added 19 commits March 19, 2021 11:24

removing all uses of cond using dependent pattern matching

047ea32

API to substitute in the ascriptions

460303d

reworking return annotations on matches, support for types as well

21c1178

snap

f66754c

substitute scrutinee bv back in the exhaustiveness guard

ad265c4

snap

e94a166

Merge branch 'master' into aseem_dependent_match

6d34974

some tweaks

1a1c20b

snap

76aef91

some comments and cleanup

79c98a6

snap

9b42f5f

nit

83d920b

printing tests

2aab421

correcting ranges in the parser

e74f54d

accept an error messages test (uvar name differs)

9ccf8c4

Merge branch 'master' into aseem_dependent_match

0ad79e6

use returns

af69890

update examples

4576964

snap

966c6ad

aseemr commented Mar 29, 2021

View reviewed changes

nikswamy reviewed Mar 29, 2021

View reviewed changes

aseemr and others added 19 commits March 30, 2021 11:15

merge with master

cc304dc

snap

3b48b43

tweaks

2aac74b

typechecker changes for exporting returns annotation in the reflectio…

8dafe7f

…n API

ulib changes for exporting returns annotation in the reflection API

4700a17

snap

f32ad9b

retaining returns annotation in NBE

a811bbd

snap

c2c5148

nit

2c0eb09

adding testcases for pretty printing match with returns annotation

dc7dbff

tweak printing of returns annotation

bea446a

another testcase with parenthesis

a47ca8c

Merge branch 'master' into aseem_dependent_match

1548098

when the returns annotation is a comp, still need to weaken the guard…

bb1553c

…s properly

hoisting branch condition computation to top-level and exposing in th…

1cb956e

…e interface

bump up checked file version

ff5b1f7

removing either type from FStar.Util, using from FStar.Pervasives

7c4237e

restoring F# build after moving either to FStar.Pervasives

7526349

adding FStar.Pervasives to parse.fsy

65c5653

nikswamy reviewed Mar 31, 2021

View reviewed changes

aseemr added 6 commits April 1, 2021 04:54

Review comment from Nik

75ac173

examples tweaks for change to the reflection API

1017e74

Merge branch 'aseem_dependent_match' of github.com:FStarLang/FStar in…

0311496

…to aseem_dependent_match

CHANGES.md

ddbf86b

another example

d82e516

test accept

18f787c

aseemr merged commit 18f787c into master Apr 1, 2021

aseemr mentioned this pull request Feb 22, 2022

Support for naming scrutinee in dependent pattern matching #2464

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Support for dependent pattern matching #2256

Support for dependent pattern matching #2256

aseemr commented Mar 19, 2021 •

edited

Loading

aseemr Mar 29, 2021

nikswamy Mar 29, 2021

aseemr Mar 31, 2021

nikswamy Mar 29, 2021

aseemr Mar 31, 2021

nikswamy Mar 31, 2021 •

edited

Loading

aseemr Apr 1, 2021

nikswamy Mar 31, 2021

aseemr Apr 1, 2021

nikswamy Mar 31, 2021

aseemr Apr 1, 2021

		@@ -1004,32 +1004,89 @@ and tc_maybe_toplevel_term env (e:term) : term (* type-checked
		check_inner_let_rec env top

		and tc_match (env : Env.env) (top : term) : term * lcomp * guard_t =

Support for dependent pattern matching #2256

Support for dependent pattern matching #2256

Conversation

aseemr commented Mar 19, 2021 • edited Loading

Overview

How does it work

Syntax etc.

Enhancements

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 Mar 31, 2021 • edited Loading

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

aseemr commented Mar 19, 2021 •

edited

Loading

nikswamy Mar 31, 2021 •

edited

Loading