text:
module Web.Raw.IndexedDB

import JS
import Web.Internal.IndexedDBPrim
import Web.Internal.Types

%default total

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

namespace IDBCursor

  export
  direction :  (0 _ : JSType t1)
            => {auto 0 _ : Elem IDBCursor (Types t1)}
            -> (obj : t1)
            -> JSIO IDBCursorDirection
  direction a = tryJS "IDBCursor.direction" $ IDBCursor.prim__direction (up a)

  export
  key :  (0 _ : JSType t1)
      => {auto 0 _ : Elem IDBCursor (Types t1)}
      -> (obj : t1)
      -> JSIO Any
  key a = tryJS "IDBCursor.key" $ IDBCursor.prim__key (up a)

  export
  primaryKey :  (0 _ : JSType t1)
             => {auto 0 _ : Elem IDBCursor (Types t1)}
             -> (obj : t1)
             -> JSIO Any
  primaryKey a = tryJS "IDBCursor.primaryKey"
               $ IDBCursor.prim__primaryKey (up a)

  export
  request :  (0 _ : JSType t1)
          => {auto 0 _ : Elem IDBCursor (Types t1)}
          -> (obj : t1)
          -> JSIO IDBRequest
  request a = primJS $ IDBCursor.prim__request (up a)

  export
  source :  (0 _ : JSType t1)
         => {auto 0 _ : Elem IDBCursor (Types t1)}
         -> (obj : t1)
         -> JSIO (NS I [ IDBObjectStore , IDBIndex ])
  source a = tryJS "IDBCursor.source" $ IDBCursor.prim__source (up a)

  export
  advance :  (0 _ : JSType t1)
          => {auto 0 _ : Elem IDBCursor (Types t1)}
          -> (obj : t1)
          -> (count : Bits32)
          -> JSIO ()
  advance a b = primJS $ IDBCursor.prim__advance (up a) b

  export
  continue :  (0 _ : JSType t1)
           => {auto 0 _ : Elem IDBCursor (Types t1)}
           -> (obj : t1)
           -> (key : Optional Any)
           -> JSIO ()
  continue a b = primJS $ IDBCursor.prim__continue (up a) (toFFI b)

  export
  continue' :  (0 _ : JSType t1)
            => {auto 0 _ : Elem IDBCursor (Types t1)}
            -> (obj : t1)
            -> JSIO ()
  continue' a = primJS $ IDBCursor.prim__continue (up a) undef

  export
  continuePrimaryKey :  (0 _ : JSType t1)
                     => {auto 0 _ : Elem IDBCursor (Types t1)}
                     -> (obj : t1)
                     -> (key : Any)
                     -> (primaryKey : Any)
                     -> JSIO ()
  continuePrimaryKey a b c = primJS
                           $ IDBCursor.prim__continuePrimaryKey (up a)
                                                                (toFFI b)
                                                                (toFFI c)

  export
  delete :  (0 _ : JSType t1)
         => {auto 0 _ : Elem IDBCursor (Types t1)}
         -> (obj : t1)
         -> JSIO IDBRequest
  delete a = primJS $ IDBCursor.prim__delete (up a)

  export
  update :  (0 _ : JSType t1)
         => {auto 0 _ : Elem IDBCursor (Types t1)}
         -> (obj : t1)
         -> (value : Any)
         -> JSIO IDBRequest
  update a b = primJS $ IDBCursor.prim__update (up a) (toFFI b)

namespace IDBCursorWithValue

  export
  value : (obj : IDBCursorWithValue) -> JSIO Any
  value a = tryJS "IDBCursorWithValue.value" $ IDBCursorWithValue.prim__value a

namespace IDBDatabase

  export
  name : (obj : IDBDatabase) -> JSIO String
  name a = primJS $ IDBDatabase.prim__name a

  export
  objectStoreNames : (obj : IDBDatabase) -> JSIO DOMStringList
  objectStoreNames a = primJS $ IDBDatabase.prim__objectStoreNames a

  export
  onabort : IDBDatabase -> Attribute False Maybe EventHandlerNonNull
  onabort v = fromNullablePrim "IDBDatabase.getonabort"
                               prim__onabort
                               prim__setOnabort
                               v

  export
  onclose : IDBDatabase -> Attribute False Maybe EventHandlerNonNull
  onclose v = fromNullablePrim "IDBDatabase.getonclose"
                               prim__onclose
                               prim__setOnclose
                               v

  export
  onerror : IDBDatabase -> Attribute False Maybe EventHandlerNonNull
  onerror v = fromNullablePrim "IDBDatabase.getonerror"
                               prim__onerror
                               prim__setOnerror
                               v

  export
  onversionchange : IDBDatabase -> Attribute False Maybe EventHandlerNonNull
  onversionchange v = fromNullablePrim "IDBDatabase.getonversionchange"
                                       prim__onversionchange
                                       prim__setOnversionchange
                                       v

  export
  version : (obj : IDBDatabase) -> JSIO JSBits64
  version a = primJS $ IDBDatabase.prim__version a

  export
  close : (obj : IDBDatabase) -> JSIO ()
  close a = primJS $ IDBDatabase.prim__close a

  export
  createObjectStore :  (0 _ : JSType t1)
                    => {auto 0 _ : Elem IDBObjectStoreParameters (Types t1)}
                    -> (obj : IDBDatabase)
                    -> (name : String)
                    -> (options : Optional t1)
                    -> JSIO IDBObjectStore
  createObjectStore a b c = primJS
                          $ IDBDatabase.prim__createObjectStore a b (optUp c)

  export
  createObjectStore' :  (obj : IDBDatabase)
                     -> (name : String)
                     -> JSIO IDBObjectStore
  createObjectStore' a b = primJS
                         $ IDBDatabase.prim__createObjectStore a b undef

  export
  deleteObjectStore : (obj : IDBDatabase) -> (name : String) -> JSIO ()
  deleteObjectStore a b = primJS $ IDBDatabase.prim__deleteObjectStore a b

  export
  transaction :  (0 _ : JSType t1)
              => {auto 0 _ : Elem IDBTransactionOptions (Types t1)}
              -> (obj : IDBDatabase)
              -> (storeNames : NS I [ String , Array String ])
              -> (mode : Optional IDBTransactionMode)
              -> (options : Optional t1)
              -> JSIO IDBTransaction
  transaction a b c d = primJS
                      $ IDBDatabase.prim__transaction a
                                                      (toFFI b)
                                                      (toFFI c)
                                                      (optUp d)

  export
  transaction' :  (obj : IDBDatabase)
               -> (storeNames : NS I [ String , Array String ])
               -> JSIO IDBTransaction
  transaction' a b = primJS
                   $ IDBDatabase.prim__transaction a (toFFI b) undef undef

namespace IDBFactory

  export
  cmp : (obj : IDBFactory) -> (first : Any) -> (second : Any) -> JSIO Int16
  cmp a b c = primJS $ IDBFactory.prim__cmp a (toFFI b) (toFFI c)

  export
  databases : (obj : IDBFactory) -> JSIO (Promise (Array IDBDatabaseInfo))
  databases a = primJS $ IDBFactory.prim__databases a

  export
  deleteDatabase :  (obj : IDBFactory)
                 -> (name : String)
                 -> JSIO IDBOpenDBRequest
  deleteDatabase a b = primJS $ IDBFactory.prim__deleteDatabase a b

  export
  open_ :  (obj : IDBFactory)
        -> (name : String)
        -> (version : Optional JSBits64)
        -> JSIO IDBOpenDBRequest
  open_ a b c = primJS $ IDBFactory.prim__open a b (toFFI c)

  export
  open' : (obj : IDBFactory) -> (name : String) -> JSIO IDBOpenDBRequest
  open' a b = primJS $ IDBFactory.prim__open a b undef

namespace IDBIndex

  export
  keyPath : (obj : IDBIndex) -> JSIO Any
  keyPath a = tryJS "IDBIndex.keyPath" $ IDBIndex.prim__keyPath a

  export
  multiEntry : (obj : IDBIndex) -> JSIO Bool
  multiEntry a = tryJS "IDBIndex.multiEntry" $ IDBIndex.prim__multiEntry a

  export
  name : IDBIndex -> Attribute True I String
  name v = fromPrim "IDBIndex.getname" prim__name prim__setName v

  export
  objectStore : (obj : IDBIndex) -> JSIO IDBObjectStore
  objectStore a = primJS $ IDBIndex.prim__objectStore a

  export
  unique : (obj : IDBIndex) -> JSIO Bool
  unique a = tryJS "IDBIndex.unique" $ IDBIndex.prim__unique a

  export
  count : (obj : IDBIndex) -> (query : Optional Any) -> JSIO IDBRequest
  count a b = primJS $ IDBIndex.prim__count a (toFFI b)

  export
  count' : (obj : IDBIndex) -> JSIO IDBRequest
  count' a = primJS $ IDBIndex.prim__count a undef

  export
  getAll :  (obj : IDBIndex)
         -> (query : Optional Any)
         -> (count : Optional Bits32)
         -> JSIO IDBRequest
  getAll a b c = primJS $ IDBIndex.prim__getAll a (toFFI b) (toFFI c)

  export
  getAll' : (obj : IDBIndex) -> JSIO IDBRequest
  getAll' a = primJS $ IDBIndex.prim__getAll a undef undef

  export
  getAllKeys :  (obj : IDBIndex)
             -> (query : Optional Any)
             -> (count : Optional Bits32)
             -> JSIO IDBRequest
  getAllKeys a b c = primJS $ IDBIndex.prim__getAllKeys a (toFFI b) (toFFI c)

  export
  getAllKeys' : (obj : IDBIndex) -> JSIO IDBRequest
  getAllKeys' a = primJS $ IDBIndex.prim__getAllKeys a undef undef

  export
  get : (obj : IDBIndex) -> (query : Any) -> JSIO IDBRequest
  get a b = primJS $ IDBIndex.prim__get a (toFFI b)

  export
  getKey : (obj : IDBIndex) -> (query : Any) -> JSIO IDBRequest
  getKey a b = primJS $ IDBIndex.prim__getKey a (toFFI b)

  export
  openCursor :  (obj : IDBIndex)
             -> (query : Optional Any)
             -> (direction : Optional IDBCursorDirection)
             -> JSIO IDBRequest
  openCursor a b c = primJS $ IDBIndex.prim__openCursor a (toFFI b) (toFFI c)

  export
  openCursor' : (obj : IDBIndex) -> JSIO IDBRequest
  openCursor' a = primJS $ IDBIndex.prim__openCursor a undef undef

  export
  openKeyCursor :  (obj : IDBIndex)
                -> (query : Optional Any)
                -> (direction : Optional IDBCursorDirection)
                -> JSIO IDBRequest
  openKeyCursor a b c = primJS
                      $ IDBIndex.prim__openKeyCursor a (toFFI b) (toFFI c)

  export
  openKeyCursor' : (obj : IDBIndex) -> JSIO IDBRequest
  openKeyCursor' a = primJS $ IDBIndex.prim__openKeyCursor a undef undef

namespace IDBKeyRange

  export
  bound :  (lower : Any)
        -> (upper : Any)
        -> (lowerOpen : Optional Bool)
        -> (upperOpen : Optional Bool)
        -> JSIO IDBKeyRange
  bound a b c d = primJS
                $ IDBKeyRange.prim__bound (toFFI a)
                                          (toFFI b)
                                          (toFFI c)
                                          (toFFI d)

  export
  bound' : (lower : Any) -> (upper : Any) -> JSIO IDBKeyRange
  bound' a b = primJS $ IDBKeyRange.prim__bound (toFFI a) (toFFI b) undef undef

  export
  lowerBound : (lower : Any) -> (open_ : Optional Bool) -> JSIO IDBKeyRange
  lowerBound a b = primJS $ IDBKeyRange.prim__lowerBound (toFFI a) (toFFI b)

  export
  lowerBound' : (lower : Any) -> JSIO IDBKeyRange
  lowerBound' a = primJS $ IDBKeyRange.prim__lowerBound (toFFI a) undef

  export
  only : (value : Any) -> JSIO IDBKeyRange
  only a = primJS $ IDBKeyRange.prim__only (toFFI a)

  export
  upperBound : (upper : Any) -> (open_ : Optional Bool) -> JSIO IDBKeyRange
  upperBound a b = primJS $ IDBKeyRange.prim__upperBound (toFFI a) (toFFI b)

  export
  upperBound' : (upper : Any) -> JSIO IDBKeyRange
  upperBound' a = primJS $ IDBKeyRange.prim__upperBound (toFFI a) undef

  export
  lower : (obj : IDBKeyRange) -> JSIO Any
  lower a = tryJS "IDBKeyRange.lower" $ IDBKeyRange.prim__lower a

  export
  lowerOpen : (obj : IDBKeyRange) -> JSIO Bool
  lowerOpen a = tryJS "IDBKeyRange.lowerOpen" $ IDBKeyRange.prim__lowerOpen a

  export
  upper : (obj : IDBKeyRange) -> JSIO Any
  upper a = tryJS "IDBKeyRange.upper" $ IDBKeyRange.prim__upper a

  export
  upperOpen : (obj : IDBKeyRange) -> JSIO Bool
  upperOpen a = tryJS "IDBKeyRange.upperOpen" $ IDBKeyRange.prim__upperOpen a

  export
  includes : (obj : IDBKeyRange) -> (key : Any) -> JSIO Bool
  includes a b = tryJS "IDBKeyRange.includes"
               $ IDBKeyRange.prim__includes a (toFFI b)

