- initial support for abstractions with explicit levels

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

diff --git a/helm/software/lambda-delta/src/text/txtParser.mly b/helm/software/lambda-delta/src/text/txtParser.mly
index 415b594ca7442f1ec7773cd53e51395325c231e7..1eae31980929ea9ab3295fc7ac972a027a8ef0a1 100644 (file)
--- 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 DECL AX CONG DEF TH GEN REQ OPEN CLOSE SORTS EOF
 
    %start entry
    %type <Txt.command option> entry
@@ -64,6 +65,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 +102,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 +121,7 @@
    decl:
       | DECL { T.Decl }
       | AX   { T.Ax   }
+      | CONG { T.Cong }
    ;
    def:   
       | DEF  { T.Def } 
@@ -123,25 +129,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                                 }
+      | 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)) }
       | 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 {} |