ad057db · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

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

commitad057dba2acd7560fdaf1a0296f70d13ddc3bc81 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 9 Apr 2014, 22:03 (13 years ago) parente707475 22d4f7e

31 files changed+528−288

compare with master

unifiedsplit

.travis.yml+2 CHANGELOG+4 libs/base/Control/Arrow.idr+1−2 libs/base/Control/Catchable.idr+1−1 src/Idris/AbsSyntax.hs+69−34 src/Idris/AbsSyntaxTree.hs+45−16 src/Idris/Core/Execute.hs+97−135 src/Idris/Coverage.hs+3−2 src/Idris/DeepSeq.hs+4−4 src/Idris/Delaborate.hs+3−3 src/Idris/ElabDecls.hs+50−31 src/Idris/ElabTerm.hs+2−11 src/Idris/IBC.hs+9−5 src/Idris/IdeSlave.hs+2 src/Idris/ParseExpr.hs+19−8 src/Idris/Parser.hs+9−3 src/Idris/PartialEval.hs+1−1 src/Idris/Providers.hs+2−1 src/Idris/REPL.hs+58−31 test/proof005/DefaultArgSubstitutionSuccess.idr+44 test/proof005/expected test/proof005/run+3 test/proof006/DefaultArgSubstitutionSyntax.idr+49 test/proof006/expected test/proof006/run+3 test/proof007/DefaultArgUnknownName.idr+4 test/proof007/expected+1 test/proof007/run+3 test/reg039/expected+2 test/reg039/reg039.idr+12 test/reg039/run+26

.travis.yml+2

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

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

77 # trifecta dependencies

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

911install:

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

1113before_script:

CHANGELOG+4

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

1+New in 0.9.13:

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

3+* IDE support for retrieving structured information about metavariables

15New in 0.9.12:

26--------------

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

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

1−module Category.Arrow

1+module Control.Arrow

33import Data.Morphisms

44import Control.Category

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

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

3838 y <- g a

3939 return (x, y)

40−

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

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

1−module Prelude.Catchable

1+module Control.Catchable

33import Control.IOExcept

src/Idris/AbsSyntax.hs+69−34

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

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

820820 en (PPi p n t s)

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

822− = let n' = mkShadow n in

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

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

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

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

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

825825 en (PLet n ty v s)

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

827827 = let n' = mkShadow n in

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

880880

881881 nseq x y = nsroot x == nsroot y

882882

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

884+ enTacImp other = other

885+

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

884887 IState ->

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

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

10761079 | otherwise = doAdd cs ns t

10771080

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

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

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

10801083

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

10821085 = getcapp c ++ getConstraints sc

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

10881091 return (UConstraint c ns)

10891092 getcapp _ = []

10901093

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

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

10921095 getName _ = []

10931096

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

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

10961099

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

10981101

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

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

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

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

11011104

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

1103−implicit' syn ignore n ptm

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

1106+implicit' info syn ignore n ptm

11041107 = do i <- getIState

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

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

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

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

11081112 addIBC (IBCImp n)

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

11101114-- i <- get

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

11121116 return tm'

1117+ where

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

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

1120+ defaultArgCheck knowns params = foldM_ notFoundInDefault knowns params

1121+

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

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

1124+ = do i <- getIState

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

1126+ Nothing -> return (n:kns)

1127+ Just name -> throwError (NoSuchVariable name)

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

1129+

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

1131+ notFound kns [] = Nothing

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

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

11131134

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

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

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

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

11561177 _ -> [])

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

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

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

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

11601181 imps True (n:env) sc

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

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

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

11641185 _ -> [])

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

