attGr.ag

imports
{


import Data.List
import Text.Parsec.Prim
import N3grammar
import System.Directory
import Data.Text (pack, count)


}

--N3 Grammar
data S
    | Mainformula f :: Formula
 
data Formula
   | Triple s, p, o :: Term
   | Implication e1, e2 :: Expression
   | Conjunction c1, c2 :: Formula

data Term
   | Universal u :: String
   | Existential ex :: String
   | URI uri :: String
   | Literal l :: String
   | Exp  e :: Expression
   | List term, list :: Term


data Expression
   | BE   b  :: Bool
   | FE   f  :: Formula

deriving S Term Expression Formula: Show
deriving S Formula Term Expression : Read
deriving S Formula Term Expression : Eq


--Core Grammar
data CFormula
     | CTriple t1, t2, t3 :: CTerm
     | CImplication e1, e2 :: CExpression
     | CConjunction f1, f2 :: CFormula
     | Quant     a :: Quant
                 f :: CFormula

data Quant 
     | Forall v :: CTerm
     | Forsome e :: CTerm



data CTerm 
     | Var t :: String
     | Con c :: String
     | CExp  e :: CExpression
     | CList t, list :: CTerm

data CExpression
   | CBE   b  :: Bool
   | CFE   f  :: CFormula


deriving CTerm  CFormula Quant Var CTerm CExpression: Show
deriving CTerm  CFormula Quant Var CTerm CExpression: Eq


-- Attributes for N3 Grammar
--Declaration
attr S
--Attributes for standard--
   syn n1 :: {[String]}
   syn n2 :: {[String]}
   syn ex :: {[String]}
   syn transformed :: CFormula
   syn formula ::  String
--attributes for EYE--
   syn eye :: CFormula
   syn eyeVar :: {[String]}
   syn eyeEx :: {[String]}
--like team submission but universal different
   syn diff :: CFormula  
--count how deeply nested universals occur
   syn count :: Int
--know which variables are the deepest
   syn deep :: {[String]}
--atrribute to find builtins
   syn be :: Int
-- count number of nested curly brackets 
   syn cb :: Int 
-- is the formula a proof?
   syn proof :: Int
-- builtin with formula expression
   syn bwfe :: Int
   syn biscope :: {[String]}
   

attr Formula
--Attributes for standard--
   syn n2 :: {[String]}
   syn n1 :: {[String]}
   inh scope :: {[String]}
   inh uni   :: {[String]}
   syn ex :: {[String]}
   syn transformed :: CFormula
   syn formula :: String
--attributes for EYE--
   syn eye :: CFormula
   syn eyeVar :: {[String]}
   syn eyeEx :: {[String]}
   inh insideQuotation :: Bool
--like team submission but universal different
   syn diff :: CFormula 
--count how deeply nested universals occur
   syn count :: Int
   inh c :: Int
--know which variables are the deepest
   syn deep :: {[String]}
--atrribute to find builtins
   syn be :: Int
-- count number of nested curly brackets 
   syn cb :: Int 
-- is the formula a proof?
   syn proof :: Int
-- builtin with formula expression
   syn bwfe :: Int
   syn biscope :: {[String]}


attr Term
--Attributes for standard--
   syn n2 :: {[String]}
   syn n1 :: {[String]}
   inh scope :: {[String]}
   syn ex :: {[String]}
   syn transformed :: CTerm
   syn formula :: String
--attributes for EYE--
   syn eye :: CTerm
   syn eyeVar :: {[String]}
   syn eyeEx :: {[String]}
   inh insideQuotation :: Bool
   inh varInImpException :: Bool
--like team submission but universal different
   syn diff :: CTerm
--count how deeply nested universals occur
   syn count :: Int
   inh c :: Int
--know which variables are the deepest
   syn deep :: {[String]}
--atrribute to find builtins
   syn be :: Int
-- count number of nested curly brackets 
   syn cb :: Int 
-- is the formula a proof?
   syn proof :: Int
-- builtin with formula expression
   syn bwfe :: Int
   syn biscope :: {[String]}


attr Expression
--Attributes for standard--
   syn n1 :: {[String]}
   inh scope :: {[String]}
   syn transformed :: CExpression
   syn formula :: String
--attributes for EYE--
   syn eye :: CExpression
   syn eyeVar :: {[String]}
   syn eyeEx :: {[String]}
   inh insideQuotation :: Bool
--like team submission but universal different
   syn diff :: CExpression  
--count how deeply nested universals occur
   syn count :: Int
   inh c :: Int
--know which variables are the deepest
   syn deep :: {[String]}
--atrribute to find builtins
   syn be :: Int
-- count number of nested curly brackets
   syn cb :: Int 
-- is the formula a proof?
   syn proof :: Int
-- builtin with formula expression
   syn bwfe :: Int
   syn biscope :: {[String]}


--Definition   
--TODO: default value should be empty list

sem S
   | Mainformula f.scope = @f.n1  `union` @f.n2
                 f.uni   = @f.n1  `union` @f.n2
                 lhs.ex = @f.ex
                 lhs.transformed = qua (sort (@f.n1  `union` @f.n2)) @f.ex @f.transformed
                 lhs.formula = quaf (sort  (@f.n1  `union` @f.n2)) @f.ex   @f.formula 
                 lhs.eye = qua (sort @f.eyeVar ) @f.eyeEx @f.eye
                 lhs.eyeEx = @f.eyeEx
                 lhs.eyeVar = @f.eyeVar
                 f.insideQuotation = False
                 lhs.diff = qua (sort  @f.eyeVar) @f.ex @f.diff
                 f.c = 1
                 lhs.count = findDepth @f.n1 1 @f.count
                 lhs.deep = deepest @f.n1 @f.deep
                 lhs.be = @f.be
                 lhs.cb = @f.cb
                 lhs.proof = @f.proof
                 lhs.bwfe = @f.bwfe
                 lhs.biscope = []
  