namespace IDBObjectStore

  export
  autoIncrement : (obj : IDBObjectStore) -> JSIO Bool
  autoIncrement a = tryJS "IDBObjectStore.autoIncrement"
                  $ IDBObjectStore.prim__autoIncrement a

  export
  indexNames : (obj : IDBObjectStore) -> JSIO DOMStringList
  indexNames a = primJS $ IDBObjectStore.prim__indexNames a

  export
  keyPath : (obj : IDBObjectStore) -> JSIO Any
  keyPath a = tryJS "IDBObjectStore.keyPath" $ IDBObjectStore.prim__keyPath a

  export
  name : IDBObjectStore -> Attribute True I String
  name v = fromPrim "IDBObjectStore.getname" prim__name prim__setName v

  export
  transaction : (obj : IDBObjectStore) -> JSIO IDBTransaction
  transaction a = primJS $ IDBObjectStore.prim__transaction a

  export
  add :  (obj : IDBObjectStore)
      -> (value : Any)
      -> (key : Optional Any)
      -> JSIO IDBRequest
  add a b c = primJS $ IDBObjectStore.prim__add a (toFFI b) (toFFI c)

  export
  add' : (obj : IDBObjectStore) -> (value : Any) -> JSIO IDBRequest
  add' a b = primJS $ IDBObjectStore.prim__add a (toFFI b) undef

  export
  clear : (obj : IDBObjectStore) -> JSIO IDBRequest
  clear a = primJS $ IDBObjectStore.prim__clear a

  export
  count : (obj : IDBObjectStore) -> (query : Optional Any) -> JSIO IDBRequest
  count a b = primJS $ IDBObjectStore.prim__count a (toFFI b)

  export
  count' : (obj : IDBObjectStore) -> JSIO IDBRequest
  count' a = primJS $ IDBObjectStore.prim__count a undef

  export
  createIndex :  (0 _ : JSType t1)
              => {auto 0 _ : Elem IDBIndexParameters (Types t1)}
              -> (obj : IDBObjectStore)
              -> (name : String)
              -> (keyPath : NS I [ String , Array String ])
              -> (options : Optional t1)
              -> JSIO IDBIndex
  createIndex a b c d = primJS
                      $ IDBObjectStore.prim__createIndex a b (toFFI c) (optUp d)

  export
  createIndex' :  (obj : IDBObjectStore)
               -> (name : String)
               -> (keyPath : NS I [ String , Array String ])
               -> JSIO IDBIndex
  createIndex' a b c = primJS
                     $ IDBObjectStore.prim__createIndex a b (toFFI c) undef

  export
  delete : (obj : IDBObjectStore) -> (query : Any) -> JSIO IDBRequest
  delete a b = primJS $ IDBObjectStore.prim__delete a (toFFI b)

  export
  deleteIndex : (obj : IDBObjectStore) -> (name : String) -> JSIO ()
  deleteIndex a b = primJS $ IDBObjectStore.prim__deleteIndex a b

  export
  getAll :  (obj : IDBObjectStore)
         -> (query : Optional Any)
         -> (count : Optional Bits32)
         -> JSIO IDBRequest
  getAll a b c = primJS $ IDBObjectStore.prim__getAll a (toFFI b) (toFFI c)

  export
  getAll' : (obj : IDBObjectStore) -> JSIO IDBRequest
  getAll' a = primJS $ IDBObjectStore.prim__getAll a undef undef

  export
  getAllKeys :  (obj : IDBObjectStore)
             -> (query : Optional Any)
             -> (count : Optional Bits32)
             -> JSIO IDBRequest
  getAllKeys a b c = primJS
                   $ IDBObjectStore.prim__getAllKeys a (toFFI b) (toFFI c)

  export
  getAllKeys' : (obj : IDBObjectStore) -> JSIO IDBRequest
  getAllKeys' a = primJS $ IDBObjectStore.prim__getAllKeys a undef undef

  export
  get : (obj : IDBObjectStore) -> (query : Any) -> JSIO IDBRequest
  get a b = primJS $ IDBObjectStore.prim__get a (toFFI b)

  export
  getKey : (obj : IDBObjectStore) -> (query : Any) -> JSIO IDBRequest
  getKey a b = primJS $ IDBObjectStore.prim__getKey a (toFFI b)

  export
  index : (obj : IDBObjectStore) -> (name : String) -> JSIO IDBIndex
  index a b = primJS $ IDBObjectStore.prim__index a b

  export
  openCursor :  (obj : IDBObjectStore)
             -> (query : Optional Any)
             -> (direction : Optional IDBCursorDirection)
             -> JSIO IDBRequest
  openCursor a b c = primJS
                   $ IDBObjectStore.prim__openCursor a (toFFI b) (toFFI c)

  export
  openCursor' : (obj : IDBObjectStore) -> JSIO IDBRequest
  openCursor' a = primJS $ IDBObjectStore.prim__openCursor a undef undef

  export
  openKeyCursor :  (obj : IDBObjectStore)
                -> (query : Optional Any)
                -> (direction : Optional IDBCursorDirection)
                -> JSIO IDBRequest
  openKeyCursor a b c = primJS
                      $ IDBObjectStore.prim__openKeyCursor a (toFFI b) (toFFI c)

  export
  openKeyCursor' : (obj : IDBObjectStore) -> JSIO IDBRequest
  openKeyCursor' a = primJS $ IDBObjectStore.prim__openKeyCursor a undef undef

  export
  put :  (obj : IDBObjectStore)
      -> (value : Any)
      -> (key : Optional Any)
      -> JSIO IDBRequest
  put a b c = primJS $ IDBObjectStore.prim__put a (toFFI b) (toFFI c)

  export
  put' : (obj : IDBObjectStore) -> (value : Any) -> JSIO IDBRequest
  put' a b = primJS $ IDBObjectStore.prim__put a (toFFI b) undef

namespace IDBOpenDBRequest

  export
  onblocked : IDBOpenDBRequest -> Attribute False Maybe EventHandlerNonNull
  onblocked v = fromNullablePrim "IDBOpenDBRequest.getonblocked"
                                 prim__onblocked
                                 prim__setOnblocked
                                 v

  export
  onupgradeneeded :  IDBOpenDBRequest
                  -> Attribute False Maybe EventHandlerNonNull
  onupgradeneeded v = fromNullablePrim "IDBOpenDBRequest.getonupgradeneeded"
                                       prim__onupgradeneeded
                                       prim__setOnupgradeneeded
                                       v

namespace IDBRequest

  export
  error :  (0 _ : JSType t1)
        => {auto 0 _ : Elem IDBRequest (Types t1)}
        -> (obj : t1)
        -> JSIO (Maybe DOMException)
  error a = tryJS "IDBRequest.error" $ IDBRequest.prim__error (up a)

  export
  onerror :  (0 _ : JSType t)
          => {auto 0 _ : Elem IDBRequest (Types t)}
          -> t
          -> Attribute False Maybe EventHandlerNonNull
  onerror v = fromNullablePrim "IDBRequest.getonerror"
                               prim__onerror
                               prim__setOnerror
                               (v :> IDBRequest)

  export
  onsuccess :  (0 _ : JSType t)
            => {auto 0 _ : Elem IDBRequest (Types t)}
            -> t
            -> Attribute False Maybe EventHandlerNonNull
  onsuccess v = fromNullablePrim "IDBRequest.getonsuccess"
                                 prim__onsuccess
                                 prim__setOnsuccess
                                 (v :> IDBRequest)

  export
  readyState :  (0 _ : JSType t1)
             => {auto 0 _ : Elem IDBRequest (Types t1)}
             -> (obj : t1)
             -> JSIO IDBRequestReadyState
  readyState a = tryJS "IDBRequest.readyState"
               $ IDBRequest.prim__readyState (up a)

  export
  result :  (0 _ : JSType t1)
         => {auto 0 _ : Elem IDBRequest (Types t1)}
         -> (obj : t1)
         -> JSIO Any
  result a = tryJS "IDBRequest.result" $ IDBRequest.prim__result (up a)

  export
  source :  (0 _ : JSType t1)
         => {auto 0 _ : Elem IDBRequest (Types t1)}
         -> (obj : t1)
         -> JSIO (Maybe (NS I [ IDBObjectStore , IDBIndex , IDBCursor ]))
  source a = tryJS "IDBRequest.source" $ IDBRequest.prim__source (up a)

  export
  transaction :  (0 _ : JSType t1)
              => {auto 0 _ : Elem IDBRequest (Types t1)}
              -> (obj : t1)
              -> JSIO (Maybe IDBTransaction)
  transaction a = tryJS "IDBRequest.transaction"
                $ IDBRequest.prim__transaction (up a)

namespace IDBTransaction

  export
  db : (obj : IDBTransaction) -> JSIO IDBDatabase
  db a = primJS $ IDBTransaction.prim__db a

  export
  durability : (obj : IDBTransaction) -> JSIO IDBTransactionDurability
  durability a = tryJS "IDBTransaction.durability"
               $ IDBTransaction.prim__durability a

  export
  error : (obj : IDBTransaction) -> JSIO (Maybe DOMException)
  error a = tryJS "IDBTransaction.error" $ IDBTransaction.prim__error a

  export
  mode : (obj : IDBTransaction) -> JSIO IDBTransactionMode
  mode a = tryJS "IDBTransaction.mode" $ IDBTransaction.prim__mode a

  export
  objectStoreNames : (obj : IDBTransaction) -> JSIO DOMStringList
  objectStoreNames a = primJS $ IDBTransaction.prim__objectStoreNames a

  export
  onabort : IDBTransaction -> Attribute False Maybe EventHandlerNonNull
  onabort v = fromNullablePrim "IDBTransaction.getonabort"
                               prim__onabort
                               prim__setOnabort
                               v

  export
  oncomplete : IDBTransaction -> Attribute False Maybe EventHandlerNonNull
  oncomplete v = fromNullablePrim "IDBTransaction.getoncomplete"
                                  prim__oncomplete
                                  prim__setOncomplete
                                  v

  export
  onerror : IDBTransaction -> Attribute False Maybe EventHandlerNonNull
  onerror v = fromNullablePrim "IDBTransaction.getonerror"
                               prim__onerror
                               prim__setOnerror
                               v

  export
  abort : (obj : IDBTransaction) -> JSIO ()
  abort a = primJS $ IDBTransaction.prim__abort a

  export
  commit : (obj : IDBTransaction) -> JSIO ()
  commit a = primJS $ IDBTransaction.prim__commit a

  export
  objectStore : (obj : IDBTransaction) -> (name : String) -> JSIO IDBObjectStore
  objectStore a b = primJS $ IDBTransaction.prim__objectStore a b

namespace IDBVersionChangeEvent

  export
  new :  (0 _ : JSType t1)
      => {auto 0 _ : Elem IDBVersionChangeEventInit (Types t1)}
      -> (type : String)
      -> (eventInitDict : Optional t1)
      -> JSIO IDBVersionChangeEvent
  new a b = primJS $ IDBVersionChangeEvent.prim__new a (optUp b)

  export
  new' : (type : String) -> JSIO IDBVersionChangeEvent
  new' a = primJS $ IDBVersionChangeEvent.prim__new a undef

  export
  newVersion : (obj : IDBVersionChangeEvent) -> JSIO (Maybe JSBits64)
  newVersion a = tryJS "IDBVersionChangeEvent.newVersion"
               $ IDBVersionChangeEvent.prim__newVersion a

  export
  oldVersion : (obj : IDBVersionChangeEvent) -> JSIO JSBits64
  oldVersion a = primJS $ IDBVersionChangeEvent.prim__oldVersion a

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

namespace IDBDatabaseInfo

  export
  new :  (name : Optional String)
      -> (version : Optional JSBits64)
      -> JSIO IDBDatabaseInfo
  new a b = primJS $ IDBDatabaseInfo.prim__new (toFFI a) (toFFI b)

  export
  new' : JSIO IDBDatabaseInfo
  new' = primJS $ IDBDatabaseInfo.prim__new undef undef

  export
  name :  (0 _ : JSType t)
       => {auto 0 _ : Elem IDBDatabaseInfo (Types t)}
       -> t
       -> Attribute False Optional String
  name v = fromUndefOrPrimNoDefault "IDBDatabaseInfo.getname"
                                    prim__name
                                    prim__setName
                                    (v :> IDBDatabaseInfo)

  export
  version :  (0 _ : JSType t)
          => {auto 0 _ : Elem IDBDatabaseInfo (Types t)}
          -> t
          -> Attribute False Optional JSBits64
  version v = fromUndefOrPrimNoDefault "IDBDatabaseInfo.getversion"
                                       prim__version
                                       prim__setVersion
                                       (v :> IDBDatabaseInfo)

namespace IDBIndexParameters

  export
  new :  (unique : Optional Bool)
      -> (multiEntry : Optional Bool)
      -> JSIO IDBIndexParameters
  new a b = primJS $ IDBIndexParameters.prim__new (toFFI a) (toFFI b)

  export
  new' : JSIO IDBIndexParameters
  new' = primJS $ IDBIndexParameters.prim__new undef undef

  export
  multiEntry :  (0 _ : JSType t)
             => {auto 0 _ : Elem IDBIndexParameters (Types t)}
             -> t
             -> Attribute True Optional Bool
  multiEntry v = fromUndefOrPrim "IDBIndexParameters.getmultiEntry"
                                 prim__multiEntry
                                 prim__setMultiEntry
                                 False
                                 (v :> IDBIndexParameters)

  export
  unique :  (0 _ : JSType t)
         => {auto 0 _ : Elem IDBIndexParameters (Types t)}
         -> t
         -> Attribute True Optional Bool
  unique v = fromUndefOrPrim "IDBIndexParameters.getunique"
                             prim__unique
                             prim__setUnique
                             False
                             (v :> IDBIndexParameters)

