12f9368 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

apply and prepare_apply elaborations

commit12f9368406d4ebd9922f870eb615eee8eadab0da authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateWed 28 Sep 2011, 13:07 (15 years ago) parent546e9f5

4 files changed+94−3

compare with master

unifiedsplit

src/Core.hs+14 src/Elaborate.hs+59 src/ProofState.hs+16−3 src/ShellParser.hs+5

src/Core.hs+14

@@ -79,6 +79,10 @@ data Binder b = Lam { binderTy :: b }

7979 | PVar { binderTy :: b }

8080 deriving (Show, Eq, Functor)

8181

82+raw_apply :: Raw -> [Raw] -> Raw

83+raw_apply f [] = f

84+raw_apply f (a : as) = raw_apply (RApp f a) as

85+

8286data RawFun = RawFun { rtype :: Raw,

8387 rval :: Raw

8488 }

@@ -144,6 +148,16 @@ unApply t = ua [] t where

144148 ua args (App f a) = ua (a:args) f

145149 ua args t = (t, reverse args)

146150

151+forget :: TT Name -> Raw

152+forget tm = fe [] tm

153+ where

154+ fe env (P _ n _) = Var n

155+ fe env (V i) = Var (env !! i)

156+ fe env (Bind n b sc) = RBind n (fmap (fe env) b)

157+ (fe (n:env) sc)

158+ fe env (App f a) = RApp (fe env f) (fe env a)

159+ fe env (Set i) = RSet i

160+

147161type Term = TT Name

148162type Type = Term

149163

src/Elaborate.hs+59

@@ -13,8 +13,11 @@ module Elaborate(module Elaborate, module ProofState) where

1313import ProofState

1414import Core

1515import Evaluate

16+import Typecheck

1617

1718import Control.Monad.State

19+import Data.Char

20+import Debug.Trace

1821

1922-- I don't really want this here, but it's useful for the test shell

2023data Command = Theorem Name Raw

@@ -48,6 +51,39 @@ get_env :: Elab Env

4851get_env = do (p, _) <- get

4952 lift $ envAtFocus p

5053

54+-- get the current goal type

55+goal :: Elab Type

56+goal = do (p, _) <- get

57+ lift $ goalAtFocus p

58+

59+-- typecheck locally

60+get_type :: Raw -> Elab Type

61+get_type tm = do ctxt <- get_context

62+ env <- get_env

63+ (val, ty) <- lift $ check ctxt env tm

64+ return (vToP ty)

65+

66+-- given a desired hole name, return a unique hole name

67+unique_hole :: Name -> Elab Name

68+unique_hole n = do env <- get_env

69+ return (uniq n (map fst env))

70+ where

71+ uniq n hs | n `elem` hs = uniq (next n) hs

72+ | otherwise = n

73+

74+next (MN i n) = MN (i+1) n

75+next (UN (x:xs)) = let (num', nm') = span isDigit (reverse x)

76+ nm = reverse nm'

