ztransformations

all_basetypes([ti(basetype(set(T)),_)],[T]).

all_basetypes([ti(basetype(set(A)),_),B|Rest], [A|TRest]) :-
    all_basetypes([B|Rest],TRest).

clearsrefs(In,Out) :-
    findschemas(In,Schemas),
    clearsrefs2(In,Schemas,Out).

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

clearsrefs2([Expr|Rest],Schemas,[CExpr|CRest]) :-
    !, clearsrefs2(Expr,Schemas,CExpr),
    clearsrefs2(Rest,Schemas,CRest).

clearsrefs2(ref(name(Name,Deco),Params),Schemas,sexpr(sref(Name,Deco,Params,[]))) :-
    member(Name,Schemas),!.

clearsrefs2(Expr,Schemas,CExpr) :-
    zexpr_conversion(Expr,Old,New,CExpr),
    clearsrefs2(Old,Schemas,New).

compset_type_convert(set(schema([field(_,Type)])),set(Type)) :- !.

compset_type_convert(set(schema(Fields)),set(tuple([Types]))) :-
    maplist(extract_field_type,Fields,Types).

construct_reference(FreetypeName,ReferencedFreetype,ref(FreetypeName,ReferencedFreetype)).

count_occurences(Expr,Search,Count) :-
    count_occurences2(Expr,Search,0,Count).

count_occurences2(ti(ref(Search,[]),_),Search,In,Out) :- !,Out is In + 1.

count_occurences2([],_,Count,Count) :- !.

count_occurences2([Expr|ERest],Search,In,Out) :-
    !,count_occurences2(Expr,Search,In,I2),
    count_occurences2(ERest,Search,I2,Out).

count_occurences2(Expr,Search,In,Out) :-
    znamespacet(Expr,Outer,Inner,Names),!,
    count_occurences2(Outer,Search,In,I2),
    % if a variable of the same name has been introduced by an quantifier,
    % we do not look further into the inner expression
    (memberchk(Search,Names) -> I2 = Out ; count_occurences2(Inner,Search,I2,Out)).

count_occurences2(Expr,Search,In,Out) :-
    zsubexpressionst(Expr,Subs),
    count_occurences2(Subs,Search,In,Out).

create_axdef_for_recfreetype(Ti,ti(axdef(Body),none)) :-
    ti_expr(Ti,data(FT,Arms)),
   
    FTSET = set(freetype(FT)),
   
    global_ft_constant(FT,Global),
    Equation = ti(equal(ti(ref(Global,[]),FTSET),RecLet),bool),
    create_typed_body([Global],[FTSET],[Equation],Body),
   
   
    RecLet = ti(reclet(ti(ref(Global,[]),FTSET),Compset),FTSET),
    Compset = ti(comp(CompsetBody,ti(nothing,none)),FTSET),
    z_counter('param__',P),Param=name(P,''),
    create_typed_body([Param],[freetype(FT)],Constraints,CompsetBody),
    create_constraints(Arms,FT,ti(ref(Param,[]),freetype(FT)),Constraints).

create_bag_count(Bag,RefParam,if(If,Then,Else)) :-
    % bcount(Bag,r) == IF r:dom(Bag) THEN Bag(r) ELSE 0 END
    make_z_member(RefParam,BagDom,If),
    make_z_domain(Bag,BagDom),
    make_z_expr(apply(Bag,RefParam),num,Then),
    make_z_number(0,Else).

create_bag_minus(Bag,NegBag,comp(Body,Just)) :- % uminus = BagDifference
    ti_type(Bag,BagType), BagType = set(tuple([Type,num])),
    make_z_expr(just(Expr),BagType,Just),
    unique_reference('i__',num,Iname,I),
    unique_reference('e__',Type,Ename,E),
    unique_reference('d__',num,Dname,D),
    create_typed_body([Ename,Iname,Dname],[Type,num,num],[Membership,Equal,Pos],Body),
    make_z_member(Pair,Bag,Membership),
    make_z_tuple([E,I],[Type,num],Pair),
    make_z_tuple([E,D],[Type,num],Expr),
    make_z_expr(equal(D,Diff),bool,Equal),
    make_z_inrel('<',Zero,D,Pos),
    make_z_number(0,Zero),
    make_z_inop('-',num,I,Count,Diff),
    make_z_bag_count(NegBag,E,Count).

