ab56c6f · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

'case' in interface methods now works

ab56c6fEdwin Brady10 years ago

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

compare with master

unifiedsplit

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

36 mx >>= \x =>

37 pure (f x)

38 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

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

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

src/Idris/AbsSyntax.hs+15

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

41import Util.DynamicLinker

42import Util.Pretty

43import Util.System

44+import Debug.Trace

45getContext :: Idris Context

46getContext :: Idris Context

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

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

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

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

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

506 interface_implementations i }

507 interface_implementations i }

507 _ -> i

508 _ -> 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"

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

517 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

509

524

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

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

511addRecord n ri = do ist <- getIState

526addRecord n ri = do ist <- getIState

src/Idris/AbsSyntaxTree.hs+3−3

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

63 , elabFC :: Maybe FC

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

65 , pe_depth :: Int

66−

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

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

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

69 , rhs_trans :: PTerm -> PTerm

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

71 }

73toplevel :: 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")

76toplevelWith :: 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")

79eInfoNames :: ElabInfo -> [Name]

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

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

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

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

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

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

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

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

78 (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

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

128 (map snd constraints)

129 [] dets)

130−

130+

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

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

133 -- of the interface)

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

142 (map fst imethods)) imethods

143 let (fnTyDecls, fnDefs) = unzip fns

144 mapM_ (rec_elabDecl info EAll info) fnTyDecls

145−

145+

146 elabMethTys <- mapM getElabMethTy fullmnames

147+

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

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

148

149

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

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

150 (zip fullmnames elabMethTys)

151 (zip fullmnames elabMethTys)

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

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

152

153

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+

153 -- build implementation constructor type

159 -- build implementation constructor type

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

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

155 conbind constraints $

161 conbind constraints $

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

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

157 constraint

163 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−

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

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

163

165

164−

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

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

166 let ddecl = PDatadecl tn NoFC tty cons

167 let ddecl = PDatadecl tn NoFC tty cons

167

168

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

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

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

199

200

200 where

201 where

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

203+

201 getElabMethTy :: Name -> Idris PTerm

204 getElabMethTy :: Name -> Idris PTerm

202 getElabMethTy n = do ist <- getIState

205 getElabMethTy n = do ist <- getIState

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

207+ Just i -> i

208+ Nothing -> []

203 case lookupTyExact n (tt_ctxt ist) of

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

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

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

206

212

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

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

219

225

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

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

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

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

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

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

229+ mkMethTy keepns cpos (n, tm)

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

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

224 where

231 where

225 num = case lookup n cpos of

232 num = case lookup n cpos of

226 Just i -> i + 1

233 Just i -> i + 1

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

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

1097 ptm <- get_term

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

1099

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

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

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

1102 inOpts)

1103

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

1168 _ -> False

1169 tcName _ = False

1170

1171+ isNotLift env n

1171− isConstraint env n = case lookupBinder n env of

1172+ = case lookupBinder n env of

1173+ Just ty ->

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

1174+ case unApply (binderTy ty) of

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

1176+ _ -> False

1173− _ -> False

1177+ _ -> False

1174

1178

1175 usedIn ns (n, b)

1179 usedIn ns (n, b)

1176 = n `elem` ns

1180 = n `elem` ns

src/Idris/ElabDecls.hs+1−1

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

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

70recinfo :: 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'

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

74elabMain :: Idris Term