60c4ef9 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Added 'impossible' keyword

60c4ef9Edwin Brady15 years ago

idris.cabal+2−1

compare with master

unifiedsplit

@@ -32,7 +32,8 @@ Executable idris

32 Idris.AbsSyntax, Idris.Parser, Idris.REPL,

33 Idris.REPLParser, Idris.ElabDecls, Idris.Error,

34 Idris.Delaborate, Idris.Primitives, Idris.Imports,

35− Idris.Compiler, Idris.Prover, Idris.ElabTerm

35+ Idris.Compiler, Idris.Prover, Idris.ElabTerm,

36+ Idris.Coverage,

37 Paths_idris

38 Paths_idris

lib/prelude/vect.idr+2

@@ -21,6 +21,8 @@ data Vect : Set -> Nat -> Set where

21lookup : Fin n -> Vect a n -> a;

22lookup fO (x :: xs) = x;

23lookup (fS k) (x :: xs) = lookup k xs;

24+lookup fO [] impossible;

25+lookup (fS k) [] impossible;

25app : Vect a n -> Vect a m -> Vect a (n + m);

27app : Vect a n -> Vect a m -> Vect a (n + m);

26app [] ys = ys;

28app [] ys = ys;

src/Core/CoreParser.hs+1−1

@@ -20,7 +20,7 @@ idrisDef = haskellDef {

20 identLetter = identLetter haskellDef <|> lchar '.',

21 reservedOpNames = [":", "..", "=", "\\", "|", "<-", "->", "=>", "**"],

22 reservedNames = ["let", "in", "data", "Set", -- "if", "then", "else",

23− "do", "dsl", "import", -- "refl",

23+ "do", "dsl", "import", "impossible", -- "refl",

24 "infix", "infixl", "infixr", "prefix",

25 "where", "with", "forall", "syntax", "proof",

26 "using", "params", "namespace", "class", "instance",

src/Idris/AbsSyntax.hs+6−2

@@ -243,10 +243,13 @@ impl = Imp False Dynamic

243expl = Exp False Dynamic

244constraint = Constraint False Static

245

246+data FnOpt = Inlinable | Partial

247+ deriving (Show, Eq)

248+

246−type FnOpts = Bool -- just inlinable, for now

249+type FnOpts = [FnOpt]

247

250

248inlinable :: FnOpts -> Bool

251inlinable :: FnOpts -> Bool

249−inlinable x = x

252+inlinable = elem Inlinable

250

253

251data PDecl' t = PFix FC Fixity [String] -- fixity declaration

254data PDecl' t = PFix FC Fixity [String] -- fixity declaration

252 | PTy SyntaxInfo FC Name t -- type declaration

255 | PTy SyntaxInfo FC Name t -- type declaration

@@ -343,6 +346,7 @@ data PTerm = PQuote Raw

343 | PProof [PTactic]

346 | PProof [PTactic]

344 | PTactics [PTactic] -- as PProof, but no auto solving

347 | PTactics [PTactic] -- as PProof, but no auto solving

345 | PElabError String -- error to report on elaboration

348 | PElabError String -- error to report on elaboration

349+ | PImpossible -- special case for declaring when an LHS can't typecheck

346 deriving Eq

350 deriving Eq

347

351

348mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm

352mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm

src/Idris/Coverage.hsnew file+11

@@ -0,0 +1,11 @@

1+module Idris.Coverage where

3+import Idris.AbsSyntax

5+-- Given a list of LHSs, generate a complete collection of clauses which cover all

6+-- cases. The ones which haven't been provided are marked 'absurd' so that the

7+-- checker will make sure they can't happen.

9+genClauses :: [PClause] -> [PClause]

10+genClauses xs = xs

11+

src/Idris/ElabDecls.hs+24−10

@@ -7,6 +7,7 @@ import Idris.Error

7import Idris.Delaborate

8import Idris.Imports

9import Idris.ElabTerm

10+import Idris.Coverage

10import Paths_idris

11import Paths_idris

12import Core.TT

13import Core.TT

@@ -18,6 +19,7 @@ import Core.CaseTree

18import Control.Monad

19import Control.Monad

19import Control.Monad.State

20import Control.Monad.State

20import Data.List

21import Data.List

22+import Data.Maybe

21import Debug.Trace

23import Debug.Trace

@@ -85,9 +87,11 @@ elabCon info syn (n, t_in, fc)

85 return (n, cty)

87 return (n, cty)

87elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()

89elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()

88−elabClauses info fc opts n_in cs = let n = liftname info n_in in

90+elabClauses info fc opts n_in cs_in = let n = liftname info n_in in

91+ do let cs = genClauses cs_in

89− do solveDeferred n

92+ solveDeferred n

90− pats <- mapM (elabClause info fc) cs

93+ pats_in <- mapM (elabClause info fc) cs

94+ let pats = mapMaybe id pats_in

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

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

92 show l ++ " = " ++

96 show l ++ " = " ++

93 show r) pats))

