ffd5e72 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

arg tactic; unification tweak

commitffd5e7291c55770ff4d73f8649f1dd578cd540b4 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateWed 28 Sep 2011, 14:34 (15 years ago) parent07f3b19

8 files changed+42−4

compare with master

unifiedsplit

impl-paper/intro.tex+9 impl-paper/literature.bib+9 impl-paper/overview.tex+7−1 src/Elaborate.hs+7 src/ProofState.hs+4−2 src/ShellParser.hs+1 src/Typecheck.hs+1−1 src/Unify.hs+4

impl-paper/intro.tex+9

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

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

1212about making the language itself practical.

1313

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+}

110@article{idioms,

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

312 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:

77\item An evaluator for well-typed terms

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

99 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}

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

1116\begin{itemize}

1217 \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:

1419 and de Bruijn indices when done.

1520\end{itemize}

1621\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.

1824\end{itemize}

1925

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

src/Elaborate.hs+7

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

154154 do args <- prepare_apply fn imps

155155 unify_fill (raw_apply fn (map Var args))

156156

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+

157164-- Some combinators on elaborations

158165

159166-- Sequencing

src/ProofState.hs+4−2

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

272272 goals g [] = g

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

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

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

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

275+ goals g (FocusGoal n : xs)

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

277+ goals g (MoveGoal n : xs)

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

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

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

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

src/ShellParser.hs+1

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

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

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

5959 return (forall n ty)

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

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

6162 return (patvar n ty)

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

src/Typecheck.hs+1−1

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

4343 return (App fv av,

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

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

4747check ctxt env (RBind n b sc)

4848 = do b' <- checkBinder b

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

src/Unify.hs+4

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

2828

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

3030 = 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

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

3236 = do h1 <- uB bnames bx by

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