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

git.iko.soy/Idris-dev

on master help sign in

Added (experimentally) auto implicit arguments

98be75cEdwin Brady15 years ago

lib/network/cgi.idr+1−1

compare with master

unifiedsplit

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

116getContent : Int -> IO String

117getContent x = getC x "" where

118 getC : Int -> String -> IO String

119− getC 0 acc = return $ rev acc

119+ getC 0 acc = return $ reverse acc

120 getC n acc = do x <- getChar

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

122

src/Idris/AbsSyntax.hs+24

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

358 pstatic :: Static }

359 | Constraint { plazy :: Bool,

360 pstatic :: Static }

361+ | TacImp { plazy :: Bool,

362+ pstatic :: Static,

363+ pscript :: PTerm }

361 deriving (Show, Eq)

364 deriving (Show, Eq)

362

365

363{-!

366{-!

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

367impl = Imp False Dynamic

370impl = Imp False Dynamic

368expl = Exp False Dynamic

371expl = Exp False Dynamic

369constraint = Constraint False Static

372constraint = Constraint False Static

373+tacimpl = TacImp False Dynamic

370

374

371data FnOpt = Inlinable | TotalFn | TCGen

375data FnOpt = Inlinable | TotalFn | TCGen

372 deriving (Show, Eq)

376 deriving (Show, Eq)

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

544 lazyarg :: Bool, getTm :: t }

548 lazyarg :: Bool, getTm :: t }

545 | PConstraint { priority :: Int,

549 | PConstraint { priority :: Int,

546 lazyarg :: Bool, getTm :: t }

550 lazyarg :: Bool, getTm :: t }

551+ | PTacImplicit { priority :: Int,

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

553+ getScript :: t,

554+ getTm :: t }

547 deriving (Show, Eq, Functor)

555 deriving (Show, Eq, Functor)

548{-!

556{-!

549deriving instance Binary PArg'

557deriving instance Binary PArg'

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

552pimp = PImp 0 True

560pimp = PImp 0 True

553pexp = PExp 0 False

561pexp = PExp 0 False

554pconst = PConstraint 0 False

562pconst = PConstraint 0 False

563+ptacimp = PTacImplicit 0 True

555

564

556type PArg = PArg' PTerm

565type PArg = PArg' PTerm

557

566

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

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

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

768 sArg (PExp _ _ tm) = seArg tm

777 sArg (PExp _ _ tm) = seArg tm

769 sArg (PConstraint _ _ tm) = scArg tm

778 sArg (PConstraint _ _ tm) = scArg tm

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

770

780

771 seArg arg = " " ++ se 0 arg

781 seArg arg = " " ++ se 0 arg

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

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

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

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

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

774

785

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

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

776 | otherwise = str

787 | otherwise = str

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

1063 put (PConstraint 10 l ty : decls,

1074 put (PConstraint 10 l ty : decls,

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

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

1065 imps True (n:env) sc

1076 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

1066 imps top env (PEq _ l r)

1085 imps top env (PEq _ l r)

1067 = do (decls, ns) <- get

1086 = do (decls, ns) <- get

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

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

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

1171 case find n given [] of

1190 case find n given [] of

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

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

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

1192 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

1174 insertImpl expected [] = []

1198 insertImpl expected [] = []

1175 insertImpl _ given = given

1199 insertImpl _ given = given

1176

1200

src/Idris/Coverage.hs+3−2

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

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

20-- names are fully explicit!

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

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

23genClauses fc n xs given

24 = do i <- getIState

25 let lhss = map (getLHS i) xs

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

34 _ -> repeat (pexp Placeholder)

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

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

37+ return new

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

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

38 where getLHS i term

39 where getLHS i term

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

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

40 | otherwise = []

41 | otherwise = []

src/Idris/Delaborate.hs+1

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

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

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

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

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

65pshow :: IState -> Err -> String

66pshow :: IState -> Err -> String

66pshow i (Msg s) = s

67pshow 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

131 cov <- coverage

132 pcover <-

133 if cov

134− then idrisCatch

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

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

136− mapM_ (elabClause info fc True) missing

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

137− return True)

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

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

139− return False)

137+ return (null missing')

140 else return False

138 else return False

141 pdef' <- applyOpts pdef

139 pdef' <- applyOpts pdef

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

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

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

207 logLvl 2 (show vtm)

205 logLvl 2 (show vtm)

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

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

209

207

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

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

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

209+checkPossible info fc tcgen fname lhs_in

212 = do ctxt <- getContext

210 = do ctxt <- getContext

213 i <- get

211 i <- get

214 let lhs = addImpl i lhs_in

212 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

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

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

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

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

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

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

219 do let lhs_tm = orderPats (getInferTerm lhs')

217 do let lhs_tm = orderPats (getInferTerm lhs')

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

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

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

222− if b

223− then return ()

219+ return (not b)

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

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

225− " is a possible case"

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

227− Error _ -> return ()

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"

228− return Nothing

227+ else return Nothing

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

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

230 = do ctxt <- getContext

229 = do ctxt <- getContext

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

230 -- 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

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

247 _ -> n

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

249+ elab' ina (PTactics ts)

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

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

251+ | otherwise = elab' ina Placeholder

250 elab' ina (PElabError e) = fail e

252 elab' ina (PElabError e) = fail e

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

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

252 = do attack

254 = do attack

src/Idris/Parser.hs+11

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

806 symbol "->"

807 sc <- pExpr syn

808 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))

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

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

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

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

811 t <- pExpr' syn

822 t <- pExpr' syn