module twelf.
accum_sig lambdayacc.
accumulate lambdayacc.

comment_list
[
	"#","% ", "%%"
].


tokchar S :- alltyp S, C is string_to_int S, 
	     not (C = 46; C = 44; C = 41; C = 40; C = 91; C = 93; 
		  C = 58; C = 92; C = 34; C = 37; C = 123; C = 125).

terminal_list
[
	infixt, prefixt, postfixt, nonet, leftt, rightt,
	namet, queryt, solvet, modet, terminatest, theoremt,
	provet, rarrowt, larrowt, lbrace,rbrace,lbracket,
	rbracket,lparen,rparen,colon,period,
	eqlt,typet,comma,astrt,plust,minust, forallst,
	forallt,existst,truet,id A,sconst B,iconst C, establisht, assertt,uset
].

nonterm_list
[
	(ary1 defelf),(ary1 decls),(ary1 sigdecl),(ary1 decl),(ary1 term),
	(ary1 mode),(ary1 termin),(ary1 order),(ary1 orders),(ary1 marg),
	(ary1 idlist),(ary1 callpats),(ary1 callpat),(ary1 args),
	(ary1 mform),(ary1 pprove),(ary1 thdecl),
	(ary1 decs),(ary1 dec),(ary1 bound),(ary1 nonterminf),(ary1 nonterminfl),
	(ary1 nonterminfr),(ary1 nontermpre),(ary1 nontermpost),(ary1 nament),
	(ary1 interm),(ary2 intermpi),(ary0 telparen)
].

%%% Tokenizer declarations
printname _ "%infix" infixt.
printname _ "%prefix" prefixt.
printname _ "%postfix" postfixt.
printname _ "none" nonet.
printname _ "left" leftt.
printname _ "right" rightt.
printname _ "%name" namet.
printname _ "%query" queryt.
printname _ "%solve" solvet.
printname _ "%mode" modet.
printname _ "%terminates" terminatest.
printname _ "%theorem" theoremt.
printname _ "%prove" provet.
printname _ "%establish" establisht.
printname _ "%assert" assertt.
printname _ "%use" uset.
printname _ "->" rarrowt.
printname _ "<-" larrowt.
printname _ "{" lbrace.
printname _ "}" rbrace.
printname _ "[" lbracket.
printname _ "]" rbracket.
printname _ "(" lparen.
printname _ ")" rparen.
printname _ ":" colon.
printname _ "." period.
printname _ "," comma.
printname _ "=" eqlt.
printname _ "type" typet.
printname _ "*" astrt.
printname _ "+" plust.
printname _ "-" minust.
printname _ "forall" forallt.
printname _ "forall*" forallst.
printname _ "exists" existst.
printname _ "true" truet.

start_symbol (defelf A).

