kos2.pli

-- rules
-- Note: inputs come as "LatestMove"

qudPush : (a:Type) -> (x:a -> Prop) -> LatestMove (Ask x)
   -o [c1 :: QUD (Q a x)];
processAnswer :  (a : Type) -> (answer:a) -> (q:a->Prop) -> LatestMove (Answer (Q a q) answer p)
   -o QUD (Q a q) -o [newFact :: (q a); _ :: Output (Ack ??? )];
produceAnswer :  (a : Type) -> (answer:a) -> (q:a->Prop) -> (proof:q answer)
   -o QUD (Q a q) -o [_ :: Output (Answer (Q a p) answer proof)];
-- fulfillAgenda : (x:Move) -> (Agenda x) -o TTake -o [r :: TRelease; o :: Output x];
assertQudInc1 : (x:Prop) -> LatestMove (Assert x) -o    [c2 :: TTake; isFact :: x; _ :: Output (Ack x)]; -- take the assertion as fact immediately
assertQudInc2 : (x:Prop) -> LatestMove (Assert x) -o    [c2 :: TTake; QUD (Q Bool (\a -> if a then x else not x)); _ :: Output (Confirmation x)]; -- confirmation request
train : (x:Object) -> (y:Name) -> (pred:Object->Name->Prop) -> QUD (pred x y) -o Train x y;
--greeting : TRelease -o UserLM NoMoves -> QUD Empty -> [f1 :: TTake; f2 :: Output Greeting];

-- Bool :: Type
-- True :: Prop
-- Q :: (a : Type) -o (p : A -o Prop) -o Question; (This interpreted as does it exist x:A such that p(x))
-- Answer :: (q :: Question) -> (x : q.a) -> q.p x -> Move
-- Ask :: (a -> Prop) -o Move
-- QUD :: Question -o Type
-- LatestMove :: Move -o Type
-- Agenda ::   Move -o Type
-- Assert :: Prop -o Move

-- context
is :: Object -> Name -> Prop;
cl001 :: Object;
cup  :: Name;
p2 :: is cl001 cup;
lm :: LatestMove (Ask (is cl001)); -- NLU (...)
--lm2 :: LatestMove (Greeting); 
--lm :: LatestMove (Assert (is cl001 cup));
--a1 :: Agenda (Greeting);
--turn :: TRelease;
--c1 :: LatestMove NoMoves;
--c2 :: QUD Empty;
-- c3 :: QNUD Empty;



-- Question :: (A:Type) -> (A -> Prop) -> Move
-- Greeting :: Move

-- Answer :: (A:Type) -> (Q:A->Prop) -> (a:A) -> (q: Q a) -> Move

-- ans : (pred : Type -> Prop) -> (obj : Type) -> (a:obj) -> (b:Type)
--    -> (q: (pred obj b)) -o QUD (pred obj) -o Ok;
-- Agenda (Assert obj pred a q);

-- p1 :: See cl001;

-- r : (q:Type) -> (a : Object) -> QUD (q a) -o Ok