8c93763 · Idris-dev · git.iko.soy

src/Core/Elaborate.hs+1−1

compare with master

unifiedsplit

@@ -422,7 +422,6 @@ apply' fillt fn imps =

422 do args <- prepare_apply fn (map fst imps)

423 env <- get_env

424 g <- goal

425− fillt (raw_apply fn (map Var args))

426 -- _Don't_ solve the arguments we're specifying by hand.

425 -- _Don't_ solve the arguments we're specifying by hand.

427 -- (remove from unified list before calling end_unify)

426 -- (remove from unified list before calling end_unify)

428 -- HMMM: Actually, if we get it wrong, the typechecker will complain!

427 -- HMMM: Actually, if we get it wrong, the typechecker will complain!

@@ -442,6 +441,7 @@ apply' fillt fn imps =

442 keepGiven dont hunis hs

441 keepGiven dont hunis hs

443 put (ES (p { dontunify = dont, unified = (n, unify),

442 put (ES (p { dontunify = dont, unified = (n, unify),

444 notunified = notunify ++ notunified p }, a) s prev)

443 notunified = notunify ++ notunified p }, a) s prev)

444+ fillt (raw_apply fn (map Var args))

445 ptm <- get_term

446 g <- goal

447-- trace ("Goal " ++ show g ++ "\n" ++ show (fn, imps, unify) ++ "\n" ++ show ptm) $

src/Idris/AbsSyntax.hs+3−3

@@ -650,12 +650,12 @@ inferTy = MN 0 "__Infer"

650inferCon = MN 0 "__infer"

651inferDecl = PDatadecl inferTy

652 PType

653− [("", inferCon, PPi impl (MN 0 "A") PType (

653+ [("", inferCon, PPi impl (MN 0 "iType") PType (

654− PPi expl (MN 0 "a") (PRef bi (MN 0 "A"))

654+ PPi expl (MN 0 "ival") (PRef bi (MN 0 "iType"))

655 (PRef bi inferTy)), bi)]

656inferOpts = []

657

658−infTerm t = PApp bi (PRef bi inferCon) [pimp (MN 0 "A") Placeholder True, pexp t]

658+infTerm t = PApp bi (PRef bi inferCon) [pimp (MN 0 "iType") Placeholder True, pexp t]

659infP = P (TCon 6 0) inferTy (TType (UVal 0))

660

661getInferTerm, getInferType :: Term -> Term

src/Idris/CaseSplit.hs+1−1

@@ -221,7 +221,7 @@ replaceVar ctxt n t (PApp fc f pats) = PApp fc f (map substArg pats)

221 subst (PApp fc (PRef _ t) pats)

222 | isTConName t ctxt = Placeholder -- infer types

223 subst (PApp fc f pats) = PApp fc f (map substArg pats)

224− subst (PEq fc l r) = PEq fc (subst l) (subst r)

224+ subst (PEq fc l r) = Placeholder -- PEq fc (subst l) (subst r)

225 subst x = x

226

227 substArg arg = arg { getTm = subst (getTm arg) }