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

src/Core/Elaborate.hs+10

compare with master

unifiedsplit

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

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

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

171

172+getLog :: Elab' aux String

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

174+ return logs

175+

172-- The primitives, from ProofState

176-- The primitives, from ProofState

173

177

174attack :: Elab' aux ()

178attack :: Elab' aux ()

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

402 (do focus f; fun

406 (do focus f; fun

403 focus s; arg)

407 focus s; arg)

404 complete_fill

408 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

405 end_unify

415 end_unify

406

416

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

417-- 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' =

294

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

296

297−-- Hmmm. YAGNI?

298regret :: RunTactic

297regret :: 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"

300

303

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

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

302addInj inj = do ps <- get

305addInj inj = do ps <- get

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

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

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

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

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

317 s <- get

320 s <- get

321+-- let valtyn = normalise ctxt env valty

322+-- let tyn = normalise ctxt env ty

318 ns <- unify' ctxt env valty ty

323 ns <- unify' ctxt env valty ty

319 ps <- get

324 ps <- get

320 let (uh, uns) = unified ps

325 let (uh, uns) = unified ps

src/Core/TT.hs+4−1

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

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

44

45data Err = Msg String

46+ | InternalMsg String

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

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

47 | NoSuchVariable Name

48 | NoSuchVariable Name

48 | NotInjective Term Term Term

49 | NotInjective Term Term Term

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

56

57

57instance Sized Err where

58instance Sized Err where

58 size (Msg msg) = length msg

59 size (Msg msg) = length msg

60+ size (InternalMsg msg) = length msg

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

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

60 size (NoSuchVariable name) = size name

62 size (NoSuchVariable name) = size name

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

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

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

74

76

75instance Show Err where

77instance Show Err where

76 show (Msg s) = s

78 show (Msg s) = s

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

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

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

78 ++ show e ++ " in " ++ show sc ++ " " ++ show i

81 ++ show e ++ " in " ++ show sc ++ " " ++ show i

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

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

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

115 x >>= k = case x of

118 x >>= k = case x of

116 OK v -> k v

119 OK v -> k v

117 Error e -> Error e

120 Error e -> Error e

118− fail e = Error (Msg e)

121+ fail e = Error (InternalMsg e)

119

122

120tfail :: Err -> TC a

123tfail :: Err -> TC a

121tfail e = Error e

124tfail e = Error e

src/Core/Unify.hs+15−11

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

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

26 Injs, Fails)

27unify ctxt env topx topy

28− = case runStateT

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

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

31+ topyn = normalise ctxt env topy in

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

30− (UI 0 [] []) of

33+ (UI 0 [] []) of

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

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

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

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

33− Error e -> tfail e

36+ Error e -> tfail e

34 where

37 where

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

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

36 notTrivial _ = True

39 notTrivial _ = True

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

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

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

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

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

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

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

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

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

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

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

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

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

82 sc 1

85 sc 1

83 combine bnames hf ha)

86 combine bnames hf ha)

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

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

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

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

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

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

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

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

88 sc 1

91 sc 1

89 combine bnames hf ha)

92 combine bnames hf ha)

90−

93+ where hnormalise [] _ _ t = t

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

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

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

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

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

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

97 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

10

11import Debug.Trace

12

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

14+

13delab :: IState -> Term -> PTerm

15delab :: IState -> Term -> PTerm

14delab i tm = delab' i tm False

16delab i tm = delab' i tm False

15

17

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

70

72

71pshow :: IState -> Err -> String

73pshow :: IState -> Err -> String

72pshow i (Msg s) = s

74pshow i (Msg s) = s

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

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

73pshow i (CantUnify x y e sc s)

77pshow i (CantUnify x y e sc s)

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

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

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

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

src/Idris/ElabTerm.hs+6−2

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

42 is <- getAux

43 tt <- get_term

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

45+ log <- getLog

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

45− return (tm, ds, is)

47+ else return (tm, ds, is)

46

48

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

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

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

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

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

55 is <- getAux

57 is <- getAux

56 tt <- get_term

58 tt <- get_term

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

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

60+ log <- getLog

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

58− return (tm, ds, is)

62+ else return (tm, ds, is)

59

63

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

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

61-- (most likely case blocks to elaborate)

65-- (most likely case blocks to elaborate)