module fndefgram.
accumulate lambdayacc, fndef.

non_terminal X :- member X [(fe A),(te B),(cl D),(dl F),(lamt G),(kep Z2),
			    (tep Z),(fm H),telparen,(idlst LS),tcomma].
ntnum 11.
terminal X :- 
  member X [lparen,rparen,(iconst V),(id S),(sconst St),negt,dott,
	      pit,sigmat,impt,impbyt,arrowt,kindt,typet,definitiont,slasht,
	      trutht,falset,fnmodt,comma,semicolon,succt,natt,ntt,zerot,formt].

%%% tokenizer declarations:
printname truth "true" trutht.
printname false "false" falset.
printname neg "not" negt.
printname and "," comma.
printname or ";" semicolon.
printname forall "pi" pit.
printname some "sigma" sigmat.
printname imp "=>" impt.
printname _ ":-" impbyt.
printname _ "(" lparen.
printname _ ")" rparen.
printname _ "\\" slasht.
printname _ "." dott.
printname _ "foldnmodule" fnmodt.
printname _ "definition" definitiont.
printname _ "type" typet.
printname _ "kind" kindt.
printname _ "->" arrowt.
printname _ "succ" succt.
printname _ "z" zerot.
printname _ "nat" natt.
printname _ "nt" ntt.
printname _ "o" formt.
% id, iconst, sconst are universal

start_symbol (fm X).  % parser returns definition of regular module

cfg
[ 
  rule ((fm D) ==> [definitiont,(id DMODNAME),dott,(dl Dl)]) 
			(D = fndefmod DMODNAME Dl),
  rule ((fm Fmod) ==> [fnmodt,(id Fmodname),dott, (dl Dfl)])
			(Fmod = fnmodule Fmodname Dfl),
  rule ((dl D1) ==> [cl C1]) (D1 = [C1]),
  rule ((dl D2) ==> [cl C2,dl D3]) (D2 = [C2|D3]),
  rule ((cl Cl1) ==> [(fe F1),dott]) (Cl1 = F1),
  rule ((cl Cl2) ==> [tep Names1,(te Type1),dott])
			(Cl2 = (typedef Names1 Type1)),
  rule ((cl Clk2) ==> [kep Namesk1,(te Kind1),dott])
			(Clk2 = (kinddef Namesk1 Kind1)),
  rule ((fe Fid) ==> [(id Iid)]) (Fid = (freevar Iid)),
  rule ((fe Fa) ==> [fe Fa1,fe Fa2]) (Fa = (Fa1 @ Fa2)),
  rule ((fe Fb) ==> [fe Fb1,comma,fe Fb2]) (Fb = (and @ Fb1 @ Fb2)),
  rule ((fe Fc) ==> [fe Fc1,semicolon,fe Fc2]) (Fc = (or @ Fc1 @ Fc2)),
  rule ((fe Fd) ==> [fe Fd1,impt,fe Fd2]) (Fb = (imp @ Fd1 @ Fd2)),
  rule ((fe Fe) ==> [fe Fe1,impbyt,fe Fe2]) (Fe = (impby @ Fe1 @ Fe2)),
  rule ((fe Fg) ==> [pit,lamt Fg1]) (Fg = (forall @ Fg1)),
  rule ((fe Fh) ==> [sigmat,lamt Fh1]) (Fh = (some @ Fh1)),
  rule ((fe Fi) ==> [lparen,fe Fi1,rparen]) (Fi = Fi1),
  rule ((fe L1) ==> [lamt L2]) (L1 = L2),
  rule ((lamt L) ==> [(id Lv),slasht,(fe Lb)])
			(formlam Lv Lb L),
  rule ((fe Ff) ==> [negt,fe Ff1]) (Ff = (neg @ Ff1)),
  rule ((fe Fj)  ==> [zerot])  (Fj = zero),
  rule ((fe Fk) ==> [succt])   (Fk = succ),
  rule ((fe Fl) ==> [natt])    (Fl = nat),
  rule ((fe Fm) ==> [trutht])  (Fm = truth),
  rule ((fe Fn) ==> [falset])  (Fn = false),
  rule ((tep N3) ==> [typet,(idlst N4)])  (N3 = N4),
  rule ((kep N5) ==> [kindt,(idlst N6)])  (N5 = N6),
  rule ((te Th) ==> [typet]) (Th = (typesym "type")),
  rule ((te Ta) ==> [(id Ta1)]) (Ta = (typesym Ta1)),
  rule ((te Tb) ==> [te Tb1,te Tb2]) (Tb = (tapp Tb1 Tb2)),
  rule ((te Tc) ==> [te Tc1,arrowt,te Tc2]) (Tc = (Tc1 arr Tc2)),
  rule ((te Td) ==> [telparen,te Td1,rparen]) (Td = Td1),
  rule (telparen ==> [lparen]) true,
  rule ((te Tf)  ==> [formt])   	(Tf = form),
  rule ((te Tg)  ==> [ntt])      	(Tg = nt),
  rule (tcomma ==> [comma]) true,
  rule ((idlst IDL1) ==> [id IDLa])	(IDL1 = [IDLa]),
  rule ((idlst IDL2) ==> [idlst IDL3,tcomma,id IDLb]) (IDL2 = [IDLb|IDL3])
].

