1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8
9. 9
10. 10
11. 11
12. 12
13. 13
14. 14
15. 15
16. 16
17. 17
18. 18
19. 19
20. 20
21. 21
22. 22
23. 23
24. 24
25. 25
26. 26
27. 27
28. 28
29. 29
30. 30
31. 31
32. 32
33. 33
34. 34
35. 35
36. 36
37. 37
38. 38
39. 39
40. 40
41. 41
42. 42
43. 43
44. 44
45. 45
46. 46
47. 47
48. 48
49. 49
50. 50
51. 51
52. 52
53. 53
54. 54
55. 55
56. 56
57. 57
58. 58
59. 59
60. 60
61. 61
62. 62
63. 63
64. 64
65. 65
66. 66
67. 67
68. 68
69. 69
70. 70
71. 71
72. 72

import Std.Data

abbrev TypeList := { αs : List Type // 0 < αs.length }

def TypeList.toType : TypeList → Type
  | ⟨[α], _⟩ => α
  | ⟨α :: α' :: αs, _⟩ => α × TypeList.toType ⟨α' :: αs, by grind⟩

inductive DTerm (α : Type)
  | const (x : α)
  | var (s : String)

def TypeList.toDTerms : TypeList → Type
  | ⟨[α], _⟩ => DTerm α
  | ⟨α :: α' :: αs, _⟩ => DTerm α × TypeList.toDTerms ⟨α' :: αs, by grind⟩

def Atom (relations : Std.HashMap String TypeList) :=
  (rel : { rel : String // rel ∈ relations.keys }) × (relations[rel.val]'(by grind)).toDTerms

def Rule (relations : Std.HashMap String TypeList) :=
  Atom relations × List (Atom relations)

def relations : Std.HashMap String TypeList :=
  .ofList [
    ("edge", ⟨[Nat, Nat], by decide⟩),
    ("path", ⟨[Nat, Nat], by decide⟩),
  ]

theorem relEdge : relations["edge"]'(by simp [relations]) = ⟨[Nat, Nat], by decide⟩ := by
  simp [relations]
  grind

theorem relPath : relations["path"]'(by simp [relations]) = ⟨[Nat, Nat], by decide⟩ := by
  simp [relations]
  grind

def pathRule : Rule relations := by
  constructor
  · simp [Atom]
    constructor
    rotate_left
    · exact ⟨"path", by simp [relations]⟩
    · simp
      rw [relPath]

      simp [TypeList.toDTerms]
      exact (.var "x", .var "y")



      --  : { rel // rel ∈ relations.keys }), (DTerm.var "x", DTerm.var "y"))
  -- (((⟨"path", by native_decide⟩ : { rel // rel ∈ relations.keys }), (DTerm.var "x", DTerm.var "y")),
  -- [
  --   ((⟨"path", by native_decide⟩ : { rel // rel ∈ relations.keys }), (DTerm.var "y", DTerm.var "z")),
  --   ((⟨"edge", by native_decide⟩ : { rel // rel ∈ relations.keys }), (DTerm.var "x", DTerm.var "z")),
  -- ])



--
-- def Relation αs (h : 0 < αs.length := by grind) [BEq (ListToTypeTuple αs h)] [Hashable (ListToTypeTuple αs h)] :=
--   Std.HashSet (ListToTypeTuple αs h)

-- def A : Relation [String, String] := .ofList [("hi", "blah")]

-- def Rule (head : )

-- #eval A.contains ("hi", "blah")


-- def main : IO Unit :=
--   IO.println s!"Hello!"