text:
||| Here we present an example not found in the paper.
|||
||| We define an *Edge Bounded Graph* as a graph whose nodes are bounded on the number of edges they can contain.
||| Here we differentiate between bounds for roots, leaf, and other nodes.
|||
||| We define a handler to generate a simple adjacency graph representation from our graph language description.
module Examples.EdgeBoundedGraph

import Data.List

import Resources

%access public export
%default total

namespace TypeLevel

  ||| The different node types.
  data Ty = LEAF | ROOT | NODE

  namespace State
    ||| Leaf nodes can accept a certain number of connections.
    record LeafState where
      constructor MkLeafState
      max_incoming : Nat
      incoming : Nat

    ||| Root nodes can make a certain number of connections.
    record RootState where
      constructor MkRootState
      max_outgoing : Nat
      outgoing : Nat

    ||| Nodes that can make, and accept, a certain number of connections.
    record NodeState where
      constructor MkNodeState
      max_incoming : Nat
      max_outgoing : Nat
      incoming : Nat
      outgoing : Nat

    ||| Map variable types to concrete abstract states.
    CalcStateType : Ty -> Type
    CalcStateType LEAF = LeafState
    CalcStateType ROOT = RootState
    CalcStateType NODE = NodeState

namespace Predicates
    data DIRECTION = O | I

    ||| Can a node be connected.
    data CanConnect : DIRECTION
                   -> Var Ty ty
                   -> StateItem Ty CalcStateType ty
                   -> Type
      where
        CanNodeIn  : CanConnect I lbl (MkStateItem NODE lbl (MkNodeState a b (S n) x))
        CanNodeOut : CanConnect O lbl (MkStateItem NODE lbl (MkNodeState a b x     (S n)))
        CanRootOut : CanConnect O lbl (MkStateItem ROOT lbl (MkRootState a (S n)))
        CanLeafIn  : CanConnect I lbl (MkStateItem LEAF lbl (MkLeafState a (S n)))

    ||| Has the node be used completely.
    data Used : StateItem Ty CalcStateType ty -> Type where
       IsNodeUsed : Used (MkStateItem NODE lbl (MkNodeState a b Z Z))
       IsRootUsed : Used (MkStateItem ROOT lbl (MkRootState a Z))
       IsLeafUsed : Used (MkStateItem LEAF lbl (MkLeafState a Z))

    ||| Has the node been used partially.
    data UsedS : StateItem Ty CalcStateType ty -> Type where
      -- All used.
      AllUsedL : UsedS (MkStateItem LEAF lbl (MkLeafState a Z))
      AllUsedR : UsedS (MkStateItem ROOT lbl (MkRootState a Z))
      AllUsedN : UsedS (MkStateItem NODE lbl (MkNodeState a b Z Z))

      -- All incoming ports are used.
      IUsedNode : UsedS (MkStateItem NODE lbl (MkNodeState a b Z x))
      IUsedLeaf : UsedS (MkStateItem LEAF lbl (MkLeafState a Z))

      -- All outgoing ports are used.
      OUsedNode : UsedS (MkStateItem NODE lbl (MkNodeState a b x Z))
      OUsedRoot : UsedS (MkStateItem ROOT lbl (MkRootState a Z))

      ||| Some ports
      SomeNodes : LTE x a
               -> LTE y b
               -> UsedS (MkStateItem NODE lbl (MkNodeState a b x y))

      SomeRoot : LTE x a
              -> UsedS (MkStateItem ROOT lbl (MkRootState a x))

      SomeLeaf : LTE x a
              -> UsedS (MkStateItem LEAF lbl (MkLeafState a x))

namespace Update

  ||| The type-level function to update a node's usage count.
  Use : (d      : DIRECTION)
     -> (item   : StateItem Ty CalcStateType ty)
     -> (bewijs : CanConnect d lbl item)
     -> StateItem Ty CalcStateType ty
  Use I (MkStateItem NODE lbl (MkNodeState a b (S n) x)) CanNodeIn {ty = NODE} =
    MkStateItem NODE lbl (MkNodeState a b n x)
  Use O (MkStateItem NODE lbl (MkNodeState a b x (S n))) CanNodeOut {ty = NODE} =
    MkStateItem NODE lbl (MkNodeState a b x n)
  Use O (MkStateItem ROOT lbl (MkRootState a (S n))) CanRootOut {ty = ROOT} =
    MkStateItem ROOT lbl (MkRootState a n)
  Use I (MkStateItem LEAF lbl (MkLeafState a (S n))) CanLeafIn {ty = LEAF} =
    MkStateItem LEAF lbl (MkLeafState a n)

namespace Declaration

{- [ Language Definition ] -}

    data GraphLang : Lang Ty CalcStateType where
      ||| Create a node that can accept `i` connections, and make `o` connections.
      Node : (i,o : Nat) -> GraphLang (Var Ty NODE) old (\lbl => MkStateItem NODE lbl (MkNodeState i o i o) :: old)
      ||| Create a new root node that can make `o` connections.
      Root : (o   : Nat) -> GraphLang (Var Ty ROOT) old (\lbl => MkStateItem ROOT lbl (MkRootState o o)     :: old)
      ||| Create a new leaf node that can accept `i` connections.
      Leaf : (i   : Nat) -> GraphLang (Var Ty LEAF) old (\lbl => MkStateItem LEAF lbl (MkLeafState i i)     :: old)

      ||| Connect two nodes together if they each have space to allow an edge.
      Stop : GraphLang () old (const Nil)

      ||| Connect two nodes together if they each have space to allow an edge.
      Connect : (a : Var Ty tyO)
             -> (b : Var Ty tyI)

             -> (prfO : InContext tyO (CanConnect O a) old)
             -> (prfI : InContext tyI (CanConnect I b) (update old prfO (Use O)))
             -> GraphLang () old (const $ update (update old prfO (Use O)) prfI (Use I))

{- [ NOTE ]

A high-level API to embedd language expressions within `LangM`, and calculate language proofs.

-}
    ||| The definition of an edge bounded graph.
    MYGRAPH : LANG Ty CalcStateType
    MYGRAPH = MkLang Ty CalcStateType GraphLang

    ||| Create a node that can accept `i` connections, and make `o` connections.
    node : (i,o : Nat)
        -> LangM m (Var Ty NODE) MYGRAPH old (\lbl => (MkStateItem NODE lbl (MkNodeState i o i o)) :: old)
    node i o = Expr $ Node i o

    ||| Create a new root node that can make `o` connections.
    root : (o   : Nat)
        -> LangM m (Var Ty ROOT) MYGRAPH old (\lbl => MkStateItem ROOT lbl (MkRootState o o)     :: old)
    root o = Expr $ Root o

    ||| Create a new leaf node that can accept `i` connections.
    leaf : (i   : Nat)
        -> LangM m (Var Ty LEAF) MYGRAPH old (\lbl => MkStateItem LEAF lbl (MkLeafState i i)     :: old)
    leaf i = Expr $ Leaf i

    ||| Declare the end of tthe specification.
    stop : LangM m () MYGRAPH old (const Nil)
    stop = Expr Stop

    ||| Connect two nodes together if they each have space to allow an edge.
    connect : (a : Var Ty tyO)
           -> (b : Var Ty tyI)

           -> {auto prfO : InContext tyO (CanConnect O a) old}
           -> {auto prfI : InContext tyI (CanConnect I b) (update old prfO (Use O))}
           -> LangM m () MYGRAPH old (const $ update (update old prfO (Use O)) prfI (Use I))
    connect a b {prfO} {prfI} = Expr $ Connect a b prfO prfI

    ||| A simple graph representation.
    record Graph where
      constructor MkGraph
      nodes : List Nat
      edges : List (Nat, Nat)

||| Nodes are *just* Natural numbers
RealVar Ty where
  CalcRealType _ = Nat

||| A pure evaluation context to generate the graph instance.
|||
||| **note** the accumulator is one that contains the node counter,
||| and the graph being constructed.
Handler Ty CalcStateType GraphLang (Nat, Graph) Basics.id where
  handle env Stop (c,g) cont = cont () Nil (c,g)
  handle env (Node i o) (c,g) cont =
    cont MkVar (MkTag c::env) (S c, record {nodes $= (c::)} g)
  handle env (Root o) (c,g) cont =
    cont MkVar (MkTag c::env) (S c, record {nodes $= (c::)} g)
  handle env (Leaf i) (c,g) cont =
    cont MkVar (MkTag c::env) (S c, record {nodes $= (c::)} g)
  handle env (Connect a b prfO prfI) (c,g) cont =
    let (MkTag l) = lookup env prfO in
    let env' = update env prfO (Use O) in
    let (MkTag r) = lookup env' prfI in
    let env'' = update env' prfI (Use I) in
      cont () env'' (c,record {edges $= ((l,r)::)} g)

||| An example program that is closed.
example : LangM m () MYGRAPH Nil (const Nil)
example = do
  a <- node 2 5
  b <- root 1
  c <- root 3

  d <- root 5
  connect c a
  connect b a
  stop

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

max_stars_repo_name: border-patrol/resources

max_issues_repo_name: border-patrol/resources

max_forks_repo_name: border-patrol/resources


text:
module IdrisJvm.Core.JAsm

import IdrisJvm.IO
import IdrisJvm.Core.Asm
import Java.Util
import Java.Lang
import Data.SortedMap

%access public export

Assembler : Type
Assembler = javaClass "IdrisJvm/Core/Assembler"

JAnnotation : Type
JAnnotation = javaClass "IdrisJvm/Core/Annotation"

JAnnString : Type
JAnnString = javaClass "IdrisJvm/Core/AnnotationValue$AnnString"

JAnnEnum : Type
JAnnEnum = javaClass "IdrisJvm/Core/AnnotationValue$AnnEnum"

JAnnInt : Type
JAnnInt = javaClass "IdrisJvm/Core/AnnotationValue$AnnInt"

JAnnBoolean : Type
JAnnBoolean = javaClass "IdrisJvm/Core/AnnotationValue$AnnBoolean"

JAnnByte : Type
JAnnByte = javaClass "IdrisJvm/Core/AnnotationValue$AnnByte"

JAnnChar : Type
JAnnChar = javaClass "IdrisJvm/Core/AnnotationValue$AnnChar"

JAnnShort : Type
JAnnShort = javaClass "IdrisJvm/Core/AnnotationValue$AnnShort"

JAnnLong : Type
JAnnLong = javaClass "IdrisJvm/Core/AnnotationValue$AnnLong"

JAnnFloat : Type
JAnnFloat = javaClass "IdrisJvm/Core/AnnotationValue$AnnFloat"

JAnnDouble : Type
JAnnDouble = javaClass "IdrisJvm/Core/AnnotationValue$AnnDouble"

JAnnClass : Type
JAnnClass = javaClass "IdrisJvm/Core/AnnotationValue$AnnClass"

JAnnArray : Type
JAnnArray = javaClass "IdrisJvm/Core/AnnotationValue$AnnArray"

JAnnAnnotation : Type
JAnnAnnotation = javaClass "IdrisJvm/Core/AnnotationValue$AnnAnnotation"

JAnnotationProperty : Type
JAnnotationProperty = javaClass "IdrisJvm/Core/AnnotationProperty"

JAnnotationValue: Type
JAnnotationValue = javaClass "IdrisJvm/Core/AnnotationValue"

Inherits JAnnotationValue JAnnInt where {}
Inherits JAnnotationValue JAnnBoolean where {}
Inherits JAnnotationValue JAnnByte where {}
Inherits JAnnotationValue JAnnChar where {}
Inherits JAnnotationValue JAnnShort where {}
Inherits JAnnotationValue JAnnLong where {}
Inherits JAnnotationValue JAnnFloat where {}
Inherits JAnnotationValue JAnnDouble where {}
Inherits JAnnotationValue JAnnEnum where {}
Inherits JAnnotationValue JAnnClass where {}
Inherits JAnnotationValue JAnnAnnotation where {}

JHandle: Type
JHandle = javaClass "IdrisJvm/Core/JHandle"

JBsmArg: Type
JBsmArg = javaClass "IdrisJvm/Core/JBsmArg"

JBsmArgGetType: Type
JBsmArgGetType = javaClass "IdrisJvm/Core/JBsmArg$JBsmArgGetType"

JBsmArgHandle: Type
JBsmArgHandle = javaClass "IdrisJvm/Core/JBsmArg$JBsmArgHandle"

toJClassOpts : ClassOpts -> Int
toJClassOpts ComputeMaxs = 1
toJClassOpts ComputeFrames = 2

mutual
    toJAnnotationValue : Asm.AnnotationValue -> JVM_IO JAnnotationValue
    toJAnnotationValue (AnnString s) = believe_me <$> FFI.new (String -> JVM_IO JAnnString) s
    toJAnnotationValue (AnnEnum enum s) = believe_me <$> FFI.new (String -> String -> JVM_IO JAnnEnum) enum s
    toJAnnotationValue (AnnInt n) = believe_me <$> FFI.new (Int -> JVM_IO JAnnInt) n
    toJAnnotationValue (AnnBoolean n) = believe_me <$> FFI.new (Bool -> JVM_IO JAnnBoolean) n
    toJAnnotationValue (AnnByte n) = believe_me <$> FFI.new (Bits8 -> JVM_IO JAnnByte) n
    toJAnnotationValue (AnnChar n) = believe_me <$> FFI.new (Char -> JVM_IO JAnnChar) n
    toJAnnotationValue (AnnShort n) = believe_me <$> FFI.new (Bits16 -> JVM_IO JAnnShort) n
    toJAnnotationValue (AnnLong n) = believe_me <$> FFI.new (Bits64 -> JVM_IO JAnnLong) n
    toJAnnotationValue (AnnFloat n) = believe_me <$> FFI.new (Double -> JVM_IO JAnnFloat) n
    toJAnnotationValue (AnnDouble n) = believe_me <$> FFI.new (Double -> JVM_IO JAnnDouble) n
    toJAnnotationValue (AnnClass n) = believe_me <$> FFI.new (String -> JVM_IO JAnnClass) n
    toJAnnotationValue (AnnAnnotation n) = do
        jAnn <- toJAnnotation n
        FFI.new (JAnnotation -> JVM_IO JAnnAnnotation) jAnn
    toJAnnotationValue (AnnArray values) = do
      jvalues <- ArrayList.fromList !(sequence $ toJAnnotationValue <$> values)
      believe_me <$> FFI.new (JList -> JVM_IO JAnnArray) (believe_me jvalues)

    toJAnnotationProperty : Asm.AnnotationProperty -> JVM_IO JAnnotationProperty
    toJAnnotationProperty (name, annValue) = do
      jAnnotationValue <- toJAnnotationValue annValue
      FFI.new (String -> JAnnotationValue -> JVM_IO JAnnotationProperty) name jAnnotationValue

    toJAnnotation : Asm.Annotation -> JVM_IO JAnnotation
    toJAnnotation (MkAnnotation name props) = do
      jprops <- ArrayList.fromList !(sequence $ toJAnnotationProperty <$> props)
      FFI.new (String -> JList -> JVM_IO JAnnotation) name (believe_me jprops)

