

-- #!/usr/bin/env runghc


-- (,st') in parse
-- {-# LANGUAGE TupleSections #-}


-- {-# LANGUAGE LambdaCase #-}


{-# LANGUAGE OverloadedStrings #-}



{-# LANGUAGE CPP #-}
-- {-# OPTIONS_GHC -cpp -DPiForallInstalled #-}


-- |
-- Copyright :  (c) Andreas Reuleaux 2015
-- License   :  BSD2
-- Maintainer:  Andreas Reuleaux <rx@a-rx.info>
-- Stability :  experimental
-- Portability: non-portable
--
-- This module tests Pire's parser, forget, and untie functionality




{-
     toggle w/ opts in cabal file

     cpp-options: -DPiForallInstalled

cf
http://stackoverflow.com/questions/6361846/where-can-i-learn-about-ifdef



+ setting ghc/ghci cmd line options (from man ghci)
-cpp  -Dsymbol=value -U  -Usymbol ...


thus eg.
ghci -cpp -DPiForallInstalled


these seem not to work (?)
cabal repl --ghc-options="-cpp -DPiForallInstalled"
anyway NOT cabal repl --ghc-options="--cpp-options=-DPiForallInstalled"


can the -cpp be set on the cabal repl cmd line at all?


but better just toggle w/
-- {-# OPTIONS_GHC -cpp -DPiForallInstalled #-}




-}




{-

usage

./tests.hs
./tests.hs -p sorting
etc

./tests.hs -h

resp.

Pire.Tests.main'

eg.
  :l Pire.Tests
  main' "*"
  or
  main' "basic"
  main' "nat"



meanwhile just
runhaskell -package-db=.cabal-sandbox/x86_64-linux-ghc-7.6.3-packages.conf.d tests.hs -p parsing


-}


-- has to be module Main (or nothing)
-- otherwise "cabal test" will not run

-- module Tests where


import ParserTests.BConst
import ParserTests.Lambda
import ParserTests.If
import ParserTests.PatternMatchCase
import ParserTests.Nat
import ParserTests.DataTypes
import ParserTests.Subst
import ParserTests.SigmaTypes
import ParserTests.Pcase
import ParserTests.Contra
import ParserTests.ErasedApp
import ParserTests.ImpProd
import ParserTests.Decls
import ParserTests.Telescope



import Pire.Syntax.Ws
import Pire.Syntax.Eps
import Pire.Syntax.Nm
import Pire.Syntax.Token
import Pire.Syntax.Binder
import Pire.Syntax


import Pire.NoPos
import Pire.Parser.Basic
import Pire.Parser.Token
import Pire.Parser.VarWildcard
import Pire.Parser.Expr
import Pire.Forget
import Pire.Untie
import Pire.Parser.ParseUtils
import Pire.Parser.PiParseUtils




#ifdef PiForallInstalled

import qualified PiForall.Parser as P

#endif





import Test.Tasty

-- import Test.Tasty.SmallCheck as SC
-- import qualified Test.Tasty.QuickCheck as QC


import Test.Tasty.HUnit

-- import qualified Test.Tasty.Runners as R
-- import Test.Tasty.Options as O




import System.Environment as Env

import Data.Either.Combinators (fromRight')


import Bound
-- import Bound.Name





main = defaultMain tests




main' pat = do
  withArgs ["-p", pat] $ defaultMain $ tests





tests :: TestTree
tests = testGroup "Tests" [basicsU

                          , impOrExpVarU
                          , wildcardU

                          , varOrConU
                          , trustmeU
                          , reflU
                          , typenU
                          , bconstU

                          , ifU

                          , lambdaU
                          , letU
                          , expProdOrAnnotOrParensU
                          , tyEqU
                          , piU
                          , varU
                          , appU
                          , argU
                          , dconappU

                            -- TODO
                          , patMatchCaseU

                          , natU
                          , telescopesU
                          , dataTypesU


                          , substU

                            -- new as of May 2015
                          , parsingSigmaTypesU
                          , parsingPcaseU
                          , parsingContraU
                          , parsingErasedAppU

                            
                          , parsingImpProdU
                          , parsingDeclsU


                          ]






-- "the ? is towards the actual"
-- actual @?= expected = assertEqual "" expected actual
-- expected @=? actual = assertEqual "" expected actual


-- main' "basics"


basicsU = testGroup "parsing basics - unit tests" $ tail
  [
    undefined



  , let s = "wow this rocks "
    in
     testGroup ("parsing '"++s++"'") $ tail [

       undefined

       , testCase ("parse ide '"++s++"'")
         $ parse ide s  @?=  "wow"

       , testCase ("parse ide_ '"++s++"'")
         $ parse id_ s  @?=  ("wow",Ws " ")



       , testCase ("parse var '"++s++"'")
         $ parse var s @?=  V "wow"



       , testCase ("parse var_ '"++s++"'")
         -- $ (parse var_ s) @?= (V_ "wow" (Ws " "))
         $ (parse var_ s) @?= (Ws_ (V "wow") (Ws " "))



       , testCase ("parse & forget var_ '"++s++"'")
         $ (forget $ parse var_ s) @?= parse var s


       , testCase ("parse & forget var2_ '"++s++"'")
         $ parse var2_ s @?= ("wow", Ws " ")


       ]



  , let s =   "Succ "
    in
     testGroup ("parsing '"++s++"'") $ tail [

       undefined

       -- but vars deserve some attention - when using constructors (in the prelude)


       , testCase ("fail parsing var '"++s++"'")
         $ failParsingP var  s @?=  "fail"


       , testCase ("fail parsing var2_ '"++s++"'")
         $ failParsingP var2_   s @?=  "fail"




       ]



  , let s =    "Nat "
    in
     testGroup ("parsing '"++s++"'") $ tail [

       undefined


       , testCase ("fail parsing var_ '"++s++"'")
         $ failParsingP var_       s  @?=  "fail"



       ]




  , let s = "in{-foo-}this rocks "
    in
     testGroup ("parsing '"++s++"'") $ tail [

       undefined

       , testCase ("parse reserved 'in' in '"++s++"'")
         $ parse (reserved "in") s  @?=  ()


       , testCase ("parse reserved_ 'in' in '"++s++"'")
         $ parse (reserved_ "in") s  @?=  Ws "{-foo-}"


       ]


  , let s = "foo{-bar-}"
    in
     testGroup ("parsing '"++s++"'") $ tail [

       undefined

       -- but no matter really if "in" or "foo"
       , testCase ("parse reserved 'foo' in '"++s++"'")
         $ parse (reserved "foo") s  @?=  ()


       , testCase ("parse reserved_ 'foo' in '"++s++"'")
         $ parse (reserved_ "foo") s @?=  Ws "{-bar-}"


       ]




  , let s =  "bar{-baz-}this rocks "
    in
     testGroup ("parsing '"++s++"'") $ tail [

       undefined

       -- want parsing failure here (but assert equal)!

       , testCase ("fail parsing of reserved 'foo' in '"++s++"'")
         $ failParsing (reserved "foo") s @?= "fail"



         -- want parsing failure here (but assert equal)!

       , testCase ("fail parsing of reserved_ 'foo' in '"++s++"'")
         $ failParsing (reserved "foo") s @?= "fail"


       ]


  , let s = "+{-foo-}this rocks "
    in
     testGroup ("parsing '"++s++"'") $ tail [

       undefined


       , testCase "parsing reservedOp '+' "
         $ parse (reservedOp "+") s @?= ()


       , testCase "parsing reservedOp_ '+' " $
         parse (reservedOp_ "+") s @?= Ws "{-foo-}"


       ]


  , let s = "+4  "
    in
     testGroup ("parsing '"++s++"'") $ tail [

       undefined

       , testCase ("parsing reservedOp '+' in '"++s++"'")
         $ parse (reservedOp "+") s  @?=  ()


       , testCase ("parsing reservedOp_ '+' in '"++s++"'")
         $ parse (reservedOp_ "+") s   @?=  Ws ""



       ]



  , let s = "++  "
    in
     testGroup ("parsing '"++s++"'") $ tail [

       undefined

       , testCase ("fail parsing reservedOp '+' in  '"++s++"'")
         $ failParsing (reservedOp "+") s  @?=  "fail"

       , testCase ("fail parsing reservedOp_ '+' in  '"++s++"'")
         $ failParsing (reservedOp_ "+") "  ++  "   @?=  "fail"


       ]




  , let s = "+ +  "
    in
     testGroup ("parsing '"++s++"'") $ tail [

       undefined

       , testCase ("parsing reservedOp '+' in  '"++s++"'")
         $ parse (reservedOp "+") s  @?=  ()


       , testCase ("parsing reservedOp_ '+' in  '"++s++"'")
         $ parse (reservedOp_ "+") s  @?=  Ws " "


       ]




  , let s = "foo  this rocks "
    in
     testGroup ("parsing '"++s++"'") $ tail [

       undefined

       -- strangely enough

       , testCase ("parsing reservedOp 'foo' in '"++s++"'")
         $ parse (reservedOp "foo") s   @?=  ()


         , testCase ("parsing reservedOp_ 'foo' in '"++s++"'")
           $ parse (reservedOp_ "foo") s @?=  Ws "  "


       ]

  ]




-- exprs and helpers
-- ! todo: split this into more manageable chunks


-- main' "impOrExpVar"

impOrExpVarU = testGroup "parsing impOrExpVar - unit tests" $ tail
  [
    undefined


  , let s =  "foo{-bar-}this rocks "
    in
     testGroup ("parsing '"++s++"'") $ tail [

       undefined


       -- helper
       , testCase "parse as impOrExpVar"
         $ parse impOrExpVar s  @?=  (V "foo",RuntimeP)




       , testCase "parse as impOrExpVar_"
         -- $ (parse impOrExpVar_ s)  @?=  (V_ "foo" (Ws "{-bar-}"),RuntimeP)
         $ (parse impOrExpVar_ s)  @?=  (Ws_ (V "foo") $ Ws "{-bar-}",RuntimeP)
         



         -- , testCase "parse & forget impOrExpVar_"
       , testCase ("parse & forget impOrExpVar_ '"++s++"'")
         $ (forget $ parse impOrExpVar_ s) @?= (parse impOrExpVar s)



#ifdef PiForallInstalled

-- untie needs PiForall (other stuff can be tested w/ pure Pire wo/ Pi-forall ie.)


  , testCase ("parse & untie impOrExpVar_ '"++s++"'")
           $ (untie $ parse impOrExpVar_ s) @?= (piParse P.impOrExpVar s)

#endif




       ]


  , let s =     "[ foo ]{-bar-}this rocks "
    in
     testGroup ("parsing '"++s++"'") $ tail [

       undefined


       , testCase "parse as impOrExpVar"
         $ parse impOrExpVar s @?=  (V "foo",ErasedP)
                                       

       , testCase ("parse & forget impOrExpVar_ '"++s++"'")
         $ (forget $ parse impOrExpVar_ s) @?= (parse impOrExpVar s)




#ifdef PiForallInstalled


  , testCase ("parse & untie impOrExpVar_ '"++s++"'")
         $ (untie $ parse impOrExpVar_ s) @?= (piParse P.impOrExpVar s)



#endif





       ]



     -- slightly more complicated
  , let s =      "[{-foo-}y{-bar-}]{-baz-}x "
    in
     testGroup ("slightly more complicated: '"++s++"'") $ tail [

       undefined



       , testCase "parse as impOrExpVar"
         $ parse impOrExpVar s  @?=  (V "y",ErasedP)
         


         -- now this is interesting for impOrExpVar_
       , testCase "parsing as impOrExpVar_"
         $ parse impOrExpVar_ s
         @?= (Brackets_
               (BracketOpen "[" (Ws "{-foo-}"))
               -- (V_ "y" $ Ws "{-bar-}")
               (Ws_ (V "y") $ Ws "{-bar-}")
               (BracketClose "]" (Ws "{-baz-}")),
               ErasedP)



         -- ; testCase ("parse & forget impOrExpVar_ '"++s++"'")
       ,  testCase ("parse & forget impOrExpVar_")
          $ (forget $ parse impOrExpVar_ s) @?= parse impOrExpVar s




#ifdef PiForallInstalled




  , testCase ("parse & untie impOrExpVar_ '"++s++"'")
         $ (untie $ parse impOrExpVar_ s) @?= (piParse P.impOrExpVar s)




#endif






       ]



     -- should test the helpers as well maybe
     -- maybe in an extra group helpersU

  , let s =       "[{-foo-}y] x "
    in
     testGroup ("test some helpers: bracketOpen_ etc.: '"++s++"'") $ tail [

       undefined

       -- should test the helpers as well maybe

       , testCase "parse as bracketOpen_"
         $ parse bracketOpen_    s @?=  BracketOpen "[" (Ws "{-foo-}")


         -- etc
         -- ! many more...

       ]





  , let s =  "foo{-bar-}this rocks "
    in
     testGroup
     -- ("...: '"++s++"'")
     "impOrExpVar' -- variation of the above that returns just some string"
     $ tail [

       undefined


       ,  testCase "parse as impOrExpVar'"
          $ parse impOrExpVar'  s   @?=  ("foo",RuntimeP)


       ]




  , let s = "[ foo ]{-bar-}this rocks "
    in
     testGroup ("same erased: '"++s++"'") $ tail [

       undefined


       , testCase "parse as impOrExpVar'"
         $ parse impOrExpVar' s  @?=  ("foo",ErasedP)


       ]



  , let s =     "[{-foo-}y{-bar-}]{-baz-}x "
    in
     testGroup ("... and the slightly more complicated: '"++s++"'") $ tail [

       undefined


       , testCase "parse as impOrExpVar'"
         $ parse impOrExpVar'   s  @?=  ("y",ErasedP)

       ]




  ]



-- test them w/
-- main' "wildcard -"

wildcardU = testGroup ("parsing wildcard - unit tests") $ tail
  [

    undefined



  , let s =  "_{-foo-}x "
    in
     testGroup ("parsing '"++s++"'") $ tail [

       undefined


       -- wildcards


       , testCase ("parsing wildcard '"++s++"'")
         $ parse wildcard s  @?=  "_"

       , testCase ("parsing wildcard_ '"++s++"'")
         -- $ parse wildcard_ s @?=  (V_ "_" $ Ws "{-foo-}")
         $ parse wildcard_ s @?=  (Ws_ (V "_") $ Ws "{-foo-}")


       , testCase ("parse & forget & extract wildcard_ '"++s++"'")
         $ (extract $ forget $ parse wildcard_ s)
         @?= (parse wildcard s)


       , testCase ("parsing wildcard2_ '"++s++"'")
         $ parse wildcard2_ s  @?=  ("_", Ws "{-foo-}")


         -- dito for varOrWildcard
       , testCase ("parsing varOrWildcard '"++s++"'")
         $ parse varOrWildcard  s @?=  "_"


       , testCase ("parsing varOrWildcard_ '"++s++"'")
         -- $ parse varOrWildcard_  s  @?=  (V_ "_" $ Ws "{-foo-}")
         $ parse varOrWildcard_  s  @?=  (Ws_ (V "_") $ Ws "{-foo-}")
         

       , testCase ("parse, forget & extract varOrWildcard_ '"++s++"'")
         $ (extract $ forget $ parse varOrWildcard_ s) @?= (parse varOrWildcard s)

       , testCase ("parsing varOrWildcard2_ '"++s++"'")
        $ parse varOrWildcard2_  s   @?=  ("_", Ws "{-foo-}")


       ]




  , let s =    "a{-foo-}x "
    in
     testGroup ("parsing '"++s++"'") $ tail [

       undefined



       -- but varOrWildcard allows for vars as well of course


       , testCase ("parsing varOrWildcard '"++s++"'")
         $ parse varOrWildcard      s     @?=  "a"


       , testCase ("parsing varOrWildcard_ '"++s++"'")
         -- $ parse varOrWildcard_    s  @?= V_ "a" (Ws "{-foo-}")
         $ parse varOrWildcard_    s  @?= Ws_ (V "a") (Ws "{-foo-}")


       , testCase ("parse & forget varOrWildcard_ '"++s++"'")
         $ (extract $ forget $ parse varOrWildcard_ s) @?= (parse varOrWildcard s)


       , testCase ("parse  varOrWildcard2_ '"++s++"'")
         $ parse varOrWildcard2_   s  @?=  ("a", Ws "{-foo-}")



       ]




  , let s =    "Nat{-foo-}x "
    in
     testGroup ("mind constructor names though, parsing '"++s++"'") $ tail [

       undefined


       , testCase ("fail parsing varOrWildcard '"++s++"'")
         $ failParsingP varOrWildcard s @?=  "fail"


       ]



  , let s =    "Zero{-foo-}x "
    in
     testGroup ("mind constructor names, parsing '"++s++"'") $ tail [

       undefined

       , testCase ("fail parsing varOrWildcard '"++s++"'")
         $ failParsingP varOrWildcard s @?=  "fail"


       ]


  ]



-- test them w/
-- main' "varOrCon"

varOrConU = testGroup ("parsing varOrCon - unit tests"
                       ++"\n  "
                       ++"parse w/ prelude (parsing*P*S)"
                      ) $ tail
  [

    undefined


  , let s =    "bar{-baz-}x"
    in
     testGroup ("parsing '"++s++"'") $ tail [

       undefined

       -- varOrCon - parse w/ prelude (parsing*P*S)



       -- example originally also preceded by comment
       -- does not work Pi-forall's parser (and thus for parse & untie) however:
       -- "  {-foo-}bar{-baz-}x "



       , testCase "parse as varOrCon"
         $ parseP varOrCon s @?=  V "bar"
                                     

       , testCase "parse as varOrCon_"
         -- $ parseP varOrCon_ s    @?=  V_ "bar" (Ws "{-baz-}")
         $ parseP varOrCon_ s    @?=  Ws_ (V "bar") (Ws "{-baz-}")


       , testCase "parse & forget varOrCon_"
         $ (forget $ parseP varOrCon_ s) @?= parseP varOrCon s
                                                



#ifdef PiForallInstalled





  , testCase "parse & untie varOrCon"
         $ (untie $ parseP varOrCon s) @?= piParseP P.varOrCon s




         -- and thus:
       , testCase "parse & untie varOrCon_"
         $ (untie $ parseP varOrCon_ s) @?= piParseP P.varOrCon s




       -- and, well varOrCon yields an expr...

       , testCase "parse & untie expr_"
         $ (untie $ parseP expr_ s) @?= piParseP P.expr s




#endif






       ]





  , let s =    "Nat{-bar-}"
    in
     testGroup ("parsing '"++s++"'") $ tail [

       undefined


         , testCase "parse as varOrCon"
           $ parseP varOrCon s @?= TCon "Nat" []


         , testCase "parse as varOrCon_"
           $ parseP varOrCon_ s @?= TCon_ (Nm_ "Nat" $ Ws "{-bar-}") []
                                       
                                       



         -- ; testCase "parse as varOrCon_ & forget"
         , testCase ("parse & forget varOrCon_ '"++s++"'")
           $ (forget $ parseP varOrCon_ s) @?= parseP varOrCon s
                                                  



#ifdef PiForallInstalled



  -- ; testCase "parse as varOrCon & untie"
  , testCase ("parse & untie varOrCon '"++s++"'")
    $ (untie $ parseP varOrCon s) @?= piParseP P.varOrCon s



           -- and thus:
         , testCase "parse & untie varOrCon_"
           $ (untie $ parseP varOrCon_ s) @?= piParseP P.varOrCon s




         , testCase "parse & untie expr_"
           $ (untie $ parseP expr_ s) @?= piParseP P.expr s




#endif




         -- ! further, more complicated TCon examples


       ]



  , let s =   "Zero{-bar-}"
    in
     testGroup ("parsing '"++s++"'") $ tail [

       undefined


         , testCase "parse as varOrCon"
           $ parseP varOrCon    s @?=  DCon "Zero" [] (Annot Nothing)
                                          


         , testCase  "parse as varOrCon_"
           $ parseP varOrCon_ s
           @?= DCon_ (Nm1_ "Zero" $ Ws "{-bar-}") [] (Annot_ Nothing NoWs)

         , testCase "parse & forget varOrCon_"
           $ (forget $ parseP varOrCon_ s ) @?= parseP varOrCon s
                                                   


#ifdef PiForallInstalled



  , testCase "parse & untie varOrCon"
  $ (untie $ parseP varOrCon s) @?= piParseP P.varOrCon s


  , testCase "parse & untie varOrCon_"
    $ (untie $ parseP varOrCon_ s) @?= piParseP P.varOrCon s



   , testCase "parse & untie expr_"
  $ (untie $ parseP expr_ s) @?= piParseP P.expr s




#endif


       ]





  , let s =    "Succ{-bar-}x"
    in
     testGroup ("parsing '"++s++"'") $ tail [

       undefined


         , testCase "parse as varOrCon"
           $ parseP varOrCon s  @?=  DCon "Succ" [] (Annot Nothing)
                                        


         -- ; testCase ("parse varOrCon_ '"++s++"'")
         , testCase "parse as varOrCon_"
           $ parseP varOrCon_    s
           @?= DCon_ (Nm1_ "Succ" $ Ws "{-bar-}") [] (Annot_ Nothing $ NoWs)




         -- ; testCase "parse as varOrCon_ & forget"
         , testCase ("parse & forget varOrCon_ '"++s++"'")
           $ (forget $ parseP varOrCon_ s ) @?= parseP varOrCon s
                                                   



#ifdef PiForallInstalled



         , testCase "parse & untie varOrCon"
           $ (untie $ parseP varOrCon s) @?= piParseP P.varOrCon s



         , testCase "parse & untie varOrCon_"
           $ (untie $ parseP varOrCon_ s) @?= piParseP P.varOrCon s


         , testCase "parse & untie expr_"
           $ (untie $ parseP expr_ s) @?= piParseP P.expr s



#endif



       ]





  , let s = "\\ x . Nat"
    in
     testGroup (">>= for TCon: \""++s++"\"") $ tail [

         undefined



       --   make sure, the bind op for TCon/TCon_ is defined
       --   trivial equality

       , testCase ("parsing expr  '"++s++"'")
         $ (parseP expr s) @?= (parseP expr s)


       , testCase ("parsing expr_  '"++s++"'")
         $ (parseP expr_ s) @?= (parseP expr_ s)





#ifdef PiForallInstalled
#endif
     
       ]








  ]



-- test them w/
-- main' "trustme"

trustmeU = testGroup "trustme - unit tests" $ tail
  [
    undefined



  , let s =      "TRUSTME{-baz-}"
    in
     testGroup ("parsing '"++s++"'") $ tail [

       undefined


       , testCase ("parsing trustme '"++s++"'")
         $ parse trustme s @?= TrustMe (Annot Nothing)

       , testCase ("parsing trustme_ '"++s++"'")
         $ parse trustme_ s @?= TrustMe_ "TRUSTME" (Ws "{-baz-}") (Annot_ Nothing $ Ws "")



       , testCase ("parse & forget trustme_ '"++s++"'")
         $ (forget $ parse trustme_ s) @?= parse trustme s




#ifdef PiForallInstalled


  , testCase ("parse & untie trustme '"++s++"'")
         $ (untie $ parse trustme s) @?= piParse P.trustme s



       , testCase ("parse & untie trustme_ '"++s++"'")
         $ (untie $ parse trustme_ s) @?= (piParse P.trustme s)



       , testCase ("parse & untie expr_ '"++s++"'")
         $ (untie $ parse expr_ s) @?= (piParse P.expr s)



#endif



       ]



  , let s = "\\ x . TRUSTME"
    in
     testGroup (">>= for trustme: \""++s++"\"") $ tail [

         undefined

       --   make sure, the bind op for trustme is defined
       --   trivial equality

       , testCase ("parsing expr  '"++s++"'")
         $ (parse expr s) @?= (parse expr s)


       , testCase ("parsing expr_  '"++s++"'")
         $ (parse expr_ s) @?= (parse expr_ s)


       -- , testCase ("parse & forget expr_ '"++s++"'")
       --   $ (forget $ parse expr_ s) @?= (parse expr s)



#ifdef PiForallInstalled
#endif
     
       ]







  ]




-- main' "refl"

reflU = testGroup "parsing refl - unit tests" $ tail
  [
    undefined


  , let s =  "refl{-foo-}"
    in
     testGroup ("refl... w/ '"++s++"'") $ tail [

       undefined



#ifdef PiForallInstalled
#endif



       , testCase ("parse refl '"++s++"'")
         $ parse refl s  @?=  Refl (Annot Nothing)


       , testCase ("parse refl_ '"++s++"'")
         $ parse refl_ s @?=  Refl_ "refl" (Ws "{-foo-}") (Annot_ Nothing $ Ws "")



       , testCase ("parse & forget refl_ '"++s++"'")
         $ (forget $ parse refl_ s) @?= parse refl s



#ifdef PiForallInstalled


       , testCase ("parse & untie refl_ '"++s++"'")
         $ (untie $ parse refl_ s) @?= (piParse P.refl s)


         -- and as expr
         , testCase ("parse & untie expr '"++s++"'")
           $ (untie $ parse expr s) @?= (fromRight' $ P.parseExpr s)


       , testCase ("parse & untie expr_ '"++s++"'")
         $ (untie $ parse expr_ s) @?= (piParse P.expr s)



#endif




       ]



  , let s = "\\ x . refl"
    in
     testGroup (">>= for refl: \""++s++"\"") $ tail [

         undefined

       --   make sure, the bind op for trustme is defined
       --   trivial equality

       , testCase ("parsing expr  '"++s++"'")
         $ (parse expr s) @?= (parse expr s)


       , testCase ("parsing expr_  '"++s++"'")
         $ (parse expr_ s) @?= (parse expr_ s)


       -- , testCase ("parse & forget expr_ '"++s++"'")
       --   $ (forget $ parse expr_ s) @?= (parse expr s)



#ifdef PiForallInstalled
#endif
     
       ]






  ]


-- main' "typen"

typenU = testGroup "parsing typen - unit tests" $ tail
  [
    undefined

  , let s =    "Type{-foo-}"
    in
     testGroup ("parsing '"++s++"'") $ tail [

       undefined




       -- typen
       , testCase ("parse typen '"++s++"'")
         $ parse typen s @?=  Type

       , testCase ("parse typen_ '"++s++"'")
         $ parse typen_ s @?=  (Type_ "Type" (Ws "{-foo-}"))
         

       , testCase ("parse & forget typen_ '"++s++"'")
         $ (forget $ parse typen_ s) @?= parse typen s



#ifdef PiForallInstalled



       , testCase ("parse & untie typen_ '"++s++"'")
         $ (untie $ parse typen_ s) @?= piParse P.typen s


       , testCase ("parse & untie expr_ '"++s++"'")
         $ (untie $ parse expr_ s) @?= piParse P.expr s



       , testCase ("parse & untie expr '"++s++"'")
         $ (untie $ parse expr s) @?= (fromRight' $ P.parseExpr s)


#endif



       ]

  ]




-- bconstU



-- lambdaU...



-- main' "let"

letU = testGroup "parsing let - unit tests" $ tail
  [
    undefined



  , let s = "let{-l-}x{-l'-}={-b-}y{-b'-}in{-i-}i{-i'-}"
    in
     testGroup ("parsing '"++s++"'") $ tail [

       undefined


       -- let


       , testCase ("parsing letExpr  '"++s++"'")
         $ (nopos $ parse letExpr    s)
         @?= Let "x" (V "y") (Scope (V (F (V "i"))))


       , testCase ("parsing letExpr_  '"++s++"'")
         $ (nopos $ parse letExpr_ s)
         -- @?= Let_ (LetTok (Ws "{-l-}")) (Binder "x" (Ws "{-l'-}")) (Equal "=" $ Ws "{-b-}") (V_ "y" (Ws "{-b'-}")) (In "in" $ Ws "{-i-}") (Scope (V_ (F (V_ "i" (Ws ""))) (Ws "{-i'-}")))
         @?= Let_ (LetTok "let" (Ws "{-l-}")) (Binder_ "x" (Ws "{-l'-}")) (Equal "=" (Ws "{-b-}")) (Ws_ (V "y") (Ws "{-b'-}")) (In "in" (Ws "{-i-}")) (Scope (Ws_ (V (F (V "i"))) (Ws "{-i'-}")))

         


       , testCase ("parse & forget letExpr_ '"++s++"'")
         $ (forget $ parse letExpr_ s) @?= (parse letExpr s)


#ifdef PiForallInstalled



       , testCase ("parse & untie letExpr_ '"++s++"'")
         $ (untie $ parse letExpr_ s) @?= (piParse P.letExpr s)



       , testCase ("parse & untie expr_ '"++s++"'")
         $ (untie $ parse expr_ s) @?= (piParse P.expr s)


       , testCase ("parse & untie expr_ '"++s++"'")
         $ (untie $ parse expr_ s) @?= (fromRight' $ P.parseExpr s)


         , testCase ("parse & untie expr '"++s++"'")
           $ (untie $ parse expr s) @?= (fromRight' $ P.parseExpr s)



#endif









       ]







  , let s = "\\ x . let x = y in i "
    in
     testGroup (">>= for let: \""++s++"\"") $ tail [

         undefined



       --   make sure, the bind op for let is defined
       --   trivial equality

       , testCase ("parsing expr  '"++s++"'")
         $ (parse expr s) @?= (parse expr s)


       , testCase ("parsing expr_  '"++s++"'")
         $ (parse expr_ s) @?= (parse expr_ s)



       -- , testCase ("parse & forget expr_ '"++s++"'")
       --   $ (forget $ parse expr_ s) @?= (parse expr s)

         




#ifdef PiForallInstalled
#endif
     
       ]









     ]




-- main' "expProd"

expProdOrAnnotOrParensU = testGroup "parsing expProdOrAnnotOrParens - unit tests"
                          $ tail
  [
    undefined



  , let s =    "({-c-}A{-c'-}){-c''-}"
    in
     testGroup ("parsing '"++s++"'") $ tail [

       undefined


       -- expProdOrAnnotOrParens


       -- (A)  w/ some ws
       , testCase ("parsing expProdOrAnnotOrParens (Paren) '"++s++"'")
         $ (nopos $ parse expProdOrAnnotOrParens s)
         @?= Paren (V "A")


       , testCase ("parsing expProdOrAnnotOrParens_ (Paren_) '"++s++"'")
         $ (nopos $ parse expProdOrAnnotOrParens_ s)
         -- @?= Paren_ (ParenOpen "(" (Ws "{-c-}")) (V_ "A" (Ws "{-c'-}")) (ParenClose ")" (Ws "{-c''-}"))
         @?= Paren_ (ParenOpen "(" (Ws "{-c-}")) (Ws_ (V "A") (Ws "{-c'-}")) (ParenClose ")" (Ws "{-c''-}"))


       , testCase ("parse & forget expProdOrAnnotOrParens_ '"++s++"'")
         $ (forget $ parse expProdOrAnnotOrParens_ s)
         @?= (parse expProdOrAnnotOrParens s)


#ifdef PiForallInstalled


       , testCase ("parse & untie expProdOrAnnotOrParens_ '"++s++"'")
         $ (untie $ parse expProdOrAnnotOrParens_ s)
         @?= (piParse P.expProdOrAnnotOrParens s)


       , testCase ("parse & untie expr '"++s++"'")
         $ (untie $ parse expr s) @?= (fromRight' $ P.parseExpr s)


       , testCase ("parse & untie expr_ '"++s++"'")
         $ (untie $ parse expr_ s) @?= (fromRight' $ P.parseExpr s)


#endif




       ]




  , let s = "\\ x . ( y ) "
    in
     testGroup (">>= for Paren: \""++s++"\"") $ tail [

         undefined



       --   make sure, the bind op for Paren/Paren_ is defined
       --   trivial equality

       , testCase ("parsing expr  '"++s++"'")
         $ (parseP expr s) @?= (parseP expr s)


       , testCase ("parsing expr_  '"++s++"'")
         $ (parseP expr_ s) @?= (parseP expr_ s)





#ifdef PiForallInstalled
#endif
     
       ]









  , let s =  "(x: A)"
    in
     testGroup ("parsing '"++s++"'") $ tail [

       undefined


       -- (x: A)  w/ some ws


       , testCase ("parsing expProdOrAnnotOrParens,  Ann    '"++s++"'")
         $ (nopos $ parse expProdOrAnnotOrParens          s)
         @?= Ann (V "x") (V "A")

         -- ! maybe same w/ expProdOrAnnotOrParens_

       , testCase ("parse & forget expProdOrAnnotOrParens_ '"++s++"'")
         $ (forget $ parse expProdOrAnnotOrParens_ s)
         @?= (parse expProdOrAnnotOrParens s)


#ifdef PiForallInstalled



       , testCase ("parse & untie expProdOrAnnotOrParens_ '"++s++"'")
         $ (untie $ parse expProdOrAnnotOrParens_ s)
         @?= (piParse P.expProdOrAnnotOrParens s)


       , testCase ("parse & untie expr_ '"++s++"'")
         $ (untie $ parse expr_ s) @?= (fromRight' $ P.parseExpr s)



#endif







       ]



  , let s = "({-o-}x{-v-}:{-c-}A{-t-}){-c'-}"
    in
     testGroup ("parsing '"++s++"'") $ tail [

       undefined


       , testCase ("parsing expProdOrAnnotOrParens (Ann) '"++s++"'")
         $ (nopos $ parse expProdOrAnnotOrParens          s)
         @?= Ann (V "x") (V "A")

       , testCase ("parsing expProdOrAnnotOrParens_ (WitnessedAnn_) '"++s++"'")
         $ (nopos $ parse expProdOrAnnotOrParens_          s)
         -- @?= WitnessedAnnInParens_ (ParenOpen "(" (Ws "{-o-}")) (Ws_ (V "x") (Ws "{-v-}")) (Colon ":" (Ws "{-c-}")) (Ws_ (V "A") (Ws "{-t-}")) (ParenClose ")" (Ws "{-c'-}"))
         @?= (Ann_ $ Paren_ (ParenOpen "(" (Ws "{-o-}")) (WitnessedAnnEx_ (Ws_ (V "x") (Ws "{-v-}")) (Colon ":" (Ws "{-c-}")) (Ws_ (V "A") (Ws "{-t-}"))) (ParenClose ")" (Ws "{-c'-}")))


       , testCase ("parse & forget expProdOrAnnotOrParens_ (WitnessedAnn_) '"++s++"'")
         $ (forget $ parse expProdOrAnnotOrParens_ s)
         @?= (parse expProdOrAnnotOrParens s)




#ifdef PiForallInstalled



       , testCase ("parse & untie expProdOrAnnotOrParens_ '"++s++"'")
         $ (untie $ parse expProdOrAnnotOrParens_ s)
         @?= (piParse P.expProdOrAnnotOrParens s)


       , testCase ("parse & untie expr_ '"++s++"'")
         $ (untie $ parse expr_ s) @?= (fromRight' $ P.parseExpr s)



       , testCase ("parse & untie expr '"++s++"'")
          $ (untie $ parse expr s) @?= (fromRight' $ P.parseExpr s)


#endif





       ]




  , let s = "\\ y . ( x : A ) "
    in
     testGroup (">>= for Ann/WitnessedAnn_: \""++s++"\"") $ tail [

         undefined



       --   make sure, the bind op for Paren/Paren_ is defined
       --   trivial equality

       , testCase ("parsing expr  '"++s++"'")
         $ (parseP expr s) @?= (parseP expr s)


       , testCase ("parsing expr_  '"++s++"'")
         $ (parseP expr_ s) @?= (parseP expr_ s)





#ifdef PiForallInstalled
#endif
     
       ]



  , let s = "\\ y . ( x : A ) -> B "
    in
     testGroup (">>= for PiP RuntimeP / PiP_ w/ WitnessedAnnP_: \""++s++"\"") $ tail [

         undefined


       , testCase ("parsing expr  '"++s++"'")
         $ (parseP expr s) @?= (parseP expr s)


       , testCase ("parsing expr_  '"++s++"'")
         $ (parseP expr_ s) @?= (parseP expr_ s)





#ifdef PiForallInstalled
#endif
     
       ]



  , let s = "\\ y . [ x : A ] -> B "
    in
     testGroup (">>= for PiP ErasedP / PiP_ w/ WitnessedAnnInBracketsP_: \""++s++"\"") $ tail [

         undefined

       , testCase ("parsing expr  '"++s++"'")
         $ (parseP expr s) @?= (parseP expr s)


       , testCase ("parsing expr_  '"++s++"'")
         $ (parseP expr_ s) @?= (parseP expr_ s)



#ifdef PiForallInstalled
#endif
     
       ]











  , let s = "(A, B) "
    in
     testGroup ("parsing '"++s++"'") $ tail [

       undefined


       -- (A, B)  w/ some ws


       , testCase ("parsing expProdOrAnnotOrParens (Prod) '"++s++"'")
         $ (nopos $ parse expProdOrAnnotOrParens          s)
         @?= Prod (V "A") (V "B") (Annot Nothing)

       , testCase ("parse & forget expProdOrAnnotOrParens_ (Prod) '"++s++"'")
         $ (forget $ parse expProdOrAnnotOrParens_ s)
         @?= (parse expProdOrAnnotOrParens s)

#ifdef PiForallInstalled


       , testCase ("parse & untie expProdOrAnnotOrParens_ '"++s++"'")
         $ (untie $ parse expProdOrAnnotOrParens_ s)
         @?= (piParse P.expProdOrAnnotOrParens s)

       , testCase ("parse & untie expr_ '"++s++"'")
         $ (untie $ parse expr_ s) @?= (fromRight' $ P.parseExpr s)



#endif




       ]




  , let s = "\\ x .  (A, B) "
    in
     testGroup (">>= for Prod, parsing '"++s++"'") $ tail [

       undefined

        
       -- just make sure no exception occurrs, trivial equality


       , testCase ("parsing expr (lambda of Prod)  '"++s++"'")
         $ (parse expr s) @?= (parse expr s)


       , testCase ("parsing expr_  '"++s++"'")
         $ (parse expr_ s) @?= (parse expr_ s)





#ifdef PiForallInstalled


#endif




       ]













  , let s = "({-o-}A{-v-},{-c-}B{-t-}){-c'-}"
    in
     testGroup ("parsing '"++s++"'") $ tail [

       undefined


     , testCase ("parsing expProdOrAnnotOrParens (Prod) '"++s++"'")
       $ (nopos $ parse expProdOrAnnotOrParens s)
       @?= Prod (V "A") (V "B") (Annot Nothing)


     , testCase ("parsing expProdOrAnnotOrParens_ (Prod_) '"++s++"'")
        $ (nopos $ parse expProdOrAnnotOrParens_          s)
       -- @?= Prod_ (ParenOpen "(" (Ws "{-o-}")) (V_ "A" (Ws "{-v-}")) (Comma "," (Ws "{-c-}")) (V_ "B" (Ws "{-t-}")) (ParenClose ")" (Ws "{-c'-}")) (Annot_ Nothing (Ws ""))
        @?= Prod_ (ParenOpen "(" (Ws "{-o-}")) (Ws_ (V "A") (Ws "{-v-}")) (Comma "," (Ws "{-c-}")) (Ws_ (V "B") (Ws "{-t-}")) (ParenClose ")" (Ws "{-c'-}")) (Annot_ Nothing (Ws ""))



     , testCase ("parse & forget expProdOrAnnotOrParens_ (Prod_) '"++s++"'")
       $ (forget $ parse expProdOrAnnotOrParens_ s)
       @?= (parse expProdOrAnnotOrParens s)


#ifdef PiForallInstalled


     , testCase ("parse & untie expProdOrAnnotOrParens_ (Prod) '"++s++"'")
       $ (untie $ parse expProdOrAnnotOrParens_ s)
       @?= (piParse P.expProdOrAnnotOrParens s)


     , testCase ("parse & untie expr_ (Prod) '"++s++"'")
       $ (untie $ parse expr_ s) @?= (fromRight' $ P.parseExpr s)

     , testCase ("parse & untie expr '"++s++"'")
       $ (untie $ parse expr s) @?= (fromRight' $ P.parseExpr s)



#endif





       ]




  , let s = "(x: A) -> B "
    in
     testGroup ("parsing '"++s++"'") $ tail [

       undefined


       , testCase ("parsing expProdOrAnnotOrParens (PiP) \""++s++"\"")
         $ (nopos $ parse expProdOrAnnotOrParens          s)
         -- @?= Pi "x" (V "A") (Scope (V (F (V "B"))))
         @?= PiP RuntimeP "x" (V "A") (Scope (V (F (V "B"))))


       , testCase ("parse & forget expProdOrAnnotOrParens_ (PiP_) \""++s++"\"")
         $ (forget $ parse expProdOrAnnotOrParens_ s)
         @?= (parse expProdOrAnnotOrParens s)


#ifdef PiForallInstalled



       , testCase ("parse & untie expProdOrAnnotOrParens_ (PiP_) \""++s++"\"")
         $ (untie $ parse expProdOrAnnotOrParens_ s)
         @?= (piParse P.expProdOrAnnotOrParens s)


       , testCase ("parse & untie expr_ (PiP_) '"++s++"'")
         $ (untie $ parse expr_ s) @?= (fromRight' $ P.parseExpr s)


#endif








       ]




  , let s = "({-open-}x{-v-}:{-colon-}A{-ty-}){-close-}->{-arr-}B{-ty'-}"
    in
     testGroup ("parsing '"++s++"'") $ tail [

       undefined



       , testCase ("parsing expProdOrAnnotOrParens (PiP)   '"++s++"'")
         $ (nopos $ parse expProdOrAnnotOrParens          s)
         -- @?= Pi "x" (V "A") (Scope (V (F (V "B"))))
         @?= PiP RuntimeP "x" (V "A") (Scope (V (F (V "B"))))

       -- TODO
       -- , testCase ("parsing expProdOrAnnotOrParens_ (PiP_)  \""++s++"\"")
       --   $ (nopos $ parse expProdOrAnnotOrParens_          s)
       --   -- @?= PiP_ RuntimeP (WitnessedAnnInParensBnd_ (ParenOpen "(" (Ws "{-open-}")) (Binder "x" $ Ws "{-v-}") (Colon ":" (Ws "{-colon-}")) (V_ "A" (Ws "{-ty-}")) (ParenClose ")" (Ws "{-close-}"))) (Arrow (Ws "{-arr-}")) (Scope (V_ (F (V_ "B" (Ws ""))) (Ws "{-ty'-}")))
       --   @?= PiP_ RuntimeP (WitnessedAnnInParensBnd_ (ParenOpen "(" (Ws "{-open-}")) (Binder "x" $ Ws "{-v-}") (Colon ":" (Ws "{-colon-}")) (Ws_ (V "A") (Ws "{-ty-}")) (ParenClose ")" (Ws "{-close-}"))) (Arrow (Ws "{-arr-}")) (Scope (V_ (F (V_ "B" (Ws ""))) (Ws "{-ty'-}")))

       , testCase ("parse & forget expProdOrAnnotOrParens_ (PiP_) '"++s++"'")
         $ (forget $ parse expProdOrAnnotOrParens_ s) @?= (parse expProdOrAnnotOrParens s)



#ifdef PiForallInstalled



       , testCase ("parse & untie expProdOrAnnotOrParens_ (PiP_) '"++s++"'")
         $ (untie $ parse expProdOrAnnotOrParens_ s)
         @?= (piParse P.expProdOrAnnotOrParens s)


       , testCase ("parse & untie expr_ (PiP_) '"++s++"'")
         $ (untie $ parse expr_ s) @?= (fromRight' $ P.parseExpr s)



       , testCase ("parse & untie expr '"++s++"'")
         $ (untie $ parse expr s) @?= (fromRight' $ P.parseExpr s)



#endif








       ]


     -- ! ErasedPi (here?)

     ]






-- test w/
-- main' "TyEq"


tyEqU = testGroup "parsing TyEq - unit tests" $ tail
  [

    undefined



  , let s = "x=y=z"
    in
     testGroup ("parsing '"++s++"'") $ tail [

       undefined


       -- = (TyEq), left assoc


       , testCase ("parsing expr (left assoc '=') '"++s++"'")
         $ (nopos $ parse expr          s)
         @?= TyEq (TyEq (V "x") (V "y")) (V "z")


       , testCase ("parse & forget expr (left assoc '=') '"++s++"'")
         $ (forget $ parse expr_ s) @?= (parse expr s)



#ifdef PiForallInstalled



       , testCase ("parse & untie expr_ (left assoc '=') '"++s++"'")
         $ (untie $ parse expr_ s) @?= (piParse P.expr s)


     , testCase ("parse & untie expr_ (left assoc '=') '"++s++"'")
       $ (untie $ parse expr_ s) @?= (fromRight' $ P.parseExpr s)



#endif



       ]



  , let s = "x ={-eq-}y ={-eq'-}z"
    in
     testGroup ("parsing '"++s++"'") $ tail [

       undefined


       -- w/ some ws


       , testCase ("parsing expr (left assoc '=') '"++s++"'")
         $ (nopos $ parse expr          s)
         @?= TyEq (TyEq (V "x") (V "y")) (V "z")


       , testCase ("parsing expr_ (left assoc '=') '"++s++"'")
         $ (nopos $ parse expr_          s)
         -- @?= TyEq_ (TyEq_ (V_ "x" (Ws " ")) (Equal "=" (Ws "{-eq-}")) (V_ "y" (Ws " "))) (Equal "=" (Ws "{-eq'-}")) (V_ "z" (Ws ""))
         @?= TyEq_ (TyEq_ (Ws_ (V "x") (Ws " ")) (Equal "=" (Ws "{-eq-}")) (Ws_ (V "y") (Ws " "))) (Equal "=" (Ws "{-eq'-}")) (Ws_ (V "z") (Ws ""))

       , testCase ("parse & forget expr_ (left assoc '=') '"++s++"'")
         $ (forget $ parse expr_ s) @?= (parse expr s)


#ifdef PiForallInstalled




       , testCase ("parse & untie expr_ (left assoc '=') '"++s++"'")
         $ (untie $ parse expr_ s) @?= (piParse P.expr s)



     , testCase ("parse & untie expr '"++s++"'")
       $ (untie $ parse expr s) @?= (fromRight' $ P.parseExpr s)



#endif





       ]

     -- ! ErasedPi (here?)





  , let s = "\\ x . y = z"
    in
     testGroup (">>= for TyEq: \""++s++"\"") $ tail [

         undefined



       --   make sure, the bind op for TyEq is defined
       --   trivial equality

       , testCase ("parsing expr  '"++s++"'")
         $ (parse expr s) @?= (parse expr s)


       , testCase ("parsing expr_  '"++s++"'")
         $ (parse expr_ s) @?= (parse expr_ s)



       -- , testCase ("parse & forget expr_ '"++s++"'")
       --   $ (forget $ parse expr_ s) @?= (parse expr s)

         




#ifdef PiForallInstalled
#endif
     
       ]







  ]




-- test them w/
-- main' "Pi -"

piU = testGroup "Pi - unit tests" $ tail
  [

    undefined

  , let s = "A->B->C"
    in
     testGroup ("parsing '"++s++"'") $ tail [

       undefined


       -- similar: -> (Pi_), right assoc


       , testCase ("parsing expr (right assoc '->') '"++s++"'")
         $ (nopos $ parse expr s)
         @?= PiP RuntimeP "_" (V "A") (Scope (PiP RuntimeP "_1" (V (F (V "B"))) (Scope (V (F (V (F (V "C"))))))))


       , testCase ("parse & forget expr_ (right assoc '->') \""++s++"\"")
         $ (forget $ parse expr_ s) @?= (parse expr s)



#ifdef PiForallInstalled

  , testCase ("parse & untie expr_ (right assoc '->') '"++s++"'")
         $ (untie $ parse expr_ s) @?= (piParse P.expr s)



       , testCase ("parse & untie expr '"++s++"'")
         $ (untie $ parse expr s) @?= (fromRight' $ P.parseExpr s)

#endif




       ]




  , let s = "A->{-a-}B->{-a'-}C"
    in
     testGroup ("parsing '"++s++"'") $ tail [

       undefined


       -- w/ some ws



       , testCase ("parsing expr (right assoc '->') \""++s++"\"")
         $ (nopos $ parse expr          s)
         @?= PiP RuntimeP "_" (V "A") (Scope (PiP RuntimeP "_1" (V (F (V "B"))) (Scope (V (F (V (F (V "C"))))))))



         -- w/ some ws
         -- ignore the ParenOpen "(" etc ws, just the Arrow ws should be kept
         -- (besides ws after A, B, C - but not exercised here)

         --- TODO
       -- , testCase ("parsing expr_ (right assoc '->') '"++s++"'")
       --   $ (nopos $ parse expr_          s)
       --   @?= PiP_ RuntimeP (InferredAnnBnd_ (Binder "_" $ Ws "") (V_ "A" (Ws ""))) (Arrow (Ws "{-a-}")) (Scope (PiP_ RuntimeP (InferredAnnBnd_ (Binder "_1" $ Ws "") (V_ (F (V_ "B" (Ws ""))) (Ws ""))) (Arrow (Ws "{-a'-}")) (Scope (V_ (F (V_ (F (V_ "C" (Ws ""))) (Ws ""))) (Ws "")))))




       , testCase ("parse & forget expr_ '"++s++"'")
         $ (forget $ parse expr_ s) @?= (parse expr s)




#ifdef PiForallInstalled



         , testCase ("parse & untie expr_ '"++s++"'")
           $ (untie $ parse expr_ s) @?= (fromRight' $ P.parseExpr s)


       , testCase ("parse & untie expr '"++s++"'")
         $ (untie $ parse expr s) @?= (fromRight' $ P.parseExpr s)



#endif





       ]









     ]



-- main' "var -"


varU = testGroup "var - unit tests" $ tail
  [

    undefined



  , let s = "foo  "
    in
     testGroup ("parsing '"++s++"'") $ tail [

       undefined


       -- w/ some ws


       , testCase ("parsing expr (var) '"++s++"'")
         $ (nopos $ parse expr s)  @?=  V "foo"

         -- ! do the same w/ expr_ maybe


       , testCase ("parse & forget expr_ (var) '"++s++"'")
         $ (forget $ parse expr_ s) @?= (parse expr s)


#ifdef PiForallInstalled


       , testCase ("parse & untie expr_ '"++s++"'")
         $ (untie $ parse expr_ s) @?= (fromRight' $ P.parseExpr s)


#endif







       ]



  , let s = "foo{-c-}"
    in
     testGroup ("parsing '"++s++"'") $ tail [

       undefined



       , testCase ("parsing expr (var) '"++s++"'")
         $ (nopos $ parse expr s)  @?=  V  "foo"

         -- TODO
       -- , testCase ("parsing expr_ (var) '"++s++"'")
       --   $ (nopos $ parse expr_ "  foo{-c-}")  @?=  (V_ "foo" (Ws "{-c-}"))


       , testCase ("parse & forget expr_ (var) '"++s++"'")
         $ (forget $ parse expr_ s) @?= (parse expr s)




#ifdef PiForallInstalled


       , testCase ("parse & untie expr_ '"++s++"'")
         $ (untie $ parse expr_ s) @?= (fromRight' $ P.parseExpr s)


     , testCase ("parse & untie expr '"++s++"'")
       $ (untie $ parse expr s) @?= (fromRight' $ P.parseExpr s)


#endif


       ]







  ]


-- main' "@"

appU = testGroup ":@ (app) - unit tests" $ tail
  [

    undefined





  , let s = "f a  "
    in
     testGroup ("parsing '"++s++"'") $ tail [

       undefined



#ifdef PiForallInstalled



       , testCase ("parsing expr (app) '"++s++"'")
         $ (nopos $ parse expr s)  @?=  V "f" :@ V "a"


#endif





       ]



  , let s = "f{-c-}a{-c'-}"
    in
     testGroup ("parsing '"++s++"'") $ tail [

       undefined



       , testCase ("parsing expr (app) '"++s++"'")
         $ (nopos $ parse expr s)  @?=  V "f" :@ V "a"

        -- TODO
       -- , testCase ("parsing expr_ (app) '"++s++"'")
       --   $ (nopos $ parse expr_ "  f{-c-}a{-c'-}")
       --   @?=  (V_ "f" (Ws "{-c-}")) :@ (V_ "a" (Ws "{-c'-}"))



       , testCase ("parse & forget expr_ '"++s++"'")
          $ (forget $ parse expr_ s) @?= (parse expr s)



#ifdef PiForallInstalled



       , testCase ("parse & untie expr_ '"++s++"'")
         $ (untie $ parse expr_ s) @?= (fromRight' $ P.parseExpr s)

       , testCase ("parse & untie expr '"++s++"'")
          $ (untie $ parse expr s) @?= (fromRight' $ P.parseExpr s)


#endif






       ]






  , let s = "f g a  "
    in
     testGroup ("parsing '"++s++"'") $ tail [

       undefined


       -- experimenting with formatting here
       -- really waiting for ghc 7.8 to arrive in debian testing
       -- so I can use (Chris Done's) formatting



       , testCase ("parsing expr (app) '"++s++"'")
         $ (nopos $ parse expr s)  @?=  (V "f" :@ V "g") :@ V "a"



       , testCase ("parse & forget expr_ '"++s++"'")
          $ (forget $ parse expr_ s) @?= (parse expr s)



#ifdef PiForallInstalled



       , testCase ("parse & untie expr_ '"++s++"'")
         $ (untie $ parse expr_ s) @?= (fromRight' $ P.parseExpr s)


       , testCase ("parse & untie expr '"++s++"'")
         $ (untie $ parse expr s) @?= (fromRight' $ P.parseExpr s)



#endif







       ]


  ]



  -- arg(s), dconapp, funapp etc - parsing w/ prelude here (for dconapp)


  -- main' "arg -"

argU = testGroup "arg - unit tests" $ tail
  [

    undefined




    -- first thing to notice:
    -- not only can args be in brackets or not,
    -- but (possibly within those brackets) they can be more complex than just vars


  , let s =  "a{-c-}"
    in
     testGroup ("parsing '"++s++"'") $ tail [

       undefined


       , testCase ("parsing arg '"++s++"'")
         $ parseP arg s @?= Arg RuntimeP (V "a")

         -- TODO
       -- , testCase ("parsing arg_    '"++s++"'")
       --   $ parseP arg_ s @?= Arg RuntimeP (V_ "a" (Ws "{-c-}"))

       , testCase ("parse & forget arg_ '"++s++"'")
         $ (forget $ parseP arg_ s) @?= (parseP arg s)



#ifdef PiForallInstalled


       , testCase ("parse & untie arg '"++s++"'")
         $ (untie $ parseP arg s) @?= (piParseP P.arg s)


       , testCase ("parse & untie arg_ '"++s++"'")
         $ (untie $ parseP arg_ s) @?= (piParseP  P.arg s)

#endif







       ]




     -- here just f
     -- but can be eg. a lambda as well (!)

     -- [later:] rethink - maybe not that interesting
     -- (don't care about the a{-c'-} part ie.)
     -- but see how it is used if within brackets


  , let s = "f{-c-}a{-c'-}"
    in
     testGroup ("parsing '"++s++"'") $ tail [

       undefined


       , testCase ("parsing arg '"++s++"'")
         $ parseP arg s @?= Arg RuntimeP (V "f")

       -- TODO
       -- , testCase ("parsing arg_     '"++s++"'")
       --   $ parseP arg_ s @?= Arg RuntimeP (V_ "f" $ Ws "{-c-}")

       , testCase ("parse & forget arg_ '"++s++"'")
         $ (forget $ parseP arg_ s) @?= (parseP arg s)





#ifdef PiForallInstalled


       , testCase ("parse & untie arg_ '"++s++"'")
         $ (untie $ parseP arg_ s) @?= (piParseP  P.arg s)


#endif



       ]

     -- within brackets "f a" would be an app

  , let s = "[{-bo-}f{-c-}a{-c'-}]{-bc-}"
    in
     testGroup ("within brackets  'f a' would be an app") $ tail [

       undefined


       , testCase ("parsing arg     '"++s++"'")
         $ (nopos $ parseP arg          s) @?= Arg ErasedP (V "f" :@ V "a")

        -- TODO
        -- , testCase ("parsing arg_    '"++s++"'")
        --  $ (nopos $ parseP arg_          s)
        --  @?= Arg ErasedP (Brackets_ (BracketOpen "[" (Ws "{-bo-}")) (V_ "f" (Ws "{-c-}") :@ V_ "a" (Ws "{-c'-}")) (BracketClose "]" (Ws "{-bc-}")))


       , testCase ("parse & forget arg_ '"++s++"'")
         $ (forget $ parseP arg_ s) @?= (parseP arg s)


#ifdef PiForallInstalled


       , testCase ("parse & untie arg '"++s++"'")
         $ (untie $ parseP arg s) @?= (piParseP P.arg s)


       , testCase ("parse & untie arg_ '"++s++"'")
         $ (untie $ parseP arg_ s) @?= (piParseP  P.arg s)


#endif




       ]



  ]


-- main' "dconapp"

dconappU = testGroup "dconapp - unit tests" $ tail
  [

    undefined



     -- now a dconapp should collect the arg n as an DCon arg
     -- rather than as an app, as funapp would parse it
     -- if parsed w/ prelude ie.

  , let s = "Succ{-c-}n{-c'-}"
    in
     testGroup ("parsing (dconapp) '"++s++"'") $ tail [

       undefined


       , testCase ("parsing dconapp  '"++s++"'")
         $ parseP dconapp   s @?= DCon "Succ" [Arg RuntimeP (V "n")] (Annot Nothing)

       -- TODO
       -- , testCase ("parsing dconapp_  '"++s++"'")
       --   $ parseP dconapp_ s
       --   @?= DCon_ (Nm_ "Succ" $ Ws "{-c-}") [Arg RuntimeP (V_ "n" (Ws "{-c'-}"))] (Annot_ Nothing (Ws ""))

       -- TODO
     -- , testCase ("parsing expr_  '"++s++"'")
     --   $ (nopos $ parseP expr_ s)
     --   @?= DCon_ (Nm_ "Succ" $ Ws "{-c-}") [Arg RuntimeP (V_ "n" (Ws "{-c'-}"))] (Annot_ Nothing (Ws ""))


         -- and finally an exp should itself parse Succ n as an dconapp
         -- rather than as a funapp


       ,  testCase ("parsing expr (DCon) '"++s++"'")
          $ (nopos $ parseP expr s)
          @?= DCon "Succ" [Arg RuntimeP (V "n")] (Annot Nothing)


       , testCase ("parse & forget dconapp_ '"++s++"'")
         $ (forget $ parseP dconapp_ s) @?= (parseP dconapp s)



#ifdef PiForallInstalled


       , testCase ("parse & untie dconapp_ '"++s++"'")
         $ (untie $ parseP dconapp_ s) @?= (piParseP  P.dconapp s)


       , testCase ("parse & untie expr_ '"++s++"'")
         $ (untie $ parseP expr_ s) @?= (piParseP  P.expr s)



       , testCase ("parse & untie dconapp '"++s++"'")
         $ (untie $ parseP dconapp s) @?= (piParseP P.dconapp s)


       , testCase ("parse & untie expr '"++s++"'")
         $ (untie $ parseP expr s) @?= (piParseP P.expr s)



#endif






       ]




  ]



-- missing I guess: funapp unit tests - but covered by app (?)



