Check-in [abb4d08745]

Not logged in

Many hyperlinks are disabled.
Use anonymous login to enable hyperlinks.

Overview
Comment:Fixed (maybe) the filtering of substitutions for "interesting" variables.
Downloads: Tarball | ZIP archive | SQL archive
Timelines: family | ancestors | descendants | both | bc-subst
Files: files | file ages | folders
SHA1:abb4d08745a5c1a1d24670b6e40bc9e721790280
User & Date: andy 2015-04-20 20:57:33
Context
2015-04-20
20:58
Updated checker module to work with the new atomic goal expansions. check-in: 4e6407ce10 user: andy tags: bc-subst
20:57
Fixed (maybe) the filtering of substitutions for "interesting" variables. check-in: abb4d08745 user: andy tags: bc-subst
09:54
Started work on making backchaining of goals a) apply the substitution to the expansion, rather than appending it as a conjunction of unifications, b) return the substitution along with each branch of the expansion, and c), return the name of the branch that was chosen (analogous to the index N parameter in `choice` proofs). check-in: 1252a63f55 user: andy tags: bc-subst
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Changes to plsrc/subst.pl.

12
13
14
15
16
17
18

19
20
21
22
23
24
25
..
62
63
64
65
66
67
68
69
70






71
72
73
74


75
76

77


78
79
80
81
82
83
84
    get_subst/3,
    get_subst/2,
    apply_subst/3,
    subst_filter/3
]).

:- use_module(library(lists)).


% An explicit substituion is a list of the form [var=value,...]. The variables
% are special atoms whose names are of the form ' varname' (i.e., they start
% with a space). The parser for specifications/reasoning will not parse atoms
% that start with a space, so it is (hopefully) impossible for users to create
% "new" variables.
%
................................................................................
lookup(Subst,Var,Value) :-
    member((Var=Value),Subst), !.

% If not an element of the substitution, then variables lookup to themselves.
lookup(_,Var,Var).

% subst_filter(Subst,Vars,S2)
% Filter the substitution so that it only contains bindings for variables in
% Vars.






subst_filter([],_,[]).
subst_filter([V = Val|Ss],Vars,[V = Val|S2]) :-
    member(V,Vars), 
    !,


    subst_filter(Ss,Vars,S2).
subst_filter([_|Ss],Vars,S2) :-

    subst_filter(Ss,Vars,S2).





% extend(Subst,Var=Value,NewSubst)
% Extend a substitution with a new binding. This will fail if the new binding 
% is inconsistent with the existing bindings.
% This isn't the most efficient way to go about this, but it's the most robust.







>







 







|
|
>
>
>
>
>
>


|
<
>
>
|
<
>
|
>
>







12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
..
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80

81
82
83

84
85
86
87
88
89
90
91
92
93
94
    get_subst/3,
    get_subst/2,
    apply_subst/3,
    subst_filter/3
]).

:- use_module(library(lists)).
:- use_module(program,[get_vars/2]).

% An explicit substituion is a list of the form [var=value,...]. The variables
% are special atoms whose names are of the form ' varname' (i.e., they start
% with a space). The parser for specifications/reasoning will not parse atoms
% that start with a space, so it is (hopefully) impossible for users to create
% "new" variables.
%
................................................................................
lookup(Subst,Var,Value) :-
    member((Var=Value),Subst), !.

% If not an element of the substitution, then variables lookup to themselves.
lookup(_,Var,Var).

% subst_filter(Subst,Vars,S2)
% Filter the substitution so that it only contains bindings for variables that
% can be traced back to those in Vars. Note that this is not the same as 
% just filtering for the bindings of variables in Vars. E.g., in 
%
%   subst_filter([x = s(n), n = z],[x],S2)
%
% we want 'n' to be in the output substitution, too, since without it the 
% substitution for x does not make any sense.
subst_filter([],_,[]).
subst_filter([V = Val|Ss],Vars,[V = Val|S2]) :-
    (member(V,Vars) -> 

        program:get_vars(Val,V2),
        union(Vars,V2,NewVars),
        subst_filter(Ss,NewVars,S2)

    ;
        subst_filter(Ss,Vars,S2)
    ).




% extend(Subst,Var=Value,NewSubst)
% Extend a substitution with a new binding. This will fail if the new binding 
% is inconsistent with the existing bindings.
% This isn't the most efficient way to go about this, but it's the most robust.