schemaexpansion

add_char_tuple(Functor,Body,Env,Result) :-
    Body=body(Decl,_),
    characteristic_tuple(Decl,Env,Exprlist),
    maybetuple(Exprlist,Expression),
    functor(R,Functor,2),
    arg(1,R,Body),
    arg(2,R,just(Expression)),
    sexpansion(R,Env,Result).

add_simple_types_info(Env,env(Env,STypes)) :-
    env_z_defs(Env,Def),
    findall(Name,(member(given(L),Def),member(Name,L)),Givens),
    findall(Name,member(namedset(Name,_),Def),Namedsets),
    append(Givens,Namedsets,STypes).

append_decls(A,B,R) :- append(A,B,M),clean_decl(M,R).

append_nonempty_decl(Vars,Type,Rest,Result) :-
    (Vars = [] ->
    Result = Rest;
    Result = [decl(Vars,Type)|Rest]).

characteristic_tuple([],_,[]).

characteristic_tuple([D|Rest],Env,Exprlist) :-
    characteristic_tuple2(D,Env,Exprs),
    append(Exprs,Restlist,Exprlist),
    characteristic_tuple(Rest,Env,Restlist).

characteristic_tuple2(decl(Vars,_),_,References) :-
    names_to_references(Vars,References).

characteristic_tuple2(sdecl(sref(Name,Deco,Params,Renamings)),Env,[binding(Bindings)]) :-
    sexpansion(sref(Name,'',Params,[]),Env,body(Decls,_)),
    vars_of_decls(Decls,Vars),
    generate_bindings(Vars,Deco,Renamings,Bindings).

clean_decl(Decls,Cleaned) :-
    clean_decl2(Decls,[],Cleaned).

clean_decl2([],_,[]).

clean_decl2([decl(Vars,Type)|Rest],Before,Cleaned) :-
    filter_vars(Vars,Before,UniqueVars),
    (UniqueVars = [] ->
    Cleaned = RestCleaned;
    Cleaned = [decl(UniqueVars,Type)|RestCleaned]),
    append(UniqueVars,Before,NBefore),
    clean_decl2(Rest,NBefore,RestCleaned).

combine_schemas(A,B,DecoOut,DecoIn,Env,Expansion) :-
    sexpansion(A,Env,AE),sexpansion(B,Env,BE),
    zsplit(AE,AD,_),zsplit(BE,BD,_),
   
    find_vars_with_deco(AD,[DecoOut],OutVars),
    find_vars_with_deco(BD,[DecoIn],InVars),
    find_matching_vars(OutVars,InVars,DecoOut,DecoIn,RenamingsA,RenamingsB,LocalVars),
    rename_variables(AE,RenamingsA,AC),
    rename_variables(BE,RenamingsB,BC),
    sexpansion(hide(sand(AC,BC),LocalVars),Env,Expansion).

contains_sdecl(body(Decl,_)) :-
    contains_sdecl2(Decl).

contains_sdecl2([sdecl(_)|_]) :- !.

contains_sdecl2([_|R]) :- contains_sdecl(R).

decorate(Expr,'',Expr) :- !.

decorate(Expr,Deco,Result) :-
    zsplit(Expr,Decls,Where),
    decorate_renamings(Decls,Deco,Renamings),
    rename_variables(body(Decls,Where),Renamings,Result).

decorate_renamings([],_,[]).

decorate_renamings([decl(Vars,_)|DRest],Deco,Renamings) :-
    findall(rename(name(Name,NewDeco),name(Name,OldDeco)),
    (member(name(Name,OldDeco),Vars),atom_concat(OldDeco,Deco,NewDeco)),
    LRenamings),
    append(LRenamings,ORenamings,Renamings),
    decorate_renamings(DRest,Deco,ORenamings).

expand_and_split(Expr,Env,Decl,Where) :-
    sexpansion(Expr,Env,Expanded),
    zsplit(Expanded,Decl,Where).

expand_decls([],_,[],[]).

