text:
module Web.Internal.ServiceworkerPrim

import JS
import Web.Internal.Types

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

namespace Cache

  export
  %foreign "browser:lambda:(x,a)=>x.addAll(a)"
  prim__addAll :  Cache
               -> Array (Union2 Request String)
               -> PrimIO (Promise Undefined)

  export
  %foreign "browser:lambda:(x,a)=>x.add(a)"
  prim__add : Cache -> Union2 Request String -> PrimIO (Promise Undefined)

  export
  %foreign "browser:lambda:(x,a,b)=>x.delete(a,b)"
  prim__delete :  Cache
               -> Union2 Request String
               -> UndefOr CacheQueryOptions
               -> PrimIO (Promise Boolean)

  export
  %foreign "browser:lambda:(x,a,b)=>x.keys(a,b)"
  prim__keys :  Cache
             -> UndefOr (Union2 Request String)
             -> UndefOr CacheQueryOptions
             -> PrimIO (Promise (Array Request))

  export
  %foreign "browser:lambda:(x,a,b)=>x.matchAll(a,b)"
  prim__matchAll :  Cache
                 -> UndefOr (Union2 Request String)
                 -> UndefOr CacheQueryOptions
                 -> PrimIO (Promise (Array Response))

  export
  %foreign "browser:lambda:(x,a,b)=>x.match(a,b)"
  prim__match :  Cache
              -> Union2 Request String
              -> UndefOr CacheQueryOptions
              -> PrimIO (Promise (Union2 Response Undefined))

  export
  %foreign "browser:lambda:(x,a,b)=>x.put(a,b)"
  prim__put :  Cache
            -> Union2 Request String
            -> Response
            -> PrimIO (Promise Undefined)

namespace CacheStorage

  export
  %foreign "browser:lambda:(x,a)=>x.delete(a)"
  prim__delete : CacheStorage -> String -> PrimIO (Promise Boolean)

  export
  %foreign "browser:lambda:(x,a)=>x.has(a)"
  prim__has : CacheStorage -> String -> PrimIO (Promise Boolean)

  export
  %foreign "browser:lambda:x=>x.keys()"
  prim__keys : CacheStorage -> PrimIO (Promise (Array String))

  export
  %foreign "browser:lambda:(x,a,b)=>x.match(a,b)"
  prim__match :  CacheStorage
              -> Union2 Request String
              -> UndefOr MultiCacheQueryOptions
              -> PrimIO (Promise (Union2 Response Undefined))

  export
  %foreign "browser:lambda:(x,a)=>x.open(a)"
  prim__open : CacheStorage -> String -> PrimIO (Promise Cache)

namespace Client

  export
  %foreign "browser:lambda:x=>x.frameType"
  prim__frameType : Client -> PrimIO String

  export
  %foreign "browser:lambda:x=>x.id"
  prim__id : Client -> PrimIO String

  export
  %foreign "browser:lambda:x=>x.type"
  prim__type : Client -> PrimIO String

  export
  %foreign "browser:lambda:x=>x.url"
  prim__url : Client -> PrimIO String

  export
  %foreign "browser:lambda:(x,a,b)=>x.postMessage(a,b)"
  prim__postMessage : Client -> AnyPtr -> Array Object -> PrimIO ()

  export
  %foreign "browser:lambda:(x,a,b)=>x.postMessage(a,b)"
  prim__postMessage1 :  Client
                     -> AnyPtr
                     -> UndefOr PostMessageOptions
                     -> PrimIO ()

namespace Clients

  export
  %foreign "browser:lambda:x=>x.claim()"
  prim__claim : Clients -> PrimIO (Promise Undefined)

  export
  %foreign "browser:lambda:(x,a)=>x.get(a)"
  prim__get : Clients -> String -> PrimIO (Promise (Union2 Client Undefined))

  export
  %foreign "browser:lambda:(x,a)=>x.matchAll(a)"
  prim__matchAll :  Clients
                 -> UndefOr ClientQueryOptions
                 -> PrimIO (Promise (Array Client))

  export
  %foreign "browser:lambda:(x,a)=>x.openWindow(a)"
  prim__openWindow :  Clients
                   -> String
                   -> PrimIO (Promise (Nullable WindowClient))

namespace ExtendableEvent

  export
  %foreign "browser:lambda:(a,b)=> new ExtendableEvent(a,b)"
  prim__new : String -> UndefOr ExtendableEventInit -> PrimIO ExtendableEvent

  export
  %foreign "browser:lambda:(x,a)=>x.waitUntil(a)"
  prim__waitUntil : ExtendableEvent -> Promise AnyPtr -> PrimIO ()

namespace ExtendableMessageEvent

  export
  %foreign "browser:lambda:(a,b)=> new ExtendableMessageEvent(a,b)"
  prim__new :  String
            -> UndefOr ExtendableMessageEventInit
            -> PrimIO ExtendableMessageEvent

  export
  %foreign "browser:lambda:x=>x.data"
  prim__data : ExtendableMessageEvent -> PrimIO AnyPtr

  export
  %foreign "browser:lambda:x=>x.lastEventId"
  prim__lastEventId : ExtendableMessageEvent -> PrimIO String

  export
  %foreign "browser:lambda:x=>x.origin"
  prim__origin : ExtendableMessageEvent -> PrimIO String

  export
  %foreign "browser:lambda:x=>x.ports"
  prim__ports : ExtendableMessageEvent -> PrimIO (Array MessagePort)

  export
  %foreign "browser:lambda:x=>x.source"
  prim__source :  ExtendableMessageEvent
               -> PrimIO (Nullable (Union3 Client ServiceWorker MessagePort))

namespace FetchEvent

  export
  %foreign "browser:lambda:(a,b)=> new FetchEvent(a,b)"
  prim__new : String -> FetchEventInit -> PrimIO FetchEvent

  export
  %foreign "browser:lambda:x=>x.clientId"
  prim__clientId : FetchEvent -> PrimIO String

  export
  %foreign "browser:lambda:x=>x.handled"
  prim__handled : FetchEvent -> PrimIO (Promise Undefined)

  export
  %foreign "browser:lambda:x=>x.preloadResponse"
  prim__preloadResponse : FetchEvent -> PrimIO (Promise AnyPtr)

  export
  %foreign "browser:lambda:x=>x.replacesClientId"
  prim__replacesClientId : FetchEvent -> PrimIO String

  export
  %foreign "browser:lambda:x=>x.request"
  prim__request : FetchEvent -> PrimIO Request

  export
  %foreign "browser:lambda:x=>x.resultingClientId"
  prim__resultingClientId : FetchEvent -> PrimIO String

  export
  %foreign "browser:lambda:(x,a)=>x.respondWith(a)"
  prim__respondWith : FetchEvent -> Promise Response -> PrimIO ()

namespace NavigationPreloadManager

  export
  %foreign "browser:lambda:x=>x.disable()"
  prim__disable : NavigationPreloadManager -> PrimIO (Promise Undefined)

  export
  %foreign "browser:lambda:x=>x.enable()"
  prim__enable : NavigationPreloadManager -> PrimIO (Promise Undefined)

  export
  %foreign "browser:lambda:x=>x.getState()"
  prim__getState :  NavigationPreloadManager
                 -> PrimIO (Promise NavigationPreloadState)

  export
  %foreign "browser:lambda:(x,a)=>x.setHeaderValue(a)"
  prim__setHeaderValue :  NavigationPreloadManager
                       -> ByteString
                       -> PrimIO (Promise Undefined)

namespace ServiceWorker

  export
  %foreign "browser:lambda:x=>x.onstatechange"
  prim__onstatechange : ServiceWorker -> PrimIO (Nullable EventHandlerNonNull)

  export
  %foreign "browser:lambda:(x,v)=>{x.onstatechange = v}"
  prim__setOnstatechange :  ServiceWorker
                         -> Nullable EventHandlerNonNull
                         -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.scriptURL"
  prim__scriptURL : ServiceWorker -> PrimIO String

  export
  %foreign "browser:lambda:x=>x.state"
  prim__state : ServiceWorker -> PrimIO String

  export
  %foreign "browser:lambda:(x,a,b)=>x.postMessage(a,b)"
  prim__postMessage : ServiceWorker -> AnyPtr -> Array Object -> PrimIO ()

  export
  %foreign "browser:lambda:(x,a,b)=>x.postMessage(a,b)"
  prim__postMessage1 :  ServiceWorker
                     -> AnyPtr
                     -> UndefOr PostMessageOptions
                     -> PrimIO ()

namespace ServiceWorkerContainer

  export
  %foreign "browser:lambda:x=>x.controller"
  prim__controller : ServiceWorkerContainer -> PrimIO (Nullable ServiceWorker)

  export
  %foreign "browser:lambda:x=>x.oncontrollerchange"
  prim__oncontrollerchange :  ServiceWorkerContainer
                           -> PrimIO (Nullable EventHandlerNonNull)

  export
  %foreign "browser:lambda:(x,v)=>{x.oncontrollerchange = v}"
  prim__setOncontrollerchange :  ServiceWorkerContainer
                              -> Nullable EventHandlerNonNull
                              -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.onmessage"
  prim__onmessage :  ServiceWorkerContainer
                  -> PrimIO (Nullable EventHandlerNonNull)

  export
  %foreign "browser:lambda:(x,v)=>{x.onmessage = v}"
  prim__setOnmessage :  ServiceWorkerContainer
                     -> Nullable EventHandlerNonNull
                     -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.onmessageerror"
  prim__onmessageerror :  ServiceWorkerContainer
                       -> PrimIO (Nullable EventHandlerNonNull)

  export
  %foreign "browser:lambda:(x,v)=>{x.onmessageerror = v}"
  prim__setOnmessageerror :  ServiceWorkerContainer
                          -> Nullable EventHandlerNonNull
                          -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.ready"
  prim__ready :  ServiceWorkerContainer
              -> PrimIO (Promise ServiceWorkerRegistration)

  export
  %foreign "browser:lambda:(x,a)=>x.getRegistration(a)"
  prim__getRegistration :  ServiceWorkerContainer
                        -> UndefOr String
                        -> PrimIO (Promise (Union2 ServiceWorkerRegistration
                                                   Undefined))

  export
  %foreign "browser:lambda:x=>x.getRegistrations()"
  prim__getRegistrations :  ServiceWorkerContainer
                         -> PrimIO (Promise (Array ServiceWorkerRegistration))

  export
  %foreign "browser:lambda:(x,a,b)=>x.register(a,b)"
  prim__register :  ServiceWorkerContainer
                 -> String
                 -> UndefOr RegistrationOptions
                 -> PrimIO (Promise ServiceWorkerRegistration)

  export
  %foreign "browser:lambda:x=>x.startMessages()"
  prim__startMessages : ServiceWorkerContainer -> PrimIO ()

