12bd089 · Idris-dev · git.iko.soy

lib/Makefile+6−1

@@ -1,4 +1,9 @@

1+SRCS = prelude.idr list.idr nat.idr prelude.idr vect.idr

2+

13check: .PHONY

2− miniidris --noprelude --check *.idr

4+ for x in *.idr ; do \

5+ echo "Checking $$x"; \

6+ miniidris --noprelude --check $$x; \

7+ done

38

49.PHONY:

src/Core/Elaborate.hs+8

@@ -81,6 +81,11 @@ get_type tm = do ctxt <- get_context

8181 (val, ty) <- lift $ check ctxt env tm

8282 return (finalise ty)

8383

84+-- get holes we've deferred for later definition

85+get_deferred :: Elab [Name]

86+get_deferred = do (p, _) <- get

87+ return (deferred p)

88+

8489-- given a desired hole name, return a unique hole name

8590unique_hole :: Name -> Elab Name

8691unique_hole n = do (p, _) <- get

@@ -162,6 +167,9 @@ focus n = processTactic' (Focus n)

162167movelast :: Name -> Elab ()

163168movelast n = processTactic' (MoveLast n)

164169

170+defer :: Name -> Elab ()

171+defer n = processTactic' (Defer n)

172+

165173proofstate :: Elab ()

166174proofstate = processTactic' ProofState

167175

src/Core/ProofState.hs+15−2

@@ -23,7 +23,7 @@ data ProofState = PS { thname :: Name,

2323 pterm :: Term, -- current proof term

2424 ptype :: Type, -- original goal

2525 unified :: (Name, [(Name, Term)]),

26− defer :: [(Name, Type)], -- names we'll need to define

26+ deferred :: [Name], -- names we'll need to define

2727 previous :: Maybe ProofState, -- for undo

2828 context :: Context,

2929 plog :: String,

@@ -52,6 +52,7 @@ data Tactic = Attack

5252 | PatVar Name

5353 | PatBind Name

5454 | Focus Name

55+ | Defer Name

5556 | MoveLast Name

5657 | ProofState

5758 | Undo

@@ -138,7 +139,6 @@ goal h tm = g [] tm where

138139 gb env (Let t v) = g env t `mplus` g env v

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

140141 gb env t = g env (binderTy t)

141−

142142tactic :: Hole -> RunTactic -> StateT TState TC ()

143143tactic h f = do ps <- get

144144 tm' <- atH (context ps) [] (pterm ps)

@@ -188,6 +188,18 @@ movelast n ctxt env t = do action (\ps -> let hs = holes ps in

188188 else ps)

189189 return t

190190

191+defer :: Name -> RunTactic

192+defer n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =

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

194+ ps { holes = hs \\ [x] })

195+ return (Bind n (GHole (mkTy (reverse env) t))

196+ (mkApp (P nt n ty) (map getP (reverse env))))

197+ where

198+ mkTy [] t = t

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

200+

201+ getP (n, b) = P Bound n (binderTy b)

202+

191203-- Hmmm. YAGNI?

192204regret :: RunTactic

193205regret = undefined

@@ -373,3 +385,4 @@ process t h = tactic (Just h) (mktac t)

373385 mktac (EvalIn r) = eval_in r

374386 mktac (Focus n) = focus n

375387 mktac (MoveLast n) = movelast n

388+ mktac (Defer n) = defer n

src/Core/TT.hs+2

@@ -118,6 +118,7 @@ data Binder b = Lam { binderTy :: b }

118118 | NLet { binderTy :: b,

119119 binderVal :: b }

120120 | Hole { binderTy :: b}

121+ | GHole { binderTy :: b}

121122 | Guess { binderTy :: b,

122123 binderVal :: b }

123124 | PVar { binderTy :: b }

@@ -303,6 +304,7 @@ showEnv' env t dbg = se 10 env t where

303304

304305 sb env n (Lam t) = showb env "\\ " " => " n t

305306 sb env n (Hole t) = showb env "? " ". " n t

307+ sb env n (GHole t) = showb env "?defer " ". " n t

306308 sb env n (Pi t) = showb env "(" ") -> " n t

307309 sb env n (PVar t) = showb env "pat " ". " n t

308310 sb env n (PVTy t) = showb env "pty " ". " n t

src/Core/Typecheck.hs+19

@@ -92,6 +92,12 @@ check ctxt env (RBind n b sc)

9292 let tt' = normalise ctxt env tt

9393 isSet ctxt env tt'

