1677c30 · Idris-dev · git.iko.soy

src/Core/Elaborate.hs+18−7

@@ -290,7 +290,7 @@ prepare_apply fn imps =

290290 env <- get_env

291291 -- let claims = getArgs ty imps

292292 -- claims <- mkClaims (normalise ctxt env ty) imps []

293− claims <- mkClaims (finalise ty) imps []

293+ claims <- mkClaims (finalise ty) imps [] (map fst env)

294294 ES (p, a) s prev <- get

295295 -- reverse the claims we made so that args go left to right

296296 let n = length (filter not imps)

@@ -301,15 +301,17 @@ prepare_apply fn imps =

301301-- (h : _) -> reorder_claims h

302302 return claims

303303 where

304− mkClaims (Bind n' (Pi t) sc) (i : is) claims =

305− do n <- unique_hole (mkMN n')

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

305+ do let t = rebind hs t_in

306+ n <- unique_hole (mkMN n')

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

307308 let sc' = instantiate (P Bound n t) sc

309+-- trace ("CLAIMING " ++ show (n, t) ++ " with " ++ show hs) $

308310 claim n (forget t)

309311 when i (movelast n)

310− mkClaims sc' is (n : claims)

311− mkClaims t [] claims = return (reverse claims)

312− mkClaims _ _ _

312+ mkClaims sc' is (n : claims) hs

313+ mkClaims t [] claims _ = return (reverse claims)

314+ mkClaims _ _ _ _

313315 | Var n <- fn

314316 = do ctxt <- get_context

315317 case lookupTy Nothing n ctxt of

@@ -324,6 +326,13 @@ prepare_apply fn imps =

324326 mkMN n@(UN x) = MN 1000 x

325327 mkMN (NS n xs) = NS (mkMN n) xs

326328

329+ rebind hs (Bind n t sc)

330+ | n `elem` hs = let n' = uniqueName n hs in

331+ Bind n' (fmap (rebind hs) t) (rebind (n':hs) sc)

332+ | otherwise = Bind n (fmap (rebind hs) t) (rebind (n:hs) sc)

333+ rebind hs (App f a) = App (rebind hs f) (rebind hs a)

334+ rebind hs t = t

335+

327336apply :: Raw -> [(Bool, Int)] -> Elab' aux [Name]

328337apply fn imps =

329338 do args <- prepare_apply fn (map fst imps)

@@ -343,7 +352,9 @@ apply fn imps =

343352 unified p

344353 let unify = dropGiven dont hs

345354 put (ES (p { dontunify = dont, unified = (n, unify) }, a) s prev)

355+ ptm <- get_term

346356 end_unify

357+ ptm <- get_term

347358 return (map (updateUnify unify) args)

348359 where updateUnify hs n = case lookup n hs of

349360 Just (P _ t _) -> t

@@ -410,7 +421,7 @@ apply_elab n args =

410421 focus n; elaboration; elabClaims failed r xs

411422

412423 mkMN n@(MN _ _) = n

413− mkMN n@(UN x) = MN 0 x

424+ mkMN n@(UN x) = MN 1000 x

414425 mkMN (NS n ns) = NS (mkMN n) ns

415426

416427simple_app :: Elab' aux () -> Elab' aux () -> Elab' aux ()

src/Core/ProofState.hs+3−2

@@ -393,8 +393,9 @@ intro mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

393393 x@(Bind y (Pi s) _) -> x

394394 _ -> normalise ctxt env t

395395 case t' of

396− Bind y (Pi s) t -> let t' = instantiate (P Bound n s) (pToV y t) in

397− return $ Bind n (Lam s) (Bind x (Hole t') (P Bound x t'))

396+ Bind y (Pi s) t -> -- trace ("in type " ++ show t') $

397+ let t' = instantiate (P Bound n s) (pToV y t) in

398+ return $ Bind n (Lam s) (Bind x (Hole t') (P Bound x t'))

398399 _ -> fail "Nothing to introduce"

399400intro n ctxt env _ = fail "Can't introduce here."

400401

src/Core/TT.hs+9−1

@@ -518,7 +518,7 @@ pToV' n i (Bind x b sc)

518518-- We can assume the inner scope has been pToVed already, so continue to

519519-- resolve names from the *outer* scope which may happen to have the same id.

520520-- | n == x = Bind x (fmap (pToV' n i) b) sc

521− | otherwise = Bind x (fmap (pToV' n i) b) (pToV' n (i+1) sc)

521+ | otherwise = Bind x (fmap (pToV' n i) b) (pToV' n (i+1) sc)

522522pToV' n i (App f a) = App (pToV' n i f) (pToV' n i a)

523523pToV' n i (Proj t idx) = Proj (pToV' n i t) idx

524524pToV' n i t = t

@@ -627,6 +627,14 @@ uniqueName :: Name -> [Name] -> Name

627627uniqueName n hs | n `elem` hs = uniqueName (nextName n) hs

628628 | otherwise = n

629629

630+uniqueBinders :: [Name] -> TT Name -> TT Name

631+uniqueBinders ns (Bind n b sc)

632+ = let n' = uniqueName n ns in

633+ Bind n' (fmap (uniqueBinders (n':ns)) b) (uniqueBinders ns sc)

634+uniqueBinders ns (App f a) = App (uniqueBinders ns f) (uniqueBinders ns a)

635+uniqueBinders ns t = t

636+

637+

630638nextName (NS x s) = NS (nextName x) s

631639nextName (MN i n) = MN (i+1) n

632640nextName (UN x) = let (num', nm') = span isDigit (reverse x)

src/Core/Typecheck.hs+8−3

@@ -64,11 +64,14 @@ check' holes ctxt env top = chk env top where

6464 chk env (RApp f a)

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

6666 (av, aty) <- chk env a

67− let fty' = case renameBinders 0 (finalise fty) of

67+ let fty' = case uniqueBinders (map fst env) (finalise fty) of

6868 ty@(Bind x (Pi s) t) -> ty

69− _ -> renameBinders 0 $ normalise ctxt env fty

69+ _ -> uniqueBinders (map fst env)

70+ $ normalise ctxt env fty

7071 case fty' of

7172 Bind x (Pi s) t ->

73+-- trace ("Converting " ++ show aty ++ " and " ++ show s ++

74+-- " from " ++ show fv ++ " : " ++ show fty) $

7275 do convertsC ctxt env aty s

7376 -- let apty = normalise initContext env

7477 -- (Bind x (Let aty av) t)

@@ -80,6 +83,7 @@ check' holes ctxt env top = chk env top where

8083 -- proofs, variables are locally bound with an explicit name. If we just

8184 -- make sure bound names in function types are locally unique, machine

8285 -- generated names, we'll be fine.

86+ -- NOTE: now replaced with 'uniqueBinders' above

8387 where renameBinders i (Bind x (Pi s) t) = Bind (MN i "binder") (Pi s)

8488 (renameBinders (i+1) t)

8589 renameBinders i sc = sc

@@ -107,7 +111,8 @@ check' holes ctxt env top = chk env top where

107111 let Set su = normalise ctxt env st

108112 let Set tu = normalise ctxt env tt

109113 when (not holes) $ put (v+1, ULE su (UVar v):ULE tu (UVar v):cs)

110− return (Bind n (Pi sv) (pToV n tv), Set (UVar v))

114+ return (Bind n (Pi (uniqueBinders (map fst env) sv))

115+ (pToV n tv), Set (UVar v))

111116 chk env (RBind n b sc)

112117 = do b' <- checkBinder b

113118 (scv, sct) <- chk ((n, b'):env) sc

src/Core/Unify.hs+3−3

@@ -24,11 +24,11 @@ data UInfo = UI Int Injs Fails

2424

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

2626 Injs, Fails)

27−unify ctxt env topx topy

28− = case runStateT (un' False [] topx topy) (UI 0 [] []) of

27+unify ctxt env topx topy =

28+-- trace ("Unifying " ++ show (topx, topy)) $

29+ case runStateT (un' False [] topx topy) (UI 0 [] []) of

2930 OK (v, UI _ inj []) -> return (filter notTrivial v, inj, [])

3031 _ ->

31−-- trace ("Unifying " ++ show (topx, topy)) $

3232 let topxn = normalise ctxt env topx

3333 topyn = normalise ctxt env topy in

3434-- trace ("Unifying " ++ show (topxn, topyn)) $

src/Idris/AbsSyntax.hs+27−15

@@ -1028,23 +1028,35 @@ matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where

10281028 checkRpts (LeftErr x) = Left x

10291029

10301030substMatches :: [(Name, PTerm)] -> PTerm -> PTerm

1031−substMatches [] t = t

1032−substMatches ((n,tm):ns) t = substMatch n tm (substMatches ns t)

1031+substMatches ms = substMatchesShadow ms []

1032+

1033+substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm

1034+substMatchesShadow [] shs t = t

1035+substMatchesShadow ((n,tm):ns) shs t

1036+ = substMatchShadow n shs tm (substMatchesShadow ns shs t)

10331037

10341038substMatch :: Name -> PTerm -> PTerm -> PTerm

1035−substMatch n tm t = sm t where

1036− sm (PRef _ n') | n == n' = tm

1037− sm (PLam x t sc) = PLam x (sm t) (sm sc)

1038− sm (PPi p x t sc) = PPi p x (sm t) (sm sc)

1039− sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)

1040− sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)

1041− sm (PEq f x y) = PEq f (sm x) (sm y)

1042− sm (PTyped x y) = PTyped (sm x) (sm y)

1043− sm (PPair f x y) = PPair f (sm x) (sm y)

1044− sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)

1045− sm (PAlternative a as) = PAlternative a (map sm as)

1046− sm (PHidden x) = PHidden (sm x)

1047− sm x = x

1039+substMatch n = substMatchShadow n []

1040+

1041+substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm

1042+substMatchShadow n shs tm t = sm shs t where

1043+ sm xs (PRef _ n') | n == n' = tm

1044+ sm xs (PLam x t sc) = PLam x (sm xs t) (sm xs sc)

1045+ sm xs (PPi p x t sc)

1046+ | x `elem` xs

1047+ = let x' = nextName x in

1048+ PPi p x' (sm (x':xs) (substMatch x (PRef (FC "" 0) x') t))

1049+ (sm (x':xs) (substMatch x (PRef (FC "" 0) x') sc))

1050+ | otherwise = PPi p x (sm xs t) (sm (x : xs) sc)

1051+ sm xs (PApp f x as) = PApp f (sm xs x) (map (fmap (sm xs)) as)

1052+ sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)

1053+ sm xs (PEq f x y) = PEq f (sm xs x) (sm xs y)

1054+ sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)

1055+ sm xs (PPair f x y) = PPair f (sm xs x) (sm xs y)

1056+ sm xs (PDPair f x t y) = PDPair f (sm xs x) (sm xs t) (sm xs y)

1057+ sm xs (PAlternative a as) = PAlternative a (map (sm xs) as)

1058+ sm xs (PHidden x) = PHidden (sm xs x)

1059+ sm xs x = x

10481060

10491061shadow :: Name -> Name -> PTerm -> PTerm

10501062shadow n n' t = sm t where

src/Idris/ElabDecls.hs+9−8

@@ -808,10 +808,16 @@ elabInstance info syn fc cs n ps t expn ds

808808 let ns = case n of

809809 NS n ns' -> ns'

810810 _ -> []

811+ -- get the implicit parameters that need passing through to the

812+ -- where block

813+ wparams <- mapM (\p -> case p of

814+ PApp _ _ args -> getWParams args

815+ _ -> return []) ps

816+ let pnames = map pname (concat (nub wparams))

811817 let mtys = map (\ (n, (op, t)) ->

812− let t' = substMatches ips t in

813− (decorate ns iname n,

814− op, coninsert cs t', t'))

818+ let t' = substMatchesShadow ips pnames t in

819+ (decorate ns iname n,

820+ op, coninsert cs t', t'))

815821 (class_methods ci)

816822 logLvl 3 (show (mtys, ips))

817823 let ds' = insertDefaults i iname (class_defaults ci) ns ds

@@ -822,11 +828,6 @@ elabInstance info syn fc cs n ps t expn ds

822828 let wbVals = map (decorateid (decorate ns iname)) ds'

823829 let wb = wbTys ++ wbVals

824830 logLvl 3 $ "Method types " ++ showSep "\n" (map (showDeclImp True . mkTyDecl) mtys)

825− -- get the implicit parameters that need passing through to the

826− -- where block

827− wparams <- mapM (\p -> case p of

828− PApp _ _ args -> getWParams args

829− _ -> return []) ps

830831 logLvl 3 $ "Instance is " ++ show ps ++ " implicits " ++

831832 show (concat (nub wparams))

832833 let lhs = case concat (nub wparams) of

src/Idris/ElabTerm.hs+6−2

@@ -180,7 +180,10 @@ elab ist info pattern tcgen fn tm

180180 elab' ina@(_, a) (PLam n Placeholder sc)

181181 = do -- n' <- unique_hole n

182182 -- let sc' = mapPT (repN n n') sc

183− attack; intro (Just n); elabE (True, a) sc; solve

183+ ptm <- get_term

184+ attack; intro (Just n);

185+ -- trace ("------ intro " ++ show n ++ " ---- \n" ++ show ptm)

186+ elabE (True, a) sc; solve

184187 where repN n n' (PRef fc x) | x == n' = PRef fc n'

185188 repN _ _ t = t

186189 elab' ina@(_, a) (PLam n ty sc)

@@ -270,7 +273,8 @@ elab ist info pattern tcgen fn tm

270273

271274 elab' ina@(_, a) (PApp fc f [arg])

272275 = erun fc $

273− do simple_app (elabE ina f) (elabE (True, a) (getTm arg))

276+ do ptm <- get_term

277+ simple_app (elabE ina f) (elabE (True, a) (getTm arg))

274278 solve

275279 elab' ina Placeholder = do (h : hs) <- get_holes

276280 movelast h