text:
module IdrisJvm.FFI

%access public export

data JVM_NativeTy = Class String
                  | Interface String

data JVM_Native  : JVM_NativeTy -> Type where
  MkJVMNative : (ty : JVM_NativeTy) -> JVM_Native ty

ThrowableClass : JVM_NativeTy
ThrowableClass = Class "java/lang/Throwable"

Throwable : Type
Throwable = JVM_Native ThrowableClass

JVM_Throwable : Type -> Type
JVM_Throwable t = Either Throwable t

mutual
    data AnnotationValue = AnnInt String -- FFI Descriptor can only take String
                         | AnnBoolean String
                         | AnnByte String
                         | AnnChar String
                         | AnnShort String
                         | AnnLong String
                         | AnnFloat String
                         | AnnDouble String
                         | AnnEnum String String
                         | AnnClass String
                         | AnnAnnotation Annotation
                         | AnnArray (List AnnotationValue)

    data Annotation = Ann String (List (String, AnnotationValue))

mutual
  data JVM_FfiFn = Static JVM_NativeTy String
                 | GetStaticField JVM_NativeTy String
                 | SetStaticField JVM_NativeTy String
                 | Lambda JVM_NativeTy String
                 | Constructor
                 | New
                 | NewArray
                 | GetArray
                 | SetArray
                 | MultiNewArray
                 | ArrayLength
                 | ClassLiteral String
                 | Instance String
                 | GetInstanceField String
                 | SetInstanceField String
                 | Super String
                 | InstanceOf String
                 | ExportStaticField String
                 | ExportInstanceField String
                 | ExportStatic String
                 | ExportInstance String
                 | ExportDefault -- Export an instance method with idris function name
                 | Anns (List Annotation)

                 -- Export a static method with method annotations and parameter annotations
                 | ExportStaticWithAnn String (List Annotation) (List (List Annotation))

                 -- Export an instance method with method annotations and parameter annotations
                 | ExportInstanceWithAnn String (List Annotation) (List (List Annotation))

  data JVM_IntTypes : Type -> Type where
      JVM_IntChar   : JVM_IntTypes Char
      JVM_IntNative : JVM_IntTypes Int
      JVM_IntBits8  : JVM_IntTypes Bits8
      JVM_IntBits16 : JVM_IntTypes Bits16
      JVM_IntBits32 : JVM_IntTypes Bits32
      JVM_IntBits64 : JVM_IntTypes Bits64

  data JFloat : Type where
      Float : (d : Double) -> JFloat

  ||| Supported JVM function types
  data JVM_FnTypes : Type -> Type where
      JVM_Fn : JVM_Types s -> JVM_FnTypes t -> JVM_FnTypes (s -> t)
      JVM_FnIO : JVM_Types t -> JVM_FnTypes (JVM_IO t)
      JVM_FnBase : JVM_Types t -> JVM_FnTypes t

  data JVM_FunctionalObject : Type -> Type where
    MkJVMFunctionalObject : (lambdaFunctionTy : t) -> JVM_FunctionalObject t

  ||| Supported JVM foreign types
  data JVM_Types : Type -> Type where
      JVM_Bool        : JVM_Types Bool
      JVM_Str         : JVM_Types String
      JVM_Double      : JVM_Types Double
      JVM_Float       : JVM_Types JFloat
      JVM_BigInteger  : JVM_Types Integer
      JVM_Unit        : JVM_Types ()
      JVM_NativeT     : JVM_Types (JVM_Native a)
      JVM_IntT        : JVM_IntTypes i -> JVM_Types i
      JVM_ArrayT      : JVM_Types t -> JVM_Types (JVM_Array t)
      JVM_ThrowableT  : JVM_Types t -> JVM_Types (JVM_Throwable t)
      JVM_FnT         : JVM_FnTypes t -> JVM_Types (JVM_FunctionalObject t)

  data JVM_Array : Type -> Type where
    MkJvmTypesArray : JVM_Types t -> JVM_Array t

  ||| A descriptor for the JVM FFI. See the constructors of `JVM_Types`
  ||| and `JVM_IntTypes` for the concrete types that are available.
  FFI_JVM : FFI
  FFI_JVM = MkFFI JVM_Types JVM_FfiFn String

  JVM_IO : Type -> Type
  JVM_IO = IO' FFI_JVM

Show JFloat where
  show (Float d) = show d

%used MkJVMFunctionalObject lambdaFunctionTy

%used Float d

%inline
javacall : (fname : JVM_FfiFn) -> (ty : Type) ->
           {auto fty : FTy FFI_JVM [] ty} -> ty
javacall fname ty = foreign FFI_JVM fname ty

%inline
jcall : (fname : JVM_FfiFn) -> (ty : Type) ->
           {fty : FTy FFI_JVM [] ty} -> ty
jcall fname ty = foreign FFI_JVM fname ty

javaClass : String -> Type
javaClass = JVM_Native . Class

javaInterface : String -> Type
javaInterface = JVM_Native . Interface

%inline
invokeInstance : String -> (ty : Type) -> {auto fty : FTy FFI_JVM [] ty} -> ty
invokeInstance method = javacall (Instance method)

%inline
invokeStatic : JVM_NativeTy -> String -> (ty : Type) -> {auto fty : FTy FFI_JVM [] ty} -> ty
invokeStatic klass method = javacall (Static klass method)

interface Inherits a b where {}

Inherits (JVM_Native t) (JVM_Native t) where {}

IdrisObject : Type
IdrisObject = javaClass "io/github/mmhelloworld/idrisjvm/runtime/IdrisObject"

namespace Object
  ObjectClass : JVM_NativeTy
  ObjectClass = Class "java/lang/Object"

  Object : Type
  Object = JVM_Native ObjectClass

  ObjectArray : Type
  ObjectArray = JVM_Array Object

  ObjectArray2d : Type
  ObjectArray2d = JVM_Array (JVM_Array Object)

  toString : Object -> JVM_IO String
  toString obj = invokeInstance "toString" (Object -> JVM_IO String) obj

Inherits Object String where {}
Inherits Object (Maybe String) where {}

Inherits Object Integer where {}

Inherits Object (JVM_Native t) where {}
Inherits Object (Maybe (JVM_Native t)) where {}

Inherits ObjectArray (JVM_Array t) where {}

implicit subtyping : Inherits (JVM_Native t) (JVM_Native s) => JVM_Native s -> JVM_Native t
subtyping = believe_me

implicit subtypingInIo : Inherits (JVM_Native super) (JVM_Native sub) => JVM_IO (JVM_Native sub) -> JVM_IO (JVM_Native super)
subtypingInIo sub = believe_me <$> sub

implicit stringIsAnObject : String -> Object
stringIsAnObject = believe_me

decl syntax [sub] inherits [super] = Inherits (JVM_Native (super)) (JVM_Native (sub)) where {}

isNull : JVM_Native t -> Bool
isNull obj = unsafePerformIO $ invokeStatic (Class "java/util/Objects") "isNull" (Object -> JVM_IO Bool) (believe_me obj)

isNullString : String -> Bool
isNullString obj = unsafePerformIO $ invokeStatic (Class "java/util/Objects") "isNull" (Object -> JVM_IO Bool) (believe_me obj)

implicit nullableToMaybe : JVM_Native a -> Maybe (JVM_Native a)
nullableToMaybe t = if isNull t then Nothing else Just t

nullableStringToMaybe : String -> Maybe String
nullableStringToMaybe str = if isNullString str then Nothing else Just str

implicit maybeToNullable : Maybe (JVM_Native t) -> JVM_Native t
maybeToNullable (Just t) = t
maybeToNullable Nothing = believe_me prim__null

maybeToNullableString : Maybe String -> String
maybeToNullableString (Just t) = t
maybeToNullableString Nothing = believe_me prim__null

%inline
javalambda : String
        -> (interfaceFnTy: Type)
        -> {auto interfaceFnJvmTy: JVM_FnTypes interfaceFnTy}
        -> lambdaTy
        -> {auto lambdaJvmTy: JVM_FnTypes lambdaTy}
        -> JVM_Native nativeTy
javalambda {nativeTy} {lambdaTy} fname interfaceFnTy lambda = unsafePerformIO $
  javacall
    (Lambda nativeTy fname)
    (JVM_FunctionalObject interfaceFnTy -> JVM_FunctionalObject lambdaTy -> JVM_IO (JVM_Native nativeTy))

    {- This value is not used. This is here so that the corresponding type can provide the interface method signature
     - which can be different from the actual lambda signature
     -}
    (believe_me "")

    (MkJVMFunctionalObject lambda)

%inline
new : (ty : Type) -> {auto fty : FTy FFI_JVM [] ty} -> ty
new ty = javacall New ty

%inline
total
newArray : (elemTy: Type) -> {auto jvmElemTy: JVM_Types elemTy} -> Nat -> JVM_IO (JVM_Array elemTy)
newArray elemTy size = assert_total $ javacall NewArray (Int -> JVM_IO $ JVM_Array elemTy) (cast size)

%inline
setArray : (ty : Type) -> {auto fty : FTy FFI_JVM [] ty} -> ty
setArray ty = javacall SetArray ty

%inline
arrayLength : {auto ft: JVM_Types elemTy} -> JVM_Array elemTy -> JVM_IO Nat
arrayLength {elemTy} arr = cast <$> javacall ArrayLength (JVM_Array elemTy -> JVM_IO Int) arr

%inline
getArray : (ty : Type) -> {auto fty : FTy FFI_JVM [] ty} -> ty
getArray ty = javacall GetArray ty

%inline
newMultiArray : (ty : Type) -> {auto fty : FTy FFI_JVM [] ty} -> ty
newMultiArray = javacall MultiNewArray

%inline
getInstanceField : String -> (ty : Type) -> {auto fty : FTy FFI_JVM [] ty} -> ty
getInstanceField fieldName = javacall (GetInstanceField fieldName)

%inline
setInstanceField : String -> (ty : Type) -> {auto fty : FTy FFI_JVM [] ty} -> ty
setInstanceField fieldName = javacall (SetInstanceField fieldName)

%inline
getStaticField : JVM_NativeTy -> String -> (ty : Type) -> {auto fty : FTy FFI_JVM [] ty} -> ty
getStaticField klass fieldName = javacall (GetStaticField klass fieldName)

%inline
setStaticField : JVM_NativeTy -> String -> (ty : Type) -> {auto fty : FTy FFI_JVM [] ty} -> ty
setStaticField klass fieldName = javacall (SetStaticField klass fieldName)

%inline
jcallInstance : String -> (ty : Type) -> FTy FFI_JVM [] ty -> ty
jcallInstance method ty fty = jcall (Instance method) ty {fty=fty}

%inline
jcallStatic : JVM_NativeTy -> String -> (ty : Type) -> FTy FFI_JVM [] ty -> ty
jcallStatic klass method ty fty = jcall (Static klass method) ty {fty=fty}

%inline
jcallNew : (ty : Type) -> FTy FFI_JVM [] ty -> ty
jcallNew ty fty = jcall New ty {fty=fty}

%inline
jcallGetInstanceField : String -> (ty : Type) -> FTy FFI_JVM [] ty -> ty
jcallGetInstanceField fieldName ty fty = jcall (GetInstanceField fieldName) ty {fty = fty}

%inline
jcallSetInstanceField : String -> (ty : Type) -> FTy FFI_JVM [] ty -> ty
jcallSetInstanceField fieldName ty fty = jcall (SetInstanceField fieldName) ty {fty = fty}

%inline
jcallGetStaticField : JVM_NativeTy -> String -> (ty : Type) -> FTy FFI_JVM [] ty -> ty
jcallGetStaticField klass fieldName ty fty = jcall (GetStaticField klass fieldName) ty {fty = fty}

%inline
jcallSetStaticField : JVM_NativeTy -> String -> (ty : Type) -> FTy FFI_JVM [] ty -> ty
jcallSetStaticField klass fieldName ty fty = jcall (SetStaticField klass fieldName) ty {fty=fty}

%inline
instanceOf : Inherits Object obj => JVM_NativeTy -> obj -> Bool
instanceOf (Class className) obj = unsafePerformIO $ javacall (InstanceOf className) (Object -> JVM_IO Bool) (believe_me obj)
instanceOf (Interface className) obj = unsafePerformIO $ javacall (InstanceOf className) (Object -> JVM_IO Bool) (believe_me obj)

namespace Class

  ClassClass : JVM_NativeTy
  ClassClass = Class "java/lang/Class"

  JClass : Type
  JClass = JVM_Native ClassClass

  forName : String -> JClass
  forName className = unsafePerformIO $ invokeStatic ClassClass "forName" (String -> JVM_IO JClass) className

  isInstance : Inherits Object (JVM_Native t) => JClass -> JVM_Native t -> Bool
  isInstance clazz obj = unsafePerformIO $ invokeInstance "isInstance" (JClass -> Object -> JVM_IO Bool) clazz (believe_me obj)

%inline
classLit : String -> JClass
classLit s = unsafePerformIO $ javacall (ClassLiteral s) (JVM_IO JClass)

RuntimeClass : JVM_NativeTy
RuntimeClass = Class "io/github/mmhelloworld/idrisjvm/runtime/Runtime"

jthrow : Inherits Throwable t => t -> JVM_IO a
jthrow t = believe_me $ invokeStatic RuntimeClass "rethrow" (Throwable -> JVM_IO Object) (believe_me t)

VirtualMachineErrorClass : JVM_NativeTy
VirtualMachineErrorClass = Class "java/lang/VirtualMachineError"

ThreadDeathClass : JVM_NativeTy
ThreadDeathClass = Class "java/lang/ThreadDeath"

LinkageErrorClass : JVM_NativeTy
LinkageErrorClass = Class "java/lang/LinkageError"

InterruptedExceptionClass : JVM_NativeTy
InterruptedExceptionClass = Class "java/lang/InterruptedException"

VirtualMachineErrorClass inherits ThrowableClass
ThreadDeathClass inherits ThrowableClass
InterruptedExceptionClass inherits ThrowableClass
LinkageErrorClass inherits ThrowableClass

