subexpressions

anon_decls([],[],[]).

anon_decls([sdecl(S)|DRest],[sdecl(S)|ARest],ERest) :-
    !,anon_decls(DRest,ARest,ERest).

anon_decls([D|DRest],[A|ARest],[E|ERest]) :- anon_decls2(D,A,E),anon_decls(DRest,ARest,ERest).

anon_decls2(decl(Vars,_),decl(Vars,E),E).

anon_decls2(letdef(Name,_),letdef(Name,E),E).

clean_where(Where,Cleaned) :-
    normalise_ands(Where,NWhere),
    clean_where2(NWhere,[],Cleaned).

clean_where2([],_,[]).

clean_where2([W|Rest],Before,Cleaned) :-
    (exists_equal(Before,W) -> Cleaned = RestCleaned ; Cleaned = [W|RestCleaned]),
    clean_where2(Rest,[W|Before],RestCleaned).

clean_where2t([],_,[]).

clean_where2t([ti(truth,bool)|Rest],Before,Cleaned) :-
    !,clean_where2t(Rest,Before,Cleaned).

clean_where2t([W|Rest],Before,Cleaned) :-
    (exists_equalt(Before,W) -> Cleaned = RestCleaned ; Cleaned = [W|RestCleaned]),
    clean_where2t(Rest,[W|Before],RestCleaned).

clean_wheret(Where,Cleaned) :-
    normalise_andst(Where,NWhere),
    clean_where2t(NWhere,[],Cleaned).

equal_expression(A,B) :- equal_expression2(A,B,[]).

equal_expression2(Expr,Expr,_) :- !.

equal_expression2([AExpr|ARest],[BExpr|BRest],Mapping) :-
    !,equal_expression2(AExpr,BExpr,Mapping),
    equal_expression2(ARest,BRest,Mapping).

equal_expression2(A,B,Mapping) :-
    same_functor(A,B),
    equal_expression3(A,B,Mapping).

equal_expression2t(Expr,Expr,_) :- !.

equal_expression2t([AExpr|ARest],[BExpr|BRest],Mapping) :-
    !,equal_expression2t(AExpr,BExpr,Mapping),
    equal_expression2t(ARest,BRest,Mapping).

equal_expression2t(ti(A,TA),ti(B,TB),Mapping) :-
    functor(A,Functor,Arit),
    functor(B,Functor,Arit),
    similiar_type(TA,TB),
    equal_expression3t(ti(A,T),ti(B,T),Mapping).

equal_expression3(ref(AName,[]),ref(BName,[]),Mapping) :-
    member(mapping(AName,AMap),Mapping),!,AMap=BName.

equal_expression3(A,B,Mapping) :-
    zsubnamespace(A,AOuter,AInner,ANames),
    !,
    zsubnamespace(B,BOuter,BInner,BNames),
    equal_expression2(AOuter,BOuter,Mapping),
    extend_mapping(ANames,BNames,Mapping,NewMapping),
    equal_expression2(AInner,BInner,NewMapping).

equal_expression3(A,B,Mapping) :-
    zexpr_conversion(A,ASubs,BSubs,B),
    equal_expression2(ASubs,BSubs,Mapping).

equal_expression3t(ti(ref(AName,[]),T),ti(ref(BName,[]),T),Mapping) :-
    member(mapping(AName,AMap),Mapping),!,AMap=BName.

equal_expression3t(A,B,Mapping) :-
    zsubnamespacet(A,AOuter,AInner,ANames,ATypes),
    !,
    zsubnamespacet(B,BOuter,BInner,BNames,BTypes),
    equal_expression2t(AOuter,BOuter,Mapping),
    similiar_type_l(ATypes,BTypes),
    extend_mapping(ANames,BNames,Mapping,NewMapping),
    equal_expression2t(AInner,BInner,NewMapping).

equal_expression3t(A,B,Mapping) :-
    zexpr_conversiont(A,ASubs,BSubs,B),
    equal_expression2t(ASubs,BSubs,Mapping).

equal_expressiont(A,B) :- equal_expression2t(A,B,[]).

exists_equal([ExprA|_],ExprB) :- equal_expression(ExprA,ExprB),!.

exists_equal([_|Rest],Expr) :- exists_equal(Rest,Expr).

exists_equalt([ExprA|_],ExprB) :- equal_expressiont(ExprA,ExprB),!.

exists_equalt([_|Rest],Expr) :- exists_equalt(Rest,Expr).

extend_mapping([],[],Mapping,Mapping) :- !.

extend_mapping([A|ARest],[B|BRest],Mapping,NewMapping) :-
    !,extend_mapping(A,B,Mapping,InterMapping),
    extend_mapping(ARest,BRest,InterMapping,NewMapping).

extend_mapping(A,B,Mapping,[mapping(A,B)|Mapping]).

extract_body_structure(Expr,Outer,Inner,Names,Decls,Exprs,Where) :-
    zns_body(Expr,body(Decls,Where),Exprs),
    append(Where,Exprs,Inner),
    findall(Type,member(decl(_,Type),Decls),Outer),
    findall(Vars,member(decl(Vars,_),Decls),VarLists),
    append(VarLists,Names).

extract_let_structure(Expr,Outer,Inner,Names,Defs) :-
    zns_let(Expr,Defs,Inner),
    findall(Name,member(letdef(Name,_),Defs),Names),
    findall(LExpr,member(letdef(_,LExpr),Defs),Outer).

extract_t_vars_outer([],[],[]).

extract_t_vars_outer([ti(decl(Vars,TypeExpr),none)|DRest],[Vars|VRest],[TypeExpr|TRest]) :-
    extract_t_vars_outer(DRest,VRest,TRest).

extract_t_vars_outer([],[],[],[],[]).

extract_t_vars_outer([ti(decl(Vars,TypeExpr),DT)|DRest],
    [Vars|VRest],
    [TypeExpr|TRest],
    [NTypeExpr|NTRest],
    [ti(decl(Vars,NTypeExpr),DT)|NDRest]) :-
    extract_t_vars_outer(DRest,VRest,TRest,NTRest,NDRest).

extract_t_vars_outerl([],[],[]).

extract_t_vars_outerl([ti(letdef(Name,Expr),none)|DRest],[Name|NRest],[Expr|ERest]) :-
    extract_t_vars_outerl(DRest,NRest,ERest).

extract_t_vars_outerl([],[],[],[],[]).

extract_t_vars_outerl([ti(letdef(Name,Expr),DT)|DRest],
    [Name|NRest],
    [Expr|ERest],
    [NExpr|NERest],
    [ti(letdef(Name,NExpr),DT)|NDRest]) :-
    extract_t_vars_outerl(DRest,NRest,ERest,NERest,NDRest).

has_body(Expr) :- zns_body(Expr,body(_,_),_),!.

normalise_ands(Ands,Normalised) :-
    normalise_ands2(Ands,Normalised,[]).

normalise_ands2([]) --> !,[].

normalise_ands2([A|Rest]) -->
    !,normalise_ands2(A),normalise_ands2(Rest).

normalise_ands2(and(A,B)) -->
    !,normalise_ands2(A), normalise_ands2(B).

normalise_ands2(truth) --> !,[].

normalise_ands2(Expr) --> [Expr].

normalise_ands2t([]) --> !,[].

normalise_ands2t([A|Rest]) -->
    !,normalise_ands2t(A),normalise_ands2t(Rest).

normalise_ands2t(ti(and(A,B),bool)) -->
    !,normalise_ands2t(A), normalise_ands2t(B).

normalise_ands2t(ti(truth,bool)) --> !,[].

normalise_ands2t(Expr) --> [Expr].

normalise_andst(Ands,Normalised) :-
    normalise_ands2t(Ands,Normalised,[]).

remove_renamings([],_,[]).

remove_renamings([rename(New,Old)|RRest],Names,Renamings) :-
    (member(Old,Names) ->
    Renamings = ORenamings;
    Renamings = [rename(New,Old)|ORenamings]),
    remove_renamings(RRest,Names,ORenamings).

rename_decl_varst([],_,[]).

rename_decl_varst([Old|ORest],Renamings,[New|NRest]) :-
    (member(rename(New,Old),Renamings) ->
    !,true;
    Old = New),
    rename_decl_varst(ORest,Renamings,NRest).

rename_declst([],_,[]).

rename_declst([ti(decl(Vars,Type),none)|DRest],Renamings,[ti(decl(RVars,Type),none)|RRest]) :-
    !,rename_decl_varst(Vars,Renamings,RVars),
    rename_declst(DRest,Renamings,RRest).

rename_fieldst([],_,[]).

rename_fieldst([field(Old,Type)|ORest],Renamings,[field(New,Type)|NRest]) :-
    (member(rename(New,Old),Renamings) ->
    !,true;
    Old = New),
    rename_fieldst(ORest,Renamings,NRest).

rename_variablest(Exprs,[],Exprs) :- !.

rename_variablest(ti(body(Decls,Where),set(schema(Fields))),Renamings,
    ti(body(RDecls,RWhere),set(schema(RFields)))) :-
    !,
    rename_declst(Decls,Renamings,RDecls),
    rename_fieldst(Fields,Renamings,RFields),
    rename_variablest2(Where,Renamings,RWhere).

rename_variablest(Expr,Renamings,Result) :- rename_variablest2(Expr,Renamings,Result).

rename_variablest2([],_,[]) :- !.

rename_variablest2([E|ERest],Renamings,[P|PRest]) :-
    !,rename_variablest2(E,Renamings,P),
    rename_variablest2(ERest,Renamings,PRest).

rename_variablest2(ti(ref(Name,P),Type),Renamings,ti(ref(New,P),Type)) :-
    !,
    (member(rename(New,Name),Renamings) ->
    !,true;
    New = Name).

rename_variablest2(Expr,Renamings,Result) :-
    znamespacet(Expr,Outer,Inner,Names,NOuter,NInner,Result),
    !,
    rename_variablest2(Outer,Renamings,NOuter),
    remove_renamings(Renamings,Names,NRenamings),
    rename_variablest2(Inner,NRenamings,NInner).

rename_variablest2(Expr,Renamings,Result) :-
    zexpr_conversiont(Expr,Subs,PSubs,Result),
    rename_variablest2(Subs,Renamings,PSubs).

similiar_type(T,T) :- !.

similiar_type(set(A),set(B)) :- similiar_type(A,B).

similiar_type(tuple(A),tuple(B)) :- similiar_type_l(A,B).

similiar_type(schema(A),schema(B)) :- same_length(A,B).

similiar_type_l([],[]).

similiar_type_l([A|Arest],[B|Brest]) :-
    similiar_type(A,B),
    similiar_type_l(Arest,Brest).

vars_and_types_of_decls([],[],[]).

vars_and_types_of_decls([decl(Vars,Type)|Rest],[Vars|NRest],[Type|TRest]) :-
    !,vars_and_types_of_decls(Rest,NRest,TRest).

vars_and_types_of_decls([sdecl(S)|Rest],NRest,[S|TRest]) :-
    vars_and_types_of_decls(Rest,NRest,TRest).

vars_and_types_of_letdefs([],[],[]).

vars_and_types_of_letdefs([letdef(Name,Expr)|Rest],[Name|NRest],[Expr|ERest]) :-
    vars_and_types_of_letdefs(Rest,NRest,ERest).

zexpr_conversion(ref(N,P),[],[],ref(N,P)).

zexpr_conversion(number(N),[],[],number(N)).

zexpr_conversion(apply(F,A),[F,A],[F2,A2],apply(F2,A2)).

zexpr_conversion(inop(N,A,B),[A,B],[A2,B2],inop(N,A2,B2)).

zexpr_conversion(ingen(N,A,B),[A,B],[A2,B2],ingen(N,A2,B2)).

zexpr_conversion(postop(N,A),[A],[A2],postop(N,A2)).

zexpr_conversion(pregen(N,A),[A],[A2],pregen(N,A2)).

zexpr_conversion(inrel(N,A,B),[A,B],[A2,B2],inrel(N,A2,B2)).

zexpr_conversion(prerel(N,A),[A],[A2],prerel(N,A2)).

zexpr_conversion(equal(A,B),[A,B],[A2,B2],equal(A2,B2)).

zexpr_conversion(member(A,B),[A,B],[A2,B2],member(A2,B2)).

zexpr_conversion(power(A),[A],[A2],power(A2)).

zexpr_conversion(cross(A),[A],[A2],cross(A2)).

zexpr_conversion(tuple(A),[A],[A2],tuple(A2)).

zexpr_conversion(if(I,T,E),[I,T,E],[I2,T2,E2],if(I2,T2,E2)).

zexpr_conversion(ext(A),[A],[A2],ext(A2)).

zexpr_conversion(seq(A),[A],[A2],seq(A2)).

zexpr_conversion(bag(A),[A],[A2],bag(A2)).

zexpr_conversion(theta(N,D,R),[],[],theta(N,D,R)).

zexpr_conversion(sexpr(A),[A],[A2],sexpr(A2)).

zexpr_conversion(select(A,N),[A],[A2],select(A2,N)).

zexpr_conversion(lambda(A,B),[A,B],[A2,B2],lambda(A2,B2)).

zexpr_conversion(comp(A,B),[A,B],[A2,B2],comp(A2,B2)).

zexpr_conversion(reclet(A,B),[A,B],[A2,B2],reclet(A2,B2)).

zexpr_conversion(just(A),[A],[A2],just(A2)).

zexpr_conversion(nothing,[],[],nothing).

