@@ -353,6 +353,9 @@ claimFn n bn t = processTactic' (ClaimFn n bn t)
353353unifyGoal :: Raw -> Elab' aux ()
354354unifyGoal t = processTactic' (UnifyGoal t)
355355
356+unifyTerms :: Raw -> Raw -> Elab' aux ()
357+unifyTerms t1 t2 = processTactic' (UnifyTerms t1 t2)
358+
356359exact :: Raw -> Elab' aux ()
357360exact t = processTactic' (Exact t)
358361
@@ -724,7 +727,12 @@ checkPiGoal n
724727 focus f
725728
726729simple_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 =
728736 do a <- getNameFrom (sMN 0 "__argTy")
729737 b <- getNameFrom (sMN 0 "__retTy")
730738 f <- getNameFrom (sMN 0 "f")
@@ -755,8 +763,49 @@ simple_app infer fun arg str =
755763 when (a `elem` hs) $ do movelast a
756764 when (b `elem` hs) $ do movelast b
757765 end_unify
758− where
759− regretWith err = try regret (lift $ tfail err)
766+
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
760809
761810-- Abstract over an argument of unknown type, giving a name for the hole
762811-- which we'll fill with the argument type too.