a few basic fv tests to make sure it's not reversed or whatever

lib/Quox/FreeVars.idr

@@ -5,12 +5,22 @@ import Data.Maybe
 import Data.Nat
 import Data.Singleton
 import Data.SortedSet
+import Derive.Prelude
 
+%language ElabReflection
+
+
+public export
+FreeVars' : Nat -> Type
+FreeVars' n = Context' Bool n
 
 public export
 record FreeVars n where
   constructor FV
-  vars : Context' Bool n
+  vars : FreeVars' n
+%name FreeVars xs
+
+%runElab deriveIndexed "FreeVars" [Eq, Ord, Show]
 
 
 export %inline
@@ -28,7 +38,7 @@ export %inline [AndS] Semigroup (FreeVars n) where (<+>) = (&&)
 export
 only : {n : Nat} -> Var n -> FreeVars n
 only i = FV $ only' i where
-  only' : {n' : Nat} -> Var n' -> Context' Bool n'
+  only' : {n' : Nat} -> Var n' -> FreeVars' n'
   only' VZ     = replicate (pred n') False :< True
   only' (VS i) = only' i :< False
 
@@ -57,7 +67,7 @@ self = tabulate (\i => FV $ tabulate (== i) n) n
 export
 shift : forall from, to. Shift from to -> FreeVars from -> FreeVars to
 shift by (FV xs) = FV $ shift' by xs where
-  shift' : Shift from' to' -> Context' Bool from' -> Context' Bool to'
+  shift' : Shift from' to' -> FreeVars' from' -> FreeVars' to'
   shift' SZ      ctx = ctx
   shift' (SS by) ctx = shift' by ctx :< False
 

tests/Tests.idr

@@ -2,6 +2,7 @@ module Tests
 
 import TAP
 import Tests.DimEq
+import Tests.FreeVars
 import Tests.Reduce
 import Tests.Equal
 import Tests.Typechecker
@@ -15,6 +16,7 @@ import System
 allTests : List Test
 allTests = [
   DimEq.tests,
+  FreeVars.tests,
   Reduce.tests,
   Equal.tests,
   Typechecker.tests,

tests/Tests/FreeVars.idr

@@ -0,0 +1,101 @@
+module Tests.FreeVars
+
+import Quox.Pretty
+import Quox.Syntax
+import Quox.FreeVars
+import AstExtra
+import TAP
+import Derive.Prelude
+
+%language ElabReflection
+
+
+private
+data FailureType = Dim | Term
+%runElab derive "FailureType" [Show]
+
+private
+record Failure where
+  constructor Fail
+  type : FailureType
+  expected, got : FreeVars n
+
+private
+ToInfo Failure where
+  toInfo f = [("type",     show f.type),
+              ("expected", show f.expected),
+              ("got",      show f.got)]
+
+private
+testFreeVars : {d, n : Nat} -> (HasFreeVars (f d), HasFreeDVars f) =>
+               (f d n -> String) -> f d n -> FreeVars' d -> FreeVars' n -> Test
+testFreeVars lbl tm dims terms =
+  test (lbl tm) $ do
+    let dims  = FV dims; terms  = FV terms
+        dims' = fdv tm;  terms' = fv tm
+    unless (dims  == dims')  $ Left $ Fail Dim  dims  dims'
+    unless (terms == terms') $ Left $ Fail Term terms terms'
+    Right ()
+
+private
+prettyWith : (a -> Eff Pretty (Doc (Opts 80))) -> a -> String
+prettyWith f = trim . render _ . runPretty . f
+
+parameters {d, n : Nat} (ds : BContext d) (ts : BContext n)
+  private
+  withContext : {opts : _} -> Doc opts -> Eff Pretty (Doc opts)
+  withContext {opts} doc =
+    if null ds && null ts then pure $ hsep ["⊢", doc]
+    else pure $ sep [hsep [!(ctx1 ds), "|", !(ctx1 ts), "⊢"], doc]
+  where
+    ctx1 : forall k. BContext k -> Eff Pretty (Doc opts)
+    ctx1 [<] = pure "·"
+    ctx1 ctx = fillSeparateTight !commaD . toList' <$>
+               traverse' (pure . prettyBind') ctx
+
+  private
+  testFreeVarsT : Term d n -> FreeVars' d -> FreeVars' n -> Test
+  testFreeVarsT = testFreeVars $ prettyWith $ withContext <=< prettyTerm ds ts
+
+  private
+  testFreeVarsE : Elim d n -> FreeVars' d -> FreeVars' n -> Test
+  testFreeVarsE = testFreeVars $ prettyWith $ withContext <=< prettyElim ds ts
+
+export
+tests : Test
+tests = "free variables" :- [
+  testFreeVarsT [<] [<] (^TYPE 0) [<] [<],
+  testFreeVarsT [<"i", "j"] [<] (^TYPE 0) [<False, False] [<],
+  testFreeVarsT [<] [<"x", "y"] (^TYPE 0) [<] [<False, False],
+  testFreeVarsT [<"i"] [<"x"] (^TYPE 0) [<False] [<False],
+
+  testFreeVarsE [<] [<] (^F "f" 0) [<] [<],
+  testFreeVarsE [<] [<] (^F "f" 6) [<] [<],
+  testFreeVarsE [<"i"] [<] (^F "f" 0) [<False] [<],
+  testFreeVarsE [<] [<"x"] (^F "f" 0) [<] [<False],
+
+  testFreeVarsE [<] [<"x"] (^BV 0) [<] [<True],
+  testFreeVarsE [<"i"] [<"x"] (^BV 0) [<False] [<True],
+  testFreeVarsE [<] [<"x","y"] (^BV 1) [<] [<True,False],
+  testFreeVarsE [<] [<"x","y"] (^BV 0) [<] [<False,True],
+  testFreeVarsE [<] [<"x","y","z"] (^BV 1) [<] [<False,True,False],
+
+  testFreeVarsE [<] [<"x","y"] (^App (^BV 1) (^BVT 0)) [<] [<True,True],
+  testFreeVarsE [<] [<"x","y","z"] (^App (^BV 1) (^BVT 0))
+                [<] [<False,True,True],
+  testFreeVarsE [<] [<"x","y"] (^App (^BV 1) (^TYPE 1)) [<] [<True,False],
+
+  testFreeVarsT [<"i"] [<"x"] (^LamY "y" (^BVT 0)) [<False] [<False],
+  testFreeVarsT [<"i"] [<"x"] (^LamN (^BVT 0)) [<False] [<True],
+
+  testFreeVarsE [<"i","j"] [<] (^DApp (^F "eq" 0) (^BV 0)) [<False,True] [<],
+  testFreeVarsE [<"i","j"] [<] (^DApp (^F "eq" 0) (^BV 1)) [<True,False] [<],
+  testFreeVarsE [<"i","j"] [<] (^DApp (^F "eq" 0) (^K Zero)) [<False,False] [<],
+
+  testFreeVarsT [<"i","j"] [<] (^DLamY "k" (E $ ^DApp (^F "eq" 0) (^BV 0)))
+                [<False,False] [<],
+  testFreeVarsT [<"i","j"] [<] (^DLamN (E $ ^DApp (^F "eq" 0) (^BV 0)))
+                [<False,True] [<],
+
+  todo "others"
+]

tests/quox-tests.ipkg

@@ -8,6 +8,7 @@ modules =
   AstExtra,
   TypingImpls,
   PrettyExtra,
+  Tests.FreeVars,
   Tests.DimEq,
   Tests.Reduce,
   Tests.Equal,