namespace IDBObjectStoreParameters

  export
  new :  (keyPath : Optional (Maybe (NS I [ String , Array String ])))
      -> (autoIncrement : Optional Bool)
      -> JSIO IDBObjectStoreParameters
  new a b = primJS $ IDBObjectStoreParameters.prim__new (toFFI a) (toFFI b)

  export
  new' : JSIO IDBObjectStoreParameters
  new' = primJS $ IDBObjectStoreParameters.prim__new undef undef

  export
  autoIncrement :  (0 _ : JSType t)
                => {auto 0 _ : Elem IDBObjectStoreParameters (Types t)}
                -> t
                -> Attribute True Optional Bool
  autoIncrement v = fromUndefOrPrim "IDBObjectStoreParameters.getautoIncrement"
                                    prim__autoIncrement
                                    prim__setAutoIncrement
                                    False
                                    (v :> IDBObjectStoreParameters)

  export
  keyPath :  (0 _ : JSType t)
          => {auto 0 _ : Elem IDBObjectStoreParameters (Types t)}
          -> t
          -> Attribute True Optional (Maybe (Union2 String (Array String)))
  keyPath v = fromUndefOrPrim "IDBObjectStoreParameters.getkeyPath"
                              prim__keyPath
                              prim__setKeyPath
                              Nothing
                              (v :> IDBObjectStoreParameters)

namespace IDBTransactionOptions

  export
  new :  (durability : Optional IDBTransactionDurability)
      -> JSIO IDBTransactionOptions
  new a = primJS $ IDBTransactionOptions.prim__new (toFFI a)

  export
  new' : JSIO IDBTransactionOptions
  new' = primJS $ IDBTransactionOptions.prim__new undef

  export
  durability :  (0 _ : JSType t)
             => {auto 0 _ : Elem IDBTransactionOptions (Types t)}
             -> t
             -> Attribute False Optional IDBTransactionDurability
  durability v = fromUndefOrPrimNoDefault "IDBTransactionOptions.getdurability"
                                          prim__durability
                                          prim__setDurability
                                          (v :> IDBTransactionOptions)

namespace IDBVersionChangeEventInit

  export
  new :  (oldVersion : Optional JSBits64)
      -> (newVersion : Optional (Maybe JSBits64))
      -> JSIO IDBVersionChangeEventInit
  new a b = primJS $ IDBVersionChangeEventInit.prim__new (toFFI a) (toFFI b)

  export
  new' : JSIO IDBVersionChangeEventInit
  new' = primJS $ IDBVersionChangeEventInit.prim__new undef undef

  export
  newVersion :  (0 _ : JSType t)
             => {auto 0 _ : Elem IDBVersionChangeEventInit (Types t)}
             -> t
             -> Attribute True Optional (Maybe JSBits64)
  newVersion v = fromUndefOrPrim "IDBVersionChangeEventInit.getnewVersion"
                                 prim__newVersion
                                 prim__setNewVersion
                                 Nothing
                                 (v :> IDBVersionChangeEventInit)

  export
  oldVersion :  (0 _ : JSType t)
             => {auto 0 _ : Elem IDBVersionChangeEventInit (Types t)}
             -> t
             -> Attribute True Optional JSBits64
  oldVersion v = fromUndefOrPrim "IDBVersionChangeEventInit.getoldVersion"
                                 prim__oldVersion
                                 prim__setOldVersion
                                 0
                                 (v :> IDBVersionChangeEventInit)


text:
import Data.Fin

fsprf : x === y -> FS x = FS y
fsprf p = cong _ p

ext: idr


text:
module Compiler.Erlang.ModuleOpts

import Data.List
import Data.Strings
import Core.Name
import Compiler.Erlang.Name

%default total

public export
record ModuleOpts where
  constructor MkModuleOpts
  ns : Namespace
  exportFunName : Maybe Name
  inlineSize : Maybe Nat

defaultModuleOpts : Namespace -> ModuleOpts
defaultModuleOpts ns = MkModuleOpts ns Nothing Nothing

data Flag
  = SetExportFunName String
  | SetInlineSize Nat

flagToOpts : Flag -> ModuleOpts -> ModuleOpts
flagToOpts (SetExportFunName exportFunName) opts = record { exportFunName = Just (NS (ns opts) (UN exportFunName)) } opts
flagToOpts (SetInlineSize inlineSize) opts = record { inlineSize = Just inlineSize } opts

flagsToOpts : Namespace -> List Flag -> ModuleOpts
flagsToOpts ns flags = flagsToOpts' flags (defaultModuleOpts ns)
  where
    flagsToOpts' : List Flag -> ModuleOpts -> ModuleOpts
    flagsToOpts' [] opts = opts
    flagsToOpts' (flag :: flags) opts = flagsToOpts' flags (flagToOpts flag opts)

stringToFlags : List String -> List Flag
stringToFlags ds = mapMaybe parseFlag (map (\d => assert_total (words d)) ds) -- TODO: Remove `assert_total` when `words` is total
  where
    parseFlag : List String -> Maybe Flag
    parseFlag ["export", exportFunName] = Just $ SetExportFunName exportFunName
    parseFlag ["inline", inlineSize] = Just $ SetInlineSize (integerToNat (cast inlineSize))
    parseFlag _ = Nothing

export
parseModuleOpts : Namespace -> List String -> ModuleOpts
parseModuleOpts ns str = flagsToOpts ns (stringToFlags str)


text:
-- ------------------------------------------------------------- [ Parsing.idr ]
-- Module      : UML.Utils.Parsing
-- Description : Parsing utilities.
-- Copyright   : (c) Jan de Muijnck-Hughes
-- License     : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module UML.Utils.Parsing

import Lightyear.Core
import Lightyear.Combinators
import Lightyear.Strings

%access public

||| An identifier parser.
|||
||| Identifiers must satisfy the form:
|||
|||    `[[:alpha:]\|[:digit:]]+`
|||
||| TODO: Allow select punctuation to be included.
||| TODO: Leading character must be `[:alpha:]`
ident : Parser String
ident = map pack (some $ satisfy isAlphaNum)

||| Implementation of a `manyTill` parser combinator.
|||
||| Inspired by parsec's `manyTill` combinator.
manyTill : Monad m => ParserT m str a -> ParserT m str b -> ParserT m str (List a)
manyTill p end = scan
  where
    scan = do { end; return List.Nil } <|>
           do { x <- p; xs <- scan; return (x::xs)}

||| A literally between parser combinator.
|||
||| Will parse anything between a pair of given character.
|||
||| @c The deliminator.
literallyBetween : (c : Char) -> Parser String
literallyBetween c = map pack $ between (char c) (char c) (some (satisfy (/= c)))

||| End of Line Parser
eol : Parser ()
eol = char '\n' *> return ()

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

max_stars_repo_name: jfdm/idris-uml

max_issues_repo_name: jfdm/idris-uml

max_forks_repo_name: jfdm/idris-uml


text:
module Step

-- Relation 'Step' for reducing terms
-- in the simply-typed lambda calculus.

import Term
import Subst

%default total
%access public export

-------------------------------------------------------------------------
-- Begin: SMALL-STEP EVALUATION RELATION FOR TERMS IN THE LAMBDA CALCULUS

