[clean-list] How to show test result and change number of test

[Pieter Koopman]

Dear Lee Ho Yeung,

The current result indicates that no counterexamples are found.
In order to obtain a definition like f x = if ( x <= 0) 1 (x*f(x-1) you 
need:
- a proper definition of the type Fun
- define or derive an instance of the generic functions for generation 
(ggen), equivalnece (gEq) en showing (genShow) element of the types 
used. Here you obviously need a special instance of genShow to obtain 
the indicate function.
- a definition of apply to turn elements of type Fun to the 
corresponding function.


The types I used are:
:: OR s t = L s | R t

:: BinOp x = OpPlus x x | OpTimes x x | OpMinus x x
:: Var = X
:: Expr = Expr (OR (OR Var IConst) (BinOp Expr))
:: FunAp = FunAp Int

:: RFun = RFun TermVal Expr (OR (OR Var IConst) (BinOp (OR (OR Var 
IConst) FunAp)))
:: Fun = Fun (OR Expr RFun)

:: TermVal = TermVal Int
:: IConst = IConst Int

The class apply looks like:

class apply d e v :: d -> e -> v

instance apply (OR x y) b c | apply x b c & apply y b c
where
     apply (L x) = apply x
     apply (R y) = apply y

instance apply (BinOp x) b v | apply x b v & +, -, * v
where
     apply (OpPlus  x y) = \b.apply x b + apply y b
     apply (OpMinus x y) = \b.apply x b - apply y b
     apply (OpTimes x y) = \b.apply x b * apply y b

// ------------ apply for ints ------------

instance apply IConst b Int where apply (IConst i) = \b.i
instance apply Var Int Int where apply X = \i.i
instance apply Var (x,Int) Int where apply X = \(_,i).i
instance apply Expr Int Int where apply (Expr f) = apply f
instance apply Expr (x,Int) Int where apply (Expr f) = \(_,i).apply f i
instance apply FunAp (Int->Int,Int) Int where apply (FunAp d) = \(f,i).f 
(i-d)
instance apply FunAp Int Int where apply (FunAp d) = abort "FunAp Int Int"
instance apply RFun Int Int
where apply rf=:(RFun (TermVal c) t e) = f
       where f i = if (i<=c) (apply t i) (apply e (f,i))
instance apply Fun Int Int where apply (Fun f) = apply f

For data generation use something like:
ggen{|TermVal|} n r = map TermVal [0..5]
ggen{|FunAp|} n r = map FunAp [1..2]
ggen{|IConst|} n r = map IConst [0..8]
derive ggen OR, BinOp, Var, Expr, RFun, Fun

printing can be done like:

genShow{|OR|} fx fy sep p (L x)            rest = fx sep p x rest
genShow{|OR|} fx fy sep p (R y)            rest = fy sep p y rest
genShow{|IConst|}   sep p (IConst c)    rest = [toString c:rest]
genShow{|BinOp|} fx sep p (OpPlus x y)    rest = [if p "(" "": fx sep 
True x ["+": fx sep True y [if p ")" "":rest]]]
genShow{|BinOp|} fx sep p (OpMinus x y)    rest = [if p "(" "": fx sep 
True x ["-": fx sep True y [if p ")" "":rest]]]
genShow{|BinOp|} fx sep p (OpTimes x y)    rest = [if p "(" "": fx sep 
True x ["*": fx sep True y [if p ")" "":rest]]]
genShow{|Var|}        sep p v                rest = ["x":rest]
genShow{|Expr|}        sep p (Expr e)        rest = genShow{|*|} sep p e 
rest
genShow{|FunAp|}    sep p (FunAp i)        rest = ["f (x-",toString 
i,")":rest]
genShow{|TermVal|}  sep p (TermVal c)    rest = [toString c:rest]
genShow{|RFun|}        sep p (RFun c t e)    rest
  = ["if (x<=":genShow{|*|} sep False c[") ":genShow{|*|} sep True t [" 
": genShow{|*|} sep True e rest]]]
genShow{|Fun|}        sep p (Fun f)        rest = ["f x = ": 
genShow{|*|} sep False f rest]

Hopefully this helps.

Best regards,

Pieter Koopman

On 09/04/2011 12:00 PM, Lee Ho Yeung wrote:
> when i try the following, it only show passed after 1000 test one case 
> rejected and repeated with a few lines, but do not show f x = if ( x 
> <= 0) 1 (x*f(x-1)) as paper systematic synthesis of functions
> which steps do i miss?
> module martin001
> import gast, StdEnv
> prop1 :: Fun -> Bool
> prop1 d = ~(f 2 == 2 && f 4 == 24 && f 6 == 720) where f = apply d
> Start = test prop1
>
>
> _______________________________________________
> clean-list mailing list
> clean-list at science.ru.nl
> http://mailman.science.ru.nl/mailman/listinfo/clean-list
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mailman.science.ru.nl/pipermail/clean-list/attachments/20110413/8e86c3f2/attachment.html>