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 +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 +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 +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)>(x) = let ++ implement list_vt_map$fopr<@(s2exp,s2exp)>(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)> (pairs) ++ list_vt_map<(s2exp,s2exp)> (pairs) ++ val () = list_vt_free(pairs) + // + implement + list_vt_fold$init (x) = x + +From 50de956561e6bf43190d7efb385bb6da658f1637 Mon Sep 17 00:00:00 2001 +From: Shea Levy +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 (x) = ++ list_vt_map$fopr (x) = + case- x of + | Script (s) => s + // + val scriptargs = filter (list_vt_copy (args)) +- val scripts = mapfree (scriptargs) ++ val scripts = map (scriptargs) ++ val () = list_vt_free (scriptargs) + // + implement + list_find$pred (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 { };