551548c · Idris-dev · git.iko.soy

miniidris.cabal+1−1

compare with master

unifiedsplit

@@ -28,7 +28,7 @@ Executable miniidris

28 Idris.AbsSyntax, Idris.Parser, Idris.REPL,

29 Idris.REPLParser, Idris.ElabDecls, Idris.Error,

30 Idris.Delaborate, Idris.Primitives, Idris.Imports,

31− Idris.Compiler

31+ Idris.Compiler, Idris.Prover

32

33 Paths_miniidris

34

src/Core/Elaborate.hs+5−1

@@ -30,6 +30,9 @@ data Command = Theorem Name Raw

30type ElabState = (ProofState, String)

31type Elab a = StateT ElabState TC a

32

33+proof :: ElabState -> ProofState

34+proof = fst

35+

33erun :: FC -> Elab a -> Elab a

36erun :: FC -> Elab a -> Elab a

34erun f elab = do s <- get

37erun f elab = do s <- get

35 case runStateT elab s of

38 case runStateT elab s of

@@ -81,7 +84,8 @@ get_holes = do (p, _) <- get

81-- get the current goal type

84-- get the current goal type

82goal :: Elab Type

85goal :: Elab Type

83goal = do (p, _) <- get

86goal = do (p, _) <- get

84− lift $ goalAtFocus p

87+ b <- lift $ goalAtFocus p

88+ return (binderTy b)

85

89

86-- typecheck locally

90-- typecheck locally

87get_type :: Raw -> Elab Type

91get_type :: Raw -> Elab Type

src/Core/ProofState.hs+4−4

@@ -5,7 +5,7 @@

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

6

7module Core.ProofState(ProofState(..), newProof, envAtFocus, goalAtFocus,

8− Tactic(..), processTactic) where

8+ Tactic(..), Goal(..), processTactic) where

9

10import Core.Typecheck

11import Core.Evaluate

@@ -124,10 +124,10 @@ envAtFocus ps

124 return (premises g)

125 | otherwise = fail "No holes"

126

127−goalAtFocus :: ProofState -> TC Type

127+goalAtFocus :: ProofState -> TC (Binder Type)

128goalAtFocus ps

129 | not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps)

130− return (binderTy (goalType g))

130+ return (goalType g)

131

132goal :: Hole -> Term -> TC Goal

133goal h tm = g [] tm where

@@ -195,7 +195,7 @@ defer n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =

195 do action (\ps -> let hs = holes ps in

196 ps { holes = hs \\ [x] })

197 return (Bind n (GHole (mkTy (reverse env) t))

198− (mkApp (P nt n ty) (map getP (reverse env))))

198+ (mkApp (P Ref n ty) (map getP (reverse env))))

199 where

200 mkTy [] t = t

201 mkTy ((n,b) : bs) t = Bind n (Pi (binderTy b)) (mkTy bs t)

src/Idris/AbsSyntax.hs+10−1

@@ -47,6 +47,7 @@ idrisInit = IState emptyContext [] emptyContext emptyContext

47-- global state (hence the IO inner monad).

48type Idris a = StateT IState IO a

49

50+

50getContext :: Idris Context

51getContext :: Idris Context

51getContext = do i <- get; return (tt_ctxt i)

52getContext = do i <- get; return (tt_ctxt i)

52

53

@@ -118,7 +119,7 @@ setTypeCase t = do i <- get

118

119

119data Command = Quit | Help | Eval PTerm

120data Command = Quit | Help | Eval PTerm

120 | Compile String

121 | Compile String

121− | Metavars

122+ | Metavars | Prove Name

122 | TTShell

123 | TTShell

123 | LogLvl Int | Spec PTerm | HNF PTerm

124 | LogLvl Int | Spec PTerm | HNF PTerm

124 | NOP

125 | NOP

@@ -216,6 +217,14 @@ data PTerm = PQuote Raw

216 | PElabError String -- error to report on elaboration

217 | PElabError String -- error to report on elaboration

217 deriving Eq

218 deriving Eq

218

219

220+data PTactic = Intro [Name]

221+ | Refine Name

222+ | Exact PTerm

223+ | Solve

224+ | Attack

225+ | Qed

226+ deriving (Show, Eq)

227+

219data PDo = DoExp FC PTerm

228data PDo = DoExp FC PTerm

220 | DoBind FC Name PTerm

229 | DoBind FC Name PTerm

221 | DoLet FC Name PTerm

230 | DoLet FC Name PTerm

src/Idris/Delaborate.hs+7

@@ -46,3 +46,10 @@ delab ist tm = de [] tm

46 imp (PImp l n _) arg = PImp l n arg

47 imp (PExp l _) arg = PExp l arg

48

49+pshow :: IState -> Err -> String

50+pshow i (Msg s) = s

51+pshow i (CantUnify x y e) = "Can't unify " ++ show (delab i x)

