Merge pull request #363 from edwinb/lineario

More on the Linear IO experiment

libs/contrib/Control/Linear/LIO.idr

@@ -1,7 +1,5 @@
 module Control.Linear.LIO
 
-import public Data.So
-
 ||| Like `Monad`, but the action and continuation must be run exactly once
 ||| to ensure that the computation is linear.
 public export
@@ -16,68 +14,87 @@ LinearBind IO where
 public export
 data Usage = None | Linear | Unrestricted
 
--- Not sure about this - it is a horrible hack, but it makes the notation
--- a bit nicer and consistent with the numbering on binders!
+-- Not sure about this, it is a horrible hack, but it makes the notation
+-- a bit nicer
 public export 
-fromInteger : (x : Integer) -> {auto _ : So (x == 0 || x == 1)} -> Usage
+fromInteger : (x : Integer) -> {auto _ : Either (x = 0) (x = 1)} -> Usage
 fromInteger 0 = None
 fromInteger 1 = Linear
 fromInteger x = Unrestricted
 
-||| A wrapper which allows operations to state the multiplicity of the value
-||| they return. For example, `L IO {u=1} File` is an IO operation which returns
-||| a file that must be used exactly once.
-export
-data L : (Type -> Type) ->
-         {default Unrestricted use : Usage} ->
-         Type -> Type where
-     MkL : (1 _ : io a) -> L io {use} a
-
-||| Run a linear program with unrestricted return value in the underlying
-||| context
-export
-run : L io a -> io a
-run (MkL p) = p
-
 public export
 0 ContType : (Type -> Type) -> Usage -> Usage -> Type -> Type -> Type
+
+||| A wrapper which allows operations to state the multiplicity of the value
+||| they return. For example, `L IO {use=1} File` is an IO operation which
+||| returns a file that must be used exactly once.
+-- This is uglier than I'd like. Perhaps multiplicity polymorphism would make
+-- it neater, but we don't have that (yet?), and fortunately none of this
+-- horror has to be exposed to the user!
+export
+data L : (io : Type -> Type) ->
+         {default Unrestricted use : Usage} ->
+         (ty : Type) -> Type where
+     [search ty]
+     -- Three separate Pures, because we need to distinguish how they are
+     -- used, and this is neater than a continuation.
+     Pure0 : (0 _ : a) -> L io {use=0} a
+     Pure1 : (1 _ : a) -> L io {use=1} a
+     PureW : a -> L io a
+     -- The action is always run once, and the type makes an assertion about
+     -- how often it's safe to use the result.
+     Action : (1 _ : io a) -> L io {use} a
+     Bind : {u_act : _} ->
+            (1 _ : L io {use=u_act} a) ->
+            (1 _ : ContType io u_act u_k a b) ->
+            L io {use=u_k} b
+
 ContType io None u_k a b = (0 _ : a) -> L io {use=u_k} b
 ContType io Linear u_k a b = (1 _ : a) -> L io {use=u_k} b
 ContType io Unrestricted u_k a b = a -> L io {use=u_k} b
 
