X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Ftext%2FtxtParser.mly;fp=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Ftext%2FtxtParser.mly;h=0000000000000000000000000000000000000000;hb=95872555aaa040a22ad2d93cb1278f79e20da70c;hp=2c9abe0793115c8991eb3614236d16860348ddbd;hpb=4025c3f5b36025380dcad84bb7a97045d08652f6;p=helm.git

diff --git a/helm/software/lambda-delta/src/text/txtParser.mly b/helm/software/lambda-delta/src/text/txtParser.mly
deleted file mode 100644
index 2c9abe079..000000000
--- a/helm/software/lambda-delta/src/text/txtParser.mly
+++ /dev/null
@@ -1,164 +0,0 @@
-/* Copyright (C) 2000, HELM Team.
- * 
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- * 
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- * 
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA  02111-1307, USA.
- * 
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- */
-
-%{
-   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 CT
-   %token GRAPH MAIN DECL AX CONG DEF TH GEN REQ OPEN CLOSE SORTS EOF
-
-   %start entry
-   %type <Txt.command option> entry
-
-   %nonassoc CP CB CA
-   %right WTO STO
-%%
-   hash:
-      |      {}
-      | HASH {}
-   ;
-   fs:
-      |    {}
-      | FS {}
-   ;
-   main:
-      |      { false }
-      | MAIN { true  }
-   ;
-   comment:
-      |         { "", "" }
-      | STR     { "", $1 }
-      | STR STR { $1, $2 }
-   ;
-   ids:
-      | ID        { [$1]     }
-      | ID CM ids { $1 :: $3 }
-   ;
-   sort:
-      | ID    { None, $1    }
-      | IX ID { Some $1, $2 }
-   ;
-   sorts:
-      | sort          { [$1]     }
-      | sort CM sorts { $1 :: $3 }
-   ;
-   level:
-      |       { N.infinite }
-      | CT IX { N.finite $2}
-   ;
-
-   abst:
-      | ID CN term { $1, true, $3  }
-      | TE term    { "", false, $2 }
-      | ID TE term { $1, false, $3 }
-   ;
-   abbr:
-      | ID EQ term { $1, $3 }
-   ;
-   absts:
-      | abst          { [$1]     }
-      | abst CM absts { $1 :: $3 }
-   ;
-   abbrs:
-      | abbr          { [$1]     }
-      | abbr CM abbrs { $1 :: $3 }
-   ;   
-   binder: 
-      | absts { T.Abst $1 }
-      | abbrs { T.Abbr $1 }
-      | 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)   }
-      | 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 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] }
-      | term CM terms { $1 :: $3 }
-   ;
-   
-   decl:
-      | DECL { T.Decl }
-      | AX   { T.Ax   }
-      | CONG { T.Cong }
-   ;
-   def:   
-      | DEF  { T.Def } 
-      | TH   { T.Th  }
-   ;
-   xentity:
-      | GRAPH ID
-         { 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]                                }
-      | GEN terms
-         { T.Generate $2                                  }      
-      | REQ ids
-         { T.Require $2                                   }
-      | OPEN ID                           
-         { T.Section (Some $2)                            }
-      | CLOSE                             
-         { T.Section None                                 }
-      | SORTS sorts
-         { T.Sorts $2                                     }
-   ;
-   start: 
-      | GRAPH {} | decl {} | def {} | GEN {} |
-      | REQ {} | OPEN {} | CLOSE {} | SORTS {} | EOF {}
-   ;
-   entry:
-      | xentity start { Some $1 }
-      | EOF           { None    }
-   ;