zexpr_conversion(mu(A,B),[A,B],[A2,B2],mu(A2,B2)).

zexpr_conversion(falsity,[],[],falsity).

zexpr_conversion(truth,[],[],truth).

zexpr_conversion(forall(A,B),[A,B],[A2,B2],forall(A2,B2)).

zexpr_conversion(exists(A,B),[A,B],[A2,B2],exists(A2,B2)).

zexpr_conversion(exists1(A,B),[A,B],[A2,B2],exists1(A2,B2)).

zexpr_conversion(and(A,B),[A,B],[A2,B2],and(A2,B2)).

zexpr_conversion(or(A,B),[A,B],[A2,B2],or(A2,B2)).

zexpr_conversion(implies(A,B),[A,B],[A2,B2],implies(A2,B2)).

zexpr_conversion(equiv(A,B),[A,B],[A2,B2],equiv(A2,B2)).

zexpr_conversion(not(A),[A],[A2],not(A2)).

zexpr_conversion(spred(S),[S],[S2],spred(S2)).

zexpr_conversion(letexpr(A,B),[A,B],[A2,B2],letexpr(A2,B2)).

zexpr_conversion(letpred(A,B),[A,B],[A2,B2],letpred(A2,B2)).

zexpr_conversion(letdef(N,A),[A],[A2],letdef(N,A2)).

zexpr_conversion(sref(N,D,P,R),[],[],sref(N,D,P,R)).

zexpr_conversion(sand(A,B),[A,B],[A2,B2],sand(A2,B2)).

zexpr_conversion(sor(A,B),[A,B],[A2,B2],sor(A2,B2)).

zexpr_conversion(simplies(A,B),[A,B],[A2,B2],simplies(A2,B2)).

zexpr_conversion(sequiv(A,B),[A,B],[A2,B2],sequiv(A2,B2)).

zexpr_conversion(snot(A),[A],[A2],snot(A2)).

zexpr_conversion(sforall(A,B),[A,B],[A2,B2],sforall(A2,B2)).

zexpr_conversion(sexists(A,B),[A,B],[A2,B2],sexists(A2,B2)).

zexpr_conversion(sexists1(A,B),[A,B],[A2,B2],sexists1(A2,B2)).

zexpr_conversion(hide(A,H),[A],[A2],hide(A2,H)).

zexpr_conversion(fatsemi(A,B),[A,B],[A2,B2],fatsemi(A2,B2)).

zexpr_conversion(project(A,B),[A,B],[A2,B2],project(A2,B2)).

zexpr_conversion(pre(A),[A],[A2],pre(A2)).

zexpr_conversion(pipe(A,B),[A,B],[A2,B2],pipe(A2,B2)).

zexpr_conversion(text(A),[A],[A2],text(A2)).

zexpr_conversion(sdef(N,D),[D],[D2],sdef(N,D2)).

zexpr_conversion(defeq(N,D),[D],[D2],defeq(N,D2)).

zexpr_conversion(eqeq(N,D),[D],[D2],eqeq(N,D2)).

zexpr_conversion(define(N,D),[D],[D2],define(N,D2)).

zexpr_conversion(axdef(D),[D],[D2],axdef(D2)).

zexpr_conversion(pred(P),[P],[P2],pred(P2)).

zexpr_conversion(given(Ns),[],[],given(Ns)).

zexpr_conversion(data(N,Arms),[Arms],[Arms2],data(N,Arms2)).

zexpr_conversion(arm(N,A),[A],[A2],arm(N,A2)).

zexpr_conversion(body(D,W),[D,W],[D2,W2],body(D2,W2)).

zexpr_conversion(decl(Ns,T),[T],[T2],decl(Ns,T2)).

zexpr_conversion(sdecl(S),[S],[S2],sdecl(S2)).

zexpr_conversion(namedset(N,Ms),[],[],namedset(N,Ms)).

zexpr_conversion(binding(Fs),[Fs],[Fs2],binding(Fs2)).

zexpr_conversion(bindfield(N,E),[E],[E2],bindfield(N,E2)).

zexpr_conversion(basetype(T),[],[],basetype(T)).

zexpr_conversion(ftconstant(F,C),[],[],ftconstant(F,C)).

zexpr_conversion(ftconstructor(F,C,E),[E],[E2],ftconstructor(F,C,E2)).

zexpr_conversion(ftdestructor(F,C,E),[E],[E2],ftdestructor(F,C,E2)).

zexpr_conversion(ftcase(F,C,E),[E],[E2],ftcase(F,C,E2)).

