53ce3cc · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Proof search now also tries recursive calls

Though not at the top level, only under a constructor, to avoid searching forever. (This can probably be improved simply to ensure that it doesn't try applying the top level function.)

commit53ce3cce5aa96559662f6f3043a6df72b0e663e0 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 30 Oct 2013, 01:51 (13 years ago) parentdcdbcc3

7 files changed+71−42

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+3−3 src/Idris/AbsSyntaxTree.hs+2−2 src/Idris/Delaborate.hs+6−2 src/Idris/ElabDecls.hs+6−6 src/Idris/ElabTerm.hs+20−19 src/Idris/ProofSearch.hs+27−4 src/Idris/REPL.hs+7−6

src/Idris/AbsSyntax.hs+3−3

@@ -281,11 +281,11 @@ addConstraints fc (v, cs)

281281addDeferred = addDeferred' Ref

282282addDeferredTyCon = addDeferred' (TCon 0 0)

283283

284−addDeferred' :: NameType -> [(Name, (Int, Type))] -> Idris ()

284+addDeferred' :: NameType -> [(Name, (Int, Maybe Name, Type))] -> Idris ()

285285addDeferred' nt ns

286− = do mapM_ (\(n, (i, t)) -> updateContext (addTyDecl n nt (tidyNames [] t))) ns

286+ = do mapM_ (\(n, (i, _, t)) -> updateContext (addTyDecl n nt (tidyNames [] t))) ns

287287 i <- getIState

288− putIState $ i { idris_metavars = map (\(n, (i, _)) -> (n, i)) ns ++

288+ putIState $ i { idris_metavars = map (\(n, (i, top, _)) -> (n, (top, i))) ns ++

289289 idris_metavars i }

290290 where tidyNames used (Bind (MN i x) b sc)

291291 = let n' = uniqueName (UN x) used in

src/Idris/AbsSyntaxTree.hs+2−2

@@ -102,7 +102,7 @@ data IState = IState {

102102 idris_name :: Int,

103103 idris_lineapps :: [((FilePath, Int), PTerm)],

104104 -- ^ Full application LHS on source line

105− idris_metavars :: [(Name, Int)], -- ^ The currently defined but not proven metavariables

105+ idris_metavars :: [(Name, (Maybe Name, Int))], -- ^ The currently defined but not proven metavariables

106106 idris_coercions :: [Name],

107107 idris_transforms :: [(Term, Term)],

108108 syntax_rules :: [Syntax],

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

615615 | Equiv t

616616 | MatchRefine Name

617617 | LetTac Name t | LetTacTy Name t t

618− | Exact t | Compute | Trivial | ProofSearch Name

618+ | Exact t | Compute | Trivial | ProofSearch (Maybe Name) Name

619619 | Solve

620620 | Attack

621621 | ProofState | ProofTerm | Undo

src/Idris/Delaborate.hs+6−2

@@ -39,7 +39,10 @@ delabTy' ist imps tm fullname = de [] imps tm

3939 | n == unitCon = PTrue un

4040 | n == falseTy = PFalse un

4141 | Just n' <- lookup n env = PRef un n'

42− | otherwise = PRef un (dens n)

42+ | otherwise

43+ = case lookup n (idris_metavars ist) of

44+ Just (Just _, mi) -> mkMVApp (dens n) []

45+ _ -> PRef un (dens n)

4346 de env _ (Bind n (Lam ty) sc)

4447 = PLam n (de env [] ty) (de ((n,n):env) [] sc)

4548 de env (PImp _ _ _ _ _ _:is) (Bind n (Pi ty) sc)

@@ -83,7 +86,8 @@ delabTy' ist imps tm fullname = de [] imps tm

8386 (de env [] r)

8487 deFn env (P _ n _) args

8588 = case lookup n (idris_metavars ist) of

86− Just mi | mi >=0 -> mkMVApp (dens n) (drop mi (map (de env []) args))

89+ Just (Just _, mi) ->

90+ mkMVApp (dens n) (drop mi (map (de env []) args))

8791 _ -> mkPApp (dens n) (map (de env []) args)

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

8993

src/Idris/ElabDecls.hs+6−6

@@ -41,8 +41,8 @@ recheckC fc env t

4141 return (tm, ty)

4242

4343checkDef fc ns = do ctxt <- getContext

44− mapM (\(n, (i, t)) -> do (t', _) <- recheckC fc [] t

45− return (n, (i, t'))) ns

44+ mapM (\(n, (i, top, t)) -> do (t', _) <- recheckC fc [] t

45+ return (n, (i, top, t'))) ns

4646

4747-- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".

4848elabType :: ElabInfo -> SyntaxInfo -> String ->

@@ -86,7 +86,7 @@ elabType info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty_in

8686 _ -> False

8787 _ -> False

8888 let opts' = if corec then (Coinductive : opts) else opts

89− ds <- checkDef fc [(n, (-1, nty))]

89+ ds <- checkDef fc [(n, (-1, Nothing, nty))]

9090 addIBC (IBCDef n)

9191 addDeferred ds

9292 setFlags n opts'

@@ -363,7 +363,7 @@ elabTransform info fc safe lhs_in rhs_in

363363 erun fc (build i info False (UN "transform") rhs)

364364 erun fc $ psolve lhs_tm

365365 tt <- get_term

366− let (tm, ds) = runState (collectDeferred tt) []

366+ let (tm, ds) = runState (collectDeferred Nothing tt) []

367367 return (tm, ds))

368368 (crhs_tm, crhs_ty) <- recheckC fc [] rhs'

369369 logLvl 3 ("Transform RHS " ++ show crhs_tm)

@@ -870,7 +870,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

870870 errAt "right hand side of " fname

871871 (erun fc $ psolve lhs_tm)

872872 tt <- get_term

873− let (tm, ds) = runState (collectDeferred tt) []

873+ let (tm, ds) = runState (collectDeferred (Just fname) tt) []

874874 return (tm, ds, is))

875875 logLvl 5 "DONE CHECK"

876876 logLvl 2 $ "---> " ++ show rhs'

@@ -1025,7 +1025,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

10251025 let imps = getImps wtype -- add to implicits context

10261026 putIState (i { idris_implicits = addDef wname imps (idris_implicits i) })

10271027 addIBC (IBCDef wname)

1028− def' <- checkDef fc [(wname, (-1, wtype))]

1028+ def' <- checkDef fc [(wname, (-1, Nothing, wtype))]

10291029 addDeferred def'

10301030

10311031 -- in the subdecls, lhs becomes:

src/Idris/ElabTerm.hs+20−19

@@ -36,7 +36,7 @@ toplevel = EInfo [] emptyContext id Nothing

3636-- Also find deferred names in the term and their types

3737

3838build :: IState -> ElabInfo -> Bool -> Name -> PTerm ->

39− ElabD (Term, [(Name, (Int, Type))], [PDecl])

39+ ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])

4040build ist info pattern fn tm

4141 = do elab ist info pattern False fn tm

4242 ivs <- get_instances

@@ -64,7 +64,7 @@ build ist info pattern fn tm

6464 ((_,_,_,e):es) -> lift (Error e)

6565 is <- getAux

6666 tt <- get_term

67− let (tm, ds) = runState (collectDeferred tt) []

67+ let (tm, ds) = runState (collectDeferred (Just fn) tt) []

6868 log <- getLog

6969 if (log /= "") then trace log $ return (tm, ds, is)

7070 else return (tm, ds, is)

@@ -74,7 +74,7 @@ build ist info pattern fn tm

7474-- know about yet on the LHS of a pattern def)

7575

7676buildTC :: IState -> ElabInfo -> Bool -> Bool -> Name -> PTerm ->

77− ElabD (Term, [(Name, (Int, Type))], [PDecl])

77+ ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])

7878buildTC ist info pattern tcgen fn tm

7979 = do elab ist info pattern tcgen fn tm

8080 probs <- get_probs

@@ -84,7 +84,7 @@ buildTC ist info pattern tcgen fn tm

8484 ((_,_,_,e):es) -> lift (Error e)

8585 is <- getAux

8686 tt <- get_term

87− let (tm, ds) = runState (collectDeferred tt) []

87+ let (tm, ds) = runState (collectDeferred (Just fn) tt) []

8888 log <- getLog

8989 if (log /= "") then trace log $ return (tm, ds, is)

9090 else return (tm, ds, is)

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

646646

647647trivial' ist

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

649−proofSearch' ist n

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

649+proofSearch' ist top n

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

651651

652652

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

@@ -736,21 +736,22 @@ resolveTC depth fn ist

736736 where isImp (PImp p _ _ _ _ _) = (True, p)

737737 isImp arg = (False, priority arg)

738738

739−collectDeferred :: Term -> State [(Name, (Int, Type))] Term

740−collectDeferred (Bind n (GHole i t) app) =

739+collectDeferred :: Maybe Name ->

740+ Term -> State [(Name, (Int, Maybe Name, Type))] Term

741+collectDeferred top (Bind n (GHole i t) app) =

741742 do ds <- get

742− when (not (n `elem` map fst ds)) $ put ((n, (i, t)) : ds)

743− collectDeferred app

744−collectDeferred (Bind n b t) = do b' <- cdb b

745− t' <- collectDeferred t

746− return (Bind n b' t')

743+ when (not (n `elem` map fst ds)) $ put ((n, (i, top, t)) : ds)

744+ collectDeferred top app

745+collectDeferred top (Bind n b t) = do b' <- cdb b

746+ t' <- collectDeferred top t

747+ return (Bind n b' t')

747748 where

748− cdb (Let t v) = liftM2 Let (collectDeferred t) (collectDeferred v)

749− cdb (Guess t v) = liftM2 Guess (collectDeferred t) (collectDeferred v)

750− cdb b = do ty' <- collectDeferred (binderTy b)

749+ cdb (Let t v) = liftM2 Let (collectDeferred top t) (collectDeferred top v)

750+ cdb (Guess t v) = liftM2 Guess (collectDeferred top t) (collectDeferred top v)

751+ cdb b = do ty' <- collectDeferred top (binderTy b)

751752 return (b { binderTy = ty' })

752−collectDeferred (App f a) = liftM2 App (collectDeferred f) (collectDeferred a)

753−collectDeferred t = return t

753+collectDeferred top (App f a) = liftM2 App (collectDeferred top f) (collectDeferred top a)

754+collectDeferred top t = return t

754755

755756-- Running tactics directly

756757-- if a tactic adds unification problems, return an error

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

862863 when autoSolve solveAll

863864 runT Compute = compute

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

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

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

866867 runT (Focus n) = focus n

867868 runT Solve = solve

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

src/Idris/ProofSearch.hs+27−4

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

3333 (tryAll xs) True

3434 else tryAll xs

3535

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

37−proofSearch elab nroot ist = psRec 10 where

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

37+proofSearch elab fn nroot ist = psRec maxDepth where

38+ maxDepth = 10

39+

3840 psRec 0 = fail "Maximum depth reached"

3941 psRec d = try' (trivial elab ist)

40− (try' (resolveByCon (d - 1))

42+ (try' (try' (resolveByCon (d - 1)) (resolveByLocals (d - 1))

43+ True)

4144 -- if all else fails, make a new metavariable

4245 (do attack; defer nroot; solve) True) True

4346

47+ getFn d Nothing = []

48+ getFn d (Just f) | d < maxDepth-1 = [f]

49+ | otherwise = []

50+

4451 resolveByCon d

4552 = do t <- goal

4653 let (f, _) = unApply t

4754 case f of

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

49− [t] -> tryCons d (con_names t)

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

5057 _ -> fail "Not a data type"

5158 _ -> fail "Not a data type"

5259

60+ -- if there are local variables which have a function type, try

61+ -- applying them too

62+ resolveByLocals d

63+ = do env <- get_env

64+ tryLocals d env

65+

66+ tryLocals d [] = fail "Locals failed"

67+ tryLocals d ((x, t) : xs) = try' (tryLocal d x t) (tryLocals d xs) True

68+

5369 tryCons d [] = fail "Constructors failed"

5470 tryCons d (c : cs) = try' (tryCon d c) (tryCons d cs) True

5571

72+ tryLocal d n t = do let a = getPArity (delab ist (binderTy t))

73+ tryLocalArg d n a

74+

75+ tryLocalArg d n 0 = elab (PRef (fileFC "prf") n)

76+ tryLocalArg d n i = simple_app (tryLocalArg d n (i - 1))

77+ (psRec d) "proof search local apply"

78+

5679 -- Like type class resolution, but searching with constructors

5780 tryCon d n

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

src/Idris/REPL.hs+7−6

@@ -428,7 +428,7 @@ process h fn (Check (PRef _ n))

428428 case lookupNames n ctxt of

429429 ts@(t:_) ->

430430 case lookup t (idris_metavars ist) of

431− Just i -> showMetavarInfo c imp ist n i

431+ Just (_, i) -> showMetavarInfo c imp ist n i

432432 Nothing -> do mapM_ (\n -> ihputStrLn h $ showName (Just ist) [] False c n ++ " : " ++

433433 showImp (Just ist) imp c (delabTy ist n)) ts

434434 ihPrintResult h ""

@@ -578,17 +578,18 @@ process h fn (MakeWith updatefile l n)

578578process h fn (DoProofSearch updatefile l n)

579579 = do src <- runIO $ readFile fn

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

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

582581 ctxt <- getContext

583582 mn <- case lookupNames n ctxt of

584583 [x] -> return x

585584 [] -> return n

586585 ns -> ierror (CantResolveAlts (map show ns))

587586 i <- getIState

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

589− Just mi -> mi

590− _ -> 0

587+ let (top, envlen) = case lookup mn (idris_metavars i) of

588+ Just mi -> mi

589+ _ -> (Nothing, 0)

591590 let fc = fileFC fn

591+ let body = PProof [Try (TSeq Intros (ProofSearch top n))

592+ (ProofSearch top n)]

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

593594 elabDecls toplevel [PClauses fc [] mn [def]]

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

@@ -645,7 +646,7 @@ process h fn (RmProof n')

645646 insertMetavar n =

646647 do i <- getIState

647648 let ms = idris_metavars i

648− putIState $ i { idris_metavars = (n, 0) : ms }

649+ putIState $ i { idris_metavars = (n, (Nothing, 0)) : ms }

649650

650651process h fn' (AddProof prf)

651652 = do fn <- do