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