Cross Reference: /hets/todo

	todo revision 183e25edd6aaf48da3cfcf6e5a5300bed5a941df
d29201dd5328b88140ce050100693c501852657dChristian MaederPlan and priority list for CoFI tool activities
7c8051ef91610c696bc9fa2e61ad1b153fbe7ce0Klaus Luettich
7c8051ef91610c696bc9fa2e61ad1b153fbe7ce0Klaus Luettichmost things have been moved to the new bug tracking system
7c8051ef91610c696bc9fa2e61ad1b153fbe7ce0Klaus Luettich
956dc203c5fce297dd8ba3ba77703df3d87c8597Christian Maedersee http://trac.informatik.uni-bremen.de:8080/hets
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescu
7c8051ef91610c696bc9fa2e61ad1b153fbe7ce0Klaus Luettich************************************************
99634745e86bb1c79da4e2b376e580f65ee67082Klaus LuettichKlaus
7c8051ef91610c696bc9fa2e61ad1b153fbe7ce0Klaus Luettich************************************************
7c8051ef91610c696bc9fa2e61ad1b153fbe7ce0Klaus Luettich
7c8051ef91610c696bc9fa2e61ad1b153fbe7ce0Klaus Luettichfor ProofManagement-GUI
99634745e86bb1c79da4e2b376e580f65ee67082Klaus Luettich  provide structured (based on spec-names) selection/deselection facility
7c8051ef91610c696bc9fa2e61ad1b153fbe7ce0Klaus Luettich    of axioms and theorems
99634745e86bb1c79da4e2b376e580f65ee67082Klaus Luettich
7c8051ef91610c696bc9fa2e61ad1b153fbe7ce0Klaus Luettichtrace if liniarity of sentences along development is given
7c8051ef91610c696bc9fa2e61ad1b153fbe7ce0Klaus Luettich
7c8051ef91610c696bc9fa2e61ad1b153fbe7ce0Klaus LuettichIgnore axiom selection for interactive provers
8a6eb5a17ea17b650b29099036549b66eec4884aChristian Maeder
8a6eb5a17ea17b650b29099036549b66eec4884aChristian Maeder((
abee46762c1663b85c6f18d934cd11df83828f6eChristian MaederImprovements:
f56cdf11927c31495bae642a9eb383212c90ba61Christian Maeder * display node name (instead of number) in uDrawGraph widow title
8a6eb5a17ea17b650b29099036549b66eec4884aChristian Maeder * add conversion of equivalent sorts into special arrow
8a6eb5a17ea17b650b29099036549b66eec4884aChristian Maeder    * needs modification of Taxnomy Graph
8a6eb5a17ea17b650b29099036549b66eec4884aChristian Maeder
8a6eb5a17ea17b650b29099036549b66eec4884aChristian MaederTranslation between Achim's ontology data structure and CASL (in Hets)
80c2d23821d095b55d9a547f48fc3fcdc27df405Christian Maeder
5607bbe40d1b360797381a83a6eae6773ee7cd2cChristian Maedervisualization of "taxonomy" of CASL signatures
5607bbe40d1b360797381a83a6eae6773ee7cd2cChristian Maeder  (subsorts = inheritance, unary preds = concepts, binary preds = relations)
7c8051ef91610c696bc9fa2e61ad1b153fbe7ce0Klaus Luettich
5607bbe40d1b360797381a83a6eae6773ee7cd2cChristian Maeder last two ... partially done
5607bbe40d1b360797381a83a6eae6773ee7cd2cChristian Maeder))
5275f013db52ff487795b71ee4dcc9268f62e574Christian Maeder
5607bbe40d1b360797381a83a6eae6773ee7cd2cChristian MaederRecognize guarded fragment of CASL:
7c8051ef91610c696bc9fa2e61ad1b153fbe7ce0Klaus Luettich  G ::= forall x . At(x) => G      where At is a conjunction of atoms
2bb73714b894c8e878fc52e31205a56a563e4805Christian Maeder      | exists x . At(x) /\ G
24b1bb673d802899fed9a32b7044dab9aa6ec121Christian Maeder
b5eebfe4b3f040df3ca96fa18208e04e2d026b0cChristian Maeder
24b1bb673d802899fed9a32b7044dab9aa6ec121Christian MaederBitte auch aus folgenden Files die todo-Listen nach Trac verschieben:
50a881b56a41120f05ad6100dd2a8f1dc3fb81faRazvan Pascanu
52e3fbd71a34c294b93a44c02829991e044d163bChristian MaederCASL_DL/AS_CASL_DL.der.hs:{- todo:
80c2d23821d095b55d9a547f48fc3fcdc27df405Christian MaederCASL_DL/PredefinedGlobalAnnos.hs:  todo:
7c8051ef91610c696bc9fa2e61ad1b153fbe7ce0Klaus LuettichCASL_DL/PredefinedSign.inline.hs: todo:
50a881b56a41120f05ad6100dd2a8f1dc3fb81faRazvan PascanuCASL_DL/Sign.hs:  todo:
076f0bae1471e0122ae67c197bcac3e6799c0a31Christian MaederCASL_DL/StatAna.hs:{- todo:
7c8051ef91610c696bc9fa2e61ad1b153fbe7ce0Klaus LuettichComorphisms/CASL2SPASS.hs:{- todo
7c8051ef91610c696bc9fa2e61ad1b153fbe7ce0Klaus LuettichComorphisms/KnownProvers.hs:{- todo:
7c8051ef91610c696bc9fa2e61ad1b153fbe7ce0Klaus LuettichComorphisms/Modal2CASL.inline.hs:   todo:
8a6eb5a17ea17b650b29099036549b66eec4884aChristian MaederOWL_DL/Logic_OWL_DL.hs:{- todo:
7c8051ef91610c696bc9fa2e61ad1b153fbe7ce0Klaus LuettichOWL_DL/Print.hs:    todo:
076f0bae1471e0122ae67c197bcac3e6799c0a31Christian MaederOWL_DL/ReadWrite.der.hs:{- todo:
734a5ebd38032798f0ab908e2d52862c71b2c127Simon UlbrichtOWL_DL/ReadWrite.hs:{- todo:
076f0bae1471e0122ae67c197bcac3e6799c0a31Christian MaederOWL_DL/StructureAna.hs:        -- TODO: check if gEmbed (Logic.Grothendieck) and G_morphism
7c8051ef91610c696bc9fa2e61ad1b153fbe7ce0Klaus LuettichGUI/ProofManagement.hs:  todo:
7c8051ef91610c696bc9fa2e61ad1b153fbe7ce0Klaus LuettichGUI/ProofManagement.hs:  -- TODO: do something with the resulting G_theory before returning it?
734a5ebd38032798f0ab908e2d52862c71b2c127Simon UlbrichtSPASS/DFGParser.hs:quantification s = do (ts',t') <- parens (do ts <- squares (commaSep1 term) -- todo: var binding should allow only simple terms
7c8051ef91610c696bc9fa2e61ad1b153fbe7ce0Klaus LuettichSPASS/PrintTPTP.hs:{- todo:
f9e0b18852b238ddb649d341194e05d7200d1bbeChristian MaederSPASS/Logic_SPASS.hs:         is_subsig SoftFOL = const $ const True -- TODO!!
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian MaederTaxonomy/MMiSSOntology.hs:   todo: add a new edge type for equivalence which should be visited only once
0e426c4d12afafe40a20b33ac4e7f3504296d945Jonathan von SchroederCommon/LaTeX_funs.hs:   TODO:
7c8051ef91610c696bc9fa2e61ad1b153fbe7ce0Klaus LuettichCommon/LaTeX_funs.hs:          -- TODO: Build a nice correction map
da955132262baab309a50fdffe228c9efe68251dCui Jian
7c8051ef91610c696bc9fa2e61ad1b153fbe7ce0Klaus Luettich************************************************
7c8051ef91610c696bc9fa2e61ad1b153fbe7ce0Klaus LuettichChristian
7c8051ef91610c696bc9fa2e61ad1b153fbe7ce0Klaus Luettich************************************************
7c8051ef91610c696bc9fa2e61ad1b153fbe7ce0Klaus Luettich
7c8051ef91610c696bc9fa2e61ad1b153fbe7ce0Klaus LuettichBitte auch aus folgenden Files die todo-Listen nach Trac verschieben:
7c8051ef91610c696bc9fa2e61ad1b153fbe7ce0Klaus Luettich
7c8051ef91610c696bc9fa2e61ad1b153fbe7ce0Klaus LuettichDriver/Options.hs:-- | 'Flattening' describes how flat the Earth really is (TODO: add comment)
1842453990fed8a1bd7a5ac792d7982c1d2bfcd5Christian MaederIsabelle/Logic_Isabelle.hs:         is_subsig Isabelle = const $ const True -- TODO!!
7c8051ef91610c696bc9fa2e61ad1b153fbe7ce0Klaus Luettich
8a6eb5a17ea17b650b29099036549b66eec4884aChristian Maeder************************************************
8a6eb5a17ea17b650b29099036549b66eec4884aChristian MaederTill
8a6eb5a17ea17b650b29099036549b66eec4884aChristian Maeder************************************************
46f27ca50ca6aa59e3c703b02ba0959e7b46ed34Christian Maeder
46f27ca50ca6aa59e3c703b02ba0959e7b46ed34Christian MaederBitte auch aus folgenden Files die todo-Listen nach Trac verschieben:
46f27ca50ca6aa59e3c703b02ba0959e7b46ed34Christian Maeder
46f27ca50ca6aa59e3c703b02ba0959e7b46ed34Christian MaederCASL/Morphism.hs:todo:
46f27ca50ca6aa59e3c703b02ba0959e7b46ed34Christian MaederCASL/SymbolMapAnalysis.hs:todo:
46f27ca50ca6aa59e3c703b02ba0959e7b46ed34Christian MaederCoCASL/Logic_CoCASL.hs:{- todo:
8a6eb5a17ea17b650b29099036549b66eec4884aChristian MaederCoCASL/StatAna.hs:{- todo:
8a6eb5a17ea17b650b29099036549b66eec4884aChristian MaederConstraintCASL/Logic_ConstraintCASL.hs:{- todo:
5607bbe40d1b360797381a83a6eae6773ee7cd2cChristian MaederConstraintCASL/StaticAna.hs:{- todo: check formulas -}
5607bbe40d1b360797381a83a6eae6773ee7cd2cChristian MaederCspCASL/Logic_CspCASL.hs:   todo:
5607bbe40d1b360797381a83a6eae6773ee7cd2cChristian MaederCspCASL/SignCSP.hs:-- todo:  implement isInclusion, computeExt
8a6eb5a17ea17b650b29099036549b66eec4884aChristian MaederCspCASL/StatAnaCSP.hs:{- todo:
3a6decfd748f532d5cb03fbcb7a42fa37b0faab3Christian MaederGUI/ConvertDevToAbstractGraph.hs:   todo:
8a6eb5a17ea17b650b29099036549b66eec4884aChristian MaederGUI/hets_cgi.hs:   todo:
8a6eb5a17ea17b650b29099036549b66eec4884aChristian MaederIsabelle/IsaPrint.hs:  todo: brackets in (? x . p x) ==> q
46f27ca50ca6aa59e3c703b02ba0959e7b46ed34Christian MaederIsabelle/IsaProve.hs:  todo: thy files in subdir, check of legal changes in thy file
46f27ca50ca6aa59e3c703b02ba0959e7b46ed34Christian MaederLogic/Grothendieck.hs:{- todo: somthing like the following...
46f27ca50ca6aa59e3c703b02ba0959e7b46ed34Christian MaederLogic/Prover.hs:{- todo:
46f27ca50ca6aa59e3c703b02ba0959e7b46ed34Christian MaederModal/Logic_Modal.hs:{- todo:
46f27ca50ca6aa59e3c703b02ba0959e7b46ed34Christian MaederPGIP/Utils.hs:{- todo: refactor getGoalList, extractGraphEdge, extractGraphLabeledEdge
46f27ca50ca6aa59e3c703b02ba0959e7b46ed34Christian MaederProofs/Automatic.hs:todo in general:
46f27ca50ca6aa59e3c703b02ba0959e7b46ed34Christian MaederProofs/Automatic.hs:{- todo: implement apply for GlobDecomp and Subsumption
46f27ca50ca6aa59e3c703b02ba0959e7b46ed34Christian MaederProofs/EdgeUtils.hs:{- todo: also treat conservativity proof status in computation of proof basis
41c4a11ab016002e5f4dd38f18f003a757afb2e8Christian MaederProofs/EdgeUtils.hs:    _ -> Right False  -- todo: also treat conservativity proof status
8a6eb5a17ea17b650b29099036549b66eec4884aChristian MaederProofs/Global.hs:todo for Jorina:
46f27ca50ca6aa59e3c703b02ba0959e7b46ed34Christian MaederProofs/HideTheoremShift.hs: todo: use compInclusion instead of compHomInclusion
46f27ca50ca6aa59e3c703b02ba0959e7b46ed34Christian MaederProofs/InferBasic.hs:todo:
46f27ca50ca6aa59e3c703b02ba0959e7b46ed34Christian MaederStatic/AnalysisArchitecture.hs:{-  todo:
46f27ca50ca6aa59e3c703b02ba0959e7b46ed34Christian MaederStatic/DevGraph.hs:todo:
46f27ca50ca6aa59e3c703b02ba0959e7b46ed34Christian MaederSyntax/Parse_AS_Structured.hs:   todo:
46f27ca50ca6aa59e3c703b02ba0959e7b46ed34Christian MaederCASL/Amalgamability.hs:TODO:
46f27ca50ca6aa59e3c703b02ba0959e7b46ed34Christian MaederCASL/Amalgamability.hs:                          -- TODO: generate proof obligations
8a6eb5a17ea17b650b29099036549b66eec4884aChristian MaederOMDoc/OMDocOutput.hs:  BUGS/TODO:
8a6eb5a17ea17b650b29099036549b66eec4884aChristian MaederOMDoc/Util.hs:-- TODO : this looks very slow...
abee46762c1663b85c6f18d934cd11df83828f6eChristian MaederPGIP/Command_Parser.hs:  TODO :
abee46762c1663b85c6f18d934cd11df83828f6eChristian MaederPGIP/Commands.hs: TODO :
abee46762c1663b85c6f18d934cd11df83828f6eChristian MaederProofs/InferBasic.hs:            -- TODO: Reimplement stuff
f56cdf11927c31495bae642a9eb383212c90ba61Christian MaederStatic/DevGraph.hs:                               dgl_type = GlobalDef, -- TODO: other type
f56cdf11927c31495bae642a9eb383212c90ba61Christian MaederStatic/DevGraph.hs:                               dgl_type = GlobalDef, -- TODO: other type
f56cdf11927c31495bae642a9eb383212c90ba61Christian MaederStatic/LogicStructured.hs:   TODO
8a6eb5a17ea17b650b29099036549b66eec4884aChristian MaederStatic/LogicStructured.hs:-- see TODO section for possible extensions for (isJust enc) and
46f27ca50ca6aa59e3c703b02ba0959e7b46ed34Christian MaederSyntax/Parse_AS_Architecture.hs:   TODO:
46f27ca50ca6aa59e3c703b02ba0959e7b46ed34Christian MaederSyntax/Parse_AS_Library.hs:   TODO:
46f27ca50ca6aa59e3c703b02ba0959e7b46ed34Christian Maeder