abf99a5 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add proofsearch tactic, with :ps at the REPL

At the moment, just invokes 'trivial'. There is a corresponding vim command, \o, which invokes this and prints the result.

commitabf99a577fe4dc505bd3fac1ae880e53ed162a45 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 29 Oct 2013, 18:32 (13 years ago) parentabf46fe

8 files changed+108−29

compare with master

unifiedsplit

idris.cabal+1 src/Idris/AbsSyntaxTree.hs+5−1 src/Idris/Delaborate.hs+9−1 src/Idris/ElabTerm.hs+10−26 src/Idris/ParseExpr.hs+1 src/Idris/ProofSearch.hs+35 src/Idris/REPL.hs+42 src/Idris/REPLParser.hs+5−1

idris.cabal+1

@@ -328,6 +328,7 @@ Executable idris

328328 , Idris.ParseData

329329 , Idris.PartialEval

330330 , Idris.Primitives

331+ , Idris.ProofSearch

331332 , Idris.Prover

332333 , Idris.Providers

333334 , Idris.REPL

src/Idris/AbsSyntaxTree.hs+5−1

@@ -243,6 +243,7 @@ data Command = Quit

243243 | CaseSplitAt Bool Int Name

244244 | AddClauseFrom Bool Int Name

245245 | MakeWith Bool Int Name

246+ | DoProofSearch Bool Int Name

246247 | SetOpt Opt

247248 | UnsetOpt Opt

248249 | NOP

@@ -419,6 +420,9 @@ data PDecl' t

419420deriving instance Binary PDecl'

420421!-}

421422

423+-- For elaborator state

424+type ElabD a = Elab' [PDecl] a

425+

422426-- | One clause of a top-level definition. Term arguments to constructors are:

423427--

424428-- 1. The whole application (missing for PClauseR and PWithR because they're within a "with" clause)

@@ -611,7 +615,7 @@ data PTactic' t = Intro [Name] | Intros | Focus Name

611615 | Equiv t

612616 | MatchRefine Name

613617 | LetTac Name t | LetTacTy Name t t

614− | Exact t | Compute | Trivial

618+ | Exact t | Compute | Trivial | ProofSearch

615619 | Solve

616620 | Attack

617621 | ProofState | ProofTerm | Undo

src/Idris/Delaborate.hs+9−1

@@ -63,6 +63,7 @@ delabTy' ist imps tm fullname = de [] imps tm

6363 dens x | fullname = x

6464 dens ns@(NS n _) = case lookupCtxt n (idris_implicits ist) of

6565 [_] -> n -- just one thing

66+ [] -> n -- metavariables have no implicits

6667 _ -> ns

6768 dens n = n

6869

@@ -80,9 +81,16 @@ delabTy' ist imps tm fullname = de [] imps tm

8081 | n == eqTy = PEq un (de env [] l) (de env [] r)

8182 | n == UN "Ex_intro" = PDPair un (de env [] l) Placeholder

8283 (de env [] r)

83− deFn env (P _ n _) args = mkPApp (dens n) (map (de env []) args)

84+ deFn env (P _ n _) args

85+ = case lookup n (idris_metavars ist) of

86+ Just mi -> mkMVApp (dens n) (drop mi (map (de env []) args))

87+ Nothing -> mkPApp (dens n) (map (de env []) args)

8488 deFn env f args = PApp un (de env [] f) (map pexp (map (de env []) args))

8589

90+ mkMVApp n []

91+ = PMetavar n

92+ mkMVApp n args

93+ = PApp un (PMetavar n) (map pexp args)

8694 mkPApp n args

8795 | [imps] <- lookupCtxt n (idris_implicits ist)

8896 = PApp un (PRef un n) (zipWith imp (imps ++ repeat (pexp undefined)) args)

src/Idris/ElabTerm.hs+10−26

@@ -5,6 +5,7 @@ module Idris.ElabTerm where

55import Idris.AbsSyntax

66import Idris.DSL

77import Idris.Delaborate

8+import Idris.ProofSearch

910import Core.Elaborate hiding (Tactic(..))

1011import Core.TT

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

2627

2728toplevel = EInfo [] emptyContext id Nothing

2829

29−type ElabD a = Elab' [PDecl] a

30−

3130-- Using the elaborator, convert a term in raw syntax to a fully

3231-- elaborated, typechecked term.

3332--

@@ -637,26 +636,6 @@ pruneByType (P _ n _) c as

637636

638637pruneByType t _ as = as

639638

640−trivial :: IState -> ElabD ()

641−trivial ist = try' (do elab ist toplevel False False (MN 0 "tac")

642− (PRefl (fileFC "prf") Placeholder)

643− return ())

