Skip to content

Commit

Permalink
Merge pull request #3378 from FStarLang/gebner_parens
Browse files Browse the repository at this point in the history 
Do not require parentheses for fun/assume/assert
  • Loading branch information
@gebner
gebner authored Sep 4, 2024
2 parents a4c6ba1 + 9d66edc commit a2e12be
Show file tree
Hide file tree
Showing 3 changed files with 99 additions and 43 deletions.
114 changes: 72 additions & 42 deletions ocaml/fstar-lib/FStar_Parser_Parse.mly
View file
Original file line number Diff line number Diff line change
Expand Up @@ -145,6 +145,11 @@ let parse_use_lang_blob (extension_name:string)
%nonassoc THEN
%nonassoc ELSE

%nonassoc ASSERT
%nonassoc EQUALTYPE
%nonassoc SUBTYPE
%nonassoc BY

%right COLON_COLON
%right AMP

Expand Down Expand Up @@ -880,7 +885,7 @@ thunk2(X):
mk_term (Abs ([mk_pattern (PatWild (None, [])) (rr $loc)], t)) (rr $loc) Expr }

ascribeTyp:
| COLON t=tmArrow(tmNoEq) tacopt=option(BY tactic=thunk(atomicTerm) {tactic}) { t, tacopt }
| COLON t=tmArrow(tmNoEq) tacopt=option(BY tactic=thunk(trailingTerm) {tactic}) { t, tacopt }

(* Remove for stratify *)
ascribeKind:
Expand Down Expand Up @@ -922,14 +927,23 @@ match_returning:
%public
noSeqTerm:
| t=typ { t }
| e=tmIff SUBTYPE t=tmIff tactic_opt=option(BY tactic=thunk(typ) {tactic})
{ mk_term (Ascribed(e,{t with level=Expr},tactic_opt,false)) (rr2 $loc(e) $loc(tactic_opt)) Expr }
| e=tmIff EQUALTYPE t=tmIff tactic_opt=option(BY tactic=thunk(typ) {tactic})
| e=tmIff SUBTYPE t=tmIff
{ mk_term (Ascribed(e,{t with level=Expr},None,false)) (rr $loc(e)) Expr }
| e=tmIff SUBTYPE t=tmIff BY tactic=thunk(typ)
{ mk_term (Ascribed(e,{t with level=Expr},Some tactic,false)) (rr2 $loc(e) $loc(tactic)) Expr }
| e=tmIff EQUALTYPE t=tmIff
{
log_issue_text (rr $loc)
(Warning_BleedingEdge_Feature,
"Equality type ascriptions is an experimental feature subject to redesign in the future");
mk_term (Ascribed(e,{t with level=Expr},None,true)) (rr $loc(e)) Expr
}
| e=tmIff EQUALTYPE t=tmIff BY tactic=thunk(typ)
{
log_issue_text (rr $loc)
(Warning_BleedingEdge_Feature,
"Equality type ascriptions is an experimental feature subject to redesign in the future");
mk_term (Ascribed(e,{t with level=Expr},tactic_opt,true)) (rr2 $loc(e) $loc(tactic_opt)) Expr
mk_term (Ascribed(e,{t with level=Expr},Some tactic,true)) (rr2 $loc(e) $loc(tactic)) Expr
}
| e1=atomicTermNotQUident op_expr=dotOperator LARROW e3=noSeqTerm
{
Expand Down Expand Up @@ -1010,20 +1024,21 @@ noSeqTerm:
let branches = focusBranches pbs (rr2 $loc($1) $loc(pbs)) in
mk_function branches (rr $loc) (rr2 $loc($1) $loc(pbs))
}
| a=ASSUME e=atomicTerm
| a=ASSUME e=noSeqTerm
{ let a = set_lid_range assume_lid (rr $loc(a)) in
mkExplicitApp (mk_term (Var a) (rr $loc(a)) Expr) [e] (rr $loc)
}

| a=ASSERT e=atomicTerm tactic_opt=option(BY tactic=thunk2(typ) {tactic})
| a=ASSERT e=noSeqTerm
{
match tactic_opt with
| None ->
let a = set_lid_range assert_lid (rr $loc(a)) in
mkExplicitApp (mk_term (Var a) (rr $loc(a)) Expr) [e] (rr $loc)
| Some tac ->
let a = set_lid_range assert_by_tactic_lid (rr $loc(a)) in
mkExplicitApp (mk_term (Var a) (rr $loc(a)) Expr) [e; tac] (rr $loc)
let a = set_lid_range assert_lid (rr $loc(a)) in
mkExplicitApp (mk_term (Var a) (rr $loc(a)) Expr) [e] (rr $loc)
}

| a=ASSERT e=noSeqTerm BY tactic=thunk2(typ)
{
let a = set_lid_range assert_by_tactic_lid (rr $loc(a)) in
mkExplicitApp (mk_term (Var a) (rr $loc(a)) Expr) [e; tactic] (rr $loc)
}

| u=UNDERSCORE BY tactic=thunk(atomicTerm)
Expand Down Expand Up @@ -1125,22 +1140,9 @@ calcStep:
CalcStep (rel, justif, next)
}

%public
typX(X,Y):
| t=Y { t }

| q=quantifier bs=binders DOT trigger=trigger e=X
{
match bs with
| [] ->
raise_error (Fatal_MissingQuantifierBinder, "Missing binders for a quantifier") (rr2 $loc(q) $loc($3))
| _ ->
let idents = idents_of_binders bs (rr2 $loc(q) $loc($3)) in
mk_term (q (bs, (idents, trigger), e)) (rr2 $loc(q) $loc(e)) Formula
}