term syntax jcatch [clazz] = \t => instanceOf clazz t

try : JVM_IO (JVM_Throwable a) -> List (List (Throwable -> Bool), Throwable -> JVM_IO a) -> JVM_IO a
try action handlers = do
    value <- action
    either (go handlers) pure value
  where
    go : List (List (Throwable -> Bool), Throwable -> JVM_IO a) -> Throwable -> JVM_IO a
    go [] t = jthrow t
    go ((ps, handler) :: handlers) t =
      if any (\p => p t) ps then
        handler t
      else
        go handlers t

export
Show Throwable where
  show throwable = unsafePerformIO $ invokeStatic RuntimeClass "showThrowable"
                     (Throwable -> JVM_IO String) throwable

-- Inspired by Scala's NonFatal
catchNonFatal : Throwable -> Bool
catchNonFatal t = not (instanceOf VirtualMachineErrorClass t
                 && instanceOf ThreadDeathClass t
                 && instanceOf InterruptedExceptionClass t
                 && instanceOf LinkageErrorClass t)

term syntax "<@>" [name] [attrs] = Ann name attrs
term syntax "<@s>" [value] = AnnString value
term syntax "<@i>" [value] = AnnInt value
term syntax "<@by>" [value] = AnnByte value
term syntax "<@b>" [value] = AnnBoolean value
term syntax "<@ch>" [value] = AnnChar value
term syntax "<@sh>" [value] = AnnShort value
term syntax "<@l>" [value] = AnnLong value
term syntax "<@f>" [value] = AnnFloat value
term syntax "<@d>" [value] = AnnDouble value
term syntax "<@c>" [value] = AnnClass value
term syntax "<@enum>" [ty] [value] = AnnEnum ty value
term syntax "<@..>" [values] = AnnArray values
term syntax "<@@>" [ann] = AnnAnnotation ann
term syntax [name] "<@:>" [value] = (name, value)


text:
module GLCore

import Types
import JSMatrix.JSMatrix

-- Create the WebGL context from a canvas element
getGLCxt : Element -> IO GLCxt
getGLCxt (MkElem e) = do
  x <- mkForeign (FFun "%0.getContext('webgl')" [FPtr] FPtr) e
  return (MkCxt x)

getGLProp : String -> GLCxt -> IO Int
getGLProp prop (MkCxt c) = mkForeign (FFun "%0[%1]" [FPtr,FString] FInt) c prop

-- Create a program for building and linking shaders
createProg : GLCxt -> IO (GLProgram,GLCxt)
createProg (MkCxt x) = do
  p <- mkForeign (FFun "%0.createProgram()" [FPtr] FPtr) x
  return ((MkGLProg p),(MkCxt x))

-- Assign the program to the given webGL context
useProg : (GLProgram, GLCxt) -> IO (GLProgram, GLCxt)
useProg ((MkGLProg y),(MkCxt x)) = do
  mkForeign (FFun "%0.useProgram(%1)" [FPtr,FPtr] FUnit) x y
  return ((MkGLProg y), (MkCxt x))

-- Enable a specific GL setting. I don't know how to access enum properties
-- using the JavaScript FFI yet so this is a bit filthy but easy to change.
enableGLSetting : Int -> GLCxt -> IO GLCxt
enableGLSetting setting (MkCxt c) = do
  _ <- mkForeign (FFun "%0.enable(%1)" [FPtr,FInt] FUnit) c setting
  return (MkCxt c)

-- Again with the enum properties. But this clears the current context.
glClear : GLCxt -> IO GLCxt
glClear (MkCxt c) = do
  mkForeign (FFun "%0.clear(%0.COLOR_BUFFER_BIT | %0.DEPTH_BUFFER_BIT)" [FPtr] FUnit) c
  return (MkCxt c)

-- Assign a clear colour to the entire gl region.
clearColor : Vect 4 Float -> GLCxt -> IO GLCxt
clearColor [r,g,b,a] (MkCxt c) = do
  mkForeign (FFun "%0.clearColor(%1,%2,%3,%4)" [FPtr,FFloat,FFloat,FFloat,FFloat] FUnit) c r g b a
  return (MkCxt c)

-- Choose a depth effect function - this time we choose to hide objects
-- that are 'behind' closer objects.
depthFun : GLCxt -> IO GLCxt
depthFun (MkCxt c) = do
  mkForeign (FFun "%0.depthFunc(%0.LEQUAL)" [FPtr] FUnit) c
  return (MkCxt c)

-- Create a buffer
-- var vertexPosBuffer = gl.createBuffer()
createBuffer : GLCxt -> IO GLBuffer
createBuffer (MkCxt c) = do
  b <- mkForeign (FFun "%0.createBuffer()" [FPtr] FPtr) c
  return (MkBuf b)

-- Bind the buffer
-- gl.bindBuffer(gl.ARRAY_BUFFER, vertextPosBuffer)
bindArrayBuffer : GLCxt -> GLBuffer -> IO GLCxt
bindArrayBuffer (MkCxt c) (MkBuf b) = do
  mkForeign (FFun "%0.bindBuffer(%0.ARRAY_BUFFER, %1)" [FPtr,FPtr] FUnit) c b
  return (MkCxt c)

-- Load the buffer data
-- gl.bufferData(gl.ARRAY_BUFFER, new Float32Array(vertices), gl.STATIC_DRAW)
bufferVertexData : F32Array -> GLCxt -> IO GLCxt
bufferVertexData (MkF32Array xs) (MkCxt c) = do
  bType <- getGLProp "ARRAY_BUFFER" (MkCxt c)
  style <- getGLProp "STATIC_DRAW" (MkCxt c)
  mkForeign (FFun "%0.bufferData(%1, %2, %3)" [FPtr,FInt,FPtr,FInt] FUnit) c bType xs style
  return (MkCxt c)

-- Helper/Convenience function to create/bind/fill an ARRAY_BUFFER with an F32Array
createBindBuffer : GLCxt -> F32Array -> IO (GLBuffer,GLCxt)
createBindBuffer cxt arr = do
  buf <- createBuffer cxt
  cxt' <- bindArrayBuffer cxt buf
  cxt'' <- bufferVertexData arr cxt'
  return (buf,cxt'')

-- call gl.drawArrays to specifically draw triangles.
-- First argument is the current program/glcontext
-- start = where on the vertex array to start reading vertices
-- nVertices = number of vertices to be read
drawTriangles : Int -> Int -> (GLProgram,GLCxt) -> IO (GLProgram,GLCxt)
drawTriangles start nVertices ((MkGLProg p),(MkCxt c)) = do
  mkForeign (FFun "%0.drawArrays(%0.TRIANGLES, %1,%2)" [FPtr,FInt,FInt] FUnit) c start nVertices
  return ((MkGLProg p),(MkCxt c))

-- Set the viewport size to the canvas element size
setViewport : Float -> Float -> GLCxt -> IO GLCxt
setViewport w h (MkCxt c) = do
  mkForeign (FFun "%0.viewport(0,0,%1,%2)" [FPtr,FFloat,FFloat] FUnit) c w h
  return (MkCxt c)

-- Get a uniform location
getUniformLocation : String -> (GLProgram,GLCxt) -> IO Int
getUniformLocation uni ((MkGLProg p),(MkCxt c)) =
  mkForeign (FFun "%0.getUniformLocation(%1,%2)" [FPtr,FPtr,FString] FInt) c p uni

-- Assign 4x4 Matrix value to uniform location
uniformMatrix4v : JSGLMat4 -> Int -> (GLProgram,GLCxt) -> IO (GLProgram,GLCxt)
uniformMatrix4v (MkMat4 mat4) loc ((MkGLProg p),(MkCxt c)) = do
  mkForeign (FFun "%0.uniformMatrix4fv(%1,false,%2)" [FPtr,FInt,FPtr] FUnit) c loc mat4
  return ((MkGLProg p),(MkCxt c))

-- Fetch the Math.PI value from JS Land
mathPI : IO Float
mathPI = mkForeign (FFun "Math.PI" [] FFloat)

ext: idr

max_stars_repo_name: mankyKitty/idris-webgl

max_issues_repo_name: mankyKitty/idris-webgl

max_forks_repo_name: mankyKitty/idris-webgl


text:
module Python.Fields

import Python.Objects
import Python.IO

import Language.Reflection

%default total
%access public export
%language ErrorReflection

infixl 4 /.
||| Attribute accessor.
|||
||| @ obj Obj with the given signature.
||| @ f   Name of the requested field.
(/.) :
  (obj : Obj sig) -> (f : String)
  -> {auto pf : sig f = Attr t}
  -> t
(/.) {t = t} (MkObj obj) f =
  unRaw . unsafePerformIO $
    foreign FFI_Py "getattr" (Ptr -> String -> PIO (Raw t)) obj f

data FieldParams : Type -> Type where
  FP : String -> .(params : pt) -> FieldParams pt

fpName : FieldParams pt -> String
fpName (FP n ps) = n

fpParams : FieldParams pt -> pt
fpParams (FP n ps) = ps