-export %inline
-lio_bind : {u_act : _} ->
-           LinearBind io =>
-           (1 _ : L io {use=u_act} a) ->
-           (1 _ : ContType io u_act u_k a b) -> L io {use=u_k} b
-lio_bind {u_act = None} (MkL act) k
-    = let (>>=) = bindL in
-          MkL $ do a' <- act
-                   let MkL ka' = k a'
-                   ka'
-lio_bind {u_act = Linear} (MkL act) k
-    = let (>>=) = bindL in
-          MkL $ do a' <- act
-                   let MkL ka' = k a'
-                   ka'
-lio_bind {u_act = Unrestricted} (MkL act) k
-    = let (>>=) = bindL in
-          MkL $ do a' <- act
-                   let MkL ka' = k a'
-                   ka'
+RunCont : Usage -> Type -> Type -> Type
+RunCont None t b = (0 _ : t) -> b
+RunCont Linear t b = (1 _ : t) -> b
+RunCont Unrestricted t b = t -> b
+
+-- The repetition here is annoying, but necessary because we don't have
+-- multiplicity polymorphism. We need to look at the usage to know what the
+-- concrete type of the continuation is.
+runK : {use : _} ->
+       LinearBind io =>
+       (1 _ : L io {use} a) -> (1 _ : RunCont use a (io b)) -> io b
+runK (Pure0 x) k = k x
+runK (Pure1 x) k = k x
+runK (PureW x) k = k x
+runK {use = None} (Action x) k = bindL x $ \x' => k x'
+runK {use = Linear} (Action x) k = bindL x $ \x' => k x'
+runK {use = Unrestricted} (Action x) k = bindL x $ \x' => k x'
+runK (Bind {u_act = None} act next) k = runK act (\x => runK (next x) k)
+runK (Bind {u_act = Linear} act next) k = runK act (\x => runK (next x) k)
+runK (Bind {u_act = Unrestricted} act next) k = runK act (\x => runK (next x) k)
+
+||| Run a linear program exactly once, with unrestricted return value in the
+||| underlying context
+run : (Applicative io, LinearBind io) =>
+      (1 _ : L io a) -> io a
+run prog = runK prog pure
 
 export
-Functor io => Functor (L io {use}) where
-  map fn (MkL act) = MkL (map fn act)
+Functor io => Functor (L io) where
+  map fn act = Bind act \a' => PureW (fn a')
 
 export
-Applicative io => Applicative (L io {use}) where
-  pure = MkL . pure
-  (<*>) (MkL f) (MkL a) = MkL (f <*> a)
+Applicative io => Applicative (L io) where
+  pure = PureW
+  (<*>) f a
+      = f `Bind` \f' =>
+        a `Bind` \a' =>
+        PureW (f' a')
 
 export
 (Applicative m, LinearBind m) => Monad (L m) where
-  (>>=) = lio_bind
+  (>>=) = Bind
 
 -- prioritise this one for concrete LIO, so we get the most useful
 -- linearity annotations.
@@ -86,18 +103,20 @@ export %inline
         LinearBind io =>
         (1 _ : L io {use=u_act} a) ->
         (1 _ : ContType io u_act u_k a b) -> L io {use=u_k} b
-(>>=) = lio_bind
+(>>=) = Bind
+
+export %inline
+pure0 : (0 x : a) -> L io {use=0} a
+pure0 = Pure0
+
+export %inline
+pure1 : (1 x : a) -> L io {use=1} a
+pure1 = Pure1
 
 export
 (LinearBind io, HasIO io) => HasIO (L io) where
-  liftIO p = MkL (liftIO p)
+  liftIO p = Action (liftIO p)
 
 public export
 LinearIO : (Type -> Type) -> Type
 LinearIO io = (LinearBind io, HasIO io)
-
--- Since the usage won't be known, we need this to be a %defaulthint to allow
--- using arbitrary IO operations at unrestricted multiplicity.
-export %defaulthint
-unrLIO : LinearBind io => HasIO io => HasIO (L io)
-unrLIO = %search

src/Core/AutoSearch.idr

@@ -434,13 +434,22 @@ concreteDets {vars} fc defaults env top pos dets (arg :: args)
                  concrete defs argnf True
                  concreteDets fc defaults env top (1 + pos) dets args
   where
+    drop : Nat -> List Nat -> List t -> List t
+    drop i ns [] = []
+    drop i ns (x :: xs)
+        = if i `elem` ns
+             then x :: drop (1+i) ns xs
+             else drop (1+i) ns xs
+
     concrete : Defs -> NF vars -> (atTop : Bool) -> Core ()
     concrete defs (NBind nfc x b sc) atTop
         = do scnf <- sc defs (toClosure defaultOpts env (Erased nfc False))
              concrete defs scnf False
     concrete defs (NTCon nfc n t a args) atTop
