ad057db · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge branch 'master' of github.com:idris-lang/Idris-dev

ad057dbEdwin Brady13 years ago

.travis.yml+2

@@ -6,6 +6,8 @@ before_install:

6 - sudo apt-get install -qq libghc-unordered-containers-dev libghc-mtl-dev libghc-network-dev libghc-xml-dev libghc-transformers-dev libghc-text-dev libghc-utf8-string-dev libghc-vector-dev libghc-split-dev libghc-ansi-terminal-dev libghc-ansi-wl-pprint-dev

7 # trifecta dependencies

8 - sudo apt-get install -qq libghc-blaze-builder-dev libghc-blaze-html-dev libghc-data-lens-dev libghc-bifunctors-dev libghc-hashable-dev libghc-semigroups-dev libghc-semigroupoids-dev libghc-parallel-dev libghc-comonad-dev libghc-terminfo-dev libghc-keys-dev

9+ # test dependency

10+ - sudo apt-get install -qq expect

9install:

11install:

10 - cabal install -f FFI -f LLVM --only-dependencies --enable-tests

12 - cabal install -f FFI -f LLVM --only-dependencies --enable-tests

11before_script:

13before_script:

CHANGELOG+4

@@ -1,3 +1,7 @@

1+New in 0.9.13:

2+--------------

3+* IDE support for retrieving structured information about metavariables

1New in 0.9.12:

5New in 0.9.12:

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

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

libs/base/Control/Arrow.idr+1−2

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

1−module Category.Arrow

1+module Control.Arrow

3import Data.Morphisms

4import Control.Category

@@ -37,4 +37,3 @@ instance Monad m => Arrow (Kleislimorphism m) where

37 (Kleisli f) &&& (Kleisli g) = Kleisli $ \a => do x <- f a

38 y <- g a

39 return (x, y)

40−

libs/base/Control/Catchable.idr+1−1

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

1−module Prelude.Catchable

1+module Control.Catchable

3import Control.IOExcept

src/Idris/AbsSyntax.hs+69−34

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

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

820 en (PPi p n t s)

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)

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

827 = let n' = mkShadow n in

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

880

881 nseq x y = nsroot x == nsroot y

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+45−16

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

37import Text.PrettyPrint.Annotated.Leijen

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]

@@ -1432,7 +1447,9 @@ showName ist bnd impl colour n = case ist of

1432showTm :: IState -- ^^ the Idris state, for information about identifiers and colours

1447showTm :: IState -- ^^ the Idris state, for information about identifiers and colours

1433 -> PTerm -- ^^ the term to show

1448 -> PTerm -- ^^ the term to show

1434 -> String

1449 -> String

1435−showTm ist = displayDecorated (consoleDecorate ist) . renderCompact . prettyImp (opt_showimp (idris_options ist))

1450+showTm ist = displayDecorated (consoleDecorate ist) .

1451+ renderPretty 0.8 100000 .

1452+ prettyImp (opt_showimp (idris_options ist))

1436

1453

1437-- | Show a term with implicits, no colours

1454-- | Show a term with implicits, no colours

1438showTmImpls :: PTerm -> String

1455showTmImpls :: PTerm -> String

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

1481

1498

1482allNamesIn :: PTerm -> [Name]

1499allNamesIn :: PTerm -> [Name]

1483allNamesIn tm = nub $ ni [] tm

1500allNamesIn tm = nub $ ni [] tm

1484− where

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

1485 ni env (PRef _ n)

1502 ni env (PRef _ n)

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

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

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

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

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

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

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

1507 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

1508 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

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

1510 ni env (PHidden tm) = ni env tm

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

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

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

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

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

1503 ni env (PNoImplicits tm) = ni env tm

1520 ni env (PNoImplicits tm) = ni env tm

1504 ni env _ = []

1521 ni env _ = []

1505

1522

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

1524+ niTacImp _ _ = []

1525+

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

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

1507boundNamesIn :: PTerm -> [Name]

1527boundNamesIn :: PTerm -> [Name]

1508boundNamesIn tm = nub $ ni tm

1528boundNamesIn tm = nub $ ni tm

1509− where

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1526 ni (PNoImplicits tm) = ni tm

1546 ni (PNoImplicits tm) = ni tm

1527 ni _ = []

1547 ni _ = []

1528

1548

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

1550+ niTacImp _ = []

1551+

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

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

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

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

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

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

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

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

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

1563 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

1564 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

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

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

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

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

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

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

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

1553 ni env (PNoImplicits tm) = ni env tm

1576 ni env (PNoImplicits tm) = ni env tm

1554 ni env _ = []

1577 ni env _ = []

1555

1578

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

1580+ niTacImp _ _ = []

1581+

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

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

1557

1583

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

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

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

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

1560− where

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

1561 ni env (PRef _ n)

1587 ni env (PRef _ n)

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

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

1563 = case lookupTy n (tt_ctxt ist) of

1589 = case lookupTy n (tt_ctxt ist) of

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

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

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

1594 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

1595 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

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

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

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

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

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

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

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

1581 ni env (PNoImplicits tm) = ni env tm

1607 ni env (PNoImplicits tm) = ni env tm

1582 ni env _ = []

1608 ni env _ = []

1583

1609

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

1611+ niTacImp _ _ = []

1612+

src/Idris/Core/Execute.hs+97−135

@@ -47,11 +47,8 @@ readMay s = case reads s of

48data Lazy = Delayed ExecEnv Context Term | Forced ExecVal deriving Show

50−data ExecState = ExecState { exec_thunks :: M.Map Int Lazy -- ^ Thunks - the result of evaluating "lazy" or calling lazy funcs

51− , exec_next_thunk :: Int -- ^ Ensure thunk key uniqueness

52− , exec_implicits :: Ctxt [PArg] -- ^ Necessary info on laziness from idris monad

53− , exec_dynamic_libs :: [DynamicLib] -- ^ Dynamic libs from idris monad

50+newtype ExecState = ExecState { exec_dynamic_libs :: [DynamicLib] -- ^ Dynamic libs from idris monad

54− }

51+ }

56data ExecVal = EP NameType Name ExecVal

53data ExecVal = EP NameType Name ExecVal

57 | EV Int

54 | EV Int

@@ -61,20 +58,20 @@ data ExecVal = EP NameType Name ExecVal

61 | EErased

58 | EErased

62 | EConstant Const

59 | EConstant Const

63 | forall a. EPtr (Ptr a)

60 | forall a. EPtr (Ptr a)

64− | EThunk Int

61+ | EThunk Context ExecEnv Term

65 | EHandle Handle

62 | EHandle Handle

67instance Show ExecVal where

64instance Show ExecVal where

68− show (EP _ n _) = show n

65+ show (EP _ n _) = show n

69− show (EV i) = "!!V" ++ show i ++ "!!"

66+ show (EV i) = "!!V" ++ show i ++ "!!"

70− show (EBind n b body) = "EBind " ++ show b ++ " <<fn>>"

67+ show (EBind n b body) = "EBind " ++ show b ++ " <<fn>>"

71− show (EApp e1 e2) = show e1 ++ " (" ++ show e2 ++ ")"

68+ show (EApp e1 e2) = show e1 ++ " (" ++ show e2 ++ ")"

72− show (EType _) = "Type"

69+ show (EType _) = "Type"

73− show EErased = "[__]"

70+ show EErased = "[__]"

74− show (EConstant c) = show c

71+ show (EConstant c) = show c

75− show (EPtr p) = "<<ptr " ++ show p ++ ">>"

72+ show (EPtr p) = "<<ptr " ++ show p ++ ">>"

76− show (EThunk i) = "<<thunk " ++ show i ++ ">>"

73+ show (EThunk _ env tm) = "<<thunk " ++ show env ++ "||||" ++ show tm ++ ">>"

77− show (EHandle h) = "<<handle " ++ show h ++ ">>"

74+ show (EHandle h) = "<<handle " ++ show h ++ ">>"

79toTT :: ExecVal -> Exec Term

76toTT :: ExecVal -> Exec Term

80toTT (EP nt n ty) = (P nt n) <$> (toTT ty)

77toTT (EP nt n ty) = (P nt n) <$> (toTT ty)

@@ -82,22 +79,25 @@ toTT (EV i) = return $ V i

82toTT (EBind n b body) = do body' <- body $ EP Bound n EErased

79toTT (EBind n b body) = do body' <- body $ EP Bound n EErased

83 b' <- fixBinder b

80 b' <- fixBinder b

84 Bind n b' <$> toTT body'

81 Bind n b' <$> toTT body'

85− where fixBinder (Lam t) = Lam <$> toTT t

82+ where fixBinder (Lam t) = Lam <$> toTT t

86− fixBinder (Pi t) = Pi <$> toTT t

83+ fixBinder (Pi t) = Pi <$> toTT t

87− fixBinder (Let t1 t2) = Let <$> toTT t1 <*> toTT t2

84+ fixBinder (Let t1 t2) = Let <$> toTT t1 <*> toTT t2

88− fixBinder (NLet t1 t2) = NLet <$> toTT t1 <*> toTT t2

85+ fixBinder (NLet t1 t2) = NLet <$> toTT t1 <*> toTT t2

89− fixBinder (Hole t) = Hole <$> toTT t

86+ fixBinder (Hole t) = Hole <$> toTT t

90 fixBinder (GHole i t) = GHole i <$> toTT t

87 fixBinder (GHole i t) = GHole i <$> toTT t

91− fixBinder (Guess t1 t2) = Guess <$> toTT t1 <*> toTT t2

88+ fixBinder (Guess t1 t2) = Guess <$> toTT t1 <*> toTT t2

92− fixBinder (PVar t) = PVar <$> toTT t

89+ fixBinder (PVar t) = PVar <$> toTT t

93− fixBinder (PVTy t) = PVTy <$> toTT t

90+ fixBinder (PVTy t) = PVTy <$> toTT t

94toTT (EApp e1 e2) = do e1' <- toTT e1

91toTT (EApp e1 e2) = do e1' <- toTT e1

95 e2' <- toTT e2

92 e2' <- toTT e2

96 return $ App e1' e2'

93 return $ App e1' e2'

97toTT (EType u) = return $ TType u

94toTT (EType u) = return $ TType u

98toTT EErased = return Erased

95toTT EErased = return Erased

99toTT (EConstant c) = return (Constant c)

96toTT (EConstant c) = return (Constant c)

100−toTT (EThunk i) = return (P (DCon 0 0) (sMN i "THUNK") Erased) --(force i) >>= toTT

97+toTT (EThunk ctxt env tm) = do env' <- mapM toBinder env

98+ return $ normalise ctxt env' tm

99+ where toBinder (n, v) = do v' <- toTT v

