Use a list of <goal>s instead of a set

kframework / matching-logic-prover

15 stars 4 forks source link

Use a list of <goal>s instead of a set #59

Closed nishantjr closed 4 years ago

nishantjr commented 4 years ago

This has two advantages:

It is more efficient, since when executing a strategy rules only try matching on the first goal, and not all the goals in the goal cell
When functions use local-contexts we no longer need to specify a goalId

nishantjr commented 4 years ago

Since the k cell is merged with the the claim cell, $PGM is part of an initial goal. Multiple claims are dispatched as subgoals one at a time with the first one being proved first.