diff --git a/language-ats.cabal b/language-ats.cabal
--- a/language-ats.cabal
+++ b/language-ats.cabal
@@ -1,6 +1,6 @@
 cabal-version: 1.18
 name: language-ats
-version: 1.2.0.6
+version: 1.2.0.7
 license: BSD3
 license-file: LICENSE
 copyright: Copyright: (c) 2018 Vanessa McHale
@@ -47,7 +47,7 @@
         microlens-th -any,
         deepseq -any,
         ansi-wl-pprint >=0.6.8,
-        recursion-schemes >=5.0.1,
+        micro-recursion-schemes >=5.0.1,
         composition-prelude -any,
         containers -any,
         transformers -any
@@ -77,7 +77,6 @@
     
     if impl(ghc >=8.0)
         ghc-options: -Wincomplete-uni-patterns -Wincomplete-record-updates
-                     -Wcompat
 
 benchmark language-ats-bench
     type: exitcode-stdio-1.0
@@ -95,4 +94,3 @@
     
     if impl(ghc >=8.0)
         ghc-options: -Wincomplete-uni-patterns -Wincomplete-record-updates
-                     -Wcompat
diff --git a/src/Language/ATS/Lexer.x b/src/Language/ATS/Lexer.x
--- a/src/Language/ATS/Lexer.x
+++ b/src/Language/ATS/Lexer.x
@@ -34,7 +34,7 @@
 $octal = 0-7
 
 -- Characters
