ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-09-21 22:17:19 +03:00
Code Issues Projects Releases Wiki Activity

Remove dodgy unification hack

Browse Source 
Also need to recheck unification problems immediately after setting
injective arguments, or we get strange results for disambiguation.
Fixes #1372
This commit is contained in:
Edwin Brady 2014-07-11 14:26:30 +01:00
parent b7756f2d23
commit 8ed343ba6a
10 changed files with 71 additions and 36 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
idris.cabal
View File

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

4
libs/neweffects/Effect/State.idr
View File

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

6
src/Idris/Core/Elaborate.hs
View File

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

2
src/Idris/Core/ProofState.hs
View File

@ -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) =

10
src/Idris/Core/Unify.hs
View File

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

58
src/Idris/ElabTerm.hs
View File

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

2
test/error003/ErrorReflection.idr
View File

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

0
test/reg046/expected Normal file
View File

19
test/reg046/reg046.idr Normal file
View File

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

3
test/reg046/run Executable file
View File

@ -0,0 +1,3 @@
#!/usr/bin/env bash
idris $@ reg046.idr --check
rm -f reg046 *.ibc