text:
module Web.Raw.Serviceworker

import JS
import Web.Internal.ServiceworkerPrim
import Web.Internal.Types

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

namespace Cache

  export
  addAll :  (obj : Cache)
         -> (requests : Array (Union2 Request String))
         -> JSIO (Promise Undefined)
  addAll a b = primJS $ Cache.prim__addAll a b

  export
  add :  (obj : Cache)
      -> (request : NS I [ Request , String ])
      -> JSIO (Promise Undefined)
  add a b = primJS $ Cache.prim__add a (toFFI b)

  export
  delete :  (0 _ : JSType t1)
         => {auto 0 _ : Elem CacheQueryOptions (Types t1)}
         -> (obj : Cache)
         -> (request : NS I [ Request , String ])
         -> (options : Optional t1)
         -> JSIO (Promise Boolean)
  delete a b c = primJS $ Cache.prim__delete a (toFFI b) (optUp c)

  export
  delete' :  (obj : Cache)
          -> (request : NS I [ Request , String ])
          -> JSIO (Promise Boolean)
  delete' a b = primJS $ Cache.prim__delete a (toFFI b) undef

  export
  keys :  (0 _ : JSType t1)
       => {auto 0 _ : Elem CacheQueryOptions (Types t1)}
       -> (obj : Cache)
       -> (request : Optional (NS I [ Request , String ]))
       -> (options : Optional t1)
       -> JSIO (Promise (Array Request))
  keys a b c = primJS $ Cache.prim__keys a (toFFI b) (optUp c)

  export
  keys' : (obj : Cache) -> JSIO (Promise (Array Request))
  keys' a = primJS $ Cache.prim__keys a undef undef

  export
  matchAll :  (0 _ : JSType t1)
           => {auto 0 _ : Elem CacheQueryOptions (Types t1)}
           -> (obj : Cache)
           -> (request : Optional (NS I [ Request , String ]))
           -> (options : Optional t1)
           -> JSIO (Promise (Array Response))
  matchAll a b c = primJS $ Cache.prim__matchAll a (toFFI b) (optUp c)

  export
  matchAll' : (obj : Cache) -> JSIO (Promise (Array Response))
  matchAll' a = primJS $ Cache.prim__matchAll a undef undef

  export
  match :  (0 _ : JSType t1)
        => {auto 0 _ : Elem CacheQueryOptions (Types t1)}
        -> (obj : Cache)
        -> (request : NS I [ Request , String ])
        -> (options : Optional t1)
        -> JSIO (Promise (Union2 Response Undefined))
  match a b c = primJS $ Cache.prim__match a (toFFI b) (optUp c)

  export
  match' :  (obj : Cache)
         -> (request : NS I [ Request , String ])
         -> JSIO (Promise (Union2 Response Undefined))
  match' a b = primJS $ Cache.prim__match a (toFFI b) undef

  export
  put :  (obj : Cache)
      -> (request : NS I [ Request , String ])
      -> (response : Response)
      -> JSIO (Promise Undefined)
  put a b c = primJS $ Cache.prim__put a (toFFI b) c

namespace CacheStorage

  export
  delete :  (obj : CacheStorage)
         -> (cacheName : String)
         -> JSIO (Promise Boolean)
  delete a b = primJS $ CacheStorage.prim__delete a b

  export
  has : (obj : CacheStorage) -> (cacheName : String) -> JSIO (Promise Boolean)
  has a b = primJS $ CacheStorage.prim__has a b

  export
  keys : (obj : CacheStorage) -> JSIO (Promise (Array String))
  keys a = primJS $ CacheStorage.prim__keys a

  export
  match :  (0 _ : JSType t1)
        => {auto 0 _ : Elem MultiCacheQueryOptions (Types t1)}
        -> (obj : CacheStorage)
        -> (request : NS I [ Request , String ])
        -> (options : Optional t1)
        -> JSIO (Promise (Union2 Response Undefined))
  match a b c = primJS $ CacheStorage.prim__match a (toFFI b) (optUp c)

  export
  match' :  (obj : CacheStorage)
         -> (request : NS I [ Request , String ])
         -> JSIO (Promise (Union2 Response Undefined))
  match' a b = primJS $ CacheStorage.prim__match a (toFFI b) undef

  export
  open_ : (obj : CacheStorage) -> (cacheName : String) -> JSIO (Promise Cache)
  open_ a b = primJS $ CacheStorage.prim__open a b

namespace Client

  export
  frameType :  (0 _ : JSType t1)
            => {auto 0 _ : Elem Client (Types t1)}
            -> (obj : t1)
            -> JSIO FrameType
  frameType a = tryJS "Client.frameType" $ Client.prim__frameType (up a)

  export
  id :  (0 _ : JSType t1)
     => {auto 0 _ : Elem Client (Types t1)}
     -> (obj : t1)
     -> JSIO String
  id a = primJS $ Client.prim__id (up a)

  export
  type :  (0 _ : JSType t1)
       => {auto 0 _ : Elem Client (Types t1)}
       -> (obj : t1)
       -> JSIO ClientType
  type a = tryJS "Client.type" $ Client.prim__type (up a)

  export
  url :  (0 _ : JSType t1)
      => {auto 0 _ : Elem Client (Types t1)}
      -> (obj : t1)
      -> JSIO String
  url a = primJS $ Client.prim__url (up a)

  export
  postMessage :  (0 _ : JSType t1)
              => {auto 0 _ : Elem Client (Types t1)}
              -> (obj : t1)
              -> (message : Any)
              -> (transfer : Array Object)
              -> JSIO ()
  postMessage a b c = primJS $ Client.prim__postMessage (up a) (toFFI b) c

  export
  postMessage1 :  (0 _ : JSType t1)
               => (0 _ : JSType t2)
               => {auto 0 _ : Elem Client (Types t1)}
               -> {auto 0 _ : Elem PostMessageOptions (Types t2)}
               -> (obj : t1)
               -> (message : Any)
               -> (options : Optional t2)
               -> JSIO ()
  postMessage1 a b c = primJS
                     $ Client.prim__postMessage1 (up a) (toFFI b) (optUp c)

  export
  postMessage1' :  (0 _ : JSType t1)
                => {auto 0 _ : Elem Client (Types t1)}
                -> (obj : t1)
                -> (message : Any)
                -> JSIO ()
  postMessage1' a b = primJS $ Client.prim__postMessage1 (up a) (toFFI b) undef

namespace Clients

  export
  claim : (obj : Clients) -> JSIO (Promise Undefined)
  claim a = primJS $ Clients.prim__claim a

  export
  get :  (obj : Clients)
      -> (id : String)
      -> JSIO (Promise (Union2 Client Undefined))
  get a b = primJS $ Clients.prim__get a b

  export
  matchAll :  (0 _ : JSType t1)
           => {auto 0 _ : Elem ClientQueryOptions (Types t1)}
           -> (obj : Clients)
           -> (options : Optional t1)
           -> JSIO (Promise (Array Client))
  matchAll a b = primJS $ Clients.prim__matchAll a (optUp b)

  export
  matchAll' : (obj : Clients) -> JSIO (Promise (Array Client))
  matchAll' a = primJS $ Clients.prim__matchAll a undef

  export
  openWindow :  (obj : Clients)
             -> (url : String)
             -> JSIO (Promise (Nullable WindowClient))
  openWindow a b = primJS $ Clients.prim__openWindow a b

namespace ExtendableEvent

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

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

  export
  waitUntil :  (0 _ : JSType t1)
            => {auto 0 _ : Elem ExtendableEvent (Types t1)}
            -> (obj : t1)
            -> (f : Promise AnyPtr)
            -> JSIO ()
  waitUntil a b = primJS $ ExtendableEvent.prim__waitUntil (up a) b

namespace ExtendableMessageEvent

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

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

  export
  data_ : (obj : ExtendableMessageEvent) -> JSIO Any
  data_ a = tryJS "ExtendableMessageEvent.data_"
          $ ExtendableMessageEvent.prim__data a

  export
  lastEventId : (obj : ExtendableMessageEvent) -> JSIO String
  lastEventId a = primJS $ ExtendableMessageEvent.prim__lastEventId a

  export
  origin : (obj : ExtendableMessageEvent) -> JSIO String
  origin a = primJS $ ExtendableMessageEvent.prim__origin a

  export
  ports : (obj : ExtendableMessageEvent) -> JSIO (Array MessagePort)
  ports a = primJS $ ExtendableMessageEvent.prim__ports a

  export
  source :  (obj : ExtendableMessageEvent)
         -> JSIO (Maybe (NS I [ Client , ServiceWorker , MessagePort ]))
  source a = tryJS "ExtendableMessageEvent.source"
           $ ExtendableMessageEvent.prim__source a

namespace FetchEvent

  export
  new :  (0 _ : JSType t1)
      => {auto 0 _ : Elem FetchEventInit (Types t1)}
      -> (type : String)
      -> (eventInitDict : t1)
      -> JSIO FetchEvent
  new a b = primJS $ FetchEvent.prim__new a (up b)

  export
  clientId : (obj : FetchEvent) -> JSIO String
  clientId a = primJS $ FetchEvent.prim__clientId a

  export
  handled : (obj : FetchEvent) -> JSIO (Promise Undefined)
  handled a = primJS $ FetchEvent.prim__handled a

  export
  preloadResponse : (obj : FetchEvent) -> JSIO (Promise AnyPtr)
  preloadResponse a = primJS $ FetchEvent.prim__preloadResponse a

  export
  replacesClientId : (obj : FetchEvent) -> JSIO String
  replacesClientId a = primJS $ FetchEvent.prim__replacesClientId a

  export
  request : (obj : FetchEvent) -> JSIO Request
  request a = primJS $ FetchEvent.prim__request a

  export
  resultingClientId : (obj : FetchEvent) -> JSIO String
  resultingClientId a = primJS $ FetchEvent.prim__resultingClientId a

  export
  respondWith : (obj : FetchEvent) -> (r : Promise Response) -> JSIO ()
  respondWith a b = primJS $ FetchEvent.prim__respondWith a b

namespace NavigationPreloadManager

  export
  disable : (obj : NavigationPreloadManager) -> JSIO (Promise Undefined)
  disable a = primJS $ NavigationPreloadManager.prim__disable a

  export
  enable : (obj : NavigationPreloadManager) -> JSIO (Promise Undefined)
  enable a = primJS $ NavigationPreloadManager.prim__enable a

  export
  getState :  (obj : NavigationPreloadManager)
           -> JSIO (Promise NavigationPreloadState)
  getState a = primJS $ NavigationPreloadManager.prim__getState a

  export
  setHeaderValue :  (obj : NavigationPreloadManager)
                 -> (value : ByteString)
                 -> JSIO (Promise Undefined)
  setHeaderValue a b = primJS
                     $ NavigationPreloadManager.prim__setHeaderValue a b

namespace ServiceWorker

  export
  onstatechange : ServiceWorker -> Attribute False Maybe EventHandlerNonNull
  onstatechange v = fromNullablePrim "ServiceWorker.getonstatechange"
                                     prim__onstatechange
                                     prim__setOnstatechange
                                     v

  export
  scriptURL : (obj : ServiceWorker) -> JSIO String
  scriptURL a = primJS $ ServiceWorker.prim__scriptURL a

  export
  state : (obj : ServiceWorker) -> JSIO ServiceWorkerState
  state a = tryJS "ServiceWorker.state" $ ServiceWorker.prim__state a

  export
  postMessage :  (obj : ServiceWorker)
              -> (message : Any)
              -> (transfer : Array Object)
              -> JSIO ()
  postMessage a b c = primJS $ ServiceWorker.prim__postMessage a (toFFI b) c

  export
  postMessage1 :  (0 _ : JSType t1)
               => {auto 0 _ : Elem PostMessageOptions (Types t1)}
               -> (obj : ServiceWorker)
               -> (message : Any)
               -> (options : Optional t1)
               -> JSIO ()
  postMessage1 a b c = primJS
                     $ ServiceWorker.prim__postMessage1 a (toFFI b) (optUp c)

  export
  postMessage1' : (obj : ServiceWorker) -> (message : Any) -> JSIO ()
  postMessage1' a b = primJS
                    $ ServiceWorker.prim__postMessage1 a (toFFI b) undef

