From 88a7338269a512ee4b33a130fbe2722da89e4dbf Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Wed, 14 Aug 2024 16:57:07 -0700 Subject: [PATCH 1/4] Do not require parens for trailing fun. --- ocaml/fstar-lib/FStar_Parser_Parse.mly | 4 ++-- tests/bug-reports/Parentheses.fst | 12 ++++++++++++ 2 files changed, 14 insertions(+), 2 deletions(-) create mode 100644 tests/bug-reports/Parentheses.fst diff --git a/ocaml/fstar-lib/FStar_Parser_Parse.mly b/ocaml/fstar-lib/FStar_Parser_Parse.mly index e638246f6c5..d2517f24196 100644 --- a/ocaml/fstar-lib/FStar_Parser_Parse.mly +++ b/ocaml/fstar-lib/FStar_Parser_Parse.mly @@ -1167,8 +1167,6 @@ conjunctivePat: 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 } @@ -1420,6 +1418,8 @@ atomicTerm: { x } | x=opPrefixTerm(atomicTermQUident) { x } + | FUN pats=nonempty_list(patternOrMultibinder) RARROW e=term + { mk_term (Abs(flatten pats, e)) (rr2 $loc($1) $loc(e)) Un } atomicTermQUident: | id=quident diff --git a/tests/bug-reports/Parentheses.fst b/tests/bug-reports/Parentheses.fst new file mode 100644 index 00000000000..dffd788e539 --- /dev/null +++ b/tests/bug-reports/Parentheses.fst @@ -0,0 +1,12 @@ +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 -> (); () \ No newline at end of file From fcc1b9ca6a69bad91a5622634cba20a5e621269a Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Wed, 14 Aug 2024 17:04:52 -0700 Subject: [PATCH 2/4] Do not require parens in assert/assume. --- ocaml/fstar-lib/FStar_Parser_Parse.mly | 4 ++-- tests/bug-reports/Parentheses.fst | 10 +++++++++- 2 files changed, 11 insertions(+), 3 deletions(-) diff --git a/ocaml/fstar-lib/FStar_Parser_Parse.mly b/ocaml/fstar-lib/FStar_Parser_Parse.mly index d2517f24196..535ea36a46c 100644 --- a/ocaml/fstar-lib/FStar_Parser_Parse.mly +++ b/ocaml/fstar-lib/FStar_Parser_Parse.mly @@ -1009,12 +1009,12 @@ 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 tactic_opt=option(BY tactic=thunk2(typ) {tactic}) { match tactic_opt with | None -> diff --git a/tests/bug-reports/Parentheses.fst b/tests/bug-reports/Parentheses.fst index dffd788e539..38a940b9089 100644 --- a/tests/bug-reports/Parentheses.fst +++ b/tests/bug-reports/Parentheses.fst @@ -9,4 +9,12 @@ let trailing_fun_does_not_require_parens : let trailing_fun_swallows_seqs : squash (forall (x: nat) (y: nat). x + y >= 0) = - forall_intro fun x -> forall_intro fun y -> (); () \ No newline at end of file + 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; + () \ No newline at end of file From 3ff6daea03065ea43c7163b6ba7eb7c8c1a69c61 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Mon, 19 Aug 2024 14:02:36 -0700 Subject: [PATCH 3/4] Fix reduce/reduce conflicts. --- ocaml/fstar-lib/FStar_Parser_Parse.mly | 82 +++++++++++++------ .../FStar_InteractiveHelpers_Effectful.ml | 2 +- 2 files changed, 59 insertions(+), 25 deletions(-) diff --git a/ocaml/fstar-lib/FStar_Parser_Parse.mly b/ocaml/fstar-lib/FStar_Parser_Parse.mly index 535ea36a46c..4c07e6ea253 100644 --- a/ocaml/fstar-lib/FStar_Parser_Parse.mly +++ b/ocaml/fstar-lib/FStar_Parser_Parse.mly @@ -144,6 +144,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 @@ -879,7 +884,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: @@ -921,14 +926,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 { @@ -1014,15 +1028,16 @@ noSeqTerm: mkExplicitApp (mk_term (Var a) (rr $loc(a)) Expr) [e] (rr $loc) } - | a=ASSERT e=noSeqTerm 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) @@ -1165,7 +1180,7 @@ disjunctivePats: conjunctivePat: | pats=separated_nonempty_list(SEMICOLON, appTerm) { pats } -simpleTerm: +%inline simpleTerm: | e=tmIff { e } maybeFocusArrow: @@ -1289,6 +1304,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 } @@ -1316,7 +1334,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 @@ -1378,22 +1396,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 } @@ -1418,6 +1444,14 @@ atomicTerm: { x } | 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 } diff --git a/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_Effectful.ml b/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_Effectful.ml index 4cc428e4c5f..a29ac191ca1 100644 --- a/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_Effectful.ml +++ b/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_Effectful.ml @@ -7741,7 +7741,7 @@ let (eterm_info_to_assertions : (Prims.of_int (822)) (Prims.of_int (10)) (Prims.of_int (864)) - (Prims.of_int (32))))) + (Prims.of_int (13))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range From 22b11afb389d8e8493cce4f7a8f33876c1375852 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Mon, 19 Aug 2024 18:26:05 -0700 Subject: [PATCH 4/4] Do not require parentheses around forall/exists --- ocaml/fstar-lib/FStar_Parser_Parse.mly | 26 +++++++++++--------------- tests/bug-reports/Parentheses.fst | 8 +++++++- 2 files changed, 18 insertions(+), 16 deletions(-) diff --git a/ocaml/fstar-lib/FStar_Parser_Parse.mly b/ocaml/fstar-lib/FStar_Parser_Parse.mly index 4c07e6ea253..a7355f7edf5 100644 --- a/ocaml/fstar-lib/FStar_Parser_Parse.mly +++ b/ocaml/fstar-lib/FStar_Parser_Parse.mly @@ -1139,22 +1139,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 } @@ -1454,6 +1441,15 @@ trailingTerm: 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 diff --git a/tests/bug-reports/Parentheses.fst b/tests/bug-reports/Parentheses.fst index 38a940b9089..8f828d0bc75 100644 --- a/tests/bug-reports/Parentheses.fst +++ b/tests/bug-reports/Parentheses.fst @@ -17,4 +17,10 @@ let assert_does_not_require_parens : unit = let assume_does_not_require_parens : False = assume 0 == 1; - () \ No newline at end of file + () + +let forall_does_not_require_parens () : Lemma (True /\ forall x. x <= x) = + () + +let exists_does_not_require_parens () : Lemma (True /\ exists x. x <= x) = + ()