-        = do traverse (\ parg => do argnf <- evalClosure defs parg
-                                    concrete defs argnf False) args
+        = do sd <- getSearchData nfc False n
+             let args' = drop 0 (detArgs sd) args
+             traverse (\ parg => do argnf <- evalClosure defs parg
+                                    concrete defs argnf False) args'
              pure ()
     concrete defs (NDCon nfc n t a args) atTop
         = do traverse (\ parg => do argnf <- evalClosure defs parg

src/Core/TT.idr

@@ -1254,6 +1254,10 @@ export
       showApp (Bind _ x (Pi c AutoImplicit ty) sc) []
           = "{auto " ++ showCount c ++ show x ++ " : " ++ show ty ++
             "} -> " ++ show sc
+      showApp (Bind _ x (Pi c (DefImplicit tm) ty) sc) []
+          = "{default " ++ show tm ++ " "
+                ++ showCount c ++ show x ++ " : " ++ show ty ++
+            "} -> " ++ show sc
       showApp (Bind _ x (PVar c Explicit ty) sc) []
           = "pat " ++ showCount c ++ show x ++ " : " ++ show ty ++
             " => " ++ show sc

src/TTImp/Elab.idr

@@ -251,13 +251,20 @@ checkTermSub defining mode opts nest env env' sub tm ty
                               _ => throw err)
          pure (fst res)
   where
