a009be6 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Allow setting function flags on instances

As well as accessibility flags. They are functions internally after all. This allows setting partiality/totality per instance, in particular.

commita009be6ad34eb49e3c48a98e8bd2a0b65c861e05 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 14 Feb 2016, 13:17 (11 years ago) parent1d97fa7

16 files changed+67−36

compare with master

unifiedsplit

idris.cabal+3 libs/prelude/Prelude/Nat.idr+1−3 src/Idris/AbsSyntax.hs+2−2 src/Idris/AbsSyntaxTree.hs+7−6 src/Idris/DeepSeq.hs+2−2 src/Idris/Docs.hs+2−2 src/Idris/Elab/Class.hs+2−2 src/Idris/Elab/Instance.hs+6−6 src/Idris/ElabDecls.hs+2−2 src/Idris/IBC.hs+5−3 src/Idris/Parser.hs+11−4 src/Idris/Parser/Helpers.hs+2−2 src/Idris/REPL.hs+2−2 test/reg070/expected+2 test/reg070/reg070.idr+15 test/reg070/run+3

idris.cabal+3

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

320320 test/reg069/run

321321 test/reg069/*.idr

322322 test/reg069/expected

323+ test/reg070/run

324+ test/reg070/*.idr

325+ test/reg070/expected

323326

324327 test/basic001/run

325328 test/basic001/*.idr

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

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

341341divCeil : Nat -> Nat -> Nat

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

343343

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

345−%default partial

344+partial

346345Integral Nat where

347346 div = divNat

348347 mod = modNat

349−%default total

350348

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

352350log2NZ 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

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

12731273 cn

12741274 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)

12761276 = PInstance doc argDocs info f

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

1278− acc n

1278+ acc opts n

12791279 nfc

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

12811281 (expandParams dec ps ns [] ty)

src/Idris/AbsSyntaxTree.hs+7−6

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

725725 SyntaxInfo

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

727727 Accessibility

728+ FnOpts

728729 Name -- class

729730 FC -- precise location of class

730731 [t] -- parameters

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

884885 (map (mapPDeclFC f g) body)

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

886887 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) =

888889 PInstance doc paramDocs syn (f fc)

889890 (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)

891892 (mapPTermFC f g instTy)

892893 instN

893894 (map (mapPDeclFC f g) body)

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

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

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

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

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

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

931932declared (PDSL n _) = [n]

932933declared (PSyntax _ _) = []

933934declared (PMutual _ ds) = concatMap declared ds

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

947948tldeclared (PMutual _ ds) = concatMap tldeclared ds

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

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

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

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

951952tldeclared _ = []

952953

953954defined :: PDecl -> [Name]

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

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

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

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

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

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

967968defined (PDSL n _) = [n]

968969defined (PSyntax _ _) = []

969970defined (PMutual _ ds) = concatMap defined ds

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

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

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

21202121 = 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)

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

21232124showDeclImp _ _ = text "..."

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

src/Idris/DeepSeq.hs+2−2

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

468468 rnf x9 `seq`

469469 rnf x10 `seq`

470470 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)

472472 = rnf x1 `seq`

473473 rnf x2 `seq`

474474 rnf x3 `seq`

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

477477 rnf x6 `seq`

478478 rnf x7 `seq`

479479 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` ()

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

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

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

src/Idris/Docs.hs+2−2

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

319319 namedInst n@(UN _) = Just n

320320 namedInst _ = Nothing

321321

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

323− getDInst _ = Nothing

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

323+ getDInst _ = Nothing

324324

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

326326 = 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

138138

139139 -- TODO: probably should normalise

140140 checkDefaultSuperclassInstance :: PDecl -> Idris ()

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

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

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

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

144144 i <- getIState

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

184184

185185 tydecl (PTy _ _ _ _ _ _ _ _) = True

186186 tydecl _ = False

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

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

188188 instdecl _ = False

189189 clause (PClauses _ _ _ _) = True

190190 clause _ = False

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

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

5656 ElabWhat -> -- phase

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

5858 Accessibility ->

59+ FnOpts ->

5960 Name -> -- the class

6061 FC -> -- precise location of class name

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

6263 PTerm -> -- full instance type

6364 Maybe Name -> -- explicit name

6465 [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

6667 ist <- getIState

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

6869 [c] -> return c

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

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

7576 ist <- getIState

7677

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

78− else [Dictionary]

78+ let totopts = Dictionary : opts

7979

8080 let emptyclass = null (class_methods ci)

8181 when (what /= EDefns) $ do

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

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

167167 Just nm -> nm

168168

169− substInstance ips pnames (PInstance doc argDocs syn _ cs acc 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

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 opts n nfc (map (substMatchesShadow ips pnames) ps) (substMatchesShadow ips pnames t) expn ds

171171

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

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

173173 = case lookupCtxtName n (idris_classes i) of

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

175175 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)

242242 | what /= EDefns

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

244244 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)

246246 = 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

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

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

250250 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

4040import Codec.Archive.Zip

4141

4242ibcVersion :: Word16

43−ibcVersion = 134

43+ibcVersion = 135

4444

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

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

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

12621262 put x10

12631263 put x11

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

12661266 do putWord8 8

12671267 put x1

12681268 put x2

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

12761276 put x10

12771277 put x11

12781278 put x12

1279+ put x13

12791280 PDSL x1 x2 -> do putWord8 9

12801281 put x1

12811282 put x2

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

13911392 x10 <- get

13921393 x11 <- get

13931394 x12 <- get

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

1395+ x13 <- get

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

13951397 9 -> do x1 <- get

13961398 x2 <- get

13971399 return (PDSL x1 x2)

src/Idris/Parser.hs+11−4

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

337337 (map (updateNs ns) ds)

338338 (updateRecCon ns cname)

339339 cdocs

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

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

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 opts (updateB ns cn) fc'

342342 ps ity (fmap (updateB ns) ni)

343343 (map (updateNs ns) ds)

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

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

907907-}

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

909909instance_ kwopt syn

910− = do acc <- accessibility

910+ = do ist <- get

911+ let initOpts = if default_total ist

912+ then [TotalFn]

913+ else []

914+ opts <- fnOpts initOpts

915+ acc <- accessibility

916+ opts' <- fnOpts opts

917+

911918 (doc, argDocs)

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

913920 else do instanceKeyword

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

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

922929 let t = bindList (PPi constraint) cs sc

923930 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]

925932 <?> "implementation declaration"

926933 where instanceName :: IdrisParser Name

927934 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

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

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

697697 = 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')

699− = PInstance doc argDocs f s cs acc n nfc ps t en (collect ds) : collect 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 opts n nfc ps t en (collect ds) : collect ds'

700700collect (d : ds) = d : collect ds

701701collect [] = []

src/Idris/REPL.hs+2−2

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

902902 fixClauses :: PDecl' t -> PDecl' t

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

904904 PClauses fc opts (getClauseName clause) css

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

906− PInstance doc argDocs syn fc constraints acc cls nfc parms ty instName (map fixClauses 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 opts cls nfc parms ty instName (map fixClauses decls)

907907 fixClauses decl = decl

908908

909909process 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

3+%default total

5+data Te = C1 | C2 | C3

7+Show Te where

8+ show C1 = "C1"

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