0 | module Text.Show.Diff

  2 | import Data.Vect

  3 | import Derive.Prelude

  4 | import public Text.Show.Pretty

  6 | %language ElabReflection

  8 | %default total

 14 | public export

 15 | data ValueDiff : Type where

 16 |   Con    : VName -> List ValueDiff -> ValueDiff

 17 |   Rec    : VName -> List (VName, ValueDiff) -> ValueDiff

 18 |   Tuple  : ValueDiff -> ValueDiff -> List ValueDiff -> ValueDiff

 19 |   Lst    : List ValueDiff -> ValueDiff

 20 |   Same   : Value -> ValueDiff

 21 |   Diff   : Value -> Value -> ValueDiff

 23 | %runElab derive "ValueDiff" [Show,Eq,PrettyVal]

 25 | public export

 26 | data LineDiff : Type where

 27 |   LineSame    : String -> LineDiff

 28 |   LineRemoved : String -> LineDiff

 29 |   LineAdded   : String -> LineDiff

 31 | %runElab derive "LineDiff" [Show,Eq,PrettyVal]

 33 | public export

 34 | data DocDiff : Type where

 35 |   DocSame    : Nat -> String -> DocDiff

 36 |   DocRemoved : Nat -> String -> DocDiff

 37 |   DocAdded   : Nat -> String -> DocDiff

 38 |   DocOpen    : Nat -> String -> DocDiff

 39 |   DocItem    : Nat -> String -> List DocDiff -> DocDiff

 40 |   DocClose   : Nat -> String -> DocDiff

 42 | %runElab derive "DocDiff" [Show,Eq,PrettyVal]

 49 | valueDiff : Value -> Value -> ValueDiff

 51 | zipDiff :

 52 |      SnocList ValueDiff

 53 |   -> List Value

 54 |   -> List Value

 55 |   -> Maybe (List ValueDiff)

 56 | zipDiff sx [] [] = Just $ sx <>> []

 57 | zipDiff sx (x :: xs) (y :: ys) = zipDiff (sx :< valueDiff x y) xs ys

 58 | zipDiff _ _ _ = Nothing

 60 | zipDiffP :

 61 |      SnocList (VName, ValueDiff)

 62 |   -> List (VName, Value)

 63 |   -> List (VName, Value)

 64 |   -> Maybe (List (VName, ValueDiff))

 65 | zipDiffP sx [] [] = Just $ sx <>> []

 66 | zipDiffP sx ((n1,x) :: xs) ((n2,y) :: ys) =

 67 |   if n1 == n2 then zipDiffP (sx :< (n1, valueDiff x y)) xs ys else Nothing

 68 | zipDiffP _ _ _ = Nothing

 70 | valueDiff x@(Con nx xs) y@(Con ny ys) =

 71 |     if nx == ny

 72 |        then maybe (Diff x y) (Con ny) (zipDiff [<] xs ys)

 73 |        else Diff x y

 74 | valueDiff x@(Rec nx xs) y@(Rec ny ys) =

 75 |     if nx == ny

 76 |        then maybe (Diff x y) (Rec ny) (zipDiffP [<] xs ys)

 77 |        else Diff x y

 78 | valueDiff x@(Lst xs) y@(Lst ys) = maybe (Diff x y) Lst (zipDiff [<] xs ys)

 79 | valueDiff x@(Tuple x1 x2 xs) y@(Tuple y1 y2 ys) = case zipDiff [<] xs ys of

 80 |   Nothing => Diff x y

 81 |   Just ds => Tuple (valueDiff x1 y1) (valueDiff x2 y2) ds

 82 | valueDiff x y = if x == y then Same x else Diff x y

 84 | take : (f : Value -> Value -> Value) -> ValueDiff -> Value

 85 | take f v = case v of

 86 |   Con x xs     => Con x $ ts xs

 87 |   Rec x xs     => Rec x $ tsP xs

 88 |   Tuple x y xs => Tuple (take f x) (take f y) (ts xs)

 89 |   Lst xs       => Lst $ ts xs

 90 |   Same x       => x

 91 |   Diff x y     => f x y

 93 |   where

 94 |     ts : List ValueDiff -> List Value

 95 |     ts []       = []

 96 |     ts (h :: t) = take f h :: ts t

 98 |     tsP : List (a,ValueDiff) -> List (a,Value)

 99 |     tsP []           = []

