git.iko.soy/Idris-dev
on master help sign in
Fix a tactic implicit bug when argument given explicitly
1f95bebEdwin Brady
CHANGELOG+8
compare with master
unifiedsplit
@@ -3,9 +3,17 @@ New in 0.9.3:
3
3
4User visible changes:
4User visible changes:
5
5
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+
6Internal changes:
13Internal changes:
7
14
8* Normalise before forcing to catch more forceable arguments
15* Normalise before forcing to catch more forceable arguments
16+* Types no longer exported in normal form
9
17
10New in 0.9.2:
18New in 0.9.2:
11-------------
19-------------
lib/builtins.idr+4−4
@@ -85,11 +85,11 @@ not : Bool -> Bool
85not True = False
85not True = False
86not False = True
86not False = True
87
87
88−infixl 5 ==, /=, ==.
88+infixl 5 ==, /=
89−infixl 6 <, <=, >, >=, <., <=., >., >=.
89+infixl 6 <, <=, >, >=
90infixl 7 <<, >>
90infixl 7 <<, >>
91−infixl 8 +,-,++,+.,-.
91+infixl 8 +,-,++
92−infixl 9 *,/,*.,/.
92+infixl 9 *,/
93
93
94--- Numeric operators
94--- Numeric operators
95
95
lib/io.idr+3
@@ -8,6 +8,9 @@ abstract
8io_bind : IO a -> (a -> IO b) -> IO b
8io_bind : IO a -> (a -> IO b) -> IO b
9io_bind (prim__IO v) k = k v
9io_bind (prim__IO v) k = k v
10
10
11+unsafePerformIO : IO a -> a
12+unsafePerformIO (prim__IO x) = x
13+
11abstract
14abstract
12io_return : a -> IO a
15io_return : a -> IO a
13io_return x = prim__IO x
16io_return x = prim__IO x
src/Idris/AbsSyntax.hs+10−3
@@ -56,6 +56,7 @@ data IState = IState { tt_ctxt :: Context,
56 idris_patdefs :: Ctxt [([Name], Term, Term)], -- not exported
56 idris_patdefs :: Ctxt [([Name], Term, Term)], -- not exported
57 idris_flags :: Ctxt [FnOpt],
57 idris_flags :: Ctxt [FnOpt],
58 idris_callgraph :: Ctxt [Name],
58 idris_callgraph :: Ctxt [Name],
59+ idris_calledgraph :: Ctxt [Name],
59 idris_totcheck :: [(FC, Name)],
60 idris_totcheck :: [(FC, Name)],
60 idris_log :: String,
61 idris_log :: String,
61 idris_options :: IOption,
62 idris_options :: IOption,
@@ -103,7 +104,7 @@ data IBCWrite = IBCFix FixDecl
103
104
104idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext
105idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext
105 emptyContext emptyContext emptyContext emptyContext
106 emptyContext emptyContext emptyContext emptyContext
106− emptyContext emptyContext
107+ emptyContext emptyContext emptyContext
107 [] "" defaultOpts 6 [] [] [] [] [] [] [] []
108 [] "" defaultOpts 6 [] [] [] [] [] [] [] []
108 Nothing Nothing Nothing [] [] [] Hidden [] Nothing
109 Nothing Nothing Nothing [] [] [] Hidden [] Nothing
109
110
@@ -158,6 +159,9 @@ addToCG :: Name -> [Name] -> Idris ()
158addToCG n ns = do i <- get
159addToCG n ns = do i <- get
159 put (i { idris_callgraph = addDef n ns (idris_callgraph i) })
160 put (i { idris_callgraph = addDef n ns (idris_callgraph i) })
160
161
162+addToCalledG :: Name -> [Name] -> Idris ()
163+addToCalledG n ns = return () -- TODO
164+
161-- Add a class instance function. Dodgy hack: Put integer instances first in the
165-- Add a class instance function. Dodgy hack: Put integer instances first in the
162-- list so they are resolved by default.
166-- list so they are resolved by default.
163
167
@@ -1658,14 +1662,17 @@ aiFn inpat ist fc f as
1658 insertImpl (PTacImplicit p l n sc ty : ps) given =
1662 insertImpl (PTacImplicit p l n sc ty : ps) given =
1659 case find n given [] of
1663 case find n given [] of
1660 Just (tm, given') -> PTacImplicit p l n sc tm : insertImpl ps given'
1664 Just (tm, given') -> PTacImplicit p l n sc tm : insertImpl ps given'
1661− Nothing -> PTacImplicit p l n sc sc
1665+ Nothing -> if inpat
1666+ then PTacImplicit p l n sc Placeholder : insertImpl ps given
1662− : insertImpl ps given
1667+ else PTacImplicit p l n sc sc : insertImpl ps given
1663 insertImpl expected [] = []
1668 insertImpl expected [] = []
1664 insertImpl _ given = given
1669 insertImpl _ given = given
1665
1670
1666 find n [] acc = Nothing
1671 find n [] acc = Nothing
1667 find n (PImp _ _ n' t : gs) acc
1672 find n (PImp _ _ n' t : gs) acc
1668 | n == n' = Just (t, reverse acc ++ gs)
1673 | n == n' = Just (t, reverse acc ++ gs)
1674+ find n (PTacImplicit _ _ n' _ t : gs) acc
1675+ | n == n' = Just (t, reverse acc ++ gs)
1669 find n (g : gs) acc = find n gs (g : acc)
1676 find n (g : gs) acc = find n gs (g : acc)
1670
1677
1671mkPApp fc a f [] = f
1678mkPApp 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
299 do let ns = namesUsed sc \\ scargs
299 do let ns = namesUsed sc \\ scargs
300 logLvl 2 $ "Called names: " ++ show ns
300 logLvl 2 $ "Called names: " ++ show ns
301 addToCG n ns
301 addToCG n ns
302+ addToCalledG n ns -- plus names in type!
302 addIBC (IBCCG n)
303 addIBC (IBCCG n)
303 _ -> return ()
304 _ -> return ()
304-- addIBC (IBCTotal n tot)
305-- addIBC (IBCTotal n tot)
@@ -380,7 +381,7 @@ elabClause info tcgen (PClause fc fname lhs_in withs rhs_in whereblock)
380 let decls = concatMap declared whereblock
381 let decls = concatMap declared whereblock
381 let newargs = pvars ist lhs_tm
382 let newargs = pvars ist lhs_tm
382 let wb = map (expandParamsD ist decorate newargs decls) whereblock
383 let wb = map (expandParamsD ist decorate newargs decls) whereblock
383− logLvl 5 $ show wb
384+ logLvl 5 $ "Where block: " ++ show wb
384 mapM_ (elabDecl' info) wb
385 mapM_ (elabDecl' info) wb
385 -- Now build the RHS, using the type of the LHS as the goal.
386 -- Now build the RHS, using the type of the LHS as the goal.
386 i <- get -- new implicits from where block
387 i <- get -- new implicits from where block