AlgorithmW.hs

module Hydra.Sources.Test.Inference.AlgorithmW where

-- Standard imports for shallow DSL tests
import Hydra.Kernel
import Hydra.Dsl.Meta.Testing                 as Testing
import Hydra.Dsl.Meta.Terms                   as Terms
import Hydra.Sources.Kernel.Types.All
import qualified Hydra.Dsl.Meta.Core          as Core
import qualified Hydra.Dsl.Meta.Phantoms      as Phantoms
import qualified Hydra.Dsl.Meta.Types         as T
import qualified Hydra.Sources.Test.TestGraph as TestGraph
import qualified Hydra.Sources.Test.TestTerms as TestTerms
import qualified Hydra.Sources.Test.TestTypes as TestTypes
import qualified Data.List                    as L
import qualified Data.Map                     as M


ns :: Namespace
ns = Namespace "hydra.test.inference.algorithmW"

module_ :: Module
module_ = Module {
            moduleNamespace = ns,
            moduleDefinitions = definitions,
            moduleTermDependencies = [TestGraph.ns],
            moduleTypeDependencies = kernelTypesNamespaces,
            moduleDescription = (Just "Algorithm W inference tests")}
  where
    definitions = [
      Phantoms.toDefinition allTests,
      Phantoms.toDefinition testGroupForSystemF]

define :: String -> TTerm a -> TTermDefinition a
define = definitionInModule module_

allTests :: TTermDefinition TestGroup
allTests = define "allTests" $
  Phantoms.doc "Algorithm W test cases" $
  supergroup "Algorithm W test cases" [
    testGroupForSystemF]

