ProLin/OneInstancePerParticipant.pli at master · GU-CLASP/ProLin · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
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
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
-- hardcoding user moves.
start :: Heard (Greet USER SYSTEM);
q1    : (t : Time) -> (n : Bus) -> (d : Location) ->
        Utter (CounterGreet SYSTEM USER) -o
	Heard (Ask (Question USER Time t (TT n t Gotaplatsen d)) USER SYSTEM);

-- q2a : (n0 : Bus) -> Utter (Ask (Question SYSTEM Bus n0 (WantBus n0)) SYSTEM USER) -o
--      Heard ((ShortAnswer Bus B55) USER SYSTEM);

q2b : (n0 : Bus) -> Utter (Ask (Question SYSTEM Bus n0 (WantBus n0)) SYSTEM USER) -o
     Heard (Assert (WantBus B55) USER SYSTEM);


-- initial state
ready :: HasTurn USER;
noMoves :: Moves Nil;
noQud :: QUD Nil;


utterAndRemember :
  (m : DP -> DP -> Move) ->
  (ms : List Move) ->
  (x y : DP) ->
  Agenda (m x y) -o
  Moves ms -o
  HasTurn x -o
  [_ :: Utter (m x y);
   _ :: Moves (Cons (m x y) ms);
   _ :: HasTurn y];

hearAndRemember  :
  (m : DP -> DP -> Move) ->
  (x y : DP) ->
  (ms : List Move) ->
  Heard (m x y) -o
  Moves ms -o
  HasTurn x       -o
  [_ :: Moves (Cons (m x y) ms);
   _ :: Pending (m x y) ;
   _ :: HasTurn y ];

greeting : (x y : DP) ->
           HasTurn x -o
           WishToOpenDialogueWith y -o
           Agenda Nil -o
           [_ :: Agenda (Greet x y)
           ];

counterGreeting : (x y : DP) ->
                  HasTurn x -*
                  Pending (Greet y x)  -o
                  [_ :: Agenda (CounterGreet x y)];

processShort : (a : Type) -> (x : a) ->  (p : Prop) ->
  (qs : List Question) -> (dp dp1 : DP) ->
  Pending (ShortAnswer a x dp1 dp) -o QUD (Cons (Question dp a x p) qs) -o
  [ _ :: UserFact p;
    _ :: QUD qs];

processAssert : (a : Type) -> (x : a) ->  (p : Prop) ->
  (qs : List Question) -> (dp dp1 : DP) ->
  Pending (Assert p dp1 dp) -o QUD (Cons (Question dp a x p) qs) -o
  [ _ :: UserFact p;
    _ :: QUD qs];

-- JG2012: (4.30)
pushQUD :
   (q : Question) -> (qs : List Question) ->
   (x y : DP) ->
   Pending (Ask q x y) -o QUD qs -o
   [_ :: QUD (Cons q qs)
   ];

produceAnswer :
   (a : Type) ->
   (x : a) !->
   (p : Prop) ->
   (qs : List Question) ->
   QUD (Cons (Question USER a x p) qs) -o
   p -*
   [_ :: Agenda (ShortAnswer a x SYSTEM USER);
    _ :: QUD qs;
    _ :: Answered (Question USER a x p)];

produceCR :
   [a : Type
   ;x : a
   ;p : Prop
   ;qs : List Question
   ;_ :: QUD (Cons (Question USER a x p) qs)
   ;_ :: p
   ] ?->
   CR;


-- === DOMAIN KNOWLEDGE ===

-- knowledge base 1 (no CR)
kb1  :: TT B18 T15   Gotaplatsen     Johanneberg ;
kb2  :: TT B55 T20   Gotaplatsen     SciencePark ;

specificCR :
  (t : Time) -> (n : Bus) -> (s d : Location) ->
  (qs : List Question) ->
  CR -o
  QUD (Cons (Question USER Time t  (TT n  t  s           d))  qs) -o
  [_ :: QUD (Cons (Question SYSTEM Bus n (WantBus n))
            (Cons (Question USER Time t (TT n t s d)) qs));
   _ :: Agenda (Ask (Question SYSTEM Bus n (WantBus n)) SYSTEM USER) ];