Browse Source

Restructure project

Nicolas Lenz 2 months ago
parent
commit
f9161736e5
5 changed files with 106 additions and 79 deletions
  1. 3
    0
      katrin.cabal
  2. 3
    78
      src/Katrin.hs
  3. 61
    0
      src/Katrin/Algebra.hs
  4. 37
    0
      src/Katrin/Core.hs
  5. 2
    1
      test/Main.hs

+ 3
- 0
katrin.cabal View File

@@ -4,7 +4,7 @@ cabal-version: 1.12
4 4
 --
5 5
 -- see: https://github.com/sol/hpack
6 6
 --
7
+-- hash: 8be90f2031d0309ad5effdfd1bccabf1108f825457ce34543279ee39e5ac9515
7 8
 
8 9
 name:           katrin
9 10
 version:        0.0.0
@@ -26,6 +26,8 @@ source-repository head
26 26
 library
27 27
   exposed-modules:
28 28
       Katrin
29
+      Katrin.Algebra
30
+      Katrin.Core
29 31
   other-modules:
30 32
       Paths_katrin
31 33
   hs-source-dirs:

+ 3
- 78
src/Katrin.hs View File

@@ -2,8 +2,10 @@
2 2
 
3 3
 module Katrin where
4 4
 
5
-import Prelude hiding (String)  -- so I don't accidentally use String instead of Text
5
+import Katrin.Core
6
+import Katrin.Algebra
6 7
 
8
+import Prelude hiding (String)  -- so I don't accidentally use String instead of Text
7 9
 import Data.Text (Text)
8 10
 import qualified Data.Text as Text
9 11
 
@@ -26,93 +28,6 @@ foldListExample :: Int
26 28
 foldListExample = foldList (ListAlg 0 (+)) (Cons 1 $ Cons 2 $ Cons 42 Nil)  -- = 1 + 2 + 42 = 45
27 29
 
28 30
 
29
-data Katrin = Katrin {typeDefs :: [TypeDef], defs :: [Def]} deriving (Show, Read, Eq)
30
-
31
-newtype ValueId = ValueId Text deriving (Show, Read, Eq)
32
-
33
-newtype ConstrId = ConstrId Text deriving (Show, Read, Eq)
34
-
35
-data TypeDef = TypeDef {
36
-    typeId :: ValueId,
37
-    typeExp :: TypeExp
38
-} deriving (Show, Read, Eq)
39
-
40
-data TypeExp = ProductType ConstrId [ValueId] | SumType TypeExp TypeExp
41
-    deriving (Show, Read, Eq)
42
-
43
-data Def = Def {
44
-    expId :: ValueId,
45
-    expType :: Exp,
46
-    exp :: Exp
47
-} deriving (Show, Read, Eq)
48
-
49
-data Exp =
50
-    Literal ConstrId
51
-    | Application {function :: Exp, argument :: Exp}
52
-    | Variable {symbol :: ValueId}
53
-    | Lambda {inPattern :: Exp, outExp :: Exp}
54
-    deriving (Show, Read, Eq)
55
-
56
-
57
-data KatrinAlg katrin valueId constrId typeDef def typeExp exp = KatrinAlg {
58
-    katrinAlg :: [typeDef] -> [def] -> katrin,
59
-    valueIdAlg :: Text -> valueId,
60
-    constrIdAlg :: Text -> constrId,
61
-    typeDefAlg :: valueId -> typeExp -> typeDef,
62
-    productTypeAlg :: constrId -> [valueId] -> typeExp,
63
-    sumTypeAlg :: typeExp -> typeExp -> typeExp,
64
-    defAlg :: valueId -> exp -> exp -> def,
65
-    literalAlg :: constrId -> exp,
66
-    applicationAlg :: exp -> exp -> exp,
67
-    variableAlg :: valueId -> exp,
68
-    lambdaAlg :: exp -> exp -> exp
69
-}
70
-
71
-
72
-foldKatrin :: KatrinAlg katrin valueId constrId typeDef def typeExp exp -> Katrin -> katrin
73
-foldKatrin alg (Katrin tds ds) = katrinAlg alg (foldTypeDef alg <$> tds) (foldDef alg <$> ds)
74
-
75
-foldValueId :: KatrinAlg katrin valueId constrId typeDef def typeExp exp -> ValueId -> valueId
76
-foldValueId alg (ValueId t) = valueIdAlg alg t
77
-
78
-foldConstrId :: KatrinAlg katrin valueId constrId typeDef def typeExp exp -> ConstrId -> constrId
79
-foldConstrId alg (ConstrId t) = constrIdAlg alg t
80
-
81
-foldTypeDef :: KatrinAlg katrin valueId constrId typeDef def typeExp exp -> TypeDef -> typeDef
82
-foldTypeDef alg (TypeDef vid te) = typeDefAlg alg (foldValueId alg vid) (foldTypeExp alg te)
83
-
84
-foldTypeExp :: KatrinAlg katrin valueId constrId typeDef def typeExp exp -> TypeExp -> typeExp
85
-foldTypeExp alg (ProductType cid vids) = productTypeAlg alg (foldConstrId alg cid) (foldValueId alg <$> vids)
86
-foldTypeExp alg (SumType te1 te2) = sumTypeAlg alg (foldTypeExp alg te1) (foldTypeExp alg te2)
87
-
88
-foldDef :: KatrinAlg katrin valueId constrId typeDef def typeExp exp -> Def -> def
89
-foldDef alg (Def vid e1 e2) = defAlg alg (foldValueId alg vid) (foldExp alg e1) (foldExp alg e2)
90
-
91
-foldExp :: KatrinAlg katrin valueId constrId typeDef def typeExp exp -> Exp -> exp
92
-foldExp alg (Literal cid) = literalAlg alg (foldConstrId alg cid)
93
-foldExp alg (Application e1 e2) = applicationAlg alg (foldExp alg e1) (foldExp alg e2)
94
-foldExp alg (Variable vid) = variableAlg alg (foldValueId alg vid)
95
-foldExp alg (Lambda e1 e2) = lambdaAlg alg (foldExp alg e1) (foldExp alg e2)
96
-
97
-
98
-katrinAlgTerm :: KatrinAlg Katrin ValueId ConstrId TypeDef Def TypeExp Exp
99
-katrinAlgTerm = KatrinAlg {
100
-    katrinAlg = Katrin, valueIdAlg = ValueId, constrIdAlg = ConstrId,
101
-    typeDefAlg = TypeDef, productTypeAlg = ProductType, sumTypeAlg = SumType,
102
-    defAlg = Def, literalAlg = Literal, applicationAlg = Application,
103
-    variableAlg = Variable, lambdaAlg = Lambda
104
-}
105
-
106 31
 
107 32
 -- | An example type definition for natural numbers.
108 33
 -- Corresponds to "data Nat = One | Succ Nat".

+ 61
- 0
src/Katrin/Algebra.hs View File

@@ -0,0 +1,61 @@
1
+module Katrin.Algebra (KatrinAlg, foldKatrin, katrinAlgTerm) where
2
+
3
+import Katrin.Core
4
+import Data.Text (Text)
5
+
6
+
7
+-- | Algebraic signature (or context-free grammar) for Katrin.
8
+data KatrinAlg katrin valueId constrId typeDef def typeExp exp = KatrinAlg {
9
+    katrinAlg :: [typeDef] -> [def] -> katrin,
10
+    valueIdAlg :: Text -> valueId,
11
+    constrIdAlg :: Text -> constrId,
12
+    typeDefAlg :: valueId -> typeExp -> typeDef,
13
+    productTypeAlg :: constrId -> [valueId] -> typeExp,
14
+    sumTypeAlg :: typeExp -> typeExp -> typeExp,
15
+    defAlg :: valueId -> exp -> exp -> def,
16
+    literalAlg :: constrId -> exp,
17
+    applicationAlg :: exp -> exp -> exp,
18
+    variableAlg :: valueId -> exp,
19
+    lambdaAlg :: exp -> exp -> exp
20
+}
21
+
22
+
23
+---- CATAMORPHIC FOLD FUNCTIONS FOR KATRIN ----
24
+
25
+foldKatrin :: KatrinAlg katrin valueId constrId typeDef def typeExp exp -> Katrin -> katrin
26
+foldKatrin alg (Katrin tds ds) = katrinAlg alg (foldTypeDef alg <$> tds) (foldDef alg <$> ds)
27
+
28
+foldValueId :: KatrinAlg katrin valueId constrId typeDef def typeExp exp -> ValueId -> valueId
29
+foldValueId alg (ValueId t) = valueIdAlg alg t
30
+
31
+foldConstrId :: KatrinAlg katrin valueId constrId typeDef def typeExp exp -> ConstrId -> constrId
32
+foldConstrId alg (ConstrId t) = constrIdAlg alg t
33
+
34
+foldTypeDef :: KatrinAlg katrin valueId constrId typeDef def typeExp exp -> TypeDef -> typeDef
35
+foldTypeDef alg (TypeDef vid te) = typeDefAlg alg (foldValueId alg vid) (foldTypeExp alg te)
36
+
37
+foldTypeExp :: KatrinAlg katrin valueId constrId typeDef def typeExp exp -> TypeExp -> typeExp
38
+foldTypeExp alg (ProductType cid vids) = productTypeAlg alg (foldConstrId alg cid) (foldValueId alg <$> vids)
39
+foldTypeExp alg (SumType te1 te2) = sumTypeAlg alg (foldTypeExp alg te1) (foldTypeExp alg te2)
40
+
41
+foldDef :: KatrinAlg katrin valueId constrId typeDef def typeExp exp -> Def -> def
42
+foldDef alg (Def vid e1 e2) = defAlg alg (foldValueId alg vid) (foldExp alg e1) (foldExp alg e2)
43
+
44
+foldExp :: KatrinAlg katrin valueId constrId typeDef def typeExp exp -> Exp -> exp
45
+foldExp alg (Literal cid) = literalAlg alg (foldConstrId alg cid)
46
+foldExp alg (Application e1 e2) = applicationAlg alg (foldExp alg e1) (foldExp alg e2)
47
+foldExp alg (Variable vid) = variableAlg alg (foldValueId alg vid)
48
+foldExp alg (Lambda e1 e2) = lambdaAlg alg (foldExp alg e1) (foldExp alg e2)
49
+
50
+
51
+---- ALGEBRAS FOR KATRIN ----
52
+
53
+-- | Term algebra for Katrin. `foldKatrin katrinAlgTerm` folds a Katrin term into a, well, Katrin term.
54
+-- Useful for compilation into a Katrin term and for testing.
55
+katrinAlgTerm :: KatrinAlg Katrin ValueId ConstrId TypeDef Def TypeExp Exp
56
+katrinAlgTerm = KatrinAlg {
57
+    katrinAlg = Katrin, valueIdAlg = ValueId, constrIdAlg = ConstrId,
58
+    typeDefAlg = TypeDef, productTypeAlg = ProductType, sumTypeAlg = SumType,
59
+    defAlg = Def, literalAlg = Literal, applicationAlg = Application,
60
+    variableAlg = Variable, lambdaAlg = Lambda
61
+}

