(* minimal-edits.ml *)
(* a list xs : 'a list is a PREFIX of a list ys : 'a list iff
there is a list zs : 'a list such that ys = xs @ zs
a list xs : 'a list is a PROPER PREFIX of a list ys : 'a list iff
xs is a prefix of ys and xs <> ys
a list xs : 'a list is a PERMUTATION of a list ys : 'a list iff for
all z : 'a, z appears the same number of times in xs as in ys *)
(* val prefix : 'a list * 'a list -> bool
only used in specifications
prefix(xs, ys) tests whether there is an 'a list zs such that
ys = xs @ zs *)
let rec prefix(xs, ys) =
match (xs, ys) with
([], _) -> true
| (_, []) -> false
| (x :: xs, y :: ys) -> x = y && prefix(xs, ys)
(* multisets
values of type 'a multiset are 'a list's whose elements are listed
in ascending order (so they may have duplicates) *)
type 'a multiset = 'a list
(* val listToMultiset : 'a list -> 'a multiset
listToMultiset xs returns a multiset that is a permutation of
xs *)
let listToMultiset xs : 'a multiset = List.sort compare xs
(* val memberMultiset : 'a * 'a multiset -> bool
memberMultiset(x, ys) tests whether x appears in ys *)
let memberMultiset((x, ys) : 'a * 'a multiset) =
(* val mem : 'a multiset -> bool
mem ys tests whether x appears in ys *)
let rec mem ys =
match ys with
[] -> false
| y :: ys ->
match compare x y with
-1 -> false
| 0 -> true
| _ -> mem ys
in mem ys
(* val submultiset : 'a multiset * 'a multiset -> bool
only used in specifications
submultiset(xs, ys) checks whether xs is a prefix of some
permutation of ys
termination: the sum of the lengths of the arguments goes down
at each recursive call *)
let rec submultiset((xs, ys) : 'a multiset * 'a multiset) =
match (xs, ys) with
([], _) -> true
| (_, []) -> false
| (u :: us, v :: vs) ->
match compare u v with
-1 -> false
| 0 -> submultiset(us, vs)
| _ -> submultiset(xs, vs)
(* val insertMultiset : 'a * 'a multiset -> 'a multiset
insertMultiset(x, ys) returns the multiset that is a permutation of
x :: ys *)
let insertMultiset((x, ys) : 'a * 'a multiset) : 'a multiset =
(* val ins : 'a multiset -> 'a multiset
ins ys returns the multiset that is a permutation of
x :: ys *)
let rec ins ys =
match ys with
[] -> [x]
| y :: ys as zs ->
if x <= y
then x :: zs
else y :: ins ys
in ins ys
(* val unionMultiset : 'a multiset * 'a multiset -> 'a multiset
only used in specifications
unionMultiset(xs, ys) returns the multiset that is a permutation
of xs @ ys
termination: the sum of the lengths of the arguments goes down
at each recursive call *)
let rec unionMultiset((xs, ys) : 'a multiset * 'a multiset) =
match (xs, ys) with
([], ys) -> ys
| (xs, []) -> xs
| (u :: us, v :: vs) ->
match compare u v with
-1 -> u :: unionMultiset(us, ys)
| 0 -> u :: v :: unionMultiset(us, vs)
| _ -> v :: unionMultiset(xs, vs)
(* val intersectMultiset : 'a multiset * 'a multiset -> 'a multiset
only used in specifications
intersectMultiset(xs, ys) returns the longest 'a multiset zs such
that zs is a prefix of a permutation of xs, and is a prefix of
a permutation of ys
termination: the sum of the lengths of the arguments goes down
at each recursive call *)
let rec intersectMultiset((xs, ys) : 'a multiset * 'a multiset) : 'a multiset =
match (xs, ys) with
([], _) -> []
| (_, []) -> []
| (u :: us, v :: vs) ->
match compare u v with
-1 -> intersectMultiset(us, ys)
| 0 -> u :: intersectMultiset(us, vs)
| _ -> intersectMultiset(xs, vs)
(* val minusMultiset : 'a multiset * 'a multiset -> 'a multiset
minusMultiset(xs, ys) removes the elements of ys from xs (if an
element of ys isn't in xs, it is ignored; if it appears more
than once in xs, only one instance is removed)
termination: the sum of the lengths of the arguments goes down
at each recursive call *)
let rec minusMultiset((xs, ys) : 'a multiset * 'a multiset) =
match (xs, ys) with
([], _) -> []
| (xs, []) -> xs
| (u :: us, v :: vs) ->
match compare u v with
-1 -> u :: minusMultiset(us, ys)
| 0 -> minusMultiset(us, vs)
| _ -> minusMultiset(xs, vs)
(* val fold : 'a list * ('a * 'b -> 'b) * 'b -> 'b
only used in specifications
fold([x1; x2; ...; x(n-1); xn], f, y) returns
f(x1, f(x2, ... f(x(n-1), f(xn, y)))); in particular,
fold([], f, y) = y *)
let rec fold(xs, f, y) =
match xs with
[] -> y
| x :: xs -> f(x, fold(xs, f, y))
(* val additionsEdit : 'a edit -> 'a multiset
only used in specifications *)
let additionsEdit edit : 'a multiset =
match edit with
Insert(_, x) -> [x]
| Append x -> [x]
| _ -> []
(* val additionsEdits : 'a edit list -> 'a multiset
only used in specifications *)
let rec additionsEdits edits : 'a multiset =
match edits with
[] -> []
| edit :: edits ->
unionMultiset(additionsEdit edit, additionsEdits edits)
(* annotated values and lists *)
type kind = Original | Transposed | New
(* a value of type 'a annot is a value of type 'a,
annotated with its kind *)
type 'a annot = 'a * kind
(* val isOriginal : 'a annot -> bool *)
let isOriginal((_, k) : 'a annot) =
match k with
Original -> true
| _ -> false
(* val isTransposed : 'a annot -> bool *)
let isTransposed((_, k) : 'a annot) =
match k with
Transposed -> true
| _ -> false
(* val isNew : 'a annot -> bool *)
let isNew((_, k) : 'a annot) =
match k with
New -> true
| _ -> false
(* val isOriginalOrTransposed : 'a annot -> bool *)
let isOriginalOrTransposed((_, k) : 'a annot) =
match k with
Original -> true
| Transposed -> true
| _ -> false
(* val transposed : 'a annot -> 'a annot *)
let transposed((x, _) : 'a annot) : 'a annot = (x, Transposed)
(* val listToAnnotList : 'a list -> 'a annot list *)
let listToAnnotList xs : 'a annot list =
List.map (function x -> (x, Original)) xs
(* val annotListToList : 'a annot list -> 'a list *)
let annotListToList(xs : 'a annot list) =
List.map (function (x, _) -> x) xs
(* val transposeAnnot : int -> 'a annot list -> 'a annot list
if 0 <= n <= List.length xs - 2 and isOriginalOrTransposed(List.nth
xs n) and isOriginalOrTransposed(List.nth xs (n + 1)), then
transposeAnnot n xs is the list ys that is identical to xs except
that List.nth ys n = transposed(List.nth xs (n + 1)) and List.nth
ys (n + 1) = transposed(List.nth xs n)
if it is not the case that 0 <= n <= List.length xs - 2 and
isOriginalOrTransposed(List.nth xs n) and
isOriginalOrTransposed(List.nth xs (n + 1)), then transposeAnnot n
xs raises Error
thus: if transposeAnnot n xs does not raise Error,
then annotListToList(transposeAnnot n xs) = transpose n
(annotListToList xs) *)
let transposeAnnot n xs =
(* val trans : int * 'a annot list * 'a annot list -> 'a annot list
if n >= 0, then:
if n <= List.length xs - 2 and
isOriginalOrTransposed(List.nth xs n) and
isOriginalOrTransposed(List.nth xs (n + 1)), then trans(n,
ys, xs) = List.rev_append ys zs, where zs is identical to xs
except that List.nth zs n = transposed(List.nth xs (n +
1)) and List.nth zs (n + 1) = transposed(List.nth xs n)
if it is not the case that n <= List.length xs - 2 and
isOriginalOrTransposed(List.nth xs n) and
isOriginalOrTransposed(List.nth xs (n + 1)), then trans(n,
ys, xs) raises Error *)
let rec trans(n, ys, xs) =
match xs with
[] -> raise Error
| [_] -> raise Error
| x1 :: (x2 :: xs as x2_xs) ->
if n = 0
then if isOriginalOrTransposed x1 &&
isOriginalOrTransposed x2
then List.rev_append
ys
(transposed x2 :: transposed x1 :: xs)
else raise Error
else trans(n - 1, x1 :: ys, x2_xs)
in if n < 0 then raise Error else trans(n, [], xs)
(* val insertAnnot : int * 'a -> 'a annot list -> 'a annot list
if 0 <= n <= List.length xs - 1, then insertAnnot (n, z) xs
is us @ [(z, New)] @ vs, where us is the first n elements of
xs, and vs is the remaining elements of xs
if it's not the case that 0 <= n <= List.length xs - 1, then
insertAnnot (n, z) xs raises Error
thus: if insertAnnot (n, z) xs doesn't raise Error, then
annotListToList(insertAnnot (n, z) xs) =
insert (n, z) (annotListToList xs) *)
let insertAnnot (n, z) (xs : 'a annot list) = insert (n, (z, New)) xs
(* val appendAnnot : 'a -> 'a annot list -> 'a annot list
appendAnnot y xs returns xs @ [(y, New)]
thus: annotListToList(appendAnnot y xs) =
append y (annotListToList xs) *)
let appendAnnot y xs : 'a annot list = xs @ [(y, New)]
(* val deleteAnnot : int -> 'a annot list -> 'a annot list
if 0 <= n <= List.length xs - 1 and isOriginal(List.nth xs n),
then deleteAnnot n xs is the list ys that is identical to xs
except that its n'th (counting from 0) element has been removed
if it is not the case that 0 <= n <= List.length xs - 1 and
isOriginal(List.nth xs n), then deleteAnnot n xs raises Error
thus: if deleteAnnot n xs does not raise Error,
then annotListToList(deleteAnnot n xs) = delete n
(annotListToList xs) *)
let deleteAnnot n xs =
(* val del : int * 'a annot list * 'a annot list -> 'a annot list
if n >= 0, then:
if n <= List.length xs - 1 and isOriginal(List.nth xs n),
then del(n, ys, xs) = List.rev_append ys zs, where the list
zs is identical to xs except that its n'th (counting from 0)
element has been removed
if it is not the case that n <= List.length xs - 1 and
isOriginal(List.nth xs n) then del(n, ys, xs) raises Error *)
let rec del(n, ys, xs) =
match xs with
[] -> raise Error
| x :: xs ->
if n = 0
then if isOriginal x
then List.rev_append ys xs
else raise Error
else del(n - 1, x :: ys, xs)
in if n < 0 then raise Error else del(n, [], xs)
(* val doEditAnnot : 'a edit * 'a annot list -> 'a annot list
we have that: if doEditAnnot(edit, xs) does not raise Error,
then annotListToList(doEditAnnot(edit, xs)) =
doEdit(edit, annotListToList xs) *)
let doEditAnnot(edit, xs) =
match edit with
Transpose n -> transposeAnnot n xs
| Insert(n, z) -> insertAnnot (n, z) xs
| Append y -> appendAnnot y xs
| Delete n -> deleteAnnot n xs
(* val doEditsAnnot : 'a edit list * 'a annot list -> 'a annot list
we have that: if doEditsAnnot(edits, xs) does not raise Error, then
annotListToList(doEditsAnnot(edits, xs)) = doEdits(edits,
annotListToList xs) *)
let rec doEditsAnnot(edits, xs) =
match edits with
[] -> xs
| edit :: edits -> doEditsAnnot(edits, doEditAnnot(edit, xs))
(* NEW LEMMA:
for all xs : 'a list and edits : 'a edit list, if
doEditsAnnot(edits, listToAnnotList xs) doesn't raise Error, then
submultiset
(List.map (function x -> (x, New)) (additionsEdits edits),
doEditsAnnot(edits, listToAnnotList xs))
this is since, with doEditsAnnot, once something is inserted
or appended, it can't be deleted or transposed *)
(* ADDITIONS LEMMA:
for all xs, ys : 'a list and edits : 'a edit list, if
annotListToList(doEditsAnnot(edits, listToAnnotList xs)) = ys,
then submultiset(additionsEdits edits, listToMultiset ys) *)
(* FUNDAMENTAL LEMMA FOR ANNOTATED LISTS:
for all xs : 'a list, ys : 'a list, edits : 'a edit list,
if doEdits(edits, xs) = ys but
doEditsAnnot(edits, listToAnnotList xs) raises Error,
then there is an edits' : 'a edit list such that
List.length edits' < List.length edits &&
annotListToList(doEditsAnnot(edits', listToAnnotList xs)) = ys *)
(* a SELECTION of an 'a multiset xs consists of a pair
(x, ys) : 'a selection,
where x is in xs and ys = minusMultiset(xs, [x]) *)
type 'a selection = 'a * 'a multiset
(* val selections: 'a multiset * ('a selection * 'b -> 'b) * 'b -> 'b
selections(xs, f, y) returns fold(zs, f, y), where zs consists
of the selections of xs, listed in order without duplicates *)
let selections((xs, f, y) : 'a multiset * ('a selection * 'b -> 'b) * 'b) =
(* sels : 'a multiset * 'a list * 'b -> 'b
the POSTPENDING of vs : 'a list to (x, us) : 'a * 'a list is
(x, us @ vs) : 'a * 'a list
if xs is sorted in descending order and the elements of ws
are greater-than-or-equal-to the elements of xs, then
sels(ws, xs, y) returns fold(zs, f, y), where zs consists of
the postpending of ws to the selections of List.rev xs whose
left sides don't appear in ws, listed in order without
duplicates
termination: second argument gets shorter *)
let rec sels(ws, xs, y) =
match xs with
[] -> y
| x :: xs ->
if match ws with
[] -> true
| w :: _ -> w > x
then sels(x :: ws, xs, f((x, List.rev_append xs ws), y))
else sels(x :: ws, xs, y)
in sels([], List.rev xs, y)
(* current state of the search process *)
type 'a state =
'a annot list * (* current annotated list *)
'a multiset * (* corresponding may adds *)
'a multiset * (* corresponding must adds *)
'a multiset (* corresponding must dels *)
(* val valid : 'a state -> bool
tests whether a state is "valid" *)
let valid((ws, mayAdds, mustAdds, mustDels) : 'a state) =
submultiset(mustAdds, mayAdds) &&
submultiset(mustDels, listToMultiset(annotListToList ws)) &&
intersectMultiset(mustAdds, mustDels) = []
(* val noProperPrefixSucceeds : 'a edit list * 'a list * 'a list -> bool
only used in specifications
noProperPrefixSucceeds(edits, xs, ys) tests whether there is
no proper prefix edits' of edits such that
annotListToList(doEditsAnnot(edits', listToAnnotList xs)) = ys *)
let noProperPrefixSucceeds(edits, xs, ys) =
(* val noPropPrefSucc : 'a edit list * 'a annot list -> bool
noPropPrefSucc(edits, ws) tests whether there is no proper
prefix edits' of edits such that
annotListToList(doEditsAnnot(edits', ws)) = ys *)
let rec noPropPrefSucc(edits, ws) =
match edits with
[] -> true
| edit :: edits ->
annotListToList ws <> ys &&
match try Some(doEditAnnot(edit, ws))
with _ -> None with
None -> true
| Some ws -> noPropPrefSucc(edits, ws)
in noPropPrefSucc(edits, listToAnnotList xs)
(* val consistent : 'a state * 'a list * 'a list * 'a edit list -> bool
only used in specifications
a consistency relation between a state, a source list, a target list,
and a list of edits *)
let consistent(((ws, mayAdds, mustAdds, mustDels) as state, xs, ys, edits) :
'a state * 'a list * 'a list * 'a edit list) =
valid state &&
submultiset(additionsEdits edits, listToMultiset ys) &&
ws = doEditsAnnot(edits, listToAnnotList xs) &&
mayAdds =
minusMultiset(listToMultiset ys, additionsEdits edits) &&
mustAdds =
minusMultiset(listToMultiset ys,
listToMultiset(annotListToList ws)) &&
mustDels =
minusMultiset(listToMultiset(annotListToList ws),
listToMultiset ys)
(* val success : 'a state * 'a list -> bool
success(state, ys) tests whether the list corresponding to the
annotated list of state is equal to ys *)
let success(((ws, _, _, _), ys) : 'a state * 'a list) =
annotListToList ws = ys
(* val impossible : 'a state * int -> bool
impossible((ws, mayAdds, mustAdds, mustDels), len) always returns
if it returns true, then, for all ys : 'a list such that
mustAdds =
minusMultiset(listToMultiset ys,
listToMultiset(annotListToList ws)) &&
mustDels =
minusMultiset(listToMultiset(annotListToList ws),
listToMultiset ys),
there is no edits : 'a edit list such that
List.length edits <= len &&
annotListToList(doEditsAnnot(edits, ws)) = ys *)
let impossible(((_, _, mustAdds, mustDels), len) : 'a state * int) =
List.length mustAdds + List.length mustDels > len
(* val initialState : 'a list * 'a list -> 'a state
for all xs, ys : 'a list,
consistent(initialState(xs, ys), xs, ys, []) *)
let initialState(xs, ys) : 'a state =
(listToAnnotList xs,
listToMultiset ys,
minusMultiset(listToMultiset ys, listToMultiset xs),
minusMultiset(listToMultiset xs, listToMultiset ys))
(* next choice in search process *)
type 'a choice =
'a edit * (* next edit *)
'a state (* resulting state *)
(* a choice (edit, (vs, mayAdds', mustAdds', mustDels')) : 'a choice
IS VALID FOR
a valid state (us, mayAdds, mustAdds, mustDels) : 'a state
iff:
doEditAnnot(edit, us) = vs &&
submultiset(additionsEdit edit, mayAdds) &&
mayAdds' = minusMultiset(mayAdds, additionsEdit edit) &&
for all ys : 'a list, if
mustAdds =
minusMultiset(listToMultiset ys, listToMultiset(annotListToList us)) &&
mustDels =
minusMultiset(listToMultiset(annotListToList us), listToMultiset ys),
then
mustAdds' =
minusMultiset(listToMultiset ys, listToMultiset(annotListToList vs)) &&
mustDels' =
minusMultiset(listToMultiset(annotListToList vs), listToMultiset ys) *)
(* VALID CHOICE LEMMA 0:
for all state, state1, state2 : 'a state and edit : 'a edit, if
valid state and (edit, state1) and (edit, state2) are both valid
choices for state, then state1 = state2 *)
(* VALID CHOICE LEMMA 1:
for all xs, ys : 'a list, edit : 'a edit, edits : 'a edit list,
state, state' : 'a state, if consistent(state, xs, ys, edits) and
(edit, state') is a valid choice for state, then consistent(state',
xs, ys, edits @ [edit]) *)
(* VALID CHOICE LEMMA 2:
for all xs, ys : 'a list, editsPref, edits : 'a edit list and
state : 'a state,
if
consistent(state, xs, ys, editsPref) &&
prefix(editsPref, edits) &&
annotListToList(doEditsAnnot(edits, listToAnnotList xs)) = ys,
then either
edits = editsPref or
there are edit : 'a edit, edits' : 'a edit list and
state' : 'a state such that
edits = editsPref @ [edit] @ edits' &&
(edit, state') is a valid choice for state *)
(* val transposes : 'a state * ('a choice * 'b -> 'b) * 'b -> 'b
if valid state, then transposes(state, f, ans) returns fold(zs, f,
ans), where zs consists of the choices with edit constructor
Transpose that are valid for state, listed in order without
duplicates *)
let transposes(((ws, mayAdds, mustAdds, mustDels), f, ans) :
'a state * ('a choice * 'b -> 'b) * 'b) =
let len = List.length ws in
(* val trs : int * 'a annot list * 'b -> 'b
if -1 <= n <= len - 2 and ys is the reversal of the first n +
2 elements of ws, then trs(n, ys, ans) returns fold(zs, f,
ans), where zs consists of the choices whose edits have the
form Transpose i, for i <= n, that are valid for (ws,
mayAdds, mustAdds, mustDels), listed in order without
duplicates
termination: first argument gets smaller *)
let rec trs(n, ys, ans) =
if n < 0
then ans
else match ys with
y1 :: (y2 :: _ as ys) ->
if isOriginalOrTransposed y1 &&
isOriginalOrTransposed y2
then let edit = Transpose n
in trs(n - 1, ys,
f((edit,
(doEditAnnot(edit, ws), mayAdds,
mustAdds, mustDels)),
ans))
else trs(n - 1, ys, ans)
| _ -> raise Error (* cannot happen *)
in if len < 2
then ans
else trs(len - 2, List.rev ws, ans)
(* val inserts : 'a state * ('a choice * 'b -> 'b) * 'b -> 'b
if valid state, then inserts(state, f, ans) returns fold(zs, f,
ans), where zs consists of the choices with edit constructor Insert
that are valid for state, listed in order without duplicates *)
let inserts(((ws, mayAdds, mustAdds, mustDels), f, ans) :
'a state * ('a choice * 'b -> 'b) * 'b) =
let len = List.length ws in
(* val insers : int * 'b -> 'b
if -1 <= n <= len - 1, then insers(n, ans) returns fold(zs,
f, ans), where zs consists of the choices whose edits
elements have the form Insert(i, _), for i <= n, that are
valid for (ws, mayAdds, mustAdds, mustDels), listed in order
without duplicates
termination: first argument gets smaller *)
let rec insers(n, ans) =
if n < 0
then ans
else insers
(n - 1,
selections
(mayAdds,
(function ((y, mayAdds), ans) ->
let edit = Insert(n, y) in
let (mustAdds, mustDels) =
if memberMultiset(y, mustAdds)
then (minusMultiset(mustAdds, [y]),
mustDels)
else (mustAdds,
insertMultiset(y, mustDels))
in f((edit,
(doEditAnnot(edit, ws), mayAdds,
mustAdds, mustDels)),
ans)),
ans))
in if len < 1
then ans
else insers(len - 1, ans)
(* val appends : 'a state * ('a choice * 'b -> 'b) * 'b -> 'b
if valid state, then appends(state, f, ans) returns fold(zs, f,
ans), where zs consists of the choices with edit constructor Append
that are valid for state, listed in order without duplicates *)
let appends(((ws, mayAdds, mustAdds, mustDels), f, ans) :
'a state * ('a choice * 'b -> 'b) * 'b) =
selections(mayAdds,
(function ((y, mayAdds), ans) ->
let (mustAdds, mustDels) =
if memberMultiset(y, mustAdds)
then (minusMultiset(mustAdds, [y]),
mustDels)
else (mustAdds,
insertMultiset(y, mustDels))
in f((Append y,
(doEditAnnot(Append y, ws), mayAdds,
mustAdds, mustDels)),
ans)),
ans)
(* val deletes : 'a state * ('a choice * 'b -> 'b) * 'b -> 'b
if valid state, then deletes(state, f, ans) returns fold(zs, f,
ans), where zs consists of the choices with edit constructor Delete
that are valid for state, listed in order without duplicates *)
let deletes(((ws, mayAdds, mustAdds, mustDels), f, ans) :
'a state * ('a choice * 'b -> 'b) * 'b) =
let len = List.length ws in
(* val dels : int * 'b -> 'b
if -1 <= n <= len - 1 and ys is the reversal of the first n +
1 elements of ws, then dels(n, ys, ans) returns fold(zs, f,
ans), where zs consists of the choices whose edits have the
form Delete i, for i <= n, that are valid for (ws, mayAdds,
mustAdds, mustDels), listed in order without duplicates
termination: first argument gets smaller *)
let rec dels(n, ys, ans) =
if n < 0
then ans
else match ys with
(y, Original) :: ys ->
let edit = Delete n in
let (mustAdds, mustDels) =
if memberMultiset(y, mustDels)
then (mustAdds, minusMultiset(mustDels, [y]))
else (insertMultiset(y, mustAdds), mustDels)
in dels(n - 1, ys,
f((edit,
(doEdit(edit, ws), mayAdds, mustAdds,
mustDels)),
ans))
| _ :: ys -> dels(n - 1, ys, ans)
| _ -> raise Error (* cannot happen *)
in if len < 1
then ans
else dels(len - 1, List.rev ws, ans)
(* val choices : 'a state * ('a choice * 'b -> 'b) * 'b -> 'b
if valid state, then choices(state, f, ans) returns fold(zs, f,
ans), where zs consists of the choices that are valid for state,
listed in order without duplicates *)
let choices(state, f, ans) =
transposes(state, f,
inserts(state, f,
appends(state, f,
deletes(state, f,
ans))))
(* val boundedFind : int * 'a list * 'a list -> 'a edit list list
if bound >= 0, then boundedFind(bound, xs, ys) returns the list
of all edits : 'a edit list such that
annotListToList(doEditsAnnot(edits, listToAnnotList xs)) = ys
List.length edits <= bound &&
noProperPrefixSucceeds(edits, xs, ys),
listed in strictly ascending order *)
let boundedFind(bound, xs, ys) =
(* val find :
'a edit list * int * 'a state * 'a edit list list ->
'a edit list list
if
len <= bound &&
len = List.length editsRev &&
noProperPrefixSucceeds(List.rev editsRev, xs, ys) &&
consistent(state, xs, ys, List.rev editsRev),
then
find(editsRev, len, state, ans) returns ans' @ ans,
where ans' is the list of all edit-lists edits such that
prefix(List.rev editsRev, edits) &&
annotListToList(doEditsAnnot(edits, listToAnnotList xs)) = ys &&
List.length edits <= bound &&
noProperPrefixSucceeds(edits, xs, ys),
listed in strictly ascending order
termination: at each recursive call, made via
choices, second argument becomes one larger, and
so closer to being equal-to bound *)
let rec find(editsRev, len, state, ans) =
if impossible(state, bound - len)
then ans
else if success(state, ys)
then List.rev editsRev :: ans
else if len = bound
then ans
else choices
(state,
(function ((edit, state), ans) ->
find(edit :: editsRev, len + 1, state, ans)),
ans)
in find([], 0, initialState(xs, ys), [])
(* val minimalEdits : 'a list * 'a list -> 'a edit list list
minimalEdits(xs, ys) returns the list of all minimal edit-lists taking
xs to ys, listed in strictly ascending order *)
let minimalEdits(xs, ys) =
(* val loop : int -> 'a edit list list
if n >= 0 and there is no edits : 'a edit list such that
List.length edits < n and doEdits(edits, xs) = ys, then loop
n returns the list of all minimal edit-lists taking xs to ys,
listed in strictly ascending order
terminates at List.length xs + List.length ys or earlier *)
let rec loop n =
match boundedFind(n, xs, ys) with
[] -> loop(n + 1)
| mins -> mins
in loop 0