jukebox 0.5.2 → 0.5.3

raw patch · 4 files changed

+46/−3 lines, 4 files

Files

jukebox.cabal +1/−1
src/Jukebox/Form.hs +33/−0
src/Jukebox/TPTP/Parse/Core.hs +1/−1
src/Jukebox/Tools/EncodeTypes.hs +11/−1

jukebox.cabal view

@@ -1,5 +1,5 @@ Name: jukebox-Version: 0.5.2+Version: 0.5.3 Cabal-version: >= 1.10 Build-type: Simple Author: Nick Smallbone

src/Jukebox/Form.hs view

@@ -105,6 +105,26 @@ size Var{} = 1 size (_f :@: xs) = 1 + sum (map size xs) +subterms :: Term -> [Term]+subterms t =+  t:+  case t of+    Var _ -> []+    _f :@: ts -> concatMap subterms ts++contexts :: Term -> [(Term, Term -> Term)]+contexts t = ctxs t id+  where+    ctxs :: Term -> (Term -> Term) -> [(Term, Term -> Term)]+    ctxs t k =+      (t, k):+      case t of+        Var _ -> []+        f :@: ts ->+          concat+          [ ctxs (ts !! i) (\u -> k (f :@: (take i ts ++ [u] ++ drop (i+1) ts)))+          | i <- [0..length ts-1] ]+ ---------------------------------------------------------------------- -- Literals @@ -519,6 +539,19 @@      generic :: Symbolic a => a -> a     generic t = recursively (subst s) t++match :: Term -> Term -> Maybe Subst+match pat t = execStateT (matchM pat t) ids+  where+    matchM (Var x) t = do+      sub <- get+      case Map.lookup x sub of+        Nothing -> put (sub |+| (x |=> t))+        Just u | u == t -> return ()+        _ -> mzero+    matchM (f :@: ts) (g :@: us) | f == g =+      zipWithM_ matchM ts us+    matchM _ _ = mzero  ---------------------------------------------------------------------- -- Functions operating on symbolic terms

src/Jukebox/TPTP/Parse/Core.hs view

@@ -56,7 +56,7 @@           | (kind, ty) <- tys ])        | (fun, tys) <- funs ])    where-     overloads f = [(ty, f ty) | ty <- [intType, ratType, realType]]+     overloads f = [(ty, f ty) | ty <- [intType, ratType, realType, indType]]      fun xs f = [(x, overloads f) | x <- xs]       funs =

src/Jukebox/Tools/EncodeTypes.hs view

@@ -82,7 +82,17 @@                 fmap notInwards $ prepare $ nt f       trType O = O       trType _ = indType-  in Form.run (translate1 scheme mono f') (return . mapType trType)+      quoteNumbers tagName name+        | isNumber name = name `variant` [tagName]+        | otherwise = name+      isNumber (Fixed (Integer _) _) = True+      isNumber (Fixed (Rational _) _) = True+      isNumber (Fixed (Real _) _) = True+      isNumber _ = False++  in Form.run (translate1 scheme mono f') $ \form -> do+    name <- newName ""+    return $ mapName (quoteNumbers name) $ mapType trType form  -- Typing functions.