git.iko.soy/Idris-dev
on master help sign in
Fix evaluation/elaboration of holes in expressions
8897b31Edwin Brady
libs/contrib/Data/Heap.idr+3−4
compare with master
unifiedsplit
@@ -61,11 +61,10 @@ orderBySize left centre right =
61 largest : Nat
61 largest : Nat
62 largest = maximum (size left) $ maximum (size centre) (size right)
62 largest = maximum (size left) $ maximum (size centre) (size right)
63
63
64−%assert_total -- relies on orderBySize doing the right thing
65merge : Ord a => MaxiphobicHeap a -> MaxiphobicHeap a -> MaxiphobicHeap a
64merge : Ord a => MaxiphobicHeap a -> MaxiphobicHeap a -> MaxiphobicHeap a
66merge Empty right = right
65merge Empty right = right
67merge left Empty = left
66merge left Empty = left
68−merge (Node ls ll le lr) (Node rs rl re rr) =
67+merge (Node ls ll le lr) (Node rs rl re rr) = assert_total $ -- relies on orderBySize doing the right thing
69 if le < re then
68 if le < re then
70 let (largest, b, c) = orderBySize ll lr (Node rs rl re rr) in
69 let (largest, b, c) = orderBySize ll lr (Node rs rl re rr) in
71 Node mergedSize largest le (merge b c)
70 Node mergedSize largest le (merge b c)
@@ -99,9 +98,9 @@ toList : Ord a => MaxiphobicHeap a -> List a
99toList Empty = []
98toList Empty = []
100toList (Node s l e r) = toList' (Node s l e r) Refl
99toList (Node s l e r) = toList' (Node s l e r) Refl
101 where
100 where
102− %assert_total -- relies on deleteMinimum making heap smaller
103 toList' : Ord a => (h : MaxiphobicHeap a) -> (isEmpty h = False) -> List a
101 toList' : Ord a => (h : MaxiphobicHeap a) -> (isEmpty h = False) -> List a
102+ toList' heap p = assert_total $ -- relies on deleteMinimum making heap smaller
104− toList' heap p = findMinimum heap p :: (Heap.toList (deleteMinimum heap p))
103+ findMinimum heap p :: (Heap.toList (deleteMinimum heap p))
105
104
106fromList : Ord a => List a -> MaxiphobicHeap a
105fromList : Ord a => List a -> MaxiphobicHeap a
107fromList = foldr insert empty
106fromList = foldr insert empty
src/Idris/AbsSyntax.hs+9−3
@@ -1939,9 +1939,9 @@ aiFn topname inpat expat qq imp_meths ist fc f ffc ds as
1939 case ns' of
1939 case ns' of
1940 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef ffc [ffc] (isImpName f f'))
1940 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef ffc [ffc] (isImpName f f'))
1941 (insertImpl ns as)
1941 (insertImpl ns as)
1942− [] -> if f `elem` (map fst (idris_metavars ist))
1942+ [] -> case metaVar f (map fst (idris_metavars ist)) of
1943− then Right $ PApp fc (PRef ffc [ffc] f) as
1943+ Just f' -> Right $ PApp fc (PRef ffc [ffc] f') as
1944− else Right $ mkPApp fc (length as) (PRef ffc [ffc] f) as
1944+ Nothing -> Right $ mkPApp fc (length as) (PRef ffc [ffc] f) as
1945 alts -> Right $
1945 alts -> Right $
1946 PAlternative [] (ExactlyOne True) $
1946 PAlternative [] (ExactlyOne True) $
1947 map (\(f', ns) -> mkPApp fc (length ns) (PRef ffc [ffc] (isImpName f f'))
1947 map (\(f', ns) -> mkPApp fc (length ns) (PRef ffc [ffc] (isImpName f f'))
@@ -1952,6 +1952,12 @@ aiFn topname inpat expat qq imp_meths ist fc f ffc ds as
1952 isImpName f f' | f `elem` imp_meths = f
1952 isImpName f f' | f `elem` imp_meths = f
1953 | otherwise = f'
1953 | otherwise = f'
1954
1954
1955+ -- If it's a metavariable name, try to qualify it from the list of
1956+ -- unsolved metavariables
1957+ metaVar f (mvn : ns) | f == nsroot mvn = Just mvn
1958+ metaVar f (_ : ns) = metaVar f ns
1959+ metaVar f [] = Nothing
1960+
1955 trimAlts [] alts = alts
1961 trimAlts [] alts = alts
1956 trimAlts ns alts
1962 trimAlts ns alts
1957 = filter (\(x, _) -> any (\d -> d `isPrefixOf` nspace x) ns) alts
1963 = filter (\(x, _) -> any (\d -> d `isPrefixOf` nspace x) ns) alts