added API for print names

This commit is contained in:
krangelov
2021-12-03 16:49:36 +01:00
parent 655576c291
commit bbff79aaa3
10 changed files with 86 additions and 8 deletions

View File

@@ -415,7 +415,14 @@ concreteFlag c name =
return (Just lit)
printName :: Concr -> Fun -> Maybe String
printName lang fun = error "TODO: printName"
printName c fun =
unsafePerformIO $
withText fun $ \c_fun ->
withForeignPtr (c_revision c) $ \c_revision ->
bracket (withPgfExn "printName" (pgf_get_printname (c_db c) c_revision c_fun)) free $ \c_name -> do
if c_name /= nullPtr
then fmap Just $ peekText c_name
else return Nothing
alignWords :: Concr -> Expr -> [(String, [Int])]
alignWords = error "TODO: alignWords"

View File

@@ -210,6 +210,10 @@ foreign import ccall "wrapper" wrapSymbol2 :: Wrapper (Ptr PgfLinearizationOutpu
foreign import ccall "wrapper" wrapSymbol3 :: Wrapper (Ptr PgfLinearizationOutputIface -> CInt -> IO ())
foreign import ccall pgf_get_printname :: Ptr PgfDB -> Ptr Concr -> Ptr PgfText -> Ptr PgfExn -> IO (Ptr PgfText)
foreign import ccall pgf_set_printname :: Ptr PgfDB -> Ptr Concr -> Ptr PgfText -> Ptr PgfText -> Ptr PgfExn -> IO ()
foreign import ccall pgf_get_global_flag :: Ptr PgfDB -> Ptr PGF -> Ptr PgfText -> Ptr PgfUnmarshaller -> Ptr PgfExn -> IO (StablePtr Literal)
foreign import ccall pgf_set_global_flag :: Ptr PgfDB -> Ptr PGF -> Ptr PgfText -> StablePtr Literal -> Ptr PgfMarshaller -> Ptr PgfExn -> IO ()

View File

@@ -24,6 +24,7 @@ module PGF2.Transactions
, dropLincat
, createLin
, dropLin
, setPrintName
) where
import PGF2.FFI
@@ -344,3 +345,9 @@ dropLin :: Fun -> Transaction Concr ()
dropLin name = Transaction $ \c_db _ c_revision c_exn ->
withText name $ \c_name ->
pgf_drop_lin c_db c_revision c_name c_exn
setPrintName :: Fun -> String -> Transaction Concr ()
setPrintName fun name = Transaction $ \c_db _ c_revision c_exn ->
withText fun $ \c_fun ->
withText name $ \c_name -> do
withPgfExn "setPrintName" (pgf_set_printname c_db c_revision c_fun c_name)

Binary file not shown.

View File

@@ -19,10 +19,10 @@ concrete basic_cnc {
lincat S = [
""
]
lin c : ∀{j<2} . N(j) -> S(0) = [
lin c : ∀{i<2} . N(i) -> S(0) = [
<0,0>
]
lin ind : ∀{j<2} . P(0) * P(0) * N(j) -> P(0) = [
lin ind : ∀{i<2} . P(0) * P(0) * N(i) -> P(0) = [
]
lin s : N(0) -> N(0) = [
<0,0> "+" "1"

View File

@@ -3,6 +3,9 @@ concrete basic_cnc of basic = open Prelude in {
lincat N = {s : Str; is_zero : Bool} ;
lincat S = Str ;
printname fun z = "0" ;
printname fun s = "1" ;
lin z = {s="0"; is_zero=True} ;
s n = {
s = case n.is_zero of {