d3eb486 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

First attempt now at substitution to default args

commitd3eb486840bc8220e43c77fda2bb0aae9f65a6e8 authorTimo Petteri Sinnemäki <timo.sinnemaki@helsinki.fi> dateWed 2 Apr 2014, 23:54 (13 years ago) parentb1028f0

10 files changed+138−81

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+70−30 src/Idris/AbsSyntaxTree.hs+10−8 src/Idris/Coverage.hs+2−2 src/Idris/DeepSeq.hs+4−4 src/Idris/Delaborate.hs+3−3 src/Idris/ElabDecls.hs+35−28 src/Idris/ElabTerm.hs+3 src/Idris/IBC.hs+8−4 src/Idris/PartialEval.hs+1−1 src/Idris/Providers.hs+2−1

src/Idris/AbsSyntax.hs+70−30

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

12051205 | otherwise = doAdd cs ns t

12061206

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

12091209

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

12111211 = getcapp c ++ getConstraints sc

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

12171217 return (UConstraint c ns)

12181218 getcapp _ = []

12191219

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

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

12211221 getName _ = []

12221222

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

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

12251225

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

12271227

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

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

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

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

12301230

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

1232−implicit' syn ignore n ptm

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

1232+implicit' info syn ignore n ptm

12331233 = do i <- getIState

12341234 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

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

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

12371239 addIBC (IBCImp n)

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

12391241-- i <- get

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

12411243 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

12421262

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

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

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

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

12851305 _ -> [])

12861306 (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,

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

12891309 imps True (n:env) sc

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

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

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

12931313 _ -> [])

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

1295− put (PConstraint 10 l Placeholder : decls,

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

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

12971317 imps True (n:env) sc

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

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

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

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

14601480 else Right $ PPatvar fc f

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

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

14621482 imp _ = True

14631483-- allImp [] = False

14641484 allImp xs = all imp xs

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

15051525 [(n,t)] -> t

15061526 _ -> Public

15071527

1508−

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

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

1511− PExp p l tm : insertImpl ps given

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

1513− PConstraint p l tm : insertImpl ps given

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

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

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

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

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]

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

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

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

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

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

1546+ let rtc = PResolveTC fc in

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

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

15171549 case find n given [] of

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

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

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

1521− let sc = addImpl ist sc' in