cfg
[

rule ((defelf ELFFILE) ==> [decls Declist]) (ELFFILE = Declist),
rule ((decls D1) ==> [sigdecl Decll1]) (D1 = [Decll1]),
rule ((decls D2) ==> [sigdecl Decll2,decls Dlist1]) (D2 = [Decll2|Dlist1]),

rule ((sigdecl SigDec) ==> [decl Clause,period]) (SigDec = Clause),

% Definitions
rule ((decl Termdef1) ==> [id String1,colon,term TTerm1]) (Termdef1 = defterm String1 TTerm1 noterm),
rule ((decl Termdef2) ==> [id String2,colon,term TTerm2,eqlt,term TTerm3]) (Termdef2 = defterm String2 TTerm2 TTerm3),
rule ((decl Termdef3) ==> [id String3,eqlt,term TTerm4]) (Termdef3 = defterm String3 TTerm4 noterm),

% Fixities
rule ((decl Fix1) ==> [nonterminf Prec1,(id String4)])  (Fix1 = fixify infn Prec1 String4),
rule ((nonterminf NINF) ==> [infixt,nonet,(iconst PrecINF1)]) ( NINF = PrecINF1),
rule ((decl Fix2) ==> [nonterminfl Prec2,(id String5)])  (Fix2 = fixify infl Prec2 String5),
rule ((nonterminfl NINF2) ==> [infixt,leftt,(iconst PrecINF2)]) ( NINF2 = PrecINF2),
rule ((decl Fix3) ==>[nonterminfr Prec3,(id String6)]) (Fix3 = fixify infr Prec3 String6),
rule ((nonterminfr NINF3) ==> [infixt,rightt,(iconst PrecINF3)]) ( NINF3 = PrecINF3),
rule ((decl Fix4) ==> [nontermpre Prec4,(id String7)])       (Fix4 = fixify pref Prec4 String7),
rule ((nontermpre NINF4) ==> [prefixt,(iconst PrecINF4)]) ( NINF4 = PrecINF4),
rule ((decl Fix5) ==> [nontermpost Prec5,(id String8)])      (Fix5 = fixify postf Prec5 String8),
rule ((nontermpost NINF5) ==> [postfixt,(iconst PrecINF5)]) ( NINF5 = PrecINF5),

% Name preference
rule ((decl Namepref1)  ==> [nament Name1,(id Name2)]) (Namepref1 = defname Name1 Name2),
rule ((nament Nament1)  ==> [namet,(id Nament2)]) (Nament1 = Nament2),
rule ((decl Querydecl1) ==> [queryt,bound Bound1,bound Bound2,term QTerm1]) (Querydecl1 = defquery Bound1 Bound2 "" QTerm1),
rule ((decl Querydecl2) ==> [queryt,bound Bound3,bound Bound4,(id Queryid),colon,term QTerm2]) (Querydecl2 = defquery Bound3 Bound4 Queryid QTerm2),

% Solve
rule ((decl Solve) ==> [solvet,(id Solvename),term Solveterm]) (Solve = defsolve Solvename Solveterm),

% Mode
rule ((decl Modedec) ==> [modet,mode Mode]) (Modedec = defmode Mode),
rule ((decl Modedec2) ==> [modet,id Modemd2]) (Modedec2 = defmode (decmode Modemd2 nil)),

% Terminates
rule ((decl Termindec) ==> [terminatest,termin Terminate]) (Termindec = defterminate Terminate),

% Theorem
rule ((decl Theoremdec) ==> [theoremt,thdecl Theorem]) (Theoremdec = deftheorem Theorem),

% Prove
rule ((decl Provedec) ==> [provet,pprove Prove]) (Provedec = defprove Prove),

% Establish
rule ((decl Estabdec) ==> [establisht,pprove Prove1]) (Estabdec = defestablish Prove1),

% Assert
rule ((decl Assertdec) ==> [assertt, callpats Assertcp]) (Assertdec = defassert Assertcp),

% Use
rule ((decl Usedec) ==> [uset, id UseID]) (Usedec = defuse UseID),

% Terms
rule ((term Term1)  ==> [typet]) (Term1 = typeterm),
rule ((term Term2)  ==> [idlist Freevar]) (termify Freevar Term2),
rule ((term Term3)  ==> [term ImpT1,rarrowt,term ImpT2]) (Term3 = (imp @ ImpT1 @ ImpT2)),
rule ((term Term4)  ==> [term ImpT3,larrowt,term ImpT4]) (Term4 = (imp @ ImpT4 @ ImpT3)),
rule ((term Term5)  ==> [term AppT1,term AppT2]) (Term5 = (AppT1 @ AppT2)),
rule ((term Term6)  ==> [term AscT1,colon,term AscT2]) (Term6 = (asc @ AscT1 @ AscT2)),
rule ((term Term8)  ==> [lbrace,(id Pi),colon,term Piterm,rbrace,term Piterm2]) ((formlam Pi Piterm2 Lamterm1),(Term8 = ((forall Pi Piterm) @ Lamterm1))),
rule ((term Term9)  ==> [intermpi Pi1a Piinterm,term Piterm3]) ((formlam Pi1a Piterm3 Lamterm2),(Term9 = ((forall Pi1a Piinterm) @ Lamterm2))),
rule ((term Term10) ==> [interm Iterm1,term Lamlamterm2]) (formlam Iterm1 Lamlamterm2 Lamterm3,Term10 = Lamterm3),
rule ((term Term12) ==> [telparen, term ParTerm1,rparen]) (Term12 = ParTerm1),

rule ((telparen) ==> [lparen]) (true),

rule ((interm Interm1) ==> [lbracket,(id Lambda),colon,term Lamterm,rbracket]) (Interm1 = Lambda),
rule ((interm Interm2) ==> [lbracket,(id Lambda2),rbracket]) (Interm2 = Lambda2),
rule ((intermpi Intermp1 Intermp1a) ==> [lbrace,(id Pi),colon,term Piterm,rbrace]) (Intermp1 = Pi,Intermp1a = Piterm),
rule ((intermpi Intermp2 Intermp2a) ==> [lbrace,(id Pi2),rbrace]) (Intermp1 = Pi2, Intermp2a = noterm),

% Bounds
rule ((bound Starbound) ==> [astrt]) (Starbound = starbound),
rule ((bound Intbound)  ==> [iconst Ibound]) (Intbound = ibound Ibound),

% Modes
rule ((mode Mode2)  ==> [(id ModeID2),mode ModeDec1]) (Mode2 = decmode ModeID2 [ModeDec1]),
rule ((mode Mode3)  ==> [mode ModeDecl2,mode ModeDecl3]) (Mode3 = modelist [ModeDecl2|[ModeDecl3]]),
rule ((mode Mode4)  ==> [plust,(id Modestr1)]) (Mode4 = modearg inmode Modestr1 noterm),
rule ((mode Mode4a) ==> [astrt,(id Modestr1a)]) (Mode4a = modearg bothmode Modestr1a noterm),
rule ((mode Mode5)  ==> [minust,(id Modestr2)]) (Mode5 = modearg outmode Modestr2 noterm),
rule ((mode Mode6)  ==> [astrt,lbrace,(id Modestr3),rbrace]) (Mode6 = modearg bothmode Modestr3 noterm),
rule ((mode Mode7)  ==> [plust,lbrace,(id Modestr4),rbrace]) (Mode7 = modearg inmode Modestr4 noterm),
rule ((mode Mode8)  ==> [minust,lbrace,(id Modestr5),rbrace]) (Mode8 = modearg outmode Modestr5 noterm),
rule ((mode Mode10) ==> [plust,lbrace,(id Modestr7),colon,term Modeterm1,rbrace]) (Mode10 = modearg inmode Modestr4 Modeterm1),
rule ((mode Mode11) ==> [minust,lbrace,(id Modestr8),colon,term Modeterm2, rbrace]) (Mode11 = modearg outmode Modestr5 Modeterm2),
rule ((mode Mode12) ==> [astrt,lbrace,(id Modestr9),colon,term Modeterm3, rbrace]) (Mode12 = modearg bothmode Modestr6 Modeterm3),
rule ((mode Mode13) ==> [mode Fullmode,term Fullmterm]) (Mode13 = decfmode Fullmterm Fullmode),

% Termiantes
rule ((termin Termin1) ==> [order Order, callpats CallPats]) (Termin1 = dectermin Order CallPats),

% Orders
rule ((orders Orders1) ==> [lparen]) (Orders1 = nil),
rule ((orders Orders2) ==> [order Orderol2,orders Ordersol1]) (Orders2 = [Ordersol2|Ordersol1]),

% Order
rule ((order Order1) ==> [marg Margo1]) (Order1 = Margo1),
rule ((order Order2) ==> [lbracket,orders Orderso1,rbracket]) (Order2 = listorder Orderso1),
rule ((order Order3) ==> [lbrace,orders Orderso2,rbrace]) (Order3 = listorder Orderso2),

% Marg
rule ((marg Marg1) ==> [id Idm1]) (Marg1 = makearg [Idm1]),
rule ((marg Marg2) ==> [lparen,idlist Idlm1,rparen]) (Marg2 = makearg Idlm1),

% Id List
rule ((idlist Idlist0) ==> [id IDTEST]) (Idlist0 = [IDTEST]),
rule ((idlist Idlist2) ==> [idlist Idlidl1, id Ididl2]) (append Idlidl1 [Ididl2] Idlist2),

% Callpats
rule ((callpats Callpats1) ==> [lparen,callpat Cpcps1,callpats Cpscps1]) (Callpats1 = [Cpcps1|Cpscps1]),
rule ((callpats Callpats0) ==> [lparen,callpat Cpcps2]) (Callpats0 = [Cpcps2]),

% Callpat
rule ((callpat Callpat1) ==> [id Idcp1,args Argscp1]) (Callpat1 = makecallpat Idcp1 Argscp1),

% Args
rule ((args Args2) ==> [rparen]) (Args2 = nil),
rule ((args Args1) ==> [id Idar1,args Argsa1]) (Args1 = [strarg Idar1|Argsa1]),

% Pprove
rule ((pprove Pprove1) ==> [iconst Icpr1,order Ordpr1,callpats Cpspr1]) (Pprove1 = provedec Icpr1 Ordpr1 Cpspr1),

% thdecl
rule ((thdecl Thdecl1) ==> [id Idtd1,colon,mform Mftd1]) (Thdecl1 = declth Idtd1 Mftd1),

% mform
rule ((mform Mform1) ==> [forallst,decs Decsmf1,mform Mfmf1]) (Mform1 = [mf forallstar Decsmf1|Mfmf1]),
rule ((mform Mform2) ==> [forallt,decs Decsmf2,mform Mfmf2]) (Mform2 = [mf forallq Decsmf2|Mfmf2]),
rule ((mform Mform3) ==> [existst,decs Decsmf3,mform Mfmf3]) (Mform3 = [mf exists Decsmf3|Mfmf3]),
rule ((mform Mform4) ==> [truet]) (Mform4 = [mf trueform nil]),

% decs
rule ((decs Decs1) ==> nil) (Decs1 = nil),
rule ((decs Decs2) ==> [dec Decdcs2,decs Decsdcs1]) (Decs2 = [Decdcs2|Decsdcs1]),

% dec
rule ((dec Dec1) ==> [lbrace,id Iddec1,colon,term Termdc1,rbrace]) (Dec1 = declare Iddec1 Termdc1),
rule ((dec Dec2) ==> [lbrace,id Iddec2,rbrace]) (Dec2 = declare Iddec2 noterm)

].

formlam S B (abs S L) :- pi x\ ((copy (freevar S) x :- !) => copy B (L x)).

% Copy Clause
copy X X :- const X.
copy (A @ B) (C @ D) :- copy A C, copy B D.
copy (abs Ps L) (abs Ps M) :- pi x\ (copy x x => (copy (L x) (M x))).

const X :- member X [freevar A, imp, asc, holeterm].

% Precedence and associativity
binaryop comma (term A) (term B) "left" 110.
binaryop rarrowt (term A) (term B) "left" 170.
binaryop colon (term A) (term B) "left" 180.
binaryop colon (id A) (term B) "left" 180.
binaryop larrowt (term A) (term B) "right" 130.
implicitop (term A) (term B) "left" 20.


% Turn a list of strings into a list of free variables
termify [Str] (freevar Str).
termify [Str|Rest] ((freevar Str) @ Rests) :- termify Rest Rests.