AndrasKovacs

{-
At ICFP 2022 I attended a talk given by Tomasz Drab, about this paper:

    "A simple and efficient implementation of strong call by need by an abstract machine"
    https://dl.acm.org/doi/10.1145/3549822

This is right up my alley since I've implemented strong call-by-need evaluation
quite a few times (without ever doing more formal analysis of it) and I'm also
interested in performance improvements. Such evaluation is required in
conversion checking in dependently typed languages.

Lysxia

{-# LANGUAGE GADTs, DeriveFunctor, LambdaCase #-}

import Data.Functor.Product
import Data.Void
import Control.Applicative

type Tag = String
type Attr = String

data HTML

TOTBWF

{-# OPTIONS --allow-exec #-}

-- Embed a file as a string inside of an agda program.
-- To use this, make sure to add '/bin/cat' to '~/.agda/executables'

module Static where

open import Function

open import Data.Unit

TOTBWF

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE TemplateHaskell #-}
module ObfuscatedSKI where

import Unsafe.Coerce (unsafeCoerce)

--------------------------------------------------------------------------------
-- A Lambda to SKI Combinator Compiler, written entirely using SKI Combinators
--

TOTBWF

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
module IOHCC where

import Unsafe.Coerce

u = unsafeCoerce

gelisam

-- A demonstration of Agda's mechanisms for generating proofs:
-- * 1. fromMaybe
-- * 2a. macros
-- * 2b. type-aware macros
-- * 2c. stuck macros
--
-- Tested using Agda-2.6.1.1 and agda-stdlib-1.4

module GeneratingCode where

IAmStoxe

jsonData='[{"name": "name#1","value": "value#1"},{"name": "name#2","value": "value#2"}]'
for row in $(echo "${jsonData}" | jq -r '.[] | @base64'); do
    _jq() {
     echo "${row}" | base64 --decode | jq -r "${1}"
    }
    
    # OPTIONAL
    # Set each property of the row to a variable
    name=$(_jq '.name')
    value=$(_jq '.value')

cdunham

#!/bin/sh
set -e
# git snap: (re-)commit a snapshot of exactly another commit
# an alternative to 'pick' in git rebase -i: use x git snap <sha>
if [ -z "$1" ]; then
  echo "usage: git snap <commit sha1>"
  exit
fi

case `git cat-file -t $1` in

adamgundry

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

AndreasPK

        Tue Aug 27 19:56 2019 Time and Allocation Profiling Report  (Final)

           ghc.exe +RTS -p -RTS Main.hs --make -O -fforce-recomp

        total time  =        7.72 secs   (7721 ticks @ 1000 us, 1 processor)
        total alloc = 9,747,651,160 bytes  (excludes profiling overheads)

COST CENTRE              MODULE      SRC                                                 %time %alloc

simplIdF                 Simplify    compiler\simplCore\Simplify.hs:899:61-79             16.9   18.1