d3eb486 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

First attempt now at substitution to default args

d3eb486Timo Petteri Sinnemäki13 years ago

src/Idris/AbsSyntax.hs+70−30

compare with master

unifiedsplit

@@ -1205,7 +1205,7 @@ addUsingConstraints syn fc t

1205 | otherwise = doAdd cs ns t

1206

1207 mkConst c args = PApp fc (PRef fc c)

1208− (map (\n -> PExp 0 [] (PRef fc n)) args)

1208+ (map (\n -> PExp 0 [] (sMN 0 "carg" (PRef fc n)) args)

1209

1210 getConstraints (PPi (Constraint _ _) _ c sc)

1211 = getcapp c ++ getConstraints sc

@@ -1217,7 +1217,7 @@ addUsingConstraints syn fc t

1217 return (UConstraint c ns)

1218 getcapp _ = []

1219

1220− getName (PExp _ _ (PRef _ n)) = return n

1220+ getName (PExp _ _ _ (PRef _ n)) = return n

1221 getName _ = []

1222

1223-- Add implicit Pi bindings for any names in the term which appear in an

@@ -1225,13 +1225,15 @@ addUsingConstraints syn fc t

1225

1226-- This has become a right mess already. Better redo it some time...

1227

1228−implicit :: SyntaxInfo -> Name -> PTerm -> Idris PTerm

1228+implicit :: ElabInfo -> SyntaxInfo -> Name -> PTerm -> Idris PTerm

1229−implicit syn n ptm = implicit' syn [] n ptm

1229+implicit info syn n ptm = implicit' info syn [] n ptm

1230

1231−implicit' :: SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm

1231+implicit' :: ElabInfo -> SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm

1232−implicit' syn ignore n ptm

1232+implicit' info syn ignore n ptm

1233 = do i <- getIState

1234 let (tm', impdata) = implicitise syn ignore i ptm

1235+ -- TODO WIP check impdata for unknown vars in default args

1236+ defaultArgCheck (eInfoNames info ++ keys (idris_implicits i)) impdata

1235-- let (tm'', spos) = findStatics i tm'

1237-- let (tm'', spos) = findStatics i tm'

1236 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }

1238 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }

1237 addIBC (IBCImp n)

1239 addIBC (IBCImp n)

@@ -1239,6 +1241,24 @@ implicit' syn ignore n ptm

1239-- i <- get

1241-- i <- get

1240-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }

1242-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }

1241 return tm'

1243 return tm'

1244+ where

1245+ -- Detect unknown names in default arguments and throw error if found.

1246+ defaultArgCheck :: [Name] -> [PArg] -> Idris ()

1247+ defaultArgCheck names params = foldM_ names params unknownInDefault

1248+

1249+ unknownInDefault :: [Name] -> PArg -> Idris [Name]

1250+ unknownInDefault ns (PTacImplicit _ _ n script _)

1251+ = case notFound (namesIn script) ns of

1252+ Nothing -> return (n:ns)

1253+ Just name -> throwError (NoSuchVariable name)

1254+ -- TODO See if PConstraint in addition to PExp can reasonably have

1255+ -- a name. Until then, 'pname p' worksn't.

1256+ unknownInDefault ns p = return (pname p):ns

1257+

1258+ unknown :: [Name] -> [Name] -> Maybe Name

1259+ unknown [] _ = Nothing

1260+ unknown (SN (WhereN _ _ _)):as bs = unknown as bs

1261+ unknown a:as bs = if elem a bs then unknown as bs else Just a

1242

1262

1243implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])

1263implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])

1244implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

1264implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

@@ -1284,7 +1304,7 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

1284 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]

1304 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]

1285 _ -> [])

1305 _ -> [])

1286 (decls, ns) <- get -- ignore decls in HO types

1306 (decls, ns) <- get -- ignore decls in HO types

1287− put (PExp (getPriority ist ty) l Placeholder : decls,

1307+ put (PExp (getPriority ist ty) l n Placeholder : decls,

1288 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

1308 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

1289 imps True (n:env) sc

1309 imps True (n:env) sc

1290 imps top env (PPi (Constraint l _) n ty sc)

1310 imps top env (PPi (Constraint l _) n ty sc)

@@ -1292,7 +1312,7 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

1292 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]

1312 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]

