a96684a · Idris-dev · git.iko.soy

src/Idris/AbsSyntax.hs+69−34

@@ -819,9 +819,9 @@ expandParams dec ps ns infs tm = en tm

819819 | otherwise = PLam n (en t) (en s)

820820 en (PPi p n t s)

821821 | n `elem` (map fst ps ++ ns)

822− = let n' = mkShadow n in

823− PPi p n' (en t) (en (shadow n n' s))

824− | otherwise = PPi p n (en t) (en s)

822+ = let n' = mkShadow n in -- TODO THINK SHADOWING TacImp?

823+ PPi (enTacImp p) n' (en t) (en (shadow n n' s))

824+ | otherwise = PPi (enTacImp p) n (en t) (en s)

825825 en (PLet n ty v s)

826826 | n `elem` (map fst ps ++ ns)

827827 = let n' = mkShadow n in

@@ -880,6 +880,9 @@ expandParams dec ps ns infs tm = en tm

880880

881881 nseq x y = nsroot x == nsroot y

882882

883+ enTacImp (TacImp aos st scr) = TacImp aos st (en scr)

884+ enTacImp other = other

885+

883886expandParamsD :: Bool -> -- True = RHS only

884887 IState ->

885888 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl

@@ -1076,7 +1079,7 @@ addUsingConstraints syn fc t

10761079 | otherwise = doAdd cs ns t

10771080

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

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

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

10801083

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

10821085 = getcapp c ++ getConstraints sc

@@ -1088,7 +1091,7 @@ addUsingConstraints syn fc t

10881091 return (UConstraint c ns)

10891092 getcapp _ = []

10901093

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

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

10921095 getName _ = []

10931096

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

@@ -1096,13 +1099,14 @@ addUsingConstraints syn fc t

10961099

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

10981101

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

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

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

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

11011104

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

1103−implicit' syn ignore n ptm

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

1106+implicit' info syn ignore n ptm

11041107 = do i <- getIState

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

1109+ defaultArgCheck (eInfoNames info ++ M.keys (idris_implicits i)) impdata

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

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

11081112 addIBC (IBCImp n)

@@ -1110,6 +1114,23 @@ implicit' syn ignore n ptm

11101114-- i <- get

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

11121116 return tm'

1117+ where

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

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

1120+ defaultArgCheck knowns params = foldM_ notFoundInDefault knowns params

1121+

1122+ notFoundInDefault :: [Name] -> PArg -> Idris [Name]

1123+ notFoundInDefault kns (PTacImplicit _ _ n script _)

1124+ = do i <- getIState

1125+ case notFound kns (namesIn [] i script) of

1126+ Nothing -> return (n:kns)

1127+ Just name -> throwError (NoSuchVariable name)

1128+ notFoundInDefault kns p = return ((pname p):kns)

1129+

1130+ notFound :: [Name] -> [Name] -> Maybe Name

1131+ notFound kns [] = Nothing

1132+ notFound kns (SN (WhereN _ _ _) : ns) = notFound kns ns -- Known already

1133+ notFound kns (n:ns) = if elem n kns then notFound kns ns else Just n

11131134

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

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

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

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

11561177 _ -> [])

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

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

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

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

11601181 imps True (n:env) sc

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

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

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

11641185 _ -> [])

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

1166− put (PConstraint 10 l Placeholder : decls,

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

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

11681189 imps True (n:env) sc

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

@@ -1329,7 +1350,7 @@ aiFn inpat True ist fc f ds []

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

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

13311352 else Right $ PPatvar fc f

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

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

13331354 imp _ = True

13341355-- allImp [] = False

13351356 allImp xs = all imp xs

@@ -1376,27 +1397,41 @@ aiFn inpat expat ist fc f ds as

13761397 [(n,t)] -> t

13771398 _ -> Public

13781399

1379−

13801400 insertImpl :: [PArg] -> [PArg] -> [PArg]

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

1382− PExp p l tm : insertImpl ps given

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

1384− PConstraint p l tm : insertImpl ps given

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

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

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

1401+ insertImpl ps as = insImpAcc M.empty ps as

1402+

1403+ insImpAcc :: M.Map Name PTerm -- accumulated param names & arg terms

1404+ -> [PArg] -- parameters

1405+ -> [PArg] -- arguments

1406+ -> [PArg]

1407+ insImpAcc pnas (PExp p l n ty : ps) (PExp _ _ _ tm : given) =

1408+ PExp p l n tm : insImpAcc (M.insert n tm pnas) ps given

1409+ insImpAcc pnas (PConstraint p l n ty : ps) (PConstraint _ _ _ tm : given) =

1410+ PConstraint p l n tm : insImpAcc (M.insert n tm pnas) ps given

1411+ insImpAcc pnas (PConstraint p l n ty : ps) given =

1412+ let rtc = PResolveTC fc in

1413+ PConstraint p l n rtc : insImpAcc (M.insert n rtc pnas) ps given

1414+ insImpAcc pnas (PImp p _ l n ty : ps) given =

13881415 case find n given [] of

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

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

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

1392− let sc = addImpl ist sc' in

1416+ Just (tm, given') ->

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

1418+ Nothing ->

1419+ PImp p True l n Placeholder :

1420+ insImpAcc (M.insert n Placeholder pnas) ps given

1421+ insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given =

1422+ let sc = addImpl ist (substMatches (M.toList pnas) sc') in

13931423 case find n given [] of

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

1395− Nothing -> if inpat

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

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

1398− insertImpl expected [] = []

1399− insertImpl _ given = given

1424+ Just (tm, given') ->

1425+ PTacImplicit p l n sc tm :

1426+ insImpAcc (M.insert n tm pnas) ps given'

1427+ Nothing ->

1428+ if inpat

1429+ then PTacImplicit p l n sc Placeholder :

1430+ insImpAcc (M.insert n Placeholder pnas) ps given

1431+ else PTacImplicit p l n sc sc :

1432+ insImpAcc (M.insert n sc pnas) ps given

1433+ insImpAcc _ expected [] = []

1434+ insImpAcc _ _ given = given

14001435

14011436 find n [] acc = Nothing

14021437 find n (PImp _ _ _ n' t : gs) acc

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

14331468 return $ PApp fc fn args'

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

14351470 return $ PImp p m l n t'

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

1437− return $ PExp p l t'

1438− slA (PConstraint p l t)

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

1472+ return $ PExp p l n t'

1473+ slA (PConstraint p l n t)

14391474 = do t' <- sl t

1440− return $ PConstraint p l t'

1475+ return $ PConstraint p l n t'

14411476 slA (PTacImplicit p l n sc t)

14421477 = do t' <- sl t

14431478 return $ PTacImplicit p l n sc t'

src/Idris/AbsSyntaxTree.hs+42−15

@@ -36,6 +36,19 @@ import Debug.Trace

3636

3737import Text.PrettyPrint.Annotated.Leijen

3838

39+-- Data to pass to recursively called elaborators; e.g. for where blocks,

40+-- paramaterised declarations, etc.

41+

42+data ElabInfo = EInfo { params :: [(Name, PTerm)],

43+ inblock :: Ctxt [Name], -- names in the block, and their params

44+ liftname :: Name -> Name,

45+ namespace :: Maybe [String] }

46+

47+toplevel = EInfo [] emptyContext id Nothing

48+

49+eInfoNames :: ElabInfo -> [Name]

50+eInfoNames info = map fst (params info) ++ M.keys (inblock info)

51+

3952data IOption = IOption { opt_logLevel :: Int,

4053 opt_typecase :: Bool,

4154 opt_typeintype :: Bool,

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

767780 pname :: Name, getTm :: t }

768781 | PExp { priority :: Int,

769782 argopts :: [ArgOpt],

783+ pname :: Name,

770784 getTm :: t }

771785 | PConstraint { priority :: Int,

772786 argopts :: [ArgOpt],

787+ pname :: Name,

773788 getTm :: t }

774789 | PTacImplicit { priority :: Int,

775790 argopts :: [ArgOpt],

@@ -786,8 +801,8 @@ lazyarg tm = Lazy `elem` argopts tm

786801

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

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

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

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

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

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

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

792807

793808{-!

@@ -796,8 +811,8 @@ deriving instance NFData PArg'

796811!-}

797812

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

799−pexp t = PExp 1 [] t

800−pconst t = PConstraint 1 [] t

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

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

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

802817

803818type PArg = PArg' PTerm

@@ -1255,8 +1270,8 @@ pprintPTerm impl bnd docArgs = prettySe 10 bnd

12551270 prettySe p bnd _ = text "test"

12561271

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

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

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

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

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

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

12611276

12621277 prettyArgSe bnd arg = prettySe 0 bnd arg

@@ -1388,12 +1403,12 @@ getImps (_ : xs) = getImps xs

13881403

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

13901405getExps [] = []

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

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

13921407getExps (_ : xs) = getExps xs

13931408

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

13951410getConsts [] = []

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

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

13971412getConsts (_ : xs) = getConsts xs

13981413

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

@@ -1481,7 +1496,7 @@ getPArity _ = 0

14811496

14821497allNamesIn :: PTerm -> [Name]

14831498allNamesIn tm = nub $ ni [] tm

1484− where

1499+ where -- TODO THINK added niTacImp, but is it right?

14851500 ni env (PRef _ n)

14861501 | not (n `elem` env) = [n]

14871502 ni env (PPatvar _ n) = [n]

@@ -1489,7 +1504,7 @@ allNamesIn tm = nub $ ni [] tm

14891504 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

14901505 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)

14911506 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

1492− ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc

1507+ ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc

14931508 ni env (PHidden tm) = ni env tm

14941509 ni env (PEq _ l r) = ni env l ++ ni env r

14951510 ni env (PRewrite _ l r _) = ni env l ++ ni env r

@@ -1503,16 +1518,19 @@ allNamesIn tm = nub $ ni [] tm

15031518 ni env (PNoImplicits tm) = ni env tm

15041519 ni env _ = []

15051520

1521+ niTacImp env (TacImp _ _ scr) = ni env scr

1522+ niTacImp _ _ = []

1523+

15061524-- Return all names defined in binders in the given term

15071525boundNamesIn :: PTerm -> [Name]

15081526boundNamesIn tm = nub $ ni tm

1509− where

1527+ where -- TODO THINK Added niTacImp, but is it right?

15101528 ni (PApp _ f as) = ni f ++ concatMap (ni) (map getTm as)

15111529 ni (PAppBind _ f as) = ni f ++ concatMap (ni) (map getTm as)

15121530 ni (PCase _ c os) = ni c ++ concatMap (ni) (map snd os)

15131531 ni (PLam n ty sc) = n : (ni ty ++ ni sc)

15141532 ni (PLet n ty val sc) = n : (ni ty ++ ni val ++ ni sc)

1515− ni (PPi _ n ty sc) = n : (ni ty ++ ni sc)

1533+ ni (PPi p n ty sc) = niTacImp p ++ (n : (ni ty ++ ni sc))

15161534 ni (PEq _ l r) = ni l ++ ni r

15171535 ni (PRewrite _ l r _) = ni l ++ ni r

15181536 ni (PTyped l r) = ni l ++ ni r

@@ -1526,6 +1544,9 @@ boundNamesIn tm = nub $ ni tm

15261544 ni (PNoImplicits tm) = ni tm

15271545 ni _ = []

15281546

1547+ niTacImp (TacImp _ _ scr) = ni scr

1548+ niTacImp _ = []

1549+

15291550-- Return names which are free in the given term.

15301551namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]

15311552namesIn uvars ist tm = nub $ ni [] tm

@@ -1539,7 +1560,7 @@ namesIn uvars ist tm = nub $ ni [] tm

15391560 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

15401561 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)

15411562 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

1542− ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc

1563+ ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc

15431564 ni env (PEq _ l r) = ni env l ++ ni env r

15441565 ni env (PRewrite _ l r _) = ni env l ++ ni env r

15451566 ni env (PTyped l r) = ni env l ++ ni env r

@@ -1553,11 +1574,14 @@ namesIn uvars ist tm = nub $ ni [] tm

15531574 ni env (PNoImplicits tm) = ni env tm

15541575 ni env _ = []

15551576

1577+ niTacImp env (TacImp _ _ scr) = ni env scr

1578+ niTacImp _ _ = []

1579+

15561580-- Return which of the given names are used in the given term.

15571581

15581582usedNamesIn :: [Name] -> IState -> PTerm -> [Name]

15591583usedNamesIn vars ist tm = nub $ ni [] tm

1560− where

1584+ where -- TODO THINK added niTacImp, but is it right?

15611585 ni env (PRef _ n)

15621586 | n `elem` vars && not (n `elem` env)

15631587 = case lookupTy n (tt_ctxt ist) of

@@ -1567,7 +1591,7 @@ usedNamesIn vars ist tm = nub $ ni [] tm

15671591 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

15681592 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)

15691593 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

1570− ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc

1594+ ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc

15711595 ni env (PEq _ l r) = ni env l ++ ni env r

15721596 ni env (PRewrite _ l r _) = ni env l ++ ni env r

15731597 ni env (PTyped l r) = ni env l ++ ni env r

@@ -1581,3 +1605,6 @@ usedNamesIn vars ist tm = nub $ ni [] tm

15811605 ni env (PNoImplicits tm) = ni env tm

15821606 ni env _ = []

15831607

1608+ niTacImp env (TacImp _ _ scr) = ni env scr

1609+ niTacImp _ _ = []

1610+

src/Idris/Coverage.hs+3−2

@@ -72,8 +72,9 @@ genClauses fc n xs given

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

7373 -- suggests)

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

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

76− _ -> repeat (pexp Placeholder)

75+ (p : _) ->

76+ p ++ repeat (PExp 0 [] (sMN 0 "gcarg") Placeholder)

77+ _ -> repeat (pexp Placeholder)

7778 let tryclauses = mkClauses parg all_args

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

7980 logLvl 1 $ 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+50−31

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

8282

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

8484 ty' <- addUsingConstraints syn fc ty'

85− ty' <- implicit syn n ty'

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

8686

8787 let ty = addImpl i ty'

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

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

204204 checkUndefined fc n

205205 ctxt <- getContext

206206 i <- getIState

207− t_in <- implicit syn n t_in

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

208+ t_in <- implicit info syn n t_in

208209 let t = addImpl i t_in

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

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

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

222223 undef <- isUndefined fc n

223224 ctxt <- getContext

224225 i <- getIState

225− t_in <- implicit syn n t_in

226+ t_in <- implicit info syn n t_in

226227 let t = addImpl i t_in

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

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

@@ -238,7 +239,8 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

238239 logLvl 2 $ "---> " ++ show cty

239240 -- temporary, to check cons

240241 when undef $ updateContext (addTyDecl n (TCon 0 0) cty)

241− cons <- mapM (elabCon info syn n codata) dcons

242+ let cnameinfo = cinfo info (map cname dcons)

243+ cons <- mapM (elabCon cnameinfo syn n codata) dcons

242244 ttag <- getName

243245 i <- getIState

244246 let as = map (const Nothing) (getArgTys cty)

@@ -321,6 +323,21 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

321323 | otherwise = count n ts

322324 mParam args (_ : rest) = Nothing : mParam args rest

323325

326+ cname (_, _, n, _, _, _) = n

327+

328+ -- Abuse of ElabInfo.

329+ -- TODO Contemplate whether the ElabInfo type needs modification.

330+ cinfo :: ElabInfo -> [Name] -> ElabInfo

331+ cinfo info ds

332+ = let newps = params info

333+ dsParams = map (\n -> (n, [])) ds

334+ newb = addAlist dsParams (inblock info)

335+ l = liftname info in

336+ info { params = newps,

337+ inblock = newb,

338+ liftname = id -- Is this appropriate?

339+ }

340+

324341type EliminatorState = StateT (Map.Map String Int) Idris

325342

326343-- TODO: Use uniqueName for generating names, rewrite everything to use idris_implicits instead of manual splitting, generally just rewrite

@@ -730,7 +747,8 @@ elabRecord :: ElabInfo -> SyntaxInfo -> Docstring -> FC -> Name ->

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

731748elabRecord info syn doc fc tyn ty cdoc cn cty

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

733− cty' <- implicit syn cn cty

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

751+ cty' <- implicit info syn cn cty

734752 i <- getIState

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

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

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

752770 where

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

754772

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

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

756774 isNonImp _ = Nothing

757775

758776 tryElabDecl info (fn, ty, val)

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

841859 = do checkUndefined fc n

842860 ctxt <- getContext

843861 i <- getIState

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

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

845863 let t = addImpl i t_in

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

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

@@ -875,7 +893,7 @@ elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)