-- The relation 'Step' defines evaluation of terms in the lambda
-- calculus following small-step semantics. 'Step' relates two
-- terms 'x' and 'y' precisely when 'x' can be rewritten into 'y'
-- in a single step of evaluation.
--
-- (Note that the arguments 'x' and 'y' to the type constructor 'Step'
-- are named only for the purpose of easing documentation.)
--
-- Note that the 'Step' relation automatically enforces preservation
-- since the arguments 'x' and 'y' are required to have the same type 't'.
data Step : (x : Term [] t) -> (y : Term [] t) -> Type where
  StApp1     : Step t1 t1' ->
               Step (TApp t1 t2) (TApp t1' t2)
  --
  StApp2     : Value v -> Step t2 t2' ->
               Step (TApp v t2) (TApp v t2')
  --
  StBeta     : Value v ->
               Step (TApp (TAbs t) v) (subst v First t)
  --
  StFix      : Step t t' ->
               Step (TFix t) (TFix t')
  --
  StFixBeta  : Step (TFix (TAbs t)) (subst (TFix (TAbs t)) First t)
  --
  StSucc     : Step t t' ->
               Step (TSucc t) (TSucc t')
  --
  StPred     : Step t t' ->
               Step (TPred t) (TPred t')
  --
  StPredZero : Step (TPred TZero) TZero
  --
  StPredSucc : Value v ->
               Step (TPred (TSucc v)) v
  --
  StIfz      : Step t1 t1' ->
               Step (TIfz t1 t2 t3) (TIfz t1' t2 t3)
  --
  StIfzZero  : Step (TIfz TZero t1 t2) t1
  --
  StIfzSucc  : Value v ->
               Step (TIfz (TSucc v) t1 t2) t2

-- End: SMALL-STEP EVALUATION RELATION FOR TERMS IN THE LAMBDA CALCULUS
-----------------------------------------------------------------------

----------------------------
-- Begin: TRANSITIVE CLOSURE

-- Data type for representing the transistive closure
-- of an arbitrary relation 'rel : a -> a -> Type'.
using (a : Type, rel : a -> a -> Type)
  data TransCl : {a : Type} -> (a -> a -> Type) -> (a -> a -> Type) where
    TClRefl   : (x : a) -> TransCl rel x x
    TClSingle : rel x y  -> TransCl rel x y
    TClTrans  : TransCl rel x y -> TransCl rel y z -> TransCl rel x z

-- Data type specifically for representing the
-- transitive closure of the 'Step' relation.
data TransStep : Term [] t -> Term [] t -> Type where
   TStRefl   : (e : Term [] t) -> TransStep e e
   TStTrans  : {e : Term [] t} -> {e' : Term [] t} -> {e'' : Term [] t} ->
               Step e e' -> TransStep e' e'' -> TransStep e e''

-- 'TransStep' is indeed transitive.
transStepTransitive : TransStep e1 e2 -> TransStep e2 e3 -> TransStep e1 e3
transStepTransitive (TStRefl _) y    = y
transStepTransitive (TStTrans x y) z = TStTrans x (transStepTransitive y z)

-- Correctness proof for 'TransStep', i.e.: TransStep => (TransCl Step).
transStepCorrect : TransStep e e' -> TransCl Step e e'
transStepCorrect (TStRefl e)    = TClRefl e
transStepCorrect (TStTrans x y) = TClTrans (TClSingle x) (transStepCorrect y)

-- Completeness proof for 'TransStep', i.e.: (TransCl Step) => TransStep.
transStepComplete : TransCl Step e e' -> TransStep e e'
transStepComplete (TClRefl e)    = TStRefl e
transStepComplete (TClSingle x)  = TStTrans x (TStRefl _)
transStepComplete (TClTrans x z) = transStepTransitive (transStepComplete x)
                                                       (transStepComplete z)

-- Operators for compact notation:
infixl 10 .++.
(.++.) : TransStep e1 e2 -> TransStep e2 e3 -> TransStep e1 e3
(.++.) = transStepTransitive

infixl 10 .+.
(.+.) : TransStep e1 e2 -> Step e2 e3 -> TransStep e1 e3
(.+.) x y = x .++. (TStTrans y (TStRefl _))

-- End: TRANSITIVE CLOSURE
--------------------------

max_stars_repo_name: normanrink/PCF

max_issues_repo_name: normanrink/PCF

max_forks_repo_name: normanrink/PCF


text:
module Yaffle.Main

import Parser.Source

import Core.Binary
import Core.Context
import Core.Directory
import Core.Env
import Core.FC
import Core.InitPrimitives
import Core.Metadata
import Core.Normalise
import Core.Options
import Core.TT
import Core.UnifyState
import Utils.Path

import TTImp.Parser
import TTImp.ProcessDecls
import TTImp.TTImp

import Yaffle.REPL

import Data.List
import Data.So
import Data.Strings
import System

%default covering

usage : String
usage = "Usage: yaffle <input file> [--timing]"

processArgs : List String -> Core Bool
processArgs [] = pure False
processArgs ["--timing"] = pure True
processArgs _
    = coreLift $ do putStrLn usage
                    exitWith (ExitFailure 1)

HasNames () where
  full _ _ = pure ()
  resolved _ _ = pure ()

export
yaffleMain : String -> List String -> Core ()
yaffleMain fname args
    = do defs <- initDefs
         c <- newRef Ctxt defs
         m <- newRef MD initMetadata
         u <- newRef UST initUState
         d <- getDirs
         t <- processArgs args
         setLogTimings t
         addPrimitives
         case extension fname of
              Just "ttc" => do coreLift $ putStrLn "Processing as TTC"
                               readFromTTC {extra = ()} True emptyFC True fname (nsAsModuleIdent emptyNS) emptyNS
                               coreLift $ putStrLn "Read TTC"
              _ => do coreLift $ putStrLn "Processing as TTImp"
                      ok <- processTTImpFile fname
                      when ok $
                         do ns <- pathToNS (working_dir d) (source_dir d) fname
                            makeBuildDirectory ns
                            writeToTTC () !(getTTCFileName fname "ttc")
                            coreLift $ putStrLn "Written TTC"
         ust <- get UST

         repl {c} {u}

ymain : IO ()
ymain
    = do (_ :: fname :: rest) <- getArgs
             | _ => do putStrLn usage
                       exitWith (ExitFailure 1)
         coreRun (yaffleMain fname rest)
               (\err : Error => putStrLn ("Uncaught error: " ++ show err))
               (\res => pure ())


text:
%default partial

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

append : Vect n a -> Vect m a -> Vect (n + m) a
append [] ys = ys
append (x :: xs) ys = x :: append xs ys

-- Primarily to check the number of cases in the totality checker doesn't
-- explode because of all the Nils and Nats
funny : Vect 4 Bool -> Int
funny [False, False, False, False] = 0
funny [False, False, False, True] = 1
funny [False, False, True, False] = 2
funny [False, False, True, True] = 3
funny [False, True, False, False] = 4
funny [False, True, False, True] = 5
funny [False, True, True, False] = 6
funny [False, True, True, True] = 7
funny [True, False, False, False] = 8
funny [True, False, False, True] = 0
funny [True, False, True, False] = 10
funny [True, False, True, True] = 11
funny [True, True, False, False] = 12
funny [True, True, False, True] = 13
funny [True, True, True, False] = 14
funny [True, True, True, True] = 15

notFunny : Vect 4 Bool -> Int
notFunny [False, False, False, False] = 0
notFunny [False, False, False, True] = 1
notFunny [False, False, True, False] = 2
-- notFunny [False, False, True, True] = 3
notFunny [False, True, False, False] = 4
notFunny [False, True, False, True] = 5
notFunny [False, True, True, False] = 6
-- notFunny [False, True, True, True] = 7
notFunny [True, False, False, False] = 8
notFunny [True, False, False, True] = 0
notFunny [True, False, True, False] = 10
notFunny [True, False, True, True] = 11
notFunny [True, True, False, False] = 12
notFunny [True, True, False, True] = 13
notFunny [True, True, True, False] = 14
notFunny [True, True, True, True] = 15


text:
module Main

import Data.Primitives.Views
import System

%default total

record Score where
  constructor MkScore
  correct   : Nat
  attempted : Nat

record GameState where
  constructor MkGameState
  score       : Score
  difficulty  : Int

initState : GameState
initState = MkGameState (MkScore 0 0) 12

Show GameState where
  show st = show (correct (score st)) ++ "/" ++
            show (attempted (score st)) ++ "\n" ++
            "Difficulty: " ++ show (difficulty st)

data Command : Type -> Type where
  PutStr : String -> Command ()
  GetLine : Command String

  GetRandom : Command Int
  GetGameState : Command GameState
  PutGameState : GameState -> Command ()

  Pure : ty -> Command ty
  Bind : Command a -> (a -> Command b) -> Command b

Functor Command where
  map f x = Bind x (\val => Pure (f val))

Applicative Command where
  pure = Pure
  f <*> x = Bind f $ \f' =>
            Bind x $ \x' =>
            Pure (f' x')

Monad Command where
  (>>=) = Bind

namespace CommandDo
  (>>=) : Command a -> (a -> Command b) -> Command b
  (>>=) = Bind

data ConsoleIO : Type -> Type where
  Quit : a -> ConsoleIO a
  Do   : Command a -> (a -> Inf (ConsoleIO b)) -> ConsoleIO b

namespace ConsoleDo
  (>>=) : Command a -> (a -> Inf (ConsoleIO b)) -> ConsoleIO b
  (>>=) = Do

setDifficulty1 : Int -> GameState -> GameState
setDifficulty1 newDiff (MkGameState score _) = MkGameState score newDiff

setDifficulty2 : Int -> GameState -> GameState
setDifficulty2 newDiff state = record { difficulty = newDiff } state

setDifficulty3 : Int -> GameState -> GameState
setDifficulty3 newDiff = record { difficulty = newDiff }

addWrong0 : GameState -> GameState
addWrong0 state = record
  { score -> attempted = attempted (score state) + 1
  } state

addCorrect0 : GameState -> GameState
addCorrect0 state = record
  { score -> correct = correct (score state) + 1
  , score -> attempted = attempted (score state) + 1
  } state

addWrong : GameState -> GameState
addWrong = record { score -> attempted $= (+1) }

addCorrect : GameState -> GameState
addCorrect = record
  { score -> attempted $= (+1)
  , score -> correct   $= (+1)
  }

data Input = Answer Int
           | QuitCmd

mutual
  correct : ConsoleIO GameState
  correct = do
    PutStr "Correct!\n"
    st <- GetGameState
    PutGameState (addCorrect st)
    quiz

  wrong : Int -> ConsoleIO GameState
  wrong ans = do
    PutStr ("Wrong, the answer is " ++ show ans ++ "\n")
    st <- GetGameState
    PutGameState (addWrong st)
    quiz

  readInput : (prompt : String) -> Command Input
  readInput prompt = do
    PutStr prompt
    answer <- GetLine
    if toLower answer == "quit"
      then Pure QuitCmd
      else Pure (Answer (cast answer))

  quiz : ConsoleIO GameState
  quiz = do num1 <- GetRandom
            num2 <- GetRandom
            st <- GetGameState
            PutStr (show st ++ "\n")
            input <- readInput (show num1 ++ " * " ++ show num2 ++ "? ")
            case input of
              Answer answer => if answer == num1 * num2
                                then correct
                                else wrong (num1 * num2)
              QuitCmd => Quit st

runCommand : Stream Int
          -> GameState
          -> Command a
          -> IO (a, Stream Int, GameState)
runCommand rnds state (PutStr x) = do
  putStr x
  pure ((), rnds, state)

runCommand rnds state GetLine = do
  str <- getLine
  pure (str, rnds, state)

runCommand (val :: rnds) state GetRandom = pure (getRandom val (difficulty state), rnds, state)
  where
    getRandom : Int -> Int -> Int
    getRandom val max with (divides val max)
      getRandom val 0 | DivByZero = 1
      getRandom ((max * div) + rem) max | (DivBy prf) = abs rem + 1

runCommand rnds state GetGameState = pure (state, rnds, state)
runCommand rnds state (PutGameState newState) = pure ((), rnds, newState)
runCommand rnds state (Pure val) = pure (val, rnds, state)
runCommand rnds state (Bind c f) = do
  (res, newRnds, newState) <- runCommand rnds state c
  runCommand newRnds newState (f res)

data Fuel = Dry | More (Lazy Fuel)

partial
forever : Fuel
forever = More forever

tank : Nat -> Fuel
tank Z = Dry
tank (S n) = More (tank n)

run : Fuel -> Stream Int -> GameState -> ConsoleIO a -> IO (Maybe a, Stream Int, GameState)
run Dry         rnds state p          = pure (Nothing, rnds, state)
run fuel        rnds state (Quit val) = pure (Just val, rnds, state)
run (More fuel) rnds state (Do c f)   = do
  (res, newRnds, newState) <- runCommand rnds state c
  run fuel newRnds newState (f res)

randoms : Int -> Stream Int
randoms seed =
  let seed' = 1664525 * seed + 1013904223
  in (seed' `shiftR` 2) :: randoms seed'

test : IO ()
test = do
  printLn initState
  printLn $ setDifficulty1 10 initState
  printLn $ setDifficulty2 11 initState
  printLn $ setDifficulty3 9  initState
  printLn $ addWrong0 initState
  printLn $ addCorrect0 initState
  printLn $ addWrong initState
  printLn $ addCorrect initState

partial
main : IO ()
main = do
  test
  -- seed <- time
  let seed = 0
  (Just score, _, state) <-
    run forever (randoms (fromInteger seed)) initState quiz
      | _ => putStrLn "Ran out of fuel"
  putStrLn ("Final score: " ++ show state)

max_stars_repo_name: luc-tielen/idris-grin

max_issues_repo_name: luc-tielen/idris-grin

max_forks_repo_name: luc-tielen/idris-grin


text:
module TTImp.TTImp.Functor

import Core.TT
import TTImp.TTImp

%default covering

mutual

  export
  Functor RawImp' where
    map f (IVar fc nm) = IVar fc (f nm)
    map f (IPi fc rig info nm a sc)
      = IPi fc rig (map (map f) info) nm (map f a) (map f sc)
    map f (ILam fc rig info nm a sc)
      = ILam fc rig (map (map f) info) nm (map f a) (map f sc)
    map f (ILet fc lhsFC rig nm ty val sc)
      = ILet fc lhsFC rig nm (map f ty) (map f val) (map f sc)
    map f (ICase fc sc ty cls)
      = ICase fc (map f sc) (map f ty) (map (map f) cls)
    map f (ILocal fc ds sc)
      = ILocal fc (map (map f) ds) (map f sc)
    map f (ICaseLocal fc userN intN args sc)
      = ICaseLocal fc userN intN args (map f sc)
    map f (IUpdate fc upds rec)
      = IUpdate fc (map (map f) upds) (map f rec)
    map f (IApp fc fn t)
      = IApp fc (map f fn) (map f t)
    map f (IAutoApp fc fn t)
      = IAutoApp fc (map f fn) (map f t)
    map f (INamedApp fc fn nm t)
      = INamedApp fc (map f fn) nm (map f t)
    map f (IWithApp fc fn t)
      = IWithApp fc (map f fn) (map f t)
    map f (ISearch fc n)
      = ISearch fc n
    map f (IAlternative fc alt ts)
      = IAlternative fc (map f alt) (map (map f) ts)
    map f (IRewrite fc e t)
      = IRewrite fc (map f e) (map f t)
    map f (ICoerced fc e)
      = ICoerced fc (map f e)
    map f (IBindHere fc bd t)
      = IBindHere fc bd (map f t)
    map f (IBindVar fc str)
      = IBindVar fc str
    map f (IAs fc nmFC side nm t)
      = IAs fc nmFC side nm (map f t)
    map f (IMustUnify fc reason t)
      = IMustUnify fc reason (map f t)
    map f (IDelayed fc reason t)
      = IDelayed fc reason (map f t)
    map f (IDelay fc t)
      = IDelay fc (map f t)
    map f (IForce fc t)
      = IForce fc (map f t)
    map f (IQuote fc t)
      = IQuote fc (map f t)
    map f (IQuoteName fc nm)
      = IQuoteName fc nm
    map f (IQuoteDecl fc ds)
      = IQuoteDecl fc (map (map f) ds)
    map f (IUnquote fc t)
      = IUnquote fc (map f t)
    map f (IRunElab fc t)
      = IRunElab fc (map f t)
    map f (IPrimVal fc c)
      = IPrimVal fc c
    map f (IType fc)
      = IType fc
    map f (IHole fc str)
      = IHole fc str
    map f (IUnifyLog fc lvl t)
      = IUnifyLog fc lvl (map f t)
    map f (Implicit fc b)
      = Implicit fc b
    map f (IWithUnambigNames fc ns t)
      = IWithUnambigNames fc ns (map f t)

  export
  Functor ImpClause' where
    map f (PatClause fc lhs rhs)
      = PatClause fc (map f lhs) (map f rhs)
    map f (WithClause fc lhs wval prf flags xs)
      = WithClause fc (map f lhs) (map f wval) prf flags (map (map f) xs)
    map f (ImpossibleClause fc lhs)
      = ImpossibleClause fc (map f lhs)

  export
  Functor ImpDecl' where
    map f (IClaim fc rig vis opts ty)
      = IClaim fc rig vis (map (map f) opts) (map f ty)
    map f (IData fc vis dt)
      = IData fc vis (map f dt)
    map f (IDef fc nm cls)
      = IDef fc nm (map (map f) cls)
    map f (IParameters fc ps ds)
      = IParameters fc (map (map  {f = ImpParameter'} f) ps) (map (map f) ds)
    map f (IRecord fc cs vis rec)
      = IRecord fc cs vis (map f rec)
    map f (INamespace fc ns ds)
      = INamespace fc ns (map (map f) ds)
    map f (ITransform fc n lhs rhs)
      = ITransform fc n (map f lhs) (map f rhs)
    map f (IRunElabDecl fc t)
      = IRunElabDecl fc (map f t)
    map f (IPragma xs k) = IPragma xs k
    map f (ILog x) = ILog x
    map f (IBuiltin fc ty n) = IBuiltin fc ty n

  export
  Functor FnOpt' where
    map f Inline = Inline
    map f TCInline = TCInline
    map f (Hint b) = Hint b
    map f (GlobalHint b) = GlobalHint b
    map f ExternFn = ExternFn
    map f (ForeignFn ts) = ForeignFn (map (map f) ts)
    map f Invertible = Invertible
    map f (Totality tot) = Totality tot
    map f Macro = Macro
    map f (SpecArgs ns) = SpecArgs ns

  export
  Functor ImpTy' where
    map f (MkImpTy fc nameFC n ty)
      = MkImpTy fc nameFC n (map f ty)

  export
  Functor ImpData' where
    map f (MkImpData fc n tycon opts datacons)
      = MkImpData fc n (map f tycon) opts (map (map f) datacons)
    map f (MkImpLater fc n tycon)
      = MkImpLater fc n (map f tycon)

  export
  Functor IField' where
    map f (MkIField fc rig info n t)
      = MkIField fc rig (map (map f) info) n (map f t)

  export
  Functor ImpRecord' where
    map f (MkImpRecord fc n params conName fields)
      = MkImpRecord fc n (map (map {f = ImpParameter'} f) params)
                    conName (map (map f) fields)

  export
  Functor ImpParameter' where
    map f (nm, rig, info, t) = (nm, rig, map (map f) info, map f t)

  export
  Functor IFieldUpdate' where
    map f (ISetField path t) = ISetField path (map f t)
    map f (ISetFieldApp path t) = ISetFieldApp path (map f t)

  export
  Functor AltType' where
    map f FirstSuccess = FirstSuccess
    map f Unique = Unique
    map f (UniqueDefault t) = UniqueDefault (map f t)


text:
data Bool = True | False

data Direction = North
               | East
               | South
               | West

turnClockwise : Direction -> Direction
turnClockwise North = East
turnClockwise East = South
turnClockwise South = West
turnClockwise West = North

||| Represents shapes
data Shape = ||| A triangle, with its base length and height
             Triangle Double Double
           | ||| A rectangle, with its length and height
             Rectangle Double Double
           | ||| A circle, with its radius
             Circle Double

%name Shape shape, shape1, shape2

area : Shape -> Double
area (Triangle base height) = 0.5 * base * height
area (Rectangle length height) = length * height
area (Circle radius) = pi * radius * radius

-- Recursive type
data Picture = Primitive Shape
             | Combine Picture Picture
             | Rotate Double Picture
             | Translate Double Double Picture

%name Picture pic, pic1, pic2

pictureArea : Picture -> Double
pictureArea (Primitive shape) = area shape
pictureArea (Combine pic pic1) = pictureArea pic + pictureArea pic1
pictureArea (Rotate _ pic) = pictureArea pic
pictureArea (Translate _ _ pic) = pictureArea pic

-- Generic type
data BSTree : Type -> Type where
  Empty : Ord e => BSTree e
  Node : Ord e => (left : BSTree e) -> (val : e) -> (right : BSTree e) -> BSTree e

total insert : e -> BSTree e -> BSTree e
insert x Empty = Node Empty x Empty
insert x (Node left y right) = case compare x y of
                                    LT => Node (insert x left) y right
                                    EQ => Node left y right
                                    GT => Node left y (insert x right)

max_stars_repo_name: brunoflores/type-driven-with-idris

max_issues_repo_name: brunoflores/type-driven-with-idris

max_forks_repo_name: brunoflores/type-driven-with-idris


text:
module Semiring

import Data.Morphisms

%default total
%hide (+)
%hide (*)
%access public export

interface Semiring a where
  (+) : a -> a -> a
  (*) : a -> a -> a
  one : a
  zer : a

sum : (Foldable f, Semiring a) => f a -> a
sum = foldl (+) zer

mul : (Foldable f, Semiring a) => f a -> a
mul = foldl (*) one

Semiring Bool where
  x + y = x || y
  x * y = x && y
  one = True
  zer = False

Semiring b => Semiring (Morphism a b) where
  (Mor f) + (Mor g) = Mor (\x => f x + g x)
  (Mor f) * (Mor g) = Mor (\x => f x * g x)
  one = Mor (\_ => one)
  zer = Mor (\_ => zer)

Semiring Double where
  (+) = prim__addFloat
  (*) = prim__mulFloat
  one = 1
  zer = 0

Semiring Int where
  (+) = prim__addInt
  (*) = prim__mulInt
  one = 1
  zer = 0

interface Semiring a => VerifiedSemiring a where
  plusAssoc : (x, y, z : a) -> (x + y) + z = x + (y + z)
  multAssoc : (x, y, z : a) -> (x * y) * z = x * (y * z)
  plusComm  : (x : a) -> (y : a) -> x + y = y + x
  plusId : (x : a) -> x + Semiring.zer = x
  mulIdR : (x : a) -> x * Semiring.one = x
  mulIdL : (x : a) -> Semiring.one * x = x
  mulAnR : (x : a) -> x * Semiring.zer = Semiring.zer
  mulAnL : (x : a) -> Semiring.zer * x = Semiring.zer
  mulDsR : (x, y, z : a) -> (x + y) * z = (x * z) + (y * z)
  mulDsL : (x, y, z : a) -> x * (y + z) = (x * y) + (x * z)

VerifiedSemiring Bool where
  plusAssoc False y z = Refl
  plusAssoc True  y z = Refl
  multAssoc False y z = Refl
  multAssoc True  y z = Refl
  plusComm False False = Refl
  plusComm False True  = Refl
  plusComm True  False = Refl
  plusComm True  True  = Refl
  plusId False = Refl
  plusId True  = Refl
  mulIdL False = Refl
  mulIdL True  = Refl
  mulIdR False = Refl
  mulIdR True  = Refl
  mulAnR False = Refl
  mulAnR True  = Refl
  mulAnL x = Refl
  mulDsR False y z = Refl
  mulDsR True False False = Refl
  mulDsR True False True  = Refl
  mulDsR True True False  = Refl
  mulDsR True True True   = Refl
  mulDsL False y z = Refl
  mulDsL True  y z = Refl

Semiring Nat where
  (+) = plus
  (*) = mult
  one = 1
  zer = 0

VerifiedSemiring Nat where
  plusAssoc x y z = sym (plusAssociative x y z)
  multAssoc x y z = sym (multAssociative x y z)
  plusComm = plusCommutative
  plusId = plusZeroRightNeutral
  mulAnL = multZeroLeftZero
  mulAnR = multZeroRightZero
  mulIdL = multOneLeftNeutral
  mulIdR = multOneRightNeutral
  mulDsL = multDistributesOverPlusRight
  mulDsR = multDistributesOverPlusLeft

interface Semigroup a => VerifiedSemigroup a where
  semigroupOpIsAssociative : (l, c, r : a) -> l <+> (c <+> r) = (l <+> c) <+> r

interface (VerifiedSemigroup a, Monoid a) => VerifiedMonoid a where
  monoidNeutralIsNeutralL : (l : a) -> l <+> neutral = l
  monoidNeutralIsNeutralR : (r : a) -> neutral <+> r = r

interface VerifiedMonoid a => CommutativeMonoid a where
  mappendCommutes : (x, y : a) -> x <+> y = y <+> x

CommutativeMonoid a => Semiring (Endomorphism a) where
  (Endo f) + (Endo g) = Endo (\x => f x <+> g x)
  (Endo f) * (Endo g) = Endo (f . g)
  zer = Endo (const neutral)
  one = Endo id

max_stars_repo_name: oisdk/belief-propagation-idris

max_issues_repo_name: oisdk/belief-propagation-idris

max_forks_repo_name: oisdk/belief-propagation-idris


text:
module JS.ByteString

import JS.Marshall

export
data ByteString : Type where [external]

export
ToFFI ByteString ByteString where toFFI = id

export
FromFFI ByteString ByteString where fromFFI = Just


text:
module Control.Optics

import public Control.Optics.Either
import public Control.Optics.Getter
import public Control.Optics.Lens
import public Control.Optics.Pair
import public Control.Optics.Prism
import public Control.Optics.Review
import public Control.Optics.Setter
import public Control.Optics.State
import public Control.Optics.Types
import public Control.Optics.Vect


text:
module Imp

import Expr
import Logic
import Maps

%access public export

%default total

data Com : Type where
  CSkip : Com
  CAss : Id -> AExp -> Com
  CSeq : Com -> Com -> Com
  CIf : BExp -> Com -> Com -> Com
  CIf1 : BExp -> Com -> Com
  CWhile : BExp -> Com -> Com
  CFor : Com -> BExp -> Com -> Com -> Com
  CRepeat : Com -> BExp -> Com

infix 5 ::=

SKIP : Com
SKIP = CSkip

(::=) : Id -> AExp -> Com
(::=) = CAss

(>>=) : Com -> (() -> Com) -> Com
(>>=) c f = CSeq c (f ())

WHILE : BExp -> Com -> Com
WHILE = CWhile

syntax IFB [b] THEN [c1] ELSE [c2] FI = CIf b c1 c2

syntax IF1 [b] THEN [c] FI = CIf1 b c

syntax FOR [init] ";" [cond] ";" [updt] DO [body] DONE = CFor init cond updt body

syntax REPEAT [c] UNTIL [b] END = CRepeat c b

data CEval : Com -> State -> State -> Type where
  E_Skip : CEval CSkip st st
  E_Ass : aeval st a1 = n -> CEval (CAss x a1) st (t_update x n st)
  E_Seq : CEval c1 st1 st2 -> CEval c2 st2 st3 ->
          CEval (CSeq c1 c2) st1 st3
  E_IfTrue : beval st b = True -> CEval c1 st st1 ->
             CEval (CIf b c1 c2) st st1
  E_IfFalse : beval st b = False -> CEval c2 st st1 ->
              CEval (CIf b c1 c2) st st1
  E_If1True : beval st b = True -> CEval c st st1 ->
              CEval (CIf1 b c) st st1
  E_If1False : beval st b = False -> CEval (CIf1 b c) st st
  E_WhileEnd : beval st b = False -> CEval (CWhile b c) st st
  E_WhileLoop : beval st b = True ->
                CEval c st st1 -> CEval (CWhile b c) st1 st2 ->
                CEval (CWhile b c) st st2
  E_For : CEval init st1 st2 ->
          CEval (CWhile cond (CSeq body updt)) st2 st3 ->
          CEval (CFor init cond updt body) st1 st3
  E_Repeat : CEval c st st1 ->
             CEval (CWhile (not b) c) st1 st2 ->
             CEval (CRepeat c b) st st2

syntax [c1] "/" [st1] "\\\\" [st2] = CEval c1 st1 st2

repeat_example_1 : CEval (REPEAT do
                            X ::= 1
                            Y ::= Y + 1
                          UNTIL X == 1 END)
                         Expr.empty_state
                         (t_update Y 1 (t_update X 1 Expr.empty_state))
repeat_example_1 = E_Repeat (E_Seq (E_Ass Refl)
                                   (E_Ass Refl))
                            (E_WhileEnd Refl)

ceval_deterministic : (c / st \\ st1) -> (c / st \\ st2) -> st1 = st2
ceval_deterministic E_Skip E_Skip = Refl
ceval_deterministic (E_Ass aev1) (E_Ass aev2) =
  rewrite sym aev1
  in rewrite sym aev2
  in Refl
ceval_deterministic {st2} (E_Seq cev11 cev12) (E_Seq {c2} cev21 cev22) =
  let ih = ceval_deterministic cev11 cev21
      cev22' = replace (sym ih) cev22 {P=\x=>CEval c2 x st2}
  in ceval_deterministic cev12 cev22'
ceval_deterministic (E_IfTrue _ cev1) (E_IfTrue _ cev2) =
  ceval_deterministic cev1 cev2
ceval_deterministic (E_IfTrue prf1 _) (E_IfFalse prf2 _) =
  absurd $ replace prf1 prf2 {P=\x=>x=False}
ceval_deterministic (E_IfFalse prf1 _) (E_IfTrue prf2 _) =
  absurd $ replace prf2 prf1 {P=\x=>x=False}
ceval_deterministic (E_IfFalse _ cev1) (E_IfFalse _ cev2) =
  ceval_deterministic cev1 cev2
ceval_deterministic (E_If1True _ cc1) (E_If1True _ cc2) =
  ceval_deterministic cc1 cc2
ceval_deterministic (E_If1True prf1 _) (E_If1False prf2) =
  absurd $ trans (sym prf1) prf2
ceval_deterministic (E_If1False prf1) (E_If1True prf2 _) =
  absurd $ trans (sym prf1) prf2
ceval_deterministic (E_If1False _) (E_If1False _) = Refl
ceval_deterministic (E_WhileEnd _) (E_WhileEnd _) = Refl
ceval_deterministic (E_WhileEnd prf1) (E_WhileLoop prf2 _ _) =
  absurd $ replace prf2 prf1 {P=\x=>x=False}
ceval_deterministic (E_WhileLoop prf1 _ _) (E_WhileEnd prf2) =
  absurd $ replace prf1 prf2 {P=\x=>x=False}
ceval_deterministic {st2} (E_WhileLoop _ cev11 cev12)
                          (E_WhileLoop {b} {c} _ cev21 cev22) =
  let ih = ceval_deterministic cev11 cev21
      cev22' = replace (sym ih) cev22 {P=\x=>CEval (CWhile b c) x st2}
  in ceval_deterministic cev12 cev22'
ceval_deterministic {st2}
                    (E_For cinit1 cwhile1)
                    (E_For {cond} {body} {updt} cinit2 cwhile2) =
  let ih = ceval_deterministic cinit1 cinit2
      cwhile2' = replace {P=\x => CEval (CWhile cond (CSeq body updt)) x st2}
                         (sym ih) cwhile2
  in ceval_deterministic cwhile1 cwhile2'
ceval_deterministic (E_Repeat cc1 cwhile1) (E_Repeat {b} {c} {st2} cc2 cwhile2) =
  let ih = ceval_deterministic cc1 cc2
      cwhile2' = replace {P=\x => CEval (CWhile (not b) c) x st2}
                         (sym ih) cwhile2
  in ceval_deterministic cwhile1 cwhile2'


text:
||| Functions for the processing of received request and
||| notifications.
|||
||| (C) The Idris Community, 2021
module Server.ProcessMessage

import Core.Context
import Core.Core
import Core.Env
import Core.Metadata
import Core.UnifyState
import Data.List
import Data.OneOf
import Data.SortedSet
import Data.String
import Idris.Doc.String
import Idris.IDEMode.Holes
import Idris.ModTree
import Idris.Package
import Idris.Pretty
import Idris.REPL
import Idris.REPL.Opts
import Idris.Resugar
import Idris.Syntax
import Language.JSON
import Language.LSP.CodeAction
import Language.LSP.CodeAction.AddClause
import Language.LSP.CodeAction.CaseSplit
import Language.LSP.CodeAction.ExprSearch
import Language.LSP.CodeAction.RefineHole
import Language.LSP.CodeAction.GenerateDef
import Language.LSP.CodeAction.MakeCase
import Language.LSP.CodeAction.MakeLemma
import Language.LSP.CodeAction.MakeWith
import Language.LSP.Definition
import Language.LSP.DocumentSymbol
import Language.LSP.SignatureHelp
import Language.LSP.Message
import Libraries.Data.PosMap
import Libraries.Data.Version
import Libraries.Utils.Path
import Server.Capabilities
import Server.Configuration
import Server.Diagnostics
import Server.Log
import Server.QuickFix
import Server.Response
import Server.SemanticTokens
import Server.Utils
import System
import System.Clock
import System.Directory
import System.File
import Data.List1
import Libraries.Data.List.Extra
import Parser.Unlit

||| Mostly copied from Idris.REPL.displayResult.
replResultToDoc : {auto c : Ref Ctxt Defs}
               -> {auto u : Ref UST UState}
               -> {auto s : Ref Syn SyntaxInfo}
               -> {auto m : Ref MD Metadata}
               -> {auto o : Ref ROpts REPLOpts}
               -> REPLResult
               -> Core (Doc IdrisAnn)
replResultToDoc (REPLError err) = pure err
replResultToDoc (Evaluated x Nothing) = pure (prettyTerm x)
replResultToDoc (Evaluated x (Just y)) = pure (prettyTerm x <++> colon <++> code (prettyTerm y))
replResultToDoc (Printed xs) = pure xs
replResultToDoc (TermChecked x y) = pure (prettyTerm x <++> colon <++> code (prettyTerm y))
replResultToDoc (FileLoaded x) = pure (reflow "Loaded file" <++> pretty x)
replResultToDoc (ModuleLoaded x) = pure (reflow "Imported module" <++> pretty x)
replResultToDoc (ErrorLoadingModule x err) = pure $ reflow "Error loading module" <++> pretty x <+> colon <++> !(perror err)
replResultToDoc (ErrorLoadingFile x err) = pure (reflow "Error loading file" <++> pretty x <+> colon <++> pretty (show err))
replResultToDoc (ErrorsBuildingFile x errs) = pure (reflow "Error(s) building file" <++> pretty x) -- messages already displayed while building
replResultToDoc NoFileLoaded = pure (reflow "No file can be reloaded")
replResultToDoc (CurrentDirectory dir) = pure (reflow "Current working directory is" <++> dquotes (pretty dir))
replResultToDoc CompilationFailed = pure (reflow "Compilation failed")
replResultToDoc (Compiled f) = pure (pretty "File" <++> pretty f <++> pretty "written")
replResultToDoc (ProofFound x) = pure (prettyTerm x)
replResultToDoc (Missed cases) = pure $ vsep (handleMissing <$> cases)
replResultToDoc (CheckedTotal xs) = pure (vsep (map (\(fn, tot) => pretty fn <++> pretty "is" <++> pretty tot) xs))
replResultToDoc (FoundHoles []) = pure (reflow "No holes")
replResultToDoc (FoundHoles [x]) = pure (reflow "1 hole" <+> colon <++> pretty x.name)
replResultToDoc (FoundHoles xs) = do
  let holes = concatWith (surround (pretty ", ")) (pretty . name <$> xs)
  pure (pretty (length xs) <++> pretty "holes" <+> colon <++> holes)
replResultToDoc (LogLevelSet Nothing) = pure (reflow "Logging turned off")
replResultToDoc (LogLevelSet (Just k)) = pure (reflow "Set log level to" <++> pretty k)
replResultToDoc (ConsoleWidthSet (Just k)) = pure (reflow "Set consolewidth to" <++> pretty k)
replResultToDoc (ConsoleWidthSet Nothing) = pure (reflow "Set consolewidth to auto")
replResultToDoc (ColorSet b) = pure (reflow (if b then "Set color on" else "Set color off"))
replResultToDoc (VersionIs x) = pure (pretty (showVersion True x))
replResultToDoc (RequestedHelp) = pure (pretty displayHelp)
replResultToDoc (Edited (DisplayEdit Empty)) = pure (pretty "")
replResultToDoc (Edited (DisplayEdit xs)) = pure xs
replResultToDoc (Edited (EditError x)) = pure x
replResultToDoc (Edited (MadeLemma lit name pty pappstr)) = pure $ pretty (relit lit (show name ++ " : " ++ show pty ++ "\n") ++ pappstr)
replResultToDoc (Edited (MadeWith lit wapp)) = pure $ pretty $ showSep "\n" (map (relit lit) wapp)
replResultToDoc (Edited (MadeCase lit cstr)) = pure $ pretty $ showSep "\n" (map (relit lit) cstr)
replResultToDoc (OptionsSet opts) = pure (vsep (pretty <$> opts))
replResultToDoc Done = pure ""
replResultToDoc (Executed _) = pure ""
replResultToDoc DefDeclared = pure ""
replResultToDoc Exited = pure ""
-- Would be nice to preserve colours in the future, but
-- sending ansi codes over the socket is a probably a no-go.
replResultToDoc (PrintedDoc doc) = pure (unAnnotate doc)

displayType : {auto c : Ref Ctxt Defs} ->
              {auto s : Ref Syn SyntaxInfo} ->
              Defs -> (Name, Int, GlobalDef) ->
              Core (Doc IdrisAnn)
displayType defs (n, i, gdef)
    = maybe (do tm <- resugar [] !(normaliseHoles defs [] (type gdef))
                pure (pretty !(aliasName (fullname gdef)) <++> colon <++> prettyTerm tm))
            (\num => reAnnotate Syntax <$> prettyHole defs [] n num (type gdef))
            (isHole gdef)

displayTerm : {auto c : Ref Ctxt Defs} ->
              {auto s : Ref Syn SyntaxInfo} ->
              Defs -> ClosedTerm ->
              Core (Doc IdrisAnn)
displayTerm defs tm
    = do ptm <- resugar [] !(normaliseHoles defs [] tm)
         pure (prettyTerm ptm)

isDirty : Ref LSPConf LSPConfiguration => DocumentURI -> Core Bool
isDirty uri = gets LSPConf (contains uri . dirtyFiles)

isError : Ref LSPConf LSPConfiguration => DocumentURI -> Core Bool
isError uri = gets LSPConf (contains uri . errorFiles)

loadURI : Ref LSPConf LSPConfiguration
       => Ref Ctxt Defs
       => Ref UST UState
       => Ref Syn SyntaxInfo
       => Ref MD Metadata
       => Ref ROpts REPLOpts
       => InitializeParams -> URI -> Maybe Int -> Core (Either String ())
loadURI conf uri version = do
  logI Server "Loading file \{show uri}"
  update LSPConf (record {openFile = Just (uri, fromMaybe 0 version)})
  resetContext (Virtual Interactive)
  let fpath = uri.path
  let Just (startFolder, startFile) = splitParent fpath
    | Nothing => do let msg = "Cannot find the parent folder for \{show uri}"
                    logE Server msg
                    pure $ Left msg
  True <- coreLift $ changeDir startFolder
    | False => do let msg = "Cannot change current directory to \{show startFolder}, folder of \{show startFile}"
                  logE Server msg
                  pure $ Left msg
  Just fname <- findIpkg (Just fpath)
    | Nothing => do let msg = "Cannot find ipkg file for \{show uri}"
                    logE Server msg
                    pure $ Left msg
  Right res <- coreLift $ File.ReadWrite.readFile fname
    | Left err => do let msg = "Cannot read file at \{show uri}"
                     logE Server msg
                     pure $ Left msg
  setSource res
  errs <- catch
            (buildDeps fname)
            (\err => do
              logE Server "Caught error which shouldn't be leaked while loading file: \{show err}"
              pure [err])
  -- FIXME: the compiler always dumps the errors on stdout, requires
  --        a compiler change.
  -- NOTE on catch: It seems the compiler sometimes throws errors instead
  -- of accumulating them in the buildDeps.
  case errs of
    [] => pure ()
    (_::_) => update LSPConf (record { errorFiles $= insert uri })
  resetProofState
  let caps = (publishDiagnostics <=< textDocument) . capabilities $ conf
  update LSPConf (record { quickfixes = [], cachedActions = empty, cachedHovers = empty })
  traverse_ (findQuickfix caps uri) errs
  sendDiagnostics caps uri version errs
  pure $ Right ()

loadIfNeeded : Ref LSPConf LSPConfiguration
            => Ref Ctxt Defs
            => Ref UST UState
            => Ref Syn SyntaxInfo
            => Ref MD Metadata
            => Ref ROpts REPLOpts
            => InitializeParams -> URI -> Maybe Int -> Core (Either String ())
loadIfNeeded conf uri version = do
  Just (oldUri, oldVersion) <- gets LSPConf openFile
    | Nothing => loadURI conf uri version
  if (oldUri == uri && (isNothing version || (Just oldVersion) == version))
     then pure $ Right ()
     else loadURI conf uri version

withURI : Ref LSPConf LSPConfiguration
       => Ref Ctxt Defs
       => Ref UST UState
       => Ref Syn SyntaxInfo
       => Ref MD Metadata
       => Ref ROpts REPLOpts
       => InitializeParams
       -> URI -> Maybe Int -> Core (Either ResponseError a) -> Core (Either ResponseError a) -> Core (Either ResponseError a)
withURI conf uri version d k = do
  False <- isError uri
    | _ => logW Server "Trying to load \{show uri} which has errors" >> d
  case !(loadIfNeeded conf uri version) of
       Right () => k
       Left err => do
         logE Server "Error while loading \{show uri}: \{show err}"
         pure $ Left (MkResponseError (Custom 3) err JNull)

||| Guard for requests that requires a successful initialization before being allowed.
whenInitializedRequest : Ref LSPConf LSPConfiguration => (InitializeParams -> Core (Either ResponseError a)) -> Core (Either ResponseError a)
whenInitializedRequest k =
  case !(gets LSPConf initialized) of
       Just conf => k conf
       Nothing => do logE Server "Cannot process requests before initalization"
                     pure $ Left $ serverNotInitialized

||| Guard for requests that cannot be sent after the shutdown protocol.
whenNotShutdownRequest : Ref LSPConf LSPConfiguration => Core (Either ResponseError a) -> Core (Either ResponseError a)
whenNotShutdownRequest k =
  if !(gets LSPConf isShutdown)
     then do logE Server "Cannot process requests after shutdown"
             pure $ Left $ invalidRequest "Server has been shutdown"
     else k

||| whenInitializedRequest + whenNotShutdownRequest
whenActiveRequest : Ref LSPConf LSPConfiguration => (InitializeParams -> Core (Either ResponseError a)) -> Core (Either ResponseError a)
whenActiveRequest = whenNotShutdownRequest . whenInitializedRequest

||| Guard for notifications that requires a successful initialization before being allowed.
whenInitializedNotification : Ref LSPConf LSPConfiguration => (InitializeParams -> Core ()) -> Core ()
whenInitializedNotification k =
  case !(gets LSPConf initialized) of
       Just conf => k conf
       Nothing => do logE Server "Cannot process notification before initialization"
                     sendUnknownResponseMessage $ serverNotInitialized

||| Guard for notifications that cannot be sent after the shutdown protocol.
whenNotShutdownNotification : Ref LSPConf LSPConfiguration => Core () -> Core ()
whenNotShutdownNotification k =
  if !(gets LSPConf isShutdown)
     then do logE Server "Cannot process notifications after shutdown"
             sendUnknownResponseMessage $ invalidRequest "Server has been shutdown"
     else k

||| whenInitializedNotification + whenNotShutdownNotification
whenActiveNotification : Ref LSPConf LSPConfiguration => (InitializeParams -> Core ()) -> Core ()
whenActiveNotification = whenNotShutdownNotification . whenInitializedNotification

export
handleRequest :
       Ref LSPConf LSPConfiguration
    => Ref Ctxt Defs
    => Ref UST UState
    => Ref Syn SyntaxInfo
    => Ref MD Metadata
    => Ref ROpts REPLOpts
    => (method : Method Client Request)
    -> (params : MessageParams method)
    -> Core (Either ResponseError (ResponseResult method))

handleRequest Initialize params = do
  -- TODO: Here we should analyze the client capabilities.
  logI Channel "Received initialization request"

  case params.initializationOptions of
       Just (JObject xs) => do
         case lookup "logFile" xs of
              Just (JString fname) => changeLogFile fname
              Just _ => logE Configuration "Incorrect type for log file location, expected string"
              Nothing => pure ()
         case lookup "longActionTimeout" xs of
              Just (JNumber v) => setSearchTimeout $ cast v
              Just _ => logE Configuration "Incorrect type for long action timeout, expected number"
              Nothing => pure ()
         case lookup "maxCodeActionResults" xs of
              Just (JNumber v) => update LSPConf (record { searchLimit = integerToNat $ cast v })
              Just _ => logE Configuration "Incorrect type for max code action results, expected number"
              Nothing => pure ()
       Just _ => logE Configuration "Incorrect type for initialization options"
       Nothing => pure ()

  update LSPConf (record {initialized = Just params})
  logI Server "Server initialized and configured"
  pure $ pure $ MkInitializeResult serverCapabilities (Just serverInfo)

handleRequest Shutdown params = do
  logI Channel "Received shutdown request"
  -- In a future multithreaded model, we must guarantee that all pending request are still executed.
  update LSPConf (record {isShutdown = True})
  logI Server "Server ready to be shutdown"
  pure $ pure $ (the (Maybe Null) Nothing)

handleRequest TextDocumentHover params = whenActiveRequest $ \conf => do
  logI Channel "Received hover request for \{show params.textDocument.uri}"
  False <- isDirty params.textDocument.uri
    | True => do logW Hover "\{show params.textDocument.uri} has unsaved changes, cannot complete the request"
                 pure $ pure $ make $ MkNull
  withURI conf params.textDocument.uri Nothing (pure $ pure $ make $ MkNull) $ do
    Nothing <- gets LSPConf (map snd . head' . searchPos (cast params.position) . cachedHovers)
      | Just hover => do logD Hover "Found cached action"
                         pure $ pure $ make hover

    defs <- get Ctxt
    nameLocs <- gets MD nameLocMap

    let Just (loc, name) = findPointInTreeLoc (params.position.line, params.position.character) nameLocs
      | Nothing => pure $ pure $ (make $ MkHover (make $ MkMarkupContent PlainText "") Nothing)
    logD Hover "Found name \{show name}"
    -- Lookup the name globally
    globals <- lookupCtxtName name (gamma defs)
    globalResult <- the (Core $ Maybe $ Doc IdrisAnn) $ case globals of
      [] => pure Nothing
      ts => do tys <- traverse (displayType defs) ts
               pure $ Just (vsep tys)
    localResult <- findTypeAt $ anyWithName name $ within (params.position.line, params.position.character)
    line <- case (globalResult, localResult) of
      -- Give precedence to the local name, as it shadows the others
      (_, Just (n, _, type)) => pure $ renderString $ unAnnotateS $ layoutUnbounded $ pretty (nameRoot n) <++> colon <++> !(displayTerm defs type)
      (Just globalDoc, Nothing) => pure $ renderString $ unAnnotateS $ layoutUnbounded globalDoc
      (Nothing, Nothing) => pure ""
    let supportsMarkup = maybe False (Markdown `elem`) $ conf.capabilities.textDocument >>= .hover >>= .contentFormat
    let markupContent = the MarkupContent $ if supportsMarkup then MkMarkupContent Markdown $ "```idris\n" ++ line ++ "\n```" else MkMarkupContent PlainText line
    let hover = MkHover (make markupContent) Nothing
    update LSPConf (record { cachedHovers $= insert (cast loc, hover) })
    pure $ pure (make hover)

handleRequest TextDocumentDefinition params = whenActiveRequest $ \conf => do
  logI Channel "Received gotoDefinition request for \{show params.textDocument.uri}"
  False <- isDirty params.textDocument.uri
    | True => do logW GotoDefinition "\{show params.textDocument.uri} has unsaved changes, cannot complete the request"
                 pure $ pure $ make $ MkNull
  withURI conf params.textDocument.uri Nothing (pure $ pure $ make $ MkNull) $ do
    Just link <- gotoDefinition params | Nothing => pure $ pure $ make MkNull
    pure $ pure $ make link

handleRequest TextDocumentCodeAction params = whenActiveRequest $ \conf => do
  logI Channel "Received codeAction request for \{show params.textDocument.uri}"
  False <- isDirty params.textDocument.uri
    | True => do logW CodeAction "\{show params.textDocument.uri} has unsaved changes, cannot complete the request"
                 pure $ pure $ make $ MkNull
  withURI conf params.textDocument.uri Nothing (pure $ pure $ make $ MkNull) $ do
    quickfixActions <- map Just <$> gets LSPConf quickfixes
    exprSearchAction <- map Just <$> exprSearch params
    splitAction <- caseSplit params
    lemmaAction <- makeLemma params
    withAction <- makeWith params
    clauseAction <- addClause params
    makeCaseAction <- handleMakeCase params
    generateDefAction <- map Just <$> generateDef params
    refineHoleAction <- map Just <$> refineHole params
    let resp = flatten $ quickfixActions ++ refineHoleAction
                           ++ [splitAction, lemmaAction, withAction, clauseAction, makeCaseAction]
                           ++ generateDefAction ++ exprSearchAction
    pure $ pure $ make resp
    where
      flatten : List (Maybe CodeAction) -> List (OneOf [Command, CodeAction])
      flatten [] = []
      flatten (Nothing :: xs) = flatten xs
      flatten ((Just x) :: xs) = make x :: flatten xs

handleRequest TextDocumentSignatureHelp params = whenActiveRequest $ \conf => do
  logI Channel "Received signatureHelp request for \{show params.textDocument.uri}"
  False <- isDirty params.textDocument.uri
    | True => do logW SignatureHelp "\{show params.textDocument.uri} has unsaved changes, cannot complete the request"
                 pure $ pure $ make $ MkNull
  withURI conf params.textDocument.uri Nothing (pure $ pure $ make $ MkNull) $ do
    Just signatureHelpData <- signatureHelp params | Nothing => pure $ pure $ make MkNull
    pure $ pure $ make signatureHelpData

handleRequest TextDocumentDocumentSymbol params = whenActiveRequest $ \conf => do
  logI Channel "Received documentSymbol request for \{show params.textDocument.uri}"
  False <- isDirty params.textDocument.uri
    | True => do logW DocumentSymbol "\{show params.textDocument.uri} has unsaved changes, cannot complete the request"
                 pure $ pure $ make $ MkNull
  withURI conf params.textDocument.uri Nothing (pure $ pure $ make $ MkNull) $ do
    documentSymbolData <- documentSymbol params
    pure $ pure $ make documentSymbolData

handleRequest TextDocumentCodeLens params = whenActiveRequest $ \conf => do
  -- TODO: still unimplemented, but send empty message to avoid errors
  -- in clients since it's a common request
  logW Channel $ "Received an unsupported codeLens request"
  pure $ pure $ make MkNull

handleRequest TextDocumentCompletion params = whenActiveRequest $ \conf => do
  -- TODO: still unimplemented, but send empty message to avoid errors
  -- in clients since it's a common request
  logW Channel $ "Received an unsupported completion request"
  pure $ pure $ make MkNull

handleRequest TextDocumentDocumentLink params = whenActiveRequest $ \conf => do
  -- TODO: still unimplemented, but send empty message to avoid errors
  -- in clients since it's a common request
  logW Channel $ "Received an unsupported documentLink request"
  pure $ pure $ make MkNull

handleRequest TextDocumentSemanticTokensFull params = whenActiveRequest $ \conf => do
    False <- isDirty params.textDocument.uri
      | True => pure $ Left (MkResponseError RequestCancelled "Document Dirty" JNull)
    False <- gets LSPConf (contains params.textDocument.uri . semanticTokensSentFiles)
      | True => pure $ Left (MkResponseError RequestCancelled "Semantic tokens already sent" JNull)
    withURI conf params.textDocument.uri Nothing (pure $ Left (MkResponseError RequestCancelled "Document Errors" JNull)) $ do
      md <- get MD
      src <- getSource
      let srcLines = forget $ lines src
      let getLineLength = \lineNum => maybe 0 (cast . length) $ elemAt srcLines (integerToNat (cast lineNum))
      tokens <- getSemanticTokens md getLineLength
      update LSPConf (record { semanticTokensSentFiles $= insert params.textDocument.uri })
      pure $ pure $ (make $ tokens)
handleRequest WorkspaceExecuteCommand
  (MkExecuteCommandParams partialResultToken "repl" (Just [json])) = whenActiveRequest $ \conf => do
    let JString cmd  = json
      | _ => do pure $ Left (invalidParams "Expected String")
    c <- getColor
    -- Turn off the colour, because JSON
    -- seems to fail to correctly escape the codes.
    setColor False
    res <- interpret cmd
    doc <- replResultToDoc res
    str <- render doc
    setColor c
    pure $ Right (JString str)
handleRequest method params = whenActiveRequest $ \conf => do
    logW Channel $ "Received a not supported \{show (toJSON method)} request"
    pure $ Left methodNotFound

export
handleNotification :
       Ref LSPConf LSPConfiguration
    => Ref Ctxt Defs
    => Ref UST UState
    => Ref Syn SyntaxInfo
    => Ref MD Metadata
    => Ref ROpts REPLOpts
    => (method : Method Client Notification)
    -> (params : MessageParams method)
    -> Core ()

handleNotification Exit params = do
  logI Channel "Received exit notification"
  status <- if !(gets LSPConf isShutdown)
               then logI Server "Quitting the server..." >> pure ExitSuccess
               else logC Server "Quitting the server without a proper shutdown" >> pure (ExitFailure 1)
  coreLift $ exitWith status

handleNotification TextDocumentDidOpen params = whenActiveNotification $ \conf => do
  logI Channel "Received didOpen notification for \{show params.textDocument.uri}"
  ignore $ loadURI conf params.textDocument.uri (Just params.textDocument.version)

handleNotification TextDocumentDidSave params = whenActiveNotification $ \conf => do
  logI Channel "Received didSave notification for \{show params.textDocument.uri}"
  update LSPConf (record
    { dirtyFiles $= delete params.textDocument.uri
    , errorFiles $= delete params.textDocument.uri
    , semanticTokensSentFiles $= delete params.textDocument.uri
    })
  ignore $ loadURI conf params.textDocument.uri Nothing
  when (fromMaybe False $ conf.capabilities.workspace >>= semanticTokens >>= refreshSupport) $ do
    logI SemanticTokens "Sending semantic tokens for \{show params.textDocument.uri}"
    sendRequestMessage_ WorkspaceSemanticTokensRefresh Nothing

handleNotification TextDocumentDidChange params = whenActiveNotification $ \conf => do
  logI Channel "Received didChange notification for \{show params.textDocument.uri}"
  update LSPConf (record { dirtyFiles $= insert params.textDocument.uri })
  logI Server "File \{show params.textDocument.uri} marked as dirty"

handleNotification TextDocumentDidClose params = whenActiveNotification $ \conf => do
  logI Channel "Received didClose notification for \{show params.textDocument.uri}"
  update LSPConf (record { openFile = Nothing
                         , quickfixes = []
                         , cachedActions = empty
                         , cachedHovers = empty
                         , dirtyFiles $= delete params.textDocument.uri
                         , errorFiles $= delete params.textDocument.uri
                         , semanticTokensSentFiles $= delete params.textDocument.uri
                         })
  logI Server $ "File \{show params.textDocument.uri} closed"

handleNotification method params = whenActiveNotification $ \conf =>
  logW Channel "Received unhandled notification for method \{stringify $ toJSON method}"


text:
module Eval

import Control.ST
import Control.ST.Exception
import DataTypes
import Util
import Lists
import Numbers
import Ratio
import Strings
import Vector
import Data.Complex
import Data.Complex
import Primitives
import Data.SortedMap
import Environment
import Data.IORef

%access public export
--------------
-- Eval
--------------
makeFunc : String -> Maybe String -> EnvRef LispVal -> List LispVal -> List LispVal -> LispVal
makeFunc name varargs envRef params body = LispFunc name (map showVal params) varargs body envRef

makeNormalFunc : String -> EnvRef LispVal -> List LispVal -> List LispVal -> LispVal
makeNormalFunc name = makeFunc name Nothing

makeVarArgs : String -> LispVal -> EnvRef LispVal -> List LispVal -> List LispVal -> LispVal
makeVarArgs name varargs = makeFunc name (Just $ showVal varargs)

getHeads : Context m => List LispVal -> ST m LispVal []
getHeads [] = pure $ LispList []
getHeads (LispList (x::_)::ys) = do
  LispList result <- getHeads ys
  pure $ LispList (x :: result)
getHeads _ = throw $ Default "Unexpected error (getHeads)"

getTails : Context m => List LispVal -> ST m LispVal []
getTails [] = pure $ LispList []
getTails (LispList [_, xs]::ys) = do
  LispList result <- getTails ys
  pure $ LispList (xs :: result)
getTails _ = throw $ Default "Unexpected error (getTails)"

ensureAtom : Context m => LispVal -> ST m LispVal []
ensureAtom n@(LispAtom _) = pure n
ensureAtom _ = throw $ Default "Type error"

ensureAtoms : Context m => List LispVal -> ST m LispVal []
ensureAtoms [] = pure LispVoid
ensureAtoms (x::xs) = do
  ensureAtom x
  ensureAtoms xs

extractVar : LispVal -> String
extractVar (LispAtom atom) = atom

liftThrows : Context m => ThrowsError a -> ST m a []
liftThrows (Left err) = throw err
liftThrows (Right val) = pure val

mutual
    evalArgs : Context m => EnvRef LispVal -> List LispVal -> ST m (List LispVal) []
    evalArgs _ [] = pure []
    evalArgs {m} envRef (x::xs) = do
        arg <- eval envRef x
        args <- evalArgs envRef xs
        pure $ (arg :: args)

    evalList : Context m => EnvRef LispVal -> List LispVal -> ST m LispVal []
    evalList _ [] = pure LispVoid
    evalList {m} envRef [a] = eval envRef a
    evalList {m} envRef (y::ys) = do
        eval envRef y
        evalList envRef ys

    --------------
    -- Apply
    --------------
    apply' : Context m => LispVal -> List LispVal -> ST m (LispVal) []
    -- apply (LispPrimitiveFunc _ func) args = func args
    apply' {m} (LispPrimitiveFunc _ func) args = liftThrows $ func args
    apply' {m} (LispFunc _ params varargs body closure) args =
      if length params /= length args && isNothing varargs
        then throw $ NumArgs (Min $ cast $ length params) (cast $ length args) args
        else do env' <- bindVars closure $ zip params args ++ varargs'
                (x::xs) <- evalBody env' body
                pure $ last (x::xs)

      where
        remainingArgs : List LispVal
        remainingArgs = drop (length params) args
        evalBody : Context m => EnvRef LispVal -> List LispVal -> ST m (List LispVal) []
        evalBody env [] = pure []
        evalBody env (x::xs) = do v <- eval env x
                                  vs <- evalBody env xs
                                  pure (v :: vs)
        varargs' : List (String, LispVal)
        varargs' =
          case varargs of
            Just argName => [(argName, LispList $ remainingArgs)]
            Nothing => []
    -- apply' {m} (LispFunc _ params varargs body closure) args =
    --     if length params /= length args && isNothing varargs
    --     then throw $ NumArgs (Min $ cast $ length params) (cast $ length args) args
    --     else do (x::xs) <- evalBody !localEnv body
    --             pure $ last (x :: xs)
    --     where
    --         traverse' : Context m => (LispVal -> ST m LispVal []) -> List LispVal -> ST m (List LispVal) []
    --         traverse' f [] = pure []
    --         traverse' f (x::xs) = do v <- f x
    --                                  vs <- traverse' f xs
    --                                  pure (v :: vs)
    --         -- remainingArgs = drop (length params) args
    --         varArgs : List (String, LispVal)
    --         varArgs = let remaining = drop (length params) args in
    --                 case varargs of
    --                      Nothing  => []
    --                      Just arg => [(arg, LispList remaining)]
    --         localEnv : Context m => ST m (EnvRef LispVal) []
    --         localEnv = bindVars closure $ zip params args ++ varArgs
    --         evalBody : Context m => EnvRef LispVal -> List LispVal -> ST m (List LispVal) []
    --         evalBody env = traverse' (eval env)

-- HERE!

        -- num = toInteger . length
        -- evalBody env = fmap last $ mapM (eval env) body'
    -- apply' {m} (LispFunc _ params varargs body closure) args
    --       = if length params /= length args && varargs == Nothing
    --            then throw $ NumArgs (Min $ cast $ length params) (cast $ length args) args
    --            else do (x :: xs) <- evalBody !localEnv body
    --                    pure $ last (x :: xs)
    --       where optArg : List (String, LispVal)
    --             optArg
    --               = let remaining = drop (length params) args in
    --                     case varargs of
    --                          Nothing  => []
    --                          Just arg => [(arg, LispList remaining)]
    --             localEnv : Context m => ST m (EnvRef LispVal) []
    --             localEnv = bindVars closure $ zip params args ++ optArg
    --             evalBody : Context m => EnvRef LispVal -> List LispVal -> ST m (List LispVal) []
    --             evalBody env = traverseE (eval env)
    -- apply' (LispIOFunc _ func) args = func args
    apply' f _ = throw $ Default $
        "application: not a procedure; " ++
        "expected a procedure that can be applied to arguments; given: " ++ show f

    -- applyProc :: IOPrimitiveFunc
    -- applyProc [func, List args] = apply func args
    -- applyProc (func:args) = apply func args
    -- applyProc _ = throw $ Default "applyProc error"
    --
    -- readProc :: IOPrimitiveFunc
    -- readProc [] = readProc [Port stdin]
    -- readProc [Port port] = (liftIO $ hGetLine port) >>= liftThrows . readExpr
    -- readProc _ = throw $ Default "readProc error"
    --
    -- load :: String -> IOThrowsError [LispVal]
    -- load filename = (liftIO $ readFile filename) >>= liftThrows . readExprList
    --
    -- readAll :: IOPrimitiveFunc
    -- readAll [String filename] = fmap List $ load filename
    -- readAll _ = throw $ Default "readAll error"

    eval : Context m => EnvRef LispVal -> LispVal -> ST m LispVal []
    eval {m} _ val@LispVoid = pure val
    eval {m} _ val@(LispString _) = pure val
    eval {m} _ val@(LispCharacter _) = pure val
    eval {m} _ val@(LispInteger _) = pure val
    eval {m} _ val@(LispVector _ _) = pure val
    eval {m} _ (LispRational val) =
      if denominator val == 1
        then pure $ LispInteger $ numerator val
        else pure $ LispRational val
    eval {m} _ val@(LispFloat _) = pure val
    eval {m} _ (LispComplex val) =
      if imagPart val == 0
        then pure $ LispFloat $ realPart val
        else pure $ LispComplex val
    eval {m} _ val@(LispBool _) = pure val
    eval {m} _ (LispList [LispAtom "quote", val]) = pure val
    eval {m} envRef (LispList [LispAtom "if", pred', conseq, alt]) =
        do result <- eval envRef pred'
           case result of
                LispBool False => eval envRef alt
                _ => eval envRef conseq
    eval {m} envRef (LispList ((LispAtom "cond")::xs)) = evalCond xs
        -- TODO: [test-expr => proc-expr]
      where
        evalCond : List LispVal -> ST m LispVal []
        evalCond [] = pure LispVoid
        evalCond [LispList (LispAtom "else"::xs')] =
            evalList envRef xs'
        evalCond (LispList (LispAtom "else"::_)::_) =
          throw $ Default "cond: bad syntax (`else` clause must be last)"
        evalCond ((LispList (pred'::conseqs))::xs') = do
          result <- eval envRef pred'
          case result of
            LispBool False => evalCond xs'
            _ =>
              case conseqs of
                [] => pure result
                _ => evalList envRef conseqs
        evalCond a = throw $ Default (show a)
    eval {m} envRef (LispList ((LispAtom "case")::key::clauses)) =
        do result <- eval envRef key
           evalClauses result clauses
        where
            inList : List LispVal -> ST m Bool []
            inList [_, LispList []] = pure False
            inList [_, (LispAtom "else")] = pure True
            inList [_, LispList (LispAtom "else"::_)] = throw $ Default "case: bad syntax (`else` clause must be last)"
            inList [key', LispList (x::xs)] =
                do eq <- liftThrows $ eqv [x, key']
                   case eq of
                        LispBool True => pure True
                        _ => inList [key', LispList xs]
            inList a = throw $ Default $ "case: bad syntax"
            evalClauses : LispVal -> List LispVal -> ST m LispVal []
            evalClauses _ [] = pure LispVoid
            evalClauses _ [LispList []] = pure LispVoid
            evalClauses key' (LispList (datum::exprs)::rest) =
                do
                    match <- call $ inList [key', datum]
                    case match of
                        True => evalList envRef exprs
                        False => evalClauses key' rest
            evalClauses _ _ = throw $ Default "case: bad syntax"
    eval {m} _ (LispList ((LispAtom "case")::_)) =
      throw $ Default "case: bad syntax in: (case)"
    eval {m} envRef (LispList [LispAtom "set!", LispAtom var, form]) =
        do val <- eval envRef form
           setVar envRef var val
           pure LispVoid
    eval {m} envRef (LispList [LispAtom "set-car!", LispAtom var, form]) =
        do newVal <- eval envRef form
           ls <- getVar envRef var
           setCar envRef ls newVal
           pure LispVoid
        where
            setCar : EnvRef LispVal -> Maybe LispVal -> LispVal -> ST m Bool []
            setCar envRef (Just (LispList (x::xs))) newVal = setVar envRef var (LispList (newVal::xs))
            setCar envRef (Just (LispDottedList (x::xs) v)) newVal = setVar envRef var (LispDottedList (newVal::xs) v)
            setCar _ _ _ = throw $ TypeMismatch "list" form
    eval {m} envRef (LispList [LispAtom "define", LispAtom var, form]) =
        do val <- eval envRef form
           defineVar envRef var val
           pure LispVoid
    eval {m} envRef (LispList (LispAtom "define"::LispList (LispAtom var::params)::body)) =
        do defineVar envRef var (makeNormalFunc var envRef params body)
           pure LispVoid
    eval {m} envRef (LispList (LispAtom "define"::LispDottedList (LispAtom var::params) varargs::body)) =
        do let val = makeVarArgs var varargs envRef params body
           defineVar envRef var val
           pure LispVoid
    eval {m} envRef (LispList (LispAtom "lambda"::LispList params::body)) = do
        s <- showEnv envRef
        pure $ makeNormalFunc "λ" envRef params body
    eval {m} envRef (LispList (LispAtom "lambda"::varargs@(LispAtom _)::body)) =
        pure $ makeVarArgs "λ" varargs envRef [] body
    eval {m} envRef (LispList (LispAtom "lambda"::LispDottedList params varargs::body)) =
        pure $ makeVarArgs "λ" varargs envRef params body
    eval {m} envRef (LispList (LispAtom "let"::LispList pairs::body)) = do
            LispList atoms <- getHeads pairs
            ensureAtoms atoms
            LispList vals <- getTails pairs
            args <- evalArgs envRef vals
            envRef' <- bindVars envRef (zipWith (\a, b => (extractVar a, b)) atoms args)
            evalList envRef' body
    eval {m} envRef (LispList (LispAtom "let*"::LispList pairs::body)) = do
            LispList atoms <- getHeads pairs
            ensureAtoms atoms
            LispList vals <- getTails pairs
            envRef' <- bindVars envRef []
            buildEnv envRef' atoms vals
            evalList envRef' body
        where
        buildEnv : EnvRef LispVal -> List LispVal -> List LispVal -> ST m () []
        buildEnv env [] [] = pure ()
        buildEnv env (atomH::atomT) (valH::valT) = do
            val <- eval env valH
            defineVar env (extractVar atomH) val
            buildEnv env atomT valT
        buildEnv _ _ _ = throw $ Default "let*: bad syntax"
    eval {m} envRef (LispList (LispAtom "letrec"::LispList pairs::body)) = do
            LispList atoms <- getHeads pairs
            ensureAtoms atoms
            LispList vals <- getTails pairs
            envRef' <- bindVars envRef []
            buildEnv envRef' atoms
            args <- evalArgs envRef' vals
            setRec envRef' (zipWith (\a, b => (extractVar a, b)) atoms args)
            evalList envRef' body
        where
            buildEnv : EnvRef LispVal -> List LispVal -> ST m () []
            buildEnv env [] = pure ()
            buildEnv env (atomH::atomT) = do
                defineVar env (extractVar atomH) LispVoid
                buildEnv env atomT
            buildEnv _ _ = throw $ Default "let*: bad syntax"
            setRec : EnvRef LispVal -> List (String, LispVal) -> ST m () []
            setRec env [] = pure ()
            setRec env ((n,v)::xs) = do
                setVar env n v
                setRec env xs
    eval {m} envRef (LispList [LispAtom "print", expr1]) = do
        -- TODO: REMOVE
        result <- eval envRef expr1
        putStr $ show result ++ "\n"
        pure LispVoid
    -- eval envRef (LispList [LispAtom "load", String filename]) = do
    --   f <- load filename
    --   _ <- traverse_ (eval env) f
    --   pure LispVoid
    -- eval envRef (List [Atom "load-print", String filename]) =
    --   load filename >>= fmap List . mapM (eval env)
    -- eval envRef (List (Atom "vector-set!":args)) =
    --   case args of
    --     [Atom var, Integer n, v] -> do
    --       Vector vec <- getVar envRef var
    --       if n < (fromIntegral $ length vec)
    --         then setVar envRef var $ Vector $ vec // [(n, v)]
    --         else throw $ outOfBoundsError "vector-ref" n vec
    --     [a, b, c] ->
    --       throw $ TypeMismatch "vector, integer, integer" $ List [a, b, c]
    --     a -> throw $ NumArgs (MinMax 3 3) (length args) a
    eval {m} envRef (LispList [LispAtom "apply", function, args]) =
        do
            -- (LispList (LispAtom "letrec"::LispList pairs::body))
            s <- showEnv envRef
            func <- eval envRef function
            argVals <- evalArgs envRef [args]
            unpacked <- unpackArgs argVals
            results <- apply' func unpacked
            pure $ results
        where
            unpackArgs : List LispVal -> ST m (List LispVal) []
            unpackArgs [LispList xs] = pure xs
            unpackArgs [arg] = throw $ TypeMismatch "list" arg
            unpackArgs args = throw $ NumArgs (MinMax 2 2) (cast $ length args) args
    eval envRef (LispList (function::args)) = do
        s <- showEnv envRef
        func <- eval envRef function
        argVals <- evalArgs envRef args
        results <- apply' func argVals
        pure $ results
    eval {m} envRef (LispAtom name) = do
        var <- getVar envRef name
        case var of
            Nothing => throw $ Default $ "Unknown atom: " ++ name
            Just var' => pure var'
    eval _ badForm = throw $ BadSpecialForm "Unrecognized special form" badForm

--------------
-- Env
-- Bindings
-- Primitives
--------------
nullEnv : Context m => ST m (EnvRef LispVal) []
nullEnv = initEnv []

primitiveBindings : Context m => ST m (EnvRef LispVal) []
primitiveBindings {m} = initEnv $ map (makeFunc' LispPrimitiveFunc) primitives
    where
        makeFunc' : (String -> (List LispVal -> a) -> LispVal) -> (String, (List LispVal -> a)) -> (String, LispVal)
        makeFunc' constr (var, func) = (var, constr var func)

-- | PrimitiveFunc String
--                   PrimitiveFunc
--   | Func { name :: String
--          , params :: [String]
--          , vararg :: (Maybe String)
--          , body :: [LispVal]
--          , closure :: Env }

-- -- loadStdLib :: Env -> IO Env
-- -- loadStdLib envRef = do
-- --   filename <- liftIO $ getDataFileName "lib/stdlib.scm"
-- --   _ <- evalString envRef $ "(load \"" ++ filename ++ "\")"
-- --   pure env
-- --

max_stars_repo_name: ebenpack/lidrisp

max_issues_repo_name: ebenpack/lidrisp

max_forks_repo_name: ebenpack/lidrisp