ebcb29b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Added proof script traces for pasting into program

commitebcb29b4eee62de93fe9200b31eb7189a9b0a459 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateSun 30 Oct 2011, 14:49 (15 years ago) parent551548c

5 files changed+44−15

compare with master

unifiedsplit

src/Core/CoreParser.hs+1−1 src/Idris/AbsSyntax.hs+3 src/Idris/ElabDecls.hs+3−1 src/Idris/Parser.hs+8 src/Idris/Prover.hs+29−13

src/Core/CoreParser.hs+1−1

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

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

2222 "do", "dsl", "import", "return", "refl",

2323 "infix", "infixl", "infixr", "prefix",

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

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

2525 "using", "params", "namespace",

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

2727 }

src/Idris/AbsSyntax.hs+3

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

214214 | PDoBlock [PDo]

215215 | PReturn FC

216216 | PMetavar Name

217+ | PProof [PTactic]

217218 | PElabError String -- error to report on elaboration

218219 deriving Eq

219220

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

222223 | Exact PTerm

223224 | Solve

224225 | Attack

226+ | ProofState | ProofTerm

225227 | Qed

226228 deriving (Show, Eq)

227229

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

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

359361 se p PSet = "Set"

360362 se p (PConstant c) = show c

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

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

362365 se p Placeholder = "_"

363366

src/Idris/ElabDecls.hs+3−1

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

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

389389 movelast h

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

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

391392 elab' (PElabError e) = fail e

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

393394

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

423424

424425runTac :: PTactic -> Elab ()

425426runTac (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 ())

427429runTac Solve = solve

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

429431

src/Idris/Parser.hs+8

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

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

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

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

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

333337 <|> try (pPair syn)

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

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

597601 return Solve

598602 <|> do reserved "attack"

599603 return Attack

604+ <|> do reserved "state"

605+ return ProofState

606+ <|> do reserved "term"

607+ return ProofTerm

600608 <|> do reserved "qed"

601609 return Qed

602610

src/Idris/Prover.hs+29−13

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

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

2525 _ -> fail "No such metavariable"

2626

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

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

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

30+ putStrLn "};\n"

31+

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

2833prove ctxt n ty

2934 = do let ps = initElaborator n ctxt ty

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

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

3136 iLOG $ "Adding " ++ show tm

37+ lift $ dumpProof n prf

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

3339 logLvl 3 (show tree)

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

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

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

6672 showG b = tshow (binderTy b)

6773

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

69−ploop d prompt e

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

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

76+ return v

77+

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

79+ploop d prompt prf e

7080 = do i <- get

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

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

73− cmd <- case x of

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

7484 Nothing -> fail "Abandoned"

7585 Just input -> do lift $ addHistory input

76− return (parseTac i input)

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

86+ return (parseTac i input, input)

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

7888 (case cmd of

7989 Left err -> do iputStrLn (show err)

80− return (False, e, False)

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

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)

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

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

83− return (False, e, True)

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

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

85− return (True, st, False))

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

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

87− return (False, e, False))

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

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

89− return tm

90− else ploop d prompt st

105+ return (tm, prf')

106+ else ploop d prompt prf' st

91107