abf99a5 · Idris-dev · git.iko.soy

idris.cabal+1

compare with master

unifiedsplit

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

328 , Idris.ParseData

329 , Idris.PartialEval

330 , Idris.Primitives

331+ , Idris.ProofSearch

331 , Idris.Prover

332 , Idris.Prover

332 , Idris.Providers

333 , Idris.Providers

333 , Idris.REPL

334 , Idris.REPL

src/Idris/AbsSyntaxTree.hs+5−1

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

243 | CaseSplitAt Bool Int Name

244 | AddClauseFrom Bool Int Name

245 | MakeWith Bool Int Name

246+ | DoProofSearch Bool Int Name

246 | SetOpt Opt

247 | SetOpt Opt

247 | UnsetOpt Opt

248 | UnsetOpt Opt

248 | NOP

249 | NOP

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

419deriving instance Binary PDecl'

420deriving instance Binary PDecl'

420!-}

421!-}

421

422

423+-- For elaborator state

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

425+

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

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

423--

427--

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

428-- 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

611 | Equiv t

615 | Equiv t

612 | MatchRefine Name

616 | MatchRefine Name

613 | LetTac Name t | LetTacTy Name t t

617 | LetTac Name t | LetTacTy Name t t

614− | Exact t | Compute | Trivial

618+ | Exact t | Compute | Trivial | ProofSearch

615 | Solve

619 | Solve

616 | Attack

620 | Attack

617 | ProofState | ProofTerm | Undo

621 | ProofState | ProofTerm | Undo

src/Idris/Delaborate.hs+9−1

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

63 dens x | fullname = x

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

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

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

66 _ -> ns

67 _ -> ns

67 dens n = n

68 dens n = n

68

69

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

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

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

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

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

82 (de env [] r)

83 (de env [] r)

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

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

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

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

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

85

89

90+ mkMVApp n []

91+ = PMetavar n

92+ mkMVApp n args

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

86 mkPApp n args

94 mkPApp n args

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

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

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

96 = 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

5import Idris.AbsSyntax

6import Idris.DSL

7import Idris.Delaborate

8+import Idris.ProofSearch

8

9

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

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

10import Core.TT

11import Core.TT

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

26

27

27toplevel = EInfo [] emptyContext id Nothing

28toplevel = EInfo [] emptyContext id Nothing

28

29

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

30−

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

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

32-- elaborated, typechecked term.

31-- elaborated, typechecked term.

33--

32--

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

637

636

638pruneByType t _ as = as

637pruneByType t _ as = as

639

638

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−

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

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

661findInstances ist t

640findInstances ist t

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

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

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

665 _ -> []

644 _ -> []

666 | otherwise = []

645 | otherwise = []

667

646

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+

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

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

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

652resolveTC 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

671resolveTC depth fn ist

654resolveTC depth fn ist

672 = do hnf_compute

655 = do hnf_compute

673 g <- goal

656 g <- goal

674 ptm <- get_term

657 ptm <- get_term

675 hs <- get_holes

658 hs <- get_holes

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

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

677− then try' (trivial ist)

660+ then try' (trivial' ist)

678 (do t <- goal

661 (do t <- goal

679 let (tc, ttypes) = unApply t

662 let (tc, ttypes) = unApply t

680 scopeOnly <- needsDefault t tc ttypes

663 scopeOnly <- needsDefault t tc ttypes

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

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

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

688 let depth' = if scopeOnly then 2 else depth

671 let depth' = if scopeOnly then 2 else depth

689 blunderbuss t depth' insts) True

672 blunderbuss t depth' insts) True

690− else do try' (trivial ist)

673+ else do try' (trivial' ist)

691 (do g <- goal

674 (do g <- goal

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

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

693-- tm <- get_term

676-- tm <- get_term

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

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

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

877 when autoSolve solveAll

860 when autoSolve solveAll

878 runT Compute = compute

861 runT Compute = compute

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

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

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

880 runT (Focus n) = focus n

864 runT (Focus n) = focus n

881 runT Solve = solve

865 runT Solve = solve

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

866 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) (

1028 return $ TSeq t (mergeSeq ts)

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

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

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

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

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

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

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

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

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

src/Idris/ProofSearch.hsnew file+35

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

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

2+

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

4+import Core.TT

5+import Core.Evaluate

6+import Core.CaseTree

7+import Core.Typecheck

8+

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)

575 unlines rest)

576 runIO $ copyFile fb fn

577 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 = ""

578

620

579process h fn (Spec t)

621process h fn (Spec t)

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

622 = 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)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

83 return (Just x))

87 return (Just x))