e363c09 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Better treatment of unbound implicits

e363c09Edwin Brady12 years ago

src/Idris/AbsSyntax.hs+97−21

compare with master

unifiedsplit

@@ -1078,6 +1078,16 @@ addStatics n tm ptm =

1078

1079-- Dealing with implicit arguments

1080

1081+-- Add some bound implicits to the using block if they aren't there already

1082+

1083+addToUsing :: [Using] -> [(Name, PTerm)] -> [Using]

1084+addToUsing us [] = us

1085+addToUsing us ((n, t) : ns)

1086+ | n `notElem` mapMaybe impName us = addToUsing (us ++ [UImplicit n t]) ns

1087+ | otherwise = addToUsing us ns

1088+ where impName (UImplicit n _) = Just n

1089+ impName _ = Nothing

1090+

1081-- Add constraint bindings from using block

1091-- Add constraint bindings from using block

1082

1092

1083addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm

1093addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm

@@ -1117,6 +1127,66 @@ addUsingConstraints syn fc t

1117 getName (PExp _ _ _ (PRef _ n)) = return n

1127 getName (PExp _ _ _ (PRef _ n)) = return n

1118 getName _ = []

1128 getName _ = []

1119

1129

1130+-- Add implicit bindings from using block, and bind any missing names

1131+addUsingImpls :: SyntaxInfo -> Name -> FC -> PTerm -> Idris PTerm

1132+addUsingImpls syn n fc t

1133+ = do ist <- getIState

1134+ let ns = implicitNamesIn (map iname uimpls) ist t

1135+ let badnames = filter (\n -> not (implicitable n) &&

1136+ n `notElem` (map iname uimpls)) ns

1137+ when (not (null badnames)) $

1138+ throwError (At fc (Elaborating "type of " n

1139+ (NoSuchVariable (head badnames))))

1140+ let cs = getArgnames t -- get already bound names

1141+ let addimpls = filter (\n -> iname n `notElem` cs) uimpls

1142+ -- if all names in the arguments of addconsts appear in ns,

1143+ -- add the constraint implicitly

1144+ return (bindFree ns (doAdd addimpls ns t))

1145+ where uimpls = filter uimpl (using syn)

1146+ uimpl (UImplicit _ _) = True

1147+ uimpl _ = False

1148+

1149+ iname (UImplicit n _) = n

1150+ iname (UConstraint _ _) = error "Can't happen addUsingImpls"

1151+

1152+ doAdd [] _ t = t

1153+ -- if all of args in ns, then add it

1154+ doAdd (UImplicit n ty : cs) ns t

1155+ | elem n ns

1156+ = PPi (Imp [] Dynamic False) n ty (doAdd cs ns t)

1157+ | otherwise = doAdd cs ns t

1158+

1159+ -- bind the free names which weren't in the using block

1160+ bindFree [] tm = tm

1161+ bindFree (n:ns) tm

1162+ | elem n (map iname uimpls) = bindFree ns tm

1163+ | otherwise

1164+ = PPi (Imp [] Dynamic False) n Placeholder (bindFree ns tm)

1165+

1166+ getArgnames (PPi _ n c sc)

1167+ = n : getArgnames sc

1168+ getArgnames _ = []

1169+

1170+-- Given the original type and the elaborated type, return the implicitness

1171+-- status of each pi-bound argument, and whether it's inaccessible (True) or not.

1172+

1173+getUnboundImplicits :: IState -> Type -> PTerm -> [(Bool, PArg)]