644− (do env <- get_env

645− g <- goal

646− tryAll env

647− return ()) True

648− where

649− tryAll [] = fail "No trivial solution"

650− tryAll ((x, b):xs)

651− = do -- if type of x has any holes in it, move on

652− hs <- get_holes

653− g <- goal

654− if all (\n -> not (n `elem` hs)) (freeNames (binderTy b))

655− then try' (elab ist toplevel False False

656− (MN 0 "tac") (PRef (fileFC "prf") x))

657− (tryAll xs) True

658− else tryAll xs

659−

660639findInstances :: IState -> Term -> [Name]

661640findInstances ist t

662641 | (P _ n _, _) <- unApply t

@@ -665,16 +644,20 @@ findInstances ist t

665644 _ -> []

666645 | otherwise = []

667646

647+trivial' ist = trivial (elab ist toplevel False False (MN 0 "tac")) ist

648+proofSearch' ist = trivial (elab ist toplevel False False (MN 0 "tac")) ist

649+

650+

668651resolveTC :: Int -> Name -> IState -> ElabD ()

669652resolveTC 0 fn ist = fail $ "Can't resolve type class"

670−resolveTC 1 fn ist = try' (trivial ist) (resolveTC 0 fn ist) True

653+resolveTC 1 fn ist = try' (trivial' ist) (resolveTC 0 fn ist) True

671654resolveTC depth fn ist

672655 = do hnf_compute

673656 g <- goal

674657 ptm <- get_term

675658 hs <- get_holes

676659 if True -- all (\n -> not (n `elem` hs)) (freeNames g)

677− then try' (trivial ist)

660+ then try' (trivial' ist)

678661 (do t <- goal

679662 let (tc, ttypes) = unApply t

680663 scopeOnly <- needsDefault t tc ttypes

@@ -687,7 +670,7 @@ resolveTC depth fn ist

687670-- if scopeOnly then fail "Can't resolve" else

688671 let depth' = if scopeOnly then 2 else depth

689672 blunderbuss t depth' insts) True

690− else do try' (trivial ist)

673+ else do try' (trivial' ist)

691674 (do g <- goal

692675 fail $ "Can't resolve " ++ show g) True

693676-- tm <- get_term

@@ -876,7 +859,8 @@ runTac autoSolve ist tac

876859 elab ist toplevel False False (MN 0 "tac") tm

877860 when autoSolve solveAll

878861 runT Compute = compute

879− runT Trivial = do trivial ist; when autoSolve solveAll

862+ runT Trivial = do trivial' ist; when autoSolve solveAll

863+ runT ProofSearch = do proofSearch' ist; when autoSolve solveAll

880864 runT (Focus n) = focus n

881865 runT Solve = solve

882866 runT (Try l r) = do try' (runT l) (runT r) True

src/Idris/ParseExpr.hs+1

@@ -1028,6 +1028,7 @@ tactic syn = do reserved "intro"; ns <- sepBy (indentPropHolds gtProp *> name) (

10281028 return $ TSeq t (mergeSeq ts)

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

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

1031+ <|> do reserved "proofsearch"; return ProofSearch

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

10321033 <|> do reserved "attack"; return Attack

10331034 <|> do reserved "state"; return ProofState

src/Idris/ProofSearch.hsnew file+35

@@ -0,0 +1,35 @@

1+module Idris.ProofSearch(trivial, proofSearch) where

3+import Core.Elaborate hiding (Tactic(..))

4+import Core.TT

5+import Core.Evaluate

6+import Core.CaseTree

7+import Core.Typecheck

9+import Idris.AbsSyntax

10+import Idris.Delaborate

11+import Idris.Error

12+

13+-- Pass in a term elaborator to avoid a cyclic dependency with ElabTerm

14+

15+trivial :: (PTerm -> ElabD ()) -> IState -> ElabD ()

16+trivial elab ist = try' (do elab (PRefl (fileFC "prf") Placeholder)

17+ return ())

18+ (do env <- get_env

19+ g <- goal

20+ tryAll env

21+ return ()) True

22+ where

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

24+ tryAll ((x, b):xs)

25+ = do -- if type of x has any holes in it, move on

26+ hs <- get_holes

27+ g <- goal

28+ if all (\n -> not (n `elem` hs)) (freeNames (binderTy b))

29+ then try' (elab (PRef (fileFC "prf") x))

