7f20feb · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Don't totality check PE definitions

Their totality arises from the totality of the thing they are generated from, and doing otherwise loses information such as assert_total.

commit7f20febb295c23255f8f169bdd03c0215bac491a authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 5 Jun 2015, 12:03 (11 years ago) parent727a3d6

6 files changed+17−9

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+1 src/Idris/Core/Evaluate.hs+2 src/Idris/Elab/Clause.hs+6−5 src/Idris/IBC.hs+5−1 test/error004/FunErrTest.idr+2−1 test/reg054/expected+1−2

src/Idris/AbsSyntaxTree.hs+1

@@ -573,6 +573,7 @@ data FnOpt = Inlinable -- always evaluate when simplifying

573573 | Specialise [(Name, Maybe Int)] -- specialise it, freeze these names

574574 | Constructor -- Data constructor type

575575 | AutoHint -- use in auto implicit search

576+ | PEGenerated -- generated by partial evaluator

576577 deriving (Show, Eq)

577578{-!

578579deriving instance Binary FnOpt

src/Idris/Core/Evaluate.hs+2

@@ -740,6 +740,7 @@ data Totality = Total [Int] -- ^ well-founded arguments

740740 | Productive -- ^ productive

741741 | Partial PReason

742742 | Unchecked

743+ | Generated

743744 deriving Eq

744745{-!

745746deriving instance NFData Totality

@@ -767,6 +768,7 @@ instance Show Totality where

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

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

769770 show (Partial (UseUndef n)) = "possibly not total because it uses the undefined name " ++ show n

771+ show Generated = "auto-generated"

770772

771773{-!

772774deriving instance Binary Accessibility

src/Idris/Elab/Clause.hs+6−5

@@ -189,9 +189,9 @@ elabClauses info' fc opts n_in cs =

189189

190190 ist <- getIState

191191 -- let wf = wellFounded ist n sc

192− let tot = if pcover || AssertTotal `elem` opts

193− then Unchecked -- finish checking later

194− else Partial NotCovering -- already know it's not total

192+ let tot | pcover || AssertTotal `elem` opts = Unchecked -- finish later

193+ | PEGenerated `elem` opts = Generated

194+ | otherwise = Partial NotCovering -- already know it's not total

195195

196196 -- case lookupCtxt (namespace info) n (idris_flags ist) of

197197 -- [fs] -> if TotalFn `elem` fs

@@ -241,7 +241,8 @@ elabClauses info' fc opts n_in cs =

241241 setContext ctxt'

242242 addIBC (IBCDef n)

243243 setTotality n tot

244− when (not reflect) $ do totcheck (fc, n)

244+ when (not reflect && PEGenerated `notElem` opts) $

245+ do totcheck (fc, n)

245246 defer_totcheck (fc, n)

246247 when (tot /= Unchecked) $ addIBC (IBCTotal n tot)

247248 i <- getIState

@@ -383,7 +384,7 @@ elabPE info fc caller r =

383384 PClause fc newnm lhs [] rhs [])

384385 (pe_clauses specdecl)

385386 trans <- elabTransform info fc False rhs lhs

386− elabClauses info fc opts newnm def

387+ elabClauses info fc (PEGenerated:opts) newnm def

387388 return [trans]

388389 else return [])

389390 -- if it doesn't work, just don't specialise. Could happen for lots

src/Idris/IBC.hs+5−1

@@ -41,7 +41,7 @@ import Codec.Archive.Zip

4141import Util.Zlib (decompressEither)

4242

4343ibcVersion :: Word16

44−ibcVersion = 111

44+ibcVersion = 112

4545

4646data IBCFile = IBCFile { ver :: Word16,

4747 sourcefile :: FilePath,

@@ -948,6 +948,7 @@ instance Binary Totality where

948948 put x1

949949 Unchecked -> do putWord8 2

950950 Productive -> do putWord8 3

951+ Generated -> do putWord8 4

951952 get

952953 = do i <- getWord8

953954 case i of

@@ -957,6 +958,7 @@ instance Binary Totality where

957958 return (Partial x1)

958959 2 -> return Unchecked

959960 3 -> return Productive

961+ 4 -> return Generated

960962 _ -> error "Corrupted binary data for Totality"

961963

962964instance Binary MetaInformation where

@@ -1007,6 +1009,7 @@ instance Binary FnOpt where

10071009 CExport x1 -> do putWord8 14

10081010 put x1

10091011 AutoHint -> putWord8 15

1012+ PEGenerated -> putWord8 16

10101013 get

10111014 = do i <- getWord8

10121015 case i of

@@ -1028,6 +1031,7 @@ instance Binary FnOpt where

10281031 14 -> do x1 <- get

10291032 return $ CExport x1

10301033 15 -> return AutoHint

1034+ 16 -> return PEGenerated

10311035 _ -> error "Corrupted binary data for FnOpt"

10321036

10331037instance Binary Fixity where

test/error004/FunErrTest.idr+2−1

@@ -17,7 +17,7 @@ cadr [] {cons1=Refl} {cons2=Refl} impossible

1717

1818extractList : TT -> Maybe TT

1919extractList (App (App reflCon (App isCons lst)) _) = Just lst

20−extractList _ = Nothing

20+extractList t = Just t -- Nothing

2121

2222total

2323has2elts : Err -> Maybe (List ErrorReportPart)

@@ -39,3 +39,4 @@ badCadr2 = cadr [1]

3939

4040goodCadr : Int

4141goodCadr = cadr [1, 2]

42+

test/reg054/expected+1−2

@@ -2,8 +2,7 @@ reg054.idr:18:5:When checking left hand side of inf:

22When checking an application of constructor Main.MkInfer:

33 Attempting concrete match on polymorphic argument: 0

44reg054.idr:34:7:When checking left hand side of weird:

5−When checking argument x to Main.weird:

6− No explicit types on left hand side: Char

5+No explicit types on left hand side: Char

76reg054.idr:37:1-8:When checking left hand side of tctrick:

87When checking an application of Main.tctrick:

98 Type mismatch between