188dda5 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Tinkering with tactics and deferred definitions

188dda5Edwin Brady15 years ago

src/Core/Elaborate.hs+2−13

compare with master

unifiedsplit

@@ -114,19 +114,8 @@ get_deferred = do ES p _ _ <- get

114unique_hole :: Name -> Elab Name

115unique_hole n = do ES p _ _ <- get

116 env <- get_env

117− return (uniq n (holes p ++ map fst env))

117+ return (uniqueName n (holes p ++ map fst env))

118 where

119− uniq n hs | n `elem` hs = uniq (next n) hs

120− | otherwise = n

121−

122−next (MN i n) = MN (i+1) n

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

124− nm = reverse nm'

125− num = readN (reverse num') in

126− UN ((nm ++ show (num+1)) : xs)

127− where

128− readN "" = 0

129− readN x = read x

130

119

131elog :: String -> Elab ()

120elog :: String -> Elab ()

132elog str = do ES p logs prev <- get

121elog str = do ES p logs prev <- get

@@ -173,7 +162,7 @@ eval_in t = processTactic' (EvalIn t)

173check_in :: Raw -> Elab ()

162check_in :: Raw -> Elab ()

174check_in t = processTactic' (CheckIn t)

163check_in t = processTactic' (CheckIn t)

175

164

176−intro :: Name -> Elab ()

165+intro :: Maybe Name -> Elab ()

177intro n = processTactic' (Intro n)

166intro n = processTactic' (Intro n)

178

167

179forall :: Name -> Raw -> Elab ()

168forall :: Name -> Raw -> Elab ()

src/Core/ProofState.hs+9−6

@@ -47,7 +47,7 @@ data Tactic = Attack

47 | Compute

48 | EvalIn Raw

49 | CheckIn Raw

50− | Intro Name

50+ | Intro (Maybe Name)

51 | Forall Name Raw

52 | LetBind Name Raw Raw

53 | Rewrite Raw

@@ -251,9 +251,12 @@ solve ctxt env (Bind x (Guess ty val) sc)

251 | otherwise = fail "I see a hole in your solution."

252solve _ _ h = fail $ "Not a guess " ++ show h

253

254−intro :: Name -> RunTactic

254+intro :: Maybe Name -> RunTactic

255−intro n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

255+intro mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

256+ do let n = case mn of

257+ Just name -> name

258+ Nothing -> x

256− do let t' = normalise ctxt env t

259+ let t' = normalise ctxt env t

257 case t' of

260 case t' of

258 Bind y (Pi s) t -> let t' = instantiate (P Bound n s) (pToV y t) in

261 Bind y (Pi s) t -> let t' = instantiate (P Bound n s) (pToV y t) in

259 return $ Bind n (Lam s) (Bind x (Hole t') (P Bound x t'))

262 return $ Bind n (Lam s) (Bind x (Hole t') (P Bound x t'))

@@ -289,8 +292,8 @@ rewrite tm ctxt env (Bind x (Hole t) xp@(P _ x' _)) | x == x' =

289 do let p = Bind rname (Lam lt) (mkP (P Bound rname lt) r l t)

292 do let p = Bind rname (Lam lt) (mkP (P Bound rname lt) r l t)

290 let newt = mkP l r l t

293 let newt = mkP l r l t

291 let sc = forget $ (Bind x (Hole newt)

294 let sc = forget $ (Bind x (Hole newt)

292− (mkApp (P Ref (UN ["replace"]) (Set 0))

295+ (mkApp (P Ref (UN ["replace"]) (Set 0))

293− [lt, l, r, p, tmv, xp]))

296+ [lt, l, r, p, tmv, xp]))

294 (scv, sct) <- lift $ check ctxt env sc

297 (scv, sct) <- lift $ check ctxt env sc

295 return scv

298 return scv

296 _ -> fail "Not an equality type"

299 _ -> fail "Not an equality type"

src/Core/ShellParser.hs+1−1

@@ -54,7 +54,7 @@ pTactic = do reserved "attack"; return attack

54 return (discard (apply tm args))

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

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

57− <|> do reserved "intro"; n <- iName []; return (intro n)

57+ <|> do reserved "intro"; n <- iName []; return (intro (Just n))

58 <|> do reserved "forall"; n <- iName []; lchar ':'; ty <- pTerm

59 return (forall n ty)

60 <|> do reserved "arg"; n <- iName []; t <- iName []; return (arg n t)

src/Core/TT.hs+14

@@ -5,6 +5,7 @@ module Core.TT where

5import Control.Monad.State

6import Debug.Trace

7import qualified Data.Map as Map

8+import Data.Char

9{- The language has:

10{- The language has:

10 * Full dependent types

11 * Full dependent types

@@ -299,6 +300,19 @@ getArgTys :: TT n -> [(n, TT n)]

299getArgTys (Bind n (Pi t) sc) = (n, t) : getArgTys sc

300getArgTys (Bind n (Pi t) sc) = (n, t) : getArgTys sc

300getArgTys _ = []

301getArgTys _ = []

301

302

303+uniqueName :: Name -> [Name] -> Name

304+uniqueName n hs | n `elem` hs = uniqueName (nextName n) hs

305+ | otherwise = n

306+

307+nextName (MN i n) = MN (i+1) n

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

309+ nm = reverse nm'

310+ num = readN (reverse num') in

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

312+ where

313+ readN "" = 0

314+ readN x = read x

315+

302type Term = TT Name

316type Term = TT Name

303type Type = Term

317type Type = Term

304

318

src/Idris/AbsSyntax.hs+11−4

@@ -6,6 +6,7 @@ module Idris.AbsSyntax where

6import Core.TT

7import Core.Evaluate

8import Core.Elaborate

9+import Core.Typecheck

10import Control.Monad.State

11import Control.Monad.State

11import Data.List

12import Data.List

@@ -47,7 +48,6 @@ idrisInit = IState emptyContext [] emptyContext emptyContext

47-- global state (hence the IO inner monad).

48-- global state (hence the IO inner monad).

48type Idris a = StateT IState IO a

49type Idris a = StateT IState IO a

50−

51getContext :: Idris Context

52getContext = do i <- get; return (tt_ctxt i)

@@ -78,9 +78,16 @@ updateContext :: (Context -> Context) -> Idris ()

78updateContext f = do i <- get; put (i { tt_ctxt = f (tt_ctxt i) } )

80addDeferred :: [(Name, Type)] -> Idris ()

81−addDeferred ns = do mapM_ (\(n, t) -> updateContext (addTyDecl n t)) ns

81+addDeferred ns = do mapM_ (\(n, t) -> updateContext (addTyDecl n (tidyNames [] t))) ns

82 i <- get

83 put (i { idris_metavars = map fst ns ++ idris_metavars i })

84+ where tidyNames used (Bind (MN i x) b sc)

85+ = let n' = uniqueName (UN [x]) used in

86+ Bind n' b $ tidyNames (n':used) sc

87+ tidyNames used (Bind n b sc)

88+ = let n' = uniqueName n used in

89+ Bind n' b $ tidyNames (n':used) sc

90+ tidyNames used b = b

85solveDeferred :: Name -> Idris ()

92solveDeferred :: Name -> Idris ()

86solveDeferred n = do i <- get

93solveDeferred n = do i <- get

@@ -220,7 +227,7 @@ data PTerm = PQuote Raw

220

227

221data PTactic = Intro [Name] | Focus Name

228data PTactic = Intro [Name] | Focus Name

222 | Refine Name [Bool] | Rewrite PTerm

229 | Refine Name [Bool] | Rewrite PTerm

223− | Exact PTerm

230+ | Exact PTerm | Compute | Trivial

224 | Solve

231 | Solve

225 | Attack

232 | Attack

226 | ProofState | ProofTerm | Undo

233 | ProofState | ProofTerm | Undo

@@ -392,7 +399,7 @@ namesIn ist tm = nub $ ni [] tm

392 = case lookupCtxt n (idris_implicits ist) of

399 = case lookupCtxt n (idris_implicits ist) of

393 Nothing -> [n]

400 Nothing -> [n]

394 _ -> []

401 _ -> []

395− ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

402+ ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

396 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

403 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

397 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc

404 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc

398 ni env (PEq _ l r) = ni env l ++ ni env r

405 ni env (PEq _ l r) = ni env l ++ ni env r

src/Idris/ElabDecls.hs+35−9

@@ -27,6 +27,10 @@ data ElabInfo = EInfo { params :: [(Name, PTerm)],

28toplevel = EInfo [] emptyContext id

30+checkDef ns = do ctxt <- getContext

31+ mapM (\(n, t) -> do (t', _) <- tclift $ recheck ctxt [] t

32+ return (n, t')) ns

33+

30elabType :: ElabInfo -> FC -> Name -> PTerm -> Idris ()

34elabType :: ElabInfo -> FC -> Name -> PTerm -> Idris ()

31elabType info fc n_in ty_in = let ty = piBind (params info) ty_in

35elabType info fc n_in ty_in = let ty = piBind (params info) ty_in

32 n = liftname info n_in in

36 n = liftname info n_in in

@@ -38,7 +42,8 @@ elabType info fc n_in ty_in = let ty = piBind (params info) ty_in

38 (cty, _) <- tclift $ recheck ctxt [] ty'

42 (cty, _) <- tclift $ recheck ctxt [] ty'

39 logLvl 2 $ "---> " ++ show cty

43 logLvl 2 $ "---> " ++ show cty

40 let nty = normalise ctxt [] cty

44 let nty = normalise ctxt [] cty

41− addDeferred ((n, nty):defer)

45+ ds <- checkDef ((n, nty):defer)

46+ addDeferred ds

43elabData :: ElabInfo -> FC -> PData -> Idris ()

48elabData :: ElabInfo -> FC -> PData -> Idris ()

44elabData info fc (PDatadecl n t dcons)

49elabData info fc (PDatadecl n t dcons)

@@ -47,7 +52,8 @@ elabData info fc (PDatadecl n t dcons)

47 ctxt <- getContext

52 ctxt <- getContext

48 ((t', defer), log) <- tclift $ elaborate ctxt n (Set 0)

53 ((t', defer), log) <- tclift $ elaborate ctxt n (Set 0)

49 (erun fc (build info False t))

54 (erun fc (build info False t))

50− addDeferred defer

55+ def' <- checkDef defer

56+ addDeferred def'

51 (cty, _) <- tclift $ recheck ctxt [] t'

57 (cty, _) <- tclift $ recheck ctxt [] t'

52 logLvl 2 $ "---> " ++ show cty

58 logLvl 2 $ "---> " ++ show cty

53 updateContext (addTyDecl n cty) -- temporary, to check cons

59 updateContext (addTyDecl n cty) -- temporary, to check cons

@@ -63,7 +69,8 @@ elabCon info (n, t, fc)

63 ((t', defer), log) <- tclift $ elaborate ctxt n (Set 0)

69 ((t', defer), log) <- tclift $ elaborate ctxt n (Set 0)

64 (erun fc (build info False t))

70 (erun fc (build info False t))

65 logLvl 2 $ "Rechecking " ++ show t'

71 logLvl 2 $ "Rechecking " ++ show t'

66− addDeferred defer

72+ def' <- checkDef defer

73+ addDeferred def'

67 (cty, _) <- tclift $ recheck ctxt [] t'

74 (cty, _) <- tclift $ recheck ctxt [] t'

68 logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty

75 logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty

69 return (n, cty)

76 return (n, cty)

@@ -128,7 +135,8 @@ elabClause info fc (PClause fname lhs withs rhs whereblock)

128 return $ runState (collectDeferred tt) [])

135 return $ runState (collectDeferred tt) [])

129 logLvl 2 $ "---> " ++ show rhs'

136 logLvl 2 $ "---> " ++ show rhs'

130 when (not (null defer)) $ iLOG $ "DEFERRED " ++ show defer

137 when (not (null defer)) $ iLOG $ "DEFERRED " ++ show defer

131− addDeferred defer

138+ def' <- checkDef defer

139+ addDeferred def'

132 ctxt <- getContext

140 ctxt <- getContext

133 (crhs, crhsty) <- tclift $ recheck ctxt [] rhs'

141 (crhs, crhsty) <- tclift $ recheck ctxt [] rhs'

134 return (clhs, crhs)

142 return (clhs, crhs)

@@ -170,7 +178,8 @@ elabClause info fc (PWith fname lhs withs wval withblock)

170 psolve lhs_tm

178 psolve lhs_tm

171 tt <- get_term

179 tt <- get_term

172 return (tt, d))

180 return (tt, d))

173− addDeferred defer

181+ def' <- checkDef defer

182+ addDeferred def'

174 (cwval, cwvalty) <- tclift $ recheck ctxt [] (getInferTerm wval')

183 (cwval, cwvalty) <- tclift $ recheck ctxt [] (getInferTerm wval')

175 logLvl 3 ("With type " ++ show cwvalty ++ "\nRet type " ++ show ret_ty)

184 logLvl 3 ("With type " ++ show cwvalty ++ "\nRet type " ++ show ret_ty)

176 windex <- getName

185 windex <- getName

@@ -179,7 +188,8 @@ elabClause info fc (PWith fname lhs withs wval withblock)

179 let wtype = bindTyArgs Pi (bargs ++ [(MN 0 "warg", getRetTy cwvalty)]) ret_ty

188 let wtype = bindTyArgs Pi (bargs ++ [(MN 0 "warg", getRetTy cwvalty)]) ret_ty

180 logLvl 3 ("New function type " ++ show wtype)

189 logLvl 3 ("New function type " ++ show wtype)

181 let wname = MN windex (show fname)

190 let wname = MN windex (show fname)

182− addDeferred [(wname, wtype)]

191+ def' <- checkDef [(wname, wtype)]

192+ addDeferred def'

183

193

184 -- in the subdecls, lhs becomes:

194 -- in the subdecls, lhs becomes:

185 -- fname pats | wpat [rest]

195 -- fname pats | wpat [rest]

@@ -200,7 +210,8 @@ elabClause info fc (PWith fname lhs withs wval withblock)

200 psolve lhs_tm

210 psolve lhs_tm

201 tt <- get_term

211 tt <- get_term

202 return (tt, d))

212 return (tt, d))

203− addDeferred defer

213+ def' <- checkDef defer

214+ addDeferred def'

204 (crhs, crhsty) <- tclift $ recheck ctxt [] rhs'

215 (crhs, crhsty) <- tclift $ recheck ctxt [] rhs'

205 return (clhs, crhs)

216 return (clhs, crhs)

206 where

217 where

@@ -346,7 +357,7 @@ elab info pattern tm = do elab' tm

346 = elab' (PApp fc (PRef fc n) [])

357 = elab' (PApp fc (PRef fc n) [])

347 | otherwise = erun fc $ do apply (Var n) []; solve

358 | otherwise = erun fc $ do apply (Var n) []; solve

348 elab' (PLam n Placeholder sc)

359 elab' (PLam n Placeholder sc)

349− = do attack; intro n; elab' sc; solve

360+ = do attack; intro (Just n); elab' sc; solve

350 elab' (PPi _ n Placeholder sc)

361 elab' (PPi _ n Placeholder sc)

351 = do attack; arg n (MN 0 "ty"); elab' sc; solve

362 = do attack; arg n (MN 0 "ty"); elab' sc; solve

352 elab' (PPi _ n ty sc)

363 elab' (PPi _ n ty sc)

@@ -424,7 +435,12 @@ collectDeferred t = return t

424

435

425runTac :: Bool -> PTactic -> Elab ()

436runTac :: Bool -> PTactic -> Elab ()

426runTac autoSolve = runT where

437runTac autoSolve = runT where

438+ runT (Intro []) = do g <- goal

439+ attack; intro (bname g)

440+ where

441+ bname (Bind n _ _) = Just n

442+ bname _ = Nothing

427− runT (Intro xs) = mapM_ (\x -> do attack; intro x) xs

443+ runT (Intro xs) = mapM_ (\x -> do attack; intro (Just x)) xs

428 runT (Exact tm) = do elab toplevel False tm

444 runT (Exact tm) = do elab toplevel False tm

429 when autoSolve solveAll

445 when autoSolve solveAll

430 runT (Refine fn imps) = do ns <- apply (Var fn) imps

446 runT (Refine fn imps) = do ns <- apply (Var fn) imps

@@ -442,6 +458,16 @@ runTac autoSolve = runT where

442 elab toplevel False tm

458 elab toplevel False tm

443 rewrite (Var letn)

459 rewrite (Var letn)

444 when autoSolve solveAll

460 when autoSolve solveAll

461+ runT Compute = compute

462+ runT Trivial = try (do elab toplevel False (PRefl (FC "prf" 0))

463+ when autoSolve solveAll)

464+ (do env <- get_env

465+ tryAll (map fst env))

466+ where

467+ tryAll [] = fail "No trivial solution"

468+ tryAll (x:xs) = try (do elab toplevel False (PRef (FC "prf" 0) x)

469+ when autoSolve solveAll)

470+ (tryAll xs)

445 runT (Focus n) = focus n

471 runT (Focus n) = focus n

446 runT Solve = solve

472 runT Solve = solve

447 runT x = fail $ "Not implemented " ++ show x

473 runT x = fail $ "Not implemented " ++ show x

src/Idris/Parser.hs+8−12

@@ -609,18 +609,14 @@ pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')

609 <|> do reserved "exact"; t <- pExpr syn;

610 i <- getState

611 return $ Exact (desugar syn i t)

612− <|> do reserved "solve"

612+ <|> do reserved "compute"; return Compute

613+ <|> do reserved "trivial"; return Trivial

613− return Solve

614+ <|> do reserved "solve"; return Solve

614− <|> do reserved "attack"

615+ <|> do reserved "attack"; return Attack

615− return Attack

616− <|> do reserved "state"

617− return ProofState

616+ <|> do reserved "state"; return ProofState

618− <|> do reserved "term"

619− return ProofTerm

617+ <|> do reserved "term"; return ProofTerm

620− <|> do reserved "undo"

618+ <|> do reserved "undo"; return Undo

621− return Undo

622− <|> do reserved "qed"

619+ <|> do reserved "qed"; return Qed

623− return Qed

624 where isImp (PImp _ _ _) = True

620 where isImp (PImp _ _ _) = True

625 isImp _ = False

621 isImp _ = False

626 imp = do lchar '?'; return False

622 imp = do lchar '?'; return False