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
73. 73
74. 74
75. 75
76. 76
77. 77
78. 78
79. 79
80. 80
81. 81
82. 82
83. 83
84. 84
85. 85
86. 86
87. 87
88. 88
89. 89
90. 90
91. 91
92. 92
93. 93
94. 94
95. 95
96. 96
97. 97
98. 98
99. 99
100. 100
101. 101
102. 102
103. 103
104. 104
105. 105
106. 106
107. 107
108. 108
109. 109
110. 110
111. 111
112. 112
113. 113
114. 114
115. 115
116. 116
117. 117
118. 118
119. 119
120. 120
121. 121
122. 122
123. 123
124. 124
125. 125
126. 126
127. 127
128. 128
129. 129
130. 130
131. 131
132. 132
133. 133
134. 134
135. 135
136. 136
137. 137
138. 138

import Cert
import Dependent

/-! # Translator from `Dependent.Term` to `Cert.Node`

`Dependent.Term` is a regular tree; the per-`app` φ-field bloat is only
introduced at *serialisation* time.  We walk the tree once, calling our
hash-consing smart constructors, so the resulting indexed AST automatically
shares duplicate subterms.

The dbify-only constructors (`name`, `vlam`, `vfn`) should be gone before we
get here; if they're present, the translator panics.
-/

namespace Cert

/-- Translator with opaque-theorem substitution: at every subterm, check
whether it `==` (BEq) one of the known theorem's body Terms.  If so, emit a
reference to that theorem's opaque leaf instead of recursing.  Each helper's
body is assumed *closed* (no free `name`s), so `dbify [] body` is independent
of the names list at the use site. -/
partial def translateTermK (known : List (_root_.Term × Nat))
    (t : _root_.Term) : BuilderM Nat := do
  match known.find? (·.1 == t) with
  | some (_, opaqueIdx) => return opaqueIdx
  | none =>
    match t with
    | _root_.Term.var x        => Cert.var x
    | _root_.Term.lam b        => do let b' ← translateTermK known b; Cert.lam b'
    | _root_.Term.app f φ a    => do
        let f' ← translateTermK known f
        let φ' ← translateTermK known φ
        let a' ← translateTermK known a
        Cert.app f' φ' a'
    | _root_.Term.typ u        => Cert.typ u
    | _root_.Term.fn α β       => do
        let α' ← translateTermK known α
        let β' ← translateTermK known β
        Cert.fn α' β'
    | _root_.Term.prod α β     => do
        let α' ← translateTermK known α
        let β' ← translateTermK known β
        Cert.prod α' β'
    | _root_.Term.pmk          => Cert.pmk
    | _root_.Term.prod_rec     => Cert.prodRec
    | _root_.Term.sum α β      => do
        let α' ← translateTermK known α
        let β' ← translateTermK known β
        Cert.sum α' β'
    | _root_.Term.inl          => Cert.inl
    | _root_.Term.inr          => Cert.inr
    | _root_.Term.sum_rec      => Cert.sumRec
    | _root_.Term.eq a a' α    => do
        let ea  ← translateTermK known a
        let ea' ← translateTermK known a'
        let eα  ← translateTermK known α
        Cert.eq ea ea' eα
    | _root_.Term.refl         => Cert.refl
    | _root_.Term.eq_rec       => Cert.eqRec
    | _root_.Term.nat          => Cert.nat
    | _root_.Term.zero         => Cert.zero
    | _root_.Term.succ         => Cert.succ
    | _root_.Term.nat_rec      => Cert.natRec
    | _root_.Term.unit         => Cert.unit
    | _root_.Term.intro        => Cert.intro
    | _root_.Term.fls          => Cert.fls
    | _root_.Term.fls_rec      => Cert.flsRec
    | _root_.Term.name s       => panic! s!"`name {s}` reached translator; call dbify first"
    | _root_.Term.vlam s _     => panic! s!"`vlam {s}` reached translator; call dbify first"
    | _root_.Term.vfn s _ _    => panic! s!"`vfn {s}` reached translator; call dbify first"

/-- Plain translator — equivalent to `translateTermK []`. -/
@[inline] def translateTerm (t : _root_.Term) : BuilderM Nat := translateTermK [] t

/-- The 14 built-in constructors that have a fixed dbtype (paired with their
tag number). -/
private def builtinConstants : List (Nat × _root_.Term) :=
  [ (6,  _root_.Term.pmk),
    (7,  _root_.Term.prod_rec),
    (9,  _root_.Term.inl),
    (10, _root_.Term.inr),
    (11, _root_.Term.sum_rec),
    (13, _root_.Term.refl),
    (14, _root_.Term.eq_rec),
    (15, _root_.Term.nat),
    (16, _root_.Term.zero),
    (17, _root_.Term.succ),
    (18, _root_.Term.nat_rec),
    (19, _root_.Term.unit),
    (20, _root_.Term.intro),
    (21, _root_.Term.fls),
    (22, _root_.Term.fls_rec) ]

/-- Translate a `(term, type)` pair from `Dependent.lean`.  Both are dbify-d
first so all `name`/`vlam`/`vfn` go away.  Also translates the dbtype of each
built-in constant so check-cert can look them up. -/
def translatePair (p : _root_.Term × _root_.Term) : BuilderM (Nat × Nat × List (Nat × Nat)) := do
  let t ← translateTerm (dbify [] p.1)
  let τ ← translateTerm (dbify [] p.2)
  let mut dbtypeIdxs : List (Nat × Nat) := []
  for (tag, c) in builtinConstants do
    let dbt := c.dbtype
    let idx ← translateTerm dbt
    dbtypeIdxs := dbtypeIdxs ++ [(tag, idx)]
  return (t, τ, dbtypeIdxs)

/-- Translate a `(term, type)` pair, treating each entry of `helpers` as an
opaque theorem.  `helpers` must be in dependency order: theorem #i may only
reference theorems #0..#(i-1) opaquely.

Each helper is registered via `opaqueTheorem` (whose body is verified by the
emitted assert before the main proof's assert runs).  The main proof is then
translated with all helpers visible — any subterm equal (BEq) to a helper's
dbify'd body is replaced by a reference to that helper's opaque leaf. -/
def translatePairWithTheorems
    (helpers : List (String × _root_.Term × _root_.Term))
    (p : _root_.Term × _root_.Term) :
    BuilderM (Nat × Nat × List (Nat × Nat)) := do
  let mut known : List (_root_.Term × Nat) := []
  for (hname, hbody, htype) in helpers do
    let dbBody := dbify [] hbody
    let dbType := dbify [] htype
    -- Capture for the closure.
    let curKnown := known
    let opaqueIdx ← opaqueTheorem hname
      (translateTermK curKnown dbBody)
      (translateTermK curKnown dbType)
    known := known ++ [(dbBody, opaqueIdx)]
  let t ← translateTermK known (dbify [] p.1)
  let τ ← translateTermK known (dbify [] p.2)
  let mut dbtypeIdxs : List (Nat × Nat) := []
  for (tag, c) in builtinConstants do
    let dbt := c.dbtype
    let idx ← translateTerm dbt
    dbtypeIdxs := dbtypeIdxs ++ [(tag, idx)]
  return (t, τ, dbtypeIdxs)

end Cert