create_bag_otimes(Factor,Bag,comp(Body,Just)) :-
    ti_type(Bag,BagType), BagType = set(tuple([Type,num])),
    make_z_expr(just(Expr),BagType,Just),
    unique_reference('i__',num,Iname,I),
    unique_reference('e__',Type,Ename,E),
    create_typed_body([Ename,Iname],[Type,num],[Where],Body),
    make_z_member(Pair,Bag,Where),
    make_z_tuple([E,I],[Type,num],Pair),
    make_z_tuple([E,Mult],[Type,num],Expr),
    make_z_inop('*',num,Factor,I,Mult).

create_bag_plus(BagA,BagB,comp(Body,Just)) :- % uplus = BagUnion
    % A \+/ B == { e,c | e:dom(A\/B) & c = bcount(A,e)+bcount(B,e)}
    ti_type(BagA,BagType), BagType = set(tuple([Type,num])),
    make_z_expr(just(Expr),BagType,Just),
    unique_reference('e__',Type,Ename,E),
    create_typed_body([Ename],[Type],[Where],Body),
    make_z_member(E,DomUnion,Where),
    make_z_inop('\\cup',set(Type),DomA,DomB,DomUnion),
    make_z_domain(BagA,DomA), make_z_domain(BagB,DomB),
    make_z_inop('+',num,CountA,CountB,Sum),
    make_z_bag_count(BagA,E,CountA), make_z_bag_count(BagB,E,CountB),
    make_z_tuple([E,Sum],[Type,num],Expr).

create_constraints([],_,_,[]).

create_constraints([ti(arm(CName,ti(just(DomSet),none)),_)|Rest],FT,Expr,
    [ti(implies(A,B),bool)|CRest]) :-
    !,ti_type(DomSet,set(CType)),
    A = ti(ftcase(FT,CName,Expr),bool),
    B = ti(member(Destr,DomSet),bool),
    Destr = ti(ftdestructor(FT,CName,Expr),CType),
    create_constraints(Rest,FT,Expr,CRest).

create_constraints([ti(arm(_,ti(nothing,none)),_)|Rest],FT,Expr,CRest) :-
    create_constraints(Rest,FT,Expr,CRest).

create_subbag(BagA,BagB,forall(Body,Pred)) :-
    ti_type(BagA,BagType), BagType = set(tuple([Type,num])),
    unique_reference('i__',num,Iname,I),
    unique_reference('e__',Type,Ename,E),
    create_typed_body([Ename,Iname],[Type,num],[Membership],Body),
    make_z_member(Pair,BagA,Membership),
    make_z_tuple([E,I],[Type,num],Pair),
    make_z_domain(BagB,DomainB),
    make_z_member(E,DomainB,CheckMember),
    make_z_expr(apply(BagB,E),num,CountB),
    make_z_inrel('\\leq',I,CountB,LessEqual),
    make_z_expr(and(CheckMember,LessEqual),bool,Pred).

create_typed_body(Params,Types,Wheres,Body) :-
    ti_expr(Body,body(Decls,Wheres)), ti_type(Body,set(schema(Fields))),
    create_typed_decl_fields(Params,Types,Decls,Fields).

create_typed_decl_fields([],[],[],[]).

create_typed_decl_fields([N|Nrest],[Type|Trest],[D|Drest],[field(N,Type)|Frest]) :-
    ti_expr(D,decl([N],Basetype)), ti_type(D,none),
    ti_expr(Basetype,basetype(set(Type))), ti_type(Basetype,set(Type)),
    create_typed_decl_fields(Nrest,Trest,Drest,Frest).

equal_bindings([],_,ti(truth,bool)).

equal_bindings([ti(bindfield(Name,ExprA),_)],Bindings2,ti(equal(ExprA,ExprB),bool)) :-
    !,member(ti(bindfield(Name,ExprB),_),Bindings2),!.

equal_bindings([ti(bindfield(Name,ExprA),_)|BRest],Bindings2,
    ti(and(ti(equal(ExprA,ExprB),bool),ERest),bool)) :-
    member(ti(bindfield(Name,ExprB),_),Bindings2),!,
    equal_bindings(BRest,Bindings2,ERest).

extract_field_type(field(_,Type),Type).

extract_fr(freetype(Name),In,Out) :- !,ord_add_element(In,Name,Out).

extract_fr(set(X),In,Out) :- !,extract_fr(X,In,Out).

extract_fr(tuple(Types),In,Out) :- !,foldl(extract_fr,Types,In,Out).

extract_fr(schema(Fields),In,Out) :-
    !,maplist(extract_field_type,Fields,Types),
    foldl(extract_fr,Types,In,Out). %% FIXED: extract_fr should probably be the first argument, but clause is not tested

extract_fr(_,Refs,Refs).

extract_freetype_arm_domain_type(ArmTi,ArmDomainType) :-
    ti_expr(ArmTi,arm(_Name,ArmDef)),
    ti_expr(ArmDef,just(ArmDomain)),
    ti_type(ArmDomain,ArmDomainType).

find_freetype_refs(FreeTypeDefinitions,References) :-
    maplist(find_freetype_refs2,FreeTypeDefinitions,ReferencesL),
    append(ReferencesL,References).

find_freetype_refs2(FreeTypeDefinition,References) :-
    ti_expr(FreeTypeDefinition,data(FreetypeName,Arms)),
    % extract the domains of the constructor arms (skip the constants)
    convlist(extract_freetype_arm_domain_type,Arms,ArmDomainTypes),
    foldl(extract_fr,ArmDomainTypes,[],ReferencedFreetypes),
    maplist(construct_reference(FreetypeName),ReferencedFreetypes,References).

findeqeq([],[],[]).

findeqeq([S|Rest],NonEqeqs,Eqeqs) :-
    (S=eqeq(_,_) ->
    (NonEqeqs,Eqeqs) = (NeRest,[S|EqRest]);
    (NonEqeqs,Eqeqs) = ([S|NeRest],EqRest)),
    findeqeq(Rest,NeRest,EqRest).

findschema(sdef(shead(Name,[]),_),Name).

findschema(defeq(shead(Name,[]),_),Name).

findschemas([],[]).

findschemas([D|Rest],Schemas) :-
    (findschema(D,Name) ->
    Schemas = [Name|SRest];
    Schemas = SRest),
    findschemas(Rest,SRest).

freetype2namedsets([],[]) :- !.

freetype2namedsets([E|ERest],[C|CRest]) :-
    !,freetype2namedsets(E,C),
    freetype2namedsets(ERest,CRest).

freetype2namedsets(data(Name,Arms),namedset(Name,Members)) :-
    % a freetype can be converted if it elements are just constants, no constructors
    \+ member(arm(_,just(_)),Arms),
    !, findall(M,member(arm(M,nothing),Arms),Members).

freetype2namedsets(E,E).

ftenv(Env,FtEnv) :- member(freetype(FtEnv),Env),!.

ftget(Env,FT,Arms,FtType) :- ftenv(Env,FtEnv),member(ft(ti(data(FT,Arms),_),FtType),FtEnv).

ggsimplify(In,Out) :-
    prepare_given_env(In,GivenEnv),
    prepare_freetype_env(In,FreetypeEnv,I2),
    Env = [given(GivenEnv),freetype(FreetypeEnv)],
    ggsimplify1(I2,Env,Out).

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

ggsimplify1([Expr|Rest],Env,[SimplExpr|SimplRest]) :-
    !,ggsimplify1(Expr,Env,SimplExpr),
    ggsimplify1(Rest,Env,SimplRest).

ggsimplify1(ti(Expr,T),Env,ti(Simpl,T)) :-
    presimplify_fixpoint(Expr,T,Env,Step1),
    zexpr_conversiont(ti(Step1,T),Subs,SSubs,ti(S,T)),
    ggsimplify1(Subs,Env,SSubs),
    ggsimplify_fixpoint(S,T,Env,Simpl).

ggsimplify2(and(ti(truth,bool),ti(X,bool)),_,_,X) :- !.

ggsimplify2(and(ti(X,bool),ti(truth,bool)),_,_,X) :- !.

ggsimplify2(implies(_,ti(truth,bool)),_,_,truth) :- !.

ggsimplify2(ref(name('\\num',''),[]),_,_,basetype(set(num))) :- !.

