Permalink
Browse files

Fix a tactic implicit bug when argument given explicitly

  • Loading branch information...
1 parent 21ffb28 commit 1f95beb86753106a7fdfb28f73e290b88079a6bc Edwin Brady committed May 4, 2012
Showing with 27 additions and 8 deletions.
  1. +8 −0 CHANGELOG
  2. +4 −4 lib/builtins.idr
  3. +3 −0 lib/io.idr
  4. +10 −3 src/Idris/AbsSyntax.hs
  5. +2 −1 src/Idris/ElabDecls.hs
View
@@ -3,9 +3,17 @@ New in 0.9.3:
User visible changes:
+* Named class instances
+* Added ':set' command, with options 'errorcontext' for displaying local
+ variables in scope when a unification error occurs, and 'showimplicits'
+ for displaying elaborated terms in full
+* Added '--errorcontext' command line swithc
+* Various minor REPL improvements and fixes
+
Internal changes:
* Normalise before forcing to catch more forceable arguments
+* Types no longer exported in normal form
New in 0.9.2:
-------------
View
@@ -85,11 +85,11 @@ not : Bool -> Bool
not True = False
not False = True
-infixl 5 ==, /=, ==.
-infixl 6 <, <=, >, >=, <., <=., >., >=.
+infixl 5 ==, /=
+infixl 6 <, <=, >, >=
infixl 7 <<, >>
-infixl 8 +,-,++,+.,-.
-infixl 9 *,/,*.,/.
+infixl 8 +,-,++
+infixl 9 *,/
--- Numeric operators
View
@@ -8,6 +8,9 @@ abstract
io_bind : IO a -> (a -> IO b) -> IO b
io_bind (prim__IO v) k = k v
+unsafePerformIO : IO a -> a
+unsafePerformIO (prim__IO x) = x
+
abstract
io_return : a -> IO a
io_return x = prim__IO x
@@ -56,6 +56,7 @@ data IState = IState { tt_ctxt :: Context,
idris_patdefs :: Ctxt [([Name], Term, Term)], -- not exported
idris_flags :: Ctxt [FnOpt],
idris_callgraph :: Ctxt [Name],
+ idris_calledgraph :: Ctxt [Name],
idris_totcheck :: [(FC, Name)],
idris_log :: String,
idris_options :: IOption,
@@ -103,7 +104,7 @@ data IBCWrite = IBCFix FixDecl
idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext
emptyContext emptyContext emptyContext emptyContext
- emptyContext emptyContext
+ emptyContext emptyContext emptyContext
[] "" defaultOpts 6 [] [] [] [] [] [] [] []
Nothing Nothing Nothing [] [] [] Hidden [] Nothing
@@ -158,6 +159,9 @@ addToCG :: Name -> [Name] -> Idris ()
addToCG n ns = do i <- get
put (i { idris_callgraph = addDef n ns (idris_callgraph i) })
+addToCalledG :: Name -> [Name] -> Idris ()
+addToCalledG n ns = return () -- TODO
+
-- Add a class instance function. Dodgy hack: Put integer instances first in the
-- list so they are resolved by default.
@@ -1658,14 +1662,17 @@ aiFn inpat ist fc f as
insertImpl (PTacImplicit p l n sc ty : ps) given =
case find n given [] of
Just (tm, given') -> PTacImplicit p l n sc tm : insertImpl ps given'
- Nothing -> PTacImplicit p l n sc sc
- : insertImpl ps given
+ Nothing -> if inpat
+ then PTacImplicit p l n sc Placeholder : insertImpl ps given
+ else PTacImplicit p l n sc sc : insertImpl ps given
insertImpl expected [] = []
insertImpl _ given = given
find n [] acc = Nothing
find n (PImp _ _ n' t : gs) acc
| n == n' = Just (t, reverse acc ++ gs)
+ find n (PTacImplicit _ _ n' _ t : gs) acc
+ | n == n' = Just (t, reverse acc ++ gs)
find n (g : gs) acc = find n gs (g : acc)
mkPApp fc a f [] = f
@@ -299,6 +299,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
do let ns = namesUsed sc \\ scargs
logLvl 2 $ "Called names: " ++ show ns
addToCG n ns
+ addToCalledG n ns -- plus names in type!
addIBC (IBCCG n)
_ -> return ()
-- addIBC (IBCTotal n tot)
@@ -380,7 +381,7 @@ elabClause info tcgen (PClause fc fname lhs_in withs rhs_in whereblock)
let decls = concatMap declared whereblock
let newargs = pvars ist lhs_tm
let wb = map (expandParamsD ist decorate newargs decls) whereblock
- logLvl 5 $ show wb
+ logLvl 5 $ "Where block: " ++ show wb
mapM_ (elabDecl' info) wb
-- Now build the RHS, using the type of the LHS as the goal.
i <- get -- new implicits from where block

0 comments on commit 1f95beb

Please sign in to comment.