Browse Source

Refactoring, get rid of graph stuff

master
Nicolas Lenz 10 months ago
parent
commit
56ab21640d
3 changed files with 4 additions and 12 deletions
  1. 0
    3
      Data/Automata.idr
  2. 0
    9
      Data/Graph.idr
  3. 4
    0
      Main.idr

+ 0
- 3
Data/Automata.idr View File

@@ -98,9 +98,6 @@ data ENFA : (state : Type) -> (alph : Type) -> Type where
98 98
     ||| @ accepting The states that accept
99 99
     MkENFA : (delta : state -> Maybe alph -> List state) -> (start : state) -> (accepting : List state) -> ENFA state alph
100 100
 
101
-[epsilon] Graph (ENFA state alph) state where
102
-    neighbors (MkENFA delta _ _) state = delta state Nothing
103
-
104 101
 -- TODO: make total (breadth-/depth-first-search?)
105 102
 partial runENFAEpsilon : ENFA state alph -> state -> List state
106 103
 runENFAEpsilon a@(MkENFA delta _ _) st = (delta st Nothing) >>= (\x => runENFAEpsilon a x)

+ 0
- 9
Data/Graph.idr View File

@@ -1,9 +0,0 @@
1
-module Data.Graph
2
-
3
-%access export
4
-
5
-interface Graph a node where
6
-    neighbors : a -> node -> List node
7
-
8
---||| Calculates the transitive closure of a graph using the (floyd-)warshall algorithm
9
---closure : Graph g => g -> (node -> List node)

+ 4
- 0
Main.idr View File

@@ -2,6 +2,7 @@ module Main
2 2
 
3 3
 import Data.Automata
4 4
 import Data.Fin
5
+import Data.Listable
5 6
 
6 7
 nenTuples : List (Fin 4, Fin 2, Fin 4)
7 8
 nenTuples = [(0, 0, 1), (0, 1, 0), (1, 0, 1), (1, 1, 2), (2, 0, 3), (2, 1, 0), (3, 0, 3), (3, 1, 3)]
@@ -26,3 +27,6 @@ l1 = listed-}
26 27
 
27 28
 drei : Nat
28 29
 drei = 3
30
+
31
+testlel : Nat
32
+testlel = testkek

Loading…
Cancel
Save