diff --git a/src/runtime/c/pgf/pgf.cxx b/src/runtime/c/pgf/pgf.cxx index cf44844d8..3f3a5bdcf 100644 --- a/src/runtime/c/pgf/pgf.cxx +++ b/src/runtime/c/pgf/pgf.cxx @@ -167,6 +167,30 @@ void pgf_iter_categories(PgfPGF* pgf, PgfItor* itor) namespace_iter(pgf->get_root()->abstract.cats, itor); } +PGF_API PgfTypeHypo* +pgf_category_context(PgfPGF *pgf, PgfText *catname, size_t *n_hypos) +{ + DB_scope scope(pgf, READER_SCOPE); + + ref abscat = + namespace_lookup(pgf->get_root()->abstract.cats, catname); + if (abscat == 0) { + *n_hypos = 0; + return NULL; + } + + PgfTypeHypo *hypos = (PgfTypeHypo *) + malloc(abscat->context->len * sizeof(PgfTypeHypo)); + for (size_t i = 0; i < abscat->context->len; i++) { + hypos[i].bind_type = abscat->context->data[i].bind_type; + hypos[i].cid = textdup(abscat->context->data[i].cid); + hypos[i].type = pgf_unmarshall_type(pgf->u, abscat->context->data[i].type); + } + + *n_hypos = abscat->context->len; + return hypos; +} + PGF_API void pgf_iter_functions(PgfPGF* pgf, PgfItor* itor) { diff --git a/src/runtime/c/pgf/pgf.h b/src/runtime/c/pgf/pgf.h index e93ee1a3a..86b81e498 100644 --- a/src/runtime/c/pgf/pgf.h +++ b/src/runtime/c/pgf/pgf.h @@ -160,6 +160,9 @@ PgfText *pgf_abstract_name(PgfPGF* pgf); PGF_API_DECL void pgf_iter_categories(PgfPGF* pgf, PgfItor* itor); +PGF_API_DECL PgfTypeHypo* +pgf_category_context(PgfPGF *pgf, PgfText *catname, size_t *n_hypos); + PGF_API_DECL void pgf_iter_functions(PgfPGF* pgf, PgfItor* itor); diff --git a/src/runtime/haskell/PGF2.hsc b/src/runtime/haskell/PGF2.hsc index 46aff9ce9..6587addab 100644 --- a/src/runtime/haskell/PGF2.hsc +++ b/src/runtime/haskell/PGF2.hsc @@ -19,7 +19,7 @@ module PGF2 (-- * PGF -- * Abstract syntax AbsName,abstractName, -- ** Categories - Cat,categories, + Cat,categories,categoryContext, -- ** Functions Fun, functions, functionsByCat, functionType, @@ -163,6 +163,34 @@ categories p = name <- peekText key writeIORef ref $ (name : names) +categoryContext :: PGF -> Cat -> [Hypo] +categoryContext p cat = + unsafePerformIO $ + withText cat $ \c_cat -> + alloca $ \p_n_hypos -> + withForeignPtr (a_pgf p) $ \c_pgf -> + mask_ $ do + c_hypos <- pgf_category_context c_pgf c_cat p_n_hypos + if c_hypos == nullPtr + then return [] + else do n_hypos <- peek p_n_hypos + hypos <- peekHypos c_hypos 0 n_hypos + free c_hypos + return hypos + where + peekHypos :: Ptr PgfTypeHypo -> CSize -> CSize -> IO [Hypo] + peekHypos c_hypo i n + | i < n = do c_cat <- (#peek PgfTypeHypo, cid) c_hypo + cat <- peekText c_cat + free c_cat + c_ty <- (#peek PgfTypeHypo, type) c_hypo + ty <- deRefStablePtr c_ty + freeStablePtr c_ty + bt <- fmap unmarshalBindType ((#peek PgfTypeHypo, bind_type) c_hypo) + hs <- peekHypos (plusPtr c_hypo (#size PgfTypeHypo)) (i+1) n + return ((bt,cat,ty) : hs) + | otherwise = return [] + -- | List of all functions defined in the abstract syntax functions :: PGF -> [Fun] functions p = diff --git a/src/runtime/haskell/PGF2/FFI.hsc b/src/runtime/haskell/PGF2/FFI.hsc index ae519dcd6..fdf1ca225 100644 --- a/src/runtime/haskell/PGF2/FFI.hsc +++ b/src/runtime/haskell/PGF2/FFI.hsc @@ -63,6 +63,9 @@ foreign import ccall "wrapper" foreign import ccall "pgf_iter_categories" pgf_iter_categories :: Ptr PgfPGF -> Ptr PgfItor -> IO () +foreign import ccall "pgf/pgf.h pgf_category_context" + pgf_category_context :: Ptr PgfPGF -> Ptr PgfText -> Ptr CSize -> IO (Ptr PgfTypeHypo) + foreign import ccall "pgf_iter_functions" pgf_iter_functions :: Ptr PgfPGF -> Ptr PgfItor -> IO () diff --git a/src/runtime/haskell/tests/basic.gf b/src/runtime/haskell/tests/basic.gf index 534c1be2d..b50286ef2 100644 --- a/src/runtime/haskell/tests/basic.gf +++ b/src/runtime/haskell/tests/basic.gf @@ -7,4 +7,7 @@ fun z : N ; fun c : N -> S ; +cat P N ; +fun ind : P z -> ((x:N) -> P x -> P (s x)) -> ((x : N) -> P x) ; + } diff --git a/src/runtime/haskell/tests/basic.hs b/src/runtime/haskell/tests/basic.hs index 032913849..2cd6b8596 100644 --- a/src/runtime/haskell/tests/basic.hs +++ b/src/runtime/haskell/tests/basic.hs @@ -5,13 +5,18 @@ main = do gr <- readPGF "tests/basic.pgf" runTestTTAndExit $ TestList [TestCase (assertEqual "abstract names" "basic" (abstractName gr)) - ,TestCase (assertEqual "abstract categories" ["Float","Int","N","S","String"] (categories gr)) - ,TestCase (assertEqual "abstract functions" ["c","s","z"] (functions 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 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" [] (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"))) ,TestCase (assertBool "type of c" (eqJust (readType "N->S") (functionType gr "c"))) + ,TestCase (assertEqual "category context 1" [] (categoryContext gr "N")) + ,TestCase (assertEqual "category context 1" [] (categoryContext gr "S")) + ,TestCase (assertEqual "category context 1" [(Explicit,"_",DTyp [] "N" [])] (categoryContext gr "P")) + ,TestCase (assertEqual "category context 1" [] (categoryContext gr "X")) -- no such category ] eqJust (Just x) (Just y) = x == y diff --git a/src/runtime/haskell/tests/basic.pgf b/src/runtime/haskell/tests/basic.pgf index d897827e8..61d1b6e01 100644 Binary files a/src/runtime/haskell/tests/basic.pgf and b/src/runtime/haskell/tests/basic.pgf differ