100 |     tsP ((a,h) :: t) = (a,take f h) :: tsP t

103 | takeLeft : ValueDiff -> Value

104 | takeLeft = take $ \x,_ => x

107 | takeRight : ValueDiff -> Value

108 | takeRight = take $ \_,y => y

110 | oneLiner : Value -> Bool

111 | oneLiner x =

112 |   case lines (valToStr x) of

113 |      _ :: Nil   => True

114 |      _          => False

116 | removed : (indent: Nat) -> String -> List DocDiff

117 | removed ind = map (DocRemoved ind) . lines

119 | added : (indent: Nat) -> String -> List DocDiff

120 | added ind = map (DocAdded ind) . lines

122 | same : (indent: Nat) -> String -> List DocDiff

123 | same ind = map (DocSame ind) . lines

125 | sameN : (indent: Nat) -> VName -> SnocList DocDiff

126 | sameN ind = ([<] <><) . same ind . unName

128 | remAdd : (indent : Nat) -> Value -> Value -> List DocDiff

129 | remAdd ind x y = removed ind (valToStr x) ++ added ind (valToStr y)

131 | oneLine : Nat -> ValueDiff -> Lazy (List DocDiff) -> List DocDiff

132 | oneLine ind v dds =

133 |   let x = takeLeft v

134 |       y = takeRight v

135 |    in if oneLiner x && oneLiner y then remAdd ind x y else dds

137 | docDiff : (indent : Nat) -> ValueDiff -> List DocDiff

139 | docDiffs :

140 |       SnocList DocDiff

141 |    ->(indent : Nat)

142 |    -> List ValueDiff

143 |    -> List DocDiff

144 | docDiffs sx ind (x :: xs) = docDiffs (sx <>< docDiff ind x) ind xs

145 | docDiffs sx ind []        = sx <>> []

147 | docItems :

148 |       SnocList DocDiff

149 |    ->(indent : Nat)

150 |    -> List ValueDiff

151 |    -> SnocList DocDiff

152 | docItems sx ind (x :: xs) =

153 |   docItems (sx :< DocItem ind ", " (docDiff 0 x)) ind xs

154 | docItems sx ind []        = sx

156 | docPairs :

157 |       SnocList DocDiff

158 |    ->(indent : Nat)

159 |    -> List (VName,ValueDiff)

160 |    -> SnocList DocDiff

161 | docPairs sx ind ((n,x) :: xs) =

162 |   let ds := sameN 0 (n <+> " =") <>> docDiff 2 x

163 |    in docPairs (sx :< DocItem ind ", " ds) ind xs

164 | docPairs sx ind []        = sx

166 | docDiff ind (Same x)   = same ind (valToStr x)

167 | docDiff ind (Diff x y) = remAdd ind x y

168 | docDiff ind v@(Con n xs) =

169 |   oneLine ind v $ docDiffs (sameN ind n) (ind + 2) xs

170 | docDiff ind v@(Lst xs) =

171 |   oneLine ind v $ DocOpen ind "[" :: (docItems [<] ind xs <>> [DocClose ind "]"])

172 | docDiff ind v@(Tuple x y xs) =

173 |   oneLine ind v $

174 |     DocOpen ind "(" ::

175 |     DocItem ind ", " (docDiff 0 x) ::

176 |     DocItem ind ", " (docDiff 0 y) ::

177 |     (docItems [<] ind xs <>> [DocClose ind ")"])

178 | docDiff ind v@(Rec n xs) =

179 |   oneLine ind v $

180 |     sameN ind n <>>

