X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Ftext%2FtxtParser.mly;h=2c9abe0793115c8991eb3614236d16860348ddbd;hb=cb3e2526b3788172cf4a11e4c0082c12e8d233d0;hp=415b594ca7442f1ec7773cd53e51395325c231e7;hpb=39b42ed90bc74c8b6293842f1ac4aca60fc0c37e;p=helm.git

diff --git a/helm/software/lambda-delta/src/text/txtParser.mly b/helm/software/lambda-delta/src/text/txtParser.mly
index 415b594ca..2c9abe079 100644
--- a/helm/software/lambda-delta/src/text/txtParser.mly
+++ b/helm/software/lambda-delta/src/text/txtParser.mly
@@ -25,14 +25,15 @@
 
 %{
    module G = Options
+   module N = Level
    module T = Txt
    
    let _ = Parsing.set_trace !G.debug_parser
 %}
    %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 GEN REQ OPEN CLOSE SORTS EOF
+   %token OP CP OB CB OA CA FS CN CM EQ STAR HASH PLUS TE WTO STO CT
+   %token GRAPH MAIN DECL AX CONG DEF TH GEN REQ OPEN CLOSE SORTS EOF
 
    %start entry
    %type <Txt.command option> entry
@@ -48,9 +49,14 @@
       |    {}
       | FS {}
    ;
+   main:
+      |      { false }
+      | MAIN { true  }
+   ;
    comment:
-      |     { "" }
-      | STR { $1 }
+      |         { "", "" }
+      | STR     { "", $1 }
+      | STR STR { $1, $2 }
    ;
    ids:
       | ID        { [$1]     }
@@ -64,6 +70,10 @@
       | sort          { [$1]     }
       | sort CM sorts { $1 :: $3 }
    ;
+   level:
+      |       { N.infinite }
+      | CT IX { N.finite $2}
+   ;
 
    abst:
       | ID CN term { $1, true, $3  }
@@ -97,16 +107,16 @@
       | atom OP terms CP { T.Inst ($1, $3)   }
    ;
    term:
-      | 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                         }
+      | 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 level fs term { T.Bind ($4, $2, $6)            }
+      | term WTO level term        { T.Impl ($3, false, "", $1, $4) }
+      | ID TE term WTO level term  { T.Impl ($5, false, $1, $3, $6) }
+      | term STO level term        { T.Impl ($3, true, "", $1, $4)  }
+      | ID TE term STO level term  { T.Impl ($5, true, $1, $3, $6)  }
+      | OP term CP                 { $2                             }
    ;
    terms:
       | term CM term  { [$1; $3] }
@@ -116,6 +126,7 @@
    decl:
       | DECL { T.Decl }
       | AX   { T.Ax   }
+      | CONG { T.Cong }
    ;
    def:   
       | DEF  { T.Def } 
@@ -123,25 +134,25 @@
    ;
    xentity:
       | GRAPH ID
-         { T.Graph $2                             }
-      | decl comment ID CN term
-         { T.Entity ($1, $3, $2, $5)              }
-      | def comment ID EQ term
-         { T.Entity ($1, $3, $2, $5)              }
-      | def comment ID EQ term CN term
-         { T.Entity ($1, $3, $2, T.Cast ($7, $5)) }
+         { T.Graph $2                                     }
+      | main decl level comment ID CN term
+         { T.Entity ($1, $2, $3, $5, $4, $7)              }
+      | main def level comment ID EQ term
+         { T.Entity ($1, $2, $3, $5, $4, $7)              }
+      | main def level comment ID EQ term CN term
+         { T.Entity ($1, $2, $3, $5, $4, T.Cast ($9, $7)) }
       | GEN term
-         { T.Generate [$2]                        }
+         { T.Generate [$2]                                }
       | GEN terms
-         { T.Generate $2                          }      
+         { T.Generate $2                                  }      
       | REQ ids
-         { T.Require $2                           }
+         { T.Require $2                                   }
       | OPEN ID                           
-         { T.Section (Some $2)                    }
+         { T.Section (Some $2)                            }
       | CLOSE                             
-         { T.Section None                         }
+         { T.Section None                                 }
       | SORTS sorts
-         { T.Sorts $2                             }
+         { T.Sorts $2                                     }
    ;
    start: 
       | GRAPH {} | decl {} | def {} | GEN {} |