sem Formula
   | Triple lhs.n2 = (@s.n2 `union` @p.n2) `union` @o.n2
            lhs.n1 = (@s.n1 `union` @p.n1) `union` @o.n1 
            lhs.ex = (@s.ex `union` @p.ex) `union` @o.ex 
            lhs.transformed = CTriple @s.transformed @p.transformed @o.transformed 
            lhs.formula =   @s.formula ++ " " ++ @p.formula ++ " " ++ @o.formula 
            lhs.eye = CTriple @s.eye @p.eye @o.eye  
            lhs.eyeVar = (@s.eyeVar `union` @p.eyeVar) `union` @o.eyeVar 
            lhs.eyeEx = (@s.eyeEx `union` @p.eyeEx) `union` @o.eyeEx 
            s.insideQuotation = @lhs.insideQuotation
            p.insideQuotation = @lhs.insideQuotation
            o.insideQuotation = @lhs.insideQuotation
            s.varInImpException = impExc @p.eye @lhs.insideQuotation
            p.varInImpException = False
            o.varInImpException = impExc @p.eye @lhs.insideQuotation
            lhs.diff = CTriple @s.diff @p.diff @o.diff 
            s.c = @lhs.c
            p.c = @lhs.c
            o.c = @lhs.c
            lhs.count = max @s.count (max @p.count @o.count)
            lhs.deep = choose @o.deep  (choose @s.deep @p.deep @s.count @p.count) @o.count (max @s.count @p.count)
            lhs.be = maximum [@s.be, @p.be, @o.be]
            lhs.cb = maximum [@s.cb, @p.cb, @o.cb]
            lhs.proof = @o.proof
            lhs.bwfe = maximum [ @p.bwfe, @s.bwfe, @o.bwfe]
            lhs.biscope = universalsInBuiltins @p.be (@s.eyeVar  `union` @o.eyeVar) ((@s.biscope `union` @p.biscope) `union` @o.biscope)
 
               
   | Implication lhs.n2 = []
                 lhs.n1 = @e1.n1 `union` @e2.n1
                 lhs.ex = []
                 lhs.transformed = CImplication @e1.transformed @e2.transformed
                 lhs.formula =  @e1.formula ++ " -> " ++ @e2.formula
                 lhs.eye = CImplication @e1.eye @e2.eye
                 lhs.eyeVar = @e1.eyeVar `union` @e2.eyeVar
                 lhs.eyeEx = keepEx @lhs.insideQuotation (@e1.eyeEx `union` @e2.eyeEx) 
                 e1.insideQuotation = @lhs.insideQuotation
                 e2.insideQuotation = @lhs.insideQuotation
                 lhs.diff = CImplication @e1.diff @e2.diff
                 e1.c = @lhs.c
                 e2.c = @lhs.c
                 lhs.count = max @e1.count @e2.count
                 lhs.deep = choose @e1.deep @e2.deep @e1.count @e2.count
                 lhs.be =  maximum [@e1.be, @e2.be]
                 lhs.cb = maximum [@e1.cb, @e2.cb]
                 lhs.proof = 0
                 lhs.bwfe = maximum [@e1.bwfe, @e2.bwfe ]
                 lhs.biscope = @e2.biscope `union` @e1.biscope

   | Conjunction lhs.n2 = @c2.n2 `union` @c1.n2
                 lhs.n1 = @c2.n1 `union` @c1.n1
                 lhs.ex = @c2.ex `union` @c1.ex
                 c1.scope = @lhs.scope
                 c2.scope = @lhs.scope
                 lhs.transformed = CConjunction @c1.transformed @c2.transformed
                 lhs.formula =   @c1.formula ++ " ^ " ++ @c2.formula
                 lhs.eye = CConjunction @c1.eye @c2.eye
                 lhs.eyeVar = @c2.eyeVar `union` @c1.eyeVar
                 lhs.eyeEx = @c2.eyeEx `union` @c1.eyeEx
                 c1.insideQuotation = @lhs.insideQuotation
                 c2.insideQuotation = @lhs.insideQuotation
                 lhs.diff = CConjunction @c1.diff @c2.diff
                 c1.c = @lhs.c
                 c2.c = @lhs.c
                 lhs.count = max @c1.count @c2.count
                 lhs.deep = choose @c1.deep @c2.deep @c1.count @c2.count
                 lhs.be = maximum [@c1.be, @c2.be]
                 lhs.cb = maximum [@c1.cb, @c2.cb]
                 lhs.proof = maximum [@c1.proof, @c2.proof]
                 lhs.bwfe = maximum [@c1.bwfe, @c2.bwfe ]
                 lhs.biscope = @c2.biscope `union` @c1.biscope
                 
