ffd5e72 · Idris-dev · git.iko.soy

impl-paper/intro.tex+9

compare with master

unifiedsplit

@@ -11,3 +11,12 @@ in the core type theory of \Epigram{}~\cite{view-left} and compiling them

11efficiently (i.e. making the language implementation practical) this paper is

12about making the language itself practical.

13

14+\subsection{Some Goals}

15+

16+\begin{itemize}

17+\item Type checking dependent types~\cite{epireloaded,lambdapi} is just one component

18+ of a language. There is folklore about what to do to turn it into a language. This

19+ paper aims to help language implementers avoid working things out for themselves.

20+\item What's the difference between a theorem prover and a practical systems programming

21+ language? Not much...

22+\end{itemize}

impl-paper/literature.bib+9

@@ -1,3 +1,12 @@

1+@article{lambdapi,

2+ author = {Andres L\"{o}h and Conor McBride and Wouter Swierstra},

3+ title = {A tutorial implementation of a dependently typed lambda calculus},

4+ year = 2010,

5+ journal = {Fundamenta Informaticae},

6+ volume = 102,

7+ number = 2

8+}

9+

1@article{idioms,

10@article{idioms,

2 author = {McBride, Conor and Paterson, Ross},

11 author = {McBride, Conor and Paterson, Ross},

3 title = {Applicative programming with effects},

12 title = {Applicative programming with effects},

impl-paper/overview.tex+7−1

@@ -7,6 +7,11 @@ High level view of steps we've taken to implement this new version:

7\item An evaluator for well-typed terms

8\item The important bit: a simple type checker. No unification or

9 inference.

10+\begin{itemize}

11+ \item It is extremely tempting to add implicit arguments and unification to the

12+ type checker. This is what I did in the first Idris prototype: I learned

13+ that it was a bad idea! Scope is a big problem.

14+\end{itemize}

10\item The proof state and a tactic engine (Oleg style~\cite{mcbride-thesis}).

15\item The proof state and a tactic engine (Oleg style~\cite{mcbride-thesis}).

11\begin{itemize}

16\begin{itemize}

12 \item Dealing with names: typechecking and evaluation in a context, managing de Bruijn

17 \item Dealing with names: typechecking and evaluation in a context, managing de Bruijn

@@ -14,7 +19,8 @@ High level view of steps we've taken to implement this new version:

14 and de Bruijn indices when done.

19 and de Bruijn indices when done.

15\end{itemize}

20\end{itemize}

16\item Unification, and incorporation into the tactic engine.

21\item Unification, and incorporation into the tactic engine.

17−\item An Elaborator, as an EDSL

22+\item An Elaborator, as an EDSL, which is a language for applying primitive tactics and

23+ constructing derived tactics.

18\end{itemize}

24\end{itemize}

19

25

20For the high level language: we need nothing more than the core type theory,

26For the high level language: we need nothing more than the core type theory,

src/Elaborate.hs+7

@@ -154,6 +154,13 @@ apply fn imps =

154 do args <- prepare_apply fn imps

155 unify_fill (raw_apply fn (map Var args))

156

157+-- Abstract over an argument of unknown type, giving a name for the hole

158+-- which we'll fill with the argument type too.

159+arg :: Name -> Name -> Elab ()

160+arg n tyhole = do ty <- unique_hole tyhole

161+ claim ty (RSet 0)

162+ forall n (Var ty)

163+

157-- Some combinators on elaborations

164-- Some combinators on elaborations

158

165

159-- Sequencing

166-- Sequencing

src/ProofState.hs+4−2

@@ -272,8 +272,10 @@ processTactic t ps

272 goals g [] = g

273 goals g (AddGoal n : xs) = goals (n : g) xs

274 goals (g:gs) (NextGoal n : xs) = goals (g : n : gs) xs

275− goals g (FocusGoal n : xs) = goals (n : (g \\ [n])) xs

275+ goals g (FocusGoal n : xs)

276+ | n `elem` g = goals (n : (g \\ [n])) xs

276− goals g (MoveGoal n : xs) = goals ((g \\ [n]) ++ [n]) xs

277+ goals g (MoveGoal n : xs)

278+ | n `elem` g = goals ((g \\ [n]) ++ [n]) xs

277 goals g (Solved n : xs) = goals (g \\ [n]) xs

279 goals g (Solved n : xs) = goals (g \\ [n]) xs

278 goals g (AlsoSolved n tm : xs) = goals (g \\ [n]) xs

280 goals g (AlsoSolved n tm : xs) = goals (g \\ [n]) xs

279 goals g (_ : xs) = goals g xs

281 goals g (_ : xs) = goals g xs

src/ShellParser.hs+1

@@ -57,6 +57,7 @@ pTactic = do reserved "attack"; return attack

57 <|> do reserved "intro"; n <- iName; return (intro n)

58 <|> do reserved "forall"; n <- iName; lchar ':'; ty <- pTerm

59 return (forall n ty)

60+ <|> do reserved "arg"; n <- iName; t <- iName; return (arg n t)

60 <|> do reserved "patvar"; n <- iName; lchar ':'; ty <- pTerm

61 <|> do reserved "patvar"; n <- iName; lchar ':'; ty <- pTerm

61 return (patvar n ty)

62 return (patvar n ty)

62 <|> do reserved "eval"; t <- pTerm; return (eval_in t)

63 <|> do reserved "eval"; t <- pTerm; return (eval_in t)

src/Typecheck.hs+1−1

@@ -43,7 +43,7 @@ check ctxt env (RApp f a)

43 return (App fv av,

44 normalise ctxt env (Bind x (Let aty av) t))

45 t -> fail "Can't apply a non-function type"

46−check ctxt env (RSet i) = return (Set i, Set (i+1))

46+check ctxt env (RSet i) = return (Set i, Set i) -- LATER: (i+1))

47check ctxt env (RBind n b sc)

48 = do b' <- checkBinder b

49 (scv, sct) <- check ctxt ((n, b'):env) sc

src/Unify.hs+4

@@ -28,6 +28,10 @@ unify ctxt env x y

28

29 un' bnames x@(App _ _) y@(App _ _)

30 = uApp bnames (unApply x) (unApply y)

31+ un' bnames x (Bind n (Lam t) (App y (P Bound n' _)))

32+ | n == n' = un' bnames x y

33+ un' bnames (Bind n (Lam t) (App x (P Bound n' _))) y

34+ | n == n' = un' bnames x y

31 un' bnames (Bind x bx sx) (Bind y by sy)

35 un' bnames (Bind x bx sx) (Bind y by sy)

32 = do h1 <- uB bnames bx by

36 = do h1 <- uB bnames bx by

33 h2 <- un' ((x,y):bnames) sx sy

37 h2 <- un' ((x,y):bnames) sx sy