[ close #1384 ] built-in Snoc-lists [< 1, 2, 3 ] (#1383)

Author: ohad

CHANGELOG.md

@@ -11,7 +11,8 @@ Library changes:
   command line options, to `contrib`.
 * Monad transformers in `Control.Monad` where restructured
   and several new transformer types where added.
-* `Data.Colist` and `Data.Colist1` where added to `base`.
+* `Data.Colist` and `Data.Colist1` were added to `base`.
+* Add `Data.SnocList` to base and `data SnocList` to `Prelude.Types`.
 * `Data.Bits`, an interface for bitwise operations, was added to `base`.
 * Interfaces `Bifoldable` and `Bitraversable` were added to the `prelude`.
 * Interface `Data.Contravariant` for contravariant functors was added
@@ -29,6 +30,8 @@ Syntax changes:
   implicit parameters and give multiplicities for parameters. The old syntax
   is still available for compatibility purposes but will be removed in the
   future.
+* Add support for SnocList syntax: `[< 1, 2, 3]` desugars into `Lin :< 1 :< 2 :< 3`
+  and their semantic highlighting.
 
 Compiler changes:
 

docs/source/tutorial/typesfuns.rst

@@ -737,13 +737,26 @@ Note that the constructor names are the same for each — constructor
 names (in fact, names in general) can be overloaded, provided that
 they are declared in different namespaces (see Section
 :ref:`sect-namespaces`), and will typically be resolved according to
-their type. As syntactic sugar, any type with the constructor names
+their type. As syntactic sugar, any implementation of the names
 ``Nil`` and ``::`` can be written in list form. For example:
 
 -  ``[]`` means ``Nil``
 
 -  ``[1,2,3]`` means ``1 :: 2 :: 3 :: Nil``
 
+Similarly, any implementation of the names ``Lin`` and ``:<`` can be
+written in **snoc**-list form:
+
+- ``[<]`` mean ``Lin``
+- ``[< 1, 2, 3]`` means ``Lin :< 1 :< 2 :< 3``.
+
+and the prelude includes a pre-defined datatype for snoc-lists:
+
+.. code-block:: idris
+
+    data SnocList a = Lin | (:<) (SnocList a) a
+
+
 The library also defines a number of functions for manipulating these
 types. ``map`` is overloaded both for ``List`` and ``Vect`` (we'll see more
 details of precisely how later when we cover interfaces in

libs/base/Data/SnocList.idr

@@ -0,0 +1,104 @@
+||| A Reversed List
+module Data.SnocList
+
+import Decidable.Equality
+import Data.List
+
+%default total
+
+infixl 7 <><
+infixr 6 <>>
+
+||| 'fish': Action of lists on snoc-lists
+public export
+(<><) : SnocList a -> List a -> SnocList a
+sx <>< [] = sx
+sx <>< (x :: xs) = sx :< x <>< xs
+
+||| 'chips': Action of snoc-lists on lists
+public export
+(<>>) : SnocList a -> List a -> List a
+Lin       <>> xs = xs
+(sx :< x) <>> xs = sx <>> x :: xs
+
+Cast (SnocList a) (List a) where
+  cast sx = sx <>> []
+
+Cast (List a) (SnocList a) where
+  cast xs = Lin <>< xs
+
+||| Transform to a list but keeping the contents in the spine order (term depth).
+public export
+asList : SnocList type -> List type
+asList = (reverse . cast)
+
+
+public export
+Eq a => Eq (SnocList a) where
+  (==) Lin Lin = True
+  (==) (sx :< x) (sy :< y) = x == y && sx == sy
+  (==) _ _ = False
+
+
+public export
+Ord a => Ord (SnocList a) where
+  compare Lin Lin = EQ
+  compare Lin (sx :< x) = LT
+  compare (sx :< x) Lin = GT
+  compare (sx :< x) (sy :< y)
+    = case compare sx sy of
+        EQ => compare x y
+        c  => c
+
+||| True iff input is Lin
+public export
+isLin : SnocList a -> Bool
+isLin Lin = True
+isLin (sx :< x) = False
+
+||| True iff input is (:<)
+public export
+isSnoc : SnocList a -> Bool
+isSnoc Lin     = False
+isSnoc (sx :< x) = True
+
+public export
+(++) : (sx, sy : SnocList a) -> SnocList a
+(++) sx Lin = sx
+(++) sx (sy :< y) = (sx ++ sy) :< y
+
+public export
+length : SnocList a -> Nat
+length Lin = Z
+length (sx :< x) = length sx + 1
+
+export
+Show a => Show (SnocList a) where
+  show xs = "[< " ++ show' "" xs ++ "]"
+    where
+      show' : String -> SnocList a -> String
+      show' acc Lin       = acc
+      show' acc (Lin :< x)= show x ++ acc
+      show' acc (xs :< x) = show' (", " ++ show x ++ acc) xs
+
+
+public export
+Functor SnocList where
+  map f Lin = Lin
+  map f (sx :< x) = (map f sx) :< (f x)
+
+
+public export
+Semigroup (SnocList a) where
+  (<+>) = (++)
+
+public export
+Monoid (SnocList a) where
+  neutral = Lin
+
+
+||| Check if something is a member of a list using the default Boolean equality.
+public export
+elem : Eq a => a -> SnocList a -> Bool
+elem x Lin = False
+elem x (sx :< y) = x == y || elem x sx

libs/base/base.ipkg

@@ -48,6 +48,7 @@ modules = Control.App,
           Data.IOArray.Prims,
           Data.IORef,
           Data.List,
+          Data.SnocList,
           Data.List.Elem,
           Data.List.Views,
           Data.List.Quantifiers,

libs/prelude/Prelude/Basics.idr

@@ -169,3 +169,14 @@ data List a =
   (::) a (List a)
 
 %name List xs, ys, zs
+
+||| Snoc lists.
+public export
+data SnocList a =
+  ||| Empty snoc-list
+  Lin
+
+  | ||| A non-empty snoc-list, consisting of the rest of the snoc-list and the final element.
+  (:<) (SnocList a) a
+
+%name SnocList sx, sy, sz

libs/prelude/Prelude/Ops.idr

@@ -11,6 +11,7 @@ infixr 4 ||
 
 -- List and String operators
 infixr 7 ::, ++
+infixl 7 :<
 
 -- Functor/Applicative/Monad/Algebra operators
 infixl 1 >>=, =<<, >>, >=>, <=<, <&>

src/Idris/Desugar.idr

@@ -353,6 +353,8 @@ mutual
            pure val
   desugarB side ps (PList fc nilFC args)
       = expandList side ps nilFC args
+  desugarB side ps (PSnocList fc nilFC args)
+      = expandSnocList side ps nilFC (reverse args)
   desugarB side ps (PPair fc l r)
       = do l' <- desugarB side ps l
            r' <- desugarB side ps r
@@ -448,6 +450,18 @@ mutual
       = pure $ apply (IVar consFC (UN "::"))
                 [!(desugarB side ps x), !(expandList side ps nilFC xs)]
 
+  expandSnocList
+             : {auto s : Ref Syn SyntaxInfo} ->
+               {auto b : Ref Bang BangData} ->
+               {auto c : Ref Ctxt Defs} ->
+               {auto u : Ref UST UState} ->
+               {auto m : Ref MD Metadata} ->
+               Side -> List Name -> (nilFC : FC) -> List (FC, PTerm) -> Core RawImp
+  expandSnocList side ps nilFC [] = pure (IVar nilFC (UN "Lin"))
+  expandSnocList side ps nilFC ((consFC, x) :: xs)
+      = pure $ apply (IVar consFC (UN ":<"))
+                [!(expandSnocList side ps nilFC xs) , !(desugarB side ps x)]
+
   addFromString : {auto c : Ref Ctxt Defs} ->
                   FC -> RawImp -> Core RawImp
   addFromString fc tm

src/Idris/DocString.idr

@@ -287,6 +287,7 @@ getDocsForPTerm (PPrimVal _ constant) = getDocsForPrimitive constant
 getDocsForPTerm (PType _) = pure ["Type : Type\n\tThe type of all types is Type. The type of Type is Type."]
 getDocsForPTerm (PString _ _) = pure ["String Literal\n\tDesugars to a fromString call"]
 getDocsForPTerm (PList _ _ _) = pure ["List Literal\n\tDesugars to (::) and Nil"]
+getDocsForPTerm (PSnocList _ _ _) = pure ["SnocList Literal\n\tDesugars to (:<) and Empty"]
 getDocsForPTerm (PPair _ _ _) = pure ["Pair Literal\n\tDesugars to MkPair or Pair"]
 getDocsForPTerm (PDPair _ _ _ _ _) = pure ["Dependant Pair Literal\n\tDesugars to MkDPair or DPair"]
 getDocsForPTerm (PUnit _) = pure ["Unit Literal\n\tDesugars to MkUnit or Unit"]

src/Idris/IDEMode/CaseSplit.idr

@@ -49,6 +49,7 @@ toStrUpdate (UN n, term)
     bracket : PTerm -> PTerm
     bracket tm@(PRef _ _) = tm
     bracket tm@(PList _ _ _) = tm
+    bracket tm@(PSnocList _ _ _) = tm
     bracket tm@(PPair _ _ _) = tm
     bracket tm@(PUnit _) = tm
     bracket tm@(PComprehension _ _ _) = tm

src/Idris/Parser.idr

@@ -384,7 +384,7 @@ mutual
            decorateKeywords fname xs
            pure (PRange fc (fst rstate) (snd rstate) y.val)
 
-  listExpr : FileName -> WithBounds t -> IndentInfo -> Rule PTerm
+  listExpr : FileName -> WithBounds () -> IndentInfo -> Rule PTerm
   listExpr fname s indents
       = do b <- bounds (do ret <- expr pnowith fname indents
                            decoratedSymbol fname "|"
@@ -407,6 +407,26 @@ mutual
                            nilFC = if null xs then fc else boundToFC fname b
                        in PList fc nilFC (map (\ t => (boundToFC fname t, t.val)) xs))
 
+  snocListExpr : FileName -> WithBounds () -> IndentInfo -> Rule PTerm
+  snocListExpr fname s indents
+      = {- TODO: comprehension -}
+        do mHeadTail <- optional $ do
+             hd <- many $ do x <- expr pdef fname indents
+                             b <- bounds (symbol ",")
+                             pure (x <$ b)
+             tl <- expr pdef fname indents
+             pure (hd, tl)
+           {- TODO: reverse ranges -}
+           b <- bounds (symbol "]")
+           pure $
+             let xs : List (WithBounds PTerm)
+                    = case mHeadTail of
+                        Nothing      => []
+                        Just (hd,tl) => hd ++ [ tl <$ b]
+                 fc = boundToFC fname (mergeBounds s b)
+                 nilFC = ifThenElse (null xs) fc (boundToFC fname s)
+             in PSnocList fc nilFC (map (\ t => (boundToFC fname t, t.val)) xs) --)
+
   nonEmptyTuple : FileName -> WithBounds t -> IndentInfo -> PTerm -> Rule PTerm
   nonEmptyTuple fname s indents e
       = do vals <- some $ do b <- bounds (symbol ",")
@@ -492,7 +512,9 @@ mutual
            pure (PUnquote (boundToFC fname b) b.val)
     <|> do start <- bounds (symbol "(")
            bracketedExpr fname start indents
-    <|> do start <- bounds (symbol "[")
+    <|> do start <- bounds (symbol "[<")
+           snocListExpr fname start indents
+    <|> do start <- bounds (symbol "[>" <|> symbol "[")
            listExpr fname start indents
     <|> do b <- bounds (decoratedSymbol fname "!" *> simpleExpr fname indents)
            pure (PBang (virtualiseFC $ boundToFC fname b) b.val)