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

git.iko.soy/Idris-dev

Tinkering with tactics and deferred definitions

commit188dda5d5b59d6deb0a5612d0b5bcd1b7e5d0128 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateTue 1 Nov 2011, 10:44 (15 years ago) parentf7a7f0b

7 files changed+80−45

compare with master

unifiedsplit

src/Core/Elaborate.hs+2−13 src/Core/ProofState.hs+9−6 src/Core/ShellParser.hs+1−1 src/Core/TT.hs+14 src/Idris/AbsSyntax.hs+11−4 src/Idris/ElabDecls.hs+35−9 src/Idris/Parser.hs+8−12

src/Core/Elaborate.hs+2−13

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

114114unique_hole :: Name -> Elab Name

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

116116 env <- get_env

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

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

118118 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

130119

131120elog :: String -> Elab ()

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

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

173162check_in :: Raw -> Elab ()

174163check_in t = processTactic' (CheckIn t)

175164

176−intro :: Name -> Elab ()

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

177166intro n = processTactic' (Intro n)

178167

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

src/Core/ProofState.hs+9−6

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

4747 | Compute

4848 | EvalIn Raw

4949 | CheckIn Raw

50− | Intro Name

50+ | Intro (Maybe Name)

5151 | Forall Name Raw

5252 | LetBind Name Raw Raw

5353 | Rewrite Raw

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

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

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

253253

254−intro :: Name -> RunTactic

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

256− do let t' = normalise ctxt env t

254+intro :: Maybe Name -> RunTactic

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

259+ let t' = normalise ctxt env t

257260 case t' of

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

259262 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' =

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

290293 let newt = mkP l r l t

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

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

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

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

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

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

295298 return scv

296299 _ -> fail "Not an equality type"

src/Core/ShellParser.hs+1−1

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

5454 return (discard (apply tm args))

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

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

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

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

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

5959 return (forall n ty)

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

src/Core/TT.hs+14

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

55import Control.Monad.State

66import Debug.Trace

77import qualified Data.Map as Map

8+import Data.Char

910{- The language has:

1011 * Full dependent types

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

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

300301getArgTys _ = []

301302

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+

302316type Term = TT Name

303317type Type = Term

304318

src/Idris/AbsSyntax.hs+11−4

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

66import Core.TT

77import Core.Evaluate

88import Core.Elaborate

9+import Core.Typecheck

910

1011import Control.Monad.State

1112import Data.List

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

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

4849type Idris a = StateT IState IO a

4950

50−

5151getContext :: Idris Context

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

5353

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

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

7979

8080addDeferred :: [(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

8282 i <- get

8383 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

8491

8592solveDeferred :: Name -> Idris ()

8693solveDeferred n = do i <- get

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

220227

221228data PTactic = Intro [Name] | Focus Name

222229 | Refine Name [Bool] | Rewrite PTerm

223− | Exact PTerm

230+ | Exact PTerm | Compute | Trivial

224231 | Solve

225232 | Attack

226233 | ProofState | ProofTerm | Undo

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

392399 = case lookupCtxt n (idris_implicits ist) of

393400 Nothing -> [n]

394401 _ -> []

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)

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

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

398405 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)],

2727

2828toplevel = EInfo [] emptyContext id

2929

30+checkDef ns = do ctxt <- getContext

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

32+ return (n, t')) ns

33+

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

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

3236 n = liftname info n_in in

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

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

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

4044 let nty = normalise ctxt [] cty

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

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

46+ addDeferred ds

4247

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

4449elabData info fc (PDatadecl n t dcons)

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

4752 ctxt <- getContext

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

4954 (erun fc (build info False t))

50− addDeferred defer

55+ def' <- checkDef defer

56+ addDeferred def'

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

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

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

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

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

6470 (erun fc (build info False t))

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

66− addDeferred defer

72+ def' <- checkDef defer

73+ addDeferred def'

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

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

6976 return (n, cty)

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

128135 return $ runState (collectDeferred tt) [])

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

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

131− addDeferred defer

138+ def' <- checkDef defer

139+ addDeferred def'

132140 ctxt <- getContext

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

134142 return (clhs, crhs)

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

170178 psolve lhs_tm

171179 tt <- get_term

172180 return (tt, d))

173− addDeferred defer

181+ def' <- checkDef defer

182+ addDeferred def'

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

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

176185 windex <- getName

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

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

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

181190 let wname = MN windex (show fname)

182− addDeferred [(wname, wtype)]

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

192+ addDeferred def'

183193

184194 -- in the subdecls, lhs becomes:

185195 -- fname pats | wpat [rest]

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

200210 psolve lhs_tm

201211 tt <- get_term

202212 return (tt, d))

203− addDeferred defer

213+ def' <- checkDef defer

214+ addDeferred def'

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

205216 return (clhs, crhs)

206217 where

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

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

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

348359 elab' (PLam n Placeholder sc)

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

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

350361 elab' (PPi _ n Placeholder sc)

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

352363 elab' (PPi _ n ty sc)

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

424435

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

426437runTac autoSolve = runT where

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

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

439+ attack; intro (bname g)

440+ where

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

442+ bname _ = Nothing

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

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

429445 when autoSolve solveAll

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

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

442458 elab toplevel False tm

443459 rewrite (Var letn)

444460 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)

445471 runT (Focus n) = focus n

446472 runT Solve = solve

447473 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 ',')

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

610610 i <- getState

611611 return $ Exact (desugar syn i t)

612− <|> do reserved "solve"

613− return Solve

614− <|> do reserved "attack"

615− return Attack

616− <|> do reserved "state"

617− return ProofState

618− <|> do reserved "term"

619− return ProofTerm

620− <|> do reserved "undo"

621− return Undo

622− <|> do reserved "qed"

623− return Qed

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

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

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

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

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

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

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

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

624620 where isImp (PImp _ _ _) = True

625621 isImp _ = False

626622 imp = do lchar '?'; return False