100+ return (n, Let Erased v')

101toTT (EHandle _) = return Erased

102

103unApplyV :: ExecVal -> (ExecVal, [ExecVal])

@@ -111,7 +111,7 @@ mkEApp f (a:args) = mkEApp (EApp f a) args

111

112initState :: Idris ExecState

113initState = do ist <- getIState

114− return $ ExecState M.empty 0 (idris_implicits ist) (idris_dynamic_libs ist)

114+ return $ ExecState (idris_dynamic_libs ist)

115

116type Exec = ErrorT String (StateT ExecState IO)

117

@@ -130,45 +130,13 @@ execFail = throwError

130execIO :: IO a -> Exec a

131execIO = lift . lift

132

133−delay :: ExecEnv -> Context -> Term -> Exec ExecVal

134−delay env ctxt tm =

135− do st <- getExecState

136− let i = exec_next_thunk st

137− putExecState $ st { exec_thunks = M.insert i (Delayed env ctxt tm) (exec_thunks st)

138− , exec_next_thunk = exec_next_thunk st + 1

139− }

140− return $ EThunk i

141−

142−force :: Int -> Exec ExecVal

143−force i = do st <- getExecState

144− case M.lookup i (exec_thunks st) of

145− Just (Delayed env ctxt tm) -> do tm' <- doExec env ctxt tm

146− case tm' of

147− EThunk i ->

148− do res <- force i

149− update res i

150− return res

151− _ -> do update tm' i

152− return tm'

153− Just (Forced tm) -> return tm

154− Nothing -> execFail "Tried to exec non-existing thunk. This is a bug!"

155− where update :: ExecVal -> Int -> Exec ()

156− update tm i = do est <- getExecState

157− putExecState $ est { exec_thunks = M.insert i (Forced tm) (exec_thunks est) }

158−

159−tryForce :: ExecVal -> Exec ExecVal

160−tryForce (EThunk i) = force i

161−tryForce tm = return tm

162−

163−debugThunks :: Exec ()

164−debugThunks = do st <- getExecState

165− execIO $ putStrLn (take 4000 (show (exec_thunks st)))

166

133

167execute :: Term -> Idris Term

134execute :: Term -> Idris Term

168execute tm = do est <- initState

135execute tm = do est <- initState

169 ctxt <- getContext

136 ctxt <- getContext

170− res <- lift . lift $ flip runExec est $ do res <- doExec [] ctxt tm

137+ res <- lift . lift . flip runExec est $

138+ do res <- doExec [] ctxt tm

171− toTT res

139+ toTT res

172 case res of

140 case res of

173 Left err -> fail err

141 Left err -> fail err

174 Right tm' -> return tm'

142 Right tm' -> return tm'

@@ -208,7 +176,18 @@ doExec env ctxt (Bind n (NLet t v) body) = trace "NLet" $ undefined

208doExec env ctxt tm@(Bind n b body) = return $

176doExec env ctxt tm@(Bind n b body) = return $

209 EBind n (fmap (\_->EErased) b)

177 EBind n (fmap (\_->EErased) b)

210 (\arg -> doExec ((n, arg):env) ctxt body)

178 (\arg -> doExec ((n, arg):env) ctxt body)

211−doExec env ctxt a@(App _ _) = execApp env ctxt (unApply a)

179+doExec env ctxt a@(App _ _) =

180+ do let (f, args) = unApply a

181+ f' <- doExec env ctxt f

182+ args' <- case f' of

183+ (EP _ d _) | d == delay ->

184+ case args of

185+ [t,a,tm] -> do t' <- doExec env ctxt t

186+ a' <- doExec env ctxt a

187+ return [t', a', EThunk ctxt env tm]

188+ _ -> mapM (doExec env ctxt) args -- partial applications are fine to evaluate

189+ fun' -> do mapM (doExec env ctxt) args

190+ execApp env ctxt f' args'

212doExec env ctxt (Constant c) = return (EConstant c)

191doExec env ctxt (Constant c) = return (EConstant c)

213doExec env ctxt (Proj tm i) = let (x, xs) = unApply tm in

192doExec env ctxt (Proj tm i) = let (x, xs) = unApply tm in

214 doExec env ctxt ((x:xs) !! i)

193 doExec env ctxt ((x:xs) !! i)

@@ -216,55 +195,39 @@ doExec env ctxt Erased = return EErased

216doExec env ctxt Impossible = fail "Tried to execute an impossible case"

195doExec env ctxt Impossible = fail "Tried to execute an impossible case"

217doExec env ctxt (TType u) = return (EType u)

196doExec env ctxt (TType u) = return (EType u)

218

197

219−execApp :: ExecEnv -> Context -> (Term, [Term]) -> Exec ExecVal

198+

220−execApp env ctxt (f, args) = do newF <- doExec env ctxt f

221− laziness <- (++ repeat False) <$> (getLaziness newF)

222− newArgs <- mapM argExec (zip args laziness)

223− res <- execApp' env ctxt newF newArgs

224− return res

225− where getLaziness (EP _ l _) | l == sUN "lazy" = return [False, True]

226− getLaziness (EP _ n _) = do est <- getExecState

227− let argInfo = exec_implicits est

228− case lookupCtxtName n argInfo of

229− [] -> return (repeat False)

230− [ps] -> return $ map lazyarg (snd ps)

231− many -> execFail $ "Ambiguous " ++ show n ++ ", found " ++ (take 200 $ show many)

232− getLaziness _ = return (repeat False) -- ok due to zip above

233− argExec :: (Term, Bool) -> Exec ExecVal

234− argExec (tm, False) = doExec env ctxt tm

235− argExec (tm, True) = delay env ctxt tm

236−

237−

238−execApp' :: ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal

199+execApp :: ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal

239−execApp' env ctxt v [] = return v -- no args is just a constant! can result from function calls

200+execApp env ctxt v [] = return v -- no args is just a constant! can result from function calls

201+execApp env ctxt (EP _ f _) (t:a:delayed:rest)

202+ | f == force

203+ , (_, [_, _, EThunk tmCtxt tmEnv tm]) <- unApplyV delayed =

204+ do tm' <- doExec tmEnv tmCtxt tm

205+ execApp env ctxt tm' rest

240−execApp' env ctxt (EP _ fp _) (ty:action:rest)

206+execApp env ctxt (EP _ fp _) (ty:action:rest)

241 | fp == upio,

207 | fp == upio,

242 (prim__IO, [_, v]) <- unApplyV action

208 (prim__IO, [_, v]) <- unApplyV action

243− = execApp' env ctxt v rest

209+ = execApp env ctxt v rest

244

210

245−execApp' env ctxt (EP _ fp _) args@(_:_:v:k:rest)

211+execApp env ctxt (EP _ fp _) args@(_:_:v:k:rest)

246 | fp == piobind,

212 | fp == piobind,

247 (prim__IO, [_, v']) <- unApplyV v =

213 (prim__IO, [_, v']) <- unApplyV v =

248− do v'' <- tryForce v'

249− res <- execApp' env ctxt k [v''] >>= tryForce

214+ do res <- execApp env ctxt k [v']

250− execApp' env ctxt res rest

215+ execApp env ctxt res rest

251−execApp' env ctxt con@(EP _ fp _) args@(tp:v:rest)

216+execApp env ctxt con@(EP _ fp _) args@(tp:v:rest)

252− | fp == pioret =

253− do v' <- tryForce v

254− execApp' env ctxt (mkEApp con [tp, v']) rest

217+ | fp == pioret = execApp env ctxt (mkEApp con [tp, v]) rest

255

218

256-- Special cases arising from not having access to the C RTS in the interpreter

219-- Special cases arising from not having access to the C RTS in the interpreter

257−execApp' env ctxt (EP _ fp _) (_:fn:EConstant (Str arg):_:rest)

220+execApp env ctxt (EP _ fp _) (_:fn:EConstant (Str arg):_:rest)

258 | fp == mkfprim,

221 | fp == mkfprim,

259 Just (FFun "putStr" _ _) <- foreignFromTT fn

222 Just (FFun "putStr" _ _) <- foreignFromTT fn

260 = do execIO (putStr arg)

223 = do execIO (putStr arg)

261− execApp' env ctxt ioUnit rest

224+ execApp env ctxt ioUnit rest

262−execApp' env ctxt (EP _ fp _) (_:fn:_:EHandle h:_:rest)

225+execApp env ctxt (EP _ fp _) (_:fn:_:EHandle h:_:rest)

263 | fp == mkfprim,

226 | fp == mkfprim,

264 Just (FFun "idris_readStr" _ _) <- foreignFromTT fn

227 Just (FFun "idris_readStr" _ _) <- foreignFromTT fn

265 = do contents <- execIO $ hGetLine h

228 = do contents <- execIO $ hGetLine h

266− execApp' env ctxt (EConstant (Str (contents ++ "\n"))) rest

229+ execApp env ctxt (EConstant (Str (contents ++ "\n"))) rest

267−execApp' env ctxt (EP _ fp _) (_:fn:EConstant (Str f):EConstant (Str mode):rest)

230+execApp env ctxt (EP _ fp _) (_:fn:EConstant (Str f):EConstant (Str mode):rest)

268 | fp == mkfprim,

231 | fp == mkfprim,

269 Just (FFun "fileOpen" _ _) <- foreignFromTT fn

232 Just (FFun "fileOpen" _ _) <- foreignFromTT fn

270 = do f <- execIO $

233 = do f <- execIO $

@@ -283,53 +246,53 @@ execApp' env ctxt (EP _ fp _) (_:fn:EConstant (Str f):EConstant (Str mode):rest)

283 in return $ Right (ioWrap (EPtr nullPtr), tail rest))

246 in return $ Right (ioWrap (EPtr nullPtr), tail rest))

284 case f of

247 case f of

285 Left err -> execFail err

248 Left err -> execFail err

286− Right (res, rest) -> execApp' env ctxt res rest

249+ Right (res, rest) -> execApp env ctxt res rest

287

250

288−execApp' env ctxt (EP _ fp _) (_:fn:(EHandle h):rest)

251+execApp env ctxt (EP _ fp _) (_:fn:(EHandle h):rest)

289 | fp == mkfprim,

252 | fp == mkfprim,

290 Just (FFun "fileEOF" _ _) <- foreignFromTT fn

253 Just (FFun "fileEOF" _ _) <- foreignFromTT fn

291 = do eofp <- execIO $ hIsEOF h

254 = do eofp <- execIO $ hIsEOF h

292 let res = ioWrap (EConstant (I $ if eofp then 1 else 0))

255 let res = ioWrap (EConstant (I $ if eofp then 1 else 0))

293− execApp' env ctxt res (tail rest)

256+ execApp env ctxt res (tail rest)

294

257

295−execApp' env ctxt (EP _ fp _) (_:fn:(EHandle h):rest)

258+execApp env ctxt (EP _ fp _) (_:fn:(EHandle h):rest)

296 | fp == mkfprim,

259 | fp == mkfprim,

297 Just (FFun "fileClose" _ _) <- foreignFromTT fn

260 Just (FFun "fileClose" _ _) <- foreignFromTT fn

298 = do execIO $ hClose h

261 = do execIO $ hClose h

299− execApp' env ctxt ioUnit (tail rest)

262+ execApp env ctxt ioUnit (tail rest)

300

263

301−execApp' env ctxt (EP _ fp _) (_:fn:(EPtr p):rest)

264+execApp env ctxt (EP _ fp _) (_:fn:(EPtr p):rest)

302 | fp == mkfprim,

265 | fp == mkfprim,

303 Just (FFun "isNull" _ _) <- foreignFromTT fn

266 Just (FFun "isNull" _ _) <- foreignFromTT fn

304 = let res = ioWrap . EConstant . I $

267 = let res = ioWrap . EConstant . I $

305 if p == nullPtr then 1 else 0

268 if p == nullPtr then 1 else 0

306− in execApp' env ctxt res (tail rest)

269+ in execApp env ctxt res (tail rest)

307

270

308-- Handles will be checked as null pointers sometimes - but if we got a

271-- Handles will be checked as null pointers sometimes - but if we got a

309-- real Handle, then it's valid, so just return 1.

272-- real Handle, then it's valid, so just return 1.

310−execApp' env ctxt (EP _ fp _) (_:fn:(EHandle h):rest)

273+execApp env ctxt (EP _ fp _) (_:fn:(EHandle h):rest)

311 | fp == mkfprim,

274 | fp == mkfprim,

312 Just (FFun "isNull" _ _) <- foreignFromTT fn

275 Just (FFun "isNull" _ _) <- foreignFromTT fn

313 = let res = ioWrap . EConstant . I $ 0

276 = let res = ioWrap . EConstant . I $ 0

314− in execApp' env ctxt res (tail rest)

277+ in execApp env ctxt res (tail rest)

315

278

316-- A foreign-returned char* has to be tested for NULL sometimes

279-- A foreign-returned char* has to be tested for NULL sometimes

317−execApp' env ctxt (EP _ fp _) (_:fn:EConstant (Str s):rest)

280+execApp env ctxt (EP _ fp _) (_:fn:EConstant (Str s):rest)

318 | fp == mkfprim,

281 | fp == mkfprim,

319 Just (FFun "isNull" _ _) <- foreignFromTT fn

282 Just (FFun "isNull" _ _) <- foreignFromTT fn

320 = let res = ioWrap . EConstant . I $ 0

283 = let res = ioWrap . EConstant . I $ 0

321− in execApp' env ctxt res (tail rest)

284+ in execApp env ctxt res (tail rest)

322

285

323-- Right now, there's no way to send command-line arguments to the executor,

286-- Right now, there's no way to send command-line arguments to the executor,

324-- so just return 0.

287-- so just return 0.

325−execApp' env ctxt (EP _ fp _) (_:fn:rest)

288+execApp env ctxt (EP _ fp _) (_:fn:rest)

326 | fp == mkfprim,

289 | fp == mkfprim,

327 Just (FFun "idris_numArgs" _ _) <- foreignFromTT fn

290 Just (FFun "idris_numArgs" _ _) <- foreignFromTT fn

328 = let res = ioWrap . EConstant . I $ 0

291 = let res = ioWrap . EConstant . I $ 0

329− in execApp' env ctxt res (tail rest)

292+ in execApp env ctxt res (tail rest)

330-- Throw away the 'World' argument to the foreign function

293-- Throw away the 'World' argument to the foreign function

331

294

332−execApp' env ctxt f@(EP _ fp _) args@(ty:fn:xs) | fp == mkfprim

295+execApp env ctxt f@(EP _ fp _) args@(ty:fn:xs) | fp == mkfprim

333 = case foreignFromTT fn of

296 = case foreignFromTT fn of

334 Just (FFun f argTs retT) | length xs >= length argTs ->

297 Just (FFun f argTs retT) | length xs >= length argTs ->

335 do let (args', xs') = (take (length argTs) xs, -- foreign args

298 do let (args', xs') = (take (length argTs) xs, -- foreign args

@@ -341,43 +304,41 @@ execApp' env ctxt f@(EP _ fp _) args@(ty:fn:xs) | fp == mkfprim

341 Just r -> return (mkEApp r xs')

304 Just r -> return (mkEApp r xs')

342 Nothing -> return (mkEApp f args)

305 Nothing -> return (mkEApp f args)

343

306

344−execApp' env ctxt c@(EP (DCon _ arity) n _) args =

307+execApp env ctxt c@(EP (DCon _ arity) n _) args =

345− do args' <- mapM tryForce (take arity args)

308+ do let args' = take arity args

346 let restArgs = drop arity args

309 let restArgs = drop arity args

347− execApp' env ctxt (mkEApp c args') restArgs

310+ execApp env ctxt (mkEApp c args') restArgs

348

311

349−execApp' env ctxt c@(EP (TCon _ arity) n _) args =

312+execApp env ctxt c@(EP (TCon _ arity) n _) args =

350− do args' <- mapM tryForce (take arity args)

313+ do let args' = take arity args

351 let restArgs = drop arity args

314 let restArgs = drop arity args

352− execApp' env ctxt (mkEApp c args') restArgs

315+ execApp env ctxt (mkEApp c args') restArgs

353

316

354−execApp' env ctxt f@(EP _ n _) args =

317+execApp env ctxt f@(EP _ n _) args =

355 do let val = lookupDef n ctxt

318 do let val = lookupDef n ctxt

356 case val of

319 case val of

357 [Function _ tm] -> fail "should already have been eval'd"

320 [Function _ tm] -> fail "should already have been eval'd"

358 [TyDecl nt ty] -> return $ mkEApp f args

321 [TyDecl nt ty] -> return $ mkEApp f args

359 [Operator tp arity op] ->

322 [Operator tp arity op] ->

360 if length args >= arity

323 if length args >= arity

361− then do args' <- mapM tryForce $ take arity args

324+ then let args' = take arity args in

362− case getOp n args' of

325+ case getOp n args' of

363− Just res -> do r <- res

326+ Just res -> do r <- res

364− execApp' env ctxt r (drop arity args)

327+ execApp env ctxt r (drop arity args)

365− Nothing -> return (mkEApp f args)

328+ Nothing -> return (mkEApp f args)

366 else return (mkEApp f args)

329 else return (mkEApp f args)

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

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

368 do rhs <- doExec env ctxt tm

331 do rhs <- doExec env ctxt tm

369− execApp' env ctxt rhs args

332+ execApp env ctxt rhs args

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

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

371 do res <- execCase env ctxt ns sc args

334 do res <- execCase env ctxt ns sc args

372 return $ fromMaybe (mkEApp f args) res

335 return $ fromMaybe (mkEApp f args) res

373 thing -> return $ mkEApp f args

336 thing -> return $ mkEApp f args

374−execApp' env ctxt bnd@(EBind n b body) (arg:args) = do ret <- body arg

337+execApp env ctxt bnd@(EBind n b body) (arg:args) = do ret <- body arg

375− let (f', as) = unApplyV ret

338+ let (f', as) = unApplyV ret

376− execApp' env ctxt f' (as ++ args)

339+ execApp env ctxt f' (as ++ args)

377−execApp' env ctxt (EThunk i) args = do f <- force i

378− execApp' env ctxt f args

379−execApp' env ctxt app@(EApp _ _) args2 | (f, args1) <- unApplyV app = execApp' env ctxt f (args1 ++ args2)

340+execApp env ctxt app@(EApp _ _) args2 | (f, args1) <- unApplyV app = execApp env ctxt f (args1 ++ args2)

380−execApp' env ctxt f args = return (mkEApp f args)

341+execApp env ctxt f args = return (mkEApp f args)

381

342

382prs = sUN "prim__readString"

343prs = sUN "prim__readString"

383pbm = sUN "prim__believe_me"

344pbm = sUN "prim__believe_me"

@@ -386,6 +347,8 @@ mkfprim = sUN "mkForeignPrim"

386pioret = sUN "prim_io_return"

347pioret = sUN "prim_io_return"

387piobind = sUN "prim_io_bind"

348piobind = sUN "prim_io_bind"

388upio = sUN "unsafePerformPrimIO"

349upio = sUN "unsafePerformPrimIO"

350+delay = sUN "Delay"

351+force = sUN "Force"

389

352

390-- | Look up primitive operations in the global table and transform them into ExecVal functions

353-- | Look up primitive operations in the global table and transform them into ExecVal functions

391getOp :: Name -> [ExecVal] -> Maybe (Exec ExecVal)

354getOp :: Name -> [ExecVal] -> Maybe (Exec ExecVal)

@@ -426,7 +389,7 @@ execCase env ctxt ns sc args =

426-- trace ("Case " ++ show sc ++ "\n in " ++ show amap ++"\n in env " ++ show env ++ "\n\n" ) $ return ()

389-- trace ("Case " ++ show sc ++ "\n in " ++ show amap ++"\n in env " ++ show env ++ "\n\n" ) $ return ()

427 caseRes <- execCase' env ctxt amap sc

390 caseRes <- execCase' env ctxt amap sc

428 case caseRes of

391 case caseRes of

429− Just res -> Just <$> execApp' (map (\(n, tm) -> (n, tm)) amap ++ env) ctxt res (drop arity args)

392+ Just res -> Just <$> execApp (map (\(n, tm) -> (n, tm)) amap ++ env) ctxt res (drop arity args)

430 Nothing -> return Nothing

393 Nothing -> return Nothing

431 else return Nothing

394 else return Nothing

432

395

@@ -436,8 +399,7 @@ execCase' env ctxt amap (UnmatchedCase _) = return Nothing

436execCase' env ctxt amap (STerm tm) =

399execCase' env ctxt amap (STerm tm) =

437 Just <$> doExec (map (\(n, v) -> (n, v)) amap ++ env) ctxt tm

400 Just <$> doExec (map (\(n, v) -> (n, v)) amap ++ env) ctxt tm

438execCase' env ctxt amap (Case n alts) | Just tm <- lookup n amap =

401execCase' env ctxt amap (Case n alts) | Just tm <- lookup n amap =

439− do tm' <- tryForce tm

440− case chooseAlt tm' alts of

402+ case chooseAlt tm alts of

441 Just (newCase, newBindings) ->

403 Just (newCase, newBindings) ->

442 let amap' = newBindings ++ (filter (\(x,_) -> not (elem x (map fst newBindings))) amap) in

404 let amap' = newBindings ++ (filter (\(x,_) -> not (elem x (map fst newBindings))) amap) in

443 execCase' env ctxt amap' newCase

405 execCase' env ctxt amap' newCase

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

73 -- suggests)

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

277 rnf (PImp x1 x2 x3 x4 x5)

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

279− rnf (PExp x1 x2 x3)

279+ rnf (PExp x1 x2 x3 x4)

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

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

281− rnf (PConstraint x1 x2 x3)

281+ rnf (PConstraint x1 x2 x3 x4)

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

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

283 rnf (PTacImplicit x1 x2 x3 x4 x5)

284 = rnf x1 `seq`

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

src/Idris/Delaborate.hs+3−3

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

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

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

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

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

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

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

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

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

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

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

122

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

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

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

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

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

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

127

128-- | How far to indent sub-errors

src/Idris/ElabDecls.hs+50−31

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

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

84 ty' <- addUsingConstraints syn fc ty'

85− ty' <- implicit syn n ty'

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

87 let ty = addImpl i 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

205 ctxt <- getContext

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

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

28import Debug.Trace

29import Debug.Trace

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)

31ibcVersion :: Word8

32−ibcVersion = 65

32+ibcVersion = 66

34data IBCFile = IBCFile { ver :: Word8,

35 sourcefile :: FilePath,

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

2037 put x3

2038 put x4

2039 put x5

2040− PExp x1 x2 x3 ->

2040+ PExp x1 x2 x3 x4 ->

2041 do putWord8 1

2042 put x1

2043 put x2

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/IdeSlave.hs+2

@@ -151,6 +151,7 @@ data IdeSlaveCommand = REPLCompletions String

151 | Apropos String

152 | GetOpts

153 | SetOpt Opt Bool

154+ | Metavariables Int -- ^^ the Int is the column count for pretty-printing

154 deriving Show

155 deriving Show

155

156

156sexpToCommand :: SExp -> Maybe IdeSlaveCommand

157sexpToCommand :: SExp -> Maybe IdeSlaveCommand

@@ -174,6 +175,7 @@ sexpToCommand (SymbolAtom "get-options")

174sexpToCommand (SexpList [SymbolAtom "set-option", SymbolAtom s, BoolAtom b])

175sexpToCommand (SexpList [SymbolAtom "set-option", SymbolAtom s, BoolAtom b])

175 | Just opt <- lookup s opts = Just (SetOpt opt b)

176 | Just opt <- lookup s opts = Just (SetOpt opt b)

176 where opts = [("show-implicits", ShowImpl), ("error-context", ErrContext)] --TODO support more

177 where opts = [("show-implicits", ShowImpl), ("error-context", ErrContext)] --TODO support more

178+sexpToCommand (SexpList [SymbolAtom "metavariables", IntegerAtom cols]) = Just (Metavariables (fromIntegral cols))

177sexpToCommand _ = Nothing

179sexpToCommand _ = Nothing

178

180

179parseMessage :: String -> Either Err (SExp, Integer)

181parseMessage :: String -> Either Err (SExp, Integer)

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

151 Just (SynTm t) -> t

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+9−3

@@ -17,14 +17,15 @@ import qualified Text.Parser.Char as Chr

17import qualified Text.Parser.Token.Highlight as Hi

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

20+import qualified Text.PrettyPrint.ANSI.Leijen as ANSI

21−import Idris.AbsSyntax

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

22import Idris.DSL

23import Idris.DSL

23import Idris.Imports

24import Idris.Imports

24import Idris.Delaborate

25import Idris.Delaborate

25import Idris.Error

26import Idris.Error

26import Idris.ElabDecls

27import Idris.ElabDecls

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

28+import Idris.ElabTerm

28import Idris.Coverage

29import Idris.Coverage

29import Idris.IBC

30import Idris.IBC

30import Idris.Unlit

31import Idris.Unlit

@@ -1120,6 +1121,11 @@ findFC x = let s = show (plain x) in

1120 (col, ':':msg) -> let pos = (read line, read col) in

1121 (col, ':':msg) -> let pos = (read line, read col) in

1121 (FC failname pos pos, msg)

1122 (FC failname pos pos, msg)

1122

1123

1124+-- | Check if the coloring matches the options and corrects if necessary

1125+fixColour :: Bool -> ANSI.Doc -> ANSI.Doc

1126+fixColour False doc = ANSI.plain doc

1127+fixColour True doc = doc

1128+

1123-- | A program is a list of declarations, possibly with associated

1129-- | A program is a list of declarations, possibly with associated

1124-- documentation strings.

1130-- documentation strings.

1125parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta ->

1131parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta ->

@@ -1132,7 +1138,7 @@ parseProg syn fname input mrk

1132 let (fc, msg) = findFC doc

1138 let (fc, msg) = findFC doc

1133 i <- getIState

1139 i <- getIState

1134 case idris_outputmode i of

1140 case idris_outputmode i of

1135− RawOutput -> ihputStrLn (idris_outh i) (show doc)

1141+ RawOutput -> ihputStrLn (idris_outh i) (show $ fixColour (idris_colourRepl i) doc)

1136 IdeSlave n -> ihWarn (idris_outh i) fc (P.text msg)

1142 IdeSlave n -> ihWarn (idris_outh i) fc (P.text msg)

1137 putIState (i { errSpan = Just fc })

1143 putIState (i { errSpan = Just fc })

1138 return []

1144 return []

src/Idris/PartialEval.hs+1−1

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

124 | imparg imp = (ImplicitD, tm)

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

126

127− imparg (PExp _ _ _) = False

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

128 imparg _ = True

129

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

src/Idris/Providers.hs+2−1

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

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

13providerTy :: FC -> PTerm -> PTerm

14+providerTy fc tm

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

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

16ioret = sUN "prim_io_return"

17ioret = sUN "prim_io_return"

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

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

src/Idris/REPL.hs+58−31

@@ -13,7 +13,7 @@ import Idris.ErrReverse

13import Idris.Delaborate

14import Idris.Docstrings (Docstring, overview, renderDocstring)

15import Idris.Prover

16−import Idris.Parser

16+import Idris.Parser hiding (indent)

17import Idris.Primitives

18import Idris.Coverage

19import Idris.UnusedArgs

@@ -79,8 +79,6 @@ import Data.Version

79import Data.Word (Word)

80import Control.DeepSeq

82−import qualified Text.PrettyPrint.ANSI.Leijen as ANSI

83−

84import Debug.Trace

82import Debug.Trace

86-- | Run the REPL

84-- | Run the REPL

@@ -286,6 +284,16 @@ ideslave orig mods

286 do setErrContext b

284 do setErrContext b

287 let msg = (IdeSlave.SymbolAtom "ok", b)

285 let msg = (IdeSlave.SymbolAtom "ok", b)

288 runIO . putStrLn $ IdeSlave.convSExp "return" msg id

286 runIO . putStrLn $ IdeSlave.convSExp "return" msg id

287+ Just (IdeSlave.Metavariables cols) ->

288+ do ist <- getIState

289+ let mvs = reverse $ map fst (idris_metavars ist) \\ primDefs

290+ imp <- impShow

291+ let mvarTys = map (delabTy ist) mvs

292+ let res = (IdeSlave.SymbolAtom "ok",

293+ zipWith (\ n (prems, concl) -> (n, prems, concl))

294+ (map (IdeSlave.StringAtom . show) mvs)

295+ (map (sexpGoal ist cols imp [] . getGoal) mvarTys))

296+ runIO . putStrLn $ IdeSlave.convSExp "return" res id

289 Nothing -> do iPrintError "did not understand")

297 Nothing -> do iPrintError "did not understand")

290 (\e -> do iPrintError $ show e))

298 (\e -> do iPrintError $ show e))

291 (\e -> do iPrintError $ show e)

299 (\e -> do iPrintError $ show e)

@@ -295,6 +303,27 @@ ideslave orig mods

295 [] -> Left ("Didn't understand name '" ++ s ++ "'")

303 [] -> Left ("Didn't understand name '" ++ s ++ "'")

296 [n] -> Right $ sUN n

304 [n] -> Right $ sUN n

297 (n:ns) -> Right $ sNS (sUN n) ns

305 (n:ns) -> Right $ sNS (sUN n) ns

306+ getGoal :: PTerm -> ([(Name, PTerm)], PTerm)

307+ getGoal (PPi _ n t sc) = let (prems, conc) = getGoal sc

308+ in ((n, t):prems, conc)

309+ getGoal tm = ([], tm)

310+ sexpGoal :: IState -> Int -> Bool -> [Name] -> ([(Name, PTerm)], PTerm)

311+ -> ([(String, String, SpanList OutputAnnotation)],

312+ (String, SpanList OutputAnnotation))

313+ sexpGoal ist cols imp ns ([], concl) =

314+ let concl' = displaySpans . renderPretty 0.9 cols . fmap (fancifyAnnots ist) $

315+ pprintPTerm imp (zip ns (repeat False)) [] concl

316+ in ([], concl')

317+ sexpGoal ist cols imp ns ((n, t):ps, concl) =

318+ let n' = case n of

319+ NS (UN nm) ns -> str nm

320+ UN nm | ('_':'_':_) <- str nm -> "_"

321+ | otherwise -> str nm

322+ _ -> "_"

323+ (t', spans) = displaySpans . renderPretty 0.9 cols . fmap (fancifyAnnots ist) $

324+ pprintPTerm imp (zip ns (repeat False)) [] t

325+ rest = sexpGoal ist cols imp (n:ns) (ps, concl)

326+ in ((n', t', spans) : fst rest, snd rest)

298

327

299ideslaveProcess :: FilePath -> Command -> Idris ()

328ideslaveProcess :: FilePath -> Command -> Idris ()

300ideslaveProcess fn Help = process stdout fn Help

329ideslaveProcess fn Help = process stdout fn Help

@@ -617,7 +646,8 @@ process h fn (DebugInfo n)

617process h fn (Info n)

646process h fn (Info n)

618 = do i <- getIState

647 = do i <- getIState

619 case lookupCtxt n (idris_classes i) of

648 case lookupCtxt n (idris_classes i) of

620− [c] -> classInfo c

649+ [c] -> do info <- classInfo c

650+ ihRenderResult h info

621 _ -> iPrintError "Not a class"

651 _ -> iPrintError "Not a class"

622process h fn (Search t) = iPrintError "Not implemented"

652process h fn (Search t) = iPrintError "Not implemented"

623-- FIXME: There is far too much repetition in the cases below!

653-- FIXME: There is far too much repetition in the cases below!

@@ -993,28 +1023,30 @@ process h fn (Apropos a) =

993 isUN (NS n _) = isUN n

1023 isUN (NS n _) = isUN n

994 isUN _ = False

1024 isUN _ = False

995

1025

996−classInfo :: ClassInfo -> Idris ()

1026+classInfo :: ClassInfo -> Idris (Doc OutputAnnotation)

997−classInfo ci = do iputStrLn "Methods:\n"

1027+classInfo ci = do ist <- getIState

1028+ ctxt <- getContext

1029+ return $

1030+ text "Parameters:" <+>

1031+ hsep (punctuate comma (map (prettyName False params') params)) <>

1032+ line <> line <>

1033+ text "Methods:" <> line <>

998− mapM_ dumpMethod (class_methods ci)

1034+ indent 2 (vsep (map (dumpMethod ist) (class_methods ci))) <> line <> line <>

999− iputStrLn ""

1000− iputStrLn "Default superclass instances:\n"

1035+ text "Default superclass instances:" <>

1036+ line <>

1001− mapM_ dumpDefaultInstance (class_default_superclasses ci)

1037+ indent 2 (vsep (map (dumpDefaultInstance ist) (class_default_superclasses ci))) <>

1002− iputStrLn ""

1038+ line <>

1003− iputStrLn "Instances:\n"

1039+ text "Instances:" <> line <>

1004− mapM_ dumpInstance (class_instances ci)

1040+ indent 2 (vsep (map (dumpInstance ist ctxt) (class_instances ci)))

1005− iPrintResult ""

1006−

1007−dumpMethod :: (Name, (FnOpts, PTerm)) -> Idris ()

1041+ where dumpMethod :: IState -> (Name, (FnOpts, PTerm)) -> Doc OutputAnnotation

1008−dumpMethod (n, (_, t)) = iputStrLn $ show n ++ " : " ++ show t

1042+ dumpMethod ist (n, (_, t)) = prettyName False [] n <+> colon <+> pp ist t

1009−

1010−dumpDefaultInstance :: PDecl -> Idris ()

1043+ dumpDefaultInstance :: IState -> PDecl -> Doc OutputAnnotation

1011−dumpDefaultInstance (PInstance _ _ _ _ _ t _ _) = iputStrLn $ show t

1044+ dumpDefaultInstance ist (PInstance _ _ _ _ _ t _ _) = pp ist t

1012−

1013−dumpInstance :: Name -> Idris ()

1045+ dumpInstance :: IState -> Context -> Name -> Doc OutputAnnotation

1014−dumpInstance n = do i <- getIState

1046+ dumpInstance ist ctxt n = pp ist $ delabTy ist n

1015− ctxt <- getContext

1047+ params = class_params ci

1016− case lookupTy n ctxt of

1048+ params' = zip params (repeat False)

1017− ts -> mapM_ (\t -> iputStrLn $ showTm i (delab i t)) ts

1049+ pp ist = pprintPTerm (opt_showimp (idris_options ist)) params' []

1018

1050

1019showTotal :: Totality -> IState -> String

1051showTotal :: Totality -> IState -> String

1020showTotal t@(Partial (Other ns)) i

1052showTotal t@(Partial (Other ns)) i

@@ -1349,11 +1381,6 @@ execScript expr = do i <- getIState

1349 res <- execute tm

1381 res <- execute tm

1350 runIO $ exitWith ExitSuccess

1382 runIO $ exitWith ExitSuccess

1351

1383

1352−-- | Check if the coloring matches the options and corrects if necessary

1353−fixColour :: Bool -> ANSI.Doc -> ANSI.Doc

1354−fixColour False doc = ANSI.plain doc

1355−fixColour True doc = doc

1356−

1357-- | Get the platform-specific, user-specific Idris dir

1384-- | Get the platform-specific, user-specific Idris dir

1358getIdrisUserDataDir :: Idris FilePath

1385getIdrisUserDataDir :: Idris FilePath

1359getIdrisUserDataDir = runIO $ getAppUserDataDirectory "idris"

1386getIdrisUserDataDir = runIO $ getAppUserDataDirectory "idris"

test/proof005/DefaultArgSubstitutionSuccess.idrnew file+44

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

1+module DefaultArgSubstitutionSuccess

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

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

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

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

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

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

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

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

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

test/reg039/expectednew file+2

@@ -0,0 +1,2 @@

1+Type checking ./reg039.idr

2+[3, 2, 1]

test/reg039/reg039.idrnew file+12

@@ -0,0 +1,12 @@

1+module LazyExec

3+-- The regression that this tests for is broken laziness in the executor.

5+covering

6+countdown : Int -> Lazy (List Int)

7+countdown n = if n > 0

8+ then (n :: countdown (n-1))

9+ else []

10+

11+go : IO ()

12+go = putStrLn $ show (Force (countdown 3))

test/reg039/runnew file+26

@@ -0,0 +1,26 @@

1+#!/usr/bin/env bash

3+# From http://unix.stackexchange.com/questions/43340/how-to-introduce-timeout-for-shell-scripting

4+# Executes command with a timeout

5+# Params:

6+# $1 timeout in seconds

7+# $2 command

8+# Returns 1 if timed out 0 otherwise

9+timeout() {

10+

11+ time=$1

12+

13+ # start the command in a subshell to avoid problem with pipes

14+ # (spawn accepts one command)

15+ command="/bin/sh -c \"$2\""

16+

17+ expect -c "set echo \"-noecho\"; set timeout $time; spawn -noecho $command; expect timeout { exit 1 } eof { exit 0 }"

18+

19+ if [ $? = 1 ] ; then

20+ echo "Timeout after ${time} seconds"

21+ fi

22+

23+}

24+

25+timeout 60 "idris $@ --nocolour reg039.idr --exec go"

26+rm -f reg039 *.ibc