namespace ServiceWorkerGlobalScope

  export
  %foreign "browser:lambda:x=>x.clients"
  prim__clients : ServiceWorkerGlobalScope -> PrimIO Clients

  export
  %foreign "browser:lambda:x=>x.onactivate"
  prim__onactivate :  ServiceWorkerGlobalScope
                   -> PrimIO (Nullable EventHandlerNonNull)

  export
  %foreign "browser:lambda:(x,v)=>{x.onactivate = v}"
  prim__setOnactivate :  ServiceWorkerGlobalScope
                      -> Nullable EventHandlerNonNull
                      -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.onfetch"
  prim__onfetch :  ServiceWorkerGlobalScope
                -> PrimIO (Nullable EventHandlerNonNull)

  export
  %foreign "browser:lambda:(x,v)=>{x.onfetch = v}"
  prim__setOnfetch :  ServiceWorkerGlobalScope
                   -> Nullable EventHandlerNonNull
                   -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.oninstall"
  prim__oninstall :  ServiceWorkerGlobalScope
                  -> PrimIO (Nullable EventHandlerNonNull)

  export
  %foreign "browser:lambda:(x,v)=>{x.oninstall = v}"
  prim__setOninstall :  ServiceWorkerGlobalScope
                     -> Nullable EventHandlerNonNull
                     -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.onmessage"
  prim__onmessage :  ServiceWorkerGlobalScope
                  -> PrimIO (Nullable EventHandlerNonNull)

  export
  %foreign "browser:lambda:(x,v)=>{x.onmessage = v}"
  prim__setOnmessage :  ServiceWorkerGlobalScope
                     -> Nullable EventHandlerNonNull
                     -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.onmessageerror"
  prim__onmessageerror :  ServiceWorkerGlobalScope
                       -> PrimIO (Nullable EventHandlerNonNull)

  export
  %foreign "browser:lambda:(x,v)=>{x.onmessageerror = v}"
  prim__setOnmessageerror :  ServiceWorkerGlobalScope
                          -> Nullable EventHandlerNonNull
                          -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.registration"
  prim__registration :  ServiceWorkerGlobalScope
                     -> PrimIO ServiceWorkerRegistration

  export
  %foreign "browser:lambda:x=>x.serviceWorker"
  prim__serviceWorker : ServiceWorkerGlobalScope -> PrimIO ServiceWorker

  export
  %foreign "browser:lambda:x=>x.skipWaiting()"
  prim__skipWaiting : ServiceWorkerGlobalScope -> PrimIO (Promise Undefined)

namespace ServiceWorkerRegistration

  export
  %foreign "browser:lambda:x=>x.active"
  prim__active : ServiceWorkerRegistration -> PrimIO (Nullable ServiceWorker)

  export
  %foreign "browser:lambda:x=>x.installing"
  prim__installing :  ServiceWorkerRegistration
                   -> PrimIO (Nullable ServiceWorker)

  export
  %foreign "browser:lambda:x=>x.navigationPreload"
  prim__navigationPreload :  ServiceWorkerRegistration
                          -> PrimIO NavigationPreloadManager

  export
  %foreign "browser:lambda:x=>x.onupdatefound"
  prim__onupdatefound :  ServiceWorkerRegistration
                      -> PrimIO (Nullable EventHandlerNonNull)

  export
  %foreign "browser:lambda:(x,v)=>{x.onupdatefound = v}"
  prim__setOnupdatefound :  ServiceWorkerRegistration
                         -> Nullable EventHandlerNonNull
                         -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.scope"
  prim__scope : ServiceWorkerRegistration -> PrimIO String

  export
  %foreign "browser:lambda:x=>x.updateViaCache"
  prim__updateViaCache : ServiceWorkerRegistration -> PrimIO String

  export
  %foreign "browser:lambda:x=>x.waiting"
  prim__waiting : ServiceWorkerRegistration -> PrimIO (Nullable ServiceWorker)

  export
  %foreign "browser:lambda:x=>x.unregister()"
  prim__unregister : ServiceWorkerRegistration -> PrimIO (Promise Boolean)

  export
  %foreign "browser:lambda:x=>x.update()"
  prim__update : ServiceWorkerRegistration -> PrimIO (Promise Undefined)

namespace WindowClient

  export
  %foreign "browser:lambda:x=>x.ancestorOrigins"
  prim__ancestorOrigins : WindowClient -> PrimIO (Array String)

  export
  %foreign "browser:lambda:x=>x.focused"
  prim__focused : WindowClient -> PrimIO Boolean

  export
  %foreign "browser:lambda:x=>x.visibilityState"
  prim__visibilityState : WindowClient -> PrimIO String

  export
  %foreign "browser:lambda:x=>x.focus()"
  prim__focus : WindowClient -> PrimIO (Promise WindowClient)

  export
  %foreign "browser:lambda:(x,a)=>x.navigate(a)"
  prim__navigate :  WindowClient
                 -> String
                 -> PrimIO (Promise (Nullable WindowClient))

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

namespace CacheQueryOptions

  export
  %foreign "browser:lambda:(a,b,c)=> {ignoreSearch: a,ignoreMethod: b,ignoreVary: c}"
  prim__new :  UndefOr Boolean
            -> UndefOr Boolean
            -> UndefOr Boolean
            -> PrimIO CacheQueryOptions

  export
  %foreign "browser:lambda:x=>x.ignoreMethod"
  prim__ignoreMethod : CacheQueryOptions -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.ignoreMethod = v}"
  prim__setIgnoreMethod : CacheQueryOptions -> UndefOr Boolean -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.ignoreSearch"
  prim__ignoreSearch : CacheQueryOptions -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.ignoreSearch = v}"
  prim__setIgnoreSearch : CacheQueryOptions -> UndefOr Boolean -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.ignoreVary"
  prim__ignoreVary : CacheQueryOptions -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.ignoreVary = v}"
  prim__setIgnoreVary : CacheQueryOptions -> UndefOr Boolean -> PrimIO ()

namespace ClientQueryOptions

  export
  %foreign "browser:lambda:(a,b)=> {includeUncontrolled: a,type: b}"
  prim__new : UndefOr Boolean -> UndefOr String -> PrimIO ClientQueryOptions

  export
  %foreign "browser:lambda:x=>x.includeUncontrolled"
  prim__includeUncontrolled : ClientQueryOptions -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.includeUncontrolled = v}"
  prim__setIncludeUncontrolled :  ClientQueryOptions
                               -> UndefOr Boolean
                               -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.type"
  prim__type : ClientQueryOptions -> PrimIO (UndefOr String)

  export
  %foreign "browser:lambda:(x,v)=>{x.type = v}"
  prim__setType : ClientQueryOptions -> UndefOr String -> PrimIO ()

namespace ExtendableEventInit

  export
  %foreign "browser:lambda:()=> {}"
  prim__new : PrimIO ExtendableEventInit

namespace ExtendableMessageEventInit

  export
  %foreign "browser:lambda:(a,b,c,d,e)=> {data: a,origin: b,lastEventId: c,source: d,ports: e}"
  prim__new :  UndefOr AnyPtr
            -> UndefOr String
            -> UndefOr String
            -> UndefOr (Nullable (Union3 Client ServiceWorker MessagePort))
            -> UndefOr (Array MessagePort)
            -> PrimIO ExtendableMessageEventInit

  export
  %foreign "browser:lambda:x=>x.data"
  prim__data : ExtendableMessageEventInit -> PrimIO (UndefOr AnyPtr)

  export
  %foreign "browser:lambda:(x,v)=>{x.data = v}"
  prim__setData : ExtendableMessageEventInit -> UndefOr AnyPtr -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.lastEventId"
  prim__lastEventId : ExtendableMessageEventInit -> PrimIO (UndefOr String)

  export
  %foreign "browser:lambda:(x,v)=>{x.lastEventId = v}"
  prim__setLastEventId :  ExtendableMessageEventInit
                       -> UndefOr String
                       -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.origin"
  prim__origin : ExtendableMessageEventInit -> PrimIO (UndefOr String)

  export
  %foreign "browser:lambda:(x,v)=>{x.origin = v}"
  prim__setOrigin : ExtendableMessageEventInit -> UndefOr String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.ports"
  prim__ports :  ExtendableMessageEventInit
              -> PrimIO (UndefOr (Array MessagePort))

  export
  %foreign "browser:lambda:(x,v)=>{x.ports = v}"
  prim__setPorts :  ExtendableMessageEventInit
                 -> UndefOr (Array MessagePort)
                 -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.source"
  prim__source :  ExtendableMessageEventInit
               -> PrimIO (UndefOr (Nullable (Union3 Client
                                                    ServiceWorker
                                                    MessagePort)))

  export
  %foreign "browser:lambda:(x,v)=>{x.source = v}"
  prim__setSource :  ExtendableMessageEventInit
                  -> UndefOr (Nullable (Union3 Client
                                               ServiceWorker
                                               MessagePort))
                  -> PrimIO ()

namespace FetchEventInit

  export
  %foreign "browser:lambda:(a,b,c,d,e,f)=> {request: a,preloadResponse: b,clientId: c,resultingClientId: d,replacesClientId: e,handled: f}"
  prim__new :  Request
            -> UndefOr (Promise AnyPtr)
            -> UndefOr String
            -> UndefOr String
            -> UndefOr String
            -> UndefOr (Promise Undefined)
            -> PrimIO FetchEventInit

  export
  %foreign "browser:lambda:x=>x.clientId"
  prim__clientId : FetchEventInit -> PrimIO (UndefOr String)

  export
  %foreign "browser:lambda:(x,v)=>{x.clientId = v}"
  prim__setClientId : FetchEventInit -> UndefOr String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.handled"
  prim__handled : FetchEventInit -> PrimIO (UndefOr (Promise Undefined))

  export
  %foreign "browser:lambda:(x,v)=>{x.handled = v}"
  prim__setHandled : FetchEventInit -> UndefOr (Promise Undefined) -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.preloadResponse"
  prim__preloadResponse : FetchEventInit -> PrimIO (UndefOr (Promise AnyPtr))

  export
  %foreign "browser:lambda:(x,v)=>{x.preloadResponse = v}"
  prim__setPreloadResponse :  FetchEventInit
                           -> UndefOr (Promise AnyPtr)
                           -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.replacesClientId"
  prim__replacesClientId : FetchEventInit -> PrimIO (UndefOr String)

  export
  %foreign "browser:lambda:(x,v)=>{x.replacesClientId = v}"
  prim__setReplacesClientId : FetchEventInit -> UndefOr String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.request"
  prim__request : FetchEventInit -> PrimIO Request

  export
  %foreign "browser:lambda:(x,v)=>{x.request = v}"
  prim__setRequest : FetchEventInit -> Request -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.resultingClientId"
  prim__resultingClientId : FetchEventInit -> PrimIO (UndefOr String)

  export
  %foreign "browser:lambda:(x,v)=>{x.resultingClientId = v}"
  prim__setResultingClientId : FetchEventInit -> UndefOr String -> PrimIO ()

namespace MultiCacheQueryOptions

  export
  %foreign "browser:lambda:(a)=> {cacheName: a}"
  prim__new : UndefOr String -> PrimIO MultiCacheQueryOptions

  export
  %foreign "browser:lambda:x=>x.cacheName"
  prim__cacheName : MultiCacheQueryOptions -> PrimIO (UndefOr String)

  export
  %foreign "browser:lambda:(x,v)=>{x.cacheName = v}"
  prim__setCacheName : MultiCacheQueryOptions -> UndefOr String -> PrimIO ()

namespace NavigationPreloadState

  export
  %foreign "browser:lambda:(a,b)=> {enabled: a,headerValue: b}"
  prim__new :  UndefOr Boolean
            -> UndefOr ByteString
            -> PrimIO NavigationPreloadState

  export
  %foreign "browser:lambda:x=>x.enabled"
  prim__enabled : NavigationPreloadState -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.enabled = v}"
  prim__setEnabled : NavigationPreloadState -> UndefOr Boolean -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.headerValue"
  prim__headerValue : NavigationPreloadState -> PrimIO (UndefOr ByteString)

  export
  %foreign "browser:lambda:(x,v)=>{x.headerValue = v}"
  prim__setHeaderValue :  NavigationPreloadState
                       -> UndefOr ByteString
                       -> PrimIO ()