30+ (tryAll xs) True

31+ else tryAll xs

32+

33+proofSearch :: (PTerm -> ElabD ()) -> IState -> ElabD ()

34+proofSearch elab ist = trivial elab ist

35+

src/Idris/REPL.hs+42

@@ -575,6 +575,48 @@ process h fn (MakeWith updatefile l n)

575575 unlines rest)

576576 runIO $ copyFile fb fn

577577 else ihputStrLn h with

578+process h fn (DoProofSearch updatefile l n)

579+ = do src <- runIO $ readFile fn

580+ let (before, tyline : later) = splitAt (l-1) (lines src)

581+ let body = PProof [Try (TSeq Intros ProofSearch) ProofSearch]

582+ ctxt <- getContext

583+ mn <- case lookupNames n ctxt of

584+ [x] -> return x

585+ [] -> return n

586+ ns -> ierror (CantResolveAlts (map show ns))

587+ i <- getIState

588+ let envlen = case lookup mn (idris_metavars i) of

589+ Just mi -> mi

590+ _ -> 0

591+ let fc = fileFC fn

592+ let def = PClause fc mn (PRef fc mn) [] body []

593+ elabDecls toplevel [PClauses fc [] mn [def]]

594+ (tm, ty) <- elabVal toplevel False (PRef fc mn)

595+ ctxt <- getContext

596+ let newmv = show (dropCtxt envlen (delab i (normaliseAll ctxt [] tm)))

597+ if updatefile then

598+ do let fb = fn ++ "~"

599+ runIO $ writeFile fb (unlines before ++

600+ updateMeta tyline (show n) newmv ++ "\n"

601+ ++ unlines later)

602+ runIO $ copyFile fb fn

603+ else ihputStrLn h newmv

604+ where dropCtxt 0 sc = sc

605+ dropCtxt i (PPi _ _ _ sc) = dropCtxt (i - 1) sc

606+ dropCtxt i (PLet _ _ _ sc) = dropCtxt (i - 1) sc

607+ dropCtxt i (PLam _ _ sc) = dropCtxt (i - 1) sc

608+ dropCtxt _ t = t

609+

610+ updateMeta ('?':cs) n new

611+ | length cs >= length n

612+ = case splitAt (length n) cs of

613+ (mv, c:cs) ->

614+ if (isSpace c && mv == n)

615+ then new ++ (c : cs)

616+ else '?' : mv ++ c : updateMeta cs n new

617+ (mv, []) -> if (mv == n) then new else '?' : mv

618+ updateMeta (c:cs) n new = c : updateMeta cs n new

619+ updateMeta [] n new = ""

578620

579621process h fn (Spec t)

580622 = do (tm, ty) <- elabVal toplevel False t

src/Idris/REPLParser.hs+5−1

@@ -43,7 +43,6 @@ pCmd = do P.whiteSpace; try (do cmd ["q", "quit"]; eof; return Quit)

4343 <|> try (do cmd ["jc", "newcompile"]; f <- P.identifier; eof; return (Compile ViaJava f))

4444 <|> try (do cmd ["js", "javascript"]; f <- P.identifier; eof; return (Compile ViaJavaScript f))

4545 <|> try (do cmd ["proofs"]; eof; return Proofs)

46− <|> try (do cmd ["p", "prove"]; n <- P.name; eof; return (Prove n))

4746 <|> try (do cmd ["rmproof"]; n <- P.name; eof; return (RmProof n))

4847 <|> try (do cmd ["showproof"]; n <- P.name; eof; return (ShowProof n))

4948 <|> try (do cmd ["log"]; i <- P.natural; eof; return (LogLvl (fromIntegral i)))

@@ -78,6 +77,11 @@ pCmd = do P.whiteSpace; try (do cmd ["q", "quit"]; eof; return Quit)

7877 upd <- option False (do P.lchar '!'; return True)

7978 l <- P.natural; n <- P.name;

8079 return (MakeWith upd (fromInteger l) n))

80+ <|> try (do cmd ["ps", "proofsearch"]; P.whiteSpace;

81+ upd <- option False (do P.lchar '!'; return True)

82+ l <- P.natural; n <- P.name;

83+ return (DoProofSearch upd (fromInteger l) n))

84+ <|> try (do cmd ["p", "prove"]; n <- P.name; eof; return (Prove n))

8185 <|> try (do cmd ["m", "metavars"]; eof; return Metavars)

8286 <|> try (do cmd ["a", "addproof"]; do n <- option Nothing (do x <- P.name;

8387 return (Just x))