52+ ++ " with " ++ show (delab i y)

53+ -- ++ "\n\t(" ++ pshow i e ++ ")"

54+pshow i (At f e) = show f ++ ":" ++ pshow i e

55+

src/Idris/ElabDecls.hs+11−3

@@ -9,7 +9,7 @@ import Idris.Imports

9import Paths_miniidris

10

11import Core.TT

12−import Core.Elaborate

12+import Core.Elaborate hiding (Tactic(..))

13import Core.Evaluate

14import Core.Typecheck

15import Core.CaseTree

@@ -122,13 +122,14 @@ elabClause info fc (PClause fname lhs withs rhs whereblock)

122 ((rhs', defer), _) <-

123 tclift $ elaborate ctxt (MN 0 "patRHS") clhsty

124 (do pbinds lhs_tm

125− (_, d) <- erun fc (build winfo False rhs)

125+ (_, _) <- erun fc (build winfo False rhs)

126 psolve lhs_tm

127 tt <- get_term

128− return (tt, d))

128+ return $ runState (collectDeferred tt) [])

129 logLvl 2 $ "---> " ++ show rhs'

130 when (not (null defer)) $ iLOG $ "DEFERRED " ++ show defer

131 addDeferred defer

132+ ctxt <- getContext

132 (crhs, crhsty) <- tclift $ recheck ctxt [] rhs'

133 (crhs, crhsty) <- tclift $ recheck ctxt [] rhs'

133 return (clhs, crhs)

134 return (clhs, crhs)

134 where

135 where

@@ -418,4 +419,11 @@ collectDeferred (Bind n b t) = do b' <- cdb b

418collectDeferred (App f a) = liftM2 App (collectDeferred f) (collectDeferred a)

419collectDeferred (App f a) = liftM2 App (collectDeferred f) (collectDeferred a)

419collectDeferred t = return t

420collectDeferred t = return t

420

421

422+-- Running tactics directly

423+

424+runTac :: PTactic -> Elab ()

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

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

427+runTac Solve = solve

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

421

429

src/Idris/Error.hs−7

@@ -23,13 +23,6 @@ liftCatch catchError m h =

23idrisCatch :: Idris a -> (IOError -> Idris a) -> Idris a

24idrisCatch op handler = liftCatch catch op handler

25

26−pshow :: IState -> Err -> String

27−pshow i (Msg s) = s

28−pshow i (CantUnify x y e) = "Can't unify " ++ show (delab i x)

29− ++ " with " ++ show (delab i y)

30− -- ++ "\n\t(" ++ pshow i e ++ ")"

31−pshow i (At f e) = show f ++ ":" ++ pshow i e

32−

33tclift :: Show a => TC a -> Idris a

26tclift :: Show a => TC a -> Idris a

34tclift tc = case tc of

27tclift tc = case tc of

35 OK v -> return v

28 OK v -> return v

src/Idris/Parser.hs+16

@@ -74,6 +74,7 @@ loadSource f = do iLOG ("Reading " ++ f)

74 return ()

75

76parseExpr i = runParser (pFullExpr defaultSyntax) i "(input)"

77+parseTac i = runParser (pTactic defaultSyntax) i "(proof)"

77

78

78parseImports :: FilePath -> String -> Idris ([String], String, SourcePos)

79parseImports :: FilePath -> String -> Idris ([String], String, SourcePos)

79parseImports fname input

80parseImports fname input

@@ -584,6 +585,21 @@ pWhereblock syn = do reserved "where"; lchar '{'

584 lchar '}';

585 lchar '}';

585 return $ concat ds

586 return $ concat ds

586

587

588+pTactic :: SyntaxInfo -> IParser PTactic

589+pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')

590+ return $ Intro ns

591+ <|> do reserved "refine"; n <- pName

592+ return $ Refine n

593+ <|> do reserved "exact"; t <- pExpr syn;

594+ i <- getState

595+ return $ Exact (desugar syn i t)

596+ <|> do reserved "solve"

597+ return Solve

598+ <|> do reserved "attack"

599+ return Attack

600+ <|> do reserved "qed"

601+ return Qed

602+

587-- Dealing with implicit arguments

603-- Dealing with implicit arguments

588

604

589implicit :: SyntaxInfo -> Name -> PTerm -> IParser PTerm

605implicit :: SyntaxInfo -> Name -> PTerm -> IParser PTerm

src/Idris/Prover.hsnew file+91

@@ -0,0 +1,91 @@

1+module Idris.Prover where

2+

3+import Core.Elaborate hiding (Tactic(..))

4+import Core.TT

5+import Core.Evaluate

6+import Core.CaseTree

7+import Core.Typecheck

8+

9+import Idris.AbsSyntax

10+import Idris.Delaborate

11+import Idris.ElabDecls

12+import Idris.Parser

13+import Idris.Error

14+

15+import System.Console.Readline

16+import Control.Monad.State

17+

18+prover :: Name -> Idris ()

19+prover x = do ctxt <- getContext

20+ i <- get

21+ case lookupTy x ctxt of

22+ Just t -> if elem x (idris_metavars i)

23+ then prove ctxt x t

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

25+ _ -> fail "No such metavariable"

26+

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

28+prove ctxt n ty

29+ = do let ps = initElaborator n ctxt ty

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

31+ iLOG $ "Adding " ++ show tm

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

33+ logLvl 3 (show tree)

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

35+ updateContext (addCasedef n False [(P Ref n ty, ptm)] ty)

36+ solveDeferred n

37+

38+elabStep :: ElabState -> Elab a -> Idris (a, ElabState)

39+elabStep st e = do case runStateT e st of

40+ OK (a, st') -> return (a, st')

41+ Error a -> do i <- get

42+ fail (pshow i a)

43+

44+dumpState :: IState -> ProofState -> IO ()

45+dumpState ist (PS nm [] _ tm _ _ _ _ _ _ _) = putStrLn $ (show nm) ++ ": no more goals"

46+dumpState ist ps@(PS nm (h:hs) _ tm _ _ i _ cyxy _ _)

47+ = do let OK ty = goalAtFocus ps

48+ let OK env = envAtFocus ps

49+ putStrLn $ "Other goals: " ++ show hs ++ "\n"

50+ putStr $ showPs (reverse env)

51+ putStrLn $ "---------------------------------- (" ++ show nm

52+ ++ ") --------"

53+ putStrLn $ show h ++ " : " ++ showG ty ++ "\n"

54+ where

55+ tshow t = show (delab ist t)

56+

57+ showPs [] = ""

58+ showPs ((n, Let t v) : bs)

59+ = " " ++ show n ++ " : " ++

60+ tshow t ++ " = " ++ tshow v ++ "\n" ++ showPs bs

61+ showPs ((n, b) : bs)

62+ = " " ++ show n ++ " : " ++

63+ tshow (binderTy b) ++ "\n" ++ showPs bs

64+

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

66+ showG b = tshow (binderTy b)

67+

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

69+ploop d prompt e

70+ = do i <- get

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

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

73+ cmd <- case x of

74+ Nothing -> fail "Abandoned"

75+ Just input -> do lift $ addHistory input

76+ return (parseTac i input)

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

78+ (case cmd of

79+ Left err -> do iputStrLn (show err)

80+ return (False, e, False)

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

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

83+ return (False, e, True)

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

85+ return (True, st, False))

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

87+ return (False, e, False))

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

