celf.grm

(*  Celf
 *  Copyright (C) 2008 Anders Schack-Nielsen and Carsten Schürmann
 *
 *  This file is part of Celf.
 *
 *  Celf 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 3 of the License, or
 *  (at your option) any later version.
 *
 *  Celf 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 Celf.  If not, see <http://www.gnu.org/licenses/>.
 *)

fun objs2spine objs =
	let fun o2s [] sp = sp
		  | o2s (ob::objs) sp = o2s objs (Syntax.TApp' (ob,sp))
	in o2s objs Syntax.TNil' end

fun getline (line, ch) = line

%%

%pos int * int

%name Clf

%term ID of string | TYPE | PI | COLON | DOT | UNDERSCORE | LOLLI | BACKLOLLI
	| AMPH | LCURLY | RCURLY | TENSOR | ONE | EXISTS | LAMBDA
	| LANGLE | RANGLE | COMMA | LET | EQUAL | IN | PROJLEFT | PROJRIGHT
	| LBRACKET | RBRACKET | ARROW | BACKARROW | LPAREN | RPAREN | EOF
	| QUERY | TRACE | EXEC
        | NUM of int | LPI | LEXISTS | AFFLOLLI | BACKAFFLOLLI | BANG | AFF 
        | APP
        | MODE | PLUS | MINUS | MINUSD

%nonterm Kind of Syntax.kind | AsyncType of Syntax.asyncType
	| UnifiedType of Parse.unifiedType
	| AtomicType of string * Syntax.obj list
	| Obj of Syntax.obj
	| ExpObj of Syntax.expObj
	| MonadObj of Syntax.monadObj | MonadObjPair of Syntax.monadObj * Syntax.monadObj
	| OPattern of Syntax.opattern | OPatternPair of Syntax.opattern * Syntax.opattern
	| TPattern of Syntax.tpattern | TPatternPair of Syntax.tpattern * Syntax.tpattern
	| Decl of Syntax.decl | DeclList of (int * Syntax.decl) list
	| Program of (int * Syntax.decl) list
	| Number of int | NumOpt of int option
        | ModeDecl of Syntax.modeDecl
        | OneMode of Syntax.mode
        | Id of string

%start Program

%nonassoc DOT
%left BACKLOLLI BACKARROW BACKAFFLOLLI
%right LOLLI ARROW AFFLOLLI
%right TENSOR AMPH
%nonassoc LPAREN LANGLE LAMBDA LCURLY ID UNDERSCORE
%nonassoc ONE LBRACKET PLUS MINUS
%left APP PROJLEFT PROJRIGHT BANG AFF
%nonassoc RPAREN

%verbose


%noshift EOF
%eop EOF

%%

Program :
	  DeclList ( DeclList )

DeclList :
	  Decl DeclList ( (getline Decl1left, Decl) :: DeclList )
	| Decl          ( [(getline Decl1left, Decl)] )

Decl :
	  Id COLON Kind DOT                        ( Syntax.ConstDecl(Id,0,Syntax.Ki Kind) )
	| Id COLON AsyncType DOT                   ( Syntax.ConstDecl(Id,0,Syntax.Ty AsyncType) )
	| Id COLON TYPE EQUAL AsyncType DOT        ( Syntax.TypeAbbrev(Id,AsyncType) )
	| Id COLON AsyncType EQUAL Obj DOT         ( Syntax.ObjAbbrev(Id,AsyncType,Obj) )
	| QUERY NumOpt NumOpt NumOpt Number AsyncType DOT
			( Syntax.Query(NumOpt1,NumOpt2,NumOpt3,Number,AsyncType) )
        | TRACE NumOpt UnifiedType DOT ( Syntax.Trace(NumOpt, Parse.unif2sync UnifiedType) )
        | EXEC NumOpt UnifiedType DOT ( Syntax.Exec(NumOpt, Parse.unif2sync UnifiedType) )
        | MODE Id ModeDecl DOT
                        ( Syntax.Mode(Id,NONE,ModeDecl) )
        | MODE Id LCURLY ModeDecl RCURLY ModeDecl DOT
                        ( Syntax.Mode(Id,SOME ModeDecl1, ModeDecl2) )

Id :      ID               ( ID )
        | PLUS             ( "+" )
        | MINUS            ( "-" )
        | MINUSD           ( "-D" )

ModeDecl :
          OneMode ModeDecl ( OneMode :: ModeDecl )
        |                  ( [] )

OneMode :
          PLUS  ( Syntax.Plus )
        | MINUS ( Syntax.Minus Syntax.Normal )
        | MINUSD ( Syntax.Minus Syntax.Destination )

Number :
	  ONE ( 1 )
	| NUM ( NUM )

NumOpt :
	  ONE    ( SOME 1 )
	| NUM    ( SOME NUM )
	| TENSOR ( NONE )

Kind :
	  TYPE                             ( Syntax.Type' )
	| PI Id COLON UnifiedType DOT Kind ( Syntax.KPi'(SOME Id,Parse.unif2async UnifiedType,Kind) )
	| UnifiedType ARROW Kind           ( Syntax.KPi'(NONE,Parse.unif2async UnifiedType,Kind) )
	| PI Id DOT Kind                   ( Syntax.KPi'(SOME Id,Syntax.newTVar(),Kind) )

AtomicType :
	  Id                          ( (Id,[]) )
	| AtomicType Obj %prec APP    ( let val (a,s) = AtomicType in (a,Obj::s) end )

AsyncType :
	  UnifiedType ( Parse.unif2async UnifiedType )

UnifiedType :
	  UnifiedType LOLLI UnifiedType           ( Parse.lolli(UnifiedType1,UnifiedType2) )
	| UnifiedType BACKLOLLI UnifiedType       ( Parse.lolli(UnifiedType2,UnifiedType1) )
	| UnifiedType AFFLOLLI UnifiedType        ( Parse.affLolli(UnifiedType1,UnifiedType2) )
	| UnifiedType BACKAFFLOLLI UnifiedType    ( Parse.affLolli(UnifiedType2,UnifiedType1) )
	| UnifiedType ARROW UnifiedType           ( Parse.arrow(UnifiedType1,UnifiedType2) )
	| UnifiedType BACKARROW UnifiedType       ( Parse.arrow(UnifiedType2,UnifiedType1) )
	| UnifiedType AMPH UnifiedType            ( Parse.addProd(UnifiedType1,UnifiedType2) )
	| PI Id COLON UnifiedType DOT UnifiedType ( Parse.tPi(Id,UnifiedType1,UnifiedType2) )
	| PI Id DOT UnifiedType                   ( Parse.tPi'(Id,UnifiedType) )
	| LPI TPattern COLON UnifiedType DOT UnifiedType
	                                          ( Parse.tLPi(TPattern,UnifiedType1,UnifiedType2) )
	| LCURLY UnifiedType RCURLY               ( Parse.monad UnifiedType )
	| AtomicType                              ( let val (a,s) = AtomicType
	                                            in Parse.Neg(Syntax.TAtomic'(a,objs2spine s)) end )
	| UnifiedType TENSOR UnifiedType          ( Parse.tensor(UnifiedType1,UnifiedType2) )
	| ONE                                     ( Parse.one )
	| EXISTS Id COLON UnifiedType DOT UnifiedType ( Parse.exists(Id,UnifiedType1,UnifiedType2) )
	| EXISTS Id DOT UnifiedType               ( Parse.exists'(Id,UnifiedType) )
	| LEXISTS TPattern COLON UnifiedType DOT UnifiedType
	                                          ( Parse.lexists(TPattern,UnifiedType1,UnifiedType2) )
	| AFF UnifiedType                         ( Parse.aff UnifiedType )
	| BANG UnifiedType                        ( Parse.bang UnifiedType )
	| LPAREN UnifiedType RPAREN               ( UnifiedType )

Obj :
	  LAMBDA OPattern COLON UnifiedType DOT Obj ( Parse.lamConstr(OPattern,UnifiedType,Obj) )
	| LAMBDA OPattern DOT Obj                ( Syntax.LLam'(OPattern,Obj) )
	| LANGLE Obj COMMA Obj RANGLE            ( Syntax.AddPair'(Obj1,Obj2) )
	| LCURLY ExpObj RCURLY                   ( Syntax.Monad' ExpObj )
	| Id                                     ( Parse.headToObj(Syntax.Const(Id)) )
	| Obj MonadObj %prec APP                 ( Parse.app(Obj,MonadObj) )
	| Obj PROJLEFT                           ( Parse.projLeft Obj )
	| Obj PROJRIGHT                          ( Parse.projRight Obj )
	| LPAREN Obj RPAREN                      ( Obj )
	| LPAREN Obj COLON AsyncType RPAREN      ( Syntax.Constraint'(Obj,AsyncType) )
	| UNDERSCORE                             ( Parse.blank() )

ExpObj :
	  LET LCURLY OPattern RCURLY EQUAL Obj IN ExpObj ( Parse.letredex(OPattern,Obj,ExpObj) )
	| MonadObj                                       ( Syntax.Mon'(MonadObj) )
	| LPAREN ExpObj RPAREN                           ( ExpObj )

MonadObj :
	  LBRACKET MonadObjPair RBRACKET ( Syntax.DepPair' MonadObjPair )
	| ONE                            ( Syntax.One' )
	| Obj %prec APP                  ( Syntax.Down'(Obj) )
	| AFF Obj                        ( Syntax.Affi'(Obj) )
	| BANG Obj                       ( Syntax.Bang'(Obj) )

MonadObjPair :
	  MonadObj COMMA MonadObjPair ( (MonadObj, Syntax.DepPair' MonadObjPair) )
	| MonadObj COMMA MonadObj     ( (MonadObj1, MonadObj2) )

OPattern :
	  ONE                            ( Syntax.POne' )
	| LBRACKET OPatternPair RBRACKET ( Syntax.PDepTensor' OPatternPair )
	| Id                             ( Syntax.PDown' Id )
	| AFF Id                         ( Syntax.PAffi' Id )
	| BANG Id                        ( Syntax.PBang' Id )
	| LPAREN OPattern RPAREN         ( OPattern )

OPatternPair :
	  OPattern COMMA OPatternPair ( (OPattern, Syntax.PDepTensor' OPatternPair) )
	| OPattern COMMA OPattern     ( (OPattern1, OPattern2) )

TPattern :
	  ONE                            ( Syntax.POne' )
	| LBRACKET TPatternPair RBRACKET ( Syntax.PDepTensor' TPatternPair )
	| UNDERSCORE                     ( Syntax.PDown' () )
	| AFF UNDERSCORE                 ( Syntax.PAffi' () )
	| BANG UNDERSCORE                ( Syntax.PBang' NONE )
	| BANG Id                        ( Syntax.PBang' (SOME Id) )
	| LPAREN TPattern RPAREN         ( TPattern )

TPatternPair :
	  TPattern COMMA TPatternPair ( (TPattern, Syntax.PDepTensor' TPatternPair) )
	| TPattern COMMA TPattern     ( (TPattern1, TPattern2) )