a3c6231 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

:addproof knows about .lidr files

a3c6231Edwin Brady15 years ago

src/Idris/Prover.hs+14−11

compare with master

unifiedsplit

@@ -17,26 +17,30 @@ import Idris.DataOpts

17import System.Console.Haskeline

18import Control.Monad.State

20−prover :: Name -> Idris ()

20+prover :: Bool -> Name -> Idris ()

21+prover lit x =

21−prover x = do ctxt <- getContext

22+ do ctxt <- getContext

22 i <- get

23 i <- get

23 case lookupTy Nothing x ctxt of

24 case lookupTy Nothing x ctxt of

24 [t] -> if elem x (idris_metavars i)

25 [t] -> if elem x (idris_metavars i)

25− then prove ctxt x t

26+ then prove ctxt lit x t

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

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

27 _ -> fail "No such metavariable"

28 _ -> fail "No such metavariable"

29−showProof :: Name -> [String] -> String

30+showProof :: Bool -> Name -> [String] -> String

30−showProof n ps = show n ++ " = proof {" ++ "\n" ++

31+showProof lit n ps

32+ = bird ++ show n ++ " = proof {" ++ break ++

31− showSep "\n" (map (\x -> " " ++ x ++ ";") ps) ++

33+ showSep break (map (\x -> " " ++ x ++ ";") ps) ++

32− "\n}\n"

34+ break ++ "}\n"

35+ where bird = if lit then "> " else ""

36+ break = "\n" ++ bird

34−prove :: Context -> Name -> Type -> Idris ()

38+prove :: Context -> Bool -> Name -> Type -> Idris ()

35−prove ctxt n ty

39+prove ctxt lit n ty

36 = do let ps = initElaborator n ctxt ty

40 = do let ps = initElaborator n ctxt ty

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

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

38 iLOG $ "Adding " ++ show tm

42 iLOG $ "Adding " ++ show tm

39− iputStrLn $ showProof n prf

43+ iputStrLn $ showProof lit n prf

40 i <- get

44 i <- get

41 put (i { last_proof = Just (n, prf) })

45 put (i { last_proof = Just (n, prf) })

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

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

@@ -46,7 +50,6 @@ prove ctxt n ty

