diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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 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.7.9.0 +version: 1.7.10.0 license: BSD3 license-file: LICENSE copyright: Copyright: (c) 2018-2019 Vanessa McHale 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 @@ -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) } 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 @@ -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 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 @@ -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 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 @@ -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) diff --git a/test/data/array-literal.dats b/test/data/array-literal.dats new file mode 100644 --- /dev/null +++ b/test/data/array-literal.dats @@ -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 + ) diff --git a/test/data/array-literal.out b/test/data/array-literal.out new file mode 100644 --- /dev/null +++ b/test/data/array-literal.out @@ -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 + ) diff --git a/test/data/crc32.dats b/test/data/crc32.dats new file mode 100644 --- /dev/null +++ b/test/data/crc32.dats @@ -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(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 } .. (i : size_t(i)) => + (i := i2sz(0) ; i < l ; i := i + 1) + let + var current_byte = $UN.ptr0_get(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 diff --git a/test/data/crc32.out b/test/data/crc32.out new file mode 100644 --- /dev/null +++ b/test/data/crc32.out @@ -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(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 } .. (i : size_t(i)) => + (i := i2sz(0) ; i < l ; i := i + 1) + let + var current_byte = $UN.ptr0_get(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 diff --git a/test/data/stdlib/filebas.out b/test/data/stdlib/filebas.out --- a/test/data/stdlib/filebas.out +++ b/test/data/stdlib/filebas.out @@ -242,7 +242,6 @@ // end of [fileref_get_exnloc] (* ****** ****** *) typedef charlst = List0(char) - vtypedef charlst_vt = List0_vt(char) (* ****** ****** *) diff --git a/test/data/str.dats b/test/data/str.dats new file mode 100644 --- /dev/null +++ b/test/data/str.dats @@ -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) diff --git a/test/data/str.out b/test/data/str.out new file mode 100644 --- /dev/null +++ b/test/data/str.out @@ -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)