diff options
Diffstat (limited to 'src-3.0/PGF')
| -rw-r--r-- | src-3.0/PGF/Data.hs | 23 |
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) |