1293 _ -> [])

1313 _ -> [])

1294 (decls, ns) <- get -- ignore decls in HO types

1314 (decls, ns) <- get -- ignore decls in HO types

1295− put (PConstraint 10 l Placeholder : decls,

1315+ put (PConstraint 10 l n Placeholder : decls,

1296 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

1316 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

1297 imps True (n:env) sc

1317 imps True (n:env) sc

1298 imps top env (PPi (TacImp l _ scr) n ty sc)

1318 imps top env (PPi (TacImp l _ scr) n ty sc)

@@ -1458,7 +1478,7 @@ aiFn inpat True ist fc f ds []

1458-- any constructor alts || any allImp ialts))

1478-- any constructor alts || any allImp ialts))

1459 then aiFn inpat False ist fc f ds [] -- use it as a constructor

1479 then aiFn inpat False ist fc f ds [] -- use it as a constructor

1460 else Right $ PPatvar fc f

1480 else Right $ PPatvar fc f

1461− where imp (PExp _ _ _) = False

1481+ where imp (PExp _ _ _ _) = False

1462 imp _ = True

1482 imp _ = True

1463-- allImp [] = False

1483-- allImp [] = False

1464 allImp xs = all imp xs

1484 allImp xs = all imp xs

@@ -1505,25 +1525,45 @@ aiFn inpat expat ist fc f ds as

1505 [(n,t)] -> t

1525 [(n,t)] -> t

1506 _ -> Public

1526 _ -> Public

1507

1527

1508−

1528+ -- TODO WIP substitution into default arg expressions.

1509− insertImpl :: [PArg] -> [PArg] -> [PArg]

1529+ -- - An extra accumulator parameter here?

1530+ -- - Accumulator of what?

1531+ -- - Map of param names and their corresponding arg terms?

1532+ -- - Perhaps in an 'inner' function, though?

1533+ -- - Though OTOH perhaps this one should become the inner

1534+ -- function?

1535+ -- - Check for existing call sites of insertImpl.

1536+ -- - Well, easy: this is in a where block :-).

1537+ insertImpl :: M.Map Name PTerm -- accumulated param names & arg terms

1538+ -> [PArg] -- parameters

1539+ -> [PArg] -- arguments

1540+ -> [PArg]

1510− insertImpl (PExp p l ty : ps) (PExp _ _ tm : given) =

1541+ insertImpl pnas (PExp p l n ty : ps) (PExp _ _ _ tm : given) =

1511− PExp p l tm : insertImpl ps given

1542+ PExp p l n tm : insertImpl (M.insert n tm pnas) ps given

1512− insertImpl (PConstraint p l ty : ps) (PConstraint _ _ tm : given) =

1543+ insertImpl pnas (PConstraint p l n ty : ps) (PConstraint _ _ _ tm : given) =

1513− PConstraint p l tm : insertImpl ps given

1544+ PConstraint p l n tm : insertImpl (M.insert n tm pnas) ps given

1514− insertImpl (PConstraint p l ty : ps) given =

1545+ insertImpl pnas (PConstraint p l n ty : ps) given =

1515− PConstraint p l (PResolveTC fc) : insertImpl ps given

1546+ let rtc = PResolveTC fc in

1547+ PConstraint p l n rtc : insertImpl (M.insert n rtc pnas) ps given

1516− insertImpl (PImp p _ l n ty : ps) given =

1548+ insertImpl pnas (PImp p _ l n ty : ps) given =

1517 case find n given [] of

1549 case find n given [] of

