ebcb29b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Added proof script traces for pasting into program

ebcb29bEdwin Brady15 years ago

src/Core/CoreParser.hs+1−1

compare with master

unifiedsplit

@@ -21,7 +21,7 @@ idrisDef = haskellDef {

21 reservedNames = ["let", "in", "data", "Set", -- "if", "then", "else",

22 "do", "dsl", "import", "return", "refl",

23 "infix", "infixl", "infixr", "prefix",

24− "where", "with", "forall", "syntax",

24+ "where", "with", "forall", "syntax", "proof",

25 "using", "params", "namespace",

26 "Int", "Float", "Char", "String", "Ptr"]

27 }

src/Idris/AbsSyntax.hs+3

@@ -214,6 +214,7 @@ data PTerm = PQuote Raw

214 | PDoBlock [PDo]

215 | PReturn FC

216 | PMetavar Name

217+ | PProof [PTactic]

217 | PElabError String -- error to report on elaboration

218 | PElabError String -- error to report on elaboration

218 deriving Eq

219 deriving Eq

219

220

@@ -222,6 +223,7 @@ data PTactic = Intro [Name]

222 | Exact PTerm

223 | Exact PTerm

223 | Solve

224 | Solve

224 | Attack

225 | Attack

226+ | ProofState | ProofTerm

225 | Qed

227 | Qed

226 deriving (Show, Eq)

228 deriving (Show, Eq)

227

229

@@ -358,6 +360,7 @@ showImp impl tm = se 10 tm where

358 se p (PDPair _ l r) = "(" ++ se 10 l ++ " ** " ++ se 10 r ++ ")"

360 se p (PDPair _ l r) = "(" ++ se 10 l ++ " ** " ++ se 10 r ++ ")"

359 se p PSet = "Set"

361 se p PSet = "Set"

360 se p (PConstant c) = show c

362 se p (PConstant c) = show c

363+ se p (PProof ts) = "proof { " ++ show ts ++ "}"

361 se p (PMetavar n) = "?" ++ show n

364 se p (PMetavar n) = "?" ++ show n

362 se p Placeholder = "_"

365 se p Placeholder = "_"

363

366

src/Idris/ElabDecls.hs+3−1

@@ -388,6 +388,7 @@ elab info pattern tm = do elab' tm

388 elab' Placeholder = do (h : hs) <- get_holes

389 movelast h

390 elab' (PMetavar n) = do attack; defer n; solve

391+ elab' (PProof ts) = do mapM_ runTac ts

391 elab' (PElabError e) = fail e

392 elab' (PElabError e) = fail e

392 elab' x = fail $ "Not implemented " ++ show x

393 elab' x = fail $ "Not implemented " ++ show x

393

394

@@ -423,7 +424,8 @@ collectDeferred t = return t

423

424

424runTac :: PTactic -> Elab ()

425runTac :: PTactic -> Elab ()

425runTac (Intro xs) = mapM_ (\x -> do attack; intro x) xs

426runTac (Intro xs) = mapM_ (\x -> do attack; intro x) xs

426−runTac (Exact tm) = elab toplevel False tm

427+runTac (Exact tm) = do elab toplevel False tm

428+ try solve (return ())

427runTac Solve = solve

429runTac Solve = solve

428runTac x = fail $ "Not implemented " ++ show x

430runTac x = fail $ "Not implemented " ++ show x

429

431

src/Idris/Parser.hs+8

@@ -329,6 +329,10 @@ pSimpleExpr syn =

329 <|> do lchar '?'; x <- pName; return (PMetavar x)

330 <|> do reserved "refl"; fc <- pfc; return (PRefl fc)

331 <|> do reserved "return"; fc <- pfc; return (PReturn fc)

332+ <|> do reserved "proof"; lchar '{';

333+ ts <- endBy (pTactic syn) (lchar ';')

334+ lchar '}'

335+ return (PProof ts)

332 <|> try (do x <- pfName; fc <- pfc; return (PRef fc x))

336 <|> try (do x <- pfName; fc <- pfc; return (PRef fc x))

333 <|> try (pPair syn)

337 <|> try (pPair syn)

334 <|> try (do lchar '('; e <- pExpr syn; lchar ')'; return e)

338 <|> try (do lchar '('; e <- pExpr syn; lchar ')'; return e)

@@ -597,6 +601,10 @@ pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')

597 return Solve

601 return Solve

598 <|> do reserved "attack"

602 <|> do reserved "attack"

599 return Attack

603 return Attack

