a13f2ab · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

more small changes

a13f2abMartin Baker7 years ago

docs/proofs/example1.rst+10−30

compare with master

unifiedsplit

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

84 - intro \`{{x}}

86 * - state now looks like this

87− - state

88−

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

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

90 :width: 312px

88 :width: 312px

91 :height: 84px

89 :height: 84px

93 * - logic now looks like this

91 * - logic now looks like this

94− - logic

95−

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

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

97 :width: 126px

93 :width: 126px

98 :height: 45px

94 :height: 45px

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

106

102

107 getHoles

103 getHoles

108

104

109− - state.

110−

111− .. code-block:: idris

105+ - .. code-block:: idris

112

106

113 getEnv=[(

107 getEnv=[(

114 `{{x}}, {

108 `{{x}}, {

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

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

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

139

133

140 * - state now looks like this

134 * - state now looks like this

141− - state

142−

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

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

144 :width: 312px

136 :width: 312px

145 :height: 124px

137 :height: 124px

146

138

147 * - logic now looks like this

139 * - logic now looks like this

148− - logic

149−

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

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

151 :width: 131px

141 :width: 131px

152 :height: 45px

142 :height: 45px

153

143

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

160

150

161 getHoles

151 getHoles

162

152

163− - state.

164−

165− .. code-block:: idris

153+ - .. code-block:: idris

166

154

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

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

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

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

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

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

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

185

173

186 * - getGuess

174 * - getGuess

187− - state.

188−

189− .. code-block:: idris

175+ - .. code-block:: idris

190

176

191 {TT:Parameter name ref

177 {TT:Parameter name ref

192 NameType=NameType just bound by intro

178 NameType=NameType just bound by intro

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

204 - solve

190 - solve

205

191

206 * - logic now looks like this

192 * - logic now looks like this

207− - logic

208−

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

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

210 :width: 131px

194 :width: 131px

211 :height: 14px

195 :height: 14px

212

196

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

219

203

220 getHoles

204 getHoles

221

205

222− - state.

223−

224− .. code-block:: idris

206+ - .. code-block:: idris

225

207

226 getEnv=[]

208 getEnv=[]

227

209

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

243 getHoles=[{hole_0}]

225 getHoles=[{hole_0}]

244

226

245 * - getGuess

227 * - getGuess

246− - state.

247−

248− .. code-block:: idris

228+ - .. code-block:: idris

249

229

250 {TT:Bind

230 {TT:Bind

251 name=`{{x}}

231 name=`{{x}}

docs/proofs/primitive.rst+17−25

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

269

270 debug : Elab a

271

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).

273

274 .. code-block:: idris

275

276 %language ElabReflection

277

278 idNat : Nat -> Nat

279− idNat = %runElab (do

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

280− intro `{{x}}

281− debug

280+ debug {a = ()}

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

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

283− -- solve

282+ solve)

284− )

285

283

286 * - debugMessage

284 * - debugMessage

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

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

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

294

292

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

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

296

294

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).

298

296

299 .. code-block:: idris

297 .. code-block:: idris

300

298

301 %language ElabReflection

299 %language ElabReflection

302 idNat : Nat -> Nat

300 idNat : Nat -> Nat

303− idNat = %runElab (do

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

304− intro `{{x}}

305− debugMessage [TextPart "error message"]

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

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

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

307− -- solve

304+ solve)

308− )

309

305

310 * - metavar

306 * - metavar

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

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

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

442

438

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

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

444

440

445− Fixme - following does not work.

446−

447 .. code-block:: idris

441 .. code-block:: idris

448

442

449 %language ElabReflection

443 %language ElabReflection

450

444

451− id1 : Elab ()

445+ f : Err -> Elab ()

452− id1 = do

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

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

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

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

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

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

456− solve

457

449

458− idNat : Nat -> Nat

450+ s2 : String

459− idNat = %runElab id1

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

460

452

461 * - fail

453 * - fail

462 - Halt elaboration with an error

454 - Halt elaboration with an error

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

482 solve

474 solve

483

475

484 idNat : Nat -> Nat

476 idNat : Nat -> Nat

485− idNat = %runElab id1</td>

477+ idNat = %runElab id1

486

478