Tools.hs revision 3cc59e09c101e2864f585527d2216280451bccc8
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiuimport qualified MMT.Tools as Generic
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiubool_from_pt :: (Generic.Tree) -> Maybe(Bool')
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiubool_from_pt x = case x of
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu (Generic.Application n Nothing args ) -> if (n == "equiv")
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu then if (length(args) == 2)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu then (Just((Equiv (fromJust (bool_from_pt (args !! 0) ) ) (fromJust (bool_from_pt (args !! 1) ) ) )))
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu else if (n == "impl")
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu then if (length(args) == 2)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu then (Just((Impl (fromJust (bool_from_pt (args !! 0) ) ) (fromJust (bool_from_pt (args !! 1) ) ) )))
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu else if (n == "not")
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu then if (length(args) == 1)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu then (Just((Not (fromJust (bool_from_pt (args !! 0) ) ) )))
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu else if (n == "or")
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu then if (length(args) == 2)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu then (Just((Or (fromJust (bool_from_pt (args !! 0) ) ) (fromJust (bool_from_pt (args !! 1) ) ) )))
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu else if (n == "and")
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu then if (length(args) == 2)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu then (Just((And (fromJust (bool_from_pt (args !! 0) ) ) (fromJust (bool_from_pt (args !! 1) ) ) )))
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu else if (n == "false")
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu then if (length(args) == 0)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu then (Just((False')))
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu else if (n == "true")
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu then if (length(args) == 0)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu then (Just((True')))
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu (Generic.Application n (Just((pat,inst))) args ) -> Nothing
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu (Generic.Bind _n _v _s ) -> Nothing
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu (Generic.Tbind _n _a _v _s ) -> Nothing
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiudecl_from_pt :: (Generic.Decl) -> Maybe(Decl)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiudecl_from_pt d = case d of
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu (Generic.Decl pname iname args ) -> if (pname == "prop")
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu then if (length(args) == 0)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu then (Just((Prop_decl (Prop iname ) )))
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu else if (pname == ".")
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu then if (length(args) == 1)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu then (Just((Dot_decl (Dot iname (fromJust (bool_from_pt (args !! 0) ) ) ) )))
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiusign_from_pt :: (Generic.Sign) -> Sigs
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiusign_from_pt (Generic.Sign sg) = (Sigs (map (fromJust.decl_from_pt) sg) )
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiuaxiom_from_pt :: (Generic.Tree) -> Bool'
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiuaxiom_from_pt ax = (fromJust (bool_from_pt ax ) )
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiutheo_from_pt :: (Generic.Theo) -> Theo
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiutheo_from_pt th = Theo{sign = (sign_from_pt (Generic.sign th) ),axioms = (map axiom_from_pt (Generic.axioms th))}