bbe9dc1 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Minor fixes for inlining and integer literals

commitbbe9dc137e18ea9bfa24038dc2bf900da4c6714a authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 20 Nov 2012, 13:01 (14 years ago) parent3d74fb2

7 files changed+15−5

compare with master

unifiedsplit

idris.cabal+1−1 lib/Prelude/Strings.idr+1 src/Core/Evaluate.hs+4−2 src/Idris/Coverage.hs+3 src/Idris/IBC.hs+2 src/Idris/Parser.hs+3−1 src/Idris/Primitives.hs+1−1

idris.cabal+1−1

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

11Name: idris

2−Version: 0.9.5.1

2+Version: 0.9.5.2

33License: BSD3

44License-file: LICENSE

55Author: Edwin Brady

lib/Prelude/Strings.idr+1

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

44import Prelude.List

55import Prelude.Chars

66import Prelude.Cast

7+import Prelude.Either

89-- Some more complex string operations

910

src/Core/Evaluate.hs+4−2

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

138138

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

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

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

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

142143usable s n ns = case lookup n ns of

143144 Just 0 -> (False, ns)

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

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

189190 | otherwise = return $ VV i

190191 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

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

193194 when (not atRepl) $ step maxred

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

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

626627 deriving Eq

627628

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

629− | Mutual [Name] | NotProductive

630+ | BelieveMe | Mutual [Name] | NotProductive

630631 deriving (Show, Eq)

631632

632633instance Show Totality where

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

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

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

639640 show (Partial NotProductive) = "not productive"

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

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

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

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

src/Idris/Coverage.hs+3

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

408408 logLvl 5 $ show newscg

409409 addToCG n ( cg { scg = newscg } )

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

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

411412

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

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

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

541542 where

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

543544 tryPath desc path [] _ = Total []

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

546+-- = Partial BelieveMe

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

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

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

src/Idris/IBC.hs+2

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

682682 Mutual x1 -> do putWord8 4

683683 put x1

684684 NotProductive -> putWord8 5

685+ BelieveMe -> putWord8 6

685686 get

686687 = do i <- getWord8

687688 case i of

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

693694 4 -> do x1 <- get

694695 return (Mutual x1)

695696 5 -> return NotProductive

697+ 6 -> return BelieveMe

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

697699

698700instance Binary Totality where

src/Idris/Parser.hs+3−1

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

771771modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm

772772modifyConst syn fc (PConstant (I x))

773773 | not (inPattern syn)

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

774+ = PAlternative False

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

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

775777 | otherwise = PAlternative False

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

777779modifyConst syn fc x = x

src/Idris/Primitives.hs+1−1

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

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

170170 (0, LStdIn) partial,

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

172− (3, LNoOp) total -- ahem

172+ (3, LNoOp) partial -- ahem

173173 ]

174174

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