aztek

q="eurT=fmap const pure 'q' abs;eslaF=fmap const show q gcd;xam=fmap const pure '=' odd;denifednu=ip<>di;dns=eurT<>xam;tsf=dns<>eslaF;ip=pure$!tsf;di=fmap const pure q cos;ton=dna<$>unlines;dna=putStr`fmap`yna;yna=mappend<*>reverse;main=let erehw main=main in fmap const ton denifednu main"
eurT=fmap const pure 'q' abs;eslaF=fmap const show q gcd;xam=fmap const pure '=' odd;denifednu=ip<>di;dns=eurT<>xam;tsf=dns<>eslaF;ip=pure$!tsf;di=fmap const pure q cos;ton=dna<$>unlines;dna=putStr`fmap`yna;yna=mappend<*>reverse;main=let erehw main=main in fmap const ton denifednu main

niam undefined not tsnoc pamf ni niam=niam where tel=niam;esrever>*<dneppam=any;any`pamf`rtStup=and;senilnu>$<and=not;soc q erup tsnoc pamf=id;fst!$erup=pi;False><snd=fst;max><True=snd;id><pi=undefined;ddo '=' erup tsnoc pamf=max;dcg q wohs tsnoc pamf=False;sba 'q' erup tsnoc pamf=True
"niam undefined not tsnoc pamf ni niam=niam where tel=niam;esrever>*<dneppam=any;any`pamf`rtStup=and;senilnu>$<and=not;soc q erup tsnoc pamf=id;fst!$erup=pi;F

aztek

open import Level using (_⊔_)
open import Function
open import Data.Fin using (Fin; zero; suc)
open import Data.Nat hiding (_⊔_)
open import Data.Nat.Properties
open import Data.Vec
open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary.Core

aztek

open import Level
open import Data.List
open import Data.Sum
open import Relation.Binary

module InsertionSort {ℓ ℓ₁ ℓ₂} (totalOrder : TotalOrder ℓ ℓ₁ ℓ₂) where

open TotalOrder totalOrder renaming (Carrier to A)
open IsTotalOrder isTotalOrder renaming (trans to ≤-trans; total to _≤?_)

aztek

module RomanNumerals where

open import Data.List
open import Data.Unit using (⊤; tt)
open import Data.Empty using (⊥)

data Literal : Set where
  𝐼 𝑉 𝑋 𝐿 𝐶 𝐷 𝑀 : Literal

infix 4 ones_

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) →

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

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

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

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

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) =>