98be75c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Added (experimentally) auto implicit arguments

commit98be75cb655a2048e151033740545471d128d08a authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateThu 26 Jan 2012, 14:03 (15 years ago) parent6dcf4c3

7 files changed+59−21

compare with master

unifiedsplit

lib/network/cgi.idr+1−1 src/Idris/AbsSyntax.hs+24 src/Idris/Coverage.hs+3−2 src/Idris/Delaborate.hs+1 src/Idris/ElabDecls.hs+16−17 src/Idris/ElabTerm.hs+3−1 src/Idris/Parser.hs+11

lib/network/cgi.idr+1−1

@@ -116,7 +116,7 @@ getVars seps query = mapMaybe readVar (split (\x => elem x seps) query)

116116getContent : Int -> IO String

117117getContent x = getC x "" where

118118 getC : Int -> String -> IO String

119− getC 0 acc = return $ rev acc

119+ getC 0 acc = return $ reverse acc

120120 getC n acc = do x <- getChar

121121 getC (n-1) (strCons x acc)

122122

src/Idris/AbsSyntax.hs+24

@@ -358,6 +358,9 @@ data Plicity = Imp { plazy :: Bool,

358358 pstatic :: Static }

359359 | Constraint { plazy :: Bool,

360360 pstatic :: Static }

361+ | TacImp { plazy :: Bool,

362+ pstatic :: Static,

363+ pscript :: PTerm }

361364 deriving (Show, Eq)

362365

363366{-!

@@ -367,6 +370,7 @@ deriving instance Binary Plicity

367370impl = Imp False Dynamic

368371expl = Exp False Dynamic

369372constraint = Constraint False Static

373+tacimpl = TacImp False Dynamic

370374

371375data FnOpt = Inlinable | TotalFn | TCGen

372376 deriving (Show, Eq)

@@ -544,6 +548,10 @@ data PArg' t = PImp { priority :: Int,

544548 lazyarg :: Bool, getTm :: t }

545549 | PConstraint { priority :: Int,

546550 lazyarg :: Bool, getTm :: t }

551+ | PTacImplicit { priority :: Int,

552+ lazyarg :: Bool, pname :: Name,

553+ getScript :: t,

554+ getTm :: t }

547555 deriving (Show, Eq, Functor)

