@@ -1550,103 +1550,109 @@ addImpl = addImpl' False [] []
1551addImpl' :: Bool -> [Name] -> [Name] -> [Name] -> IState -> PTerm -> PTerm
1551addImpl' :: Bool -> [Name] -> [Name] -> [Name] -> IState -> PTerm -> PTerm
1552addImpl' inpat env infns imp_meths ist ptm
1552addImpl' inpat env infns imp_meths ist ptm
1553− = mkUniqueNames env [] (ai False (zip env (repeat Nothing)) [] ptm)
1553+ = mkUniqueNames env [] (ai inpat False (zip env (repeat Nothing)) [] ptm)
1555+ topname = case ptm of
1557+ PApp _ (PRef _ _ n) _ -> n
1558+ _ -> sUN "" -- doesn't matter then
1555− ai :: Bool -> [(Name, Maybe PTerm)] -> [[T.Text]] -> PTerm -> PTerm
1560+ ai :: Bool -> Bool -> [(Name, Maybe PTerm)] -> [[T.Text]] -> PTerm -> PTerm
1556− ai qq env ds (PRef fc fcs f)
1561+ ai inpat qq env ds (PRef fc fcs f)
1557 | f `elem` infns = PInferRef fc fcs f
1562 | f `elem` infns = PInferRef fc fcs f
1558− | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat qq imp_meths ist fc f fc ds []
1563+ | not (f `elem` map fst env) = handleErr $ aiFn topname inpat inpat qq imp_meths ist fc f fc ds [] []
1559− ai qq env ds (PHidden (PRef fc hl f))
1564+ ai inpat qq env ds (PHidden (PRef fc hl f))
1560− | not (f `elem` map fst env) = PHidden (handleErr $ aiFn inpat False qq imp_meths ist fc f fc ds [])
1565+ | not (f `elem` map fst env) = PHidden (handleErr $ aiFn topname inpat False qq imp_meths ist fc f fc ds [] [])
1561− ai qq env ds (PRewrite fc l r g)
1566+ ai inpat qq env ds (PRewrite fc l r g)
1562− = let l' = ai qq env ds l
1567+ = let l' = ai inpat qq env ds l
1563− r' = ai qq env ds r
1568+ r' = ai inpat qq env ds r
1564− g' = fmap (ai qq env ds) g in
1569+ g' = fmap (ai inpat qq env ds) g in
1565 PRewrite fc l' r' g'
1570 PRewrite fc l' r' g'
1566− ai qq env ds (PTyped l r)
1571+ ai inpat qq env ds (PTyped l r)
1567− = let l' = ai qq env ds l
1572+ = let l' = ai inpat qq env ds l
1568− r' = ai qq env ds r in
1573+ r' = ai inpat qq env ds r in
1569 PTyped l' r'
1574 PTyped l' r'
1570− ai qq env ds (PPair fc hls p l r)
1575+ ai inpat qq env ds (PPair fc hls p l r)
1571− = let l' = ai qq env ds l
1576+ = let l' = ai inpat qq env ds l
1572− r' = ai qq env ds r in
1577+ r' = ai inpat qq env ds r in
1573 PPair fc hls p l' r'
1578 PPair fc hls p l' r'
1574− ai qq env ds (PDPair fc hls p l t r)
1579+ ai inpat qq env ds (PDPair fc hls p l t r)
1575− = let l' = ai qq env ds l
1580+ = let l' = ai inpat qq env ds l
1576− t' = ai qq env ds t
1581+ t' = ai inpat qq env ds t
1577− r' = ai qq env ds r in
1582+ r' = ai inpat qq env ds r in
1578 PDPair fc hls p l' t' r'
1583 PDPair fc hls p l' t' r'
1579− ai qq env ds (PAlternative ms a as)
1584+ ai inpat qq env ds (PAlternative ms a as)
1580− = let as' = map (ai qq env ds) as in
1585+ = let as' = map (ai inpat qq env ds) as in
1581 PAlternative ms a as'
1586 PAlternative ms a as'
1582− ai qq env _ (PDisamb ds' as) = ai qq env ds' as
1587+ ai inpat qq env _ (PDisamb ds' as) = ai inpat qq env ds' as
1583− ai qq env ds (PApp fc (PInferRef ffc hl f) as)
1588+ ai inpat qq env ds (PApp fc (PInferRef ffc hl f) as)
1584− = let as' = map (fmap (ai qq env ds)) as in
1589+ = let as' = map (fmap (ai inpat qq env ds)) as in
1585 PApp fc (PInferRef ffc hl f) as'
1590 PApp fc (PInferRef ffc hl f) as'
1586− ai qq env ds (PApp fc ftm@(PRef ffc hl f) as)
1591+ ai inpat qq env ds (PApp fc ftm@(PRef ffc hl f) as)
1587− | f `elem` infns = ai qq env ds (PApp fc (PInferRef ffc hl f) as)
1592+ | f `elem` infns = ai inpat qq env ds (PApp fc (PInferRef ffc hl f) as)
1588 | not (f `elem` map fst env)
1593 | not (f `elem` map fst env)
1589− = let as' = map (fmap (ai qq env ds)) as in
1594+ = let as' = map (fmap (ai inpat qq env ds)) as
1595+ asdotted' = map (fmap (ai False qq env ds)) as in
1590− handleErr $ aiFn inpat False qq imp_meths ist fc f ffc ds as'
1596+ handleErr $ aiFn topname inpat False qq imp_meths ist fc f ffc ds as' asdotted'
1591 | Just (Just ty) <- lookup f env =
1597 | Just (Just ty) <- lookup f env =
1592− let as' = map (fmap (ai qq env ds)) as
1598+ let as' = map (fmap (ai inpat qq env ds)) as
1593 arity = getPArity ty in
1599 arity = getPArity ty in
1594 mkPApp fc arity ftm as'
1600 mkPApp fc arity ftm as'
1595− ai qq env ds (PApp fc f as)
1601+ ai inpat qq env ds (PApp fc f as)
1596− = let f' = ai qq env ds f
1602+ = let f' = ai inpat qq env ds f
1597− as' = map (fmap (ai qq env ds)) as in
1603+ as' = map (fmap (ai inpat qq env ds)) as in
1598 mkPApp fc 1 f' as'
1604 mkPApp fc 1 f' as'
1599− ai qq env ds (PCase fc c os)
1605+ ai inpat qq env ds (PCase fc c os)
1600− = let c' = ai qq env ds c in
1606+ = let c' = ai inpat qq env ds c in
1601 -- leave os alone, because they get lifted into a new pattern match
1607 -- leave os alone, because they get lifted into a new pattern match
1602− -- definition which is passed through addImpl again with more scope
1608+ -- definition which is passed through addImpl agai inpatn with more scope
1603 -- information
1609 -- information
1604 PCase fc c' os
1610 PCase fc c' os
1606− ai qq env ds (PIfThenElse fc c t f) = PIfThenElse fc (ai qq env ds c)
1612+ ai inpat qq env ds (PIfThenElse fc c t f) = PIfThenElse fc (ai inpat qq env ds c)
1607− (ai qq env ds t)
1613+ (ai inpat qq env ds t)
1608− (ai qq env ds f)
1614+ (ai inpat qq env ds f)
1610 -- If the name in a lambda is a constructor name, do this as a 'case'
1616 -- If the name in a lambda is a constructor name, do this as a 'case'
1611 -- instead (it is harmless to do so, especially since the lambda will
1617 -- instead (it is harmless to do so, especially since the lambda will
1612 -- be lifted anyway!)
1618 -- be lifted anyway!)
1613− ai qq env ds (PLam fc n nfc ty sc)
1619+ ai inpat qq env ds (PLam fc n nfc ty sc)
1614 = case lookupDef n (tt_ctxt ist) of
1620 = case lookupDef n (tt_ctxt ist) of
1615− [] -> let ty' = ai qq env ds ty
1621+ [] -> let ty' = ai inpat qq env ds ty
1616− sc' = ai qq ((n, Just ty):env) ds sc in
1622+ sc' = ai inpat qq ((n, Just ty):env) ds sc in
1617 PLam fc n nfc ty' sc'
1623 PLam fc n nfc ty' sc'
1618− _ -> ai qq env ds (PLam fc (sMN 0 "lamp") NoFC ty
1624+ _ -> ai inpat qq env ds (PLam fc (sMN 0 "lamp") NoFC ty
1619 (PCase fc (PRef fc [] (sMN 0 "lamp") )
1625 (PCase fc (PRef fc [] (sMN 0 "lamp") )
1620 [(PRef fc [] n, sc)]))
1626 [(PRef fc [] n, sc)]))
1621− ai qq env ds (PLet fc n nfc ty val sc)
1627+ ai inpat qq env ds (PLet fc n nfc ty val sc)
1622 = case lookupDef n (tt_ctxt ist) of
1628 = case lookupDef n (tt_ctxt ist) of
1623− [] -> let ty' = ai qq env ds ty
1629+ [] -> let ty' = ai inpat qq env ds ty
1624− val' = ai qq env ds val
1630+ val' = ai inpat qq env ds val
1625− sc' = ai qq ((n, Just ty):env) ds sc in
1631+ sc' = ai inpat qq ((n, Just ty):env) ds sc in
1626 PLet fc n nfc ty' val' sc'
1632 PLet fc n nfc ty' val' sc'
1628− ai qq env ds (PCase fc val [(PRef fc [] n, sc)])
1634+ ai inpat qq env ds (PCase fc val [(PRef fc [] n, sc)])
1629− ai qq env ds (PPi p n nfc ty sc)
1635+ ai inpat qq env ds (PPi p n nfc ty sc)
1630− = let ty' = ai qq env ds ty
1636+ = let ty' = ai inpat qq env ds ty
1631 env' = if n `elem` imp_meths then env
1637 env' = if n `elem` imp_meths then env
1632 else ((n, Just ty) : env)
1638 else ((n, Just ty) : env)
1633− sc' = ai qq env' ds sc in
1639+ sc' = ai inpat qq env' ds sc in
1634 PPi p n nfc ty' sc'
1640 PPi p n nfc ty' sc'
1635− ai qq env ds (PGoal fc r n sc)
1641+ ai inpat qq env ds (PGoal fc r n sc)
1636− = let r' = ai qq env ds r
1642+ = let r' = ai inpat qq env ds r
1637− sc' = ai qq ((n, Nothing):env) ds sc in
1643+ sc' = ai inpat qq ((n, Nothing):env) ds sc in
1638 PGoal fc r' n sc'
1644 PGoal fc r' n sc'
1639− ai qq env ds (PHidden tm) = PHidden (ai qq env ds tm)
1645+ ai inpat qq env ds (PHidden tm) = PHidden (ai inpat qq env ds tm)
1640 -- Don't do PProof or PTactics since implicits get added when scope is
1646 -- Don't do PProof or PTactics since implicits get added when scope is
1641 -- properly known in ElabTerm.runTac
1647 -- properly known in ElabTerm.runTac
1642− ai qq env ds (PUnifyLog tm) = PUnifyLog (ai qq env ds tm)
1648+ ai inpat qq env ds (PUnifyLog tm) = PUnifyLog (ai inpat qq env ds tm)
1643− ai qq env ds (PNoImplicits tm) = PNoImplicits (ai qq env ds tm)
1649+ ai inpat qq env ds (PNoImplicits tm) = PNoImplicits (ai inpat qq env ds tm)
1644− ai qq env ds (PQuasiquote tm g) = PQuasiquote (ai True env ds tm)
1650+ ai inpat qq env ds (PQuasiquote tm g) = PQuasiquote (ai inpat True env ds tm)
1645− (fmap (ai True env ds) g)
1651+ (fmap (ai inpat True env ds) g)
1646− ai qq env ds (PUnquote tm) = PUnquote (ai False env ds tm)
1652+ ai inpat qq env ds (PUnquote tm) = PUnquote (ai inpat False env ds tm)
1647− ai qq env ds (PRunElab fc tm ns) = PRunElab fc (ai False env ds tm) ns
1653+ ai inpat qq env ds (PRunElab fc tm ns) = PRunElab fc (ai inpat False env ds tm) ns
1648− ai qq env ds (PConstSugar fc tm) = PConstSugar fc (ai qq env ds tm)
1654+ ai inpat qq env ds (PConstSugar fc tm) = PConstSugar fc (ai inpat qq env ds tm)
1649− ai qq env ds tm = tm
1655+ ai inpat qq env ds tm = tm
1651 handleErr (Left err) = PElabError err
1657 handleErr (Left err) = PElabError err
1652 handleErr (Right x) = x
1658 handleErr (Right x) = x
@@ -1654,14 +1660,15 @@ addImpl' inpat env infns imp_meths ist ptm
1654-- if in a pattern, and there are no arguments, and there's no possible
1660-- if in a pattern, and there are no arguments, and there's no possible
1655-- names with zero explicit arguments, don't add implicits.
1661-- names with zero explicit arguments, don't add implicits.
1657−aiFn :: Bool -> Bool -> Bool
1663+aiFn :: Name -> Bool -> Bool -> Bool
1658 -> [Name]
1664 -> [Name]
1659 -> IState -> FC
1665 -> IState -> FC
1660 -> Name -- ^ function being applied
1666 -> Name -- ^ function being applied
1661 -> FC -> [[T.Text]]
1667 -> FC -> [[T.Text]]
1662− -> [PArg] -- ^ initial arguments
1668+ -> [PArg] -- ^ initial arguments (if in a pattern)
1669+ -> [PArg] -- ^ initial arguments (if in an expression)
1663 -> Either Err PTerm
1670 -> Either Err PTerm
1664−aiFn inpat True qq imp_meths ist fc f ffc ds []
1671+aiFn topname inpat True qq imp_meths ist fc f ffc ds [] _
1665 = case lookupDef f (tt_ctxt ist) of
1672 = case lookupDef f (tt_ctxt ist) of
1666 [] -> Right $ PPatvar ffc f
1673 [] -> Right $ PPatvar ffc f
1667 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
1674 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
@@ -1669,7 +1676,7 @@ aiFn inpat True qq imp_meths ist fc f ffc ds []
1669 if (not (vname f) || tcname f
1676 if (not (vname f) || tcname f
1670 || any (conCaf (tt_ctxt ist)) ialts)
1677 || any (conCaf (tt_ctxt ist)) ialts)
1671-- any constructor alts || any allImp ialts))
1678-- any constructor alts || any allImp ialts))
1672− then aiFn inpat False qq imp_meths ist fc f ffc ds [] -- use it as a constructor
1679+ then aiFn topname inpat False qq imp_meths ist fc f ffc ds [] [] -- use it as a constructor
1673 else Right $ PPatvar ffc f
1680 else Right $ PPatvar ffc f
1674 where imp (PExp _ _ _ _) = False
1681 where imp (PExp _ _ _ _) = False
1675 imp _ = True
1682 imp _ = True
@@ -1683,9 +1690,9 @@ aiFn inpat True qq imp_meths ist fc f ffc ds []
1683 vname (UN n) = True -- non qualified
1690 vname (UN n) = True -- non qualified
1684 vname _ = False
1691 vname _ = False
1686−aiFn inpat expat qq imp_meths ist fc f ffc ds as
1693+aiFn topname inpat expat qq imp_meths ist fc f ffc ds as asexp
1687 | f `elem` primNames = Right $ PApp fc (PRef ffc [ffc] f) as
1694 | f `elem` primNames = Right $ PApp fc (PRef ffc [ffc] f) as
1688−aiFn inpat expat qq imp_meths ist fc f ffc ds as
1695+aiFn topname inpat expat qq imp_meths ist fc f ffc ds as asexp
1689 -- This is where namespaces get resolved by adding PAlternative
1696 -- This is where namespaces get resolved by adding PAlternative
1690 = do let ns = lookupCtxtName f (idris_implicits ist)
1697 = do let ns = lookupCtxtName f (idris_implicits ist)
1691 let nh = filter (\(n, _) -> notHidden n) ns
1698 let nh = filter (\(n, _) -> notHidden n) ns
@@ -1693,15 +1700,25 @@ aiFn inpat expat qq imp_meths ist fc f ffc ds as
1693 [] -> nh
1700 [] -> nh
1695 case ns' of
1702 case ns' of
1696− [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef ffc [ffc] (isImpName f f')) (insertImpl ns as)
1703+ [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef ffc [ffc] (isImpName f f'))
1704+ (insertImpl ns (chooseArgs f' as asexp))
1697 [] -> if f `elem` (map fst (idris_metavars ist))
1705 [] -> if f `elem` (map fst (idris_metavars ist))
1698 then Right $ PApp fc (PRef ffc [ffc] f) as
1706 then Right $ PApp fc (PRef ffc [ffc] f) as
1699 else Right $ mkPApp fc (length as) (PRef ffc [ffc] f) as
1707 else Right $ mkPApp fc (length as) (PRef ffc [ffc] f) as
1700 alts -> Right $
1708 alts -> Right $
1701 PAlternative [] (ExactlyOne True) $
1709 PAlternative [] (ExactlyOne True) $
1702 map (\(f', ns) -> mkPApp fc (length ns) (PRef ffc [ffc] (isImpName f f'))
1710 map (\(f', ns) -> mkPApp fc (length ns) (PRef ffc [ffc] (isImpName f f'))
1703− (insertImpl ns as)) alts
1711+ (insertImpl ns (chooseArgs f' as asexp))) alts
1713+ -- choose whether to treat the arguments as patterns or expressions
1714+ -- if 'f' is a defined function, treat as expression, otherwise do the default.
1715+ -- This is so any names which later go under a PHidden are treated
1716+ -- as function names rather than bound pattern variables
1717+ chooseArgs f as asexp | isConName f (tt_ctxt ist) = as
1718+ | f == topname = as
1719+ | Nothing <- lookupDefExact f (tt_ctxt ist) = as
1720+ | otherwise = asexp
1705 -- if the name is in imp_meths, we should actually refer to the bound
1722 -- if the name is in imp_meths, we should actually refer to the bound
1706 -- name rather than the global one after expanding implicits
1723 -- name rather than the global one after expanding implicits
1707 isImpName f f' | f `elem` imp_meths = f
1724 isImpName f f' | f `elem` imp_meths = f