-$special = [\+\-\&\|\[\]\{\}\(\)\_\=\!\%\^\$\@\;\~\,\.\\\#\<\>\:\?]
+$special = [\+\-\*\&\|\[\]\{\}\(\)\_\=\!\%\^\$\@\;\~\,\.\\\#\<\>\:\?]
 $alpha = [a-zA-Z]
 $terminal = $printable # $white
 $esc_char = \27
diff --git a/src/Language/ATS/Parser.y b/src/Language/ATS/Parser.y
--- a/src/Language/ATS/Parser.y
+++ b/src/Language/ATS/Parser.y
@@ -170,6 +170,7 @@
     cloref1Arrow { Arrow $$ "=<cloref1>" }
     cloptr1Arrow { Arrow $$ "=<cloptr1>" }
     lincloptr1Arrow { Arrow $$ "=<lincloptr1>" }
+    lincloref1Arrow { Arrow $$ "=<lin,cloref1>" }
     spear { Arrow $$ "=>>" }
     proofArrow { Arrow $$ "=/=>" }
     lsqbracket { Special $$ "[" }
@@ -376,6 +377,7 @@
             | cloref1Arrow { Full $1 "cloref1" } -- FIXME this is a bad heuristic
             | cloptr1Arrow { Full $1 "cloptr1" }
             | lincloptr1Arrow { Full $1 "lincloptr1" }
+            | lincloref1Arrow { Full $1 "lin,cloref1" }
             | minus {% left $ Expected $1 "Arrow" "-" }
             | openParen {% left $ Expected $1 "Arrow" "(" }
             | closeParen {% left $ Expected $1 "Arrow" ")" }
@@ -457,6 +459,7 @@
               | let ATS in Expression end { Let $1 $2 (Just $4) }
               | let ATS in Expression vbar {% left $ Expected $5 "end" "|" }
               | let ATS fun {% left $ Expected $3 "in" "fun" }
+              | let ATS plainArrow {% left $ Expected $3 "in" "=>" } 
               | lambda Pattern LambdaArrow Expression { Lambda $1 $3 $2 $4 }
               | llambda Pattern LambdaArrow Expression { LinearLambda $1 $3 $2 $4 }
               | addrAt PreExpression { AddrAt $1 $2 }
@@ -513,6 +516,7 @@
 QuantifierArgs : comma_sep(IdentifierOr) { $1 }
                | { [] }
 
+-- FIXME handle [l:addr;n:int]
 Existential : lsqbracket QuantifierArgs colon Sort vbar StaticExpression rsqbracket { Existential $2 False (Just $4) (Just $6) }
             | lsqbracket QuantifierArgs colon Sort rsqbracket { Existential $2 False (Just $4) Nothing }
             | openExistential QuantifierArgs colon Sort rsqbracket { Existential $2 True (Just $4) Nothing }
@@ -870,7 +874,9 @@
             | cblock { CBlock $1 }
             | datasort identifierSpace eq DataSortLeaves { DataSort $1 (to_string $2) $4 }
             | macdef IdentifierOr doubleParens eq Expression { MacDecl $1 $2 [] $5 }
+            | macdef customOperator doubleParens eq Expression { MacDecl $1 (to_string $2) [] $5 }
             | macdef IdentifierOr openParen IdentifiersIn closeParen eq Expression { MacDecl $1 $2 $4 $7 }
+            | macdef customOperator openParen IdentifiersIn closeParen eq Expression { MacDecl $1 (to_string $2) $4 $7 }
             | lineComment { Comment (to_string $1) }
             | Comment { $1 }
             | Load underscore eq string { Load (fst $1) (get_staload $ snd $1) (Just "_") $4 }
diff --git a/src/Language/ATS/PrettyPrint.hs b/src/Language/ATS/PrettyPrint.hs
--- a/src/Language/ATS/PrettyPrint.hs
+++ b/src/Language/ATS/PrettyPrint.hs
@@ -132,6 +132,7 @@
         a (ParenExprF _ e)              = parens e
         a (UnaryF op e) = pretty op <> pretty e
         a (BinListF op@Add es)          = prettyBinary (pretty op) es
+        a (BinListF op@Con{} es)        = prettyBinary (pretty op) es
         a (BinaryF op e e')
             | splits op = e </> pretty op <+> e'
             | otherwise = e <+> pretty op <+> e'
diff --git a/src/Language/ATS/Types.hs b/src/Language/ATS/Types.hs
--- a/src/Language/ATS/Types.hs
+++ b/src/Language/ATS/Types.hs
@@ -1,3 +1,4 @@
+{-# OPTIONS_GHC -fno-warn-duplicate-exports #-}
 {-# LANGUAGE DeriveAnyClass             #-}
 {-# LANGUAGE DeriveDataTypeable         #-}
 {-# LANGUAGE DeriveFoldable             #-}
@@ -29,6 +30,7 @@
     , ExpressionF (..)
     , Implementation (..)
     , BinOp (..)
+    , BinOp (Con)
     , UnOp (..)
     , TypeF (..)
     , Existential (..)
@@ -261,6 +263,11 @@
              | SpecialInfix a String
              deriving (Show, Eq, Generic, NFData)
 
+
+pattern Con :: a -> BinOp a
+pattern Con l = SpecialInfix l "::"
+
+
 data StaticExpression a = StaticVal (Name a)
                         | StaticBinary (BinOp a) (StaticExpression a) (StaticExpression a)
                         | StaticInt Int
@@ -472,6 +479,8 @@
         | compareFixity st op' op'' = Binary op'' e (Binary op' e' e'')
     a (BinaryF Add e (BinList Add es))               = BinList Add (e : es)
     a (BinaryF Add e e')                             = BinList Add [e, e']
+    a (BinaryF Con{} e (BinList Add es))             = BinList (SpecialInfix undefined "::") (e : es)
+    a (BinaryF Con{} e e')                           = BinList (SpecialInfix undefined "::") [e, e']
     a (ParenExprF _ e@Precede{})                     = e
     a (ParenExprF _ e@PrecedeList{})                 = e
     a (WhereExpF e (ATS ds))                         = WhereExp e (ATS (rewriteDecl st <$> ds))
diff --git a/test/data/gmp.out b/test/data/gmp.out
new file mode 100644
--- /dev/null
+++ b/test/data/gmp.out
@@ -0,0 +1,955 @@
+(* ****** ****** *)
+//
+// API in ATS for libgmp
+//
+(* ****** ****** *)
+(*
+** ATS/Postiats - Unleashing the Potential of Types!
+** Copyright (C) 2011-2013 Hongwei Xi, ATS Trustful Software, Inc.
+** All rights reserved
+**
+** Permission to use, copy, modify, and distribute this software for any
+** purpose with or without fee is hereby granted, provided that the above
+** copyright notice and this permission notice appear in all copies.
+** 
+** THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+** WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+** MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
+** ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+** WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+** ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
+** OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
+*)
+(* ****** ****** *)
+(*
+** Author: Hongwei Xi // MPZ and MPQ
+** Authoremail: hwxi AT cs DOT bu DOT edu
+*)
+(*
+** Author: Shivkumar Chandrasekaran // MPF
+** Authoremail: shiv AT ece DOT ucsb DOT edu)
+*)
+(* ****** ****** *)
+//
+%{#
+//
+#include \
+"atscntrb-hx-libgmp/CATS/gmp.cats"
+//
+%}
+
+// end of [%{#]
+//
+(* ****** ****** *)
+//
+#define ATS_PACKNAME "ATSCNTRB.gmp"
+
+//
+(* ****** ****** *)
+//
+// HX: prefix for extern names
+// HX: prefix for static names
+//
+#define ATS_EXTERN_PREFIX"atscntrb_gmp_"
+#define ATS_EXTERN_STATIC"_atscntrb_gmp_"
+
+//
+(* ****** ****** *)
+//
+// integral numbers
+//
+absvt@ype mpz_vt0ype = $extype "atscntrb_gmp_mpz"
+
+//
+// rational numbers
+//
+absvt@ype mpq_vt0ype = $extype "atscntrb_gmp_mpq"
+
+//
+// floating point numbers
+//
+absvt@ype mpf_vt0ype = $extype "atscntrb_gmp_mpf"
+
+//
+(* ****** ****** *)
+//
+stadef mpz  = mpz_vt0ype: vt@ype
+stadef mpq  = mpq_vt0ype: vt@ype
+stadef mpf  = mpf_vt0ype: vt@ype
+
+//
+(* ****** ****** *)
+//
+// HX: for
+// outputing MP numbers
+//
+typedef mp_base = intBtwe(2, 36): t@ype
+
+//
+(* ****** ****** *)
+//
+// integral number operations
+//
+(* ****** ****** *)
+//
+// [x] is initialized with 0
+//
+fun mpz_init(x : &mpz? >> mpz) : void =
+  "mac#%"
+
+//
+(* ****** ****** *)
+//
+// [x] is initialized with 0 while given [n]-bit space
+//
+fun mpz_init2(x : &mpz? >> mpz, n : ulint) : void =
+  "mac#%"
+
+//
+(* ****** ****** *)
+//
+// [x] is cleared
+//
+fun mpz_clear(x : &mpz >> mpz?) : void =
+  "mac#%"
+
+//
+(* ****** ****** *)
+//
+// [x] is reallocated
+// the original value of [x] is carried over if there
+// is enough space, or 0 is assigned to [x] otherwise.
+//
+fun mpz_realloc2(x : &mpz >> mpz, n : ulint) : void =
+  "mac#%"
+
+//
+(* ****** ****** *)
+//
+fun mpz_get_int(x : &RD(mpz)) : int =
+  "mac#%"
+
+fun mpz_get_lint(x : &RD(mpz)) : lint =
+  "mac#%"
+
+//
+fun mpz_get_uint(x : &RD(mpz)) : uint =
+  "mac#%"
+
+fun mpz_get_ulint(x : &RD(mpz)) : ulint =
+  "mac#%"
+
+//
+fun mpz_get_double(x : &RD(mpz)) : double =
+  "mac#%"
+
+//
+(* ****** ****** *)
+//
+// HX-2013-04:
+// [res] should hold enough memory for output
+//
+fun mpz_get_str(res : ptr, base : mp_base, x : &RD(mpz)) : Strptr1 =
+  "mac#%"
+
+fun mpz_get_str_null(base : mp_base, x : &RD(mpz)) : Strptr1 =
+  "mac#%"
+
+//
+(* ****** ****** *)
+//
+// x := y
+//
+fun mpz_set_int(x : &mpz >> _, y : int) : void =
+  "mac#%"
+
+fun mpz_set_lint(x : &mpz >> _, y : lint) : void =
+  "mac#%"
+
+//
+fun mpz_set_uint(x : &mpz >> _, y : uint) : void =
+  "mac#%"
+
+fun mpz_set_ulint(x : &mpz >> _, y : ulint) : void =
+  "mac#%"
+
+//
+fun mpz_set_double(x : &mpz >> _, y : double) : void =
+  "mac#%"
+
+//
+fun mpz_set_mpz(x : &mpz >> _, y : &RD(mpz)) : void =
+  "mac#%"
+
+fun mpz_set_mpq(x : &mpz >> _, y : &RD(mpq)) : void =
+  "mac#%"
+
+fun mpz_set_mpf(x : &mpz >> _, y : &RD(mpf)) : void =
+  "mac#%"
+
+//
+(* ****** ****** *)
+//
+// HX: the function returns 0/-1 if the string is valid/not
+//
+fun mpz_set_str(x : &mpz >> _, inp : string, base : mp_base) : int =
+  "mac#%"
+
+// end of [mpz_set_str]
+//
+fun mpz_set_str_exn(x : &mpz >> _, inp : string, base : mp_base) :
+  void =
+  "mac#%"
+
+// end of [mpz_set_str_exn]
+(* ****** ****** *)
+//
+fun mpz_init_set_mpz(x : &mpz? >> mpz, y : &mpz) : void =
+  "mac#%"
+
+//
+fun mpz_init_set_int(x : &mpz? >> mpz, y : int) : void =
+  "mac#%"
+
+fun mpz_init_set_uint(x : &mpz? >> mpz, y : uint) : void =
+  "mac#%"
+
+fun mpz_init_set_lint(x : &mpz? >> mpz, y : lint) : void =
+  "mac#%"
+
+fun mpz_init_set_ulint(x : &mpz? >> mpz, y : ulint) : void =
+  "mac#%"
+
+//
+symintr mpz_init_set
+
+// x := y
+//
+overload mpz_init_set with mpz_init_set_mpz
+
+overload mpz_init_set with mpz_init_set_int
+
+overload mpz_init_set with mpz_init_set_uint
+
+overload mpz_init_set with mpz_init_set_lint
+
+overload mpz_init_set with mpz_init_set_ulint
+
+//
+(* ****** ****** *)
+fun mpz_size(x : &RD(mpz)) : size_t =
+  "mac#%"
+
+(* ****** ****** *)
+//
+fun mpz_out_str(out : FILEref, base : mp_base, x : &RD(mpz)) : size_t =
+  "mac#%"
+
+// end of [mpz_out_str]
+fun mpz_inp_str(x : &mpz >> _, inp : FILEref, base : mp_base) : size_t =
+  "mac#%"
+
+// end of [mpz_inp_str]
+//
+(* ****** ****** *)
+//
+fun fprint_mpz(out : FILEref, x : &RD(mpz)) : void =
+  "mac#%"
+
+fun fprint_mpz_base(out : FILEref, x : &RD(mpz), base : mp_base) :
+  void =
+  "mac#%"
+
+//
+overload fprint with fprint_mpz
+
+overload fprint with fprint_mpz_base
+
+//
+(* ****** ****** *)
+fun mpz_out_raw(out : FILEref, x : &RD(mpz)) : size_t =
+  "mac#%"
+
+fun mpz_inp_raw(x : &mpz >> _, out : FILEref) : size_t =
+  "mac#%"
+
+(* ****** ****** *)
+fun mpz_odd_p(x : &RD(mpz)) :<> bool =
+  "mac#%"
+
+fun mpz_even_p(x : &RD(mpz)) :<> bool =
+  "mac#%"
+
+(* ****** ****** *)
+//
+// HX: negation
+//
+symintr mpz_neg
+
+//
+// x := -x // -y
+//
+fun mpz_neg1(x : &mpz >> _) : void =
+  "mac#%"
+
+fun mpz_neg2(x : &mpz >> _, y : &mpz) : void =
+  "mac#%"
+
+overload mpz_neg with mpz_neg1
+
+overload mpz_neg with mpz_neg2
+
+//
+(* ****** ****** *)
+//
+// absolute value
+//
+symintr mpz_abs
+
+//
+// x := |x| // |y|
+//
+fun mpz_abs1(x : &mpz >> _) : void =
+  "mac#%"
+
+fun mpz_abs2(x : &mpz >> _, y : &mpz) : void =
+  "mac#%"
+
+overload mpz_abs with mpz_abs1
+
+overload mpz_abs with mpz_abs2
+
+//
+(* ****** ****** *)
+//
+// addition
+//
+symintr mpz_add
+
+//
+fun mpz_add2_mpz(x : &mpz >> _, y : &mpz) : void =
+  "mac#%"
+
+fun mpz_add2_int(x : &mpz >> _, y : int) : void =
+  "mac#%"
+
+fun mpz_add2_lint(x : &mpz >> _, y : lint) : void =
+  "mac#%"
+
+fun mpz_add2_uint(x : &mpz >> _, y : uint) : void =
+  "mac#%"
+
+fun mpz_add2_ulint(x : &mpz >> _, y : ulint) : void =
+  "mac#%"
+
+fun mpz_add3_mpz(x : &mpz >> _, y : &mpz, z : &mpz) : void =
+  "mac#%"
+
+fun mpz_add3_int(x : &mpz >> _, y : &mpz, z : int) : void =
+  "mac#%"
+
+fun mpz_add3_lint(x : &mpz >> _, y : &mpz, z : lint) : void =
+  "mac#%"
+
+fun mpz_add3_uint(x : &mpz >> _, y : &mpz, z : uint) : void =
+  "mac#%"
+
+fun mpz_add3_ulint(x : &mpz >> _, y : &mpz, z : ulint) : void =
+  "mac#%"
+
+//
+overload mpz_add with mpz_add2_mpz
+
+overload mpz_add with mpz_add2_int
+
+overload mpz_add with mpz_add2_lint
+
+overload mpz_add with mpz_add2_uint
+
+overload mpz_add with mpz_add2_ulint
+
+overload mpz_add with mpz_add3_mpz
+
+overload mpz_add with mpz_add3_int
+
+overload mpz_add with mpz_add3_lint
+
+overload mpz_add with mpz_add3_uint
+
+overload mpz_add with mpz_add3_ulint
+
+//
+(* ****** ****** *)
+//
+// subtraction
+//
+fun mpz_sub2_mpz(x : &mpz >> _, y : &mpz) : void =
+  "mac#%"
+
+fun mpz_sub2_int(x : &mpz >> _, y : int) : void =
+  "mac#%"
+
+fun mpz_sub2_lint(x : &mpz >> _, y : lint) : void =
+  "mac#%"
+
+fun mpz_sub2_uint(x : &mpz >> _, y : uint) : void =
+  "mac#%"
+
+fun mpz_sub2_ulint(x : &mpz >> _, y : ulint) : void =
+  "mac#%"
+
+fun mpz_sub3_mpz(x : &mpz >> _, y : &mpz, z : &mpz) : void =
+  "mac#%"
+
+fun mpz_sub3_int(x : &mpz >> _, y : &mpz, z : int) : void =
+  "mac#%"
+
+fun mpz_sub3_lint(x : &mpz >> _, y : &mpz, z : lint) : void =
+  "mac#%"
+
+fun mpz_sub3_uint(x : &mpz >> _, y : &mpz, z : uint) : void =
+  "mac#%"
+
+fun mpz_sub3_ulint(x : &mpz >> _, y : &mpz, z : ulint) : void =
+  "mac#%"
+
+//
+symintr mpz_sub
+
+//
+overload mpz_sub with mpz_sub2_mpz
+
+overload mpz_sub with mpz_sub2_int
+
+overload mpz_sub with mpz_sub2_lint
+
+overload mpz_sub with mpz_sub2_uint
+
+overload mpz_sub with mpz_sub2_ulint
+
+overload mpz_sub with mpz_sub3_mpz
+
+overload mpz_sub with mpz_sub3_int
+
+overload mpz_sub with mpz_sub3_lint
+
+overload mpz_sub with mpz_sub3_uint
+
+overload mpz_sub with mpz_sub3_ulint
+
+//
+(* ****** ****** *)
+//
+// multiplication
+//
+fun mpz_mul2_mpz(x : &mpz >> _, y : &mpz) : void =
+  "mac#%"
+
+fun mpz_mul2_int(x : &mpz >> _, y : int) : void =
+  "mac#%"
+
+fun mpz_mul2_lint(x : &mpz >> _, y : lint) : void =
+  "mac#%"
+
+fun mpz_mul2_uint(x : &mpz >> _, y : uint) : void =
+  "mac#%"
+
+fun mpz_mul2_ulint(x : &mpz >> _, y : ulint) : void =
+  "mac#%"
+
+fun mpz_mul3_mpz(x : &mpz >> _, y : &mpz, z : &mpz) : void =
+  "mac#%"
+
+fun mpz_mul3_int(x : &mpz >> _, y : &mpz, z : int) : void =
+  "mac#%"
+
+fun mpz_mul3_lint(x : &mpz >> _, y : &mpz, z : lint) : void =
+  "mac#%"
+
+fun mpz_mul3_uint(x : &mpz >> _, y : &mpz, z : uint) : void =
+  "mac#%"
+
+fun mpz_mul3_ulint(x : &mpz >> _, y : &mpz, z : ulint) : void =
+  "mac#%"
+
+//
+symintr mpz_mul
+
+//
+overload mpz_mul with mpz_mul2_mpz
+
+overload mpz_mul with mpz_mul2_int
+
+overload mpz_mul with mpz_mul2_lint
+
+overload mpz_mul with mpz_mul2_uint
+
+overload mpz_mul with mpz_mul2_ulint
+
+overload mpz_mul with mpz_mul3_mpz
+
+overload mpz_mul with mpz_mul3_int
+
+overload mpz_mul with mpz_mul3_lint
+
+overload mpz_mul with mpz_mul3_uint
+
+overload mpz_mul with mpz_mul3_ulint
+
+//
+(* ****** ****** *)
+(*
+**
+** Author: Zhiqiang Ren
+** Authoremail: arenATcsDOTbuDOTedu
+**
+** Description:
+** Set res to arg * (2 ^ exp)
+** The same object can be passed for both res and arg1.
+** It's up to an application to call functions like mpz_mul_2exp when appropriate.
+** General purpose functions like mpz_mul make no attempt to identify powers of two
+** or other special forms.
+**
+*)
+//
+fun mpz_mul3_2exp(res : &mpz >> _, arg : &mpz, exp : ulint) : void =
+  "mac#%"
+
+// end-of-function
+//
+symintr mpz_mul_2exp
+
+//
+overload mpz_mul_2exp with mpz_mul3_2exp
+
+//
+(* ****** ****** *)
+//
+// trunc-division-functions
+// x := trunc(x/y) // trunc(y/z)
+//
+fun mpz_tdiv2_q_mpz(x : &mpz >> _, y : &mpz) : void =
+  "mac#%"
+
+fun mpz_tdiv2_q_uint(x : &mpz >> _, y : uint) : void =
+  "mac#%"
+
+fun mpz_tdiv2_q_ulint(x : &mpz >> _, y : ulint) : void =
+  "mac#%"
+
+//
+fun mpz_tdiv3_q_mpz(x : &mpz >> _, y : &mpz, z : &mpz) : void =
+  "mac#%"
+
+fun mpz_tdiv3_q_uint(x : &mpz >> _, y : &mpz, z : uint) : void =
+  "mac#%"
+
+fun mpz_tdiv3_q_ulint(x : &mpz >> _, y : &mpz, z : ulint) : void =
+  "mac#%"
+
+//
+symintr mpz_tdiv_q
+
+//
+overload mpz_tdiv_q with mpz_tdiv2_q_mpz
+
+overload mpz_tdiv_q with mpz_tdiv2_q_uint
+
+overload mpz_tdiv_q with mpz_tdiv2_q_ulint
+
+overload mpz_tdiv_q with mpz_tdiv3_q_mpz
+
+overload mpz_tdiv_q with mpz_tdiv3_q_uint
+
+overload mpz_tdiv_q with mpz_tdiv3_q_ulint
+
+//
+// x := x-trunc(x/y)*y // y-trunc(y/z)*z
+//
+fun mpz_tdiv2_r_mpz(x : &mpz >> _, y : &mpz) : void =
+  "mac#%"
+
+fun mpz_tdiv2_r_uint(x : &mpz >> _, y : uint) : void =
+  "mac#%"
+
+fun mpz_tdiv2_r_ulint(x : &mpz >> _, y : ulint) : void =
+  "mac#%"
+
+fun mpz_tdiv3_r_mpz(x : &mpz >> _, y : &mpz, z : &mpz) : void =
+  "mac#%"
+
+fun mpz_tdiv3_r_uint(x : &mpz >> _, y : &mpz, z : uint) : void =
+  "mac#%"
+
+fun mpz_tdiv3_r_ulint(x : &mpz >> _, y : &mpz, z : ulint) : void =
+  "mac#%"
+
+//
+symintr mpz_tdiv_r
+
+//
+overload mpz_tdiv_r with mpz_tdiv2_r_mpz
+
+overload mpz_tdiv_r with mpz_tdiv2_r_uint
+
+overload mpz_tdiv_r with mpz_tdiv2_r_ulint
+
+overload mpz_tdiv_r with mpz_tdiv3_r_mpz
+
+overload mpz_tdiv_r with mpz_tdiv3_r_uint
+
+overload mpz_tdiv_r with mpz_tdiv3_r_ulint
+
+//
+(* ****** ****** *)
+//
+fun mpz_tdiv3_qr_mpz(xq : &mpz >> _, xr : &mpz >> _, y : &mpz) : void =
+  "mac#%"
+
+fun mpz_tdiv3_qr_uint(xq : &mpz >> _, xr : &mpz >> _, y : uint) : void =
+  "mac#%"
+
+fun mpz_tdiv3_qr_ulint(xq : &mpz >> _, xr : &mpz >> _, y : ulint) :
+  void =
+  "mac#%"
+
+fun mpz_tdiv4_qr_mpz( xq : &mpz >> _
+                    , xr : &mpz >> _
+                    , y : &mpz
+                    , z : &mpz
+                    ) : void =
+  "mac#%"
+
+fun mpz_tdiv4_qr_uint( xq : &mpz >> _
+                     , xr : &mpz >> _
+                     , y : &mpz
+                     , z : uint
+                     ) : void =
+  "mac#%"
+
+fun mpz_tdiv4_qr_ulint( xq : &mpz >> _
+                      , xr : &mpz >> _
+                      , y : &mpz
+                      , z : ulint
+                      ) : void =
+  "mac#%"
+
+//
+symintr mpz_tdiv_qr
+
+//
+overload mpz_tdiv_qr with mpz_tdiv3_qr_mpz
+
+overload mpz_tdiv_qr with mpz_tdiv3_qr_uint
+
+overload mpz_tdiv_qr with mpz_tdiv3_qr_ulint
+
+overload mpz_tdiv_qr with mpz_tdiv4_qr_mpz
+
+overload mpz_tdiv_qr with mpz_tdiv4_qr_uint
+
+overload mpz_tdiv_qr with mpz_tdiv4_qr_ulint
+
+//
+(* ****** ****** *)
+//
+// floor-division-functions
+//
+fun mpz_fdiv_uint(x : &mpz, d : uint) : uint =
+  "mac#%"
+
+fun mpz_fdiv_ulint(x : &mpz, d : ulint) : ulint =
+  "mac#%"
+
+//
+symintr mpz_fdiv
+
+//
+overload mpz_fdiv with mpz_fdiv_uint
+
+overload mpz_fdiv with mpz_fdiv_ulint
+
+//
+// x := floor(x/y) // floor(y/z)
+//
+fun mpz_fdiv2_q_uint(x : &mpz >> _, y : uint) : void =
+  "mac#%"
+
+fun mpz_fdiv2_q_ulint(x : &mpz >> _, y : ulint) : void =
+  "mac#%"
+
+fun mpz_fdiv3_q_uint(x : &mpz >> _, y : &mpz, z : uint) : void =
+  "mac#%"
+
+fun mpz_fdiv3_q_ulint(x : &mpz >> _, y : &mpz, z : ulint) : void =
+  "mac#%"
+
+//
+symintr mpz_fdiv_q
+
+//
+overload mpz_fdiv_q with mpz_fdiv2_q_uint
+
+overload mpz_fdiv_q with mpz_fdiv2_q_ulint
+
+overload mpz_fdiv_q with mpz_fdiv3_q_uint
+
+overload mpz_fdiv_q with mpz_fdiv3_q_ulint
+
+//
+(* ****** ****** *)
+(*
+**
+**
+** Author: Zhiqiang Ren
+** Authoremail: arenATcsDOTbuDOTedu
+**
+** Description:
+** Set quot and rem so that dividend = quot * divisor + rem
+** Rounds quot down towards negative infinity, and rem will
+** have the same sign as divisor, and 0 <= |rem| < |divisor|.
+** The same object cannot be passed for both quot and rem, or the result will be
+** unpredictable. No other constraints on the passing arguments.
+*)
+//
+fun mpz_fdiv4_qr_mpz( quot : &mpz >> _
+                    , rem : &mpz >> _
+                    , dividend : &mpz
+                    , divisor : &mpz
+                    ) :<> void =
+  "mac#%"
+
+fun mpz_fdiv4_qr_ulint( quot : &mpz >> _
+                      , rem : &mpz >> _
+                      , dividend : &mpz
+                      , divisor : ulint
+                      ) :<> ulint =
+  "mac#%"
+
+//
+symintr mpz_fdiv_qr
+
+//
+overload mpz_fdiv_qr with mpz_fdiv4_qr_mpz
+
+overload mpz_fdiv_qr with mpz_fdiv4_qr_ulint
+
+//
+(* ****** ****** *)
+//
+// ceiling-division-functions
+//
+fun mpz_cdiv_uint(x : &mpz, d : uint) : uint =
+  "mac#%"
+
+fun mpz_cdiv_ulint(x : &mpz, d : ulint) : ulint =
+  "mac#%"
+
+//
+symintr mpz_cdiv
+
+//
+overload mpz_cdiv with mpz_cdiv_uint
+
+overload mpz_cdiv with mpz_cdiv_ulint
+
+//
+// x := ceiling(x/y) // ceiling(y/z)
+//
+fun mpz_cdiv2_q_uint(x : &mpz >> _, y : uint) : void =
+  "mac#%"
+
+fun mpz_cdiv2_q_ulint(x : &mpz >> _, y : uint) : void =
+  "mac#%"
+
+fun mpz_cdiv3_q_uint(x : &mpz >> _, y : &mpz, z : uint) : void =
+  "mac#%"
+
+fun mpz_cdiv3_q_ulint(x : &mpz >> _, y : &mpz, z : ulint) : void =
+  "mac#%"
+
+//
+symintr mpz_cdiv_q
+
+//
+overload mpz_cdiv_q with mpz_cdiv2_q_uint
+
+overload mpz_cdiv_q with mpz_cdiv2_q_ulint
+
+overload mpz_cdiv_q with mpz_cdiv3_q_uint
+
+overload mpz_cdiv_q with mpz_cdiv3_q_ulint
+
+//
+(* ****** ****** *)
+//
+// modulo-functions
+//
+fun mpz_mod2_mpz(r : &mpz >> _, d : &mpz) : void =
+  "mac#%"
+
+//
+fun mpz_mod2_uint(r : &mpz >> _, d : uint) : uint =
+  "mac#%"
+
+//
+fun mpz_mod2_ulint(r : &mpz >> _, d : ulint) : ulint =
+  "mac#%"
+
+//
+fun mpz_mod3_mpz(r : &mpz >> _, n : &mpz, d : &mpz) : void =
+  "mac#%"
+
+fun mpz_mod3_uint(r : &mpz >> _, n : &mpz, d : uint) : uint =
+  "mac#%"
+
+fun mpz_mod3_ulint(r : &mpz >> _, n : &mpz, d : ulint) : ulint =
+  "mac#%"
+
+//
+symintr mpz_mod
+
+//
+overload mpz_mod with mpz_mod2_mpz
+
+overload mpz_mod with mpz_mod2_uint
+
+overload mpz_mod with mpz_mod2_ulint
+
+overload mpz_mod with mpz_mod3_mpz
+
+overload mpz_mod with mpz_mod3_uint
+
+overload mpz_mod with mpz_mod3_ulint
+
+//
+(* ****** ****** *)
+//
+// add/mul combination
+// addmul (x, y, z): x := x + y * z
+//
+fun mpz_addmul3_mpz(x : &mpz >> _, y : &mpz, z : &mpz) : void =
+  "mac#%"
+
+fun mpz_addmul3_uint(x : &mpz >> _, y : &mpz, z : uint) : void =
+  "mac#%"
+
+fun mpz_addmul3_ulint(x : &mpz >> _, y : &mpz, z : ulint) : void =
+  "mac#%"
+
+//
+symintr mpz_addmul
+
+//
+overload mpz_addmul with mpz_addmul3_mpz
+
+overload mpz_addmul with mpz_addmul3_uint
+
+overload mpz_addmul with mpz_addmul3_ulint
+
+//
+// sub/mul combination
+// submul (x, y, z): x := x - y * z
+//
+fun mpz_submul3_mpz(x : &mpz >> _, y : &mpz, z : &mpz) : void =
+  "mac#%"
+
+fun mpz_submul3_uint(x : &mpz >> _, y : &mpz, z : uint) : void =
+  "mac#%"
+
+fun mpz_submul3_ulint(x : &mpz >> _, y : &mpz, z : ulint) : void =
+  "mac#%"
+
+//
+symintr mpz_submul
+
+//
+overload mpz_submul with mpz_submul3_mpz
+
+overload mpz_submul with mpz_submul3_uint
+
+overload mpz_submul with mpz_submul3_ulint
+
+//
+(* ****** ****** *)
+//
+// comparison-functions
+//
+fun mpz_cmp_mpz(x : &mpz, y : &mpz) :<> int =
+  "mac#%"
+
+fun mpz_cmp_int(x : &mpz, y : int) :<> int =
+  "mac#%"
+
+fun mpz_cmp_uint(x : &mpz, y : uint) :<> int =
+  "mac#%"
+
+fun mpz_cmp_lint(x : &mpz, y : lint) :<> int =
+  "mac#%"
+
+fun mpz_cmp_ulint(x : &mpz, y : ulint) :<> int =
+  "mac#%"
+
+//
+symintr mpz_cmp
+
+//
+overload mpz_cmp with mpz_cmp_mpz
+
+overload mpz_cmp with mpz_cmp_int
+
+overload mpz_cmp with mpz_cmp_uint
+
+overload mpz_cmp with mpz_cmp_lint
+
+overload mpz_cmp with mpz_cmp_ulint
+
+//
+(* ****** ****** *)
+//
+fun mpz_fac_uint(x : &mpz >> _, n : uint) : void =
+  "mac#%"
+
+//
+(* ****** ****** *)
+//
+fun mpz_pow_uint(pwr : &mpz >> _, base : &mpz, exp : uint) : void =
+  "mac#%"
+
+fun mpz_pow_ulint(pwr : &mpz >> _, base : &mpz, exp : ulint) : void =
+  "mac#%"
+
+//
+fun mpz_ui_pow_ui(pwr : &mpz >> _, base : ulint, exp : ulint) : void =
+  "mac#%"
+
+//
+symintr mpz_pow
+
+//
+overload mpz_pow with mpz_cmp_uint
+
+overload mpz_pow with mpz_cmp_ulint
+
+//
+(* ****** ****** *)
+//
+fun mpz_fib_uint(x : &mpz >> _, n : uint) : void =
+  "mac#%"
+
+fun mpz_fib2_uint(x1 : &mpz >> _, x2 : &mpz >> _, n : uint) : void =
+  "mac#%"
+
+//
+symintr mpz_fib
+
+symintr mpz_fib2
+
+//
+overload mpz_fib with mpz_fib_uint
+
+overload mpz_fib2 with mpz_fib2_uint
+
+//
+(* ****** ****** *)
+(* end of [gmp.sats] *)
diff --git a/test/data/gmp.sats b/test/data/gmp.sats
new file mode 100644
--- /dev/null
+++ b/test/data/gmp.sats
@@ -0,0 +1,747 @@
+(* ****** ****** *)
+//
+// API in ATS for libgmp
+//
+(* ****** ****** *)
+
+(*
+** ATS/Postiats - Unleashing the Potential of Types!
+** Copyright (C) 2011-2013 Hongwei Xi, ATS Trustful Software, Inc.
+** All rights reserved
+**
+** Permission to use, copy, modify, and distribute this software for any
+** purpose with or without fee is hereby granted, provided that the above
+** copyright notice and this permission notice appear in all copies.
+** 
+** THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+** WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+** MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
+** ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+** WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+** ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
+** OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
+*)
+
+(* ****** ****** *)
+
+(*
+** Author: Hongwei Xi // MPZ and MPQ
+** Authoremail: hwxi AT cs DOT bu DOT edu
+*)
+(*
+** Author: Shivkumar Chandrasekaran // MPF
+** Authoremail: shiv AT ece DOT ucsb DOT edu)
+*)
+
+(* ****** ****** *)
+//
+%{#
+//
+#include \
+"atscntrb-hx-libgmp/CATS/gmp.cats"
+//
+%} // end of [%{#]
+//
+(* ****** ****** *)
+//
+#define ATS_PACKNAME "ATSCNTRB.gmp"
+//
+(* ****** ****** *)
+//
+// HX: prefix for extern names
+// HX: prefix for static names
+//
+#define
+ATS_EXTERN_PREFIX "atscntrb_gmp_"
+#define
+ATS_EXTERN_STATIC "_atscntrb_gmp_"
+//
+(* ****** ****** *)
+//
+// integral numbers
+//
+absvt@ype
+mpz_vt0ype =
+$extype"atscntrb_gmp_mpz"
+//
+// rational numbers
+//
+absvt@ype
+mpq_vt0ype =
+$extype"atscntrb_gmp_mpq"
+//
+// floating point numbers
+//
+absvt@ype
+mpf_vt0ype =
+$extype"atscntrb_gmp_mpf"
+//
+(* ****** ****** *)
+//
+stadef mpz = mpz_vt0ype: vt@ype
+stadef mpq = mpq_vt0ype: vt@ype
+stadef mpf = mpf_vt0ype: vt@ype
+//
+(* ****** ****** *)
+//
+// HX: for
+// outputing MP numbers
+//
+typedef
+mp_base = intBtwe(2, 36): t@ype
+//
+(* ****** ****** *)
+//
+// integral number operations
+//
+(* ****** ****** *)
+//
+// [x] is initialized with 0
+//
+fun mpz_init
+  (x: &mpz? >> mpz): void = "mac#%"
+//
+(* ****** ****** *)
+//
+// [x] is initialized with 0 while given [n]-bit space
+//
+fun mpz_init2
+  (x: &mpz? >> mpz, n: ulint): void = "mac#%"
+//
+(* ****** ****** *)
+//
+// [x] is cleared
+//
+fun mpz_clear(x: &mpz >> mpz?): void = "mac#%"
+//
+(* ****** ****** *)
+//
+// [x] is reallocated
+// the original value of [x] is carried over if there
+// is enough space, or 0 is assigned to [x] otherwise.
+//
+fun mpz_realloc2
+  (x: &mpz >> mpz, n: ulint): void = "mac#%"
+//
+(* ****** ****** *)
+//
+fun mpz_get_int (x: &RD(mpz)): int = "mac#%"
+fun mpz_get_lint (x: &RD(mpz)): lint = "mac#%"
+//
+fun mpz_get_uint (x: &RD(mpz)): uint = "mac#%"
+fun mpz_get_ulint (x: &RD(mpz)): ulint = "mac#%"
+//
+fun mpz_get_double (x: &RD(mpz)): double = "mac#%"
+//
+(* ****** ****** *)
+//
+// HX-2013-04:
+// [res] should hold enough memory for output
+//
+fun mpz_get_str
+(
+  res: ptr
+, base: mp_base, x: &RD(mpz)
+) : Strptr1 = "mac#%"
+fun mpz_get_str_null
+   (base: mp_base, x: &RD(mpz)) : Strptr1 = "mac#%"
+//
+(* ****** ****** *)
+//
+// x := y
+//
+fun mpz_set_int
+  (x: &mpz >> _, y: int): void = "mac#%"
+fun mpz_set_lint
+  (x: &mpz >> _, y: lint): void = "mac#%"
+//
+fun mpz_set_uint
+  (x: &mpz >> _, y: uint): void = "mac#%"
+fun mpz_set_ulint
+  (x: &mpz >> _, y: ulint): void = "mac#%"
+//
+fun mpz_set_double
+  (x: &mpz >> _, y: double): void = "mac#%"
+//
+fun mpz_set_mpz
+  (x: &mpz >> _, y: &RD(mpz)): void = "mac#%"
+fun mpz_set_mpq
+  (x: &mpz >> _, y: &RD(mpq)): void = "mac#%"
+fun mpz_set_mpf
+  (x: &mpz >> _, y: &RD(mpf)): void = "mac#%"
+//
+(* ****** ****** *)
+//
+// HX: the function returns 0/-1 if the string is valid/not
+//
+fun mpz_set_str
+  (x: &mpz >> _, inp: string, base: mp_base): int = "mac#%"
+// end of [mpz_set_str]
+//
+fun mpz_set_str_exn
+  (x: &mpz >> _, inp: string, base: mp_base): void = "mac#%"
+// end of [mpz_set_str_exn]
+
+(* ****** ****** *)
+//
+fun
+mpz_init_set_mpz
+  (x: &mpz? >> mpz, y: &mpz): void = "mac#%"
+//
+fun
+mpz_init_set_int
+  (x: &mpz? >> mpz, y: int): void = "mac#%"
+fun
+mpz_init_set_uint
+  (x: &mpz? >> mpz, y: uint): void = "mac#%"
+fun
+mpz_init_set_lint
+  (x: &mpz? >> mpz, y: lint): void = "mac#%"
+fun
+mpz_init_set_ulint
+  (x: &mpz? >> mpz, y: ulint): void = "mac#%"
+//
+symintr mpz_init_set // x := y
+//
+overload mpz_init_set with mpz_init_set_mpz
+overload mpz_init_set with mpz_init_set_int
+overload mpz_init_set with mpz_init_set_uint
+overload mpz_init_set with mpz_init_set_lint
+overload mpz_init_set with mpz_init_set_ulint
+//
+(* ****** ****** *)
+
+fun mpz_size (x: &RD(mpz)): size_t = "mac#%"
+
+(* ****** ****** *)
+//
+fun
+mpz_out_str
+  (out: FILEref, base: mp_base, x: &RD(mpz)): size_t = "mac#%"
+// end of [mpz_out_str]
+fun
+mpz_inp_str
+  (x: &mpz >> _, inp: FILEref, base: mp_base): size_t = "mac#%"
+// end of [mpz_inp_str]
+//
+(* ****** ****** *)
+//
+fun
+fprint_mpz
+  (out: FILEref, x: &RD(mpz)): void = "mac#%"
+fun
+fprint_mpz_base
+  (out: FILEref, x: &RD(mpz), base: mp_base): void = "mac#%"
+//
+overload fprint with fprint_mpz
+overload fprint with fprint_mpz_base
+//
+(* ****** ****** *)
+
+fun mpz_out_raw (out: FILEref, x: &RD(mpz)): size_t = "mac#%"
+fun mpz_inp_raw (x: &mpz >> _, out: FILEref): size_t = "mac#%"
+
+(* ****** ****** *)
+
+fun mpz_odd_p (x: &RD(mpz)):<> bool = "mac#%"
+fun mpz_even_p (x: &RD(mpz)):<> bool = "mac#%"
+
+(* ****** ****** *)
+//
+// HX: negation
+//
+symintr mpz_neg
+//
+// x := -x // -y
+//
+fun mpz_neg1
+  (x: &mpz >> _): void = "mac#%"
+fun mpz_neg2
+  (x: &mpz >> _, y: &mpz): void = "mac#%"
+overload mpz_neg with mpz_neg1
+overload mpz_neg with mpz_neg2
+//
+(* ****** ****** *)
+//
+// absolute value
+//
+symintr mpz_abs
+//
+// x := |x| // |y|
+//
+fun mpz_abs1
+  (x: &mpz >> _): void = "mac#%"
+fun mpz_abs2
+  (x: &mpz >> _, y: &mpz): void = "mac#%"
+overload mpz_abs with mpz_abs1
+overload mpz_abs with mpz_abs2
+//
+(* ****** ****** *)
+//
+// addition
+//
+symintr mpz_add
+//
+fun mpz_add2_mpz
+  (x: &mpz >> _, y: &mpz): void = "mac#%"
+fun mpz_add2_int
+  (x: &mpz >> _, y: int): void = "mac#%"
+fun mpz_add2_lint
+  (x: &mpz >> _, y: lint): void = "mac#%"
+fun mpz_add2_uint
+  (x: &mpz >> _, y: uint): void = "mac#%"
+fun mpz_add2_ulint
+  (x: &mpz >> _, y: ulint): void = "mac#%"
+fun mpz_add3_mpz
+  (x: &mpz >> _, y: &mpz, z: &mpz): void = "mac#%"
+fun mpz_add3_int
+  (x: &mpz >> _, y: &mpz, z: int): void = "mac#%"
+fun mpz_add3_lint
+  (x: &mpz >> _, y: &mpz, z: lint): void = "mac#%"
+fun mpz_add3_uint
+  (x: &mpz >> _, y: &mpz, z: uint): void = "mac#%"
+fun mpz_add3_ulint
+  (x: &mpz >> _, y: &mpz, z: ulint): void = "mac#%"
+//
+overload mpz_add with mpz_add2_mpz
+overload mpz_add with mpz_add2_int
+overload mpz_add with mpz_add2_lint
+overload mpz_add with mpz_add2_uint
+overload mpz_add with mpz_add2_ulint
+overload mpz_add with mpz_add3_mpz
+overload mpz_add with mpz_add3_int
+overload mpz_add with mpz_add3_lint
+overload mpz_add with mpz_add3_uint
+overload mpz_add with mpz_add3_ulint
+//
+(* ****** ****** *)
+//
+// subtraction
+//
+fun mpz_sub2_mpz
+  (x: &mpz >> _, y: &mpz): void = "mac#%"
+fun mpz_sub2_int
+  (x: &mpz >> _, y: int): void = "mac#%"
+fun mpz_sub2_lint
+  (x: &mpz >> _, y: lint): void = "mac#%"
+fun mpz_sub2_uint
+  (x: &mpz >> _, y: uint): void = "mac#%"
+fun mpz_sub2_ulint
+  (x: &mpz >> _, y: ulint): void = "mac#%"
+fun mpz_sub3_mpz
+  (x: &mpz >> _, y: &mpz, z: &mpz): void = "mac#%"
+fun mpz_sub3_int
+  (x: &mpz >> _, y: &mpz, z: int): void = "mac#%"
+fun mpz_sub3_lint
+  (x: &mpz >> _, y: &mpz, z: lint): void = "mac#%"
+fun mpz_sub3_uint
+  (x: &mpz >> _, y: &mpz, z: uint): void = "mac#%"
+fun mpz_sub3_ulint
+  (x: &mpz >> _, y: &mpz, z: ulint): void = "mac#%"
+//
+symintr mpz_sub
+//
+overload mpz_sub with mpz_sub2_mpz
+overload mpz_sub with mpz_sub2_int
+overload mpz_sub with mpz_sub2_lint
+overload mpz_sub with mpz_sub2_uint
+overload mpz_sub with mpz_sub2_ulint
+overload mpz_sub with mpz_sub3_mpz
+overload mpz_sub with mpz_sub3_int
+overload mpz_sub with mpz_sub3_lint
+overload mpz_sub with mpz_sub3_uint
+overload mpz_sub with mpz_sub3_ulint
+//
+(* ****** ****** *)
+//
+// multiplication
+//
+fun mpz_mul2_mpz
+  (x: &mpz >> _, y: &mpz): void = "mac#%"
+fun mpz_mul2_int
+  (x: &mpz >> _, y: int): void = "mac#%"
+fun mpz_mul2_lint
+  (x: &mpz >> _, y: lint): void = "mac#%"
+fun mpz_mul2_uint
+  (x: &mpz >> _, y: uint): void = "mac#%"
+fun mpz_mul2_ulint
+  (x: &mpz >> _, y: ulint): void = "mac#%"
+fun mpz_mul3_mpz
+  (x: &mpz >> _, y: &mpz, z: &mpz): void = "mac#%"
+fun mpz_mul3_int
+  (x: &mpz >> _, y: &mpz, z: int): void = "mac#%"
+fun mpz_mul3_lint
+  (x: &mpz >> _, y: &mpz, z: lint): void = "mac#%"
+fun mpz_mul3_uint
+  (x: &mpz >> _, y: &mpz, z: uint): void = "mac#%"
+fun mpz_mul3_ulint
+  (x: &mpz >> _, y: &mpz, z: ulint): void = "mac#%"
+//
+symintr mpz_mul
+//
+overload mpz_mul with mpz_mul2_mpz
+overload mpz_mul with mpz_mul2_int
+overload mpz_mul with mpz_mul2_lint
+overload mpz_mul with mpz_mul2_uint
+overload mpz_mul with mpz_mul2_ulint
+overload mpz_mul with mpz_mul3_mpz
+overload mpz_mul with mpz_mul3_int
+overload mpz_mul with mpz_mul3_lint
+overload mpz_mul with mpz_mul3_uint
+overload mpz_mul with mpz_mul3_ulint
+//
+(* ****** ****** *)
+
+(*
+**
+** Author: Zhiqiang Ren
+** Authoremail: arenATcsDOTbuDOTedu
+**
+** Description:
+** Set res to arg * (2 ^ exp)
+** The same object can be passed for both res and arg1.
+** It's up to an application to call functions like mpz_mul_2exp when appropriate.
+** General purpose functions like mpz_mul make no attempt to identify powers of two
+** or other special forms.
+**
+*)
+//
+fun
+mpz_mul3_2exp
+(
+  res: &mpz >> _, arg: &mpz, exp: ulint
+) : void = "mac#%" // end-of-function
+//
+symintr mpz_mul_2exp
+//
+overload mpz_mul_2exp with mpz_mul3_2exp 
+//
+(* ****** ****** *)
+//
+// trunc-division-functions
+// x := trunc(x/y) // trunc(y/z)
+//
+fun
+mpz_tdiv2_q_mpz
+  (x: &mpz >> _, y: &mpz): void = "mac#%"
+fun
+mpz_tdiv2_q_uint
+  (x: &mpz >> _, y: uint): void = "mac#%"
+fun
+mpz_tdiv2_q_ulint
+  (x: &mpz >> _, y: ulint): void = "mac#%"
+//
+fun
+mpz_tdiv3_q_mpz
+  (x: &mpz >> _, y: &mpz, z: &mpz): void = "mac#%"
+fun
+mpz_tdiv3_q_uint
+  (x: &mpz >> _, y: &mpz, z: uint): void = "mac#%"
+fun
+mpz_tdiv3_q_ulint
+  (x: &mpz >> _, y: &mpz, z: ulint): void = "mac#%"
+//
+symintr mpz_tdiv_q
+//
+overload mpz_tdiv_q with mpz_tdiv2_q_mpz
+overload mpz_tdiv_q with mpz_tdiv2_q_uint
+overload mpz_tdiv_q with mpz_tdiv2_q_ulint
+overload mpz_tdiv_q with mpz_tdiv3_q_mpz
+overload mpz_tdiv_q with mpz_tdiv3_q_uint
+overload mpz_tdiv_q with mpz_tdiv3_q_ulint
+//
+// x := x-trunc(x/y)*y // y-trunc(y/z)*z
+//
+fun
+mpz_tdiv2_r_mpz
+  (x: &mpz >> _, y: &mpz): void = "mac#%"
+fun
+mpz_tdiv2_r_uint
+  (x: &mpz >> _, y: uint): void = "mac#%"
+fun
+mpz_tdiv2_r_ulint
+  (x: &mpz >> _, y: ulint): void = "mac#%"
+fun
+mpz_tdiv3_r_mpz
+  (x: &mpz >> _, y: &mpz, z: &mpz): void = "mac#%"
+fun
+mpz_tdiv3_r_uint
+  (x: &mpz >> _, y: &mpz, z: uint): void = "mac#%"
+fun
+mpz_tdiv3_r_ulint
+  (x: &mpz >> _, y: &mpz, z: ulint): void = "mac#%"
+//
+symintr mpz_tdiv_r
+//
+overload mpz_tdiv_r with mpz_tdiv2_r_mpz
+overload mpz_tdiv_r with mpz_tdiv2_r_uint
+overload mpz_tdiv_r with mpz_tdiv2_r_ulint
+overload mpz_tdiv_r with mpz_tdiv3_r_mpz
+overload mpz_tdiv_r with mpz_tdiv3_r_uint
+overload mpz_tdiv_r with mpz_tdiv3_r_ulint
+//
+(* ****** ****** *)
+//
+fun mpz_tdiv3_qr_mpz
+  (xq: &mpz >> _, xr: &mpz >> _, y: &mpz): void = "mac#%"
+fun mpz_tdiv3_qr_uint
+  (xq: &mpz >> _, xr: &mpz >> _, y: uint): void = "mac#%"
+fun mpz_tdiv3_qr_ulint
+  (xq: &mpz >> _, xr: &mpz >> _, y: ulint): void = "mac#%"
+fun mpz_tdiv4_qr_mpz
+  (xq: &mpz >> _, xr: &mpz >> _, y: &mpz, z: &mpz): void = "mac#%"
+fun mpz_tdiv4_qr_uint
+  (xq: &mpz >> _, xr: &mpz >> _, y: &mpz, z: uint): void = "mac#%"
+fun mpz_tdiv4_qr_ulint
+  (xq: &mpz >> _, xr: &mpz >> _, y: &mpz, z: ulint): void = "mac#%"
+//
+symintr mpz_tdiv_qr
+//
+overload mpz_tdiv_qr with mpz_tdiv3_qr_mpz
+overload mpz_tdiv_qr with mpz_tdiv3_qr_uint
+overload mpz_tdiv_qr with mpz_tdiv3_qr_ulint
+overload mpz_tdiv_qr with mpz_tdiv4_qr_mpz
+overload mpz_tdiv_qr with mpz_tdiv4_qr_uint
+overload mpz_tdiv_qr with mpz_tdiv4_qr_ulint
+//
+(* ****** ****** *)
+//
+// floor-division-functions
+//
+fun
+mpz_fdiv_uint
+  (x: &mpz, d: uint): uint = "mac#%"
+fun
+mpz_fdiv_ulint
+  (x: &mpz, d: ulint): ulint = "mac#%"
+//
+symintr mpz_fdiv
+//
+overload mpz_fdiv with mpz_fdiv_uint
+overload mpz_fdiv with mpz_fdiv_ulint
+//
+// x := floor(x/y) // floor(y/z)
+//
+fun
+mpz_fdiv2_q_uint
+  (x: &mpz >> _, y: uint): void = "mac#%"
+fun
+mpz_fdiv2_q_ulint
+  (x: &mpz >> _, y: ulint): void = "mac#%"
+fun
+mpz_fdiv3_q_uint
+  (x: &mpz >> _, y: &mpz, z: uint): void = "mac#%"
+fun
+mpz_fdiv3_q_ulint // x := floor(y / z)
+  (x: &mpz >> _, y: &mpz, z: ulint): void = "mac#%"
+//
+symintr mpz_fdiv_q
+//
+overload mpz_fdiv_q with mpz_fdiv2_q_uint
+overload mpz_fdiv_q with mpz_fdiv2_q_ulint
+overload mpz_fdiv_q with mpz_fdiv3_q_uint
+overload mpz_fdiv_q with mpz_fdiv3_q_ulint
+//
+(* ****** ****** *)
+(*
+**
+**
+** Author: Zhiqiang Ren
+** Authoremail: arenATcsDOTbuDOTedu
+**
+** Description:
+** Set quot and rem so that dividend = quot * divisor + rem
+** Rounds quot down towards negative infinity, and rem will
+** have the same sign as divisor, and 0 <= |rem| < |divisor|.
+** The same object cannot be passed for both quot and rem, or the result will be
+** unpredictable. No other constraints on the passing arguments.
+*)
+//
+fun
+mpz_fdiv4_qr_mpz
+(
+  quot: &mpz >> _, rem: &mpz >> _, dividend: &mpz, divisor: &mpz
+) :<> void = "mac#%"
+fun
+mpz_fdiv4_qr_ulint
+(
+  quot: &mpz >> _, rem: &mpz >> _, dividend: &mpz, divisor: ulint
+) :<> ulint = "mac#%"
+//
+symintr mpz_fdiv_qr
+//
+overload mpz_fdiv_qr with mpz_fdiv4_qr_mpz
+overload mpz_fdiv_qr with mpz_fdiv4_qr_ulint
+//
+(* ****** ****** *)
+//
+// ceiling-division-functions
+//
+fun
+mpz_cdiv_uint
+  (x: &mpz, d: uint): uint = "mac#%"
+fun
+mpz_cdiv_ulint
+  (x: &mpz, d: ulint): ulint = "mac#%"
+//
+symintr mpz_cdiv
+//
+overload mpz_cdiv with mpz_cdiv_uint
+overload mpz_cdiv with mpz_cdiv_ulint
+//
+// x := ceiling(x/y) // ceiling(y/z)
+//
+fun
+mpz_cdiv2_q_uint
+  (x: &mpz >> _, y: uint): void = "mac#%"
+fun
+mpz_cdiv2_q_ulint
+  (x: &mpz >> _, y: uint): void = "mac#%"
+fun
+mpz_cdiv3_q_uint
+  (x: &mpz >> _, y: &mpz, z: uint): void = "mac#%"
+fun
+mpz_cdiv3_q_ulint // x := ceiling(y / z)
+  (x: &mpz >> _, y: &mpz, z: ulint): void = "mac#%"
+//
+symintr mpz_cdiv_q
+//
+overload mpz_cdiv_q with mpz_cdiv2_q_uint
+overload mpz_cdiv_q with mpz_cdiv2_q_ulint
+overload mpz_cdiv_q with mpz_cdiv3_q_uint
+overload mpz_cdiv_q with mpz_cdiv3_q_ulint
+//
+(* ****** ****** *)
+//
+// modulo-functions
+//
+fun
+mpz_mod2_mpz
+  (r: &mpz >> _, d: &mpz): void = "mac#%"
+//
+fun
+mpz_mod2_uint
+  (r: &mpz >> _, d: uint): uint = "mac#%"
+//
+fun
+mpz_mod2_ulint
+  (r: &mpz >> _, d: ulint): ulint = "mac#%"
+//
+fun
+mpz_mod3_mpz
+  (r: &mpz >> _, n: &mpz, d: &mpz): void = "mac#%"
+fun
+mpz_mod3_uint
+  (r: &mpz >> _, n: &mpz, d: uint): uint = "mac#%"
+fun
+mpz_mod3_ulint
+  (r: &mpz >> _, n: &mpz, d: ulint): ulint = "mac#%"
+//
+symintr mpz_mod
+//
+overload mpz_mod with mpz_mod2_mpz
+overload mpz_mod with mpz_mod2_uint
+overload mpz_mod with mpz_mod2_ulint
+overload mpz_mod with mpz_mod3_mpz
+overload mpz_mod with mpz_mod3_uint
+overload mpz_mod with mpz_mod3_ulint
+//
+(* ****** ****** *)
+//
+// add/mul combination
+// addmul (x, y, z): x := x + y * z
+//
+fun
+mpz_addmul3_mpz
+  (x: &mpz >> _, y: &mpz, z: &mpz): void = "mac#%"
+fun
+mpz_addmul3_uint
+  (x: &mpz >> _, y: &mpz, z: uint): void = "mac#%"
+fun
+mpz_addmul3_ulint
+  (x: &mpz >> _, y: &mpz, z: ulint): void = "mac#%"
+//
+symintr mpz_addmul
+//
+overload mpz_addmul with mpz_addmul3_mpz
+overload mpz_addmul with mpz_addmul3_uint
+overload mpz_addmul with mpz_addmul3_ulint
+//
+// sub/mul combination
+// submul (x, y, z): x := x - y * z
+//
+fun
+mpz_submul3_mpz
+  (x: &mpz >> _, y: &mpz, z: &mpz): void = "mac#%"
+fun
+mpz_submul3_uint
+  (x: &mpz >> _, y: &mpz, z: uint): void = "mac#%"
+fun
+mpz_submul3_ulint
+  (x: &mpz >> _, y: &mpz, z: ulint): void = "mac#%"
+//
+symintr mpz_submul
+//
+overload mpz_submul with mpz_submul3_mpz
+overload mpz_submul with mpz_submul3_uint
+overload mpz_submul with mpz_submul3_ulint
+//
+(* ****** ****** *)
+//
+// comparison-functions
+//
+fun mpz_cmp_mpz (x: &mpz, y: &mpz):<> int = "mac#%"
+fun mpz_cmp_int (x: &mpz, y: int):<> int = "mac#%"
+fun mpz_cmp_uint (x: &mpz, y: uint):<> int = "mac#%"
+fun mpz_cmp_lint (x: &mpz, y: lint):<> int = "mac#%"
+fun mpz_cmp_ulint (x: &mpz, y: ulint):<> int = "mac#%"
+//
+symintr mpz_cmp
+//
+overload mpz_cmp with mpz_cmp_mpz
+overload mpz_cmp with mpz_cmp_int
+overload mpz_cmp with mpz_cmp_uint
+overload mpz_cmp with mpz_cmp_lint
+overload mpz_cmp with mpz_cmp_ulint
+//
+(* ****** ****** *)
+//
+fun
+mpz_fac_uint
+  (x: &mpz >> _, n: uint): void = "mac#%"
+//
+(* ****** ****** *)
+//
+fun
+mpz_pow_uint
+  (pwr: &mpz >> _, base: &mpz, exp: uint): void = "mac#%"
+fun
+mpz_pow_ulint
+  (pwr: &mpz >> _, base: &mpz, exp: ulint): void = "mac#%"
+//
+fun mpz_ui_pow_ui
+  (pwr: &mpz >> _, base: ulint, exp: ulint): void = "mac#%"
+//
+symintr mpz_pow
+//
+overload mpz_pow with mpz_cmp_uint
+overload mpz_pow with mpz_cmp_ulint
+//
+(* ****** ****** *)
+//
+fun
+mpz_fib_uint
+  (x: &mpz >> _, n: uint): void = "mac#%"
+fun
+mpz_fib2_uint
+  (x1: &mpz >> _, x2: &mpz >> _, n: uint): void = "mac#%"
+//
+symintr mpz_fib
+symintr mpz_fib2
+//
+overload mpz_fib with mpz_fib_uint
+overload mpz_fib2 with mpz_fib2_uint
+//
+(* ****** ****** *)
+
+(* end of [gmp.sats] *)