220 Lines

create_refmap(TypeMap,IdMap,ktypenv(Env,StartEnv)) :-
    empty_avl(StartEnv),
    create_refmap_types(TypeMap,StartEnv,TypeEnv),
    create_refmap_ids(IdMap,TypeEnv,Env).

Calls:

Name: create_refmap_ids/3	Module: kodkod_typing
Name: create_refmap_types/3	Module: kodkod_typing
Name: empty_avl/1	Module: foo_error

Called:

Name: kodkod_insert_casts/4

Module: kodkod_typing

create_refmap_ids/3

create_refmap_ids(IdMap,In,Out) :-
avl_range(IdMap,Relations),
foldl(add_to_refmap,Relations,In,Out).

Calls:

Name: foldl/4	Module: tools
Name: avl_range/2	Module: foo_error

Called:

Name: create_refmap/3

Module: kodkod_typing

create_refmap_types/3

create_refmap_types(TypeMap,In,Out) :-
    avl_range(TypeMap,Relations1),
    maplist(remove_relation_wrapper,Relations1,Relations),
    foldl(add_to_refmap,Relations,In,Out).

Calls:

Name: foldl/4	Module: tools
Name: maplist/3	Module: foo_error
Name: avl_range/2	Module: foo_error

Called:

Name: create_refmap/3

Module: kodkod_typing

get_rel_types/3

get_rel_types(reldef(Id,Types,_,_,_),Id,Types).

get_rel_types(intsetrel(Id,_,_),Id,[R]) :-
intset_relation_kodkod_name(R).

get_rel_types(pow2rel(Id,_,_),Id,[R]) :-
pow2integer_relation_kodkod_name(R).

Calls:

Name: pow2integer_relation_kodkod_name/1	Module: foo_error
Name: intset_relation_kodkod_name/1	Module: foo_error

Called:

Name: add_to_refmap/3

Module: kodkod_typing

kodkod_insert_casts/4

kodkod_insert_casts(Kin,TypeMap,IdMap,Kout) :-
create_refmap(TypeMap,IdMap,Env),
type_kodkod(Kin,Env,formula,Kout).

Calls:

Name: type_kodkod/4	Module: kodkod_typing
Name: create_refmap/3	Module: kodkod_typing

ktype/2

ktype(true,formula).

ktype(false,formula).

ktype(not(formula),formula).

ktype(and(formula,formula),formula).

ktype(or(formula,formula),formula).

ktype(implies(formula,formula),formula).

ktype(iff(formula,formula),formula).

ktype(one(rel(_)), formula).

ktype(some(rel(_)), formula).

ktype(no(rel(_)), formula).

ktype(lone(rel(_)), formula).

ktype(set(rel(_)), formula).

ktype(in(rel(T),rel(T)), formula).

ktype(equals(T,T),formula).

ktype(pfunc(rel(_),rel(_),rel(_)), formula).

ktype(func(rel(_),rel(_),rel(_)), formula).

ktype(empty,rel(_)).

ktype(iden,rel(_)).

ktype(univ,rel(_)).

ktype(intersection(rel(A),rel(A)), rel(A)).

ktype(union(rel(A),rel(A)), rel(A)).

ktype(difference(rel(A),rel(A)), rel(A)).

ktype(overwrite(rel(A),rel(A)), rel(A)).

ktype(closure(rel(A)), rel(A)).

ktype(reflexive_closure(rel(A)), rel(A)).

ktype(product(rel(A),rel(B)), rel(C)) :- safe_append(A,B,C).

ktype(transpose(rel(R)), rel(T)) :- safe_reverse(R,T).

ktype(join(rel(A),rel([Bhead|Btail])), rel(C)) :-
safe_append(Astart,[Bhead],A),
safe_append(Astart,Btail,C).

ktype(if(formula,rel(R),rel(R)), rel(R)).

ktype(gt(int_expression,int_expression), formula).

ktype(gte(int_expression,int_expression), formula).

ktype(lt(int_expression,int_expression), formula).