ggsimplify2(power(ti(basetype(T),T)),_,_,basetype(set(T))) :- !.

ggsimplify2(pregen(name('\\finset',''),ti(basetype(T),T)),_,_,basetype(set(T))) :- !.

ggsimplify2(cross(List),_,_,basetype(set(tuple(Types)))) :-
    all_basetypes(List,Types),!.

ggsimplify2(ingen(name('\\rel',''),ti(basetype(set(A)),_),ti(basetype(set(B)),_)),_,_,
    basetype(set(tuple([A,B])))) :- !.

ggsimplify2(ref(Name,[]),set(given(Name)),Env,basetype(set(given(Name)))) :-
    member(given(GivenEnv),Env),member(Name,GivenEnv),!.

ggsimplify2(comp(ti(body(_,[]),_),ti(nothing,none)),Type,_,basetype(Type)) :- !.

ggsimplify2(comp(BodyTi, ti(just(ResultTi),_)), _,_, comp(NewBody,ti(nothing,none))) :-
    !, simplify_compset(BodyTi,ResultTi,NewBody).

ggsimplify2(mu(BodyTi, ti(just(ResultTi),_)), _,_, mu(NewBody,ti(nothing,none))) :-
    !,simplify_compset(BodyTi,ResultTi,NewBody).

ggsimplify2(equal(ti(binding(B1),_),ti(binding(B2),_)), _,_, Result) :-
    !, equal_bindings(B1,B2,ti(Result,bool)).

ggsimplify2(exists1(ti(body(Decl,Where),BType),Condition), _, Env, equal(Card,ti(number(1),num))) :-
    !,
    Card1 = ti(apply(Ref,Comp),num),
    Ref = ti(ref(name('\\#',''),[]),set(tuple([SetType,num]))),
    Comp = ti(comp(ti(body(Decl,NewWhere),BType),ti(nothing,none)),SetType),
    compset_type_convert(BType,SetType),
    append(Where,[Condition],NewWhere),
    ggsimplify1(Card1,Env,Card).

ggsimplify2(inop(name('\\circ',''), A, B), _,_, inop(name('\\comp',''), B, A)) :- !.

ggsimplify2(apply(ti(ref(name('succ',''),[]),_), Arg), _,_,
    inop(name('+',''),Arg, ti(number(1),num))) :- !.

ggsimplify2(body(Decls,Where), _,_, body(Decls,NewWhere)) :-
    !,clean_wheret(Where,NewWhere).

ggsimplify2(member(Expr, ti(comp(Body,ti(nothing,none)),_)), _,_, Condition) :-
    Body = ti(body([ti(decl([Var],_),_)],Wheres),_),
    !,simplify_member(Expr,Var,Wheres,ti(Condition,bool)).

ggsimplify2(member(_,ti(basetype(_),_)), _,_, truth) :- !.

ggsimplify2(postop(name('\\star',''),ExprTi), RelType, _, inop(name('\\cup',''),TransCls,Id)) :-
    RelType = set(tuple([T,T])),!,
    TransCls = ti(postop(name('\\plus',''),ExprTi),RelType),
    Id = ti(pregen(name('\\id',''),ti(basetype(set(T)),set(T))),RelType).

ggsimplify2(apply(ti(lambda(ti(body([ti(decl([Param],_),_)],[]),_),ExprTi),_),
    ArgTi),_,_,
    NewExpr) :-
    !,replace_expression(ExprTi,Param,ArgTi,ti(NewExpr,_)).

ggsimplify2(bag(Expressions), BagType, _Env, apply(ItemsFun,Seq)) :- !,
    BagType = set(tuple([X,num])), SeqType = set(tuple([num,X])),
    ItemsFun = ti(ref(name('items',''),[]),set(tuple([BagType,SeqType]))),
    Seq = ti(seq(Expressions),set(SeqType)).

ggsimplify2(pregen(name('\\bag',''),Set), _Type, _Env, ingen(name('\\pfun',''), Set, Nat1)) :-
    ti_expr(Nat1,ref(name('\\nat','_1'),[])),
    ti_type(Nat1,set(num)).