97 show r) pats))

@@ -127,7 +131,17 @@ elabVal info aspat tm_in

127 logLvl 2 (show vtm)

131 logLvl 2 (show vtm)

128 recheckC ctxt (FC "prompt" 0) [] vtm

132 recheckC ctxt (FC "prompt" 0) [] vtm

129

133

130−elabClause :: ElabInfo -> FC -> PClause -> Idris (Term, Term)

134+elabClause :: ElabInfo -> FC -> PClause -> Idris (Maybe (Term, Term))

135+elabClause info fc (PClause fname lhs_in [] PImpossible [])

136+ = do ctxt <- getContext

137+ i <- get

138+ let lhs = addImpl i lhs_in

139+ -- if the LHS type checks, it is possible, so report an error

140+ case elaborate ctxt (MN 0 "patLHS") infP

141+ (erun fc (build i info True (infTerm lhs))) of

142+ OK _ -> fail $ show fc ++ ":" ++ show lhs ++ " is a possible case"

143+ Error _ -> return ()

144+ return Nothing

131elabClause info fc (PClause fname lhs_in withs rhs_in whereblock)

145elabClause info fc (PClause fname lhs_in withs rhs_in whereblock)

132 = do ctxt <- getContext

146 = do ctxt <- getContext

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

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

@@ -171,7 +185,7 @@ elabClause info fc (PClause fname lhs_in withs rhs_in whereblock)

171 addDeferred def'

185 addDeferred def'

172 ctxt <- getContext

186 ctxt <- getContext

173 (crhs, crhsty) <- recheckC ctxt fc [] rhs'

187 (crhs, crhsty) <- recheckC ctxt fc [] rhs'

174− return (clhs, crhs)

188+ return $ Just (clhs, crhs)

175 where

189 where

176 decorate x = UN (show fname ++ "#" ++ show x)

190 decorate x = UN (show fname ++ "#" ++ show x)

177 pinfo ns ps i

191 pinfo ns ps i

@@ -253,7 +267,7 @@ elabClause info fc (PWith fname lhs_in withs wval_in withblock)

253 def' <- checkDef fc defer

267 def' <- checkDef fc defer

254 addDeferred def'

268 addDeferred def'

255 (crhs, crhsty) <- recheckC ctxt fc [] rhs'

269 (crhs, crhsty) <- recheckC ctxt fc [] rhs'

256− return (clhs, crhs)

270+ return $ Just (clhs, crhs)

257 where

271 where

258 getImps (Bind n (Pi _) t) = pexp Placeholder : getImps t

272 getImps (Bind n (Pi _) t) = pexp Placeholder : getImps t

259 getImps _ = []

273 getImps _ = []

@@ -364,7 +378,7 @@ elabClass info syn fc constraints tn ps ds

364 iLOG (showImp True ty)

378 iLOG (showImp True ty)

365 iLOG (showImp True lhs ++ " = " ++ showImp True rhs)

379 iLOG (showImp True lhs ++ " = " ++ showImp True rhs)

