language-ats 1.6.0.0 → 1.7.0.0

raw patch · 20 files changed

+2168/−100 lines, 20 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGELOG.md +14/−1
• language-ats.cabal +3/−1
• src/Language/ATS/Parser.y +39/−25
• src/Language/ATS/PrettyPrint.hs +23/−14
• src/Language/ATS/Rewrite.hs +16/−2
• src/Language/ATS/Types.hs +60/−33
• src/Language/ATS/Types/Lens.hs +13/−8
• test/data/concurrency.out +2/−2
• test/data/fastcount.out +3/−3
• test/data/levenshtein2.out +2/−2
• test/data/prf_sqrt2.dats +0/−3
• test/data/prf_sqrt2.out +1/−6
• test/data/recursion.dats +41/−0
• test/data/recursion.out +47/−0
• test/data/stdlib/DATS/bool.dats +74/−0
• test/data/stdlib/DATS/integer_fixed.dats +553/−0
• test/data/stdlib/DATS/integer_long.dats +576/−0
• test/data/stdlib/DATS/integer_ptr.dats +183/−0
• test/data/stdlib/DATS/integer_short.dats +183/−0
• test/data/stdlib/DATS/integer_size.dats +335/−0

@@ -1,5 +1,18 @@ # language-ats  +## 1.7.0.0++Bug Fixes:+  +  * Now accepts proof-level lambdas.+  * Include all test data++Breaking Changes:+  +  * `PrVar` and `PrVal` now take a `StaticExpression`+  * `PrFun`, `PrFn`, and `Praxi` now take a `StaticExpression`+  * Add a rewrite phase for `StaticExpression`s+ ## 1.6.0.0  Breaking Changes:@@ -12,7 +25,7 @@    * Better Error messages   * Add support for boxed records-  * Add support for proof expressions introducing witnesses (`[ m | [] ]`)+  * Add support for proof expressions introducing witnesses (`[ m | () ]`)  Bug Fixes: 

