[ compat ] with current Idris

Author: gallais

Code/Lecture1/Core/Core.idr

@@ -56,6 +56,10 @@ export %inline
 map : (a -> b) -> Core a -> Core b
 map f (MkCore a) = MkCore (map (map f) a)
 
+export %inline
+ignore : Core a -> Core ()
+ignore = map (\ _ => ())
+
 export %inline
 (<$>) : (a -> b) -> Core a -> Core b
 (<$>) f (MkCore a) = MkCore (map (map f) a)
@@ -69,6 +73,11 @@ export %inline
                                Left err => pure (Left err)
                                Right val => runCore (f val)))
 
+-- Monad (specialised)
+export %inline
+(>>) : Core () -> Core b -> Core b
+ma >> mb = ma >>= \ () => mb
+
 -- Applicative (specialised)
 export %inline
 pure : a -> Core a
@@ -111,7 +120,7 @@ traverse f xs = traverse' f xs []
 
 export
 traverseList1 : (a -> Core b) -> List1 a -> Core (List1 b)
-traverseList1 f (x :: xs) = [| f x :: traverse f xs |]
+traverseList1 f (x ::: xs) = [| f x ::: traverse f xs |]
 
 export
 traverseVect : (a -> Core b) -> Vect n a -> Core (Vect n b)
@@ -124,15 +133,15 @@ traverseOpt f Nothing = pure Nothing
 traverseOpt f (Just x) = map Just (f x)
 
 export
-traverse_ : (a -> Core b) -> List a -> Core ()
+traverse_ : (a -> Core ()) -> List a -> Core ()
 traverse_ f [] = pure ()
 traverse_ f (x :: xs)
     = do f x
          traverse_ f xs
 
 export
-traverseList1_ : (a -> Core b) -> List1 a -> Core ()
-traverseList1_ f (x :: xs) = do
+traverseList1_ : (a -> Core ()) -> List1 a -> Core ()
+traverseList1_ f (x ::: xs) = do
   f x
   traverse_ f xs
 

Code/Lecture1/lecture1.ipkg

@@ -1,3 +1,14 @@
 package lecture1
 
 opts = "-p contrib"
+
+modules
+ = Ref
+ , Search
+ , QTT
+ , WarmupExercise.Ex2
+ , WarmupExercise.Ex1
+ , WarmupExercise.Ex3
+ , RLE
+ , Append
+ , Core.Core

Code/Lecture2/Core/TT.idr

@@ -152,7 +152,7 @@ nameAt : {vars : _} ->
 nameAt {vars = n :: ns} Z First = n
 nameAt {vars = n :: ns} (S k) (Later p) = nameAt k p
 
-export 
+export
 {vars : _} -> Show (Term vars) where
   show tm = let (fn, args) = getFnArgs tm in showApp fn args
     where

Code/Lecture2/lecture2.ipkg

@@ -1,3 +1,10 @@
 package lecture1
 
 opts = "-p contrib"
+
+
+modules
+ = Ref
+ , Core.CaseTree
+ , Core.TT
+ , Core.Core

Code/Lecture3/TinyIdris-v1/src/Core/Core.idr

@@ -98,6 +98,11 @@ export %inline
 map : (a -> b) -> Core a -> Core b
 map f (MkCore a) = MkCore (map (map f) a)
 
+-- Functor (specialised)
+export %inline
+ignore : Core a -> Core ()
+ignore = map (\ _ => ())
+
 export %inline
 (<$>) : (a -> b) -> Core a -> Core b
 (<$>) f (MkCore a) = MkCore (map (map f) a)
@@ -111,6 +116,11 @@ export %inline
                                Left err => pure (Left err)
                                Right val => runCore (f val)))
 
+-- Monad (specialised)
+export %inline
+(>>) : Core () -> Core b -> Core b
+ma >> mb = ma >>= \ () => mb
+
 -- Applicative (specialised)
 export %inline
 pure : a -> Core a
@@ -153,7 +163,7 @@ traverse f xs = traverse' f xs []
 
 export
 traverseList1 : (a -> Core b) -> List1 a -> Core (List1 b)
-traverseList1 f (x :: xs) = [| f x :: traverse f xs |]
+traverseList1 f (x ::: xs) = [| f x ::: traverse f xs |]
 
 export
 traverseVect : (a -> Core b) -> Vect n a -> Core (Vect n b)
