mirror of
https://github.com/NixOS/nixpkgs.git
synced 2024-11-16 23:03:40 +01:00
Add ats-extsolve (formerly patsolve)
This commit is contained in:
Shea Levy
parent
6823b5e657
commit
a704233a87
5 changed files with 175 additions and 0 deletions
35
pkgs/development/compilers/ats-extsolve/default.nix
Normal file
35
pkgs/development/compilers/ats-extsolve/default.nix
Normal file
|
|
@ -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 ];
|
||||
};
|
||||
}
|
||||
136
pkgs/development/compilers/ats-extsolve/misc-fixes.patch
Normal file
136
pkgs/development/compilers/ats-extsolve/misc-fixes.patch
Normal file
|
|
@ -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) =
|
||||
|
|
@ -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";
|
||||
|
|
|
|||
1
pkgs/development/compilers/ats2/setup-hook.sh
Normal file
1
pkgs/development/compilers/ats2/setup-hook.sh
Normal file
|
|
@ -0,0 +1 @@
|
|||
export PATSHOME=@out@/lib/ats2-postiats-@version@
|
||||
|
|
@ -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 { };
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue