:- module varset. :- use_module assoc_list, bool, builtin, int, list, map, private_builtin, require, set, std_util, string, term. :- type (varset:varset(T)) ---> varset((term:var_supply(T)), (tree234:tree234((term:var(T)), string)), (tree234:tree234((term:var(T)), (term:term(T))))) . :- pred varset:new_vars_2((varset:varset(T_1)), int, (list:list((term:var(T_1)))), (list:list((term:var(T_1)))), (varset:varset(T_1))). :- mode varset:new_vars_2((builtin:in), (builtin:in), (builtin:in), (builtin:out), (builtin:out)) is det. :- pred varset:vars_2((term:var_supply(T_1)), (term:var_supply(T_1)), (list:list((term:var(T_1)))), (list:list((term:var(T_1))))). :- mode varset:vars_2((builtin:in), (builtin:in), (builtin:in), (builtin:out)) is det. :- pred varset:bind_vars_2((list:list((std_util:pair((term:var(T_1)), (term:term(T_1)))))), (varset:varset(T_1)), (varset:varset(T_1))). :- mode varset:bind_vars_2((builtin:in), (builtin:in), (builtin:out)) is det. :- pred varset:merge_subst((bool:bool), (varset:varset(T_1)), (varset:varset(T_1)), (varset:varset(T_1)), (tree234:tree234((term:var(T_1)), (term:term(T_1))))). :- mode varset:merge_subst((builtin:in), (builtin:in), (builtin:in), (builtin:out), (builtin:out)) is det. :- pred varset:merge_subst_2((bool:bool), (term:var_supply(T_1)), (term:var_supply(T_1)), (tree234:tree234((term:var(T_1)), string)), (tree234:tree234((term:var(T_1)), (term:term(T_1)))), (varset:varset(T_1)), (tree234:tree234((term:var(T_1)), (term:term(T_1)))), (varset:varset(T_1)), (tree234:tree234((term:var(T_1)), (term:term(T_1))))). :- mode varset:merge_subst_2((builtin:in), (builtin:in), (builtin:in), (builtin:in), (builtin:in), (builtin:in), (builtin:in), (builtin:out), (builtin:out)) is det. :- pred varset:ensure_unique_names_2((list:list((term:var(T_1)))), string, (set:set(string)), (tree234:tree234((term:var(T_1)), string)), (tree234:tree234((term:var(T_1)), string)), (tree234:tree234((term:var(T_1)), string))). :- mode varset:ensure_unique_names_2((builtin:in), (builtin:in), (builtin:in), (builtin:in), (builtin:in), (builtin:out)) is det. varset:init((varset:varset(VarSupply_2, Names_3, Vals_4))) :- term:init_var_supply(VarSupply_2), map:init(Names_3), map:init(Vals_4). varset:init = VS_2 :- varset:init(VS_2). varset:is_empty((varset:varset(VarSupply_2, V_3, V_4))) :- term:init_var_supply(VarSupply_2). varset:new_var((varset:varset(MaxId0_4, Names_5, Vals_6)), Var_7, (varset:varset(MaxId_8, Names_5, Vals_6))) :- term:create_var(MaxId0_4, Var_7, MaxId_8). varset:new_named_var((varset:varset(MaxId0_5, Names0_6, Vals_7)), Name_8, Var_9, (varset:varset(MaxId_10, Names_11, Vals_7))) :- term:create_var(MaxId0_5, Var_9, MaxId_10), map:set(Names0_6, Var_9, Name_8, Names_11). varset:new_vars(Varset0_5, NumVars_6, NewVars_7, Varset_8) :- V_9 = list:[], varset:new_vars_2(Varset0_5, NumVars_6, V_9, NewVars_7, Varset_8). varset:delete_var((varset:varset(MaxId_4, Names0_5, Vals0_6)), Var_7, (varset:varset(MaxId_4, Names_8, Vals_9))) :- map:delete(Names0_5, Var_7, Names_8), map:delete(Vals0_6, Var_7, Vals_9). varset:delete_var(VS1_4, V_5) = VS2_6 :- varset:delete_var(VS1_4, V_5, VS2_6). varset:delete_vars(VS1_4, Vs_5) = VS2_6 :- varset:delete_vars(VS1_4, Vs_5, VS2_6). varset:vars((varset:varset(MaxId0_3, V_4, V_5)), L_6) :- term:init_var_supply(V0_7), V_9 = list:[], varset:vars_2(V0_7, MaxId0_3, V_9, L1_8), list:reverse(L1_8, L_6). varset:vars(VS_3) = Vs_4 :- varset:vars(VS_3, Vs_4). varset:name_var(VarSet0_5, Id_6, Name_7, VarSet_8) :- VarSet0_5 = varset:varset(MaxId_9, Names0_10, Vals_11), map:set(Names0_10, Id_6, Name_7, Names_12), VarSet_8 = varset:varset(MaxId_9, Names_12, Vals_11). varset:name_var(VS1_5, V_6, S_7) = VS2_8 :- varset:name_var(VS1_5, V_6, S_7, VS2_8). varset:lookup_name(VS_4, V_5) = S_6 :- varset:lookup_name(VS_4, V_5, S_6). varset:lookup_name(VS1_5, V_6, S_7) = S2_8 :- varset:lookup_name(VS1_5, V_6, S_7, S2_8). varset:search_name((varset:varset(V_4, Names_5, V_6)), Id_7, Name_8) :- map:search(Names_5, Id_7, Name0_9), Name_8 = Name0_9. varset:bind_var((varset:varset(MaxId_5, Names_6, Vals0_7)), Id_8, Val_9, (varset:varset(MaxId_5, Names_6, Vals_10))) :- map:set(Vals0_7, Id_8, Val_9, Vals_10). varset:bind_var(VS1_5, V_6, T_7) = VS2_8 :- varset:bind_var(VS1_5, V_6, T_7, VS2_8). varset:bind_vars(Varset0_4, Subst_5, Varset_6) :- map:to_assoc_list(Subst_5, VarTermList_7), varset:bind_vars_2(VarTermList_7, Varset0_4, Varset_6). varset:bind_vars(VS1_4, S_5) = VS2_6 :- varset:bind_vars(VS1_4, S_5, VS2_6). varset:search_var((varset:varset(V_4, V_5, Vals_6)), Id_7, Val_8) :- map:search(Vals_6, Id_7, Val_8). varset:lookup_vars((varset:varset(V_3, V_4, Subst_5)), Subst_5). varset:lookup_vars(VS_3) = S_4 :- varset:lookup_vars(VS_3, S_4). varset:merge(VarSet0_6, VarSet1_7, TermList0_8, VarSet_9, TermList_10) :- IncludeNames_11 = bool:yes, varset:merge_subst(IncludeNames_11, VarSet0_6, VarSet1_7, VarSet_9, Subst_12), term:apply_substitution_to_list(TermList0_8, Subst_12, TermList_10). varset:merge_subst(VarSet0_5, (varset:varset(MaxId_6, Names_7, Vals_8)), VarSet_9, Subst_10) :- IncludeNames_11 = bool:yes, V_12 = varset:varset(MaxId_6, Names_7, Vals_8), varset:merge_subst(IncludeNames_11, VarSet0_5, V_12, VarSet_9, Subst_10). varset:merge_without_names(VarSet0_6, VarSet1_7, TermList0_8, VarSet_9, TermList_10) :- IncludeNames_11 = bool:no, varset:merge_subst(IncludeNames_11, VarSet0_6, VarSet1_7, VarSet_9, Subst_12), term:apply_substitution_to_list(TermList0_8, Subst_12, TermList_10). varset:merge_subst_without_names(VarSet0_5, (varset:varset(MaxId_6, Names_7, Vals_8)), VarSet_9, Subst_10) :- IncludeNames_11 = bool:no, V_12 = varset:varset(MaxId_6, Names_7, Vals_8), varset:merge_subst(IncludeNames_11, VarSet0_5, V_12, VarSet_9, Subst_10). varset:get_bindings((varset:varset(V_3, V_4, Subst_5)), Subst_5). varset:get_bindings(VS_3) = S_4 :- varset:get_bindings(VS_3, S_4). varset:set_bindings((varset:varset(C_4, N_5, V_6)), S_7, (varset:varset(C_4, N_5, S_7))). varset:set_bindings(VS1_4, S_5) = VS2_6 :- varset:set_bindings(VS1_4, S_5, VS2_6). varset:create_name_var_map((varset:varset(V_3, VarNameIndex_4, V_5)), NameVarIndex_6) :- map:keys(VarNameIndex_4, Vars_7), map:values(VarNameIndex_4, Names_8), map:from_corresponding_lists(Names_8, Vars_7, NameVarIndex_6). varset:create_name_var_map(VS_3) = M_4 :- varset:create_name_var_map(VS_3, M_4). varset:var_name_list((varset:varset(V_3, VarNameIndex_4, V_5)), VarNameList_6) :- map:to_assoc_list(VarNameIndex_4, VarNameList_6). varset:var_name_list(VS_3) = AL_4 :- varset:var_name_list(VS_3, AL_4). varset:ensure_unique_names(AllVars_5, Suffix_6, (varset:varset(Supply_7, VarNameMap0_8, Values_9)), (varset:varset(Supply_7, VarNameMap_10, Values_9))) :- set:init(UsedNames_11), map:init(VarNameMap1_12), varset:ensure_unique_names_2(AllVars_5, Suffix_6, UsedNames_11, VarNameMap0_8, VarNameMap1_12, VarNameMap_10). varset:ensure_unique_names(Vs_5, S1_6, VS1_7) = VS2_8 :- varset:ensure_unique_names(Vs_5, S1_6, VS1_7, VS2_8). varset:select((varset:varset(Supply_4, VarNameMap0_5, Values0_6)), Vars_7, (varset:varset(Supply_4, VarNameMap_8, Values_9))) :- map:select(VarNameMap0_5, Vars_7, VarNameMap_8), map:select(Values0_6, Vars_7, Values_9). varset:select(VS1_4, S_5) = VS2_6 :- varset:select(VS1_4, S_5, VS2_6). varset:coerce(A_3, B_4) :- private_builtin:unsafe_type_cast(A_3, B_4). varset:coerce(VS1_3) = VS2_4 :- varset:coerce(VS1_3, VS2_4). varset:merge_subst(IncludeNames_6, VarSet0_7, (varset:varset(MaxId_8, Names_9, Vals_10)), VarSet_11, Subst_12) :- term:init_var_supply(N_13), map:init(Subst0_14), varset:merge_subst_2(IncludeNames_6, N_13, MaxId_8, Names_9, Vals_10, VarSet0_7, Subst0_14, VarSet_11, Subst_12). :- pragma termination_info(varset:init((builtin:out)), infinite, can_loop). :- pragma termination_info((varset:init) = (builtin:out), infinite, can_loop). :- pragma termination_info(varset:is_empty((builtin:in)), finite(0, [no, no]), can_loop). :- pragma termination_info(varset:new_var((builtin:in), (builtin:out), (builtin:out)), infinite, can_loop). :- pragma termination_info(varset:new_named_var((builtin:in), (builtin:in), (builtin:out), (builtin:out)), infinite, can_loop). :- pragma termination_info(varset:new_uniquely_named_var((builtin:in), (builtin:in), (builtin:out), (builtin:out)), infinite, can_loop). :- pragma termination_info(varset:new_maybe_named_var((builtin:in), (builtin:in), (builtin:out), (builtin:out)), infinite, can_loop). :- pragma termination_info(varset:new_vars((builtin:in), (builtin:in), (builtin:out), (builtin:out)), infinite, can_loop). :- pragma termination_info(varset:delete_var((builtin:in), (builtin:in), (builtin:out)), infinite, can_loop). :- pragma termination_info(varset:delete_var((builtin:in), (builtin:in)) = (builtin:out), infinite, can_loop). :- pragma termination_info(varset:delete_vars((builtin:in), (builtin:in), (builtin:out)), infinite, can_loop). :- pragma termination_info(varset:delete_vars((builtin:in), (builtin:in)) = (builtin:out), infinite, can_loop). :- pragma termination_info(varset:vars((builtin:in), (builtin:out)), infinite, can_loop). :- pragma termination_info(varset:vars((builtin:in)) = (builtin:out), infinite, can_loop). :- pragma termination_info(varset:name_var((builtin:in), (builtin:in), (builtin:in), (builtin:out)), infinite, can_loop). :- pragma termination_info(varset:name_var((builtin:in), (builtin:in), (builtin:in)) = (builtin:out), infinite, can_loop). :- pragma termination_info(varset:lookup_name((builtin:in), (builtin:in), (builtin:out)), infinite, can_loop). :- pragma termination_info(varset:lookup_name((builtin:in), (builtin:in)) = (builtin:out), infinite, can_loop). :- pragma termination_info(varset:lookup_name((builtin:in), (builtin:in), (builtin:in), (builtin:out)), infinite, can_loop). :- pragma termination_info(varset:lookup_name((builtin:in), (builtin:in), (builtin:in)) = (builtin:out), infinite, can_loop). :- pragma termination_info(varset:search_name((builtin:in), (builtin:in), (builtin:out)), infinite, can_loop). :- pragma termination_info(varset:bind_var((builtin:in), (builtin:in), (builtin:in), (builtin:out)), infinite, can_loop). :- pragma termination_info(varset:bind_var((builtin:in), (builtin:in), (builtin:in)) = (builtin:out), infinite, can_loop). :- pragma termination_info(varset:bind_vars((builtin:in), (builtin:in), (builtin:out)), infinite, can_loop). :- pragma termination_info(varset:bind_vars((builtin:in), (builtin:in)) = (builtin:out), infinite, can_loop). :- pragma termination_info(varset:search_var((builtin:in), (builtin:in), (builtin:out)), infinite, can_loop). :- pragma termination_info(varset:lookup_vars((builtin:in), (builtin:out)), finite(-3, [no, yes, no]), cannot_loop). :- pragma termination_info(varset:lookup_vars((builtin:in)) = (builtin:out), finite(-3, [no, yes, no]), cannot_loop). :- pragma termination_info(varset:merge((builtin:in), (builtin:in), (builtin:in), (builtin:out), (builtin:out)), infinite, can_loop). :- pragma termination_info(varset:merge_subst((builtin:in), (builtin:in), (builtin:out), (builtin:out)), infinite, can_loop). :- pragma termination_info(varset:merge_without_names((builtin:in), (builtin:in), (builtin:in), (builtin:out), (builtin:out)), infinite, can_loop). :- pragma termination_info(varset:merge_subst_without_names((builtin:in), (builtin:in), (builtin:out), (builtin:out)), infinite, can_loop). :- pragma termination_info(varset:get_bindings((builtin:in), (builtin:out)), finite(-3, [no, yes, no]), cannot_loop). :- pragma termination_info(varset:get_bindings((builtin:in)) = (builtin:out), finite(-3, [no, yes, no]), cannot_loop). :- pragma termination_info(varset:set_bindings((builtin:in), (builtin:in), (builtin:out)), finite(0, [no, yes, yes, no]), cannot_loop). :- pragma termination_info(varset:set_bindings((builtin:in), (builtin:in)) = (builtin:out), finite(0, [no, yes, yes, no]), cannot_loop). :- pragma termination_info(varset:create_name_var_map((builtin:in), (builtin:out)), infinite, can_loop). :- pragma termination_info(varset:create_name_var_map((builtin:in)) = (builtin:out), infinite, can_loop). :- pragma termination_info(varset:var_name_list((builtin:in), (builtin:out)), infinite, can_loop). :- pragma termination_info(varset:var_name_list((builtin:in)) = (builtin:out), infinite, can_loop). :- pragma termination_info(varset:ensure_unique_names((builtin:in), (builtin:in), (builtin:in), (builtin:out)), infinite, can_loop). :- pragma termination_info(varset:ensure_unique_names((builtin:in), (builtin:in), (builtin:in)) = (builtin:out), infinite, can_loop). :- pragma termination_info(varset:select((builtin:in), (builtin:in), (builtin:out)), infinite, can_loop). :- pragma termination_info(varset:select((builtin:in), (builtin:in)) = (builtin:out), infinite, can_loop). :- pragma termination_info(varset:squash((builtin:in), (builtin:in), (builtin:out), (builtin:out)), infinite, can_loop). :- pragma termination_info(varset:coerce((builtin:in), (builtin:out)), infinite, cannot_loop). :- pragma termination_info(varset:coerce((builtin:in)) = (builtin:out), infinite, cannot_loop).