@@ -48,28 +48,20 @@ The following is a walkthough looking at the state after each tactic:
4848 * - The term is:
4949 - ?{hole_0} ≈ ? {hole_2} . {hole_2} . {hole_0}
5050
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.
5252
53− - .. code-block:: idris
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+
55+ .. code-block:: idris
5456
5557 getEnv=[]
5658
57− getGoal=({hole_2}, {TT:Bind
58− name=`{{__pi_arg}}
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"]}
68− TT={TT:TType
69− tt=ext=./Prelude/Nat.idr#20
70− }
71− }
72− })
59+ getGoal=(hole_2, __pi_arg:(Nat.["Nat", "Prelude"]:{
60+ type constructor tag=8 number=0}.Type:U=(20:./Prelude/Nat.idr)->.
61+ {name ref{type constructor tag=8 number=0}Nat.["Nat","Prelude"]:
62+ Type:U=(20:./Prelude/Nat.idr)
63+ })
64+ })
7365
7466 getHoles=[{hole_2},{hole_0}]
7567
@@ -96,24 +88,14 @@ The following is a walkthough looking at the state after each tactic:
9688
9789 - .. code-block:: idris
9890
99− getEnv=[(
100− `{{x}}, {
101− λ ({`{{Nat}}.["Nat", "Prelude"]}:{type const tag=8,0}).
102− {TT:TType
103− tt=ext=./Prelude/Nat.idr#20
104− }
105− }
106− )]
107−
108− getGoal=({hole_2},{
109− TT:Parameter name ref
110− NameType={type const tag=8,0}
111− TTName={`{{Nat}}.["Nat", "Prelude"]}
112− TT={TT:TType
113− tt=ext=./Prelude/Nat.idr#20
114− }
115− }
116− )
91+ getEnv=[(x, {λ (Nat.["Nat", "Prelude"]:{
92+ type constructor tag=8 number=0}).
93+ Type:U=(20:./Prelude/Nat.idr)
94+ })]
95+
96+ getGoal=(hole_2, {name ref{type constructor tag=8 number=0}
97+ Nat.["Nat","Prelude"]:Type:U=(20:./Prelude/Nat.idr)
98+ })
11799
118100 getHoles=[{hole_2},{hole_0}]
119101
@@ -140,38 +122,24 @@ The following is a walkthough looking at the state after each tactic:
140122
141123 - .. code-block:: idris
142124
143− getEnv=[(`{{x}}, {λ ({`{{Nat}}.["Nat", "Prelude"]}:
144− {type const tag=8,0}).
145− {TT:TType
146− tt=ext=./Prelude/Nat.idr#20
147− }
148− }
149− )]
150−
151− getGoal=({hole_2},
152− {TT:Parameter name ref
153− NameType={type const tag=8,0}
154− TTName={`{{Nat}}.["Nat", "Prelude"]}
155− TT={TT:TType
156− tt=ext=./Prelude/Nat.idr#20
157− }
158− })
125+ getEnv=[(x, {λ (Nat.["Nat", "Prelude"]:
126+ {type constructor tag=8 number=0}).
127+ Type:U=(20:./Prelude/Nat.idr)
128+ })]
129+
130+ getGoal=(hole_2, {name ref{type constructor tag=8 number=0}
131+ Nat.["Nat","Prelude"]:Type:U=(20:./Prelude/Nat.idr)
132+ })
159133
160134 getHoles=[{hole_2}, {hole_0}]
161135
162136 * - getGuess
163137 - .. code-block:: idris
164138
165− {TT:Parameter name ref
166− NameType=NameType just bound by intro
167− TTName=`{{x}}
168− TT={TT:Parameter name ref
169− NameType={type const tag=8,0}
170− TTName={`{{Nat}}.["Nat", "Prelude"]}
171− TT={TT:TType
172− tt=ext=./Prelude/Nat.idr#20
173− }
174− }
139+ {name ref bound x:
140+ {name ref{type constructor tag=8 number=0}
141+ Nat.["Nat","Prelude"]:Type:U=(20:./Prelude/Nat.idr)
142+ }
175143 }
176144
177145 * - Substitute a guess into a hole.
@@ -195,45 +163,30 @@ The following is a walkthough looking at the state after each tactic:
195163
196164 getEnv=[]
197165
198− getGoal=({hole_0}, {TT:Bind
199− name=`{{__pi_arg}}
200− binder={
201− Π ({`{{Nat}}.["Nat", "Prelude"]}:
202− {type const tag=8,0}).{TT:TType
203− tt=ext=./Prelude/Nat.idr#20
204− }
205− }
206− tt={TT:Parameter name ref
207− NameType={type const tag=8,0}
208− TTName={`{{Nat}}.["Nat","Prelude"]}
209− TT={TT:TType tt=ext=./Prelude/Nat.idr#20}
210− }
211− })
166+ getGoal=(hole_0, __pi_arg:(Nat.["Nat", "Prelude"]:{
167+ type constructor tag=8 number=0}.
168+ Type:U=(20:./Prelude/Nat.idr)
169+ ->.{name ref
170+ {type constructor tag=8 number=0}
171+ Nat.["Nat","Prelude"]:Type:U=(20:./Prelude/Nat.idr)
172+ })
173+ })
212174
213175 getHoles=[{hole_0}]
214176
215177 * - getGuess
216178 - .. code-block:: idris
217179
218− {TT:Bind
219− name=`{{x}}
220− binder={λ ({`{{Nat}}.["Nat","Prelude"]}:{type const tag=8,0}).{
221− TT:TType
222− tt=ext=./Prelude/Nat.idr#20
223− }
180+ x:({λ (Nat.["Nat", "Prelude"]:{
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}
186+ Nat.["Nat","Prelude"]:Type:U=(20:./Prelude/Nat.idr)
187+ }
188+ })
224189 }
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− }
237190
238191.. target-notes::
239192.. _`my code`: https://github.com/martinbaker/Idris-dev/blob/uglyTTPrinter/libs/prelude/Language/Reflection/TTPrinter.idr