

{-# 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: sigma types
--------------------------------------------------------------------


module ParserTests.SigmaTypes where




import Test.Tasty
import Test.Tasty.HUnit


import Pire.Syntax
import Pire.NoPos
import Pire.Parser.ParseUtils
import Pire.Parser.PiParseUtils
import Pire.Parser.Expr
import Pire.Forget
import Pire.Untie




import Bound




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




-- sigma types, cf. beginning of test/Hw1.pi
-- new as of May 2015
-- test w/
-- main' "sigma"

parsingSigmaTypesU = testGroup "parsing sigma types - unit tests" $ tail [

  undefined

    
  , let s = "{ x : A | B }"
    in
      testGroup ("sigma type '"++s++"'") $ tail [

        undefined

        -- as a sigma type
        , testCase ("parsing sigmaTy  '"++s++"'")
          $ (nopos $ parse  sigmaTy s) @?= (Sigma "x" (V "A") (Scope (V (F (V "B")))))



          -- and as an expr as well, course
        , testCase ("parsing expr  '"++s++"'")
          $ (nopos $ parse  expr s) @?= (Sigma "x" (V "A") (Scope (V (F (V "B")))))


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

        ]

      
#ifdef PiForallInstalled

  ++ tail [

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

    ]
  
#endif


  , let s = "\\ y . { x : A | B }"
    in
      testGroup ("bind op for sigma type: \""++s++"\"") $ tail [

        undefined

        -- TODO seems silly, rethink
        
        , 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++"'")
          --   $ (parse expr s) @?= (parse expr s)
          
        ]


  , let s = "more stuff to come here... - more complicated: w/ whitespace etc"
    in
      testGroup ("sigma type '"++s++"'") $ tail [
        
        undefined

        
        ]


      -- indent!
      ]
