FGrammar.gf 1.38 KB
Newer Older
jfschaefer's avatar
jfschaefer committed
1
2
-- abstract grammar for formulae
abstract FGrammar = MCats ** {
jfschaefer's avatar
jfschaefer committed
3
4
5
6
7
8
9
10
11
    cat
        FIdentifier;        -- identifier literals in formulae (e.g. "n")
        FNumeral;           -- numeral (e.g. "1")
        FBinRelation;       -- binary relations (e.g. "<")

        FComplexIdentifier; -- complex identifier in formuale (e.g. "x_1")
        FExpression;        -- expression
        FStatement;         -- statement

jfschaefer's avatar
jfschaefer committed
12
13
    fun
        fidentifier_to_fcomplexidentifier : FIdentifier -> FComplexIdentifier;    -- n -> mi ( n )
14
15
16
        fnumeral_to_fexpression : FNumeral -> FExpression;              -- 1 -> mn ( 1 )
        fcomplexidentifier_to_fexpression : FComplexIdentifier -> FExpression;
        fexpression_row : FExpression -> FExpression;
jfschaefer's avatar
jfschaefer committed
17

18
19
20
21
        apply_bin_rel : FBinRelation -> FExpression -> FExpression -> FStatement;


        fstatement_to_statement : FStatement -> Statement;
22
        fcomplexidentifier_to_identifer : FComplexIdentifier -> Identifier; -- mi ( n ) => $ mi ( cn ) $
23
24
        fcid_fbinrel_fexpr_to_identifier :                    -- introduces one identifier (like in 1 < n < 10)
            FComplexIdentifier -> FBinRelation -> FExpression -> Identifier;
25
26
        fexpr_fbinrel_fcid_fbinrel_fexpr_to_identifier :                    -- introduces one identifier (like in 1 < n < 10)
            FExpression -> FBinRelation -> FComplexIdentifier -> FBinRelation -> FExpression -> Identifier;
jfschaefer's avatar
jfschaefer committed
27
}