ab56c6f · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

'case' in interface methods now works

At least partially: specifically, it works as long as there are no other methods of the interface referenced in the body of the case.

commitab56c6f0e687bd7047901bd13e131ed5acd89309 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 25 Jan 2017, 18:30 (10 years ago) parent57ea7fe

6 files changed+47−21

compare with master

unifiedsplit

libs/contrib/Interfaces/Verified.idr+1−1 src/Idris/AbsSyntax.hs+15 src/Idris/AbsSyntaxTree.hs+3−3 src/Idris/Elab/Interface.hs+19−12 src/Idris/Elab/Term.hs+8−4 src/Idris/ElabDecls.hs+1−1

libs/contrib/Interfaces/Verified.idr+1−1

@@ -36,7 +36,7 @@ interface (Monad m, VerifiedApplicative m) => VerifiedMonad (m : Type -> Type) w

3636 mx >>= \x =>

3737 pure (f x)

3838 monadLeftIdentity : (x : a) -> (f : a -> m b) -> pure x >>= f = f x

39− monadRightIdentity : (mx : m a) -> mx >>= pure = mx

39+ monadRightIdentity : (mx : m a) -> mx >>= Applicative.pure = mx

4040 monadAssociativity : (mx : m a) -> (f : a -> m b) -> (g : b -> m c) ->

4141 (mx >>= f) >>= g = mx >>= (\x => f x >>= g)

4242

src/Idris/AbsSyntax.hs+15

@@ -41,6 +41,7 @@ import Data.Generics.Uniplate.Data (descend, descendM)

4141import Util.DynamicLinker

4242import Util.Pretty

4343import Util.System

44+import Debug.Trace

4445

4546getContext :: Idris Context

4647getContext = do i <- getIState; return (tt_ctxt i)

@@ -505,7 +506,21 @@ addInterface n i

505506 [c] -> i { interface_implementations = interface_implementations c ++

506507 interface_implementations i }

507508 _ -> i

509+ putIState $ ist { idris_interfaces = addDef n i' (idris_interfaces ist) }

510+

511+updateIMethods :: Name -> [(Name, PTerm)] -> Idris ()

512+updateIMethods n meths

513+ = do ist <- getIState

514+ let i = case lookupCtxtExact n (idris_interfaces ist) of

515+ Just c -> c { interface_methods = update (interface_methods c) }

516+ Nothing -> error "Can't happen updateIMethods"

508517 putIState $ ist { idris_interfaces = addDef n i (idris_interfaces ist) }

518+ where

519+ update [] = []

520+ update (m@(n, (b, opts, t)) : rest)

521+ | Just ty <- lookup n meths

522+ = (n, (b, opts, ty)) : update rest

523+ | otherwise = m : update rest

509524

510525addRecord :: Name -> RecordInfo -> Idris ()

511526addRecord n ri = do ist <- getIState

src/Idris/AbsSyntaxTree.hs+3−3

@@ -63,7 +63,7 @@ data ElabInfo = EInfo {

6363 , elabFC :: Maybe FC

6464 , constraintNS :: String -- ^ filename for adding to constraint variables

6565 , pe_depth :: Int

66−

66+ , noCaseLift :: [Name] -- ^ types which shouldn't be made arguments to case

6767 -- | We may, recursively, collect transformations to do on the rhs,

6868 -- e.g. rewriting recursive calls to functions defined by 'with'

6969 , rhs_trans :: PTerm -> PTerm

@@ -71,10 +71,10 @@ data ElabInfo = EInfo {

7171 }

7272

7373toplevel :: ElabInfo

74−toplevel = EInfo [] emptyContext id [] Nothing "(toplevel)" 0 id (\_ _ _ -> fail "Not implemented")

74+toplevel = EInfo [] emptyContext id [] Nothing "(toplevel)" 0 [] id (\_ _ _ -> fail "Not implemented")

7575

7676toplevelWith :: String -> ElabInfo

77−toplevelWith ns = EInfo [] emptyContext id [] Nothing ns 0 id (\_ _ _ -> fail "Not implemented")

77+toplevelWith ns = EInfo [] emptyContext id [] Nothing ns 0 [] id (\_ _ _ -> fail "Not implemented")

7878

7979eInfoNames :: ElabInfo -> [Name]

8080eInfoNames info = map fst (params info) ++ M.keys (inblock info)

src/Idris/Elab/Interface.hs+19−12

@@ -72,7 +72,7 @@ elabInterface :: ElabInfo

7272 -> Maybe (Name, FC) -- ^ implementation ctor name and location

7373 -> Docstring (Either Err PTerm) -- ^ implementation ctor docs

7474 -> Idris ()

75−elabInterface info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

75+elabInterface info_in syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

7676 = do let cn = fromMaybe (SN (ImplementationCtorN tn)) (fst <$> mcn)

7777 let constraint = PApp fc (PRef fc [] tn)

7878 (map (pexp . PRef fc []) (map (\(n, _, _) -> n) ps))

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

127127 (map (\(n, _, _) -> n) ps)

128128 (map snd constraints)

129129 [] dets)

130−

130+

131131 -- for each constraint, build a top level function to chase it

132132 -- elaborate types now, bodies later (after we've done the constructor

133133 -- of the interface)

@@ -142,26 +142,27 @@ elabInterface info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

142142 (map fst imethods)) imethods