expand_decls([D|DRest],Env,DExpanded,WExpanded) :-
    expand_decls2(D,Env,DE,WE),
    append(DE,DERest,DExpanded),
    append(WE,WERest,WExpanded),
    expand_decls(DRest,Env,DERest,WERest).

expand_decls2(decl(Vars,Type),Env,[decl(Vars,EType)],Where) :-
    sexpansion(Type,Env,EType),
    generate_membership(Vars,EType,Where).

expand_decls2(sdecl(S),Env,Decls,Where) :-
    expand_and_split(S,Env,Decls,Where).

filter_vars([],_,[]).

filter_vars([Var|Rest],Existing,Result) :-
    (member(Var,Existing) -> Result = RestResult ; Result = [Var|RestResult]),
    filter_vars(Rest,Existing,RestResult).

find_common(ListA,ListB,UniqueA,UniqueB,Common) :-
    find_common2(ListA,ListB,ListA,UniqueA,UniqueB,Common).

find_common2([A|Rest],ListB,ListA,UniqueA,UniqueB,Common) :-
    ( member(A,ListB) ->
    (UniqueA = RUniqueA, Common = [A|RCommon])
    ;
    (UniqueA = [A|RUniqueA], Common = RCommon)),
    find_common2(Rest,ListB,ListA,RUniqueA,UniqueB,RCommon).

find_common2([],ListB,ListA,[],UniqueB,Common) :-
    find_common3(ListB,ListA,UniqueB,Common).

find_common3([B|Rest],ListA,UniqueB,Common) :-
    ( member(B,ListA) ->
    (UniqueB = RUniqueB, Common = [B|RCommon])
    ;
    (UniqueB = [B|RUniqueB], Common = RCommon)),
    find_common3(Rest,ListA,RUniqueB,RCommon).

find_common3([],_,[],[]).

find_matching_vars([],_,_,_,[],[],[]).

find_matching_vars([name(Name,DecoOut)|OutRest],InVars,
    DecoOut,DecoIn,
    [rename(New,name(Name,DecoOut))|ARest],
    [rename(New,name(Name,DecoIn))|BRest],
    [New|NewRest]) :-
    member(name(Name,DecoIn),InVars),!,
    z_counter('match__',NewName),New=name(NewName,''),
    find_matching_vars(OutRest,InVars,DecoOut,DecoIn,ARest,BRest,NewRest).

find_vars_with_deco(Decls,Decos,Postvars) :-
    findall(name(N,D),
    (member(decl(Vars,_),Decls),
    member(name(N,D),Vars),
    member(D,Decos)),
    Postvars).

generate_bindings([],_,_,[]).

generate_bindings([Fieldname|FRest],Deco,Renamings,[bindfield(Fieldname,ref(Refname,[]))|BRest]) :-
    Fieldname = name(OldName,OldDeco),
    atom_concat(OldDeco,Deco,NewDeco),
    (member(rename(Refname,name(OldName,NewDeco)),Renamings) ->
    !,true;
    Refname = name(OldName,NewDeco)),
    generate_bindings(FRest,Deco,Renamings,BRest).

generate_membership([],_,[]).

generate_membership([Var|VRest],Set,[member(ref(Var,[]),Set)|MRest]) :-
    generate_membership(VRest,Set,MRest).

lookup(env(Env,_),Name,Params,Expr) :- zlookup_schema(Env,Name,Params,Expr).

maybetuple([E],E) :- !.

maybetuple([A,B|R],tuple([A,B|R])).

names_to_references([],[]).

names_to_references([Name|Nrest],[ref(Name,[])|Rrest]) :-
    names_to_references(Nrest,Rrest).

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).

remove_vars_from_decls([],_,[],[]).

remove_vars_from_decls([decl(Vars,Type)|Rest],ToRemove,RestDecls,RemovedDecls) :-
    split_found_and_rest(Vars,ToRemove,RestVars,RemovedVars),
    append_nonempty_decl(RestVars,Type,RRestDecls,RestDecls),
    append_nonempty_decl(RemovedVars,Type,RRemovedDecls,RemovedDecls),
    remove_vars_from_decls(Rest,ToRemove,RRestDecls,RRemovedDecls).

