module ExprSpec where
import Test.Hspec

import Kernel.Name.Internal
import Kernel.Level.Internal
import Kernel.Expr.Internal

mkType = mkSort mkLevelOne

getFreeVarRangeSpec =
  let e1 = mkConstant (mkName ["c1"]) []
      e2 = mkApp e1 (mkVar 1)
      e3 = mkSort mkZero
      e4 = mkLambdaDefault e3 e2
      e5 = mkPiDefault e3 e4 in do
    describe "getFreeVarRange" $ do
      it "should be 0 for constants" $ do
        getFreeVarRange e1 `shouldBe` 0
      it "should be 1+vIdx for Vars inside Apps" $ do
        getFreeVarRange e2 `shouldBe` 2
      it "should be 0 for sorts" $ do
        getFreeVarRange e3 `shouldBe` 0
      it "should decrement for each lambda" $ do
        getFreeVarRange e4 `shouldBe` 1
      it "should decrement for each pi" $ do
        getFreeVarRange e5 `shouldBe` 0


exprHasLevelParamSpec =
  let lp1 = mkLevelParam (mkName ["l1"])
      gp1 = mkGlobalLevel (mkName ["g1"])
      level1 = mkIteratedSucc (mkIMax lp1 mkLevelTwo) 2
      level2 = mkIteratedSucc (mkMax (mkSucc mkZero) gp1) 3
      const1 = mkConstant (mkName ["c1"]) [level1]
      const2 = mkConstant (mkName ["c2"]) [level2]
      const12 = mkConstant (mkName ["c12"]) [level1,level2]
      e1 = mkLambdaDefault mkProp const1
      e2 = mkPiDefault const2 const2
      e12 = mkPiDefault const12 e2
      e3 = mkPiDefault (mkSort lp1) const2 in do
    describe "exprHasLevelParam" $ do
      it "should be True for constants with level params" $ do
        exprHasLevelParam e1 `shouldBe` True
      it "should be False for constants with no level params" $ do
        exprHasLevelParam e2 `shouldBe` False
      it "should be True for constants with some level params" $ do
        exprHasLevelParam e12 `shouldBe` True
      it "should be True if there is a sort with a level param" $ do
        exprHasLevelParam e3 `shouldBe` True

instantiateSpec :: Spec
instantiateSpec =
  let c1 = mkConstant (mkName ["c1"]) []
      c2 = mkConstant (mkName ["c2"]) []

      e1 = mkLambdaDefault (mkApp c1 c2) (mkVar 1)
      subst1 = mkApp (mkVar 10) mkType
      ret1 = instantiate e1 subst1
      expectedRet1 = mkLambdaDefault (mkApp c1 c2) (mkApp (mkVar 11) mkType)

      e2 = mkLambdaDefault mkType (mkAppSeq (mkVar 0) [mkVar 1,mkVar 2])
      subst2 = c1
      ret2 = instantiate e2 subst2
      expectedRet2 = mkLambdaDefault mkType (mkAppSeq (mkVar 0) [c1,mkVar 1])

      ret3 = instantiate ret2 c2
      expectedRet3 = mkLambdaDefault mkType (mkAppSeq (mkVar 0) [c1,c2])

      ret4 = instantiate (mkPiDefault (mkVar 3) (mkVar 4)) (mkVar 0)
      expectedRet4 = mkPiDefault (mkVar 2) (mkVar 3)
  in do
    describe "instantiate" $ do
      it "should lift free vars in subst" $ do
        ret1 `shouldBe` expectedRet1
      it "should lift free vars in subst" $ do
        ret2 `shouldBe` expectedRet2
      it "should lift free vars in subst" $ do
        ret3 `shouldBe` expectedRet3
      it "should decrement untouched free vars in e" $ do
        ret4 `shouldBe` expectedRet4

instantiateLevelParamsSpec :: Spec
instantiateLevelParamsSpec =
  let lp1 = mkLevelParam (mkName ["l1"])
      gp1 = mkGlobalLevel (mkName ["g1"])
      level1 = mkIteratedSucc (mkIMax lp1 mkLevelTwo) 2
      level2 = mkIteratedSucc (mkMax (mkSucc mkZero) gp1) 3
      const1 = mkConstant (mkName ["c1"]) [level1]
      const2 = mkConstant (mkName ["c2"]) [level2]
      const12 = mkConstant (mkName ["c12"]) [level1,level2]
      e1 = mkLambdaDefault mkProp const1
      e2 = mkPiDefault const2 const2
      e12 = mkPiDefault const12 e2
      e3 = mkPiDefault (mkSort lp1) const2 in do
    describe "instantiateLevelParams" $ do
      it "sanity test" $ do
        instantiateLevelParams e1 [mkName ["l1"]] [level2] `shouldBe`
          (mkLambdaDefault mkProp (mkConstant (mkName ["c1"]) [mkIteratedSucc (mkIMax level2 mkLevelTwo) 2]))
      it "should work even if subst contains the same level params" $ do
        instantiateLevelParams e1 [mkName ["l1"]] [level1] `shouldBe`
          (mkLambdaDefault mkProp (mkConstant (mkName ["c1"]) [mkIteratedSucc (mkIMax level1 mkLevelTwo) 2]))


