9b28211 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Stylize fixes

commit9b28211ca91e58c2f13deb74acc7ba8cff75d36e authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 26 Jan 2017, 09:26 (10 years ago) parentab56c6f

3 files changed+24−24

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+5−5 src/Idris/Elab/Interface.hs+17−17 src/Idris/Elab/Term.hs+2−2

src/Idris/AbsSyntax.hs+5−5

@@ -38,10 +38,10 @@ import System.IO.Error (tryIOError)

3838

3939import Data.Generics.Uniplate.Data (descend, descendM)

4040

41+import Debug.Trace

4142import Util.DynamicLinker

4243import Util.Pretty

4344import Util.System

44−import Debug.Trace

4545

4646getContext :: Idris Context

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

@@ -503,7 +503,7 @@ addInterface :: Name -> InterfaceInfo -> Idris ()

503503addInterface n i

504504 = do ist <- getIState

505505 let i' = case lookupCtxt n (idris_interfaces ist) of

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

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

507507 interface_implementations i }

508508 _ -> i

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

@@ -518,7 +518,7 @@ updateIMethods n meths

518518 where

519519 update [] = []

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

521− | Just ty <- lookup n meths

521+ | Just ty <- lookup n meths

522522 = (n, (b, opts, ty)) : update rest

523523 | otherwise = m : update rest

524524

@@ -1943,7 +1943,7 @@ addImpl' inpat env infns imp_meths ist ptm

19431943 ai inpat qq env ds (PPi p n nfc ty sc)

19441944 = let ty' = ai inpat qq env ds ty

19451945 env' = if n `elem` imp_meths then env

1946− else

1946+ else

19471947 ((n, Just ty) : env)

19481948 sc' = ai inpat qq env' ds sc in

19491949 PPi p n nfc ty' sc'

@@ -2400,7 +2400,7 @@ substMatchesShadow nmap shs t = sm shs t where

24002400 PPi p x' fc (sm (x':xs) (substMatch x (PRef emptyFC [] x') t))

24012401 (sm (x':xs) (substMatch x (PRef emptyFC [] x') sc))

24022402 | otherwise = PPi p x fc (sm xs t) (sm (x : xs) sc)

2403− sm xs (PLet fc x xfc val t sc)

2403+ sm xs (PLet fc x xfc val t sc)

24042404 = PLet fc x xfc (sm xs val) (sm xs t) (sm xs sc)

24052405 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)

24062406 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)

src/Idris/Elab/Interface.hs+17−17

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

107107 concatMap (namesIn [] ist) (map snd constraints)

108108

109109 mapM_ (checkConstraintName (map (\(x, _, _) -> x) ps)) constraintNames

110−

110+

111111 let pre_ddecl = PLaterdecl tn NoFC tty

112112 -- Elaborate the interface header

113113 elabData info (syn { no_imp = no_imp syn ++ mnames,

@@ -121,20 +121,20 @@ elabInterface info_in syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

121121 let (methods, imethods)

122122 = unzip (map (\ (x, y, z) -> (x, y)) ims)

123123 let defaults = map (\ (x, (y, z)) -> (x,y)) defs

124−

124+

125125 addInterface tn (CI cn (map nodoc imethods) defaults idecls

126126 (map (\(n, _, _) -> n) impps)

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)

134134 cfns <- mapM (cfun cn constraint syn (map fst imethods)) constraints

135135 let (cfnTyDecls, cfnDefs) = unzip cfns

136136 mapM_ (rec_elabDecl info EAll info) cfnTyDecls

137−

137+

138138 -- for each method, build a top level function

139139 -- 'tfun' builds appropriate implicits for the constructor

140140 -- declaration

@@ -142,12 +142,12 @@ elabInterface info_in 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

147147

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

149−

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

149+

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

151151 (zip fullmnames elabMethTys)

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

153153

@@ -155,9 +155,9 @@ elabInterface info_in syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

155155 -- types with the parameter removed

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

157157 updateIMethods tn storemeths

158−

158+

159159 -- build implementation constructor type

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

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

161161 conbind constraints $

162162 pibind (map (mkMethTy False cpos) (zip fullmnames elabMethTys))

163163 constraint

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

200200

201201 where

202202 info = info_in { noCaseLift = tn : noCaseLift info_in }

203−

203+

204204 getElabMethTy :: Name -> Idris PTerm

205205 getElabMethTy n = do ist <- getIState

206206 let impls = case lookupCtxtExact n (idris_implicits ist) of

@@ -217,16 +217,16 @@ elabInterface info_in syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

217217 findConstraint = findPos 0

218218 where

219219 findPos i (PPi _ _ _ (PRef _ _ n) sc)

220− | n == tn = i

220+ | n == tn = i

221221 findPos i (PPi _ _ _ (PApp _ (PRef _ _ n) _) sc)

222− | n == tn = i

222+ | n == tn = i

223223 findPos i (PPi _ _ _ ty sc) = findPos (i + 1) sc

224224 findPos i _ = -1 -- Can't happen!

225225

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

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

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

229− mkMethTy keepns cpos (n, tm)

229+ mkMethTy keepns cpos (n, tm)

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

231231 where

232232 num = case lookup n cpos of

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

237237 dropPis _ tm = tm

238238

239239 dropImp (PApp fc (PRef fcr fcs n) args)

240− | Just pos <- lookup n cpos

240+ | Just pos <- lookup n cpos

241241 = PApp fc (PRef fcr fcs (nsroot n))

242242 (filter notConstr (drop (pos + 1) args))

243243 dropImp (PApp fc f args)

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

289289

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

291291 getMName (PData _ _ _ _ _ (PLaterdecl n nfc _)) = nsroot n

292−

292+

293293 getFullMName (PTy _ _ _ _ _ n nfc _) = n

294294 getFullMName (PData _ _ _ _ _ (PLaterdecl n nfc _)) = n

295295

@@ -382,8 +382,8 @@ elabInterface info_in syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

382382 return (PTy doc [] syn fc o m mfc ty',

383383 PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []])

384384

385− updateIMethod :: [(Name, PTerm)] ->

386− (Name, (a, b, c, d, PTerm)) ->

385+ updateIMethod :: [(Name, PTerm)] ->

386+ (Name, (a, b, c, d, PTerm)) ->

387387 (Name, (a, b, c, d, PTerm))

388388 updateIMethod ns tm@(n, (isf, mfc, doc, o, ty))

389389 | Just ty' <- lookup (nsroot n) ns = (n, (isf, mfc, doc, o, ty'))

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

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

11681168 _ -> False

11691169 tcName _ = False

11701170

1171− isNotLift env n

1171+ isNotLift env n

11721172 = case lookupBinder n env of

1173− Just ty ->

1173+ Just ty ->

11741174 case unApply (binderTy ty) of

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

11761176 _ -> False