+    bindImps' : {vs : _} ->
+                FC -> Env Term vs -> List (Name, Term vs) -> RawImp ->
+                Core RawImp
+    bindImps' loc env [] ty = pure ty
+    bindImps' loc env ((n, ty) :: ntys) sc
+        = pure $ IPi loc erased Implicit (Just n)
+                     (Implicit loc True) !(bindImps' loc env ntys sc)
+
     bindImps : {vs : _} ->
                FC -> Env Term vs -> List (Name, Term vs) -> RawImp ->
                Core RawImp
-    bindImps loc env [] ty = pure ty
-    bindImps loc env ((n, ty) :: ntys) sc
-        = pure $ IPi loc erased Implicit (Just n)
-                     !(unelabNoSugar env ty) !(bindImps loc env ntys sc)
+    bindImps loc env ns (IBindHere fc m ty)
+        = pure $ IBindHere fc m !(bindImps' loc env ns ty)
+    bindImps loc env ns ty = bindImps' loc env ns ty
 
 export
 checkTerm : {vars : _} ->

src/TTImp/Elab/App.idr

@@ -266,6 +266,7 @@ mutual
                 _ => pure True
   needsDelayExpr True (IApp _ f _) = needsDelayExpr True f
   needsDelayExpr True (IImplicitApp _ f _ _) = needsDelayExpr True f
+  needsDelayExpr True (ILam _ _ _ _ _ _) = pure True
   needsDelayExpr True (ICase _ _ _ _) = pure True
   needsDelayExpr True (ILocal _ _ _) = pure True
   needsDelayExpr True (IUpdate _ _ _) = pure True

src/TTImp/Elab/Binders.idr

@@ -141,6 +141,10 @@ checkLambda rig_in elabinfo nest env fc rigl info n argTy scope Nothing
           inferLambda rig elabinfo nest env fc rigl info n argTy scope Nothing
 checkLambda rig_in elabinfo nest env fc rigl info n argTy scope (Just expty_in)
     = do let rig = the RigCount $ if isErased rig_in then erased else linear
+         let solvemode = case elabMode elabinfo of
+                              InLHS _ => inLHS
+                              _ => inTermP False
+         solveConstraints solvemode Normal
          expty <- getTerm expty_in
          exptynf <- getTyNF env expty
          defs <- get Ctxt

tests/Main.idr

@@ -71,6 +71,7 @@ idrisTests
        -- QTT and linearity related
        "linear001", "linear002", "linear003", "linear004", "linear005",
        "linear006", "linear007", "linear008", "linear009", "linear010",
+       "linear011",
        -- Namespace blocks
        "namespace001",
        -- Parameters blocks

tests/idris2/coverage008/expected

@@ -1,6 +1,6 @@
 1/1: Building wcov (wcov.idr)
 Main> Main.tfoo is total
 Main> Main.wfoo is total
-Main> Main.wbar is not covering due to call to function Main.with block in 1387
+Main> Main.wbar is not covering due to call to function Main.with block in 1393
 Main> Main.wbar1 is total
 Main> Bye for now!

tests/idris2/coverage010/expected

@@ -3,4 +3,4 @@ casetot.idr:12:1--13:1:main is not covering at:
 12	main : IO ()
 13	main = do
 
-	Calls non covering function Main.case block in 2114(619)
+	Calls non covering function Main.case block in 2145(622)

tests/idris2/linear011/Network.idr

@@ -0,0 +1,33 @@
+import Control.Linear.LIO
+
+import Network.Socket
+
+data SocketState = Ready | Bound | Listening | Open | Closed
+
+data Socket : SocketState -> Type where
+     MkSocket : Socket.Data.Socket -> Socket st
+
+newSocket : LinearIO io
+      => (fam  : SocketFamily)
+      -> (ty   : SocketType)
+      -> (pnum : ProtocolNumber)
+      -> (success : (1 _ : Socket Ready) -> L io ())
+      -> (fail : SocketError -> L io ())
+      -> L io ()
+newSocket fam ty pnum success fail
+    = do Right rawsock <- socket fam ty pnum
+               | Left err => fail err
+         success (MkSocket rawsock)
+
+bind : LinearIO io =>
+       (1 _ : Socket Ready) ->
+       (addr : Maybe SocketAddress) ->
+       (port : Port) ->
+       L io {use=1} (Res Bool (\res => Socket (case res of
+                                                    False => Closed
+                                                    True => Bound)))
+bind (MkSocket sock) addr port
+    = do ok <- Socket.bind sock addr port
+         if ok == 0
+            then pure1 (True # ?foo1)
+            else pure1 (False # ?foo2)

tests/idris2/linear011/expected

@@ -0,0 +1,17 @@
+1/1: Building Network (Network.idr)
+Main>  0 io : Type -> Type
+   sock : Socket
+   port : Int
+   addr : Maybe SocketAddress
+   ok : Int
+-------------------------------------
+foo1 : Socket Bound
+Main>  0 io : Type -> Type
+   sock : Socket
+   port : Int
+   addr : Maybe SocketAddress
+   ok : Int
+-------------------------------------
+foo2 : Socket Closed
+Main> 
+Bye for now!

tests/idris2/linear011/input

@@ -0,0 +1,2 @@
+:t foo1
+:t foo2

tests/idris2/linear011/run

@@ -0,0 +1,3 @@
+$1 --no-banner Network.idr -p contrib -p network < input
+
+rm -rf build

tests/idris2/reflection003/expected

@@ -1,6 +1,6 @@
 1/1: Building refprims (refprims.idr)
 LOG 0: Name: Prelude.List.++
-LOG 0: Type: (%pi Rig0 Implicit (Just a) %type (%pi Rig1 Explicit (Just xs) (Prelude.List a) (%pi RigW Explicit (Just {arg:6371}) (Prelude.List a) (Prelude.List a))))
+LOG 0: Type: (%pi Rig0 Implicit (Just a) %type (%pi Rig1 Explicit (Just xs) (Prelude.List a) (%pi RigW Explicit (Just {arg:6310}) (Prelude.List a) (Prelude.List a))))
 LOG 0: Name: Prelude.Strings.++
 LOG 0: Type: (%pi Rig1 Explicit (Just x) String (%pi Rig1 Explicit (Just y) String String))
 LOG 0: Resolved name: Prelude.Nat