22b4dc4 · Idris-dev · git.iko.soy

decls.mi+11−7

@@ -8,13 +8,16 @@ data List a = Nil | Cons a (List a);

88

99data Vect : Set -> Nat -> Set where

1010 VNil : Vect a O

11− | (::) : a -> Vect a k -> Vect a (S k);

11+ | (::) : a -> Vect a k -> Vect a (S k);

1212

1313data Env : Vect Set n -> Set where

1414 Empty : Env VNil

1515 | Extend : {xs : Vect Set n} -> a -> Env xs -> Env (a :: xs);

1616

17−plus : Nat -> Nat -> Nat;

17+PLUSTY : Set;

18+PLUSTY = Nat -> Nat -> Nat;

19+

20+plus : PLUSTY;

1821plus O y = y;

1922plus (S k) y = S (plus k y);

2023

@@ -22,15 +25,16 @@ app : Vect a n -> Vect a m -> Vect a (plus n m);

2225app VNil ys = ys;

2326app (x :: xs) ys = x :: app xs ys;

2427

28+map : (a -> b) -> Vect a n -> Vect b n;

29+map f VNil = VNil;

30+map f (x :: xs) = f x :: map f xs;

31+

2532test : Nat -> Vect Nat (S (S O));

2633test n = n :: n :: VNil;

2734

2835tvect : Vect Nat (S (S (S (S O))));

2936tvect = app (test O) (test (S O));

3037

31−infixl 5 .+. ;

32−

33−(.+.) : Nat -> Nat -> Nat;

34−O .+. y = y;

35−(S k) .+. y = S (k .+. y);

38+mapPlus : Vect Nat n -> Vect Nat n;

39+mapPlus = map (plus (S (S O)));

3640

src/Core/Elaborate.hs+52−1

@@ -117,6 +117,12 @@ exact t = processTactic' (Exact t)

117117fill :: Raw -> Elab ()

118118fill t = processTactic' (Fill t)

119119

120+prep_fill :: Name -> [Name] -> Elab ()

121+prep_fill n ns = processTactic' (PrepFill n ns)

122+

123+complete_fill :: Elab ()

124+complete_fill = processTactic' CompleteFill

125+

120126solve :: Elab ()

121127solve = processTactic' Solve

122128

@@ -171,8 +177,10 @@ undo = processTactic' Undo

171177prepare_apply :: Raw -> [Bool] -> Elab [Name]

172178prepare_apply fn imps =

173179 do ty <- get_type fn

180+ ctxt <- get_context

181+ env <- get_env

174182 -- let claims = getArgs ty imps

175− claims <- doClaims ty imps []

183+ claims <- doClaims (normalise ctxt env ty) imps []

176184 (p, s) <- get

177185 -- reverse the claims we made so that args go left to right

178186 let n = length (filter not imps)

@@ -204,6 +212,49 @@ apply fn imps =

204212 end_unify

205213 return args

206214

215+apply_elab :: Name -> [Maybe (Elab ())] -> Elab ()

216+apply_elab n args =

217+ do ty <- get_type (Var n)

218+ ctxt <- get_context

219+ env <- get_env

220+ claims <- doClaims (normalise ctxt env ty) args []

221+ prep_fill n (map fst claims)

222+ elabClaims claims

223+ complete_fill

224+ end_unify

225+ where

