blob: 8d28f0db0b05a56d342d0fdaa83acef27d90891f (
plain)
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
|
{-
$ ../../transferc -i../../lib reflexive.tra
$ gf English.gf reflexive.trc
> p -tr "John sees John" | at -tr reflexivize_S | l
PredV2 See John John
ReflV2 See John
John sees himself
> p -tr "John and Bill see John and Bill" | at -tr reflexivize_S | l
PredV2 See (ConjNP And John Bill) (ConjNP And John Bill)
ReflV2 See (ConjNP And John Bill)
John and Bill see themselves
> p -tr "John sees Mary" | at -tr reflexivize_S | l
PredV2 See John Mary
PredV2 See John Mary
John sees Mary
-}
import tree
reflexivize : (C : Cat) -> Tree C -> Tree C
reflexivize _ (PredV2 v s o) | eq ? (eq_Tree ?) s o = ReflV2 v s
reflexivize _ t = composOp ? ? compos_Tree ? reflexivize t
reflexivize_S : Tree S -> Tree S
reflexivize_S = reflexivize S
{-
With a type checker and hidden arguments we could write:
reflexivize : {C : Cat} -> Tree C -> Tree C
reflexivize (PredV2 v s o) | s == o = ReflV2 v s
reflexivize t = composOp reflexivize t
-}
|
