Skip to content

Instantly share code, notes, and snippets.

View phile314's full-sized avatar

Philipp Hausmann phile314

  • Zürich, Switzerland
View GitHub Profile
@phile314
phile314 / Pinch codegen
Last active January 5, 2021 21:25
Pinch codegen example (simplified)
-- thrift source
namespace hs Thrift
# Trivial exception for testing only.
exception Exception {
# The exception simply contains a message string.
1: required string message;
}
module ReflApp where
open import Reflection
open import IO
open import Data.Unit
open import Data.List
import IO.Primitive
g : Term
g = app (lam visible (abs "x" (var 0 []))) [ (arg (arg-info visible relevant) (def (quote putStrLn) [ (arg (arg-info visible relevant) (quoteTerm "dfgdfg")) ])) ]
@phile314
phile314 / RunWithIO.agda
Last active August 29, 2015 14:16
PiWare IO Runner
open import PiWare.Atom.Bool using (Atomic-B)
open import PiWare.Gates Atomic-B
module Test.RunWithIO (Gt : Gates) where
-- A = type of atoms
open import Data.Vec as Vec using (Vec)
open import Data.Nat as Nat using (ℕ; _≤?_; suc; _+_)
open import Data.Maybe as Maybe using (Maybe; just; nothing)
open import Data.String as String using (String; fromList; toList; Costring)