toJFieldInitialValue : FieldInitialValue -> Object
toJFieldInitialValue (IntField n) = believe_me $ JInteger.valueOf n
toJFieldInitialValue (StringField s) = believe_me s
toJFieldInitialValue (DoubleField d) = believe_me $ JDouble.valueOf d

accessNum : Access -> Int
accessNum Final     = 16
accessNum Private   = 2
accessNum Public    = 1
accessNum Static    = 8
accessNum Synthetic = 4096

fieldInsTypeNum : FieldInsType -> Int
fieldInsTypeNum FGetStatic = 178
fieldInsTypeNum FPutStatic = 179
fieldInsTypeNum FGetField  = 180
fieldInsTypeNum FPutField  = 181

frameTypeNum : FrameType -> Int
frameTypeNum FFull   = 0
frameTypeNum FSame   = 3
frameTypeNum FAppend = 1

invocTypeNum : InvocType -> Int
invocTypeNum InvokeInterface = 185
invocTypeNum InvokeSpecial   = 183
invocTypeNum InvokeStatic    = 184
invocTypeNum InvokeVirtual   = 182

handleTagOpcode : HandleTag -> Int
handleTagOpcode HGetField         = 1
handleTagOpcode HGetStatic        = 2
handleTagOpcode HPutField         = 3
handleTagOpcode HPutStatic        = 4
handleTagOpcode HInvokeVirtual    = 5
handleTagOpcode HInvokeStatic     = 6
handleTagOpcode HInvokeSpecial    = 7
handleTagOpcode HNewInvokeSpecial = 8
handleTagOpcode HInvokeInterface  = 9

constantToObject : Constant -> Object
constantToObject (DoubleConst d) = believe_me $ JDouble.valueOf d
constantToObject (IntegerConst n) = believe_me $ JInteger.valueOf n
constantToObject (LongConst n) = believe_me $ Long.valueOf n
constantToObject (StringConst str) = believe_me str
constantToObject (TypeConst str) = believe_me str

toJHandle : Handle -> JVM_IO JHandle
toJHandle (MkHandle tag hcname hmname hdesc hIsIntf) = do
  let tagNum = handleTagOpcode tag
  FFI.new (Int -> String -> String -> String -> Bool -> JVM_IO JHandle) tagNum hcname hmname hdesc hIsIntf

toJbsmArg : BsmArg -> JVM_IO JBsmArg
toJbsmArg (BsmArgGetType desc) = believe_me <$> FFI.new (String -> JVM_IO JBsmArgGetType) desc
toJbsmArg (BsmArgHandle handle) = do
  jhandle <- toJHandle handle
  believe_me <$> FFI.new (JHandle -> JVM_IO JBsmArgHandle) jhandle

record AsmState where
  constructor MkAsmState
  subroutines : List (Asm ())
  functionTypes : SortedMap JMethodName InferredFunctionType
  functionLocTypes : InferredTypeStore
  functionRetType : InferredType

singleInst : AsmState -> JVM_IO a -> JVM_IO (a, AsmState)
singleInst state m = do
  a <- m
  pure (a, state)

runAsm : AsmState -> Assembler -> Asm a -> JVM_IO (a, AsmState)
runAsm state assembler Aaload = singleInst state $ invokeInstance "aaload" (Assembler -> JVM_IO ()) assembler

runAsm state assembler Aastore = singleInst state $ invokeInstance "aastore" (Assembler -> JVM_IO ()) assembler

runAsm state assembler Aconstnull = singleInst state $ invokeInstance "aconstnull" (Assembler -> JVM_IO ()) assembler

runAsm state assembler (Aload n) = singleInst state $ invokeInstance "aload" (Assembler -> Int -> JVM_IO ()) assembler n

runAsm state assembler (Anewarray desc) = singleInst state $ invokeInstance "anewarray" (Assembler -> String -> JVM_IO ()) assembler desc
runAsm state assembler Anewintarray     = singleInst state $ invokeInstance "anewintarray" (Assembler -> JVM_IO ()) assembler
runAsm state assembler Anewbooleanarray = singleInst state $ invokeInstance "anewbooleanarray" (Assembler -> JVM_IO ()) assembler
runAsm state assembler Anewbytearray    = singleInst state $ invokeInstance "anewbytearray" (Assembler -> JVM_IO ()) assembler
runAsm state assembler Anewchararray    = singleInst state $ invokeInstance "anewchararray" (Assembler -> JVM_IO ()) assembler
runAsm state assembler Anewshortarray   = singleInst state $ invokeInstance "anewshortarray" (Assembler -> JVM_IO ()) assembler
runAsm state assembler Anewlongarray    = singleInst state $ invokeInstance "anewlongarray" (Assembler -> JVM_IO ()) assembler
runAsm state assembler Anewfloatarray   = singleInst state $ invokeInstance "anewfloatarray" (Assembler -> JVM_IO ()) assembler
runAsm state assembler Anewdoublearray  = singleInst state $ invokeInstance "anewdoublearray" (Assembler -> JVM_IO ()) assembler
runAsm state assembler Arraylength      = singleInst state $ invokeInstance "arraylength" (Assembler -> JVM_IO ()) assembler
runAsm state assembler Areturn          = singleInst state $ invokeInstance "areturn" (Assembler -> JVM_IO ()) assembler
runAsm state assembler (Astore n)       = singleInst state $ invokeInstance "astore" (Assembler -> Int -> JVM_IO ()) assembler n
runAsm state assembler Baload           = singleInst state $ invokeInstance "baload" (Assembler -> JVM_IO ()) assembler
runAsm state assembler Bastore          = singleInst state $ invokeInstance "bastore" (Assembler -> JVM_IO ()) assembler
runAsm state assembler Caload           = singleInst state $ invokeInstance "caload" (Assembler -> JVM_IO ()) assembler
runAsm state assembler Castore          = singleInst state $ invokeInstance "castore" (Assembler -> JVM_IO ()) assembler
runAsm state assembler (Checkcast desc) = singleInst state $ invokeInstance "checkcast" (Assembler -> String -> JVM_IO ()) assembler desc
runAsm state assembler (ClassCodeStart version access className sig parent intf anns) = singleInst state $ do
  janns <- sequence $ toJAnnotation <$> anns
  interfaces <- ArrayList.fromList intf
  annotations <- ArrayList.fromList janns
  invokeInstance
    "classCodeStart"
    (Assembler -> Int -> Int -> ClassName -> Signature -> ClassName -> JList -> JList -> JVM_IO ())
    assembler
    version
    (accessNum access)
    className
    (maybeToNullableString sig)
    parent
    (believe_me interfaces)
    (believe_me annotations)

runAsm state assembler (ClassCodeEnd out) = singleInst state $ invokeInstance "classCodeEnd" (Assembler -> String -> JVM_IO ()) assembler out
runAsm state assembler (CreateClass opts) = singleInst state $ invokeInstance "createClass" (Assembler -> Int -> JVM_IO ()) assembler (toJClassOpts opts)
runAsm state assembler (CreateField accs className fieldName desc sig fieldInitialValue) = singleInst state $ do
  let jaccs = sum $ accessNum <$> accs
  invokeInstance
    "createField"
    (Assembler -> Int -> ClassName -> FieldName -> Descriptor -> Signature -> Object -> JVM_IO ())
    assembler
    jaccs
    className
    fieldName
    desc
    (maybeToNullableString sig)
    (maybeToNullable (toJFieldInitialValue <$> fieldInitialValue))

runAsm state assembler (CreateLabel label) = singleInst state $ do
  invokeInstance "createLabel" (Assembler -> String -> JVM_IO ()) assembler label
  pure label

runAsm state assembler (CreateMethod accs className methodName desc sig exceptions anns paramAnns) = singleInst state $ do
  let jaccs = sum $ accessNum <$> accs
  jexceptions <- sequence $ ArrayList.fromList <$> exceptions
  janns <- ArrayList.fromList !(sequence $ toJAnnotation <$> anns)
  jparamAnns <- ArrayList.fromList !(sequence $ (\paramAnn => ArrayList.fromList !(sequence $ toJAnnotation <$> paramAnn)) <$> paramAnns)
  invokeInstance
    "createMethod"
    (Assembler -> Int -> ClassName -> MethodName -> Descriptor -> Signature -> JList -> JList -> JList -> JVM_IO ())
    assembler
    jaccs
    className
    methodName
    desc
    (maybeToNullableString sig)
    (maybeToNullable $ believe_me jexceptions)
    (believe_me janns)
    (believe_me jparamAnns)

runAsm state assembler D2i = singleInst state $ invokeInstance "d2i" (Assembler -> JVM_IO ()) assembler
runAsm state assembler D2f = singleInst state $ invokeInstance "d2f" (Assembler -> JVM_IO ()) assembler
runAsm state assembler Dadd = singleInst state $ invokeInstance "dadd" (Assembler -> JVM_IO ()) assembler
runAsm state assembler (Dconst n) = singleInst state $ invokeInstance "dconst" (Assembler -> Double -> JVM_IO ()) assembler n
runAsm state assembler Daload = singleInst state $ invokeInstance "daload" (Assembler -> JVM_IO ()) assembler
runAsm state assembler Dastore = singleInst state $ invokeInstance "dastore" (Assembler -> JVM_IO ()) assembler
runAsm state assembler Ddiv = singleInst state $ invokeInstance "ddiv" (Assembler -> JVM_IO ()) assembler

runAsm state assembler (Debug msg) = singleInst state $ invokeInstance "debug" (Assembler -> String -> JVM_IO ()) assembler msg

runAsm state assembler (Dload n) = singleInst state $ invokeInstance "dload" (Assembler -> Int -> JVM_IO ()) assembler n
runAsm state assembler Dmul = singleInst state $ invokeInstance "dmul" (Assembler -> JVM_IO ()) assembler
runAsm state assembler Drem = singleInst state $ invokeInstance "drem" (Assembler -> JVM_IO ()) assembler
runAsm state assembler Dreturn = singleInst state $ invokeInstance "dreturn" (Assembler -> JVM_IO ()) assembler
runAsm state assembler (Dstore n) = singleInst state $ invokeInstance "dstore" (Assembler -> Int -> JVM_IO ()) assembler n
runAsm state assembler Dsub = singleInst state $ invokeInstance "dsub" (Assembler -> JVM_IO ()) assembler
runAsm state assembler Dup = singleInst state $ invokeInstance "dup" (Assembler -> JVM_IO ()) assembler
runAsm state assembler (Error err) = singleInst state $ invokeInstance "error" (Assembler -> String -> JVM_IO ()) assembler err
runAsm state assembler F2d = singleInst state $ invokeInstance "f2d" (Assembler -> JVM_IO ()) assembler
runAsm state assembler Faload = singleInst state $ invokeInstance "faload" (Assembler -> JVM_IO ()) assembler
runAsm state assembler Fastore = singleInst state $ invokeInstance "fastore" (Assembler -> JVM_IO ()) assembler
runAsm state assembler (Fconst n) = singleInst state $ invokeInstance "fconst" (Assembler -> Double -> JVM_IO ()) assembler n
runAsm state assembler (Field finsType cname fname desc) = singleInst state $ do
  let finsTypeNum = fieldInsTypeNum finsType
  invokeInstance
    "field"
    (Assembler -> Int -> ClassName -> FieldName -> Descriptor -> JVM_IO ())
    assembler
    finsTypeNum
    cname
    fname
    desc

runAsm state assembler FieldEnd = singleInst state $ invokeInstance "fieldEnd" (Assembler -> JVM_IO ()) assembler

runAsm state assembler (Fload n) = singleInst state $ invokeInstance "fload" (Assembler -> Int -> JVM_IO ()) assembler n

runAsm state assembler (Frame frameType nLocal localSigs nStack stackSigs) = singleInst state $ do
  let ftypeNum = frameTypeNum frameType
  jlocalSigs <- ArrayList.fromList localSigs
  jstackSigs <- ArrayList.fromList stackSigs
  invokeInstance
    "frame"
    (Assembler -> Int -> Int -> JList -> Int -> JList -> JVM_IO ())
    assembler
    ftypeNum
    (cast nLocal)
    (believe_me jlocalSigs)
    (cast nStack)
    (believe_me jstackSigs)

runAsm state assembler FreshIfIndex = singleInst state $ do
  index <- invokeInstance "freshIfIndex" (Assembler -> JVM_IO Int) assembler
  pure $ cast index

runAsm state assembler (FreshLambdaIndex cname) = singleInst state $ do
  index <- invokeInstance "freshLambdaIndex" (Assembler -> String -> JVM_IO Int) assembler cname
  pure $ cast index

runAsm state assembler FreshSwitchIndex = singleInst state $ do
  index <- invokeInstance "freshSwitchIndex" (Assembler -> JVM_IO Int) assembler
  pure $ cast index

