

-- #!/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, declartions in particular
--------------------------------------------------------------------


module ParserTests.Decls where


import Test.Tasty
import Test.Tasty.HUnit

import Pire.Syntax.Nm
import Pire.Syntax.Ws
import Pire.Syntax.Token
import Pire.Syntax.Telescope
import Pire.Syntax.Eps
import Pire.Syntax.Decl
import Pire.Syntax.Constructor
import Pire.Syntax

import Pire.NoPos
import Pire.Forget
import Pire.Untie

import Pire.Parser.ParseUtils
import Pire.Parser.PiParseUtils
import Pire.Parser.Decl
-- import Pire.Parser.DataType



#ifdef PiForallInstalled
import qualified PiForall.Parser as P
#endif





-- main' "decls"

parsingDeclsU = testGroup "parsing decls - unit tests" $ tail [

  undefined

  
  -- sigs
  , let s = "foo : bar"
    in
      testGroup ("sig '"++s++"'") $ tail [
        undefined


        , testCase ("parsing sigDef  '"++s++"'")
          $ (nopos $ parse sigDef s) @?= (Sig "foo" $ V "bar")


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

        ]

      
#ifdef PiForallInstalled
  
  ++ tail [

    undefined
    
    , testCase ("parse & untie sigDef '"++s++"'")
      $ (untie $ parse sigDef s) @?= (piParse P.sigDef s)
      
      
    , testCase ("parse & untie sigDef_ '"++s++"'")
      $ (untie $ parseP sigDef_ s) @?= (piParseP  P.sigDef s)
      
      
    , testCase ("parse & untie decl_ '"++s++"'")
      $ (untie $ parseP decl_ s) @?= (piParseP  P.decl s)
    ]
  
#endif
  



  , let s = "foo{-f-}:{-c-}bar{-b-}"
    in
      testGroup ("sig '"++s++"'") $ tail [

        undefined


        , testCase ("parsing sigDef  '"++s++"'")
          $ (nopos $ parse sigDef s) @?= (Sig "foo" $ V "bar")
          
        , testCase ("parsing sigDef_  '"++s++"'")
         $ (nopos $ parse sigDef_ s)
          -- @?= (Sig_ (Nm_ "foo" $ Ws "{-f-}") (Colon ":" $ Ws "{-c-}") $ V_ "bar" $ Ws "{-b-}")
          @?= (Sig_ (Nm1_ "foo" $ Ws "{-f-}") (Colon ":" $ Ws "{-c-}") $ Ws_ (V "bar") $ Ws "{-b-}")
              

       , testCase ("parse & forget sigDef_ '"++s++"'")
         $ (forget $ parseP sigDef_ s) @?= (parseP sigDef s)
         
       ]

            
#ifdef PiForallInstalled

  
  ++ tail [
    undefined

    , testCase ("parse & untie sigDef_ '"++s++"'")
      $ (untie $ parseP sigDef_ s) @?= (piParseP  P.sigDef s)
      
    , testCase ("parse & untie decl_ '"++s++"'")
      $ (untie $ parseP decl_ s) @?= (piParseP  P.decl s)
      
    ]

#endif








  -- vals

  -- , let s = "  foo = bar"
  --   in
  --    testCase ("parsing valDef  '"++s++"'")
  --    $ (nopos $ parse valDef s)
  --    @?= (Def "foo" $ V "bar")


  , let s = "foo = bar"
    in
      testGroup ("valDef '"++s++"'") $ tail [
        
        undefined


        , testCase ("parsing valDef  '"++s++"'")
          $ (nopos $ parse valDef s) @?= (Def "foo" $ V "bar")
          

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

        ]
          
#ifdef PiForallInstalled

  
  ++ tail [

    undefined


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


    , testCase ("parse & untie valDef_ '"++s++"'")
      $ (untie $ parseP valDef_ s) @?= (piParseP  P.valDef s)
    
    
    , testCase ("parse & untie decl_ '"++s++"'")
      $ (untie $ parseP decl_ s) @?= (piParseP  P.decl s)

    ]
    

#endif



  , let s = "foo{-f-}={-c-}bar{-b-}"
    in
     testGroup ("val '"++s++"'") $ tail [
       
       undefined
       

       , testCase ("parsing valDef  '"++s++"'")
         $ (nopos $ parse valDef s)
         @?= (Def "foo" $ V "bar")

       , testCase ("parsing valDef_  '"++s++"'")
         $ (nopos $ parse valDef_ s)
         -- @?= (Def_ (Nm_ "foo" $ Ws "{-f-}") (Equal $ Ws "{-c-}") $ V_ "bar" $ Ws "{-b-}")
         @?= (Def_ (Nm1_ "foo" $ Ws "{-f-}") (Equal "=" $ Ws "{-c-}") $ Ws_ (V "bar") $ Ws "{-b-}")
         

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

       ]
            
#ifdef PiForallInstalled
  
  ++ tail [

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

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

    ]
  
#endif



  -- dataDef


  {-
    for cut & paste in ghci / cabal repl

    let s = unlines ["data Nat : Type where","    Zero" ,"    Succ of (Nat)"]

   -}


  , let s = unlines $ tail [
          undefined
          , "data Nat : Type where"
          , "    Zero"
          , "    Succ of (Nat)"
          ]
        
        
    in
      testGroup ("dataDef '"++s++"'") $ tail [

        undefined


        , testCase ("parsing dataDef  '"++s++"'")
          $ (nopos $ parse dataDef s)
          @?= (Data "Nat" EmptyTele [ConstructorDef' "Zero" EmptyTele,ConstructorDef' "Succ" (Cons RuntimeP "_" (TCon "Nat" []) EmptyTele)])



        -- ,  testCase ("parsing dataDef_  '"++s++"'")
        --    $ (nopos $ parse dataDef_ s)
        --    @?= (Data_ (DataTok "data" $ Ws " ") (Nm_ "Nat" $ Ws " ") EmptyTele (Colon ":" (Ws " ")) (Type_ "Type" (Ws " ")) (Where "where" (Ws "\n    ")) Nothing [(ConstructorDef'_ (Nm_ "Zero" $ Ws "\n    ") Nothing EmptyTele,Nothing),(ConstructorDef'_ (Nm_ "Succ" $ Ws " ") (Just (Of "of" (Ws " "))) (ConsWildInParens_ RuntimeP (ParenOpen "(" (Ws "")) "_" (TCon_ (Nm_ "Nat" $ Ws "") []) (ParenClose ")" (Ws "\n")) EmptyTele),Nothing)] Nothing)


        -- ,  testCase ("parsing dataDef_  '"++s++"'")
        --    $ (nopos $ parse dataDef_ s)
        --    @?= (Data_ (DataTok "data" $ Ws " ") (Nm_ "Nat" $ Ws " ") EmptyTele (Colon ":" (Ws " ")) (Type_ "Type" (Ws " ")) (Where "where" (Ws "\n    ")) Nothing [(ConstructorDef'_ (Nm_ "Zero" $ Ws "\n    ") Nothing EmptyTele,Nothing),(ConstructorDef'_ (Nm_ "Succ" $ Ws " ") (Just (Of "of" (Ws " "))) (ConsWildInParens_ RuntimeP (ParenOpen "(" (Ws "")) (InvisibleBinder 0) (TCon_ (Nm_ "Nat" $ Ws "") []) (ParenClose ")" (Ws "\n")) EmptyTele),Nothing)] Nothing)


        ,  testCase ("parsing dataDef_  '"++s++"'")
           $ (nopos $ parse dataDef_ s)
           @?= (Data_ (DataTok "data" $ Ws " ") (Nm1_ "Nat" $ Ws " ") EmptyTele (Colon ":" (Ws " ")) (Type_ "Type" (Ws " ")) (Where "where" (Ws "\n    ")) Nothing [(ConstructorDef'_ (Nm1_ "Zero" $ Ws "\n    ") Nothing EmptyTele,Nothing),(ConstructorDef'_ (Nm1_ "Succ" $ Ws " ") (Just (Of "of" (Ws " "))) (ConsWildInParens_ RuntimeP (ParenOpen "(" (Ws "")) (InvisibleBinder 0) (TCon_ (Nm_ "Nat" $ Ws "") []) (ParenClose ")" (Ws "\n")) EmptyTele),Nothing)] Nothing)





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

        ]


            
#ifdef PiForallInstalled

  
  ++ tail [
    
    undefined

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


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


      -- need telescopes+constructor defs  first...

    , testCase ("parse & untie dataDef w/ nopos '"++s++"'")
      $ (nopos $ untie $ parse dataDef s) @?= (nopos $ piParse P.dataDef s)

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

#endif
  

  ]


