diff --git a/ocaml/fstar-lib/generated/FStar_Syntax_Resugar.ml b/ocaml/fstar-lib/generated/FStar_Syntax_Resugar.ml index 498f3f2fd5c..4a378d13efb 100644 --- a/ocaml/fstar-lib/generated/FStar_Syntax_Resugar.ml +++ b/ocaml/fstar-lib/generated/FStar_Syntax_Resugar.ml @@ -867,27 +867,43 @@ let rec (resugar_term' : else FStar_Pervasives_Native.None | uu___4 -> FStar_Pervasives_Native.None in let uu___3 = - (let uu___4 = is_projector e in - FStar_Pervasives_Native.uu___is_Some uu___4) && - ((FStar_Compiler_List.length args1) = Prims.int_one) in + ((let uu___4 = is_projector e in + FStar_Pervasives_Native.uu___is_Some uu___4) && + ((FStar_Compiler_List.length args1) >= Prims.int_one)) + && + (let uu___4 = + let uu___5 = FStar_Compiler_List.hd args1 in + FStar_Pervasives_Native.snd uu___5 in + FStar_Pervasives_Native.uu___is_None uu___4) in if uu___3 then - let uu___4 = - let uu___5 = is_projector e in - FStar_Pervasives_Native.__proj__Some__item__v uu___5 in + let uu___4 = args1 in (match uu___4 with - | (uu___5, fi) -> - let arg = - let uu___6 = - let uu___7 = FStar_Compiler_List.hd args1 in - FStar_Pervasives_Native.fst uu___7 in - resugar_term' env uu___6 in - let uu___6 = - let uu___7 = - let uu___8 = FStar_Ident.lid_of_ids [fi] in - (arg, uu___8) in - FStar_Parser_AST.Project uu___7 in - mk uu___6) + | arg1::rest_args -> + let uu___5 = + let uu___6 = is_projector e in + FStar_Pervasives_Native.__proj__Some__item__v uu___6 in + (match uu___5 with + | (uu___6, fi) -> + let arg = + resugar_term' env + (FStar_Pervasives_Native.fst arg1) in + let h = + let uu___7 = + let uu___8 = + let uu___9 = FStar_Ident.lid_of_ids [fi] in + (arg, uu___9) in + FStar_Parser_AST.Project uu___8 in + mk uu___7 in + FStar_Compiler_List.fold_left + (fun acc -> + fun uu___7 -> + match uu___7 with + | (a, q) -> + let aa = resugar_term' env a in + let qq = resugar_aqual env q in + mk (FStar_Parser_AST.App (acc, aa, qq))) + h rest_args)) else (let unsnoc l = let rec unsnoc' acc uu___5 = diff --git a/src/syntax/FStar.Syntax.Resugar.fst b/src/syntax/FStar.Syntax.Resugar.fst index 16f27562e0c..ace437b5140 100644 --- a/src/syntax/FStar.Syntax.Resugar.fst +++ b/src/syntax/FStar.Syntax.Resugar.fst @@ -470,10 +470,19 @@ let rec resugar_term' (env: DsEnv.env) (t : S.term) : A.term = else None | _ -> None in - if Some? (is_projector e) && List.length args = 1 then + (* We have a projector, applied to at least one argument, and the first argument + is explicit (so not one of the parameters of the type). In this case we resugar nicely. *) + if Some? (is_projector e) && List.length args >= 1 && None? (snd (List.hd args)) then + let arg1 :: rest_args = args in let (_, fi) = Some?.v (is_projector e) in - let arg = resugar_term' env (fst (List.hd args)) in - mk <| Project (arg, Ident.lid_of_ids [fi]) + let arg = resugar_term' env (fst arg1) in + let h = mk <| Project (arg, Ident.lid_of_ids [fi]) in + (* Add remaining args if any. *) + rest_args |> List.fold_left (fun acc (a, q) -> + let aa = resugar_term' env a in + let qq = resugar_aqual env q in + mk (A.App (acc, aa, qq))) + h else let unsnoc (#a:Type) (l : list a) : (list a & a) = let rec unsnoc' acc = function diff --git a/tests/error-messages/Bug3227.fst b/tests/error-messages/Bug3227.fst index 946f145490d..8dd41c3d116 100644 --- a/tests/error-messages/Bug3227.fst +++ b/tests/error-messages/Bug3227.fst @@ -5,4 +5,16 @@ let proj (b : box (box (box int))) : int = b.x.x.x type box2 (a:Type) = | Box2 : x:a -> box2 a -let test (b : box2 (box2 int)) = Box2? b && Box2? (Box2?.x b) \ No newline at end of file +let test (b : box2 (box2 int)) = Box2? b && Box2? (Box2?.x b) + +noeq +type boxf (a:Type) = { ff : a -> a } + +let test2 (r : boxf int) = r.ff 5 + +noeq +type boxfi (a:Type) = { ff : (#_:a -> a) } + +let test3 (r : boxfi int) = r.ff #5 + +let test4 (#a:Type) (r : boxf a) (x:a) : a = r.ff x diff --git a/tests/error-messages/Bug3227.fst.expected b/tests/error-messages/Bug3227.fst.expected index 4a4a9d19016..1221b3c449e 100644 --- a/tests/error-messages/Bug3227.fst.expected +++ b/tests/error-messages/Bug3227.fst.expected @@ -9,6 +9,15 @@ type box2 (a: Type) = | Box2 : x: a -> Bug3227.box2 a let test b = Box2? b && Box2? b.x +noeq +type boxf (a: Type) = { } + +let test2 r = ff r 5 +noeq +type boxfi (a: Type) = { } + +let test3 r = ff r +let test4 r x = ff r x <: a ] Exports: [ type box (a: Type) = { } @@ -19,6 +28,15 @@ type box2 (a: Type) = | Box2 : x: a -> Bug3227.box2 a let test b = Box2? b && Box2? b.x +noeq +type boxf (a: Type) = { } + +let test2 r = ff r 5 +noeq +type boxfi (a: Type) = { } + +let test3 r = ff r +let test4 r x = ff r x <: a ] Module before type checking: @@ -32,6 +50,15 @@ type box2 (a: Type) = | Box2 : x: a -> Bug3227.box2 a let test b = Box2? b && Box2? b.x +noeq +type boxf (a: Type) = { } + +let test2 r = ff r 5 +noeq +type boxfi (a: Type) = { } + +let test3 r = ff r +let test4 r x = ff r x <: a ] Exports: [ type box (a: Type) = { } @@ -42,6 +69,15 @@ type box2 (a: Type) = | Box2 : x: a -> Bug3227.box2 a let test b = Box2? b && Box2? b.x +noeq +type boxf (a: Type) = { } + +let test2 r = ff r 5 +noeq +type boxfi (a: Type) = { } + +let test3 r = ff r +let test4 r x = ff r x <: a ] Module after type checking: @@ -61,6 +97,17 @@ val box2__uu___haseq: forall (a: Type). {:pattern Prims.hasEq (Bug3227.box2 a)} let test b = Box2? b && Box2? b.x +noeq +type boxf (a: Type) = { ff:_: a -> a } + + +let test2 r = r.ff 5 +noeq +type boxfi (a: Type) = { ff:a } + + +let test3 r = r.ff +let test4 r x = r.ff x <: a ] Exports: [ type box (a: Type) = { x:a } @@ -77,6 +124,17 @@ val box2__uu___haseq: forall (a: Type). {:pattern Prims.hasEq (Bug3227.box2 a)} let test b = Box2? b && Box2? b.x +noeq +type boxf (a: Type) = { ff:_: a -> a } + + +let test2 r = r.ff 5 +noeq +type boxfi (a: Type) = { ff:a } + + +let test3 r = r.ff +let test4 r x = r.ff x <: a ] Verified module: Bug3227