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

git.iko.soy/Idris-dev

Unification tweak

commit33bf2bdefae2375c79326d38104f1da1d89ae4ef authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateMon 16 Jan 2012, 10:06 (15 years ago) parent5ef6475

7 files changed+45−23

compare with master

unifiedsplit

src/Core/Elaborate.hs+7−2 src/Core/ProofState.hs+25−11 src/Core/Unify.hs+4−4 src/Idris/AbsSyntax.hs+2−2 src/Idris/ElabTerm.hs+4−1 src/Idris/Prover.hs+2−2 test/test001/test001.idr+1−1

src/Core/Elaborate.hs+7−2

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

400400 case runStateT t1 s of

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

402402 return v

403− _ -> do put s; t2

404−

403+ Error e1 -> do put s

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+

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

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

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

src/Core/ProofState.hs+25−11

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

2323 pterm :: Term, -- current proof term

2424 ptype :: Type, -- original goal

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

26+ problems :: Fails,

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

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

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

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

6970-- Some utilites on proof and tactic states

7071

7172instance Show ProofState where

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

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

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

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

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

7576 wkenv = premises g in

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

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

106107 addInj inj

107108 case fails of

108109 [] -> return u

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

110+ err ->

111+ do ps <- get

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

113+ return []

110114

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

112116getName tag = do ps <- get

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

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

125129newProof n ctxt ty = let h = holeName 0

126130 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, []) [] []

128132 [] []

129133 Nothing ctxt "" False

130134

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

437441 | Just v <- lookup n xs = v

438442updateSolved xs t = t

439443

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+

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

441451processTactic QED ps = case holes ps of

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

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

448458processTactic Undo ps = case previous ps of

449459 Nothing -> fail "Nothing to undo."

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

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

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

453− return (ps { pterm = tm',

454− unified = (h, []),

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

456− (injective ps),

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

461+processTactic EndUnify ps

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

463+ tm' = updateSolved ns (pterm ps)

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

465+ case probs' of

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

467+ unified = (h, []),

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

469+ (injective ps),

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

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

458472processTactic (Reorder n) ps

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

460474 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

33import Core.TT

44import Core.Evaluate

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

1616-- at the time

1717

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

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

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

2020

2121data UInfo = UI Int Injs Fails

2222

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

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

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

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

102102 return [] -- lift $ tfail err

103103

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

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

119119 let err = CantUnify topx topy

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

121121 s

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

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

123123 return [] -- lift $ tfail err

124124

125125 combine bnames as [] = return as

src/Idris/AbsSyntax.hs+2−2

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

945945 case lookupP Nothing n (tt_ctxt i) of

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

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

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

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

949949 [] -> 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))

951951 pri (PTrue _) = 0

952952 pri (PFalse _) = 0

953953 pri (PRefl _) = 1

src/Idris/ElabTerm.hs+4−1

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

196196 = unzip $

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

198198 (zip ns args)

199− elabArgs (ina || not isinf)

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

200200 [] 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))))

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

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

203206 solve)

src/Idris/Prover.hs+2−2

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

5454 fail (pshow i a)

5555

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

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

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

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

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

5959 = do let OK ty = goalAtFocus ps

6060 let OK env = envAtFocus ps

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

test/test001/test001.idr+1−1

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

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

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

3939 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

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

4242

4343 eId : Expr G (TyFun TyInt TyInt)