diff --git a/src/ml/FStarC_Parser_Parse.mly b/src/ml/FStarC_Parser_Parse.mly index 4805d11233a..ae839ee1cfb 100644 --- a/src/ml/FStarC_Parser_Parse.mly +++ b/src/ml/FStarC_Parser_Parse.mly @@ -67,6 +67,54 @@ type tc_constraint = { r: FStarC_Range.t; } +let pattern_must_be_binder (p : pattern) : binder = + match p.pat with + | PatConst Const_unit -> + (* A unit pattern: `()`. Unsure if this is the right place to look + for it. *) + let x = gen p.prange in + let u = + unit_type p.prange + (* mk_term (Const Const_unit) p.prange Expr *) + in + mk_binder (Annotated (x, u)) p.prange Expr None + + | PatAscribed ({ pat = PatVar (x, aq, attrs)}, (t, _tac_opt)) -> + mk_binder_with_attrs (Annotated (x, t)) p.prange Expr aq attrs + + | PatVar (x, aq, attrs) -> + mk_binder_with_attrs (Variable x) p.prange Expr aq attrs + + | PatAscribed ({ pat = PatWild (aq, attrs)}, (t, _tac_opt)) -> + let x = gen p.prange in + mk_binder_with_attrs (Annotated (x, t)) p.prange Expr aq attrs + + | PatWild (aq, attrs) -> + let x = gen p.prange in + mk_binder_with_attrs (Variable x) p.prange Expr aq attrs + + | _ -> + raise_error_text p.prange Fatal_SyntaxError + ("Must be a simple binder: " ^ pat_to_string p) + +(* For a multibinder like `(a b c : Type | eq, ord)`, this generates + binders + {| _ : eq a |} {| _ : ord a |} + {| _ : eq b |} {| _ : ord b |} + {| _ : eq c |} {| _ : ord c |} + in that order. +*) +let expand_inline_constraints (cts : term list) (xs : ident list) : pattern list = + List.concat_map (fun x -> + List.concat_map (fun ct -> + let r = ct.range in + let x_t = mk_term (Var (lid_of_ids [x])) r Expr in + let ct = mk_term (App (ct, x_t, Nothing)) r Expr in + let id = gen r in + [ mk_pattern (PatAscribed(mk_pattern (PatVar (id, Some TypeClassArg, [])) r, (ct, None))) r ] + ) cts + ) xs + %} %token STRING @@ -508,7 +556,7 @@ letoperatorbinding: } letbinding: - | focus_opt=maybeFocus lid=lidentOrOperator lbp=nonempty_list(patternOrMultibinder) ascr_opt=ascribeTyp? EQUALS tm=term + | focus_opt=maybeFocus lid=lidentOrOperator lbp=nonempty_list(genBinder) ascr_opt=ascribeTyp? EQUALS tm=term { let pat = mk_pattern (PatVar(lid, None, [])) (rr $loc(lid)) in let pat = mk_pattern (PatApp (pat, flatten lbp)) (rr2 $loc(focus_opt) $loc(lbp)) in @@ -681,24 +729,62 @@ tuplePattern: constructorPattern: | pat=constructorPattern COLON_COLON pats=constructorPattern { mk_pattern (consPat (rr $loc(pats)) pat pats) (rr $loc) } - | uid=quident args=nonempty_list(atomicPattern) + | uid=quident args=nonempty_list(singleAtomicPattern) { let head_pat = mk_pattern (PatName uid) (rr $loc(uid)) in mk_pattern (PatApp (head_pat, args)) (rr $loc) } - | pat=atomicPattern + | pat=singleAtomicPattern { pat } +singleAtomicPattern: + | pats=atomicPattern + { + match pats with + | [p] -> p + | _ -> raise_error_text (rr $loc) Fatal_SyntaxError "Syntax error: expected a single atomic pattern, not a list" + } + atomicPattern: - | DOT_DOT + | a=atomicPatternNoLParen + { [a] } + | LPAREN + pats=nonempty_list(tuplePattern) + ann=genBinderAnnotation + RPAREN { - mk_pattern PatRest (rr $loc) + let t_ann, ref_opt, tc_cts = ann in + let t_pos = rr $loc(ann) in + (* let pats = List.flatten pats in *) + let n = List.length pats in + let bs : pattern list = + List.mapi (fun idx pat -> + (* let pat = mk_pattern (PatVar (x, aq, attrs)) pos in *) + (* Only the last binder carries the refinement, if any. *) + let ref_opt = if idx = Int.sub n 1 then ref_opt else None in + (* ^ The - symbol resolves to F* addition. *) + match t_ann with + | Some ty -> + mkRefinedPattern pat ty true ref_opt t_pos pat.prange + | None -> pat + ) pats + in + let rec pat_names bs = + match bs with + | [] -> [] + | b::bs' -> + match b.pat with + | PatAscribed ({pat = PatVar (x, _, _)}, _) + | PatVar (x, _, _) -> x::pat_names bs' + | _ -> pat_names bs' + in + bs @ expand_inline_constraints tc_cts (pat_names bs) } - | LPAREN pat=tuplePattern COLON t=simpleArrow phi_opt=refineOpt RPAREN + +atomicPatternNoLParen: + | DOT_DOT { - let pos_t = rr2 $loc(pat) $loc(t) in - let pos = rr $loc in - mkRefinedPattern pat t true phi_opt pos_t pos + mk_pattern PatRest (rr $loc) } | LBRACK pats=right_flexible_list(SEMICOLON, tuplePattern) RBRACK { mk_pattern (PatList pats) (rr2 $loc($1) $loc($3)) } @@ -706,13 +792,8 @@ atomicPattern: { mk_pattern (PatRecord record_pat) (rr $loc) } | LENS_PAREN_LEFT pat0=constructorPattern COMMA pats=separated_nonempty_list(COMMA, constructorPattern) LENS_PAREN_RIGHT { mk_pattern (PatTuple(pat0::pats, true)) (rr $loc) } - | LPAREN pat=tuplePattern RPAREN { pat } | LPAREN op=operator RPAREN { mk_pattern (PatOp op) (rr $loc) } - | UNDERSCORE - { mk_pattern (PatWild (None, [])) (rr $loc) } - | HASH UNDERSCORE - { mk_pattern (PatWild (Some Implicit, [])) (rr $loc) } | c=constant { mk_pattern (PatConst c) (rr $loc(c)) } | tok=MINUS c=constant @@ -733,6 +814,10 @@ atomicPattern: { let (aqual, attrs), lid = qual_id in mk_pattern (PatVar (lid, aqual, attrs)) (rr $loc(qual_id)) } + | qual_id=aqualifiedWithAttrs(UNDERSCORE) + { + let (aqual, attrs), _ = qual_id in + mk_pattern (PatWild (aqual, attrs)) (rr $loc(qual_id)) } | uid=quident { mk_pattern (PatName uid) (rr $loc(uid)) } @@ -749,83 +834,24 @@ tc_constraint: {id; t; r} } +(* Typeclass constraints: what appears inside a {| ... |}. They can +be named or anonymous *) tc_constraints: | constraints=right_flexible_nonempty_list(COMMA, tc_constraint) { constraints } - - (* (x : t) is already covered by atomicPattern *) - (* we do *NOT* allow _ in multibinder () since it creates reduce/reduce conflicts when*) - (* preprocessing to ocamlyacc/fsyacc (which is expected since the macro are expanded) *) -patternOrMultibinder: - | LBRACE_BAR constraints=tc_constraints BAR_RBRACE - { - let constraint_as_pat (c:tc_constraint) = - let w = mk_pattern (PatVar (c.id, Some TypeClassArg, [])) c.r in - let asc = (c.t, None) in - mk_pattern (PatAscribed(w, asc)) c.r - in - List.map constraint_as_pat constraints - } - - | pat=atomicPattern { [pat] } - | LPAREN - qual_id0=aqualifiedWithAttrs(lident) - qual_ids=nonempty_list(aqualifiedWithAttrs(lident)) - COLON - t=simpleArrow r=refineOpt - RPAREN - { - let pos = rr $loc in - let t_pos = rr $loc(t) in - let qual_ids = qual_id0 :: qual_ids in - let n = List.length qual_ids in - List.mapi (fun idx ((aq, attrs), x) -> - let pat = mk_pattern (PatVar (x, aq, attrs)) pos in - (* Only the last binder carries the refinement, if any. *) - let refine_opt = if idx = Int.sub n 1 then r else None in - (* ^ The - symbol resolves to F* addition. *) - mkRefinedPattern pat t true refine_opt t_pos pos - ) qual_ids - } - -binder: - | aqualifiedWithAttrs_lid=aqualifiedWithAttrs(lidentOrUnderscore) - { - let (q, attrs), lid = aqualifiedWithAttrs_lid in - mk_binder_with_attrs (Variable lid) (rr $loc(aqualifiedWithAttrs_lid)) Type_level q attrs - } + +(* Constraints on binders: like (#a : Type | deq) *) +type_tc_constraints: + | BAR constraints=right_flexible_nonempty_list(COMMA, tmEqNoRefinement) { constraints } + | { [] } %public -multiBinder: - | LBRACE_BAR constraints=tc_constraints BAR_RBRACE - { - let constraint_as_binder (c:tc_constraint) = - mk_binder (Annotated (c.id, c.t)) c.r Type_level (Some TypeClassArg) - in - List.map constraint_as_binder constraints - } - - | LPAREN qual_ids=nonempty_list(aqualifiedWithAttrs(lidentOrUnderscore)) COLON t=simpleArrow r=refineOpt RPAREN - { - let should_bind_var = match qual_ids with | [ _ ] -> true | _ -> false in - let n = List.length qual_ids in - List.mapi (fun idx ((q, attrs), x) -> - let refine_opt = if idx = Int.sub n 1 then r else None in - mkRefinedBinder x t true refine_opt (rr $loc) q attrs - ) qual_ids - } - - | LPAREN_RPAREN +binders: + | bss=list(genBinder) { - let r = rr $loc in - let unit_t = mk_term (Var (lid_of_ids [(mk_ident("unit", r))])) r Un in - [mk_binder (Annotated (gen r, unit_t)) r Un None] + let bs = flatten bss in + List.map pattern_must_be_binder bs } - | b=binder { [b] } - -%public -binders: bss=list(bs=multiBinder {bs}) { flatten bss } - aqualifiedWithAttrs(X): | aq=aqual attrs=binderAttributes x=X { (Some aq, attrs), x } | aq=aqual x=X { (Some aq, []), x } @@ -1255,6 +1281,7 @@ simpleArrowDomain: (* Tm already accounts for ( term ), we need to add an explicit case for (#Tm), (#[@@@...]Tm) and ([@@@...]Tm) *) %inline tmArrowDomain(Tm): + (* Replace all this for genBinder? *) | LBRACE_BAR t=Tm BAR_RBRACE { ((Some TypeClassArg, []), t) } | LPAREN q=aqual attrs_opt=ioption(binderAttributes) dom_tm=Tm RPAREN { (Some q, none_to_empty_list attrs_opt), dom_tm } | LPAREN attrs=binderAttributes dom_tm=Tm RPAREN { (None, attrs), dom_tm } @@ -1469,7 +1496,7 @@ trailingTerm: { x } onlyTrailingTerm: - | FUN pats=nonempty_list(patternOrMultibinder) RARROW e=term + | FUN pats=nonempty_list(genBinder) RARROW e=term { mk_term (Abs(flatten pats, e)) (rr2 $loc($1) $loc(e)) Un } | q=quantifier bs=binders DOT trigger=trigger e=term { @@ -1688,3 +1715,26 @@ reverse_left_flexible_nonempty_list(delim, X): %inline left_flexible_nonempty_list(delim, X): xs = reverse_left_flexible_nonempty_list(delim, X) { List.rev xs } + +genBinderAnnotation: + | { None, None, [] } + | COLON + t=simpleArrow + r=refineOpt + cts=type_tc_constraints + { + (Some t), r, cts + } + +genBinder: + | LBRACE_BAR constraints=tc_constraints BAR_RBRACE + { + let constraint_as_pat (c:tc_constraint) = + let w = mk_pattern (PatVar (c.id, Some TypeClassArg, [])) c.r in + let asc = (c.t, None) in + mk_pattern (PatAscribed(w, asc)) c.r + in + List.map constraint_as_pat constraints + } + + | pats=atomicPattern { pats } diff --git a/src/parser/FStarC.Parser.AST.fst b/src/parser/FStarC.Parser.AST.fst index 50f92650a20..0edbd2c77f2 100644 --- a/src/parser/FStarC.Parser.AST.fst +++ b/src/parser/FStarC.Parser.AST.fst @@ -177,7 +177,8 @@ let mkListLit r elts = let mkSeqLit r elts = mk_term (SeqLiteral elts) r Expr -let unit_const r = mk_term(Const Const_unit) r Expr +let unit_const r = mk_term (Const Const_unit) r Expr +let unit_type r = mk_term (Var (Ident.lid_of_str (`%unit))) r Expr let ml_comp t = let lid = C.effect_ML_lid () in @@ -997,12 +998,14 @@ instance pretty_quote_kind : pretty quote_kind = { let ctor (n: string) (args: list document) = nest 2 (group (parens (flow (break_ 1) (doc_of_string n :: args)))) +// let ctor (n: string) (arg: document) : document = +// nest 2 (group (parens (doc_of_string n ^/^ arg))) let pp_list' (#a:Type) (f: a -> document) (xs: list a) : document = (pp_list a { pp = f }).pp xs // hack instance showable_arg_qualifier : showable arg_qualifier = { - show = function + show = function | Implicit -> "Implicit" | Equality -> "Equality" | Meta i -> "Meta" @@ -1047,7 +1050,7 @@ let rec pp_term (t:term) : document = ctor "LetOpBinding" [pp i; pp_pattern p; pp_term b] in ctor "LetOperator" [pp_list' pp_letopbinding lbs; pp_term body] - | LetOpen (lid, t) -> + | LetOpen (lid, t) -> ctor "LetOpen" [pp lid; pp_term t] | LetOpenRecord (t1, t2, t3) -> ctor "LetOpenRecord" [pp_term t1; pp_term t2; pp_term t3] @@ -1222,7 +1225,7 @@ instance pretty_constructor_payload : pretty constructor_payload = { pp = pp_con let pp_tycon (tc : tycon) : document = match tc with - | TyconAbstract (i, bs, knd) -> + | TyconAbstract (i, bs, knd) -> ctor "TyconAbstract" [pp i; pp bs; pp knd] | TyconAbbrev (i, bs, knd, t) -> ctor "TyconAbbrev" [pp i; pp bs; pp knd; doc_of_string "_"] @@ -1252,7 +1255,7 @@ let pp_decl (d:decl) : document = let pp_pat_term (p, t) = ctor "PatTerm" [pp p; pp t] in ctor "TopLevelLet" [doc_of_string (show q); pp_list' pp_pat_term pats] - | Assume (i, t_opt) -> + | Assume (i, t_opt) -> let pp_opt_term = function None -> doc_of_string "None" | Some t -> pp_term t in ctor "Assume" [pp i; pp_term t_opt] | Tycon (r, tps, tys) -> diff --git a/src/parser/FStarC.Parser.AST.fsti b/src/parser/FStarC.Parser.AST.fsti index 2008133bfcb..32d8e4bdcd5 100644 --- a/src/parser/FStarC.Parser.AST.fsti +++ b/src/parser/FStarC.Parser.AST.fsti @@ -328,6 +328,7 @@ val consPat : range -> pattern -> pattern -> pattern' val consTerm : range -> term -> term -> term val unit_const : range -> term +val unit_type : range -> term val ml_comp : term -> term val tot_comp : term -> term diff --git a/tests/micro-benchmarks/MinusVsNegParsing.fst b/tests/micro-benchmarks/MinusVsNegParsing.fst new file mode 100644 index 00000000000..87ed7b88a5b --- /dev/null +++ b/tests/micro-benchmarks/MinusVsNegParsing.fst @@ -0,0 +1,42 @@ +module MinusVsNegParsing + +let test (x:int) : bool = + match x with + | (-5) -> true + | -3 -> true + | _ -> false + +// Parses as a match against (-5) +val x : (y:int{y == -5}) -> int +let x - 5 = 1 + +// Parses as a match against (-5) +val y : (y:int{y == -5}) -> int +let y -5 = 1 + +(* Make sure we fail for negative *unsigned* machine ints. *) +[@@expect_failure] let _ = -1uy +[@@expect_failure] let _ = -1us +[@@expect_failure] let _ = -1ul +[@@expect_failure] let _ = -1uL +[@@expect_failure] let _ = -1sz +[@@expect_failure] let _ = -1z + +let _ = 1uy +let _ = 1us +let _ = 1ul +let _ = 1uL +let _ = 1sz +let _ = 1z + +(* All good for signed variants. *) + +let _ = -1y +let _ = -1s +let _ = -1l +let _ = -1L + +let _ = 1y +let _ = 1s +let _ = 1l +let _ = 1L diff --git a/tests/micro-benchmarks/Parsing.fst b/tests/micro-benchmarks/Parsing.fst new file mode 100644 index 00000000000..6c105e82cbc --- /dev/null +++ b/tests/micro-benchmarks/Parsing.fst @@ -0,0 +1,73 @@ +module Parsing + +(* Miscellaneous parsing tests, mostly about patterns +for now. *) + +let foo (x,y : int & int) = x + y + +// Currently parses (-1) as a pattern... odd but ok +val bar : (x:int{x == -1}) -> int +let bar - 1 = 2 + +type t = | A + +let baz A = () + +type box t = | Box of t + +let unbox (Box x) = x + +let buz2 (Box x, Box y) = x + y + +let buz1 (Box x) = x + +let bub p = + let (x, y) = p in + x + y + +let bub2 p = + let x, y = p in + x + y + +let bab (x y : int {x >= y}) : nat = x - y + +// Should fail and does +// val bab_box (Box x : box int) : nat +// Should fail and does +// val bab_box (Box x) : nat +// Should fail and does +// val bab_box : (Box x : int) -> nat + +val bab_box (x y : box int {unbox x >= unbox y}) : nat +let bab_box (Box x) (Box y) : nat = x - y + +// This should probably require parentheses, +// it looks really wrong. +let many_tuples (x,y z,w ) = x+y+z+w +let many_tuples_t (x,y z,w : int & int) = x+y+z+w +// This would be nice +let many_tuples_ok ((x,y) (z,w)) = x+y+z+w +let many_tuples_t_ok ((x,y) (z,w) : int & int) = x+y+z+w + +val equality1 ($x : unit) : unit +let equality1 ($x : unit) : unit = () + +// Should parse, but fail +let test_eq_match (x : int) : int = + match x with + | $x -> x + +// Should parse, but fail later +let test_eq_match2 (x : int) : int = + match x with + | $_ -> x + +// Should work +val equality2 ($_ : unit) : unit +let equality2 ($_ : unit) : unit = () + +// Should not work? It parses and desugars, and then +// fails to infer the type of wildcard. It makes sense, just +// maybe nicer to fail earlier? +[@@expect_failure [66]] +val noparens _ : unit diff --git a/tests/micro-benchmarks/TcSyntax.fst b/tests/micro-benchmarks/TcSyntax.fst index 2c3a19921fa..72531d89b46 100644 --- a/tests/micro-benchmarks/TcSyntax.fst +++ b/tests/micro-benchmarks/TcSyntax.fst @@ -1,6 +1,15 @@ module TcSyntax -open FStar.Class.Eq +open FStar.Class.Eq.Raw +open FStar.Class.Ord.Raw + +let has_eq (a : Type | deq) (x : a) = x = x + +let _ = has_eq int 1 + +let has_eq2 (a b : Type | deq) (x : a) = x = x + +let has_ord (a : Type | ord) : unit = () let foo1 (#a #b : Type) @@ -12,7 +21,7 @@ let foo1 let foo2 (#a #b : Type) - {| deq a, deq b |} + {| _ : deq a, db : deq b |} (a1 a2 : a) (b1 b2 : b) : Tot bool @@ -25,3 +34,32 @@ let foo3 (b1 b2 : b) : Tot bool = a1 = a2 && b1 = b2 + +let foo4 + (#a #b : Type | deq) + (a1 a2 : a) + (b1 b2 : b) + : Tot bool + = a1 = a2 && b1 = b2 + +let foo5 + (#a #b : Type | deq, ord, ) + (a1 a2 : a) + (b1 b2 : b) + : Tot bool + = a1 = a2 && b1 = b2 + +let foo6 + (a b : Type | deq) + (a1 a2 : a) + (b1 b2 : b) + : Tot bool + = a1 = a2 && b1 = b2 + +let _ = foo6 int int #_ #_ 1 2 3 4 + +let foo7 + (#a : Type | deq) + (a1 a2 : a) + : Tot bool + = (a1 = a2) = (a2 = a1)