search

spechub / Hets

The Heterogeneous Tool Set
http://hets.eu
GNU General Public License v2.0
57 stars 19 forks source link

development graph transformations for sending structured theories to provers #508

Open sternk opened 10 years ago

sternk commented 10 years ago

Reported by till and assigned to maeder Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/508

There are the following levels of support of structuring mechanisms:

  1. none
  2. imports without renaming
  3. non-disjoint unions
  4. imports with renaming
  5. hiding
  6. heterogeneity/comorphisms Implement functions for eliminating these features at the different levels.
  7. nothing to do
  8. use function computeTheory in spechub/Hets:Static/DGToSpec.hs
  9. have a look OMDoc output
  10. use function computeTheory in spechub/Hets:Static/DGToSpec.hs
  11. use normal form computation in spechub/Hets:Static/Proofs/TheoremHideShift.hs
  12. use something like function computeTheory in spechub/Hets:Static/DGToSpec.hs. However, only translations along comorphisms need to be considered. Using these functions, send a development graph or at least some structured theory to the provers, according to their abilities. Equip the prover data structure ProverTemplate in spechub/Hets:Logic/Prover.hs with data indicating provers' abilibties. For each level, realise translation functions translating away the features specific to this level:
libEnv_translation :: LibEnv -> Result LibEnv
dg_translation :: DGraph -> Result DGraph

similar to those in spechub/Hets:Static/DGTranslation.hs Start with translating away featues of level 2. Then, implement translating away featues of level 4.

sternk commented 10 years ago

Comment by maeder Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/508#comment:7

Igor doesn't know how to "send a development graph or at least some structured theory to the provers, according to their abilities". (And I think, that needs more discussion.) Currently, we can create one Isabelle theory file out of a single development graph node. Assuming we are going to create one Isabelle theory file for every node, we need to create "imports"-parts for inclusions. That is the translation of a single node needs to know the names of incomining nodes and the corresponding morphisms (if they are more than just an inclusions). Another problem is that the signature of an extension should translate only new signature elements and not those from incoming nodes. Maybe therefore a signature_difference method should be added to the class Logic (to be implemented by every Logic instance).

sternk commented 10 years ago

Comment by till Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/508#comment:8

It is easier to display the resulting development graph in a new window and forget about the proof history. Users want to keep the old DG anyway.

sternk commented 10 years ago

Comment by till Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/508#comment:9

Try to keep the structure of the libraries, such that reference nodes refering to nodes of other development graphs remain as they are (unless development graph links are completely flattened out).

sternk commented 10 years ago

Comment by maeder Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/508#comment:10

This needs to be finished (at least for VSE) until the end of January

sternk commented 10 years ago

Comment by maeder Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/508#comment:11

My last comment really applies to #311. The transformations are basically implemented (but may be improved).

sternk commented 10 years ago

Comment by maeder Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/508#comment:12

When flattening heterogeneity i.e. in spechub/Hets:VSE/test/List_Rev.casl the nodes are changed in the history, but do no need to change.

sternk commented 10 years ago

Comment by maeder Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/508#comment:13

"Proofs -> Flattening -> Disjoint unions" of spechub/Hets:VSE/test/List_Rev.casl creates one additional node. But the same operation after "Proofs -> Automatic" creates 11 additional nodes!

sternk commented 10 years ago

Comment by maeder Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/508#comment:14

"Proofs -> Flattening -> Heterogeneity" on spechub/Hets:VSE/test/Imports.casl moves the sentences from Nat into the local theory of List. This should not happen for structured proofs.

sternk commented 10 years ago

Comment by maeder Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/508#comment:15

Replying to maeder:

"Proofs -> Flattening -> Heterogeneity" on source:trunk/VSE/test/Imports.casl moves the sentences from Nat into the local theory of List. This should not happen for structured proofs.

This problem was fixed by spechub/Hets@d6ca60f1259d30c191869dce7ec2205ec60aeb37 (but leaves #735)

sternk commented 10 years ago

Comment by maeder Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/508#comment:16

I've created #769 and #770 from some comments above. A generic prover template (also see #311) for structured proofs is still missing. (Only VSE can be used for structured proofs, currently.)