X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Ftext%2FtxtParser.mly;h=6aafbb5517f01b1ec909f8b081995e75cd100edd;hb=ab739c4972971725f59c52275a3257ebf524143f;hp=9812253819889dd6c25e9afd09bd1736081ad2d5;hpb=689118326fbe47231865b26c66ae89144459be6a;p=helm.git

diff --git a/helm/software/lambda-delta/text/txtParser.mly b/helm/software/lambda-delta/text/txtParser.mly
index 981225381..6aafbb551 100644
--- 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 GRAPH DECL AX DEF TH OPEN CLOSE SORTS EOF
+   %token OP CP OB CB OA CA FS CN CM EQ STAR HASH PLUS TE WTO STO 
+   %token GRAPH DECL AX DEF TH GEN REQ 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 term    { "", false, $2 }
+      | ID TE term { $1, false, $3 }
    ;
    abbr:
       | ID EQ term { $1, $3 }
@@ -83,21 +88,29 @@
       | ids   { T.Void $1 }
    ;      
    atom:
-      | STAR IX         { T.Sort $2       }
-      | STAR ID         { T.NSrt $2       }
-      | hash IX         { T.LRef ($2, 0)  }
-      | hash IX PLUS IX { T.LRef ($2, $4) }
-      | hash ID         { T.NRef $2       }
+      | STAR IX          { T.Sort $2         }
+      | STAR ID          { T.NSrt $2         }
+      | hash IX          { T.LRef ($2, 0)    }
+      | hash IX PLUS IX  { T.LRef ($2, $4)   }
+      | ID               { T.NRef $1         }
+      | HASH ID          { T.NRef $2         }
+      | atom OP term CP  { T.Inst ($1, [$3]) }
+      | atom OP terms CP { T.Inst ($1, $3)   }
    ;
    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 term CP fs term   { T.Appl ([$2], $5)          }
+      | OP terms CP fs term  { T.Appl ($2, $5)            }
+      | OB binder CB fs term { T.Bind ($2, $5)            }
+      | term WTO term        { T.Impl (false, "", $1, $3) }
+      | ID TE term WTO term  { T.Impl (false, $1, $3, $5) }
+      | term STO term        { T.Impl (true, "", $1, $3)  }
+      | ID TE term STO term  { T.Impl (true, $1, $3, $5)  }
+      | OP term CP           { $2                         }
    ;
    terms:
-      | term          { [$1]     }
+      | term CM term  { [$1; $3] }
       | term CM terms { $1 :: $3 }
    ;
    
@@ -118,6 +131,12 @@
          { Some (T.Entity ($1, $3, $2, $5))              }
       | def comment ID EQ term CN term
          { Some (T.Entity ($1, $3, $2, T.Cast ($7, $5))) }
+      | GEN term
+         { Some (T.Generate [$2])                        }
+      | GEN terms
+         { Some (T.Generate $2)                          }      
+      | REQ ids
+         { Some (T.Require $2)                           }
       | OPEN ID                           
          { Some (T.Section (Some $2))                    }
       | CLOSE                             
@@ -128,8 +147,8 @@
          { None                                          }
    ;
    start: 
-      | GRAPH {} | decl {} | def {} 
-      | OPEN {} | CLOSE {} | SORTS {} | EOF {}
+      | GRAPH {} | decl {} | def {} | GEN {} |
+      | REQ {} | OPEN {} | CLOSE {} | SORTS {} | EOF {}
    ;
    entry:
       | xentity       { $1, false }