+ 37
- 0
src/Katrin/Core.hs View File

@@ -0,0 +1,37 @@
1
+module Katrin.Core where
2
+
3
+import Data.Text (Text)
4
+
5
+
6
+-- | Main data type for a Katrin library consisting of a list of type definitions and a list of definitions.
7
+data Katrin = Katrin {typeDefs :: [TypeDef], defs :: [Def]} deriving (Show, Read, Eq)
8
+
9
+-- | Type for an identifier of a value, like an integer, a function, a type etc.
10
+newtype ValueId = ValueId Text deriving (Show, Read, Eq)
11
+
12
+-- | Type for an identifier of a constructor.
13
+newtype ConstrId = ConstrId Text deriving (Show, Read, Eq)
14
+
15
+-- | A type definition, consisting of an identifier for the type and the corresponding type expression.
16
+data TypeDef = TypeDef {
17
+    typeId :: ValueId,
18
+    typeExp :: TypeExp
19
+} deriving (Show, Read, Eq)
20
+
21
+-- | A type expression, consisting of stuff.
22
+-- TODO explain that. I'm too lazy right now.
23
+data TypeExp = ProductType ConstrId [ValueId] | SumType TypeExp TypeExp
24
+    deriving (Show, Read, Eq)
25
+
26
+data Def = Def {
27
+    expId :: ValueId,
28
+    expType :: Exp,
29
+    exp :: Exp
30
+} deriving (Show, Read, Eq)
31
+
32
+data Exp =
33
+    Literal ConstrId
34
+    | Application {function :: Exp, argument :: Exp}
35
+    | Variable {symbol :: ValueId}
36
+    | Lambda {inPattern :: Exp, outExp :: Exp}
37
+    deriving (Show, Read, Eq)

+ 2
- 1
test/Main.hs View File

@@ -3,7 +3,8 @@ module Main where
3 3
 import Test.Tasty
4 4
 import Test.Tasty.QuickCheck
5 5
 import Test.QuickCheck.Instances
6
-import Katrin
6
+import Katrin.Core
7
+import Katrin.Algebra
7 8
 import Data.Text
8 9
 
9 10
 main :: IO ()

Loading…
Cancel
Save