0 | module Goop.Diff.Algo.Naive
 1 |
 2 | import Data.Vect
 3 | import Decidable.Equality
 4 |
 5 | import Goop.Diff.Interface
 6 |
 7 | %default total
 8 |
 9 | public export
10 | data Modification : Vect n item -> Vect m item -> Type where
11 |   Insert : {0 prev : Vect n item} -> (idx : Fin (S n)) -> (it : item)
12 |     -> Modification prev (insertAt idx it prev)
13 |   Delete : {0 prev : Vect (S n) item} -> (idx : Fin (S n))
14 |     -> Modification prev (deleteAt idx prev)
15 |
16 |
17 | deletePrf : {idx : _}
18 |   -> (x :: deleteAt idx intermediate) = deleteAt (FS idx) (x :: intermediate) 
19 | deletePrf {idx = FZ} = 
20 |   rewrite lemma intermediate {y = x} in Refl
21 |   where
22 |     lemma : (ys : Vect (S n) item) -> deleteAt (FS FZ) (y :: ys) = y :: deleteAt FZ ys
23 |     lemma (z :: zs) = Refl
24 | deletePrf {idx = (FS y)} = 
25 |   rewrite lemma intermediate {idx = (FS y)} {y = x} in Refl
26 |   where
27 |     lemma : (ys : Vect (S n) item) 
28 |       -> {0 y : item}
29 |       -> deleteAt (FS idx) (y :: ys) = y :: deleteAt idx ys
30 |     lemma (z :: xs) = Refl
31 |
32 | extend : {x : item}
33 |   -> Chain len Vect Modification input output 
34 |   -> Chain len Vect Modification (x :: input) (x :: output) 
35 | extend {input = output, output, x} Same = Same
36 | extend {input} {output = (insertAt idx it _)} {x} (Apply prev (Insert idx it)) = 
37 |   let prev' = extend prev
38 |   in Apply prev' (Insert (FS idx) it)
39 | extend {input} {output = (deleteAt idx intermediate)} {x} (Apply prev (Delete idx)) = 
40 |   let prev' = extend prev
41 |   in 
42 |     Apply prev' $
43 |       rewrite deletePrf {intermediate} {idx} {x} in 
44 |       Delete (FS idx)
45 |
46 | insertAll : (output : Vect n item) -> Chain n Vect Modification [] output
47 | insertAll [] = Same
48 | insertAll (x :: xs) = 
49 |   Apply (insertAll xs) (Insert 0 x)
50 |
51 | deleteAll : (input : Vect n item) -> Chain n Vect Modification input []
52 | deleteAll [] = Same
53 | deleteAll (x :: xs) = Apply (extend (deleteAll xs)) (Delete 0)
54 |
55 | export
56 | naive : {n,m : _} -> DecEq item => (input : Vect n item) -> (output : Vect m item)
57 |   -> (len ** Chain len Vect Modification input output)
58 | naive [] [] = (_ ** Same)
59 | naive [] (o :: os) = (_ ** insertAll (o :: os))
60 | naive (i :: is) [] = (_ ** deleteAll (i :: is))
61 | naive (i :: is) (o :: os) = 
62 |   case decEq i o of
63 |     Yes Refl => 
64 |       let (_ ** rest) = naive is os
65 |       in (_ ** extend rest)
66 |     No _ => 
67 |       let (_ ** rest) = naive is os
68 |           rest = extend {x = i} rest
69 |       in (_ ** Apply (Apply rest (Delete 0)) (Insert 0 o))
70 |