3d2fa6c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Better elaboration of applications

3d2fa6cEdwin Brady11 years ago

src/Idris/Core/Elaborate.hs+52−3

compare with master

unifiedsplit

@@ -353,6 +353,9 @@ claimFn n bn t = processTactic' (ClaimFn n bn t)

353unifyGoal :: Raw -> Elab' aux ()

354unifyGoal t = processTactic' (UnifyGoal t)

355

356+unifyTerms :: Raw -> Raw -> Elab' aux ()

357+unifyTerms t1 t2 = processTactic' (UnifyTerms t1 t2)

358+

356exact :: Raw -> Elab' aux ()

359exact :: Raw -> Elab' aux ()

357exact t = processTactic' (Exact t)

360exact t = processTactic' (Exact t)

358

361

@@ -724,7 +727,12 @@ checkPiGoal n

724 focus f

727 focus f

725

728

726simple_app :: Bool -> Elab' aux () -> Elab' aux () -> String -> Elab' aux ()

729simple_app :: Bool -> Elab' aux () -> Elab' aux () -> String -> Elab' aux ()

727−simple_app infer fun arg str =

730+simple_app infer fun arg str =

731+ try (dep_app fun arg str)

732+ (infer_app infer fun arg str)

733+

734+infer_app :: Bool -> Elab' aux () -> Elab' aux () -> String -> Elab' aux ()

735+infer_app infer fun arg str =

728 do a <- getNameFrom (sMN 0 "__argTy")

736 do a <- getNameFrom (sMN 0 "__argTy")

729 b <- getNameFrom (sMN 0 "__retTy")

737 b <- getNameFrom (sMN 0 "__retTy")

730 f <- getNameFrom (sMN 0 "f")

738 f <- getNameFrom (sMN 0 "f")

@@ -755,8 +763,49 @@ simple_app infer fun arg str =

755 when (a `elem` hs) $ do movelast a

763 when (a `elem` hs) $ do movelast a

756 when (b `elem` hs) $ do movelast b

764 when (b `elem` hs) $ do movelast b

757 end_unify

765 end_unify

758− where

766+

759− regretWith err = try regret (lift $ tfail err)

767+dep_app :: Elab' aux () -> Elab' aux () -> String -> Elab' aux ()

768+dep_app fun arg str =

769+ do a <- getNameFrom (sMN 0 "__argTy")

770+ b <- getNameFrom (sMN 0 "__retTy")

771+ fty <- getNameFrom (sMN 0 "__fnTy")

772+ f <- getNameFrom (sMN 0 "f")

773+ s <- getNameFrom (sMN 0 "s")

774+ claim a RType

775+ claim fty RType

776+ claim f (Var fty)

777+ tm <- get_term

778+ g <- goal

779+ start_unify s

780+ claim s (Var a)

781+

782+ prep_fill f [s]

783+ focus f; attack; fun

784+ end_unify

785+ fty <- goal

786+ solve

787+ focus s; attack;

788+ ctxt <- get_context

789+ env <- get_env

790+ case normalise ctxt env fty of

791+ -- if f gives a function type, unify our argument type with

792+ -- f's expected argument type

793+ Bind _ (Pi _ argty _) _ -> unifyGoal (forget argty)

794+ -- Can't infer a type for 'f', so fail here (and drop back to

795+ -- simply typed application where we infer the type for f)

796+ _ -> fail "Can't make type"

797+ end_unify

798+ arg

799+ solve

800+ complete_fill

801+

802+ -- We don't need a and b in the hole queue any more since they were

803+ -- just for checking f, so move them to the end. If they never end up

804+ -- getting solved, we'll get an 'Incomplete term' error.

805+ hs <- get_holes

806+ when (a `elem` hs) $ do movelast a

807+ when (b `elem` hs) $ do movelast b

808+ end_unify

760

809

761-- Abstract over an argument of unknown type, giving a name for the hole

810-- Abstract over an argument of unknown type, giving a name for the hole

762-- which we'll fill with the argument type too.

811-- which we'll fill with the argument type too.

src/Idris/Core/ProofState.hs+10

@@ -91,6 +91,7 @@ data Tactic = Attack

91 | MatchProblems Bool

92 | UnifyProblems

93 | UnifyGoal Raw

94+ | UnifyTerms Raw Raw

94 | ProofState

95 | ProofState

95 | Undo

96 | Undo

96 | QED

97 | QED

@@ -477,6 +478,13 @@ unifyGoal tm ctxt env h@(Bind x b sc) =

477 return h

478 return h

478unifyGoal _ _ _ _ = fail "The focus is not a binder."

479unifyGoal _ _ _ _ = fail "The focus is not a binder."

479

480

481+unifyTerms :: Raw -> Raw -> RunTactic

482+unifyTerms tm1 tm2 ctxt env h =

483+ do (tm1v, _) <- lift $ check ctxt env tm1

484+ (tm2v, _) <- lift $ check ctxt env tm2

485+ ns' <- unify' ctxt env (tm1v, Nothing) (tm2v, Nothing)

486+ return h

487+

480exact :: Raw -> RunTactic

488exact :: Raw -> RunTactic

481exact guess ctxt env (Bind x (Hole ty) sc) =

489exact guess ctxt env (Bind x (Hole ty) sc) =

482 do (val, valty) <- lift $ check ctxt env guess

490 do (val, valty) <- lift $ check ctxt env guess

@@ -1113,3 +1121,5 @@ process t h = tactic (Just h) (mktac t)

1113 mktac (SetInjective n) = setinj n

1121 mktac (SetInjective n) = setinj n

1114 mktac (MoveLast n) = movelast n

1122 mktac (MoveLast n) = movelast n

1115 mktac (UnifyGoal r) = unifyGoal r

1123 mktac (UnifyGoal r) = unifyGoal r

1124+ mktac (UnifyTerms x y) = unifyTerms x y

1125+

test/reg001/reg001.idr+6

@@ -191,3 +191,9 @@ bar = case foom 5 of

191 Nothing => print 42

192 Just n => print n

193

194+Max : (Nat -> Type) -> Type

195+Max p = (Nat , (k : Nat) -> p k -> Nat)

196+

197+maxEquiv : Max p -> (n1 : Nat) -> p n1 -> Nat

198+maxEquiv a n1 pr1 = snd a n1 pr1

199+