Merge pull request #229 from granule-project/fractional

Fractional permissions for mutable and immutable borrowing

Author: dorchard

StdLib/List.gr

@@ -14,7 +14,7 @@ import Result
 import Maybe
 import Bool
 
-data List a where Empty; Next a (List a)
+data List a where Empty | Next a (List a)
 
 --- Append two lists
 append_list : forall {a : Type} . List a -> List a -> List a

StdLib/Vec.gr

@@ -128,11 +128,11 @@ uncons
 uncons (Cons x xs) = (x,xs)
 
 --- Split a vector at position 'n'
-split
+splitVec
   : forall {a : Type, m n : Nat}
   . N n -> (Vec (n + m) a) -> (Vec n a, Vec m a)
-split Z xs = (Nil, xs);
-split (S n) (Cons x xs) = let (xs', ys') = split n xs in (Cons x xs', ys')
+splitVec Z xs = (Nil, xs);
+splitVec (S n) (Cons x xs) = let (xs', ys') = splitVec n xs in (Cons x xs', ys')
 
 --- Sum a vector of integers (using `foldr`)
 sum

compiler/src/Language/Granule/Compiler/HSCodegen.hs

@@ -134,15 +134,18 @@ cgType (GrType.TyApp t1 t2) =
     t2' <- cgType t2
     return $ Hs.TyApp () t1' t2'
 cgType (GrType.Star _t t2) = cgType t2
+cgType (GrType.Borrow _t t2) = cgType t2
 cgType (GrType.TyInt i) = return mkUnit
 cgType (GrType.TyRational ri) = return mkUnit
+cgType (GrType.TyFraction ri) = return mkUnit
 cgType (GrType.TyGrade mt i) = return mkUnit
 cgType (GrType.TyInfix t1 t2 t3) = return mkUnit
 cgType (GrType.TySet p l_t) = return mkUnit
 cgType (GrType.TyCase t l_p_tt) = unsupported "cgType: tycase not implemented"
 cgType (GrType.TySig t t2) = unsupported "cgType: tysig not implemented"
 cgType (GrType.TyExists _ _ _) = unsupported "cgType: tyexists not implemented"
 cgType (GrType.TyForall _ _ _) = unsupported "cgType: tyforall not implemented"
+cgType (GrType.TyName _) = unsupported "cgType: tyname not implemented"
 
 isTupleType :: GrType.Type -> Bool
 isTupleType (GrType.TyApp (GrType.TyCon id) _) = id == Id "," ","

docs/style.css

