From 7ee26238f59c76e8365f2db6217a3e25bd19ae00 Mon Sep 17 00:00:00 2001 From: krasimir Date: Mon, 2 Jun 2008 07:45:45 +0000 Subject: Some more documentation --- src-3.0/PGF/Data.hs | 23 +++++++++++++++-------- 1 file changed, 15 insertions(+), 8 deletions(-) (limited to 'src-3.0/PGF') 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) -- cgit v1.2.3