99a8a66 · Idris-dev · git.iko.soy

src/Core/Elaborate.hs+6−3

compare with master

unifiedsplit

@@ -391,10 +391,13 @@ apply fn imps =

391 else

392 map fst (filter (not.snd) (zip args (map fst imps)))

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

394− unified p

394+ unified p

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

396− dropGiven dont hunis hs

396+ dropGiven dont hunis hs

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

398+ keepGiven dont hunis hs

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

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

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

398 ptm <- get_term

401 ptm <- get_term

399 g <- goal

402 g <- goal

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

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

src/Core/Evaluate.hs+3−3

@@ -703,10 +703,10 @@ addCtxtDef n d c = let ctxt = definitions c

703 ctxt' = addDef n (d, Public, Unchecked) ctxt in

704 c { definitions = ctxt' }

705

706−addTyDecl :: Name -> Type -> Context -> Context

706+addTyDecl :: Name -> NameType -> Type -> Context -> Context

707−addTyDecl n ty uctxt

707+addTyDecl n nt ty uctxt

708 = let ctxt = definitions uctxt

709− ctxt' = addDef n (TyDecl Ref ty, Public, Unchecked) ctxt in

709+ ctxt' = addDef n (TyDecl nt ty, Public, Unchecked) ctxt in

710 uctxt { definitions = ctxt' }

711

712addDatatype :: Datatype Name -> Context -> Context

src/Core/ProofState.hs+27−7

@@ -5,7 +5,8 @@

5 evaluation/checking inside the proof system, etc. --}

6

7module Core.ProofState(ProofState(..), newProof, envAtFocus, goalAtFocus,

8− Tactic(..), Goal(..), processTactic, dropGiven) where

8+ Tactic(..), Goal(..), processTactic,

9+ dropGiven, keepGiven) where

9

10

10import Core.Typecheck

11import Core.Typecheck

11import Core.Evaluate

12import Core.Evaluate

@@ -27,6 +28,7 @@ data ProofState = PS { thname :: Name,

27 ptype :: Type, -- original goal

28 ptype :: Type, -- original goal

28 dontunify :: [Name], -- explicitly given by programmer, leave it

29 dontunify :: [Name], -- explicitly given by programmer, leave it

29 unified :: (Name, [(Name, Term)]),

30 unified :: (Name, [(Name, Term)]),

31+ notunified :: [(Name, Term)],

30 solved :: Maybe (Name, Term),

32 solved :: Maybe (Name, Term),

31 problems :: Fails,

33 problems :: Fails,

32 injective :: [Name],

34 injective :: [Name],

@@ -78,8 +80,8 @@ data Tactic = Attack

78-- Some utilites on proof and tactic states

80-- Some utilites on proof and tactic states

79

81

80instance Show ProofState where

82instance Show ProofState where

81− show (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _) = show nm ++ ": no more goals"

83+ show (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _ _) = show nm ++ ": no more goals"

82− show (PS nm (h:hs) _ _ tm _ _ _ _ _ _ i _ _ ctxt _ _)

84+ show (PS nm (h:hs) _ _ tm _ _ _ _ _ _ _ i _ _ ctxt _ _)

83 = let OK g = goal (Just h) tm

85 = let OK g = goal (Just h) tm

84 wkenv = premises g in

86 wkenv = premises g in

85 "Other goals: " ++ show hs ++ "\n" ++

87 "Other goals: " ++ show hs ++ "\n" ++

@@ -102,12 +104,12 @@ instance Show ProofState where

102 showG ps b = showEnv ps (binderTy b)

104 showG ps b = showEnv ps (binderTy b)

103

105

104instance Pretty ProofState where

106instance Pretty ProofState where

105− pretty (PS nm [] _ _ trm _ _ _ _ _ _ _ _ _ _ _ _) =

107+ pretty (PS nm [] _ _ trm _ _ _ _ _ _ _ _ _ _ _ _ _) =

106 if size nm > breakingSize then

108 if size nm > breakingSize then

107 pretty nm <> colon $$ nest nestingSize (text " no more goals.")

109 pretty nm <> colon $$ nest nestingSize (text " no more goals.")

108 else

110 else

109 pretty nm <> colon <+> text " no more goals."

111 pretty nm <> colon <+> text " no more goals."

110− pretty p@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ i _ _ ctxt _ _) =

