git.iko.soy/Idris-dev
on master help sign in
Propagate solutions properly
commit6682ebb9c6c0339cf348509c2621b19e0637da50 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateMon 16 Jan 2012, 21:57 (15 years ago) parent991c229
5 files changed+101−9
compare with master
unifiedsplit
samples/interp-alt.idr+81 src/Core/ProofState.hs+14−5 src/Idris/ElabTerm.hs+3 src/Idris/Prover.hs+2−2 tutorial/examples/binary.idr+1−2
samples/interp-alt.idrnew file+81
@@ -0,0 +1,81 @@
1+module main
2+
3+data Ty = TyInt | TyBool| TyFun Ty Ty
4+
5+interpTy : Ty -> Set
6+interpTy TyInt = Int
7+interpTy TyBool = Bool
8+interpTy (TyFun s t) = interpTy s -> interpTy t
9+
10+using (G : Vect Ty n)
11+
12+ data Env : Vect Ty n -> Set where
13+ Nil : Env Nil
14+ (::) : interpTy a -> Env G -> Env (a :: G)
15+
16+-- data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Set where
17+-- stop : HasType fO (t :: G) t
18+-- pop : HasType k G t -> HasType (fS k) (u :: G) t
19+
20+ lookup : (i:Fin n) -> Env G -> interpTy (lookup i G)
21+ lookup fO (x :: xs) = x
22+ lookup (fS i) (x :: xs) = lookup i xs
23+
24+ data Expr : Vect Ty n -> Ty -> Set where
25+ Var : (i : Fin n) -> Expr G (lookup i G)
26+ Val : (x : Int) -> Expr G TyInt
27+ Lam : Expr (a :: G) t -> Expr G (TyFun a t)
28+ App : Expr G (TyFun a t) -> Expr G a -> Expr G t
29+ Op : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->
30+ Expr G c
31+ If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a
32+ Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b
33+
34+ interp : Env G -> {static} Expr G t -> interpTy t
35+ interp env (Var i) = lookup i env
36+ interp env (Val x) = x
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)
41+ interp env (Bind v f) = interp env (f (interp env v))
42+
43+ eId : Expr G (TyFun TyInt TyInt)
44+ eId = Lam (Var fO)
45+
46+ eTEST : Expr G (TyFun TyInt (TyFun TyInt TyInt))
47+ eTEST = Lam (Lam (Var (fS fO)))
48+
49+ eAdd : Expr G (TyFun TyInt (TyFun TyInt TyInt))
50+ eAdd = Lam (Lam (Op prim__addInt (Var fO) (Var (fS fO))))
51+
52+-- eDouble : Expr G (TyFun TyInt TyInt)
53+-- eDouble = Lam (App (App (Lam (Lam (Op' (+) (Var fO) (Var (fS fO))))) (Var fO)) (Var fO))
54+
55+ eDouble : Expr G (TyFun TyInt TyInt)
56+ eDouble = Lam (App (App eAdd (Var fO)) (Var fO))
57+
58+ app : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t
59+ app = \f, a => App f a
60+
61+ eFac : Expr G (TyFun TyInt TyInt)
62+ eFac = Lam (If (Op (==) (Var fO) (Val 0))
63+ (Val 1) (Op (*) (app eFac (Op (-) (Var fO) (Val 1))) (Var fO)))
64+
65+ -- Exercise elaborator: Complicated way of doing \x y => x*4 + y*2
66+
67+ eProg : Expr G (TyFun TyInt (TyFun TyInt TyInt))
68+ eProg = Lam (Lam (Bind (App eDouble (Var (fS fO)))
69+ (\x => Bind (App eDouble (Var fO))
70+ (\y => Bind (App eDouble (Val x))
71+ (\z => App (App eAdd (Val y)) (Val z))))))
72+
73+test : Int
74+test = interp [] eProg 2 2
75+
76+testFac : Int
77+testFac = interp [] eFac 4
78+
79+main : IO ()
80+main = do print test
81+ print testFac
src/Core/ProofState.hs+14−5
@@ -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+ solved :: Maybe (Name, Term),
2627 problems :: Fails,
2728 injective :: [(Term, Term, Term)],
2829 deferred :: [Name], -- names we'll need to define
@@ -70,8 +71,8 @@ data Tactic = Attack
7071-- Some utilites on proof and tactic states
7172
7273instance Show ProofState where
73− show (PS nm [] _ tm _ _ _ _ _ _ _ _ _ _) = show nm ++ ": no more goals"
74− show (PS nm (h:hs) _ tm _ _ _ _ i _ _ ctxt _ _)
74+ show (PS nm [] _ tm _ _ _ _ _ _ _ _ _ _ _) = show nm ++ ": no more goals"
75+ show (PS nm (h:hs) _ tm _ _ _ _ _ i _ _ ctxt _ _)
7576 = let OK g = goal (Just h) tm
7677 wkenv = premises g in
7778 "Other goals: " ++ show hs ++ "\n" ++
@@ -128,7 +129,8 @@ addLog str = action (\ps -> ps { plog = plog ps ++ str ++ "\n" })
128129newProof :: Name -> Context -> Type -> ProofState
129130newProof n ctxt ty = let h = holeName 0
130131 ty' = vToP ty in
131− PS n [h] 1 (Bind h (Hole ty') (P Bound h ty')) ty (h, []) [] []
132+ PS n [h] 1 (Bind h (Hole ty') (P Bound h ty')) ty (h, [])
133+ Nothing [] []
132134 [] []
133135 Nothing ctxt "" False
134136
@@ -302,6 +304,7 @@ solve ctxt env (Bind x (Guess ty val) sc)
302304 | pureTerm val = do ps <- get
303305 let (uh, uns) = unified ps
304306 action (\ps -> ps { holes = holes ps \\ [x],
307+ solved = Just (x, val),
305308 -- unified = (uh, uns ++ [(x, val)]),
306309 instances = instances ps \\ [x] })
307310 return $ {- Bind x (Let ty val) sc -} instantiate val (pToV x sc)
@@ -461,7 +464,8 @@ processTactic Undo ps = case previous ps of
461464processTactic EndUnify ps
462465 = let (h, ns) = unified ps
463466 ns' = map (\ (n, t) -> (n, updateSolved ns t)) ns
464− tm' = updateSolved ns' (pterm ps)
467+ tm' = -- trace ("Updating " ++ show ns' ++ " in " ++ show (pterm ps)) $
468+ updateSolved ns' (pterm ps)
465469 probs' = updateProblems ns' (problems ps) in
466470 case probs' of
467471 [] -> return (ps { pterm = tm',
@@ -477,7 +481,12 @@ processTactic t ps
477481 = case holes ps of
478482 [] -> fail "Nothing to fill in."
479483 (h:_) -> do ps' <- execStateT (process t h) ps
480− return (ps' { previous = Just ps, plog = "" }, plog ps')
484+ let pterm' = case solved ps' of
485+ Just s -> updateSolved [s] (pterm ps')
486+ _ -> pterm ps'
487+ return (ps' { pterm = pterm',
488+ solved = Nothing,
489+ previous = Just ps, plog = "" }, plog ps')
481490
482491process :: Tactic -> Name -> StateT TState TC ()
483492process EndUnify _
src/Idris/ElabTerm.hs+3
@@ -350,13 +350,16 @@ resolveTC depth fn ist
350350 | depth == 0 = fail $ "Can't resolve type class"
351351 | otherwise
352352 = do t <- goal
353+ -- if there's a hole in the goal, don't even try
353354 let imps = case lookupCtxtName Nothing n (idris_implicits ist) of
354355 [] -> []
355356 [args] -> map isImp (snd args) -- won't be overloaded!
356357 args <- apply (Var n) imps
358+ tm <- get_term
357359 mapM_ (\ (_,n) -> do focus n
358360 resolveTC (depth - 1) fn ist)
359361 (filter (\ (x, y) -> not x) (zip (map fst imps) args))
362+ -- if there's any arguments left, we've failed to resolve
360363 solve
361364 where isImp (PImp p _ _ _) = (True, p)
362365 isImp arg = (False, priority arg)
src/Idris/Prover.hs+2−2
@@ -57,8 +57,8 @@ elabStep st e = do case runStateT e st of
5757 fail (pshow i a)
5858
5959dumpState :: IState -> ProofState -> IO ()
60−dumpState ist (PS nm [] _ tm _ _ _ _ _ _ _ _ _ _) = putStrLn $ (show nm) ++ ": no more goals"
61−dumpState ist ps@(PS nm (h:hs) _ tm _ _ _ problems i _ _ ctxy _ _)
60+dumpState ist (PS nm [] _ tm _ _ _ _ _ _ _ _ _ _ _) = putStrLn $ (show nm) ++ ": no more goals"
61+dumpState ist ps@(PS nm (h:hs) _ tm _ _ _ _ problems i _ _ ctxy _ _)
6262 = do let OK ty = goalAtFocus ps
6363 let OK env = envAtFocus ps
6464-- putStrLn $ "Other goals: " ++ show hs ++ "\n"
tutorial/examples/binary.idr+1−2
@@ -34,8 +34,7 @@ intToNat x = if (x>0) then (S (intToNat (x-1))) else O
3434main : IO ()
3535main = do putStr "Enter a number: "
3636 x <- getLine
37− let b = natToBin (fromInteger (cast x))
38− print b
37+ print $ natToBin (fromInteger (cast x))
3938
4039---------- Proofs ----------
4140