604+ <|> do reserved "state"

605+ return ProofState

606+ <|> do reserved "term"

607+ return ProofTerm

600 <|> do reserved "qed"

608 <|> do reserved "qed"

601 return Qed

609 return Qed

602

610

src/Idris/Prover.hs+29−13

@@ -24,11 +24,17 @@ prover x = do ctxt <- getContext

24 else fail $ show x ++ " is not a metavariable"

25 _ -> fail "No such metavariable"

27+dumpProof :: Name -> [String] -> IO ()

28+dumpProof n ps = do putStrLn $ show n ++ " = proof {"

29+ mapM_ (\x -> putStrLn $ " " ++ x ++ ";") ps

30+ putStrLn "};\n"

31+

27prove :: Context -> Name -> Type -> Idris ()

32prove :: Context -> Name -> Type -> Idris ()

28prove ctxt n ty

33prove ctxt n ty

29 = do let ps = initElaborator n ctxt ty

34 = do let ps = initElaborator n ctxt ty

30− tm <- ploop True ("-" ++ show n) (ps, "")

35+ (tm, prf) <- ploop True ("-" ++ show n) [] (ps, "")

31 iLOG $ "Adding " ++ show tm

36 iLOG $ "Adding " ++ show tm

37+ lift $ dumpProof n prf

32 let tree = simpleCase False [(P Ref n ty, tm)]

38 let tree = simpleCase False [(P Ref n ty, tm)]

33 logLvl 3 (show tree)

39 logLvl 3 (show tree)

34 (ptm, pty) <- tclift $ recheck ctxt [] tm

40 (ptm, pty) <- tclift $ recheck ctxt [] tm

@@ -65,27 +71,37 @@ dumpState ist ps@(PS nm (h:hs) _ tm _ _ i _ cyxy _ _)

65 showG (Guess t v) = tshow t ++ " =?= " ++ tshow v

71 showG (Guess t v) = tshow t ++ " =?= " ++ tshow v

66 showG b = tshow (binderTy b)

72 showG b = tshow (binderTy b)

74+lifte :: ElabState -> Elab a -> Idris a

75+lifte st e = do (v, _) <- elabStep st e

76+ return v

77+

68−ploop :: Bool -> String -> ElabState -> Idris Term

78+ploop :: Bool -> String -> [String] -> ElabState -> Idris (Term, [String])

69−ploop d prompt e

79+ploop d prompt prf e

70 = do i <- get

80 = do i <- get

71 when d $ lift $ dumpState i (proof e)

81 when d $ lift $ dumpState i (proof e)

72 x <- lift $ readline (prompt ++ "> ")

82 x <- lift $ readline (prompt ++ "> ")

73− cmd <- case x of

83+ (cmd, step) <- case x of

74 Nothing -> fail "Abandoned"

84 Nothing -> fail "Abandoned"

75 Just input -> do lift $ addHistory input

85 Just input -> do lift $ addHistory input

76− return (parseTac i input)

86+ return (parseTac i input, input)

77− (d, st, done) <- idrisCatch

87+ (d, st, done, prf') <- idrisCatch

78 (case cmd of

88 (case cmd of

79 Left err -> do iputStrLn (show err)

89 Left err -> do iputStrLn (show err)

80− return (False, e, False)

90+ return (False, e, False, prf)

91+ Right ProofState ->

92+ return (True, e, False, prf)

93+ Right ProofTerm ->

94+ do tm <- lifte e get_term

95+ iputStrLn $ "TT: " ++ show tm ++ "\n"

96+ return (False, e, False, prf)

81− Right Qed -> do (hs, _) <- elabStep e get_holes

97+ Right Qed -> do hs <- lifte e get_holes

82 when (not (null hs)) $ fail "Incomplete proof"

98 when (not (null hs)) $ fail "Incomplete proof"

83− return (False, e, True)

99+ return (False, e, True, prf)

84 Right tac -> do (_, st) <- elabStep e (runTac tac)

100 Right tac -> do (_, st) <- elabStep e (runTac tac)

85− return (True, st, False))

101+ return (True, st, False, prf ++ [step]))

86 (\err -> do iputStrLn (report err)

102 (\err -> do iputStrLn (report err)

87− return (False, e, False))

103+ return (False, e, False, prf))

88 if done then do (tm, _) <- elabStep st get_term

104 if done then do (tm, _) <- elabStep st get_term

89− return tm

105+ return (tm, prf')

90− else ploop d prompt st

106+ else ploop d prompt prf' st

107