21c3a30 · Idris-dev · git.iko.soy

src/Core/Elaborate.hs+5−1

@@ -427,7 +427,11 @@ tryAll xs = tryAll' [] (cantResolve, 0) (map fst xs)

427427 OK (v, s') -> tryAll' ((do put s'

428428 return v):cs) f xs

429429 Error err -> do put s

430− tryAll' cs (better err f) xs

430+ if (score err) < 100

431+ then

432+ tryAll' cs (better err f) xs

433+ else

434+ tryAll' [] (better err f) xs -- give up

431435

432436 better err (f, i) = let s = score err in

433437 if (s >= i) then (lift (tfail err), s)

src/Core/TT.hs+2

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

3939

4040data Err = Msg String

4141 | CantUnify Term Term Err Int -- Int is 'score' - how much we did unify

42+ | NoSuchVariable Name

4243 | NotInjective Term Term Term

4344 | CantResolve Term

4445 | IncompleteTerm Term

@@ -50,6 +51,7 @@ data Err = Msg String

5051score :: Err -> Int

5152score (CantUnify _ _ m s) = s + score m

5253score (CantResolve _) = 20

54+score (NoSuchVariable _) = 1000

5355score _ = 0

5456

5557instance Show Err where

src/Core/Typecheck.hs+1−1

@@ -53,7 +53,7 @@ check' holes ctxt env top = chk env top where

5353 chk env (Var n)

5454 | Just (i, ty) <- lookupTyEnv n env = return (P Bound n ty, ty)

5555 | (P nt n' ty : _) <- lookupP Nothing n ctxt = return (P nt n' ty, ty)

56− | otherwise = do fail $ "No such variable " ++ show n ++ " in " ++ show (map fst env)

56+ | otherwise = do lift $ tfail $ NoSuchVariable n

5757 chk env (RApp f a)

5858 = do (fv, fty) <- chk env f

5959 (av, aty) <- chk env a

src/Idris/AbsSyntax.hs+19−15

@@ -484,7 +484,7 @@ data PTerm = PQuote Raw

484484 | PMetavar Name

485485 | PProof [PTactic]

486486 | PTactics [PTactic] -- as PProof, but no auto solving

487− | PElabError String -- error to report on elaboration

487+ | PElabError Err -- error to report on elaboration

488488 | PImpossible -- special case for declaring when an LHS can't typecheck

489489 deriving Eq

490490{-!

@@ -777,7 +777,7 @@ showImp impl tm = se 10 tm where

777777 se p PImpossible = "impossible"

778778 se p Placeholder = "_"

779779 se p (PDoBlock _) = "do block show not implemented"

780− se p (PElabError s) = s

780+ se p (PElabError s) = show s

781781-- se p x = "Not implemented"

782782

783783 sArg (PImp _ _ n tm) = siArg (n, tm)

@@ -1141,9 +1141,9 @@ addImpl' :: Bool -> [Name] -> IState -> PTerm -> PTerm

11411141addImpl' inpat env ist ptm = ai env ptm

11421142 where

11431143 ai env (PRef fc f)

1144− | not (f `elem` env) = aiFn inpat ist fc f []

1144+ | not (f `elem` env) = handleErr $ aiFn inpat ist fc f []

11451145 ai env (PHidden (PRef fc f))

1146− | not (f `elem` env) = aiFn False ist fc f []

1146+ | not (f `elem` env) = handleErr $ aiFn False ist fc f []

11471147 ai env (PEq fc l r) = let l' = ai env l

11481148 r' = ai env r in

11491149 PEq fc l' r'

@@ -1162,7 +1162,7 @@ addImpl' inpat env ist ptm = ai env ptm

11621162 ai env (PApp fc (PRef _ f) as)

11631163 | not (f `elem` env)

11641164 = let as' = map (fmap (ai env)) as in

1165− aiFn False ist fc f as'

1165+ handleErr $ aiFn False ist fc f as'

11661166 ai env (PApp fc f as) = let f' = ai env f

11671167 as' = map (fmap (ai env)) as in

11681168 mkPApp fc 1 f' as'

@@ -1185,30 +1185,34 @@ addImpl' inpat env ist ptm = ai env ptm

11851185 ai env (PTactics ts) = PTactics (map (fmap (ai env)) ts)

11861186 ai env tm = tm

11871187

1188+ handleErr (Left err) = PElabError err

1189+ handleErr (Right x) = x

1190+

11881191-- if in a pattern, and there are no arguments, and there's no possible

11891192-- names with zero explicit arguments, don't add implicits.

11901193

1191−aiFn :: Bool -> IState -> FC -> Name -> [PArg] -> PTerm

1194+aiFn :: Bool -> IState -> FC -> Name -> [PArg] -> Either Err PTerm

11921195aiFn True ist fc f []

11931196 = case lookupCtxt Nothing f (idris_implicits ist) of

1194− [] -> PRef fc f

1197+ [] -> Right $ PRef fc f

11951198 alts -> if (any (all imp) alts)

11961199 then aiFn False ist fc f [] -- use it as a constructor

1197− else PRef fc f

1200+ else Right $ PRef fc f

11981201 where imp (PExp _ _ _) = False

11991202 imp _ = True

12001203aiFn inpat ist fc f as

1201− | f `elem` primNames = PApp fc (PRef fc f) as

1204+ | f `elem` primNames = Right $ PApp fc (PRef fc f) as

12021205aiFn inpat ist fc f as

12031206 -- This is where namespaces get resolved by adding PAlternative

12041207 = case lookupCtxtName Nothing f (idris_implicits ist) of

1205− [(f',ns)] -> mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)

1208+ [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)

12061209 [] -> if f `elem` idris_metavars ist

1207− then PApp fc (PRef fc f) as

1208− else mkPApp fc (length as) (PRef fc f) as

1209− alts -> PAlternative $

1210− map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')

1211− (insertImpl ns as)) alts

1210+ then Right $ PApp fc (PRef fc f) as

1211+ else Right $ mkPApp fc (length as) (PRef fc f) as

1212+ alts -> Right $

1213+ PAlternative $

1214+ map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')

1215+ (insertImpl ns as)) alts

12121216 where

12131217 insertImpl :: [PArg] -> [PArg] -> [PArg]

12141218 insertImpl (PExp p l ty : ps) (PExp _ _ tm : given) =

src/Idris/DSL.hs+5−5

@@ -38,7 +38,7 @@ expandDo dsl (PReturn fc) = dsl_return dsl

3838expandDo dsl (PDoBlock ds) = expandDo dsl $ block (dsl_bind dsl) ds

3939 where

4040 block b [DoExp fc tm] = tm

41− block b [a] = PElabError "Last statement in do block must be an expression"

41+ block b [a] = PElabError (Msg "Last statement in do block must be an expression")

4242 block b (DoBind fc n tm : rest)

4343 = PApp fc b [pexp tm, pexp (PLam n Placeholder (block b rest))]

4444 block b (DoBindP fc p tm : rest)

@@ -53,7 +53,7 @@ expandDo dsl (PDoBlock ds) = expandDo dsl $ block (dsl_bind dsl) ds

5353 = PApp fc b

5454 [pexp tm,

5555 pexp (PLam (MN 0 "bindx") Placeholder (block b rest))]

56− block b _ = PElabError "Invalid statement in do block"

56+ block b _ = PElabError (Msg "Invalid statement in do block")

5757

5858expandDo dsl (PIdiom fc e) = expandDo dsl $ unIdiom (dsl_apply dsl) (dsl_pure dsl) fc e

5959expandDo dsl t = t

@@ -62,7 +62,7 @@ var :: DSL -> Name -> PTerm -> Int -> PTerm

6262var dsl n t i = v' i t where

6363 v' i (PRef fc x) | x == n =

6464 case dsl_var dsl of

65− Nothing -> PElabError "No 'variable' defined in dsl"

65+ Nothing -> PElabError (Msg "No 'variable' defined in dsl")

6666 Just v -> PApp fc v [pexp (mkVar fc i)]

6767 v' i (PLam n ty sc)

6868 | Nothing <- dsl_lambda dsl

@@ -85,10 +85,10 @@ var dsl n t i = v' i t where

8585 v' i t = t

8686

8787 mkVar fc 0 = case index_first dsl of

88− Nothing -> PElabError "No index_first defined"

88+ Nothing -> PElabError (Msg "No index_first defined")

8989 Just f -> f

9090 mkVar fc n = case index_next dsl of

91− Nothing -> PElabError "No index_next defined"

91+ Nothing -> PElabError (Msg "No index_next defined")

9292 Just f -> PApp fc f [pexp (mkVar fc (n-1))]

9393

9494unIdiom :: PTerm -> PTerm -> FC -> PTerm -> PTerm

src/Idris/Delaborate.hs+1

@@ -75,6 +75,7 @@ pshow i (NotInjective p x y) = "Can't verify injectivity of " ++ show (delab i p

7575 " when unifying " ++ show (delab i x) ++ " and " ++

7676 show (delab i y)

7777pshow i (CantResolve c) = "Can't resolve type class " ++ show (delab i c)

78+pshow i (NoSuchVariable n) = "No such variable " ++ show n

7879pshow i (IncompleteTerm t) = "Incomplete term " ++ show t

7980pshow i UniverseError = "Universe inconsistency"

8081pshow i ProgramLineComment = "Program line next to comment"

src/Idris/ElabDecls.hs+1−1

@@ -391,7 +391,7 @@ elabClause info fc tcgen (PWith fname lhs_in withs wval_in withblock)

391391 (clhs, clhsty) <- recheckC ctxt fc [] lhs_tm

392392 logLvl 5 ("Checked " ++ show clhs)

393393 let bargs = getPBtys lhs_tm

394− let wval = addImpl i wval_in

394+ let wval = addImplBound i (map fst bargs) wval_in

395395 logLvl 5 ("Checking " ++ showImp True wval)

396396 -- Elaborate wval in this context

397397 ((wval', defer, is), _) <-

src/Idris/ElabTerm.hs+14−16

@@ -4,6 +4,7 @@ module Idris.ElabTerm where

44

55import Idris.AbsSyntax

66import Idris.DSL

7+import Idris.Delaborate

78

89import Core.Elaborate hiding (Tactic(..))

910import Core.TT

@@ -233,12 +234,6 @@ elab ist info pattern tcgen fn tm

233234 when (not pattern || (ina && not tcgen)) $

234235 mapM_ (\n -> do focus n

235236 resolveTC 7 fn ist) (ivs' \\ ivs)

236−-- ivs <- get_instances

237−-- when (not (null ivs)) $

238−-- do t <- get_term

239−-- trace (show ivs ++ "\n" ++ show t) $

240−-- mapM_ (\n -> do focus n

241−-- resolveTC ist) ivs

242237 where tcArg (n, PConstraint _ _ Placeholder) = True

243238 tcArg _ = False

244239

@@ -258,7 +253,7 @@ elab ist info pattern tcgen fn tm

258253 elab' ina (PTactics ts)

259254 | not pattern = do mapM_ (runTac False ist) ts

260255 | otherwise = elab' ina Placeholder

261− elab' ina (PElabError e) = fail e

256+ elab' ina (PElabError e) = fail (pshow ist e)

262257 elab' ina@(_, a) c@(PCase fc scr opts)

263258 = do attack

264259 tyn <- unique_hole (MN 0 "scty")

@@ -344,15 +339,17 @@ trivial ist = try (do elab ist toplevel False False (MN 0 "tac") (PRefl (FC "prf

344339

345340resolveTC :: Int -> Name -> IState -> ElabD ()

346341resolveTC 0 fn ist = fail $ "Can't resolve type class"

342+resolveTC 1 fn ist = try (trivial ist) (resolveTC 0 fn ist)

347343resolveTC depth fn ist

348344 = try (trivial ist)

349345 (do t <- goal

350346 let (tc, ttypes) = unApply t

351− needsDefault t tc ttypes

347+ scopeOnly <- needsDefault t tc ttypes

352348 tm <- get_term

353349-- traceWhen (depth > 6) ("GOAL: " ++ show t ++ "\nTERM: " ++ show tm) $

354350-- (tryAll (map elabTC (map fst (ctxtAlist (tt_ctxt ist)))))

355− blunderbuss t (map fst (ctxtAlist (tt_ctxt ist))))

351+ let depth' = if scopeOnly then 2 else depth

352+ blunderbuss t depth' (map fst (ctxtAlist (tt_ctxt ist))))

356353 where

357354 elabTC n | n /= fn && tcname n = (resolve n depth, show n)

358355 | otherwise = (fail "Can't resolve", show n)

@@ -361,17 +358,18 @@ resolveTC depth fn ist

361358 = do focus a

362359 fill (RConstant IType) -- default Int

363360 solve

364−-- needsDefault t f as

365−-- | all boundVar as = fail $ "Can't resolve " ++ show t

366− needsDefault t f a = return ()

361+ return False

362+ needsDefault t f as

363+ | all boundVar as = return True -- fail $ "Can't resolve " ++ show t

364+ needsDefault t f a = return False -- trace (show t) $ return ()

367365

368366 boundVar (P Bound _ _) = True

369367 boundVar _ = False

370368

371− blunderbuss t [] = lift $ tfail $ CantResolve t

372− blunderbuss t (n:ns) | n /= fn && tcname n = try (resolve n depth)

373− (blunderbuss t ns)

374− | otherwise = blunderbuss t ns

369+ blunderbuss t d [] = lift $ tfail $ CantResolve t

370+ blunderbuss t d (n:ns) | n /= fn && tcname n = try (resolve n d)

371+ (blunderbuss t d ns)

372+ | otherwise = blunderbuss t d ns

375373

376374 resolve n depth

377375 | depth == 0 = fail $ "Can't resolve type class"

src/Idris/IBC.hs+4−4

@@ -836,8 +836,8 @@ instance Binary PTerm where

836836 put x1

837837 PTactics x1 -> do putWord8 22

838838 put x1

839− PElabError x1 -> do putWord8 23

840− put x1

839+-- PElabError x1 -> do putWord8 23

840+-- put x1

841841 PImpossible -> putWord8 24

842842 get

843843 = do i <- getWord8

@@ -904,8 +904,8 @@ instance Binary PTerm where

904904 return (PProof x1)

905905 22 -> do x1 <- get

906906 return (PTactics x1)

907− 23 -> do x1 <- get

908− return (PElabError x1)

907+-- 23 -> do x1 <- get

908+-- return (PElabError x1)

909909 24 -> return PImpossible

910910 _ -> error "Corrupted binary data for PTerm"

911911