changing syntax of beta and phi

The erased portions now require {| |} instead of just { }
cedille · Jan 13, 2020 · 3e9579f · 3e9579f
1 parent 144e703
commit 3e9579f
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 2 deletions.
diff --git a/parser/src/CedilleLexer.x b/parser/src/CedilleLexer.x
@@ -43,6 +43,8 @@ token :-
       <0> \|                                    { mkTokenEmpty TPipe         }            
       <0> \{\^                                  { mkTokenEmpty TLSpan        }
       <0> \^\}                                  { mkTokenEmpty TRSpan        }
+      <0> \{\|                                  { mkTokenEmpty TLErased      }
+      <0> \|\}                                  { mkTokenEmpty TRErased      }
       <0> module                                { mkTokenEmpty TModule       }
       <0> import                                { mkTokenEmpty TImport       }
       <0> as                                    { mkTokenEmpty TAs           }
@@ -170,6 +172,8 @@ data TokenClass =
      |  TEpsRM    
      |  TLSpan     
      |  TRSpan
+     |  TLErased
+     |  TRErased
      |  TImport
      |  TAs
      |  TData          
@@ -207,6 +211,8 @@ instance Show TokenClass where
   show (TEpsRM)      = "TEpsRM"    
   show (TLSpan)      = "TLSpan"
   show (TRSpan)      = "TRSpan"
+  show (TLErased)    = "TLErased"
+  show (TRErased)    = "TRErased"
   show (TImport)     = "TImport"
   show (TAs)         = "TAs"
   show (TData)       = "TData"  

diff --git a/parser/src/CedilleParser.y b/parser/src/CedilleParser.y
@@ -50,6 +50,8 @@ import System.Environment
   'close'    { Token $$ TClose }
   '{^'       { Token $$ TLSpan }
   '^}'       { Token $$ TRSpan }
+  '{|'       { Token $$ TLErased }
+  '|}'       { Token $$ TRErased }
   'θ'        { Token $$ TTheta }
   'θ+'       { Token $$ TThetaEq }
   'θ<'       { Token $$ TThetaVars }
@@ -203,7 +205,7 @@ Nums :: { [CedilleTypes.Num] }
 
 OptTerm :: { Maybe PosTerm }
         :                               { Nothing }
-        | '{' Term '}'                  { Just (PosTerm $2 (pos2Txt1 $3)) }
+        | '{|' Term '|}'                  { Just (PosTerm $2 (pos2Txt1 $3)) }
 
 OptTermAngle :: { Maybe PosTerm }
           :                             { Nothing }
@@ -262,7 +264,7 @@ Term :: { Term }
      | 'open' Qvar '-' Term             { Open (pos2Txt $1) True (tPosTxt $2) (tTxt $2) $4 }
      | 'close' Qvar '-' Term            { Open (pos2Txt $1) False (tPosTxt $2) (tTxt $2) $4 }
      | 'ρ' OptPlus OptNums Lterm OptGuide '-' Term { Rho (pos2Txt $1) $2 $3 $4 $5 $7 }
-     | 'φ' Lterm '-' Term '{' Term '}'  { Phi (pos2Txt $1) $2 $4 $6 (pos2Txt1 $7) }
+     | 'φ' Lterm '-' Pterm '{|' Term '|}'  { Phi (pos2Txt $1) $2 $4 $6 (pos2Txt1 $7) }
      | 'χ' OptType '-' Term             { Chi (pos2Txt $1) $2 $4 }
      | 'δ' OptType '-' Term             { Delta (pos2Txt $1) $2 $4 }
      | Theta Lterm Lterms               { Theta (snd $1) (fst $1) $2 $3 }