Skip to content

Instantly share code, notes, and snippets.

Nickolay Kudasov fizruk

View GitHub Profile
View isaprop_isaprop.v
Require Export UniMath.Foundations.Propositions.
(* A simpler definition of proposition. *)
Definition isaprop' (X : UU) : UU := ∏ (x y : X), x = y.
(* Simpler definition implies standard isaprop. *)
Definition isaprop'_to_isaprop {X : UU} :
isaprop' X → isaprop X.
Proof.
intros f x y.
View servant-token-bearer.hs
#! /usr/bin/env nix-shell
#! nix-shell -i runghc -p "haskellPackages.ghcWithPackages (pkgs: with pkgs; [servant-server])"
-- =======================================================================
--
-- If you have have Nix installed — just run this script as an executable:
--
-- $ ./servant-token-bearer.hs
-- Starting server at http://localhost:8088
--
-- You can then check that everything works using cURL:
@fizruk
fizruk / replace-sub-api.hs
Last active Aug 9, 2018
Replace sub api to change implementation for an endpoint handler to a more efficient one.
View replace-sub-api.hs
#! /usr/bin/env nix-shell
#! nix-shell -i runghc -p "haskellPackages.ghcWithPackages (pkgs: with pkgs; [servant-swagger servant-swagger-ui])"
{-# OPTIONS_GHC -Wall #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
@fizruk
fizruk / servant-overrided-as.hs
Last active Aug 9, 2018
OverridableAs combinator to enable efficient implementations for some Servant endpoints after the fact.
View servant-overrided-as.hs
#! /usr/bin/env nix-shell
#! nix-shell -i runghc -p "haskellPackages.ghcWithPackages (pkgs: with pkgs; [servant-swagger servant-swagger-ui])"
{-# OPTIONS_GHC -Wall #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
View stack-ghcjs-docker.yaml
resolver: lts-6.20
compiler: ghcjs-0.2.0.9006020_ghc-7.10.3
compiler-check: match-exact
packages:
- '.'
# where to get GHCJS from (you don't need it when using Docker)
setup-info:
ghcjs:
@fizruk
fizruk / config.yml
Created Mar 26, 2018
Circle CI 2.0 config for a Haskell Stack project (for LTS 11.0).
View config.yml
version: 2
jobs:
build:
docker:
- image: fpco/stack-build:lts-11.0
steps:
- checkout
- restore_cache:
@fizruk
fizruk / README.md
Last active Nov 21, 2017
Run GHCJSi for a project with static files.
View README.md
  1. Put irunner.js into your repository at ghcjs/lib/etc/irunner.js.
  2. Put static content (CSS, images, etc.) for executable at <executable name>/static.
  3. Put ghcjsiClient.html to <executable name>/static and add any headers you want.
  4. Run run.sh <package name> <executable name>.

Caveats

npm packages

In order for everything to work you need to install a few packages via npm.

@fizruk
fizruk / HasServerVerb.hs
Created May 15, 2017
Verb with multiple methods.
View HasServerVerb.hs
class AllReflectMethod methods where
reflectMethods :: Proxy methods -> [Method]
instance AllReflectMethod '[] where
reflectMethods _ = []
instance (ReflectMethod m, AllReflectMethod ms) => AllReflectMethod (m:ms) where
reflectMethods _ = reflectMethod (Proxy @m) : reflectMethods (Proxy @ms)
instance OVERLAPPING_
View servant-swagger-description.hs
data Description (sym :: Symbol)
instance (KnownSymbol sym, HasSwagger api) => HasSwagger (Description sym :> api) where
toSwagger _ = toSwagger (Proxy :: Proxy api)
& allOperations.description ?~ desc
where
desc = symbolVal (Proxy :: Proxy sym)
View ToSchemaEither.hs
{-# LANGUAGE ScopedTypeVariables #-}
import Control.Lens
import Data.Typeable
import qualified Data.Text as Text
instance {-# OVERLAPPING #-} (Typeable a, ToSchema a) => ToSchema (Either WalletError a) where
declareNamedSchema proxy = genericDeclareNamedSchema defaultSchemaOptions proxy
& mapped.name ?~ Text.pack ("Either WalletError " ++ show (typeOf (undefined :: a)))
You can’t perform that action at this time.