git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1031 from tpsinnem/default-arg-subst
a96684aEdwin Brady
src/Idris/AbsSyntax.hs+69−34
compare with master
unifiedsplit
@@ -819,9 +819,9 @@ expandParams dec ps ns infs tm = en tm
819 | otherwise = PLam n (en t) (en s)
819 | otherwise = PLam n (en t) (en s)
820 en (PPi p n t s)
820 en (PPi p n t s)
821 | n `elem` (map fst ps ++ ns)
821 | n `elem` (map fst ps ++ ns)
822− = let n' = mkShadow n in
822+ = let n' = mkShadow n in -- TODO THINK SHADOWING TacImp?
823− PPi p n' (en t) (en (shadow n n' s))
823+ PPi (enTacImp p) n' (en t) (en (shadow n n' s))
824− | otherwise = PPi p n (en t) (en s)
824+ | otherwise = PPi (enTacImp p) n (en t) (en s)
825 en (PLet n ty v s)
825 en (PLet n ty v s)
826 | n `elem` (map fst ps ++ ns)
826 | n `elem` (map fst ps ++ ns)
827 = let n' = mkShadow n in
827 = let n' = mkShadow n in
@@ -880,6 +880,9 @@ expandParams dec ps ns infs tm = en tm
880
880
881 nseq x y = nsroot x == nsroot y
881 nseq x y = nsroot x == nsroot y
882
882
883+ enTacImp (TacImp aos st scr) = TacImp aos st (en scr)
884+ enTacImp other = other
885+
883expandParamsD :: Bool -> -- True = RHS only
886expandParamsD :: Bool -> -- True = RHS only
884 IState ->
887 IState ->
885 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
888 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
@@ -1076,7 +1079,7 @@ addUsingConstraints syn fc t
1076 | otherwise = doAdd cs ns t
1079 | otherwise = doAdd cs ns t
1077
1080
1078 mkConst c args = PApp fc (PRef fc c)
1081 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)
1080
1083
1081 getConstraints (PPi (Constraint _ _) _ c sc)
1084 getConstraints (PPi (Constraint _ _) _ c sc)
1082 = getcapp c ++ getConstraints sc
1085 = getcapp c ++ getConstraints sc
@@ -1088,7 +1091,7 @@ addUsingConstraints syn fc t
1088 return (UConstraint c ns)
1091 return (UConstraint c ns)
1089 getcapp _ = []
1092 getcapp _ = []
1090
1093
1091− getName (PExp _ _ (PRef _ n)) = return n
1094+ getName (PExp _ _ _ (PRef _ n)) = return n
1092 getName _ = []
1095 getName _ = []
1093
1096
1094-- Add implicit Pi bindings for any names in the term which appear in an
1097-- Add implicit Pi bindings for any names in the term which appear in an
@@ -1096,13 +1099,14 @@ addUsingConstraints syn fc t
1096
1099
1097-- This has become a right mess already. Better redo it some time...
1100-- This has become a right mess already. Better redo it some time...
1098
1101
1099−implicit :: SyntaxInfo -> Name -> PTerm -> Idris PTerm
1102+implicit :: ElabInfo -> SyntaxInfo -> Name -> PTerm -> Idris PTerm
1100−implicit syn n ptm = implicit' syn [] n ptm
1103+implicit info syn n ptm = implicit' info syn [] n ptm
1101
1104
1102−implicit' :: SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
1105+implicit' :: ElabInfo -> SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
1103−implicit' syn ignore n ptm
1106+implicit' info syn ignore n ptm
1104 = do i <- getIState
1107 = do i <- getIState
1105 let (tm', impdata) = implicitise syn ignore i ptm
1108 let (tm', impdata) = implicitise syn ignore i ptm
1109+ defaultArgCheck (eInfoNames info ++ M.keys (idris_implicits i)) impdata
1106-- let (tm'', spos) = findStatics i tm'
1110-- let (tm'', spos) = findStatics i tm'
1107 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
1111 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
1108 addIBC (IBCImp n)
1112 addIBC (IBCImp n)
@@ -1110,6 +1114,23 @@ implicit' syn ignore n ptm
1110-- i <- get
1114-- i <- get
1111-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }
1115-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }
1112 return tm'
1116 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
1113
1134
1114implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
1135implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
1115implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1136implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
@@ -1155,7 +1176,7 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1155 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1176 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1156 _ -> [])
1177 _ -> [])
1157 (decls, ns) <- get -- ignore decls in HO types
1178 (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,
1159 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1180 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1160 imps True (n:env) sc
1181 imps True (n:env) sc
1161 imps top env (PPi (Constraint l _) n ty sc)
1182 imps top env (PPi (Constraint l _) n ty sc)
@@ -1163,7 +1184,7 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1163 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1184 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1164 _ -> [])
1185 _ -> [])
1165 (decls, ns) <- get -- ignore decls in HO types
1186 (decls, ns) <- get -- ignore decls in HO types
1166− put (PConstraint 10 l Placeholder : decls,
1187+ put (PConstraint 10 l n Placeholder : decls,
1167 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1188 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1168 imps True (n:env) sc
1189 imps True (n:env) sc
1169 imps top env (PPi (TacImp l _ scr) n ty sc)
1190 imps top env (PPi (TacImp l _ scr) n ty sc)
@@ -1329,7 +1350,7 @@ aiFn inpat True ist fc f ds []
1329-- any constructor alts || any allImp ialts))
1350-- any constructor alts || any allImp ialts))
1330 then aiFn inpat False ist fc f ds [] -- use it as a constructor
1351 then aiFn inpat False ist fc f ds [] -- use it as a constructor
1331 else Right $ PPatvar fc f
1352 else Right $ PPatvar fc f
1332− where imp (PExp _ _ _) = False
1353+ where imp (PExp _ _ _ _) = False
1333 imp _ = True
1354 imp _ = True
1334-- allImp [] = False
1355-- allImp [] = False
1335 allImp xs = all imp xs
1356 allImp xs = all imp xs
@@ -1376,27 +1397,41 @@ aiFn inpat expat ist fc f ds as
1376 [(n,t)] -> t
1397 [(n,t)] -> t
1377 _ -> Public
1398 _ -> Public
1378
1399
1379−
1380 insertImpl :: [PArg] -> [PArg] -> [PArg]
1400 insertImpl :: [PArg] -> [PArg] -> [PArg]
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]
1381− insertImpl (PExp p l ty : ps) (PExp _ _ tm : given) =
1407+ insImpAcc pnas (PExp p l n ty : ps) (PExp _ _ _ tm : given) =
1382− PExp p l tm : insertImpl ps given
1408+ PExp p l n tm : insImpAcc (M.insert n tm pnas) ps given
1383− insertImpl (PConstraint p l ty : ps) (PConstraint _ _ tm : given) =
1409+ insImpAcc pnas (PConstraint p l n ty : ps) (PConstraint _ _ _ tm : given) =
1384− PConstraint p l tm : insertImpl ps given
1410+ PConstraint p l n tm : insImpAcc (M.insert n tm pnas) ps given
1385− insertImpl (PConstraint p l ty : ps) given =
1411+ insImpAcc pnas (PConstraint p l n ty : ps) given =
1386− PConstraint p l (PResolveTC fc) : insertImpl ps given
1412+ let rtc = PResolveTC fc in
1413+ PConstraint p l n rtc : insImpAcc (M.insert n rtc pnas) ps given
1387− insertImpl (PImp p _ l n ty : ps) given =
1414+ insImpAcc pnas (PImp p _ l n ty : ps) given =
1388 case find n given [] of
1415 case find n given [] of
1416+ Just (tm, given') ->
1389− Just (tm, given') -> PImp p False l n tm : insertImpl ps given'
1417+ PImp p False l n tm : insImpAcc (M.insert n tm pnas) ps given'
1418+ Nothing ->
1390− Nothing -> PImp p True l n Placeholder : insertImpl ps given
1419+ PImp p True l n Placeholder :
1420+ insImpAcc (M.insert n Placeholder pnas) ps given
1391− insertImpl (PTacImplicit p l n sc' ty : ps) given =
1421+ insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given =
1392− let sc = addImpl ist sc' in
1422+ let sc = addImpl ist (substMatches (M.toList pnas) sc') in
1393 case find n given [] of
1423 case find n given [] of
1424+ Just (tm, given') ->
1394− Just (tm, given') -> PTacImplicit p l n sc tm : insertImpl ps given'
1425+ PTacImplicit p l n sc tm :
1426+ insImpAcc (M.insert n tm pnas) ps given'
1395− Nothing -> if inpat
1427+ Nothing ->
1428+ if inpat
1396− then PTacImplicit p l n sc Placeholder : insertImpl ps given
1429+ then PTacImplicit p l n sc Placeholder :
1430+ insImpAcc (M.insert n Placeholder pnas) ps given
1397− else PTacImplicit p l n sc sc : insertImpl ps given
1431+ else PTacImplicit p l n sc sc :
1432+ insImpAcc (M.insert n sc pnas) ps given
1398− insertImpl expected [] = []
1433+ insImpAcc _ expected [] = []
1399− insertImpl _ given = given
1434+ insImpAcc _ _ given = given
1400
1435
1401 find n [] acc = Nothing
1436 find n [] acc = Nothing
1402 find n (PImp _ _ _ n' t : gs) acc
1437 find n (PImp _ _ _ n' t : gs) acc
@@ -1433,11 +1468,11 @@ stripLinear i tm = evalState (sl tm) [] where
1433 return $ PApp fc fn args'
1468 return $ PApp fc fn args'
1434 where slA (PImp p m l n t) = do t' <- sl t
1469 where slA (PImp p m l n t) = do t' <- sl t
1435 return $ PImp p m l n t'
1470 return $ PImp p m l n t'
1436− slA (PExp p l t) = do t' <- sl t
1471+ slA (PExp p l n t) = do t' <- sl t
1437− return $ PExp p l t'
1472+ return $ PExp p l n t'
1438− slA (PConstraint p l t)
1473+ slA (PConstraint p l n t)
1439 = do t' <- sl t
1474 = do t' <- sl t
1440− return $ PConstraint p l t'
1475+ return $ PConstraint p l n t'
1441 slA (PTacImplicit p l n sc t)
1476 slA (PTacImplicit p l n sc t)
1442 = do t' <- sl t
1477 = do t' <- sl t
1443 return $ PTacImplicit p l n sc t'
1478 return $ PTacImplicit p l n sc t'
src/Idris/AbsSyntaxTree.hs+42−15
@@ -36,6 +36,19 @@ import Debug.Trace
36
36
37import Text.PrettyPrint.Annotated.Leijen
37import Text.PrettyPrint.Annotated.Leijen
38
38
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+
39data IOption = IOption { opt_logLevel :: Int,
52data IOption = IOption { opt_logLevel :: Int,
40 opt_typecase :: Bool,
53 opt_typecase :: Bool,
41 opt_typeintype :: Bool,
54 opt_typeintype :: Bool,
@@ -767,9 +780,11 @@ data PArg' t = PImp { priority :: Int,
767 pname :: Name, getTm :: t }
780 pname :: Name, getTm :: t }
768 | PExp { priority :: Int,
781 | PExp { priority :: Int,
769 argopts :: [ArgOpt],
782 argopts :: [ArgOpt],
783+ pname :: Name,
770 getTm :: t }
784 getTm :: t }
771 | PConstraint { priority :: Int,
785 | PConstraint { priority :: Int,
772 argopts :: [ArgOpt],
786 argopts :: [ArgOpt],
787+ pname :: Name,
773 getTm :: t }
788 getTm :: t }
774 | PTacImplicit { priority :: Int,
789 | PTacImplicit { priority :: Int,
775 argopts :: [ArgOpt],
790 argopts :: [ArgOpt],
@@ -786,8 +801,8 @@ lazyarg tm = Lazy `elem` argopts tm
786
801
787instance Sized a => Sized (PArg' a) where
802instance Sized a => Sized (PArg' a) where
788 size (PImp p _ l nm trm) = 1 + size nm + size trm
803 size (PImp p _ l nm trm) = 1 + size nm + size trm
789− size (PExp p l trm) = 1 + size trm
804+ size (PExp p l nm trm) = 1 + size nm + size trm
790− size (PConstraint p l trm) = 1 + size trm
805+ size (PConstraint p l nm trm) = 1 + size nm +size nm + size trm
791 size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
806 size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
792
807
793{-!
808{-!
@@ -796,8 +811,8 @@ deriving instance NFData PArg'
796!-}
811!-}
797
812
798pimp n t mach = PImp 1 mach [Lazy] n t
813pimp n t mach = PImp 1 mach [Lazy] n t
799−pexp t = PExp 1 [] t
814+pexp t = PExp 1 [] (sMN 0 "arg") t
800−pconst t = PConstraint 1 [] t
815+pconst t = PConstraint 1 [] (sMN 0 "carg") t
801ptacimp n s t = PTacImplicit 2 [Lazy] n s t
816ptacimp n s t = PTacImplicit 2 [Lazy] n s t
802
817
803type PArg = PArg' PTerm
818type PArg = PArg' PTerm
@@ -1255,8 +1270,8 @@ pprintPTerm impl bnd docArgs = prettySe 10 bnd
1255 prettySe p bnd _ = text "test"
1270 prettySe p bnd _ = text "test"
1256
1271
1257 prettyArgS bnd (PImp _ _ _ n tm) = prettyArgSi bnd (n, tm)
1272 prettyArgS bnd (PImp _ _ _ n tm) = prettyArgSi bnd (n, tm)
1258− prettyArgS bnd (PExp _ _ tm) = prettyArgSe bnd tm
1273+ prettyArgS bnd (PExp _ _ _ tm) = prettyArgSe bnd tm
1259− prettyArgS bnd (PConstraint _ _ tm) = prettyArgSc bnd tm
1274+ prettyArgS bnd (PConstraint _ _ _ tm) = prettyArgSc bnd tm
1260 prettyArgS bnd (PTacImplicit _ _ n _ tm) = prettyArgSti bnd (n, tm)
1275 prettyArgS bnd (PTacImplicit _ _ n _ tm) = prettyArgSti bnd (n, tm)
1261
1276
1262 prettyArgSe bnd arg = prettySe 0 bnd arg
1277 prettyArgSe bnd arg = prettySe 0 bnd arg
@@ -1388,12 +1403,12 @@ getImps (_ : xs) = getImps xs
1388
1403
1389getExps :: [PArg] -> [PTerm]
1404getExps :: [PArg] -> [PTerm]
1390getExps [] = []
1405getExps [] = []
1391−getExps (PExp _ _ tm : xs) = tm : getExps xs
1406+getExps (PExp _ _ _ tm : xs) = tm : getExps xs
1392getExps (_ : xs) = getExps xs
1407getExps (_ : xs) = getExps xs
1393
1408
1394getConsts :: [PArg] -> [PTerm]
1409getConsts :: [PArg] -> [PTerm]
1395getConsts [] = []
1410getConsts [] = []
1396−getConsts (PConstraint _ _ tm : xs) = tm : getConsts xs
1411+getConsts (PConstraint _ _ _ tm : xs) = tm : getConsts xs
1397getConsts (_ : xs) = getConsts xs
1412getConsts (_ : xs) = getConsts xs
1398
1413
1399getAll :: [PArg] -> [PTerm]
1414getAll :: [PArg] -> [PTerm]
@@ -1481,7 +1496,7 @@ getPArity _ = 0
1481
1496
1482allNamesIn :: PTerm -> [Name]
1497allNamesIn :: PTerm -> [Name]
1483allNamesIn tm = nub $ ni [] tm
1498allNamesIn tm = nub $ ni [] tm
1484− where
1499+ where -- TODO THINK added niTacImp, but is it right?
1485 ni env (PRef _ n)
1500 ni env (PRef _ n)
1486 | not (n `elem` env) = [n]
1501 | not (n `elem` env) = [n]
1487 ni env (PPatvar _ n) = [n]
1502 ni env (PPatvar _ n) = [n]
@@ -1489,7 +1504,7 @@ allNamesIn tm = nub $ ni [] tm
1489 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1504 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1490 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
1505 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
1491 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1506 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
1493 ni env (PHidden tm) = ni env tm
1508 ni env (PHidden tm) = ni env tm
1494 ni env (PEq _ l r) = ni env l ++ ni env r
1509 ni env (PEq _ l r) = ni env l ++ ni env r
1495 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1510 ni env (PRewrite _ l r _) = ni env l ++ ni env r
@@ -1503,16 +1518,19 @@ allNamesIn tm = nub $ ni [] tm
1503 ni env (PNoImplicits tm) = ni env tm
1518 ni env (PNoImplicits tm) = ni env tm
1504 ni env _ = []
1519 ni env _ = []
1505
1520
1521+ niTacImp env (TacImp _ _ scr) = ni env scr
1522+ niTacImp _ _ = []
1523+
1506-- Return all names defined in binders in the given term
1524-- Return all names defined in binders in the given term
1507boundNamesIn :: PTerm -> [Name]
1525boundNamesIn :: PTerm -> [Name]
1508boundNamesIn tm = nub $ ni tm
1526boundNamesIn tm = nub $ ni tm
1509− where
1527+ where -- TODO THINK Added niTacImp, but is it right?
1510 ni (PApp _ f as) = ni f ++ concatMap (ni) (map getTm as)
1528 ni (PApp _ f as) = ni f ++ concatMap (ni) (map getTm as)
1511 ni (PAppBind _ f as) = ni f ++ concatMap (ni) (map getTm as)
1529 ni (PAppBind _ f as) = ni f ++ concatMap (ni) (map getTm as)
1512 ni (PCase _ c os) = ni c ++ concatMap (ni) (map snd os)
1530 ni (PCase _ c os) = ni c ++ concatMap (ni) (map snd os)
1513 ni (PLam n ty sc) = n : (ni ty ++ ni sc)
1531 ni (PLam n ty sc) = n : (ni ty ++ ni sc)
1514 ni (PLet n ty val sc) = n : (ni ty ++ ni val ++ ni sc)
1532 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))
1516 ni (PEq _ l r) = ni l ++ ni r
1534 ni (PEq _ l r) = ni l ++ ni r
1517 ni (PRewrite _ l r _) = ni l ++ ni r
1535 ni (PRewrite _ l r _) = ni l ++ ni r
1518 ni (PTyped l r) = ni l ++ ni r
1536 ni (PTyped l r) = ni l ++ ni r
@@ -1526,6 +1544,9 @@ boundNamesIn tm = nub $ ni tm
1526 ni (PNoImplicits tm) = ni tm
1544 ni (PNoImplicits tm) = ni tm
1527 ni _ = []
1545 ni _ = []
1528
1546
1547+ niTacImp (TacImp _ _ scr) = ni scr
1548+ niTacImp _ = []
1549+
1529-- Return names which are free in the given term.
1550-- Return names which are free in the given term.
1530namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
1551namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
1531namesIn uvars ist tm = nub $ ni [] tm
1552namesIn uvars ist tm = nub $ ni [] tm
@@ -1539,7 +1560,7 @@ namesIn uvars ist tm = nub $ ni [] tm
1539 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1560 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1540 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
1561 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
1541 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1562 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
1543 ni env (PEq _ l r) = ni env l ++ ni env r
1564 ni env (PEq _ l r) = ni env l ++ ni env r
1544 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1565 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1545 ni env (PTyped l r) = ni env l ++ ni env r
1566 ni env (PTyped l r) = ni env l ++ ni env r
@@ -1553,11 +1574,14 @@ namesIn uvars ist tm = nub $ ni [] tm
1553 ni env (PNoImplicits tm) = ni env tm
1574 ni env (PNoImplicits tm) = ni env tm
1554 ni env _ = []
1575 ni env _ = []
1555
1576
1577+ niTacImp env (TacImp _ _ scr) = ni env scr
1578+ niTacImp _ _ = []
1579+
1556-- Return which of the given names are used in the given term.
1580-- Return which of the given names are used in the given term.
1557
1581
1558usedNamesIn :: [Name] -> IState -> PTerm -> [Name]
1582usedNamesIn :: [Name] -> IState -> PTerm -> [Name]
1559usedNamesIn vars ist tm = nub $ ni [] tm
1583usedNamesIn vars ist tm = nub $ ni [] tm
1560− where
1584+ where -- TODO THINK added niTacImp, but is it right?
1561 ni env (PRef _ n)
1585 ni env (PRef _ n)
1562 | n `elem` vars && not (n `elem` env)
1586 | n `elem` vars && not (n `elem` env)
1563 = case lookupTy n (tt_ctxt ist) of
1587 = case lookupTy n (tt_ctxt ist) of
@@ -1567,7 +1591,7 @@ usedNamesIn vars ist tm = nub $ ni [] tm
1567 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1591 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1568 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
1592 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
1569 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1593 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
1571 ni env (PEq _ l r) = ni env l ++ ni env r
1595 ni env (PEq _ l r) = ni env l ++ ni env r
1572 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1596 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1573 ni env (PTyped l r) = ni env l ++ ni env r
1597 ni env (PTyped l r) = ni env l ++ ni env r
@@ -1581,3 +1605,6 @@ usedNamesIn vars ist tm = nub $ ni [] tm
1581 ni env (PNoImplicits tm) = ni env tm
1605 ni env (PNoImplicits tm) = ni env tm
1582 ni env _ = []
1606 ni env _ = []
1583
1607
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
72 -- there may be more case splitting that the idris_implicits record
72 -- there may be more case splitting that the idris_implicits record
73 -- suggests)
73 -- suggests)
74 let parg = case lookupCtxt n (idris_implicits i) of
74 let parg = case lookupCtxt n (idris_implicits i) of
75+ (p : _) ->
75− (p : _) -> p ++ repeat (PExp 0 [] Placeholder)
76+ p ++ repeat (PExp 0 [] (sMN 0 "gcarg") Placeholder)
76− _ -> repeat (pexp Placeholder)
77+ _ -> repeat (pexp Placeholder)
77 let tryclauses = mkClauses parg all_args
78 let tryclauses = mkClauses parg all_args
78 logLvl 2 $ show (length tryclauses) ++ " initially to check"
79 logLvl 2 $ show (length tryclauses) ++ " initially to check"
79 logLvl 1 $ showSep "\n" (map (showTm i) tryclauses)
80 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
276instance (NFData t) => NFData (PArg' t) where
276instance (NFData t) => NFData (PArg' t) where
277 rnf (PImp x1 x2 x3 x4 x5)
277 rnf (PImp x1 x2 x3 x4 x5)
278 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()
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)
283 rnf (PTacImplicit x1 x2 x3 x4 x5)
284 = rnf x1 `seq`
284 = rnf x1 `seq`
285 rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `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)
58 = PLam n (de env [] ty) (de ((n,n):env) [] sc)
59 de env ((PImp { argopts = opts }):is) (Bind n (Pi ty) 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)
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)
62 = PPi constraint n (de env [] ty) (de ((n,n):env) is sc)
63 de env (PTacImplicit _ _ _ tac _:is) (Bind n (Pi ty) 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)
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)
121 | otherwise = PApp un (PRef un n) (map pexp args)
122
122
123 imp (PImp p m l n _) arg = PImp p m l n arg
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
126 imp (PTacImplicit p l n sc _) arg = PTacImplicit p l n sc arg
127
127
128-- | How far to indent sub-errors
128-- | 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
82
82
83 logLvl 3 $ show n ++ " pre-type " ++ showTmImpls ty'
83 logLvl 3 $ show n ++ " pre-type " ++ showTmImpls ty'
84 ty' <- addUsingConstraints syn fc ty'
84 ty' <- addUsingConstraints syn fc ty'
85− ty' <- implicit syn n ty'
85+ ty' <- implicit info syn n ty'
86
86
87 let ty = addImpl i ty'
87 let ty = addImpl i ty'
88 logLvl 3 $ show n ++ " type " ++ showTmImpls ty
88 logLvl 3 $ show n ++ " type " ++ showTmImpls ty
@@ -204,7 +204,8 @@ elabData info syn doc argDocs fc opts (PLaterdecl n t_in)
204 checkUndefined fc n
204 checkUndefined fc n
205 ctxt <- getContext
205 ctxt <- getContext
206 i <- getIState
206 i <- getIState
207+ -- TODO think: something more in info?
207− t_in <- implicit syn n t_in
208+ t_in <- implicit info syn n t_in
208 let t = addImpl i t_in
209 let t = addImpl i t_in
209 ((t', defer, is), log) <- tclift $ elaborate ctxt n (TType (UVal 0)) []
210 ((t', defer, is), log) <- tclift $ elaborate ctxt n (TType (UVal 0)) []
210 (erun fc (build i info False [] n t))
211 (erun fc (build i info False [] n t))
@@ -222,7 +223,7 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)
222 undef <- isUndefined fc n
223 undef <- isUndefined fc n
223 ctxt <- getContext
224 ctxt <- getContext
224 i <- getIState
225 i <- getIState
225− t_in <- implicit syn n t_in
226+ t_in <- implicit info syn n t_in
226 let t = addImpl i t_in
227 let t = addImpl i t_in
227 ((t', defer, is), log) <-
228 ((t', defer, is), log) <-
228 tclift $ elaborate ctxt n (TType (UVal 0)) []
229 tclift $ elaborate ctxt n (TType (UVal 0)) []
@@ -238,7 +239,8 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)
238 logLvl 2 $ "---> " ++ show cty
239 logLvl 2 $ "---> " ++ show cty
239 -- temporary, to check cons
240 -- temporary, to check cons
240 when undef $ updateContext (addTyDecl n (TCon 0 0) cty)
241 when undef $ updateContext (addTyDecl n (TCon 0 0) cty)
242+ let cnameinfo = cinfo info (map cname dcons)
241− cons <- mapM (elabCon info syn n codata) dcons
243+ cons <- mapM (elabCon cnameinfo syn n codata) dcons
242 ttag <- getName
244 ttag <- getName
243 i <- getIState
245 i <- getIState
244 let as = map (const Nothing) (getArgTys cty)
246 let as = map (const Nothing) (getArgTys cty)
@@ -321,6 +323,21 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)
321 | otherwise = count n ts
323 | otherwise = count n ts
322 mParam args (_ : rest) = Nothing : mParam args rest
324 mParam args (_ : rest) = Nothing : mParam args rest
323
325
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+
324type EliminatorState = StateT (Map.Map String Int) Idris
341type EliminatorState = StateT (Map.Map String Int) Idris
325
342
326-- TODO: Use uniqueName for generating names, rewrite everything to use idris_implicits instead of manual splitting, generally just rewrite
343-- 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 ->
730 PTerm -> Docstring -> Name -> PTerm -> Idris ()
747 PTerm -> Docstring -> Name -> PTerm -> Idris ()
731elabRecord info syn doc fc tyn ty cdoc cn cty
748elabRecord info syn doc fc tyn ty cdoc cn cty
732 = do elabData info syn doc [] fc [] (PDatadecl tyn ty [(cdoc, [], cn, cty, fc, [])])
749 = do elabData info syn doc [] fc [] (PDatadecl tyn ty [(cdoc, [], cn, cty, fc, [])])
750+ -- TODO think: something more in info?
733− cty' <- implicit syn cn cty
751+ cty' <- implicit info syn cn cty
734 i <- getIState
752 i <- getIState
735 cty <- case lookupTy cn (tt_ctxt i) of
753 cty <- case lookupTy cn (tt_ctxt i) of
736 [t] -> return (delab i t)
754 [t] -> return (delab i t)
@@ -752,7 +770,7 @@ elabRecord info syn doc fc tyn ty cdoc cn cty
752 where
770 where
753-- syn = syn_in { syn_namespace = show (nsroot tyn) : syn_namespace syn_in }
771-- syn = syn_in { syn_namespace = show (nsroot tyn) : syn_namespace syn_in }
754
772
755− isNonImp (PExp _ _ _, a) = Just a
773+ isNonImp (PExp _ _ _ _, a) = Just a
756 isNonImp _ = Nothing
774 isNonImp _ = Nothing
757
775
758 tryElabDecl info (fn, ty, val)
776 tryElabDecl info (fn, ty, val)
@@ -841,7 +859,7 @@ elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)
841 = do checkUndefined fc n
859 = do checkUndefined fc n
842 ctxt <- getContext
860 ctxt <- getContext
843 i <- getIState
861 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)
845 let t = addImpl i t_in
863 let t = addImpl i t_in
846 logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t
864 logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t
847 ((t', defer, is), log) <-
865 ((t', defer, is), log) <-
@@ -875,7 +893,7 @@ elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)
875
893
876 mkLazy (PPi pl n ty sc)
894 mkLazy (PPi pl n ty sc)
877 = let ty' = if getTyName ty
895 = let ty' = if getTyName ty
878− then PApp fc (PRef fc (sUN "Lazy'"))
896+ then PApp fc (PRef fc (sUN "Lazy'"))
879 [pexp (PRef fc (sUN "LazyCodata")),
897 [pexp (PRef fc (sUN "LazyCodata")),
880 pexp ty]
898 pexp ty]
881 else ty in
899 else ty in
@@ -1292,7 +1310,7 @@ checkPossible info fc tcgen fname lhs_in
1292 ((P _ x _, _), (P _ y _, _)) -> x == y
1310 ((P _ x _, _), (P _ y _, _)) -> x == y
1293 _ -> False
1311 _ -> False
1294
1312
1295−getFixedInType i env (PExp _ _ _ : is) (Bind n (Pi t) sc)
1313+getFixedInType i env (PExp _ _ _ _ : is) (Bind n (Pi t) sc)
1296 = getFixedInType i (n : env) is (instantiate (P Bound n t) sc)
1314 = getFixedInType i (n : env) is (instantiate (P Bound n t) sc)
1297getFixedInType i env (_ : is) (Bind n (Pi t) sc)
1315getFixedInType i env (_ : is) (Bind n (Pi t) sc)
1298 = getFixedInType i (n : env) is (instantiate (P Bound n t) sc)
1316 = 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)
1423 -- Elaborate where block
1441 -- Elaborate where block
1424 ist <- getIState
1442 ist <- getIState
1425 windex <- getName
1443 windex <- getName
1426− let winfo = pinfo (pvars ist lhs_tm) whereblock windex
1427 let decls = nub (concatMap declared whereblock)
1444 let decls = nub (concatMap declared whereblock)
1428 let defs = nub (decls ++ concatMap defined whereblock)
1445 let defs = nub (decls ++ concatMap defined whereblock)
1429 let newargs = pvars ist lhs_tm
1446 let newargs = pvars ist lhs_tm
1447+ let winfo = pinfo info newargs defs windex
1430 let wb = map (expandParamsD False ist decorate newargs defs) whereblock
1448 let wb = map (expandParamsD False ist decorate newargs defs) whereblock
1431
1449
1432 -- Split the where block into declarations with a type, and those
1450 -- 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)
1435 let (wbefore, wafter) = sepBlocks wb
1453 let (wbefore, wafter) = sepBlocks wb
1436
1454
1437 logLvl 2 $ "Where block:\n " ++ show wbefore ++ "\n" ++ show wafter
1455 logLvl 2 $ "Where block:\n " ++ show wbefore ++ "\n" ++ show wafter
1438− mapM_ (elabDecl' EAll info) wbefore
1456+ mapM_ (elabDecl' EAll winfo) wbefore
1439 -- Now build the RHS, using the type of the LHS as the goal.
1457 -- Now build the RHS, using the type of the LHS as the goal.
1440 i <- getIState -- new implicits from where block
1458 i <- getIState -- new implicits from where block
1441 logLvl 5 (showTmImpls (expandParams decorate newargs defs (defs \\ decls) rhs_in))
1459 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)
1450 mapM_ setinj (nub (params ++ inj))
1468 mapM_ setinj (nub (params ++ inj))
1451 setNextName
1469 setNextName
1452 (_, _, is) <- errAt "right hand side of " fname
1470 (_, _, 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))
1454 errAt "right hand side of " fname
1472 errAt "right hand side of " fname
1455 (erun fc $ psolve lhs_tm)
1473 (erun fc $ psolve lhs_tm)
1456 hs <- get_holes
1474 hs <- get_holes
@@ -1478,8 +1496,8 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
1478 -- Now the remaining deferred (i.e. no type declarations) clauses
1496 -- Now the remaining deferred (i.e. no type declarations) clauses
1479 -- from the where block
1497 -- from the where block
1480
1498
1481− mapM_ (elabDecl' EAll info) wafter
1499+ mapM_ (elabDecl' EAll winfo) wafter
1482− mapM_ (elabCaseBlock info opts) is
1500+ mapM_ (elabCaseBlock winfo opts) is
1483
1501
1484 ctxt <- getContext
1502 ctxt <- getContext
1485 logLvl 5 $ "Rechecking"
1503 logLvl 5 $ "Rechecking"
@@ -1509,6 +1527,19 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
1509 addErrRev (crhs, clhs)
1527 addErrRev (crhs, clhs)
1510 return $ (Right (clhs, crhs), lhs)
1528 return $ (Right (clhs, crhs), lhs)
1511 where
1529 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+
1512 mkLHSapp t@(PRef _ _) = trace ("APP " ++ show t) $ PApp fc t []
1543 mkLHSapp t@(PRef _ _) = trace ("APP " ++ show t) $ PApp fc t []
1513 mkLHSapp t = t
1544 mkLHSapp t = t
1514
1545
@@ -1531,19 +1562,6 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
1531 (b : bf, af)
1562 (b : bf, af)
1532 sepBlocks' ns [] = ([], [])
1563 sepBlocks' ns [] = ([], [])
1533
1564
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−
1547
1565
1548 -- if a hole is just an argument/result of a case block, treat it as
1566 -- if a hole is just an argument/result of a case block, treat it as
1549 -- the unit type. Hack to help elaborate case in do blocks.
1567 -- the unit type. Hack to help elaborate case in do blocks.
@@ -1808,7 +1826,7 @@ elabClass info syn doc fc constraints tn ps ds
1808
1826
1809 getMName (PTy _ _ _ _ _ n _) = nsroot n
1827 getMName (PTy _ _ _ _ _ n _) = nsroot n
1810 tdecl allmeths (PTy doc _ syn _ o n t)
1828 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
1812 logLvl 5 $ "Method " ++ show n ++ " : " ++ showTmImpls t'
1830 logLvl 5 $ "Method " ++ show n ++ " : " ++ showTmImpls t'
1813 return ( (n, (toExp (map fst ps) Exp t')),
1831 return ( (n, (toExp (map fst ps) Exp t')),
1814 (n, (doc, o, (toExp (map fst ps) Imp t'))),
1832 (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
2012 -- TODO: largely based upon elabType' - should try to abstract
2030 -- TODO: largely based upon elabType' - should try to abstract
2013 elabFindOverlapping i ci iname syn t
2031 elabFindOverlapping i ci iname syn t
2014 = do ty' <- addUsingConstraints syn fc t
2032 = do ty' <- addUsingConstraints syn fc t
2033+ -- TODO think: something more in info?
2015− ty' <- implicit syn iname ty'
2034+ ty' <- implicit info syn iname ty'
2016 let ty = addImpl i ty'
2035 let ty = addImpl i ty'
2017 ctxt <- getContext
2036 ctxt <- getContext
2018 ((tyT, _, _), _) <-
2037 ((tyT, _, _), _) <-
@@ -2050,9 +2069,9 @@ elabInstance info syn what fc cs n ps t expn ds = do
2050 methArgs i (PPi (Imp _ _ _) n ty sc)
2069 methArgs i (PPi (Imp _ _ _) n ty sc)
2051 = PImp 0 True [] n (PRef fc (sMN i "meth")) : methArgs (i+1) sc
2070 = PImp 0 True [] n (PRef fc (sMN i "meth")) : methArgs (i+1) sc
2052 methArgs i (PPi (Exp _ _ _) n ty sc)
2071 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
2054 methArgs i (PPi (Constraint _ _) n ty sc)
2073 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
2056 methArgs i _ = []
2075 methArgs i _ = []
2057
2076
2058 papp fc f [] = f
2077 papp fc f [] = f
src/Idris/ElabTerm.hs+2−11
@@ -3,6 +3,7 @@
3module Idris.ElabTerm where
3module Idris.ElabTerm where
4
4
5import Idris.AbsSyntax
5import Idris.AbsSyntax
6+import Idris.AbsSyntaxTree
6import Idris.DSL
7import Idris.DSL
7import Idris.Delaborate
8import Idris.Delaborate
8import Idris.Error
9import Idris.Error
@@ -27,16 +28,6 @@ import qualified Data.Text as T
27
28
28import Debug.Trace
29import Debug.Trace
29
30
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−
40-- Using the elaborator, convert a term in raw syntax to a fully
31-- Using the elaborator, convert a term in raw syntax to a fully
41-- elaborated, typechecked term.
32-- elaborated, typechecked term.
42--
33--
@@ -697,7 +688,7 @@ elab ist info pattern opts fn tm
697 where
688 where
698 mkDelay (PAlternative b xs) = PAlternative b (map mkDelay xs)
689 mkDelay (PAlternative b xs) = PAlternative b (map mkDelay xs)
699 mkDelay t = let fc = fileFC "Delay" in
690 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"))
701 [pexp t])
692 [pexp t])
702
693
703 insertCoerce ina t =
694 insertCoerce ina t =
src/Idris/IBC.hs+9−5
@@ -29,7 +29,7 @@ import Codec.Compression.Zlib (compress)
29import Util.Zlib (decompressEither)
29import Util.Zlib (decompressEither)
30
30
31ibcVersion :: Word8
31ibcVersion :: Word8
32−ibcVersion = 65
32+ibcVersion = 66
33
33
34data IBCFile = IBCFile { ver :: Word8,
34data IBCFile = IBCFile { ver :: Word8,
35 sourcefile :: FilePath,
35 sourcefile :: FilePath,
@@ -2037,16 +2037,18 @@ instance (Binary t) => Binary (PArg' t) where
2037 put x3
2037 put x3
2038 put x4
2038 put x4
2039 put x5
2039 put x5
2040− PExp x1 x2 x3 ->
2040+ PExp x1 x2 x3 x4 ->
2041 do putWord8 1
2041 do putWord8 1
2042 put x1
2042 put x1
2043 put x2
2043 put x2
2044 put x3
2044 put x3
2045+ put x4
2045− PConstraint x1 x2 x3 ->
2046+ PConstraint x1 x2 x3 x4 ->
2046 do putWord8 2
2047 do putWord8 2
2047 put x1
2048 put x1
2048 put x2
2049 put x2
2049 put x3
2050 put x3
2051+ put x4
2050 PTacImplicit x1 x2 x3 x4 x5 ->
2052 PTacImplicit x1 x2 x3 x4 x5 ->
2051 do putWord8 3
2053 do putWord8 3
2052 put x1
2054 put x1
@@ -2066,11 +2068,13 @@ instance (Binary t) => Binary (PArg' t) where
2066 1 -> do x1 <- get
2068 1 -> do x1 <- get
2067 x2 <- get
2069 x2 <- get
2068 x3 <- get
2070 x3 <- get
2071+ x4 <- get
2069− return (PExp x1 x2 x3)
2072+ return (PExp x1 x2 x3 x4)
2070 2 -> do x1 <- get
2073 2 -> do x1 <- get
2071 x2 <- get
2074 x2 <- get
2072 x3 <- get
2075 x3 <- get
2076+ x4 <- get
2073− return (PConstraint x1 x2 x3)
2077+ return (PConstraint x1 x2 x3 x4)
2074 3 -> do x1 <- get
2078 3 -> do x1 <- get
2075 x2 <- get
2079 x2 <- get
2076 x3 <- get
2080 x3 <- get
src/Idris/ParseExpr.hs+19−8
@@ -150,15 +150,23 @@ extension syn (Rule ssym ptm _)
150 update ns (PRef fc n) = case lookup n ns of
150 update ns (PRef fc n) = case lookup n ns of
151 Just (SynTm t) -> t
151 Just (SynTm t) -> t
152 _ -> PRef fc n
152 _ -> PRef fc n
153+ update ns (PLam n ty sc)
153− update ns (PLam n ty sc) = PLam (updateB ns n) (update ns ty) (update (dropn n ns) 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)
154− update ns (PPi p n ty sc) = PPi p (updateB ns n) (update ns ty) (update (dropn n ns) sc)
157+ (update ns ty) (update (dropn n ns) sc)
158+ update ns (PLet n ty val sc)
155− update ns (PLet n ty val sc) = PLet (updateB ns n) (update ns ty) (update ns val)
159+ = PLet (updateB ns n) (update ns ty)
156− (update (dropn n ns) sc)
160+ (update ns val) (update (dropn n ns) sc)
161+ update ns (PApp fc t args)
157− update ns (PApp fc t args) = PApp fc (update ns t) (map (fmap (update ns)) args)
162+ = PApp fc (update ns t) (map (fmap (update ns)) args)
163+ update ns (PAppBind fc t args)
158− update ns (PAppBind fc t args) = PAppBind fc (update ns t) (map (fmap (update ns)) args)
164+ = PAppBind fc (update ns t) (map (fmap (update ns)) args)
165+ update ns (PCase fc c opts)
159− update ns (PCase fc c opts) = PCase fc (update ns c) (map (pmap (update ns)) opts)
166+ = PCase fc (update ns c) (map (pmap (update ns)) opts)
160 update ns (PPair fc p l r) = PPair fc p (update ns l) (update ns r)
167 update ns (PPair fc p l r) = PPair fc p (update ns l) (update ns r)
168+ update ns (PDPair fc p l t r)
161− update ns (PDPair fc p l t r) = PDPair fc p (update ns l) (update ns t) (update ns r)
169+ = PDPair fc p (update ns l) (update ns t) (update ns r)
162 update ns (PAlternative a as) = PAlternative a (map (update ns) as)
170 update ns (PAlternative a as) = PAlternative a (map (update ns) as)
163 update ns (PHidden t) = PHidden (update ns t)
171 update ns (PHidden t) = PHidden (update ns t)
164 update ns (PDoBlock ds) = PDoBlock $ upd ns ds
172 update ns (PDoBlock ds) = PDoBlock $ upd ns ds
@@ -176,6 +184,9 @@ extension syn (Rule ssym ptm _)
176 update ns (PGoal fc r n sc) = PGoal fc (update ns r) n (update ns sc)
184 update ns (PGoal fc r n sc) = PGoal fc (update ns r) n (update ns sc)
177 update ns t = t
185 update ns t = t
178
186
187+ updTacImp ns (TacImp o st scr) = TacImp o st (update ns scr)
188+ updTacImp _ x = x
189+
179{- | Parses a (normal) built-in expression
190{- | Parses a (normal) built-in expression
180@
191@
181InternalExpr ::=
192InternalExpr ::=
src/Idris/Parser.hs+2−2
@@ -18,13 +18,13 @@ import qualified Text.Parser.Token.Highlight as Hi
18
18
19import Text.PrettyPrint.ANSI.Leijen (Doc, plain)
19import Text.PrettyPrint.ANSI.Leijen (Doc, plain)
20
20
21−import Idris.AbsSyntax
21+import Idris.AbsSyntax hiding (namespace, params)
22import Idris.DSL
22import Idris.DSL
23import Idris.Imports
23import Idris.Imports
24import Idris.Delaborate
24import Idris.Delaborate
25import Idris.Error
25import Idris.Error
26import Idris.ElabDecls
26import Idris.ElabDecls
27−import Idris.ElabTerm hiding (namespace, params)
27+import Idris.ElabTerm
28import Idris.Coverage
28import Idris.Coverage
29import Idris.IBC
29import Idris.IBC
30import Idris.Unlit
30import Idris.Unlit
src/Idris/PartialEval.hs+1−1
@@ -124,7 +124,7 @@ getSpecApps ist env tm = ga env (explicitNames tm) where
124 | imparg imp = (ImplicitD, tm)
124 | imparg imp = (ImplicitD, tm)
125 | otherwise = (ExplicitD, (P Ref (sUN (show n ++ "arg")) Erased))
125 | otherwise = (ExplicitD, (P Ref (sUN (show n ++ "arg")) Erased))
126
126
127− imparg (PExp _ _ _) = False
127+ imparg (PExp _ _ _ _) = False
128 imparg _ = True
128 imparg _ = True
129
129
130 buildApp env [] [] _ _ = []
130 buildApp env [] [] _ _ = []
src/Idris/Providers.hs+2−1
@@ -11,7 +11,8 @@ import Debug.Trace
11
11
12-- | Wrap a type provider in the type of type providers
12-- | Wrap a type provider in the type of type providers
13providerTy :: FC -> PTerm -> PTerm
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]
15
16
16ioret = sUN "prim_io_return"
17ioret = sUN "prim_io_return"
17ermod = sNS (sUN "Error") ["Providers"]
18ermod = 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