b573bf0 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Improve addImpl under PHidden

Under a PHidden we can't encounter new pattern variables, so make addImpl aware of this. As a result, there's no longer any need to qualify constant function names under a function application on the lhs.

commitb573bf0e63e56c7588d5ba74cb40bcac818c5927 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 1 Sep 2015, 20:26 (11 years ago) parent908f2f2

2 files changed+92−73

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+88−71 src/Idris/Core/ProofState.hs+4−2

src/Idris/AbsSyntax.hs+88−71

@@ -1550,103 +1550,109 @@ addImpl = addImpl' False [] []

15501550

15511551addImpl' :: Bool -> [Name] -> [Name] -> [Name] -> IState -> PTerm -> PTerm

15521552addImpl' 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)

15541554 where

1555− ai :: Bool -> [(Name, Maybe PTerm)] -> [[T.Text]] -> PTerm -> PTerm

1556− ai qq env ds (PRef fc fcs f)

1555+ topname = case ptm of

1556+ PRef _ _ n -> n

1557+ PApp _ (PRef _ _ n) _ -> n

1558+ _ -> sUN "" -- doesn't matter then

1559+

1560+ ai :: Bool -> Bool -> [(Name, Maybe PTerm)] -> [[T.Text]] -> PTerm -> PTerm

1561+ ai inpat qq env ds (PRef fc fcs f)

15571562 | 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 []

1559− ai 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 [])

1561− ai qq env ds (PRewrite fc l r g)

1562− = let l' = ai qq env ds l

1563− r' = ai qq env ds r

1564− g' = fmap (ai qq env ds) g in

1563+ | not (f `elem` map fst env) = handleErr $ aiFn topname inpat inpat qq imp_meths ist fc f fc ds [] []

1564+ ai inpat qq env ds (PHidden (PRef fc hl f))

1565+ | not (f `elem` map fst env) = PHidden (handleErr $ aiFn topname inpat False qq imp_meths ist fc f fc ds [] [])

1566+ ai inpat qq env ds (PRewrite fc l r g)

1567+ = let l' = ai inpat qq env ds l

1568+ r' = ai inpat qq env ds r

1569+ g' = fmap (ai inpat qq env ds) g in

15651570 PRewrite fc l' r' g'

1566− ai qq env ds (PTyped l r)

1567− = let l' = ai qq env ds l

1568− r' = ai qq env ds r in

1571+ ai inpat qq env ds (PTyped l r)

1572+ = let l' = ai inpat qq env ds l

1573+ r' = ai inpat qq env ds r in

15691574 PTyped l' r'

1570− ai qq env ds (PPair fc hls p l r)

1571− = let l' = ai qq env ds l

1572− r' = ai qq env ds r in

1575+ ai inpat qq env ds (PPair fc hls p l r)

1576+ = let l' = ai inpat qq env ds l

1577+ r' = ai inpat qq env ds r in

15731578 PPair fc hls p l' r'

1574− ai qq env ds (PDPair fc hls p l t r)

1575− = let l' = ai qq env ds l

1576− t' = ai qq env ds t

1577− r' = ai qq env ds r in

1579+ ai inpat qq env ds (PDPair fc hls p l t r)

1580+ = let l' = ai inpat qq env ds l

1581+ t' = ai inpat qq env ds t

1582+ r' = ai inpat qq env ds r in

15781583 PDPair fc hls p l' t' r'

1579− ai qq env ds (PAlternative ms a as)

1580− = let as' = map (ai qq env ds) as in

1584+ ai inpat qq env ds (PAlternative ms a as)

1585+ = let as' = map (ai inpat qq env ds) as in

15811586 PAlternative ms a as'

