MarcelineVQ

module Network.Curl.Prim

import Data.Bytes.Lazy

import Control.App
import Network.Curl.Types
import Network.Curl.Option

import Data.Bytes.Strict
import Data.Word.Word8

MarcelineVQ

-- makeHasIO "what" Private ["c:foo","javascript:borp"] `[ prim_gob : Int -> Int -> PrimIO Int ]
-- This generates:
-- %foreign "c:foo" "javascript:borp"
-- prim_gob : Int -> Int -> PrimIO Int
-- And:
-- private
-- what : HasIO io => Int -> Int -> io Int
makeHasIO : String -> Visibility -> List String -> List Decl -> Elab ()
makeHasIO funname0 vis str ys = do
    [(IClaim pfc pmw pvis _ pty@(MkTy tyfc primname primty))] <- pure ys

MarcelineVQ

-- Not compelete since it doesn't go to HasIO yet, but given:
-- makeHasIO "what" ["c:foo","javascript:borp"] `[ prim_gob : Int -> Int -> PrimIO Int ]
-- This generates:
-- %foreign "c:foo" "javascript:borp"
-- what : Int -> Int -> PrimIO Int
makeHasIO : String -> List String -> List Decl -> Elab ()
makeHasIO funname str ys = do
  [IClaim fc mw vis _ (MkTy tyfc _ ty)] <- pure ys
    | _ => fail "bad format"
  let r = IClaim fc mw vis [ForeignFn str] (MkTy tyfc (UN funname) ty)

MarcelineVQ

%foreign "C:worf,libutf8"
worf : Char -> Char

%foreign "C:worf2,libutf8"
worf2 : Int -> Int

main : IO ()
main = do
  putCharLn '😀'
  putCharLn (worf 'a')

MarcelineVQ

module Control.Monad.Codensity

import Control.Monad.Trans

import Control.Linear.LIO

public export
data Codensity : (m : Type -> Type) -> (a : Type) -> Type where
  MkCodensity : (1 _ : (forall b. (a -> m b) -> m b)) -> Codensity m a

MarcelineVQ

data Of : Type -> Type -> Type where
  ||| Streaming depends on the Lazyness of r currently
  (:>) : a -> Lazy r -> Of a r

data Stream : (f : Type -> Type) -> (m : Type -> Type) -> Type -> Type where
  Return : (1 _ : r) -> Stream f m r
  Effect : (1 _ : m (Stream f m r)) -> Stream f m r
  Step : (1 _ : f (Stream f m r)) -> Stream f m r
  ||| Fusion constructor
  ||| We don't have a serious rewrite system in idris2 yet so this does the job

MarcelineVQ

module Network.Curl.Prim

import Data.Bytes.Lazy

import Control.App
import Network.Curl.Types
import Network.Curl.Option

import Data.Bytes.Strict
import Data.Word.Word8

MarcelineVQ

record Fef1 a {auto g : Num a} where
  constructor Raf1
  fef : a -> a

blopo1 : Num a => a -> Fef1 a
blopo1 r = Raf1 (+r)

record Fef2 a where
  constructor Raf2
  fef2 : Num a => a -> a

MarcelineVQ

'atom-text-editor[data-grammar~="idris"]':
  'ctrl-alt-h': 'language-idris:holes'

MarcelineVQ

Jul 09 04:02:09 <kiwi_45>       dmj`: what should I do now ?
Jul 09 04:02:21 *       cosimone (~cosimone@2001:b07:ae5:db26:9520:741c:a5e9:2223) has joined
Jul 09 04:02:33 <Marked>        Oh thanks
Jul 09 04:03:02 <dmj`>  kiwi_45: you do as I tell you, use the cookie package since servant auth lacks HttpOnly it seems
Jul 09 04:03:41 <dmj`>  kiwi_45: you are going to need to make a session token that you store in the cookie, this can be a UUID for now or anything really, some people use JWTs for this, but meh. 
Jul 09 04:04:20 <dmj`>  kiwi_45: Cookies with HttpOnly using Https (is secure), is a good first step
Jul 09 04:04:51 *       kiwi_45 has quit (Quit: Ping timeout (120 seconds))