text:
module Node.Error

public export
data SystemErrorCode
  = EACCES
  | EADDRINUSE
  | ECONNREFUSED
  | ECONNRESET
  | EEXIST
  | EISDIR
  | EMFILE
  | ENOENT
  | ENOTDIR
  | ENOTEMPTY
  | ENOTFOUND
  | EPERM
  | EPIPE
  | ETIMEDOUT
  | OtherSystemErrorCode String

public export
data Code
  = ABORT_ERR
  | ERR_AMBIGUOUS_ARGUMENT
  | ERR_ARG_NOT_ITERABLE
  | ERR_ASSERTION
  | ERR_ASYNC_CALLBACK
  | ERR_ASYNC_TYPE
  | ERR_BROTLI_COMPRESSION_FAILED
  | ERR_BROTLI_INVALID_PARAM
  | ERR_BUFFER_CONTEXT_NOT_AVAILABLE
  | ERR_BUFFER_OUT_OF_BOUNDS
  | ERR_BUFFER_TOO_LARGE
  | ERR_CANNOT_WATCH_SIGINT
  | ERR_CHILD_CLOSED_BEFORE_REPLY
  | ERR_CHILD_PROCESS_IPC_REQUIRED
  | ERR_CHILD_PROCESS_STDIO_MAXBUFFER
  | ERR_CLOSED_MESSAGE_PORT
  | ERR_CONSOLE_WRITABLE_STREAM
  | ERR_CONSTRUCT_CALL_INVALID
  | ERR_CONSTRUCT_CALL_REQUIRED
  | ERR_CONTEXT_NOT_INITIALIZED
  | ERR_CPU_USAGE
  | ERR_CRYPTO_CUSTOM_ENGINE_NOT_SUPPORTED
  | ERR_CRYPTO_ECDH_INVALID_FORMAT
  | ERR_CRYPTO_ECDH_INVALID_PUBLIC_KEY
  | ERR_CRYPTO_ENGINE_UNKNOWN
  | ERR_CRYPTO_FIPS_FORCED
  | ERR_CRYPTO_FIPS_UNAVAILABLE
  | ERR_CRYPTO_HASH_FINALIZED
  | ERR_CRYPTO_HASH_UPDATE_FAILED
  | ERR_CRYPTO_INCOMPATIBLE_KEY
  | ERR_CRYPTO_INCOMPATIBLE_KEY_OPTIONS
  | ERR_CRYPTO_INVALID_DIGEST
  | ERR_CRYPTO_INVALID_KEY_OBJECT_TYPE
  | ERR_CRYPTO_INVALID_STATE
  | ERR_CRYPTO_PBKDF2_ERROR
  | ERR_CRYPTO_SCRYPT_INVALID_PARAMETER
  | ERR_CRYPTO_SCRYPT_NOT_SUPPORTED
  | ERR_CRYPTO_SIGN_KEY_REQUIRED
  | ERR_CRYPTO_TIMING_SAFE_EQUAL_LENGTH
  | ERR_CRYPTO_UNKNOWN_CIPHER
  | ERR_CRYPTO_UNKNOWN_DH_GROUP
  | ERR_DEBUGGER_ERROR
  | ERR_DEBUGGER_STARTUP_ERROR
  | ERR_DIR_CLOSED
  | ERR_DIR_CONCURRENT_OPERATION
  | ERR_DNS_SET_SERVERS_FAILED
  | ERR_DOMAIN_CALLBACK_NOT_AVAILABLE
  | ERR_DOMAIN_CANNOT_SET_UNCAUGHT_EXCEPTION_CAPTURE
  | ERR_ENCODING_INVALID_ENCODED_DATA
  | ERR_ENCODING_NOT_SUPPORTED
  | ERR_EVAL_ESM_CANNOT_PRINT
  | ERR_EVENT_RECURSION
  | ERR_EXECUTION_ENVIRONMENT_NOT_AVAILABLE
  | ERR_FALSY_VALUE_REJECTION
  | ERR_FEATURE_UNAVAILABLE_ON_PLATFORM
  | ERR_FS_EISDIR
  | ERR_FS_FILE_TOO_LARGE
  | ERR_FS_INVALID_SYMLINK_TYPE
  | ERR_HTTP_HEADERS_SENT
  | ERR_HTTP_INVALID_HEADER_VALUE
  | ERR_HTTP_INVALID_STATUS_CODE
  | ERR_HTTP_TRAILER_INVALID
  | ERR_HTTP2_ALTSVC_INVALID_ORIGIN
  | ERR_HTTP2_ALTSVC_LENGTH
  | ERR_HTTP2_CONNECT_AUTHORITY
  | ERR_HTTP2_CONNECT_PATH
  | ERR_HTTP2_CONNECT_SCHEME
  | ERR_HTTP2_ERROR
  | ERR_HTTP2_GOAWAY_SESSION
  | ERR_HTTP2_HEADER_SINGLE_VALUE
  | ERR_HTTP2_HEADERS_AFTER_RESPOND
  | ERR_HTTP2_HEADERS_SENT
  | ERR_HTTP2_INFO_STATUS_NOT_ALLOWED
  | ERR_HTTP2_INVALID_CONNECTION_HEADERS
  | ERR_HTTP2_INVALID_HEADER_VALUE
  | ERR_HTTP2_INVALID_INFO_STATUS
  | ERR_HTTP2_INVALID_ORIGIN
  | ERR_HTTP2_INVALID_PACKED_SETTINGS_LENGTH
  | ERR_HTTP2_INVALID_PSEUDOHEADER
  | ERR_HTTP2_INVALID_SESSION
  | ERR_HTTP2_INVALID_SETTING_VALUE
  | ERR_HTTP2_INVALID_STREAM
  | ERR_HTTP2_MAX_PENDING_SETTINGS_ACK
  | ERR_HTTP2_NESTED_PUSH
  | ERR_HTTP2_NO_SOCKET_MANIPULATION
  | ERR_HTTP2_ORIGIN_LENGTH
  | ERR_HTTP2_OUT_OF_STREAMS
  | ERR_HTTP2_PAYLOAD_FORBIDDEN
  | ERR_HTTP2_PING_CANCEL
  | ERR_HTTP2_PING_LENGTH
  | ERR_HTTP2_PSEUDOHEADER_NOT_ALLOWED
  | ERR_HTTP2_PUSH_DISABLED
  | ERR_HTTP2_SEND_FILE
  | ERR_HTTP2_SEND_FILE_NOSEEK
  | ERR_HTTP2_SESSION_ERROR
  | ERR_HTTP2_SETTINGS_CANCEL
  | ERR_HTTP2_SOCKET_BOUND
  | ERR_HTTP2_SOCKET_UNBOUND
  | ERR_HTTP2_STATUS_101
  | ERR_HTTP2_STATUS_INVALID
  | ERR_HTTP2_STREAM_CANCEL
  | ERR_HTTP2_STREAM_ERROR
  | ERR_HTTP2_STREAM_SELF_DEPENDENCY
  | ERR_HTTP2_TRAILERS_ALREADY_SENT
  | ERR_HTTP2_TRAILERS_NOT_READY
  | ERR_HTTP2_UNSUPPORTED_PROTOCOL
  | ERR_INCOMPATIBLE_OPTION_PAIR
  | ERR_INPUT_TYPE_NOT_ALLOWED
  | ERR_INSPECTOR_ALREADY_ACTIVATED
  | ERR_INSPECTOR_ALREADY_CONNECTED
  | ERR_INSPECTOR_CLOSED
  | ERR_INSPECTOR_COMMAND
  | ERR_INSPECTOR_NOT_ACTIVE
  | ERR_INSPECTOR_NOT_AVAILABLE
  | ERR_INSPECTOR_NOT_CONNECTED
  | ERR_INSPECTOR_NOT_WORKER
  | ERR_INTERNAL_ASSERTION
  | ERR_INVALID_ADDRESS_FAMILY
  | ERR_INVALID_ARG_TYPE
  | ERR_INVALID_ARG_VALUE
  | ERR_INVALID_ASYNC_ID
  | ERR_INVALID_BUFFER_SIZE
  | ERR_INVALID_CALLBACK
  | ERR_INVALID_CHAR
  | ERR_INVALID_CURSOR_POS
  | ERR_INVALID_FD
  | ERR_INVALID_FD_TYPE
  | ERR_INVALID_FILE_URL_HOST
  | ERR_INVALID_FILE_URL_PATH
  | ERR_INVALID_HANDLE_TYPE
  | ERR_INVALID_HTTP_TOKEN
  | ERR_INVALID_IP_ADDRESS
  | ERR_INVALID_MODULE_SPECIFIER
  | ERR_INVALID_OPT_VALUE
  | ERR_INVALID_OPT_VALUE_ENCODING
  | ERR_INVALID_PACKAGE_CONFIG
  | ERR_INVALID_PACKAGE_TARGET
  | ERR_INVALID_PERFORMANCE_MARK
  | ERR_INVALID_PROTOCOL
  | ERR_INVALID_REPL_EVAL_CONFIG
  | ERR_INVALID_REPL_INPUT
  | ERR_INVALID_RETURN_PROPERTY
  | ERR_INVALID_RETURN_PROPERTY_VALUE
  | ERR_INVALID_RETURN_VALUE
  | ERR_INVALID_SYNC_FORK_INPUT
  | ERR_INVALID_THIS
  | ERR_INVALID_TRANSFER_OBJECT
  | ERR_INVALID_TUPLE
  | ERR_INVALID_URI
  | ERR_INVALID_URL
  | ERR_INVALID_URL_SCHEME
  | ERR_IPC_CHANNEL_CLOSED
  | ERR_IPC_DISCONNECTED
  | ERR_IPC_ONE_PIPE
  | ERR_IPC_SYNC_FORK
  | ERR_MANIFEST_ASSERT_INTEGRITY
  | ERR_MANIFEST_DEPENDENCY_MISSING
  | ERR_MANIFEST_INTEGRITY_MISMATCH
  | ERR_MANIFEST_INVALID_RESOURCE_FIELD
  | ERR_MANIFEST_PARSE_POLICY
  | ERR_MANIFEST_TDZ
  | ERR_MANIFEST_UNKNOWN_ONERROR
  | ERR_MEMORY_ALLOCATION_FAILED
  | ERR_MESSAGE_TARGET_CONTEXT_UNAVAILABLE
  | ERR_METHOD_NOT_IMPLEMENTED
  | ERR_MISSING_ARGS
  | ERR_MISSING_MESSAGE_PORT_IN_TRANSFER_LIST
  | ERR_MISSING_OPTION
  | ERR_MISSING_PASSPHRASE
  | ERR_MISSING_PLATFORM_FOR_WORKER
  | ERR_MODULE_NOT_FOUND
  | ERR_MULTIPLE_CALLBACK
  | ERR_NAPI_CONS_FUNCTION
  | ERR_NAPI_INVALID_DATAVIEW_ARGS
  | ERR_NAPI_INVALID_TYPEDARRAY_ALIGNMENT
  | ERR_NAPI_INVALID_TYPEDARRAY_LENGTH
  | ERR_NAPI_TSFN_CALL_JS
  | ERR_NAPI_TSFN_GET_UNDEFINED
  | ERR_NAPI_TSFN_START_IDLE_LOOP
  | ERR_NAPI_TSFN_STOP_IDLE_LOOP
  | ERR_NO_CRYPTO
  | ERR_NO_ICU
  | ERR_NON_CONTEXT_AWARE_DISABLED
  | ERR_OPERATION_FAILED
  | ERR_OUT_OF_RANGE
  | ERR_PACKAGE_IMPORT_NOT_DEFINED
  | ERR_PACKAGE_PATH_NOT_EXPORTED
  | ERR_PROTO_ACCESS
  | ERR_REQUIRE_ESM
  | ERR_SCRIPT_EXECUTION_INTERRUPTED
  | ERR_SCRIPT_EXECUTION_TIMEOUT
  | ERR_SERVER_ALREADY_LISTEN
  | ERR_SERVER_NOT_RUNNING
  | ERR_SOCKET_ALREADY_BOUND
  | ERR_SOCKET_BAD_BUFFER_SIZE
  | ERR_SOCKET_BAD_PORT
  | ERR_SOCKET_BAD_TYPE
  | ERR_SOCKET_BUFFER_SIZE
  | ERR_SOCKET_CLOSED
  | ERR_SOCKET_DGRAM_IS_CONNECTED
  | ERR_SOCKET_DGRAM_NOT_CONNECTED
  | ERR_SOCKET_DGRAM_NOT_RUNNING
  | ERR_SRI_PARSE
  | ERR_STREAM_ALREADY_FINISHED
  | ERR_STREAM_CANNOT_PIPE
  | ERR_STREAM_DESTROYED
  | ERR_STREAM_NULL_VALUES
  | ERR_STREAM_PREMATURE_CLOSE
  | ERR_STREAM_PUSH_AFTER_EOF
  | ERR_STREAM_UNSHIFT_AFTER_END_EVENT
  | ERR_STREAM_WRAP
  | ERR_STREAM_WRITE_AFTER_END
  | ERR_STRING_TOO_LONG
  | ERR_SYNTHETIC
  | ERR_SYSTEM_ERROR
  | ERR_TLS_CERT_ALTNAME_INVALID
  | ERR_TLS_DH_PARAM_SIZE
  | ERR_TLS_HANDSHAKE_TIMEOUT
  | ERR_TLS_INVALID_CONTEXT
  | ERR_TLS_INVALID_PROTOCOL_METHOD
  | ERR_TLS_INVALID_PROTOCOL_VERSION
  | ERR_TLS_INVALID_STATE
  | ERR_TLS_PROTOCOL_VERSION_CONFLICT
  | ERR_TLS_PSK_SET_IDENTIY_HINT_FAILED
  | ERR_TLS_RENEGOTIATION_DISABLED
  | ERR_TLS_REQUIRED_SERVER_NAME
  | ERR_TLS_SESSION_ATTACK
  | ERR_TLS_SNI_FROM_SERVER
  | ERR_TRACE_EVENTS_CATEGORY_REQUIRED
  | ERR_TRACE_EVENTS_UNAVAILABLE
  | ERR_TRANSFORM_ALREADY_TRANSFORMING
  | ERR_TRANSFORM_WITH_LENGTH_0
  | ERR_TTY_INIT_FAILED
  | ERR_UNAVAILABLE_DURING_EXIT
  | ERR_UNCAUGHT_EXCEPTION_CAPTURE_ALREADY_SET
  | ERR_UNESCAPED_CHARACTERS
  | ERR_UNHANDLED_ERROR
  | ERR_UNKNOWN_BUILTIN_MODULE
  | ERR_UNKNOWN_CREDENTIAL
  | ERR_UNKNOWN_ENCODING
  | ERR_UNKNOWN_FILE_EXTENSION
  | ERR_UNKNOWN_MODULE_FORMAT
  | ERR_UNKNOWN_SIGNAL
  | ERR_UNSUPPORTED_DIR_IMPORT
  | ERR_UNSUPPORTED_ESM_URL_SCHEME
  | ERR_VALID_PERFORMANCE_ENTRY_TYPE
  | ERR_VM_DYNAMIC_IMPORT_CALLBACK_MISSING
  | ERR_VM_MODULE_ALREADY_LINKED
  | ERR_VM_MODULE_CACHED_DATA_REJECTED
  | ERR_VM_MODULE_CANNOT_CREATE_CACHED_DATA
  | ERR_VM_MODULE_DIFFERENT_CONTEXT
  | ERR_VM_MODULE_LINKING_ERRORED
  | ERR_VM_MODULE_LINK_FAILURE
  | ERR_VM_MODULE_NOT_MODULE
  | ERR_VM_MODULE_STATUS
  | ERR_WASI_ALREADY_STARTED
  | ERR_WASI_NOT_STARTED
  | ERR_WORKER_INIT_FAILED
  | ERR_WORKER_INVALID_EXEC_ARGV
  | ERR_WORKER_NOT_RUNNING
  | ERR_WORKER_OUT_OF_MEMORY
  | ERR_WORKER_PATH
  | ERR_WORKER_UNSERIALIZABLE_ERROR
  | ERR_WORKER_UNSUPPORTED_EXTENSION
  | ERR_WORKER_UNSUPPORTED_OPERATION
  | ERR_ZLIB_INITIALIZATION_FAILED
  | HPE_HEADER_OVERFLOW
  | HPE_UNEXPECTED_CONTENT_LENGTH
  | MODULE_NOT_FOUND
  | SystemError SystemErrorCode
  | OtherCode String