548556{-!

549557deriving instance Binary PArg'

@@ -552,6 +560,7 @@ deriving instance Binary PArg'

552560pimp = PImp 0 True

553561pexp = PExp 0 False

554562pconst = PConstraint 0 False

563+ptacimp = PTacImplicit 0 True

555564

556565type PArg = PArg' PTerm

557566

@@ -767,10 +776,12 @@ showImp impl tm = se 10 tm where

767776 sArg (PImp _ _ n tm) = siArg (n, tm)

768777 sArg (PExp _ _ tm) = seArg tm

769778 sArg (PConstraint _ _ tm) = scArg tm

779+ sArg (PTacImplicit _ _ n _ tm) = stiArg (n, tm)

770780

771781 seArg arg = " " ++ se 0 arg

772782 siArg (n, val) = " {" ++ show n ++ " = " ++ se 10 val ++ "}"

773783 scArg val = " {{" ++ se 10 val ++ "}}"

784+ stiArg (n, val) = " {auto " ++ show n ++ " = " ++ se 10 val ++ "}"

774785

775786 bracket outer inner str | inner > outer = "(" ++ str ++ ")"

776787 | otherwise = str

@@ -1063,6 +1074,14 @@ implicitise syn ist tm

10631074 put (PConstraint 10 l ty : decls,

10641075 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

10651076 imps True (n:env) sc

1077+ imps top env (PPi (TacImp l _ scr) n ty sc)

1078+ = do let isn = nub (namesIn uvars ist ty ++ case sc of

1079+ (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]

1080+ _ -> [])

1081+ (decls, ns) <- get -- ignore decls in HO types

1082+ put (PTacImplicit 10 l n scr ty : decls,

1083+ nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

1084+ imps True (n:env) sc

10661085 imps top env (PEq _ l r)

10671086 = do (decls, ns) <- get

10681087 let isn = namesIn uvars ist l ++ namesIn uvars ist r

@@ -1171,6 +1190,11 @@ aiFn ist fc f as

11711190 case find n given [] of

11721191 Just (tm, given') -> PImp p l n tm : insertImpl ps given'

11731192 Nothing -> PImp p l n Placeholder : insertImpl ps given

1193+ insertImpl (PTacImplicit p l n sc ty : ps) given =

1194+ case find n given [] of

1195+ Just (tm, given') -> PTacImplicit p l n sc tm : insertImpl ps given'

1196+ Nothing -> PTacImplicit p l n sc sc

1197+ : insertImpl ps given

11741198 insertImpl expected [] = []

11751199 insertImpl _ given = given

11761200

src/Idris/Coverage.hs+3−2

@@ -19,7 +19,7 @@ import Debug.Trace

1919-- This will only work after the given clauses have been typechecked and the

2020-- names are fully explicit!

2121

22−genClauses :: FC -> Name -> [Term] -> [PClause] -> Idris [PClause]

22+genClauses :: FC -> Name -> [Term] -> [PClause] -> Idris [PTerm]

2323genClauses fc n xs given

2424 = do i <- getIState

2525 let lhss = map (getLHS i) xs

@@ -34,7 +34,8 @@ genClauses fc n xs given

3434 _ -> repeat (pexp Placeholder)

3535 let new = mnub i $ filter (noMatch i) $ mkClauses parg all_args

3636 logLvl 7 $ "New clauses: \n" ++ showSep "\n" (map (showImp True) new)

37− return (map (\t -> PClause n t [] PImpossible []) new)

37+ return new

38+-- return (map (\t -> PClause n t [] PImpossible []) new)

3839 where getLHS i term

3940 | (f, args) <- unApply term = map (\t -> delab' i t True) args

4041 | otherwise = []

src/Idris/Delaborate.hs+1

@@ -61,6 +61,7 @@ delab' ist tm fullname = de [] tm

6161 imp (PImp p l n _) arg = PImp p l n arg

6262 imp (PExp p l _) arg = PExp p l arg

6363 imp (PConstraint p l _) arg = PConstraint p l arg

64+ imp (PTacImplicit p l n sc _) arg = PTacImplicit p l n sc arg

6465

6566pshow :: IState -> Err -> String

6667pshow i (Msg s) = s

src/Idris/ElabDecls.hs+16−17

@@ -131,12 +131,10 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

131131 cov <- coverage

132132 pcover <-

133133 if cov

134− then idrisCatch

135− (do missing <- genClauses fc n (map fst pdef) cs

136− mapM_ (elabClause info fc True) missing

137− return True)

138− (\c -> do -- iputStrLn $ "Warning: " ++ show c

139− return False)

134+ then do missing <- genClauses fc n (map fst pdef) cs

135+ missing' <- filterM (checkPossible info fc True n) missing

136+ logLvl 5 $ "Must be unreachable: " ++ show missing' ++ " from " ++ show missing

137+ return (null missing')

140138 else return False

141139 pdef' <- applyOpts pdef

142140 let tree@(CaseDef _ sc _) = simpleCase tcase pcover pdef

@@ -207,25 +205,26 @@ elabVal info aspat tm_in

207205 logLvl 2 (show vtm)

208206 recheckC ctxt (FC "prompt" 0) [] vtm

209207

210−elabClause :: ElabInfo -> FC -> Bool -> PClause -> Idris (Maybe (Term, Term))

211−elabClause info fc tcgen (PClause fname lhs_in [] PImpossible [])

208+checkPossible :: ElabInfo -> FC -> Bool -> Name -> PTerm -> Idris Bool

209+checkPossible info fc tcgen fname lhs_in

212210 = do ctxt <- getContext

213211 i <- get

214212 let lhs = addImpl i lhs_in

215− -- if the LHS type checks, it is possible, so report an error

213+ -- if the LHS type checks, it is possible

216214 case elaborate ctxt (MN 0 "patLHS") infP []

217215 (erun fc (buildTC i info True tcgen fname (infTerm lhs))) of

218216 OK ((lhs', _, _), _) ->

219217 do let lhs_tm = orderPats (getInferTerm lhs')

220−-- checkInferred fc (delab' i lhs_tm True) lhs

221218 b <- inferredDiff fc (delab' i lhs_tm True) lhs

222− if b

223− then return ()

224− else fail $ show fc ++ ":" ++ showImp True (delab' i lhs_tm True) ++

225− " is a possible case"

226− ++ "\n" ++ showImp True lhs

227− Error _ -> return ()

228− return Nothing

219+ return (not b)

220+-- trace (show (delab' i lhs_tm True) ++ "\n" ++ show lhs) $ return (not b)

221+ Error _ -> return False

222+

223+elabClause :: ElabInfo -> FC -> Bool -> PClause -> Idris (Maybe (Term, Term))

224+elabClause info fc tcgen (PClause fname lhs_in [] PImpossible [])

225+ = do b <- checkPossible info fc tcgen fname lhs_in

226+ if b then fail $ show fc ++ ":" ++ show lhs_in ++ " is a possible case"

227+ else return Nothing

229228elabClause info fc tcgen (PClause fname lhs_in withs rhs_in whereblock)

230229 = do ctxt <- getContext

231230 -- Build the LHS as an "Infer", and pull out its type and

src/Idris/ElabTerm.hs+3−1

@@ -246,7 +246,9 @@ elab ist info pattern tcgen fn tm

246246 Just xs@(_:_) -> NS n xs

247247 _ -> n

248248 elab' ina (PProof ts) = do mapM_ (runTac True ist) ts

249− elab' ina (PTactics ts) = do mapM_ (runTac False ist) ts

249+ elab' ina (PTactics ts)

250+ | not pattern = do mapM_ (runTac False ist) ts

251+ | otherwise = elab' ina Placeholder

250252 elab' ina (PElabError e) = fail e

251253 elab' ina c@(PCase fc scr opts)

252254 = do attack

src/Idris/Parser.hs+11

@@ -806,6 +806,17 @@ pPi syn =

806806 symbol "->"

807807 sc <- pExpr syn

808808 return (bindList (PPi (Imp lazy st)) xt sc))

809+ <|> try (do lchar '{'; reserved "auto"

810+ xt <- tyDeclList syn; lchar '}'

811+ symbol "->"

812+ sc <- pExpr syn

813+ return (bindList (PPi (TacImp False Dynamic (PTactics [Trivial]))) xt sc))

814+ <|> try (do lchar '{'; reserved "default"

815+ script <- pSimpleExpr syn

816+ xt <- tyDeclList syn; lchar '}'

817+ symbol "->"

818+ sc <- pExpr syn

819+ return (bindList (PPi (TacImp False Dynamic script)) xt sc))

809820 <|> do --lazy <- option False (do lchar '|'; return True)

810821 lchar '{'; reserved "static"; lchar '}'

811822 t <- pExpr' syn