summaryrefslogtreecommitdiff
path: root/src-3.0/PGF/Data.hs
diff options
context:
space:
mode:
authorkrasimir <krasimir@chalmers.se>2008-06-02 07:45:45 +0000
committerkrasimir <krasimir@chalmers.se>2008-06-02 07:45:45 +0000
commit7ee26238f59c76e8365f2db6217a3e25bd19ae00 (patch)
treeb35902f6708ccc20ad2ed35300e686e772da2721 /src-3.0/PGF/Data.hs
parentcd6fa423a92fcab89d5bb5d7a1c651fd2d8845d8 (diff)
Some more documentation
Diffstat (limited to 'src-3.0/PGF/Data.hs')
-rw-r--r--src-3.0/PGF/Data.hs23
1 files changed, 15 insertions, 8 deletions
diff --git a/src-3.0/PGF/Data.hs b/src-3.0/PGF/Data.hs
index 95ea2e1a7..95db1fedf 100644
--- a/src-3.0/PGF/Data.hs
+++ b/src-3.0/PGF/Data.hs
@@ -42,15 +42,18 @@ data Type =
DTyp [Hypo] CId [Exp]
deriving (Eq,Ord,Show)
+-- | An expression representing the abstract syntax tree
+-- in PGF. The same expression is used in the dependent
+-- types.
data Exp =
- EAbs [CId] Exp
- | EApp CId [Exp]
- | EStr String
- | EInt Integer
- | EFloat Double
- | EMeta Integer
- | EVar CId
- | EEq [Equation]
+ EAbs [CId] Exp -- ^ lambda abstraction. The list should contain at least one variable
+ | EApp CId [Exp] -- ^ application. Note that unevaluated lambda abstractions are not allowed
+ | EStr String -- ^ string constant
+ | EInt Integer -- ^ integer constant
+ | EFloat Double -- ^ floating point constant
+ | EMeta Integer -- ^ meta variable
+ | EVar CId -- ^ variable reference
+ | EEq [Equation] -- ^ lambda function defined as a set of equations with pattern matching
deriving (Eq,Ord,Show)
data Term =
@@ -79,6 +82,10 @@ data Hypo =
Hyp CId Type
deriving (Eq,Ord,Show)
+-- | The equation is used to define lambda function as a sequence
+-- of equations with pattern matching. The list of 'Exp' represents
+-- the patterns and the second 'Exp' is the function body for this
+-- equation.
data Equation =
Equ [Exp] Exp
deriving (Eq,Ord,Show)