btype2(identifier(I1), Pos, Env, identifier(I), Type, Infos, TRin, TRout) :-
!, % In case the identifier is a list, join it with '.' (e.g. ['M',x] -> 'M.x')
(is_list(I1) -> ajoin_with_sep(I1,'.',I) ; I1=I),
% get the identifier's type from the type environment
lookup_type(I,Env,Pos,Type,TRin,TR1),
% copy also additional information from the environment,
lookup_infos(I,Env,AllInfos),
% but not all (e.g. no position information)
extract_id_information(AllInfos,Infos),
% an access to this identifier might be illegal, check this
(member(error(Error),AllInfos) -> store_typecheck_error(Error, Pos, TR1, TRout) ; TR1=TRout).
btype2(primed_identifier(Id,N), Pos, Env, identifier(FullId), Type, Infos, TRin, TRout) :-
!, % a primed identifier is of the form x$0, we just convert it to
% a normal identifier called "x$0" and type-check it.
number_suffix(Id,N,FullId),
btype(primed_identifier(Id,N),identifier(Pos,FullId),Env,Type,TId,TRin,TRout),
get_texpr_info(TId,Infos).
btype2(forall(Ids,EImplication), _, Env, forall(TIdentifiers,TDomain,TPred), pred, [], TRin, TRout) :-
!,add_ext_variables_with_info(Ids,Env,[introduced_by(forall)],TIdentifiers,Subenv,TRin,TR1),
ext2int(btype2,EImplication,Implication,IPos,_,_,_,_),
(btype_rewrite(Implication,Env,IPos,Implication2,IPos2) -> true % in case we have a definition we need to expand it now to transform it into an implication
; Implication2=Implication, IPos2=IPos),
% we expect an implication as predicate, if not, generate an error
( Implication2=implication(Domain,Pred) ->
btype(forall_domain(Ids),Domain,Subenv,pred,TDomain,TR1,TR2),
btype(forall_pred(Ids),Pred,Subenv,pred,TPred,TR2,TRout)
;
store_typecheck_error('expected implication in universal quantification ',IPos2,TR1,TR2),
create_texpr(truth,pred,[],TDomain),
btype(foralle_impl(Ids),EImplication,Subenv,pred,TPred,TR2,TRout)
).
btype2(external_function_call(FunName,FunParams,_FunDef,TypeParams,Decl), Pos, Env,
external_function_call(FunName,TFunParams), OutputType , [], TRin, TRout) :-
/* note: position info is automatically added to info field; hence [] ok */
(FunParams = [] -> InputType = empty_type, FullType = set(OutputType)
; FullType = set(set(couple(InputType,OutputType)))),
!, btype_external_call(FunName,TypeParams,FunParams,Decl,FullType,
InputType,Pos,Env,TFunParams,TRin,TRout).
btype2(external_pred_call(FunName,FunParams,_FunDef,TypeParams,Decl), Pos, Env,
external_pred_call(FunName,TFunParams), pred, [], TRin, TRout) :-
!, btype_external_call(FunName,TypeParams,FunParams,Decl,set(InputType),InputType,
Pos,Env,TFunParams,TRin,TRout).
btype2(external_subst_call(FunName,FunParams,_FunDef,TypeParams,Decl), Pos, Env,
external_subst_call(FunName,TFunParams), subst, [], TRin, TRout) :-
!, btype_external_call(FunName,TypeParams,FunParams,Decl,set(InputType),InputType,
Pos,Env,TFunParams,TRin,TRout).
btype2(integer(I), _, _, integer(I), integer, [], TR, TR) :- !.
btype2(integer_set(S), _, _, integer_set(S), set(integer), [], TR, TR) :- !.
btype2(real(I), _, _, real(I), real, [], TR, TR) :- !.
btype2(string(I), _, _, string(I), string, [], TR, TR) :- !, assert_machine_string(I).
btype2(assign(IdFuns,Exprs), Pos, Env, assign(TIdFuns,TExprs), subst, [], TRin, TRout) :-
!,
common_prefix(IdFuns,Exprs,IdFuns1,Exprs1,OK),
btype_l(IdFuns1,Env,Types,TIdFuns,TRin,TR1),
btype_l(Exprs1, Env,Types,TExprs, TR1, TR2),
foldl(check_assign_lhs(Env),TIdFuns,TR2,TR3),
( OK=same_length -> TRout=TR3
;
store_typecheck_error('different number of variables on left and right side of a substitution ',Pos,TR3,TRout)
).
btype2(becomes_element_of(Ids,Expr), _, Env, becomes_element_of(TIds,TExpr), subst, [], TRin, TRout) :-
!,btype_l(Ids,Env,Types,TIds,TRin,TR1),
foldl(check_assign_lhs(Env),TIds,TR1,TR2),
couplise_list(Types,Type),
btype(becomes_element_of(Ids),Expr,Env,set(Type),TExpr,TR2, TRout).
btype2(becomes_such(Ids,Pred), _, Env, becomes_such(TIds,TPred), subst, [], TRin, TRout) :-
!,btype_l(Ids,Env,_,TIds,TRin,TR1),
foldl(check_assign_lhs(Env),TIds,TR1,TR2),
% for each LHS identifier x (in Ids), we add an identifier of the form
% x$0 with the same type to the environment
foldl(add_primed_id,TIds,Env,Subenv),
btype(becomes_such,Pred,Subenv,pred,TPred,TR2,TRout).
btype2(evb2_becomes_such(Ids,Pred), _, Env, evb2_becomes_such(TIds,TPred), subst, [], TRin, TRout) :-
!,check_evb_becomes_such(evb2_becomes_such,Ids,Pred,Env,TIds,TPred,TRin,TRout).
btype2(operation_call(Op,Res,Args), Pos, Env, TOp, subst, Infos, TRin, TRout) :-
%print(opcall(Op)),nl, portray_env(Env),nl,
!,type_operation_call(Op,Res,Args,Pos,Env,TOp,Infos,TRin,TRout).
btype2(operation_call_in_expr(Op,Args), Pos, Env, operation_call_in_expr(TOp,TArgs), Type, Infos, TRin, TRout) :-
!, ext2int(btype2_opcall,Op,identifier(Opid),IPos,_,_,_,_),
btype2(identifier(op(Opid)),IPos,Env,Identifier,op(ArgTypes,ResTypes),OpInfos,TRin,TR1),
Identifier = identifier(_), % Identifier = identifier(op(Opid))
create_texpr(Identifier,subst,OpInfos,TOp),
(same_length(Args,ArgTypes)
-> btype_l(Args,Env,ArgTypes,TArgs,TR1,TR2)
; add_operation_call_error(ArgTypes,Args,Pos,Opid,'arguments(s)',_,TR1,TR2),
TArgs=[]
),
when(ground(ResTypes),
% sometimes, e.g., in ASSERTIONS, operations have not yet been type checked and ResType is a variable
(couplise_list(ResTypes,Type) -> true
; add_error(btype2,'Unexpected return type calling operation in expression:',Opid,Pos))),
get_operation_infos(OpInfos,Infos),
% print(op_call_in_expr(Opid,ResTypes,Infos,Type)),nl,
( memberchk(modifies(Modifies),Infos) ->
(Modifies==[] -> TR2=TRout
; var(Modifies) -> TR2=TRout,
% the info has not yet been computed; add a co-routine (which must however raise error immediately)
when(nonvar(Modifies),(Modifies==[] -> true
; add_error(btype2,'Read-only operation expected when calling operation in expressions ',Opid,Pos)))
; print(error(Infos)),nl, store_typecheck_error('Read-only operation expected when calling operation in expressions ',Pos,TR2,TRout) % used to be called query operation
)
; add_internal_error(btypechecker,'Missing modifies info field:',operation_call_in_expr(Op,Args),Pos),TR2=TRout
).
btype2(case(Expr,Eithers,Else), _, Env, case(TExpr,TEithers,TElse), subst, [], TRin, TRout) :-
!,btype(case,Expr,Env,Type,TExpr,TRin,TR1),
foldl(btype_caseor(Env,Type),Eithers,TEithers,LExprs,TR1,TR2),
append(LExprs,Exprs),
btype(case_else,Else,Env,subst,TElse,TR2,TR3),
% The next check could be made dependend on a preference (non-literal values allowed in
% CASE statements), in that case add TR3=TRout as an alternative
check_case_expressions(Exprs,TR3,TRout).
btype2(struct(Fields), Pos, Env, struct(TRecord), set(RType), [], TRin, TRout) :-
!, btype(struct,rec(Pos,Fields),Env,_,TRecord,TRin,TR1),
get_texpr_expr(TRecord,rec(TFields)),
foldl(extract_field_type,TFields,FieldTypes,TR1,TR2),
normalise_record_type(record(FieldTypes),RType),
TR2=TRout.
btype2(rec(Fields), Pos, Env, rec(TFields), RType, [], TRin, TRout) :-
!, foldl(btype_field_rec(Env),Fields,FTypes,TFields1,TRin,TR2),
normalise_record_type(record(FTypes),RType),
% we sort the field arguments here, so we do not have to normalise them every
% time in the interpreter
RType = record(NormedFieldTypes),
sort_record_fields(NormedFieldTypes,TFields1,TFields),
(record_has_multiple_field_names(NormedFieldTypes,FieldName)
-> ajoin(['Field ',FieldName,' used multiple times in record '],Msg),
store_typecheck_error(Msg,Pos,TR2,TRout)
; TR2=TRout
).
btype2(record_field(Record,I), Pos, Env, record_field(TRecord,Id), Type, [], TRin, TRout) :-
!,
btype(record_field,Record, Env, RType, TRecord, TRin, TR1),
remove_pos(I,identifier(Id)),
unify_types(record(Fields),RType,Pos,TRecord,TR1,TR2),
check_field_type(Fields,Id,Type,Pos,TR2,TRout).
btype2(refined_operation(Id,Results,Args,_RefinesID,Body), Pos, Env, TExpr, Type, Infos, TRin, TRout) :-
!, % TO DO: do we need to treat RefinesID ?
btype2(operation(Id,Results,Args,Body), Pos, Env, TExpr, Type, Infos, TRin, TRout).
btype2(operation(Id,Results,Args,Body), Pos, Env, operation(TId,TResults,TArgs,TBody), Type,
Infos, TRin, TRout) :-
%print(checking_op(Id)),nl,
!, %debug_stats(checking_operation(Id,Args)),
% type-check the identifier to look up the operation's type
% in the environment.
% we call ext2int and btype2/7 directly instead of going over
% btype/5, because we use op(Name) instead of Name to look up
% the type. This is done to seperate operation and variable name
% spaces (Note: that was a stupid and ugly hack)
ext2int(btype2_operation,Id,identifier(Opid),IPos,Type,Topid,IdInfos,TId),
btype2(identifier(op(Opid)),IPos,Env,Topid,Type,IdInfos,TRin,TR0),
% introduce a sub-environment Subenv by adding the argument and
% result variables
check_for_duplicate_raw_ids(Results,[],'results for operation ',Opid,FilteredResults,TR0,TR1),
add_ext_variables_with_info(FilteredResults,Env,[introduced_by(operation)],TResults,Subenv1,TR1,TR2),
check_for_duplicate_raw_ids(Args,[],'arguments for operation ',Opid,FilteredArgs,TR2,TR2b),
add_ext_variables_with_info(FilteredArgs,Subenv1,[readonly,introduced_by(operation)],TArgs,Subenv,TR2b,TR3),
% get their types and determine the resulting operation's type
get_texpr_types(TResults,LResultTypes),
get_texpr_types(TArgs,LArgTypes),
unify_types(op(LArgTypes,LResultTypes),Type,Pos,TId,TR3,TR4),
% type the operation's body in the sub-environment
btype(operation(Id),Body, Subenv, subst, TBody, TR4, TRout),
% the list of modified machine variables is the list of changed
% variables by the substitutions in the body minus the result variables
compute_accessed_vars_infos_for_operation(Id,TResults,TArgs,TBody,Modifies,Reads,NonDetModified,Infos),
%assertz(op_modifies_reads_cache(Opid,Modifies,Reads)), % cache information for operation_calls; possibly temporary solution until we understand the code for operation_call [Note: we can have multiple versions ! at different refinement levels !!]
% make sure that the List of modified variables of this operation
% is also up-to-date in the type environment
(memberchk(modifies(EnvModifies),IdInfos),
memberchk(reads(EnvReads),IdInfos),
memberchk(non_det_modifies(EnvNonDetModifies),IdInfos) ->
% Check if the environment variables and the local variables are unifiable.
% If not, an operation with the same name must have been defined before
% We can ignore this, later an error message will be raised.
( EnvModifies=Modifies -> true; add_message(btypechecker,'Conflict in modifies info for ',Id,IPos)),
( EnvReads=Reads -> true; add_message(btypechecker,'Conflict in reads info for ',Id,IPos)),
( EnvNonDetModifies=NonDetModified -> true; add_message(btypechecker,'Conflict in non_det_modifies info for ',Id,IPos))
; add_error(btypechecker,'Cannot store modifies/reads info for: ',Opid,IPos)
),
debug_format(9,'Finished checking operation ~w, reads:~w, writes=~w~n',[Id,Reads,Modifies]).
btype2(while(Pred,Body,Inv,Var), _, Env, while(TPred,TBody,TInv,TVar), subst, FullInfo, TRin, TRout) :- !,
btype(while,Pred,Env,pred,TPred,TRin,TR1),
btype(while_body,Body,Env,subst,TBody,TR1,TR2),
% In contrast to the other substitutions, in the invariant and variant
% part of a while loop it is possible to reference abstract variables,
% as they are not used to influence the behaviour of the substitution.
% We create a new environment InvEnv where those access restrictions are
% removed.
allow_access_to_abstract_vars(Env,InvEnv),
add_primed_old_value_variables(InvEnv,PInvEnv),
btype(while_inv,Inv,PInvEnv,pred,TInv,TR2,TR3),
btype(while_variant,Var,InvEnv,integer,TVar,TR3,TRout),
% tag this statement with an appropiate info if a reference to the original value
% of a variable is made in the invariant.
% This info is used in the clean_up (see b_ast_cleanup) to insert a LET statement.
check_for_old_state_references(TInv,Info),
FullInfo = [modifies(Modifies),reads(AllReads)|Info],
% TO DO: ideally we should compute those in one go for all substitutions:
% here we compute information again which we have already computed for operations
get_accessed_vars(b(while(TPred,TBody,TInv,TVar),subst,Info),[],Modifies,_NonDetModifies,Reads),
(debug:debug_mode(off) -> true
; format('WHILE Reads : ~w~n Modifies : ~w~n',[Reads,Modifies]),
print('VARIANT: '),translate:print_bexpr(TVar),nl
),
(member(refers_to_old_state(SortedRefs),Info)
-> findall(Primed,member(oref(Primed,_,_),SortedRefs),PrimedDollarVars), sort(PrimedDollarVars,SPDV),
ord_union(SPDV,Reads,AllReads) %, print(add(SPDV,Reads)),nl
; AllReads = Reads).
btype2(parallel(Substs),Pos,Env,parallel(TSubsts), subst, [], TRin, TRout) :-
!, btype_l(Substs,Env,_,TSubsts,TRin,TR1),
check_no_double_assignment(TSubsts,Pos,TR1,TRout).
btype2(minus_or_set_subtract(A,B), Pos, Env, minus_or_set_subtract(TA,TB), Type, [], TRin, TRout) :-
!,btype_l([A,B],Env,[TypeA,TypeB],[TA,TB],TRin,TR1),
delayed_type_minus(TypeA,TypeB,Type,Pos,A,B,TR1,TRout).
btype2(add(A,B), Pos, Env, add(TA,TB), Type, [], TRin, TRout) :-
allow_to_use_real_types,
!,TypeA=TypeB, TypeA=Type,
btype_l([A,B],Env,[TypeA,TypeB],[TA,TB],TRin,TR1),
delayed_type_arith('+',Type,Pos,TR1,TRout).
btype2(div(A,B), Pos, Env, div(TA,TB), Type, [], TRin, TRout) :-
allow_to_use_real_types,
!,TypeA=TypeB, TypeA=Type,
btype_l([A,B],Env,[TypeA,TypeB],[TA,TB],TRin,TR1),
delayed_type_arith('/',Type,Pos,TR1,TRout).
btype2(unary_minus(A), Pos, Env, unary_minus(TA), Type, [], TRin, TRout) :-
allow_to_use_real_types,
!,btype_l([A],Env,[TypeA],[TA],TRin,TR1),
delayed_type_arith_unary('-',TypeA,Type,Pos,A,TR1,TRout).
btype2(power_of(A,B), Pos, Env, power_of(TA,TB), Type, [], TRin, TRout) :-
allow_to_use_real_types,
!,btype_l([A,B],Env,[TypeA,integer],[TA,TB],TRin,TR1), % second arg must be integer
delayed_type_arith_unary('**',TypeA,Type,Pos,A,TR1,TRout).
btype2(general_sum(A,B,C), Pos, Env, Res, Type, [], TRin, TRout) :- !, % SIGMA
(allow_to_use_real_types -> true ; Type=integer),
btype3(general_sum(A,B,C), Pos, Env, Res, Type, [], TRin, TR1),
delayed_type_arith(general_sum,Type,Pos,TR1,TRout).
btype2(general_product(A,B,C), Pos, Env, Res, Type, [], TRin, TRout) :- !, % PI
(allow_to_use_real_types -> true ; Type=integer),
btype3(general_product(A,B,C), Pos, Env, Res, Type, [], TRin, TR1),
delayed_type_arith(general_product,Type,Pos,TR1,TRout).
btype2(less_equal(A,B), Pos, Env, less_equal(TA,TB), pred, [], TRin, TRout) :-
allow_to_use_real_types,
!, TypeA=TypeB, btype_l([A,B],Env,[TypeA,TypeB],[TA,TB],TRin,TR1),
delayed_type_arith_comparison('<=',TypeA,Pos,TR1,TRout).
btype2(greater_equal(A,B), Pos, Env, greater_equal(TA,TB), pred, [], TRin, TRout) :-
allow_to_use_real_types,
!, TypeA=TypeB, btype_l([A,B],Env,[TypeA,TypeB],[TA,TB],TRin,TR1),
delayed_type_arith_comparison('>=',TypeA,Pos,TR1,TRout).
btype2(less(A,B), Pos, Env, less(TA,TB), pred, [], TRin, TRout) :-
allow_to_use_real_types,
!, TypeA=TypeB, btype_l([A,B],Env,[TypeA,TypeB],[TA,TB],TRin,TR1),
delayed_type_arith_comparison('<',TypeA,Pos,TR1,TRout).
btype2(greater(A,B), Pos, Env, greater(TA,TB), pred, [], TRin, TRout) :-
allow_to_use_real_types,
!, TypeA=TypeB, btype_l([A,B],Env,[TypeA,TypeB],[TA,TB],TRin,TR1),
delayed_type_arith_comparison('>',TypeA,Pos,TR1,TRout).
btype2(concat(A,B), Pos, Env, concat(TA,TB), Type, [], TRin, TRout) :-
get_preference(allow_sequence_operators_on_strings,true), % a^b --> STRING_APPEND(a,b)
btype_l([A,B],Env,[TypeA,TypeB],[TA,TB],TRin,TR1),
TypeA \== integer, % otherwise trigger error_rewrite below for exponentiation
!,
delayed_type_string_or_seq(TypeA,TypeB,Type,Pos,A,B,TR1,TRout).
btype2(rev(A), Pos, Env, rev(TA), Type, [], TRin, TRout) :-
get_preference(allow_sequence_operators_on_strings,true), % rev(Str) --> STRING_REV(Str)
Type = TypeA,
btype_l([A],Env,[TypeA],[TA],TRin,TR1),
!,
delayed_type_string_or_seq(TypeA,TypeA,TypeA,Pos,A,A,TR1,TRout).
btype2(size(A), Pos, Env, size(TA), Type, [], TRin, TRout) :-
get_preference(allow_sequence_operators_on_strings,true), % size(Str) --> STRING_LENGTH(Str)
Type = integer,
btype_l([A],Env,[TypeA],[TA],TRin,TR1),
!,
delayed_type_string_or_seq(TypeA,TypeA,TypeA,Pos,A,A,TR1,TRout).
btype2(general_concat(A), Pos, Env, general_concat(TA), Type, [], TRin, TRout) :-
get_preference(allow_sequence_operators_on_strings,true), % conc(Strs) --> STRING_CONC(Str)
btype_l([A],Env,[TypeA],[TA],TRin,TR1),
!,
delayed_type_seq_string_or_seq_seq(TypeA,Type,Pos,A,TR1,TRout).
btype2(mult_or_cart(A,B), Pos, Env, mult_or_cart(TA,TB), Type, [], TRin, TRout) :-
!,btype_l([A,B],Env,[TypeA,TypeB],[TA,TB],TRin,TR1),
delayed_type_times(TypeA,TypeB,Type,Pos,A,B,TR1,TRout).
btype2(substitution(Subst,Pred), _Pos, Env, TSubst, pred, [], TRin, TRout) :-
!, type_substitution_expression(Subst,Pred,Env,TSubst,TRin,TRout).
btype2(extended_expr(Id,Args,Args2), Pos, Env, Result, Type, [was_operator(Id)|Info], TRin, TRout) :-
!, lookup_eventb_operator(Id,Args,Args2,Pos,Env,expr,Result,Type,Info,TRin,TRout).
btype2(extended_pred(Id,Args,Args2), Pos, Env, Result, Type, [was_operator(Id)|Info], TRin, TRout) :-
!, lookup_eventb_operator(Id,Args,Args2,Pos,Env,pred,Result,Type,Info,TRin,TRout).
btype2(recursive_let(Id,Set),_Pos,Env,recursive(TId,TSet),set(Type),[],TRin,TRout) :- !,
add_ext_variables([Id], Env, [TId], SubEnv, TRin, TR1),
get_texpr_type(TId,set(Type)),
btype(recursive,Set,SubEnv,set(Type),TSet,TR1,TRout).
btype2(set_extension(RawList),Pos,_Env,value(Val),set(Type),[],TR,TR) :-
% optimisation: -> skip type checking the content and just generate an AVL set directly
% can have a large performance impact for data validation projects
simple_set_extension_type(RawList,Type),
(read_raw_simple_values(set(Type),set_extension(Pos,RawList),Val)
-> true %,add_message(btypechecker,'Converted set_extension:',Type,Pos)
; %add_message(btypechecker,'Failed to convert set_extension:',Type,Pos),
fail), !.
btype2(sequence_extension(RawList),Pos,_Env,value(Val),seq(Type),[],TR,TR) :-
% ditto for sequence extensions
simple_set_extension_type(RawList,Type),
(read_raw_simple_values(set(couple(integer,Type)),sequence_extension(Pos,RawList),Val)
-> true %,add_message(btypechecker,'Converted sequence_extension:',Type,Pos)
; %add_message(btypechecker,'Failed to convert sequence_extension:',Type,Pos),
fail), !.
btype2(typeset,_Pos,_Env,typeset,set(_),[],TR,TR) :- !.
btype2(typeof(InnerExpr,TypeExpr),_Pos,Env,Expr,Type,Info,TRin,TRout) :-
!, btype(typeof,TypeExpr,Env,set(Type),_TTypeExpr,TRin,TR1),
btype(typeof,InnerExpr,Env,Type,TExpr,TR1,TRout),
get_texpr_expr(TExpr,Expr),get_texpr_info(TExpr,Info).
btype2(label(Label,Node), _Pos, Env, TExpr, Type, InfosOut, TRin, TRout) :- !,
btype(label, Node, Env, Type, Result, TRin, TRout),
get_texpr_expr(Result,TExpr),
get_texpr_info(Result,Infos),
add_label_to_infos(Infos,Label,InfosOut).
btype2(description(Desc,Node), _Pos, Env, TExpr, Type, [description(Desc)|Infos], TRin, TRout) :- !,
btype(description, Node, Env, Type, Result, TRin, TRout),
get_texpr_expr(Result,TExpr),
get_texpr_info(Result,Infos).
btype2(symbolic_comprehension_set(A,B), Pos, Env, TExpr, Type, [prob_annotation('SYMBOLIC')|Infos], TRin, TRout) :- !,
btype2(comprehension_set(A,B), Pos, Env, TExpr, Type, Infos, TRin, TRout).
btype2(symbolic_quantified_union(A,B,C), Pos, Env, TExpr, Type, [prob_annotation('SYMBOLIC')|Infos], TRin, TRout) :- !,
btype2(quantified_union(A,B,C), Pos, Env, TExpr, Type, Infos, TRin, TRout).
btype2(symbolic_lambda(A,B,C), Pos, Env, TExpr, Type, [prob_annotation('SYMBOLIC')|Infos], TRin, TRout) :- !,
btype2(lambda(A,B,C), Pos, Env, TExpr, Type, Infos, TRin, TRout).
btype2(symbolic_composition(A,B), Pos, Env, TExpr, Type, [prob_annotation('SYMBOLIC')|Infos], TRin, TRout) :- !,
btype2(composition(A,B), Pos, Env, TExpr, Type, Infos, TRin, TRout).
btype2(conversion(Node), _Pos, Env, TExpr, Type, [conversion|Infos], TRin, TRout) :- !,
btype(conversion, Node, Env, Type, Result, TRin, TRout),
get_texpr_expr(Result,TExpr),
get_texpr_info(Result,Infos).
btype2(let_predicate(Ids,Equalities,Pred), Pos, Env, let_predicate(TIdsOut,TExprsOut,TPred), pred, [], TRin, TRout) :- !,
check_for_duplicate_raw_ids(Ids,[],'LET arguments','',FIds,TRin,TR0),
add_ext_variables_with_info(FIds,Env,[introduced_by(let_predicate)],TIds,Subenv,TR0,TR1),
btype(let_predicate, Equalities, Subenv, pred, TEqualities, TR1, TR2), % should we introduced variables only one by one ?
btype(let_predicate, Pred, Subenv, pred, TPred, TR2, TR3),
btype_static_check_let(TIds,TEqualities,Pos,allow_reuse,Env,TR3,TR4),
split_let_equalities_into_ids_and_expressions(Ids,TEqualities,TIdsOut,TExprsOut,Pos,TR4,TRout).
btype2(let_expression(Ids,Equalities,Expr), Pos, Env, let_expression(TIdsOut,TExprsOut,TExpr), Type, [], TRin, TRout) :- !,
check_for_duplicate_raw_ids(Ids,[],'LET arguments','',FIds,TRin,TR0),
add_ext_variables_with_info(FIds,Env,[introduced_by(let_expression)],TIds,Subenv,TR0,TR1),
btype(let_expression, Equalities, Subenv, pred, TEqualities, TR1, TR2),
btype(let_expression, Expr, Subenv, Type, TExpr, TR2, TR3),
btype_static_check_let(TIds,TEqualities,Pos,allow_reuse,Env,TR3,TR4),
split_let_equalities_into_ids_and_expressions(Ids,TEqualities,TIdsOut,TExprsOut,Pos,TR4,TRout).
btype2(value(Val),_Pos,_Env,value(Val),Type,[],TR,TR) :- % support value/1 terms in raw ast
infer_value_type(Val,Type),
!.
btype2(Expr, Pos, Env, TExpr, Type, V, TRin, TRout) :-
btype3(Expr, Pos, Env, TExpr, Type, V, TRin, TRout).