equal
deleted
inserted
replaced
1 {- |
1 {- |
2 A narrowing-based Evaluator for Formulas in Prefix Normal Form based on the compilation technique of LazySmallCheck |
2 A narrowing-based Evaluator for Formulas in Prefix Normal Form based on the compilation technique of LazySmallCheck |
3 -} |
3 -} |
4 module Narrowing_Engine where |
4 module Narrowing_Engine where |
5 |
5 |
6 import Monad |
6 import Control.Monad |
7 import Control.Exception |
7 import Control.Exception |
|
8 import System.IO |
8 import System.Exit |
9 import System.Exit |
9 import Maybe |
10 import Data.Maybe |
10 import List (partition, findIndex) |
11 import Data.List (partition, findIndex) |
11 import qualified Generated_Code |
12 import qualified Generated_Code |
12 |
13 |
13 |
14 |
14 type Pos = [Int] |
15 type Pos = [Int] |
15 |
16 |
33 termListOf pos es = termListOf' 0 es |
34 termListOf pos es = termListOf' 0 es |
34 where |
35 where |
35 termListOf' i [] = [] |
36 termListOf' i [] = [] |
36 termListOf' i (e : es) = |
37 termListOf' i (e : es) = |
37 let |
38 let |
38 (ts, rs) = List.partition (\e -> head (posOf e) == i) (e : es) |
39 (ts, rs) = Data.List.partition (\e -> head (posOf e) == i) (e : es) |
39 t = termOf (pos ++ [i]) (map tailPosEdge ts) |
40 t = termOf (pos ++ [i]) (map tailPosEdge ts) |
40 in |
41 in |
41 (t : termListOf' (i + 1) rs) |
42 (t : termListOf' (i + 1) rs) |
42 {- |
43 {- |
43 conv :: [[Term] -> a] -> Term -> a |
44 conv :: [[Term] -> a] -> Term -> a |