Merge dev-minor

examples/set.gr

@@ -0,0 +1,23 @@
+language GradedBase
+
+data List a = Cons a (List a) | Nil
+
+data Privilege = Camera | Contacts | Location | Microphone
+
+getLocation : String [{Location}]
+getLocation = ["051.28°N 001.08°E"]
+
+getContacts : (List String) [{Contacts}]
+getContacts = [Cons "Alice" (Cons "Bob" (Cons "Carol" Nil))]
+
+example : (List String) [{Contacts, Location}]
+example =
+  let [location] : String [{Location}] = getLocation;
+      [contacts] : (List String) [{Contacts}] = getContacts
+  in [Cons location contacts]
+
+non-example : (List String) [{Contacts}]
+non-example =
+  let [location] : String [{Location}] = getLocation;
+      [contacts] : (List String) [{Contacts}] = getContacts
+  in [Cons location contacts]

frontend/src/Language/Granule/Checker/Checker.hs

@@ -1502,10 +1502,20 @@ synthExpr defs gam pol (Val s _ rf (Abs _ p Nothing e)) = do
 
   newConjunct
 
+  -- if graded base
+  scrutinee <-
+    if usingExtension GradedBase
+      then do
+        s <- freshTyVarInContext (mkId "s") kcoeffect
+        r <- freshTyVarInContext (mkId "scrutinee") (TyVar s)
+        return (Just (TyVar r, TyVar s))
+      else
+        return Nothing
+
   tyVar <- freshTyVarInContext (mkId "t") (Type 0)
   let sig = (TyVar tyVar)
 
-  (bindings, localVars, substP, elaboratedP, _) <- ctxtFromTypedPattern s InCase sig p NotFull
+  (bindings, localVars, substP, elaboratedP, _) <- ctxtFromTypedPattern' scrutinee s InCase sig p NotFull
 
   newConjunct
 
@@ -1514,9 +1524,10 @@ synthExpr defs gam pol (Val s _ rf (Abs _ p Nothing e)) = do
      (tau, gam'', subst, elaboratedE) <- synthExpr defs (bindings <> gam) pol e
 
      -- Locally we should have this property (as we are under a binder)
+     debugM "abs-inner-check:" (pretty (gam'' `intersectCtxts` bindings) <> "<: " <> pretty bindings)
      subst0 <- ctxtApprox s (gam'' `intersectCtxts` bindings) bindings
 
-     let finalTy = FunTy Nothing Nothing sig tau
+     let finalTy = FunTy Nothing (fmap fst scrutinee) sig tau
      let elaborated = Val s finalTy rf (Abs finalTy elaboratedP (Just sig) elaboratedE)
      finalTy' <- substitute substP finalTy
      substFinal <- combineManySubstitutions s [subst0, substP, subst]

frontend/src/Language/Granule/Checker/Constraints.hs

@@ -258,7 +258,7 @@ freshSolverVarScoped quant name (isExt -> Just t) q k =
 freshSolverVarScoped quant name (TyVar v) q k =
   quant q name (\solverVar -> k (sTrue, SUnknown $ SynLeaf $ Just solverVar))
 
-freshSolverVarScoped quant name (Language.Granule.Syntax.Type.isSet -> Just (elemTy, polarity)) q k =
+freshSolverVarScoped quant name (isSet -> Just (elemTy, polarity)) q k =
       quant q name (\solverVar -> k (inUniverse solverVar, SSet polarity solverVar))
     where
 
