bbe9dc1 · Idris-dev · git.iko.soy

idris.cabal+1−1

compare with master

unifiedsplit

@@ -1,5 +1,5 @@

1Name: idris

2−Version: 0.9.5.1

2+Version: 0.9.5.2

3License: BSD3

4License-file: LICENSE

5Author: Edwin Brady

lib/Prelude/Strings.idr+1

@@ -4,6 +4,7 @@ import Builtins

4import Prelude.List

5import Prelude.Chars

6import Prelude.Cast

7+import Prelude.Either

7

8

8-- Some more complex string operations

9-- Some more complex string operations

9

10

src/Core/Evaluate.hs+4−2

@@ -138,6 +138,7 @@ unbindEnv (_:bs) (Bind n b sc) = unbindEnv bs sc

138

139usable :: Bool -> Name -> [(Name, Int)] -> (Bool, [(Name, Int)])

140usable _ _ ns@((MN 0 "STOP", _) : _) = (False, ns)

141+usable True (UN "io_bind") ns = (False, ns)

141usable s n [] = (True, [])

142usable s n [] = (True, [])

142usable s n ns = case lookup n ns of

143usable s n ns = case lookup n ns of

143 Just 0 -> (False, ns)

144 Just 0 -> (False, ns)

@@ -188,7 +189,7 @@ eval traceon ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where

188 ev ntimes stk top env (V i) | i < length env = return $ env !! i

189 ev ntimes stk top env (V i) | i < length env = return $ env !! i

189 | otherwise = return $ VV i

190 | otherwise = return $ VV i

190 ev ntimes stk top env (Bind n (Let t v) sc)

191 ev ntimes stk top env (Bind n (Let t v) sc)

191− | not simpl || vinstances 0 sc < 2

192+ | not simpl -- || vinstances 0 sc < 2

192 = do v' <- ev ntimes stk top env v --(finalise v)

193 = do v' <- ev ntimes stk top env v --(finalise v)

193 when (not atRepl) $ step maxred

194 when (not atRepl) $ step maxred

194 sc' <- ev ntimes stk top (v' : env) sc

195 sc' <- ev ntimes stk top (v' : env) sc

@@ -626,7 +627,7 @@ data Totality = Total [Int] -- well-founded arguments

626 deriving Eq

627 deriving Eq

627

628

628data PReason = Other [Name] | Itself | NotCovering | NotPositive | UseUndef Name

629data PReason = Other [Name] | Itself | NotCovering | NotPositive | UseUndef Name

629− | Mutual [Name] | NotProductive

630+ | BelieveMe | Mutual [Name] | NotProductive

630 deriving (Show, Eq)

631 deriving (Show, Eq)

631

632

632instance Show Totality where

633instance Show Totality where

@@ -637,6 +638,7 @@ instance Show Totality where

637 show (Partial NotCovering) = "not total as there are missing cases"

638 show (Partial NotCovering) = "not total as there are missing cases"

638 show (Partial NotPositive) = "not strictly positive"

639 show (Partial NotPositive) = "not strictly positive"

639 show (Partial NotProductive) = "not productive"

640 show (Partial NotProductive) = "not productive"

641+ show (Partial BelieveMe) = "not total due to use of believe_me in proof"

640 show (Partial (Other ns)) = "possibly not total due to: " ++ showSep ", " (map show ns)

642 show (Partial (Other ns)) = "possibly not total due to: " ++ showSep ", " (map show ns)

641 show (Partial (Mutual ns)) = "possibly not total due to recursive path " ++

643 show (Partial (Mutual ns)) = "possibly not total due to recursive path " ++

642 showSep " --> " (map show ns)

644 showSep " --> " (map show ns)

src/Idris/Coverage.hs+3

@@ -408,6 +408,7 @@ buildSCG (_, n) = do

408 logLvl 5 $ show newscg

409 addToCG n ( cg { scg = newscg } )

410 [] -> logLvl 5 $ "Could not build SCG for " ++ show n ++ "\n"

411+ x -> error $ "buildSCG: " ++ show (n, x)

411

412

412buildSCG' :: IState -> SC -> [Name] -> [SCGEntry]

413buildSCG' :: IState -> SC -> [Name] -> [SCGEntry]

413buildSCG' ist sc args = nub $ scg sc (zip args args)

414buildSCG' ist sc args = nub $ scg sc (zip args args)

@@ -541,6 +542,8 @@ checkMP ist i mp = if i > 0

541 where

542 where

542 tryPath :: Int -> [(SCGEntry, Int)] -> MultiPath -> Int -> Totality

543 tryPath :: Int -> [(SCGEntry, Int)] -> MultiPath -> Int -> Totality

543 tryPath desc path [] _ = Total []

544 tryPath desc path [] _ = Total []

545+-- tryPath desc path ((UN "believe_me", _) : _) arg

546+-- = Partial BelieveMe

544 -- if we get to a constructor, it's fine as long as it's strictly positive

547 -- if we get to a constructor, it's fine as long as it's strictly positive

545 tryPath desc path ((f, _) :es) arg

548 tryPath desc path ((f, _) :es) arg

546 | [TyDecl (DCon _ _) _] <- lookupDef Nothing f (tt_ctxt ist)

549 | [TyDecl (DCon _ _) _] <- lookupDef Nothing f (tt_ctxt ist)

src/Idris/IBC.hs+2

@@ -682,6 +682,7 @@ instance Binary PReason where

682 Mutual x1 -> do putWord8 4

683 put x1

684 NotProductive -> putWord8 5

685+ BelieveMe -> putWord8 6

685 get

686 get

686 = do i <- getWord8

687 = do i <- getWord8

687 case i of

688 case i of

@@ -693,6 +694,7 @@ instance Binary PReason where

693 4 -> do x1 <- get

694 4 -> do x1 <- get

694 return (Mutual x1)

695 return (Mutual x1)

695 5 -> return NotProductive

696 5 -> return NotProductive

697+ 6 -> return BelieveMe

696 _ -> error "Corrupted binary data for PReason"

698 _ -> error "Corrupted binary data for PReason"

697

699

698instance Binary Totality where

700instance Binary Totality where

src/Idris/Parser.hs+3−1

@@ -771,7 +771,9 @@ pCaseOpt syn = do lhs <- pExpr syn; symbol "=>"; rhs <- pExpr syn

771modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm

772modifyConst syn fc (PConstant (I x))

773 | not (inPattern syn)

774+ = PAlternative False

774− = PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (I x))]

775+ [PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (I x))],

776+ PConstant (I x), PConstant (BI (toEnum x))]

775 | otherwise = PAlternative False

777 | otherwise = PAlternative False

776 [PConstant (I x), PConstant (BI (toEnum x))]

778 [PConstant (I x), PConstant (BI (toEnum x))]

777modifyConst syn fc x = x

779modifyConst syn fc x = x

src/Idris/Primitives.hs+1−1

@@ -169,7 +169,7 @@ primitives =

169 Prim (UN "prim__stdin") (ty [] PtrType) 0 (p_cantreduce)

170 (0, LStdIn) partial,

171 Prim (UN "prim__believe_me") believeTy 3 (p_believeMe)

172− (3, LNoOp) total -- ahem

172+ (3, LNoOp) partial -- ahem

173 ]

174

175p_believeMe [_,_,x] = Just x