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

diff --git a/helm/software/lambda-delta/text/txtParser.mly b/helm/software/lambda-delta/text/txtParser.mly
index ee995aa2d..6aafbb551 100644
--- a/helm/software/lambda-delta/text/txtParser.mly
+++ b/helm/software/lambda-delta/text/txtParser.mly
@@ -33,12 +33,12 @@
    %token <int> IX
    %token <string> ID STR
    %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
+   %token GRAPH DECL AX DEF TH GEN REQ OPEN CLOSE SORTS EOF
 
    %start entry
    %type <Txt.command option * bool> entry
 
-   %nonassoc CP CB CA 
+   %nonassoc CP CB CA
    %right WTO STO
 %%
    hash:
@@ -67,9 +67,9 @@
    ;
 
    abst:
-      | ID CN term    { $1, true, $3  }
-      | TE CN term    { "", false, $3 }
-      | TE ID CN term { $2, false, $4 }
+      | ID CN term { $1, true, $3  }
+      | TE term    { "", false, $2 }
+      | ID TE term { $1, false, $3 }
    ;
    abbr:
       | ID EQ term { $1, $3 }
@@ -88,27 +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.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)  }
+      | 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 }
    ;
    
@@ -129,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                             
@@ -139,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 }