Added license headers

spechub · Apr 19, 2023 · 0f67b7b · 0f67b7b
1 parent be1944d
commit 0f67b7b
Show file tree

Hide file tree

Showing 25 changed files with 139 additions and 0 deletions.
diff --git a/.gitignore b/.gitignore
@@ -25,6 +25,8 @@ doc/*.out
 doc/UserGuide.pdf
 doc/hs2isa.ps
 docs/
+__pycache__
+.idea
 programatica/
 OWL2/*.jar
 OWL2/java/build/

diff --git a/HetsAPI.hs b/HetsAPI.hs
@@ -1,3 +1,9 @@
+{- |
+Description :  Exports HETS functionality as a structured API
+Copyright   :  (c) Otto-von-Guericke University of Magdeburg
+License     :  GPLv2 or higher, see LICENSE.txt
+-}
+
 module HetsAPI (
     -- HetsAPI.Commands
     automatic

diff --git a/HetsAPI/Commands.hs b/HetsAPI/Commands.hs
@@ -1,3 +1,8 @@
+{- |
+Description :  All commands to interact with the HETS API
+Copyright   :  (c) Otto-von-Guericke University of Magdeburg
+License     :  GPLv2 or higher, see LICENSE.txt
+-}
 module HetsAPI.Commands (
    automatic
    , globalSubsume

diff --git a/HetsAPI/DataTypes.hs b/HetsAPI/DataTypes.hs
@@ -1,3 +1,8 @@
+{- |
+Description :  Common Datatypes used by the HETS API
+Copyright   :  (c) Otto-von-Guericke University of Magdeburg
+License     :  GPLv2 or higher, see LICENSE.txt
+-}
 module HetsAPI.DataTypes (
     Sentence
   , SentenceByName

diff --git a/HetsAPI/InfoCommands.hs b/HetsAPI/InfoCommands.hs
@@ -1,4 +1,10 @@
 {-# LANGUAGE ScopedTypeVariables #-}
+{- |
+Description :  Commands providing information about the state of the development graph and selected theories
+Copyright   :  (c) Otto-von-Guericke University of Magdeburg
+License     :  GPLv2 or higher, see LICENSE.txt
+-}
+
 
 module HetsAPI.InfoCommands (
      getGraphForLibrary

diff --git a/HetsAPI/Internal.hs b/HetsAPI/Internal.hs
@@ -1,3 +1,9 @@
+{- |
+Description :  This module aims to bundle all internals required to work with the API. The main reason is for the Python API to only import to modules.
+Copyright   :  (c) Otto-von-Guericke University of Magdeburg
+License     :  GPLv2 or higher, see LICENSE.txt
+-}
+
 module HetsAPI.Internal (
     fromJust
     , Result, resultToMaybe, Diagnosis

diff --git a/HetsAPI/ProveCommands.hs b/HetsAPI/ProveCommands.hs
@@ -1,3 +1,8 @@
+{- |
+Description :  All commands to prove or check the consistency of a theory, node or edge
+Copyright   :  (c) Otto-von-Guericke University of Magdeburg
+License     :  GPLv2 or higher, see LICENSE.txt
+-}
 module HetsAPI.ProveCommands (
     availableComorphisms
     , usableProvers

diff --git a/HetsAPI/Python.hs b/HetsAPI/Python.hs
@@ -1,3 +1,8 @@
+{- |
+Description :  HetsAPIs python interface. This module reexports all commands and functionality from the API and hides certain unsupported features from the python interface.
+Copyright   :  (c) Otto-von-Guericke University of Magdeburg
+License     :  GPLv2 or higher, see LICENSE.txt
+-}
 module HetsAPI.Python (
     PyTheory
     , PyComorphism

diff --git a/python/hets/Comorphism.py b/python/hets/Comorphism.py
@@ -1,3 +1,9 @@
+"""
+Description :  Represents `Logic.Comorphism`
+Copyright   :  (c) Otto-von-Guericke University of Magdeburg
+License     :  GPLv2 or higher, see LICENSE.txt
+"""
+
 from .haskell import getComorphismName, PyComorphism
 
 

diff --git a/python/hets/ConsistencyChecker.py b/python/hets/ConsistencyChecker.py
@@ -1,3 +1,8 @@
+"""
+Description :  Represents `Logic.Prover.ConsChecker`
+Copyright   :  (c) Otto-von-Guericke University of Magdeburg
+License     :  GPLv2 or higher, see LICENSE.txt
+"""
 from .haskell import getConsCheckerName, PyConsChecker
 
 class ConsistencyChecker:

diff --git a/python/hets/ConsistencyStatus.py b/python/hets/ConsistencyStatus.py
@@ -1,3 +1,9 @@
+"""
+Description :  Represents `Static.DgUtils.ConsStatus`
+Copyright   :  (c) Otto-von-Guericke University of Magdeburg
+License     :  GPLv2 or higher, see LICENSE.txt
+"""
+
 from .haskell import ConsStatus, showConsistencyStatus
 
 

diff --git a/python/hets/DevGraphEdge.py b/python/hets/DevGraphEdge.py
@@ -1,3 +1,9 @@
+"""
+Description :  Represents `Static.DevGraph.DGLinkLab`
+Copyright   :  (c) Otto-von-Guericke University of Magdeburg
+License     :  GPLv2 or higher, see LICENSE.txt
+"""
+
 from typing import Tuple, Optional
 
 from .haskell import DGLinkLab, fstOf3, sndOf3, thd

diff --git a/python/hets/DevGraphNode.py b/python/hets/DevGraphNode.py
@@ -1,3 +1,9 @@
+"""
+Description :  Represents `Static.DevGraph.DGNodeLab`
+Copyright   :  (c) Otto-von-Guericke University of Magdeburg
+License     :  GPLv2 or higher, see LICENSE.txt
+"""
+
 from typing import Tuple, Optional, List
 
 from .ConsistencyStatus import ConsistencyStatus

diff --git a/python/hets/DevelopmentGraph.py b/python/hets/DevelopmentGraph.py
@@ -1,3 +1,8 @@
+"""
+Description :  Represents `Static.DevGraph.DGraph`
+Copyright   :  (c) Otto-von-Guericke University of Magdeburg
+License     :  GPLv2 or higher, see LICENSE.txt
+"""
 from typing import List, Optional
 
 from .DevGraphNode import DevGraphNode

diff --git a/python/hets/HsWrapper.py b/python/hets/HsWrapper.py
@@ -1,3 +1,9 @@
+"""
+Description :  Defines a common base class for wrapped haskell elements
+Copyright   :  (c) Otto-von-Guericke University of Magdeburg
+License     :  GPLv2 or higher, see LICENSE.txt
+"""
+
 from typing import Generic, TypeVar, Optional
 
 

diff --git a/python/hets/Library.py b/python/hets/Library.py
@@ -1,3 +1,9 @@
+"""
+Description :  Represents `(Common.LibName.LibName, Static.DevGraph.LibEnv)`
+Copyright   :  (c) Otto-von-Guericke University of Magdeburg
+License     :  GPLv2 or higher, see LICENSE.txt
+"""
+
 from typing import Optional
 
 from .HsWrapper import HsWrapper, HsHierarchyElement

diff --git a/python/hets/ProofState.py b/python/hets/ProofState.py
@@ -1,3 +1,9 @@
+"""
+Description :  Represents `Proofs.AbstractState.ProofState`
+Copyright   :  (c) Otto-von-Guericke University of Magdeburg
+License     :  GPLv2 or higher, see LICENSE.txt
+"""
+
 from typing import List
 
 from .Sentence import Sentence

diff --git a/python/hets/ProofStatus.py b/python/hets/ProofStatus.py
@@ -1,3 +1,8 @@
+"""
+Description :  Represents `Logic.Prover.ProofStatus`
+Copyright   :  (c) Otto-von-Guericke University of Magdeburg
+License     :  GPLv2 or higher, see LICENSE.txt
+"""
 from .haskell import ProofStatus as ProofStatusHs, GoalStatus, TimeOfDay, TacticScript
 
 from typing import Any, List

diff --git a/python/hets/Prover.py b/python/hets/Prover.py
@@ -1,3 +1,9 @@
+"""
+Description :  Represents `Logic.Prover.Prover`
+Copyright   :  (c) Otto-von-Guericke University of Magdeburg
+License     :  GPLv2 or higher, see LICENSE.txt
+"""
+
 from typing import Optional, List
 
 from .haskell import getProverName, PyProver, PyComorphism

diff --git a/python/hets/Sentence.py b/python/hets/Sentence.py
@@ -1,3 +1,8 @@
+"""
+Description :  Represents `Logic.Logic.Sentences`
+Copyright   :  (c) Otto-von-Guericke University of Magdeburg
+License     :  GPLv2 or higher, see LICENSE.txt
+"""
 from typing import Tuple, Callable
 
 from .haskell import fst, snd, Sentence as PySentence

diff --git a/python/hets/Theory.py b/python/hets/Theory.py
@@ -1,3 +1,9 @@
+"""
+Description :  Represents `Static.GTheory.G_theory`
+Copyright   :  (c) Otto-von-Guericke University of Magdeburg
+License     :  GPLv2 or higher, see LICENSE.txt
+"""
+
 from typing import List, Optional, Tuple
 
 from .HsWrapper import HsHierarchyElement

diff --git a/python/hets/__init__.py b/python/hets/__init__.py
@@ -1,3 +1,9 @@
+"""
+Description :  Reexports all modules of the API
+Copyright   :  (c) Otto-von-Guericke University of Magdeburg
+License     :  GPLv2 or higher, see LICENSE.txt
+"""
+
 from .Comorphism import *
 from .ConsistencyChecker import *
 from .DevelopmentGraph import *

diff --git a/python/hets/haskell/__init__.py b/python/hets/haskell/__init__.py
@@ -1,5 +1,12 @@
+"""
+Description :  Python interface to the haskell API. Imports all functionionality through hyphen.
+Copyright   :  (c) Otto-von-Guericke University of Magdeburg
+License     :  GPLv2 or higher, see LICENSE.txt
+"""
+
 import hyphen
 
+# Some moules in a module hierachy do not exist in haskell. E.g. the module `Driver.Options` in python implies the existence of a module `Driver` which does not have to exist in python. Hence, these modules need to be marked explicitely empty
 hyphen.importing.FORCED_EMPTY += ["Driver", "Common", "Static", "Logic", "Proofs", "HetsAPI"]
 hyphen.importing.EXPECTED_EMPTY += ["Driver", "Common", "Static", "Logic", "Proofs", "HetsAPI"]
 

diff --git a/python/hets/haskell/__init__.pyi b/python/hets/haskell/__init__.pyi
@@ -1,3 +1,9 @@
+"""
+Description : Type hints for the python interface to the haskell API
+Copyright   :  (c) Otto-von-Guericke University of Magdeburg
+License     :  GPLv2 or higher, see LICENSE.txt
+"""
+
 from typing import Any, Tuple, TypeVar, Generic, List, Callable
 
 from .OMap import OMap

diff --git a/python/hets/result.py b/python/hets/result.py
@@ -1,3 +1,9 @@
+"""
+Description :  Provides utility functions to interact with `Common.Result.Result` instances
+Copyright   :  (c) Otto-von-Guericke University of Magdeburg
+License     :  GPLv2 or higher, see LICENSE.txt
+"""
+
 from typing import Any, TypeVar, Generic
 from .haskell import Result, resultToMaybe, fromJust, Just, show