Ling.cf

layout toplevel ;
layout "of" ;

comment "--" ;
comment "{-" "-}" ;

Prg. Program ::= [Dec] ;

token Name ( ["_"] (letter | ["-+*/%:=<>&|."] | digit)*
                   (letter | ["-+*/%:=<>&|."])
                   (letter | ["-+*/%:=<>&|.'"] | digit)*
             ["_"]
           | ["_"]
           | letter
             (letter | ["_-'"] | digit)*
           | digit
             (letter | ["_-'"] | digit)*
             letter
             (letter | ["_-'"] | digit)*
           );

-- This "new/"·Name
token NewName
  {"new/"} ( ["_"] (letter | ["-+*/%:=<>&|."] | digit)*
                   (letter | ["-+*/%:=<>&|."])
                   (letter | ["-+*/%:=<>&|.'"] | digit)*
             ["_"]
           | ["_"]
           | letter
             (letter | ["_-'"] | digit)*
           | digit
             (letter | ["_-'"] | digit)*
             letter
             (letter | ["_-'"] | digit)*
           );

token OpName
  ( (letter | ["-+*/%"] | digit)*
    ["-+*/%"]
    (letter | ["-+*/%_'"] | digit)*
  | (letter | ["-+*/%=<>&|"] | digit)*
    ["-+*/%=<>&|"]+
    (letter | ["-+*/%_=<>&|'"] | digit)*
  | ["-+*/%=<>&|."]* ["."] ["-+*/%=<>&|."]+
  | ["-+*/%=<>&|."]+ ["."]
  );

DDef. Dec ::= Name OptSig "=" Term ;
DSig. Dec ::= Name ":" Term ;
DDat. Dec ::= "data" Name "=" [ConName] ;

DAsr. Dec ::= "assert" Assertion ;

AEq. Assertion ::= Term "=" Term OptSig ;

CN. ConName ::= "`" Name ;

separator ConName "|" ;

NoSig. OptSig ::= ;
SoSig. OptSig ::= ":" Term ;

separator Dec "," ;

VD. VarDec ::= "(" Name OptSig ")" ;

CD. ChanDec ::= Name OptRepl OptSession ;

separator ChanDec "," ;

Br. Branch ::= ConName "->" Term ;

separator Branch "," ;

LInteger. Literal ::= Integer ;
LDouble.  Literal ::= Double  ;
LString.  Literal ::= String  ;
LChar.    Literal ::= Char    ;

-- Atomic terms
Var.     ATerm ::= Name ;
Op.      ATerm ::= OpName ;
Lit.     ATerm ::= Literal ;
Con.     ATerm ::= ConName ;
TTyp.    ATerm ::= "Type" ;
TProto.  ATerm ::= "<" [RSession] ">" ;
Paren.   ATerm ::= "(" Term OptSig ")" ;

-- Sessions
End.     ATerm ::= "end" ;
Par.     ATerm ::= "{"  [RSession]  "}" ;
Ten.     ATerm ::= "["  [RSession]  "]" ;
Seq.     ATerm ::= "[:" [RSession] ":]" ;

separator ATerm "" ;

RawApp.   Term3  ::= ATerm [ATerm] ;

Case.     Term2  ::= "case" Term "of" "{" [Branch] "}" ;
Snd.      Term2  ::= "!" Term3 CSession ;
Rcv.      Term2  ::= "?" Term3 CSession ;
Dual.     Term2  ::= "~" Term2 ;
TRecv.    Term2  ::= "<-" Name ;
_.        Term2  ::= Term3 ;

Loli.     Term1  ::= Term2 "-o" Term1 ;
-- WARNING: Dependent `->`/`**` (e.g. Π/Σ) are recognized afterwards.
-- Notice that `Term2` is used on the left of `->` and `**`.
-- In Ling.Reify this `Term2` is analysed:
-- If it matches against `("(" Name [Name] ":" Term ")")+` then this is a
-- dependent (`->`/`**`).
-- Otherwise it is considered as a *non* dependent `->`/`**`.
-- For instance `(Vec Int n : Type)-> F Vec Int n` is a dependent `->`
-- which introduces 3 types `Vec`, `Int`, and `n`, while
-- `(Vec Int 42 : Type)-> T` is single non-dependent `->` where `: Type` is
-- an annotation.
TFun.     Term1  ::= Term2 "->" Term1 ;
TSig.     Term1  ::= Term2 "**" Term1 ;
Let.      Term1  ::= "let" Name OptSig "=" Term "in" Term ;
_.        Term1  ::= Term2 ;

