aboutsummaryrefslogtreecommitdiff
path: root/LeanAStar
diff options
context:
space:
mode:
authorAndreas Grois <andi@grois.info>2025-01-11 23:39:24 +0100
committerAndreas Grois <andi@grois.info>2025-01-11 23:39:24 +0100
commit0f1e30d0ab59a518c52eb64b0042eec4d212ef2f (patch)
tree8dbb76e368050500c00ea0db21c2c48b570b1bce /LeanAStar
parentbf12dcd38698d9e7fd0396722d7dd75ea1cefc88 (diff)
Add simple unit test (and fix path output, as discovered by test)
Diffstat (limited to 'LeanAStar')
-rw-r--r--LeanAStar/Basic.lean14
1 files changed, 7 insertions, 7 deletions
diff --git a/LeanAStar/Basic.lean b/LeanAStar/Basic.lean
index ba1cc33..a2920f1 100644
--- a/LeanAStar/Basic.lean
+++ b/LeanAStar/Basic.lean
@@ -85,7 +85,7 @@ structure StartPoint (α : Type u) [AStarNode α Costs] where
initial_costs : Costs
protected structure PathFindCosts (α : Type u) [AStarNode α Costs] where
- previousNodes : List α
+ pathUpToHere : List α
actualCosts : Costs
protected structure PathFindCostsAdapter (α : Type u) [AStarNode α Costs] where
@@ -114,15 +114,15 @@ protected instance {α : Type u} [AStarNode α Costs] : AStarNode (LeanAStar.Pat
costsLe := λa b ↦ AStarNode.costsLe α a.actualCosts b.actualCosts
costs_order := ⟨λa b c ↦ AStarNode.costs_order.left a.actualCosts b.actualCosts c.actualCosts, λa b ↦ AStarNode.costs_order.right a.actualCosts b.actualCosts⟩
getNeighbours := λx ↦
- (AStarNode.getNeighbours x.node).map λ(node, actualCosts) ↦ ({node},{previousNodes := [x.node], actualCosts})
+ (AStarNode.getNeighbours x.node).map λ(node, actualCosts) ↦ ({node},{pathUpToHere := [node], actualCosts})
isGoal := AStarNode.isGoal ∘ PathFindCostsAdapter.node
remaining_costs_heuristic := λx ↦
- {previousNodes := [x.node], actualCosts := AStarNode.remaining_costs_heuristic x.node}
+ {pathUpToHere := [], actualCosts := AStarNode.remaining_costs_heuristic x.node}
protected instance {α : Type u} [AStarNode α Costs] [Add Costs] : Add (LeanAStar.PathFindCosts α) where
add := λa b ↦
{
- previousNodes := b.previousNodes ++ a.previousNodes
+ pathUpToHere := b.pathUpToHere ++ a.pathUpToHere
actualCosts := a.actualCosts + b.actualCosts
}
@@ -151,10 +151,10 @@ def findShortestPath {α : Type u} [AStarNode α Costs] [Add Costs] [LawfulBEq Î
{
start := {node := start}
initial_costs := {
- previousNodes := [start]
+ pathUpToHere := [start]
actualCosts := initial_costs
}
}
let i := findLowestCosts starts
- i.map λ{previousNodes, actualCosts} ↦
- (actualCosts, previousNodes)
+ i.map λ{pathUpToHere, actualCosts} ↦
+ (actualCosts, pathUpToHere.reverse)