runAsm state assembler Freturn = singleInst state $ invokeInstance "freturn" (Assembler -> JVM_IO ()) assembler
runAsm state assembler (Fstore n) = singleInst state $ invokeInstance "fstore" (Assembler -> Int -> JVM_IO ()) assembler n
runAsm state assembler GetFunctionName = singleInst state $ do
  cname <- invokeInstance "getClassName" (Assembler -> JVM_IO String) assembler
  mname <- invokeInstance "getMethodName" (Assembler -> JVM_IO String) assembler
  pure $ MkJMethodName cname mname

runAsm state assembler GetFunctionLocTypes = pure (functionLocTypes state, state)
runAsm state assembler GetFunctionRetType = pure (functionRetType state, state)
runAsm state assembler GetFunctionTypes = pure (functionTypes state, state)

runAsm state assembler GetLocalVarCount = singleInst state $ do
  index <- invokeInstance "getLocalVarCount" (Assembler -> JVM_IO Int) assembler
  pure $ cast index
runAsm state assembler (Goto label) = singleInst state $ invokeInstance "gotoLabel" (Assembler -> String -> JVM_IO ()) assembler label

runAsm state assembler I2b = singleInst state $ invokeInstance "i2b" (Assembler -> JVM_IO ()) assembler
runAsm state assembler I2c = singleInst state $ invokeInstance "i2c" (Assembler -> JVM_IO ()) assembler
runAsm state assembler I2d = singleInst state $ invokeInstance "i2d" (Assembler -> JVM_IO ()) assembler
runAsm state assembler I2l = singleInst state $ invokeInstance "i2l" (Assembler -> JVM_IO ()) assembler
runAsm state assembler I2s = singleInst state $ invokeInstance "i2s" (Assembler -> JVM_IO ()) assembler
runAsm state assembler Iadd = singleInst state $ invokeInstance "iadd" (Assembler -> JVM_IO ()) assembler
runAsm state assembler Iaload = singleInst state $ invokeInstance "iaload" (Assembler -> JVM_IO ()) assembler
runAsm state assembler Iand = singleInst state $ invokeInstance "iand" (Assembler -> JVM_IO ()) assembler
runAsm state assembler Iastore = singleInst state $ invokeInstance "iastore" (Assembler -> JVM_IO ()) assembler
runAsm state assembler Ior = singleInst state $ invokeInstance "ior" (Assembler -> JVM_IO ()) assembler
runAsm state assembler Ixor = singleInst state $ invokeInstance "ixor" (Assembler -> JVM_IO ()) assembler
runAsm state assembler Icompl = singleInst state $ invokeInstance "icompl" (Assembler -> JVM_IO ()) assembler
runAsm state assembler (Iconst n) = singleInst state $ invokeInstance "iconst" (Assembler -> Int -> JVM_IO ()) assembler n
runAsm state assembler Idiv = singleInst state $ invokeInstance "idiv" (Assembler -> JVM_IO ()) assembler
runAsm state assembler (Ifeq label) = singleInst state $ invokeInstance "ifeq" (Assembler -> String -> JVM_IO ()) assembler label
runAsm state assembler (Ificmpge label) = singleInst state $ invokeInstance "ificmpge" (Assembler -> String -> JVM_IO ()) assembler label
runAsm state assembler (Ificmpgt label) = singleInst state $ invokeInstance "ificmpgt" (Assembler -> String -> JVM_IO ()) assembler label
runAsm state assembler (Ificmple label) = singleInst state $ invokeInstance "ificmple" (Assembler -> String -> JVM_IO ()) assembler label
runAsm state assembler (Ificmplt label) = singleInst state $ invokeInstance "ificmplt" (Assembler -> String -> JVM_IO ()) assembler label
runAsm state assembler (Ifnonnull label) = singleInst state $ invokeInstance "ifnonnull" (Assembler -> String -> JVM_IO ()) assembler label
runAsm state assembler (Ifnull label) = singleInst state $ invokeInstance "ifnull" (Assembler -> String -> JVM_IO ()) assembler label
runAsm state assembler (Iload n) = singleInst state $ invokeInstance "iload" (Assembler -> Int -> JVM_IO ()) assembler n
runAsm state assembler Imul = singleInst state $ invokeInstance "imul" (Assembler -> JVM_IO ()) assembler
runAsm state assembler (InstanceOf className) = singleInst state $ invokeInstance "instanceOf" (Assembler -> String -> JVM_IO ()) assembler className
runAsm state assembler (InvokeMethod invocType cname mname desc isIntf) = singleInst state $ do
  let invocTypeAsm = invocTypeNum invocType
  invokeInstance
    "invokeMethod"
    (Assembler -> Int -> ClassName -> MethodName -> Descriptor -> Bool -> JVM_IO ())
    assembler
    invocTypeAsm
    cname
    mname
    desc
    isIntf

runAsm state assembler (InvokeDynamic mname desc handle bsmArgs) = singleInst state $ do
  jbsmArgsList <- sequence $ toJbsmArg <$> bsmArgs
  jbsmArgs <- ArrayList.fromList jbsmArgsList
  jhandle <- toJHandle handle
  invokeInstance
    "invokeDynamic"
    (Assembler -> MethodName -> Descriptor -> JHandle -> JList -> JVM_IO ())
    assembler
    mname
    desc
    jhandle
    (believe_me jbsmArgs)

runAsm state assembler Irem = singleInst state $ invokeInstance "irem" (Assembler -> JVM_IO ()) assembler
runAsm state assembler Ireturn = singleInst state $ invokeInstance "ireturn" (Assembler -> JVM_IO ()) assembler
runAsm state assembler Ishl = singleInst state $ invokeInstance "ishl" (Assembler -> JVM_IO ()) assembler
runAsm state assembler Ishr = singleInst state $ invokeInstance "ishr" (Assembler -> JVM_IO ()) assembler
runAsm state assembler (Istore n) = singleInst state $ invokeInstance "istore" (Assembler -> Int -> JVM_IO ()) assembler n
runAsm state assembler Isub = singleInst state $ invokeInstance "isub" (Assembler -> JVM_IO ()) assembler
runAsm state assembler Iushr = singleInst state $ invokeInstance "iushr" (Assembler -> JVM_IO ()) assembler
runAsm state assembler L2i = singleInst state $ invokeInstance "l2i" (Assembler -> JVM_IO ()) assembler
runAsm state assembler (LabelStart label) = singleInst state $ invokeInstance "labelStart" (Assembler -> String -> JVM_IO ()) assembler label
runAsm state assembler Ladd = singleInst state $ invokeInstance "ladd" (Assembler -> JVM_IO ()) assembler
runAsm state assembler Land = singleInst state $ invokeInstance "land" (Assembler -> JVM_IO ()) assembler
runAsm state assembler Laload = singleInst state $ invokeInstance "laload" (Assembler -> JVM_IO ()) assembler
runAsm state assembler Lastore = singleInst state $ invokeInstance "lastore" (Assembler -> JVM_IO ()) assembler
runAsm state assembler Lor = singleInst state $ invokeInstance "lor" (Assembler -> JVM_IO ()) assembler
runAsm state assembler Lxor = singleInst state $ invokeInstance "lxor" (Assembler -> JVM_IO ()) assembler
runAsm state assembler Lcompl = singleInst state $ invokeInstance "lcompl" (Assembler -> JVM_IO ()) assembler
runAsm state assembler (Lconst c) = singleInst state $ invokeInstance "lconst" (Assembler -> Bits64 -> JVM_IO ()) assembler c

runAsm state assembler (Ldc (TypeConst ty)) = singleInst state $ invokeInstance "ldcType" (Assembler -> String -> JVM_IO ()) assembler ty
runAsm state assembler (Ldc constant) = singleInst state $ invokeInstance "ldc" (Assembler -> Object -> JVM_IO ()) assembler (constantToObject constant)

runAsm state assembler Ldiv = singleInst state $ invokeInstance "ldiv" (Assembler -> JVM_IO ()) assembler
runAsm state assembler (Lload n) = singleInst state $ invokeInstance "lload" (Assembler -> Int -> JVM_IO ()) assembler n
runAsm state assembler Lmul = singleInst state $ invokeInstance "lmul" (Assembler -> JVM_IO ()) assembler
runAsm state assembler (LookupSwitch defaultLabel labels cases) = singleInst state $ do
  jlabels <- ArrayList.fromList labels
  jcases <- ArrayList.fromList $ JInteger.valueOf <$> cases
  invokeInstance
    "lookupSwitch"
    (Assembler -> String -> JList -> JList -> JVM_IO ())
    assembler
    defaultLabel
    (believe_me jlabels)
    (believe_me jcases)

runAsm state assembler Lrem = singleInst state $ invokeInstance "lrem" (Assembler -> JVM_IO ()) assembler
runAsm state assembler Lreturn = singleInst state $ invokeInstance "lreturn" (Assembler -> JVM_IO ()) assembler
runAsm state assembler Lshl = singleInst state $ invokeInstance "lshl" (Assembler -> JVM_IO ()) assembler
runAsm state assembler Lshr = singleInst state $ invokeInstance "lshr" (Assembler -> JVM_IO ()) assembler
runAsm state assembler (Lstore n) = singleInst state $ invokeInstance "lstore" (Assembler -> Int -> JVM_IO ()) assembler n
runAsm state assembler Lsub = singleInst state $ invokeInstance "lsub" (Assembler -> JVM_IO ()) assembler
runAsm state assembler Lushr = singleInst state $ invokeInstance "lushr" (Assembler -> JVM_IO ()) assembler
runAsm state assembler (MaxStackAndLocal stack local)
  = singleInst state $ invokeInstance "maxStackAndLocal" (Assembler -> Int -> Int -> JVM_IO ()) assembler stack local
runAsm state assembler MethodCodeStart = singleInst state $ invokeInstance "methodCodeStart" (Assembler -> JVM_IO ()) assembler
runAsm state assembler MethodCodeEnd = singleInst state $ invokeInstance "methodCodeEnd" (Assembler -> JVM_IO ()) assembler
runAsm state assembler (Multianewarray desc dims)
  = singleInst state $ invokeInstance "multiANewArray" (Assembler -> String -> Int -> JVM_IO ()) assembler desc (cast dims)
runAsm state assembler (New cname) = singleInst state $ invokeInstance "asmNew" (Assembler -> String -> JVM_IO ()) assembler cname
runAsm state assembler Pop = singleInst state $ invokeInstance "pop" (Assembler -> JVM_IO ()) assembler
runAsm state assembler Pop2 = singleInst state $ invokeInstance "pop2" (Assembler -> JVM_IO ()) assembler
runAsm state assembler Return = singleInst state $ invokeInstance "asmReturn" (Assembler -> JVM_IO ()) assembler
runAsm state assembler Saload = singleInst state $ invokeInstance "saload" (Assembler -> JVM_IO ()) assembler
runAsm state assembler Sastore = singleInst state $ invokeInstance "sastore" (Assembler -> JVM_IO ()) assembler
runAsm state assembler ShouldDescribeFrame = singleInst state $ invokeInstance "shouldDescribeFrame" (Assembler -> JVM_IO Bool) assembler
runAsm state assembler (SourceInfo sourceFileName)
  = singleInst state $ invokeInstance "sourceInfo" (Assembler -> String -> JVM_IO ()) assembler sourceFileName
runAsm state assembler (Subroutine subroutine) = pure ((), record { subroutines $= (subroutine ::) } state)
runAsm state assembler (UpdateFunctionName (MkJMethodName cname fname))
  = singleInst state $ invokeInstance "updateFunctionName" (Assembler -> String -> String -> JVM_IO ()) assembler cname fname
runAsm state assembler (UpdateFunctionLocTypes types) = pure ((), record { functionLocTypes = types} state)
runAsm state assembler (UpdateFunctionRetType retTy) = pure ((), record { functionRetType = retTy } state)
runAsm state assembler (UpdateFunctionTypes types) = pure ((), record { functionTypes = types } state)
runAsm state assembler (UpdateLocalVarCount n)
  = singleInst state $ invokeInstance "updateLocalVarCount" (Assembler -> Int -> JVM_IO ()) assembler (cast n)
runAsm state assembler (UpdateShouldDescribeFrame shouldDescribeFrame)
  = singleInst state $ invokeInstance "updateShouldDescribeFrame" (Assembler -> Bool -> JVM_IO ()) assembler shouldDescribeFrame
runAsm state assembler (UpdateSwitchIndex n)
  = singleInst state $ invokeInstance "updateSwitchIndex" (Assembler -> Int -> JVM_IO ()) assembler (cast n)
runAsm state assembler (UpdateIfIndex n)
  = singleInst state $ invokeInstance "updateIfIndex" (Assembler -> Int -> JVM_IO ()) assembler (cast n)
runAsm state assembler (Pure v) = pure (v, state)
runAsm state assembler (Bind asm f) = do
  (v, newState) <- runAsm state assembler asm
  runAsm newState assembler $ f v

ext: idr


text:
module Data.List.TR

import Data.Iterable
import Data.List
import Control.MonadRec
import Control.Monad.Identity

export
replicateM : MonadRec m => Nat -> m a -> m (List a)
replicateM n ma = iterM (\_,as => (:: as) <$> ma) id Nil n

export
iterateM : MonadRec m => Nat -> (a -> m a) -> a -> m (List a)
iterateM n f ini = iterM next snd (ini,Nil) n
  where next : Nat -> (a,List a) -> m (a,List a)

export
replicateTR : Nat -> a -> List a
replicateTR n va = run Nil n
  where run : List a -> Nat -> List a
        run xs 0     = xs
        run xs (S k) = run (va :: xs) k

export
iterateTR : Nat -> (a -> a) -> a -> List a
iterateTR n f = run Nil n
  where run : List a -> Nat -> a -> List a
        run xs 0     _  = reverse xs
        run xs (S k) va = run (va :: xs) k (f va)

export
mapTR : (a -> b) -> List a -> List b
mapTR f = run Nil
  where run : List b -> List a -> List b
        run bs []       = reverse bs
        run bs (h :: t) = run (f h :: bs) t


text:
module DB.SQLite.SQLiteCodes
-- Status codes for SQLite

%access public
%default total

SQLiteCode : Type
SQLiteCode = Int

