01c4f2a · Idris-dev · git.iko.soy

src/Idris/Core/Binary.hs+4

compare with master

unifiedsplit

@@ -27,12 +27,16 @@ instance Binary Provenance where

27 put ExpectedType = putWord8 0

28 put (SourceTerm t) = do putWord8 1

29 put t

30+ put InferredVal = putWord8 2

31+ put GivenVal = putWord8 3

30

32

31 get = do i <- getWord8

33 get = do i <- getWord8

32 case i of

34 case i of

33 0 -> return ExpectedType

35 0 -> return ExpectedType

34 1 -> do x1 <- get

36 1 -> do x1 <- get

35 return (SourceTerm x1)

37 return (SourceTerm x1)

38+ 2 -> return InferredVal

39+ 3 -> return GivenVal

36 _ -> error "Corrupted binary data for Provenance"

40 _ -> error "Corrupted binary data for Provenance"

37

41

38instance Binary a => Binary (Err' a) where

42instance Binary a => Binary (Err' a) where

src/Idris/Core/DeepSeq.hs+2

@@ -45,6 +45,8 @@ instance NFData FC where

45

46instance NFData Provenance where

47 rnf ExpectedType = ()

48+ rnf InferredVal = ()

49+ rnf GivenVal = ()

48 rnf (SourceTerm x1) = rnf x1 `seq` ()

50 rnf (SourceTerm x1) = rnf x1 `seq` ()

49

51

50instance NFData Err where

52instance NFData Err where

src/Idris/Core/ProofState.hs+11−4

@@ -493,7 +493,8 @@ match_fill guess ctxt env (Bind x (Hole ty) sc) =

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

494-- let valtyn = normalise ctxt env valty

495-- let tyn = normalise ctxt env ty

496− ns <- match_unify' ctxt env (valty, Nothing) (ty, Nothing)

496+ ns <- match_unify' ctxt env (valty, Just $ SourceTerm val)

497+ (ty, Just ExpectedType)

497 ps <- get

498 ps <- get

498 let (uh, uns) = unified ps

499 let (uh, uns) = unified ps

499-- put (ps { unified = (uh, uns ++ ns) })

500-- put (ps { unified = (uh, uns ++ ns) })

@@ -511,7 +512,8 @@ complete_fill :: RunTactic

511complete_fill ctxt env (Bind x (Guess ty val) sc) =

512complete_fill ctxt env (Bind x (Guess ty val) sc) =

512 do let guess = forget val

513 do let guess = forget val

513 (val', valty) <- lift $ check ctxt env guess

514 (val', valty) <- lift $ check ctxt env guess

514− ns <- unify' ctxt env (valty, Nothing) (ty, Nothing)

515+ ns <- unify' ctxt env (valty, Just $ SourceTerm val')

516+ (ty, Just ExpectedType)

515 ps <- get

517 ps <- get

516 let (uh, uns) = unified ps

518 let (uh, uns) = unified ps

517-- put (ps { unified = (uh, uns ++ ns) })

519-- put (ps { unified = (uh, uns ++ ns) })

@@ -529,7 +531,8 @@ solve ctxt env (Bind x (Guess ty val) sc)

529 dropdots <-

531 dropdots <-

530 case lookup x (notunified ps) of

532 case lookup x (notunified ps) of

531 Just tm -> -- trace ("NEED MATCH: " ++ show (x, tm, val) ++ "\nIN " ++ show (pterm ps)) $

533 Just tm -> -- trace ("NEED MATCH: " ++ show (x, tm, val) ++ "\nIN " ++ show (pterm ps)) $

532− do match_unify' ctxt env (tm, Nothing) (val, Nothing)

534+ do match_unify' ctxt env (tm, Just InferredVal)

535+ (val, Just GivenVal)

533 return [x]

536 return [x]

534 _ -> return []

537 _ -> return []

535 action (\ps -> ps { holes = traceWhen (unifylog ps) ("Dropping hole " ++ show x) $

538 action (\ps -> ps { holes = traceWhen (unifylog ps) ("Dropping hole " ++ show x) $

@@ -822,13 +825,17 @@ updateEnv ns [] = []

822updateEnv ns ((n, b) : env)

825updateEnv ns ((n, b) : env)

823 = (n, fmap (updateSolvedTerm ns) b) : updateEnv ns env

826 = (n, fmap (updateSolvedTerm ns) b) : updateEnv ns env

824

827

828+updateProv ns (SourceTerm t) = SourceTerm $ updateSolvedTerm ns t

829+updateProv ns p = p

830+

825updateError [] err = err

831updateError [] err = err

826updateError ns (At f e) = At f (updateError ns e)

832updateError ns (At f e) = At f (updateError ns e)

827updateError ns (Elaborating s n e) = Elaborating s n (updateError ns e)

833updateError ns (Elaborating s n e) = Elaborating s n (updateError ns e)

828updateError ns (ElaboratingArg f a env e)

834updateError ns (ElaboratingArg f a env e)

829 = ElaboratingArg f a env (updateError ns e)

835 = ElaboratingArg f a env (updateError ns e)

830updateError ns (CantUnify b (l,lp) (r,rp) e xs sc)

836updateError ns (CantUnify b (l,lp) (r,rp) e xs sc)

837+ = CantUnify b (updateSolvedTerm ns l, fmap (updateProv ns) lp)

831− = CantUnify b (updateSolvedTerm ns l, lp) (updateSolvedTerm ns r, rp) (updateError ns e) xs sc

838+ (updateSolvedTerm ns r, fmap (updateProv ns) rp) (updateError ns e) xs sc

832updateError ns e = e

839updateError ns e = e

833

840

834solveInProblems x val [] = []

841solveInProblems x val [] = []

src/Idris/Core/TT.hs+2

@@ -121,6 +121,8 @@ data ErrorReportPart = TextPart String

121-- Language.Reflection.Errors.Err in the stdlib!

122

123data Provenance = ExpectedType

124+ | InferredVal

125+ | GivenVal

124 | SourceTerm Term

126 | SourceTerm Term

125 deriving (Show, Eq, Data, Typeable)

127 deriving (Show, Eq, Data, Typeable)

126{-!

128{-!

src/Idris/Delaborate.hs+2

@@ -196,6 +196,8 @@ pprintTerm' ist bnd tm = pprintPTerm (ppOptionIst ist) bnd [] (idris_infixes ist

196

197pprintProv :: IState -> [(Name, Term)] -> Provenance -> Doc OutputAnnotation

198pprintProv i e ExpectedType = text "Expected type"

199+pprintProv i e InferredVal = text "Inferred value"

200+pprintProv i e GivenVal = text "Given value"

199pprintProv i e (SourceTerm tm)

201pprintProv i e (SourceTerm tm)

200 = text "Type of " <> pprintTerm' i (zip (map fst e) (repeat False)) (delab i tm)

202 = text "Type of " <> pprintTerm' i (zip (map fst e) (repeat False)) (delab i tm)

201

203

test/tutorial006/expected+1−1

@@ -1,7 +1,7 @@

1tutorial006a.idr:5:23:When elaborating right hand side of vapp:

2When elaborating argument [95mxs[0m to constructor [91mData.VectType.Vect.::[0m:

3 Can't unify

4− [94mVect[0m ([95mn[0m [92m+[0m [95mn[0m) [95ma[0m (Type of vapp _ _)

4+ [94mVect[0m ([95mn[0m [92m+[0m [95mn[0m) [95ma[0m (Type of vapp [95mxs[0m [95mxs[0m)

5 with

6 [94mVect[0m ([92mplus[0m [95mn[0m [95mm[0m) [95ma[0m (Expected type)

7