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

idris.cabal+3

compare with master

unifiedsplit

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

311 test/reg063/run

312 test/reg063/*.idr

313 test/reg063/expected

314+ test/reg064/run

315+ test/reg064/*.idr

316+ test/reg064/expected

314

317

315 test/basic001/run

318 test/basic001/run

316 test/basic001/*.idr

319 test/basic001/*.idr

libs/effects/Effects.idr+13−5

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

314||| implicit and initialised automatically.

315|||

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

317+%no_implicit

318+run : Applicative m =>

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

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

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

320+ m a

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

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

320

322

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

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

322|||

324|||

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

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

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

325|||

327|||

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

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

329+%no_implicit

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

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

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

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

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

329

333

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

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

331|||

335|||

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

333|||

337|||

334||| @env The environment to use.

338||| @env The environment to use.

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

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

340+%no_implicit

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

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

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

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

338

343

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

342|||

347|||

343||| @env The environment to use.

348||| @env The environment to use.

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

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

350+%no_implicit

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

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

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

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

347

353

354+%no_implicit

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

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

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

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

350

357

358+%no_implicit

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

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

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

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

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

361runEnv 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 =

566 let dont = if null imps

567 then head hs : dontunify p

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

570 unified p

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

572 dropGiven dont hunis hs

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

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

574− keepGiven dont hunis hs

574+ keepGiven dont hunis hs

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

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

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

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

872updateError ns e = e

873

874+updateRes ns [] = []

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

876+

874solveInProblems x val [] = []

877solveInProblems x val [] = []

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

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

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

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

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

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

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

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

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

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

903-- 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+

902 hs = holes ps

913 hs = holes ps

903 inj = injective ps

914 inj = injective ps

904 ctxt = context ps

915 ctxt = context ps

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

906 usupp = map fst (notunified ps)

917 usupp = map fst (notunified ps)

907 dont = dontunify ps

918 dont = dontunify ps

908

919

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

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

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

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

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

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

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

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

913 (lp, rp) = getProvenance err

924 (lp, rp) = getProvenance err

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

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

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

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

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

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

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

921− up (ns ++ v') ps

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

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

933 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

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

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

928

943

929-- attempt to solve remaining problems with match_unify

944-- attempt to solve remaining problems with match_unify

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

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

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

995 previous = Just ps, plog = "",

1010 previous = Just ps, plog = "",

996 notunified = updateNotunified ns' (notunified ps),

1011 notunified = updateNotunified ns' (notunified ps),

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

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

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

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

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

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

999processTactic (MatchProblems all) ps

1016processTactic (MatchProblems all) ps

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

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

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

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

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

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

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

1023 traceWhen (unifylog ps)

1040 traceWhen (unifylog ps)

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

1041 ("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')) $

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

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

1027 solved = Nothing,

1045 solved = Nothing,

1028 problems = probs',

1046 problems = probs',

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

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

1030 previous = Just ps, plog = "",

1048 previous = Just ps, plog = "",

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

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

1033

1052

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

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

1035process EndUnify _

1054process EndUnify _

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

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

300 res ->

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

302 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") $

304 case runStateT (un False [] topxn topyn)

305 (UI 0 []) of

306 OK (v, UI _ fails) ->

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

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

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

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

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

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

310 Error e -> tfail e

311 Error e -> tfail e

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

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

105 probs <- get_probs

106 case probs of

107 [] -> 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) $

109 if inf then return ()

110 else lift (Error e)

111

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

259 elabE ina fc' t =

260 do solved <- get_recents

261 as <- get_autos

262+ hs <- get_holes

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

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

263 -- have another go at solving them now.

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

265 then solveAuto ist fn False a

266 then solveAuto ist fn False a

266 else return ()) as

267 else return ()) as

267

268

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

721 mapM_ checkIfInjective (map snd ns)

722 mapM_ checkIfInjective (map snd ns)

722 unifyProblems -- try again with the new information,

723 unifyProblems -- try again with the new information,

723 -- to help with disambiguation

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

727 ulog <- getUnifyLog

725 ulog <- getUnifyLog

728

726

729 annot <- findHighlight f

727 annot <- findHighlight f

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

731

729

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

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

733 [] fc False f

731 [] fc False f

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

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

735 (f == sUN "Force")

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

737 imp <- if (e_isfn ina) then

735 imp <- if (e_isfn ina) then

738 do guess <- get_guess

736 do guess <- get_guess

739 gty <- get_type (forget guess)

737 gty <- get_type (forget guess)

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

785 = i : getReqImps sc

783 = i : getReqImps sc

786 getReqImps _ = []

784 getReqImps _ = []

787

785

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−

830 checkIfInjective n = do

786 checkIfInjective n = do

831 env <- get_env

787 env <- get_env

832 case lookup n env of

788 case lookup n env of

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

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

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

1451solveAuto ist fn ambigok n

1407solveAuto ist fn ambigok n

1452 = do hs <- get_holes

1408 = do hs <- get_holes

1409+ tm <- get_term

1453 when (n `elem` hs) $ do

1410 when (n `elem` hs) $ do

1454 focus n

1411 focus n

1455 g <- goal

1412 g <- goal

src/Idris/ProofSearch.hs+13−4

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

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

89 = do compute

90 ty <- goal

91+ hs <- get_holes

92+ env <- get_env

93+ tm <- get_term

91 argsok <- conArgsOK ty

94 argsok <- conArgsOK ty

92 if ambigok || argsok then

95 if ambigok || argsok then

93 case lookupCtxt nroot (idris_tyinfodata ist) of

96 case lookupCtxt nroot (idris_tyinfodata ist) of

94 [TISolution ts] -> findInferredTy ts

97 [TISolution ts] -> findInferredTy ts

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

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

99+ else do ptm <- get_term

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

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

97 where

101 where

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

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

99

103

100 conArgsOK ty

104 conArgsOK ty

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

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

102− case f of

106+ case f of

107+ P _ n _ ->

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

109+ Nothing -> []

110+ Just hs -> hs in

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

111+ case lookupCtxtExact n (idris_datatypes ist) of

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

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

113+ (autohints ++ con_names t)

105 return (and rs)

114 return (and rs)

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

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

107 return True

116 return True

test/effects001/test021.idr+1−1

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

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

29

30main : IO ()

31−main = run testFile

31+main = run testFile

32

33

test/proof010/proof010.idr−2

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

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

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

37

38−

39−

test/reg054/expected+6−4

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

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

5When elaborating argument x to Main.weird:

6 No explicit types on left hand side: Char

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

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

8− Maybe a1

10+ Maybe a1 (Type of Just x)

9−with

11+ with

10− a

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

9+

test/reg064/runnew file+3

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

1+#!/usr/bin/env bash

2+idris $@ reg064.idr --check

3+rm -f *.ibc