author  bulwahn 
Fri, 23 Mar 2012 12:03:59 +0100  
changeset 47090  6b53d954255b 
parent 46758  4106258260b3 
child 49193  0067d83414c8 
permissions  rwrr 
43313  1 
{ 
2 
A narrowingbased Evaluator for Formulas in Prefix Normal Form based on the compilation technique of LazySmallCheck 

3 
} 

4 
module Narrowing_Engine where 

5 

46408
2520cd337056
using fully qualified module names in Haskell source, which seems to be required by GHC 7.0.4 (also cf. 0fd9ab902b5a)
bulwahn
parents:
45760
diff
changeset

6 
import Control.Monad 
43313  7 
import Control.Exception 
46408
2520cd337056
using fully qualified module names in Haskell source, which seems to be required by GHC 7.0.4 (also cf. 0fd9ab902b5a)
bulwahn
parents:
45760
diff
changeset

8 
import System.IO 
43313  9 
import System.Exit 
46408
2520cd337056
using fully qualified module names in Haskell source, which seems to be required by GHC 7.0.4 (also cf. 0fd9ab902b5a)
bulwahn
parents:
45760
diff
changeset

10 
import Data.Maybe 
2520cd337056
using fully qualified module names in Haskell source, which seems to be required by GHC 7.0.4 (also cf. 0fd9ab902b5a)
bulwahn
parents:
45760
diff
changeset

11 
import Data.List (partition, findIndex) 
45081
f00e52acbd42
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowingbased Quickcheck
bulwahn
parents:
45003
diff
changeset

12 
import qualified Generated_Code 
43313  13 

14 

15 
type Pos = [Int] 

16 

17 
 Term refinement 

18 

19 
 Operation: termOf 

20 

21 
posOf :: Edge > Pos 

22 
posOf (VN pos _) = pos 

23 
posOf (CtrB pos _) = pos 

24 

25 
tailPosEdge :: Edge > Edge 

26 
tailPosEdge (VN pos ty) = VN (tail pos) ty 

27 
tailPosEdge (CtrB pos ts) = CtrB (tail pos) ts 

28 

45081
f00e52acbd42
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowingbased Quickcheck
bulwahn
parents:
45003
diff
changeset

29 
termOf :: Pos > Path > Generated_Code.Narrowing_term 
46758
4106258260b3
choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in QuickcheckNarrowing
bulwahn
parents:
46408
diff
changeset

30 
termOf pos (CtrB [] i : es) = Generated_Code.Narrowing_constructor i (termListOf pos es) 
4106258260b3
choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in QuickcheckNarrowing
bulwahn
parents:
46408
diff
changeset

31 
termOf pos [VN [] ty] = Generated_Code.Narrowing_variable pos ty 
43313  32 

45081
f00e52acbd42
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowingbased Quickcheck
bulwahn
parents:
45003
diff
changeset

33 
termListOf :: Pos > Path > [Generated_Code.Narrowing_term] 
43313  34 
termListOf pos es = termListOf' 0 es 
35 
where 

36 
termListOf' i [] = [] 

37 
termListOf' i (e : es) = 

38 
let 

46408
2520cd337056
using fully qualified module names in Haskell source, which seems to be required by GHC 7.0.4 (also cf. 0fd9ab902b5a)
bulwahn
parents:
45760
diff
changeset

39 
(ts, rs) = Data.List.partition (\e > head (posOf e) == i) (e : es) 
43313  40 
t = termOf (pos ++ [i]) (map tailPosEdge ts) 
41 
in 