1582− ai qq env _ (PDisamb ds' as) = ai qq env ds' as

1583− ai qq env ds (PApp fc (PInferRef ffc hl f) as)

1584− = let as' = map (fmap (ai qq env ds)) as in

1587+ ai inpat qq env _ (PDisamb ds' as) = ai inpat qq env ds' as

1588+ ai inpat qq env ds (PApp fc (PInferRef ffc hl f) as)

1589+ = let as' = map (fmap (ai inpat qq env ds)) as in

15851590 PApp fc (PInferRef ffc hl f) as'

1586− ai 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)

1591+ ai inpat qq env ds (PApp fc ftm@(PRef ffc hl f) as)

1592+ | f `elem` infns = ai inpat qq env ds (PApp fc (PInferRef ffc hl f) as)

15881593 | not (f `elem` map fst env)

1589− = let as' = map (fmap (ai qq env ds)) as in

1590− handleErr $ aiFn inpat False qq imp_meths ist fc f ffc ds as'

1594+ = let as' = map (fmap (ai inpat qq env ds)) as

1595+ asdotted' = map (fmap (ai False qq env ds)) as in

1596+ handleErr $ aiFn topname inpat False qq imp_meths ist fc f ffc ds as' asdotted'

15911597 | 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

15931599 arity = getPArity ty in

15941600 mkPApp fc arity ftm as'

1595− ai qq env ds (PApp fc f as)

1596− = let f' = ai qq env ds f

1597− as' = map (fmap (ai qq env ds)) as in

1601+ ai inpat qq env ds (PApp fc f as)

1602+ = let f' = ai inpat qq env ds f

1603+ as' = map (fmap (ai inpat qq env ds)) as in

15981604 mkPApp fc 1 f' as'

1599− ai qq env ds (PCase fc c os)

1600− = let c' = ai qq env ds c in

1605+ ai inpat qq env ds (PCase fc c os)

1606+ = let c' = ai inpat qq env ds c in

16011607 -- 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

16031609 -- information

16041610 PCase fc c' os

16051611

1606− ai qq env ds (PIfThenElse fc c t f) = PIfThenElse fc (ai qq env ds c)

1607− (ai qq env ds t)

1608− (ai qq env ds f)

1612+ ai inpat qq env ds (PIfThenElse fc c t f) = PIfThenElse fc (ai inpat qq env ds c)

1613+ (ai inpat qq env ds t)

1614+ (ai inpat qq env ds f)

16091615

16101616 -- If the name in a lambda is a constructor name, do this as a 'case'

16111617 -- instead (it is harmless to do so, especially since the lambda will

16121618 -- 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)

16141620 = case lookupDef n (tt_ctxt ist) of

1615− [] -> let ty' = ai qq env ds ty

1616− sc' = ai qq ((n, Just ty):env) ds sc in

1621+ [] -> let ty' = ai inpat qq env ds ty

1622+ sc' = ai inpat qq ((n, Just ty):env) ds sc in

16171623 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

16191625 (PCase fc (PRef fc [] (sMN 0 "lamp") )

16201626 [(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)

16221628 = case lookupDef n (tt_ctxt ist) of

1623− [] -> let ty' = ai qq env ds ty

1624− val' = ai qq env ds val

1625− sc' = ai qq ((n, Just ty):env) ds sc in

1629+ [] -> let ty' = ai inpat qq env ds ty

1630+ val' = ai inpat qq env ds val

1631+ sc' = ai inpat qq ((n, Just ty):env) ds sc in

16261632 PLet fc n nfc ty' val' sc'

16271633 defs ->

1628− ai qq env ds (PCase fc val [(PRef fc [] n, sc)])

1629− ai qq env ds (PPi p n nfc ty sc)

1630− = let ty' = ai qq env ds ty

1634+ ai inpat qq env ds (PCase fc val [(PRef fc [] n, sc)])

1635+ ai inpat qq env ds (PPi p n nfc ty sc)

1636+ = let ty' = ai inpat qq env ds ty

16311637 env' = if n `elem` imp_meths then env

16321638 else ((n, Just ty) : env)

1633− sc' = ai qq env' ds sc in

1639+ sc' = ai inpat qq env' ds sc in

16341640 PPi p n nfc ty' sc'

1635− ai qq env ds (PGoal fc r n sc)

1636− = let r' = ai qq env ds r

1637− sc' = ai qq ((n, Nothing):env) ds sc in

1641+ ai inpat qq env ds (PGoal fc r n sc)

1642+ = let r' = ai inpat qq env ds r

1643+ sc' = ai inpat qq ((n, Nothing):env) ds sc in

16381644 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)

16401646 -- Don't do PProof or PTactics since implicits get added when scope is

16411647 -- properly known in ElabTerm.runTac

1642− ai qq env ds (PUnifyLog tm) = PUnifyLog (ai qq env ds tm)

1643− ai qq env ds (PNoImplicits tm) = PNoImplicits (ai qq env ds tm)

1644− ai qq env ds (PQuasiquote tm g) = PQuasiquote (ai True env ds tm)

1645− (fmap (ai True env ds) g)

1646− ai qq env ds (PUnquote tm) = PUnquote (ai False env ds tm)

1647− ai qq env ds (PRunElab fc tm ns) = PRunElab fc (ai False env ds tm) ns

1648− ai qq env ds (PConstSugar fc tm) = PConstSugar fc (ai qq env ds tm)

1649− ai qq env ds tm = tm

1648+ ai inpat qq env ds (PUnifyLog tm) = PUnifyLog (ai inpat qq env ds tm)

1649+ ai inpat qq env ds (PNoImplicits tm) = PNoImplicits (ai inpat qq env ds tm)

1650+ ai inpat qq env ds (PQuasiquote tm g) = PQuasiquote (ai inpat True env ds tm)

1651+ (fmap (ai inpat True env ds) g)

1652+ ai inpat qq env ds (PUnquote tm) = PUnquote (ai inpat False env ds tm)

1653+ ai inpat qq env ds (PRunElab fc tm ns) = PRunElab fc (ai inpat False env ds tm) ns

1654+ ai inpat qq env ds (PConstSugar fc tm) = PConstSugar fc (ai inpat qq env ds tm)

1655+ ai inpat qq env ds tm = tm

16501656

16511657 handleErr (Left err) = PElabError err

16521658 handleErr (Right x) = x

@@ -1654,14 +1660,15 @@ addImpl' inpat env infns imp_meths ist ptm

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

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

16561662

1657−aiFn :: Bool -> Bool -> Bool

1663+aiFn :: Name -> Bool -> Bool -> Bool

16581664 -> [Name]

16591665 -> IState -> FC

16601666 -> Name -- ^ function being applied

16611667 -> FC -> [[T.Text]]

1662− -> [PArg] -- ^ initial arguments

1668+ -> [PArg] -- ^ initial arguments (if in a pattern)

1669+ -> [PArg] -- ^ initial arguments (if in an expression)

16631670 -> 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 [] _

16651672 = case lookupDef f (tt_ctxt ist) of

16661673 [] -> Right $ PPatvar ffc f

16671674 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in

@@ -1669,7 +1676,7 @@ aiFn inpat True qq imp_meths ist fc f ffc ds []

16691676 if (not (vname f) || tcname f

16701677 || any (conCaf (tt_ctxt ist)) ialts)

16711678-- 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

16731680 else Right $ PPatvar ffc f

16741681 where imp (PExp _ _ _ _) = False

16751682 imp _ = True

@@ -1683,9 +1690,9 @@ aiFn inpat True qq imp_meths ist fc f ffc ds []

16831690 vname (UN n) = True -- non qualified

16841691 vname _ = False

16851692

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

16871694 | 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

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

16901697 = do let ns = lookupCtxtName f (idris_implicits ist)

16911698 let nh = filter (\(n, _) -> notHidden n) ns

@@ -1693,15 +1700,25 @@ aiFn inpat expat qq imp_meths ist fc f ffc ds as

16931700 [] -> nh

16941701 x -> x

16951702 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))

