<commit_before>{-# LANGUAGE UnicodeSyntax #-}
--------------------------------------------------------------------------------
-- File   : Base
-- Author : <NAME>
-- Date   : Sat Apr 18 14:11:27 2015
-- Description : Basic functions for parsing
--------------------------------------------------------------------------------
-- Change log :

--------------------------------------------------------------------------------

module TSTP.Base where

import Data.TSTP
import Data.Function (on)
import Data.Set (Set,toList,fromList,difference,unions,singleton,empty)

--TODO: implement this
univquant_free_vars :: Formula -> Formula
univquant_free_vars cnf = Quant All free_vars cnf
    where free_vars = toList $ freeVarsF cnf

freeVarsF ∷ Formula → Set V
freeVarsF ((:~:) x)         = freeVarsF x
freeVarsF (Quant _ vars x)  = difference (freeVarsF x) (fromList vars)
freeVarsF (BinOp x _ y)     = (mappend `on` freeVarsF) x y
freeVarsF (InfixPred x _ y) = (mappend `on` freeVarsT) x y
freeVarsF (PredApp _ args)  = unions (fmap freeVarsT args)

freeVarsT ∷ Term → Set V
freeVarsT (Var x)         = singleton x
freeVarsT (FunApp _ args) = unions (fmap freeVarsT args)
freeVarsT _               = empty


<commit_msg>More travis fixs<commit_after>{-# LANGUAGE UnicodeSyntax #-}
--------------------------------------------------------------------------------
-- File   : Base
-- Author : <NAME>
-- Date   : Sat Apr 18 14:11:27 2015
-- Description : Basic functions for parsing
--------------------------------------------------------------------------------
-- Change log :

--------------------------------------------------------------------------------

module TSTP.Base where

import Data.TSTP
import Data.Function (on)
import Data.Set (Set,toList,fromList,difference,unions,singleton,empty)
import Data.Monoid (mappend)

--TODO: implement this
univquant_free_vars :: Formula -> Formula
univquant_free_vars cnf = Quant All free_vars cnf
    where free_vars = toList $ freeVarsF cnf

freeVarsF ∷ Formula → Set V
freeVarsF ((:~:) x)         = freeVarsF x
freeVarsF (Quant _ vars x)  = difference (freeVarsF x) (fromList vars)
freeVarsF (BinOp x _ y)     = (mappend `on` freeVarsF) x y
freeVarsF (InfixPred x _ y) = (mappend `on` freeVarsT) x y
freeVarsF (PredApp _ args)  = unions (fmap freeVarsT args)

freeVarsT ∷ Term → Set V
freeVarsT (Var x)         = singleton x
freeVarsT (FunApp _ args) = unions (fmap freeVarsT args)
freeVarsT _               = empty



{'fraction_non_alphanumeric': 0.276604386677498, 'fraction_numerical': 0.00974817221770918, 'mean_word_length': 1.6742671009771988, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 7, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2047543', 'n_tokens_mistral': 745, 'n_tokens_neox': 738, 'n_words': 229}