lib/Quox/Context.idr

@@ -109,21 +109,18 @@ fromSnocVect [<]       = [<]
 fromSnocVect (sx :< x) = fromSnocVect sx :< x
 
 
-public export
-tabulateLT : (n : Nat) -> ((i : Nat) -> (0 p : i `LT` n) => tm i) ->
-             Context tm n
-tabulateLT 0     f = [<]
-tabulateLT (S k) f =
-  tabulateLT k (\i => f i @{lteSuccRight %search}) :< f k @{reflexive}
+export
+tabulateVar : (n : Nat) -> (Var n -> a) -> Context' a n
+tabulateVar 0     f = [<]
+tabulateVar (S k) f = tabulateVar k (f . VS) :< f VZ
 
-public export
-tabulate : ((n : Nat) -> tm n) -> (n : Nat) -> Context tm n
-tabulate f n = tabulateLT n (\i => f i)
--- [todo] fixup argument order lol
+export
+allVars : (n : Nat) -> Context' (Var n) n
+allVars n = tabulateVar n id
 
 public export
 replicate : (n : Nat) -> a -> Context' a n
-replicate n x = tabulate (const x) n
+replicate n x = tabulateVar n $ const x
 
 
 public export

lib/Quox/FreeVars.idr

@@ -62,7 +62,7 @@ export %inline [AndM] {n : Nat} -> Monoid (FreeVars n) where neutral = all
 
 private
 self : {n : Nat} -> Context' (FreeVars n) n
-self = tabulate (\i => FV $ tabulate (== i) n) n
+self = tabulateVar n $ \i => FV $ tabulateVar n (== i)
 
 export
 shift : forall from, to. Shift from to -> FreeVars from -> FreeVars to
@@ -74,13 +74,12 @@ shift by (FV xs) = FV $ shift' by xs where
 
 export
 fromSet : {n : Nat} -> SortedSet (Var n) -> FreeVars n
-fromSet vs = FV $ tabulateLT n $ \i => contains (V i) vs
+fromSet vs = FV $ tabulateVar n $ \i => contains i vs
 
 export
 toSet : {n : Nat} -> FreeVars n -> SortedSet (Var n)
-toSet (FV vs) =
-  foldl_ (\s, i => maybe s (\i => insert i s) i) empty $
-  zipWith (\i, b => guard b $> i) (tabulateLT n V) vs
+toSet (FV vs) = SortedSet.fromList $ fold $
+                Context.zipWith (\i, b => i <$ guard b) (allVars n) vs
 
 
 public export
@@ -230,7 +229,7 @@ HasFreeVars (Elim d) where
 
 private
 expandDShift : {d1 : Nat} -> Shift d1 d2 -> Loc -> Context' (Dim d2) d1
-expandDShift by loc = tabulateLT d1 (\i => BV i loc // by)
+expandDShift by loc = tabulateVar d1 (\i => B i loc // by)
 
 private
 expandDSubst : {d1 : Nat} -> DSubst d1 d2 -> Loc -> Context' (Dim d2) d1

lib/Quox/Var.idr

@@ -144,15 +144,7 @@ interface FromVar f where %inline fromVar : Var n -> Loc -> f n
 
 public export FromVar Var where fromVar x _ = x
 
-export
-tabulateV : {0 tm : Nat -> Type} -> (forall n. Var n -> tm n) ->
-            (n : Nat) -> Vect n (tm n)
-tabulateV f 0     = []
-tabulateV f (S n) = f VZ :: tabulateV (f . VS) n
 
-export
-allVars : (n : Nat) -> Vect n (Var n)
-allVars n = tabulateV id n
 
 
 public export

tests/Tests/FreeVars.idr

@@ -26,6 +26,15 @@ ToInfo Failure where
               ("expected", show f.expected),
               ("got",      show f.got)]
 
+private
+testFreeVars1 : {d : Nat} -> HasFreeVars f =>
+                (f d -> String) -> f d -> FreeVars' d -> Test
+testFreeVars1 lbl tm dims =
+  test (lbl tm) $ do
+    let dims = FV dims; dims' = fv tm
+    unless (dims == dims')  $ Left $ Fail Dim dims dims'
+    Right ()
+
 private
 testFreeVars : {d, n : Nat} -> (HasFreeVars (f d), HasFreeDVars f) =>
                (f d n -> String) -> f d n -> FreeVars' d -> FreeVars' n -> Test
@@ -45,6 +54,22 @@ private
 prettyWith : (a -> Eff Pretty Doc80) -> a -> String
 prettyWith f = trim . render _ . runPretty . f
 
+parameters {d : Nat} (ds : BContext d)
+  private
+  withContext1 : Doc80 -> Eff Pretty Doc80
+  withContext1 doc =
+    if null ds then pure $ hsep ["⊢", doc]
+    else pure $ sep [hsep [!(ctx1 ds), "⊢"], doc]
+  where
+    ctx1 : forall k. BContext k -> Eff Pretty Doc80
+    ctx1 [<] = pure "·"
+    ctx1 ctx = fillSeparateTight !commaD . toList' <$>
+               traverse' (pure . prettyBind') ctx
+
+  private
+  testFreeVarsD : Dim d -> FreeVars' d -> Test
+  testFreeVarsD = testFreeVars1 $ prettyWith $ withContext1 <=< prettyDim ds
+
 parameters {d, n : Nat} (ds : BContext d) (ts : BContext n)
   private
   withContext : Doc80 -> Eff Pretty Doc80
@@ -67,7 +92,13 @@ parameters {d, n : Nat} (ds : BContext d) (ts : BContext n)
 
 export
 tests : Test
-tests = "free variables" :- [
+tests = "free variables (fv/fdv)" :- [
+  testFreeVarsD [<] (^K Zero) [<],
+  testFreeVarsD [<"i", "j"] (^K Zero) [<False, False],
+  testFreeVarsD [<"i", "j"] (^BV 0) [<False, True],
+  testFreeVarsD [<"i", "j"] (^BV 1) [<True, False],
+  testFreeVarsD [<"i", "j", "k", "l"] (^BV 2) [<False, True, False, False],
+
   testFreeVarsT [<] [<] (^TYPE 0) [<] [<],
   testFreeVarsT [<"i", "j"] [<] (^TYPE 0) [<False, False] [<],
   testFreeVarsT [<] [<"x", "y"] (^TYPE 0) [<] [<False, False],
@@ -98,6 +129,10 @@ tests = "free variables" :- [
 
   testFreeVarsT [<"i","j"] [<] (^DLamY "k" (E $ ^DApp (^F "eq" 0) (^BV 0)))
                 [<False,False] [<],
+  testFreeVarsT [<"i","j"] [<] (^DLamY "k" (E $ ^DApp (^F "eq" 0) (^BV 2)))
+                [<True,False] [<],
+  testFreeVarsT [<"i","j"] [<] (^DLamY "i" (E $ ^DApp (^F "eq" 0) (^BV 0)))
+                [<False,False] [<],
   testFreeVarsT [<"i","j"] [<] (^DLamN (E $ ^DApp (^F "eq" 0) (^BV 0)))
                 [<False,True] [<],