diff --git a/documentation.sh b/documentation.sh index 4670d93..b27808f 100755 --- a/documentation.sh +++ b/documentation.sh @@ -1,4 +1,6 @@ #!/bin/sh cabal haddock --hyperlink-source sed -i 's/file\:\/\/\/usr\/local\/haskell\/ghc\-7\.8\.3\-x86_64\/share\/doc\/ghc\/html\/libraries\/\(base\-4\.7\.0\.1\)/http:\/\/hackage.haskell.org\/package\/\1\/docs/g' dist/doc/html/NLambda/NLambda.html +sed -i 's/file\:\/\/\/usr\/local\/haskell\/ghc\-7\.8\.3\-x86_64\/share\/doc\/ghc\/html\/libraries\/\(containers\-0\.5\.5\.1\)/http:\/\/hackage.haskell.org\/package\/\1\/docs/g' dist/doc/html/NLambda/NLambda.html +sed -i 's/file\:\/\/\/usr\/local\/haskell\/ghc\-7\.8\.3\-x86_64\/lib\/\(mtl\-2\.1\.3\.1\)\/doc\/html/http:\/\/hackage.haskell.org\/package\/\1\/docs/g' dist/doc/html/NLambda/NLambda.html sed -i 's/Nominal.html/NLambda.html/g' dist/doc/html/NLambda/NLambda.html diff --git a/src/Main b/src/Main deleted file mode 100755 index 86b020a..0000000 Binary files a/src/Main and /dev/null differ diff --git a/src/Main.hs b/src/Main.hs deleted file mode 100644 index b72a583..0000000 --- a/src/Main.hs +++ /dev/null @@ -1,4 +0,0 @@ -import NLambda - - -main = print $ (result1,result2,result3,result4,result5) diff --git a/src/Nominal/Conditional.hs b/src/Nominal/Conditional.hs index 7cb1ec2..9c5ce0a 100644 --- a/src/Nominal/Conditional.hs +++ b/src/Nominal/Conditional.hs @@ -21,7 +21,7 @@ instance Conditional b => Conditional (a -> b) where instance (Conditional a) => Conditional [a] where cond c l1 l2 = if length l1 == length l2 then zipWith (cond c) l1 l2 - else ifSolve c l1 l2 (error "cond cannot be applied to lists of different sizes with unsolvable condition") + else ifSolve c l1 l2 (error "cond cannot be applied to lists of different sizes with undetermined condition") instance Conditional () where cond c _ _ = () diff --git a/src/Nominal/TestFormula.hs b/src/Nominal/TestFormula.hs deleted file mode 100644 index 36f42f2..0000000 --- a/src/Nominal/TestFormula.hs +++ /dev/null @@ -1,148 +0,0 @@ -module Nominal.TestFormula where - -import Nominal.Formula -import Nominal.Type -import Nominal.Variable -import Prelude hiding (not) -import Test.HUnit - -x = variable "x" -y = variable "y" -z = variable "z" -xy = eq x y -xz = eq x z -yz = eq y z -lt = lessThan -le = lessEquals -gt = greaterThan -ge = greaterEquals - -x1 = variable "x1" -x2 = variable "x2" -x3 = variable "x3" -x4 = variable "x4" -x5 = variable "x5" -x6 = variable "x6" -f1 = existsVar x2 $ eq x1 x2 \/ eq x2 x3 -f2 = existsVar x5 $ eq x4 x5 \/ eq x5 x6 - -tests = test [true ~=? eq x x, -- 0 - eq x y ~=? eq y x, -- 1 - false ~=? neq x x, -- 2 - neq x y ~=? neq y x, -- 3 - - false ~=? lt x x, -- 4 - gt x y ~=? lt y x, -- 5 - true ~=? le x x, -- 6 - ge x y ~=? le y x, -- 7 - - false ~=? gt x x, -- 8 - lt x y ~=? gt y x, -- 9 - true ~=? ge x x, -- 10 - le x y ~=? ge y x, -- 11 - - true ~=? not false, -- 12 - false ~=? not true, -- 13 - neq x y ~=? not (eq x y), -- 14 - eq x y ~=? not (neq x y), -- 15 - ge x y ~=? not (lt x y), -- 16 - gt x y ~=? not (le x y), -- 17 - lt x y ~=? not (ge x y), -- 18 - le x y ~=? not (gt x y), -- 19 - - true ~=? true /\ true, -- 20 - false ~=? true /\ false, -- 21 - false ~=? false /\ true, -- 22 - false ~=? false /\ false, -- 23 - - true ~=? true \/ true, -- 24 - true ~=? true \/ false, -- 25 - true ~=? false \/ true, -- 26 - false ~=? false \/ false, -- 27 - - xy ~=? true /\ xy, -- 28 - xy ~=? xy /\ true, -- 29 - false ~=? false /\ xy, -- 30 - false ~=? xy /\ false, -- 31 - - true ~=? true \/ true, -- 32 - true ~=? true \/ false, -- 33 - true ~=? false \/ true, -- 34 - false ~=? false \/ false, -- 35 - - true ~=? true \/ xy, -- 36 - true ~=? xy \/ true, -- 37 - xy ~=? false \/ xy, -- 38 - xy ~=? xy \/ false, -- 39 - - xy /\ (xz /\ yz) ~=? (xy /\ xz) /\ yz, -- 40 - xy \/ (xz \/ yz) ~=? (xy \/ xz) \/ yz, -- 41 - xy ~=? xy /\ (lt y z \/ ge x z), -- 42 - - lt x y ~=? lt x y /\ lt x y, -- 43 - lt x y ~=? lt x y /\ le x y, -- 44 - false ~=? lt x y /\ eq x y, -- 45 - lt x y ~=? lt x y /\ neq x y, -- 46 - false ~=? lt x y /\ ge x y, -- 47 - false ~=? lt x y /\ gt x y, -- 48 - - lt x y ~=? le x y /\ lt x y, -- 49 - le x y ~=? le x y /\ le x y, -- 50 - eq x y ~=? le x y /\ eq x y, -- 51 - lt x y ~=? le x y /\ neq x y, -- 52 - eq x y ~=? le x y /\ ge x y, -- 53 - false ~=? le x y /\ gt x y, -- 54 - - false ~=? eq x y /\ lt x y, -- 55 - eq x y ~=? eq x y /\ le x y, -- 56 - eq x y ~=? eq x y /\ eq x y, -- 57 - false ~=? eq x y /\ neq x y, -- 58 - eq x y ~=? eq x y /\ ge x y, -- 59 - false ~=? eq x y /\ gt x y, -- 60 - - lt x y ~=? neq x y /\ lt x y, -- 61 - lt x y ~=? neq x y /\ le x y, -- 62 - false ~=? neq x y /\ eq x y, -- 63 - neq x y ~=? neq x y /\ neq x y, -- 64 - gt x y ~=? neq x y /\ ge x y, -- 65 - gt x y ~=? neq x y /\ gt x y, -- 66 - - false ~=? ge x y /\ lt x y, -- 67 - eq x y ~=? ge x y /\ le x y, -- 68 - eq x y ~=? ge x y /\ eq x y, -- 69 - gt x y ~=? ge x y /\ neq x y, -- 70 - ge x y ~=? ge x y /\ ge x y, -- 71 - gt x y ~=? ge x y /\ gt x y, -- 72 - - f1 ~=? f1 /\ f1, -- 73 - f1 ~=? true /\ f1, -- 74 - f1 ~=? f1 /\ true, -- 75 - false ~=? false /\ f1, -- 76 - false ~=? f1 /\ false, -- 77 - false ~=? f1 /\ not f1 /\ f2, -- 78 - f1 ~=? f1 /\ (f1 \/ f2), -- 79 - f1 /\ f2 ~=? f1 /\ (not f1 \/ f2), -- 80 - false ~=? eq x y /\ neq y x, -- 81 - eq x y /\ eq x z ~=? eq z y /\ eq y x /\ eq z x, -- 82 - - f1 ~=? f1 \/ f1, -- 83 - true ~=? true \/ f1, -- 84 - true ~=? f1 \/ true, -- 85 - f1 ~=? false \/ f1, -- 86 - f1 ~=? f1 \/ false, -- 87 - true ~=? f1 \/ not f1 \/ f2, -- 88 - f1 ~=? f1 \/ (f1 /\ f2), -- 89 - f1 \/ f2 ~=? f1 \/ (not f1 /\ f2), -- 90 - true ~=? eq x y \/ neq y x, -- 91 - - true ~=? (∀) x true, -- 92 - false ~=? (∀) x false, -- 93 - eq y z ~=? (∀) x (eq y z), -- 94 - false ~=? (∀) x (eq x y), -- 95 - - true ~=? (∃) x true, -- 96 - false ~=? (∃) x false, -- 97 - eq y z ~=? (∃) x (eq y z), -- 98 - true ~=? (∃) x (eq x y)] -- 99 - -main = runTestTT tests diff --git a/src/Nominal/Util/UnionFind.hs b/src/Nominal/Util/UnionFind.hs deleted file mode 100644 index 88e9e1e..0000000 --- a/src/Nominal/Util/UnionFind.hs +++ /dev/null @@ -1,34 +0,0 @@ -module Nominal.Util.UnionFind where - -import Data.Map (Map) -import qualified Data.Map as Map - ----------------------------------------------------------------------------------------------------- --- Disjoint-set data structure ----------------------------------------------------------------------------------------------------- - -data UnionFind a = UnionFind {parents :: Map a a, ranks :: Map a Int} deriving Show - -empty :: UnionFind a -empty = UnionFind Map.empty Map.empty - -find :: Ord a => a -> UnionFind a -> (a, UnionFind a) -find e uf@(UnionFind ps rs) = case Map.lookup e ps of - Nothing -> (e, uf) - Just parent -> let (repr, UnionFind ps' rs') = find parent uf - in (repr, UnionFind (Map.insert e repr ps') rs') - -union :: Ord a => a -> a -> UnionFind a -> UnionFind a -union e1 e2 uf@(UnionFind ps rs) - | repr1 == repr2 = uf - | r1 > r2 = UnionFind (Map.insert repr2 repr1 ps') rs' - | r1 < r2 = UnionFind (Map.insert repr1 repr2 ps') rs' - | otherwise = UnionFind (Map.insert repr2 repr1 ps') (Map.insert repr1 (succ r1) rs') - where (repr1, uf') = find e1 uf - (repr2, UnionFind ps' rs') = find e2 uf' - r1 = Map.findWithDefault 0 repr1 rs' - r2 = Map.findWithDefault 0 repr2 rs' - -assocs :: Ord a => UnionFind a -> [(a, a)] -assocs uf@(UnionFind ps rs) = snd $ foldl (\(uf', res) e -> let (repr, uf'') = find e uf' - in (uf'', (e, repr) : res)) (uf, []) (Map.keys ps) diff --git a/src/TODO b/src/TODO deleted file mode 100644 index cfff90c..0000000 --- a/src/TODO +++ /dev/null @@ -1,51 +0,0 @@ -- dodać moduł BinaryRelation z ktorego bedzie korzystał graph -- specjalny show dla prostego zbioru atomów -- pomyśleć nad kratą dla folda na zbiorze nominalnym - - -- dokumentacja za pomoca haddock, -- pragma MINIMAL -- stworzyc listy eksportowe dla modułów, -- napisać testy jednostkowe - -- Formula: --- przenieść ifFormula i dodać simplify i solve, --- ew. przeniesc upraszczanie formul do oddzielnego modułu --- poprawić nawiasowanie przy kwantyfikatorach --- ustawić infixl dla operatorów, --- upraszczanie: ---- (a /\ b) \/ (a /\ not b) -> a, ---- (a \/ b) /\ (a \/ not b) -> a /\ not b - -- Nominal: --- zastanowić się jaki ma być "strict", --- dodac instancje dla NominalType, Conditional: Either, Maybe, Map, Set --- pomyśleć nad odpowiednikami operacji z ' na koncu, ktore czesciej rozwiazuja formuly (ewentualnie za pomoca makra #define), --- sprawdzic czy potrzebne sa wewnetrzne optymalne funkcje: isSubsetOf, intersection, difference. --- zaimplementować pairs i podobne, --- pomyśleć nad problemem rozwiązywania konfliktu nazw zmiennych iteracyjnych - czy istnieje rozwiązanie "strict"? --- pomyśleć nad problemem obliczania wsparcia dla zbioru: insert a atomSet - może przy "insert" trzeba sprawdzić "contains", czyli rozwiązać formułę --- rozwiązywanie konfliktów zmiennych - poziomy zgodnie z zagnieżdzeniem, a nie: {{{(a₁,c₁,b₁) : for b₁ ∊ 𝔸} : for c₁ ∊ 𝔸} : for a₁ ∊ 𝔸} -- zrównoleglić wyszukiwanie zmiennych z równym i różnym id w funkcji checkIdentifiers - --- rozmiar zbioru, fold - krata, obliczanie maxa dla funkcji Atom -> Int --- automatyczne wyliczanie formuł --- upraszczanie formuł (moze za pomocą Z3) --- programy: spojność w grafie, minimalizacji automatu - -Algorytmy: -- zbiory: --- istnieje ekwiwariantna bijekcja: (A\{a} A\{b} {a,b}) -- grafy: --- dwudzielnosc, --- trojkolorowalnosc, --- dijkstra, --- osiagalnosc, -- automaty: --- minimalizacja, --- rownowaznosc. - - -rozważyć eliminację zmiennych nie występujących w iteracji i wartości -!!! wykorzystać variants w wariantach, a nie tylko w zbiorach -!!! pomyslec o stosach formula przy uruchamianiu solverow - moze warianty i zbiory powinny miec specyficzne implementacje ite'