Add ats-extsolve (formerly patsolve)

5 files changed, 175 insertions, 0 deletions

diff --git a/pkgs/development/compilers/ats-extsolve/default.nix b/pkgs/development/compilers/ats-extsolve/default.nix
new file mode 100644
index 000000000000..9cd6d3adb324
--- /dev/null
+++ b/pkgs/development/compilers/ats-extsolve/default.nix
@@ -0,0 +1,35 @@
+{ stdenv, fetchurl, ats2, python, z3, pkgconfig, json_c }:
+
+stdenv.mkDerivation {
+  name = "ats-extsolve-0pre6a9b752";
+
+  buildInputs = [ python z3 ats2 pkgconfig json_c ];
+
+  src = fetchurl {
+    url = "https://github.com/githwxi/ATS-Postiats-contrib/archive/6a9b752efb8af1e4f77213f9e81fc2b7fa050877.tar.gz";
+    sha256 = "1zz4fqjm1rdvpm0m0sdck6vx55iiqlk2p8z078fca2q9xyxqjkqd";
+  };
+
+  postUnpack = ''
+    export PATSHOMERELOC="$PWD/$sourceRoot";
+    export NIX_CFLAGS_COMPILE="$NIX_CFLAGS_COMPILE -I$PATSHOMERELOC"
+  '';
+
+  patches = [ ./misc-fixes.patch ];
+
+  preBuild = "cd projects/MEDIUM/ATS-extsolve";
+
+  buildFlags = [ "setup" "patsolve" ];
+
+  installPhase = ''
+    install -d -m755 $out/bin
+    install -m755 patsolve $out/bin
+  '';
+
+  meta = {
+    platforms = ats2.meta.platforms;
+    homepage = http://www.illtyped.com/projects/patsolve;
+    description = "External Constraint-Solving for ATS2";
+    maintainer = [ stdenv.lib.maintainers.shlevy ];
+  };
+}
diff --git a/pkgs/development/compilers/ats-extsolve/misc-fixes.patch b/pkgs/development/compilers/ats-extsolve/misc-fixes.patch
new file mode 100644
index 000000000000..8775bb83ba4c
--- /dev/null
+++ b/pkgs/development/compilers/ats-extsolve/misc-fixes.patch
@@ -0,0 +1,136 @@
+From bfc7216250e666a59e304f3b7518f8b0bccccbae Mon Sep 17 00:00:00 2001
+From: Shea Levy <shea@shealevy.com>
+Date: Thu, 30 Apr 2015 16:50:47 -0400
+Subject: [PATCH] Add missing case in fprint_s2rt
+
+---
+ projects/MEDIUM/ATS-extsolve/constraint/constraint_s2rt.dats | 1 +
+ 1 file changed, 1 insertion(+)
+
+diff --git a/projects/MEDIUM/ATS-extsolve/constraint/constraint_s2rt.dats b/projects/MEDIUM/ATS-extsolve/constraint/constraint_s2rt.dats
+index a841b5f..5bc28d7 100644
+--- a/projects/MEDIUM/ATS-extsolve/constraint/constraint_s2rt.dats
++++ b/projects/MEDIUM/ATS-extsolve/constraint/constraint_s2rt.dats
+@@ -113,6 +113,7 @@ case+ s2t0 of
+ | S2RTfun (args, ret) => fprint (out, "S2RTfun()")
+ | S2RTtup () => fprint (out, "S2RTtup()")
+ | S2RTerr () => fprint (out, "S2RTerr()")
++| S2RTuninterp (str) => fprint! (out, "S2RTuninterp(", str, ")")
+ //
+ | S2RTignored () => fprint (out, "S2RTignored()")
+ //
+From 9d4c7669d0d3bc8725648684391a2962ed5a922e Mon Sep 17 00:00:00 2001
+From: Shea Levy <shea@shealevy.com>
+Date: Thu, 30 Apr 2015 17:13:35 -0400
+Subject: [PATCH] ATS-extsolve: Get rid of verbose . overload
+
+---
+ projects/MEDIUM/ATS-extsolve/solving/solver.dats | 2 +-
+ projects/MEDIUM/ATS-extsolve/solving/solver.sats | 6 ------
+ 2 files changed, 1 insertion(+), 7 deletions(-)
+
+diff --git a/projects/MEDIUM/ATS-extsolve/solving/solver.dats b/projects/MEDIUM/ATS-extsolve/solving/solver.dats
+index 8446cd5..f2f77b4 100644
+--- a/projects/MEDIUM/ATS-extsolve/solving/solver.dats
++++ b/projects/MEDIUM/ATS-extsolve/solving/solver.dats
+@@ -250,7 +250,7 @@ end // end of [c3nstr_solve_main]
+ implement c3nstr_solve (c3t, scripts, verbose) = let
+   var env : smtenv
+   val _ = smtenv_nil (env)
+-  val () = env.verbose (verbose)
++  val () = smtenv_set_verbose(env, verbose)
+   val () = 
+       case+ scripts of 
+           | list_nil () => ()
+diff --git a/projects/MEDIUM/ATS-extsolve/solving/solver.sats b/projects/MEDIUM/ATS-extsolve/solving/solver.sats
+index e43a028..dae452c 100644
+--- a/projects/MEDIUM/ATS-extsolve/solving/solver.sats
++++ b/projects/MEDIUM/ATS-extsolve/solving/solver.sats
+@@ -39,14 +39,8 @@ fun smtenv_load_scripts (env: &smtenv, scripts: List0(string)): void
+ 
+ fun smtenv_get_solver (env: &smtenv): solver
+ 
+-fun smtenv_get_verbose (env: &smtenv): bool
+-
+-overload .verbose with smtenv_get_verbose
+-
+ fun smtenv_set_verbose (env: &smtenv, verbose: bool): void
+ 
+-overload .verbose with smtenv_set_verbose
+-
+ fun formula_cst (s2c: s2cst): formula
+ 
+ (* ****** ****** *)
+From e3473a8d9dc7c56cda1111a439db7123254d00b4 Mon Sep 17 00:00:00 2001
+From: Shea Levy <shea@shealevy.com>
+Date: Thu, 30 Apr 2015 18:09:33 -0400
+Subject: [PATCH 1/2] solver_smt.dats: Don't use mapfree on linear list of
+ non-linear values
+
+---
+ projects/MEDIUM/ATS-extsolve/solving/solver_smt.dats | 5 +++--
+ 1 file changed, 3 insertions(+), 2 deletions(-)
+
+diff --git a/projects/MEDIUM/ATS-extsolve/solving/solver_smt.dats b/projects/MEDIUM/ATS-extsolve/solving/solver_smt.dats
+index 04055b9..b49602d 100644
+--- a/projects/MEDIUM/ATS-extsolve/solving/solver_smt.dats
++++ b/projects/MEDIUM/ATS-extsolve/solving/solver_smt.dats
+@@ -348,7 +348,7 @@ in
+         //
+         val () = assertloc (length(pairs) > 0)
+         //
+-        implement list_vt_mapfree$fopr<@(s2exp,s2exp)><formula>(x) = let
++        implement list_vt_map$fopr<@(s2exp,s2exp)><formula>(x) = let
+           val (pf, fpf | Env) = $UN.ptr1_vtake{smtenv}(addr@ env)
+           val met = formula_make (!Env, x.0)
+           val bound = formula_make (!Env, x.1)
+@@ -362,7 +362,8 @@ in
+         end
+         //
+         val assertions =
+-          list_vt_mapfree<(s2exp,s2exp)><formula> (pairs)
++          list_vt_map<(s2exp,s2exp)><formula> (pairs)
++        val () = list_vt_free(pairs)
+         //
+         implement 
+         list_vt_fold$init<formula><formula> (x) = x
+
+From 50de956561e6bf43190d7efb385bb6da658f1637 Mon Sep 17 00:00:00 2001
+From: Shea Levy <shea@shealevy.com>
+Date: Thu, 30 Apr 2015 18:18:56 -0400
+Subject: [PATCH 2/2] ats-extsolve/main.dats: Don't use mapfree on linear list
+ of non-linear values
+
+---
+ projects/MEDIUM/ATS-extsolve/main.dats | 7 ++++---
+ 1 file changed, 4 insertions(+), 3 deletions(-)
+
+diff --git a/projects/MEDIUM/ATS-extsolve/main.dats b/projects/MEDIUM/ATS-extsolve/main.dats
+index ac30ca0..930697d 100644
+--- a/projects/MEDIUM/ATS-extsolve/main.dats
++++ b/projects/MEDIUM/ATS-extsolve/main.dats
+@@ -34,7 +34,7 @@ dynload "commarg.dats"
+ 
+ (* ****** ****** *)
+ 
+-overload mapfree with list_vt_mapfree
++overload map with list_vt_map
+ overload filter with list_vt_filter
+ 
+ (* ****** ****** *)
+@@ -56,12 +56,13 @@ implement main0 (argc, argv) = let
+       | Script (s) => true
+       | _ =>> false
+   implement
+-  list_vt_mapfree$fopr<commarg><string> (x) =
++  list_vt_map$fopr<commarg><string> (x) =
+     case- x of
+       | Script (s) => s
+   //
+   val scriptargs = filter (list_vt_copy (args))
+-  val scripts = mapfree<commarg><string> (scriptargs)
++  val scripts = map<commarg><string> (scriptargs)
++  val () = list_vt_free (scriptargs)
+   //
+   implement
+   list_find$pred<commarg> (x) =
diff --git a/pkgs/development/compilers/ats2/default.nix b/pkgs/development/compilers/ats2/default.nix
index 304d5c284aea..8345a353f3f9 100644
--- a/pkgs/development/compilers/ats2/default.nix
+++ b/pkgs/development/compilers/ats2/default.nix
@@ -11,6 +11,8 @@ stdenv.mkDerivation rec {
 
   buildInputs = [ gmp ];
 
+  setupHook = ./setup-hook.sh;
+
   meta = {
     description = "Functional programming language with dependent types";
     homepage    = "http://www.ats-lang.org";
diff --git a/pkgs/development/compilers/ats2/setup-hook.sh b/pkgs/development/compilers/ats2/setup-hook.sh
new file mode 100644
index 000000000000..67647b1edf69
--- /dev/null
+++ b/pkgs/development/compilers/ats2/setup-hook.sh
@@ -0,0 +1 @@
+export PATSHOME=@out@/lib/ats2-postiats-@version@
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index e3f0d172705b..356ef9bb6902 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -3375,6 +3375,7 @@ let
 
   ats = callPackage ../development/compilers/ats { };
   ats2 = callPackage ../development/compilers/ats2 { };
+  ats-extsolve = callPackage ../development/compilers/ats-extsolve { };
 
   avra = callPackage ../development/compilers/avra { };