6923ac1 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Started theorem prover and tactics

6923ac1Edwin Brady15 years ago

miniidris.cabal+3−2

compare with master

unifiedsplit

@@ -17,9 +17,10 @@ Build-type: Simple

17Executable miniidris

18 Main-is: Main.hs

19 hs-source-dirs: src

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

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

21+ ProofState, CoreParser, ShellParser

22− Build-depends: base>=4 && <5, parsec, mtl, Cabal

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

24 Extensions: MultiParamTypeClasses, FunctionalDependencies,

25 Extensions: MultiParamTypeClasses, FunctionalDependencies,

25 FlexibleInstances

26 FlexibleInstances

src/Core.hs+4−2

@@ -35,7 +35,7 @@ data Name = UN [String]

35instance Show Name where

36 show (UN [n]) = n

37 show (UN (n:ns)) = show (UN [n]) ++ "." ++ show (UN ns)

38− show (MN i s) = "{" ++ s ++ ":" ++ show i ++ "}"

38+ show (MN i s) = "{" ++ s ++ show i ++ "}"

40data Raw = Var Name

41 | RBind Name (Binder Raw) Raw

@@ -74,7 +74,7 @@ data TT n = P NameType n (TT n) -- embed type

74 | Bind n (Binder (TT n)) (TT n)

75 | App (TT n) (TT n) (TT n) -- function, function type, arg

76 | Set Int

77− deriving Eq

77+ deriving (Functor, Eq)

79type EnvTT n = [(n, Binder (TT n))]

@@ -147,6 +147,8 @@ data Def = Function Fun

147

148type Context = [(Name, Def)]

149

150+emptyContext = []

151+

150lookupTy :: Name -> Context -> Maybe Type

152lookupTy :: Name -> Context -> Maybe Type

151lookupTy n ctxt = do def <- lookup n ctxt

153lookupTy n ctxt = do def <- lookup n ctxt

152 case def of

154 case def of

src/Main.hs+10−1

@@ -1,6 +1,15 @@

1module Main where

3+import CoreParser

4+import ShellParser

5+import Core

3import Typecheck

6import Typecheck

4import ProofState

7import ProofState

8+import ProofShell

6−main = putStrLn "Nothing Happens"

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

11+ let Right defs = parseFile f

12+ print defs

13+ let OK ctxt = checkProgram [] defs

14+ print ctxt

15+ runShell (initState ctxt)

src/ProofShell.hs+8−5

@@ -26,19 +26,22 @@ processCommand (Theorem n ty) state

26 err -> (state, show err)

27processCommand Quit state = (state { exitNow = True }, "Bye bye")

28processCommand (Tac t) state

