Last active
November 23, 2019 13:22
-
-
Save derekelkins/d32af329b6e44ed814de6d6589534fd6 to your computer and use it in GitHub Desktop.
A LolliMon (https://github.com/clf/lollimon) implementation of an Euler path calculator.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
maybe : type -> type. | |
nothing : maybe T. | |
just : T -> maybe T. | |
node : type. | |
edge : int -> node -> node -> o. | |
untraversed_edge : int -> node -> node -> o. | |
unvisited_node : node -> o. | |
a : node. | |
b : node. | |
c : node. | |
d : node. | |
#linear unvisited_node a. | |
#linear unvisited_node b. | |
#linear unvisited_node c. | |
#linear unvisited_node d. | |
(* Example 1 - Output of #query 4 4 1 (euler_path Edges): | |
[Edges := 5 :: 6 :: 4 :: 2 :: 1 :: 3 :: nil] | |
[Edges := 1 :: 3 :: 5 :: 6 :: 4 :: 2 :: nil] | |
[Edges := 3 :: 5 :: 6 :: 4 :: 2 :: 1 :: nil] | |
[Edges := 6 :: 4 :: 2 :: 1 :: 3 :: 5 :: nil] *) | |
edge 1 a b. | |
edge 2 b a. | |
edge 3 b c. | |
edge 4 c b. | |
edge 5 c d. | |
edge 6 d c. | |
#linear untraversed_edge 1 a b. | |
#linear untraversed_edge 2 b a. | |
#linear untraversed_edge 3 b c. | |
#linear untraversed_edge 4 c b. | |
#linear untraversed_edge 5 c d. | |
#linear untraversed_edge 6 d c. | |
(* Example 2 - Output of #query 2 1 1 (euler_path Edges): [Edges := 1 :: 2 :: 3 :: 4 :: nil] *) | |
(* | |
edge 1 a b. | |
edge 2 b c. | |
edge 3 c d. | |
edge 4 d c. | |
#linear untraversed_edge 1 a b. | |
#linear untraversed_edge 2 b c. | |
#linear untraversed_edge 3 c d. | |
#linear untraversed_edge 4 d c. | |
*) | |
start_edge : int -> o. | |
connection : int -> int -> o. | |
incident_edge : int -> node -> int -> o. | |
euler_path : list int -> o. | |
euler_step : int -> node -> maybe int -> list int -> o. | |
euler_prestep : int -> node -> maybe int -> list int -> o. | |
consume_connections : int -> list int -> o. | |
euler_path Edges | |
o- unvisited_node Start | |
o- once (untraversed_edge Id Start Next) | |
o- (unvisited_node Start -@ start_edge Id -o once (euler_prestep Id Next nothing Edges)). | |
euler_path nil o- unvisited_node Start. | |
euler_prestep PrevId Node MaybeNext Edges | |
o- unvisited_node Node | |
o- ((pi Id \ pi End \ (incident_edge Id End PrevId o- untraversed_edge Id Node End)) | |
=> once (euler_step PrevId Node MaybeNext Edges)). | |
euler_prestep PrevId Node MaybeNext Edges | |
o- once (euler_step PrevId Node MaybeNext Edges). | |
euler_step PrevId Node MaybeNext Edges | |
o- once (untraversed_edge Id Node Next) | |
o- (connection PrevId Id -o once (euler_prestep Id Next MaybeNext Edges)). | |
euler_step OldPrevId Node nothing Edges | |
o- once (incident_edge Id Next PrevId) | |
o- connection PrevId NextId | |
o- (connection PrevId Id -o once (euler_prestep Id Next (just NextId) Edges)). | |
euler_step OldPrevId Node (just OldNextId) Edges | |
o- once (incident_edge Id Next PrevId) | |
o- connection PrevId NextId | |
o- (connection OldPrevId OldNextId -o connection PrevId Id -o once (euler_prestep Id Next (just NextId) Edges)). | |
euler_step PrevId Node nothing Edges | |
(* Would like to have a "not (untraversed_edge Id Start End)" here. Could use a counter... *) | |
o- start_edge StartId | |
o- consume_connections StartId Edges. | |
euler_step PrevId Node (just NextId) Edges | |
(* Would like to have a "not (untraversed_edge Id Start End)" here. Could use a counter... *) | |
o- start_edge StartId | |
o- (connection PrevId NextId -o consume_connections StartId Edges). | |
consume_connections Id (Id :: Edges) | |
o- connection Id NextId | |
o- consume_connections NextId Edges. | |
consume_connections Id (Id :: nil) o- one. | |
#query 2 1 1 (euler_path Edges). |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment