Permalink
Browse files

Added 'impossible' keyword

  • Loading branch information...
1 parent 7384683 commit 60c4ef9598faa4adc813c81b15ae9a40e01d81e6 Edwin Brady committed Dec 5, 2011
Showing with 48 additions and 15 deletions.
  1. +2 −1 idris.cabal
  2. +2 −0 lib/prelude/vect.idr
  3. +1 −1 src/Core/CoreParser.hs
  4. +6 −2 src/Idris/AbsSyntax.hs
  5. +11 −0 src/Idris/Coverage.hs
  6. +24 −10 src/Idris/ElabDecls.hs
  7. +2 −1 src/Idris/Parser.hs
View
@@ -32,7 +32,8 @@ Executable idris
Idris.AbsSyntax, Idris.Parser, Idris.REPL,
Idris.REPLParser, Idris.ElabDecls, Idris.Error,
Idris.Delaborate, Idris.Primitives, Idris.Imports,
- Idris.Compiler, Idris.Prover, Idris.ElabTerm
+ Idris.Compiler, Idris.Prover, Idris.ElabTerm,
+ Idris.Coverage,
Paths_idris
View
@@ -21,6 +21,8 @@ data Vect : Set -> Nat -> Set where
lookup : Fin n -> Vect a n -> a;
lookup fO (x :: xs) = x;
lookup (fS k) (x :: xs) = lookup k xs;
+lookup fO [] impossible;
+lookup (fS k) [] impossible;
app : Vect a n -> Vect a m -> Vect a (n + m);
app [] ys = ys;
View
@@ -20,7 +20,7 @@ idrisDef = haskellDef {
identLetter = identLetter haskellDef <|> lchar '.',
reservedOpNames = [":", "..", "=", "\\", "|", "<-", "->", "=>", "**"],
reservedNames = ["let", "in", "data", "Set", -- "if", "then", "else",
- "do", "dsl", "import", -- "refl",
+ "do", "dsl", "import", "impossible", -- "refl",
"infix", "infixl", "infixr", "prefix",
"where", "with", "forall", "syntax", "proof",
"using", "params", "namespace", "class", "instance",
View
@@ -243,10 +243,13 @@ impl = Imp False Dynamic
expl = Exp False Dynamic
constraint = Constraint False Static
-type FnOpts = Bool -- just inlinable, for now
+data FnOpt = Inlinable | Partial
+ deriving (Show, Eq)
+
+type FnOpts = [FnOpt]
inlinable :: FnOpts -> Bool
-inlinable x = x
+inlinable = elem Inlinable
data PDecl' t = PFix FC Fixity [String] -- fixity declaration
| PTy SyntaxInfo FC Name t -- type declaration
@@ -343,6 +346,7 @@ data PTerm = PQuote Raw
| PProof [PTactic]
| PTactics [PTactic] -- as PProof, but no auto solving
| PElabError String -- error to report on elaboration
+ | PImpossible -- special case for declaring when an LHS can't typecheck
deriving Eq
mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
View
@@ -0,0 +1,11 @@
+module Idris.Coverage where
+
+import Idris.AbsSyntax
+
+-- Given a list of LHSs, generate a complete collection of clauses which cover all
+-- cases. The ones which haven't been provided are marked 'absurd' so that the
+-- checker will make sure they can't happen.
+
+genClauses :: [PClause] -> [PClause]
+genClauses xs = xs
+
View
@@ -7,6 +7,7 @@ import Idris.Error
import Idris.Delaborate
import Idris.Imports
import Idris.ElabTerm
+import Idris.Coverage
import Paths_idris
import Core.TT
@@ -18,6 +19,7 @@ import Core.CaseTree
import Control.Monad
import Control.Monad.State
import Data.List
+import Data.Maybe
import Debug.Trace
@@ -85,9 +87,11 @@ elabCon info syn (n, t_in, fc)
return (n, cty)
elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()
-elabClauses info fc opts n_in cs = let n = liftname info n_in in
- do solveDeferred n
- pats <- mapM (elabClause info fc) cs
+elabClauses info fc opts n_in cs_in = let n = liftname info n_in in
+ do let cs = genClauses cs_in
+ solveDeferred n
+ pats_in <- mapM (elabClause info fc) cs
+ let pats = mapMaybe id pats_in
logLvl 3 (showSep "\n" (map (\ (l,r) ->
show l ++ " = " ++
show r) pats))
@@ -127,7 +131,17 @@ elabVal info aspat tm_in
logLvl 2 (show vtm)
recheckC ctxt (FC "prompt" 0) [] vtm
-elabClause :: ElabInfo -> FC -> PClause -> Idris (Term, Term)
+elabClause :: ElabInfo -> FC -> PClause -> Idris (Maybe (Term, Term))
+elabClause info fc (PClause fname lhs_in [] PImpossible [])
+ = do ctxt <- getContext
+ i <- get
+ let lhs = addImpl i lhs_in
+ -- if the LHS type checks, it is possible, so report an error
+ case elaborate ctxt (MN 0 "patLHS") infP
+ (erun fc (build i info True (infTerm lhs))) of
+ OK _ -> fail $ show fc ++ ":" ++ show lhs ++ " is a possible case"
+ Error _ -> return ()
+ return Nothing
elabClause info fc (PClause fname lhs_in withs rhs_in whereblock)
= do ctxt <- getContext
-- 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)
addDeferred def'
ctxt <- getContext
(crhs, crhsty) <- recheckC ctxt fc [] rhs'
- return (clhs, crhs)
+ return $ Just (clhs, crhs)
where
decorate x = UN (show fname ++ "#" ++ show x)
pinfo ns ps i
@@ -253,7 +267,7 @@ elabClause info fc (PWith fname lhs_in withs wval_in withblock)
def' <- checkDef fc defer
addDeferred def'
(crhs, crhsty) <- recheckC ctxt fc [] rhs'
- return (clhs, crhs)
+ return $ Just (clhs, crhs)
where
getImps (Bind n (Pi _) t) = pexp Placeholder : getImps t
getImps _ = []
@@ -364,7 +378,7 @@ elabClass info syn fc constraints tn ps ds
iLOG (showImp True ty)
iLOG (showImp True lhs ++ " = " ++ showImp True rhs)
return [PTy syn fc cfn ty,
- PClauses fc True cfn [PClause cfn lhs [] rhs []]]
+ PClauses fc [Inlinable] cfn [PClause cfn lhs [] rhs []]]
tfun cn c syn all (m, ty)
= do let ty' = insertConstraint c ty
@@ -378,7 +392,7 @@ elabClass info syn fc constraints tn ps ds
iLOG (show (m, ty', capp, margs))
iLOG (showImp True lhs ++ " = " ++ showImp True rhs)
return [PTy syn fc m ty',
- PClauses fc True m [PClause m lhs [] rhs []]]
+ PClauses fc [Inlinable] m [PClause m lhs [] rhs []]]
getMArgs (PPi (Imp _ _) n ty sc) = IA : getMArgs sc
getMArgs (PPi (Exp _ _) n ty sc) = EA : getMArgs sc
@@ -434,7 +448,7 @@ elabInstance info syn fc cs n ps t ds
let lhs = PRef fc iname
let rhs = PApp fc (PRef fc (instanceName ci))
(map (pexp . mkMethApp) mtys)
- let idecl = PClauses fc True iname [PClause iname lhs [] rhs wb]
+ let idecl = PClauses fc [Inlinable] iname [PClause iname lhs [] rhs wb]
iLOG (show idecl)
elabDecl info idecl
where
@@ -472,7 +486,7 @@ elabInstance info syn fc cs n ps t ds
insertDef meth def ns decls
| null $ filter (clauseFor meth ns) decls
- = decls ++ [PClauses fc True meth
+ = decls ++ [PClauses fc [Inlinable] meth
[PClause meth (PApp fc (PRef fc meth) []) []
(PApp fc (PRef fc def) []) []]]
| otherwise = decls
View
@@ -698,7 +698,7 @@ pSimpleCon syn
pPattern :: SyntaxInfo -> IParser PDecl
pPattern syn = do clause <- pClause syn
fc <- pfc
- return (PClauses fc False (MN 2 "_") [clause]) -- collect together later
+ return (PClauses fc [] (MN 2 "_") [clause]) -- collect together later
pArgExpr syn = let syn' = syn { inPattern = True } in
try (pHSimpleExpr syn') <|> pSimpleExtExpr syn'
@@ -707,6 +707,7 @@ pRHS :: SyntaxInfo -> Name -> IParser PTerm
pRHS syn n = do lchar '='; pExpr syn
<|> do symbol "?="; rhs <- pExpr syn;
return (PLet (UN "value") Placeholder rhs (PMetavar n'))
+ <|> do reserved "impossible"; return PImpossible
where n' = case n of
UN x -> UN (x++"_lemma_1")
x -> x

0 comments on commit 60c4ef9

Please sign in to comment.