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

src/Core/Elaborate.hs+18−7

compare with master

unifiedsplit

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

290 env <- get_env

291 -- let claims = getArgs ty imps

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

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

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

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

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

296 let n = length (filter not imps)

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

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

302 return claims

303 where

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

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

305+ do let t = rebind hs t_in

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

306+ n <- unique_hole (mkMN n')

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

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

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

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

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

308 claim n (forget t)

310 claim n (forget t)

309 when i (movelast n)

311 when i (movelast n)

310− mkClaims sc' is (n : claims)

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

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

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

312− mkClaims _ _ _

314+ mkClaims _ _ _ _

313 | Var n <- fn

315 | Var n <- fn

314 = do ctxt <- get_context

316 = do ctxt <- get_context

315 case lookupTy Nothing n ctxt of

317 case lookupTy Nothing n ctxt of

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

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

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

325 mkMN (NS n xs) = NS (mkMN n) xs

327 mkMN (NS n xs) = NS (mkMN n) xs

326

328

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+

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

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

328apply fn imps =

337apply fn imps =

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

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

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

343 unified p

352 unified p

344 let unify = dropGiven dont hs

353 let unify = dropGiven dont hs

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

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

355+ ptm <- get_term

346 end_unify

356 end_unify

357+ ptm <- get_term

347 return (map (updateUnify unify) args)

358 return (map (updateUnify unify) args)

348 where updateUnify hs n = case lookup n hs of

359 where updateUnify hs n = case lookup n hs of

349 Just (P _ t _) -> t

360 Just (P _ t _) -> t

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

410 focus n; elaboration; elabClaims failed r xs

421 focus n; elaboration; elabClaims failed r xs

411

422

412 mkMN n@(MN _ _) = n

423 mkMN n@(MN _ _) = n

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

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

414 mkMN (NS n ns) = NS (mkMN n) ns

425 mkMN (NS n ns) = NS (mkMN n) ns

415

426

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

427simple_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' =

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

394 _ -> normalise ctxt env t

395 case t' of

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

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

397+ 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'))

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

398 _ -> fail "Nothing to introduce"

399 _ -> fail "Nothing to introduce"

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

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

400

401

src/Core/TT.hs+9−1

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

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

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

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

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

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

524pToV' n i t = t

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

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

628 | otherwise = n

629

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+

630nextName (NS x s) = NS (nextName x) s

638nextName (NS x s) = NS (nextName x) s

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

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

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

640nextName (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

64 chk env (RApp f a)

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

66 (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

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

69+ _ -> uniqueBinders (map fst env)

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

70+ $ normalise ctxt env fty

70 case fty' of

71 case fty' of

71 Bind x (Pi s) t ->

72 Bind x (Pi s) t ->

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

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

72 do convertsC ctxt env aty s

75 do convertsC ctxt env aty s

73 -- let apty = normalise initContext env

76 -- let apty = normalise initContext env

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

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

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

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

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

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

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

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

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

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

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

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

84 (renameBinders (i+1) t)

88 (renameBinders (i+1) t)

85 renameBinders i sc = sc

89 renameBinders i sc = sc

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

107 let Set su = normalise ctxt env st

111 let Set su = normalise ctxt env st

108 let Set tu = normalise ctxt env tt

112 let Set tu = normalise ctxt env tt

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

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

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

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

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

111 chk env (RBind n b sc)

116 chk env (RBind n b sc)

112 = do b' <- checkBinder b

117 = do b' <- checkBinder b

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

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

src/Core/Unify.hs+3−3

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

24

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

26 Injs, Fails)

27−unify ctxt env topx topy

27+unify ctxt env topx topy =

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

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

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

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

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

30 _ ->

31 _ ->

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

32 let topxn = normalise ctxt env topx

33 topyn = normalise ctxt env topy in

34-- 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

1028 checkRpts (LeftErr x) = Left x

1029

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

1031−substMatches [] t = t

1031+substMatches ms = substMatchesShadow ms []

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

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)

1033

1037

1034substMatch :: Name -> PTerm -> PTerm -> PTerm

1038substMatch :: Name -> PTerm -> PTerm -> PTerm

1035−substMatch n tm t = sm t where

1039+substMatch n = substMatchShadow n []

1040+

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

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

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

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

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

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

1038− sm (PPi p x t sc) = PPi p x (sm t) (sm 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)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1047− sm x = x

1059+ sm xs x = x

1048

1060

1049shadow :: Name -> Name -> PTerm -> PTerm

1061shadow :: Name -> Name -> PTerm -> PTerm

1050shadow n n' t = sm t where

1062shadow 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

808 let ns = case n of

809 NS n ns' -> ns'

810 _ -> []

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

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

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

812− let t' = substMatches ips t in

818+ let t' = substMatchesShadow ips pnames t in

813− (decorate ns iname n,

819+ (decorate ns iname n,

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

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

815 (class_methods ci)

821 (class_methods ci)

816 logLvl 3 (show (mtys, ips))

822 logLvl 3 (show (mtys, ips))

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

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

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

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

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

823 let wb = wbTys ++ wbVals

829 let wb = wbTys ++ wbVals

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

830 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

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

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

831 show (concat (nub wparams))

832 show (concat (nub wparams))

832 let lhs = case concat (nub wparams) of

833 let lhs = case concat (nub wparams) of

src/Idris/ElabTerm.hs+6−2

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

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

181 = do -- n' <- unique_hole n

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

183+ ptm <- get_term

184+ attack; intro (Just n);

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

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

186+ elabE (True, a) sc; solve

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

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

185 repN _ _ t = t

188 repN _ _ t = t

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

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

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

270

273

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

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

272 = erun fc $

275 = erun fc $

276+ do ptm <- get_term

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

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

274 solve

278 solve

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

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

276 movelast h

280 movelast h