fromString : String -> Code
fromString str = case str of
    "ABORT_ERR" => ABORT_ERR
    "ERR_AMBIGUOUS_ARGUMENT" => ERR_AMBIGUOUS_ARGUMENT
    "ERR_ARG_NOT_ITERABLE" => ERR_ARG_NOT_ITERABLE
    "ERR_ASSERTION" => ERR_ASSERTION
    "ERR_ASYNC_CALLBACK" => ERR_ASYNC_CALLBACK
    "ERR_ASYNC_TYPE" => ERR_ASYNC_TYPE
    "ERR_BROTLI_COMPRESSION_FAILED" => ERR_BROTLI_COMPRESSION_FAILED
    "ERR_BROTLI_INVALID_PARAM" => ERR_BROTLI_INVALID_PARAM
    "ERR_BUFFER_CONTEXT_NOT_AVAILABLE" => ERR_BUFFER_CONTEXT_NOT_AVAILABLE
    "ERR_BUFFER_OUT_OF_BOUNDS" => ERR_BUFFER_OUT_OF_BOUNDS
    "ERR_BUFFER_TOO_LARGE" => ERR_BUFFER_TOO_LARGE
    "ERR_CANNOT_WATCH_SIGINT" => ERR_CANNOT_WATCH_SIGINT
    "ERR_CHILD_CLOSED_BEFORE_REPLY" => ERR_CHILD_CLOSED_BEFORE_REPLY
    "ERR_CHILD_PROCESS_IPC_REQUIRED" => ERR_CHILD_PROCESS_IPC_REQUIRED
    "ERR_CHILD_PROCESS_STDIO_MAXBUFFER" => ERR_CHILD_PROCESS_STDIO_MAXBUFFER
    "ERR_CLOSED_MESSAGE_PORT" => ERR_CLOSED_MESSAGE_PORT
    "ERR_CONSOLE_WRITABLE_STREAM" => ERR_CONSOLE_WRITABLE_STREAM
    "ERR_CONSTRUCT_CALL_INVALID" => ERR_CONSTRUCT_CALL_INVALID
    "ERR_CONSTRUCT_CALL_REQUIRED" => ERR_CONSTRUCT_CALL_REQUIRED
    "ERR_CONTEXT_NOT_INITIALIZED" => ERR_CONTEXT_NOT_INITIALIZED
    "ERR_CPU_USAGE" => ERR_CPU_USAGE
    "ERR_CRYPTO_CUSTOM_ENGINE_NOT_SUPPORTED" => ERR_CRYPTO_CUSTOM_ENGINE_NOT_SUPPORTED
    "ERR_CRYPTO_ECDH_INVALID_FORMAT" => ERR_CRYPTO_ECDH_INVALID_FORMAT
    "ERR_CRYPTO_ECDH_INVALID_PUBLIC_KEY" => ERR_CRYPTO_ECDH_INVALID_PUBLIC_KEY
    "ERR_CRYPTO_ENGINE_UNKNOWN" => ERR_CRYPTO_ENGINE_UNKNOWN
    "ERR_CRYPTO_FIPS_FORCED" => ERR_CRYPTO_FIPS_FORCED
    "ERR_CRYPTO_FIPS_UNAVAILABLE" => ERR_CRYPTO_FIPS_UNAVAILABLE
    "ERR_CRYPTO_HASH_FINALIZED" => ERR_CRYPTO_HASH_FINALIZED
    "ERR_CRYPTO_HASH_UPDATE_FAILED" => ERR_CRYPTO_HASH_UPDATE_FAILED
    "ERR_CRYPTO_INCOMPATIBLE_KEY" => ERR_CRYPTO_INCOMPATIBLE_KEY
    "ERR_CRYPTO_INCOMPATIBLE_KEY_OPTIONS" => ERR_CRYPTO_INCOMPATIBLE_KEY_OPTIONS
    "ERR_CRYPTO_INVALID_DIGEST" => ERR_CRYPTO_INVALID_DIGEST
    "ERR_CRYPTO_INVALID_KEY_OBJECT_TYPE" => ERR_CRYPTO_INVALID_KEY_OBJECT_TYPE
    "ERR_CRYPTO_INVALID_STATE" => ERR_CRYPTO_INVALID_STATE
    "ERR_CRYPTO_PBKDF2_ERROR" => ERR_CRYPTO_PBKDF2_ERROR
    "ERR_CRYPTO_SCRYPT_INVALID_PARAMETER" => ERR_CRYPTO_SCRYPT_INVALID_PARAMETER
    "ERR_CRYPTO_SCRYPT_NOT_SUPPORTED" => ERR_CRYPTO_SCRYPT_NOT_SUPPORTED
    "ERR_CRYPTO_SIGN_KEY_REQUIRED" => ERR_CRYPTO_SIGN_KEY_REQUIRED
    "ERR_CRYPTO_TIMING_SAFE_EQUAL_LENGTH" => ERR_CRYPTO_TIMING_SAFE_EQUAL_LENGTH
    "ERR_CRYPTO_UNKNOWN_CIPHER" => ERR_CRYPTO_UNKNOWN_CIPHER
    "ERR_CRYPTO_UNKNOWN_DH_GROUP" => ERR_CRYPTO_UNKNOWN_DH_GROUP
    "ERR_DEBUGGER_ERROR" => ERR_DEBUGGER_ERROR
    "ERR_DEBUGGER_STARTUP_ERROR" => ERR_DEBUGGER_STARTUP_ERROR
    "ERR_DIR_CLOSED" => ERR_DIR_CLOSED
    "ERR_DIR_CONCURRENT_OPERATION" => ERR_DIR_CONCURRENT_OPERATION
    "ERR_DNS_SET_SERVERS_FAILED" => ERR_DNS_SET_SERVERS_FAILED
    "ERR_DOMAIN_CALLBACK_NOT_AVAILABLE" => ERR_DOMAIN_CALLBACK_NOT_AVAILABLE
    "ERR_DOMAIN_CANNOT_SET_UNCAUGHT_EXCEPTION_CAPTURE" => ERR_DOMAIN_CANNOT_SET_UNCAUGHT_EXCEPTION_CAPTURE
    "ERR_ENCODING_INVALID_ENCODED_DATA" => ERR_ENCODING_INVALID_ENCODED_DATA
    "ERR_ENCODING_NOT_SUPPORTED" => ERR_ENCODING_NOT_SUPPORTED
    "ERR_EVAL_ESM_CANNOT_PRINT" => ERR_EVAL_ESM_CANNOT_PRINT
    "ERR_EVENT_RECURSION" => ERR_EVENT_RECURSION
    "ERR_EXECUTION_ENVIRONMENT_NOT_AVAILABLE" => ERR_EXECUTION_ENVIRONMENT_NOT_AVAILABLE
    "ERR_FALSY_VALUE_REJECTION" => ERR_FALSY_VALUE_REJECTION
    "ERR_FEATURE_UNAVAILABLE_ON_PLATFORM" => ERR_FEATURE_UNAVAILABLE_ON_PLATFORM
    "ERR_FS_EISDIR" => ERR_FS_EISDIR
    "ERR_FS_FILE_TOO_LARGE" => ERR_FS_FILE_TOO_LARGE
    "ERR_FS_INVALID_SYMLINK_TYPE" => ERR_FS_INVALID_SYMLINK_TYPE
    "ERR_HTTP_HEADERS_SENT" => ERR_HTTP_HEADERS_SENT
    "ERR_HTTP_INVALID_HEADER_VALUE" => ERR_HTTP_INVALID_HEADER_VALUE
    "ERR_HTTP_INVALID_STATUS_CODE" => ERR_HTTP_INVALID_STATUS_CODE
    "ERR_HTTP_TRAILER_INVALID" => ERR_HTTP_TRAILER_INVALID
    "ERR_HTTP2_ALTSVC_INVALID_ORIGIN" => ERR_HTTP2_ALTSVC_INVALID_ORIGIN
    "ERR_HTTP2_ALTSVC_LENGTH" => ERR_HTTP2_ALTSVC_LENGTH
    "ERR_HTTP2_CONNECT_AUTHORITY" => ERR_HTTP2_CONNECT_AUTHORITY
    "ERR_HTTP2_CONNECT_PATH" => ERR_HTTP2_CONNECT_PATH
    "ERR_HTTP2_CONNECT_SCHEME" => ERR_HTTP2_CONNECT_SCHEME
    "ERR_HTTP2_ERROR" => ERR_HTTP2_ERROR
    "ERR_HTTP2_GOAWAY_SESSION" => ERR_HTTP2_GOAWAY_SESSION
    "ERR_HTTP2_HEADER_SINGLE_VALUE" => ERR_HTTP2_HEADER_SINGLE_VALUE
    "ERR_HTTP2_HEADERS_AFTER_RESPOND" => ERR_HTTP2_HEADERS_AFTER_RESPOND
    "ERR_HTTP2_HEADERS_SENT" => ERR_HTTP2_HEADERS_SENT
    "ERR_HTTP2_INFO_STATUS_NOT_ALLOWED" => ERR_HTTP2_INFO_STATUS_NOT_ALLOWED
    "ERR_HTTP2_INVALID_CONNECTION_HEADERS" => ERR_HTTP2_INVALID_CONNECTION_HEADERS
    "ERR_HTTP2_INVALID_HEADER_VALUE" => ERR_HTTP2_INVALID_HEADER_VALUE
    "ERR_HTTP2_INVALID_INFO_STATUS" => ERR_HTTP2_INVALID_INFO_STATUS
    "ERR_HTTP2_INVALID_ORIGIN" => ERR_HTTP2_INVALID_ORIGIN
    "ERR_HTTP2_INVALID_PACKED_SETTINGS_LENGTH" => ERR_HTTP2_INVALID_PACKED_SETTINGS_LENGTH
    "ERR_HTTP2_INVALID_PSEUDOHEADER" => ERR_HTTP2_INVALID_PSEUDOHEADER
    "ERR_HTTP2_INVALID_SESSION" => ERR_HTTP2_INVALID_SESSION
    "ERR_HTTP2_INVALID_SETTING_VALUE" => ERR_HTTP2_INVALID_SETTING_VALUE
    "ERR_HTTP2_INVALID_STREAM" => ERR_HTTP2_INVALID_STREAM
    "ERR_HTTP2_MAX_PENDING_SETTINGS_ACK" => ERR_HTTP2_MAX_PENDING_SETTINGS_ACK
    "ERR_HTTP2_NESTED_PUSH" => ERR_HTTP2_NESTED_PUSH
    "ERR_HTTP2_NO_SOCKET_MANIPULATION" => ERR_HTTP2_NO_SOCKET_MANIPULATION
    "ERR_HTTP2_ORIGIN_LENGTH" => ERR_HTTP2_ORIGIN_LENGTH
    "ERR_HTTP2_OUT_OF_STREAMS" => ERR_HTTP2_OUT_OF_STREAMS
    "ERR_HTTP2_PAYLOAD_FORBIDDEN" => ERR_HTTP2_PAYLOAD_FORBIDDEN
    "ERR_HTTP2_PING_CANCEL" => ERR_HTTP2_PING_CANCEL
    "ERR_HTTP2_PING_LENGTH" => ERR_HTTP2_PING_LENGTH
    "ERR_HTTP2_PSEUDOHEADER_NOT_ALLOWED" => ERR_HTTP2_PSEUDOHEADER_NOT_ALLOWED
    "ERR_HTTP2_PUSH_DISABLED" => ERR_HTTP2_PUSH_DISABLED
    "ERR_HTTP2_SEND_FILE" => ERR_HTTP2_SEND_FILE
    "ERR_HTTP2_SEND_FILE_NOSEEK" => ERR_HTTP2_SEND_FILE_NOSEEK
    "ERR_HTTP2_SESSION_ERROR" => ERR_HTTP2_SESSION_ERROR
    "ERR_HTTP2_SETTINGS_CANCEL" => ERR_HTTP2_SETTINGS_CANCEL
    "ERR_HTTP2_SOCKET_BOUND" => ERR_HTTP2_SOCKET_BOUND
    "ERR_HTTP2_SOCKET_UNBOUND" => ERR_HTTP2_SOCKET_UNBOUND
    "ERR_HTTP2_STATUS_101" => ERR_HTTP2_STATUS_101
    "ERR_HTTP2_STATUS_INVALID" => ERR_HTTP2_STATUS_INVALID
    "ERR_HTTP2_STREAM_CANCEL" => ERR_HTTP2_STREAM_CANCEL
    "ERR_HTTP2_STREAM_ERROR" => ERR_HTTP2_STREAM_ERROR
    "ERR_HTTP2_STREAM_SELF_DEPENDENCY" => ERR_HTTP2_STREAM_SELF_DEPENDENCY
    "ERR_HTTP2_TRAILERS_ALREADY_SENT" => ERR_HTTP2_TRAILERS_ALREADY_SENT
    "ERR_HTTP2_TRAILERS_NOT_READY" => ERR_HTTP2_TRAILERS_NOT_READY
    "ERR_HTTP2_UNSUPPORTED_PROTOCOL" => ERR_HTTP2_UNSUPPORTED_PROTOCOL
    "ERR_INCOMPATIBLE_OPTION_PAIR" => ERR_INCOMPATIBLE_OPTION_PAIR
    "ERR_INPUT_TYPE_NOT_ALLOWED" => ERR_INPUT_TYPE_NOT_ALLOWED
    "ERR_INSPECTOR_ALREADY_ACTIVATED" => ERR_INSPECTOR_ALREADY_ACTIVATED
    "ERR_INSPECTOR_ALREADY_CONNECTED" => ERR_INSPECTOR_ALREADY_CONNECTED
    "ERR_INSPECTOR_CLOSED" => ERR_INSPECTOR_CLOSED
    "ERR_INSPECTOR_COMMAND" => ERR_INSPECTOR_COMMAND
    "ERR_INSPECTOR_NOT_ACTIVE" => ERR_INSPECTOR_NOT_ACTIVE
    "ERR_INSPECTOR_NOT_AVAILABLE" => ERR_INSPECTOR_NOT_AVAILABLE
    "ERR_INSPECTOR_NOT_CONNECTED" => ERR_INSPECTOR_NOT_CONNECTED
    "ERR_INSPECTOR_NOT_WORKER" => ERR_INSPECTOR_NOT_WORKER
    "ERR_INTERNAL_ASSERTION" => ERR_INTERNAL_ASSERTION
    "ERR_INVALID_ADDRESS_FAMILY" => ERR_INVALID_ADDRESS_FAMILY
    "ERR_INVALID_ARG_TYPE" => ERR_INVALID_ARG_TYPE
    "ERR_INVALID_ARG_VALUE" => ERR_INVALID_ARG_VALUE
    "ERR_INVALID_ASYNC_ID" => ERR_INVALID_ASYNC_ID
    "ERR_INVALID_BUFFER_SIZE" => ERR_INVALID_BUFFER_SIZE
    "ERR_INVALID_CALLBACK" => ERR_INVALID_CALLBACK
    "ERR_INVALID_CHAR" => ERR_INVALID_CHAR
    "ERR_INVALID_CURSOR_POS" => ERR_INVALID_CURSOR_POS
    "ERR_INVALID_FD" => ERR_INVALID_FD
    "ERR_INVALID_FD_TYPE" => ERR_INVALID_FD_TYPE
    "ERR_INVALID_FILE_URL_HOST" => ERR_INVALID_FILE_URL_HOST
    "ERR_INVALID_FILE_URL_PATH" => ERR_INVALID_FILE_URL_PATH
    "ERR_INVALID_HANDLE_TYPE" => ERR_INVALID_HANDLE_TYPE
    "ERR_INVALID_HTTP_TOKEN" => ERR_INVALID_HTTP_TOKEN
    "ERR_INVALID_IP_ADDRESS" => ERR_INVALID_IP_ADDRESS
    "ERR_INVALID_MODULE_SPECIFIER" => ERR_INVALID_MODULE_SPECIFIER
    "ERR_INVALID_OPT_VALUE" => ERR_INVALID_OPT_VALUE
    "ERR_INVALID_OPT_VALUE_ENCODING" => ERR_INVALID_OPT_VALUE_ENCODING
    "ERR_INVALID_PACKAGE_CONFIG" => ERR_INVALID_PACKAGE_CONFIG
    "ERR_INVALID_PACKAGE_TARGET" => ERR_INVALID_PACKAGE_TARGET
    "ERR_INVALID_PERFORMANCE_MARK" => ERR_INVALID_PERFORMANCE_MARK
    "ERR_INVALID_PROTOCOL" => ERR_INVALID_PROTOCOL
    "ERR_INVALID_REPL_EVAL_CONFIG" => ERR_INVALID_REPL_EVAL_CONFIG
    "ERR_INVALID_REPL_INPUT" => ERR_INVALID_REPL_INPUT
    "ERR_INVALID_RETURN_PROPERTY" => ERR_INVALID_RETURN_PROPERTY
    "ERR_INVALID_RETURN_PROPERTY_VALUE" => ERR_INVALID_RETURN_PROPERTY_VALUE
    "ERR_INVALID_RETURN_VALUE" => ERR_INVALID_RETURN_VALUE
    "ERR_INVALID_SYNC_FORK_INPUT" => ERR_INVALID_SYNC_FORK_INPUT
    "ERR_INVALID_THIS" => ERR_INVALID_THIS
    "ERR_INVALID_TRANSFER_OBJECT" => ERR_INVALID_TRANSFER_OBJECT
    "ERR_INVALID_TUPLE" => ERR_INVALID_TUPLE
    "ERR_INVALID_URI" => ERR_INVALID_URI
    "ERR_INVALID_URL" => ERR_INVALID_URL
    "ERR_INVALID_URL_SCHEME" => ERR_INVALID_URL_SCHEME
    "ERR_IPC_CHANNEL_CLOSED" => ERR_IPC_CHANNEL_CLOSED
    "ERR_IPC_DISCONNECTED" => ERR_IPC_DISCONNECTED
    "ERR_IPC_ONE_PIPE" => ERR_IPC_ONE_PIPE
    "ERR_IPC_SYNC_FORK" => ERR_IPC_SYNC_FORK
    "ERR_MANIFEST_ASSERT_INTEGRITY" => ERR_MANIFEST_ASSERT_INTEGRITY
    "ERR_MANIFEST_DEPENDENCY_MISSING" => ERR_MANIFEST_DEPENDENCY_MISSING
    "ERR_MANIFEST_INTEGRITY_MISMATCH" => ERR_MANIFEST_INTEGRITY_MISMATCH
    "ERR_MANIFEST_INVALID_RESOURCE_FIELD" => ERR_MANIFEST_INVALID_RESOURCE_FIELD
    "ERR_MANIFEST_PARSE_POLICY" => ERR_MANIFEST_PARSE_POLICY
    "ERR_MANIFEST_TDZ" => ERR_MANIFEST_TDZ
    "ERR_MANIFEST_UNKNOWN_ONERROR" => ERR_MANIFEST_UNKNOWN_ONERROR
    "ERR_MEMORY_ALLOCATION_FAILED" => ERR_MEMORY_ALLOCATION_FAILED
    "ERR_MESSAGE_TARGET_CONTEXT_UNAVAILABLE" => ERR_MESSAGE_TARGET_CONTEXT_UNAVAILABLE
    "ERR_METHOD_NOT_IMPLEMENTED" => ERR_METHOD_NOT_IMPLEMENTED
    "ERR_MISSING_ARGS" => ERR_MISSING_ARGS
    "ERR_MISSING_MESSAGE_PORT_IN_TRANSFER_LIST" => ERR_MISSING_MESSAGE_PORT_IN_TRANSFER_LIST
    "ERR_MISSING_OPTION" => ERR_MISSING_OPTION
    "ERR_MISSING_PASSPHRASE" => ERR_MISSING_PASSPHRASE
    "ERR_MISSING_PLATFORM_FOR_WORKER" => ERR_MISSING_PLATFORM_FOR_WORKER
    "ERR_MODULE_NOT_FOUND" => ERR_MODULE_NOT_FOUND
    "ERR_MULTIPLE_CALLBACK" => ERR_MULTIPLE_CALLBACK
    "ERR_NAPI_CONS_FUNCTION" => ERR_NAPI_CONS_FUNCTION
    "ERR_NAPI_INVALID_DATAVIEW_ARGS" => ERR_NAPI_INVALID_DATAVIEW_ARGS
    "ERR_NAPI_INVALID_TYPEDARRAY_ALIGNMENT" => ERR_NAPI_INVALID_TYPEDARRAY_ALIGNMENT
    "ERR_NAPI_INVALID_TYPEDARRAY_LENGTH" => ERR_NAPI_INVALID_TYPEDARRAY_LENGTH
    "ERR_NAPI_TSFN_CALL_JS" => ERR_NAPI_TSFN_CALL_JS
    "ERR_NAPI_TSFN_GET_UNDEFINED" => ERR_NAPI_TSFN_GET_UNDEFINED
    "ERR_NAPI_TSFN_START_IDLE_LOOP" => ERR_NAPI_TSFN_START_IDLE_LOOP
    "ERR_NAPI_TSFN_STOP_IDLE_LOOP" => ERR_NAPI_TSFN_STOP_IDLE_LOOP
    "ERR_NO_CRYPTO" => ERR_NO_CRYPTO
    "ERR_NO_ICU" => ERR_NO_ICU
    "ERR_NON_CONTEXT_AWARE_DISABLED" => ERR_NON_CONTEXT_AWARE_DISABLED
    "ERR_OPERATION_FAILED" => ERR_OPERATION_FAILED
    "ERR_OUT_OF_RANGE" => ERR_OUT_OF_RANGE
    "ERR_PACKAGE_IMPORT_NOT_DEFINED" => ERR_PACKAGE_IMPORT_NOT_DEFINED
    "ERR_PACKAGE_PATH_NOT_EXPORTED" => ERR_PACKAGE_PATH_NOT_EXPORTED
    "ERR_PROTO_ACCESS" => ERR_PROTO_ACCESS
    "ERR_REQUIRE_ESM" => ERR_REQUIRE_ESM
    "ERR_SCRIPT_EXECUTION_INTERRUPTED" => ERR_SCRIPT_EXECUTION_INTERRUPTED
    "ERR_SCRIPT_EXECUTION_TIMEOUT" => ERR_SCRIPT_EXECUTION_TIMEOUT
    "ERR_SERVER_ALREADY_LISTEN" => ERR_SERVER_ALREADY_LISTEN
    "ERR_SERVER_NOT_RUNNING" => ERR_SERVER_NOT_RUNNING
    "ERR_SOCKET_ALREADY_BOUND" => ERR_SOCKET_ALREADY_BOUND
    "ERR_SOCKET_BAD_BUFFER_SIZE" => ERR_SOCKET_BAD_BUFFER_SIZE
    "ERR_SOCKET_BAD_PORT" => ERR_SOCKET_BAD_PORT
    "ERR_SOCKET_BAD_TYPE" => ERR_SOCKET_BAD_TYPE
    "ERR_SOCKET_BUFFER_SIZE" => ERR_SOCKET_BUFFER_SIZE
    "ERR_SOCKET_CLOSED" => ERR_SOCKET_CLOSED
    "ERR_SOCKET_DGRAM_IS_CONNECTED" => ERR_SOCKET_DGRAM_IS_CONNECTED
    "ERR_SOCKET_DGRAM_NOT_CONNECTED" => ERR_SOCKET_DGRAM_NOT_CONNECTED
    "ERR_SOCKET_DGRAM_NOT_RUNNING" => ERR_SOCKET_DGRAM_NOT_RUNNING
    "ERR_SRI_PARSE" => ERR_SRI_PARSE
    "ERR_STREAM_ALREADY_FINISHED" => ERR_STREAM_ALREADY_FINISHED
    "ERR_STREAM_CANNOT_PIPE" => ERR_STREAM_CANNOT_PIPE
    "ERR_STREAM_DESTROYED" => ERR_STREAM_DESTROYED
    "ERR_STREAM_NULL_VALUES" => ERR_STREAM_NULL_VALUES
    "ERR_STREAM_PREMATURE_CLOSE" => ERR_STREAM_PREMATURE_CLOSE
    "ERR_STREAM_PUSH_AFTER_EOF" => ERR_STREAM_PUSH_AFTER_EOF
    "ERR_STREAM_UNSHIFT_AFTER_END_EVENT" => ERR_STREAM_UNSHIFT_AFTER_END_EVENT
    "ERR_STREAM_WRAP" => ERR_STREAM_WRAP
    "ERR_STREAM_WRITE_AFTER_END" => ERR_STREAM_WRITE_AFTER_END
    "ERR_STRING_TOO_LONG" => ERR_STRING_TOO_LONG
    "ERR_SYNTHETIC" => ERR_SYNTHETIC
    "ERR_SYSTEM_ERROR" => ERR_SYSTEM_ERROR
    "ERR_TLS_CERT_ALTNAME_INVALID" => ERR_TLS_CERT_ALTNAME_INVALID
    "ERR_TLS_DH_PARAM_SIZE" => ERR_TLS_DH_PARAM_SIZE
    "ERR_TLS_HANDSHAKE_TIMEOUT" => ERR_TLS_HANDSHAKE_TIMEOUT
    "ERR_TLS_INVALID_CONTEXT" => ERR_TLS_INVALID_CONTEXT
    "ERR_TLS_INVALID_PROTOCOL_METHOD" => ERR_TLS_INVALID_PROTOCOL_METHOD
    "ERR_TLS_INVALID_PROTOCOL_VERSION" => ERR_TLS_INVALID_PROTOCOL_VERSION
    "ERR_TLS_INVALID_STATE" => ERR_TLS_INVALID_STATE
    "ERR_TLS_PROTOCOL_VERSION_CONFLICT" => ERR_TLS_PROTOCOL_VERSION_CONFLICT
    "ERR_TLS_PSK_SET_IDENTIY_HINT_FAILED" => ERR_TLS_PSK_SET_IDENTIY_HINT_FAILED
    "ERR_TLS_RENEGOTIATION_DISABLED" => ERR_TLS_RENEGOTIATION_DISABLED
    "ERR_TLS_REQUIRED_SERVER_NAME" => ERR_TLS_REQUIRED_SERVER_NAME
    "ERR_TLS_SESSION_ATTACK" => ERR_TLS_SESSION_ATTACK
    "ERR_TLS_SNI_FROM_SERVER" => ERR_TLS_SNI_FROM_SERVER
    "ERR_TRACE_EVENTS_CATEGORY_REQUIRED" => ERR_TRACE_EVENTS_CATEGORY_REQUIRED
    "ERR_TRACE_EVENTS_UNAVAILABLE" => ERR_TRACE_EVENTS_UNAVAILABLE
    "ERR_TRANSFORM_ALREADY_TRANSFORMING" => ERR_TRANSFORM_ALREADY_TRANSFORMING
    "ERR_TRANSFORM_WITH_LENGTH_0" => ERR_TRANSFORM_WITH_LENGTH_0
    "ERR_TTY_INIT_FAILED" => ERR_TTY_INIT_FAILED
    "ERR_UNAVAILABLE_DURING_EXIT" => ERR_UNAVAILABLE_DURING_EXIT
    "ERR_UNCAUGHT_EXCEPTION_CAPTURE_ALREADY_SET" => ERR_UNCAUGHT_EXCEPTION_CAPTURE_ALREADY_SET
    "ERR_UNESCAPED_CHARACTERS" => ERR_UNESCAPED_CHARACTERS
    "ERR_UNHANDLED_ERROR" => ERR_UNHANDLED_ERROR
    "ERR_UNKNOWN_BUILTIN_MODULE" => ERR_UNKNOWN_BUILTIN_MODULE
    "ERR_UNKNOWN_CREDENTIAL" => ERR_UNKNOWN_CREDENTIAL
    "ERR_UNKNOWN_ENCODING" => ERR_UNKNOWN_ENCODING
    "ERR_UNKNOWN_FILE_EXTENSION" => ERR_UNKNOWN_FILE_EXTENSION
    "ERR_UNKNOWN_MODULE_FORMAT" => ERR_UNKNOWN_MODULE_FORMAT
    "ERR_UNKNOWN_SIGNAL" => ERR_UNKNOWN_SIGNAL
    "ERR_UNSUPPORTED_DIR_IMPORT" => ERR_UNSUPPORTED_DIR_IMPORT
    "ERR_UNSUPPORTED_ESM_URL_SCHEME" => ERR_UNSUPPORTED_ESM_URL_SCHEME
    "ERR_VALID_PERFORMANCE_ENTRY_TYPE" => ERR_VALID_PERFORMANCE_ENTRY_TYPE
    "ERR_VM_DYNAMIC_IMPORT_CALLBACK_MISSING" => ERR_VM_DYNAMIC_IMPORT_CALLBACK_MISSING
    "ERR_VM_MODULE_ALREADY_LINKED" => ERR_VM_MODULE_ALREADY_LINKED
    "ERR_VM_MODULE_CACHED_DATA_REJECTED" => ERR_VM_MODULE_CACHED_DATA_REJECTED
    "ERR_VM_MODULE_CANNOT_CREATE_CACHED_DATA" => ERR_VM_MODULE_CANNOT_CREATE_CACHED_DATA
    "ERR_VM_MODULE_DIFFERENT_CONTEXT" => ERR_VM_MODULE_DIFFERENT_CONTEXT
    "ERR_VM_MODULE_LINKING_ERRORED" => ERR_VM_MODULE_LINKING_ERRORED
    "ERR_VM_MODULE_LINK_FAILURE" => ERR_VM_MODULE_LINK_FAILURE
    "ERR_VM_MODULE_NOT_MODULE" => ERR_VM_MODULE_NOT_MODULE
    "ERR_VM_MODULE_STATUS" => ERR_VM_MODULE_STATUS
    "ERR_WASI_ALREADY_STARTED" => ERR_WASI_ALREADY_STARTED
    "ERR_WASI_NOT_STARTED" => ERR_WASI_NOT_STARTED
    "ERR_WORKER_INIT_FAILED" => ERR_WORKER_INIT_FAILED
    "ERR_WORKER_INVALID_EXEC_ARGV" => ERR_WORKER_INVALID_EXEC_ARGV
    "ERR_WORKER_NOT_RUNNING" => ERR_WORKER_NOT_RUNNING
    "ERR_WORKER_OUT_OF_MEMORY" => ERR_WORKER_OUT_OF_MEMORY
    "ERR_WORKER_PATH" => ERR_WORKER_PATH
    "ERR_WORKER_UNSERIALIZABLE_ERROR" => ERR_WORKER_UNSERIALIZABLE_ERROR
    "ERR_WORKER_UNSUPPORTED_EXTENSION" => ERR_WORKER_UNSUPPORTED_EXTENSION
    "ERR_WORKER_UNSUPPORTED_OPERATION" => ERR_WORKER_UNSUPPORTED_OPERATION
    "ERR_ZLIB_INITIALIZATION_FAILED" => ERR_ZLIB_INITIALIZATION_FAILED
    "HPE_HEADER_OVERFLOW" => HPE_HEADER_OVERFLOW
    "HPE_UNEXPECTED_CONTENT_LENGTH" => HPE_UNEXPECTED_CONTENT_LENGTH
    "MODULE_NOT_FOUND" => MODULE_NOT_FOUND
    "EACCES" => SystemError EACCES
    "EADDRINUSE" => SystemError EADDRINUSE
    "ECONNREFUSED" => SystemError ECONNREFUSED
    "ECONNRESET" => SystemError ECONNRESET
    "EEXIST" => SystemError EEXIST
    "EISDIR" => SystemError EISDIR
    "EMFILE" => SystemError EMFILE
    "ENOENT" => SystemError ENOENT
    "ENOTDIR" => SystemError ENOTDIR
    "ENOTEMPTY" => SystemError ENOTEMPTY
    "ENOTFOUND" => SystemError ENOTFOUND
    "EPERM" => SystemError EPERM
    "EPIPE" => SystemError EPIPE
    "ETIMEDOUT" => SystemError ETIMEDOUT
    a => OtherCode a

