Skip to content

Instantly share code, notes, and snippets.

View thelissimus's full-sized avatar

kei thelissimus

View GitHub Profile
@thelissimus
thelissimus / Parser.hs
Last active October 5, 2023 18:37
Toy URI parser with megaparsec
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RecordWildCards #-}
module Parser (module Parser) where
import Control.Monad (void)
import Data.Kind (Type)
import Data.List.Extra (groupSort)
@thelissimus
thelissimus / shell.nix
Created October 5, 2023 16:59
Nix shell for solving zlib problem.
{ pkgs ? import <nixpkgs> { } }:
pkgs.mkShell rec {
buildInputs = with pkgs; [ zlib ];
shellHook = ''
export LD_LIBRARY_PATH="${pkgs.lib.makeLibraryPath buildInputs}:$LD_LIBRARY_PATH"
export LD_LIBRARY_PATH="${pkgs.stdenv.cc.cc.lib.outPath}/lib:$LD_LIBRARY_PATH"
'';
}
@thelissimus
thelissimus / Hiccup.lean
Last active January 16, 2024 10:41
Hiccup renderer in Lean 4
inductive Hiccup : Type
| tag : String -> List (String × String) -> List Hiccup -> Hiccup
| value : String -> Hiccup
deriving Repr
open Hiccup
partial def render : Hiccup -> String
| tag name attrs rest => s!"<{name} {buildAttrs attrs}>{rest.map render |> String.join}</{name}>"
| value s => s
@thelissimus
thelissimus / SaidScript.lean
Last active January 17, 2024 13:22
SaidScript
import Lean.Data.AssocList
import Parser
namespace SaidScript
abbrev Env := Lean.AssocList String Int
inductive Op : Type
| add | sub | mul | div
deriving Repr
@thelissimus
thelissimus / HindleyMilner.lean
Last active January 20, 2024 14:40
Hindley-Milner type inference in Lean 4. (WIP)
import Lean.Data.AssocList
import Lean.Data.HashMap
abbrev Name := String
inductive Literal : Type
| LInt : Int -> Literal
| LBool : Bool -> Literal
deriving Repr, Inhabited, DecidableEq, Ord
@thelissimus
thelissimus / printf.lean
Last active January 23, 2024 07:04
Type-safe printf in Lean 4.
inductive Format : Type
| string : Format → Format
| int : Format → Format
| other : Char → Format → Format
| nil : Format
deriving Repr
open Format
def mkSignature (res : Type) : Format → Type
@thelissimus
thelissimus / Config.ts
Last active February 21, 2024 06:50
Usage of Layer and Config from Effect for DI and configuration.
import { Effect as IO, Config, Context, Layer, pipe } from "effect";
export type ServerConfig = Readonly<{
port: number;
mode: "development" | "production" | "test";
}>;
export class ServerConfigCtx extends Context.Tag("ServerConfigCtx")<ServerConfigCtx, ServerConfig>() {}
const getNodeEnv = Config.literal("development", "production", "test")("NODE_ENV");
@thelissimus
thelissimus / Main.hs
Last active February 24, 2024 20:27
Usage example of servant, persistent, esqueleto, warp Haskell libraries. A CRUD server with API contract.
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE OverloadedRecordDot #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE DuplicateRecordFields #-}
{-# LANGUAGE LambdaCase #-}
module Main (main) where
import Control.DeepSeq (NFData, force)
import Control.Exception (evaluate)
@thelissimus
thelissimus / BitPack.hs
Last active March 1, 2024 06:48
Bit-packing Word32 and Word8 into Word64 in Haskell.
import Data.Bits (Bits (shiftL, shiftR, (.&.), (.|.)))
import Data.Word (Word32, Word64, Word8)
word64 :: (Word32, Word8) -> Word64
word64 (w32, w8) = ((fromIntegral w32 :: Word64) `shiftL` 8) .|. (fromIntegral w8 :: Word64)
{-# INLINE [0] word64 #-}
unword64Fst :: Word64 -> Word32
unword64Fst w = fromIntegral (w `shiftR` 8)
{-# INLINE [0] unword64Fst #-}