ats-extsolve: bump
This commit is contained in:
Shea Levy
parent
c0727fb751
commit
c13f189b19
@ -1,22 +1,21 @@
|
|||||||
{ stdenv, fetchurl, ats2, python, z3, pkgconfig, json_c }:
|
{ stdenv, fetchurl, ats2, python, z3, pkgconfig, json_c }:
|
||||||
|
|
||||||
stdenv.mkDerivation {
|
stdenv.mkDerivation {
|
||||||
name = "ats-extsolve-0pre6a9b752";
|
name = "ats-extsolve-0pre11177d9";
|
||||||
|
|
||||||
buildInputs = [ python z3 ats2 pkgconfig json_c ];
|
buildInputs = [ python z3 ats2 pkgconfig json_c ];
|
||||||
|
|
||||||
src = fetchurl {
|
src = fetchurl {
|
||||||
url = "https://github.com/githwxi/ATS-Postiats-contrib/archive/6a9b752efb8af1e4f77213f9e81fc2b7fa050877.tar.gz";
|
url = "https://github.com/wdblair/ATS-Postiats-contrib/archive/11177d9194b852392d5e92e67d0ecc7b6abc02bf.tar.gz";
|
||||||
sha256 = "1zz4fqjm1rdvpm0m0sdck6vx55iiqlk2p8z078fca2q9xyxqjkqd";
|
sha256 = "12fhlcpq5b4pc3h21w1i7yv1ymrll2g4zlf1pvg0v8cr6aa6i813";
|
||||||
};
|
};
|
||||||
|
|
||||||
postUnpack = ''
|
postUnpack = ''
|
||||||
export PATSHOMERELOC="$PWD/$sourceRoot";
|
export PATSHOMERELOC="$PWD/$sourceRoot"
|
||||||
export NIX_CFLAGS_COMPILE="$NIX_CFLAGS_COMPILE -I$PATSHOMERELOC"
|
export NIX_CFLAGS_COMPILE="$NIX_CFLAGS_COMPILE -I$PATSHOMERELOC"
|
||||||
|
export INCLUDE_ATS="-IATS $PATSHOMERELOC"
|
||||||
'';
|
'';
|
||||||
|
|
||||||
patches = [ ./misc-fixes.patch ];
|
|
||||||
|
|
||||||
preBuild = "cd projects/MEDIUM/ATS-extsolve";
|
preBuild = "cd projects/MEDIUM/ATS-extsolve";
|
||||||
|
|
||||||
buildFlags = [ "setup" "patsolve" ];
|
buildFlags = [ "setup" "patsolve" ];
|
||||||
|
|||||||
@ -1,136 +0,0 @@
|
|||||||
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) =
|
|
||||||
Loading…
x
Reference in New Issue
Block a user