4c9b9ef · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

auto_implicit fix

4c9b9efEdwin Brady11 years ago

src/Idris/AbsSyntax.hs+15−16

compare with master

unifiedsplit

@@ -1536,18 +1536,15 @@ implicit' :: ElabInfo -> SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm

1536implicit' info syn ignore n ptm

1537 = do i <- getIState

1538 auto <- getAutoImpls

1539− if not auto

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

1540− then return ptm

1541− else do

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

1543− defaultArgCheck (eInfoNames info ++ M.keys (idris_implicits i)) impdata

1540+ defaultArgCheck (eInfoNames info ++ M.keys (idris_implicits i)) impdata

1544− -- let (tm'', spos) = findStatics i tm'

1541+-- let (tm'', spos) = findStatics i tm'

1545− putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }

1542+ putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }

1546− addIBC (IBCImp n)

1543+ addIBC (IBCImp n)

1547− logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)

1544+ logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)

1548− -- i <- get

1545+-- i <- get

1549− -- putIState $ i { idris_statics = addDef n spos (idris_statics i) }

1546+-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }

1550− return tm'

1547+ return tm'

1551 where

1548 where

1552 -- Detect unknown names in default arguments and throw error if found.

1549 -- Detect unknown names in default arguments and throw error if found.

1553 defaultArgCheck :: [Name] -> [PArg] -> Idris ()

1550 defaultArgCheck :: [Name] -> [PArg] -> Idris ()

@@ -1566,15 +1563,17 @@ implicit' info syn ignore n ptm

1566 notFound kns (SN (WhereN _ _ _) : ns) = notFound kns ns -- Known already

1563 notFound kns (SN (WhereN _ _ _) : ns) = notFound kns ns -- Known already

1567 notFound kns (n:ns) = if elem n kns then notFound kns ns else Just n

1564 notFound kns (n:ns) = if elem n kns then notFound kns ns else Just n

1568

1565

1566+-- Even if auto_implicits is off, we need to call this so we record which

1567+-- arguments are implicit

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

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

1570−implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

1569+implicitise auto syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

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

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

1572− ns = filter (\n -> implicitable n || elem n (map fst uvars)) $

1571+ ns = filter (\n -> auto && implicitable n || elem n (map fst uvars)) $

1573 ns' \\ (map fst pvars ++ no_imp syn ++ ignore)

1572 ns' \\ (map fst pvars ++ no_imp syn ++ ignore)

1574 nsOrder = filter (not . inUsing) ns ++ filter inUsing ns in

1573 nsOrder = filter (not . inUsing) ns ++ filter inUsing ns in

1575 if null ns

1574 if null ns

1576 then (tm, reverse declimps)

1575 then (tm, reverse declimps)

1577− else implicitise syn ignore ist (pibind uvars nsOrder tm)

1576+ else implicitise auto syn ignore ist (pibind uvars nsOrder tm)

1578 where

1577 where

1579 uvars = map ipair (filter uimplicit (using syn))

1578 uvars = map ipair (filter uimplicit (using syn))

1580 pvars = syn_params syn

1579 pvars = syn_params syn

src/Idris/Elab/Class.hs+1−1

@@ -84,7 +84,7 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

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

87− logElab 1 $ "Building methods " ++ show mnames

87+ logElab 2 $ "Building methods " ++ show mnames

88 ims <- mapM (tdecl mnames) mdecls

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

90 (filter clause ds)

src/Idris/Elab/Type.hs+1−1

@@ -64,7 +64,7 @@ buildType info syn fc opts n ty' = do

64 let ty = addImpl (imp_methods syn) i ty'

66 logElab 5 $ show n ++ " type pre-addimpl " ++ showTmImpls ty'

67− logElab 5 $ show "with methods " ++ show (imp_methods syn)

67+ logElab 5 $ "with methods " ++ show (imp_methods syn)

68 logElab 2 $ show n ++ " type " ++ show (using syn) ++ "\n" ++ showTmImpls ty

70 (ElabResult tyT' defer is ctxt' newDecls highlights newGName, log) <-