cc0dc09 · Idris-dev · git.iko.soy

impl-paper/overview.tex+2−1

compare with master

unifiedsplit

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

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

11\begin{itemize}

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

13− indices becomes tricky.

13+ indices becomes tricky. Instead: global names, local names during construction,

14+ and de Bruijn indices when done.

14\end{itemize}

15\end{itemize}

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

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

16\item An Elaborator, as an EDSL

17\item An Elaborator, as an EDSL

miniidris.cabal+1−1

@@ -19,7 +19,7 @@ Executable miniidris

19 hs-source-dirs: src

20 Other-modules: Core, Evaluate, Typecheck, ProofState,

21 ProofState, CoreParser, ShellParser,

22− Unify

22+ Unify, Elaborate

23

24 Build-depends: base>=4 && <5, parsec, mtl, Cabal, readline

25

src/Elaborate.hsnew file+89

@@ -0,0 +1,89 @@

1+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}

2+

3+{- A high level language of tactic composition, for building

4+ elaborators from a high level language into the core theory.

5+

6+ This is our interface to proof construction, rather than

7+ ProofState, because this gives us a language to build derived

8+ tactics out of the primitives.

9+-}

10+

11+module Elaborate(module Elaborate, module ProofState) where

12+

13+import ProofState

14+import Core

15+import Evaluate

16+

17+-- I don't really want this here, but it's useful for the test shell

18+data Command = Theorem Name Raw

19+ | Eval Raw

20+ | Quit

21+ | Print Name

22+ | Tac Elab

23+

24+type Elab = ProofState -> TC (ProofState, String)

25+

26+initElaborator :: Name -> Context -> Type -> ProofState

27+initElaborator = newProof

28+

29+-- The primitives, from ProofState

30+

31+attack :: Elab

32+attack = processTactic Attack

33+

34+claim :: Name -> Raw -> Elab

35+claim n t = processTactic (Claim n t)

36+

37+fill :: Raw -> Elab

38+fill t = processTactic (Fill t)

39+

40+unify_fill :: Raw -> Elab

41+unify_fill t = processTactic (UnifyFill t)

42+

43+solve :: Elab

44+solve = processTactic Solve

45+

46+regret :: Elab

47+regret = processTactic Regret

48+

49+compute :: Elab

50+compute = processTactic Compute

51+

52+eval_in :: Raw -> Elab

53+eval_in t = processTactic (EvalIn t)

54+

55+check_in :: Raw -> Elab

56+check_in t = processTactic (CheckIn t)

57+

58+intro :: Name -> Elab

59+intro n = processTactic (Intro n)

60+

61+forall :: Name -> Raw -> Elab

62+forall n t = processTactic (Forall n t)

63+

64+focus :: Name -> Elab

65+focus n = processTactic (Focus n)

66+

67+proofstate :: Elab

68+proofstate = processTactic ProofState

69+

70+qed :: Elab

71+qed = processTactic QED

72+

73+-- Some combinators on elaborations

74+

75+-- Sequencing

76+infixr 5 ==>

77+

78+(==>) :: Elab -> Elab -> Elab

79+(==>) t1 t2 ps = do (ps', log') <- t1 ps

80+ (ps'', log'') <- t2 ps'

81+ return (ps'', log' ++ log')

82+

83+-- Try a tactic, if it fails, try another

84+try :: Elab -> Elab -> Elab

85+try t1 t2 ps = case t1 ps of

86+ OK v -> return v

87+ _ -> t2 ps

88+

89+

src/Main.hs−1

@@ -4,7 +4,6 @@ import CoreParser

4import ShellParser

5import Core

6import Typecheck

7−import ProofState

8import ProofShell

7import ProofShell

9

8

10main = do f <- readFile "test.mi"

9main = do f <- readFile "test.mi"

src/ProofShell.hs+3−3

@@ -5,8 +5,8 @@ module ProofShell where

5import Typecheck

6import Evaluate

7import Core

8−import ProofState

9import ShellParser

8import ShellParser

9+import Elaborate

10

11import Control.Monad.State

12import System.Console.Readline

@@ -38,8 +38,8 @@ processCommand (Print n) state =

38 case lookupDef n (ctxt state) of

39 Just tm -> (state, show tm)

40 Nothing -> (state, "No such name")

41−processCommand (Tac t) state

41+processCommand (Tac e) state

42− | Just ps <- prf state = case processTactic t ps of

42+ | Just ps <- prf state = case e ps of

