1 files changed, 57 insertions, 0 deletions
diff --git a/Library/Formula/agda.rb b/Library/Formula/agda.rb
new file mode 100644
index 000000000..ec8fdf7dc
--- /dev/null
+++ b/Library/Formula/agda.rb
@@ -0,0 +1,57 @@
+require "language/haskell"
+
+class Agda < Formula
+  include Language::Haskell::Cabal
+
+  homepage "http://wiki.portal.chalmers.se/agda/"
+  url "http://hackage.haskell.org/package/Agda-2.4.2.2/Agda-2.4.2.2.tar.gz"
+  sha1 "fbdf7df3d5a036e683210ac7ccf4f8ec0c9fea05"
+
+  devel do
+    url "https://github.com/agda/agda.git", :branch => "maint-2.4.2"
+    version "2.4.2.3-beta"
+  end
+
+  head "https://github.com/agda/agda.git", :branch => "master"
+
+  option "without-epic-backend", "Exclude the 'epic' compiler backend"
+
+  depends_on "ghc" => :build
+  depends_on "cabal-install" => :build
+  depends_on "gmp"
+  depends_on "bdw-gc" if build.with? "epic-backend"
+
+  def install
+    if build.with? "epic-backend"
+      epic_flag = "-fepic"
+    else
+      epic_flag = "-f-epic"
+    end
+    cabal_sandbox do
+      cabal_install_tools "alex", "happy", "cpphs"
+      cabal_install "--only-dependencies", epic_flag
+      cabal_install "--prefix=#{prefix}", epic_flag
+    end
+    cabal_clean_lib
+  end
+
+  test do
+    # run Agda's built-in test suite
+    system bin/"agda", "--test"
+
+    # typecheck and compile a simple module
+    path = testpath/"test.agda"
+    path.write <<-EOS.undent
+      module test where
+      open import Agda.Primitive
+      infixr 6 _::_
+      data List {i} (A : Set i) : Set i where
+        [] : List A
+        _::_ : A -> List A -> List A
+      snoc : forall {i} {A : Set i} -> List A -> A -> List A
+      snoc [] x = x :: []
+      snoc (x :: xs) y = x :: (snoc xs y)
+    EOS
+    system bin/"agda", "-c", "--no-main", "--safe", "--without-K", path
+  end
+end