9297ae4 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Allow 'data' declarations in interfaces

This leads to a method and a top level function as normal, but an implementation of the interface must define the method by returing a type constructor (or some other injective function application). The effect is that Idris treats the top level function as a data type, which helps with unification and interface resolution.

commit9297ae47fba90c5428023eda0ab06555d0e2904a authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 9 May 2016, 21:50 (10 years ago) parenta574e74

18 files changed+167−57

compare with master

unifiedsplit

CHANGELOG.md+5 idris.cabal+3 src/IRTS/Compiler.hs+1−1 src/Idris/ASTUtils.hs+1−1 src/Idris/AbsSyntax.hs+6 src/Idris/AbsSyntaxTree.hs+3−1 src/Idris/CaseSplit.hs+2−2 src/Idris/Core/Evaluate.hs+45−32 src/Idris/Core/Unify.hs+3−1 src/Idris/Core/WHNF.hs+1 src/Idris/DeepSeq.hs+1 src/Idris/Directives.hs+5 src/Idris/Elab/Class.hs+24−6 src/Idris/Elab/Instance.hs+35−1 src/Idris/IBC.hs+11−2 src/Idris/Parser.hs+8−1 src/Idris/Parser/Data.hs+11−7 src/Idris/TypeSearch.hs+2−2

CHANGELOG.md+5

@@ -29,6 +29,11 @@

2929 neutral = 1

