Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Frontend support for language extension with #lang-X #3363

Merged
merged 18 commits into from
Jul 21, 2024
Merged

Frontend support for language extension with #lang-X #3363

Show file tree
Hide file tree
Changes from 10 commits
Commits
Show all changes
18 commits
Select commit Hold shift + click to select a range
0682aaf
changes in preparation for #lang-<ext>
nikswamy Jul 18, 2024
6879011
Merge remote-tracking branch 'origin/master' into nik_use_lang
nikswamy Jul 18, 2024
c9cba30
supporting for #lang-X, with some unit tests; also works for #lang-pulse
nikswamy Jul 18, 2024
c78bdc4
Merge remote-tracking branch 'origin/master' into nik_use_lang
nikswamy Jul 18, 2024
6b97853
support for detecting the current file in the IDE, and an Unparseable…
nikswamy Jul 18, 2024
b4b804a
allow desugared blobs to be compared with a callback
nikswamy Jul 18, 2024
5b32f96
support for syntax extension to offer their own dependence scanning
nikswamy Jul 19, 2024
a7b9123
remove dump module in parser.driver (debugging)
nikswamy Jul 19, 2024
1edff2f
mistakenly commented out some unit tests
nikswamy Jul 19, 2024
648d685
snap
nikswamy Jul 19, 2024
7c1bc74
backwards compat for fstar-mode.el use of Push operations in ide mode…
nikswamy Jul 19, 2024
afe6ca4
stashing open namespaces and module abbrevs in the repl_lang state fo…
nikswamy Jul 20, 2024
efad29a
Merge remote-tracking branch 'origin/master' into nik_use_lang
nikswamy Jul 20, 2024
fe1e92e
remove stray debugging message
nikswamy Jul 20, 2024
fa29b7d
exporting parser productons for decls with and without decorations
nikswamy Jul 20, 2024
f84799b
simplifying desugaring of extension code, passing desugaring environm…
nikswamy Jul 20, 2024
53d4a50
fix interleaving splices; fix handling of typeclass decorations
nikswamy Jul 20, 2024
3e1a61c
remove explicit passing of open namespaces to extension_lang parsers;…
nikswamy Jul 20, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
26 changes: 26 additions & 0 deletions ocaml/fstar-lib/FStar_Parser_LexFStar.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -261,6 +261,7 @@ let maybe_trim_lines start_column comment =

let comment_buffer = Buffer.create 128
let blob_buffer = Buffer.create 128
let use_lang_buffer = Buffer.create 128

let start_comment lexbuf =
Buffer.add_string comment_buffer "(*" ;
Expand Down Expand Up @@ -452,6 +453,15 @@ match%sedlex lexbuf with
| "`%" -> BACKTICK_PERC
| "`#" -> BACKTICK_HASH
| "`@" -> BACKTICK_AT
| "#lang-", ident -> (
let s = L.lexeme lexbuf in
let lang_name = BatString.lchop ~n:6 s in
let snap = Sedlexing.snapshot lexbuf in
Buffer.clear use_lang_buffer;
let pos = L.current_pos lexbuf in
use_lang_blob snap lang_name pos use_lang_buffer lexbuf
)

| "#set-options" -> PRAGMA_SET_OPTIONS
| "#reset-options" -> PRAGMA_RESET_OPTIONS
| "#push-options" -> PRAGMA_PUSH_OPTIONS
Expand Down Expand Up @@ -686,6 +696,22 @@ match %sedlex lexbuf with
uninterpreted_blob snap name pos buffer lexbuf
| _ -> assert false

and use_lang_blob snap name pos buffer lexbuf =
match %sedlex lexbuf with
| "#end-lang" ->
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What do you think about ending an extension block with #lang-fstar (or #lang-pulse for that matter)?

I wonder if it is feasible for the extension parser/lexer to call back into the main parser. That is, if we could just add a #lang- rule to the pulse grammer?

One disadvantage of detecting the end of the extension block here is that it is unaware of the lexical syntax of the extension language (namely string literals and comments).

#lang-pulse

(*
We can exit a pulse block like this:
#end-lang
*)

fn foo () requires emp returns _: string ensures emp {
  "This is how you end a pulse extension block:
#end-lang
Everything after that is F* again."
}

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Or an optional #end-lang-X to match a #lang-X?

The extension parser for Pulse does call back into the F* parser and lexer. So, it can, in principle, handle a nested #lang-x ... #end-lang-x block

The disadvantage you mentioned remains, but I guess it's not so bad ... you should be aware of the placement of the end-lang block.

That said, for Pulse itself, I don't see any reason to actually end the #lang-pulse block. Do you?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What I'm suggesting is that #lang-foo means "parse the rest of the file using Foo." And then the parser for Foo could have the same command, calling back to the main parser.

#lang-pulse

fn foo () requires emp ensures emp { () }

// not really necessary, as you point out
#lang-fstar

let bar = 42

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Right, this works. You can even do

#lang-pulse
fn stuff ...
#lang-pulse
fn more stuff

And it will recursively call back into the Pulse parser for the second block

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I also registered an #lang-fstar parser and removed #end-lang