namespace ServiceWorkerContainer

  export
  controller : (obj : ServiceWorkerContainer) -> JSIO (Maybe ServiceWorker)
  controller a = tryJS "ServiceWorkerContainer.controller"
               $ ServiceWorkerContainer.prim__controller a

  export
  oncontrollerchange :  ServiceWorkerContainer
                     -> Attribute False Maybe EventHandlerNonNull
  oncontrollerchange v = fromNullablePrim "ServiceWorkerContainer.getoncontrollerchange"
                                          prim__oncontrollerchange
                                          prim__setOncontrollerchange
                                          v

  export
  onmessage :  ServiceWorkerContainer
            -> Attribute False Maybe EventHandlerNonNull
  onmessage v = fromNullablePrim "ServiceWorkerContainer.getonmessage"
                                 prim__onmessage
                                 prim__setOnmessage
                                 v

  export
  onmessageerror :  ServiceWorkerContainer
                 -> Attribute False Maybe EventHandlerNonNull
  onmessageerror v = fromNullablePrim "ServiceWorkerContainer.getonmessageerror"
                                      prim__onmessageerror
                                      prim__setOnmessageerror
                                      v

  export
  ready :  (obj : ServiceWorkerContainer)
        -> JSIO (Promise ServiceWorkerRegistration)
  ready a = primJS $ ServiceWorkerContainer.prim__ready a

  export
  getRegistration :  (obj : ServiceWorkerContainer)
                  -> (clientURL : Optional String)
                  -> JSIO (Promise (Union2 ServiceWorkerRegistration Undefined))
  getRegistration a b = primJS
                      $ ServiceWorkerContainer.prim__getRegistration a (toFFI b)

  export
  getRegistration' :  (obj : ServiceWorkerContainer)
                   -> JSIO (Promise (Union2 ServiceWorkerRegistration
                                            Undefined))
  getRegistration' a = primJS
                     $ ServiceWorkerContainer.prim__getRegistration a undef

  export
  getRegistrations :  (obj : ServiceWorkerContainer)
                   -> JSIO (Promise (Array ServiceWorkerRegistration))
  getRegistrations a = primJS $ ServiceWorkerContainer.prim__getRegistrations a

  export
  register :  (0 _ : JSType t1)
           => {auto 0 _ : Elem RegistrationOptions (Types t1)}
           -> (obj : ServiceWorkerContainer)
           -> (scriptURL : String)
           -> (options : Optional t1)
           -> JSIO (Promise ServiceWorkerRegistration)
  register a b c = primJS $ ServiceWorkerContainer.prim__register a b (optUp c)

  export
  register' :  (obj : ServiceWorkerContainer)
            -> (scriptURL : String)
            -> JSIO (Promise ServiceWorkerRegistration)
  register' a b = primJS $ ServiceWorkerContainer.prim__register a b undef

  export
  startMessages : (obj : ServiceWorkerContainer) -> JSIO ()
  startMessages a = primJS $ ServiceWorkerContainer.prim__startMessages a

namespace ServiceWorkerGlobalScope

  export
  clients : (obj : ServiceWorkerGlobalScope) -> JSIO Clients
  clients a = primJS $ ServiceWorkerGlobalScope.prim__clients a

  export
  onactivate :  ServiceWorkerGlobalScope
             -> Attribute False Maybe EventHandlerNonNull
  onactivate v = fromNullablePrim "ServiceWorkerGlobalScope.getonactivate"
                                  prim__onactivate
                                  prim__setOnactivate
                                  v

  export
  onfetch :  ServiceWorkerGlobalScope
          -> Attribute False Maybe EventHandlerNonNull
  onfetch v = fromNullablePrim "ServiceWorkerGlobalScope.getonfetch"
                               prim__onfetch
                               prim__setOnfetch
                               v

  export
  oninstall :  ServiceWorkerGlobalScope
            -> Attribute False Maybe EventHandlerNonNull
  oninstall v = fromNullablePrim "ServiceWorkerGlobalScope.getoninstall"
                                 prim__oninstall
                                 prim__setOninstall
                                 v

  export
  onmessage :  ServiceWorkerGlobalScope
            -> Attribute False Maybe EventHandlerNonNull
  onmessage v = fromNullablePrim "ServiceWorkerGlobalScope.getonmessage"
                                 prim__onmessage
                                 prim__setOnmessage
                                 v

  export
  onmessageerror :  ServiceWorkerGlobalScope
                 -> Attribute False Maybe EventHandlerNonNull
  onmessageerror v = fromNullablePrim "ServiceWorkerGlobalScope.getonmessageerror"
                                      prim__onmessageerror
                                      prim__setOnmessageerror
                                      v

  export
  registration :  (obj : ServiceWorkerGlobalScope)
               -> JSIO ServiceWorkerRegistration
  registration a = primJS $ ServiceWorkerGlobalScope.prim__registration a

  export
  serviceWorker : (obj : ServiceWorkerGlobalScope) -> JSIO ServiceWorker
  serviceWorker a = primJS $ ServiceWorkerGlobalScope.prim__serviceWorker a

  export
  skipWaiting : (obj : ServiceWorkerGlobalScope) -> JSIO (Promise Undefined)
  skipWaiting a = primJS $ ServiceWorkerGlobalScope.prim__skipWaiting a

namespace ServiceWorkerRegistration

  export
  active : (obj : ServiceWorkerRegistration) -> JSIO (Maybe ServiceWorker)
  active a = tryJS "ServiceWorkerRegistration.active"
           $ ServiceWorkerRegistration.prim__active a

  export
  installing : (obj : ServiceWorkerRegistration) -> JSIO (Maybe ServiceWorker)
  installing a = tryJS "ServiceWorkerRegistration.installing"
               $ ServiceWorkerRegistration.prim__installing a

  export
  navigationPreload :  (obj : ServiceWorkerRegistration)
                    -> JSIO NavigationPreloadManager
  navigationPreload a = primJS
                      $ ServiceWorkerRegistration.prim__navigationPreload a

  export
  onupdatefound :  ServiceWorkerRegistration
                -> Attribute False Maybe EventHandlerNonNull
  onupdatefound v = fromNullablePrim "ServiceWorkerRegistration.getonupdatefound"
                                     prim__onupdatefound
                                     prim__setOnupdatefound
                                     v

  export
  scope : (obj : ServiceWorkerRegistration) -> JSIO String
  scope a = primJS $ ServiceWorkerRegistration.prim__scope a

  export
  updateViaCache :  (obj : ServiceWorkerRegistration)
                 -> JSIO ServiceWorkerUpdateViaCache
  updateViaCache a = tryJS "ServiceWorkerRegistration.updateViaCache"
                   $ ServiceWorkerRegistration.prim__updateViaCache a

  export
  waiting : (obj : ServiceWorkerRegistration) -> JSIO (Maybe ServiceWorker)
  waiting a = tryJS "ServiceWorkerRegistration.waiting"
            $ ServiceWorkerRegistration.prim__waiting a

  export
  unregister : (obj : ServiceWorkerRegistration) -> JSIO (Promise Boolean)
  unregister a = primJS $ ServiceWorkerRegistration.prim__unregister a

  export
  update : (obj : ServiceWorkerRegistration) -> JSIO (Promise Undefined)
  update a = primJS $ ServiceWorkerRegistration.prim__update a

namespace WindowClient

  export
  ancestorOrigins : (obj : WindowClient) -> JSIO (Array String)
  ancestorOrigins a = primJS $ WindowClient.prim__ancestorOrigins a

  export
  focused : (obj : WindowClient) -> JSIO Bool
  focused a = tryJS "WindowClient.focused" $ WindowClient.prim__focused a

  export
  visibilityState : (obj : WindowClient) -> JSIO VisibilityState
  visibilityState a = tryJS "WindowClient.visibilityState"
                    $ WindowClient.prim__visibilityState a

  export
  focus : (obj : WindowClient) -> JSIO (Promise WindowClient)
  focus a = primJS $ WindowClient.prim__focus a

  export
  navigate :  (obj : WindowClient)
           -> (url : String)
           -> JSIO (Promise (Nullable WindowClient))
  navigate a b = primJS $ WindowClient.prim__navigate a b

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

namespace CacheQueryOptions

  export
  new :  (ignoreSearch : Optional Bool)
      -> (ignoreMethod : Optional Bool)
      -> (ignoreVary : Optional Bool)
      -> JSIO CacheQueryOptions
  new a b c = primJS $ CacheQueryOptions.prim__new (toFFI a) (toFFI b) (toFFI c)

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

  export
  ignoreMethod :  (0 _ : JSType t)
               => {auto 0 _ : Elem CacheQueryOptions (Types t)}
               -> t
               -> Attribute True Optional Bool
  ignoreMethod v = fromUndefOrPrim "CacheQueryOptions.getignoreMethod"
                                   prim__ignoreMethod
                                   prim__setIgnoreMethod
                                   False
                                   (v :> CacheQueryOptions)

  export
  ignoreSearch :  (0 _ : JSType t)
               => {auto 0 _ : Elem CacheQueryOptions (Types t)}
               -> t
               -> Attribute True Optional Bool
  ignoreSearch v = fromUndefOrPrim "CacheQueryOptions.getignoreSearch"
                                   prim__ignoreSearch
                                   prim__setIgnoreSearch
                                   False
                                   (v :> CacheQueryOptions)

  export
  ignoreVary :  (0 _ : JSType t)
             => {auto 0 _ : Elem CacheQueryOptions (Types t)}
             -> t
             -> Attribute True Optional Bool
  ignoreVary v = fromUndefOrPrim "CacheQueryOptions.getignoreVary"
                                 prim__ignoreVary
                                 prim__setIgnoreVary
                                 False
                                 (v :> CacheQueryOptions)

namespace ClientQueryOptions

  export
  new :  (includeUncontrolled : Optional Bool)
      -> (type : Optional ClientType)
      -> JSIO ClientQueryOptions
  new a b = primJS $ ClientQueryOptions.prim__new (toFFI a) (toFFI b)

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

  export
  includeUncontrolled :  (0 _ : JSType t)
                      => {auto 0 _ : Elem ClientQueryOptions (Types t)}
                      -> t
                      -> Attribute True Optional Bool
  includeUncontrolled v = fromUndefOrPrim "ClientQueryOptions.getincludeUncontrolled"
                                          prim__includeUncontrolled
                                          prim__setIncludeUncontrolled
                                          False
                                          (v :> ClientQueryOptions)

  export
  type :  (0 _ : JSType t)
       => {auto 0 _ : Elem ClientQueryOptions (Types t)}
       -> t
       -> Attribute False Optional ClientType
  type v = fromUndefOrPrimNoDefault "ClientQueryOptions.gettype"
                                    prim__type
                                    prim__setType
                                    (v :> ClientQueryOptions)

namespace ExtendableEventInit

  export
  new : JSIO ExtendableEventInit
  new = primJS $ ExtendableEventInit.prim__new

namespace ExtendableMessageEventInit

  export
  new :  (data_ : Optional Any)
      -> (origin : Optional String)
      -> (lastEventId : Optional String)
      -> (source : Optional (Maybe (NS I [ Client
                                         , ServiceWorker
                                         , MessagePort
                                         ])))
      -> (ports : Optional (Array MessagePort))
      -> JSIO ExtendableMessageEventInit
  new a b c d e = primJS
                $ ExtendableMessageEventInit.prim__new (toFFI a)
                                                       (toFFI b)
                                                       (toFFI c)
                                                       (toFFI d)
                                                       (toFFI e)

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

  export
  data_ :  (0 _ : JSType t)
        => {auto 0 _ : Elem ExtendableMessageEventInit (Types t)}
        -> t
        -> Attribute True Optional Any
  data_ v = fromUndefOrPrim "ExtendableMessageEventInit.getdata"
                            prim__data
                            prim__setData
                            (MkAny $ null {a = ()})
                            (v :> ExtendableMessageEventInit)

  export
  lastEventId :  (0 _ : JSType t)
              => {auto 0 _ : Elem ExtendableMessageEventInit (Types t)}
              -> t
              -> Attribute True Optional String
  lastEventId v = fromUndefOrPrim "ExtendableMessageEventInit.getlastEventId"
                                  prim__lastEventId
                                  prim__setLastEventId
                                  ""
                                  (v :> ExtendableMessageEventInit)

  export
  origin :  (0 _ : JSType t)
         => {auto 0 _ : Elem ExtendableMessageEventInit (Types t)}
         -> t
         -> Attribute True Optional String
  origin v = fromUndefOrPrim "ExtendableMessageEventInit.getorigin"
                             prim__origin
                             prim__setOrigin
                             ""
                             (v :> ExtendableMessageEventInit)

  export
  ports :  (0 _ : JSType t)
        => {auto 0 _ : Elem ExtendableMessageEventInit (Types t)}
        -> t
        -> Attribute False Optional (Array MessagePort)
  ports v = fromUndefOrPrimNoDefault "ExtendableMessageEventInit.getports"
                                     prim__ports
                                     prim__setPorts
                                     (v :> ExtendableMessageEventInit)

  export
  source :  (0 _ : JSType t)
         => {auto 0 _ : Elem ExtendableMessageEventInit (Types t)}
         -> t
         -> Attribute True Optional (Maybe (NS I [ Client
                                                 , ServiceWorker
                                                 , MessagePort
                                                 ]))
  source v = fromUndefOrPrim "ExtendableMessageEventInit.getsource"
                             prim__source
                             prim__setSource
                             Nothing
                             (v :> ExtendableMessageEventInit)

