consistencycheck

catom(A) :- (atom(A) -> true; error('atom expected:',A)).

check_labels([],_,_).

check_labels([label(L)|Rest],Labels,Expr) :-
    !,(member(L,Labels) ->
    !,check_labels(Rest,Labels,Expr);
    (atom_concat('label not present: ',L,Msg),
    error(Msg,Expr))).

check_labels([nlabel(L)|Rest],Labels,Expr) :-
    !,(member(L,Labels) ->
    (!,atom_concat('label present: ',L,Msg),
    error(Msg,Expr));
    check_labels(Rest,Labels,Expr)).

check_labels([Assertion|_],_,Expr) :-
    atom_concat('unmatched assertion: ',Assertion,Msg),
    error(Msg,Expr).

check_z_structure(Z,Comment,Assertions) :- check_z_substructure(Z,list(top),Comment,Assertions).

check_z_structuret(Z,Comment,Assertions) :- check_z_substructuret(Z,list(top),Comment,Assertions).

check_z_substructure(Z,Pos,Comment,Assertions) :- checkzstr(Z,untyped,Pos,Comment,Assertions).

check_z_substructuret(Z,Pos,Comment,Assertions) :- checkzstr(Z,typed,Pos,Comment,Assertions).

checkschematype([],_).

checkschematype([field(N,T)|Rest],Assertions) :-
    czstr(N,name,typed,Assertions),
    checktype(expr,T,Assertions),
    checkschematype(Rest,Assertions).

checktype(pred,bool,_).

checktype(top,none,_).

checktype(opt,none,_).

checktype(arm,none,_).

checktype(letdef,none,_).

checktype(bfield,none,_).

checktype(sexpr,set(schema(S)),Assertions) :- checkschematype(S,Assertions).

checktype(body,set(schema(S)),Assertions) :- checkschematype(S,Assertions).

checktype(decl,none,_).

checktype(expr,num,_).

checktype(expr,given(N),Assertions) :- czstr(N,name,typed,Assertions).

checktype(expr,freetype(N),Assertions) :- czstr(N,name,typed,Assertions).

checktype(expr,set(T),Assertions) :- checktype(expr,T,Assertions).

checktype(expr,tuple(L),Assertions) :- checktype_l(L,Assertions).

checktype(expr,schema(F),Assertions) :- checkschematype(F,Assertions).

checktype(expr,param(_),_).

checktype_l([],_).

checktype_l([E|Rest],Assertions) :-
    checktype(expr,E,Assertions),checktype_l(Rest,Assertions).

checkzstr(Z,Mode,Pos,_,Assertions) :- retractall(errorl(_,_)),czstr(Z,Pos,Mode,Assertions),!.

checkzstr(_,_,_,Comment,_) :- errorl(Msg,Expr),
    atom_concat(Comment,': ',M1),atom_concat(M1,Msg,M),
    add_error(consistencycheck,M,Expr),fail.

czstr([],list(_),_,_) :- !.

czstr([E|Rest],list(Type),Mode,Assertions) :-
    !,czstr(E,Type,Mode,Assertions),czstr(Rest,list(Type),Mode,Assertions).

czstr(Expr,number,_,_) :- !,(number(Expr) -> true; error('number expected:',Expr)).

czstr(Expr,name,_,_) :- !,(Expr=name(N,D)->true;error('name expected:',Expr)),catom(N),catom(D).

czstr(Expr,shead,M,Assertions) :-
    !,(Expr=shead(N,P)->true;error('shead expected:',Expr)),
    catom(N),czstr(P,list(name),M,Assertions).

czstr(Expr,lhs,M,Assertions) :-
    !,(Expr=lhs(N,P)->true;error('lhs expected:',Expr)),
    czstr(N,name,M,Assertions),czstr(P,list(name),M,Assertions).

czstr(Expr,token,_,_) :- !,catom(Expr).

czstr(Expr,type,_,Assertions) :-
    !,(checktype(expr,Expr,Assertions)->true;error('invalid type:',Expr)).

czstr(Expr,Type,untyped,Assertions) :-
    !,czstr2(Expr,Type,untyped,Assertions).

czstr(ti(Expr,TypeExpr),Type,typed,Assertions) :-
    !,
    (checktype(Type,TypeExpr,Assertions)->true;error('invalid type in mode ',Type,TypeExpr)),
    czstr2(Expr,Type,typed,Assertions).

czstr(Expr,_,typed,_) :- error('type info expected',Expr).

czstr2(Expr,Type,Mode,Assertions) :-
    same_functor(Expr,TInfo),
    (zstrcheck(TInfo,Type,Labels) ->
    true;error('unexpected expression in mode ',Type,Expr)),!,
    check_labels(Assertions,Labels,Expr),
    Expr =.. [_|Args],
    TInfo =.. [_|ArgTypes],
    (same_length(Args,ArgTypes)->true;error('unexpected number of arguments',Expr)),
    czstr_l(Args,ArgTypes,Mode,Assertions).

czstr_l([],[],_,_).

czstr_l([E|ERest],[Type|TRest],Mode,Assertions) :-
    czstr(E,Type,Mode,Assertions),
    czstr_l(ERest,TRest,Mode,Assertions).

