f1c7faf · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Added tactics construct, and tactic sequencing/choice

commitf1c7faf888100551b16443ac0cd89c385b0afa70 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateTue 15 Nov 2011, 17:12 (15 years ago) parent71c1a0e

3 files changed+24

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+7 src/Idris/ElabDecls.hs+3 src/Idris/Parser.hs+14

src/Idris/AbsSyntax.hs+7

@@ -295,6 +295,7 @@ data PTerm = PQuote Raw

295295 | PReturn FC

296296 | PMetavar Name

297297 | PProof [PTactic]

298+ | PTactics [PTactic] -- as PProof, but no auto solving

298299 | PElabError String -- error to report on elaboration

299300 deriving Eq

300301

@@ -310,6 +311,7 @@ mapPT f t = f (mpt t) where

310311 mpt (PHidden t) = PHidden (mapPT f t)

311312 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)

312313 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)

314+ mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)

313315 mpt x = x

314316

315317

@@ -319,6 +321,8 @@ data PTactic' t = Intro [Name] | Focus Name

319321 | Solve

320322 | Attack

321323 | ProofState | ProofTerm | Undo

324+ | Try (PTactic' t) (PTactic' t)

325+ | TSeq (PTactic' t) (PTactic' t)

322326 | Qed

323327 deriving (Show, Eq, Functor)

324328

@@ -489,6 +493,7 @@ showImp impl tm = se 10 tm where

489493 se p PSet = "Set"

490494 se p (PConstant c) = show c

491495 se p (PProof ts) = "proof { " ++ show ts ++ "}"

496+ se p (PTactics ts) = "tactics { " ++ show ts ++ "}"

492497 se p (PMetavar n) = "?" ++ show n

493498 se p Placeholder = "_"

494499

@@ -617,6 +622,7 @@ expandParams dec ps ns tm = en tm

617622 en (PHidden t) = PHidden (en t)

618623 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)

619624 en (PProof ts) = PProof (map (fmap en) ts)

625+ en (PTactics ts) = PTactics (map (fmap en) ts)

620626

621627 en (PQuote (Var n))

622628 | n `elem` ns = PQuote (Var (dec n))

@@ -809,6 +815,7 @@ addImpl ist ptm = ai [] ptm

809815 PPi p n ty' sc'

810816 ai env (PHidden tm) = PHidden (ai env tm)

811817 ai env (PProof ts) = PProof (map (fmap (ai env)) ts)

818+ ai env (PTactics ts) = PTactics (map (fmap (ai env)) ts)

812819 ai env tm = tm

813820

814821aiFn :: IState -> FC -> Name -> [PArg] -> PTerm

src/Idris/ElabDecls.hs+3

@@ -609,6 +609,7 @@ elab ist info pattern tm

609609 movelast h

610610 elab' (PMetavar n) = do attack; defer n; solve

611611 elab' (PProof ts) = do mapM_ (runTac True ist) ts

612+ elab' (PTactics ts) = do mapM_ (runTac False ist) ts

612613 elab' (PElabError e) = fail e

613614 elab' x = fail $ "Not implemented " ++ show x

614615

@@ -721,6 +722,8 @@ runTac autoSolve ist tac = runT (fmap (addImpl ist) tac) where

721722 runT Trivial = do trivial ist; when autoSolve solveAll

722723 runT (Focus n) = focus n

723724 runT Solve = solve

725+ runT (Try l r) = do try (runT l) (runT r)

726+ runT (TSeq l r) = do runT l; runT r

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

725728

726729solveAll = try (do solve; solveAll) (return ())

src/Idris/Parser.hs+14

@@ -411,6 +411,10 @@ pSimpleExpr syn =

411411 ts <- endBy (pTactic syn) (lchar ';')

412412 lchar '}'

413413 return (PProof ts)

414+ <|> do reserved "tactics"; lchar '{';

415+ ts <- endBy (pTactic syn) (lchar ';')

416+ lchar '}'

417+ return (PTactics ts)

414418 <|> try (do x <- pfName; fc <- pfc; return (PRef fc x))

415419 <|> try (pPair syn)

416420 <|> try (do lchar '('; e <- pExpr syn; lchar ')'; return e)

@@ -726,6 +730,16 @@ pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')

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

727731 i <- getState

728732 return $ Exact (desugar syn i t)

733+ <|> do reserved "try"; t <- pTactic syn;

734+ lchar '|';

735+ t1 <- pTactic syn

736+ return $ Try t t1

737+ <|> do lchar '{'

738+ t <- pTactic syn;

739+ lchar ';';

740+ t1 <- pTactic syn;

741+ lchar '}'

742+ return $ TSeq t t1

729743 <|> do reserved "compute"; return Compute

730744 <|> do reserved "trivial"; return Trivial

731745 <|> do reserved "solve"; return Solve