ggsimplify2(inop(name('\\bcount',''),Bag,Elem),Type,Env,IfThenElse) :-
    !,create_bag_count(Bag,Elem,IfThenElse1), ggsimplify1(ti(IfThenElse1,Type),Env,ti(IfThenElse,_)).

ggsimplify2(apply(Count,Bag), _Type, _Env, lambda(Body,Expr)) :-
    ti_expr(Count,ref(name('count',''),[])),!,
    ti_type(Bag,BagType),
    BagType = set(tuple([ArgType,num])),
    z_counter('param__',P),Param=name(P,''),
    Body = ti(body([ti(decl([Param],ti(basetype(set(ArgType)),set(ArgType))),none)],[]),
    set(schema([field(Param,ArgType)]))),
    ti_expr(RefParam,ref(Param,[])), ti_type(RefParam,ArgType),
    create_bag_count(Bag,RefParam,IfThenElse),
    ti_expr(Expr,IfThenElse), ti_type(Expr,num).

ggsimplify2(inop(name('\\otimes',''),Factor,Bag),Type,Env,Comp) :-
    !,create_bag_otimes(Factor,Bag,Comp1), ggsimplify1(ti(Comp1,Type),Env,ti(Comp,_)).

ggsimplify2(inop(name('\\uminus',''),A,B),Type,Env,Comp) :-
    !,create_bag_minus(A,B,Comp1), ggsimplify1(ti(Comp1,Type),Env,ti(Comp,_)).

ggsimplify2(inop(name('\\uplus',''),A,B),Type,Env,Comp) :-
    !,create_bag_plus(A,B,Comp1), ggsimplify1(ti(Comp1,Type),Env,ti(Comp,_)).

ggsimplify2(inrel(name('\\inbag',''),Elem,Bag),_Type,_Env,member(Elem,Domain)) :-
    !,make_z_domain(Bag,Domain).

ggsimplify2(inrel(name('\\subbageq',''),BagA,BagB),_Type,_Env,Pred) :-
    !,create_subbag(BagA,BagB,Pred).

ggsimplify2(ref(CName,[]),freetype(FT),Env,ftconstant(FT,CName)) :-
    is_ftconstant2(Env,FT,CName),!.

ggsimplify2(ref(CName,[]),set(tuple([ArgType,freetype(FT)])),Env,Lambda) :-
    is_ftconstructor2(Env,FT,CName,DomSet),!,
    Lambda1 = lambda(ti(body([ti(decl([Param],ti(basetype(set(ArgType)),set(ArgType))),none)],
    [ti(member(ti(ref(Param,[]),ArgType),DomSet),bool)]),
    set(schema([field(Param,ArgType)]))),
    ti(ftconstructor(FT,CName,ti(ref(Param,[]),ArgType)),freetype(FT))),
    z_counter('param__',P),Param=name(P,''),
    ggsimplify1(ti(Lambda1,set(tuple([ArgType,freetype(FT)]))),Env,ti(Lambda,_)).

ggsimplify2(ref(FT,[]),set(freetype(FT)),Env,Result) :-
    ftget(Env,FT,Arms,simpl),!,
    z_counter('param__',P),Param=name(P,''),
    Result1 = comp(ti(body([ti(decl([Param],ti(basetype(set(freetype(FT))),set(freetype(FT)))),none)],
    Constraints),BType),ti(nothing,none)),
    BType = set(schema([field(Param,freetype(FT))])),
    create_constraints(Arms,FT,ti(ref(Param,[]),freetype(FT)),Constraints),
    ggsimplify1(ti(Result1,set(freetype(FT))),Env,ti(Result,_)).

ggsimplify2(ref(FT,[]),set(freetype(FT)),Env,ref(Global,[])) :-
    ftget(Env,FT,_,rec),!,
    global_ft_constant(FT,Global).

ggsimplify_fixpoint(Expr,T,Env,Result) :-
    ggsimplify2(Expr,T,Env,Inter),
    Expr \= Inter,
    !,ggsimplify_fixpoint(Inter,T,Env,Result).

ggsimplify_fixpoint(Expr,_,_,Expr).

global_ft_constant(name(S,Deco),name(Global,Deco)) :-
    atom_concat(S,'__rec',Global).

ignore_name(name('\\prozignore','')).

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