@@ -12,11 +12,16 @@ body {
 }
 
 .code pre {
-  white-space: pre-wrap;       /* css-3 */
-  white-space: -moz-pre-wrap;  /* Mozilla, since 1999 */
-  white-space: -pre-wrap;      /* Opera 4-6 */
-  white-space: -o-pre-wrap;    /* Opera 7 */
-  word-wrap: break-word;       /* Internet Explorer 5.5+ */
+  white-space: pre-wrap;
+  /* css-3 */
+  white-space: -moz-pre-wrap;
+  /* Mozilla, since 1999 */
+  white-space: -pre-wrap;
+  /* Opera 4-6 */
+  white-space: -o-pre-wrap;
+  /* Opera 7 */
+  word-wrap: break-word;
+  /* Internet Explorer 5.5+ */
 }
 
 .inline {
@@ -65,6 +70,11 @@ body {
   color: rgb(194, 2, 50);
 }
 
+.perm,
+.perm span {
+  color: rgb(34, 102, 34);
+}
+
 #navigator {
   width: calc(25vw - 20px - 2 * 20px);
   margin: 0px;

examples/effects_nondet.gr

@@ -10,7 +10,7 @@ import List
 
 data Labels = Toss | Drop
 
--- Operations
+-- (Sigma functor) - Signature of operations
 data GameOps : Set Labels -> Type -> Type where
   FlipCoin : forall {r : Type} . () -> (Bool -> r) [2] -> GameOps {Toss} r;
   Fumble   : forall {r : Type} . () -> (Void -> r) [0] -> GameOps {Drop} r
@@ -33,7 +33,7 @@ foo = call FlipCoin ()
 
 -- Two coin flips, all good
 example1 : (Bool, Bool) <Eff (Set Labels) GameOps {Toss}>
-example1 = let
+example1 = let  -- do x <- ...
   x <- call FlipCoin ();
   y <- call FlipCoin ()
   in pure (x, y)

examples/parallelWithMutation.gr

@@ -0,0 +1,65 @@
+import Parallel
+import Prelude
+import Vec
+
+--- Convert an indexed natural number to an untyped int
+natToInt'
+  : forall {n : Nat}
+  . N n -> Int
+natToInt' Z = 0;
+natToInt' (S m) = 1 + natToInt' m
+
+toFloatArray : forall {n : Nat} . Vec n Float -> exists {id : Name} . *(FloatArray id)
+toFloatArray v =
+  let (n', v) = length' v
+  in unpack <id, arr> = newFloatArray (natToInt' n')
+  in pack <id, (toFloatArrayAux arr [0] v)> as exists {id : Name} . *(FloatArray id)
+
+toFloatArrayAux : forall {n : Nat, id : Name} . *(FloatArray id) -> Int [n] -> Vec n Float -> *(FloatArray id)
+toFloatArrayAux a [n] Nil = a;
+toFloatArrayAux a [n] (Cons x xs) =
+  toFloatArrayAux (writeFloatArray a n x) [n + 1] xs
+
+sumFromTo : forall {id : Name, f : Fraction} . & f (FloatArray id) ->  !Int -> !Int -> (Float, & f (FloatArray id))
+sumFromTo array [i] [n] =
+  if i == n
+    then (0.0, array)
+    else
+      let (x, a) = readFloatArray array i;
+          (y, arr) = sumFromTo a [i+1] [n]
+      in  (x + y, arr)
+
+-- A reference to a droppable value can be written to without violating linearity
+writeRef : forall {a : Type, id : Name} . {Dropable a} => a -> & 1 (Ref id a) -> & 1 (Ref id a)
+writeRef x r = let
+    (y, r') = swapRef r x;
+    () = drop@a y in r'
+
+parSum : forall {id id' : Name} . *(FloatArray id) -> *(Ref id' Float) -> *(Ref id' Float, FloatArray id)
+parSum array ref = let
+     ([n], array) : (!Int, *(FloatArray id))     = lengthFloatArray array;
+     compIn                                      = borrowPull (ref, array)
+  in flip withBorrow compIn (\compIn ->
+
+                let (ref, array)      = borrowPush compIn;
+                    (array1, array2)  = split array;
+
+                    -- Compute in parallel
+                    ((x, array1), (y, array2)) =
+                                par (\() -> sumFromTo array1 [0] [div n 2])
+                                    (\() -> sumFromTo array2 [div n 2] [n]);
+
+                    -- Update the reference
+                    ref'        = writeRef ((x : Float) + y) ref;
+                    compOut     = borrowPull (ref', join (array1, array2))
+
+                  in compOut)
+
+main : Float
+main =
+  unpack <id , arr> = toFloatArray (Cons 10.0 (Cons 20.0 (Cons 30.0 (Cons 40.0 Nil)))) in
+  unpack <id', ref> = newRef 0.0 in
+  let
+      (result, array) = borrowPush (parSum arr ref);
+      () = deleteFloatArray array
+  in freezeRef result

examples/simple-clone.gr

@@ -0,0 +1,4 @@
+example : ()
+example = unpack <id , a> = newFloatArray 3 in
+  clone (share a) as x in
+    unpack <id' , a'> = x in (deleteFloatArray a')

frontend/granule-frontend.cabal

@@ -71,6 +71,7 @@ library
   other-modules:
       Language.Granule.Checker.CoeffectsTypeConverter
       Language.Granule.Checker.Constraints.Compile
+      Language.Granule.Checker.Constraints.SFrac
       Language.Granule.Checker.Constraints.SymbolicGrades
       Language.Granule.Checker.Effects
       Language.Granule.Checker.Exhaustivity

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

@@ -663,6 +663,22 @@ checkExpr defs gam pol topLevel tau
       else
         throw $ TypeError { errLoc = s, tyExpected = TyCon $ mkId "DFloat", tyActual = tau }
 
+-- Clone
+-- Pattern match on an applicable of `uniqueBind fun e`
+checkExpr defs gam pol topLevel tau
+   expr@(App s a rf
+     (App _ _ _
+       (Val _ _ _ (Var _ (internalName -> "uniqueBind")))
+       (Val _ _ _ (Abs _ (PVar _ _ _ var) _ body)))
+     e) = do
+  debugM "checkExpr[Clone]" (pretty s <> " : " <> pretty tau)
+  (tau', gam, subst, elab) <- synthExpr defs gam pol expr
+  -- Check the return types match
+  (eqT, _, substTy) <- equalTypes s tau tau'
+  unless eqT $ throw TypeError{ errLoc = s, tyExpected = tau, tyActual = tau' }
+  substF <- combineSubstitutions s subst substTy
+  return (gam, subst, elab)
+
 -- Application checking
 checkExpr defs gam pol topLevel tau (App s a rf e1 e2) | (usingExtension GradedBase) = do
   debugM "checkExpr[App]-gradedBase" (pretty s <> " : " <> pretty tau)
@@ -745,6 +761,15 @@ checkExpr defs gam pol _ ty@(Star demand tau) (Val s _ rf (Nec _ e)) = do
     let elaborated = Val s ty rf (Nec tau elaboratedE)
     return (gam', subst, elaborated)
 
+checkExpr defs gam pol _ ty@(Borrow demand tau) (Val s _ rf (Ref _ e)) = do
+    debugM "checkExpr[Borrow]" (pretty s <> " : " <> pretty ty)
+
+    -- Checker the expression being borrowed
+    (gam', subst, elaboratedE) <- checkExpr defs gam pol False tau e
+
+    let elaborated = Val s ty rf (Ref tau elaboratedE)
+    return (gam', subst, elaborated)
+
 -- Check a case expression
 checkExpr defs gam pol True tau (Case s _ rf guardExpr cases) = do
   debugM "checkExpr[Case]" (pretty s <> " : " <> pretty tau)
@@ -888,8 +913,9 @@ synthExpr :: (?globals :: Globals)
 
 -- Hit an unfilled hole
 synthExpr _ ctxt _ (Hole s _ _ _ _) = do
+  st <- get
   debugM "synthExpr[Hole]" (pretty s)
-  throw $ InvalidHolePosition s
+  throw $ InvalidHolePosition s ctxt (tyVarContext st)
 
 -- Literals can have their type easily synthesised
 synthExpr _ _ _ (Val s _ rf (NumInt n))  = do
@@ -912,6 +938,51 @@ synthExpr _ _ _ (Val s _ rf (StringLiteral c)) = do
   let t = TyCon $ mkId "String"
   return (t, usedGhostVariableContext, [], Val s t rf (StringLiteral c))
 
+-- Clone
+-- Pattern match on an applicable of `uniqueBind fun e`
+synthExpr defs gam pol
+   expr@(App s a rf
+     (App _ _ _
+       (Val _ _ _ (Var _ (internalName -> "uniqueBind")))
+       (Val _ _ _ (Abs _ (PVar _ _ _ var) _ body)))
+     e) = do
+  debugM "synthExpr[uniqueBind]" (pretty s <> pretty expr)
+  -- Infer the type of e (the boxed argument)
+  (ty, ghostVarCtxt, subst0, elabE) <- synthExpr defs gam pol e
+  -- Check that ty is actually a boxed type
+  case ty of
+    Box r tyA -> do
+      -- existential type for the cloned var ((exists {id : Name} . *(Rename id a))
+      idVar <- mkId <$> freshIdentifierBase "id"
+      let clonedInputTy =
+            TyExists idVar (TyCon $ mkId "Name")
+              (Borrow (TyCon $ mkId "Star") (TyApp (TyApp (TyCon $ mkId "Rename") (TyVar idVar)) tyA))
+      let clonedAssumption = (var, Linear clonedInputTy)
+
+      debugM "synthExpr[uniqueBind]body" (pretty clonedAssumption)
+      -- synthesise the type of the body for the clone
+      (tyB, ghostVarCtxt', subst1, elabBody) <- synthExpr defs (clonedAssumption : gam) pol body
+
+      let contType = FunTy Nothing Nothing (Box r tyA) tyB
+      let funType  = FunTy Nothing Nothing clonedInputTy tyB
+      let cloneType = FunTy Nothing Nothing contType funType
+      let elab = App s tyB rf
+                  (App s contType rf (Val s cloneType rf (Var cloneType $ mkId "uniqueBind"))
+                     (Val s funType rf (Abs funType (PVar s clonedInputTy rf var) Nothing elabBody))) elabE
+
+      -- Add constraints of `clone`
+      -- Constraint that 1 : s <= r
+      (semiring, subst2, _) <- synthKind s r
+      let constraint = ApproximatedBy s (TyGrade (Just semiring) 1) r semiring
+      addConstraint constraint
+      -- Cloneable constraint
+      otherTypeConstraints <- enforceConstraints s [TyApp (TyCon $ mkId "Cloneable") tyA]
+      registerWantedTypeConstraints otherTypeConstraints
+
+      substFinal <- combineSubstitutions s subst0 subst1
+      return (tyB, ghostVarCtxt <> (deleteVar var ghostVarCtxt'), substFinal, elab)
+    _ -> throw TypeError{ errLoc = s, tyExpected = Box (TyVar $ mkId "a") (TyVar $ mkId "b"), tyActual = ty }
+
 -- Secret syntactic weakening
 synthExpr defs gam pol
     (App s _ _ (Val _ _ _ (Var _ (sourceName -> "weak__"))) v@(Val _ _ _ (Var _ x))) = do
@@ -1195,7 +1266,7 @@ synthExpr defs gam pol (TryCatch s _ rf e1 p mty e2 e3) = do
 
 -- Variables
 synthExpr defs gam _ (Val s _ rf (Var _ x)) = do
-   debugM "synthExpr[Var]" (pretty s)
+   debugM ("synthExpr[Var] - " <> pretty x) (pretty s)
 
    -- Try the local context
    case lookup x gam of
@@ -1387,6 +1458,25 @@ synthExpr defs gam pol (Val s _ rf (Nec _ e)) = do
   let elaborated = Val s finalTy rf (Nec t elaboratedE)
   return (finalTy, gam', subst, elaborated)
 
+-- Infer type for references
+synthExpr defs gam pol (Val s _ rf (Ref _ e)) = do
+  debugM "synthExpr[Ref]" (pretty s)
+
+   -- Create a fresh kind variable for this permission
+  vark <- freshIdentifierBase $ "kref_[" <> pretty (startPos s) <> "]"
+   -- remember this new kind variable in the kind environment
+  modify (\st -> st { tyVarContext = (mkId vark, (kguarantee, InstanceQ)) : tyVarContext st })
+
+   -- Create a fresh permission variable for the permission of the borrowed expression
+  var <- freshTyVarInContext (mkId $ "ref_[" <> pretty (startPos s) <> "]") (tyVar vark)
+
+  -- Synth type of necessitated expression
+  (t, gam', subst, elaboratedE) <- synthExpr defs gam pol e
+
+  let finalTy = Borrow (TyVar var) t
+  let elaborated = Val s finalTy rf (Ref t elaboratedE)
+  return (finalTy, gam', subst, elaborated)
+
 -- BinOp
 synthExpr defs gam pol (Binop s _ rf op e1 e2) = do
     debugM "synthExpr[BinOp]" (pretty s)

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

@@ -1,13 +1,12 @@
 {-# LANGUAGE GADTs #-}
 module Language.Granule.Checker.CoeffectsTypeConverter(includeOnlyGradeVariables, tyVarContextExistential) where
 
-import Control.Monad.Except (catchError)
 import Control.Monad.State.Strict
 import Data.Maybe(catMaybes, mapMaybe)
 
 import Language.Granule.Checker.Monad
 import Language.Granule.Checker.Predicates
-import Language.Granule.Checker.Kinding (checkKind)
+import Language.Granule.Checker.Kinding (requiresSolver)
 
 import Language.Granule.Context
 
@@ -22,9 +21,11 @@ includeOnlyGradeVariables :: (?globals :: Globals)
   => Span -> Ctxt (Type, b) -> Checker (Ctxt (Type, b))
 includeOnlyGradeVariables s xs = mapM convert xs >>= (return . catMaybes)
   where
-    convert (var, (t, q)) = (do
-      k <- checkKind s t kcoeffect <|> checkKind s t keffect
-      return $ Just (var, (t, q))) `catchError` const (return Nothing)
+    convert (var, (t, q)) = do
+      reqSolver <- requiresSolver s t
+      return $ if reqSolver
+        then Just (var, (t, q))
+        else Nothing
 
 tyVarContextExistential :: Checker (Ctxt (Type, Quantifier))
 tyVarContextExistential = do