8ed343b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Remove dodgy unification hack

8ed343bEdwin Brady12 years ago

idris.cabal+3

compare with master

unifiedsplit

@@ -240,6 +240,9 @@ Extra-source-files:

240 test/reg045/run

241 test/reg045/*.idr

242 test/reg045/expected

243+ test/reg046/run

244+ test/reg046/*.idr

245+ test/reg046/expected

243

246

244 test/basic001/run

247 test/basic001/run

245 test/basic001/*.idr

248 test/basic001/*.idr

libs/neweffects/Effect/State.idr+2−2

@@ -8,8 +8,8 @@ data State : Effect where

8 Get : { a } State a

9 Put : b -> { a ==> b } State ()

11−using (m : Type -> Type)

11+-- using (m : Type -> Type)

12− instance Handler State m where

12+instance Handler State m where

13 handle st Get k = k st st

14 handle st (Put n) k = k () n

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

@@ -514,8 +514,10 @@ apply' fillt fn imps =

514 put (ES (p { dontunify = dont, unified = (n, unify),

515 notunified = notunify ++ notunified p }, a) s prev)

516 fillt (raw_apply fn (map (Var . snd) args))

517−-- trace ("Goal " ++ show g ++ "\n" ++ show (fn, imps, unify) ++ "\n" ++ show ptm) $

517+ ulog <- getUnifyLog

518+ g <- goal

519+ traceWhen ulog ("Goal " ++ show g ++ " -- when elaborating " ++ show fn) $

518− end_unify

520+ end_unify

519 return $! (map (\(argName, argHole) -> (argName, updateUnify unify argHole)) args)

521 return $! (map (\(argName, argHole) -> (argName, updateUnify unify argHole)) args)

520 where updateUnify us n = case lookup n us of

522 where updateUnify us n = case lookup n us of

521 Just (P _ t _) -> t

523 Just (P _ t _) -> t

src/Idris/Core/ProofState.hs+1−1

@@ -871,7 +871,7 @@ updateNotunified ns nu = up nu where

871

872updateProblems :: Context -> [(Name, TT Name)] -> Fails -> [Name] -> [Name]

873 -> ([(Name, TT Name)], Fails)

874−updateProblems ctxt [] ps inj holes = ([], ps)

874+-- updateProblems ctxt [] ps inj holes = ([], ps)

875updateProblems ctxt ns ps inj holes = up ns ps where

876 up ns [] = (ns, [])

877 up ns ((x, y, env, err, while, um) : ps) =

src/Idris/Core/Unify.hs+2−8

@@ -428,18 +428,12 @@ unify ctxt env topx topy inj holes from =

428

429 unApp fn bnames appx@(App fx ax) appy@(App fy ay)

430 | (injectiveApp fx && injectiveApp fy)

431− || (injectiveApp fx && rigid appx && metavarApp appy && numArgs appx == numArgs appy)

432− || (injectiveApp fy && rigid appy && metavarApp appx && numArgs appx == numArgs appy)

433 || (injectiveApp fx && metavarApp fy && ax == ay)

431 || (injectiveApp fx && metavarApp fy && ax == ay)

434 || (injectiveApp fy && metavarApp fx && ax == ay)

432 || (injectiveApp fy && metavarApp fx && ax == ay)

435 = do let (headx, _) = unApply fx

433 = do let (headx, _) = unApply fx

436 let (heady, _) = unApply fy

434 let (heady, _) = unApply fy

437 -- fail quickly if the heads are disjoint

435 -- fail quickly if the heads are disjoint

438 checkHeads headx heady

436 checkHeads headx heady

439−-- if True then -- (injective fx || injective fy || fx == fy) then

440−-- if (injective fx && metavarApp appy) ||

441−-- (injective fy && metavarApp appx) ||

442−-- (injective fx && injective fy) || fx == fy

443 uplus

437 uplus

444 (do hf <- un' True bnames fx fy

438 (do hf <- un' True bnames fx fy

445 let ax' = hnormalise hf ctxt env (substNames hf ax)

439 let ax' = hnormalise hf ctxt env (substNames hf ax)

@@ -624,9 +618,9 @@ envPos x i ((y, _) : ys) | x == y = i

624-- ASSUMPTION: inputs are in normal form

618-- ASSUMPTION: inputs are in normal form

625

619

626recoverable t@(App _ _) _

620recoverable t@(App _ _) _

627− | (P _ (UN l) _, _) <- unApply t, l == txt "Lazy" = False

621+ | (P _ (UN l) _, _) <- unApply t, l == txt "Lazy'" = False

628recoverable _ t@(App _ _)

622recoverable _ t@(App _ _)

629− | (P _ (UN l) _, _) <- unApply t, l == txt "Lazy" = False

623+ | (P _ (UN l) _, _) <- unApply t, l == txt "Lazy'" = False

630recoverable (P (DCon _ _) x _) (P (DCon _ _) y _) = x == y

624recoverable (P (DCon _ _) x _) (P (DCon _ _) y _) = x == y

631recoverable (P (TCon _ _) x _) (P (TCon _ _) y _) = x == y

625recoverable (P (TCon _ _) x _) (P (TCon _ _) y _) = x == y

632recoverable (Constant _) (P (DCon _ _) y _) = False

626recoverable (Constant _) (P (DCon _ _) y _) = False

src/Idris/ElabTerm.hs+37−23

@@ -245,12 +245,8 @@ elab ist info emode opts fn tm

245 elab' ina (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes

246 = do g <- goal; resolveTC 5 g fn ist

247 elab' ina (PResolveTC fc)

248− | True = do c <- getNameFrom (sMN 0 "class")

248+ = do c <- getNameFrom (sMN 0 "class")

249− instanceArg c

250− | otherwise = do g <- goal

251− try (resolveTC 2 g fn ist)

252− (do c <- getNameFrom (sMN 0 "class")

253− instanceArg c)

249+ instanceArg c

254 elab' ina (PRefl fc t)

250 elab' ina (PRefl fc t)

255 = elab' ina (PApp fc (PRef fc eqCon) [pimp (sMN 0 "A") Placeholder True,

251 = elab' ina (PApp fc (PRef fc eqCon) [pimp (sMN 0 "A") Placeholder True,

256 pimp (sMN 0 "x") t False])

252 pimp (sMN 0 "x") t False])

@@ -485,7 +481,9 @@ elab ist info emode opts fn tm

485 -- we can unify with them

481 -- we can unify with them

486 case lookupCtxt f (idris_classes ist) of

482 case lookupCtxt f (idris_classes ist) of

487 [] -> return ()

483 [] -> return ()

488− _ -> mapM_ setInjective (map getTm args)

484+ _ -> do mapM_ setInjective (map getTm args)

485+ -- maybe more things are solvable now

486+ unifyProblems

489 ctxt <- get_context

487 ctxt <- get_context

490 let guarded = isConName f ctxt

488 let guarded = isConName f ctxt

491-- trace ("args is " ++ show args) $ return ()

489-- trace ("args is " ++ show args) $ return ()

@@ -498,10 +496,11 @@ elab ist info emode opts fn tm

498 -- Sort so that the implicit tactics and alternatives go last

496 -- Sort so that the implicit tactics and alternatives go last

499 let (ns', eargs) = unzip $

497 let (ns', eargs) = unzip $

500 sortBy cmpArg (zip ns args)

498 sortBy cmpArg (zip ns args)

499+ ulog <- getUnifyLog

501 elabArgs ist (ina || not isinf, guarded, inty, qq)

500 elabArgs ist (ina || not isinf, guarded, inty, qq)

502 [] fc False f ns'

501 [] fc False f ns'

503 (f == sUN "Force")

502 (f == sUN "Force")

504− (map (\x -> (False, getTm x)) eargs) -- TODO: remove this False arg

503+ (map (\x -> getTm x) eargs) -- TODO: remove this False arg

505 solve

504 solve

506 ivs' <- get_instances

505 ivs' <- get_instances

507 -- Attempt to resolve any type classes which have 'complete' types,

506 -- Attempt to resolve any type classes which have 'complete' types,

@@ -525,16 +524,23 @@ elab ist info emode opts fn tm

525 -- FIXME: Better would be to allow alternative resolution to be

524 -- FIXME: Better would be to allow alternative resolution to be

526 -- retried after more information is in.

525 -- retried after more information is in.

527 cmpArg (_, x) (_, y)

526 cmpArg (_, x) (_, y)

527+ | constraint x && not (constraint y) = LT

528+ | constraint y && not (constraint x) = GT

529+ | otherwise

528 = compare (conDepth 0 (getTm x) + priority x + alt x)

530 = compare (conDepth 0 (getTm x) + priority x + alt x)

529 (conDepth 0 (getTm y) + priority y + alt y)

531 (conDepth 0 (getTm y) + priority y + alt y)

530 where alt t = case getTm t of

532 where alt t = case getTm t of

531 PAlternative False _ -> 5

533 PAlternative False _ -> 5

532− PAlternative True _ -> 1

534+ PAlternative True _ -> 2

533 PTactics _ -> 150

535 PTactics _ -> 150

534− PLam _ _ _ -> 2

536+ PLam _ _ _ -> 3

535− PRewrite _ _ _ _ -> 3

537+ PRewrite _ _ _ _ -> 4

536− _ -> 0

538+ PResolveTC _ -> 0

537−

539+ _ -> 1

540+

541+ constraint (PConstraint _ _ _ _) = True

542+ constraint _ = False

543+

538 -- Score a point for every level where there is a non-constructor

544 -- Score a point for every level where there is a non-constructor

539 -- function (so higher score --> done later)

545 -- function (so higher score --> done later)

540 -- Only relevant when on lhs

546 -- Only relevant when on lhs

@@ -546,6 +552,7 @@ elab ist info emode opts fn tm

546 conDepth d (PPatvar _ _) = 0

552 conDepth d (PPatvar _ _) = 0

547 conDepth d (PAlternative _ as) = maximum (map (conDepth d) as)

553 conDepth d (PAlternative _ as) = maximum (map (conDepth d) as)

548 conDepth d Placeholder = 0

554 conDepth d Placeholder = 0

555+ conDepth d (PResolveTC _) = 0

549 conDepth d t = max (100 - d) 1

556 conDepth d t = max (100 - d) 1

550

557

551 checkIfInjective n = do

558 checkIfInjective n = do

@@ -558,7 +565,14 @@ elab ist info emode opts fn tm

558 case lookupCtxt c (idris_classes ist) of

565 case lookupCtxt c (idris_classes ist) of

559 [] -> return ()

566 [] -> return ()

560 _ -> -- type class, set as injective

567 _ -> -- type class, set as injective

561− mapM_ setinjArg args

568+ do mapM_ setinjArg args

569+ -- maybe we can solve more things now...

570+ ulog <- getUnifyLog

571+ probs <- get_probs

572+ traceWhen ulog ("Injective now " ++ show args ++ "\n" ++ qshow probs) $

573+ unifyProblems

574+ probs <- get_probs

575+ traceWhen ulog (qshow probs) $ return ()

562 _ -> return ()

576 _ -> return ()

563

577

564 setinjArg (P _ n _) = setinj n

578 setinjArg (P _ n _) = setinj n

@@ -832,17 +846,13 @@ elab ist info emode opts fn tm

832 -> Name -- ^ Name of the function being applied

846 -> Name -- ^ Name of the function being applied

833 -> [(Name, Name)] -- ^ (Argument Name, Hole Name)

847 -> [(Name, Name)] -- ^ (Argument Name, Hole Name)

834 -> Bool -- ^ under a 'force'

848 -> Bool -- ^ under a 'force'

835− -> [(Bool, PTerm)] -- ^ (Laziness, argument)

849+ -> [PTerm] -- ^ (Laziness, argument)

836 -> ElabD ()

850 -> ElabD ()

837 elabArgs ist ina failed fc retry f [] force _ = return ()

851 elabArgs ist ina failed fc retry f [] force _ = return ()

838− elabArgs ist ina failed fc r f (n:ns) force ((_, Placeholder) : args)

852+ elabArgs ist ina failed fc r f (n:ns) force (Placeholder : args)

839 = elabArgs ist ina failed fc r f ns force args

853 = elabArgs ist ina failed fc r f ns force args

840− elabArgs ist ina failed fc r f ((argName, holeName):ns) force ((lazy, t) : args)

854+ elabArgs ist ina failed fc r f ((argName, holeName):ns) force (t : args)

841− | lazy && not pattern

842− = elabArg argName holeName (PApp bi (PRef bi (sUN "Delay"))

843− [pimp (sUN "a") Placeholder True,

844− pexp t])

845− | otherwise = elabArg argName holeName t

855+ = do elabArg argName holeName t

846 where elabArg argName holeName t =

856 where elabArg argName holeName t =

847 do now_elaborating fc f argName

857 do now_elaborating fc f argName

848 wrapErr f argName $ do

858 wrapErr f argName $ do

@@ -854,7 +864,11 @@ elab ist info emode opts fn tm

854 failed' <- -- trace (show (n, t, hs, tm)) $

864 failed' <- -- trace (show (n, t, hs, tm)) $

855 -- traceWhen (not (null cs)) (show ty ++ "\n" ++ showImp True t) $

865 -- traceWhen (not (null cs)) (show ty ++ "\n" ++ showImp True t) $

856 case holeName `elem` hs of

866 case holeName `elem` hs of

867+ True -> do focus holeName;

868+ g <- goal

869+ ulog <- getUnifyLog

870+ traceWhen ulog ("Elaborating argument " ++ show (argName, holeName, g)) $

857− True -> do focus holeName; elab ina t; return failed

871+ elab ina t; return failed

858 False -> return failed

872 False -> return failed

859 done_elaborating_arg f argName

873 done_elaborating_arg f argName

860 elabArgs ist ina failed fc r f ns force args

874 elabArgs ist ina failed fc r f ns force args

test/error003/ErrorReflection.idr+1−1

@@ -58,7 +58,7 @@ dslerr (CantUnify _ tm1 tm2 _ _ _) = do tm1' <- getTmTy tm1

58 tm2' <- getTmTy tm2

59 ty1 <- reifyTy tm1'

60 ty2 <- reifyTy tm2'

61− return [TextPart $ "DSL type error: " ++ (show ty1) ++ " doesn't match " ++(show ty2)]

61+ Just [TextPart $ "DSL type error: " ++ (show ty1) ++ " doesn't match " ++(show ty2)]

62dslerr _ = Nothing

test/reg046/expectednew file

No changes to the content.

test/reg046/reg046.idrnew file+19

@@ -0,0 +1,19 @@

1+module test

3+data MyList : (A : Type) -> Type where

4+ nil : (A : Type) -> MyList A

5+ cons : (A : Type) -> A -> MyList A -> MyList A

7+elimList : (A : Type) ->

8+ (m : MyList A -> Type) ->

9+ (f1 : m (nil A)) ->

10+ (f2 : (a : A) -> (as : MyList A) -> m as -> m (cons A a as)) ->

11+ (e : MyList A) ->

12+ m e

13+elimList A m f1 f2 (nil A) = f1

14+elimList A m f1 f2 (cons A a as) = f2 a as (elimList A m f1 f2 as)

15+

16+append : (A : Type) -> (b : MyList A) -> (c : MyList A) -> MyList A

17+append A b c = (elimList A (\ d => MyList A) c

18+ (\ d => \ e => \ f => cons A d f)

19+ b)

test/reg046/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+idris $@ reg046.idr --check

3+rm -f reg046 *.ibc