181 |     DocOpen ind "{" ::

182 |     (docPairs [<] (ind + 2) xs <>> [DocClose ind "}"])

184 | spaces : Nat -> String

185 | spaces ind = fastPack $ replicate ind ' '

187 | mkLineDiff : (ind : Nat) -> String -> DocDiff -> List LineDiff

189 | mkLineDiffs :

190 |      SnocList LineDiff

191 |   -> (ind : Nat)

192 |   -> List DocDiff

193 |   -> List LineDiff

194 | mkLineDiffs sx ind (x :: xs) =

195 |   mkLineDiffs (sx <>< mkLineDiff ind "" x) ind xs

196 | mkLineDiffs sx ind []        = sx <>> []

198 | mkLineDiff ind0 pre0 diff =

199 |   case diff of

200 |     DocSame i x    => [LineSame $ mkLinePrefix i ++ x]

201 |     DocRemoved i x => [LineRemoved $ mkLinePrefix i ++ x]

202 |     DocAdded i x   => [LineAdded $ mkLinePrefix i ++ x]

203 |     DocOpen i x    => [LineSame $ mkLinePrefix i ++ x]

204 |     DocClose i x   => [LineSame $ spaces (mkLineIndent i) ++ x]

205 |     DocItem _ _ [] => []

206 |     DocItem i p (x@(DocRemoved _ _) :: y@(DocAdded _ _) :: xs) =>

207 |       mkLineDiff (mkLineIndent i) p x ++

208 |       mkLineDiff (mkLineIndent i) p y ++

209 |       mkLineDiffs [<] (mkLineIndent (i + length p)) xs

211 |     DocItem i p (x :: xs) =>

212 |       mkLineDiff (mkLineIndent i) p x ++

213 |       mkLineDiffs [<] (mkLineIndent (i + length p)) xs

215 |   where mkLinePrefix : Nat -> String

216 |         mkLinePrefix ind = spaces ind0 ++ pre0 ++ spaces ind

218 |         mkLineIndent : Nat -> Nat

219 |         mkLineIndent ind = ind0 + length pre0 + ind

221 | collapseOpen : List DocDiff -> List DocDiff

222 | collapseOpen (DocSame ind l :: DocOpen _ bra :: xs) =

223 |   DocSame ind (l ++ " " ++ bra) :: collapseOpen xs

224 | collapseOpen (DocItem ind pre xs :: ys) =

225 |   DocItem ind pre (collapseOpen xs) :: collapseOpen ys

226 | collapseOpen (x :: xs) = x :: collapseOpen xs

227 | collapseOpen [] = []

229 | dropLeadingSep : List DocDiff -> List DocDiff

230 | dropLeadingSep (DocOpen oind bra :: DocItem ind pre xs :: ys) =

231 |      DocOpen oind bra

232 |   :: DocItem (ind + length pre) "" (dropLeadingSep xs)

233 |   :: dropLeadingSep ys

234 | dropLeadingSep (DocItem ind pre xs :: ys) =

235 |   DocItem ind pre (dropLeadingSep xs) :: dropLeadingSep ys

236 | dropLeadingSep (x :: xs) = x :: dropLeadingSep xs

237 | dropLeadingSep [] = []

240 | toLineDiff : ValueDiff -> List LineDiff

241 | toLineDiff v =

242 |   concatMap (mkLineDiff 0 "") .

243 |   collapseOpen .

244 |   dropLeadingSep $

245 |   docDiff 0 v

248 | lineDiff : Value -> Value -> List LineDiff

249 | lineDiff x y = toLineDiff $ valueDiff x y

252 | renderLineDiff : LineDiff -> String

253 | renderLineDiff (LineSame x)    = "  " ++ x

254 | renderLineDiff (LineRemoved x) = "- " ++ x

255 | renderLineDiff (LineAdded x)   = "+ " ++ x

258 | renderValueDiff : ValueDiff -> String

259 | renderValueDiff = unlines . map renderLineDiff . toLineDiff