z_type2(ref(Name,Params),Env,ref(Name,NewParams),Type) :-
( lookup_type(Env,Name,T) ->
( nonvar(T),T=generic(GenParams,GenType) ->
prepare_generic(Params,Env,GenType,GenParams,Type)
; Type=T -> true
; add_warning(proz,'Type mismatch: ',Name:Type:T),fail
),
update_params(Name,Params,NewParams)
;
add_error(proz,'Internal error: Unknown type of ', Name), fail).
z_type2(number(N),_,number(N),num).
z_type2(apply(Ref,Arg),Env,apply(RefTI,ArgTI),ResultType) :-
z_type(Ref,Env,FunType,RefTI),
zrel(ArgType,ResultType,FunType),
z_type(Arg,Env,ArgType,ArgTI).
z_type2(inop(Name,A,B),Env,inop(Name,Ati,Bti),Type) :-
ti_expr(ApplyTI,apply(_,ArgTI)),
ti_expr(ArgTI,tuple([Ati,Bti])),
z_type(apply(ref(Name,[]),tuple([A,B])),Env,Type,ApplyTI).
z_type2(ingen(Name,A,B),Env,ingen(Name,Ati,Bti),Type) :-
ti_expr(InopTI,inop(_,Ati,Bti)),
z_type(inop(Name,A,B),Env,Type,InopTI).
z_type2(postop(Name,Arg),Env,postop(Name,ArgTI),Type) :-
ti_expr(ApplyTI,apply(_,ArgTI)),
z_type(apply(ref(Name,[]),Arg),Env,Type,ApplyTI).
z_type2(pregen(Name,Arg),Env,pregen(Name,ArgTI),Type) :-
z_type2(postop(Name,Arg),Env,postop(_,ArgTI),Type).
z_type2(inrel(Name,A,B),Env,inrel(Name,Ati,Bti),Type) :-
ti_expr(MemTI,member(TupleTI,_)),
ti_expr(TupleTI,tuple([Ati,Bti])),
z_type(member(tuple([A,B]),ref(Name,[])),Env,Type,MemTI).
z_type2(prerel(Name,Arg),Env,prerel(Name,ArgTI),Type) :-
ti_expr(MemTI,member(ArgTI,_)),
z_type(member(Arg,ref(Name,[])),Env,Type,MemTI).
z_type2(equal(A,B), Env, equal(Ati,Bti), bool) :-
z_types_common([A,B],Env,_,[Ati,Bti]).
z_type2(member(A,B), Env, member(Ati,Bti), bool) :-
z_type(A,Env,Type,Ati),
z_type(B,Env,set(Type),Bti).
z_type2(power(A), Env, power(Ati),set(Type)) :-
z_type(A,Env,Type,Ati).
z_type2(cross(Args), Env, cross(TypeInfos), set(tuple(Types))) :-
z_type_sets(Args, Env, Types, TypeInfos).
z_type2(tuple(Args), Env, tuple(TypeInfos), tuple(Types)) :-
z_type_l(Args, Env, Types,TypeInfos).
z_type2(if(If,Then,Else), Env, if(Ifti,Thenti,Elseti), Type) :-
z_type(If,Env,bool,Ifti),
z_type(Then,Env,Type,Thenti),
z_type(Else,Env,Type,Elseti).
z_type2(ext(Expressions), Env, ext(TypeInfos), set(Type)) :-
z_types_common(Expressions,Env,Type,TypeInfos).
z_type2(seq(Expressions), Env, seq(TypeInfos), Type) :-
zseq(IType,Type),
z_types_common(Expressions,Env,IType,TypeInfos).
z_type2(bag(Expressions), Env, bag(TypeInfos), set(tuple([Type,num]))) :-
z_types_common(Expressions,Env,Type,TypeInfos).
z_type2(theta(Name,Deco,Renamings), Env, theta(Name,Deco,Renamings), Type) :-
z_type(sref(Name,'',[],[]),Env,set(Type),_).
z_type2(sexpr(Sexpr), Env, sexpr(SexprTi), Type) :-
z_type(Sexpr,Env,Type,SexprTi).
z_type2(select(Record,Field), Env, select(RecordTi,Field), Type) :-
z_type(Record,Env,schema(Fields),RecordTi),
type_of_field(Fields,Field,Type).
z_type2(lambda(Body,Expr), Env, lambda(BodyTi,ExprTi), Type) :-
Body = body(Decls,_),
declaration_tuple(Decls,Env,Tuple),
ti_expr(TypeInfo,comp(BodyTi,JustTi)),
ti_expr(InopTi,inop(_,_,ExprTi)),
ti_expr(JustTi,just(InopTi)),
z_type(comp(Body,just(inop(name('\\mapsto',''),Tuple,Expr))),
Env,Type,TypeInfo).
z_type2(comp(Body,Expr), Env, comp(BodyTi,ExprTi), set(Type)) :-
ti_expr(TypeInfo,mu(BodyTi,ExprTi)),
z_type(mu(Body,Expr),Env,Type,TypeInfo).
z_type2(mu(Body,MuExpr), Env, mu(BodyTi,ExprTypeInfo), Type) :-
( MuExpr = nothing ->
ExprTypeInfo = ti(nothing,none),
Body = body(Decls,_),declaration_tuple(Decls,Env,Tuple),
ti_expr(TypeInfo,mu(BodyTi,_)),
z_type(mu(Body,just(Tuple)), Env, Type, TypeInfo)
; MuExpr = just(Expr) ->
z_type_body(Body,Env,_,BodyTi,Subenv),
z_type(just(Expr),Subenv,_,ExprTypeInfo),
ti_expr(ExprTypeInfo,just(ExprTi)),
ti_type(ExprTi,Type) ).
z_type2(letexpr(Letdefs,Expr), Env, letexpr(Lettis,ExprTi), Type) :-
types_in_let(Letdefs,Env,LetTypes,Lettis),
create_subenv(Env,LetTypes,LetEnv),
z_type(Expr,LetEnv,Type,ExprTi).
z_type2(nothing,_,nothing,none).
z_type2(just(Expr),Env,just(ExprTi),none) :-
z_type(Expr,Env,_,ExprTi).
z_type2(falsity, _, falsity, bool).
z_type2(truth, _, truth, bool).
z_type2(forall(Body,Expr), Env, forall(BodyTi,ExprTi), bool) :-
z_type_body(Body,Env,_,BodyTi,Subenv),
z_type(Expr,Subenv,bool,ExprTi).
z_type2(exists(Body,Expr), Env, exists(BodyTi,ExprTi), Type) :-
z_type2(forall(Body,Expr),Env,forall(BodyTi,ExprTi),Type).
z_type2(exists1(Body,Expr), Env, exists1(BodyTi,ExprTi), Type) :-
z_type2(forall(Body,Expr),Env,forall(BodyTi,ExprTi),Type).
z_type2(and(A,B), Env, and(Ati,Bti), bool) :-
z_type(A,Env,bool,Ati),z_type(B,Env,bool,Bti).
z_type2(or(A,B), Env, or(Ati,Bti), Type) :-
z_type2(and(A,B),Env,and(Ati,Bti),Type).
z_type2(implies(A,B), Env, implies(Ati,Bti), Type) :-
z_type2(and(A,B),Env,and(Ati,Bti),Type).
z_type2(equiv(A,B), Env, equiv(Ati,Bti), Type) :-
z_type2(and(A,B),Env,and(Ati,Bti),Type).
z_type2(not(E), Env, not(Eti), bool) :- z_type(E,Env,bool,Eti).
z_type2(letpred(Letdefs,Expr), Env, letpred(Letties,ExprTi), bool) :-
z_type2(letexpr(Letdefs,Expr), Env, letexpr(Letties,ExprTi), bool).
z_type2(spred(SExpr), Env, spred(SExprTi), bool) :-
z_type(SExpr,Env,set(schema(_)),SExprTi).
z_type2(sref(Name,Deco,ParamValues,Renamings), Env, sref(Name,Deco,ParamValues,Renamings), Type) :-
zlookup_schema(Env,Name,ParamNames,Expr),
z_type_schemabody(Expr,Deco,ParamNames,ParamValues,Renamings,Env,Type,_).
z_type2(sand(A,B), Env, sand(Ati,Bti), Type) :-
logical_bin_schema(A,B,Env,Ati,Bti,Type).
z_type2(sor(A,B), Env, sor(Ati,Bti), Type) :-
logical_bin_schema(A,B,Env,Ati,Bti,Type).
z_type2(simplies(A,B), Env, simplies(Ati,Bti), Type) :-
logical_bin_schema(A,B,Env,Ati,Bti,Type).
z_type2(sequiv(A,B), Env, sequiv(Ati,Bti), Type) :-
logical_bin_schema(A,B,Env,Ati,Bti,Type).
z_type2(snot(A), Env, snot(Ati), Type) :-
z_type(A,Env,Type,Ati).
z_type2(sforall(Body,Schema), Env, sforall(BodyTi,SchemaTi), Type) :-
type_schema_quantifier(Body,Schema,Env,BodyTi,SchemaTi,Type).
z_type2(sexists(Body,Schema), Env, sexists(BodyTi,SchemaTi), Type) :-
type_schema_quantifier(Body,Schema,Env,BodyTi,SchemaTi,Type).
z_type2(sexists1(Body,Schema), Env, sexists1(BodyTi,SchemaTi), Type) :-
type_schema_quantifier(Body,Schema,Env,BodyTi,SchemaTi,Type).
z_type2(hide(Schema,Vars), Env, hide(SchemaTi,Vars), set(schema(Fields))) :-
z_type(Schema,Env,set(schema(InnerFields)),SchemaTi),
remove_fields_by_name(InnerFields,Vars,UFields),
normalize_fields(UFields,Fields).
z_type2(fatsemi(A,B), Env, fatsemi(Ati,Bti), set(schema(Fields))) :-
get_fields(A,B,Env,Ati,Bti,FieldsA,FieldsB),
composite_fields(FieldsA,FieldsB,Out,In),
remove_fields_by_name(FieldsA,Out,Aall),
remove_fields_by_name(FieldsB,In,Ball),
append_not_duplicate(Aall,Ball,UFields),
normalize_fields(UFields,Fields).
z_type2(project(A,B), Env, project(Ati,Bti), set(schema(Fields))) :-
z_type(A,Env,set(schema(_)),Ati),
z_type(B,Env,set(schema(Fields)),Bti).
z_type2(pre(Schema), Env, pre(SchemaTi), set(schema(Fields))) :-
z_type(Schema,Env,set(schema(AllFields)),SchemaTi),
findall(name(Name,Deco),
(member(field(name(Name,Deco),_),AllFields),
member(Deco,['\'','!'])),
ToRemove),
remove_fields_by_name(AllFields,ToRemove,UFields),
normalize_fields(UFields,Fields).
z_type2(pipe(A,B), Env, pipe(Ati,Bti), set(schema(Fields))) :-
z_type(A,Env,set(schema(FieldsA)),Ati),
z_type(B,Env,set(schema(FieldsB)),Bti),
pipe_fields(FieldsA,FieldsB,Out,In),
remove_fields_by_name(FieldsA,Out,AwoO),
remove_fields_by_name(FieldsB,In,BwoI),
append_not_duplicate(AwoO,BwoI,UFields),
normalize_fields(UFields,Fields).
z_type2(body(Decl,Where), Env, TypedBody, Type) :-
z_type_body(body(Decl,Where),Env,Type,BodyTi,_),
ti_expr(BodyTi,TypedBody).
z_type2(text(Text), Env, text(TextTi), Type) :-
z_type(Text,Env,Type,TextTi).
z_type2(given(Vars), _, given(Vars), none).
z_type2(namedset(SetName,Vars), _, namedset(SetName,Vars), none).
z_type2(data(Name,Arms), Env, data(Name,ArmsTi), none) :-
z_type_arms(Arms,Env,Name,ArmsTi).
z_type2(sdef(Head,Body), Env, sdef(Head,BodyTi), none) :-
z_type_schema(Head,Body,Env,BodyTi).
z_type2(defeq(Head,Body), Env, defeq(Head,BodyTi), none) :-
z_type_schema(Head,Body,Env,BodyTi).
z_type2(eqeq(lhs(Name,ParamNames),Expr), Env, eqeq(lhs(Name,ParamNames),ExprTi), none) :-
create_param_env(ParamNames,Env,ParamEnv),
z_type(Expr,ParamEnv,PType,ExprTi),
generic_type(ParamNames,PType,Type),
lookup_type(Env,Name,Type).
z_type2(axdef(Body), Env, axdef(BodyTi), none) :-
z_type_globaldef(Body,[],Env,BodyTi).
z_type2(define(ParamNames,Body), Env, define(ParamNames,BodyTi), none) :-
z_type_globaldef(Body,ParamNames,Env,BodyTi).
z_type2(pred(Pred), Env, pred(PredTi), none) :-
z_type(Pred,Env,bool,PredTi).
z_type2(basetype(Type), _, basetype(Type), Type).
z_type2(binding(Bindings), Env, binding(BindingTis), schema(Fields)) :-
z_type_binding(Bindings,Env,UFields,BindingTis),
normalize_fields(UFields,Fields).
z_type2(ftconstant(Freetype,Name), _, ftconstant(Freetype,Name),freetype(Freetype)).
z_type2(ftconstructor(Freetype,Name,Expr), Env,
ftconstructor(Freetype,Name,ExprTi), freetype(Freetype)) :-
z_type(Expr,Env,_,ExprTi).
z_type2(ftdestructor(Freetype,Name,Expr), Env, ftdestructor(Freetype,Name,ExprTi), Type) :-
z_type(Expr,Env,freetype(Freetype),ExprTi),
lookup_type(Env,Name,ConstructorType),
zrel(Type,freetype(Freetype),ConstructorType).
z_type2(ftcase(Freetype,Name,Expr), Env, ftcase(Freetype,Name,ExprTi), bool) :-
z_type(Expr,Env,freetype(Freetype),ExprTi).