AlgorithmW.hs

module Hydra.Sources.Test.Inference.AlgorithmW (algorithmWTests) where

import Hydra.Kernel
import Hydra.Testing
import qualified Hydra.Dsl.Phantoms as Base
import qualified Hydra.Dsl.Core as Core
import Hydra.Dsl.Testing as Testing
import Hydra.Dsl.ShorthandTypes
import qualified Hydra.Dsl.Terms as Terms
import qualified Hydra.Dsl.Types as Types
import Hydra.Sources.Test.TestGraph
import Hydra.Dsl.TTerms as TTerms
import qualified Hydra.Dsl.TTypes as T
import Hydra.Sources.Test.Inference.Fundamentals

import qualified Data.Map as M
import Prelude hiding (map, sum)


algorithmWTests :: TTerm TestGroup
algorithmWTests = supergroup "Algorithm W test cases" [
  testGroupForSystemF]

-- @wisnesky's original Algorithm W test cases, modified so as to normalize type variables
testGroupForSystemF :: TTerm TestGroup
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_neg
    primSucc = primitive _math_neg