sqlite_OK : Int
sqlite_OK = 0 -- Successful result
-- beginning-of-error-codes

sqlite_ERROR : Int
sqlite_ERROR = 1 -- SQL error or missing database

sqlite_INTERNAL : Int
sqlite_INTERNAL = 2 -- Internal logic error in SQLite

sqlite_PERM : Int
sqlite_PERM = 3 -- Access permission denied

sqlite_ABORT : Int
sqlite_ABORT = 4 -- Callback routine requested an abort

sqlite_BUSY : Int
sqlite_BUSY = 5 -- The database file is locked

sqlite_LOCKED : Int
sqlite_LOCKED = 6 -- A table in the database is locked

sqlite_NOMEM : Int
sqlite_NOMEM = 7 -- A malloc() failed

sqlite_READONLY : Int
sqlite_READONLY = 8 -- Attempt to write a readonly database

sqlite_INTERRUPT : Int
sqlite_INTERRUPT = 9 -- Operation terminated by sqlite3_interrupt()

sqlite_IOERR : Int
sqlite_IOERR = 10 -- Some kind of disk I/O error occurred

sqlite_CORRUPT : Int
sqlite_CORRUPT = 11 -- The database disk image is malformed

sqlite_NOTFOUND : Int
sqlite_NOTFOUND = 12 -- Unknown opcode in sqlite3_file_control()

sqlite_FULL : Int
sqlite_FULL = 13 -- Insertion failed because database is full

sqlite_CANTOPEN : Int
sqlite_CANTOPEN = 14 -- Unable to open the database file

sqlite_PROTOCOL : Int
sqlite_PROTOCOL = 15 -- Database lock protocol error

sqlite_EMPTY : Int
sqlite_EMPTY = 16 -- Database is empty

sqlite_SCHEMA : Int
sqlite_SCHEMA = 17 -- The database schema changed

sqlite_TOOBIG : Int
sqlite_TOOBIG = 18 -- String or BLOB exceeds size limit

sqlite_CONSTRAINT : Int
sqlite_CONSTRAINT = 19 -- Abort due to constraint violation

sqlite_MISMATCH : Int
sqlite_MISMATCH = 20 -- Data type mismatch

sqlite_MISUSE : Int
sqlite_MISUSE = 21 -- Library used incorrectly

sqlite_NOLFS : Int
sqlite_NOLFS = 22 -- Uses OS features not supported on host

sqlite_AUTH : Int
sqlite_AUTH = 23 -- Authorization denied

sqlite_FORMAT : Int
sqlite_FORMAT = 24 -- Auxiliary database format error

sqlite_RANGE : Int
sqlite_RANGE = 25 -- 2nd parameter to sqlite3_bind out of range

sqlite_NOTADB : Int
sqlite_NOTADB = 26 -- File opened that is not a database file

sqlite_NOTICE : Int
sqlite_NOTICE = 27 -- Notifications from sqlite3_log()

sqlite_WARNING : Int
sqlite_WARNING = 28 -- Warnings from sqlite3_log()

sqlite_ROW : Int
sqlite_ROW = 100 -- sqlite3_step() has another row ready

sqlite_DONE : Int
sqlite_DONE = 101 -- sqlite3_step() has finished executing
-- end-of-error-codes

data StepResult = Unstarted
                | StepFail
                | StepComplete
                | NoMoreRows

-- FIXME: For some reason, pattern matching doesn't work
-- when using the
stepResult : Int -> StepResult
stepResult 100 = StepComplete -- step complete, but more data available
stepResult 101 = NoMoreRows -- statement has been fully executed
stepResult _ = StepFail -- an error occurred

hasMoreRows : StepResult -> Bool
hasMoreRows NoMoreRows = False
hasMoreRows StepComplete = True
hasMoreRows StepFail = True
hasMoreRows Unstarted = True

max_stars_repo_name: ethansr/IdrisSqlite

max_issues_repo_name: ethansr/IdrisSqlite

max_forks_repo_name: ethansr/IdrisSqlite


text:
module Compiler.Jvm.FunctionTree

import Compiler.Common
import Compiler.CompileExpr
import Compiler.Inline

import Core.Context
import Core.Name

import Compiler.Jvm.Asm
import Compiler.Jvm.Jname
import Compiler.Jvm.Tree

import Libraries.Data.SortedSet
import Data.Vect

parameters (defs: Map String NamedDef)
    mutual
        buildFunctionTreeConAlt : List (Tree Name) -> SortedSet Name -> List NamedConAlt -> (SortedSet Name, List (Tree Name))
        buildFunctionTreeConAlt acc visited [] = (visited, acc)
        buildFunctionTreeConAlt acc visited ((MkNConAlt n _ tag args sc) :: alts) =
            let (visited, newAcc) = buildFunctionTreeExp acc visited sc
            in buildFunctionTreeConAlt newAcc visited alts

        buildFunctionTreeConstAlt : List (Tree Name) -> SortedSet Name -> List NamedConstAlt -> (SortedSet Name, List (Tree Name))
        buildFunctionTreeConstAlt acc visited [] = (visited, acc)
        buildFunctionTreeConstAlt acc visited ((MkNConstAlt c exp) :: alts) =
            let (visited, newAcc) = buildFunctionTreeExp acc visited exp
            in buildFunctionTreeConstAlt newAcc visited alts

        buildFunctionTreeArgs : List (Tree Name) -> SortedSet Name -> Vect n NamedCExp -> (SortedSet Name, List (Tree Name))
        buildFunctionTreeArgs acc visited [] = (visited, acc)
        buildFunctionTreeArgs acc visited (arg :: args) =
            let (visited, newAcc) = buildFunctionTreeExp acc visited arg
            in buildFunctionTreeArgs newAcc visited args

        buildFunctionTreeCApp : List (Tree Name) -> SortedSet Name -> List NamedCExp -> (SortedSet Name, List (Tree Name))
        buildFunctionTreeCApp acc visited [] = (visited, acc)
        buildFunctionTreeCApp acc visited (arg :: args) =
            let (visited, newAcc) = buildFunctionTreeExp acc visited arg
            in buildFunctionTreeCApp newAcc visited args

        buildFunctionTreeExp : List (Tree Name) -> SortedSet Name -> NamedCExp -> (SortedSet Name, List (Tree Name))
        buildFunctionTreeExp acc visited (NmLocal fc el) = (visited, acc)
        buildFunctionTreeExp acc visited (NmLam fc x sc) = buildFunctionTreeExp acc visited sc
        buildFunctionTreeExp acc visited (NmLet fc x val sc) =
            let (visited, valAcc) = buildFunctionTreeExp acc visited val
            in buildFunctionTreeExp valAcc visited sc
        buildFunctionTreeExp acc visited (NmApp fc (NmRef _ f) args) =
            let (visited, newAcc) = buildFunctionTreeCApp acc visited args
            in
                if SortedSet.contains f visited then
                    (visited, newAcc)
                else let (visited, child) = buildFunctionTree visited f
                     in (visited, child :: newAcc)
        buildFunctionTreeExp acc visited (NmApp fc f args) =
            let (visited, newAcc) = buildFunctionTreeCApp acc visited args
            in buildFunctionTreeExp newAcc visited f
        buildFunctionTreeExp acc visited (NmCon fc name _ tag args) = buildFunctionTreeCApp acc visited args
        buildFunctionTreeExp acc visited (NmOp fc op args) = buildFunctionTreeArgs acc visited args
        buildFunctionTreeExp acc visited (NmExtPrim fc p args) = buildFunctionTreeCApp acc visited args
        buildFunctionTreeExp acc visited (NmForce fc _ t) = buildFunctionTreeExp acc visited t
        buildFunctionTreeExp acc visited (NmDelay fc _ t) = buildFunctionTreeExp acc visited t
        buildFunctionTreeExp acc visited (NmConCase fc sc alts def)
            = let (visited, accSc) = buildFunctionTreeExp acc visited sc
                  (visited, accDefc) = maybe ((visited, accSc)) (\v => buildFunctionTreeExp accSc visited v) def
              in buildFunctionTreeConAlt accDefc visited alts
        buildFunctionTreeExp acc visited (NmConstCase fc sc alts def)
            = let (visited, accDefc) = maybe ((visited, acc)) (\v => buildFunctionTreeExp acc visited v) def
                  (visited, accSc) = buildFunctionTreeExp accDefc visited sc
              in buildFunctionTreeConstAlt accSc visited alts
        buildFunctionTreeExp acc visited (NmPrimVal fc c) = (visited, acc)
        buildFunctionTreeExp acc visited (NmErased fc) = (visited, acc)
        buildFunctionTreeExp acc visited (NmCrash fc msg) = (visited, acc)
        buildFunctionTreeExp acc visited expr = (visited, acc)

        buildFunctionTreeDef : SortedSet Name -> Name -> NamedDef -> (SortedSet Name, List (Tree Name))
        buildFunctionTreeDef visited n (MkNmFun args exp) = buildFunctionTreeExp [] visited exp
        buildFunctionTreeDef visited n (MkNmError exp) = buildFunctionTreeExp [] visited exp
        buildFunctionTreeDef visited n (MkNmForeign _ _ _) = (visited, [])
        buildFunctionTreeDef visited n (MkNmCon _ _ _) = (visited, [])

        findDef : Name -> Maybe NamedDef
        findDef name =
            let nameStr = jvmSimpleName name
            in unsafePerformIO $ Map.get defs nameStr

        buildFunctionTree : SortedSet Name -> Name -> (SortedSet Name, Tree Name)
        buildFunctionTree visitedSoFar name =
            let visited = SortedSet.insert name visitedSoFar
            in case findDef name of
               Nothing => (visited, Node name [])
               Just d => let (visited, children) = buildFunctionTreeDef visited name d
                    in (visited, Node name children)

export
buildFunctionTreeMain : Name -> Map String NamedDef -> Tree Name
buildFunctionTreeMain mainFunctionName defs = snd $ buildFunctionTree defs SortedSet.empty mainFunctionName


text:
module Subst

-- This module constructs an expressively typed substitution
-- function 'subst' for substituting variables in the simply-typed
-- lambda calculus.
--
-- The key point is that the expressive type signature of the
-- function 'subst' can be read as the following theorem:
--
--    "Given a context 'ctx' and a variable with
--     de Bruijn index 'i'. Given further the terms
--       ts : Term sctx s, and
--       tt : Term (insertAt i s ctx) t.
--     Then 'subst ts i tt' has type 't' in context '(ctx++sctx)'."
--
-- Note that 'subst ts i tt' is typically written as "tt[ts/(TVar i)]".
--
-- Note that the theorem that is expressed by the type signature
-- of 'subst' is usually referred to as
--
--    *** the substitution lemma ***
--
-- and casually summarized as
--
--    *** substitution preserves type ***.
--

import FinCmp
import Term

%default total

-------------------------------------------------------------
-- Begin: WEAKENING, I.E. ADDING UNUSED VARIABLES TO CONTEXTS

-- Abbreviate the name of the function 'weakenN'
-- from 'Data.Fin' (for better readability):
wkN : (n : Nat) -> Fin m -> Fin (m + n)
wkN = Data.Fin.weakenN

