src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs
changeset 46758 4106258260b3
parent 46408 2520cd337056
child 47090 6b53d954255b
equal deleted inserted replaced
46757:ad878aff9c15 46758:4106258260b3
    25 tailPosEdge :: Edge -> Edge
    25 tailPosEdge :: Edge -> Edge
    26 tailPosEdge (VN pos ty) = VN (tail pos) ty
    26 tailPosEdge (VN pos ty) = VN (tail pos) ty
    27 tailPosEdge (CtrB pos ts) = CtrB (tail pos) ts
    27 tailPosEdge (CtrB pos ts) = CtrB (tail pos) ts
    28 
    28 
    29 termOf :: Pos -> Path -> Generated_Code.Narrowing_term
    29 termOf :: Pos -> Path -> Generated_Code.Narrowing_term
    30 termOf pos (CtrB [] i : es) = Generated_Code.Ctr i (termListOf pos es)
    30 termOf pos (CtrB [] i : es) = Generated_Code.Narrowing_constructor i (termListOf pos es)
    31 termOf pos [VN [] ty] = Generated_Code.Var pos ty
    31 termOf pos [VN [] ty] = Generated_Code.Narrowing_variable pos ty
    32 
    32 
    33 termListOf :: Pos -> Path -> [Generated_Code.Narrowing_term]
    33 termListOf :: Pos -> Path -> [Generated_Code.Narrowing_term]
    34 termListOf pos es = termListOf' 0 es
    34 termListOf pos es = termListOf' 0 es
    35   where
    35   where
    36     termListOf' i [] = []
    36     termListOf' i [] = []
   147 
   147 
   148 refineTree :: [Edge] -> Pos -> QuantTree -> QuantTree
   148 refineTree :: [Edge] -> Pos -> QuantTree -> QuantTree
   149 refineTree es p t = updateTree refine (pathPrefix p es) t
   149 refineTree es p t = updateTree refine (pathPrefix p es) t
   150   where
   150   where
   151     pathPrefix p es = takeWhile (\e -> posOf e /= p) es  
   151     pathPrefix p es = takeWhile (\e -> posOf e /= p) es  
   152     refine (VarNode q r p (Generated_Code.SumOfProd ps) t) =
   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 ]
   153       CtrBranch q r p [ foldr (\(i,ty) t -> VarNode q r (p++[i]) ty t) t (zip [0..] ts) | ts <- ps ]
   154 
   154 
   155 -- refute
   155 -- refute
   156 
   156 
   157 refute :: ([Generated_Code.Narrowing_term] -> Bool) -> Bool -> Int -> QuantTree -> IO QuantTree
   157 refute :: ([Generated_Code.Narrowing_term] -> Bool) -> Bool -> Int -> QuantTree -> IO QuantTree
   228     error ""
   228     error ""
   229 -}
   229 -}
   230 termlist_of :: Pos -> ([Generated_Code.Narrowing_term], QuantTree) -> ([Generated_Code.Narrowing_term], QuantTree)
   230 termlist_of :: Pos -> ([Generated_Code.Narrowing_term], QuantTree) -> ([Generated_Code.Narrowing_term], QuantTree)
   231 termlist_of p' (terms, Node b) = (terms, Node b) 
   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
   232 termlist_of p' (terms, VarNode q r p ty t) = if p' == take (length p') p then
   233     termlist_of p' (terms ++ [Generated_Code.Var p ty], t)
   233     termlist_of p' (terms ++ [Generated_Code.Narrowing_variable p ty], t)
   234   else
   234   else
   235     (terms, VarNode q r p ty t)
   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
   236 termlist_of p' (terms, CtrBranch q r p ts) = if p' == take (length p') p then
   237     let
   237     let
   238       Just i = findIndex (\t -> evalOf t == Eval False) ts
   238       Just i = findIndex (\t -> evalOf t == Eval False) ts
   239       (subterms, t') = fixp (\j -> termlist_of (p ++ [j])) 0 ([], ts !! i)
   239       (subterms, t') = fixp (\j -> termlist_of (p ++ [j])) 0 ([], ts !! i)
   240     in
   240     in
   241       (terms ++ [Generated_Code.Ctr i subterms], t')
   241       (terms ++ [Generated_Code.Narrowing_constructor i subterms], t')
   242   else
   242   else
   243     (terms, CtrBranch q r p ts)
   243     (terms, CtrBranch q r p ts)
   244   where
   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)
   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 
   246 
   247 
   247 
   248 alltermlist_of :: Pos -> ([Generated_Code.Narrowing_term], QuantTree) -> [([Generated_Code.Narrowing_term], QuantTree)]
   248 alltermlist_of :: Pos -> ([Generated_Code.Narrowing_term], QuantTree) -> [([Generated_Code.Narrowing_term], QuantTree)]
   249 alltermlist_of p' (terms, Node b) = [(terms, Node b)] 
   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
   250 alltermlist_of p' (terms, VarNode q r p ty t) = if p' == take (length p') p then
   251     alltermlist_of p' (terms ++ [Generated_Code.Var p ty], t)
   251     alltermlist_of p' (terms ++ [Generated_Code.Narrowing_variable p ty], t)
   252   else
   252   else
   253     [(terms, VarNode q r p ty t)]
   253     [(terms, VarNode q r p ty t)]
   254 alltermlist_of p' (terms, CtrBranch q r p ts) =
   254 alltermlist_of p' (terms, CtrBranch q r p ts) =
   255   if p' == take (length p') p then
   255   if p' == take (length p') p then
   256     let
   256     let
   257       its = filter (\(i, t) -> evalOf t == Eval False) (zip [0..] ts)
   257       its = filter (\(i, t) -> evalOf t == Eval False) (zip [0..] ts)
   258     in
   258     in
   259       concatMap
   259       concatMap
   260         (\(i, t) -> map (\(subterms, t') -> (terms ++ [Generated_Code.Ctr i subterms], t'))
   260         (\(i, t) -> map (\(subterms, t') -> (terms ++ [Generated_Code.Narrowing_constructor i subterms], t'))
   261            (fixp (\j -> alltermlist_of (p ++ [j])) 0 ([], t))) its
   261            (fixp (\j -> alltermlist_of (p ++ [j])) 0 ([], t))) its
   262   else
   262   else
   263     [(terms, CtrBranch q r p ts)]
   263     [(terms, CtrBranch q r p ts)]
   264   where
   264   where
   265     fixp f j s = case (f j s) of
   265     fixp f j s = case (f j s) of