1550+ Just (tm, given') ->

1518− Just (tm, given') -> PImp p False l n tm : insertImpl ps given'

1551+ PImp p False l n tm : insertImpl (M.insert n tm pnas) ps given'

1552+ Nothing ->

1519− Nothing -> PImp p True l n Placeholder : insertImpl ps given

1553+ PImp p True l n Placeholder :

1554+ insertImpl (M.insert n Placeholder pnas) ps given

1520− insertImpl (PTacImplicit p l n sc' ty : ps) given =

1555+ insertImpl pnas (PTacImplicit p l n sc' ty : ps) given =

1521− let sc = addImpl ist sc' in

1556+ let sc = addImpl ist (substMatches (toList pnas) sc') in

1522 case find n given [] of

1557 case find n given [] of

1558+ Just (tm, given') ->

1523− Just (tm, given') -> PTacImplicit p l n sc tm : insertImpl ps given'

1559+ PTacImplicit p l n sc tm :

1560+ insertImpl (M.insert n tm pnas) ps given'

1524− Nothing -> if inpat

1561+ Nothing ->

1562+ if inpat

1525− then PTacImplicit p l n sc Placeholder : insertImpl ps given

1563+ then PTacImplicit p l n sc Placeholder :

1564+ insertImpl (M.insert n Placeholder pnas) ps given

1526− else PTacImplicit p l n sc sc : insertImpl ps given

1565+ else PTacImplicit p l n sc sc :

1566+ insertImpl (M.insert n sc pnas) ps given

1527 insertImpl expected [] = []

1567 insertImpl expected [] = []

1528 insertImpl _ given = given

1568 insertImpl _ given = given

1529

1569

@@ -1562,11 +1602,11 @@ stripLinear i tm = evalState (sl tm) [] where

1562 return $ PApp fc fn args'

1602 return $ PApp fc fn args'

1563 where slA (PImp p m l n t) = do t' <- sl t

1603 where slA (PImp p m l n t) = do t' <- sl t

1564 return $ PImp p m l n t'

1604 return $ PImp p m l n t'

1565− slA (PExp p l t) = do t' <- sl t

1605+ slA (PExp p l n t) = do t' <- sl t

1566− return $ PExp p l t'

1606+ return $ PExp p l n t'

1567− slA (PConstraint p l t)

1607+ slA (PConstraint p l n t)

1568 = do t' <- sl t

1608 = do t' <- sl t

1569− return $ PConstraint p l t'

1609+ return $ PConstraint p l n t'

1570 slA (PTacImplicit p l n sc t)

1610 slA (PTacImplicit p l n sc t)

1571 = do t' <- sl t

1611 = do t' <- sl t

1572 return $ PTacImplicit p l n sc t'

1612 return $ PTacImplicit p l n sc t'

src/Idris/AbsSyntaxTree.hs+10−8

@@ -771,9 +771,11 @@ data PArg' t = PImp { priority :: Int,

771 pname :: Name, getTm :: t }

772 | PExp { priority :: Int,

773 argopts :: [ArgOpt],

774+ pname :: Name,

774 getTm :: t }

775 getTm :: t }

775 | PConstraint { priority :: Int,

776 | PConstraint { priority :: Int,

776 argopts :: [ArgOpt],

777 argopts :: [ArgOpt],

778+ pname :: Name,

777 getTm :: t }

779 getTm :: t }

778 | PTacImplicit { priority :: Int,

780 | PTacImplicit { priority :: Int,

779 argopts :: [ArgOpt],

781 argopts :: [ArgOpt],

@@ -790,8 +792,8 @@ lazyarg tm = Lazy `elem` argopts tm

790

792

791instance Sized a => Sized (PArg' a) where

793instance Sized a => Sized (PArg' a) where

792 size (PImp p _ l nm trm) = 1 + size nm + size trm

794 size (PImp p _ l nm trm) = 1 + size nm + size trm

793− size (PExp p l trm) = 1 + size trm

795+ size (PExp p l nm trm) = 1 + size nm + size trm

794− size (PConstraint p l trm) = 1 + size trm

796+ size (PConstraint p l nm trm) = 1 + size nm +size nm + size trm

795 size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm

797 size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm

796

798

797{-!

799{-!

@@ -800,8 +802,8 @@ deriving instance NFData PArg'

800!-}

802!-}

801

803

802pimp n t mach = PImp 1 mach [Lazy] n t

804pimp n t mach = PImp 1 mach [Lazy] n t

803−pexp t = PExp 1 [] t

805+pexp t = PExp 1 [] (sMN 0 "arg") t

804−pconst t = PConstraint 1 [] t

806+pconst t = PConstraint 1 [] (sMN 0 "carg") t

805ptacimp n s t = PTacImplicit 2 [Lazy] n s t

807ptacimp n s t = PTacImplicit 2 [Lazy] n s t

806

808

807type PArg = PArg' PTerm

809type PArg = PArg' PTerm

@@ -1259,8 +1261,8 @@ pprintPTerm impl bnd docArgs = prettySe 10 bnd

1259 prettySe p bnd _ = text "test"

1261 prettySe p bnd _ = text "test"

1260

1262

1261 prettyArgS bnd (PImp _ _ _ n tm) = prettyArgSi bnd (n, tm)

1263 prettyArgS bnd (PImp _ _ _ n tm) = prettyArgSi bnd (n, tm)

1262− prettyArgS bnd (PExp _ _ tm) = prettyArgSe bnd tm

1264+ prettyArgS bnd (PExp _ _ _ tm) = prettyArgSe bnd tm

1263− prettyArgS bnd (PConstraint _ _ tm) = prettyArgSc bnd tm

1265+ prettyArgS bnd (PConstraint _ _ _ tm) = prettyArgSc bnd tm

1264 prettyArgS bnd (PTacImplicit _ _ n _ tm) = prettyArgSti bnd (n, tm)

1266 prettyArgS bnd (PTacImplicit _ _ n _ tm) = prettyArgSti bnd (n, tm)

1265

1267

1266 prettyArgSe bnd arg = prettySe 0 bnd arg

1268 prettyArgSe bnd arg = prettySe 0 bnd arg

@@ -1389,12 +1391,12 @@ getImps (_ : xs) = getImps xs

1389

1391

1390getExps :: [PArg] -> [PTerm]

1392getExps :: [PArg] -> [PTerm]

1391getExps [] = []

1393getExps [] = []

1392−getExps (PExp _ _ tm : xs) = tm : getExps xs

1394+getExps (PExp _ _ _ tm : xs) = tm : getExps xs

1393getExps (_ : xs) = getExps xs

1395getExps (_ : xs) = getExps xs

1394

1396

1395getConsts :: [PArg] -> [PTerm]

1397getConsts :: [PArg] -> [PTerm]

1396getConsts [] = []

1398getConsts [] = []

1397−getConsts (PConstraint _ _ tm : xs) = tm : getConsts xs

1399+getConsts (PConstraint _ _ _ tm : xs) = tm : getConsts xs

1398getConsts (_ : xs) = getConsts xs

1400getConsts (_ : xs) = getConsts xs

1399

1401

1400getAll :: [PArg] -> [PTerm]

1402getAll :: [PArg] -> [PTerm]

src/Idris/Coverage.hs+2−2

@@ -56,8 +56,8 @@ genClauses fc n xs given

56 -- there may be more case splitting that the idris_implicits record

57 -- suggests)

58 let parg = case lookupCtxt n (idris_implicits i) of

59− (p : _) -> p ++ repeat (PExp 0 [] Placeholder)

59+ (p : _) -> p ++ repeat (PExp 0 [] (sMN 0 "gcarg") Placeholder)

60− _ -> repeat (pexp Placeholder)

60+ _ -> repeat (pexp Placeholder)

61 let tryclauses = mkClauses parg all_args

62 logLvl 2 $ show (length tryclauses) ++ " initially to check"

63 logLvl 5 $ showSep "\n" (map (showTm i) tryclauses)

src/Idris/DeepSeq.hs+4−4

@@ -276,10 +276,10 @@ instance (NFData t) => NFData (PDo' t) where

276instance (NFData t) => NFData (PArg' t) where

277 rnf (PImp x1 x2 x3 x4 x5)

278 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

279− rnf (PExp x1 x2 x3)

279+ rnf (PExp x1 x2 x3 x4)

280− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

280+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

281− rnf (PConstraint x1 x2 x3)

281+ rnf (PConstraint x1 x2 x3 x4)

282− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

282+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

283 rnf (PTacImplicit x1 x2 x3 x4 x5)

284 = rnf x1 `seq`

285 rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

src/Idris/Delaborate.hs+3−3

@@ -58,7 +58,7 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

58 = PLam n (de env [] ty) (de ((n,n):env) [] sc)

59 de env ((PImp { argopts = opts }):is) (Bind n (Pi ty) sc)

60 = PPi (Imp opts Dynamic False) n (de env [] ty) (de ((n,n):env) is sc)

61− de env (PConstraint _ _ _:is) (Bind n (Pi ty) sc)

61+ de env (PConstraint _ _ _ _:is) (Bind n (Pi ty) sc)

62 = PPi constraint n (de env [] ty) (de ((n,n):env) is sc)

63 de env (PTacImplicit _ _ _ tac _:is) (Bind n (Pi ty) sc)

64 = PPi (tacimpl tac) n (de env [] ty) (de ((n,n):env) is sc)

@@ -121,8 +121,8 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

121 | otherwise = PApp un (PRef un n) (map pexp args)

122

123 imp (PImp p m l n _) arg = PImp p m l n arg

124− imp (PExp p l _) arg = PExp p l arg

124+ imp (PExp p l n _) arg = PExp p l n arg

125− imp (PConstraint p l _) arg = PConstraint p l arg

125+ imp (PConstraint p l n _) arg = PConstraint p l n arg

126 imp (PTacImplicit p l n sc _) arg = PTacImplicit p l n sc arg

127

128-- | How far to indent sub-errors

src/Idris/ElabDecls.hs+35−28

@@ -80,7 +80,7 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

81 logLvl 3 $ show n ++ " pre-type " ++ showTmImpls ty'

82 ty' <- addUsingConstraints syn fc ty'

83− ty' <- implicit syn n ty'

83+ ty' <- implicit info syn n ty'

85 let ty = addImpl i ty'

86 logLvl 3 $ show n ++ " type " ++ showTmImpls ty

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

202 checkUndefined fc n

203 ctxt <- getContext

204 i <- getIState

205+ -- TODO think: something more in info?

205− t_in <- implicit syn n t_in

206+ t_in <- implicit info syn n t_in

206 let t = addImpl i t_in

207 let t = addImpl i t_in

207 ((t', defer, is), log) <- tclift $ elaborate ctxt n (TType (UVal 0)) []

208 ((t', defer, is), log) <- tclift $ elaborate ctxt n (TType (UVal 0)) []

208 (erun fc (build i info False [] n t))

209 (erun fc (build i info False [] n t))

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

220 undef <- isUndefined fc n

221 undef <- isUndefined fc n

221 ctxt <- getContext

222 ctxt <- getContext

222 i <- getIState

223 i <- getIState

223− t_in <- implicit syn n t_in

224+ t_in <- implicit info syn n t_in

224 let t = addImpl i t_in

225 let t = addImpl i t_in

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

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

226 tclift $ elaborate ctxt n (TType (UVal 0)) []

227 tclift $ elaborate ctxt n (TType (UVal 0)) []

@@ -728,7 +729,8 @@ elabRecord :: ElabInfo -> SyntaxInfo -> Docstring -> FC -> Name ->

728 PTerm -> Docstring -> Name -> PTerm -> Idris ()

729 PTerm -> Docstring -> Name -> PTerm -> Idris ()

729elabRecord info syn doc fc tyn ty cdoc cn cty

730elabRecord info syn doc fc tyn ty cdoc cn cty

730 = do elabData info syn doc [] fc [] (PDatadecl tyn ty [(cdoc, [], cn, cty, fc, [])])

731 = do elabData info syn doc [] fc [] (PDatadecl tyn ty [(cdoc, [], cn, cty, fc, [])])

732+ -- TODO think: something more in info?

731− cty' <- implicit syn cn cty

733+ cty' <- implicit info syn cn cty

732 i <- getIState

734 i <- getIState

733 cty <- case lookupTy cn (tt_ctxt i) of

735 cty <- case lookupTy cn (tt_ctxt i) of

734 [t] -> return (delab i t)

736 [t] -> return (delab i t)

@@ -750,7 +752,7 @@ elabRecord info syn doc fc tyn ty cdoc cn cty

750 where

752 where

751-- syn = syn_in { syn_namespace = show (nsroot tyn) : syn_namespace syn_in }

753-- syn = syn_in { syn_namespace = show (nsroot tyn) : syn_namespace syn_in }

752

754

753− isNonImp (PExp _ _ _, a) = Just a

755+ isNonImp (PExp _ _ _ _, a) = Just a

754 isNonImp _ = Nothing

756 isNonImp _ = Nothing

755

757

756 tryElabDecl info (fn, ty, val)

758 tryElabDecl info (fn, ty, val)

@@ -839,7 +841,8 @@ elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)

839 = do checkUndefined fc n

841 = do checkUndefined fc n

840 ctxt <- getContext

842 ctxt <- getContext

841 i <- getIState

843 i <- getIState

844+ -- TODO think: something more in info?

842− t_in <- implicit syn n (if codata then mkLazy t_in else t_in)

845+ t_in <- implicit info syn n (if codata then mkLazy t_in else t_in)

843 let t = addImpl i t_in

846 let t = addImpl i t_in

844 logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t

847 logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t

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

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

@@ -1288,7 +1291,7 @@ checkPossible info fc tcgen fname lhs_in

1288 ((P _ x _, _), (P _ y _, _)) -> x == y

1291 ((P _ x _, _), (P _ y _, _)) -> x == y

1289 _ -> False

1292 _ -> False

1290

1293

1291−getFixedInType i env (PExp _ _ _ : is) (Bind n (Pi t) sc)

1294+getFixedInType i env (PExp _ _ _ _ : is) (Bind n (Pi t) sc)

1292 = getFixedInType i (n : env) is (instantiate (P Bound n t) sc)

1295 = getFixedInType i (n : env) is (instantiate (P Bound n t) sc)

1293getFixedInType i env (_ : is) (Bind n (Pi t) sc)

1296getFixedInType i env (_ : is) (Bind n (Pi t) sc)

1294 = getFixedInType i (n : env) is (instantiate (P Bound n t) sc)

1297 = getFixedInType i (n : env) is (instantiate (P Bound n t) sc)

@@ -1416,10 +1419,10 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1416 -- Elaborate where block

1419 -- Elaborate where block

1417 ist <- getIState

1420 ist <- getIState

1418 windex <- getName

1421 windex <- getName

1419− let winfo = pinfo (pvars ist lhs_tm) whereblock windex

1420 let decls = nub (concatMap declared whereblock)

1422 let decls = nub (concatMap declared whereblock)

1421 let defs = nub (decls ++ concatMap defined whereblock)

1423 let defs = nub (decls ++ concatMap defined whereblock)

1422 let newargs = pvars ist lhs_tm

1424 let newargs = pvars ist lhs_tm

1425+ let winfo = pinfo info newargs defs windex

1423 let wb = map (expandParamsD False ist decorate newargs defs) whereblock

1426 let wb = map (expandParamsD False ist decorate newargs defs) whereblock

1424

1427

1425 -- Split the where block into declarations with a type, and those

1428 -- Split the where block into declarations with a type, and those

@@ -1428,7 +1431,11 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1428 let (wbefore, wafter) = sepBlocks wb

1431 let (wbefore, wafter) = sepBlocks wb

1429

1432

1430 logLvl 2 $ "Where block:\n " ++ show wbefore ++ "\n" ++ show wafter

1433 logLvl 2 $ "Where block:\n " ++ show wbefore ++ "\n" ++ show wafter

1434+ -- FIXME Changed info to winfo. Make sure that breaksn't things!

1435+ -- - Changed it back for now; possibly want a differently

1436+ -- modified ElabInfo.

1437+ -- - Changed back back after modifying pinfo.

1431− mapM_ (elabDecl' EAll info) wbefore

1438+ mapM_ (elabDecl' EAll winfo) wbefore

1432 -- Now build the RHS, using the type of the LHS as the goal.

1439 -- Now build the RHS, using the type of the LHS as the goal.

1433 i <- getIState -- new implicits from where block

1440 i <- getIState -- new implicits from where block

1434 logLvl 5 (showTmImpls (expandParams decorate newargs defs (defs \\ decls) rhs_in))

1441 logLvl 5 (showTmImpls (expandParams decorate newargs defs (defs \\ decls) rhs_in))

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

1443 mapM_ setinj (nub (params ++ inj))

1450 mapM_ setinj (nub (params ++ inj))

1444 setNextName

1451 setNextName

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

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

1446− (erun fc (build i info False opts fname rhs))

1453+ (erun fc (build i winfo False opts fname rhs))

1447 errAt "right hand side of " fname

1454 errAt "right hand side of " fname

1448 (erun fc $ psolve lhs_tm)

1455 (erun fc $ psolve lhs_tm)

1449 hs <- get_holes

1456 hs <- get_holes

@@ -1471,8 +1478,8 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1471 -- Now the remaining deferred (i.e. no type declarations) clauses

1478 -- Now the remaining deferred (i.e. no type declarations) clauses

1472 -- from the where block

1479 -- from the where block

1473

1480

1474− mapM_ (elabDecl' EAll info) wafter

1481+ mapM_ (elabDecl' EAll winfo) wafter

1475− mapM_ (elabCaseBlock info opts) is

1482+ mapM_ (elabCaseBlock winfo opts) is

1476

1483

1477 ctxt <- getContext

1484 ctxt <- getContext

1478 logLvl 5 $ "Rechecking"

1485 logLvl 5 $ "Rechecking"

@@ -1524,19 +1531,6 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1524 (b : bf, af)

1531 (b : bf, af)

1525 sepBlocks' ns [] = ([], [])

1532 sepBlocks' ns [] = ([], [])

1526

1533

1527− pinfo ns ps i

1528− = let ds = concatMap declared ps

1529− newps = params info ++ ns

1530− dsParams = map (\n -> (n, map fst newps)) ds

1531− newb = addAlist dsParams (inblock info)

1532− l = liftname info in

1533− info { params = newps,

1534− inblock = newb,

1535− liftname = id -- (\n -> case lookupCtxt n newb of

1536− -- Nothing -> n

1537− -- _ -> MN i (show n)) . l

1538− }

1539−

1540

1534

1541 -- if a hole is just an argument/result of a case block, treat it as

1535 -- if a hole is just an argument/result of a case block, treat it as

1542 -- the unit type. Hack to help elaborate case in do blocks.

1536 -- the unit type. Hack to help elaborate case in do blocks.

@@ -2005,7 +1999,8 @@ elabInstance info syn what fc cs n ps t expn ds = do

2005 -- TODO: largely based upon elabType' - should try to abstract

1999 -- TODO: largely based upon elabType' - should try to abstract

2006 elabFindOverlapping i ci iname syn t

2000 elabFindOverlapping i ci iname syn t

2007 = do ty' <- addUsingConstraints syn fc t

2001 = do ty' <- addUsingConstraints syn fc t

2002+ -- TODO think: something more in info?

2008− ty' <- implicit syn iname ty'

2003+ ty' <- implicit info syn iname ty'

2009 let ty = addImpl i ty'

2004 let ty = addImpl i ty'

2010 ctxt <- getContext

2005 ctxt <- getContext

2011 ((tyT, _, _), _) <-

2006 ((tyT, _, _), _) <-

@@ -2043,9 +2038,9 @@ elabInstance info syn what fc cs n ps t expn ds = do

2043 methArgs i (PPi (Imp _ _ _) n ty sc)

2038 methArgs i (PPi (Imp _ _ _) n ty sc)

2044 = PImp 0 True [] n (PRef fc (sMN i "meth")) : methArgs (i+1) sc

2039 = PImp 0 True [] n (PRef fc (sMN i "meth")) : methArgs (i+1) sc

2045 methArgs i (PPi (Exp _ _ _) n ty sc)

2040 methArgs i (PPi (Exp _ _ _) n ty sc)

2046− = PExp 0 [] (PRef fc (sMN i "meth")) : methArgs (i+1) sc

2041+ = PExp 0 [] (sMN 0 "marg") (PRef fc (sMN i "meth")) : methArgs (i+1) sc

2047 methArgs i (PPi (Constraint _ _) n ty sc)

2042 methArgs i (PPi (Constraint _ _) n ty sc)

2048− = PConstraint 0 [] (PResolveTC fc) : methArgs (i+1) sc

2043+ = PConstraint 0 [] (sMN 0 "marg") (PResolveTC fc) : methArgs (i+1) sc

2049 methArgs i _ = []

2044 methArgs i _ = []

2050

2045

2051 papp fc f [] = f

2046 papp fc f [] = f

@@ -2166,6 +2161,18 @@ psolve tm = return ()

2166pvars ist (Bind n (PVar t) sc) = (n, delab ist t) : pvars ist sc

2161pvars ist (Bind n (PVar t) sc) = (n, delab ist t) : pvars ist sc

2167pvars ist _ = []

2162pvars ist _ = []

2168

2163

2164+pinfo info ns ds i

2165+ = let newps = params info ++ ns

2166+ dsParams = map (\n -> (n, map fst newps)) ds

2167+ newb = addAlist dsParams (inblock info)

2168+ l = liftname info in

2169+ info { params = newps,

2170+ inblock = newb,

2171+ liftname = id -- (\n -> case lookupCtxt n newb of

2172+ -- Nothing -> n

2173+ -- _ -> MN i (show n)) . l

2174+ }

2175+

2169data ElabWhat = ETypes | EDefns | EAll

2176data ElabWhat = ETypes | EDefns | EAll

2170 deriving (Show, Eq)

2177 deriving (Show, Eq)

2171

2178

src/Idris/ElabTerm.hs+3

@@ -36,6 +36,9 @@ data ElabInfo = EInfo { params :: [(Name, PTerm)],

37toplevel = EInfo [] emptyContext id Nothing

39+eInfoNames :: ElabInfo -> [Name]

40+eInfoNames info = map fst (params info) ++ keys (inblock info)

41+

39-- Using the elaborator, convert a term in raw syntax to a fully

42-- Using the elaborator, convert a term in raw syntax to a fully

40-- elaborated, typechecked term.

43-- elaborated, typechecked term.

41--

44--

src/Idris/IBC.hs+8−4

@@ -2030,16 +2030,18 @@ instance (Binary t) => Binary (PArg' t) where

2030 put x3

2031 put x4

2032 put x5

2033− PExp x1 x2 x3 ->

2033+ PExp x1 x2 x3 x4 ->

2034 do putWord8 1

2035 put x1

2036 put x2

2037 put x3

2038+ put x4

2038− PConstraint x1 x2 x3 ->

2039+ PConstraint x1 x2 x3 x4 ->

2039 do putWord8 2

2040 do putWord8 2

2040 put x1

2041 put x1

2041 put x2

2042 put x2

2042 put x3

2043 put x3

2044+ put x4

2043 PTacImplicit x1 x2 x3 x4 x5 ->

2045 PTacImplicit x1 x2 x3 x4 x5 ->

2044 do putWord8 3

2046 do putWord8 3

2045 put x1

2047 put x1

@@ -2059,11 +2061,13 @@ instance (Binary t) => Binary (PArg' t) where

2059 1 -> do x1 <- get

2061 1 -> do x1 <- get

2060 x2 <- get

2062 x2 <- get

2061 x3 <- get

2063 x3 <- get

2064+ x4 <- get

2062− return (PExp x1 x2 x3)

2065+ return (PExp x1 x2 x3 x4)

2063 2 -> do x1 <- get

2066 2 -> do x1 <- get

2064 x2 <- get

2067 x2 <- get

2065 x3 <- get

2068 x3 <- get

2069+ x4 <- get

2066− return (PConstraint x1 x2 x3)

2070+ return (PConstraint x1 x2 x3 x4)

2067 3 -> do x1 <- get

2071 3 -> do x1 <- get

2068 x2 <- get

2072 x2 <- get

2069 x3 <- get

2073 x3 <- get

src/Idris/PartialEval.hs+1−1

@@ -124,7 +124,7 @@ getSpecApps ist env tm = ga env (explicitNames tm) where

124 | imparg imp = (ImplicitD, tm)

125 | otherwise = (ExplicitD, (P Ref (sUN (show n ++ "arg")) Erased))

126

127− imparg (PExp _ _ _) = False

127+ imparg (PExp _ _ _ _) = False

128 imparg _ = True

129

130 buildApp env [] [] _ _ = []

src/Idris/Providers.hs+2−1

@@ -11,7 +11,8 @@ import Debug.Trace

12-- | Wrap a type provider in the type of type providers

13providerTy :: FC -> PTerm -> PTerm

14+providerTy fc tm

14−providerTy fc tm = PApp fc (PRef fc $ sUN "Provider") [PExp 0 [] tm]

15+ = PApp fc (PRef fc $ sUN "Provider") [PExp 0 [] (sMN 0 "pvarg") tm]

16ioret = sUN "prim_io_return"

17ioret = sUN "prim_io_return"

17ermod = sNS (sUN "Error") ["Providers"]

18ermod = sNS (sUN "Error") ["Providers"]