error(Msg,Expr) :- assertz(errorl(Msg,Expr)),fail.

error(Msg1,Msg2,Expr) :- ajoin([Msg1,Msg2],Msg),error(Msg,Expr).

zstrcheck(ref(name,list(expr)),expr,[]).

zstrcheck(number(number),expr,[]).

zstrcheck(apply(expr,expr),expr,[]).

zstrcheck(inop(name,expr,expr),expr,[]).

zstrcheck(ingen(name,expr,expr),expr,[]).

zstrcheck(postop(name,expr),expr,[]).

zstrcheck(pregen(name,expr),expr,[]).

zstrcheck(inrel(name,expr,expr),pred,[]).

zstrcheck(prerel(name,expr),pred,[]).

zstrcheck(equal(expr,expr),pred,[]).

zstrcheck(member(expr,expr),pred,[]).

zstrcheck(power(expr),expr,[]).

zstrcheck(cross(list(expr)),expr,[]).

zstrcheck(tuple(list(expr)),expr,[]).

zstrcheck(if(pred,expr,expr),expr,[]).

zstrcheck(ext(list(expr)),expr,[]).

zstrcheck(seq(list(expr)),expr,[]).

zstrcheck(bag(list(expr)),expr,[]).

zstrcheck(theta(token,token,list(rename)),expr,[]).

zstrcheck(sexpr(sexpr),expr,[]).

zstrcheck(select(expr,name),expr,[]).

zstrcheck(lambda(body,expr),expr,[]).

zstrcheck(comp(body,opt),expr,[]).

zstrcheck(reclet(expr,expr),expr,[]).

zstrcheck(just(expr),opt,[]).

zstrcheck(nothing,opt,[]).

zstrcheck(mu(body,opt),expr,[]).

zstrcheck(falsity,pred,[]).

zstrcheck(truth,pred,[]).

zstrcheck(forall(body,pred),pred,[]).

zstrcheck(exists(body,pred),pred,[]).

zstrcheck(exists1(body,pred),pred,[]).

zstrcheck(and(pred,pred),pred,[]).

zstrcheck(or(pred,pred),pred,[]).

zstrcheck(implies(pred,pred),pred,[]).

zstrcheck(equiv(pred,pred),pred,[]).

zstrcheck(not(pred),pred,[]).

zstrcheck(spred(sexpr),pred,[]).

zstrcheck(letexpr(list(letdef),expr),expr,[]).

zstrcheck(letpred(list(letdef),pred),pred,[]).

zstrcheck(letdef(name,expr),letdef,[]).

zstrcheck(sref(token,token,list(expr),list(rename)),sexpr,[scalc]).

zstrcheck(sand(sexpr,sexpr),sexpr,[scalc]).

zstrcheck(sor(sexpr,sexpr),sexpr,[scalc]).

zstrcheck(simplies(sexpr,sexpr),sexpr,[scalc]).

zstrcheck(sequiv(sexpr,sexpr),sexpr,[scalc]).

zstrcheck(snot(sexpr),sexpr,[scalc]).

zstrcheck(sforall(body,sexpr),sexpr,[scalc]).

zstrcheck(sexists(body,sexpr),sexpr,[scalc]).

zstrcheck(sexists1(body,sexpr),sexpr,[scalc]).

zstrcheck(hide(sexpr,list(name)),sexpr,[scalc]).

zstrcheck(fatsemi(sexpr,sexpr),sexpr,[scalc]).

zstrcheck(project(sexpr,sexpr),sexpr,[scalc]).

zstrcheck(pre(sexpr),sexpr,[scalc]).

zstrcheck(pipe(sexpr,sexpr),sexpr,[scalc]).

zstrcheck(text(body),sexpr,[scalc]).

zstrcheck(sdef(shead,body),top,[]).

zstrcheck(defeq(shead,sexpr),top,[]).

zstrcheck(eqeq(lhs,expr),top,[]).

zstrcheck(define(list(name),body),top,[]).

zstrcheck(axdef(body),top,[]).

zstrcheck(pred(pred),top,[]).

zstrcheck(given(list(name)),top,[]).

zstrcheck(data(name,list(arm)),top,[]).

zstrcheck(arm(name,opt),arm,[]).

zstrcheck(body(list(decl),list(pred)),body,[]).

zstrcheck(body(list(decl),list(pred)),sexpr,[]).

zstrcheck(decl(list(name),expr),decl,[]).

zstrcheck(sdecl(sexpr),decl,[]).

zstrcheck(rename(name,name),rename,[]).

zstrcheck(namedset(name,list(name)),top,[]).

zstrcheck(binding(list(bfield)),expr,[]).

zstrcheck(bindfield(name,expr),bfield,[]).

zstrcheck(basetype(type),expr,[]).

zstrcheck(ftconstant(name,name),expr,[]).

zstrcheck(ftconstructor(name,name,expr),expr,[]).

zstrcheck(ftdestructor(name,name,expr),expr,[]).

zstrcheck(ftcase(name,name,expr),pred,[]).