From b573bf0e63e56c7588d5ba74cb40bcac818c5927 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Tue, 1 Sep 2015 20:26:35 +0100 Subject: [PATCH] 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. --- src/Idris/AbsSyntax.hs | 159 +++++++++++++++++++---------------- src/Idris/Core/ProofState.hs | 6 +- 2 files changed, 92 insertions(+), 73 deletions(-) diff --git a/src/Idris/AbsSyntax.hs b/src/Idris/AbsSyntax.hs index df9daf5f8..628c6a533 100644 --- a/src/Idris/AbsSyntax.hs +++ b/src/Idris/AbsSyntax.hs @@ -1550,103 +1550,109 @@ addImpl = addImpl' False [] [] addImpl' :: Bool -> [Name] -> [Name] -> [Name] -> IState -> PTerm -> PTerm addImpl' inpat env infns imp_meths ist ptm - = mkUniqueNames env [] (ai False (zip env (repeat Nothing)) [] ptm) + = mkUniqueNames env [] (ai inpat False (zip env (repeat Nothing)) [] ptm) where - ai :: Bool -> [(Name, Maybe PTerm)] -> [[T.Text]] -> PTerm -> PTerm - ai qq env ds (PRef fc fcs f) + topname = case ptm of + PRef _ _ n -> n + PApp _ (PRef _ _ n) _ -> n + _ -> sUN "" -- doesn't matter then + + ai :: Bool -> Bool -> [(Name, Maybe PTerm)] -> [[T.Text]] -> PTerm -> PTerm + ai inpat qq env ds (PRef fc fcs f) | f `elem` infns = PInferRef fc fcs f - | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat qq imp_meths ist fc f fc ds [] - ai qq env ds (PHidden (PRef fc hl f)) - | not (f `elem` map fst env) = PHidden (handleErr $ aiFn inpat False qq imp_meths ist fc f fc ds []) - ai qq env ds (PRewrite fc l r g) - = let l' = ai qq env ds l - r' = ai qq env ds r - g' = fmap (ai qq env ds) g in + | not (f `elem` map fst env) = handleErr $ aiFn topname inpat inpat qq imp_meths ist fc f fc ds [] [] + ai inpat qq env ds (PHidden (PRef fc hl f)) + | not (f `elem` map fst env) = PHidden (handleErr $ aiFn topname inpat False qq imp_meths ist fc f fc ds [] []) + ai inpat qq env ds (PRewrite fc l r g) + = let l' = ai inpat qq env ds l + r' = ai inpat qq env ds r + g' = fmap (ai inpat qq env ds) g in PRewrite fc l' r' g' - ai qq env ds (PTyped l r) - = let l' = ai qq env ds l - r' = ai qq env ds r in + ai inpat qq env ds (PTyped l r) + = let l' = ai inpat qq env ds l + r' = ai inpat qq env ds r in PTyped l' r' - ai qq env ds (PPair fc hls p l r) - = let l' = ai qq env ds l - r' = ai qq env ds r in + ai inpat qq env ds (PPair fc hls p l r) + = let l' = ai inpat qq env ds l + r' = ai inpat qq env ds r in PPair fc hls p l' r' - ai qq env ds (PDPair fc hls p l t r) - = let l' = ai qq env ds l - t' = ai qq env ds t - r' = ai qq env ds r in + ai inpat qq env ds (PDPair fc hls p l t r) + = let l' = ai inpat qq env ds l + t' = ai inpat qq env ds t + r' = ai inpat qq env ds r in PDPair fc hls p l' t' r' - ai qq env ds (PAlternative ms a as) - = let as' = map (ai qq env ds) as in + ai inpat qq env ds (PAlternative ms a as) + = let as' = map (ai inpat qq env ds) as in PAlternative ms a as' - ai qq env _ (PDisamb ds' as) = ai qq env ds' as - ai qq env ds (PApp fc (PInferRef ffc hl f) as) - = let as' = map (fmap (ai qq env ds)) as in + ai inpat qq env _ (PDisamb ds' as) = ai inpat qq env ds' as + ai inpat qq env ds (PApp fc (PInferRef ffc hl f) as) + = let as' = map (fmap (ai inpat qq env ds)) as in PApp fc (PInferRef ffc hl f) as' - ai qq env ds (PApp fc ftm@(PRef ffc hl f) as) - | f `elem` infns = ai qq env ds (PApp fc (PInferRef ffc hl f) as) + ai inpat qq env ds (PApp fc ftm@(PRef ffc hl f) as) + | f `elem` infns = ai inpat qq env ds (PApp fc (PInferRef ffc hl f) as) | not (f `elem` map fst env) - = let as' = map (fmap (ai qq env ds)) as in - handleErr $ aiFn inpat False qq imp_meths ist fc f ffc ds as' + = let as' = map (fmap (ai inpat qq env ds)) as + asdotted' = map (fmap (ai False qq env ds)) as in + handleErr $ aiFn topname inpat False qq imp_meths ist fc f ffc ds as' asdotted' | Just (Just ty) <- lookup f env = - let as' = map (fmap (ai qq env ds)) as + let as' = map (fmap (ai inpat qq env ds)) as arity = getPArity ty in mkPApp fc arity ftm as' - ai qq env ds (PApp fc f as) - = let f' = ai qq env ds f - as' = map (fmap (ai qq env ds)) as in + ai inpat qq env ds (PApp fc f as) + = let f' = ai inpat qq env ds f + as' = map (fmap (ai inpat qq env ds)) as in mkPApp fc 1 f' as' - ai qq env ds (PCase fc c os) - = let c' = ai qq env ds c in + ai inpat qq env ds (PCase fc c os) + = let c' = ai inpat qq env ds c in -- leave os alone, because they get lifted into a new pattern match - -- definition which is passed through addImpl again with more scope + -- definition which is passed through addImpl agai inpatn with more scope -- information PCase fc c' os - ai qq env ds (PIfThenElse fc c t f) = PIfThenElse fc (ai qq env ds c) - (ai qq env ds t) - (ai qq env ds f) + ai inpat qq env ds (PIfThenElse fc c t f) = PIfThenElse fc (ai inpat qq env ds c) + (ai inpat qq env ds t) + (ai inpat qq env ds f) -- If the name in a lambda is a constructor name, do this as a 'case' -- instead (it is harmless to do so, especially since the lambda will -- be lifted anyway!) - ai qq env ds (PLam fc n nfc ty sc) + ai inpat qq env ds (PLam fc n nfc ty sc) = case lookupDef n (tt_ctxt ist) of - [] -> let ty' = ai qq env ds ty - sc' = ai qq ((n, Just ty):env) ds sc in + [] -> let ty' = ai inpat qq env ds ty + sc' = ai inpat qq ((n, Just ty):env) ds sc in PLam fc n nfc ty' sc' - _ -> ai qq env ds (PLam fc (sMN 0 "lamp") NoFC ty + _ -> ai inpat qq env ds (PLam fc (sMN 0 "lamp") NoFC ty (PCase fc (PRef fc [] (sMN 0 "lamp") ) [(PRef fc [] n, sc)])) - ai qq env ds (PLet fc n nfc ty val sc) + ai inpat qq env ds (PLet fc n nfc ty val sc) = case lookupDef n (tt_ctxt ist) of - [] -> let ty' = ai qq env ds ty - val' = ai qq env ds val - sc' = ai qq ((n, Just ty):env) ds sc in + [] -> let ty' = ai inpat qq env ds ty + val' = ai inpat qq env ds val + sc' = ai inpat qq ((n, Just ty):env) ds sc in PLet fc n nfc ty' val' sc' defs -> - ai qq env ds (PCase fc val [(PRef fc [] n, sc)]) - ai qq env ds (PPi p n nfc ty sc) - = let ty' = ai qq env ds ty + ai inpat qq env ds (PCase fc val [(PRef fc [] n, sc)]) + ai inpat qq env ds (PPi p n nfc ty sc) + = let ty' = ai inpat qq env ds ty env' = if n `elem` imp_meths then env else ((n, Just ty) : env) - sc' = ai qq env' ds sc in + sc' = ai inpat qq env' ds sc in PPi p n nfc ty' sc' - ai qq env ds (PGoal fc r n sc) - = let r' = ai qq env ds r - sc' = ai qq ((n, Nothing):env) ds sc in + ai inpat qq env ds (PGoal fc r n sc) + = let r' = ai inpat qq env ds r + sc' = ai inpat qq ((n, Nothing):env) ds sc in PGoal fc r' n sc' - ai qq env ds (PHidden tm) = PHidden (ai qq env ds tm) + ai inpat qq env ds (PHidden tm) = PHidden (ai inpat qq env ds tm) -- Don't do PProof or PTactics since implicits get added when scope is -- properly known in ElabTerm.runTac - ai qq env ds (PUnifyLog tm) = PUnifyLog (ai qq env ds tm) - ai qq env ds (PNoImplicits tm) = PNoImplicits (ai qq env ds tm) - ai qq env ds (PQuasiquote tm g) = PQuasiquote (ai True env ds tm) - (fmap (ai True env ds) g) - ai qq env ds (PUnquote tm) = PUnquote (ai False env ds tm) - ai qq env ds (PRunElab fc tm ns) = PRunElab fc (ai False env ds tm) ns - ai qq env ds (PConstSugar fc tm) = PConstSugar fc (ai qq env ds tm) - ai qq env ds tm = tm + ai inpat qq env ds (PUnifyLog tm) = PUnifyLog (ai inpat qq env ds tm) + ai inpat qq env ds (PNoImplicits tm) = PNoImplicits (ai inpat qq env ds tm) + ai inpat qq env ds (PQuasiquote tm g) = PQuasiquote (ai inpat True env ds tm) + (fmap (ai inpat True env ds) g) + ai inpat qq env ds (PUnquote tm) = PUnquote (ai inpat False env ds tm) + ai inpat qq env ds (PRunElab fc tm ns) = PRunElab fc (ai inpat False env ds tm) ns + ai inpat qq env ds (PConstSugar fc tm) = PConstSugar fc (ai inpat qq env ds tm) + ai inpat qq env ds tm = tm handleErr (Left err) = PElabError err handleErr (Right x) = x @@ -1654,14 +1660,15 @@ addImpl' inpat env infns imp_meths ist ptm -- if in a pattern, and there are no arguments, and there's no possible -- names with zero explicit arguments, don't add implicits. -aiFn :: Bool -> Bool -> Bool +aiFn :: Name -> Bool -> Bool -> Bool -> [Name] -> IState -> FC -> Name -- ^ function being applied -> FC -> [[T.Text]] - -> [PArg] -- ^ initial arguments + -> [PArg] -- ^ initial arguments (if in a pattern) + -> [PArg] -- ^ initial arguments (if in an expression) -> Either Err PTerm -aiFn inpat True qq imp_meths ist fc f ffc ds [] +aiFn topname inpat True qq imp_meths ist fc f ffc ds [] _ = case lookupDef f (tt_ctxt ist) of [] -> Right $ PPatvar ffc f alts -> let ialts = lookupCtxtName f (idris_implicits ist) in @@ -1669,7 +1676,7 @@ aiFn inpat True qq imp_meths ist fc f ffc ds [] if (not (vname f) || tcname f || any (conCaf (tt_ctxt ist)) ialts) -- any constructor alts || any allImp ialts)) - then aiFn inpat False qq imp_meths ist fc f ffc ds [] -- use it as a constructor + then aiFn topname inpat False qq imp_meths ist fc f ffc ds [] [] -- use it as a constructor else Right $ PPatvar ffc f where imp (PExp _ _ _ _) = False imp _ = True @@ -1683,9 +1690,9 @@ aiFn inpat True qq imp_meths ist fc f ffc ds [] vname (UN n) = True -- non qualified vname _ = False -aiFn inpat expat qq imp_meths ist fc f ffc ds as +aiFn topname inpat expat qq imp_meths ist fc f ffc ds as asexp | f `elem` primNames = Right $ PApp fc (PRef ffc [ffc] f) as -aiFn inpat expat qq imp_meths ist fc f ffc ds as +aiFn topname inpat expat qq imp_meths ist fc f ffc ds as asexp -- This is where namespaces get resolved by adding PAlternative = do let ns = lookupCtxtName f (idris_implicits ist) let nh = filter (\(n, _) -> notHidden n) ns @@ -1693,15 +1700,25 @@ aiFn inpat expat qq imp_meths ist fc f ffc ds as [] -> nh x -> x case ns' of - [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef ffc [ffc] (isImpName f f')) (insertImpl ns as) + [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef ffc [ffc] (isImpName f f')) + (insertImpl ns (chooseArgs f' as asexp)) [] -> if f `elem` (map fst (idris_metavars ist)) then Right $ PApp fc (PRef ffc [ffc] f) as else Right $ mkPApp fc (length as) (PRef ffc [ffc] f) as alts -> Right $ PAlternative [] (ExactlyOne True) $ map (\(f', ns) -> mkPApp fc (length ns) (PRef ffc [ffc] (isImpName f f')) - (insertImpl ns as)) alts + (insertImpl ns (chooseArgs f' as asexp))) alts where + -- choose whether to treat the arguments as patterns or expressions + -- if 'f' is a defined function, treat as expression, otherwise do the default. + -- This is so any names which later go under a PHidden are treated + -- as function names rather than bound pattern variables + chooseArgs f as asexp | isConName f (tt_ctxt ist) = as + | f == topname = as + | Nothing <- lookupDefExact f (tt_ctxt ist) = as + | otherwise = asexp + -- if the name is in imp_meths, we should actually refer to the bound -- name rather than the global one after expanding implicits isImpName f f' | f `elem` imp_meths = f diff --git a/src/Idris/Core/ProofState.hs b/src/Idris/Core/ProofState.hs index b5f2bbbc9..588156458 100644 --- a/src/Idris/Core/ProofState.hs +++ b/src/Idris/Core/ProofState.hs @@ -904,6 +904,8 @@ getProvenance :: Err -> (Maybe Provenance, Maybe Provenance) getProvenance (CantUnify _ (_, lp) (_, rp) _ _ _) = (lp, rp) getProvenance _ = (Nothing, Nothing) +setReady (x, y, _, env, err, c, at) = (x, y, True, env, err, c, at) + updateProblems :: ProofState -> [(Name, TT Name)] -> Fails -> ([(Name, TT Name)], Fails) -- updateProblems ctxt [] ps inj holes = ([], ps) @@ -1009,7 +1011,7 @@ processTactic (ComputeLet n) ps computeLet (context ps) n (getProofTerm (pterm ps)) }, "") processTactic UnifyProblems ps - = do let (ns', probs') = updateProblems ps [] (problems ps) + = do let (ns', probs') = updateProblems ps [] (map setReady (problems ps)) pterm' = updateSolved ns' (pterm ps) traceWhen (unifylog ps) ("(UnifyProblems) Dropping holes: " ++ show (map fst ns')) $ return (ps { pterm = pterm', solved = Nothing, problems = probs', @@ -1020,7 +1022,7 @@ processTactic UnifyProblems ps holes = holes ps \\ (map fst ns') }, plog ps) where notIn ns (h, _) = h `notElem` map fst ns processTactic (MatchProblems all) ps - = do let (ns', probs') = matchProblems all ps [] (problems ps) + = do let (ns', probs') = matchProblems all ps [] (map setReady (problems ps)) (ns'', probs'') = matchProblems all ps ns' probs' pterm' = orderUpdateSolved ns'' (resetProofTerm (pterm ps)) traceWhen (unifylog ps) ("(MatchProblems) Dropping holes: " ++ show ns'') $