git.iko.soy/Idris-dev
on master help sign in
Library rearrangement done.
commite1f139a9894a9cea0a51b8f65047277bc10273f4 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateThu 19 Mar 2015, 18:09 (12 years ago) parent41d0309
13 files changed+10−24
compare with master
unifiedsplit
src/Idris/Elab/Provider.hs+1−1 src/Idris/Providers.hs+3−3 test/basic011/run+1−1 test/docs002/docs002.idr−3 test/ffi002/expected+1−1 test/ffi002/test023.idr−2 test/ffi004/test026.idr−2 test/ffi005/Postulate.idr−2 test/interactive007/run+1−1 test/io003/run+2−2 test/primitives003/expected−2 test/primitives003/test038.idr−3 test/reg048/run+1−1
src/Idris/Elab/Provider.hs+1−1
@@ -112,7 +112,7 @@ elabProvider doc info syn fc what n
112112 -- error messages with less normalisation
113113 providerOf :: Type -> Type
114114 providerOf ty = App (P Ref (sUN "IO") Erased) $
115− App (P Ref (sNS (sUN "Provider") ["Providers"]) Erased)
115+ App (P Ref (sNS (sUN "Provider") ["Providers", "Prelude"]) Erased)
116116 ty
117117
118118 isProviderOf :: Context -> TT Name -> TT Name -> Bool
src/Idris/Providers.hs+3−3
@@ -10,16 +10,16 @@ import Idris.Error
1010-- | Wrap a type provider in the type of type providers
1111providerTy :: FC -> PTerm -> PTerm
1212providerTy fc tm
13− = PApp fc (PRef fc $ sUN "Provider") [PExp 0 [] (sMN 0 "pvarg") tm]
13+ = PApp fc (PRef fc $ sNS (sUN "Provider" ) ["Providers", "Prelude"]) [PExp 0 [] (sMN 0 "pvarg") tm]
1414
1515ioret :: Name
1616ioret = sUN "prim_io_return"
1717
1818ermod :: Name
19−ermod = sNS (sUN "Error") ["Providers"]
19+ermod = sNS (sUN "Error") ["Providers", "Prelude"]
2020
2121prmod :: Name
22−prmod = sNS (sUN "Provide") ["Providers"]
22+prmod = sNS (sUN "Provide") ["Providers", "Prelude"]
2323
2424data Provided a = Provide a
2525 deriving (Show, Eq, Functor)
test/basic011/run+1−1
@@ -1,4 +1,4 @@
11#!/usr/bin/env bash
2−idris $@ basic011.idr -o basic011
2+idris $@ basic011.idr -p contrib -o basic011
33./basic011
44rm -f basic011 *.ibc
test/docs002/docs002.idr−3
@@ -1,9 +1,6 @@
11module Main
22
33-- Simple test case for type provider documentation.
4−
5−import Providers
6−
74%language TypeProviders
85
96getType : Int -> IO (Provider Type)
test/ffi002/expected+1−1
@@ -1 +1 @@
1−test023.idr:22:21:Type provider error: Always fails
1+test023.idr:20:21:Type provider error: Always fails
test/ffi002/test023.idr−2
@@ -2,8 +2,6 @@ module Main
22
33-- Simple test case for trivial type providers.
44
5−import Providers
6−
75%language TypeProviders
86
97-- Provide the Unit type
test/ffi004/test026.idr−2
@@ -2,8 +2,6 @@ module Main
22
33-- Simple test case for trivial type providers.
44
5−import Providers
6−
75%language TypeProviders
86
97strToType : String -> Type
test/ffi005/Postulate.idr−2
@@ -1,7 +1,5 @@
11module Main
22
3−import Providers
4−
53%language TypeProviders
64
75bad : IO (Provider Type)
test/interactive007/run+1−1
@@ -1,2 +1,2 @@
11#!/usr/bin/env bash
2−idris --nobanner --nocolor < input
2+idris -p contrib --nobanner --nocolor < input
test/io003/run+2−2
@@ -1,6 +1,6 @@
11#!/usr/bin/env bash
2−idris $@ test018.idr -o test018
3−idris $@ test018a.idr -o test018a
2+idris $@ test018.idr -p contrib -o test018
3+idris $@ test018a.idr -p contrib -o test018a
44./test018
55#./test018a
66rm -f test018 test018a *.ibc
test/primitives003/expected−2
@@ -16,8 +16,6 @@ True
1616False
1717True
1818False
19−True
20−False
2119False
2220True
2321False
test/primitives003/test038.idr−3
@@ -40,9 +40,6 @@ main = do
4040 -- Booleans
4141 putStrLn . show $ test True True
4242 putStrLn . show $ test True False
43− -- Float
44− putStrLn . show $ test 1.0 1.0
45− putStrLn . show $ test 1.0 2.0
4643 -- Maybe
4744 putStrLn . show $ test (Just "hello") (Just "hello")
4845 putStrLn . show $ test (Just "hello") (Just "world")
test/reg048/run+1−1
@@ -1,4 +1,4 @@
11#!/usr/bin/env bash
2−idris $@ reg048.idr -o reg048
2+idris $@ reg048.idr -p contrib -o reg048
33./reg048
44rm -f reg048 *.ibc