1
0
forked from GitHub/gf-core

added testsuite for linearization

This commit is contained in:
krangelov
2021-12-09 08:46:29 +01:00
parent 0069946f42
commit 72982d2344
8 changed files with 104 additions and 12 deletions

View File

@@ -64,3 +64,13 @@ test-suite transactions
HUnit >= 1.6.1.0, HUnit >= 1.6.1.0,
containers, containers,
pgf2 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

View File

@@ -8,6 +8,11 @@ data z : N ;
data c : N -> S ; data c : N -> S ;
cat P N ; 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 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;
} }

View File

@@ -15,9 +15,9 @@ main = do
grammarTests gr = grammarTests gr =
[TestCase (assertEqual "abstract names" "basic" (abstractName gr)) [TestCase (assertEqual "abstract names" "basic" (abstractName gr))
,TestCase (assertEqual "abstract categories" ["Float","Int","N","P","S","String"] (categories 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 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 (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 z" (eqJust (readType "N") (functionType gr "z")))
,TestCase (assertBool "type of s" (eqJust (readType "N->N") (functionType gr "s"))) ,TestCase (assertBool "type of s" (eqJust (readType "N->N") (functionType gr "s")))

Binary file not shown.

View File

@@ -5,12 +5,34 @@ abstract basic {
cat P N ; -- 0.693147 cat P N ; -- 0.693147
cat S ; -- 0.693147 cat S ; -- 0.693147
cat String ; -- 0.693147 cat String ; -- 0.693147
data c : N -> S ; -- -0 data c : N -> S ; -- 1.38629
fun ind : P z -> ((x : N) -> P x -> P (s x)) -> (x : N) -> P x ; -- -0 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 data s : N -> N ; -- 0.693147
fun stringLit : String -> S ; -- 1.38629
data z : N ; -- 0.693147 data z : N ; -- 0.693147
} }
concrete basic_cnc { 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 = [ lincat N = [
"s" "s"
] ]
@@ -21,11 +43,13 @@ concrete basic_cnc {
<0,0> <0,0>
] ]
lincat P = [ lincat P = [
"s"
] ]
lindef P : String(0) -> P(0) = [ lindef P : String(0) -> P(0) = [
<0,0>
] ]
linref P : P(0) -> String(0) = [ linref P : P(0) -> String(0) = [
<0,0>
] ]
lincat S = [ lincat S = [
"" ""
@@ -36,10 +60,29 @@ concrete basic_cnc {
linref S : S(0) -> String(0) = [ linref S : S(0) -> String(0) = [
<0,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) = [ lin c : ∀{i<2} . N(i) -> S(0) = [
<0,0> <0,0>
] ]
lin floatLit : Float(0) -> S(0) = [
<0,0>
]
lin ind : ∀{i<2} . P(0) * P(0) * N(i) -> P(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) = [ lin s : N(0) -> N(0) = [
<0,0> "+" "1" <0,0> "+" "1"
@@ -47,6 +90,9 @@ concrete basic_cnc {
lin s : N(1) -> N(0) = [ lin s : N(1) -> N(0) = [
"1" "1"
] ]
lin stringLit : String(0) -> S(0) = [
<0,0>
]
lin z : N(1) = [ lin z : N(1) = [
"0" "0"
] ]

View File

@@ -17,6 +17,12 @@ lin z = {s="0"; is_zero=True} ;
lin c n = n.s ; 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 ;
} }

View File

@@ -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}"

View File

@@ -26,17 +26,17 @@ main = do
c <- runTestTT $ c <- runTestTT $
TestList $ TestList $
[TestCase (assertEqual "original functions" ["c","ind","s","z"] (functions gr1)) [TestCase (assertEqual "original functions" ["c","floatLit","ind","intLit","nat","s","stringLit","z"] (functions gr1))
,TestCase (assertEqual "extended functions" ["c","foo","ind","s","z"] (functions gr2)) ,TestCase (assertEqual "extended functions" ["c","floatLit","foo","ind","intLit","nat","s","stringLit","z"] (functions gr2))
,TestCase (assertEqual "branched functions" ["bar","c","ind","s","z"] (functions gr3)) ,TestCase (assertEqual "branched functions" ["bar","c","floatLit","ind","intLit","nat","s","stringLit","z"] (functions gr3))
,TestCase (assertEqual "checked-out extended functions" ["c","foo","ind","s","z"] (functions gr4)) ,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","ind","s","z"] (functions gr5)) ,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 "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 "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 "branched categories" ["Float","Int","N","P","R","S","String"] (categories gr3))
,TestCase (assertEqual "Q context" (Just [(Explicit,"x",ty)]) (categoryContext gr2 "Q")) ,TestCase (assertEqual "Q context" (Just [(Explicit,"x",ty)]) (categoryContext gr2 "Q"))
,TestCase (assertEqual "R context" (Just [(Explicit,"x",ty)]) (categoryContext gr3 "R")) ,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 "reduced categories" ["Float","Int","N","P","String"] (categories gr6))
,TestCase (assertEqual "old function type" Nothing (functionType gr1 "foo")) ,TestCase (assertEqual "old function type" Nothing (functionType gr1 "foo"))
,TestCase (assertEqual "new function type" (Just ty) (functionType gr2 "foo")) ,TestCase (assertEqual "new function type" (Just ty) (functionType gr2 "foo"))