Merge pull request #33 from VariantSync/benjamin/hierarchical-modules

Use hierarchical modules in the proofs subproject

Author: pmbittner

proofs/app/ExampleFeatures.hs

@@ -1,6 +1,6 @@
 module ExampleFeatures where
 
-import Propositions
+import Feature.Propositions
 
 fFire  = PVariable "Fire"
 fGrass = PVariable "Grass"

proofs/app/VariationTreeExamples.hs

@@ -3,10 +3,10 @@
 import Time
 import VariationTree
 import VariationDiff
-import PaperLabels
+import Labels.PaperLabels
 
-import Logic
-import Propositions
+import Feature.Logic
+import Feature.Propositions
 import ExampleFeatures
 import MainUtils
 

proofs/package.yaml

@@ -1,7 +1,7 @@
 name:                proofs
 version:             0.1.0.0
 github:              "githubuser/proofs"
-license:             BSD3
+license:             LGPL-3.0
 author:              "Author name here"
 maintainer:          "[email protected]"
 copyright:           "2021 Author name here"
@@ -28,8 +28,6 @@ dependencies:
 library:
   source-dirs:
     - src
-    - src/feature
-    - src/labels
 
 executables:
   proofs-exe:

proofs/src/feature/Logic.hs proofs/src/Feature/Logic.hsproofs/src/feature/Logic.hs renamed to proofs/src/Feature/Logic.hs

@@ -4,7 +4,7 @@ License: GNU LGPLv3
 Maintainer: [email protected]
 Type class for reasoning on 'Logic's.
 -}
-module Logic where
+module Feature.Logic where
 
 class Negatable f where
     -- | Negation of a logical formula.

proofs/src/feature/Propositions.hs proofs/src/Feature/Propositions.hsproofs/src/feature/Propositions.hs renamed to proofs/src/Feature/Propositions.hs

@@ -4,9 +4,9 @@ License: GNU LGPLv3
 Maintainer: [email protected]
 Definition and operations of propositional logic.
 -}
-module Propositions where
+module Feature.Propositions where
 
-import Logic
+import Feature.Logic
 import Data.List ( intercalate )
 
 -- | Sum type similar to a grammar for building propositional formulas.

proofs/src/labels/MinimalLabels.hs proofs/src/Labels/MinimalLabels.hsproofs/src/labels/MinimalLabels.hs renamed to proofs/src/Labels/MinimalLabels.hs

@@ -1,9 +1,9 @@
 {-# LANGUAGE GADTs #-}
 
-module MinimalLabels where
+module Labels.MinimalLabels where
 
 import VariationTree
-import Logic
+import Feature.Logic
 import Data.Maybe ( fromJust )
 
 data MinimalLabels f where
@@ -27,4 +27,4 @@ instance Comparable f => Eq (MinimalLabels f) where
     x == y = case (x, y) of
         (Artifact a, Artifact b) -> a == b
         (Mapping a, Mapping b) -> lequivalent a b
-        (_, _) -> False
+        (_, _) -> False

proofs/src/labels/PaperLabels.hs proofs/src/Labels/PaperLabels.hsproofs/src/labels/PaperLabels.hs renamed to proofs/src/Labels/PaperLabels.hs

@@ -1,10 +1,10 @@
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE StandaloneDeriving #-}
 
-module PaperLabels where
+module Labels.PaperLabels where
 
 import VariationTree
-import Logic
+import Feature.Logic
 import Data.Maybe ( fromJust )
 
 data PaperLabels f where

proofs/src/labels/WithElif.hs proofs/src/Labels/WithElif.hsproofs/src/labels/WithElif.hs renamed to proofs/src/Labels/WithElif.hs

@@ -1,10 +1,10 @@
 {-# LANGUAGE GADTs #-}
 
-module WithElif where
+module Labels.WithElif where
 
 import VariationTree
 import Data.Maybe (fromJust)
-import Logic
+import Feature.Logic
 
 data WithElif f where
     Artifact :: ArtifactReference -> WithElif f

proofs/src/proofs/Completeness.hs proofs/src/Proofs/Completeness.hsproofs/src/proofs/Completeness.hs renamed to proofs/src/Proofs/Completeness.hs

@@ -1,4 +1,4 @@
-module Completeness where
+module Proofs.Completeness where
 
 {-
 Definitions for fast lookup:
@@ -89,4 +89,4 @@ where
 Note that we cannot prove that all possible functions of type "VariationTree l f -> VariationTree l f -> VariationDiff l f" are valid diff as these functions could
 create any resulting diff (for example an empty diff). In fact, the above equalities are axioms any diff has to fulfill to be valid and we showed that there exists at
 least one valid diff.
--}
+-}

proofs/src/VariationDiff.hs

@@ -6,7 +6,7 @@ import Data.List ( intercalate )
 
 import VariationTree
 import Time
-import Logic
+import Feature.Logic
 
 type Delta l f = Either (VTNode l f) (VTEdge l f) -> DiffType