16971705 [] -> if f `elem` (map fst (idris_metavars ist))

16981706 then Right $ PApp fc (PRef ffc [ffc] f) as

16991707 else Right $ mkPApp fc (length as) (PRef ffc [ffc] f) as

17001708 alts -> Right $

17011709 PAlternative [] (ExactlyOne True) $

17021710 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

17041712 where

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

1721+

17051722 -- if the name is in imp_meths, we should actually refer to the bound

17061723 -- name rather than the global one after expanding implicits

17071724 isImpName f f' | f `elem` imp_meths = f

src/Idris/Core/ProofState.hs+4−2

@@ -904,6 +904,8 @@ getProvenance :: Err -> (Maybe Provenance, Maybe Provenance)

904904getProvenance (CantUnify _ (_, lp) (_, rp) _ _ _) = (lp, rp)

905905getProvenance _ = (Nothing, Nothing)

906906

907+setReady (x, y, _, env, err, c, at) = (x, y, True, env, err, c, at)

908+

907909updateProblems :: ProofState -> [(Name, TT Name)] -> Fails

908910 -> ([(Name, TT Name)], Fails)

909911-- updateProblems ctxt [] ps inj holes = ([], ps)

@@ -1009,7 +1011,7 @@ processTactic (ComputeLet n) ps

10091011 computeLet (context ps) n

10101012 (getProofTerm (pterm ps)) }, "")

10111013processTactic UnifyProblems ps

1012− = do let (ns', probs') = updateProblems ps [] (problems ps)

1014+ = do let (ns', probs') = updateProblems ps [] (map setReady (problems ps))

10131015 pterm' = updateSolved ns' (pterm ps)

10141016 traceWhen (unifylog ps) ("(UnifyProblems) Dropping holes: " ++ show (map fst ns')) $

10151017 return (ps { pterm = pterm', solved = Nothing, problems = probs',

@@ -1020,7 +1022,7 @@ processTactic UnifyProblems ps

10201022 holes = holes ps \\ (map fst ns') }, plog ps)

10211023 where notIn ns (h, _) = h `notElem` map fst ns

10221024processTactic (MatchProblems all) ps

1023− = do let (ns', probs') = matchProblems all ps [] (problems ps)

1025+ = do let (ns', probs') = matchProblems all ps [] (map setReady (problems ps))

10241026 (ns'', probs'') = matchProblems all ps ns' probs'

10251027 pterm' = orderUpdateSolved ns'' (resetProofTerm (pterm ps))

10261028 traceWhen (unifylog ps) ("(MatchProblems) Dropping holes: " ++ show ns'') $