# ========================================
# Minigraf: Recursive Rules Demo
# ========================================
# This file demonstrates recursive Datalog rules
# including transitive closure, cycle handling,
# and multi-hop graph reachability.
#
# Run with: cargo run < demos/demo_recursive.txt
# ========================================

# ========================================
# 1. SIMPLE TRANSITIVE CLOSURE
# ========================================
# Create a chain: A -> B -> C -> D

(transact [[:a :connected :b]
           [:b :connected :c]
           [:c :connected :d]])

# Define recursive reachability rules:
# - Base case: directly connected nodes are reachable
# - Recursive case: if X connects to Z, and Z reaches Y, then X reaches Y

(rule [(reach ?x ?y) [?x :connected ?y]])
(rule [(reach ?x ?y) [?x :connected ?z] (reach ?z ?y)])

# Query: What can A reach?
# Expected: B, C, D (all nodes in the chain)
(query [:find ?to :where (reach :a ?to)])

# Query: What can B reach?
# Expected: C, D (nodes after B)
(query [:find ?to :where (reach :b ?to)])

# ========================================
# 2. CYCLE HANDLING
# ========================================
# Create a cycle: X -> Y -> Z -> X
# This tests that the evaluator converges correctly
# without infinite loops

(transact [[:x :link :y]
           [:y :link :z]
           [:z :link :x]])

# Define reachability via links
(rule [(via-link ?from ?to) [?from :link ?to]])
(rule [(via-link ?from ?to) [?from :link ?mid] (via-link ?mid ?to)])

# Query: What can X reach?
# Expected: Y, Z, and X itself (cycle completes back)
# This verifies convergence and cycle detection
(query [:find ?to :where (via-link :x ?to)])

# ========================================
# 3. LONG CHAIN (6 nodes)
# ========================================
# Create a longer chain to demonstrate scalability:
# n1 -> n2 -> n3 -> n4 -> n5 -> n6

(transact [[:n1 :next :n2]
           [:n2 :next :n3]
           [:n3 :next :n4]
           [:n4 :next :n5]
           [:n5 :next :n6]])

# Define sequence reachability
(rule [(seq ?x ?y) [?x :next ?y]])
(rule [(seq ?x ?y) [?x :next ?z] (seq ?z ?y)])

# Query: What can n1 reach?
# Expected: n2, n3, n4, n5, n6 (all 5 nodes ahead)
(query [:find ?to :where (seq :n1 ?to)])

# Query: What can n3 reach?
# Expected: n4, n5, n6 (3 nodes ahead)
(query [:find ?to :where (seq :n3 ?to)])

# ========================================
# 4. ANCESTRY / FAMILY TREE
# ========================================
# Demonstrate hierarchical relationships

(transact [[:alice :parent :bob]
           [:alice :parent :charlie]
           [:bob :parent :diana]
           [:bob :parent :eve]
           [:charlie :parent :frank]])

# Define ancestor relationship (transitive parent)
(rule [(ancestor ?a ?d) [?a :parent ?d]])
(rule [(ancestor ?a ?d) [?a :parent ?p] (ancestor ?p ?d)])

# Query: Who are Alice's descendants?
# Expected: Bob, Charlie (children), Diana, Eve, Frank (grandchildren)
(query [:find ?descendant :where (ancestor :alice ?descendant)])

# Query: Who are Bob's descendants?
# Expected: Diana, Eve (Bob's children)
(query [:find ?descendant :where (ancestor :bob ?descendant)])

# ========================================
# 5. TEMPORAL QUERIES WITH RECURSIVE RULES
# ========================================
# :as-of and :valid-at compose with recursive rules.

# --- tx-time (:as-of) ---
# Build a graph in two transactions:
# tx N:   alpha → beta
# tx N+1: beta → gamma (extends the chain)

(transact [[:alpha :arc :beta]])
(transact [[:beta  :arc :gamma]])

(rule [(path ?a ?b) [?a :arc ?b]])
(rule [(path ?a ?b) [?a :arc ?mid] (path ?mid ?b)])

# Current state: alpha can reach beta and gamma
# Expected: :beta, :gamma
(query [:find ?to :where (path :alpha ?to)])

# As of the first transact (only alpha→beta existed), alpha could only reach beta
# Sections 1–4 issued several transacts; alpha→beta is added as tx 9.
# Adjust :as-of to match the tx count printed after the first arc transact.
# Expected: :beta
(query [:find ?to
        :as-of 9
        :where (path :alpha ?to)])

# --- valid-time (:valid-at) ---
# Model connections that are only active during certain periods.
(transact {:valid-from "2024-01-01" :valid-to "2024-12-31"}
          [[:hub-a :route :hub-b]])
(transact [[:hub-b :route :hub-c]])

(rule [(reachable ?x ?y) [?x :route ?y]])
(rule [(reachable ?x ?y) [?x :route ?m] (reachable ?m ?y)])

# In 2024, hub-a→hub-b is active; hub-a can reach both b and c
# Expected: :hub-b, :hub-c
(query [:find ?to
        :valid-at "2024-06-01"
        :where (reachable :hub-a ?to)])

# In 2025, hub-a→hub-b has expired; hub-a cannot reach anything
# Expected: no results
(query [:find ?to
        :valid-at "2025-06-01"
        :where (reachable :hub-a ?to)])

EXIT

# ========================================
# Summary
# ========================================
# Recursive rules enable powerful graph queries:
# - Transitive closure (reachability)
# - Cycle handling with convergence
# - Arbitrary-depth traversals
# - Hierarchical relationships (ancestors, descendants)
# - Time-travel: :as-of queries graph state at a prior tx
# - Valid-time: :valid-at activates only edges valid at that instant
#
# The semi-naive evaluation algorithm ensures:
# - Efficient computation (only processes new facts)
# - Guaranteed termination (max iteration limit)
# - Correct results even with cycles
# ========================================
