ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-09-22 06:29:37 +03:00
Code Issues Projects Releases Wiki Activity

Merge branch 'master' into wip/tactical

Browse Source
This commit is contained in:
David Raymond Christiansen 2015-03-02 14:02:33 +01:00
commit 20e602829a
59 changed files with 391 additions and 240 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
.travis.yml
View File

@ -1,4 +1,10 @@
language: haskell
ghc:
# Idris won't build on 7.4 and earlier due to dependency
# problems. 7.10 isn't yet supported on Travis.
- 7.6
- 7.8
before_install:
- sudo add-apt-repository --yes ppa:h-rayflood/llvm
- sudo apt-get update -qq

13
CHANGELOG
View File

@ -8,7 +8,18 @@ New in 0.9.17:
* Quasiquotation supports the generation of Language.Reflection.Raw terms
in addition to Language.Reflection.TT. Types are used for disambiguation,
defaulting to TT at the REPL.
* Library operators have been renamed for consistency with Haskell. In
particular, Applicative.(<$>) is now Applicative.(<*>) and (<$>) is
now an alias for Functor.map. Correspondingly, ($>) and (<$) have
been renamed to (<*) and (*>). The cascading effects of this rename
are that Algebra.(<*>) has been renamed to Algebra.(<.>) and
Matrix.(<.>) is now Matrix.(<:>).
* Binding forms in DSL notation are now given an extra argument: a
reflected representation of the name that the user chose.
Specifically, the rewritten lambda, pi, and let binders will now get
an extra argument of type TTName. This allows more understandable
dynamic errors in DSL code and more readable code generation results.
New in 0.9.16:
--------------
* Inductive-inductive definitions are now supported (i.e. simultaneously

29
CITATION.md Normal file
View File

@ -0,0 +1,29 @@
# Citing `Idris`
If you use `Idris` in your work we would prefer it if you would use the following reference in your work.
## BibTeX
```bibtex
@article{JFP:9060502,
author = {BRADY,EDWIN},
title = {Idris, a general-purpose dependently typed programming language: Design and implementation},
journal = {Journal of Functional Programming},
volume = {23},
issue = {05},
month = {9},
year = {2013},
issn = {1469-7653},
pages = {552--593},
numpages = {42},
doi = {10.1017/S095679681300018X},
URL = {http://journals.cambridge.org/article_S095679681300018X},
}
```
## Textual
EDWIN BRADY (2013). Idris, a general-purpose dependently typed
programming language: Design and implementation. Journal of
Functional Programming, 23, pp
552-593. doi:10.1017/S095679681300018X.

5
contribs/lib/SQLite3/Makefile
View File

@ -7,10 +7,9 @@ sqltest : testunit.idr Sqlite3.idr sqlite3api.o
idris testunit.idr -o sqltest
sqlite3api.o : sqlite3api.c
gcc -c sqlite3api.c
gcc -I . -c sqlite3api.c
sqlite3api.so: sqlite3api.c
gcc -fPIC -o sqlite3api.so -shared sqlite3api.c
gcc -I . -fPIC -o sqlite3api.so -shared sqlite3api.c
all : sqltest sqlite3api.o

92
contribs/lib/SQLite3/Sqlite3.idr
View File

@ -1,8 +1,9 @@
module Sqlite3
import Sqlexpr
import public Sqlexpr
%lib C "sqlite3"
-- %link C "sqlite3.o"
-- %include C "sqlite3.h"
%link C "sqlite3api.o"
%include C "sqlite3api.h"
@ -47,7 +48,7 @@ instance Functor DB where
instance Applicative DB where
pure = MkDB . return . Right
(MkDB f) <$> (MkDB x) = MkDB (do f' <- f
(MkDB f) <*> (MkDB x) = MkDB (do f' <- f
case f' of
Left err => return (Left err)
Right op => x >>= (return . map op))
@ -59,7 +60,7 @@ instance Monad DB where
Left err => return (Left err)
Right v => case k v of
MkDB k' => k')
return x = MkDB (return (Right x))
--return x = MkDB (return (Right x))
fail : String -> DB a
fail err = MkDB (return (Left err))
@ -83,7 +84,7 @@ runDB (MkDB f) = do f' <- f
-----------------------------------------------------------------------------
open_db : String -> DB DBPointer
open_db name = do x <- liftIO (mkForeign (FFun "sqlite3_open_idr" [FString] FPtr) name)
open_db name = do x <- liftIO (foreign FFI_C "sqlite3_open_idr" (String -> IO Ptr) name)
return (MkDBPointer x)
-----------------------------------------------------------------------------
@ -91,7 +92,7 @@ open_db name = do x <- liftIO (mkForeign (FFun "sqlite3_open_idr" [FString] FPtr
-----------------------------------------------------------------------------
close_db : DBPointer -> DB Int
close_db (MkDBPointer pointer) = liftIO (mkForeign (FFun "sqlite3_close_idr" [FPtr] FInt) pointer)
close_db (MkDBPointer pointer) = liftIO (foreign FFI_C "sqlite3_close_idr" (Ptr -> IO Int) pointer)
-----------------------------------------------------------------------------
-- | Wrapper around prepare, step and finalize.
@ -99,7 +100,7 @@ close_db (MkDBPointer pointer) = liftIO (mkForeign (FFun "sqlite3_close_idr" [FP
exec_db : DBPointer -> String -> DB Int
exec_db (MkDBPointer pointer) stmt = do
x <- liftIO (mkForeign (FFun "sqlite3_exec_idr" [FPtr, FString] FInt) pointer stmt)
x <- liftIO (foreign FFI_C "sqlite3_exec_idr" (Ptr -> String -> IO Int) pointer stmt)
if (x == 1)
then fail "Could not execute."
else return x
@ -110,7 +111,7 @@ exec_db (MkDBPointer pointer) stmt = do
exec_db_v2 : StmtPtr -> DB Int
exec_db_v2 (MkStmtPtr pointer) = do
x <- liftIO (mkForeign (FFun "exec_db" [FPtr] FInt) pointer)
x <- liftIO (foreign FFI_C "exec_db" (Ptr -> IO Int) pointer)
if (x == 21)
then fail "No data returned."
else return x
@ -122,8 +123,7 @@ exec_db_v2 (MkStmtPtr pointer) = do
-----------------------------------------------------------------------------
get_error : DBPointer -> IO String
get_error (MkDBPointer pointer) = mkForeign (FFun "sqlite3_get_error" [FPtr] FString) pointer
get_error (MkDBPointer pointer) = foreign FFI_C "sqlite3_get_error" (Ptr -> IO String) pointer
-----------------------------------------------------------------------------
-- | Compiles the query inot a byte-code program in order to execute it.
@ -133,7 +133,7 @@ get_error (MkDBPointer pointer) = mkForeign (FFun "sqlite3_get_error" [FPtr] FSt
prepare_db : DBPointer -> String -> DB StmtPtr
prepare_db (MkDBPointer pointer) cmd = do
result <- liftIO (mkForeign (FFun "sqlite3_prepare_idr" [FPtr, FString] FPtr) pointer cmd)
result <- liftIO (foreign FFI_C "sqlite3_prepare_idr" (Ptr -> String -> IO Ptr) pointer cmd)
flag <- liftIO (nullPtr result)
if flag
then fail "Error occured while preparing"
@ -147,8 +147,8 @@ prepare_db (MkDBPointer pointer) cmd = do
step_db : StmtPtr -> DB Int
step_db (MkStmtPtr pointer)= do
x <- liftIO (mkForeign (FFun "sqlite3_step_idr" [FPtr] FInt)pointer)
if ( x == 101)
x <- liftIO (foreign FFI_C "sqlite3_step_idr" (Ptr -> IO Int) pointer)
if (x == 101)
then fail "SQLITE_DONE"
else return x
@ -159,7 +159,7 @@ step_db (MkStmtPtr pointer)= do
finalize_db : StmtPtr -> DB Int
finalize_db (MkStmtPtr pointer) = do
x <- liftIO (mkForeign (FFun "sqlite3_finalize_idr" [FPtr] FInt) pointer)
x <- liftIO (foreign FFI_C "sqlite3_finalize_idr" (Ptr -> IO Int) pointer)
if (x /= 0)
then fail "Could not finalize"
else return x
@ -170,7 +170,7 @@ finalize_db (MkStmtPtr pointer) = do
reset_db : StmtPtr -> DB Int
reset_db (MkStmtPtr pointer) = do
x <- liftIO (mkForeign (FFun "sqlite3_reset_idr" [FPtr] FInt) pointer)
x <- liftIO (foreign FFI_C "sqlite3_reset_idr" (Ptr -> IO Int) pointer)
if (x /= 0)
then fail "Could not reset"
else return x
@ -181,38 +181,34 @@ reset_db (MkStmtPtr pointer) = do
column_count : DBPointer -> IO (Either String Int)
column_count (MkDBPointer pointer) = do
x <- mkForeign (FFun "sqlite3_column_count_idr" [FPtr] FInt) pointer
return $ if (x == 0 )
x <- foreign FFI_C "sqlite3_column_count_idr" (Ptr -> IO Int) pointer
return $ if (x == 0)
then Left "No Data"
else (Right x)
column_name : DBPointer -> Int -> IO String
column_name (MkDBPointer pointer) iCol =
mkForeign (FFun "sqlite3_column_name_idr" [FPtr, FInt] FString) pointer iCol
foreign FFI_C "sqlite3_column_name_idr" (Ptr -> Int -> IO String) pointer iCol
column_decltype : DBPointer -> Int -> IO String
column_decltype (MkDBPointer pointer) iCol =
mkForeign (FFun "sqlite3_column_decltype_idr" [FPtr, FInt] FString) pointer iCol
foreign FFI_C "sqlite3_column_decltype_idr" (Ptr -> Int -> IO String) pointer iCol
column_bytes : DBPointer -> Int -> IO Int
column_bytes (MkDBPointer pointer) iCol =
mkForeign (FFun "sqlite3_column_bytes_idr" [FPtr, FInt] FInt) pointer iCol
foreign FFI_C "sqlite3_column_bytes_idr" (Ptr -> Int -> IO Int) pointer iCol
column_blob : DBPointer -> Int -> IO String
column_blob (MkDBPointer pointer) iCol =
mkForeign (FFun "sqlite3_column_bytes_idr" [FPtr, FInt] FString) pointer iCol
foreign FFI_C "sqlite3_column_bytes_idr" (Ptr -> Int -> IO String) pointer iCol
column_text : DBPointer -> Int -> IO String
column_text (MkDBPointer pointer) iCol =
mkForeign (FFun "sqlite3_column_text_idr" [FPtr, FInt] FString) pointer iCol
foreign FFI_C "sqlite3_column_text_idr" (Ptr -> Int -> IO String) pointer iCol
column_Int : DBPointer -> Int -> IO Int
column_Int (MkDBPointer pointer) iCol =
mkForeign (FFun "sqlite3_column_int_idr" [FPtr, FInt] FInt) pointer iCol
foreign FFI_C "sqlite3_column_int_idr" (Ptr -> Int -> IO Int) pointer iCol
-----------------------------------------------------------------------------
-- | These routines support some of SQLite backup functions.
@ -220,22 +216,21 @@ column_Int (MkDBPointer pointer) iCol =
backup_init : DBPointer -> String -> DBPointer -> String -> IO DBPointer
backup_init (MkDBPointer des_pointer) destName (MkDBPointer src_pointer) srcName =
do x <- mkForeign (FFun "sqlite3_backup_init_idr" [FPtr,FString, FPtr, FString] FPtr)
do x <- foreign FFI_C "sqlite3_backup_init_idr" (Ptr -> String -> Ptr -> String -> IO Ptr)
des_pointer destName src_pointer srcName
return (MkDBPointer x)
backup_step : DBPointer -> Int -> IO Int
backup_step (MkDBPointer pointer) nPage =
mkForeign (FFun "sqlite3_backup_step_idr" [FPtr, FInt] FInt) pointer nPage
foreign FFI_C "sqlite3_backup_step_idr" (Ptr -> Int -> IO Int) pointer nPage
backup_finish : DBPointer -> IO Int
backup_finish (MkDBPointer pointer) =
mkForeign (FFun "sqlite3_backup_finish_idr" [FPtr] FInt) pointer
foreign FFI_C "sqlite3_backup_finish_idr" (Ptr -> IO Int) pointer
backup_remaining : DBPointer -> IO Int
backup_remaining (MkDBPointer pointer) =
mkForeign (FFun "sqlite3_backup_remaining_idr" [FPtr] FInt) pointer
foreign FFI_C "sqlite3_backup_remaining_idr" (Ptr -> IO Int) pointer
-----------------------------------------------------------------------------
-- | Use of this interface is not recommended.
@ -246,19 +241,18 @@ backup_remaining (MkDBPointer pointer) =
get_table : DBPointer -> String -> DB TBPointer
get_table (MkDBPointer pointer) name = do
x <- liftIO(mkForeign (FFun "sqlite3_get_table_idr" [FPtr, FString] FPtr) pointer name)
x <- liftIO(foreign FFI_C "sqlite3_get_table_idr" (Ptr -> String -> IO Ptr) pointer name)
flag <- liftIO (nullPtr x)
if flag
then do x <- liftIO(get_error_table pointer) ; fail x
else return (MkTBPointer x)
where
get_error_table : Ptr-> IO String
get_error_table pointer = do x <- mkForeign (FFun "sqlite3_get_error" [FPtr] FString) pointer
get_error_table pointer = do x <- foreign FFI_C "sqlite3_get_error" (Ptr -> IO String) pointer
return x
free_table : TBPointer -> IO ()
free_table (MkTBPointer pointer) = do x <- mkForeign (FFun "sqlite3_free_table_idr" [FPtr] FUnit) pointer
free_table (MkTBPointer pointer) = do x <- foreign FFI_C "sqlite3_free_table_idr" (Ptr -> IO ()) pointer
return ()
-----------------------------------------------------------------------------
@ -267,11 +261,11 @@ free_table (MkTBPointer pointer) = do x <- mkForeign (FFun "sqlite3_free_table_i
-----------------------------------------------------------------------------
num_row : TBPointer -> IO Int
num_row (MkTBPointer pointer) = do x <- mkForeign (FFun "sqlite3_get_num_row" [FPtr] FInt) pointer
num_row (MkTBPointer pointer) = do x <- foreign FFI_C "sqlite3_get_num_row" (Ptr -> IO Int) pointer
return x
num_col : TBPointer -> IO Int
num_col (MkTBPointer pointer) = do x <- mkForeign (FFun "sqlite3_get_num_col" [FPtr] FInt) pointer
num_col (MkTBPointer pointer) = do x <- foreign FFI_C "sqlite3_get_num_col" (Ptr -> IO Int) pointer
return x
-----------------------------------------------------------------------------
@ -280,11 +274,11 @@ num_col (MkTBPointer pointer) = do x <- mkForeign (FFun "sqlite3_get_num_col" [F
-----------------------------------------------------------------------------
num_row_v2 : DBPointer -> IO Int
num_row_v2 (MkDBPointer pointer) = do x <- mkForeign (FFun "sqlite3_get_num_row_v2" [FPtr] FInt) pointer
num_row_v2 (MkDBPointer pointer) = do x <- foreign FFI_C "sqlite3_get_num_row_v2" (Ptr -> IO Int) pointer
return x
num_col_v2 : DBPointer -> IO Int
num_col_v2 (MkDBPointer pointer) = do x <- mkForeign (FFun "sqlite3_get_num_col_v2" [FPtr] FInt) pointer
num_col_v2 (MkDBPointer pointer) = do x <- foreign FFI_C "sqlite3_get_num_col_v2" (Ptr -> IO Int) pointer
return x
-----------------------------------------------------------------------------
@ -299,18 +293,18 @@ get_data (MkDBPointer pointer) row col = do
helper ty
where get_data_type : Ptr ->Int -> Int -> IO Int
get_data_type pointer row col =
mkForeign (FFun "sqlite3_get_data_type" [FPtr, FInt, FInt] FInt) pointer row col
foreign FFI_C "sqlite3_get_data_type" (Ptr -> Int -> Int -> IO Int) pointer row col
get_data_val_int : Ptr -> Int -> IO Int
get_data_val_int pointer col =
mkForeign (FFun "sqlite3_get_val_int" [FPtr,FInt] FInt) pointer col
foreign FFI_C "sqlite3_get_val_int" (Ptr -> Int -> IO Int) pointer col
get_data_val_text : Ptr -> Int -> IO String
get_data_val_text pointer col =
mkForeign (FFun "sqlite3_get_val_text" [FPtr, FInt] FString) pointer col
foreign FFI_C "sqlite3_get_val_text" (Ptr -> Int -> IO String) pointer col
get_data_val_float : Ptr -> Int -> IO Float
get_data_val_float pointer col =
mkForeign (FFun "sqlite3_get_float" [FPtr, FInt] FFloat) pointer col
foreign FFI_C "sqlite3_get_float" (Ptr -> Int -> IO Float) pointer col
helper : Int -> IO DBVal
helper 1 = do i <- get_data_val_int pointer col ; return (DBInt i)
@ -360,7 +354,7 @@ strcat str1 str2 = str1 ++ str2
bind_int : StmtPtr -> Int -> Int -> DB StmtPtr
bind_int (MkStmtPtr pointer) indexval val = do
x <- liftIO (mkForeign (FFun "sqlite3_bind_int_idr" [FPtr, FInt, FInt] FPtr) pointer indexval val)
x <- liftIO (foreign FFI_C "sqlite3_bind_int_idr" (Ptr -> Int -> Int -> IO Ptr) pointer indexval val)
flag <- liftIO (nullPtr x)
if flag
then fail "Could not bind int."
@ -369,7 +363,7 @@ bind_int (MkStmtPtr pointer) indexval val = do
bind_float : StmtPtr -> Int -> Float -> DB StmtPtr
bind_float (MkStmtPtr pointer) indexval val = do
x <- liftIO (mkForeign (FFun "sqlite3_bind_float_idr" [FPtr, FInt, FFloat] FPtr) pointer indexval val)
x <- liftIO (foreign FFI_C "sqlite3_bind_float_idr" (Ptr -> Int -> Float -> IO Ptr) pointer indexval val)
flag <- liftIO (nullPtr x)
if flag
then fail "Could not bind float."
@ -377,7 +371,7 @@ bind_float (MkStmtPtr pointer) indexval val = do
bind_text : StmtPtr -> String -> Int -> Int -> DB StmtPtr
bind_text (MkStmtPtr pointer) text indexval lengthval = do
x <- liftIO (mkForeign (FFun "sqlite3_bind_text_idr" [FPtr, FString, FInt, FInt] FPtr)
x <- liftIO (foreign FFI_C "sqlite3_bind_text_idr" (Ptr -> String -> Int -> Int -> IO Ptr)
pointer text indexval lengthval)
flag <- liftIO(nullPtr x)
if flag
@ -386,7 +380,7 @@ bind_text (MkStmtPtr pointer) text indexval lengthval = do
bind_null : StmtPtr -> Int -> DB StmtPtr
bind_null (MkStmtPtr pointer) indexval = do
x <- liftIO (mkForeign (FFun "sqlite3_bind_null_idr" [FPtr, FInt] FPtr) pointer indexval)
x <- liftIO (foreign FFI_C "sqlite3_bind_null_idr" (Ptr -> Int -> IO Ptr) pointer indexval)
flag <- liftIO (nullPtr x)
if flag
then fail "Could not bind null."
@ -397,7 +391,7 @@ bind_null (MkStmtPtr pointer) indexval = do
-----------------------------------------------------------------------------
strlen : String -> DB Int
strlen str = liftIO (mkForeign (FFun "strLength" [FString] FInt) str)
strlen str = liftIO (foreign FFI_C "strLength" (String -> IO Int) str)
instance Show DBVal where
show (DBInt i) = "Int val: " ++ show i ++ "\n"

2
contribs/lib/SimpleParser/SimpleParser.idr
View File

@ -30,7 +30,7 @@ instance Functor Parser where
instance Applicative Parser where
pure v = P (\inp => Right (v, inp))
a <$> b = P (\inp => do (f, rest) <- parse a inp
a <*> b = P (\inp => do (f, rest) <- parse a inp
(x, rest') <- parse b rest
pure ((f x), rest'))

2
libs/base/Control/Arrow.idr
View File

@ -95,7 +95,7 @@ instance Arrow a => Functor (ArrowMonad a) where
instance Arrow a => Applicative (ArrowMonad a) where
pure x = MkArrowMonad $ arrow $ \_ => x
(MkArrowMonad f) <$> (MkArrowMonad x) = MkArrowMonad $ f &&& x >>> arrow (uncurry id)
(MkArrowMonad f) <*> (MkArrowMonad x) = MkArrowMonad $ f &&& x >>> arrow (uncurry id)
instance ArrowApply a => Monad (ArrowMonad a) where
(MkArrowMonad m) >>= f =

4
libs/base/Control/IOExcept.idr
View File

@ -10,8 +10,8 @@ instance Functor (IOExcept e) where
instance Applicative (IOExcept e) where
pure x = ioM (pure (pure x))
(ioM f) <$> (ioM a) = ioM (do f' <- f; a' <- a
return (f' <$> a'))
(ioM f) <*> (ioM a) = ioM (do f' <- f; a' <- a
return (f' <*> a'))
instance Monad (IOExcept e) where
(ioM x) >>= k = ioM (do x' <- x;

2
libs/base/Control/Monad/Identity.idr
View File

@ -9,7 +9,7 @@ instance Functor Identity where
instance Applicative Identity where
pure x = Id x
(Id f) <$> (Id g) = Id (f g)
(Id f) <*> (Id g) = Id (f g)
instance Monad Identity where
(Id x) >>= k = k x

2
libs/base/Control/Monad/RWS.idr
View File

@ -21,7 +21,7 @@ instance Monad m => Functor (RWST r w s m) where
instance (Monoid w, Monad m) => Applicative (RWST r w s m) where
pure a = MkRWST $ \_,s => return (a, s, neutral)
(MkRWST f) <$> (MkRWST v) = MkRWST $ \r,s => do (a, s', w) <- v r s
(MkRWST f) <*> (MkRWST v) = MkRWST $ \r,s => do (a, s', w) <- v r s
(fn, ss, w') <- f r s
return (fn a, ss, w <+> w)

2
libs/base/Control/Monad/Reader.idr
View File

@ -27,7 +27,7 @@ instance Functor f => Functor (ReaderT r f) where
instance Applicative m => Applicative (ReaderT r m) where
pure = liftReaderT . pure
(RD f) <$> (RD v) = RD $ \r => f r <$> v r
(RD f) <*> (RD v) = RD $ \r => f r <*> v r
instance Alternative m => Alternative (ReaderT r m) where
empty = liftReaderT empty

2
libs/base/Control/Monad/State.idr
View File

@ -25,7 +25,7 @@ instance Functor f => Functor (StateT s f) where
instance Monad f => Applicative (StateT s f) where
pure x = ST (\st => pure (x, st))
(ST f) <$> (ST a) = ST (\st => do (g, r) <- f st
(ST f) <*> (ST a) = ST (\st => do (g, r) <- f st
(b, t) <- a r
return (g b, t))

2
libs/base/Control/Monad/Writer.idr
View File

@ -25,7 +25,7 @@ instance Functor f => Functor (WriterT w f) where
instance (Monoid w, Applicative m) => Applicative (WriterT w m) where
pure a = WR $ pure (a, neutral)
(WR f) <$> (WR v) = WR $ liftA2 merge f v where
(WR f) <*> (WR v) = WR $ liftA2 merge f v where
merge (fn, w) (a, w') = (fn a, w <+> w')
instance (Monoid w, Alternative m) => Alternative (WriterT w m) where

2
libs/base/Data/Erased.idr
View File

@ -16,7 +16,7 @@ instance Functor Erased where
instance Applicative Erased where
pure = Erase
(<$>) (Erase f) (Erase x) = Erase (f x)
(<*>) (Erase f) (Erase x) = Erase (f x)
instance Monad Erased where
(>>=) (Erase x) f = f x

58
libs/base/Data/Matrix.idr
View File

@ -7,13 +7,13 @@ import Data.Vect
%default total
infixr 2 <.> -- vector inner product
infixr 2 <:> -- vector inner product
infixr 2 >< -- vector outer product
infixr 2 <<>> -- matrix commutator
infixr 2 >><< -- matrix anticommutator
infixl 3 <\> -- row times a matrix
infixr 4 </> -- matrix times a column
infixr 5 <> -- matrix multiplication
infixr 5 <> -- matrix multiplication
infixr 7 \&\ -- vector tensor product
infixr 7 <&> -- matrix tensor product
@ -26,14 +26,14 @@ instance Semigroup a => Semigroup (Vect n a) where
instance Monoid a => Monoid (Vect n a) where
neutral {n} = replicate n neutral
instance Group a => Group (Vect n a) where
inverse = map inverse
instance AbelianGroup a => AbelianGroup (Vect n a) where {}
instance Ring a => Ring (Vect n a) where
(<*>) v w = zipWith (<*>) v w
(<.>) v w = zipWith (<.>) v w
instance RingWithUnity a => RingWithUnity (Vect n a) where
unity {n} = replicate n unity
@ -42,7 +42,7 @@ instance Field a => Field (Vect n a) where
inverseM = map inverseM
instance RingWithUnity a => Module a (Vect n a) where
(<#>) r v = map (r <*>) v
(<#>) r v = map (r <.>) v
instance RingWithUnity a => Module a (Vect n (Vect l a)) where
(<#>) r m = map (r <#>) m
@ -53,12 +53,12 @@ instance RingWithUnity a => Module a (Vect n (Vect l a)) where
-----------------------------------------------------------------------
||| Inner product of ring vectors
(<.>) : Ring a => Vect n a -> Vect n a -> a
(<.>) w v = foldr (<+>) neutral (zipWith (<*>) w v)
(<:>) : Ring a => Vect n a -> Vect n a -> a
(<:>) w v = foldr (<+>) neutral (zipWith (<.>) w v)
||| Tensor multiply (⊗) ring vectors
(\&\) : Ring a => Vect n a -> Vect m a -> Vect (n * m) a
(\&\) {n} {m} v w = zipWith (<*>) (oextend m v) (orep n w) where
(\&\) {n} {m} v w = zipWith (<.>) (oextend m v) (orep n w) where
orep : (n : Nat) -> Vect m a -> Vect (n * m) a
orep n v = concat $ replicate n v
oextend : (n : Nat) -> Vect k a -> Vect (k * n) a
@ -90,15 +90,15 @@ indices f1 f2 m = index f2 (index f1 m)
||| Matrix times a column vector
(</>) : Ring a => Matrix n m a -> Vect m a -> Vect n a
(</>) m v = map (v <.>) m
(</>) m v = map (v <:>) m
||| Matrix times a row vector
(<\>) : Ring a => Vect n a -> Matrix n m a -> Vect m a
(<\>) r m = map (r <.>) $ transpose m
(<\>) r m = map (r <:>) $ transpose m
||| Matrix multiplication
(<>) : Ring a => Matrix n k a ->
Matrix k m a ->
(<>) : Ring a => Matrix n k a ->
Matrix k m a ->
Matrix n m a
(<>) m1 m2 = map (<\> m2) m1
@ -110,11 +110,11 @@ indices f1 f2 m = index f2 (index f1 m)
stepTwo : Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) w2 a
stepTwo {h1} m1 m2 = concat $ (Vect.replicate h1) m2
||| Cast a vector from a standard Vect to a proper n x 1 matrix
||| Cast a vector from a standard Vect to a proper n x 1 matrix
col : Vect n a -> Matrix n 1 a
col v = map (\x => [x]) v
||| Cast a row from a standard Vect to a proper 1 x n matrix
||| Cast a row from a standard Vect to a proper 1 x n matrix
row : Vect n a -> Matrix 1 n a
row r = [r]
@ -157,11 +157,11 @@ instance Monoid Integer where
instance Group Integer where
inverse = (* -1)
instance AbelianGroup Integer
instance Ring Integer where
(<*>) = (*)
instance Ring Integer where
(<.>) = (*)
instance RingWithUnity Integer where
unity = 1
@ -175,11 +175,11 @@ instance Monoid Int where
instance Group Int where
inverse = (* -1)
instance AbelianGroup Int
instance Ring Int where
(<*>) = (*)
instance Ring Int where
(<.>) = (*)
instance RingWithUnity Int where
unity = 1
@ -193,11 +193,11 @@ instance Monoid Float where
instance Group Float where
inverse = (* -1)
instance AbelianGroup Float
instance Ring Float where
(<*>) = (*)
instance Ring Float where
(<.>) = (*)
instance RingWithUnity Float where
unity = 1
@ -211,7 +211,7 @@ instance Semigroup Nat where
instance Monoid Nat where
neutral = 0
instance VerifiedSemigroup Nat where
semigroupOpIsAssociative = plusAssociative
@ -228,12 +228,12 @@ instance Monoid ZZ where
instance Group ZZ where
inverse = (* -1)
instance AbelianGroup ZZ
instance Ring ZZ where
(<*>) = (*)
instance Ring ZZ where
(<.>) = (*)
instance RingWithUnity ZZ where
unity = 1
@ -250,7 +250,7 @@ instance Group a => Group (Complex a) where
instance Ring a => AbelianGroup (Complex a) where {}
instance Ring a => Ring (Complex a) where
(<*>) (a :+ b) (c :+ d) = (a <*> c <-> b <*> d) :+ (a <*> d <+> b <*> c)
(<.>) (a :+ b) (c :+ d) = (a <.> c <-> b <.> d) :+ (a <.> d <+> b <.> c)
instance RingWithUnity a => RingWithUnity (Complex a) where
unity = (unity :+ neutral)

2
libs/base/Data/Morphisms.idr
View File

@ -25,7 +25,7 @@ instance Functor (Morphism r) where
instance Applicative (Morphism r) where
pure a = Mor $ const a
(Mor f) <$> (Mor a) = Mor $ \r => f r $ a r
(Mor f) <*> (Mor a) = Mor $ \r => f r $ a r
instance Monad (Morphism r) where
(Mor h) >>= f = Mor $ \r => applyMor (f $ h r) r

2
libs/base/Data/VectType.idr
View File

@ -529,7 +529,7 @@ transpose (x :: xs) = zipWith (::) x (transpose xs)
instance Applicative (Vect k) where
pure = replicate _
fs <$> vs = zipWith apply fs vs
fs <*> vs = zipWith apply fs vs
instance Monad (Vect n) where
m >>= f = diag (map f m)

2
libs/base/Network/Cgi.idr
View File

@ -36,7 +36,7 @@ instance Functor CGI where
instance Applicative CGI where
pure v = MkCGI (\s => return (v, s))
(MkCGI a) <$> (MkCGI b) = MkCGI (\s => do (f, i) <- a s
(MkCGI a) <*> (MkCGI b) = MkCGI (\s => do (f, i) <- a s
(c, j) <- b i
return (f c, j))

6
libs/base/Providers.idr
View File

@ -17,9 +17,9 @@ instance Functor Provider where
map f (Error err) = Error err
instance Applicative Provider where
(Provide f) <$> (Provide x) = Provide (f x)
(Provide f) <$> (Error err) = Error err
(Error err) <$> _ = Error err
(Provide f) <*> (Provide x) = Provide (f x)
(Provide f) <*> (Error err) = Error err
(Error err) <*> _ = Error err
pure = Provide
instance Monad Provider where

2
libs/base/System/Concurrency/Process.idr
View File

@ -19,7 +19,7 @@ instance Functor (Process msg) where
instance Applicative (Process msg) where
pure = Lift . return
(Lift f) <$> (Lift a) = Lift (f <$> a)
(Lift f) <*> (Lift a) = Lift (f <*> a)
instance Monad (Process msg) where
(Lift io) >>= k = Lift (do x <- io

24
libs/effects/Effect/Memory.idr
View File

@ -24,11 +24,11 @@ data RawMemory : Effect where
(size : Nat) ->
So (offset + size <= i) ->
RawMemory (Vect size Bits8)
(MemoryChunk n i) (\v => MemoryChunk n i)
(MemoryChunk n i) (\v => MemoryChunk n i)
Poke : (offset : Nat) ->
(Vect size Bits8) ->
So (offset <= i && offset + size <= n) ->
RawMemory () (MemoryChunk n i) (\v => MemoryChunk n (max i (offset + size)))
RawMemory () (MemoryChunk n i) (\v => MemoryChunk n (max i (offset + size)))
Move : (src : MemoryChunk src_size src_init) ->
(dst_offset : Nat) ->
(src_offset : Nat) ->
@ -36,8 +36,8 @@ data RawMemory : Effect where
So (dst_offset <= dst_init && dst_offset + size <= dst_size) ->
So (src_offset + size <= src_init) ->
RawMemory () (MemoryChunk dst_size dst_init)
(\v => MemoryChunk dst_size (max dst_init (dst_offset + size)))
GetRawPtr : RawMemory (MemoryChunk n i) (MemoryChunk n i) (\v => MemoryChunk n i)
(\v => MemoryChunk dst_size (max dst_init (dst_offset + size)))
GetRawPtr : RawMemory (MemoryChunk n i) (MemoryChunk n i) (\v => MemoryChunk n i)
private
do_malloc : Nat -> IOExcept String Ptr
@ -84,9 +84,9 @@ instance Handler RawMemory (IOExcept String) where
= do ptr <- do_malloc n
k () (CH ptr)
handle {-{res = MemoryChunk _ offset}-} (CH ptr) (Initialize {i} c size _) k
= ioe_lift (do_memset ptr i c size) $> k () (CH ptr)
= ioe_lift (do_memset ptr i c size) *> k () (CH ptr)
handle (CH ptr) (Free) k
= ioe_lift (do_free ptr) $> k () ()
= ioe_lift (do_free ptr) *> k () ()
handle (CH ptr) (Peek offset size _) k
= do res <- ioe_lift (do_peek ptr offset size)
k res (CH ptr)
@ -102,7 +102,7 @@ instance Handler RawMemory (IOExcept String) where
RAW_MEMORY : Type -> EFFECT
RAW_MEMORY t = MkEff t RawMemory
allocate : (n : Nat) ->
allocate : (n : Nat) ->
Eff () [RAW_MEMORY ()] (\v => [RAW_MEMORY (MemoryChunk n 0)])
allocate size = call $ Allocate size
@ -111,7 +111,7 @@ initialize : {i : Nat} ->
Bits8 ->
(size : Nat) ->
So (i + size <= n) ->
Eff () [RAW_MEMORY (MemoryChunk n i)]
Eff () [RAW_MEMORY (MemoryChunk n i)]
(\v => [RAW_MEMORY (MemoryChunk n (i + size))])
initialize c size prf = call $ Initialize c size prf
@ -122,7 +122,7 @@ peek : {i : Nat} ->
(offset : Nat) ->
(size : Nat) ->
So (offset + size <= i) ->
{ [RAW_MEMORY (MemoryChunk n i)] } Eff (Vect size Bits8)
{ [RAW_MEMORY (MemoryChunk n i)] } Eff (Vect size Bits8)
peek offset size prf = call $ Peek offset size prf
poke : {n : Nat} ->
@ -130,12 +130,12 @@ poke : {n : Nat} ->
(offset : Nat) ->
Vect size Bits8 ->
So (offset <= i && offset + size <= n) ->
Eff () [RAW_MEMORY (MemoryChunk n i)]
Eff () [RAW_MEMORY (MemoryChunk n i)]
(\v => [RAW_MEMORY (MemoryChunk n (max i (offset + size)))])
poke offset content prf = call $ Poke offset content prf
private
getRawPtr : { [RAW_MEMORY (MemoryChunk n i)] } Eff (MemoryChunk n i)
getRawPtr : { [RAW_MEMORY (MemoryChunk n i)] } Eff (MemoryChunk n i)
getRawPtr = call $ GetRawPtr
private
@ -173,5 +173,5 @@ move : {dst_size : Nat} ->
move dst_offset src_offset size dst_bounds src_bounds
= do src_ptr <- Src :- getRawPtr
Dst :- move' src_ptr dst_offset src_offset size dst_bounds src_bounds
return ()
return ()

2
libs/effects/Effect/Monad.idr
View File

@ -11,7 +11,7 @@ using (xs : List EFFECT, m : Type -> Type)
instance Applicative (\a => EffM m a xs (\v => xs)) where
pure = value
(<$>) f a = do f' <- f
(<*>) f a = do f' <- f
a' <- a
value (f' a')

6
libs/effects/Effects.idr
View File

@ -174,7 +174,7 @@ return x = value x
-- ------------------------------------------------------ [ for idiom brackets ]
infixl 2 <$>
infixl 2 <*>
pure : a -> Eff a xs (\v => xs)
pure = value
@ -182,9 +182,9 @@ pure = value
pureM : (val : a) -> Eff a (xs val) xs
pureM = value
(<$>) : Eff (a -> b) xs (\v => xs) ->
(<*>) : Eff (a -> b) xs (\v => xs) ->
Eff a xs (\v => xs) -> Eff b xs (\v => xs)
(<$>) prog v = do fn <- prog
(<*>) prog v = do fn <- prog
arg <- v
return (fn arg)

2
libs/oldeffects/Effect/Monad.idr
View File

@ -11,7 +11,7 @@ using (xs : List EFFECT, m : Type -> Type)
instance Applicative (\a => EffM m a xs (\v => xs)) where
pure = value
(<$>) f a = do f' <- f
(<*>) f a = do f' <- f
a' <- a
value (f' a')

6
libs/oldeffects/Effects.idr
View File

@ -185,16 +185,16 @@ return x = value x
-- ------------------------------------------------------ [ for idiom brackets ]
infixl 2 <$>
infixl 2 <*>
pure : a -> Eff m a xs (\v => xs)
pure = value
syntax pureM [val] = with_val val (pure ())
(<$>) : Eff m (a -> b) xs (\v => xs) ->
(<*>) : Eff m (a -> b) xs (\v => xs) ->
Eff m a xs (\v => xs) -> Eff m b xs (\v => xs)
(<$>) prog v = do fn <- prog
(<*>) prog v = do fn <- prog
arg <- v
return (fn arg)

2
libs/prelude/Language/Reflection/Tactical.idr
View File

@ -45,7 +45,7 @@ instance Functor Tactical where
instance Applicative Tactical where
pure x = prim__PureTactical x
f <$> x = prim__BindTactical f $ \g =>
f <*> x = prim__BindTactical f $ \g =>
prim__BindTactical x $ \y =>
prim__PureTactical $ g y

16
libs/prelude/Prelude.idr
View File

@ -249,31 +249,31 @@ instance Functor (Either e) where
instance Applicative PrimIO where
pure = prim_io_return
am <$> bm = prim_io_bind am (\f => prim_io_bind bm (prim_io_return . f))
am <*> bm = prim_io_bind am (\f => prim_io_bind bm (prim_io_return . f))
instance Applicative (IO' ffi) where
pure x = io_return x
f <$> a = io_bind f (\f' =>
f <*> a = io_bind f (\f' =>
io_bind a (\a' =>
io_return (f' a')))
instance Applicative Maybe where
pure = Just
(Just f) <$> (Just a) = Just (f a)
_ <$> _ = Nothing
(Just f) <*> (Just a) = Just (f a)
_ <*> _ = Nothing
instance Applicative (Either e) where
pure = Right
(Left a) <$> _ = Left a
(Right f) <$> (Right r) = Right (f r)
(Right _) <$> (Left l) = Left l
(Left a) <*> _ = Left a
(Right f) <*> (Right r) = Right (f r)
(Right _) <*> (Left l) = Left l
instance Applicative List where
pure x = [x]
fs <$> vs = concatMap (\f => map f vs) fs
fs <*> vs = concatMap (\f => map f vs) fs
---- Alternative instances

74
libs/prelude/Prelude/Algebra.idr
View File

@ -5,7 +5,7 @@ import Builtins
-- XXX: change?
infixl 6 <->
infixl 6 <+>
infixl 6 <*>
infixl 6 <.>
infixl 5 <#>
%access public
@ -96,18 +96,18 @@ class (VerifiedGroup a, AbelianGroup a) => VerifiedAbelianGroup a where
||| + Inverse for `<+>`:
||| forall a, a <+> inverse a == neutral
||| forall a, inverse a <+> a == neutral
||| + Associativity of `<*>`:
||| forall a b c, a <*> (b <*> c) == (a <*> b) <*> c
||| + Distributivity of `<*>` and `<->`:
||| forall a b c, a <*> (b <+> c) == (a <*> b) <+> (a <*> c)
||| forall a b c, (a <+> b) <*> c == (a <*> c) <+> (b <*> c)
||| + Associativity of `<.>`:
||| forall a b c, a <.> (b <.> c) == (a <.> b) <.> c
||| + Distributivity of `<.>` and `<->`:
||| forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)
||| forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)
class AbelianGroup a => Ring a where
(<*>) : a -> a -> a
(<.>) : a -> a -> a
class (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where
total ringOpIsAssociative : (l, c, r : a) -> l <*> (c <*> r) = (l <*> c) <*> r
total ringOpIsDistributiveL : (l, c, r : a) -> l <*> (c <+> r) = (l <*> c) <+> (l <*> r)
total ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <*> r = (l <*> r) <+> (c <*> r)
total ringOpIsAssociative : (l, c, r : a) -> l <.> (c <.> r) = (l <.> c) <.> r
total ringOpIsDistributiveL : (l, c, r : a) -> l <.> (c <+> r) = (l <.> c) <+> (l <.> r)
total ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <.> r = (l <.> r) <+> (c <.> r)
||| Sets equipped with two binary operations, one associative and commutative
||| supplied with a neutral element, and the other associative supplied with a
@ -124,20 +124,20 @@ class (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where
||| + Inverse for `<+>`:
||| forall a, a <+> inverse a == neutral
||| forall a, inverse a <+> a == neutral
||| + Associativity of `<*>`:
||| forall a b c, a <*> (b <*> c) == (a <*> b) <*> c
||| + Neutral for `<*>`:
||| forall a, a <*> unity == a
||| forall a, unity <*> a == a
||| + Distributivity of `<*>` and `<->`:
||| forall a b c, a <*> (b <+> c) == (a <*> b) <+> (a <*> c)
||| forall a b c, (a <+> b) <*> c == (a <*> c) <+> (b <*> c)
||| + Associativity of `<.>`:
||| forall a b c, a <.> (b <.> c) == (a <.> b) <.> c
||| + Neutral for `<.>`:
||| forall a, a <.> unity == a
||| forall a, unity <.> a == a
||| + Distributivity of `<.>` and `<->`:
||| forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)
||| forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)
class Ring a => RingWithUnity a where
unity : a
class (VerifiedRing a, RingWithUnity a) => VerifiedRingWithUnity a where
total ringWithUnityIsUnityL : (l : a) -> l <*> unity = l
total ringWithUnityIsUnityR : (r : a) -> unity <*> r = r
total ringWithUnityIsUnityL : (l : a) -> l <.> unity = l
total ringWithUnityIsUnityR : (r : a) -> unity <.> r = r
||| Sets equipped with a binary operation that is commutative, associative and
||| idempotent. Must satisfy the following laws:
@ -281,31 +281,31 @@ class (VerifiedBoundedJoinSemilattice a, VerifiedBoundedMeetSemilattice a, Verif
||| + Inverse for `<+>`:
||| forall a, a <+> inverse a == neutral
||| forall a, inverse a <+> a == neutral
||| + Associativity of `<*>`:
||| forall a b c, a <*> (b <*> c) == (a <*> b) <*> c
||| + Unity for `<*>`:
||| forall a, a <*> unity == a
||| forall a, unity <*> a == a
||| + InverseM of `<*>`:
||| forall a, a <*> inverseM a == unity
||| forall a, inverseM a <*> a == unity
||| + Distributivity of `<*>` and `<->`:
||| forall a b c, a <*> (b <+> c) == (a <*> b) <+> (a <*> c)
||| forall a b c, (a <+> b) <*> c == (a <*> c) <+> (b <*> c)
||| + Associativity of `<.>`:
||| forall a b c, a <.> (b <.> c) == (a <.> b) <.> c
||| + Unity for `<.>`:
||| forall a, a <.> unity == a
||| forall a, unity <.> a == a
||| + InverseM of `<.>`:
||| forall a, a <.> inverseM a == unity
||| forall a, inverseM a <.> a == unity
||| + Distributivity of `<.>` and `<->`:
||| forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)
||| forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)
class RingWithUnity a => Field a where
inverseM : a -> a
class (VerifiedRing a, Field a) => VerifiedField a where
total fieldInverseIsInverseL : (l : a) -> l <*> inverseM l = unity
total fieldInverseIsInverseR : (r : a) -> inverseM r <*> r = unity
total fieldInverseIsInverseL : (l : a) -> l <.> inverseM l = unity
total fieldInverseIsInverseR : (r : a) -> inverseM r <.> r = unity
||| A module over a ring is an additive abelian group of 'vectors' endowed with a
||| scale operation multiplying vectors by ring elements, and distributivity laws
||| relating the scale operation to both ring addition and module addition.
||| scale operation multiplying vectors by ring elements, and distributivity laws
||| relating the scale operation to both ring addition and module addition.
||| Must satisfy the following laws:
|||
||| + Compatibility of scalar multiplication with ring multiplication:
||| forall a b v, a <#> (b <#> v) = (a <*> b) <#> v
||| forall a b v, a <#> (b <#> v) = (a <.> b) <#> v
||| + Ring unity is the identity element of scalar multiplication:
||| forall v, unity <#> v = v
||| + Distributivity of `<#>` and `<+>`:
@ -315,7 +315,7 @@ class (RingWithUnity a, AbelianGroup b) => Module a b where
(<#>) : a -> b -> b
class (VerifiedRingWithUnity a, VerifiedAbelianGroup b, Module a b) => VerifiedModule a b where
total moduleScalarMultiplyComposition : (x,y : a) -> (v : b) -> x <#> (y <#> v) = (x <*> y) <#> v
total moduleScalarMultiplyComposition : (x,y : a) -> (v : b) -> x <#> (y <#> v) = (x <.> y) <#> v
total moduleScalarUnityIsUnity : (v : b) -> unity <#> v = v
total moduleScalarMultDistributiveWRTVectorAddition : (s : a) -> (v, w : b) -> s <#> (v <+> w) = (s <#> v) <+> (s <#> w)
total moduleScalarMultDistributiveWRTModuleAddition : (s, t : a) -> (v : b) -> (s <+> t) <#> v = (s <#> v) <+> (t <#> v)

34
libs/prelude/Prelude/Applicative.idr
View File

@ -9,46 +9,46 @@ import Prelude.Functor
---- Applicative functors/Idioms
infixl 2 <$>
infixl 2 <*>
class Functor f => Applicative (f : Type -> Type) where
pure : a -> f a
(<$>) : f (a -> b) -> f a -> f b
(<*>) : f (a -> b) -> f a -> f b
instance Applicative id where
pure a = a
f <$> a = f a
f <*> a = f a
class (Applicative f, VerifiedFunctor f) => VerifiedApplicative (f : Type -> Type) where
applicativeMap : (x : f a) -> (g : a -> b) ->
map g x = pure g <$> x
applicativeIdentity : (x : f a) -> pure id <$> x = x
map g x = pure g <*> x
applicativeIdentity : (x : f a) -> pure id <*> x = x
applicativeComposition : (x : f a) -> (g1 : f (a -> b)) -> (g2 : f (b -> c)) ->
((pure (.) <$> g2) <$> g1) <$> x = g2 <$> (g1 <$> x)
((pure (.) <*> g2) <*> g1) <*> x = g2 <*> (g1 <*> x)
applicativeHomomorphism : (x : a) -> (g : a -> b) ->
(<$>) {f} (pure g) (pure x) = pure {f} (g x)
(<*>) {f} (pure g) (pure x) = pure {f} (g x)
applicativeInterchange : (x : a) -> (g : f (a -> b)) ->
g <$> pure x = pure (\g' : a -> b => g' x) <$> g
g <*> pure x = pure (\g' : a -> b => g' x) <*> g
infixl 2 <$
(<$) : Applicative f => f a -> f b -> f a
a <$ b = map const a <$> b
infixl 2 <*
(<*) : Applicative f => f a -> f b -> f a
a <* b = map const a <*> b
infixl 2 $>
($>) : Applicative f => f a -> f b -> f b
a $> b = map (const id) a <$> b
infixl 2 *>
(*>) : Applicative f => f a -> f b -> f b
a *> b = map (const id) a <*> b
||| Lift a function to an applicative
liftA : Applicative f => (a -> b) -> f a -> f b
liftA f a = pure f <$> a
liftA f a = pure f <*> a
||| Lift a two-argument function to an applicative
liftA2 : Applicative f => (a -> b -> c) -> f a -> f b -> f c
liftA2 f a b = (map f a) <$> b
liftA2 f a b = (map f a) <*> b
||| Lift a three-argument function to an applicative
liftA3 : Applicative f => (a -> b -> c -> d) -> f a -> f b -> f c -> f d
liftA3 f a b c = (map f a) <$> b <$> c
liftA3 f a b c = (map f a) <*> b <*> c
infixl 3 <|>
class Applicative f => Alternative (f : Type -> Type) where

8
libs/prelude/Prelude/Functor.idr
View File

@ -10,6 +10,14 @@ class Functor (f : Type -> Type) where
||| @ m the morphism
map : (m : a -> b) -> f a -> f b
infixl 4 <$>
||| An infix alias for `map`: the action of a functor on morphisms.
||| @ f the functor
||| @ m the morphism
(<$>) : Functor f => (m : a -> b) -> f a -> f b
m <$> x = map m x
class Functor f => VerifiedFunctor (f : Type -> Type) where
functorIdentity : {a : Type} -> (x : f a) -> map id x = id x
functorComposition : {a : Type} -> {b : Type} -> (x : f a) ->

2
libs/prelude/Prelude/Monad.idr
View File

@ -16,7 +16,7 @@ class Applicative m => Monad (m : Type -> Type) where
class (Monad m, VerifiedApplicative m) => VerifiedMonad (m : Type -> Type) where
monadApplicative : (mf : m (a -> b)) -> (mx : m a) ->
mf <$> mx = mf >>= \f =>
mf <*> mx = mf >>= \f =>
mx >>= \x =>
pure (f x)
monadLeftIdentity : (x : a) -> (f : a -> m b) -> return x >>= f = f x

2
libs/prelude/Prelude/Stream.idr
View File

@ -111,7 +111,7 @@ scanr f (x :: xs) = f x (foldr f xs) :: scanr f xs
instance Applicative Stream where
pure = repeat
(<$>) = zipWith apply
(<*>) = zipWith apply
instance Monad Stream where
s >>= f = diag (map f s)

4
libs/prelude/Prelude/Traversable.idr
View File

@ -8,10 +8,10 @@ import Prelude.Foldable
import Prelude.Functor
traverse_ : (Foldable t, Applicative f) => (a -> f b) -> t a -> f ()
traverse_ f = foldr (($>) . f) (pure ())
traverse_ f = foldr ((*>) . f) (pure ())
sequence_ : (Foldable t, Applicative f) => t (f a) -> f ()
sequence_ = foldr ($>) (pure ())
sequence_ = foldr (*>) (pure ())
for_ : (Foldable t, Applicative f) => t a -> (a -> f b) -> f ()
for_ = flip traverse_

2
rts/Makefile
View File

@ -18,7 +18,7 @@ endif
endif
ifeq ($(OS), windows)
OBJS += windows/idris_stdfgn.o windows/idris_net.o
OBJS += windows/idris_stdfgn.o windows/idris_net.o windows/win_utils.o
else
OBJS += idris_stdfgn.o idris_net.o
endif

13
rts/windows/idris_stdfgn.c
View File

@ -5,9 +5,12 @@
#include <fcntl.h>
#include <stdio.h>
#include <time.h>
#include <io.h>
extern char** environ;
int win_fpoll(void* h);
void putStr(char* str) {
printf("%s", str);
}
@ -32,14 +35,18 @@ int fileError(void* h) {
return ferror(f);
}
void fputStr(void* h, char* str) {
int idris_writeStr(void* h, char* str) {
FILE* f = (FILE*)h;
fputs(str, f);
if (fputs(str, f)) {
return 0;
} else {
return -1;
}
}
int fpoll(void* h)
{
return 0;
return win_fpoll(h);
}
void* do_popen(const char* cmd, const char* mode) {

21
rts/windows/win_utils.c Normal file
View File

@ -0,0 +1,21 @@
#include <windows.h>
#include <io.h>
#include <stdio.h>
// THis file exists to avoid clashes between windows.h and idris_rts.h
//
int win_fpoll(void* h)
{
HANDLE wh =(HANDLE) _get_osfhandle(_fileno((FILE*)h));
if (wh == INVALID_HANDLE_VALUE) {
return -1;
}
DWORD ret = WaitForSingleObject(wh, 1000);
// Imitate the return values of select()
if (ret == WAIT_OBJECT_0)
return 1;
if (ret == WAIT_TIMEOUT)
return 0;
return -1;
}

4
samples/interp.idr
View File

@ -37,8 +37,8 @@ using (G : Vect n Ty)
index_first = stop
index_next = pop
(<$>) : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t
(<$>) = \f, a => App f a
(<*>) : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t
(<*>) = \f, a => App f a
pure : Expr G a -> Expr G a
pure = id

9
src/Idris/AbsSyntax.hs
View File

@ -1714,6 +1714,10 @@ stripLinear i tm = evalState (sl tm) [] where
return (a' : as')
slAlts ns [] = return []
sl (PPair fc p l r) = do l' <- sl l; r' <- sl r; return (PPair fc p l' r')
sl (PDPair fc p l t r) = do l' <- sl l
t' <- sl t
r' <- sl r
return (PDPair fc p l' t' r')
sl (PApp fc fn args) = do -- Just the args, fn isn't matchable as a var
args' <- mapM slA args
return $ PApp fc fn args'
@ -1978,8 +1982,11 @@ shadow :: Name -> Name -> PTerm -> PTerm
shadow n n' t = sm t where
sm (PRef fc x) | n == x = PRef fc n'
sm (PLam fc x t sc) | n /= x = PLam fc x (sm t) (sm sc)
sm (PPi p x t sc) | n /=x = PPi p x (sm t) (sm sc)
| otherwise = PLam fc x (sm t) sc
sm (PPi p x t sc) | n /= x = PPi p x (sm t) (sm sc)
| otherwise = PPi p x (sm t) sc
sm (PLet fc x t v sc) | n /= x = PLet fc x (sm t) (sm v) (sm sc)
| otherwise = PLet fc x (sm t) (sm v) sc
sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
sm (PAppBind f x as) = PAppBind f (sm x) (map (fmap sm) as)
sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)

2
src/Idris/AbsSyntaxTree.hs
View File

@ -1157,7 +1157,7 @@ updateSyntaxRules rules (SyntaxRules sr) = SyntaxRules newRules
initDSL = DSL (PRef f (sUN ">>="))
(PRef f (sUN "return"))
(PRef f (sUN "<$>"))
(PRef f (sUN "<*>"))
(PRef f (sUN "pure"))
Nothing
Nothing

2
src/Idris/CmdOptions.hs
View File

@ -26,7 +26,7 @@ runArgParser = do opts <- execParser $ info parser
idrisProgDesc = PP.vsep [PP.empty,
PP.text "Idris is a general purpose pure functional programming language with dependent",
PP.text "types. Dependent types allow types to be predicated on values, meaning that",
PP.text "some aspects of a program’s behaviour can be specified precisely in the type.",
PP.text "some aspects of a program's behaviour can be specified precisely in the type.",
PP.text "It is compiled, with eager evaluation. Its features are influenced by Haskell",
PP.text "and ML.",
PP.empty,

34
src/Idris/DSL.hs
View File

@ -17,21 +17,43 @@ desugar :: SyntaxInfo -> IState -> PTerm -> PTerm
desugar syn i t = let t' = expandDo (dsl_info syn) t in
t' -- addImpl i t'
mkTTName :: FC -> Name -> PTerm
mkTTName fc n =
let mkList fc [] = PRef fc (sNS (sUN "Nil") ["List", "Prelude"])
mkList fc (x:xs) = PApp fc (PRef fc (sNS (sUN "::") ["List", "Prelude"]))
[ pexp (stringC x)
, pexp (mkList fc xs)]
stringC = PConstant . Str . str
intC = PConstant . I
reflm n = sNS (sUN n) ["Reflection", "Language"]
in case n of
UN nm -> PApp fc (PRef fc (reflm "UN")) [ pexp (stringC nm)]
NS nm ns -> PApp fc (PRef fc (reflm "NS")) [ pexp (mkTTName fc nm)
, pexp (mkList fc ns)]
MN i nm -> PApp fc (PRef fc (reflm "MN")) [ pexp (intC i)
, pexp (stringC nm)]
otherwise -> PRef fc $ reflm "NErased"
expandDo :: DSL -> PTerm -> PTerm
expandDo dsl (PLam fc n ty tm)
| Just lam <- dsl_lambda dsl
= let sc = PApp fc lam [pexp (var dsl n tm 0)] in
expandDo dsl sc
= let sc = PApp fc lam [ pexp (mkTTName fc n)
, pexp (var dsl n tm 0)]
in expandDo dsl sc
expandDo dsl (PLam fc n ty tm) = PLam fc n (expandDo dsl ty) (expandDo dsl tm)
expandDo dsl (PLet fc n ty v tm)
| Just letb <- dsl_let dsl
= let sc = PApp (fileFC "(dsl)") letb [pexp v, pexp (var dsl n tm 0)] in
expandDo dsl sc
= let sc = PApp (fileFC "(dsl)") letb [ pexp (mkTTName fc n)
, pexp v
, pexp (var dsl n tm 0)]
in expandDo dsl sc
expandDo dsl (PLet fc n ty v tm) = PLet fc n (expandDo dsl ty) (expandDo dsl v) (expandDo dsl tm)
expandDo dsl (PPi p n ty tm)
| Just pi <- dsl_pi dsl
= let sc = PApp (fileFC "(dsl)") pi [pexp ty, pexp (var dsl n tm 0)] in
expandDo dsl sc
= let sc = PApp (fileFC "(dsl)") pi [ pexp (mkTTName (fileFC "(dsl)") n)
, pexp ty
, pexp (var dsl n tm 0)]
in expandDo dsl sc
expandDo dsl (PPi p n ty tm) = PPi p n (expandDo dsl ty) (expandDo dsl tm)
expandDo dsl (PApp fc t args) = PApp fc (expandDo dsl t)
(map (fmap (expandDo dsl)) args)

6
src/Idris/Elab/Clause.hs
View File

@ -648,9 +648,9 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
-- Now build the RHS, using the type of the LHS as the goal.
i <- getIState -- new implicits from where block
logLvl 5 (showTmImpls (expandParams decorate newargs defs (defs \\ decls) rhs_in))
let rhs = addImplBoundInf i (map fst newargs) (defs \\ decls)
let rhs = addImplBoundInf i (map fst newargs_all) (defs \\ decls)
(expandParams decorate newargs defs (defs \\ decls) rhs_in)
logLvl 2 $ "RHS: " ++ showTmImpls rhs
logLvl 2 $ "RHS: " ++ show (map fst newargs_all) ++ " " ++ showTmImpls rhs
ctxt <- getContext -- new context with where block added
logLvl 5 "STARTING CHECK"
((rhs', defer, is, probs), _) <-
@ -673,7 +673,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_,_) -> (x,y)) probs)
logLvl 5 "DONE CHECK"
logLvl 2 $ "---> " ++ show rhs'
logLvl 4 $ "---> " ++ show rhs'
when (not (null defer)) $ iLOG $ "DEFERRED " ++
show (map (\ (n, (_,_,t)) -> (n, t)) defer)
def' <- checkDef fc defer

6
src/Idris/Elab/Data.hs
View File

@ -316,11 +316,13 @@ elabCaseFun ind paramPos n ty cons info = do
eliminatorClauses <- mapM (\(cns, cnsElim) -> generateEliminatorClauses cns cnsElim clauseGeneralArgs generalParams) (zip cons clauseConsElimArgs)
let eliminatorDef = PClauses emptyFC [TotalFn] elimDeclName eliminatorClauses
elimLog $ "-- case function definition: " ++ (show . showDeclImp verbosePPOption) eliminatorDef
State.lift $ idrisCatch (rec_elabDecl info EAll info eliminatorTyDecl) (\err -> return ())
State.lift $ idrisCatch (rec_elabDecl info EAll info eliminatorTyDecl)
(ierror . Elaborating "type declaration of " elimDeclName)
-- Do not elaborate clauses if there aren't any
case eliminatorClauses of
[] -> State.lift $ solveDeferred elimDeclName -- Remove meta-variable for type
_ -> State.lift $ idrisCatch (rec_elabDecl info EAll info eliminatorDef) (\err -> return ())
_ -> State.lift $ idrisCatch (rec_elabDecl info EAll info eliminatorDef)
(ierror . Elaborating "clauses of " elimDeclName)
where elimLog :: String -> EliminatorState ()
elimLog s = State.lift (logLvl 2 s)

10
src/Idris/ElabTerm.hs
View File

@ -893,9 +893,17 @@ elab ist info emode opts fn tm
-- Drop the unique arguments used in the term already
-- and in the scrutinee (since it's
-- not valid to use them again anyway)
--
-- Also drop unique arguments which don't appear explicitly
-- in either case branch so they don't count as used
-- unnecessarily (can only do this for unique things, since we
-- assume they don't appear implicitly in types)
ptm <- get_term
let inOpts = (filter (/= scvn) (map fst args)) \\ (concatMap (\x -> allNamesIn (snd x)) opts)
let argsDropped = filter (isUnique envU)
(nub $ allNamesIn scr ++ inApp ptm)
(nub $ allNamesIn scr ++ inApp ptm ++
inOpts)
let args' = filter (\(n, _) -> n `notElem` argsDropped) args

18
src/Idris/ParseHelpers.hs
View File

@ -105,30 +105,28 @@ isEol :: Char -> Bool
isEol '\n' = True
isEol _ = False
-- | A parser that succeeds at the end of the line
eol :: MonadicParsing m => m ()
eol = (satisfy isEol *> pure ()) <|> lookAhead eof <?> "end of line"
{- | Consumes a single-line comment
@
SingleLineComment_t ::= '--' EOL_t
| '--' ~DocCommentMarker_t ~EOL_t* EOL_t
;
SingleLineComment_t ::= '--' ~EOL_t* EOL_t ;
@
-}
singleLineComment :: MonadicParsing m => m ()
singleLineComment = try (string "--" *> eol *> pure ())
<|> try (string "--" *> many simpleWhiteSpace *>
many (satisfy (not . isEol)) *>
eol *> pure ())
<?> ""
singleLineComment = (string "--" *>
many (satisfy (not . isEol)) *>
eol *> pure ())
<?> "single-line comment"
{- | Consumes a multi-line comment
@
MultiLineComment_t ::=
'{ -- }'
| '{ -' ~DocCommentMarker_t InCommentChars_t
| '{ -' InCommentChars_t
;
@
@ -154,7 +152,7 @@ multiLineComment = try (string "{-" *> (string "-}") *> pure ())
startEnd :: String
startEnd = "{}-"
{-| Parses a documentation comment (similar to haddock) given a marker character
{-| Parses a documentation comment
@
DocComment_t ::= '|||' ~EOL_t* EOL_t

16
src/Idris/Parser.hs
View File

@ -1311,8 +1311,24 @@ loadSource lidr f toline
mapM_ (addIBC . IBCImport) [(reexport, realName) | (reexport, realName, alias, fc) <- imports]
let syntax = defaultSyntax{ syn_namespace = reverse mname,
maxline = toline }
ist <- getIState
-- Save the span from parsing the module header, because
-- an empty program parse might obliterate it.
let oldSpan = idris_parsedSpan ist
ds' <- parseProg syntax f file pos
case (ds', oldSpan) of
([], Just fc) ->
-- If no program elements were parsed, we dind't
-- get a loaded region in the IBC file. That
-- means we need to add it back.
do ist <- getIState
putIState ist { idris_parsedSpan = oldSpan
, ibc_write = IBCParsedRegion fc :
ibc_write ist
}
_ -> return ()
-- Parsing done, now process declarations
let ds = namespaces mname ds'

6
src/Idris/REPL.hs
View File

@ -821,7 +821,7 @@ process fn (Undefine names) = undefine names
-- Keep track of which names you've removed so you can
-- print them out to the user afterward
undefine names = undefine' names []
undefine' [] list = do iRenderOutput $ printUndefinedNames list
undefine' [] list = do iRenderResult $ printUndefinedNames list
return ()
undefine' (n:names) already = do
allDefined <- idris_repl_defs `fmap` get
@ -1104,10 +1104,12 @@ process fn Execute
(tmpn, tmph) <- runIO tempfile
runIO $ hClose tmph
t <- codegen
-- gcc adds .exe when it builds windows programs
progName <- return $ if isWindows then tmpn ++ ".exe" else tmpn
ir <- compile t tmpn m
runIO $ generate t (fst (head (idris_imported ist))) ir
case idris_outputmode ist of
RawOutput h -> do runIO $ rawSystem tmpn []
RawOutput h -> do runIO $ rawSystem progName []
return ()
IdeMode n h -> runIO . hPutStrLn h $
IdeMode.convSExp "run-program" tmpn n)

4
src/Pkg/PParser.hs
View File

@ -16,7 +16,7 @@ import Idris.CmdOptions
import Control.Monad.State.Strict
import Control.Applicative
import System.Info (os)
import Util.System
type PParser = StateT PkgDesc IdrisInnerParser
@ -63,7 +63,7 @@ pClause :: PParser ()
pClause = do reserved "executable"; lchar '=';
exec <- iName []
st <- get
put (st { execout = Just (if os `elem` ["win32", "mingw32", "cygwin32"]
put (st { execout = Just (if isWindows
then ((show exec) ++ ".exe")
else ( show exec )
) })

6
src/Util/System.hs
View File

@ -1,4 +1,4 @@
module Util.System(tempfile,withTempdir,rmFile,catchIO) where
module Util.System(tempfile,withTempdir,rmFile,catchIO, isWindows) where
-- System helper functions.
import Control.Monad (when)
@ -9,6 +9,7 @@ import System.Directory (getTemporaryDirectory
)
import System.FilePath ((</>), normalise)
import System.IO
import System.Info
import System.IO.Error
import Control.Exception as CE
@ -18,6 +19,9 @@ catchIO = CE.catch
throwIO :: IOError -> IO a
throwIO = CE.throw
isWindows :: Bool
isWindows = os `elem` ["win32", "mingw32", "cygwin32"]
tempfile :: IO (FilePath, Handle)
tempfile = do dir <- getTemporaryDirectory
openTempFile (normalise dir) "idris"

5
test/dsl001/test001.idr
View File

@ -35,8 +35,11 @@ using (G : Vect n Ty)
If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a
Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b
lam_ : TTName -> Expr (a :: G) t -> Expr G (TyFun a t)
lam_ _ = Lam
dsl expr
lambda = Lam
lambda = lam_
variable = Var
index_first = stop
index_next = pop

7
test/dsl002/Resimp.idr
View File

@ -156,6 +156,11 @@ using (i: Fin n, gam : Vect n Ty, gam' : Vect n Ty, gam'' : Vect n Ty)
= interp env v (\env', v' => do n <- v'
interp env' (f n) k)
let_ : _ -> Creator (interpTy a) ->
Res (a :: gam) (Val () :: gam') (R t) ->
Res gam gam' (R t)
let_ _ = Let
-- run : {static} Res [] [] (R t) -> IO t
-- run prog = interp [] prog (\env, res => res)
@ -163,7 +168,7 @@ syntax run [prog] = interp [] prog (\env, res => res)
dsl res
variable = id
let = Let
let = let_
index_first = stop
index_next = pop

10
test/dsl003/DSLPi.idr
View File

@ -5,8 +5,11 @@ import Data.Vect
data Ty = BOOL | INT | UNIT | ARR Ty Ty
arr_ : _ -> Ty -> Ty -> Ty
arr_ _ = ARR
dsl simple_type
pi = ARR
pi = arr_
test1 : simple_type (BOOL -> INT -> UNIT) = BOOL `ARR` (INT `ARR` UNIT)
test1 = Refl
@ -25,8 +28,11 @@ using (vars : Vect n Ty)
implicit exprSpec : Expr vars BOOL -> Spec vars
exprSpec = ItHolds
forall_ : _ -> (t : Ty) -> Spec (t :: vars) -> Spec vars
forall_ _ = ForAll
dsl specs
pi = ForAll
pi = forall_
variable = Var
index_first = FZ
index_next = FS

2
test/reg027/reg027.idr
View File

@ -14,7 +14,7 @@ instance Functor IntFn where -- (\x => Int -> x) where
instance Applicative (\x => Int -> x) where
pure v = \x => v
(<$>) f a = \x => f x (a x)
(<*>) f a = \x => f x (a x)
instance Monad IntFn where
f >>= k = \x => k (f x) x

15
test/reg050/expected
View File

@ -12,17 +12,18 @@ When elaborating an application of function Prelude.Monad.>>=:
\{uv0} => argTy -> uv
./baddoublebang.idr:6:26: error: not
a terminator, expected: "$",
"$>", "&&", "*", "+", "++", "-",
"&&", "*", "*>", "+", "++", "-",
"->", ".", "/", "/=", "::", ";",
"<", "<#>", "<$", "<$>", "<*>",
"<+>", "<->", "<<", "<=", "<|>",
"=", "==", ">", ">=", ">>",
">>=", "\\\\", "`", "in", "||",
"~=~",
"<", "<#>", "<$>", "<*", "<*>",
"<+>", "<->", "<.>", "<<", "<=",
"<|>", "=", "==", ">", ">=",
">>", ">>=", "\\\\", "`", "in",
"||", "~=~",
ambiguous use of a left-associative operator,
ambiguous use of a non-associative operator,
ambiguous use of a right-associative operator,
end of input, function argument,
matching application expression
matching application expression,
single-line comment
doubleBang mmn = do pure !!mmn
^

2
test/reg053/four.idr
View File

@ -5,5 +5,5 @@ data FourFunctor y = Four y y y y
traverseFourFunctor : Applicative f ->
(x -> f b) -> FourFunctor x -> f (FourFunctor b)
traverseFourFunctor constr f (Four w x y z)
= pure Four <$> (f w) <$> (f x) <$> (f y) <$> (f z)
= pure Four <*> (f w) <*> (f x) <*> (f y) <*> (f z)

4
test/sourceLocation001/SourceLoc.idr
View File

@ -54,6 +54,8 @@ using (ctxt : Vect n Ty)
run (App f x) env = !(run f env) !(run x env)
run (Die {loc}) _ = Left loc
lam_ : _ -> Tm (t::ctxt) t' -> Tm ctxt (Arr t t')
lam_ _ = Lam
exec : Tm [] t -> IO ()
exec tm = case run tm [] of
@ -64,7 +66,7 @@ dsl lang
variable = Var
index_first = FZ
index_next = FS
lambda = Lam
lambda = lam_
testTerm1 : Tm [] (Arr U U)
testTerm1 = lang (\x=>Die)

4
test/sourceLocation001/expected
View File

@ -3,9 +3,9 @@ FileLoc "SourceLoc.idr" (16, 11) (16, 11)
Testing using inline tactics
FileLoc "SourceLoc.idr" (20, 17) (20, 17)
Testing using metavariable with later definition
FileLoc "SourceLoc.idr" (96, 16) (96, 16)
FileLoc "SourceLoc.idr" (98, 16) (98, 16)
-----------------------
Success!
Error at FileLoc "SourceLoc.idr" (70, 23) (70, 23)
Error at FileLoc "SourceLoc.idr" (72, 23) (72, 23)
Success!
Success!

2
test/sugar001/test007.idr
View File

@ -19,7 +19,7 @@ instance Functor Eval where
instance Applicative Eval where
pure x = MkEval (\e => Just x)
(<$>) (MkEval f) (MkEval g) = MkEval (\x => appAux (f x) (g x)) where
(<*>) (MkEval f) (MkEval g) = MkEval (\x => appAux (f x) (g x)) where
appAux : Maybe (a -> b) -> Maybe a -> Maybe b
appAux (Just fx) (Just gx) = Just (fx gx)
appAux _ _ = Nothing

2
test/tutorial003/tutorial003.idr
View File

@ -19,7 +19,7 @@ instance Functor Eval where
instance Applicative Eval where
pure x = MkEval (\e => Just x)
(<$>) (MkEval f) (MkEval g) = MkEval (\x => app (f x) (g x)) where
(<*>) (MkEval f) (MkEval g) = MkEval (\x => app (f x) (g x)) where
app : Maybe (a -> b) -> Maybe a -> Maybe b
app (Just fx) (Just gx) = Just (fx gx)
app _ _ = Nothing