-- @wisnesky's original Algorithm W test cases, modified so as to normalize type variables
testGroupForSystemF :: TTermDefinition TestGroup
testGroupForSystemF = define "testGroupForSystemF" $
  subgroup "STLC to System F" [

--  --Untyped input:
--  --	(\x. x)
--  --System F type:
--  -- 	(v0 -> v0)
    expectPoly 1 []
      (lambda "x" $ var "x")
      ["t0"] (T.functionMany [T.var "t0", T.var "t0"]),

--  --Untyped input:
--  --	letrecs foo = (\x. x)
--  --		in 42
--  --System F type:
--  -- 	Nat
    expectMono 2 []
      (lets [
        "foo" >: lambda "x" $ var "x"]
        $ int32 42)
      T.int32,

--  --Untyped input:
--  --	let f = (\x. x) in (f 0)
--  --System F type:
--  -- 	Nat
    expectMono 3 []
      (lets [
        "f" >: lambda "x" $ var "x"]
        $ var "f" @@ int32 0)
      T.int32,

--  --Untyped input:
--  --	let f = ((\x. x) 0) in f
--  --System F type:
--  -- 	Nat
    expectMono 4 []
      (lets [
        "f" >: (lambda "x" $ var "x") @@ int32 0]
        $ var "f")
      T.int32,

---- TODO
----testAdt3 = TestCase "testAdt3" $ Abs "z" $ ExprConst (Fold "List")
----  @@ Var "z"
----  @@ ExprConst (Con "Nil")
----  @@ ExprConst (Con "Cons")
----
----foldl :: TTerm ((b -> a -> b) -> b -> [a] -> b)
----cons :: TTerm (a -> [a] -> [a])
----
----[testAdt3]
----Untyped input:
----	(\z. (fold_List z Nil Cons))
----Type inferred by Hindley-Milner:
----	(List v6 -> List v6)
----
----System F translation:
----	(\z:List v6 . ((fold_List [List v6 ,v6]) z (Nil [v6]) (Cons [v6])))
----  H.it "testAdt3" $ expectPolytype
----    ()
----    [t0] (tFun t0 t0)
--
--  --Untyped input:
--  --	let sng = (\x. (cons x nil)) in sng
--  --System F type:
--  -- 	(v5 -> (List v5))
    expectPoly 5 []
      (lets [
        "sng" >: lambda "x" $ list [var "x"]]
        $ var "sng")
      ["t0"] (T.function (T.var "t0") (T.list $ T.var "t0")),

--  --Untyped input:
--  --	let sng = (\x. (cons x nil)) in (pair (sng 0) (sng alice))
--  --System F type:
--  -- 	((List Nat) * (List String))
    expectMono 6 []
      (lets [
        "sng" >: lambda "x" $ list [var "x"]]
        $ pair (var "sng" @@ int32 0) (var "sng" @@ string "alice"))
      (T.pair (T.list T.int32) (T.list T.string)),

--  --Untyped input:
--  --	letrecs + = (\x. (\y. (S (+ (P x) y))))
--  --		in (+ (S (S 0)) (S 0))
--  --System F type:
--  -- 	Nat
    expectMono 7 []
      (lets [
        "+" >: lambdas ["x", "y"] (primSucc @@ (var "+" @@ (primPred @@ var "x") @@ var "y"))]
        $ var "+" @@ (primSucc @@ (primSucc @@ int32 0)) @@ (primSucc @@ int32 0))
      T.int32,

--  --Untyped input:
--  --	letrecs f = (\x. (\y. (f 0 x)))
--  --		in f
--  --System F type:
--  -- 	(Nat -> (Nat -> v5))
    expectPoly 9 []
      (lets [
        "f" >: lambdas ["x", "y"] (var "f" @@ int32 0 @@ var "x")]
        $ var "f")
      ["t0"] (T.functionMany [T.int32, T.int32, T.var "t0"]),

----Untyped input:
----	letrec f = (\x. (\y. (f 0 x)))
----		g = (\xx. (\yy. (g 0 xx)))
----		in (pair f g)
----Type inferred by Hindley-Milner:
----	((Int32 -> (Int32 -> v12)) * (Int32 -> (Int32 -> v14)))
    expectPoly 10 []
      (lets [
        "f">: lambdas ["x", "y"] (var "f" @@ int32 0 @@ var "x"),
        "g">: lambda "xx" $ lambda "yy" (var "g" @@ int32 0 @@ var "xx")]
        $ pair (var "f") (var "g"))
      ["t0", "t1"] (T.pair
        (T.functionMany [T.int32, T.int32, T.var "t0"])
        (T.functionMany [T.int32, T.int32, T.var "t1"])),

    -- Note: in the following three test cases, the original Algorithm W implementation and the new inference
    --       implementation find slightly different results. This is a result of tradeoffs between stronger support
    --       for monomorphic recursion vs. stronger support for wide letrecs with polymorphism.
--  --Untyped input:
--  --	letrecs f = (\x. (\y. (g 0 x)))
--  --		g = (\u. (\v. (f v 0)))
--  --		in (pair f g)
--  --System F type:
--  -- 	((v12 -> (Nat -> v13)) * (Nat -> (v15 -> v16)))
    expectPoly 11 []
      (lets [
        "f">: lambda "x" $ lambda "y" (var "g" @@ int32 0 @@ var "x"),
        "g">: lambda "u" $ lambda "v" (var "f" @@ var "v" @@ int32 0)]
        $ pair (var "f") (var "g"))
      ["t0", "t1", "t2", "t3"] (T.pair
        (T.functionMany [T.var "t0", T.int32, T.var "t1"])
        (T.functionMany [T.int32, T.var "t2", T.var "t3"])),

--  --Untyped input:
--  --	letrecs f = (\x. (\y. (g 0 0)))
--  --		g = (\u. (\v. (f v 0)))
--  --		in (pair f g)
--  --System F type:
--  -- 	((Nat -> (Nat -> v12)) * (Nat -> (Nat -> v14)))
    expectPoly 12 []
      (lets [
        "f">: lambda "x" $ lambda "y" (var "g" @@ int32 0 @@ int32 0),
        "g">: lambda "u" $ lambda "v" (var "f" @@ var "v" @@ int32 0)]
        $ pair (var "f") (var "g"))
      ["t0", "t1"] (T.pair
        (T.functionMany [T.int32, T.int32, T.var "t0"])
        (T.functionMany [T.int32, T.int32, T.var "t1"])),

--  --Untyped input:
--  --	letrecs f = (\x. (\y. (g 0 x)))
--  --		g = (\u. (\v. (f 0 0)))
--  --		in (pair f g)
--  --System F type:
--  -- 	((Nat -> (Nat -> v12)) * (Nat -> (Nat -> v14)))
    expectPoly 13 []
      (lets [
        "f">: lambda "x" $ lambda "y" (var "g" @@ int32 0 @@ var "x"),
        "g">: lambda "u" $ lambda "v" (var "f" @@ int32 0 @@ int32 0)]
        $ pair (var "f") (var "g"))
      ["t0", "t1"] (T.pair
        (T.functionMany [T.int32, T.int32, T.var "t0"])
        (T.functionMany [T.int32, T.int32, T.var "t1"]))]
  where
    -- Placeholders for the primitives in @wisnesky's test cases; they are not necessarily the same functions,
    -- but they have the same types.
    primPred = primitive _math_negate
    primSucc = primitive _math_negate