Inline ATS support for Pure

diff --git a/pure/examples/bitcode/inline_ats_examp.pure b/pure/examples/bitcode/inline_ats_examp.pure
new file mode 100644
--- /dev/null
+++ b/pure/examples/bitcode/inline_ats_examp.pure
@@ -0,0 +1,56 @@
+
+/* Example of inline code written in ATS. */
+
+%< -*- ATS -*-
+
+// A factorial function that verifies its result is the factorial;
+// based on an example given in ‘Introduction to Programming in ATS’
+// (which is available at http://www.ats-lang.org).
+//
+// The ifact function returns both the factorial and a proof, but the
+// proof code is ‘erased’ after type-checking, so the Pure program
+// sees only a function returning the factorial.
+
+#include "share/atspre_staload.hats"
+
+// A recursive definition of the factorial relation.
+// FACT (n, r) means ‘the factorial of n equals r’.
+// MUL (i, j, k) means ‘the product of i and j equals k’.
+dataprop FACT (int, int) =
+  | FACT_base (0, 1)
+  | {n : nat} {r1, r : int}
+    FACT_induction (n, r) of
+      (FACT (n-1, r1), MUL (n, r1, r))
+
+// Declare ifact as an ATS function that is referred to in C by the
+// name ‘ifact_nonneg’. The ‘ifact_nonneg’ function returns an integer
+// equal to r, where r satisfies the relation FACT (n, r).
+extern fun ifact :
+    {n : nat} (int n) -<> [r : int] (FACT (n, r) | int r) =
+      "ext#ifact_nonneg"
+
+implement ifact (n) =
+  let
+    fun fact {n : nat} .<n>. (n : int n) :<>
+        [r : int] (FACT (n, r) | int r) =
+      begin
+        if n > 0 then
+          let
+            val (pf1 | r1) = ifact (n - 1)
+            val (pfmul | r) = g1int_mul2 (n, r1)
+          in
+            (FACT_induction (pf1, pfmul) | r)
+          end
+        else
+          (FACT_base () | 1)
+      end
+  in
+    fact n
+  end
+
+%>
+
+ifact n::int = ifact_nonneg n if 0 <= n;
+
+map ifact (0..9);
+
diff --git a/pure/interpreter.cc b/pure/interpreter.cc
--- a/pure/interpreter.cc
+++ b/pure/interpreter.cc
@@ -2570,6 +2570,9 @@
      standards). If this is omitted, the default is old-style (fixed form)
      Fortran.

+   - "-*- ats -*-" selects ATS (PURE_ATSCC environment variable,
+     patscc -fplugin=dragonegg by default).
+
    - "-*- dsp:name -*-" selects Faust (PURE_FAUST environment variable, faust
      by default), where 'name' denotes the name of the Faust dsp, which is
      used as the namespace for the dsp interface functions.
@@ -2633,8 +2636,10 @@
 {
   // Get the language tag and configure accordingly.
   string modname, tag = lang_tag(code, modname), ext = "", optargs = "";
+  string intermediate_ext = "";
   const char *env, *drv, *args;
   char *asmargs = 0;
+  bool remove_intermediate = false;
   if (tag == "c") {
     env = "PURE_CC";
     drv = "clang";
@@ -2652,6 +2657,15 @@
     // gfortran doesn't understand -x, so we have to do some trickery with
     // filename extensions instead.
     args = " -emit-llvm -c "; ext = ".f"+std;
+  } else if (tag == "ats") {
+    env = "PURE_ATSCC";
+    // The default command is for ATS2-Postiats with gcc as the C
+    // compiler.
+    drv = "patscc -fplugin=dragonegg";
+    args = " -emit-llvm -c ";
+    ext = ".dats";
+    intermediate_ext = "_dats.c";
+    remove_intermediate = true;
   } else if (tag == "dsp") {
     env = "PURE_FAUST"; drv = "faust -double";
     args = " -lang llvm ";
@@ -2729,6 +2743,10 @@
     if (vflag) std::cerr << cmd << '\n';
     int status = system(cmd.c_str());
     unlink(nm.c_str());
+    if (remove_intermediate) {
+      string intermediate_name = string(fnm)+intermediate_ext;
+      unlink(intermediate_name.c_str());
+    }
     if (asmargs) free(asmargs);
     if (WIFEXITED(status) && WEXITSTATUS(status) == 0) {
       if (ext == ".ll") {