1166− put (PConstraint 10 l Placeholder : decls,

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

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

11681189 imps True (n:env) sc

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

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

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

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

13311352 else Right $ PPatvar fc f

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

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

13331354 imp _ = True

13341355-- allImp [] = False

13351356 allImp xs = all imp xs

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

13761397 [(n,t)] -> t

13771398 _ -> Public

13781399

1379−

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

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

1382− PExp p l tm : insertImpl ps given

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

1384− PConstraint p l tm : insertImpl ps given

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

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

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

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

1402+

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

1404+ -> [PArg] -- parameters

1405+ -> [PArg] -- arguments

1406+ -> [PArg]

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

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

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

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

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

1412+ let rtc = PResolveTC fc in

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

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

13881415 case find n given [] of

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

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

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

1392− let sc = addImpl ist sc' in

1416+ Just (tm, given') ->

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

1418+ Nothing ->

1419+ PImp p True l n Placeholder :

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

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

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

13931423 case find n given [] of

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

1395− Nothing -> if inpat

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

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

1398− insertImpl expected [] = []

1399− insertImpl _ given = given

1424+ Just (tm, given') ->

1425+ PTacImplicit p l n sc tm :

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

1427+ Nothing ->

1428+ if inpat

1429+ then PTacImplicit p l n sc Placeholder :

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

1431+ else PTacImplicit p l n sc sc :

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

1433+ insImpAcc _ expected [] = []

1434+ insImpAcc _ _ given = given

14001435

14011436 find n [] acc = Nothing

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

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

14331468 return $ PApp fc fn args'

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

14351470 return $ PImp p m l n t'

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

1437− return $ PExp p l t'

1438− slA (PConstraint p l t)

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

1472+ return $ PExp p l n t'

1473+ slA (PConstraint p l n t)

14391474 = do t' <- sl t

1440− return $ PConstraint p l t'

1475+ return $ PConstraint p l n t'

14411476 slA (PTacImplicit p l n sc t)

14421477 = do t' <- sl t

14431478 return $ PTacImplicit p l n sc t'

src/Idris/AbsSyntaxTree.hs+45−16

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

3636

3737import Text.PrettyPrint.Annotated.Leijen

3838

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

40+-- paramaterised declarations, etc.

41+

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

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

44+ liftname :: Name -> Name,

45+ namespace :: Maybe [String] }

46+

47+toplevel = EInfo [] emptyContext id Nothing

48+

49+eInfoNames :: ElabInfo -> [Name]

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

51+

3952data IOption = IOption { opt_logLevel :: Int,

4053 opt_typecase :: Bool,

4154 opt_typeintype :: Bool,

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

767780 pname :: Name, getTm :: t }

768781 | PExp { priority :: Int,

769782 argopts :: [ArgOpt],

783+ pname :: Name,

770784 getTm :: t }

771785 | PConstraint { priority :: Int,

772786 argopts :: [ArgOpt],

787+ pname :: Name,

773788 getTm :: t }

774789 | PTacImplicit { priority :: Int,

775790 argopts :: [ArgOpt],

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

786801

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

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

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

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

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

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

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

792807

793808{-!

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

796811!-}

797812

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

799−pexp t = PExp 1 [] t

800−pconst t = PConstraint 1 [] t

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

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

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

802817

803818type PArg = PArg' PTerm

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

12551270 prettySe p bnd _ = text "test"

12561271

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

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

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

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

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

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

12611276

12621277 prettyArgSe bnd arg = prettySe 0 bnd arg

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

13881403

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

13901405getExps [] = []

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

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

13921407getExps (_ : xs) = getExps xs

13931408

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

13951410getConsts [] = []

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

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

13971412getConsts (_ : xs) = getConsts xs

13981413

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

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

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

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

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

14361453

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

14381455showTmImpls :: PTerm -> String

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

14811498

14821499allNamesIn :: PTerm -> [Name]

14831500allNamesIn tm = nub $ ni [] tm

1484− where

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

14851502 ni env (PRef _ n)

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

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

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

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

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

14911508 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

14931510 ni env (PHidden tm) = ni env tm

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

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

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

15031520 ni env (PNoImplicits tm) = ni env tm

15041521 ni env _ = []

15051522

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

1524+ niTacImp _ _ = []

1525+

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

15071527boundNamesIn :: PTerm -> [Name]

15081528boundNamesIn tm = nub $ ni tm

1509− where

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

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

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

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

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

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

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

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

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

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

15261546 ni (PNoImplicits tm) = ni tm

15271547 ni _ = []

15281548

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

1550+ niTacImp _ = []

1551+

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

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

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

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

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

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

15411564 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

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

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

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

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

15531576 ni env (PNoImplicits tm) = ni env tm

15541577 ni env _ = []

15551578

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

1580+ niTacImp _ _ = []

1581+

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

15571583

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

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

1560− where

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

15611587 ni env (PRef _ n)

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

15631589 = case lookupTy n (tt_ctxt ist) of

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

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

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

15691595 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

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

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

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

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

15811607 ni env (PNoImplicits tm) = ni env tm

15821608 ni env _ = []

15831609

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

4747

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

4949

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

54− }

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

51+ }

5552

5653data ExecVal = EP NameType Name ExecVal

5754 | EV Int

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

6158 | EErased

6259 | EConstant Const

6360 | forall a. EPtr (Ptr a)

64− | EThunk Int

61+ | EThunk Context ExecEnv Term

6562 | EHandle Handle

6663

6764instance Show ExecVal where

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

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

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

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

72− show (EType _) = "Type"

73− show EErased = "[__]"

74− show (EConstant c) = show c

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

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

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

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

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

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

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

69+ show (EType _) = "Type"

70+ show EErased = "[__]"

71+ show (EConstant c) = show c

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

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

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

7875

7976toTT :: ExecVal -> Exec Term

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

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

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

8380 b' <- fixBinder b

8481 Bind n b' <$> toTT body'

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

9592 e2' <- toTT e2

9693 return $ App e1' e2'

9794toTT (EType u) = return $ TType u

9895toTT EErased = return Erased

9996toTT (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')

101101toTT (EHandle _) = return Erased

102102

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

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

111111

112112initState :: Idris ExecState

113113initState = do ist <- getIState

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

114+ return $ ExecState (idris_dynamic_libs ist)

115115

116116type Exec = ErrorT String (StateT ExecState IO)

117117

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

130130execIO :: IO a -> Exec a

131131execIO = lift . lift

132132

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

166133

167134execute :: Term -> Idris Term

168135execute tm = do est <- initState

169136 ctxt <- getContext

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

171− toTT res

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

138+ do res <- doExec [] ctxt tm

139+ toTT res

172140 case res of

173141 Left err -> fail err

174142 Right tm' -> return tm'

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

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

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

210178 (\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'

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

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

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

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

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

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

218197

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

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

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

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

198+

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

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

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

241207 | fp == upio,

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

243− = execApp' env ctxt v rest

209+ = execApp env ctxt v rest

244210

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

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

246212 | fp == piobind,

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

248− do v'' <- tryForce v'

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

250− execApp' env ctxt res rest

251−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

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

215+ execApp env ctxt res rest

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

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

255218

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

258221 | fp == mkfprim,

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

260223 = do execIO (putStr arg)

261− execApp' env ctxt ioUnit rest

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

224+ execApp env ctxt ioUnit rest

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

263226 | fp == mkfprim,

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

265228 = do contents <- execIO $ hGetLine h

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

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

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

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

268231 | fp == mkfprim,

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

270233 = do f <- execIO $

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

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

284247 case f of

285248 Left err -> execFail err

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

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

287250

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

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

289252 | fp == mkfprim,

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

291254 = do eofp <- execIO $ hIsEOF h

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

294257

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

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

296259 | fp == mkfprim,

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

298261 = do execIO $ hClose h

299− execApp' env ctxt ioUnit (tail rest)

262+ execApp env ctxt ioUnit (tail rest)

300263

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

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

302265 | fp == mkfprim,

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

304267 = let res = ioWrap . EConstant . I $

305268 if p == nullPtr then 1 else 0

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

269+ in execApp env ctxt res (tail rest)

307270

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

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

311274 | fp == mkfprim,

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

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

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

277+ in execApp env ctxt res (tail rest)

315278

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

318281 | fp == mkfprim,

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

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

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

284+ in execApp env ctxt res (tail rest)

322285

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

324287-- so just return 0.

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

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

326289 | fp == mkfprim,

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

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

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

292+ in execApp env ctxt res (tail rest)

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

331294

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

333296 = case foreignFromTT fn of

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

335298 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

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

342305 Nothing -> return (mkEApp f args)

343306

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

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

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

308+ do let args' = take arity args

346309 let restArgs = drop arity args

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

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

348311

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

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

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

313+ do let args' = take arity args

351314 let restArgs = drop arity args

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

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

353316

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

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

355318 do let val = lookupDef n ctxt

356319 case val of

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

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

359322 [Operator tp arity op] ->

360323 if length args >= arity

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

362− case getOp n args' of

363− Just res -> do r <- res

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

365− Nothing -> return (mkEApp f args)

324+ then let args' = take arity args in

325+ case getOp n args' of

326+ Just res -> do r <- res

327+ execApp env ctxt r (drop arity args)

328+ Nothing -> return (mkEApp f args)

366329 else return (mkEApp f args)

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

368331 do rhs <- doExec env ctxt tm

369− execApp' env ctxt rhs args

332+ execApp env ctxt rhs args

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

371334 do res <- execCase env ctxt ns sc args

372335 return $ fromMaybe (mkEApp f args) res

373336 thing -> return $ mkEApp f args

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

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

376− 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)

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

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

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

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

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

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

381342

382343prs = sUN "prim__readString"

383344pbm = sUN "prim__believe_me"

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

386347pioret = sUN "prim_io_return"

387348piobind = sUN "prim_io_bind"

388349upio = sUN "unsafePerformPrimIO"

350+delay = sUN "Delay"

351+force = sUN "Force"

389352

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

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

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

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

427390 caseRes <- execCase' env ctxt amap sc

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

430393 Nothing -> return Nothing

431394 else return Nothing

432395

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

436399execCase' env ctxt amap (STerm tm) =

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

438401execCase' 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

441403 Just (newCase, newBindings) ->

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

443405 execCase' env ctxt amap' newCase

src/Idris/Coverage.hs+3−2

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

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

7373 -- suggests)

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

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

76− _ -> repeat (pexp Placeholder)

75+ (p : _) ->

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

77+ _ -> repeat (pexp Placeholder)

7778 let tryclauses = mkClauses parg all_args

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

7980 logLvl 1 $ showSep "\n" (map (showTm i) tryclauses)

src/Idris/DeepSeq.hs+4−4

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

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

277277 rnf (PImp x1 x2 x3 x4 x5)

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

279− rnf (PExp x1 x2 x3)

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

281− rnf (PConstraint x1 x2 x3)

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

279+ rnf (PExp x1 x2 x3 x4)

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

281+ rnf (PConstraint x1 x2 x3 x4)

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

283283 rnf (PTacImplicit x1 x2 x3 x4 x5)

284284 = rnf x1 `seq`

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

src/Idris/Delaborate.hs+3−3

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

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

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

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

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

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

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

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

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

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

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

122122

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

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

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

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

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

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

127127

128128-- | How far to indent sub-errors

src/Idris/ElabDecls.hs+50−31

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

8282

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

8484 ty' <- addUsingConstraints syn fc ty'

85− ty' <- implicit syn n ty'

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

8686

8787 let ty = addImpl i ty'

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

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

204204 checkUndefined fc n

205205 ctxt <- getContext

206206 i <- getIState

207− t_in <- implicit syn n t_in

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

208+ t_in <- implicit info syn n t_in

208209 let t = addImpl i t_in

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

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

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

222223 undef <- isUndefined fc n

223224 ctxt <- getContext

224225 i <- getIState

225− t_in <- implicit syn n t_in

226+ t_in <- implicit info syn n t_in

226227 let t = addImpl i t_in

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

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

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

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

239240 -- temporary, to check cons

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

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

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

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

242244 ttag <- getName

243245 i <- getIState

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

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

321323 | otherwise = count n ts

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

323325

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

327+

328+ -- Abuse of ElabInfo.

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

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

331+ cinfo info ds

332+ = let newps = params info

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

334+ newb = addAlist dsParams (inblock info)

335+ l = liftname info in

336+ info { params = newps,

337+ inblock = newb,

338+ liftname = id -- Is this appropriate?

339+ }

340+

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

325342

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

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

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

731748elabRecord info syn doc fc tyn ty cdoc cn cty

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

733− cty' <- implicit syn cn cty

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

751+ cty' <- implicit info syn cn cty

734752 i <- getIState

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

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

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

752770 where

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

754772

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

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

756774 isNonImp _ = Nothing

757775

758776 tryElabDecl info (fn, ty, val)

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

841859 = do checkUndefined fc n

842860 ctxt <- getContext

843861 i <- getIState

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

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

845863 let t = addImpl i t_in

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

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

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

875893

876894 mkLazy (PPi pl n ty sc)

877895 = let ty' = if getTyName ty

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

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

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

880898 pexp ty]

