git.iko.soy/Idris-dev
on master help sign in
If the goal is not a function type when elaborating \, invent one

...and attempt to solve it by unification

commitf1e61da283d37d30effd7dfba914ea968b004067 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 28 Mar 2013, 12:39 (14 years ago) parentb27ad3e
3 files changed+21
compare with master
unifiedsplit
CHANGELOG+2 src/Core/Elaborate.hs+17 src/Idris/ElabTerm.hs+2
CHANGELOG+2
@@ -9,10 +9,12 @@ User visible changes:
99* Tab completion in REPL
1010* Dynamic loading of C libraries in the interpreter
1111* Testing IO actions at the REPL with :x command
12+* Fixed some INTERNAL ERROR messages
1213
1314Internal changes:
1415
1516* Improved name disambiguation
17+* More flexible unification and elaboration of lambdas
1618* Various unification and totality checking bug fixes
1719
1820New in 0.9.7:
src/Core/Elaborate.hs+17
@@ -469,6 +469,23 @@ apply_elab n args =
469469 mkMN n@(UN x) = MN 1000 x
470470 mkMN (NS n ns) = NS (mkMN n) ns
471471
472+-- If the goal is not a Pi-type, invent some names and make it a pi type
473+checkPiGoal :: Elab' aux ()
474+checkPiGoal = do g <- goal
475+ case g of
476+ Bind _ (Pi _) _ -> return ()
477+ _ -> do a <- unique_hole (MN 0 "argTy")
478+ b <- unique_hole (MN 0 "retTy")
479+ f <- unique_hole (MN 0 "f")
480+ claim a RType
481+ claim b RType
482+ claim f (RBind (MN 0 "aX") (Pi (Var a)) (Var b))
483+ movelast a
484+ movelast b
485+ fill (Var f)
486+ solve
487+ focus f
488+
472489simple_app :: Elab' aux () -> Elab' aux () -> Elab' aux ()
473490simple_app fun arg =
474491 do a <- unique_hole (MN 0 "argTy")
src/Idris/ElabTerm.hs+2
@@ -230,6 +230,7 @@ elab ist info pattern tcgen fn tm
230230 -- let sc' = mapPT (repN n n') sc
231231 ptm <- get_term
232232 g <- goal
233+ checkPiGoal
233234 attack; intro (Just n);
234235 -- trace ("------ intro " ++ show n ++ " ---- \n" ++ show ptm)
235236 elabE (True, a) sc; solve
@@ -239,6 +240,7 @@ elab ist info pattern tcgen fn tm
239240 = do hsin <- get_holes
240241 ptmin <- get_term
241242 tyn <- unique_hole (MN 0 "lamty")
243+ checkPiGoal
242244 claim tyn RType
243245 attack
244246 ptm <- get_term