3034fb6 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Remove argument ordering hack in elaborator

This used to be needed because the elaborator wasn't good at going back and patching up things that didn't work right, but now it just gets in the way and causes all sorts of other problems. This tidies up elaboration/unification a bit more.

commit3034fb619c020975e446160196fb4f703899e167 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 17 May 2015, 00:43 (11 years ago) parentf79455e

13 files changed+88−79

compare with master

unifiedsplit

idris.cabal+3 libs/effects/Effects.idr+13−5 src/Idris/Core/Elaborate.hs+3−3 src/Idris/Core/ProofState.hs+29−10 src/Idris/Core/Unify.hs+2−1 src/Idris/Elab/Term.hs+6−49 src/Idris/ProofSearch.hs+13−4 test/effects001/test021.idr+1−1 test/proof010/proof010.idr−2 test/reg054/expected+6−4 test/reg064/expected test/reg064/reg064.idr+9 test/reg064/run+3

idris.cabal+3

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

311311 test/reg063/run

312312 test/reg063/*.idr

313313 test/reg063/expected

314+ test/reg064/run

315+ test/reg064/*.idr

316+ test/reg064/expected

314317

315318 test/basic001/run

316319 test/basic001/*.idr

libs/effects/Effects.idr+13−5

@@ -314,9 +314,11 @@ lift e {prf} = liftP prf e

314314||| implicit and initialised automatically.

315315|||

316316||| @prog The effectful program to run.

317−run : Applicative m => {default MkDefaultEnv env : Env m xs}

318− -> (prog : EffM m a xs xs') -> m a

319−run {env} prog = eff env prog (\r, env => pure r)

317+%no_implicit

318+run : Applicative m =>

319+ (prog : EffM m a xs xs') -> {default MkDefaultEnv env : Env m xs} ->

320+ m a

321+run prog {env} = eff env prog (\r, env => pure r)

320322

321323||| Run an effectful program in the identity context.

322324|||

@@ -324,8 +326,10 @@ run {env} prog = eff env prog (\r, env => pure r)

324326||| The `env` argument is implicit and initialised automatically.

325327|||

326328||| @prog The effectful program to run.

327−runPure : {default MkDefaultEnv env : Env id xs} -> (prog : EffM id a xs xs') -> a

328−runPure {env} prog = eff env prog (\r, env => r)

329+%no_implicit

330+runPure : (prog : EffM id a xs xs') ->

331+ {default MkDefaultEnv env : Env id xs} -> a

332+runPure prog {env} = eff env prog (\r, env => r)

329333

330334||| Run an effectful program in a given context `m` with a default value for the environment.

331335|||

@@ -333,6 +337,7 @@ runPure {env} prog = eff env prog (\r, env => r)

333337|||

334338||| @env The environment to use.

335339||| @prog The effectful program to run.

340+%no_implicit

336341runInit : Applicative m => (env : Env m xs) -> (prog : EffM m a xs xs') -> m a

337342runInit env prog = eff env prog (\r, env => pure r)

338343

@@ -342,12 +347,15 @@ runInit env prog = eff env prog (\r, env => pure r)

342347|||

343348||| @env The environment to use.

344349||| @prog The effectful program to run.

350+%no_implicit

345351runPureInit : (env : Env id xs) -> (prog : EffM id a xs xs') -> a

346352runPureInit env prog = eff env prog (\r, env => r)

347353

354+%no_implicit

348355runWith : (a -> m a) -> Env m xs -> EffM m a xs xs' -> m a

349356runWith inj env prog = eff env prog (\r, env => inj r)

350357

358+%no_implicit

351359runEnv : Applicative m => Env m xs -> EffM m a xs xs' ->

352360 m (x : a ** Env m (xs' x))

353361runEnv env prog = eff env prog (\r, env => pure (r ** env))

src/Idris/Core/Elaborate.hs+3−3

@@ -566,12 +566,12 @@ apply' fillt fn imps =

566566 let dont = if null imps

567567 then head hs : dontunify p

568568 else getNonUnify (head hs : dontunify p) imps args

569− let (n, hunis) = -- trace ("AVOID UNIFY: " ++ show (fn, dont) ++ "\n" ++ show ptm) $

569+ let (n, hunis) = -- trace ("AVOID UNIFY: " ++ show (fn, dont)) $

570570 unified p

571571 let unify = -- trace ("Not done " ++ show hs) $

572572 dropGiven dont hunis hs

573− let notunify = -- trace ("Not done " ++ show hs) $

574− keepGiven dont hunis hs

573+ let notunify = -- trace ("Not done " ++ show (hs, hunis)) $

574+ keepGiven dont hunis hs

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

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

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

src/Idris/Core/ProofState.hs+29−10

@@ -871,6 +871,9 @@ updateError ns (CantUnify b (l,lp) (r,rp) e xs sc)

871871 (updateSolvedTerm ns r, fmap (updateProv ns) rp) (updateError ns e) xs sc

872872updateError ns e = e

873873

874+updateRes ns [] = []

875+updateRes ns ((x, t) : ts) = (x, updateSolvedTerm ns t) : updateRes ns ts

876+

874877solveInProblems x val [] = []

875878solveInProblems x val ((l, r, env, err) : ps)

876879 = ((psubst x val l, psubst x val r,

@@ -898,7 +901,15 @@ getProvenance _ = (Nothing, Nothing)

898901updateProblems :: ProofState -> [(Name, TT Name)] -> Fails

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

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

901−updateProblems ps updates probs = up updates probs where

904+updateProblems ps updates probs = rec 10 updates probs

905+ where

906+ -- keep trying if we make progress, but not too many times...

907+ rec 0 us fs = (us, fs)

908+ rec n us fs = case up us [] fs of

909+ res@(_, []) -> res

910+ res@(us', _) | length us' == length us -> res

911+ (us', fs') -> rec (n - 1) us' fs'

912+

902913 hs = holes ps

903914 inj = injective ps

904915 ctxt = context ps

@@ -906,8 +917,8 @@ updateProblems ps updates probs = up updates probs where

906917 usupp = map fst (notunified ps)

907918 dont = dontunify ps

908919

909− up ns [] = (ns, [])

910− up ns (prob@(x, y, ready, env, err, while, um) : ps) =

920+ up ns acc [] = (ns, map (updateNs ns) (reverse acc))

921+ up ns acc (prob@(x, y, ready, env, err, while, um) : ps) =

911922 let (x', newx) = updateSolvedTerm' ns x

912923 (y', newy) = updateSolvedTerm' ns y

913924 (lp, rp) = getProvenance err

@@ -918,13 +929,17 @@ updateProblems ps updates probs = up updates probs where

918929 case unify ctxt env' (x', lp) (y', rp) inj hs usupp while of

919930 OK (v, []) -> traceWhen ulog ("DID " ++ show (x',y',ready,v,dont)) $

920931 let v' = filter (\(n, _) -> n `notElem` dont) v in

921− up (ns ++ v') ps

932+ up (ns ++ v') acc ps

922933 e -> -- trace ("FAILED " ++ show (x',y',ready,e)) $

923− let (ns', ps') = up ns ps in

924− (ns', (x',y', False, env',err', while, um) : ps')

934+ up ns ((x',y',False,env',err',while,um) : acc) ps

925935 else -- trace ("SKIPPING " ++ show (x,y,ready)) $

926− let (ns', ps') = up ns ps in

927− (ns', (x',y', False, env',err', while, um) : ps')

936+ up ns ((x',y', False, env',err', while, um) : acc) ps

937+

938+ updateNs ns (x, y, t, env, err, fc, fa)

939+ = let (x', newx) = updateSolvedTerm' ns x

940+ (y', newy) = updateSolvedTerm' ns y in

941+ (x', y', newx || newy,

942+ updateEnv ns env, updateError ns err, fc, fa)

928943

929944-- attempt to solve remaining problems with match_unify

930945matchProblems :: Bool -> ProofState -> [(Name, TT Name)] -> Fails

@@ -995,7 +1010,9 @@ processTactic UnifyProblems ps

9951010 previous = Just ps, plog = "",

9961011 notunified = updateNotunified ns' (notunified ps),

9971012 recents = recents ps ++ map fst ns',

1013+ dotted = filter (notIn ns') (dotted ps),

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

1015+ where notIn ns (h, _) = h `notElem` map fst ns

9991016processTactic (MatchProblems all) ps

10001017 = do let (ns', probs') = matchProblems all ps [] (problems ps)

10011018 (ns'', probs'') = matchProblems all ps ns' probs'

@@ -1022,14 +1039,16 @@ processTactic t ps

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

10231040 traceWhen (unifylog ps)

10241041 ("Updated problems after solve " ++ qshow probs' ++ "\n" ++

1025− "(Toplevel) Dropping holes: " ++ show (map fst ns')) $

1042+ "(Toplevel) Dropping holes: " ++ show (map fst ns') ++ "\n" ++

1043+ "Holes were: " ++ show (holes ps')) $

10261044 return (ps' { pterm = pterm'',

10271045 solved = Nothing,

10281046 problems = probs',

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

10301048 previous = Just ps, plog = "",

10311049 recents = recents ps' ++ map fst ns',

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

1050+ holes = holes ps' \\ (map fst ns')

1051+ }, plog ps')

10331052

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

10351054process EndUnify _

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

@@ -300,11 +300,12 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

300300 res ->

301301 let topxn = renameBindersTm env (normalise ctxt env topx)

302302 topyn = renameBindersTm env (normalise ctxt env topy) in

303−-- trace ("Unifying " ++ show (topx, topy) ++ "\n\n==>\n" ++ show (topxn, topyn) ++ "\n\n" ++ show res ++ "\n\n") $

303+-- trace ("Unifying " ++ show (topx, topy) ++ "\n\n==>\n" ++ show (topxn, topyn) ++ "\n\n") $

304304 case runStateT (un False [] topxn topyn)

305305 (UI 0 []) of

306306 OK (v, UI _ fails) ->

307307 do v' <- trimSolutions (topx, xfrom) (topy, yfrom) from env v

308+-- trace ("OK " ++ show (topxn, topyn, v, holes)) $

308309 return (map (renameBinders env) v', reverse fails)

309310-- Error e@(CantUnify False _ _ _ _ _) -> tfail e

310311 Error e -> tfail e

src/Idris/Elab/Term.hs+6−49

@@ -105,7 +105,7 @@ build ist info emode opts fn tm

105105 probs <- get_probs

106106 case probs of

107107 [] -> return ()

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

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

109109 if inf then return ()

110110 else lift (Error e)

111111

@@ -259,9 +259,10 @@ elab ist info emode opts fn tm

259259 elabE ina fc' t =

260260 do solved <- get_recents

261261 as <- get_autos

262+ hs <- get_holes

262263 -- If any of the autos use variables which have recently been solved,

263264 -- have another go at solving them now.

264− mapM_ (\(a, ns) -> if any (\n -> n `elem` solved) ns

265+ mapM_ (\(a, ns) -> if any (\n -> n `elem` solved) ns && head hs /= a

265266 then solveAuto ist fn False a

266267 else return ()) as

267268

@@ -721,9 +722,6 @@ elab ist info emode opts fn tm

721722 mapM_ checkIfInjective (map snd ns)

722723 unifyProblems -- try again with the new information,

723724 -- to help with disambiguation

724− -- Sort so that the implicit tactics and alternatives go last

725− let (ns', eargs) = unzip $

726− sortBy cmpArg (zip ns args)

727725 ulog <- getUnifyLog

728726

729727 annot <- findHighlight f

@@ -731,9 +729,9 @@ elab ist info emode opts fn tm

731729

732730 elabArgs ist (ina { e_inarg = e_inarg ina || not isinf })

733731 [] fc False f

734− (zip ns' (unmatchableArgs ++ repeat False))

732+ (zip ns (unmatchableArgs ++ repeat False))

735733 (f == sUN "Force")

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

734+ (map (\x -> getTm x) args) -- TODO: remove this False arg

737735 imp <- if (e_isfn ina) then

738736 do guess <- get_guess

739737 gty <- get_type (forget guess)

@@ -785,48 +783,6 @@ elab ist info emode opts fn tm

785783 = i : getReqImps sc

786784 getReqImps _ = []

787785

788− -- normal < alternatives < lambdas < rewrites < tactic < default tactic

789− -- reason for lambdas after alternatives is that having

790− -- the alternative resolved can help with typechecking the lambda

791− -- or the rewrite. Rewrites/tactics need as much information

792− -- as possible about the type.

793− -- FIXME: Better would be to allow alternative resolution to be

794− -- retried after more information is in.

795− cmpArg (_, x) (_, y)

796− | constraint x && not (constraint y) = LT

797− | constraint y && not (constraint x) = GT

798− | otherwise

799− = compare (conDepth 0 (getTm x) + priority x + alt x)

800− (conDepth 0 (getTm y) + priority y + alt y)

801− where alt t = case getTm t of

802− PAlternative False _ -> 5

803− PAlternative True _ -> 2

804− PTactics _ -> 150

805− PLam _ _ _ _ _ -> 3

806− PRewrite _ _ _ _ -> 4

807− PResolveTC _ -> 0

808− PHidden _ -> 150

809− _ -> 1

810−

811− constraint (PConstraint _ _ _ _) = True

812− constraint _ = False

813−

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

815− -- function (so higher score --> done later), and lots of points

816− -- if there is a PHidden since this should be unifiable.

817− -- Only relevant when on lhs

818− conDepth d t | not pattern = 0

819− conDepth d (PRef _ f) | isConName f (tt_ctxt ist) = 0

820− | otherwise = max (100 - d) 1

821− conDepth d (PApp _ f as)

822− = conDepth d f + sum (map (conDepth (d+1)) (map getTm as))

823− conDepth d (PPatvar _ _) = 0

824− conDepth d (PAlternative _ as) = maximum (map (conDepth d) as)

825− conDepth d (PHidden _) = 150

826− conDepth d Placeholder = 0

827− conDepth d (PResolveTC _) = 0

828− conDepth d t = max (100 - d) 1

829−

830786 checkIfInjective n = do

831787 env <- get_env

832788 case lookup n env of

@@ -1450,6 +1406,7 @@ findInstances ist t

14501406solveAuto :: IState -> Name -> Bool -> Name -> ElabD ()

14511407solveAuto ist fn ambigok n

14521408 = do hs <- get_holes

1409+ tm <- get_term

14531410 when (n `elem` hs) $ do

14541411 focus n

14551412 g <- goal

src/Idris/ProofSearch.hs+13−4

@@ -88,20 +88,29 @@ proofSearch False fromProver ambigok deferonfail depth elab _ nroot [fn] ist

8888proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist

8989 = do compute

9090 ty <- goal

91+ hs <- get_holes

92+ env <- get_env

93+ tm <- get_term

9194 argsok <- conArgsOK ty

9295 if ambigok || argsok then

9396 case lookupCtxt nroot (idris_tyinfodata ist) of

9497 [TISolution ts] -> findInferredTy ts

9598 _ -> psRec rec maxDepth [] S.empty

96− else autoArg (sUN "auto") -- not enough info in the type yet

99+ else do ptm <- get_term

100+ autoArg (sUN "auto") -- not enough info in the type yet

97101 where

98102 findInferredTy (t : _) = elab (delab ist (toUN t))

99103

100104 conArgsOK ty

101105 = let (f, as) = unApply ty in

102− case f of

103− P _ n _ -> case lookupCtxtExact n (idris_datatypes ist) of

104− Just t -> do rs <- mapM (conReady as) (con_names t)

106+ case f of

107+ P _ n _ ->

108+ let autohints = case lookupCtxtExact n (idris_autohints ist) of

109+ Nothing -> []

110+ Just hs -> hs in

111+ case lookupCtxtExact n (idris_datatypes ist) of

112+ Just t -> do rs <- mapM (conReady as)

113+ (autohints ++ con_names t)

105114 return (and rs)

106115 Nothing -> -- local variable, go for it

107116 return True

test/effects001/test021.idr+1−1

@@ -28,6 +28,6 @@ testFile = do True <- open "testFile" Read | False => putStrLn "Error!"

2828 putStrLn (show !(Count :- get))

2929

3030main : IO ()

31−main = run testFile

31+main = run testFile

3232

3333

test/proof010/proof010.idr−2

@@ -35,5 +35,3 @@ main : IO ()

3535main = do putStrLn $ testShow2 [(2, (+1)), (3, abs)]

3636 putStrLn $ testShow [(True, False), (False, True)]

3737

38−

39−

test/reg054/expected+6−4

@@ -4,7 +4,9 @@ When elaborating an application of constructor Main.MkInfer:

44reg054.idr:34:7:When elaborating left hand side of weird:

55When elaborating argument x to Main.weird:

66 No explicit types on left hand side: Char

7−reg054.idr:37:9:Can't convert

8− Maybe a1

9−with

10− a

7+reg054.idr:37:1-8:When elaborating left hand side of tctrick:

8+When elaborating an application of Main.tctrick:

9+ Can't unify

10+ Maybe a1 (Type of Just x)

11+ with

12+ a (Expected type)

test/reg064/expectednew file

No changes to the content.

test/reg064/reg064.idrnew file+9

@@ -0,0 +1,9 @@

1+sigmaEq2 : {A : Type} ->

2+ {P : A -> Type} ->

3+ {s1: Sigma A P} ->

4+ {s2: Sigma A P} ->

5+ getWitness s1 = getWitness s2 ->

6+ getProof s1 = getProof s2 ->

7+ s1 = s2

8+sigmaEq2 {A} {P} {s1 = (x ** prf)} {s2 = (x ** prf)} Refl Refl = Refl

test/reg064/runnew file+3

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

1+#!/usr/bin/env bash

2+idris $@ reg064.idr --check

3+rm -f *.ibc