%---------------------------------------
% Foundations of Language Interaction
% Program Three: Intentions, Knowledge and Choice
% M. Stone, 6-07-01
% mdstone@cs.rutgers.edu
%---------------------------------------

%---------------------------------------
% Truth in knowledge databases.
%---------------------------------------

module LK.

kind agent, object, fact	type.

%---------------------------------------
% Building blocks of a logic of knowledge.
%   k A F : agent A knows fact F
%   sm x\FL x : there is an x for which 
%       all the facts in (FL x) are true.
%---------------------------------------

type k	    agent -> fact -> fact.
type sm	    (object -> list fact) -> fact.
type self   agent.
type other  agent.
type all    agent.

%---------------------------------------
% Match F G
%    true if G follows when F is true.
% Builds in simple relationships among
%    modalities, so as to automate the
%    inferences of veridicality and
%    positive introspection (with search).
% Cuts ensure one F-G match, avoiding
%    ambiguities with multiple operators.   
%---------------------------------------

type m_match agent -> agent -> o.

m_match all Any.
m_match self self.
m_match other other.

type match  fact -> fact -> o.

% Axiom.   
match F F :- !.

% Veridicality.
match (k A F) G :- match F G, !.

% Positive introspection.
match (k A F) (k B G) :-
	m_match A B,
	match (k A F) G, 
	!.

%---------------------------------------
% Entailment
%    does one body of facts follow
%    from another; computed using match.
% entail_one KB G
%    true if F follows from KB.
%    multiple matches are appropriate
%    since they may involve distinct
%    values for variables.
% entail_all KB Gs
%    true if all Gs follow from KB.      
%---------------------------------------

type entail_one   list fact -> fact -> o.

entail_one (F::_) G :-
	   match F G.

entail_one (_::Fs) G :-
	   entail_one Fs G.

type entail_all  list fact -> list fact -> o.

entail_all KB nil.
entail_all KB (G::Gs) :-
	   entail_one KB G,
	   entail_all KB Gs.

%---------------------------------------
% know_all Ag KB Gs
%    like entail_all, but true only if
%    each fact in Gs is of the form 
%    (k Ag G). 
%---------------------------------------

type know_all	agent -> list fact -> list fact -> o.

know_all Ag KB nil.
know_all Ag KB ((k Ag G) :: Gs) :-
	 entail_one KB (k Ag G),
	 know_all Ag KB Gs.

%---------------------------------------
% make_known A Fs KB
%   shortcut for perception: true if
%   KB is a list of (k A F) for each
%   F in Fs.
%---------------------------------------

type make_known agent -> list fact -> list fact -> o.

make_known Ag nil nil.
make_known Ag (F :: Fs) ((k Ag F) :: Gs) :-
	   make_known Ag Fs Gs.

%%%%%%%%%%%%%%
%---------------------------------------
% List Processing
%---------------------------------------

module Lists.

type member	A -> list A -> o.
type remove_elt	A -> list A -> list A -> o.
type remove	list A -> list A -> list A -> o.
type sublist	list A -> list A -> o.
type disjoint	list A -> list A -> o.
type union 	list A -> list A -> list A -> o.

% (member A L) if A is an element of L.

member A (A :: R).
member A (H :: R) :- member A R.

% (sublist L1 L2) if 
%    every element of L1 is an element of L2.

sublist nil L.
sublist (E::R) L :-
	member E L,
	sublist R L.

% (remove_elt A L1 L2) if
%    L2 is like L1 except that
%    all occurrences of A are 
%    omitted in L2.

remove_elt A nil nil.
remove_elt A (A::R) G :- !,
	remove_elt A R G.
remove_elt A (E::R) (E::L) :-
	remove_elt A R L.

% (remove R L1 L2) if
%    L2 is like L1 except that
%    all occurrences of elements of R
%    are omitted in L2.

remove nil L L.
remove (A::R) L F :-
	remove_elt A L M,
	remove R M F.
	
% (disjoint L R) if
%     L and R have no elements in common.

disjoint L R :-
	not (sigma e\ (member e L, member e R)).

% (union X Y Z) if
%      Z is a list with the elements of
%      X in order followed by the elements
%      of Y in order.

union nil R R.
union (A::L) R (A::U) :-
	union L R U.

%%%%%%
%---------------------------------------
% Plan checking with knowledge and choice
% (and strips-style action representation)
%---------------------------------------

module KnowledgePlan.
accumulate LK.
accumulate Lists.

%---------------------------------------
% actions are things you can do

kind action	type.

