MarcelineVQ

module Control.Monad.Cont

import Control.Monad.Identity
import Control.Monad.Trans

public export
record ContT r m a where
  constructor MkContT
  runContT : (a -> m r) -> m r

MarcelineVQ

infixr 3 `foober`
infix 8 @@@

foober : Int -> Int -> Int
foober = ?fsdsdf

(@@@) : Int -> Int -> Int
x @@@ y = ?dsfsfdsfd

MarcelineVQ

module Main

import Data.IORef

import Data.Buffer
import Network.Curl.Easy

partial
expect : String -> (1 _ : Maybe t) -> t
expect msg Nothing = idris_crash msg

MarcelineVQ

data Name : Type where
     UN : String -> Name -- user written name
     MN : String -> Int -> Name -- machine generated name

-- In the term representation, we represent local variables as an index into
-- a list of bound names:
data IsVar : Name -> Nat -> List Name -> Type where
     First : IsVar n Z (n :: ns)
     Later : IsVar n i ns -> IsVar n (S i) (m :: ns)

MarcelineVQ

`( [| ( x , y ) |] )
IAlternative
  (UniqueDefault
    (IApp
      (IApp
        (IVar (UN "<*>"))
        (IApp
          (IApp
            (IVar (UN "<*>"))
            (IApp

MarcelineVQ

[internal] ToCode (CurlOption ty) where
  toCode = enumTo [1..273]

export
{ty : _} -> ToCode (CurlOption ty) where
  toCode opt = toCode @{internal} opt + (toCode ty)

MarcelineVQ

import Data.Buffer

-- Redefining this here to modify it
%foreign "scheme:blodwen-new-buffer"
prim_newBuffer' : Int -> PrimIO Buffer

export
newBuffer' : HasIO io => (bytes : Int) -> io Buffer
newBuffer' size = primIO $ prim_newBuffer' size
-- No Maybe, if we can't allocate memory then die.

MarcelineVQ

-- We use TTImp instead of Name because in name quotation on primtypes `{{Int}}
-- is not parsed as a name, in fact prims are specifically excluded from this.
||| newtype "Foo" `(Int) ~~> data Foo : Type where MkFoo : Int -> Foo
newtype : String -> Visibility -> TTImp -> Elab ()
newtype name0 vis ty = do
    name <- inCurrentNS (UN name0)
    let con = MkTy eFC (mapName ("Mk" ++) name) `(~ty -> ~(IVar eFC name))
    let decl = IData eFC vis $ MkData eFC name (IType eFC) [] [con]
    declare [decl]

MarcelineVQ

public export
Semigroup a => Semigroup (Managed a) where
  x <+> y = [| x <+> y |]

MarcelineVQ

module Foo


import System.File
import Control.Monad.Managed

export
withFile' : HasIO io => String -> Mode -> (Either FileError File -> io a) -> io a
withFile' file mode act = do res <- openFile file mode
                             a <- act res