33bf2bd · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Unification tweak

33bf2bdEdwin Brady15 years ago

src/Core/Elaborate.hs+7−2

compare with master

unifiedsplit

@@ -400,8 +400,13 @@ try t1 t2 = do s <- get

400 case runStateT t1 s of

401 OK (v, s') -> do put s'

402 return v

403− _ -> do put s; t2

403+ Error e1 -> do put s

404−

404+ case runStateT t2 s of

405+ OK (v, s') -> do put s'; return v

406+ Error e2 -> if score e1 > score e2

407+ then lift (tfail e1)

408+ else lift (tfail e2)

409+

405-- Try a selection of tactics. Exactly one must work, all others must fail

410-- Try a selection of tactics. Exactly one must work, all others must fail

406tryAll :: [(Elab' aux a, String)] -> Elab' aux a

411tryAll :: [(Elab' aux a, String)] -> Elab' aux a

407tryAll xs = tryAll' [] (cantResolve, 0) (map fst xs)

412tryAll xs = tryAll' [] (cantResolve, 0) (map fst xs)

src/Core/ProofState.hs+25−11

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

23 pterm :: Term, -- current proof term

24 ptype :: Type, -- original goal

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

26+ problems :: Fails,

26 injective :: [(Term, Term, Term)],

27 injective :: [(Term, Term, Term)],

27 deferred :: [Name], -- names we'll need to define

28 deferred :: [Name], -- names we'll need to define

28 instances :: [Name], -- instance arguments (for type classes)

29 instances :: [Name], -- instance arguments (for type classes)

@@ -69,8 +70,8 @@ data Tactic = Attack

69-- Some utilites on proof and tactic states

70-- Some utilites on proof and tactic states

71instance Show ProofState where

72instance Show ProofState where

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

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

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

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

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

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

75 wkenv = premises g in

76 wkenv = premises g in

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

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

@@ -106,7 +107,10 @@ unify' ctxt env topx topy = do (u, inj, fails) <- lift $ unify ctxt env topx top

106 addInj inj

107 addInj inj

107 case fails of

108 case fails of

108 [] -> return u

109 [] -> return u

109− ((_,_,err):_) -> lift $ tfail err

110+ err ->

111+ do ps <- get

112+ put (ps { problems = err ++ problems ps })

113+ return []

110

114

111getName :: Monad m => String -> StateT TState m Name

115getName :: Monad m => String -> StateT TState m Name

112getName tag = do ps <- get

116getName tag = do ps <- get

@@ -124,7 +128,7 @@ addLog str = action (\ps -> ps { plog = plog ps ++ str ++ "\n" })

124newProof :: Name -> Context -> Type -> ProofState

128newProof :: Name -> Context -> Type -> ProofState

125newProof n ctxt ty = let h = holeName 0

129newProof n ctxt ty = let h = holeName 0

126 ty' = vToP ty in

130 ty' = vToP ty in

127− PS n [h] 1 (Bind h (Hole ty') (P Bound h ty')) ty (h, []) []

131+ PS n [h] 1 (Bind h (Hole ty') (P Bound h ty')) ty (h, []) [] []

128 [] []

132 [] []

129 Nothing ctxt "" False

133 Nothing ctxt "" False

130

134

@@ -437,6 +441,12 @@ updateSolved xs (P _ n _)

437 | Just v <- lookup n xs = v

441 | Just v <- lookup n xs = v

438updateSolved xs t = t

442updateSolved xs t = t

439

443

444+updateProblems ns [] = []

445+updateProblems ns ((x, y, env, err) : ps) =

446+ let x' = updateSolved ns x

447+ y' = updateSolved ns y in

448+ (x',y',env,err) : updateProblems ns ps

449+

440processTactic :: Tactic -> ProofState -> TC (ProofState, String)

450processTactic :: Tactic -> ProofState -> TC (ProofState, String)

441processTactic QED ps = case holes ps of

451processTactic QED ps = case holes ps of

442 [] -> do let tm = {- normalise (context ps) [] -} (pterm ps)

452 [] -> do let tm = {- normalise (context ps) [] -} (pterm ps)

@@ -448,13 +458,17 @@ processTactic ProofState ps = return (ps, showEnv [] (pterm ps))

448processTactic Undo ps = case previous ps of

458processTactic Undo ps = case previous ps of

449 Nothing -> fail "Nothing to undo."

459 Nothing -> fail "Nothing to undo."

450 Just pold -> return (pold, "")

460 Just pold -> return (pold, "")

451−processTactic EndUnify ps = let (h, ns) = unified ps

461+processTactic EndUnify ps

462+ = let (h, ns) = unified ps

452− tm' = updateSolved ns (pterm ps) in

463+ tm' = updateSolved ns (pterm ps)

464+ probs' = updateProblems ns (problems ps) in

465+ case probs' of

453− return (ps { pterm = tm',

466+ [] -> return (ps { pterm = tm',

454− unified = (h, []),

467+ unified = (h, []),

455− injective = map (tmap (updateSolved ns))

468+ injective = map (tmap (updateSolved ns))

456− (injective ps),

469+ (injective ps),

457− holes = holes ps \\ map fst ns }, "")

470+ holes = holes ps \\ map fst ns }, "")

471+ errs@((_,_,_,err):_) -> tfail err

458processTactic (Reorder n) ps

472processTactic (Reorder n) ps

459 = do ps' <- execStateT (tactic (Just n) reorder_claims) ps

473 = do ps' <- execStateT (tactic (Just n) reorder_claims) ps

460 return (ps' { previous = Just ps, plog = "" }, plog ps')

474 return (ps' { previous = Just ps, plog = "" }, plog ps')

src/Core/Unify.hs+4−4

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

1−module Core.Unify(unify) where

1+module Core.Unify(unify, Fails) where

3import Core.TT

4import Core.Evaluate

@@ -16,7 +16,7 @@ import Debug.Trace

16-- at the time

18type Injs = [(TT Name, TT Name, TT Name)]

19−type Fails = [(TT Name, TT Name, Err)]

19+type Fails = [(TT Name, TT Name, Env, Err)]

21data UInfo = UI Int Injs Fails

@@ -98,7 +98,7 @@ unify ctxt env topx topy

98 | x == y = do sc 1; return []

99 | otherwise = do UI s i f <- get

100 let err = CantUnify topx topy (CantUnify x y (Msg "") s) s

101− put (UI s i ((x, y, err) : f))

101+ put (UI s i ((x, y, env, err) : f))

102 return [] -- lift $ tfail err

103

104 uB bnames (Let tx vx) (Let ty vy)

@@ -119,7 +119,7 @@ unify ctxt env topx topy

119 let err = CantUnify topx topy

120 (CantUnify (binderTy x) (binderTy y) (Msg "") s)

121 s

122− put (UI s i ((binderTy x, binderTy y, err) : f))

122+ put (UI s i ((binderTy x, binderTy y, env, err) : f))

123 return [] -- lift $ tfail err

124

125 combine bnames as [] = return as

src/Idris/AbsSyntax.hs+2−2

@@ -945,9 +945,9 @@ getPriority i tm = pri tm

945 case lookupP Nothing n (tt_ctxt i) of

946 ((P (DCon _ _) _ _):_) -> 1

947 ((P (TCon _ _) _ _):_) -> 1

948− ((P Ref _ _):_) -> 3

948+ ((P Ref _ _):_) -> 4

949 [] -> 0 -- must be locally bound, if it's not an error...

950− pri (PPi _ _ x y) = max 4 (max (pri x) (pri y))

950+ pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))

951 pri (PTrue _) = 0

952 pri (PFalse _) = 0

953 pri (PRefl _) = 1

src/Idris/ElabTerm.hs+4−1

@@ -196,8 +196,11 @@ elab ist info pattern tcgen fn tm

196 = unzip $

197 sortBy (\(_,x) (_,y) -> compare (priority x) (priority y))

198 (zip ns args)

199− elabArgs (ina || not isinf)

199+ try (elabArgs (ina || not isinf)

200 [] False ns' (map (\x -> (lazyarg x, getTm x)) eargs))

201+ (elabArgs (ina || not isinf)

202+ [] False (reverse ns')

203+ (map (\x -> (lazyarg x, getTm x)) (reverse eargs))))

201-- (try (do apply2 (Var f) (map (toElab' (ina || not isinf)) args))

204-- (try (do apply2 (Var f) (map (toElab' (ina || not isinf)) args))

202 (do apply_elab f (map (toElab (ina || not isinf)) args)

205 (do apply_elab f (map (toElab (ina || not isinf)) args)

203 solve)

206 solve)

src/Idris/Prover.hs+2−2

@@ -54,8 +54,8 @@ elabStep st e = do case runStateT e st of

54 fail (pshow i a)

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

57−dumpState ist (PS nm [] _ tm _ _ _ _ _ _ _ _ _) = putStrLn $ (show nm) ++ ": no more goals"

57+dumpState ist (PS nm [] _ tm _ _ _ _ _ _ _ _ _ _) = putStrLn $ (show nm) ++ ": no more goals"

58−dumpState ist ps@(PS nm (h:hs) _ tm _ _ _ i _ _ ctxy _ _)

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

59 = do let OK ty = goalAtFocus ps

60 let OK env = envAtFocus ps

61-- putStrLn $ "Other goals: " ++ show hs ++ "\n"

test/test001/test001.idr+1−1

@@ -37,7 +37,7 @@ using (G : Vect Ty n) {

37 interp env (Lam sc) = \x => interp (x :: env) sc

38 interp env (App f s) = (interp env f) (interp env s)

39 interp env (Op op x y) = op (interp env x) (interp env y)

40− interp env (If x t e) = if (interp env x) then (interp env t) else (interp env e)

40+ interp env (If x t e) = if interp env x then interp env t else interp env e

41 interp env (Bind v f) = interp env (f (interp env v))

43 eId : Expr G (TyFun TyInt TyInt)