appSeqSpec :: Spec
appSeqSpec =
  let cs = map (\s -> mkConstant (mkName [s]) []) ["c1","c2","c3","c4"]

      e = mkApp (mkApp (mkApp (cs!!0) (cs!!1)) (cs!!2)) (cs!!3)
      op = getOperator e
      args = getAppArgs e
      e' = mkAppSeq op args

      s = mkLambdaDefault mkProp (mkVar 2)
  in do
    describe "appSeq" $ do
      it "mkAppSeq (getOperator e) (getAppArgs e) should yield e" $ do
        e `shouldBe` e'
      it "getOperator e = e if e is not app" $ do
        (getOperator s) `shouldBe` s
      it "getAppArgs e = [] if e is not app" $ do
        (getAppArgs s) `shouldBe` []

innerBodyOfLambdaSpec :: Spec
innerBodyOfLambdaSpec =
  let c = mkConstant (mkName ["c"]) []
      e = mkLambdaDefault mkProp (mkLambdaDefault mkType c) in do
    describe "innerBodyOfLambda" $ do
      it "should return body of nested lambdas" $ do
        (innerBodyOfLambda e) `shouldBe` c
      it "should do nothing on constants" $ do
        (innerBodyOfLambda (innerBodyOfLambda e)) `shouldBe` (innerBodyOfLambda e)


spec :: Spec
spec = do
  getFreeVarRangeSpec
  exprHasLevelParamSpec
  instantiateSpec
  instantiateLevelParamsSpec
  appSeqSpec
  innerBodyOfLambdaSpec

module ExprSpec where
import Test.Hspec

import Kernel.Name.Internal
import Kernel.Level.Internal
import Kernel.Expr.Internal

mkType = mkSort mkLevelOne

getFreeVarRangeSpec =
  let e1 = mkConstant (mkName ["c1"]) []
      e2 = mkApp e1 (mkVar 1)
      e3 = mkSort mkZero
      e4 = mkLambdaDefault e3 e2
      e5 = mkPiDefault e3 e4 in do
    describe "getFreeVarRange" $ do
      it "should be 0 for constants" $ do
        getFreeVarRange e1 `shouldBe` 0
      it "should be 1+vIdx for Vars inside Apps" $ do
        getFreeVarRange e2 `shouldBe` 2
      it "should be 0 for sorts" $ do
        getFreeVarRange e3 `shouldBe` 0
      it "should decrement for each lambda" $ do
        getFreeVarRange e4 `shouldBe` 1
      it "should decrement for each pi" $ do
        getFreeVarRange e5 `shouldBe` 0


exprHasLevelParamSpec =
  let lp1 = mkLevelParam (mkName ["l1"])
      gp1 = mkGlobalLevel (mkName ["g1"])
      level1 = mkIteratedSucc (mkIMax lp1 mkLevelTwo) 2
      level2 = mkIteratedSucc (mkMax (mkSucc mkZero) gp1) 3
      const1 = mkConstant (mkName ["c1"]) [level1]
      const2 = mkConstant (mkName ["c2"]) [level2]
      const12 = mkConstant (mkName ["c12"]) [level1,level2]
      e1 = mkLambdaDefault mkProp const1
      e2 = mkPiDefault const2 const2
      e12 = mkPiDefault const12 e2
      e3 = mkPiDefault (mkSort lp1) const2 in do
    describe "exprHasLevelParam" $ do
      it "should be True for constants with level params" $ do
        exprHasLevelParam e1 `shouldBe` True
      it "should be False for constants with no level params" $ do
        exprHasLevelParam e2 `shouldBe` False
      it "should be True for constants with some level params" $ do
        exprHasLevelParam e12 `shouldBe` True
      it "should be True if there is a sort with a level param" $ do
        exprHasLevelParam e3 `shouldBe` True

