forked from GitHub/gf-core
added testcases for evaluation with suspension
This commit is contained in:
@@ -11,6 +11,9 @@ def g2 1 x = x ;
|
|||||||
fun g0 : Int -> Int -> Int ;
|
fun g0 : Int -> Int -> Int ;
|
||||||
def g0 = g2 ;
|
def g0 = g2 ;
|
||||||
|
|
||||||
|
fun g3 : Int -> (Int -> Int) ;
|
||||||
|
def g3 3 = g ;
|
||||||
|
|
||||||
fun const : Int -> Int -> Int ;
|
fun const : Int -> Int -> Int ;
|
||||||
def const x _ = x ;
|
def const x _ = x ;
|
||||||
|
|
||||||
@@ -25,4 +28,14 @@ def dec zero = zero ;
|
|||||||
dec (succ n) = n ;
|
dec (succ n) = n ;
|
||||||
dec n = err ; -- for fall through checking
|
dec n = err ; -- for fall through checking
|
||||||
|
|
||||||
|
fun plus : Nat -> Nat -> Nat ;
|
||||||
|
def plus err zero = err ;
|
||||||
|
plus m err = err ;
|
||||||
|
plus m zero = m ;
|
||||||
|
plus m (succ n) = plus (succ m) n ;
|
||||||
|
|
||||||
|
fun dec2 : Int -> Nat -> Nat ;
|
||||||
|
def dec2 0 zero = err ;
|
||||||
|
dec2 _ (succ n) = n ;
|
||||||
|
|
||||||
}
|
}
|
||||||
@@ -27,3 +27,8 @@ pt -compute dec (succ (succ zero))
|
|||||||
pt -compute dec (succ ?)
|
pt -compute dec (succ ?)
|
||||||
pt -compute \x -> dec x
|
pt -compute \x -> dec x
|
||||||
pt -compute dec ?
|
pt -compute dec ?
|
||||||
|
pt -compute (\f -> f 0) (g3 ?)
|
||||||
|
pt -compute g (g2 ? 0)
|
||||||
|
pt -compute plus (succ zero) (succ zero)
|
||||||
|
pt -compute dec2 0 (succ zero)
|
||||||
|
pt -compute plus err (succ zero)
|
||||||
@@ -48,3 +48,13 @@ succ zero
|
|||||||
|
|
||||||
\v0 -> g v0
|
\v0 -> g v0
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
g ?
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
5
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|||||||
Reference in New Issue
Block a user