Propagate solutions properly

samples/interp-alt.idr

@@ -0,0 +1,81 @@
+module main
+
+data Ty = TyInt | TyBool| TyFun Ty Ty
+
+interpTy : Ty -> Set
+interpTy TyInt       = Int
+interpTy TyBool      = Bool
+interpTy (TyFun s t) = interpTy s -> interpTy t
+
+using (G : Vect Ty n)
+
+  data Env : Vect Ty n -> Set where
+      Nil  : Env Nil
+      (::) : interpTy a -> Env G -> Env (a :: G)
+
+--   data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Set where
+--       stop : HasType fO (t :: G) t
+--       pop  : HasType k G t -> HasType (fS k) (u :: G) t
+
+  lookup : (i:Fin n) -> Env G -> interpTy (lookup i G)
+  lookup fO     (x :: xs) = x
+  lookup (fS i) (x :: xs) = lookup i xs
+
+  data Expr : Vect Ty n -> Ty -> Set where
+      Var : (i : Fin n) -> Expr G (lookup i G)
+      Val : (x : Int) -> Expr G TyInt
+      Lam : Expr (a :: G) t -> Expr G (TyFun a t)
+      App : Expr G (TyFun a t) -> Expr G a -> Expr G t
+      Op  : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b -> 
+            Expr G c
+      If  : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a
+      Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b
+
+  interp : Env G -> {static} Expr G t -> interpTy t
+  interp env (Var i)     = lookup i env
+  interp env (Val x)     = x
+  interp env (Lam sc)    = \x => interp (x :: env) sc
+  interp env (App f s)   = (interp env f) (interp env s)
+  interp env (Op op x y) = op (interp env x) (interp env y)
+  interp env (If x t e)  = if (interp env x) then (interp env t) else (interp env e)
+  interp env (Bind v f)  = interp env (f (interp env v))
+
+  eId : Expr G (TyFun TyInt TyInt)
+  eId = Lam (Var fO)
+
+  eTEST : Expr G (TyFun TyInt (TyFun TyInt TyInt))
+  eTEST = Lam (Lam (Var (fS fO)))
+
+  eAdd : Expr G (TyFun TyInt (TyFun TyInt TyInt))
+  eAdd = Lam (Lam (Op prim__addInt (Var fO) (Var (fS fO))))
+
+--   eDouble : Expr G (TyFun TyInt TyInt)
+--   eDouble = Lam (App (App (Lam (Lam (Op' (+) (Var fO) (Var (fS fO))))) (Var fO)) (Var fO))
+
+  eDouble : Expr G (TyFun TyInt TyInt)
+  eDouble = Lam (App (App eAdd (Var fO)) (Var fO))
+
+  app : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t
+  app = \f, a => App f a
+
+  eFac : Expr G (TyFun TyInt TyInt)
+  eFac = Lam (If (Op (==) (Var fO) (Val 0))
+                 (Val 1) (Op (*) (app eFac (Op (-) (Var fO) (Val 1))) (Var fO)))
+
+  -- Exercise elaborator: Complicated way of doing \x y => x*4 + y*2
+
+  eProg : Expr G (TyFun TyInt (TyFun TyInt TyInt))
+  eProg = Lam (Lam (Bind (App eDouble (Var (fS fO)))
+              (\x => Bind (App eDouble (Var fO))
+              (\y => Bind (App eDouble (Val x))
+              (\z => App (App eAdd (Val y)) (Val z))))))
+
+test : Int
+test = interp [] eProg 2 2
+
+testFac : Int
+testFac = interp [] eFac 4
+
+main : IO ()
+main = do print test
+          print testFac

src/Core/ProofState.hs

@@ -23,6 +23,7 @@ data ProofState = PS { thname   :: Name,
                        pterm    :: Term,   -- current proof term
                        ptype    :: Type,   -- original goal
                        unified  :: (Name, [(Name, Term)]),
+                       solved   :: Maybe (Name, Term),
                        problems :: Fails,
                        injective :: [(Term, Term, Term)],
                        deferred :: [Name], -- names we'll need to define
@@ -70,8 +71,8 @@ data Tactic = Attack
 -- Some utilites on proof and tactic states
 
 instance Show ProofState where
-    show (PS nm [] _ tm _ _ _ _ _ _ _ _ _ _) = show nm ++ ": no more goals"
-    show (PS nm (h:hs) _ tm _ _ _ _ i _ _ ctxt _ _) 
+    show (PS nm [] _ tm _ _ _ _ _ _ _ _ _ _ _) = show nm ++ ": no more goals"
+    show (PS nm (h:hs) _ tm _ _ _ _ _ i _ _ ctxt _ _) 
           = let OK g = goal (Just h) tm
                 wkenv = premises g in
                 "Other goals: " ++ show hs ++ "\n" ++
@@ -128,7 +129,8 @@ addLog str = action (\ps -> ps { plog = plog ps ++ str ++ "\n" })
 newProof :: Name -> Context -> Type -> ProofState
 newProof n ctxt ty = let h = holeName 0 
                          ty' = vToP ty in
-                         PS n [h] 1 (Bind h (Hole ty') (P Bound h ty')) ty (h, []) [] []
+                         PS n [h] 1 (Bind h (Hole ty') (P Bound h ty')) ty (h, []) 
+                            Nothing [] []
                             [] []
                             Nothing ctxt "" False
 
@@ -302,6 +304,7 @@ solve ctxt env (Bind x (Guess ty val) sc)
    | pureTerm val = do ps <- get
                        let (uh, uns) = unified ps
                        action (\ps -> ps { holes = holes ps \\ [x],
+                                           solved = Just (x, val),
                                            -- unified = (uh, uns ++ [(x, val)]),
                                            instances = instances ps \\ [x] })
                        return $ {- Bind x (Let ty val) sc -} instantiate val (pToV x sc)
@@ -461,7 +464,8 @@ processTactic Undo ps = case previous ps of
 processTactic EndUnify ps 
     = let (h, ns) = unified ps
           ns' = map (\ (n, t) -> (n, updateSolved ns t)) ns 
-          tm' = updateSolved ns' (pterm ps) 
+          tm' = -- trace ("Updating " ++ show ns' ++ " in " ++ show (pterm ps)) $
+                updateSolved ns' (pterm ps) 
           probs' = updateProblems ns' (problems ps) in
           case probs' of
             [] -> return (ps { pterm = tm', 
@@ -477,7 +481,12 @@ processTactic t ps
     = case holes ps of
         [] -> fail "Nothing to fill in."
         (h:_)  -> do ps' <- execStateT (process t h) ps
-                     return (ps' { previous = Just ps, plog = "" }, plog ps')
+                     let pterm' = case solved ps' of
+                                    Just s -> updateSolved [s] (pterm ps')
+                                    _ -> pterm ps'
+                     return (ps' { pterm = pterm',
+                                   solved = Nothing,
+                                   previous = Just ps, plog = "" }, plog ps')
 
 process :: Tactic -> Name -> StateT TState TC ()
 process EndUnify _ 

src/Idris/ElabTerm.hs

@@ -350,13 +350,16 @@ resolveTC depth fn ist
        | depth == 0 = fail $ "Can't resolve type class"
        | otherwise 
               = do t <- goal
+                   -- if there's a hole in the goal, don't even try
                    let imps = case lookupCtxtName Nothing n (idris_implicits ist) of
                                 [] -> []
                                 [args] -> map isImp (snd args) -- won't be overloaded!
                    args <- apply (Var n) imps
+                   tm <- get_term
                    mapM_ (\ (_,n) -> do focus n
                                         resolveTC (depth - 1) fn ist) 
                          (filter (\ (x, y) -> not x) (zip (map fst imps) args))
+                   -- if there's any arguments left, we've failed to resolve
                    solve
        where isImp (PImp p _ _ _) = (True, p)
              isImp arg = (False, priority arg)

src/Idris/Prover.hs

@@ -57,8 +57,8 @@ elabStep st e = do case runStateT e st of
                                    fail (pshow i a)
 
 dumpState :: IState -> ProofState -> IO ()
-dumpState ist (PS nm [] _ tm _ _ _ _ _ _ _ _ _ _) = putStrLn $ (show nm) ++ ": no more goals"
-dumpState ist ps@(PS nm (h:hs) _ tm _ _ _ problems i _ _ ctxy _ _)
+dumpState ist (PS nm [] _ tm _ _ _ _ _ _ _ _ _ _ _) = putStrLn $ (show nm) ++ ": no more goals"
+dumpState ist ps@(PS nm (h:hs) _ tm _ _ _ _ problems i _ _ ctxy _ _)
    = do let OK ty = goalAtFocus ps
         let OK env = envAtFocus ps
 --         putStrLn $ "Other goals: " ++ show hs ++ "\n"

tutorial/examples/binary.idr

@@ -34,8 +34,7 @@ intToNat x = if (x>0) then (S (intToNat (x-1))) else O
 main : IO ()
 main = do putStr "Enter a number: "
           x <- getLine
-          let b = natToBin (fromInteger (cast x))
-          print b
+          print $ natToBin (fromInteger (cast x))
 
 ---------- Proofs ----------