143143 let (fnTyDecls, fnDefs) = unzip fns

144144 mapM_ (rec_elabDecl info EAll info) fnTyDecls

145−

145+

146146 elabMethTys <- mapM getElabMethTy fullmnames

147+

147148 logElab 3 $ "Method types:\n" ++ showSep "\n" (map showTmImpls elabMethTys)

148149

149150 let cpos = map (\ (n, ty) -> (n, findConstraint ty))

150151 (zip fullmnames elabMethTys)

151152 logElab 5 $ "Constraint pos: " ++ show cpos

152153

154+ -- Method types to store in the IState, taken from the elaborated

155+ -- types with the parameter removed

156+ let storemeths = map (mkMethTy True cpos) (zip fullmnames elabMethTys)

157+ updateIMethods tn storemeths

158+

153159 -- build implementation constructor type

154160 let cty = impbind [(pn, pt) | (pn, _, pt) <- impps ++ ps] $

155161 conbind constraints $

156− pibind (map (mkMethTy cpos) (zip fullmnames elabMethTys))

162+ pibind (map (mkMethTy False cpos) (zip fullmnames elabMethTys))

157163 constraint

158− let ctyOld = impbind [(pn, pt) | (pn, _, pt) <- impps ++ ps] $ conbind constraints

159− $ pibind (map (\ (n, ty) -> (nsroot n, ty)) methods)

160− constraint

161−

162164 logElab 3 $ "Constraint constructor type: " ++ showTmImpls cty

163165

164−

165166 let cons = [(cd, pDocs ++ mapMaybe memberDocs ds, cn, NoFC, cty, fc, [])]

166167 let ddecl = PDatadecl tn NoFC tty cons

167168

@@ -198,10 +199,15 @@ elabInterface info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

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

199200

200201 where

202+ info = info_in { noCaseLift = tn : noCaseLift info_in }

203+

201204 getElabMethTy :: Name -> Idris PTerm

202205 getElabMethTy n = do ist <- getIState

206+ let impls = case lookupCtxtExact n (idris_implicits ist) of

207+ Just i -> i

208+ Nothing -> []

203209 case lookupTyExact n (tt_ctxt ist) of

204− Just ty -> return (delabDirect ist ty)

210+ Just ty -> return (delabTy' ist impls ty False False False)

205211 Nothing -> tclift $ tfail (At fc (InternalMsg "Can't happen, elabMethTy"))

206212

207213 -- Find the argument position of the current interface in a method type

@@ -219,8 +225,9 @@ elabInterface info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

219225

220226 -- Make the method component of the constructor type by taking the

221227 -- elaborated top level method and removing the implicits/constraint

222− mkMethTy :: [(Name, Int)] -> (Name, PTerm) -> (Name, PTerm)

223− mkMethTy cpos (n, tm) = (nsroot n, dropPis num (mapPT dropImp tm))

228+ mkMethTy :: Bool -> [(Name, Int)] -> (Name, PTerm) -> (Name, PTerm)

229+ mkMethTy keepns cpos (n, tm)

230+ = (if keepns then n else nsroot n, dropPis num (mapPT dropImp tm))

224231 where

225232 num = case lookup n cpos of

226233 Just i -> i + 1

src/Idris/Elab/Term.hs+8−4

@@ -1097,7 +1097,7 @@ elab ist info emode opts fn tm

10971097 ptm <- get_term

10981098 let inOpts = (filter (/= scvn) (map fstEnv args)) \\ (concatMap (\x -> allNamesIn (snd x)) opts)

10991099

1100− let argsDropped = filter (\t -> isUnique envU t || isConstraint args t)

1100+ let argsDropped = filter (\t -> isUnique envU t || isNotLift args t)

11011101 (nub $ allNamesIn scr ++ inApp ptm ++

11021102 inOpts)

11031103

@@ -1168,9 +1168,13 @@ elab ist info emode opts fn tm

11681168 _ -> False

11691169 tcName _ = False

11701170

1171− isConstraint env n = case lookupBinder n env of

1172− Just ty -> False -- tcName (binderTy ty)

1173− _ -> False

1171+ isNotLift env n

1172+ = case lookupBinder n env of

1173+ Just ty ->

1174+ case unApply (binderTy ty) of

1175+ (P _ n _, _) -> n `elem` noCaseLift info

1176+ _ -> False

1177+ _ -> False

11741178

11751179 usedIn ns (n, b)

11761180 = n `elem` ns

src/Idris/ElabDecls.hs+1−1

@@ -68,7 +68,7 @@ import Debug.Trace

6868

6969-- | Top level elaborator info, supporting recursive elaboration

7070recinfo :: FC -> ElabInfo

71−recinfo fc = EInfo [] emptyContext id [] (Just fc) (fc_fname fc) 0 id elabDecl'

71+recinfo fc = EInfo [] emptyContext id [] (Just fc) (fc_fname fc) 0 [] id elabDecl'

7272

7373-- | Return the elaborated term which calls 'main'

7474elabMain :: Idris Term