e6c3f56 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge remote-tracking branch 'upstream/master' into error-reflection

e6c3f56David Raymond Christiansen13 years ago

CHANGELOG+2

compare with master

unifiedsplit

@@ -1,6 +1,8 @@

1New in 0.9.11:

2-------------

3* Agda-style equational reasoning (in Syntax.PreorderReasoning)

4* Agda-style equational reasoning (in Syntax.PreorderReasoning)

5+* 'case' construct now abstracts over the scrutinee in its type

5New in 0.9.10:

7New in 0.9.10:

6--------------

8--------------

libs/effects/Effect/Memory.idr+2−2

@@ -80,8 +80,8 @@ instance Handler RawMemory (IOExcept String) where

80 handle () (Allocate n) k

81 = do ptr <- do_malloc n

82 k (CH ptr) ()

83− handle {res = MemoryChunk _ offset} (CH ptr) (Initialize c size _) k

83+ handle (CH ptr) (Initialize {i} c size _) k

84− = ioe_lift (do_memset ptr offset c size) $> k (CH ptr) ()

84+ = ioe_lift (do_memset ptr i c size) $> k (CH ptr) ()

85 handle (CH ptr) (Free) k

86 = ioe_lift (do_free ptr) $> k () ()

87 handle (CH ptr) (Peek offset size _) k

libs/prelude/Prelude/Either.idr+11

@@ -63,6 +63,17 @@ maybeToEither def (Just j) = Right j

63maybeToEither def Nothing = Left def

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+

66--------------------------------------------------------------------------------

77--------------------------------------------------------------------------------

67-- Injectivity of constructors

78-- Injectivity of constructors

68--------------------------------------------------------------------------------

79--------------------------------------------------------------------------------

src/IRTS/Compiler.hs+1−1

@@ -157,7 +157,7 @@ declArgs args inl n x = LFun (if inl then [Inline] else []) n args x

157

158mkLDecl n (Function tm _) = do e <- ir tm

159 return (declArgs [] True n e)

160−mkLDecl n (CaseOp ci _ _ pats cd)

160+mkLDecl n (CaseOp ci _ _ _ pats cd)

161 = let (args, sc) = cases_runtime cd in

162 do e <- ir (args, sc)

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

44 , ("reflect", Just ExprTArg)

45 , ("fill", Just ExprTArg)

46 , ("try", Just AltsTArg)

47+ , ("induction", Just NameTArg)

47 ] ++ map (\x -> (x, Nothing)) [

48 ] ++ map (\x -> (x, Nothing)) [

48 "intros", "compute", "trivial", "solve", "attack",

49 "intros", "compute", "trivial", "solve", "attack",

49 "state", "term", "undo", "qed", "abandon", ":q"

50 "state", "term", "undo", "qed", "abandon", ":q"

src/Idris/Core/CaseTree.hs+103−36

@@ -67,7 +67,7 @@ instance Show t => Show (SC' t) where

68type CaseTree = SC

69type Clause = ([Pat], (Term, Term))

70−type CS = ([Term], Int)

70+type CS = ([Term], Int, [(Name, Type)])

72instance TermSize SC where

73 termsize n (Case n' as) = termsize n as

@@ -183,9 +183,10 @@ data Phase = CompileTime | RunTime

183-- Work Right to Left

184

185simpleCase :: Bool -> Bool -> Bool ->

186+ Phase -> FC -> [Type] ->

186− Phase -> FC -> [([Name], Term, Term)] ->

187+ [([Name], Term, Term)] ->

187 TC CaseDef

188 TC CaseDef

188−simpleCase tc cover reflect phase fc cs

189+simpleCase tc cover reflect phase fc argtys cs

189 = sc' tc cover phase fc (filter (\(_, _, r) ->

190 = sc' tc cover phase fc (filter (\(_, _, r) ->

190 case r of

191 case r of

191 Impossible -> False

192 Impossible -> False

@@ -195,6 +196,7 @@ simpleCase tc cover reflect phase fc cs

195 = return $ CaseDef [] (UnmatchedCase "No pattern clauses") []

196 = return $ CaseDef [] (UnmatchedCase "No pattern clauses") []

196 sc' tc cover phase fc cs

197 sc' tc cover phase fc cs

197 = let proj = phase == RunTime

198 = let proj = phase == RunTime

199+ vnames = fstT (head cs)

198 pats = map (\ (avs, l, r) ->

200 pats = map (\ (avs, l, r) ->

199 (avs, toPats reflect tc l, (l, r))) cs

201 (avs, toPats reflect tc l, (l, r))) cs

200 chkPats = mapM chkAccessible pats in

202 chkPats = mapM chkAccessible pats in

@@ -204,13 +206,19 @@ simpleCase tc cover reflect phase fc cs

204 ns = take numargs args

206 ns = take numargs args

205 (ns', ps') = order ns pats

207 (ns', ps') = order ns pats

206 (tree, st) = runState

208 (tree, st) = runState

207− (match ns' ps' (defaultCase cover)) ([], numargs)

209+ (match ns' ps' (defaultCase cover))

210+ ([], numargs, [])

208− t = CaseDef ns (prune proj (depatt ns' tree)) (fst st) in

211+ t = CaseDef ns (prune proj (depatt ns' tree)) (fstT st) in

209− if proj then return (stripLambdas t) else return t

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

210 Error err -> Error (At fc err)

216 Error err -> Error (At fc err)

211 where args = map (\i -> MN i "e") [0..]

217 where args = map (\i -> MN i "e") [0..]

212 defaultCase True = STerm Erased

218 defaultCase True = STerm Erased

213 defaultCase False = UnmatchedCase "Error"

219 defaultCase False = UnmatchedCase "Error"

220+ fstT (x, _, _) = x

221+ lstT (_, _, x) = x

214

222

215 chkAccessible (avs, l, c)

223 chkAccessible (avs, l, c)

216 | phase == RunTime || reflect = return (l, c)

224 | phase == RunTime || reflect = return (l, c)

@@ -218,17 +226,62 @@ simpleCase tc cover reflect phase fc cs

218 return (l, c)

226 return (l, c)

219

227

220 acc [] n = Error (Inaccessible n)

228 acc [] n = Error (Inaccessible n)

221− acc (PV x : xs) n | x == n = OK ()

229+ acc (PV x t : xs) n | x == n = OK ()

222 acc (PCon _ _ ps : xs) n = acc (ps ++ xs) n

230 acc (PCon _ _ ps : xs) n = acc (ps ++ xs) n

223 acc (PSuc p : xs) n = acc (p : xs) n

231 acc (PSuc p : xs) n = acc (p : xs) n

224 acc (_ : xs) n = acc xs n

232 acc (_ : xs) n = acc xs n

225

233

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+

226data Pat = PCon Name Int [Pat]

278data Pat = PCon Name Int [Pat]

227 | PConst Const

279 | PConst Const

228− | PV Name

280+ | PV Name Type

229 | PSuc Pat -- special case for n+1 on Integer

281 | PSuc Pat -- special case for n+1 on Integer

230 | PReflected Name [Pat]

282 | PReflected Name [Pat]

231 | PAny

283 | PAny

284+ | PTyPat -- typecase, not allowed, inspect last

232 deriving Show

285 deriving Show

233

286

234-- If there are repeated variables, take the *last* one (could be name shadowing

287-- 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) []

250 = do p' <- toPat' p []

303 = do p' <- toPat' p []

251 return $ PSuc p'

304 return $ PSuc p'

252 -- Typecase

305 -- Typecase

253− toPat' (P (TCon t a) n _) args | tc

306+-- toPat' (P (TCon t a) n _) args | tc

254− = do args' <- mapM (\x -> toPat' x []) args

307+-- = do args' <- mapM (\x -> toPat' x []) args

255− return $ PCon n t args'

308+-- return $ PCon n t args'

256− toPat' (Constant (AType (ATInt ITNative))) []

309+-- toPat' (Constant (AType (ATInt ITNative))) []

257− | tc = return $ PCon (UN "Int") 1 []

310+-- | tc = return $ PCon (UN "Int") 1 []

258− toPat' (Constant (AType ATFloat)) [] | tc = return $ PCon (UN "Float") 2 []

311+-- toPat' (Constant (AType ATFloat)) [] | tc = return $ PCon (UN "Float") 2 []

259− toPat' (Constant (AType (ATInt ITChar))) [] | tc = return $ PCon (UN "Char") 3 []

312+-- toPat' (Constant (AType (ATInt ITChar))) [] | tc = return $ PCon (UN "Char") 3 []

260− toPat' (Constant StrType) [] | tc = return $ PCon (UN "String") 4 []

313+-- toPat' (Constant StrType) [] | tc = return $ PCon (UN "String") 4 []

261− toPat' (Constant PtrType) [] | tc = return $ PCon (UN "Ptr") 5 []

314+-- toPat' (Constant PtrType) [] | tc = return $ PCon (UN "Ptr") 5 []

262− toPat' (Constant (AType (ATInt ITBig))) []

315+-- toPat' (Constant (AType (ATInt ITBig))) []

263− | tc = return $ PCon (UN "Integer") 6 []

316+-- | tc = return $ PCon (UN "Integer") 6 []

264− toPat' (Constant (AType (ATInt (ITFixed n)))) []

317+-- toPat' (Constant (AType (ATInt (ITFixed n)))) []

265− | tc = return $ PCon (UN (fixedN n)) (7 + fromEnum n) [] -- 7-10 inclusive

318+-- | tc = return $ PCon (UN (fixedN n)) (7 + fromEnum n) [] -- 7-10 inclusive

266− toPat' (P Bound n _) [] = do ns <- get

319+ toPat' (P Bound n ty) [] = -- trace (show (n, ty)) $

320+ do ns <- get

267 if n `elem` ns

321 if n `elem` ns

268 then return PAny

322 then return PAny

269 else do put (n : ns)

323 else do put (n : ns)

270− return (PV n)

324+ return (PV n ty)

271 toPat' (App f a) args = toPat' f (a : args)

325 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

272 toPat' (Constant x) [] = return $ PConst x

330 toPat' (Constant x) [] = return $ PConst x

273 toPat' (Bind n (Pi t) sc) [] | reflect && noOccurrence n sc

331 toPat' (Bind n (Pi t) sc) [] | reflect && noOccurrence n sc

274 = do t' <- toPat' t []

332 = do t' <- toPat' t []

@@ -289,9 +347,10 @@ data Partition = Cons [Clause]

289 | Vars [Clause]

347 | Vars [Clause]

290 deriving Show

348 deriving Show

291

349

292−isVarPat (PV _ : ps , _) = True

350+isVarPat (PV _ _ : ps , _) = True

293−isVarPat (PAny : ps , _) = True

351+isVarPat (PAny : ps , _) = True

352+isVarPat (PTyPat : ps , _) = True

294−isVarPat _ = False

353+isVarPat _ = False

295

354

296isConPat (PCon _ _ _ : ps, _) = True

355isConPat (PCon _ _ _ : ps, _) = True

297isConPat (PReflected _ _ : ps, _) = True

356isConPat (PReflected _ _ : ps, _) = True

@@ -337,8 +396,8 @@ order ns cs = let patnames = transpose (map (zip ns) (map fst cs))

337match :: [Name] -> [Clause] -> SC -- error case

396match :: [Name] -> [Clause] -> SC -- error case

338 -> State CS SC

397 -> State CS SC

339match [] (([], ret) : xs) err

398match [] (([], ret) : xs) err

340− = do (ts, v) <- get

399+ = do (ts, v, ntys) <- get

341− put (ts ++ (map (fst.snd) xs), v)

400+ put (ts ++ (map (fst.snd) xs), v, ntys)

342 case snd ret of

401 case snd ret of

343 Impossible -> return ImpossibleCase

402 Impossible -> return ImpossibleCase

344 tm -> return $ STerm tm -- run out of arguments

403 tm -> return $ STerm tm -- run out of arguments

@@ -408,12 +467,17 @@ argsToAlt rs@((r, m) : rest)

408 return (newArgs, addRs rs)

467 return (newArgs, addRs rs)

409 where

468 where

410 getNewVars [] = return []

469 getNewVars [] = return []

411− getNewVars ((PV n) : ns) = do v <- getVar "e"

470+ getNewVars ((PV n t) : ns) = do v <- getVar "e"

471+ (cs, i, ntys) <- get

472+ put (cs, i, (v, t) : ntys)

412− nsv <- getNewVars ns

473+ nsv <- getNewVars ns

413− return (v : nsv)

474+ return (v : nsv)

414 getNewVars (PAny : ns) = do v <- getVar "i"

475 getNewVars (PAny : ns) = do v <- getVar "i"

415 nsv <- getNewVars ns

476 nsv <- getNewVars ns

416 return (v : nsv)

477 return (v : nsv)

478+ getNewVars (PTyPat : ns) = do v <- getVar "t"

479+ nsv <- getNewVars ns

480+ return (v : nsv)

417 getNewVars (_ : ns) = do v <- getVar "e"

481 getNewVars (_ : ns) = do v <- getVar "e"

418 nsv <- getNewVars ns

482 nsv <- getNewVars ns

419 return (v : nsv)

483 return (v : nsv)

@@ -424,7 +488,7 @@ argsToAlt rs@((r, m) : rest)

424 uniq i n = n

488 uniq i n = n

425

489

426getVar :: String -> State CS Name

490getVar :: 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)

428

492

429groupCons :: [Clause] -> State CS [Group]

493groupCons :: [Clause] -> State CS [Group]

430groupCons cs = gc [] cs

494groupCons cs = gc [] cs

@@ -454,12 +518,15 @@ groupCons cs = gc [] cs

454

518

455varRule :: [Name] -> [Clause] -> SC -> State CS SC

519varRule :: [Name] -> [Clause] -> SC -> State CS SC

456varRule (v : vs) alts err =

520varRule (v : vs) alts err =

457− do let alts' = map (repVar v) alts

521+ do alts' <- mapM (repVar v) alts

458 match vs alts' err

522 match vs alts' err

459 where

523 where

460− repVar v (PV p : ps , (lhs, res))

524+ repVar v (PV p ty : ps , (lhs, res))

525+ = do (cs, i, ntys) <- get

526+ put (cs, i, (v, ty) : ntys)

461− = (ps, (lhs, subst p (P Bound v Erased) res))

527+ return (ps, (lhs, subst p (P Bound v ty) res))

462− repVar v (PAny : ps , res) = (ps, res)

528+ repVar v (PAny : ps , res) = return (ps, res)

529+ repVar v (PTyPat : ps , res) = return (ps, res)

463

530

464-- fix: case e of S k -> f (S k) ==> case e of S k -> f e

531-- fix: case e of S k -> f (S k) ==> case e of S k -> f e

465

532

src/Idris/Core/Evaluate.hs+22−20

@@ -211,7 +211,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

211 ev ntimes (n:stk) True env tm

212 [(TyDecl nt ty, _)] -> do vty <- ev ntimes stk True env ty

213 return $ VP nt n vty

214− [(CaseOp ci _ _ _ cd, acc)]

214+ [(CaseOp ci _ _ _ _ cd, acc)]

215 | (acc /= Frozen) &&

216 null (fst (cases_totcheck cd)) -> -- unoptimised version

217 let (ns, tree) = getCases cd in

@@ -284,7 +284,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

284 reapply ntimes stk top env f@(VP Ref n ty) args

285 = let val = lookupDefAcc n (spec || atRepl) ctxt in

286 case val of

287− [(CaseOp ci _ _ _ cd, acc)] ->

287+ [(CaseOp ci _ _ _ _ cd, acc)] ->

288 let (ns, tree) = getCases cd in

289 do c <- evCase ntimes n (n:stk) top env ns args tree

290 case c of

@@ -310,7 +310,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

310 if u then

311 do let val = lookupDefAcc n (spec || atRepl) ctxt

312 case val of

313− [(CaseOp ci _ _ _ cd, acc)]

313+ [(CaseOp ci _ _ _ _ cd, acc)]

314 | acc /= Frozen -> -- unoptimised version

315 let (ns, tree) = getCases cd in

316 if blockSimplify ci n stk

@@ -561,8 +561,8 @@ convEq ctxt = ceq [] where

561 sameDefs ps x y = case (lookupDef x ctxt, lookupDef y ctxt) of

562 ([Function _ xdef], [Function _ ydef])

563 -> ceq ((x,y):ps) xdef ydef

564− ([CaseOp _ _ _ _ xd],

564+ ([CaseOp _ _ _ _ _ xd],

565− [CaseOp _ _ _ _ yd])

565+ [CaseOp _ _ _ _ _ yd])

566 -> let (_, xdef) = cases_compiletime xd

567 (_, ydef) = cases_compiletime yd in

568 caseeq ((x,y):ps) xdef ydef

@@ -588,6 +588,7 @@ data Def = Function !Type !Term

588 | Operator Type Int ([Value] -> Maybe Value)

589 | CaseOp CaseInfo

590 !Type

591+ ![Type] -- argument types

591 ![Either Term (Term, Term)] -- original definition

592 ![Either Term (Term, Term)] -- original definition

592 ![([Name], Term, Term)] -- simplified for totality check definition

593 ![([Name], Term, Term)] -- simplified for totality check definition

593 !CaseDefs

594 !CaseDefs

@@ -620,7 +621,7 @@ instance Show Def where

620 show (Function ty tm) = "Function: " ++ show (ty, tm)

621 show (Function ty tm) = "Function: " ++ show (ty, tm)

621 show (TyDecl nt ty) = "TyDecl: " ++ show nt ++ " " ++ show ty

622 show (TyDecl nt ty) = "TyDecl: " ++ show nt ++ " " ++ show ty

622 show (Operator ty _ _) = "Operator: " ++ show ty

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

624 = let (ns, sc) = cases_compiletime cd

625 = let (ns, sc) = cases_compiletime cd

625 (ns_t, sc_t) = cases_totcheck cd

626 (ns_t, sc_t) = cases_totcheck cd

626 (ns', sc') = cases_runtime cd in

627 (ns', sc') = cases_runtime cd in

@@ -752,6 +753,7 @@ addDatatype (Data n tag ty cons) uctxt

752

753

753-- FIXME: Too many arguments! Refactor all these Bools.

754-- FIXME: Too many arguments! Refactor all these Bools.

754addCasedef :: Name -> CaseInfo -> Bool -> Bool -> Bool -> Bool ->

755addCasedef :: Name -> CaseInfo -> Bool -> Bool -> Bool -> Bool ->

756+ [Type] -> -- argument types

755 [Either Term (Term, Term)] ->

757 [Either Term (Term, Term)] ->

756 [([Name], Term, Term)] -> -- totality

758 [([Name], Term, Term)] -> -- totality

757 [([Name], Term, Term)] -> -- compile time

759 [([Name], Term, Term)] -> -- compile time

@@ -759,16 +761,16 @@ addCasedef :: Name -> CaseInfo -> Bool -> Bool -> Bool -> Bool ->

759 [([Name], Term, Term)] -> -- run time

761 [([Name], Term, Term)] -> -- run time

760 Type -> Context -> Context

762 Type -> Context -> Context

761addCasedef n ci@(CaseInfo alwaysInline tcdict)

763addCasedef n ci@(CaseInfo alwaysInline tcdict)

762− tcase covering reflect asserted ps_in

764+ tcase covering reflect asserted argtys

763− ps_tot ps_inl ps_ct ps_rt ty uctxt

765+ ps_in ps_tot ps_inl ps_ct ps_rt ty uctxt

764 = let ctxt = definitions uctxt

766 = let ctxt = definitions uctxt

765 access = case lookupDefAcc n False uctxt of

767 access = case lookupDefAcc n False uctxt of

766 [(_, acc)] -> acc

768 [(_, acc)] -> acc

767 _ -> Public

769 _ -> Public

768− ctxt' = case (simpleCase tcase covering reflect CompileTime emptyFC ps_tot,

770+ ctxt' = case (simpleCase tcase covering reflect CompileTime emptyFC argtys ps_tot,

769− simpleCase tcase covering reflect CompileTime emptyFC ps_ct,

771+ simpleCase tcase covering reflect CompileTime emptyFC argtys ps_ct,

770− simpleCase tcase covering reflect CompileTime emptyFC ps_inl,

772+ simpleCase tcase covering reflect CompileTime emptyFC argtys ps_inl,

771− simpleCase tcase covering reflect RunTime emptyFC ps_rt) of

773+ simpleCase tcase covering reflect RunTime emptyFC argtys ps_rt) of

772 (OK (CaseDef args_tot sc_tot _),

774 (OK (CaseDef args_tot sc_tot _),

773 OK (CaseDef args_ct sc_ct _),

775 OK (CaseDef args_ct sc_ct _),

774 OK (CaseDef args_inl sc_inl _),

776 OK (CaseDef args_inl sc_inl _),

@@ -781,7 +783,7 @@ addCasedef n ci@(CaseInfo alwaysInline tcdict)

781 (args_inl, sc_inl)

783 (args_inl, sc_inl)

782 (args_rt, sc_rt) in

784 (args_rt, sc_rt) in

783 addDef n (CaseOp (ci { case_inlinable = inlc })

785 addDef n (CaseOp (ci { case_inlinable = inlc })

784− ty ps_in ps_tot cdef,

786+ ty argtys ps_in ps_tot cdef,

785 access, Unchecked, EmptyMI) ctxt in

787 access, Unchecked, EmptyMI) ctxt in

786 uctxt { definitions = ctxt' }

788 uctxt { definitions = ctxt' }

787

789

@@ -790,15 +792,15 @@ simplifyCasedef :: Name -> Context -> Context

790simplifyCasedef n uctxt

792simplifyCasedef n uctxt

791 = let ctxt = definitions uctxt

793 = let ctxt = definitions uctxt

792 ctxt' = case lookupCtxt n ctxt of

794 ctxt' = case lookupCtxt n ctxt of

793− [(CaseOp ci ty [] ps _, acc, tot, metainf)] ->

795+ [(CaseOp ci ty atys [] ps _, acc, tot, metainf)] ->

794 ctxt -- nothing to simplify (or already done...)

796 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)] ->

796 let ps_in' = map simpl ps_in

798 let ps_in' = map simpl ps_in

797 pdef = map debind ps_in' in

799 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

799 OK (CaseDef args sc _) ->

801 OK (CaseDef args sc _) ->

800 addDef n (CaseOp ci

802 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) }),

802 acc, tot, metainf) ctxt

804 acc, tot, metainf) ctxt

