diff --git a/ocaml/fstar-lib/FStar_Parser_Parse.mly b/ocaml/fstar-lib/FStar_Parser_Parse.mly index d95415224ae..4c27d7a0e72 100644 --- a/ocaml/fstar-lib/FStar_Parser_Parse.mly +++ b/ocaml/fstar-lib/FStar_Parser_Parse.mly @@ -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 @@ -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: @@ -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 { @@ -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) @@ -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 } @@ -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 } @@ -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 } @@ -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 @@ -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 } @@ -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 { diff --git a/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_Effectful.ml b/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_Effectful.ml index 5be54322872..f214b5d761b 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 diff --git a/tests/bug-reports/Parentheses.fst b/tests/bug-reports/Parentheses.fst new file mode 100644 index 00000000000..8f828d0bc75 --- /dev/null +++ b/tests/bug-reports/Parentheses.fst @@ -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) = + ()