diff options
| author | aarne <aarne@cs.chalmers.se> | 2007-10-05 09:02:47 +0000 |
|---|---|---|
| committer | aarne <aarne@cs.chalmers.se> | 2007-10-05 09:02:47 +0000 |
| commit | 945a49214bd49fb082e8f613fc68d192a1b38743 (patch) | |
| tree | 4d6582426ea0bb5458b12a74a1c7c86fc0981553 /src/GF/GFCC/GFCC.cf | |
| parent | cc104236df63dafebaf87612aa379156cf914063 (diff) | |
cleaned up new GFCC, but added RP as deprecated
Diffstat (limited to 'src/GF/GFCC/GFCC.cf')
| -rw-r--r-- | src/GF/GFCC/GFCC.cf | 19 |
1 files changed, 10 insertions, 9 deletions
diff --git a/src/GF/GFCC/GFCC.cf b/src/GF/GFCC/GFCC.cf index 4ecf7e942..23ee38e58 100644 --- a/src/GF/GFCC/GFCC.cf +++ b/src/GF/GFCC/GFCC.cf @@ -26,8 +26,8 @@ Cat. CatDef ::= CId "[" [Hypo] "]" ; Fun. FunDef ::= CId ":" Type "=" Exp ; Lin. LinDef ::= CId "=" Term ; -Typ. Type ::= [CId] "->" CId ; -- context-free type -Tr. Exp ::= "(" Atom [Exp] ")" ; -- context-free term +DTyp. Type ::= "[" [Hypo] "]" CId [Exp] ; -- dependent type +DTr. Exp ::= "[" "(" [CId] ")" Atom [Exp] "]" ; -- term with bindings AC. Atom ::= CId ; AS. Atom ::= String ; @@ -51,6 +51,8 @@ KP. Tokn ::= "[" "pre" [String] "[" [Variant] "]" "]" ; Var. Variant ::= [String] "/" [String] ; +RP. Term ::= "(" Term "@" Term ")"; -- DEPRECATED: record parameter alias + terminator Concrete ";" ; terminator Flag ";" ; terminator CatDef ";" ; @@ -64,16 +66,15 @@ separator Variant "," ; token CId (('_' | letter) (letter | digit | '\'' | '_')*) ; + -- the following are needed if dependent types or HOAS or defs are present -Hyp. Hypo ::= CId ":" Type ; -DTyp. Type ::= "[" [Hypo] "]" CId [Exp] ; -- dependent type -DTr. Exp ::= "[" "(" [CId] ")" Atom [Exp] "]" ; -- term with bindings -AV. Atom ::= "$" CId ; +Hyp. Hypo ::= CId ":" Type ; +AV. Atom ::= "$" CId ; -EEq. Exp ::= "{" [Equation] "}" ; -- list of pattern eqs; primitive notion: [] -Equ. Equation ::= [Exp] "->" Exp ; -- patterns are encoded as exps +EEq. Exp ::= "{" [Equation] "}" ; -- list of pattern eqs; primitive: [] +Equ. Equation ::= [Exp] "->" Exp ; -- patterns are encoded as exps -terminator Hypo ";" ; +separator Hypo "," ; terminator Equation ";" ; |