rename_decl_vars([],_,[]).

rename_decl_vars([Old|ORest],Renamings,[New|NRest]) :-
    (memberchk(rename(New,Old),Renamings) -> true ; Old = New),
    rename_decl_vars(ORest,Renamings,NRest).

rename_decls([],_,[]).

rename_decls([sdecl(S)|DRest],Renamings,[sdecl(S)|RRest]) :-
    !,rename_decls(DRest,Renamings,RRest).

rename_decls([decl(Vars,Type)|DRest],Renamings,[decl(RVars,Type)|RRest]) :-
    !,rename_decl_vars(Vars,Renamings,RVars),
    rename_decls(DRest,Renamings,RRest).

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

rename_variables(body(Decls,Where),Renamings,body(RDecls,RWhere)) :-
    !,
    rename_decls(Decls,Renamings,RDecls),
    rename_variables2(Where,Renamings,RWhere).

rename_variables(Expr,Renamings,Result) :- rename_variables2(Expr,Renamings,Result).

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

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

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

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

rename_variables2(Expr,Renamings,Result) :-
    zexpr_conversion(Expr,Subs,PSubs,Result),
    rename_variables2(Subs,Renamings,PSubs).

sexpansion(In,Out) :-
    create_initial_zenvironment(In,Env),
    add_simple_types_info(Env,SEnv),
    sexpansion(In,SEnv,Out).

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

sexpansion([E|Rest],Env,[Exp|ERest]) :-
    !,sexpansion(E,Env,Exp),
    sexpansion(Rest,Env,ERest).

sexpansion(sref(Name,Deco,ParamValues,Renamings),Env,Result) :-
    !,
    lookup(Env,Name,Params,Expr),
    sexpansion(Expr,Env,Expansion),
    same_length(ParamValues,Params),
    insert_parameter(Expansion,Params,ParamValues,PExp),
    decorate(PExp,Deco,DExp),
    rename_variables(DExp,Renamings,Result).

sexpansion(body(Decls,Where),Env,body(EDecl,EWhere)) :-
    !,expand_decls(Decls,Env,ExpandedDeclsD,NWhere),
    clean_decl(ExpandedDeclsD,EDecl),
    append(NWhere,ExWhere,DWhere),
    sexpansion(Where,Env,ExWhere),
    clean_where(DWhere,EWhere).

sexpansion(text(S),Env,Expansion) :-
    !,sexpansion(S,Env,Expansion).

sexpansion(sand(A,B),Env,Expanded) :-
    !,sexpansion(body([sdecl(A),sdecl(B)],[]),Env,Expanded).

sexpansion(sor(A,B),Env,body(EDecl,EWhere)) :-
    !,expand_and_split(A,Env,DA,WA),
    expand_and_split(B,Env,DB,WB),
    append_decls(DA,DB,EDecl),
    find_common(WA,WB,UA,UB,Common),
    z_conjunction(UA,AExpr),
    z_conjunction(UB,BExpr),
    z_disjunction([AExpr,BExpr],Or),
    append(Common,[Or],EWhere).

sexpansion(simplies(A,B),Env,Expansion) :-
    !,sexpansion_logic(implies,A,B,Env,Expansion).

sexpansion(sequiv(A,B),Env,Expansion) :-
    !,sexpansion_logic(equiv,A,B,Env,Expansion).

sexpansion(snot(S),Env,body(Decls,[not(Condition)])) :-
    !,expand_and_split(S,Env,Decls,Where),
    z_conjunction(Where,Condition).

sexpansion(sforall(Body,S),Env,Expansion) :-
    !,sexpansion_quantifier(forall,Body,S,Env,Expansion).

sexpansion(sexists(Body,S),Env,Expansion) :-
    !,sexpansion_quantifier(exists,Body,S,Env,Expansion).

sexpansion(sexists1(Body,S),Env,Expansion) :-
    !,sexpansion_quantifier(exists1,Body,S,Env,Expansion).