803 Error err -> error (show err)

805 Error err -> error (show err)

804 _ -> ctxt in

806 _ -> ctxt in

@@ -836,7 +838,7 @@ lookupTy n ctxt

836 (Function ty _) -> return ty

838 (Function ty _) -> return ty

837 (TyDecl _ ty) -> return ty

839 (TyDecl _ ty) -> return ty

838 (Operator ty _ _) -> return ty

840 (Operator ty _ _) -> return ty

839− (CaseOp _ ty _ _ _) -> return ty

841+ (CaseOp _ ty _ _ _ _) -> return ty

840

842

841isConName :: Name -> Context -> Bool

843isConName :: Name -> Context -> Bool

842isConName n ctxt = isTConName n ctxt || isDConName n ctxt

844isConName n ctxt = isTConName n ctxt || isDConName n ctxt

@@ -861,7 +863,7 @@ isFnName n ctxt

861 case tfst def of

863 case tfst def of

862 (Function _ _) -> return True

864 (Function _ _) -> return True

863 (Operator _ _ _) -> return True

865 (Operator _ _ _) -> return True

864− (CaseOp _ _ _ _ _) -> return True

866+ (CaseOp _ _ _ _ _ _) -> return True

865 _ -> return False

867 _ -> return False

866

868

867lookupP :: Name -> Context -> [Term]

869lookupP :: Name -> Context -> [Term]

@@ -870,7 +872,7 @@ lookupP n ctxt

870 p <- case def of

872 p <- case def of

871 (Function ty tm, a, _, _) -> return (P Ref n ty, a)

873 (Function ty tm, a, _, _) -> return (P Ref n ty, a)

872 (TyDecl nt ty, a, _, _) -> return (P nt n ty, a)

874 (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)

874 (Operator ty _ _, a, _, _) -> return (P Ref n ty, a)

876 (Operator ty _ _, a, _, _) -> return (P Ref n ty, a)

875 case snd p of

877 case snd p of

876 Hidden -> []

878 Hidden -> []

src/Idris/Core/Execute.hs+4−4

@@ -188,9 +188,9 @@ doExec env ctxt p@(P Ref n ty) =

188 [Function _ tm] -> doExec env ctxt tm

189 [TyDecl _ _] -> return (EP Ref n EErased) -- abstract def

190 [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

192 doExec env ctxt tm

193− [CaseOp _ _ _ _ (CaseDefs _ (ns, sc) _ _)] -> return (EP Ref n EErased)

193+ [CaseOp _ _ _ _ _ (CaseDefs _ (ns, sc) _ _)] -> return (EP Ref n EErased)

194 [] -> execFail $ "Could not find " ++ show n ++ " in definitions."

195 thing -> trace (take 200 $ "got to " ++ show thing ++ " lookup up " ++ show n) $ undefined

196doExec env ctxt p@(P Bound n ty) =

@@ -328,10 +328,10 @@ execApp' env ctxt f@(EP _ n _) args =

328 execApp' env ctxt r (drop arity args)

329 Nothing -> return (mkEApp f args)

330 else return (mkEApp f args)

331− [CaseOp _ _ _ _ (CaseDefs _ ([], STerm tm) _ _)] -> -- nullary fun

331+ [CaseOp _ _ _ _ _ (CaseDefs _ ([], STerm tm) _ _)] -> -- nullary fun

332 do rhs <- doExec env ctxt tm

333 execApp' env ctxt rhs args

334− [CaseOp _ _ _ _ (CaseDefs _ (ns, sc) _ _)] ->

334+ [CaseOp _ _ _ _ _ (CaseDefs _ (ns, sc) _ _)] ->

335 do res <- execCase env ctxt ns sc args

336 return $ fromMaybe (mkEApp f args) res

337 thing -> return $ mkEApp f args

src/Idris/Core/ProofState.hs+22−12

@@ -184,24 +184,26 @@ unify' ctxt env topx topy =

184 " in " ++ show env ++

185 "\nHoles: " ++ show (holes ps) ++ "\n") $

186 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

187 traceWhen (unifylog ps)

190 traceWhen (unifylog ps)

188 ("Unified " ++ show (topx, topy) ++ " without " ++ show dont ++

191 ("Unified " ++ show (topx, topy) ++ " without " ++ show dont ++

189 "\nSolved: " ++ show u ++ "\nNew problems: " ++ qshow fails

192 "\nSolved: " ++ show u ++ "\nNew problems: " ++ qshow fails

193+ ++ "\nNot unified:\n" ++ show (notunified ps)

190 ++ "\nCurrent problems:\n" ++ qshow (problems ps)

194 ++ "\nCurrent problems:\n" ++ qshow (problems ps)

191-- ++ show (pterm ps)

195-- ++ show (pterm ps)

192 ++ "\n----------") $

196 ++ "\n----------") $

193− case fails of

194−-- [] -> return u

195− err ->

196− do ps <- get

197+ do ps <- get

197− let (h, ns) = unified ps

198+ let (h, ns) = unified ps

198− let (ns', probs') = updateProblems (context ps) (u ++ ns)

199+ let (ns', probs') = updateProblems (context ps) (u ++ ns)

199− (err ++ problems ps)

200+ (fails ++ problems ps)

200− (injective ps)

201+ (injective ps)

201− (holes ps)

202+ (holes ps)