226+ doClaims (Bind n' (Pi t) sc) (i : is) claims =

227+ do n <- unique_hole n'

228+ when (null claims) (start_unify n)

229+ let sc' = instantiate (P Bound n t) sc

230+ claim n (forget t)

231+ doClaims sc' is ((n, i) : claims)

232+ doClaims t [] claims = return (reverse claims)

233+ doClaims _ _ _ = fail "Wrong number of arguments"

234+

235+ elabClaims [] = return ()

236+ elabClaims ((n, Nothing) : xs) = elabClaims xs

237+ elabClaims ((n, Just elaboration) : xs) =

238+ do (p, _) <- get

239+ focus n; elaboration; elabClaims xs

240+

241+simple_app :: Elab () -> Elab () -> Elab ()

242+simple_app fun arg =

243+ do a <- unique_hole (MN 0 "a")

244+ b <- unique_hole (MN 0 "b")

245+ f <- unique_hole (MN 0 "f")

246+ s <- unique_hole (MN 0 "s")

247+ claim a (RSet 0)

248+ claim b (RSet 0)

249+ claim f (RBind (MN 0 "aX") (Pi (Var a)) (Var b))

250+ start_unify s

251+ claim s (Var a)

252+ prep_fill f [s]

253+ focus f; fun

254+ focus s; arg

255+ complete_fill

256+ end_unify

257+

207258-- Abstract over an argument of unknown type, giving a name for the hole

208259-- which we'll fill with the argument type too.

209260arg :: Name -> Name -> Elab ()

src/Core/Evaluate.hs+16−10

@@ -55,6 +55,10 @@ eval ctxt genv tm = ev [] tm where

5555 ev env (P Ref n ty) = case lookupDef n ctxt of

5656 Just (Function (Fun _ _ _ v)) -> v

5757 Just (Constant nt ty hty) -> VP nt n hty

58+ Just (CaseOp _ [] tree) ->

59+ case evCase env [] [] tree of

60+ (Nothing, _) -> VP Ref n (ev env ty)

61+ (Just v, _) -> v

5862 _ -> VP Ref n (ev env ty)

5963 ev env (P nt n ty) = VP nt n (ev env ty)

6064 ev env (V i) | i < length env = env !! i

@@ -65,28 +69,30 @@ eval ctxt genv tm = ev [] tm where

6569 = VBind n (Let (ev env t) (ev env v)) $ (\x -> ev (ev env v : env) sc)

6670 ev env (Bind n b sc) = VBind n (vbind env b) (\x -> ev (x:env) sc)

6771 where vbind env t = fmap (ev env) t

68− ev env (App f a) = evApply env [a] f

72+ ev env (App f a) = evApply env [ev env a] (ev env f)

6973 ev env (Set i) = VSet i

7074

71− evApply env args (App f a) = evApply env (a:args) f

72− evApply env args f = apply env (ev env f) args

75+ evApply env args (VApp f a) = evApply env (a:args) f

76+ evApply env args f = apply env f args

7377

74− apply env (VBind n (Lam t) sc) (a:as) = wknV (-1) $ apply env (sc (ev env a)) as

78+ apply env (VBind n (Lam t) sc) (a:as) = wknV (-1) $ apply env (sc a) as

7579 apply env (VP Ref n ty) args

7680 | Just (CaseOp _ ns tree) <- lookupDef n ctxt

7781 = case evCase env ns args tree of

78− Nothing -> unload env (VP Ref n ty) args

79− Just v -> v

82+ (Nothing, _) -> unload env (VP Ref n ty) args

83+ (Just v, rest) -> evApply env rest v

8084 apply env f (a:as) = unload env f (a:as)

8185 apply env f [] = f

8286

8387 unload env f [] = f

84− unload env f (a:as) = unload env (VApp f (ev env a)) as

88+ unload env f (a:as) = unload env (VApp f a) as

8589

8690 evCase env ns args tree

87− | length ns == length args

88− = evTree env (zipWith (\n t -> (n, ev env t)) ns args) tree

89− | otherwise = Nothing

91+ | length ns <= length args

92+ = let args' = take (length ns) args

93+ rest = drop (length ns) args in

94+ (evTree env (zipWith (\n t -> (n, t)) ns args') tree, rest)

95+ | otherwise = (Nothing, args)

9096

9197 evTree :: [Value] -> [(Name, Value)] -> SC -> Maybe Value

9298 evTree env amap (UnmatchedCase str) = Nothing

src/Core/ProofState.hs+20

@@ -38,6 +38,8 @@ data Tactic = Attack

3838 | Claim Name Raw

3939 | Exact Raw

4040 | Fill Raw

41+ | PrepFill Name [Name]

42+ | CompleteFill

4143 | Regret

4244 | Solve

4345 | StartUnify Name

@@ -210,6 +212,22 @@ fill guess ctxt env (Bind x (Hole ty) sc) =

210212 return $ Bind x (Guess ty val) sc

211213fill _ _ _ _ = fail "Can't fill here."

212214

215+prep_fill :: Name -> [Name] -> RunTactic

216+prep_fill f as ctxt env (Bind x (Hole ty) sc) =

217+ do let val = mkApp (P Ref f undefined) (map (\n -> P Ref n undefined) as)

218+ return $ Bind x (Guess ty val) sc

219+prep_fill f as ctxt env t = fail $ "Can't prepare fill at " ++ show t

220+

221+complete_fill :: RunTactic

222+complete_fill ctxt env (Bind x (Guess ty val) sc) =

223+ do let guess = forget val

224+ (val', valty) <- lift $ check ctxt env guess

225+ ns <- lift $ unify ctxt env valty ty

226+ ps <- get

227+ let (uh, uns) = unified ps

228+ put (ps { unified = (uh, uns ++ ns) })

229+ return $ Bind x (Guess ty val) sc

230+

213231solve :: RunTactic

214232solve ctxt env (Bind x (Guess ty val) sc)

215233 | pureTerm val = do action (\ps -> ps { holes = holes ps \\ [x] })

@@ -340,6 +358,8 @@ process t h = tactic (Just h) (mktac t)

340358 mktac (Claim n r) = claim n r

341359 mktac (Exact r) = exact r

342360 mktac (Fill r) = fill r

361+ mktac (PrepFill n ns) = prep_fill n ns

362+ mktac CompleteFill = complete_fill

343363 mktac Regret = regret

344364 mktac Solve = solve

345365 mktac (StartUnify n) = start_unify n

src/Core/TT.hs+4

@@ -220,6 +220,10 @@ unApply t = ua [] t where

220220 ua args (App f a) = ua (a:args) f

221221 ua args t = (t, reverse args)

222222

223+mkApp :: TT n -> [TT n] -> TT n

224+mkApp f [] = f

225+mkApp f (a:as) = mkApp (App f a) as

226+

223227forget :: TT Name -> Raw

224228forget tm = fe [] tm

225229 where

src/Idris/AbsSyntax.hs+20−13

@@ -22,7 +22,7 @@ defaultOpts = IOption 0

2222

2323data IState = IState { tt_ctxt :: Context,

2424 idris_infixes :: [FixDecl],

25− idris_implicits :: Ctxt [Name],

25+ idris_implicits :: Ctxt ([Name], Int), -- implicits, arity

2626 idris_log :: String,

2727 idris_options :: IOption

2828 }

@@ -237,6 +237,7 @@ infP = P (TCon 0) inferTy (Set 0)

237237getInferTerm, getInferType :: Term -> Term

238238getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc

239239getInferTerm (App (App _ _) tm) = tm

240+getInferTerm tm = error ("getInferTerm " ++ show tm)

240241

241242getInferType (Bind n b sc) = Bind n b $ getInferType sc

242243getInferType (App (App _ ty) _) = ty

@@ -247,23 +248,25 @@ getInferType (App (App _ ty) _) = ty

247248-- Add implicit Pi bindings for any names in the term which appear in an

248249-- argument position.

249250

250−implicitise :: IState -> PTerm -> (PTerm, [Name])

251+implicitise :: IState -> PTerm -> (PTerm, ([Name], Int))

251252implicitise ist tm

252− = let (declimps, ns) = execState (imps [] tm) ([], []) in

253− (pibind ns tm, ns ++ reverse declimps)

253+ = let (declimps, a, ns) = execState (imps [] tm) ([], 0, []) in

254+ (pibind ns tm, (ns ++ reverse declimps, a))

254255 where

255256 imps env (PApp f is es)

256− = do (decls, ns) <- get

257+ = do (decls, a, ns) <- get

257258 let isn = concatMap (namesIn ist) (map snd is)

258259 let esn = concatMap (namesIn ist) es

259− put (decls, nub (ns ++ ((isn ++ esn) \\ env)))

260+ put (decls, a, nub (ns ++ ((isn ++ esn) \\ env)))

260261 imps env (PPi Imp n ty sc)

261262 = do imps env ty

262− (decls, ns) <- get

263− put (n:decls, ns)

263+ (impdecls, a, ns) <- get

264+ put (n:impdecls, a+1, ns)

264265 imps (n:env) sc

265266 imps env (PPi Exp n ty sc)

266267 = do imps env ty

268+ (impdecls, a, ns) <- get

269+ put (impdecls, a+1, ns)

267270 imps (n:env) sc

268271 imps env (PLam n ty sc)

269272 = do imps env ty

@@ -297,12 +300,16 @@ addImpl ist ptm = ai [] ptm

297300

298301 aiFn env (PRef f) is es | not (f `elem` env)

299302 = case lookupCtxt f (idris_implicits ist) of

300− Just ns -> pApp (PRef f) (insertImpl ns is) es

301− Nothing -> pApp (PRef f) is es

302− aiFn env f is es = pApp f is es

303+ Just (ns, a) -> pApp a (PRef f) (insertImpl ns is) es

304+ Nothing -> pApp 1 (PRef f) is es

305+ aiFn env f is es = pApp 1 f is es

303306

304− pApp f [] [] = f

305− pApp f is es = PApp f is es

307+ pApp a f [] [] = f

308+ pApp a f is es = let rest = drop a es in

309+ appRest (PApp f is (take a es)) rest

310+

311+ appRest f [] = f

312+ appRest f (a : as) = appRest (PApp f [] [a]) as

306313

307314 insertImpl [] given = []

308315 insertImpl (n:ns) given

src/Idris/ElabDecls.hs+11−3

@@ -18,7 +18,7 @@ elabType n ty

1818 (ty', log) <- tclift $ elaborate ctxt n (Set 0) (build False ty)

1919 (cty, _) <- tclift $ recheck ctxt [] ty'

2020 logLvl 2 $ "---> " ++ show cty

21− updateContext (addConstant n cty)

21+ updateContext (addConstant n (normalise ctxt [] cty))

2222

2323elabData :: PData -> Idris ()

2424elabData (PDatadecl n t dcons)

@@ -82,6 +82,7 @@ elabClause (PClause _ lhs rhs)

8282 build False rhs

8383 psolve lhs_tm

8484 get_term)

85+ logLvl 2 $ "---> " ++ show rhs'

8586 (crhs, crhsty) <- tclift $ recheck ctxt [] rhs'

8687 return (clhs, crhs)

8788 where

@@ -111,7 +112,7 @@ elabDecl' d@(PClauses n ps) = do iLOG $ "Elaborating " ++ show n

111112

112113build :: Bool -> PTerm -> Elab Term

113114build pattern tm = do elab pattern tm

114− get_term

115+ get_term

115116

116117elab :: Bool -> PTerm -> Elab ()

117118elab pattern tm = do elab' tm

@@ -121,6 +122,9 @@ elab pattern tm = do elab' tm

121122 isph (_, Placeholder) = True

122123 isph _ = False

123124

125+ toElab (_, Placeholder) = Nothing

126+ toElab (_, v) = Just (elab' v)

127+

124128 mkPat = do hs <- get_holes

125129 case hs of

126130 (h: hs) -> do patvar h; mkPat

@@ -148,7 +152,11 @@ elab pattern tm = do elab' tm

148152 = try (do ns <- apply (Var f) (map isph imps ++ map (\x -> False) args)

149153 solve

150154 elabArgs ns (map snd imps ++ args))

151− (do fail "Not tried this way yet")

155+ (do apply_elab f (map toElab imps ++ map (Just . elab') args)

156+ solve)

157+ elab' (PApp f [] [arg])

158+ = do simple_app (elab' f) (elab' arg)

159+ solve

152160 elab' x = fail $ "Not implemented " ++ show x

153161

154162 elabArgs [] _ = return ()

src/Idris/Parser.hs+6−3

@@ -56,7 +56,10 @@ collect (PClauses _ [c@(PClause n l r)] : ds) = clauses n [c] ds

5656collect (d : ds) = d : collect ds

5757collect [] = []

5858

59−pFullExpr = do x <- pExpr; eof; return x

59+pFullExpr :: IParser PTerm

60+pFullExpr = do x <- pExpr; eof;

61+ i <- getState

62+ return (addImpl i x)

6063

6164pDecl :: IParser PDecl

6265pDecl = do d <- pDecl'

@@ -222,8 +225,8 @@ pClause = try (do n <- pfName

222225implicit :: Name -> PTerm -> IParser PTerm

223226implicit n ptm

224227 = do i <- getState

225− let (tm', names) = implicitise i ptm

226− setState (i { idris_implicits = addDef n names (idris_implicits i) })

228+ let (tm', name_arity) = implicitise i ptm

229+ setState (i { idris_implicits = addDef n name_arity (idris_implicits i) })

227230 return tm'

228231

229232addImplicits :: PTerm -> IParser PTerm

src/Idris/REPL.hs+1

@@ -8,6 +8,7 @@ import Idris.ElabDecls

88

99import Core.Evaluate

1010import Core.ProofShell

11+import Core.TT

1112

1213import System.Console.Readline

1314import Control.Monad