git.iko.soy/Idris-dev
on master help sign in
Test for simple file-based type providers
0250ca6David Christiansen
test/README+2
compare with master
unifiedsplit
@@ -24,5 +24,7 @@ Tests:
24022: dynamic C library loading and interpreter IO
24022: dynamic C library loading and interpreter IO
25023: trivial (non-I/O) type providers
25023: trivial (non-I/O) type providers
26024: interpreter I/O
26024: interpreter I/O
27+025: memory effects
28+026: simple file-I/O-based type provider
27
29
28regxxx: various regression tests
30regxxx: various regression tests
test/test026/expectednew file+3
@@ -0,0 +1,3 @@
1+Type checking ./test026.idr
2+2 : Int
3+2 : Nat
test/test026/inputnew file+2
@@ -0,0 +1,2 @@
1+foo
2+bar
test/test026/runnew file+3
@@ -0,0 +1,3 @@
1+#!/bin/bash
2+idris --quiet test026.idr < input
3+rm -f *.ibc
test/test026/test026.idrnew file+26
@@ -0,0 +1,26 @@
1+module Main
2+
3+-- Simple test case for trivial type providers.
4+
5+import Providers
6+
7+%language TypeProviders
8+
9+strToType : String -> Type
10+strToType "Int" = Int
11+strToType _ = Nat
12+
13+-- If the file contains "Int", provide Int as a type, otherwise provide Nat
14+fromFile : String -> IO (Provider Type)
15+fromFile fname = do str <- readFile fname
16+ return (Provide (strToType str))
17+
18+%provide (T1 : Type) with fromFile "theType"
19+%provide (T2 : Type) with fromFile "theOtherType"
20+
21+foo : T1
22+foo = 2
23+
24+bar : T2
25+bar = 2
26+
test/test026/theOtherTypenew file+1
@@ -0,0 +1 @@
1+Nat
test/test026/theTypenew file+1
@@ -0,0 +1 @@
1+Int