git.iko.soy/Idris-dev
on master help sign in
Stylize fixes
9b28211Edwin Brady
src/Idris/AbsSyntax.hs+5−5
compare with master
unifiedsplit
@@ -38,10 +38,10 @@ import System.IO.Error (tryIOError)
38
38
39import Data.Generics.Uniplate.Data (descend, descendM)
39import Data.Generics.Uniplate.Data (descend, descendM)
40
40
41+import Debug.Trace
41import Util.DynamicLinker
42import Util.DynamicLinker
42import Util.Pretty
43import Util.Pretty
43import Util.System
44import Util.System
44−import Debug.Trace
45
45
46getContext :: Idris Context
46getContext :: Idris Context
47getContext = do i <- getIState; return (tt_ctxt i)
47getContext = do i <- getIState; return (tt_ctxt i)
@@ -503,7 +503,7 @@ addInterface :: Name -> InterfaceInfo -> Idris ()
503addInterface n i
503addInterface n i
504 = do ist <- getIState
504 = do ist <- getIState
505 let i' = case lookupCtxt n (idris_interfaces ist) of
505 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 ++
507 interface_implementations i }
507 interface_implementations i }
508 _ -> i
508 _ -> i
509 putIState $ ist { idris_interfaces = addDef n i' (idris_interfaces ist) }
509 putIState $ ist { idris_interfaces = addDef n i' (idris_interfaces ist) }
@@ -518,7 +518,7 @@ updateIMethods n meths
518 where
518 where
519 update [] = []
519 update [] = []
520 update (m@(n, (b, opts, t)) : rest)
520 update (m@(n, (b, opts, t)) : rest)
521− | Just ty <- lookup n meths
521+ | Just ty <- lookup n meths
522 = (n, (b, opts, ty)) : update rest
522 = (n, (b, opts, ty)) : update rest
523 | otherwise = m : update rest
523 | otherwise = m : update rest
524
524
@@ -1943,7 +1943,7 @@ addImpl' inpat env infns imp_meths ist ptm
1943 ai inpat qq env ds (PPi p n nfc ty sc)
1943 ai inpat qq env ds (PPi p n nfc ty sc)
1944 = let ty' = ai inpat qq env ds ty
1944 = let ty' = ai inpat qq env ds ty
1945 env' = if n `elem` imp_meths then env
1945 env' = if n `elem` imp_meths then env
1946− else
1946+ else
1947 ((n, Just ty) : env)
1947 ((n, Just ty) : env)
1948 sc' = ai inpat qq env' ds sc in
1948 sc' = ai inpat qq env' ds sc in
1949 PPi p n nfc ty' sc'
1949 PPi p n nfc ty' sc'
@@ -2400,7 +2400,7 @@ substMatchesShadow nmap shs t = sm shs t where
2400 PPi p x' fc (sm (x':xs) (substMatch x (PRef emptyFC [] x') t))
2400 PPi p x' fc (sm (x':xs) (substMatch x (PRef emptyFC [] x') t))
2401 (sm (x':xs) (substMatch x (PRef emptyFC [] x') sc))
2401 (sm (x':xs) (substMatch x (PRef emptyFC [] x') sc))
2402 | otherwise = PPi p x fc (sm xs t) (sm (x : xs) sc)
2402 | 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)
2404 = PLet fc x xfc (sm xs val) (sm xs t) (sm xs sc)
2404 = PLet fc x xfc (sm xs val) (sm xs t) (sm xs sc)
2405 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
2405 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
2406 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
2406 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
107 concatMap (namesIn [] ist) (map snd constraints)
107 concatMap (namesIn [] ist) (map snd constraints)
108
108
109 mapM_ (checkConstraintName (map (\(x, _, _) -> x) ps)) constraintNames
109 mapM_ (checkConstraintName (map (\(x, _, _) -> x) ps)) constraintNames
110−
110+
111 let pre_ddecl = PLaterdecl tn NoFC tty
111 let pre_ddecl = PLaterdecl tn NoFC tty
112 -- Elaborate the interface header
112 -- Elaborate the interface header
113 elabData info (syn { no_imp = no_imp syn ++ mnames,
113 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
121 let (methods, imethods)
121 let (methods, imethods)
122 = unzip (map (\ (x, y, z) -> (x, y)) ims)
122 = unzip (map (\ (x, y, z) -> (x, y)) ims)
123 let defaults = map (\ (x, (y, z)) -> (x,y)) defs
123 let defaults = map (\ (x, (y, z)) -> (x,y)) defs
124−
124+
125 addInterface tn (CI cn (map nodoc imethods) defaults idecls
125 addInterface tn (CI cn (map nodoc imethods) defaults idecls
126 (map (\(n, _, _) -> n) impps)
126 (map (\(n, _, _) -> n) impps)
127 (map (\(n, _, _) -> n) ps)
127 (map (\(n, _, _) -> n) ps)
128 (map snd constraints)
128 (map snd constraints)
129 [] dets)
129 [] dets)
130−
130+
131 -- for each constraint, build a top level function to chase it
131 -- for each constraint, build a top level function to chase it
132 -- elaborate types now, bodies later (after we've done the constructor
132 -- elaborate types now, bodies later (after we've done the constructor
133 -- of the interface)
133 -- of the interface)
134 cfns <- mapM (cfun cn constraint syn (map fst imethods)) constraints
134 cfns <- mapM (cfun cn constraint syn (map fst imethods)) constraints
135 let (cfnTyDecls, cfnDefs) = unzip cfns
135 let (cfnTyDecls, cfnDefs) = unzip cfns
136 mapM_ (rec_elabDecl info EAll info) cfnTyDecls
136 mapM_ (rec_elabDecl info EAll info) cfnTyDecls
137−
137+
138 -- for each method, build a top level function
138 -- for each method, build a top level function
139 -- 'tfun' builds appropriate implicits for the constructor
139 -- 'tfun' builds appropriate implicits for the constructor
140 -- declaration
140 -- declaration
@@ -142,12 +142,12 @@ elabInterface info_in syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd
142 (map fst imethods)) imethods
142 (map fst imethods)) imethods
143 let (fnTyDecls, fnDefs) = unzip fns
143 let (fnTyDecls, fnDefs) = unzip fns
144 mapM_ (rec_elabDecl info EAll info) fnTyDecls
144 mapM_ (rec_elabDecl info EAll info) fnTyDecls
145−
145+
146 elabMethTys <- mapM getElabMethTy fullmnames
146 elabMethTys <- mapM getElabMethTy fullmnames
147
147
148 logElab 3 $ "Method types:\n" ++ showSep "\n" (map showTmImpls elabMethTys)
148 logElab 3 $ "Method types:\n" ++ showSep "\n" (map showTmImpls elabMethTys)
149−
149+
150− let cpos = map (\ (n, ty) -> (n, findConstraint ty))
150+ let cpos = map (\ (n, ty) -> (n, findConstraint ty))
151 (zip fullmnames elabMethTys)
151 (zip fullmnames elabMethTys)
152 logElab 5 $ "Constraint pos: " ++ show cpos
152 logElab 5 $ "Constraint pos: " ++ show cpos
153
153
@@ -155,9 +155,9 @@ elabInterface info_in syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd
155 -- types with the parameter removed
155 -- types with the parameter removed
156 let storemeths = map (mkMethTy True cpos) (zip fullmnames elabMethTys)
156 let storemeths = map (mkMethTy True cpos) (zip fullmnames elabMethTys)
157 updateIMethods tn storemeths
157 updateIMethods tn storemeths
158−
158+
159 -- build implementation constructor type
159 -- build implementation constructor type
160− let cty = impbind [(pn, pt) | (pn, _, pt) <- impps ++ ps] $
160+ let cty = impbind [(pn, pt) | (pn, _, pt) <- impps ++ ps] $
161 conbind constraints $
161 conbind constraints $
162 pibind (map (mkMethTy False cpos) (zip fullmnames elabMethTys))
162 pibind (map (mkMethTy False cpos) (zip fullmnames elabMethTys))
163 constraint
163 constraint
@@ -200,7 +200,7 @@ elabInterface info_in syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd
200
200
201 where
201 where
202 info = info_in { noCaseLift = tn : noCaseLift info_in }
202 info = info_in { noCaseLift = tn : noCaseLift info_in }
203−
203+
204 getElabMethTy :: Name -> Idris PTerm
204 getElabMethTy :: Name -> Idris PTerm
205 getElabMethTy n = do ist <- getIState
205 getElabMethTy n = do ist <- getIState
206 let impls = case lookupCtxtExact n (idris_implicits ist) of
206 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
217 findConstraint = findPos 0
217 findConstraint = findPos 0
218 where
218 where
219 findPos i (PPi _ _ _ (PRef _ _ n) sc)
219 findPos i (PPi _ _ _ (PRef _ _ n) sc)
220− | n == tn = i
220+ | n == tn = i
221 findPos i (PPi _ _ _ (PApp _ (PRef _ _ n) _) sc)
221 findPos i (PPi _ _ _ (PApp _ (PRef _ _ n) _) sc)
222− | n == tn = i
222+ | n == tn = i
223 findPos i (PPi _ _ _ ty sc) = findPos (i + 1) sc
223 findPos i (PPi _ _ _ ty sc) = findPos (i + 1) sc
224 findPos i _ = -1 -- Can't happen!
224 findPos i _ = -1 -- Can't happen!
225
225
226 -- Make the method component of the constructor type by taking the
226 -- Make the method component of the constructor type by taking the
227 -- elaborated top level method and removing the implicits/constraint
227 -- elaborated top level method and removing the implicits/constraint
228 mkMethTy :: Bool -> [(Name, Int)] -> (Name, PTerm) -> (Name, PTerm)
228 mkMethTy :: Bool -> [(Name, Int)] -> (Name, PTerm) -> (Name, PTerm)
229− mkMethTy keepns cpos (n, tm)
229+ mkMethTy keepns cpos (n, tm)
230 = (if keepns then n else nsroot n, dropPis num (mapPT dropImp tm))
230 = (if keepns then n else nsroot n, dropPis num (mapPT dropImp tm))
231 where
231 where
232 num = case lookup n cpos of
232 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
237 dropPis _ tm = tm
237 dropPis _ tm = tm
238
238
239 dropImp (PApp fc (PRef fcr fcs n) args)
239 dropImp (PApp fc (PRef fcr fcs n) args)
240− | Just pos <- lookup n cpos
240+ | Just pos <- lookup n cpos
241 = PApp fc (PRef fcr fcs (nsroot n))
241 = PApp fc (PRef fcr fcs (nsroot n))
242 (filter notConstr (drop (pos + 1) args))
242 (filter notConstr (drop (pos + 1) args))
243 dropImp (PApp fc f args)
243 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
289
289
290 getMName (PTy _ _ _ _ _ n nfc _) = nsroot n
290 getMName (PTy _ _ _ _ _ n nfc _) = nsroot n
291 getMName (PData _ _ _ _ _ (PLaterdecl n nfc _)) = nsroot n
291 getMName (PData _ _ _ _ _ (PLaterdecl n nfc _)) = nsroot n
292−
292+
293 getFullMName (PTy _ _ _ _ _ n nfc _) = n
293 getFullMName (PTy _ _ _ _ _ n nfc _) = n
294 getFullMName (PData _ _ _ _ _ (PLaterdecl n nfc _)) = n
294 getFullMName (PData _ _ _ _ _ (PLaterdecl n nfc _)) = n
295
295
@@ -382,8 +382,8 @@ elabInterface info_in syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd
382 return (PTy doc [] syn fc o m mfc ty',
382 return (PTy doc [] syn fc o m mfc ty',
383 PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []])
383 PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []])
384
384
385− updateIMethod :: [(Name, PTerm)] ->
385+ updateIMethod :: [(Name, PTerm)] ->
386− (Name, (a, b, c, d, PTerm)) ->
386+ (Name, (a, b, c, d, PTerm)) ->
387 (Name, (a, b, c, d, PTerm))
387 (Name, (a, b, c, d, PTerm))
388 updateIMethod ns tm@(n, (isf, mfc, doc, o, ty))
388 updateIMethod ns tm@(n, (isf, mfc, doc, o, ty))
389 | Just ty' <- lookup (nsroot n) ns = (n, (isf, mfc, doc, o, ty'))
389 | 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
1168 _ -> False
1168 _ -> False
1169 tcName _ = False
1169 tcName _ = False
1170
1170
1171− isNotLift env n
1171+ isNotLift env n
1172 = case lookupBinder n env of
1172 = case lookupBinder n env of
1173− Just ty ->
1173+ Just ty ->
1174 case unApply (binderTy ty) of
1174 case unApply (binderTy ty) of
1175 (P _ n _, _) -> n `elem` noCaseLift info
1175 (P _ n _, _) -> n `elem` noCaseLift info
1176 _ -> False
1176 _ -> False