diff --git a/idris.cabal b/idris.cabal index ac3225539..6c3a2e3e0 100644 --- a/idris.cabal +++ b/idris.cabal @@ -240,6 +240,9 @@ Extra-source-files: test/reg045/run test/reg045/*.idr test/reg045/expected + test/reg046/run + test/reg046/*.idr + test/reg046/expected test/basic001/run test/basic001/*.idr diff --git a/libs/neweffects/Effect/State.idr b/libs/neweffects/Effect/State.idr index eda463514..55df66628 100644 --- a/libs/neweffects/Effect/State.idr +++ b/libs/neweffects/Effect/State.idr @@ -8,8 +8,8 @@ data State : Effect where Get : { a } State a Put : b -> { a ==> b } State () -using (m : Type -> Type) - instance Handler State m where +-- using (m : Type -> Type) +instance Handler State m where handle st Get k = k st st handle st (Put n) k = k () n diff --git a/src/Idris/Core/Elaborate.hs b/src/Idris/Core/Elaborate.hs index e2b9f93f5..2682ed010 100644 --- a/src/Idris/Core/Elaborate.hs +++ b/src/Idris/Core/Elaborate.hs @@ -514,8 +514,10 @@ apply' fillt fn imps = put (ES (p { dontunify = dont, unified = (n, unify), notunified = notunify ++ notunified p }, a) s prev) fillt (raw_apply fn (map (Var . snd) args)) --- trace ("Goal " ++ show g ++ "\n" ++ show (fn, imps, unify) ++ "\n" ++ show ptm) $ - end_unify + ulog <- getUnifyLog + g <- goal + traceWhen ulog ("Goal " ++ show g ++ " -- when elaborating " ++ show fn) $ + end_unify return $! (map (\(argName, argHole) -> (argName, updateUnify unify argHole)) args) where updateUnify us n = case lookup n us of Just (P _ t _) -> t diff --git a/src/Idris/Core/ProofState.hs b/src/Idris/Core/ProofState.hs index 6c6383079..7852a4114 100644 --- a/src/Idris/Core/ProofState.hs +++ b/src/Idris/Core/ProofState.hs @@ -871,7 +871,7 @@ updateNotunified ns nu = up nu where updateProblems :: Context -> [(Name, TT Name)] -> Fails -> [Name] -> [Name] -> ([(Name, TT Name)], Fails) -updateProblems ctxt [] ps inj holes = ([], ps) +-- updateProblems ctxt [] ps inj holes = ([], ps) updateProblems ctxt ns ps inj holes = up ns ps where up ns [] = (ns, []) up ns ((x, y, env, err, while, um) : ps) = diff --git a/src/Idris/Core/Unify.hs b/src/Idris/Core/Unify.hs index 05dd3281e..39b3765fd 100644 --- a/src/Idris/Core/Unify.hs +++ b/src/Idris/Core/Unify.hs @@ -428,18 +428,12 @@ unify ctxt env topx topy inj holes from = unApp fn bnames appx@(App fx ax) appy@(App fy ay) | (injectiveApp fx && injectiveApp fy) - || (injectiveApp fx && rigid appx && metavarApp appy && numArgs appx == numArgs appy) - || (injectiveApp fy && rigid appy && metavarApp appx && numArgs appx == numArgs appy) || (injectiveApp fx && metavarApp fy && ax == ay) || (injectiveApp fy && metavarApp fx && ax == ay) = do let (headx, _) = unApply fx let (heady, _) = unApply fy -- fail quickly if the heads are disjoint checkHeads headx heady --- if True then -- (injective fx || injective fy || fx == fy) then --- if (injective fx && metavarApp appy) || --- (injective fy && metavarApp appx) || --- (injective fx && injective fy) || fx == fy uplus (do hf <- un' True bnames fx fy let ax' = hnormalise hf ctxt env (substNames hf ax) @@ -624,9 +618,9 @@ envPos x i ((y, _) : ys) | x == y = i -- ASSUMPTION: inputs are in normal form recoverable t@(App _ _) _ - | (P _ (UN l) _, _) <- unApply t, l == txt "Lazy" = False + | (P _ (UN l) _, _) <- unApply t, l == txt "Lazy'" = False recoverable _ t@(App _ _) - | (P _ (UN l) _, _) <- unApply t, l == txt "Lazy" = False + | (P _ (UN l) _, _) <- unApply t, l == txt "Lazy'" = False recoverable (P (DCon _ _) x _) (P (DCon _ _) y _) = x == y recoverable (P (TCon _ _) x _) (P (TCon _ _) y _) = x == y recoverable (Constant _) (P (DCon _ _) y _) = False diff --git a/src/Idris/ElabTerm.hs b/src/Idris/ElabTerm.hs index a34fe5fa7..b6d52cfc5 100644 --- a/src/Idris/ElabTerm.hs +++ b/src/Idris/ElabTerm.hs @@ -245,12 +245,8 @@ elab ist info emode opts fn tm elab' ina (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes = do g <- goal; resolveTC 5 g fn ist elab' ina (PResolveTC fc) - | True = do c <- getNameFrom (sMN 0 "class") - instanceArg c - | otherwise = do g <- goal - try (resolveTC 2 g fn ist) - (do c <- getNameFrom (sMN 0 "class") - instanceArg c) + = do c <- getNameFrom (sMN 0 "class") + instanceArg c elab' ina (PRefl fc t) = elab' ina (PApp fc (PRef fc eqCon) [pimp (sMN 0 "A") Placeholder True, pimp (sMN 0 "x") t False]) @@ -485,7 +481,9 @@ elab ist info emode opts fn tm -- we can unify with them case lookupCtxt f (idris_classes ist) of [] -> return () - _ -> mapM_ setInjective (map getTm args) + _ -> do mapM_ setInjective (map getTm args) + -- maybe more things are solvable now + unifyProblems ctxt <- get_context let guarded = isConName f ctxt -- trace ("args is " ++ show args) $ return () @@ -498,10 +496,11 @@ elab ist info emode opts fn tm -- Sort so that the implicit tactics and alternatives go last let (ns', eargs) = unzip $ sortBy cmpArg (zip ns args) + ulog <- getUnifyLog elabArgs ist (ina || not isinf, guarded, inty, qq) [] fc False f ns' (f == sUN "Force") - (map (\x -> (False, getTm x)) eargs) -- TODO: remove this False arg + (map (\x -> getTm x) eargs) -- TODO: remove this False arg solve ivs' <- get_instances -- Attempt to resolve any type classes which have 'complete' types, @@ -525,16 +524,23 @@ elab ist info emode opts fn tm -- FIXME: Better would be to allow alternative resolution to be -- retried after more information is in. cmpArg (_, x) (_, y) + | constraint x && not (constraint y) = LT + | constraint y && not (constraint x) = GT + | otherwise = compare (conDepth 0 (getTm x) + priority x + alt x) (conDepth 0 (getTm y) + priority y + alt y) where alt t = case getTm t of PAlternative False _ -> 5 - PAlternative True _ -> 1 + PAlternative True _ -> 2 PTactics _ -> 150 - PLam _ _ _ -> 2 - PRewrite _ _ _ _ -> 3 - _ -> 0 + PLam _ _ _ -> 3 + PRewrite _ _ _ _ -> 4 + PResolveTC _ -> 0 + _ -> 1 + constraint (PConstraint _ _ _ _) = True + constraint _ = False + -- Score a point for every level where there is a non-constructor -- function (so higher score --> done later) -- Only relevant when on lhs @@ -546,6 +552,7 @@ elab ist info emode opts fn tm conDepth d (PPatvar _ _) = 0 conDepth d (PAlternative _ as) = maximum (map (conDepth d) as) conDepth d Placeholder = 0 + conDepth d (PResolveTC _) = 0 conDepth d t = max (100 - d) 1 checkIfInjective n = do @@ -558,7 +565,14 @@ elab ist info emode opts fn tm case lookupCtxt c (idris_classes ist) of [] -> return () _ -> -- type class, set as injective - mapM_ setinjArg args + do mapM_ setinjArg args + -- maybe we can solve more things now... + ulog <- getUnifyLog + probs <- get_probs + traceWhen ulog ("Injective now " ++ show args ++ "\n" ++ qshow probs) $ + unifyProblems + probs <- get_probs + traceWhen ulog (qshow probs) $ return () _ -> return () setinjArg (P _ n _) = setinj n @@ -832,17 +846,13 @@ elab ist info emode opts fn tm -> Name -- ^ Name of the function being applied -> [(Name, Name)] -- ^ (Argument Name, Hole Name) -> Bool -- ^ under a 'force' - -> [(Bool, PTerm)] -- ^ (Laziness, argument) + -> [PTerm] -- ^ (Laziness, argument) -> ElabD () elabArgs ist ina failed fc retry f [] force _ = return () - elabArgs ist ina failed fc r f (n:ns) force ((_, Placeholder) : args) + elabArgs ist ina failed fc r f (n:ns) force (Placeholder : args) = elabArgs ist ina failed fc r f ns force args - elabArgs ist ina failed fc r f ((argName, holeName):ns) force ((lazy, t) : args) - | lazy && not pattern - = elabArg argName holeName (PApp bi (PRef bi (sUN "Delay")) - [pimp (sUN "a") Placeholder True, - pexp t]) - | otherwise = elabArg argName holeName t + elabArgs ist ina failed fc r f ((argName, holeName):ns) force (t : args) + = do elabArg argName holeName t where elabArg argName holeName t = do now_elaborating fc f argName wrapErr f argName $ do @@ -854,7 +864,11 @@ elab ist info emode opts fn tm failed' <- -- trace (show (n, t, hs, tm)) $ -- traceWhen (not (null cs)) (show ty ++ "\n" ++ showImp True t) $ case holeName `elem` hs of - True -> do focus holeName; elab ina t; return failed + True -> do focus holeName; + g <- goal + ulog <- getUnifyLog + traceWhen ulog ("Elaborating argument " ++ show (argName, holeName, g)) $ + elab ina t; return failed False -> return failed done_elaborating_arg f argName elabArgs ist ina failed fc r f ns force args diff --git a/test/error003/ErrorReflection.idr b/test/error003/ErrorReflection.idr index 7c8fe4c25..11b512ca7 100644 --- a/test/error003/ErrorReflection.idr +++ b/test/error003/ErrorReflection.idr @@ -58,7 +58,7 @@ dslerr (CantUnify _ tm1 tm2 _ _ _) = do tm1' <- getTmTy tm1 tm2' <- getTmTy tm2 ty1 <- reifyTy tm1' ty2 <- reifyTy tm2' - return [TextPart $ "DSL type error: " ++ (show ty1) ++ " doesn't match " ++(show ty2)] + Just [TextPart $ "DSL type error: " ++ (show ty1) ++ " doesn't match " ++(show ty2)] dslerr _ = Nothing diff --git a/test/reg046/expected b/test/reg046/expected new file mode 100644 index 000000000..e69de29bb diff --git a/test/reg046/reg046.idr b/test/reg046/reg046.idr new file mode 100644 index 000000000..a3c005dbf --- /dev/null +++ b/test/reg046/reg046.idr @@ -0,0 +1,19 @@ +module test + +data MyList : (A : Type) -> Type where + nil : (A : Type) -> MyList A + cons : (A : Type) -> A -> MyList A -> MyList A + +elimList : (A : Type) -> + (m : MyList A -> Type) -> + (f1 : m (nil A)) -> + (f2 : (a : A) -> (as : MyList A) -> m as -> m (cons A a as)) -> + (e : MyList A) -> + m e +elimList A m f1 f2 (nil A) = f1 +elimList A m f1 f2 (cons A a as) = f2 a as (elimList A m f1 f2 as) + +append : (A : Type) -> (b : MyList A) -> (c : MyList A) -> MyList A +append A b c = (elimList A (\ d => MyList A) c + (\ d => \ e => \ f => cons A d f) + b) diff --git a/test/reg046/run b/test/reg046/run new file mode 100755 index 000000000..6e7526d7e --- /dev/null +++ b/test/reg046/run @@ -0,0 +1,3 @@ +#!/usr/bin/env bash +idris $@ reg046.idr --check +rm -f reg046 *.ibc