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

git.iko.soy/Idris-dev

on master help sign in

Proof search now also tries recursive calls

53ce3ccEdwin Brady13 years ago

src/Idris/AbsSyntax.hs+3−3

compare with master

unifiedsplit

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

281addDeferred = addDeferred' Ref

282addDeferredTyCon = addDeferred' (TCon 0 0)

283

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

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

285addDeferred' 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

287 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 ++

289 idris_metavars i }

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

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

src/Idris/AbsSyntaxTree.hs+2−2

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

102 idris_name :: Int,

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

104 -- ^ 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

106 idris_coercions :: [Name],

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

108 syntax_rules :: [Syntax],

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

615 | Equiv t

616 | MatchRefine Name

617 | LetTac Name t | LetTacTy Name t t

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

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

619 | Solve

620 | Attack

621 | ProofState | ProofTerm | Undo

src/Idris/Delaborate.hs+6−2

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

39 | n == unitCon = PTrue un

40 | n == falseTy = PFalse un

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

42+ | otherwise

43+ = case lookup n (idris_metavars ist) of

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

42− | otherwise = PRef un (dens n)

45+ _ -> PRef un (dens n)

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

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

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

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

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

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

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

83 (de env [] r)

86 (de env [] r)

84 deFn env (P _ n _) args

87 deFn env (P _ n _) args

85 = case lookup n (idris_metavars ist) of

88 = case lookup n (idris_metavars ist) of

89+ Just (Just _, mi) ->

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

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

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

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

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

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

src/Idris/ElabDecls.hs+6−6

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

41 return (tm, ty)

43checkDef fc ns = do ctxt <- getContext

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

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

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

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

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

48elabType :: ElabInfo -> SyntaxInfo -> String ->

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

86 _ -> False

87 _ -> False

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

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

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

90 addIBC (IBCDef n)

91 addDeferred ds

92 setFlags n opts'

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

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

364 erun fc $ psolve lhs_tm

365 tt <- get_term

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

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

367 return (tm, ds))

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

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

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

870 errAt "right hand side of " fname

871 (erun fc $ psolve lhs_tm)

872 tt <- get_term

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

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

874 return (tm, ds, is))

875 logLvl 5 "DONE CHECK"

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

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

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

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

1027 addIBC (IBCDef wname)

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

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

1029 addDeferred def'

1030

1031 -- in the subdecls, lhs becomes:

src/Idris/ElabTerm.hs+20−19

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

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

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

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

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

40build ist info pattern fn tm

41 = do elab ist info pattern False fn tm

42 ivs <- get_instances

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

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

65 is <- getAux

66 tt <- get_term

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

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

68 log <- getLog

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

70 else return (tm, ds, is)

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

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

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

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

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

78buildTC ist info pattern tcgen fn tm

79 = do elab ist info pattern tcgen fn tm

80 probs <- get_probs

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

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

85 is <- getAux

86 tt <- get_term

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

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

88 log <- getLog

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

90 else return (tm, ds, is)

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

646

647trivial' ist

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

649−proofSearch' ist n

649+proofSearch' ist top n

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

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

651

652

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

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

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

737 isImp arg = (False, priority arg)

738

739+collectDeferred :: Maybe Name ->

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

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

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

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

741 do ds <- get

742 do ds <- get

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

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

743− collectDeferred app

744+ collectDeferred top app

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

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

745− t' <- collectDeferred t

746+ t' <- collectDeferred top t

746− return (Bind n b' t')

747+ return (Bind n b' t')

747 where

748 where

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

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

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

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

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

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

751 return (b { binderTy = ty' })

752 return (b { binderTy = ty' })

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

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

753−collectDeferred t = return t

754+collectDeferred top t = return t

754

755

755-- Running tactics directly

756-- Running tactics directly

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

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

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

862 when autoSolve solveAll

863 when autoSolve solveAll

863 runT Compute = compute

864 runT Compute = compute

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

865 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

866 runT (Focus n) = focus n

867 runT (Focus n) = focus n

867 runT Solve = solve

868 runT Solve = solve

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

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

33 (tryAll xs) True

34 else tryAll xs

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

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

37−proofSearch elab nroot ist = psRec 10 where

37+proofSearch elab fn nroot ist = psRec maxDepth where

38+ maxDepth = 10

39+

38 psRec 0 = fail "Maximum depth reached"

40 psRec 0 = fail "Maximum depth reached"

39 psRec d = try' (trivial elab ist)

41 psRec d = try' (trivial elab ist)

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

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

43+ True)

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

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

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

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

47+ getFn d Nothing = []

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

49+ | otherwise = []

50+

44 resolveByCon d

51 resolveByCon d

45 = do t <- goal

52 = do t <- goal

46 let (f, _) = unApply t

53 let (f, _) = unApply t

47 case f of

54 case f of

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

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

50 _ -> fail "Not a data type"

57 _ -> fail "Not a data type"

51 _ -> fail "Not a data type"

58 _ -> fail "Not a data type"

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+

53 tryCons d [] = fail "Constructors failed"

69 tryCons d [] = fail "Constructors failed"

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

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

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+

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

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

57 tryCon d n

80 tryCon d n

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

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

428 case lookupNames n ctxt of

429 ts@(t:_) ->

430 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

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

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

434 ihPrintResult h ""

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

578process 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 n)) (ProofSearch n)]

582 ctxt <- getContext

581 ctxt <- getContext

583 mn <- case lookupNames n ctxt of

582 mn <- case lookupNames n ctxt of

584 [x] -> return x

583 [x] -> return x

585 [] -> return n

584 [] -> return n

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

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

587 i <- getIState

586 i <- getIState

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

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

589− Just mi -> mi

588+ Just mi -> mi

590− _ -> 0

589+ _ -> (Nothing, 0)

591 let fc = fileFC fn

590 let fc = fileFC fn

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

592+ (ProofSearch top n)]

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

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

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

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

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

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

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

645 insertMetavar n =

646 insertMetavar n =

646 do i <- getIState

647 do i <- getIState

647 let ms = idris_metavars i

648 let ms = idris_metavars i

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

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

649

650

650process h fn' (AddProof prf)

651process h fn' (AddProof prf)

651 = do fn <- do

652 = do fn <- do