This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE DerivingStrategies #-} | |
{-# LANGUAGE OverloadedStrings #-} | |
{-# LANGUAGE RecordWildCards #-} | |
module Parser (module Parser) where | |
import Control.Monad (void) | |
import Data.Kind (Type) | |
import Data.List.Extra (groupSort) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{ 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" | |
''; | |
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
import Lean.Data.AssocList | |
import Parser | |
namespace SaidScript | |
abbrev Env := Lean.AssocList String Int | |
inductive Op : Type | |
| add | sub | mul | div | |
deriving Repr |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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"); |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE DataKinds #-} | |
{-# LANGUAGE DeriveAnyClass #-} | |
{-# LANGUAGE ImplicitParams #-} | |
{-# LANGUAGE OverloadedRecordDot #-} | |
{-# LANGUAGE OverloadedStrings #-} | |
{-# LANGUAGE QuasiQuotes #-} | |
{-# LANGUAGE TemplateHaskell #-} | |
{-# LANGUAGE TypeFamilies #-} | |
{-# LANGUAGE UndecidableInstances #-} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE BlockArguments #-} | |
{-# LANGUAGE DeriveAnyClass #-} | |
{-# LANGUAGE DerivingStrategies #-} | |
{-# LANGUAGE DuplicateRecordFields #-} | |
{-# LANGUAGE LambdaCase #-} | |
module Main (main) where | |
import Control.DeepSeq (NFData, force) | |
import Control.Exception (evaluate) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 #-} |
OlderNewer