35268c1 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Some paper updates, getting final version ready

35268c1Edwin Brady13 years ago

papers/impl-paper/elaboration.tex+43−29

compare with master

unifiedsplit

@@ -266,8 +266,8 @@ removes a hole from the head of the queue:

266

267\DM{

268\AR{

269−\MO{NewHole}\;=\;\RW{do}\;\AR{

269+\MO{NewHole}\;\vn\;=\;\RW{do}\;\AR{

270−(\vC,\Delta,\vP,\vQ)\gets\MO{Get}\\

270+(\vC,\Delta,\ve,\vP,\vQ)\gets\MO{Get}\\

271\MO{Put}\;(\vC,\Delta,\ve,\vP,\vn;\vQ)\\

272}

273\\

@@ -312,7 +312,8 @@ given in Figure \ref{runtac} which

312locates the appropriate sub-term, applies the tactic with the context

313local to this sub-term, and

314replaces the sub-term with the term returned by the

315−tactic.

315+tactic. Note that monadic lifting is left implicit in this Figure, so that

316+the details of the algorithm are not obscured.

316% It then updates the hole queue in the proof state, and updates holes which have

317% It then updates the hole queue in the proof state, and updates holes which have

317% been solved by unification. If the tactic creates new holes, these are automatically

318% been solved by unification. If the tactic creates new holes, these are automatically

318% added to the \remph{head} of the hole queue.

319% added to the \remph{head} of the hole queue.

@@ -322,7 +323,7 @@ tactic.

322\MO{Tactic}\;\VV{tac}\;=\;\RW{do}\;\AR{

323\MO{Tactic}\;\VV{tac}\;=\;\RW{do}\;\AR{

323\ve\Gets\MO{Term}\\

324\ve\Gets\MO{Term}\\

324\vh\Gets\MO{NextHole}\\

325\vh\Gets\MO{NextHole}\\

325−\ve'\Gets\MO{Tactic'}\;\langle\rangle\;\ve\;\VV{tac}\;\vh\\

326+\ve'\Gets\MO{Tactic'}\;\langle\rangle\;\ve\\

326\MO{SetTerm}\;\ve'

327\MO{SetTerm}\;\ve'

327}

328}

328\medskip

329\medskip

@@ -331,8 +332,23 @@ tactic.

331\RW{where} \\

332\RW{where} \\

332& \MO{Tactic'} & \Gamma & (\hole{\vx}{\vT}\SC\ve)

333& \MO{Tactic'} & \Gamma & (\hole{\vx}{\vT}\SC\ve)

333& \MoRet{\VV{tac}_\Gamma\;(\hole{\vx}{\vT}\SC\ve)\hg\mbox{if}\;\vx=\vh} \\

334& \MoRet{\VV{tac}_\Gamma\;(\hole{\vx}{\vT}\SC\ve)\hg\mbox{if}\;\vx=\vh} \\

335+& \MO{Tactic'} & \Gamma & (\hole{\vx}{\vT}\SC\ve)

336+& \MoRet{

337+\RW{do}\; \AR{\vT'\Gets\;\MO{Tactic'}\;\Gamma\;\vT\\

338+\RW{return}\;(\hole{\vx}{\vT'}\SC \MO{Tactic'}\;(\Gamma;\hole{\vx}{\vT'})\;\ve)

339+\hg\RW{otherwise}}

340+}

341+\\

334& \MO{Tactic'} & \Gamma & (\guess{\vx}{\vT}{\vv}\SC\ve)

342& \MO{Tactic'} & \Gamma & (\guess{\vx}{\vT}{\vv}\SC\ve)

335& \MoRet{\VV{tac}_\Gamma\;(\guess{\vx}{\vT}{\vv}\SC\ve)\hg\mbox{if}\;\vx=\vh} \\

343& \MoRet{\VV{tac}_\Gamma\;(\guess{\vx}{\vT}{\vv}\SC\ve)\hg\mbox{if}\;\vx=\vh} \\

344+

345+& \MO{Tactic'} & \Gamma & (\guess{\vx}{\vT}{\vv}\SC\ve)

346+& \MoRet{\RW{do}\;\AR{\vv'\Gets\;\MO{Tactic'}\;\Gamma\;\vv\\

347+\vT'\Gets\;\MO{Tactic'}\;\Gamma\;\vT\\

348+\RW{return}\;(\guess{\vx}{\vT'}{\vv'}\SC

349+\MO{Tactic'}\;(\Gamma;\guess{\vx}{\vT'}{\vv'}\;\ve)

350+\hg\RW{otherwise}}} \\

351+

336& \MO{Tactic'} & \Gamma & (\lam{\vx}{\vT}\SC\ve)

352& \MO{Tactic'} & \Gamma & (\lam{\vx}{\vT}\SC\ve)

337& \MoRet{

353& \MoRet{

338\RW{do}\; \AR{\vT'\Gets\;\MO{Tactic'}\;\Gamma\;\vT\\

354\RW{do}\; \AR{\vT'\Gets\;\MO{Tactic'}\;\Gamma\;\vT\\

@@ -345,11 +361,11 @@ tactic.

345\RW{return}\;(\all{\vx}{\vT'}\SC \MO{Tactic'}\;(\Gamma;\all{\vx}{\vT'})\;\ve)}

361\RW{return}\;(\all{\vx}{\vT'}\SC \MO{Tactic'}\;(\Gamma;\all{\vx}{\vT'})\;\ve)}

346}

362}

347\\

363\\

348−& \MO{Tactic'} & \Gamma & (\LET\;\vx\defq\vt\Hab\vT\SC\ve)

364+& \MO{Tactic'} & \Gamma & (\LET\;\vx\defq\vv\Hab\vT\SC\ve)

349−& \MoRet{\RW{do}\;\AR{\vt'\Gets\;\MO{Tactic'}\;\Gamma\;\vt\\

365+& \MoRet{\RW{do}\;\AR{\vv'\Gets\;\MO{Tactic'}\;\Gamma\;\vv\\

350\vT'\Gets\;\MO{Tactic'}\;\Gamma\;\vT\\

366\vT'\Gets\;\MO{Tactic'}\;\Gamma\;\vT\\

351−\RW{return}\;(\LET\;\vx\defq\vt'\Hab\vT'\SC

367+\RW{return}\;(\LET\;\vx\defq\vv'\Hab\vT'\SC

352−\MO{Tactic'}\;(\Gamma;\LET\;\vx\defq\vt'\Hab\vT')\;\ve)}} \\

368+\MO{Tactic'}\;(\Gamma;\LET\;\vx\defq\vv'\Hab\vT')\;\ve)}} \\

353& \MO{Tactic'} & \Gamma & (\vf\;\va) &

369& \MO{Tactic'} & \Gamma & (\vf\;\va) &

354\MoRet{\RW{return}\;(\MO{Tactic'}\;\Gamma\;\vf)\; (\MO{Tactic'}\;\Gamma\;\va)}\\

370\MoRet{\RW{return}\;(\MO{Tactic'}\;\Gamma\;\vf)\; (\MO{Tactic'}\;\Gamma\;\va)}\\

355& \MO{Tactic'} & \Gamma & \vt & \MoRet{\RW{return}\;\vt}

371& \MO{Tactic'} & \Gamma & \vt & \MoRet{\RW{return}\;\vt}

@@ -429,7 +445,8 @@ keeping $\vx$ at the head:

429\PA{\A\A}{

445\PA{\A\A}{

430\MO{Claim}_\Gamma & (\vy \Hab\vS) & (\hole{\vx}{\vT}\SC\ve) &

446\MO{Claim}_\Gamma & (\vy \Hab\vS) & (\hole{\vx}{\vT}\SC\ve) &

431 \MoRet{\RW{do}\;\AR{\MO{NewHole}\;\vy\\

447 \MoRet{\RW{do}\;\AR{\MO{NewHole}\;\vy\\

448+ \MO{Focus}\:\vx\\

432− \RW{return}\;\hole{\vx}{\vT}\SC\hole{\vy}{\vS}\SC\ve}} \\

449+ \RW{return}\;\hole{\vy}{\vS}\SC\hole{\vx}{\vT}\SC\ve}} \\

433}

450}

434}

451}

435

452

@@ -692,23 +709,21 @@ the goal type.

692\medskip

709\medskip

693\\

710\\

694\mbox{Initial state}

711\mbox{Initial state}

695−& \hole{\vx}{\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA}\SC\vx

712+& \underline{\hole{\vx}{\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA}\SC\vx}

696& \langle\vx\rangle \\

713& \langle\vx\rangle \\

697%

714%

698\MO{Attack} &

715\MO{Attack} &

699−\underline{

700\guess{\vx}{\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA}{

716\guess{\vx}{\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA}{

701−\hole{\vh_0}{\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA}\SC\vh_0

717+\underline{\hole{\vh_0}{\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA}\SC\vh_0}

702}

718}

703\SC\vx

719\SC\vx

704−}

705&

720&

706\langle\vh_0,\vx\rangle\\

721\langle\vh_0,\vx\rangle\\

707%

722%

708\MO{Lambda}\;\vA &

723\MO{Lambda}\;\vA &

709\guess{\vx}{\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA}{

724\guess{\vx}{\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA}{

710−\underline{

725+\lam{\vA}{\Type}\SC\underline{

711−\lam{\vA}{\Type}\SC\hole{\vh_0}{\all{\va}{\vA}\SC\vA}\SC\vh_0

726+\hole{\vh_0}{\all{\va}{\vA}\SC\vA}\SC\vh_0

712}

727}

713}

728}

714\SC\vx

729\SC\vx

@@ -718,12 +733,12 @@ the goal type.

718\MO{Attack} &

733\MO{Attack} &

719\guess{\vx}{\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA}{

734\guess{\vx}{\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA}{

720\lam{\vA}{\Type}\SC

735\lam{\vA}{\Type}\SC

721−\underline{

722\guess{\vh_0}{\all{\va}{\vA}\SC\vA}

736\guess{\vh_0}{\all{\va}{\vA}\SC\vA}

737+{

738+\underline{

723−{\hole{\vh_1}{\all{\va}{\vA}\SC\vA}\SC\vh_1}

739+\hole{\vh_1}{\all{\va}{\vA}\SC\vA}\SC\vh_1}}

724\SC\vh_0

740\SC\vh_0

725}

741}

726−}

727\SC\vx

742\SC\vx

728&

743&

729\langle\vh_1,\vh_0,\vx\rangle\\

744\langle\vh_1,\vh_0,\vx\rangle\\

@@ -733,8 +748,8 @@ the goal type.

733\lam{\vA}{\Type}\SC

748\lam{\vA}{\Type}\SC

734\guess{\vh_0}{\all{\va}{\vA}\SC\vA}

749\guess{\vh_0}{\all{\va}{\vA}\SC\vA}

735{

750{

736−\underline{

751+\lam{\va}{\vA}\SC\underline{

737−\lam{\va}{\vA}\SC\hole{\vh_1}{\vA}\SC\vh_1

752+\hole{\vh_1}{\vA}\SC\vh_1

738}

753}

739}

754}

740\SC\vh_0

755\SC\vh_0

@@ -746,9 +761,10 @@ the goal type.

746\MO{Fill}\;\va &

761\MO{Fill}\;\va &

747\guess{\vx}{\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA}{

762\guess{\vx}{\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA}{

748\lam{\vA}{\Type}\SC

763\lam{\vA}{\Type}\SC

749−\\

764+%\\

750−&

765+%&

766+%\hg\hg\hg\hg\hg\hg\hg

751−\hg\hg\hg\hg\hg\hg\hg\guess{\vh_0}{\all{\va}{\vA}\SC\vA}

767+\guess{\vh_0}{\all{\va}{\vA}\SC\vA}

752{

768{

753\lam{\va}{\vA}\SC

769\lam{\va}{\vA}\SC

754\underline{

770\underline{

@@ -764,37 +780,35 @@ the goal type.

764\MO{Solve} &

780\MO{Solve} &

765\guess{\vx}{\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA}{

781\guess{\vx}{\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA}{

766\lam{\vA}{\Type}\SC

782\lam{\vA}{\Type}\SC

783+\underline{

767\guess{\vh_0}{\all{\va}{\vA}\SC\vA}

784\guess{\vh_0}{\all{\va}{\vA}\SC\vA}

768{

785{

769\lam{\va}{\vA}\SC

786\lam{\va}{\vA}\SC

770−\underline{

771\va

787\va

772}

788}

773−}

774\SC\vh_0

789\SC\vh_0

775}

790}

791+}

776\SC\vx

792\SC\vx

777&

793&

778\langle\vh_0,\vx\rangle\\

794\langle\vh_0,\vx\rangle\\

779%

795%

780\MO{Solve} &

796\MO{Solve} &

797+\underline{

781\guess{\vx}{\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA}{

798\guess{\vx}{\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA}{

782\lam{\vA}{\Type}\SC

799\lam{\vA}{\Type}\SC

783−\underline{

784\lam{\va}{\vA}\SC

800\lam{\va}{\vA}\SC

785\va

801\va

786}

802}

787−}

788\SC\vx

803\SC\vx

804+}

789&

805&

790\langle\vx\rangle\\

806\langle\vx\rangle\\

791%

807%

792\MO{Solve} &

808\MO{Solve} &

793−\underline{

794\lam{\vA}{\Type}\SC

809\lam{\vA}{\Type}\SC

795\lam{\va}{\vA}\SC

810\lam{\va}{\vA}\SC

796\va

811\va

797−}

798&

812&

799\langle\rangle\\

813\langle\rangle\\

800

814

papers/impl-paper/hll.tex+1−1

@@ -221,7 +221,7 @@ index : {a:Type} -> {n:Nat} -> Fin n -> Vect n a -> a

221Implicit arguments, given in braces \texttt{\{\}} in the type signature, are

222not given in applications of \texttt{index}; their values can be inferred from

223the types of the \texttt{Fin n} and \texttt{Vect n a} arguments. Any name which

224−appears as a parameter or index in a type signature, but which is otherwise

224+appears in a non-function position in a type signature, but which is otherwise

225free, will be automatically bound as an implicit argument. Implicit arguments

226can still be given explicitly in applications, using the syntax

227\texttt{\{a=value\}} and \texttt{\{n=value\}}, for example:

papers/impl-paper/impldtp.tex+2−1

@@ -132,7 +132,8 @@ level language constructs.

132

133This work was funded by the Scottish Informatics and Computer Science Alliance

134(SICSA) and by EU Framework 7 Project No. 248828 (ADVANCE). My thanks to

135−Philip H\"{o}lzenspies, Kevin Hammond, Vilhelm Sj\"{o}berg and Falko Spiller

135+Philip H\"{o}lzenspies, Kevin Hammond, Vilhelm Sj\"{o}berg, Falko Spiller

136+and Nathan Collins

136for their comments on an earlier draft of this paper, and to the anonymous

137for their comments on an earlier draft of this paper, and to the anonymous

137referees for their many insightful and constructive comments.

138referees for their many insightful and constructive comments.

138

139

papers/impl-paper/macros.ltx+1−1

@@ -408,7 +408,7 @@ Program & Version & Instructions & Thunks & Memory Accesses & Cells \\

408\newcommand{\pat}[2]{\RW{var}\:#1\pad{\!}{:}#2}

409\newcommand{\pty}[2]{\RW{pty}\:#1\pad{\!}{:}#2}

410\newcommand{\hole}[2]{?#1\pad{\!}{:}#2}

411−\newcommand{\guess}[3]{?#1\pad{\!}{:}#2\approx#3}

411+\newcommand{\guess}[3]{?#1\pad{\!}\approx#3{:}#2}

412\newcommand{\remlam}[2]{\lambda\{#1\pad{\!}{:}#2\}}

413\newcommand{\remall}[2]{\forall\{#1\pad{\!}{:}#2\}}

414\newcommand{\allpi}[2]{\Pi#1\pad{\!}{:}#2}