git.iko.soy/Idris-dev
on master help sign in
Merge remote-tracking branch 'upstream/master' into error-reflection
commite6c3f565e5a990a0a03748af2ae4df9eb7e59742 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateMon 13 Jan 2014, 08:55 (13 years ago) parent037b4a423787c2
18 files changed+312−189
compare with master
unifiedsplit
CHANGELOG+2 libs/effects/Effect/Memory.idr+2−2 libs/prelude/Prelude/Either.idr+11 src/IRTS/Compiler.hs+1−1 src/Idris/Completion.hs+1 src/Idris/Core/CaseTree.hs+103−36 src/Idris/Core/Evaluate.hs+22−20 src/Idris/Core/Execute.hs+4−4 src/Idris/Core/ProofState.hs+22−12 src/Idris/Core/Unify.hs+16−8 src/Idris/Coverage.hs+2−2 src/Idris/ElabDecls.hs+20−18 src/Idris/ElabTerm.hs+71−52 src/Idris/IBC.hs+11−9 src/Idris/Prover.hs+2−1 src/Idris/REPL.hs+15−22 src/Util/DynamicLinker.hs+6−2 test/reg005/reg005.idr+1
CHANGELOG+2
@@ -1,6 +1,8 @@
11New in 0.9.11:
22-------------
3+
34* Agda-style equational reasoning (in Syntax.PreorderReasoning)
5+* 'case' construct now abstracts over the scrutinee in its type
46
57New in 0.9.10:
68--------------
libs/effects/Effect/Memory.idr+2−2
@@ -80,8 +80,8 @@ instance Handler RawMemory (IOExcept String) where
8080 handle () (Allocate n) k
8181 = do ptr <- do_malloc n
8282 k (CH ptr) ()
83− handle {res = MemoryChunk _ offset} (CH ptr) (Initialize c size _) k
84− = ioe_lift (do_memset ptr offset c size) $> k (CH ptr) ()
83+ handle (CH ptr) (Initialize {i} c size _) k
84+ = ioe_lift (do_memset ptr i c size) $> k (CH ptr) ()
8585 handle (CH ptr) (Free) k
8686 = ioe_lift (do_free ptr) $> k () ()
8787 handle (CH ptr) (Peek offset size _) k
libs/prelude/Prelude/Either.idr+11
@@ -63,6 +63,17 @@ maybeToEither def (Just j) = Right j
6363maybeToEither def Nothing = Left def
6464
6565
66+--------------------------------------------------------------------------------
67+-- Instances
68+--------------------------------------------------------------------------------
69+
70+instance (Eq a, Eq b) => Eq (Either a b) where
71+ (==) (Left x) (Left y) = x == y
72+ (==) (Right x) (Right y) = x == y
73+ (==) _ _ = False
74+
75+
76+
6677--------------------------------------------------------------------------------
6778-- Injectivity of constructors
6879--------------------------------------------------------------------------------
src/IRTS/Compiler.hs+1−1
@@ -157,7 +157,7 @@ declArgs args inl n x = LFun (if inl then [Inline] else []) n args x
157157
158158mkLDecl n (Function tm _) = do e <- ir tm
159159 return (declArgs [] True n e)
160−mkLDecl n (CaseOp ci _ _ pats cd)
160+mkLDecl n (CaseOp ci _ _ _ pats cd)
161161 = let (args, sc) = cases_runtime cd in
162162 do e <- ir (args, sc)
163163 return (declArgs [] (case_inlinable ci) n e)
src/Idris/Completion.hs+1
@@ -44,6 +44,7 @@ tacticArgs = [ ("intro", Nothing) -- FIXME syntax for intro (fresh name)
4444 , ("reflect", Just ExprTArg)
4545 , ("fill", Just ExprTArg)
4646 , ("try", Just AltsTArg)
47+ , ("induction", Just NameTArg)
4748 ] ++ map (\x -> (x, Nothing)) [
4849 "intros", "compute", "trivial", "solve", "attack",
4950 "state", "term", "undo", "qed", "abandon", ":q"
src/Idris/Core/CaseTree.hs+103−36
@@ -67,7 +67,7 @@ instance Show t => Show (SC' t) where
6767
6868type CaseTree = SC
6969type Clause = ([Pat], (Term, Term))
70−type CS = ([Term], Int)
70+type CS = ([Term], Int, [(Name, Type)])
7171
7272instance TermSize SC where
7373 termsize n (Case n' as) = termsize n as
@@ -183,9 +183,10 @@ data Phase = CompileTime | RunTime
183183-- Work Right to Left
184184
185185simpleCase :: Bool -> Bool -> Bool ->
186− Phase -> FC -> [([Name], Term, Term)] ->
186+ Phase -> FC -> [Type] ->
187+ [([Name], Term, Term)] ->
187188 TC CaseDef
188−simpleCase tc cover reflect phase fc cs
189+simpleCase tc cover reflect phase fc argtys cs
189190 = sc' tc cover phase fc (filter (\(_, _, r) ->
190191 case r of
191192 Impossible -> False
@@ -195,6 +196,7 @@ simpleCase tc cover reflect phase fc cs
195196 = return $ CaseDef [] (UnmatchedCase "No pattern clauses") []
196197 sc' tc cover phase fc cs
197198 = let proj = phase == RunTime
199+ vnames = fstT (head cs)
198200 pats = map (\ (avs, l, r) ->
199201 (avs, toPats reflect tc l, (l, r))) cs
200202 chkPats = mapM chkAccessible pats in
@@ -204,13 +206,19 @@ simpleCase tc cover reflect phase fc cs
204206 ns = take numargs args
205207 (ns', ps') = order ns pats
206208 (tree, st) = runState
207− (match ns' ps' (defaultCase cover)) ([], numargs)
208− t = CaseDef ns (prune proj (depatt ns' tree)) (fst st) in
209− if proj then return (stripLambdas t) else return t
209+ (match ns' ps' (defaultCase cover))
210+ ([], numargs, [])
211+ t = CaseDef ns (prune proj (depatt ns' tree)) (fstT st) in
212+ if proj then return (stripLambdas t)
213+ else if checkSameTypes (lstT st) tree
214+ then return t
215+ else Error (At fc (Msg "Typecase is not allowed"))
210216 Error err -> Error (At fc err)
211217 where args = map (\i -> MN i "e") [0..]
212218 defaultCase True = STerm Erased
213219 defaultCase False = UnmatchedCase "Error"
220+ fstT (x, _, _) = x
221+ lstT (_, _, x) = x
214222
215223 chkAccessible (avs, l, c)
216224 | phase == RunTime || reflect = return (l, c)
@@ -218,17 +226,62 @@ simpleCase tc cover reflect phase fc cs
218226 return (l, c)
219227
220228 acc [] n = Error (Inaccessible n)
221− acc (PV x : xs) n | x == n = OK ()
229+ acc (PV x t : xs) n | x == n = OK ()
222230 acc (PCon _ _ ps : xs) n = acc (ps ++ xs) n
223231 acc (PSuc p : xs) n = acc (p : xs) n
224232 acc (_ : xs) n = acc xs n
225233
234+-- For each 'Case', make sure every choice is in the same type family,
235+-- as directed by the variable type (i.e. there is no implicit type casing
236+-- going on).
237+
238+checkSameTypes :: [(Name, Type)] -> SC -> Bool
239+checkSameTypes tys (Case n alts)
240+ = case lookup n tys of
241+ Just t -> and (map (checkAlts t) alts)
242+ _ -> and (map ((checkSameTypes tys).getSC) alts)
243+ where
244+ checkAlts t (ConCase n _ _ sc) = isType n t && checkSameTypes tys sc
245+ checkAlts (Constant t) (ConstCase c sc) = isConstType c t && checkSameTypes tys sc
246+ checkAlts _ (ConstCase c sc) = False
247+ checkAlts _ _ = True
248+
249+ getSC (ConCase _ _ _ sc) = sc
250+ getSC (FnCase _ _ sc) = sc
251+ getSC (ConstCase _ sc) = sc
252+ getSC (SucCase _ sc) = sc
253+ getSC (DefaultCase sc) = sc
254+checkSameTypes _ _ = True
255+
256+-- FIXME: All we're actually doing here is checking that we haven't arrived
257+-- at a specific constructor for a polymorphic argument. I *think* this
258+-- is sufficient, but if it turns out not to be, fix it!
259+isType n t | (P (TCon _ _) _ _, _) <- unApply t = True
260+isType n t | (P Ref _ _, _) <- unApply t = True
261+isType n t = False
262+
263+isConstType (I _) (AType (ATInt ITNative)) = True
264+isConstType (BI _) (AType (ATInt ITBig)) = True
265+isConstType (Fl _) (AType ATFloat) = True
266+isConstType (Ch _) (AType (ATInt ITChar)) = True
267+isConstType (Str _) StrType = True
268+isConstType (B8 _) (AType (ATInt _)) = True
269+isConstType (B16 _) (AType (ATInt _)) = True
270+isConstType (B32 _) (AType (ATInt _)) = True
271+isConstType (B64 _) (AType (ATInt _)) = True
272+isConstType (B8V _) (AType (ATInt _)) = True
273+isConstType (B16V _) (AType (ATInt _)) = True
274+isConstType (B32V _) (AType (ATInt _)) = True
275+isConstType (B64V _) (AType (ATInt _)) = True
276+isConstType _ _ = False
277+
226278data Pat = PCon Name Int [Pat]
227279 | PConst Const
228− | PV Name
280+ | PV Name Type
229281 | PSuc Pat -- special case for n+1 on Integer
230282 | PReflected Name [Pat]
231283 | PAny
284+ | PTyPat -- typecase, not allowed, inspect last
232285 deriving Show
233286
234287-- If there are repeated variables, take the *last* one (could be name shadowing
@@ -250,25 +303,30 @@ toPat reflect tc tms = evalState (mapM (\x -> toPat' x []) tms) []
250303 = do p' <- toPat' p []
251304 return $ PSuc p'
252305 -- Typecase
253− toPat' (P (TCon t a) n _) args | tc
254− = do args' <- mapM (\x -> toPat' x []) args
255− return $ PCon n t args'
256− toPat' (Constant (AType (ATInt ITNative))) []
257− | tc = return $ PCon (UN "Int") 1 []
258− toPat' (Constant (AType ATFloat)) [] | tc = return $ PCon (UN "Float") 2 []
259− toPat' (Constant (AType (ATInt ITChar))) [] | tc = return $ PCon (UN "Char") 3 []
260− toPat' (Constant StrType) [] | tc = return $ PCon (UN "String") 4 []
261− toPat' (Constant PtrType) [] | tc = return $ PCon (UN "Ptr") 5 []
262− toPat' (Constant (AType (ATInt ITBig))) []
263− | tc = return $ PCon (UN "Integer") 6 []
264− toPat' (Constant (AType (ATInt (ITFixed n)))) []
265− | tc = return $ PCon (UN (fixedN n)) (7 + fromEnum n) [] -- 7-10 inclusive
266− toPat' (P Bound n _) [] = do ns <- get
306+-- toPat' (P (TCon t a) n _) args | tc
307+-- = do args' <- mapM (\x -> toPat' x []) args
308+-- return $ PCon n t args'
309+-- toPat' (Constant (AType (ATInt ITNative))) []
310+-- | tc = return $ PCon (UN "Int") 1 []
311+-- toPat' (Constant (AType ATFloat)) [] | tc = return $ PCon (UN "Float") 2 []
312+-- toPat' (Constant (AType (ATInt ITChar))) [] | tc = return $ PCon (UN "Char") 3 []
313+-- toPat' (Constant StrType) [] | tc = return $ PCon (UN "String") 4 []
314+-- toPat' (Constant PtrType) [] | tc = return $ PCon (UN "Ptr") 5 []
315+-- toPat' (Constant (AType (ATInt ITBig))) []
316+-- | tc = return $ PCon (UN "Integer") 6 []
317+-- toPat' (Constant (AType (ATInt (ITFixed n)))) []
318+-- | tc = return $ PCon (UN (fixedN n)) (7 + fromEnum n) [] -- 7-10 inclusive
319+ toPat' (P Bound n ty) [] = -- trace (show (n, ty)) $
320+ do ns <- get
267321 if n `elem` ns
268322 then return PAny
269323 else do put (n : ns)
270− return (PV n)
324+ return (PV n ty)
271325 toPat' (App f a) args = toPat' f (a : args)
326+ toPat' (Constant (AType _)) [] = return PTyPat
327+ toPat' (Constant StrType) [] = return PTyPat
328+ toPat' (Constant PtrType) [] = return PTyPat
329+ toPat' (Constant VoidType) [] = return PTyPat
272330 toPat' (Constant x) [] = return $ PConst x
273331 toPat' (Bind n (Pi t) sc) [] | reflect && noOccurrence n sc
274332 = do t' <- toPat' t []
@@ -289,9 +347,10 @@ data Partition = Cons [Clause]
289347 | Vars [Clause]
290348 deriving Show
291349
292−isVarPat (PV _ : ps , _) = True
293−isVarPat (PAny : ps , _) = True
294−isVarPat _ = False
350+isVarPat (PV _ _ : ps , _) = True
351+isVarPat (PAny : ps , _) = True
352+isVarPat (PTyPat : ps , _) = True
353+isVarPat _ = False
295354
296355isConPat (PCon _ _ _ : ps, _) = True
297356isConPat (PReflected _ _ : ps, _) = True
@@ -337,8 +396,8 @@ order ns cs = let patnames = transpose (map (zip ns) (map fst cs))
337396match :: [Name] -> [Clause] -> SC -- error case
338397 -> State CS SC
339398match [] (([], ret) : xs) err
340− = do (ts, v) <- get
341− put (ts ++ (map (fst.snd) xs), v)
399+ = do (ts, v, ntys) <- get
400+ put (ts ++ (map (fst.snd) xs), v, ntys)
342401 case snd ret of
343402 Impossible -> return ImpossibleCase
344403 tm -> return $ STerm tm -- run out of arguments
@@ -408,12 +467,17 @@ argsToAlt rs@((r, m) : rest)
408467 return (newArgs, addRs rs)
409468 where
410469 getNewVars [] = return []
411− getNewVars ((PV n) : ns) = do v <- getVar "e"
412− nsv <- getNewVars ns
413− return (v : nsv)
470+ getNewVars ((PV n t) : ns) = do v <- getVar "e"
471+ (cs, i, ntys) <- get
472+ put (cs, i, (v, t) : ntys)
473+ nsv <- getNewVars ns
474+ return (v : nsv)
414475 getNewVars (PAny : ns) = do v <- getVar "i"
415476 nsv <- getNewVars ns
416477 return (v : nsv)
478+ getNewVars (PTyPat : ns) = do v <- getVar "t"
479+ nsv <- getNewVars ns
480+ return (v : nsv)
417481 getNewVars (_ : ns) = do v <- getVar "e"
418482 nsv <- getNewVars ns
419483 return (v : nsv)
@@ -424,7 +488,7 @@ argsToAlt rs@((r, m) : rest)
424488 uniq i n = n
425489
426490getVar :: String -> State CS Name
427−getVar b = do (t, v) <- get; put (t, v+1); return (MN v b)
491+getVar b = do (t, v, ntys) <- get; put (t, v+1, ntys); return (MN v b)
428492
429493groupCons :: [Clause] -> State CS [Group]
430494groupCons cs = gc [] cs
@@ -454,12 +518,15 @@ groupCons cs = gc [] cs
454518
455519varRule :: [Name] -> [Clause] -> SC -> State CS SC
456520varRule (v : vs) alts err =
457− do let alts' = map (repVar v) alts
521+ do alts' <- mapM (repVar v) alts
458522 match vs alts' err
459523 where
460− repVar v (PV p : ps , (lhs, res))
461− = (ps, (lhs, subst p (P Bound v Erased) res))
462− repVar v (PAny : ps , res) = (ps, res)
524+ repVar v (PV p ty : ps , (lhs, res))
525+ = do (cs, i, ntys) <- get
526+ put (cs, i, (v, ty) : ntys)
527+ return (ps, (lhs, subst p (P Bound v ty) res))
528+ repVar v (PAny : ps , res) = return (ps, res)
529+ repVar v (PTyPat : ps , res) = return (ps, res)
463530
464531-- fix: case e of S k -> f (S k) ==> case e of S k -> f e
465532
src/Idris/Core/Evaluate.hs+22−20
@@ -211,7 +211,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
211211 ev ntimes (n:stk) True env tm
212212 [(TyDecl nt ty, _)] -> do vty <- ev ntimes stk True env ty
213213 return $ VP nt n vty
214− [(CaseOp ci _ _ _ cd, acc)]
214+ [(CaseOp ci _ _ _ _ cd, acc)]
215215 | (acc /= Frozen) &&
216216 null (fst (cases_totcheck cd)) -> -- unoptimised version
217217 let (ns, tree) = getCases cd in
@@ -284,7 +284,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
284284 reapply ntimes stk top env f@(VP Ref n ty) args
285285 = let val = lookupDefAcc n (spec || atRepl) ctxt in
286286 case val of
287− [(CaseOp ci _ _ _ cd, acc)] ->
287+ [(CaseOp ci _ _ _ _ cd, acc)] ->
288288 let (ns, tree) = getCases cd in
289289 do c <- evCase ntimes n (n:stk) top env ns args tree
290290 case c of
@@ -310,7 +310,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
310310 if u then
311311 do let val = lookupDefAcc n (spec || atRepl) ctxt
312312 case val of
313− [(CaseOp ci _ _ _ cd, acc)]
313+ [(CaseOp ci _ _ _ _ cd, acc)]
314314 | acc /= Frozen -> -- unoptimised version
315315 let (ns, tree) = getCases cd in
316316 if blockSimplify ci n stk
@@ -561,8 +561,8 @@ convEq ctxt = ceq [] where
561561 sameDefs ps x y = case (lookupDef x ctxt, lookupDef y ctxt) of
562562 ([Function _ xdef], [Function _ ydef])
563563 -> ceq ((x,y):ps) xdef ydef
564− ([CaseOp _ _ _ _ xd],
565− [CaseOp _ _ _ _ yd])
564+ ([CaseOp _ _ _ _ _ xd],
565+ [CaseOp _ _ _ _ _ yd])
566566 -> let (_, xdef) = cases_compiletime xd
567567 (_, ydef) = cases_compiletime yd in
568568 caseeq ((x,y):ps) xdef ydef
@@ -588,6 +588,7 @@ data Def = Function !Type !Term
588588 | Operator Type Int ([Value] -> Maybe Value)
589589 | CaseOp CaseInfo
590590 !Type
591+ ![Type] -- argument types
591592 ![Either Term (Term, Term)] -- original definition
592593 ![([Name], Term, Term)] -- simplified for totality check definition
593594 !CaseDefs
@@ -620,7 +621,7 @@ instance Show Def where
620621 show (Function ty tm) = "Function: " ++ show (ty, tm)
621622 show (TyDecl nt ty) = "TyDecl: " ++ show nt ++ " " ++ show ty
622623 show (Operator ty _ _) = "Operator: " ++ show ty
623− show (CaseOp (CaseInfo inlc inlr) ty ps_in ps cd)
624+ show (CaseOp (CaseInfo inlc inlr) ty atys ps_in ps cd)
624625 = let (ns, sc) = cases_compiletime cd
625626 (ns_t, sc_t) = cases_totcheck cd
626627 (ns', sc') = cases_runtime cd in
@@ -752,6 +753,7 @@ addDatatype (Data n tag ty cons) uctxt
752753
753754-- FIXME: Too many arguments! Refactor all these Bools.
754755addCasedef :: Name -> CaseInfo -> Bool -> Bool -> Bool -> Bool ->
756+ [Type] -> -- argument types
755757 [Either Term (Term, Term)] ->
756758 [([Name], Term, Term)] -> -- totality
757759 [([Name], Term, Term)] -> -- compile time
@@ -759,16 +761,16 @@ addCasedef :: Name -> CaseInfo -> Bool -> Bool -> Bool -> Bool ->
759761 [([Name], Term, Term)] -> -- run time
760762 Type -> Context -> Context
761763addCasedef n ci@(CaseInfo alwaysInline tcdict)
762− tcase covering reflect asserted ps_in
763− ps_tot ps_inl ps_ct ps_rt ty uctxt
764+ tcase covering reflect asserted argtys
765+ ps_in ps_tot ps_inl ps_ct ps_rt ty uctxt
764766 = let ctxt = definitions uctxt
765767 access = case lookupDefAcc n False uctxt of
766768 [(_, acc)] -> acc
767769 _ -> Public
768− ctxt' = case (simpleCase tcase covering reflect CompileTime emptyFC ps_tot,
769− simpleCase tcase covering reflect CompileTime emptyFC ps_ct,
770− simpleCase tcase covering reflect CompileTime emptyFC ps_inl,
771− simpleCase tcase covering reflect RunTime emptyFC ps_rt) of
770+ ctxt' = case (simpleCase tcase covering reflect CompileTime emptyFC argtys ps_tot,
771+ simpleCase tcase covering reflect CompileTime emptyFC argtys ps_ct,
772+ simpleCase tcase covering reflect CompileTime emptyFC argtys ps_inl,
773+ simpleCase tcase covering reflect RunTime emptyFC argtys ps_rt) of
772774 (OK (CaseDef args_tot sc_tot _),
773775 OK (CaseDef args_ct sc_ct _),
774776 OK (CaseDef args_inl sc_inl _),
@@ -781,7 +783,7 @@ addCasedef n ci@(CaseInfo alwaysInline tcdict)
781783 (args_inl, sc_inl)
782784 (args_rt, sc_rt) in
783785 addDef n (CaseOp (ci { case_inlinable = inlc })
784− ty ps_in ps_tot cdef,
786+ ty argtys ps_in ps_tot cdef,
785787 access, Unchecked, EmptyMI) ctxt in
786788 uctxt { definitions = ctxt' }
787789
@@ -790,15 +792,15 @@ simplifyCasedef :: Name -> Context -> Context
790792simplifyCasedef n uctxt
791793 = let ctxt = definitions uctxt
792794 ctxt' = case lookupCtxt n ctxt of
793− [(CaseOp ci ty [] ps _, acc, tot, metainf)] ->
795+ [(CaseOp ci ty atys [] ps _, acc, tot, metainf)] ->
794796 ctxt -- nothing to simplify (or already done...)
795− [(CaseOp ci ty ps_in ps cd, acc, tot, metainf)] ->
797+ [(CaseOp ci ty atys ps_in ps cd, acc, tot, metainf)] ->
796798 let ps_in' = map simpl ps_in
797799 pdef = map debind ps_in' in
798− case simpleCase False True False CompileTime emptyFC pdef of
800+ case simpleCase False True False CompileTime emptyFC atys pdef of
799801 OK (CaseDef args sc _) ->
800802 addDef n (CaseOp ci
801− ty ps_in' ps (cd { cases_totcheck = (args, sc) }),
803+ ty atys ps_in' ps (cd { cases_totcheck = (args, sc) }),
802804 acc, tot, metainf) ctxt
803805 Error err -> error (show err)
804806 _ -> ctxt in
@@ -836,7 +838,7 @@ lookupTy n ctxt
836838 (Function ty _) -> return ty
837839 (TyDecl _ ty) -> return ty
838840 (Operator ty _ _) -> return ty
839− (CaseOp _ ty _ _ _) -> return ty
841+ (CaseOp _ ty _ _ _ _) -> return ty
840842
841843isConName :: Name -> Context -> Bool
842844isConName n ctxt = isTConName n ctxt || isDConName n ctxt
@@ -861,7 +863,7 @@ isFnName n ctxt
861863 case tfst def of
862864 (Function _ _) -> return True
863865 (Operator _ _ _) -> return True
864− (CaseOp _ _ _ _ _) -> return True
866+ (CaseOp _ _ _ _ _ _) -> return True
865867 _ -> return False
866868
867869lookupP :: Name -> Context -> [Term]
@@ -870,7 +872,7 @@ lookupP n ctxt
870872 p <- case def of
871873 (Function ty tm, a, _, _) -> return (P Ref n ty, a)
872874 (TyDecl nt ty, a, _, _) -> return (P nt n ty, a)
873− (CaseOp _ ty _ _ _, a, _, _) -> return (P Ref n ty, a)
875+ (CaseOp _ ty _ _ _ _, a, _, _) -> return (P Ref n ty, a)
874876 (Operator ty _ _, a, _, _) -> return (P Ref n ty, a)
875877 case snd p of
876878 Hidden -> []
src/Idris/Core/Execute.hs+4−4
@@ -188,9 +188,9 @@ doExec env ctxt p@(P Ref n ty) =
188188 [Function _ tm] -> doExec env ctxt tm
189189 [TyDecl _ _] -> return (EP Ref n EErased) -- abstract def
190190 [Operator tp arity op] -> return (EP Ref n EErased) -- will be special-cased later
191− [CaseOp _ _ _ _ (CaseDefs _ ([], STerm tm) _ _)] -> -- nullary fun
191+ [CaseOp _ _ _ _ _ (CaseDefs _ ([], STerm tm) _ _)] -> -- nullary fun
192192 doExec env ctxt tm
193− [CaseOp _ _ _ _ (CaseDefs _ (ns, sc) _ _)] -> return (EP Ref n EErased)
193+ [CaseOp _ _ _ _ _ (CaseDefs _ (ns, sc) _ _)] -> return (EP Ref n EErased)
194194 [] -> execFail $ "Could not find " ++ show n ++ " in definitions."
195195 thing -> trace (take 200 $ "got to " ++ show thing ++ " lookup up " ++ show n) $ undefined
196196doExec env ctxt p@(P Bound n ty) =
@@ -328,10 +328,10 @@ execApp' env ctxt f@(EP _ n _) args =
328328 execApp' env ctxt r (drop arity args)
329329 Nothing -> return (mkEApp f args)
330330 else return (mkEApp f args)
331− [CaseOp _ _ _ _ (CaseDefs _ ([], STerm tm) _ _)] -> -- nullary fun
331+ [CaseOp _ _ _ _ _ (CaseDefs _ ([], STerm tm) _ _)] -> -- nullary fun
332332 do rhs <- doExec env ctxt tm
333333 execApp' env ctxt rhs args
334− [CaseOp _ _ _ _ (CaseDefs _ (ns, sc) _ _)] ->
334+ [CaseOp _ _ _ _ _ (CaseDefs _ (ns, sc) _ _)] ->
335335 do res <- execCase env ctxt ns sc args
336336 return $ fromMaybe (mkEApp f args) res
337337 thing -> return $ mkEApp f args
src/Idris/Core/ProofState.hs+22−12
@@ -184,24 +184,26 @@ unify' ctxt env topx topy =
184184 " in " ++ show env ++
185185 "\nHoles: " ++ show (holes ps) ++ "\n") $
186186 lift $ unify ctxt env topx topy dont (holes ps)
187+ let notu = filter (\ (n, t) -> case t of
188+ P _ _ _ -> False
189+ _ -> n `elem` dont) u
187190 traceWhen (unifylog ps)
188191 ("Unified " ++ show (topx, topy) ++ " without " ++ show dont ++
189192 "\nSolved: " ++ show u ++ "\nNew problems: " ++ qshow fails
193+ ++ "\nNot unified:\n" ++ show (notunified ps)
190194 ++ "\nCurrent problems:\n" ++ qshow (problems ps)
191195-- ++ show (pterm ps)
192196 ++ "\n----------") $
193− case fails of
194−-- [] -> return u
195− err ->
196− do ps <- get
197− let (h, ns) = unified ps
198− let (ns', probs') = updateProblems (context ps) (u ++ ns)
199− (err ++ problems ps)
200− (injective ps)
201− (holes ps)
202− put (ps { problems = probs',
203− unified = (h, ns') })
204− return u
197+ do ps <- get
198+ let (h, ns) = unified ps
199+ let (ns', probs') = updateProblems (context ps) (u ++ ns)
200+ (fails ++ problems ps)
201+ (injective ps)
202+ (holes ps)
203+ put (ps { problems = probs',
204+ unified = (h, ns'),
205+ notunified = notu ++ notunified ps })
206+ return u
205207
206208getName :: Monad m => String -> StateT TState m Name
207209getName tag = do ps <- get
@@ -760,6 +762,11 @@ solveInProblems x val ((l, r, env, err) : ps)
760762 = ((instantiate val (pToV x l), instantiate val (pToV x r),
761763 updateEnv [(x, val)] env, err) : solveInProblems x val ps)
762764
765+updateNotunified ns nu = up nu where
766+ up [] = []
767+ up ((n, t) : ns) = let t' = updateSolved ns t in
768+ ((n, t') : up ns)
769+
763770updateProblems ctxt ns ps inj holes = up ns ps where
764771 up ns [] = (ns, [])
765772 up ns ((x, y, env, err) : ps) =
@@ -809,6 +816,7 @@ processTactic EndUnify ps
809816 return (ps { pterm = tm',
810817 unified = (h, []),
811818 problems = probs',
819+ notunified = updateNotunified ns (notunified ps),
812820 holes = holes ps \\ map fst ns'' }, "")
813821processTactic (Reorder n) ps
814822 = do ps' <- execStateT (tactic (Just n) reorder_claims) ps
@@ -823,6 +831,7 @@ processTactic UnifyProblems ps
823831 pterm' = updateSolved ns' (pterm ps) in
824832 return (ps { pterm = pterm', solved = Nothing, problems = probs',
825833 previous = Just ps, plog = "",
834+ notunified = updateNotunified ns' (notunified ps),
826835 holes = holes ps \\ (map fst ns') }, plog ps)
827836processTactic MatchProblems ps
828837 = let (ns', probs') = matchProblems (context ps)
@@ -850,6 +859,7 @@ processTactic t ps
850859 return (ps' { pterm = pterm'',
851860 solved = Nothing,
852861 problems = probs',
862+ notunified = updateNotunified ns' (notunified ps'),
853863 previous = Just ps, plog = "",
854864 holes = holes ps' \\ (map fst ns')}, plog ps')
855865
src/Idris/Core/Unify.hs+16−8
@@ -35,20 +35,20 @@ match_unify :: Context -> Env -> TT Name -> TT Name -> [Name] -> [Name] ->
3535 TC [(Name, TT Name)]
3636match_unify ctxt env topx topy dont holes =
3737 case runStateT (un [] topx topy) (UI 0 []) of
38− OK (v, UI _ []) -> return (filter notTrivial v)
38+ OK (v, UI _ []) -> return (trimSolutions v)
3939 res ->
4040 let topxn = normalise ctxt env topx
4141 topyn = normalise ctxt env topy in
4242 case runStateT (un [] topxn topyn)
4343 (UI 0 []) of
4444 OK (v, UI _ fails) ->
45− return (filter notTrivial v)
45+ return (trimSolutions v)
4646 Error e ->
4747 -- just normalise the term we're matching against
4848 case runStateT (un [] topxn topy)
4949 (UI 0 []) of
5050 OK (v, UI _ fails) ->
51− return (filter notTrivial v)
51+ return (trimSolutions v)
5252 _ -> tfail e
5353 where
5454 un names (P _ x _) tm
@@ -128,9 +128,17 @@ match_unify ctxt env topx topy dont holes =
128128 where inst [] tm = tm
129129 inst ((n, _) : ns) tm = inst ns (substV (P Bound n Erased) tm)
130130
131−notTrivial (x, P _ x' _) = x /= x'
132−notTrivial _ = True
133−
131+trimSolutions ns = dropPairs ns
132+ where dropPairs [] = []
133+ dropPairs (n@(x, P _ x' _) : ns)
134+ | x == x' = dropPairs ns
135+ | otherwise
136+ = n : dropPairs
137+ (filter (\t -> case t of
138+ (n, P _ n' _) -> not (n == x' && n' == x)
139+ _ -> True) ns)
140+ dropPairs (n : ns) = n : dropPairs ns
141+
134142expandLets env (x, tm) = (x, doSubst (reverse env) tm)
135143 where
136144 doSubst [] tm = tm
@@ -146,7 +154,7 @@ unify ctxt env topx topy dont holes =
146154-- trace ("Unifying " ++ show (topx, topy)) $
147155 -- don't bother if topx and topy are different at the head
148156 case runStateT (un False [] topx topy) (UI 0 []) of
149− OK (v, UI _ []) -> return (filter notTrivial v,
157+ OK (v, UI _ []) -> return (trimSolutions v,
150158 [])
151159 res ->
152160 let topxn = normalise ctxt env topx
@@ -155,7 +163,7 @@ unify ctxt env topx topy dont holes =
155163 case runStateT (un False [] topxn topyn)
156164 (UI 0 []) of
157165 OK (v, UI _ fails) ->
158− return (filter notTrivial v, reverse fails)
166+ return (trimSolutions v, reverse fails)
159167-- Error e@(CantUnify False _ _ _ _ _) -> tfail e
160168 Error e -> tfail e
161169 where
src/Idris/Coverage.hs+2−2
@@ -325,7 +325,7 @@ checkTotality path fc n
325325 t' <- case t of
326326 Unchecked ->
327327 case lookupDef n ctxt of
328− [CaseOp _ _ _ pats _] ->
328+ [CaseOp _ _ _ _ pats _] ->
329329 do t' <- if AssertTotal `elem` opts
330330 then return $ Total []
331331 else calcTotality path fc n pats
@@ -389,7 +389,7 @@ buildSCG (_, n) = do
389389 ist <- getIState
390390 case lookupCtxt n (idris_callgraph ist) of
391391 [cg] -> case lookupDef n (tt_ctxt ist) of
392− [CaseOp _ _ pats _ cd] ->
392+ [CaseOp _ _ _ pats _ cd] ->
393393 let (args, sc) = cases_totcheck cd in
394394 do logLvl 2 $ "Building SCG for " ++ show n ++ " from\n"
395395 ++ show pats ++ "\n" ++ show sc
src/Idris/ElabDecls.hs+20−18
@@ -74,7 +74,7 @@ elabType' norm info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty
7474 logLvl 2 $ show n ++ " type " ++ showImp Nothing True False ty
7575 ((tyT, defer, is), log) <-
7676 tclift $ elaborate ctxt n (TType (UVal 0)) []
77− (errAt "type of " n (erun fc (build i info False n ty)))
77+ (errAt "type of " n (erun fc (build i info False [] n ty)))
7878 ds <- checkDef fc defer
7979 let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds
8080 addDeferred ds'
@@ -182,7 +182,7 @@ elabData info syn doc fc opts (PLaterdecl n t_in)
182182 t_in <- implicit syn n t_in
183183 let t = addImpl i t_in
184184 ((t', defer, is), log) <- tclift $ elaborate ctxt n (TType (UVal 0)) []
185− (erun fc (build i info False n t))
185+ (erun fc (build i info False [] n t))
186186 def' <- checkDef fc defer
187187 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) def'
188188 addDeferredTyCon def''
@@ -201,7 +201,7 @@ elabData info syn doc fc opts (PDatadecl n t_in dcons)
201201 let t = addImpl i t_in
202202 ((t', defer, is), log) <-
203203 tclift $ elaborate ctxt n (TType (UVal 0)) []
204− (errAt "data declaration " n (erun fc (build i info False n t)))
204+ (errAt "data declaration " n (erun fc (build i info False [] n t)))
205205 def' <- checkDef fc defer
206206 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) def'
207207 -- if n is defined already, make sure it is just a type declaration
@@ -659,7 +659,7 @@ elabTransform info fc safe lhs_in rhs_in
659659 let lhs = addImplPat i lhs_in
660660 ((lhs', dlhs, []), _) <-
661661 tclift $ elaborate ctxt (MN 0 "transLHS") infP []
662− (erun fc (buildTC i info True False (UN "transform")
662+ (erun fc (buildTC i info True [] (UN "transform")
663663 (infTerm lhs)))
664664 let lhs_tm = orderPats (getInferTerm lhs')
665665 let lhs_ty = getInferType lhs'
@@ -671,7 +671,7 @@ elabTransform info fc safe lhs_in rhs_in
671671 ((rhs', defer), _) <-
672672 tclift $ elaborate ctxt (MN 0 "transRHS") clhs_ty []
673673 (do pbinds lhs_tm
674− erun fc (build i info False (UN "transform") rhs)
674+ erun fc (build i info False [] (UN "transform") rhs)
675675 erun fc $ psolve lhs_tm
676676 tt <- get_term
677677 let (tm, ds) = runState (collectDeferred Nothing tt) []
@@ -805,7 +805,7 @@ elabCon info syn tn codata (doc, n, t_in, fc)
805805 logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ showImp Nothing True False t
806806 ((t', defer, is), log) <-
807807 tclift $ elaborate ctxt n (TType (UVal 0)) []
808− (errAt "constructor " n (erun fc (build i info False n t)))
808+ (errAt "constructor " n (erun fc (build i info False [] n t)))
809809 logLvl 2 $ "Rechecking " ++ show t'
810810 def' <- checkDef fc defer
811811 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) def'
@@ -846,6 +846,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
846846 -- question: CAFs in where blocks?
847847 tclift $ tfail $ At fc (NoTypeDecl n)
848848 [ty] -> return ty
849+ let atys = map snd (getArgTys fty)
849850 pats_in <- mapM (elabClause info opts)
850851 (zip [0..] cs)
851852 logLvl 3 $ "Elaborated patterns:\n" ++ show pats_in
@@ -928,7 +929,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
928929
929930 let optpdef = map debind optpats -- \$ map (simple_lhs (tt_ctxt ist)) optpats
930931 tree@(CaseDef scargs sc _) <- tclift $
931− simpleCase tcase False reflect CompileTime fc pdef
932+ simpleCase tcase False reflect CompileTime fc atys pdef
932933 cov <- coverage
933934 pmissing <-
934935 if cov
@@ -976,7 +977,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
976977 let knowncovering = (pcover && cov) || AssertTotal `elem` opts
977978
978979 tree' <- tclift $ simpleCase tcase knowncovering reflect
979− RunTime fc pdef'
980+ RunTime fc atys pdef'
980981 logLvl 3 (show tree)
981982 logLvl 3 $ "Optimised: " ++ show tree'
982983 ctxt <- getContext
@@ -989,6 +990,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
989990 tcase knowncovering
990991 reflect
991992 (AssertTotal `elem` opts)
993+ atys
992994 pats
993995 pdef pdef pdef_inl pdef' ty)
994996 addIBC (IBCDef n)
@@ -998,7 +1000,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
9981000 when (tot /= Unchecked) $ addIBC (IBCTotal n tot)
9991001 i <- getIState
10001002 case lookupDef n (tt_ctxt i) of
1001− (CaseOp _ _ _ _ cd : _) ->
1003+ (CaseOp _ _ _ _ _ cd : _) ->
10021004 let (scargs, sc) = cases_compiletime cd
10031005 (scargs', sc') = cases_runtime cd in
10041006 do let calls = findCalls sc' scargs'
@@ -1167,7 +1169,7 @@ elabValBind info aspat tm_in
11671169-- tctry (elaborate ctxt (MN 0 "val") (TType (UVal 0)) []
11681170-- (build i info aspat (MN 0 "val") tm))
11691171 tclift (elaborate ctxt (MN 0 "val") infP []
1170− (build i info aspat (MN 0 "val") (infTerm tm)))
1172+ (build i info aspat [Reflection] (MN 0 "val") (infTerm tm)))
11711173 let vtm = orderPats (getInferTerm tm')
11721174
11731175 def' <- checkDef (fileFC "(input)") defer
@@ -1198,7 +1200,7 @@ checkPossible info fc tcgen fname lhs_in
11981200 let lhs = addImpl i lhs_in
11991201 -- if the LHS type checks, it is possible
12001202 case elaborate ctxt (MN 0 "patLHS") infP []
1201− (erun fc (buildTC i info True tcgen fname (infTerm lhs))) of
1203+ (erun fc (buildTC i info True [] fname (infTerm lhs))) of
12021204 OK ((lhs', _, _), _) ->
12031205 do let lhs_tm = orderPats (getInferTerm lhs')
12041206 case recheck ctxt [] (forget lhs_tm) lhs_tm of
@@ -1254,7 +1256,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
12541256 ((lhs', dlhs, []), _) <-
12551257 tclift $ elaborate ctxt (MN 0 "patLHS") infP []
12561258 (errAt "left hand side of " fname
1257− (erun fc (buildTC i info True tcgen fname (infTerm lhs))))
1259+ (erun fc (buildTC i info True opts fname (infTerm lhs))))
12581260 let lhs_tm = orderPats (getInferTerm lhs')
12591261 let lhs_ty = getInferType lhs'
12601262 logLvl 3 ("Elaborated: " ++ show lhs_tm)
@@ -1297,7 +1299,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
12971299 tclift $ elaborate ctxt (MN 0 "patRHS") clhsty []
12981300 (do pbinds lhs_tm
12991301 (_, _, is) <- errAt "right hand side of " fname
1300− (erun fc (build i info False fname rhs))
1302+ (erun fc (build i info False opts fname rhs))
13011303 errAt "right hand side of " fname
13021304 (erun fc $ psolve lhs_tm)
13031305 hs <- get_holes
@@ -1426,12 +1428,12 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
14261428 -- Build the LHS as an "Infer", and pull out its type and
14271429 -- pattern bindings
14281430 i <- getIState
1429− let lhs = addImplPat i lhs_in
1431+ let lhs = addImplPat i (stripLinear i lhs_in)
14301432 logLvl 5 ("LHS: " ++ showImp Nothing True False lhs)
14311433 ((lhs', dlhs, []), _) <-
14321434 tclift $ elaborate ctxt (MN 0 "patLHS") infP []
14331435 (errAt "left hand side of with in " fname
1434− (erun fc (buildTC i info True tcgen fname (infTerm lhs))) )
1436+ (erun fc (buildTC i info True opts fname (infTerm lhs))) )
14351437 let lhs_tm = orderPats (getInferTerm lhs')
14361438 let lhs_ty = getInferType lhs'
14371439 let ret_ty = getRetTy lhs_ty
@@ -1448,7 +1450,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
14481450 (do pbinds lhs_tm
14491451 -- TODO: may want where here - see winfo abpve
14501452 (_', d, is) <- errAt "with value in " fname
1451− (erun fc (build i info False fname (infTerm wval)))
1453+ (erun fc (build i info False opts fname (infTerm wval)))
14521454 erun fc $ psolve lhs_tm
14531455 tt <- get_term
14541456 return (tt, d, is))
@@ -1509,7 +1511,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
15091511 ((rhs', defer, is), _) <-
15101512 tclift $ elaborate ctxt (MN 0 "wpatRHS") clhsty []
15111513 (do pbinds lhs_tm
1512− (_, d, is) <- erun fc (build i info False fname rhs)
1514+ (_, d, is) <- erun fc (build i info False opts fname rhs)
15131515 psolve lhs_tm
15141516 tt <- get_term
15151517 return (tt, d, is))
@@ -1847,7 +1849,7 @@ elabInstance info syn fc cs n ps t expn ds
18471849 ctxt <- getContext
18481850 ((tyT, _, _), _) <-
18491851 tclift $ elaborate ctxt iname (TType (UVal 0)) []
1850− (errAt "type of " iname (erun fc (build i info False iname ty)))
1852+ (errAt "type of " iname (erun fc (build i info False [] iname ty)))
18511853 ctxt <- getContext
18521854 (cty, _) <- recheckC fc [] tyT
18531855 let nty = normalise ctxt [] cty
src/Idris/ElabTerm.hs+71−52
@@ -38,10 +38,10 @@ toplevel = EInfo [] emptyContext id Nothing
3838
3939-- Also find deferred names in the term and their types
4040
41−build :: IState -> ElabInfo -> Bool -> Name -> PTerm ->
41+build :: IState -> ElabInfo -> Bool -> FnOpts -> Name -> PTerm ->
4242 ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])
43−build ist info pattern fn tm
44− = do elab ist info pattern False fn tm
43+build ist info pattern opts fn tm
44+ = do elab ist info pattern opts fn tm
4545 ivs <- get_instances
4646 hs <- get_holes
4747 ptm <- get_term
@@ -78,10 +78,10 @@ build ist info pattern fn tm
7878-- (Separate, so we don't go overboard resolving things that we don't
7979-- know about yet on the LHS of a pattern def)
8080
81−buildTC :: IState -> ElabInfo -> Bool -> Bool -> Name -> PTerm ->
81+buildTC :: IState -> ElabInfo -> Bool -> FnOpts -> Name -> PTerm ->
8282 ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])
83−buildTC ist info pattern tcgen fn tm
84− = do elab ist info pattern tcgen fn tm
83+buildTC ist info pattern opts fn tm
84+ = do elab ist info pattern opts fn tm
8585 probs <- get_probs
8686 tm <- get_term
8787 case probs of
@@ -97,19 +97,22 @@ buildTC ist info pattern tcgen fn tm
9797-- Returns the set of declarations we need to add to complete the definition
9898-- (most likely case blocks to elaborate)
9999
100−elab :: IState -> ElabInfo -> Bool -> Bool -> Name -> PTerm ->
100+elab :: IState -> ElabInfo -> Bool -> FnOpts -> Name -> PTerm ->
101101 ElabD ()
102−elab ist info pattern tcgen fn tm
102+elab ist info pattern opts fn tm
103103 = do let loglvl = opt_logLevel (idris_options ist)
104104 when (loglvl > 5) $ unifyLog True
105105 compute -- expand type synonyms, etc
106− elabE (False, False) tm -- (in argument, guarded)
106+ elabE (False, False, False) tm -- (in argument, guarded, in type)
107107 end_unify
108108 when pattern -- convert remaining holes to pattern vars
109109 (do update_term orderPats
110110 tm <- get_term
111111 mkPat)
112112 where
113+ tcgen = Dictionary `elem` opts
114+ reflect = Reflection `elem` opts
115+
113116 isph arg = case getTm arg of
114117 Placeholder -> (True, priority arg)
115118 _ -> (False, priority arg)
@@ -128,6 +131,7 @@ elab ist info pattern tcgen fn tm
128131 (h: hs) -> do patvar h; mkPat
129132 [] -> return ()
130133
134+ elabE :: (Bool, Bool, Bool) -> PTerm -> ElabD ()
131135 elabE ina t = {- do g <- goal
132136 tm <- get_term
133137 trace ("Elaborating " ++ show t ++ " : " ++ show g ++ "\n\tin " ++ show tm)
@@ -147,9 +151,18 @@ elab ist info pattern tcgen fn tm
147151
148152 local f = do e <- get_env
149153 return (f `elem` map fst e)
154+
155+ constType (AType _) = True
156+ constType StrType = True
157+ constType PtrType = True
158+ constType VoidType = True
159+ constType _ = False
150160
151161 elab' ina (PNoImplicits t) = elab' ina t -- skip elabE step
152162 elab' ina PType = do apply RType []; solve
163+ elab' (_,_,inty) (PConstant c)
164+ | constType c && pattern && not reflect && not inty
165+ = lift $ tfail (Msg "Typecase is not allowed")
153166 elab' ina (PConstant c) = do apply (RConstant c) []; solve
154167 elab' ina (PQuote r) = do fill r; solve
155168 elab' ina (PTrue fc) = try (elab' ina (PRef fc unitCon))
@@ -171,13 +184,13 @@ elab ist info pattern tcgen fn tm
171184 [pimp (MN 0 "a") Placeholder True,
172185 pimp (MN 0 "b") Placeholder False,
173186 pexp l, pexp r])
174− elab' ina@(_, a) (PPair fc l r)
187+ elab' ina@(_, a, inty) (PPair fc l r)
175188 = do hnf_compute
176189 g <- goal
177190 case g of
178− TType _ -> elabE (True, a) (PApp fc (PRef fc pairTy)
179− [pexp l,pexp r])
180− _ -> elabE (True, a) (PApp fc (PRef fc pairCon)
191+ TType _ -> elabE (True, a,inty) (PApp fc (PRef fc pairTy)
192+ [pexp l,pexp r])
193+ _ -> elabE (True, a, inty) (PApp fc (PRef fc pairCon)
181194 [pimp (MN 0 "A") Placeholder True,
182195 pimp (MN 0 "B") Placeholder True,
183196 pexp l, pexp r])
@@ -225,7 +238,10 @@ elab ist info pattern tcgen fn tm
225238 trySeq' deferr (x : xs)
226239 = try' (elab' ina x) (trySeq' deferr xs) True
227240 elab' ina (PPatvar fc n) | pattern = patvar n
228− elab' (ina, guarded) (PRef fc n) | pattern && not (inparamBlock n)
241+ elab' (_, _, inty) (PRef fc f)
242+ | isTConName f (tt_ctxt ist) && pattern && not reflect && not inty
243+ = lift $ tfail (Msg "Typecase is not allowed")
244+ elab' (ina, guarded, inty) (PRef fc n) | pattern && not (inparamBlock n)
229245 = do ctxt <- get_context
230246 let defined = case lookupTy n ctxt of
231247 [] -> False
@@ -242,7 +258,7 @@ elab ist info pattern tcgen fn tm
242258 _ -> True
243259 elab' ina f@(PInferRef fc n) = elab' ina (PApp fc f [])
244260 elab' ina (PRef fc n) = erun fc $ do apply (Var n) []; solve
245− elab' ina@(_, a) (PLam n Placeholder sc)
261+ elab' ina@(_, a, inty) (PLam n Placeholder sc)
246262 = do -- n' <- unique_hole n
247263 -- let sc' = mapPT (repN n n') sc
248264 ptm <- get_term
@@ -250,10 +266,10 @@ elab ist info pattern tcgen fn tm
250266 checkPiGoal n
251267 attack; intro (Just n);
252268 -- trace ("------ intro " ++ show n ++ " ---- \n" ++ show ptm)
253− elabE (True, a) sc; solve
269+ elabE (True, a, inty) sc; solve
254270 where repN n n' (PRef fc x) | x == n' = PRef fc n'
255271 repN _ _ t = t
256− elab' ina@(_, a) (PLam n ty sc)
272+ elab' ina@(_, a, inty) (PLam n ty sc)
257273 = do hsin <- get_holes
258274 ptmin <- get_term
259275 tyn <- unique_hole (MN 0 "lamty")
@@ -268,12 +284,12 @@ elab ist info pattern tcgen fn tm
268284 introTy (Var tyn) (Just n)
269285 -- end_unify
270286 focus tyn
271− elabE (True, a) ty
272− elabE (True, a) sc
287+ elabE (True, a, True) ty
288+ elabE (True, a, inty) sc
273289 solve
274− elab' ina@(_,a) (PPi _ n Placeholder sc)
275− = do attack; arg n (MN 0 "ty"); elabE (True, a) sc; solve
276− elab' ina@(_,a) (PPi _ n ty sc)
290+ elab' ina@(_, a, _) (PPi _ n Placeholder sc)
291+ = do attack; arg n (MN 0 "ty"); elabE (True, a, True) sc; solve
292+ elab' ina@(_, a, _) (PPi _ n ty sc)
277293 = do attack; tyn <- unique_hole (MN 0 "ty")
278294 claim tyn RType
279295 n' <- case n of
@@ -281,10 +297,10 @@ elab ist info pattern tcgen fn tm
281297 _ -> return n
282298 forall n' (Var tyn)
283299 focus tyn
284− elabE (True, a) ty
285− elabE (True, a) sc
300+ elabE (True, a, True) ty
301+ elabE (True, a, True) sc
286302 solve
287− elab' ina@(_,a) (PLet n ty val sc)
303+ elab' ina@(_, a, inty) (PLet n ty val sc)
288304 = do attack;
289305 tyn <- unique_hole (MN 0 "letty")
290306 claim tyn RType
@@ -296,17 +312,17 @@ elab ist info pattern tcgen fn tm
296312 Placeholder -> return ()
297313 _ -> do focus tyn
298314 explicit tyn
299− elabE (True, a) ty
315+ elabE (True, a, True) ty
300316 focus valn
301− elabE (True, a) val
317+ elabE (True, a, True) val
302318 env <- get_env
303− elabE (True, a) sc
319+ elabE (True, a, inty) sc
304320 -- HACK: If the name leaks into its type, it may leak out of
305321 -- scope outside, so substitute in the outer scope.
306322 expandLet n (case lookup n env of
307323 Just (Let t v) -> v)
308324 solve
309− elab' ina@(_,a) (PGoal fc r n sc) = do
325+ elab' ina@(_, a, inty) (PGoal fc r n sc) = do
310326 rty <- goal
311327 attack
312328 tyn <- unique_hole (MN 0 "letty")
@@ -315,10 +331,10 @@ elab ist info pattern tcgen fn tm
315331 claim valn (Var tyn)
316332 letbind n (Var tyn) (Var valn)
317333 focus valn
318− elabE (True, a) (PApp fc r [pexp (delab ist rty)])
334+ elabE (True, a, True) (PApp fc r [pexp (delab ist rty)])
319335 env <- get_env
320336 computeLet n
321− elabE (True, a) sc
337+ elabE (True, a, inty) sc
322338 solve
323339-- elab' ina (PLet n Placeholder
324340-- (PApp fc r [pexp (delab ist rty)]) sc)
@@ -368,14 +384,17 @@ elab ist info pattern tcgen fn tm
368384 Just xs@(_:_) -> NS n xs
369385 _ -> n
370386
371− elab' (ina, g) (PMatchApp fc fn)
387+ elab' ina (PMatchApp fc fn)
372388 = do (fn', imps) <- case lookupCtxtName fn (idris_implicits ist) of
373389 [(n, args)] -> return (n, map (const True) args)
374390 _ -> lift $ tfail (NoSuchVariable fn)
375391 ns <- match_apply (Var fn') (map (\x -> (x,0)) imps)
376392 solve
393+ elab' (_, _, inty) (PApp fc (PRef _ f) args')
394+ | isTConName f (tt_ctxt ist) && pattern && not reflect && not inty
395+ = lift $ tfail (Msg "Typecase is not allowed")
377396 -- if f is local, just do a simple_app
378− elab' (ina, g) tm@(PApp fc (PRef _ f) args')
397+ elab' (ina, g, inty) tm@(PApp fc (PRef _ f) args')
379398 = do let args = {- case lookupCtxt f (inblock info) of
380399 Just ps -> (map (pexp . (PRef fc)) ps ++ args')
381400 _ -> -} args'
@@ -383,8 +402,8 @@ elab ist info pattern tcgen fn tm
383402 env <- get_env
384403 if (f `elem` map fst env && length args' == 1)
385404 then -- simple app, as below
386− do simple_app (elabE (ina, g) (PRef fc f))
387− (elabE (True, g) (getTm (head args')))
405+ do simple_app (elabE (ina, g, inty) (PRef fc f))
406+ (elabE (True, g, inty) (getTm (head args')))
388407 (show tm)
389408 solve
390409 else
@@ -408,7 +427,7 @@ elab ist info pattern tcgen fn tm
408427 sortBy (\(_,x) (_,y) ->
409428 compare (priority x) (priority y))
410429 (zip ns args)
411− elabArgs (ina || not isinf, guarded)
430+ elabArgs (ina || not isinf, guarded, inty)
412431 [] fc False ns' (map (\x -> (lazyarg x, getTm x)) eargs)
413432 mkSpecialised ist fc f (map getTm args') tm
414433 solve
@@ -439,9 +458,9 @@ elab ist info pattern tcgen fn tm
439458 setInjective (PApp _ (PRef _ n) _) = setinj n
440459 setInjective _ = return ()
441460
442− elab' ina@(_, a) tm@(PApp fc f [arg])
461+ elab' ina@(_, a, inty) tm@(PApp fc f [arg])
443462 = erun fc $
444− do simple_app (elabE ina f) (elabE (True, a) (getTm arg))
463+ do simple_app (elabE ina f) (elabE (True, a, inty) (getTm arg))
445464 (show tm)
446465 solve
447466 elab' ina Placeholder = do (h : hs) <- get_holes
@@ -490,7 +509,7 @@ elab ist info pattern tcgen fn tm
490509 elab' ina sc
491510 elab' ina (PRef fc letn)
492511 solve
493− elab' ina@(_, a) c@(PCase fc scr opts)
512+ elab' ina@(_, a, inty) c@(PCase fc scr opts)
494513 = do attack
495514 tyn <- unique_hole (MN 0 "scty")
496515 claim tyn RType
@@ -499,7 +518,7 @@ elab ist info pattern tcgen fn tm
499518 claim valn (Var tyn)
500519 letbind scvn (Var tyn) (Var valn)
501520 focus valn
502− elabE (True, a) scr
521+ elabE (True, a, inty) scr
503522 args <- get_env
504523 cname <- unique_hole' True (mkCaseName fn)
505524 let cname' = mkN cname
@@ -682,9 +701,9 @@ findInstances ist t
682701 | otherwise = []
683702
684703trivial' ist
685− = trivial (elab ist toplevel False False (MN 0 "tac")) ist
704+ = trivial (elab ist toplevel False [] (MN 0 "tac")) ist
686705proofSearch' ist top n hints
687− = proofSearch (elab ist toplevel False False (MN 0 "tac")) top n hints ist
706+ = proofSearch (elab ist toplevel False [] (MN 0 "tac")) top n hints ist
688707
689708
690709resolveTC :: Int -> Term -> Name -> IState -> ElabD ()
@@ -813,7 +832,7 @@ runTac autoSolve ist tac
813832 where
814833 bname (Bind n _ _) = Just n
815834 bname _ = Nothing
816− runT (Exact tm) = do elab ist toplevel False False (MN 0 "tac") tm
835+ runT (Exact tm) = do elab ist toplevel False [] (MN 0 "tac") tm
817836 when autoSolve solveAll
818837 runT (MatchRefine fn)
819838 = do fnimps <-
@@ -860,7 +879,7 @@ runTac autoSolve ist tac
860879 letn <- unique_hole (MN 0 "equiv_val")
861880 letbind letn (Var tyn) (Var valn)
862881 focus tyn
863− elab ist toplevel False False (MN 0 "tac") tm
882+ elab ist toplevel False [] (MN 0 "tac") tm
864883 focus valn
865884 when autoSolve solveAll
866885 runT (Rewrite tm) -- to elaborate tm, let bind it, then rewrite by that
@@ -873,7 +892,7 @@ runTac autoSolve ist tac
873892 letn <- unique_hole (MN 0 "rewrite_rule")
874893 letbind letn (Var tyn) (Var valn)
875894 focus valn
876− elab ist toplevel False False (MN 0 "tac") tm
895+ elab ist toplevel False [] (MN 0 "tac") tm
877896 rewrite (Var letn)
878897 when autoSolve solveAll
879898 runT (Induction nm)
@@ -888,7 +907,7 @@ runTac autoSolve ist tac
888907 letn <- unique_hole n
889908 letbind letn (Var tyn) (Var valn)
890909 focus valn
891− elab ist toplevel False False (MN 0 "tac") tm
910+ elab ist toplevel False [] (MN 0 "tac") tm
892911 when autoSolve solveAll
893912 runT (LetTacTy n ty tm)
894913 = do attack
@@ -899,9 +918,9 @@ runTac autoSolve ist tac
899918 letn <- unique_hole n
900919 letbind letn (Var tyn) (Var valn)
901920 focus tyn
902− elab ist toplevel False False (MN 0 "tac") ty
921+ elab ist toplevel False [] (MN 0 "tac") ty
903922 focus valn
904− elab ist toplevel False False (MN 0 "tac") tm
923+ elab ist toplevel False [] (MN 0 "tac") tm
905924 when autoSolve solveAll
906925 runT Compute = compute
907926 runT Trivial = do trivial' ist; when autoSolve solveAll
@@ -919,7 +938,7 @@ runTac autoSolve ist tac
919938 scriptvar <- unique_hole (MN 0 "scriptvar" )
920939 letbind scriptvar scriptTy (Var script)
921940 focus script
922− elab ist toplevel False False (MN 0 "tac") tm
941+ elab ist toplevel False [] (MN 0 "tac") tm
923942 (script', _) <- get_type_val (Var scriptvar)
924943 -- now that we have the script apply
925944 -- it to the reflected goal and context
@@ -952,7 +971,7 @@ runTac autoSolve ist tac
952971 letbind scriptvar scriptTy (Var script)
953972 focus script
954973 ptm <- get_term
955− elab ist toplevel False False (MN 0 "tac")
974+ elab ist toplevel False [] (MN 0 "tac")
956975 (PApp emptyFC tm [pexp (delabTy' ist [] tgoal True True)])
957976 (script', _) <- get_type_val (Var scriptvar)
958977 -- now that we have the script apply
@@ -980,7 +999,7 @@ runTac autoSolve ist tac
980999 letn <- unique_hole (MN 0 "letvar")
9811000 letbind letn (Var tyn) (Var valn)
9821001 focus valn
983− elab ist toplevel False False (MN 0 "tac") v
1002+ elab ist toplevel False [] (MN 0 "tac") v
9841003 (value, _) <- get_type_val (Var letn)
9851004 ctxt <- get_context
9861005 env <- get_env
@@ -994,7 +1013,7 @@ runTac autoSolve ist tac
9941013 letn <- unique_hole (MN 0 "letvar")
9951014 letbind letn (Var tyn) (Var valn)
9961015 focus valn
997− elab ist toplevel False False (MN 0 "tac") v
1016+ elab ist toplevel False [] (MN 0 "tac") v
9981017 (value, _) <- get_type_val (Var letn)
9991018 ctxt <- get_context
10001019 env <- get_env
src/Idris/IBC.hs+11−9
@@ -23,7 +23,7 @@ import Debug.Trace
2323import Paths_idris
2424
2525ibcVersion :: Word8
26−ibcVersion = 49
26+ibcVersion = 50
2727
2828data IBCFile = IBCFile { ver :: Word8,
2929 sourcefile :: FilePath,
@@ -801,12 +801,13 @@ instance Binary Def where
801801 put x2
802802 -- all primitives just get added at the start, don't write
803803 Operator x1 x2 x3 -> do return ()
804− CaseOp x1 x2 x3 x3a x4 -> do putWord8 3
805− put x1
806− put x2
807− put x3
808− -- no x3a
809− put x4
804+ CaseOp x1 x2 x2a x3 x3a x4 -> do putWord8 3
805+ put x1
806+ put x2
807+ put x2a
808+ put x3
809+ -- no x3a
810+ put x4
810811 get
811812 = do i <- getWord8
812813 case i of
@@ -820,9 +821,10 @@ instance Binary Def where
820821 3 -> do x1 <- get
821822 x2 <- get
822823 x3 <- get
823− -- x3 <- get always []
824824 x4 <- get
825− return (CaseOp x1 x2 x3 [] x4)
825+ -- x3 <- get always []
826+ x5 <- get
827+ return (CaseOp x1 x2 x3 x4 [] x5)
826828 _ -> error "Corrupted binary data for Def"
827829
828830instance Binary Accessibility where
src/Idris/Prover.hs+2−1
@@ -65,7 +65,7 @@ prove ctxt lit n ty
6565 ideslavePutSExp "end-proof-mode" n
6666 let proofs = proof_list i
6767 putIState (i { proof_list = (n, prf) : proofs })
68− let tree = simpleCase False True False CompileTime (fileFC "proof") [([], P Ref n ty, tm)]
68+ let tree = simpleCase False True False CompileTime (fileFC "proof") [] [([], P Ref n ty, tm)]
6969 logLvl 3 (show tree)
7070 (ptm, pty) <- recheckC (fileFC "proof") [] tm
7171 logLvl 5 ("Proof type: " ++ show pty ++ "\n" ++
@@ -75,6 +75,7 @@ prove ctxt lit n ty
7575 Error e -> ierror (CantUnify False ty pty e [] 0)
7676 ptm' <- applyOpts ptm
7777 updateContext (addCasedef n (CaseInfo True False) False False True False
78+ []
7879 [Right (P Ref n ty, ptm)]
7980 [([], P Ref n ty, ptm)]
8081 [([], P Ref n ty, ptm)]
src/Idris/REPL.hs+15−22
@@ -77,14 +77,12 @@ import Debug.Trace
7777
7878-- | Run the REPL
7979repl :: IState -- ^ The initial state
80− -> MVar IState -- ^ Server's MVar
8180 -> [FilePath] -- ^ The loaded modules
8281 -> InputT Idris ()
83−repl orig stvar mods
82+repl orig mods
8483 = H.catch
8584 (do let quiet = opt_quiet (idris_options orig)
8685 i <- lift getIState
87− lift $ runIO $ swapMVar stvar i -- update shared state
8886 let colour = idris_colourRepl i
8987 let theme = idris_colourTheme i
9088 let mvs = idris_metavars i
@@ -98,15 +96,15 @@ repl orig stvar mods
9896 Nothing -> do lift $ when (not quiet) (iputStrLn "Bye bye")
9997 return ()
10098 Just input -> H.catch
101− (do ms <- lift $ processInput stvar input orig mods
99+ (do ms <- lift $ processInput input orig mods
102100 case ms of
103− Just mods -> repl orig stvar mods
101+ Just mods -> repl orig mods
104102 Nothing -> return ())
105103 ctrlC)
106104 ctrlC
107105 where ctrlC :: SomeException -> InputT Idris ()
108106 ctrlC e = do lift $ iputStrLn (show e)
109− repl orig stvar mods
107+ repl orig mods
110108
111109 showMVs c thm [] = ""
112110 showMVs c thm ms = "Metavariables: " ++
@@ -124,15 +122,14 @@ repl orig stvar mods
124122 else show n
125123
126124-- | Run the REPL server
127−startServer :: IState -> MVar IState -> [FilePath] -> Idris ()
128−startServer orig stvar fn_in = do tid <- runIO $ forkOS serverLoop
129− return ()
125+startServer :: IState -> [FilePath] -> Idris ()
126+startServer orig fn_in = do tid <- runIO $ forkOS serverLoop
127+ return ()
130128 where serverLoop :: IO ()
131129 -- TODO: option for port number
132130 serverLoop = withSocketsDo $
133131 do sock <- listenOnLocalhost $ PortNumber 4294
134− i <- readMVar stvar
135− loop fn i sock
132+ loop fn orig sock
136133
137134 fn = case fn_in of
138135 (f:_) -> f
@@ -146,19 +143,16 @@ startServer orig stvar fn_in = do tid <- runIO $ forkOS serverLoop
146143 host == "127.0.0.1")
147144 then do
148145 cmd <- hGetLine h
149− takeMVar stvar
150− (ist', fn) <- processNetCmd stvar orig ist h fn cmd
151− putMVar stvar ist'
146+ (ist', fn) <- processNetCmd orig ist h fn cmd
152147 hClose h
153148 loop fn ist' sock
154149 else do
155150 putStrLn $ "Closing connection attempt from non-localhost " ++ host
156151 hClose h
157152
158−processNetCmd :: MVar IState ->
159− IState -> IState -> Handle -> FilePath -> String ->
153+processNetCmd :: IState -> IState -> Handle -> FilePath -> String ->
160154 IO (IState, FilePath)
161−processNetCmd stvar orig i h fn cmd
155+processNetCmd orig i h fn cmd
162156 = do res <- case parseCmd i "(net)" cmd of
163157 Failure err -> return (Left (Msg " invalid command"))
164158 Success c -> runErrorT $ evalStateT (processNet fn c) i
@@ -337,9 +331,9 @@ lit f = case splitExtension f of
337331 (_, ".lidr") -> True
338332 _ -> False
339333
340−processInput :: MVar IState -> String ->
334+processInput :: String ->
341335 IState -> [FilePath] -> Idris (Maybe [FilePath])
342−processInput stvar cmd orig inputs
336+processInput cmd orig inputs
343337 = do i <- getIState
344338 let opts = idris_options i
345339 let quiet = opt_quiet opts
@@ -1224,9 +1218,8 @@ idrisMain opts =
12241218
12251219 when (runrepl && not idesl) $ do
12261220 initScript
1227− stvar <- runIO $ newMVar ist
1228− startServer ist stvar inputs
1229− runInputT (replSettings (Just historyFile)) $ repl ist stvar inputs
1221+ startServer ist inputs
1222+ runInputT (replSettings (Just historyFile)) $ repl ist inputs
12301223 when (idesl) $ ideslaveStart ist inputs
12311224 ok <- noErrors
12321225 when (not ok) $ runIO (exitWith (ExitFailure 1))
src/Util/DynamicLinker.hs+6−2
@@ -5,11 +5,12 @@ module Util.DynamicLinker where
55
66#ifdef IDRIS_FFI
77import Foreign.LibFFI
8−import Foreign.Ptr (nullPtr, FunPtr, nullFunPtr,castPtrToFunPtr)
8+import Foreign.Ptr (Ptr(), nullPtr, FunPtr, nullFunPtr, castPtrToFunPtr)
99import System.Directory
1010#ifndef WINDOWS
1111import System.Posix.DynamicLinker
1212#else
13+import qualified Control.Exception as Exception (catch, IOException)
1314import System.Win32.DLL
1415import System.Win32.Types
1516type DL = HMODULE
@@ -63,10 +64,13 @@ tryLoadFn fn (Lib _ h) = do cFn <- dlsym h fn
6364tryLoadLib :: String -> IO (Maybe DynamicLib)
6465tryLoadLib lib = do exactName <- doesFileExist lib
6566 let filename = if exactName then lib else lib ++ "." ++ hostDynamicLibExt
66− handle <- loadLibrary filename
67+ handle <- Exception.catch (loadLibrary filename) nullPtrOnException
6768 if handle == nullPtr
6869 then return Nothing
6970 else return . Just $ Lib lib handle
71+ where nullPtrOnException :: Exception.IOException -> IO DL
72+ nullPtrOnException e = return nullPtr
73+ -- `show e` will however give broken error message
7074
7175tryLoadFn :: String -> DynamicLib -> IO (Maybe ForeignFun)
7276tryLoadFn fn (Lib _ h) = do cFn <- getProcAddress h fn
test/reg005/reg005.idr+1
@@ -48,3 +48,4 @@ Main.eqCharOK = proof {
4848 exact x = x;
4949}
5050
51+