namespace FetchEventInit

  export
  new :  (request : Request)
      -> (preloadResponse : Optional (Promise AnyPtr))
      -> (clientId : Optional String)
      -> (resultingClientId : Optional String)
      -> (replacesClientId : Optional String)
      -> (handled : Optional (Promise Undefined))
      -> JSIO FetchEventInit
  new a b c d e f = primJS
                  $ FetchEventInit.prim__new a
                                             (toFFI b)
                                             (toFFI c)
                                             (toFFI d)
                                             (toFFI e)
                                             (toFFI f)

  export
  new' : (request : Request) -> JSIO FetchEventInit
  new' a = primJS $ FetchEventInit.prim__new a undef undef undef undef undef

  export
  clientId :  (0 _ : JSType t)
           => {auto 0 _ : Elem FetchEventInit (Types t)}
           -> t
           -> Attribute True Optional String
  clientId v = fromUndefOrPrim "FetchEventInit.getclientId"
                               prim__clientId
                               prim__setClientId
                               ""
                               (v :> FetchEventInit)

  export
  handled :  (0 _ : JSType t)
          => {auto 0 _ : Elem FetchEventInit (Types t)}
          -> t
          -> Attribute False Optional (Promise Undefined)
  handled v = fromUndefOrPrimNoDefault "FetchEventInit.gethandled"
                                       prim__handled
                                       prim__setHandled
                                       (v :> FetchEventInit)

  export
  preloadResponse :  (0 _ : JSType t)
                  => {auto 0 _ : Elem FetchEventInit (Types t)}
                  -> t
                  -> Attribute False Optional (Promise AnyPtr)
  preloadResponse v = fromUndefOrPrimNoDefault "FetchEventInit.getpreloadResponse"
                                               prim__preloadResponse
                                               prim__setPreloadResponse
                                               (v :> FetchEventInit)

  export
  replacesClientId :  (0 _ : JSType t)
                   => {auto 0 _ : Elem FetchEventInit (Types t)}
                   -> t
                   -> Attribute True Optional String
  replacesClientId v = fromUndefOrPrim "FetchEventInit.getreplacesClientId"
                                       prim__replacesClientId
                                       prim__setReplacesClientId
                                       ""
                                       (v :> FetchEventInit)

  export
  request :  (0 _ : JSType t)
          => {auto 0 _ : Elem FetchEventInit (Types t)}
          -> t
          -> Attribute True I Request
  request v = fromPrim "FetchEventInit.getrequest"
                       prim__request
                       prim__setRequest
                       (v :> FetchEventInit)

  export
  resultingClientId :  (0 _ : JSType t)
                    => {auto 0 _ : Elem FetchEventInit (Types t)}
                    -> t
                    -> Attribute True Optional String
  resultingClientId v = fromUndefOrPrim "FetchEventInit.getresultingClientId"
                                        prim__resultingClientId
                                        prim__setResultingClientId
                                        ""
                                        (v :> FetchEventInit)

namespace MultiCacheQueryOptions

  export
  new : (cacheName : Optional String) -> JSIO MultiCacheQueryOptions
  new a = primJS $ MultiCacheQueryOptions.prim__new (toFFI a)

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

  export
  cacheName :  (0 _ : JSType t)
            => {auto 0 _ : Elem MultiCacheQueryOptions (Types t)}
            -> t
            -> Attribute False Optional String
  cacheName v = fromUndefOrPrimNoDefault "MultiCacheQueryOptions.getcacheName"
                                         prim__cacheName
                                         prim__setCacheName
                                         (v :> MultiCacheQueryOptions)

namespace NavigationPreloadState

  export
  new :  (enabled : Optional Bool)
      -> (headerValue : Optional ByteString)
      -> JSIO NavigationPreloadState
  new a b = primJS $ NavigationPreloadState.prim__new (toFFI a) (toFFI b)

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

  export
  enabled :  (0 _ : JSType t)
          => {auto 0 _ : Elem NavigationPreloadState (Types t)}
          -> t
          -> Attribute True Optional Bool
  enabled v = fromUndefOrPrim "NavigationPreloadState.getenabled"
                              prim__enabled
                              prim__setEnabled
                              False
                              (v :> NavigationPreloadState)

  export
  headerValue :  (0 _ : JSType t)
              => {auto 0 _ : Elem NavigationPreloadState (Types t)}
              -> t
              -> Attribute False Optional ByteString
  headerValue v = fromUndefOrPrimNoDefault "NavigationPreloadState.getheaderValue"
                                           prim__headerValue
                                           prim__setHeaderValue
                                           (v :> NavigationPreloadState)

namespace RegistrationOptions

  export
  new :  (scope : Optional String)
      -> (type : Optional WorkerType)
      -> (updateViaCache : Optional ServiceWorkerUpdateViaCache)
      -> JSIO RegistrationOptions
  new a b c = primJS
            $ RegistrationOptions.prim__new (toFFI a) (toFFI b) (toFFI c)

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

  export
  scope :  (0 _ : JSType t)
        => {auto 0 _ : Elem RegistrationOptions (Types t)}
        -> t
        -> Attribute False Optional String
  scope v = fromUndefOrPrimNoDefault "RegistrationOptions.getscope"
                                     prim__scope
                                     prim__setScope
                                     (v :> RegistrationOptions)

  export
  type :  (0 _ : JSType t)
       => {auto 0 _ : Elem RegistrationOptions (Types t)}
       -> t
       -> Attribute False Optional WorkerType
  type v = fromUndefOrPrimNoDefault "RegistrationOptions.gettype"
                                    prim__type
                                    prim__setType
                                    (v :> RegistrationOptions)

  export
  updateViaCache :  (0 _ : JSType t)
                 => {auto 0 _ : Elem RegistrationOptions (Types t)}
                 -> t
                 -> Attribute False Optional ServiceWorkerUpdateViaCache
  updateViaCache v = fromUndefOrPrimNoDefault "RegistrationOptions.getupdateViaCache"
                                              prim__updateViaCache
                                              prim__setUpdateViaCache
                                              (v :> RegistrationOptions)


text:
module NonDet

-- Non-determinism, based on http://okmij.org/ftp/tagless-final/nondet-paper.pdf

import Control.Monad.Identity

interface NDet (rep : Type -> Type) (val : Type -> Type) | rep where
  nil : rep a
  cons : val a -> rep a -> rep a
  list : List a -> rep a
  decon : rep a -> (() -> rep a) -> (val a -> rep a -> rep a) -> rep a
  foldr : (val a -> rep a -> rep a) -> rep a -> rep a -> rep a
  fail : rep a
  (||) : rep a -> rep a -> rep a

data Lists : Type -> Type where
  In : List (List a) -> Lists a

NDet Lists Identity where
  nil = In [[]]
  cons (Id y) (In xss) = In $ map (\xs => y :: xs) xss
  list xs = In [xs]
  decon (In xss) onnil oncons = In $ xss >>= (\xs => case xs of
                                                      [] => let (In yss) = onnil () in yss
                                                      h :: t => let (In yss) = oncons (Id h) (In [t]) in yss)

  foldr f seed (In xss) = In $ xss >>= (\xs => let (In yss) = foldr (\x, acc => f (Id x) acc) seed xs in yss)

  fail = In []
  (||) (In xs) (In ys) = In (xs ++ ys)

insert : NDet rep val => val a -> rep a -> rep a
insert x l = cons x l || decon l (\() => fail) (\h, t => cons h (insert x t))

perm : NDet rep val => List a -> rep a
perm xs = foldr (\x, xs => insert x xs) nil (list xs)

test : Lists Int
test = perm [1, 2, 3]

ext: idr

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


text:
-- ------------------------------------------------------------ [ RedBlack.idr ]
-- Module    : RedBlack.idr
-- Copyright : (c) 2015,2016 See CONTRIBUTORS.md
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
||| Testing Stacks using silly stupid tests
module Data.Test.RedBlack

import Test.Unit
import Test.Random.Values

import Data.RedBlack.Tree

%access export

list1 : List Integer
list1 = rndListIntU 123456789 (0,100) 30

list2 : List Integer
list2 = rndListIntU 987654321 (0,100) 30

-- ------------------------------------------------------------ [ Construction ]
partial
testBuilding : IO Bool
testBuilding = genericTest
    (Just "List, Building" )
    (Tree.size $ Tree.fromList (list1 ++ list1))
    30
    (==)

-- ---------------------------------------------------------------- [ Updating ]
partial
testUpdate : IO Bool
testUpdate = genericTest
    (Just "Insert")
    (Tree.size $ insert 1 $ Tree.fromList list2)
    31
    (==)

partial
testContains : IO Bool
testContains = genericTest
    (Just "Contains")
    (Tree.contains 4 $ Tree.fromList [1,2,3,4])
    (True)
    (==)

partial
runTest : IO ()
runTest = do
    putStrLn "Testing RedBlack Tree"
    putStrLn infoLine
    NonReporting.runTests [
        testBuilding
      , testUpdate
      , testContains
    ]

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

max_stars_repo_name: MarcelineVQ/idris-containers

max_issues_repo_name: MarcelineVQ/idris-containers

max_forks_repo_name: MarcelineVQ/idris-containers


text:
module Generics.Newtype.Num

import Generics.Derive
%language ElabReflection

--------------------------------------------------------------------------------
--          Num
--------------------------------------------------------------------------------

-- Derivation of Num for n-ary products or newtypes
-- e.g. `(a,b,c)` or `data Foo a = MkFoo a`  or  `data Foo = Foo Int`

-- n-ary products, e.g. (a,b,c)   (data Foo x y = MkFoo x y)
public export
(all : NP (Num . f) ks) => Num (NP f ks) where
  (+) = hcliftA2 (Num . f) (+)
  (*) = hcliftA2 (Num . f) (*)
  fromInteger {all = []} _ = []
  fromInteger {all = _::_} i = fromInteger i :: fromInteger i

-- This type of deriving is for newtypes so we restrict oursellves to single constructor types.
public export
(all : NP (Num . f) [k']) => Num (NS f [k']) where
  -- encode = hconcat . hcmap (Encode . f) encode
  (+) {all = _::_} (Z x) (Z y) = Z $ x + y
  (*) {all = _::_} (Z x) (Z y) = Z $ x * y
  fromInteger {all = _::_} i = Z (fromInteger i)

public export
POP (Num . f) kss => Num (POP f kss) where
  (+) (MkPOP nps1) (MkPOP nps2) = MkPOP $ nps1 + nps2
  (*) (MkPOP nps1) (MkPOP nps2) = MkPOP $ nps1 * nps2
  fromInteger i = MkPOP (fromInteger i)

public export
POP (Num . f) [ks] => Num (SOP f [ks]) where
  (+) (MkSOP nps1) (MkSOP nps2) = MkSOP $ nps1 + nps2
  (*) (MkSOP nps1) (MkSOP nps2) = MkSOP $ nps1 * nps2
  fromInteger i = MkSOP (fromInteger i)

export
genericPlus : Generic t [code] => POP Num [code] => t -> t -> t
genericPlus x y = to $ (+) (from x) (from y)

export
genericMult : Generic t [code] => POP Num [code] => t -> t -> t
genericMult x y = to $ (*) (from x) (from y)

export
genericFromInteger : Generic t [code] => POP Num [code] => Integer -> t
genericFromInteger = to . fromInteger

export
||| Derives a `Num` implementation for the given data type
||| and visibility.
NumVis : Visibility -> DeriveUtil -> InterfaceImpl
NumVis vis g = MkInterfaceImpl "Num" vis []
                       `(MkNum genericPlus genericMult genericFromInteger)
                       (implementationType `(Num) g)

export
||| Alias for `EncodeVis Public`.
Num : DeriveUtil -> InterfaceImpl
Num = NumVis Public


text:
module Text.CSS.Length

import Text.CSS.Render

%default total

public export
data Length : Type where
  Pt       : Bits16 -> Length
  Px       : Bits16 -> Length
  Em       : Double -> Length
  Rem      : Double -> Length

export
Render Length where
  render (Pt x)   = show x ++ "pt"
  render (Px x)   = show x ++ "px"
  render (Em x)   = show x ++ "em"
  render (Rem x)  = show x ++ "rem"

export %inline
pt : Cast Length a => Bits16 -> a
pt = cast . Pt

export %inline
px : Cast Length a => Bits16 -> a
px = cast . Px

export %inline
em : Cast Length a => Double -> a
em = cast . Em

export %inline
rem : Cast Length a => Double -> a
rem = cast . Rem


text:
module Sixel

import public Data.Buffer

import Sixel.Library
import public Sixel.Symbols
import public Sixel.Allocator
import public Sixel.Output
import public Sixel.Dither
import public Sixel.Encoder
import public Sixel.Decoder
import public Sixel.Helpers

%foreign (sixel "sixel_encode")
sixel_encode :
  (pixels : Buffer) -> (w : Int) -> (h : Int) -> (depth : Int) -> PrimDither -> PrimOutput ->
  PrimIO Int

