b7b55b7 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Allow hints to be given to proof search

:ps now takes an optional list of names to be used as hints in the proof search.

commitb7b55b7e917e11400e0d55b242ee5da900a3d21a authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 31 Oct 2013, 17:13 (13 years ago) parentb16baad

6 files changed+29−13

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+3−2 src/Idris/CaseSplit.hs+1 src/Idris/ElabTerm.hs+4−3 src/Idris/ProofSearch.hs+6−3 src/Idris/REPL.hs+13−4 src/Idris/REPLParser.hs+2−1

src/Idris/AbsSyntaxTree.hs+3−2

@@ -244,7 +244,7 @@ data Command = Quit

244244 | AddClauseFrom Bool Int Name

245245 | AddMissing Bool Int Name

246246 | MakeWith Bool Int Name

247− | DoProofSearch Bool Int Name

247+ | DoProofSearch Bool Int Name [Name]

248248 | SetOpt Opt

249249 | UnsetOpt Opt

250250 | NOP

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

616616 | Equiv t

617617 | MatchRefine Name

618618 | LetTac Name t | LetTacTy Name t t

619− | Exact t | Compute | Trivial | ProofSearch (Maybe Name) Name

619+ | Exact t | Compute | Trivial

620+ | ProofSearch (Maybe Name) Name [Name]

620621 | Solve

621622 | Attack

622623 | ProofState | ProofTerm | Undo

src/Idris/CaseSplit.hs+1

@@ -256,6 +256,7 @@ nameRoot acc nm =

256256 case span (/='_') nm of

257257 (before, ('_' : after)) -> nameRoot (acc ++ [before]) after

258258 _ -> showSep "_" (acc ++ [nm])

259+

259260getClause :: Int -> -- ^ Line type is declared on

260261 Name -> -- ^ Function name

261262 FilePath -> -- ^ Source file name

src/Idris/ElabTerm.hs+4−3

@@ -646,8 +646,8 @@ findInstances ist t

646646

647647trivial' ist

648648 = trivial (elab ist toplevel False False (MN 0 "tac")) ist

649−proofSearch' ist top n

650− = proofSearch (elab ist toplevel False False (MN 0 "tac")) top n ist

649+proofSearch' ist top n hints

650+ = proofSearch (elab ist toplevel False False (MN 0 "tac")) top n hints ist

651651

652652

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

@@ -863,7 +863,8 @@ runTac autoSolve ist tac

863863 when autoSolve solveAll

864864 runT Compute = compute

865865 runT Trivial = do trivial' ist; when autoSolve solveAll

866− runT (ProofSearch top n) = do proofSearch' ist top n; when autoSolve solveAll

866+ runT (ProofSearch top n hints)

867+ = do proofSearch' ist top n hints; when autoSolve solveAll

867868 runT (Focus n) = focus n

868869 runT Solve = solve

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

src/Idris/ProofSearch.hs+6−3

@@ -33,8 +33,9 @@ trivial elab ist = try' (do elab (PRefl (fileFC "prf") Placeholder)

3333 (tryAll xs) True

3434 else tryAll xs

3535

36−proofSearch :: (PTerm -> ElabD ()) -> Maybe Name -> Name -> IState -> ElabD ()

37−proofSearch elab fn nroot ist = psRec maxDepth

36+proofSearch :: (PTerm -> ElabD ()) -> Maybe Name -> Name -> [Name] ->

37+ IState -> ElabD ()

38+proofSearch elab fn nroot hints ist = psRec maxDepth

3839 where

3940 maxDepth = 6

4041

@@ -54,7 +55,8 @@ proofSearch elab fn nroot ist = psRec maxDepth

5455 let (f, _) = unApply t

5556 case f of

5657 P _ n _ -> case lookupCtxt n (idris_datatypes ist) of

57− [t] -> tryCons d (con_names t ++ getFn d fn)

58+ [t] -> tryCons d (hints ++ con_names t ++

59+ getFn d fn)

5860 _ -> fail "Not a data type"

5961 _ -> fail "Not a data type"

6062

@@ -82,6 +84,7 @@ proofSearch elab fn nroot ist = psRec maxDepth

8284 do let imps = case lookupCtxtName n (idris_implicits ist) of

8385 [] -> []

8486 [args] -> map isImp (snd args)

87+ _ -> fail "Ambiguous name"

8588 ps <- get_probs

8689 args <- apply (Var n) imps

8790 ps' <- get_probs

src/Idris/REPL.hs+13−4

@@ -588,6 +588,10 @@ process h fn (AddMissing updatefile l n)

588588 dens (PRef fc n) = PRef fc (nsroot n)

589589 dens t = t

590590

591+ nsroot (NS n _) = nsroot n

592+ nsroot (SN (WhereN _ _ n)) = nsroot n

593+ nsroot n = n

594+

591595 getAppName (PApp _ r _) = getAppName r

592596 getAppName (PRef _ r) = r

593597 getAppName _ = n

@@ -612,7 +616,7 @@ process h fn (MakeWith updatefile l n)

612616 unlines rest)

613617 runIO $ copyFile fb fn

614618 else ihputStrLn h with

615−process h fn (DoProofSearch updatefile l n)

619+process h fn (DoProofSearch updatefile l n hints)

616620 = do src <- runIO $ readFile fn

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

618622 ctxt <- getContext

@@ -625,8 +629,8 @@ process h fn (DoProofSearch updatefile l n)

625629 Just mi -> mi

626630 _ -> (Nothing, 0)

627631 let fc = fileFC fn

628− let body t = PProof [Try (TSeq Intros (ProofSearch top n))

629− (ProofSearch t n)]

632+ let body t = PProof [Try (TSeq Intros (ProofSearch t n hints))

633+ (ProofSearch t n hints)]

630634 let def = PClause fc mn (PRef fc mn) [] (body top) []

631635 newmv <- idrisCatch

632636 (do elabDecl' EAll toplevel (PClauses fc [] mn [def])

@@ -634,7 +638,8 @@ process h fn (DoProofSearch updatefile l n)

634638 ctxt <- getContext

635639 i <- getIState

636640 return $ show (stripNS

637− (dropCtxt envlen (delab i (normaliseAll ctxt [] tm)))))

641+ (dropCtxt envlen

642+ (delab i (specialise ctxt [] [(mn, 1)] tm)))))

638643 (\e -> return ("?" ++ show n))

639644 if updatefile then

640645 do let fb = fn ++ "~"

@@ -653,6 +658,10 @@ process h fn (DoProofSearch updatefile l n)

653658 dens (PRef fc n) = PRef fc (nsroot n)

654659 dens t = t

655660

661+ nsroot (NS n _) = nsroot n

662+ nsroot (SN (WhereN _ _ n)) = nsroot n

663+ nsroot n = n

664+

656665 updateMeta ('?':cs) n new

657666 | length cs >= length n

658667 = case splitAt (length n) cs of

src/Idris/REPLParser.hs+2−1

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

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

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

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

87− return (DoProofSearch upd (fromInteger l) n))

87+ hints <- many P.name

88+ return (DoProofSearch upd (fromInteger l) n hints))

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

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

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