- we added some syntactic sugar in the text parser

[helm.git] / helm / software / lambda-delta / text / txtParser.mly

diff --git a/helm/software/lambda-delta/text/txtParser.mly b/helm/software/lambda-delta/text/txtParser.mly
index 9812253819889dd6c25e9afd09bd1736081ad2d5..ee995aa2d140e88224b93b07b096cff4449c5f31 100644 (file)
--- a/helm/software/lambda-delta/text/txtParser.mly
+++ b/helm/software/lambda-delta/text/txtParser.mly
@@ -32,11 +32,14 @@
 %}
    %token <int> IX
    %token <string> ID STR
-   %token OP CP OB CB OA CA FS CN CM EQ STAR HASH PLUS
+   %token OP CP OB CB OA CA FS CN CM EQ STAR HASH PLUS TE WTO STO 
    %token GRAPH DECL AX DEF TH OPEN CLOSE SORTS EOF
 
    %start entry
    %type <Txt.command option * bool> entry
+
+   %nonassoc CP CB CA 
+   %right WTO STO
 %%
    hash:
       |      {}
@@ -64,7 +67,9 @@
    ;
 
    abst:
-      | ID CN term { $1, $3 }
+      | ID CN term    { $1, true, $3  }
+      | TE CN term    { "", false, $3 }
+      | TE ID CN term { $2, false, $4 }
    ;
    abbr:
       | ID EQ term { $1, $3 }
@@ -90,11 +95,17 @@
       | hash ID         { T.NRef $2       }
    ;
    term:
-      | atom                 { $1                       }
-      | OA term CA fs term   { T.Cast ($2, $5)          }
-      | OP terms CP fs term  { T.Appl ($2, $5)          }
-      | atom OP terms CP     { T.Appl (List.rev $3, $1) }
-      | OB binder CB fs term { T.Bind ($2, $5)          }
+      | atom                   { $1                         }
+      | OA term CA fs term     { T.Cast ($2, $5)            }
+      | OP terms CP fs term    { T.Appl ($2, $5)            }
+      | atom OP terms CP       { T.Inst ($1, $3)            }
+      | OB binder CB fs term   { T.Bind ($2, $5)            }
+      | term WTO term          { T.Impl (false, "", $1, $3) }
+      | TE CN term WTO term    { T.Impl (false, "", $3, $5) }
+      | TE ID CN term WTO term { T.Impl (false, $2, $4, $6) }
+      | term STO term          { T.Impl (true, "", $1, $3)  }
+      | TE CN term STO term    { T.Impl (true, "", $3, $5)  }
+      | TE ID CN term STO term { T.Impl (true, $2, $4, $6)  }
    ;
    terms:
       | term          { [$1]     }