%---------------------------------------
%
% plans are structures showing how
%    doing a sequence of action
%    in the current circumstances
%    leads to desired effects.
% (finish G) represents the endpoint,
%     when desired facts G are true.
% (step Circ Agent Act Subs) represents
%     a staged plan, that must be
%     executed when Circ are all true;
%     first Agent will do Act, then we
%     continue with plan Subs.
% (whatever Circ Char Fn) represents
%     a plan with a possible instantiation
%     in the current circumstances Circ.
%     There must be an individual x
%     characterized by (Char x), and 
%     for any such x, (Fn x) is the plan
%     to carry out.
% (find Action Plan) is an annotation 
%     on plan Plan that indicates the scope
%     required for the action term Action.
% (know Agent Circ Plan) represents a
%     stage of deliberation for agent Agent,
%     in which facts Circ characterize Agent's
%     information, and this information supports
%     the plan Plan.

kind plan		type.

type finish	list fact -> plan.
type step	list fact -> 
		agent -> action -> plan -> plan.
type whatever	list fact -> 
		(object -> list fact) -> (object -> plan) -> plan.
type find	action -> plan -> plan.
type know	agent -> list fact -> plan -> plan.

%---------------------------------------

type describe_plan plan -> o.

% (describe_plan Plan)
%   Always true; as a side-effect, print out
%   a sketchy description of Plan to the terminal.

describe_plan (finish A) :-
	output std_out "finish.\n".

describe_plan (step Circ Ag Act P) :-
	term_to_string Act ActS,
	term_to_string Ag AgS,
	Z is (AgS ^ " will do " ^ ActS ^ "; "),
	output std_out Z,
	describe_plan P.

describe_plan (whatever Circ Char PFn) :-
	pi o\ (describe_plan (PFn o)).

describe_plan (find A P) :-
	describe_plan P.

describe_plan (know A C P) :-
	describe_plan P.

%---------------------------------------

type circ	plan -> list fact -> o.

% (circ P Circ)
%     true if Circ are the circumstances
%     required now for P to be pursued to
%     success.

circ (finish Goals) Goals.
circ (step Pre Ag Act Plan) Pre.
circ (whatever Pre Char PFn) Pre.
circ (know Ag Pre Plan) Pre.
circ (find A Plan) Pre :- circ Plan Pre.

type subplan	plan -> plan -> o.

% (subplan P Q)
%   true if Q may be the plan to be
%   considered next upon embarking on P.

subplan (whatever _ _ PFn) (PFn O).
subplan (step _ _ _ P) P.
subplan (know _ _ P) P.
subplan (find _ P) P.

%----------------------------------------

type applies	list fact -> plan -> o.

% (applies Circ Plan)
%     true if Plan can be executed in Circ

applies Facts Plan :-
	circ Plan Deps,
	entail_all Facts Deps.

%----------------------------------------

type is_action	action -> list fact -> list fact -> list fact -> o.

% The domain will specify an inventory of action in
% STRIPS representation:
%	(is_action A Preconditions Additions Deletions) 
% true if action A can be executed in a state where
% Preconditions are all true, resulting in establishing
% all the facts in Additions as true while terminating
% all the relationships in Deletions.

%----------------------------------------

type consistent		plan -> o.
kind check_state	type.
type check_plan		list fact -> check_state -> plan -> o.

% consistent Plan
%    is true if Plan actually maps out a good
%    argument about a successful course of deliberation,
%    choice and action for a group of agents.
%
% This involves a check to make sure that factual
% dependencies are propagated through the proof
% in a way that respects inferences about knowledge
% and action in the domain, as with ordinary plans.
% It also involves a check to make sure that the
% structure of the plan faithfully reflects the 
% decision-making processes of an agent.  This
% means checking for the order of operators:
%   (find Act ... know Ag ... step Ag Act ...)*
%   (know Ag ... finish G)
% Both checks are admininstered by the check_plan
% relation, which has auxiliary arguments for the
% list of circumstances assumed, and a check_state
% entry indicating where in the finite state
% plan description we are.

consistent Plan :-
	circ Plan Facts,
	check_plan Facts ics Plan.


type ics		check_state.
type mcs		action -> check_state.
type ks			agent -> check_state -> check_state.


check_plan C (ks A ics) (finish G) :-
	   entail_all C G.

check_plan C State (whatever Pre Char PFn) :-
	   entail_all C Pre,
	   pi o\ sigma c'\(union (Char o) Pre c',
                           check_plan c' State (PFn o)).

check_plan C State (know A K P) :-
	   know_all A C K,
	   check_plan K (ks A State) P.

check_plan C ics (find A P) :-
	   check_plan C (mcs A) P.

check_plan C (ks Ag (mcs Act)) (step MC Ag Act Plan) :-
	   entail_all C MC,
	   is_action Act Pre Add Del,
	   entail_all MC Pre,
	   remove Del MC Temp,
	   union Temp Add C',
	   check_plan C' ics Plan.

%---------------------------------------

