language-ats 1.7.9.0 → 1.7.10.0
raw patch · 13 files changed
+626/−11 lines, 13 filesPVP ok
version bump matches the API change (PVP)
API changes (from Hackage documentation)
+ Language.ATS: ArrayLit :: a -> Type a -> Maybe (StaticExpression a) -> [Expression a] -> Expression a
+ Language.ATS: LShift :: BinOp a
+ Language.ATS: RShift :: BinOp a
Files
- CHANGELOG.md +6/−0
- language-ats.cabal +1/−1
- src/Language/ATS/Parser.y +6/−1
- src/Language/ATS/PrettyPrint.hs +24/−8
- src/Language/ATS/Rewrite.hs +2/−0
- src/Language/ATS/Types.hs +4/−0
- test/data/array-literal.dats +258/−0
- test/data/array-literal.out +258/−0
- test/data/crc32.dats +27/−0
- test/data/crc32.out +30/−0
- test/data/stdlib/filebas.out +0/−1
- test/data/str.dats +5/−0
- test/data/str.out +5/−0
CHANGELOG.md view
@@ -1,5 +1,11 @@ # language-ats +# 1.7.10.0++ * Add support for left/right shift operators in expressions+ * Add support for array literals+ * Fix bug in `absvt@ype` and `abst@ype` pretty-printing+ # 1.7.9.0 * Support float literals as something other than double literals
language-ats.cabal view
@@ -1,6 +1,6 @@ cabal-version: 1.18 name: language-ats-version: 1.7.9.0+version: 1.7.10.0 license: BSD3 license-file: LICENSE copyright: Copyright: (c) 2018-2019 Vanessa McHale
src/Language/ATS/Parser.y view
@@ -216,6 +216,7 @@ doubleBraces { DoubleBracesTok $$ } doubleBrackets { DoubleBracketTok $$ } prfTransform { Operator $$ ">>" } -- For types like &a >> a?!+ leftShift { Operator $$ "<<" } refType { Special $$ "&" } -- For types like &a maybeProof { Operator $$ "?" } -- For types like a? fromVT { Operator $$ "?!" } -- For types like a?!@@ -551,13 +552,15 @@ | lineComment PreExpression { CommentExpr (to_string $1) $2 } | comma parens(identifier) { MacroVar $1 (to_string $2) } | PreExpression where braces(ATS) { WhereExp $1 $3 }+ | at sqbrackets(Type) sqbrackets(StaticExpression) parens(comma_sep(PreExpression)) { ArrayLit $1 $2 (Just $3) (toList $4) }+ | at sqbrackets(Type) parens(comma_sep(PreExpression)) { ArrayLit $1 $2 Nothing (toList $3) }+ | at sqbrackets(Type) sqbrackets(StaticExpression) doubleParens { ArrayLit $1 $2 (Just $3) [] } | include {% left $ Expected $1 "Expression" "include" } | staload {% left $ Expected (token_posn $1) "Expression" "staload" } | overload {% left $ Expected $1 "Expression" "overload" } | var {% left $ Expected $1 "Expression" "var" } | Termetric {% left $ Expected (fst $1) "Expression" "termetric" } | fromVT {% left $ Expected $1 "Expression" "?!" }- | prfTransform {% left $ Expected $1 "Expression" ">>" } | maybeProof {% left $ Expected $1 "Expression" "?" } | let openParen {% left $ Expected $1 "Expression" "let (" } | let ATS in Expression lineComment {% left $ Expected (token_posn $5) "end" (take 2 $ to_string $5) }@@ -743,6 +746,8 @@ | mutateEq { Mutate } | at { At } | mutateArrow { SpearOp }+ | prfTransform { RShift }+ | leftShift { LShift } | customOperator { SpecialInfix (token_posn $1) (to_string $1) } | backslash identifierSpace { SpecialInfix $1 ('\\' : to_string $2) }
src/Language/ATS/PrettyPrint.hs view
@@ -78,6 +78,8 @@ pretty Mutate = ":=" pretty SpearOp = "->" pretty At = "@"+ pretty RShift = ">>"+ pretty LShift = ">>" pretty (SpecialInfix _ s) = text s splits :: BinOp a -> Bool@@ -181,6 +183,8 @@ a (ProofExprF _ es e') = "(" <> prettyProofExpr es <+> "|" <+> e' <> ")" a (TypeSignatureF e t) = e <+> ":" <+> pretty t a (WhereExpF e d) = prettyWhere e d+ a (ArrayLitF _ ty (Just se) e) = "@[" <> pretty ty <> "][" <> pretty se <> "]" <> prettyArgs e+ a (ArrayLitF _ ty Nothing e) = "@[" <> pretty ty <> "]" <> prettyArgs e 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'@@ -410,6 +414,20 @@ isVal AndDecl{} = True isVal _ = False +isTyDecl :: Declaration a -> Bool+isTyDecl ViewTypeDef{} = True+isTyDecl TypeDef{} = True+isTyDecl ViewDef{} = True+isTyDecl _ = False++isAbsTyDecl :: Declaration a -> Bool+isAbsTyDecl AbsView{} = True+isAbsTyDecl AbsViewType{} = True+isAbsTyDecl AbsVT0p{} = True+isAbsTyDecl AbsT0p{} = True+isAbsTyDecl AbsType{} = True+isAbsTyDecl _ = False+ isOverload :: Declaration a -> Bool isOverload OverloadOp{} = True isOverload OverloadIdent{} = True@@ -426,18 +444,14 @@ glue x y | isVal x && isVal y = True | isOverload x && isOverload y = True+ | isTyDecl x && isTyDecl y = True+ | isAbsTyDecl x && isAbsTyDecl y = True glue Stadef{} Stadef{} = True glue Load{} Load{} = True glue Define{} Define{} = True glue Include{} Include{} = True glue FixityDecl{} FixityDecl{} = True-glue ViewTypeDef{} ViewTypeDef{} = True-glue AbsViewType{} AbsViewType{} = True-glue AbsType{} AbsType{} = True-glue AbsType{} AbsViewType{} = True-glue AbsViewType{} AbsType{} = True glue AbsImpl{} AbsImpl{} = True-glue TypeDef{} TypeDef{} = True glue Comment{} _ = True glue (Func _ Fnx{}) (Func _ And{}) = True glue Assume{} Assume{} = True@@ -691,8 +705,10 @@ pretty (AndD d (Stadef i as (Left (se, mt)))) = pretty d <+> "and" <+> text i <+> prettySortArgs as <+> "=" <+> pretty se <> maybeT mt pretty (AbsView _ i as t) = "absview" <+> text i <> prettySortArgs as <> prettyMaybeType t pretty (AbsVT0p _ i as t) = "absvt@ype" <+> text i <> prettySortArgs as <> prettyMaybeType t- pretty (AbsT0p _ i Nothing t) = "abst@ype" <+> text i <+> "=" <+> pretty t- pretty (AbsT0p _ i as t) = "abst@ype" <+> text i <> prettySortArgs as <> "=" <+> pretty t+ pretty (AbsT0p _ i Nothing Nothing) = "abst@ype" <+> text i+ pretty (AbsT0p _ i Nothing (Just t)) = "abst@ype" <+> text i <+> "=" <+> pretty t+ pretty (AbsT0p _ i as Nothing) = "abst@ype" <+> text i <> prettySortArgs as+ pretty (AbsT0p _ i as (Just t)) = "abst@ype" <+> text i <> prettySortArgs as <> "=" <+> pretty t pretty (ViewDef _ s as t) = "viewdef" <+> text s <> prettySortArgs as <+> "=" <#> pretty t pretty (TKind _ n s) = pretty n <+> "=" <+> text s pretty (SortDef _ s t) = "sortdef" <+> text s <+> "=" <+> either pretty pretty t
src/Language/ATS/Rewrite.hs view
@@ -75,6 +75,8 @@ getFixity _ StaticEq = infix_ 30 getFixity _ Mod = leftFix 60 getFixity _ LessThan = infix_ 40+getFixity _ LShift = leftFix 0+getFixity _ RShift = rightFix 0 getFixity st (SpecialInfix _ op') = case M.lookup op' st of (Just f) -> f
src/Language/ATS/Types.hs view
@@ -296,6 +296,8 @@ | Mutate -- ^ @:=@ | At | SpearOp -- ^ @->@+ | LShift+ | RShift | SpecialInfix a String deriving (Show, Eq, Generic, NFData) @@ -406,6 +408,7 @@ | ParenExpr a (Expression a) | CommentExpr String (Expression a) | MacroVar a String+ | ArrayLit a (Type a) (Maybe (StaticExpression a)) [Expression a] deriving (Show, Eq, Generic, NFData, Recursive, Corecursive) data ExpressionF a x = LetF a (ATS a) (Maybe x)@@ -455,6 +458,7 @@ | ParenExprF a x | CommentExprF String x | MacroVarF a String+ | ArrayLitF a (Type a) (Maybe (StaticExpression a)) [x] deriving (Generic, Functor) type instance Base (Expression a) = (ExpressionF a)
+ test/data/array-literal.dats view
@@ -0,0 +1,258 @@+// TODO: uint32?+val crc32_table = @[uint32][256]( 0x00000000u+ , 0x77073096u+ , 0xEE0E612Cu+ , 0x990951BAu+ , 0x076DC419u+ , 0x706AF48Fu+ , 0xE963A535u+ , 0x9E6495A3u+ , 0x0EDB8832u+ , 0x79DCB8A4u+ , 0xE0D5E91Eu+ , 0x97D2D988u+ , 0x09B64C2Bu+ , 0x7EB17CBDu+ , 0xE7B82D07u+ , 0x90BF1D91u+ , 0x1DB71064u+ , 0x6AB020F2u+ , 0xF3B97148u+ , 0x84BE41DEu+ , 0x1ADAD47Du+ , 0x6DDDE4EBu+ , 0xF4D4B551u+ , 0x83D385C7u+ , 0x136C9856u+ , 0x646BA8C0u+ , 0xFD62F97Au+ , 0x8A65C9ECu+ , 0x14015C4Fu+ , 0x63066CD9u+ , 0xFA0F3D63u+ , 0x8D080DF5u+ , 0x3B6E20C8u+ , 0x4C69105Eu+ , 0xD56041E4u+ , 0xA2677172u+ , 0x3C03E4D1u+ , 0x4B04D447u+ , 0xD20D85FDu+ , 0xA50AB56Bu+ , 0x35B5A8FAu+ , 0x42B2986Cu+ , 0xDBBBC9D6u+ , 0xACBCF940u+ , 0x32D86CE3u+ , 0x45DF5C75u+ , 0xDCD60DCFu+ , 0xABD13D59u+ , 0x26D930ACu+ , 0x51DE003Au+ , 0xC8D75180u+ , 0xBFD06116u+ , 0x21B4F4B5u+ , 0x56B3C423u+ , 0xCFBA9599u+ , 0xB8BDA50Fu+ , 0x2802B89Eu+ , 0x5F058808u+ , 0xC60CD9B2u+ , 0xB10BE924u+ , 0x2F6F7C87u+ , 0x58684C11u+ , 0xC1611DABu+ , 0xB6662D3Du+ , 0x76DC4190u+ , 0x01DB7106u+ , 0x98D220BCu+ , 0xEFD5102Au+ , 0x71B18589u+ , 0x06B6B51Fu+ , 0x9FBFE4A5u+ , 0xE8B8D433u+ , 0x7807C9A2u+ , 0x0F00F934u+ , 0x9609A88Eu+ , 0xE10E9818u+ , 0x7F6A0DBBu+ , 0x086D3D2Du+ , 0x91646C97u+ , 0xE6635C01u+ , 0x6B6B51F4u+ , 0x1C6C6162u+ , 0x856530D8u+ , 0xF262004Eu+ , 0x6C0695EDu+ , 0x1B01A57Bu+ , 0x8208F4C1u+ , 0xF50FC457u+ , 0x65B0D9C6u+ , 0x12B7E950u+ , 0x8BBEB8EAu+ , 0xFCB9887Cu+ , 0x62DD1DDFu+ , 0x15DA2D49u+ , 0x8CD37CF3u+ , 0xFBD44C65u+ , 0x4DB26158u+ , 0x3AB551CEu+ , 0xA3BC0074u+ , 0xD4BB30E2u+ , 0x4ADFA541u+ , 0x3DD895D7u+ , 0xA4D1C46Du+ , 0xD3D6F4FBu+ , 0x4369E96Au+ , 0x346ED9FCu+ , 0xAD678846u+ , 0xDA60B8D0u+ , 0x44042D73u+ , 0x33031DE5u+ , 0xAA0A4C5Fu+ , 0xDD0D7CC9u+ , 0x5005713Cu+ , 0x270241AAu+ , 0xBE0B1010u+ , 0xC90C2086u+ , 0x5768B525u+ , 0x206F85B3u+ , 0xB966D409u+ , 0xCE61E49Fu+ , 0x5EDEF90Eu+ , 0x29D9C998u+ , 0xB0D09822u+ , 0xC7D7A8B4u+ , 0x59B33D17u+ , 0x2EB40D81u+ , 0xB7BD5C3Bu+ , 0xC0BA6CADu+ , 0xEDB88320u+ , 0x9ABFB3B6u+ , 0x03B6E20Cu+ , 0x74B1D29Au+ , 0xEAD54739u+ , 0x9DD277AFu+ , 0x04DB2615u+ , 0x73DC1683u+ , 0xE3630B12u+ , 0x94643B84u+ , 0x0D6D6A3Eu+ , 0x7A6A5AA8u+ , 0xE40ECF0Bu+ , 0x9309FF9Du+ , 0x0A00AE27u+ , 0x7D079EB1u+ , 0xF00F9344u+ , 0x8708A3D2u+ , 0x1E01F268u+ , 0x6906C2FEu+ , 0xF762575Du+ , 0x806567CBu+ , 0x196C3671u+ , 0x6E6B06E7u+ , 0xFED41B76u+ , 0x89D32BE0u+ , 0x10DA7A5Au+ , 0x67DD4ACCu+ , 0xF9B9DF6Fu+ , 0x8EBEEFF9u+ , 0x17B7BE43u+ , 0x60B08ED5u+ , 0xD6D6A3E8u+ , 0xA1D1937Eu+ , 0x38D8C2C4u+ , 0x4FDFF252u+ , 0xD1BB67F1u+ , 0xA6BC5767u+ , 0x3FB506DDu+ , 0x48B2364Bu+ , 0xD80D2BDAu+ , 0xAF0A1B4Cu+ , 0x36034AF6u+ , 0x41047A60u+ , 0xDF60EFC3u+ , 0xA867DF55u+ , 0x316E8EEFu+ , 0x4669BE79u+ , 0xCB61B38Cu+ , 0xBC66831Au+ , 0x256FD2A0u+ , 0x5268E236u+ , 0xCC0C7795u+ , 0xBB0B4703u+ , 0x220216B9u+ , 0x5505262Fu+ , 0xC5BA3BBEu+ , 0xB2BD0B28u+ , 0x2BB45A92u+ , 0x5CB36A04u+ , 0xC2D7FFA7u+ , 0xB5D0CF31u+ , 0x2CD99E8Bu+ , 0x5BDEAE1Du+ , 0x9B64C2B0u+ , 0xEC63F226u+ , 0x756AA39Cu+ , 0x026D930Au+ , 0x9C0906A9u+ , 0xEB0E363Fu+ , 0x72076785u+ , 0x05005713u+ , 0x95BF4A82u+ , 0xE2B87A14u+ , 0x7BB12BAEu+ , 0x0CB61B38u+ , 0x92D28E9Bu+ , 0xE5D5BE0Du+ , 0x7CDCEFB7u+ , 0x0BDBDF21u+ , 0x86D3D2D4u+ , 0xF1D4E242u+ , 0x68DDB3F8u+ , 0x1FDA836Eu+ , 0x81BE16CDu+ , 0xF6B9265Bu+ , 0x6FB077E1u+ , 0x18B74777u+ , 0x88085AE6u+ , 0xFF0F6A70u+ , 0x66063BCAu+ , 0x11010B5Cu+ , 0x8F659EFFu+ , 0xF862AE69u+ , 0x616BFFD3u+ , 0x166CCF45u+ , 0xA00AE278u+ , 0xD70DD2EEu+ , 0x4E048354u+ , 0x3903B3C2u+ , 0xA7672661u+ , 0xD06016F7u+ , 0x4969474Du+ , 0x3E6E77DBu+ , 0xAED16A4Au+ , 0xD9D65ADCu+ , 0x40DF0B66u+ , 0x37D83BF0u+ , 0xA9BCAE53u+ , 0xDEBB9EC5u+ , 0x47B2CF7Fu+ , 0x30B5FFE9u+ , 0xBDBDF21Cu+ , 0xCABAC28Au+ , 0x53B39330u+ , 0x24B4A3A6u+ , 0xBAD03605u+ , 0xCDD70693u+ , 0x54DE5729u+ , 0x23D967BFu+ , 0xB3667A2Eu+ , 0xC4614AB8u+ , 0x5D681B02u+ , 0x2A6F2B94u+ , 0xB40BBE37u+ , 0xC30C8EA1u+ , 0x5A05DF1Bu+ , 0x2D02EF8Du+ )
+ test/data/array-literal.out view
@@ -0,0 +1,258 @@+// TODO: uint32?+val crc32_table = @[uint32][256]( 0x00000000u+ , 0x77073096u+ , 0xEE0E612Cu+ , 0x990951BAu+ , 0x076DC419u+ , 0x706AF48Fu+ , 0xE963A535u+ , 0x9E6495A3u+ , 0x0EDB8832u+ , 0x79DCB8A4u+ , 0xE0D5E91Eu+ , 0x97D2D988u+ , 0x09B64C2Bu+ , 0x7EB17CBDu+ , 0xE7B82D07u+ , 0x90BF1D91u+ , 0x1DB71064u+ , 0x6AB020F2u+ , 0xF3B97148u+ , 0x84BE41DEu+ , 0x1ADAD47Du+ , 0x6DDDE4EBu+ , 0xF4D4B551u+ , 0x83D385C7u+ , 0x136C9856u+ , 0x646BA8C0u+ , 0xFD62F97Au+ , 0x8A65C9ECu+ , 0x14015C4Fu+ , 0x63066CD9u+ , 0xFA0F3D63u+ , 0x8D080DF5u+ , 0x3B6E20C8u+ , 0x4C69105Eu+ , 0xD56041E4u+ , 0xA2677172u+ , 0x3C03E4D1u+ , 0x4B04D447u+ , 0xD20D85FDu+ , 0xA50AB56Bu+ , 0x35B5A8FAu+ , 0x42B2986Cu+ , 0xDBBBC9D6u+ , 0xACBCF940u+ , 0x32D86CE3u+ , 0x45DF5C75u+ , 0xDCD60DCFu+ , 0xABD13D59u+ , 0x26D930ACu+ , 0x51DE003Au+ , 0xC8D75180u+ , 0xBFD06116u+ , 0x21B4F4B5u+ , 0x56B3C423u+ , 0xCFBA9599u+ , 0xB8BDA50Fu+ , 0x2802B89Eu+ , 0x5F058808u+ , 0xC60CD9B2u+ , 0xB10BE924u+ , 0x2F6F7C87u+ , 0x58684C11u+ , 0xC1611DABu+ , 0xB6662D3Du+ , 0x76DC4190u+ , 0x01DB7106u+ , 0x98D220BCu+ , 0xEFD5102Au+ , 0x71B18589u+ , 0x06B6B51Fu+ , 0x9FBFE4A5u+ , 0xE8B8D433u+ , 0x7807C9A2u+ , 0x0F00F934u+ , 0x9609A88Eu+ , 0xE10E9818u+ , 0x7F6A0DBBu+ , 0x086D3D2Du+ , 0x91646C97u+ , 0xE6635C01u+ , 0x6B6B51F4u+ , 0x1C6C6162u+ , 0x856530D8u+ , 0xF262004Eu+ , 0x6C0695EDu+ , 0x1B01A57Bu+ , 0x8208F4C1u+ , 0xF50FC457u+ , 0x65B0D9C6u+ , 0x12B7E950u+ , 0x8BBEB8EAu+ , 0xFCB9887Cu+ , 0x62DD1DDFu+ , 0x15DA2D49u+ , 0x8CD37CF3u+ , 0xFBD44C65u+ , 0x4DB26158u+ , 0x3AB551CEu+ , 0xA3BC0074u+ , 0xD4BB30E2u+ , 0x4ADFA541u+ , 0x3DD895D7u+ , 0xA4D1C46Du+ , 0xD3D6F4FBu+ , 0x4369E96Au+ , 0x346ED9FCu+ , 0xAD678846u+ , 0xDA60B8D0u+ , 0x44042D73u+ , 0x33031DE5u+ , 0xAA0A4C5Fu+ , 0xDD0D7CC9u+ , 0x5005713Cu+ , 0x270241AAu+ , 0xBE0B1010u+ , 0xC90C2086u+ , 0x5768B525u+ , 0x206F85B3u+ , 0xB966D409u+ , 0xCE61E49Fu+ , 0x5EDEF90Eu+ , 0x29D9C998u+ , 0xB0D09822u+ , 0xC7D7A8B4u+ , 0x59B33D17u+ , 0x2EB40D81u+ , 0xB7BD5C3Bu+ , 0xC0BA6CADu+ , 0xEDB88320u+ , 0x9ABFB3B6u+ , 0x03B6E20Cu+ , 0x74B1D29Au+ , 0xEAD54739u+ , 0x9DD277AFu+ , 0x04DB2615u+ , 0x73DC1683u+ , 0xE3630B12u+ , 0x94643B84u+ , 0x0D6D6A3Eu+ , 0x7A6A5AA8u+ , 0xE40ECF0Bu+ , 0x9309FF9Du+ , 0x0A00AE27u+ , 0x7D079EB1u+ , 0xF00F9344u+ , 0x8708A3D2u+ , 0x1E01F268u+ , 0x6906C2FEu+ , 0xF762575Du+ , 0x806567CBu+ , 0x196C3671u+ , 0x6E6B06E7u+ , 0xFED41B76u+ , 0x89D32BE0u+ , 0x10DA7A5Au+ , 0x67DD4ACCu+ , 0xF9B9DF6Fu+ , 0x8EBEEFF9u+ , 0x17B7BE43u+ , 0x60B08ED5u+ , 0xD6D6A3E8u+ , 0xA1D1937Eu+ , 0x38D8C2C4u+ , 0x4FDFF252u+ , 0xD1BB67F1u+ , 0xA6BC5767u+ , 0x3FB506DDu+ , 0x48B2364Bu+ , 0xD80D2BDAu+ , 0xAF0A1B4Cu+ , 0x36034AF6u+ , 0x41047A60u+ , 0xDF60EFC3u+ , 0xA867DF55u+ , 0x316E8EEFu+ , 0x4669BE79u+ , 0xCB61B38Cu+ , 0xBC66831Au+ , 0x256FD2A0u+ , 0x5268E236u+ , 0xCC0C7795u+ , 0xBB0B4703u+ , 0x220216B9u+ , 0x5505262Fu+ , 0xC5BA3BBEu+ , 0xB2BD0B28u+ , 0x2BB45A92u+ , 0x5CB36A04u+ , 0xC2D7FFA7u+ , 0xB5D0CF31u+ , 0x2CD99E8Bu+ , 0x5BDEAE1Du+ , 0x9B64C2B0u+ , 0xEC63F226u+ , 0x756AA39Cu+ , 0x026D930Au+ , 0x9C0906A9u+ , 0xEB0E363Fu+ , 0x72076785u+ , 0x05005713u+ , 0x95BF4A82u+ , 0xE2B87A14u+ , 0x7BB12BAEu+ , 0x0CB61B38u+ , 0x92D28E9Bu+ , 0xE5D5BE0Du+ , 0x7CDCEFB7u+ , 0x0BDBDF21u+ , 0x86D3D2D4u+ , 0xF1D4E242u+ , 0x68DDB3F8u+ , 0x1FDA836Eu+ , 0x81BE16CDu+ , 0xF6B9265Bu+ , 0x6FB077E1u+ , 0x18B74777u+ , 0x88085AE6u+ , 0xFF0F6A70u+ , 0x66063BCAu+ , 0x11010B5Cu+ , 0x8F659EFFu+ , 0xF862AE69u+ , 0x616BFFD3u+ , 0x166CCF45u+ , 0xA00AE278u+ , 0xD70DD2EEu+ , 0x4E048354u+ , 0x3903B3C2u+ , 0xA7672661u+ , 0xD06016F7u+ , 0x4969474Du+ , 0x3E6E77DBu+ , 0xAED16A4Au+ , 0xD9D65ADCu+ , 0x40DF0B66u+ , 0x37D83BF0u+ , 0xA9BCAE53u+ , 0xDEBB9EC5u+ , 0x47B2CF7Fu+ , 0x30B5FFE9u+ , 0xBDBDF21Cu+ , 0xCABAC28Au+ , 0x53B39330u+ , 0x24B4A3A6u+ , 0xBAD03605u+ , 0xCDD70693u+ , 0x54DE5729u+ , 0x23D967BFu+ , 0xB3667A2Eu+ , 0xC4614AB8u+ , 0x5D681B02u+ , 0x2A6F2B94u+ , 0xB40BBE37u+ , 0xC30C8EA1u+ , 0x5A05DF1Bu+ , 0x2D02EF8Du+ )
+ test/data/crc32.dats view
@@ -0,0 +1,27 @@+staload UN = "prelude/SATS/unsafe.sats"++fn byteview_read_as_uint8 {l0:addr}{m:nat}{ l1 : addr | l1 <= l0+m }(pf : !bytes_v(l0, m) | p : ptr(l1)) : uint8 =+ $UN.ptr0_get<uint8>(p)++extern+castfn uint2uint8(uint32) : uint8++extern+castfn uint2uint32(uint) : uint32++// from here: https://docs.microsoft.com/en-us/openspecs/office_protocols/ms-abs/06966aa2-70da-4bf9-8448-3355f277cd77?redirectedfrom=MSDN+fn crc32 {l:addr}{m:nat}(pf : !bytes_v(l, m) | p : ptr(l), l : size_t(m)) : uint32 =+ let+ var crc32_start: uint32 = uint2uint32(0xFFFFFFFFu)+ var i: size_t+ val () = for* { i : nat | i <= m } .<m-i>. (i : size_t(i)) =>+ (i := i2sz(0) ; i < l ; i := i + 1)+ let+ var current_byte = $UN.ptr0_get<uint8>(add_ptr_bsz(p, i))+ var crc_trunc = uint2uint8(crc32_start)+ var ix = g0uint_lxor_uint8(crc_trunc, current_byte)+ var crc_shift = crc32_start >> 8+ in end+ in+ g0uint_lxor_uint32(crc32_start, uint2uint32(0xFFFFFFFFu))+ end
+ test/data/crc32.out view
@@ -0,0 +1,30 @@+staload UN = "prelude/SATS/unsafe.sats"++fn byteview_read_as_uint8+{l0:addr}{m:nat}{ l1 : addr | l1 <= l0+m }(pf : !bytes_v(l0, m)+| p : ptr(l1)) : uint8 =+ $UN.ptr0_get<uint8>(p)++extern+castfn uint2uint8(uint32) : uint8++extern+castfn uint2uint32(uint) : uint32++// from here: https://docs.microsoft.com/en-us/openspecs/office_protocols/ms-abs/06966aa2-70da-4bf9-8448-3355f277cd77?redirectedfrom=MSDN+fn crc32 {l:addr}{m:nat}(pf : !bytes_v(l, m)+ | p : ptr(l), l : size_t(m)) : uint32 =+ let+ var crc32_start: uint32 = uint2uint32(0xFFFFFFFFu)+ var i: size_t+ val () = for* { i : nat | i <= m } .<m-i>. (i : size_t(i)) =>+ (i := i2sz(0) ; i < l ; i := i + 1)+ let+ var current_byte = $UN.ptr0_get<uint8>(add_ptr_bsz(p, i))+ var crc_trunc = uint2uint8(crc32_start)+ var ix = g0uint_lxor_uint8(crc_trunc, current_byte)+ var crc_shift = crc32_start >> 8+ in end+ in+ g0uint_lxor_uint32(crc32_start, uint2uint32(0xFFFFFFFFu))+ end
test/data/stdlib/filebas.out view
@@ -242,7 +242,6 @@ // end of [fileref_get_exnloc] (* ****** ****** *) typedef charlst = List0(char)- vtypedef charlst_vt = List0_vt(char) (* ****** ****** *)
+ test/data/str.dats view
@@ -0,0 +1,5 @@+abst@ype strlen(n: int)+viewdef string_v(n:int, l:addr) = strlen(n) @ l+vtypedef string_vt(n: int, l:addr) = (string_v(n, l) | ptr(l))++vtypedef String_vt = [n:nat][l:addr | l > null] string_vt(n, l)
+ test/data/str.out view
@@ -0,0 +1,5 @@+abst@ype strlen(n: int)++viewdef string_v(n: int, l: addr) = strlen(n) @ l+vtypedef string_vt(n: int, l: addr) = (string_v(n, l) | ptr(l))+vtypedef String_vt = [n:nat][ l : addr | l > null ] string_vt(n, l)