43 OK (ps', resp) ->

44 if (not (done ps'))

45 then (state { prf = Just ps' }, resp)

src/ProofState.hs+17−9

@@ -1,6 +1,11 @@

1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}

2

3+{- Implements a proof state, some primitive tactics for manipulating

4+ proofs, and some high level commands for introducing new theorems,

5+ evaluation/checking inside the proof system, etc. --}

6+

3−module ProofState where

7+module ProofState(ProofState(..), newProof,

8+ Tactic(..), processTactic) where

4

9

5import Typecheck

10import Typecheck

6import Evaluate

11import Evaluate

@@ -25,12 +30,6 @@ data Goal = GD { premises :: Env,

25 goalType :: Binder Term

30 goalType :: Binder Term

26 }

31 }

27

32

28−data Command = Theorem Name Raw

29− | Eval Raw

30− | Quit

31− | Print Name

32− | Tac Tactic

33−

34data Tactic = Attack

33data Tactic = Attack

35 | Claim Name Raw

34 | Claim Name Raw

36 | Fill Raw

35 | Fill Raw

@@ -41,6 +40,7 @@ data Tactic = Attack

41 | EvalIn Raw

40 | EvalIn Raw

42 | CheckIn Raw

41 | CheckIn Raw

43 | Intro Name

42 | Intro Name

43+ | Forall Name Raw

44 | Focus Name

45 | ProofState

46 | QED

@@ -154,6 +154,7 @@ focus :: Name -> RunTactic

154focus n ctxt env t = do action (FocusGoal n)

155 return t

156

157+-- Hmmm. YAGNI?

157regret :: RunTactic

158regret :: RunTactic

158regret = undefined

159regret = undefined

159

160

@@ -194,6 +195,14 @@ intro n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

194 _ -> fail "Nothing to introduce"

195 _ -> fail "Nothing to introduce"

195intro ctxt env _ _ = fail "Can't introduce here."

196intro ctxt env _ _ = fail "Can't introduce here."

196

197

198+forall :: Name -> Raw -> RunTactic

199+forall n ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

200+ do (tyv, tyt) <- lift $ check ctxt env ty

201+ lift $ isSet ctxt env tyt

202+ lift $ isSet ctxt env t

203+ return $ Bind n (Pi tyv) (Bind x (Hole t) (P Bound x t))

204+

205+

197compute :: RunTactic

206compute :: RunTactic

198compute ctxt env (Bind x (Hole ty) sc) =

207compute ctxt env (Bind x (Hole ty) sc) =

199 do return $ Bind x (Hole (normalise ctxt env ty)) sc

208 do return $ Bind x (Hole (normalise ctxt env ty)) sc

@@ -256,8 +265,6 @@ processTactic t ps

256 updateSolved xs (App f a) = App (updateSolved xs f) (updateSolved xs a)

265 updateSolved xs (App f a) = App (updateSolved xs f) (updateSolved xs a)

257 updateSolved xs t = t

266 updateSolved xs t = t

258

267

259−

260−

261process :: Tactic -> Name -> ProofState -> StateT TState TC ProofState

268process :: Tactic -> Name -> ProofState -> StateT TState TC ProofState

262process t h ps = tactic (Just h) ps (context ps) (mktac t)

269process t h ps = tactic (Just h) ps (context ps) (mktac t)

263 where mktac Attack = attack

270 where mktac Attack = attack

@@ -268,6 +275,7 @@ process t h ps = tactic (Just h) ps (context ps) (mktac t)

268 mktac Solve = solve

275 mktac Solve = solve

269 mktac Compute = compute

276 mktac Compute = compute

270 mktac (Intro n) = intro n

277 mktac (Intro n) = intro n

278+ mktac (Forall n t) = forall n t

271 mktac (CheckIn r) = check_in r

279 mktac (CheckIn r) = check_in r

272 mktac (EvalIn r) = eval_in r

280 mktac (EvalIn r) = eval_in r

273 mktac (Focus n) = focus n

281 mktac (Focus n) = focus n

src/ShellParser.hs+17−15

@@ -3,7 +3,7 @@

3module ShellParser(parseCommand, parseTactic) where

4

5import Core

6−import ProofState

6+import Elaborate

7import CoreParser

8

9import Text.ParserCombinators.Parsec

@@ -43,20 +43,22 @@ pCommand = do reserved "theorem"; n <- iName; lchar ':'; ty <- pTerm

43 <|> do reserved "quit";

44 return Quit

45

46−pTactic :: Parser Tactic

46+pTactic :: Parser Elab

47−pTactic = do reserved "attack"; return Attack

47+pTactic = do reserved "attack"; return attack

48 <|> do reserved "claim"; n <- iName; lchar ':'; ty <- pTerm

49− return (Claim n ty)

49+ return (claim n ty)

50− <|> do reserved "regret"; return Regret

50+ <|> do reserved "regret"; return regret

51− <|> do reserved "fill"; tm <- pTerm; return (Fill tm)

51+ <|> do reserved "fill"; tm <- pTerm; return (fill tm)

52− <|> do reserved "unify"; tm <- pTerm; return (UnifyFill tm)

52+ <|> do reserved "unify"; tm <- pTerm; return (unify_fill tm)

53− <|> do reserved "solve"; return Solve

53+ <|> do reserved "solve"; return solve

54− <|> do reserved "compute"; return Compute

54+ <|> do reserved "compute"; return compute

55− <|> do reserved "intro"; n <- iName; return (Intro n)

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

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

57+ return (forall n ty)

56− <|> do reserved "eval"; t <- pTerm; return (EvalIn t)

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

57− <|> do reserved "check"; t <- pTerm; return (CheckIn t)

59+ <|> do reserved "check"; t <- pTerm; return (check_in t)

58− <|> do reserved "focus"; n <- iName; return (Focus n)

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

59− <|> do reserved "state"; return ProofState

61+ <|> do reserved "state"; return proofstate

60− <|> do reserved "qed"; return QED

62+ <|> do reserved "qed"; return qed

61

63

62

64