type split	plan -> action -> plan -> o.
type scan	plan -> plan -> o.

% (split Whole First Rest)
%	split divides up a plan
%	the current stage of action and
%	subsequent stages of deliberation.
% It's true if First is the first
% action in plan Whole, and Rest
% contains the suplan starting with
% the specification of the acting
% agent's knowledge at the following stage of
% deliberation and choice.

split (step _ _ A P) A N :-
      !,
      scan P N.

split P A N :-
      subplan P P',
      split P' A N.

scan (know A C P) (know A C P) :- !.

scan P N :-
     subplan P P',
     scan P' N.

%------------------------------------------

type achieves plan -> list fact -> o.

% (achieves Plan Goals)
%     True if Plan results in quantifier-free
%     conditions Goals being true at the end
%     of the plan.

achieves (finish Gs) Fs :-
	 !,
	 entail_all Gs Fs.

achieves P Fs :-
	 subplan P P',
	 achieves P' Fs.

%---------------------------------------

%%%%%%
%---------------------------------------
% Simulation Loop for an Agent with Intentions.
%---------------------------------------

module IntendingKnowAgent.
accumulate KnowledgePlan.

%---------------------------------------
%
% As always we'll record the agent's
% history in state data structures.

kind state 	type.
type start	state.
type do		action -> state -> state.

%---------------------------------------
% Interact with the world 
%    (via side effects).

type perceive	state -> list fact -> o.

perceive State Knowledge :-
	output std_out "What is agent's current db?\n",
	input_line std_in FactString,
	string_to_term FactString Facts,
	make_known self Facts Knowledge.

type execute	state -> action -> o.

execute State Action :-
	output std_out "Agent performs action ",
	term_to_string Action AS,
	output std_out AS,
	output std_out ".\n\n".

%---------------------------------------
%
% At this stage, it would be too cumbersome
% to worry about search for plans, because
% it would take us into the hairy business
% of modal deduction.
%
% So we'll just have a set of plans that the
% agent can consider - the proposition
%
% (stored_plan P)
%
% will be true if P is in that set.  Before
% running any (new) agent, the predicate
%   
% (store_consistent)
%
% can be used to make sure
% that all these data structures are 
% correctly defined.

type stored_plan plan -> o.
type store_consistent o.

store_consistent :-
	not (stored_plan P,
	     not (consistent P)).

%---------------------------------------
%
% Predicates describing deliberation.
%   At each point, the agent has a
%   history and its intentions for the future.

type agitate 	state -> list fact -> plan -> o.
type act 	state -> list fact -> plan -> o.
type update	state -> list fact -> list fact -> plan -> plan -> o.
   
% Agent simulation involves carrying out a
%    Perception,
%    Deliberation,
%    Action 
% loop. ! here keeps time flowing forward. 

agitate State Goals Intentions :-
	perceive State Knowledge,
	update State Knowledge Goals Intentions NewIntentions,
	!,
	act State Goals NewIntentions.

% Act:
%  Do the next action, and continue
%    deliberating.
%  If no next action, you're done: Stop.

act State Goals ComplexPlan :-
	split ComplexPlan Action Next,
	!,
	execute State Action,
	agitate (do Action State) Goals Next.

act _ _ _.

% To determine your new intentions:
% - continue with what you were doing, if it's working,
% - try something else, otherwise.

update State Facts Goals Plan Plan :-
	applies Facts Plan,
	output std_out "Agent continues with plan.\n".

update State Facts Goals Plan Next :-
        stored_plan Next,
	achieves Next Goals,
	applies Facts Next,
	output std_out "Agent decides ",
	describe_plan Next.

%%%%%%
%---------------------------------------
% Test domain.
%---------------------------------------

module A6.
accumulate IntendingKnowAgent.

type full	fact.
type food	object -> fact.

type look	action.
type eat	object -> action.

type f7		object.

is_action look  ((food X)::nil) ((k self (food X))::nil) nil.
is_action (eat X) ((food X)::nil) ((k self full)::nil) ((food X)::nil).

stored_plan (find look
	     (know self ((k self (sm x\ ((food x)::nil)))::nil)
	      (whatever ((sm x\ ((food x)::nil))::nil)
			(x\ ((food x)::nil))
			f\ (step ((food f)::nil)
			    self look
			    (find (eat f)
			     (know self ((k self (food f))::nil)
			      (step ((food f)::nil)
			       self (eat f)
			       (know self ((k self full)::nil)
			        (finish (full::nil)))))))))).

% :- agitate start (full::nil) (finish (full::nil)).
%
% First perception - there must be some food.
%
% (sm x\ ((food x)::nil)) :: nil.
%
% Next perception - f7 is the food.
%
% (food f7)::nil.
%
% Final state: yum.
%
% full::nil.