1	import Base
2	import ./Sequence.bend as S
3	import ../EdlibTypes.bend as E
4	import ./Reconstruction.bend as R
5	
6	# Myers owns nonempty distance and location searches. This module builds
7	# ordered results, preserves empty-input returns and validates reconstructed PATH.
8	type Location is Data:
9	  Location{end: E.Coordinate, start: Nat}
10	
11	type Best is Data:
12	  Best{score: U32, locations: List<&2, Location>}
13	
14	def update_best(best: Best, score: U32, location: Location, comparison: Cmp) -> Best:
15	  match best comparison:
16	    case Best{_, _} LT{}:
17	      Best{score, [location]}
18	    case Best{old, locations} EQ{}:
19	      Best{old, location <> locations}
20	    case _ GT{}:
21	      best
22	
23	def ordered(best: Best) -> Best:
24	  match best:
25	    case Best{score, locations}:
26	      Best{score, List.reverse(&2, Location, locations)}
27	
28	def ends(locations: List<&2, Location>) -> List<&2, E.Coordinate>:
29	  match locations:
30	    case Nil{}:
31	      Nil{}
32	    case Location{end, _} <> tail:
33	      end <> ends(tail)
34	
35	def starts(locations: List<&2, Location>) -> List<&2, E.Coordinate>:
36	  match locations:
37	    case Nil{}:
38	      Nil{}
39	    case Location{_, start} <> tail:
40	      E.Position{start} <> starts(tail)
41	
42	def span(target: String, location: Location) -> String:
43	  match location:
44	    case Location{E.BeforeStart{}, _}:
45	      ""
46	    case Location{E.Position{index}, start}:
47	      String.drop(String.take(target, 1n+index), start)
48	
49	def path_result(score: U32, +locations: List<&2, Location>,
50	                +operations: List<&2, E.Operation>, format: E.CigarFormat) -> E.AlignResult:
51	  E.AlignResult{E.Ok{}, E.Found{U32.to_nat(score)}, ends(locations),
52	    Some{starts(locations)}, Some{operations}, Some{E.alignment_to_cigar(operations, format)}}
53	
54	def location_valid(target: String, location: Location) -> Bool:
55	  match location:
56	    case Location{E.BeforeStart{}, start}:
57	      Nat.is_eq(start, 0n)
58	    case Location{E.Position{+end}, start}:
59	      Bool.and(Nat.is_lt(end, S.length(target)), Nat.is_le(start, 1n+end))
60	
61	def path_checked(score: U32, locations: List<&2, Location>, format: E.CigarFormat,
62	                  operations: List<&2, E.Operation>, valid: Bool) -> E.AlignResult:
63	  match valid:
64	    case True{}:
65	      path_result(score, locations, operations, format)
66	    case False{}:
67	      E.AlignResult{E.Error{}, E.NotFound{}, Nil{}, None{}, None{}, None{}}
68	
69	def path_validate(query: String, segment: String, pairs: List<&2, E.EqualityPair>,
70	                   +score: U32, locations: List<&2, Location>, format: E.CigarFormat,
71	                   +operations: List<&2, E.Operation>, valid_location: Bool) -> E.AlignResult:
72	  path_checked(score, locations, format, operations,
73	    Bool.and(valid_location, R.valid_path(query, segment, operations, pairs, U32.to_nat(score))))
74	
75	def path_reconstruct(+query: String, +segment: String, +pairs: List<&2, E.EqualityPair>,
76	                      score: U32, locations: List<&2, Location>, format: E.CigarFormat,
77	                      valid_location: Bool) -> E.AlignResult:
78	  path_validate(query, segment, pairs, score, locations, format,
79	    R.reconstruct(query, segment, pairs), valid_location)
80	
81	def result(query: String, target: String, task: E.Task,
82	           pairs: List<&2, E.EqualityPair>, format: E.CigarFormat,
83	           best: Best, accepted: Bool) -> E.AlignResult:
84	  match task best accepted:
85	    case _ _ False{}:
86	      E.not_found()
87	    case E.Distance{} Best{score, locations} True{}:
88	      E.AlignResult{E.Ok{}, E.Found{U32.to_nat(score)}, ends(locations), None{}, None{}, None{}}
89	    case E.Locations{} Best{score, +locations} True{}:
90	      E.AlignResult{E.Ok{}, E.Found{U32.to_nat(score)}, ends(locations), Some{starts(locations)}, None{}, None{}}
91	    case E.Path{} Best{_, Nil{}} True{}:
92	      E.AlignResult{E.Error{}, E.NotFound{}, Nil{}, None{}, None{}, None{}}
93	    case E.Path{} Best{score, +location <> tail} True{}:
94	      +sequence = target
95	      path_reconstruct(query, span(sequence, location), pairs, score,
96	        location <> tail, format, location_valid(sequence, location))
97	
98	# Pinned Edlib returns before applying k or calculating starts/path on empty
99	# inputs, including PATH. Preserve that observable oracle behavior.
100	def empty_result(query: String, target: String, config: E.AlignConfig) -> E.AlignResult:
101	  match query target config:
102	    case SNil{} +t E.AlignConfig{E.NW{}, _, _, _, _}:
103	      +length = S.length(t)
104	      E.distance_result(length, E.end_coordinate(length), True{})
105	    case SNil{} _ _:
106	      E.distance_result(0n, E.BeforeStart{}, True{})
107	    case SCon{_, qt} SNil{} _:
108	      E.distance_result(1n+S.length(qt), E.BeforeStart{}, True{})
109	    # Internal precondition: Myers calls this only when one input is empty.
110	    case _ _ _:
111	      E.AlignResult{E.Error{}, E.NotFound{}, Nil{}, None{}, None{}, None{}}