infixl 4 //.
(//.) :
  (obj : Obj sig) -> (fps : FieldParams pt)
  -> {auto pf : sig (fpName fps) = PAttr pt tf}
  -> tf (fpParams fps)
(//.) {tf=tf} (MkObj obj) (FP f ps) =
  unRaw . unsafePerformIO $
    foreign FFI_Py "getattr" (Ptr -> String -> PIO (Raw $ tf ps)) obj f

infixl 4 /:
||| Attribute accessor, useful for chaining.
|||
||| @ obj PIO action returning an object.
||| @ f   Name of the requested field.
(/:) :
  (obj : PIO (Obj sig)) -> (f : String)
  -> {auto pf : sig f = Attr t}
  -> PIO t
(/:) obj f = (/. f) <$> obj

infixl 4 //:
(//:) :
  (obj : PIO (Obj sig)) -> (fps : FieldParams pt)
  -> {auto pf : sig (fpName fps) = PAttr pt tf}
  -> PIO (tf (fpParams fps))
(//:) obj fps = (//. fps) <$> obj

-- Error reflection for better error messages.
-- TODO: generalise this
fieldErr : Err -> Maybe (List ErrorReportPart)
{-
fieldErr (CantSolveGoal `(~(App sig fn) = PAttr Unit ~(Bind v (Lam _) ty)) ntms)
  = Just
    [ TextPart "Field", TermPart fn
    , TextPart "does not exist in object signature", TermPart sig
    , TextPart "with the type", TermPart ty, TextPart "(or at all)."
    ]
fieldErr (CantSolveGoal `(~(App sig fn) = ~rhs) ntms)
  = Just
    [ TextPart "Field", TermPart fn
    , TextPart "does not exist in object signature", TermPart sig
    , TextPart "with the correct type (or at all)."
    ]
-}
fieldErr (CantSolveGoal `(PAttr Unit ~(Bind _ (Lam _) tyl) = PAttr Unit ~(Bind _ (Lam _) tyr)) ntms)
  = Just
    [ TextPart "Cannot match field type", TermPart tyl
    , TextPart "with context-required type", TermPart tyr
    ]

fieldErr (CantSolveGoal `(NotField = ~rhs) ntms)
  = Just
    [ TextPart "The requested field does not exist."
    ]
fieldErr _ = Nothing

%error_handlers Python.Fields.(/.) pf fieldErr
%error_handlers Python.Fields.(//.) pf fieldErr
%error_handlers Python.Fields.(/:) pf fieldErr
%error_handlers Python.Fields.(//:) pf fieldErr

max_stars_repo_name: ziman/idris-py

max_issues_repo_name: ziman/idris-py

max_forks_repo_name: ziman/idris-py


text:
module Main

import Data.Vect

vdrop : (n:Nat) -> Vect (n+m) a -> Vect m a
vdrop Z v = v
vdrop (S k) (x::xs) = vdrop k xs

main : IO ()
-- BOOOM!
main = putStrLn (show (vdrop 6 (1 :: 2 :: 3 :: 4 :: 5 :: Nil)))

max_stars_repo_name: janschultecom/idris-examples

max_issues_repo_name: janschultecom/idris-examples

max_forks_repo_name: janschultecom/idris-examples


text:
module Rationals

import ZZ

%access public export

Pair : Type
Pair = (Integer, Integer)

ZZPair : Type
ZZPair = (ZZ, ZZ)

ZZtoDb : ZZ -> Double
ZZtoDb x = cast{from=Integer}{to=Double} (cast{from=ZZ}{to=Integer} x)

DbtoZZ : Double -> ZZ
DbtoZZ x = cast{from=Integer}{to=ZZ} (cast{from=Double}{to=Integer} x)

apZZ : (f: ZZ -> ZZ) -> (n: ZZ) -> (m: ZZ) -> n = m -> f n = f m
apZZ f m m Refl = Refl

isNotZero : Nat -> Bool
isNotZero Z = False
isNotZero (S k) = True

isFactorInt : Integer -> Integer -> Type  --Needed for defining Integer division
isFactorInt m n = (k : Integer ** (m * k = n))

divides : (m: Integer) -> (n: Integer) -> (k: Integer ** (m * k = n)) -> Integer
divides m n k = (fst k)

--Integer implemetation of gcd
CalcGCD : (Integer, Integer) -> Integer
CalcGCD (a, b) = if (isNotZero (toNat b)) then next else a where
    next = CalcGCD (b, toIntegerNat (modNat (toNat a) (toNat b)))

OnlyPositive : (x: Pair) -> Pair
OnlyPositive x = (if (fst x)>0 then fst x else (-1)*(fst x), if(snd x)>0 then (snd x) else (-1)*(snd x))

--Integer implemetation of gcd
gccd : (Integer, Integer) -> Integer
gccd x = CalcGCD (OnlyPositive x)

data NotZero : Integer -> Type where --Proof that a number is not zero, needed to construct Q
  OneNotZero : NotZero 1
  NegativeNotZero : ( n: Integer ) -> NotZero n -> NotZero (-n)
  PositiveNotZero : ( m: Integer ) -> LTE 1 (fromIntegerNat m)  -> NotZero m

data ZZNotZero : ZZ -> Type where
  ZZOneNotZero : ZZNotZero 1
  ZZNegativeNotZero : ( n: ZZ ) -> ZZNotZero n -> ZZNotZero (-n)
  ZZPositiveNotZero : ( m: ZZ ) -> LTE 1 (fromIntegerNat (cast(m)))  -> ZZNotZero m

--Type for equality of two Rationals
data EqRat : Pair -> Pair -> Type where
  IdEq : (m : Pair) -> EqRat m m
  MulEq : (c : Integer) -> EqRat n m -> EqRat ((fst n)*c,(snd n)*c) m

make_rational : (p: Nat) -> (q: Integer) -> NotZero q -> Pair
make_rational p q x = (toIntegerNat(p), q)

InclusionMap : (n : Nat) -> Pair --Includes the naturals in Q
InclusionMap n = make_rational n 1 OneNotZero

AddRationals : (x: ZZPair) -> ZZNotZero (snd x) -> (y: ZZPair) -> ZZNotZero (snd y) -> ZZPair
AddRationals x a y b = ((fst x)*(snd y) + (snd x)*(fst y), (snd x)*(snd y))

MultiplyRationals : (x: ZZPair) -> ZZNotZero (snd x) -> (y: ZZPair) -> ZZNotZero (snd y) -> ZZPair
MultiplyRationals x a y b =((fst x)*(fst y), (snd x)*(snd y))

MultInverse : (x: ZZPair) -> ZZNotZero (fst x) -> ZZNotZero (snd x) -> ZZPair
MultInverse x y z = ((snd x), (fst x))

AddInverse : (x: ZZPair) -> ZZNotZero (snd x) -> ZZPair
AddInverse x a = (-(fst x), (snd x))

Subtraction : (x: ZZPair) -> ZZNotZero (snd x) -> (y: ZZPair) -> ZZNotZero (snd y) -> ZZPair
Subtraction x a y b = AddRationals x a (AddInverse y b) b

Division : (x: ZZPair) -> ZZNotZero (snd x) -> (y: ZZPair) -> ZZNotZero (fst y) -> ZZNotZero (snd y) -> ZZPair
Division x a y b c = MultiplyRationals x a (MultInverse y b c) b

--SimplifyRational : (x: Pair) -> NotZero (snd x) -> Pair
--SimplifyRational x a = (divides (gcdab fromIntegerNat((fst x)) fromIntegerNat((snd x))) ___ (fst x), divides (gcdab fromIntegerNat((fst x)) fromIntegerNat((snd x)) __ (snd x))

--To prove that the SimplifyRational works, we can just check if the output is equal to the input
-- To be done

simplifyRational : (x : ZZPair) -> ZZPair
simplifyRational (a, b) = (sa, sb) where
  sa = DbtoZZ (da / g) where
    da = ZZtoDb a
    g = cast {from=Integer} {to=Double}
      (gccd (cast {from=ZZ} {to=Integer}a,cast {from=ZZ} {to=Integer}b))
  sb = DbtoZZ (db / g) where
    db = ZZtoDb b
    g = cast {from=Integer} {to=Double}
      (gccd (cast {from=ZZ} {to=Integer}a,cast {from=ZZ} {to=Integer}b))

--Above, I will need to supply a proof that the GCD divides the two numbers. Then, the function defined above will produce the rational in simplified form.

xAndInverseNotZero : (x: ZZPair) -> (k: ZZNotZero (snd x)) -> ZZNotZero (snd (AddInverse x k))
xAndInverseNotZero x (ZZPositiveNotZero (snd x) y) = (ZZPositiveNotZero (snd x) y)

FirstIsInverted : (x: ZZPair) -> (k: ZZNotZero (snd x)) -> (a: ZZ) -> (a = (fst x)) -> ((-a) = fst (AddInverse x k))
FirstIsInverted x k a prf = (apZZ (\x => -x) a (fst x) prf)

SecondStaysSame : (x: ZZPair) -> (k: ZZNotZero (snd x)) -> (b: ZZ) -> (b = (snd x)) -> (b = (snd (AddInverse x k)))
SecondStaysSame x k b prf = (apZZ (\x => x) b (snd x) prf)

xplusinverse: (x: ZZPair) -> (k: ZZNotZero (snd x)) -> ZZPair
xplusinverse x k = AddRationals x k (AddInverse x k) (xAndInverseNotZero x k)

addinverselemma: (a: ZZ) -> (b: ZZ) -> ((-a)=b) -> (a + b = ((-a) + a)) -> ((-a)+a =0 ) -> (a + b = 0)
addinverselemma a b prf prf1 prf2 = trans prf1 prf2

addinverseFST: (x: ZZPair) -> (k: ZZNotZero (snd x)) -> (a: ZZ) -> (a = (fst x)) -> (fst (AddInverse x k) = b) -> ((-a) = b)
addinverseFST x k a prf prf1 = trans (FirstIsInverted x k a prf) (prf1)

addinverseSND: (x: ZZPair) -> (k: ZZNotZero (snd x)) -> (c: ZZ) -> (c = (snd x)) -> (snd (AddInverse x k) = b) -> (c = b)
addinverseSND x k c prf prf1 = trans (SecondStaysSame x k c prf) (prf1)


text:
{-
0.42
1.68
1.34
0.34
0.5 < 0.5 => False
0.5 <= 0.5 => True
0.5 == 0.5 => True
0.5 >= 0.5 => True
0.5 > 0.5 => False
0.5 compare 0.5 => EQ
0.5 max 0.5 => 0.5
0.5 min 0.5 => 0.5
0.5 < 1 => True
0.5 <= 1 => True
0.5 == 1 => False
0.5 >= 1 => False
0.5 > 1 => False
0.5 compare 1 => LT
0.5 max 1 => 1
0.5 min 1 => 0.5
1 < 0.5 => False
1 <= 0.5 => False
1 == 0.5 => False
1 >= 0.5 => True
1 > 0.5 => True
1 compare 0.5 => GT
1 max 0.5 => 1
1 min 0.5 => 0.5
1 < 1 => False
1 <= 1 => True
1 == 1 => True
1 >= 1 => True
1 > 1 => False
1 compare 1 => EQ
1 max 1 => 1
1 min 1 => 1
abs -1 => 1
- (-1) => 1
abs 1 => 1
- (1) => -1
-}
import CIL.FFI.Single

implementation Show Ordering where
  show EQ = "EQ"
  show LT = "LT"
  show GT = "GT"

testNum : IO ()
testNum =
  for_ [(*), (/), (+), (-)] $ \op =>
    printLn $ single 0.84 `op` single 0.5

testOrd : IO ()
testOrd = traverse_ putStrLn (test singles singles)
  where
    singles = [ single 0.5, single 1.0 ]

    op : Show r => String -> (Single -> Single -> r) -> (Single -> Single -> String)
    op name o = \x, y => show x ++ " " ++  name ++ " " ++ show y ++ " => " ++ show (x `o` y)

    operators : List (Single -> Single -> String)
    operators = [ op "<" (<), op "<=" (<=), op "==" (==)
                , op ">=" (>=), op ">" (>), op "compare" compare
                , op "max" max, op "min" min ]

    test : List Single -> List Single -> List String
    test xs ys = do
      x <- xs
      y <- ys
      map (\o => x `o` y) operators

testNeg : IO ()
testNeg =
  for_ [ single (-1), single 1 ] $ \x => do
    putStrLn $ "abs " ++ show x ++ " => " ++ show (abs x)
    putStrLn $ "- (" ++ show x ++ ") => " ++ show (-x)

main : IO ()
main = do
  testNum
  testOrd
  testNeg

-- Local Variables:
-- idris-load-packages: ("cil")
-- End:

max_stars_repo_name: timjs/iris-clean

max_issues_repo_name: timjs/iris-clean

max_forks_repo_name: timjs/iris-clean


text:
module Commons.Test.Unit.Parser

import Text.PrettyPrint.WL

import Text.Lexer
import Text.Parser

import Commons.Data.Location

import Commons.Text.Lexer.Run
import Commons.Text.Parser.Run

%default total
%access export

data TestReport : Type -> Type where
  ExpectedSuccess : (title : String) -> TestReport tok

  Failure : Show a => (title : String) -> (Run.ParseError a) -> TestReport a

  UnexpectedSuccess : (Show a)
                   => (title : String)
                   -> (made  : a)
                   -> TestReport tok

  FailureCmp : (Eq a, Show a)
            => (title, input : String)
            -> (expected : a)
            -> (given : a)
            -> TestReport tok

isSuccess : TestReport e -> Bool
isSuccess (ExpectedSuccess _) = True
isSuccess _ = False

parseTest : Show tok
         => (title : String)
         -> (p : String -> Either (Run.ParseError tok) ty)
         -> String
         -> TestReport tok
parseTest t run i =
  case run i of
    Left err => Failure t err
    Right _ => ExpectedSuccess t

parseFail : Show ty
         => (title : String)
         -> (p : String -> Either (Run.ParseError tok) (ty))
         -> String
         -> TestReport tok
parseFail t run i =
  case run i of
    Left _ => ExpectedSuccess t
    Right (res) => UnexpectedSuccess t res

parseTestAssert : (Show tok, Eq ty, Show ty)
               => (title : String)
               -> (p : String -> Either (Run.ParseError tok) (ty))
               -> String
               -> ty
               -> (ty -> ty -> Bool)
               -> TestReport tok
parseTestAssert t run i exp eq =
  case run i of
    Left err => Failure t err
    Right (given) =>
      if eq given exp
        then ExpectedSuccess t
        else FailureCmp t i exp given

showReport : (Run.ParseError tok -> String) -> TestReport tok -> Doc
showReport f (ExpectedSuccess t) =  text "[PASS]" <+> text t
showReport f (Failure t m) =
  vcat [ text "[FAIL] [PARSING]" <+> text t
       , indent 2 $ text "Gave error:"
       , indent 4 $ text (f m)
       ]
showReport f (UnexpectedSuccess t res) =
  vcat [ text "[FAIL] [RESULT]" <+> text t
       , indent 2 $ text "Unexpectedly made:"
       , indent 4 $ (text . show) res
       ]
showReport f (FailureCmp t i e g) =
  vcat [ text "[FAIL] [PARSING]" <+> text t
       , indent 2 $ text "Given input:"
       , indent 4 (text i)
       , indent 2 $ (text "Should have made:")
       , indent 4 $ (text . show) e
       , indent 2 $ (text "but made:")
       , indent 4 $ (text . show) g
       ]

runParseTest : Show tok => (Run.ParseError tok -> String) -> TestReport tok -> IO Bool
runParseTest f r = do putStrLn ((toString . showReport f) r)
                      pure (isSuccess r)

max_stars_repo_name: jfdm/idris-common

max_issues_repo_name: jfdm/idris-common

max_forks_repo_name: jfdm/idris-common


text:
import Arduino.Raw

import Control.Monad.Coop

forever : Monad m => m a -> m b
forever x = do x; forever x

export
main : IO Unit
main = runCoop $ do
  pinMode 3 1
  digitalWrite 3 1
  sleepFor 1000
  digitalWrite 3 0
  pinMode 13 1
  pinMode 6 1
  (<||>)
    (forever $ do
      digitalWrite 13 1
      sleepFor 1000
      digitalWrite 13 0
      sleepFor 2000)
    (forever $ do
      digitalWrite 6 1
      sleepFor 350
      digitalWrite 6 0
      sleepFor 750)

max_stars_repo_name: buzden/idris-arduino-lib

max_issues_repo_name: buzden/idris-arduino-lib

max_forks_repo_name: buzden/idris-arduino-lib


text:
module Prelude.Basics

import Builtin

%default total

public export
Not : Type -> Type
Not x = x -> Void

-----------------------
-- UTILITY FUNCTIONS --
-----------------------

||| Manually assign a type to an expression.
||| @ a the type to assign
||| @ x the element to get the type
public export %inline
the : (0 a : Type) -> (1 x : a) -> a
the _ x = x

||| Identity function.
public export %inline
id : (1 x : a) -> a           -- Hopefully linearity annotation won't
                              -- break equality proofs involving id
id x = x

||| Function that duplicates its input
public export
dup : a -> (a, a)
dup x = (x, x)

||| Constant function.  Ignores its second argument.
public export %inline
const : a -> b -> a
const x = \value => x

||| Function composition.
public export %inline
(.) : (b -> c) -> (a -> b) -> a -> c
(.) f g = \x => f (g x)

||| Takes in the first two arguments in reverse order.
||| @ f the function to flip
public export
flip : (f : a -> b -> c) -> b -> a -> c
flip f x y = f y x

||| Function application.
public export
apply : (a -> b) -> a -> b
apply f a = f a

public export
curry : ((a, b) -> c) -> a -> b -> c
curry f a b = f (a, b)

public export
uncurry : (a -> b -> c) -> (a, b) -> c
uncurry f (a, b) = f a b

-- $ is compiled specially to shortcut any tricky unification issues, but if
-- it did have a type this is what it would be, and it might be useful to
-- use directly sometimes (e.g. in higher order functions)
public export
($) : forall a, b . ((x : a) -> b x) -> (x : a) -> b x
($) f a = f a

-------------------
-- PROOF HELPERS --
-------------------

||| Equality is a congruence.
public export
cong : (0 f : t -> u) -> (1 p : a = b) -> f a = f b
cong f Refl = Refl

||| Two-holed congruence.
export
-- These are natural in equational reasoning.
cong2 : (0 f : t1 -> t2 -> u) -> (1 p1 : a = b) -> (1 p2 : c = d) -> f a c = f b d
cong2 f Refl Refl = Refl

--------------
-- BOOLEANS --
--------------

||| Boolean Data Type.
public export
data Bool = True | False

||| Boolean NOT.
public export
not : (1 b : Bool) -> Bool
not True = False
not False = True

||| Boolean AND only evaluates the second argument if the first is `True`.
public export
(&&) : (1 b : Bool) -> Lazy Bool -> Bool
(&&) True x = x
(&&) False x = False

||| Boolean OR only evaluates the second argument if the first is `False`.
public export
(||) : (1 b : Bool) -> Lazy Bool -> Bool
(||) True x = True
(||) False x = x

%inline
public export
intToBool : Int -> Bool
intToBool 0 = False
intToBool x = True


text:
module Language.Reflection.Types

-- inspired by https://github.com/MarcelineVQ/idris2-elab-deriving/

import public Language.Reflection.Pretty
import public Language.Reflection.Syntax
import public Language.Reflection
import Text.PrettyPrint.Prettyprinter

%language ElabReflection

--------------------------------------------------------------------------------
--          Utilities
--------------------------------------------------------------------------------

public export
Res : Type -> Type
Res = Either String

Eq Namespace where
  (MkNS xs) == (MkNS ys) = xs == ys

Eq Name where
  (UN a)   == (UN x)   = a == x
  (MN a b) == (MN x y) = a == x && b == y
  (NS a b) == (NS x y) = a == x && b == y
  (DN a b) == (DN x y) = a == x && b == y
  (RF a)   == (RF x)   = a == x
  _        == _        = False

--------------------------------------------------------------------------------
--          General Types
--------------------------------------------------------------------------------

||| Constructor of a data type
public export
record Con where
  constructor MkCon
  name : Name
  args : List NamedArg
  type : TTImp

||| Tries to lookup a constructor by name.
export
getCon : Name -> Elab Con
getCon n = do (n',tt)    <- lookupName n
              (args,tpe) <- unPiNamed tt
              pure $ MkCon n' args tpe

export
Pretty Con where
  prettyPrec p (MkCon n args tpe) = applyH p "MkCon" [n, args, tpe]

||| Information about a data type
|||
||| @name : Name of the data type
|||         Note: There is no guarantee that the name will be fully
|||         qualified
||| @args : Type arguments of the data type
||| @cons : List of data constructors
public export
record TypeInfo where
  constructor MkTypeInfo
  name : Name
  args : List NamedArg
  cons : List Con

export
Pretty TypeInfo where
  pretty (MkTypeInfo name args cons) =
    let head = applyH Open "MkTypeInfo" [name, args]
        cons = indent 2 $ vsep (map pretty cons)
     in vsep [head,cons]

||| Tries to get information about the data type specified
||| by name. The name need not be fully qualified, but
||| needs to be unambiguous.
export
getInfo' : Name -> Elab TypeInfo
getInfo' n =
  do (n',tt)        <- lookupName n
     (args,IType _) <- unPiNamed tt
                    | (_,_) => fail "Type declaration does not end in IType"
     conNames       <- getCons n'
     cons           <- traverse getCon conNames
     pure (MkTypeInfo n' args cons)

||| macro version of `getInfo'`
export %macro
getInfo : Name -> Elab TypeInfo
getInfo = getInfo'

||| Tries to get the name of the sole constructor
||| of data type specified by name. Fails, if
||| the name is not unambiguous, or if the data type
||| in question has not exactly one constructor.
export %macro
singleCon : Name -> Elab Name
singleCon n = do (MkTypeInfo _ _ cs) <- getInfo' n
                 (c::Nil) <- pure cs | _ => fail "not a single constructor"
                 pure $ name c

--------------------------------------------------------------------------------
--          Parameterized Types
--------------------------------------------------------------------------------

||| Explicit arg of a data constructor
|||
||| The `hasParam` flag indicates, whether one of the
||| type parameters of the data type makes an appearance
||| in the arguments type.
|||
||| For instance, in the following data type, arguments
||| a1 and a3 would have `hasParam` set to `True`.
|||
||| ```
|||   data MyData : (f : Type -> Type) -> (t : Type) -> Type where
|||     A : (a1 : f Int) -> (a2 : String) -> MyData f a
|||     B : (a3 : f a)   -> MyData f a
||| ```
public export
record ExplicitArg where
  constructor MkExplicitArg
  name     : Name
  tpe      : TTImp
  hasParam : Bool

export
Pretty ExplicitArg where
  prettyPrec p (MkExplicitArg n tpe hasParam) =
    applyH p "MkExplicitArg" [n, tpe, hasParam]

||| Constructor of a parameterized data type.
|||
||| We only accept two types of arguments for
||| such a constructor: Implicit arguments
||| corresponding to the parameters of the data types
||| and explicit arguments.
|||
||| See `ParamTypeInfo` for examples about what is
||| allowed and what not.
public export
record ParamCon where
  constructor MkParamCon
  name         : Name
  explicitArgs : List ExplicitArg

export
Pretty ParamCon where
  prettyPrec p (MkParamCon n explicitArgs) =
    applyH p "MkParamCon" [n, explicitArgs]

export
hasParamTypes : ParamCon -> List TTImp
hasParamTypes = mapMaybe hasParamType . explicitArgs
  where hasParamType : ExplicitArg -> Maybe TTImp
        hasParamType (MkExplicitArg _ t True) = Just t
        hasParamType _                        = Nothing

||| Information about a parameterized data type.
|||
||| The constructors of such a data type are only
||| allowed to have two kinds of arguments:
||| Implicit arguments corresponding to the data
||| type's parameters and explicit arguments.
|||
||| Auto implicits or existentials are not allowed.
|||
||| Below are some examples of valid parameterized data types
|||
||| ```
||| data Foo a = Val a | Nope
|||
||| data Reader : (m : Type -> Type) -> (e : Type) -> (a : Type) -> Type where
|||   MkReader : (run : e -> m a) -> Reader m e a
|||
||| data Wrapper : (n : Nat) -> (t : Type) -> Type
|||   Wrap : Vect n t -> Wrapper n t
||| ```
|||
||| Examples of valid parameterized data types
|||
||| Indexed types families:
|||
||| ```
||| data GADT : (t : Type) -> Type where
|||   A : GADT Int
|||   B : GADT ()
|||   Any : a -> GADT a
||| ```
|||
||| Existentials:
|||
||| ```
||| data Forget : Type where
|||  DoForget : a -> Forget
||| ```
|||
||| Constraint types:
|||
||| ```
||| data ShowableForget : Type where
|||  ShowForget : Show a => a -> Forget
||| ```
public export
record ParamTypeInfo where
  constructor MkParamTypeInfo
  name   : Name
  params : List (Name,TTImp)
  cons   : List ParamCon

export
Pretty ParamTypeInfo where
  pretty (MkParamTypeInfo name params cons) =
    let head = applyH Open "MkParamTypeInfo" [name, toList params]
        cons = indent 2 $ vsep (map pretty cons)
     in vsep [head,cons]

-- Given a Vect of type parameters (from the surrounding
-- data type), tries to extract a list of type parameter names
-- from the type declaration of a constructor.
private
conParams : (con : Name) -> Vect n a -> TTImp -> Res $ Vect n Name
conParams con as t = run as (snd $ unApp t)
  where err : String
        err = show con
            ++ ": Constructor type arguments do not match "
            ++ "data type type arguments."

        run : Vect k a -> List TTImp -> Res $ Vect k Name
        run [] []                        = Right []
        run (_ :: as) ((IVar _ n) :: ts) = (n ::) <$> run as ts
        run _         _                  = Left err

-- Renames all type parameter names in an argument's
-- type according to the given Vect of pairs.
-- Returns the renamed type and `True` if at least
-- one parameter was found, `False` otherwise.
private
rename : Vect n (Name,Name) -> TTImp -> (TTImp, Bool)
rename ns (IVar x n)        = case lookup n ns of
                                Nothing => (IVar x n, False)
                                Just n' => (IVar x n', True)

rename ns (IPi x y z w a r) = let (a',ba) = rename ns a
                                  (r',br) = rename ns r
                               in (IPi x y z w a' r', ba || br)

rename ns (IApp x y z)      = let (y',by) = rename ns y
                                  (z',bz) = rename ns z
                               in (IApp x y' z', by || bz)

rename _ t                  = (t, False)

private
implicitErr : (con: Name) -> (n : Name) -> Res a
implicitErr con n = Left $  show con
                         ++ ": Non-explicit constructor argument \""
                         ++ show n
                         ++ "\" is not a type parameter."

private
indicesErr : (con : Name) -> (ns : Vect k Name) -> Res a
indicesErr con ns = Left $ show con ++ ": Type indices found: " ++ show ns

-- For a constructor, takes a list of type parameter
-- names and tries to remove the corresponding implicit
-- arguments from the head of the given argument list.
-- Extracts explicit argument names and types from the rest of
-- the list.
--
-- Fails if : a) Not all values in `names` are present as implicit
--               function arguments
--            b) The function has additional non-implicit arguments
private
argPairs :  (con : Name)
         -> Vect n (Name,Name)
         -> List NamedArg
         -> Res $ List ExplicitArg
argPairs con names = run names
  where delete : Name -> Vect (S k) (Name,a) -> Res $ Vect k (Name,a)
        delete m ((n,a) :: ns)  =
          if m == n then Right ns
                    else case ns of
                              []        => implicitErr con m
                              ns@(_::_) => ((n,a) ::) <$> delete m ns

        mkArg : NamedArg -> Res ExplicitArg
        mkArg (MkArg _ ExplicitArg n t) = let (t',isP) = rename names t
                                           in Right $ MkExplicitArg n t' isP
        mkArg (MkArg _ _ n _)           = implicitErr con n

        run : Vect k (Name,a) -> List NamedArg -> Res $ List ExplicitArg
        run [] as = traverse mkArg as
        run ps@(_::_) ((MkArg _ ImplicitArg n _) :: t) = run !(delete n ps) t
        run ps _ = indicesErr con (map fst ps)

private
paramCon : Vect n Name -> Con -> Res $ ParamCon
paramCon ns (MkCon n as t) = do params <- conParams n ns t
                                args   <- argPairs n (zip params ns) as
                                pure $ MkParamCon n args

private
toParamTypeInfo : TypeInfo -> Res ParamTypeInfo
toParamTypeInfo (MkTypeInfo n as cs) =
  do ps  <- traverse expPair as
     let ns = map fst $ fromList ps
     cs' <- traverse (paramCon ns) cs
     pure $ MkParamTypeInfo n ps cs'
  where expPair : NamedArg -> Res (Name,TTImp)
        expPair  (MkArg _ ExplicitArg n t) = Right (n,t)
        expPair _ = Left $  show n
                         ++ ": Non-explicit type arguments are not supported"

||| Returns information about a parameterized data type
||| specified by the given (probably not fully qualified) name.
|||
||| The implementation makes sure, that all occurences of
||| type parameters in the constructors have been given
||| the same names as occurences in the type declaration.
export
getParamInfo' : Name -> Elab ParamTypeInfo
getParamInfo' n = do ti         <- getInfo' n
                     (Right pt) <- pure (toParamTypeInfo ti)
                                | (Left err) => fail err
                     pure pt

||| macro version of `getParamInfo`.
export %macro
getParamInfo : Name -> Elab ParamTypeInfo
getParamInfo = getParamInfo'


text:
module FunExt

public export
funext : {a : Type} -> {b : a -> Type} ->
         {f, g : (1 x : a) -> b x} -> (0 _ : (1 x : a) -> f x = g x) -> f = g
funext _  = believe_me ()

public export
funextW : {a : Type} -> {b : a -> Type} ->
          {f, g : (x : a) -> b x} -> (0 _ : (x : a) -> f x = g x) -> f = g
funextW _  = believe_me ()

public export
0 piext : {a : Type} -> {b : a -> Type} -> {b' : a -> Type} ->
         (0 _ : (1 x : a) -> b x = b' x) ->
         ((1 x : a) -> b x) = ((1 x : a) -> b' x)
piext p = cong (\ z => (1 x : a) -> z x) (funext p)

max_stars_repo_name: g-nakov/quantitative-poly

max_issues_repo_name: g-nakov/quantitative-poly

max_forks_repo_name: g-nakov/quantitative-poly


text:
module Main

import Language.Reflection
import Erlang

%default total
%language ElabReflection

%runElab generateAtomHelpers ["ok", "error"]

main : IO ()
main = do
  printLn A_ok
  printLn A_error


text:
data EqNat : (num1 : Nat) -> (num2 : Nat) -> Type where
     Same : (num : Nat) -> EqNat num num

sameS : (k : Nat) -> (j : Nat) -> (eq : EqNat k j) -> EqNat (S k) (S j)
sameS k k (Same k) = Same (S k)

sameS' : (eq : EqNat k j) -> EqNat (S k) (S j)
sameS' (Same k) = Same (S k)

checkEqNat : (num1 : Nat) -> (num2 : Nat) -> Maybe (EqNat num1 num2)
checkEqNat Z Z = Just $ Same 0
checkEqNat Z (S k) = Nothing
checkEqNat (S k) Z = Nothing
checkEqNat (S k) (S j) = case checkEqNat k j of
                              Nothing => Nothing
                              Just eq => Just (sameS _ _ eq)

data Vect : Nat -> Type -> Type where
  Nil : Vect Z a
  (::) : a -> Vect k a -> Vect (S k) a

exactLength : (len : Nat) -> (input : Vect m a) -> Maybe (Vect len a)
exactLength {m} len input = case checkEqNat m len of
                                 Nothing => Nothing
                                 Just (Same len) => Just input


text:
module SpecIOExample

import Specdris.SpecIO

%access private
%default total

startDb : IO ()
startDb = putStrLn "start database ..."

stopDb : IO ()
stopDb = putStrLn "... stoped database"

testData : IO SpecResult -> IO SpecResult
testData resultIO = do putStrLn "insert test data"
                       result <- resultIO
                       putStrLn "delete test data"

                       pure result

record User where
  constructor MkUser

  id : Nat
  name : String

getUser : Nat -> IO User
getUser id = pure (MkUser id "foo")

getUserSpec : SpecTree
getUserSpec = describe "User table" $ do
                it "get a user by id" $ do
                  user <- getUser 0

                  pure $ do (name user) === "foo"

export
specSuite : IO ()
specSuite = specIO {beforeAll = startDb} {around = testData} {afterAll = stopDb} $ do
              getUserSpec

max_stars_repo_name: pheymann/specdris

max_issues_repo_name: pheymann/specdris

max_forks_repo_name: pheymann/specdris


text:
-- ---------------------------------------------------------------- [ JSON.idr ]
-- Description : Parse JSON files.
--               This code was borrowed and improved from lightyear examples.
--
-- Copyright   : (c) Jan de Muijnck-Hughes
-- License     : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module Config.JSON

import public Data.AVL.Dict

import Effects
import Effect.File

import public Lightyear
import public Lightyear.Char
import public Lightyear.Strings

import public Config.Error

import Config.Parse.Utils
import Config.Parse.Common

%access private

-- ------------------------------------------------------------------- [ Model ]

public export
data JsonValue = JsonString String
               | JsonNumber Double
               | JsonBool Bool
               | JsonNull
               | JsonArray (List JsonValue)
               | JsonObject (Dict String JsonValue)

public export
Show JsonValue where
  show (JsonString s)   = show s
  show (JsonNumber x)   = show x
  show (JsonBool True ) = "true"
  show (JsonBool False) = "false"
  show  JsonNull        = "null"
  show (JsonArray  xs)  = show xs
  show (JsonObject xs)  =
      "{" ++ unwords (intersperse "," (map fmtItem $ Dict.toList xs)) ++ "}"
    where
      fmtItem (k, v) = show k ++ " : " ++ show v

-- ------------------------------------------------------------------ [ Parser ]
jsonString : Parser String
jsonString = quoted '"' <?> "JSON String"

jsonNumber : Parser Double
jsonNumber = map scientificToFloat parseScientific <?> "JSON Number"

jsonBool : Parser Bool
jsonBool  =  (char 't' >! string "rue"  *> pure True)
         <|> (char 'f' >! string "alse" *> pure False)
         <?> "JSON Bool"

jsonNull : Parser ()
jsonNull = (char 'n' >! string "ull" >! pure ()) <?> "JSON Null"

mutual
  jsonArray : Parser (List JsonValue)
  jsonArray = brackets (commaSep jsonValue) <?> "JSON Array"

  keyValuePair : Parser (String, JsonValue)
  keyValuePair = do
      key <- spaces *> jsonString <* spaces
      colon
      value <- jsonValue
      pure (key, value)
    <?> "JSON KV Pair"

  jsonObject : Parser (Dict String JsonValue)
  jsonObject = map fromList $ braces (commaSep (keyValuePair)) <?> "JSON Object"

  jsonValue' : Parser JsonValue
  jsonValue' =  (map JsonString jsonString)
            <|> (map JsonNumber jsonNumber)
            <|> (map JsonBool   jsonBool)
            <|> (pure JsonNull <* jsonNull)
            <|>| map JsonArray  jsonArray
            <|>| map JsonObject jsonObject

  jsonValue : Parser JsonValue
  jsonValue = spaces *> jsonValue' <* spaces <?> "JSON Value"

export
parseJSONFile : Parser JsonValue
parseJSONFile = (map JsonArray jsonArray)
            <|> (map JsonObject jsonObject)
            <?> "JSON Files"

export
toString : JsonValue -> String
toString doc = show doc

export
fromString : String -> Either ConfigError JsonValue
fromString str =
    case parse parseJSONFile str of
      Left err  => Left (PureParseErr err)
      Right doc => Right doc

-- -------------------------------------------------------------------- [ Read ]
export
readJSONConfig : String -> Eff (Either ConfigError JsonValue) [FILE ()]
readJSONConfig = readConfigFile parseJSONFile

-- --------------------------------------------------------------------- [ EOF ]

max_stars_repo_name: jfdm/idris-config

max_issues_repo_name: jfdm/idris-config

max_forks_repo_name: jfdm/idris-config


text:
||| Functionality to convert an Idris `NamedCExp`
||| to a sequence of imperative statements.
module Compiler.ES.ToAst

import Data.DPair
import Data.Nat
import Data.List1
import Data.Vect
import Compiler.Common
import Core.CompileExpr
import Core.Context
import Compiler.ES.Ast
import Compiler.ES.State
import Libraries.Data.SortedMap

--------------------------------------------------------------------------------
--          Converting NamedCExp
--------------------------------------------------------------------------------

-- used to convert data and type constructor tags
tag : Name -> Maybe Int -> Either Int Name
tag n = maybe (Right n) Left

-- creates a single assignment statement.
assign : (e : Effect) -> Exp -> Stmt (Just e)
assign Returns          = Return
assign (ErrorWithout v) = Assign v

mutual
  getInteger : NamedCExp -> Maybe Integer
  getInteger (NmPrimVal _ $ BI x) = Just x
  getInteger x                    = integerArith x

  -- this is a local hack to fix #1320 for the JS backend
  -- the moste basic sequences of arithmetic `Integer` expressions
  -- are evaluated to prevent us from introducing slow
  -- cascades of (1n + ...) coming from small `Nat` literals.
  integerArith : NamedCExp -> Maybe Integer
  integerArith (NmOp _ (Add IntegerType) [x,y]) =
    [| getInteger x + getInteger y |]
  integerArith (NmOp _ (Mul IntegerType) [x,y]) =
    [| getInteger x * getInteger y |]
  integerArith _ = Nothing

mutual
  -- Converts a `NamedCExp` by calling `stmt` with a
  -- newly generated local variable.
  -- If the result is a single assignment statement
  -- and the given filter function returns a `Just a`,
  -- only result `a` is returned.
  -- If the result is more complex or the filter returns
  -- `Nothing`, the resulting block
  -- will be kept and a pointer to the new variable
  -- will be returned which can then be used for instance
  -- as a function's argument.
  lift :  { auto c : Ref ESs ESSt }
       -> NamedCExp
       -> (filter  : Exp -> Maybe a)
       -> (fromVar : Var -> a)
       -> Core (List (Stmt Nothing), a)
  lift n filter fromVar = do
    l <- nextLocal
    b <- stmt (ErrorWithout l) n
    let pair = ([declare b], fromVar l)
    case b of
      -- elaborator needed some help here
      Assign _ e => pure $ maybe pair (the (List _) [],) (filter e)
      _          => pure pair

  -- Convert and lift (if necessary, see comment for `lift`)
  -- a function argument. The filter function used to
  -- decide whether to keep or lift a function argument
  -- comes from the passed `ESSt` state and can therefore
  -- vary across backends.
  liftArg : { auto c : Ref ESs ESSt }
           -> NamedCExp
           -> Core (List (Stmt Nothing), Exp)
  liftArg x = do
    f <- isArg <$> get ESs
    lift x (\e => guard (f e) $> e) (EMinimal . MVar)

  -- Convert and lift (if necessary, see comment for `lift`)
  -- a function expression.
  liftFun : { auto c : Ref ESs ESSt }
           -> NamedCExp
           -> Core (List (Stmt Nothing), Exp)
  liftFun x = do
    f <- isFun <$> get ESs
    lift x (\e => guard (f e) $> e) (EMinimal . MVar)

  -- Convert and lift (if necessary, see comment for `liftArg`)
  -- a `Vect` of function arguments.
  liftArgsVect : { auto c : Ref ESs ESSt }
               -> Vect n NamedCExp
               -> Core (List (Stmt Nothing), Vect n Exp)
  liftArgsVect xs = do
    ps <- traverseVect liftArg xs
    pure (concatMap fst ps, map snd ps)

  -- Convert and lift (if necessary, see comment for `liftArg`)
  -- a `List` of function arguments.
  liftArgs : { auto c : Ref ESs ESSt }
           -> List NamedCExp
           -> Core (List (Stmt Nothing), List Exp)
  liftArgs xs = do
    ps <- traverse liftArg xs
    pure (concatMap fst ps, map snd ps)

  -- Convert and lift an expression. If the result is
  -- not a `Minimal` expression, an additional assignment statement is
  -- generated. This is used to lift the scrutinees of
  -- constructor case expressions to make sure they are
  -- only evluated once (see also PR #1494).
  liftMinimal : { auto c : Ref ESs ESSt }
              -> NamedCExp
              -> Core (List (Stmt Nothing), Minimal)
  liftMinimal n = lift n toMinimal MVar

  -- creates a (possibly multiargument) lambda.
  lambda : {auto c : Ref ESs ESSt} -> Name -> NamedCExp -> Core Exp
  lambda n x = go [n] x
    where go : List Name -> NamedCExp -> Core Exp
          go ns (NmLam _  n x) = go (n :: ns) x
          go ns x              = do
            vs <- traverse registerLocal (reverse ns)
            ELam vs <$> stmt Returns x

  -- convert a `NamedCExp` to a sequence of statements.
  export
  stmt :  {auto c : Ref ESs ESSt}
        -> (e : Effect)
        -> NamedCExp
        -> Core (Stmt $ Just e)
  -- a local name gets registered or resolved
  stmt e (NmLocal _ n) = assign e . EMinimal <$> getOrRegisterLocal n

  -- a function name gets registered or resolved
  stmt e (NmRef _ n) = assign e . EMinimal . MVar <$> getOrRegisterRef n

  stmt e (NmLam _ n x) = assign e <$> lambda n x

  -- in case of a let expression, we just generate two
  -- blocks of statements and concatenate them.
  -- We always introduce a new local variable for `n`,
  -- since a variable called `n` might be used in both blocks.
  stmt e (NmLet _ n y z) = do
    v  <- nextLocal
    b1 <- stmt (ErrorWithout v) y
    addLocal n (MVar v)
    b2 <- stmt e z
    pure $ prepend [declare b1] b2

  -- when applying a function, we potentially need to
  -- lift both, the function expression itself and the argument
  -- list, to the surrounding scope.
  stmt e (NmApp _ x xs) = do
    (mbx, vx)    <- liftFun x
    (mbxs, args) <- liftArgs xs
    pure . prepend (mbx ++ mbxs) $ assign e (EApp vx args)

  stmt e (NmCon _ n ci tg xs) = do
    (mbxs, args) <- liftArgs xs
    pure . prepend mbxs $ assign e (ECon (tag n tg) ci args)

  stmt e o@(NmOp _ x xs) =
    case integerArith o of
      Just n  => pure . assign e $ EPrimVal (BI n)
      Nothing => do
        (mbxs, args) <- liftArgsVect xs
        pure . prepend mbxs $ assign e (EOp x args)

  stmt e (NmExtPrim _ n xs) = do
    (mbxs, args) <- liftArgs xs
    pure . prepend mbxs $ assign e (EExtPrim n args)

  stmt e (NmForce _ _ x) = do
    (mbx, vx) <- liftFun x
    pure . prepend mbx $ assign e (EApp vx [])

  stmt e (NmDelay _ _ x) = assign e . ELam [] <$> stmt Returns x

  -- No need for a `switch` if we only have a single branch.
  -- It's still necessary to lift the scrutinee, however,
  -- since its fields might be accessed several times in
  -- the implementation of `x`.
  stmt e (NmConCase _ sc [x] Nothing) = do
    (mbx, vx) <- liftMinimal sc
    b         <- body <$> conAlt e vx x
    pure $ prepend mbx b

  -- No need for a `switch` statement if we only have
  -- a `default` branch.
  stmt e (NmConCase _ _  [] (Just x)) = stmt e x

  -- Create a `switch` statement from a pattern match
  -- on constructors. The scrutinee is lifted to the
  -- surrounding scope and memoized if necessary.
  stmt e (NmConCase _ sc xs x) = do
    (mbx, vx) <- liftMinimal sc
    alts      <- traverse (conAlt e vx) xs
    def       <- traverseOpt (stmt e) x
    pure . prepend mbx $ ConSwitch e vx alts def

  -- Pattern matches on constants behave very similar
  -- to the ones on constructors.
  stmt e (NmConstCase _ _  [x] Nothing) = body <$> constAlt e x
  stmt e (NmConstCase _ _  [] (Just x)) = stmt e x
  stmt e (NmConstCase _ sc xs x) = do
    (mbx, ex) <- liftArg sc
    alts      <- traverse (constAlt e) xs
    def       <- traverseOpt (stmt e) x
    pure . prepend mbx $ ConstSwitch e ex alts def

  stmt e (NmPrimVal _ x) = pure . assign e $ EPrimVal x

  stmt e (NmErased _)    = pure . assign e $ EErased

  stmt _ (NmCrash _ x)   = pure $ Error x

  -- a single branch in a pattern match on constructors
  conAlt :  { auto c : Ref ESs ESSt }
         -> (e         : Effect)
         -> (scrutinee : Minimal)
         -> NamedConAlt
         -> Core (EConAlt e)
  conAlt e sc (MkNConAlt n ci tg args x) = do
    -- We map the list of args to the corresponding
    -- data projections (field accessors). They'll
    -- be then properly inlined when converting `x`.
    projections sc args
    MkEConAlt (tag n tg) ci <$> stmt e x

  -- a single branch in a pattern match on a constant
  constAlt :  { auto c : Ref ESs ESSt }
           -> (e : Effect)
           -> NamedConstAlt
           -> Core (EConstAlt e)
  constAlt e (MkNConstAlt c x) = MkEConstAlt c <$> stmt e x


text:
module Web.Internal.GeometryPrim

import JS
import Web.Internal.Types

--------------------------------------------------------------------------------
--          Interfaces
--------------------------------------------------------------------------------

namespace DOMMatrix

  export
  %foreign "browser:lambda:(a)=>DOMMatrix.fromFloat32Array(a)"
  prim__fromFloat32Array : Float32Array -> PrimIO DOMMatrix

  export
  %foreign "browser:lambda:(a)=>DOMMatrix.fromFloat64Array(a)"
  prim__fromFloat64Array : Float64Array -> PrimIO DOMMatrix

  export
  %foreign "browser:lambda:(a)=>DOMMatrix.fromMatrix(a)"
  prim__fromMatrix : UndefOr DOMMatrixInit -> PrimIO DOMMatrix

  export
  %foreign "browser:lambda:x=>x.invertSelf()"
  prim__invertSelf : DOMMatrix -> PrimIO DOMMatrix

  export
  %foreign "browser:lambda:(x,a)=>x.multiplySelf(a)"
  prim__multiplySelf : DOMMatrix -> UndefOr DOMMatrixInit -> PrimIO DOMMatrix

  export
  %foreign "browser:lambda:(x,a)=>x.preMultiplySelf(a)"
  prim__preMultiplySelf : DOMMatrix -> UndefOr DOMMatrixInit -> PrimIO DOMMatrix

  export
  %foreign "browser:lambda:(x,a,b,c,d)=>x.rotateAxisAngleSelf(a,b,c,d)"
  prim__rotateAxisAngleSelf :  DOMMatrix
                            -> UndefOr Double
                            -> UndefOr Double
                            -> UndefOr Double
                            -> UndefOr Double
                            -> PrimIO DOMMatrix

  export
  %foreign "browser:lambda:(x,a,b)=>x.rotateFromVectorSelf(a,b)"
  prim__rotateFromVectorSelf :  DOMMatrix
                             -> UndefOr Double
                             -> UndefOr Double
                             -> PrimIO DOMMatrix

  export
  %foreign "browser:lambda:(x,a,b,c)=>x.rotateSelf(a,b,c)"
  prim__rotateSelf :  DOMMatrix
                   -> UndefOr Double
                   -> UndefOr Double
                   -> UndefOr Double
                   -> PrimIO DOMMatrix

  export
  %foreign "browser:lambda:(x,a,b,c,d)=>x.scale3dSelf(a,b,c,d)"
  prim__scale3dSelf :  DOMMatrix
                    -> UndefOr Double
                    -> UndefOr Double
                    -> UndefOr Double
                    -> UndefOr Double
                    -> PrimIO DOMMatrix

  export
  %foreign "browser:lambda:(x,a,b,c,d,e,f)=>x.scaleSelf(a,b,c,d,e,f)"
  prim__scaleSelf :  DOMMatrix
                  -> UndefOr Double
                  -> UndefOr Double
                  -> UndefOr Double
                  -> UndefOr Double
                  -> UndefOr Double
                  -> UndefOr Double
                  -> PrimIO DOMMatrix

  export
  %foreign "browser:lambda:(x,a)=>x.setMatrixValue(a)"
  prim__setMatrixValue : DOMMatrix -> String -> PrimIO DOMMatrix

  export
  %foreign "browser:lambda:(x,a)=>x.skewXSelf(a)"
  prim__skewXSelf : DOMMatrix -> UndefOr Double -> PrimIO DOMMatrix

  export
  %foreign "browser:lambda:(x,a)=>x.skewYSelf(a)"
  prim__skewYSelf : DOMMatrix -> UndefOr Double -> PrimIO DOMMatrix

  export
  %foreign "browser:lambda:(x,a,b,c)=>x.translateSelf(a,b,c)"
  prim__translateSelf :  DOMMatrix
                      -> UndefOr Double
                      -> UndefOr Double
                      -> UndefOr Double
                      -> PrimIO DOMMatrix

namespace DOMMatrixReadOnly

  export
  %foreign "browser:lambda:(a)=>DOMMatrixReadOnly.fromFloat32Array(a)"
  prim__fromFloat32Array : Float32Array -> PrimIO DOMMatrixReadOnly

  export
  %foreign "browser:lambda:(a)=>DOMMatrixReadOnly.fromFloat64Array(a)"
  prim__fromFloat64Array : Float64Array -> PrimIO DOMMatrixReadOnly

  export
  %foreign "browser:lambda:(a)=>DOMMatrixReadOnly.fromMatrix(a)"
  prim__fromMatrix : UndefOr DOMMatrixInit -> PrimIO DOMMatrixReadOnly

  export
  %foreign "browser:lambda:x=>x.a"
  prim__a : DOMMatrixReadOnly -> PrimIO Double

  export
  %foreign "browser:lambda:x=>x.b"
  prim__b : DOMMatrixReadOnly -> PrimIO Double

  export
  %foreign "browser:lambda:x=>x.c"
  prim__c : DOMMatrixReadOnly -> PrimIO Double

  export
  %foreign "browser:lambda:x=>x.d"
  prim__d : DOMMatrixReadOnly -> PrimIO Double

  export
  %foreign "browser:lambda:x=>x.e"
  prim__e : DOMMatrixReadOnly -> PrimIO Double

  export
  %foreign "browser:lambda:x=>x.f"
  prim__f : DOMMatrixReadOnly -> PrimIO Double

  export
  %foreign "browser:lambda:x=>x.is2D"
  prim__is2D : DOMMatrixReadOnly -> PrimIO Boolean

  export
  %foreign "browser:lambda:x=>x.isIdentity"
  prim__isIdentity : DOMMatrixReadOnly -> PrimIO Boolean

  export
  %foreign "browser:lambda:x=>x.m11"
  prim__m11 : DOMMatrixReadOnly -> PrimIO Double

  export
  %foreign "browser:lambda:x=>x.m12"
  prim__m12 : DOMMatrixReadOnly -> PrimIO Double

  export
  %foreign "browser:lambda:x=>x.m13"
  prim__m13 : DOMMatrixReadOnly -> PrimIO Double

  export
  %foreign "browser:lambda:x=>x.m14"
  prim__m14 : DOMMatrixReadOnly -> PrimIO Double

  export
  %foreign "browser:lambda:x=>x.m21"
  prim__m21 : DOMMatrixReadOnly -> PrimIO Double

  export
  %foreign "browser:lambda:x=>x.m22"
  prim__m22 : DOMMatrixReadOnly -> PrimIO Double

  export
  %foreign "browser:lambda:x=>x.m23"
  prim__m23 : DOMMatrixReadOnly -> PrimIO Double

  export
  %foreign "browser:lambda:x=>x.m24"
  prim__m24 : DOMMatrixReadOnly -> PrimIO Double

  export
  %foreign "browser:lambda:x=>x.m31"
  prim__m31 : DOMMatrixReadOnly -> PrimIO Double

  export
  %foreign "browser:lambda:x=>x.m32"
  prim__m32 : DOMMatrixReadOnly -> PrimIO Double

  export
  %foreign "browser:lambda:x=>x.m33"
  prim__m33 : DOMMatrixReadOnly -> PrimIO Double

  export
  %foreign "browser:lambda:x=>x.m34"
  prim__m34 : DOMMatrixReadOnly -> PrimIO Double

  export
  %foreign "browser:lambda:x=>x.m41"
  prim__m41 : DOMMatrixReadOnly -> PrimIO Double

  export
  %foreign "browser:lambda:x=>x.m42"
  prim__m42 : DOMMatrixReadOnly -> PrimIO Double

  export
  %foreign "browser:lambda:x=>x.m43"
  prim__m43 : DOMMatrixReadOnly -> PrimIO Double

  export
  %foreign "browser:lambda:x=>x.m44"
  prim__m44 : DOMMatrixReadOnly -> PrimIO Double

  export
  %foreign "browser:lambda:x=>x.flipX()"
  prim__flipX : DOMMatrixReadOnly -> PrimIO DOMMatrix

  export
  %foreign "browser:lambda:x=>x.flipY()"
  prim__flipY : DOMMatrixReadOnly -> PrimIO DOMMatrix

  export
  %foreign "browser:lambda:x=>x.inverse()"
  prim__inverse : DOMMatrixReadOnly -> PrimIO DOMMatrix

  export
  %foreign "browser:lambda:(x,a)=>x.multiply(a)"
  prim__multiply :  DOMMatrixReadOnly
                 -> UndefOr DOMMatrixInit
                 -> PrimIO DOMMatrix

  export
  %foreign "browser:lambda:(x,a,b,c,d)=>x.rotateAxisAngle(a,b,c,d)"
  prim__rotateAxisAngle :  DOMMatrixReadOnly
                        -> UndefOr Double
                        -> UndefOr Double
                        -> UndefOr Double
                        -> UndefOr Double
                        -> PrimIO DOMMatrix

  export
  %foreign "browser:lambda:(x,a,b,c)=>x.rotate(a,b,c)"
  prim__rotate :  DOMMatrixReadOnly
               -> UndefOr Double
               -> UndefOr Double
               -> UndefOr Double
               -> PrimIO DOMMatrix

  export
  %foreign "browser:lambda:(x,a,b)=>x.rotateFromVector(a,b)"
  prim__rotateFromVector :  DOMMatrixReadOnly
                         -> UndefOr Double
                         -> UndefOr Double
                         -> PrimIO DOMMatrix

  export
  %foreign "browser:lambda:(x,a,b,c,d)=>x.scale3d(a,b,c,d)"
  prim__scale3d :  DOMMatrixReadOnly
                -> UndefOr Double
                -> UndefOr Double
                -> UndefOr Double
                -> UndefOr Double
                -> PrimIO DOMMatrix

  export
  %foreign "browser:lambda:(x,a,b,c,d,e,f)=>x.scale(a,b,c,d,e,f)"
  prim__scale :  DOMMatrixReadOnly
              -> UndefOr Double
              -> UndefOr Double
              -> UndefOr Double
              -> UndefOr Double
              -> UndefOr Double
              -> UndefOr Double
              -> PrimIO DOMMatrix

  export
  %foreign "browser:lambda:(x,a,b)=>x.scaleNonUniform(a,b)"
  prim__scaleNonUniform :  DOMMatrixReadOnly
                        -> UndefOr Double
                        -> UndefOr Double
                        -> PrimIO DOMMatrix

  export
  %foreign "browser:lambda:(x,a)=>x.skewX(a)"
  prim__skewX : DOMMatrixReadOnly -> UndefOr Double -> PrimIO DOMMatrix

  export
  %foreign "browser:lambda:(x,a)=>x.skewY(a)"
  prim__skewY : DOMMatrixReadOnly -> UndefOr Double -> PrimIO DOMMatrix

  export
  %foreign "browser:lambda:x=>x.toFloat32Array()"
  prim__toFloat32Array : DOMMatrixReadOnly -> PrimIO Float32Array

  export
  %foreign "browser:lambda:x=>x.toFloat64Array()"
  prim__toFloat64Array : DOMMatrixReadOnly -> PrimIO Float64Array

  export
  %foreign "browser:lambda:x=>x.toJSON()"
  prim__toJSON : DOMMatrixReadOnly -> PrimIO Object

  export
  %foreign "browser:lambda:x=>x.toString()"
  prim__toString : DOMMatrixReadOnly -> PrimIO String

  export
  %foreign "browser:lambda:(x,a)=>x.transformPoint(a)"
  prim__transformPoint :  DOMMatrixReadOnly
                       -> UndefOr DOMPointInit
                       -> PrimIO DOMPoint

  export
  %foreign "browser:lambda:(x,a,b,c)=>x.translate(a,b,c)"
  prim__translate :  DOMMatrixReadOnly
                  -> UndefOr Double
                  -> UndefOr Double
                  -> UndefOr Double
                  -> PrimIO DOMMatrix

namespace DOMPoint

  export
  %foreign "browser:lambda:(a)=>DOMPoint.fromPoint(a)"
  prim__fromPoint : UndefOr DOMPointInit -> PrimIO DOMPoint

namespace DOMPointReadOnly

  export
  %foreign "browser:lambda:(a)=>DOMPointReadOnly.fromPoint(a)"
  prim__fromPoint : UndefOr DOMPointInit -> PrimIO DOMPointReadOnly

  export
  %foreign "browser:lambda:x=>x.w"
  prim__w : DOMPointReadOnly -> PrimIO Double

  export
  %foreign "browser:lambda:x=>x.x"
  prim__x : DOMPointReadOnly -> PrimIO Double

  export
  %foreign "browser:lambda:x=>x.y"
  prim__y : DOMPointReadOnly -> PrimIO Double

  export
  %foreign "browser:lambda:x=>x.z"
  prim__z : DOMPointReadOnly -> PrimIO Double

  export
  %foreign "browser:lambda:(x,a)=>x.matrixTransform(a)"
  prim__matrixTransform :  DOMPointReadOnly
                        -> UndefOr DOMMatrixInit
                        -> PrimIO DOMPoint

  export
  %foreign "browser:lambda:x=>x.toJSON()"
  prim__toJSON : DOMPointReadOnly -> PrimIO Object

namespace DOMQuad

  export
  %foreign "browser:lambda:(a)=>DOMQuad.fromQuad(a)"
  prim__fromQuad : UndefOr DOMQuadInit -> PrimIO DOMQuad

  export
  %foreign "browser:lambda:(a)=>DOMQuad.fromRect(a)"
  prim__fromRect : UndefOr DOMRectInit -> PrimIO DOMQuad

  export
  %foreign "browser:lambda:x=>x.p1"
  prim__p1 : DOMQuad -> PrimIO DOMPoint

  export
  %foreign "browser:lambda:x=>x.p2"
  prim__p2 : DOMQuad -> PrimIO DOMPoint

  export
  %foreign "browser:lambda:x=>x.p3"
  prim__p3 : DOMQuad -> PrimIO DOMPoint

  export
  %foreign "browser:lambda:x=>x.p4"
  prim__p4 : DOMQuad -> PrimIO DOMPoint

  export
  %foreign "browser:lambda:x=>x.getBounds()"
  prim__getBounds : DOMQuad -> PrimIO DOMRect

  export
  %foreign "browser:lambda:x=>x.toJSON()"
  prim__toJSON : DOMQuad -> PrimIO Object

namespace DOMRect

  export
  %foreign "browser:lambda:(a)=>DOMRect.fromRect(a)"
  prim__fromRect : UndefOr DOMRectInit -> PrimIO DOMRect

namespace DOMRectList

  export
  %foreign "browser:lambda:x=>x.length"
  prim__length : DOMRectList -> PrimIO Bits32

  export
  %foreign "browser:lambda:(x,a)=>x.item(a)"
  prim__item : DOMRectList -> Bits32 -> PrimIO (Nullable DOMRect)

namespace DOMRectReadOnly

  export
  %foreign "browser:lambda:(a)=>DOMRectReadOnly.fromRect(a)"
  prim__fromRect : UndefOr DOMRectInit -> PrimIO DOMRectReadOnly

  export
  %foreign "browser:lambda:x=>x.bottom"
  prim__bottom : DOMRectReadOnly -> PrimIO Double

  export
  %foreign "browser:lambda:x=>x.height"
  prim__height : DOMRectReadOnly -> PrimIO Double

  export
  %foreign "browser:lambda:x=>x.left"
  prim__left : DOMRectReadOnly -> PrimIO Double

  export
  %foreign "browser:lambda:x=>x.right"
  prim__right : DOMRectReadOnly -> PrimIO Double

  export
  %foreign "browser:lambda:x=>x.top"
  prim__top : DOMRectReadOnly -> PrimIO Double

  export
  %foreign "browser:lambda:x=>x.width"
  prim__width : DOMRectReadOnly -> PrimIO Double

  export
  %foreign "browser:lambda:x=>x.x"
  prim__x : DOMRectReadOnly -> PrimIO Double

  export
  %foreign "browser:lambda:x=>x.y"
  prim__y : DOMRectReadOnly -> PrimIO Double

  export
  %foreign "browser:lambda:x=>x.toJSON()"
  prim__toJSON : DOMRectReadOnly -> PrimIO Object

--------------------------------------------------------------------------------
--          Dictionaries
--------------------------------------------------------------------------------

namespace DOMMatrix2DInit

  export
  %foreign "browser:lambda:(a,b,c,d,e,f,g,h,i,j,k,l)=> {a: a,b: b,c: c,d: d,e: e,f: f,m11: g,m12: h,m21: i,m22: j,m41: k,m42: l}"
  prim__new :  UndefOr Double
            -> UndefOr Double
            -> UndefOr Double
            -> UndefOr Double
            -> UndefOr Double
            -> UndefOr Double
            -> UndefOr Double
            -> UndefOr Double
            -> UndefOr Double
            -> UndefOr Double
            -> UndefOr Double
            -> UndefOr Double
            -> PrimIO DOMMatrix2DInit

  export
  %foreign "browser:lambda:x=>x.a"
  prim__a : DOMMatrix2DInit -> PrimIO (UndefOr Double)

  export
  %foreign "browser:lambda:(x,v)=>{x.a = v}"
  prim__setA : DOMMatrix2DInit -> UndefOr Double -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.b"
  prim__b : DOMMatrix2DInit -> PrimIO (UndefOr Double)

  export
  %foreign "browser:lambda:(x,v)=>{x.b = v}"
  prim__setB : DOMMatrix2DInit -> UndefOr Double -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.c"
  prim__c : DOMMatrix2DInit -> PrimIO (UndefOr Double)

  export
  %foreign "browser:lambda:(x,v)=>{x.c = v}"
  prim__setC : DOMMatrix2DInit -> UndefOr Double -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.d"
  prim__d : DOMMatrix2DInit -> PrimIO (UndefOr Double)

  export
  %foreign "browser:lambda:(x,v)=>{x.d = v}"
  prim__setD : DOMMatrix2DInit -> UndefOr Double -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.e"
  prim__e : DOMMatrix2DInit -> PrimIO (UndefOr Double)

  export
  %foreign "browser:lambda:(x,v)=>{x.e = v}"
  prim__setE : DOMMatrix2DInit -> UndefOr Double -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.f"
  prim__f : DOMMatrix2DInit -> PrimIO (UndefOr Double)

  export
  %foreign "browser:lambda:(x,v)=>{x.f = v}"
  prim__setF : DOMMatrix2DInit -> UndefOr Double -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.m11"
  prim__m11 : DOMMatrix2DInit -> PrimIO (UndefOr Double)

  export
  %foreign "browser:lambda:(x,v)=>{x.m11 = v}"
  prim__setM11 : DOMMatrix2DInit -> UndefOr Double -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.m12"
  prim__m12 : DOMMatrix2DInit -> PrimIO (UndefOr Double)

  export
  %foreign "browser:lambda:(x,v)=>{x.m12 = v}"
  prim__setM12 : DOMMatrix2DInit -> UndefOr Double -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.m21"
  prim__m21 : DOMMatrix2DInit -> PrimIO (UndefOr Double)

  export
  %foreign "browser:lambda:(x,v)=>{x.m21 = v}"
  prim__setM21 : DOMMatrix2DInit -> UndefOr Double -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.m22"
  prim__m22 : DOMMatrix2DInit -> PrimIO (UndefOr Double)

  export
  %foreign "browser:lambda:(x,v)=>{x.m22 = v}"
  prim__setM22 : DOMMatrix2DInit -> UndefOr Double -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.m41"
  prim__m41 : DOMMatrix2DInit -> PrimIO (UndefOr Double)

  export
  %foreign "browser:lambda:(x,v)=>{x.m41 = v}"
  prim__setM41 : DOMMatrix2DInit -> UndefOr Double -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.m42"
  prim__m42 : DOMMatrix2DInit -> PrimIO (UndefOr Double)

  export
  %foreign "browser:lambda:(x,v)=>{x.m42 = v}"
  prim__setM42 : DOMMatrix2DInit -> UndefOr Double -> PrimIO ()

namespace DOMMatrixInit

  export
  %foreign "browser:lambda:(a,b,c,d,e,f,g,h,i,j,k)=> {m13: a,m14: b,m23: c,m24: d,m31: e,m32: f,m33: g,m34: h,m43: i,m44: j,is2D: k}"
  prim__new :  UndefOr Double
            -> UndefOr Double
            -> UndefOr Double
            -> UndefOr Double
            -> UndefOr Double
            -> UndefOr Double
            -> UndefOr Double
            -> UndefOr Double
            -> UndefOr Double
            -> UndefOr Double
            -> UndefOr Boolean
            -> PrimIO DOMMatrixInit

  export
  %foreign "browser:lambda:x=>x.is2D"
  prim__is2D : DOMMatrixInit -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.is2D = v}"
  prim__setIs2D : DOMMatrixInit -> UndefOr Boolean -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.m13"
  prim__m13 : DOMMatrixInit -> PrimIO (UndefOr Double)

  export
  %foreign "browser:lambda:(x,v)=>{x.m13 = v}"
  prim__setM13 : DOMMatrixInit -> UndefOr Double -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.m14"
  prim__m14 : DOMMatrixInit -> PrimIO (UndefOr Double)

  export
  %foreign "browser:lambda:(x,v)=>{x.m14 = v}"
  prim__setM14 : DOMMatrixInit -> UndefOr Double -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.m23"
  prim__m23 : DOMMatrixInit -> PrimIO (UndefOr Double)

  export
  %foreign "browser:lambda:(x,v)=>{x.m23 = v}"
  prim__setM23 : DOMMatrixInit -> UndefOr Double -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.m24"
  prim__m24 : DOMMatrixInit -> PrimIO (UndefOr Double)

  export
  %foreign "browser:lambda:(x,v)=>{x.m24 = v}"
  prim__setM24 : DOMMatrixInit -> UndefOr Double -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.m31"
  prim__m31 : DOMMatrixInit -> PrimIO (UndefOr Double)

  export
  %foreign "browser:lambda:(x,v)=>{x.m31 = v}"
  prim__setM31 : DOMMatrixInit -> UndefOr Double -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.m32"
  prim__m32 : DOMMatrixInit -> PrimIO (UndefOr Double)

  export
  %foreign "browser:lambda:(x,v)=>{x.m32 = v}"
  prim__setM32 : DOMMatrixInit -> UndefOr Double -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.m33"
  prim__m33 : DOMMatrixInit -> PrimIO (UndefOr Double)

  export
  %foreign "browser:lambda:(x,v)=>{x.m33 = v}"
  prim__setM33 : DOMMatrixInit -> UndefOr Double -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.m34"
  prim__m34 : DOMMatrixInit -> PrimIO (UndefOr Double)

  export
  %foreign "browser:lambda:(x,v)=>{x.m34 = v}"
  prim__setM34 : DOMMatrixInit -> UndefOr Double -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.m43"
  prim__m43 : DOMMatrixInit -> PrimIO (UndefOr Double)

  export
  %foreign "browser:lambda:(x,v)=>{x.m43 = v}"
  prim__setM43 : DOMMatrixInit -> UndefOr Double -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.m44"
  prim__m44 : DOMMatrixInit -> PrimIO (UndefOr Double)

  export
  %foreign "browser:lambda:(x,v)=>{x.m44 = v}"
  prim__setM44 : DOMMatrixInit -> UndefOr Double -> PrimIO ()

namespace DOMPointInit

  export
  %foreign "browser:lambda:(a,b,c,d)=> {x: a,y: b,z: c,w: d}"
  prim__new :  UndefOr Double
            -> UndefOr Double
            -> UndefOr Double
            -> UndefOr Double
            -> PrimIO DOMPointInit

  export
  %foreign "browser:lambda:x=>x.w"
  prim__w : DOMPointInit -> PrimIO (UndefOr Double)

  export
  %foreign "browser:lambda:(x,v)=>{x.w = v}"
  prim__setW : DOMPointInit -> UndefOr Double -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.x"
  prim__x : DOMPointInit -> PrimIO (UndefOr Double)

  export
  %foreign "browser:lambda:(x,v)=>{x.x = v}"
  prim__setX : DOMPointInit -> UndefOr Double -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.y"
  prim__y : DOMPointInit -> PrimIO (UndefOr Double)

  export
  %foreign "browser:lambda:(x,v)=>{x.y = v}"
  prim__setY : DOMPointInit -> UndefOr Double -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.z"
  prim__z : DOMPointInit -> PrimIO (UndefOr Double)

  export
  %foreign "browser:lambda:(x,v)=>{x.z = v}"
  prim__setZ : DOMPointInit -> UndefOr Double -> PrimIO ()

namespace DOMQuadInit

  export
  %foreign "browser:lambda:(a,b,c,d)=> {p1: a,p2: b,p3: c,p4: d}"
  prim__new :  UndefOr DOMPointInit
            -> UndefOr DOMPointInit
            -> UndefOr DOMPointInit
            -> UndefOr DOMPointInit
            -> PrimIO DOMQuadInit

  export
  %foreign "browser:lambda:x=>x.p1"
  prim__p1 : DOMQuadInit -> PrimIO (UndefOr DOMPointInit)

  export
  %foreign "browser:lambda:(x,v)=>{x.p1 = v}"
  prim__setP1 : DOMQuadInit -> UndefOr DOMPointInit -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.p2"
  prim__p2 : DOMQuadInit -> PrimIO (UndefOr DOMPointInit)

  export
  %foreign "browser:lambda:(x,v)=>{x.p2 = v}"
  prim__setP2 : DOMQuadInit -> UndefOr DOMPointInit -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.p3"
  prim__p3 : DOMQuadInit -> PrimIO (UndefOr DOMPointInit)

  export
  %foreign "browser:lambda:(x,v)=>{x.p3 = v}"
  prim__setP3 : DOMQuadInit -> UndefOr DOMPointInit -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.p4"
  prim__p4 : DOMQuadInit -> PrimIO (UndefOr DOMPointInit)

  export
  %foreign "browser:lambda:(x,v)=>{x.p4 = v}"
  prim__setP4 : DOMQuadInit -> UndefOr DOMPointInit -> PrimIO ()

namespace DOMRectInit

  export
  %foreign "browser:lambda:(a,b,c,d)=> {x: a,y: b,width: c,height: d}"
  prim__new :  UndefOr Double
            -> UndefOr Double
            -> UndefOr Double
            -> UndefOr Double
            -> PrimIO DOMRectInit

  export
  %foreign "browser:lambda:x=>x.height"
  prim__height : DOMRectInit -> PrimIO (UndefOr Double)

  export
  %foreign "browser:lambda:(x,v)=>{x.height = v}"
  prim__setHeight : DOMRectInit -> UndefOr Double -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.width"
  prim__width : DOMRectInit -> PrimIO (UndefOr Double)

  export
  %foreign "browser:lambda:(x,v)=>{x.width = v}"
  prim__setWidth : DOMRectInit -> UndefOr Double -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.x"
  prim__x : DOMRectInit -> PrimIO (UndefOr Double)

  export
  %foreign "browser:lambda:(x,v)=>{x.x = v}"
  prim__setX : DOMRectInit -> UndefOr Double -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.y"
  prim__y : DOMRectInit -> PrimIO (UndefOr Double)

  export
  %foreign "browser:lambda:(x,v)=>{x.y = v}"
  prim__setY : DOMRectInit -> UndefOr Double -> PrimIO ()


text:
import Data.So

data Tree : (a: Type) -> Type where
  Leaf  : Tree a
  Node  : (key: a) -> (left: Tree a) -> (right: Tree a) -> Tree a

minVal : Ord a => Tree a -> Maybe a
minVal Leaf                      = Nothing
minVal (Node key Leaf _)         = Just key
minVal (Node key left right)     = minVal left

maxVal : Ord a => Tree a -> Maybe a
maxVal Leaf                      = Nothing
maxVal (Node key _ Leaf)         = Just key
maxVal (Node left key right)     = maxVal right

data Comp = LT | EQ | GT

lessTree : Ord a => a -> Tree a -> Bool
lessTree x node = case minVal node of
                   Nothing => True
                   Just key  => x < key

moreTree : Ord a => a -> Tree a -> Bool
moreTree x node = case maxVal node of
                   Nothing => True
                   Just key  => x >= key

comp : Ord a => a -> a -> Comp
comp x y = if x > y then GT else if x < y then LT else EQ

IsLft : Ord a => (x: a) -> (left: Tree a) -> Type
IsLft x left = So (moreTree x left)

IsRgt : Ord a => (x: a) -> (right: Tree a) -> Type
IsRgt x right = So (lessTree x right)

mkIsLft : Ord a => (x: a) -> (l: Tree a) -> (IsLft x l)
mkIsLft x l =
  case (choose (moreTree x l)) of
       Left proofYes => proofYes

mkIsRgt : Ord a => (x: a) -> (r: Tree a) -> (IsRgt x r)
mkIsRgt x r =
  case (choose (lessTree x r)) of
       Left proofYes => proofYes

data IsBST : (t : Tree a) -> Type where
  IsBSTLeaf : IsBST Leaf
  IsBSTNode : Ord a => (x: a) -> (IsBST left) -> (IsLft x left) -> (IsBST right) -> (IsRgt x right) -> (IsBST (Node x left right))

BSTree : Type -> Type
BSTree a = (t' : (Tree a) ** (IsBST t'))

insert : Ord a => (x : a) -> BSTree a -> BSTree a
insert x (Leaf ** IsBSTLeaf) =
  let isLftPrf = mkIsLft x Leaf
      isRgtPrf = mkIsRgt x Leaf
  in  ((Node x Leaf Leaf) ** (IsBSTNode x IsBSTLeaf isLftPrf IsBSTLeaf isRgtPrf))
insert x ((Node y left right) ** (IsBSTNode y lPrf isLftPrf rPrf isRgtPrf)) =
  case comp y x of
       GT =>
       let (lTree ** pl) = insert x (left ** lPrf)
           isLft         = mkIsLft y lTree
       in  ((Node y lTree right) ** (IsBSTNode y pl isLft rPrf isRgtPrf))
       LT =>
       let (rTree ** pr) = insert x (right ** rPrf)
           isRgt         = mkIsRgt y rTree
       in  ((Node y left rTree) ** (IsBSTNode y lPrf isLftPrf pr isRgt))
       EQ => ((Node y left right) ** (IsBSTNode y lPrf isLftPrf rPrf isRgtPrf))

-- wrongInsert : Ord a => (x : a) -> BSTree a -> BSTree a
-- wrongInsert x (Leaf ** IsBSTLeaf)  =
--   let isLftPrf = mkIsLft x Leaf
--       isRgtPrf = mkIsRgt x Leaf
--   in  ((Node x Leaf Leaf) ** (IsBSTNode x IsBSTLeaf isLftPrf IsBSTLeaf isRgtPrf))
-- wrongInsert x ((Node y left right) ** (IsBSTNode y lPrf isLftPrf rPrf isRgtPrf)) =
--   case comp y x of
--        GT =>
--        let (lTree ** pl) = insert x (left ** lPrf)
--            isLft         = mkIsLft y lTree
--        in  ((Node y right lTree) ** (IsBSTNode y rPrf isRgtPrf pl isLft))
--        LT =>
--        let (rTree ** pr) = insert x (right ** rPrf)
--            isRgt         = mkIsRgt y rTree
--        in  ((Node y left rTree) ** (IsBSTNode y lPrf isLftPrf pr isRgt))
--        EQ => ((Node y left right) ** (IsBSTNode y lPrf isLftPrf rPrf isRgtPrf))

max_stars_repo_name: LucasTornai/pgc-ufabc

max_issues_repo_name: LucasTornai/pgc-ufabc

max_forks_repo_name: LucasTornai/pgc-ufabc


text:
module Test.Hamming

import Data.Vect
import Test.Assertions
import System

import Hamming

collect : {default 0 acc : Nat} -> (List (IO Bool)) -> IO Nat
collect {acc} []               = pure acc
collect {acc} (test :: tests) = do
    bool <- test
    case bool of
        True  => collect {acc=acc}   tests
        False => collect {acc=S acc} tests

export
runTests : IO ()
runTests = do
    let empty = the (Vect _ Nucleotide) []
    count <- collect
        [ assertEquals (hamming_distance [A] [A]) 0
        , assertEquals (hamming_distance [G,G,A,C,T,G,A] [G,G,A,C,T,G,A]) 0
        , assertEquals (hamming_distance [A] [G]) 1
        , assertEquals (hamming_distance [A,G] [C,T]) 2
        , assertEquals (hamming_distance [A,T] [C,T]) 1
        , assertEquals (hamming_distance [G,G,A,C,G] [G,G,T,C,G]) 1
        , assertEquals (hamming_distance [A,C,C,A,G,G,G] [A,C,T,A,T,G,G]) 2
        , assertEquals (hamming_distance [A,G,A] [A,G,G]) 1
        , assertEquals (hamming_distance [A,G,G] [A,G,A]) 1
        , assertEquals (hamming_distance [T,A,G] [G,A,T]) 2
        , assertEquals (hamming_distance [G,A,T,A,C,A] [G,C,A,T,A,A]) 4
        , assertEquals (hamming_distance [G,G,A,C,G,G,A,T,T,C,T,G] [A,G,G,A,C,G,G,A,T,T,C,T]) 9
        , assertEquals (hamming_distance empty empty) 0
        , assertEquals version "1.0.0"
        ]
    case count of
        Z => exitSuccess
        _ => exitFailure


text:
import Data.Vect

{-
data Range : (begin : Nat) -> (end : Nat) -> Type where
  EmptyRange : Range 0 0
  MkRange : (begin : Nat) -> (end: Nat) -> Range begin end

interface Encoding a where
  alphabet : Range n m
  digit : Range n m

Encoding ASCII where
  alphabet = MkRange 64 116
  digit = MkRange 48 60

Cast ASCII Char where
  cast (MkASCII n) = chr (cast n)
-}

data ASCII : Type where
  MkASCII : ASCII

data Unicode : Type where
  MkUnicode : Unicode

interface Encoding a where
  alphabet : a -> (Nat, Nat)
  upper : a -> (Nat, Nat)
  digits : a -> (Nat, Nat)

Encoding ASCII where
  alphabet MkASCII = (64, 116)
  upper MkASCII = (64, 66)
  digits MkASCII = (0, 9)

Encoding Unicode where
  alphabet MkUnicode = (0, 52)
  upper MkUnicode = (64, 66)
  digits MkUnicode = (100, 109)

inRangeProof : (Nat, Nat) -> Nat -> Type
inRangeProof (min, max) n = case (min <= n) && (n <= max) of
                                 True => Elem True [True]
                                 False => Elem False [True]

data Character : e -> Nat -> Type where
  Digit  : Encoding e =>
           (e' : e) ->
           (n : Nat) ->
           { auto inRange : inRangeProof (digits e') n } ->
           Character e' n

  Upper : Encoding e =>
          (e' : e) ->
          (n : Nat) ->
          { auto inRange : inRangeProof (upper e') n } ->
          Character e' n

  Letter  : Encoding e =>
            (e' : e) ->
            (n : Nat) ->
            { auto inRange : inRangeProof (alphabet e') n } ->
            Character e' n

isDigit : Character e n -> Nat
isDigit (Digit e n) = 0
isDigit (Upper e n) = 1
isDigit (Letter e n) = 2

max_stars_repo_name: ostera/asdf

max_issues_repo_name: ostera/asdf

max_forks_repo_name: ostera/asdf


text:
module Minecraft.Base.PreClassic.Void

import public Minecraft.Core.Univ.Level.Gen
import public Minecraft.Base.PreClassic

%default total

public export %hint
voidGen : (seed : Bits64) => LevelGen seed preClassic (new Air.Block MkBlock)
voidGen @{seed} = MkLevelGen blockAt where
  blockAt : Pos -> As Block
  blockAt (At 31 60 31 {chunk = 9223372036854775807}) = new Cobblestone.Block MkBlock
  blockAt (At x  60 z  {chunk = 9223372036854775807}) =
    if x <= 47 && x >= 15 && z <= 47 && z >= 15
      then new Stone.Block MkBlock
      else new Air.Block MkBlock
  blockAt _ = new Air.Block MkBlock

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


text:
> module PNat.Operations

> import PNat.PNat
> import Nat.Positive
> import Nat.Operations
> import Nat.OperationsProperties
> import Pairs.Operations

> %default total
> %access public export

> ||| The predecessor of a PNat
> pred : PNat -> Nat
> pred (Element _ (MkPositive {n})) = n

> |||
> fromNat : (m : Nat) -> Z `LT` m -> PNat
> {-
> fromNat  Z zLTz = absurd zLTz
> fromNat (S m) _ = Element (S m) (MkPositive {n = m})
> ----}
> --{-
> fromNat m prf = Element m pm where
>   pm : Positive m
>   pm = fromSucc (pred m prf) m (predLemma m prf)
> ---}

> |||
> toNat : PNat -> Nat
> toNat = getWitness

> |||
> plus : PNat -> PNat -> PNat
> plus (Element m pm) (Element n pn) = Element (m + n) (plusPreservesPositivity pm pn)

> |||
> (+) : PNat -> PNat -> PNat
> (+) = plus

> |||
> mult : PNat -> PNat -> PNat
> mult (Element m pm) (Element n pn) = Element (m * n) (multPreservesPositivity pm pn)

> |||
> (*) : PNat -> PNat -> PNat
> (*) = mult

> {-

> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Main

import System

readNum : IO (Maybe Nat)
readNum = do
  input <- getLine
  let output =  if all isDigit (unpack input)
    then (Just (cast input))
    else Nothing
  pure output

takeGuess : (target : Nat) -> IO (Maybe Ordering)
takeGuess target = do
  Just g <- readNum
    | Nothing => pure Nothing
  pure (Just (compare g target))

guess : (target : Nat) -> (guesses : Nat) -> IO ()
guess target guesses = do
  putStr ((show guesses) ++ ": Guess? ")
  result <- takeGuess target
  case result of
    Just EQ => putStrLn "Got it!"
    Nothing => putStrLn "Invalid Number" >>= \_ => guess target (S guesses)
    Just LT => putStrLn "Too Low" >>= \_ => guess target (S guesses)
    Just GT => putStrLn "Too High" >>= \_ => guess target (S guesses)

main : IO ()
main = do
  t <- time
  let target = mod t 100
  guess (cast target) Z

max_stars_repo_name: tekerson/type-driven-development

max_issues_repo_name: tekerson/type-driven-development

max_forks_repo_name: tekerson/type-driven-development


text:
module Idris.Pretty.Render

import Core.Context
import Core.Core

import Idris.REPL.Opts

import Libraries.Control.ANSI.SGR
import Libraries.Text.PrettyPrint.Prettyprinter
import public Libraries.Text.PrettyPrint.Prettyprinter.Render.Terminal
import Libraries.Utils.Term

import System

%default total

getPageWidth : {auto o : Ref ROpts REPLOpts} -> Core PageWidth
getPageWidth = do
  consoleWidth <- getConsoleWidth
  case consoleWidth of
    Nothing => do
      cols <- coreLift getTermCols
      pure $ if cols == 0 then Unbounded else AvailablePerLine cols 1
    Just 0 => pure $ Unbounded
    Just cw => pure $ AvailablePerLine (cast cw) 1

export
render : {auto o : Ref ROpts REPLOpts} ->
         (ann -> AnsiStyle) ->
         Doc ann -> Core String
render stylerAnn doc = do
  color <- getColor
  isDumb <- (Just "dumb" ==) <$> coreLift (getEnv "TERM")
  -- ^-- emacs sets the TERM variable to `dumb` and expects the compiler
  --     to not emit any ANSI escape codes
  pageWidth <- getPageWidth
  let opts = MkLayoutOptions pageWidth
  let layout = layoutPretty opts doc
  pure $ renderString $
    if color && not isDumb
      then reAnnotateS stylerAnn layout
      else unAnnotateS layout

export
renderWithoutColor : {auto o : Ref ROpts REPLOpts} -> Doc ann -> Core String
renderWithoutColor doc = do
  pageWidth <- getPageWidth
  let opts = MkLayoutOptions pageWidth
  let layout = layoutPretty opts doc
  pure $ renderString $ unAnnotateS layout

export
renderWithSpans : {auto o : Ref ROpts REPLOpts} ->
  Doc ann ->
  Core (String, List (Span ann))
renderWithSpans doc = do
  pageWidth <- getPageWidth
  let opts = MkLayoutOptions pageWidth
  let layout = layoutPretty opts doc
  pure $ displaySpans layout


text:
module Main

import Control.App
import Control.App.Console

{-
  App is defined as:

  data App: {default MayThrow l : Path} -> (es : List Error) -> Type -> Type

  where `Error` is a synonym for `Type`.
-}

hello : Console es => App es ()
hello = putStrLn "Hello, world"

main : IO ()
main = run hello

max_stars_repo_name: timmyjose-study/idris-from-the-docs

max_issues_repo_name: timmyjose-study/idris-from-the-docs

max_forks_repo_name: timmyjose-study/idris-from-the-docs


text:
module Functions

intFunction : Int
intFunction = 1887

stringFunction : String
stringFunction = "A study in Scarlet"

max_stars_repo_name: kkirstein/proglang-playground

max_issues_repo_name: kkirstein/proglang-playground

max_forks_repo_name: kkirstein/proglang-playground


text:
module Libraries.Data.IOMatrix

import Data.IOArray.Prims

%default total

export
record IOMatrix a where
  constructor MkIOMatrix
  maxWidth  : Int
  maxHeight : Int
  content   : ArrayData (Maybe a)

export
width : IOMatrix a -> Int
width = maxWidth

export
height : IOMatrix a -> Int
height = maxHeight

export
new : HasIO io => (width, height : Int) -> io (IOMatrix a)
new width height
  = pure $ MkIOMatrix width height
         !(primIO (prim__newArray (width * height) Nothing))

toPosition : IOMatrix a -> Int -> Int -> Maybe Int
toPosition (MkIOMatrix w h arr) i j
  = do guard (not (i < 0 || j < 0 || i >= w || j >= h))
       pure (i * h + j)

export
write : HasIO io => IOMatrix a -> Int -> Int -> a -> io Bool
write mat i j el = case toPosition mat i j of
  Nothing => pure False
  Just pos => True <$ primIO (prim__arraySet (content mat) pos (Just el))

export
read : HasIO io => IOMatrix a -> Int -> Int -> io (Maybe a)
read mat i j = case toPosition mat i j of
  Nothing => pure Nothing
  Just pos => primIO (prim__arrayGet (content mat) pos)


text:
data Success a = MkSuccess a
data Error a = MkError a
data Profile a = MkProfile a

record State where
  constructor MkState
  id : Nat

Traveling can suck.
Clients may be too set in their ways.
Sometimes it's hard to have a life.

Nothing too bad, but they did get nervous.

University Program is good.

Culture dillution?