git.iko.soy/Idris-dev
on master help sign in
Type class instance resolution, and some Num overloading
be3a53aEdwin Brady
lib/builtins.idr+20−17
compare with master
unifiedsplit
@@ -71,14 +71,26 @@ intToBool x = True;
71boolOp : (a -> a -> Int) -> a -> a -> Bool;
71boolOp : (a -> a -> Int) -> a -> a -> Bool;
72boolOp op x y = intToBool (op x y);
72boolOp op x y = intToBool (op x y);
73
73
74−(+) : Int -> Int -> Int;
74+data Num : Set -> Set where
75−(+) = prim__addInt;
75+ NumInstance : (plus : a -> a -> a) ->
76+ (sub : a -> a -> a) ->
77+ (mult : a -> a -> a) ->
78+ Num a;
76
79
77−(-) : Int -> Int -> Int;
80+ (+) : Num a => a -> a -> a;
78−(-) = prim__subInt;
81+ (+) {{NumInstance p s m}} x y = p x y;
79
82
80−(*) : Int -> Int -> Int;
83+ (-) : Num a => a -> a -> a;
81−(*) = prim__mulInt;
84+ (-) {{NumInstance p s m}} x y = s x y;
85+
86+ (*) : Num a => a -> a -> a;
87+ (*) {{NumInstance p s m}} x y = m x y;
88+
89+instance numInt : Num Int;
90+instance numInt = NumInstance prim__addInt prim__subInt prim__mulInt;
91+
92+instance numFloat : Num Float;
93+instance numFloat = NumInstance prim__addFloat prim__subFloat prim__mulFloat;
82
94
83div : Int -> Int -> Int;
95div : Int -> Int -> Int;
84div = prim__divInt;
96div = prim__divInt;
@@ -98,17 +110,8 @@ div = prim__divInt;
98(>=) : Int -> Int -> Bool;
110(>=) : Int -> Int -> Bool;
99(>=) = boolOp prim__gteInt;
111(>=) = boolOp prim__gteInt;
100
112
101−(+.) : Float -> Float -> Float;
102−(+.) = prim__addFloat;
103−
104−(-.) : Float -> Float -> Float;
105−(-.) = prim__subFloat;
106−
107−(*.) : Float -> Float -> Float;
108−(*.) = prim__mulFloat;
109−
110−(/.) : Float -> Float -> Float;
113+(/) : Float -> Float -> Float;
111−(/.) = prim__divFloat;
114+(/) = prim__divFloat;
112
115
113(==.) : Float -> Float -> Bool;
116(==.) : Float -> Float -> Bool;
114(==.) = boolOp prim__eqFloat;
117(==.) = boolOp prim__eqFloat;
lib/nat.idr+12
@@ -27,3 +27,15 @@ plus_commutes_Sk = proof {
27 rewrite (sym ih);
27 rewrite (sym ih);
28 refine plusn_Sm;
28 refine plusn_Sm;
29};
29};
30+
31+sub : Nat -> Nat -> Nat;
32+sub O y = O;
33+sub (S k) (S y) = sub k y;
34+sub x O = x;
35+
36+mult : Nat -> Nat -> Nat;
37+mult O y = O;
38+mult (S k) y = plus y (mult k y);
39+
40+instance numNat : Num Nat;
41+instance numNat = NumInstance plus sub mult;
lib/vect.idr+1−1
@@ -14,7 +14,7 @@ vlookup : Fin n -> Vect a n -> a;
14vlookup fO (x :: xs) = x;
14vlookup fO (x :: xs) = x;
15vlookup (fS k) (x :: xs) = vlookup k xs;
15vlookup (fS k) (x :: xs) = vlookup k xs;
16
16
17−vapp : Vect a n -> Vect a m -> Vect a (plus n m);
17+vapp : Vect a n -> Vect a m -> Vect a (n + m);
18vapp VNil ys = ys;
18vapp VNil ys = ys;
19vapp (x :: xs) ys = x :: vapp xs ys;
19vapp (x :: xs) ys = x :: vapp xs ys;
20
20
src/Core/CoreParser.hs+1−1
@@ -22,7 +22,7 @@ idrisDef = haskellDef {
22 "do", "dsl", "import", "return", -- "refl",
22 "do", "dsl", "import", "return", -- "refl",
23 "infix", "infixl", "infixr", "prefix",
23 "infix", "infixl", "infixr", "prefix",
24 "where", "with", "forall", "syntax", "proof",
24 "where", "with", "forall", "syntax", "proof",
25− "using", "params", "namespace",
25+ "using", "params", "namespace", "class", "instance",
26 "Int", "Float", "Char", "String", "Ptr"]
26 "Int", "Float", "Char", "String", "Ptr"]
27 }
27 }
28
28
src/Core/Elaborate.hs+8−1
@@ -110,6 +110,11 @@ get_deferred :: Elab [Name]
110get_deferred = do ES p _ _ <- get
110get_deferred = do ES p _ _ <- get
111 return (deferred p)
111 return (deferred p)
112
112
113+-- get instance argument names
114+get_instances :: Elab [Name]
115+get_instances = do ES p _ _ <- get
116+ return (instances p)
117+
113-- given a desired hole name, return a unique hole name
118-- given a desired hole name, return a unique hole name
114unique_hole :: Name -> Elab Name
119unique_hole :: Name -> Elab Name
115unique_hole n = do ES p _ _ <- get
120unique_hole n = do ES p _ _ <- get
@@ -189,6 +194,9 @@ movelast n = processTactic' (MoveLast n)
189defer :: Name -> Elab ()
194defer :: Name -> Elab ()
190defer n = processTactic' (Defer n)
195defer n = processTactic' (Defer n)
191
196
197+instanceArg :: Name -> Elab ()
198+instanceArg n = processTactic' (Instance n)
199+
192proofstate :: Elab ()
200proofstate :: Elab ()
193proofstate = processTactic' ProofState
201proofstate = processTactic' ProofState
194
202
@@ -200,7 +208,6 @@ qed = do processTactic' QED
200undo :: Elab ()
208undo :: Elab ()
201undo = processTactic' Undo
209undo = processTactic' Undo
202
210
203−
204prepare_apply :: Raw -> [Bool] -> Elab [Name]
211prepare_apply :: Raw -> [Bool] -> Elab [Name]
205prepare_apply fn imps =
212prepare_apply fn imps =
206 do ty <- get_type fn
213 do ty <- get_type fn
src/Core/ProofState.hs+18−5
@@ -24,6 +24,7 @@ data ProofState = PS { thname :: Name,
24 ptype :: Type, -- original goal
24 ptype :: Type, -- original goal
25 unified :: (Name, [(Name, Term)]),
25 unified :: (Name, [(Name, Term)]),
26 deferred :: [Name], -- names we'll need to define
26 deferred :: [Name], -- names we'll need to define
27+ instances :: [Name], -- instance arguments (for type classes)
27 previous :: Maybe ProofState, -- for undo
28 previous :: Maybe ProofState, -- for undo
28 context :: Context,
29 context :: Context,
29 plog :: String,
30 plog :: String,
@@ -55,6 +56,7 @@ data Tactic = Attack
55 | PatBind Name
56 | PatBind Name
56 | Focus Name
57 | Focus Name
57 | Defer Name
58 | Defer Name
59+ | Instance Name
58 | MoveLast Name
60 | MoveLast Name
59 | ProofState
61 | ProofState
60 | Undo
62 | Undo
@@ -64,8 +66,8 @@ data Tactic = Attack
64-- Some utilites on proof and tactic states
66-- Some utilites on proof and tactic states
65
67
66instance Show ProofState where
68instance Show ProofState where
67− show (PS nm [] _ tm _ _ _ _ _ _ _) = show nm ++ ": no more goals"
69+ show (PS nm [] _ tm _ _ _ _ _ _ _ _) = show nm ++ ": no more goals"
68− show (PS nm (h:hs) _ tm _ _ i _ ctxt _ _)
70+ show (PS nm (h:hs) _ tm _ _ i _ _ ctxt _ _)
69 = let OK g = goal (Just h) tm
71 = let OK g = goal (Just h) tm
70 wkenv = premises g in
72 wkenv = premises g in
71 "Other goals: " ++ show hs ++ "\n" ++
73 "Other goals: " ++ show hs ++ "\n" ++
@@ -112,7 +114,8 @@ addLog str = action (\ps -> ps { plog = plog ps ++ str ++ "\n" })
112newProof :: Name -> Context -> Type -> ProofState
114newProof :: Name -> Context -> Type -> ProofState
113newProof n ctxt ty = let h = holeName 0
115newProof n ctxt ty = let h = holeName 0
114 ty' = vToP ty in
116 ty' = vToP ty in
115− PS n [h] 1 (Bind h (Hole ty') (P Bound h ty')) ty (h, []) []
117+ PS n [h] 1 (Bind h (Hole ty') (P Bound h ty')) ty (h, [])
118+ [] []
116 Nothing ctxt "" False
119 Nothing ctxt "" False
117
120
118type TState = ProofState -- [TacticAction])
121type TState = ProofState -- [TacticAction])
@@ -191,6 +194,14 @@ movelast n ctxt env t = do action (\ps -> let hs = holes ps in
191 else ps)
194 else ps)
192 return t
195 return t
193
196
197+instanceArg :: Name -> RunTactic
198+instanceArg n ctxt env (Bind x (Hole t) sc)
199+ = do action (\ps -> let hs = holes ps
200+ is = instances ps in
201+ ps { holes = (hs \\ [x]) ++ [x],
202+ instances = x:is })
203+ return (Bind x (Hole t) sc)
204+
194defer :: Name -> RunTactic
205defer :: Name -> RunTactic
195defer n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =
206defer n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =
196 do action (\ps -> let hs = holes ps in
207 do action (\ps -> let hs = holes ps in
@@ -246,7 +257,8 @@ complete_fill ctxt env t = fail $ "Can't complete fill at " ++ show t
246
257
247solve :: RunTactic
258solve :: RunTactic
248solve ctxt env (Bind x (Guess ty val) sc)
259solve ctxt env (Bind x (Guess ty val) sc)
249− | pureTerm val = do action (\ps -> ps { holes = holes ps \\ [x] })
260+ | pureTerm val = do action (\ps -> ps { holes = holes ps \\ [x],
261+ instances = instances ps \\ [x] })
250 return $ {- Bind x (Let ty val) sc -} instantiate val (pToV x sc)
262 return $ {- Bind x (Let ty val) sc -} instantiate val (pToV x sc)
251 | otherwise = fail "I see a hole in your solution."
263 | otherwise = fail "I see a hole in your solution."
252solve _ _ h = fail $ "Not a guess " ++ show h
264solve _ _ h = fail $ "Not a guess " ++ show h
@@ -426,5 +438,6 @@ process t h = tactic (Just h) (mktac t)
426 mktac (CheckIn r) = check_in r
438 mktac (CheckIn r) = check_in r
427 mktac (EvalIn r) = eval_in r
439 mktac (EvalIn r) = eval_in r
428 mktac (Focus n) = focus n
440 mktac (Focus n) = focus n
429− mktac (MoveLast n) = movelast n
430 mktac (Defer n) = defer n
441 mktac (Defer n) = defer n
442+ mktac (Instance n) = instanceArg n
443+ mktac (MoveLast n) = movelast n
src/Idris/AbsSyntax.hs+31−2
@@ -171,10 +171,13 @@ data Plicity = Imp { plazy :: Bool,
171 pstatic :: Static }
171 pstatic :: Static }
172 | Exp { plazy :: Bool,
172 | Exp { plazy :: Bool,
173 pstatic :: Static }
173 pstatic :: Static }
174+ | Constraint { plazy :: Bool,
175+ pstatic :: Static }
174 deriving (Show, Eq)
176 deriving (Show, Eq)
175
177
176impl = Imp False Dynamic
178impl = Imp False Dynamic
177expl = Exp False Dynamic
179expl = Exp False Dynamic
180+constraint = Constraint False Static
178
181
179data PDecl' t = PFix FC Fixity [String] -- fixity declaration
182data PDecl' t = PFix FC Fixity [String] -- fixity declaration
180 | PTy SyntaxInfo FC Name t -- type declaration
183 | PTy SyntaxInfo FC Name t -- type declaration
@@ -243,6 +246,7 @@ data PTerm = PQuote Raw
243 | PTrue FC
246 | PTrue FC
244 | PFalse FC
247 | PFalse FC
245 | PRefl FC
248 | PRefl FC
249+ | PResolveTC FC
246 | PEq FC PTerm PTerm
250 | PEq FC PTerm PTerm
247 | PPair FC PTerm PTerm
251 | PPair FC PTerm PTerm
248 | PDPair FC PTerm PTerm
252 | PDPair FC PTerm PTerm
@@ -292,10 +296,12 @@ type PDo = PDo' PTerm
292
296
293data PArg' t = PImp { lazyarg :: Bool, pname :: Name, getTm :: t }
297data PArg' t = PImp { lazyarg :: Bool, pname :: Name, getTm :: t }
294 | PExp { lazyarg :: Bool, getTm :: t }
298 | PExp { lazyarg :: Bool, getTm :: t }
299+ | PConstraint { lazyarg :: Bool, getTm :: t }
295 deriving (Show, Eq, Functor)
300 deriving (Show, Eq, Functor)
296
301
297pimp = PImp False
302pimp = PImp False
298pexp = PExp False
303pexp = PExp False
304+pconst = PConstraint False
299
305
300type PArg = PArg' PTerm
306type PArg = PArg' PTerm
301
307
@@ -372,6 +378,11 @@ getExps [] = []
372getExps (PExp _ tm : xs) = tm : getExps xs
378getExps (PExp _ tm : xs) = tm : getExps xs
373getExps (_ : xs) = getExps xs
379getExps (_ : xs) = getExps xs
374
380
381+getConsts :: [PArg] -> [PTerm]
382+getConsts [] = []
383+getConsts (PConstraint _ tm : xs) = tm : getConsts xs
384+getConsts (_ : xs) = getConsts xs
385+
375getAll :: [PArg] -> [PTerm]
386getAll :: [PArg] -> [PTerm]
376getAll = map getTm
387getAll = map getTm
377
388
@@ -400,6 +411,8 @@ showImp impl tm = se 10 tm where
400 where st = case s of
411 where st = case s of
401 Static -> "[static] "
412 Static -> "[static] "
402 _ -> ""
413 _ -> ""
414+ se p (PPi (Constraint _ _) n ty sc)
415+ = bracket p 2 $ se 10 ty ++ " => " ++ se 10 sc
403 se p (PApp _ (PRef _ f) [])
416 se p (PApp _ (PRef _ f) [])
404 | not impl = show f
417 | not impl = show f
405 se p (PApp _ (PRef _ op@(UN [f:_])) args)
418 se p (PApp _ (PRef _ op@(UN [f:_])) args)
@@ -407,11 +420,13 @@ showImp impl tm = se 10 tm where
407 = let [l, r] = getExps args in
420 = let [l, r] = getExps args in
408 bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 0 r
421 bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 0 r
409 se p (PApp _ f as)
422 se p (PApp _ f as)
410− = let (imps, args) = (getImps as, getExps as) in
423+ = let (imps, cs, args) = (getImps as, getConsts as, getExps as) in
424+ bracket p 1 $ se 1 f ++ concatMap scArg cs
411− bracket p 1 $ se 1 f ++ (if impl then concatMap siArg imps else "")
425+ ++ (if impl then concatMap siArg imps else "")
412 ++ concatMap seArg args
426 ++ concatMap seArg args
413 se p (PHidden tm) = "." ++ se 0 tm
427 se p (PHidden tm) = "." ++ se 0 tm
414 se p (PRefl _) = "refl"
428 se p (PRefl _) = "refl"
429+ se p (PResolveTC _) = "resolvetc"
415 se p (PTrue _) = "()"
430 se p (PTrue _) = "()"
416 se p (PFalse _) = "_|_"
431 se p (PFalse _) = "_|_"
417 se p (PEq _ l r) = bracket p 2 $ se 10 l ++ " = " ++ se 10 r
432 se p (PEq _ l r) = bracket p 2 $ se 10 l ++ " = " ++ se 10 r
@@ -425,6 +440,7 @@ showImp impl tm = se 10 tm where
425
440
426 seArg arg = " " ++ se 0 arg
441 seArg arg = " " ++ se 0 arg
427 siArg (n, val) = " {" ++ show n ++ " = " ++ se 10 val ++ "}"
442 siArg (n, val) = " {" ++ show n ++ " = " ++ se 10 val ++ "}"
443+ scArg val = " {{" ++ se 10 val ++ "}}"
428
444
429 bracket outer inner str | inner > outer = "(" ++ str ++ ")"
445 bracket outer inner str | inner > outer = "(" ++ str ++ ")"
430 | otherwise = str
446 | otherwise = str
@@ -626,6 +642,14 @@ implicitise syn ist tm
626 put (PExp l ty : decls,
642 put (PExp l ty : decls,
627 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
643 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
628 imps True (n:env) sc
644 imps True (n:env) sc
645+ imps top env (PPi (Constraint l _) n ty sc)
646+ = do let isn = nub (namesIn ist ty ++ case sc of
647+ (PRef _ x) -> namesIn ist sc `dropAll` [n]
648+ _ -> [])
649+ (decls, ns) <- get -- ignore decls in HO types
650+ put (PConstraint l ty : decls,
651+ nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
652+ imps True (n:env) sc
629 imps top env (PEq _ l r)
653 imps top env (PEq _ l r)
630 = do (decls, ns) <- get
654 = do (decls, ns) <- get
631 let isn = namesIn ist l ++ namesIn ist r
655 let isn = namesIn ist l ++ namesIn ist r
@@ -701,6 +725,10 @@ aiFn ist fc f as
701 insertImpl :: [PArg] -> [PArg] -> [PArg]
725 insertImpl :: [PArg] -> [PArg] -> [PArg]
702 insertImpl (PExp l ty : ps) (PExp _ tm : given) =
726 insertImpl (PExp l ty : ps) (PExp _ tm : given) =
703 PExp l tm : insertImpl ps given
727 PExp l tm : insertImpl ps given
728+ insertImpl (PConstraint l ty : ps) (PConstraint _ tm : given) =
729+ PConstraint l tm : insertImpl ps given
730+ insertImpl (PConstraint l ty : ps) given =
731+ PConstraint l (PResolveTC fc) : insertImpl ps given
704 insertImpl (PImp l n ty : ps) given =
732 insertImpl (PImp l n ty : ps) given =
705 case find n given [] of
733 case find n given [] of
706 Just (tm, given') -> PImp l n tm : insertImpl ps given'
734 Just (tm, given') -> PImp l n tm : insertImpl ps given'
@@ -789,6 +817,7 @@ matchClause x y = match x y where
789 mr <- match r r'
817 mr <- match r r'
790 return (ml ++ mr)
818 return (ml ++ mr)
791 match (PRefl _) (PRefl _) = return []
819 match (PRefl _) (PRefl _) = return []
820+ match (PResolveTC _) (PResolveTC _) = return []
792 match (PTrue _) (PTrue _) = return []
821 match (PTrue _) (PTrue _) = return []
793 match (PFalse _) (PFalse _) = return []
822 match (PFalse _) (PFalse _) = return []
794 match (PReturn _) (PReturn _) = return []
823 match (PReturn _) (PReturn _) = return []
src/Idris/Delaborate.hs+1
@@ -45,6 +45,7 @@ delab ist tm = de [] tm
45
45
46 imp (PImp l n _) arg = PImp l n arg
46 imp (PImp l n _) arg = PImp l n arg
47 imp (PExp l _) arg = PExp l arg
47 imp (PExp l _) arg = PExp l arg
48+ imp (PConstraint l _) arg = PConstraint l arg
48
49
49pshow :: IState -> Err -> String
50pshow :: IState -> Err -> String
50pshow i (Msg s) = s
51pshow i (Msg s) = s
src/Idris/ElabDecls.hs+55−34
@@ -16,6 +16,7 @@ import Core.CaseTree
16
16
17import Control.Monad
17import Control.Monad
18import Control.Monad.State
18import Control.Monad.State
19+import Data.List
19import Debug.Trace
20import Debug.Trace
20
21
21-- Data to pass to recursively called elaborators; e.g. for where blocks,
22-- Data to pass to recursively called elaborators; e.g. for where blocks,
@@ -104,14 +105,14 @@ elabClauses info fc n_in cs = let n = liftname info n_in in
104 depat (Bind n (PVar t) sc) = depat (instantiate (P Bound n t) sc)
105 depat (Bind n (PVar t) sc) = depat (instantiate (P Bound n t) sc)
105 depat x = x
106 depat x = x
106
107
107−elabVal :: ElabInfo -> PTerm -> Idris (Term, Type)
108+elabVal :: ElabInfo -> Bool -> PTerm -> Idris (Term, Type)
108−elabVal info tm_in
109+elabVal info aspat tm_in
109 = do ctxt <- getContext
110 = do ctxt <- getContext
110 i <- get
111 i <- get
111 let tm = addImpl i tm_in
112 let tm = addImpl i tm_in
112 logLvl 10 (showImp True tm)
113 logLvl 10 (showImp True tm)
113 ((tm', defer), _) <- tclift $ elaborate ctxt (MN 0 "val") infP
114 ((tm', defer), _) <- tclift $ elaborate ctxt (MN 0 "val") infP
114− (build i info True (infTerm tm))
115+ (build i info aspat (infTerm tm))
115 logLvl 3 ("Value: " ++ show tm')
116 logLvl 3 ("Value: " ++ show tm')
116 let vtm = getInferTerm tm'
117 let vtm = getInferTerm tm'
117 logLvl 2 (show vtm)
118 logLvl 2 (show vtm)
@@ -360,27 +361,6 @@ elab ist info pattern tm
360 (h: hs) -> do patvar h; mkPat
361 (h: hs) -> do patvar h; mkPat
361 [] -> return ()
362 [] -> return ()
362
363
363− -- Expand implict arguments here, then move on to main elaborator
364−-- elabE (PRef fc n)
365−-- | Just ps <- lookupCtxt n (inblock info)
366−-- = -- let exp = (PApp fc (PRef fc n) (map (pexp . (PRef fc)) ps))
367−-- elabE (PApp fc (PRef fc n) [])
368−-- elabE f@(PApp fc fn args) = trace ("Elaborating " ++ show f) $ elab' f
369−-- elabE (PRef fc f)
370−-- = do l <- local f
371−-- elabN f l
372−-- where elabN f False = let afn = aiFn ist fc f [] in
373−-- -- trace ("Ref expanded to " ++ showImp True afn) $
374−-- elab' afn
375−-- elabN f True = elab' (PRef fc f)
376−-- elabE (PApp fc fn@(PRef _ f) args)
377−-- = do l <- local f
378−-- elabApp f args l -- no implicits
379−-- where elabApp f args False = let afn = aiFn ist fc f args in
380−-- -- trace ("Expanded to " ++ showImp True afn) $
381−-- elab' afn
382−-- elabApp f args True = elab' (PApp fc fn args)
383−-- elabE (PApp fc f as) = elab' (mkPApp fc 1 f as)
384 elabE t = elab' t
364 elabE t = elab' t
385
365
386 local f = do e <- get_env
366 local f = do e <- get_env
@@ -392,6 +372,8 @@ elab ist info pattern tm
392 elab' (PTrue fc) = try (elab' (PRef fc unitCon))
372 elab' (PTrue fc) = try (elab' (PRef fc unitCon))
393 (elab' (PRef fc unitTy))
373 (elab' (PRef fc unitTy))
394 elab' (PFalse fc) = elab' (PRef fc falseTy)
374 elab' (PFalse fc) = elab' (PRef fc falseTy)
375+ elab' (PResolveTC fc) = do c <- unique_hole (MN 0 "c")
376+ instanceArg c
395 elab' (PRefl fc) = elab' (PApp fc (PRef fc eqCon) [pimp (MN 0 "a") Placeholder,
377 elab' (PRefl fc) = elab' (PApp fc (PRef fc eqCon) [pimp (MN 0 "a") Placeholder,
396 pimp (MN 0 "x") Placeholder])
378 pimp (MN 0 "x") Placeholder])
397 elab' (PEq fc l r) = elab' (PApp fc (PRef fc eqTy) [pimp (MN 0 "a") Placeholder,
379 elab' (PEq fc l r) = elab' (PApp fc (PRef fc eqTy) [pimp (MN 0 "a") Placeholder,
@@ -452,11 +434,25 @@ elab ist info pattern tm
452 = do let args = {- case lookupCtxt f (inblock info) of
434 = do let args = {- case lookupCtxt f (inblock info) of
453 Just ps -> (map (pexp . (PRef fc)) ps ++ args')
435 Just ps -> (map (pexp . (PRef fc)) ps ++ args')
454 _ ->-} args'
436 _ ->-} args'
437+ ivs <- get_instances
455 try (do ns <- apply (Var f) (map isph args)
438 try (do ns <- apply (Var f) (map isph args)
456 solve
439 solve
457 elabArgs ns (map (\x -> (lazyarg x, getTm x)) args))
440 elabArgs ns (map (\x -> (lazyarg x, getTm x)) args))
458 (do apply_elab f (map toElab args)
441 (do apply_elab f (map toElab args)
459 solve)
442 solve)
443+ ivs' <- get_instances
444+ when (not pattern) $
445+ mapM_ (\n -> do focus n
446+ resolveTC ist) (ivs' \\ ivs)
447+-- ivs <- get_instances
448+-- when (not (null ivs)) $
449+-- do t <- get_term
450+-- trace (show ivs ++ "\n" ++ show t) $
451+-- mapM_ (\n -> do focus n
452+-- resolveTC ist) ivs
453+ where tcArg (n, PConstraint _ Placeholder) = True
454+ tcArg _ = False
455+
460 elab' (PApp fc f [arg])
456 elab' (PApp fc f [arg])
461 = erun fc $
457 = erun fc $
462 do simple_app (elabE f) (elabE (getTm arg))
458 do simple_app (elabE f) (elabE (getTm arg))
@@ -478,7 +474,40 @@ elab ist info pattern tm
478 elabArgs ns args
474 elabArgs ns args
479 | otherwise
475 | otherwise
480 = do focus n; elabE t; elabArgs ns args
476 = do focus n; elabE t; elabArgs ns args
481−
477+
478+trivial :: IState -> Elab ()
479+trivial ist = try (elab ist toplevel False (PRefl (FC "prf" 0)))
480+ (do env <- get_env
481+ tryAll (map fst env))
482+ where
483+ tryAll [] = fail "No trivial solution"
484+ tryAll (x:xs) = try (elab ist toplevel False (PRef (FC "prf" 0) x))
485+ (tryAll xs)
486+
487+resolveTC :: IState -> Elab ()
488+resolveTC ist = do t <- goal
489+ tm <- get_term
490+ try (trivial ist)
491+ (blunderbuss t (map fst (toAlist (tt_ctxt ist))))
492+ where
493+ blunderbuss t [] = fail $ "Can't resolve type class " ++ show t
494+ blunderbuss t (n:ns) | tcname n = try (resolve n)
495+ (blunderbuss t ns)
496+ | otherwise = blunderbuss t ns
497+ tcname (UN (('@':_) : _)) = True
498+ tcname _ = False
499+
500+ resolve n = do t <- goal
501+ let imps = case lookupCtxt n (idris_implicits ist) of
502+ Nothing -> []
503+ Just args -> map isImp args
504+ args <- apply (Var n) imps
505+ mapM_ (\ (_,n) -> do focus n
506+ resolveTC ist)
507+ (filter (\ (x, y) -> not x) (zip imps args))
508+ solve
509+ where isImp (PImp _ _ _) = True
510+ isImp _ = False
482
511
483collectDeferred :: Term -> State [(Name, Type)] Term
512collectDeferred :: Term -> State [(Name, Type)] Term
484collectDeferred (Bind n (GHole t) app) =
513collectDeferred (Bind n (GHole t) app) =
@@ -531,15 +560,7 @@ runTac autoSolve ist tac = runT (fmap (addImpl ist) tac) where
531 rewrite (Var letn)
560 rewrite (Var letn)
532 when autoSolve solveAll
561 when autoSolve solveAll
533 runT Compute = compute
562 runT Compute = compute
534− runT Trivial = try (do elab ist toplevel False (PRefl (FC "prf" 0))
535− when autoSolve solveAll)
536− (do env <- get_env
537− tryAll (map fst env))
538− where
539− tryAll [] = fail "No trivial solution"
540− tryAll (x:xs) = try (do elab ist toplevel False (PRef (FC "prf" 0) x)
541− when autoSolve solveAll)
563+ runT Trivial = do trivial ist; when autoSolve solveAll
542− (tryAll xs)
543 runT (Focus n) = focus n
564 runT (Focus n) = focus n
544 runT Solve = solve
565 runT Solve = solve
545 runT x = fail $ "Not implemented " ++ show x
566 runT x = fail $ "Not implemented " ++ show x
src/Idris/Parser.hs+29−6
@@ -335,7 +335,10 @@ pExt syn (Rule (s:ssym) ptm)
335
335
336pName = do i <- getState
336pName = do i <- getState
337 iName (syntax_keywords i)
337 iName (syntax_keywords i)
338− where
338+ <|> do reserved "instance"
339+ i <- getState
340+ UN (n:ns) <- iName (syntax_keywords i)
341+ return (UN (('@':n) : ns))
339
342
340pfName = try pName
343pfName = try pName
341 <|> do lchar '('; o <- operator; lchar ')'; return (UN [o])
344 <|> do lchar '('; o <- operator; lchar ')'; return (UN [o])
@@ -379,7 +382,8 @@ pApp syn = do f <- pSimpleExpr syn
379 return (PApp fc f args)
382 return (PApp fc f args)
380
383
381pArg :: SyntaxInfo -> IParser PArg
384pArg :: SyntaxInfo -> IParser PArg
382−pArg syn = pImplicitArg syn
385+pArg syn = try (pImplicitArg syn)
386+ <|> try (pConstraintArg syn)
383 <|> do e <- pSimpleExpr syn
387 <|> do e <- pSimpleExpr syn
384 return (pexp e)
388 return (pexp e)
385
389
@@ -389,8 +393,13 @@ pImplicitArg syn = do lchar '{'; n <- pName
389 lchar '}'
393 lchar '}'
390 return (pimp n v)
394 return (pimp n v)
391
395
396+pConstraintArg syn = do symbol "{{"; e <- pExpr syn; symbol "}}"
397+ return (pconst e)
398+
392pTSig syn = do lchar ':'
399pTSig syn = do lchar ':'
400+ cs <- pConstList syn
393− pExpr syn
401+ sc <- pExpr syn
402+ return (bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc)
394
403
395pLambda syn = do lchar '\\';
404pLambda syn = do lchar '\\';
396 xt <- tyOptDeclList syn
405 xt <- tyOptDeclList syn
@@ -422,6 +431,16 @@ pPi syn =
422 sc <- pExpr syn
431 sc <- pExpr syn
423 return (PPi (Exp False Static) (MN 0 "X") t sc)
432 return (PPi (Exp False Static) (MN 0 "X") t sc)
424
433
434+pConstList :: SyntaxInfo -> IParser [PTerm]
435+pConstList syn = try (do lchar '('
436+ tys <- sepBy1 (pExpr' syn) (lchar ',')
437+ lchar ')'
438+ reservedOp "=>"
439+ return tys)
440+ <|> try (do t <- pExpr syn
441+ reservedOp "=>"
442+ return [t])
443+ <|> return []
425
444
426tyDeclList syn = sepBy1 (do x <- pfName; t <- pTSig syn; return (x,t))
445tyDeclList syn = sepBy1 (do x <- pfName; t <- pTSig syn; return (x,t))
427 (lchar ',')
446 (lchar ',')
@@ -548,6 +567,7 @@ whereSyn n syn args = let ns = concatMap allNamesIn args
548pClause :: SyntaxInfo -> IParser PClause
567pClause :: SyntaxInfo -> IParser PClause
549pClause syn
568pClause syn
550 = try (do n <- pfName
569 = try (do n <- pfName
570+ cargs <- many (pConstraintArg syn)
551 iargs <- many (pImplicitArg syn)
571 iargs <- many (pImplicitArg syn)
552 fc <- pfc
572 fc <- pfc
553 args <- many (pHSimpleExpr syn)
573 args <- many (pHSimpleExpr syn)
@@ -556,12 +576,15 @@ pClause syn
556 rhs <- pExpr syn
576 rhs <- pExpr syn
557 ist <- getState
577 ist <- getState
558 let ctxt = tt_ctxt ist
578 let ctxt = tt_ctxt ist
559− let wsyn = whereSyn n syn (map getTm iargs ++ args ++ wargs)
579+ let wsyn = whereSyn n syn (map getTm cargs ++
580+ map getTm iargs ++
581+ args ++ wargs)
560 (wheres, nmap) <- choice [pWhereblock n syn, do lchar ';'
582 (wheres, nmap) <- choice [pWhereblock n syn, do lchar ';'
561 return ([], [])]
583 return ([], [])]
562 return $ PClause n (PApp fc (PRef fc n)
584 return $ PClause n (PApp fc (PRef fc n)
563− (iargs ++ map pexp args)) wargs rhs wheres)
585+ (cargs ++ iargs ++ map pexp args)) wargs rhs wheres)
564 <|> try (do n <- pfName
586 <|> try (do n <- pfName
587+ cargs <- many (pConstraintArg syn)
565 iargs <- many (pImplicitArg syn)
588 iargs <- many (pImplicitArg syn)
566 fc <- pfc
589 fc <- pfc
567 args <- many (pHSimpleExpr syn)
590 args <- many (pHSimpleExpr syn)
@@ -573,7 +596,7 @@ pClause syn
573 let withs = concat ds
596 let withs = concat ds
574 lchar '}'
597 lchar '}'
575 return $ PWith n (PApp fc (PRef fc n)
598 return $ PWith n (PApp fc (PRef fc n)
576− (iargs ++ map pexp args)) wargs wval withs)
599+ (cargs ++ iargs ++ map pexp args)) wargs wval withs)
577
600
578 <|> do l <- pSimpleExpr syn
601 <|> do l <- pSimpleExpr syn
579 op <- operator
602 op <- operator
src/Idris/Prover.hs+2−2
@@ -48,8 +48,8 @@ elabStep st e = do case runStateT e st of
48 fail (pshow i a)
48 fail (pshow i a)
49
49
50dumpState :: IState -> ProofState -> IO ()
50dumpState :: IState -> ProofState -> IO ()
51−dumpState ist (PS nm [] _ tm _ _ _ _ _ _ _) = putStrLn $ (show nm) ++ ": no more goals"
51+dumpState ist (PS nm [] _ tm _ _ _ _ _ _ _ _) = putStrLn $ (show nm) ++ ": no more goals"
52−dumpState ist ps@(PS nm (h:hs) _ tm _ _ i _ cyxy _ _)
52+dumpState ist ps@(PS nm (h:hs) _ tm _ _ i _ _ ctxy _ _)
53 = do let OK ty = goalAtFocus ps
53 = do let OK ty = goalAtFocus ps
54 let OK env = envAtFocus ps
54 let OK env = envAtFocus ps
55 putStrLn $ "Other goals: " ++ show hs ++ "\n"
55 putStrLn $ "Other goals: " ++ show hs ++ "\n"
src/Idris/REPL.hs+3−3
@@ -77,7 +77,7 @@ process f Edit
77 where getEditor env | Just ed <- lookup "EDITOR" env = ed
77 where getEditor env | Just ed <- lookup "EDITOR" env = ed
78 | Just ed <- lookup "VISUAL" env = ed
78 | Just ed <- lookup "VISUAL" env = ed
79 | otherwise = "vi"
79 | otherwise = "vi"
80−process _ (Eval t) = do (tm, ty) <- elabVal toplevel t
80+process _ (Eval t) = do (tm, ty) <- elabVal toplevel False t
81 ctxt <- getContext
81 ctxt <- getContext
82 ist <- get
82 ist <- get
83 let tm' = normaliseC ctxt [] tm
83 let tm' = normaliseC ctxt [] tm
@@ -85,13 +85,13 @@ process _ (Eval t) = do (tm, ty) <- elabVal toplevel t
85 logLvl 3 $ "Raw: " ++ show (tm', ty')
85 logLvl 3 $ "Raw: " ++ show (tm', ty')
86 iputStrLn (show (delab ist tm') ++ " : " ++
86 iputStrLn (show (delab ist tm') ++ " : " ++
87 show (delab ist ty'))
87 show (delab ist ty'))
88−process _ (Spec t) = do (tm, ty) <- elabVal toplevel t
88+process _ (Spec t) = do (tm, ty) <- elabVal toplevel False t
89 ctxt <- getContext
89 ctxt <- getContext
90 ist <- get
90 ist <- get
91 let tm' = specialise ctxt (idris_statics ist) tm
91 let tm' = specialise ctxt (idris_statics ist) tm
92 iputStrLn (show (delab ist tm'))
92 iputStrLn (show (delab ist tm'))
93process _ (Prove n) = prover n
93process _ (Prove n) = prover n
94−process _ (HNF t) = do (tm, ty) <- elabVal toplevel t
94+process _ (HNF t) = do (tm, ty) <- elabVal toplevel False t
95 ctxt <- getContext
95 ctxt <- getContext
96 ist <- get
96 ist <- get
97 let tm' = hnf ctxt [] tm
97 let tm' = hnf ctxt [] tm