diff --git a/src/runtime/haskell/pgf2.cabal b/src/runtime/haskell/pgf2.cabal index 6be68584f..79995e0c2 100644 --- a/src/runtime/haskell/pgf2.cabal +++ b/src/runtime/haskell/pgf2.cabal @@ -64,3 +64,13 @@ test-suite transactions HUnit >= 1.6.1.0, containers, pgf2 + +test-suite linearization + type: exitcode-stdio-1.0 + main-is: tests/linearization.hs + default-language: Haskell2010 + build-depends: + base, + HUnit >= 1.6.1.0, + containers, + pgf2 diff --git a/src/runtime/haskell/tests/basic.gf b/src/runtime/haskell/tests/basic.gf index 84b6efe80..229fa320d 100644 --- a/src/runtime/haskell/tests/basic.gf +++ b/src/runtime/haskell/tests/basic.gf @@ -8,6 +8,11 @@ data z : N ; data c : N -> S ; cat P N ; +fun nat : (x : N) -> P x ; fun ind : P z -> ((x:N) -> P x -> P (s x)) -> ((x : N) -> P x) ; +fun intLit : Int -> S; +fun stringLit : String -> S; +fun floatLit : Float -> S; + } diff --git a/src/runtime/haskell/tests/basic.hs b/src/runtime/haskell/tests/basic.hs index 257aa54b6..b790103ce 100644 --- a/src/runtime/haskell/tests/basic.hs +++ b/src/runtime/haskell/tests/basic.hs @@ -15,9 +15,9 @@ main = do grammarTests gr = [TestCase (assertEqual "abstract names" "basic" (abstractName gr)) ,TestCase (assertEqual "abstract categories" ["Float","Int","N","P","S","String"] (categories gr)) - ,TestCase (assertEqual "abstract functions" ["c","ind","s","z"] (functions gr)) + ,TestCase (assertEqual "abstract functions" ["c","floatLit","ind","intLit","nat","s","stringLit","z"] (functions gr)) ,TestCase (assertEqual "abstract functions by cat 1" ["s","z"] (functionsByCat gr "N")) - ,TestCase (assertEqual "abstract functions by cat 2" ["c"] (functionsByCat gr "S")) + ,TestCase (assertEqual "abstract functions by cat 2" ["c","floatLit","intLit","stringLit"] (functionsByCat gr "S")) ,TestCase (assertEqual "abstract functions by cat 2" [] (functionsByCat gr "X")) -- no such category ,TestCase (assertBool "type of z" (eqJust (readType "N") (functionType gr "z"))) ,TestCase (assertBool "type of s" (eqJust (readType "N->N") (functionType gr "s"))) diff --git a/src/runtime/haskell/tests/basic.pgf b/src/runtime/haskell/tests/basic.pgf index 88c7627cc..e3e5795f9 100644 Binary files a/src/runtime/haskell/tests/basic.pgf and b/src/runtime/haskell/tests/basic.pgf differ diff --git a/src/runtime/haskell/tests/basic.pmcfg b/src/runtime/haskell/tests/basic.pmcfg index c0077b8a0..705cef3d9 100644 --- a/src/runtime/haskell/tests/basic.pmcfg +++ b/src/runtime/haskell/tests/basic.pmcfg @@ -5,12 +5,34 @@ abstract basic { cat P N ; -- 0.693147 cat S ; -- 0.693147 cat String ; -- 0.693147 - data c : N -> S ; -- -0 - fun ind : P z -> ((x : N) -> P x -> P (s x)) -> (x : N) -> P x ; -- -0 + data c : N -> S ; -- 1.38629 + fun floatLit : Float -> S ; -- 1.38629 + fun ind : P z -> ((x : N) -> P x -> P (s x)) -> (x : N) -> P x ; -- 0.693147 + fun intLit : Int -> S ; -- 1.38629 + fun nat : (x : N) -> P x ; -- 0.693147 data s : N -> N ; -- 0.693147 + fun stringLit : String -> S ; -- 1.38629 data z : N ; -- 0.693147 } concrete basic_cnc { + lincat Float = [ + "s" + ] + lindef Float : String(0) -> Float(0) = [ + <0,0> + ] + linref Float : Float(0) -> String(0) = [ + <0,0> + ] + lincat Int = [ + "s" + ] + lindef Int : String(0) -> Int(0) = [ + <0,0> + ] + linref Int : Int(0) -> String(0) = [ + <0,0> + ] lincat N = [ "s" ] @@ -21,11 +43,13 @@ concrete basic_cnc { <0,0> ] lincat P = [ + "s" ] lindef P : String(0) -> P(0) = [ + <0,0> ] linref P : P(0) -> String(0) = [ - + <0,0> ] lincat S = [ "" @@ -36,10 +60,29 @@ concrete basic_cnc { linref S : S(0) -> String(0) = [ <0,0> ] + lincat String = [ + "s" + ] + lindef String : String(0) -> String(0) = [ + <0,0> + ] + linref String : String(0) -> String(0) = [ + <0,0> + ] lin c : ∀{i<2} . N(i) -> S(0) = [ <0,0> ] + lin floatLit : Float(0) -> S(0) = [ + <0,0> + ] lin ind : ∀{i<2} . P(0) * P(0) * N(i) -> P(0) = [ + <0,0> "&" "λ" SOFT_BIND <1,$0> SOFT_BIND "," SOFT_BIND <1,$1> "." <1,0> + ] + lin intLit : Int(0) -> S(0) = [ + <0,0> + ] + lin nat : ∀{i<2} . N(i) -> P(0) = [ + "nat" SOFT_BIND "(" SOFT_BIND <0,0> SOFT_BIND ")" ] lin s : N(0) -> N(0) = [ <0,0> "+" "1" @@ -47,6 +90,9 @@ concrete basic_cnc { lin s : N(1) -> N(0) = [ "1" ] + lin stringLit : String(0) -> S(0) = [ + <0,0> + ] lin z : N(1) = [ "0" ] diff --git a/src/runtime/haskell/tests/basic_cnc.gf b/src/runtime/haskell/tests/basic_cnc.gf index 40c42f3e6..75cbd86c2 100644 --- a/src/runtime/haskell/tests/basic_cnc.gf +++ b/src/runtime/haskell/tests/basic_cnc.gf @@ -17,6 +17,12 @@ lin z = {s="0"; is_zero=True} ; lin c n = n.s ; -lincat P = {}; +lincat P = {s:Str}; +lin nat n = {s="nat"++SOFT_BIND++"("++SOFT_BIND++n.s++SOFT_BIND++")"}; +lin ind pz ps n = {s=pz.s ++ "&" ++ "λ"++SOFT_BIND++ps.$0++SOFT_BIND++","++SOFT_BIND++ps.$1 ++ "." ++ ps.s} ; + +lin intLit n = n.s ; +lin stringLit s = s.s ; +lin floatLit f = f.s ; } diff --git a/src/runtime/haskell/tests/linearization.hs b/src/runtime/haskell/tests/linearization.hs new file mode 100644 index 000000000..3f1c5f345 --- /dev/null +++ b/src/runtime/haskell/tests/linearization.hs @@ -0,0 +1,25 @@ +import Test.HUnit +import PGF2 +import qualified Data.Map as Map + +main = do + gr <- readPGF "tests/basic.pgf" + let Just cnc = Map.lookup "basic_cnc" (languages gr) + runTestTTAndExit $ + TestList + [TestCase (assertEqual "zero" "0" (linearize cnc (mkApp "z" []))) + ,TestCase (assertEqual "one" "1" (linearize cnc (mkApp "s" [mkApp "z" []]))) + ,TestCase (assertEqual "two" "1 + 1" (linearize cnc (mkApp "s" [mkApp "s" [mkApp "z" []]]))) + ,TestCase (assertEqual "two'" "(S:1 (N:2 (N:3 1) + 1))" (showBracketedString (head (bracketedLinearize cnc (mkApp "c" [mkApp "s" [mkApp "s" [mkApp "z" []]]]))))) + ,TestCase (assertEqual "foo" "(S:1 (N:2 (N:3 [foo]) + 1))" (showBracketedString (head (bracketedLinearize cnc (mkApp "c" [mkApp "s" [mkApp "foo" []]]))))) + ,TestCase (assertEqual "meta" "(S:1 (N:2 (N:3 ?1) + 1))" (showBracketedString (head (bracketedLinearize cnc (mkApp "c" [mkApp "s" [mkMeta 1]]))))) + ,TestCase (assertEqual "ind" "nat(0) & λx,p . nat(x + 1)" (linearize cnc (mkApp "ind" [mkApp "nat" [mkApp "z" []], mkAbs Explicit "x" (mkAbs Explicit "p" (mkApp "nat" [mkApp "s" [mkVar 1]])),mkApp "s" [mkApp "z" []]]))) + ,TestCase (assertEqual "parse tree 1" graphviz_parse1 (graphvizParseTree cnc graphvizDefaults (mkApp "c" [mkApp "s" [mkMeta 1]]))) + ,TestCase (assertEqual "intLit" "666" (linearize cnc (mkApp "intLit" [mkInt 666]))) + ,TestCase (assertEqual "floatLit" "3.14" (linearize cnc (mkApp "floatLit" [mkFloat 3.14]))) + ,TestCase (assertEqual "stringLit" "abcd" (linearize cnc (mkApp "stringLit" [mkStr "abcd"]))) + ,TestCase (assertEqual "parse tree 2" graphviz_parse2 (graphvizParseTree cnc graphvizDefaults (mkApp "stringLit" [mkStr "abcd"]))) + ] + +graphviz_parse1="graph {\n node[shape=plaintext]\n\n subgraph {\n rank=same;\n n1[label=\"c : S\"]\n }\n\n subgraph {\n rank=same;\n n2[label=\"s : N\"]\n }\n n1 -- n2\n\n subgraph {\n rank=same;\n n3[label=\"_ : N\"]\n }\n n2 -- n3\n\n subgraph {\n rank=same;\n edge[style=invis]\n n100000[label=\"?1\"]\n n100001[label=\"+\"]\n n100002[label=\"1\"]\n n100000 -- n100001 -- n100002\n }\n n3 -- n100000\n n2 -- n100001\n n2 -- n100002\n}" +graphviz_parse2="graph {\n node[shape=plaintext]\n\n subgraph {\n rank=same;\n n1[label=\"stringLit : S\"]\n }\n\n subgraph {\n rank=same;\n n2[label=\"_ : String\"]\n }\n n1 -- n2\n\n subgraph {\n rank=same;\n n100000[label=\"abcd\"]\n }\n n2 -- n100000\n}" diff --git a/src/runtime/haskell/tests/transactions.hs b/src/runtime/haskell/tests/transactions.hs index d1925222a..84a3e1c34 100644 --- a/src/runtime/haskell/tests/transactions.hs +++ b/src/runtime/haskell/tests/transactions.hs @@ -26,17 +26,17 @@ main = do c <- runTestTT $ TestList $ - [TestCase (assertEqual "original functions" ["c","ind","s","z"] (functions gr1)) - ,TestCase (assertEqual "extended functions" ["c","foo","ind","s","z"] (functions gr2)) - ,TestCase (assertEqual "branched functions" ["bar","c","ind","s","z"] (functions gr3)) - ,TestCase (assertEqual "checked-out extended functions" ["c","foo","ind","s","z"] (functions gr4)) - ,TestCase (assertEqual "checked-out branched functions" ["bar","c","ind","s","z"] (functions gr5)) + [TestCase (assertEqual "original functions" ["c","floatLit","ind","intLit","nat","s","stringLit","z"] (functions gr1)) + ,TestCase (assertEqual "extended functions" ["c","floatLit","foo","ind","intLit","nat","s","stringLit","z"] (functions gr2)) + ,TestCase (assertEqual "branched functions" ["bar","c","floatLit","ind","intLit","nat","s","stringLit","z"] (functions gr3)) + ,TestCase (assertEqual "checked-out extended functions" ["c","floatLit","foo","ind","intLit","nat","s","stringLit","z"] (functions gr4)) + ,TestCase (assertEqual "checked-out branched functions" ["bar","c","floatLit","ind","intLit","nat","s","stringLit","z"] (functions gr5)) ,TestCase (assertEqual "original categories" ["Float","Int","N","P","S","String"] (categories gr1)) ,TestCase (assertEqual "extended categories" ["Float","Int","N","P","Q","S","String"] (categories gr2)) ,TestCase (assertEqual "branched categories" ["Float","Int","N","P","R","S","String"] (categories gr3)) ,TestCase (assertEqual "Q context" (Just [(Explicit,"x",ty)]) (categoryContext gr2 "Q")) ,TestCase (assertEqual "R context" (Just [(Explicit,"x",ty)]) (categoryContext gr3 "R")) - ,TestCase (assertEqual "reduced functions" ["c","s","z"] (functions gr6)) + ,TestCase (assertEqual "reduced functions" ["c","floatLit","intLit","nat","s","stringLit","z"] (functions gr6)) ,TestCase (assertEqual "reduced categories" ["Float","Int","N","P","String"] (categories gr6)) ,TestCase (assertEqual "old function type" Nothing (functionType gr1 "foo")) ,TestCase (assertEqual "new function type" (Just ty) (functionType gr2 "foo"))