a13f2ab · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

more small changes

commita13f2ab452b9b4c92b8a6c38b005dba8612c0503 authorMartin Baker <git87465@martinb.com> dateSun 19 May 2019, 11:30 (7 years ago) parent73dfb0c

2 files changed+27−55

compare with master

unifiedsplit

docs/proofs/example1.rst+10−30 docs/proofs/primitive.rst+17−25

docs/proofs/example1.rst+10−30

@@ -84,16 +84,12 @@ The following is a walkthough looking at the state after each tactic:

8484 - intro \`{{x}}

8585

8686 * - state now looks like this

87− - state

88−

89− .. image:: ../image/elabProofStateEx1_2.png

87+ - .. image:: ../image/elabProofStateEx1_2.png

9088 :width: 312px

9189 :height: 84px

9290

9391 * - logic now looks like this

94− - logic

95−

96− .. image:: ../image/elabLogicEx1_2.png

92+ - .. image:: ../image/elabLogicEx1_2.png

9793 :width: 126px

9894 :height: 45px

9995

@@ -106,9 +102,7 @@ The following is a walkthough looking at the state after each tactic:

106102

107103 getHoles

108104

109− - state.

110−

111− .. code-block:: idris

105+ - .. code-block:: idris

112106

113107 getEnv=[(

114108 `{{x}}, {

@@ -138,16 +132,12 @@ The following is a walkthough looking at the state after each tactic:

138132 - fill (Var \`{{x}})

139133

140134 * - state now looks like this

141− - state

142−

143− .. image:: ../image/elabProofStateEx1_3.png

135+ - .. image:: ../image/elabProofStateEx1_3.png

144136 :width: 312px

145137 :height: 124px

146138

147139 * - logic now looks like this

148− - logic

149−

150− .. image:: ../image/elabLogicEx1_3.png

140+ - .. image:: ../image/elabLogicEx1_3.png

151141 :width: 131px

152142 :height: 45px

153143

@@ -160,9 +150,7 @@ The following is a walkthough looking at the state after each tactic:

160150

161151 getHoles

162152

163− - state.

164−

165− .. code-block:: idris

153+ - .. code-block:: idris

166154

167155 getEnv=[(`{{x}}, {λ ({`{{Nat}}.["Nat", "Prelude"]}:

168156 {type const tag=8,0}).

@@ -184,9 +172,7 @@ The following is a walkthough looking at the state after each tactic:

184172 getHoles=[{hole_2}, {hole_0}]

185173

186174 * - getGuess

187− - state.

188−

189− .. code-block:: idris

175+ - .. code-block:: idris

190176

191177 {TT:Parameter name ref

192178 NameType=NameType just bound by intro

@@ -204,9 +190,7 @@ The following is a walkthough looking at the state after each tactic:

204190 - solve

205191

206192 * - logic now looks like this

207− - logic

208−

209− .. image:: ../image/elabLogicEx1_4.png

193+ - .. image:: ../image/elabLogicEx1_4.png

210194 :width: 131px

211195 :height: 14px

212196

@@ -219,9 +203,7 @@ The following is a walkthough looking at the state after each tactic:

219203

220204 getHoles

221205

222− - state.

223−

224− .. code-block:: idris

206+ - .. code-block:: idris

225207

226208 getEnv=[]

227209

@@ -243,9 +225,7 @@ The following is a walkthough looking at the state after each tactic:

243225 getHoles=[{hole_0}]

244226

245227 * - getGuess

246− - state.

247−

248− .. code-block:: idris

228+ - .. code-block:: idris

249229

250230 {TT:Bind

251231 name=`{{x}}

docs/proofs/primitive.rst+17−25

@@ -269,19 +269,17 @@ Primitive Operators

269269

270270 debug : Elab a

271271

272− Only seems to compile if 'debug' is last tactic so comment out following tactics like this:

272+ If 'debug' is not the last tactic then make sure its type is sufficiently constrained. In particular, its type is Elab a, but there's no way for Idris to find out which type was meant for a. This can be fixed by either writing an explicit type (e.g. debug {a = ()}) or by using a helper that constrains the type (such as simple in Pruviloj, e.g. simple debug as a line).

273273

274274 .. code-block:: idris

275275

276276 %language ElabReflection

277277

278278 idNat : Nat -> Nat

279− idNat = %runElab (do

280− intro `{{x}}

281− debug

282− -- fill (Var `{{x}})

283− -- solve

284− )

279+ idNat = %runElab (do intro `{{x}}

280+ debug {a = ()}

281+ fill (Var `{{x}})

282+ solve)

285283

286284 * - debugMessage

287285 - Halt elaboration, dumping the internal state and displaying a message.

@@ -294,18 +292,16 @@ Primitive Operators

294292

295293 debugMessage : (msg : List ErrorReportPart) -> Elab a

296294

297− Only seems to compile if 'debug' is last tactic so comment out following tactics like this:

295+ If 'debugMessage' is not the last tactic then make sure its type is sufficiently constrained. In particular, its type is Elab a, but there's no way for Idris to find out which type was meant for a. This can be fixed by either writing an explicit type (e.g. debugMessage [TextPart "message"] {a = ()}) or by using a helper that constrains the type (such as simple in Pruviloj, e.g. simple debug as a line).

298296

299297 .. code-block:: idris

300298

301299 %language ElabReflection

302300 idNat : Nat -> Nat

303− idNat = %runElab (do

304− intro `{{x}}

305− debugMessage [TextPart "error message"]

306− -- fill (Var `{{x}})

307− -- solve

308− )

301+ idNat = %runElab (do intro `{{x}}

302+ debugMessage [TextPart "error message"] {a = ()}

303+ fill (Var `{{x}})

304+ solve)

309305

310306 * - metavar

311307 - Create a new top-level metavariable to solve the current hole.

@@ -442,21 +438,17 @@ Error Handling

442438

443439 tryCatch : Elab a -> (Err -> Elab a) -> Elab a

444440

445− Fixme - following does not work.

446−

447441 .. code-block:: idris

448442

449443 %language ElabReflection

450444

451− id1 : Elab ()

452− id1 = do

453− tryCatch (intro `{{x}})

454− (\err -> (intro `{{x}}))

455− fill (Var `{{x}})

456− solve

445+ f : Err -> Elab ()

446+ f (Msg _) = fill `("message error")

447+ f (CantUnify _ _ _ _ _ _) = fill `("unification error")

448+ f _ = fill `("other")

457449

458− idNat : Nat -> Nat

459− idNat = %runElab id1

450+ s2 : String

451+ s2 = %runElab (do tryCatch (fill `(True)) f ; solve)

460452

461453 * - fail

462454 - Halt elaboration with an error

@@ -482,5 +474,5 @@ Error Handling

482474 solve

483475

484476 idNat : Nat -> Nat

485− idNat = %runElab id1</td>

477+ idNat = %runElab id1

486478