aztek

#include <iostream>
using namespace std;

template <int N> struct Factorial {
    enum { value = N * Factorial<N - 1>::value };
};

template <> struct Factorial<0> {
    enum { value = 1 };
};

aztek

package com.myapp

object IntegerFunctions {
  val increment: Int => Int = _ + 1
  val decrement: Int => Int = _ + 1

  val lolNoIntegers: String => String = _ + "!!!"
}

aztek

Require Import Coq.Program.Basics.
Require Import Coq.Program.Syntax.
Require Import Coq.Init.Datatypes.
Require Import Coq.Unicode.Utf8.

Open Local Scope program_scope.
Open Local Scope list_scope.
Open Local Scope type_scope.

Class Functor (φ : Type → Type) := {

aztek

import language.experimental.macros
import reflect.macros.Context

object WeirdMacro {
  def show_structure(something: Any): String = macro show_structure_impl

  def show_structure_impl(c: Context)(something: c.Expr[Any]): c.Expr[String] = {
    import c.universe._

    c.Expr[String](Literal(Constant(something.tree.toString)))

aztek

diff --git a/src/compiler/scala/reflect/reify/phases/Reshape.scala b/src/compiler/scala/reflect/reify/phases/Reshape.scala
index f31c3d4..ce243d9 100644
--- a/src/compiler/scala/reflect/reify/phases/Reshape.scala
+++ b/src/compiler/scala/reflect/reify/phases/Reshape.scala
@@ -187,8 +187,12 @@ trait Reshape {
     }

     private def toPreTyperTypedOrAnnotated(tree: Tree): Tree = tree match {
-      case ty @ Typed(expr1, tt @ TypeTree()) =>
+      case ty @ Typed(expr1, tt) =>

aztek

java.lang.Error: unexpected: bound type that doesn't have a tpe: Ident(newTypeName("Any"))
21at scala.reflect.reify.codegen.GenTrees$class.reifyBoundType$1(GenTrees.scala:154)
	at scala.reflect.reify.codegen.GenTrees$class.reifyBoundType(GenTrees.scala:201)
	at scala.reflect.reify.codegen.GenTrees$class.reifyTree(GenTrees.scala:56)
	at scala.reflect.reify.Reifier.reifyTree(Reifier.scala:14)
	at scala.reflect.reify.phases.Reify$$anonfun$reify$1.apply(Reify.scala:44)
	at scala.reflect.reify.phases.Reify$$anonfun$reify$1.apply(Reify.scala:37)
	at scala.reflect.reify.phases.Reify$reifyStack$.push(Reify.scala:25)
	at scala.reflect.reify.phases.Reify$class.reify(Reify.scala:37)
	at scala.reflect.reify.Reifier.reify(Reifier.scala:14)

aztek

import idioms._ // http://github.com/aztek/scala-idioms

trait Cell[T] {
  def ! : T
  def := (value: T) { throw new UnsupportedOperationException }
}

val frp = new Idiom[Cell] {
  def pure[A](a: ⇒ A) = new Cell[A] {
    private var value = a

aztek

sealed trait Trampoline[A] {
  def map[B](f: A => B): Trampoline[B] =
    flatMap(a => More(() => Done(f(a))))
  def flatMap[B](f: A => Trampoline[B]): Trampoline[B] =
    Cont(this, f)
  def run: A = {
    var cur: Trampoline[_] = this
    var stack: List[Any => Trampoline[A]] = List()
    var maxStackSize = 0 // NEW
    var result: Option[A] = None

aztek

/* Basic example */
@workflow[List] val x = List(1, 2) * List(4, 5)

/* Using @context */
@context[Option] object optionExamples {
  $(Some(42) + 1) should equal (Some(43))
  $(Some(10) + Some(5) * Some(2)) should equal (Some(20))
}

@context[List] object listExamples {

aztek

ℕ³-induction : ∀ {P : ℕ → ℕ → ℕ → Set} → P 0 0 0 →
               (∀ {n} → P n 0 0 → P (succ n) 0 0) →
               (∀ {m} → P 0 m 0 → P 0 (succ m) 0) →
               (∀ {k} → P 0 0 k → P 0 0 (succ k)) →
               (∀ {n m} → P n m 0 → P (succ n) (succ m) 0) →
               (∀ {n k} → P n 0 k → P (succ n) 0 (succ k)) →
               (∀ {m k} → P 0 m k → P 0 (succ m) (succ k)) →
               (∀ {n m k} → P n m k →
                            P (succ n) m k → P n (succ m) k → P n m (succ k) →
                            P (succ n) (succ m) k → P (succ n) m (succ k) → P n (succ m) (succ k) →