diff options
Diffstat (limited to 'transfer/examples/reflexive/reflexive.tra')
| -rw-r--r-- | transfer/examples/reflexive/reflexive.tra | 40 |
1 files changed, 0 insertions, 40 deletions
diff --git a/transfer/examples/reflexive/reflexive.tra b/transfer/examples/reflexive/reflexive.tra deleted file mode 100644 index 8d28f0db0..000000000 --- a/transfer/examples/reflexive/reflexive.tra +++ /dev/null @@ -1,40 +0,0 @@ -{- - -$ ../../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 - --}
\ No newline at end of file |