0 | module Goop.Diff.Algo.Naive

 2 | import Data.Vect

 3 | import Decidable.Equality

 5 | import Goop.Diff.Interface

 7 | %default total

 9 | public export

10 | data Chain : (len : Nat) -> (t : Nat -> Type -> Type)

11 |   -> (m : forall a, b . t a item -> t b item -> Type)

12 |   -> (input : t a' item) -> (output : t b' item) -> Type where

13 |   Same : {m : forall a, b . t a item -> t b item -> Type} -> Chain 0 t m x x

14 |   Apply : {m : forall a, b . t a item -> t b item -> Type} 

15 |     -> (prev : Chain len t m input intermediate) -> (modification : m intermediate output) 

16 |     -> Chain (S len) t m input output

18 | public export

19 | data Modification : Vect n item -> Vect m item -> Type where

20 |   Insert : {0 prev : Vect n item} -> (idx : Fin (S n)) -> (it : item)

21 |     -> Modification prev (insertAt idx it prev)

22 |   Delete : {0 prev : Vect (S n) item} -> (idx : Fin (S n))

23 |     -> Modification prev (deleteAt idx prev)

25 | deletePrf : {idx : _}

26 |   -> (x :: deleteAt idx intermediate) = deleteAt (FS idx) (x :: intermediate) 

27 | deletePrf {idx = FZ} = 

28 |   rewrite lemma intermediate {y = x} in Refl

29 |   where

30 |     lemma : (ys : Vect (S n) item) -> deleteAt (FS FZ) (y :: ys) = y :: deleteAt FZ ys

31 |     lemma (z :: zs) = Refl

32 | deletePrf {idx = (FS y)} = 

33 |   rewrite lemma intermediate {idx = (FS y)} {y = x} in Refl

34 |   where

35 |     lemma : (ys : Vect (S n) item) 

36 |       -> {0 y : item}

37 |       -> deleteAt (FS idx) (y :: ys) = y :: deleteAt idx ys

38 |     lemma (z :: xs) = Refl

40 | extend : {x : item}

41 |   -> Chain len Vect Modification input output 

42 |   -> Chain len Vect Modification (x :: input) (x :: output) 

43 | extend {input = output, output, x} Same = Same

44 | extend {input} {output = (insertAt idx it _)} {x} (Apply prev (Insert idx it)) = 

45 |   let prev' = extend prev

46 |   in Apply prev' (Insert (FS idx) it)

47 | extend {input} {output = (deleteAt idx intermediate)} {x} (Apply prev (Delete idx)) = 

48 |   let prev' = extend prev

49 |   in 

50 |     Apply prev' $

51 |       rewrite deletePrf {intermediate} {idx} {x} in 

52 |       Delete (FS idx)

54 | insertAll : (output : Vect n item) -> Chain n Vect Modification [] output

55 | insertAll [] = Same

56 | insertAll (x :: xs) = 

57 |   Apply (insertAll xs) (Insert 0 x)

59 | deleteAll : (input : Vect n item) -> Chain n Vect Modification input []

60 | deleteAll [] = Same

61 | deleteAll (x :: xs) = Apply (extend (deleteAll xs)) (Delete 0)

64 | naive : {n,m : _} -> DecEq item => (input : Vect n item) -> (output : Vect m item)

65 |   -> (len ** Chain len Vect Modification input output)

66 | naive [] [] = (_ ** Same)

67 | naive [] (o :: os) = (_ ** insertAll (o :: os))

68 | naive (i :: is) [] = (_ ** deleteAll (i :: is))

69 | naive (i :: is) (o :: os) = 

70 |   case decEq i o of

71 |     Yes Refl => 

72 |       let (_ ** rest) = naive is os

73 |       in (_ ** extend rest)

74 |     No _ => 

75 |       let (_ ** rest) = naive is os

76 |           rest = extend {x = i} rest

77 |       in (_ ** Apply (Apply rest (Delete 0)) (Insert 0 o))