zexpr_conversiont(ti(E,Type),ESubs,CSubs,ti(C,Type)) :-
    zexpr_conversion(E,ESubs,CSubs,C).

znamespace(Expr,Outer,Inner,Names) :-
    has_body(Expr),!,
    extract_body_structure(Expr,Outer,Inner,Names,_Decls,_Exprs,_Where).

znamespace(Expr,Outer,Inner,Names) :-
    extract_let_structure(Expr,Outer,Inner,Names,_Defs).

znamespace(Expr,Outer,Inner,Names,NOuter,NInner,Result) :-
    has_body(Expr),!,
    extract_body_structure(Expr,Outer,Inner,Names,Decls,Exprs,Where),
   
    same_functor(Expr,Term),
    zns_body(Term,body(XDecls,XWhere),XExprs),
    anon_decls(Decls,XDecls,NOuter),
    same_length(Where,XWhere),
    same_length(Exprs,XExprs),
    append(XWhere,XExprs,NInner),
    Term = Result.

znamespace(Expr,Outer,Inner,Names,NOuter,NInner,Result) :-
    extract_let_structure(Expr,Outer,Inner,Names,Defs),
   
    same_functor(Expr,Term),
    zns_let(Term,XDefs,XExpr),
    anon_decls(Defs,XDefs,NOuter),
    NInner = XExpr,
    Result = Term.

znamespacet(ti(E,_),Outer,Inner,Names) :-
    zns_body2(E,ti(body(Decls,Where),_),Exprs),!,
    extract_t_vars_outer(Decls,DeclVars,Outer),
    append(DeclVars,Names),
    append(Where,Exprs,Inner).

znamespacet(ti(E,_),Outer,Inner,Names) :-
    zns_let(E,Defs,Inner),!,
    extract_t_vars_outerl(Defs,Names,Outer).

znamespacet(ti(E,Type),Outer,[Exprs,Where],Names,NOuter,[NExprs,NWhere],ti(N,Type)) :-
    zns_body2(E,ti(body(Decls,Where),BType),Exprs),!,
    extract_t_vars_outer(Decls,DeclVars,Outer,NOuter,NDecls),
    functor(E,Functor,Arity),functor(N,Functor,Arity),
    zns_body2(N,ti(body(NDecls,NWhere),BType),NExprs),
    same_length(Where,NWhere),
    same_length(Exprs,NExprs),
    append(DeclVars,Names).

znamespacet(ti(E,Type),Outer,Inner,Names,NOuter,NInner,ti(N,Type)) :-
    zns_let(E,Defs,Inner),!,
    subexpressions:extract_t_vars_outerl(Defs,Names,Outer,NOuter,NDefs),
    functor(E,Functor,Arity),functor(N,Functor,Arity),
    zns_let(N,NDefs,NInner).

zns_body(body(Decl,Where),body(Decl,Where),[]) :- !.

zns_body(Expr,Body,Res) :- zns_body2(Expr,Body,Res).

zns_body2(forall(Body,Expr),Body,[Expr]).

zns_body2(exists(Body,Expr),Body,[Expr]).

zns_body2(exists1(Body,Expr),Body,[Expr]).

zns_body2(sforall(Body,Expr),Body,[Expr]).

zns_body2(sexists(Body,Expr),Body,[Expr]).

zns_body2(sexists1(Body,Expr),Body,[Expr]).

zns_body2(mu(Body,Expr),Body,[Expr]).

zns_body2(comp(Body,Expr),Body,[Expr]).

zns_body2(lambda(Body,Expr),Body,[Expr]).

zns_let(letexpr(Defs,Expr),Defs,Expr).

zns_let(letpred(Defs,Pred),Defs,Pred).

zsubexpressionst(ti(Expr,_),Subs) :-
    zexpr_conversion(Expr,Subs,_,_).

zsubnamespace(Expr,Outer,[Where,Exprs],Names) :-
    zns_body(Expr,body(Decls,Where),Exprs),
    !,
    vars_and_types_of_decls(Decls,Names,Outer).

zsubnamespace(Expr,Outer,Inner,Names) :-
    zns_let(Expr,Defs,Inner),
    vars_and_types_of_letdefs(Defs,Names,Outer).

zsubnamespacet(ti(E,Type),Outer,[Where,Exprs],Names,[Type,BType]) :-
    zns_body2(E,ti(body(Decls,Where),BType),Exprs),!,
    extract_t_vars_outer(Decls,Names,Outer).

zsubnamespacet(ti(E,Type),Outer,Inner,Names,[Type]) :-
    zns_let(E,Defs,Inner),!,
    extract_t_vars_outerl(Defs,Names,Outer).