112+ pretty p@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ _ i _ _ ctxt _ _) =

111 let OK g = goal (Just h) tm in

113 let OK g = goal (Just h) tm in

112 let wkEnv = premises g in

114 let wkEnv = premises g in

113 text "Other goals" <+> colon <+> pretty hs $$

115 text "Other goals" <+> colon <+> pretty hs $$

@@ -194,7 +196,7 @@ newProof :: Name -> Context -> Type -> ProofState

194newProof n ctxt ty = let h = holeName 0

196newProof n ctxt ty = let h = holeName 0

195 ty' = vToP ty in

197 ty' = vToP ty in

196 PS n [h] [] 1 (Bind h (Hole ty')

198 PS n [h] [] 1 (Bind h (Hole ty')

197− (P Bound h ty')) ty [] (h, [])

199+ (P Bound h ty')) ty [] (h, []) []

198 Nothing [] []

200 Nothing [] []

199 [] []

201 [] []

200 Nothing ctxt "" False

202 Nothing ctxt "" False

@@ -387,10 +389,19 @@ complete_fill ctxt env (Bind x (Guess ty val) sc) =

387 return $ Bind x (Guess ty val) sc

389 return $ Bind x (Guess ty val) sc

388complete_fill ctxt env t = fail $ "Can't complete fill at " ++ show t

390complete_fill ctxt env t = fail $ "Can't complete fill at " ++ show t

389

391

392+-- When solving something in the 'dont unify' set, we should check

393+-- that the guess we are solving it with unifies with the thing unification

394+-- found for it, if anything.

395+

390solve :: RunTactic

396solve :: RunTactic

391solve ctxt env (Bind x (Guess ty val) sc)

397solve ctxt env (Bind x (Guess ty val) sc)

392 | True = do ps <- get

398 | True = do ps <- get

393 let (uh, uns) = unified ps

399 let (uh, uns) = unified ps

400+ case lookup x (notunified ps) of

401+ Just tm -> do -- trace ("AVOIDED " ++ show (x, tm, val)) $

402+ -- return []

403+ unify' ctxt env tm val

404+ _ -> return []

394 action (\ps -> ps { holes = holes ps \\ [x],

405 action (\ps -> ps { holes = holes ps \\ [x],

395 solved = Just (x, val),

406 solved = Just (x, val),

396-- problems = solveInProblems

407-- problems = solveInProblems

@@ -565,6 +576,15 @@ dropGiven du (u@(n, _) : us) hs

565-- dropGiven du (u@(_, P a n ty) : us) | n `elem` du = dropGiven du us

576-- dropGiven du (u@(_, P a n ty) : us) | n `elem` du = dropGiven du us

566dropGiven du (u : us) hs = u : dropGiven du us hs

577dropGiven du (u : us) hs = u : dropGiven du us hs

567

578

579+keepGiven du [] hs = []

580+keepGiven du ((n, P Bound t ty) : us) hs

581+ | n `elem` du && not (t `elem` du)

582+ && n `elem` hs && t `elem` hs

583+ = keepGiven du us hs

584+keepGiven du (u@(n, _) : us) hs

585+ | n `elem` du = u : keepGiven du us hs

586+keepGiven du (u : us) hs = keepGiven du us hs

587+

568updateSolved xs x = -- trace ("Updating " ++ show xs ++ " in " ++ show x) $

588updateSolved xs x = -- trace ("Updating " ++ show xs ++ " in " ++ show x) $

569 updateSolved' xs x

589 updateSolved' xs x

570updateSolved' xs (Bind n (Hole ty) t)

590updateSolved' xs (Bind n (Hole ty) t)

@@ -618,7 +638,7 @@ processTactic EndUnify ps

618 ns' = map (\ (n, t) -> (n, updateSolved ns t)) ns

638 ns' = map (\ (n, t) -> (n, updateSolved ns t)) ns

619 (ns'', probs') = updateProblems (context ps) ns' (problems ps)

639 (ns'', probs') = updateProblems (context ps) ns' (problems ps)

620 (injective ps) (holes ps)

640 (injective ps) (holes ps)

621− tm' = -- trace ("Updating " ++ show ns' ++ "\n" ++ show ns'') $ -- ++ " in " ++ show (pterm ps)) $

641+ tm' = -- trace ("Updating " ++ show ns_in ++ "\n" ++ show ns'') $ -- ++ " in " ++ show (pterm ps)) $

622 updateSolved ns'' (pterm ps) in

642 updateSolved ns'' (pterm ps) in

623 return (ps { pterm = tm',

643 return (ps { pterm = tm',

624 unified = (h, []),

644 unified = (h, []),

src/Core/Typecheck.hs+1−1

@@ -227,7 +227,7 @@ checkProgram ctxt [] = return ctxt

227checkProgram ctxt ((n, RConst t) : xs)

228 = do (t', tt') <- trace (show n) $ check ctxt [] t

229 isType ctxt [] tt'

230− checkProgram (addTyDecl n t' ctxt) xs

230+ checkProgram (addTyDecl n Ref t' ctxt) xs

231checkProgram ctxt ((n, RFunction (RawFun ty val)) : xs)

232 = do (ty', tyt') <- trace (show n) $ check ctxt [] ty

233 (val', valt') <- check ctxt [] val

src/Core/Unify.hs+10−9

@@ -56,7 +56,7 @@ unify ctxt env topx topy dont holes =

56 injective (P (TCon _ _) _ _) = True

57 injective (App f (P _ _ _)) = injective f

58 injective (App f (Constant _)) = injective f

59− injective (App f a) = injective f && injective a

59+ injective (App f a) = injective f -- && injective a

60 injective _ = False

61

62 notP (P _ _ _) = False

@@ -133,10 +133,9 @@ unify ctxt env topx topy dont holes =

133 | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []

134

135 un' fn bnames appx@(App fx ax) appy@(App fy ay)

136− | injective fx && sameArgStruct appx appy && metavarApp appy

136+ | (injective fx && sameArgStruct appx appy && metavarApp appy)

137− || injective fy && sameArgStruct appx appy && metavarApp appx

137+ || (injective fy && sameArgStruct appx appy && metavarApp appx)

138− || injective fx && injective fy

138+ || (injective fx && injective fy)

139− || fx == fy

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

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

141 let (heady, _) = unApply fy

140 let (heady, _) = unApply fy

142 -- fail quickly if the heads are disjoint

141 -- fail quickly if the heads are disjoint

@@ -158,17 +157,19 @@ unify ctxt env topx topy dont holes =

158 hf <- un' False bnames fx' fy'

157 hf <- un' False bnames fx' fy'

159 sc 1

158 sc 1

160 combine bnames hf ha)

159 combine bnames hf ha)

161− | otherwise

160+ | otherwise =

162− = do let (headx, argsx) = unApply appx

161+ do let (headx, argsx) = unApply appx

163 let (heady, argsy) = unApply appy

162 let (heady, argsy) = unApply appy

163+ -- traceWhen (headx == heady) (show (appx, appy)) $

164 if (length argsx == length argsy &&

165− ((headx == heady) || (argsx == argsy) ||

165+ ((headx == heady && inenv headx) || (argsx == argsy) ||

166 (and (zipWith sameStruct (headx:argsx) (heady:argsy)))))

167 then

168-- (notFn headx && notFn heady))) then

169 do uf <- un' True bnames headx heady

170 unArgs uf argsx argsy

171+ else -- trace ("TMPFAIL " ++ show (appx, appy, injective appx, injective appy)) $

171− else unifyTmpFail appx appy

172+ unifyTmpFail appx appy

172 where hnormalise [] _ _ t = t

173 where hnormalise [] _ _ t = t

173 hnormalise ns ctxt env t = normalise ctxt env t

174 hnormalise ns ctxt env t = normalise ctxt env t

174 checkHeads (P (DCon _ _) x _) (P (DCon _ _) y _)

175 checkHeads (P (DCon _ _) x _) (P (DCon _ _) y _)

src/Idris/AbsSyntax.hs+8−4

@@ -222,10 +222,14 @@ addConstraints fc (v, cs)

222 let ics = zip cs (repeat fc) ++ idris_constraints i

223 putIState $ i { tt_ctxt = ctxt', idris_constraints = ics }

224

225+addDeferred = addDeferred' Ref

226+addDeferredTyCon = addDeferred' (TCon 0 0)

227+

225−addDeferred :: [(Name, Type)] -> Idris ()

228+addDeferred' :: NameType -> [(Name, Type)] -> Idris ()

229+addDeferred' nt ns

226−addDeferred ns = do mapM_ (\(n, t) -> updateContext (addTyDecl n (tidyNames [] t))) ns

230+ = do mapM_ (\(n, t) -> updateContext (addTyDecl n nt (tidyNames [] t))) ns

227− i <- getIState

231+ i <- getIState

228− putIState $ i { idris_metavars = map fst ns ++ idris_metavars i }

232+ putIState $ i { idris_metavars = map fst ns ++ idris_metavars i }

229 where tidyNames used (Bind (MN i x) b sc)

233 where tidyNames used (Bind (MN i x) b sc)

230 = let n' = uniqueName (UN x) used in

234 = let n' = uniqueName (UN x) used in

231 Bind n' b $ tidyNames (n':used) sc

235 Bind n' b $ tidyNames (n':used) sc

src/Idris/ElabDecls.hs+5−4

@@ -121,11 +121,11 @@ elabData info syn doc fc codata (PLaterdecl n t_in)

121 ((t', defer, is), log) <- tclift $ elaborate ctxt n (TType (UVal 0)) []

122 (erun fc (build i info False n t))

123 def' <- checkDef fc defer

124− addDeferred def'

124+ addDeferredTyCon def'

125 mapM_ (elabCaseBlock info) is

126 (cty, _) <- recheckC fc [] t'

127 logLvl 2 $ "---> " ++ show cty

128− updateContext (addTyDecl n cty) -- temporary, to check cons

128+ updateContext (addTyDecl n (TCon 0 0) cty) -- temporary, to check cons

129

130elabData info syn doc fc codata (PDatadecl n t_in dcons)

131 = do iLOG (show fc)

@@ -137,12 +137,12 @@ elabData info syn doc fc codata (PDatadecl n t_in dcons)

137 ((t', defer, is), log) <- tclift $ elaborate ctxt n (TType (UVal 0)) []

138 (erun fc (build i info False n t))

139 def' <- checkDef fc defer

140− addDeferred def'

140+ addDeferredTyCon def'

141 mapM_ (elabCaseBlock info) is

142 (cty, _) <- recheckC fc [] t'

143 logLvl 2 $ "---> " ++ show cty

144 -- temporary, to check cons

145− when undef $ updateContext (addTyDecl n cty)

145+ when undef $ updateContext (addTyDecl n (TCon 0 0) cty)

146 cons <- mapM (elabCon info syn n codata) dcons

147 ttag <- getName

148 i <- getIState

@@ -585,6 +585,7 @@ checkPossible info fc tcgen fname lhs_in

585 case recheck ctxt [] (forget lhs_tm) lhs_tm of

586 OK _ -> return True

587 _ -> return False

588+

588-- b <- inferredDiff fc (delab' i lhs_tm True) lhs

589-- b <- inferredDiff fc (delab' i lhs_tm True) lhs

589-- return (not b) -- then return (Just lhs_tm) else return Nothing

590-- return (not b) -- then return (Just lhs_tm) else return Nothing

590-- trace (show (delab' i lhs_tm True) ++ "\n" ++ show lhs) $ return (not b)

591-- trace (show (delab' i lhs_tm True) ++ "\n" ++ show lhs) $ return (not b)

src/Idris/ElabTerm.hs+2−1

@@ -96,9 +96,10 @@ elab :: IState -> ElabInfo -> Bool -> Bool -> Name -> PTerm ->

96 ElabD ()

97elab ist info pattern tcgen fn tm

98 = do elabE (False, False) tm -- (in argument, guarded)

99+ end_unify

99 when pattern -- convert remaining holes to pattern vars

100 when pattern -- convert remaining holes to pattern vars

100 (do update_term orderPats

101 (do update_term orderPats

101−-- tm <- get_term

102+ tm <- get_term

102 mkPat)

103 mkPat)

103 where

104 where

104 isph arg = case getTm arg of

105 isph arg = case getTm arg of

src/Idris/Prover.hs+2−2

@@ -78,9 +78,9 @@ elabStep st e = do case runStateT e st of

78 fail (pshow i a)

79

80dumpState :: IState -> ProofState -> IO ()

81−dumpState ist (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _) =

81+dumpState ist (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _ _) =

82 putStrLn . render $ pretty nm <> colon <+> text "No more goals."

83−dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ problems i _ _ ctxy _ _) = do

83+dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _) = do

84 let OK ty = goalAtFocus ps

85 let OK env = envAtFocus ps

86 putStrLn . render $

test/reg018/expected+1

@@ -1,3 +1,4 @@

1reg018a.idr:16:conat.minusCoNat is not productive

2reg018b.idr:8:A.showB is possibly not total due to recursive path A.showB

3reg018c.idr:19:CodataTest.inf is not productive

4+reg018d.idr:5:Main.pull is not total as there are missing cases

test/reg018/reg018d.idrnew file+12

@@ -0,0 +1,12 @@

1+module Main

2+

3+total

4+pull : Fin (S n) -> Vect a (S n) -> (a, Vect a n)

5+pull {n=O} _ (x :: xs) = (x, xs)

6+-- pull {n=S q} fO (Vect.(::) {n=S _} x xs) = (x, xs)

7+pull {n=S _} (fS n) (x :: xs) =

8+ let (v, vs) = pull n xs in

9+ (v, x::vs)

10+

11+main : IO ()

12+main = print (pull fO [0, 1, 2])

test/reg018/run+1

@@ -2,3 +2,4 @@

2idris $@ reg018a.idr --check

3idris $@ reg018b.idr --check

4idris $@ reg018c.idr --check

5+idris $@ reg018d.idr --check

test/test014/Resimp.idr+8−1

@@ -69,6 +69,13 @@ using (i: Fin n, gam : Vect Ty n, gam' : Vect Ty n, gam'' : Vect Ty n)

69 envUpdate (pop k) val (x :: xs) = x :: envUpdate k val xs

70 envUpdate stop _ Nil impossible

71

72+ total

73+ envUpdateVal : (p:HasType gam i a) -> (val:b) ->

74+ Env gam -> Env (update gam p (Val b))

75+ envUpdateVal stop val (x :: xs) = val :: xs

76+ envUpdateVal (pop k) val (x :: xs) = x :: envUpdateVal k val xs

77+ envUpdateVal stop _ Nil impossible

78+

72 envTail : Env (a :: gam) -> Env gam

79 envTail : Env (a :: gam) -> Env gam

73 envTail (x :: xs) = xs

80 envTail (x :: xs) = xs

74

81

@@ -121,7 +128,7 @@ using (i: Fin n, gam : Vect Ty n, gam' : Vect Ty n, gam'' : Vect Ty n)

121 (\env', scope' => k (envTail env') scope')

128 (\env', scope' => k (envTail env') scope')

122 interp env (Update method x) k

129 interp env (Update method x) k

123 = do x' <- getUpdater (method (envLookup x env))

130 = do x' <- getUpdater (method (envLookup x env))

124− k (envUpdate x x' env) (return ())

131+ k (envUpdateVal x x' env) (return ())

125 interp env (Use method x) k

132 interp env (Use method x) k

126 = do x' <- getReader (method (envLookup x env))

133 = do x' <- getReader (method (envLookup x env))

127 k env (return x')

134 k env (return x')