cc0dc09 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Added elaborate; a language for composing primitive tactics.

commitcc0dc0925dc9f8458cf5bcb4300889f442b13d2d authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateTue 27 Sep 2011, 17:50 (15 years ago) parentcbc60eb

7 files changed+129−30

compare with master

unifiedsplit

impl-paper/overview.tex+2−1 miniidris.cabal+1−1 src/Elaborate.hs+89 src/Main.hs−1 src/ProofShell.hs+3−3 src/ProofState.hs+17−9 src/ShellParser.hs+17−15

impl-paper/overview.tex+2−1

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

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

1111\begin{itemize}

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

1415\end{itemize}

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

1617\item An Elaborator, as an EDSL

miniidris.cabal+1−1

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

1919 hs-source-dirs: src

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

2121 ProofState, CoreParser, ShellParser,

22− Unify

22+ Unify, Elaborate

2323

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

2525

src/Elaborate.hsnew file+89

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

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

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

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

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

44import ShellParser

55import Core

66import Typecheck

7−import ProofState

87import ProofShell

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

src/ProofShell.hs+3−3

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

55import Typecheck

66import Evaluate

77import Core

8−import ProofState

98import ShellParser

9+import Elaborate

1010

1111import Control.Monad.State

1212import System.Console.Readline

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

3838 case lookupDef n (ctxt state) of

3939 Just tm -> (state, show tm)

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

41−processCommand (Tac t) state

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

41+processCommand (Tac e) state

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

4343 OK (ps', resp) ->

4444 if (not (done ps'))

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

src/ProofState.hs+17−9

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

11{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}

3−module ProofState where

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

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

8+ Tactic(..), processTactic) where

510import Typecheck

611import Evaluate

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

2530 goalType :: Binder Term

2631 }

2732

28−data Command = Theorem Name Raw

29− | Eval Raw

30− | Quit

31− | Print Name

32− | Tac Tactic

33−

3433data Tactic = Attack

3534 | Claim Name Raw

3635 | Fill Raw

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

4140 | EvalIn Raw

4241 | CheckIn Raw

4342 | Intro Name

43+ | Forall Name Raw

4444 | Focus Name

4545 | ProofState

4646 | QED

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

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

155155 return t

156156

157+-- Hmmm. YAGNI?

157158regret :: RunTactic

158159regret = undefined

159160

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

194195 _ -> fail "Nothing to introduce"

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

196197

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+

197206compute :: RunTactic

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

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

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

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

257266 updateSolved xs t = t

258267

259−

260−

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

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

263270 where mktac Attack = attack

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

268275 mktac Solve = solve

269276 mktac Compute = compute

270277 mktac (Intro n) = intro n

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

271279 mktac (CheckIn r) = check_in r

272280 mktac (EvalIn r) = eval_in r

273281 mktac (Focus n) = focus n

src/ShellParser.hs+17−15

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

33module ShellParser(parseCommand, parseTactic) where

55import Core

6−import ProofState

6+import Elaborate

77import CoreParser

99import Text.ParserCombinators.Parsec

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

4343 <|> do reserved "quit";

4444 return Quit

4545

46−pTactic :: Parser Tactic

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

46+pTactic :: Parser Elab

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

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

49− return (Claim n ty)

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

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

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

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

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

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

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

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

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

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

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

49+ return (claim n ty)

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

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

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

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

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

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

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

57+ return (forall n ty)

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

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

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

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

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

6163

6264