dcdbcc3 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Proof search now tries appropriate constructors

It will take the first one which works, which will not always be what you want, of course, but if there is enough structure in the type then it limits the ones which are valid. \o in vim invokes proof search.

commitdcdbcc344cdf2f205f4c64e7764c3e98dc12f813 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 29 Oct 2013, 21:55 (13 years ago) parent2474e10

4 files changed+45−7

compare with master

unifiedsplit

src/Idris/Delaborate.hs+1−1 src/Idris/ElabDecls.hs+2−2 src/Idris/ProofSearch.hs+36−3 src/Idris/REPL.hs+6−1

src/Idris/Delaborate.hs+1−1

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

8383 (de env [] r)

8484 deFn env (P _ n _) args

8585 = case lookup n (idris_metavars ist) of

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

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

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

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

8989

src/Idris/ElabDecls.hs+2−2

@@ -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, (0, nty))]

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

9090 addIBC (IBCDef n)

9191 addDeferred ds

9292 setFlags n opts'

@@ -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, (0, wtype))]

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

10291029 addDeferred def'

10301030

10311031 -- in the subdecls, lhs becomes:

src/Idris/ProofSearch.hs+36−3

@@ -10,6 +10,9 @@ import Idris.AbsSyntax

1010import Idris.Delaborate

1111import Idris.Error

1212

13+import Control.Monad

14+import Debug.Trace

15+

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

1417

1518trivial :: (PTerm -> ElabD ()) -> IState -> ElabD ()

@@ -31,8 +34,38 @@ trivial elab ist = try' (do elab (PRefl (fileFC "prf") Placeholder)

3134 else tryAll xs

3235

3336proofSearch :: (PTerm -> ElabD ()) -> Name -> IState -> ElabD ()

34−proofSearch elab nroot ist

35− = try (trivial elab ist)

36− (do attack; defer nroot; solve)

37+proofSearch elab nroot ist = psRec 10 where

38+ psRec 0 = fail "Maximum depth reached"

39+ psRec d = try' (trivial elab ist)

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

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

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

3743

44+ resolveByCon d

45+ = do t <- goal

46+ let (f, _) = unApply t

47+ case f of

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

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

50+ _ -> fail "Not a data type"

51+ _ -> fail "Not a data type"

3852

53+ tryCons d [] = fail "Constructors failed"

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

55+

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

57+ tryCon d n

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

59+ [] -> []

60+ [args] -> map isImp (snd args)

61+ ps <- get_probs

62+ args <- apply (Var n) imps

63+ ps' <- get_probs

64+ when (length ps < length ps') $ fail "Can't apply constructor"

65+ mapM_ (\ (_, h) -> do focus h

66+ psRec d)

67+ (filter (\ (x, y) -> not x) (zip (map fst imps) args))

68+ solve

69+

70+ isImp (PImp p _ _ _ _ _) = (True, p)

71+ isImp arg = (False, priority arg)

src/Idris/REPL.hs+6−1

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

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

595595 ctxt <- getContext

596596 i <- getIState

597− let newmv = show (dropCtxt envlen (delab i (normaliseAll ctxt [] tm)))

597+ let newmv = show (stripNS

598+ (dropCtxt envlen (delab i (normaliseAll ctxt [] tm))))

598599 if updatefile then

599600 do let fb = fn ++ "~"

600601 runIO $ writeFile fb (unlines before ++

@@ -607,6 +608,10 @@ process h fn (DoProofSearch updatefile l n)

607608 dropCtxt i (PLet _ _ _ sc) = dropCtxt (i - 1) sc

608609 dropCtxt i (PLam _ _ sc) = dropCtxt (i - 1) sc

609610 dropCtxt _ t = t

611+

612+ stripNS tm = mapPT dens tm where

613+ dens (PRef fc n) = PRef fc (nsroot n)

614+ dens t = t

610615

611616 updateMeta ('?':cs) n new

612617 | length cs >= length n