-- WARNING: The `Term2` is further analysed as: `("(" Name [Name] ":" Term ")")+`
Lam.      Term   ::= "\\" Term2 "->" Term ;
TProc.    Term   ::= "proc" "(" [ChanDec] ")" Proc ;
_.        Term   ::= Term1 ;

PAct.     Proc1 ::= Act ;
PPrll.    Proc1 ::= "(" [Proc] ")" ;
PRepl.    Proc1 ::= ReplKind "^" ATerm WithIndex Proc1 ;

PNxt.     Proc ::= Proc1 Proc ;
PDot.     Proc ::= Proc1 "." Proc ;
PSem.     Proc ::= Proc1 ";" Proc ;
_.        Proc ::= Proc1 ;
separator Proc "|" ;

ReplSeq.  ReplKind ::= "sequence" ;
ReplPar.  ReplKind ::= "parallel" ;

NoIndex.  WithIndex ::= ;
SoIndex.  WithIndex ::= "with" Name ;

Nu.       Act ::= NewAlloc ;
Split.    Act ::= Split ;
Send.     Act ::= "send" Name ATerm ;
NewSend.  Act ::= Name OptSession "<-" ATerm ;
Recv.     Act ::= "recv" Name VarDec ;
NewRecv.  Act ::= "let" Name OptSig "<-" Name ;
LetRecv.  Act ::= "let" Name OptSig "<=" ATerm ;
Ax.       Act ::= "fwd" ASession "(" [ChanDec] ")" ;
SplitAx.  Act ::= "fwd" Integer ASession Name ;
At.       Act ::= "@" ATerm TopCPatt ;
LetA.     Act ::= "let" Name OptSig "=" ATerm ;

AS.       ASession ::= ATerm ;

PatSplit. Split ::= "split" Name OptAs CPatt ;
ParSplit. Split ::= Name "{" [ChanDec] "}" ;
TenSplit. Split ::= Name "[" [ChanDec] "]" ;
SeqSplit. Split ::= Name "[:" [ChanDec] ":]" ;

NoAs. OptAs ::= ;
SoAs. OptAs ::= "as" ;

OldTopPatt. TopCPatt ::= "(" [ChanDec] ")" ;
ParTopPatt. TopCPatt ::= "{"  [CPatt]  "}" ;
TenTopPatt. TopCPatt ::= "["  [CPatt]  "]" ;
SeqTopPatt. TopCPatt ::= "[:" [CPatt] ":]" ;

ChaPatt.  CPatt ::= ChanDec ;
ParPatt.  CPatt ::= "{"  [CPatt]  "}" ;
TenPatt.  CPatt ::= "["  [CPatt]  "]" ;
SeqPatt.  CPatt ::= "[:" [CPatt] ":]" ;

separator CPatt "," ;

NoSession. OptSession ::= ;
SoSession. OptSession ::= ":" RSession ;

Repl. RSession ::= Term OptRepl ;
separator RSession "," ;

One.  OptRepl  ::= ;
Some. OptRepl  ::= "^" ATerm ;

Cont. CSession ::= "." Term1 ;
Done. CSession ::= ;

NoNewSig.   NewSig  ::= ;
NewTypeSig. NewSig  ::= ":*" Term ;
NewSessSig. NewSig  ::= ":" Term ;

TenNewPatt. NewPatt ::= "["  [CPatt]  "]" ;
SeqNewPatt. NewPatt ::= "[:" [CPatt] ":]" ;
CntNewPatt. NewPatt ::= "(" Name NewSig ")" ;

New.      NewAlloc ::= "new" NewPatt ;
NewSAnn.  NewAlloc ::= "new/" "(" Term OptSig ")" NewPatt ;
NewNAnn.  NewAlloc ::= NewName NewPatt ;