Move some tests around

Add a 'search' category

tests/Main.idr

@@ -7,13 +7,14 @@ import System
 ttimpTests : List String
 ttimpTests 
     = ["basic001", "basic002", "basic003", "basic004", "basic005",
-       "basic006", "basic007",
+       "basic006",
        "dot001",
        "eta001", "eta002",
        "lazy001",
        "nest001", "nest002",
        "perf001", "perf002", "perf003",
-       "qtt001", "qtt002", "qtt003"]
+       "qtt001", "qtt002", "qtt003",
+       "search001", "search002"]
 
 chdir : String -> IO Bool
 chdir dir 

tests/ttimp/basic003/expected

@@ -1,6 +1,11 @@
 Processing as TTImp
 Written TTC
-Yaffle> (((((Main.There [Just {a:17} = Main.Nat]) [Just y = (Main.S Main.Z)]) [Just xs = (((Main.Cons [Just a = Main.Nat]) Main.Z) (Main.Nil [Just a = Main.Nat]))]) [Just x = Main.Z]) (((Main.Here [Just {a:10} = Main.Nat]) [Just xs = (Main.Nil [Just a = Main.Nat])]) [Just x = Main.Z]))
-Yaffle> (((Main.Here [Just {a:10} = Main.Nat]) [Just xs = (((Main.Cons [Just a = Main.Nat]) Main.Z) (Main.Nil [Just a = Main.Nat]))]) [Just x = (Main.S Main.Z)])
-Yaffle> ((((Main.MkPair [Just b = Integer]) [Just a = String]) "b") 94)
+Yaffle> Main.foo : (%pi Rig0 Explicit Just {m:39} Main.Nat (%pi Rig0 Explicit Just {a:38} %type (%pi Rig0 Explicit Just {k:37} Main.Nat (%pi RigW Explicit Nothing {a:38} (%pi RigW Explicit Nothing ((Main.Vect {k:37}) {a:38}) (%pi RigW Explicit Nothing ((Main.Vect {m:39}) {a:38}) ((Main.Vect ((Main.plus {k:37}) {m:39})) {a:38})))))))
+Yaffle> Bye for now!
+Processing as TTC
+Read 1 holes
+Read 0 guesses
+Read 0 constraints
+Read TTC
+Yaffle> Main.foo : (%pi Rig0 Explicit Just {m:39} Main.Nat (%pi Rig0 Explicit Just {a:38} %type (%pi Rig0 Explicit Just {k:37} Main.Nat (%pi RigW Explicit Nothing {a:38} (%pi RigW Explicit Nothing ((Main.Vect {k:37}) {a:38}) (%pi RigW Explicit Nothing ((Main.Vect {m:39}) {a:38}) ((Main.Vect ((Main.plus {k:37}) {m:39})) {a:38})))))))
 Yaffle> Bye for now!

tests/ttimp/basic003/input

@@ -1,4 +1,2 @@
-isThere
-isThere2
-foo (MkPair (\x => x) (MkPair 'a' "b")) 94
+:t foo
 :q

tests/ttimp/basic003/run

@@ -1,3 +1,4 @@
-$1 Auto.yaff < input
+$1 Hole.yaff < input
+$1 build/Hole.ttc < input
 
 rm -rf build

tests/ttimp/basic007/expected

@@ -1,11 +0,0 @@
-Processing as TTImp
-Written TTC
-Yaffle> Main.foo : (%pi Rig0 Explicit Just {m:39} Main.Nat (%pi Rig0 Explicit Just {a:38} %type (%pi Rig0 Explicit Just {k:37} Main.Nat (%pi RigW Explicit Nothing {a:38} (%pi RigW Explicit Nothing ((Main.Vect {k:37}) {a:38}) (%pi RigW Explicit Nothing ((Main.Vect {m:39}) {a:38}) ((Main.Vect ((Main.plus {k:37}) {m:39})) {a:38})))))))
-Yaffle> Bye for now!
-Processing as TTC
-Read 1 holes
-Read 0 guesses
-Read 0 constraints
-Read TTC
-Yaffle> Main.foo : (%pi Rig0 Explicit Just {m:39} Main.Nat (%pi Rig0 Explicit Just {a:38} %type (%pi Rig0 Explicit Just {k:37} Main.Nat (%pi RigW Explicit Nothing {a:38} (%pi RigW Explicit Nothing ((Main.Vect {k:37}) {a:38}) (%pi RigW Explicit Nothing ((Main.Vect {m:39}) {a:38}) ((Main.Vect ((Main.plus {k:37}) {m:39})) {a:38})))))))
-Yaffle> Bye for now!

tests/ttimp/basic007/input

@@ -1,2 +0,0 @@
-:t foo
-:q

tests/ttimp/basic007/run

@@ -1,4 +0,0 @@
-$1 Hole.yaff < input
-$1 build/Hole.ttc < input
-
-rm -rf build

tests/ttimp/search001/expected

@@ -0,0 +1,6 @@
+Processing as TTImp
+Written TTC
+Yaffle> (((((Main.There [Just {a:17} = Main.Nat]) [Just y = (Main.S Main.Z)]) [Just xs = (((Main.Cons [Just a = Main.Nat]) Main.Z) (Main.Nil [Just a = Main.Nat]))]) [Just x = Main.Z]) (((Main.Here [Just {a:10} = Main.Nat]) [Just xs = (Main.Nil [Just a = Main.Nat])]) [Just x = Main.Z]))
+Yaffle> (((Main.Here [Just {a:10} = Main.Nat]) [Just xs = (((Main.Cons [Just a = Main.Nat]) Main.Z) (Main.Nil [Just a = Main.Nat]))]) [Just x = (Main.S Main.Z)])
+Yaffle> ((((Main.MkPair [Just b = Integer]) [Just a = String]) "b") 94)
+Yaffle> Bye for now!

tests/ttimp/search001/input

@@ -0,0 +1,4 @@
+isThere
+isThere2
+foo (MkPair (\x => x) (MkPair 'a' "b")) 94
+:q

tests/ttimp/search001/run

@@ -0,0 +1,3 @@
+$1 Auto.yaff < input
+
+rm -rf build