%inline
typ:
| t=typX(noSeqTerm,simpleTerm) { t }
| t=simpleTerm { t }

%inline quantifier:
| FORALL { fun x -> QForall x }
Expand All @@ -1166,10 +1168,8 @@ disjunctivePats:
conjunctivePat:
| pats=separated_nonempty_list(SEMICOLON, appTerm) { pats }

simpleTerm:
%inline simpleTerm:
| e=tmIff { e }
| FUN pats=nonempty_list(patternOrMultibinder) RARROW e=term
{ mk_term (Abs(flatten pats, e)) (rr2 $loc($1) $loc(e)) Un }

maybeFocusArrow:
| RARROW { false }
Expand Down Expand Up @@ -1292,6 +1292,9 @@ tmEqWith(X):
| e=tmNoEqWith(X)
{ e }

%inline recordTerm:
| LBRACE e=recordExp RBRACE { e }

tmNoEqWith(X):
| e1=tmNoEqWith(X) COLON_COLON e2=tmNoEqWith(X)
{ consTerm (rr $loc) e1 e2 }
Expand Down Expand Up @@ -1319,7 +1322,7 @@ tmNoEqWith(X):
{ mkApp op [ e1, Infix; e2, Nothing ] (rr $loc) }
| e1=tmNoEqWith(X) op=OPINFIX4 e2=tmNoEqWith(X)
{ mk_term (Op(mk_ident(op, rr $loc(op)), [e1; e2])) (rr $loc) Un}
| LBRACE e=recordExp RBRACE { e }
| e=recordTerm { e }
| BACKTICK_PERC e=atomicTerm
{ mk_term (VQuote e) (rr $loc) Un }
| op=TILDE e=atomicTerm
Expand Down Expand Up @@ -1381,22 +1384,30 @@ simpleDef:
| e=separated_pair(qlidentOrOperator, EQUALS, noSeqTerm) { e }
| lid=qlidentOrOperator { lid, mk_term (Name (lid_of_ids [ ident_of_lid lid ])) (rr $loc(lid)) Un }

%inline appTermCommon(argTerm):
| head=indexingTerm args=list(argTerm)
appTermArgs:
| h=maybeHash a=onlyTrailingTerm { [h, a] }
| h=maybeHash a=indexingTerm rest=appTermArgs { (h, a) :: rest }
| h=maybeHash a=recordTerm rest=appTermArgs { (h, a) :: rest }
| a=universe rest=appTermArgs { a :: rest }
| { [] }

appTermCommon(args):
| head=indexingTerm args=args
{ mkApp head (map (fun (x,y) -> (y,x)) args) (rr2 $loc(head) $loc(args)) }

%public
appTerm:
| t=appTermCommon(t=argTerm {t} | h=maybeHash LBRACE t=recordExp RBRACE {h, t}) {t}
| t=onlyTrailingTerm { t }
| t=appTermCommon(appTermArgs) { t }

%public
appTermNoRecordExp:
| t=appTermCommon(argTerm) {t}
appTermArgsNoRecordExp:
| h=maybeHash a=indexingTerm rest=appTermArgsNoRecordExp { (h, a) :: rest }
| a=universe rest=appTermArgsNoRecordExp { a :: rest }
| { [] }

%public
argTerm:
| x=pair(maybeHash, indexingTerm) { x }
| u=universe { u }
appTermNoRecordExp:
| t=appTermCommon(appTermArgsNoRecordExp) {t}

%inline maybeHash:
| { Nothing }
Expand All @@ -1422,6 +1433,25 @@ atomicTerm:
| x=opPrefixTerm(atomicTermQUident)
{ x }

trailingTerm:
| x=atomicTerm
{ x }
| x=onlyTrailingTerm
{ x }

onlyTrailingTerm:
| FUN pats=nonempty_list(patternOrMultibinder) RARROW e=term
{ mk_term (Abs(flatten pats, e)) (rr2 $loc($1) $loc(e)) Un }
| q=quantifier bs=binders DOT trigger=trigger e=term
{
match bs with
| [] ->
raise_error (Fatal_MissingQuantifierBinder, "Missing binders for a quantifier") (rr2 $loc(q) $loc($3))
| _ ->
let idents = idents_of_binders bs (rr2 $loc(q) $loc($3)) in
mk_term (q (bs, (idents, trigger), e)) (rr2 $loc(q) $loc(e)) Formula
}

atomicTermQUident:
| id=quident
{
Expand Down
2 changes: 1 addition & 1 deletion ocaml/fstar-lib/generated/FStar_InteractiveHelpers_Effectful.ml
View file

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

26 changes: 26 additions & 0 deletions tests/bug-reports/Parentheses.fst
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
module Parentheses

let forall_intro #t (#p: t->Type0) (h: (x:t -> squash (p x))) : squash (forall x. p x) =
Classical.Sugar.forall_intro _ _ h

let trailing_fun_does_not_require_parens :
squash (forall (x: nat) (y: nat). x + y >= 0) =
forall_intro fun x -> forall_intro fun y -> ()

let trailing_fun_swallows_seqs :
squash (forall (x: nat) (y: nat). x + y >= 0) =
forall_intro fun x -> forall_intro fun y -> (); ()

let assert_does_not_require_parens : unit =
assert 8 < 42;
()

let assume_does_not_require_parens : False =
assume 0 == 1;
()

let forall_does_not_require_parens () : Lemma (True /\ forall x. x <= x) =
()

let exists_does_not_require_parens () : Lemma (True /\ exists x. x <= x) =
()

0 comments on commit a2e12be

Please sign in to comment.