export
encode :
  (pixels : Buffer) -> (w : Int) -> (h : Int) -> (depth : Int) -> Dither n -> Output m ->
  IO (Either Status ())
encode pixels w h depth dither output = do
  status <- MkStatus <$> fromPrim (sixel_encode pixels w h depth (toPrim dither) (toPrim output))
  pure $ if succeeded status then Right () else Left status

max_stars_repo_name: Kaiepi/id-sixel

max_issues_repo_name: Kaiepi/id-sixel

max_forks_repo_name: Kaiepi/id-sixel


text:
module Parser.Lexer.Package

import public Parser.Lexer.Common
import public Libraries.Text.Lexer
import public Libraries.Text.Parser
import public Libraries.Text.Bounded
import Libraries.Text.PrettyPrint.Prettyprinter

import Data.List
import Data.List1
import Data.String
import Libraries.Data.String.Extra
import Libraries.Utils.String

import Core.Name.Namespace

%default total

public export
data Token
  = Comment String
  | EndOfInput
  | Equals
  | DotSepIdent (Maybe Namespace) String
  | Separator
  | Dot
  | LTE
  | GTE
  | LT
  | GT
  | EqOp
  | AndOp
  | Space
  | StringLit String
  | IntegerLit Integer

public export
Show Token where
  show (Comment str) = "Comment: " ++ str
  show EndOfInput = "EndOfInput"
  show Equals = "Equals"
  show (DotSepIdent ns n) = "DotSepIdentifier: " ++ show ns ++ "." ++ show n
  show Separator = "Separator"
  show Dot = "Dot"
  show LTE = "LTE"
  show GTE = "GTE"
  show LT = "LT"
  show GT = "GT"
  show EqOp = "EqOp"
  show AndOp = "AndOp"
  show Space = "Space"
  show (StringLit s) = "StringLit: " ++ s
  show (IntegerLit i) = "IntegerLit: " ++ show i

public export
Pretty Token where
  pretty (Comment str) = "Comment:" <++> pretty str
  pretty EndOfInput = "EndOfInput"
  pretty Equals = "Equals"
  pretty (DotSepIdent ns n) = "DotSepIdentifier:" <++> pretty ns <+> dot <+> pretty n
  pretty Separator = "Separator"
  pretty Dot = "Dot"
  pretty LTE = "LTE"
  pretty GTE = "GTE"
  pretty LT = "LT"
  pretty GT = "GT"
  pretty EqOp = "EqOp"
  pretty AndOp = "AndOp"
  pretty Space = "Space"
  pretty (StringLit s) = "StringLit:" <++> pretty s
  pretty (IntegerLit i) = "IntegerLit:" <++> pretty i

equals : Lexer
equals = is '='

separator : Lexer
separator = is ','

dot : Lexer
dot = is '.'

lte : Lexer
lte = is '<' <+> is '='

gte : Lexer
gte = is '>' <+> is '='

lt : Lexer
lt = is '<'

gt : Lexer
gt = is '>'

eqop : Lexer
eqop = is '=' <+> is '='

andop : Lexer
andop = is '&' <+> is '&'

rawTokens : TokenMap Token
rawTokens =
  [ (comment, Comment . drop 2)
  , (namespacedIdent, uncurry DotSepIdent . mkNamespacedIdent)
  , (identAllowDashes, DotSepIdent Nothing)
  , (separator, const Separator)
  , (dot, const Dot)
  , (lte, const LTE)
  , (gte, const GTE)
  , (lt, const LT)
  , (gt, const GT)
  , (eqop, const EqOp)
  , (andop, const AndOp)
  , (equals, const Equals)
  , (spacesOrNewlines, const Space)
  , (stringLit, \s => StringLit (stripQuotes s))
  , (intLit, \i => IntegerLit (cast i))
  ]

export
lex : String -> Either (Int, Int, String) (List (WithBounds Token))
lex str =
  case lexTo (const False) rawTokens str of
       (tokenData, (l, c, "")) =>
         Right $ (filter (useful . val) tokenData)
          ++ [MkBounded EndOfInput False (MkBounds l c l c)]
       (_, fail) => Left fail
  where
    useful : Token -> Bool
    useful (Comment c) = False
    useful Space       = False
    useful _ = True


text:
-- SPDX-FileCopyrightText: 2021 The ipkg-idr developers
--
-- SPDX-License-Identifier: MPL-2.0

module Language.IPKG.Value

import Data.List
import Data.List1
import Data.Strings

public export
Identifier : Type
Identifier = String

public export
ModuleIdent : Type
ModuleIdent = List1 Identifier

public export
record PkgDesc where
    constructor MkPkgDesc
    name        : Identifier
    version     : String -- TODO should be a proper type
    authors     : String
    maintainers : Maybe String
    license     : Maybe String
    brief       : Maybe String
    readme      : Maybe String
    homepage    : Maybe String
    sourceloc   : Maybe String
    bugtracker  : Maybe String
    depends     : List Identifier -- packages to add to search path
    modules     : List ModuleIdent -- modules to install (namespace, filename)
    mainmod     : Maybe ModuleIdent -- main file (i.e. file to load at REPL)
    executable  : Maybe String -- name of executable
    options     : Maybe String
    sourcedir   : Maybe String
    builddir    : Maybe String
    outputdir   : Maybe String

    prebuild    : Maybe String -- Script to run before building
    postbuild   : Maybe String -- Script to run after building
    preinstall  : Maybe String -- Script to run after building, before installing
    postinstall : Maybe String -- Script to run after installing
    preclean    : Maybe String -- Script to run before cleaning
    postclean   : Maybe String -- Script to run after cleaning

private
showModule : ModuleIdent -> String
showModule m = fastConcat . intersperse "." $ forget m

export
Show PkgDesc where
    show pkg = "Package: " ++ name pkg ++ "\n" ++
                "Version: " ++ version pkg ++ "\n" ++
                "Authors: " ++ authors pkg ++ "\n" ++
                maybe "" (\m => "Maintainers: " ++ m ++ "\n") (maintainers pkg) ++
                maybe "" (\m => "License: "     ++ m ++ "\n") (license pkg)     ++
                maybe "" (\m => "Brief: "       ++ m ++ "\n") (brief pkg)       ++
                maybe "" (\m => "ReadMe: "      ++ m ++ "\n") (readme pkg)      ++
                maybe "" (\m => "HomePage: "    ++ m ++ "\n") (homepage pkg)    ++
                maybe "" (\m => "SourceLoc: "   ++ m ++ "\n") (sourceloc pkg)   ++
                maybe "" (\m => "BugTracker: "  ++ m ++ "\n") (bugtracker pkg)  ++
                "Depends: " ++ show (depends pkg) ++ "\n" ++
                "Modules: " ++ show (map showModule $ modules pkg) ++ "\n" ++
                maybe "" (\m => "Main: " ++ showModule m ++ "\n") (mainmod pkg) ++
                maybe "" (\m => "Exec: " ++ m ++ "\n") (executable pkg) ++
                maybe "" (\m => "Opts: " ++ m ++ "\n") (options pkg) ++
                maybe "" (\m => "SourceDir: " ++ m ++ "\n") (sourcedir pkg) ++
                maybe "" (\m => "BuildDir: " ++ m ++ "\n") (builddir pkg) ++
                maybe "" (\m => "OutputDir: " ++ m ++ "\n") (outputdir pkg) ++
                maybe "" (\m => "Prebuild: " ++ m ++ "\n") (prebuild pkg) ++
                maybe "" (\m => "Postbuild: " ++ m ++ "\n") (postbuild pkg) ++
                maybe "" (\m => "Preinstall: " ++ m ++ "\n") (preinstall pkg) ++
                maybe "" (\m => "Postinstall: " ++ m ++ "\n") (postinstall pkg) ++
                maybe "" (\m => "Preclean: " ++ m ++ "\n") (preclean pkg) ++
                maybe "" (\m => "Postclean: " ++ m ++ "\n") (postclean pkg)

max_stars_repo_name: tiatomee/ipkg-idr

max_issues_repo_name: tiatomee/ipkg-idr

max_forks_repo_name: tiatomee/ipkg-idr


text:
import Data.Vect

createEmpties : Vect n (Vect 0 elem)
createEmpties = replicate _ []

transposeHelper : (x : Vect n elem) -> (xsTrans : Vect n (Vect len elem)) -> Vect n (Vect (S len) elem)
transposeHelper [] [] = []
transposeHelper (x :: xs) (y :: ys) = (x :: y) :: transposeHelper xs ys

transposeMat : Vect m (Vect n elem) -> Vect n (Vect m elem)
transposeMat [] = createEmpties
transposeMat (x :: xs) = let xsTrans = transposeMat xs in
                             zipWith (::) x xsTrans
addMatrix : Num a => Vect m (Vect n a) -> Vect m (Vect n a) -> Vect m (Vect n a)
addMatrix [] [] = []
addMatrix xs ys = zipWith (zipWith (+)) xs ys

-- dotProdHelper : Num a => (xs : Vect n (Vect m a)) -> (ys : Vect p (Vect m a)) -> Vect n (Vect p a)
-- dotProdHelper [] [] = []
-- dotProdHelper [] (x :: xs) = ?dotProdHelper_rhs_4
-- -- dotProdHelper (x :: xs) ys = (foldl (\acc, row => acc ++ (sum $ Data.Vect.zipWith (*) x row)) [[]] ys) -- ++ dotProdHelper xs ys

-- dotProd : Num a => Vect n (Vect m a) -> Vect m (Vect p a) -> Vect n (Vect p a)
-- dotProd [] [] = []
-- dotProd [] (x :: xs) = []
-- dotProd xs ys = dotProdHelper xs (transposeMat ys)


text:
||| A version of `Dec` that returns a meaningful error message as well as proof of void.
|||
||| When dealing with decidable properties for type-level computations
||| the existing `Dec` data type is useful.  However, when using
||| decidable properties interactively one cannot easily tell why a
||| property failed.  One can always encode failing cases within the
||| property itself but that is not necessarily a advantageous.
|||
||| `DecInfo` provides a data structure to capture decidable properties together with an informative error message for when the property does not hold.
module Toolkit.Decidable.Informative

import Decidable.Equality
%default total

public export
data DecInfo : (errType : Type) -> (prop : Type) -> Type where
   Yes : (prfWhy : prop) -> DecInfo errType prop
   No  : (msgWhyNot : errType) -> (prfWhyNot : prop -> Void) -> DecInfo errType prop

export
embed : (f   : a -> e)
     -> (res : DecInfo a p)
            -> DecInfo e p
embed _ (Yes prfWhy) = Yes prfWhy
embed f (No msgWhyNot prfWhyNot) = No (f msgWhyNot) prfWhyNot

export
otherwise : DecInfo e b -> (a -> b) -> Either (e, Not a) b
otherwise (Yes prfWhy) f = Right prfWhy
otherwise (No msgWhyNot prfWhyNot) f = Left (msgWhyNot, \x => prfWhyNot (f x))

export
try : DecInfo e b -> (a -> b) -> Either (e, Not a) b
try = otherwise

export
decInfoDo : Either (e, Not a) a -> DecInfo e a
decInfoDo (Left (x, y)) = No x y
decInfoDo (Right x) = Yes x

namespace Lift

  export
  otherwise : DecInfo eB b -> (eB -> eA) -> (a -> b) -> Either (eA, Not a) b
  otherwise (Yes prfWhy) _ _ = Right prfWhy
  otherwise (No msgWhyNot prfWhyNot) g f = Left (g msgWhyNot, \x => prfWhyNot (f x))

  export
  try : DecInfo eB b -> (eB -> eA) -> (a -> b) -> Either (eA, Not a) b
  try = otherwise

namespace Either

   public export
   asEither : DecInfo e p -> Either e p
   asEither (Yes prfWhy) = Right prfWhy
   asEither (No msgWhyNot prfWhyNot) = Left msgWhyNot

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

max_stars_repo_name: gallais/linear-circuits

max_issues_repo_name: gallais/linear-circuits

max_forks_repo_name: gallais/linear-circuits


text:
module Main -- where

main : IO ()
main = do
  let f (x :: xs) = ((x + 1) :: f xs)
  printLn $ f [1,2,3,4,5]

max_stars_repo_name: andorp/IdrisExtSTGCodegen

max_issues_repo_name: andorp/IdrisExtSTGCodegen

max_forks_repo_name: andorp/IdrisExtSTGCodegen


text:
module Crypto.Sodium

import Crypto.RawSodium

-- Key generation

export
data Key = MkKey ManagedPtr

newKey : (len : Int) -> IO Key
newKey l = pure $ MkKey !(do_newKey l)

export
newSymmKey : IO Key
newSymmKey = do len <- secretbox_keyLength
                newKey len

export
newSecretKey : IO Key
newSecretKey = do len <- box_secretKeyLength
                  newKey len