@@ -1,6 +1,6 @@ cabal-version: 1.18 name: language-ats-version: 1.6.0.0+version: 1.7.0.0 license: BSD3 license-file: LICENSE copyright: Copyright: (c) 2018 Vanessa McHale@@ -17,6 +17,8 @@     test/data/*.sats     test/data/*.out     test/data/stdlib/*.sats+    test/data/stdlib/*.out+    test/data/stdlib/DATS/*.dats     test/data/stdlib/*.out extra-doc-files: README.md                  CHANGELOG.md

@@ -182,6 +182,8 @@     cloptr1Arrow { Arrow $$ "=<cloptr1>" }     lincloptr1Arrow { Arrow $$ "=<lincloptr1>" }     lincloref1Arrow { Arrow $$ "=<lin,cloref1>" }+    proofLambda { Arrow $$ "=<prf>" }+    proofLinearLambda { Arrow $$ "=<lin,prf>" }     spear { Arrow $$ "=>>" }     proofArrow { Arrow $$ "=/=>" }     proofSpear { Arrow $$ "=/=>>" }@@ -399,6 +401,8 @@             | cloptr1Arrow { Full $1 "cloptr1" }             | lincloptr1Arrow { Full $1 "lincloptr1" }             | lincloref1Arrow { Full $1 "lin,cloref1" }+            | proofLambda { Full $1 "prf" }+            | proofLinearLambda { Full $1 "lin,prf" }             | minus {% left $ Expected $1 "Arrow" "-" }             | openParen {% left $ Expected $1 "Arrow" "(" }             | closeParen {% left $ Expected $1 "Arrow" ")" }@@ -447,23 +451,28 @@                  | intLit { StaticInt $1 }                  | hexLit { StaticHex $1 }                  | string { SString $1 }-                 | doubleParens { StaticVoid $1 }+                 | doubleParens { StaticVoid $1 } -- TODO: static tuple?                  | sif StaticExpression then StaticExpression else StaticExpression { Sif $2 $4 $6 }                  | identifierSpace { StaticVal (Unqualified $ to_string $1) }                  | identifierSpace StaticExpression { SCall (Unqualified $ to_string $1) [] [$2] }                  | Name parens(StaticArgs) { SCall $1 [] $2 }-                 | identifierSpace parens(StaticArgs) { SCall (Unqualified $ to_string $1) [] $2 } -- TODO: static tuple?+                 | Name TypeArgs parens(StaticArgs) { SCall $1 $2 $3 }+                 | Name TypeArgs doubleParens { SCall $1 $2 [] }+                 | Name doubleParens { SCall $1 [] [] }+                 | identifierSpace TypeArgs parens(StaticArgs) { SCall (Unqualified $ to_string $1) $2 $3 }+                 | identifierSpace parens(StaticArgs) { SCall (Unqualified $ to_string $1) [] $2 }+                 | identifierSpace doubleParens { SCall (Unqualified $ to_string $1) [] [] } -- TODO: this causes an ambiguity because we might have SCall void instead!                  | StaticExpression semicolon StaticExpression { SPrecede $1 $3 }                  | UnOp StaticExpression { SUnary $1 $2 }-                 | identifierSpace doubleParens { SCall (Unqualified $ to_string $1) [] [] }-                 | identifier TypeArgs doubleParens { SCall (Unqualified $ to_string $1) $2 [] }-                 | identifier doubleParens { SCall (Unqualified $ to_string $1) [] [] }                  | let StaticDecls comment_after(in) end { SLet $1 (reverse $2) Nothing }                  | let StaticDecls in StaticExpression end { SLet $1 (reverse $2) (Just $4) }                  | parens(StaticExpression) { $1 }                  | openParen lineComment StaticExpression closeParen { $3 }                  | case StaticExpression of StaticCase { SCase $1 $2 $4 }                  | openExistential StaticExpression vbar StaticExpression rsqbracket { Witness $1 $2 $4 }+                 | lambda Pattern LambdaArrow StaticExpression { ProofLambda $1 $3 $2 $4 }+                 | llambda Pattern LambdaArrow StaticExpression { ProofLinearLambda $1 $3 $2 $4 }+                 | StaticExpression where braces(ATS) { WhereStaExp $1 $3 }  -- | Parse an expression that can be called without parentheses PreExpression : identifier lsqbracket PreExpression rsqbracket { Index $2 (Unqualified $ to_string $1) $3 }@@ -712,20 +721,25 @@         | { Nothing }  -- | Parse a type signature and optional function body-PreFunction : FunName openParen Args closeParen OptType OptExpression { PreF $1 (fmap fst $5) [] [] (Just $3) (fmap snd $5) Nothing $6 }-            | FunName Universals OptTermetric OptType OptExpression { PreF $1 (fmap fst $4) [] $2 Nothing (fmap snd $4) $3 $5 }-            | FunName Universals OptTermetric doubleParens OptType OptExpression { PreF $1 (fmap fst $5) [] $2 (Just []) (fmap snd $5) $3 $6 }-            | FunName Universals OptTermetric openParen Args closeParen OptType OptExpression { PreF $1 (fmap fst $7) [] $2 (Just $5) (fmap snd $7) $3 $8 }-            | Universals FunName Universals OptTermetric openParen Args closeParen OptType OptExpression { PreF $2 (fmap fst $8) $1 $3 (Just $6) (fmap snd $8) $4 $9 }-            | Universals FunName Universals OptTermetric doubleParens OptType OptExpression { PreF $2 (fmap fst $6) $1 $3 (Just []) (fmap snd $6) $4 $7 }-            | Universals FunName Universals OptTermetric OptType OptExpression { PreF $2 (fmap fst $5) $1 $3 Nothing (fmap snd $5) $4 $6 }-            | prval {% left $ Expected $1 "Function signature" "prval" }-            | var {% left $ Expected $1 "Function signature" "var" }-            | val {% left $ Expected (token_posn $1) "Function signature" "val" }-            | lambda {% left $ Expected $1 "Function signature" "lam" }-            | llambda {% left $ Expected $1 "Function signature" "llam" }-            | lsqbracket {% left $ Expected $1 "Function signature" "[" }+preFunction(p)+    : FunName openParen Args closeParen OptType p { PreF $1 (fmap fst $5) [] [] (Just $3) (fmap snd $5) Nothing $6 }+    | FunName Universals OptTermetric OptType p { PreF $1 (fmap fst $4) [] $2 Nothing (fmap snd $4) $3 $5 }+    | FunName Universals OptTermetric doubleParens OptType p { PreF $1 (fmap fst $5) [] $2 (Just []) (fmap snd $5) $3 $6 }+    | FunName Universals OptTermetric openParen Args closeParen OptType p { PreF $1 (fmap fst $7) [] $2 (Just $5) (fmap snd $7) $3 $8 }+    | Universals FunName Universals OptTermetric openParen Args closeParen OptType p { PreF $2 (fmap fst $8) $1 $3 (Just $6) (fmap snd $8) $4 $9 }+    | Universals FunName Universals OptTermetric doubleParens OptType p { PreF $2 (fmap fst $6) $1 $3 (Just []) (fmap snd $6) $4 $7 }+    | Universals FunName Universals OptTermetric OptType p { PreF $2 (fmap fst $5) $1 $3 Nothing (fmap snd $5) $4 $6 }+    | prval {% left $ Expected $1 "Function signature" "prval" }+    | var {% left $ Expected $1 "Function signature" "var" }+    | val {% left $ Expected (token_posn $1) "Function signature" "val" }+    | lambda {% left $ Expected $1 "Function signature" "lam" }+    | llambda {% left $ Expected $1 "Function signature" "llam" }+    | lsqbracket {% left $ Expected $1 "Function signature" "[" } +PreStaFunction : preFunction(OptStaticExpression) { $1 }++PreFunction : preFunction(OptExpression) { $1 }+ -- | Parse affiliated `sortdef`s AndSort : AndSort and IdentifierOr eq Sort { AndD $1 (SortDef $2 $3 (Left $5)) }         | sortdef IdentifierOr eq Sort { SortDef $1 $2 (Left $4) }@@ -744,8 +758,8 @@           | AndStadef and IdentifierOr SortArgs StaticDef { AndD $1 (Stadef $3 $4 $5) }           | AndStadef and Operator SortArgs StaticDef { AndD $1 (Stadef $3 $4 $5) } -StafunDecl : prfun PreFunction { Func $1 (PrFun $2) }-           | prfn PreFunction { Func $1 (PrFn $2) }+StafunDecl : prfun PreStaFunction { Func $1 (PrFun $2) }+           | prfn PreStaFunction { Func $1 (PrFn $2) }  -- | Function declaration FunDecl : fun PreFunction { [ Func $1 (Fun $2) ] }@@ -869,13 +883,13 @@         | extern ValDecl { over _head (Extern $1) $2 }         | val Pattern eq colon {% left $ Expected $4 "Expression" ":" } -StaticDeclaration : prval Pattern eq Expression { PrVal $2 (Just $4) Nothing }+StaticDeclaration : prval Pattern eq StaticExpression { PrVal $2 (Just $4) Nothing } -- FIXME: prval should use static expressions as well.                   | prval Pattern colon Type { PrVal $2 Nothing (Just $4) }-                  | prval Pattern colon Type eq Expression { PrVal $2 (Just $6) (Just $4) }-                  | prvar Pattern eq Expression { PrVar $2 (Just $4) Nothing }+                  | prval Pattern colon Type eq StaticExpression { PrVal $2 (Just $6) (Just $4) }+                  | prvar Pattern eq StaticExpression { PrVar $2 (Just $4) Nothing }                   | prvar Pattern colon Type { PrVar $2 Nothing (Just $4) }-                  | prvar Pattern colon Type eq Expression { PrVar $2 (Just $6) (Just $4) }-                  | praxi PreFunction { Func $1 (Praxi $2) }+                  | prvar Pattern colon Type eq StaticExpression { PrVar $2 (Just $6) (Just $4) }+                  | praxi PreStaFunction { Func $1 (Praxi $2) }                   | primplmnt FunArgs StaticImplementation { ProofImpl $2 $3 }                   | StafunDecl { $1 }                   | extern StaticDeclaration { Extern $1 $2 }

@@ -26,6 +26,10 @@  infixr 5 $$ +instance Eq Doc where+    (==) = (==) `on` (($ "") . displayS . renderCompact)++ -- | Pretty-print with sensible defaults. printATS :: Eq a => ATS a -> String printATS = (<> "\n") . printATSCustom 0.6 120@@ -119,6 +123,9 @@ prettyProofExpr (e:|[]) = e prettyProofExpr es      = mconcat (punctuate ", " (toList es)) +prettyLam :: (Pretty a, Pretty b) => Doc -> a -> b -> Doc -> Doc+prettyLam bind p lt e = let pre = bind <+> pretty p <+> pretty lt in flatAlt (lengthAlt pre e) (pre <+> e)+ instance Eq a => Pretty (Expression a) where     pretty = cata a where         a (IfF e e' (Just e''))         = "if" <+> e <+> "then" <$> indent 2 e' <$> "else" <$> indent 2 e''@@ -129,8 +136,8 @@         a (UintLitF u)                  = pretty u <> "u"         a (IntLitF i)                   = pretty i         a (HexLitF hi)                  = "0x" <> text hi-        a (LambdaF _ lt p e)            = let pre = "lam" <+> pretty p <+> pretty lt in flatAlt (lengthAlt pre e) (pre <+> e)-        a (LinearLambdaF _ lt p e)      = let pre = "llam" <+> pretty p <+> pretty lt in flatAlt (lengthAlt pre e) (pre <+> e)+        a (LambdaF _ lt p e)            = prettyLam "lam" p lt e+        a (LinearLambdaF _ lt p e)      = prettyLam "llam" p lt e         a (FloatLitF f)                 = pretty f         a (StringLitF s)                = text s -- FIXME escape indentation in multi-line strings.         a (ParenExprF _ e)              = parens e@@ -145,15 +152,9 @@         a (CallF nam [] [] Nothing [])  = pretty nam <> "()"         a (CallF nam [] [] e xs)        = pretty nam <> prettyArgsProof e xs         a (CallF nam [] us Nothing [])  = pretty nam <> prettyTypes us-        a (CallF nam [] us Nothing [x])-            | startsParens x = pretty nam <> prettyTypes us <> pretty x         a (CallF nam [] us e xs)        = pretty nam <> prettyTypes us <> prettyArgsProof e xs         a (CallF nam is [] Nothing [])  = pretty nam <> prettyImplicits is-        a (CallF nam is [] Nothing [x])-            | startsParens x = pretty nam <> prettyImplicits is <> pretty x         a (CallF nam is [] e xs)        = pretty nam <> prettyImplicits is <> prettyArgsProof e xs-        a (CallF nam is us Nothing [x])-            | startsParens x = pretty nam <> prettyImplicits is <> prettyTypes us <> pretty x         a (CallF nam is us e xs)        = pretty nam <> prettyImplicits is <> prettyTypes us <> prettyArgsProof e xs         a (CaseF _ add' e cs)           = "case" <> pretty add' <+> e <+> "of" <$> indent 2 (prettyCases cs)         a (IfCaseF _ cs)                = "ifcase" <$> indent 2 (prettyIfCase cs)@@ -172,7 +173,7 @@         a (CharLitF c)                 = "'" <> char c <> "'"         a (ProofExprF _ es e')         = "(" <> prettyProofExpr es <+> "|" <+> e' <> ")"         a (TypeSignatureF e t)         = e <+> ":" <+> pretty t-        a (WhereExpF e d)              = e <+> "where" <$> braces (" " <> nest 2 (pretty d) <> " ")+        a (WhereExpF e d)              = prettyWhere e d         a (TupleExF _ es)              = parens (mconcat $ punctuate ", " (toList $ NE.reverse es))         a (BoxTupleExF _ es)           = "'(" <> mconcat (punctuate ", " (toList $ NE.reverse es)) <> ")"         a (WhileF _ e e')              = "while" <> parens e <> e'@@ -260,6 +261,9 @@ prettyImplicits :: Pretty a => [[a]] -> Doc prettyImplicits = prettyExtras "<" ">" +prettyWhere :: Pretty a => Doc -> a -> Doc+prettyWhere e d = e <+> "where" <$> braces (" " <> nest 2 (pretty d) <> " ")+ instance Eq a => Pretty (StaticExpression a) where     pretty = cata a where         a (StaticValF n)            = pretty n@@ -270,6 +274,8 @@         a (StaticHexF h)            = text h         a StaticVoidF{}             = "()"         a (SifF e e' e'')           = "sif" <+> e <+> "then" <$> indent 2 e' <$> "else" <$> indent 2 e''+        a (SCallF n [] ["()"])      = pretty n <> "()"+        a (SCallF n us ["()"])      = pretty n <> prettyTypes us <> "()"         a (SCallF n [] cs)          = pretty n <> parens (mconcat (punctuate "," . fmap pretty $ cs))         a (SCallF n us cs)          = pretty n <> prettyTypes us <> parens (mconcat (punctuate "," . fmap pretty $ cs))         a (SPrecedeF e e')          = e <> ";" <+> e'@@ -280,6 +286,9 @@         a (SCaseF ad e sls) = "case" <> pretty ad <+> e <+> "of" <$> indent 2 (prettyCases sls)         a (SStringF s)      = text s         a (WitnessF _ e e') = "#[" <+> e <+> "|" <+> e' <+> "]"+        a (ProofLambdaF _ lt p e)       = prettyLam "lam" p lt e+        a (ProofLinearLambdaF _ lt p e) = prettyLam "llam" p lt e+        a (WhereStaExpF e ds) = prettyWhere e ds  instance Eq a => Pretty (Sort a) where     pretty = cata a where@@ -363,10 +372,10 @@     pretty (Implement _ [] is [] n (Just ias) e) = pretty n <> prettyOr is <+> prettyArgs ias <+> "=" <$> indent 2 (prettyImplExpr e)     pretty (Implement _ [] is us n (Just ias) e) = pretty n <> prettyOr is <+> foldMap pretty us </> prettyArgs ias <+> "=" <$> indent 2 (prettyImplExpr e)     pretty (Implement _ [] is us n Nothing e) = pretty n <> prettyOr is <+> foldMap pretty us </> "=" <$> indent 2 (prettyImplExpr e)-    pretty (Implement _ ps is [] n (Just ias) e) = foldMap pretty (reverse ps) </> pretty n <> prettyOr is <+> prettyArgs ias <+> "=" <$> indent 2 (prettyImplExpr e)-    pretty (Implement _ ps is [] n Nothing e)    = foldMap pretty (reverse ps) </> pretty n <> prettyOr is <+> "=" <$> indent 2 (prettyImplExpr e)-    pretty (Implement _ ps is us n (Just ias) e) = foldMap pretty (reverse ps) </> pretty n <> prettyOr is </> foldMap pretty us <+> prettyArgs ias <+> "=" <$> indent 2 (prettyImplExpr e)-    pretty (Implement _ ps is us n Nothing e) = foldMap pretty (reverse ps) </> pretty n <> prettyOr is </> foldMap pretty us <+> "=" <$> indent 2 (prettyImplExpr e)+    pretty (Implement _ ps is [] n (Just ias) e) = foldMap pretty ps </> pretty n <> prettyOr is <+> prettyArgs ias <+> "=" <$> indent 2 (prettyImplExpr e)+    pretty (Implement _ ps is [] n Nothing e)    = foldMap pretty ps </> pretty n <> prettyOr is <+> "=" <$> indent 2 (prettyImplExpr e)+    pretty (Implement _ ps is us n (Just ias) e) = foldMap pretty ps </> pretty n <> prettyOr is </> foldMap pretty us <+> prettyArgs ias <+> "=" <$> indent 2 (prettyImplExpr e)+    pretty (Implement _ ps is us n Nothing e) = foldMap pretty ps </> pretty n <> prettyOr is </> foldMap pretty us <+> "=" <$> indent 2 (prettyImplExpr e)  isVal :: Declaration a -> Bool isVal Val{}     = True@@ -532,7 +541,7 @@ prettyMTermetric = maybe mempty prettyTermetric  -- FIXME figure out a nicer algorithm for when/how to split lines.-instance Eq a => Pretty (PreFunction a) where+instance (Eq a, Pretty (ek a)) => Pretty (PreFunction ek a) where     pretty (PreF i si [] [] as rt Nothing (Just e)) = pretty i <> prettyArgsNil as <> prettySig si rt <> "=" <$> indent 2 (pretty e)     pretty (PreF i si [] us as rt t (Just e)) = pretty i </> fancyU us <> prettyMTermetric t <> prettyArgsNil as <> prettySig si rt <> "=" <$> indent 2 (pretty e)     pretty (PreF i si pus [] as rt Nothing (Just e)) = fancyU pus </> pretty i <> prettyArgsNil as <> prettySig si rt <> "=" <$> indent 2 (pretty e)

@@ -1,3 +1,5 @@+{-# LANGUAGE FlexibleContexts #-}+ module Language.ATS.Rewrite ( rewriteDecl                             -- * Fixity                             , defaultFixityState@@ -13,8 +15,11 @@ import           Lens.Micro  exprLens :: Eq a => FixityState a -> ASetter s t (Expression a) (Expression a) -> s -> t-exprLens st = flip over (rewriteATS st)+exprLens = flip over . rewriteATS +exprStaLens :: Eq a => FixityState a -> ASetter s t (StaticExpression a) (StaticExpression a) -> s -> t+exprStaLens = flip over . rewriteStaATS+ exprLenses :: Eq a => FixityState a -> [ASetter b b (Expression a) (Expression a)] -> b -> b exprLenses st = thread . fmap (exprLens st) @@ -22,9 +27,10 @@ rewriteDecl st (Extern l d) = Extern l (rewriteDecl st d) rewriteDecl st x@Val{} = exprLens st valExpression x rewriteDecl st x@Var{} = exprLenses st [varExpr1._Just, varExpr2._Just] x+rewriteDecl st x@PrVal{} = exprStaLens st (prValExpr._Just) x+rewriteDecl st x@PrVar{} = exprStaLens st (prValExpr._Just) x rewriteDecl st x@Func{} = exprLens st (fun.preF.expression._Just) x rewriteDecl st x@Impl{} = exprLens st (impl.iExpression._Right) x-rewriteDecl st x@PrVal{} = exprLens st (prValExpr._Just) x rewriteDecl st x@AndDecl{} = exprLens st andExpr x rewriteDecl st x@DataProp{} = exprLenses st (fmap ((propLeaves.each).) [propExpr1, propExpr2._Just]) x rewriteDecl _ x@SumViewType{} = g x@@ -78,6 +84,14 @@ -- FIXME this should account for right vs. left associativity. compareFixity :: Eq a => FixityState a -> BinOp a -> BinOp a -> Bool compareFixity st = (== GT) .* on compare (getFixity st)++rewriteStaATS :: Eq a => FixityState a -> StaticExpression a -> StaticExpression a+rewriteStaATS st = cata a where+    a (SCallF n ts [StaticVoid{}]) = SCall n ts []+    a (StaticBinaryF op (StaticBinary op' e e') e'')+        | compareFixity st op op'  = StaticBinary op e (StaticBinary op' e' e'')+    a (WhereStaExpF se (ATS ds))   = WhereStaExp se (ATS (rewriteDecl st <$> ds))+    a x                            = embed x  -- | Among other things, this rewrites expressions so that operator precedence -- is respected; this ensures @1 + 2 * 3@ will be parsed as the correct

@@ -84,8 +84,8 @@                    | ProofImpl { implArgs :: Args a, _impl :: Implementation a }                    | Val { add :: Addendum, valT :: Maybe (Type a), valPat :: Pattern a, _valExpression :: Expression a }                    | StaVal [Universal a] String (Type a)-                   | PrVal { prvalPat :: Pattern a, _prValExpr :: Maybe (Expression a), prValType :: Maybe (Type a) }-                   | PrVar { prvarPat :: Pattern a, _prVarExpr :: Maybe (Expression a), prVarType :: Maybe (Type a) }+                   | PrVal { prvalPat :: Pattern a, _prValExpr :: Maybe (StaticExpression a), prValType :: Maybe (Type a) }+                   | PrVar { prvarPat :: Pattern a, _prVarExpr :: Maybe (StaticExpression a), prVarType :: Maybe (Type a) }                    | Var { varT :: Maybe (Type a), varPat :: Pattern a, _varExpr1 :: Maybe (Expression a), _varExpr2 :: Maybe (Expression a) }                    | AndDecl { andT :: Maybe (Type a), andPat :: Pattern a, _andExpr :: Expression a }                    | Include String@@ -368,6 +368,9 @@                         | SCase Addendum (StaticExpression a) [(Pattern a, LambdaType a, StaticExpression a)]                         | SString String -- ^ @ext#@                         | Witness a (StaticExpression a) (StaticExpression a) -- ^ @#[ m | () ]@+                        | ProofLambda a (LambdaType a) (Pattern a) (StaticExpression a) -- TODO: are linear proof-level lambdas allowed?+                        | ProofLinearLambda a (LambdaType a) (Pattern a) (StaticExpression a) -- TODO: are linear proof-level lambdas allowed?+                        | WhereStaExp (StaticExpression a) (ATS a)                         deriving (Show, Eq, Generic, NFData)  data StaticExpressionF a x = StaticValF (Name a)@@ -383,25 +386,49 @@                            | SCaseF Addendum x [(Pattern a, LambdaType a, x)]                            | SStringF String                            | WitnessF a x x+                           | ProofLambdaF a (LambdaType a) (Pattern a) x+                           | ProofLinearLambdaF a (LambdaType a) (Pattern a) x+                           | WhereStaExpF x (ATS a)                            deriving (Functor)  type instance Base (StaticExpression a) = StaticExpressionF a  instance Recursive (StaticExpression a) where-    project (StaticVal n)         = StaticValF n-    project (StaticBinary b x x') = StaticBinaryF b x x'-    project (StaticHex h)         = StaticHexF h-    project (StaticInt i)         = StaticIntF i-    project (SPrecede x x')       = SPrecedeF x x'-    project (StaticVoid x)        = StaticVoidF x-    project (Sif e e' e'')        = SifF e e' e''-    project (SCall n ts es)       = SCallF n ts es-    project (SUnary u x)          = SUnaryF u x-    project (SLet x ds e)         = SLetF x ds e-    project (SCase a x ples)      = SCaseF a x ples-    project (SString s)           = SStringF s-    project (Witness a e e')      = WitnessF a e e'+    project (StaticVal n)               = StaticValF n+    project (StaticBinary b x x')       = StaticBinaryF b x x'+    project (StaticHex h)               = StaticHexF h+    project (StaticInt i)               = StaticIntF i+    project (SPrecede x x')             = SPrecedeF x x'+    project (StaticVoid x)              = StaticVoidF x+    project (Sif e e' e'')              = SifF e e' e''+    project (SCall n ts es)             = SCallF n ts es+    project (SUnary u x)                = SUnaryF u x+    project (SLet x ds e)               = SLetF x ds e+    project (SCase a x ples)            = SCaseF a x ples+    project (SString s)                 = SStringF s+    project (Witness a e e')            = WitnessF a e e'+    project (ProofLambda a l p e)       = ProofLambdaF a l p e+    project (ProofLinearLambda a l p e) = ProofLinearLambdaF a l p e+    project (WhereStaExp e ds)          = WhereStaExpF e ds +instance Corecursive (StaticExpression a) where+    embed (StaticValF n)               = StaticVal n+    embed (StaticBinaryF b e e')       = StaticBinary b e e'+    embed (StaticHexF h)               = StaticHex h+    embed (StaticIntF i)               = StaticInt i+    embed (SPrecedeF e e')             = SPrecede e e'+    embed (StaticVoidF l)              = StaticVoid l+    embed (SifF e e' e'')              = Sif e e' e''+    embed (SCallF n ts es)             = SCall n ts es+    embed (SUnaryF u e)                = SUnary u e+    embed (SLetF l ds e)               = SLet l ds e+    embed (SCaseF a x ples)            = SCase a x ples+    embed (SStringF s)                 = SString s+    embed (WitnessF l e e')            = Witness l e e'+    embed (ProofLambdaF a l p e)       = ProofLambda a l p e+    embed (ProofLinearLambdaF a l p e) = ProofLinearLambda a l p e+    embed (WhereStaExpF e ds)          = WhereStaExp e ds+ -- | A (possibly effectful) expression. data Expression a = Let a (ATS a) (Maybe (Expression a))                   | VoidLiteral a -- ^ The '()' literal representing inaction.@@ -616,14 +643,14 @@  -- | A function declaration accounting for all keywords ATS uses to -- define them.-data Function a = Fun { _preF :: PreFunction a }-                | Fn { _preF :: PreFunction a }-                | Fnx { _preF :: PreFunction a }-                | And { _preF :: PreFunction a }-                | PrFun { _preF :: PreFunction a }-                | PrFn { _preF :: PreFunction a }-                | Praxi { _preF :: PreFunction a }-                | CastFn { _preF :: PreFunction a }+data Function a = Fun { _preF :: PreFunction Expression a }+                | Fn { _preF :: PreFunction Expression a }+                | Fnx { _preF :: PreFunction Expression a }+                | And { _preF :: PreFunction Expression a }+                | PrFun { _preStaF :: PreFunction StaticExpression a }+                | PrFn { _preStaF :: PreFunction StaticExpression a }+                | Praxi { _preStaF :: PreFunction StaticExpression a }+                | CastFn { _preF :: PreFunction Expression a }                 deriving (Show, Eq, Generic, NFData)  -- | A type for stack-allocated functions. See@@ -636,16 +663,16 @@                               }                               deriving (Show, Eq, Generic, NFData) -data PreFunction a = PreF { fname         :: Name a -- ^ Function name-                          , sig           :: Maybe String -- ^ e.g. <> or \<!wrt>-                          , preUniversals :: [Universal a] -- ^ Universal quantifiers making a function generic-                          , universals    :: [Universal a] -- ^ (Universal a) quantifiers/refinement type-                          , args          :: Args a -- ^ Actual function arguments-                          , returnType    :: Maybe (Type a) -- ^ Return type-                          , termetric     :: Maybe (StaticExpression a) -- ^ Optional termination metric-                          , _expression   :: Maybe (Expression a) -- ^ Expression holding the actual function body (not present in static templates)-                          }-                          deriving (Show, Eq, Generic, NFData)+data PreFunction ek a = PreF { fname         :: Name a -- ^ Function name+                             , sig           :: Maybe String -- ^ e.g. <> or \<!wrt>+                             , preUniversals :: [Universal a] -- ^ Universal quantifiers making a function generic+                             , universals    :: [Universal a] -- ^ (Universal a) quantifiers/refinement type+                             , args          :: Args a -- ^ Actual function arguments+                             , returnType    :: Maybe (Type a) -- ^ Return type+                             , termetric     :: Maybe (StaticExpression a) -- ^ Optional termination metric+                             , _expression   :: Maybe (ek a) -- ^ Expression holding the actual function body (not present in static templates)+                             }+                             deriving (Show, Eq, Generic, NFData)  -- FIXME left vs. right shouldn't be treated the same instance (Eq a) => Ord (Fixity a) where

@@ -11,13 +11,13 @@                                , fun                                , impl                                , valExpression-                               , prValExpr                                , varExpr1                                , varExpr2                                , andExpr                                , propLeaves                                , leaves                                , comment+                               , prValExpr                                ) where  import           Data.List.NonEmpty (NonEmpty)@@ -27,12 +27,9 @@ constructorUniversals :: Lens' (Leaf a) [Universal a] constructorUniversals f s = fmap (\x -> s { _constructorUniversals = x}) (f (_constructorUniversals s)) -expression :: Lens' (PreFunction a) (Maybe (Expression a))+expression :: Lens' (PreFunction ek a) (Maybe (ek a)) expression f s = fmap (\x -> s { _expression = x}) (f (_expression s)) -preF :: Lens' (Function a) (PreFunction a)-preF f s = fmap (\x -> s { _preF = x}) (f (_preF s))- iExpression :: Lens' (Implementation a) (Either (StaticExpression a) (Expression a)) iExpression f s = fmap (\x -> s { _iExpression = x}) (f (_iExpression s)) @@ -42,6 +39,13 @@ propExpr2 :: Lens' (DataPropLeaf a) (Maybe (Expression a)) propExpr2 f s = fmap (\x -> s { _propExpr2 = x}) (f (_propExpr2 s)) +preF :: Traversal' (Function a) (PreFunction Expression a)+preF f (Fun x)    = (\x' -> Fun x') <$> f x+preF f (Fn x)     = (\x' -> Fn x') <$> f x+preF f (CastFn x) = (\x' -> CastFn x') <$> f x+preF f (Fnx x)    = (\x' -> Fnx x') <$> f x+preF f (And x)    = (\x' -> And x') <$> f x+preF _ x          = pure x  typeCall :: Traversal' (Type a) (Name a) typeCall f (Dependent x y) = (\x' -> Dependent x' y) <$> f x@@ -64,9 +68,10 @@ valExpression f (Val a v p e) = Val a v p <$> f e valExpression _ x             = pure x -prValExpr :: Traversal' (Declaration a) (Maybe (Expression a))-prValExpr f (PrVal p me t) = (\me' -> PrVal p me' t) <$> f me-prValExpr _ x              = pure x+prValExpr :: Traversal' (Declaration a) (Maybe (StaticExpression a))+prValExpr f (PrVal p me mt) = (\e -> PrVal p e mt) <$> f me+prValExpr f (PrVar p me mt) = (\e -> PrVar p e mt) <$> f me+prValExpr _ x               = pure x  varExpr1 :: Traversal' (Declaration a) (Maybe (Expression a)) varExpr1 f (Var t p e e') = (\e'' -> Var t p e'' e') <$> f e

@@ -212,7 +212,7 @@     val+ CHANNEL{l0,l1,l2,l3}(ch) = chan     val mutex = unsafe_mutex_vt2t(ch.mutex)     val (prf | ()) = mutex_lock(mutex)-    val xs = $UN.castvwtp0{queue(a)}(prf | ch.queue)+    val xs = $UN.castvwtp0{queue(a)}((prf | ch.queue))     val () = channel_insert_helper<a>(chan, xs, x)     prval prf = $UN.castview0{locked_v(l1)}(xs)     val () = mutex_unlock(prf | mutex)@@ -223,7 +223,7 @@   { val+ CHANNEL{l0,l1,l2,l3}(ch) = chan     val mutex = unsafe_mutex_vt2t(ch.mutex)     val (prf | ()) = mutex_lock(mutex)-    val xs = $UN.castvwtp0{queue(a)}(prf | ch.queue)+    val xs = $UN.castvwtp0{queue(a)}((prf | ch.queue))     val x = channel_remove_helper<a>(chan, xs)     prval prf = $UN.castview0{locked_v(l1)}(xs)     val () = mutex_unlock(prf | mutex) }

@@ -52,14 +52,14 @@       let         prval (pf21, pf22) = array_v_uncons(pf2)         var res = wclbuf(pf22 | ptr_succ<byte>(p2), pz, c, res + 1)-        prval () = pf2 := array_v_cons(pf21, pf22)-        prval () = pf := bytes_v_unsplit(pf1, pf2)+        prval () = pf2 := array_v_cons(pf21,pf22)+        prval () = pf := bytes_v_unsplit(pf1,pf2)       in         res       end     else       let-        prval () = pf := bytes_v_unsplit(pf1, pf2)+        prval () = pf := bytes_v_unsplit(pf1,pf2)       in         res       end

@@ -51,7 +51,7 @@               val () = p := ptr1_succ<int>(p)                              //-              prval () = pf0 := array_v_extend{int}(pf0, pf_at)+              prval () = pf0 := array_v_extend{int}(pf0,pf_at)               val () = i := i + 1                              //@@ -61,7 +61,7 @@         //         prval () = pf_arr := pf0         prval () = array_v_unnil{int?}(pf1)-        prval pf_arr = array_v_cons{int}(pf1_at, pf_arr)+        prval pf_arr = array_v_cons{int}(pf1_at,pf_arr)                  //         val res = arrayptr_encode(pf_arr, pf_gc | p_arr)

@@ -100,7 +100,6 @@ ( // argless ) : [false] void = let-// prval pfprm = __assert() where {@@ -108,12 +107,10 @@ } prval [m2:int] () = mylemma_main{m,n,2}(pfprm)-// prval () = __assert() where { extern praxi __assert(): [m > n] void } prval () = __assert() where { extern praxi __assert(): [m2 >= 1] void }-// in   auxmain{n,m2}() end

@@ -46,7 +46,7 @@     prval () = square_is_nat{n}()     prval () = lemma_PRIME_param(pfprm)     prval pfmod1 = lemma_MOD0_intr{m*m,p,n*n}()-    prval pfmod2 = mylemma1{m,p}(pfmod1, pfprm)+    prval pfmod2 = mylemma1{m,p}(pfmod1,pfprm)     prval [m2:int]EQINT() = lemma_MOD0_elim(pfmod2)     prval EQINT() = pfeq_mm_pnn     prval () = __assert{p}{p*m2*m2,n*n}() where@@ -70,21 +70,16 @@     prfun auxmain { m, n : nat | n >= 1; m*m == 2*n*n } .<m>. () :       [false] void =       let-        //         prval pfprm = __assert() where         { extern           praxi __assert() : PRIME(2) }         prval [m2:int]() = mylemma_main{m,n,2}(pfprm)-        -        //         prval () = __assert() where         { extern           praxi __assert() : [m > n] void }         prval () = __assert() where         { extern           praxi __assert() : [m2 >= 1] void }-        -        //       in         auxmain{n,m2}()       end

@@ -0,0 +1,41 @@+absprop FUNCTOR_PROP (A : prop, n : int)++absprop BASE_FUNCTOR_PROP (A : prop, B : prop)++dataprop LIST_PROP(A: prop, int) =+  | LIST_PROP_NIL(A, 0) of ()+  | { n : nat | n > 0 } LIST_PROP_CONS(A, n) of (A, LIST_PROP(A, n - 1))++dataprop LISTF_PROP(A: prop, B: prop) =+  | LISTF_PROP_NIL(A, B) of ()+  | LISTF_PROP_CONS(A, B) of (A, B)++extern+prfun MAP {A:prop}{B:prop}{C:prop} (F : B -<prf> C, X : BASE_FUNCTOR_PROP(A, B)) : BASE_FUNCTOR_PROP(A, C)++propdef ALGEBRA (A : prop, B : prop) = BASE_FUNCTOR_PROP(A, B) -<prf> B++extern+prfun {A:prop} PROJECT {n:nat} (FUNCTOR_PROP(A,n)) : BASE_FUNCTOR_PROP(A, FUNCTOR_PROP(A,n-1))++extern+prfn {A:prop}{B:prop} EMPTY_FUNCTOR {n:nat}  : BASE_FUNCTOR_PROP(A, FUNCTOR_PROP(A,n))++assume FUNCTOR_PROP(A, n) = LIST_PROP(A, n)+assume BASE_FUNCTOR_PROP(A, B) = LISTF_PROP(A, B)++prfun {A:prop}{B:prop} CATA {n:nat} .<n>. (F : ALGEBRA(A, B), A : FUNCTOR_PROP(A, n)) : B =+  sif n == 0 then+    F(LISTF_PROP_NIL)+  else+    F(MAP(lam A0 =<prf> CATA(F,A0),PROJECT(A)))++primplmnt MAP (F, XS) =+  case+ XS of+    | LISTF_PROP_NIL() => LISTF_PROP_NIL()+    | LISTF_PROP_CONS (Y, YS) => LISTF_PROP_CONS(Y,F(YS))++primplmnt {A} PROJECT (A) =+  case+ A of+    | LIST_PROP_NIL() => LISTF_PROP_NIL()+    | LIST_PROP_CONS (B, BS) => LISTF_PROP_CONS(B,BS)

@@ -0,0 +1,47 @@+absprop FUNCTOR_PROP (A : prop, n : int)++absprop BASE_FUNCTOR_PROP (A : prop, B : prop)++dataprop LIST_PROP(A: prop, int) =+  | LIST_PROP_NIL(A, 0) of ()+  | { n : nat | n > 0 } LIST_PROP_CONS(A, n) of (A, LIST_PROP(A, n - 1))++dataprop LISTF_PROP(A: prop, B: prop) =+  | LISTF_PROP_NIL(A, B) of ()+  | LISTF_PROP_CONS(A, B) of (A, B)++extern+prfun MAP {A:prop}{B:prop}{C:prop} ( F : B -<prf> C+                                   , X : BASE_FUNCTOR_PROP(A, B)+                                   ) : BASE_FUNCTOR_PROP(A, C)++propdef ALGEBRA (A : prop, B : prop) = BASE_FUNCTOR_PROP(A, B) -<prf> B++extern+prfun {A:prop} PROJECT {n:nat} (FUNCTOR_PROP(A,n)) :+  BASE_FUNCTOR_PROP(A, FUNCTOR_PROP(A,n-1))++extern+prfn {A:prop}{B:prop} EMPTY_FUNCTOR {n:nat}  :+  BASE_FUNCTOR_PROP(A, FUNCTOR_PROP(A,n))++assume FUNCTOR_PROP(A, n) = LIST_PROP(A, n)+assume BASE_FUNCTOR_PROP(A, B) = LISTF_PROP(A, B)++prfun {A:prop}{B:prop} CATA {n:nat} .<n>. ( F : ALGEBRA(A, B)+                                          , A : FUNCTOR_PROP(A, n)+                                          ) : B =+  sif n == 0 then+    F(LISTF_PROP_NIL)+  else+    F(MAP(lam A0 =<prf> CATA(F,A0),PROJECT(A)))++primplmnt MAP (F, XS) =+  case+ XS of+    | LISTF_PROP_NIL() => LISTF_PROP_NIL()+    | LISTF_PROP_CONS (Y, YS) => LISTF_PROP_CONS(Y,F(YS))++primplmnt {A} PROJECT (A) =+  case+ A of+    | LIST_PROP_NIL() => LISTF_PROP_NIL()+    | LIST_PROP_CONS (B, BS) => LISTF_PROP_CONS(B,BS)

@@ -0,0 +1,74 @@+(***********************************************************************)+(*                                                                     *)+(*                         Applied Type System                         *)+(*                                                                     *)+(***********************************************************************)++(*+** ATS/Postiats - Unleashing the Potential of Types!+** Copyright (C) 2010-2015 Hongwei Xi, ATS Trustful Software, Inc.+** All rights reserved+**+** ATS is free software;  you can  redistribute it and/or modify it under+** the terms of  the GNU GENERAL PUBLIC LICENSE (GPL) as published by the+** Free Software Foundation; either version 3, or (at  your  option)  any+** later version.+**+** ATS is distributed in the hope that it will be useful, but WITHOUT ANY+** WARRANTY; without  even  the  implied  warranty  of MERCHANTABILITY or+** FITNESS FOR A PARTICULAR PURPOSE.  See the  GNU General Public License+** for more details.+**+** You  should  have  received  a  copy of the GNU General Public License+** along  with  ATS;  see the  file COPYING.  If not, please write to the+** Free Software Foundation,  51 Franklin Street, Fifth Floor, Boston, MA+** 02110-1301, USA.+*)++(* ****** ****** *)++(*+** Source:+** $PATSHOME/prelude/DATS/CODEGEN/bool.atxt+** Time of generation: Thu Jan 11 11:00:12 2018+*)++(* ****** ****** *)++(* Author: Hongwei Xi *)+(* Authoremail: hwxi AT cs DOT bu DOT edu *)+(* Start time: Feburary, 2012 *)++(* ****** ****** *)++#define ATS_DYNLOADFLAG 0 // no dynloading at run-time++(* ****** ****** *)++(*+//+// HX: see CATS/bool.cats+//+implement+bool2string+  (b) = if b then "true" else "false"+// end of [bool2string]+*)++(* ****** ****** *)++(*+//+// HX: see CATS/bool.cats+//+implement+fprint_bool (out, x) =+  fprint_string (out, bool2string (x))+// end of [fprint_bool]+*)++implement fprint_val<bool> = fprint_bool++(* ****** ****** *)++(* end of [bool.dats] *)

@@ -0,0 +1,553 @@+(***********************************************************************)+(*                                                                     *)+(*                         Applied Type System                         *)+(*                                                                     *)+(***********************************************************************)++(*+** ATS/Postiats - Unleashing the Potential of Types!+** Copyright (C) 2010-2015 Hongwei Xi, ATS Trustful Software, Inc.+** All rights reserved+**+** ATS is free software;  you can  redistribute it and/or modify it under+** the terms of  the GNU GENERAL PUBLIC LICENSE (GPL) as published by the+** Free Software Foundation; either version 3, or (at  your  option)  any+** later version.+**+** ATS is distributed in the hope that it will be useful, but WITHOUT ANY+** WARRANTY; without  even  the  implied  warranty  of MERCHANTABILITY or+** FITNESS FOR A PARTICULAR PURPOSE.  See the  GNU General Public License+** for more details.+**+** You  should  have  received  a  copy of the GNU General Public License+** along  with  ATS;  see the  file COPYING.  If not, please write to the+** Free Software Foundation,  51 Franklin Street, Fifth Floor, Boston, MA+** 02110-1301, USA.+*)++(* ****** ****** *)++(* Author: Hongwei Xi *)+(* Authoremail: gmhwxiATgmailDOTcom *)+(* Start time: February, 2014 *)++(* ****** ****** *)++(*+** Source:+** $PATSHOME/prelude/DATS/CODEGEN/integer_fixed.atxt+** Time of generation: Thu Jan 11 11:00:14 2018+*)++(* ****** ****** *)++#define+ATS_DYNLOADFLAG 0 // no dynloading++(* ****** ****** *)+//+staload UN = "prelude/SATS/unsafe.sats"+//+(* ****** ****** *)+//+implement+g0int2int<int8knd,intknd> = g0int2int_int8_int+implement+g0int2int<int16knd,intknd> = g0int2int_int16_int+implement+g0int2int<int32knd,intknd> = g0int2int_int32_int+implement+g0int2int<int64knd,intknd> = g0int2int_int64_int+//+(* ****** ****** *)+//+implement+g0int2uint<int8knd,uintknd> = g0int2uint_int8_uint+implement+g0int2uint<int16knd,uintknd> = g0int2uint_int16_uint+implement+g0int2uint<int32knd,uintknd> = g0int2uint_int32_uint+implement+g0int2uint<int64knd,uintknd> = g0int2uint_int64_uint+//+implement+g0uint2int<uint8knd,intknd> = g0uint2int_uint8_int+implement+g0uint2int<uint16knd,intknd> = g0uint2int_uint16_int+implement+g0uint2int<uint32knd,intknd> = g0uint2int_uint32_int+implement+g0uint2int<uint64knd,intknd> = g0uint2int_uint64_int+//+implement+g0uint2uint<uint8knd,uintknd> = g0uint2uint_uint8_uint+implement+g0uint2uint<uint16knd,uintknd> = g0uint2uint_uint16_uint+implement+g0uint2uint<uint32knd,uintknd> = g0uint2uint_uint32_uint+implement+g0uint2uint<uint64knd,uintknd> = g0uint2uint_uint64_uint+//+(* ****** ****** *)+//+implement+g0int_neg<int8knd> = g0int_neg_int8+implement+g0int_abs<int8knd> = g0int_abs_int8+implement+g0int_succ<int8knd> = g0int_succ_int8+implement+g0int_pred<int8knd> = g0int_pred_int8+implement+g0int_half<int8knd> = g0int_half_int8+implement+g0int_add<int8knd> = g0int_add_int8+implement+g0int_sub<int8knd> = g0int_sub_int8+implement+g0int_mul<int8knd> = g0int_mul_int8+implement+g0int_div<int8knd> = g0int_div_int8+implement+g0int_mod<int8knd> = g0int_mod_int8+implement+g0int_asl<int8knd> = g0int_asl_int8+implement+g0int_asr<int8knd> = g0int_asr_int8+implement+g0int_isltz<int8knd> = g0int_isltz_int8+implement+g0int_isltez<int8knd> = g0int_isltez_int8+implement+g0int_isgtz<int8knd> = g0int_isgtz_int8+implement+g0int_isgtez<int8knd> = g0int_isgtez_int8+implement+g0int_iseqz<int8knd> = g0int_iseqz_int8+implement+g0int_isneqz<int8knd> = g0int_isneqz_int8+implement+g0int_lt<int8knd> = g0int_lt_int8+implement+g0int_lte<int8knd> = g0int_lte_int8+implement+g0int_gt<int8knd> = g0int_gt_int8+implement+g0int_gte<int8knd> = g0int_gte_int8+implement+g0int_eq<int8knd> = g0int_eq_int8+implement+g0int_neq<int8knd> = g0int_neq_int8+implement+g0int_compare<int8knd> = g0int_compare_int8+implement+g0int_max<int8knd> = g0int_max_int8+implement+g0int_min<int8knd> = g0int_min_int8+//+implement+fprint_val<int8> (out, x) = fprint_int8 (out, x)+//+implement+g0int_neg<int16knd> = g0int_neg_int16+implement+g0int_abs<int16knd> = g0int_abs_int16+implement+g0int_succ<int16knd> = g0int_succ_int16+implement+g0int_pred<int16knd> = g0int_pred_int16+implement+g0int_half<int16knd> = g0int_half_int16+implement+g0int_add<int16knd> = g0int_add_int16+implement+g0int_sub<int16knd> = g0int_sub_int16+implement+g0int_mul<int16knd> = g0int_mul_int16+implement+g0int_div<int16knd> = g0int_div_int16+implement+g0int_mod<int16knd> = g0int_mod_int16+implement+g0int_asl<int16knd> = g0int_asl_int16+implement+g0int_asr<int16knd> = g0int_asr_int16+implement+g0int_isltz<int16knd> = g0int_isltz_int16+implement+g0int_isltez<int16knd> = g0int_isltez_int16+implement+g0int_isgtz<int16knd> = g0int_isgtz_int16+implement+g0int_isgtez<int16knd> = g0int_isgtez_int16+implement+g0int_iseqz<int16knd> = g0int_iseqz_int16+implement+g0int_isneqz<int16knd> = g0int_isneqz_int16+implement+g0int_lt<int16knd> = g0int_lt_int16+implement+g0int_lte<int16knd> = g0int_lte_int16+implement+g0int_gt<int16knd> = g0int_gt_int16+implement+g0int_gte<int16knd> = g0int_gte_int16+implement+g0int_eq<int16knd> = g0int_eq_int16+implement+g0int_neq<int16knd> = g0int_neq_int16+implement+g0int_compare<int16knd> = g0int_compare_int16+implement+g0int_max<int16knd> = g0int_max_int16+implement+g0int_min<int16knd> = g0int_min_int16+//+implement+fprint_val<int16> (out, x) = fprint_int16 (out, x)+//+implement+g0int_neg<int32knd> = g0int_neg_int32+implement+g0int_abs<int32knd> = g0int_abs_int32+implement+g0int_succ<int32knd> = g0int_succ_int32+implement+g0int_pred<int32knd> = g0int_pred_int32+implement+g0int_half<int32knd> = g0int_half_int32+implement+g0int_add<int32knd> = g0int_add_int32+implement+g0int_sub<int32knd> = g0int_sub_int32+implement+g0int_mul<int32knd> = g0int_mul_int32+implement+g0int_div<int32knd> = g0int_div_int32+implement+g0int_mod<int32knd> = g0int_mod_int32+implement+g0int_asl<int32knd> = g0int_asl_int32+implement+g0int_asr<int32knd> = g0int_asr_int32+implement+g0int_isltz<int32knd> = g0int_isltz_int32+implement+g0int_isltez<int32knd> = g0int_isltez_int32+implement+g0int_isgtz<int32knd> = g0int_isgtz_int32+implement+g0int_isgtez<int32knd> = g0int_isgtez_int32+implement+g0int_iseqz<int32knd> = g0int_iseqz_int32+implement+g0int_isneqz<int32knd> = g0int_isneqz_int32+implement+g0int_lt<int32knd> = g0int_lt_int32+implement+g0int_lte<int32knd> = g0int_lte_int32+implement+g0int_gt<int32knd> = g0int_gt_int32+implement+g0int_gte<int32knd> = g0int_gte_int32+implement+g0int_eq<int32knd> = g0int_eq_int32+implement+g0int_neq<int32knd> = g0int_neq_int32+implement+g0int_compare<int32knd> = g0int_compare_int32+implement+g0int_max<int32knd> = g0int_max_int32+implement+g0int_min<int32knd> = g0int_min_int32+//+implement+fprint_val<int32> (out, x) = fprint_int32 (out, x)+//+implement+g0int_neg<int64knd> = g0int_neg_int64+implement+g0int_abs<int64knd> = g0int_abs_int64+implement+g0int_succ<int64knd> = g0int_succ_int64+implement+g0int_pred<int64knd> = g0int_pred_int64+implement+g0int_half<int64knd> = g0int_half_int64+implement+g0int_add<int64knd> = g0int_add_int64+implement+g0int_sub<int64knd> = g0int_sub_int64+implement+g0int_mul<int64knd> = g0int_mul_int64+implement+g0int_div<int64knd> = g0int_div_int64+implement+g0int_mod<int64knd> = g0int_mod_int64+implement+g0int_asl<int64knd> = g0int_asl_int64+implement+g0int_asr<int64knd> = g0int_asr_int64+implement+g0int_isltz<int64knd> = g0int_isltz_int64+implement+g0int_isltez<int64knd> = g0int_isltez_int64+implement+g0int_isgtz<int64knd> = g0int_isgtz_int64+implement+g0int_isgtez<int64knd> = g0int_isgtez_int64+implement+g0int_iseqz<int64knd> = g0int_iseqz_int64+implement+g0int_isneqz<int64knd> = g0int_isneqz_int64+implement+g0int_lt<int64knd> = g0int_lt_int64+implement+g0int_lte<int64knd> = g0int_lte_int64+implement+g0int_gt<int64knd> = g0int_gt_int64+implement+g0int_gte<int64knd> = g0int_gte_int64+implement+g0int_eq<int64knd> = g0int_eq_int64+implement+g0int_neq<int64knd> = g0int_neq_int64+implement+g0int_compare<int64knd> = g0int_compare_int64+implement+g0int_max<int64knd> = g0int_max_int64+implement+g0int_min<int64knd> = g0int_min_int64+//+implement+fprint_val<int64> (out, x) = fprint_int64 (out, x)+//+(* ****** ****** *)+//+implement+g0uint_succ<uint8knd> = g0uint_succ_uint8+implement+g0uint_pred<uint8knd> = g0uint_pred_uint8+implement+g0uint_half<uint8knd> = g0uint_half_uint8+implement+g0uint_add<uint8knd> = g0uint_add_uint8+implement+g0uint_sub<uint8knd> = g0uint_sub_uint8+implement+g0uint_mul<uint8knd> = g0uint_mul_uint8+implement+g0uint_div<uint8knd> = g0uint_div_uint8+implement+g0uint_mod<uint8knd> = g0uint_mod_uint8+implement+g0uint_lsl<uint8knd> = g0uint_lsl_uint8+implement+g0uint_lsr<uint8knd> = g0uint_lsr_uint8+implement+g0uint_lnot<uint8knd> = g0uint_lnot_uint8+implement+g0uint_lor<uint8knd> = g0uint_lor_uint8+implement+g0uint_lxor<uint8knd> = g0uint_lxor_uint8+implement+g0uint_land<uint8knd> = g0uint_land_uint8+implement+g0uint_isgtz<uint8knd> = g0uint_isgtz_uint8+implement+g0uint_iseqz<uint8knd> = g0uint_iseqz_uint8+implement+g0uint_isneqz<uint8knd> = g0uint_isneqz_uint8+implement+g0uint_lt<uint8knd> = g0uint_lt_uint8+implement+g0uint_lte<uint8knd> = g0uint_lte_uint8+implement+g0uint_gt<uint8knd> = g0uint_gt_uint8+implement+g0uint_gte<uint8knd> = g0uint_gte_uint8+implement+g0uint_eq<uint8knd> = g0uint_eq_uint8+implement+g0uint_neq<uint8knd> = g0uint_neq_uint8+implement+g0uint_compare<uint8knd> = g0uint_compare_uint8+implement+g0uint_max<uint8knd> = g0uint_max_uint8+implement+g0uint_min<uint8knd> = g0uint_min_uint8+//+implement+fprint_val<uint8> (out, x) = fprint_uint8 (out, x)+//+implement+g0uint_succ<uint16knd> = g0uint_succ_uint16+implement+g0uint_pred<uint16knd> = g0uint_pred_uint16+implement+g0uint_half<uint16knd> = g0uint_half_uint16+implement+g0uint_add<uint16knd> = g0uint_add_uint16+implement+g0uint_sub<uint16knd> = g0uint_sub_uint16+implement+g0uint_mul<uint16knd> = g0uint_mul_uint16+implement+g0uint_div<uint16knd> = g0uint_div_uint16+implement+g0uint_mod<uint16knd> = g0uint_mod_uint16+implement+g0uint_lsl<uint16knd> = g0uint_lsl_uint16+implement+g0uint_lsr<uint16knd> = g0uint_lsr_uint16+implement+g0uint_lnot<uint16knd> = g0uint_lnot_uint16+implement+g0uint_lor<uint16knd> = g0uint_lor_uint16+implement+g0uint_lxor<uint16knd> = g0uint_lxor_uint16+implement+g0uint_land<uint16knd> = g0uint_land_uint16+implement+g0uint_isgtz<uint16knd> = g0uint_isgtz_uint16+implement+g0uint_iseqz<uint16knd> = g0uint_iseqz_uint16+implement+g0uint_isneqz<uint16knd> = g0uint_isneqz_uint16+implement+g0uint_lt<uint16knd> = g0uint_lt_uint16+implement+g0uint_lte<uint16knd> = g0uint_lte_uint16+implement+g0uint_gt<uint16knd> = g0uint_gt_uint16+implement+g0uint_gte<uint16knd> = g0uint_gte_uint16+implement+g0uint_eq<uint16knd> = g0uint_eq_uint16+implement+g0uint_neq<uint16knd> = g0uint_neq_uint16+implement+g0uint_compare<uint16knd> = g0uint_compare_uint16+implement+g0uint_max<uint16knd> = g0uint_max_uint16+implement+g0uint_min<uint16knd> = g0uint_min_uint16+//+implement+fprint_val<uint16> (out, x) = fprint_uint16 (out, x)+//+implement+g0uint_succ<uint32knd> = g0uint_succ_uint32+implement+g0uint_pred<uint32knd> = g0uint_pred_uint32+implement+g0uint_half<uint32knd> = g0uint_half_uint32+implement+g0uint_add<uint32knd> = g0uint_add_uint32+implement+g0uint_sub<uint32knd> = g0uint_sub_uint32+implement+g0uint_mul<uint32knd> = g0uint_mul_uint32+implement+g0uint_div<uint32knd> = g0uint_div_uint32+implement+g0uint_mod<uint32knd> = g0uint_mod_uint32+implement+g0uint_lsl<uint32knd> = g0uint_lsl_uint32+implement+g0uint_lsr<uint32knd> = g0uint_lsr_uint32+implement+g0uint_lnot<uint32knd> = g0uint_lnot_uint32+implement+g0uint_lor<uint32knd> = g0uint_lor_uint32+implement+g0uint_lxor<uint32knd> = g0uint_lxor_uint32+implement+g0uint_land<uint32knd> = g0uint_land_uint32+implement+g0uint_isgtz<uint32knd> = g0uint_isgtz_uint32+implement+g0uint_iseqz<uint32knd> = g0uint_iseqz_uint32+implement+g0uint_isneqz<uint32knd> = g0uint_isneqz_uint32+implement+g0uint_lt<uint32knd> = g0uint_lt_uint32+implement+g0uint_lte<uint32knd> = g0uint_lte_uint32+implement+g0uint_gt<uint32knd> = g0uint_gt_uint32+implement+g0uint_gte<uint32knd> = g0uint_gte_uint32+implement+g0uint_eq<uint32knd> = g0uint_eq_uint32+implement+g0uint_neq<uint32knd> = g0uint_neq_uint32+implement+g0uint_compare<uint32knd> = g0uint_compare_uint32+implement+g0uint_max<uint32knd> = g0uint_max_uint32+implement+g0uint_min<uint32knd> = g0uint_min_uint32+//+implement+fprint_val<uint32> (out, x) = fprint_uint32 (out, x)+//+implement+g0uint_succ<uint64knd> = g0uint_succ_uint64+implement+g0uint_pred<uint64knd> = g0uint_pred_uint64+implement+g0uint_half<uint64knd> = g0uint_half_uint64+implement+g0uint_add<uint64knd> = g0uint_add_uint64+implement+g0uint_sub<uint64knd> = g0uint_sub_uint64+implement+g0uint_mul<uint64knd> = g0uint_mul_uint64+implement+g0uint_div<uint64knd> = g0uint_div_uint64+implement+g0uint_mod<uint64knd> = g0uint_mod_uint64+implement+g0uint_lsl<uint64knd> = g0uint_lsl_uint64+implement+g0uint_lsr<uint64knd> = g0uint_lsr_uint64+implement+g0uint_lnot<uint64knd> = g0uint_lnot_uint64+implement+g0uint_lor<uint64knd> = g0uint_lor_uint64+implement+g0uint_lxor<uint64knd> = g0uint_lxor_uint64+implement+g0uint_land<uint64knd> = g0uint_land_uint64+implement+g0uint_isgtz<uint64knd> = g0uint_isgtz_uint64+implement+g0uint_iseqz<uint64knd> = g0uint_iseqz_uint64+implement+g0uint_isneqz<uint64knd> = g0uint_isneqz_uint64+implement+g0uint_lt<uint64knd> = g0uint_lt_uint64+implement+g0uint_lte<uint64knd> = g0uint_lte_uint64+implement+g0uint_gt<uint64knd> = g0uint_gt_uint64+implement+g0uint_gte<uint64knd> = g0uint_gte_uint64+implement+g0uint_eq<uint64knd> = g0uint_eq_uint64+implement+g0uint_neq<uint64knd> = g0uint_neq_uint64+implement+g0uint_compare<uint64knd> = g0uint_compare_uint64+implement+g0uint_max<uint64knd> = g0uint_max_uint64+implement+g0uint_min<uint64knd> = g0uint_min_uint64+//+implement+fprint_val<uint64> (out, x) = fprint_uint64 (out, x)+//+(* ****** ****** *)++(* end of [integer_fixed.dats] *)

@@ -0,0 +1,576 @@+(***********************************************************************)+(*                                                                     *)+(*                         Applied Type System                         *)+(*                                                                     *)+(***********************************************************************)++(*+** ATS/Postiats - Unleashing the Potential of Types!+** Copyright (C) 2010-2015 Hongwei Xi, ATS Trustful Software, Inc.+** All rights reserved+**+** ATS is free software;  you can  redistribute it and/or modify it under+** the terms of  the GNU GENERAL PUBLIC LICENSE (GPL) as published by the+** Free Software Foundation; either version 3, or (at  your  option)  any+** later version.+**+** ATS is distributed in the hope that it will be useful, but WITHOUT ANY+** WARRANTY; without  even  the  implied  warranty  of MERCHANTABILITY or+** FITNESS FOR A PARTICULAR PURPOSE.  See the  GNU General Public License+** for more details.+**+** You  should  have  received  a  copy of the GNU General Public License+** along  with  ATS;  see the  file COPYING.  If not, please write to the+** Free Software Foundation,  51 Franklin Street, Fifth Floor, Boston, MA+** 02110-1301, USA.+*)++(* ****** ****** *)++(* Author: Hongwei Xi *)+(* Authoremail: gmhwxiATgmailDOTcom *)+(* Start time: February, 2014 *)++(* ****** ****** *)++(*+** Source:+** $PATSHOME/prelude/DATS/CODEGEN/integer_long.atxt+** Time of generation: Thu Jan 11 11:00:12 2018+*)++(* ****** ****** *)++#define+ATS_DYNLOADFLAG 0 // no dynloading++(* ****** ****** *)+//+staload UN = "prelude/SATS/unsafe.sats"+//+(* ****** ****** *)+//+implement+g0int2int<intknd,lintknd> = g0int2int_int_lint+implement+g1int2int<intknd,lintknd> = g1int2int_int_lint+//+implement+g0uint2int<uintknd,lintknd> = g0uint2int_uint_lint+implement+g1uint2int<uintknd,lintknd> = g1uint2int_uint_lint+//+(* ****** ****** *)+//+implement+g0int2uint<intknd,ulintknd> = g0int2uint_int_ulint+implement+g1int2uint<intknd,ulintknd> = g1int2uint_int_ulint+//+implement+g0uint2uint<uintknd,ulintknd> = g0uint2uint_uint_ulint+implement+g1uint2uint<uintknd,ulintknd> = g1uint2uint_uint_ulint+//+(* ****** ****** *)+//+implement+g0int2int<intknd,llintknd> = g0int2int_int_llint+implement+g1int2int<intknd,llintknd> = g1int2int_int_llint+//+implement+g0uint2int<uintknd,llintknd> = g0uint2int_uint_llint+implement+g1uint2int<uintknd,llintknd> = g1uint2int_uint_llint+//+(* ****** ****** *)+//+implement+g0int2uint<intknd,ullintknd> = g0int2uint_int_ullint+implement+g1int2uint<intknd,ullintknd> = g1int2uint_int_ullint+//+implement+g0uint2uint<uintknd,ullintknd> = g0uint2uint_uint_ullint+implement+g1uint2uint<uintknd,ullintknd> = g1uint2uint_uint_ullint+//+(* ****** ****** *)+//+implement+g0int2int<lintknd,lintknd> = g0int2int_lint_lint+implement+g0int2int<lintknd,llintknd> = g0int2int_lint_llint+//+implement+g0int2uint<lintknd,ulintknd> = g0int2uint_lint_ulint+implement+g0int2uint<lintknd,ullintknd> = g0int2uint_lint_ullint+//+(* ****** ****** *)+//+implement+g0uint2int<ulintknd,lintknd> = g0uint2int_ulint_lint+implement+g0uint2int<ulintknd,llintknd> = g0uint2int_ulint_llint+//+implement+g0uint2uint<ulintknd,ulintknd> = g0uint2uint_ulint_ulint+implement+g0uint2uint<ulintknd,ullintknd> = g0uint2uint_ulint_ullint+//+(* ****** ****** *)+//+implement+g0int2int<llintknd,llintknd> = g0int2int_llint_llint+//+implement+g0int2uint<llintknd,ullintknd> = g0int2uint_llint_ullint+//+(* ****** ****** *)+//+implement+g0uint2int<ullintknd,llintknd> = g0uint2int_ullint_llint+//+implement+g0uint2uint<ullintknd,ullintknd> = g0uint2uint_ullint_ullint+//+(* ****** ****** *)+//+implement g0int2string<lintknd> = g0int2string_lint+implement g0int2string<llintknd> = g0int2string_llint+//+implement g0string2int<lintknd> = g0string2int_lint+implement g0string2int<llintknd> = g0string2int_llint+implement g0string2uint<ulintknd> = g0string2uint_ulint+implement g0string2uint<ullintknd> = g0string2uint_ullint+//+(* ****** ****** *)+//+implement+g0int_neg<lintknd> = g0int_neg_lint+implement+g0int_abs<lintknd> = g0int_abs_lint+implement+g0int_succ<lintknd> = g0int_succ_lint+implement+g0int_pred<lintknd> = g0int_pred_lint+implement+g0int_half<lintknd> = g0int_half_lint+implement+g0int_add<lintknd> = g0int_add_lint+implement+g0int_sub<lintknd> = g0int_sub_lint+implement+g0int_mul<lintknd> = g0int_mul_lint+implement+g0int_div<lintknd> = g0int_div_lint+implement+g0int_mod<lintknd> = g0int_mod_lint+implement+g0int_asl<lintknd> = g0int_asl_lint+implement+g0int_asr<lintknd> = g0int_asr_lint+implement+g0int_isltz<lintknd> = g0int_isltz_lint+implement+g0int_isltez<lintknd> = g0int_isltez_lint+implement+g0int_isgtz<lintknd> = g0int_isgtz_lint+implement+g0int_isgtez<lintknd> = g0int_isgtez_lint+implement+g0int_iseqz<lintknd> = g0int_iseqz_lint+implement+g0int_isneqz<lintknd> = g0int_isneqz_lint+implement+g0int_lt<lintknd> = g0int_lt_lint+implement+g0int_lte<lintknd> = g0int_lte_lint+implement+g0int_gt<lintknd> = g0int_gt_lint+implement+g0int_gte<lintknd> = g0int_gte_lint+implement+g0int_eq<lintknd> = g0int_eq_lint+implement+g0int_neq<lintknd> = g0int_neq_lint+implement+g0int_compare<lintknd> = g0int_compare_lint+implement+g0int_max<lintknd> = g0int_max_lint+implement+g0int_min<lintknd> = g0int_min_lint+//+implement+fprint_val<lint> (out, x) = fprint_lint (out, x)//+implement+g1int_neg<lintknd> = g1int_neg_lint+implement+g1int_abs<lintknd> = g1int_abs_lint+implement+g1int_succ<lintknd> = g1int_succ_lint+implement+g1int_pred<lintknd> = g1int_pred_lint+implement+g1int_half<lintknd> = g1int_half_lint+implement+g1int_add<lintknd> = g1int_add_lint+implement+g1int_sub<lintknd> = g1int_sub_lint+implement+g1int_mul<lintknd> = g1int_mul_lint+implement+g1int_div<lintknd> = g1int_div_lint+implement+g1int_nmod<lintknd> = g1int_nmod_lint+implement+g1int_isltz<lintknd> = g1int_isltz_lint+implement+g1int_isltez<lintknd> = g1int_isltez_lint+implement+g1int_isgtz<lintknd> = g1int_isgtz_lint+implement+g1int_isgtez<lintknd> = g1int_isgtez_lint+implement+g1int_iseqz<lintknd> = g1int_iseqz_lint+implement+g1int_isneqz<lintknd> = g1int_isneqz_lint+implement+g1int_lt<lintknd> = g1int_lt_lint+implement+g1int_lte<lintknd> = g1int_lte_lint+implement+g1int_gt<lintknd> = g1int_gt_lint+implement+g1int_gte<lintknd> = g1int_gte_lint+implement+g1int_eq<lintknd> = g1int_eq_lint+implement+g1int_neq<lintknd> = g1int_neq_lint+implement+g1int_compare<lintknd> = g1int_compare_lint+implement+g1int_max<lintknd> = g1int_max_lint+implement+g1int_min<lintknd> = g1int_min_lint+//+(* ****** ****** *)+//+implement+g0int_neg<llintknd> = g0int_neg_llint+implement+g0int_abs<llintknd> = g0int_abs_llint+implement+g0int_succ<llintknd> = g0int_succ_llint+implement+g0int_pred<llintknd> = g0int_pred_llint+implement+g0int_half<llintknd> = g0int_half_llint+implement+g0int_add<llintknd> = g0int_add_llint+implement+g0int_sub<llintknd> = g0int_sub_llint+implement+g0int_mul<llintknd> = g0int_mul_llint+implement+g0int_div<llintknd> = g0int_div_llint+implement+g0int_mod<llintknd> = g0int_mod_llint+implement+g0int_asl<llintknd> = g0int_asl_llint+implement+g0int_asr<llintknd> = g0int_asr_llint+implement+g0int_isltz<llintknd> = g0int_isltz_llint+implement+g0int_isltez<llintknd> = g0int_isltez_llint+implement+g0int_isgtz<llintknd> = g0int_isgtz_llint+implement+g0int_isgtez<llintknd> = g0int_isgtez_llint+implement+g0int_iseqz<llintknd> = g0int_iseqz_llint+implement+g0int_isneqz<llintknd> = g0int_isneqz_llint+implement+g0int_lt<llintknd> = g0int_lt_llint+implement+g0int_lte<llintknd> = g0int_lte_llint+implement+g0int_gt<llintknd> = g0int_gt_llint+implement+g0int_gte<llintknd> = g0int_gte_llint+implement+g0int_eq<llintknd> = g0int_eq_llint+implement+g0int_neq<llintknd> = g0int_neq_llint+implement+g0int_compare<llintknd> = g0int_compare_llint+implement+g0int_max<llintknd> = g0int_max_llint+implement+g0int_min<llintknd> = g0int_min_llint+//+implement+fprint_val<llint> (out, x) = fprint_llint (out, x)//+implement+g1int_neg<llintknd> = g1int_neg_llint+implement+g1int_abs<llintknd> = g1int_abs_llint+implement+g1int_succ<llintknd> = g1int_succ_llint+implement+g1int_pred<llintknd> = g1int_pred_llint+implement+g1int_half<llintknd> = g1int_half_llint+implement+g1int_add<llintknd> = g1int_add_llint+implement+g1int_sub<llintknd> = g1int_sub_llint+implement+g1int_mul<llintknd> = g1int_mul_llint+implement+g1int_div<llintknd> = g1int_div_llint+implement+g1int_nmod<llintknd> = g1int_nmod_llint+implement+g1int_isltz<llintknd> = g1int_isltz_llint+implement+g1int_isltez<llintknd> = g1int_isltez_llint+implement+g1int_isgtz<llintknd> = g1int_isgtz_llint+implement+g1int_isgtez<llintknd> = g1int_isgtez_llint+implement+g1int_iseqz<llintknd> = g1int_iseqz_llint+implement+g1int_isneqz<llintknd> = g1int_isneqz_llint+implement+g1int_lt<llintknd> = g1int_lt_llint+implement+g1int_lte<llintknd> = g1int_lte_llint+implement+g1int_gt<llintknd> = g1int_gt_llint+implement+g1int_gte<llintknd> = g1int_gte_llint+implement+g1int_eq<llintknd> = g1int_eq_llint+implement+g1int_neq<llintknd> = g1int_neq_llint+implement+g1int_compare<llintknd> = g1int_compare_llint+implement+g1int_max<llintknd> = g1int_max_llint+implement+g1int_min<llintknd> = g1int_min_llint+//+(* ****** ****** *)+//+implement+g0uint_succ<ulintknd> = g0uint_succ_ulint+implement+g0uint_pred<ulintknd> = g0uint_pred_ulint+implement+g0uint_half<ulintknd> = g0uint_half_ulint+implement+g0uint_add<ulintknd> = g0uint_add_ulint+implement+g0uint_sub<ulintknd> = g0uint_sub_ulint+implement+g0uint_mul<ulintknd> = g0uint_mul_ulint+implement+g0uint_div<ulintknd> = g0uint_div_ulint+implement+g0uint_mod<ulintknd> = g0uint_mod_ulint+implement+g0uint_lsl<ulintknd> = g0uint_lsl_ulint+implement+g0uint_lsr<ulintknd> = g0uint_lsr_ulint+implement+g0uint_lnot<ulintknd> = g0uint_lnot_ulint+implement+g0uint_lor<ulintknd> = g0uint_lor_ulint+implement+g0uint_lxor<ulintknd> = g0uint_lxor_ulint+implement+g0uint_land<ulintknd> = g0uint_land_ulint+implement+g0uint_isgtz<ulintknd> = g0uint_isgtz_ulint+implement+g0uint_iseqz<ulintknd> = g0uint_iseqz_ulint+implement+g0uint_isneqz<ulintknd> = g0uint_isneqz_ulint+implement+g0uint_lt<ulintknd> = g0uint_lt_ulint+implement+g0uint_lte<ulintknd> = g0uint_lte_ulint+implement+g0uint_gt<ulintknd> = g0uint_gt_ulint+implement+g0uint_gte<ulintknd> = g0uint_gte_ulint+implement+g0uint_eq<ulintknd> = g0uint_eq_ulint+implement+g0uint_neq<ulintknd> = g0uint_neq_ulint+implement+g0uint_compare<ulintknd> = g0uint_compare_ulint+implement+g0uint_max<ulintknd> = g0uint_max_ulint+implement+g0uint_min<ulintknd> = g0uint_min_ulint+//+implement+fprint_val<ulint> (out, x) = fprint_ulint (out, x)//+implement+g1uint_succ<ulintknd> = g1uint_succ_ulint+implement+g1uint_pred<ulintknd> = g1uint_pred_ulint+implement+g1uint_half<ulintknd> = g1uint_half_ulint+implement+g1uint_add<ulintknd> = g1uint_add_ulint+implement+g1uint_sub<ulintknd> = g1uint_sub_ulint+implement+g1uint_mul<ulintknd> = g1uint_mul_ulint+implement+g1uint_div<ulintknd> = g1uint_div_ulint+implement+g1uint_mod<ulintknd> = g1uint_mod_ulint+implement+g1uint_isgtz<ulintknd> = g1uint_isgtz_ulint+implement+g1uint_iseqz<ulintknd> = g1uint_iseqz_ulint+implement+g1uint_isneqz<ulintknd> = g1uint_isneqz_ulint+implement+g1uint_lt<ulintknd> = g1uint_lt_ulint+implement+g1uint_lte<ulintknd> = g1uint_lte_ulint+implement+g1uint_gt<ulintknd> = g1uint_gt_ulint+implement+g1uint_gte<ulintknd> = g1uint_gte_ulint+implement+g1uint_eq<ulintknd> = g1uint_eq_ulint+implement+g1uint_neq<ulintknd> = g1uint_neq_ulint+implement+g1uint_compare<ulintknd> = g1uint_compare_ulint+implement+g1uint_max<ulintknd> = g1uint_max_ulint+implement+g1uint_min<ulintknd> = g1uint_min_ulint+//+(* ****** ****** *)+//+implement+g0uint_succ<ullintknd> = g0uint_succ_ullint+implement+g0uint_pred<ullintknd> = g0uint_pred_ullint+implement+g0uint_half<ullintknd> = g0uint_half_ullint+implement+g0uint_add<ullintknd> = g0uint_add_ullint+implement+g0uint_sub<ullintknd> = g0uint_sub_ullint+implement+g0uint_mul<ullintknd> = g0uint_mul_ullint+implement+g0uint_div<ullintknd> = g0uint_div_ullint+implement+g0uint_mod<ullintknd> = g0uint_mod_ullint+implement+g0uint_lsl<ullintknd> = g0uint_lsl_ullint+implement+g0uint_lsr<ullintknd> = g0uint_lsr_ullint+implement+g0uint_lnot<ullintknd> = g0uint_lnot_ullint+implement+g0uint_lor<ullintknd> = g0uint_lor_ullint+implement+g0uint_lxor<ullintknd> = g0uint_lxor_ullint+implement+g0uint_land<ullintknd> = g0uint_land_ullint+implement+g0uint_isgtz<ullintknd> = g0uint_isgtz_ullint+implement+g0uint_iseqz<ullintknd> = g0uint_iseqz_ullint+implement+g0uint_isneqz<ullintknd> = g0uint_isneqz_ullint+implement+g0uint_lt<ullintknd> = g0uint_lt_ullint+implement+g0uint_lte<ullintknd> = g0uint_lte_ullint+implement+g0uint_gt<ullintknd> = g0uint_gt_ullint+implement+g0uint_gte<ullintknd> = g0uint_gte_ullint+implement+g0uint_eq<ullintknd> = g0uint_eq_ullint+implement+g0uint_neq<ullintknd> = g0uint_neq_ullint+implement+g0uint_compare<ullintknd> = g0uint_compare_ullint+implement+g0uint_max<ullintknd> = g0uint_max_ullint+implement+g0uint_min<ullintknd> = g0uint_min_ullint+//+implement+fprint_val<ullint> (out, x) = fprint_ullint (out, x)//+implement+g1uint_succ<ullintknd> = g1uint_succ_ullint+implement+g1uint_pred<ullintknd> = g1uint_pred_ullint+implement+g1uint_half<ullintknd> = g1uint_half_ullint+implement+g1uint_add<ullintknd> = g1uint_add_ullint+implement+g1uint_sub<ullintknd> = g1uint_sub_ullint+implement+g1uint_mul<ullintknd> = g1uint_mul_ullint+implement+g1uint_div<ullintknd> = g1uint_div_ullint+implement+g1uint_mod<ullintknd> = g1uint_mod_ullint+implement+g1uint_isgtz<ullintknd> = g1uint_isgtz_ullint+implement+g1uint_iseqz<ullintknd> = g1uint_iseqz_ullint+implement+g1uint_isneqz<ullintknd> = g1uint_isneqz_ullint+implement+g1uint_lt<ullintknd> = g1uint_lt_ullint+implement+g1uint_lte<ullintknd> = g1uint_lte_ullint+implement+g1uint_gt<ullintknd> = g1uint_gt_ullint+implement+g1uint_gte<ullintknd> = g1uint_gte_ullint+implement+g1uint_eq<ullintknd> = g1uint_eq_ullint+implement+g1uint_neq<ullintknd> = g1uint_neq_ullint+implement+g1uint_compare<ullintknd> = g1uint_compare_ullint+implement+g1uint_max<ullintknd> = g1uint_max_ullint+implement+g1uint_min<ullintknd> = g1uint_min_ullint+//+(* ****** ****** *)+//+implement+nmod_g1int_int1<lintknd>+  (x, y) = g1i2i(g1int_nmod<lintknd>(x, g1i2i(y)))+implement+nmod_g1int_int1<llintknd>+  (x, y) = g1i2i(g1int_nmod<llintknd>(x, g1i2i(y)))+//+(* ****** ****** *)++(* end of [integer_long.dats] *)

@@ -0,0 +1,183 @@+(***********************************************************************)+(*                                                                     *)+(*                         Applied Type System                         *)+(*                                                                     *)+(***********************************************************************)++(*+** ATS/Postiats - Unleashing the Potential of Types!+** Copyright (C) 2010-2015 Hongwei Xi, ATS Trustful Software, Inc.+** All rights reserved+**+** ATS is free software;  you can  redistribute it and/or modify it under+** the terms of  the GNU GENERAL PUBLIC LICENSE (GPL) as published by the+** Free Software Foundation; either version 3, or (at  your  option)  any+** later version.+**+** ATS is distributed in the hope that it will be useful, but WITHOUT ANY+** WARRANTY; without  even  the  implied  warranty  of MERCHANTABILITY or+** FITNESS FOR A PARTICULAR PURPOSE.  See the  GNU General Public License+** for more details.+**+** You  should  have  received  a  copy of the GNU General Public License+** along  with  ATS;  see the  file COPYING.  If not, please write to the+** Free Software Foundation,  51 Franklin Street, Fifth Floor, Boston, MA+** 02110-1301, USA.+*)++(* ****** ****** *)++(* Author: Hongwei Xi *)+(* Authoremail: gmhwxiATgmailDOTcom *)+(* Start time: February, 2014 *)++(* ****** ****** *)++(*+** Source:+** $PATSHOME/prelude/DATS/CODEGEN/integer_ptr.atxt+** Time of generation: Thu Jan 11 11:00:14 2018+*)++(* ****** ****** *)++#define+ATS_DYNLOADFLAG 0 // no dynloading++(* ****** ****** *)+//+staload UN = "prelude/SATS/unsafe.sats"+//+(* ****** ****** *)++implement+g0int2int<intknd,intptrknd> = g0int2int_int_intptr+implement+g0int2int<lintknd,intptrknd> = g0int2int_lint_intptr++(* ****** ****** *)++implement+g0uint2uint<uintknd,uintptrknd> = g0uint2uint_uint_uintptr+implement+g0uint2uint<ulintknd,uintptrknd> = g0uint2uint_ulint_uintptr++(* ****** ****** *)+//+implement+g0int_neg<intptrknd> = g0int_neg_intptr+implement+g0int_abs<intptrknd> = g0int_abs_intptr+implement+g0int_succ<intptrknd> = g0int_succ_intptr+implement+g0int_pred<intptrknd> = g0int_pred_intptr+implement+g0int_half<intptrknd> = g0int_half_intptr+implement+g0int_add<intptrknd> = g0int_add_intptr+implement+g0int_sub<intptrknd> = g0int_sub_intptr+implement+g0int_mul<intptrknd> = g0int_mul_intptr+implement+g0int_div<intptrknd> = g0int_div_intptr+implement+g0int_mod<intptrknd> = g0int_mod_intptr+implement+g0int_asl<intptrknd> = g0int_asl_intptr+implement+g0int_asr<intptrknd> = g0int_asr_intptr+implement+g0int_isltz<intptrknd> = g0int_isltz_intptr+implement+g0int_isltez<intptrknd> = g0int_isltez_intptr+implement+g0int_isgtz<intptrknd> = g0int_isgtz_intptr+implement+g0int_isgtez<intptrknd> = g0int_isgtez_intptr+implement+g0int_iseqz<intptrknd> = g0int_iseqz_intptr+implement+g0int_isneqz<intptrknd> = g0int_isneqz_intptr+implement+g0int_lt<intptrknd> = g0int_lt_intptr+implement+g0int_lte<intptrknd> = g0int_lte_intptr+implement+g0int_gt<intptrknd> = g0int_gt_intptr+implement+g0int_gte<intptrknd> = g0int_gte_intptr+implement+g0int_eq<intptrknd> = g0int_eq_intptr+implement+g0int_neq<intptrknd> = g0int_neq_intptr+implement+g0int_compare<intptrknd> = g0int_compare_intptr+implement+g0int_max<intptrknd> = g0int_max_intptr+implement+g0int_min<intptrknd> = g0int_min_intptr+//+implement+fprint_val<intptr> (out, x) = fprint_intptr (out, x)+//+implement+g0uint_succ<uintptrknd> = g0uint_succ_uintptr+implement+g0uint_pred<uintptrknd> = g0uint_pred_uintptr+implement+g0uint_half<uintptrknd> = g0uint_half_uintptr+implement+g0uint_add<uintptrknd> = g0uint_add_uintptr+implement+g0uint_sub<uintptrknd> = g0uint_sub_uintptr+implement+g0uint_mul<uintptrknd> = g0uint_mul_uintptr+implement+g0uint_div<uintptrknd> = g0uint_div_uintptr+implement+g0uint_mod<uintptrknd> = g0uint_mod_uintptr+implement+g0uint_lsl<uintptrknd> = g0uint_lsl_uintptr+implement+g0uint_lsr<uintptrknd> = g0uint_lsr_uintptr+implement+g0uint_lnot<uintptrknd> = g0uint_lnot_uintptr+implement+g0uint_lor<uintptrknd> = g0uint_lor_uintptr+implement+g0uint_lxor<uintptrknd> = g0uint_lxor_uintptr+implement+g0uint_land<uintptrknd> = g0uint_land_uintptr+implement+g0uint_isgtz<uintptrknd> = g0uint_isgtz_uintptr+implement+g0uint_iseqz<uintptrknd> = g0uint_iseqz_uintptr+implement+g0uint_isneqz<uintptrknd> = g0uint_isneqz_uintptr+implement+g0uint_lt<uintptrknd> = g0uint_lt_uintptr+implement+g0uint_lte<uintptrknd> = g0uint_lte_uintptr+implement+g0uint_gt<uintptrknd> = g0uint_gt_uintptr+implement+g0uint_gte<uintptrknd> = g0uint_gte_uintptr+implement+g0uint_eq<uintptrknd> = g0uint_eq_uintptr+implement+g0uint_neq<uintptrknd> = g0uint_neq_uintptr+implement+g0uint_compare<uintptrknd> = g0uint_compare_uintptr+implement+g0uint_max<uintptrknd> = g0uint_max_uintptr+implement+g0uint_min<uintptrknd> = g0uint_min_uintptr+//+implement+fprint_val<uintptr> (out, x) = fprint_uintptr (out, x)+//+(* ****** ****** *)++(* end of [integer_ptr.dats] *)

@@ -0,0 +1,183 @@+(***********************************************************************)+(*                                                                     *)+(*                         Applied Type System                         *)+(*                                                                     *)+(***********************************************************************)++(*+** ATS/Postiats - Unleashing the Potential of Types!+** Copyright (C) 2010-2015 Hongwei Xi, ATS Trustful Software, Inc.+** All rights reserved+**+** ATS is free software;  you can  redistribute it and/or modify it under+** the terms of  the GNU GENERAL PUBLIC LICENSE (GPL) as published by the+** Free Software Foundation; either version 3, or (at  your  option)  any+** later version.+**+** ATS is distributed in the hope that it will be useful, but WITHOUT ANY+** WARRANTY; without  even  the  implied  warranty  of MERCHANTABILITY or+** FITNESS FOR A PARTICULAR PURPOSE.  See the  GNU General Public License+** for more details.+**+** You  should  have  received  a  copy of the GNU General Public License+** along  with  ATS;  see the  file COPYING.  If not, please write to the+** Free Software Foundation,  51 Franklin Street, Fifth Floor, Boston, MA+** 02110-1301, USA.+*)++(* ****** ****** *)++(* Author: Hongwei Xi *)+(* Authoremail: gmhwxiATgmailDOTcom *)+(* Start time: February, 2014 *)++(* ****** ****** *)++(*+** Source:+** $PATSHOME/prelude/DATS/CODEGEN/integer_short.atxt+** Time of generation: Thu Jan 11 11:00:12 2018+*)++(* ****** ****** *)++#define+ATS_DYNLOADFLAG 0 // no dynloading++(* ****** ****** *)+//+staload UN = "prelude/SATS/unsafe.sats"+//+(* ****** ****** *)+//+implement+g0int2int<sintknd,intknd> = g0int2int_sint_int+implement+g0int2uint<sintknd,uintknd> = g0int2uint_sint_uint+//+(* ****** ****** *)+//+implement+g0uint2int<usintknd,intknd> = g0uint2int_usint_int+implement+g0uint2uint<usintknd,uintknd> = g0uint2uint_usint_uint+//+(* ****** ****** *)+//+implement+g0int_neg<sintknd> = g0int_neg_sint+implement+g0int_abs<sintknd> = g0int_abs_sint+implement+g0int_succ<sintknd> = g0int_succ_sint+implement+g0int_pred<sintknd> = g0int_pred_sint+implement+g0int_half<sintknd> = g0int_half_sint+implement+g0int_add<sintknd> = g0int_add_sint+implement+g0int_sub<sintknd> = g0int_sub_sint+implement+g0int_mul<sintknd> = g0int_mul_sint+implement+g0int_div<sintknd> = g0int_div_sint+implement+g0int_mod<sintknd> = g0int_mod_sint+implement+g0int_asl<sintknd> = g0int_asl_sint+implement+g0int_asr<sintknd> = g0int_asr_sint+implement+g0int_isltz<sintknd> = g0int_isltz_sint+implement+g0int_isltez<sintknd> = g0int_isltez_sint+implement+g0int_isgtz<sintknd> = g0int_isgtz_sint+implement+g0int_isgtez<sintknd> = g0int_isgtez_sint+implement+g0int_iseqz<sintknd> = g0int_iseqz_sint+implement+g0int_isneqz<sintknd> = g0int_isneqz_sint+implement+g0int_lt<sintknd> = g0int_lt_sint+implement+g0int_lte<sintknd> = g0int_lte_sint+implement+g0int_gt<sintknd> = g0int_gt_sint+implement+g0int_gte<sintknd> = g0int_gte_sint+implement+g0int_eq<sintknd> = g0int_eq_sint+implement+g0int_neq<sintknd> = g0int_neq_sint+implement+g0int_compare<sintknd> = g0int_compare_sint+implement+g0int_max<sintknd> = g0int_max_sint+implement+g0int_min<sintknd> = g0int_min_sint+//+implement+fprint_val<sint> (out, x) = fprint_sint (out, x)+//+implement+g0uint_succ<usintknd> = g0uint_succ_usint+implement+g0uint_pred<usintknd> = g0uint_pred_usint+implement+g0uint_half<usintknd> = g0uint_half_usint+implement+g0uint_add<usintknd> = g0uint_add_usint+implement+g0uint_sub<usintknd> = g0uint_sub_usint+implement+g0uint_mul<usintknd> = g0uint_mul_usint+implement+g0uint_div<usintknd> = g0uint_div_usint+implement+g0uint_mod<usintknd> = g0uint_mod_usint+implement+g0uint_lsl<usintknd> = g0uint_lsl_usint+implement+g0uint_lsr<usintknd> = g0uint_lsr_usint+implement+g0uint_lnot<usintknd> = g0uint_lnot_usint+implement+g0uint_lor<usintknd> = g0uint_lor_usint+implement+g0uint_lxor<usintknd> = g0uint_lxor_usint+implement+g0uint_land<usintknd> = g0uint_land_usint+implement+g0uint_isgtz<usintknd> = g0uint_isgtz_usint+implement+g0uint_iseqz<usintknd> = g0uint_iseqz_usint+implement+g0uint_isneqz<usintknd> = g0uint_isneqz_usint+implement+g0uint_lt<usintknd> = g0uint_lt_usint+implement+g0uint_lte<usintknd> = g0uint_lte_usint+implement+g0uint_gt<usintknd> = g0uint_gt_usint+implement+g0uint_gte<usintknd> = g0uint_gte_usint+implement+g0uint_eq<usintknd> = g0uint_eq_usint+implement+g0uint_neq<usintknd> = g0uint_neq_usint+implement+g0uint_compare<usintknd> = g0uint_compare_usint+implement+g0uint_max<usintknd> = g0uint_max_usint+implement+g0uint_min<usintknd> = g0uint_min_usint+//+implement+fprint_val<usint> (out, x) = fprint_usint (out, x)+//+(* ****** ****** *)++(* end of [integer_short.dats] *)

@@ -0,0 +1,335 @@+(***********************************************************************)+(*                                                                     *)+(*                         Applied Type System                         *)+(*                                                                     *)+(***********************************************************************)++(*+** ATS/Postiats - Unleashing the Potential of Types!+** Copyright (C) 2010-2015 Hongwei Xi, ATS Trustful Software, Inc.+** All rights reserved+**+** ATS is free software;  you can  redistribute it and/or modify it under+** the terms of  the GNU GENERAL PUBLIC LICENSE (GPL) as published by the+** Free Software Foundation; either version 3, or (at  your  option)  any+** later version.+**+** ATS is distributed in the hope that it will be useful, but WITHOUT ANY+** WARRANTY; without  even  the  implied  warranty  of MERCHANTABILITY or+** FITNESS FOR A PARTICULAR PURPOSE.  See the  GNU General Public License+** for more details.+**+** You  should  have  received  a  copy of the GNU General Public License+** along  with  ATS;  see the  file COPYING.  If not, please write to the+** Free Software Foundation,  51 Franklin Street, Fifth Floor, Boston, MA+** 02110-1301, USA.+*)++(* ****** ****** *)++(* Author: Hongwei Xi *)+(* Authoremail: gmhwxiATgmailDOTcom *)+(* Start time: May, 2012 *)++(* ****** ****** *)++(*+** Source:+** $PATSHOME/prelude/DATS/CODEGEN/integer_size.atxt+** Time of generation: Thu Jan 11 11:00:12 2018+*)++(* ****** ****** *)++#define+ATS_DYNLOADFLAG 0 // no dynloading++(* ****** ****** *)+//+staload UN = "prelude/SATS/unsafe.sats"+//+(* ****** ****** *)+//+implement+g0int2uint<intknd,sizeknd> = g0int2uint_int_size+implement+g1int2uint<intknd,sizeknd> = g1int2uint_int_size+//+implement+g0uint2uint<uintknd,sizeknd> = g0uint2uint_uint_size+implement+g1uint2uint<uintknd,sizeknd> = g1uint2uint_uint_size+//+(* ****** ****** *)+//+implement+g0int2int<intknd,ssizeknd> = g0int2int_int_ssize+implement+g1int2int<intknd,ssizeknd> = g1int2int_int_ssize+//+implement+g0uint2int<uintknd,ssizeknd> = g0uint2int_uint_ssize+implement+g1uint2int<uintknd,ssizeknd> = g1uint2int_uint_ssize+//+(* ****** ****** *)+//+implement+g0uint2int<sizeknd,intknd> = g0uint2int_size_int+implement+g1uint2int<sizeknd,intknd> = g1uint2int_size_int+//+implement+g0uint2uint<sizeknd,uintknd> = g0uint2uint_size_uint+implement+g1uint2uint<sizeknd,uintknd> = g1uint2uint_size_uint+//+implement+g0uint2uint<sizeknd,sizeknd> = g0uint2uint_size_size+implement+g1uint2uint<sizeknd,sizeknd> = g1uint2uint_size_size+//+(* ****** ****** *)+//+implement+g0int2int<ssizeknd,intknd> = g0int2int_ssize_int+implement+g1int2int<ssizeknd,intknd> = g1int2int_ssize_int+//+implement+g0int2uint<ssizeknd,uintknd> = g0int2uint_ssize_uint+implement+g1int2uint<ssizeknd,uintknd> = g1int2uint_ssize_uint+//+implement+g0int2int<ssizeknd,ssizeknd> = g0int2int_ssize_ssize+implement+g1int2int<ssizeknd,ssizeknd> = g1int2int_ssize_ssize+//+(* ****** ****** *)+//+implement+g0uint2int<sizeknd,ssizeknd> = g0uint2int_size_ssize+implement+g1uint2int<sizeknd,ssizeknd> = g1uint2int_size_ssize+//+implement+g0int2uint<ssizeknd,sizeknd> = g0int2uint_ssize_size+implement+g1int2uint<ssizeknd,sizeknd> = g1int2uint_ssize_size+//+(* ****** ****** *)+//+implement+g0uint_succ<sizeknd> = g0uint_succ_size+implement+g0uint_pred<sizeknd> = g0uint_pred_size+implement+g0uint_half<sizeknd> = g0uint_half_size+implement+g0uint_add<sizeknd> = g0uint_add_size+implement+g0uint_sub<sizeknd> = g0uint_sub_size+implement+g0uint_mul<sizeknd> = g0uint_mul_size+implement+g0uint_div<sizeknd> = g0uint_div_size+implement+g0uint_mod<sizeknd> = g0uint_mod_size+implement+g0uint_lsl<sizeknd> = g0uint_lsl_size+implement+g0uint_lsr<sizeknd> = g0uint_lsr_size+implement+g0uint_lnot<sizeknd> = g0uint_lnot_size+implement+g0uint_lor<sizeknd> = g0uint_lor_size+implement+g0uint_lxor<sizeknd> = g0uint_lxor_size+implement+g0uint_land<sizeknd> = g0uint_land_size+implement+g0uint_isgtz<sizeknd> = g0uint_isgtz_size+implement+g0uint_iseqz<sizeknd> = g0uint_iseqz_size+implement+g0uint_isneqz<sizeknd> = g0uint_isneqz_size+implement+g0uint_lt<sizeknd> = g0uint_lt_size+implement+g0uint_lte<sizeknd> = g0uint_lte_size+implement+g0uint_gt<sizeknd> = g0uint_gt_size+implement+g0uint_gte<sizeknd> = g0uint_gte_size+implement+g0uint_eq<sizeknd> = g0uint_eq_size+implement+g0uint_neq<sizeknd> = g0uint_neq_size+implement+g0uint_compare<sizeknd> = g0uint_compare_size+implement+g0uint_max<sizeknd> = g0uint_max_size+implement+g0uint_min<sizeknd> = g0uint_min_size+//+implement+fprint_val<size_t> (out, x) = fprint_size (out, x)+//+implement+g1uint_succ<sizeknd> = g1uint_succ_size+implement+g1uint_pred<sizeknd> = g1uint_pred_size+implement+g1uint_half<sizeknd> = g1uint_half_size+implement+g1uint_add<sizeknd> = g1uint_add_size+implement+g1uint_sub<sizeknd> = g1uint_sub_size+implement+g1uint_mul<sizeknd> = g1uint_mul_size+implement+g1uint_div<sizeknd> = g1uint_div_size+implement+g1uint_mod<sizeknd> = g1uint_mod_size+implement+g1uint_isgtz<sizeknd> = g1uint_isgtz_size+implement+g1uint_iseqz<sizeknd> = g1uint_iseqz_size+implement+g1uint_isneqz<sizeknd> = g1uint_isneqz_size+implement+g1uint_lt<sizeknd> = g1uint_lt_size+implement+g1uint_lte<sizeknd> = g1uint_lte_size+implement+g1uint_gt<sizeknd> = g1uint_gt_size+implement+g1uint_gte<sizeknd> = g1uint_gte_size+implement+g1uint_eq<sizeknd> = g1uint_eq_size+implement+g1uint_neq<sizeknd> = g1uint_neq_size+implement+g1uint_compare<sizeknd> = g1uint_compare_size+implement+g1uint_max<sizeknd> = g1uint_max_size+implement+g1uint_min<sizeknd> = g1uint_min_size++//+(* ****** ****** *)+//+implement+g0int_neg<ssizeknd> = g0int_neg_ssize+implement+g0int_abs<ssizeknd> = g0int_abs_ssize+implement+g0int_succ<ssizeknd> = g0int_succ_ssize+implement+g0int_pred<ssizeknd> = g0int_pred_ssize+implement+g0int_half<ssizeknd> = g0int_half_ssize+implement+g0int_add<ssizeknd> = g0int_add_ssize+implement+g0int_sub<ssizeknd> = g0int_sub_ssize+implement+g0int_mul<ssizeknd> = g0int_mul_ssize+implement+g0int_div<ssizeknd> = g0int_div_ssize+implement+g0int_mod<ssizeknd> = g0int_mod_ssize+implement+g0int_asl<ssizeknd> = g0int_asl_ssize+implement+g0int_asr<ssizeknd> = g0int_asr_ssize+implement+g0int_isltz<ssizeknd> = g0int_isltz_ssize+implement+g0int_isltez<ssizeknd> = g0int_isltez_ssize+implement+g0int_isgtz<ssizeknd> = g0int_isgtz_ssize+implement+g0int_isgtez<ssizeknd> = g0int_isgtez_ssize+implement+g0int_iseqz<ssizeknd> = g0int_iseqz_ssize+implement+g0int_isneqz<ssizeknd> = g0int_isneqz_ssize+implement+g0int_lt<ssizeknd> = g0int_lt_ssize+implement+g0int_lte<ssizeknd> = g0int_lte_ssize+implement+g0int_gt<ssizeknd> = g0int_gt_ssize+implement+g0int_gte<ssizeknd> = g0int_gte_ssize+implement+g0int_eq<ssizeknd> = g0int_eq_ssize+implement+g0int_neq<ssizeknd> = g0int_neq_ssize+implement+g0int_compare<ssizeknd> = g0int_compare_ssize+implement+g0int_max<ssizeknd> = g0int_max_ssize+implement+g0int_min<ssizeknd> = g0int_min_ssize+//+implement+fprint_val<ssize_t> (out, x) = fprint_ssize (out, x)+//+implement+g1int_neg<ssizeknd> = g1int_neg_ssize+implement+g1int_abs<ssizeknd> = g1int_abs_ssize+implement+g1int_succ<ssizeknd> = g1int_succ_ssize+implement+g1int_pred<ssizeknd> = g1int_pred_ssize+implement+g1int_half<ssizeknd> = g1int_half_ssize+implement+g1int_add<ssizeknd> = g1int_add_ssize+implement+g1int_sub<ssizeknd> = g1int_sub_ssize+implement+g1int_mul<ssizeknd> = g1int_mul_ssize+implement+g1int_div<ssizeknd> = g1int_div_ssize+implement+g1int_nmod<ssizeknd> = g1int_nmod_ssize+implement+g1int_isltz<ssizeknd> = g1int_isltz_ssize+implement+g1int_isltez<ssizeknd> = g1int_isltez_ssize+implement+g1int_isgtz<ssizeknd> = g1int_isgtz_ssize+implement+g1int_isgtez<ssizeknd> = g1int_isgtez_ssize+implement+g1int_iseqz<ssizeknd> = g1int_iseqz_ssize+implement+g1int_isneqz<ssizeknd> = g1int_isneqz_ssize+implement+g1int_lt<ssizeknd> = g1int_lt_ssize+implement+g1int_lte<ssizeknd> = g1int_lte_ssize+implement+g1int_gt<ssizeknd> = g1int_gt_ssize+implement+g1int_gte<ssizeknd> = g1int_gte_ssize+implement+g1int_eq<ssizeknd> = g1int_eq_ssize+implement+g1int_neq<ssizeknd> = g1int_neq_ssize+implement+g1int_compare<ssizeknd> = g1int_compare_ssize+implement+g1int_max<ssizeknd> = g1int_max_ssize+implement+g1int_min<ssizeknd> = g1int_min_ssize++//+(* ****** ****** *)++(* end of [integer_size.dats] *)