881899 else ty in

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

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

12931311 _ -> False

12941312

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

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

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

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

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

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

14231441 -- Elaborate where block

14241442 ist <- getIState

14251443 windex <- getName

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

14271444 let decls = nub (concatMap declared whereblock)

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

14291446 let newargs = pvars ist lhs_tm

1447+ let winfo = pinfo info newargs defs windex

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

14311449

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

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

14351453 let (wbefore, wafter) = sepBlocks wb

14361454

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

1438− mapM_ (elabDecl' EAll info) wbefore

1456+ mapM_ (elabDecl' EAll winfo) wbefore

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

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

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

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

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

14511469 setNextName

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

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

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

14541472 errAt "right hand side of " fname

14551473 (erun fc $ psolve lhs_tm)

14561474 hs <- get_holes

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

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

14791497 -- from the where block

14801498

1481− mapM_ (elabDecl' EAll info) wafter

1482− mapM_ (elabCaseBlock info opts) is

1499+ mapM_ (elabDecl' EAll winfo) wafter

1500+ mapM_ (elabCaseBlock winfo opts) is

14831501

14841502 ctxt <- getContext

14851503 logLvl 5 $ "Rechecking"

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

15091527 addErrRev (crhs, clhs)

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

15111529 where

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

1531+ pinfo info ns ds i

1532+ = let newps = params info ++ ns

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

1534+ newb = addAlist dsParams (inblock info)

1535+ l = liftname info in

1536+ info { params = newps,

1537+ inblock = newb,

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

1539+ -- Nothing -> n

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

1541+ }

1542+

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

15131544 mkLHSapp t = t

15141545

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

15311562 (b : bf, af)

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

15331564

1534− pinfo ns ps i

1535− = let ds = concatMap declared ps

1536− newps = params info ++ ns

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

1538− newb = addAlist dsParams (inblock info)

1539− l = liftname info in

1540− info { params = newps,

1541− inblock = newb,

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

1543− -- Nothing -> n

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

1545− }

1546−

15471565

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

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

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

18081826

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

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

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

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

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

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

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

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

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

20132031 elabFindOverlapping i ci iname syn t

20142032 = do ty' <- addUsingConstraints syn fc t

2015− ty' <- implicit syn iname ty'

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

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

20162035 let ty = addImpl i ty'

20172036 ctxt <- getContext

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

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

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

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

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

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

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

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

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

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

20562075 methArgs i _ = []

20572076

20582077 papp fc f [] = f

src/Idris/ElabTerm.hs+2−11

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

33module Idris.ElabTerm where

55import Idris.AbsSyntax

6+import Idris.AbsSyntaxTree

67import Idris.DSL

78import Idris.Delaborate

89import Idris.Error

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

2728

2829import Debug.Trace

2930

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

31−-- paramaterised declarations, etc.

32−

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

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

35− liftname :: Name -> Name,

36− namespace :: Maybe [String] }

37−

38−toplevel = EInfo [] emptyContext id Nothing

39−

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

4132-- elaborated, typechecked term.

4233--

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

697688 where

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

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

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

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

701692 [pexp t])

702693

703694 insertCoerce ina t =

src/Idris/IBC.hs+9−5

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

2929import Util.Zlib (decompressEither)

3030

3131ibcVersion :: Word8

32−ibcVersion = 65

32+ibcVersion = 66

3333

3434data IBCFile = IBCFile { ver :: Word8,

3535 sourcefile :: FilePath,

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

20372037 put x3

20382038 put x4

20392039 put x5

2040− PExp x1 x2 x3 ->

2040+ PExp x1 x2 x3 x4 ->

20412041 do putWord8 1

20422042 put x1

20432043 put x2

20442044 put x3

2045− PConstraint x1 x2 x3 ->

2045+ put x4

2046+ PConstraint x1 x2 x3 x4 ->

20462047 do putWord8 2

20472048 put x1

20482049 put x2

20492050 put x3

2051+ put x4

20502052 PTacImplicit x1 x2 x3 x4 x5 ->

20512053 do putWord8 3

20522054 put x1

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

20662068 1 -> do x1 <- get

20672069 x2 <- get

20682070 x3 <- get

2069− return (PExp x1 x2 x3)

2071+ x4 <- get

2072+ return (PExp x1 x2 x3 x4)

20702073 2 -> do x1 <- get

20712074 x2 <- get

20722075 x3 <- get

2073− return (PConstraint x1 x2 x3)

2076+ x4 <- get

2077+ return (PConstraint x1 x2 x3 x4)

20742078 3 -> do x1 <- get

20752079 x2 <- get

20762080 x3 <- get

src/Idris/IdeSlave.hs+2

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

151151 | Apropos String

152152 | GetOpts

153153 | SetOpt Opt Bool

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

154155 deriving Show

155156

156157sexpToCommand :: SExp -> Maybe IdeSlaveCommand

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

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

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

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

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

177179sexpToCommand _ = Nothing

178180

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

src/Idris/ParseExpr.hs+19−8

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

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

151151 Just (SynTm t) -> t

152152 _ -> PRef fc n

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

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

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

156− (update (dropn n ns) sc)

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

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

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

153+ update ns (PLam n ty sc)

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

155+ update ns (PPi p n ty sc)

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

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

158+ update ns (PLet n ty val sc)

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

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

161+ update ns (PApp fc t args)

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

163+ update ns (PAppBind fc t args)

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

165+ update ns (PCase fc c opts)

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

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

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

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

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

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

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

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

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

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

177185 update ns t = t

178186

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

188+ updTacImp _ x = x

189+

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

180191@

181192InternalExpr ::=

src/Idris/Parser.hs+9−3

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

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

1818

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

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

2021

21−import Idris.AbsSyntax

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

2223import Idris.DSL

2324import Idris.Imports

2425import Idris.Delaborate

2526import Idris.Error

2627import Idris.ElabDecls

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

28+import Idris.ElabTerm

2829import Idris.Coverage

2930import Idris.IBC

3031import Idris.Unlit

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

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

11211122 (FC failname pos pos, msg)

11221123

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+

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

11241130-- documentation strings.

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

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

11321138 let (fc, msg) = findFC doc

11331139 i <- getIState

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

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

11371143 putIState (i { errSpan = Just fc })

11381144 return []

src/Idris/PartialEval.hs+1−1

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

124124 | imparg imp = (ImplicitD, tm)

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

126126

127− imparg (PExp _ _ _) = False

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

128128 imparg _ = True

129129

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

src/Idris/Providers.hs+2−1

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

1111

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

1313providerTy :: FC -> PTerm -> PTerm

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

14+providerTy fc tm

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

1516

1617ioret = sUN "prim_io_return"

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

src/Idris/REPL.hs+58−31

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

1313import Idris.Delaborate

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

1515import Idris.Prover

16−import Idris.Parser

16+import Idris.Parser hiding (indent)

1717import Idris.Primitives

1818import Idris.Coverage

1919import Idris.UnusedArgs

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

7979import Data.Word (Word)

8080import Control.DeepSeq

8181

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

83−

8482import Debug.Trace

8583

8684-- | Run the REPL

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

286284 do setErrContext b

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

288286 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

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

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

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

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

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

296304 [n] -> Right $ sUN n

297305 (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)

298327

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

300329ideslaveProcess fn Help = process stdout fn Help

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

617646process h fn (Info n)

618647 = do i <- getIState

619648 case lookupCtxt n (idris_classes i) of

620− [c] -> classInfo c

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

650+ ihRenderResult h info

621651 _ -> iPrintError "Not a class"

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

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

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

9931023 isUN (NS n _) = isUN n

9941024 isUN _ = False

9951025

996−classInfo :: ClassInfo -> Idris ()

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

998− mapM_ dumpMethod (class_methods ci)

999− iputStrLn ""

1000− iputStrLn "Default superclass instances:\n"

1001− mapM_ dumpDefaultInstance (class_default_superclasses ci)

1002− iputStrLn ""

1003− iputStrLn "Instances:\n"

1004− mapM_ dumpInstance (class_instances ci)

1005− iPrintResult ""

1006−

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

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

1009−

1010−dumpDefaultInstance :: PDecl -> Idris ()

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

1012−

1013−dumpInstance :: Name -> Idris ()

1014−dumpInstance n = do i <- getIState

1015− ctxt <- getContext

1016− case lookupTy n ctxt of

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

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

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

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

1035+ text "Default superclass instances:" <>

1036+ line <>

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

1038+ line <>

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

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

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

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

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

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

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

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

1047+ params = class_params ci

1048+ params' = zip params (repeat False)

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

10181050

10191051showTotal :: Totality -> IState -> String

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

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

13491381 res <- execute tm

13501382 runIO $ exitWith ExitSuccess

13511383

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−

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

13581385getIdrisUserDataDir :: Idris FilePath

13591386getIdrisUserDataDir = 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