8897b31 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix evaluation/elaboration of holes in expressions

Not that we often do this, but it should still work - elaborating an expression with a hole in at the REPL no longer causes an internal error.

commit8897b31e1a994928a29bf30b8f861c5934df5cd4 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 19 Jun 2016, 17:30 (10 years ago) parent1c927eb

2 files changed+12−7

compare with master

unifiedsplit

libs/contrib/Data/Heap.idr+3−4 src/Idris/AbsSyntax.hs+9−3

libs/contrib/Data/Heap.idr+3−4

@@ -61,11 +61,10 @@ orderBySize left centre right =

6161 largest : Nat

6262 largest = maximum (size left) $ maximum (size centre) (size right)

6363

64−%assert_total -- relies on orderBySize doing the right thing

6564merge : Ord a => MaxiphobicHeap a -> MaxiphobicHeap a -> MaxiphobicHeap a

6665merge Empty right = right

6766merge 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

6968 if le < re then

7069 let (largest, b, c) = orderBySize ll lr (Node rs rl re rr) in

7170 Node mergedSize largest le (merge b c)

@@ -99,9 +98,9 @@ toList : Ord a => MaxiphobicHeap a -> List a

9998toList Empty = []

10099toList (Node s l e r) = toList' (Node s l e r) Refl

101100 where

102− %assert_total -- relies on deleteMinimum making heap smaller

103101 toList' : Ord a => (h : MaxiphobicHeap a) -> (isEmpty h = False) -> List a

104− toList' heap p = findMinimum heap p :: (Heap.toList (deleteMinimum heap p))

102+ toList' heap p = assert_total $ -- relies on deleteMinimum making heap smaller

103+ findMinimum heap p :: (Heap.toList (deleteMinimum heap p))

105104

106105fromList : Ord a => List a -> MaxiphobicHeap a

107106fromList = 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

19391939 case ns' of

19401940 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef ffc [ffc] (isImpName f f'))

19411941 (insertImpl ns as)

1942− [] -> if f `elem` (map fst (idris_metavars ist))

1943− then Right $ PApp fc (PRef ffc [ffc] f) as

1944− else Right $ mkPApp fc (length as) (PRef ffc [ffc] f) as

1942+ [] -> case metaVar f (map fst (idris_metavars ist)) of

1943+ Just f' -> Right $ PApp fc (PRef ffc [ffc] f') as

1944+ Nothing -> Right $ mkPApp fc (length as) (PRef ffc [ffc] f) as

19451945 alts -> Right $

19461946 PAlternative [] (ExactlyOne True) $

19471947 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

19521952 isImpName f f' | f `elem` imp_meths = f

19531953 | otherwise = f'

19541954

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+

19551961 trimAlts [] alts = alts

19561962 trimAlts ns alts

19571963 = filter (\(x, _) -> any (\d -> d `isPrefixOf` nspace x) ns) alts