insert_selects([Expr|Rest],Var,Fields,[IExpr|IRest]) :-
    !,insert_selects(Expr,Var,Fields,IExpr),
    insert_selects(Rest,Var,Fields,IRest).

insert_selects(ti(ref(Name,[]),Type),Var,Fields,ti(select(Var,Name),Type)) :-
    member(field(Name,_),Fields),!.

insert_selects(Expr,Var,Fields,Result) :-
    znamespacet(Expr,Outer,Inner,Names,NOuter,NInner,Result),
    !,insert_selects(Outer,Var,Fields,NOuter),
    remove_fields_by_name(Fields,Names,NewFields),
    insert_selects(Inner,Var,NewFields,NInner).

insert_selects(Expr,Var,Fields,Result) :-
    zexpr_conversiont(Expr,OldSubs,NewSubs,Result),
    insert_selects(OldSubs,Var,Fields,NewSubs).

is_cyclic(Node,Freetype,Refs,_) :-
    member(ref(Node,Freetype),Refs),!.

is_cyclic(Node,Freetype,Refs,Old) :-
    member(ref(Node,Next),Refs),
    \+ member(Next,Old),
    is_cyclic(Next,Freetype,Refs,[Next|Old]),!.

is_cyclic_freetype(Refs,FreetypeDefinition) :-
    ti_expr(FreetypeDefinition,data(FreetypeName,_Arms)),
    is_cyclic(FreetypeName,FreetypeName,Refs,[]).

is_ftconstant2(Env,FT,Name) :-
    ftget(Env,FT,Arms,_),
    member(ti(arm(Name,ti(nothing,none)),_),Arms),!.

is_ftconstructor2(Env,FT,CName,DomSet) :-
    ftget(Env,FT,Arms,_),
    member(ti(arm(CName,ti(just(DomSet),none)),_),Arms),!.

is_ftconstructor_expression(ti(ref(CName,[]),set(tuple([IType,freetype(FT)]))),Env,FT,CName,IType) :-
    is_ftconstructor2(Env,FT,CName,_).

is_ftconstructor_expression(ti(postop(name('\\inv',''),Arg),set(tuple([IType,freetype(FT)]))),
    Env,FT,CName,IType) :-
    is_ftdestructor_expression(Arg,Env,FT,CName,IType).

is_ftdestructor_expression(ti(postop(name('\\inv',''),Arg),set(tuple([freetype(FT),_]))),Env,FT,CName,IType) :-
    is_ftconstructor_expression(Arg,Env,FT,CName,IType).

make_z_bag_count(Bag,Element,Count) :-
    make_z_inop('\\bcount',num,Bag,Element,Count).

make_z_domain(Relation,Domain) :-
    ti_type(Relation,RelType),
    RelType = set(tuple([A,_])),
    make_z_expr(apply(DomOp,Relation),set(A),Domain),
    make_z_expr(ref(name('\\dom',''),[]),set(tuple([RelType,set(A)])),DomOp).

make_z_expr(Expr,Type,Z) :-
    ti_expr(Z,Expr), ti_type(Z,Type).

make_z_inop(Op,Type,A,B,Expr) :-
    make_z_expr(inop(name(Op,''),A,B),Type,Expr).

make_z_inrel(Op,A,B,Expr) :-
    make_z_expr(inrel(name(Op,''),A,B),bool,Expr).

make_z_member(Elem,Set,Member) :-
    make_z_expr(member(Elem,Set),bool,Member).

make_z_number(Number,Expr) :-
    make_z_expr(number(Number),num,Expr).

make_z_tuple(Elements,Types,Expr) :-
    make_z_expr(tuple(Elements),tuple(Types),Expr).

prepare_freetype_env(TypedDef,FreetypeEnv,NewDefs) :-
    findall(ti(data(Freetype,Arms),Type),
    member(ti(data(Freetype,Arms),Type),TypedDef),
    DataEnv),
    ( DataEnv = [] ->
    FreetypeEnv = [],NewDefs = TypedDef
    ;
    split_recursive_freetypes(DataEnv,Recursive,NonRecursive),
   
    findall(ft(F,rec),member(F,Recursive),FRec),
    findall(ft(F,simpl),member(F,NonRecursive),FNRec),
    append(FRec,FNRec,FreetypeEnv),
   
    maplist(create_axdef_for_recfreetype,Recursive,Axdefs),
    append(Axdefs,TypedDef,NewDefs)
).

