Matthis Kruse DasNaCl

## stlcsubrec.v
Set Implicit Arguments.
Require Import List Program FunctionalExtensionality.

Definition var : Type := nat.

Definition total_map (B:Type) := var -> B.
Definition t_empty {B:Type} (v : B) : total_map B :=
  (fun _ => v)
.
Definition t_update {B:Type} (m : total_map B)

## stlc+nat.v
Set Implicit Arguments.
Require Import List Program FunctionalExtensionality.

(** Proof of syntactic type safety for call-by-value STLC extended with ℕ. *)

(** Names/Variables will be identified with a natural number.
    λx.λy.y x is represented as λλ0 1 *)
Definition var : Type := nat.

(** There is a need for partial maps, e.g., to keep track of what variable

## shift_or.cpp
/**
 * This implements the Shift-Or-Algorithm.
 * Text input is via STDIN, pattern is expected as cmd argument.
 * Example call: echo "12121321231" | ./a.out 123
 *
 * The algorithm exits early as soon as a match was found. It can be easily modified
 * to count all pattern occurences or even to provide all start positions.
 *
 * Compilation:   g++ -O3 shiftor.cpp -o program
 * Execution:     ./program AA text.txt

## simple_cexpr_map.cpp
#include <functional>
#include <iterator>
#include <cassert>
#include <cstring>
#include <string>
#include <tuple>
#include <array>

#include <initializer_list>

## pomodoro.sh
#!/usr/bin/env bash

if [ -z $1 ]; then
  echo "Expected total number of pomodoro sessions. Use \"?\" or \"h\" if you don\'t know about pomodoro."
  exit 0
fi

if [ "$1" = "h" ] || [ "$1" = "help" ] || [ "$1" = "?" ] || [ "$1" = "-h" ] || [ "$1" = "--help" ]; then
  echo "The task-completion technique consists of 6 steps:"
  echo -e "  1) Decide on the task to be done.\n"

## day-mode
#!/bin/bash

# export DBUS_SESSION_BUS_ADDRESS environment variable because cron hates me
PID=$(pgrep -u USER gnome-session-b)
export DBUS_SESSION_BUS_ADDRESS=$(grep -z DBUS_SESSION_BUS_ADDRESS /proc/$PID/environ|cut -d= -f2-)

/usr/bin/gsettings set org.gnome.shell.extensions.user-theme name 'Flat-Plat'
/usr/bin/gsettings set org.gnome.desktop.interface gtk-theme 'Flat-Plat'
/usr/bin/gsettings set org.gnome.desktop.background picture-uri 'file://WALLPAPER-PATH'
/usr/bin/gsettings --schemadir ~/.local/share/gnome-shell/extensions/drop-down-terminal@gs-extensions.zzrough.org set org.zzrough.gs-extensions.drop-down-terminal background-color 'rgb(69,90,100)'

## ubiq_trick.cpp
#include <type_traits>

template<int> struct int_constant {};
template<char> struct char_constant {};

inline constexpr struct ubiq
{
  template<class T>
  constexpr operator T() const noexcept
  { return T{}; }

## crtp.cpp
/*
   Copyright 2018 Matthis Kruse

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
	Set Implicit Arguments.
	Require Import List Program FunctionalExtensionality.

	Definition var : Type := nat.

	Definition total_map (B:Type) := var -> B.
	Definition t_empty {B:Type} (v : B) : total_map B :=
	(fun _ => v)
	.
	Definition t_update {B:Type} (m : total_map B)
	Set Implicit Arguments.
	Require Import List Program FunctionalExtensionality.

	(** Proof of syntactic type safety for call-by-value STLC extended with ℕ. *)

	(** Names/Variables will be identified with a natural number.
	λx.λy.y x is represented as λλ0 1 *)
	Definition var : Type := nat.

	(** There is a need for partial maps, e.g., to keep track of what variable
	/**
	* This implements the Shift-Or-Algorithm.
	* Text input is via STDIN, pattern is expected as cmd argument.
	* Example call: echo "12121321231" \| ./a.out 123
	*
	* The algorithm exits early as soon as a match was found. It can be easily modified
	* to count all pattern occurences or even to provide all start positions.
	*
	* Compilation: g++ -O3 shiftor.cpp -o program
	* Execution: ./program AA text.txt
	#include <functional>
	#include <iterator>
	#include <cassert>
	#include <cstring>
	#include <string>
	#include <tuple>
	#include <array>

	#include <initializer_list>
	#!/usr/bin/env bash

	if [ -z $1 ]; then
	echo "Expected total number of pomodoro sessions. Use \"?\" or \"h\" if you don\'t know about pomodoro."
	exit 0
	fi

	if [ "$1" = "h" ] \|\| [ "$1" = "help" ] \|\| [ "$1" = "?" ] \|\| [ "$1" = "-h" ] \|\| [ "$1" = "--help" ]; then
	echo "The task-completion technique consists of 6 steps:"
	echo -e " 1) Decide on the task to be done.\n"
	#!/bin/bash

	# export DBUS_SESSION_BUS_ADDRESS environment variable because cron hates me
	PID=$(pgrep -u USER gnome-session-b)
	export DBUS_SESSION_BUS_ADDRESS=$(grep -z DBUS_SESSION_BUS_ADDRESS /proc/$PID/environ\|cut -d= -f2-)

	/usr/bin/gsettings set org.gnome.shell.extensions.user-theme name 'Flat-Plat'
	/usr/bin/gsettings set org.gnome.desktop.interface gtk-theme 'Flat-Plat'
	/usr/bin/gsettings set org.gnome.desktop.background picture-uri 'file://WALLPAPER-PATH'
	/usr/bin/gsettings --schemadir ~/.local/share/gnome-shell/extensions/drop-down-terminal@gs-extensions.zzrough.org set org.zzrough.gs-extensions.drop-down-terminal background-color 'rgb(69,90,100)'
	#include <type_traits>

	template<int> struct int_constant {};
	template<char> struct char_constant {};

	inline constexpr struct ubiq
	{
	template<class T>
	constexpr operator T() const noexcept
	{ return T{}; }
	/*
	Copyright 2018 Matthis Kruse

	Licensed under the Apache License, Version 2.0 (the "License");
	you may not use this file except in compliance with the License.
	You may obtain a copy of the License at

	http://www.apache.org/licenses/LICENSE-2.0

	Unless required by applicable law or agreed to in writing, software