content: module Oden.Infer.SubsumptionSpec where
  
  import           Test.Hspec
  
  import           Oden.Infer.Subsumption
  import           Oden.SourceInfo
  import           Oden.Core.Expr
  import           Oden.Identifier
  import           Oden.Metadata
  import           Oden.Predefined
  import           Oden.Type.Polymorphic
  import           Oden.Pretty ()
  
  import           Oden.Assertions
  import           Oden.Infer.Fixtures
  
  spec :: Spec
  spec =
    describe "subsumedBy" $ do
  
      it "tvar is subsumed by same tvar" $
        scheme tvarA `subsumedBy` Literal (Metadata Predefined) Unit tvarA
        `shouldSucceedWith`
        (scheme tvarA, Literal (Metadata Predefined) Unit tvarA)
  
      it "tvar b is subsumed by tvar a and all a tvars are substituted" $
        scheme tvarB `subsumedBy` Literal (Metadata Predefined) Unit tvarA
        `shouldSucceedWith`
        (scheme tvarB, Literal (Metadata Predefined) Unit tvarB)
  
      it "int is subsumed by int" $
        scheme typeInt `subsumedBy` Literal (Metadata Predefined) (Int 1) typeInt
        `shouldSucceedWith`
        (scheme typeInt, Literal (Metadata Predefined) (Int 1) typeInt)
  
      it "string is subsumed by string" $
        scheme typeString `subsumedBy` Literal (Metadata Predefined) (String "foo") typeString
        `shouldSucceedWith`
        (scheme typeString, Literal (Metadata Predefined) (String "foo") typeString)
  
      it "string is not subsumed by int" $
        shouldFail (scheme typeString `subsumedBy` Literal (Metadata Predefined) (Int 1) typeInt)
  
      it "int is not subsumed by string" $
        shouldFail (scheme typeInt `subsumedBy` Literal (Metadata Predefined) (String "foo") typeString)
  
      it "TFn of TVars is subsumed by same TFn" $
        let expr tv = Fn (Metadata Predefined)
                      (NameBinding missing (Identifier "x"))
                      (Symbol missing (Identifier "x") tv) (typeFn tv tv) in
          scheme (typeFn tvarA tvarA) `subsumedBy` expr tvarB
          `shouldSucceedWith`
          (scheme (typeFn tvarA tvarA), expr tvarA)
  
      it "TFn of a tvars is not subsumed by TFn from string to int" $
        let expr = Fn (Metadata Predefined)
                      (NameBinding missing (Identifier "x"))
                      (Symbol missing (Identifier "x") tvarA) (typeFn tvarA tvarA)
        in shouldFail (scheme (typeFn typeString typeInt) `subsumedBy` expr)
  
      it "TVar is not subsumed by TFn" $
        let expr = Symbol missing (Identifier "x") (typeFn tvarB tvarB) in
          shouldFail (scheme tvarA `subsumedBy` expr)
  
      it "tuple of tvars is subsumed by tuple of same tvars" $
        let tupleType = (TTuple (Metadata Predefined) tvarA tvarA [])
            expr = Symbol missing (Identifier "x") tupleType in
          scheme tupleType `subsumedBy` expr
          `shouldSucceedWith`
          (scheme tupleType, expr)
  
      it "tvar slice is subsumed by same tvar slice" $
        let expr tv = Slice (Metadata Predefined) [Symbol missing (Identifier "x") tv] (typeSlice tv) in
          scheme (typeSlice tvarA) `subsumedBy` expr tvarA
          `shouldSucceedWith`
          (scheme (typeSlice tvarA), expr tvarA)
  
      it "TNamed TFn of TVars is subsumed by unnamed but equal TFn" $
        let expr tv = Fn (Metadata Predefined)
                      (NameBinding missing (Identifier "x"))
                      (Symbol missing (Identifier "x") tv) (typeFn tv tv) in
          scheme (named "MyFn" $ typeFn tvarA tvarA) `subsumedBy` expr tvarB
          `shouldSucceedWith`
          (scheme (named "MyFn" $ typeFn tvarA tvarA), expr tvarA)
  
      it "empty record is subsumed by empty record" $
        let expr = Symbol missing (Identifier "x") emptyRow in
          scheme emptyRow `subsumedBy` expr
          `shouldSucceedWith`
          (scheme emptyRow, expr)
  
      it "empty record is not subsumed by one field record" $
        let oneFieldRow = RExtension missing (Identifier "foo") typeInt emptyRow
            expr = Symbol missing (Identifier "x") oneFieldRow in
          scheme emptyRow `subsumedBy` expr
          `shouldFailWith`
          SubsumptionError Missing emptyRow oneFieldRow
  
      it "one field record is not subsumed by extended record" $
        let oneFieldRow = RExtension missing (Identifier "foo") typeInt emptyRow
            twoFieldRow = RExtension missing (Identifier "bar") typeString oneFieldRow
            expr = Symbol missing (Identifier "x") twoFieldRow in
          scheme oneFieldRow `subsumedBy` expr
          `shouldFailWith`
          SubsumptionError Missing oneFieldRow twoFieldRow
  
      it "two field record is not subsumed by one field record" $
        let oneFieldRow = RExtension missing (Identifier "foo") typeInt emptyRow
            twoFieldRow = RExtension missing (Identifier "bar") typeString oneFieldRow
            expr = Symbol missing (Identifier "x") oneFieldRow in
          scheme twoFieldRow `subsumedBy` expr
          `shouldFailWith`
          SubsumptionError Missing twoFieldRow oneFieldRow
  
      it "record with row variable is not subsumed by other row variable record" $
        let firstRow = RExtension missing (Identifier "foo") typeInt tvarA
            secondRow = RExtension missing (Identifier "foo") typeInt tvarB
            expr = Symbol missing (Identifier "x") secondRow in
          scheme firstRow `subsumedBy` expr
          `shouldFailWith`
          SubsumptionError Missing firstRow secondRow
  
      it "record with row variable is not subsumed by multi-field record" $
        let firstRow = RExtension missing (Identifier "foo") typeInt tvarA
            twoFieldRow = RExtension missing (Identifier "bar") typeString (RExtension missing (Identifier "foo") typeInt (REmpty missing))
            expr = Symbol missing (Identifier "x") twoFieldRow in
          scheme firstRow `subsumedBy` expr
          `shouldFailWith`
          SubsumptionError Missing firstRow twoFieldRow
  
      it "record with row variable is not subsumed by multi-field record with row variable" $
        let firstRow = RExtension missing (Identifier "foo") typeInt tvarA
            twoFieldRow = RExtension missing (Identifier "bar") typeString (RExtension missing (Identifier "foo") typeInt tvarB)
            expr = Symbol missing (Identifier "x") twoFieldRow in
          scheme firstRow `subsumedBy` expr
          `shouldFailWith`
          SubsumptionError Missing firstRow twoFieldRow
  
      it "{ foo: int | b } -> { foo: int | b } is subsumed by a -> a" $
        let row = RExtension missing (Identifier "bar") typeString (RExtension missing (Identifier "foo") typeInt tvarB)
            expr t = Symbol missing (Identifier "x") (TFn missing t t) in
          scheme (TFn missing row row) `subsumedBy` (expr tvarA)
          `shouldSucceedWith'`
          (scheme (TFn missing row row), expr row)
  
      it "{ foo: c | d } -> c is subsumed by a -> b" $
        let row = (RExtension missing (Identifier "foo") tvarC tvarD)
            expr d r = Symbol missing (Identifier "x") (TFn missing d r) in
          scheme (TFn missing row tvarC) `subsumedBy` (expr tvarA tvarB)
          `shouldSucceedWith'`
          (scheme (TFn missing row tvarC), expr row tvarC)
  