sexpansion(pre(S),Env,Expansion) :-
    !,sexpansion(S,Env,SE),zsplit(SE,Decls,_),
    find_vars_with_deco(Decls,['\'','!'],PostVars),
    sexpansion(hide(SE,PostVars),Env,Expansion).

sexpansion(hide(S,VarsToHide),Env,body(NewDecls,[Exists])) :-
    !,Exists = exists(body(ExistsDecls,Where),truth),
    expand_and_split(S,Env,Decls,Where),
    remove_vars_from_decls(Decls,VarsToHide,NewDecls,ExistsDecls).

sexpansion(project(A,B),Env,Expansion) :-
    !,sexpansion(A,Env,AE),sexpansion(B,Env,BE),
    zsplit(AE,AD,_),zsplit(BE,BD,_),
    vars_of_decls(AD,VarsA),
    vars_of_decls(BD,VarsB),
    remove_all(VarsA,VarsB,VarsToRemove),
    sexpansion(hide(sand(AE,BE),VarsToRemove),Env,Expansion).

sexpansion(fatsemi(A,B),Env,Expansion) :-
    !,combine_schemas(A,B,'\'','',Env,Expansion).

sexpansion(pipe(A,B),Env,Expansion) :-
    !,combine_schemas(A,B,'!','?',Env,Expansion).

sexpansion(spred(S),Env,Expansion) :-
    !,expand_and_split(S,Env,_,Where),
    z_conjunction(Where,Expansion).

sexpansion(comp(Body,nothing),Env,Expansion) :-
    contains_sdecl(Body),!,
    add_char_tuple(comp,Body,Env,Expansion).

sexpansion(mu(Body,nothing),Env,Expansion) :-
    contains_sdecl(Body),!,
    add_char_tuple(mu,Body,Env,Expansion).

sexpansion(lambda(Body,Result),Env,comp(ExpBody,just(Expression))) :-
    Expression = tuple([Argument,ExpResult]),
    contains_sdecl(Body),!,
    sexpansion(Result,Env,ExpResult),
    sexpansion(comp(Body,nothing),Env,comp(ExpBody,just(Argument))).

sexpansion(theta(Name,Deco,Renamings),Env,binding(Bindings)) :-
    !,schema_vars(sref(Name,'',[],[]),Env,Vars),
    generate_bindings(Vars,Deco,Renamings,Bindings).

sexpansion(Expr,Env,Expansion) :-
    zexpr_conversion(Expr,Subs,ESubs,Expansion),
    sexpansion(Subs,Env,ESubs).

sexpansion_logic(Junctor,A,B,Env,body(Decl,[Condition])) :-
    expand_and_split(A,Env,DA,WA),
    expand_and_split(B,Env,DB,WB),
    append_decls(DA,DB,Decl),
    z_conjunction(WA,ExprA),
    z_conjunction(WB,ExprB),
    Condition =.. [Junctor,ExprA,ExprB].

sexpansion_quantifier(Quantifier,QBody,S,Env,body(NewSDecls,[Quant])) :-
    functor(Quant,Quantifier,2),
    arg(1,Quant,body(QDecls,QWhere)), arg(2,Quant,Expr),
    %Quant =.. [Quantifier,body(QDecls,QWhere),Expr],
    expand_and_split(QBody,Env,QDecls,QWhere),
    expand_and_split(S,Env,SDecls,SWhere),
    vars_of_decls(QDecls,QVars), remove_vars_from_decls(SDecls,QVars,NewSDecls,_),
    z_conjunction(SWhere,Expr).

split_found_and_rest([],_,[],[]).

split_found_and_rest([Var|VRest],ToRemove,RRest,[Var|RRemoved]) :-
    member(Var,ToRemove),!,
    split_found_and_rest(VRest,ToRemove,RRest,RRemoved).

split_found_and_rest([Var|VRest],ToRemove,[Var|RRest],RRemoved) :-
    split_found_and_rest(VRest,ToRemove,RRest,RRemoved).

vars_of_decls(Decls,Vars) :-
    findall(V,(member(decl(Vs,_),Decls),member(V,Vs)),Vars).

zsplit(body(Decl,Where),Decl,Where).