3a4a26b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Better dealing with names in patterns

3a4a26bEdwin Brady15 years ago

src/Idris/AbsSyntax.hs+30−6

compare with master

unifiedsplit

@@ -1118,12 +1118,25 @@ implicitise syn ist tm

1118 Nothing -> PPi (Imp False Dynamic) n Placeholder (pibind using ns sc)

1119

1120-- Add implicit arguments in function calls

1121+addImplPat :: IState -> PTerm -> PTerm

1122+addImplPat = addImpl' True []

1123+

1124+addImplBound :: IState -> [Name] -> PTerm -> PTerm

1125+addImplBound ist ns = addImpl' False ns ist

1121

1126

1122addImpl :: IState -> PTerm -> PTerm

1127addImpl :: IState -> PTerm -> PTerm

1128+addImpl = addImpl' False []

1129+

1130+-- TODO: in patterns, don't add implicits to function names guarded by constructors

1131+-- and *not* inside a PHidden

1132+

1133+addImpl' :: Bool -> [Name] -> IState -> PTerm -> PTerm

1123−addImpl ist ptm = ai [] ptm

1134+addImpl' inpat env ist ptm = ai env ptm

1124 where

1135 where

1125 ai env (PRef fc f)

1136 ai env (PRef fc f)

1126− | not (f `elem` env) = aiFn ist fc f []

1137+ | not (f `elem` env) = aiFn inpat ist fc f []

1138+ ai env (PHidden (PRef fc f))

1139+ | not (f `elem` env) = aiFn False ist fc f []

1127 ai env (PEq fc l r) = let l' = ai env l

1140 ai env (PEq fc l r) = let l' = ai env l

1128 r' = ai env r in

1141 r' = ai env r in

1129 PEq fc l' r'

1142 PEq fc l' r'

@@ -1142,7 +1155,7 @@ addImpl ist ptm = ai [] ptm

1142 ai env (PApp fc (PRef _ f) as)

1155 ai env (PApp fc (PRef _ f) as)

1143 | not (f `elem` env)

1156 | not (f `elem` env)

1144 = let as' = map (fmap (ai env)) as in

1157 = let as' = map (fmap (ai env)) as in

1145− aiFn ist fc f as'

1158+ aiFn False ist fc f as'

1146 ai env (PApp fc f as) = let f' = ai env f

1159 ai env (PApp fc f as) = let f' = ai env f

1147 as' = map (fmap (ai env)) as in

1160 as' = map (fmap (ai env)) as in

1148 mkPApp fc 1 f' as'

1161 mkPApp fc 1 f' as'

@@ -1165,10 +1178,21 @@ addImpl ist ptm = ai [] ptm

1165 ai env (PTactics ts) = PTactics (map (fmap (ai env)) ts)

1178 ai env (PTactics ts) = PTactics (map (fmap (ai env)) ts)

1166 ai env tm = tm

1179 ai env tm = tm

1167

1180

1181+-- if in a pattern, and there are no arguments, and there's no possible

1182+-- names with zero explicit arguments, don't add implicits.

1183+

1168−aiFn :: IState -> FC -> Name -> [PArg] -> PTerm

1184+aiFn :: Bool -> IState -> FC -> Name -> [PArg] -> PTerm

1185+aiFn True ist fc f []

1186+ = case lookupCtxt Nothing f (idris_implicits ist) of

1187+ [] -> PRef fc f

1188+ alts -> if (any (all imp) alts)

1189+ then aiFn False ist fc f [] -- use it as a constructor

1190+ else PRef fc f

1191+ where imp (PExp _ _ _) = False

1192+ imp _ = True

1169−aiFn ist fc f as

1193+aiFn inpat ist fc f as

1170 | f `elem` primNames = PApp fc (PRef fc f) as

1194 | f `elem` primNames = PApp fc (PRef fc f) as

1171−aiFn ist fc f as

1195+aiFn inpat ist fc f as

1172 -- This is where namespaces get resolved by adding PAlternative

1196 -- This is where namespaces get resolved by adding PAlternative

1173 = case lookupCtxtName Nothing f (idris_implicits ist) of

1197 = case lookupCtxtName Nothing f (idris_implicits ist) of

1174 [(f',ns)] -> mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)

1198 [(f',ns)] -> mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)

src/Idris/ElabDecls.hs+3−3

@@ -284,7 +284,7 @@ elabClause info fc tcgen (PClause fname lhs_in withs rhs_in whereblock)

284 -- Build the LHS as an "Infer", and pull out its type and

285 -- pattern bindings

286 i <- get

287− let lhs = addImpl i lhs_in

287+ let lhs = addImplPat i lhs_in

288 logLvl 5 ("LHS: " ++ showImp True lhs)

289 ((lhs', dlhs, []), _) <-

290 tclift $ elaborate ctxt (MN 0 "patLHS") infP []

@@ -306,8 +306,8 @@ elabClause info fc tcgen (PClause fname lhs_in withs rhs_in whereblock)

306 -- Now build the RHS, using the type of the LHS as the goal.

307 i <- get -- new implicits from where block

308 logLvl 5 (showImp True (expandParams decorate newargs decls rhs_in))

309+ let rhs = addImplBound i (map fst newargs)

309− let rhs = addImpl i (expandParams decorate newargs decls rhs_in)

310+ (expandParams decorate newargs decls rhs_in)

310− -- TODO: but don't do names in scope

311 logLvl 2 (showImp True rhs)

312 ctxt <- getContext -- new context with where block added

313 ((rhs', defer, is), _) <-