Update dsl001 test
Add some :printdef to ensure that the interpreter (and library
functions) are successfully partially evaluated for factorial
commit8fea0b0d3cd1d862d3c2fb0d00f408018a10ba91
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateSat 27 Aug 2016, 11:04 (10 years ago)
parent037ea33
test/dsl001/expected+12
@@ -1,2 +1,14 @@
1124
2212
3+testFac : Int
4+testFac = PE_interp_f79b3e31 [] (PE_fromInteger_a0377313 4)
5+PE_interp_f79b3e31 : Env G -> Int -> Int
6+PE_interp_f79b3e31 (3arg) = \x =>
7+ ifThenElse (PE_==_a03270d8 x
8+ (PE_fromInteger_a0377313 0))
9+ (Delay (PE_fromInteger_a0377313 1))
10+ (Delay (PE_*_a725d5d6 (PE_interp_f79b3e31 (x ::
11+ (3arg))
12+ (PE_-_a71cf640 x
13+ (PE_fromInteger_a0377313 1)))
14+ x))
test/dsl001/inputnew file+2
@@ -0,0 +1,2 @@
1+:printdef testFac
2+:printdef PE_interp_f79b3e31
test/dsl001/run+1
@@ -1,4 +1,5 @@
11#!/usr/bin/env bash
22${IDRIS:-idris} $@ test001.idr -o test001
33./test001
4+${IDRIS:-idris} $@ test001.idr --quiet < input
45rm -f test001 test001.ibc
test/dsl001/test001.idr+1
@@ -35,6 +35,7 @@ using (G : Vect n Ty)
3535 If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a
3636 Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b
3737
38+ %static
3839 lam_ : TTName -> Expr (a :: G) t -> Expr G (TyFun a t)
3940 lam_ _ = Lam
4041