e6bec02 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Fix parameter propagation on CAFs

e6bec02Edwin Brady12 years ago

src/Idris/ElabDecls.hs+13−7

compare with master

unifiedsplit

@@ -1472,8 +1472,8 @@ paramNames args env (p : ps)

1472 _ -> paramNames args env ps

1473 | otherwise = paramNames args env ps

1474

1475−propagateParams :: [Name] -> Type -> PTerm -> PTerm

1475+propagateParams :: IState -> [Name] -> Type -> PTerm -> PTerm

1476−propagateParams ps t tm@(PApp _ (PRef fc n) args)

1476+propagateParams i ps t tm@(PApp _ (PRef fc n) args)

1477 = PApp fc (PRef fc n) (addP t args)

1478 where addP (Bind n _ sc) (t : ts)

1479 | Placeholder <- getTm t,

@@ -1482,9 +1482,15 @@ propagateParams ps t tm@(PApp _ (PRef fc n) args)

1482 = t { getTm = PRef fc n } : addP sc ts

1483 addP (Bind n _ sc) (t : ts) = t : addP sc ts

1484 addP _ ts = ts

1485−propagateParams ps t (PRef fc n)

1485+propagateParams i ps t (PRef fc n)

1486+ = case lookupCtxt n (idris_implicits i) of

1487+ [is] -> let ps' = filter (isImplicit is) ps in

1486− = PApp fc (PRef fc n) (map (\x -> pimp x (PRef fc x) True) ps)

1488+ PApp fc (PRef fc n) (map (\x -> pimp x (PRef fc x) True) ps')

1489+ _ -> PRef fc n

1490+ where isImplicit [] n = False

1491+ isImplicit (PImp _ _ _ x _ : is) n | x == n = True

1492+ isImplicit (_ : is) n = isImplicit is n

1487−propagateParams ps t x = x

1493+propagateParams i ps t x = x

1488

1494

1489-- Return the elaborated LHS/RHS, and the original LHS with implicits added

1495-- Return the elaborated LHS/RHS, and the original LHS with implicits added

1490elabClause :: ElabInfo -> FnOpts -> (Int, PClause) ->

1496elabClause :: ElabInfo -> FnOpts -> (Int, PClause) ->

@@ -1516,7 +1522,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1516 _ -> []

1522 _ -> []

1517 let params = getParamsInType i [] fn_is fn_ty

1523 let params = getParamsInType i [] fn_is fn_ty

1518 let lhs = mkLHSapp $ stripUnmatchable i $

1524 let lhs = mkLHSapp $ stripUnmatchable i $

1519− propagateParams params fn_ty (addImplPat i (stripLinear i lhs_in))

1525+ propagateParams i params fn_ty (addImplPat i (stripLinear i lhs_in))

1520 logLvl 5 ("LHS: " ++ show fc ++ " " ++ showTmImpls lhs)

1526 logLvl 5 ("LHS: " ++ show fc ++ " " ++ showTmImpls lhs)

1521 logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show lhs_in ++

1527 logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show lhs_in ++

1522 "\n" ++ show (fn_ty, fn_is))

1528 "\n" ++ show (fn_ty, fn_is))

@@ -1711,7 +1717,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

1711 [t] -> t

1717 [t] -> t

1712 _ -> []

1718 _ -> []

1713 let params = getParamsInType i [] fn_is fn_ty

1719 let params = getParamsInType i [] fn_is fn_ty

1714− let lhs = propagateParams params fn_ty (addImplPat i (stripLinear i lhs_in))

1720+ let lhs = propagateParams i params fn_ty (addImplPat i (stripLinear i lhs_in))

1715 logLvl 2 ("LHS: " ++ show lhs)

1721 logLvl 2 ("LHS: " ++ show lhs)

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

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

1717 tclift $ elaborate ctxt (sMN 0 "patLHS") infP []

1723 tclift $ elaborate ctxt (sMN 0 "patLHS") infP []