export
newPublicKey : IO Key
newPublicKey = do len <- box_publicKeyLength
                  newKey len

export
newKeyPair : IO (Key, Key)
newKeyPair = do kp <- do_newKeyPair
                pk <- do_getPublic kp
                sk <- do_getSecret kp
                do_freeKeyPair kp
                pure (MkKey pk, MkKey sk)

export
keyLen : Key -> Int
keyLen (MkKey k) = unsafePerformIO (do_getKeyLen k)

export
keyIdx : Key -> Int -> Int
keyIdx (MkKey k) i = unsafePerformIO (do_getKeyIdx k i)

export
setKeyIdx : Key -> Int -> Int -> IO ()
setKeyIdx (MkKey k) i b = do_setKeyIdx k i b

-- Nonces

export
data Nonce = MkNonce ManagedPtr

export
newNonce : (len : Int) -> IO Nonce
newNonce l = pure $ MkNonce !(do_newNonce l)

export
newNonceFromString : (str : String) -> IO Nonce
newNonceFromString str = pure $ MkNonce !(do_newNonceFromString str)

export
setNonceIdx : Nonce -> Int -> Int -> IO ()
setNonceIdx (MkNonce k) i b = do_setNonceIdx k i b

-- An Encrypted box holds raw encrypted data, and its length
export
data EncryptedBox = MkEnc ManagedPtr | EncFailed

export
newSymmBox : Int -> IO EncryptedBox
newSymmBox l = pure $ MkEnc !(do_newSecretBox l)

export
newBox : Int -> IO EncryptedBox
newBox l = pure $ MkEnc !(do_newBox l)

export
getBoxLen : EncryptedBox -> Int
getBoxLen (MkEnc e) = unsafePerformIO $ do_getBoxLen e

export
getBoxIdx : EncryptedBox -> Int -> Int
getBoxIdx (MkEnc e) i = unsafePerformIO $ do_getBoxIdx e i

export
getBytes : EncryptedBox -> List Int
getBytes e = getAll [] 0 (getBoxLen e)
   where getAll : List Int -> Int -> Int -> List Int
         getAll acc i len
             = if i == len
                  then reverse acc
                  else getAll (getBoxIdx e i :: acc) (i + 1) len

export
validBox : EncryptedBox -> Bool
validBox (MkEnc e) = True
validBox EncFailed = False

-- freeBox : EncryptedBox -> IO ()
-- freeBox (MkEnc e) = do_freeBox e

-- An open box holds plain text, and its length

export
data OpenBox = MkDec ManagedPtr | DecFailed

export
readBox : OpenBox -> String
readBox (MkDec p) = unsafePerformIO (do_readBoxOpen p)

export
validOpenBox : OpenBox -> Bool
validOpenBox (MkDec e) = True
validOpenBox DecFailed = False

-- freeOpenBox : OpenBox -> IO ()
-- freeOpenBox (MkDec e) = do_freeBoxOpen e

-- Nonce lengths

export
symmNonceLength : Int
symmNonceLength = unsafePerformIO secretbox_nonceLength

export
nonceLength : Int
nonceLength = unsafePerformIO box_nonceLength

-- Symmetric key encryption

export
cryptoSecretBox : (plaintext : String) -> (nonce : Nonce) ->
                  (key : Key) -> IO EncryptedBox
cryptoSecretBox m (MkNonce n) (MkKey k)
    = case !(do_cryptoSecretBox m n k) of
           Just p => pure (MkEnc p)
           Nothing => pure EncFailed

export
cryptoSecretBoxOpen : (ciphertext : EncryptedBox) -> (nonce : Nonce) ->
                      (key : Key) -> IO OpenBox
cryptoSecretBoxOpen (MkEnc e) (MkNonce n) (MkKey k)
    = case !(do_cryptoSecretBoxOpen e n k) of
           Just p => pure (MkDec p)
           Nothing => pure DecFailed

-- Public key encryption

export
cryptoBox : (plaintext : String) -> (nonce : Nonce) ->
            (pkey : Key) -> (skey : Key) -> IO EncryptedBox
cryptoBox m (MkNonce n) (MkKey pk) (MkKey sk)
    = case !(do_cryptoBox m n pk sk) of
           Just p => pure (MkEnc p)
           Nothing => pure EncFailed

export
cryptoBoxOpen : (ciphertext : EncryptedBox) -> (nonce : Nonce) ->
                (pkey : Key) -> (skey : Key) -> IO OpenBox
cryptoBoxOpen (MkEnc e) (MkNonce n) (MkKey pk) (MkKey sk)
    = case !(do_cryptoBoxOpen e n pk sk) of
           Just p => pure (MkDec p)
           Nothing => pure DecFailed


text:
module Ziria

-- Based on https://github.com/dimitriv/ziria-sem/blob/master/Haskell/ZirStepper.hs

data ZirS : (s : Type) -> (i : Type) -> (o : Type) -> (v : Type) -> Type where
  Yield : s -> o -> ZirS s i o v
  Skip : s -> ZirS s i o v
  Done : v -> ZirS s i o v
  NeedInput : (i -> s) -> ZirS s i o v

data Zir : (i : Type) -> (o : Type) -> (v : Type) -> Type where
  ZirC : s -> (s -> ZirS s i o v) -> Zir i o v

return : v -> Zir i o v
return v = ZirC () (\() => Done v)