46 updateContext (addCasedef n True False True [(P Ref n ty, ptm)]

50 updateContext (addCasedef n True False True [(P Ref n ty, ptm)]

47 [(P Ref n ty, ptm')] ty)

51 [(P Ref n ty, ptm')] ty)

48 solveDeferred n

52 solveDeferred n

49−

50elabStep :: ElabState [PDecl] -> ElabD a -> Idris (a, ElabState [PDecl])

53elabStep :: ElabState [PDecl] -> ElabD a -> Idris (a, ElabState [PDecl])

51elabStep st e = do case runStateT e st of

54elabStep st e = do case runStateT e st of

52 OK (a, st') -> return (a, st')

55 OK (a, st') -> return (a, st')

src/Idris/REPL.hs+63−56

@@ -54,6 +54,10 @@ mkPrompt [] = "Idris"

54mkPrompt [x] = "*" ++ dropExtension x

55mkPrompt (x:xs) = "*" ++ dropExtension x ++ " " ++ mkPrompt xs

57+lit f = case splitExtension f of

58+ (_, ".lidr") -> True

59+ _ -> False

60+

57processInput :: String -> IState -> [FilePath] -> Idris (Maybe [FilePath])

61processInput :: String -> IState -> [FilePath] -> Idris (Maybe [FilePath])

58processInput cmd orig inputs

62processInput cmd orig inputs

59 = do i <- get

63 = do i <- get

@@ -74,7 +78,7 @@ processInput cmd orig inputs

74 return (Just inputs)

78 return (Just inputs)

75 Right Quit -> do iputStrLn "Bye bye"

79 Right Quit -> do iputStrLn "Bye bye"

76 return Nothing

80 return Nothing

77− Right cmd -> do idrisCatch (process cmd)

81+ Right cmd -> do idrisCatch (process fn cmd)

78 (\e -> iputStrLn (show e))

82 (\e -> iputStrLn (show e))

79 return (Just inputs)

83 return (Just inputs)

@@ -107,7 +111,7 @@ addProof f orig

107 i <- get

111 i <- get

108 case last_proof i of

112 case last_proof i of

109 Nothing -> iputStrLn "No proof to add"

113 Nothing -> iputStrLn "No proof to add"

110− Just (n, p) -> do let prog' = insertScript (showProof n p) (lines prog)

114+ Just (n, p) -> do let prog' = insertScript (showProof (lit f) n p) (lines prog)

111 liftIO $ writeFile f (unlines prog')

115 liftIO $ writeFile f (unlines prog')

112 iputStrLn $ "Added proof " ++ show n

116 iputStrLn $ "Added proof " ++ show n

113 put (i { last_proof = Nothing })

117 put (i { last_proof = Nothing })

@@ -119,9 +123,10 @@ insertScript prf (p@"---------- Proofs ----------" : "" : xs)

119 = p : "" : prf : xs

123 = p : "" : prf : xs

120insertScript prf (x : xs) = x : insertScript prf xs

124insertScript prf (x : xs) = x : insertScript prf xs

121

125

122−process :: Command -> Idris ()

126+process :: FilePath -> Command -> Idris ()

123−process Help = iputStrLn displayHelp

127+process fn Help = iputStrLn displayHelp

128+process fn (Eval t)

124−process (Eval t) = do (tm, ty) <- elabVal toplevel False t

129+ = do (tm, ty) <- elabVal toplevel False t

125 ctxt <- getContext

130 ctxt <- getContext

126 ist <- get

131 ist <- get

127 let tm' = normaliseAll ctxt [] tm

132 let tm' = normaliseAll ctxt [] tm

@@ -130,7 +135,8 @@ process (Eval t) = do (tm, ty) <- elabVal toplevel False t

130 imp <- impShow

135 imp <- impShow

131 iputStrLn (showImp imp (delab ist tm') ++ " : " ++

136 iputStrLn (showImp imp (delab ist tm') ++ " : " ++

132 showImp imp (delab ist ty'))

137 showImp imp (delab ist ty'))

138+process fn (ExecVal t)

133−process (ExecVal t) = do (tm, ty) <- elabVal toplevel False t

139+ = do (tm, ty) <- elabVal toplevel False t

134-- (PApp fc (PRef fc (NS (UN "print") ["prelude"]))

140-- (PApp fc (PRef fc (NS (UN "print") ["prelude"]))

135-- [pexp t])

141-- [pexp t])

136 (tmpn, tmph) <- liftIO tempfile

142 (tmpn, tmph) <- liftIO tempfile

@@ -139,7 +145,7 @@ process (ExecVal t) = do (tm, ty) <- elabVal toplevel False t

139 liftIO $ system tmpn

145 liftIO $ system tmpn

140 return ()

146 return ()

141 where fc = FC "(input)" 0

147 where fc = FC "(input)" 0

142−process (Check (PRef _ n))

148+process fn (Check (PRef _ n))

143 = do ctxt <- getContext

149 = do ctxt <- getContext

144 ist <- get

150 ist <- get

145 imp <- impShow

151 imp <- impShow

@@ -147,74 +153,75 @@ process (Check (PRef _ n))

147 [t] -> iputStrLn $ show n ++ " : " ++

153 [t] -> iputStrLn $ show n ++ " : " ++

148 showImp imp (delab ist t)

154 showImp imp (delab ist t)

149 _ -> iputStrLn $ "No such variable " ++ show n

155 _ -> iputStrLn $ "No such variable " ++ show n

150−process (Check t) = do (tm, ty) <- elabVal toplevel False t

156+process fn (Check t) = do (tm, ty) <- elabVal toplevel False t

151− ctxt <- getContext

157+ ctxt <- getContext

152− ist <- get

158+ ist <- get

153− imp <- impShow

159+ imp <- impShow

154− let ty' = normaliseC ctxt [] ty

160+ let ty' = normaliseC ctxt [] ty

155− iputStrLn (showImp imp (delab ist tm) ++ " : " ++

161+ iputStrLn (showImp imp (delab ist tm) ++ " : " ++

156− showImp imp (delab ist ty))

162+ showImp imp (delab ist ty))

157−process Universes = do i <- get

163+process fn Universes = do i <- get

158− let cs = idris_constraints i

164+ let cs = idris_constraints i

159-- iputStrLn $ showSep "\n" (map show cs)

165-- iputStrLn $ showSep "\n" (map show cs)

160− liftIO $ print (map fst cs)

166+ liftIO $ print (map fst cs)

161− let n = length cs

167+ let n = length cs

162− iputStrLn $ "(" ++ show n ++ " constraints)"

168+ iputStrLn $ "(" ++ show n ++ " constraints)"

163− case ucheck cs of

169+ case ucheck cs of

164 Error e -> iputStrLn $ pshow i e

170 Error e -> iputStrLn $ pshow i e

165 OK _ -> iputStrLn "Universes OK"

171 OK _ -> iputStrLn "Universes OK"

166−process (Defn n) = do i <- get

172+process fn (Defn n) = do i <- get

167− iputStrLn "Compiled patterns:\n"

173+ iputStrLn "Compiled patterns:\n"

168− liftIO $ print (lookupDef Nothing n (tt_ctxt i))

174+ liftIO $ print (lookupDef Nothing n (tt_ctxt i))

169− case lookupCtxt Nothing n (idris_patdefs i) of

175+ case lookupCtxt Nothing n (idris_patdefs i) of

170− [] -> return ()

176+ [] -> return ()

171− [d] -> do iputStrLn "Original definiton:\n"

177+ [d] -> do iputStrLn "Original definiton:\n"

172− mapM_ (printCase i) d

178+ mapM_ (printCase i) d

173 where printCase i (lhs, rhs) = do liftIO $ putStr $ showImp True (delab i lhs)

179 where printCase i (lhs, rhs) = do liftIO $ putStr $ showImp True (delab i lhs)

174 liftIO $ putStr " = "

180 liftIO $ putStr " = "

175 liftIO $ putStrLn $ showImp True (delab i rhs)

181 liftIO $ putStrLn $ showImp True (delab i rhs)

176−process (Info n) = do i <- get

182+process fn (Info n) = do i <- get

177− let oi = lookupCtxt Nothing n (idris_optimisation i)

183+ let oi = lookupCtxt Nothing n (idris_optimisation i)

178− liftIO $ print oi

184+ liftIO $ print oi

179−process (Spec t) = do (tm, ty) <- elabVal toplevel False t

185+process fn (Spec t) = do (tm, ty) <- elabVal toplevel False t

180− ctxt <- getContext

186+ ctxt <- getContext

181− ist <- get

187+ ist <- get

182− let tm' = specialise ctxt (idris_statics ist) tm

188+ let tm' = specialise ctxt (idris_statics ist) tm

183− iputStrLn (show (delab ist tm'))

189+ iputStrLn (show (delab ist tm'))

184−process (Prove n) = prover n

190+process fn (Prove n) = prover (lit fn) n

185−process (HNF t) = do (tm, ty) <- elabVal toplevel False t

191+process fn (HNF t) = do (tm, ty) <- elabVal toplevel False t

186− ctxt <- getContext

192+ ctxt <- getContext

187− ist <- get

193+ ist <- get

188− let tm' = simplify ctxt [] tm

194+ let tm' = simplify ctxt [] tm

189− iputStrLn (show (delab ist tm'))

195+ iputStrLn (show (delab ist tm'))

190−process TTShell = do ist <- get

196+process fn TTShell = do ist <- get

191− let shst = initState (tt_ctxt ist)

197+ let shst = initState (tt_ctxt ist)

192− shst' <- lift $ runShell shst

198+ shst' <- lift $ runShell shst

193− return ()

199+ return ()

194−process Execute = do (m, _) <- elabVal toplevel False

200+process fn Execute = do (m, _) <- elabVal toplevel False

195 (PApp fc

201 (PApp fc

196 (PRef fc (UN "run__IO"))

202 (PRef fc (UN "run__IO"))

197 [pexp $ PRef fc (NS (UN "main") ["main"])])

203 [pexp $ PRef fc (NS (UN "main") ["main"])])

198-- (PRef (FC "main" 0) (NS (UN "main") ["main"]))

204-- (PRef (FC "main" 0) (NS (UN "main") ["main"]))

199− (tmpn, tmph) <- liftIO tempfile

205+ (tmpn, tmph) <- liftIO tempfile

200− liftIO $ hClose tmph

206+ liftIO $ hClose tmph

201− compile tmpn m

207+ compile tmpn m

202− liftIO $ system tmpn

208+ liftIO $ system tmpn

203− return ()

209+ return ()

204 where fc = FC "main" 0

210 where fc = FC "main" 0

205−process (Compile f) = do (m, _) <- elabVal toplevel False

211+process fn (Compile f) = do (m, _) <- elabVal toplevel False

206 (PApp fc

212 (PApp fc

207 (PRef fc (UN "run__IO"))

213 (PRef fc (UN "run__IO"))

208 [pexp $ PRef fc (NS (UN "main") ["main"])])

214 [pexp $ PRef fc (NS (UN "main") ["main"])])

209− compile f m

215+ compile f m

210 where fc = FC "main" 0

216 where fc = FC "main" 0

211−process (LogLvl i) = setLogLevel i

217+process fn (LogLvl i) = setLogLevel i

212−process Metavars = do ist <- get

218+process fn Metavars

219+ = do ist <- get

213 let mvs = idris_metavars ist \\ primDefs

220 let mvs = idris_metavars ist \\ primDefs

214 case mvs of

221 case mvs of

215 [] -> iputStrLn "No global metavariables to solve"

222 [] -> iputStrLn "No global metavariables to solve"

216 _ -> iputStrLn $ "Global metavariables:\n\t" ++ show mvs

223 _ -> iputStrLn $ "Global metavariables:\n\t" ++ show mvs

217−process NOP = return ()

224+process fn NOP = return ()

218

225

219displayHelp = let vstr = showVersion version in

226displayHelp = let vstr = showVersion version in

220 "\nIdris version " ++ vstr ++ "\n" ++

227 "\nIdris version " ++ vstr ++ "\n" ++

src/Main.hs+1−1

@@ -66,7 +66,7 @@ runIdris opts =

66 ok <- noErrors

67 when ok $ case output of

68 [] -> return ()

69− (o:_) -> process (Compile o)

69+ (o:_) -> process "" (Compile o)

70 when runrepl $ repl ist inputs

71 ok <- noErrors

72 when (not ok) $ liftIO (exitWith (ExitFailure 1))