ckoparkar

installPlugin :: [GHC.CommandLineOption] -> [GHC.CoreToDo]
              -> GHC.CoreM [GHC.CoreToDo]
installPlugin _ todos = return (testCoreTodo : todos)
  where
    testCoreTodo :: GHC.CoreToDo
    testCoreTodo = GHC.CoreDoPluginPass "TEST" test

    test :: GHC.ModGuts -> GHC.CoreM GHC.ModGuts
    test mod_guts = do
        hsc_env &lt- GHC.getHscEnv

ckoparkar

Rough notes as I read and use https://p.hagelb.org/letrec.html:

• I'm using luarocks for the first time today, but what's bad about it and what is letrec trying to fix?
• Dang, letrec should be named something else...
• The store should slurp in modules compiled as .so/.dll files as well? Need to search under package.cpath...
• Minor point, but all the built-in modules (table, string etc.) should be added to skip-module?.
• "-meta" files should contain more metadata...? Maybe something like:

   STORE/
 + log-meta-SHA.lua

ckoparkar

-- ghc-8.6.5 -O0 -ddump-ds -ddump-simpl -ddump-to-file -fexpose-all-unfoldings -dsuppress-uniques \
--   -fforce-recomp -dsuppress-idinfo A.hs

module A where

import qualified Data.Map as M

data Foo = A Int
         | B Foo Int
  deriving Eq

ckoparkar

Require Import List.
Require Import Omega.

Import ListNotations.

Definition strong_head {A : Type} : forall ls : list A, ls <> [] -> A.
  refine (fun (ls : list A) =>
            match ls with
            | []     => fun _ => _
            | a :: _ => fun _ => a

ckoparkar

diff --git a/pldi19/bench.sh b/pldi19/bench.sh
index 1bf8650..412c330 100755
--- a/pldi19/bench.sh
+++ b/pldi19/bench.sh
@@ -138,9 +138,17 @@ echo "MACHINE,NAME,VARIANT,SIZE,TRIALS,ITERS,SELFTIMED(sec)" >> $LITMUS_RESULT_F
 echo "Running in-memory benchmarks (Table 1)..."
 echo "Sending results to $LITMUS_RESULT_FILE"
 
-# Some benchmarks require 100M iterations. Only used for CNF and Cap'n Proto.
+

ckoparkar

#include <assert.h>
#include <stdio.h>
// #include <stdint.h>
#include <stdlib.h>
#include <string.h>
#include <time.h>
#include <alloca.h>
#include <sys/mman.h>
#include <sys/resource.h>
#include <sys/stat.h>

ckoparkar

#include <assert.h>
#include <stdio.h>
// #include <stdint.h>
#include <stdlib.h>
#include <string.h>
#include <time.h>
#include <alloca.h>
#include <sys/mman.h>
#include <sys/resource.h>
#include <sys/stat.h>

ckoparkar

Prog {ddefs = [("Tree",
                DDef {tyName = "Tree",
                      dataCons = [("Leaf", [(False, IntTy)]),
                                  ("Node",
                                   [(False, PackedTy "Tree" "loc92"),
                                    (False, PackedTy "Tree" "loc93")]),
                                  ("Node^",
                                   [(False, CursorTy),(False, PackedTy "Tree" "loc94"),
                                    (False, PackedTy "Tree" "loc95")]),
                                  ("INDIRECTION159", [(False, CursorTy)])]})],

ckoparkar

{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ForeignFunctionInterface #-}
{-# OPTIONS_GHC -Wno-name-shadowing #-}
module Bug where

{-

`rts.c` has a minimal RTS I'm using to test the object file linking. It houses the `main` function.
The main function calls `main_expr`, which is provided by this LLVM module. 

ckoparkar

module Blade where

import qualified Data.Set as S

-- Implemented the inclusion-exclusion algorithm:
-- <https://stackoverflow.com/a/27248971>

-- (∑ Aj) in the formula
-- These all the numbers we've counted more than once
doubleCounts :: [Int]