sem Term
   | Universal lhs.n2 = ["U"++ @u]
               lhs.n1 = []
               lhs.ex = []
               lhs.transformed = Var  ("U"++ @u) 
               lhs.formula = "U"++ @u 
               lhs.eyeVar = ["U" ++ @u]
               lhs.eye = Var  ("U"++ @u)
               lhs.eyeEx = [] 
               lhs.diff = Var  ("U"++ @u) 
               lhs.count = 0
               lhs.deep = []
               lhs.be = 0
               lhs.cb = 0
               lhs.proof = 0 
               lhs.bwfe = 0
               lhs.biscope = []
               

   | Existential lhs.n2 = []
                lhs.n1 = []
                lhs.ex = ["E"++ @ex]
                lhs.transformed = Var ("E"++ @ex)
                lhs.formula = "E"++ @ex
                lhs.eyeVar = []
                lhs.eye = Var ("E"++ @ex)
                lhs.eyeEx = ["E"++ @ex]
                lhs.diff = Var ("E"++ @ex)
                lhs.count = 0
                lhs.deep = []
                lhs.be = 0
                lhs.cb = 0
                lhs.proof = 0
                lhs.bwfe = 0
                lhs.biscope = []

   | URI lhs.n2 = []
              lhs.n1 = []
              lhs.ex = []
              lhs.transformed = Con ("uri_"++ @uri)
              lhs.formula = "uri_"++ @uri
              lhs.eyeVar = []
              lhs.eye = Con ("uri_" ++ @uri)
              lhs.eyeEx = []
              lhs.diff = Con ("uri_" ++ @uri)
              lhs.count = 0
              lhs.deep = []
              lhs.be =  isBuiltIn @uri
              lhs.cb = 0
              lhs.proof = isProof @uri
              lhs.bwfe = 0
              lhs.biscope = []

   | Literal lhs.n2 = []
              lhs.n1 = []
              lhs.ex = []
              lhs.transformed = Con ("l_"++ @l)
              lhs.formula = "l_"++ @l
              lhs.eyeVar = []
              lhs.eye = Con ("l_"++ @l)
              lhs.eyeEx = []
              lhs.diff = Con ("l_"++ @l)
              lhs.count = 0
              lhs.deep = []
              lhs.be = 0
              lhs.cb = 0
              lhs.proof = 0
              lhs.bwfe = 0 
              lhs.biscope = []
    
   | Exp  lhs.n2 = []
          lhs.n1 = @e.n1
          lhs.ex = []
          lhs.transformed = CExp @e.transformed 
          lhs.formula =  @e.formula
          lhs.eye = CExp @e.eye
          lhs.eyeEx= exception @lhs.varInImpException @lhs.insideQuotation @e.eyeEx
          e.insideQuotation = True
          lhs.diff = CExp @e.diff
          lhs.count= @e.count
          lhs.deep = @e.deep
          lhs.be = @e.be
          lhs.cb = @e.cb
          lhs.proof = 0
          lhs.bwfe = @e.bwfe
          lhs.biscope = @e.biscope
           

   |List  lhs.n2 = @term.n2 `union` @list.n2
          lhs.n1 = @term.n1 `union` @list.n1
          lhs.ex = @term.ex `union` @list.ex
          lhs.transformed = CList @term.transformed @list.transformed
          lhs.formula =  "(" ++ @term.formula ++ "," ++ @list.formula ++ ")" 
          lhs.eyeVar = @term.eyeVar ++ @list.eyeVar
          lhs.eye = CList @term.transformed @list.transformed
          lhs.eyeEx = @term.eyeEx ++ @list.eyeEx
          lhs.diff = CList @term.diff @list.diff      
          term.c = @lhs.c
          list.c = @lhs.c
          lhs.count = max @term.count @list.count
          lhs.deep = @term.deep `union` @list.deep 
          lhs.be = 0
          lhs.cb = maximum [@term.cb, @list.cb]     
          lhs.proof = 0   
          lhs.bwfe =  maximum [@term.bwfe, @list.bwfe] 
          lhs.biscope = @term.biscope `union` @list.biscope  
          

sem Expression
   | BE lhs.n1 = []
          lhs.transformed = CBE @b
          lhs.formula = if @b == True then "<>" else "false"
          lhs.eyeVar = []
          lhs.eye = CBE @b
          lhs.eyeEx = []
          lhs.diff = CBE @b
          lhs.count = 0
          lhs.deep = []
          lhs.be = 0
          lhs.cb = 0
          lhs.proof = 0
          lhs.bwfe = 0
          lhs.biscope = []

   | FE   lhs.n1 = @f.n2
          f.scope = @lhs.scope `union` @f.n1 
          lhs.transformed = CFE (qua (@f.n1 \\ @lhs.scope) @f.ex @f.transformed)  
          lhs.formula = "<"++ (quaf (@f.n1 \\ @lhs.scope) @f.ex @f.formula) ++">"
          f.uni = @f.n1 \\ @lhs.scope
          lhs.eye = CFE (qua [] (imp @lhs.insideQuotation @f.eyeEx) @f.eye )
          lhs.eyeEx = @f.eyeEx
          lhs.diff = CFE (qua [] @f.ex @f.diff)
          f.insideQuotation = True
          f.c = @lhs.c+1
          lhs.count = findDepth (@f.n1 \\ @lhs.scope) (@lhs.c +1) @f.count -- max (@lhs.c+1) @f.count
          lhs.deep = deepest (@f.n1 \\ @lhs.scope) @f.deep
          lhs.be = @f.be
          lhs.cb = @f.cb + 1
          lhs.proof = 0
          lhs.bwfe =  b @f.bwfe (@f.biscope \\ @lhs.scope)
          lhs.biscope = []