cast : (s -> s') -> ZirS s i o v -> ZirS s' i o v
cast f (Yield s o) = Yield (f s) o
cast f (Skip s) = Skip (f s)
cast f (Done x) = Done x
cast f (NeedInput g) = NeedInput (f . g)

(>>=) : Zir i o v -> (v -> Zir i o w) -> Zir i o w
(>>=) (ZirC x step1) f = ZirC (Left x) (step step1)
  where
    s2step : Zir i o w -> ZirS (Either s (Zir i o w)) i o w
    s2step (ZirC s2 step2) = cast (\x => Right (ZirC x step2)) (step2 s2)
    step : (s -> ZirS s i o v) -> Either s (Zir i o w) -> ZirS (Either s (Zir i o w)) i o w
    step step1 (Right zir) = s2step zir
    step step1 (Left l) with (step1 l)
      step step1 (Left l) | (Yield s1' z) = Yield (Left s1') z
      step step1 (Left l) | (Skip s1') = Skip (Left s1')
      step step1 (Left l) | (Done y) = s2step (f y)
      step step1 (Left l) | (NeedInput g) = NeedInput (\i => Left (g i))

step' : (s1 -> ZirS s1 i m v) -> (s2 -> ZirS s2 m o v) -> (s1, s2) -> ZirS (s1, s2) i o v
step' step1 step2 (s1, s2) with (step2 s2)
  step' step1 step2 (s1, s2) | (Yield s2' ot) = Yield (s1, s2') ot
  step' step1 step2 (s1, s2) | (Skip s2') = Skip (s1, s2')
  step' step1 step2 (s1, s2) | (Done x) = Done x
  step' step1 step2 (s1, s2) | (NeedInput f) with (step1 s1)
    step' step1 step2 (s1, s2) | (NeedInput f) | (Yield s1' ot) = Skip (s1', f ot)
    step' step1 step2 (s1, s2) | (NeedInput f) | (Skip s1') = Skip (s1', s2)
    step' step1 step2 (s1, s2) | (NeedInput f) | (Done x) = Done x
    step' step1 step2 (s1, s2) | (NeedInput f) | (NeedInput g) = NeedInput (\i => ((g i), s2))

infixl 9 >>>
(>>>) : Zir i m v -> Zir m o v -> Zir i o v
(>>>) (ZirC s1 step1) (ZirC s2 step2) = ZirC (s1, s2) (step' step1 step2)

emit : o -> Zir i o ()
emit x = ZirC True aux
  where
    aux : Bool -> ZirS Bool i o ()
    aux False = Done ()
    aux True = Yield False x

take : Zir i o i
take = ZirC Nothing aux
  where
    aux : Maybe i -> ZirS (Maybe i) i o i
    aux Nothing = NeedInput Just
    aux (Just x) = Done x

run : Zir i o v -> Stream i -> (v, List o)
run (ZirC st step) input = loop step [] input (step st)
  where
    loop : (s -> ZirS s i o v) -> List o -> Stream i -> ZirS s i o v -> (v, List o)
    loop step acc input (Yield st ot) = loop step (ot :: acc) input (step st)
    loop step acc input (Skip st) = loop step acc input (step st)
    loop step acc input (Done v) = (v, reverse acc)
    loop step acc (x :: xs) (NeedInput f) = loop step acc xs (step (f x))

example : Zir Int Int Int
example = do x <- take
             emit (x + 1)
             y <- take
             emit (y + 2)
             return (x + y)

test : (Int, List Int)
test = run example [1..]


text:
module Utils.Lens

-- Note: Their are lenses out their for Idris
--          https://github.com/HuwCampbell/idris-lens/blob/master/Control/Lens/Types.idr
--          https://github.com/idris-hackers/idris-lens/blob/master/Lens.idr
-- However, they are over complicated for performance and composability reasons.
--  Conclusion: Use a custom bare minimum (easy understandable) now and if needed replace with a more sophisticated implementation later (if needed)

public export
record Lens w p where
    constructor MkLens
    get : w -> p
    update : w -> (p -> p) -> w     -- Defining over update (instead of set) seems more efficient (without getting to complex)

-- Implicit versions of the accessors
export
(.set) : Lens w p -> w -> p -> w
(.set)  lens wv pv = lens.update wv (\_ => pv)

export
set : Lens w p -> w -> p -> w
set lens wv pv = lens.set wv pv

-- Views: Not yet needed remove if it stays that way
public export
record View w p where
    constructor MkView
    lens : Lens w p
    value : w

getV : View w p -> p
getV (MkView lens wv) = lens.get wv

setV : View w p -> p -> View w p
setV (MkView lens wv) pv = MkView lens (lens.set wv pv)

updateV : View w p -> (p -> p) -> View w p
updateV (MkView lens wv) fn = MkView lens (lens.update wv fn)

Semigroup p => Semigroup (View w p) where
    (<+>) vl vr = updateV vl (<+> (getV vr))

-- Compositors
export
join : Lens w m -> Lens m p -> Lens w p
join lo li = MkLens (\wv => li.get $ lo.get wv) (\wv,fn => lo.update wv (\mv => li.update mv fn))

-- identity
export
idLens : Lens a a
idLens = MkLens id (\av,fn => fn av)

-- Tuple
export
leftLens : Lens (a,b) a
leftLens = MkLens (\(av,bv) => av) (\(av,bv),fn => (fn av,bv))

export
rightLens : Lens (a,b) b
rightLens = MkLens (\(av,bv) => bv) (\(av,bv),fn => (av,fn bv))

-- List
-- Not the nicest but I do not implement Prisms just for this - especially if the normal use is to fail anyway
export
headFailLens : Lens (List a) a
headFailLens = MkLens read update
    where read : List a -> a
          read (head::xs) = head
          read _ = assert_total $ idris_crash "List was empty"
          update : List a -> (a -> a) -> List a
          update (head::xs) headUpdate = (headUpdate head)::xs
          update _ _ = assert_total $ idris_crash "List was empty"

export
tailFailLens : Lens (List a) (List a)
tailFailLens = MkLens read update
    where read : List a -> List a
          read (head::xs) = xs
          read _ = assert_total $ idris_crash "List was empty"
          update : List a -> (List a ->  List a) -> List a
          update (head::xs) tailUpdate = head::(tailUpdate xs)
          update _ _ = assert_total $ idris_crash "List was empty"

max_stars_repo_name: skyro-compiler/skyro

max_issues_repo_name: skyro-compiler/skyro

max_forks_repo_name: skyro-compiler/skyro


text:
-- -------------------------------------------------------------- [ Parser.idr ]
-- Module      : UML.Deployment.Parser
-- Description : Parser for textual UML deployment diagrams.
-- Copyright   : (c) Jan de Muijnck-Hughes
-- License     : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module UML.Deployment.Parser

import Lightyear
import Lightyear.Strings

import UML.Types

import UML.Deployment.Model
import UML.Utils.Parsing

%access private
-- -------------------------------------------------------------------- [ Misc ]
||| Parse a key-value pair.
|||
||| Key value pairs are of the form: `<key> : "<value>"`.
|||
kvpair : Parser Attribute
kvpair = do
    key <- ident <* space
    colon
    value <- literallyBetween '\"'
    pure (key, value)
  <?> "KV Pair"

||| Parse pair of braces containing many comma separated KV pairs.
kvBody : Parser Attributes
kvBody = braces $ (commaSep1 (kvpair <* space) <* space)
  <?> "KV Body"

||| Parse several properties.
properties : Parser Attributes
properties = do
    token "properties"
    ps <- kvBody
    pure ps
  <?> "Properties"

-- --------------------------------------------------------------- [ Relations ]
||| Parse a relation defined between two entities.
relation : Parser $ DeploymentModel RELA
relation = do
    xID <- ident <* space
    token "commsWith"
    yID <- ident <* space
    token "via"
    proto <- ident <* space
    pure $ Relation xID yID proto
  <?> "Relation"

-- ----------------------------------------------------------- [ Specification ]

spec : Parser $ DeploymentModel SPEC
spec = do
    token "spec"
    id <- ident <* space
    as <- opt kvBody
    pure $ Spec id $ fromMaybe Nil as

-- ---------------------------------------------------------------- [ Artifact ]

artifactTy : Parser ArtifactTy
artifactTy = do token "doc"
                pure Document
         <|> do token "src"
                pure Source
         <|> do token "lib"
                pure Library
         <|> do token "exe"
                pure Executable
         <|> do token "script"
                pure Script
         <?> "Artifact Type"

artifact : Parser $ DeploymentModel ARTIFACT
artifact = do
    token "artifact"
    ty <- artifactTy
    id <- ident <* space
    s <- opt artBody
    pure $ Artifact ty id s
   <?> "Artifact"
  where
    artBody : Parser (DeploymentModel SPEC)
    artBody = do
      token "with" <* space
      s <- spec
      pure s

-- ----------------------------------------------------------------- [ Exe Env ]

envTy : Parser EnvTy
envTy = do token "os"
           pure OS
    <|> do token "engine"
           pure Engine
    <|> do token "container"
           pure Container
    <|> do token "appserver"
           pure AppServer
    <|> do token "app"
           pure App
    <?> "ExeEnv Type"

exenv : Parser $ DeploymentModel ENV
exenv = do
    token "env"
    ty <- envTy <* space
    id <- ident <* space
    (as, ps) <- braces (exenvBody <* space)
    pure $ Env ty id as ps
   <?> "Execution Environment"
  where
    exenvBody : Parser (List $ DeploymentModel ARTIFACT, Maybe Attributes)
    exenvBody = do
      as <- some (artifact <* space)
      ps <- opt properties <* space
      pure (as, ps)

-- ----------------------------------------------------------------- [ Devices ]
devTy : Parser DeviceTy
devTy = do token "embedded"
           pure Embedded
    <|> do token "mobile"
           pure Mobile
    <|> do token "workstation"
           pure Workstation
    <|> do token "server"
           pure Server
    <?> "Device Type"

device : Parser $ DeploymentModel DEVICE
device = do
    token "device"
    ty <- opt devTy
    id <- ident <* space
    (es, ps) <- braces $ deviceBody
    pure $ Device (fromMaybe GenericDev ty) id es ps
   <?> "Device"
  where
    deviceBody : Parser (List $ DeploymentModel ENV, Maybe Attributes)
    deviceBody = do
      es <- some (exenv <* space)
      ps <- opt properties <* space
      pure (es, ps)

public
deploymentModel : Parser UML
deploymentModel = do
    ds <- some (device <* space)
    rs <- some (relation <* space)
    pure $ Deployment $ MkDeployment ds rs
  <?> "Deployment Model"
-- --------------------------------------------------------------------- [ EOF ]

max_stars_repo_name: jfdm/idris-uml

max_issues_repo_name: jfdm/idris-uml

max_forks_repo_name: jfdm/idris-uml


text:
{-

:doc Eq

interface Eq ty where
  (==) : ty -> ty -> Bool
  (/=) : ty -> ty -> Bool
-}

occurrences : Eq ty => (item : ty) -> (values : List ty) -> Nat
occurrences item [] = 0
occurrences item (value :: values) = case value == item of
                                          False => occurrences item values
                                          True => 1 + occurrences item values

data Matter = Solid | Liquid | Gas

Eq Matter where
    (==) Solid Solid = True
    (==) Liquid Liquid = True
    (==) Gas Gas = True
    (==) _ _ = False

-- occurrences Liquid [Solid, Liquid, Liquid, Gas]

[myEq] Eq Matter where
    (==) _ _ = True

-- occurrences @{myEq} Liquid [Solid, Liquid, Liquid, Gas]

max_stars_repo_name: wdomitrz/Coq-Exercises

max_issues_repo_name: wdomitrz/Coq-Exercises

max_forks_repo_name: wdomitrz/Coq-Exercises


text:
module Idrlisp.Env

import Data.IORef
import Data.SortedMap

%default total

||| An abstract representation of idrlisp environments.
export
record Env a where
  constructor MkEnv
  parent : Maybe (Env a)
  table : IORef (SortedMap String a)

export
new : Maybe (Env a) -> IO (Env a)
new parent = do
  table <- newIORef empty
  pure $ MkEnv parent table

export
define : String -> a -> Env a -> IO ()
define key value env = modifyIORef (table env) (insert key value)

export
set : String -> a -> Env a -> IO (Either String ())
set key value env = do
  t <- readIORef (table env)
  case lookup key t of
    Just _ => do
      writeIORef (table env) (insert key value t)
      pure $ Right ()
    Nothing =>
      case parent env of
        Just e => set key value (assert_smaller env e)
        Nothing => pure $ Left key

export
lookup : String -> Env a -> IO (Either String a)
lookup key env = do
  t <- readIORef (table env)
  case lookup key t of
    Just x => pure $ Right x
    Nothing =>
      case parent env of
        Just e => lookup key (assert_smaller env e)
        Nothing => pure $ Left key

max_stars_repo_name: yubrot/idrlisp

max_issues_repo_name: yubrot/idrlisp

max_forks_repo_name: yubrot/idrlisp


text:
module Intro

sm : List Nat -> Nat
sm [] = 0
sm (x :: xs) = x + (sm xs)

fct : Nat -> Nat
fct Z = 1
fct (S k) = (S k) * (fct k)

fbp : Nat -> (Nat, Nat)
fbp Z = (1, 1)
fbp (S k) = (snd (fbp k), fst (fbp k) + snd (fbp k))

fib : Nat -> Nat
fib n = fst (fbp n)

public export
add : Nat -> Nat -> Nat
add Z j = j
add (S k) j = S (add k j)

mul : Nat -> Nat -> Nat
mul Z j = Z
mul (S k) j = add j (mul k j)

sub : (n: Nat) -> (m : Nat) -> (LTE m n) -> Nat
sub n Z LTEZero = n
sub (S right) (S left) (LTESucc x) = sub right left x

oneLTEFour : LTE 1 4
oneLTEFour = LTESucc LTEZero

fourMinusOne : Nat
fourMinusOne = sub 4 1 oneLTEFour

reflLTE : (n: Nat) -> LTE n n
reflLTE Z = LTEZero
reflLTE (S k) = LTESucc (reflLTE k)

sillyZero: Nat -> Nat
sillyZero n = sub n n (reflLTE n)

idNat : Nat -> Nat
idNat = \x => x

loop: Nat -> Nat
loop k = loop (S k)


text:
module Group

%access public export

||| Given a type and a binary operation the type of proofs that the operation is associative
total
Associative : (typ : Type) -> ((*): typ -> typ -> typ) -> Type
Associative typ (*) = (a : typ) -> (b : typ) -> (c : typ) -> ((a * b) * c) = (a * (b * c))

||| Given a type and a binary operation the type of proofs that the operation is commutative
total
Commutative : (typ : Type) -> ((*) : typ -> typ -> typ) -> Type
Commutative typ (*) = (a : typ) -> (b : typ) -> (a * b) = (b * a)

||| Given a type and a binary operation the type of proofs that identity exists
total
IdentityExists : (typ : Type) -> ((*) : typ -> typ -> typ) -> Type
IdentityExists typ (*) = (e : typ ** (a : typ ** ((a*e) = a, (e*a) = a)))

||| Given a type and a binary operation the type of proofs that each element has its inverse
total
InverseExists : (typ : Type) -> ((*) : typ -> typ -> typ) -> Type
InverseExists typ (*) = (pfid : (IdentityExists typ (*)) ** ((a : typ) -> (a_inv : typ ** ((a*a_inv = fst(pfid)),(a_inv*a = fst(pfid))))))

--||| Given a type and a binary operation the type of proofs that the type along with the
||| operation is a group
total
IsGroup : (grp : Type) -> ((*) : grp -> grp -> grp) -> Type
IsGroup grp (*) = (Associative grp (*), (IdentityExists grp (*), InverseExists grp (*)))

-- Generates inverses
Inv: (grp : Type) -> ((*) : grp -> grp -> grp) -> IsGroup grp (*) -> (x: grp) -> grp
Inv grp (*) y x = fst(snd(snd(snd(y))) x)

-- Given a group, the type of proofs that it is abelian
total
IsAbelian:  (grp : Type) -> ((*) : grp -> grp -> grp) -> IsGroup grp (*) -> Type
IsAbelian grp (*) x = (a:grp) -> (b:grp) -> (a*b = b*a)

-- The type of proofs that a given function f between x and y is injective
total
Inj: (x: Type) -> (y: Type) -> (f: x-> y) -> Type
Inj x y f = ((a: x) -> (b: x) -> (f a = f b) -> a = b)

-- The type of proofs that a function between groups is a homomorphism
total
Hom: (grp : Type) -> ((*) : grp -> grp -> grp) -> (g : Type) -> ((***) : g -> g -> g) -> (f: grp -> g) -> Type
Hom grp (*) g (+) f = (a: grp) -> (b: grp) -> ((f (a*b)) = ((f a)+(f b)))

-- The type of proofs that a given group is a subgroup of another, via injective homorphisms
total
Subgroup: (h: Type) -> ((+) : h -> h -> h) -> (IsGroup h (+)) -> (g: Type) -> ((*) : g -> g -> g) -> (IsGroup g (*)) -> Type
Subgroup h (+) x g (*) y = DPair (h->g) (\f => ((Hom h (+) g (*) f), (Inj h g f)))

-- The type of proofs that a given subgroup is self-conjugate
total
NSub: (h: Type) -> ((+) : h -> h -> h) -> (x: IsGroup h (+)) -> (g: Type) -> ((*) : g -> g -> g) -> (y: IsGroup g (*)) -> (Subgroup h (+) x g (*) y) -> Type
NSub h (+) x g (*) y z = (a: h) -> (b: g) -> (x: h ** (b*(f a)*(inv b) = (f x))) where
  f = fst(z)
  inv = Inv g (*) y

{-
-- The type generated by the image of a function
data Imgfn: (x: Type) -> (y: Type) -> (f: x -> y) -> Type where
  Gen: (q: y) -> ((p: x ** (f(p) = q)) -> Unit) -> Imgfn x y f

-- Generates the coset over h of a given element in g
Coset: (h: Type) -> ((+) : h -> h -> h) -> (pf1: IsGroup h (+)) -> (g: Type) -> ((*) : g -> g -> g) -> (pf2: IsGroup g (*)) -> (Subgroup h (+) pf1 g (*) pf2) -> (a: g) -> Type
Coset h (+) pf1 g (*) pf2 sbgrp a =  Imgfn h g (\r => a*(fst(sbgrp) r))

-- Embedding the generated Imgfn in the image type
Imgembed: (x: Type) -> (y: Type) -> (f: x -> y) -> (Imgfn x y f) -> y
Imgembed x y f (Gen q pf) = q

-- Embedding the coset in g
Cosetembed: (h: Type) -> ((+) : h -> h -> h) -> (pf1: IsGroup h (+)) -> (g: Type) -> ((*) : g -> g -> g) -> (pf2: IsGroup g (*)) -> (sbgrp: Subgroup h (+) pf1 g (*) pf2) -> (a: g) -> (Coset h (+) pf1 g (*) pf2 sbgrp a) -> g
Cosetembed h (+) pf1 g (*) pf2 sbgrp a (Gen q pf) = q
-}


text:
module Parser.Lexer.Common

import public Text.Lexer

%default total

||| In `comment` we are careful not to parse closing delimiters as
||| valid comments. i.e. you may not write many dashes followed by
||| a closing brace and call it a valid comment.
export
comment : Lexer
comment
   =  is '-' <+> is '-'                  -- comment opener
  <+> many (is '-') <+> reject (is '}')  -- not a closing delimiter
  <+> many (isNot '\n')                  -- till the end of line

-- Identifier Lexer
-- There are multiple variants.

public export
data Flavour = AllowDashes | Capitalised | Normal

isIdentStart : Flavour -> Char -> Bool
isIdentStart _           '_' = True
isIdentStart Capitalised  x  = isUpper x || x > chr 160
isIdentStart _            x  = isAlpha x || x > chr 160

isIdentTrailing : Flavour -> Char -> Bool
isIdentTrailing AllowDashes '-'  = True
isIdentTrailing _           '\'' = True
isIdentTrailing _           '_'  = True
isIdentTrailing _            x   = isAlphaNum x || x > chr 160

export %inline
isIdent : Flavour -> String -> Bool
isIdent flavour string =
  case unpack string of
    []      => False
    (x::xs) => isIdentStart flavour x && all (isIdentTrailing flavour) xs

export %inline
ident : Flavour -> Lexer
ident flavour =
  (pred $ isIdentStart flavour) <+>
    (many . pred $ isIdentTrailing flavour)

export
isIdentNormal : String -> Bool
isIdentNormal = isIdent Normal

export
identNormal : Lexer
identNormal = ident Normal

export
identAllowDashes : Lexer
identAllowDashes = ident AllowDashes

namespaceIdent : Lexer
namespaceIdent = ident Capitalised <+> many (is '.' <+> ident Capitalised <+> expect (is '.'))

export
namespacedIdent : Lexer
namespacedIdent = namespaceIdent <+> opt (is '.' <+> identNormal)

export
spacesOrNewlines : Lexer
spacesOrNewlines = some (space <|> newline)


text:
module Optimisation.StaticProcessing.StaticTransformer

import Core.Context
import CairoCode.CairoCode
import CairoCode.CairoCodeUtils

import Data.List
import Data.SortedSet
import Data.SortedMap
import Primitives.Primitives
import Primitives.Externals
import Primitives.Common
import Optimisation.StaticProcessing.InstructionDeduplication
import CairoCode.Traversal.Base
import CairoCode.Traversal.ValueTracker
import CairoCode.Traversal.Composition
import Optimisation.StaticProcessing.StaticTracker
import Utils.Helpers
import Utils.Lens
import Debug.Trace

%hide Prelude.toList

record LocalStaticOptimState where
    constructor MkLocalStaticOptimState
    dedupState : TrackerState
    bindings : ScopedBindings StaticInfo
    elimDepth : Int

-- Lenses for leaner and more readable main definitions
dedupStateLens : Lens LocalStaticOptimState TrackerState
dedupStateLens = MkLens dedupState (\ts,fn => {dedupState $= fn} ts)

elimDepthLens : Lens LocalStaticOptimState Int
elimDepthLens = MkLens elimDepth (\ts,fn => {elimDepth $= fn} ts)

bindingsLens : Lens LocalStaticOptimState (ScopedBindings StaticInfo)
bindingsLens = MkLens bindings (\ts,fn => {bindings $= fn} ts)

inlineError : List StaticInfo -> List CairoReg -> Lazy (List (InstVisit CairoReg)) -> Traversal LocalStaticOptimState (List (InstVisit CairoReg))
inlineError args res noErrorTrav = if isCons errors
    then pure $ map (\r => VisitError r consolidateErrors) res
    else pure noErrorTrav
    where extractError : StaticInfo -> List String
          extractError (MKStaticInfo _ (Error err)) = [err]
          extractError _ = []
          errors : List String
          errors = args >>= extractError
          consolidateErrors : String
          consolidateErrors = foldl (\acc,err => acc ++ " " ++ err) "" errors

-- Because of assigns, repackings etc.. we may end up with multiple registers storing the same value
--  This function chooses one. It tries to choose the one least likely to be eliminated (or one that does not cost Insts if not eliminated)
-- Note: This assumes that list is sorted according to lifetime (which is default for CairoReg in CairoCode)
chooseBestReg : List CairoReg -> CairoReg
chooseBestReg (x::Nil) = x -- This is the case most likely to happen (only one candidate)
-- Note: If sort changes implement this differently (that is  why we treated this case seperately)
chooseBestReg (x::xs) = x
-- Note: This case is only used in Projection, everywhere else this would mean a mistake in the tracker
chooseBestReg Nil = Eliminated

export
resolveInfToReg : StaticInfo -> CairoReg
resolveInfToReg inf = result $ extractSingleConstant inf
    where result : Maybe CairoConst -> CairoReg
          result Nothing = chooseBestReg $ toList (inf.sources)
          result (Just c) = Const c

manifestRegister : CairoReg -> CairoReg -> InstVisit CairoReg
manifestRegister res (Const c) = VisitMkConstant res c
manifestRegister res Eliminated = VisitError res "CanNotManifestEliminatedRegister"
manifestRegister res reg = VisitAssign res reg

manifestConstant : CairoReg -> Maybe CairoConst -> InstVisit CairoReg
manifestConstant res Nothing = VisitError res "UndefinedConstantOperation"
manifestConstant res (Just c) = VisitMkConstant res c

canManifestEvalRes : EvalRes -> Bool
canManifestEvalRes (Failure _) = True
canManifestEvalRes (NewValue val) = isJust $ extractSingleConstant $ fromValueInfo val
canManifestEvalRes (ArgValue _) = True

manifestEvalRes : CairoReg -> EvalRes -> List StaticInfo -> InstVisit CairoReg
manifestEvalRes reg (Failure s) _ = VisitError reg "UndefinedPrimitiveOperation"
manifestEvalRes reg (NewValue val) _ = (manifestConstant reg) $ extractSingleConstant $ fromValueInfo val
manifestEvalRes reg (ArgValue Z) (x::xs) = VisitAssign reg (resolveInfToReg x)
manifestEvalRes reg (ArgValue (S rem)) (x::xs) = manifestEvalRes reg (ArgValue rem) xs
manifestEvalRes _  _ _ = assert_total $ idris_crash "can not process eval res"

reassignUnusedLinearImplicits : SortedSet LinearImplicit -> SortedMap LinearImplicit (StaticInfo, CairoReg) -> List (InstVisit CairoReg)
reassignUnusedLinearImplicits usedLinearImplicits availableLinearImplicits = map (\(_,(f,t)) => VisitAssign t (resolveInfToReg f)) unusedLinearImplicits
    where unusedLinearImplicits : List (LinearImplicit, (StaticInfo, CairoReg))
          unusedLinearImplicits = filter (\(i,_) => not (contains i usedLinearImplicits)) (toList availableLinearImplicits)

export
resolveLinearImplicits : SortedMap LinearImplicit (StaticInfo, CairoReg) -> SortedMap LinearImplicit (CairoReg, CairoReg)
resolveLinearImplicits linImpls = mapValueMap (\(f,t) => (resolveInfToReg f,t)) linImpls

canEliminate : Traversal LocalStaticOptimState Bool
canEliminate = map (/=0) (readStateL elimDepthLens)

eliminateBranch : Traversal LocalStaticOptimState (Maybe (List (InstVisit CairoReg)))
eliminateBranch = map (\_ => Just []) (updateStateL elimDepthLens (+1))

keepBranch : InstVisit CairoReg -> Traversal LocalStaticOptimState (Maybe (List (InstVisit CairoReg)))
keepBranch inst = pure $ Just [inst]

forwardBranchInst : Traversal LocalStaticOptimState (Maybe (List (InstVisit CairoReg)))
forwardBranchInst = pure Nothing

caseBindings : Traversal LocalStaticOptimState (Maybe StaticInfo)
caseBindings = composeState bindingsLens resolveCaseBinding
    where resolveCaseBinding : Traversal (ScopedBindings StaticInfo) (Maybe StaticInfo)
          resolveCaseBinding = case !getCaseReg of
              Nothing => pure Nothing
              (Just (Const c)) => pure $ Just $ MKStaticInfo (singleton $ Const c) (Const $ singleton c)
              (Just reg) => getBinding reg

branchFilter : InstVisit CairoReg -> Traversal LocalStaticOptimState (Maybe (List (InstVisit CairoReg)))
branchFilter (VisitConBranch reg) = canEliminate >>= process
    where process : Bool -> Traversal LocalStaticOptimState (Maybe (List (InstVisit CairoReg)))
          process True = eliminateBranch
          process False = forwardBranchInst

branchFilter (VisitConstBranch reg) = canEliminate >>= process
    where process : Bool -> Traversal LocalStaticOptimState (Maybe (List (InstVisit CairoReg)))
          process True = eliminateBranch
          process False = forwardBranchInst

branchFilter VisitBranchEnd = canEliminate >>= process
   where process : Bool -> Traversal LocalStaticOptimState (Maybe (List (InstVisit CairoReg)))
         process True = map (\_ => Just []) (updateStateL elimDepthLens (\a => a-1))
         process False = forwardBranchInst

branchFilter _ = canEliminate >>= process
   where process : Bool -> Traversal LocalStaticOptimState (Maybe (List (InstVisit CairoReg)))
         process True = pure $ Just []
         process False = forwardBranchInst

branchEliminationDetection : InstVisit StaticInfo -> Traversal LocalStaticOptimState (Maybe (List (InstVisit CairoReg)))
branchEliminationDetection (VisitConBranch (Just t)) = case !caseBindings of
    (Just (MKStaticInfo _ (Constructed ctrs))) => if isJust (lookup t ctrs) then keepBranch (VisitConBranch (Just t)) else eliminateBranch
    _ => keepBranch (VisitConBranch (Just t))
branchEliminationDetection (VisitConstBranch (Just c)) = case !caseBindings of
    (Just (MKStaticInfo _ (Const vals))) => if contains c vals then keepBranch (VisitConstBranch (Just c)) else eliminateBranch
    _ => keepBranch (VisitConstBranch (Just c))
branchEliminationDetection (VisitConBranch Nothing) = keepBranch (VisitConBranch Nothing)
branchEliminationDetection (VisitConstBranch Nothing) = keepBranch (VisitConstBranch Nothing)
branchEliminationDetection VisitBranchEnd = keepBranch VisitBranchEnd
branchEliminationDetection _ = forwardBranchInst

constantFoldTransform : SortedMap Name CairoDef -> InstVisit StaticInfo -> Traversal LocalStaticOptimState (List (InstVisit CairoReg))
constantFoldTransform defs inst = transformer inst
    where extractLinearImplicits : CairoDef -> SortedSet LinearImplicit
          extractLinearImplicits (FunDef _ linImpls _ _) = fromList $ keys linImpls
          extractLinearImplicits (ForeignDef info _ _) = fromList $ implicits info
          implicitLookup : SortedMap Name (SortedSet LinearImplicit)
          implicitLookup = mapValueMap extractLinearImplicits defs
          transformer : InstVisit StaticInfo -> Traversal LocalStaticOptimState (List (InstVisit CairoReg))
          transformer (VisitFunction name params impls rets) = pure [VisitFunction name params impls rets]
          transformer (VisitForeignFunction name info args rets) = pure [VisitForeignFunction name info args rets]
          transformer (VisitAssign res from) = inlineError [from] [res] [manifestRegister res (resolveInfToReg from)]
          transformer (VisitMkCon res tag args) = inlineError args [res] inst
            where repackedSrcs : List CairoReg
                  repackedSrcs = toList (findRepackedSrcs (resolveTag tag) args)
                  inst : List (InstVisit CairoReg)
                  inst = if isNil repackedSrcs
                    then [VisitMkCon res tag (map resolveInfToReg args)]
                    else [manifestRegister res (chooseBestReg repackedSrcs)]
          transformer (VisitMkClosure res name miss args) = inlineError args [res] [VisitMkClosure res name miss (map resolveInfToReg args)]
          transformer (VisitApply res linImpls (MKStaticInfo _ (Closure (Just (name, 1)) args)) arg) = inlineError allArgs [res] ((VisitCall [res] callLinearImplicits name (map resolveInfToReg allArgs))::implicitReassigns)
            where allArgs : List StaticInfo
                  allArgs = args ++ [arg]
                  usedLinearImplicits : SortedSet LinearImplicit
                  usedLinearImplicits = fromMaybe empty (lookup name implicitLookup)
                  callLinearImplicits : SortedMap LinearImplicit (CairoReg, CairoReg)
                  callLinearImplicits = resolveLinearImplicits $ fromList $ filter (\(i,_) => contains i usedLinearImplicits) (toList $ linImpls)
                  implicitReassigns : List (InstVisit CairoReg)
                  implicitReassigns = reassignUnusedLinearImplicits usedLinearImplicits linImpls
          transformer (VisitApply res linImpls (MKStaticInfo _ (Closure (Just (name, (S rem))) args)) arg) = inlineError allArgs [res] ((VisitMkClosure res name rem (map resolveInfToReg allArgs))::implicitReassigns)
            where allArgs : List StaticInfo
                  allArgs = args ++ [arg]
                  implicitReassigns : List (InstVisit CairoReg)
                  implicitReassigns = reassignUnusedLinearImplicits empty linImpls
          transformer (VisitApply res linImpls clo arg) = inlineError [clo,arg] [res] [VisitApply res (resolveLinearImplicits linImpls) (resolveInfToReg clo) (resolveInfToReg arg)]
          transformer (VisitOp res linImpls fn args) = inlineError args [res] (result (evaluateConstantOp fn (map toValueInfo args)))
                      where result : Maybe EvalRes -> List (InstVisit CairoReg)
                            result (Just nRes) = if canManifestEvalRes nRes
                              then (manifestEvalRes res nRes args)::(reassignUnusedLinearImplicits empty linImpls)
                              else [VisitOp res (resolveLinearImplicits linImpls) fn (map resolveInfToReg args)]
                            result _ = [VisitOp res (resolveLinearImplicits linImpls) fn (map resolveInfToReg args)]
          transformer (VisitCall res linImpls name args) = inlineError args res [VisitCall res (resolveLinearImplicits linImpls) name (map resolveInfToReg args)]
          transformer (VisitExtprim res linImpls name args) = inlineError args res (result (externalEval name (length res) (map toValueInfo args)))
            where result : Maybe (List EvalRes) -> List (InstVisit CairoReg)
                  result (Just nRes) = if all canManifestEvalRes nRes
                    then (zipWith (\reg,res => manifestEvalRes reg res args) res nRes) ++ (reassignUnusedLinearImplicits empty linImpls)
                    else [VisitExtprim res (resolveLinearImplicits linImpls) name (map resolveInfToReg args)]
                  result _ = [VisitExtprim res (resolveLinearImplicits linImpls) name (map resolveInfToReg args)]
          transformer (VisitReturn res linImpls) = pure [VisitReturn (map resolveInfToReg res) (mapValueMap resolveInfToReg linImpls)]
          transformer (VisitProject res arg@(MKStaticInfo _ (Constructed ctrs)) pos) = inlineError [arg] [res] (result (resolveInfToReg (extractField ctrs pos)))
            where result : CairoReg -> List (InstVisit CairoReg)
                  result Eliminated = [VisitProject res (resolveInfToReg arg) pos]
                  result reg = [manifestRegister res reg]
          transformer (VisitProject res arg pos) = inlineError [arg] [res] [VisitProject res (resolveInfToReg arg) pos]
          transformer (VisitCase reg) = pure [VisitCase (resolveInfToReg reg)]
          -- Untouched ones
          transformer VisitCaseEnd = pure $ [VisitCaseEnd]
          transformer (VisitNull reg) = pure $ [VisitNull reg]
          transformer (VisitError reg err) = pure $ [VisitError reg err]
          transformer (VisitMkConstant reg c) = pure $ [VisitMkConstant reg c]
          transformer VisitEndFunction = pure $ [VisitEndFunction]
          -- Covered by Branch Eliminator --
          transformer (VisitConBranch t) = assert_total $ idris_crash "constantFoldTransform must be coupled with a branch hanlder"
          transformer (VisitConstBranch c) = assert_total $ idris_crash "constantFoldTransform must be coupled with a branch hanlder"
          transformer VisitBranchEnd = assert_total $ idris_crash "constantFoldTransform must be coupled with a branch hanlder"

{-
 1. skips the instruction if it lies in an eliminated branch
 2. it substitutes registers for their statically known value
 3. if a branch instruction it decides if the branch is needed or not (used in 1.)
    for unneeded branches the branching instruction is skipped
 4. it replaces or eliminates instructions based on the static value of the used registers where possible
 5. it eliminates duplicated instructions (instructions already executed earlier on the same registers)
 6. for the remaining transformed instructions it statically executes them where possible to find the static values of its returns based on the static values of the inputs (for 2.)

 start - value (Reg) & state -> branchFilter | case Just: - value (Reg) & state ------------------------------------------------------------------------------v
                                             | case Nothing: - state ->  valueTransformer ( staticValueTracker, transformerPipeline) - value (Reg) & state -> end

 transformPipeline: start - value (StaticInfo) & state -> branchAwareFolder - state & [value (Reg)] -> for each value : instructionDeduplication - state & [value (Reg)] -> end

 branchAwareFolder: start - value (StaticInfo) & state -> branchEliminationDetection | case Just: - value (Reg) & state -----------------------------------------v
                    |                                                                | case Nothing: - state -> constantFoldTransform - [value (Reg)] & state -> end
                    | - value (StaticInfo) ---------------------------------------------------------------------^

branchFilter : Skippes unused branches
instructionDeduplication : Removes duplicated instructions (same regs as inputs)
constantFoldTransform : Simplifies instruction based on static input
-}
export
localStaticOptimizeDef : List (Name, CairoDef) -> (Name, CairoDef) -> (Name, CairoDef)
localStaticOptimizeDef defs def = snd $ runVisitTransformCairoDef (transformerPipeline, initialState) def
    where liftedStaticValueTracker: (v:InstVisit StaticInfo) -> Traversal LocalStaticOptimState (ValBindType v StaticInfo)
          liftedStaticValueTracker inst = composeState bindingsLens (staticValueTracker inst)
          branchAwareFolder : InstVisit StaticInfo -> Traversal LocalStaticOptimState (List (InstVisit CairoReg))
          branchAwareFolder = fallbackTraversal branchEliminationDetection (constantFoldTransform (fromList defs))
          transformPipeline : InstVisit StaticInfo -> Traversal LocalStaticOptimState (List (InstVisit CairoReg))
          transformPipeline = chainedTraversal branchAwareFolder (lensTraversal dedupStateLens instructionDeduplication)
          dbgDef : (Name, CairoDef) -> CairoReg -> StaticInfo
          dbgDef (name, def) reg = trace "Register not bound in \{show name}: \{show reg}" (MKStaticInfo (singleton reg) Unknown)
          activeBranchPipeline : InstVisit CairoReg -> Traversal LocalStaticOptimState (List (InstVisit CairoReg))
          activeBranchPipeline = valueTransformer bindingsLens (dbgDef def) liftedStaticValueTracker transformPipeline
          transformerPipeline : InstVisit CairoReg -> Traversal LocalStaticOptimState (List (InstVisit CairoReg))
          transformerPipeline = fallbackTraversal branchFilter activeBranchPipeline
          initialState : LocalStaticOptimState
          initialState = MkLocalStaticOptimState initialDedupState initialTrackerState 0

public export
localStaticOptimizeDefs : List (Name, CairoDef) -> List (Name, CairoDef)
localStaticOptimizeDefs defs = map (localStaticOptimizeDef defs) defs

-- A version witch allows generified call handling --
public export
record GlobalStaticOptimState s where
    constructor MkGlobalStaticOptimState
    folderState : LocalStaticOptimState
    globalState : s

-- Lenses for leaner and more readable main definitions
folderStateLens : Lens (GlobalStaticOptimState s) LocalStaticOptimState
folderStateLens = MkLens folderState (\ts,fn => {folderState $= fn} ts)

globalStateLens : Lens (GlobalStaticOptimState s) s
globalStateLens = MkLens globalState (\ts,fn => {globalState $= fn} ts)

public export
interface CallHandler s where
    -- Binds values of function value
    context : (List CairoReg, SortedMap LinearImplicit CairoReg) -> Traversal s (List StaticInfo, SortedMap LinearImplicit StaticInfo)
    -- Binds returns of a function
    return : List StaticInfo -> SortedMap LinearImplicit StaticInfo -> Traversal s ()
    -- Extract tracked values from processed function
    track : CallData -> Traversal s (List StaticInfo, SortedMap LinearImplicit StaticInfo)
    -- Replace tracked function with inlined code
    transform : CallData -> Traversal s (List (InstVisit CairoReg))
    -- defaults (same as unmodified value Tracker)
    context (params, impls) = pure (map paramInit params, mapValueMap paramInit impls)
        where paramInit : CairoReg -> StaticInfo
              paramInit reg = MKStaticInfo (singleton reg) Unknown
    return _ _ = pure ()
    track (MKCallData _ impls _ rs) = pure (map (\r => MKStaticInfo (singleton r) Unknown) rs, staticImplTracker impls)
    -- todo: make a more advanced inline error based one here as default -- needs to factor out traversal
    transform (MKCallData name impls args rs) = pure [VisitCall rs (resolveLinearImplicits impls) name (map resolveInfToReg args)]

callTracking : CallHandler s => CallData -> Traversal (GlobalStaticOptimState s) (List StaticInfo, SortedMap LinearImplicit StaticInfo)
callTracking callData = composeState globalStateLens (track callData)

callTransform: CallHandler s => CallData -> Traversal (GlobalStaticOptimState s) (List (InstVisit CairoReg))
callTransform callData = composeState globalStateLens (transform callData)

-- The actual generified folder (usable for global folding, inlining, specialisation, ...)
{-
 Works the same as localStaticOptimizeDef. However it can customize how call instructions are treated over a CallHandler
 Further it allows to collect the static values produced by  return instructions over CallHandler
 It introduces an additional state for the functions used in CallHandler
 This allows to define recursive algorithms that follow the call graph (thus global instead of local)
-}
public export
globalStaticOptimizeDef : CallHandler s => SortedMap Name CairoDef -> s -> (Name, CairoDef) -> ((Name, CairoDef), s)
globalStaticOptimizeDef defs globalState def = extract $ runVisitTransformCairoDef (transformerPipeline, initialState) def
    where bindLens : Lens (GlobalStaticOptimState s) (ScopedBindings StaticInfo)
          bindLens = join folderStateLens bindingsLens
          -- these just lift traversals defined on LocalStaticOptimState to work with (GlobalStaticOptimState s) by using a lense to point to the LocalStaticOptimState
          liftedStaticValueTracker: (v:InstVisit StaticInfo) -> Traversal (GlobalStaticOptimState s) (ValBindType v StaticInfo)
          liftedStaticValueTracker inst = composeState bindLens (staticValueTracker inst)
          liftedBranchEliminatorTransform : InstVisit StaticInfo -> Traversal (GlobalStaticOptimState s) (Maybe (List (InstVisit CairoReg)))
          liftedBranchEliminatorTransform inst = composeState folderStateLens (branchEliminationDetection inst)
          liftedBranchFilter : InstVisit CairoReg -> Traversal (GlobalStaticOptimState s) (Maybe (List (InstVisit CairoReg)))
          liftedBranchFilter inst = composeState folderStateLens (branchFilter inst)
          liftedConstantFoldTransform : InstVisit StaticInfo -> Traversal (GlobalStaticOptimState s) (List (InstVisit CairoReg))
          liftedConstantFoldTransform inst = composeState folderStateLens (constantFoldTransform defs inst)
          -- These use the CallHandler to customize the value Tracker
          -- we use explicit branching for 'customizedStaticValueTracker' because 'fallbackTraversal' has problems handling dependent type 'ValBindType v StaticInfo'
          customizedStaticValueTracker : (v:InstVisit StaticInfo) -> Traversal (GlobalStaticOptimState s) (ValBindType v StaticInfo)
          customizedStaticValueTracker (VisitCall rs impls name args) = callTracking (MKCallData name impls args rs)
          customizedStaticValueTracker (VisitFunction _ params impls _) = composeState globalStateLens (context (params, impls))
          -- Note: Putting this here is suboptimal as it requires the tracker to handle it
          --  but putting it in the transform prevents transformations of returns
          --  thats why its here and why we added a forwarding in the return case of the tracker
          customizedStaticValueTracker (VisitReturn res impls) = composeState globalStateLens (return res impls)
          customizedStaticValueTracker inst = liftedStaticValueTracker inst
          -- These use the CallHandler to customize the constant Folder
          -- we use explicit branching for 'customizedConstantFoldTransform' to be congruent with 'customizedStaticValueTracker'
          customizedConstantFoldTransform : InstVisit StaticInfo -> Traversal (GlobalStaticOptimState s) (List (InstVisit CairoReg))
          customizedConstantFoldTransform (VisitCall rs impls name args) = callTransform (MKCallData name impls args rs)
          customizedConstantFoldTransform inst = liftedConstantFoldTransform inst
          -- These are the same as in the local variant
          branchAwareFolder : InstVisit StaticInfo -> Traversal (GlobalStaticOptimState s) (List (InstVisit CairoReg))
          branchAwareFolder = fallbackTraversal liftedBranchEliminatorTransform customizedConstantFoldTransform
          transformPipeline : InstVisit StaticInfo -> Traversal (GlobalStaticOptimState s) (List (InstVisit CairoReg))
          transformPipeline = chainedTraversal branchAwareFolder (lensTraversal (join folderStateLens dedupStateLens) instructionDeduplication)
          dbgDef : (Name, CairoDef) -> CairoReg -> StaticInfo
          dbgDef (name, def) reg = trace "Register not bound in \{show name}: \{show reg}" (MKStaticInfo (singleton reg) Unknown)
          activeBranchPipeline : InstVisit CairoReg -> Traversal (GlobalStaticOptimState s) (List (InstVisit CairoReg))
          activeBranchPipeline = valueTransformer bindLens (dbgDef def) customizedStaticValueTracker transformPipeline
          transformerPipeline : InstVisit CairoReg -> Traversal (GlobalStaticOptimState s) (List (InstVisit CairoReg))
          transformerPipeline = fallbackTraversal liftedBranchFilter activeBranchPipeline
          initialState : GlobalStaticOptimState s
          initialState = MkGlobalStaticOptimState (MkLocalStaticOptimState initialDedupState initialTrackerState 0) globalState
          -- this does extract the CallHandler state from the GlobalStaticOptimState
          extract : (GlobalStaticOptimState s, (Name, CairoDef)) -> ((Name, CairoDef), s)
          extract (MkGlobalStaticOptimState _ globalState, def) = (def, globalState)