]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/src/text/txtParser.mly
- ld-html-root: ported to permanent lambda-delta url
[helm.git] / helm / software / lambda-delta / src / text / txtParser.mly
index 1eae31980929ea9ab3295fc7ac972a027a8ef0a1..2c9abe0793115c8991eb3614236d16860348ddbd 100644 (file)
@@ -33,7 +33,7 @@
    %token <int> IX
    %token <string> ID STR
    %token OP CP OB CB OA CA FS CN CM EQ STAR HASH PLUS TE WTO STO CT
-   %token GRAPH DECL AX CONG DEF TH GEN REQ OPEN CLOSE SORTS EOF
+   %token GRAPH MAIN DECL AX CONG DEF TH GEN REQ OPEN CLOSE SORTS EOF
 
    %start entry
    %type <Txt.command option> entry
       |    {}
       | FS {}
    ;
+   main:
+      |      { false }
+      | MAIN { true  }
+   ;
    comment:
-      |     { "" }
-      | STR { $1 }
+      |         { "", "" }
+      | STR     { "", $1 }
+      | STR STR { $1, $2 }
    ;
    ids:
       | ID        { [$1]     }
    ;
    xentity:
       | GRAPH ID
-         { T.Graph $2                                 }
-      | decl level comment ID CN term
-         { T.Entity ($1, $2, $4, $3, $6)              }
-      | def level comment ID EQ term
-         { T.Entity ($1, $2, $4, $3, $6)              }
-      | def level comment ID EQ term CN term
-         { T.Entity ($1, $2, $4, $3, T.Cast ($8, $6)) }
+         { 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 {} |