documentation of the mapping of Hets/DG datatypes to the database

Symbols in this document:

[ ] means: Not done yet

[x] means: Done

[o] means: nothing to do - just an explanation

[-] means: partially done

[?] means: there is an open question

Hets - database

[o] LibEnv - need not be represented in the database

[x] instead, all contained (LibName,DGraph)s will be stored as Documents

[x] proceed from the leaves of the LibEnv graph to the top. Then each DGRef can be resolved.

[x] Note that the current Document is needed in all contained OMS and Mappings.

[x] call getLibDepRel in order to compute (and then store) dependency relation on Documents

(LibName,DGraph) - Document

[x] LibName: store version and both IRIs (one is the location, one is the id of the Document)

DGraph:

[o] globalAnnos - leave for later

[o] optLibDefn - leave for later

[o] globalEnv - leave for later

[-] dgBody - go through the graph and represent all nodes and edges, and these

link to the respective Document. Hence a DGraph can be recovered using all nodes and edges of a given Document

[o] currentBaseTheory - ignore

[o] refTree - leave for later

[o] specRoots - ignore

[o] nameMap - ignore

[o] archSpecDiags - leave for later

[o] getNewEdgeId - ignore

[o] allRefNodes - ignore

[x] sigMap - use it in order to index signatures of a document (avoid duplicates)

[?] thMap - use it in order to index OMS of a document (avoid duplicates)

optionally add association OMS -- Theory -- Sentence

[x] morMap - use it in order to index signature morphisms of a document (avoid duplicates)

[o] proofHistory - ignore

[o] redoHistory - ignore

[x] Range - Range [S]

[x] only two Pos are needed, and only one filename

[x] NodeName - NodeName

[o] xpath is caching information and can be ignored

[x] DGOrigin - OMSOrigin

[x] just an enumeration (additional data can be ignored)

[x] Conservativtiy - String (for Unknown, take the argument string)

[x] ConsStatus - ConsStatus represent 2x Conservativtiy, omit ThmLinkStatus

[-] (DGNodeLab,Node) - OMS (create a new OMS only if nodeInfo is a DGNode)

[x] note that Node is just an integer, pointing to a development graph node, aka OMS

[x] dgn_theory: the G_theory can be represented inline:

[x] gTheoryLogic, gTheorySign can be stored as Signature

[x] gTheorySyntax is stored as an assoication to Serialization

only fill the url, there can be one or none

[x] gTheorySignIdx, gTheorySelfIdx is the index of the theory in thMap above (use it to avoid duplicates)

[x] gTheorySens is stored as an assoication to Sentence. The proof info can be ignored

[o] globalTheory is caching information and can be ignored

[x] labelHasHiding should be represented

[x] labelHasFree should be represented

[x] dgn_nf pointer to OMS

[x] dgn_sigma :: Maybe GMorphism -- inclusion of signature into nf signature

[x] dgn_freenf pointer to OMS

[x] dgn_phi :: Maybe GMorphism -- morphism from signature to nffree signature

[x] nodeInfo respent directly:

[x] DGNode

[x] node_origin represent as enumeration

[x] node_cons_status repredent as ConsStatus

[x] DGRef - here, no new OMS needs be created. Instead, lookup the ref_node (pointer to OMS)

[o] nodeMod - can be ignored

[o] xnode - can be ignored

[o] dgn_lock - can be ignored

[o] (dgn_symbolpathlist - can be ignored)

[x] an OMS should also contain a pointer (association) to its Document, which can be obtained through the enclosing LibEnv

[x] G_theory - represented only as part of OMS

[x] G_sign - Signature

[x] gSignLogic the logic, store it

[x] gSign

[x] plainSign Store signature as XML string or JSON.

[x] nonImportedSymbols indicates whether a symbol has been imported or not. Store it using an association class SignatureSymbol

[x] gSignSelfIdx is the index of the signature in sigMap above (use it to avoid duplicates)

[x] (DGLinkLab,Node,Node) - Mapping

[x] dgl_morphism see GMorphism

[x] dgl_type - represent only the enumerations, ConsStatus: see above

[x] dgl_origin - use an enumeration

[x] dglPending - store

[o] dgl_id - ingore

[x] dglName - store

[x] MaybeNode - pointer to OMS

[x] should we use inheritance table or not?

[?] in case of EmptyNode create a new OMS with empty signature and given logic (if not existing yet) - make the target null at first

[?] each logic should point to an OMS with the empty signature over that logic (association from Logic to Signature) - Leave it out at first.

[x] GMorphism - SignatureMorphism

[x] gMorphismComor - store as LogicMapping

[o] gMorphismSign - ignore

[o] gMorphismSignIdx - ignore

[x] gMorphismMor - Store as XML string or JSON.

[x] gMorphismMorIdx - use it to eliminate duplicates, using morMap above

-----------------------

[x] Signature to JSON: Is the symbols function in ToJson the correct one?

anwer: yes

[x] There is no SymbolMapping in the schema.

use Logic.Logic.symmap_of

[ ] languageStandardizationStatus = "TODO" -- TODO: add to class Logic

create a ticket for till

[ ] languageDefinedBy = "registry" -- TODO: add to class Logic

leave it for till - #1753

[x] use options to determine Document Kind