instantiateSpec :: Spec
instantiateSpec =
  let c1 = mkConstant (mkName ["c1"]) []
      c2 = mkConstant (mkName ["c2"]) []

      e1 = mkLambdaDefault (mkApp c1 c2) (mkVar 1)
      subst1 = mkApp (mkVar 10) mkType
      ret1 = instantiate e1 subst1
      expectedRet1 = mkLambdaDefault (mkApp c1 c2) (mkApp (mkVar 11) mkType)

      e2 = mkLambdaDefault mkType (mkAppSeq (mkVar 0) [mkVar 1,mkVar 2])
      subst2 = c1
      ret2 = instantiate e2 subst2
      expectedRet2 = mkLambdaDefault mkType (mkAppSeq (mkVar 0) [c1,mkVar 1])

      ret3 = instantiate ret2 c2
      expectedRet3 = mkLambdaDefault mkType (mkAppSeq (mkVar 0) [c1,c2])

      ret4 = instantiate (mkPiDefault (mkVar 3) (mkVar 4)) (mkVar 0)
      expectedRet4 = mkPiDefault (mkVar 2) (mkVar 3)
  in do
    describe "instantiate" $ do
      it "should lift free vars in subst" $ do
        ret1 `shouldBe` expectedRet1
      it "should lift free vars in subst" $ do
        ret2 `shouldBe` expectedRet2
      it "should lift free vars in subst" $ do
        ret3 `shouldBe` expectedRet3
      it "should decrement untouched free vars in e" $ do
        ret4 `shouldBe` expectedRet4

instantiateLevelParamsSpec :: Spec
instantiateLevelParamsSpec =
  let lp1 = mkLevelParam (mkName ["l1"])
      gp1 = mkGlobalLevel (mkName ["g1"])
      level1 = mkIteratedSucc (mkIMax lp1 mkLevelTwo) 2
      level2 = mkIteratedSucc (mkMax (mkSucc mkZero) gp1) 3
      const1 = mkConstant (mkName ["c1"]) [level1]
      const2 = mkConstant (mkName ["c2"]) [level2]
      const12 = mkConstant (mkName ["c12"]) [level1,level2]
      e1 = mkLambdaDefault mkProp const1
      e2 = mkPiDefault const2 const2
      e12 = mkPiDefault const12 e2
      e3 = mkPiDefault (mkSort lp1) const2 in do
    describe "instantiateLevelParams" $ do
      it "sanity test" $ do
        instantiateLevelParams e1 [mkName ["l1"]] [level2] `shouldBe`
          (mkLambdaDefault mkProp (mkConstant (mkName ["c1"]) [mkIteratedSucc (mkIMax level2 mkLevelTwo) 2]))
      it "should work even if subst contains the same level params" $ do
        instantiateLevelParams e1 [mkName ["l1"]] [level1] `shouldBe`
          (mkLambdaDefault mkProp (mkConstant (mkName ["c1"]) [mkIteratedSucc (mkIMax level1 mkLevelTwo) 2]))


appSeqSpec :: Spec
appSeqSpec =
  let cs = map (\s -> mkConstant (mkName [s]) []) ["c1","c2","c3","c4"]

      e = mkApp (mkApp (mkApp (cs!!0) (cs!!1)) (cs!!2)) (cs!!3)
      op = getOperator e
      args = getAppArgs e
      e' = mkAppSeq op args

      s = mkLambdaDefault mkProp (mkVar 2)
  in do
    describe "appSeq" $ do
      it "mkAppSeq (getOperator e) (getAppArgs e) should yield e" $ do
        e `shouldBe` e'
      it "getOperator e = e if e is not app" $ do
        (getOperator s) `shouldBe` s
      it "getAppArgs e = [] if e is not app" $ do
        (getAppArgs s) `shouldBe` []

innerBodyOfLambdaSpec :: Spec
innerBodyOfLambdaSpec =
  let c = mkConstant (mkName ["c"]) []
      e = mkLambdaDefault mkProp (mkLambdaDefault mkType c) in do
    describe "innerBodyOfLambda" $ do
      it "should return body of nested lambdas" $ do
        (innerBodyOfLambda e) `shouldBe` c
      it "should do nothing on constants" $ do
        (innerBodyOfLambda (innerBodyOfLambda e)) `shouldBe` (innerBodyOfLambda e)


spec :: Spec
spec = do
  getFreeVarRangeSpec
  exprHasLevelParamSpec
  instantiateSpec
  instantiateLevelParamsSpec
  appSeqSpec
  innerBodyOfLambdaSpec
