a009be6 · Idris-dev · git.iko.soy

idris.cabal+3

compare with master

unifiedsplit

@@ -320,6 +320,9 @@ Extra-source-files:

320 test/reg069/run

321 test/reg069/*.idr

322 test/reg069/expected

323+ test/reg070/run

324+ test/reg070/*.idr

325+ test/reg070/expected

323

326

324 test/basic001/run

327 test/basic001/run

325 test/basic001/*.idr

328 test/basic001/*.idr

libs/prelude/Prelude/Nat.idr+1−3

@@ -341,12 +341,10 @@ partial

341divCeil : Nat -> Nat -> Nat

342divCeil x (S y) = divCeilNZ x (S y) SIsNotZ

343

344−-- TMP HACK until it's possible to set flags on instances

345−%default partial

344+partial

346Integral Nat where

345Integral Nat where

347 div = divNat

346 div = divNat

348 mod = modNat

347 mod = modNat

349−%default total

350

348

351log2NZ : (x: Nat) -> Not (x = Z) -> Nat

349log2NZ : (x: Nat) -> Not (x = Z) -> Nat

352log2NZ Z p = void (p Refl)

350log2NZ Z p = void (p Refl)

src/Idris/AbsSyntax.hs+2−2

@@ -1272,10 +1272,10 @@ expandParamsD rhs ist dec ps ns (PClass doc info f cs n nfc params pDocs fds dec

1272 (map (expandParamsD rhs ist dec ps ns) decls)

1273 cn

1274 cd

1275−expandParamsD rhs ist dec ps ns (PInstance doc argDocs info f cs acc n nfc params ty cn decls)

1275+expandParamsD rhs ist dec ps ns (PInstance doc argDocs info f cs acc opts n nfc params ty cn decls)

1276 = PInstance doc argDocs info f

1277 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)

1278− acc n

1278+ acc opts n

1279 nfc

1280 (map (expandParams dec ps ns []) params)

1281 (expandParams dec ps ns [] ty)

src/Idris/AbsSyntaxTree.hs+7−6

@@ -725,6 +725,7 @@ data PDecl' t

725 SyntaxInfo

726 FC [(Name, t)] -- constraints

727 Accessibility

728+ FnOpts

728 Name -- class

729 Name -- class

729 FC -- precise location of class

730 FC -- precise location of class

730 [t] -- parameters

731 [t] -- parameters

@@ -884,10 +885,10 @@ mapPDeclFC f g (PClass doc syn fc constrs n nfc params paramDocs det body ctor c

884 (map (mapPDeclFC f g) body)

885 (map (mapPDeclFC f g) body)

885 (fmap (\(n, nfc) -> (n, g nfc)) ctor)

886 (fmap (\(n, nfc) -> (n, g nfc)) ctor)

886 ctorDoc

887 ctorDoc

887−mapPDeclFC f g (PInstance doc paramDocs syn fc constrs cn acc cnfc params instTy instN body) =

888+mapPDeclFC f g (PInstance doc paramDocs syn fc constrs cn acc opts cnfc params instTy instN body) =

888 PInstance doc paramDocs syn (f fc)

889 PInstance doc paramDocs syn (f fc)

889 (map (\(constrN, constrT) -> (constrN, mapPTermFC f g constrT)) constrs)

890 (map (\(constrN, constrT) -> (constrN, mapPTermFC f g constrT)) constrs)

890− cn acc (g cnfc) (map (mapPTermFC f g) params)

891+ cn acc opts (g cnfc) (map (mapPTermFC f g) params)

891 (mapPTermFC f g instTy)

892 (mapPTermFC f g instTy)

892 instN

893 instN

893 (map (mapPDeclFC f g) body)

894 (map (mapPDeclFC f g) body)

@@ -927,7 +928,7 @@ declared (PParams _ _ ds) = concatMap declared ds

927declared (PNamespace _ _ ds) = concatMap declared ds

928declared (PNamespace _ _ ds) = concatMap declared ds

928declared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)

929declared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)

929declared (PClass _ _ _ _ n _ _ _ _ ms cn cd) = n : (map fst (maybeToList cn) ++ concatMap declared ms)

930declared (PClass _ _ _ _ n _ _ _ _ ms cn cd) = n : (map fst (maybeToList cn) ++ concatMap declared ms)

930−declared (PInstance _ _ _ _ _ _ _ _ _ _ _ _) = []

931+declared (PInstance _ _ _ _ _ _ _ _ _ _ _ _ _) = []

931declared (PDSL n _) = [n]

932declared (PDSL n _) = [n]

932declared (PSyntax _ _) = []

933declared (PSyntax _ _) = []

933declared (PMutual _ ds) = concatMap declared ds

934declared (PMutual _ ds) = concatMap declared ds

@@ -947,7 +948,7 @@ tldeclared (PParams _ _ ds) = []

947tldeclared (PMutual _ ds) = concatMap tldeclared ds

948tldeclared (PMutual _ ds) = concatMap tldeclared ds

948tldeclared (PNamespace _ _ ds) = concatMap tldeclared ds

949tldeclared (PNamespace _ _ ds) = concatMap tldeclared ds

949tldeclared (PClass _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap tldeclared ms)

950tldeclared (PClass _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap tldeclared ms)

950−tldeclared (PInstance _ _ _ _ _ _ _ _ _ _ _ _) = []

951+tldeclared (PInstance _ _ _ _ _ _ _ _ _ _ _ _ _) = []

951tldeclared _ = []

952tldeclared _ = []

952

953

953defined :: PDecl -> [Name]

954defined :: PDecl -> [Name]

@@ -963,7 +964,7 @@ defined (PParams _ _ ds) = concatMap defined ds

963defined (PNamespace _ _ ds) = concatMap defined ds

964defined (PNamespace _ _ ds) = concatMap defined ds

964defined (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)

965defined (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)

965defined (PClass _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap defined ms)

966defined (PClass _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap defined ms)

966−defined (PInstance _ _ _ _ _ _ _ _ _ _ _ _) = []

967+defined (PInstance _ _ _ _ _ _ _ _ _ _ _ _ _) = []

967defined (PDSL n _) = [n]

968defined (PDSL n _) = [n]

968defined (PSyntax _ _) = []

969defined (PSyntax _ _) = []

969defined (PMutual _ ds) = concatMap defined ds

970defined (PMutual _ ds) = concatMap defined ds

@@ -2118,7 +2119,7 @@ showDeclImp o (PNamespace n fc ps) = text "namespace" <+> text n <> braces (lin

2118showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)

2119showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)

2119showDeclImp o (PClass _ _ _ cs n _ ps _ _ ds _ _)

2120showDeclImp o (PClass _ _ _ cs n _ ps _ _ ds _ _)

2120 = text "interface" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds

2121 = text "interface" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds

2121−showDeclImp o (PInstance _ _ _ _ cs acc n _ _ t _ ds)

2122+showDeclImp o (PInstance _ _ _ _ cs acc _ n _ _ t _ ds)

2122 = text "implementation" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds

2123 = text "implementation" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds

2123showDeclImp _ _ = text "..."

2124showDeclImp _ _ = text "..."

2124-- showDeclImp (PImport o) = "import " ++ o

2125-- showDeclImp (PImport o) = "import " ++ o

src/Idris/DeepSeq.hs+2−2

@@ -468,7 +468,7 @@ instance (NFData t) => NFData (PDecl' t) where

468 rnf x9 `seq`

469 rnf x10 `seq`

470 rnf x11 `seq` rnf x12 `seq` ()

471− rnf (PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)

471+ rnf (PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)

472 = rnf x1 `seq`

473 rnf x2 `seq`

474 rnf x3 `seq`

@@ -477,7 +477,7 @@ instance (NFData t) => NFData (PDecl' t) where

477 rnf x6 `seq`

478 rnf x7 `seq`

479 rnf x8 `seq`

480− rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` rnf x12 `seq` ()

480+ rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` rnf x12 `seq` rnf x13 `seq` ()

481 rnf (PDSL x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

482 rnf (PSyntax x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

483 rnf (PMutual x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

src/Idris/Docs.hs+2−2

@@ -319,8 +319,8 @@ docClass n ci

319 namedInst n@(UN _) = Just n

320 namedInst _ = Nothing

321

322− getDInst (PInstance _ _ _ _ _ _ _ _ _ t _ _) = Just t

322+ getDInst (PInstance _ _ _ _ _ _ _ _ _ _ t _ _) = Just t

323− getDInst _ = Nothing

323+ getDInst _ = Nothing

324

325 isSubclass (PPi (Constraint _ _) _ _ (PApp _ _ args) (PApp _ (PRef _ _ nm) args'))

326 = nm == n && map getTm args == map getTm args'

src/Idris/Elab/Class.hs+2−2

@@ -138,7 +138,7 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

138

139 -- TODO: probably should normalise

140 checkDefaultSuperclassInstance :: PDecl -> Idris ()

141− checkDefaultSuperclassInstance (PInstance _ _ _ fc cs _ n _ ps _ _ _)

141+ checkDefaultSuperclassInstance (PInstance _ _ _ fc cs _ _ n _ ps _ _ _)

142 = do when (not $ null cs) . tclift

143 $ tfail (At fc (Msg $ "Default superclass instances can't have constraints."))

144 i <- getIState

@@ -184,7 +184,7 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

184

185 tydecl (PTy _ _ _ _ _ _ _ _) = True

186 tydecl _ = False

187− instdecl (PInstance _ _ _ _ _ _ _ _ _ _ _ _) = True

187+ instdecl (PInstance _ _ _ _ _ _ _ _ _ _ _ _ _) = True

188 instdecl _ = False

189 clause (PClauses _ _ _ _) = True

190 clause _ = False

src/Idris/Elab/Instance.hs+6−6

@@ -56,13 +56,14 @@ elabInstance :: ElabInfo -> SyntaxInfo ->

56 ElabWhat -> -- phase

57 FC -> [(Name, PTerm)] -> -- constraints

58 Accessibility ->

59+ FnOpts ->

59 Name -> -- the class

60 Name -> -- the class

60 FC -> -- precise location of class name

61 FC -> -- precise location of class name

61 [PTerm] -> -- class parameters (i.e. instance)

62 [PTerm] -> -- class parameters (i.e. instance)

62 PTerm -> -- full instance type

63 PTerm -> -- full instance type

63 Maybe Name -> -- explicit name

64 Maybe Name -> -- explicit name

64 [PDecl] -> Idris ()

65 [PDecl] -> Idris ()

65−elabInstance info syn doc argDocs what fc cs acc n nfc ps t expn ds = do

66+elabInstance info syn doc argDocs what fc cs acc opts n nfc ps t expn ds = do

66 ist <- getIState

67 ist <- getIState

67 (n, ci) <- case lookupCtxtName n (idris_classes ist) of

68 (n, ci) <- case lookupCtxtName n (idris_classes ist) of

68 [c] -> return c

69 [c] -> return c

@@ -74,8 +75,7 @@ elabInstance info syn doc argDocs what fc cs acc n nfc ps t expn ds = do

74 putIState (ist { hide_list = addDef iname acc (hide_list ist) })

75 putIState (ist { hide_list = addDef iname acc (hide_list ist) })

75 ist <- getIState

76 ist <- getIState

76

77

77− let totopts = if default_total ist then [TotalFn, Dictionary]

78+ let totopts = Dictionary : opts

78− else [Dictionary]

79

80 let emptyclass = null (class_methods ci)

81 when (what /= EDefns) $ do

@@ -166,10 +166,10 @@ elabInstance info syn doc argDocs what fc cs acc n nfc ps t expn ds = do

166 Just m -> sNS (SN (sInstanceN n' (map show ps'))) m

167 Just nm -> nm

168

169− substInstance ips pnames (PInstance doc argDocs syn _ cs acc n nfc ps t expn ds)

169+ substInstance ips pnames (PInstance doc argDocs syn _ cs acc opts n nfc ps t expn ds)

170− = PInstance doc argDocs syn fc cs acc n nfc (map (substMatchesShadow ips pnames) ps) (substMatchesShadow ips pnames t) expn ds

170+ = PInstance doc argDocs syn fc cs acc opts n nfc (map (substMatchesShadow ips pnames) ps) (substMatchesShadow ips pnames t) expn ds

171

172− isOverlapping i (PInstance doc argDocs syn _ _ _ n nfc ps t expn _)

172+ isOverlapping i (PInstance doc argDocs syn _ _ _ _ n nfc ps t expn _)

173 = case lookupCtxtName n (idris_classes i) of

174 [(n, ci)] -> let iname = (mkiname n (namespace info) ps expn) in

175 case lookupTy iname (tt_ctxt i) of

src/Idris/ElabDecls.hs+2−2

@@ -242,9 +242,9 @@ elabDecl' what info (PClass doc s f cs n nfc ps pdocs fds ds cn cd)

242 | what /= EDefns

243 = do logElab 1 $ "Elaborating class " ++ show n

244 elabClass info (s { syn_params = [] }) doc f cs n nfc ps pdocs fds ds cn cd

245−elabDecl' what info (PInstance doc argDocs s f cs acc n nfc ps t expn ds)

245+elabDecl' what info (PInstance doc argDocs s f cs acc fnopts n nfc ps t expn ds)

246 = do logElab 1 $ "Elaborating instance " ++ show n

247− elabInstance info s doc argDocs what f cs acc n nfc ps t expn ds

247+ elabInstance info s doc argDocs what f cs acc fnopts n nfc ps t expn ds

248elabDecl' what info (PRecord doc rsyn fc opts name nfc ps pdocs fs cname cdoc csyn)

249 = do logElab 1 $ "Elaborating record " ++ show name

250 elabRecord info what doc rsyn fc opts name nfc ps pdocs fs cname cdoc csyn

src/Idris/IBC.hs+5−3

@@ -40,7 +40,7 @@ import System.Directory

40import Codec.Archive.Zip

41

42ibcVersion :: Word16

43−ibcVersion = 134

43+ibcVersion = 135

44

45-- When IBC is being loaded - we'll load different things (and omit different

46-- structures/definitions) depending on which phase we're in

@@ -1262,7 +1262,7 @@ instance (Binary t) => Binary (PDecl' t) where

1262 put x10

1263 put x11

1264 put x12

1265− PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ->

1265+ PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 ->

1266 do putWord8 8

1267 put x1

1268 put x2

@@ -1276,6 +1276,7 @@ instance (Binary t) => Binary (PDecl' t) where

1276 put x10

1277 put x11

1278 put x12

1279+ put x13

1279 PDSL x1 x2 -> do putWord8 9

1280 PDSL x1 x2 -> do putWord8 9

1280 put x1

1281 put x1

1281 put x2

1282 put x2

@@ -1391,7 +1392,8 @@ instance (Binary t) => Binary (PDecl' t) where

1391 x10 <- get

1392 x10 <- get

1392 x11 <- get

1393 x11 <- get

1393 x12 <- get

1394 x12 <- get

1395+ x13 <- get

1394− return (PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)

1396+ return (PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)

1395 9 -> do x1 <- get

1397 9 -> do x1 <- get

1396 x2 <- get

1398 x2 <- get

1397 return (PDSL x1 x2)

1399 return (PDSL x1 x2)

src/Idris/Parser.hs+11−4

@@ -337,8 +337,8 @@ declExtension syn ns rules =

337 (map (updateNs ns) ds)

338 (updateRecCon ns cname)

339 cdocs

340− updateNs ns (PInstance docs pdocs s fc cs acc cn fc' ps ity ni ds)

340+ updateNs ns (PInstance docs pdocs s fc cs acc opts cn fc' ps ity ni ds)

341− = PInstance docs pdocs s fc cs acc (updateB ns cn) fc'

341+ = PInstance docs pdocs s fc cs acc opts (updateB ns cn) fc'

342 ps ity (fmap (updateB ns) ni)

343 (map (updateNs ns) ds)

344 updateNs ns (PMutual fc ds) = PMutual fc (map (updateNs ns) ds)

@@ -907,7 +907,14 @@ InstanceName ::= '[' Name ']';

907-}

908instance_ :: Bool -> SyntaxInfo -> IdrisParser [PDecl]

909instance_ kwopt syn

910+ = do ist <- get

911+ let initOpts = if default_total ist

912+ then [TotalFn]

913+ else []

914+ opts <- fnOpts initOpts

910− = do acc <- accessibility

915+ acc <- accessibility

916+ opts' <- fnOpts opts

917+

911 (doc, argDocs)

918 (doc, argDocs)

912 <- try (docstring syn <* if kwopt then optional instanceKeyword

919 <- try (docstring syn <* if kwopt then optional instanceKeyword

913 else do instanceKeyword

920 else do instanceKeyword

@@ -921,7 +928,7 @@ instance_ kwopt syn

921 let sc = PApp fc (PRef cnfc [cnfc] cn) (map pexp args)

928 let sc = PApp fc (PRef cnfc [cnfc] cn) (map pexp args)

922 let t = bindList (PPi constraint) cs sc

929 let t = bindList (PPi constraint) cs sc

923 ds <- instanceBlock syn

930 ds <- instanceBlock syn

924− return [PInstance doc argDocs syn fc cs' acc cn cnfc args t en ds]

931+ return [PInstance doc argDocs syn fc cs' acc opts' cn cnfc args t en ds]

925 <?> "implementation declaration"

932 <?> "implementation declaration"

926 where instanceName :: IdrisParser Name

933 where instanceName :: IdrisParser Name

927 instanceName = do lchar '['; n_in <- fst <$> fnName; lchar ']'

934 instanceName = do lchar '['; n_in <- fst <$> fnName; lchar ']'

src/Idris/Parser/Helpers.hs+2−2

@@ -695,7 +695,7 @@ collect (PMutual f ms : ds) = PMutual f (collect ms) : collect ds

695collect (PNamespace ns fc ps : ds) = PNamespace ns fc (collect ps) : collect ds

696collect (PClass doc f s cs n nfc ps pdocs fds ds cn cd : ds')

697 = PClass doc f s cs n nfc ps pdocs fds (collect ds) cn cd : collect ds'

698−collect (PInstance doc argDocs f s cs acc n nfc ps t en ds : ds')

698+collect (PInstance doc argDocs f s cs acc opts n nfc ps t en ds : ds')

699− = PInstance doc argDocs f s cs acc n nfc ps t en (collect ds) : collect ds'

699+ = PInstance doc argDocs f s cs acc opts n nfc ps t en (collect ds) : collect ds'

700collect (d : ds) = d : collect ds

701collect [] = []

src/Idris/REPL.hs+2−2

@@ -902,8 +902,8 @@ process fn (NewDefn decls) = do

902 fixClauses :: PDecl' t -> PDecl' t

903 fixClauses (PClauses fc opts _ css@(clause:cs)) =

904 PClauses fc opts (getClauseName clause) css

905− fixClauses (PInstance doc argDocs syn fc constraints acc cls nfc parms ty instName decls) =

905+ fixClauses (PInstance doc argDocs syn fc constraints acc opts cls nfc parms ty instName decls) =

906− PInstance doc argDocs syn fc constraints acc cls nfc parms ty instName (map fixClauses decls)

906+ PInstance doc argDocs syn fc constraints acc opts cls nfc parms ty instName (map fixClauses decls)

907 fixClauses decl = decl

908

909process fn (Undefine names) = undefine names

test/reg070/expectednew file+2

@@ -0,0 +1,2 @@

1+reg070.idr:7:1:

2+Test_show.Te implementation of Prelude.Show.Show is possibly not total due to: Prelude.Show.Test_show.Te implementation of Prelude.Show.Show, method show

test/reg070/reg070.idrnew file+15

@@ -0,0 +1,15 @@

1+module Test_show

2+

3+%default total

4+

5+data Te = C1 | C2 | C3

6+

7+Show Te where

8+ show C1 = "C1"

9+

10+-- Eq Te where

11+-- (==) C1 C3 = False

12+

13+-- foo : Te -> String

14+-- foo = show

15+

test/reg070/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+${IDRIS:-idris} $@ reg070.idr --check

3+rm -f *.ibc