git.iko.soy/Idris-dev
on master help sign in
Fix cyclic universe checking bug
commita7adbdbdca8b6aea36c8f092ea4089ba368e440e authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 6 Oct 2012, 15:52 (14 years ago) parent783d45f
4 files changed+35−17
compare with master
unifiedsplit
src/Core/Constraints.hs+9−3 src/Idris/AbsSyntax.hs+9−6 src/Idris/ElabDecls.hs+16−8 src/Idris/Parser.hs+1
src/Core/Constraints.hs+9−3
@@ -11,6 +11,7 @@ import Data.List
1111import Data.Maybe
1212import qualified Data.Map as M
1313
14+import Debug.Trace
1415
1516ucheck :: [(UConstraint, FC)] -> TC ()
1617ucheck cs = acyclic rels (map fst (M.toList rels))
@@ -23,11 +24,16 @@ type Relations = M.Map UExp [(UConstraint, FC)]
2324mkRels :: [(UConstraint, FC)] -> Relations -> Relations
2425mkRels [] acc = acc
2526mkRels ((c, f) : cs) acc
26− = case M.lookup (lhs c) acc of
27− Nothing -> mkRels cs (M.insert (lhs c) [(c,f)] acc)
28− Just rs -> mkRels cs (M.insert (lhs c) ((c,f):rs) acc)
27+ | not (ignore c)
28+ = case M.lookup (lhs c) acc of
29+ Nothing -> mkRels cs (M.insert (lhs c) [(c,f)] acc)
30+ Just rs -> mkRels cs (M.insert (lhs c) ((c,f):rs) acc)
31+ | otherwise = mkRels cs acc
2932 where lhs (ULT l _) = l
3033 lhs (ULE l _) = l
34+ ignore (ULE l r) = l == r
35+ ignore _ = False
36+
3137
3238acyclic :: Relations -> [UExp] -> TC ()
3339acyclic r cvs = checkCycle (FC "root" 0) r [] 0 cvs
src/Idris/AbsSyntax.hs+9−6
@@ -526,9 +526,12 @@ addStatics n tm ptm =
526526-- This has become a right mess already. Better redo it some time...
527527
528528implicit :: SyntaxInfo -> Name -> PTerm -> Idris PTerm
529−implicit syn n ptm
529+implicit syn n ptm = implicit' syn [] n ptm
530+
531+implicit' :: SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
532+implicit' syn ignore n ptm
530533 = do i <- get
531− let (tm', impdata) = implicitise syn i ptm
534+ let (tm', impdata) = implicitise syn ignore i ptm
532535-- let (tm'', spos) = findStatics i tm'
533536 put (i { idris_implicits = addDef n impdata (idris_implicits i) })
534537 addIBC (IBCImp n)
@@ -537,13 +540,13 @@ implicit syn n ptm
537540-- put (i { idris_statics = addDef n spos (idris_statics i) })
538541 return tm'
539542
540−implicitise :: SyntaxInfo -> IState -> PTerm -> (PTerm, [PArg])
541−implicitise syn ist tm
543+implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
544+implicitise syn ignore ist tm
542545 = let (declimps, ns') = execState (imps True [] tm) ([], [])
543− ns = ns' \\ (map fst pvars ++ no_imp syn) in
546+ ns = ns' \\ (map fst pvars ++ no_imp syn ++ ignore) in
544547 if null ns
545548 then (tm, reverse declimps)
546− else implicitise syn ist (pibind uvars ns tm)
549+ else implicitise syn ignore ist (pibind uvars ns tm)
547550 where
548551 uvars = using syn
549552 pvars = syn_params syn
src/Idris/ElabDecls.hs+16−8
@@ -554,15 +554,20 @@ elabClass info syn fc constraints tn ps ds
554554 let constraint = PApp fc (PRef fc tn)
555555 (map (pexp . PRef fc) (map fst ps))
556556 -- build data declaration
557− ims <- mapM tdecl (filter tydecl ds)
557+ let mdecls = filter tydecl ds -- method declarations
558+ let mnames = map getMName mdecls
559+ logLvl 2 $ "Building methods " ++ show mnames
560+ ims <- mapM (tdecl mnames) mdecls
558561 defs <- mapM (defdecl (map (\ (x,y,z) -> z) ims) constraint)
559562 (filter clause ds)
560563 let (methods, imethods) = unzip (map (\ (x,y,z) -> (x, y)) ims)
561564 let cty = impbind ps $ conbind constraints $ pibind methods constraint
562565 let cons = [(cn, cty, fc)]
563− let ddecl = PData syn fc (PDatadecl tn tty cons)
564− elabDecl info ddecl
566+ let ddecl = PDatadecl tn tty cons
567+ logLvl 5 $ "Class data " ++ showDImp True ddecl
568+ elabData info (syn { no_imp = no_imp syn ++ mnames }) fc ddecl
565569 -- for each constraint, build a top level function to chase it
570+ logLvl 5 $ "Building functions"
566571 let usyn = syn { using = ps ++ using syn }
567572 fns <- mapM (cfun cn constraint usyn (map fst imethods)) constraints
568573 mapM_ (elabDecl info) (concat fns)
@@ -583,11 +588,14 @@ elabClass info syn fc constraints tn ps ds
583588 conbind (ty : ns) x = PPi constraint (MN 0 "c") ty (conbind ns x)
584589 conbind [] x = x
585590
586− tdecl (PTy syn _ o n t) = do t' <- implicit syn n t
587− return ( (n, (toExp (map fst ps) Exp t')),
588− (n, (o, (toExp (map fst ps) Imp t'))),
589− (n, (syn, o, t) ) )
590− tdecl _ = fail "Not allowed in a class declaration"
591+ getMName (PTy _ _ _ n _) = nsroot n
592+ tdecl allmeths (PTy syn _ o n t)
593+ = do t' <- implicit' syn allmeths n t
594+ logLvl 5 $ "Method " ++ show n ++ " : " ++ showImp True t'
595+ return ( (n, (toExp (map fst ps) Exp t')),
596+ (n, (o, (toExp (map fst ps) Imp t'))),
597+ (n, (syn, o, t) ) )
598+ tdecl _ _ = fail "Not allowed in a class declaration"
591599
592600 -- Create default definitions
593601 defdecl mtys c d@(PClauses fc opts n cs) =
src/Idris/Parser.hs+1
@@ -108,6 +108,7 @@ loadSource lidr f
108108 iLOG ("Finished " ++ f)
109109 ibcsd <- valIBCSubDir i
110110 let ibc = ibcPathNoFallback ibcsd f
111+ iLOG "Universe checking"
111112 iucheck
112113 i <- getIState
113114 addHides (hide_list i)