a7adbdb · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Fix cyclic universe checking bug

a7adbdbEdwin Brady14 years ago

src/Core/Constraints.hs+9−3

compare with master

unifiedsplit

@@ -11,6 +11,7 @@ import Data.List

11import Data.Maybe

12import qualified Data.Map as M

14+import Debug.Trace

15ucheck :: [(UConstraint, FC)] -> TC ()

16ucheck :: [(UConstraint, FC)] -> TC ()

16ucheck cs = acyclic rels (map fst (M.toList rels))

17ucheck cs = acyclic rels (map fst (M.toList rels))

@@ -23,11 +24,16 @@ type Relations = M.Map UExp [(UConstraint, FC)]

23mkRels :: [(UConstraint, FC)] -> Relations -> Relations

24mkRels :: [(UConstraint, FC)] -> Relations -> Relations

24mkRels [] acc = acc

25mkRels [] acc = acc

25mkRels ((c, f) : cs) acc

26mkRels ((c, f) : cs) acc

27+ | not (ignore c)

26− = case M.lookup (lhs c) acc of

28+ = case M.lookup (lhs c) acc of

27− Nothing -> mkRels cs (M.insert (lhs c) [(c,f)] acc)

29+ Nothing -> mkRels cs (M.insert (lhs c) [(c,f)] acc)

28− Just rs -> mkRels cs (M.insert (lhs c) ((c,f):rs) acc)

30+ Just rs -> mkRels cs (M.insert (lhs c) ((c,f):rs) acc)

31+ | otherwise = mkRels cs acc

29 where lhs (ULT l _) = l

32 where lhs (ULT l _) = l

30 lhs (ULE l _) = l

33 lhs (ULE l _) = l

34+ ignore (ULE l r) = l == r

35+ ignore _ = False

36+

32acyclic :: Relations -> [UExp] -> TC ()

38acyclic :: Relations -> [UExp] -> TC ()

33acyclic r cvs = checkCycle (FC "root" 0) r [] 0 cvs

39acyclic r cvs = checkCycle (FC "root" 0) r [] 0 cvs

src/Idris/AbsSyntax.hs+9−6

@@ -526,9 +526,12 @@ addStatics n tm ptm =

526-- This has become a right mess already. Better redo it some time...

527

528implicit :: 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

530 = do i <- get

533 = do i <- get

531− let (tm', impdata) = implicitise syn i ptm

534+ let (tm', impdata) = implicitise syn ignore i ptm

532-- let (tm'', spos) = findStatics i tm'

535-- let (tm'', spos) = findStatics i tm'

533 put (i { idris_implicits = addDef n impdata (idris_implicits i) })

536 put (i { idris_implicits = addDef n impdata (idris_implicits i) })

534 addIBC (IBCImp n)

537 addIBC (IBCImp n)

@@ -537,13 +540,13 @@ implicit syn n ptm

537-- put (i { idris_statics = addDef n spos (idris_statics i) })

540-- put (i { idris_statics = addDef n spos (idris_statics i) })

538 return tm'

541 return tm'

539

542

540−implicitise :: SyntaxInfo -> IState -> PTerm -> (PTerm, [PArg])

543+implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])

541−implicitise syn ist tm

544+implicitise syn ignore ist tm

542 = let (declimps, ns') = execState (imps True [] tm) ([], [])

545 = 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

544 if null ns

547 if null ns

545 then (tm, reverse declimps)

548 then (tm, reverse declimps)

546− else implicitise syn ist (pibind uvars ns tm)

549+ else implicitise syn ignore ist (pibind uvars ns tm)

547 where

550 where

548 uvars = using syn

551 uvars = using syn

549 pvars = syn_params syn

552 pvars = syn_params syn

src/Idris/ElabDecls.hs+16−8

@@ -554,15 +554,20 @@ elabClass info syn fc constraints tn ps ds

554 let constraint = PApp fc (PRef fc tn)

555 (map (pexp . PRef fc) (map fst ps))

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

558 defs <- mapM (defdecl (map (\ (x,y,z) -> z) ims) constraint)

561 defs <- mapM (defdecl (map (\ (x,y,z) -> z) ims) constraint)

559 (filter clause ds)

562 (filter clause ds)

560 let (methods, imethods) = unzip (map (\ (x,y,z) -> (x, y)) ims)

563 let (methods, imethods) = unzip (map (\ (x,y,z) -> (x, y)) ims)

561 let cty = impbind ps $ conbind constraints $ pibind methods constraint

564 let cty = impbind ps $ conbind constraints $ pibind methods constraint

562 let cons = [(cn, cty, fc)]

565 let cons = [(cn, cty, fc)]

563− let ddecl = PData syn fc (PDatadecl tn tty cons)

566+ let ddecl = PDatadecl tn tty cons

564− elabDecl info ddecl

567+ logLvl 5 $ "Class data " ++ showDImp True ddecl

568+ elabData info (syn { no_imp = no_imp syn ++ mnames }) fc ddecl

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

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

570+ logLvl 5 $ "Building functions"

566 let usyn = syn { using = ps ++ using syn }

571 let usyn = syn { using = ps ++ using syn }

567 fns <- mapM (cfun cn constraint usyn (map fst imethods)) constraints

572 fns <- mapM (cfun cn constraint usyn (map fst imethods)) constraints

568 mapM_ (elabDecl info) (concat fns)

573 mapM_ (elabDecl info) (concat fns)

@@ -583,11 +588,14 @@ elabClass info syn fc constraints tn ps ds

583 conbind (ty : ns) x = PPi constraint (MN 0 "c") ty (conbind ns x)

588 conbind (ty : ns) x = PPi constraint (MN 0 "c") ty (conbind ns x)

584 conbind [] x = x

589 conbind [] x = x

585

590

591+ getMName (PTy _ _ _ n _) = nsroot n

586− tdecl (PTy syn _ o n t) = do t' <- implicit syn n t

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'

587− return ( (n, (toExp (map fst ps) Exp t')),

595+ return ( (n, (toExp (map fst ps) Exp t')),

588− (n, (o, (toExp (map fst ps) Imp t'))),

596+ (n, (o, (toExp (map fst ps) Imp t'))),

589− (n, (syn, o, t) ) )

597+ (n, (syn, o, t) ) )

590− tdecl _ = fail "Not allowed in a class declaration"

598+ tdecl _ _ = fail "Not allowed in a class declaration"

591

599

592 -- Create default definitions

600 -- Create default definitions

593 defdecl mtys c d@(PClauses fc opts n cs) =

601 defdecl mtys c d@(PClauses fc opts n cs) =

src/Idris/Parser.hs+1

@@ -108,6 +108,7 @@ loadSource lidr f

108 iLOG ("Finished " ++ f)

109 ibcsd <- valIBCSubDir i

110 let ibc = ibcPathNoFallback ibcsd f

111+ iLOG "Universe checking"

111 iucheck

112 iucheck

112 i <- getIState

113 i <- getIState

113 addHides (hide_list i)

114 addHides (hide_list i)