jukebox 0.3.5 → 0.3.6

raw patch · 3 files changed

+10/−10 lines, 3 files

Files

• jukebox.cabal +1/−1
• src/Jukebox/Tools/EncodeTypes.hs +2/−2
• src/Jukebox/Tools/HornToUnit.hs +7/−7

@@ -1,5 +1,5 @@ Name: jukebox-Version: 0.3.5+Version: 0.3.6 Cabal-version: >= 1.8 Build-type: Simple Author: Nick Smallbone

@@ -99,7 +99,7 @@ tags :: Bool -> Scheme tags moreAxioms = Scheme   { makeFunction = \ty ->-      newFunction ("$to_" ++ base ty) [ty] ty,+      newFunction ("$$to_" ++ base ty) [ty] ty,     scheme1 = tags1 moreAxioms }  tags1 :: Bool -> (Type -> Bool) -> (Type -> Function) -> Scheme1@@ -147,7 +147,7 @@ guards :: Scheme guards = Scheme   { makeFunction = \ty ->-      newFunction ("$is_" ++ base ty) [ty] O,+      newFunction ("$$is_" ++ base ty) [ty] O,     scheme1 = guards1 }  guards1 :: (Type -> Bool) -> (Type -> Function) -> Scheme1

@@ -116,8 +116,8 @@       ((p ::: FunType tys bool) :@: ts) :=: true      (bool, true) = run_ prob $ do-      bool <- newType "bool"-      true <- newFunction "true" [] bool+      bool <- newType "$$bool"+      true <- newFunction "$$true" [] bool       return (bool, true :@: [])  eliminateMultiplePreconditions :: HornFlags -> Problem Clause -> Problem Clause@@ -166,9 +166,9 @@     addConjecture c = clause (Pos (a :=: b):toLiterals c)      (a, b) = run_ prob $ do-      token <- newType "$token"-      a <- newFunction "$a" [] token-      b <- newFunction "$b" [] token+      token <- newType "$$token"+      a <- newFunction "$$a" [] token+      b <- newFunction "$$b" [] token       return (a :@: [], b :@: [])  eliminateHornClauses :: HornFlags -> Problem Clause -> Either (Input Clause) (Problem Clause)@@ -286,8 +286,8 @@         what = clause [Pos l] }      (ifeqName, passiveName, xvar, yvar, zvar) = run_ prob $ do-      ifeqName <- newName "$ifeq"-      passiveName <- newName "$passive"+      ifeqName <- newName "$$ifeq"+      passiveName <- newName "$$passive"       xvar <- newName "A"       yvar <- newName "B"       zvar <- newName "C"