Merge branch 'unscheme' into master

libs/base/Data/Strings.idr

@@ -16,11 +16,21 @@ partial
 foldl1 : (a -> a -> a) -> List a -> a
 foldl1 f (x::xs) = foldl f x xs
 
+-- This function runs fast when compiled but won't compute at compile time.
+-- If you need to unpack strings at compile time, use Prelude.unpack.
+%foreign
+  "scheme:string-unpack"
+export
+fastUnpack : String -> List Char
+
 -- This works quickly because when string-concat builds the result, it allocates
 -- enough room in advance so there's only one allocation, rather than lots!
+--
+-- Like fastUnpack, this function won't reduce at compile time.
+-- If you need to concatenate strings at compile time, use Prelude.concat.
 %foreign
-    "scheme:string-concat"
-    "javascript:lambda:(xs)=>''.concat(...__prim_idris2js_array(xs))"
+  "scheme:string-concat"
+  "javascript:lambda:(xs)=>''.concat(...__prim_idris2js_array(xs))"
 export
 fastConcat : List String -> String
 

libs/contrib/Data/List/Lazy.idr

@@ -0,0 +1,55 @@
+module Data.List.Lazy
+
+%default total
+
+-- All functions here are public export
+-- because their definitions are pretty much the specification.
+
+public export
+data LazyList : Type -> Type where
+  Nil : LazyList a
+  (::) : (1 x : a) -> (1 xs : Lazy (LazyList a)) -> LazyList a
+
+public export
+Semigroup (LazyList a) where
+  [] <+> ys = ys
+  (x :: xs) <+> ys = x :: (xs <+> ys)
+
+public export
+Monoid (LazyList a) where
+  neutral = []
+
+public export
+Foldable LazyList where
+  foldr op nil [] = nil
+  foldr op nil (x :: xs) = x `op` foldr op nil xs
+
+  foldl op acc [] = acc
+  foldl op acc (x :: xs) = foldl op (acc `op` x) xs
+
+public export
+Functor LazyList where
+  map f [] = []
+  map f (x :: xs) = f x :: map f xs
+
+public export
+Applicative LazyList where
+  pure x = [x]
+  fs <*> vs = concatMap (\f => map f vs) fs
+
+public export
+Alternative LazyList where
+  empty = []
+  (<|>) = (<+>)
+
+public export
+Monad LazyList where
+  m >>= f = concatMap f m
+
+-- There is no Traversable instance for lazy lists.
+-- The result of a traversal will be a non-lazy list in general
+-- (you can't delay the "effect" of an applicative functor).
+public export
+traverse : Applicative f => (a -> f b) -> LazyList a -> f (List b)
+traverse g [] = pure []
+traverse g (x :: xs) = [| g x :: traverse g xs |]

libs/contrib/Data/SortedSet.idr

@@ -65,3 +65,11 @@ Ord k => Monoid (SortedSet k) where
 export
 keySet : SortedMap k v -> SortedSet k
 keySet = SetWrapper . map (const ())
+
+export
+singleton : Ord k => k -> SortedSet k
+singleton k = insert k empty
+
+export
+null : SortedSet k -> Bool
+null (SetWrapper m) = SortedMap.null m

libs/contrib/Data/String/Iterator.idr

@@ -0,0 +1,74 @@
+module Data.String.Iterator
+
+import public Data.List.Lazy
+
+%default total
+
+-- Backend-dependent string iteration type,
+-- parameterised by the string that it iterates over.
+--
+-- Beware: the index is checked only up to definitional equality.
+-- In theory, you could run `decEq` on two strings
+-- with the same content but allocated in different memory locations
+-- and use the obtained Refl to coerce iterators between them.
+--
+-- The strictly correct solution is to make the iterators independent
+-- from the exact memory location of the string given to `uncons`.
+-- (For example, byte offsets satisfy this requirement.)
+export
+data StringIterator : String -> Type where [external]
+
+-- This function is private
+-- to avoid subverting the linearity guarantees of withString.
+%foreign
+  "scheme:blodwen-string-iterator-new"
+  "javascript:stringIterator:new"
+private
+fromString : (str : String) -> StringIterator str
+
+-- This function uses a linear string iterator
+-- so that backends can use mutating iterators.
+export
+withString : (str : String) -> ((1 it : StringIterator str) -> a) -> a
+withString str f = f (fromString str)
+
+-- We use a custom data type instead of Maybe (Char, StringIterator)
+-- to remove one level of pointer indirection
+-- in every iteration of something that's likely to be a hot loop,
+-- and to avoid one allocation per character.
+--
+-- The Char field of Character is unrestricted for flexibility.
+public export
+data UnconsResult : String -> Type where
+  EOF : UnconsResult str
+  Character : (c : Char) -> (1 it : StringIterator str) -> UnconsResult str
+
+-- We pass the whole string to the uncons function
+-- to avoid yet another allocation per character
+-- because for many backends, StringIterator can be simply an integer
+-- (e.g. byte offset into an UTF-8 string).
+%foreign
+  "scheme:blodwen-string-iterator-next"
+  "javascript:stringIterator:next"
+export
+uncons : (str : String) -> (1 it : StringIterator str) -> UnconsResult str
+
+export
+foldl : (accTy -> Char -> accTy) -> accTy -> String -> accTy
+foldl op acc str = withString str (loop acc)
+  where
+    loop : accTy -> (1 it : StringIterator str) -> accTy
+    loop acc it =
+      case uncons str it of
+        EOF => acc
+        Character c it' => loop (acc `op` c) (assert_smaller it it')
+
+export
+unpack : String -> LazyList Char
+unpack str = withString str unpack'
+  where
+    unpack' : (1 it : StringIterator str) -> LazyList Char
+    unpack' it =
+      case uncons str it of
+        EOF => []
+        Character c it' => c :: Delay (unpack' $ assert_smaller it it')

