diff options
| author | krasimir <krasimir@chalmers.se> | 2008-06-02 07:45:45 +0000 |
|---|---|---|
| committer | krasimir <krasimir@chalmers.se> | 2008-06-02 07:45:45 +0000 |
| commit | 7ee26238f59c76e8365f2db6217a3e25bd19ae00 (patch) | |
| tree | b35902f6708ccc20ad2ed35300e686e772da2721 /src-3.0/PGF/Data.hs | |
| parent | cd6fa423a92fcab89d5bb5d7a1c651fd2d8845d8 (diff) | |
Some more documentation
Diffstat (limited to 'src-3.0/PGF/Data.hs')
| -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) |