@@ -458,8 +458,8 @@ compileCoeffect (TyGrade k' n) k _ | k == extendedNat && (k' == Nothing || k' ==
 compileCoeffect (TyRational r) (TyCon k) _ | internalName k == "Q" =
   return (SFloat  . fromRational $ r, sTrue)
 
-compileCoeffect (TySet _ xs) (Language.Granule.Syntax.Type.isSet -> Just (elemTy, polarity)) _ =
-    return ((SSet polarity) . S.fromList $ mapMaybe justTyConNames xs, sTrue)
+compileCoeffect (TySet _ xs) (isSet -> Just (elemTy, polarity)) _ =
+    return (SSet polarity . S.fromList $ mapMaybe justTyConNames xs, sTrue)
   where
     justTyConNames (TyCon x) = Just (internalName x)
     justTyConNames t = error $ "Cannot have a type " ++ show t ++ " in a symbolic list"
@@ -538,8 +538,8 @@ compileCoeffect (TyGrade k' 0) k vars = do
 
     (isSet -> Just (elemTy, polarity)) ->
       case polarity of
-        Normal   -> setEmpty polarity
-        Opposite -> setUniverse polarity elemTy
+        Normal   -> setUniverse polarity elemTy
+        Opposite -> setEmpty polarity
 
     (TyVar _) -> return (SUnknown (SynLeaf (Just 0)), sTrue)
 
@@ -578,8 +578,8 @@ compileCoeffect (TyGrade k' 1) k vars = do
 
     (isSet -> Just (elemTy, polarity)) ->
       case polarity of
-        Normal   -> setUniverse polarity elemTy
-        Opposite -> setEmpty polarity
+        Normal   -> setEmpty polarity
+        Opposite -> setUniverse polarity elemTy
 
     (TyVar _) -> return (SUnknown (SynLeaf (Just 1)), sTrue)
 
@@ -632,10 +632,10 @@ approximatedByOrEqualConstraint (SFloat n) (SFloat m)  = return $ n .<= m
 approximatedByOrEqualConstraint SPoint SPoint          = return $ sTrue
 approximatedByOrEqualConstraint (SOOZ s) (SOOZ r) = pure $ s .== r
 approximatedByOrEqualConstraint (SSet Normal s) (SSet Normal t) =
-  pure $ s `S.isSubsetOf` t
+  pure $ t `S.isSubsetOf` s
 
 approximatedByOrEqualConstraint (SSet Opposite s) (SSet Opposite t) =
-  pure $ t `S.isSubsetOf` s
+  pure $ s `S.isSubsetOf` t
 
 
 approximatedByOrEqualConstraint (SLevel l) (SLevel k) =

frontend/src/Language/Granule/Checker/Constraints/Compile.hs

@@ -1,4 +1,3 @@
-{-# LANGUAGE TypeSynonymInstances #-}
 {-# LANGUAGE ImplicitParams #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE DataKinds #-}
@@ -116,6 +115,9 @@ isDefinedConstraint s (TyApp (TyCon (internalName -> "Sends")) protocol)
 isDefinedConstraint s (TyApp (TyCon (internalName -> "ExactSemiring")) semiring)
   = return (exactSemiring semiring)
 
+isDefinedConstraint s (TyApp (TyCon (internalName -> "NonInterfering")) semiring)
+  = return (nonInterfering semiring)
+
 isDefinedConstraint s (TyApp (TyCon (internalName -> "Dropable")) typ)
   = return (dropable typ)
 
@@ -168,15 +170,22 @@ exactSemiring (TyApp
                  s2) = exactSemiring s1 && exactSemiring s2
 exactSemiring _ = False
 
+nonInterfering :: Type -> Bool
+nonInterfering (TyCon (internalName -> "Level")) = True
+nonInterfering (TyCon (internalName -> "Set")) = True
+nonInterfering (TyCon (internalName -> "SetOp")) = True
+nonInterfering (TyApp (TyApp (TyCon (internalName -> ",,")) s1) s2) = nonInterfering s1 && nonInterfering s2
+nonInterfering _ = False
+
 dropable :: Type -> Bool
 dropable =
     runIdentity . typeFoldM (TypeFold
-      { tfTy = \_ -> return $ True
+      { tfTy = \_ -> return True
       , tfFunTy = \_ c x y -> return y
-      , tfTyCon = \id -> return $ not (id `elem` nonDropable)
+      , tfTyCon = \id -> return $ notElem id nonDropable
       , tfBox = \x y -> return (x && y)
-      , tfDiamond = \x y -> return $ (x && y)
-      , tfStar = \x y -> return $ (x && y)
+      , tfDiamond = \x y -> return (x && y)
+      , tfStar = \x y -> return (x && y)
       , tfTyVar = \_ -> return False
       , tfTyApp = \x y -> return x
       , tfTyInt = \_ -> return True

frontend/src/Language/Granule/Checker/Constraints/SymbolicGrades.hs

@@ -298,8 +298,8 @@ symGradeEq s t = solverError $ cannotDo ".==" s t
 -- | Meet operation on symbolic grades
 symGradeMeet :: SGrade -> SGrade -> Symbolic SGrade
 symGradeMeet (SNat n1) (SNat n2)     = return $ SNat $ n1 `smin` n2
-symGradeMeet (SSet Normal s) (SSet Normal t) = return $ SSet Normal $ S.union s t
-symGradeMeet (SSet Opposite s) (SSet Opposite t) = return $ SSet Opposite $ S.intersection s t
+symGradeMeet (SSet Normal s) (SSet Normal t)     = return $ SSet Normal $ S.intersection s t
+symGradeMeet (SSet Opposite s) (SSet Opposite t) = return $ SSet Opposite $ S.union s t
 symGradeMeet (SLevel s) (SLevel t) =
   -- Using the join (!) from the Agda code (by cases)
   return $ SLevel $ ite (s .== literal unusedRepresentation) t -- join Unused x = x
@@ -334,8 +334,8 @@ symGradeMeet s t = solverError $ cannotDo "meet" s t
 -- | Join operation on symbolic grades
 symGradeJoin :: SGrade -> SGrade -> Symbolic SGrade
 symGradeJoin (SNat n1) (SNat n2) = return $ SNat (n1 `smax` n2)
-symGradeJoin (SSet Normal s) (SSet Normal t)   = return $ SSet Normal $ S.intersection s t
-symGradeJoin (SSet Opposite s) (SSet Opposite t) = return $ SSet Opposite $ S.union s t
+symGradeJoin (SSet Normal s) (SSet Normal t)     = return $ SSet Normal $ S.union s t
+symGradeJoin (SSet Opposite s) (SSet Opposite t) = return $ SSet Opposite $ S.intersection s t
 symGradeJoin (SLevel s) (SLevel t) =
   -- Using the meet (!) from the Agda code (by cases)
   return $ SLevel $ ite (s .== literal unusedRepresentation) t -- meet Unused x = x
@@ -383,8 +383,8 @@ symGradeJoin s t = solverError $ cannotDo "join" s t
 -- | Plus operation on symbolic grades
 symGradePlus :: SGrade -> SGrade -> Symbolic SGrade
 symGradePlus (SNat n1) (SNat n2) = return $ SNat (n1 + n2)
-symGradePlus (SSet Normal s) (SSet Normal t) = return $ SSet Normal $ S.union s t
-symGradePlus (SSet Opposite s) (SSet Opposite t) = return $ SSet Opposite $ S.intersection s t
+symGradePlus (SSet Normal s) (SSet Normal t) = return $ SSet Normal $ S.intersection s t
+symGradePlus (SSet Opposite s) (SSet Opposite t) = return $ SSet Opposite $ S.union s t
 symGradePlus (SLevel lev1) (SLevel lev2) = symGradeJoin (SLevel lev1) (SLevel lev2)
 symGradePlus (SFloat n1) (SFloat n2) = return $ SFloat $ n1 + n2
 symGradePlus (SExtNat x) (SExtNat y) = return $ SExtNat (x + y)
@@ -432,8 +432,8 @@ symGradeTimes :: SGrade -> SGrade -> Symbolic SGrade
 symGradeTimes (SNat n1) (SNat n2) = return $ SNat (n1 * n2)
 symGradeTimes (SNat n1) (SExtNat (SNatX n2)) = return $ SExtNat $ SNatX (n1 * n2)
 symGradeTimes (SExtNat (SNatX n1)) (SNat n2) = return $ SExtNat $ SNatX (n1 * n2)
-symGradeTimes (SSet Normal s) (SSet Normal t) = return $ SSet Normal $ S.intersection s t
-symGradeTimes (SSet Opposite s) (SSet Opposite t) = return $ SSet Opposite $ S.union s t
+symGradeTimes (SSet Normal s) (SSet Normal t) = return $ SSet Normal $ S.union s t
+symGradeTimes (SSet Opposite s) (SSet Opposite t) = return $ SSet Opposite $ S.intersection s t
 symGradeTimes (SLevel lev1) (SLevel lev2) = symGradeJoin (SLevel lev1) (SLevel lev2)
 symGradeTimes (SFloat n1) (SFloat n2) = return $ SFloat $ n1 * n2
 symGradeTimes (SExtNat x) (SExtNat y) = return $ SExtNat (x * y)

frontend/src/Language/Granule/Checker/Kinding.hs

@@ -955,7 +955,7 @@ cProduct x y = TyApp (TyApp (TyCon (mkId ",,")) x) y
 -- | Find out whether a coeffect if flattenable, and if so get the operation
 -- | used to represent flattening on the grades
 flattenable :: (?globals :: Globals)
-            => Type -> Type -> Checker (Maybe ((Coeffect -> Coeffect -> Coeffect), Substitution, Type))
+            => Type -> Type -> Checker (Maybe (Coeffect -> Coeffect -> Coeffect, Substitution, Type))
 flattenable t1 t2
  | t1 == t2 = case t1 of
     t1 | t1 == extendedNat -> return $ Just (TyInfix TyOpTimes, [], t1)
@@ -969,7 +969,7 @@ flattenable t1 t2
     -- Sets can use multiply to fold two levels
     (isSet -> Just (elemType, polarity)) -> return $ Just (TyInfix TyOpTimes, [], t1)
 
-    _ -> return $ Nothing
+    _ -> return Nothing
  | otherwise =
       case (t1, t2) of
         (isInterval -> Just t, TyCon (internalName -> "LNL")) | t == extendedNat ->
@@ -1301,4 +1301,3 @@ instance Unifiable t => Unifiable (Maybe t) where
     unify' Nothing _ = return []
     unify' _ Nothing = return []
     unify' (Just x) (Just y) = unify' x y
-

frontend/src/Language/Granule/Checker/Patterns.hs

@@ -371,7 +371,7 @@ ctxtFromTypedPattern' _ s _ t p _ = do
   debugM "dataConstructors in checker state" $ show $ dataConstructors st
   case t of
     (Star _ t') -> throw $ UniquenessError { errLoc = s, uniquenessMismatch = UniquePromotion t'}
-    otherwise -> throw $ PatternTypingError { errLoc = s, errPat = p, tyExpected = t }
+    _ -> throw PatternTypingError { errLoc = s, errPat = p, tyExpected = t }
 
 flattenCoeffects :: (?globals :: Globals) => Span -> Maybe (Coeffect, Type) -> Maybe (Coeffect, Type) -> Checker (Maybe (Coeffect, Type), Substitution)
 flattenCoeffects s Nothing Nothing | usingExtension GradedBase = do

frontend/src/Language/Granule/Checker/Primitives.hs

@@ -53,9 +53,9 @@ overlapsAllowed =
 typeConstructors :: (?globals :: Globals) => [(Id, (Type, [Id], [Int]))]
 typeConstructors =
   -- If we have the security levels extension turned on then include these things
-  (extensionDependent [(SecurityLevels, [(mkId "Level",    (kcoeffect, [], []))
+  extensionDependent [(SecurityLevels, [ (mkId "Level",    (kcoeffect, [], []))
                                        , (mkId "Unused",   (tyCon "Level", [], []))
-                                       , (mkId "Dunno",    (tyCon "Level", [], []))])] [])
+                                       , (mkId "Dunno",    (tyCon "Level", [], []))])] []
  ++
   -- Everything else is always in scope
     [ (mkId "Coeffect",  (Type 2, [], []))
@@ -70,16 +70,17 @@ typeConstructors =
     , (mkId "Char",   (Type 0, [], []))
     , (mkId "Void",   (Type 0, [], []))
     , (mkId "String", (Type 0, [], []))
-    , (mkId "Inverse", ((funTy (Type 0) (Type 0)), [], []))
+    , (mkId "Inverse", (funTy (Type 0) (Type 0), [], []))
     -- Predicates on deriving operations:x
     , (mkId "Dropable", (funTy (Type 0) kpredicate, [], [0]))
     -- TODO: add deriving for this
     -- , (mkId "Moveable", (funTy (Type 0) kpredicate, [], [0]))
     -- Session type related things
     , (mkId "ExactSemiring", (funTy (tyCon "Semiring") (tyCon "Predicate"), [], []))
+    , (mkId "NonInterfering", (funTy (tyCon "Coeffect") (tyCon "Predicate"), [], []))
     , (mkId "Protocol", (Type 0, [], []))
-    , (mkId "SingleAction", ((funTy (tyCon "Protocol") (tyCon "Predicate")), [], [0]))
-    , (mkId "ReceivePrefix", ((funTy (tyCon "Protocol") (tyCon "Predicate")), [], [0]))
+    , (mkId "SingleAction", (funTy (tyCon "Protocol") (tyCon "Predicate"), [], [0]))
+    , (mkId "ReceivePrefix", (funTy (tyCon "Protocol") (tyCon "Predicate"), [], [0]))
     , (mkId "Sends", (funTy (tyCon "Nat") (funTy (tyCon "Protocol") (tyCon "Predicate")), [], [0]))
     , (mkId "Graded", (funTy (tyCon "Nat") (funTy (tyCon "Protocol") (tyCon "Protocol")), [], [0]))
 
@@ -793,4 +794,3 @@ builtins :: [(Id, TypeScheme)]
 -- List of primitives that can't be promoted in CBV
 unpromotables :: [String]
 unpromotables = ["newFloatArray", "forkLinear", "forkMulticast", "forkReplicate", "forkReplicateExactly"]
-

frontend/src/Language/Granule/Syntax/Def.hs

@@ -262,11 +262,15 @@ instance Monad m => Freshenable m (Def v a) where
 instance Term (EquationList v a) where
   freeVars (EquationList _ name _ eqs) =
     delete name (concatMap freeVars eqs)
+  hasHole (EquationList _ name _ eqs) = any hasHole eqs
 
 instance Term (Equation v a) where
   freeVars (Equation s _ a _ binders body) =
       freeVars body \\ concatMap boundVars binders
+  hasHole (Equation _ _ _ _ _ body) = hasHole body
 
 instance Term (Def v a) where
   freeVars (Def _ name _ _ equations _) =
     delete name (freeVars equations)
+  hasHole (Def _ name _ _ equations _) =
+    hasHole equations

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

@@ -16,6 +16,7 @@ import Language.Granule.Syntax.Expr
 import Language.Granule.Syntax.Type
 import Language.Granule.Syntax.Identifiers
 -- import Control.Monad.Logic
+import Language.Granule.Syntax.Helpers hiding (freshIdentifierBase)
 import Language.Granule.Syntax.Pretty
 import Language.Granule.Syntax.Pattern
 import Language.Granule.Syntax.Span
@@ -513,7 +514,11 @@ runExamples eval ast@(AST decls defs imports hidden mod) examples defId = do
           map (\(Example input output _) -> makeEquality input output) examples'
     -- remove the existing main function (should probably keep the main function so we can stitch it back in after)
 
-    let defsWithoutMain = filter (\(Def _ mIdent _ _ _ _) -> mIdent /= mkId entryPoint) defs
+    let defsWithoutMain =
+         filter (\(Def _ mIdent _ _ defs _) ->
+                       mIdent /= mkId entryPoint
+                       -- filter out any definitions that have a hole
+                    && not (hasHole defs)) defs
 
     let foundBoolDecl = find (\(DataDecl _ dIdent _ _ _) ->  dIdent == mkId "Bool") decls
     let declsWithBool = case foundBoolDecl of

frontend/tests/cases/positive/graded-base/nestedLambda.gr

@@ -0,0 +1,4 @@
+-- gr --no-eval
+language GradedBase
+quad' : forall {a : Type}. a % 4 -> ((a, a), (a, a))
+quad' = \x -> (\y -> (y, y)) (x, x)

interpreter/src/Language/Granule/Interpreter.hs

@@ -66,7 +66,15 @@ main :: IO ()
 main = do
     (globPatterns, config) <- getGrConfig
     if grShowVersion config
-      then putStrLn $ "Granule version " <> showVersion version
+      then
+        putStrLn $ unlines
+          [ "The Granule Interpreter"
+          , "version: "     <> showVersion version
+          , "branch: "      <> $(gitBranch)
+          , "commit hash: " <> $(gitHash)
+          , "commit date: " <> $(gitCommitDate)
+          , if $(gitDirty) then "(uncommitted files present)" else ""
+          ]
       else
         if null globPatterns
           then runGrOnStdIn config