ktype(lte(int_expression,int_expression), formula).

ktype(card(rel(_)), int_expression).

ktype(add(int_expression,int_expression), int_expression).

ktype(sub(int_expression,int_expression), int_expression).

ktype(mul(int_expression,int_expression), int_expression).

ktype(div(int_expression,int_expression), int_expression).

ktype(floored_div(int_expression,int_expression), int_expression).

ktype(mod(int_expression,int_expression), int_expression).

ktype(sum(rel([_])), int_expression).

Calls:

Name: safe_append/3	Module: kodkod_typing
Name: safe_reverse/2	Module: kodkod_typing

Called:

Name: type_kodkod2/4

Module: kodkod_typing

lookup_reltypes/3

lookup_reltypes(Id,ktypenv(Env,_Vars),Types) :-
avl_fetch(Id,Env,Types).

Calls:

Name: avl_fetch/3

Module: foo_error

Called:

Name: type_kodkod2/4

Module: kodkod_typing

lookup_vartypes/3

lookup_vartypes(Id,ktypenv(_Env,Vars),Types) :-
avl_fetch(Id,Vars,Types).

Calls:

Name: avl_fetch/3

Module: foo_error

Called:

Name: type_kodkod2/4

Module: kodkod_typing

nth0s/3

nth0s(Positions,List,Elements) :- maplist(nth0s2(List),Positions,Elements).

Calls:

Name: maplist/3

Module: foo_error

Called:

Name: type_kodkod2/4

Module: kodkod_typing

nth0s2/3

nth0s2(List,Position,Element) :- nth0(Position,List,Element).

Calls:

Name: nth0/3

Module: foo_error

remove_relation_wrapper/2

remove_relation_wrapper(relation(_,_,Rel),Rel).

safe_append/3

safe_append(A,B,C) :-
    complete_list(A,AComplete),
    complete_list(B,BComplete),
    complete_list(C,CComplete),
    safe_append2(A,B,C,AComplete,BComplete,CComplete).

Calls:

Name: safe_append2/6	Module: kodkod_typing
Name: complete_list/2	Module: kodkod_typing

Called:

Name: type_kodkod_declarations/6	Module: kodkod_typing
Name: ktype/2	Module: kodkod_typing

safe_append2/6

Block: safe_append2(?,?,?,-,-,?) safe_append2(?,?,?,-,?,-)

safe_append2(A,B,C,1,1,1) :- append(A,B,C),!.

Calls:

Name: !
Name: append/3

Called:

Name: safe_append/3

Module: kodkod_typing

safe_reverse/2

safe_reverse(A,B) :-
safe_reverse2(A,[],B),
safe_reverse2(B,[],A).

Calls:

Name: safe_reverse2/3

Module: kodkod_typing

Called:

Name: ktype/2

Module: kodkod_typing

safe_reverse2/3

Block: safe_reverse2(-,?,?)

safe_reverse2([],Acc,Acc).

safe_reverse2([H|T],Acc,Rev) :-
safe_reverse2(T,[H|Acc],Rev).

Calls:

Name: RECURSIVE_CALL/3

Module: kodkod_typing

Called:

Name: safe_reverse/2

Module: kodkod_typing

type_kodkod/4

type_kodkod(KExpr1, Env, OuterType, OuterExpr) :-
    ( KExpr1 = KExpr:ExpectedType ->
    % The expression has an explicit type associated,
    % first make sure that this expected type matches the type seen
    % by the caller (insert cast if necessary)
    unify_kodkod_types(ExpectedType,OuterType,Expr,OuterExpr)
    ;
    % If there is no explicit type given, the type seen by the
    % outside is used as the expected type. No cast is needed
    KExpr=KExpr1, ExpectedType=OuterType, OuterExpr=Expr
    ),
    % Now type-check the expression itself
    type_kodkod2(KExpr, Env, InnerType, InnerExpr),
    % and try to match the types (insert cat if necessary)
    unify_kodkod_types(ExpectedType,InnerType,InnerExpr,Expr).

Calls:

Name: unify_kodkod_types/4	Module: kodkod_typing
Name: type_kodkod2/4	Module: kodkod_typing
Name: =/2
Name: ->/3

Called:

Name: type_kodkod2/4	Module: kodkod_typing
Name: type_kodkod_declaration/6	Module: kodkod_typing
Name: kodkod_insert_casts/4	Module: kodkod_typing
Name: type_quantifier/6	Module: kodkod_typing
Name: type_kodkod3/4	Module: kodkod_typing

type_kodkod2/4

type_kodkod2(relref(Id), Env, rel(Types), relref(Id)) :- !,
    lookup_reltypes(Id,Env,Types).

type_kodkod2(varref(Id), Env, VType, K) :- !,
    lookup_vartypes(Id,Env,Types),
    ( Types = [p2i] ->
    VType = int_expression, K=expr2int(varref(Id))
    ;
    VType = rel(Types), K=varref(Id)).

type_kodkod2(int(I), _Env, int_expression, int(I)) :- !.

type_kodkod2(prj(Pos,Arg), Env, rel(P), prj(Pos,NArg)) :-
    !,type_kodkod(Arg,Env,rel(S),NArg),
    nth0s(Pos,S,P).

type_kodkod2(forall(Decls,Formula), Env, formula, forall(NDecls,NFormula)) :-
    !,type_quantifier(Decls,Formula,Env,_,NDecls,NFormula).

type_kodkod2(exists(Decls,Formula), Env, formula, exists(NDecls,NFormula)) :-
    !,type_quantifier(Decls,Formula,Env,_,NDecls,NFormula).

type_kodkod2(comp(Decls,Expr), Env, rel(Types), comp(NDecls,NExpr)) :-
    !,type_quantifier(Decls,Expr,Env,rel(Types),NDecls,NExpr).

type_kodkod2(Expr, Env, Type, NExpr) :-
    functor(Expr,F,Arity),
    functor(Lookup,F,Arity),
    ktype(Lookup,Type),!,
    Expr =.. [_|Args], Lookup =.. [_|Types],
    maplist(type_kodkod3(Env),Args,Types,NArgs),
    NExpr =.. [F|NArgs].

type_kodkod2(Expr, _Env, _Type, _NExpr) :-
    throw( unsupported_kodkod_expression(Expr) ).

Calls:

Name: throw/1
Name: =../2
Name: maplist/4	Module: foo_error
Name: !
Name: ktype/2	Module: kodkod_typing
Name: functor/3
Name: type_quantifier/6	Module: kodkod_typing
Name: nth0s/3	Module: kodkod_typing
Name: type_kodkod/4	Module: kodkod_typing
Name: =/2
Name: ->/3
Name: lookup_vartypes/3	Module: kodkod_typing
Name: lookup_reltypes/3	Module: kodkod_typing

Called:

Name: type_kodkod/4

Module: kodkod_typing

type_kodkod3/4

type_kodkod3(Env,Expr,Type,NExpr) :-
type_kodkod(Expr,Env,Type,NExpr).

Calls:

Name: type_kodkod/4

Module: kodkod_typing

type_kodkod_declaration/6

type_kodkod_declaration(decl(Id,Arity,Mult,Expr),Env,EnvIn,
    decl(Id,Arity,Mult,NExpr),EnvOut,Types) :-
    add_var_to_type_env(Id,Types,Env,Subenv),
    type_kodkod(Expr,Subenv,rel(Types),NExpr),
    add_var_to_type_env(Id,Types,EnvIn,EnvOut).

Calls:

Name: add_var_to_type_env/4	Module: kodkod_typing
Name: type_kodkod/4	Module: kodkod_typing

Called:

Name: type_kodkod_declarations/6

Module: kodkod_typing

type_kodkod_declarations/6

type_kodkod_declarations([],_,Env,[],Env,[]).

