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

git.iko.soy/Idris-dev

Added 'impossible' keyword

commit60c4ef9598faa4adc813c81b15ae9a40e01d81e6 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateMon 5 Dec 2011, 12:15 (15 years ago) parent7384683

7 files changed+48−15

compare with master

unifiedsplit

idris.cabal+2−1 lib/prelude/vect.idr+2 src/Core/CoreParser.hs+1−1 src/Idris/AbsSyntax.hs+6−2 src/Idris/Coverage.hs+11 src/Idris/ElabDecls.hs+24−10 src/Idris/Parser.hs+2−1

idris.cabal+2−1

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

3232 Idris.AbsSyntax, Idris.Parser, Idris.REPL,

3333 Idris.REPLParser, Idris.ElabDecls, Idris.Error,

3434 Idris.Delaborate, Idris.Primitives, Idris.Imports,

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

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

36+ Idris.Coverage,

3637

3738 Paths_idris

3839

lib/prelude/vect.idr+2

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

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

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

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

24+lookup fO [] impossible;

25+lookup (fS k) [] impossible;

2426

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

2628app [] ys = ys;

src/Core/CoreParser.hs+1−1

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

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

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

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

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

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

2424 "infix", "infixl", "infixr", "prefix",

2525 "where", "with", "forall", "syntax", "proof",

2626 "using", "params", "namespace", "class", "instance",

src/Idris/AbsSyntax.hs+6−2

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

243243expl = Exp False Dynamic

244244constraint = Constraint False Static

245245

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

246+data FnOpt = Inlinable | Partial

247+ deriving (Show, Eq)

248+

249+type FnOpts = [FnOpt]

247250

248251inlinable :: FnOpts -> Bool

249−inlinable x = x

252+inlinable = elem Inlinable

250253

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

252255 | PTy SyntaxInfo FC Name t -- type declaration

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

343346 | PProof [PTactic]

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

345348 | PElabError String -- error to report on elaboration

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

346350 deriving Eq

347351

348352mapPT :: (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

77import Idris.Delaborate

88import Idris.Imports

99import Idris.ElabTerm

10+import Idris.Coverage

1011import Paths_idris

1112

1213import Core.TT

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

1819import Control.Monad

1920import Control.Monad.State

2021import Data.List

22+import Data.Maybe

2123import Debug.Trace

2224

2325

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

8587 return (n, cty)

8688

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

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

89− do solveDeferred n

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

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

91+ do let cs = genClauses cs_in

92+ solveDeferred n

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

94+ let pats = mapMaybe id pats_in

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

9296 show l ++ " = " ++

9397 show r) pats))

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

127131 logLvl 2 (show vtm)

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

129133

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

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

132146 = do ctxt <- getContext

133147 -- 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)

171185 addDeferred def'

172186 ctxt <- getContext

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

174− return (clhs, crhs)

188+ return $ Just (clhs, crhs)

175189 where

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

177191 pinfo ns ps i

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

253267 def' <- checkDef fc defer

254268 addDeferred def'

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

256− return (clhs, crhs)

270+ return $ Just (clhs, crhs)

257271 where

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

259273 getImps _ = []

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

364378 iLOG (showImp True ty)

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

366380 return [PTy syn fc cfn ty,

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

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

368382

369383 tfun cn c syn all (m, ty)

370384 = do let ty' = insertConstraint c ty

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

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

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

380394 return [PTy syn fc m ty',

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

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

382396

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

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

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

434448 let lhs = PRef fc iname

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

436450 (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]

438452 iLOG (show idecl)

439453 elabDecl info idecl

440454 where

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

472486

473487 insertDef meth def ns decls

474488 | null $ filter (clauseFor meth ns) decls

475− = decls ++ [PClauses fc True meth

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

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

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

478492 | otherwise = decls

src/Idris/Parser.hs+2−1

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

698698pPattern :: SyntaxInfo -> IParser PDecl

699699pPattern syn = do clause <- pClause syn

700700 fc <- pfc

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

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

702702

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

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

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

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

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

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

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

710711 where n' = case n of

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

712713 x -> x