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

git.iko.soy/Idris-dev

A bit more unification error provenance

commit01c4f2a39c9a9bb391d70e98713d6de16548a67b authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 16 Mar 2015, 19:36 (12 years ago) parent75f6c2d

6 files changed+22−5

compare with master

unifiedsplit

src/Idris/Core/Binary.hs+4 src/Idris/Core/DeepSeq.hs+2 src/Idris/Core/ProofState.hs+11−4 src/Idris/Core/TT.hs+2 src/Idris/Delaborate.hs+2 test/tutorial006/expected+1−1

src/Idris/Core/Binary.hs+4

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

2727 put ExpectedType = putWord8 0

2828 put (SourceTerm t) = do putWord8 1

2929 put t

30+ put InferredVal = putWord8 2

31+ put GivenVal = putWord8 3

3032

3133 get = do i <- getWord8

3234 case i of

3335 0 -> return ExpectedType

3436 1 -> do x1 <- get

3537 return (SourceTerm x1)

38+ 2 -> return InferredVal

39+ 3 -> return GivenVal

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

3741

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

src/Idris/Core/DeepSeq.hs+2

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

4545

4646instance NFData Provenance where

4747 rnf ExpectedType = ()

48+ rnf InferredVal = ()

49+ rnf GivenVal = ()

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

4951

5052instance NFData Err where

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

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

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

494494-- let valtyn = normalise ctxt env valty

495495-- 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)

497498 ps <- get

498499 let (uh, uns) = unified ps

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

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

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

512513 do let guess = forget val

513514 (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)

515517 ps <- get

516518 let (uh, uns) = unified ps

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

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

529531 dropdots <-

530532 case lookup x (notunified ps) of

531533 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)

533536 return [x]

534537 _ -> return []

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

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

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

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

824827

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

829+updateProv ns p = p

830+

825831updateError [] err = err

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

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

828834updateError ns (ElaboratingArg f a env e)

829835 = ElaboratingArg f a env (updateError ns e)

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

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

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

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

832839updateError ns e = e

833840

834841solveInProblems x val [] = []

src/Idris/Core/TT.hs+2

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

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

122122

123123data Provenance = ExpectedType

124+ | InferredVal

125+ | GivenVal

124126 | SourceTerm Term

125127 deriving (Show, Eq, Data, Typeable)

126128{-!

src/Idris/Delaborate.hs+2

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

196196

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

198198pprintProv i e ExpectedType = text "Expected type"

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

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

199201pprintProv i e (SourceTerm tm)

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

201203

test/tutorial006/expected+1−1

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

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

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

33 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)

55 with

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