MarcelineVQ

data LReal : Type -> Type where
  LInteger : Integer -> LReal Integer
  LFloat   : Float -> LReal Float
  LRational : Rational -> LReal Rational
  
instance NUm (LReal a) where ...

MarcelineVQ

module Main

import Language.Reflection

%language ElabReflection

-- This is an issue because elaboration on datatypes requires many traverersals,
-- of the types, the constructors, building up results etc.
-- logMsg is set to 12 because we're not interested in executing it, it's just
-- an easy placeholder

MarcelineVQ

my_uniq : Ord a => List a -> Maybe a
my_sort : Ord a => List a -> List a

[myeq] Eq a where

[myord] Ord a using myeq where

faf : List a -> Maybe a
faf xs = let _ = myord in my_uniq $ my_sort xs

MarcelineVQ

do let a = dsfsd
       b = dsfasdsd
       c = sdfsdfsd !(foo b)
       e = expr c
   ?sdfsd

do let a = dsfsd
       b = dsfasdsd
   z <- foo b
   let c = sdfsdfsd z

MarcelineVQ

-- given (%pi RigW Explicit Nothing %type (%pi RigW Explicit Nothing %type %type))
-- only
-- getArity' (IPi _ _ _ _ _ retTy) = ...
-- matches. None of the other PiInfo cases match, ExplicitArg/ImplicitArg etc
getArity' : TTImp -> Nat
getArity' (IPi _ M0 _ _ _ retTy) = getArity' retTy
getArity' (IPi _ _     ExplicitArg _ _ retTy) = S (getArity' retTy)
getArity' (IPi _ _     ImplicitArg _ _ retTy) = S (getArity' retTy)
getArity' (IPi _ _ (DefImplicit _) _ _ retTy) = S (getArity' retTy)
getArity' (IPi _ _ AutoImplicit _ _ retTy)    = S (getArity' retTy)

MarcelineVQ

infixr 9 -*
(-*) : Type -> Type -> Type
(-*) a b = (1 _ : a) -> b

Eff : Type
Eff = IO ()
-- Negation, 
N : Type -> Type
N a = a -* Eff

MarcelineVQ

<jacks2> "*** Exception: Text.ParserCombinators.Parsec.Prim.many: combinator 'many' is applied to a parser that accepts an empty string."
<monochrom> rev is recursive. This is the one you can rewrite.
<jacks2> is there a way to force this, despite that message?
<monochrom> I'll let you take time to accept it.
<liiae> monochrom: so the first rule, if a function A would be another functionB's fixed point, that B must be a recursive function at first?
<liiae> so we can have A = fix B
* gienah (~mwright@gentoo/developer/gienah) has joined
<awpr> `reverse' = const Prelude.reverse`
<jacks2> nevermind, I fixed it it
<ezzieyguywuf> I'm very confused about how to add a dependency using stack

MarcelineVQ

module Test.SimpleTime

import Data.List

-- Helpers
-----------------------------------------------------------

infixr 10 ^
(^) : Num a => a -> Nat -> a
(^) m 0 = 1

MarcelineVQ

racketSec : String
racketSec = "(lambda (t) (truncate (inexact->exact (/ t 1000))))"

-- extract nanoseconds from a Time Object
racketNanosec : String
racketNanosec = "(lambda (t) (modulo (truncate (inexact->exact (* t 1000000))) 1000000000))"

%foreign "scheme:chez,current-time"
         "scheme:racket,current-inexact-milliseconds"
primGetTime : PrimIO (Ptr TimePtr)

MarcelineVQ

%foreign "scheme:chez,real-time"
         "scheme:racket,current-milliseconds"
time' : PrimIO Int

getTime : IO Int
getTime = primIO time'

export
foo : IO Int -- records time properly, roughly 2 seconds of work