libs/contrib/Text/Lexer/Core.idr

@@ -199,13 +199,13 @@ tokenise pred line col acc tmap str
 export
 lex : TokenMap a -> String -> (List (TokenData a), (Int, Int, String))
 lex tmap str
-    = let (ts, (l, c, str')) = tokenise (const False) 0 0 [] tmap (unpack str) in
+    = let (ts, (l, c, str')) = tokenise (const False) 0 0 [] tmap (fastUnpack str) in
           (ts, (l, c, pack str'))
 
 export
 lexTo : (TokenData a -> Bool) ->
         TokenMap a -> String -> (List (TokenData a), (Int, Int, String))
 lexTo pred tmap str
-    = let (ts, (l, c, str')) = tokenise pred 0 0 [] tmap (unpack str) in
+    = let (ts, (l, c, str')) = tokenise pred 0 0 [] tmap (fastUnpack str) in
           (ts, (l, c, pack str'))
 

libs/contrib/contrib.ipkg

@@ -21,6 +21,7 @@ modules = Control.ANSI,
           Data.List.TailRec,
           Data.List.Equalities,
           Data.List.Reverse,
+          Data.List.Lazy,
           Data.List.Views.Extra,
           Data.List.Palindrome,
 
@@ -48,6 +49,7 @@ modules = Control.ANSI,
           Data.Stream.Extra,
           Data.String.Extra,
           Data.String.Interpolation,
+          Data.String.Iterator,
           Data.String.Parser,
           Data.String.Parser.Expression,
 

src/Compiler/ES/ES.idr

@@ -73,6 +73,28 @@ addSupportToPreamble : {auto c : Ref ESs ESSt} -> String -> String -> Core Strin
 addSupportToPreamble name code =
   addToPreamble name name code
 
+addStringIteratorToPreamble : {auto c : Ref ESs ESSt} -> Core String
+addStringIteratorToPreamble =
+  do
+    let defs = "
+function __prim_stringIteratorNew(str) {
+  return str[Symbol.iterator]();
+}
+function __prim_stringIteratorNext(str, it) {
+  const char = it.next();
+  if (char.done) {
+    return {h: 0}; // EOF
+  } else {
+    return {
+      h: 1, // Character
+      a1: char.value,
+      a2: it
+    };
+  }
+}"
+    let name = "stringIterator"
+    let newName = esName name
+    addToPreamble name newName defs
 
 jsIdent : String -> String
 jsIdent s = concatMap okchar (unpack s)
@@ -312,6 +334,13 @@ makeForeign n x =
           lib_code <- readDataFile ("js/" ++ lib ++ ".js")
           addSupportToPreamble lib lib_code
           pure $ "const " ++ jsName n ++ " = " ++ lib ++ "_" ++ name ++ "\n"
+      "stringIterator" =>
+        do
+          addStringIteratorToPreamble
+          case def of
+            "new" => pure $ "const " ++ jsName n ++ " = __prim_stringIteratorNew;\n"
+            "next" => pure $ "const " ++ jsName n ++ " = __prim_stringIteratorNext;\n"
+            _ => throw (InternalError $ "invalid string iterator function: " ++ def ++ ", supported functions are \"new\", \"next\"")
 
 
       _ => throw (InternalError $ "invalid foreign type : " ++ ty ++ ", supported types are \"lambda\", \"lambdaRequire\", \"support\"")

src/Core/Hash.idr

@@ -5,7 +5,9 @@ import Core.TT
 
 import Data.List
 import Data.List1
+import Data.List.Lazy
 import Data.Strings
+import Data.String.Iterator
 
 %default covering
 
@@ -56,15 +58,7 @@ Hashable a => Hashable (Maybe a) where
 
 export
 Hashable String where
-  hashWithSalt h str = hashChars h 0 (cast (length str)) str
-    where
-      hashChars : Int -> Int -> Int -> String -> Int
-      hashChars h p len str
-          = assert_total $
-              if p == len
-                 then h
-                 else hashChars (h * 33 + cast (strIndex str p))
-                                (p + 1) len str
+  hashWithSalt h = String.Iterator.foldl hashWithSalt h
 
 export
 Hashable Namespace where

src/Data/StringMap.idr

@@ -293,6 +293,13 @@ export
 mergeLeft : StringMap v -> StringMap v -> StringMap v
 mergeLeft x y = mergeWith const x y
 
+export
+adjust : String -> (v -> v) -> StringMap v -> StringMap v
+adjust k f m =
+  case lookup k m of
+    Nothing => m
+    Just v => insert k (f v) m
+
 export
 Show v => Show (StringMap v) where
   show m = show $ map {b=String} (\(k,v) => k ++ "->" ++ show v) $ toList m

src/Text/Lexer/Core.idr

@@ -171,12 +171,12 @@ tokenise pred line col acc tmap str
 export
 lex : TokenMap a -> String -> (List (WithBounds a), (Int, Int, String))
 lex tmap str
-    = let (ts, (l, c, str')) = tokenise (const False) 0 0 [] tmap (unpack str) in
+    = let (ts, (l, c, str')) = tokenise (const False) 0 0 [] tmap (fastUnpack str) in
           (ts, (l, c, fastPack str'))
 
 export
 lexTo : (WithBounds a -> Bool) ->
         TokenMap a -> String -> (List (WithBounds a), (Int, Int, String))
 lexTo pred tmap str
-    = let (ts, (l, c, str')) = tokenise pred 0 0 [] tmap (unpack str) in
+    = let (ts, (l, c, str')) = tokenise pred 0 0 [] tmap (fastUnpack str) in
           (ts, (l, c, fastPack str'))

support/c/Makefile

@@ -52,4 +52,7 @@ cleandep: clean
 
 install: build
 	mkdir -p ${PREFIX}/idris2-${IDRIS2_VERSION}/lib
-	install $(LIBTARGET) $(DYLIBTARGET) ${PREFIX}/idris2-${IDRIS2_VERSION}/lib
+	mkdir -p ${PREFIX}/idris2-${IDRIS2_VERSION}/include
+	install -m 755 $(DYLIBTARGET) ${PREFIX}/idris2-${IDRIS2_VERSION}/lib
+	install -m 644 $(LIBTARGET)   ${PREFIX}/idris2-${IDRIS2_VERSION}/lib
+	install -m 644 *.h            ${PREFIX}/idris2-${IDRIS2_VERSION}/include

support/c/idris_buffer.c

@@ -4,7 +4,7 @@
 
 typedef struct {
     int size;
-    uint8_t data[0];
+    uint8_t data[];
 } Buffer;
 
 void* idris2_newBuffer(int bytes) {
@@ -46,13 +46,17 @@ void idris2_setBufferByte(void* buffer, int loc, int byte) {
     }
 }
 
-void idris2_setBufferInt(void* buffer, int loc, int val) {
+void idris2_setBufferInt(void* buffer, int loc, int64_t val) {
     Buffer* b = buffer;
     if (loc >= 0 && loc+3 < b->size) {
-        b->data[loc] = val & 0xff;
-        b->data[loc+1] = (val >> 8) & 0xff;
+        b->data[loc  ] =  val        & 0xff;
+        b->data[loc+1] = (val >>  8) & 0xff;
         b->data[loc+2] = (val >> 16) & 0xff;
         b->data[loc+3] = (val >> 24) & 0xff;
+        b->data[loc+4] = (val >> 32) & 0xff;
+        b->data[loc+5] = (val >> 40) & 0xff;
+        b->data[loc+6] = (val >> 48) & 0xff;
+        b->data[loc+7] = (val >> 56) & 0xff;
     }
 }
 
@@ -77,7 +81,7 @@ void idris2_setBufferString(void* buffer, int loc, char* str) {
     }
 }
 
-int idris2_getBufferByte(void* buffer, int loc) {
+uint8_t idris2_getBufferByte(void* buffer, int loc) {
     Buffer* b = buffer;
     if (loc >= 0 && loc < b->size) {
         return b->data[loc];
@@ -86,13 +90,14 @@ int idris2_getBufferByte(void* buffer, int loc) {
     }
 }
 
-int idris2_getBufferInt(void* buffer, int loc) {
+int64_t idris2_getBufferInt(void* buffer, int loc) {
     Buffer* b = buffer;
-    if (loc >= 0 && loc+3 < b->size) {
-        return b->data[loc] +
-               (b->data[loc+1] << 8) +
-               (b->data[loc+2] << 16) +
-               (b->data[loc+3] << 24);
+    if (loc >= 0 && loc+7 < b->size) {
+        int64_t result = 0;
+        for (size_t i=0; i<8; i++) {
+            result |= b->data[loc + i] << (8 * i);
+        }
+        return result;
     } else {
         return 0;
     }
@@ -124,10 +129,10 @@ char* idris2_getBufferString(void* buffer, int loc, int len) {
     return rs;
 }
 
-int idris2_readBufferData(FILE* h, char* buffer, int loc, int max) {
+size_t idris2_readBufferData(FILE* h, char* buffer, size_t loc, size_t max) {
     return fread(buffer+loc, sizeof(uint8_t), (size_t)max, h);
 }
 
-int idris2_writeBufferData(FILE* h, char* buffer, int loc, int len) {
+size_t idris2_writeBufferData(FILE* h, const char* buffer, size_t loc, size_t len) {
     return fwrite(buffer+loc, sizeof(uint8_t), len, h);
 }