1174+getUnboundImplicits i (Bind n (Pi t) sc) (PPi p n' t' sc')

1175+ | n == n' = argInfo n p : getUnboundImplicits i sc sc'

1176+ where

1177+ argInfo n (Imp opt _ _) = (True, PImp (getPriority i t') True opt n t')

1178+ argInfo n (Exp opt _ _) = (InaccessibleArg `elem` opt,

1179+ PExp (getPriority i t') opt n t')

1180+ argInfo n (Constraint opt _) = (InaccessibleArg `elem` opt,

1181+ PConstraint 10 opt n t')

1182+ argInfo n (TacImp opt _ scr) = (InaccessibleArg `elem` opt,

1183+ PTacImplicit 10 opt n scr t')

1184+getUnboundImplicits i (Bind n (Pi t) sc) tm

1185+ = impBind n t : getUnboundImplicits i sc tm

1186+ where

1187+ impBind n t = (True, PImp 1 True [] n Placeholder)

1188+getUnboundImplicits i sc tm = []

1189+

1120-- Add implicit Pi bindings for any names in the term which appear in an

1190-- Add implicit Pi bindings for any names in the term which appear in an

1121-- argument position.

1191-- argument position.

1122

1192

@@ -1428,40 +1498,46 @@ aiFn inpat expat qq ist fc f ds as

1428 _ -> Public

1498 _ -> Public

1429

1499

1430 insertImpl :: [PArg] -> [PArg] -> [PArg]

1500 insertImpl :: [PArg] -> [PArg] -> [PArg]

1431− insertImpl ps as = insImpAcc M.empty ps as

1501+ insertImpl ps as = insImpAcc M.empty ps (filter exp as) (filter (not.exp) as)

1502+

1503+ exp (PExp _ _ _ _) = True

1504+ exp (PConstraint _ _ _ _) = True

1505+ exp _ = False

1432

1506

1433 insImpAcc :: M.Map Name PTerm -- accumulated param names & arg terms

1507 insImpAcc :: M.Map Name PTerm -- accumulated param names & arg terms

1434 -> [PArg] -- parameters

1508 -> [PArg] -- parameters

1435− -> [PArg] -- arguments

1509+ -> [PArg] -- explicit arguments

1510+ -> [PArg] -- implicits given

1436 -> [PArg]

1511 -> [PArg]

1437− insImpAcc pnas (PExp p l n ty : ps) (PExp _ _ _ tm : given) =

1512+ insImpAcc pnas (PExp p l n ty : ps) (PExp _ _ _ tm : given) imps =

1438− PExp p l n tm : insImpAcc (M.insert n tm pnas) ps given

1513+ PExp p l n tm : insImpAcc (M.insert n tm pnas) ps given imps

1439− insImpAcc pnas (PConstraint p l n ty : ps) (PConstraint _ _ _ tm : given) =

1514+ insImpAcc pnas (PConstraint p l n ty : ps) (PConstraint _ _ _ tm : given) imps =

1440− PConstraint p l n tm : insImpAcc (M.insert n tm pnas) ps given

1515+ PConstraint p l n tm : insImpAcc (M.insert n tm pnas) ps given imps

1441− insImpAcc pnas (PConstraint p l n ty : ps) given =

1516+ insImpAcc pnas (PConstraint p l n ty : ps) given imps =

1442 let rtc = PResolveTC fc in

1517 let rtc = PResolveTC fc in

1443− PConstraint p l n rtc : insImpAcc (M.insert n rtc pnas) ps given

1518+ PConstraint p l n rtc : insImpAcc (M.insert n rtc pnas) ps given imps

1444− insImpAcc pnas (PImp p _ l n ty : ps) given =

1519+ insImpAcc pnas (PImp p _ l n ty : ps) given imps =

1445− case find n given [] of

1520+ case find n imps [] of

1446− Just (tm, given') ->

1521+ Just (tm, imps') ->

1447− PImp p False l n tm : insImpAcc (M.insert n tm pnas) ps given'

1522+ PImp p False l n tm : insImpAcc (M.insert n tm pnas) ps given imps'

1448 Nothing ->

1523 Nothing ->

1449 PImp p True l n Placeholder :

1524 PImp p True l n Placeholder :

1450− insImpAcc (M.insert n Placeholder pnas) ps given

1525+ insImpAcc (M.insert n Placeholder pnas) ps given imps

1451− insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given =

1526+ insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given imps =

1452 let sc = addImpl ist (substMatches (M.toList pnas) sc') in

1527 let sc = addImpl ist (substMatches (M.toList pnas) sc') in

1453− case find n given [] of

1528+ case find n imps [] of

1454− Just (tm, given') ->

1529+ Just (tm, imps') ->

1455 PTacImplicit p l n sc tm :

1530 PTacImplicit p l n sc tm :

1456− insImpAcc (M.insert n tm pnas) ps given'

1531+ insImpAcc (M.insert n tm pnas) ps given imps'

1457 Nothing ->

1532 Nothing ->

1458 if inpat

1533 if inpat

1459 then PTacImplicit p l n sc Placeholder :

1534 then PTacImplicit p l n sc Placeholder :

1460− insImpAcc (M.insert n Placeholder pnas) ps given

1535+ insImpAcc (M.insert n Placeholder pnas) ps given imps

1461 else PTacImplicit p l n sc sc :

1536 else PTacImplicit p l n sc sc :

1462− insImpAcc (M.insert n sc pnas) ps given

1537+ insImpAcc (M.insert n sc pnas) ps given imps

1463− insImpAcc _ expected [] = []

1538+ insImpAcc _ expected [] imps = imps -- so that unused implicits give error

1539+ -- TODO: report here, and prune alternatives

1464− insImpAcc _ _ given = given

1540+ insImpAcc _ _ given imps = given ++ imps

1465

1541

1466 find n [] acc = Nothing

1542 find n [] acc = Nothing

1467 find n (PImp _ _ _ n' t : gs) acc

1543 find n (PImp _ _ _ n' t : gs) acc

src/Idris/AbsSyntaxTree.hs+36

@@ -1669,6 +1669,42 @@ boundNamesIn tm = nub $ ni tm

1669 niTacImp (TacImp _ _ scr) = ni scr

1670 niTacImp _ = []

1671

1672+-- Return names which are valid implicits in the given term (type).

1673+implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]

1674+implicitNamesIn uvars ist tm = nub $ ni [] tm

1675+ where

1676+ ni env (PRef _ n)

1677+ | not (n `elem` env)

1678+ = case lookupTy n (tt_ctxt ist) of

1679+ [] -> [n]

1680+ _ -> if n `elem` uvars then [n] else []

1681+ ni env (PApp _ f@(PRef _ n) as)

1682+ | n `elem` uvars = ni env f ++ concatMap (ni env) (map getTm as)

1683+ | otherwise = concatMap (ni env) (map getTm as)

1684+ ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

1685+ ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

1686+ ni env (PCase _ c os) = ni env c ++

1687+ -- names in 'os', not counting the names bound in the cases

1688+ (nub (concatMap (ni env) (map snd os))

1689+ \\ nub (concatMap (ni env) (map fst os)))

1690+ ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

1691+ ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc

1692+ ni env (PEq _ l r) = ni env l ++ ni env r

1693+ ni env (PRewrite _ l r _) = ni env l ++ ni env r

1694+ ni env (PTyped l r) = ni env l ++ ni env r

1695+ ni env (PPair _ _ l r) = ni env l ++ ni env r

1696+ ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r

1697+ ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r

1698+ ni env (PAlternative a as) = concatMap (ni env) as

1699+ ni env (PHidden tm) = ni env tm

1700+ ni env (PUnifyLog tm) = ni env tm

1701+ ni env (PDisamb _ tm) = ni env tm

1702+ ni env (PNoImplicits tm) = ni env tm

1703+ ni env _ = []

1704+

1705+ niTacImp env (TacImp _ _ scr) = ni env scr

1706+ niTacImp _ _ = []

1707+

1672-- Return names which are free in the given term.

1708-- Return names which are free in the given term.

1673namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]

1709namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]

1674namesIn uvars ist tm = nub $ ni [] tm

1710namesIn uvars ist tm = nub $ ni [] tm

src/Idris/CaseSplit.hs+2−2

@@ -55,7 +55,7 @@ split n t'

55 = do ist <- getIState

56 -- Make sure all the names in the term are accessible

57 mapM_ (\n -> setAccessibility n Public) (allNamesIn t')

58− (tm, ty, pats) <- elabValBind toplevel True True (addImplPat ist t')

58+ (tm, ty, pats) <- elabValBind toplevel ELHS True (addImplPat ist t')

59 -- ASSUMPTION: tm is in normal form after elabValBind, so we don't

60 -- need to do anything special to find out what family each argument

61 -- is in

@@ -201,7 +201,7 @@ tidy ist tm ty = return tm

201-- tidyVar t = t

202

203elabNewPat :: PTerm -> Idris (Maybe PTerm)

204−elabNewPat t = idrisCatch (do (tm, ty) <- elabVal toplevel True t

204+elabNewPat t = idrisCatch (do (tm, ty) <- elabVal toplevel ELHS t

205 i <- getIState

206 return (Just (delab i tm)))

207 (\e -> do i <- getIState

src/Idris/Core/Elaborate.hs+2−1

@@ -77,6 +77,7 @@ getNameFrom n = do (ES (p, a) s e) <- get

77 then MN (next+500) x

78 else MN (next+100) x

79 NS (UN x) s -> MN (next+100) x

80+ _ -> n

80 return $! n'

81 return $! n'

82setNextName :: Elab' aux ()

83setNextName :: Elab' aux ()

@@ -456,7 +457,7 @@ prepare_apply fn imps =

456 -> [(Name, Name)] -- ^ Accumulator for produced claims

457 -> [(Name, Name)] -- ^ Accumulator for produced claims

457 -> [Name] -- ^ Hypotheses

458 -> [Name] -- ^ Hypotheses

458 -> Elab' aux [(Name, Name)] -- ^ The names of the arguments and their holes, resp.

459 -> Elab' aux [(Name, Name)] -- ^ The names of the arguments and their holes, resp.

459− mkClaims (Bind n' (Pi t_in) sc) (i : is) claims hs =

460+ mkClaims (Bind n' (Pi t_in) sc) (i : is) claims hs =

460 do let t = rebind hs t_in

461 do let t = rebind hs t_in

461 n <- getNameFrom (mkMN n')

462 n <- getNameFrom (mkMN n')

462-- when (null claims) (start_unify n)

463-- when (null claims) (start_unify n)

src/Idris/Core/Evaluate.hs+6

@@ -549,6 +549,12 @@ convEq ctxt holes topx topy = ceq [] topx topy where

549 | n == n' = ceq ps x y

550 ceq ps (Bind n (Lam t) (App x (P Bound n' _))) y

551 | n == n' = ceq ps x y

552+

553+ ceq ps (Bind n (PVar t) sc) y = ceq ps sc y

554+ ceq ps x (Bind n (PVar t) sc) = ceq ps x sc

555+ ceq ps (Bind n (PVTy t) sc) y = ceq ps sc y

556+ ceq ps x (Bind n (PVTy t) sc) = ceq ps x sc

557+

552 ceq ps (V x) (V y) = return (x == y)

558 ceq ps (V x) (V y) = return (x == y)

553 ceq ps (V x) (P _ y _)

559 ceq ps (V x) (P _ y _)

554 | x >= 0 && length ps > x = return (fst (ps!!x) == y)

560 | x >= 0 && length ps > x = return (fst (ps!!x) == y)

src/Idris/Core/ProofState.hs+39−26

@@ -168,12 +168,16 @@ match_unify' ctxt env topx topy =

168 ++ "\n" ++ show (pterm ps) ++ "\n\n"

169 ) $

170 case match_unify ctxt env topx topy inj (holes ps) while of

171+ OK u -> traceWhen (unifylog ps)

172+ ("Matched " ++ show u) $

171− OK u -> do let (h, ns) = unified ps

173+ do let (h, ns) = unified ps

172− put (ps { unified = (h, u ++ ns) })

174+ put (ps { unified = (h, u ++ ns) })

173− return u

175+ return u

176+ Error e -> traceWhen (unifylog ps)

177+ ("No match " ++ show e) $

174− Error e -> do put (ps { problems = (topx, topy, env, e, while, Match) :

178+ do put (ps { problems = (topx, topy, env, e, while, Match) :

175− problems ps })

179+ problems ps })

176− return []

180+ return []

177-- traceWhen (unifylog ps)

181-- traceWhen (unifylog ps)

178-- ("Matched " ++ show (topx, topy) ++ " without " ++ show dont ++

182-- ("Matched " ++ show (topx, topy) ++ " without " ++ show dont ++

179-- "\nSolved: " ++ show u

183-- "\nSolved: " ++ show u

@@ -231,7 +235,8 @@ unify' ctxt env topx topy =

231 (holes ps)

235 (holes ps)

232 let (notu', probs_notu) = mergeNotunified env (notu ++ notunified ps)

236 let (notu', probs_notu) = mergeNotunified env (notu ++ notunified ps)

233 traceWhen (unifylog ps)

237 traceWhen (unifylog ps)

234− ("Now solved: " ++ show ns') $

238+ ("Now solved: " ++ show ns' ++

239+ "\nNow problems: " ++ qshow (probs' ++ probs_notu)) $

235 put (ps { problems = probs' ++ probs_notu,

240 put (ps { problems = probs' ++ probs_notu,

236 unified = (h, ns'),

241 unified = (h, ns'),

237 injective = updateInj u (injective ps),

242 injective = updateInj u (injective ps),

@@ -538,10 +543,11 @@ solve ctxt env (Bind x (Guess ty val) sc)

538 = do ps <- get

543 = do ps <- get

539 let (uh, uns) = unified ps

544 let (uh, uns) = unified ps

540 case lookup x (notunified ps) of

545 case lookup x (notunified ps) of

541− Just tm -> -- trace ("NEED MATCH: " ++ show (tm, val)) $

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

542 match_unify' ctxt env tm val

547 match_unify' ctxt env tm val

543 _ -> return []

548 _ -> return []

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

544− action (\ps -> ps { holes = holes ps \\ [x],

550+ holes ps \\ [x],

545 solved = Just (x, val),

551 solved = Just (x, val),

546 notunified = updateNotunified [(x,val)]

552 notunified = updateNotunified [(x,val)]

547 (notunified ps),

553 (notunified ps),

@@ -605,7 +611,9 @@ forall n ty ctxt env _ = fail "Can't pi bind here"

605

611

606patvar :: Name -> RunTactic

612patvar :: Name -> RunTactic

607patvar n ctxt env (Bind x (Hole t) sc) =

613patvar n ctxt env (Bind x (Hole t) sc) =

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

608− do action (\ps -> ps { holes = holes ps \\ [x],

615+ holes ps \\ [x],

616+ solved = Just (x, P Bound n t),

609 notunified = updateNotunified [(x,P Bound n t)]

617 notunified = updateNotunified [(x,P Bound n t)]

610 (notunified ps),

618 (notunified ps),

611 injective = addInj n x (injective ps) })

619 injective = addInj n x (injective ps) })

@@ -787,7 +795,8 @@ solve_unified ctxt env tm =

787 do ps <- get

795 do ps <- get

788 let (_, ns) = unified ps

796 let (_, ns) = unified ps

789 let unify = dropGiven (dontunify ps) ns (holes ps)

797 let unify = dropGiven (dontunify ps) ns (holes ps)

798+ action (\ps -> ps { holes = traceWhen (unifylog ps) ("Dropping holes " ++ show (map fst unify)) $

790− action (\ps -> ps { holes = holes ps \\ map fst unify })

799+ holes ps \\ map fst unify })

791 action (\ps -> ps { pterm = updateSolved unify (pterm ps) })

800 action (\ps -> ps { pterm = updateSolved unify (pterm ps) })

792 return (updateSolved unify tm)

801 return (updateSolved unify tm)

793

802

@@ -913,11 +922,12 @@ processTactic EndUnify ps

913 (ns'', probs') = updateProblems (context ps) ns' (problems ps)

922 (ns'', probs') = updateProblems (context ps) ns' (problems ps)

914 (injective ps) (holes ps)

923 (injective ps) (holes ps)

915 tm' = updateSolved ns'' (pterm ps) in

924 tm' = updateSolved ns'' (pterm ps) in

925+ traceWhen (unifylog ps) ("Dropping holes: " ++ show (map fst ns'')) $

916− return (ps { pterm = tm',

926+ return (ps { pterm = tm',

917− unified = (h, []),

927+ unified = (h, []),

918− problems = probs',

928+ problems = probs',

919− notunified = updateNotunified ns'' (notunified ps),

929+ notunified = updateNotunified ns'' (notunified ps),

920− holes = holes ps \\ map fst ns'' }, "")

930+ holes = holes ps \\ map fst ns'' }, "")

921processTactic UnifyAll ps

931processTactic UnifyAll ps

922 = let tm' = updateSolved (notunified ps) (pterm ps) in

932 = let tm' = updateSolved (notunified ps) (pterm ps) in

923 return (ps { pterm = tm',

933 return (ps { pterm = tm',

@@ -934,10 +944,11 @@ processTactic UnifyProblems ps

934 (injective ps)

944 (injective ps)

935 (holes ps)

945 (holes ps)

936 pterm' = updateSolved ns' (pterm ps) in

946 pterm' = updateSolved ns' (pterm ps) in

947+ traceWhen (unifylog ps) ("Dropping holes: " ++ show (map fst ns')) $

937− return (ps { pterm = pterm', solved = Nothing, problems = probs',

948+ return (ps { pterm = pterm', solved = Nothing, problems = probs',

938− previous = Just ps, plog = "",

949+ previous = Just ps, plog = "",

939− notunified = updateNotunified ns' (notunified ps),

950+ notunified = updateNotunified ns' (notunified ps),

940− holes = holes ps \\ (map fst ns') }, plog ps)

951+ holes = holes ps \\ (map fst ns') }, plog ps)

941processTactic (MatchProblems all) ps

952processTactic (MatchProblems all) ps

942 = let (ns', probs') = matchProblems all [] (context ps)

953 = let (ns', probs') = matchProblems all [] (context ps)

943 (problems ps)

954 (problems ps)

@@ -948,6 +959,7 @@ processTactic (MatchProblems all) ps

948 (injective ps)

959 (injective ps)

949 (holes ps)

960 (holes ps)

950 pterm' = updateSolved ns'' (pterm ps) in

961 pterm' = updateSolved ns'' (pterm ps) in

962+ traceWhen (unifylog ps) ("Dropping holes: " ++ show (map fst ns'')) $

951 return (ps { pterm = pterm', solved = Nothing, problems = probs'',

963 return (ps { pterm = pterm', solved = Nothing, problems = probs'',

952 previous = Just ps, plog = "",

964 previous = Just ps, plog = "",

953 notunified = updateNotunified ns'' (notunified ps),

965 notunified = updateNotunified ns'' (notunified ps),

@@ -968,12 +980,13 @@ processTactic t ps

968 -- rechecking problems may find more solutions, so

980 -- rechecking problems may find more solutions, so

969 -- apply them here

981 -- apply them here

970 let pterm'' = updateSolved ns' (pterm ps')

982 let pterm'' = updateSolved ns' (pterm ps')

983+ traceWhen (unifylog ps) ("Dropping holes: " ++ show (map fst ns')) $

971− return (ps' { pterm = pterm'',

984+ return (ps' { pterm = pterm'',

972− solved = Nothing,

985+ solved = Nothing,

973− problems = probs',

986+ problems = probs',

974− notunified = updateNotunified ns' (notunified ps'),

987+ notunified = updateNotunified ns' (notunified ps'),

975− previous = Just ps, plog = "",

988+ previous = Just ps, plog = "",

976− holes = holes ps' \\ (map fst ns')}, plog ps')

989+ holes = holes ps' \\ (map fst ns')}, plog ps')

977

990

978process :: Tactic -> Name -> StateT TState TC ()

991process :: Tactic -> Name -> StateT TState TC ()

979process EndUnify _

992process EndUnify _

src/Idris/Core/TT.hs+42−1

@@ -384,7 +384,7 @@ tcname _ = False

384implicitable (NS n _) = implicitable n

385implicitable (UN xs) | T.null xs = False

386 | otherwise = isLower (T.head xs)

387−implicitable (MN _ _) = True

387+implicitable (MN _ x) = not (tnull x) && thead x /= '_'

388implicitable _ = False

389

390nsroot (NS n _) = n

@@ -1264,8 +1264,11 @@ weakenTmEnv i = map (\ (n, b) -> (n, fmap (weakenTm i) b))

1264orderPats :: Term -> Term

1265orderPats tm = op [] tm

1266 where

1267+ op [] (App f a) = App f (op [] a) -- for Infer terms

1268+

1267 op ps (Bind n (PVar t) sc) = op ((n, PVar t) : ps) sc

1269 op ps (Bind n (PVar t) sc) = op ((n, PVar t) : ps) sc

1268 op ps (Bind n (Hole t) sc) = op ((n, Hole t) : ps) sc

1270 op ps (Bind n (Hole t) sc) = op ((n, Hole t) : ps) sc

1271+ op ps (Bind n (Pi t) sc) = op ((n, Pi t) : ps) sc

1269 op ps sc = bindAll (sortP ps) sc

1272 op ps sc = bindAll (sortP ps) sc

1270

1273

1271 sortP ps = pick [] (reverse ps)

1274 sortP ps = pick [] (reverse ps)

@@ -1288,6 +1291,44 @@ orderPats tm = op [] tm

1288 = (n', t') : insert n t ps

1291 = (n', t') : insert n t ps

1289 | otherwise = (n,t):(n',t'):ps

1292 | otherwise = (n,t):(n',t'):ps

1290

1293

1294+-- Make sure all the pattern bindings are as far out as possible

1295+liftPats :: Term -> Term

1296+liftPats tm = let (tm', ps) = runState (getPats tm) [] in

1297+ orderPats $ bindPats (reverse ps) tm'

1298+ where

1299+ bindPats [] tm = tm

1300+ bindPats ((n, t):ps) tm

1301+ | n `notElem` map fst ps = Bind n (PVar t) (bindPats ps tm)

1302+ | otherwise = bindPats ps tm

1303+

1304+ getPats :: Term -> State [(Name, Type)] Term

1305+ getPats (Bind n (PVar t) sc) = do ps <- get

1306+ put ((n, t) : ps)

1307+ getPats sc

1308+ getPats (Bind n (Guess t v) sc) = do t' <- getPats t

1309+ v' <- getPats v

1310+ sc' <- getPats sc

1311+ return (Bind n (Guess t' v') sc')

1312+ getPats (Bind n (Let t v) sc) = do t' <- getPats t

1313+ v' <- getPats v

1314+ sc' <- getPats sc

1315+ return (Bind n (Let t' v') sc')

1316+ getPats (Bind n (Pi t) sc) = do t' <- getPats t

1317+ sc' <- getPats sc

1318+ return (Bind n (Pi t') sc')

1319+ getPats (Bind n (Lam t) sc) = do t' <- getPats t

1320+ sc' <- getPats sc

1321+ return (Bind n (Lam t') sc')

1322+ getPats (Bind n (Hole t) sc) = do t' <- getPats t

1323+ sc' <- getPats sc

1324+ return (Bind n (Hole t') sc')

1325+

1326+

1327+ getPats (App f a) = do f' <- getPats f

1328+ a' <- getPats a

1329+ return (App f' a')

1330+ getPats t = return t

1331+

1291allTTNames :: Eq n => TT n -> [n]

1332allTTNames :: Eq n => TT n -> [n]

1292allTTNames = nub . allNamesIn

1333allTTNames = nub . allNamesIn

1293 where allNamesIn (P _ n _) = [n]

1334 where allNamesIn (P _ n _) = [n]

src/Idris/Core/Unify.hs+7−5

@@ -84,11 +84,11 @@ match_unify ctxt env topx topy inj holes from =

84 = let n' = uniqueName fn (map fst env) in

85 checkCycle names (f, Bind n' (Lam t) x)

87− un names (P _ x _) tm

87+ un names tx@(P _ x _) tm

88− | holeIn env x || x `elem` holes

88+ | tx /= tm && holeIn env x || x `elem` holes

89 = do sc 1; checkCycle names (x, tm)

90− un names tm (P _ y _)

90+ un names tm ty@(P _ y _)

91− | holeIn env y || y `elem` holes

91+ | ty /= tm && holeIn env y || y `elem` holes

92 = do sc 1; checkCycle names (y, tm)

93 un bnames (V i) (P _ x _)

94 | length bnames > i,

@@ -153,11 +153,13 @@ match_unify ctxt env topx topy inj holes from =

153 = case lookup n as of

154 Nothing -> combine bnames (as ++ [(n,t)]) bs

155 Just t' -> do ns <- un bnames t t'

156− -- make sure there's n mapping from n in ns

157 let ns' = filter (\ (x, _) -> x/=n) ns

156 let ns' = filter (\ (x, _) -> x/=n) ns

158 sc 1

157 sc 1

159 combine bnames as (ns' ++ bs)

158 combine bnames as (ns' ++ bs)

160

159

160+-- substN n tm (var, sol) = (var, subst n tm sol)

161+

162+ checkCycle ns p@(x, P _ x' _) | x == x' = return []

161 checkCycle ns p@(x, P _ _ _) = return [p]

163 checkCycle ns p@(x, P _ _ _) = return [p]

162 checkCycle ns (x, tm)

164 checkCycle ns (x, tm)

163 | not (x `elem` freeNames tm) = checkScope ns (x, tm)

165 | not (x `elem` freeNames tm) = checkScope ns (x, tm)

src/Idris/ElabDecls.hs+140−137

@@ -71,33 +71,28 @@ checkAddDef add toplvl fc ((n, (i, top, t)) : ns)

71-- mapM (\(n, (i, top, t)) -> do (t', _) <- recheckC fc [] t

72-- return (n, (i, top, t'))) ns

74−-- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".

75−elabType :: ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] ->

76− FC -> FnOpts -> Name -> PTerm -> Idris Type

74+buildType :: ElabInfo -> SyntaxInfo -> FC -> FnOpts -> Name -> PTerm ->

77−elabType = elabType' False

75+ Idris (Type, PTerm, [(Int, Name)])

78−

76+buildType info syn fc opts n ty' = do

79−elabType' :: Bool -> -- normalise it

80− ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] ->

81− FC -> FnOpts -> Name -> PTerm -> Idris Type

82−elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params info) ty_in

83− n = liftname info n_in in -}

84− do checkUndefined fc n

85 ctxt <- getContext

77 ctxt <- getContext

86 i <- getIState

78 i <- getIState

88− logLvl 5 $ show n ++ " pre-type " ++ showTmImpls ty'

80+ logLvl 3 $ show n ++ " pre-type " ++ showTmImpls ty'

89 ty' <- addUsingConstraints syn fc ty'

81 ty' <- addUsingConstraints syn fc ty'

90− ty' <- implicit info syn n ty'

82+ ty' <- addUsingImpls syn n fc ty'

83+ let ty = addImpl i ty'

92− let ty = addImpl i ty'

93− inacc = inaccessibleArgs 0 ty

94− logLvl 5 $ show n ++ " type pre-addimpl " ++ showTmImpls ty'

85+ logLvl 3 $ show n ++ " type pre-addimpl " ++ showTmImpls ty'

95− logLvl 5 $ show n ++ " type " ++ showTmImpls ty

86+ logLvl 3 $ show n ++ " type " ++ show (using syn) ++ "\n" ++ showTmImpls ty

96− logLvl 3 $ show n ++ ": inaccessible arguments: " ++ show inacc

98− ((tyT, defer, is), log) <-

88+ ((tyT', defer, is), log) <-

99 tclift $ elaborate ctxt n (TType (UVal 0)) []

89 tclift $ elaborate ctxt n (TType (UVal 0)) []

100− (errAt "type of " n (erun fc (build i info False [] n ty)))

90+ (errAt "type of " n (erun fc (build i info ETyDecl [] n ty)))

91+

92+ let tyT = patToImp tyT'

93+

94+ logLvl 3 $ show ty ++ "\nElaborated: " ++ show tyT'

95+

101 ds <- checkAddDef True False fc defer

96 ds <- checkAddDef True False fc defer

102 -- if the type is not complete, note that we'll need to infer

97 -- if the type is not complete, note that we'll need to infer

103 -- things later (for solving metavariables)

98 -- things later (for solving metavariables)

@@ -107,19 +102,52 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

107 ctxt <- getContext

102 ctxt <- getContext

108 logLvl 5 $ "Rechecking"

103 logLvl 5 $ "Rechecking"

109 logLvl 6 $ show tyT

104 logLvl 6 $ show tyT

105+ logLvl 10 $ "Elaborated to " ++ showEnvDbg [] tyT

110 (cty, _) <- recheckC fc [] tyT

106 (cty, _) <- recheckC fc [] tyT

107+

108+ -- record the implicit and inaccessible arguments

109+ i <- getIState

110+ let (inaccData, impls) = unzip $ getUnboundImplicits i cty ty

111+ let inacc = inaccessibleImps 0 cty inaccData

112+ logLvl 3 $ show n ++ ": inaccessible arguments: " ++ show inacc

113+

114+ putIState $ i { idris_implicits = addDef n impls (idris_implicits i) }

115+ logLvl 3 ("Implicit " ++ show n ++ " " ++ show impls)

116+ addIBC (IBCImp n)

117+

118+ return (cty, ty, inacc)

119+ where

120+ patToImp (Bind n (PVar t) sc) = Bind n (Pi t) (patToImp sc)

121+ patToImp (Bind n b sc) = Bind n b (patToImp sc)

122+ patToImp t = t

123+

124+

125+-- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".

126+elabType :: ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] ->

127+ FC -> FnOpts -> Name -> PTerm -> Idris Type

128+elabType = elabType' False

129+

130+elabType' :: Bool -> -- normalise it

131+ ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] ->

132+ FC -> FnOpts -> Name -> PTerm -> Idris Type

133+elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params info) ty_in

134+ n = liftname info n_in in -}

135+ do checkUndefined fc n

136+ (cty, ty, inacc) <- buildType info syn fc opts n ty'

137+

111− addStatics n cty ty'

138+ addStatics n cty ty

112− logLvl 6 $ "Elaborated to " ++ showEnvDbg [] tyT

113 logLvl 2 $ "Rechecked to " ++ show cty

139 logLvl 2 $ "Rechecked to " ++ show cty

114 let nty = cty -- normalise ctxt [] cty

140 let nty = cty -- normalise ctxt [] cty

115 -- if the return type is something coinductive, freeze the definition

141 -- if the return type is something coinductive, freeze the definition

142+ ctxt <- getContext

116 let nty' = normalise ctxt [] nty

143 let nty' = normalise ctxt [] nty

117

144

118 -- Add normalised type to internals

145 -- Add normalised type to internals

146+ i <- getIState

119 rep <- useREPL

147 rep <- useREPL

120 when rep $ do

148 when rep $ do

121− addInternalApp (fc_fname fc) (fst . fc_start $ fc) (mergeTy ty' (delab i nty')) -- TODO: Should use span instead of line and filename?

149+ addInternalApp (fc_fname fc) (fst . fc_start $ fc) ty' -- (mergeTy ty' (delab i nty')) -- TODO: Should use span instead of line and filename?

122− addIBC (IBCLineApp (fc_fname fc) (fst . fc_start $ fc) (mergeTy ty' (delab i nty')))

150+ addIBC (IBCLineApp (fc_fname fc) (fst . fc_start $ fc) ty') -- (mergeTy ty' (delab i nty')))

123

151

124 let (t, _) = unApply (getRetTy nty')

152 let (t, _) = unApply (getRetTy nty')

125 let corec = case t of

153 let corec = case t of

@@ -163,7 +191,7 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

163 -- for making an internalapp, we only want the explicit ones, and don't

191 -- for making an internalapp, we only want the explicit ones, and don't

164 -- want the parameters, so just take the arguments which correspond to the

192 -- want the parameters, so just take the arguments which correspond to the

165 -- user declared explicit ones

193 -- user declared explicit ones

166− mergeTy (PPi e n ty sc) (PPi e' _ _ sc')

194+ mergeTy (PPi e n ty sc) (PPi e' n' _ sc')

167 | e == e' = PPi e n ty (mergeTy sc sc')

195 | e == e' = PPi e n ty (mergeTy sc sc')

168 | otherwise = mergeTy sc sc'

196 | otherwise = mergeTy sc sc'

169 mergeTy _ sc = sc

197 mergeTy _ sc = sc

@@ -184,6 +212,14 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

184 , ns4 == map txt ["Errors","Reflection","Language"] = True

212 , ns4 == map txt ["Errors","Reflection","Language"] = True

185 tyIsHandler _ = False

213 tyIsHandler _ = False

186

214

215+-- Get the list of (index, name) of inaccessible arguments from an elaborated

216+-- type

217+inaccessibleImps :: Int -> Type -> [Bool] -> [(Int, Name)]

218+inaccessibleImps i (Bind n (Pi t) sc) (inacc : ins)

219+ | inacc = (i, n) : inaccessibleImps (i + 1) sc ins

220+ | otherwise = inaccessibleImps (i + 1) sc ins

221+inaccessibleImps _ _ _ = []

222+

187-- Get the list of (index, name) of inaccessible arguments from the type.

223-- Get the list of (index, name) of inaccessible arguments from the type.

188inaccessibleArgs :: Int -> PTerm -> [(Int, Name)]

224inaccessibleArgs :: Int -> PTerm -> [(Int, Name)]

189inaccessibleArgs i (PPi (Imp _ _ _) n Placeholder t)

225inaccessibleArgs i (PPi (Imp _ _ _) n Placeholder t)

@@ -210,42 +246,20 @@ elabData info syn doc argDocs fc opts (PLaterdecl n t_in)

210 = do let codata = Codata `elem` opts

246 = do let codata = Codata `elem` opts

211 iLOG (show (fc, doc))

247 iLOG (show (fc, doc))

212 checkUndefined fc n

248 checkUndefined fc n

213− ctxt <- getContext

249+ (cty, t, inacc) <- buildType info syn fc [] n t_in

214− i <- getIState

250+

215− -- TODO think: something more in info?

216− t_in <- implicit info syn n t_in

217− let t = addImpl i t_in

218− ((t', defer, is), log) <- tclift $ elaborate ctxt n (TType (UVal 0)) []

219− (erun fc (build i info False [] n t))

220− def' <- checkDef fc defer

221− let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) def'

222− addDeferredTyCon def''

223 addIBC (IBCDef n)

251 addIBC (IBCDef n)

224− mapM_ (elabCaseBlock info []) is

225− (cty, _) <- recheckC fc [] t'

226− logLvl 2 $ "---> " ++ show cty

227 updateContext (addTyDecl n (TCon 0 0) cty) -- temporary, to check cons

252 updateContext (addTyDecl n (TCon 0 0) cty) -- temporary, to check cons

228

253

229elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

254elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

230 = do let codata = Codata `elem` opts

255 = do let codata = Codata `elem` opts

231 iLOG (show fc)

256 iLOG (show fc)

232 undef <- isUndefined fc n

257 undef <- isUndefined fc n

233− ctxt <- getContext

258+ (cty, t, inacc) <- buildType info syn fc [] n t_in

234− i <- getIState

235− t_in <- implicit info syn n t_in

236− let t = addImpl i t_in

237− ((t', defer, is), log) <-

238− tclift $ elaborate ctxt n (TType (UVal 0)) []

239− (errAt "data declaration " n (erun fc (build i info False [] n t)))

240− def' <- checkDef fc defer

241− let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) def'

242 -- if n is defined already, make sure it is just a type declaration

259 -- if n is defined already, make sure it is just a type declaration

243 -- with the same type we've just elaborated

260 -- with the same type we've just elaborated

261+ i <- getIState

244− checkDefinedAs fc n t' (tt_ctxt i)

262+ checkDefinedAs fc n cty (tt_ctxt i)

245− addDeferredTyCon def''

246− mapM_ (elabCaseBlock info []) is

247− (cty, _) <- recheckC fc [] t'

248− logLvl 2 $ "---> " ++ show cty

249 -- temporary, to check cons

263 -- temporary, to check cons

250 when undef $ updateContext (addTyDecl n (TCon 0 0) cty)

264 when undef $ updateContext (addTyDecl n (TCon 0 0) cty)

251 let cnameinfo = cinfo info (map cname dcons)

265 let cnameinfo = cinfo info (map cname dcons)

@@ -262,7 +276,7 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

262 (idris_datatypes i) })

276 (idris_datatypes i) })

263 addIBC (IBCDef n)

277 addIBC (IBCDef n)

264 addIBC (IBCData n)

278 addIBC (IBCData n)

265− checkDocs fc argDocs t_in

279+ checkDocs fc argDocs t

266 addDocStr n doc argDocs

280 addDocStr n doc argDocs

267 addIBC (IBCDoc n)

281 addIBC (IBCDoc n)

268 let metainf = DataMI params

282 let metainf = DataMI params

@@ -368,6 +382,56 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

368 liftname = id -- Is this appropriate?

382 liftname = id -- Is this appropriate?

369 }

383 }

370

384

385+-- FIXME: 'forcenames' is an almighty hack! Need a better way of

386+-- erasing non-forceable things

387+-- ^^^

388+-- TODO: the above is a comment from the past;

389+-- forcenames is probably no longer needed

390+elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->

391+ (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name]) -> Idris (Name, Type)

392+elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)

393+ = do checkUndefined fc n

394+ (cty, t, inacc) <- buildType info syn fc [] n (if codata then mkLazy t_in else t_in)

395+ ctxt <- getContext

396+ let cty' = normalise ctxt [] cty

397+

398+ logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t

399+ logLvl 5 $ "Inaccessible args: " ++ show inacc

400+ logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty'

401+

402+ addIBC (IBCDef n)

403+ checkDocs fc argDocs t

404+ addDocStr n doc argDocs

405+ addIBC (IBCDoc n)

406+ fputState (opt_inaccessible . ist_optimisation n) inacc

407+ addIBC (IBCOpt n)

408+ return (n, cty')

409+ where

410+ tyIs (Bind n b sc) = tyIs sc

411+ tyIs t | (P _ n' _, _) <- unApply t

412+ = if n' /= tn then tclift $ tfail (At fc (Msg (show n' ++ " is not " ++ show tn)))

413+ else return ()

414+ tyIs t = tclift $ tfail (At fc (Msg (show t ++ " is not " ++ show tn)))

415+

416+ mkLazy (PPi pl n ty sc)

417+ = let ty' = if getTyName ty

418+ then PApp fc (PRef fc (sUN "Lazy'"))

419+ [pexp (PRef fc (sUN "LazyCodata")),

420+ pexp ty]

421+ else ty in

422+ PPi pl n ty' (mkLazy sc)

423+ mkLazy t = t

424+

425+ getTyName (PApp _ (PRef _ n) _) = n == nsroot tn

426+ getTyName (PRef _ n) = n == nsroot tn

427+ getTyName _ = False

428+

429+

430+ getNamePos :: Int -> PTerm -> Name -> Maybe Int

431+ getNamePos i (PPi _ n _ sc) x | n == x = Just i

432+ | otherwise = getNamePos (i + 1) sc x

433+ getNamePos _ _ _ = Nothing

434+

371type EliminatorState = StateT (Map.Map String Int) Idris

435type EliminatorState = StateT (Map.Map String Int) Idris

372

436

373-- TODO: Rewrite everything to use idris_implicits instead of manual splitting (or in TT)

437-- TODO: Rewrite everything to use idris_implicits instead of manual splitting (or in TT)

@@ -699,15 +763,15 @@ elabProvider info syn fc what n

699 -- First elaborate the expected type (and check that it's a type)

763 -- First elaborate the expected type (and check that it's a type)

700 -- The goal type for a postulate is always Type.

764 -- The goal type for a postulate is always Type.

701 (ty', typ) <- case what of

765 (ty', typ) <- case what of

702− ProvTerm ty p -> elabVal toplevel False ty

766+ ProvTerm ty p -> elabVal toplevel ERHS ty

703− ProvPostulate _ -> elabVal toplevel False PType

767+ ProvPostulate _ -> elabVal toplevel ERHS PType

704 unless (isTType typ) $

768 unless (isTType typ) $

705 ifail ("Expected a type, got " ++ show ty' ++ " : " ++ show typ)

769 ifail ("Expected a type, got " ++ show ty' ++ " : " ++ show typ)

706

770

707 -- Elaborate the provider term to TT and check that the type matches

771 -- Elaborate the provider term to TT and check that the type matches

708 (e, et) <- case what of

772 (e, et) <- case what of

709− ProvTerm _ tm -> elabVal toplevel False tm

773+ ProvTerm _ tm -> elabVal toplevel ERHS tm

710− ProvPostulate tm -> elabVal toplevel False tm

774+ ProvPostulate tm -> elabVal toplevel ERHS tm

711 unless (isProviderOf (normalise ctxt [] ty') et) $

775 unless (isProviderOf (normalise ctxt [] ty') et) $

712 ifail $ "Expected provider type IO (Provider (" ++

776 ifail $ "Expected provider type IO (Provider (" ++

713 show ty' ++ "))" ++ ", got " ++ show et ++ " instead."

777 show ty' ++ "))" ++ ", got " ++ show et ++ " instead."

@@ -756,7 +820,7 @@ elabTransform info fc safe lhs_in rhs_in

756 let lhs = addImplPat i lhs_in

820 let lhs = addImplPat i lhs_in

757 ((lhs', dlhs, []), _) <-

821 ((lhs', dlhs, []), _) <-

758 tclift $ elaborate ctxt (sMN 0 "transLHS") infP []

822 tclift $ elaborate ctxt (sMN 0 "transLHS") infP []

759− (erun fc (buildTC i info True [] (sUN "transform")

823+ (erun fc (buildTC i info ELHS [] (sUN "transform")

760 (infTerm lhs)))

824 (infTerm lhs)))

761 let lhs_tm = orderPats (getInferTerm lhs')

825 let lhs_tm = orderPats (getInferTerm lhs')

762 let lhs_ty = getInferType lhs'

826 let lhs_ty = getInferType lhs'

@@ -769,7 +833,7 @@ elabTransform info fc safe lhs_in rhs_in

769 tclift $ elaborate ctxt (sMN 0 "transRHS") clhs_ty []

833 tclift $ elaborate ctxt (sMN 0 "transRHS") clhs_ty []

770 (do pbinds i lhs_tm

834 (do pbinds i lhs_tm

771 setNextName

835 setNextName

772− erun fc (build i info False [] (sUN "transform") rhs)

836+ erun fc (build i info ERHS [] (sUN "transform") rhs)

773 erun fc $ psolve lhs_tm

837 erun fc $ psolve lhs_tm

774 tt <- get_term

838 tt <- get_term

775 return (runState (collectDeferred Nothing tt) []))

839 return (runState (collectDeferred Nothing tt) []))

@@ -945,70 +1009,6 @@ elabRecord info syn doc fc tyn ty opts cdoc cn cty_in

945 then PPi impl n' ty (implBindUp ns is t)

1009 then PPi impl n' ty (implBindUp ns is t)

946 else implBindUp ns is t

1010 else implBindUp ns is t

947

1011

948−-- FIXME: 'forcenames' is an almighty hack! Need a better way of

949−-- erasing non-forceable things

950−-- ^^^

951−-- TODO: the above is a comment from the past;

952−-- forcenames is probably no longer needed

953−elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->

954− (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name]) -> Idris (Name, Type)

955−elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)

956− = do checkUndefined fc n

957− ctxt <- getContext

958− i <- getIState

959− t_in <- implicit info syn n (if codata then mkLazy t_in else t_in)

960− let t = addImpl i t_in

961− logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t

962− let inacc = inaccessibleArgs 0 t

963− logLvl 5 $ "Inaccessible args: " ++ show inacc

964− ((t', defer, is), log) <-

965− tclift $ elaborate ctxt n (TType (UVal 0)) []

966− (errAt "constructor " n (erun fc (build i info False [] n t)))

967− logLvl 2 $ "Rechecking " ++ show t'

968− def' <- checkDef fc defer

969− let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) def'

970− addDeferred def''

971− mapM_ (\(n, _) -> addIBC (IBCDef n)) def''

972−

973− mapM_ (elabCaseBlock info []) is

974− ctxt <- getContext

975− (cty, _) <- recheckC fc [] t'

976− let cty' = normaliseC ctxt [] cty

977− tyIs cty'

978− logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty'

979− addIBC (IBCDef n)

980− checkDocs fc argDocs t_in

981− addDocStr n doc argDocs

982− addIBC (IBCDoc n)

983− fputState (opt_inaccessible . ist_optimisation n) inacc

984− addIBC (IBCOpt n)

985− return (n, cty')

986− where

987− tyIs (Bind n b sc) = tyIs sc

988− tyIs t | (P _ n' _, _) <- unApply t

989− = if n' /= tn then tclift $ tfail (At fc (Msg (show n' ++ " is not " ++ show tn)))

990− else return ()

991− tyIs t = tclift $ tfail (At fc (Msg (show t ++ " is not " ++ show tn)))

992−

993− mkLazy (PPi pl n ty sc)

994− = let ty' = if getTyName ty

995− then PApp fc (PRef fc (sUN "Lazy'"))

996− [pexp (PRef fc (sUN "LazyCodata")),

997− pexp ty]

998− else ty in

999− PPi pl n ty' (mkLazy sc)

1000− mkLazy t = t

1001−

1002− getTyName (PApp _ (PRef _ n) _) = n == nsroot tn

1003− getTyName (PRef _ n) = n == nsroot tn

1004− getTyName _ = False

1005−

1006−

1007− getNamePos :: Int -> PTerm -> Name -> Maybe Int

1008− getNamePos i (PPi _ n _ sc) x | n == x = Just i

1009− | otherwise = getNamePos (i + 1) sc x

1010− getNamePos _ _ _ = Nothing

1011−

1012-- | Elaborate a collection of left-hand and right-hand pairs - that is, a

1013-- top-level definition.

1014elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()

@@ -1322,7 +1322,7 @@ elabPE info fc caller r =

1322

1323-- Elaborate a value, returning any new bindings created (this will only

1324-- happen if elaborating as a pattern clause)

1325−elabValBind :: ElabInfo -> Bool -> Bool -> PTerm -> Idris (Term, Type, [(Name, Type)])

1325+elabValBind :: ElabInfo -> ElabMode -> Bool -> PTerm -> Idris (Term, Type, [(Name, Type)])

1326elabValBind info aspat norm tm_in

1327 = do ctxt <- getContext

1328 i <- getIState

@@ -1356,7 +1356,7 @@ elabValBind info aspat norm tm_in

1356

1357 return (vtm, vty, bargs)

1358

1359−elabVal :: ElabInfo -> Bool -> PTerm -> Idris (Term, Type)

1359+elabVal :: ElabInfo -> ElabMode -> PTerm -> Idris (Term, Type)

1360elabVal info aspat tm_in

1361 = do (tm, ty, _) <- elabValBind info aspat False tm_in

1362 return (tm, ty)

@@ -1371,7 +1371,7 @@ checkPossible info fc tcgen fname lhs_in

1371 let lhs = addImplPat i lhs_in

1372 -- if the LHS type checks, it is possible

1373 case elaborate ctxt (sMN 0 "patLHS") infP []

1374− (erun fc (buildTC i info True [] fname (infTerm lhs))) of

1374+ (erun fc (buildTC i info ELHS [] fname (infTerm lhs))) of

1375 OK ((lhs', _, _), _) ->

1376 do let lhs_tm = orderPats (getInferTerm lhs')

1377 case recheck ctxt [] (forget lhs_tm) lhs_tm of

@@ -1524,7 +1524,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1524 (((lhs', dlhs, []), probs, inj), _) <-

1525 tclift $ elaborate ctxt (sMN 0 "patLHS") infP []

1526 (do res <- errAt "left hand side of " fname

1527− (erun fc (buildTC i info True opts fname (infTerm lhs)))

1527+ (erun fc (buildTC i info ELHS opts fname (infTerm lhs)))

1528 probs <- get_probs

1529 inj <- get_inj

1530 return (res, probs, inj))

@@ -1582,7 +1582,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1582 mapM_ setinj (nub (params ++ inj))

1583 setNextName

1584 (_, _, is) <- errAt "right hand side of " fname

1585− (erun fc (build i winfo False opts fname rhs))

1585+ (erun fc (build i winfo ERHS opts fname rhs))

1586 errAt "right hand side of " fname

1587 (erun fc $ psolve lhs_tm)

1588 hs <- get_holes

@@ -1716,7 +1716,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

1716 ((lhs', dlhs, []), _) <-

1717 tclift $ elaborate ctxt (sMN 0 "patLHS") infP []

1718 (errAt "left hand side of with in " fname

1719− (erun fc (buildTC i info True opts fname (infTerm lhs))) )

1719+ (erun fc (buildTC i info ELHS opts fname (infTerm lhs))) )

1720 let lhs_tm = orderPats (getInferTerm lhs')

1721 let lhs_ty = getInferType lhs'

1722 let ret_ty = getRetTy lhs_ty

@@ -1734,7 +1734,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

1734 setNextName

1735 -- TODO: may want where here - see winfo abpve

1736 (_', d, is) <- errAt "with value in " fname

1737− (erun fc (build i info False opts fname (infTerm wval)))

1737+ (erun fc (build i info ERHS opts fname (infTerm wval)))

1738 erun fc $ psolve lhs_tm

1739 tt <- get_term

1740 return (tt, d, is))

@@ -1797,7 +1797,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

1797 tclift $ elaborate ctxt (sMN 0 "wpatRHS") clhsty []

1798 (do pbinds i lhs_tm

1799 setNextName

1800− (_, d, is) <- erun fc (build i info False opts fname rhs)

1800+ (_, d, is) <- erun fc (build i info ERHS opts fname rhs)

1801 psolve lhs_tm

1802 tt <- get_term

1803 return (tt, d, is))

@@ -1874,11 +1874,14 @@ data MArgTy = IA | EA | CA deriving Show

1874elabClass :: ElabInfo -> SyntaxInfo -> Docstring ->

1875 FC -> [PTerm] ->

1876 Name -> [(Name, PTerm)] -> [(Name, Docstring)] -> [PDecl] -> Idris ()

1877−elabClass info syn doc fc constraints tn ps pDocs ds

1877+elabClass info syn_in doc fc constraints tn ps pDocs ds

1878 = do let cn = SN (InstanceCtorN tn) -- sUN ("instance" ++ show tn) -- MN 0 ("instance" ++ show tn)

1879 let tty = pibind ps PType

1880 let constraint = PApp fc (PRef fc tn)

1881 (map (pexp . PRef fc) (map fst ps))

1882+

1883+ let syn = syn_in { using = addToUsing (using syn_in) ps }

1884+

1882 -- build data declaration

1885 -- build data declaration

1883 let mdecls = filter tydecl ds -- method declarations

1886 let mdecls = filter tydecl ds -- method declarations

1884 let idecls = filter instdecl ds -- default superclass instance declarations

1887 let idecls = filter instdecl ds -- default superclass instance declarations

@@ -1904,12 +1907,12 @@ elabClass info syn doc fc constraints tn ps pDocs ds

1904 elabData info (syn { no_imp = no_imp syn ++ mnames }) doc pDocs fc [] ddecl

1907 elabData info (syn { no_imp = no_imp syn ++ mnames }) doc pDocs fc [] ddecl

1905 -- for each constraint, build a top level function to chase it

1908 -- for each constraint, build a top level function to chase it

1906 logLvl 5 $ "Building functions"

1909 logLvl 5 $ "Building functions"

1907− let usyn = syn { using = map (\ (x,y) -> UImplicit x y) ps

1910+-- let usyn = syn { using = map (\ (x,y) -> UImplicit x y) ps

1908− ++ using syn }

1911+-- ++ using syn }

1909− fns <- mapM (cfun cn constraint usyn (map fst imethods)) constraints

1912+ fns <- mapM (cfun cn constraint syn (map fst imethods)) constraints

1910 mapM_ (elabDecl EAll info) (concat fns)

1913 mapM_ (elabDecl EAll info) (concat fns)

1911 -- for each method, build a top level function

1914 -- for each method, build a top level function

1912− fns <- mapM (tfun cn constraint usyn (map fst imethods)) imethods

1915+ fns <- mapM (tfun cn constraint syn (map fst imethods)) imethods

1913 mapM_ (elabDecl EAll info) (concat fns)

1916 mapM_ (elabDecl EAll info) (concat fns)

1914 -- add the default definitions

1917 -- add the default definitions

1915 mapM_ (elabDecl EAll info) (concat (map (snd.snd) defs))

1918 mapM_ (elabDecl EAll info) (concat (map (snd.snd) defs))

@@ -2154,7 +2157,7 @@ elabInstance info syn what fc cs n ps t expn ds = do

2154 ctxt <- getContext

2157 ctxt <- getContext

2155 ((tyT, _, _), _) <-

2158 ((tyT, _, _), _) <-

2156 tclift $ elaborate ctxt iname (TType (UVal 0)) []

2159 tclift $ elaborate ctxt iname (TType (UVal 0)) []

2157− (errAt "type of " iname (erun fc (build i info False [] iname ty)))

2160+ (errAt "type of " iname (erun fc (build i info ERHS [] iname ty)))

2158 ctxt <- getContext

2161 ctxt <- getContext

2159 (cty, _) <- recheckC fc [] tyT

2162 (cty, _) <- recheckC fc [] tyT

2160 let nty = normalise ctxt [] cty

2163 let nty = normalise ctxt [] cty

src/Idris/ElabTerm.hs+49−26

@@ -29,6 +29,9 @@ import qualified Data.Text as T

30import Debug.Trace

32+data ElabMode = ETyDecl | ELHS | ERHS

33+ deriving Eq

34+

32-- Using the elaborator, convert a term in raw syntax to a fully

35-- Using the elaborator, convert a term in raw syntax to a fully

33-- elaborated, typechecked term.

36-- elaborated, typechecked term.

34--

37--

@@ -37,10 +40,10 @@ import Debug.Trace

38-- Also find deferred names in the term and their types

41-- Also find deferred names in the term and their types

40−build :: IState -> ElabInfo -> Bool -> FnOpts -> Name -> PTerm ->

43+build :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->

41 ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])

44 ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])

42−build ist info pattern opts fn tm

45+build ist info emode opts fn tm

43− = do elab ist info pattern opts fn tm

46+ = do elab ist info emode opts fn tm

44 let tmIn = tm

47 let tmIn = tm

45 let inf = case lookupCtxt fn (idris_tyinfodata ist) of

48 let inf = case lookupCtxt fn (idris_tyinfodata ist) of

46 [TIPartial] -> True

49 [TIPartial] -> True

@@ -80,20 +83,32 @@ build ist info pattern opts fn tm

80 ((_,_,_,e,_,_):es) -> traceWhen u ("Final problems:\n" ++ show probs) $

83 ((_,_,_,e,_,_):es) -> traceWhen u ("Final problems:\n" ++ show probs) $

81 if inf then return ()

84 if inf then return ()

82 else lift (Error e)

85 else lift (Error e)

86+

87+ when tydecl (do update_term orderPats

88+ mkPat)

89+-- update_term liftPats)

83 is <- getAux

90 is <- getAux

84 tt <- get_term

91 tt <- get_term

85 let (tm, ds) = runState (collectDeferred (Just fn) tt) []

92 let (tm, ds) = runState (collectDeferred (Just fn) tt) []

86 log <- getLog

93 log <- getLog

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

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

88 else return (tm, ds, is)

95 else return (tm, ds, is)

96+ where pattern = emode == ELHS

97+ tydecl = emode == ETyDecl

98+

99+ mkPat = do hs <- get_holes

100+ tm <- get_term

101+ case hs of

102+ (h: hs) -> do patvar h; mkPat

103+ [] -> return ()

104

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

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

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

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

92-- know about yet on the LHS of a pattern def)

107-- know about yet on the LHS of a pattern def)

108

94−buildTC :: IState -> ElabInfo -> Bool -> FnOpts -> Name -> PTerm ->

109+buildTC :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->

95 ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])

110 ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])

96−buildTC ist info pattern opts fn tm

111+buildTC ist info emode opts fn tm

97 = do -- set name supply to begin after highest index in tm

112 = do -- set name supply to begin after highest index in tm

98 let ns = allNamesIn tm

113 let ns = allNamesIn tm

99 let tmIn = tm

114 let tmIn = tm

@@ -101,7 +116,7 @@ buildTC ist info pattern opts fn tm

101 [TIPartial] -> True

116 [TIPartial] -> True

102 _ -> False

117 _ -> False

103 initNextNameFrom ns

118 initNextNameFrom ns

104− elab ist info pattern opts fn tm

119+ elab ist info emode opts fn tm

105 probs <- get_probs

120 probs <- get_probs

106 tm <- get_term

121 tm <- get_term

107 case probs of

122 case probs of

@@ -114,13 +129,14 @@ buildTC ist info pattern opts fn tm

114 log <- getLog

129 log <- getLog

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

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

116 else return (tm, ds, is)

131 else return (tm, ds, is)

132+ where pattern = emode == ELHS

117

133

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

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

119-- (most likely case blocks to elaborate)

135-- (most likely case blocks to elaborate)

120

136

121−elab :: IState -> ElabInfo -> Bool -> FnOpts -> Name -> PTerm ->

137+elab :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->

122 ElabD ()

138 ElabD ()

123−elab ist info pattern opts fn tm

139+elab ist info emode opts fn tm

124 = do let loglvl = opt_logLevel (idris_options ist)

140 = do let loglvl = opt_logLevel (idris_options ist)

125 when (loglvl > 5) $ unifyLog True

141 when (loglvl > 5) $ unifyLog True

126 compute -- expand type synonyms, etc

142 compute -- expand type synonyms, etc

@@ -133,12 +149,15 @@ elab ist info pattern opts fn tm

133 unifyProblems

149 unifyProblems

134 mkPat)

150 mkPat)

135 where

151 where

152+ pattern = emode == ELHS

153+ bindfree = emode == ETyDecl || emode == ELHS

154+

136 tcgen = Dictionary `elem` opts

155 tcgen = Dictionary `elem` opts

137 reflection = Reflection `elem` opts

156 reflection = Reflection `elem` opts

138

157

139 isph arg = case getTm arg of

158 isph arg = case getTm arg of

140 Placeholder -> (True, priority arg)

159 Placeholder -> (True, priority arg)

141− _ -> (False, priority arg)

160+ tm -> (False, priority arg)

142

161

143 toElab ina arg = case getTm arg of

162 toElab ina arg = case getTm arg of

144 Placeholder -> Nothing

163 Placeholder -> Nothing

@@ -290,25 +309,29 @@ elab ist info pattern opts fn tm

290 trySeq' deferr [] = proofFail deferr

309 trySeq' deferr [] = proofFail deferr

291 trySeq' deferr (x : xs)

310 trySeq' deferr (x : xs)

292 = try' (elab' ina x) (trySeq' deferr xs) True

311 = try' (elab' ina x) (trySeq' deferr xs) True

293− elab' ina (PPatvar fc n) | pattern = patvar n

312+ elab' ina (PPatvar fc n) | bindfree = do patvar n; -- update_term liftPats

294-- elab' (_, _, inty) (PRef fc f)

313-- elab' (_, _, inty) (PRef fc f)

295-- | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty

314-- | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty

296-- = lift $ tfail (Msg "Typecase is not allowed")

315-- = lift $ tfail (Msg "Typecase is not allowed")

297− elab' (ina, guarded, inty, qq) (PRef fc n) | pattern && not (inparamBlock n) && not qq

316+ elab' (ina, guarded, inty, qq) (PRef fc n)

317+ | (pattern || (bindfree && bindable n)) && not (inparamBlock n) && not qq

298 = do ctxt <- get_context

318 = do ctxt <- get_context

299 let defined = case lookupTy n ctxt of

319 let defined = case lookupTy n ctxt of

300 [] -> False

320 [] -> False

301 _ -> True

321 _ -> True

302 -- this is to stop us resolve type classes recursively

322 -- this is to stop us resolve type classes recursively

303 -- trace (show (n, guarded)) $

323 -- trace (show (n, guarded)) $

304− if (tcname n && ina) then erun fc $ patvar n

324+ if (tcname n && ina) then erun fc $ do patvar n; -- update_term liftPats

305 else if (defined && not guarded)

325 else if (defined && not guarded)

306 then do apply (Var n) []; solve

326 then do apply (Var n) []; solve

307 else try (do apply (Var n) []; solve)

327 else try (do apply (Var n) []; solve)

308− (patvar n)

328+ (do patvar n; ) -- update_term liftPats)

309 where inparamBlock n = case lookupCtxtName n (inblock info) of

329 where inparamBlock n = case lookupCtxtName n (inblock info) of

310 [] -> False

330 [] -> False

311 _ -> True

331 _ -> True

332+ bindable (NS _ _) = False

333+ bindable (UN xs) = True

334+ bindable n = implicitable n

312 elab' ina f@(PInferRef fc n) = elab' ina (PApp fc f [])

335 elab' ina f@(PInferRef fc n) = elab' ina (PApp fc f [])

313 elab' ina (PRef fc n) = erun fc $ do apply (Var n) []; solve

336 elab' ina (PRef fc n) = erun fc $ do apply (Var n) []; solve

314 elab' ina@(_, a, inty, qq) (PLam n Placeholder sc)

337 elab' ina@(_, a, inty, qq) (PLam n Placeholder sc)

@@ -924,11 +947,11 @@ findInstances ist t

924 | otherwise = []

947 | otherwise = []

925

948

926trivial' ist

949trivial' ist

927− = trivial (elab ist toplevel False [] (sMN 0 "tac")) ist

950+ = trivial (elab ist toplevel ERHS [] (sMN 0 "tac")) ist

928proofSearch' ist rec depth prv top n hints

951proofSearch' ist rec depth prv top n hints

929 = do unifyProblems

952 = do unifyProblems

930 proofSearch rec prv depth

953 proofSearch rec prv depth

931− (elab ist toplevel False [] (sMN 0 "tac")) top n hints ist

954+ (elab ist toplevel ERHS [] (sMN 0 "tac")) top n hints ist

932

955

933resolveTC :: Int -> Term -> Name -> IState -> ElabD ()

956resolveTC :: Int -> Term -> Name -> IState -> ElabD ()

934resolveTC = resTC' []

957resolveTC = resTC' []

@@ -1048,7 +1071,7 @@ case_ ind autoSolve ist fn tm = do

1048 letn <- getNameFrom (sMN 0 "irule")

1071 letn <- getNameFrom (sMN 0 "irule")

1049 letbind letn (Var tyn) (Var valn)

1072 letbind letn (Var tyn) (Var valn)

1050 focus valn

1073 focus valn

1051− elab ist toplevel False [] (sMN 0 "tac") tm

1074+ elab ist toplevel ERHS [] (sMN 0 "tac") tm

1052 env <- get_env

1075 env <- get_env

1053 let (Just binding) = lookup letn env

1076 let (Just binding) = lookup letn env

1054 let val = binderVal binding

1077 let val = binderVal binding

@@ -1081,7 +1104,7 @@ runTac autoSolve ist fn tac

1081 where

1104 where

1082 bname (Bind n _ _) = Just n

1105 bname (Bind n _ _) = Just n

1083 bname _ = Nothing

1106 bname _ = Nothing

1084− runT (Exact tm) = do elab ist toplevel False [] (sMN 0 "tac") tm

1107+ runT (Exact tm) = do elab ist toplevel ERHS [] (sMN 0 "tac") tm

1085 when autoSolve solveAll

1108 when autoSolve solveAll

1086 runT (MatchRefine fn)

1109 runT (MatchRefine fn)

1087 = do fnimps <-

1110 = do fnimps <-

@@ -1130,7 +1153,7 @@ runTac autoSolve ist fn tac

1130 letn <- getNameFrom (sMN 0 "equiv_val")

1153 letn <- getNameFrom (sMN 0 "equiv_val")

1131 letbind letn (Var tyn) (Var valn)

1154 letbind letn (Var tyn) (Var valn)

1132 focus tyn

1155 focus tyn

1133− elab ist toplevel False [] (sMN 0 "tac") tm

1156+ elab ist toplevel ERHS [] (sMN 0 "tac") tm

1134 focus valn

1157 focus valn

1135 when autoSolve solveAll

1158 when autoSolve solveAll

1136 runT (Rewrite tm) -- to elaborate tm, let bind it, then rewrite by that

1159 runT (Rewrite tm) -- to elaborate tm, let bind it, then rewrite by that

@@ -1143,7 +1166,7 @@ runTac autoSolve ist fn tac

1143 letn <- getNameFrom (sMN 0 "rewrite_rule")

1166 letn <- getNameFrom (sMN 0 "rewrite_rule")

1144 letbind letn (Var tyn) (Var valn)

1167 letbind letn (Var tyn) (Var valn)

1145 focus valn

1168 focus valn

1146− elab ist toplevel False [] (sMN 0 "tac") tm

1169+ elab ist toplevel ERHS [] (sMN 0 "tac") tm

1147 rewrite (Var letn)

1170 rewrite (Var letn)

1148 when autoSolve solveAll

1171 when autoSolve solveAll

1149 runT (Induction tm) -- let bind tm, similar to the others

1172 runT (Induction tm) -- let bind tm, similar to the others

@@ -1159,7 +1182,7 @@ runTac autoSolve ist fn tac

1159 letn <- unique_hole n

1182 letn <- unique_hole n

1160 letbind letn (Var tyn) (Var valn)

1183 letbind letn (Var tyn) (Var valn)

1161 focus valn

1184 focus valn

1162− elab ist toplevel False [] (sMN 0 "tac") tm

1185+ elab ist toplevel ERHS [] (sMN 0 "tac") tm

1163 when autoSolve solveAll

1186 when autoSolve solveAll

1164 runT (LetTacTy n ty tm)

1187 runT (LetTacTy n ty tm)

1165 = do attack

1188 = do attack

@@ -1170,9 +1193,9 @@ runTac autoSolve ist fn tac

1170 letn <- unique_hole n

1193 letn <- unique_hole n

1171 letbind letn (Var tyn) (Var valn)

1194 letbind letn (Var tyn) (Var valn)

1172 focus tyn

1195 focus tyn

1173− elab ist toplevel False [] (sMN 0 "tac") ty

1196+ elab ist toplevel ERHS [] (sMN 0 "tac") ty

1174 focus valn

1197 focus valn

1175− elab ist toplevel False [] (sMN 0 "tac") tm

1198+ elab ist toplevel ERHS [] (sMN 0 "tac") tm

1176 when autoSolve solveAll

1199 when autoSolve solveAll

1177 runT Compute = compute

1200 runT Compute = compute

1178 runT Trivial = do trivial' ist; when autoSolve solveAll

1201 runT Trivial = do trivial' ist; when autoSolve solveAll

@@ -1192,7 +1215,7 @@ runTac autoSolve ist fn tac

1192 scriptvar <- getNameFrom (sMN 0 "scriptvar" )

1215 scriptvar <- getNameFrom (sMN 0 "scriptvar" )

1193 letbind scriptvar scriptTy (Var script)

1216 letbind scriptvar scriptTy (Var script)

1194 focus script

1217 focus script

1195− elab ist toplevel False [] (sMN 0 "tac") tm

1218+ elab ist toplevel ERHS [] (sMN 0 "tac") tm

1196 (script', _) <- get_type_val (Var scriptvar)

1219 (script', _) <- get_type_val (Var scriptvar)

1197 -- now that we have the script apply

1220 -- now that we have the script apply

1198 -- it to the reflected goal and context

1221 -- it to the reflected goal and context

@@ -1225,7 +1248,7 @@ runTac autoSolve ist fn tac

1225 letbind scriptvar scriptTy (Var script)

1248 letbind scriptvar scriptTy (Var script)

1226 focus script

1249 focus script

1227 ptm <- get_term

1250 ptm <- get_term

1228− elab ist toplevel False [] (sMN 0 "tac")

1251+ elab ist toplevel ERHS [] (sMN 0 "tac")

1229 (PApp emptyFC tm [pexp (delabTy' ist [] tgoal True True)])

1252 (PApp emptyFC tm [pexp (delabTy' ist [] tgoal True True)])

1230 (script', _) <- get_type_val (Var scriptvar)

1253 (script', _) <- get_type_val (Var scriptvar)

1231 -- now that we have the script apply

1254 -- now that we have the script apply

@@ -1253,7 +1276,7 @@ runTac autoSolve ist fn tac

1253 letn <- getNameFrom (sMN 0 "letvar")

1276 letn <- getNameFrom (sMN 0 "letvar")

1254 letbind letn (Var tyn) (Var valn)

1277 letbind letn (Var tyn) (Var valn)

1255 focus valn

1278 focus valn

1256− elab ist toplevel False [] (sMN 0 "tac") v

1279+ elab ist toplevel ERHS [] (sMN 0 "tac") v

1257 (value, _) <- get_type_val (Var letn)

1280 (value, _) <- get_type_val (Var letn)

1258 ctxt <- get_context

1281 ctxt <- get_context

1259 env <- get_env

1282 env <- get_env

@@ -1267,7 +1290,7 @@ runTac autoSolve ist fn tac

1267 letn <- getNameFrom (sMN 0 "letvar")

1290 letn <- getNameFrom (sMN 0 "letvar")

1268 letbind letn (Var tyn) (Var valn)

1291 letbind letn (Var tyn) (Var valn)

1269 focus valn

1292 focus valn

1270− elab ist toplevel False [] (sMN 0 "tac") v

1293+ elab ist toplevel ERHS [] (sMN 0 "tac") v

1271 (value, _) <- get_type_val (Var letn)

1294 (value, _) <- get_type_val (Var letn)

1272 ctxt <- get_context

1295 ctxt <- get_context

1273 env <- get_env

1296 env <- get_env

src/Idris/Interactive.hs+2−1

@@ -12,6 +12,7 @@ import Idris.Core.Evaluate

12import Idris.CaseSplit

13import Idris.AbsSyntax

14import Idris.ElabDecls

15+import Idris.ElabTerm

15import Idris.Error

16import Idris.Error

16import Idris.Delaborate

17import Idris.Delaborate

17import Idris.Output

18import Idris.Output

@@ -173,7 +174,7 @@ doProofSearch h fn updatefile rec l n hints (Just depth)

173 let def = PClause fc mn (PRef fc mn) [] (body top) []

174 let def = PClause fc mn (PRef fc mn) [] (body top) []

174 newmv <- idrisCatch

175 newmv <- idrisCatch

175 (do elabDecl' EAll toplevel (PClauses fc [] mn [def])

176 (do elabDecl' EAll toplevel (PClauses fc [] mn [def])

176− (tm, ty) <- elabVal toplevel False (PRef fc mn)

177+ (tm, ty) <- elabVal toplevel ERHS (PRef fc mn)

177 ctxt <- getContext

178 ctxt <- getContext

178 i <- getIState

179 i <- getIState

179 return . flip displayS "" . renderPretty 1.0 80 $

180 return . flip displayS "" . renderPretty 1.0 80 $

src/Idris/Prover.hs+2−2

@@ -264,7 +264,7 @@ ploop fn d prompt prf e h

264 let OK env = envAtFocus (proof e)

265 ctxt' = envCtxt env ctxt

266 putIState ist { tt_ctxt = ctxt' }

267− (tm, ty) <- elabVal toplevel False t

267+ (tm, ty) <- elabVal toplevel ERHS t

268 let ppo = ppOptionIst ist

269 ty' = normaliseC ctxt [] ty

270 h = idris_outh ist

@@ -288,7 +288,7 @@ ploop fn d prompt prf e h

288 ist' = ist { tt_ctxt = ctxt' }

289 bnd = map (\x -> (fst x, False)) env

290 putIState ist'

291− (tm, ty) <- elabVal toplevel False t

291+ (tm, ty) <- elabVal toplevel ERHS t

292 let tm' = force (normaliseAll ctxt' env tm)

293 ty' = force (normaliseAll ctxt' env ty)

294 ppo = ppOption (idris_options ist')

src/Idris/REPL.hs+11−11

@@ -651,7 +651,7 @@ process h fn (ChangeDirectory f)

651 return ()

652process h fn (Eval t)

653 = withErrorReflection $ do logLvl 5 $ show t

654− (tm, ty) <- elabVal toplevel False t

654+ (tm, ty) <- elabVal toplevel ERHS t

655 ctxt <- getContext

656 let tm' = force (normaliseAll ctxt [] tm)

657 let ty' = force (normaliseAll ctxt [] ty)

@@ -681,7 +681,7 @@ process h fn (NewDefn decls) = logLvl 3 ("Defining names using these decls: " ++

681 elabClauses toplevel fc opts name (concatMap getClauses decls)

682 defineName [PClauses fc opts _ [clause]] = do

683 let pterm = getRHS clause

684− (tm,ty) <- elabVal toplevel False pterm

684+ (tm,ty) <- elabVal toplevel ERHS pterm

685 ctxt <- getContext

686 let tm' = force (normaliseAll ctxt [] tm)

687 let ty' = force (normaliseAll ctxt [] ty)

@@ -699,7 +699,7 @@ process h fn (NewDefn decls) = logLvl 3 ("Defining names using these decls: " ++

699process h fn (ExecVal t)

700 = do ctxt <- getContext

701 ist <- getIState

702− (tm, ty) <- elabVal toplevel False t

702+ (tm, ty) <- elabVal toplevel ERHS t

703-- let tm' = normaliseAll ctxt [] tm

704 let ty' = normaliseAll ctxt [] ty

705 res <- execute tm

@@ -743,7 +743,7 @@ process h fn (Check (PRef _ n))

743

744

745process h fn (Check t)

746− = do (tm, ty) <- elabVal toplevel False t

746+ = do (tm, ty) <- elabVal toplevel ERHS t

747 ctxt <- getContext

748 ist <- getIState

749 let ppo = ppOptionIst ist

@@ -838,7 +838,7 @@ process h fn (MakeLemma updatefile l n)

838process h fn (DoProofSearch updatefile rec l n hints)

839 = doProofSearch h fn updatefile rec l n hints Nothing

840process h fn (Spec t)

841− = do (tm, ty) <- elabVal toplevel False t

841+ = do (tm, ty) <- elabVal toplevel ERHS t

842 ctxt <- getContext

843 ist <- getIState

844 let tm' = simplify ctxt [] {- (idris_statics ist) -} tm

@@ -917,13 +917,13 @@ process h fn (Prove n')

917 warnTotality

918

919process h fn (HNF t)

920− = do (tm, ty) <- elabVal toplevel False t

920+ = do (tm, ty) <- elabVal toplevel ERHS t

921 ctxt <- getContext

922 ist <- getIState

923 let tm' = hnf ctxt [] tm

924 iPrintResult (show (delab ist tm'))

925process h fn (TestInline t)

926− = do (tm, ty) <- elabVal toplevel False t

926+ = do (tm, ty) <- elabVal toplevel ERHS t

927 ctxt <- getContext

928 ist <- getIState

929 let tm' = inlineTerm ist tm

@@ -932,7 +932,7 @@ process h fn (TestInline t)

932process h fn Execute

933 = idrisCatch

934 (do ist <- getIState

935− (m, _) <- elabVal toplevel False

935+ (m, _) <- elabVal toplevel ERHS

936 (PApp fc

937 (PRef fc (sUN "run__IO"))

938 [pexp $ PRef fc (sNS (sUN "main") ["Main"])])

@@ -948,7 +948,7 @@ process h fn Execute

948 (\e -> getIState >>= ihRenderError stdout . flip pprintErr e)

949 where fc = fileFC "main"

950process h fn (Compile codegen f)

951− = do (m, _) <- elabVal toplevel False

951+ = do (m, _) <- elabVal toplevel ERHS

952 (PApp fc (PRef fc (sUN "run__IO"))

953 [pexp $ PRef fc (sNS (sUN "main") ["Main"])])

954 compile codegen f m

@@ -956,7 +956,7 @@ process h fn (Compile codegen f)

956process h fn (LogLvl i) = setLogLevel i

957-- Elaborate as if LHS of a pattern (debug command)

958process h fn (Pattelab t)

959− = do (tm, ty) <- elabVal toplevel True t

959+ = do (tm, ty) <- elabVal toplevel ELHS t

960 iPrintResult $ show tm ++ "\n\n : " ++ show ty

961

962process h fn (Missing n)

@@ -1374,7 +1374,7 @@ execScript expr = do i <- getIState

1374 Failure err -> do iputStrLn $ show (fixColour c err)

1375 runIO $ exitWith (ExitFailure 1)

1376 Success term -> do ctxt <- getContext

1377− (tm, _) <- elabVal toplevel False term

1377+ (tm, _) <- elabVal toplevel ERHS term

1378 res <- execute tm

1379 runIO $ exitWith ExitSuccess

1380

test/basic001/basic001a.idrnew file+32

@@ -0,0 +1,32 @@

1+module Main

3+data RLE : Vect n Char -> Type where

4+ REnd : RLE []

5+ RChar : {xs : Vect k Char} ->

6+ (n : Nat) -> (c : Char) -> (rs : RLE xs) ->

7+ RLE (replicate (S n) c ++ xs)

9+------------

10+

11+rle : (xs : Vect n Char) -> RLE xs

12+rle [] = REnd

13+rle (x :: xs) with (rle xs)

14+ rle (x :: []) | REnd = RChar 0 x REnd

15+ rle (x :: (c :: (replicate n c ++ ys))) | (RChar n c rs) with (decEq x c)

16+ rle (x :: (x :: (replicate n x ++ ys))) | (RChar n x rs) | (Yes refl)

17+ = RChar (S n) x rs

18+ rle (x :: (c :: (replicate n c ++ ys))) | (RChar n c rs) | (No f)

19+ = RChar 0 x (RChar n c rs)

20+

21+compress : Vect n Char -> String

22+compress xs with (rle xs)

23+ compress [] | REnd = ""

24+ compress (c :: (replicate n c ++ xs1)) | (RChar n c rs)

25+ = show (the Integer (cast (S n))) ++

26+ strCons c (compress xs1)

27+

28+compressString : String -> String

29+compressString xs = compress (fromList (unpack xs))

30+

31+main : IO ()

32+main = putStrLn (compressString "foooobaaaarbaaaz")

test/basic001/expected+1

@@ -1 +1,2 @@

11f4o1b4a1r1b3a1z

2+1f4o1b4a1r1b3a1z

test/basic001/run+3−1

@@ -1,4 +1,6 @@

1#!/usr/bin/env bash

2idris $@ reg005.idr -o reg005

3+idris $@ basic001a.idr -o basic001a

3./reg005

4./reg005

5+./basic001a

4−rm -f reg005 *.ibc

6+rm -f reg005 basic001a *.ibc

test/error003/expected+1−1

@@ -1,2 +1,2 @@

1ErrorReflection.idr:67:5:When elaborating right hand side of bad:

2−DSL type error: (t(503) => t'(504)) doesn't match ()

2+DSL type error: (t(502) => t'(503)) doesn't match ()

test/proof007/expected+2−1

@@ -1 +1,2 @@

1−No such variable sadgjhsag

1+DefaultArgUnknownName.idr:3:18:When elaborating type of DefaultArgUnknownName.funWithBadDefArg:

2+Can't infer type for sadgjhsag

test/reg003/expected+1−1

@@ -1,2 +1,2 @@

1−reg003a.idr:4:20:When elaborating constructor Main.ECons:

1+reg003a.idr:4:11:When elaborating type of Main.ECons:

2No such variable OddList

test/reg034/expected+6−6

@@ -1,24 +1,24 @@

1reg034.idr:6:5:When elaborating left hand side of bar:

2When elaborating an application of main.bar:

3 Can't unify

4− [92mlength[0m [95mys[0m [94m=[0m [92mlength[0m [95mys[0m

4+ [92mlength[0m ys [94m=[0m [92mlength[0m ys

5 with

6− [92mlength[0m [95mxs[0m [94m=[0m [92mlength[0m [95mys[0m

6+ [92mlength[0m [95mxs[0m [94m=[0m [92mlength[0m ys

8 Specifically:

9 Can't unify

10− [92mlength[0m [95mys[0m

10+ [92mlength[0m ys

11 with

12 [92mlength[0m [95mxs[0m

13reg034.idr:9:5:When elaborating left hand side of foo:

14When elaborating an application of main.foo:

15 Can't unify

16− [95mf[0m [95my[0m [94m=[0m [95mf[0m [95my[0m

16+ [95mf[0m y [94m=[0m [95mf[0m y

17 with

18− [95mf[0m [95mx[0m [94m=[0m [95mf[0m [95my[0m

18+ [95mf[0m [95mx[0m [94m=[0m [95mf[0m y

20 Specifically:

21 Can't unify

22− [95mf[0m [95my[0m

22+ [95mf[0m y

23 with

24 [95mf[0m [95mx[0m