9494 return (Hole tv')

95+ checkBinder (GHole t)

96+ = do (tv, tt) <- check ctxt env t

97+ let tv' = normalise ctxt env tv

98+ let tt' = normalise ctxt env tt

99+ isSet ctxt env tt'

100+ return (GHole tv')

95101 checkBinder (Guess t v)

96102 = do (tv, tt) <- check ctxt env t

97103 (vv, vt) <- check ctxt env v

@@ -106,6 +112,13 @@ check ctxt env (RBind n b sc)

106112 let tt' = normalise ctxt env tt

107113 isSet ctxt env tt'

108114 return (PVar tv')

115+ checkBinder (PVTy t)

116+ = do (tv, tt) <- check ctxt env t

117+ let tv' = normalise ctxt env tv

118+ let tt' = normalise ctxt env tt

119+ isSet ctxt env tt'

120+ return (PVTy tv')

121+ checkBinder x = fail (show x)

109122

110123 discharge n (Lam t) scv sct

111124 = return (Bind n (Lam t) scv, Bind n (Pi t) sct)

@@ -119,12 +132,18 @@ check ctxt env (RBind n b sc)

119132 = do -- A hole can't appear in the type of its scope

120133 checkNotHoley 0 sct

121134 return (Bind n (Hole t) scv, sct)

135+ discharge n (GHole t) scv sct

136+ = do -- A hole can't appear in the type of its scope

137+ checkNotHoley 0 sct

138+ return (Bind n (GHole t) scv, sct)

122139 discharge n (Guess t v) scv sct

123140 = do -- A hole can't appear in the type of its scope

124141 checkNotHoley 0 sct

125142 return (Bind n (Guess t v) scv, sct)

126143 discharge n (PVar t) scv sct

127144 = return (Bind n (PVar t) scv, Bind n (PVTy t) sct)

145+ discharge n (PVTy t) scv sct

146+ = return (Bind n (PVTy t) scv, sct)

128147

129148 checkNotHoley i (V v)

130149 | v == i = fail "You can't put a hole where a hole don't belong"

src/Idris/AbsSyntax.hs+21−2

@@ -29,11 +29,12 @@ data IState = IState { tt_ctxt :: Context,

2929 idris_log :: String,

3030 idris_options :: IOption,

3131 idris_name :: Int,

32+ idris_metavars :: [Name],

3233 imported :: [FilePath],

3334 idris_prims :: [(Name, ([E.Name], E.Term))]

3435 }

3536

36−idrisInit = IState emptyContext [] emptyContext "" defaultOpts 0 [] []

37+idrisInit = IState emptyContext [] emptyContext "" defaultOpts 0 [] [] []

3738

3839-- The monad for the main REPL - reading and processing files and updating

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

@@ -54,12 +55,27 @@ getName = do i <- get;

5455 put (i { idris_name = idx + 1 })

5556 return idx

5657

58+checkUndefined :: Name -> Idris ()

59+checkUndefined n = do i <- getContext

60+ case lookupCtxt n i of

61+ Just _ -> fail $ show n ++ " already defined"

62+ _ -> return ()

63+

5764setContext :: Context -> Idris ()

5865setContext ctxt = do i <- get; put (i { tt_ctxt = ctxt } )

5966

6067updateContext :: (Context -> Context) -> Idris ()

6168updateContext f = do i <- get; put (i { tt_ctxt = f (tt_ctxt i) } )

6269

70+addDeferred :: [(Name, Type)] -> Idris ()

71+addDeferred ns = do mapM_ (\(n, t) -> updateContext (addTyDecl n t)) ns

72+ i <- get

73+ put (i { idris_metavars = map fst ns ++ idris_metavars i })

74+

75+solveDeferred :: Name -> Idris ()

76+solveDeferred n = do i <- get

77+ put (i { idris_metavars = idris_metavars i \\ [n] })

78+

6379iputStrLn :: String -> Idris ()

6480iputStrLn = lift.putStrLn

6581

@@ -87,6 +103,7 @@ iLOG = logLvl 1

87103

88104data Command = Quit | Help | Eval PTerm

89105 | Compile String

106+ | Metavars

90107 | TTShell

91108 | NOP

92109

@@ -162,6 +179,7 @@ data PTerm = PQuote Raw

162179 | Placeholder

163180 | PDoBlock [PDo]

164181 | PReturn

182+ | PMetavar Name

165183 | PElabError String -- error to report on elaboration

166184

167185data PDo = DoExp PTerm

@@ -258,6 +276,7 @@ showImp impl tm = se 10 tm where

258276 se p (PPair l r) = "(" ++ se 10 l ++ ", " ++ se 10 r ++ ")"

259277 se p PSet = "Set"

260278 se p (PConstant c) = show c

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

261280 se p Placeholder = "_"

262281

263282 seArg arg = " " ++ se 0 arg

@@ -312,7 +331,7 @@ getInferTerm tm = error ("getInferTerm " ++ show tm)

312331getInferType (Bind n b sc) = Bind n b $ getInferType sc

313332getInferType (App (App _ ty) _) = ty

314333

315−-- Handy primitives: Unit, False, Pair, MkPair

334+-- Handy primitives: Unit, False, Pair, MkPair, mkForeign

316335

317336unitTy = MN 0 "__Unit"

318337unitCon = MN 0 "__II"

src/Idris/Compiler.hs+2

@@ -13,6 +13,8 @@ import Control.Monad.State

1313import Epic.Epic hiding (Term, Type, Name, fn, compile)

1414import qualified Epic.Epic as E

1515

16+primDefs = [UN ["mkForeign"]]

17+

1618compile :: FilePath -> Idris ()

1719compile f = do ds <- mkDecls

1820 lift $ compileWith [Debug] (mkProgram ds) f

src/Idris/ElabDecls.hs+49−20

@@ -30,17 +30,21 @@ toplevel = EInfo [] emptyContext id

3030elabType :: ElabInfo -> Name -> PTerm -> Idris ()

3131elabType info n_in ty_in = let ty = piBind (params info) ty_in

3232 n = liftname info n_in in

33− do ctxt <- getContext

33+ do checkUndefined n

34+ ctxt <- getContext

3435 logLvl 2 $ "Type " ++ showImp True ty

35− (ty', log) <- tclift $ elaborate ctxt n (Set 0) (build info False ty)

36+ ((ty', defer), log) <- tclift $ elaborate ctxt n (Set 0) (build info False ty)

3637 (cty, _) <- tclift $ recheck ctxt [] ty'

3738 logLvl 2 $ "---> " ++ show cty

38− updateContext (addTyDecl n (normalise ctxt [] cty))

39+ let nty = normalise ctxt [] cty

40+ addDeferred ((n, nty):defer)

3941

4042elabData :: ElabInfo -> PData -> Idris ()

4143elabData info (PDatadecl n t dcons)

42− = do ctxt <- getContext

43− (t', log) <- tclift $ elaborate ctxt n (Set 0) (build info False t)

44+ = do checkUndefined n

45+ ctxt <- getContext

46+ ((t', defer), log) <- tclift $ elaborate ctxt n (Set 0) (build info False t)

47+ addDeferred defer

4448 (cty, _) <- tclift $ recheck ctxt [] t'

4549 logLvl 2 $ "---> " ++ show cty

4650 updateContext (addTyDecl n cty) -- temporary, to check cons

@@ -49,17 +53,20 @@ elabData info (PDatadecl n t dcons)

4953

5054elabCon :: ElabInfo -> (Name, PTerm) -> Idris (Name, Type)

5155elabCon info (n, t)

52− = do ctxt <- getContext

56+ = do checkUndefined n

57+ ctxt <- getContext

5358 logLvl 2 $ "Constructor " ++ show n ++ " : " ++ showImp True t

54− (t', log) <- tclift $ elaborate ctxt n (Set 0) (build info False t)

59+ ((t', defer), log) <- tclift $ elaborate ctxt n (Set 0) (build info False t)

5560-- logLvl 2 $ "Rechecking " ++ show t'

61+ addDeferred defer

5662 (cty, _) <- tclift $ recheck ctxt [] t'

5763 logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty

5864 return (n, cty)

5965

6066elabClauses :: ElabInfo -> Name -> [PClause] -> Idris ()

6167elabClauses info n_in cs = let n = liftname info n_in in

62− do pats <- mapM (elabClause info) cs

68+ do solveDeferred n

69+ pats <- mapM (elabClause info) cs

6370 logLvl 3 (showSep "\n" (map (\ (l,r) ->

6471 show l ++ " = " ++

6572 show r) pats))

@@ -78,8 +85,8 @@ elabVal :: ElabInfo -> PTerm -> Idris (Term, Type)

7885elabVal info tm

7986 = do ctxt <- getContext

8087 logLvl 10 (show tm)

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

82− (build info False (infTerm tm))

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

89+ (build info False (infTerm tm))

8390 logLvl 3 ("Value: " ++ show tm')

8491 let vtm = getInferTerm tm'

8592 logLvl 2 (show vtm)

@@ -90,8 +97,8 @@ elabClause info (PClause fname lhs rhs whereblock)

9097 = do ctxt <- getContext

9198 -- Build the LHS as an "Infer", and pull out its type and

9299 -- pattern bindings

93− (lhs', _) <- tclift $ elaborate ctxt (MN 0 "patLHS") infP

94− (build info True (infTerm lhs))

100+ ((lhs', dlhs), _) <- tclift $ elaborate ctxt (MN 0 "patLHS") infP

101+ (build info True (infTerm lhs))

95102 let lhs_tm = getInferTerm lhs'

96103 let lhs_ty = getInferType lhs'

97104 logLvl 3 (show lhs_tm)

@@ -104,12 +111,15 @@ elabClause info (PClause fname lhs rhs whereblock)

104111 -- Now build the RHS, using the type of the LHS as the goal.

105112 logLvl 2 (showImp True rhs)

106113 ctxt <- getContext -- new context with where block added

107− (rhs', _) <- tclift $ elaborate ctxt (MN 0 "patRHS") clhsty

108− (do pbinds lhs_tm

109− build winfo False rhs

110− psolve lhs_tm

111− get_term)

114+ ((rhs', defer), _) <- tclift $ elaborate ctxt (MN 0 "patRHS") clhsty

115+ (do pbinds lhs_tm

116+ (_, d) <- build winfo False rhs

117+ psolve lhs_tm

118+ tt <- get_term

119+ return (tt, d))

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

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

122+ addDeferred defer

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

114124 return (clhs, crhs)

115125 where

@@ -165,9 +175,12 @@ elabDecl' info (PParams ns ps) = mapM_ (elabDecl' pinfo) ps

165175-- If building a pattern match, we convert undeclared variables from

166176-- holes to pattern bindings.

167177

168−build :: ElabInfo -> Bool -> PTerm -> Elab Term

178+-- Also find deferred names in the term and their types

179+

180+build :: ElabInfo -> Bool -> PTerm -> Elab (Term, [(Name, Type)])

169181build info pattern tm = do elab info pattern tm

170− get_term

182+ tt <- get_term

183+ return $ runState (collectDeferred tt) []

171184

172185elab :: ElabInfo -> Bool -> PTerm -> Elab ()

173186elab info pattern tm = do elab' tm

@@ -235,12 +248,28 @@ elab info pattern tm = do elab' tm

235248 = do simple_app (elab' f) (elab' (getTm arg))

236249 solve

237250 elab' Placeholder = fail $ "Can't deal with a placeholder here"

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

238252 elab' (PElabError e) = fail e

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

240254

241255 elabArgs [] _ = return ()

242256 elabArgs (n:ns) (Placeholder : args) = elabArgs ns args

243257 elabArgs (n:ns) (t : args) = do focus n; elab' t; elabArgs ns args

244−

258+

259+collectDeferred :: Term -> State [(Name, Type)] Term

260+collectDeferred (Bind n (GHole t) app) =

261+ do ds <- get

262+ put ((n, t) : ds)

263+ return app

264+collectDeferred (Bind n b t) = do b' <- cdb b

265+ t' <- collectDeferred t

266+ return (Bind n b' t')

267+ where

268+ cdb (Let t v) = liftM2 Let (collectDeferred t) (collectDeferred v)

269+ cdb (Guess t v) = liftM2 Guess (collectDeferred t) (collectDeferred v)

270+ cdb b = do ty' <- collectDeferred (binderTy b)

271+ return (b { binderTy = ty' })

272+collectDeferred (App f a) = liftM2 App (collectDeferred f) (collectDeferred a)

273+collectDeferred t = return t

245274

246275

src/Idris/Parser.hs+1

@@ -212,6 +212,7 @@ pfName = try iName

212212pSimpleExpr syn =

213213 try (do symbol "!["; t <- pTerm; lchar ']'

214214 return $ PQuote t)

215+ <|> try (do lchar '?'; x <- iName; return (PMetavar x))

215216 <|> try (do reserved "return"; return PReturn)

216217 <|> try (do x <- pfName; return (PRef x))

217218 <|> try (do lchar '('; l <- pExpr syn; lchar ','; r <- pExpr syn; lchar ')';

src/Idris/REPL.hs+6−1

@@ -16,7 +16,7 @@ import Core.TT

1616import System.Console.Readline

1717import Control.Monad

1818import Control.Monad.State

19−

19+import Data.List

2020

2121repl :: Idris ()

2222repl = do x <- lift $ readline "Idris> "

@@ -54,5 +54,10 @@ process TTShell = do ist <- get

5454 shst' <- lift $ runShell shst

5555 return ()

5656process (Compile f) = do compile f

57+process Metavars = do ist <- get

58+ let mvs = idris_metavars ist \\ primDefs

59+ case mvs of

60+ [] -> iputStrLn "No global metavariables to solve"

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

5762process NOP = return ()

5863

src/Idris/REPLParser.hs+1

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

2323 <|> try (do cmd ["h", "?", "help"]; return Help)

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

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

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

2627 <|> do t <- pFullExpr defaultSyntax; return (Eval t)

2728 <|> do eof; return NOP