QuasiQuotes for F*

[W95Psp]

Hi,

This (draft) PR adds some support for quasi-quotes in F*, with a syntax similar to Haskell's quasi-quotes. It's quite experimental for now, and I wanted to have some feedback about whether this would be an interesting feature to have or not in F*.

Basically, the syntax [foo|anything|] calls the F* meta-program foo with the body anything. The quasiquote body anything consists in a sequence of interleaved (1) raw arbitrary characters or (2) F* quotations.

foo is a function that takes as an input a Tac computation producing an heterogeneous list of terms and string. For example, [foo|hello `name!|] is (more or less) desugared to foo (fun () -> ["hello "; quote name; "!"]).

Quasi-quotes allows for quite flexible & custom used-defined domain-specific syntax.

Examples

Template literals (or string interpolation)

The file examples/quasiquotes/TemplateLiterals.fst defines a quasiquoter that allows the following:

let simple = 
  let x = 1 in
  let y = 2 in
  let z = "hello" in
  [str|list=`[x;y] x=`x, y=`y rev=`(rev [x;y]), and z is `z|]

This normalizes to the string "list=[1, 2] x=1, y=2 rev=[2, 1], and z is hello".

List comprehension

Using string_to_term from PR #2260 (~that I should revive!~) and a parser library, it's pretty easy to define a (user-land) list comprehension syntax (à la Haskell) for F*. For instance, the following typechecks:

open FStar.Mul
let bar = 
  [ Inl 1 ; Inl 2 ; Inl 3 ; Inl 4 ; Inl 5
  ; Inr 11; Inr 12; Inr 13; Inr 14; Inr 15 ]
let example = [lc| x,y | Inl x <- bar, x > 1,
                         let x = x * 1000,
                         Inr y <- bar, y % 2 = 0 |]
let _ = assert_norm ( 
     example
  == [ (2000, 12); (2000, 14); (3000, 12)
     ; (3000, 14); (4000, 12); (4000, 14)
     ; (5000, 12); (5000, 14)
     ])

Other

QQ can be useful for DSLs, for debugging purposes, for FFIs, etc.

Details and quirks

My current implementation of QQ in F* is quite experimental and have a few quirks.

Lexing

Quasiquotes require the lexer to be a bit contextual: when lexing inside a quasiquote, every chunk of characters that contains no quotation should be lexed as one big token. Quasiquotes can also be nested.

Desugaring

For now, I desguar QQ directly as regular terms right within the parser, which is not really nice. Though it's quite easy to add a constructor to F*'s AST.

Synthetizing polymorphic QQs

The quasiquote [foo|body|] is actually desugared into foo transformed_body ().

The extras () are there because of polymorphism. Consider the list comprehension quasiquote: it is polymorphic in the type of the list to be constructed. To be able to synthetize values of "tactic-decided" types, I use the following construction:

noeq type quasiquoter = {
  t: Type u#t;
  process: list (either string term) -> Tac t;
  make_type:  t -> Tac unit;
  make_value: t -> Tac unit;
}

let synth_quasiquote
    (qq: quasiquoter u#qq)
    (input: unit -> Tac (list (either string term)))
    (#[(let data = qq.process (input ()) in 
        exact (quote data))] data : qq.t)
    (#[qq.make_type data]    typ  : Type u#t)
    (#[qq.make_value data]   value:  typ)
    ()
    = value

With this definition, a quasiquote first parses and process its inputs with process. synth_quasiquote runs process on some inputs via the meta-argument data, then produces some typ and value. If I omit the last unit parameter, I get a Variable "data#..." not found on qq.make_type data.

Ranges

Ranges are not translated correctly in many cases within quasiquotes, so that's something else to fix.

Patterns and names in general

Introducing names (e.g. something à la Coq like [tac| intro [a | b] h. |]; something a) or translating quasiquotes to patterns (i.e. match Plus 1 2 with | [mydsl|x + y|] -> … x … y | …) seems impossible to me currently, since this would require incremental desugaring: if I'm not mistaking.

TODO

• [ ] Fix ranges translation
  • [x] revive PR #2188
• [ ] Clean up the lexer
• [ ] Move desugaring from the parser to the desugaring phase
  • [ ] add QuasiQuote node to FStar.Parser.AST
• [x] revive #2260

[nikswamy]

Wow! This is really cool. It would be great to have something like this. Can we discuss it more broadly in one of our upcoming F* dev meetings?

[W95Psp]

Nice then :) Yes, sure, I would be glad to!