blob: 05cdfc9ae537c99abf8db4392b027c78ee6d1f48 (
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
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
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
|
module Data.Term.Zipper
import Data.DPair
import Data.Fin.Occurs
import Data.Vect.Properties.Map
import Data.Term
import Syntax.PreorderReasoning
-- Utilities -------------------------------------------------------------------
mapInsertAt :
(0 f : a -> b) ->
(i : Fin (S k)) ->
(x : a) ->
(xs : Vect k a) ->
map f (insertAt i x xs) = insertAt i (f x) (map f xs)
mapInsertAt f FZ x xs = Refl
mapInsertAt f (FS i) x (y :: xs) = cong (f y ::) $ mapInsertAt f i x xs
insertAtDeleteAt :
(i : Fin (S k)) ->
(xs : Vect (S k) a) ->
insertAt i (index i xs) (deleteAt i xs) = xs
insertAtDeleteAt FZ (x :: xs) = Refl
insertAtDeleteAt (FS i) (x :: xs@(_ :: _)) = cong (x ::) $ insertAtDeleteAt i xs
indexInsertAt :
(i : Fin (S k)) ->
(x : a) ->
(xs : Vect k a) ->
index i (insertAt i x xs) = x
indexInsertAt FZ x xs = Refl
indexInsertAt (FS i) x (y :: xs) = indexInsertAt i x xs
-- Definition ------------------------------------------------------------------
public export
data Zipper : Signature -> Nat -> Type where
Top : Zipper sig n
Op : sig.Operator (S k) -> Fin (S k) -> Vect k (Term sig n) -> Zipper sig n -> Zipper sig n
%name Zipper zip
-- Monoid ----------------------------------------------------------------------
export
(++) : Zipper sig n -> Zipper sig n -> Zipper sig n
Top ++ zip2 = zip2
Op op i ts zip1 ++ zip2 = Op op i ts (zip1 ++ zip2)
-- Properties
export
leftUnit : (zip : Zipper sig n) -> Top ++ zip = zip
leftUnit zip = Refl
export
rightUnit : (zip : Zipper sig n) -> zip ++ Top = zip
rightUnit Top = Refl
rightUnit (Op op i ts zip) = cong (Op op i ts) (rightUnit zip)
export
assoc : (zip1, zip2, zip3 : Zipper sig n) -> (zip1 ++ zip2) ++ zip3 = zip1 ++ (zip2 ++ zip3)
assoc Top zip2 zip3 = Refl
assoc (Op op i ts zip1) zip2 zip3 = cong (Op op i ts) (assoc zip1 zip2 zip3)
-- Action ----------------------------------------------------------------------
-- NOTE: should this be public?
public export
(+) : Zipper sig n -> Term sig n -> Term sig n
Top + t = t
Op op i ts zip + t = Op op (insertAt i (zip + t) ts)
-- Properties
export
actionAssoc :
(zip1, zip2 : Zipper sig n) ->
(t : Term sig n) ->
(zip1 ++ zip2) + t = zip1 + (zip2 + t)
actionAssoc Top zip2 t = Refl
actionAssoc (Op op i ts zip1) zip2 t =
cong (\t => Op op (insertAt i t ts)) $ actionAssoc zip1 zip2 t
-- Substitution ----------------------------------------------------------------
export
(<$>) : (Fin k -> Term sig n) -> Zipper sig k -> Zipper sig n
f <$> Top = Top
f <$> Op op i ts zip = Op op i (map (f <$>) ts) (f <$> zip)
-- Properties
export
actionHomo :
(0 f : Fin k -> Term sig n) ->
(zip : Zipper sig k) ->
(0 t : Term sig k) ->
f <$> zip + t = (f <$> zip) + (f <$> t)
actionHomo f Top t = Refl
actionHomo f (Op op i ts zip) t = cong (Op op) $ Calc $
|~ map (f <$>) (insertAt i (zip + t) ts)
~~ insertAt i (f <$> zip + t) (map (f <$>) ts) ...(mapInsertAt (f <$>) i (zip + t) ts)
~~ insertAt i ((f <$> zip) + (f <$> t)) (map (f <$>) ts) ...(cong (\t => insertAt i t (map (f <$>) ts)) $ actionHomo f zip t)
export
invertActionTop : (zip : Zipper sig k) -> (0 _ : f <$> zip = Top) -> zip = Top
invertActionTop Top prf = Refl
-- Cycles ----------------------------------------------------------------------
pivotAt : sig.Operator (S k) -> Fin (S k) -> Vect (S k) (Term sig n) -> Zipper sig n
pivotAt op i ts = Op op i (deleteAt i ts) Top
actionPivotAt :
(op : sig.Operator (S k)) ->
(i : Fin (S k)) ->
(ts : Vect (S k) (Term sig n)) ->
pivotAt op i ts + index i ts = Op op ts
actionPivotAt op i ts = cong (Op op) $ insertAtDeleteAt i ts
pivotNotTop : (zip : Zipper sig k) -> Not (zip ++ pivotAt op i ts = Top)
pivotNotTop (Op op' j us zip) prf impossible
export
noCycles : (zip : Zipper sig k) -> (t : Term sig k) -> zip + t = t -> zip = Top
noCycles Top t prf = Refl
noCycles (Op {k} op i ts zip') t@(Op {k = S j} op' us@(_ :: _)) prf =
void $ pivotNotTop zip' prf''
where
i' : Fin (S k)
i' = i
I : Fin (S j)
I = replace {p = Fin} (opInjectiveLen prf) i
prf' : ((zip' ++ pivotAt op' I us) + index I us = index I us)
prf' = Calc $
|~ (zip' ++ pivotAt op' I us) + index I us
~~ zip' + (pivotAt op' I us + index I us) ...(actionAssoc zip' (pivotAt op' I us) (index I us))
~~ zip' + Op op' us ...(cong (zip' +) $ actionPivotAt op' I us)
~~ index i (insertAt i (zip' + Op op' us) ts) ..<(indexInsertAt i (zip' + Op op' us) ts)
~~ index i (rewrite opInjectiveLen prf in us) ...(cong (index i) $ opInjectiveTs prf)
~~ index I us ...(rewrite opInjectiveLen prf in Refl)
prf'' : zip' ++ pivotAt op' I us = Top
prf'' = noCycles (zip' ++ pivotAt op' I us) (assert_smaller t (index I us)) prf'
|
