View patterns (but also as-pattern & pattern guards)

[W95Psp]

Hi,

Chatting with @theolaurent a while back, he had a nice idea: implementing view patterns in F*.

It's a pretty nice feature, that could especially be useful for meta-programming (so that we can pattern-match nested terms inspecting on the fly its nested term_views). But it also gives us for free:

1. pattern matching on non-inductive structures / abstract datatypes
2. as-patterns,
3. if/when clauses (since F* when clauses are basically disabled),
4. disjunctive patterns,
5. fancy pattern matching on lists (or anything that has a prefix/suffix),
6. ranges of integers (or ranges of anything, actually).

This PR is still quite draft, I just wrote it quickly during this week-end, some part are really ugly. The SMT encoding I wrote for those view patterns is fairly broken (in interactive mode it yields errors, but retrying a code block make it pass).
There's a lot of room for improvement, but I wanted to get some feedback anyway, before spending more time on it.

Examples

1. Matching on abstract data types

Example of pattern matching deeply in terms:

// this code is a bit of a lie, there are some issues with term/term_view coercions currently
let string_of_fv (f: fv): string = implode_qn (inspect_fv f)
let foo (x: int) = x
let extract_foo_int_payload t 
  = match inspect_ln t with
  | Tv_App ((Tv_FVar (`%foo <- string_of_fv)) <- inspect_ln')
           ((Tv_Const (C_Int n))) <- inspect_ln', _) -> Some n
  | _ -> None

Other applications: matching over types defined in external OCaml libraries (e.g. yojson), data structures with multiple views (e.g. graphs stored as adjacency matrixes but consumed as adjacency lists)...

2. As-patterns

Example of as-patterns:

let y = match [[1;2];[3]] with
  | ((1::_) as hello) :: _ -> 0::hello
  | ((2::_) as hello) :: _ -> 1::hello
  | _ -> []

3. If clauses

Example of if clauses (this is a bit silly to have both when and if, it's just for demo purposes):

let z = match Some 5 with
  | Some (x if (x > 3)) -> x
  | Some x -> 3
  | _ -> 0

4. Disjunctive patterns

let disj1 (x: list (either int int)) = match x with
    | [(Inl a | Inr a); (Inl b | Inr b); (Inl c | Inr c)] -> a + b + c
    | _ -> 0
// or even, combine a if clause (note the `if` applies only to the [Inr] case)
let disj3 (x: list (either int int)) = match x with
    | [(Inl a | Inr a); (Inl b | Inr b if (b < 10))] -> a + b
    | _ -> 0
let _ = assert_norm (disj3 [Inl 5; Inl 20] == 25)
let _ = assert_norm (disj3 [Inl 5; Inr 20] == 0)

5. Fancy pattern matching on lists

let dotdot = match [10;2; 999; 888; 3;4] with
  | (Some ((a,b), middle, (c,d))) <- (fun (l: list int) -> 
         match l with
       | a::b::((middle, [c;d]) <- (splitAt_rev 2)) -> 
         Some ((a, b), [0], (c, d))
       | _ -> None
    ) -> a + b + c + d
  // we could easily have syntax like:
  // | [a;b; ...; c; d] -> a + b + c + d
  | _ -> 0
let _ = assert_norm (dotdot == 10 + 2 + 3 + 4)

6. Ranges

let range (a:int) (b:int): int -> bool = fun x -> x >= a && x <= b
let x y = match [y] with
  | [((true <- (range 0 4)) | (true <- (range 6 10))) as n] -> n + 100
  // we could add the syntax:
  // | [(0..4 | 6..10) as n] -> n + 100
  | _ -> 1

There are more examples in examples/misc/ViewPatterns.fst.

---

What do you think about adding that to F*?

[karthikbhargavan]

What is the status on this? It looks very useful!