6682ebb · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Propagate solutions properly

6682ebbEdwin Brady15 years ago

samples/interp-alt.idrnew file+81

compare with master

unifiedsplit

@@ -0,0 +1,81 @@

1+module main

3+data Ty = TyInt | TyBool| TyFun Ty Ty

5+interpTy : Ty -> Set

6+interpTy TyInt = Int

7+interpTy TyBool = Bool

8+interpTy (TyFun s t) = interpTy s -> interpTy t

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,

23 pterm :: Term, -- current proof term

24 ptype :: Type, -- original goal

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

26+ solved :: Maybe (Name, Term),

26 problems :: Fails,

27 problems :: Fails,

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

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

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

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

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

70-- Some utilites on proof and tactic states

71-- Some utilites on proof and tactic states

72instance Show ProofState where

73instance Show ProofState where

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

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

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

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

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

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

76 wkenv = premises g in

77 wkenv = premises g in

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

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

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

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

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

129newProof n ctxt ty = let h = holeName 0

130newProof n ctxt ty = let h = holeName 0

130 ty' = vToP ty in

131 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 [] []

132 [] []

134 [] []

133 Nothing ctxt "" False

135 Nothing ctxt "" False

134

136

@@ -302,6 +304,7 @@ solve ctxt env (Bind x (Guess ty val) sc)

302 | pureTerm val = do ps <- get

304 | pureTerm val = do ps <- get

303 let (uh, uns) = unified ps

305 let (uh, uns) = unified ps

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

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

307+ solved = Just (x, val),

305 -- unified = (uh, uns ++ [(x, val)]),

308 -- unified = (uh, uns ++ [(x, val)]),

306 instances = instances ps \\ [x] })

309 instances = instances ps \\ [x] })

307 return $ {- Bind x (Let ty val) sc -} instantiate val (pToV x sc)

310 return $ {- Bind x (Let ty val) sc -} instantiate val (pToV x sc)

@@ -461,7 +464,8 @@ processTactic Undo ps = case previous ps of

461processTactic EndUnify ps

464processTactic EndUnify ps

462 = let (h, ns) = unified ps

465 = let (h, ns) = unified ps

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

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

467+ tm' = -- trace ("Updating " ++ show ns' ++ " in " ++ show (pterm ps)) $

464− tm' = updateSolved ns' (pterm ps)

468+ updateSolved ns' (pterm ps)

465 probs' = updateProblems ns' (problems ps) in

469 probs' = updateProblems ns' (problems ps) in

466 case probs' of

470 case probs' of

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

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

@@ -477,7 +481,12 @@ processTactic t ps

477 = case holes ps of

481 = case holes ps of

478 [] -> fail "Nothing to fill in."

482 [] -> fail "Nothing to fill in."

479 (h:_) -> do ps' <- execStateT (process t h) ps

483 (h:_) -> do ps' <- execStateT (process t h) 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,

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

489+ previous = Just ps, plog = "" }, plog ps')

481

490

482process :: Tactic -> Name -> StateT TState TC ()

491process :: Tactic -> Name -> StateT TState TC ()

483process EndUnify _

492process EndUnify _

src/Idris/ElabTerm.hs+3

@@ -350,13 +350,16 @@ resolveTC depth fn ist

350 | depth == 0 = fail $ "Can't resolve type class"

351 | otherwise

352 = do t <- goal

353+ -- if there's a hole in the goal, don't even try

353 let imps = case lookupCtxtName Nothing n (idris_implicits ist) of

354 let imps = case lookupCtxtName Nothing n (idris_implicits ist) of

354 [] -> []

355 [] -> []

355 [args] -> map isImp (snd args) -- won't be overloaded!

356 [args] -> map isImp (snd args) -- won't be overloaded!

356 args <- apply (Var n) imps

357 args <- apply (Var n) imps

358+ tm <- get_term

357 mapM_ (\ (_,n) -> do focus n

359 mapM_ (\ (_,n) -> do focus n

358 resolveTC (depth - 1) fn ist)

360 resolveTC (depth - 1) fn ist)

359 (filter (\ (x, y) -> not x) (zip (map fst imps) args))

361 (filter (\ (x, y) -> not x) (zip (map fst imps) args))

362+ -- if there's any arguments left, we've failed to resolve

360 solve

363 solve

361 where isImp (PImp p _ _ _) = (True, p)

364 where isImp (PImp p _ _ _) = (True, p)

362 isImp arg = (False, priority arg)

365 isImp arg = (False, priority arg)

src/Idris/Prover.hs+2−2

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

57 fail (pshow i a)

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

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

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

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

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

62 = do let OK ty = goalAtFocus ps

63 let OK env = envAtFocus ps

64-- 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

34main : IO ()

35main = do putStr "Enter a number: "

36 x <- getLine

37− let b = natToBin (fromInteger (cast x))

37+ print $ natToBin (fromInteger (cast x))

38− print b

40---------- Proofs ----------

39---------- Proofs ----------