git.iko.soy/Idris-dev
on master help sign in
Remove priority ordering on function arguments
f9678b7Edwin Brady
src/Core/Unify.hs+11−5
compare with master
unifiedsplit
@@ -28,14 +28,14 @@ unify ctxt env topx topy
28 = -- case runStateT (un' False [] topx topy) (UI 0 [] []) of
28 = -- case runStateT (un' False [] topx topy) (UI 0 [] []) of
29 -- OK (v, UI _ inj []) -> return (filter notTrivial v, inj, [])
29 -- OK (v, UI _ inj []) -> return (filter notTrivial v, inj, [])
30 -- _ ->
30 -- _ ->
31−-- trace ("Unifying " ++ show (topx, topy)) $
31+-- trace ("Unifying " ++ show (topx, topy)) $
32 let topxn = normalise ctxt env topx
32 let topxn = normalise ctxt env topx
33 topyn = normalise ctxt env topy in
33 topyn = normalise ctxt env topy in
34-- trace ("Unifying " ++ show (topxn, topyn)) $
34-- trace ("Unifying " ++ show (topxn, topyn)) $
35 case runStateT (un' False [] topxn topyn)
35 case runStateT (un' False [] topxn topyn)
36 (UI 0 [] []) of
36 (UI 0 [] []) of
37+ OK (v, UI _ inj fails) ->
37− OK (v, UI _ inj fails) -> return (filter notTrivial v, inj, reverse fails)
38+ return (filter notTrivial v, inj, reverse fails)
38−-- OK (_, UI s _ ((_,_,f):fs)) -> tfail $ CantUnify topx topy f s
39 Error e -> tfail e
39 Error e -> tfail e
40 where
40 where
41 notTrivial (x, P _ x' _) = x /= x'
41 notTrivial (x, P _ x' _) = x /= x'
@@ -75,12 +75,18 @@ unify ctxt env topx topy
75 | (x,y) `elem` bnames = do sc 1; return []
75 | (x,y) `elem` bnames = do sc 1; return []
76 un' fn bnames (P Bound x _) tm
76 un' fn bnames (P Bound x _) tm
77 | holeIn env x = do UI s i f <- get
77 | holeIn env x = do UI s i f <- get
78+ -- injectivity check
79+ when (notP tm && fn) $
80+-- trace (show (x, tm, normalise ctxt env tm)) $
78− when (notP tm && fn) $ put (UI s ((tm, topx, topy) : i) f)
81+ put (UI s ((tm, topx, topy) : i) f)
79 sc 1
82 sc 1
80 checkCycle (x, tm)
83 checkCycle (x, tm)
81 un' fn bnames tm (P Bound y _)
84 un' fn bnames tm (P Bound y _)
82 | holeIn env y = do UI s i f <- get
85 | holeIn env y = do UI s i f <- get
86+ -- injectivity check
87+ when (notP tm && fn) $
88+-- trace (show (y, tm, normalise ctxt env tm)) $
83− when (notP tm && fn) $ put (UI s ((tm, topx, topy) : i) f)
89+ put (UI s ((tm, topx, topy) : i) f)
84 sc 1
90 sc 1
85 checkCycle (y, tm)
91 checkCycle (y, tm)
86 un' fn bnames (V i) (P Bound x _)
92 un' fn bnames (V i) (P Bound x _)
src/Idris/AbsSyntax.hs+2−2
@@ -577,13 +577,13 @@ mapsnd f (x, t) = (x, f t)
577-- * finally, everything else (3)
577-- * finally, everything else (3)
578
578
579getPriority :: IState -> PTerm -> Int
579getPriority :: IState -> PTerm -> Int
580−getPriority i tm = pri tm
580+getPriority i tm = 1 -- pri tm
581 where
581 where
582 pri (PRef _ n) =
582 pri (PRef _ n) =
583 case lookupP Nothing n (tt_ctxt i) of
583 case lookupP Nothing n (tt_ctxt i) of
584 ((P (DCon _ _) _ _):_) -> 1
584 ((P (DCon _ _) _ _):_) -> 1
585 ((P (TCon _ _) _ _):_) -> 1
585 ((P (TCon _ _) _ _):_) -> 1
586− ((P Ref _ _):_) -> 4
586+ ((P Ref _ _):_) -> 1
587 [] -> 0 -- must be locally bound, if it's not an error...
587 [] -> 0 -- must be locally bound, if it's not an error...
588 pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))
588 pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))
589 pri (PTrue _) = 0
589 pri (PTrue _) = 0