prepare_given_env(TypedDef,GivenEnv) :-
    findall(G,
    (member(ti(given(Ns),none),TypedDef),member(G,Ns)),
    Given),
    findall(N,member(ti(namedset(N,_),none),TypedDef),NamedSets),
    append(Given,NamedSets,GivenEnv).

presimplify(decl(Vars,ti(_,Type)),_,_,decl(Vars,ti(basetype(Type),Type))) :- !.

presimplify(pregen(Name,_),Type,_,basetype(Type)) :- ignore_name(Name).

presimplify(apply(ti(ref(name('\\proztestftconstant',''),[]),_),Arg),
    freetype(FT),_,ftconstant(FT,Case)) :-
    !,
    (Arg = ti(tuple([ti(ref(FT,[]),set(freetype(FT))),
    ti(ref(Case,[]),freetype(FT))]),_)
    -> true
    ; add_error(ztransformations,'wrong arguments for \\proztestftconstant')).

presimplify(apply(ti(ref(name('\\proztestftconstructor',''),[]),_),Arg),
    freetype(FT),_,ftconstructor(FT,Case,Inner)) :-
    !,
    (Arg = ti(tuple([ti(ref(FT,[]),set(freetype(FT))),
    ti(ref(Case,[]),set(tuple([_,freetype(FT)]))),
    Inner]),_)
    -> true
    ; add_error(ztransformations,'wrong arguments for \\proztestftconstructor')).

presimplify(apply(ti(ref(name('\\proztestftdestructor',''),[]),_),Arg),
    _,_,ftdestructor(FT,Case,ti(Inner,freetype(FT)))) :-
    !,
    (Arg = ti(tuple([ti(ref(FT,[]),set(freetype(FT))),
    ti(ref(Case,[]),set(tuple([_,freetype(FT)]))),
    ti(Inner,freetype(FT))]),_)
    -> true
    ; add_error(ztransformations,'wrong arguments for \\proztestftdestructor')).

presimplify(prerel(name('\\proztestftcase',''),Arg),_,_,ftcase(FT,Case,ti(Expr,freetype(FT)))) :-
    !,
    ((Arg = ti(tuple([ti(ref(FT,[]),set(freetype(FT))),
    ti(ref(Case,[]),CaseType),
    ti(Expr,freetype(FT))]),_),
    (CaseType=freetype(FT);CaseType=set(tuple([_,freetype(FT)]))))
    -> !,true
    ; add_error(ztransformations,'wrong arguments for \\proztestftcase')).

presimplify(apply(FunTi,ArgTi),IType,Env,ftdestructor(FT,CName,ArgTi)) :-
    is_ftdestructor_expression(FunTi,Env,FT,CName,IType).

presimplify(member(Expr,ti(apply(ti(ref(name('\\ran',''),[]),_),Constructor),set(freetype(FT)))),
    bool,Env,ftcase(FT,CName,Expr)) :-
    is_ftconstructor_expression(Constructor,Env,FT,CName,_).

presimplify(member(Expr,ti(apply(ti(ref(name('\\dom',''),[]),_),Destructor),set(freetype(FT)))),
    bool,Env,ftcase(FT,CName,Expr)) :-
    is_ftdestructor_expression(Destructor,Env,FT,CName,_).

presimplify(inrel(name('\\notin',''),Expr,
    ti(apply(ti(ref(name('\\ran',''),[]),_),Constructor),set(freetype(FT)))),
    bool,Env,not(ti(ftcase(FT,CName,Expr),bool))) :-
    is_ftconstructor_expression(Constructor,Env,FT,CName,_).

presimplify(inrel(name('\\notin',''),Expr,
    ti(apply(ti(ref(name('\\dom',''),[]),_),Destructor),set(freetype(FT)))),
    bool,Env,not(ti(ftcase(FT,CName,Expr),bool))) :-
    is_ftdestructor_expression(Destructor,Env,FT,CName,_).

presimplify_fixpoint(Expr,T,Env,Result) :-
    presimplify(Expr,T,Env,Inter),
    Expr \= Inter,
    !,presimplify_fixpoint(Inter,T,Env,Result).

