git.iko.soy/Idris-dev
on master help sign in
Fix a tactic implicit bug when argument given explicitly
commit1f95beb86753106a7fdfb28f73e290b88079a6bc authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateFri 4 May 2012, 13:35 (14 years ago) parent21ffb28
5 files changed+27−8
compare with master
unifiedsplit
CHANGELOG+8 lib/builtins.idr+4−4 lib/io.idr+3 src/Idris/AbsSyntax.hs+10−3 src/Idris/ElabDecls.hs+2−1
CHANGELOG+8
@@ -3,9 +3,17 @@ New in 0.9.3:
33
44User visible changes:
55
6+* Named class instances
7+* Added ':set' command, with options 'errorcontext' for displaying local
8+ variables in scope when a unification error occurs, and 'showimplicits'
9+ for displaying elaborated terms in full
10+* Added '--errorcontext' command line swithc
11+* Various minor REPL improvements and fixes
12+
613Internal changes:
714
815* Normalise before forcing to catch more forceable arguments
16+* Types no longer exported in normal form
917
1018New in 0.9.2:
1119-------------
lib/builtins.idr+4−4
@@ -85,11 +85,11 @@ not : Bool -> Bool
8585not True = False
8686not False = True
8787
88−infixl 5 ==, /=, ==.
89−infixl 6 <, <=, >, >=, <., <=., >., >=.
88+infixl 5 ==, /=
89+infixl 6 <, <=, >, >=
9090infixl 7 <<, >>
91−infixl 8 +,-,++,+.,-.
92−infixl 9 *,/,*.,/.
91+infixl 8 +,-,++
92+infixl 9 *,/
9393
9494--- Numeric operators
9595
lib/io.idr+3
@@ -8,6 +8,9 @@ abstract
88io_bind : IO a -> (a -> IO b) -> IO b
99io_bind (prim__IO v) k = k v
1010
11+unsafePerformIO : IO a -> a
12+unsafePerformIO (prim__IO x) = x
13+
1114abstract
1215io_return : a -> IO a
1316io_return x = prim__IO x
src/Idris/AbsSyntax.hs+10−3
@@ -56,6 +56,7 @@ data IState = IState { tt_ctxt :: Context,
5656 idris_patdefs :: Ctxt [([Name], Term, Term)], -- not exported
5757 idris_flags :: Ctxt [FnOpt],
5858 idris_callgraph :: Ctxt [Name],
59+ idris_calledgraph :: Ctxt [Name],
5960 idris_totcheck :: [(FC, Name)],
6061 idris_log :: String,
6162 idris_options :: IOption,
@@ -103,7 +104,7 @@ data IBCWrite = IBCFix FixDecl
103104
104105idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext
105106 emptyContext emptyContext emptyContext emptyContext
106− emptyContext emptyContext
107+ emptyContext emptyContext emptyContext
107108 [] "" defaultOpts 6 [] [] [] [] [] [] [] []
108109 Nothing Nothing Nothing [] [] [] Hidden [] Nothing
109110
@@ -158,6 +159,9 @@ addToCG :: Name -> [Name] -> Idris ()
158159addToCG n ns = do i <- get
159160 put (i { idris_callgraph = addDef n ns (idris_callgraph i) })
160161
162+addToCalledG :: Name -> [Name] -> Idris ()
163+addToCalledG n ns = return () -- TODO
164+
161165-- Add a class instance function. Dodgy hack: Put integer instances first in the
162166-- list so they are resolved by default.
163167
@@ -1658,14 +1662,17 @@ aiFn inpat ist fc f as
16581662 insertImpl (PTacImplicit p l n sc ty : ps) given =
16591663 case find n given [] of
16601664 Just (tm, given') -> PTacImplicit p l n sc tm : insertImpl ps given'
1661− Nothing -> PTacImplicit p l n sc sc
1662− : insertImpl ps given
1665+ Nothing -> if inpat
1666+ then PTacImplicit p l n sc Placeholder : insertImpl ps given
1667+ else PTacImplicit p l n sc sc : insertImpl ps given
16631668 insertImpl expected [] = []
16641669 insertImpl _ given = given
16651670
16661671 find n [] acc = Nothing
16671672 find n (PImp _ _ n' t : gs) acc
16681673 | n == n' = Just (t, reverse acc ++ gs)
1674+ find n (PTacImplicit _ _ n' _ t : gs) acc
1675+ | n == n' = Just (t, reverse acc ++ gs)
16691676 find n (g : gs) acc = find n gs (g : acc)
16701677
16711678mkPApp fc a f [] = f
src/Idris/ElabDecls.hs+2−1
@@ -299,6 +299,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
299299 do let ns = namesUsed sc \\ scargs
300300 logLvl 2 $ "Called names: " ++ show ns
301301 addToCG n ns
302+ addToCalledG n ns -- plus names in type!
302303 addIBC (IBCCG n)
303304 _ -> return ()
304305-- addIBC (IBCTotal n tot)
@@ -380,7 +381,7 @@ elabClause info tcgen (PClause fc fname lhs_in withs rhs_in whereblock)
380381 let decls = concatMap declared whereblock
381382 let newargs = pvars ist lhs_tm
382383 let wb = map (expandParamsD ist decorate newargs decls) whereblock
383− logLvl 5 $ show wb
384+ logLvl 5 $ "Where block: " ++ show wb
384385 mapM_ (elabDecl' info) wb
385386 -- Now build the RHS, using the type of the LHS as the goal.
386387 i <- get -- new implicits from where block