packages feed

ivory-stdlib (empty) → 0.1.0.0

raw patch · 13 files changed

+905/−0 lines, 13 filesdep +basedep +filepathdep +ivorysetup-changed

Dependencies added: base, filepath, ivory

Files

+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c)2013, Galois, Inc++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Galois, Inc nor the names of its contributors+      may be used to endorse or promote products derived from this software+      without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ ivory-stdlib.cabal view
@@ -0,0 +1,39 @@+name:                ivory-stdlib+version:             0.1.0.0+author:              Galois, Inc.+maintainer:          pat@galois.com+copyright:           2013 Galois, Inc.+category:            Language+synopsis:            Ivory standard library.+description:         A standard library for Ivory.+homepage:            http://smaccmpilot.org/languages/ivory-introduction.html+build-type:          Simple+cabal-version:       >= 1.10+license:             BSD3+license-file:        LICENSE+data-files: support/ivory_stdlib_string_prim.h,+            support/ivory_stdlib_string_prim.c+source-repository    this+  type:     git+  location: https://github.com/GaloisInc/ivory+  tag:      hackage-stdlib-0100++library+  exposed-modules:      Ivory.Stdlib,+                        Ivory.Stdlib.Control,+                        Ivory.Stdlib.Memory,+                        Ivory.Stdlib.Operators,+                        Ivory.Stdlib.String,+                        Ivory.Stdlib.Trig,+                        Ivory.Stdlib.SearchDir,+                        Ivory.Stdlib.Maybe++  other-modules:        Paths_ivory_stdlib++  build-depends:        base >= 4.6 && < 4.7,+                        filepath,+                        ivory++  hs-source-dirs:       src+  default-language:     Haskell2010+  ghc-options:          -Wall
+ src/Ivory/Stdlib.hs view
@@ -0,0 +1,23 @@++module Ivory.Stdlib+  ( module Ivory.Stdlib.Control+  , module Ivory.Stdlib.Memory+  , module Ivory.Stdlib.Operators+  , module Ivory.Stdlib.String+  , module Ivory.Stdlib.Maybe+  , stdlibModules+  ) where++import Ivory.Language (Module)++import Ivory.Stdlib.Control+import Ivory.Stdlib.Memory+import Ivory.Stdlib.Operators+import Ivory.Stdlib.String+import Ivory.Stdlib.Maybe++stdlibModules :: [Module]+stdlibModules =+  [ stdlibStringModule+  ]+
+ src/Ivory/Stdlib/Control.hs view
@@ -0,0 +1,87 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE TypeFamilies #-}++module Ivory.Stdlib.Control+  ( ifte+  , when+  , unless+  , cond_, cond, (==>)+  ) where++import Ivory.Language++ifte :: ( IvoryStore a+        , IvoryZero (Stored a)+        , GetAlloc eff ~ Scope s+        ) => IBool+          -> Ivory eff a+          -> Ivory eff a+          -> Ivory eff a+ifte c t f = do+  r <- local izero+  ifte_ c+    (t >>= store r)+    (f >>= store r)+  deref r++when :: IBool -> Ivory eff () -> Ivory eff ()+when c t = ifte_ c t (return ())++unless :: IBool -> Ivory eff () -> Ivory eff ()+unless c f =  ifte_ c (return ()) f++data Cond eff a = Cond IBool (Ivory eff a)++(==>) :: IBool -> Ivory eff a -> Cond eff a+(==>) = Cond++infix 0 ==>++-- | A multi-way if.  This is useful for avoiding an explosion of+-- nesting and parentheses in complex conditionals.+--+-- Instead of writing nested chains of ifs:+--+-- > ifte_ (x >? 100)+-- >   (store result 10)+-- >   (ifte_ (x >? 50)+-- >     (store result 5)+-- >     (ifte_ (x >? 0)+-- >       (store result 1)+-- >       (store result 0)))+--+-- You can write:+--+-- > cond_+-- >   [ x >? 100 ==> store result 10+-- >   , x >? 50  ==> store result 5+-- >   , x >? 0   ==> store result 1+-- >   , true     ==> store result 0+-- >   ]+--+-- Note that "==>" is non-associative and has precedence 0, so you+-- will need parentheses to call functions with "$" on the left-hand+-- side:+--+-- > cond_ [ (f $ g x) ==> y ]+--+-- rather than:+--+-- > cond_ [ f $ g x ==> y ]+cond_ :: [Cond eff ()] -> Ivory eff ()+cond_ [] = return ()+cond_ ((Cond b f):cs) = ifte_ b f (cond_ cs)++cond :: ( IvoryStore a+        , IvoryZero (Stored a)+        , GetAlloc eff ~ Scope s+        ) => [Cond eff a] -> Ivory eff a+cond as = do+  r <- local izero+  aux as r+  deref r+  where+  aux [] _ = return ()+  aux ((Cond b f):cs) r = ifte_ b (f >>= store r) (aux cs r)
+ src/Ivory/Stdlib/Maybe.hs view
@@ -0,0 +1,178 @@+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE FlexibleContexts #-}+--+-- Maybe.hs --- Optional Ivory values.+--+-- Copyright (C) 2013, Galois, Inc.+-- All Rights Reserved.+--+-- This software is released under the "BSD3" license.  Read the file+-- "LICENSE" for more information.+--++-- | This module provides an interface for a nullable Ivory type.+--+-- To define a type like Haskell's @Maybe Float@, define an+-- Ivory structure type, and make the structure an instance+-- of 'MaybeType'.+--+-- > [ivory|+-- > struct maybe_float+-- >   { mf_valid :: Stored IBool+-- >   ; mf_value :: Stored IFloat+-- >   }+-- > |]+-- >+-- > instance MaybeType "maybe_float" IFloat where+-- >   maybeValidLabel = mf_valid+-- >   maybeValueLabel = mf_value+--+-- With this definition in place, any of the functions in this+-- module will accept a @Struct \"maybe_float\"@.+--+-- These structure types must be defined in an Ivory module as+-- usual, and it is recommended to make them private unless they+-- are necessary as part of the module's public interface.+module Ivory.Stdlib.Maybe+  (+  -- * Interface+  MaybeType(..)++  -- * Initialization+  , initJust, initNothing++  -- * Getting+  , getMaybe++  -- * Setting+  , setJust, setNothing+  , setDefault, setDefault_++  -- * Modifying+  , mapMaybe+  , mapMaybeM, mapMaybeM_+  , forMaybeM, forMaybeM_+  ) where++import GHC.TypeLits++import Ivory.Language++class (IvoryStruct sym, IvoryExpr t, IvoryStore t, IvoryInit t) =>+      MaybeType (sym :: Symbol) t | sym -> t where+  -- | Return a boolean field indicating whether the value is valid.+  maybeValidLabel :: Label sym (Stored IBool)+  -- | Return the field containing a value, if it is valid.+  maybeValueLabel :: Label sym (Stored t)++-- | Return an initializer for a maybe type with a valid value.+initJust :: MaybeType sym a => a -> Init (Struct sym)+initJust x =+  istruct+    [ maybeValidLabel .= ival true+    , maybeValueLabel .= ival x+    ]++-- | Return an initializer for a maybe type with no value.+initNothing :: MaybeType sym a => Init (Struct sym)+initNothing =+  istruct+    [ maybeValidLabel .= ival false+    ]++-- | Retrieve a maybe's value given a default if it is nothing.+getMaybe :: MaybeType sym a+         => ConstRef s1 (Struct sym)+         -> a+         -> Ivory eff a+getMaybe ref def = do+  valid <- deref (ref ~> maybeValidLabel)+  value <- deref (ref ~> maybeValueLabel)+  assign (valid ? (value, def))++-- | Set a maybe's value to a default if it is nothing, returning+-- the current value.+setDefault :: MaybeType sym a+           => Ref s1 (Struct sym)+           -> a+           -> Ivory eff a+setDefault ref def = do+  setDefault_ ref def+  deref (ref ~> maybeValueLabel)++-- | Set a maybe's value to a default value if it is nothing.+setDefault_ :: MaybeType sym a+            => Ref s1 (Struct sym)+            -> a+            -> Ivory eff ()+setDefault_ ref def = do+  valid <- deref (ref ~> maybeValidLabel)+  ifte_ (iNot valid)+    (do store (ref ~> maybeValidLabel) true+        store (ref ~> maybeValueLabel) def)+    (return ())++-- | Modify a maybe value by an expression if it is not nothing.+mapMaybe :: MaybeType sym a+         => (a -> a)+         -> Ref s1 (Struct sym)+         -> Ivory eff ()+mapMaybe f ref = mapMaybeM (return . f) ref++-- | Modify a maybe value by an action if it is not nothing.+mapMaybeM :: MaybeType sym a+          => (a -> Ivory eff a)+          -> Ref s1 (Struct sym)+          -> Ivory eff ()+mapMaybeM f ref = do+  valid <- deref (ref ~> maybeValidLabel)+  ifte_ valid+    (do value  <- deref (ref ~> maybeValueLabel)+        value' <- f value+        store (ref ~> maybeValueLabel) value')+    (return ())++-- | Flipped version of 'mapMaybeM'.+forMaybeM :: MaybeType sym a+          => Ref s1 (Struct sym)+          -> (a -> Ivory eff a)+          -> Ivory eff ()+forMaybeM = flip mapMaybeM++-- | Call an action with a maybe value if it is not nothing.+mapMaybeM_ :: MaybeType sym a+           => (a -> Ivory eff ())+           -> Ref s1 (Struct sym)+           -> Ivory eff ()+mapMaybeM_ f ref = do+  valid <- deref (ref ~> maybeValidLabel)+  ifte_ valid+    (do value <- deref (ref ~> maybeValueLabel)+        f value)+    (return ())++-- | Flipped version of 'mapMaybeM_'.+forMaybeM_ :: MaybeType sym a+           => Ref s1 (Struct sym)+           -> (a -> Ivory eff ())+           -> Ivory eff ()+forMaybeM_ = flip mapMaybeM_++-- | Set a maybe value to a valid value.+setJust :: MaybeType sym a+        => Ref s1 (Struct sym)+        -> a+        -> Ivory eff ()+setJust ref x = do+  store (ref ~> maybeValidLabel) true+  store (ref ~> maybeValueLabel) x++-- | Set a maybe value to an invalid value.+setNothing :: MaybeType sym a+           => Ref s1 (Struct sym)+           -> Ivory eff ()+setNothing ref = store (ref ~> maybeValidLabel) false+
+ src/Ivory/Stdlib/Memory.hs view
@@ -0,0 +1,68 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE ScopedTypeVariables #-}++module Ivory.Stdlib.Memory+  ( resultInto+  , into+  , arrayCopy+  ) where++import Ivory.Language+import Ivory.Stdlib.Control++-- | handy shorthand for transfering members+resultInto :: IvoryStore a =>+     Ivory eff a -> Ref s (Stored a) -> Ivory eff ()+resultInto a b = store b =<< a++into :: IvoryStore a =>+     Ref s (Stored a) -> Ref s' (Stored a) -> Ivory eff ()+into a b = store b =<< deref a++-- XXX Belongs with Pack.hs and SafePack.hs.++-- | Copies a prefix of an array into a postfix of another array.  That is, copy+-- from array @from@ (either a 'Ref' or a 'ConstRef') into array @to@ starting+-- at index @toOffset@ in @to@.  Copying continues until either the from array+-- is fully copied, the @to@ array is full, or index @end@ in the @from@ array+-- is reached (index @end@ is not copied).  to copy the full @from@ array, let+-- @end@ equal 'arrayLen from'.+arrayCopy :: forall n m r s0 s1 s2 eff t.+           ( SingI n, SingI m, IvoryRef r+           , IvoryExpr (r s2 (Array m (Stored t)))+           , IvoryExpr (r s2 (Stored t))+           , IvoryStore t+           , GetAlloc eff ~ Scope s0+           )+        => Ref s1 (Array n (Stored t))+        -> r s2 (Array m (Stored t))+        -> Sint32+        -> Sint32+        -> Ivory eff ()+arrayCopy to from toOffset end = do+  assert (toOffset >=? 0 .&& toOffset <? toLen)+  assert (end      >=? 0 .&& end     <=? frLen)+  arrayMap $ go+  where+  -- The index is w.r.t. the from array.+  go ix =+    cond_+      [   -- We've reached the @end@ index: stop copying.+          (fromIx ix >=? end)+      ==> return ()+      ,   -- We've reached the end of the @to@ array: stop copying.+          (fromIx ix + toOffset >=? toLen)+      ==> return ()+      ,   true+      ==> (deref (from ! ix) >>= store (to ! mkIx ix))+      ]++  toLen = arrayLen to+  frLen = arrayLen from++  mkIx :: Ix m -> Ix n+  mkIx ix = toIx (toOffset + fromIx ix)+
+ src/Ivory/Stdlib/Operators.hs view
@@ -0,0 +1,39 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE FlexibleContexts #-}++module Ivory.Stdlib.Operators where++import Ivory.Language++-- | Infix structure field access and dereference.+-- This is a shorthand for 'deref $ s~>x'.+(~>*) :: (IvoryVar a, IvoryStruct sym, IvoryRef ref,+          IvoryExpr (ref s (Stored a)),+          IvoryExpr (ref s (Struct sym))) =>+            ref s (Struct sym) -> Label sym (Stored a) -> Ivory eff a+struct ~>* label = deref $ struct~>label+infixl 8 ~>*+++-- | Modify the value stored at a reference by a function.+(%=) :: IvoryStore a =>+     Ref s (Stored a) -> (a -> a) -> Ivory eff ()+ref %= f = do+  val <- deref ref+  store ref (f val)++-- | Modify the value stored at a reference by a function that returns+-- a value in the Ivory monad+(%=!) :: IvoryStore a =>+         Ref s (Stored a) -> (a -> Ivory eff a) -> Ivory eff ()+ref %=! mf = do+  val  <- deref ref+  val' <- mf val+  store ref val'++-- | Increment the value stored at a reference.+(+=) :: (Num a, IvoryStore a) =>+        Ref s (Stored a) -> a -> Ivory eff ()+ref += x = ref %= (+ x)+
+ src/Ivory/Stdlib/SearchDir.hs view
@@ -0,0 +1,13 @@++module Ivory.Stdlib.SearchDir where++import System.FilePath++import qualified Paths_ivory_stdlib++searchDir :: IO FilePath+searchDir = do+  base <- Paths_ivory_stdlib.getDataDir+  return $ base </> "support"++
+ src/Ivory/Stdlib/String.hs view
@@ -0,0 +1,264 @@+{-# OPTIONS_GHC -fno-warn-orphans #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE QuasiQuotes #-}+--+-- String.hs --- C-string utilities for Ivory.+--+-- Copyright (C) 2013, Galois, Inc.+-- All Rights Reserved.+--++module Ivory.Stdlib.String where+  -- ( copy_istring , strcpy , strncpy , strncpy_uint8 , strncmp+  -- , stdlibStringModule+  -- ) where++import Data.Char (ord)+import GHC.TypeLits++import Ivory.Language++import qualified Control.Monad as M++----------------------------------------------------------------------+-- Yet Another Ivory String Type++-- TODO: Should we generate a warning or error if the string+-- is too long for the string type?+gen_stringInit :: (IvoryStruct name, SingI len)+               => Label name (Array len (Stored Uint8))+               -> Label name (Stored (Ix len))+               -> String+               -> Init (Struct name)+gen_stringInit l_data l_len xs =+  istruct+    [ l_data .= iarray (map (ival . fromIntegral . ord) xs)+    , l_len  .= ival (toIx len)+    ]+  where+  len :: Sint32+  len = fromIntegral (length xs)++stringInit :: IvoryString str => String -> Init str+stringInit = gen_stringInit stringDataL stringLengthL++----------------------------------------------------------------------+-- Generic Functions++stringCapacity :: forall ref str s.+                  (IvoryString str, IvoryRef ref)+               => ref s str -> Sint32+stringCapacity _ = len+  where+  len :: Sint32+  len = fromIntegral (fromSing (sing :: Sing (Capacity str)))++-- Polymorphic "stringLength" function allowing read/write access+-- to the string length.  This is not exported, only a specialized+-- read-only version.+stringLength :: ( IvoryString str+                , IvoryRef ref+                , IvoryExpr (ref s (Stored (Ix (Capacity str))))+                , IvoryExpr (ref s str))+             => ref s str -> ref s (Stored (Ix (Capacity str)))+stringLength x = x ~> stringLengthL++stringData :: ( IvoryString str+              , IvoryRef ref+              , IvoryExpr (ref s (Array (Capacity str) (Stored Uint8)))+              , IvoryExpr (ref s (CArray (Stored Uint8)))+              , IvoryExpr (ref s str))+           => ref s str -> ref s (CArray (Stored Uint8))+stringData x = toCArray (x ~> stringDataL)++-- | Binding to the C "memcmp" function.+memcmp :: Def ('[ ConstRef s1 (CArray (Stored Uint8))+                , ConstRef s2 (CArray (Stored Uint8))+                , Sint32] :-> Sint32)+memcmp = importProc "memcmp" "string.h"++-- | Binding to the C "memcpy" function.+memcpy :: Def ('[ Ref      s1 (CArray (Stored Uint8))+                , ConstRef s2 (CArray (Stored Uint8))+                , Sint32] :-> Sint32)+memcpy = importProc "memcpy" "string.h"++-- | Return the length of a string.+istr_len :: IvoryString str+         => ConstRef s str+         -> Ivory eff (Ix (Capacity str))+istr_len str = do+  len <- deref (stringLength str)+  assert (fromIx len <? stringCapacity str)+  return len++-- | Copy one string into another of the same type.+istr_copy :: IvoryString str+          => Ref      s1 str+          -> ConstRef s2 str+          -> Ivory eff ()+istr_copy dest src = do+  len <- istr_len src+  call_ memcpy (stringData dest) (stringData src) (fromIx len)+  store (stringLength dest) len++-- | Copy one string to another of a possibly different type.  If+-- the destination string is too small, the output may be truncated.+-- This returns true if the string fit, and false if it was+-- truncated to fit the destination.+--+-- TODO: Implement this once it's needed.+istr_convert :: (IvoryString str1, IvoryString str2)+             => Ref      s1 str1+             -> ConstRef s2 str2+             -> Ivory eff IBool+istr_convert = undefined++-- | Internal function to compare strings for equality.+do_istr_eq :: Def ('[ ConstRef s1 (CArray (Stored Uint8))+                    , Sint32+                    , ConstRef s2 (CArray (Stored Uint8))+                    , Sint32+                    ] :-> IBool)+do_istr_eq = proc "ivory_string_eq" $ \s1 len1 s2 len2 -> body $ do+  ifte_ (len1 ==? len2)+    (do r <- call memcmp s1 s2 len1+        ret (r ==? 0))+    (ret false)++-- | Compare strings (of possibly different types) for equality.+-- Returns true if the strings are the same length and contain the+-- same bytes.+istr_eq :: (IvoryString str1, IvoryString str2)+        => ConstRef s1 str1+        -> ConstRef s2 str2+        -> Ivory eff IBool+istr_eq s1 s2 = do+  len1 <- istr_len s1+  ptr1 <- assign (stringData s1)+  len2 <- istr_len s2+  ptr2 <- assign (stringData s2)+  call do_istr_eq ptr1 (fromIx len1) ptr2 (fromIx len2)++-- | Primitive function to do a bounded string copy.+string_copy :: Def ('[ Ref s1 (CArray (Stored Uint8))+                     , Sint32+                     , ConstRef s2 (CArray (Stored Uint8))+                     , Sint32] :-> Sint32)+string_copy = importProc "ivory_stdlib_string_copy"+                         "ivory_stdlib_string_prim.h"++-- | Primitive function to do a bounded null-terminated string copy.+string_copy_z :: Def ('[ Ref s1 (CArray (Stored Uint8))+                       , Sint32+                       , ConstRef s2 (CArray (Stored Uint8))+                       , Sint32] :-> Sint32)+string_copy_z = importProc "ivory_stdlib_string_copy_z"+                           "ivory_stdlib_string_prim.h"++-- | Copy the contents of a fixed-size C string into an Ivory+-- string.  If the source string is not null terminated (and+-- therefore corrupt), this will copy no more than 'len'+-- characters.+--+-- FIXME: This should return false if the string was truncated.+-- (Can we actually detect this at compile-time?  I think we+-- should be able to...)+istr_from_sz :: forall s1 s2 eff len str.+                (SingI len, IvoryString str)+             => Ref      s1 str+             -> ConstRef s2 (Array len (Stored Uint8))+             -> Ivory eff ()+istr_from_sz dest src = do+  len1     <- assign (stringCapacity (constRef dest))+  ptr1     <- assign (stringData dest)+  let len2  = fromIntegral (fromSing (sing :: Sing len))+  ptr2     <- assign (toCArray src)+  result   <- call string_copy_z ptr1 len1 ptr2 len2+  store (stringLength dest) (toIx result)++-- | Copy an Ivory string to a fixed-size, null-terminated C+-- string.  The destination string is always properly terminated,+-- but may be truncated if the buffer is too small.+--+-- FIXME: This should return false if the string was truncated.+-- (Can we actually detect this at compile-time?  I think we+-- should be able to...)+sz_from_istr :: forall s1 s2 eff len str.+                (SingI len, IvoryString str)+             => Ref      s1 (Array len (Stored Uint8))+             -> ConstRef s2 str+             -> Ivory eff ()+sz_from_istr dest src = do+  let dest_capacity = fromSing (sing :: Sing len)+  M.when (dest_capacity > 0) $ do+    let dest_len = fromIntegral (dest_capacity - 1)+    src_data <- assign (stringData src)+    src_len  <- istr_len src+    _result  <- call string_copy (toCArray dest) dest_len src_data (fromIx src_len)+    -- XXX is this right?  shouldn't it use "result"?+    store (dest ! toIx (dest_len - 1)) 0++----------------------------------------------------------------------+-- Old String Functions++-- TODO: Delete these if they aren't used anymore.++-- | Safely copy an IString (string literal) into a character array.+-- The resulting string will always be null terminated.+copy_istring :: Def ('[ Ref s (CArray (Stored IChar)) -- dest+                      , IString                       -- src+                      , Uint32]                       -- len+                     :-> ())+copy_istring = importProc "ivory_stdlib_strlcpy" "ivory_stdlib_string_prim.h"++-- | Type class to generate the correct call to a string function to+-- copy one C string to another.+class (IvoryType dest, IvoryType src) => Strcpy dest src where+  strcpy :: dest -> src -> Ivory eff ()++-- | Strcpy instance for copying string constants to arrays of+-- characters.+instance (SingI len) => Strcpy (Ref s (Array len (Stored IChar))) IString where+  strcpy dest src = call_ copy_istring (toCArray dest) src (arrayLen dest)++-- | Binding to the C "strncmp" function.+strncmp :: Def ('[ ConstRef s1 (CArray (Stored IChar)) -- s1+                 , ConstRef s2 (CArray (Stored IChar)) -- s2+                 , Uint32]                             -- len+                :-> Sint32)+strncmp = importProc "strncmp" "string.h"+++strncpy :: Def ('[ Ref s1  (CArray (Stored IChar))+                 , ConstRef s2 (CArray (Stored IChar))+                 , Uint32+                 ] :-> ())+strncpy = importProc "strncpy" "string.h"++strncpy_uint8 :: Def ('[ Ref s1  (CArray (Stored Uint8))+                 , ConstRef s2 (CArray (Stored IChar))+                 , Uint32+                 ] :-> ())+strncpy_uint8 = importProc "ivory_stdlib_strncpy_uint8" "ivory_stdlib_string_prim.h"++-- | Ivory module definition.+stdlibStringModule :: Module+stdlibStringModule = package "ivory_stdlib_string" $ do+  inclHeader "ivory_stdlib_string_prim.h"+  inclHeader "string.h"+  incl copy_istring+  incl strncmp+  incl memcmp+  incl memcpy+  incl do_istr_eq+  incl string_copy+  incl string_copy_z+  sourceDep "ivory_stdlib_string_prim.h"+  sourceDep "ivory_stdlib_string_prim.c"+
+ src/Ivory/Stdlib/Trig.hs view
@@ -0,0 +1,15 @@++module Ivory.Stdlib.Trig+  ( iAtan2+  ) where++import Ivory.Language++-- spec: http://en.wikipedia.org/wiki/Atan2+iAtan2 :: (IvoryOrd a, Floating a) => a -> a -> a+iAtan2 y x = ((x >? 0)?(                   atan(y/x)+              ,((y >=? 0).&&(x <? 0))?(    atan(y/x) + pi+               ,((y <? 0).&&(x <? 0))?(    atan(y/x) - pi+                ,((y >? 0).&&(x ==? 0))?(  pi/2+                 ,((y <? 0).&&(x ==? 0))?( -1*(pi/2)+                  ,0))))))
+ support/ivory_stdlib_string_prim.c view
@@ -0,0 +1,104 @@++#include "ivory_stdlib_string_prim.h"+#include <string.h>++void ivory_stdlib_strncpy_uint8(uint8_t *dest, const char *src,  uint32_t size) {+    strncpy((char*)dest, src, size);+}++/*+ * Copy src to string dst of size siz.  At most siz-1 characters+ * will be copied.  Always NUL terminates (unless siz == 0).+ * Returns strlen(src); if retval >= siz, truncation occurred.+ *+ * Copyright (c) 1998 Todd C. Miller <Todd.Miller@courtesan.com>+ * All rights reserved.+ *+ * Redistribution and use in source and binary forms, with or without+ * modification, are permitted provided that the following conditions+ * are met:+ * 1. Redistributions of source code must retain the above copyright+ *    notice, this list of conditions and the following disclaimer.+ * 2. Redistributions in binary form must reproduce the above copyright+ *    notice, this list of conditions and the following disclaimer in the+ *    documentation and/or other materials provided with the distribution.+ * 3. The name of the author may not be used to endorse or promote products+ *    derived from this software without specific prior written permission.+ *+ * THIS SOFTWARE IS PROVIDED ``AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES,+ * INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY+ * AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL+ * THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,+ * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,+ * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS;+ * OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY,+ * WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR+ * OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF+ * ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.+ */+uint32_t ivory_stdlib_strlcpy(char *dest, const char *src, uint32_t size)+{+    char *d = dest;+    const char *s = src;+    uint32_t n = size;++    /* Copy as many bytes as will fit */+    if (n != 0 && --n != 0) {+        do {+            if ((*d++ = *s++) == 0)+                break;+        } while (--n != 0);+    }++    /* Not enough room in dest, add NUL and traverse rest of src */+    if (n == 0) {+        if (size != 0)+            *d = '\0';		/* NUL-terminate dest */+        while (*s++)+            ;+    }++    return (s - src - 1);	/* count does not include NUL */+}++/* Copy at most 'min(dest_len, src_len)' bytes from 'src' to+ * dest.  Returns the number of bytes written to 'dest', which+ * is not null terminated. */+int32_t ivory_stdlib_string_copy(+    uint8_t *dest, int32_t dest_len,+    const uint8_t *src, int32_t src_len)+{+    int32_t result = 0;+    int32_t n = dest_len < src_len ? dest_len : src_len;++    for (int32_t i = 0; i < n; ++i) {+        dest[i] = src[i];+        ++result;+    }++  return result;+}++/* Copy at most 'min(dest_len, src_len)' bytes from 'src' to+ * dest, stopping early if a null terminator is encountered.+ *+ * Returns the number of bytes written to 'dest' (which is+ * never null-terminated. */+int32_t ivory_stdlib_string_copy_z(+    uint8_t *dest, int32_t dest_len,+    const uint8_t *src, int32_t src_len)+{+    int32_t result = 0;+    int32_t n = dest_len < src_len ? dest_len : src_len;++    for (int32_t i = 0; i < n; ++i) {+        if (src[i] == 0)+            break;++        dest[i] = src[i];+        ++result;+    }++  return result;+}+
+ support/ivory_stdlib_string_prim.h view
@@ -0,0 +1,43 @@+/* -*- Mode: C; indent-tabs-mode: nil; c-basic-offset: 4 -*- */+/*+ * ivory_string_stdlib_prim.h --- C string primitives.+ *+ * Copyright (C) 2013, Galois, Inc.+ * All Rights Reserved.+ */++#ifndef __IVORY_STDLIB_STRING_PRIM_H__+#define __IVORY_STDLIB_STRING_PRIM_H__++#include <stdlib.h>+#include <stdint.h>++#ifdef __cplusplus+extern "C" {+#endif++uint32_t ivory_stdlib_strlcpy(char *dest, const char *src,  uint32_t size);++void ivory_stdlib_strncpy_uint8( uint8_t *dest, const char *src, uint32_t size);++/* Copy at most 'min(dest_len, src_len)' bytes from 'src' to+ * dest, stopping early if a null terminator is encountered.+ *+ * Returns the number of bytes written to 'dest' (which is+ * never null-terminated. */+int32_t ivory_stdlib_string_copy_z(+  uint8_t *dest, int32_t dest_len,+  const uint8_t *src, int32_t src_len);++/* Copy at most 'min(dest_len, src_len)' bytes from 'src' to+ * dest.  Returns the number of bytes written to 'dest', which+ * is not null terminated. */+int32_t ivory_stdlib_string_copy(+    uint8_t *dest, int32_t dest_len,+    const uint8_t *src, int32_t src_len);++#ifdef __cplusplus+}+#endif++#endif  /* !defined __IVORY_STDLIB_STRING_PRIM_H__ */