89+ return tm

90+ else ploop d prompt st

91+

src/Idris/REPL.hs+2

@@ -8,6 +8,7 @@ import Idris.ElabDecls

8import Idris.Error

9import Idris.Delaborate

10import Idris.Compiler

11+import Idris.Prover

11

12

12import Core.Evaluate

13import Core.Evaluate

13import Core.ProofShell

14import Core.ProofShell

@@ -55,6 +56,7 @@ process (Spec t) = do (tm, ty) <- elabVal toplevel t

55 ist <- get

56 ist <- get

56 let tm' = specialise ctxt (idris_statics ist) tm

57 let tm' = specialise ctxt (idris_statics ist) tm

57 iputStrLn (show (delab ist tm'))

58 iputStrLn (show (delab ist tm'))

59+process (Prove n) = prover n

58process (HNF t) = do (tm, ty) <- elabVal toplevel t

60process (HNF t) = do (tm, ty) <- elabVal toplevel t

59 ctxt <- getContext

61 ctxt <- getContext

60 ist <- get

62 ist <- get

src/Idris/REPLParser.hs+1

@@ -25,6 +25,7 @@ pCmd = try (do cmd ["q", "quit"]; eof; return Quit)

25 <|> try (do cmd ["ttshell"]; eof; return TTShell)

26 <|> try (do cmd ["c", "compile"]; f <- identifier; eof; return (Compile f))

27 <|> try (do cmd ["m", "metavars"]; eof; return Metavars)

28+ <|> try (do cmd ["p", "prove"]; n <- pName; eof; return (Prove n))

28 <|> try (do cmd ["log"]; i <- natural; eof; return (LogLvl (fromIntegral i)))

29 <|> try (do cmd ["log"]; i <- natural; eof; return (LogLvl (fromIntegral i)))

29 <|> try (do cmd ["spec"]; t <- pFullExpr defaultSyntax; return (Spec t))

30 <|> try (do cmd ["spec"]; t <- pFullExpr defaultSyntax; return (Spec t))

30 <|> try (do cmd ["hnf"]; t <- pFullExpr defaultSyntax; return (HNF t))

31 <|> try (do cmd ["hnf"]; t <- pFullExpr defaultSyntax; return (HNF t))