pec-0.1: test_cases/StrBuf.pec

module StrBuf exports all

where

import Prelude

type StrBuf #cnt = | StrBuf (Array (SuccCnt cnt) Char)

extern "strcmp" c_strcmp :: Ptr Char -> Ptr Char -> I32
extern "strlen" c_strlen :: Ptr Char -> W32
extern "strncpy" c_strncpy :: Ptr Char -> Ptr Char -> I32 -> Ptr Char
// a different name can be used for the C call if necessary

>type StrBuf a = StrBuf_ a
>
>strbuf_ :: (Count cnt, Typed cnt) => Term (cnt -> StrBuf cnt)
>strbuf_ = lam_ $ \(a :: Term cnt) ->
>  cast (app2 array_ (unused :: Term (SuccCnt cnt)) (char '\0'))
>
>from_strbuf_ :: Count cnt => Term (Ptr (StrBuf cnt) -> Ptr Char)
>from_strbuf_ = lam_ bitcast
>
>put_ :: Count cnt => Term (Ptr (StrBuf cnt) -> ())
>put_ = lam_ $ \p -> app puts_ (app from_strbuf_ p)
>
>strlen_ :: Count cnt => Term (Ptr (StrBuf cnt) -> W32)
>strlen_ = lam_ $ \x -> app c_strlen_ (app from_strbuf_ x)
>
>strcmp_ :: (Count a, Count b) =>
>  Term (Ptr (StrBuf a) -> Ptr (StrBuf b) -> Ordering_)
>strcmp_ = lam2_ $ \x y ->
>  app to_ordering_ (app2 c_strcmp_ (app from_strbuf_ x) (app from_strbuf_ y))
>
>to_strbuf_ :: Count cnt => Term (IString -> Ptr (StrBuf cnt) -> Bool_)
>to_strbuf_ = lam2_ $ \x y -> app2 strncpy (app from_istring_ x) y
>
>strcpy_ :: (Count a, Count b) =>
>  Term (Ptr (StrBuf a) -> Ptr (StrBuf b) -> Bool_)
>strcpy_ = lam2_ $ \x y -> app2 strncpy (app from_strbuf_ x) y
>
>strncpy :: Count cnt => Term (Ptr Char -> Ptr (StrBuf cnt) -> Bool_)
>strncpy = lam2_ $ \x (y :: Term (Ptr (StrBuf cnt))) -> Lift $ do
>  let n = countof (unused :: cnt)
>  evalv $ app3 c_strncpy_ (app from_strbuf_ y) x (int $ succ n)
>  c <- eval $ idx (app unwrap_ptr_ y) (int n)
>  return $ app3 if_ (load c `eq` char '\0')
>    true_
>    (lift (eval (store c (char '\0')) >> return false_))