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

src/Idris/AbsSyntaxTree.hs+1

compare with master

unifiedsplit

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

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

574 | Constructor -- Data constructor type

575 | AutoHint -- use in auto implicit search

576+ | PEGenerated -- generated by partial evaluator

576 deriving (Show, Eq)

577 deriving (Show, Eq)

577{-!

578{-!

578deriving instance Binary FnOpt

579deriving instance Binary FnOpt

src/Idris/Core/Evaluate.hs+2

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

740 | Productive -- ^ productive

741 | Partial PReason

742 | Unchecked

743+ | Generated

743 deriving Eq

744 deriving Eq

744{-!

745{-!

745deriving instance NFData Totality

746deriving instance NFData Totality

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

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

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

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

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

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

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

771+ show Generated = "auto-generated"

770

772

771{-!

773{-!

772deriving instance Binary Accessibility

774deriving instance Binary Accessibility

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

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

189

190 ist <- getIState

191 -- let wf = wellFounded ist n sc

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

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

193− then Unchecked -- finish checking later

193+ | PEGenerated `elem` opts = Generated

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

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

195

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

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

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

241 setContext ctxt'

242 addIBC (IBCDef n)

243 setTotality n tot

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

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

245+ do totcheck (fc, n)

245 defer_totcheck (fc, n)

246 defer_totcheck (fc, n)

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

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

247 i <- getIState

248 i <- getIState

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

383 PClause fc newnm lhs [] rhs [])

384 PClause fc newnm lhs [] rhs [])

384 (pe_clauses specdecl)

385 (pe_clauses specdecl)

385 trans <- elabTransform info fc False rhs lhs

386 trans <- elabTransform info fc False rhs lhs

386− elabClauses info fc opts newnm def

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

387 return [trans]

388 return [trans]

388 else return [])

389 else return [])

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

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

41import Util.Zlib (decompressEither)

42

43ibcVersion :: Word16

44−ibcVersion = 111

44+ibcVersion = 112

45

46data IBCFile = IBCFile { ver :: Word16,

47 sourcefile :: FilePath,

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

948 put x1

949 Unchecked -> do putWord8 2

950 Productive -> do putWord8 3

951+ Generated -> do putWord8 4

951 get

952 get

952 = do i <- getWord8

953 = do i <- getWord8

953 case i of

954 case i of

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

957 return (Partial x1)

958 return (Partial x1)

958 2 -> return Unchecked

959 2 -> return Unchecked

959 3 -> return Productive

960 3 -> return Productive

961+ 4 -> return Generated

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

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

961

963

962instance Binary MetaInformation where

964instance Binary MetaInformation where

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

1007 CExport x1 -> do putWord8 14

1009 CExport x1 -> do putWord8 14

1008 put x1

1010 put x1

1009 AutoHint -> putWord8 15

1011 AutoHint -> putWord8 15

1012+ PEGenerated -> putWord8 16

1010 get

1013 get

1011 = do i <- getWord8

1014 = do i <- getWord8

1012 case i of

1015 case i of

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

1028 14 -> do x1 <- get

1031 14 -> do x1 <- get

1029 return $ CExport x1

1032 return $ CExport x1

1030 15 -> return AutoHint

1033 15 -> return AutoHint

1034+ 16 -> return PEGenerated

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

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

1032

1036

1033instance Binary Fixity where

1037instance Binary Fixity where

test/error004/FunErrTest.idr+2−1

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

17

18extractList : TT -> Maybe TT

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

20−extractList _ = Nothing

20+extractList t = Just t -- Nothing

21

22total

23has2elts : Err -> Maybe (List ErrorReportPart)

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

39

40goodCadr : Int

41goodCadr = cadr [1, 2]

42+

test/reg054/expected+1−2

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

2When checking an application of constructor Main.MkInfer:

3 Attempting concrete match on polymorphic argument: 0

4reg054.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

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

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

8When checking an application of Main.tctrick:

7When checking an application of Main.tctrick:

9 Type mismatch between

8 Type mismatch between