-- Note that we only require weakening of a context 'ctx'
-- by appending another context on the right only.
weakeningPreservesType : {ctx : Context m} -> {ctx' : Context n} ->
                         {i : Fin m} ->
                         (index i ctx = t) ->
                         (index (wkN n i) (ctx ++ ctx') = t)
weakeningPreservesType {ctx = (_::_)}   {i = FZ}      eq = eq
weakeningPreservesType {ctx = (_:: xs)} {i = (FS i')} eq =
  weakeningPreservesType {i = i'} eq

weakenContext : {m : Nat} -> (ctx : Context m) ->
                {n : Nat} -> (ctx' : Context n) ->
                Term ctx t ->
                Term (ctx ++ ctx') t
weakenContext ctx {n = n} ctx' (TVar i {prf = p}) =
  TVar (wkN n i) {prf = weakeningPreservesType p}
--
weakenContext ctx ctx' (TAbs {s} e)    = TAbs (weakenContext (s::ctx) ctx' e)
weakenContext ctx ctx' (TApp e1 e2)    = TApp (weakenContext ctx ctx' e1)
                                              (weakenContext ctx ctx' e2)
weakenContext ctx ctx' (TFix e)        = TFix (weakenContext ctx ctx' e)
weakenContext _   _    TZero           = TZero
weakenContext ctx ctx' (TSucc e)       = TSucc (weakenContext ctx ctx' e)
weakenContext ctx ctx' (TPred e)       = TPred (weakenContext ctx ctx' e)
weakenContext ctx ctx' (TIfz e1 e2 e3) = TIfz (weakenContext ctx ctx' e1)
                                              (weakenContext ctx ctx' e2)
                                              (weakenContext ctx ctx' e3)

-- End: WEAKENING, I.E. ADDING UNUSED VARIABLES TO CONTEXTS
-----------------------------------------------------------

-----------------------------------------------------------------
-- Begin: TECHNICAL LEMMATA ABOUT INDEXING INTO MODIFIED CONTEXTS

-- Function 'lookupInserted' yields a proof of the following:
--
--     "Let ctx' = insertAt i s ctx, and let i = j.
--      If (index j ctx' = t), then t = s."
--
lookupInserted : {ctx : Context n} -> {s : Ty} -> {t : Ty} ->
                 {i : Fin (S n)} -> {j : Fin (S n)} ->
                 i = j ->
                 index j (insertAt i s ctx) = t ->
                 t = s
lookupInserted                {i = FZ}      {j = FZ}      _  prf = sym prf
lookupInserted {ctx} {s} {t}  {i = FZ}      {j = (FS j')} eq prf =
  sym $ replace {P = \k => index k (insertAt FZ s ctx) = t} (sym eq) prf
--
lookupInserted {ctx} {s} {t}  {i = (FS i')} {j = FZ}      eq prf =
  sym $ replace {P = \k => index FZ (insertAt k s ctx) = t} eq prf
--
lookupInserted {ctx = (_::_)} {i = (FS i')} {j = (FS j')} eq  prf =
  lookupInserted (FSinjective eq) prf

-- Function 'shiftDown' yields a proof of the following:
--
--     "Let ctx' = insertAt i s ctx, and let i < (j+1).
--      If (index (j+1) ctx' = t), then (index j ctx = t)."
--
shiftDown : {ctx : Context n} -> {s : Ty} ->
            {i : Fin (S n)} -> {j : Fin n} ->
            i :<: (FS j) ->
            index (FS j) (insertAt i s ctx) = t ->
            index j ctx = t
--
shiftDown {i = FZ}     {j = _}      _  prf = prf
shiftDown {i = (FS _)} {j = FZ}     lt prf =
  absurd $ finNotLtZ $ finLtPred lt
--
shiftDown {ctx = (_::xs)} {s} {i = (FS i')} {j = (FS j')} lt prf =
  shiftDown {ctx = xs} {s} {i = i'} {j = j'} (finLtPred lt) prf

-- Function 'indexZeroLemma' yields a proof of the following:
--
--     "Let ctx a non-empty context, and let ctx' = insertAt t (i+1) ctx.
--      Then, (index 0 ctx') = (index 0 ctx)."
--
indexZeroLemma : {ctx : Context (S n)} ->
                 (i : Fin (S n)) ->
                 index FZ (insertAt (FS i) t ctx) = index FZ ctx
--
indexZeroLemma {ctx = (_::_)} _ = Refl

-- Function 'pushLemma' yields a proof of the following:
--
--    "Let ctx be a context, and let (index i ctx = t).
--     Then, index (i+1) (s::ctx) = t."
--
pushLemma : (s : Ty) ->
            index i ctx = t ->
            index (FS i) (s::ctx) = t
pushLemma _ eq = eq

-- Function 'tightenBound' yields a proof of the following:
--
--     "Let ctx be a context, and let ctx' = insertAt i s ctx.
--      If (j < i) and (index j ctx' = t), then index j ctx = t."
--
-- The function 'tightenBound' returns a dependent pair.
--
-- The first component of the pair is 'j_', which represents
-- the same value as the function argument 'j' (as natural
-- numbers); but note that the bound on the ordinal 'j_' has
-- been tightened (by using the assumption "j < i"):
--   "j_ : Fin n"  while  "j : Fin (S n)".
--
-- The second component of the dependent pair is a proof of
--   "index j_ ctx = t".
--
tightenBound :  {n : Nat} -> {ctx : Context n} ->
                (j : Fin (S n)) -> {i : Fin (S n)} ->
                j :<: i ->
                index j (insertAt i s ctx) = t ->
                (j_ : Fin n ** (index j_ ctx = t))
--
tightenBound                 _       {i = FZ}      lt _  =
  absurd $ finNotLtZ lt
--
tightenBound {n = (S n')}    FZ      {i = (FS i')} _  eq =
  let izl = indexZeroLemma i'
      eq_ = trans (sym izl) eq
  in (FZ ** eq_)
--
tightenBound {ctx = (x::xs)} (FS j') {i = (FS i')} lt eq =
  let (j_ ** eq_) = tightenBound {ctx = xs} j' (finLtPred lt) eq
  in (FS j_ ** pushLemma x eq_)

-- When adding variables in 'ctx' in the middle of
-- a context 'ctx1++ctx2', de Bruijn indices must
-- be adjusted accordingly:
shift : {ctx1 : Context n1} -> {ctx2 : Context n2} -> {i : Fin (n1+n2)} ->
        (ctx : Context n) -> index i (ctx1++ctx2) = t ->
        (i' : Fin (n1+(n+n2)) ** index i' (ctx1++(ctx++ctx2)) = t)
shift {ctx1 = []}         {i}         []       eq = (i ** eq)
--
shift {ctx1 = []}         {i}         (c::ctx) eq =
  let (i' ** eq') = shift {ctx1=[]} ctx eq
  in (FS i' ** eq')
shift {ctx1 = (_::ctx1')} {i = FZ}    ctx      eq = (FZ ** eq)
--
shift {ctx1 = (_::ctx1')} {i = FS i'} ctx      eq =
  let (i' ** eq') = shift {ctx1=ctx1'} ctx eq
  in (FS i' ** eq')

shiftTerm : (ctx : Context n) -> Term (ctx1++ctx2) t ->
            Term (ctx1++(ctx++ctx2)) t
shiftTerm {n = n} {ctx1 = ctx1} {ctx2 = ctx2} ctx (TVar i {prf}) =
  let (i' ** prf') = shift {ctx1=ctx1} {ctx2=ctx2} ctx prf
  in TVar i' {prf=prf'}
--
shiftTerm {n = n} {ctx1 = ctx1} {ctx2 = ctx2} {t = t1 :->: t2} ctx (TAbs e) =
  let e' = shiftTerm {ctx1=(t1::ctx1)} {ctx2=ctx2} ctx e
  in TAbs e'
--
shiftTerm {n = n} {ctx1 = ctx1} {ctx2 = ctx2} ctx (TApp e1 e2) =
  let e1' = shiftTerm {ctx1=ctx1} {ctx2=ctx2} ctx e1
      e2' = shiftTerm {ctx1=ctx1} {ctx2=ctx2} ctx e2
  in TApp e1' e2'
--
shiftTerm {n = n} {ctx1 = ctx1} {ctx2 = ctx2} ctx (TFix e) =
  let e' = shiftTerm {ctx1=ctx1} {ctx2=ctx2} ctx e
  in TFix e'
--
shiftTerm {n = n} {ctx1 = ctx1} {ctx2 = ctx2} ctx TZero = TZero
--
shiftTerm {n = n} {ctx1 = ctx1} {ctx2 = ctx2} ctx (TSucc e) =
  let e' = shiftTerm {ctx1=ctx1} {ctx2=ctx2} ctx e
  in TSucc e'
--
shiftTerm {n = n} {ctx1 = ctx1} {ctx2 = ctx2} ctx (TPred e) =
  let e' = shiftTerm {ctx1=ctx1} {ctx2=ctx2} ctx e
  in TPred e'
--
shiftTerm {n = n} {ctx1 = ctx1} {ctx2 = ctx2} ctx (TIfz e1 e2 e3) =
  let e1' = shiftTerm {ctx1=ctx1} {ctx2=ctx2} ctx e1
      e2' = shiftTerm {ctx1=ctx1} {ctx2=ctx2} ctx e2
      e3' = shiftTerm {ctx1=ctx1} {ctx2=ctx2} ctx e3
  in TIfz e1' e2' e3'

-- End: TECHNICAL LEMMATA ABOUT INDEXING INTO MODIFIED CONTEXTS
---------------------------------------------------------------

-----------------------------------------------------------------------------
-- Begin: SUBSTITUTION PRESERVES TYPING OF EXPRESSIONS IN THE LAMBDA CALCULUS

subst_var' : Term sctx s ->      -- Term of type 's' is subtituted in.
             (i : Fin (S n)) ->  -- The i-th variable (Var i) is substituted for.
             (j : Fin (S n)) ->  -- Substitution takes place inside the term (Var j).
             index j (insertAt i s ctx) = t ->
             Term (ctx++sctx) t
subst_var' {sctx} {ctx} {s} {t} ts i j prf = case finCmpDec i j of
--
-- An actual substitution occurs only if "i = j".
--
-- For "i /= j" no substitution occurs, but the proof 'prf'
-- in the returned expression 'TVar _ {prf}' has to be
-- adjusted to account for the fact that the context has
-- been shortened from (insertAt s i ctx) to 'ctx'.
  CmpEq eq => let eq' = lookupInserted eq prf
                  ts' = shiftTerm {ctx1 = []} {ctx2 = sctx} ctx ts
              in rewrite eq' in ts'
  CmpLt lt => case j of
    FZ    => absurd $ finNotLtZ lt
    FS j' => let t' = TVar j' {ctx = ctx} {prf = shiftDown lt prf}
             in weakenContext ctx sctx t'
  CmpGt gt => case i of
    FZ    => absurd $ finNotLtZ gt
    FS i' => let (j_ ** prf_) = tightenBound j gt prf
                 t' = TVar j_ {ctx = ctx} {prf = prf_}
             in weakenContext ctx sctx t'

export subst : Term sctx s ->                -- Term of type 's' is substituted in.
               (i : Fin (S n)) ->            -- The i-th varibale (Var i) is substituted for.
               Term (insertAt i s ctx) t ->  -- Substitution takes place inside this
                                             -- term of type 't'
               Term (ctx++sctx) t            -- The resulting term is again of type 't'.
--
-- The hard part is substitution in expressions that
-- are variables, i.e. substitution in 'Var j'.
subst ts i (TVar j {prf}) = subst_var' ts i j prf
--
-- Substitution in expressions that are not variables
-- is handled by recursing over (and substituting in)
-- subexpressions:
--
subst {ctx} {t = t1:->:t2} ts i (TAbs e) =
  TAbs $ subst {ctx=t1::ctx} ts (FS i) e
--
subst ts i (TApp e1 e2)    = TApp (subst ts i e1) (subst ts i e2)
subst ts i (TFix e)        = TFix (subst ts i e)
subst _  _ TZero           = TZero
subst ts i (TSucc e)       = TSucc (subst ts i e)
subst ts i (TPred e)       = TPred (subst ts i e)
subst ts i (TIfz e1 e2 e3) = TIfz (subst ts i e1) (subst ts i e2) (subst ts i e3)

-- End: SUBSTITUTION PRESERVES TYPING OF EXPRESSIONS IN THE LAMBDA CALCULUS
---------------------------------------------------------------------------

------------------------------
-- Begin: STRUCTURAL RELATIONS
--
-- Terms always exist in a specific context. As a consequence, terms with different
-- contexts cannot be equal. In fact, they cannot even be compared because the contexts
-- are part of the (Idris) type of a term and therefore comparing terms that exist in
-- different contexts means attempting to compare Idris expressions at different Idris types.
--
-- The following defines relations (data types suffixed with 'R') that hold between
-- structurally equal terms, even if the terms are typed in different contexts.
-- The main result this leads to is captured by the function 'ctxREq' which shows
-- that two terms that are structurally equal and typed in the same context are
-- in fact equal.

-- Finite numbers can be structurally equal even
-- if subject to different bounds 'm' and 'n':
data FinR : {m : Nat} -> {n : Nat} ->
            Fin m -> Fin n -> Type where
  FRZ : FinR (FZ {k=m}) (FZ {k=n})
  FRS : FinR i j -> FinR (FS i) (FS j)

-- The relation 'FinR' holds, for example, bewteen
-- a bounded number 'i' and a weakened version of 'i'
-- where the bound has been weakend with '0':
weakenZeroFinR : (i : Fin m) -> FinR {m=(m+0)} {n=m} (weakenN 0 i) i
weakenZeroFinR FZ      = FRZ
weakenZeroFinR (FS i') = FRS $ weakenZeroFinR i'

-- If 'FinR' holds between finite numbers that are subject
-- to the same bound 'n', then the numbers are equal:
finREq : (i : Fin n) -> (j : Fin n) -> FinR i j -> i = j
finREq FZ      FZ      FRZ      = Refl
finREq (FS i') (FS j') (FRS fr) = cong $ finREq i' j' fr

-- The relation 'TermCtxR' holds for terms that
-- are structurally equal even if typed in different
-- contexts 'ctx1' and 'ctx2':
data TermCtxR : {ctx1 : Context m} -> {ctx2: Context n} ->
                Term ctx1 t -> Term ctx2 t -> Type where
  TCRVar  : {prf1 : index i ctx1 = t} -> {prf2 : index j ctx2 = t} ->
            FinR i j ->
            TermCtxR {ctx1=ctx1} {ctx2=ctx2}
                     (TVar {ctx=ctx1} i {prf=prf1})
                     (TVar {ctx=ctx2} j {prf=prf2})
  --
  TCRAbs  : TermCtxR {ctx1=(t::ctx1')} {ctx2=(t::ctx2')} e e' ->
            TermCtxR {ctx1=ctx1'} {ctx2=ctx2'} (TAbs e) (TAbs e')
  --
  TCRApp  : TermCtxR e1 e1' -> TermCtxR e2 e2' ->
            TermCtxR (TApp e1 e2) (TApp e1' e2')
  --
  TCRFix  : TermCtxR e e' -> TermCtxR (TFix e) (TFix e')
  --
  TCRZero : TermCtxR TZero TZero
  --
  TCRSucc : TermCtxR e e' ->
            TermCtxR (TSucc e) (TSucc e')
  --
  TCRPred : TermCtxR e e' -> TermCtxR (TPred e) (TPred e')
  --
  TCRIfz  : TermCtxR e1 e1' -> TermCtxR e2 e2' -> TermCtxR e3 e3' ->
            TermCtxR (TIfz e1 e2 e3) (TIfz e1' e2' e3')

-- Structural equality of terms 'e1' and 'e2' in the
-- same context 'ctx' implies equality 'e1 = e2:
ctxREq : (e1 : Term ctx t) -> (e2 : Term ctx t) -> TermCtxR e1 e2 -> e1 = e2
--
ctxREq {ctx} {t} (TVar i {prf=prf1}) (TVar j {prf=prf2}) (TCRVar fr) =
  case finREq i j fr of
       Refl => case prf1 of
                    Refl => case prf2 of
                                 Refl => Refl
               -- By matching on the equality proofs 'prf1' and 'prf2' one
               -- effectively ends up using "uniqueness of identity proofs":
               -- Both proofs are matched to the same constructor 'Refl',
               -- and this causes Idris to refine the two arguments of 'ctxREq'
               -- to identical (Idris) expressions, i.e. 'TVar i {prf=Refl}'.
--
ctxREq (TAbs e) (TAbs e') (TCRAbs r) = cong $ ctxREq e e' r
--
ctxREq (TApp e1 e2) (TApp e1' e2') (TCRApp r1 r2) =
  let eq1 = ctxREq e1 e1' r1
      eq2 = ctxREq e2 e2' r2
  in rewrite eq1 in rewrite eq2 in Refl
--
ctxREq (TFix e) (TFix e') (TCRFix r) = cong $ ctxREq e e' r
--
ctxREq TZero TZero TCRZero = Refl
--
ctxREq (TSucc e) (TSucc e') (TCRSucc r) = cong $ ctxREq e e' r
--
ctxREq (TPred e) (TPred e') (TCRPred r) = cong $ ctxREq e e' r
--
ctxREq (TIfz e1 e2 e3) (TIfz e1' e2' e3') (TCRIfz r1 r2 r3) =
  let eq1 = ctxREq e1 e1' r1
      eq2 = ctxREq e2 e2' r2
      eq3 = ctxREq e3 e3' r3
  in rewrite eq1 in rewrite eq2 in rewrite eq3 in Refl

-- Weakening the context 'ctx' of a term 'e' with the empty context '[]'
-- retains the term's structure, i.e. the relation 'TermCtxR' holds
-- between the original term and the weakend one:
weakenEmptyCtxR : (e : Term ctx t) ->
                  TermCtxR {ctx1=(ctx++[])} {ctx2=ctx} (weakenContext ctx [] e) e
--
weakenEmptyCtxR {ctx} (TVar i {prf}) = TCRVar {ctx1=(ctx++[])} {ctx2=ctx} {prf2=prf}
                                              (weakenZeroFinR i)
--
weakenEmptyCtxR (TAbs e)        = TCRAbs (weakenEmptyCtxR e)
weakenEmptyCtxR (TApp e1 e2)    = TCRApp (weakenEmptyCtxR e1) (weakenEmptyCtxR e2)
weakenEmptyCtxR (TFix e)        = TCRFix (weakenEmptyCtxR e)
weakenEmptyCtxR TZero           = TCRZero
weakenEmptyCtxR (TSucc e)       = TCRSucc (weakenEmptyCtxR e)
weakenEmptyCtxR (TPred e)       = TCRPred (weakenEmptyCtxR e)
weakenEmptyCtxR (TIfz e1 e2 e3) = TCRIfz (weakenEmptyCtxR e1)
                                         (weakenEmptyCtxR e2)
                                         (weakenEmptyCtxR e3)

-- Finally, the previous developments of structural equality can be
-- used to show that a term 'e' remains unchanged when its context
-- is weakend with the empty context '[]':
weakenEmptyWithEmpty : (e : Term [] t) -> weakenContext [] [] e = e
weakenEmptyWithEmpty e = let wCtxR = weakenEmptyCtxR e
                         in ctxREq (weakenContext [] [] e) e wCtxR

-- Define 'omega' to be the diverging term that
-- is the fix-point of the identity function:
public export omega : Term [] TyNat
omega = TFix (TAbs $ TVar FZ)

-- To show (later) that 'omega' diverges, one needs the result that
-- substituting 'omega' into a single variable 'TVar FZ' reproduces
-- the term 'omega' itself:
export substOmega : subst {ctx=[]} {s=TyNat} {t=TyNat} Subst.omega FZ (TVar FZ) = Subst.omega
-- Note that while 'substOmega' is a special case of the more general
-- result 'substInVar' (see above), the general result is in fact not
-- needed. This is because the Idris type checker can evaluate
-- 'weakenContext _ _ omega' (resulting from 'subst'), but it cannot
-- evaluate 'weakenContext _ _ e' for a variable 'e' because 'weakenContext'
-- is defined by recursion on the structure of 'e'.
substOmega = Refl

-- End: STRUCTURAL RELATIONS
----------------------------

max_stars_repo_name: normanrink/PCF

max_issues_repo_name: normanrink/PCF

max_forks_repo_name: normanrink/PCF


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

%name Vect xs, ys, zs

elem : Eq a => (value : a) -> (xs : Vect n a) -> Bool
elem value [] = False
elem value (x :: xs) = case value == x of
                            False => elem value xs
                            True => True

max_issues_repo_name: gdevanla/TypeDD-Samples

max_forks_repo_name: gdevanla/TypeDD-Samples


text:
module Main

import Objects.User

main : IO ()
main = putStrLn "hello IdrisVKAPI!"

max_stars_repo_name: GrandArchTemplar/IdrisVKAPI

max_issues_repo_name: GrandArchTemplar/IdrisVKAPI

max_forks_repo_name: GrandArchTemplar/IdrisVKAPI


text:
module Main
import Data.Vect as V
import Prelude.List as L
import Prelude.Basics as B
import Data.String as S
import Utils as U

%default total

data Player = X | O

other : Player -> Player
other X = O
other O = X

Show Player where
	show X = "X"
	show O = "O"

Eq Player where
	X == X = True
	O == O = True
	_ == _ = False

record Board where
	constructor MkBoard
	columns : Matrix 7 7 $ Maybe Player

rows : Board -> Matrix 7 7 $ Maybe Player
rows = transpose . columns

Show Board where
    show = unlines . map (concat . map (maybe "." show)) . L.toList . rows

diagonals1 : Board -> List $ List $ Maybe Player
diagonals1 board = map catMaybes
                 $ transpose
                 $ zipWith (++) (take 7 $ iterate (Nothing::) []) (map (map Just) $ U.toList $ columns board)

diagonals2 : Board -> List $ List $ Maybe Player
diagonals2 = diagonals1 . MkBoard . transpose . columns

draw : Board -> Bool
draw = all (all isJust) . rows

winner : Board -> Maybe Player
winner board = head'
             $ catMaybes
	         $ mapMaybe head' -- Is there a better way to handle the impossible case [] with a proof?
			 $ L.filter (\x => L.length x >= 4)
			 $ concatMap {t = List} {a = List $ Maybe Player} group
			 $ concatMap (\ f => f board) {t = List} {a = Board -> List $ List $ Maybe Player}
			 $ [U.toList . rows, U.toList . columns, diagonals1, diagonals2]

legalMove : (n : Nat) -> Board -> Maybe $ LTE n 6
legalMove n board with (natToFin' n 7)
	| Nothing = Nothing
	| Just (f, p) = map (\ _ => fromLteSucc p) (V.index f $ V.head $ rows board)

dropColumn : Player -> Vect 7 $ Maybe Player -> Vect 7 $ Maybe Player
dropColumn player column =
	let tmp = V.catMaybes $ (Just player) :: (tail column) in
	let n = fst tmp in
	let xs = snd tmp in
	let p1 = catMaybesLTE {xs = (Just player) :: (tail column)} in
	let p2 : ((minus 7 n) + n = 7) = rewrite plusCommutative (minus 7 n) n in plusMinusNeutral p1 in
	rewrite sym p2 in
	(replicate (minus 7 n) Nothing) ++ (map Just xs)

move : Player -> Nat -> Board -> Maybe Board
move player n board with (legalMove n board)
    | Nothing = Nothing
    | Just p = Just board' where
    	tmp : (Vect n $ Vect 7 $ Maybe Player, Vect 7 $ Maybe Player, Vect (minus 6 n) $ Vect 7 $ Maybe Player)
    	tmp = splitAt' n $ rewrite plusMinusNeutral p in columns board

    	board' = let (left, column, right) = tmp in
    		MkBoard $
    		replace {P = \n => Matrix n 7 $ Maybe Player} (plusMinusNeutral $ lteSuccRight p) $
			rewrite sym $ succMinus p in
	        left ++ [dropColumn player column] ++ right

record Game where
	constructor MkGame
	player : Player
	board : Board

partial gameloop : Game -> IO ()
gameloop game@(MkGame player board) = do
    putStr $ show player ++ "s turn: "
    line <- getLine
    case (parsePositive line) >>= (\n => move player n board) of
        Nothing => (print board) >>= (\_ => gameloop game)
        Just board' => do
            print board'
            if draw board
                then putStrLn "Draw!"
                else case winner board' of
                    Just player => putStrLn $ show player ++ " Won!"
                    Nothing => gameloop $ MkGame (other player) board'

partial main : IO ()
main = do
    let board = MkBoard (replicate 7 $ replicate 7 Nothing)
    print board
    gameloop $ MkGame X board


text:
-- ----------------------------------------------------------------- [ Org.idr ]
-- Module    : Org.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module Text.Markup.Edda.Test.Org

import Text.Markup.Edda.Model
import Text.Markup.Edda.Reader.Org

import Lightyear.Testing

export
runTests : IO ()
runTests = Testing.runTests [
      parseTest ( "Markup") (many $ lexeme inline) "asasas *bold* /italic/ ~code~ +strike-through+ =verbatim= $mart$ Hello 'Bye bye'.\n"

    , parseTest ( "Links 1") (many inline) "[[http://www.cs.st-andrews.ac.uk][URL]] [[http://www.cs.st-andrews.ac.uk][URL]] [[http://www.cs.st-andrews.ac.uk][URL]]\n"

    , parseTest ( "Links 2") (many inline) "[[http://www.cs.st-andrews.ac.uk]] [[Boneh2001]] [[citet:Boneh2001]] [[citep:Boneh2001]]\n"

    , parseTest ( "Links 3") (many inline) "[fn:label:description]\n"

    , parseTest ("Attribute Title")  (attribute "TITLE")  "#+TITLE: I am a Title\n\n"
    , parseTest ("Attribute Author") (attribute "AUTHOR") "#+AUTHOR: I am an Author\n\n"
    , parseTest ("Attribute Date ")  (attribute "DATE")   "#+DATE: I is a date\n\n"

    , parseTest ( "Environments")
                (many block)
                """#+CAPTION: sdsd
#+NAME: asas:asasre
#+BEGIN_THEOREM
sdsdsdsd
#+END_THEOREM
#+CAPTION: sdsd
#+NAME: asas:asasre
#+BEGIN_COROLLARY
sdsdsdsd
#+END_COROLLARY
#+CAPTION: sdsd
#+NAME: asas:asasre
#+BEGIN_LEMMA
sdsdsdsd
#+END_LEMMA
#+CAPTION: sdsd
#+NAME: asas:asasre
#+BEGIN_PROPOSITION
sdsdsdsd
#+END_PROPOSITION
#+CAPTION: sdsd
#+NAME: asas:asasre
#+BEGIN_PROOF
sdsdsdsd
#+END_PROOF
#+CAPTION: sdsd
#+NAME: asas:asasre
#+BEGIN_DEFINITION
sdsdsdsd
#+END_DEFINITION
#+CAPTION: sdsd
#+NAME: asas:asasre
#+BEGIN_EXAMPLE
sdsdsdsd
#+END_EXAMPLE
#+CAPTION: sdsd
#+NAME: asas:asasre
#+BEGIN_EXERCISE
sdsdsdsd
#+END_EXERCISE
#+CAPTION: sdsd
#+NAME: asas:asasre
#+BEGIN_NOTE
sdsdsdsd
#+END_NOTE
#+CAPTION: sdsd
#+NAME: asas:asasre
#+BEGIN_PROBLEM
sdsdsdsd
#+END_PROBLEM
#+CAPTION: sdsd
#+NAME: asas:asasre
#+BEGIN_QUESTION
sdsdsdsd
#+END_QUESTION
#+CAPTION: sdsd
#+NAME: asas:asasre
#+BEGIN_REMARK
sdsdsdsd
#+END_REMARK
#+CAPTION: sdsd
#+NAME: asas:asasre
#+BEGIN_SOLUTION
sdsdsdsd
#+END_SOLUTION
"""

    , parseTest ( "Headers")
                (many header)
                """* Introduction

** Contribution

** Outline

* Methodology

** System

** Procedure

* Results

* Discussion

* Conclusion

"""

    , parseTest ( "Source Block 1")
                (orgBlock)
                """#+CAPTION: sdsd
#+NAME: asas:asasre
#+BEGIN_SRC idris

main : IO ()
main = putStrLn "Hello World!"
#+END_SRC

"""

    , parseTest ( "Source Block 2")
                (orgBlock)
                """#+BEGIN_SRC idris
main : IO ()
main = putStrLn "Hello World!"
main : IO ()
main = putStrLn "Hello World!"
#+END_SRC

"""

    , parseTest ( "Quotes")
                (orgBlock)
                """#+BEGIN_QUOTE
dfkljfzdjf
#+END_QUOTE

"""

    , parseTest ( "Figures")
           (orgBlock)
           """#+CAPTION: sdsd
#+NAME: asas:asasre
[[dfjkdjfldjkf]]

"""

    , parseTest ( "Equations")
                (many orgBlock)
                """#+BEGIN_EQUATION
y = a*x^2 + b*x + c
#+END_EQUATION

#+NAME: asas
#+BEGIN_EQUATION
y^2 = x^3 + ax + b
#+END_EQUATION

"""

    , parseTest ("Lists")
                (many orgBlock)
                """+ a
+ b
+ c
+ a
+ b
+ c
- a
- b
- c

1. a
1. b
2. c
3. a
3. b
1. c
2. a
2. b
3. c

+ Term :: Description
+ Term :: Description
+ Term :: Description
+ Term :: Description
+ Term :: Description
+ Term :: Description

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

max_stars_repo_name: jfdm/edda

max_issues_repo_name: jfdm/edda

max_forks_repo_name: jfdm/edda


text:
import AppendVec
import CheckEqDec
import CheckEqMaybe
import EqNat
import ExactLength
import ExactLengthDec
import ReverseVec
import TCVects
import Void


text:
module Minecraft.Core.Block.GenericData

%default total

public export
record GenericBlockData where
  constructor MkBlock
  {auto waterLogged : Bool}

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


text:
module GCrypt
import Effects

%link C "gcrypt_idr.o"
%include C "gcrypt_idr.h"
%lib C "gcrypt"

-- Unimplemented. Eventually, this should encapsulate the flags
-- available to message digest contexts, which this library could
-- OR together.
HashFlag : Type
HashFlag = Int

GCryptResult : Type
GCryptResult = Int

data GCryptStep = GCryptLibInitialised -- Lib initialised
                | GCryptMDInitialised -- Message digest context initialised
                | GCryptMDWritten -- Message digest context has written out the digest

data GCryptRes : Step -> Type where
  LibInitialised : GCryptHashRes s
  -- IOExcept would avoid the need for this...
  LibInitFailed : GCryptHashRes s
  HashContextInitialised : Ptr -> GCryptHashRes s
  HashContextInvalid : GCryptHashRes s

data GCrypt : Effect where
  -- Currently, marshalling a null pointer to a string results in a segfault.
  -- For now, we'll treat this as a bool...
  InitialiseGCrypt : Maybe String -> GCrypt () (GCryptRes GCryptLibInitialised) (Bool) -- (Maybe String)
  InitialiseHashContext : HashAlgorithm -> List HashFlag -> GCrypt (GCryptRes GCryptLibInitialised)
                                                                   (GCryptRes GCryptMDInitialised)
                                                                   (Bool)
{- Not really needed.
  FinaliseHashContext : GCrypt (GCryptRes GCryptMDInitialised)
                               (GCryptRes GCryptMDFinalised)
                               ()
-}

  DisposeHashContext : GCrypt (GCryptRes GCryptMDWritten)
                              (GCryptRes GCryptLibInitialised)
                              ()

  ResetHashContext : GCrypt (GCryptRes GCryptMDWritten)
                            (GCryptRes GCryptMDInitialised)
                            ()

  -- Strings only for now. It'd be nice to get the full AoB thing going, but that might take a bit
  -- of FFI rewriting...
  GetStringMessageDigest : String -> GCrypt (GCryptRes GCryptMDInitialised)
                                            (GCryptRes GCryptMDWritten)
                                            (String)

GCRYPT : Type -> EFFECT
GCRYPT t = MkEff t GCrypt

{- Functions -}
initialiseGCrypt : Maybe String -> EffM IO [GCRYPT ()] [GCRYPT (GCryptRes GCryptLibInitialised)] Bool -- (Maybe String)
initialiseGCrypt ver = (InitialiseGCrypt ver)

-- Initialises a hash context within the library, given an algorithm and a list of flags.
initialiseHashContext : HashAlgorithm -> List HashFlag -> EffM [GCRYPT (GCryptRes GCryptLibInitialised)]
                                                               [GCRYPT (GCryptRes GCryptMDInitialised)]
                                                               (Bool)
initialiseHashContext alg flags = (InitialiseHashContext alg flags)

-- Disposes of a hash context, freeing associated resources
disposeHashContext : EffM IO [GCRYPT (GCryptRes GCryptMDWritten)]
                             [GCRYPT (GCryptRes GCryptLibInitialised)]
                             ()
disposeHashContext = DisposeHashContext

-- Resets a hash context
resetHashContext : EffM IO [GCRYPT (GCryptRes GCryptMDWritten)]
                           [GCRYPT (GCryptRes GCryptMDInitialised)]
                           ()
resetHashContext = ResetHashContext

-- Gets the message digest of a string, using one of the
-- BIG TODO: Tactic to ensure that the given hash algorithm is available
getStringMessageDigest : String -> EffM IO [GCRYPT (GCryptRes GCryptMDInitialised)]
                                           [GCRYPT (GCryptRes GCryptMDWritten)]
                                           (String)
getStringMessageDigest str = (GetStringMessageDigest str)

cleanupResStruct : Ptr -> IO ()
cleanupResStruct ptr = do
  res <- mkForeign (FFun "idris_gcry_dispose_res" [FPtr] FUnit) ptr
  pure ()

instance Handler GCrypt IO where
  handle () (InitialiseGCrypt (Just ver)) k = do
    res <- mkForeign (FFun "idris_gcry_init" [FString] FPtr) ver
    null_res <- isNull res
    if null_res then
      k (LibInitFailed) False
    else
      k (LibInitialised) True

  handle () (InitialiseGCrypt Nothing) k = do
    res <- mkForeign (FFun "idris_gcry_init" [FString] FPtr) ""
    null_res <- isNull res
    if null_res then
      k (LibInitFailed) False
    else
      k (LibInitialised) True

  handle (LibInitialised) (InitialiseHashContext alg flags) = do
    -- TODO: We're ignoring flags for now
    res <- mkForeign (FFun "idris_gcry_init_md" [FInt, FInt] FPtr) alg 0
    -- Res is a structure demonstrating the result code and a pointer
    -- which may, so long as the call was correct, point to a hashing
    -- context. The intermediate library will not return NULL here.
    err <- mkForeign (FFun "idris_gcry_get_struct_err" [FPtr] FInt) res
    -- Once again, I'm quickly hacking around this. The error value returned
    -- by LibGCrypt consists of two distinct parts: the error code, and the
    -- error location. If, however, the operation was successful, then the
    -- whole thing will be 0.
    -- Expect this interface to change when I do it properly.
    if err == 0 then do
      -- Success
      context <- mkForeign (FFun "idris_gcry_get_struct_data" [FPtr] FPtr) res
      -- Prudent to do a null check in case something's gone wrong
      context_null <- isNull context
      cleanupResStruct res
      if context_null then do
        k (HashContextInvalid) Nothing
      else
        k (HashContextInitialised context)
    else
      k (HashContextInvalid) Nothing

max_stars_repo_name: idris-hackers/IdrisWeb

max_issues_repo_name: idris-hackers/IdrisWeb

max_forks_repo_name: idris-hackers/IdrisWeb


text:
module Main

import Data.ZZ
import Data.Matrix
import Data.Matrix.RowEchelon
import Data.Matrix.ZZModuleSpan

import Data.Matrix.ZZGaussianElimination

%flag C "-O3"

-- 1s & 0s only, please.
testmat : Matrix 3 2 ZZ
testmat = map (map Pos) [[0,1],[1,1],[1,0]]

-- 1s & 0s only, please.
testmat2 : Matrix 2 2 ZZ
testmat2 = map (map Pos) [[1,0],[0,1]]

-- 1s & 0s only, please.
testmat3 : Matrix 1 2 ZZ
testmat3 = [[Pos 1, Pos 0]]

-- 1s & 0s only, please.
testmat4 : Matrix 1 2 ZZ
testmat4 = [[Pos 0, Pos 1]]

testmat5 : Matrix 2 1 ZZ
testmat5 = [[Pos 2],[Pos 3]]

testelim : (n' : Nat ** (gexs : Matrix n' 2 ZZ
		** (rowEchelon gexs, bispanslz gexs Main.testmat)))
testelim = gaussElimlz testmat

{-
testelim2 : (n' : Nat ** (gexs : Matrix n' 2 ZZ
		** (rowEchelon gexs, bispanslz gexs Main.testmat2)))
testelim2 = gaussElimlz testmat2

testelim2' : Matrix (getWitness Main.testelim2) 2 ZZ
testelim2' = getWitness $ getProof $ gaussElimlz testmat2
-}

testelim2_ : (n' : Nat ** Matrix n' 2 ZZ)
testelim2_ = (_ ** getWitness $ getProof $ gaussElimlz testmat2)

testelim4_ : (n' : Nat ** Matrix n' 2 ZZ)
testelim4_ = (_ ** getWitness $ getProof $ gaussElimlz testmat4)

testelim5_ : (n' : Nat ** Matrix n' 1 ZZ)
testelim5_ = (_ ** getWitness $ getProof $ gaussElimlz testmat5)

main : IO ()
main = putStrLn $ show $ getProof testelim4_


text:
module Dbcritic.Check.Timestamptz

import Control.IOExcept
import Dbcritic.Check
import Dbcritic.Libpq

mkIssue : String -> String -> Issue
mkIssue table column =
    let
        qual        = table ++ "." ++ column
        identifier  = [ table, column ]
        description = "The column ‘" ++ qual ++ "’ stores timestamps in an ambiguous format."
        problems    = [ "You cannot tell when the event happened without more information."
                      , "Timestamps in different time zones may accumulate in the database." ]
        solutions   = [ "Change the type of the column ‘" ++ qual ++ "’ to ‘timestamptz’." ]
    in
        MkIssue identifier description problems solutions IsNonEmpty IsNonEmpty IsNonEmpty

export
checkTimestamptz : Check
checkTimestamptz = MkCheck name help inspect
    where
    name = "timestamptz"
    help = "Check that columns are of the type ‘timestamptz’ rather than of the type ‘timestamp’."

    inspectRow : List (Maybe String) -> IOExcept String Issue
    inspectRow [Just table, Just column] = pure (mkIssue table column)
    inspectRow _ = ioe_fail "checkTimestamptz: Bad result"

    inspect : PgConnection -> IOExcept String (List Issue)
    inspect conn = do
        res <- pgExecute conn """
            SELECT
                pg_class.relname,
                pg_attribute.attname
            FROM
                pg_attribute
                JOIN pg_class ON pg_class.oid = pg_attribute.attrelid
            WHERE
                pg_attribute.atttypid = 'timestamp' :: regtype AND
                pg_class.relnamespace <> regnamespace 'information_schema' AND
                pg_class.relnamespace <> regnamespace 'pg_catalog'
            ORDER BY
                pg_class.relname,
                pg_attribute.attname
        """
        traverse inspectRow (pgGrid res)

max_stars_repo_name: channable/dbcritic

max_issues_repo_name: channable/dbcritic

max_forks_repo_name: channable/dbcritic


text:
module Idris.Doc.String

import Core.Context
import Core.Context.Log
import Core.Core
import Core.Env
import Core.Metadata
import Core.TT

import Idris.Pretty
import Idris.Pretty.Render
import Idris.REPL.Opts
import Idris.Resugar
import Idris.Syntax

import TTImp.TTImp
import TTImp.TTImp.Functor
import TTImp.Elab.Prim

import Data.List
import Data.List1
import Data.Maybe
import Data.String

import Libraries.Data.ANameMap
import Libraries.Data.NameMap
import Libraries.Data.SortedMap
import Libraries.Data.StringMap as S
import Libraries.Data.String.Extra

import Libraries.Control.ANSI.SGR
import public Libraries.Text.PrettyPrint.Prettyprinter
import public Libraries.Text.PrettyPrint.Prettyprinter.Util

import Parser.Lexer.Source

%default covering

public export
data IdrisDocAnn
  = Header
  | Declarations
  | Decl Name
  | DocStringBody
  | UserDocString
  | Syntax IdrisSyntax

export
-- TODO: how can we deal with bold & so on?
docToDecoration : IdrisDocAnn -> Maybe Decoration
docToDecoration (Syntax syn) = syntaxToDecoration syn
docToDecoration _ = Nothing

export
styleAnn : IdrisDocAnn -> AnsiStyle
styleAnn Header        = underline
styleAnn Declarations  = []
styleAnn (Decl{})      = []
styleAnn DocStringBody = []
styleAnn UserDocString = []
styleAnn (Syntax syn)  = syntaxAnn syn

export
tCon : Name -> Doc IdrisDocAnn -> Doc IdrisDocAnn
tCon n = annotate (Syntax $ TCon (Just n))

export
dCon : Name -> Doc IdrisDocAnn -> Doc IdrisDocAnn
dCon n = annotate (Syntax $ DCon (Just n))

export
fun : Name -> Doc IdrisDocAnn -> Doc IdrisDocAnn
fun n = annotate (Syntax $ Fun n)

export
header : Doc IdrisDocAnn -> Doc IdrisDocAnn
header d = annotate Header d <+> colon

-- Add a doc string for a module name
export
addModDocString : {auto s : Ref Syn SyntaxInfo} ->
                  ModuleIdent -> String ->
                  Core ()
addModDocString mi doc
    = do syn <- get Syn
         put Syn (record { saveMod $= (mi ::)
                         , modDocstrings $= insert mi doc } syn)

-- Add a doc string for a name in the current namespace
export
addDocString : {auto c : Ref Ctxt Defs} ->
               {auto s : Ref Syn SyntaxInfo} ->
               Name -> String ->
               Core ()
addDocString n_in doc
    = do n <- inCurrentNS n_in
         log "doc.record" 50 $
           "Adding doc for " ++ show n_in ++ " (aka " ++ show n ++ " in current NS)"
         syn <- get Syn
         put Syn (record { defDocstrings $= addName n doc,
                           saveDocstrings $= insert n () } syn)

-- Add a doc string for a name, in an extended namespace (e.g. for
-- record getters)
export
addDocStringNS : {auto c : Ref Ctxt Defs} ->
                 {auto s : Ref Syn SyntaxInfo} ->
                 Namespace -> Name -> String ->
                 Core ()
addDocStringNS ns n_in doc
    = do n <- inCurrentNS n_in
         let n' = case n of
                       NS old root => NS (old <.> ns) root
                       root => NS ns root
         syn <- get Syn
         put Syn (record { defDocstrings $= addName n' doc,
                           saveDocstrings $= insert n' () } syn)

prettyTerm : IPTerm -> Doc IdrisDocAnn
prettyTerm = reAnnotate Syntax . Idris.Pretty.prettyTerm

prettyName : Name -> Doc IdrisDocAnn
prettyName n =
  case userNameRoot n of
    -- shouldn't happen: we only show UN anyways...
    Nothing => pretty (nameRoot n)
    Just un => if isOpUserName un then parens (pretty un) else pretty un

prettyKindedName : Maybe String -> Doc IdrisDocAnn -> Doc IdrisDocAnn
prettyKindedName Nothing   nm = nm
prettyKindedName (Just kw) nm
  = annotate (Syntax Keyword) (pretty kw) <++> nm

export
getDocsForPrimitive : {auto c : Ref Ctxt Defs} ->
                      {auto s : Ref Syn SyntaxInfo} ->
                      Constant -> Core (Doc IdrisDocAnn)
getDocsForPrimitive constant = do
    let (_, type) = checkPrim EmptyFC constant
    let typeString = pretty (show constant)
                   <++> colon <++> prettyTerm !(resugar [] type)
    pure (typeString <+> Line <+> indent 2 "Primitive")

public export
data Config : Type where
  ||| Configuration of the printer for a name
  ||| @ longNames   Do we print qualified names?
  ||| @ dropFirst   Do we drop the first argument in the type?
  ||| @ getTotality Do we print the totality status of the function?
  MkConfig : {default True  longNames   : Bool} ->
             {default False dropFirst   : Bool} ->
             {default True  getTotality : Bool} ->
             Config

||| Printer configuration for interface methods
||| * longNames turned off for interface methods because the namespace is
|||             already spelt out for the interface itself
||| * dropFirst turned on for interface methods because the first argument
|||             is always the interface constraint
||| * totality  turned off for interface methods because the methods themselves
|||             are just projections out of a record and so are total
export
methodsConfig : Config
methodsConfig
  = MkConfig {longNames = False}
             {dropFirst = True}
             {getTotality = False}

export
shortNamesConfig : Config
shortNamesConfig
  = MkConfig {longNames = False}
             {dropFirst = False}
             {getTotality = True}

export
getDocsForName : {auto o : Ref ROpts REPLOpts} ->
                 {auto c : Ref Ctxt Defs} ->
                 {auto s : Ref Syn SyntaxInfo} ->
                 FC -> Name -> Config -> Core (Doc IdrisDocAnn)
getDocsForName fc n config
    = do syn <- get Syn
         defs <- get Ctxt
         let extra = case nameRoot n of
                       "-" => [NS numNS (UN $ Basic "negate")]
                       _ => []
         resolved <- lookupCtxtName n (gamma defs)
         let all@(_ :: _) = extra ++ map fst resolved
             | _ => undefinedName fc n
         let ns@(_ :: _) = concatMap (\n => lookupName n (defDocstrings syn)) all
             | [] => pure emptyDoc
         docs <- traverse (showDoc config) ns
         pure $ vcat docs
  where

    showDoc : Config -> (Name, String) -> Core (Doc IdrisDocAnn)

    -- Avoid generating too much whitespace by not returning a single empty line
    reflowDoc : String -> List (Doc IdrisDocAnn)
    reflowDoc "" = []
    reflowDoc str = map (indent 2 . reflow) (forget $ Extra.lines str)

    showTotal : Name -> Totality -> Doc IdrisDocAnn
    showTotal n tot
        = case isTerminating tot of
               Unchecked => ""
               _ => header "Totality" <++> pretty tot

    getDConDoc : Name -> Core (Doc IdrisDocAnn)
    getDConDoc con
        = do defs <- get Ctxt
             Just def <- lookupCtxtExact con (gamma defs)
                  -- should never happen, since we know that the DCon exists:
                  | Nothing => pure Empty
             syn <- get Syn
             ty <- resugar [] =<< normaliseHoles defs [] (type def)
             let conWithTypeDoc = annotate (Decl con) (hsep [dCon con (prettyName con), colon, prettyTerm ty])
             case lookupName con (defDocstrings syn) of
               [(n, "")] => pure conWithTypeDoc
               [(n, str)] => pure $ vcat
                    [ conWithTypeDoc
                    , annotate DocStringBody
                    $ annotate UserDocString
                    $ vcat $ reflowDoc str
                    ]
               _ => pure conWithTypeDoc

    getImplDoc : Name -> Core (List (Doc IdrisDocAnn))
    getImplDoc n
        = do defs <- get Ctxt
             Just def <- lookupCtxtExact n (gamma defs)
                  | Nothing => pure []
             ty <- resugar [] =<< normaliseHoles defs [] (type def)
             pure [annotate (Decl n) $ prettyTerm ty]

    getMethDoc : Method -> Core (List (Doc IdrisDocAnn))
    getMethDoc meth
        = do syn <- get Syn
             let [nstr] = lookupName meth.name (defDocstrings syn)
                  | _ => pure []
             pure <$> showDoc methodsConfig nstr

    getInfixDoc : Name -> Core (List (Doc IdrisDocAnn))
    getInfixDoc n
        = do let Just (Basic n) = userNameRoot n
                    | _ => pure []
             let Just (fixity, assoc) = S.lookup n (infixes !(get Syn))
                    | Nothing => pure []
             pure $ pure $ hsep
                  [ pretty (show fixity)
                  , "operator,"
                  , "level"
                  , pretty (show assoc)
                  ]

    getPrefixDoc : Name -> Core (List (Doc IdrisDocAnn))
    getPrefixDoc n
        = do let Just (Basic n) = userNameRoot n
                    | _ => pure []
             let Just assoc = S.lookup n (prefixes !(get Syn))
                    | Nothing => pure []
             pure $ ["prefix operator, level" <++> pretty (show assoc)]

    getFixityDoc : Name -> Core (List (Doc IdrisDocAnn))
    getFixityDoc n =
      pure $ case toList !(getInfixDoc n) ++ toList !(getPrefixDoc n) of
        []  => []
        [f] => [header "Fixity Declaration" <++> f]
        fs  => [header "Fixity Declarations" <+> Line <+>
                 indent 2 (vcat fs)]

    getIFaceDoc : (Name, IFaceInfo) -> Core (Doc IdrisDocAnn)
    getIFaceDoc (n, iface)
        = do let params =
                case params iface of
                     [] => []
                     ps => [hsep (header "Parameters" :: punctuate comma (map (pretty . show) ps))]
             let constraints =
                case !(traverse (pterm . map defaultKindedName) (parents iface)) of
                     [] => []
                     ps => [hsep (header "Constraints" :: punctuate comma (map (pretty . show) ps))]
             let icon = case dropNS (iconstructor iface) of
                          DN _ _ => [] -- machine inserted
                          nm => [hsep [header "Constructor", dCon nm (prettyName nm)]]
             mdocs <- traverse getMethDoc (methods iface)
             let meths = case concat mdocs of
                           [] => []
                           docs => [vcat [header "Methods", annotate Declarations $ vcat $ map (indent 2) docs]]
             sd <- getSearchData fc False n
             idocs <- case hintGroups sd of
                           [] => pure (the (List (List (Doc IdrisDocAnn))) [])
                           ((_, tophs) :: _) => traverse getImplDoc tophs
             let insts = case concat idocs of
                           [] => []
                           [doc] => [header "Implementation" <++> annotate Declarations doc]
                           docs => [vcat [header "Implementations"
                                   , annotate Declarations $ vcat $ map (indent 2) docs]]
             pure (vcat (params ++ constraints ++ icon ++ meths ++ insts))

    getFieldDoc : Name -> Core (Doc IdrisDocAnn)
    getFieldDoc nm
      = do syn <- get Syn
           defs <- get Ctxt
           Just def <- lookupCtxtExact nm (gamma defs)
                -- should never happen, since we know that the DCon exists:
                | Nothing => pure Empty
           ty <- resugar [] =<< normaliseHoles defs [] (type def)
           let prettyName = prettyName nm
           let projDecl = annotate (Decl nm) $ hsep [ fun nm prettyName, colon, prettyTerm ty ]
           case lookupName nm (defDocstrings syn) of
                [(_, "")] => pure projDecl
                [(_, str)] =>
                  pure $ vcat [ projDecl
                              , annotate DocStringBody
                              $ annotate UserDocString
                              $ vcat $ reflowDoc str
                              ]
                _ => pure projDecl

    getFieldsDoc : Name -> Core (Maybe (Doc IdrisDocAnn))
    getFieldsDoc recName
      = do let (Just ns, n) = displayName recName
               | _ => pure Nothing
           let recNS = ns <.> mkNamespace n
           defs <- get Ctxt
           let fields = getFieldNames (gamma defs) recNS
           syn <- get Syn
           case fields of
             [] => pure Nothing
             [proj] => pure $ Just $ header "Projection" <++> annotate Declarations !(getFieldDoc proj)
             projs => pure $ Just $ vcat
                           [ header "Projections"
                           , annotate Declarations $ vcat $
                               map (indent 2) $ !(traverse getFieldDoc projs)
                           ]

    getExtra : Name -> GlobalDef -> Core (Maybe String, List (Doc IdrisDocAnn))
    getExtra n d = do
      do syn <- get Syn
         let [] = lookupName n (ifaces syn)
             | [ifacedata] => (Just "interface",) . pure <$> getIFaceDoc ifacedata
             | _ => pure (Nothing, []) -- shouldn't happen, we've resolved ambiguity by now
         case definition d of
           PMDef _ _ _ _ _ => pure (Nothing, [showTotal n (totality d)])
           TCon _ _ _ _ _ _ cons _ =>
             do let tot = [showTotal n (totality d)]
                cdocs <- traverse (getDConDoc <=< toFullNames) cons
                cdoc <- case cdocs of
                  [] => pure (Just "data", [])
                  [doc] =>
                    let cdoc = header "Constructor" <++> annotate Declarations doc in
                    case !(getFieldsDoc n) of
                      Nothing => pure (Just "data", [cdoc])
                      Just fs => pure (Just "record", cdoc :: [fs])
                  docs => pure (Just "data"
                               , [vcat [header "Constructors"
                                       , annotate Declarations $
                                           vcat $ map (indent 2) docs]])
                pure (map (tot ++) cdoc)
           _ => pure (Nothing, [])

    showDoc (MkConfig {longNames, dropFirst, getTotality}) (n, str)
        = do defs <- get Ctxt
             Just def <- lookupCtxtExact n (gamma defs)
                  | Nothing => undefinedName fc n
             -- First get the extra stuff because this also tells us whether a
             -- definition is `data`, `record`, or `interface`.
             (typ, extra) <- ifThenElse getTotality
                               (getExtra n def)
                               (pure (Nothing, []))

             -- Then form the type declaration
             ty <- resugar [] =<< normaliseHoles defs [] (type def)
             -- when printing e.g. interface methods there is no point in
             -- repeating the interface's name
             let ty = ifThenElse (not dropFirst) ty $ case ty of
                        PPi _ _ AutoImplicit _ _ sc => sc
                        _ => ty
             nm <- aliasName n
             -- when printing e.g. interface methods there is no point in
             -- repeating the namespace the interface lives in
             let cat = showCategory Syntax def
             let nm = prettyKindedName typ $ cat
                    $ ifThenElse longNames (pretty (show nm)) (prettyName nm)
             let docDecl = annotate (Decl n) (hsep [nm, colon, prettyTerm ty])

             -- Finally add the user-provided docstring
             let docText = let docs = reflowDoc str in
                           annotate UserDocString (vcat docs)
                           <$ guard (not $ null docs)
             fixes <- getFixityDoc n
             let docBody =
                  let docs = maybe id (::) docText
                           $ map (indent 2) (extra ++ fixes)
                  in annotate DocStringBody
                     (concatWith (\l, r => l <+> hardline <+> r) docs)
                     <$ guard (not (null docs))
             pure (vcat (docDecl :: docBody))

export
getDocsForPTerm : {auto o : Ref ROpts REPLOpts} ->
                  {auto c : Ref Ctxt Defs} ->
                  {auto s : Ref Syn SyntaxInfo} ->
                  PTerm -> Core (Doc IdrisDocAnn)
getDocsForPTerm (PRef fc name) = getDocsForName fc name MkConfig
getDocsForPTerm (PPrimVal _ c) = getDocsForPrimitive c
getDocsForPTerm (PType _) = pure $ vcat
  [ "Type : Type"
  , indent 2 "The type of all types is Type. The type of Type is Type."
  ]
getDocsForPTerm (PString _ _) = pure $ vcat
  [ "String Literal"
  , indent 2 "Desugars to a fromString call"
  ]
getDocsForPTerm (PList _ _ _) = pure $ vcat
  [ "List Literal"
  , indent 2 "Desugars to (::) and Nil"
  ]
getDocsForPTerm (PSnocList _ _ _) = pure $ vcat
  [ "SnocList Literal"
  , indent 2 "Desugars to (:<) and Empty"
  ]
getDocsForPTerm (PPair _ _ _) = pure $ vcat
  [ "Pair Literal"
  , indent 2 "Desugars to MkPair or Pair"
  ]
getDocsForPTerm (PDPair _ _ _ _ _) = pure $ vcat
  [ "Dependant Pair Literal"
  , indent 2 "Desugars to MkDPair or DPair"
  ]
getDocsForPTerm (PUnit _) = pure $ vcat
  [ "Unit Literal"
  , indent 2 "Desugars to MkUnit or Unit"
  ]
getDocsForPTerm pterm = pure $
  "Docs not implemented for" <++> pretty (show pterm) <++> "yet"

summarise : {auto c : Ref Ctxt Defs} ->
            {auto s : Ref Syn SyntaxInfo} ->
            Name -> Core (Doc IdrisDocAnn)
summarise n -- n is fully qualified
    = do syn <- get Syn
         defs <- get Ctxt
         Just def <- lookupCtxtExact n (gamma defs)
             | _ => pure ""
         ty <- normaliseHoles defs [] (type def)
         pure $ showCategory Syntax def (prettyName n)
              <++> colon <++> hang 0 (prettyTerm !(resugar [] ty))

-- Display all the exported names in the given namespace
export
getContents : {auto o : Ref ROpts REPLOpts} ->
              {auto c : Ref Ctxt Defs} ->
              {auto s : Ref Syn SyntaxInfo} ->
              Namespace -> Core (Doc IdrisDocAnn)
getContents ns
   = -- Get all the names, filter by any that match the given namespace
     -- and are visible, then display with their type
     do defs <- get Ctxt
        ns <- allNames (gamma defs)
        let allNs = filter inNS ns
        allNs <- filterM (visible defs) allNs
        vsep <$> traverse summarise (sort allNs)
  where
    visible : Defs -> Name -> Core Bool
    visible defs n
        = do Just def <- lookupCtxtExact n (gamma defs)
                  | Nothing => pure False
             pure (visibility def /= Private)

    inNS : Name -> Bool
    inNS (NS xns (UN _)) = ns `isParentOf` xns
    inNS _ = False


text:
module Backprop.CanBack

import Data.Vect

||| an interface used for manipulating gradient values of type `a` when backpropagating
public export
interface CanBack a where
  ||| representation of 1
  one : a
  ||| representation of 0
  zero : a
  ||| addition
  add : a -> a -> a

export
CanBack Double where
  one = 1
  zero = 0
  add = (+)


text:
import System

testTime : IO ()
testTime = do timeValue <- time
              putStrLn (show (mod timeValue 100))

testRepl : IO ()
testRepl = repl "Put string: " (\x => "Input string was: " ++ show x)