"Not" is no longer a definition

[helm.git] / helm / software / lambda-delta / text / txtParser.mly

diff --git a/helm/software/lambda-delta/text/txtParser.mly b/helm/software/lambda-delta/text/txtParser.mly
index b3c7037a35c9a4804cd0c878b70710058ce1a53a..6aafbb5517f01b1ec909f8b081995e75cd100edd 100644 (file)
--- 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 OPEN CLOSE GLOBAL 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.entity option * bool> entry
+   %type <Txt.command option * bool> entry
+
+   %nonassoc CP CB CA
+   %right WTO STO
 %%
    hash:
       |      {}
@@ -54,9 +57,19 @@
       | ID        { [$1]     }
       | ID CM ids { $1 :: $3 }
    ;
+   sort:
+      | ID    { None, $1    }
+      | IX ID { Some $1, $2 }
+   ;
+   sorts:
+      | sort          { [$1]     }
+      | sort CM sorts { $1 :: $3 }
+   ;
 
    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 }
@@ -75,34 +88,69 @@
       | 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 }
    ;
    
-   start: OPEN {} | CLOSE {} | GLOBAL {} | EOF {} ;
+   decl:
+      | DECL { T.Decl }
+      | AX   { T.Ax   }
+   ;
+   def:   
+      | DEF  { T.Def } 
+      | TH   { T.Th  }
+   ;
    xentity:
-      | OPEN ID                           { Some (T.Section (Some $2))                      }
-      | CLOSE                             { Some (T.Section None)                           }
-      | GLOBAL comment ID CN term         { Some (T.Global (false, $3, $2, $5))             }
-      | GLOBAL comment ID EQ term         { Some (T.Global (true, $3, $2, $5))              }
-      | GLOBAL comment ID EQ term CN term { Some (T.Global (true, $3, $2, T.Cast ($7, $5))) }
-      | EOF                               { None                                            }
-   ;
-  entry:
+      | GRAPH ID
+         { Some (T.Graph $2)                             }
+      | decl comment ID CN term
+         { Some (T.Entity ($1, $3, $2, $5))              }
+      | def comment ID EQ term
+         { 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                             
+         { Some (T.Section None)                         }
+      | SORTS sorts
+         { Some (T.Sorts $2)                             }
+      | EOF                               
+         { None                                          }
+   ;
+   start: 
+      | GRAPH {} | decl {} | def {} | GEN {} |
+      | REQ {} | OPEN {} | CLOSE {} | SORTS {} | EOF {}
+   ;
+   entry:
       | xentity       { $1, false }
       | xentity start { $1, true  }
    ;