export
data NodeError : Type where [external]

export
%foreign "node:lambda: e => e.message"
message : NodeError -> String

export
%foreign "node:lambda: e => e.stack"
stack : NodeError -> String

%foreign "node:lambda: e => e.code"
ffi_code : NodeError -> String

export
code : NodeError -> Code
code = fromString . ffi_code

max_stars_repo_name: kbertalan/tyttp

max_issues_repo_name: kbertalan/tyttp

max_forks_repo_name: kbertalan/tyttp


text:
||| Additional utility functions for the `Bifoldable` interface.
module Data.Bifoldable

%default total

||| Left associative monadic bifold over a structure.
public export
bifoldlM : Monad m => Bifoldable p =>
          (f: a -> b -> m a) ->
          (g: a -> c -> m a) ->
          (init: a) ->
          (input: p b c) -> m a
bifoldlM f g a0 = bifoldl (\ma,b => ma >>= flip f b)
                          (\ma,c => ma >>= flip g c)
                          (pure a0)

||| Combines the elements of a structure,
||| given ways of mapping them to a common monoid.
public export
bifoldMap : Monoid m => Bifoldable p => (a -> m) -> (b -> m) -> p a b -> m
bifoldMap f g = bifoldr ((<+>) . f) ((<+>) . g) neutral

||| Combines the elements of a structure using a monoid.
public export
biconcat : Monoid m => Bifoldable p => p m m -> m
biconcat = bifoldr (<+>) (<+>) neutral

||| Combines the elements of a structure,
||| given ways of mapping them to a common monoid.
public export
biconcatMap : Monoid m => Bifoldable p => (a -> m) -> (b -> m) -> p a b -> m
biconcatMap f g = bifoldr ((<+>) . f) ((<+>) . g) neutral

||| The conjunction of all elements of a structure containing lazy boolean
||| values.  `biand` short-circuits from left to right, evaluating until either an
||| element is `False` or no elements remain.
public export
biand : Bifoldable p => p (Lazy Bool) (Lazy Bool) -> Bool
biand = bifoldl (&&) (&&) True

||| The disjunction of all elements of a structure containing lazy boolean
||| values.  `bior` short-circuits from left to right, evaluating either until an
||| element is `True` or no elements remain.
public export
bior : Bifoldable p => p (Lazy Bool) (Lazy Bool) -> Bool
bior = bifoldl (||) (||) False