875893

876894 mkLazy (PPi pl n ty sc)

877895 = let ty' = if getTyName ty

878− then PApp fc (PRef fc (sUN "Lazy'"))

896+ then PApp fc (PRef fc (sUN "Lazy'"))

879897 [pexp (PRef fc (sUN "LazyCodata")),

880898 pexp ty]

881899 else ty in

@@ -1292,7 +1310,7 @@ checkPossible info fc tcgen fname lhs_in

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

12931311 _ -> False

12941312

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

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

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

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

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

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

14231441 -- Elaborate where block

14241442 ist <- getIState

14251443 windex <- getName

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

14271444 let decls = nub (concatMap declared whereblock)

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

14291446 let newargs = pvars ist lhs_tm

1447+ let winfo = pinfo info newargs defs windex

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

14311449

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

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

14351453 let (wbefore, wafter) = sepBlocks wb

14361454

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

1438− mapM_ (elabDecl' EAll info) wbefore

1456+ mapM_ (elabDecl' EAll winfo) wbefore

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

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

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

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

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

14511469 setNextName

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

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

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

14541472 errAt "right hand side of " fname

14551473 (erun fc $ psolve lhs_tm)

14561474 hs <- get_holes

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

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

14791497 -- from the where block

14801498

1481− mapM_ (elabDecl' EAll info) wafter

1482− mapM_ (elabCaseBlock info opts) is

1499+ mapM_ (elabDecl' EAll winfo) wafter

1500+ mapM_ (elabCaseBlock winfo opts) is

14831501

14841502 ctxt <- getContext

14851503 logLvl 5 $ "Rechecking"

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

15091527 addErrRev (crhs, clhs)

15101528 return $ (Right (clhs, crhs), lhs)

15111529 where

1530+ pinfo :: ElabInfo -> [(Name, PTerm)] -> [Name] -> Int -> ElabInfo

1531+ pinfo info ns ds i

1532+ = let newps = params info ++ ns

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

1534+ newb = addAlist dsParams (inblock info)

1535+ l = liftname info in

1536+ info { params = newps,

1537+ inblock = newb,

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

1539+ -- Nothing -> n

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

1541+ }

1542+

15121543 mkLHSapp t@(PRef _ _) = trace ("APP " ++ show t) $ PApp fc t []

15131544 mkLHSapp t = t

15141545

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

15311562 (b : bf, af)

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

15331564

1534− pinfo ns ps i

1535− = let ds = concatMap declared ps

1536− newps = params info ++ ns

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

1538− newb = addAlist dsParams (inblock info)

1539− l = liftname info in

1540− info { params = newps,

1541− inblock = newb,

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

1543− -- Nothing -> n

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

1545− }

1546−

15471565

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

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

@@ -1808,7 +1826,7 @@ elabClass info syn doc fc constraints tn ps ds

18081826

18091827 getMName (PTy _ _ _ _ _ n _) = nsroot n

18101828 tdecl allmeths (PTy doc _ syn _ o n t)

1811− = do t' <- implicit' syn allmeths n t

1829+ = do t' <- implicit' info syn allmeths n t

18121830 logLvl 5 $ "Method " ++ show n ++ " : " ++ showTmImpls t'

18131831 return ( (n, (toExp (map fst ps) Exp t')),

18141832 (n, (doc, o, (toExp (map fst ps) Imp t'))),

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

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

20132031 elabFindOverlapping i ci iname syn t

20142032 = do ty' <- addUsingConstraints syn fc t

2015− ty' <- implicit syn iname ty'

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

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

20162035 let ty = addImpl i ty'

20172036 ctxt <- getContext

20182037 ((tyT, _, _), _) <-

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

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

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

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

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

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

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

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

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

20562075 methArgs i _ = []

20572076

20582077 papp fc f [] = f

src/Idris/ElabTerm.hs+2−11

@@ -3,6 +3,7 @@

33module Idris.ElabTerm where

44

55import Idris.AbsSyntax

6+import Idris.AbsSyntaxTree

67import Idris.DSL

78import Idris.Delaborate

89import Idris.Error

@@ -27,16 +28,6 @@ import qualified Data.Text as T

2728

2829import Debug.Trace

2930

30−-- Data to pass to recursively called elaborators; e.g. for where blocks,

31−-- paramaterised declarations, etc.

32−

33−data ElabInfo = EInfo { params :: [(Name, PTerm)],

34− inblock :: Ctxt [Name], -- names in the block, and their params

35− liftname :: Name -> Name,

36− namespace :: Maybe [String] }

37−

38−toplevel = EInfo [] emptyContext id Nothing

39−

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

4132-- elaborated, typechecked term.

4233--

@@ -697,7 +688,7 @@ elab ist info pattern opts fn tm

697688 where

698689 mkDelay (PAlternative b xs) = PAlternative b (map mkDelay xs)

699690 mkDelay t = let fc = fileFC "Delay" in

700− addImpl ist (PApp fc (PRef fc (sUN "Delay"))

691+ addImpl ist (PApp fc (PRef fc (sUN "Delay"))

701692 [pexp t])

702693

703694 insertCoerce ina t =

src/Idris/IBC.hs+9−5

@@ -29,7 +29,7 @@ import Codec.Compression.Zlib (compress)

2929import Util.Zlib (decompressEither)

3030

3131ibcVersion :: Word8

32−ibcVersion = 65

32+ibcVersion = 66

3333

3434data IBCFile = IBCFile { ver :: Word8,

3535 sourcefile :: FilePath,

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

20372037 put x3

20382038 put x4

20392039 put x5

2040− PExp x1 x2 x3 ->

2040+ PExp x1 x2 x3 x4 ->

20412041 do putWord8 1

20422042 put x1

20432043 put x2

20442044 put x3

2045− PConstraint x1 x2 x3 ->

2045+ put x4

2046+ PConstraint x1 x2 x3 x4 ->

20462047 do putWord8 2

20472048 put x1

20482049 put x2

20492050 put x3

2051+ put x4

20502052 PTacImplicit x1 x2 x3 x4 x5 ->

20512053 do putWord8 3

20522054 put x1

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

20662068 1 -> do x1 <- get

20672069 x2 <- get

20682070 x3 <- get

2069− return (PExp x1 x2 x3)

2071+ x4 <- get

2072+ return (PExp x1 x2 x3 x4)

20702073 2 -> do x1 <- get

20712074 x2 <- get

20722075 x3 <- get

2073− return (PConstraint x1 x2 x3)

2076+ x4 <- get

2077+ return (PConstraint x1 x2 x3 x4)

20742078 3 -> do x1 <- get

20752079 x2 <- get

20762080 x3 <- get

src/Idris/ParseExpr.hs+19−8

@@ -150,15 +150,23 @@ extension syn (Rule ssym ptm _)

150150 update ns (PRef fc n) = case lookup n ns of

151151 Just (SynTm t) -> t

152152 _ -> PRef fc n

153− update ns (PLam n ty sc) = PLam (updateB ns n) (update ns ty) (update (dropn n ns) sc)

154− update ns (PPi p n ty sc) = PPi p (updateB ns n) (update ns ty) (update (dropn n ns) sc)

155− update ns (PLet n ty val sc) = PLet (updateB ns n) (update ns ty) (update ns val)

156− (update (dropn n ns) sc)

157− update ns (PApp fc t args) = PApp fc (update ns t) (map (fmap (update ns)) args)

158− update ns (PAppBind fc t args) = PAppBind fc (update ns t) (map (fmap (update ns)) args)

159− update ns (PCase fc c opts) = PCase fc (update ns c) (map (pmap (update ns)) opts)

153+ update ns (PLam n ty sc)

154+ = PLam (updateB ns n) (update ns ty) (update (dropn n ns) sc)

155+ update ns (PPi p n ty sc)

156+ = PPi (updTacImp ns p) (updateB ns n)

157+ (update ns ty) (update (dropn n ns) sc)

158+ update ns (PLet n ty val sc)

159+ = PLet (updateB ns n) (update ns ty)

160+ (update ns val) (update (dropn n ns) sc)

161+ update ns (PApp fc t args)

162+ = PApp fc (update ns t) (map (fmap (update ns)) args)

163+ update ns (PAppBind fc t args)

164+ = PAppBind fc (update ns t) (map (fmap (update ns)) args)

165+ update ns (PCase fc c opts)

166+ = PCase fc (update ns c) (map (pmap (update ns)) opts)

160167 update ns (PPair fc p l r) = PPair fc p (update ns l) (update ns r)

161− update ns (PDPair fc p l t r) = PDPair fc p (update ns l) (update ns t) (update ns r)

168+ update ns (PDPair fc p l t r)

169+ = PDPair fc p (update ns l) (update ns t) (update ns r)

162170 update ns (PAlternative a as) = PAlternative a (map (update ns) as)

163171 update ns (PHidden t) = PHidden (update ns t)

164172 update ns (PDoBlock ds) = PDoBlock $ upd ns ds

@@ -176,6 +184,9 @@ extension syn (Rule ssym ptm _)

176184 update ns (PGoal fc r n sc) = PGoal fc (update ns r) n (update ns sc)

177185 update ns t = t

178186

187+ updTacImp ns (TacImp o st scr) = TacImp o st (update ns scr)

188+ updTacImp _ x = x

189+

179190{- | Parses a (normal) built-in expression

180191@

181192InternalExpr ::=

src/Idris/Parser.hs+2−2

@@ -18,13 +18,13 @@ import qualified Text.Parser.Token.Highlight as Hi

1818

1919import Text.PrettyPrint.ANSI.Leijen (Doc, plain)

2020

21−import Idris.AbsSyntax

21+import Idris.AbsSyntax hiding (namespace, params)

2222import Idris.DSL

2323import Idris.Imports

2424import Idris.Delaborate

2525import Idris.Error

2626import Idris.ElabDecls

27−import Idris.ElabTerm hiding (namespace, params)

27+import Idris.ElabTerm

2828import Idris.Coverage

2929import Idris.IBC

3030import Idris.Unlit

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

test/proof005/DefaultArgSubstitutionSuccess.idrnew file+44

@@ -0,0 +1,44 @@

1+module DefaultArgSubstitutionSuccess

2+

3+DecProofType : {a:Type} -> Dec a -> Type

4+DecProofType {a} (Yes _) = a

5+DecProofType {a} (No _) = a -> _|_

6+

7+decProof : {a:Type} -> (dec : Dec a) -> DecProofType dec

8+decProof (Yes x) = x

9+decProof (No x) = x

10+

11+DecType : {a:Type} -> Dec a -> Type

12+DecType {a} _ = a

13+

14+

15+argsAreSame : (n:Nat) -> (m:Nat)

16+ -> { default (decProof (decEq m n)) same : (m=n) } -> ()

17+argsAreSame _ _ = ()

18+

19+

20+argsAreDiff : (n:Nat) -> (m:Nat)

21+ -> { default (decProof (decEq m n)) same : (m=n) -> _|_ } -> ()

22+argsAreDiff _ _ = ()

23+

24+

25+data SameNats : Type where

26+ same : (n:Nat) -> (m:Nat) ->

27+ { default (decProof (decEq m n)) same : (m=n) } -> SameNats

28+

29+data DiffNats : Type where

30+ diff : (n:Nat) -> (m:Nat) ->

31+ { default (decProof (decEq m n)) same : (m=n) -> _|_ } -> DiffNats

32+

33+

34+zArgsAreSame : ()

35+zArgsAreSame = argsAreSame Z Z

36+

37+zszArgsAreDiff : ()

38+zszArgsAreDiff = argsAreDiff Z (S Z)

39+

40+sameNatZs : SameNats

41+sameNatZs = same Z Z

42+

43+diffNatsZSZ : DiffNats

44+diffNatsZSZ = diff Z (S Z)

test/proof005/expectednew file

No changes to the content.

test/proof005/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+idris --check $@ DefaultArgSubstitutionSuccess.idr

3+rm -f *.ibc

test/proof006/DefaultArgSubstitutionSyntax.idrnew file+49

@@ -0,0 +1,49 @@

1+module DefaultArgSubstitutionSyntax

2+

3+DecProofType : {a:Type} -> Dec a -> Type

4+DecProofType {a} (Yes _) = a

5+DecProofType {a} (No _) = a -> _|_

6+

7+decProof : {a:Type} -> (dec : Dec a) -> DecProofType dec

8+decProof (Yes x) = x

9+decProof (No x) = x

10+

11+DecType : {a:Type} -> Dec a -> Type

12+DecType {a} _ = a

13+

14+

15+syntax "{{" [prfname] ":" "accept" [dec] "}}" "->" [ret]

16+ = { default (decProof dec) prfname : DecType dec } -> ret

17+

18+syntax "{{" [prfname] ":" "reject" [dec] "}}" "->" [ret]

19+ = { default (decProof dec) prfname : DecType dec -> _|_ } -> ret

20+

21+

22+argsAreSame : (n:Nat) -> (m:Nat)

23+ -> {{ same : accept (decEq n m) }} -> ()

24+argsAreSame _ _ = ()

25+

26+

27+argsAreDiff : (n:Nat) -> (m:Nat)

28+ -> {{ diff : reject (decEq m n) }} -> ()

29+argsAreDiff _ _ = ()

30+

31+

32+data SameNats : Type where

33+ same : (n:Nat) -> (m:Nat) -> {{ same : accept (decEq m n) }} -> SameNats

34+

35+data DiffNats : Type where

36+ diff : (n:Nat) -> (m:Nat) -> {{ diff : reject (decEq m n) }} -> DiffNats

37+

38+

39+zArgsAreSame : ()

40+zArgsAreSame = argsAreSame Z Z

41+

42+zszArgsAreDiff : ()

43+zszArgsAreDiff = argsAreDiff Z (S Z)

44+

45+sameNatZs : SameNats

46+sameNatZs = same Z Z

47+

48+diffNatsZSZ : DiffNats

49+diffNatsZSZ = diff Z (S Z)

test/proof006/expectednew file

No changes to the content.

test/proof006/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+idris --check $@ DefaultArgSubstitutionSyntax.idr

3+rm -f *.ibc

test/proof007/DefaultArgUnknownName.idrnew file+4

@@ -0,0 +1,4 @@

1+module DefaultArgUnknownName

2+

3+funWithBadDefArg : { default sadgjhsag arg : () } -> ()

4+funWithBadDefArg : _ = ()

test/proof007/expectednew file+1

@@ -0,0 +1 @@

1+No such variable sadgjhsag

test/proof007/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+idris --check $@ DefaultArgUnknownName.idr

3+rm -f *.ibc