3030 ```

3131

32+* Interface definitions can now include data declarations (but not data

33+ definitions). Any implementation of the interface must define the method

34+ using a data type. The effect is to cause Idris to treat the method as

35+ a data type (for unification and interface resolution purposes).

36+

3237* Experimentally, allow named implementations to be available by default in a

3338 block of declarations with `using` notation. For example:

3439

idris.cabal+3

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

620620 test/interfaces004/*.idr

621621 test/interfaces004/run

622622 test/interfaces004/expected

623+ test/interfaces005/*.idr

624+ test/interfaces005/run

625+ test/interfaces005/expected

623626

624627 test/io001/run

625628 test/io001/*.idr

src/IRTS/Compiler.hs+1−1

@@ -439,7 +439,7 @@ irTerm vs env tm@(App _ f a) = do

439439 | otherwise = n

440440

441441 used = maybe [] (map fst . usedpos) $ lookupCtxtExact uName (idris_callgraph ist)

442− fst4 (x,_,_,_) = x

442+ fst4 (x,_,_,_,_) = x

443443

444444irTerm vs env (P _ n _) = return $ LV (Glob n)

445445irTerm vs env (V i)

src/Idris/ASTUtils.hs+1−1

@@ -138,7 +138,7 @@ opts_idrisCmdline =

138138-------------

139139-- This has a terrible name, but I'm not sure of a better one that isn't

140140-- confusingly close to tt_ctxt

141−known_terms :: Field IState (Ctxt (Def, Accessibility, Totality, MetaInformation))

141+known_terms :: Field IState (Ctxt (Def, Injectivity, Accessibility, Totality, MetaInformation))

142142known_terms = Field (definitions . tt_ctxt)

143143 (\v state -> state {tt_ctxt = (tt_ctxt state) {definitions = v}})

144144

src/Idris/AbsSyntax.hs+6

@@ -218,6 +218,12 @@ setTotality n a

218218 let ctxt = setTotal n a (tt_ctxt i)

219219 putIState $ i { tt_ctxt = ctxt }

220220

221+setInjectivity :: Name -> Injectivity -> Idris ()

222+setInjectivity n a

223+ = do i <- getIState

224+ let ctxt = setInjective n a (tt_ctxt i)

225+ putIState $ i { tt_ctxt = ctxt }

226+

221227getTotality :: Name -> Idris Totality

222228getTotality n

223229 = do i <- getIState

src/Idris/AbsSyntaxTree.hs+3−1

@@ -333,6 +333,7 @@ data IBCWrite = IBCFix FixDecl

333333 | IBCAccess Name Accessibility

334334 | IBCMetaInformation Name MetaInformation

335335 | IBCTotal Name Totality

336+ | IBCInjective Name Injectivity

336337 | IBCFlags Name [FnOpt]

337338 | IBCFnInfo Name FnInfo

338339 | IBCTrans Name (Term, Term)

@@ -775,6 +776,7 @@ data Directive = DLib Codegen String

775776 | DInclude Codegen String

776777 | DHide Name

777778 | DFreeze Name

779+ | DInjective Name

778780 | DAccess Accessibility

779781 | DDefault DefaultTotality

780782 | DLogging Integer

@@ -1377,7 +1379,7 @@ highestFC (PAppImpl t _) = highestFC t

13771379-- Type class data

13781380

13791381data ClassInfo = CI { instanceCtorName :: Name,

1380− class_methods :: [(Name, (FnOpts, PTerm))],

1382+ class_methods :: [(Name, (Bool, FnOpts, PTerm))], -- flag whether it's a "data" method

13811383 class_defaults :: [(Name, (Name, PDecl))], -- method name -> default impl

13821384 class_default_superclasses :: [PDecl],

13831385 class_params :: [Name],

src/Idris/CaseSplit.hs+2−2

@@ -410,10 +410,10 @@ getClause l fn un fp

410410 sUN "z"]) used

411411

412412 -- write method declarations, indent with 4 spaces

413− mkClassBodies :: IState -> [(Name, (FnOpts, PTerm))] -> String

413+ mkClassBodies :: IState -> [(Name, (Bool, FnOpts, PTerm))] -> String

414414 mkClassBodies i ns

415415 = showSep "\n"

416− (zipWith (\(n, (_, ty)) m -> " " ++

416+ (zipWith (\(n, (_, _, ty)) m -> " " ++

417417 def (show (nsroot n)) ++ " "

418418 ++ mkApp i ty []

419419 ++ "= ?"

src/Idris/Core/Evaluate.hs+45−32

@@ -6,14 +6,15 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC,

66 normaliseAll, normaliseBlocking, toValue, quoteTerm,

77 rt_simplify, simplify, specialise, hnf, convEq, convEq',

88 Def(..), CaseInfo(..), CaseDefs(..),

9− Accessibility(..), Totality(..), PReason(..), MetaInformation(..),

9+ Accessibility(..), Injectivity, Totality(..), PReason(..), MetaInformation(..),

1010 Context, initContext, ctxtAlist, next_tvar,

11− addToCtxt, setAccess, setTotal, setMetaInformation, addCtxtDef, addTyDecl,

11+ addToCtxt, setAccess, setInjective, setTotal, setMetaInformation, addCtxtDef, addTyDecl,

1212 addDatatype, addCasedef, simplifyCasedef, addOperator,

1313 lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact,

1414 lookupP, lookupP_all, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal,

1515 mapDefCtxt,

16− lookupTotal, lookupTotalExact, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict, isDConName, canBeDConName, isTConName, isConName, isFnName,

16+ lookupTotal, lookupTotalExact, lookupInjectiveExact,

17+ lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict, isDConName, canBeDConName, isTConName, isConName, isFnName,

1718 Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions,

1819 isUniverse) where

1920

@@ -759,6 +760,8 @@ instance Show Accessibility where

759760 show Private = "private"

760761 show Hidden = "hidden"

761762

763+type Injectivity = Bool

764+

762765-- | The result of totality checking

763766data Totality = Total [Int] -- ^ well-founded arguments

764767 | Productive -- ^ productive

@@ -816,7 +819,7 @@ data MetaInformation =

816819-- universe constraints and existing definitions.

817820data Context = MkContext {

818821 next_tvar :: Int,

819− definitions :: Ctxt (Def, Accessibility, Totality, MetaInformation)

822+ definitions :: Ctxt (Def, Injectivity, Accessibility, Totality, MetaInformation)

820823 } deriving Show

821824

822825

@@ -826,47 +829,53 @@ initContext = MkContext 0 emptyContext

826829

827830mapDefCtxt :: (Def -> Def) -> Context -> Context

828831mapDefCtxt f (MkContext t !defs) = MkContext t (mapCtxt f' defs)

829− where f' (!d, a, t, m) = f' (f d, a, t, m)

832+ where f' (!d, i, a, t, m) = f' (f d, i, a, t, m)

830833

831834-- | Get the definitions from a context

832835ctxtAlist :: Context -> [(Name, Def)]

833−ctxtAlist ctxt = map (\(n, (d, a, t, m)) -> (n, d)) $ toAlist (definitions ctxt)

836+ctxtAlist ctxt = map (\(n, (d, i, a, t, m)) -> (n, d)) $ toAlist (definitions ctxt)

834837

835838veval ctxt env t = evalState (eval False ctxt [] env t []) initEval

836839

837840addToCtxt :: Name -> Term -> Type -> Context -> Context

838841addToCtxt n tm ty uctxt

839842 = let ctxt = definitions uctxt

840− !ctxt' = addDef n (Function ty tm, Public, Unchecked, EmptyMI) ctxt in

843+ !ctxt' = addDef n (Function ty tm, False, Public, Unchecked, EmptyMI) ctxt in

841844 uctxt { definitions = ctxt' }

842845

843846setAccess :: Name -> Accessibility -> Context -> Context

844847setAccess n a uctxt

845848 = let ctxt = definitions uctxt

846− !ctxt' = updateDef n (\ (d, _, t, m) -> (d, a, t, m)) ctxt in

849+ !ctxt' = updateDef n (\ (d, i, _, t, m) -> (d, i, a, t, m)) ctxt in

850+ uctxt { definitions = ctxt' }

851+

852+setInjective :: Name -> Injectivity -> Context -> Context

853+setInjective n i uctxt

854+ = let ctxt = definitions uctxt

855+ !ctxt' = updateDef n (\ (d, _, a, t, m) -> (d, i, a, t, m)) ctxt in

847856 uctxt { definitions = ctxt' }

848857

849858setTotal :: Name -> Totality -> Context -> Context

850859setTotal n t uctxt

851860 = let ctxt = definitions uctxt

852− !ctxt' = updateDef n (\ (d, a, _, m) -> (d, a, t, m)) ctxt in

861+ !ctxt' = updateDef n (\ (d, i, a, _, m) -> (d, i, a, t, m)) ctxt in

853862 uctxt { definitions = ctxt' }

854863

855864setMetaInformation :: Name -> MetaInformation -> Context -> Context

856865setMetaInformation n m uctxt

857866 = let ctxt = definitions uctxt

858− !ctxt' = updateDef n (\ (d, a, t, _) -> (d, a, t, m)) ctxt in

867+ !ctxt' = updateDef n (\ (d, i, a, t, _) -> (d, i, a, t, m)) ctxt in

859868 uctxt { definitions = ctxt' }

860869

861870addCtxtDef :: Name -> Def -> Context -> Context

862871addCtxtDef n d c = let ctxt = definitions c

863− !ctxt' = addDef n (d, Public, Unchecked, EmptyMI) $! ctxt in

872+ !ctxt' = addDef n (d, False, Public, Unchecked, EmptyMI) $! ctxt in

864873 c { definitions = ctxt' }

865874

866875addTyDecl :: Name -> NameType -> Type -> Context -> Context

867876addTyDecl n nt ty uctxt

868877 = let ctxt = definitions uctxt

869− !ctxt' = addDef n (TyDecl nt ty, Public, Unchecked, EmptyMI) ctxt in

878+ !ctxt' = addDef n (TyDecl nt ty, False, Public, Unchecked, EmptyMI) ctxt in

870879 uctxt { definitions = ctxt' }

871880

872881addDatatype :: Datatype Name -> Context -> Context

@@ -874,14 +883,14 @@ addDatatype (Data n tag ty unique cons) uctxt

874883 = let ctxt = definitions uctxt

875884 ty' = normalise uctxt [] ty

876885 !ctxt' = addCons 0 cons (addDef n

877− (TyDecl (TCon tag (arity ty')) ty, Public, Unchecked, EmptyMI) ctxt) in

886+ (TyDecl (TCon tag (arity ty')) ty, True, Public, Unchecked, EmptyMI) ctxt) in

878887 uctxt { definitions = ctxt' }

879888 where

880889 addCons tag [] ctxt = ctxt

881890 addCons tag ((n, ty) : cons) ctxt

882891 = let ty' = normalise uctxt [] ty in

883892 addCons (tag+1) cons (addDef n

884− (TyDecl (DCon tag (arity ty') unique) ty, Public, Unchecked, EmptyMI) ctxt)

893+ (TyDecl (DCon tag (arity ty') unique) ty, True, Public, Unchecked, EmptyMI) ctxt)

885894

886895-- FIXME: Too many arguments! Refactor all these Bools.

887896--

@@ -923,7 +932,7 @@ addCasedef n ei ci@(CaseInfo inline alwaysInline tcdict)

923932 (args_rt, sc_rt)

924933 op = (CaseOp (ci { case_inlinable = inlc })

925934 ty argtys ps_in ps_tot cdef,

926− access, Unchecked, EmptyMI)

935+ False, access, Unchecked, EmptyMI)

927936 in return $ addDef n op ctxt

928937-- other -> tfail (Msg $ "Error adding case def: " ++ show other)

929938 return uctxt { definitions = ctxt' }

@@ -933,15 +942,15 @@ simplifyCasedef :: Name -> ErasureInfo -> Context -> TC Context

933942simplifyCasedef n ei uctxt

934943 = do let ctxt = definitions uctxt

935944 ctxt' <- case lookupCtxt n ctxt of

936− [(CaseOp ci ty atys [] ps _, acc, tot, metainf)] ->

945+ [(CaseOp ci ty atys [] ps _, inj, acc, tot, metainf)] ->

937946 return ctxt -- nothing to simplify (or already done...)

938− [(CaseOp ci ty atys ps_in ps cd, acc, tot, metainf)] ->

947+ [(CaseOp ci ty atys ps_in ps cd, inj, acc, tot, metainf)] ->

939948 do let ps_in' = map simpl ps_in

940949 pdef = map debind ps_in'

941950 CaseDef args sc _ <- simpleCase False (STerm Erased) False CompileTime emptyFC [] atys pdef ei

942951 return $ addDef n (CaseOp ci

943952 ty atys ps_in' ps (cd { cases_totcheck = (args, sc) }),

944− acc, tot, metainf) ctxt

953+ inj, acc, tot, metainf) ctxt

945954

946955 _ -> return ctxt

947956 return uctxt { definitions = ctxt' }

@@ -961,10 +970,10 @@ addOperator :: Name -> Type -> Int -> ([Value] -> Maybe Value) ->

961970 Context -> Context

962971addOperator n ty a op uctxt

963972 = let ctxt = definitions uctxt

964− ctxt' = addDef n (Operator ty a op, Public, Unchecked, EmptyMI) ctxt in

973+ ctxt' = addDef n (Operator ty a op, False, Public, Unchecked, EmptyMI) ctxt in

965974 uctxt { definitions = ctxt' }

966975

967−tfst (a, _, _, _) = a

976+tfst (a, _, _, _, _) = a

968977

969978lookupNames :: Name -> Context -> [Name]

970979lookupNames n ctxt

@@ -1041,10 +1050,10 @@ lookupP_all :: Bool -> Bool -> Name -> Context -> [Term]

10411050lookupP_all all exact n ctxt

10421051 = do (n', def) <- names

10431052 p <- case def of

1044− (Function ty tm, a, _, _) -> return (P Ref n' ty, a)

1045− (TyDecl nt ty, a, _, _) -> return (P nt n' ty, a)

1046− (CaseOp _ ty _ _ _ _, a, _, _) -> return (P Ref n' ty, a)

1047− (Operator ty _ _, a, _, _) -> return (P Ref n' ty, a)

1053+ (Function ty tm, inj, a, _, _) -> return (P Ref n' ty, a)

1054+ (TyDecl nt ty, _, a, _, _) -> return (P nt n' ty, a)

1055+ (CaseOp _ ty _ _ _ _, inj, a, _, _) -> return (P Ref n' ty, a)

1056+ (Operator ty _ _, inj, a, _, _) -> return (P Ref n' ty, a)

10481057 case snd p of

10491058 Hidden -> if all then return (fst p) else []

10501059 Private -> if all then return (fst p) else []

@@ -1071,24 +1080,28 @@ lookupDefAcc :: Name -> Bool -> Context ->

10711080lookupDefAcc n mkpublic ctxt

10721081 = map mkp $ lookupCtxt n (definitions ctxt)

10731082 -- io_bind a special case for REPL prettiness

1074− where mkp (d, a, _, _) = if mkpublic && (not (n == sUN "io_bind" || n == sUN "io_return"))

1075− then (d, Public) else (d, a)

1083+ where mkp (d, inj, a, _, _) = if mkpublic && (not (n == sUN "io_bind" || n == sUN "io_return"))

1084+ then (d, Public) else (d, a)

10761085

10771086lookupDefAccExact :: Name -> Bool -> Context ->

10781087 Maybe (Def, Accessibility)

10791088lookupDefAccExact n mkpublic ctxt

10801089 = fmap mkp $ lookupCtxtExact n (definitions ctxt)

10811090 -- io_bind a special case for REPL prettiness

1082− where mkp (d, a, _, _) = if mkpublic && (not (n == sUN "io_bind" || n == sUN "io_return"))

1083− then (d, Public) else (d, a)

1091+ where mkp (d, inj, a, _, _) = if mkpublic && (not (n == sUN "io_bind" || n == sUN "io_return"))

1092+ then (d, Public) else (d, a)

10841093

10851094lookupTotal :: Name -> Context -> [Totality]

10861095lookupTotal n ctxt = map mkt $ lookupCtxt n (definitions ctxt)

1087− where mkt (d, a, t, m) = t

1096+ where mkt (d, inj, a, t, m) = t

10881097

10891098lookupTotalExact :: Name -> Context -> Maybe Totality

10901099lookupTotalExact n ctxt = fmap mkt $ lookupCtxtExact n (definitions ctxt)

1091− where mkt (d, a, t, m) = t

1100+ where mkt (d, inj, a, t, m) = t

1101+

1102+lookupInjectiveExact :: Name -> Context -> Maybe Injectivity

1103+lookupInjectiveExact n ctxt = fmap mkt $ lookupCtxtExact n (definitions ctxt)

1104+ where mkt (d, inj, a, t, m) = inj

10921105

10931106-- Check if a name is reducible in the type checker. Partial definitions

10941107-- are not reducible (so treated as a constant)

@@ -1100,10 +1113,10 @@ tcReducible n ctxt = case lookupTotalExact n ctxt of

11001113

11011114lookupMetaInformation :: Name -> Context -> [MetaInformation]

11021115lookupMetaInformation n ctxt = map mkm $ lookupCtxt n (definitions ctxt)

1103− where mkm (d, a, t, m) = m

1116+ where mkm (d, inj, a, t, m) = m

11041117

11051118lookupNameTotal :: Name -> Context -> [(Name, Totality)]

1106−lookupNameTotal n = map (\(n, (_, _, t, _)) -> (n, t)) . lookupCtxtName n . definitions

1119+lookupNameTotal n = map (\(n, (_, _, _, t, _)) -> (n, t)) . lookupCtxtName n . definitions

11071120

11081121

11091122lookupVal :: Name -> Context -> [Value]

src/Idris/Core/Unify.hs+3−1

@@ -292,6 +292,8 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

292292

293293 injective (P (DCon _ _ _) _ _) = True

294294 injective (P (TCon _ _) _ _) = True

295+ injective (P Ref n _)

296+ | Just i <- lookupInjectiveExact n ctxt = i

295297 injective (App _ f a) = injective f -- && injective a

296298 injective _ = False

297299

@@ -573,7 +575,7 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

573575

574576 rigid (P (DCon _ _ _) _ _) = True

575577 rigid (P (TCon _ _) _ _) = True

576− rigid t@(P Ref _ _) = inenv t || globmetavar t

578+ rigid t@(P Ref _ _) = inenv t || globmetavar t

577579 rigid (Constant _) = True

578580 rigid (App _ f a) = rigid f && rigid a

579581 rigid t = not (metavar t) || globmetavar t

src/Idris/Core/WHNF.hs+1

@@ -75,6 +75,7 @@ do_whnf ctxt env tm = eval env [] tm

7575 = let wp = case nt of

7676 DCon t a u -> WDCon t a u n (ty, env)

7777 TCon t a -> WTCon t a n (ty, env)

78+ Ref -> WPRef n (ty, env)

7879 _ -> WPRef n (ty, env)

7980 in

8081 case lookupDefExact n ctxt of

src/Idris/DeepSeq.hs+1

@@ -284,6 +284,7 @@ instance NFData IBCWrite where

284284 rnf (IBCAccess name accessibility) = rnf name `seq` rnf accessibility `seq` ()

285285 rnf (IBCMetaInformation name metaInformation) = rnf name `seq` rnf metaInformation `seq` ()

286286 rnf (IBCTotal name totality) = rnf name `seq` rnf totality `seq` ()

287+ rnf (IBCInjective name inj) = rnf name `seq` rnf inj `seq` ()

287288 rnf (IBCFlags name fnOpts) = rnf name `seq` rnf fnOpts `seq` ()

288289 rnf (IBCFnInfo name fnInfo) = rnf name `seq` rnf fnInfo `seq` ()

289290 rnf (IBCTrans name terms) = rnf name `seq` rnf terms `seq` ()

src/Idris/Directives.hs+5

@@ -42,6 +42,11 @@ directiveAction (DFreeze n') = do

4242 mapM_ (\n -> do

4343 setAccessibility n Frozen

4444 addIBC (IBCAccess n Frozen)) ns

45+directiveAction (DInjective n') = do

46+ ns <- allNamespaces n'

47+ mapM_ (\n -> do

48+ setInjectivity n True

49+ addIBC (IBCInjective n True)) ns

4550

4651directiveAction (DAccess acc) = do updateIState (\i -> i { default_access = acc })

4752

src/Idris/Elab/Class.hs+24−6

@@ -119,6 +119,11 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

119119 -- Elaborate the the top level methods

120120 mapM_ (rec_elabDecl info EAll info) (concat fns)

121121

122+ -- Flag all the top level data declarations as injective

123+ mapM_ (\n -> do setInjectivity n True

124+ addIBC (IBCInjective n True))

125+ (map fst (filter (\(_, (inj, _, _, _, _)) -> inj) imethods))

126+

122127 -- add the default definitions

123128 mapM_ (rec_elabDecl info EAll info) (concat (map (snd.snd) defs))

124129 addIBC (IBCClass tn)

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

130135 maybe [] (\(conN, conNFC) -> [(conNFC, AnnName conN Nothing Nothing Nothing)]) mcn

131136

132137 where

133− nodoc (n, (_, _, o, t)) = (n, (o, t))

138+ nodoc (n, (inj, _, _, o, t)) = (n, (inj, o, t))

134139

135140 pibind [] x = x

136141 pibind ((n, ty): ns) x = PPi expl n NoFC ty (pibind ns (chkUniq ty x))

@@ -171,14 +176,26 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

171176 conbind [] x = x

172177

173178 getMName (PTy _ _ _ _ _ n nfc _) = nsroot n

179+ getMName (PData _ _ _ _ _ (PLaterdecl n nfc _)) = nsroot n

180+

174181 tdecl allmeths (PTy doc _ syn _ o n nfc t)

175182 = do t' <- implicit' info syn (map (\(n, _, _) -> n) ps ++ allmeths) n t

176183 logElab 2 $ "Method " ++ show n ++ " : " ++ showTmImpls t'

177184 return ( (n, (toExp (map (\(pn, _, _) -> pn) ps) Exp t')),

178− (n, (nfc, doc, o, (toExp (map (\(pn, _, _) -> pn) ps)

185+ (n, (False, nfc, doc, o, (toExp (map (\(pn, _, _) -> pn) ps)

186+ (\ l s p -> Imp l s p Nothing True) t'))),

187+ (n, (nfc, syn, o, t) ) )

188+ tdecl allmeths (PData doc _ syn _ _ (PLaterdecl n nfc t))

189+ = do let o = []

190+ t' <- implicit' info syn (map (\(n, _, _) -> n) ps ++ allmeths) n t

191+ logElab 2 $ "Data method " ++ show n ++ " : " ++ showTmImpls t'

192+ return ( (n, (toExp (map (\(pn, _, _) -> pn) ps) Exp t')),

193+ (n, (True, nfc, doc, o, (toExp (map (\(pn, _, _) -> pn) ps)

179194 (\ l s p -> Imp l s p Nothing True) t'))),

180195 (n, (nfc, syn, o, t) ) )

181− tdecl _ _ = ifail "Not allowed in a class declaration"

196+ tdecl allmeths (PData doc _ syn _ _ _)

197+ = ierror $ At fc (Msg "Data definitions not allowed in a class declaration")

198+ tdecl _ _ = ierror $ At fc (Msg "Not allowed in a class declaration")

182199

183200 -- Create default definitions

184201 defdecl mtys c d@(PClauses fc opts n cs) =

@@ -190,13 +207,14 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

190207 PClauses fc (o ++ opts) n cs]

191208 logElab 1 (show ds)

192209 return (n, ((defaultdec n, ds!!1), ds))

193− _ -> ifail $ show n ++ " is not a method"

210+ _ -> ierror $ At fc (Msg (show n ++ " is not a method"))

194211 defdecl _ _ _ = ifail "Can't happen (defdecl)"

195212

196213 defaultdec (UN n) = sUN ("default#" ++ str n)

197214 defaultdec (NS n ns) = NS (defaultdec n) ns

198215

199216 tydecl (PTy{}) = True

217+ tydecl (PData _ _ _ _ _ _) = True

200218 tydecl _ = False

201219 instdecl (PInstance{}) = True

202220 instdecl _ = False

@@ -233,10 +251,10 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

233251 tfun :: Name -- ^ The name of the class

234252 -> PTerm -- ^ A constraint for the class, to be inserted under the implicit bindings

235253 -> SyntaxInfo -> [Name] -- ^ All the method names

236− -> (Name, (FC, Docstring (Either Err PTerm), FnOpts, PTerm))

254+ -> (Name, (Bool, FC, Docstring (Either Err PTerm), FnOpts, PTerm))

237255 -- ^ The present declaration

238256 -> Idris [PDecl]

239− tfun cn c syn all (m, (mfc, doc, o, ty))

257+ tfun cn c syn all (m, (isdata, mfc, doc, o, ty))

240258 = do let ty' = expandMethNS syn (insertConstraint c all ty)

241259 let mnames = take (length all) $ map (\x -> sMN x "meth") [0..]

242260 let capp = PApp fc (PRef fc [] cn) (map (pexp . PRef fc []) mnames)

src/Idris/Elab/Instance.hs+35−1

@@ -123,7 +123,7 @@ elabInstance info syn doc argDocs what fc cs parents acc opts n nfc ps pextra t

123123 logElab 3 $ "Head var types " ++ show headVarTypes ++ " from " ++ show ty

124124

125125 let all_meths = map (nsroot . fst) (class_methods ci)

126− let mtys = map (\ (n, (op, t)) ->

126+ let mtys = map (\ (n, (inj, op, t)) ->

127127 let t_in = substMatchesShadow ips pnames t

128128 mnamemap =

129129 map (\n -> (n, PApp fc (PRef fc [] (decorate ns iname n))

@@ -139,6 +139,7 @@ elabInstance info syn doc argDocs what fc cs parents acc opts n nfc ps pextra t

139139 logElab 3 ("After defaults: " ++ show ds_defs ++ "\n")

140140 let ds' = reorderDefs (map fst (class_methods ci)) $ ds_defs

141141 logElab 1 ("Reordered: " ++ show ds' ++ "\n")

142+

142143 mapM_ (warnMissing ds' ns iname) (map fst (class_methods ci))

143144 mapM_ (checkInClass (map fst (class_methods ci))) (concatMap defined ds')

144145 let wbTys = map mkTyDecl mtys

@@ -187,6 +188,8 @@ elabInstance info syn doc argDocs what fc cs parents acc opts n nfc ps pextra t

187188 let wbVals' = map (addParams prop_params) wbVals

188189

189190 mapM_ (rec_elabDecl info EAll info) wbVals'

191+

192+ mapM_ (checkInjectiveDef fc (class_methods ci)) (zip ds' wbVals')

190193

191194 pop_estack

192195

@@ -436,6 +439,37 @@ addParams ps (PClauses fc opts n cs) = PClauses fc opts n (map addCParams cs)

436439

437440addParams ps d = d

438441

442+-- Check a given method definition is injective, if the class info

443+-- says it needs to be.

444+-- Takes originally written decl and the one with name decoration, so

445+-- we know which name to look up.

446+checkInjectiveDef :: FC -> [(Name, (Bool, FnOpts, PTerm))] ->

447+ (PDecl, PDecl) -> Idris ()

448+checkInjectiveDef fc ns (PClauses _ _ n cs, PClauses _ _ elabn _)

449+ | Just (True, _, _) <- clookup n ns

450+ = do ist <- getIState

451+ case lookupDefExact elabn (tt_ctxt ist) of

452+ Just (CaseOp _ _ _ _ _ cdefs) ->

453+ checkInjectiveCase ist (snd (cases_compiletime cdefs))

454+ where

455+ checkInjectiveCase ist (STerm tm)

456+ = checkInjectiveApp ist (fst (unApply tm))

457+ checkInjectiveCase _ _ = notifail

458+

459+ checkInjectiveApp ist (P (TCon _ _) n _) = return ()

460+ checkInjectiveApp ist (P (DCon _ _ _) n _) = return ()

461+ checkInjectiveApp ist (P Ref n _)

462+ | Just True <- lookupInjectiveExact n (tt_ctxt ist) = return ()

463+ checkInjectiveApp ist (P Ref n _) = notifail

464+ checkInjectiveApp _ _ = notifail

465+

466+ notifail = ierror $ At fc (Msg (show n ++ " must be defined by a type or data constructor"))

467+

468+ clookup n [] = Nothing

469+ clookup n ((n', d) : ds) | nsroot n == nsroot n' = Just d

470+ | otherwise = Nothing

471+checkInjectiveDef fc ns _ = return()

472+

439473checkInjectiveArgs :: FC -> Name -> [Int] -> Maybe Type -> Idris ()

440474checkInjectiveArgs fc n ds Nothing = return ()

441475checkInjectiveArgs fc n ds (Just ty)

src/Idris/IBC.hs+11−2

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

4040import Codec.Archive.Zip

4141

4242ibcVersion :: Word16

43−ibcVersion = 140

43+ibcVersion = 141

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

@@ -95,6 +95,7 @@ data IBCFile = IBCFile { ver :: Word16,

9595 ibc_deprecated :: ![(Name, String)],

9696 ibc_defs :: ![(Name, Def)],

9797 ibc_total :: ![(Name, Totality)],

98+ ibc_injective :: ![(Name, Injectivity)],

9899 ibc_access :: ![(Name, Accessibility)],

99100 ibc_fragile :: ![(Name, String)]

100101 }

@@ -104,7 +105,7 @@ deriving instance Binary IBCFile

104105!-}

105106

106107initIBC :: IBCFile

107−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] [] [] [] [] [] [] []

108+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] [] [] [] [] [] [] [] []

108109

109110hasValidIBCVersion :: FilePath -> Idris Bool

110111hasValidIBCVersion fp = do

@@ -197,6 +198,7 @@ entries i = catMaybes [Just $ toEntry "ver" 0 (encode $ ver i),

197198 makeEntry "ibc_deprecated" (ibc_deprecated i),

198199 makeEntry "ibc_defs" (ibc_defs i),

199200 makeEntry "ibc_total" (ibc_total i),

201+ makeEntry "ibc_injective" (ibc_injective i),

200202 makeEntry "ibc_access" (ibc_access i),

201203 makeEntry "ibc_fragile" (ibc_fragile i)]

202204

@@ -300,6 +302,7 @@ ibc i (IBCAccess n a) f = return f { ibc_access = (n,a) : ibc_access f }

300302ibc i (IBCFlags n a) f = return f { ibc_flags = (n,a) : ibc_flags f }

301303ibc i (IBCFnInfo n a) f = return f { ibc_fninfo = (n,a) : ibc_fninfo f }

302304ibc i (IBCTotal n a) f = return f { ibc_total = (n,a) : ibc_total f }

305+ibc i (IBCInjective n a) f = return f { ibc_injective = (n,a) : ibc_injective f }

303306ibc i (IBCTrans n t) f = return f { ibc_transforms = (n, t) : ibc_transforms f }

304307ibc i (IBCErrRev t) f = return f { ibc_errRev = t : ibc_errRev f }

305308ibc i (IBCLineApp fp l t) f

@@ -394,6 +397,7 @@ process reexp phase archive fn = do

394397 processDeprecate archive

395398 processDefs archive

396399 processTotal archive

400+ processInjective archive

397401 processAccess reexp phase archive

398402 processFragile archive

399403

@@ -718,6 +722,11 @@ processTotal ar = do

718722 ds <- getEntry [] "ibc_total" ar

719723 mapM_ (\ (n, a) -> updateIState (\i -> i { tt_ctxt = setTotal n a (tt_ctxt i) })) ds

720724

725+processInjective :: Archive -> Idris ()

726+processInjective ar = do

727+ ds <- getEntry [] "ibc_injective" ar

728+ mapM_ (\ (n, a) -> updateIState (\i -> i { tt_ctxt = setInjective n a (tt_ctxt i) })) ds

729+

721730processTotalityCheckError :: Archive -> Idris ()

722731processTotalityCheckError ar = do

723732 es <- getEntry [] "ibc_totcheckfail" ar

src/Idris/Parser.hs+8−1

@@ -877,7 +877,10 @@ classBlock syn = do reservedHL "where"

877877 ist <- get

878878 let cd' = annotate syn ist cd

879879

880− ds <- many (notEndBlock >> try (instance_ True syn) <|> fnDecl syn)

880+ ds <- many (notEndBlock >> try (instance_ True syn)

881+ <|> do x <- data_ syn

882+ return [x]

883+ <|> fnDecl syn)

881884 closeBlock

882885 return (cn, cd', concat ds)

883886 <?> "class block"

@@ -1377,6 +1380,10 @@ directive syn = do try (lchar '%' *> reserved "lib")

13771380 return [PDirective (DHide n)]

13781381 <|> do try (lchar '%' *> reserved "freeze"); n <- fst <$> iName []

13791382 return [PDirective (DFreeze n)]

1383+ -- injectivity assertins are intended for debugging purposes

1384+ -- only, and won't be documented/could be removed at any point

1385+ <|> do try (lchar '%' *> reserved "assert_injective"); n <- fst <$> fnName

1386+ return [PDirective (DInjective n)]

13801387 <|> do try (lchar '%' *> reserved "access")

13811388 acc <- accessibility

13821389 ist <- get

src/Idris/Parser/Data.hs+11−7

@@ -204,18 +204,21 @@ data_ syn = do (doc, argDocs, acc, dataOpts) <- try (do

204204 fc <- getFC

205205 (tyn_in, nfc) <- fnName

206206 (do try (lchar ':')

207− popIndent

208207 ty <- typeExpr (allowImp syn)

209208 let tyn = expandNS syn tyn_in

210− option (PData doc argDocs syn fc dataOpts (PLaterdecl tyn nfc ty)) (do

209+ d <- option (PData doc argDocs syn fc dataOpts (PLaterdecl tyn nfc ty)) (do

211210 reservedHL "where"

212211 cons <- indentedBlock (constructor syn)

213212 accData acc tyn (map (\ (_, _, n, _, _, _, _) -> n) cons)

214− return $ PData doc argDocs syn fc dataOpts (PDatadecl tyn nfc ty cons))) <|> (do

215− args <- many (fst <$> name)

213+ return $ PData doc argDocs syn fc dataOpts (PDatadecl tyn nfc ty cons))

214+ terminator

215+ return d) <|> (do

216+ args <- many (do notEndApp

217+ x <- fst <$> name

218+ return x)

216219 let ty = bindArgs (map (const (PType fc)) args) (PType fc)

217220 let tyn = expandNS syn tyn_in

218− option (PData doc argDocs syn fc dataOpts (PLaterdecl tyn nfc ty)) (do

221+ d <- option (PData doc argDocs syn fc dataOpts (PLaterdecl tyn nfc ty)) (do

219222 try (lchar '=') <|> do reservedHL "where"

220223 let kw = (if DefaultEliminator `elem` dataOpts then "%elim" else "") ++ (if Codata `elem` dataOpts then "co" else "") ++ "data "

221224 let n = show tyn_in ++ " "

@@ -228,13 +231,14 @@ data_ syn = do (doc, argDocs, acc, dataOpts) <- try (do

228231 let fix3 = s ++ ": " ++ ss ++ " -> Type where\n ..."

229232 fail $ fixErrorMsg "unexpected \"where\"" [fix1, fix2, fix3]

230233 cons <- sepBy1 (simpleConstructor (syn { withAppAllowed = False })) (reservedOp "|")

231− terminator

232234 let conty = mkPApp fc (PRef fc [] tyn) (map (PRef fc []) args)

233235 cons' <- mapM (\ (doc, argDocs, x, xfc, cargs, cfc, fs) ->

234236 do let cty = bindArgs cargs conty

235237 return (doc, argDocs, x, xfc, cty, cfc, fs)) cons

236238 accData acc tyn (map (\ (_, _, n, _, _, _, _) -> n) cons')

237− return $ PData doc argDocs syn fc dataOpts (PDatadecl tyn nfc ty cons')))

239+ return $ PData doc argDocs syn fc dataOpts (PDatadecl tyn nfc ty cons'))

240+ terminator

241+ return d)

238242 <?> "data type declaration"

239243 where

240244 mkPApp :: FC -> PTerm -> [PTerm] -> PTerm

src/Idris/TypeSearch.hs+2−2

@@ -92,8 +92,8 @@ searchPred istate ty1 = matcher where

9292 matcher = matchTypesBulk istate maxScore ty1

9393

9494

95−typeFromDef :: (Def, b, c, d) -> Maybe Type

96−typeFromDef (def, _, _, _) = get def where

95+typeFromDef :: (Def, i, b, c, d) -> Maybe Type

96+typeFromDef (def, _, _, _, _) = get def where

9797 get :: Def -> Maybe Type

9898 get (Function ty _) = Just ty

9999 get (TyDecl _ ty) = Just ty