@@ -166,15 +176,15 @@ traverseOpt f Nothing = pure Nothing
 traverseOpt f (Just x) = map Just (f x)
 
 export
-traverse_ : (a -> Core b) -> List a -> Core ()
+traverse_ : (a -> Core ()) -> List a -> Core ()
 traverse_ f [] = pure ()
 traverse_ f (x :: xs)
     = do f x
          traverse_ f xs
 
 export
-traverseList1_ : (a -> Core b) -> List1 a -> Core ()
-traverseList1_ f (x :: xs) = do
+traverseList1_ : (a -> Core ()) -> List1 a -> Core ()
+traverseList1_ f (x ::: xs) = do
   f x
   traverse_ f xs
 

Code/Lecture3/TinyIdris-v1/src/Core/Env.idr

@@ -13,7 +13,7 @@ revOnto xs [] = Refl
 revOnto xs (v :: vs)
     = rewrite revOnto (v :: xs) vs in
         rewrite appendAssociative (reverse vs) [v] xs in
-				  rewrite revOnto [v] vs in Refl
+          rewrite revOnto [v] vs in Refl
 
 revNs : (vs, ns : List a) -> reverse ns ++ reverse vs = reverse (vs ++ ns)
 revNs [] ns = rewrite appendNilRightNeutral (reverse ns) in Refl

Code/Lecture3/TinyIdris-v1/src/Core/TT.idr

@@ -125,7 +125,7 @@ data Term : List Name -> Type where
      Erased : Term vars
 
 public export
-interface Weaken (tm : List Name -> Type) where
+interface Weaken (0 tm : List Name -> Type) where
   weaken : {n, vars : _} -> tm vars -> tm (n :: vars)
   weakenNs : {vars : _} -> (ns : List Name) -> tm vars -> tm (ns ++ vars)
 
@@ -384,7 +384,7 @@ nameAt : {vars : _} ->
 nameAt {vars = n :: ns} Z First = n
 nameAt {vars = n :: ns} (S k) (Later p) = nameAt k p
 
-export 
+export
 {vars : _} -> Show (Term vars) where
   show tm = let (fn, args) = getFnArgs tm in showApp fn args
     where

Code/Lecture3/TinyIdris-v1/src/Parser/Lexer/Package.idr

@@ -27,7 +27,7 @@ Show Token where
   show (Comment str) = "Comment: " ++ str
   show EndOfInput = "EndOfInput"
   show Equals = "Equals"
-  show (DotSepIdent dsid) = "DotSepIdentifier: " ++ dotSep (List1.toList dsid)
+  show (DotSepIdent dsid) = "DotSepIdentifier: " ++ dotSep (forget dsid)
   show Separator = "Separator"
   show Space = "Space"
   show (StringLit s) = "StringLit: " ++ s

Code/Lecture3/TinyIdris-v1/src/Parser/Lexer/Source.idr

@@ -46,7 +46,7 @@ Show Token where
   -- Identifiers
   show (HoleIdent x) = "hole identifier " ++ x
   show (Ident x) = "identifier " ++ x
-  show (DotSepIdent xs) = "namespaced identifier " ++ dotSep (List1.toList $ reverse xs)
+  show (DotSepIdent xs) = "namespaced identifier " ++ dotSep (forget $ reverse xs)
   show (DotIdent x) = "dot+identifier " ++ x
   show (Symbol x) = "symbol " ++ x
   -- Comments
@@ -222,7 +222,7 @@ rawTokens =
                    else Ident x
     parseNamespace : String -> Token
     parseNamespace ns = case List1.reverse . split (== '.') $ ns of
-                             [ident] => parseIdent ident
+                             (ident ::: []) => parseIdent ident
                              ns      => DotSepIdent ns
 
 export

Code/Lecture3/TinyIdris-v1/src/Parser/Rule/Package.idr