namespace RegistrationOptions

  export
  %foreign "browser:lambda:(a,b,c)=> {scope: a,type: b,updateViaCache: c}"
  prim__new :  UndefOr String
            -> UndefOr String
            -> UndefOr String
            -> PrimIO RegistrationOptions

  export
  %foreign "browser:lambda:x=>x.scope"
  prim__scope : RegistrationOptions -> PrimIO (UndefOr String)

  export
  %foreign "browser:lambda:(x,v)=>{x.scope = v}"
  prim__setScope : RegistrationOptions -> UndefOr String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.type"
  prim__type : RegistrationOptions -> PrimIO (UndefOr String)

  export
  %foreign "browser:lambda:(x,v)=>{x.type = v}"
  prim__setType : RegistrationOptions -> UndefOr String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.updateViaCache"
  prim__updateViaCache : RegistrationOptions -> PrimIO (UndefOr String)

  export
  %foreign "browser:lambda:(x,v)=>{x.updateViaCache = v}"
  prim__setUpdateViaCache : RegistrationOptions -> UndefOr String -> PrimIO ()


text:
StringOrInt : Bool -> Type
StringOrInt x = case x of
  True => Int
  False => String

getStringOrInt : (x : Bool) -> StringOrInt x
getStringOrInt x = case x of
  True => 94
  False => "Ninety four"

valToString : (x : Bool) -> StringOrInt x -> String
valToString x val = case x of
  True => cast val
  False => val
  -- True => ?xTrueType
  -- False => ?xFalseType

ext: idr

max_stars_repo_name: jeremy-miller/type-driven-development

max_issues_repo_name: jeremy-miller/type-driven-development

max_forks_repo_name: jeremy-miller/type-driven-development


text:
module Problem1

import Common.Lte

%default total

Decr : (Nat -> Nat) -> Type
Decr f = (x : Nat) -> LTE (f (S x)) (f x)

Valley : (Nat -> Nat) -> Nat -> Nat -> Type
Valley f n x = (y : Nat) -> LTE x y -> LTE y (n+x) -> f y = f x

decrN : (n : Nat) -> (f : Nat -> Nat) -> Decr f -> (x : Nat) ->
        LTE (f (n + x)) (f x)