presimplify_fixpoint(Expr,_,_,Expr).

remove_ignore_decl([],[]).

remove_ignore_decl([define(Sets,body(Decls,Wheres))|Rest],Result) :-
    !,remove_ignore_decl2(Decls,NewDecls),
    (NewDecls = [], Wheres = [] ->
    Result = IRest;
    Result = [define(Sets,body(NewDecls,Wheres))|IRest]),
    remove_ignore_decl(Rest,IRest).

remove_ignore_decl([Def|Rest],[Def|IRest]) :-
    remove_ignore_decl(Rest,IRest).

remove_ignore_decl2([],[]).

remove_ignore_decl2([decl(Vars,Type)|Rest],Result) :-
    ignore_name(Ignore),
    remove_all(Vars,[Ignore],NewVars),
    (NewVars = [] ->
    Result = IRest;
    Result = [decl(NewVars,Type)|IRest]),
    remove_ignore_decl2(Rest,IRest).

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

removeabbr2([Expr|ERest],Eqeqs,[Result|RRest]) :-
    !,removeabbr2(Expr,Eqeqs,Result),
    removeabbr2(ERest,Eqeqs,RRest).

removeabbr2(ref(Name,Values),Eqeqs,Result) :-
    member(eqeq(lhs(Name,Params),EqExpr),Eqeqs),
    !,insert_parameter(EqExpr,Params,Values,Result1),
    % If the inserted expression has the form body(_,_), it
    % is an schema expression and will be marked with sexpr.
    (EqExpr = body(_,_) ->
    Result2 = sexpr(EqExpr);
    Result2 = Result1),
    % Check if the inserted expression makes use of another abbreviation.
    removeabbr2(Result2,Eqeqs,Result).

removeabbr2(Expr,Eqeqs,Result) :-
    zexpr_conversion(Expr,Old,New,Result),
    removeabbr2(Old,Eqeqs,New).

removeabbreviations(In,Out) :-
    findeqeq(In,NonEqeqs,EqEqs),
    (EqEqs = [] ->
    In = Out ;
    removeabbr2(NonEqeqs,EqEqs,Out)).

removesexpr(In,Out) :- removesexpr2(In,Out).

removesexpr2([],[]) :- !.

removesexpr2([Expr|Rest],[RExpr|RRest]) :-
    !,removesexpr2(Expr,RExpr),
    removesexpr2(Rest,RRest).

removesexpr2(ti(sexpr(SexprTi),SType),ti(comp(Body,ti(nothing,none)),SType)) :-
    !,
    SType = set(Type),Type=schema(Fields),
    z_counter('rec__',Name),Var = name(Name,''),
   
    Body = ti(body([Decl],NewWheres),set(schema([field(Var,Type)]))),
    Decl = ti(decl([Var],ti(basetype(SType),SType)),none),
    removesexpr2(SexprTi,ti(body(_,Wheres),_)),
    insert_selects(Wheres,ti(ref(Var,[]),Type),Fields,NewWheres).

removesexpr2(Expr,Result) :-
    zexpr_conversiont(Expr,OldSubs,NewSubs,Result),
    removesexpr2(OldSubs,NewSubs).

replace_cleanup(Wheres,Var,New,Condition) :-
    replace_expression(Wheres,Var,New,Conditions),
    clean_wheret(Conditions,CConditions),
    z_conjunctiont(CConditions,Condition).

replace_expression(ti(ref(Expr,[]),_),Expr,New,New) :- !.

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

replace_expression([E|Rest],Old,New,[RE|RRest]) :-
    !,replace_expression(E,Old,New,RE),
    replace_expression(Rest,Old,New,RRest).

replace_expression(Expr,Old,New,RExpr) :-
    znamespacet(Expr,Outer,Inner,Names,NOuter,NInner,RExpr),!,
    replace_expression(Outer,Old,New,NOuter),
    (member(Old,Names) ->
    Inner = NInner;
    replace_expression(Inner,Old,New,NInner)).

replace_expression(Expr,Old,New,RExpr) :-
    zexpr_conversiont(Expr,OldSubs,NewSubs,RExpr),
    replace_expression(OldSubs,Old,New,NewSubs).