@@ -34,7 +34,7 @@ export
 exactProperty : String -> Rule String
 exactProperty p = terminal ("Expected property " ++ p)
                            (\x => case tok x of
-                                       DotSepIdent [p'] =>
+                                       DotSepIdent (p' ::: []) =>
                                          if p == p' then Just p
                                          else Nothing
                                        _ => Nothing)
@@ -64,7 +64,7 @@ export
 packageName : Rule String
 packageName = terminal "Expected package name"
                        (\x => case tok x of
-                                   DotSepIdent [str] =>
+                                   DotSepIdent (str ::: []) =>
                                      if isIdent AllowDashes str then Just str
                                      else Nothing
                                    _ => Nothing)

Code/Lecture3/TinyIdris-v1/src/Parser/Rule/Source.idr

@@ -124,7 +124,7 @@ namespacedIdent
     = terminal "Expected namespaced name"
         (\x => case tok x of
             DotSepIdent ns => Just ns
-            Ident i => Just [i]
+            Ident i => Just (i ::: [])
             _ => Nothing)
 
 export
@@ -133,7 +133,7 @@ moduleIdent
     = terminal "Expected module identifier"
         (\x => case tok x of
             DotSepIdent ns => Just ns
-            Ident i => Just [i]
+            Ident i => Just (i ::: [])
             _ => Nothing)
 
 export

Code/Lecture3/TinyIdris-v1/src/TTImp/Parser.idr

@@ -33,6 +33,8 @@ collectDefs : List ImpDecl -> List ImpDecl
 
 %hide Prelude.(>>=)
 %hide Core.Core.(>>=)
+%hide Prelude.(>>)
+%hide Core.Core.(>>)
 %hide Prelude.pure
 %hide Core.Core.pure
 

Code/Lecture3/TinyIdris-v1/src/Text/Literate.idr

@@ -26,6 +26,7 @@ module Text.Literate
 import Text.Lexer
 
 import Data.List
+import Data.List1
 import Data.List.Views
 import Data.Strings
 
@@ -68,7 +69,7 @@ reduce (MkToken _ _ _ _ (Any x) :: rest) acc = reduce rest (blank_content::acc)
   where
     -- Preserve the original document's line count.
     blank_content : String
-    blank_content = fastAppend (replicate (length (lines x)) "\n")
+    blank_content = fastAppend (replicate (length (forget $ lines x)) "\n")
 
 reduce (MkToken _ _ _ _ (CodeLine m src) :: rest) acc =
     if m == trim src
@@ -79,10 +80,9 @@ reduce (MkToken _ _ _ _ (CodeLine m src) :: rest) acc =
                       )::acc)
 
 reduce (MkToken _ _ _ _ (CodeBlock l r src) :: rest) acc with (lines src) -- Strip the deliminators surrounding the block.
-  reduce (MkToken _ _ _ _ (CodeBlock l r src) :: rest) acc | [] = reduce rest acc -- 1
-  reduce (MkToken _ _ _ _ (CodeBlock l r src) :: rest) acc | (s :: ys) with (snocList ys)
-    reduce (MkToken _ _ _ _ (CodeBlock l r src) :: rest) acc | (s :: []) | Empty = reduce rest acc -- 2
-    reduce (MkToken _ _ _ _ (CodeBlock l r src) :: rest) acc | (s :: (srcs ++ [f])) | (Snoc f srcs rec) =
+  reduce (MkToken _ _ _ _ (CodeBlock l r src) :: rest) acc | (s ::: ys) with (snocList ys)
+    reduce (MkToken _ _ _ _ (CodeBlock l r src) :: rest) acc | (s ::: []) | Empty = reduce rest acc -- 2
+    reduce (MkToken _ _ _ _ (CodeBlock l r src) :: rest) acc | (s ::: (srcs ++ [f])) | (Snoc f srcs rec) =
         reduce rest ("\n" :: unlines srcs :: acc)
 
 -- [ NOTE ] 1 & 2 shouldn't happen as code blocks are well formed i.e. have two deliminators.

Code/Lecture3/TinyIdris-v1/src/Text/Parser.idr

@@ -41,7 +41,7 @@ optional p = option Nothing (map Just p)
 ||| which option succeeded. If both would succeed, the left option
 ||| takes priority.
 export
-choose : {c1, c2 : Bool} -> 
+choose : {c1, c2 : Bool} ->
          (l : Grammar tok c1 a) ->
          (r : Grammar tok c2 b) ->
          Grammar tok (c1 && c2) (Either a b)
@@ -64,7 +64,7 @@ choiceMap {c} f xs = foldr (\x, acc => rewrite sym (andSameNeutral c) in
 ||| Try each grammar in a container until the first one succeeds.
 ||| Fails if the container is empty.
 export
-choice : Foldable t => 
+choice : Foldable t =>
          {c : Bool} ->
          t (Grammar tok c a) ->
          Grammar tok c a