1550+ Just (tm, given') ->

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

1552+ Nothing ->

1553+ PImp p True l n Placeholder :

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

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

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

15221557 case find n given [] of

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

1524− Nothing -> if inpat

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

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

1558+ Just (tm, given') ->

1559+ PTacImplicit p l n sc tm :

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

1561+ Nothing ->

1562+ if inpat

1563+ then PTacImplicit p l n sc Placeholder :

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

1565+ else PTacImplicit p l n sc sc :

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

15271567 insertImpl expected [] = []

15281568 insertImpl _ given = given

15291569

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

15621602 return $ PApp fc fn args'

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

15641604 return $ PImp p m l n t'

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

1566− return $ PExp p l t'

1567− slA (PConstraint p l t)

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

1606+ return $ PExp p l n t'

1607+ slA (PConstraint p l n t)

15681608 = do t' <- sl t

1569− return $ PConstraint p l t'

1609+ return $ PConstraint p l n t'

15701610 slA (PTacImplicit p l n sc t)

15711611 = do t' <- sl t

15721612 return $ PTacImplicit p l n sc t'

src/Idris/AbsSyntaxTree.hs+10−8

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

771771 pname :: Name, getTm :: t }

772772 | PExp { priority :: Int,

773773 argopts :: [ArgOpt],

774+ pname :: Name,

774775 getTm :: t }

775776 | PConstraint { priority :: Int,

776777 argopts :: [ArgOpt],

778+ pname :: Name,

777779 getTm :: t }

778780 | PTacImplicit { priority :: Int,

779781 argopts :: [ArgOpt],

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

790792

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

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

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

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

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

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

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

796798

797799{-!

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

800802!-}

801803

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

803−pexp t = PExp 1 [] t

804−pconst t = PConstraint 1 [] t

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

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

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

806808

807809type PArg = PArg' PTerm

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

12591261 prettySe p bnd _ = text "test"

12601262

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

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

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

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

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

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

12651267

12661268 prettyArgSe bnd arg = prettySe 0 bnd arg

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

13891391

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

13911393getExps [] = []

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

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

13931395getExps (_ : xs) = getExps xs

13941396

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

13961398getConsts [] = []

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

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

13981400getConsts (_ : xs) = getConsts xs

13991401

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

src/Idris/Coverage.hs+2−2

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

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

5757 -- suggests)

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

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

60− _ -> repeat (pexp Placeholder)

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

60+ _ -> repeat (pexp Placeholder)

6161 let tryclauses = mkClauses parg all_args

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

6363 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

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

277277 rnf (PImp x1 x2 x3 x4 x5)

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

279− rnf (PExp x1 x2 x3)

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

281− rnf (PConstraint x1 x2 x3)

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

279+ rnf (PExp x1 x2 x3 x4)

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

281+ rnf (PConstraint x1 x2 x3 x4)

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

283283 rnf (PTacImplicit x1 x2 x3 x4 x5)

284284 = rnf x1 `seq`

285285 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

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

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

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

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

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

6464 = 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

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

122122

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

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

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

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

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

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

127127

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

8080

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

8282 ty' <- addUsingConstraints syn fc ty'

83− ty' <- implicit syn n ty'

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

8484

8585 let ty = addImpl i ty'

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

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

202202 checkUndefined fc n

203203 ctxt <- getContext

204204 i <- getIState

205− t_in <- implicit syn n t_in

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

206+ t_in <- implicit info syn n t_in

206207 let t = addImpl i t_in

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

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

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

220221 undef <- isUndefined fc n

221222 ctxt <- getContext

222223 i <- getIState

223− t_in <- implicit syn n t_in

224+ t_in <- implicit info syn n t_in

224225 let t = addImpl i t_in

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

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

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

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

729730elabRecord info syn doc fc tyn ty cdoc cn cty

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

731− cty' <- implicit syn cn cty

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

733+ cty' <- implicit info syn cn cty

732734 i <- getIState

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

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

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

750752 where

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

752754

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

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

754756 isNonImp _ = Nothing

755757

756758 tryElabDecl info (fn, ty, val)

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

839841 = do checkUndefined fc n

840842 ctxt <- getContext

841843 i <- getIState

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

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

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

843846 let t = addImpl i t_in

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

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

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

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

12891292 _ -> False

12901293

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

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

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

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

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

14161419 -- Elaborate where block

14171420 ist <- getIState

14181421 windex <- getName

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

14201422 let decls = nub (concatMap declared whereblock)

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

14221424 let newargs = pvars ist lhs_tm

1425+ let winfo = pinfo info newargs defs windex

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

14241427

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

14281431 let (wbefore, wafter) = sepBlocks wb

14291432

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

1431− mapM_ (elabDecl' EAll info) wbefore

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.

1438+ mapM_ (elabDecl' EAll winfo) wbefore

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

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

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

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

14441451 setNextName

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

14471454 errAt "right hand side of " fname

14481455 (erun fc $ psolve lhs_tm)

14491456 hs <- get_holes

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

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

14721479 -- from the where block

14731480

1474− mapM_ (elabDecl' EAll info) wafter

1475− mapM_ (elabCaseBlock info opts) is

1481+ mapM_ (elabDecl' EAll winfo) wafter

1482+ mapM_ (elabCaseBlock winfo opts) is

14761483

14771484 ctxt <- getContext

14781485 logLvl 5 $ "Rechecking"

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

15241531 (b : bf, af)

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

15261533

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−

15401534

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

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

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

20062000 elabFindOverlapping i ci iname syn t

20072001 = do ty' <- addUsingConstraints syn fc t

2008− ty' <- implicit syn iname ty'

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

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

20092004 let ty = addImpl i ty'

20102005 ctxt <- getContext

20112006 ((tyT, _, _), _) <-

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

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

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

20452040 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

20472042 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

20492044 methArgs i _ = []

20502045

20512046 papp fc f [] = f

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

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

21672162pvars ist _ = []

21682163

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+

21692176data ElabWhat = ETypes | EDefns | EAll

21702177 deriving (Show, Eq)

21712178

src/Idris/ElabTerm.hs+3

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

3636

3737toplevel = EInfo [] emptyContext id Nothing

3838

39+eInfoNames :: ElabInfo -> [Name]

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

41+

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

4043-- elaborated, typechecked term.

4144--

src/Idris/IBC.hs+8−4

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

20302030 put x3

20312031 put x4

20322032 put x5

2033− PExp x1 x2 x3 ->

2033+ PExp x1 x2 x3 x4 ->

20342034 do putWord8 1

20352035 put x1

20362036 put x2

20372037 put x3

2038− PConstraint x1 x2 x3 ->

2038+ put x4

2039+ PConstraint x1 x2 x3 x4 ->

20392040 do putWord8 2

20402041 put x1

20412042 put x2

20422043 put x3

2044+ put x4

20432045 PTacImplicit x1 x2 x3 x4 x5 ->

20442046 do putWord8 3

20452047 put x1

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

20592061 1 -> do x1 <- get

20602062 x2 <- get

20612063 x3 <- get

2062− return (PExp x1 x2 x3)

2064+ x4 <- get

2065+ return (PExp x1 x2 x3 x4)

20632066 2 -> do x1 <- get

20642067 x2 <- get

20652068 x3 <- get

2066− return (PConstraint x1 x2 x3)

2069+ x4 <- get

2070+ return (PConstraint x1 x2 x3 x4)

20672071 3 -> do x1 <- get

20682072 x2 <- get

20692073 x3 <- get

src/Idris/PartialEval.hs+1−1

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

124124 | imparg imp = (ImplicitD, tm)

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

126126

127− imparg (PExp _ _ _) = False

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

128128 imparg _ = True

129129

130130 buildApp env [] [] _ _ = []

src/Idris/Providers.hs+2−1

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

1111

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

1313providerTy :: FC -> PTerm -> PTerm

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

14+providerTy fc tm

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

1516

1617ioret = sUN "prim_io_return"

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