plucky (3) Diffing_with_keys.3o.gz

NAME

       Diffing_with_keys  -  When diffing lists where each element has a distinct key, we can refine the diffing
       patch by introducing two composite edit moves: swaps and moves.

Module

       Module   Diffing_with_keys

Documentation

       Module Diffing_with_keys
        : sig end

       When diffing lists where each element has a distinct key, we can refine the diffing patch by  introducing
       two composite edit moves: swaps and moves.

       Swap  s exchange the position of two elements.  Swap cost is set to 2 * change - epsilon .  Move s change
       the position of one element.  Move cost is set to delete + addition - epsilon .

       When the cost delete + addition is greater than change and with those specific weights, the optimal patch
       with Swap s and Move s can be computed directly and cheaply from the original optimal patch.

       type 'a with_pos = {
        pos : int ;
        data : 'a ;
        }

       val with_pos : 'a list -> 'a with_pos list

       type ('l, 'r, 'diff) mismatch =
        | Name of {
        pos : int ;
        got : string ;
        expected : string ;
        types_match : bool ;
        }
        | Type of {
        pos : int ;
        got : 'l ;
        expected : 'r ;
        reason : 'diff ;
        }

       type ('l, 'r, 'diff) change =
        | Change of ('l, 'r, 'diff) mismatch
        | Swap of {
        pos : int * int ;
        first : string ;
        last : string ;
        }
        | Move of {
        name : string ;
        got : int ;
        expected : int ;
        }
        | Insert of {
        pos : int ;
        insert : 'r ;
        }
        | Delete of {
        pos : int ;
        delete : 'l ;
        }

       This specialized version of changes introduces two composite changes: Move and Swap

       val prefix : ('l, 'r, 'diff) change Format_doc.printer

       module Define : (D : sig end) -> sig end