||| The disjunction of the collective results of applying a predicate to all
||| elements of a structure. `biany` short-circuits from left to right.
public export
biany : Bifoldable p => (a -> Bool) -> (b -> Bool) -> p a b -> Bool
biany f g = bifoldl (\x,y => x || f y) (\x,y => x || g y) False

||| The disjunction of the collective results of applying a predicate to all
||| elements of a structure.  `biall` short-circuits from left to right.
public export
biall : Bifoldable p => (a -> Bool) -> (b -> Bool) -> p a b -> Bool
biall f g = bifoldl (\x,y => x && f y) (\x,y => x && g y) True

||| Add together all the elements of a structure.
public export
bisum : Num a => Bifoldable p => p a a -> a
bisum = bifoldr (+) (+) 0

||| Add together all the elements of a structure.
||| Same as `bisum` but tail recursive.
export
bisum' : Num a => Bifoldable p => p a a -> a
bisum' = bifoldl (+) (+) 0

||| Multiply together all elements of a structure.
public export
biproduct : Num a => Bifoldable p => p a a -> a
biproduct = bifoldr (*) (*) 1

||| Multiply together all elements of a structure.
||| Same as `product` but tail recursive.
export
biproduct' : Num a => Bifoldable p => p a a -> a
biproduct' = bifoldl (*) (*) 1

||| Map each element of a structure to a computation, evaluate those
||| computations and discard the results.
public export
bitraverse_ :  (Bifoldable p, Applicative f)
            => (a -> f x)
            -> (b -> f y)
            -> p a b
            -> f ()
bitraverse_ f g = bifoldr ((*>) . f) ((*>) . g) (pure ())

||| Evaluate each computation in a structure and discard the results.
public export
bisequence_ : Applicative f => Bifoldable p => p (f a) (f b) -> f ()
bisequence_ = bifoldr (*>) (*>) (pure ())

||| Like `bitraverse_` but with the arguments flipped.
public export
bifor_ :  (Bifoldable p, Applicative f)
       => p a b
       -> (a -> f x)
       -> (b -> f y)
       -> f ()
bifor_ p f g = bitraverse_ f g p

||| Bifold using Alternative.
|||
||| If you have a left-biased alternative operator `<|>`, then `choice` performs
||| left-biased choice from a list of alternatives, which means that it
||| evaluates to the left-most non-`empty` alternative.
public export
bichoice : Alternative f => Bifoldable p => p (Lazy (f a)) (Lazy (f a)) -> f a
bichoice t = bifoldr {a = Lazy (f a)} {b = Lazy (f a)} {acc = Lazy (f a)}
                 (\ x, xs => x <|> xs)
                 (\ x, xs => x <|> xs)
                 empty
                 t

||| A fused version of `bichoice` and `bimap`.
public export
bichoiceMap : (Bifoldable p, Alternative f)
            => (a -> f x)
            -> (b -> f x)
            -> p a b ->
            f x
bichoiceMap fa fb t = bifoldr {a} {b} {acc = Lazy (f x)}
                        (\e, fx => fa e <|> fx)
                        (\e, fx => fb e <|> fx)
                        empty
                        t

ext: idr


text:
module NatUtils

import Order

%default total
%access public export

|||Proof of the type that an implication implies its contrapositive
impliesContrapositive : (a : Type) -> (b : Type) -> (a -> b) -> (Not b) -> (Not a)
impliesContrapositive a b aImpliesb bFalse x = bFalse (aImpliesb x)

|||Proof that m = n implies f m = f n
--Taken from Lecture.intro with modifications
--Prelude.Basics.cong serves the same function, use cong instead
functionExtendsEquality : (typ : Type) -> (f : typ -> typ) -> (n : typ) -> (m : typ) -> (n = m) -> (f n = f m)
functionExtendsEquality type f m m Refl = Refl

|||An injective predecessor "function"
predInjective : (n : Nat) -> (Not (n = Z)) -> (k ** (S k) = n)
predInjective Z proofNotZ = void (proofNotZ Refl)
predInjective (S k) _ = (k ** Refl)

|||Proof that Z is not equal to successor of any natural number
ZIsNotS : {n : Nat} -> (Not (Z = S n))
ZIsNotS {n} proofEq = SIsNotZ (sym proofEq)

|||difference of Nats, taken from Lecture.intro
sub : (a : Nat) -> (b : Nat) -> (LTE b a) -> Nat
sub a Z LTEZero = a
sub (S a) (S b) (LTESucc proofLTE) = sub a b proofLTE

|||Proof that the sum is greater than its parts
partsLTEsum : (LTE a (a + b), LTE b (a + b))
partsLTEsum {a = Z} {b} = (LTEZero, lteRefl)
partsLTEsum {a = S n} {b} = (LTESucc (fst(partsLTEsum)), lteSuccRight(snd(partsLTEsum)))

|||Proof that S a = S b implies a = b
--Same as succInjective, but implicit
predEqual : {a : Nat} -> {b : Nat} -> (S a = S b) -> (a = b)
predEqual Refl = Refl

|||Proof that a != b implies (S a) != (S b)
notEqualSucc : {a : Nat} -> {b : Nat} -> (Not (a = b)) -> (Not ((S a) = (S b)))
notEqualSucc {a} {b} proofNotEq proofEq = proofNotEq (predEqual proofEq)

|||Proof that (S a) != (S b) implies a != b
notEqualPred : {a : Nat} -> {b : Nat} -> (Not ((S a) = (S b))) -> (Not (a = b))
notEqualPred {a} {b} proofNotEq proofEq = proofNotEq (cong proofEq)

|||Proof that (a + b) = 0 implies a = 0 and b = 0
sumZeroImpliesZero : {a : Nat} -> {b : Nat} -> (a + b = Z) -> (a = Z, b = Z)
sumZeroImpliesZero {a = Z} {b = Z} Refl = (Refl, Refl)
sumZeroImpliesZero {a = Z} {b = S k} proofEq = void (SIsNotZ proofEq)
sumZeroImpliesZero {a = S k} {b} proofEq = void (SIsNotZ proofEq)

|||Proof that a + k = b and k != 0 implies a != b
nonZeroSumNotEqual : {a : Nat} -> {b : Nat} -> {k : Nat} -> (a + k = b) -> (Not (k = Z)) -> (Not (a = b))
nonZeroSumNotEqual {a} {b} {k} proofEq proofNotZ proofaEqb = proofNotZ kEqZ where
	kEqZ = (plusLeftCancel a k Z aPluskEqaPlusZ) where
		aPluskEqaPlusZ = (trans aPluskPlEqbPlusZ (sym ((cong {f = (\n => (n + Z))}) proofaEqb))) where
			aPluskPlEqbPlusZ = rewrite (plusZeroRightNeutral b) in proofEq

|||Proof that (S a) + b = a + (S b)
plusSymmetricInS : {a : Nat} -> {b : Nat} -> ((S a) + b = a + (S b))
plusSymmetricInS {a = Z} {b} = Refl
plusSymmetricInS {a = S k} {b} = cong (plusSymmetricInS {a = k} {b})

|||Proof that a = b implies c * a = c * b
multConstantLeft : {a : Nat} -> {b : Nat} -> (c : Nat) -> (a = b) -> ((c * a) = (c * b))
multConstantLeft {a} {b} Z _ = Refl
multConstantLeft {a} {b} (S k) proofEq =
	trans (cong {f = (\n => n + (k * a))} proofEq) (cong {f = (\n => b + n)} inductiveProofEq) where
		inductiveProofEq = multConstantLeft {a} {b} k proofEq

|||Proof that a = b implies a * c = b * c
multConstantRight : {a : Nat} -> {b : Nat} -> (c : Nat) -> (a = b) -> ((a * c) = (b * c))
multConstantRight {a} {b} c proofEq = rewrite (multCommutative a c) in
								rewrite (multCommutative b c) in
								multConstantLeft c proofEq

|||Proof that c * a != c * b implies a != b
multConstantLeftNot : {a : Nat} -> {b : Nat} -> {c : Nat} -> (Not ((c * a) = (c * b))) -> (Not (a = b))
multConstantLeftNot {a} {b} {c} proofNotEq proofEq = void (proofNotEq (cong {f = (\n => c * n)} proofEq))

|||Proof that a *c != b * c implies a != b
multConstantRightNot : {a : Nat} -> {b : Nat} -> {c : Nat} -> (Not ((a * c) = (b * c))) -> (Not (a = b))
multConstantRightNot {a} {b} {c} proofNotEq proofEq = void (proofNotEq (cong {f = (\n => n * c)} proofEq))

||| Proof that a = c, b = d and a <= b implies c <= d
lteSubstitutes : {a : Nat} -> {b : Nat} -> {c : Nat} -> {d : Nat} ->
				(LTE a b) -> (a = c) -> (b = d) -> (LTE c d)
lteSubstitutes proofLTE Refl Refl = proofLTE

|||Proof that a < b implies a <= b
ltImpliesLTE : {a : Nat} -> {b : Nat} -> (LT a b) -> (LTE a b)
ltImpliesLTE proofLTE = lteSuccLeft proofLTE

|||Proof that a = b implies a <= b
eqImpliesLTE : {a : Nat} -> {b : Nat} -> (a = b) -> (LTE a b)
eqImpliesLTE {a = Z} {b = Z} Refl = LTEZero
eqImpliesLTE {a = S k} {b = Z} proofEq = void(SIsNotZ proofEq)
eqImpliesLTE {a = Z} {b = S l} proofEq = void(SIsNotZ (sym proofEq))
eqImpliesLTE {a = S k} {b = S l} proofEq = LTESucc (eqImpliesLTE (predEqual proofEq))

|||The theorem that (a <= b) and (b <= a) implies a = b
lteAndGTEImpliesEqual : {a : Nat} -> {b : Nat} -> (LTE a b) -> (LTE b a) -> (a = b)
lteAndGTEImpliesEqual LTEZero LTEZero = Refl
lteAndGTEImpliesEqual (LTESucc a) (LTESucc b) = cong (lteAndGTEImpliesEqual a b)

|||Proof that a < b implies S a = b or S a < b
ltImpliesEqOrLT : (a : Nat) -> (b : Nat) -> (LT a b) -> Either (S a = b) (LT (S a) b)
ltImpliesEqOrLT Z (S Z) (LTESucc LTEZero) = Left Refl
ltImpliesEqOrLT Z (S (S b)) (LTESucc LTEZero) = Right (LTESucc (LTESucc LTEZero))
ltImpliesEqOrLT (S a) (S b) proofSaLTSb =
	case (ltImpliesEqOrLT a b (fromLteSucc proofSaLTSb)) of
		(Left proofSaEqb) => Left (cong proofSaEqb)
		(Right proofSaLTb) => Right (LTESucc proofSaLTb)

|||Proof that a <= b implies a <= (c + b)
ltePlusConstant : {a : Nat} -> {b : Nat} -> (c : Nat) -> (LTE a b) -> (LTE a (c + b))
ltePlusConstant {a} {b} c proofLTE = lteSubstitutes (lteTransitive proofLTE (lteAddRight b)) Refl (plusCommutative b c)

|||Proof that a <= b implies (c + a) <= (c + b)
ltePlusConstantLeft : {a : Nat} -> {b : Nat} -> (c : Nat) -> (LTE a b) -> (LTE (c + a) (c + b))
ltePlusConstantLeft Z proofLTE = proofLTE
ltePlusConstantLeft (S k) proofLTE = LTESucc (ltePlusConstantLeft k proofLTE)

|||Proof that a <= b implies (a + c) <= (b + c)
ltePlusConstantRight : {a : Nat} -> {b : Nat} -> (c : Nat) -> (LTE a b) -> (LTE (a + c) (b + c))
ltePlusConstantRight {a} {b} c proofLTE = rewrite (plusCommutative a c) in
									rewrite (plusCommutative b c) in
									(ltePlusConstantLeft c proofLTE)

|||Proof that (c + a) <= (c + b) implies a <= b
lteMinusConstantLeft : {a : Nat} -> {b : Nat} -> {c : Nat} -> (LTE (c + a) (c + b)) -> (LTE a b)
lteMinusConstantLeft {c = Z} proofLTE = proofLTE
lteMinusConstantLeft {c = S k} (LTESucc proofLTE) = lteMinusConstantLeft {c = k} proofLTE

|||Proof that (a + c) <= (b + c) implies a <= b
lteMinusConstantRight : {a : Nat} -> {b : Nat} -> {c : Nat} -> (LTE (a + c) (b + c)) -> (LTE a b)
lteMinusConstantRight {a} {b} {c} proofLTE =
	lteMinusConstantLeft (lteSubstitutes proofLTE (plusCommutative a c) (plusCommutative b c))

|||Proof that if a <= b, and c <= d, then (a + c) <= (b + d)
ltePlusIsLTE : {a : Nat} -> {b : Nat} -> {c : Nat} -> {d : Nat} ->
			(LTE a b) -> (LTE c d) -> (LTE (a + c) (b + d))
ltePlusIsLTE {a = a0} {b = b0} {c = c0} {d = d0} proofLeftLTE proofRightLTE =
	lteTransitive (ltePlusConstantRight {a = a0} {b = b0} c0 proofLeftLTE) (ltePlusConstantLeft {a = c0} {b = d0} b0 proofRightLTE)

|||Proof that m <= (S k) * m
lteMultLeft : (k : Nat) -> (m : Nat) -> (LTE m ((S k) * m))
lteMultLeft Z m = rewrite (multOneLeftNeutral m) in (lteRefl)
lteMultLeft (S k) m = ltePlusConstant m (lteMultLeft k m)

|||Proof that a <= b implies (c * a) <= (c * b)
lteMultConstantLeft : {a : Nat} -> {b : Nat} -> (c : Nat) -> (LTE a b) -> (LTE (c * a) (c * b))
lteMultConstantLeft {a} {b} Z _ = LTEZero
lteMultConstantLeft {a} {b} (S k) proofLTE =
	ltePlusIsLTE proofLTE (lteMultConstantLeft {a} {b} k proofLTE)

|||Proof that a <= b implies (a * c) <= (b * c)
lteMultConstantRight : {a : Nat} -> {b : Nat} -> (c : Nat) -> (LTE a b) -> (LTE (a * c) (b * c))
lteMultConstantRight {a} {b} c proofLTE = rewrite (multCommutative a c) in
									rewrite (multCommutative b c) in
									(lteMultConstantLeft c proofLTE)

|||Proof that if a <= b, and c <= d, then (a * c) <= (b * d)
lteMultIsLTE : {a : Nat} -> {b : Nat} -> {c : Nat} -> {d : Nat} ->
			(LTE a b) -> (LTE c d) -> (LTE (a * c) (b * d))
lteMultIsLTE {a = a0} {b = b0} {c = c0} {d = d0} proofLeftLTE proofRightLTE =
	lteTransitive (lteMultConstantRight {a = a0} {b = b0} c0 proofLeftLTE) (lteMultConstantLeft {a = c0} {b = d0} b0 proofRightLTE)

|||Proof that n is not lesser than n
succNotLTEn : {n : Nat} -> (LT n n) -> Void
succNotLTEn {n = Z} proofLTE = void (succNotLTEzero proofLTE)
succNotLTEn {n = S k} (LTESucc proofLTE) = succNotLTEn {n = k} proofLTE

|||Proof that a < b implies a != b and !(b < a)
ltImpliesNotEqNotGT : {a : Nat} -> {b : Nat} -> (LT a b) -> (Not (a = b), Not (LT b a))
ltImpliesNotEqNotGT {a} {b = Z} proofLT = void(succNotLTEzero proofLT)
ltImpliesNotEqNotGT {a = Z} {b = S l} proofLT = (ZIsNotS, succNotLTEzero)
ltImpliesNotEqNotGT {a = S k} {b = S l} (LTESucc proofLT) =
	((\proofEq => inductionStep1 (predEqual proofEq)), (\proofLT => inductionStep2 (lteMinusConstantLeft {c = 1} proofLT))) where
		inductionStep1 = fst (ltImpliesNotEqNotGT {a = k} {b = l} proofLT)
		inductionStep2 = snd (ltImpliesNotEqNotGT {a = k} {b = l} proofLT)

|||Proof that a = b implies !(a < b) and !(b < a)
eqImpliesNotLTNotGT : {a : Nat} -> {b : Nat} -> (a = b) -> (Not (LT a b), Not (LT b a))
eqImpliesNotLTNotGT {a = k} {b = k} Refl = (succNotLTEn, succNotLTEn)

|||Proof that a*b = a*c implies b = c
multLeftCancel : (left : Nat) -> (right : Nat) -> (right1 : Nat) -> Not(left = 0) -> (left*right = left*right1) -> (right = right1)
multLeftCancel Z _ _ pfnotz _ = void (pfnotz Refl)
multLeftCancel (S Z) right right1 SIsNotZ pfrefl =  rewrite (sym (multOneLeftNeutral right)) in
																										rewrite (sym (multOneLeftNeutral right1)) in
																										pfrefl
multLeftCancel (S (S k)) right right1 pf pfeq = ?fill