% types and kinds are not distinguished at parse time.

binaryop arrowt (te A) (te B) "right" 6.  
binaryop comma (fe A) (fe B) "left" 5.
binaryop semicolon (fe A) (fe B) "left" 5.
binaryop impbyt (fe A) (fe B) "left" 7.     % less tighter than A
binaryop impt (fe A) (fe B) "right" 6.
implicitop (fe A) (fe B) "left" 3.  % application assoc's to left.
implicitop (te A) (te B) "left" 3.
unaryop negt (fe A) 4.		
unaryop slasht (fe A) 9.     % lambda terms have widest scope


% freshcopy : needed!
freshcopy (fe A) (fe B) :- !.
freshcopy (te A) (te B) :- !.
freshcopy (cl A) (cl B) :- !.
freshcopy (dl A) (dl B) :- !.
freshcopy (lamt A) (lamt B) :- !.
freshcopy (fm A) (fm B) :- !.
freshcopy (tep A) (tep B) :- !.
freshcopy (kep A) (kep B) :- !.
freshcopy (idlst A) (idlst B) :- !.
freshcopy T T.

% additional semantic action clauses:
formlam S B (abs S Ty L) :-
  pi x\ ((copy (freevar S) x :- !) => copy B (L x)).


% Post-parse processing of definitions and clauses:
% all capital letters interpreted as universals.
% validity of definitions checked after parsing

const X :- member X [truth,false,neg,and,or,imp,impby,forall,some,zero,succ,nat].
tconst X :- member X [nt,form,term].
tcopy X X :- tconst X.
tcopy (tapp T1 T2) (tapp T3 T4) :- tcopy T1 T3, tcopy T2 T4.
tcopy (T1 arr T2) (T3 arr T4) :- tcopy T1 T3, tcopy T2 T4.
tcopy (typesym S) (typesym S).

% makedef interprets a formula as a definition, quantifies over capitals.
%is_capitalized X :- Y is (string_to_int X), Y > 64, Y < 91.

%find_capitals X nil :- const X.
%find_capitals (freevar X) [X] :- is_capitalized X, !.
%find_capitals (freevar X) nil.
%find_capitals (T1 @ T2) C :- 
%  find_capitals T1 A, find_capitals T2 B, append A B C.
%find_capitals (abs S Ty T) C :-
%  pi x\ (find_capitals x nil => find_capitals (T x) C).

%makedef (impby @ A @ D) Def :- 
%   find_capitals (impby @ A @ D) Caps, form_def Caps A D Def.

% type inference needed here:
%form_def nil A D (A2 =^ D2) :- copy A A2, copy D D2.
%form_def [C|Cs] A D (alldef Ty Def) :-   
%  pi x\ ((copy (freevar C) x :- !) => form_def Cs A D (Defs x)).