type_kodkod_declarations([Decl|Drest],Env,EnvIn,[NDecl|Nrest],EnvOut,Types) :-
    type_kodkod_declaration(Decl,Env,EnvIn,NDecl,EnvInter,Types1),
    safe_append(Types1,Types2,Types),
    type_kodkod_declarations(Drest,Env,EnvInter,Nrest,EnvOut,Types2).

Calls:

Name: RECURSIVE_CALL/6	Module: kodkod_typing
Name: safe_append/3	Module: kodkod_typing
Name: type_kodkod_declaration/6	Module: kodkod_typing

Called:

Name: type_quantifier/6

Module: kodkod_typing

type_quantifier/6

type_quantifier(Decls,Subexpr,Env,rel(Types),NDecls,NSubexpr) :-
type_kodkod_declarations(Decls,Env,Env,NDecls,Subenv,Types),
type_kodkod(Subexpr,Subenv,formula,NSubexpr).

Calls:

Name: type_kodkod/4	Module: kodkod_typing
Name: type_kodkod_declarations/6	Module: kodkod_typing

Called:

Name: type_kodkod2/4

Module: kodkod_typing

unify_kodkod_types/4

Block: unify_kodkod_types(-,-,?,?)

unify_kodkod_types(rel(A),rel(B),Expr,NewExpr) :- !,
    ( A=B -> Expr=NewExpr
    % both relations can be unified, good
    ; A=[IS],intset_relation_kodkod_name(IS),
    B=[P2I],pow2integer_relation_kodkod_name(P2I) ->
    % expected was a set of integers but given was a set representing
    % one integer by its bits
    % TODO: this conversion is not optimal, better try to avoid rel([p2i])
    NewExpr = int2intset(expr2int(Expr))
    ; A = [P2I],pow2integer_relation_kodkod_name(P2I),
    B = [IS],intset_relation_kodkod_name(IS)
    -> % happens in test 709 when rewriting (x=E or x=F) into x:{E,F}
    % ((x=y or x=z) => (y=x or z=x)) & ((x=y or x=z) <=> (y=x or z=x))
    % Test 2197 tests it explicitly
    NewExpr = int2pow2(expr2int(Expr))
).

unify_kodkod_types(int_expression,int_expression,Expr,Expr) :- !.

unify_kodkod_types(formula,formula,Expr,Expr) :- !.

unify_kodkod_types(rel([R]),int_expression,Expr,int2intset(Expr)) :-
    intset_relation_kodkod_name(R),!.

unify_kodkod_types(rel([R]),int_expression,Expr,int2pow2(Expr)) :-
    pow2integer_relation_kodkod_name(R),!.

unify_kodkod_types(int_expression,rel([_]),Expr,expr2int(Expr)).

Calls:

Name: !
Name: pow2integer_relation_kodkod_name/1	Module: foo_error
Name: intset_relation_kodkod_name/1	Module: foo_error
Name: =/2
Name: ->/2
Name: ->/3

Called:

Name: type_kodkod/4

Module: kodkod_typing

Determinacy Checker

Determinacy Checker:

! Existence error in argument 1 of absolute_file_name/3
! file probsrc(module_information) does not exist
! goal: absolute_file_name(probsrc(module_information),_261,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kodkod/kodkod_typing.pl')])

kodkod_typing

prob_prolog/src/kodkod/kodkod_typing.pl

Modules

Predicates of kodkod_typing

Module Information

220 Lines

25 Predicates

Imported Modules: lists avl kodkod_tools

1 Exports

2 specified Imports

Predicates:

add_to_refmap/3

add_var_to_type_env/4

complete_list/2

create_refmap/3

create_refmap_ids/3

create_refmap_types/3

get_rel_types/3

kodkod_insert_casts/4

ktype/2

lookup_reltypes/3

lookup_vartypes/3

nth0s/3

nth0s2/3

remove_relation_wrapper/2

safe_append/3

safe_append2/6

safe_reverse/2

safe_reverse2/3

type_kodkod/4

type_kodkod2/4

type_kodkod3/4

type_kodkod_declaration/6

type_kodkod_declarations/6

type_quantifier/6

unify_kodkod_types/4

Determinacy Checker: