6cb70bc · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix for simple function applications

commit6cb70bc6eb9eed1f4b920f912412524990d644e4 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateWed 2 May 2012, 20:04 (14 years ago) parente1c7b0f

6 files changed+46−16

compare with master

unifiedsplit

src/Core/Elaborate.hs+10 src/Core/ProofState.hs+7−2 src/Core/TT.hs+4−1 src/Core/Unify.hs+15−11 src/Idris/Delaborate.hs+4 src/Idris/ElabTerm.hs+6−2

src/Core/Elaborate.hs+10

@@ -169,6 +169,10 @@ elog :: String -> Elab' aux ()

169169elog str = do ES p logs prev <- get

170170 put (ES p (logs ++ str ++ "\n") prev)

171171

172+getLog :: Elab' aux String

173+getLog = do ES p logs _ <- get

174+ return logs

175+

172176-- The primitives, from ProofState

173177

174178attack :: Elab' aux ()

@@ -402,6 +406,12 @@ simple_app fun arg =

402406 (do focus f; fun

403407 focus s; arg)

404408 complete_fill

409+ hs <- get_holes

410+ -- We don't need a and b in the hole queue any more since they were just for

411+ -- checking f, so discard them if they are still there. If they haven't been solved,

412+ -- regret will fail

413+ when (a `elem` hs) $ do focus a; regret

414+ when (b `elem` hs) $ do focus b; regret

405415 end_unify

406416

407417-- Abstract over an argument of unknown type, giving a name for the hole

src/Core/ProofState.hs+7−2

@@ -294,9 +294,12 @@ defer n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =

294294

295295 getP (n, b) = P Bound n (binderTy b)

296296

297−-- Hmmm. YAGNI?

298297regret :: RunTactic

299−regret = undefined

298+regret ctxt env (Bind x (Hole t) sc) | noOccurrence x sc =

299+ do action (\ps -> let hs = holes ps in

300+ ps { holes = hs \\ [x] })

301+ return sc

302+regret ctxt env (Bind x (Hole t) _) = fail $ show x ++ " : " ++ show t ++ " is not solved"

300303

301304addInj :: [(Term, Term, Term)] -> StateT TState TC ()

302305addInj inj = do ps <- get

@@ -315,6 +318,8 @@ fill :: Raw -> RunTactic

315318fill guess ctxt env (Bind x (Hole ty) sc) =

316319 do (val, valty) <- lift $ check ctxt env guess

317320 s <- get

321+-- let valtyn = normalise ctxt env valty

322+-- let tyn = normalise ctxt env ty

318323 ns <- unify' ctxt env valty ty

319324 ps <- get

320325 let (uh, uns) = unified ps

src/Core/TT.hs+4−1

@@ -43,6 +43,7 @@ instance Show FC where

4343 show (FC f l) = f ++ ":" ++ show l

4444

4545data Err = Msg String

46+ | InternalMsg String

4647 | CantUnify Term Term Err [(Name, Type)] Int -- Int is 'score' - how much we did unify

4748 | NoSuchVariable Name

4849 | NotInjective Term Term Term

@@ -56,6 +57,7 @@ data Err = Msg String

5657

5758instance Sized Err where

5859 size (Msg msg) = length msg

60+ size (InternalMsg msg) = length msg

5961 size (CantUnify left right err _ score) = size left + size right + size err

6062 size (NoSuchVariable name) = size name

6163 size (NotInjective l c r) = size l + size c + size r

@@ -74,6 +76,7 @@ score _ = 0

7476

7577instance Show Err where

7678 show (Msg s) = s

79+ show (InternalMsg s) = "Internal error: " ++ show s

7780 show (CantUnify l r e sc i) = "CantUnify " ++ show l ++ " " ++ show r ++ " "

7881 ++ show e ++ " in " ++ show sc ++ " " ++ show i

7982 show (Inaccessible n) = show n ++ " is not an accessible pattern variable"

@@ -115,7 +118,7 @@ instance Monad TC where

115118 x >>= k = case x of

116119 OK v -> k v

117120 Error e -> Error e

118− fail e = Error (Msg e)

121+ fail e = Error (InternalMsg e)

119122

120123tfail :: Err -> TC a

121124tfail e = Error e

src/Core/Unify.hs+15−11

@@ -25,12 +25,15 @@ data UInfo = UI Int Injs Fails

2525unify :: Context -> Env -> TT Name -> TT Name -> TC ([(Name, TT Name)],

2626 Injs, Fails)

2727unify ctxt env topx topy

28− = case runStateT

29− (un' False [] (normalise ctxt env topx) (normalise ctxt env topy))

30− (UI 0 [] []) of

31− OK (v, UI _ inj fails) -> return (filter notTrivial v, inj, reverse fails)

32−-- OK (_, UI s _ ((_,_,f):fs)) -> tfail $ CantUnify topx topy f s

33− Error e -> tfail e

28+ = -- case runStateT (un' False [] topx topy) (UI 0 [] []) of

29+ -- OK (v, UI _ inj []) -> return (filter notTrivial v, inj, [])

30+ let topxn = normalise ctxt env topx

31+ topyn = normalise ctxt env topy in

32+ case runStateT (un' False [] topxn topyn)

33+ (UI 0 [] []) of

34+ OK (v, UI _ inj fails) -> return (filter notTrivial v, inj, reverse fails)

35+-- OK (_, UI s _ ((_,_,f):fs)) -> tfail $ CantUnify topx topy f s

36+ Error e -> tfail e

3437 where

3538 notTrivial (x, P _ x' _) = x /= x'

3639 notTrivial _ = True

@@ -76,18 +79,19 @@ unify ctxt env topx topy

7679 un' fn bnames (App fx ax) (App fy ay)

7780 = do uplus -- do the second one if the first adds any errors

7881 (do hf <- un' True bnames fx fy

79− let ax' = normalise ctxt env (substNames hf ax)

80− let ay' = normalise ctxt env (substNames hf ay)

82+ let ax' = hnormalise hf ctxt env (substNames hf ax)

83+ let ay' = hnormalise hf ctxt env (substNames hf ay)

8184 ha <- un' False bnames ax' ay'

8285 sc 1

8386 combine bnames hf ha)

8487 (do ha <- un' False bnames ax ay

85− let fx' = normalise ctxt env (substNames ha fx)

86− let fy' = normalise ctxt env (substNames ha fy)

88+ let fx' = hnormalise ha ctxt env (substNames ha fx)

89+ let fy' = hnormalise ha ctxt env (substNames ha fy)

8790 hf <- un' False bnames fx' fy'

8891 sc 1

8992 combine bnames hf ha)

90−

93+ where hnormalise [] _ _ t = t

94+ hnormalise ns ctxt env t = normalise ctxt env t

9195 un' fn bnames x (Bind n (Lam t) (App y (P Bound n' _)))

9296 | n == n' = un' False bnames x y

9397 un' fn bnames (Bind n (Lam t) (App x (P Bound n' _))) y

src/Idris/Delaborate.hs+4

@@ -10,6 +10,8 @@ import Core.TT

1010

1111import Debug.Trace

1212

13+bugaddr = "https://github.com/edwinb/Idris-dev/issues"

14+

1315delab :: IState -> Term -> PTerm

1416delab i tm = delab' i tm False

1517

@@ -70,6 +72,8 @@ delab' ist tm fullname = de [] tm

7072

7173pshow :: IState -> Err -> String

7274pshow i (Msg s) = s

75+pshow i (InternalMsg s) = "INTERNAL ERROR: " ++ show s ++

76+ "\nThis is probably a bug. Please consider reporting at " ++ bugaddr

7377pshow i (CantUnify x y e sc s)

7478 = "Can't unify " ++ show (delab i x)

7579 ++ " with " ++ show (delab i y) ++

src/Idris/ElabTerm.hs+6−2

@@ -42,7 +42,9 @@ build ist info pattern fn tm

4242 is <- getAux

4343 tt <- get_term

4444 let (tm, ds) = runState (collectDeferred tt) []

45− return (tm, ds, is)

45+ log <- getLog

46+ if (log /= "") then trace log $ return (tm, ds, is)

47+ else return (tm, ds, is)

4648

4749-- Build a term autogenerated as a typeclass method definition

4850-- (Separate, so we don't go overboard resolving things that we don't

@@ -55,7 +57,9 @@ buildTC ist info pattern tcgen fn tm

5557 is <- getAux

5658 tt <- get_term

5759 let (tm, ds) = runState (collectDeferred tt) []

58− return (tm, ds, is)

60+ log <- getLog

61+ if (log /= "") then trace log $ return (tm, ds, is)

62+ else return (tm, ds, is)

5963

6064-- Returns the set of declarations we need to add to complete the definition

6165-- (most likely case blocks to elaborate)