dcdbcc3 · Idris-dev · git.iko.soy

src/Idris/Delaborate.hs+1−1

compare with master

unifiedsplit

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

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

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

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

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

89

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

86 _ -> False

87 _ -> False

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

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

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

90 addIBC (IBCDef n)

91 addDeferred ds

92 setFlags n opts'

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

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

1029 addDeferred def'

1030

1031 -- in the subdecls, lhs becomes:

src/Idris/ProofSearch.hs+36−3

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

10import Idris.Delaborate

11import Idris.Error

12

13+import Control.Monad

14+import Debug.Trace

15+

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

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

14

17

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

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

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

31 else tryAll xs

34 else tryAll xs

32

35

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

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

34−proofSearch elab nroot ist

37+proofSearch elab nroot ist = psRec 10 where

38+ psRec 0 = fail "Maximum depth reached"

35− = try (trivial elab ist)

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

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

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

36− (do attack; defer nroot; solve)

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

37

43

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"

38

52

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)

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

595 ctxt <- getContext

596 i <- getIState

597+ let newmv = show (stripNS

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

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

598 if updatefile then

599 if updatefile then

599 do let fb = fn ++ "~"

600 do let fb = fn ++ "~"

600 runIO $ writeFile fb (unlines before ++

601 runIO $ writeFile fb (unlines before ++

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

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

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

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

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

609 dropCtxt _ t = t

610 dropCtxt _ t = t

611+

612+ stripNS tm = mapPT dens tm where

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

614+ dens t = t

610

615

611 updateMeta ('?':cs) n new

616 updateMeta ('?':cs) n new

612 | length cs >= length n

617 | length cs >= length n