mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-10-26 09:54:23 +03:00
Fix deprecation warnings in benchmarks
Most of this is from purification, two are switching from the %assert_total directive to the assert_total function.
This commit is contained in:
parent
5b2711f870
commit
938e8611e0
@ -31,7 +31,7 @@ splitAt' n s = let s' = unpack s in (pack $ take n s', pack $ drop n s')
|
||||
writeAlu : String -> String -> IO ()
|
||||
writeAlu name s0 = putStrLn name *> go s0
|
||||
where
|
||||
go "" = return ()
|
||||
go "" = pure ()
|
||||
go s = let (h,t) = splitAt' 60 s in putStrLn h *> go t
|
||||
|
||||
replicate : Int -> Char -> String
|
||||
@ -64,7 +64,7 @@ make name n0 tbl seed0 = do
|
||||
lookupTable = Foldable.concat (fill (scanl accum ('a',0) tbl) 0)
|
||||
|
||||
make' : Int -> Int -> Int -> String -> IO Int
|
||||
make' 0 col seed buf = when (col > 0) (putStrLn buf) *> return seed
|
||||
make' 0 col seed buf = when (col > 0) (putStrLn buf) *> pure seed
|
||||
make' n col seed buf = do
|
||||
let newseed = modInt (seed * 3877 + 29573) modulus
|
||||
let nextchar = strIndex lookupTable newseed
|
||||
@ -80,4 +80,4 @@ main = do
|
||||
writeAlu ">ONE Homo sapiens alu" (takeRepeat (fromInteger (cast n)*2) alu)
|
||||
nseed <- make ">TWO IUB ambiguity codes" (fromInteger (cast n)*3) iub 42
|
||||
make ">THREE Homo sapiens frequency" (fromInteger (cast n)*5) homosapiens nseed
|
||||
return ()
|
||||
pure ()
|
||||
|
@ -46,7 +46,7 @@ pidigit = do
|
||||
let n = fromIntegerNat (the Integer (cast a))
|
||||
let l = str (MkF 1 0 1) 1 n
|
||||
loop 10 0 l
|
||||
return ()
|
||||
pure ()
|
||||
|
||||
main : IO ()
|
||||
main = pidigit
|
||||
|
@ -14,24 +14,24 @@ Parser : Nat -> Type
|
||||
Parser n = Either ParseErr (b : Board n ** LegalBoard b)
|
||||
|
||||
mapM : Monad m => (a -> m b) -> Vect n a -> m (Vect n b)
|
||||
mapM _ Nil = return Vect.Nil
|
||||
mapM _ Nil = pure Vect.Nil
|
||||
mapM f (x::xs) = do
|
||||
x' <- f x
|
||||
xs' <- mapM f xs
|
||||
return (Vect.(::) x' xs')
|
||||
pure (Vect.(::) x' xs')
|
||||
|
||||
parseToken : String -> Either String (Cell n)
|
||||
parseToken "." = return Nothing
|
||||
parseToken "." = pure Nothing
|
||||
parseToken "0" = Left "Got cell 0, expected 1-based numbering"
|
||||
parseToken x = map Just (tryParseFin ((cast x) - 1))
|
||||
where
|
||||
tryParseFin : Int -> Either String (Fin n)
|
||||
tryParseFin {n=Z} _ = Left ("Given cell " ++ x ++ " out of range")
|
||||
tryParseFin {n=S k} 0 = return FZ
|
||||
tryParseFin {n=S k} 0 = pure FZ
|
||||
tryParseFin {n=S k} x =
|
||||
case tryParseFin {n=k} (x-1) of
|
||||
Left err => Left err
|
||||
Right fin => return (FS fin)
|
||||
Right fin => pure (FS fin)
|
||||
|
||||
length : Vect n a -> Nat
|
||||
length {n=n} _ = n
|
||||
@ -45,7 +45,7 @@ parseCols {n=S k} row l cs = helper last l
|
||||
let here = (x, row) -- TODO: Determine why naming this makes idris smarter
|
||||
tok <- parseToken {n=S k} (index x cs)
|
||||
case tok of
|
||||
Nothing => return (_ ** l)
|
||||
Nothing => pure (_ ** l)
|
||||
Just t =>
|
||||
case legalVal b here t of
|
||||
Yes prf => Right (_ ** Step prf l)
|
||||
@ -79,4 +79,4 @@ parse str =
|
||||
let rows = fromList (lines str) in
|
||||
case parseRows {n=length rows} emptyBoard Base rows of
|
||||
Left msg => Left msg
|
||||
Right board => return (_ ** board)
|
||||
Right board => pure (_ ** board)
|
||||
|
@ -184,9 +184,8 @@ fillBoard {n=(S n)} b l with (emptyCell b)
|
||||
| Left full = Just (b ** (l, full))
|
||||
| Right (coords ** p) = recurse last
|
||||
where
|
||||
%assert_total
|
||||
tryAll : (v : Fin (S n)) -> (Fin (S n), Maybe (b' : Board (S n) ** LegalBoard b'))
|
||||
tryAll v = --trace ("Trying " ++ show (the Int (cast v))) $
|
||||
tryAll v = assert_total $ --trace ("Trying " ++ show (the Int (cast v))) $
|
||||
case tryValue l coords p v of
|
||||
Right success => (v, Just success)
|
||||
Left _ => -- TODO: Prove unsolvable
|
||||
@ -194,9 +193,8 @@ fillBoard {n=(S n)} b l with (emptyCell b)
|
||||
FS k => tryAll (weaken k)
|
||||
FZ => (v, Nothing)
|
||||
|
||||
%assert_total
|
||||
recurse : Fin (S n) -> Maybe (b' : Board (S n) ** CompleteBoard b')
|
||||
recurse start =
|
||||
recurse start = assert_total $
|
||||
case tryAll start of
|
||||
(_, Nothing) => Nothing
|
||||
(FZ, Just (b' ** l')) => fillBoard b' l'
|
||||
|
@ -15,8 +15,8 @@ vsort [] = []
|
||||
vsort (x :: xs) = insert x (vsort xs)
|
||||
|
||||
mkSortVec : (n : Nat) -> Eff (Vect n Int) [RND]
|
||||
mkSortVec Z = return []
|
||||
mkSortVec (S k) = return (fromInteger !(rndInt 0 10000) :: !(mkSortVec k))
|
||||
mkSortVec Z = pure []
|
||||
mkSortVec (S k) = pure (fromInteger !(rndInt 0 10000) :: !(mkSortVec k))
|
||||
|
||||
main : IO ()
|
||||
main = do (_ :: arg :: _) <- getArgs
|
||||
|
Loading…
Reference in New Issue
Block a user