29− | Just ps <- prf state = let (ps', resp) = processTactic t ps in

29+ | Just ps <- prf state = case processTactic t ps of

30− (state { prf = Just ps' }, resp)

30+ OK (ps', resp) -> (state { prf = Just ps' }, resp)

31+ err -> (state, show err)

31 | otherwise = (state, "No proof in progress")

32 | otherwise = (state, "No proof in progress")

33runShell :: ShellState -> IO ShellState

34runShell :: ShellState -> IO ShellState

34−runShell st = do prompt <- maybe (return "> ")

35+runShell st = do (prompt, parser) <-

36+ maybe (return ("> ", parseCommand))

37+ (\st -> do print st

35− (\st -> do print st; return (show (thname st) ++ "> "))

38+ return (show (thname st) ++ "> ", parseTactic))

36 (prf st)

39 (prf st)

37 x <- readline prompt

40 x <- readline prompt

38 cmd <- case x of

41 cmd <- case x of

39 Nothing -> return $ Right Quit

42 Nothing -> return $ Right Quit

40 Just input -> do addHistory input

43 Just input -> do addHistory input

41− return (parseCommand input)

44+ return (parser input)

42 case cmd of

45 case cmd of

43 Left err -> do putStrLn (show err)

46 Left err -> do putStrLn (show err)

44 runShell st

47 runShell st

src/ProofState.hs+77−8

@@ -7,23 +7,59 @@ import Evaluate

7import Core

8import Control.Monad.State

10+data ProofState = PS { thname :: Name,

10−data ProofState = PS { holes :: [Name], -- holes still to be solved

11+ holes :: [Name], -- holes still to be solved

11− nextname :: Int, -- name supply

12+ nextname :: Int, -- name supply

12− pterm :: Term -- current proof term

13+ pterm :: Term, -- current proof term

14+ context :: Context,

15+ complete :: Bool

13 }

16 }

15data Goal = GD { premises :: Env,

18data Goal = GD { premises :: Env,

16− goalType :: Term

19+ goalType :: Binder Term

17 }

20 }

22+data Command = Theorem Name Raw

23+ | Eval Raw

24+ | Quit

25+ | Tac Tactic

26+

27+data Tactic = Attack

28+ | Claim Name Raw

29+ | Try Raw

30+ | Regret

31+ | Solve

32+ | QED

33+

34+instance Show ProofState where

35+ show (PS nm [] _ tm _ _) = show nm ++ ": no more goals"

36+ show (PS nm (h:hs) _ tm ctxt _)

37+ = let OK g = goal (Just h) tm ctxt in

38+ showEnv (premises g) ++ "\n" ++

39+ "-------------------------------- (" ++ show nm ++

40+ ") -------\n" ++

41+ show h ++ " : " ++ showG (goalType g) ++ "\n"

42+ where showEnv [] = ""

43+ showEnv ((n, b):bs) = " " ++ show n ++ " : " ++ show (binderTy b) ++ "\n" ++

44+ showEnv bs

45+ showG (Guess t v) = show t ++ " =?= " ++ show v

46+ showG b = show (binderTy b)

47+

48+holeName i = MN i "hole"

49+

50+newProof :: Name -> Context -> Type -> ProofState

51+newProof n ctxt ty = let h = holeName 0 in

52+ PS n [h] 1 (Bind h (Hole ty) (V 0)) ctxt False

53+

19data TacticAction = AddGoal Name

54data TacticAction = AddGoal Name

20−

55+ | Log String

56+

21−type Tactic = Context -> Env -> Term -> StateT [TacticAction] TC Term

57+type RunTactic = Context -> Env -> Term -> StateT [TacticAction] TC Term

22type Hole = Maybe Name -- Nothing = default hole, first in list in proof state

58type Hole = Maybe Name -- Nothing = default hole, first in list in proof state

24goal :: Hole -> Term -> Context -> TC Goal

60goal :: Hole -> Term -> Context -> TC Goal

25goal h tm ctxt = g [] tm where

61goal h tm ctxt = g [] tm where

26− g env (Bind n b sc) | hole b && same h n = return $ GD env (binderTy b)

62+ g env (Bind n b sc) | hole b && same h n = return $ GD env b

27 | otherwise = gb env b `mplus` g ((n,b):env) sc

63 | otherwise = gb env b `mplus` g ((n,b):env) sc

28 g env (App f t a) = g env f `mplus` g env t `mplus` g env a

64 g env (App f t a) = g env f `mplus` g env t `mplus` g env a

29 g env t = Error "Can't find hole"

65 g env t = Error "Can't find hole"

@@ -32,7 +68,7 @@ goal h tm ctxt = g [] tm where

32 gb env (Guess t v) = g env t `mplus` g env v

68 gb env (Guess t v) = g env t `mplus` g env v

33 gb env t = g env (binderTy t)

69 gb env t = g env (binderTy t)

35−tactic :: Hole -> Term -> Context -> Tactic -> StateT [TacticAction] TC Term

71+tactic :: Hole -> Term -> Context -> RunTactic -> StateT [TacticAction] TC Term

36tactic h tm ctxt f = atH [] tm where

72tactic h tm ctxt f = atH [] tm where

37 atH env binder@(Bind n b sc)

73 atH env binder@(Bind n b sc)

38 | hole b && same h n = f ctxt env binder

74 | hole b && same h n = f ctxt env binder

@@ -58,4 +94,37 @@ same (Just x) n = x == n

58hole (Hole _) = True

94hole (Hole _) = True

59hole (Guess _ _) = True

95hole (Guess _ _) = True

97+attack :: RunTactic

98+attack = undefined

99+

100+claim :: Name -> Raw -> RunTactic

101+claim = undefined

102+

103+regret :: RunTactic

104+regret = undefined

105+

106+fill :: Raw -> RunTactic -- Try

107+fill = undefined

108+

109+solve :: RunTactic

110+solve = undefined

111+

112+processTactic :: Tactic -> ProofState -> TC (ProofState, String)

113+processTactic QED ps = case holes ps of

114+ [] -> return (ps { complete = True }, "QED")

115+ _ -> Error "Still holes to fill"

116+processTactic t ps = case holes ps of

117+ [] -> Error "Nothing to fill in"

118+ (h:_) -> do (ps', actions) <- runStateT (process t h ps) []

119+ return (ps', logs actions)

120+ where logs [] = ""

121+ logs (Log x : xs) = x ++ "\n" ++ logs xs

122+ logs (_ : xs) = logs xs

123+

124+process :: Tactic -> Name -> ProofState -> StateT [TacticAction] TC ProofState

125+process (Try x) h ps = undefined

126+

127+

128+

129+

130

src/ShellParser.hs+4−3

@@ -32,7 +32,7 @@ reservedOp= PTok.reservedOp lexer

32lchar = lexeme.char

34parseCommand = parse pCommand "(input)"

35−parseTactic = parse pTactic "(input)"

35+parseTactic = parse (pTactic >>= return . Tac) "(input)"

37pCommand :: Parser Command

38pCommand = do reserved "theorem"; n <- identifier; lchar ':'; ty <- pTerm

@@ -44,8 +44,9 @@ pCommand = do reserved "theorem"; n <- identifier; lchar ':'; ty <- pTerm

45pTactic :: Parser Tactic

46pTactic = do reserved "attack"; return Attack

47− <|> do reserved "claim"; ty <- pTerm; return (Claim ty)

47+ <|> do reserved "claim"; n <- identifier; lchar ':'; ty <- pTerm

48+ return (Claim (UN [n]) ty)

48 <|> do reserved "try"; tm <- pTerm; return (Try tm)

49 <|> do reserved "try"; tm <- pTerm; return (Try tm)

49 <|> do reserved "regret"; return Regret

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

50 <|> do reserved "solve"; return Solve

51 <|> do reserved "solve"; return Solve

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

52+ <|> do reserved "qed"; return QED

src/Test.hs+1−1

@@ -8,4 +8,4 @@ test = do f <- readFile "test.mi"

8 let Right defs = parseFile f

9 print defs

10 let ctxt = checkProgram [] defs

11− print ctxt

11+ print ctxt

src/Typecheck.hs+4−1

@@ -10,7 +10,10 @@ import Evaluate

11data TC a = OK a

12 | Error String -- TMP! Make this an informative data structure

13− deriving Show

13+

14+instance Show a => Show (TC a) where

15+ show (OK x) = show x

16+ show (Error str) = "Error: " ++ str

15-- at some point, this instance should also carry type checking options

18-- at some point, this instance should also carry type checking options

16-- (e.g. Set:Set)

19-- (e.g. Set:Set)