739e0b5 · Idris-dev · git.iko.soy

miniidris.cabal+1−1

compare with master

unifiedsplit

@@ -23,7 +23,7 @@ Executable miniidris

23 Core.CaseTree,

24

25 Idris.AbsSyntax, Idris.Parser, Idris.REPL,

26− Idris.REPLParser, Idris.ElabDecls

26+ Idris.REPLParser, Idris.ElabDecls, Idris.Error

27

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

29 containers, process, transformers

src/Core/ProofState.hs+1

@@ -227,6 +227,7 @@ complete_fill ctxt env (Bind x (Guess ty val) sc) =

227 let (uh, uns) = unified ps

228 put (ps { unified = (uh, uns ++ ns) })

229 return $ Bind x (Guess ty val) sc

230+complete_fill ctxt env t = fail $ "Can't complete fill at " ++ show t

230

231

231solve :: RunTactic

232solve :: RunTactic

232solve ctxt env (Bind x (Guess ty val) sc)

233solve ctxt env (Bind x (Guess ty val) sc)

src/Core/Unify.hs+3

@@ -11,6 +11,9 @@ import Control.Monad

11-- which can be filled in, by matching one term's normal form against another.

12-- Returns a list of hole names paired with the term which solves them.

13

14+-- FIXME! Needs to be cleverer: when we solve a variable, fill it in and normalise

15+-- to help the rest of the unification

16+

14unify :: Context -> Env -> TT Name -> TT Name -> TC [(Name, TT Name)]

17unify :: Context -> Env -> TT Name -> TT Name -> TC [(Name, TT Name)]

15unify ctxt env x y

18unify ctxt env x y

16 = case un' [] x y of -- try without normalising first, for speed

19 = case un' [] x y of -- try without normalising first, for speed

src/Idris/AbsSyntax.hs+1−1

@@ -257,7 +257,7 @@ implicitise ist tm

257 = do (decls, a, ns) <- get

258 let isn = concatMap (namesIn ist) (map snd is)

259 let esn = concatMap (namesIn ist) es

260− put (decls, a, nub (ns ++ ((isn ++ esn) \\ env)))

260+ put (decls, a, nub (ns ++ ((isn ++ esn) \\ (env ++ decls))))

261 imps env (PPi Imp n ty sc)

262 = do imps env ty

263 (impdecls, a, ns) <- get

src/Idris/ElabDecls.hs+6−4

@@ -3,6 +3,7 @@

3module Idris.ElabDecls where

4

5import Idris.AbsSyntax

6+import Idris.Error

6

7

7import Core.TT

8import Core.TT

8import Core.Elaborate

9import Core.Elaborate

@@ -63,6 +64,7 @@ elabVal tm

63 (tm', _) <- tclift $ elaborate ctxt (MN 0 "val") infP

64 (tm', _) <- tclift $ elaborate ctxt (MN 0 "val") infP

64 (build False (infTerm tm))

65 (build False (infTerm tm))

65 let vtm = getInferTerm tm'

66 let vtm = getInferTerm tm'

67+ iLOG (show vtm)

66 tclift $ recheck ctxt [] vtm

68 tclift $ recheck ctxt [] vtm

67

69

68elabClause :: PClause -> Idris (Term, Term)

70elabClause :: PClause -> Idris (Term, Term)

@@ -94,7 +96,7 @@ elabClause (PClause _ lhs rhs)

94 psolve tm = return ()

96 psolve tm = return ()

95

97

96elabDecl :: PDecl -> Idris ()

98elabDecl :: PDecl -> Idris ()

97−elabDecl d = idrisCatch (elabDecl' d) (\e -> iputStrLn (show e))

99+elabDecl d = idrisCatch (elabDecl' d) (\e -> iputStrLn (report e))

98

100

99elabDecl' (PFix _ _) = return () -- nothing to elaborate

101elabDecl' (PFix _ _) = return () -- nothing to elaborate

100elabDecl' (PTy n ty) = do iLOG $ "Elaborating type decl " ++ show n

102elabDecl' (PTy n ty) = do iLOG $ "Elaborating type decl " ++ show n

@@ -149,11 +151,11 @@ elab pattern tm = do elab' tm

149 elab' sc

151 elab' sc

150 solve

152 solve

151 elab' (PApp (PRef f) imps args)

153 elab' (PApp (PRef f) imps args)

154+ = try (do apply_elab f (map toElab imps ++ map (Just . elab') args)

155+ solve)

152− = try (do ns <- apply (Var f) (map isph imps ++ map (\x -> False) args)

156+ (do ns <- apply (Var f) (map isph imps ++ map (\x -> False) args)

153 solve

157 solve

154 elabArgs ns (map snd imps ++ args))

158 elabArgs ns (map snd imps ++ args))

155− (do apply_elab f (map toElab imps ++ map (Just . elab') args)

156− solve)

157 elab' (PApp f [] [arg])

159 elab' (PApp f [] [arg])

158 = do simple_app (elab' f) (elab' arg)

160 = do simple_app (elab' f) (elab' arg)

159 solve

161 solve

src/Idris/Error.hsnew file+10

@@ -0,0 +1,10 @@

1+module Idris.Error where

2+

3+import Idris.AbsSyntax

4+import System.IO.Error

5+

6+report :: IOError -> String

7+report e

8+ | isUserError e = ioeGetErrorString e

9+ | otherwise = show e

10+

src/Idris/REPL.hs+3−1

@@ -5,6 +5,7 @@ module Idris.REPL where

5import Idris.AbsSyntax

6import Idris.REPLParser

7import Idris.ElabDecls

8+import Idris.Error

8

9

9import Core.Evaluate

10import Core.Evaluate

10import Core.ProofShell

11import Core.ProofShell

@@ -31,7 +32,8 @@ processInput cmd

31 return True

32 return True

32 Right Quit -> do iputStrLn "Bye bye"

33 Right Quit -> do iputStrLn "Bye bye"

33 return False

34 return False

34− Right cmd -> do process cmd

35+ Right cmd -> do idrisCatch (process cmd)

36+ (\e -> iputStrLn (report e))

35 return True

37 return True

36

38

37process :: Command -> Idris ()

39process :: Command -> Idris ()