author  bulwahn 
Mon, 26 Sep 2011 10:30:37 +0200  
changeset 45081  f00e52acbd42 
parent 45003  7591039fb6b4 
child 45685  e2e928af750b 
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 

6 
import Monad 

7 
import Control.Exception 

8 
import System.Exit 

9 
import Maybe 

10 
import 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

11 
import qualified Generated_Code 
43313  12 

13 

14 
type Pos = [Int] 

15 

16 
 Term refinement 

17 

18 
 Operation: termOf 

19 

20 
posOf :: Edge > Pos 

21 
posOf (VN pos _) = pos 

22 
posOf (CtrB pos _) = pos 

23 

24 
tailPosEdge :: Edge > Edge 

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

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

27 

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

28 
termOf :: Pos > Path > Generated_Code.Narrowing_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

29 
termOf pos (CtrB [] i : es) = Generated_Code.Ctr i (termListOf pos es) 
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

30 
termOf pos [VN [] ty] = Generated_Code.Var pos ty 
43313  31 

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

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

35 
termListOf' i [] = [] 

36 
termListOf' i (e : es) = 

37 
let 

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

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

40 
in 

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

42 
{ 

43 
conv :: [[Term] > a] > Term > a 

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

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

46 
} 

47 
 Answers 

48 

49 
data Answer = Known Bool  Unknown Pos deriving Show; 

50 

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

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

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

55 
Right b > known b 

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

57 
Left e > throw e 

58 

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

59 
answer :: Bool > (Bool > IO b) > (Pos > IO b) > IO b; 
7591039fb6b4
catch PatternMatchFail exceptions in narrowingbased quickcheck
bulwahn
parents:
44751
diff
changeset

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

61 
Control.Exception.catch (answeri a known unknown) 
7591039fb6b4
catch PatternMatchFail exceptions in narrowingbased quickcheck
bulwahn
parents:
44751
diff
changeset

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

63 

43313  64 
 Proofs and Refutation 
65 

66 
data Quantifier = ExistentialQ  UniversalQ 

67 

68 
data EvaluationResult = Eval Bool  UnknownValue Bool deriving Eq 

69 
{ 

70 
instance Show EvaluationResult where 

71 
show (Eval True) = "T" 

72 
show (Eval False) = "F" 

73 
show (UnknownValue False) = "U" 

74 
show (UnknownValue True) = "X" 

75 
} 

76 
uneval = UnknownValue True 

77 
unknown = UnknownValue False 

78 

79 
andOp :: EvaluationResult > EvaluationResult > EvaluationResult 

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

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

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

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

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

85 
andOp (UnknownValue b1) (UnknownValue b2) = UnknownValue (b1  b2) 

86 

87 
orOp :: EvaluationResult > EvaluationResult > EvaluationResult 

88 
orOp (Eval b1) (Eval b2) = Eval (b1  b2) 

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

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

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

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

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

94 

95 

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

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

99 
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

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

103 
instance Show QuantTree where 

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

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

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

107 
} 

108 
evalOf :: QuantTree > EvaluationResult 

109 
evalOf (Node r) = r 

110 
evalOf (VarNode _ r _ _ _) = r 

111 
evalOf (CtrBranch _ r _ _) = r 

112 

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

114 

115 
find :: QuantTree > Path 

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

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

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

119 
where 

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

121 

122 
 Operation: updateNode ( and simplify) 

123 

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

125 
updateNode :: Path > EvaluationResult > QuantTree > QuantTree 

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

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

128 
where 

129 
t' = updateNode es v t 

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

131 
where 

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

133 
y' = updateNode es v y 

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

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

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

137 

138 
 Operation: refineTree 

139 

140 
updateTree :: (QuantTree > QuantTree) > Path > QuantTree > QuantTree 

141 
updateTree f [] t = (f t) 

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

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

144 
where 

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

146 

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

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

149 
where 

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

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

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

154 
 refute 

155 

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

156 
refute :: ([Generated_Code.Narrowing_term] > Bool) > Int > QuantTree > IO QuantTree 
43313  157 
refute exec d t = ref t 
158 
where 

159 
ref t = 

160 
let path = find t in 

161 
do 

162 
t' < answer (exec (termListOf [] path)) (\b > return (updateNode path (Eval b) t)) 

163 
(\p > return (if length p < d then refineTree path p t else updateNode path unknown t)); 

164 
case evalOf t' of 

165 
UnknownValue True > ref t' 

166 
_ > return t' 

167 

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

168 
depthCheck :: Int > Generated_Code.Property > IO () 
43313  169 
depthCheck d p = refute (checkOf p) d (treeOf 0 p) >>= (\t > 
170 
case evalOf t of 

171 
Eval False > putStrLn ("SOME (" ++ show (counterexampleOf (reifysOf p) (exampleOf 0 t)) ++ ")") 

172 
_ > putStrLn ("NONE")) 

173 

174 

175 
 presentation of counterexample 

176 

177 

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

178 
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

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

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

182 
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

183 
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

184 
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

185 
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

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

189 
posOf :: Edge > Pos 

190 
posOf (VN pos _) = pos 

191 
posOf (CtrB pos _) = pos 

192 

193 
tailPosEdge :: Edge > Edge 

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

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

196 

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

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

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

200 

201 
termListOf :: Pos > [Narrowing_term] 

202 
termListOf pos es = termListOf' 0 es 

203 
where 

204 
termListOf' i [] = [] 

205 
termListOf' i (e : es) = 

206 
let 

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

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

209 
in 

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

211 

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

213 

214 
termlist_of p' (Node r) 

215 

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

217 
(Some (Var ty), t) 

218 
else 

219 
(None, t) 

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

221 
if p == p' then 

222 
let 

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

224 
in 

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

226 
else 

227 
error "" 

228 
} 

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

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

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

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

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

236 
let 

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

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

239 
in 

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

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

243 
where 

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

245 

246 

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

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

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

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

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

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

255 
let 

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

257 
in 

258 
concatMap 

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

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

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

263 
where 

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

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

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

267 

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

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

270 
quantifierOf (VarNode q _ _ _ _) = q 

271 
quantifierOf (CtrBranch q _ _ _) = q 

272 

273 
exampleOf :: Int > QuantTree > Example 

274 
exampleOf _ (Node _) = EmptyExample 

275 
exampleOf p t = 

276 
case quantifierOf t of 

277 
UniversalQ > 

278 
let 

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

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

281 
ExistentialQ > 

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

283 

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

284 
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

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

287 
instance Show Counterexample where { 

288 
show Empty_Assignment = "Narrowing_Generators.Empty_Assignment"; 

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

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

291 
}; 

292 

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

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

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

297 

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

298 
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

299 
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

300 
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

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

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

303 
dummy = Generated_Code.Var [] (Generated_Code.SumOfProd [[]]) 
43313  304 

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

305 
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

306 
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

307 
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

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

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

310 
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

311 
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

312 
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

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