diff options
Diffstat (limited to 'pkgs/development/compilers/ats-extsolve/misc-fixes.patch')
| -rw-r--r-- | pkgs/development/compilers/ats-extsolve/misc-fixes.patch | 136 |
1 files changed, 136 insertions, 0 deletions
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) = |