42 
(t : termListOf' (i + 1) rs) 

43 
{ 

44 
conv :: [[Term] > a] > Term > a 

45 
conv cs (Var p _) = error ('\0':map toEnum p) 

46 
conv cs (Ctr i xs) = (cs !! i) xs 

47 
} 

48 
 Answers 

49 

50 
data Answer = Known Bool  Unknown Pos deriving Show; 

51 

45003
7591039fb6b4
catch PatternMatchFail exceptions in narrowingbased quickcheck
bulwahn
parents:
44751
diff
changeset

52 
answeri :: a > (a > IO b) > (Pos > IO b) > IO b; 
7591039fb6b4
catch PatternMatchFail exceptions in narrowingbased quickcheck
bulwahn
parents:
44751
diff
changeset

53 
answeri a known unknown = 
43313  54 
do res < try (evaluate a) 
55 
case res of 

56 
Right b > known b 

57 
Left (ErrorCall ('\0':p)) > unknown (map fromEnum p) 

58 
Left e > throw e 

59 

45685
e2e928af750b
quickcheck narrowing also shows potential counterexamples
bulwahn
parents:
45081
diff
changeset

60 
answer :: Bool > Bool > (Bool > IO b) > (Pos > IO b) > IO b; 
45760
3b5a735897c3
inverted flag potential to genuine_only in the quickcheck narrowing Haskell code
bulwahn
parents:
45685
diff
changeset

61 
answer genuine_only a known unknown = 
45003
7591039fb6b4
catch PatternMatchFail exceptions in narrowingbased quickcheck
bulwahn
parents:
44751
diff
changeset

62 
Control.Exception.catch (answeri a known unknown) 
45760
3b5a735897c3
inverted flag potential to genuine_only in the quickcheck narrowing Haskell code
bulwahn
parents:
45685
diff
changeset

63 
(\ (PatternMatchFail _) > known genuine_only) 
45003
7591039fb6b4
catch PatternMatchFail exceptions in narrowingbased quickcheck
bulwahn
parents:
44751
diff
changeset

64 

43313  65 
 Proofs and Refutation 
66 

67 
data Quantifier = ExistentialQ  UniversalQ 

68 

69 
data EvaluationResult = Eval Bool  UnknownValue Bool deriving Eq 

70 
{ 

71 
instance Show EvaluationResult where 

72 
show (Eval True) = "T" 

73 
show (Eval False) = "F" 

74 
show (UnknownValue False) = "U" 

75 
show (UnknownValue True) = "X" 

76 
} 

77 
uneval = UnknownValue True 

78 
unknown = UnknownValue False 

79 

80 
andOp :: EvaluationResult > EvaluationResult > EvaluationResult 

81 
andOp (Eval b1) (Eval b2) = Eval (b1 && b2) 

82 
andOp (Eval True) (UnknownValue b) = UnknownValue b 

83 
andOp (Eval False) (UnknownValue _) = Eval False 

84 
andOp (UnknownValue b) (Eval True) = UnknownValue b 

85 
andOp (UnknownValue _) (Eval False) = Eval False 

86 
andOp (UnknownValue b1) (UnknownValue b2) = UnknownValue (b1  b2) 

87 

88 
orOp :: EvaluationResult > EvaluationResult > EvaluationResult 

89 
orOp (Eval b1) (Eval b2) = Eval (b1  b2) 

90 
orOp (Eval False) (UnknownValue b) = UnknownValue b 

91 
orOp (Eval True) (UnknownValue _) = Eval True 

92 
orOp (UnknownValue b) (Eval False) = UnknownValue b 

93 
orOp (UnknownValue _) (Eval True) = Eval True 

94 
orOp (UnknownValue b1) (UnknownValue b2) = UnknownValue (b1 && b2) 

95 

96 

45081
f00e52acbd42
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowingbased Quickcheck
bulwahn
parents:
45003
diff
changeset

97 
data Edge = VN Pos Generated_Code.Narrowing_type  CtrB Pos Int 
43313  98 
type Path = [Edge] 
99 

100 
data QuantTree = Node EvaluationResult 

45081
f00e52acbd42
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowingbased Quickcheck
bulwahn
parents:
45003
diff
changeset

101 
 VarNode Quantifier EvaluationResult Pos Generated_Code.Narrowing_type QuantTree 
43313  102 
 CtrBranch Quantifier EvaluationResult Pos [QuantTree] 
103 
{ 

104 
instance Show QuantTree where 

105 
show (Node r) = "Node " ++ show r 

106 
show (VarNode q r p _ t) = "VarNode " ++ show q ++ " " ++ show r ++ " " ++ show p ++ " " ++ show t 

107 
show (CtrBranch q r p ts) = "CtrBranch " ++ show q ++ show r ++ show p ++ show ts 

108 
} 

109 
evalOf :: QuantTree > EvaluationResult 

110 
evalOf (Node r) = r 

111 
evalOf (VarNode _ r _ _ _) = r 

112 
evalOf (CtrBranch _ r _ _) = r 

113 

114 
 Operation find: finds first relevant unevaluated node and returns its path 

115 

116 
find :: QuantTree > Path 

117 
find (Node (UnknownValue True)) = [] 

118 
find (VarNode _ _ pos ty t) = VN pos ty : (find t) 

119 
find (CtrBranch _ _ pos ts) = CtrB pos i : find (ts !! i) 

120 
where 

121 
Just i = findIndex (\t > evalOf t == uneval) ts 

122 

123 
 Operation: updateNode ( and simplify) 

124 

125 
{ updates the Node and the stored evaluation results along the upper nodes } 

126 
updateNode :: Path > EvaluationResult > QuantTree > QuantTree 

127 
updateNode [] v (Node _) = Node v 

128 
updateNode (VN _ _ : es) v (VarNode q r p ty t) = VarNode q (evalOf t') p ty t' 

129 
where 

130 
t' = updateNode es v t 

131 
updateNode (CtrB _ i : es) v (CtrBranch q r pos ts) = CtrBranch q r' pos ts' 

132 
where 

133 
(xs, y : ys) = splitAt i ts 

134 
y' = updateNode es v y 

135 
ts' = xs ++ (y' : ys) 

136 
r' = foldl (\s t > oper s (evalOf t)) neutral ts' 

137 
(neutral, oper) = case q of { UniversalQ > (Eval True, andOp); ExistentialQ > (Eval False, orOp)} 

138 

139 
 Operation: refineTree 

140 

141 
updateTree :: (QuantTree > QuantTree) > Path > QuantTree > QuantTree 

142 
updateTree f [] t = (f t) 

143 
updateTree f (VN _ _ : es) (VarNode q r pos ty t) = VarNode q r pos ty (updateTree f es t) 

144 
updateTree f (CtrB _ i : es) (CtrBranch q r pos ts) = CtrBranch q r pos (xs ++ (updateTree f es y : ys)) 

145 
where 

146 
(xs, y : ys) = splitAt i ts 

147 

148 
refineTree :: [Edge] > Pos > QuantTree > QuantTree 

149 
refineTree es p t = updateTree refine (pathPrefix p es) t 

150 
where 

151 
pathPrefix p es = takeWhile (\e > posOf e /= p) es 

46758
4106258260b3
choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in QuickcheckNarrowing
bulwahn
parents:
46408
diff
changeset

152 
refine (VarNode q r p (Generated_Code.Narrowing_sum_of_products ps) t) = 
43313  153 
CtrBranch q r p [ foldr (\(i,ty) t > VarNode q r (p++[i]) ty t) t (zip [0..] ts)  ts < ps ] 
154 

155 
 refute 

156 

45685
e2e928af750b
quickcheck narrowing also shows potential counterexamples
bulwahn
parents:
45081
diff
changeset

157 
refute :: ([Generated_Code.Narrowing_term] > Bool) > Bool > Int > QuantTree > IO QuantTree 
45760
3b5a735897c3
inverted flag potential to genuine_only in the quickcheck narrowing Haskell code
bulwahn
parents:
45685
diff
changeset

158 
refute exec genuine_only d t = ref t 
43313  159 
where 
160 
ref t = 

161 
let path = find t in 

162 
do 

45760
3b5a735897c3
inverted flag potential to genuine_only in the quickcheck narrowing Haskell code
bulwahn
parents:
45685
diff
changeset

163 
t' < answer genuine_only (exec (termListOf [] path)) (\b > return (updateNode path (Eval b) t)) 
43313  164 
(\p > return (if length p < d then refineTree path p t else updateNode path unknown t)); 
165 
case evalOf t' of 

166 
UnknownValue True > ref t' 

167 
_ > return t' 

168 

45685
e2e928af750b
quickcheck narrowing also shows potential counterexamples
bulwahn
parents:
45081
diff
changeset

169 
depthCheck :: Bool > Int > Generated_Code.Property > IO () 
45760
3b5a735897c3
inverted flag potential to genuine_only in the quickcheck narrowing Haskell code
bulwahn
parents:
45685
diff
changeset

170 
depthCheck genuine_only d p = refute (checkOf p) genuine_only d (treeOf 0 p) >>= (\t > 
43313  171 
case evalOf t of 
172 
Eval False > putStrLn ("SOME (" ++ show (counterexampleOf (reifysOf p) (exampleOf 0 t)) ++ ")") 

173 
_ > putStrLn ("NONE")) 

174 

175 

176 
 presentation of counterexample 

177 

178 

45081
f00e52acbd42
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowingbased Quickcheck
bulwahn
parents:
45003
diff
changeset

179 
instance Show Generated_Code.Typerep where { 
f00e52acbd42
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowingbased Quickcheck
bulwahn
parents:
45003
diff
changeset

180 
show (Generated_Code.Typerep c ts) = "Type (\"" ++ c ++ "\", " ++ show ts ++ ")"; 
43313  181 
}; 
182 

45081
f00e52acbd42
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowingbased Quickcheck
bulwahn
parents:
45003
diff
changeset

183 
instance Show Generated_Code.Term where { 
f00e52acbd42
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowingbased Quickcheck
bulwahn
parents:
45003
diff
changeset

184 
show (Generated_Code.Const c t) = "Const (\"" ++ c ++ "\", " ++ show t ++ ")"; 
f00e52acbd42
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowingbased Quickcheck
bulwahn
parents:
45003
diff
changeset

185 
show (Generated_Code.App s t) = "(" ++ show s ++ ") $ (" ++ show t ++ ")"; 
f00e52acbd42
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowingbased Quickcheck
bulwahn
parents:
45003
diff
changeset

186 
show (Generated_Code.Abs s ty t) = "Abs (\"" ++ s ++ "\", " ++ show ty ++ ", " ++ show t ++ ")"; 
f00e52acbd42
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowingbased Quickcheck
bulwahn
parents:
45003
diff
changeset

187 
show (Generated_Code.Free s ty) = "Free (\"" ++ s ++ "\", " ++ show ty ++ ")"; 
43313  188 
}; 
189 
{ 

190 
posOf :: Edge > Pos 

191 
posOf (VN pos _) = pos 

192 
posOf (CtrB pos _) = pos 

193 

194 
tailPosEdge :: Edge > Edge 

195 
tailPosEdge (VN pos ty) = VN (tail pos) ty 

196 
tailPosEdge (CtrB pos ts) = CtrB (tail pos) ts 

197 

198 
termOf :: Pos > Tree > (Narrowing_term, Tree) 

199 
termOf pos = if Ctr i (termListOf (pos ++ [i]) ) 

200 
termOf pos [VN [] ty] = Var pos ty 

201 

202 
termListOf :: Pos > [Narrowing_term] 

203 
termListOf pos es = termListOf' 0 es 

204 
where 

205 
termListOf' i [] = [] 

206 
termListOf' i (e : es) = 

207 
let 

208 
(ts, rs) = List.partition (\e > head (posOf e) == i) (e : es) 

209 
t = termOf (pos ++ [i]) (map tailPosEdge ts) 

210 
in 

211 
(t : termListOf' (i + 1) rs) 

212 

213 
termlist_of :: Pos > QuantTree > ([Term], QuantTree) 

214 

215 
termlist_of p' (Node r) 

216 

217 
term_of p' (VarNode _ _ p ty t) = if p == p' then 

218 
(Some (Var ty), t) 

219 
else 

220 
(None, t) 

221 
term_of p' (CtrBranch q _ p ts) = 

222 
if p == p' then 

223 
let 

224 
i = findindex (\t > evalOf t == Eval False) 

225 
in 

226 
Ctr i (termlist_of (p ++ [i]) (ts ! i) []) 

227 
else 

228 
error "" 

229 
} 

45081
f00e52acbd42
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowingbased Quickcheck
bulwahn
parents:
45003
diff
changeset

230 
termlist_of :: Pos > ([Generated_Code.Narrowing_term], QuantTree) > ([Generated_Code.Narrowing_term], QuantTree) 
43313  231 
termlist_of p' (terms, Node b) = (terms, Node b) 
232 
termlist_of p' (terms, VarNode q r p ty t) = if p' == take (length p') p then 

46758
4106258260b3
choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in QuickcheckNarrowing
bulwahn
parents:
46408
diff
changeset

233 
termlist_of p' (terms ++ [Generated_Code.Narrowing_variable p ty], t) 
43313  234 
else 
235 
(terms, VarNode q r p ty t) 

236 
termlist_of p' (terms, CtrBranch q r p ts) = if p' == take (length p') p then 

237 
let 

238 
Just i = findIndex (\t > evalOf t == Eval False) ts 

239 
(subterms, t') = fixp (\j > termlist_of (p ++ [j])) 0 ([], ts !! i) 

240 
in 

46758
4106258260b3
choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in QuickcheckNarrowing
bulwahn
parents:
46408
diff
changeset

241 
(terms ++ [Generated_Code.Narrowing_constructor i subterms], t') 
43313  242 
else 
243 
(terms, CtrBranch q r p ts) 

244 
where 

245 
fixp f j s = if length (fst (f j s)) == length (fst s) then s else fixp f (j + 1) (f j s) 

246 

247 

45081
f00e52acbd42
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowingbased Quickcheck
bulwahn
parents:
45003
diff
changeset

248 
alltermlist_of :: Pos > ([Generated_Code.Narrowing_term], QuantTree) > [([Generated_Code.Narrowing_term], QuantTree)] 
43313  249 
alltermlist_of p' (terms, Node b) = [(terms, Node b)] 
250 
alltermlist_of p' (terms, VarNode q r p ty t) = if p' == take (length p') p then 

46758
4106258260b3
choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in QuickcheckNarrowing
bulwahn
parents:
46408
diff
changeset

251 
alltermlist_of p' (terms ++ [Generated_Code.Narrowing_variable p ty], t) 
43313  252 
else 
253 
[(terms, VarNode q r p ty t)] 

254 
alltermlist_of p' (terms, CtrBranch q r p ts) = 

255 
if p' == take (length p') p then 

256 
let 

257 
its = filter (\(i, t) > evalOf t == Eval False) (zip [0..] ts) 

258 
in 

259 
concatMap 

46758
4106258260b3
choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in QuickcheckNarrowing
bulwahn
parents:
46408
diff
changeset

260 
(\(i, t) > map (\(subterms, t') > (terms ++ [Generated_Code.Narrowing_constructor i subterms], t')) 
43313  261 
(fixp (\j > alltermlist_of (p ++ [j])) 0 ([], t))) its 
262 
else 

263 
[(terms, CtrBranch q r p ts)] 

264 
where 

265 
fixp f j s = case (f j s) of 

266 
[s'] > if length (fst s') == length (fst s) then [s'] else concatMap (fixp f (j + 1)) (f j s) 

267 
_ > concatMap (fixp f (j + 1)) (f j s) 

268 

45081
f00e52acbd42
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowingbased Quickcheck
bulwahn
parents:
45003
diff
changeset

269 
data Example = UnivExample Generated_Code.Narrowing_term Example  ExExample [(Generated_Code.Narrowing_term, Example)]  EmptyExample 
43313  270 

271 
quantifierOf (VarNode q _ _ _ _) = q 

272 
quantifierOf (CtrBranch q _ _ _) = q 

273 

274 
exampleOf :: Int > QuantTree > Example 

275 
exampleOf _ (Node _) = EmptyExample 

276 
exampleOf p t = 

277 
case quantifierOf t of 

278 
UniversalQ > 

279 
let 

280 
([term], rt) = termlist_of [p] ([], t) 

281 
in UnivExample term (exampleOf (p + 1) rt) 

282 
ExistentialQ > 

283 
ExExample (map (\([term], rt) > (term, exampleOf (p + 1) rt)) (alltermlist_of [p] ([], t))) 

284 

45081
f00e52acbd42
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowingbased Quickcheck
bulwahn
parents:
45003
diff
changeset

285 
data Counterexample = Universal_Counterexample (Generated_Code.Term, Counterexample) 
f00e52acbd42
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowingbased Quickcheck
bulwahn
parents:
45003
diff
changeset

286 
 Existential_Counterexample [(Generated_Code.Term, Counterexample)]  Empty_Assignment 
43313  287 

288 
instance Show Counterexample where { 

289 
show Empty_Assignment = "Narrowing_Generators.Empty_Assignment"; 

290 
show (Universal_Counterexample x) = "Narrowing_Generators.Universal_Counterexample" ++ show x; 

291 
show (Existential_Counterexample x) = "Narrowing_Generators.Existential_Counterexample" ++ show x; 

292 
}; 

293 

45081
f00e52acbd42
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowingbased Quickcheck
bulwahn
parents:
45003
diff
changeset

294 
counterexampleOf :: [Generated_Code.Narrowing_term > Generated_Code.Term] > Example > Counterexample 
43313  295 
counterexampleOf [] EmptyExample = Empty_Assignment 
296 
counterexampleOf (reify : reifys) (UnivExample t ex) = Universal_Counterexample (reify t, counterexampleOf reifys ex) 

297 
counterexampleOf (reify : reifys) (ExExample exs) = Existential_Counterexample (map (\(t, ex) > (reify t, counterexampleOf reifys ex)) exs) 

298 

45081
f00e52acbd42
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowingbased Quickcheck
bulwahn
parents:
45003
diff
changeset

299 
checkOf :: Generated_Code.Property > [Generated_Code.Narrowing_term] > Bool 
f00e52acbd42
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowingbased Quickcheck
bulwahn
parents:
45003
diff
changeset

300 
checkOf (Generated_Code.Property b) = (\[] > b) 
f00e52acbd42
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowingbased Quickcheck
bulwahn
parents:
45003
diff
changeset

301 
checkOf (Generated_Code.Universal _ f _) = (\(t : ts) > checkOf (f t) ts) 
f00e52acbd42
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowingbased Quickcheck
bulwahn
parents:
45003
diff
changeset

302 
checkOf (Generated_Code.Existential _ f _) = (\(t : ts) > checkOf (f t) ts) 
43313  303 

47090
6b53d954255b
adjusting to longer names in PNF_Narrowing_Engine, which was overlooked in 4106258260b3
bulwahn
parents:
46758
diff
changeset

304 
dummy = Generated_Code.Narrowing_variable [] (Generated_Code.Narrowing_sum_of_products [[]]) 
43313  305 

45081
f00e52acbd42
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowingbased Quickcheck
bulwahn
parents:
45003
diff
changeset

306 
treeOf :: Int > Generated_Code.Property > QuantTree 
f00e52acbd42
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowingbased Quickcheck
bulwahn
parents:
45003
diff
changeset

307 
treeOf n (Generated_Code.Property _) = Node uneval 
f00e52acbd42
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowingbased Quickcheck
bulwahn
parents:
45003
diff
changeset

308 
treeOf n (Generated_Code.Universal ty f _) = VarNode UniversalQ uneval [n] ty (treeOf (n + 1) (f dummy)) 
f00e52acbd42
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowingbased Quickcheck
bulwahn
parents:
45003
diff
changeset

309 
treeOf n (Generated_Code.Existential ty f _) = VarNode ExistentialQ uneval [n] ty (treeOf (n + 1) (f dummy)) 
43313  310 

45081
f00e52acbd42
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowingbased Quickcheck
bulwahn
parents:
45003
diff
changeset

311 
reifysOf :: Generated_Code.Property > [Generated_Code.Narrowing_term > Generated_Code.Term] 
f00e52acbd42
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowingbased Quickcheck
bulwahn
parents:
45003
diff
changeset

312 
reifysOf (Generated_Code.Property _) = [] 
f00e52acbd42
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowingbased Quickcheck
bulwahn
parents:
45003
diff
changeset

313 
reifysOf (Generated_Code.Universal _ f r) = (r : (reifysOf (f dummy))) 
f00e52acbd42
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowingbased Quickcheck
bulwahn
parents:
45003
diff
changeset

314 
reifysOf (Generated_Code.Existential _ f r) = (r : (reifysOf (f dummy))) 
43313  315 