src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs
changeset 49193 0067d83414c8
parent 47090 6b53d954255b
child 49253 4b11240d80bf
equal deleted inserted replaced
49192:d383fd5dbd3c 49193:0067d83414c8
     9 import System.Exit
     9 import System.Exit
    10 import Data.Maybe
    10 import Data.Maybe
    11 import Data.List (partition, findIndex)
    11 import Data.List (partition, findIndex)
    12 import qualified Generated_Code
    12 import qualified Generated_Code
    13 
    13 
    14 
       
    15 type Pos = [Int]
    14 type Pos = [Int]
    16 
    15 
       
    16 --  Refinement Tree
       
    17 
       
    18 data Quantifier = Existential | Universal
       
    19 
       
    20 data Truth = Eval Bool | Unevaluated | Unknown deriving Eq
       
    21 
       
    22 conj :: Truth -> Truth -> Truth
       
    23 conj (Eval True) b = b
       
    24 conj (Eval False) _ = Eval False
       
    25 conj b (Eval True) = b
       
    26 conj _ (Eval False) = Eval False
       
    27 conj Unevaluated _ = Unevaluated
       
    28 conj _ Unevaluated = Unevaluated
       
    29 conj Unknown Unknown = Unknown
       
    30 
       
    31 disj :: Truth -> Truth -> Truth
       
    32 disj (Eval True) _ = Eval True
       
    33 disj (Eval False) b = b
       
    34 disj _ (Eval True) = Eval True
       
    35 disj b (Eval False) = b
       
    36 disj Unknown _ = Unknown
       
    37 disj _ Unknown = Unknown
       
    38 disj Unevaluated Unevaluated = Unevaluated
       
    39 
       
    40 ball ts = foldl (\s t -> conj s (value_of t)) (Eval True) ts
       
    41 bexists ts = foldl (\s t -> disj s (value_of t)) (Eval False) ts
       
    42 
       
    43 data Tree = Leaf Truth
       
    44   | Variable Quantifier Truth Pos Generated_Code.Narrowing_type Tree
       
    45   | Constructor Quantifier Truth Pos [Tree]
       
    46 
       
    47 value_of :: Tree -> Truth
       
    48 value_of (Leaf r) = r
       
    49 value_of (Variable _ r _ _ _) = r
       
    50 value_of (Constructor _ r _ _) = r
       
    51 
       
    52 data Edge = V Pos Generated_Code.Narrowing_type | C Pos Int
       
    53 type Path = [Edge]
       
    54 
       
    55 position_of :: Edge -> Pos
       
    56 position_of (V pos _) = pos
       
    57 position_of (C pos _) = pos
       
    58 
       
    59 -- Operation find: finds first relevant unevaluated node and returns its path
       
    60 
       
    61 find :: Tree -> Path
       
    62 find (Leaf Unevaluated) = []
       
    63 find (Variable _ _ pos ty t) = V pos ty : (find t)
       
    64 find (Constructor _ _ pos ts) = C pos i : find (ts !! i)
       
    65   where  
       
    66     Just i = findIndex (\t -> value_of t == Unevaluated) ts
       
    67 
       
    68 -- Operation update: updates the leaf and the cached truth values results along the path
       
    69 
       
    70 update :: Path -> Truth -> Tree -> Tree
       
    71 update [] v (Leaf _) = Leaf v
       
    72 update (V _ _ : es) v (Variable q r p ty t) = Variable q (value_of t') p ty t'
       
    73   where
       
    74     t' = update es v t    
       
    75 update (C _ i : es) v (Constructor q r pos ts) = Constructor q r' pos ts' 
       
    76   where
       
    77     (xs, y : ys) = splitAt i ts
       
    78     y' = update es v y
       
    79     ts' = xs ++ (y' : ys)
       
    80     r' = valueOf ts'
       
    81     valueOf = case q of { Universal -> ball; Existential -> bexists}
       
    82  
       
    83 -- Operation: refineTree
       
    84 
       
    85 replace :: (Tree -> Tree) -> Path -> Tree -> Tree
       
    86 replace f [] t = (f t)
       
    87 replace f (V _ _ : es) (Variable q r pos ty t) = Variable q r pos ty (replace f es t)
       
    88 replace f (C _ i : es) (Constructor q r pos ts) = Constructor q r pos (xs ++ (replace f es y : ys))
       
    89    where
       
    90      (xs, y : ys) = splitAt i ts
       
    91 
       
    92 refine_tree :: [Edge] -> Pos -> Tree -> Tree
       
    93 refine_tree es p t = replace refine (path_of_position p es) t
       
    94   where
       
    95     path_of_position p es = takeWhile (\e -> position_of e /= p) es  
       
    96     refine (Variable q r p (Generated_Code.Narrowing_sum_of_products ps) t) =
       
    97       Constructor q r p [ foldr (\(i,ty) t -> Variable q r (p++[i]) ty t) t (zip [0..] ts) | ts <- ps ]
       
    98 
       
    99 -- refute
       
   100 
       
   101 refute :: ([Generated_Code.Narrowing_term] -> Bool) -> Bool -> Int -> Tree -> IO Tree
       
   102 refute exec genuine_only d t = ref t
       
   103   where
       
   104     ref t =
       
   105       let path = find t in
       
   106         do
       
   107           t' <- answer genuine_only (exec (terms_of [] path)) (\b -> return (update path (Eval b) t))
       
   108             (\p -> return (if length p < d then refine_tree path p t else update path Unknown t));
       
   109           case value_of t' of
       
   110             Unevaluated -> ref t'
       
   111             _ -> return t'
       
   112 
       
   113 depthCheck :: Bool -> Int -> Generated_Code.Property -> IO ()
       
   114 depthCheck genuine_only d p = refute (checkOf p) genuine_only d (treeOf 0 p) >>= (\t -> 
       
   115   case value_of t of
       
   116    Eval False -> putStrLn ("SOME (" ++ show (counterexampleOf (reifysOf p) (exampleOf 0 t)) ++ ")")  
       
   117    _ -> putStrLn ("NONE"))
       
   118 
    17 -- Term refinement
   119 -- Term refinement
    18 
   120 
    19 -- Operation: termOf
   121 -- Operation: termOf
    20 
   122 
    21 posOf :: Edge -> Pos
   123 term_of :: Pos -> Path -> Generated_Code.Narrowing_term
    22 posOf (VN pos _) = pos
   124 term_of p (C [] i : es) = Generated_Code.Narrowing_constructor i (terms_of p es)
    23 posOf (CtrB pos _) = pos
   125 term_of p [V [] ty] = Generated_Code.Narrowing_variable p ty
    24 
   126 
    25 tailPosEdge :: Edge -> Edge
   127 terms_of :: Pos -> Path -> [Generated_Code.Narrowing_term]
    26 tailPosEdge (VN pos ty) = VN (tail pos) ty
   128 terms_of p es = terms_of' 0 es
    27 tailPosEdge (CtrB pos ts) = CtrB (tail pos) ts
   129   where
    28 
   130     terms_of' i [] = []
    29 termOf :: Pos -> Path -> Generated_Code.Narrowing_term
   131     terms_of' i (e : es) = (t : terms_of' (i + 1) rs) 
    30 termOf pos (CtrB [] i : es) = Generated_Code.Narrowing_constructor i (termListOf pos es)
   132       where
    31 termOf pos [VN [] ty] = Generated_Code.Narrowing_variable pos ty
   133         (ts, rs) = Data.List.partition (\e -> head (position_of e) == i) (e : es)
    32 
   134         t = term_of (p ++ [i]) (map (map_pos tail) ts)
    33 termListOf :: Pos -> Path -> [Generated_Code.Narrowing_term]
   135         map_pos f (V p ty) = V (f p) ty
    34 termListOf pos es = termListOf' 0 es
   136         map_pos f (C p ts) = C (f p) ts
    35   where
   137 
    36     termListOf' i [] = []
       
    37     termListOf' i (e : es) =
       
    38       let 
       
    39         (ts, rs) = Data.List.partition (\e -> head (posOf e) == i) (e : es)
       
    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
   138 -- Answers
    49 
   139 
    50 data Answer = Known Bool | Unknown Pos deriving Show;
   140 data Answer = Known Bool | Refine Pos;
    51 
   141 
    52 answeri :: a -> (a -> IO b) -> (Pos -> IO b) -> IO b;
   142 answeri :: a -> (a -> IO b) -> (Pos -> IO b) -> IO b;
    53 answeri a known unknown =
   143 answeri a known unknown =
    54   do res <- try (evaluate a)
   144   do res <- try (evaluate a)
    55      case res of
   145      case res of
    59 
   149 
    60 answer :: Bool -> Bool -> (Bool -> IO b) -> (Pos -> IO b) -> IO b;
   150 answer :: Bool -> Bool -> (Bool -> IO b) -> (Pos -> IO b) -> IO b;
    61 answer genuine_only a known unknown =
   151 answer genuine_only a known unknown =
    62   Control.Exception.catch (answeri a known unknown) 
   152   Control.Exception.catch (answeri a known unknown) 
    63     (\ (PatternMatchFail _) -> known genuine_only)
   153     (\ (PatternMatchFail _) -> known genuine_only)
    64 
       
    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 
       
    97 data Edge = VN Pos Generated_Code.Narrowing_type | CtrB Pos Int
       
    98 type Path = [Edge]
       
    99 
       
   100 data QuantTree = Node EvaluationResult
       
   101   | VarNode Quantifier EvaluationResult Pos Generated_Code.Narrowing_type QuantTree
       
   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  
       
   152     refine (VarNode q r p (Generated_Code.Narrowing_sum_of_products ps) t) =
       
   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 
       
   157 refute :: ([Generated_Code.Narrowing_term] -> Bool) -> Bool -> Int -> QuantTree -> IO QuantTree
       
   158 refute exec genuine_only d t = ref t
       
   159   where
       
   160     ref t =
       
   161       let path = find t in
       
   162         do
       
   163           t' <- answer genuine_only (exec (termListOf [] path)) (\b -> return (updateNode path (Eval b) t))
       
   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 
       
   169 depthCheck :: Bool -> Int -> Generated_Code.Property -> IO ()
       
   170 depthCheck genuine_only d p = refute (checkOf p) genuine_only d (treeOf 0 p) >>= (\t -> 
       
   171   case evalOf t of
       
   172    Eval False -> putStrLn ("SOME (" ++ show (counterexampleOf (reifysOf p) (exampleOf 0 t)) ++ ")")  
       
   173    _ -> putStrLn ("NONE"))
       
   174 
   154 
   175 
   155 
   176 -- presentation of counterexample
   156 -- presentation of counterexample
   177 
   157 
   178 
   158 
   225     in
   205     in
   226       Ctr i (termlist_of (p ++ [i])  (ts ! i) [])
   206       Ctr i (termlist_of (p ++ [i])  (ts ! i) [])
   227   else
   207   else
   228     error ""
   208     error ""
   229 -}
   209 -}
   230 termlist_of :: Pos -> ([Generated_Code.Narrowing_term], QuantTree) -> ([Generated_Code.Narrowing_term], QuantTree)
   210 termlist_of :: Pos -> ([Generated_Code.Narrowing_term], Tree) -> ([Generated_Code.Narrowing_term], Tree)
   231 termlist_of p' (terms, Node b) = (terms, Node b) 
   211 termlist_of p' (terms, Leaf b) = (terms, Leaf b) 
   232 termlist_of p' (terms, VarNode q r p ty t) = if p' == take (length p') p then
   212 termlist_of p' (terms, Variable q r p ty t) = if p' == take (length p') p then
   233     termlist_of p' (terms ++ [Generated_Code.Narrowing_variable p ty], t)
   213     termlist_of p' (terms ++ [Generated_Code.Narrowing_variable p ty], t)
   234   else
   214   else
   235     (terms, VarNode q r p ty t)
   215     (terms, Variable q r p ty t)
   236 termlist_of p' (terms, CtrBranch q r p ts) = if p' == take (length p') p then
   216 termlist_of p' (terms, Constructor q r p ts) = if p' == take (length p') p then
   237     let
   217     let
   238       Just i = findIndex (\t -> evalOf t == Eval False) ts
   218       Just i = findIndex (\t -> value_of t == Eval False) ts
   239       (subterms, t') = fixp (\j -> termlist_of (p ++ [j])) 0 ([], ts !! i)
   219       (subterms, t') = fixp (\j -> termlist_of (p ++ [j])) 0 ([], ts !! i)
   240     in
   220     in
   241       (terms ++ [Generated_Code.Narrowing_constructor i subterms], t')
   221       (terms ++ [Generated_Code.Narrowing_constructor i subterms], t')
   242   else
   222   else
   243     (terms, CtrBranch q r p ts)
   223     (terms, Constructor q r p ts)
   244   where
   224   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)
   225     fixp f j s = if length (fst (f j s)) == length (fst s) then s else fixp f (j + 1) (f j s)
   246 
   226 
   247 
   227 
   248 alltermlist_of :: Pos -> ([Generated_Code.Narrowing_term], QuantTree) -> [([Generated_Code.Narrowing_term], QuantTree)]
   228 alltermlist_of :: Pos -> ([Generated_Code.Narrowing_term], Tree) -> [([Generated_Code.Narrowing_term], Tree)]
   249 alltermlist_of p' (terms, Node b) = [(terms, Node b)] 
   229 alltermlist_of p' (terms, Leaf b) = [(terms, Leaf b)] 
   250 alltermlist_of p' (terms, VarNode q r p ty t) = if p' == take (length p') p then
   230 alltermlist_of p' (terms, Variable q r p ty t) = if p' == take (length p') p then
   251     alltermlist_of p' (terms ++ [Generated_Code.Narrowing_variable p ty], t)
   231     alltermlist_of p' (terms ++ [Generated_Code.Narrowing_variable p ty], t)
   252   else
   232   else
   253     [(terms, VarNode q r p ty t)]
   233     [(terms, Variable q r p ty t)]
   254 alltermlist_of p' (terms, CtrBranch q r p ts) =
   234 alltermlist_of p' (terms, Constructor q r p ts) =
   255   if p' == take (length p') p then
   235   if p' == take (length p') p then
   256     let
   236     let
   257       its = filter (\(i, t) -> evalOf t == Eval False) (zip [0..] ts)
   237       its = filter (\(i, t) -> value_of t == Eval False) (zip [0..] ts)
   258     in
   238     in
   259       concatMap
   239       concatMap
   260         (\(i, t) -> map (\(subterms, t') -> (terms ++ [Generated_Code.Narrowing_constructor i subterms], t'))
   240         (\(i, t) -> map (\(subterms, t') -> (terms ++ [Generated_Code.Narrowing_constructor i subterms], t'))
   261            (fixp (\j -> alltermlist_of (p ++ [j])) 0 ([], t))) its
   241            (fixp (\j -> alltermlist_of (p ++ [j])) 0 ([], t))) its
   262   else
   242   else
   263     [(terms, CtrBranch q r p ts)]
   243     [(terms, Constructor q r p ts)]
   264   where
   244   where
   265     fixp f j s = case (f j s) of
   245     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)
   246       [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)
   247       _ -> concatMap (fixp f (j + 1)) (f j s)
   268 
   248 
   269 data Example = UnivExample Generated_Code.Narrowing_term Example | ExExample [(Generated_Code.Narrowing_term, Example)] | EmptyExample
   249 data Example = UnivExample Generated_Code.Narrowing_term Example | ExExample [(Generated_Code.Narrowing_term, Example)] | EmptyExample
   270 
   250 
   271 quantifierOf (VarNode q _ _ _ _) = q
   251 quantifierOf (Variable q _ _ _ _) = q
   272 quantifierOf (CtrBranch q _ _ _) = q
   252 quantifierOf (Constructor q _ _ _) = q
   273 
   253 
   274 exampleOf :: Int -> QuantTree -> Example
   254 exampleOf :: Int -> Tree -> Example
   275 exampleOf _ (Node _) = EmptyExample
   255 exampleOf _ (Leaf _) = EmptyExample
   276 exampleOf p t =
   256 exampleOf p t =
   277    case quantifierOf t of
   257    case quantifierOf t of
   278      UniversalQ ->
   258      Universal ->
   279        let
   259        let
   280          ([term], rt) = termlist_of [p] ([], t)
   260          ([term], rt) = termlist_of [p] ([], t)
   281        in UnivExample term (exampleOf (p + 1) rt)
   261        in UnivExample term (exampleOf (p + 1) rt)
   282      ExistentialQ ->
   262      Existential ->
   283        ExExample (map (\([term], rt) -> (term, exampleOf (p + 1) rt)) (alltermlist_of [p] ([], t)))
   263        ExExample (map (\([term], rt) -> (term, exampleOf (p + 1) rt)) (alltermlist_of [p] ([], t)))
   284 
   264 
   285 data Counterexample = Universal_Counterexample (Generated_Code.Term, Counterexample)
   265 data Counterexample = Universal_Counterexample (Generated_Code.Term, Counterexample)
   286   | Existential_Counterexample [(Generated_Code.Term, Counterexample)] | Empty_Assignment
   266   | Existential_Counterexample [(Generated_Code.Term, Counterexample)] | Empty_Assignment
   287   
   267   
   301 checkOf (Generated_Code.Universal _ f _) = (\(t : ts) -> checkOf (f t) ts)
   281 checkOf (Generated_Code.Universal _ f _) = (\(t : ts) -> checkOf (f t) ts)
   302 checkOf (Generated_Code.Existential _ f _) = (\(t : ts) -> checkOf (f t) ts)
   282 checkOf (Generated_Code.Existential _ f _) = (\(t : ts) -> checkOf (f t) ts)
   303 
   283 
   304 dummy = Generated_Code.Narrowing_variable [] (Generated_Code.Narrowing_sum_of_products [[]])
   284 dummy = Generated_Code.Narrowing_variable [] (Generated_Code.Narrowing_sum_of_products [[]])
   305 
   285 
   306 treeOf :: Int -> Generated_Code.Property -> QuantTree
   286 treeOf :: Int -> Generated_Code.Property -> Tree
   307 treeOf n (Generated_Code.Property _) = Node uneval
   287 treeOf n (Generated_Code.Property _) = Leaf Unevaluated
   308 treeOf n (Generated_Code.Universal ty f _)  = VarNode UniversalQ uneval [n] ty (treeOf (n + 1) (f dummy)) 
   288 treeOf n (Generated_Code.Universal ty f _)  = Variable Universal Unevaluated [n] ty (treeOf (n + 1) (f dummy)) 
   309 treeOf n (Generated_Code.Existential ty f _) = VarNode ExistentialQ uneval [n] ty (treeOf (n + 1) (f dummy))
   289 treeOf n (Generated_Code.Existential ty f _) = Variable Existential Unevaluated [n] ty (treeOf (n + 1) (f dummy))
   310 
   290 
   311 reifysOf :: Generated_Code.Property -> [Generated_Code.Narrowing_term -> Generated_Code.Term]
   291 reifysOf :: Generated_Code.Property -> [Generated_Code.Narrowing_term -> Generated_Code.Term]
   312 reifysOf (Generated_Code.Property _) = []
   292 reifysOf (Generated_Code.Property _) = []
   313 reifysOf (Generated_Code.Universal _ f r)  = (r : (reifysOf (f dummy)))
   293 reifysOf (Generated_Code.Universal _ f r)  = (r : (reifysOf (f dummy)))
   314 reifysOf (Generated_Code.Existential _ f r) = (r : (reifysOf (f dummy)))
   294 reifysOf (Generated_Code.Existential _ f r) = (r : (reifysOf (f dummy)))