模块 Diffing_with_keys

module Diffing_with_keys: sig .. end

当对每个元素都有唯一键的列表进行差异比较时，我们可以通过引入两个复合编辑操作来细化差异补丁：交换和移动。

Swap 交换两个元素的位置。 Swap 的成本设置为 2 * change - epsilon。 Move 改变一个元素的位置。 Move 的成本设置为 delete + addition - epsilon。

当成本 delete + addition 大于 change 并且具有这些特定的权重时，可以使用 Swap 和 Move 的最佳补丁直接且廉价地从原始最佳补丁计算得出。

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;


}

此更改的专门版本引入了两个复合更改：Move 和 Swap

val prefix : Format.formatter -> ('l, 'r, 'diff) change -> unit

module Define: functor (D : Diffing.Defs  with type eq := unit) -> sig .. end