Merge pull request #3341 from mtzguido/resugar

Resugar: improve resugaring for projectors

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

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)
+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

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