cpsa-4.4.5: src/cpsa4prolog.pl
% -*- mode: prolog -*-
%% Library of predicates for analyzing cpsa4dbprolog output
%% The cpsa4db and cpsa4dbprolog programs are used to analyze the
%% output of cpsa4. They translate cpsa4 output into a Prolog database
%% that captures the essential features of the output in a form that
%% can be queried using all of the power and flexibility of Prolog.
%% cpsa4db assembles the skeletons in the output into a forest of
%% derivation trees. cpsa4dbprolog then prints the forest in Prolog
%% syntax. To be loadable by Prolog, the output must be sorted so
%% that clauses of one predicate are colocated. The sorting program
%% provided in all dialects of Unix does the job.
%% The output should be used by SWI Prolog as strings must not be
%% atoms. Load the file generated by cpsa4prolog using consult/1.
%% Next load your query. This file contains useful predicates that
%% may help formulate your query. The comments for each predicate are
%% intended help users understand the output format.
%% Copyright (c) 2024 The MITRE Corporation
%% This program is free software: you can redistribute it and/or
%% modify it under the terms of the BSD License as published by the
%% University of California.
%% PATHS
%% The predicate path(L, Ls) is true if Ls is a path through the
%% derivation tree that starts with label L and ends with the label of
%% a skeleton that is at the root of the tree that contains L. The
%% path predicate uses the step/3 predicate to determine if a skeletion
%% was derived from another skeleton.
%% The step predicate defines a transition relation for individual
%% cpsa4 steps. step(P, O, L) is true if a cpsa4 step that started at
%% the skeleton labeled P produced a skeleton labeled L using the
%% operation O. Notice that the same skeleton can appear as the
%% result of a step starting at different skeletons. This means the
%% path predicate can find more than one path to the root.
%% For the path predicate, the operation field information is not
%% used.
path(L, [L]) :-
root(L).
path(L, [L|Ls]) :-
step(P, _, L),
path(P, Ls).
%% A derivation tree is really a directed acyclic graph. If the links
%% used for seen children are removed, the derivation tree becomes a
%% true tree--every child has exactly one parent. The child/2
%% predicate encodes that relation. It is used to traverse the tree
%% without revisiting a skeleton twice. One can use it to count the
%% number of skeletons in a tree, for example. Here we use it to find
%% the terminal skeletons without deplicates. A terminal node is one
%% that has no successors.
terminal(L) :-
step(L, _, _), !,
fail.
terminal(_).
acc(W, W).
acc(W, X) :-
child(W, Y),
acc(Y, X).
%% A query to find the terminal skeletons using these predicates follows.
%% ask(L) :-
%% root(W), acc(W, L), terminal(L).
%% SKELETON ASSOCIATION LISTS
%% The body of a skeleton is available as an association list. It can
%% be queried using has_key_val(L, K, V), where L is a skeleton label,
%% K is a key, and V is its value.
has_key_val(L, K, V) :-
skel(L, A),
assoc(A, K, V).
assoc([[K | V] | _], K, V).
assoc([_ | A], K, V) :-
assoc(A, K, V).
%% A query to find the labels of skeletons that are not eventually
%% dead follows.
%% ask(L) :-
%% root(W), acc(W, L), acc(L, X), terminal(X), \+has_key_val(X, dead, _).
%% ask_all(Ls) :-
%% findall(L, ask(L), Ls).