Fix problems in pull derivation

frontend/src/Language/Granule/Synthesis/Deriving.hs

@@ -249,6 +249,39 @@ mkConstructorApplication s name consType  exprs ty =
   Val s () True (Constr () name [])
   -- error $ "In making constructor for " ++ pretty name ++ " with exprs args " ++ pretty exprs ++ " at type " ++ pretty ty
 
+mkConstrApp2 :: (?globals :: Globals) => Span -> Id -> Type -> [(Type, Expr () ())] -> Type -> Checker (Expr () ())
+mkConstrApp2 s name consType args t = mkConstructorApplication2 s name consType base_constr args t
+  where base_constr = Val s () True (Constr () name [])
+
+-- Apply a list of arguments to a ty constructor, based on all of their types
+mkConstructorApplication2 :: (?globals :: Globals) => Span -> Id -> Type -> Expr () () -> [(Type, Expr () ())] -> Type -> Checker (Expr () ())
+mkConstructorApplication2 s name consType acc [] ty =
+  return acc
+
+mkConstructorApplication2 s name consType acc ((Box k t, expr):exprs) (FunTy _ _ t1 t2) = do
+  acc' <- case t1 of
+    Box k' t' -> do
+      debugM "mkConstructorApplication2" $ "boxed " <> pretty t <> " is compatible with " <> pretty t1
+      return $ App s () True acc expr
+    _ -> do
+      -- we're passing a boxed argument into an unboxed constructor parameter
+      -- so we unbox it and pass the result in through a let-bind
+      debugM "mkConstructorApplication2" $ "unboxing " <> pretty t <> " to pass in to " <> pretty t1
+      v <- freshIdentifierBase "y" <&> mkId
+      let result = letBox s (PVar s () True v) expr $ App s () True acc $ Val s () True $ Var () v
+      debugM "mkConstructorApplication2" $ "returning unboxed result " <> pretty result
+      return result
+  mkConstructorApplication2 s name consType acc' exprs t2
+
+mkConstructorApplication2 s name consType acc ((ty, expr):exprs) (FunTy _ _ t1 t2) = do
+  debugM "mkConstructorApplication2" $ "non-boxed " <> pretty ty <> " is compatible with " <> pretty t1
+  let acc' = App s () True acc expr
+  mkConstructorApplication2 s name consType acc' exprs t2
+
+mkConstructorApplication2 s name consType acc exprs ty =
+  -- no applicable arguments
+  return acc
+
 
 derivePull :: (?globals :: Globals) => Span -> Type -> Checker (TypeScheme, Def () ())
 derivePull s ty = do
@@ -419,24 +452,26 @@ derivePull' s topLevel gamma argTy@(leftmostOfApplication -> TyCon name) arg = d
                     consParamsVars <- forM consParamsTypes (\_ -> freshIdentifierBase "y" <&> mkId)
                     debugM "consParamsVars: " (pretty consParamsVars)
 
+                    let makeArgPattern ty var = case ty of
+                          Box k ty -> PBox s () True (PVar s () True var)
+                          FunTy _ (Just k) _ _ -> PBox s () True (PVar s () True var)
+                          _ -> PVar s () True var
+
                     -- Build the pattern for this case
                     let consPattern =
-                          PConstr s () True dataConsName [] (zipWith (\ty var -> PBox s () True (PVar s () True var)) consParamsTypes consParamsVars)
+                          PConstr s () True dataConsName [] (zipWith (\ty var -> makeArgPattern ty var) consParamsTypes consParamsVars)
                     debugM "derive-pull" ("consPattern " <> pretty consPattern )
                     -- Push on all the parameters of a the constructor
                     retTysAndExprs <- zipWithM (\ty var -> do
                       debugM "derive-pull" ("Deriving argument of case for " <> pretty dataConsName <> " at type " <> pretty ty)
                       derivePull' s False gamma ty (makeVarUntyped var))
                                       consParamsTypes consParamsVars
-                    let (_retTys, exprs, coeffs) = unzip3 retTysAndExprs
+                    let (retTys, exprs, coeffs) = unzip3 retTysAndExprs
                     let coeffs' = coeffectMeet coeffs
-                    debugM "retTys: " (show _retTys)
-                    let bodyExpr = mkConstructorApplication s dataConsName dataConsType (reverse exprs) dataConsType
-                    let bodyExpr' = (\bExpr -> case coeffs' of
-                                             Just c -> makeBoxUntyped bExpr
-                                             Nothing -> bExpr)
-                                           bodyExpr
-                    return (_retTys, consPattern, bodyExpr', coeffs'))
+                    debugM "retTys: " (show retTys)
+                    bodyExpr <- mkConstrApp2 s dataConsName dataConsType (zip retTys exprs) dataConsType
+                    let bodyExpr' = makeBoxUntyped bodyExpr
+                    return (retTys, consPattern, bodyExpr', coeffs'))
 
               -- Got all the branches to make the following case now
 
@@ -450,6 +485,8 @@ derivePull' s topLevel gamma argTy@(leftmostOfApplication -> TyCon name) arg = d
               let patExprs = zip pats exprs
               debugM "res: " (pretty (Case s () True arg patExprs))
               case coeffs of