202− put (ps { problems = probs',

203+ put (ps { problems = probs',

203− unified = (h, ns') })

204+ unified = (h, ns'),

205+ notunified = notu ++ notunified ps })

204− return u

206+ return u

205

207

206getName :: Monad m => String -> StateT TState m Name

208getName :: Monad m => String -> StateT TState m Name

207getName tag = do ps <- get

209getName tag = do ps <- get

@@ -760,6 +762,11 @@ solveInProblems x val ((l, r, env, err) : ps)

760 = ((instantiate val (pToV x l), instantiate val (pToV x r),

762 = ((instantiate val (pToV x l), instantiate val (pToV x r),

761 updateEnv [(x, val)] env, err) : solveInProblems x val ps)

763 updateEnv [(x, val)] env, err) : solveInProblems x val ps)

762

764

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+

763updateProblems ctxt ns ps inj holes = up ns ps where

770updateProblems ctxt ns ps inj holes = up ns ps where

764 up ns [] = (ns, [])

771 up ns [] = (ns, [])

765 up ns ((x, y, env, err) : ps) =

772 up ns ((x, y, env, err) : ps) =

@@ -809,6 +816,7 @@ processTactic EndUnify ps

809 return (ps { pterm = tm',

816 return (ps { pterm = tm',

810 unified = (h, []),

817 unified = (h, []),

811 problems = probs',

818 problems = probs',

819+ notunified = updateNotunified ns (notunified ps),

812 holes = holes ps \\ map fst ns'' }, "")

820 holes = holes ps \\ map fst ns'' }, "")

813processTactic (Reorder n) ps

821processTactic (Reorder n) ps

814 = do ps' <- execStateT (tactic (Just n) reorder_claims) ps

822 = do ps' <- execStateT (tactic (Just n) reorder_claims) ps

@@ -823,6 +831,7 @@ processTactic UnifyProblems ps

823 pterm' = updateSolved ns' (pterm ps) in

831 pterm' = updateSolved ns' (pterm ps) in

824 return (ps { pterm = pterm', solved = Nothing, problems = probs',

832 return (ps { pterm = pterm', solved = Nothing, problems = probs',

825 previous = Just ps, plog = "",

833 previous = Just ps, plog = "",

834+ notunified = updateNotunified ns' (notunified ps),

826 holes = holes ps \\ (map fst ns') }, plog ps)

835 holes = holes ps \\ (map fst ns') }, plog ps)

827processTactic MatchProblems ps

836processTactic MatchProblems ps

828 = let (ns', probs') = matchProblems (context ps)

837 = let (ns', probs') = matchProblems (context ps)

@@ -850,6 +859,7 @@ processTactic t ps

850 return (ps' { pterm = pterm'',

859 return (ps' { pterm = pterm'',

851 solved = Nothing,

860 solved = Nothing,

852 problems = probs',

861 problems = probs',

862+ notunified = updateNotunified ns' (notunified ps'),

853 previous = Just ps, plog = "",

863 previous = Just ps, plog = "",

854 holes = holes ps' \\ (map fst ns')}, plog ps')

864 holes = holes ps' \\ (map fst ns')}, plog ps')

855

865

src/Idris/Core/Unify.hs+16−8

@@ -35,20 +35,20 @@ match_unify :: Context -> Env -> TT Name -> TT Name -> [Name] -> [Name] ->

35 TC [(Name, TT Name)]

36match_unify ctxt env topx topy dont holes =

37 case runStateT (un [] topx topy) (UI 0 []) of

38− OK (v, UI _ []) -> return (filter notTrivial v)

38+ OK (v, UI _ []) -> return (trimSolutions v)

39 res ->

40 let topxn = normalise ctxt env topx

41 topyn = normalise ctxt env topy in

42 case runStateT (un [] topxn topyn)

43 (UI 0 []) of

44 OK (v, UI _ fails) ->

45− return (filter notTrivial v)

45+ return (trimSolutions v)

46 Error e ->

47 -- just normalise the term we're matching against

48 case runStateT (un [] topxn topy)

49 (UI 0 []) of

50 OK (v, UI _ fails) ->

51− return (filter notTrivial v)

51+ return (trimSolutions v)

52 _ -> tfail e

53 where

54 un names (P _ x _) tm

@@ -128,9 +128,17 @@ match_unify ctxt env topx topy dont holes =

128 where inst [] tm = tm

129 inst ((n, _) : ns) tm = inst ns (substV (P Bound n Erased) tm)

130

131−notTrivial (x, P _ x' _) = x /= x'

131+trimSolutions ns = dropPairs ns

132−notTrivial _ = True

132+ where dropPairs [] = []

133−

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+

134expandLets env (x, tm) = (x, doSubst (reverse env) tm)

142expandLets env (x, tm) = (x, doSubst (reverse env) tm)

135 where

143 where

136 doSubst [] tm = tm

144 doSubst [] tm = tm

@@ -146,7 +154,7 @@ unify ctxt env topx topy dont holes =

146-- trace ("Unifying " ++ show (topx, topy)) $

154-- trace ("Unifying " ++ show (topx, topy)) $

147 -- don't bother if topx and topy are different at the head

155 -- don't bother if topx and topy are different at the head

148 case runStateT (un False [] topx topy) (UI 0 []) of

156 case runStateT (un False [] topx topy) (UI 0 []) of

149− OK (v, UI _ []) -> return (filter notTrivial v,

157+ OK (v, UI _ []) -> return (trimSolutions v,

150 [])

158 [])

151 res ->

159 res ->

152 let topxn = normalise ctxt env topx

160 let topxn = normalise ctxt env topx

@@ -155,7 +163,7 @@ unify ctxt env topx topy dont holes =

155 case runStateT (un False [] topxn topyn)

163 case runStateT (un False [] topxn topyn)

156 (UI 0 []) of

164 (UI 0 []) of

157 OK (v, UI _ fails) ->

165 OK (v, UI _ fails) ->

158− return (filter notTrivial v, reverse fails)

166+ return (trimSolutions v, reverse fails)

159-- Error e@(CantUnify False _ _ _ _ _) -> tfail e

167-- Error e@(CantUnify False _ _ _ _ _) -> tfail e

160 Error e -> tfail e

168 Error e -> tfail e

161 where

169 where

src/Idris/Coverage.hs+2−2

@@ -325,7 +325,7 @@ checkTotality path fc n

325 t' <- case t of

326 Unchecked ->

327 case lookupDef n ctxt of

328− [CaseOp _ _ _ pats _] ->

328+ [CaseOp _ _ _ _ pats _] ->

329 do t' <- if AssertTotal `elem` opts

330 then return $ Total []

331 else calcTotality path fc n pats

@@ -389,7 +389,7 @@ buildSCG (_, n) = do

389 ist <- getIState

390 case lookupCtxt n (idris_callgraph ist) of

391 [cg] -> case lookupDef n (tt_ctxt ist) of

392− [CaseOp _ _ pats _ cd] ->

392+ [CaseOp _ _ _ pats _ cd] ->

393 let (args, sc) = cases_totcheck cd in

394 do logLvl 2 $ "Building SCG for " ++ show n ++ " from\n"

395 ++ 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

74 logLvl 2 $ show n ++ " type " ++ showImp Nothing True False ty

75 ((tyT, defer, is), log) <-

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

78 ds <- checkDef fc defer

79 let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds

80 addDeferred ds'

@@ -182,7 +182,7 @@ elabData info syn doc fc opts (PLaterdecl n t_in)

182 t_in <- implicit syn n t_in

183 let t = addImpl i t_in

184 ((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))

186 def' <- checkDef fc defer

187 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) def'

188 addDeferredTyCon def''

@@ -201,7 +201,7 @@ elabData info syn doc fc opts (PDatadecl n t_in dcons)

201 let t = addImpl i t_in

202 ((t', defer, is), log) <-

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

205 def' <- checkDef fc defer

206 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) def'

207 -- 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

659 let lhs = addImplPat i lhs_in

660 ((lhs', dlhs, []), _) <-

661 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")

663 (infTerm lhs)))

664 let lhs_tm = orderPats (getInferTerm lhs')

665 let lhs_ty = getInferType lhs'

@@ -671,7 +671,7 @@ elabTransform info fc safe lhs_in rhs_in

671 ((rhs', defer), _) <-

672 tclift $ elaborate ctxt (MN 0 "transRHS") clhs_ty []

673 (do pbinds lhs_tm

674− erun fc (build i info False (UN "transform") rhs)

674+ erun fc (build i info False [] (UN "transform") rhs)

675 erun fc $ psolve lhs_tm

676 tt <- get_term

677 let (tm, ds) = runState (collectDeferred Nothing tt) []

@@ -805,7 +805,7 @@ elabCon info syn tn codata (doc, n, t_in, fc)

805 logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ showImp Nothing True False t

806 ((t', defer, is), log) <-

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

809 logLvl 2 $ "Rechecking " ++ show t'

810 def' <- checkDef fc defer

811 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

846 -- question: CAFs in where blocks?

847 tclift $ tfail $ At fc (NoTypeDecl n)

848 [ty] -> return ty

849+ let atys = map snd (getArgTys fty)

849 pats_in <- mapM (elabClause info opts)

850 pats_in <- mapM (elabClause info opts)

850 (zip [0..] cs)

851 (zip [0..] cs)

851 logLvl 3 $ "Elaborated patterns:\n" ++ show pats_in

852 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

928

929

929 let optpdef = map debind optpats -- \$ map (simple_lhs (tt_ctxt ist)) optpats

930 let optpdef = map debind optpats -- \$ map (simple_lhs (tt_ctxt ist)) optpats

930 tree@(CaseDef scargs sc _) <- tclift $

931 tree@(CaseDef scargs sc _) <- tclift $

931− simpleCase tcase False reflect CompileTime fc pdef

932+ simpleCase tcase False reflect CompileTime fc atys pdef

932 cov <- coverage

933 cov <- coverage

933 pmissing <-

934 pmissing <-

934 if cov

935 if cov

@@ -976,7 +977,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

976 let knowncovering = (pcover && cov) || AssertTotal `elem` opts

977 let knowncovering = (pcover && cov) || AssertTotal `elem` opts

977

978

978 tree' <- tclift $ simpleCase tcase knowncovering reflect

979 tree' <- tclift $ simpleCase tcase knowncovering reflect

979− RunTime fc pdef'

980+ RunTime fc atys pdef'

980 logLvl 3 (show tree)

981 logLvl 3 (show tree)

981 logLvl 3 $ "Optimised: " ++ show tree'

982 logLvl 3 $ "Optimised: " ++ show tree'

982 ctxt <- getContext

983 ctxt <- getContext

@@ -989,6 +990,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

989 tcase knowncovering

990 tcase knowncovering

990 reflect

991 reflect

991 (AssertTotal `elem` opts)

992 (AssertTotal `elem` opts)

993+ atys

992 pats

994 pats

993 pdef pdef pdef_inl pdef' ty)

995 pdef pdef pdef_inl pdef' ty)

994 addIBC (IBCDef n)

996 addIBC (IBCDef n)

@@ -998,7 +1000,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

998 when (tot /= Unchecked) $ addIBC (IBCTotal n tot)

1000 when (tot /= Unchecked) $ addIBC (IBCTotal n tot)

999 i <- getIState

1001 i <- getIState

1000 case lookupDef n (tt_ctxt i) of

1002 case lookupDef n (tt_ctxt i) of

1001− (CaseOp _ _ _ _ cd : _) ->

1003+ (CaseOp _ _ _ _ _ cd : _) ->

1002 let (scargs, sc) = cases_compiletime cd

1004 let (scargs, sc) = cases_compiletime cd

1003 (scargs', sc') = cases_runtime cd in

1005 (scargs', sc') = cases_runtime cd in

1004 do let calls = findCalls sc' scargs'

1006 do let calls = findCalls sc' scargs'

@@ -1167,7 +1169,7 @@ elabValBind info aspat tm_in

1167-- tctry (elaborate ctxt (MN 0 "val") (TType (UVal 0)) []

1169-- tctry (elaborate ctxt (MN 0 "val") (TType (UVal 0)) []

1168-- (build i info aspat (MN 0 "val") tm))

1170-- (build i info aspat (MN 0 "val") tm))

1169 tclift (elaborate ctxt (MN 0 "val") infP []

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

1171 let vtm = orderPats (getInferTerm tm')

1173 let vtm = orderPats (getInferTerm tm')

1172

1174

1173 def' <- checkDef (fileFC "(input)") defer

1175 def' <- checkDef (fileFC "(input)") defer

@@ -1198,7 +1200,7 @@ checkPossible info fc tcgen fname lhs_in

1198 let lhs = addImpl i lhs_in

1200 let lhs = addImpl i lhs_in

1199 -- if the LHS type checks, it is possible

1201 -- if the LHS type checks, it is possible

1200 case elaborate ctxt (MN 0 "patLHS") infP []

1202 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

1202 OK ((lhs', _, _), _) ->

1204 OK ((lhs', _, _), _) ->

1203 do let lhs_tm = orderPats (getInferTerm lhs')

1205 do let lhs_tm = orderPats (getInferTerm lhs')

1204 case recheck ctxt [] (forget lhs_tm) lhs_tm of

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

1254 ((lhs', dlhs, []), _) <-

1256 ((lhs', dlhs, []), _) <-

1255 tclift $ elaborate ctxt (MN 0 "patLHS") infP []

1257 tclift $ elaborate ctxt (MN 0 "patLHS") infP []

1256 (errAt "left hand side of " fname

1258 (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))))

1258 let lhs_tm = orderPats (getInferTerm lhs')

1260 let lhs_tm = orderPats (getInferTerm lhs')

1259 let lhs_ty = getInferType lhs'

1261 let lhs_ty = getInferType lhs'

1260 logLvl 3 ("Elaborated: " ++ show lhs_tm)

1262 logLvl 3 ("Elaborated: " ++ show lhs_tm)

@@ -1297,7 +1299,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1297 tclift $ elaborate ctxt (MN 0 "patRHS") clhsty []

1299 tclift $ elaborate ctxt (MN 0 "patRHS") clhsty []

1298 (do pbinds lhs_tm

1300 (do pbinds lhs_tm

1299 (_, _, is) <- errAt "right hand side of " fname

1301 (_, _, 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))

1301 errAt "right hand side of " fname

1303 errAt "right hand side of " fname

1302 (erun fc $ psolve lhs_tm)

1304 (erun fc $ psolve lhs_tm)

1303 hs <- get_holes

1305 hs <- get_holes

@@ -1426,12 +1428,12 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

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

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

1427 -- pattern bindings

1429 -- pattern bindings

1428 i <- getIState

1430 i <- getIState

1429− let lhs = addImplPat i lhs_in

1431+ let lhs = addImplPat i (stripLinear i lhs_in)

1430 logLvl 5 ("LHS: " ++ showImp Nothing True False lhs)

1432 logLvl 5 ("LHS: " ++ showImp Nothing True False lhs)

1431 ((lhs', dlhs, []), _) <-

1433 ((lhs', dlhs, []), _) <-

1432 tclift $ elaborate ctxt (MN 0 "patLHS") infP []

1434 tclift $ elaborate ctxt (MN 0 "patLHS") infP []

1433 (errAt "left hand side of with in " fname

1435 (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))) )

1435 let lhs_tm = orderPats (getInferTerm lhs')

1437 let lhs_tm = orderPats (getInferTerm lhs')

1436 let lhs_ty = getInferType lhs'

1438 let lhs_ty = getInferType lhs'

1437 let ret_ty = getRetTy lhs_ty

1439 let ret_ty = getRetTy lhs_ty

@@ -1448,7 +1450,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

1448 (do pbinds lhs_tm

1450 (do pbinds lhs_tm

1449 -- TODO: may want where here - see winfo abpve

1451 -- TODO: may want where here - see winfo abpve

1450 (_', d, is) <- errAt "with value in " fname

1452 (_', 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)))

1452 erun fc $ psolve lhs_tm

1454 erun fc $ psolve lhs_tm

1453 tt <- get_term

1455 tt <- get_term

1454 return (tt, d, is))

1456 return (tt, d, is))

@@ -1509,7 +1511,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

1509 ((rhs', defer, is), _) <-

1511 ((rhs', defer, is), _) <-

1510 tclift $ elaborate ctxt (MN 0 "wpatRHS") clhsty []

1512 tclift $ elaborate ctxt (MN 0 "wpatRHS") clhsty []

1511 (do pbinds lhs_tm

1513 (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)

1513 psolve lhs_tm

1515 psolve lhs_tm

1514 tt <- get_term

1516 tt <- get_term

1515 return (tt, d, is))

1517 return (tt, d, is))

@@ -1847,7 +1849,7 @@ elabInstance info syn fc cs n ps t expn ds

1847 ctxt <- getContext

1849 ctxt <- getContext

1848 ((tyT, _, _), _) <-

1850 ((tyT, _, _), _) <-

1849 tclift $ elaborate ctxt iname (TType (UVal 0)) []

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

1851 ctxt <- getContext

1853 ctxt <- getContext

1852 (cty, _) <- recheckC fc [] tyT

1854 (cty, _) <- recheckC fc [] tyT

1853 let nty = normalise ctxt [] cty

1855 let nty = normalise ctxt [] cty

src/Idris/ElabTerm.hs+71−52

@@ -38,10 +38,10 @@ toplevel = EInfo [] emptyContext id Nothing

39-- Also find deferred names in the term and their types

41−build :: IState -> ElabInfo -> Bool -> Name -> PTerm ->

41+build :: IState -> ElabInfo -> Bool -> FnOpts -> Name -> PTerm ->

42 ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])

43−build ist info pattern fn tm

43+build ist info pattern opts fn tm

44− = do elab ist info pattern False fn tm

44+ = do elab ist info pattern opts fn tm

45 ivs <- get_instances

46 hs <- get_holes

47 ptm <- get_term

@@ -78,10 +78,10 @@ build ist info pattern fn tm

78-- (Separate, so we don't go overboard resolving things that we don't

79-- know about yet on the LHS of a pattern def)

81−buildTC :: IState -> ElabInfo -> Bool -> Bool -> Name -> PTerm ->

81+buildTC :: IState -> ElabInfo -> Bool -> FnOpts -> Name -> PTerm ->

82 ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])

83−buildTC ist info pattern tcgen fn tm

83+buildTC ist info pattern opts fn tm

84− = do elab ist info pattern tcgen fn tm

84+ = do elab ist info pattern opts fn tm

85 probs <- get_probs

86 tm <- get_term

87 case probs of

@@ -97,19 +97,22 @@ buildTC ist info pattern tcgen fn tm

97-- Returns the set of declarations we need to add to complete the definition

98-- (most likely case blocks to elaborate)

100−elab :: IState -> ElabInfo -> Bool -> Bool -> Name -> PTerm ->

100+elab :: IState -> ElabInfo -> Bool -> FnOpts -> Name -> PTerm ->

101 ElabD ()

102−elab ist info pattern tcgen fn tm

102+elab ist info pattern opts fn tm

103 = do let loglvl = opt_logLevel (idris_options ist)

104 when (loglvl > 5) $ unifyLog True

105 compute -- expand type synonyms, etc

106− elabE (False, False) tm -- (in argument, guarded)

106+ elabE (False, False, False) tm -- (in argument, guarded, in type)

107 end_unify

108 when pattern -- convert remaining holes to pattern vars

109 (do update_term orderPats

110 tm <- get_term

111 mkPat)

112 where

113+ tcgen = Dictionary `elem` opts

114+ reflect = Reflection `elem` opts

115+

113 isph arg = case getTm arg of

116 isph arg = case getTm arg of

114 Placeholder -> (True, priority arg)

117 Placeholder -> (True, priority arg)

115 _ -> (False, priority arg)

118 _ -> (False, priority arg)

@@ -128,6 +131,7 @@ elab ist info pattern tcgen fn tm

128 (h: hs) -> do patvar h; mkPat

131 (h: hs) -> do patvar h; mkPat

129 [] -> return ()

132 [] -> return ()

130

133

134+ elabE :: (Bool, Bool, Bool) -> PTerm -> ElabD ()

131 elabE ina t = {- do g <- goal

135 elabE ina t = {- do g <- goal

132 tm <- get_term

136 tm <- get_term

133 trace ("Elaborating " ++ show t ++ " : " ++ show g ++ "\n\tin " ++ show tm)

137 trace ("Elaborating " ++ show t ++ " : " ++ show g ++ "\n\tin " ++ show tm)

@@ -147,9 +151,18 @@ elab ist info pattern tcgen fn tm

147

151

148 local f = do e <- get_env

152 local f = do e <- get_env

149 return (f `elem` map fst e)

153 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

150

160

151 elab' ina (PNoImplicits t) = elab' ina t -- skip elabE step

161 elab' ina (PNoImplicits t) = elab' ina t -- skip elabE step

152 elab' ina PType = do apply RType []; solve

162 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")

153 elab' ina (PConstant c) = do apply (RConstant c) []; solve

166 elab' ina (PConstant c) = do apply (RConstant c) []; solve

154 elab' ina (PQuote r) = do fill r; solve

167 elab' ina (PQuote r) = do fill r; solve

155 elab' ina (PTrue fc) = try (elab' ina (PRef fc unitCon))

168 elab' ina (PTrue fc) = try (elab' ina (PRef fc unitCon))

@@ -171,13 +184,13 @@ elab ist info pattern tcgen fn tm

171 [pimp (MN 0 "a") Placeholder True,

184 [pimp (MN 0 "a") Placeholder True,

172 pimp (MN 0 "b") Placeholder False,

185 pimp (MN 0 "b") Placeholder False,

173 pexp l, pexp r])

186 pexp l, pexp r])

174− elab' ina@(_, a) (PPair fc l r)

187+ elab' ina@(_, a, inty) (PPair fc l r)

175 = do hnf_compute

188 = do hnf_compute

176 g <- goal

189 g <- goal

177 case g of

190 case g of

178− TType _ -> elabE (True, a) (PApp fc (PRef fc pairTy)

191+ TType _ -> elabE (True, a,inty) (PApp fc (PRef fc pairTy)

179− [pexp l,pexp r])

192+ [pexp l,pexp r])

180− _ -> elabE (True, a) (PApp fc (PRef fc pairCon)

193+ _ -> elabE (True, a, inty) (PApp fc (PRef fc pairCon)

181 [pimp (MN 0 "A") Placeholder True,

194 [pimp (MN 0 "A") Placeholder True,

182 pimp (MN 0 "B") Placeholder True,

195 pimp (MN 0 "B") Placeholder True,

183 pexp l, pexp r])

196 pexp l, pexp r])

@@ -225,7 +238,10 @@ elab ist info pattern tcgen fn tm

225 trySeq' deferr (x : xs)

238 trySeq' deferr (x : xs)

226 = try' (elab' ina x) (trySeq' deferr xs) True

239 = try' (elab' ina x) (trySeq' deferr xs) True

227 elab' ina (PPatvar fc n) | pattern = patvar n

240 elab' ina (PPatvar fc n) | pattern = patvar 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")

228− elab' (ina, guarded) (PRef fc n) | pattern && not (inparamBlock n)

244+ elab' (ina, guarded, inty) (PRef fc n) | pattern && not (inparamBlock n)

229 = do ctxt <- get_context

245 = do ctxt <- get_context

230 let defined = case lookupTy n ctxt of

246 let defined = case lookupTy n ctxt of

231 [] -> False

247 [] -> False

@@ -242,7 +258,7 @@ elab ist info pattern tcgen fn tm

242 _ -> True

258 _ -> True

243 elab' ina f@(PInferRef fc n) = elab' ina (PApp fc f [])

259 elab' ina f@(PInferRef fc n) = elab' ina (PApp fc f [])

244 elab' ina (PRef fc n) = erun fc $ do apply (Var n) []; solve

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

246 = do -- n' <- unique_hole n

262 = do -- n' <- unique_hole n

247 -- let sc' = mapPT (repN n n') sc

263 -- let sc' = mapPT (repN n n') sc

248 ptm <- get_term

264 ptm <- get_term

@@ -250,10 +266,10 @@ elab ist info pattern tcgen fn tm

250 checkPiGoal n

266 checkPiGoal n

251 attack; intro (Just n);

267 attack; intro (Just n);

252 -- trace ("------ intro " ++ show n ++ " ---- \n" ++ show ptm)

268 -- trace ("------ intro " ++ show n ++ " ---- \n" ++ show ptm)

253− elabE (True, a) sc; solve

269+ elabE (True, a, inty) sc; solve

254 where repN n n' (PRef fc x) | x == n' = PRef fc n'

270 where repN n n' (PRef fc x) | x == n' = PRef fc n'

255 repN _ _ t = t

271 repN _ _ t = t

256− elab' ina@(_, a) (PLam n ty sc)

272+ elab' ina@(_, a, inty) (PLam n ty sc)

257 = do hsin <- get_holes

273 = do hsin <- get_holes

258 ptmin <- get_term

274 ptmin <- get_term

259 tyn <- unique_hole (MN 0 "lamty")

275 tyn <- unique_hole (MN 0 "lamty")

@@ -268,12 +284,12 @@ elab ist info pattern tcgen fn tm

268 introTy (Var tyn) (Just n)

284 introTy (Var tyn) (Just n)

269 -- end_unify

285 -- end_unify

270 focus tyn

286 focus tyn

271− elabE (True, a) ty

287+ elabE (True, a, True) ty

272− elabE (True, a) sc

288+ elabE (True, a, inty) sc

273 solve

289 solve

274− elab' ina@(_,a) (PPi _ n Placeholder sc)

290+ elab' ina@(_, a, _) (PPi _ n Placeholder sc)

275− = do attack; arg n (MN 0 "ty"); elabE (True, a) sc; solve

291+ = do attack; arg n (MN 0 "ty"); elabE (True, a, True) sc; solve

276− elab' ina@(_,a) (PPi _ n ty sc)

292+ elab' ina@(_, a, _) (PPi _ n ty sc)

277 = do attack; tyn <- unique_hole (MN 0 "ty")

293 = do attack; tyn <- unique_hole (MN 0 "ty")

278 claim tyn RType

294 claim tyn RType

279 n' <- case n of

295 n' <- case n of

@@ -281,10 +297,10 @@ elab ist info pattern tcgen fn tm

281 _ -> return n

297 _ -> return n

282 forall n' (Var tyn)

298 forall n' (Var tyn)

283 focus tyn

299 focus tyn

284− elabE (True, a) ty

300+ elabE (True, a, True) ty

285− elabE (True, a) sc

301+ elabE (True, a, True) sc

286 solve

302 solve

287− elab' ina@(_,a) (PLet n ty val sc)

303+ elab' ina@(_, a, inty) (PLet n ty val sc)

288 = do attack;

304 = do attack;

289 tyn <- unique_hole (MN 0 "letty")

305 tyn <- unique_hole (MN 0 "letty")

290 claim tyn RType

306 claim tyn RType

@@ -296,17 +312,17 @@ elab ist info pattern tcgen fn tm

296 Placeholder -> return ()

312 Placeholder -> return ()

297 _ -> do focus tyn

313 _ -> do focus tyn

298 explicit tyn

314 explicit tyn

299− elabE (True, a) ty

315+ elabE (True, a, True) ty

300 focus valn

316 focus valn

301− elabE (True, a) val

317+ elabE (True, a, True) val

302 env <- get_env

318 env <- get_env

303− elabE (True, a) sc

319+ elabE (True, a, inty) sc

304 -- HACK: If the name leaks into its type, it may leak out of

320 -- HACK: If the name leaks into its type, it may leak out of

305 -- scope outside, so substitute in the outer scope.

321 -- scope outside, so substitute in the outer scope.

306 expandLet n (case lookup n env of

322 expandLet n (case lookup n env of

307 Just (Let t v) -> v)

323 Just (Let t v) -> v)

308 solve

324 solve

309− elab' ina@(_,a) (PGoal fc r n sc) = do

325+ elab' ina@(_, a, inty) (PGoal fc r n sc) = do

310 rty <- goal

326 rty <- goal

311 attack

327 attack

312 tyn <- unique_hole (MN 0 "letty")

328 tyn <- unique_hole (MN 0 "letty")

@@ -315,10 +331,10 @@ elab ist info pattern tcgen fn tm

315 claim valn (Var tyn)

331 claim valn (Var tyn)

316 letbind n (Var tyn) (Var valn)

332 letbind n (Var tyn) (Var valn)

317 focus valn

333 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)])

319 env <- get_env

335 env <- get_env

320 computeLet n

336 computeLet n

321− elabE (True, a) sc

337+ elabE (True, a, inty) sc

322 solve

338 solve

323-- elab' ina (PLet n Placeholder

339-- elab' ina (PLet n Placeholder

324-- (PApp fc r [pexp (delab ist rty)]) sc)

340-- (PApp fc r [pexp (delab ist rty)]) sc)

@@ -368,14 +384,17 @@ elab ist info pattern tcgen fn tm

368 Just xs@(_:_) -> NS n xs

384 Just xs@(_:_) -> NS n xs

369 _ -> n

385 _ -> n

370

386

371− elab' (ina, g) (PMatchApp fc fn)

387+ elab' ina (PMatchApp fc fn)

372 = do (fn', imps) <- case lookupCtxtName fn (idris_implicits ist) of

388 = do (fn', imps) <- case lookupCtxtName fn (idris_implicits ist) of

373 [(n, args)] -> return (n, map (const True) args)

389 [(n, args)] -> return (n, map (const True) args)

374 _ -> lift $ tfail (NoSuchVariable fn)

390 _ -> lift $ tfail (NoSuchVariable fn)

375 ns <- match_apply (Var fn') (map (\x -> (x,0)) imps)

391 ns <- match_apply (Var fn') (map (\x -> (x,0)) imps)

376 solve

392 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")

377 -- if f is local, just do a simple_app

396 -- 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')

379 = do let args = {- case lookupCtxt f (inblock info) of

398 = do let args = {- case lookupCtxt f (inblock info) of

380 Just ps -> (map (pexp . (PRef fc)) ps ++ args')

399 Just ps -> (map (pexp . (PRef fc)) ps ++ args')

381 _ -> -} args'

400 _ -> -} args'

@@ -383,8 +402,8 @@ elab ist info pattern tcgen fn tm

383 env <- get_env

402 env <- get_env

384 if (f `elem` map fst env && length args' == 1)

403 if (f `elem` map fst env && length args' == 1)

385 then -- simple app, as below

404 then -- simple app, as below

386− do simple_app (elabE (ina, g) (PRef fc f))

405+ do simple_app (elabE (ina, g, inty) (PRef fc f))

387− (elabE (True, g) (getTm (head args')))

406+ (elabE (True, g, inty) (getTm (head args')))

388 (show tm)

407 (show tm)

389 solve

408 solve

390 else

409 else

@@ -408,7 +427,7 @@ elab ist info pattern tcgen fn tm

408 sortBy (\(_,x) (_,y) ->

427 sortBy (\(_,x) (_,y) ->

409 compare (priority x) (priority y))

428 compare (priority x) (priority y))

410 (zip ns args)

429 (zip ns args)

411− elabArgs (ina || not isinf, guarded)

430+ elabArgs (ina || not isinf, guarded, inty)

412 [] fc False ns' (map (\x -> (lazyarg x, getTm x)) eargs)

431 [] fc False ns' (map (\x -> (lazyarg x, getTm x)) eargs)

413 mkSpecialised ist fc f (map getTm args') tm

432 mkSpecialised ist fc f (map getTm args') tm

414 solve

433 solve

@@ -439,9 +458,9 @@ elab ist info pattern tcgen fn tm

439 setInjective (PApp _ (PRef _ n) _) = setinj n

458 setInjective (PApp _ (PRef _ n) _) = setinj n

440 setInjective _ = return ()

459 setInjective _ = return ()

441

460

442− elab' ina@(_, a) tm@(PApp fc f [arg])

461+ elab' ina@(_, a, inty) tm@(PApp fc f [arg])

443 = erun fc $

462 = 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))

445 (show tm)

464 (show tm)

446 solve

465 solve

447 elab' ina Placeholder = do (h : hs) <- get_holes

466 elab' ina Placeholder = do (h : hs) <- get_holes

@@ -490,7 +509,7 @@ elab ist info pattern tcgen fn tm

490 elab' ina sc

509 elab' ina sc

491 elab' ina (PRef fc letn)

510 elab' ina (PRef fc letn)

492 solve

511 solve

493− elab' ina@(_, a) c@(PCase fc scr opts)

512+ elab' ina@(_, a, inty) c@(PCase fc scr opts)

494 = do attack

513 = do attack

495 tyn <- unique_hole (MN 0 "scty")

514 tyn <- unique_hole (MN 0 "scty")

496 claim tyn RType

515 claim tyn RType

@@ -499,7 +518,7 @@ elab ist info pattern tcgen fn tm

499 claim valn (Var tyn)

518 claim valn (Var tyn)

500 letbind scvn (Var tyn) (Var valn)

519 letbind scvn (Var tyn) (Var valn)

501 focus valn

520 focus valn

502− elabE (True, a) scr

521+ elabE (True, a, inty) scr

503 args <- get_env

522 args <- get_env

504 cname <- unique_hole' True (mkCaseName fn)

523 cname <- unique_hole' True (mkCaseName fn)

505 let cname' = mkN cname

524 let cname' = mkN cname

@@ -682,9 +701,9 @@ findInstances ist t

682 | otherwise = []

701 | otherwise = []

683

702

684trivial' ist

703trivial' ist

685− = trivial (elab ist toplevel False False (MN 0 "tac")) ist

704+ = trivial (elab ist toplevel False [] (MN 0 "tac")) ist

686proofSearch' ist top n hints

705proofSearch' 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

688

707

689

708

690resolveTC :: Int -> Term -> Name -> IState -> ElabD ()

709resolveTC :: Int -> Term -> Name -> IState -> ElabD ()

@@ -813,7 +832,7 @@ runTac autoSolve ist tac

813 where

832 where

814 bname (Bind n _ _) = Just n

833 bname (Bind n _ _) = Just n

815 bname _ = Nothing

834 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

817 when autoSolve solveAll

836 when autoSolve solveAll

818 runT (MatchRefine fn)

837 runT (MatchRefine fn)

819 = do fnimps <-

838 = do fnimps <-

@@ -860,7 +879,7 @@ runTac autoSolve ist tac

860 letn <- unique_hole (MN 0 "equiv_val")

879 letn <- unique_hole (MN 0 "equiv_val")

861 letbind letn (Var tyn) (Var valn)

880 letbind letn (Var tyn) (Var valn)

862 focus tyn

881 focus tyn

863− elab ist toplevel False False (MN 0 "tac") tm

882+ elab ist toplevel False [] (MN 0 "tac") tm

864 focus valn

883 focus valn

865 when autoSolve solveAll

884 when autoSolve solveAll

866 runT (Rewrite tm) -- to elaborate tm, let bind it, then rewrite by that

885 runT (Rewrite tm) -- to elaborate tm, let bind it, then rewrite by that

@@ -873,7 +892,7 @@ runTac autoSolve ist tac

873 letn <- unique_hole (MN 0 "rewrite_rule")

892 letn <- unique_hole (MN 0 "rewrite_rule")

874 letbind letn (Var tyn) (Var valn)

893 letbind letn (Var tyn) (Var valn)

875 focus valn

894 focus valn

876− elab ist toplevel False False (MN 0 "tac") tm

895+ elab ist toplevel False [] (MN 0 "tac") tm

877 rewrite (Var letn)

896 rewrite (Var letn)

878 when autoSolve solveAll

897 when autoSolve solveAll

879 runT (Induction nm)

898 runT (Induction nm)

@@ -888,7 +907,7 @@ runTac autoSolve ist tac

888 letn <- unique_hole n

907 letn <- unique_hole n

889 letbind letn (Var tyn) (Var valn)

908 letbind letn (Var tyn) (Var valn)

890 focus valn

909 focus valn

891− elab ist toplevel False False (MN 0 "tac") tm

910+ elab ist toplevel False [] (MN 0 "tac") tm

892 when autoSolve solveAll

911 when autoSolve solveAll

893 runT (LetTacTy n ty tm)

912 runT (LetTacTy n ty tm)

894 = do attack

913 = do attack

@@ -899,9 +918,9 @@ runTac autoSolve ist tac

899 letn <- unique_hole n

918 letn <- unique_hole n

900 letbind letn (Var tyn) (Var valn)

919 letbind letn (Var tyn) (Var valn)

901 focus tyn

920 focus tyn

902− elab ist toplevel False False (MN 0 "tac") ty

921+ elab ist toplevel False [] (MN 0 "tac") ty

903 focus valn

922 focus valn

904− elab ist toplevel False False (MN 0 "tac") tm

923+ elab ist toplevel False [] (MN 0 "tac") tm

905 when autoSolve solveAll

924 when autoSolve solveAll

906 runT Compute = compute

925 runT Compute = compute

907 runT Trivial = do trivial' ist; when autoSolve solveAll

926 runT Trivial = do trivial' ist; when autoSolve solveAll

@@ -919,7 +938,7 @@ runTac autoSolve ist tac

919 scriptvar <- unique_hole (MN 0 "scriptvar" )

938 scriptvar <- unique_hole (MN 0 "scriptvar" )

920 letbind scriptvar scriptTy (Var script)

939 letbind scriptvar scriptTy (Var script)

921 focus script

940 focus script

922− elab ist toplevel False False (MN 0 "tac") tm

941+ elab ist toplevel False [] (MN 0 "tac") tm

923 (script', _) <- get_type_val (Var scriptvar)

942 (script', _) <- get_type_val (Var scriptvar)

924 -- now that we have the script apply

943 -- now that we have the script apply

925 -- it to the reflected goal and context

944 -- it to the reflected goal and context

@@ -952,7 +971,7 @@ runTac autoSolve ist tac

952 letbind scriptvar scriptTy (Var script)

971 letbind scriptvar scriptTy (Var script)

953 focus script

972 focus script

954 ptm <- get_term

973 ptm <- get_term

955− elab ist toplevel False False (MN 0 "tac")

974+ elab ist toplevel False [] (MN 0 "tac")

956 (PApp emptyFC tm [pexp (delabTy' ist [] tgoal True True)])

975 (PApp emptyFC tm [pexp (delabTy' ist [] tgoal True True)])

957 (script', _) <- get_type_val (Var scriptvar)

976 (script', _) <- get_type_val (Var scriptvar)

958 -- now that we have the script apply

977 -- now that we have the script apply

@@ -980,7 +999,7 @@ runTac autoSolve ist tac

980 letn <- unique_hole (MN 0 "letvar")

999 letn <- unique_hole (MN 0 "letvar")

981 letbind letn (Var tyn) (Var valn)

1000 letbind letn (Var tyn) (Var valn)

982 focus valn

1001 focus valn

983− elab ist toplevel False False (MN 0 "tac") v

1002+ elab ist toplevel False [] (MN 0 "tac") v

984 (value, _) <- get_type_val (Var letn)

1003 (value, _) <- get_type_val (Var letn)

985 ctxt <- get_context

1004 ctxt <- get_context

986 env <- get_env

1005 env <- get_env

@@ -994,7 +1013,7 @@ runTac autoSolve ist tac

994 letn <- unique_hole (MN 0 "letvar")

1013 letn <- unique_hole (MN 0 "letvar")

995 letbind letn (Var tyn) (Var valn)

1014 letbind letn (Var tyn) (Var valn)

996 focus valn

1015 focus valn

997− elab ist toplevel False False (MN 0 "tac") v

1016+ elab ist toplevel False [] (MN 0 "tac") v

998 (value, _) <- get_type_val (Var letn)

1017 (value, _) <- get_type_val (Var letn)

999 ctxt <- get_context

1018 ctxt <- get_context

1000 env <- get_env

1019 env <- get_env

src/Idris/IBC.hs+11−9

@@ -23,7 +23,7 @@ import Debug.Trace

23import Paths_idris

25ibcVersion :: Word8

26−ibcVersion = 49

26+ibcVersion = 50

28data IBCFile = IBCFile { ver :: Word8,

29 sourcefile :: FilePath,

@@ -801,12 +801,13 @@ instance Binary Def where

801 put x2

802 -- all primitives just get added at the start, don't write

803 Operator x1 x2 x3 -> do return ()

804− CaseOp x1 x2 x3 x3a x4 -> do putWord8 3

804+ CaseOp x1 x2 x2a x3 x3a x4 -> do putWord8 3

805− put x1

805+ put x1

806− put x2

806+ put x2

807− put x3

807+ put x2a

808+ put x3

808− -- no x3a

809+ -- no x3a

809− put x4

810+ put x4

810 get

811 get

811 = do i <- getWord8

812 = do i <- getWord8

812 case i of

813 case i of

@@ -820,9 +821,10 @@ instance Binary Def where

820 3 -> do x1 <- get

821 3 -> do x1 <- get

821 x2 <- get

822 x2 <- get

822 x3 <- get

823 x3 <- get

823− -- x3 <- get always []

824 x4 <- get

825+ -- x3 <- get always []

826+ x5 <- get

825− return (CaseOp x1 x2 x3 [] x4)

827+ return (CaseOp x1 x2 x3 x4 [] x5)

826 _ -> error "Corrupted binary data for Def"

828 _ -> error "Corrupted binary data for Def"

827

829

828instance Binary Accessibility where

830instance Binary Accessibility where

src/Idris/Prover.hs+2−1

@@ -65,7 +65,7 @@ prove ctxt lit n ty

65 ideslavePutSExp "end-proof-mode" n

66 let proofs = proof_list i

67 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)]

69 logLvl 3 (show tree)

70 (ptm, pty) <- recheckC (fileFC "proof") [] tm

71 logLvl 5 ("Proof type: " ++ show pty ++ "\n" ++

@@ -75,6 +75,7 @@ prove ctxt lit n ty

75 Error e -> ierror (CantUnify False ty pty e [] 0)

76 ptm' <- applyOpts ptm

77 updateContext (addCasedef n (CaseInfo True False) False False True False

78+ []

78 [Right (P Ref n ty, ptm)]

79 [Right (P Ref n ty, ptm)]

79 [([], P Ref n ty, ptm)]

80 [([], P Ref n ty, ptm)]

81 [([], P Ref n ty, ptm)]

src/Idris/REPL.hs+15−22

@@ -77,14 +77,12 @@ import Debug.Trace

78-- | Run the REPL

79repl :: IState -- ^ The initial state

80− -> MVar IState -- ^ Server's MVar

81 -> [FilePath] -- ^ The loaded modules

80 -> [FilePath] -- ^ The loaded modules

82 -> InputT Idris ()

81 -> InputT Idris ()

83−repl orig stvar mods

82+repl orig mods

84 = H.catch

83 = H.catch

85 (do let quiet = opt_quiet (idris_options orig)

84 (do let quiet = opt_quiet (idris_options orig)

86 i <- lift getIState

85 i <- lift getIState

87− lift $ runIO $ swapMVar stvar i -- update shared state

88 let colour = idris_colourRepl i

86 let colour = idris_colourRepl i

89 let theme = idris_colourTheme i

87 let theme = idris_colourTheme i

90 let mvs = idris_metavars i

88 let mvs = idris_metavars i

@@ -98,15 +96,15 @@ repl orig stvar mods

98 Nothing -> do lift $ when (not quiet) (iputStrLn "Bye bye")

96 Nothing -> do lift $ when (not quiet) (iputStrLn "Bye bye")

99 return ()

97 return ()

100 Just input -> H.catch

98 Just input -> H.catch

101− (do ms <- lift $ processInput stvar input orig mods

99+ (do ms <- lift $ processInput input orig mods

102 case ms of

100 case ms of

103− Just mods -> repl orig stvar mods

101+ Just mods -> repl orig mods

104 Nothing -> return ())

102 Nothing -> return ())

105 ctrlC)

103 ctrlC)

106 ctrlC

104 ctrlC

107 where ctrlC :: SomeException -> InputT Idris ()

105 where ctrlC :: SomeException -> InputT Idris ()

108 ctrlC e = do lift $ iputStrLn (show e)

106 ctrlC e = do lift $ iputStrLn (show e)

109− repl orig stvar mods

107+ repl orig mods

110

108

111 showMVs c thm [] = ""

109 showMVs c thm [] = ""

112 showMVs c thm ms = "Metavariables: " ++

110 showMVs c thm ms = "Metavariables: " ++

@@ -124,15 +122,14 @@ repl orig stvar mods

124 else show n

122 else show n

125

123

126-- | Run the REPL server

124-- | Run the REPL server

127−startServer :: IState -> MVar IState -> [FilePath] -> Idris ()

125+startServer :: IState -> [FilePath] -> Idris ()

128−startServer orig stvar fn_in = do tid <- runIO $ forkOS serverLoop

126+startServer orig fn_in = do tid <- runIO $ forkOS serverLoop

129− return ()

127+ return ()

130 where serverLoop :: IO ()

128 where serverLoop :: IO ()

131 -- TODO: option for port number

129 -- TODO: option for port number

132 serverLoop = withSocketsDo $

130 serverLoop = withSocketsDo $

133 do sock <- listenOnLocalhost $ PortNumber 4294

131 do sock <- listenOnLocalhost $ PortNumber 4294

134− i <- readMVar stvar

135− loop fn i sock

132+ loop fn orig sock

136

133

137 fn = case fn_in of

134 fn = case fn_in of

138 (f:_) -> f

135 (f:_) -> f

@@ -146,19 +143,16 @@ startServer orig stvar fn_in = do tid <- runIO $ forkOS serverLoop

146 host == "127.0.0.1")

143 host == "127.0.0.1")

147 then do

144 then do

148 cmd <- hGetLine h

145 cmd <- hGetLine h

149− takeMVar stvar

150− (ist', fn) <- processNetCmd stvar orig ist h fn cmd

146+ (ist', fn) <- processNetCmd orig ist h fn cmd

151− putMVar stvar ist'

152 hClose h

147 hClose h

153 loop fn ist' sock

148 loop fn ist' sock

154 else do

149 else do

155 putStrLn $ "Closing connection attempt from non-localhost " ++ host

150 putStrLn $ "Closing connection attempt from non-localhost " ++ host

156 hClose h

151 hClose h

157

152

158−processNetCmd :: MVar IState ->

159− IState -> IState -> Handle -> FilePath -> String ->

153+processNetCmd :: IState -> IState -> Handle -> FilePath -> String ->

160 IO (IState, FilePath)

154 IO (IState, FilePath)

161−processNetCmd stvar orig i h fn cmd

155+processNetCmd orig i h fn cmd

162 = do res <- case parseCmd i "(net)" cmd of

156 = do res <- case parseCmd i "(net)" cmd of

163 Failure err -> return (Left (Msg " invalid command"))

157 Failure err -> return (Left (Msg " invalid command"))

164 Success c -> runErrorT $ evalStateT (processNet fn c) i

158 Success c -> runErrorT $ evalStateT (processNet fn c) i

@@ -337,9 +331,9 @@ lit f = case splitExtension f of

337 (_, ".lidr") -> True

331 (_, ".lidr") -> True

338 _ -> False

332 _ -> False

339

333

340−processInput :: MVar IState -> String ->

334+processInput :: String ->

341 IState -> [FilePath] -> Idris (Maybe [FilePath])

335 IState -> [FilePath] -> Idris (Maybe [FilePath])

342−processInput stvar cmd orig inputs

336+processInput cmd orig inputs

343 = do i <- getIState

337 = do i <- getIState

344 let opts = idris_options i

338 let opts = idris_options i

345 let quiet = opt_quiet opts

339 let quiet = opt_quiet opts

@@ -1224,9 +1218,8 @@ idrisMain opts =

1224

1218

1225 when (runrepl && not idesl) $ do

1219 when (runrepl && not idesl) $ do

1226 initScript

1220 initScript

1227− stvar <- runIO $ newMVar ist

1228− startServer ist stvar inputs

1221+ startServer ist inputs

1229− runInputT (replSettings (Just historyFile)) $ repl ist stvar inputs

1222+ runInputT (replSettings (Just historyFile)) $ repl ist inputs

1230 when (idesl) $ ideslaveStart ist inputs

1223 when (idesl) $ ideslaveStart ist inputs

1231 ok <- noErrors

1224 ok <- noErrors

1232 when (not ok) $ runIO (exitWith (ExitFailure 1))

1225 when (not ok) $ runIO (exitWith (ExitFailure 1))

src/Util/DynamicLinker.hs+6−2

@@ -5,11 +5,12 @@ module Util.DynamicLinker where

6#ifdef IDRIS_FFI

7import Foreign.LibFFI

8−import Foreign.Ptr (nullPtr, FunPtr, nullFunPtr,castPtrToFunPtr)

8+import Foreign.Ptr (Ptr(), nullPtr, FunPtr, nullFunPtr, castPtrToFunPtr)

9import System.Directory

10#ifndef WINDOWS

11import System.Posix.DynamicLinker

12#else

13+import qualified Control.Exception as Exception (catch, IOException)

13import System.Win32.DLL

14import System.Win32.DLL

14import System.Win32.Types

15import System.Win32.Types

15type DL = HMODULE

16type DL = HMODULE

@@ -63,10 +64,13 @@ tryLoadFn fn (Lib _ h) = do cFn <- dlsym h fn

63tryLoadLib :: String -> IO (Maybe DynamicLib)

64tryLoadLib :: String -> IO (Maybe DynamicLib)

64tryLoadLib lib = do exactName <- doesFileExist lib

65tryLoadLib lib = do exactName <- doesFileExist lib

65 let filename = if exactName then lib else lib ++ "." ++ hostDynamicLibExt

66 let filename = if exactName then lib else lib ++ "." ++ hostDynamicLibExt

66− handle <- loadLibrary filename

67+ handle <- Exception.catch (loadLibrary filename) nullPtrOnException

67 if handle == nullPtr

68 if handle == nullPtr

68 then return Nothing

69 then return Nothing

69 else return . Just $ Lib lib handle

70 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

71tryLoadFn :: String -> DynamicLib -> IO (Maybe ForeignFun)

75tryLoadFn :: String -> DynamicLib -> IO (Maybe ForeignFun)

72tryLoadFn fn (Lib _ h) = do cFn <- getProcAddress h fn

76tryLoadFn fn (Lib _ h) = do cFn <- getProcAddress h fn

test/reg005/reg005.idr+1

@@ -48,3 +48,4 @@ Main.eqCharOK = proof {

48 exact x = x;

49}

51+