{




             
parseToCoreTree :: String -> IO ()
parseToCoreTree filename = do {
                       input <- readFile filename
                       ; case runParser mainparser 0 filename input of
                       {
                       Left err -> print err
                       ; Right ans -> putStrLn $   show (  transformed_Syn_S (  wrap_S  (sem_S  (read (show ans))) Inh_S  )  ) 
                       }
                       }  

              
eyeToCore :: String -> IO ()
eyeToCore fname = do {
               input <- readFile fname
              ; case runParser mainparser 0 fname input of
              { Left err -> print err
              ; Right ans -> putStrLn $ show (  eye_Syn_S (  wrap_S  (sem_S  (read (show ans))) Inh_S  )  )  
              }}

parseToCoreFormula :: String -> IO ()
parseToCoreFormula fname = do {
                input <- readFile fname
                ; case runParser mainparser 0 fname input of
                { Left err -> print err
                ; Right ans -> print (  formula_Syn_S (  wrap_S  (sem_S  (read (show ans))) Inh_S  ) )
                }
              }


testp :: String -> IO ()
testp fname = do {
                  input <- readFile fname
                  ; case runParser mainparser 0 fname input of
                  { Left err -> print err
                  ; Right ans -> putStrLn $   show (  eyeVar_Syn_S (  wrap_S  (sem_S  (read (show ans))) Inh_S  )  ) 
                  } 
              }


-- function for quantifiers: takes Universals and existentials as lists and the formula without quantifier and produces a quantified formula
qua :: [String] -> [String] -> CFormula -> CFormula
--qua u e f = foldr fa f u
--fa :: String ->  CFormula
--fa  u f = Quant (Forall (Var u)) f

qua [] [] f  = f
qua [] (a:as) f = Quant (Forsome (Var a)) (qua [] as f)
qua (a:as) g f = Quant (Forall (Var a)) (qua as g f)





--the qua function to generate a formula (just to see the translation as text)
quaf :: [String] -> [String] -> String -> String
quaf [] [] s = s
quaf [] (a:as) s = "ForSome " ++ a ++ ". " ++ (quaf [] as s)
quaf (a:as) g s = "ForAll " ++ a ++ ". " ++ (quaf as g s)

findDepth :: [String] -> Int -> Int -> Int
findDepth [] n m = m
findDepth set n m = max n m

deepest :: [String] -> [String]  ->[String]
deepest new [] = new
deepest new old = old

choose :: [String] -> [String] -> Int -> Int ->[String]
choose first second n m = if (n>m) then first
                          else second



imp :: Bool -> [String] -> [String]
imp False l  = l
imp f l = []

--not really pretty, but at least easy
printTree :: String -> Int -> String 
printTree ('(':b) n = "\n"++ ( concat (replicate (n+1) "|  ") ) ++ ( printTree b (n+1) )
printTree (')':b) n = ( printTree b (n-1) )
printTree (s:b)   n  =  (s    : ( printTree b n))
printTree s       n  =  s 


makeTree :: String -> String -> IO()
makeTree fname "uni" = do {
                input <- readFile fname
                ; case runParser mainparser 0 fname input of
                { Left err -> print err
                ; Right ans -> putStrLn $ printTree  (show (  eye_Syn_S (  wrap_S  (sem_S  (read (show ans))) Inh_S  )  )) 0
                }}
makeTree fname "cwm" = do {
                input <- readFile fname
                ; case runParser mainparser 0 fname input of
                { Left err -> print err
                ; Right ans -> putStrLn $ printTree  (show  (  transformed_Syn_S (  wrap_S  (sem_S  (read (show ans))) Inh_S  )  )) 0
                }
                }
makeTree fname "eye" = do {
                input <- readFile fname
                ; case runParser mainparser 0 fname input of
                { Left err -> print err
                ; Right ans -> putStrLn $ printTree  (show  (  diff_Syn_S (  wrap_S  (sem_S  (read (show ans))) Inh_S  )  )) 0
                }
                }


--simple function to compare tree strings, later that comparison should be on tree level
compareTree :: String -> String -> String -> Int -> String
compareTree (x:b) (y:c) s n 
           | (x==y) = compareTree b c (s++[x]) (n+1)
           | otherwise = "Difference at pos. "++ show(n)  ++ "\n" ++ s ++
                               "\n CWM:  " ++ (take 100 (x:b)) ++ "... \n and \n Other:  " ++ (take 100 (y:c))++ "..."
compareTree [][] s n = "no differences found"

compareB :: String -> IO()
compareB fname = do {
               input <- readFile fname
               ; case runParser mainparser 0 fname input of
                        { 
                          Left err -> print err
                          ; Right ans -> putStrLn $  compareTree (show (  transformed_Syn_S (  wrap_S  (sem_S  (read (show ans))) Inh_S  )  )) 
                                                              (show (  eye_Syn_S         (  wrap_S  (sem_S  (read (show ans))) Inh_S  )  ))
                                                              []
                                                              0
                        }
               }


topUni :: String -> IO()
topUni fname = do {
               input <- readFile fname
               ; case runParser mainparser 0 fname input of
                        { 
                          Left err -> print err
                          ; Right ans -> putStrLn $ show (  n1_Syn_S (  wrap_S  (sem_S  (read (show ans))) Inh_S  )  ) 
  
                        }
               }






compareU :: String -> IO()
compareU fname = do {
               input <- readFile fname
               ; case runParser mainparser 0 fname input of
                        { 
                          Left err -> print err
                          ; Right ans -> putStrLn $  compareTree (show (  transformed_Syn_S (  wrap_S  (sem_S  (read (show ans))) Inh_S  )  )) 
                                                              (show (  diff_Syn_S         (  wrap_S  (sem_S  (read (show ans))) Inh_S  )  ))
                                                              []
                                                              0
                        }
               }
depth :: String -> IO()
depth fname =  do {
               input <- readFile fname
               ; case runParser mainparser 0 fname input of
                        { 
                          Left err -> print err
                          ; Right ans -> putStrLn $ show (  count_Syn_S (  wrap_S  (sem_S  (read (show ans))) Inh_S  )  )
                        }
               }

deepvars :: String -> IO()
deepvars fname =  do {
               input <- readFile fname
               ; case runParser mainparser 0 fname input of
                        { 
                          Left err -> print err
                          ; Right ans -> putStrLn $ show (  deep_Syn_S (  wrap_S  (sem_S  (read (show ans))) Inh_S  )  )
                        }
               }

--not used any more
--hasBuiltins :: String -> Int
hasBuiltins foname [] result = do { return (reverse result) } 
hasBuiltins foname fs result =
                    do {
                        let fname = (head fs)
                        ; input <- readFile $ foname ++ "/"++ fname
                        ; case   ( (count (pack ("e:")) (pack input) ) > 1) 
                         || ( (count (pack ("prolog:")) (pack input) ) > 1) 
                         || ( (count (pack ("fn:")) (pack input) ) > 1)  
                         || ( (count (pack ("crypto:")) (pack input) ) > 1) 
                         || ( (count (pack ("list:")) (pack input) ) > 1) 
                         || ( (count (pack ("log:")) (pack input) ) > 1)  
                         || ( (count (pack ("math:")) (pack input) ) > 1) 
                         || (isInfixOf " rdf:first" input) 
                         || (isInfixOf " rdf:rest" input) 
                         || ( (count (pack ("string:")) (pack input) ) > 1) 
                         || ( (count (pack ("time:")) (pack input) ) > 1) 
                         || ( (count (pack ("func:")) (pack input) ) > 1) 
                         || ( (count (pack ("pred:")) (pack input) ) > 1) 
                        of
                        {
                         True -> (hasBuiltins foname (tail fs) (1:result))
                         ; False -> (hasBuiltins foname (tail fs) (0:result))
                        }
                  }



compareAll :: String -> String ->  IO ()
compareAll foname target = do {
               
                files <- getDirectoryContents foname
                ; let fs = (filter (isSuffixOf ".n3") files)
               -- ; let fname = head fs
               -- ;  input <- readFile (foname ++"/"++fname)
               -- ; case runParser mainparser 0 fname input of
               -- { Left err ->   writeFile "err.txt" (show err)
               -- ; Right ans ->  writeFile "out.txt" $ niceTable (read (show ans)) fname
                                
               -- }
               --this here is to only consider the files containing the symbol ?, only those can contain universals
               ;  newfs <- findFilesWithUniversals foname fs []
               --; builtins <- hasBuiltins foname newfs []
               ;   (values, count) <- (readAll foname newfs [] [0, 0, 0, 0, 0,0,0,0, 0, 0])
               ; let table = makeTable newfs values count
               ; writeFile target $ ((replicate 40 ' ') ++ "cwm/es2  " ++ "cwm/eye  " ++ "eye/es2  " ++ "builtin " ++ "proof  "++ "nested "++ "depth  " ++ "reason \n" )++ table
               }


--readAll :: String -> [String] ->  -> IO() 
readAll foname [] list [a, b, c, d, e, r1, r2, r3, ne, pc ] = do { 
                            return $ ((reverse list), [a,b,c,d, e, r1 , r2, r3, ne, pc])
                            }
readAll foname fs list [a, b, c, d, e, r1, r2, r3, ne, pc]  = do { 
                         let fname = (head fs)
                         ; input <- readFile $ foname ++ "/"++ fname
                         ; print (foname ++ "/"++ fname ++ " parsed \n" )  
                                    ;case runParser mainparser 0 fname input of
                                    {
                                    Left  err ->   (readAll foname (tail fs) ( [9,9,9,9,9,9,9,9, 9 ]:list ) [a, b, c, d, e, r1, r2, r3, ne, pc] )
                                    ;Right ans -> case ((  eyeVar_Syn_S (  wrap_S  (sem_S  (read (show ans))) Inh_S  )  )== []) of
                                                    {
                                                     True -> (readAll foname (tail fs) ( [9,9,9,9,9,9,9,9, 9]:list ) [a, b, c, d, e, r1, r2, r3, ne, pc] )
                                                     ; False ->
                                                         (\res -> ((\x y z zz zzzz proof zzz ff r  -> (readAll foname (tail fs) (
                                                             [x, 
                                                              y, 
                                                              z,
                                                              zz,
                                                              zzzz,
                                                              proof,
                                                              ff,
                                                              zzz ,
                                                              r
                                                             ]:list ) 
                                                             [(a+x), (b+y), (c+z), (d+1), (e+zzzz), (countR1 r1 r), (countR2 r2 r), ( countR3 r3 r), (countBI ne ff), pc + proof ]
                                                             ) )
                                                             (cwm_and_eye res )
                                                             (cwm_and_diff res)
                                                             (eye_and_diff res)
                                                             (boolToInt ( (eyeVar_Syn_S (  wrap_S  (sem_S  res) Inh_S   ))==[]))
                                                             (be_Syn_S (  wrap_S  (sem_S  (read (show ans))) Inh_S  ))
                                                             (proof_Syn_S (  wrap_S  (sem_S  (read (show ans))) Inh_S  ))
                                                             (  count_Syn_S (  wrap_S  (sem_S  (read (show ans))) Inh_S  )  )
                                                             (  cb_Syn_S (  wrap_S  (sem_S  (read (show ans))) Inh_S  )  )
                                                             )
                                                           --r
                                                           (reason (cwm_and_diff res) (  proof_Syn_S (  wrap_S  (sem_S  (read (show ans))) Inh_S  )  )  (  count_Syn_S (  wrap_S  (sem_S  (read (show ans))) Inh_S  )  ) (  bwfe_Syn_S (  wrap_S  (sem_S  (read (show ans))) Inh_S  )  ) ) 
                                                           )
                                                             (read (show ans))
                                      }
                                   }
                               
                            
                            }
                         
findFilesWithUniversals foname [] newfs = do { return (reverse newfs) }                        
findFilesWithUniversals foname fs newfs = do {
                                             let fname = (head fs)
                                             ; input <- readFile $ foname ++ "/"++ fname
                                             ; case (isInfixOf "?" input) of
                                                   {
                                                   True  -> ( findFilesWithUniversals foname (tail fs) (fname:newfs))
                                                   ;False -> ( findFilesWithUniversals foname (tail fs) newfs)
                                                   }
                                             }


                       
                                  
--todo: every parsing only once               
cwm_and_eye :: S -> Int
cwm_and_eye f = boolToInt (   ( eye_Syn_S  x ) ==  (   transformed_Syn_S x  )   ) 
           where x = (  wrap_S  (sem_S  f) Inh_S   )     
               
cwm_and_diff :: S -> Int
cwm_and_diff f = boolToInt ((  diff_Syn_S  x ) ==  (   transformed_Syn_S x  )   ) 
           where x = (  wrap_S  (sem_S  f) Inh_S   ) 

eye_and_diff :: S -> Int
eye_and_diff f = boolToInt ((   diff_Syn_S  x ) ==  (  eye_Syn_S x   ) )
           where x = (  wrap_S  (sem_S  f) Inh_S   ) 
           
           
niceTable :: S -> String -> String
niceTable f fname = (replicate 30 ' ') ++ "cwm/eye  " ++ "cwm/uni  " ++ "uni/eye \n" 
                     ++ fname ++ (replicate (30 - length(fname)) ' ')  ++ (show  ( cwm_and_eye f ))++ (replicate 8 ' ') ++ (show  ( cwm_and_diff f )) ++ (replicate 8 ' ') ++ (show  ( eye_and_diff f ))       


makeTable :: [String] -> [[Int]] -> [Int] -> String
makeTable [] values stat = lastLine stat
makeTable names ([a , b, c , 1, e1, e, f, r, p]:v) [s1, s2, s3, s4, s5, s6 , s7] = (makeTable (tail names) v [(s1-a), (s2-b), (s3-c), (s4-1),(s5-e1)])
makeTable names ([a , b, c , d, e1, e, f, r, p]:v) stat = (head names) ++ (replicate (40 - length(head names)) ' ') ++ (concat $ fmap makeEntry [a, b, c, e1,  e, f , r, p]) ++ "\n"
                         ++ (makeTable (tail names) v stat)


lastLine :: [Int]-> String
lastLine [a,b,c, d, e, r1, r2, r3, bi, pc] = "--------------------------------------------------------------------------------------------------------------" ++ "\n"
                      ++ "Absolute Number (from " 
                      ++ (show d) ++ "): " 
                      ++ (replicate(15 - (length(show d))) ' ')
                      ++ (show a) ++ (replicate (9 - (length(show a))) ' ')
                      ++ (show b) ++ (replicate (9 - (length(show b))) ' ')
                      ++ (show c) ++ (replicate (9 - (length(show c))) ' ')
                      ++ (show e) ++ (replicate (9 - (length(show e))) ' ')
                      ++ (show pc) ++ (replicate (9 - (length(show pc))) ' ')
                      ++ (show bi) ++ (replicate (9 - (length(show bi))) ' ')
                      ++ "\n"
                      ++ "Percentage: "
                      ++ (show ((fromIntegral a)/(fromIntegral d)))
                      ++" "
                      ++ (show $ (fromIntegral b)/(fromIntegral d))
                      ++ " "
                      ++ (show $ (fromIntegral c)/(fromIntegral d))
                      ++ " "
                      ++ (show $ (fromIntegral e)/(fromIntegral d))
                      ++ " "
                      ++ (show $ (fromIntegral pc)/(fromIntegral d))
                      ++ " "
                      ++ (show $ (fromIntegral bi)/(fromIntegral d))
                      ++ "\n" ++ "\n"
                      ++ "Distribution of Errors in EYE vs. CWM" ++ "\n"
                      ++ "Nesting:  " ++ (show r1) ++ " (absolut) "
                      ++ (show $ (fromIntegral r1)/(fromIntegral d)) ++ " (from all files) " ++ (show $ (fromIntegral r1)/(fromIntegral (d - b) )) ++ " (from differences) " ++ "\n"
                      ++ "Proof:  " ++ (show r2) ++ " (absolut) "
                      ++ (show $ (fromIntegral r2)/(fromIntegral d)) ++ " (from all files) " ++ (show $ (fromIntegral r2)/(fromIntegral (d - b) )) ++ " (from differences) " ++ "\n"
                      ++ "Builtins:  " ++ (show r3) ++ " (absolut) "
                      ++ (show $ (fromIntegral r3)/(fromIntegral d)) ++ " (from all files) " ++ (show $ (fromIntegral r3)/(fromIntegral (d - b) )) ++ " (from differences) " ++ "\n"
 
makeEntry :: Int -> String 
makeEntry n = (show n) ++ (replicate 8 ' ')


--data TreeElem = CFormula | CTerm

-- function to compare trees
--compareTrees :: TreeElem -> TreeElem -> [(TreeElem, TreeElem)]
--compareTrees (CFormula rest)(CFormula rest2) = compareTrees rest rest2
--compareTrees (CTriple t1 t2 t3)(CTriple t11 t22 t33) = (compareTrees t1 t11)++(compareTrees t2 t22)++(compareTrees t3 t33)
--compareTrees a b = [(a,b)]

--compareTrees (Var x) (Var y) 
--            | (x == y) = []
--            | otherwise = [(x,y)]


boolToInt :: Bool -> Int
boolToInt False = 0
boolToInt True = 1

keepEx :: Bool -> [String] -> [String]
keepEx True l = l
keepEx False l = []

impExc :: CTerm -> Bool -> Bool
impExc (Con "uri_http://www.w3.org/2000/10/swap/log#implies") b = True
impExc t b = b 

exception :: Bool -> Bool -> [String] -> [String]
exception True False s = []
exception t    f s = s


boolToString :: Bool -> String
boolToString True = "TRUE"
boolToString False = "FALSE"


isProof :: String -> Int
isProof string
        |string == "r:Proof" = 1
        | otherwise = 0

isBuiltIn :: String -> Int
isBuiltIn string 
          | elem string builtinlist = 1
          | isPrefixOf "prolog:" string = 1
          | otherwise = 0

builtinlist = [ "e:avg",
                "e:becomes",
                "e:biconditional", 
                "e:binaryEntropy", 
                "e:calculate", 
                "e:call", 
                "e:cartesianProduct", 
                "e:compoundTerm", 
                "e:cov", 
                "e:csvTuple", 
                "e:derive", 
                "e:fail",
                "e:finalize",
                "e:findall",
                "e:firstRest",
                "e:format",
                "e:graphCopy",
                "e:graphDifference",
                "e:graphIntersection",
                "e:graphList",
                "e:graphMember",
                "e:graphPair",
                "e:hmac-sha",
                "e:ignore",
                "e:label",
                "e:labelvars",
                "e:length",
                "e:match",
                "e:max",
                "e:min",
                "e:multisetEqualTo",
                "e:multisetNotEqualTo",
                "e:notLabel",
                "e:numeral",
                "e:optional",
                "e:pcc",
                "e:prefix",
                "e:propertyChainExtension",
                "e:random",
                "e:relabel",
                "e:rms",
                "e:roc",
                "e:roots",
                "e:sha",
                "e:sigmoid",
                "e:skolem",
                "e:sort",
                "e:std",
                "e:stringEscape",
                "e:stringReverse",
                "e:stringSplit",
                "e:subsequence",
                "e:trace",
                "e:transaction",
                "e:transpose",
                "e:tripleList",
                "e:tuple",
                "e:unique",
                "e:whenGround",
                "e:wwwFormEncode",
                "crypto:sha",
                "list:append",
                "list:first",
                "list:in",
                "list:last",
                "list:member",
                "list:rest",
                "log:conclusion",
                "log:conjunction",
                "log:dtlit",
                "log:equalTo",
                "log:implies",
                "log:includes",
                "log:notEqualTo",
                "log:notIncludes",
                "log:outputString",
                "log:rawType",
                "log:semantics",
                "log:uri",
                "math:absoluteValue",
                "math:atan2",
                "math:cos",
                "math:cosh",
                "math:degrees",
                "math:difference",
                "math:equalTo",
                "math:exponentiation",
                "math:greaterThan",
                "math:integerQuotient",
                "math:lessThan",
                "math:memberCount",
                "math:negation",
                "math:notEqualTo",
                "math:notGreaterThan",
                "math:notLessThan",
                "math:product",
                "math:quotient",
                "math:remainder",
                "math:rounded",
                "math:sin",
                "math:sinh",
                "math:sum",
                "math:tan",
                "math:tanh",
                "rdf:first",
                "rdf:rest",
                "string:concatenation",
                "string:contains",
                "string:containsIgnoringCase",
                "string:endsWith",
                "string:equalIgnoringCase",
                "string:greaterThan",
                "string:lessThan",
                "string:matches",
                "string:notEqualIgnoringCase",
                "string:notGreaterThan",
                "string:notLessThan",
                "string:notMatches",
                "string:replace",
                "string:scrape",
                "string:search",
                "string:startsWith",
                "time:day",
                "time:month",
                "time:year",
                "pred:literal-not-identical",
                "pred:iri-string",
                "pred:numeric-equal",
                "pred:numeric-less-than",
                "pred:numeric-greater-than",
                "pred:numeric-not-equal",
                "pred:numeric-less-than-or-equal",
                "pred:numeric-greater-than-or-equal",
                "func:not",
                "pred:boolean-equal",
                "pred:boolean-less-than",
                "pred:boolean-greater-than",
                "func:compare",
                "func:concat",
                "func:string-join",
                "func:substring",
                "func:string-length",
                "func:upper-case",
                "func:lower-case",
                "func:encode-for-uri",
                "func:substring-before",
                "func:substring-after",
                "pred:contains",
                "pred:starts-with",
                "pred:ends-with",
                "pred:matches",
                "func:year-from-dateTime",
                "func:month-from-dateTime",
                "func:day-from-dateTime",
                "func:hours-from-dateTime",
                "func:minutes-from-dateTime",
                "func:seconds-from-dateTime",
                "func:year-from-date",
                "func:month-from-date",
                "func:day-from-date",
                "func:hours-from-time",
                "func:minutes-from-time",
                "func:seconds-from-time",
                "func:years-from-duration",
                "func:months-from-duration",
                "func:days-from-duration",
                "func:hours-from-duration",
                "func:minutes-from-duration",
                "func:seconds-from-duration",
                "func:timezone-from-dateTime",
                "func:timezone-from-date",
                "func:timezone-from-time",
                "func:subtract-dateTimes",
                "func:subtract-dates",
                "func:subtract-times",
                "func:add-yearMonthDurations",
                "func:subtract-yearMonthDurations",
                "func:multiply-yearMonthDuration",
                "func:divide-yearMonthDuration",
                "func:divide-yearMonthDuration-by-yearMonthDuration",
                "func:add-dayTimeDurations",
                "func:subtract-dayTimeDurations",
                "func:multiply-dayTimeDuration",
                "func:divide-dayTimeDuration",
                "func:divide-dayTimeDuration-by-dayTimeDuration",
                "func:add-yearMonthDuration-to-dateTime",
                "func:add-yearMonthDuration-to-date",
                "func:add-dayTimeDuration-to-dateTime",
                "func:add-dayTimeDuration-to-date",
                "func:add-dayTimeDuration-to-time",
                "func:subtract-yearMonthDuration-from-dateTime",
                "func:subtract-yearMonthDuration-from-date",
                "func:subtract-dayTimeDuration-from-dateTime",
                "func:subtract-dayTimeDuration-from-date",
                "func:subtract-dayTimeDuration-from-time",
                "pred:dateTime-equal",
                "pred:dateTime-less-than",
                "pred:dateTime-greater-than",
                "pred:date-equal",
                "pred:date-less-than",
                "pred:date-greater-than",
                "pred:time-equal",
                "pred:time-less-than",
                "pred:time-greater-than",
                "pred:duration-equal",
                "pred:dayTimeDuration-less-than",
                "pred:dayTimeDuration-greater-than",
                "pred:yearMonthDuration-less-than",
                "pred:yearMonthDuration-greater-than",
                "pred:dateTime-not-equal",
                "pred:dateTime-less-than-or-equal",
                "pred:dateTime-greater-than-or-equal",
                "pred:date-not-equal",
                "pred:date-less-than-or-equal",
                "pred:date-greater-than-or-equal",
                "pred:time-not-equal",
                "pred:time-less-than-or-equal",
                "pred:time-greater-than-or-equal",
                "pred:duration-not-equal",
                "pred:dayTimeDuration-less-than-or-equal",
                "pred:dayTimeDuration-greater-than-or-equal",
                "pred:yearMonthDuration-less-than-or-equal",
                "pred:yearMonthDuration-greater-than-or-equal",
                "func:PlainLiteral-from-string-lang",
                "func:string-from-PlainLiteral",
                "func:lang-from-PlainLiteral",
                "func:PlainLiteral-compare",
                "func:PlainLiteral-length",
                "pred:matches-language-range",
                "pred:is-list",
                "pred:list-contains",
                "func:make-list",
                "func:count",
                "func:get",
                "func:sublist",
                "func:append",
                "func:concatenate",
                "func:insert-before",
                "func:remove",
                "func:reverse",
                "func:index-of",
                "func:union",
                "func:distinct-values",
                "func:intersect",
                "func:except"
                ]

reason :: Int -> Int -> Int -> Int -> Int
-- "no problem" = 0,  "nesting" = 1, "proof" = 2, "builtin" = 3
reason 1 n1 n2 n3 = 0
reason 0 n1 n2 n3
       | (n3 > 0)  = 3
       | (n1 == 1) && (n2 > 2) = 1
       | (n1 == 1) = 2
       | otherwise = 1
 


b :: Int -> [String] -> Int
b 0 [] = 0
b n  set = 1 


-- universalsInBuiltins @p.be @lhs.n2 ((@s.biscope `union` @p.biscope) `union` @o.biscope)
universalsInBuiltins :: Int -> [String] -> [String] -> [String]
universalsInBuiltins 0 s1 s2 = s2
universalsInBuiltins 1 s1 s2 = (s1 `union` s2) 

countR1 :: Int -> Int -> Int
countR1 r1 1 = r1 + 1
countR1 r1 r = r1

countR2 :: Int -> Int -> Int
countR2 r2 2 = r2 + 1
countR2 r2 r = r2

countR3 :: Int -> Int -> Int
countR3 r3 3 = r3 + 1
countR3 r3 r = r3

--this is to count nesting
countBI :: Int -> Int -> Int
countBI ne 1 = ne
countBI ne ff = ne +1
}