git.iko.soy/Idris-dev
on master help sign in
explain getEnv, getGoal, getHoles and getGuess better
cf3071dmartinbaker
docs/proofs/example1.rst+47−94
compare with master
unifiedsplit
@@ -48,28 +48,20 @@ The following is a walkthough looking at the state after each tactic:
48 * - The term is:
48 * - The term is:
49 - ?{hole_0} ≈ ? {hole_2} . {hole_2} . {hole_0}
49 - ?{hole_0} ≈ ? {hole_2} . {hole_2} . {hole_0}
50
50
51− * - It is possible to read the state from the script by calling getEnv, getGoal and getHoles. To show the results I hacked this: `my code`_.
51+ * - It is possible to read the state from the script by calling getEnv, getGoal and getHoles.
52
52
53+ - The output of these calls contain structures with TT code. To show the results I hacked this: `my code`_. TT code is not really designed to be readable by humans, all the names are fully expanded, everything has a type down to universes (type of types). This is shown here to illustrate the information available.
54+
53− - .. code-block:: idris
55+ .. code-block:: idris
54
56
55 getEnv=[]
57 getEnv=[]
56
58
57− getGoal=({hole_2}, {TT:Bind
59+ getGoal=(hole_2, __pi_arg:(Nat.["Nat", "Prelude"]:{
58− name=`{{__pi_arg}}
60+ type constructor tag=8 number=0}.Type:U=(20:./Prelude/Nat.idr)->.
59− binder={
60− Π ({`{{Nat}}.["Nat", "Prelude"]}:{type const tag=8,0}).{
61− TT:TType tt=ext=./Prelude/Nat.idr#20
62− }
63− }
64− tt={
65− TT:Parameter name ref
66− NameType={type const tag=8,0}
67− TTName={`{{Nat}}.["Nat","Prelude"]}
61+ {name ref{type constructor tag=8 number=0}Nat.["Nat","Prelude"]:
68− TT={TT:TType
69− tt=ext=./Prelude/Nat.idr#20
62+ Type:U=(20:./Prelude/Nat.idr)
70− }
63+ })
71− }
72− })
64+ })
73
65
74 getHoles=[{hole_2},{hole_0}]
66 getHoles=[{hole_2},{hole_0}]
75
67
@@ -96,24 +88,14 @@ The following is a walkthough looking at the state after each tactic:
96
88
97 - .. code-block:: idris
89 - .. code-block:: idris
98
90
99− getEnv=[(
100− `{{x}}, {
101− λ ({`{{Nat}}.["Nat", "Prelude"]}:{type const tag=8,0}).
91+ getEnv=[(x, {λ (Nat.["Nat", "Prelude"]:{
102− {TT:TType
92+ type constructor tag=8 number=0}).
103− tt=ext=./Prelude/Nat.idr#20
93+ Type:U=(20:./Prelude/Nat.idr)
104− }
105− }
106− )]
94+ })]
107−
95+
108− getGoal=({hole_2},{
96+ getGoal=(hole_2, {name ref{type constructor tag=8 number=0}
109− TT:Parameter name ref
110− NameType={type const tag=8,0}
111− TTName={`{{Nat}}.["Nat", "Prelude"]}
97+ Nat.["Nat","Prelude"]:Type:U=(20:./Prelude/Nat.idr)
112− TT={TT:TType
113− tt=ext=./Prelude/Nat.idr#20
114− }
98+ })
115− }
116− )
117
99
118 getHoles=[{hole_2},{hole_0}]
100 getHoles=[{hole_2},{hole_0}]
119
101
@@ -140,38 +122,24 @@ The following is a walkthough looking at the state after each tactic:
140
122
141 - .. code-block:: idris
123 - .. code-block:: idris
142
124
143− getEnv=[(`{{x}}, {λ ({`{{Nat}}.["Nat", "Prelude"]}:
125+ getEnv=[(x, {λ (Nat.["Nat", "Prelude"]:
144− {type const tag=8,0}).
126+ {type constructor tag=8 number=0}).
145− {TT:TType
146− tt=ext=./Prelude/Nat.idr#20
127+ Type:U=(20:./Prelude/Nat.idr)
147− }
148− }
149− )]
128+ })]
150−
129+
151− getGoal=({hole_2},
130+ getGoal=(hole_2, {name ref{type constructor tag=8 number=0}
152− {TT:Parameter name ref
153− NameType={type const tag=8,0}
154− TTName={`{{Nat}}.["Nat", "Prelude"]}
131+ Nat.["Nat","Prelude"]:Type:U=(20:./Prelude/Nat.idr)
155− TT={TT:TType
156− tt=ext=./Prelude/Nat.idr#20
157− }
158− })
132+ })
159
133
160 getHoles=[{hole_2}, {hole_0}]
134 getHoles=[{hole_2}, {hole_0}]
161
135
162 * - getGuess
136 * - getGuess
163 - .. code-block:: idris
137 - .. code-block:: idris
164
138
165− {TT:Parameter name ref
139+ {name ref bound x:
166− NameType=NameType just bound by intro
140+ {name ref{type constructor tag=8 number=0}
167− TTName=`{{x}}
168− TT={TT:Parameter name ref
169− NameType={type const tag=8,0}
170− TTName={`{{Nat}}.["Nat", "Prelude"]}
141+ Nat.["Nat","Prelude"]:Type:U=(20:./Prelude/Nat.idr)
171− TT={TT:TType
172− tt=ext=./Prelude/Nat.idr#20
173− }
174− }
142+ }
175 }
143 }
176
144
177 * - Substitute a guess into a hole.
145 * - Substitute a guess into a hole.
@@ -195,45 +163,30 @@ The following is a walkthough looking at the state after each tactic:
195
163
196 getEnv=[]
164 getEnv=[]
197
165
198− getGoal=({hole_0}, {TT:Bind
199− name=`{{__pi_arg}}
200− binder={
201− Π ({`{{Nat}}.["Nat", "Prelude"]}:
166+ getGoal=(hole_0, __pi_arg:(Nat.["Nat", "Prelude"]:{
202− {type const tag=8,0}).{TT:TType
167+ type constructor tag=8 number=0}.
203− tt=ext=./Prelude/Nat.idr#20
168+ Type:U=(20:./Prelude/Nat.idr)
204− }
205− }
206− tt={TT:Parameter name ref
169+ ->.{name ref
207− NameType={type const tag=8,0}
170+ {type constructor tag=8 number=0}
208− TTName={`{{Nat}}.["Nat","Prelude"]}
171+ Nat.["Nat","Prelude"]:Type:U=(20:./Prelude/Nat.idr)
209− TT={TT:TType tt=ext=./Prelude/Nat.idr#20}
210− }
172+ })
211− })
173+ })
212
174
213 getHoles=[{hole_0}]
175 getHoles=[{hole_0}]
214
176
215 * - getGuess
177 * - getGuess
216 - .. code-block:: idris
178 - .. code-block:: idris
217
179
218− {TT:Bind
219− name=`{{x}}
220− binder={λ ({`{{Nat}}.["Nat","Prelude"]}:{type const tag=8,0}).{
180+ x:({λ (Nat.["Nat", "Prelude"]:{
221− TT:TType
181+ type constructor tag=8 number=0}).
182+ Type:U=(20:./Prelude/Nat.idr)
183+ }.{
184+ name ref bound
185+ x:{name ref {type constructor tag=8 number=0}
222− tt=ext=./Prelude/Nat.idr#20
186+ Nat.["Nat","Prelude"]:Type:U=(20:./Prelude/Nat.idr)
187+ }
223− }
188+ })
224 }
189 }
225− tt={TT:Parameter name ref
226− NameType=NameType just bound by intro
227− TTName=`{{x}}
228− TT={TT:Parameter name ref
229− NameType={type const tag=8,0}
230− TTName={`{{Nat}}.["Nat", "Prelude"]}
231− TT={TT:TType
232− tt=ext=./Prelude/Nat.idr#20
233− }
234− }
235− }
236− }
237
190
238.. target-notes::
191.. target-notes::
239.. _`my code`: https://github.com/martinbaker/Idris-dev/blob/uglyTTPrinter/libs/prelude/Language/Reflection/TTPrinter.idr
192.. _`my code`: https://github.com/martinbaker/Idris-dev/blob/uglyTTPrinter/libs/prelude/Language/Reflection/TTPrinter.idr