366 return [PTy syn fc cfn ty,

380 return [PTy syn fc cfn ty,

367− PClauses fc True cfn [PClause cfn lhs [] rhs []]]

381+ PClauses fc [Inlinable] cfn [PClause cfn lhs [] rhs []]]

368

382

369 tfun cn c syn all (m, ty)

383 tfun cn c syn all (m, ty)

370 = do let ty' = insertConstraint c ty

384 = do let ty' = insertConstraint c ty

@@ -378,7 +392,7 @@ elabClass info syn fc constraints tn ps ds

378 iLOG (show (m, ty', capp, margs))

392 iLOG (show (m, ty', capp, margs))

379 iLOG (showImp True lhs ++ " = " ++ showImp True rhs)

393 iLOG (showImp True lhs ++ " = " ++ showImp True rhs)

380 return [PTy syn fc m ty',

394 return [PTy syn fc m ty',

381− PClauses fc True m [PClause m lhs [] rhs []]]

395+ PClauses fc [Inlinable] m [PClause m lhs [] rhs []]]

382

396

383 getMArgs (PPi (Imp _ _) n ty sc) = IA : getMArgs sc

397 getMArgs (PPi (Imp _ _) n ty sc) = IA : getMArgs sc

384 getMArgs (PPi (Exp _ _) n ty sc) = EA : getMArgs sc

398 getMArgs (PPi (Exp _ _) n ty sc) = EA : getMArgs sc

@@ -434,7 +448,7 @@ elabInstance info syn fc cs n ps t ds

434 let lhs = PRef fc iname

448 let lhs = PRef fc iname

435 let rhs = PApp fc (PRef fc (instanceName ci))

449 let rhs = PApp fc (PRef fc (instanceName ci))

436 (map (pexp . mkMethApp) mtys)

450 (map (pexp . mkMethApp) mtys)

437− let idecl = PClauses fc True iname [PClause iname lhs [] rhs wb]

451+ let idecl = PClauses fc [Inlinable] iname [PClause iname lhs [] rhs wb]

438 iLOG (show idecl)

452 iLOG (show idecl)

439 elabDecl info idecl

453 elabDecl info idecl

440 where

454 where

@@ -472,7 +486,7 @@ elabInstance info syn fc cs n ps t ds

472

486

473 insertDef meth def ns decls

487 insertDef meth def ns decls

474 | null $ filter (clauseFor meth ns) decls

488 | null $ filter (clauseFor meth ns) decls

475− = decls ++ [PClauses fc True meth

489+ = decls ++ [PClauses fc [Inlinable] meth

476 [PClause meth (PApp fc (PRef fc meth) []) []

490 [PClause meth (PApp fc (PRef fc meth) []) []

477 (PApp fc (PRef fc def) []) []]]

491 (PApp fc (PRef fc def) []) []]]

478 | otherwise = decls

492 | otherwise = decls

src/Idris/Parser.hs+2−1

@@ -698,7 +698,7 @@ pSimpleCon syn

698pPattern :: SyntaxInfo -> IParser PDecl

699pPattern syn = do clause <- pClause syn

700 fc <- pfc

701− return (PClauses fc False (MN 2 "_") [clause]) -- collect together later

701+ return (PClauses fc [] (MN 2 "_") [clause]) -- collect together later

702

703pArgExpr syn = let syn' = syn { inPattern = True } in

704 try (pHSimpleExpr syn') <|> pSimpleExtExpr syn'

@@ -707,6 +707,7 @@ pRHS :: SyntaxInfo -> Name -> IParser PTerm

707pRHS syn n = do lchar '='; pExpr syn

708 <|> do symbol "?="; rhs <- pExpr syn;

709 return (PLet (UN "value") Placeholder rhs (PMetavar n'))

710+ <|> do reserved "impossible"; return PImpossible

710 where n' = case n of

711 where n' = case n of

711 UN x -> UN (x++"_lemma_1")

712 UN x -> UN (x++"_lemma_1")

712 x -> x

713 x -> x