GitHub/gf-core
1
0
Fork 1
mirror of https://github.com/GrammaticalFramework/gf-core.git synced 2026-09-28 13:13:37 -06:00
Code Issues Packages Projects Releases Wiki Activity

first draft of a typechecker

Browse Source
This commit is contained in:
Krasimir Angelov
2024-03-06 09:08:15 +01:00
parent 14a9a8d463
commit 5426b4209f
13 changed files with 708 additions and 105 deletions
Download Patch File Download Diff File Expand all files Collapse all files
src/runtime/haskell/PGF2.hsc
+66 -2
View File
@@ -481,7 +481,37 @@ exprProbability p e =
withPgfExn "exprProbability" (pgf_expr_prob (a_db p) c_revision c_e marshaller)
checkExpr :: PGF -> Expr -> Type -> Either String Expr
checkExpr = error "TODO: checkExpr"
checkExpr p e ty =
unsafePerformIO $
withForeignPtr (a_revision p) $ \c_revision ->
bracket (newStablePtr e) freeStablePtr $ \c_e ->
bracket (newStablePtr ty) freeStablePtr $ \c_ty ->
allocaBytes (#size PgfExn) $ \c_exn -> do
c_e <- pgf_check_expr (a_db p) c_revision c_e c_ty marshaller unmarshaller c_exn
ex_type <- (#peek PgfExn, type) c_exn :: IO (#type PgfExnType)
case ex_type of
(#const PGF_EXN_NONE) -> do
e <- deRefStablePtr c_e
freeStablePtr c_e
return (Right e)
(#const PGF_EXN_SYSTEM_ERROR) -> do
errno <- (#peek PgfExn, code) c_exn
c_msg <- (#peek PgfExn, msg) c_exn
mb_fpath <- if c_msg == nullPtr
then return Nothing
else fmap Just (peekCString c_msg)
ioError (errnoToIOError "checkExpr" (Errno errno) Nothing mb_fpath)
(#const PGF_EXN_PGF_ERROR) -> do
c_msg <- (#peek PgfExn, msg) c_exn
msg <- peekCString c_msg
free c_msg
throwIO (PGFError "checkExpr" msg)
(#const PGF_EXN_TYPE_ERROR) -> do
c_msg <- (#peek PgfExn, msg) c_exn
msg <- peekCString c_msg
free c_msg
return (Left msg)
_ -> throwIO (PGFError "checkExpr" "An unidentified error occurred")
-- | Tries to infer the type of an expression. Note that
-- even if the expression is type correct it is not always
@@ -513,6 +543,11 @@ inferExpr p e =
else fmap Just (peekCString c_msg)
ioError (errnoToIOError "inferExpr" (Errno errno) Nothing mb_fpath)
(#const PGF_EXN_PGF_ERROR) -> do
c_msg <- (#peek PgfExn, msg) c_exn
msg <- peekCString c_msg
free c_msg
throwIO (PGFError "inferExpr" msg)
(#const PGF_EXN_TYPE_ERROR) -> do
c_msg <- (#peek PgfExn, msg) c_exn
msg <- peekCString c_msg
free c_msg
@@ -522,7 +557,36 @@ inferExpr p e =
-- | Check whether a type is consistent with the abstract
-- syntax of the grammar.
checkType :: PGF -> Type -> Either String Type
checkType pgf ty = Right ty
checkType p ty =
unsafePerformIO $
withForeignPtr (a_revision p) $ \c_revision ->
bracket (newStablePtr ty) freeStablePtr $ \c_ty ->
allocaBytes (#size PgfExn) $ \c_exn -> do
c_ty <- pgf_check_type (a_db p) c_revision c_ty marshaller unmarshaller c_exn
ex_type <- (#peek PgfExn, type) c_exn :: IO (#type PgfExnType)
case ex_type of
(#const PGF_EXN_NONE) -> do
ty <- deRefStablePtr c_ty
freeStablePtr c_ty
return (Right ty)
(#const PGF_EXN_SYSTEM_ERROR) -> do
errno <- (#peek PgfExn, code) c_exn
c_msg <- (#peek PgfExn, msg) c_exn
mb_fpath <- if c_msg == nullPtr
then return Nothing
else fmap Just (peekCString c_msg)
ioError (errnoToIOError "checkType" (Errno errno) Nothing mb_fpath)
(#const PGF_EXN_PGF_ERROR) -> do
c_msg <- (#peek PgfExn, msg) c_exn
msg <- peekCString c_msg
free c_msg
throwIO (PGFError "checkType" msg)
(#const PGF_EXN_TYPE_ERROR) -> do
c_msg <- (#peek PgfExn, msg) c_exn
msg <- peekCString c_msg
free c_msg
return (Left msg)
_ -> throwIO (PGFError "checkType" "An unidentified error occurred")
-- | Check whether a context is consistent with the abstract
-- syntax of the grammar.
src/runtime/haskell/PGF2/FFI.hsc
+2 -2
View File
@@ -203,11 +203,11 @@ foreign import ccall pgf_concrete_language_code :: Ptr PgfDB -> Ptr Concr -> Ptr
foreign import ccall pgf_expr_prob :: Ptr PgfDB -> Ptr PGF -> StablePtr Expr -> Ptr PgfMarshaller -> Ptr PgfExn -> IO (#type prob_t)
foreign import ccall pgf_check_expr :: Ptr PgfDB -> Ptr PGF -> Ptr (StablePtr Expr) -> StablePtr Type -> Ptr PgfMarshaller -> Ptr PgfUnmarshaller -> Ptr PgfExn -> IO ()
foreign import ccall pgf_check_expr :: Ptr PgfDB -> Ptr PGF -> StablePtr Expr -> StablePtr Type -> Ptr PgfMarshaller -> Ptr PgfUnmarshaller -> Ptr PgfExn -> IO (StablePtr Expr)
foreign import ccall pgf_infer_expr :: Ptr PgfDB -> Ptr PGF -> Ptr (StablePtr Expr) -> Ptr PgfMarshaller -> Ptr PgfUnmarshaller -> Ptr PgfExn -> IO (StablePtr Type)
foreign import ccall pgf_check_type :: Ptr PgfDB -> Ptr PGF -> Ptr (StablePtr Type) -> Ptr PgfMarshaller -> Ptr PgfUnmarshaller -> Ptr PgfExn -> IO ()
foreign import ccall pgf_check_type :: Ptr PgfDB -> Ptr PGF -> StablePtr Type -> Ptr PgfMarshaller -> Ptr PgfUnmarshaller -> Ptr PgfExn -> IO (StablePtr Type)
foreign import ccall pgf_generate_random :: Ptr PgfDB -> Ptr PGF -> Ptr (Ptr Concr) -> CSize -> StablePtr Type -> CSize -> Ptr Word64 -> Ptr (#type prob_t) -> Ptr PgfMarshaller -> Ptr PgfUnmarshaller -> Ptr PgfExn -> IO (StablePtr Expr)
src/runtime/haskell/pgf2.cabal
+10
View File
@@ -73,3 +73,13 @@ test-suite linearization
HUnit >= 1.6.1.0,
containers,
pgf2
test-suite typechecking
type: exitcode-stdio-1.0
main-is: tests/typechecking.hs
default-language: Haskell2010
build-depends:
base,
HUnit >= 1.6.1.0,
containers,
pgf2
src/runtime/haskell/tests/basic.gf
+2
View File
@@ -11,6 +11,8 @@ 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 imp : ({x},y : N) -> S ;
fun intLit : Int -> S;
fun stringLit : String -> S;
fun floatLit : Float -> S;
src/runtime/haskell/tests/basic.hs
+2 -2
View File
@@ -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","floatLit","ind","intLit","nat","s","stringLit","z"] (functions gr))
,TestCase (assertEqual "abstract functions" ["c","floatLit","imp","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","floatLit","intLit","stringLit"] (functionsByCat gr "S"))
,TestCase (assertEqual "abstract functions by cat 2" ["c","floatLit","imp","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")))
src/runtime/haskell/tests/basic.pgf
BIN
View File
Binary file not shown.
src/runtime/haskell/tests/basic.pmcfg
+5 -4
View File
@@ -5,13 +5,14 @@ abstract basic {
cat P N ; -- 0.693147
cat S ; -- 0.693147
cat String ; -- 0.693147
data c : N -> S ; -- 1.38629
fun floatLit : Float -> S ; -- 1.38629
data c : N -> S ; -- 1.60944
fun floatLit : Float -> S ; -- 1.60944
fun imp : ({x} : N) -> (y : N) -> S ; -- 1.60944
fun ind : P z -> ((x : N) -> P x -> P (s x)) -> (x : N) -> P x ; -- 0.693147
fun intLit : Int -> S ; -- 1.38629
fun intLit : Int -> S ; -- 1.60944
fun nat : (x : N) -> P x ; -- 0.693147
data s : N -> N ; -- 0.693147
fun stringLit : String -> S ; -- 1.38629
fun stringLit : String -> S ; -- 1.60944
data z : N ; -- 0.693147
}
concrete basic_cnc {
src/runtime/haskell/tests/transactions.hs
+3 -3
View File
@@ -41,11 +41,11 @@ main = do
c <- runTestTT $
TestList $
[TestCase (assertEqual "original functions" ["c","floatLit","ind","intLit","nat","s","stringLit","z"] (functions gr1))
[TestCase (assertEqual "original functions" ["c","floatLit","imp","ind","intLit","nat","s","stringLit","z"] (functions gr1))
,TestCase (assertEqual "existing function" (Left (PGFError "modifyPGF" "A function with that name already exists")) excpt1)
,TestCase (assertEqual "existing category" (Left (PGFError "modifyPGF" "A category with that name already exists")) excpt2)
,TestCase (assertEqual "extended functions" ["c","floatLit","foo","ind","intLit","nat","s","stringLit","z"] (functions gr2))
,TestCase (assertEqual "checked-out extended functions" ["c","floatLit","foo","ind","intLit","nat","s","stringLit","z"] (functions gr4))
,TestCase (assertEqual "extended functions" ["c","floatLit","foo","imp","ind","intLit","nat","s","stringLit","z"] (functions gr2))
,TestCase (assertEqual "checked-out extended functions" ["c","floatLit","foo","imp","ind","intLit","nat","s","stringLit","z"] (functions gr4))
,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 "Q context" (Just [(Explicit,"x",ty)]) (categoryContext gr2 "Q"))
src/runtime/haskell/tests/typechecking.hs
+73
View File
@@ -0,0 +1,73 @@
import Test.HUnit
import Test.HUnit.Text
import PGF2
main = do
gr <- readPGF "tests/basic.pgf"
runTestTTAndExit $
TestList $
[TestCase (assertInference "infer fun" gr (Right "N") "z")
,TestCase (assertInference "infer app" gr (Right "N") "s z")
,TestCase (assertInference "infer n-args 1" gr (Left "Too many arguments") "z z")
,TestCase (assertInference "infer n-args 2" gr (Left "Too many arguments") "s z z")
,TestCase (assertInference "infer implarg 1" gr (Left "Unexpected implicit argument") "s {z}")
,TestCase (assertInference "infer implarg 2" gr (Right "(y : N) -> S") "imp {z}") --
,TestCase (assertInference "infer implarg 3" gr (Right "S") "imp {z} z")
,TestCase (assertInference "infer implarg 4" gr (Right "({x},y : N) -> S") "imp")
,TestCase (assertInference' "infer implarg 4" gr (Right ("imp {?} z","S")) "imp z")
,TestCase (assertInference "infer typed 1" gr (Right "N->N") "<s : N->N>")
,TestCase (assertInference "infer typed 2" gr (Left "Types doesn't match") "<s : N>")
,TestCase (assertInference "infer typed 3" gr (Left "Too many arguments to category N - 0 expected but 1 given") "<s : N z>")
,TestCase (assertInference "infer hoas 1" gr (Left "Types doesn't match") "s s")
,TestCase (assertInference "infer literal 1" gr (Right "Int") "0")
,TestCase (assertInference "infer literal 2" gr (Right "Float") "3.14")
,TestCase (assertInference "infer literal 3" gr (Right "String") "\"abc\"")
,TestCase (assertInference "infer meta 1" gr (Left "Cannot infer the type of a meta variable") "?")
,TestCase (assertInference "infer meta 2" gr (Right "N->N") "<? : N->N>")
,TestCase (assertChecking "check fun" gr (Right "s") "s" "N->N")
,TestCase (assertChecking "check fun" gr (Right "s z") "s z" "N")
,TestCase (assertChecking "check fun" gr (Left "Types doesn't match") "s z" "N->N")
,TestCase (assertType "check type 1" gr (Right "N -> N") "N -> N")
,TestCase (assertType "check type 2" gr (Left "Category s is not defined") "s")
,TestCase (assertType "check type 3" gr (Left "Too many arguments to category N - 0 expected but 1 given") "N z")
,TestCase (assertType "check type 4" gr (Left "Too few arguments to category P - 1 expected but 0 given") "P")
,TestCase (assertType "check type 5" gr (Right "P z") "P z")
,TestCase (assertType "check type 6" gr (Left "Types doesn't match") "P s")
,TestCase (assertType "check type 7" gr (Left "Unexpected implicit argument") "P {z}")
]
assertInference name gr (Left msg) e =
case readExpr e of
Just e -> assertEqual name (Left msg) (inferExpr gr e)
_ -> error "Reading the expression failed"
assertInference name gr (Right ty) e =
case (readType ty, readExpr e) of
(Just ty,Just e) -> assertEqual name (Right (e,ty)) (inferExpr gr e)
_ -> error "Reading the type/expression failed"
assertInference' name gr (Left msg) e =
case readExpr e of
Just e -> assertEqual name (Left msg) (inferExpr gr e)
_ -> error "Reading the expression failed"
assertInference' name gr (Right (e1,ty)) e0 =
case (readExpr e1, readType ty, readExpr e0) of
(Just e1,Just ty,Just e0) -> assertEqual name (Right (e1,ty)) (inferExpr gr e0)
_ -> error "Reading the type/expression failed"
assertChecking name gr (Left msg) e ty =
case (readExpr e, readType ty) of
(Just e,Just ty) -> assertEqual name (Left msg) (checkExpr gr e ty)
_ -> error "Reading the expression failed"
assertChecking name gr (Right e1) e ty =
case (readExpr e1, readExpr e, readType ty) of
(Just e1,Just e,Just ty) -> assertEqual name (Right e1) (checkExpr gr e ty)
_ -> error "Reading the type/expression failed"
assertType name gr (Left msg) ty =
case readType ty of
Just ty -> assertEqual name (Left msg) (checkType gr ty)
_ -> error "Reading the type failed"
assertType name gr (Right ty) ty0 =
case (readType ty, readType ty0) of
(Just ty,Just ty0) -> assertEqual name (Right ty) (checkType gr ty0)
_ -> error "Reading the type failed"