quox/tests/Tests/FreeVars.idr

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
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
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
Doc80 : Type
Doc80 = Doc $ Opts 80

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
  withContext 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 Doc80
    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 (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],
  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"] [<] (^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] [<],

  todo "others"
]