|||Proof that a not LTE b implies b LTE a
-- taken from Lecture.GCD
switchLTE : (n: Nat) -> (m: Nat) -> (contra : (LTE n m) -> Void) -> LTE m n
switchLTE Z m contra = void (contra (LTEZero))
switchLTE (S k) Z contra = LTEZero
switchLTE (S k) (S j) contra =
  LTESucc (switchLTE k j previousContra) where
    previousContra = \evidence : (LTE k j) => contra (LTESucc evidence)

|||Returns Max of two numbers with proof that it is maximum
max : (a : Nat) -> (b : Nat) -> (n : Nat ** ((LTE a n, LTE b n), Either (a=n) (b=n)))
max a b = case isLTE a b of
	(Yes prf) => (b ** ((prf, lteRefl), (Right Refl)))
	(No contra) => (a ** ((lteRefl, (switchLTE a b contra)), (Left Refl)))


text:
module BigStep

-- Relation 'BigStep' for fully reducing terms
-- in the untyped lambda calculus to values.

import Term
import Subst

%default total
%access public export

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

-- The relation 'BigStep' defines evaluation of terms in the lambda
-- calculus following big-step semantics.
--
-- Big-step semantics fully evaluates terms to values.
-- (A proof of this statement appears below.)
data BigStep : Term 0 -> (y: Term 0) -> Type where
  BStValue    : (v : Value e) -> BigStep e e
  --
  BStApp      : BigStep e1 (TAbs e1') ->
                BigStep e2 e2' ->
                BigStep (subst e2' FZ e1') e ->
                BigStep (TApp e1 e2) e
  --
  BStSucc     : BigStep e e' ->
                BigStep (TSucc e) (TSucc e')
  --
  BStPredZero : BigStep e TZero ->
                BigStep (TPred e) TZero
  --
  BStPredSucc : BigStep e (TSucc e') ->
                BigStep (TPred e) e'
  --
  BStIfzZero  : BigStep e1 TZero ->
                BigStep e2 e ->
                BigStep (TIfz e1 e2 _) e
  --
  BStIfzSucc  : BigStep e1 (TSucc _) ->
                BigStep e3 e ->
                BigStep (TIfz e1 _ e3) e

bigStepFst : {e : Term 0} -> BigStep e _ -> Term 0
bigStepFst {e = e} _ = e

bigStepSnd : {e : Term 0} -> BigStep _ e -> Term 0
bigStepSnd {e = e} _ = e

bigStepValue : BigStep _ e -> Value e
bigStepValue (BStValue v)     = v
bigStepValue (BStApp _ _ z)   = bigStepValue z
bigStepValue (BStSucc z)      = VSucc (bigStepValue z)
bigStepValue (BStPredZero _)  = VZero
bigStepValue (BStPredSucc z)  = case bigStepValue z of
                                     VZero impossible
                                     VSucc v => v
bigStepValue (BStIfzZero _ z) = bigStepValue z
bigStepValue (BStIfzSucc _ z) = bigStepValue z

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

max_stars_repo_name: normanrink/PCF

max_issues_repo_name: normanrink/PCF

max_forks_repo_name: normanrink/PCF


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

||| The intermediate representation for GRL-Derived Languages.
module GRL.IR

import GRL.Common

%access export
-- ---------------------------------------------------------- [ AST Definition ]

||| An IR to aid in converting DSL language constructs into Goal Graph
||| objects.
public export
data GExpr : GTy -> Type where
  Elem  : GElemTy -> String
       -> Maybe SValue -> GExpr ELEM

  ILink : GIntentTy -> CValue
       -> GExpr ELEM -> GExpr ELEM -> GExpr INTENT

  SLink : GStructTy -> GExpr ELEM
        -> List (GExpr ELEM) -> GExpr STRUCT

getTitle : GExpr ELEM -> String
getTitle (Elem ty t s) = t

-- -------------------------------------------------------------------- [ Show ]

private
shGExprE : GExpr ELEM -> String
shGExprE (Elem ty t ms) = with List unwords ["[Element", show ty, show t, show ms,"]"]

private
shGExprI : GExpr INTENT -> String
shGExprI (ILink ty cty a b) = with List unwords ["[Intent", show ty, show cty, shGExprE a, shGExprE b, "]"]

private
shGExprS : GExpr STRUCT -> String
shGExprS (SLink ty x ys) = with List unwords ["[Structure", show ty, shGExprE x, show' ys, "]"]
  where
    show' : List (GExpr ELEM) -> String
    show' ys = "[" ++ (unwords $ intersperse "," (map shGExprE ys)) ++ "]"

private
shGExpr : {ty : GTy} -> GExpr ty -> String
shGExpr {ty=ELEM}   x = shGExprE x
shGExpr {ty=INTENT} x = shGExprI x
shGExpr {ty=STRUCT} x = shGExprS x

Show (GExpr ty) where
  show x = shGExpr x

-- ------------------------------------------------------------- [ Eq Instance ]

private
eqGExprE : GExpr ELEM -> GExpr ELEM -> Bool
eqGExprE (Elem xty x sx) (Elem yty y sy) = xty == yty && x == y && sx == sy

private
eqGExprI : GExpr INTENT -> GExpr INTENT -> Bool
eqGExprI (ILink xty xc xa xb) (ILink yty yc ya yb) = xty == yty && xc == yc && eqGExprE xa ya && eqGExprE xb yb

private
eqGExprS : GExpr STRUCT -> GExpr STRUCT -> Bool
eqGExprS (SLink xty xa (xbs)) (SLink yty ya (ybs)) =
      xty == yty && eqGExprE xa ya && eqGExprList xbs ybs
    where
      eqGExprList : List (GExpr ELEM) -> List (GExpr ELEM) -> Bool
      eqGExprList Nil Nil = True
      eqGExprList (x::xs) (y::ys) =
        if eqGExprE x y
          then (eqGExprList (assert_smaller (x::xs) xs) (assert_smaller (y::ys) ys))
          else False
      eqGExprList _       _       = False

export
eqGExpr : GExpr a -> GExpr b -> Bool
eqGExpr {a=ELEM}   {b=ELEM}   x y = eqGExprE x y
eqGExpr {a=INTENT} {b=INTENT} x y = eqGExprI x y
eqGExpr {a=STRUCT} {b=STRUCT} x y = eqGExprS x y
eqGExpr _          _          = False

Eq (GExpr ty) where
  (==) x y = eqGExpr x y

||| The GRL Class for allowing DSL designers to instruct the Goal
||| Graph builder how to convert expressions in the DSL to the IR.
|||
||| @a The DSL which is indexed by `GTy` type.
public export
interface GRL (a : GTy -> Type) where
  ||| Instruct the interpreter to construct a goal node.
  mkElem   : a ELEM   -> GExpr ELEM
  ||| Intruct the interpreter to construct a intent link.
  mkIntent : a INTENT -> GExpr INTENT
  ||| Instruct the interpreter to consturct a structural link.
  mkStruct : a STRUCT -> GExpr STRUCT

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

max_stars_repo_name: jfdm/idris-grl

max_issues_repo_name: jfdm/idris-grl

max_forks_repo_name: jfdm/idris-grl


text:
--- --------------------------------------------------------------- [ Types.idr ]
-- Module      : XML.XPath.Types
-- Copyright   : (c) Jan de Muijnck-Hughes
-- License     : see LICENSE
--
-- Types for an XPath EDSL.
-- --------------------------------------------------------------------- [ EOH ]
module XML.XPath.Types

import public Commons.Data.Location
import public Commons.Text.Lexer.Run
import public Commons.Text.Parser.Support
import public Commons.Text.Parser.Run

import XML.DOM

%default total
%access public export

public export
data Token = ReservedNode String
           | UserNode String
           | Symbol String
           | WS String
           | NotRecog String
           | EndInput

public export
Eq Token where
  (==) (ReservedNode x) (ReservedNode y) = x == y
  (==) (UserNode x) (UserNode y) = x == y
  (==) (Symbol x) (Symbol y) = x == y
  (==) (NotRecog x) (NotRecog y) = x == y
  (==) EndInput EndInput = True
  (==) _ _ = False

public export
Show Token where
  show (ReservedNode s) = "(ReservedNode " ++ s ++ ")"
  show (UserNode s) = "(UserNode " ++ s ++ ")"
  show (Symbol s) = "(Symbol " ++ s ++ ")"
  show (WS s) = "(WS " ++ s ++ ")"
  show (NotRecog s) = "(NotRecog " ++ s ++ ")"
  show (EndInput) = "EndInput"

data XPathTy = NODE | PATH | QUERY | ROOT | TEST Bool

data ValidPath : (head : XPathTy) -> (tail : XPathTy) -> Type where
  AbsPathRoot      : ValidPath ROOT NODE
  AbsPath          : ValidPath ROOT PATH
  AbsPathEnd       : ValidPath ROOT (TEST b)
  ValidSubEnd      : ValidPath NODE (TEST b)
  ValidSubPath     : ValidPath NODE NODE
  ValidSubPathPath : ValidPath NODE PATH

infixl 2 </>
infixl 2 <//>

||| Add anynode for singular case '//node'
||| Attributes
||| Predicates
data XPath : NodeTy -> XPathTy -> Type where
  ||| An XPath Query
  Query : XPath ty a -> XPath ty QUERY

  Any  : XPath ELEMENT NODE
  Elem : String -> XPath ELEMENT NODE

  Attr    : String -> XPath TEXT (TEST True)
  Text    : XPath TEXT    (TEST False)
  Comment : XPath COMMENT (TEST False)
  CData   : XPath CDATA   (TEST False)

  Root  : XPath ELEMENT NODE -> XPath ELEMENT ROOT
  DRoot : XPath ELEMENT NODE -> XPath ELEMENT ROOT

  ||| An absolute path
  PathA : XPath ELEMENT a
       -> XPath tyB b
       -> (prf : ValidPath a b)
       -> XPath tyB PATH
  ||| Get decendants
  PathD : XPath ELEMENT a
       -> XPath tyB b
       -> (prf : ValidPath a b)
       -> XPath tyB PATH

(</>) : XPath ELEMENT a
     -> XPath tyB b
     -> {auto prf : ValidPath a b}
     -> XPath tyB PATH
(</>) a b {prf} = PathA a b prf

(<//>) : XPath ELEMENT a
      -> XPath tyB b
      -> {auto prf : ValidPath a b}
      -> XPath tyB PATH
(<//>) a b {prf} = PathD a b prf

Show (XPath ty x) where
  show (Query q) = unwords ["[Query ", show q, "]\n"]
  show (Elem e)  = e
  show (Any)     = "*"
  show (Root r)  = "/" ++ show r
  show (DRoot r) = "//" ++ show r
  show (Attr a)  = "@" ++ a
  show (Text)    = "text()"
  show (Comment) = "comment()"
  show (CData)   = "cdata()"
  show (PathA p c prf) = show p ++ "/" ++ show c
  show (PathD p c prf) = show p ++ "//" ++ show c

-- ------------------------------------------------------------------- [ ERROR ]

data XPathError : Type where
  MalformedQuery : (qstr : String) -> Run.ParseError Token -> XPathError
  QueryError     : (qstr : XPath ty a) -> (loc : XMLElem) -> (msg : Maybe String) -> XPathError
  SingletonError : String -> XPathError
  GenericError   : String -> XPathError

showParseError : Run.ParseError Token -> String
showParseError (FError e) = show e
showParseError (PError e) = unlines [maybe "" show (location e), error e]
showParseError (LError (MkLexFail l i)) = unlines [show l, show i]

Show XPathError where
  show (MalformedQuery q err) = unwords
    [ "Query:"
    , show q
    , "is malformed because"
    , showParseError err
    ]

  show (QueryError qstr loc msg) = unlines
    [ unwords ["QueryError:", fromMaybe "" msg]
    , "Asking for:"
    , unwords ["\t", show qstr]
    , "in"
    , unwords ["\t", (getTagName loc)]]
  show (GenericError msg) = unwords ["Generic Error:", msg]
  show (SingletonError m) = unwords ["At Least one node expected.", show m]
-- --------------------------------------------------------------------- [ EOF ]

max_stars_repo_name: jfdm/idris-xml

max_issues_repo_name: jfdm/idris-xml

max_forks_repo_name: jfdm/idris-xml


text:
||| Manual test:
||| since times (naturally) vary between runs, this can only be verified by manually inspecting the output
import System.Clock

main : IO ()
main = do
  printLn !(clockTime UTC)
  printLn !(clockTime Monotonic)
  printLn !(clockTime Duration)
  printLn !(clockTime Process)
  printLn !(clockTime Thread)
  printLn !(clockTime GCCPU)
  printLn !(clockTime GCReal)

max_stars_repo_name: boxfire/rapid

max_issues_repo_name: boxfire/rapid

max_forks_repo_name: boxfire/rapid


text:
interface Queue (q: Type -> Type) where
  empty : q a
  isEmpty : q a -> Bool
  snoc : q a -> a -> q a
  head : q a -> a
  tail : q a -> q a

data CatList : (Type -> Type) -> Type -> Type where
  E : CatList q a
  C : {0 q : Type -> Type} -> a -> q (Lazy (CatList q a)) -> CatList q a

link : (Queue q) => CatList q a -> Lazy (CatList q a) -> CatList q a
link E s = s -- Just to satisfy totality for now.
link (C x xs) s = C x (snoc xs s)


text:
module Tests

import System
import Language.JSON.Decode

test : String -> (() -> Either String Bool) -> IO ()
test name f = do
    putStrLn $ "Test: " ++ name
    case f () of
        Right _ => putStrLn "OK"
        Left err => do
            putStrLn $ "Failed: " ++ err
            exit 1

testInt : Bool -> String -> Either String Bool
testInt val str =
    case (val, Language.JSON.Decode.decodeString int str) of
        (True, Right v) => Right True
        (True, Left err) => Left err
        (False, Left err) => Right False
        (False, Right v) => Left $ "Expected to fail but succeeded: " ++ str

intTests : IO ()
intTests = do
    test "whole int" $ \() => testInt True "4"
    test "-whole int" $ \() => testInt True "-4"
    test "whole float" $ \() => testInt True "4.0"
    test "-whole float" $ \() => testInt True "-4.0"
    test "large int" $ \() => testInt True "1801439850948"
    test "-large int" $ \() => testInt True "-1801439850948"
    test "float" $ \() => testInt False "4.2"
    test "-float" $ \() => testInt False "-4.2"
    test "Infinity" $ \() => testInt False "Infinity"
    test "-Infinity" $ \() => testInt False "-Infinity"
    test "NaN" $ \() => testInt False "NaN"
    test "-NaN" $ \() => testInt False "-NaN"
    test "true" $ \() => testInt False "true"
    test "false" $ \() => testInt False "false"
    test "string" $ \() => testInt False "\"string\""
    test "object" $ \() => testInt False "{}"
    test "null" $ \() => testInt False "null"
    test "undefined" $ \() => testInt False "undefined"

customTests : IO ()
customTests =
    test "customDecoder preserves user error messages" $ \() => assertion
    where
        jsonString : String
        jsonString = "{ \"foo\": \"bar\" }"

        customErrorMessage : String
        customErrorMessage = "I want to see this message!"

        myDecoder : Decoder Int
        myDecoder = andThen (\foo => fail customErrorMessage) (field "foo" string)

        assertion : Either String Bool
        assertion =
            case decodeString myDecoder jsonString of
                Right _ =>
                    Left $ "expected `customDecoder` to produce Left, but got Right"

                Left message =>
                    if isInfixOf customErrorMessage message then
                        Right True
                    else
                        Left $
                            "expected `customDecoder` to preserve user's error message '"
                                ++ customErrorMessage
                                ++ "', but instead got: "
                                ++ message

export
tests : IO ()
tests = do
    intTests
    --customTests

max_stars_repo_name: brainrape/idris-json-decode

max_issues_repo_name: brainrape/idris-json-decode

max_forks_repo_name: brainrape/idris-json-decode


text:
-- ---------------------------------------------- [ DependentStateMachines.idr ]
-- Module      : Exercises.DependentStateMachines
-- Description : Solutions to the Chapter 14 exercises in Edwin Brady's
--               book, "Type-Driven Development with Idris."
-- --------------------------------------------------------------------- [ EOH ]
module Exercises.DependentStateMachines

import public Chapter.DependentStateMachines

-- -------------------------------------------------------- [ 14.2.5 Exercises ]

%access public export

data Access = LoggedOut | LoggedIn
data PwdCheck = Correct | Incorrect

data ShellCmd  : (ty : Type) -> Access -> (ty -> Access) -> Type where
     Password  : String -> ShellCmd PwdCheck LoggedOut
                                             (\res => case res of
                                                           Correct => LoggedIn
                                                           Incorrect => LoggedOut)
     Logout    : ShellCmd () LoggedIn (const LoggedOut)
     GetSecret : ShellCmd String LoggedIn (const LoggedIn)

     PutStr    : String -> ShellCmd () state (const state)
     Pure      : (res : ty) -> ShellCmd ty (state_fn res) state_fn
     (>>=)     : ShellCmd a state1 state2_fn ->
                 ((res : a) -> ShellCmd b (state2_fn res) state3_fn) ->
                 ShellCmd b state1 state3_fn

%access export

session : ShellCmd () LoggedOut (const LoggedOut)
session = do Correct <- Password "wurzel"
               | Incorrect => PutStr "Wrong password"
             PutStr $ "Secret code: " ++ show !GetSecret ++ "\n"
             Logout

-- NOTE: The following should not type check.
{-
bad_session : ShellCmd () LoggedOut (const LoggedOut)
bad_session = do Password "wurzel"
                 PutStr $ "Secret code: " ++ !GetSecret ++ "\n"
                 Logout

no_logout : ShellCmd () LoggedOut (const LoggedOut)
no_logout = do Correct <- Password "wurzel"
                 | Incorrect => PutStr "Wrong password"
               PutStr $ "Secret code: " ++ show !GetSecret ++ "\n"
-}

namespace DependentVendingMachine

    export
    VendState : Type
    VendState = (Nat, Nat)

    public export
    data Input = COIN
               | VEND
               | CHANGE
               | REFILL Nat

    data CoinResult = Inserted | Rejected

    public export
    data MachineCmd : (ty : Type) -> VendState -> (ty -> VendState) -> Type where

         InsertCoin : MachineCmd CoinResult (pounds, chocs)
                                 (\res => case res of
                                               Inserted => (S pounds, chocs)
                                               Rejected => (pounds, chocs))

         Vend : MachineCmd () (S pounds, S chocs) (const (pounds, chocs))

         GetCoins : MachineCmd () (pounds, chocs) (const (Z, chocs))

         Refill : (bars : Nat) -> MachineCmd () (Z, chocs)
                                             (const (Z, bars + chocs))

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

         GetInput : MachineCmd (Maybe Input) state (const state)

         Pure : (res : ty) -> MachineCmd ty (state_fn res) state_fn

         (>>=) : MachineCmd a state1 state2_fn ->
                 ((res : a) -> MachineCmd b (state2_fn res) state3_fn) ->
                 MachineCmd b state1 state3_fn

    public export
    data MachineIO : VendState -> Type where
         Do : MachineCmd a state1 state2_fn ->
              ((res : a) -> Inf (MachineIO (state2_fn res))) -> MachineIO state1

namespace MachineDo

    public export
    (>>=) : MachineCmd a state1 state2_fn ->
            ((res : a) -> Inf (MachineIO (state2_fn res))) -> MachineIO state1
    (>>=) = Do

-- --------------------------------------- [ 13.1.4 A Verified Vending Machine ]

mutual

  vend : MachineIO (pounds, chocs)
  vend {pounds = S _} {chocs = S _} = do Vend
                                         Display "Enjoy!"
                                         machineLoop
  vend {pounds = Z}                 = do Display "Insert a coin"
                                         machineLoop
  vend {chocs = Z}                  = do Display "Out of stock"
                                         machineLoop

  refill : (num : Nat) -> MachineIO (pounds, chocs)
  refill {pounds = Z} num = do Refill num
                               machineLoop
  refill _                = do Display "Can't refill: Coins in machine"
                               machineLoop

  machineLoop : MachineIO (pounds, chocs)
  machineLoop =
      do Just x <- GetInput
           | Nothing => do Display "Invalid input"
                           machineLoop
         case x of
              COIN       => do Inserted <- InsertCoin
                                 | Rejected => do Display "Coin rejected"
                                                  machineLoop
                               Display "Coin inserted"
                               machineLoop
              VEND       => vend
              CHANGE     => do GetCoins
                               Display "Change returned"
                               machineLoop
              REFILL num => refill num

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

max_stars_repo_name: yurrriq/tdd-with-idris

max_issues_repo_name: yurrriq/tdd-with-idris

max_forks_repo_name: yurrriq/tdd-with-idris


text:
module Ui

import Command
import State
import World
import Terminal
import Data.Vect

%default total

export
setup : IO ()
setup = do
  setRaw
  hideCursor

export
tearDown : IO ()
tearDown = do
  showCursor

showTile : Nat -> Nat -> Tile -> IO ()
showTile x y tile = do
  moveCursor (S x) (S y)
  case tile of
    Empty => do
      setColour White
      putStr "."
    Wall => do
      setColour BrightBlack
      putStr "x"
    Finish => do
      setColour Green
      putStr "x"

showColumn : Vect ylimit Tile -> Nat -> Nat -> IO ()
showColumn Nil _ _ = pure ()
showColumn (tile :: rest) x y = do
  showTile x y tile
  showColumn rest x (S y)

showColumns : Vect cols (Vect rows Tile) -> Nat -> IO ()
showColumns Vect.Nil _ = pure ()
showColumns (col::rest) x = do
  showColumn col x Z
  showColumns rest (S x)

showTurtle : Turtle xlimit ylimit -> IO ()
showTurtle (MkTurtle x y heading) =
  let turtleChar = case heading of
                     North => '^'
                     South => 'v'
                     West => '<'
                     East => '>'
   in do
    setColour Yellow
    moveCursor (S (finToNat x)) (S (finToNat y))
    putChar turtleChar

commandToChar : Command -> Char
commandToChar TurnLeft = '<'
commandToChar TurnRight = '>'
commandToChar Forward = '^'

showProgram : List Command -> Nat -> IO ()
showProgram commands row =
  let commandString = pack $ map commandToChar commands
   in do
      setColour Blue
      moveCursor Z (S row)
      putStrLn commandString

rows : Vect xlimit (Vect ylimit a) -> Nat
rows _ {ylimit} = ylimit

export
showState : State -> IO ()
showState (MkState (MkWorld turtle grid) program) = do
  clearScreen
  showColumns grid Z
  showTurtle turtle
  showProgram program (rows grid)

max_stars_repo_name: PeterHajdu/tulis

max_issues_repo_name: PeterHajdu/tulis

max_forks_repo_name: PeterHajdu/tulis


text:
module Minecraft.Core.Item.Put

import public Minecraft.Core.Item
import public Minecraft.Core.Tangible
import public Minecraft.Data.Type.As

%default total

public export
interface Item self => Put (self : Type) where
  putItem : self -> As Tangible

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


text:
import Interfaces

infixr 7 :::
infixr 7 +++

data MyList : (a : Type) -> Type where
  MyNil : MyList a
  (:::) : a -> MyList a -> MyList a

data ListEq : list1 -> list2 -> Type where
  nilEq : ListEq MyNil MyNil
  consEq : (headEqPrf : x = y) -> (tailEqPrf : ListEq xs ys) -> ListEq (x ::: xs) (y ::: ys)

(+++) : (xlist : MyList a) -> (ylist : MyList a) -> MyList a
(+++) MyNil ylist = ylist
(+++) xlist MyNil = xlist
(+++) (x ::: xs) ylist = x ::: (xs +++ ylist)

listEqReflexive : {xlist : MyList a} -> xlist `ListEq` xlist
listEqReflexive {xlist = MyNil} = nilEq
listEqReflexive {xlist = (x ::: xs)} = consEq Refl listEqReflexive

listEqSymmetry : {xlist, ylist : MyList a} -> xlist `ListEq` ylist -> ylist `ListEq` xlist
listEqSymmetry {xlist = MyNil} {ylist = MyNil} nilEq = nilEq
listEqSymmetry {xlist = MyNil} {ylist = (x ::: y)} xlist_eq_ylist impossible
listEqSymmetry {xlist = (x ::: xs)} {ylist = MyNil} xlist_eq_ylist impossible
listEqSymmetry {xlist = (x ::: xs)} {ylist = (y ::: ys)} (consEq headEqPrf tailEqPrf) =
  consEq (sym headEqPrf) (listEqSymmetry tailEqPrf)

listEqTransitive : {xlist, ylist, zlist : MyList a} -> xlist `ListEq` ylist -> ylist `ListEq` zlist -> xlist `ListEq` zlist
listEqTransitive {xlist = MyNil} {ylist = MyNil} {zlist = MyNil} nilEq ylist_eq_zlist = ylist_eq_zlist
listEqTransitive {xlist = MyNil} {ylist = MyNil} {zlist = (x ::: y)} nilEq ylist_eq_zlist impossible
listEqTransitive {xlist = (x:::xs)} {ylist = (y:::ys)} {zlist = MyNil} (consEq headEqPrf tailEqPrf) ylist_eq_zlist impossible
listEqTransitive {xlist = (x:::xs)} {ylist = (y:::ys)} {zlist = (z:::zs)} (consEq x_eq_y xs_eq_ys) (consEq y_eq_z ys_eq_zs) =
  consEq (rewrite x_eq_y in y_eq_z) (listEqTransitive xs_eq_ys ys_eq_zs)

mapList : (f : a -> b) -> (xs : MyList a) -> MyList b
mapList f MyNil = MyNil
mapList f (x ::: xs) = f x ::: mapList f xs

listFunctorLawIdentity : (xlist : MyList a) -> mapList Prelude.id xlist `ListEq` xlist
listFunctorLawIdentity MyNil = nilEq
listFunctorLawIdentity (x ::: xs) = consEq Refl (listFunctorLawIdentity xs)

listFunctorLawComposition : (v : b -> c) -> (u : a -> b) -> (xlist : MyList a) -> mapList (v . u) xlist `ListEq` mapList v (mapList u xlist)
listFunctorLawComposition v u MyNil = nilEq
listFunctorLawComposition v u (x ::: xs) = consEq Refl (listFunctorLawComposition v u xs)

MyFunctor MyList where
  equalsTo = ListEq
  eqReflexive = listEqReflexive
  eqSymmetry = listEqSymmetry
  eqTransitive = listEqTransitive
  myMap = mapList
  functorLawIdentity = listFunctorLawIdentity
  functorLawComposition = listFunctorLawComposition

returnList : a -> MyList a
returnList x = x ::: MyNil

infixl 1 >>>==

(>>>==) : (xlist : MyList a) -> (f : a -> MyList b) -> MyList b
MyNil >>>== f = MyNil
(x ::: xs) >>>== f = f x +++ (xs >>>== f)

listMonadLawIdentityLeftLemma : (z : MyList b) -> ListEq (z +++ MyNil) z
listMonadLawIdentityLeftLemma MyNil = nilEq
listMonadLawIdentityLeftLemma (z ::: zs) = consEq Refl listEqReflexive

listMonadLawIdentityLeft : (x : a) -> (f : a -> MyList b) -> (returnList x >>>== f) `ListEq` (f x)
listMonadLawIdentityLeft x f = listMonadLawIdentityLeftLemma (f x)

listTwoEqLemma : (z : a) -> (xlist : MyList a) -> (ylist : MyList a) -> (xlist_eq_ylist : ListEq xlist ylist) -> ListEq ((z ::: MyNil) +++ ylist) (z ::: xlist)
listTwoEqLemma z MyNil MyNil nilEq = consEq Refl nilEq
listTwoEqLemma _ MyNil (_ ::: _) nilEq impossible
listTwoEqLemma _ MyNil (_ ::: _) (consEq headEqPrf tailEqPrf) impossible
listTwoEqLemma _ (_ ::: _) MyNil nilEq impossible
listTwoEqLemma _ (_ ::: _) MyNil (consEq headEqPrf tailEqPrf) impossible
listTwoEqLemma z (x ::: xs) (y ::: ys) (consEq headEqPrf tailEqPrf) = consEq Refl (consEq (sym headEqPrf) (listEqSymmetry tailEqPrf))

listMonadLawIdentityRight : (n : MyList a) -> (n >>>== (::: MyNil)) `ListEq` n
listMonadLawIdentityRight MyNil = nilEq
listMonadLawIdentityRight (x ::: xs) = listTwoEqLemma x xs (xs >>>== (::: MyNil)) (listEqSymmetry $ listMonadLawIdentityRight xs)

listAppendNilLemma : (xlist : MyList a) -> xlist `ListEq` (xlist +++ MyNil)
listAppendNilLemma MyNil = nilEq
listAppendNilLemma (x ::: xs) = listEqReflexive

replaceLeft : (xlist : MyList a) -> (ylist : MyList a) -> (zlist : MyList a) -> (xlist_eq_ylist : ListEq xlist ylist) ->
              ListEq (xlist +++ zlist) (ylist +++ zlist)
replaceLeft MyNil MyNil MyNil nilEq = nilEq
replaceLeft MyNil MyNil (z ::: zs) nilEq = listEqReflexive
replaceLeft MyNil (_ ::: _) MyNil nilEq impossible
replaceLeft MyNil (_ ::: _) MyNil (consEq headEqPrf tailEqPrf) impossible
replaceLeft MyNil (_ ::: _) (_ ::: _) nilEq impossible
replaceLeft MyNil (_ ::: _) (_ ::: _) (consEq headEqPrf tailEqPrf) impossible
replaceLeft (_ ::: _) MyNil MyNil nilEq impossible
replaceLeft (_ ::: _) MyNil MyNil (consEq headEqPrf tailEqPrf) impossible
replaceLeft (_ ::: _) MyNil (_ ::: _) nilEq impossible
replaceLeft (_ ::: _) MyNil (_ ::: _) (consEq headEqPrf tailEqPrf) impossible
replaceLeft (x ::: xs) (y ::: ys) MyNil (consEq headEqPrf tailEqPrf) = consEq headEqPrf tailEqPrf
replaceLeft (x ::: xs) (y ::: ys) (z ::: zs) (consEq headEqPrf tailEqPrf) = consEq headEqPrf (replaceLeft xs ys (z ::: zs) tailEqPrf)

replaceRight : (xlist : MyList a) -> (ylist : MyList a) -> (zlist : MyList a) -> (xlist_eq_ylist : ListEq ylist zlist) ->
              ListEq (xlist +++ ylist) (xlist +++ zlist)
replaceRight MyNil MyNil MyNil nilEq = nilEq
replaceRight MyNil MyNil (_ ::: _) nilEq impossible
replaceRight MyNil MyNil (_ ::: _) (consEq headEqPrf tailEqPrf) impossible
replaceRight MyNil (_ ::: _) MyNil nilEq impossible
replaceRight MyNil (_ ::: _) MyNil (consEq headEqPrf tailEqPrf) impossible
replaceRight MyNil (y ::: ys) (z ::: zs) (consEq headEqPrf tailEqPrf) = consEq headEqPrf tailEqPrf
replaceRight (x ::: xs) MyNil MyNil nilEq = listEqReflexive
replaceRight (_ ::: _) MyNil (_ ::: _) nilEq impossible
replaceRight (_ ::: _) MyNil (_ ::: _) (consEq headEqPrf tailEqPrf) impossible
replaceRight (_ ::: _) (_ ::: _) MyNil nilEq impossible
replaceRight (_ ::: _) (_ ::: _) MyNil (consEq headEqPrf tailEqPrf) impossible
replaceRight (x ::: xs) (y ::: ys) (z ::: zs) (consEq headEqPrf tailEqPrf) = consEq Refl (replaceRight xs (y ::: ys) (z ::: zs) (consEq headEqPrf tailEqPrf))

replaceBoth : (xlist : MyList a) -> (ylist : MyList a) -> (zlist : MyList a) -> (wlist : MyList a) -> (xlist_eq_zlist : ListEq xlist zlist) -> (ylist_eq_wlist : ListEq ylist wlist) ->
              ListEq (xlist +++ ylist) (zlist +++ wlist)
replaceBoth xlist ylist zlist wlist xlist_eq_zlist ylist_eq_wlist =
  (listEqReflexive `listEqTransitive` replaceLeft xlist zlist ylist xlist_eq_zlist) `listEqTransitive` replaceRight zlist ylist wlist ylist_eq_wlist

concatAssociative : (xlist : MyList a) -> (ylist : MyList a) -> (zlist : MyList a) ->
                    ListEq (xlist +++ ylist +++ zlist) ((xlist +++ ylist) +++ zlist)
concatAssociative MyNil MyNil MyNil = nilEq
concatAssociative MyNil MyNil (z ::: zs) = listEqReflexive
concatAssociative MyNil (y ::: ys) MyNil = listEqReflexive
concatAssociative MyNil (y ::: ys) (z ::: zs) = listEqReflexive
concatAssociative (x ::: xs) MyNil MyNil = listEqReflexive
concatAssociative (x ::: xs) MyNil (z ::: zs) = listEqReflexive
concatAssociative (x ::: xs) (y ::: ys) MyNil = listEqReflexive
concatAssociative (x ::: xs) (y ::: ys) (z ::: zs) = consEq Refl (concatAssociative xs (y ::: ys) (z ::: zs))

distributiveLaw : (z : a) -> (zs : MyList a) -> (x : a) -> (xs : MyList a) -> (g : a -> MyList b) ->
                           (induction_assumption : ListEq ((zs +++ (x ::: xs)) >>>== g) ((zs >>>== g) +++ ((x ::: xs) >>>== g))) ->
                           ListEq (g z +++ ((zs +++ (x ::: xs)) >>>== g)) (g z +++ (zs >>>== g) +++ ((x ::: xs) >>>== g))
distributiveLaw z zs x xs g induction_assumption =
  replaceRight (g z) ((zs +++ (x ::: xs)) >>>== g) ((zs >>>== g) +++ ((x ::: xs) >>>== g)) induction_assumption

--(((z ::: zs) +++ (x ::: xs)) >>>== g) -- distribute1
--(g z +++ ((zs +++ (x ::: xs)) >>>== g)) -- distributeIndctionLemma
--(g z +++ (zs >>>== g) +++ ((x ::: xs) >>>== g)) -- distribute 2
--(g z +++ (zs >>>== g) +++ g x +++ (xs >>>== g)) -- assosiativeLemma
--((g z +++ (zs >>>== g)) +++ (g x +++ (xs >>>== g))) -- distribute 3
--((z ::: zs) >>>== g) +++ ((x ::: xs) >>>== g)

listMonadLawCompositionLemma : (zlist : MyList a) -> (xlist : MyList a) -> (g : a -> MyList b) ->
                               ListEq ((zlist +++ xlist) >>>== g) ((zlist >>>== g) +++ (xlist >>>== g))
listMonadLawCompositionLemma MyNil MyNil g = nilEq
listMonadLawCompositionLemma MyNil (x ::: xs) g = listEqReflexive
listMonadLawCompositionLemma (z ::: zs) MyNil g = listAppendNilLemma (g z +++ (zs >>>== g))
listMonadLawCompositionLemma (z ::: zs) (x ::: xs) g =
  distributiveLaw z zs x xs g (listMonadLawCompositionLemma zs (x ::: xs) g) `listEqTransitive`
  concatAssociative (g z) (zs >>>== g) (g x  +++ (xs >>>== g))

--((x ::: xs) >>>== f) >>>== g
--(f x +++ (xs >>>== f)) >>>== g
--((f x) >>>== g) +++ ((xs >>>== f) >>>== g)
--((f x) >>>== g) +++ (xs >>>== \z => f z >>>== g)
--((x ::: MyNil) >>>== \z -> f z >>>== g) +++ (xs >>>== \z => f z >>>== g)
--((x ::: MyNil) +++ xs) >>>== \z => f z >>>= g
--(x ::: xs) >>>== \z => fz >>>= g

listMonadLawComposition : (xlist : MyList a) -> (f : a -> MyList b) -> (g : b -> MyList c) ->
                          ((xlist >>>== f) >>>== g) `ListEq` (xlist >>>== \z => f z >>>== g)
listMonadLawComposition MyNil f g = nilEq
listMonadLawComposition (x ::: xs) f g =
  (listMonadLawCompositionLemma (f x) (xs >>>== f) g `listEqTransitive`
  replaceRight (f x >>>== g) ((xs >>>== f) >>>== g) (xs >>>== (\z => f z >>>== g)) (listMonadLawComposition xs f g)) `listEqTransitive`
  listEqReflexive

MyMonad MyList where
  myReturn = returnList
  (>>>=) = (>>>==)
  monadLawIdentityLeft = listMonadLawIdentityLeft
  monadLawIdentityRight = listMonadLawIdentityRight
  monadLawComposition = listMonadLawComposition

max_stars_repo_name: yutaro-sakamoto/prove-monad

max_issues_repo_name: yutaro-sakamoto/prove-monad

max_forks_repo_name: yutaro-sakamoto/prove-monad


text:
module Extra.Alternative

import Data.List1
import public Extra.Applicative

infixl 2 <|>|

public export
interface Alternative f => LazyAlternative f where
  (<|>|) : f a -> Lazy (f a) -> f a

||| succeed multiple times until failure, and returns all the successful results
export
many : (LazyApplicative f, Alternative f) => f a -> f (List a)
many p = ((::) <$> p <*>| many p) <|> pure neutral

||| `many` but must succeed the first time
export
some : (LazyApplicative f, Alternative f) => f a -> f (List1 a)
some p = (:::) <$> p <*>| many p

export
sepBy : (LazyApplicative f, Alternative f) => f a -> f b -> f (List a)
sepBy parser seperator = (::) <$> parser <*>| ((seperator *>| sepBy parser seperator) <|> pure neutral)

||| `sepBy1` but must succeed the first time
export
sepBy1 : (LazyApplicative f, Alternative f) => f a -> f b -> f (List1 a)
sepBy1 parser seperator = (:::) <$> parser <*>| ((seperator *> sepBy parser seperator) <|> pure neutral)

export
manyTill : (LazyApplicative f, LazyAlternative f) => f a -> f b -> f (List a)
manyTill parser end = (end $> Nil) <|>| ((::) <$> parser <*>| manyTill parser end)

||| If the alternative fails, then defaults to a pure value
export
option : Alternative f => (defaultsTo : a) -> f a -> f a
option def f = f <|> pure def

||| If the alternative fails, return Nothing, otherwise return a Just
export
optional : Alternative f => f a -> f (Maybe a)
optional f = option Nothing (Just <$> f)


text:
import Data.Vect

tryIndex : Integer -> Vect n a -> Maybe a
tryIndex {n} i xs = case integerToFin i n of
                         Nothing => Nothing
                         (Just idx) => Just $ index idx xs


text:
import Data.Maybe

%default total

FromString Int where
  fromString x = cast x

test1 : Int
test1 = "42"

test2 : Int
test2 = "abc"

convert : String -> Maybe Bool
convert "True" = Just True
convert "False" = Just False
convert _ = Nothing

fromString : (str : String) -> {auto prf : IsJust (convert str)} -> Bool
fromString str {prf} with (convert str)
  fromString str {prf = ItIsJust} | (Just ret) = ret


text:
module Eq

import Data.List

%default total

occurrences : Eq ty => ty -> List ty -> Nat
occurrences _ [] = 0
occurrences v (x :: xs) = case v == x of
                               False => occurrences v xs
                               True => 1 + occurrences v xs

data Matter = Solid | Liquid | Gas

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

    (==) x y = not (x /= y)
    (/=) x y = not (x == y)

-}

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

data Tree elem = Empty | Node (Tree elem) elem (Tree elem)

Eq ty => Eq (Tree ty) where
  (==) Empty Empty = True
  (==) (Node l v r) (Node l' v' r') = l == l' && v == v' && r == r'
  (==) _ _  = False

partial
fromList : List ty -> Tree ty
fromList [] = Empty
fromList [x] = Node Empty x Empty
fromList (x :: xs) = Node (fromList left) x (fromList right)
         where
           len : Nat
           len = integerToNat $ (natToInteger (length xs)) `div` 2

           left : List ty
           left = take len xs

           right : List ty
           right = drop len xs

max_stars_repo_name: timmyjose-study/tdd-with-idris

max_issues_repo_name: timmyjose-study/tdd-with-idris

max_forks_repo_name: timmyjose-study/tdd-with-idris


text:
data ValidPassword : (min: Nat) -> (max: Nat) -> Type where
  MkPass: (xs: String) ->
          { auto p: length xs >= min && length xs <= max = True } ->
          ValidPassword min max

validPassword : ValidPassword 4 8
validPassword = MkPass "abcd"

invalidPassword : ValidPassword 4 8
invalidPassword = MkPass "abcd"

-- see https://github.com/hackle/idris/blob/master/range.idr

max_stars_repo_name: hackle/blogger

max_issues_repo_name: hackle/blogger

max_forks_repo_name: hackle/blogger


text:
module AOC.Day.Three

import AOC.Solution
import Data.Vect
import Data.String
import Data.Nat

%default total

----------------------------------------------------------------------------
-- Types -------------------------------------------------------------------
----------------------------------------------------------------------------

data Bit : Type where
  Low : Bit
  High : Bit

Binary : (n : Nat) -> Type
Binary n = Vect n Bit

InputType : Type
InputType = (m ** List (Binary m))

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

Show Bit where
  show Low = "0"
  show High = "1"

-- Could be more efficient with fold and cons but eh.
[BinaryShow] Show (Binary n) where
  show [] = ""
  show (x :: xs) = show x ++ show @{BinaryShow} xs

Cast Bit Nat where
  cast Low = 0
  cast High = 1

Cast Bit Integer where
  cast x = the Integer (cast (the Nat (cast x)))

Cast Nat (Maybe Bit) where
  cast 0 = Just Low
  cast 1 = Just High
  cast _ = Nothing

Cast Bool Bit where
  cast False = Low
  cast True  = High

Cast (Binary n) Nat where
  cast = foldl (\acc, x => acc * 2 + x) 0 . map cast

Cast (Binary n) Integer where
  cast x = the Integer (cast (the Nat (cast x)))

----------------------------------------------------------------------------
-- Helper Functions --------------------------------------------------------
----------------------------------------------------------------------------

countBit : Bit -> Integer -> Integer
countBit Low x = x - 1
countBit High x = x + 1

moreOf : {n : Nat} -> List (Binary n) -> Vect n Integer
moreOf {n} list = foldr (\x, acc => zipWith countBit x acc) (replicate n 0) list

mostCommon : Vect n Integer -> Binary n
mostCommon = map (cast . (> 0))

leastCommon : Vect n Integer -> Binary n
leastCommon = map (cast . (< 0))

----------------------------------------------------------------------------
-- Solutions ---------------------------------------------------------------
----------------------------------------------------------------------------

part1 : InputType -> String
part1 (m ** list) = show $ (cast . mostCommon $ mf) * (cast . leastCommon $ mf)
  where
    mf : Vect m Integer
    mf = moreOf list

----------------------------------------------------------------------------
-- Parsing Helper Functions ------------------------------------------------
----------------------------------------------------------------------------

toBinaryDep' : (s : List Char) -> Maybe (n ** Binary n)
toBinaryDep' [] = Just (0 ** [])
toBinaryDep' ('0' :: str) = (toBinaryDep' str) >>= (\(n ** bin) => Just $ (S n ** Low :: bin))
toBinaryDep' ('1' :: str) = (toBinaryDep' str) >>= (\(n ** bin) => Just $ (S n ** High :: bin))
toBinaryDep' _ = Nothing

toBinaryDep : (s : String) -> Maybe (n ** Binary n)
toBinaryDep s = toBinaryDep' (unpack s)

-- Stolen from https://github.com/jumper149/AoC2021/blob/main/03/src/Main.idr
exactLengths : (len : Nat) -> Traversable t => t (n ** Binary n) -> Maybe (t (Binary len))
exactLengths len xs = traverse (\ x => exactLength len x.snd) xs

-- I thought one could define validateBinaryList recursively without
-- exactLengths, but while that compiles, it results in returning Nothing
-- always. Not precisely sure which Nothing either (from the recursive call or
-- from the call to exactLength).
validateBinaryList : List (n ** Binary n) -> Maybe (InputType)
validateBinaryList [] = Just (0 ** [])
validateBinaryList ((len ** bin) :: ys) = do
  list <- exactLengths len ys
  pure (len ** bin :: list)

----------------------------------------------------------------------------
-- Interface for input/output ----------------------------------------------
----------------------------------------------------------------------------

parser : String -> Maybe (InputType)
parser = join . map validateBinaryList . sequence . map toBinaryDep . lines

export
day3 : (inputType ** AOCSolution inputType)
day3 = solutionToDP (MkAOCSolution {
    day = 3
  , parser = parser
  , part1 = part1
  , part2 = \x => "part2"
  })


text:
works : (n : (Nat, Nat)) ->
        let mk = n in
            {y : Bool} -> (z : Bool) -> String
works (m, k) {y} z = ?h1

FailType : (Nat, Nat) -> Type
FailType (m, k) = {y : Bool} -> (z : Bool) -> String

fails : (n : (Nat, Nat)) -> FailType n
fails (m, k) {y} z = ?h2

fails2 : (n : (Nat, Nat)) ->
         let (m, k) = n in
             {y : Bool} -> (z : Bool) -> String
fails2 (m, k) {y} z = ?h3


text:
module IdrisJvm.IR.Exports

import IdrisJvm.IR.Types
import IdrisJvm.IO

%access public export

funknown : FDesc
fcon : String -> FDesc
fstr : String -> FDesc
fio : FDesc -> FDesc
fapp : String -> List FDesc -> FDesc

consFDesc : FDesc -> List FDesc -> List FDesc
emptyFDesc : List FDesc

consSDecl : SDecl -> List SDecl -> List SDecl
consSDecl = (::)

emptySDecl : List SDecl
emptySDecl = []

consExportIFace : ExportIFace -> List ExportIFace -> List ExportIFace
consExportIFace = (::)

emptyExportIFace : List ExportIFace
emptyExportIFace = []

consString : String -> List String -> List String
emptyListString : List String

consExport : Export -> List Export -> List Export
emptyExport : List Export

loc : Int -> LVar
glob : String -> LVar
it8 : NativeTy
it16 : NativeTy
it32 : NativeTy
it64 : NativeTy
itFixed : NativeTy -> IntTy
itNative : IntTy
itBig : IntTy
itChar : IntTy
atInt : IntTy -> ArithTy
atFloat : ArithTy
lPlus : ArithTy -> PrimFn
lMinus : ArithTy -> PrimFn
lTimes : ArithTy -> PrimFn
lSDiv : ArithTy -> PrimFn
lSRem : ArithTy -> PrimFn
lEq : ArithTy -> PrimFn
lSLt : ArithTy -> PrimFn
lSLe : ArithTy -> PrimFn
lSGt : ArithTy -> PrimFn
lSGe : ArithTy -> PrimFn
lUDiv : IntTy -> PrimFn
lURem : IntTy -> PrimFn
lAnd : IntTy -> PrimFn
lOr : IntTy -> PrimFn
lXOr : IntTy -> PrimFn
lCompl : IntTy -> PrimFn
lSHL : IntTy -> PrimFn
lLSHR : IntTy -> PrimFn
lASHR : IntTy -> PrimFn
lLt : IntTy -> PrimFn
lLe : IntTy -> PrimFn
lGt : IntTy -> PrimFn
lGe : IntTy -> PrimFn
lIntFloat : IntTy -> PrimFn
lFloatInt : IntTy -> PrimFn
lIntStr : IntTy -> PrimFn
lStrInt : IntTy -> PrimFn
lChInt : IntTy -> PrimFn
lIntCh : IntTy -> PrimFn
lFExp : PrimFn
lFLog : PrimFn
lFSin : PrimFn
lFCos : PrimFn
lFTan : PrimFn
lFASin : PrimFn
lFACos : PrimFn
lFATan : PrimFn
lFSqrt : PrimFn
lFFloor : PrimFn
lFCeil : PrimFn
lFNegate : PrimFn
lStrHead : PrimFn
lStrTail : PrimFn
lStrCons : PrimFn
lStrIndex : PrimFn
lStrRev : PrimFn
lStrSubstr : PrimFn
lReadStr : PrimFn
lWriteStr : PrimFn
lSystemInfo : PrimFn
lFork : PrimFn
lPar : PrimFn
lCrash : PrimFn
lNoOp : PrimFn
lStrConcat : PrimFn
lStrLt : PrimFn
lStrEq : PrimFn
lStrLen : PrimFn
lFloatStr : PrimFn
lStrFloat : PrimFn
lSExt : IntTy -> IntTy -> PrimFn
lZExt : IntTy -> IntTy -> PrimFn
lTrunc : IntTy -> IntTy -> PrimFn
lBitCast : ArithTy -> ArithTy -> PrimFn
lExternal : String -> PrimFn
exportData : FDesc -> Export
exportFun : String -> FDesc -> FDesc -> List FDesc -> Export
mkExportIFace : String -> String -> List Export -> ExportIFace
sV : LVar -> SExp
sApp : Bool -> String -> List LVar -> SExp
sLet : LVar -> SExp -> SExp -> SExp
sUpdate : LVar -> SExp -> SExp
sCon : (Maybe LVar) -> Int -> String -> List LVar -> SExp
sCase : CaseType -> LVar -> List SAlt -> SExp
sChkCase : LVar -> List SAlt -> SExp
sProj : LVar -> Int -> SExp
sConst : Const -> SExp
sForeign : FDesc -> FDesc -> List (FDesc, LVar) -> SExp
sOp : PrimFn -> List LVar -> SExp
sNothing : SExp
sError : String -> SExp
mkSForeignArg : FDesc -> LVar -> (FDesc, LVar)
consSAlt : SAlt -> List SAlt -> List SAlt
emptySAlt : List SAlt
consSForeignArg : (FDesc, LVar) -> List (FDesc, LVar) -> List (FDesc, LVar)
emptySForeignArg : List (FDesc, LVar)
consLVar : LVar -> List LVar -> List LVar
emptyLVar : List LVar
constI : Int -> Const
constBI : String -> Const
constFl : Double -> Const
constCh : Char -> Const
constStr : String -> Const
constB8 : Bits8 -> Const
constB16 : Bits16 -> Const
constB32 : Int -> Const
constB64 : Bits64 -> Const
aType : ArithTy -> Const
strType : Const
worldType : Const
theWorld : Const
voidType : Const
forgot : Const
sFun : String -> List String -> Int -> SExp -> SDecl
sConCase : Int -> Int -> String -> List String -> SExp -> SAlt
sConstCase : Const -> SExp -> SAlt
sDefaultCase : SExp -> SAlt
nothingLVar : Maybe LVar
justLVar : LVar -> Maybe LVar
updatable : CaseType
shared : CaseType

funknown = FUnknown

fcon = FCon

fstr = FStr

fio = FIO

fapp = FApp

consFDesc = (::)

emptyFDesc = []

consString = (::)

emptyListString  = []

consExport = (::)

emptyExport = []

loc = Loc

glob = Glob

it8 = IT8

it16 = IT16

it32 = IT32

it64 = IT64

itFixed = ITFixed

itNative = ITNative

itBig = ITBig

itChar = ITChar

atInt = ATInt

atFloat = ATFloat

{- PrimFn exports -}

lPlus = LPlus

lMinus = LMinus

lTimes = LTimes

lSDiv = LSDiv

lSRem = LSRem

lEq = LEq

lSLt = LSLt

lSLe = LSLe

lSGt = LSGt

lSGe = LSGe

lUDiv = LUDiv

lURem = LURem

lAnd = LAnd

lOr = LOr

lXOr = LXOr

lCompl = LCompl

lSHL = LSHL

lLSHR = LLSHR

lASHR = LASHR

lLt = LLt

lLe = LLe

lGt = LGt

lGe = LGe

lIntFloat = LIntFloat

lFloatInt = LFloatInt

lIntStr = LIntStr

lStrInt = LStrInt

lChInt = LChInt

lIntCh = LIntCh

lFExp = LFExp

lFLog = LFLog

lFSin = LFSin

lFCos = LFCos

lFTan = LFTan

lFASin = LFASin

lFACos = LFACos

lFATan = LFATan

lFSqrt = LFSqrt

lFFloor = LFFloor

lFCeil = LFCeil

lFNegate = LFNegate

lStrHead = LStrHead

lStrTail = LStrTail

lStrCons = LStrCons

lStrIndex = LStrIndex

lStrRev = LStrRev

lStrSubstr = LStrSubstr

lReadStr = LReadStr

lWriteStr = LWriteStr

lSystemInfo = LSystemInfo

lFork = LFork

lPar = LPar

lCrash = LCrash

lNoOp = LNoOp

lStrConcat = LStrConcat

lStrLt = LStrLt

lStrEq = LStrEq

lStrLen = LStrLen

lFloatStr = LFloatStr

lStrFloat = LStrFloat

lSExt = LSExt

lZExt = LZExt

lTrunc = LTrunc

lBitCast = lBitCast

lExternal = LExternal

exportData = ExportData

exportFun = ExportFun

mkExportIFace = MkExportIFace

sV = SV

sApp = SApp

sLet = SLet

sUpdate = SUpdate

sCon = SCon

sCase = SCase

sChkCase = SChkCase

sProj = SProj

sConst = SConst

sForeign = SForeign

sOp = SOp

sNothing = SNothing

sError = SError

mkSForeignArg fdesc lvar = (fdesc, lvar)

consSAlt = (::)

emptySAlt = []

consSForeignArg = (::)

emptySForeignArg = []

consLVar = (::)

emptyLVar = []

constI = I

constBI = BI

constFl = Fl

constCh = Ch

constStr = Str

constB8 = B8

constB16 = B16

constB32 = B32

constB64 = B64

aType = AType

strType = StrType

worldType = WorldType

theWorld = TheWorld

voidType = VoidType

forgot = Forgot

sFun n args locs exp = SFun n args locs exp

sConCase = SConCase

sConstCase = SConstCase

sDefaultCase = SDefaultCase

nothingLVar = Nothing

justLVar = Just

updatable = Updatable

shared = Shared


text:
module Main

import Data.Vect

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

-- checkEqNat : (num1 : Nat) -> (num2 : Nat) -> Maybe (EqNat num1 num2)
-- checkEqNat Z Z = ?checkEqNat_rhs_3
-- checkEqNat Z (S k) = ?checkEqNat_rhs_4
-- checkEqNat (S k) num2 = ?checkEqNat_rhs_2

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

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

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

same_cons : {xs : List a} -> {ys : List a} -> xs = ys -> x :: xs = x :: ys
same_cons {xs = []} {ys = []} prf = Refl
same_cons {xs = []} {ys = (x :: xs)} prf = cong prf
same_cons {xs = (x :: xs)} {ys = []} prf = cong prf
same_cons {xs = (x :: xs)} {ys = (y :: ys)} prf = cong prf

same_lists : {xs : List a} -> {ys : List a} ->  (x = y) -> (xs = ys) -> (x :: xs) = (y :: ys)
same_lists {x = x} {y = x} Refl prf1 = cong prf1

data ThreeEq : (x: Nat) -> (y: Nat) -> (z: Nat) -> Type where
  SameThree : (x: Nat) -> ThreeEq x x x

allSameS : (x, y, z: Nat) -> ThreeEq x y z -> ThreeEq (S x) (S y) (S z)
allSameS k k k (SameThree k) = SameThree (S k)

myReverse : Vect n elem -> Vect n elem
myReverse [] = []
myReverse {n = S k} (x :: xs) = let rev_xs = myReverse xs
                                    result = rev_xs ++ [x] in
                                    rewrite plusCommutative 1 k in result

myReverse1 : Vect n elem -> Vect n elem
myReverse1 [] = []
myReverse1 (x :: xs) = reverseProof (myReverse xs ++ [x]) where
           reverseProof: Vect (len + 1) elem -> Vect (S len) elem
           reverseProof {len} xs = rewrite plusCommutative 1 len in xs

appendnil : (Vect m elem) -> (Vect (plus m 0) elem)
appendnil {m} elem = rewrite plusZeroRightNeutral m in elem

append : Vect n elem -> Vect m elem -> Vect (m + n) elem
append [] ys = appendnil ys
append (x :: xs) ys = ?append_proof (x :: append xs ys)

-- append [] ys = ?append_rhs_1append (x :: xs) ys = ?append_rhs_2

data VElem : (value : a ) -> (xs: Vect k a) -> Type where
  Here: VElem x (x::xs)
  There: (later: VElem x xs) -> VElem x (y::xs)

-- maryInVector : VElem "Mary" ["Peter", "Paul", "Mary"]
-- maryInVector = There (There Here)

Uninhabited (VElem x []) where
  uninhabited x impossible

removeElem : (value: a) -> (xs: Vect (S n) a) -> (prf: VElem value xs) -> Vect n a
removeElem value (value :: ys) Here = ys
removeElem {n = Z} value (y :: []) (There later) =  absurd later
removeElem {n = (S k)} value (y :: ys) (There later) = y :: removeElem value ys later

removeElem_auto : (value: a) -> (xs: Vect (S n) a) -> {auto prf: VElem value xs} -> Vect n a
removeElem_auto value (value :: ys) {prf=Here} = ys
removeElem_auto {n = Z} value (y :: []) {prf=There later} =  absurd later
removeElem_auto {n = (S k)} value (y :: ys) {prf=There later} = y :: removeElem_auto value ys

max_stars_repo_name: gdevanla/idris-learn

max_issues_repo_name: gdevanla/idris-learn

max_forks_repo_name: gdevanla/idris-learn


text:
module Mod2

foo : Nat
foo = 2


text:
module JS.Buffer

import JS.Marshall

%default total

export
data ArrayBuffer : Type where [external]

export
ToFFI ArrayBuffer ArrayBuffer where toFFI = id

export
FromFFI ArrayBuffer ArrayBuffer where fromFFI = Just

export
data UInt8ClampedArray : Type where [external]

export
ToFFI UInt8ClampedArray UInt8ClampedArray where toFFI = id

export
FromFFI UInt8ClampedArray UInt8ClampedArray where fromFFI = Just

%foreign "javascript:lambda:x => new Uint8ClampedArray(x)"
prim__toUint8ClampedArray : ArrayBuffer -> UInt8ClampedArray

export
Cast ArrayBuffer UInt8ClampedArray where
  cast = prim__toUint8ClampedArray

export
data UInt8Array : Type where [external]

export
ToFFI UInt8Array UInt8Array where toFFI = id

export
FromFFI UInt8Array UInt8Array where fromFFI = Just

%foreign "javascript:lambda:x => new Uint8Array(x)"
prim__toUint8Array : ArrayBuffer -> UInt8Array

export
Cast ArrayBuffer UInt8Array where
  cast = prim__toUint8Array

export
data UInt16Array : Type where [external]

export
ToFFI UInt16Array UInt16Array where toFFI = id

export
FromFFI UInt16Array UInt16Array where fromFFI = Just

%foreign "javascript:lambda:x => new Uint16Array(x)"
prim__toUint16Array : ArrayBuffer -> UInt16Array

export
Cast ArrayBuffer UInt16Array where
  cast = prim__toUint16Array

export
data UInt32Array : Type where [external]

export
ToFFI UInt32Array UInt32Array where toFFI = id

export
FromFFI UInt32Array UInt32Array where fromFFI = Just

%foreign "javascript:lambda:x => new Uint32Array(x)"
prim__toUint32Array : ArrayBuffer -> UInt32Array

export
Cast ArrayBuffer UInt32Array where
  cast = prim__toUint32Array

export
data Int8Array : Type where [external]

export
ToFFI Int8Array Int8Array where toFFI = id

export
FromFFI Int8Array Int8Array where fromFFI = Just

%foreign "javascript:lambda:x => new Int8Array(x)"
prim__toInt8Array : ArrayBuffer -> Int8Array

export
Cast ArrayBuffer Int8Array where
  cast = prim__toInt8Array

export
data Int16Array : Type where [external]

export
ToFFI Int16Array Int16Array where toFFI = id

export
FromFFI Int16Array Int16Array where fromFFI = Just

%foreign "javascript:lambda:x => new Int16Array(x)"
prim__toInt16Array : ArrayBuffer -> Int16Array

export
Cast ArrayBuffer Int16Array where
  cast = prim__toInt16Array

export
data Int32Array : Type where [external]

export
ToFFI Int32Array Int32Array where toFFI = id

export
FromFFI Int32Array Int32Array where fromFFI = Just

%foreign "javascript:lambda:x => new Int32Array(x)"
prim__toInt32Array : ArrayBuffer -> Int32Array

export
Cast ArrayBuffer Int32Array where
  cast = prim__toInt32Array

export
data Float32Array : Type where [external]

export
ToFFI Float32Array Float32Array where toFFI = id

export
FromFFI Float32Array Float32Array where fromFFI = Just

%foreign "javascript:lambda:x => new Float32Array(x)"
prim__toFloat32Array : ArrayBuffer -> Float32Array

export
Cast ArrayBuffer Float32Array where
  cast = prim__toFloat32Array

export
data Float64Array : Type where [external]

export
ToFFI Float64Array Float64Array where toFFI = id

export
FromFFI Float64Array Float64Array where fromFFI = Just

%foreign "javascript:lambda:x => new Float64Array(x)"
prim__toFloat64Array : ArrayBuffer -> Float64Array

export
Cast ArrayBuffer Float64Array where
  cast = prim__toFloat64Array

export
data DataView : Type where [external]

export
ToFFI DataView DataView where toFFI = id

export
FromFFI DataView DataView where fromFFI = Just


text:
filter : (p : a -> Bool) -> List a -> List a
filter p []        = []
filter p (x :: xs) with (p x)
  _ | True  = x :: filter p xs
  _ | False = filter p xs

filterFilter : (p : a -> Bool) -> (xs : List a) ->
               filter p (filter p xs) === filter p xs
filterFilter p []        = Refl
filterFilter p (x :: xs) with (p x) proof eq
  _ | False = filterFilter p xs
  _ | True  with (p x)
    _ | True = cong (x ::) (filterFilter p xs)


text:
import Language.JSON

import Data.List
import Data.String

main : IO ()
main = printLn $ filter (not . roundTrips) chars
  where chars : List Int
        chars = [0 .. 55295]

        roundTrips : Int -> Bool
        roundTrips n =
          let s = singleton $ chr n
              v = JString s
           in case parse (show v) of
                   Just (JString x) => x == s
                   _                => False


text:
module BoehmBerarducci

%default total

NatQ : Type
NatQ = (A : Type) -> (A -> A) -> A -> A

unNatQ : {A : Type} -> (A -> A) -> A -> NatQ -> A
unNatQ f a q = q _ f a

succQ : NatQ -> NatQ
succQ q = \_, f, a => f (q _ f a)

zeroQ : NatQ
zeroQ = \_, f, a => a

fromNatQ : NatQ -> Nat
fromNatQ q = unNatQ S Z q

toNatQ : Nat -> NatQ
toNatQ (S n) = succQ (toNatQ n)
toNatQ Z     = zeroQ

iterated : Nat -> (a -> a) -> a -> a
iterated (S n) f a = f (iterated n f a)
iterated Z f a     = a

test_iterated : (n : Nat) -> iterated n S Z = n
test_iterated (S n) = rewrite test_iterated n in Refl
test_iterated Z     = Refl

test_fromNatQ : (n : Nat) -> fromNatQ (iterated n succQ zeroQ) = n
test_fromNatQ (S n) = rewrite test_fromNatQ n in Refl
test_fromNatQ Z     = Refl

test_toNatQ : (n : Nat) -> toNatQ n = iterated n succQ zeroQ
test_toNatQ (S n) = rewrite test_toNatQ n in Refl
test_toNatQ Z = Refl

ListQ : Type -> Type
ListQ A = (B : Type) -> (A -> B -> B) -> B -> B

unListQ : {A, B : Type} -> (A -> B -> B) -> B -> ListQ A -> B
unListQ f b q = q _ f b

consQ : {A : Type} -> A -> ListQ A -> ListQ A
consQ a q = \_, f, b => f a (q _ f b)

nilQ : {A : Type} -> ListQ A
nilQ = \_, f, b => b

fromListQ : {A : Type} -> ListQ A -> List A
fromListQ q = unListQ (::) [] q

toListQ : {A : Type} -> List A -> ListQ A
toListQ (a :: aa) = consQ a (toListQ aa)
toListQ []        = nilQ

max_stars_repo_name: mietek/scott-encoding

max_issues_repo_name: mietek/scott-encoding

max_forks_repo_name: mietek/scott-encoding


text:
module Inigo.Package.ParseHelpers

import Toml

export
maybe : Either String a -> Either String (Maybe a)
maybe (Left err) = Right Nothing
maybe (Right val) = Right (Just val)

export
withDefault : a -> Either String a -> Either String a
withDefault x (Left err) = Right x
withDefault _ els = els

export
string : List String -> Toml -> Either String String
string key toml =
  case get key toml of
    Just (Str x) =>
      Right x

    _ =>
      Left ("Missing or invalid key: " ++ (show key))

export
listStr : List String -> Toml -> Either String (List String)
listStr key toml =
  case get key toml of
    Just (Lst l) =>
      foldl (\acc, el =>
        case (acc, el) of
          (Right l, Str s) =>
            Right (s :: l)
          (Left err, _) =>
            Left err
          _ =>
            Left ("Invalid value type for " ++ (show key))
      ) (Right []) l
    _ =>
      Left ("Missing or invalid key: " ++ (show key))

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module Debug.Buffer

import Data.Buffer
import Data.List
import Data.String.Extra

toHex : Int -> Int -> String
toHex d n = pack $ reverse $ foldl toHexDigit [] (slice d n [])
    where
        toHexDigit : List Char ->Int -> List Char
        toHexDigit acc i = chr (if i < 10 then i + ord '0' else (i-10) + ord 'A')::acc
        slice : Int -> Int -> List Int -> List Int
        slice 0 _ acc = acc
        slice d n acc = slice (d-1) (n `div` 16) ((n `mod` 16)::acc)

showSep : String -> Nat -> List String -> String
showSep sep _ [] = ""
showSep sep n [x] = x ++ replicate (3*n) ' '
showSep sep Z (x :: xs) = x ++ sep ++ showSep sep Z xs
showSep sep (S n) (x :: xs) = x ++ sep ++ showSep sep n xs

renderRow : List Int -> String
renderRow dat =  showSep " " 16 (map (toHex 2) dat) ++
                "      " ++ pack (map (\i => if i > 0x1f && i < 0x80 then chr i else '.') dat)

group : Nat -> List a -> List (List a)
group n xs = worker [] xs
    where
        worker : List (List a) -> List a -> List (List a)
        worker acc [] = reverse acc
        worker acc ys = worker ((take n ys)::acc) (drop n ys)

export
dumpBuffer : HasIO io => Buffer -> io String
dumpBuffer buf = do
    size <- liftIO $ rawSize buf
    dat <- liftIO $ bufferData buf
    let rows = group 16 dat
    let hex = showSep "\n" 0 (map renderRow rows)
    pure $ hex ++ "\n\ntotal size = " ++ show size

export
printBuffer : HasIO io => Buffer -> io ()
printBuffer buf = putStrLn $ !(dumpBuffer buf)