f1c7faf · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Added tactics construct, and tactic sequencing/choice

f1c7fafEdwin Brady15 years ago

src/Idris/AbsSyntax.hs+7

compare with master

unifiedsplit

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

295 | PReturn FC

296 | PMetavar Name

297 | PProof [PTactic]

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

298 | PElabError String -- error to report on elaboration

299 | PElabError String -- error to report on elaboration

299 deriving Eq

300 deriving Eq

300

301

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

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

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

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

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

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

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

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

313 mpt x = x

315 mpt x = x

314

316

315

317

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

319 | Solve

321 | Solve

320 | Attack

322 | Attack

321 | ProofState | ProofTerm | Undo

323 | ProofState | ProofTerm | Undo

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

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

322 | Qed

326 | Qed

323 deriving (Show, Eq, Functor)

327 deriving (Show, Eq, Functor)

324

328

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

489 se p PSet = "Set"

493 se p PSet = "Set"

490 se p (PConstant c) = show c

494 se p (PConstant c) = show c

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

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

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

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

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

493 se p Placeholder = "_"

498 se p Placeholder = "_"

494

499

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

617 en (PHidden t) = PHidden (en t)

622 en (PHidden t) = PHidden (en t)

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

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

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

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

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

620

626

621 en (PQuote (Var n))

627 en (PQuote (Var n))

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

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

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

809 PPi p n ty' sc'

815 PPi p n ty' sc'

810 ai env (PHidden tm) = PHidden (ai env tm)

816 ai env (PHidden tm) = PHidden (ai env tm)

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

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

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

812 ai env tm = tm

819 ai env tm = tm

813

820

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

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

src/Idris/ElabDecls.hs+3

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

609 movelast h

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

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

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

612 elab' (PElabError e) = fail e

613 elab' (PElabError e) = fail e

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

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

614

615

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

721 runT Trivial = do trivial ist; when autoSolve solveAll

722 runT Trivial = do trivial ist; when autoSolve solveAll

722 runT (Focus n) = focus n

723 runT (Focus n) = focus n

723 runT Solve = solve

724 runT Solve = solve

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

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

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

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

725

728

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

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

src/Idris/Parser.hs+14

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

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

412 lchar '}'

413 return (PProof ts)

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

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

416+ lchar '}'

417+ return (PTactics ts)

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

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

415 <|> try (pPair syn)

419 <|> try (pPair syn)

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

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

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

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

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

727 i <- getState

731 i <- getState

728 return $ Exact (desugar syn i t)

732 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

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

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

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

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

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

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