+                -- TODO is it really just supposed to return the first coeffect?
+                -- or should it take the meet of all the coeffects?
                 c:cs -> return (ty, Case s () True arg patExprs, c)
                 _ -> return (ty, Case s () True arg patExprs, Nothing)
 

frontend/tests/cases/positive/deriving/pull.gr

@@ -0,0 +1,19 @@
+import Nat
+
+-- rather nonsense constructor to exercise pull
+data Pullable t where
+    Not : Pullable t;
+    JustOne : t -> Pullable t -> Pullable t;
+    Evens : t -> t -> Pullable t -> Pullable t
+
+dropSome : forall {a : Type, n : Nat} . N n -> (Pullable a) [0..1] -> Pullable a
+dropSome Z [p] = p;
+dropSome (S n) [Not] = dropSome n [Not];
+dropSome (S n) [JustOne _ rest] = dropSome n [rest];
+dropSome (S n) [Evens _ x rest] = dropSome n [JustOne x rest]
+
+toBePulled : Pullable (Int [0..1])
+toBePulled = Evens [0] [1] (Evens [2] [3] (Evens [4] [5] (JustOne [6] Not)))
+
+main : Pullable Int
+main = dropSome (S (S (S Z))) (pull @Pullable toBePulled)

frontend/tests/cases/positive/deriving/pull.gr.output

@@ -0,0 +1 @@
+JustOne 3 (Evens 4 5 (JustOne 6 Not))

frontend/tests/cases/positive/deriving/pullList.gr

@@ -0,0 +1,11 @@
+import List
+import Nat
+
+dropElems : forall {a : Type, n: Nat} . N n -> (List a) [0..1] -> List a
+dropElems Z [xs] = xs;
+dropElems (S n) [Empty] = dropElems n [Empty];
+dropElems (S n) [Next _ xs] = dropElems n [xs]
+
+main : List Int
+main = dropElems (S (S Z)) (pull @List (Next [1] (Next [2] (Next [3] (Next [4] (Next [5] Empty))))))
+

frontend/tests/cases/positive/deriving/pullList.gr.output

@@ -0,0 +1 @@
+Next 3 (Next 4 (Next 5 Empty))

frontend/tests/cases/positive/deriving/pullVec.gr

@@ -0,0 +1,9 @@
+import Vec
+
+dropElems'
+  : forall {a : Type, m n : Nat}
+  . N m -> Vec n (a [0..1]) -> Vec (n - m) a
+dropElems' n vs = dropElems n (pull @(Vec n) vs)
+
+main : Vec 3 Int
+main = dropElems' (S (S Z)) (Cons [1] (Cons [2] (Cons [3] (Cons [4] (Cons [5] Nil)))))

frontend/tests/cases/positive/deriving/pullVec.gr.output

@@ -0,0 +1 @@
+Cons 3 (Cons 4 (Cons 5 Nil))

frontend/tests/cases/positive/deriving/readLines.gr

@@ -0,0 +1,39 @@
+import List
+
+listSnoc : forall {a: Type} . List a -> a -> List a
+listSnoc list elem = append_list list (singleton_list elem)
+
+readLinesFromHandle : (Handle R) -> String -> (List String) -> (List String) <{Open,Read,IOExcept,Close}>
+readLinesFromHandle handle line lines = let
+    (handle', eof) <- isEOF handle
+    in
+        if eof
+        then let
+            () <- closeHandle handle';
+            [_] : String [(0: Ext Nat)..Inf] <- pure (moveString line)
+        in pure lines
+        else let
+            (handle'', c) <- readChar handle' in let
+            [c'] : Char [(0 : Ext Nat)..∞] <- pure (moveChar c)
+        in if (charToInt c') == 10
+        then readLinesFromHandle handle'' "" (listSnoc lines line)
+        else readLinesFromHandle handle'' (stringSnoc line c') lines
+
+gradeLine : forall {n:Nat} . String -> String [n]
+gradeLine s = moveString s
+
+gradeLineList : forall {n:Nat} . List String -> List (String [n])
+gradeLineList Empty = Empty;
+gradeLineList (Next x xs) = Next (gradeLine x) (gradeLineList xs)
+
+readInputLines : forall {n: Nat} . String -> ((List String) [n]) <{Open,Read,IOExcept,Close}>
+readInputLines filename = let
+        handle <- openHandle ReadMode filename;
+        ungradedInputLines <- readLinesFromHandle handle "" Empty in let
+        gradedLines = gradeLineList ungradedInputLines
+    in
+        pure (pull@List gradedLines)
+
+main : forall {n : Nat} . ((List String) [n]) <{Open,Read,IOExcept,Close}>
+main = readInputLines "LICENSE"
+

frontend/tests/cases/positive/deriving/readLines.gr.output

@@ -0,0 +1 @@
+[Next "Copyright 2017 Dominic Orchard <D.A.Orchard@kent.ac.uk>" (Next "" (Next "Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:" (Next "" (Next "1. Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer." (Next "" (Next "2. Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution." (Next "" (Next "3. Neither the name of the copyright holder nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission." (Next "" (Next "THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS \"AS IS\" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE." Empty))))))))))]