77+ num = readN (reverse num') in

78+ UN ((nm ++ show (num+1)) : xs)

79+ where

80+ readN "" = 0

81+ readN x = read x

82+

83+log :: String -> Elab ()

84+log str = do (p, logs) <- get

85+ put (p, logs ++ str ++ "\n")

86+

5187-- The primitives, from ProofState

5288

5389attack :: Elab ()

@@ -86,12 +122,35 @@ forall n t = processTactic' (Forall n t)

86122focus :: Name -> Elab ()

87123focus n = processTactic' (Focus n)

88124

125+movelast :: Name -> Elab ()

126+movelast n = processTactic' (MoveLast n)

127+

89128proofstate :: Elab ()

90129proofstate = processTactic' ProofState

91130

92131qed :: Elab ()

93132qed = processTactic' QED

94133

134+prepare_apply :: Raw -> [Bool] -> Elab [Name]

135+prepare_apply fn imps =

136+ do ty <- get_type fn

137+ let claims = getArgs ty imps

138+ mapM doClaim claims

139+ where

140+ getArgs (Bind n (Pi t) sc) (i : is) = (n, t, i):getArgs sc is

141+ getArgs t i = []

142+

143+ doClaim (n', t, i) =

144+ do n <- unique_hole n'

145+ claim n (forget t)

146+ when i (movelast n)

147+ return n

148+

149+apply :: Raw -> [Bool] -> Elab ()

150+apply fn imps =

151+ do args <- prepare_apply fn imps

152+ unify_fill (raw_apply fn (map Var args))

153+

95154-- Some combinators on elaborations

96155

97156-- Sequencing

src/ProofState.hs+16−3

@@ -4,7 +4,7 @@

44 proofs, and some high level commands for introducing new theorems,

55 evaluation/checking inside the proof system, etc. --}

7−module ProofState(ProofState(..), newProof, envAtFocus,

7+module ProofState(ProofState(..), newProof, envAtFocus, goalAtFocus,

88 Tactic(..), processTactic) where

1010import Typecheck

@@ -42,13 +42,14 @@ data Tactic = Attack

4242 | Intro Name

4343 | Forall Name Raw

4444 | Focus Name

45+ | MoveLast Name

4546 | ProofState

4647 | QED

47−-- Next: add 'EvalHere' and 'CheckHere' tactics

4848

4949data TacticAction = AddGoal Name -- add a new goal, solve immediately

5050 | NextGoal Name -- add a new goal, solve it after current one

5151 | FocusGoal Name -- focus on this goal next

52+ | MoveGoal Name -- move this goal to the end of the hole queue

5253 | Solved Name

5354 | AlsoSolved Name Term -- goals solved by unification

5455 | Log String

@@ -111,6 +112,11 @@ envAtFocus ps

111112 return (premises g)

112113 | otherwise = fail "No holes"

113114

115+goalAtFocus :: ProofState -> TC Type

116+goalAtFocus ps

117+ | not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps)

118+ return (binderTy (goalType g))

119+

114120goal :: Hole -> Term -> TC Goal

115121goal h tm = g [] tm where

116122 g env (Bind n b sc) | hole b && same h n = return $ GD env b

@@ -160,6 +166,10 @@ focus :: Name -> RunTactic

160166focus n ctxt env t = do action (FocusGoal n)

161167 return t

162168

169+movelast :: Name -> RunTactic

170+movelast n ctxt env t = do action (MoveGoal n)

171+ return t

172+

163173-- Hmmm. YAGNI?

164174regret :: RunTactic

165175regret = undefined

@@ -257,6 +267,7 @@ processTactic t ps

257267 goals g (AddGoal n : xs) = goals (n : g) xs

258268 goals (g:gs) (NextGoal n : xs) = goals (g : n : gs) xs

259269 goals g (FocusGoal n : xs) = goals (n : (g \\ [n])) xs

270+ goals g (MoveGoal n : xs) = goals ((g \\ [n]) ++ [n]) xs

260271 goals g (Solved n : xs) = goals (g \\ [n]) xs

261272 goals g (AlsoSolved n tm : xs) = goals (g \\ [n]) xs

262273 goals g (_ : xs) = goals g xs

@@ -265,8 +276,9 @@ processTactic t ps

265276 getSolved (AlsoSolved n tm : xs) = (n, tm) : getSolved xs

266277 getSolved (_ : xs) = getSolved xs

267278

268− updateSolved xs (Bind n b t)

279+ updateSolved xs (Bind n b@(Hole _) t)

269280 | Just v <- lookup n xs = Bind n (Let (binderTy b) v) (updateSolved xs t)

281+ updateSolved xs (Bind n b t)

270282 | otherwise = Bind n (fmap (updateSolved xs) b) (updateSolved xs t)

271283 updateSolved xs (App f a) = App (updateSolved xs f) (updateSolved xs a)

272284 updateSolved xs t = t

@@ -285,3 +297,4 @@ process t h ps = tactic (Just h) ps (context ps) (mktac t)

285297 mktac (CheckIn r) = check_in r

286298 mktac (EvalIn r) = eval_in r

287299 mktac (Focus n) = focus n

300+ mktac (MoveLast n) = movelast n

src/ShellParser.hs+5

@@ -50,6 +50,8 @@ pTactic = do reserved "attack"; return attack

5050 <|> do reserved "regret"; return regret

5151 <|> do reserved "fill"; tm <- pTerm; return (fill tm)

5252 <|> do reserved "unify"; tm <- pTerm; return (unify_fill tm)

53+ <|> do reserved "apply"; tm <- pTerm; args <- many pArgType;

54+ return (apply tm args)

5355 <|> do reserved "solve"; return solve

5456 <|> do reserved "compute"; return compute

5557 <|> do reserved "intro"; n <- iName; return (intro n)

@@ -61,4 +63,7 @@ pTactic = do reserved "attack"; return attack

6163 <|> do reserved "state"; return proofstate

6264 <|> do reserved "qed"; return qed

6365

66+pArgType :: Parser Bool

67+pArgType = do lchar '_'; return True -- implicit (machine fills in)

68+ <|> do lchar '?'; return False -- user fills in

6469