44b38a6 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Fix implicits bug

44b38a6Edwin Brady12 years ago

src/Idris/AbsSyntax.hs+22−15

compare with master

unifiedsplit

@@ -1178,21 +1178,28 @@ addUsingImpls syn n fc t

1178-- status of each pi-bound argument, and whether it's inaccessible (True) or not.

1179

1180getUnboundImplicits :: IState -> Type -> PTerm -> [(Bool, PArg)]

1181−getUnboundImplicits i (Bind n (Pi t) sc) (PPi p n' t' sc')

1181+getUnboundImplicits i t tm = getImps t (collectImps tm)

1182− | n == n' = argInfo n p : getUnboundImplicits i sc sc'

1182+ where collectImps (PPi p n t sc)

1183+ = (n, (p, t)) : collectImps sc

1184+ collectImps _ = []

1185+

1186+ getImps (Bind n (Pi t) sc) imps

1187+ | Just (p, t') <- lookup n imps = argInfo n p t' : getImps sc imps

1183− where

1188+ where

1189+ argInfo n (Imp opt _ _) t'

1184− argInfo n (Imp opt _ _) = (True, PImp (getPriority i t') True opt n t')

1190+ = (True, PImp (getPriority i t') True opt n t')

1191+ argInfo n (Exp opt _ _) t'

1185− argInfo n (Exp opt _ _) = (InaccessibleArg `elem` opt,

1192+ = (InaccessibleArg `elem` opt,

1186− PExp (getPriority i t') opt n t')

1193+ PExp (getPriority i t') opt n t')

1194+ argInfo n (Constraint opt _) t'

1187− argInfo n (Constraint opt _) = (InaccessibleArg `elem` opt,

1195+ = (InaccessibleArg `elem` opt,

1188− PConstraint 10 opt n t')

1196+ PConstraint 10 opt n t')

1197+ argInfo n (TacImp opt _ scr) t'

1189− argInfo n (TacImp opt _ scr) = (InaccessibleArg `elem` opt,

1198+ = (InaccessibleArg `elem` opt,

1190− PTacImplicit 10 opt n scr t')

1199+ PTacImplicit 10 opt n scr t')

1191−getUnboundImplicits i (Bind n (Pi t) sc) tm

1200+ getImps (Bind n (Pi t) sc) imps = impBind n t : getImps sc imps

1192− = impBind n t : getUnboundImplicits i sc tm

1193− where

1194− impBind n t = (True, PImp 1 True [] n Placeholder)

1201+ where impBind n t = (True, PImp 1 True [] n Placeholder)

1195−getUnboundImplicits i sc tm = []

1202+ getImps sc tm = []

1196

1203

1197-- Add implicit Pi bindings for any names in the term which appear in an

1204-- Add implicit Pi bindings for any names in the term which appear in an

1198-- argument position.

1205-- argument position.

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

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

86 i <- getIState

87 let (inaccData, impls) = unzip $ getUnboundImplicits i cty ty

88 let inacc = inaccessibleImps 0 cty inaccData

89− logLvl 3 $ show n ++ ": inaccessible arguments: " ++ show inacc

89+ logLvl 3 $ show n ++ ": inaccessible arguments: " ++ show inacc ++

90+ " from " ++ show (cty, ty)

91 putIState $ i { idris_implicits = addDef n impls (idris_implicits i) }

92 putIState $ i { idris_implicits = addDef n impls (idris_implicits i) }

92 logLvl 3 ("Implicit " ++ show n ++ " " ++ show impls)

93 logLvl 3 ("Implicit " ++ show n ++ " " ++ show impls)