diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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: 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.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 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 @@ -182,6 +182,8 @@ cloptr1Arrow { Arrow $$ "=" } lincloptr1Arrow { Arrow $$ "=" } lincloref1Arrow { Arrow $$ "=" } + proofLambda { Arrow $$ "=" } + proofLinearLambda { Arrow $$ "=" } 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 } 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 @@ -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) diff --git a/src/Language/ATS/Rewrite.hs b/src/Language/ATS/Rewrite.hs --- a/src/Language/ATS/Rewrite.hs +++ b/src/Language/ATS/Rewrite.hs @@ -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 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 @@ -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 \ - , 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 \ + , 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 diff --git a/src/Language/ATS/Types/Lens.hs b/src/Language/ATS/Types/Lens.hs --- a/src/Language/ATS/Types/Lens.hs +++ b/src/Language/ATS/Types/Lens.hs @@ -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 diff --git a/test/data/concurrency.out b/test/data/concurrency.out --- a/test/data/concurrency.out +++ b/test/data/concurrency.out @@ -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(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(chan, xs) prval prf = $UN.castview0{locked_v(l1)}(xs) val () = mutex_unlock(prf | mutex) } diff --git a/test/data/fastcount.out b/test/data/fastcount.out --- a/test/data/fastcount.out +++ b/test/data/fastcount.out @@ -52,14 +52,14 @@ let prval (pf21, pf22) = array_v_uncons(pf2) var res = wclbuf(pf22 | ptr_succ(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 diff --git a/test/data/levenshtein2.out b/test/data/levenshtein2.out --- a/test/data/levenshtein2.out +++ b/test/data/levenshtein2.out @@ -51,7 +51,7 @@ val () = p := ptr1_succ(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) diff --git a/test/data/prf_sqrt2.dats b/test/data/prf_sqrt2.dats --- a/test/data/prf_sqrt2.dats +++ b/test/data/prf_sqrt2.dats @@ -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 diff --git a/test/data/prf_sqrt2.out b/test/data/prf_sqrt2.out --- a/test/data/prf_sqrt2.out +++ b/test/data/prf_sqrt2.out @@ -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 } .. () : [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 diff --git a/test/data/recursion.dats b/test/data/recursion.dats new file mode 100644 --- /dev/null +++ b/test/data/recursion.dats @@ -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 - C, X : BASE_FUNCTOR_PROP(A, B)) : BASE_FUNCTOR_PROP(A, C) + +propdef ALGEBRA (A : prop, B : prop) = BASE_FUNCTOR_PROP(A, B) - 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} .. (F : ALGEBRA(A, B), A : FUNCTOR_PROP(A, n)) : B = + sif n == 0 then + F(LISTF_PROP_NIL) + else + F(MAP(lam A0 = 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) diff --git a/test/data/recursion.out b/test/data/recursion.out new file mode 100644 --- /dev/null +++ b/test/data/recursion.out @@ -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 - C + , X : BASE_FUNCTOR_PROP(A, B) + ) : BASE_FUNCTOR_PROP(A, C) + +propdef ALGEBRA (A : prop, B : prop) = BASE_FUNCTOR_PROP(A, B) - 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} .. ( F : ALGEBRA(A, B) + , A : FUNCTOR_PROP(A, n) + ) : B = + sif n == 0 then + F(LISTF_PROP_NIL) + else + F(MAP(lam A0 = 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) diff --git a/test/data/stdlib/DATS/bool.dats b/test/data/stdlib/DATS/bool.dats new file mode 100644 --- /dev/null +++ b/test/data/stdlib/DATS/bool.dats @@ -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 = fprint_bool + +(* ****** ****** *) + +(* end of [bool.dats] *) diff --git a/test/data/stdlib/DATS/integer_fixed.dats b/test/data/stdlib/DATS/integer_fixed.dats new file mode 100644 --- /dev/null +++ b/test/data/stdlib/DATS/integer_fixed.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 = g0int2int_int8_int +implement +g0int2int = g0int2int_int16_int +implement +g0int2int = g0int2int_int32_int +implement +g0int2int = g0int2int_int64_int +// +(* ****** ****** *) +// +implement +g0int2uint = g0int2uint_int8_uint +implement +g0int2uint = g0int2uint_int16_uint +implement +g0int2uint = g0int2uint_int32_uint +implement +g0int2uint = g0int2uint_int64_uint +// +implement +g0uint2int = g0uint2int_uint8_int +implement +g0uint2int = g0uint2int_uint16_int +implement +g0uint2int = g0uint2int_uint32_int +implement +g0uint2int = g0uint2int_uint64_int +// +implement +g0uint2uint = g0uint2uint_uint8_uint +implement +g0uint2uint = g0uint2uint_uint16_uint +implement +g0uint2uint = g0uint2uint_uint32_uint +implement +g0uint2uint = g0uint2uint_uint64_uint +// +(* ****** ****** *) +// +implement +g0int_neg = g0int_neg_int8 +implement +g0int_abs = g0int_abs_int8 +implement +g0int_succ = g0int_succ_int8 +implement +g0int_pred = g0int_pred_int8 +implement +g0int_half = g0int_half_int8 +implement +g0int_add = g0int_add_int8 +implement +g0int_sub = g0int_sub_int8 +implement +g0int_mul = g0int_mul_int8 +implement +g0int_div = g0int_div_int8 +implement +g0int_mod = g0int_mod_int8 +implement +g0int_asl = g0int_asl_int8 +implement +g0int_asr = g0int_asr_int8 +implement +g0int_isltz = g0int_isltz_int8 +implement +g0int_isltez = g0int_isltez_int8 +implement +g0int_isgtz = g0int_isgtz_int8 +implement +g0int_isgtez = g0int_isgtez_int8 +implement +g0int_iseqz = g0int_iseqz_int8 +implement +g0int_isneqz = g0int_isneqz_int8 +implement +g0int_lt = g0int_lt_int8 +implement +g0int_lte = g0int_lte_int8 +implement +g0int_gt = g0int_gt_int8 +implement +g0int_gte = g0int_gte_int8 +implement +g0int_eq = g0int_eq_int8 +implement +g0int_neq = g0int_neq_int8 +implement +g0int_compare = g0int_compare_int8 +implement +g0int_max = g0int_max_int8 +implement +g0int_min = g0int_min_int8 +// +implement +fprint_val (out, x) = fprint_int8 (out, x) +// +implement +g0int_neg = g0int_neg_int16 +implement +g0int_abs = g0int_abs_int16 +implement +g0int_succ = g0int_succ_int16 +implement +g0int_pred = g0int_pred_int16 +implement +g0int_half = g0int_half_int16 +implement +g0int_add = g0int_add_int16 +implement +g0int_sub = g0int_sub_int16 +implement +g0int_mul = g0int_mul_int16 +implement +g0int_div = g0int_div_int16 +implement +g0int_mod = g0int_mod_int16 +implement +g0int_asl = g0int_asl_int16 +implement +g0int_asr = g0int_asr_int16 +implement +g0int_isltz = g0int_isltz_int16 +implement +g0int_isltez = g0int_isltez_int16 +implement +g0int_isgtz = g0int_isgtz_int16 +implement +g0int_isgtez = g0int_isgtez_int16 +implement +g0int_iseqz = g0int_iseqz_int16 +implement +g0int_isneqz = g0int_isneqz_int16 +implement +g0int_lt = g0int_lt_int16 +implement +g0int_lte = g0int_lte_int16 +implement +g0int_gt = g0int_gt_int16 +implement +g0int_gte = g0int_gte_int16 +implement +g0int_eq = g0int_eq_int16 +implement +g0int_neq = g0int_neq_int16 +implement +g0int_compare = g0int_compare_int16 +implement +g0int_max = g0int_max_int16 +implement +g0int_min = g0int_min_int16 +// +implement +fprint_val (out, x) = fprint_int16 (out, x) +// +implement +g0int_neg = g0int_neg_int32 +implement +g0int_abs = g0int_abs_int32 +implement +g0int_succ = g0int_succ_int32 +implement +g0int_pred = g0int_pred_int32 +implement +g0int_half = g0int_half_int32 +implement +g0int_add = g0int_add_int32 +implement +g0int_sub = g0int_sub_int32 +implement +g0int_mul = g0int_mul_int32 +implement +g0int_div = g0int_div_int32 +implement +g0int_mod = g0int_mod_int32 +implement +g0int_asl = g0int_asl_int32 +implement +g0int_asr = g0int_asr_int32 +implement +g0int_isltz = g0int_isltz_int32 +implement +g0int_isltez = g0int_isltez_int32 +implement +g0int_isgtz = g0int_isgtz_int32 +implement +g0int_isgtez = g0int_isgtez_int32 +implement +g0int_iseqz = g0int_iseqz_int32 +implement +g0int_isneqz = g0int_isneqz_int32 +implement +g0int_lt = g0int_lt_int32 +implement +g0int_lte = g0int_lte_int32 +implement +g0int_gt = g0int_gt_int32 +implement +g0int_gte = g0int_gte_int32 +implement +g0int_eq = g0int_eq_int32 +implement +g0int_neq = g0int_neq_int32 +implement +g0int_compare = g0int_compare_int32 +implement +g0int_max = g0int_max_int32 +implement +g0int_min = g0int_min_int32 +// +implement +fprint_val (out, x) = fprint_int32 (out, x) +// +implement +g0int_neg = g0int_neg_int64 +implement +g0int_abs = g0int_abs_int64 +implement +g0int_succ = g0int_succ_int64 +implement +g0int_pred = g0int_pred_int64 +implement +g0int_half = g0int_half_int64 +implement +g0int_add = g0int_add_int64 +implement +g0int_sub = g0int_sub_int64 +implement +g0int_mul = g0int_mul_int64 +implement +g0int_div = g0int_div_int64 +implement +g0int_mod = g0int_mod_int64 +implement +g0int_asl = g0int_asl_int64 +implement +g0int_asr = g0int_asr_int64 +implement +g0int_isltz = g0int_isltz_int64 +implement +g0int_isltez = g0int_isltez_int64 +implement +g0int_isgtz = g0int_isgtz_int64 +implement +g0int_isgtez = g0int_isgtez_int64 +implement +g0int_iseqz = g0int_iseqz_int64 +implement +g0int_isneqz = g0int_isneqz_int64 +implement +g0int_lt = g0int_lt_int64 +implement +g0int_lte = g0int_lte_int64 +implement +g0int_gt = g0int_gt_int64 +implement +g0int_gte = g0int_gte_int64 +implement +g0int_eq = g0int_eq_int64 +implement +g0int_neq = g0int_neq_int64 +implement +g0int_compare = g0int_compare_int64 +implement +g0int_max = g0int_max_int64 +implement +g0int_min = g0int_min_int64 +// +implement +fprint_val (out, x) = fprint_int64 (out, x) +// +(* ****** ****** *) +// +implement +g0uint_succ = g0uint_succ_uint8 +implement +g0uint_pred = g0uint_pred_uint8 +implement +g0uint_half = g0uint_half_uint8 +implement +g0uint_add = g0uint_add_uint8 +implement +g0uint_sub = g0uint_sub_uint8 +implement +g0uint_mul = g0uint_mul_uint8 +implement +g0uint_div = g0uint_div_uint8 +implement +g0uint_mod = g0uint_mod_uint8 +implement +g0uint_lsl = g0uint_lsl_uint8 +implement +g0uint_lsr = g0uint_lsr_uint8 +implement +g0uint_lnot = g0uint_lnot_uint8 +implement +g0uint_lor = g0uint_lor_uint8 +implement +g0uint_lxor = g0uint_lxor_uint8 +implement +g0uint_land = g0uint_land_uint8 +implement +g0uint_isgtz = g0uint_isgtz_uint8 +implement +g0uint_iseqz = g0uint_iseqz_uint8 +implement +g0uint_isneqz = g0uint_isneqz_uint8 +implement +g0uint_lt = g0uint_lt_uint8 +implement +g0uint_lte = g0uint_lte_uint8 +implement +g0uint_gt = g0uint_gt_uint8 +implement +g0uint_gte = g0uint_gte_uint8 +implement +g0uint_eq = g0uint_eq_uint8 +implement +g0uint_neq = g0uint_neq_uint8 +implement +g0uint_compare = g0uint_compare_uint8 +implement +g0uint_max = g0uint_max_uint8 +implement +g0uint_min = g0uint_min_uint8 +// +implement +fprint_val (out, x) = fprint_uint8 (out, x) +// +implement +g0uint_succ = g0uint_succ_uint16 +implement +g0uint_pred = g0uint_pred_uint16 +implement +g0uint_half = g0uint_half_uint16 +implement +g0uint_add = g0uint_add_uint16 +implement +g0uint_sub = g0uint_sub_uint16 +implement +g0uint_mul = g0uint_mul_uint16 +implement +g0uint_div = g0uint_div_uint16 +implement +g0uint_mod = g0uint_mod_uint16 +implement +g0uint_lsl = g0uint_lsl_uint16 +implement +g0uint_lsr = g0uint_lsr_uint16 +implement +g0uint_lnot = g0uint_lnot_uint16 +implement +g0uint_lor = g0uint_lor_uint16 +implement +g0uint_lxor = g0uint_lxor_uint16 +implement +g0uint_land = g0uint_land_uint16 +implement +g0uint_isgtz = g0uint_isgtz_uint16 +implement +g0uint_iseqz = g0uint_iseqz_uint16 +implement +g0uint_isneqz = g0uint_isneqz_uint16 +implement +g0uint_lt = g0uint_lt_uint16 +implement +g0uint_lte = g0uint_lte_uint16 +implement +g0uint_gt = g0uint_gt_uint16 +implement +g0uint_gte = g0uint_gte_uint16 +implement +g0uint_eq = g0uint_eq_uint16 +implement +g0uint_neq = g0uint_neq_uint16 +implement +g0uint_compare = g0uint_compare_uint16 +implement +g0uint_max = g0uint_max_uint16 +implement +g0uint_min = g0uint_min_uint16 +// +implement +fprint_val (out, x) = fprint_uint16 (out, x) +// +implement +g0uint_succ = g0uint_succ_uint32 +implement +g0uint_pred = g0uint_pred_uint32 +implement +g0uint_half = g0uint_half_uint32 +implement +g0uint_add = g0uint_add_uint32 +implement +g0uint_sub = g0uint_sub_uint32 +implement +g0uint_mul = g0uint_mul_uint32 +implement +g0uint_div = g0uint_div_uint32 +implement +g0uint_mod = g0uint_mod_uint32 +implement +g0uint_lsl = g0uint_lsl_uint32 +implement +g0uint_lsr = g0uint_lsr_uint32 +implement +g0uint_lnot = g0uint_lnot_uint32 +implement +g0uint_lor = g0uint_lor_uint32 +implement +g0uint_lxor = g0uint_lxor_uint32 +implement +g0uint_land = g0uint_land_uint32 +implement +g0uint_isgtz = g0uint_isgtz_uint32 +implement +g0uint_iseqz = g0uint_iseqz_uint32 +implement +g0uint_isneqz = g0uint_isneqz_uint32 +implement +g0uint_lt = g0uint_lt_uint32 +implement +g0uint_lte = g0uint_lte_uint32 +implement +g0uint_gt = g0uint_gt_uint32 +implement +g0uint_gte = g0uint_gte_uint32 +implement +g0uint_eq = g0uint_eq_uint32 +implement +g0uint_neq = g0uint_neq_uint32 +implement +g0uint_compare = g0uint_compare_uint32 +implement +g0uint_max = g0uint_max_uint32 +implement +g0uint_min = g0uint_min_uint32 +// +implement +fprint_val (out, x) = fprint_uint32 (out, x) +// +implement +g0uint_succ = g0uint_succ_uint64 +implement +g0uint_pred = g0uint_pred_uint64 +implement +g0uint_half = g0uint_half_uint64 +implement +g0uint_add = g0uint_add_uint64 +implement +g0uint_sub = g0uint_sub_uint64 +implement +g0uint_mul = g0uint_mul_uint64 +implement +g0uint_div = g0uint_div_uint64 +implement +g0uint_mod = g0uint_mod_uint64 +implement +g0uint_lsl = g0uint_lsl_uint64 +implement +g0uint_lsr = g0uint_lsr_uint64 +implement +g0uint_lnot = g0uint_lnot_uint64 +implement +g0uint_lor = g0uint_lor_uint64 +implement +g0uint_lxor = g0uint_lxor_uint64 +implement +g0uint_land = g0uint_land_uint64 +implement +g0uint_isgtz = g0uint_isgtz_uint64 +implement +g0uint_iseqz = g0uint_iseqz_uint64 +implement +g0uint_isneqz = g0uint_isneqz_uint64 +implement +g0uint_lt = g0uint_lt_uint64 +implement +g0uint_lte = g0uint_lte_uint64 +implement +g0uint_gt = g0uint_gt_uint64 +implement +g0uint_gte = g0uint_gte_uint64 +implement +g0uint_eq = g0uint_eq_uint64 +implement +g0uint_neq = g0uint_neq_uint64 +implement +g0uint_compare = g0uint_compare_uint64 +implement +g0uint_max = g0uint_max_uint64 +implement +g0uint_min = g0uint_min_uint64 +// +implement +fprint_val (out, x) = fprint_uint64 (out, x) +// +(* ****** ****** *) + +(* end of [integer_fixed.dats] *) diff --git a/test/data/stdlib/DATS/integer_long.dats b/test/data/stdlib/DATS/integer_long.dats new file mode 100644 --- /dev/null +++ b/test/data/stdlib/DATS/integer_long.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 = g0int2int_int_lint +implement +g1int2int = g1int2int_int_lint +// +implement +g0uint2int = g0uint2int_uint_lint +implement +g1uint2int = g1uint2int_uint_lint +// +(* ****** ****** *) +// +implement +g0int2uint = g0int2uint_int_ulint +implement +g1int2uint = g1int2uint_int_ulint +// +implement +g0uint2uint = g0uint2uint_uint_ulint +implement +g1uint2uint = g1uint2uint_uint_ulint +// +(* ****** ****** *) +// +implement +g0int2int = g0int2int_int_llint +implement +g1int2int = g1int2int_int_llint +// +implement +g0uint2int = g0uint2int_uint_llint +implement +g1uint2int = g1uint2int_uint_llint +// +(* ****** ****** *) +// +implement +g0int2uint = g0int2uint_int_ullint +implement +g1int2uint = g1int2uint_int_ullint +// +implement +g0uint2uint = g0uint2uint_uint_ullint +implement +g1uint2uint = g1uint2uint_uint_ullint +// +(* ****** ****** *) +// +implement +g0int2int = g0int2int_lint_lint +implement +g0int2int = g0int2int_lint_llint +// +implement +g0int2uint = g0int2uint_lint_ulint +implement +g0int2uint = g0int2uint_lint_ullint +// +(* ****** ****** *) +// +implement +g0uint2int = g0uint2int_ulint_lint +implement +g0uint2int = g0uint2int_ulint_llint +// +implement +g0uint2uint = g0uint2uint_ulint_ulint +implement +g0uint2uint = g0uint2uint_ulint_ullint +// +(* ****** ****** *) +// +implement +g0int2int = g0int2int_llint_llint +// +implement +g0int2uint = g0int2uint_llint_ullint +// +(* ****** ****** *) +// +implement +g0uint2int = g0uint2int_ullint_llint +// +implement +g0uint2uint = g0uint2uint_ullint_ullint +// +(* ****** ****** *) +// +implement g0int2string = g0int2string_lint +implement g0int2string = g0int2string_llint +// +implement g0string2int = g0string2int_lint +implement g0string2int = g0string2int_llint +implement g0string2uint = g0string2uint_ulint +implement g0string2uint = g0string2uint_ullint +// +(* ****** ****** *) +// +implement +g0int_neg = g0int_neg_lint +implement +g0int_abs = g0int_abs_lint +implement +g0int_succ = g0int_succ_lint +implement +g0int_pred = g0int_pred_lint +implement +g0int_half = g0int_half_lint +implement +g0int_add = g0int_add_lint +implement +g0int_sub = g0int_sub_lint +implement +g0int_mul = g0int_mul_lint +implement +g0int_div = g0int_div_lint +implement +g0int_mod = g0int_mod_lint +implement +g0int_asl = g0int_asl_lint +implement +g0int_asr = g0int_asr_lint +implement +g0int_isltz = g0int_isltz_lint +implement +g0int_isltez = g0int_isltez_lint +implement +g0int_isgtz = g0int_isgtz_lint +implement +g0int_isgtez = g0int_isgtez_lint +implement +g0int_iseqz = g0int_iseqz_lint +implement +g0int_isneqz = g0int_isneqz_lint +implement +g0int_lt = g0int_lt_lint +implement +g0int_lte = g0int_lte_lint +implement +g0int_gt = g0int_gt_lint +implement +g0int_gte = g0int_gte_lint +implement +g0int_eq = g0int_eq_lint +implement +g0int_neq = g0int_neq_lint +implement +g0int_compare = g0int_compare_lint +implement +g0int_max = g0int_max_lint +implement +g0int_min = g0int_min_lint +// +implement +fprint_val (out, x) = fprint_lint (out, x)// +implement +g1int_neg = g1int_neg_lint +implement +g1int_abs = g1int_abs_lint +implement +g1int_succ = g1int_succ_lint +implement +g1int_pred = g1int_pred_lint +implement +g1int_half = g1int_half_lint +implement +g1int_add = g1int_add_lint +implement +g1int_sub = g1int_sub_lint +implement +g1int_mul = g1int_mul_lint +implement +g1int_div = g1int_div_lint +implement +g1int_nmod = g1int_nmod_lint +implement +g1int_isltz = g1int_isltz_lint +implement +g1int_isltez = g1int_isltez_lint +implement +g1int_isgtz = g1int_isgtz_lint +implement +g1int_isgtez = g1int_isgtez_lint +implement +g1int_iseqz = g1int_iseqz_lint +implement +g1int_isneqz = g1int_isneqz_lint +implement +g1int_lt = g1int_lt_lint +implement +g1int_lte = g1int_lte_lint +implement +g1int_gt = g1int_gt_lint +implement +g1int_gte = g1int_gte_lint +implement +g1int_eq = g1int_eq_lint +implement +g1int_neq = g1int_neq_lint +implement +g1int_compare = g1int_compare_lint +implement +g1int_max = g1int_max_lint +implement +g1int_min = g1int_min_lint +// +(* ****** ****** *) +// +implement +g0int_neg = g0int_neg_llint +implement +g0int_abs = g0int_abs_llint +implement +g0int_succ = g0int_succ_llint +implement +g0int_pred = g0int_pred_llint +implement +g0int_half = g0int_half_llint +implement +g0int_add = g0int_add_llint +implement +g0int_sub = g0int_sub_llint +implement +g0int_mul = g0int_mul_llint +implement +g0int_div = g0int_div_llint +implement +g0int_mod = g0int_mod_llint +implement +g0int_asl = g0int_asl_llint +implement +g0int_asr = g0int_asr_llint +implement +g0int_isltz = g0int_isltz_llint +implement +g0int_isltez = g0int_isltez_llint +implement +g0int_isgtz = g0int_isgtz_llint +implement +g0int_isgtez = g0int_isgtez_llint +implement +g0int_iseqz = g0int_iseqz_llint +implement +g0int_isneqz = g0int_isneqz_llint +implement +g0int_lt = g0int_lt_llint +implement +g0int_lte = g0int_lte_llint +implement +g0int_gt = g0int_gt_llint +implement +g0int_gte = g0int_gte_llint +implement +g0int_eq = g0int_eq_llint +implement +g0int_neq = g0int_neq_llint +implement +g0int_compare = g0int_compare_llint +implement +g0int_max = g0int_max_llint +implement +g0int_min = g0int_min_llint +// +implement +fprint_val (out, x) = fprint_llint (out, x)// +implement +g1int_neg = g1int_neg_llint +implement +g1int_abs = g1int_abs_llint +implement +g1int_succ = g1int_succ_llint +implement +g1int_pred = g1int_pred_llint +implement +g1int_half = g1int_half_llint +implement +g1int_add = g1int_add_llint +implement +g1int_sub = g1int_sub_llint +implement +g1int_mul = g1int_mul_llint +implement +g1int_div = g1int_div_llint +implement +g1int_nmod = g1int_nmod_llint +implement +g1int_isltz = g1int_isltz_llint +implement +g1int_isltez = g1int_isltez_llint +implement +g1int_isgtz = g1int_isgtz_llint +implement +g1int_isgtez = g1int_isgtez_llint +implement +g1int_iseqz = g1int_iseqz_llint +implement +g1int_isneqz = g1int_isneqz_llint +implement +g1int_lt = g1int_lt_llint +implement +g1int_lte = g1int_lte_llint +implement +g1int_gt = g1int_gt_llint +implement +g1int_gte = g1int_gte_llint +implement +g1int_eq = g1int_eq_llint +implement +g1int_neq = g1int_neq_llint +implement +g1int_compare = g1int_compare_llint +implement +g1int_max = g1int_max_llint +implement +g1int_min = g1int_min_llint +// +(* ****** ****** *) +// +implement +g0uint_succ = g0uint_succ_ulint +implement +g0uint_pred = g0uint_pred_ulint +implement +g0uint_half = g0uint_half_ulint +implement +g0uint_add = g0uint_add_ulint +implement +g0uint_sub = g0uint_sub_ulint +implement +g0uint_mul = g0uint_mul_ulint +implement +g0uint_div = g0uint_div_ulint +implement +g0uint_mod = g0uint_mod_ulint +implement +g0uint_lsl = g0uint_lsl_ulint +implement +g0uint_lsr = g0uint_lsr_ulint +implement +g0uint_lnot = g0uint_lnot_ulint +implement +g0uint_lor = g0uint_lor_ulint +implement +g0uint_lxor = g0uint_lxor_ulint +implement +g0uint_land = g0uint_land_ulint +implement +g0uint_isgtz = g0uint_isgtz_ulint +implement +g0uint_iseqz = g0uint_iseqz_ulint +implement +g0uint_isneqz = g0uint_isneqz_ulint +implement +g0uint_lt = g0uint_lt_ulint +implement +g0uint_lte = g0uint_lte_ulint +implement +g0uint_gt = g0uint_gt_ulint +implement +g0uint_gte = g0uint_gte_ulint +implement +g0uint_eq = g0uint_eq_ulint +implement +g0uint_neq = g0uint_neq_ulint +implement +g0uint_compare = g0uint_compare_ulint +implement +g0uint_max = g0uint_max_ulint +implement +g0uint_min = g0uint_min_ulint +// +implement +fprint_val (out, x) = fprint_ulint (out, x)// +implement +g1uint_succ = g1uint_succ_ulint +implement +g1uint_pred = g1uint_pred_ulint +implement +g1uint_half = g1uint_half_ulint +implement +g1uint_add = g1uint_add_ulint +implement +g1uint_sub = g1uint_sub_ulint +implement +g1uint_mul = g1uint_mul_ulint +implement +g1uint_div = g1uint_div_ulint +implement +g1uint_mod = g1uint_mod_ulint +implement +g1uint_isgtz = g1uint_isgtz_ulint +implement +g1uint_iseqz = g1uint_iseqz_ulint +implement +g1uint_isneqz = g1uint_isneqz_ulint +implement +g1uint_lt = g1uint_lt_ulint +implement +g1uint_lte = g1uint_lte_ulint +implement +g1uint_gt = g1uint_gt_ulint +implement +g1uint_gte = g1uint_gte_ulint +implement +g1uint_eq = g1uint_eq_ulint +implement +g1uint_neq = g1uint_neq_ulint +implement +g1uint_compare = g1uint_compare_ulint +implement +g1uint_max = g1uint_max_ulint +implement +g1uint_min = g1uint_min_ulint +// +(* ****** ****** *) +// +implement +g0uint_succ = g0uint_succ_ullint +implement +g0uint_pred = g0uint_pred_ullint +implement +g0uint_half = g0uint_half_ullint +implement +g0uint_add = g0uint_add_ullint +implement +g0uint_sub = g0uint_sub_ullint +implement +g0uint_mul = g0uint_mul_ullint +implement +g0uint_div = g0uint_div_ullint +implement +g0uint_mod = g0uint_mod_ullint +implement +g0uint_lsl = g0uint_lsl_ullint +implement +g0uint_lsr = g0uint_lsr_ullint +implement +g0uint_lnot = g0uint_lnot_ullint +implement +g0uint_lor = g0uint_lor_ullint +implement +g0uint_lxor = g0uint_lxor_ullint +implement +g0uint_land = g0uint_land_ullint +implement +g0uint_isgtz = g0uint_isgtz_ullint +implement +g0uint_iseqz = g0uint_iseqz_ullint +implement +g0uint_isneqz = g0uint_isneqz_ullint +implement +g0uint_lt = g0uint_lt_ullint +implement +g0uint_lte = g0uint_lte_ullint +implement +g0uint_gt = g0uint_gt_ullint +implement +g0uint_gte = g0uint_gte_ullint +implement +g0uint_eq = g0uint_eq_ullint +implement +g0uint_neq = g0uint_neq_ullint +implement +g0uint_compare = g0uint_compare_ullint +implement +g0uint_max = g0uint_max_ullint +implement +g0uint_min = g0uint_min_ullint +// +implement +fprint_val (out, x) = fprint_ullint (out, x)// +implement +g1uint_succ = g1uint_succ_ullint +implement +g1uint_pred = g1uint_pred_ullint +implement +g1uint_half = g1uint_half_ullint +implement +g1uint_add = g1uint_add_ullint +implement +g1uint_sub = g1uint_sub_ullint +implement +g1uint_mul = g1uint_mul_ullint +implement +g1uint_div = g1uint_div_ullint +implement +g1uint_mod = g1uint_mod_ullint +implement +g1uint_isgtz = g1uint_isgtz_ullint +implement +g1uint_iseqz = g1uint_iseqz_ullint +implement +g1uint_isneqz = g1uint_isneqz_ullint +implement +g1uint_lt = g1uint_lt_ullint +implement +g1uint_lte = g1uint_lte_ullint +implement +g1uint_gt = g1uint_gt_ullint +implement +g1uint_gte = g1uint_gte_ullint +implement +g1uint_eq = g1uint_eq_ullint +implement +g1uint_neq = g1uint_neq_ullint +implement +g1uint_compare = g1uint_compare_ullint +implement +g1uint_max = g1uint_max_ullint +implement +g1uint_min = g1uint_min_ullint +// +(* ****** ****** *) +// +implement +nmod_g1int_int1 + (x, y) = g1i2i(g1int_nmod(x, g1i2i(y))) +implement +nmod_g1int_int1 + (x, y) = g1i2i(g1int_nmod(x, g1i2i(y))) +// +(* ****** ****** *) + +(* end of [integer_long.dats] *) diff --git a/test/data/stdlib/DATS/integer_ptr.dats b/test/data/stdlib/DATS/integer_ptr.dats new file mode 100644 --- /dev/null +++ b/test/data/stdlib/DATS/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_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 = g0int2int_int_intptr +implement +g0int2int = g0int2int_lint_intptr + +(* ****** ****** *) + +implement +g0uint2uint = g0uint2uint_uint_uintptr +implement +g0uint2uint = g0uint2uint_ulint_uintptr + +(* ****** ****** *) +// +implement +g0int_neg = g0int_neg_intptr +implement +g0int_abs = g0int_abs_intptr +implement +g0int_succ = g0int_succ_intptr +implement +g0int_pred = g0int_pred_intptr +implement +g0int_half = g0int_half_intptr +implement +g0int_add = g0int_add_intptr +implement +g0int_sub = g0int_sub_intptr +implement +g0int_mul = g0int_mul_intptr +implement +g0int_div = g0int_div_intptr +implement +g0int_mod = g0int_mod_intptr +implement +g0int_asl = g0int_asl_intptr +implement +g0int_asr = g0int_asr_intptr +implement +g0int_isltz = g0int_isltz_intptr +implement +g0int_isltez = g0int_isltez_intptr +implement +g0int_isgtz = g0int_isgtz_intptr +implement +g0int_isgtez = g0int_isgtez_intptr +implement +g0int_iseqz = g0int_iseqz_intptr +implement +g0int_isneqz = g0int_isneqz_intptr +implement +g0int_lt = g0int_lt_intptr +implement +g0int_lte = g0int_lte_intptr +implement +g0int_gt = g0int_gt_intptr +implement +g0int_gte = g0int_gte_intptr +implement +g0int_eq = g0int_eq_intptr +implement +g0int_neq = g0int_neq_intptr +implement +g0int_compare = g0int_compare_intptr +implement +g0int_max = g0int_max_intptr +implement +g0int_min = g0int_min_intptr +// +implement +fprint_val (out, x) = fprint_intptr (out, x) +// +implement +g0uint_succ = g0uint_succ_uintptr +implement +g0uint_pred = g0uint_pred_uintptr +implement +g0uint_half = g0uint_half_uintptr +implement +g0uint_add = g0uint_add_uintptr +implement +g0uint_sub = g0uint_sub_uintptr +implement +g0uint_mul = g0uint_mul_uintptr +implement +g0uint_div = g0uint_div_uintptr +implement +g0uint_mod = g0uint_mod_uintptr +implement +g0uint_lsl = g0uint_lsl_uintptr +implement +g0uint_lsr = g0uint_lsr_uintptr +implement +g0uint_lnot = g0uint_lnot_uintptr +implement +g0uint_lor = g0uint_lor_uintptr +implement +g0uint_lxor = g0uint_lxor_uintptr +implement +g0uint_land = g0uint_land_uintptr +implement +g0uint_isgtz = g0uint_isgtz_uintptr +implement +g0uint_iseqz = g0uint_iseqz_uintptr +implement +g0uint_isneqz = g0uint_isneqz_uintptr +implement +g0uint_lt = g0uint_lt_uintptr +implement +g0uint_lte = g0uint_lte_uintptr +implement +g0uint_gt = g0uint_gt_uintptr +implement +g0uint_gte = g0uint_gte_uintptr +implement +g0uint_eq = g0uint_eq_uintptr +implement +g0uint_neq = g0uint_neq_uintptr +implement +g0uint_compare = g0uint_compare_uintptr +implement +g0uint_max = g0uint_max_uintptr +implement +g0uint_min = g0uint_min_uintptr +// +implement +fprint_val (out, x) = fprint_uintptr (out, x) +// +(* ****** ****** *) + +(* end of [integer_ptr.dats] *) diff --git a/test/data/stdlib/DATS/integer_short.dats b/test/data/stdlib/DATS/integer_short.dats new file mode 100644 --- /dev/null +++ b/test/data/stdlib/DATS/integer_short.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 = g0int2int_sint_int +implement +g0int2uint = g0int2uint_sint_uint +// +(* ****** ****** *) +// +implement +g0uint2int = g0uint2int_usint_int +implement +g0uint2uint = g0uint2uint_usint_uint +// +(* ****** ****** *) +// +implement +g0int_neg = g0int_neg_sint +implement +g0int_abs = g0int_abs_sint +implement +g0int_succ = g0int_succ_sint +implement +g0int_pred = g0int_pred_sint +implement +g0int_half = g0int_half_sint +implement +g0int_add = g0int_add_sint +implement +g0int_sub = g0int_sub_sint +implement +g0int_mul = g0int_mul_sint +implement +g0int_div = g0int_div_sint +implement +g0int_mod = g0int_mod_sint +implement +g0int_asl = g0int_asl_sint +implement +g0int_asr = g0int_asr_sint +implement +g0int_isltz = g0int_isltz_sint +implement +g0int_isltez = g0int_isltez_sint +implement +g0int_isgtz = g0int_isgtz_sint +implement +g0int_isgtez = g0int_isgtez_sint +implement +g0int_iseqz = g0int_iseqz_sint +implement +g0int_isneqz = g0int_isneqz_sint +implement +g0int_lt = g0int_lt_sint +implement +g0int_lte = g0int_lte_sint +implement +g0int_gt = g0int_gt_sint +implement +g0int_gte = g0int_gte_sint +implement +g0int_eq = g0int_eq_sint +implement +g0int_neq = g0int_neq_sint +implement +g0int_compare = g0int_compare_sint +implement +g0int_max = g0int_max_sint +implement +g0int_min = g0int_min_sint +// +implement +fprint_val (out, x) = fprint_sint (out, x) +// +implement +g0uint_succ = g0uint_succ_usint +implement +g0uint_pred = g0uint_pred_usint +implement +g0uint_half = g0uint_half_usint +implement +g0uint_add = g0uint_add_usint +implement +g0uint_sub = g0uint_sub_usint +implement +g0uint_mul = g0uint_mul_usint +implement +g0uint_div = g0uint_div_usint +implement +g0uint_mod = g0uint_mod_usint +implement +g0uint_lsl = g0uint_lsl_usint +implement +g0uint_lsr = g0uint_lsr_usint +implement +g0uint_lnot = g0uint_lnot_usint +implement +g0uint_lor = g0uint_lor_usint +implement +g0uint_lxor = g0uint_lxor_usint +implement +g0uint_land = g0uint_land_usint +implement +g0uint_isgtz = g0uint_isgtz_usint +implement +g0uint_iseqz = g0uint_iseqz_usint +implement +g0uint_isneqz = g0uint_isneqz_usint +implement +g0uint_lt = g0uint_lt_usint +implement +g0uint_lte = g0uint_lte_usint +implement +g0uint_gt = g0uint_gt_usint +implement +g0uint_gte = g0uint_gte_usint +implement +g0uint_eq = g0uint_eq_usint +implement +g0uint_neq = g0uint_neq_usint +implement +g0uint_compare = g0uint_compare_usint +implement +g0uint_max = g0uint_max_usint +implement +g0uint_min = g0uint_min_usint +// +implement +fprint_val (out, x) = fprint_usint (out, x) +// +(* ****** ****** *) + +(* end of [integer_short.dats] *) diff --git a/test/data/stdlib/DATS/integer_size.dats b/test/data/stdlib/DATS/integer_size.dats new file mode 100644 --- /dev/null +++ b/test/data/stdlib/DATS/integer_size.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 = g0int2uint_int_size +implement +g1int2uint = g1int2uint_int_size +// +implement +g0uint2uint = g0uint2uint_uint_size +implement +g1uint2uint = g1uint2uint_uint_size +// +(* ****** ****** *) +// +implement +g0int2int = g0int2int_int_ssize +implement +g1int2int = g1int2int_int_ssize +// +implement +g0uint2int = g0uint2int_uint_ssize +implement +g1uint2int = g1uint2int_uint_ssize +// +(* ****** ****** *) +// +implement +g0uint2int = g0uint2int_size_int +implement +g1uint2int = g1uint2int_size_int +// +implement +g0uint2uint = g0uint2uint_size_uint +implement +g1uint2uint = g1uint2uint_size_uint +// +implement +g0uint2uint = g0uint2uint_size_size +implement +g1uint2uint = g1uint2uint_size_size +// +(* ****** ****** *) +// +implement +g0int2int = g0int2int_ssize_int +implement +g1int2int = g1int2int_ssize_int +// +implement +g0int2uint = g0int2uint_ssize_uint +implement +g1int2uint = g1int2uint_ssize_uint +// +implement +g0int2int = g0int2int_ssize_ssize +implement +g1int2int = g1int2int_ssize_ssize +// +(* ****** ****** *) +// +implement +g0uint2int = g0uint2int_size_ssize +implement +g1uint2int = g1uint2int_size_ssize +// +implement +g0int2uint = g0int2uint_ssize_size +implement +g1int2uint = g1int2uint_ssize_size +// +(* ****** ****** *) +// +implement +g0uint_succ = g0uint_succ_size +implement +g0uint_pred = g0uint_pred_size +implement +g0uint_half = g0uint_half_size +implement +g0uint_add = g0uint_add_size +implement +g0uint_sub = g0uint_sub_size +implement +g0uint_mul = g0uint_mul_size +implement +g0uint_div = g0uint_div_size +implement +g0uint_mod = g0uint_mod_size +implement +g0uint_lsl = g0uint_lsl_size +implement +g0uint_lsr = g0uint_lsr_size +implement +g0uint_lnot = g0uint_lnot_size +implement +g0uint_lor = g0uint_lor_size +implement +g0uint_lxor = g0uint_lxor_size +implement +g0uint_land = g0uint_land_size +implement +g0uint_isgtz = g0uint_isgtz_size +implement +g0uint_iseqz = g0uint_iseqz_size +implement +g0uint_isneqz = g0uint_isneqz_size +implement +g0uint_lt = g0uint_lt_size +implement +g0uint_lte = g0uint_lte_size +implement +g0uint_gt = g0uint_gt_size +implement +g0uint_gte = g0uint_gte_size +implement +g0uint_eq = g0uint_eq_size +implement +g0uint_neq = g0uint_neq_size +implement +g0uint_compare = g0uint_compare_size +implement +g0uint_max = g0uint_max_size +implement +g0uint_min = g0uint_min_size +// +implement +fprint_val (out, x) = fprint_size (out, x) +// +implement +g1uint_succ = g1uint_succ_size +implement +g1uint_pred = g1uint_pred_size +implement +g1uint_half = g1uint_half_size +implement +g1uint_add = g1uint_add_size +implement +g1uint_sub = g1uint_sub_size +implement +g1uint_mul = g1uint_mul_size +implement +g1uint_div = g1uint_div_size +implement +g1uint_mod = g1uint_mod_size +implement +g1uint_isgtz = g1uint_isgtz_size +implement +g1uint_iseqz = g1uint_iseqz_size +implement +g1uint_isneqz = g1uint_isneqz_size +implement +g1uint_lt = g1uint_lt_size +implement +g1uint_lte = g1uint_lte_size +implement +g1uint_gt = g1uint_gt_size +implement +g1uint_gte = g1uint_gte_size +implement +g1uint_eq = g1uint_eq_size +implement +g1uint_neq = g1uint_neq_size +implement +g1uint_compare = g1uint_compare_size +implement +g1uint_max = g1uint_max_size +implement +g1uint_min = g1uint_min_size + +// +(* ****** ****** *) +// +implement +g0int_neg = g0int_neg_ssize +implement +g0int_abs = g0int_abs_ssize +implement +g0int_succ = g0int_succ_ssize +implement +g0int_pred = g0int_pred_ssize +implement +g0int_half = g0int_half_ssize +implement +g0int_add = g0int_add_ssize +implement +g0int_sub = g0int_sub_ssize +implement +g0int_mul = g0int_mul_ssize +implement +g0int_div = g0int_div_ssize +implement +g0int_mod = g0int_mod_ssize +implement +g0int_asl = g0int_asl_ssize +implement +g0int_asr = g0int_asr_ssize +implement +g0int_isltz = g0int_isltz_ssize +implement +g0int_isltez = g0int_isltez_ssize +implement +g0int_isgtz = g0int_isgtz_ssize +implement +g0int_isgtez = g0int_isgtez_ssize +implement +g0int_iseqz = g0int_iseqz_ssize +implement +g0int_isneqz = g0int_isneqz_ssize +implement +g0int_lt = g0int_lt_ssize +implement +g0int_lte = g0int_lte_ssize +implement +g0int_gt = g0int_gt_ssize +implement +g0int_gte = g0int_gte_ssize +implement +g0int_eq = g0int_eq_ssize +implement +g0int_neq = g0int_neq_ssize +implement +g0int_compare = g0int_compare_ssize +implement +g0int_max = g0int_max_ssize +implement +g0int_min = g0int_min_ssize +// +implement +fprint_val (out, x) = fprint_ssize (out, x) +// +implement +g1int_neg = g1int_neg_ssize +implement +g1int_abs = g1int_abs_ssize +implement +g1int_succ = g1int_succ_ssize +implement +g1int_pred = g1int_pred_ssize +implement +g1int_half = g1int_half_ssize +implement +g1int_add = g1int_add_ssize +implement +g1int_sub = g1int_sub_ssize +implement +g1int_mul = g1int_mul_ssize +implement +g1int_div = g1int_div_ssize +implement +g1int_nmod = g1int_nmod_ssize +implement +g1int_isltz = g1int_isltz_ssize +implement +g1int_isltez = g1int_isltez_ssize +implement +g1int_isgtz = g1int_isgtz_ssize +implement +g1int_isgtez = g1int_isgtez_ssize +implement +g1int_iseqz = g1int_iseqz_ssize +implement +g1int_isneqz = g1int_isneqz_ssize +implement +g1int_lt = g1int_lt_ssize +implement +g1int_lte = g1int_lte_ssize +implement +g1int_gt = g1int_gt_ssize +implement +g1int_gte = g1int_gte_ssize +implement +g1int_eq = g1int_eq_ssize +implement +g1int_neq = g1int_neq_ssize +implement +g1int_compare = g1int_compare_ssize +implement +g1int_max = g1int_max_ssize +implement +g1int_min = g1int_min_ssize + +// +(* ****** ****** *) + +(* end of [integer_size.dats] *)