USE_LANG_BLOB(name, Buffer.contents buffer, pos, snap)
| eof ->
L.rollback lexbuf; (* leave the eof to be consumed later *)
USE_LANG_BLOB(name, Buffer.contents buffer, pos, snap)
| newline ->
L.new_line lexbuf;
Buffer.add_string buffer (L.lexeme lexbuf);
use_lang_blob snap name pos buffer lexbuf
| any ->
Buffer.add_string buffer (L.lexeme lexbuf);
use_lang_blob snap name pos buffer lexbuf
| _ -> assert false

and ignore_endline lexbuf =
match%sedlex lexbuf with
| Star ' ', newline -> token lexbuf
Expand Down
36 changes: 28 additions & 8 deletions ocaml/fstar-lib/FStar_Parser_Parse.mly
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -58,6 +58,13 @@ let parse_extension_blob (extension_name:string)
(extension_syntax_start:range) : FStar_Parser_AST.decl' =
DeclSyntaxExtension (extension_name, s, blob_range, extension_syntax_start)

let parse_use_lang_blob (extension_name:string)
(s:string)
(blob_range:range)
(extension_syntax_start:range)
: FStar_Parser_AST.decl list
= FStar_Parser_AST_Util.parse_extension_lang extension_name s extension_syntax_start

%}

%token <string> STRING
Expand Down Expand Up @@ -129,6 +136,7 @@ let parse_extension_blob (extension_name:string)
%token<string> OPPREFIX OPINFIX0a OPINFIX0b OPINFIX0c OPINFIX0d OPINFIX1 OPINFIX2 OPINFIX3 OPINFIX4
%token<string> OP_MIXFIX_ASSIGNMENT OP_MIXFIX_ACCESS
%token<string * string * Lexing.position * FStar_Sedlexing.snap> BLOB
%token<string * string * Lexing.position * FStar_Sedlexing.snap> USE_LANG_BLOB

/* These are artificial */
%token EOF
Expand Down Expand Up @@ -157,7 +165,7 @@ let parse_extension_blob (extension_name:string)
%start warn_error_list
%start oneDeclOrEOF
%type <FStar_Parser_AST.inputFragment> inputFragment
%type <(FStar_Parser_AST.decl * FStar_Sedlexing.snap option) option> oneDeclOrEOF
%type <(FStar_Parser_AST.decl list * FStar_Sedlexing.snap option) option> oneDeclOrEOF
%type <FStar_Parser_AST.term> term
%type <FStar_Ident.ident> lident
%type <(FStar_Errors_Codes.error_flag * string) list> warn_error_list
Expand All @@ -167,7 +175,7 @@ let parse_extension_blob (extension_name:string)
inputFragment:
| decls=list(decl) EOF
{
as_frag decls
as_frag (List.flatten decls)
}

oneDeclOrEOF:
Expand All @@ -178,7 +186,7 @@ idecl:
| d=decl snap=startOfNextDeclToken
{ d, snap }


%public
startOfNextDeclToken:
| EOF { None }
| pragmaStartToken { None }
Expand All @@ -204,7 +212,7 @@ startOfNextDeclToken:
| POLYMONADIC_BIND { None }
| POLYMONADIC_SUBCOMP { None }
| b=BLOB { let _, _, _, snap = b in Some snap }

| b=USE_LANG_BLOB { let _, _, _, snap = b in Some snap }

pragmaStartToken:
| PRAGMA_SET_OPTIONS
Expand Down Expand Up @@ -259,17 +267,29 @@ decoration:
| x=qualifier
{ Qualifier x }

%public
decl:
| ASSUME lid=uident COLON phi=formula
{ mk_decl (Assume(lid, phi)) (rr $loc) [ Qualifier Assumption ] }
{ [mk_decl (Assume(lid, phi)) (rr $loc) [ Qualifier Assumption ]] }

| blob=USE_LANG_BLOB
{
let ext_name, contents, pos, snap = blob in
(* blob_range is the full range of the blob, starting from the #lang pragma *)
let blob_range = rr (snd snap, snd $loc) in
(* extension_syntax_start_range is where the extension syntax starts not including
the "#lang ident" prefix *)
let extension_syntax_start_range = (rr (pos, pos)) in
parse_use_lang_blob ext_name contents blob_range extension_syntax_start_range
}

| ds=list(decoration) decl=rawDecl
{ mk_decl decl (rr $loc(decl)) ds }
{ [mk_decl decl (rr $loc(decl)) ds] }

| ds=list(decoration) decl=typeclassDecl
{ let (decl, extra_attrs) = decl in
let d = mk_decl decl (rr $loc(decl)) ds in
{ d with attrs = extra_attrs @ d.attrs }
[{ d with attrs = extra_attrs @ d.attrs }]
}

typeclassDecl:
Expand Down Expand Up @@ -374,7 +394,7 @@ rawDecl:
let ext_name, contents, pos, snap = blob in
(* blob_range is the full range of the blob, including the enclosing ``` *)
let blob_range = rr (snd snap, snd $loc) in
(* extension_syntax_start_range is where the extension syntax starts not incluing
(* extension_syntax_start_range is where the extension syntax starts not including
the "```ident" prefix *)
let extension_syntax_start_range = (rr (pos, pos)) in
parse_extension_blob ext_name contents blob_range extension_syntax_start_range
Expand Down
Loading
Loading