decrN Z f decr x = lteRefl
decrN (S n') f decr x =
  let ind = decrN n' f decr x
      decrLte = decr (n' + x)
  in lteTransitive decrLte ind

boundedAbove : (decr : Decr f) -> (a : Nat) -> (x : Nat) -> LTE a x ->
               LTE (f x) (f a)
boundedAbove decr a x lte =
  case splitLte lte of
    (Left eq) => rewrite eq in lteRefl
    (Right lt) =>
      let S x' = x
          lte' = fromLteSucc lt
          ind = boundedAbove decr a x' lte'
      in decr x' `lteTransitive` ind

boundedBelow : (n : Nat) -> (decr : Decr f) ->
               (a : Nat) -> (x : Nat) -> LTE x (n + a) ->
               LTE (f (n + a)) (f x)
boundedBelow Z decr a x lte = boundedAbove decr x a lte
boundedBelow n@(S n') decr a x lte =
  case splitLte lte of
    (Left eq) => boundedAbove decr x (S (n' + a)) lte
    (Right lt) =>
      let ind = boundedBelow n' decr a x (fromLteSucc lt)
      in decr (n' + a) `lteTransitive` ind

mkValley : (n : Nat) -> (f : Nat -> Nat) -> (decr : Decr f) ->
           (x : Nat) -> f x = f (n + x) ->
           (y : Nat) -> LTE x y -> LTE y (n + x) -> f y = f x
mkValley n f decr x prf y lteL lteU =
  let u = boundedAbove decr x y lteL
      l = boundedBelow n decr x y lteU
  in tightBound u (rewrite prf in l)

decrValley_rec : (n : Nat) -> (f : Nat -> Nat) -> (decr : Decr f) ->
                 (x : Nat) -> (bound : Nat) -> (boundLte : LTE (f x) bound) ->
                 (a : Nat ** Valley f n a)
decrValley_rec n f decr x Z boundLte =
  let boundLteN = decrN n f decr x
      boundLteN' = lteTransitive boundLteN boundLte
      xEqZ = lteZeqZ boundLte
      xNEqZ = lteZeqZ boundLteN'
      xEqNx = xEqZ `trans` sym xNEqZ
  in (x ** mkValley n f decr x xEqNx)

decrValley_rec n f decr x bound@(S bound') boundLte =
  case splitLte boundLte of
    (Right (LTESucc boundLte')) => decrValley_rec n f decr x bound' boundLte'
    (Left boundEq) =>
      let boundLteN = decrN n f decr x
      in case splitLte boundLteN of
              (Right boundLtN) =>
                let boundLteN' = fromLteSucc (boundLtN `lteTransitive` boundLte)
                in decrValley_rec n f decr (n + x) bound' boundLteN'
              (Left boundEqN) => (x ** mkValley n f decr x (sym boundEqN))

decrValley : (n : Nat) -> (f : Nat -> Nat) -> Decr f -> (x : Nat ** Valley f n x)
decrValley n f decr = decrValley_rec n f decr Z (f Z) lteRefl

max_stars_repo_name: farrellm/dailyprover

max_issues_repo_name: farrellm/dailyprover

max_forks_repo_name: farrellm/dailyprover


text:
module Compiler.Interpreter.VMCode

import Core.Core
import Core.Context
import Core.Context.Log
import Core.Primitives
import Core.Value
import Compiler.Common
import Compiler.VMCode
import Libraries.Data.IOArray
import Libraries.Data.NameMap
import Data.Nat
import Data.SnocList
import Data.Vect

public export
data Object : Type where
    Closure : (predMissing : Nat) -> (args : SnocList Object) -> Name -> Object
    Constructor : (tag : Either Int Name) -> (args : List Object) -> Object
    Const : Constant -> Object
    Null : Object

showType : Object -> String
showType (Closure _ _ _) = "Closure"
showType (Constructor _ _) = "Constructor"
showType (Const _) = "Constant"
showType Null = "Null"

mutual
    showSep : Nat -> List Object -> String
    showSep k [] = ""
    showSep k [o] = showDepth k o
    showSep k (o :: os) = showDepth k o ++ ", " ++ showSep k os

    showDepth : Nat -> Object -> String
    showDepth (S k) (Closure mis args fn) = show fn ++ "-" ++ show mis ++ "(" ++ showSep k (args <>> []) ++ ")"
    showDepth (S k) (Constructor (Left t) args) = "tag" ++ show t ++ "(" ++ showSep k args ++ ")"
    showDepth (S k) (Const c) = show c
    showDepth _ obj = showType obj

Show Object where
    show = showDepth 5

data State : Type where
record InterpState where
    constructor MkInterpState
    defs : NameMap VMDef
    locals : IOArray Object
    returnObj : Maybe Object

initInterpState : List (Name, VMDef) -> Core InterpState
initInterpState defsList = do
    let defs = fromList defsList
    locals <- coreLift $ newArray 0
    let returnObj = Nothing
    pure $ MkInterpState defs locals returnObj

0
Stack : Type
Stack = List Name

interpError : Ref State InterpState => Stack -> String -> Core a
interpError stk msg = do
    MkInterpState _ ls ret <- get State
    lsList <- coreLift $ toList ls
    throw $ InternalError $ "Interpreter Error in " ++ show (take 10 stk) ++ ":\n" ++ msg
        ++ "\n\nlocals:\n" ++ showWithIndex lsList
        ++ "\nreturn:\n  " ++ show ret
  where
    showWithIndex : forall a. {default 0 idx : Nat} -> Show a => List a -> String
    showWithIndex {idx} [] = ""
    showWithIndex {idx} (x :: xs) = "  " ++ show idx ++ ": " ++ show x ++ "\n" ++ showWithIndex {idx = S idx} xs

getReg : Ref State InterpState => Stack -> Reg -> Core Object
getReg stk (Loc i) = do
    ls <- locals <$> get State
    objm <- coreLift $ readArray ls i
    case objm of
        Just obj => pure obj
        Nothing =>
            interpError stk $ "Missing local " ++ show i
getReg stk RVal = do
    objm <- returnObj <$> get State
    case objm of
        Just obj => pure obj
        Nothing => interpError stk "Missing returnObj val"
getReg stk Discard = pure Null

setReg : Ref State InterpState => Stack -> Reg -> Object -> Core ()
setReg stk RVal obj = update State $ record { returnObj = Just obj }
setReg stk (Loc i) obj = do
    ls <- locals <$> get State
    when (i >= max ls) $ interpError stk $ "Attempt to set register: " ++ show i ++ ", size of locals: " ++ show (max ls)
    coreLift $ writeArray ls i obj
setReg stk Discard _ = pure ()

saveLocals : Ref State InterpState => Core a -> Core a
saveLocals act = do
    st <- get State
    x <- act
    put State st
    pure x

total
indexMaybe : List a -> Int -> Maybe a
indexMaybe [] _ = Nothing
indexMaybe (x :: xs) idx = if idx <= 0 then Just x else indexMaybe xs (idx - 1)

callPrim : Ref State InterpState => Stack -> PrimFn ar -> Vect ar Object -> Core Object
callPrim stk BelieveMe [_, _, obj] = pure obj
callPrim stk fn args = case the (Either Object (Vect ar Constant)) $ traverse getConst args of
    Right args' => case getOp {vars=[]} fn (NPrimVal EmptyFC <$> args') of
        Just (NPrimVal _ res) => pure $ Const res
        _ => interpError stk $ "OP: Error calling " ++ show (opName fn) ++ " with operands: " ++ show args'
    Left obj => interpError stk $ "OP: Expected Constant, found " ++ showType obj
  where
    getConst : Object -> Either Object Constant
    getConst (Const c) = Right c
    getConst o = Left o

NS_UN : Namespace -> String -> Name
NS_UN ns un = NS ns (UN $ Basic un)

argError : Ref State InterpState => Stack -> Vect h Object -> Core a
argError stk obj = interpError stk $ "Unexpected arguments: " ++ foldMap ((" " ++) . showType) obj

unit : Object
unit = Const (I 0)

ioRes : Object -> Object
ioRes obj = Constructor (Left 0) [Const WorldVal, obj]

-- TODO: add more?
knownForeign : NameMap (ar ** (Ref State InterpState => Stack -> Vect ar Object -> Core Object))
knownForeign = fromList
    [ (NS_UN ioNS "prim__putChar", (2 ** prim_putChar))
    , (NS_UN ioNS "prim__getChar", (1 ** prim_getChar))
    , (NS_UN ioNS "prim__getStr", (1 ** prim_getStr))
    , (NS_UN ioNS "prim__putStr", (2 ** prim_putStr))
    ]
  where
    prim_putChar : Ref State InterpState => Stack -> Vect 2 Object -> Core Object
    prim_putChar _ [Const (Ch c), Const WorldVal] = ioRes unit <$ coreLift_ (putChar c)
    prim_putChar stk as = argError stk as
    prim_getChar : Ref State InterpState => Stack -> Vect 1 Object -> Core Object
    prim_getChar _ [Const WorldVal] = ioRes . Const . Ch <$> coreLift getChar
    prim_getChar stk as = argError stk as
    prim_getStr : Ref State InterpState => Stack -> Vect 1 Object -> Core Object
    prim_getStr _ [Const WorldVal] = Const . Str <$> coreLift getLine
    prim_getStr stk as = argError stk as
    prim_putStr : Ref State InterpState => Stack -> Vect 2 Object -> Core Object
    prim_putStr _ [Const (Str s), Const WorldVal] = ioRes unit <$ coreLift_ (putStr s)
    prim_putStr stk as = argError stk as

knownExtern : NameMap (ar ** (Ref State InterpState => Stack -> Vect ar Object -> Core Object))
knownExtern = empty

beginFunction : Ref State InterpState => List (Int, Object) -> List VMInst -> Int -> Core (List VMInst)
beginFunction args (DECLARE (Loc i) :: is) maxLoc = beginFunction args is (Prelude.max i maxLoc)
beginFunction args (DECLARE _ :: is) maxLoc = beginFunction args is maxLoc
beginFunction args (START :: is) maxLoc = do
    locals <- coreLift $ newArray (maxLoc + 1)
    ignore $ traverse (\(idx, arg) => coreLift $ writeArray locals idx arg) args
    update State $ record { locals = locals, returnObj = Nothing }
    pure is
beginFunction args is maxLoc = pure is

parameters {auto c : Ref Ctxt Defs}
  mutual
    step : Stack -> Ref State InterpState => VMInst -> Core ()
    step stk (DECLARE _) = pure ()
    step stk START = pure ()
    step stk (ASSIGN target val) = do
        valObj <- getReg stk val
        setReg stk target valObj
    step stk (MKCON target tag args) = do
        argObjs <- traverse (getReg stk) args
        setReg stk target $ Constructor tag argObjs
    step stk (MKCLOSURE target fn missing args) = do
        argObjs <- traverse (getReg stk) args
        setReg stk target $ Closure (pred missing) ([<] <>< argObjs) fn
    step stk (MKCONSTANT target c) = setReg stk target $ Const c
    step stk (APPLY target fn arg) = do
        fnObj <- getReg stk fn
        argObj <- getReg stk arg
        case fnObj of
            Closure Z args fn => do
                res <- callFunc stk fn (args <>> [argObj])
                setReg stk target res
            Closure (S k) args fn => setReg stk target $ Closure k (args :< argObj) fn
            obj => interpError stk $ "APPLY: While applying " ++ show fn ++ ", expected closure, found: " ++ show obj
    step stk (CALL target _ fn args) = do
        argObjs <- traverse (getReg stk) args
        res <- callFunc stk fn argObjs
        setReg stk target res
    step stk (OP target fn args) = do
        argObjs <- traverseVect (getReg stk) args
        res <- callPrim stk fn argObjs
        setReg stk target res
    step stk (EXTPRIM target fn args) = case lookup fn knownExtern of
        Nothing => interpError stk $ "EXTPRIM: Unkown foreign function: " ++ show fn
        Just (ar ** op) => case toVect ar args of
            Nothing => interpError stk $ "EXTPRIM: Wrong number of arguments, found: " ++ show (length args) ++ ", expected: " ++ show ar
            Just argsVect => do
                argObjs <- traverseVect (getReg stk) argsVect
                res <- op stk argObjs
                setReg stk target res
    step stk (CASE sc alts def) = do
        scObj <- getReg stk sc
        case scObj of
            Constructor tag _ => matchCon stk tag alts def
            _ => interpError stk $ "CASE: Expected Constructor, found " ++ showType scObj
      where
        matchCon : Stack -> Either Int Name -> List (Either Int Name, List VMInst) -> Maybe (List VMInst) -> Core ()
        matchCon stk tag [] Nothing = interpError stk "CASE: Missing matching alternative or default"
        matchCon stk tag [] (Just is) = traverse_ (step stk) is
        matchCon stk tag ((t, is) :: alts) def =
            if tag == t
                then traverse_ (step stk) is
                else matchCon stk tag alts def
    step stk (CONSTCASE sc alts def) = do
        scObj <- getReg stk sc
        case scObj of
            Const c => matchConst stk c alts def
            _ => interpError stk $ "CONSTCASE: Expected Constant, found " ++ showType scObj
      where
        matchConst : Stack -> Constant -> List (Constant, List VMInst) -> Maybe (List VMInst) -> Core ()
        matchConst stk c [] Nothing = interpError stk "CONSTCASE: Missing matching alternative or default"
        matchConst stk c [] (Just is) = traverse_ (step stk) is
        matchConst stk c ((c', is) :: alts) def =
            if c == c'
                then traverse_ (step stk) is
                else matchConst stk c alts def
    step stk (PROJECT target val idx) = do
        valObj <- getReg stk val
        case valObj of
            Constructor _ args => case indexMaybe args idx of
                Nothing => interpError stk
                    $ "PROJECT: Unable to project index " ++ show idx
                    ++ ", missing arguments for constructor:\n" ++ show valObj
                Just arg => setReg stk target arg
            _ => interpError stk $ "PROJECT: Expected Constructor, found " ++ showType valObj
    step stk (NULL reg) = setReg stk reg Null
    step stk (ERROR msg) = interpError stk $ "ERROR: " ++ msg

    callFunc : Ref State InterpState => Stack -> Name -> List Object -> Core Object
    callFunc stk fn args = saveLocals $ do
        let ind = pack $ '|' <$ stk
        logCallStack <- logging "compiler.interpreter" 25
        when logCallStack $ coreLift $ putStrLn $ ind ++ "Calling " ++ show fn ++ " with args: " ++ show args
        let stk' = fn :: stk
        defs <- defs <$> get State
        res <- case lookup fn defs of
            Nothing => interpError stk $ "Undefined function: " ++ show fn
            Just (MkVMFun as is) => do
                when (length as /= length args) $ interpError stk
                    $ "Unexpected argument count during function call, expected: "
                    ++ show (length as) ++ ", found: " ++ show (length args)
                is' <- beginFunction (zip as args) is (foldl max (-1) as)
                traverse_ (step stk') is'
                getReg stk' RVal
            Just (MkVMForeign _ _ _) => case lookup fn knownForeign of
                Nothing => interpError stk $ "Unkown foreign function: " ++ show fn
                Just (ar ** op) => case toVect ar args of
                    Nothing => interpError stk $ "Wrong number of arguments, found: " ++ show (length args) ++ ", expected: " ++ show ar
                    Just argsVect => op stk argsVect
            Just (MkVMError is) => do
                traverse_ (step stk') is
                getReg stk' RVal
        when logCallStack $ coreLift $ putStrLn $ ind ++ "Result: " ++ show res
        pure res

compileExpr : Ref Ctxt Defs -> String -> String -> ClosedTerm -> String -> Core (Maybe String)
compileExpr _ _ _ _ _ = Nothing <$ throw {a=()} (InternalError "compile not implemeted for vmcode-interp")

executeExpr : Ref Ctxt Defs -> String -> ClosedTerm -> Core ()
executeExpr c _ tm = do
    cdata <- getCompileData False VMCode tm
    st <- newRef State !(initInterpState cdata.vmcode)
    ignore $ callFunc [] (MN "__mainExpression" 0) []

export
codegenVMCodeInterp : Codegen
codegenVMCodeInterp = MkCG compileExpr executeExpr Nothing Nothing


text:
-- Idris 0.9.20
module Main

import data.Vect
import Data.List

%default total

-- Aliases

Queen : Type
Queen = (Nat, Nat)

IsValid : Type
IsValid = Bool

Valid : IsValid
Valid = True

Invalid : IsValid
Invalid = False

Boardsize : Type
Boardsize = Nat

Queens : Nat -> Type
Queens n = Vect n Queen

-- Helper methods

forAllPairsWithList : List a -> a -> (a -> a -> Bool) -> Bool
forAllPairsWithList [] element p = True
forAllPairsWithList (x :: xs) element p = if p element x then forAllPairsWithList xs element p else False

forAllPairsInList : List a -> (a -> a -> Bool) -> Bool
forAllPairsInList [] p = True
forAllPairsInList (x :: xs) p = (forAllPairsWithList xs x p) && forAllPairsInList xs p

-- NQueens

isValidNQueens : {n : Boardsize} -> Queens n -> IsValid
isValidNQueens {n=boardsize} queens =
  let
    queenList = toList queens
    isAllOnBoard = all (isOnBoard boardsize) queenList
    isAllDifferentRows = forAllPairsInList queenList isDifferentRows
    isAllDifferentCols = forAllPairsInList queenList isDifferentCols
    isAllDifferentDiags = forAllPairsInList queenList isDifferentDiags
  in
    isAllOnBoard && isAllDifferentRows && isAllDifferentCols && isAllDifferentDiags
  where
    isOnBoard : Boardsize -> Queen -> Bool
    isOnBoard boardsize (a, b) = a < boardsize && b < boardsize

    isDifferentRows : Queen -> Queen -> Bool
    isDifferentRows (a1, a2) (b1, b2) = a1 /= b1

    isDifferentCols : Queen -> Queen -> Bool
    isDifferentCols (a1, a2) (b1, b2) = a2 /= b2

    -- False if they're on the same diagonale looking from 0/0 to n/n; True otherwise
    isDifferentDiags1 : Queen -> Queen -> Bool
    isDifferentDiags1 ((S a1), (S a2)) b = assert_total (isDifferentDiags1 (a1, a2) b) -- meh
    isDifferentDiags1 a ((S b1), (S b2)) = assert_total (isDifferentDiags1 a (b1, b2)) -- meh
    isDifferentDiags1 (a1, a2) (b1, b2) = if (a1 == b1 && a2 == b2) then False else True

    -- False if they're on the same diagonale looking from 0/n to n/0; True otherwise
    isDifferentDiags2 : Queen -> Queen -> Bool
    isDifferentDiags2 ((S a1), a2) (b1, (S b2)) = assert_total (isDifferentDiags2 (a1, a2) (b1, b2)) -- meh
    isDifferentDiags2 (a1, (S a2)) ((S b1), b2) = assert_total (isDifferentDiags2 (a1, a2) (b1, b2)) -- meh
    isDifferentDiags2 (a1, a2) (b1, b2) = if (a1 == b1 && a2 == b2) then False else True

    isDifferentDiags : Queen -> Queen -> Bool
    isDifferentDiags a b = (isDifferentDiags1 a b) && (isDifferentDiags2 a b)

data NQueens : Boardsize -> IsValid -> Type where
  MkNQueens : (queens : Queens n) -> NQueens n (isValidNQueens queens)
  MkInvalidNQueens : (n : Nat) -> NQueens n Invalid

instance Show (NQueens n isValid) where
  show (MkNQueens queens) =
    if (isValidNQueens queens) then -- meh
      (show (length queens)) ++ "-Queens " ++ (show queens)
    else
      "Invalid " ++ (show (length queens)) ++ "-Queens"
  show (MkInvalidNQueens n) = "Invalid " ++ (show n) ++ "-Queens"

-- (Compile) Tests

queen1 : Queen
queen1 = (3, 2)

queen2 : Queen
queen2 = (2, 0)

queen3 : Queen
queen3 = (1, 3)

queen4 : Queen
queen4 = (0, 1)

nQueens1 : NQueens 1 Valid
nQueens1 = MkNQueens [(0, 0)]

invalidNQueens1 : NQueens 1 Invalid
invalidNQueens1 = MkInvalidNQueens _

nQueens4 : NQueens 4 Valid
nQueens4 = MkNQueens [queen1, queen2, queen3, queen4]

invalidNQueens4 : NQueens 4 Invalid
invalidNQueens4 = MkNQueens [queen1, (3, 3), queen3, queen4]

invalidNQueens4b : NQueens 4 Invalid
invalidNQueens4b = MkNQueens [(2, 2), (3, 0), queen3, queen4]

---- Does not compile! :-)
--invalidNQueens1Error : NQueens 1 Invalid
--invalidNQueens1Error = MkNQueens [(0, 0)]

--invalidNQueens2Error : NQueens 2 Valid -- Does not even compile as Invalid!
--invalidNQueens2Error = MkNQueens [(0, 0)]

--invalidNQueens4Error : NQueens 4 Valid
--invalidNQueens4Error = MkNQueens [queen1, (3, 3), queen3, queen4]

max_stars_repo_name: ExNexu/nqueens-idris

max_issues_repo_name: ExNexu/nqueens-idris

max_forks_repo_name: ExNexu/nqueens-idris


text:
module Door

-- Adapted from:
-- https://github.com/idris-lang/Idris2/blob/523c0a6d7823d2b9a614d4a30efb52da015f9367/tests/typedd-book/chapter14/DoorJam.idr

import Control.Monad.TransitionIndexed
import Control.Monad.TransitionIndexed.Do

data DoorState = DoorClosed | DoorOpen

data DoorResult = OK | Jammed

data DoorCmd : (ty : Type) ->
               DoorState ->
               (ty -> DoorState) ->
               Type where
  Open :     DoorCmd DoorResult DoorClosed (\res => case res of
                                                         OK => DoorOpen
                                                         Jammed => DoorClosed)
  Close :    DoorCmd ()         DoorOpen   (const DoorClosed)
  RingBell : DoorCmd ()         DoorClosed (const DoorClosed)

  Display : String -> DoorCmd () state (const state)

  Pure : (res : ty) -> DoorCmd ty (state_fn res) state_fn
  Bind : DoorCmd a state1 state2_fn ->
          ((res: a) -> DoorCmd b (state2_fn res) state3_fn) ->
          DoorCmd b state1 state3_fn

TransitionIndexedPointed DoorState DoorCmd where
  pure = Pure

TransitionIndexedMonad DoorState DoorCmd where
  bind = Bind

logOpen : DoorCmd DoorResult DoorClosed
                             (\res => case res of
                                           OK => DoorOpen
                                           Jammed => DoorClosed)
logOpen = do Display "Trying to open the door"
             OK <- Open | Jammed => do Display "Jammed"
                                       Pure Jammed
             Display "Success"
             Pure OK

doorProg : DoorCmd () DoorClosed (const DoorClosed)
doorProg = do RingBell
              jam <- Open
              Display "Trying to open the door"
              case jam of
                   OK => do Display "Glad To Be Of Service"
                            Close
                   Jammed => Display "Door Jammed"

doorProg2 : DoorCmd () DoorClosed (const DoorClosed)
doorProg2 = do RingBell
               OK <- Open | Jammed => Display "Door Jammed"
               Display "Glad To Be Of Service"
               Close
               OK <- Open | Jammed => Display "Door Jammed"
               Display "Glad To Be Of Service"
               Close

doorProg3 : (diagnostic : Bool) -> DoorCmd () DoorClosed (const DoorClosed)
doorProg3 diagnostic =
  do RingBell
     OK <- Open
       | Jammed => do Display "Door Jammed"
                      when diagnostic $
                        Display "debug: after first ring of bell."
     unless diagnostic $
       Display "Glad To Be Of Service"
     Close

max_stars_repo_name: mattpolzin/idris-indexed

max_issues_repo_name: mattpolzin/idris-indexed

max_forks_repo_name: mattpolzin/idris-indexed


text:
module Effect.Select

import Effects

data Selection : Effect where
     Select : List a -> { () } Selection a

instance Handler Selection Maybe where
     handle _ (Select xs) k = tryAll xs where
         tryAll [] = Nothing
         tryAll (x :: xs) = case k x () of
                                 Nothing => tryAll xs
                                 Just v => Just v

instance Handler Selection List where
     handle r (Select xs) k = concatMap (\x => k x r) xs

SELECT : EFFECT
SELECT = MkEff () Selection

select : List a -> { [SELECT] } Eff m a
select xs = Select xs

max_stars_repo_name: edwinb/Eff-new

max_issues_repo_name: edwinb/Eff-new

max_forks_repo_name: edwinb/Eff-new


text:
data Expr num = Val num
              | Add (Expr num) (Expr num)
              | Sub (Expr num) (Expr num)
              | Mul (Expr num) (Expr num)
              | Div (Expr num) (Expr num)
              | Abs (Expr num)

eval : (Neg num, Integral num) => Expr num -> num
eval (Val x) = x
eval (Add x y) = eval x + eval y
eval (Sub x y) = eval x - eval y
eval (Mul x y) = eval x * eval y
eval (Div x y) = eval x `div` eval y
eval (Abs x) = abs (eval x)

Num ty => Num (Expr ty) where
    (+) = Add
    (*) = Mul
    fromInteger = Val . fromInteger

Neg ty => Neg (Expr ty) where
    negate x = 0 - x
    (-) = Sub
    abs = Abs

max_stars_repo_name: PiotrJander/TypeDD-Samples

max_issues_repo_name: gdevanla/TypeDD-Samples

max_forks_repo_name: gdevanla/TypeDD-Samples


text:
-- | Exercises on Boolean Relations.
module Koans.Boolean

logicalAND : Bool
logicalAND = True && True == True

logicalOR : Bool
logicalOR = False || False == False

logicalNOT : Bool
logicalNOT = not True == False

logicalPredicate : Bool
logicalPredicate = not (False && True) || (True && False) == True

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

max_stars_repo_name: harrisi/on-being-better

max_issues_repo_name: harrisi/on-being-better

max_forks_repo_name: harrisi/on-being-better


text:
module Issue710a

record r where
  constructor MkR


text:
module Ch04.SubTerm

import Ch03.Arith

||| Propositional type describing that one term is an direct subterm of another one.
data DirectSubTerm : Term -> Term -> Type where
  IsIfTerm : (x : Term) -> DirectSubTerm x (IfThenElse x y z)
  IsThenTerm : (y : Term) -> DirectSubTerm y (IfThenElse x y z)
  IsElseTerm : (z : Term) -> DirectSubTerm z (IfThenElse x y z)
  IsSuccSubTerm : (x : Term) -> DirectSubTerm x (Succ x)
  IsPredSubTerm : (x : Term) -> DirectSubTerm x (Pred x)

||| Propositional type describing that one term is a subterm of another one.
data SubTerm : Term -> Term -> Type where
  IsSubTermOfDirectSubTerm : SubTerm x y -> DirectSubTerm y z -> SubTerm x z
  IsEqual : SubTerm x x

max_stars_repo_name: mr-infty/tapl

max_issues_repo_name: mr-infty/tapl

max_forks_repo_name: mr-infty/tapl


text:
||| More functions and properties for relative numbers
||| Re-exports all of `Data.ZZ` from contrib for convenience
module Data.ZZ.Extra

import Data.Nat
import Data.Sign
import public Data.ZZ

%default total

||| Proof that if the absolute value of a number is 0, then this number is 0
||| @y: a relative number which we take absolute value of
public export
absZIsPosZ : {y : ZZ } -> (absZ y = 0) -> (y = Pos 0)
absZIsPosZ {y = (Pos Z)}     Refl = Refl
absZIsPosZ {y = (Pos (S _))} Refl impossible
absZIsPosZ {y = (NegS _)}    Refl impossible

public export
contrapositive : (a -> b) -> (Not b -> Not a)
contrapositive = flip (.)

||| Proof that if a number is not 0, its absolute value is not 0
||| This is the contrapositive proof to `absZIsPosZ`
||| @y: a Relative number which is not 0
public export
notPosZIsNotAbsZ : {y : ZZ } -> ((y = Pos 0) -> Void) -> ((absZ y = 0) -> Void)
notPosZIsNotAbsZ = contrapositive absZIsPosZ

public export
divNatNZ' : Nat -> (y: Nat) -> { prf : Not (y = Z) } -> Nat
divNatNZ' left Z         {prf} = void (prf Refl)
divNatNZ' left (S right) = div' left left right
  where
    div' : Nat -> Nat -> Nat -> Nat
    div' Z        centre right = Z
    div' (S left) centre right =
      if lte centre right then
        Z
      else
        S (div' left (minus centre (S right)) right)

||| Euclidean division of 2 `ZZ` numbers ensuring divisor is not 0
||| We compute using `Nat`'s division and checking the `multiply` of the signs
||| of both numbers, observing that if the sign is  `Zero` then this implis `x`
||| is 0 and thus the result is 0.
|||
||| @x: dividend of euclidean division
||| @y: divisor of euclidean division
||| @divisorNotZ: a proof the divisor is not null
public export
divZZNZ : (x : ZZ) -> (y : ZZ) -> {z : Not (y = Pos Z) } -> ZZ
divZZNZ x (Pos Z) {z} = absurd (z Refl)
divZZNZ x y {z} with (sign x `multiply` sign y)
  divZZNZ x y {z} | Zero = Pos Z
  divZZNZ x y {z} | Plus = Pos $ divNatNZ' (absZ x) (absZ y) { prf = notPosZIsNotAbsZ z }
  divZZNZ x y {z} | Minus = NegS $ divNatNZ' (absZ x) (absZ y) { prf = notPosZIsNotAbsZ  z }

||| A strictly Positive `ZZ` is not 0
public export
PosSIsNotZ : Not (Pos (S k) = Pos 0)
PosSIsNotZ Refl impossible

||| A negative `ZZ` is not 0
public export
NegSIsNotZ : Not (NegS (S k) = Pos 0)
NegSIsNotZ Refl impossible

max_stars_repo_name: steshaw/hsgames

max_issues_repo_name: steshaw/hsgames

max_forks_repo_name: steshaw/hsgames


text:
module Sub05LTE216t225

import ProofColDivSeqBase
import ProofColDivSeqPostulate

%default total

-- 6(36t+37)+3 --FE[5,0,-4]--> 6(8t+7)+3
export
lte216t225 : (m : Nat) -> LTE (S (S (S (S (S (S (S (S (m+m+m+m)+(m+m+m+m)))))))))
  (S (((S (S ((S (S (m+m+m)))+(S (S (m+m+m))))))+(S (S ((S (S (m+m+m)))+(S (S (m+m+m))))))) + ((S (S ((S (S (m+m+m)))+(S (S (m+m+m))))))+(S (S ((S (S (m+m+m)))+(S (S (m+m+m))))))) + ((S (S ((S (S (m+m+m)))+(S (S (m+m+m))))))+(S (S ((S (S (m+m+m)))+(S (S (m+m+m)))))))))
lte216t225 Z     = (lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc) LTEZero
lte216t225 (S m) =
  let lemma = lte216t225 m in

  rewrite (sym (plusSuccRightSucc m m)) in

  rewrite (sym (plusSuccRightSucc (plus m m) m)) in

  rewrite (sym (plusSuccRightSucc (plus (plus m m) m) m)) in

  rewrite (sym (plusSuccRightSucc (plus (plus (plus m m) m) m)
                                  (S (S (S (plus (plus (plus m m) m) m)))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus m m) m) m)
                                     (S (S (plus (plus (plus m m) m) m))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus m m) m) m)
                                        (S (plus (plus (plus m m) m) m)))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus m m) m) m)
                                           (plus (plus (plus m m) m) m))) in

  rewrite (sym (plusSuccRightSucc (plus (plus m m) m) (S (S (S (S (plus (plus m m) m))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus m m) m)    (S (S (S (plus (plus m m) m)))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus m m) m)       (S (S (plus (plus m m) m))))) in

  rewrite (sym (plusSuccRightSucc (plus (plus (plus m m) m) (S (S (plus (plus m m) m))))
                  (S (S (S (S (S (S (S (S (S (plus (plus (plus m m) m) (S (S (plus (plus m m) m))))))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus m m) m) (S (S (plus (plus m m) m))))
                     (S (S (S (S (S (S (S (S (plus (plus (plus m m) m) (S (S (plus (plus m m) m)))))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus m m) m) (S (S (plus (plus m m) m))))
                        (S (S (S (S (S (S (S (plus (plus (plus m m) m) (S (S (plus (plus m m) m))))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus m m) m) (S (S (plus (plus m m) m))))
                           (S (S (S (S (S (S (plus (plus (plus m m) m) (S (S (plus (plus m m) m)))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus m m) m) (S (S (plus (plus m m) m))))
                              (S (S (S (S (S (plus (plus (plus m m) m) (S (S (plus (plus m m) m))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus m m) m) (S (S (plus (plus m m) m))))
                                 (S (S (S (S (plus (plus (plus m m) m) (S (S (plus (plus m m) m)))))))))) in

  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus m m) m) (S (S (plus (plus m m) m))))
                        (S (S (S (S (plus (plus (plus m m) m) (S (S (plus (plus m m) m)))))))))
                  (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus m m) m)
                                                                              (S (S (plus (plus m m) m))))
                                                                        (S (S (S (S (plus (plus (plus m m) m)
                                                                                (S (S (plus (plus m m)
                                m)))))))))))))))))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus m m) m) (S (S (plus (plus m m) m))))
                        (S (S (S (S (plus (plus (plus m m) m) (S (S (plus (plus m m) m)))))))))
                     (S (S (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus m m) m)
                                                                              (S (S (plus (plus m m) m))))
                                                                        (S (S (S (S (plus (plus (plus m m) m)
                                                                                (S (S (plus (plus m m)
                                m))))))))))))))))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus m m) m) (S (S (plus (plus m m) m))))
                        (S (S (S (S (plus (plus (plus m m) m) (S (S (plus (plus m m) m)))))))))
                        (S (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus m m) m)
                                                                              (S (S (plus (plus m m) m))))
                                                                        (S (S (S (S (plus (plus (plus m m) m)
                                                                                (S (S (plus (plus m m)
                                m)))))))))))))))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus m m) m) (S (S (plus (plus m m) m))))
                        (S (S (S (S (plus (plus (plus m m) m) (S (S (plus (plus m m) m)))))))))
                           (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus m m) m)
                                                                              (S (S (plus (plus m m) m))))
                                                                        (S (S (S (S (plus (plus (plus m m) m)
                                                                                (S (S (plus (plus m m)
                                m))))))))))))))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus m m) m) (S (S (plus (plus m m) m))))
                        (S (S (S (S (plus (plus (plus m m) m) (S (S (plus (plus m m) m)))))))))
                              (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus m m) m)
                                                                              (S (S (plus (plus m m) m))))
                                                                        (S (S (S (S (plus (plus (plus m m) m)
                                                                                (S (S (plus (plus m m)
                                m)))))))))))))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus m m) m) (S (S (plus (plus m m) m))))
                        (S (S (S (S (plus (plus (plus m m) m) (S (S (plus (plus m m) m)))))))))
                                 (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus m m) m)
                                                                              (S (S (plus (plus m m) m))))
                                                                        (S (S (S (S (plus (plus (plus m m) m)
                                                                                (S (S (plus (plus m m)
                                m))))))))))))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus m m) m) (S (S (plus (plus m m) m))))
                        (S (S (S (S (plus (plus (plus m m) m) (S (S (plus (plus m m) m)))))))))
                                    (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus m m) m)
                                                                              (S (S (plus (plus m m) m))))
                                                                        (S (S (S (S (plus (plus (plus m m) m)
                                                                                (S (S (plus (plus m m)
                                m)))))))))))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus m m) m) (S (S (plus (plus m m) m))))
                        (S (S (S (S (plus (plus (plus m m) m) (S (S (plus (plus m m) m)))))))))
                                       (S (S (S (S (S (S (S (S (plus (plus (plus (plus m m) m)
                                                                              (S (S (plus (plus m m) m))))
                                                                        (S (S (S (S (plus (plus (plus m m) m)
                                                                                (S (S (plus (plus m m)
                                m))))))))))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus m m) m) (S (S (plus (plus m m) m))))
                        (S (S (S (S (plus (plus (plus m m) m) (S (S (plus (plus m m) m)))))))))
                                          (S (S (S (S (S (S (S (plus (plus (plus (plus m m) m)
                                                                              (S (S (plus (plus m m) m))))
                                                                        (S (S (S (S (plus (plus (plus m m) m)
                                                                                (S (S (plus (plus m m)
                                m)))))))))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus m m) m) (S (S (plus (plus m m) m))))
                        (S (S (S (S (plus (plus (plus m m) m) (S (S (plus (plus m m) m)))))))))
                                             (S (S (S (S (S (S (plus (plus (plus (plus m m) m)
                                                                              (S (S (plus (plus m m) m))))
                                                                        (S (S (S (S (plus (plus (plus m m) m)
                                                                                (S (S (plus (plus m m)
                                m))))))))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus m m) m) (S (S (plus (plus m m) m))))
                        (S (S (S (S (plus (plus (plus m m) m) (S (S (plus (plus m m) m)))))))))
                                                (S (S (S (S (S (plus (plus (plus (plus m m) m)
                                                                              (S (S (plus (plus m m) m))))
                                                                        (S (S (S (S (plus (plus (plus m m) m)
                                                                                (S (S (plus (plus m m)
                                m)))))))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus m m) m) (S (S (plus (plus m m) m))))
                        (S (S (S (S (plus (plus (plus m m) m) (S (S (plus (plus m m) m)))))))))
                                                   (S (S (S (S (plus (plus (plus (plus m m) m)
                                                                              (S (S (plus (plus m m) m))))
                                                                        (S (S (S (S (plus (plus (plus m m) m)
                                                                                (S (S (plus (plus m m)
                                m))))))))))))))) in

  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus m m) m)
                                    (S (S (plus (plus m m) m))))
                              (S (S (S (S (plus (plus (plus m m) m)
                                                (S (S (plus (plus m m) m)))))))))
                        (S (S (S (S (plus (plus (plus (plus m m) m)
                                                (S (S (plus (plus m m) m))))
                                          (S (S (S (S (plus (plus (plus m m) m)
                                                            (S (S (plus (plus m m)
                                                                        m))))))))))))))
                  (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus m m) m)
                           (S (S (plus (plus m m) m))))
                           (S (S (S (S (plus (plus (plus m m) m)
                           (S (S (plus (plus m m)
                   m)))))))))))))))))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus m m) m)
                                    (S (S (plus (plus m m) m))))
                              (S (S (S (S (plus (plus (plus m m) m)
                                                (S (S (plus (plus m m) m)))))))))
                        (S (S (S (S (plus (plus (plus (plus m m) m)
                                                (S (S (plus (plus m m) m))))
                                          (S (S (S (S (plus (plus (plus m m) m)
                                                            (S (S (plus (plus m m)
                                                                        m))))))))))))))
                     (S (S (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus m m) m)
                           (S (S (plus (plus m m) m))))
                           (S (S (S (S (plus (plus (plus m m) m)
                           (S (S (plus (plus m m)
                   m))))))))))))))))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus m m) m)
                                    (S (S (plus (plus m m) m))))
                              (S (S (S (S (plus (plus (plus m m) m)
                                                (S (S (plus (plus m m) m)))))))))
                        (S (S (S (S (plus (plus (plus (plus m m) m)
                                                (S (S (plus (plus m m) m))))
                                          (S (S (S (S (plus (plus (plus m m) m)
                                                            (S (S (plus (plus m m)
                                                                        m))))))))))))))
                        (S (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus m m) m)
                           (S (S (plus (plus m m) m))))
                           (S (S (S (S (plus (plus (plus m m) m)
                           (S (S (plus (plus m m)
                   m)))))))))))))))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus m m) m)
                                    (S (S (plus (plus m m) m))))
                              (S (S (S (S (plus (plus (plus m m) m)
                                                (S (S (plus (plus m m) m)))))))))
                        (S (S (S (S (plus (plus (plus (plus m m) m)
                                                (S (S (plus (plus m m) m))))
                                          (S (S (S (S (plus (plus (plus m m) m)
                                                            (S (S (plus (plus m m)
                                                                        m))))))))))))))
                           (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus m m) m)
                           (S (S (plus (plus m m) m))))
                           (S (S (S (S (plus (plus (plus m m) m)
                           (S (S (plus (plus m m)
                   m))))))))))))))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus m m) m)
                                    (S (S (plus (plus m m) m))))
                              (S (S (S (S (plus (plus (plus m m) m)
                                                (S (S (plus (plus m m) m)))))))))
                        (S (S (S (S (plus (plus (plus (plus m m) m)
                                                (S (S (plus (plus m m) m))))
                                          (S (S (S (S (plus (plus (plus m m) m)
                                                            (S (S (plus (plus m m)
                                                                        m))))))))))))))
                              (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus m m) m)
                           (S (S (plus (plus m m) m))))
                           (S (S (S (S (plus (plus (plus m m) m)
                           (S (S (plus (plus m m)
                   m)))))))))))))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus m m) m)
                                    (S (S (plus (plus m m) m))))
                              (S (S (S (S (plus (plus (plus m m) m)
                                                (S (S (plus (plus m m) m)))))))))
                        (S (S (S (S (plus (plus (plus (plus m m) m)
                                                (S (S (plus (plus m m) m))))
                                          (S (S (S (S (plus (plus (plus m m) m)
                                                            (S (S (plus (plus m m)
                                                                        m))))))))))))))
                                 (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus m m) m)
                           (S (S (plus (plus m m) m))))
                           (S (S (S (S (plus (plus (plus m m) m)
                           (S (S (plus (plus m m)
                   m))))))))))))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus m m) m)
                                    (S (S (plus (plus m m) m))))
                              (S (S (S (S (plus (plus (plus m m) m)
                                                (S (S (plus (plus m m) m)))))))))
                        (S (S (S (S (plus (plus (plus (plus m m) m)
                                                (S (S (plus (plus m m) m))))
                                          (S (S (S (S (plus (plus (plus m m) m)
                                                            (S (S (plus (plus m m)
                                                                        m))))))))))))))
                                    (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus m m) m)
                           (S (S (plus (plus m m) m))))
                           (S (S (S (S (plus (plus (plus m m) m)
                           (S (S (plus (plus m m)
                   m)))))))))))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus m m) m)
                                    (S (S (plus (plus m m) m))))
                              (S (S (S (S (plus (plus (plus m m) m)
                                                (S (S (plus (plus m m) m)))))))))
                        (S (S (S (S (plus (plus (plus (plus m m) m)
                                                (S (S (plus (plus m m) m))))
                                          (S (S (S (S (plus (plus (plus m m) m)
                                                            (S (S (plus (plus m m)
                                                                        m))))))))))))))
                                       (S (S (S (S (S (S (S (S (plus (plus (plus (plus m m) m)
                           (S (S (plus (plus m m) m))))
                           (S (S (S (S (plus (plus (plus m m) m)
                           (S (S (plus (plus m m)
                   m))))))))))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus m m) m)
                                    (S (S (plus (plus m m) m))))
                              (S (S (S (S (plus (plus (plus m m) m)
                                                (S (S (plus (plus m m) m)))))))))
                        (S (S (S (S (plus (plus (plus (plus m m) m)
                                                (S (S (plus (plus m m) m))))
                                          (S (S (S (S (plus (plus (plus m m) m)
                                                            (S (S (plus (plus m m)
                                                                        m))))))))))))))
                                          (S (S (S (S (S (S (S (plus (plus (plus (plus m m) m)
                           (S (S (plus (plus m m) m))))
                           (S (S (S (S (plus (plus (plus m m) m)
                           (S (S (plus (plus m m)
                   m)))))))))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus m m) m)
                                    (S (S (plus (plus m m) m))))
                              (S (S (S (S (plus (plus (plus m m) m)
                                                (S (S (plus (plus m m) m)))))))))
                        (S (S (S (S (plus (plus (plus (plus m m) m)
                                                (S (S (plus (plus m m) m))))
                                          (S (S (S (S (plus (plus (plus m m) m)
                                                            (S (S (plus (plus m m)
                                                                        m))))))))))))))
                                             (S (S (S (S (S (S (plus (plus (plus (plus m m) m)
                           (S (S (plus (plus m m) m))))
                           (S (S (S (S (plus (plus (plus m m) m)
                           (S (S (plus (plus m m)
                   m))))))))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus m m) m)
                                    (S (S (plus (plus m m) m))))
                              (S (S (S (S (plus (plus (plus m m) m)
                                                (S (S (plus (plus m m) m)))))))))
                        (S (S (S (S (plus (plus (plus (plus m m) m)
                                                (S (S (plus (plus m m) m))))
                                          (S (S (S (S (plus (plus (plus m m) m)
                                                            (S (S (plus (plus m m)
                                                                        m))))))))))))))
                                                (S (S (S (S (S (plus (plus (plus (plus m m) m)
                           (S (S (plus (plus m m) m))))
                           (S (S (S (S (plus (plus (plus m m) m)
                           (S (S (plus (plus m m)
                   m)))))))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus m m) m)
                                    (S (S (plus (plus m m) m))))
                              (S (S (S (S (plus (plus (plus m m) m)
                                                (S (S (plus (plus m m) m)))))))))
                        (S (S (S (S (plus (plus (plus (plus m m) m)
                                                (S (S (plus (plus m m) m))))
                                          (S (S (S (S (plus (plus (plus m m) m)
                                                            (S (S (plus (plus m m)
                                                                        m))))))))))))))
                                                   (S (S (S (S (plus (plus (plus (plus m m) m)
                           (S (S (plus (plus m m) m))))
                           (S (S (S (S (plus (plus (plus m m) m)
                           (S (S (plus (plus m m)
                   m))))))))))))))) in

    (lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc) lemma


text:
module Poly

%access public export

%default total

repeat : (x : x_ty) -> (count : Nat) -> List x_ty
repeat x Z = []
repeat x (S k) = x :: repeat x k

test_repeat1 : repeat 4 2 = [4, 4]
test_repeat1 = Refl

test_repeat2 : repeat False 1 = [False]
test_repeat2 = Refl

namespace MumbleGrumble
    data Mumble : Type where
        A : Mumble
        B : Mumble -> Nat -> Mumble
        C : Mumble

    data Grumble : (x : Type) -> Type where
        D : Mumble -> Grumble x
        E : x -> Grumble x

rev : (l : List a) -> List a
rev [] = []
rev (h :: t) = (rev t) ++ [h]

test_rev1 : rev [1, 2] = [2, 1]
test_rev1 = Refl

test_rev2 : rev [True] = [True]
test_rev2 = Refl

len : (l : List a) -> Nat
len [] = Z
len (h :: t) = S (len t)

test_length1 : length [1, 2, 3] = 3
test_length1 = Refl

app_nil_r : (l : List a) -> l ++ [] = l
app_nil_r [] = Refl
app_nil_r (x :: xs) = rewrite app_nil_r xs in Refl

app_nil : (l : List a) -> [] ++ l = l
app_nil l = Refl

app_assoc : (l, m, n : List a) -> l ++ m ++ n = (l ++ m) ++ n
app_assoc [] m n = Refl
app_assoc (x :: xs) m n = rewrite app_assoc xs m n in Refl

app_length : (l1, l2 : List a) -> length (l1 ++ l2) = length l1 + length l2
app_length [] l2 = Refl
app_length (x :: xs) l2 = rewrite app_length xs l2 in Refl

rev_app_distr : (l1, l2 : List a) -> rev (l1 ++ l2) = rev l2 ++ rev l1
rev_app_distr [] l2 = rewrite app_nil_r (rev l2) in Refl
rev_app_distr (x :: xs) l2 =
    rewrite rev_app_distr xs l2 in
        rewrite sym $ app_assoc (rev l2) (rev xs) [x] in
            Refl

rev_involutive : (l : List a) -> rev (rev l) = l
rev_involutive [] = Refl
rev_involutive (x :: xs) =
    rewrite rev_app_distr (rev xs) [x] in
        rewrite rev_involutive xs in
            Refl

split : (l : List (x, y)) -> (List x, List y)
split [] = ([], [])
split ((a, b) :: xs) =
    let
        (ys, zs) = split xs
    in
        (a :: ys, b :: zs)

test_split : split [(1, False), (2, False)] = ([1, 2], [False, False])
test_split = Refl

nth_error : (l : List a) -> (n : Nat) -> Maybe a
nth_error [] n = Nothing
nth_error (x :: xs) Z = Just x
nth_error (x :: xs) (S k) = nth_error xs k

test_nth_error1 : nth_error [4, 5, 6, 7] 0 = Just 4
test_nth_error1 = Refl

test_nth_error2 : nth_error [[1], [2]] 1 = Just [2]
test_nth_error2 = Refl

test_nth_error3 : nth_error [True] 2 = Nothing
test_nth_error3 = Refl

hd_error : (l : List a) -> Maybe a
hd_error [] = Nothing
hd_error (x :: xs) = Just x

test_hd_error1 : hd_error [1, 2] = Just 1
test_hd_error1 = Refl

test_hd_error2 : hd_error [[1], [2]] = Just [1]
test_hd_error2 = Refl

map_rev : (f : x -> y) -> (l : List x) -> map f (rev l) = rev (map f l)
map_rev f [] = Refl
map_rev f (x :: xs) = ?map_rev_rhs_2


text:
-- --------------------------------------------------------------- [ Model.idr ]
-- Module    : Model.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]

||| The GRL Model as  Goal Graph
module GRL.Model

import public Data.AVL.Graph
import public Data.List

import GRL.Common
import Debug.Trace

%access export

-- ------------------------------------------------------------------- [ Nodes ]

||| Nodes in the Goal Graph
public export
record GoalNode where
  constructor GNode
  getNodeTy    : GElemTy
  getNodeTitle : String
  getSValue    : Maybe SValue
  getStructTy  : Maybe GStructTy

Show GoalNode where
  show (GNode ty n s d) = with List unwords ["[GNode", show ty, n, show s, show d, "]"]

Eq GoalNode where
  (==) (GNode xty x xs xd) (GNode yty y ys yd) =
      xty == yty &&
      x   == y   &&
      xs  == ys  &&
      xd  == yd

-- ------------------------------------------------------------------- [ Edges ]

public export
data GoalEdge  : Type where
  Contribution : CValue -> GoalEdge
  Correlation  : CValue -> GoalEdge
  Decomp       : GoalEdge

Show GoalEdge where
  show (Contribution ty) = with List unwords ["[Contrib", show ty, "]"]
  show (Correlation ty)  = with List unwords ["[Correl", show ty, "]"]
  show Decomp            = with List unwords ["[Decomp]"]

Eq GoalEdge where
  (==) (Contribution x) (Contribution y) = x == y
  (==) (Correlation x)  (Correlation y)  = x == y
  (==) Decomp           Decomp           = True
  (==) _                _                = False

-- ---------------------------------------------------------------- [ Synonyms ]

public export
GModel : Type
GModel = Graph (GoalNode) (GoalEdge)

-- ---------------------------------------------------------- [ Util Functions ]

isDeCompEdge : Maybe GoalEdge -> Bool
isDeCompEdge (Just Decomp) = True
isDeCompEdge _             = False

isContribEdge : Maybe GoalEdge -> Bool
isContribEdge (Just (Contribution y)) = True
isContribEdge _                       = False

isCorrelEdge : Maybe GoalEdge -> Bool
isCorrelEdge (Just (Correlation y)) = True
isCorrelEdge _                      = False

getGoalByTitle : String -> GModel -> Maybe GoalNode
getGoalByTitle t g = getValueUsing (\x => getNodeTitle x == t) g

getGoalIDByTitle : String -> GModel -> Maybe NodeID
getGoalIDByTitle t g = getNodeIDUsing (\x => getNodeTitle x == t) g

getGoalByTitle' : GoalNode -> GModel -> Maybe GoalNode
getGoalByTitle' t g = getGoalByTitle (getNodeTitle t) g

hasGoal : String -> GModel -> Bool
hasGoal t m = isJust $ getValueUsing (\x => getNodeTitle x == t) m

updateGoalNode : (sfunc : GoalNode -> Bool)
              -> (ufunc : GoalNode -> GoalNode)
              -> (model : GModel)
              -> GModel
updateGoalNode f u m =
    case getValueUsing f m of
      Nothing  => m
      Just val => updateNodeValueUsing val u m

getDeCompEdges : NodeID -> GModel -> List (DemiEdge GoalEdge)
getDeCompEdges n m = filter (\(y,l) => isDeCompEdge l) cs
  where
    cs : List (DemiEdge GoalEdge)
    cs = getEdgesByID n m

getIntentEdges : NodeID -> GModel -> List (DemiEdge GoalEdge)
getIntentEdges n m = filter (\(y,l) => not (isDeCompEdge l)) cs
  where
    cs : List (DemiEdge GoalEdge)
    cs = getEdgesByID n m
-- --------------------------------------------------------------------- [ EOF ]

max_stars_repo_name: jfdm/idris-grl

max_issues_repo_name: jfdm/idris-grl

max_forks_repo_name: jfdm/idris-grl


text:
module LightClick.Check

import Decidable.Equality

import Data.List
import Data.Vect

import Toolkit.Data.DList
import Toolkit.Data.DList.DeBruijn
import Toolkit.Data.DVect

import Toolkit.Data.Location
import Toolkit.Data.Rig

import Language.SystemVerilog.Gates
import Language.SystemVerilog.Utilities

import LightClick.Error

import LightClick.Types
import LightClick.Types.Equality
import LightClick.Terms

import LightClick.Connection

import LightClick.Values
import LightClick.Env

%default covering

public export
TyCheck : Type -> Type
TyCheck = Either LightClick.Error

mutual
  namespace Field

    hasKey : (fc    : FileContext)
          -> (label : String)
          -> (store : List String)
                   -> TyCheck (List String)
    hasKey fc label store with (isElem label store)
      hasKey fc label store | Yes prf =
        Left (LabelAlreadyExists fc label store)
      hasKey fc label store | No contra = Right (label :: store)

    export
    check : (env   : Env ctxt)
         -> (key   : String)
         -> (value : Term ctxt DATA)
         -> (store : List String)
         -> TyCheck ( Pair String (Value DATA)
                    , Pair String (Ty DATA)
                    , List String
                    , Env ctxt
                    )
    -- References are special
    check env key (Ref {label} fc idx) store
      = do (v,t,env') <- check env (Ref fc idx)
           store' <- hasKey fc key store
           pure ((key, VRef label DATA), (key,t), store, env' )

    -- Rest is normal
    check env key term store
      = do (v,t,env') <- check env term
           fc <- getFC term
           store' <- hasKey fc key store
           pure ((key,v), (key,t), store, env')

  namespace Fields
    export
    check : {n : Nat}
         -> (env   : Env ctxt)
         -> (kvs   : Vect (S n) (Pair String (Term ctxt DATA)))
         -> (store : List String)
                  -> TyCheck
                         ( Vect (S n) (Pair String (Value DATA))
                         , Vect (S n) (Pair String (Ty DATA))
                         )
    check {n = n} env ((k,v) :: xs) store with (check env k v store)
      check {n = n} env ((k,v) :: xs) store | Left err = Left err
      check {n = n} env ((k,v) :: xs) store | Right (kv, kt, store', env') with (xs)
        check {n = Z} env ((k,v) :: Nil) store | Right (kv, kt, store', env') | Nil
          = pure ([kv], [kt])
        check {n = S n} env ((k,v) :: xs) store | Right (kv, kt, store', env') | (y::ys)
          = do (kvs, kts) <- check env' (y::ys) store'
               pure ((kv::kvs), kt::kts)

  namespace Modules

    export
    check : (env   : Env ctxt)
         -> (ports : DVect String
                           (\s => Term ctxt (PORT s))
                           (S n)
                           names)
         -> TyCheck ( DVect String (Value . PORT) (S n) names
                    , DVect String (Ty . PORT)    (S n) names
                    , Env ctxt)
    check {n = n} env (ex :: rest) with (Check.check env ex)
      check {n = n} env (ex :: rest) | (Left l) = Left l
      check {n = n} env (ex :: rest) | (Right (valueX, typeX, env')) with (rest)
        check {n = Z} env (ex :: Nil) | (Right (valueX, typeX, env')) | Nil
          = Right ([valueX], [typeX], env')
        check {n = S n} env (ex :: xs) | (Right (valueX, typeX, env')) | (y::ys)
          = do (pvs, pts, env'') <- Modules.check env' (y::ys)
               Right (valueX::pvs, typeX::pts, env'')

  namespace Port
    export
    use : {s : String} -> FileContext -> Ty (PORT s) -> TyCheck (Ty (PORT s))
    use fc type {s} = do u <- shiftUsage fc s (getUsage type)
                         Right (setUsage type u)

      where
        shiftUsage : FileContext -> String -> TyRig -> TyCheck TyRig
        shiftUsage fc s None  = Left (PortInUse fc s)
        shiftUsage _  _ One   = Right None
        shiftUsage _  _ Tonne = Right Tonne

    export
    check : (env  : Env ctxt)
         -> (term : Term ctxt (PORT s))
                 -> TyCheck (Value (PORT s), Ty (PORT s), Env ctxt)

    check env (Ref fc idx) with (Check.check env (Ref fc idx))
      check env (Ref fc idx) | Left l = Left l
      check env (Ref fc idx) | Right (v,t,env') with (t)
        check env (Ref fc idx) | Right (v,t,env') | portTy with (use fc portTy)
          check env (Ref fc idx) | Right (v,t,env') | portTy | Left l = Left l
          check env (Ref fc idx) | Right (v,t,env') | portTy | Right portTy'
            = do let env'' = updateWith env' idx (\(MkEntry value (MkTheType s portTy)) => MkEntry value (MkTheType s portTy'))
                 Right (v,portTy', env'')

    -- projection is just projection
    check env (Index fc mod idx) = Check.check env (Index fc mod idx)

    -- Seqs and Lets are not supposed to be here.
    check env _ = Left (NotSupposedToHappen (Just "Port.check"))

  namespace Fan

    export
    check : (env   : Env ctxt)
         -> (ports : DVect String
                           (\s => Term ctxt (PORT s))
                           (S (S n))
                           names)
         -> TyCheck
                   ( DVect String (Value . PORT) (S (S n)) names
                   , DVect String (Ty . PORT)    (S (S n)) names
                   , Env ctxt)
    check {n = n} env (x::y::xs) with (Port.check env x)
      check {n = n} env (x::y::xs) | Left l = Left l

      check {n = n} env (x::y::xs) | Right (vx,tx,ex) with (xs)
        check {n = Z} env (x::y::xs) | Right (vx,tx,ex) | Nil with (Port.check ex y)
          check {n = Z} env (x::y::xs) | Right (vx,tx,ex) | Nil | Left l
            = Left l
          check {n = Z} env (x::y::xs) | Right (vx,tx,ex) | Nil | Right (vy,ty,ey)
            = Right ([vx,vy], [tx,ty], ey)

        check {n = S n} env (x::y::xs) | Right (vx,tx,ex) | (z::zs) with (Fan.check ex (y::z::zs))
          check {n = S n} env (x::y::xs) | Right (vx,tx,ex) | (z::zs) | Left l = Left l
          check {n = S n} env (x::y::xs) | Right (vx,tx,ex) | (z::zs) | Right (vs, ts, env')
            = Right ((vx::vs), (tx::ts), env')

  -- [ Top Level Check Definition Begins Here ]

  export
  check : (env  : Env ctxt)
       -> (term : Term ctxt mty)
       -> TyCheck (Value (interp mty), Ty mty, Env ctxt)

  -- [ Checking References ]
  check env (Ref fc prf) with (read prf env)
    check env (Ref fc prf) | (MkEntry value (MkTheType name type))
      = Right (value, type, env)

  -- [ Checking Let Bindings ]
  check env (Let fc label this inThis)
    = do (ev, et, env') <- check env this
         (bv, bt, (u::env'')) <- check (MkEntry ev (MkTheType label et)::env') inThis
         Right (VLet label ev bv, bt, env'')

  -- [ Checking Sequencing ]
  check env (Seq x y)
    = do (vX, tX, env') <- check env x
         (vY, tY, env'') <- check env' y
         Right (VSeq vX vY, tY, env'')

  -- [ Checking Data Types]

  -- Logic
  check env (DataLogic fc) = Right (VDataLogic, TyLogic, env)

  -- Arrays
  check env (DataArray fc type size)
    = do (vs, ty', env') <- check env type
         Right (VDataArray vs size, TyArray ty' size, env')

  -- Data Strucutres

  -- Structs

  check env (DataStruct fc kvs)
    = do (kvalues, ktypes) <- check env kvs Nil
         Right (VDataStruct kvalues, TyStruct ktypes, env)

  -- Unions
  check env (DataUnion fc kvs)
    = do (kvalues, ktypes) <- check env kvs Nil
         Right (VDataUnion kvalues, TyUnion ktypes, env)

  -- [ Checking Ports ]
  check env (Port fc l d s w (Ref {label} x y))
    = do (v, t, env') <- check env (Ref x y)
         Right (VPort l d (VRef label DATA), TyPort l d s w t One, env')

  check env (Port fc l d s w term)
    = do (v, t, env') <- check env term
         Right (VPort l d v, TyPort l d s w t One, env')

  -- [ Checking Modules ]

  check env (Module fc ports)
    = do (vs, ts, env') <- check env ports
         Right (VModule vs, TyModule ts, env')

  -- [ Checking Module projection ]

  check env (Index fc m idx) with (check env m)
    check env (Index fc m idx) | Left l = Left l
    check env (Index fc (Ref fc' {label} midx) idx) | Right (v, t, env') with (t)
      check env (Index fc (Ref fc' {label} midx) idx) | Right (v, t, env') | TyModule names with (index names idx)
        check env (Index fc (Ref fc' {label} midx) idx) | Right (v, t, env') | TyModule names | portTy with (use fc portTy)
          check env (Index fc (Ref fc' {label} midx) idx) | Right (v, t, env') | TyModule names | portTy | Left l = Left l
          check env (Index fc (Ref fc' {label} midx) idx) | Right (v, t, env') | TyModule names | portTy | Right portTy'
            = do let names' = update names idx portTy'
                 let env''  = updateWith env' midx (\(MkEntry value (MkTheType s (TyModule names))) => MkEntry value (MkTheType s (TyModule names')))
                 port <- getPortFromModule v idx
                 Right (newIDX (recoverRef v label) port, portTy, env'')

    check env (Index fc _ idx) | Right (v, t, env') = Left (ConstantsNotAllowed fc)

  -- [ Checking Direct Connections ]

  check env (Connect fc left right)
    = do (vX, tyX, envx) <- Port.check env  left
         (vY, tyY, envy) <- Port.check envx right

         case compatible tyX tyY of
           No msg contra => Left (Nest (Mismatch fc tyX tyY)
                                       (UnSafeDirectConnection fc msg))
           Yes prf => do
             ty <- getData vX

             nX <- genNameConn vX
             nY <- genNameConn vY
             let n = newName [nX,nY]

             Right (VLet n (VChan ty) (newConn n vX vY), TyConn, envy)

  -- [ Checking Fanouts]

  check env (FanOut fc i fan)
    = do (vI, tyIN,  envi) <- Port.check env i
         (vF, tyFAN,  envf) <- Fan.check envi fan
         case Fanout.compatible tyIN tyFAN of
           No (PListError pos ty reason) contra =>
             Left (Nest (Mismatch fc tyIN ty) (UnSafeFan fc FANOUT pos reason))

           Yes prf => do
               ty <- getData vI

               nI <- genNameConn vI
               nF <- genNameFan vF
               let n = newName ["fan_out_from", nI, "to", nF]
               Right (VLet n (VChan ty) (newConn n vI vF) , TyConn, envf)

  -- [ Checking Multiplexers ]

  check env (Mux fc fan ctrl o)
    = do (fs, tf, envf) <- Fan.check  env  fan
         (vC, tc, envc) <- Port.check envf ctrl
         (vO, to, envo) <- Port.check envc o

         case Mux.compatible tf tc to of
           No (CtrlNotSafe c x) contra =>
                Left (Nest (Mismatch fc c tc)
                           (UnSafeMuxCtrl !(getFC ctrl) x))

           No (MuxNotSafe (PListError pos ty reason)) contra =>
             Left (Nest  (Mismatch fc ty to)
                         (UnSafeFan fc FANIN pos reason))
           Yes prf => do
             nO <- genNameConn vO
             nC <- genNameConn vC
             nF <- genNameFan  fs
             nFS <- getNameFan fs

             dC <- getData vC
             dO <- getData vO

             let mName = newName ["mux", nO, nC, nF]

             dualFS <- dualFan' ("input_") fs
             dualC  <- mkDual "control_" vC
             dualO  <- mkDual "output_" vO

             let mRef = (VRef mName (MODULE (nC::nO::nFS)))
             fi <- newConn (newName [mName, "fanin"]) dO mRef fs dualFS
             Right (VLet mName
                           (VModule (dualC::dualO::dualFS))
                           (VLet (newName [mName, "control"])
                                 (VChan dC)
                                 (VLet (newName [mName, "output"])
                                       (VChan dO)
                                       (VSeq (Direct.newConn (newName [mName, "control"]) vC (newIDX mRef dualC))
                                             (VSeq (Direct.newConn (newName [mName,"output"]) vO (newIDX mRef dualO))
                                                   fi
                                             )
                                       )

                                   )
                           )
                   , TyConn, envo)

  -- [ Checking NOT ]
  check env (NOT fc i o)
    = do (vX, tyX, envx) <- Port.check env  i
         (vY, tyY, envy) <- Port.check envx o

         case compatible tyX tyY of
           No msg contra =>
             Left (Nest (Mismatch fc tyX tyY)
                        (UnSafeDirectConnection fc msg))
           Yes prf => do

             ty <- getData vX

             nX <- genNameConn vX
             nY <- genNameConn vY

             let c_in_name = newName ["not_in",   nX, nY]
             let c_out_name = newName ["not_out", nX, nY]

             Right (VLet c_in_name
                         (VChan ty)
                         (VLet c_out_name
                               (VChan ty)
                               (VSeq (Gate.newConn c_in_name vX)
                                     (VSeq (Gate.newConn c_out_name vY)
                                           (VNot (VRef c_out_name CHAN)
                                                 (VRef c_in_name  CHAN)
                                         )
                                    )
                               )
                         )
                   , TyGate, envy
                   )

  -- [ Checking the GATE ]
  check env (GATE fc ty is o)
    = do (fs, tf, envf) <- Fan.check  env  is
         (vO, to, envo) <- Port.check envf o

         case Fanin.compatible tf to of
           No (PListError pos ty reason) contra => do
             Left (Nest (Mismatch fc ty to) (UnSafeFan fc FANIN pos reason))

           Yes prf => do

             tyO <- getData vO
             nO  <- genNameConn vO

             nF  <- genNameFan  fs

             let c_out_name = newName [Gates.toString ty, nO, nF, "out"]
             let c_in_name  = newName [toString ty, nO, nF, "in"]

             (ins', conns) <- Gate.FanIn.newConn c_in_name tyO fs

             Right (VLet c_out_name
                         (VChan tyO)
                         (VSeq conns
                               (VSeq (Gate.newConn c_out_name vO)
                                     (VGate ty (VRef c_out_name CHAN) ins')
                               )
                         )
                   , TyGate, envo)

  -- [ Checking the End ]
  check env End with (free env)
    check env End | Nil = Right (VEnd, TyUnit, env)
    check env End | (x::xs) = Left (UnusedPorts (x::xs))

export
runCheck : (term : Term Nil UNIT) -> TyCheck (Value UNIT)
runCheck term with (check Nil term)
  runCheck term | (Left l) = Left l
  runCheck term | (Right (value, ty, env)) = Right (value)

-- [ EOF ]

max_stars_repo_name: border-patrol/lightclick

max_issues_repo_name: border-patrol/lightclick

max_forks_repo_name: border-patrol/lightclick