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

decls.mi+11−7

compare with master

unifiedsplit

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

8

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

10 VNil : Vect a O

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

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

12

13data Env : Vect Set n -> Set where

14 Empty : Env VNil

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

16

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

17+PLUSTY : Set;

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

19+

20+plus : PLUSTY;

18plus O y = y;

21plus O y = y;

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

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

20

23

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

22app VNil ys = ys;

25app VNil ys = ys;

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

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

24

27

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+

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

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

26test n = n :: n :: VNil;

33test n = n :: n :: VNil;

27

34

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

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

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

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

30

37

31−infixl 5 .+. ;

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

32−

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

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

34−O .+. y = y;

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

36

40

src/Core/Elaborate.hs+52−1

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

117fill :: Raw -> Elab ()

118fill t = processTactic' (Fill t)

119

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+

120solve :: Elab ()

126solve :: Elab ()

121solve = processTactic' Solve

127solve = processTactic' Solve

122

128

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

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

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

172prepare_apply fn imps =

178prepare_apply fn imps =

173 do ty <- get_type fn

179 do ty <- get_type fn

180+ ctxt <- get_context

181+ env <- get_env

174 -- let claims = getArgs ty imps

182 -- let claims = getArgs ty imps

175− claims <- doClaims ty imps []

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

176 (p, s) <- get

184 (p, s) <- get

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

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

178 let n = length (filter not imps)

186 let n = length (filter not imps)

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

204 end_unify

212 end_unify

205 return args

213 return args

206

214

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+

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

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

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

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

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

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

src/Core/Evaluate.hs+16−10

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

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

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

57 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

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

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

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

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

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

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

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

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

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

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

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

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

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

69 ev env (Set i) = VSet i

73 ev env (Set i) = VSet i

70

74

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

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

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

76+ evApply env args f = apply env f args

73

77

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

75 apply env (VP Ref n ty) args

79 apply env (VP Ref n ty) args

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

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

77 = case evCase env ns args tree of

81 = case evCase env ns args tree of

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

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

79− Just v -> v

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

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

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

81 apply env f [] = f

85 apply env f [] = f

82

86

83 unload env f [] = f

87 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

85

89

86 evCase env ns args tree

90 evCase env ns args tree

87− | length ns == length args

91+ | length ns <= length args

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

93+ rest = drop (length ns) args in

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

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

89− | otherwise = Nothing

95+ | otherwise = (Nothing, args)

90

96

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

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

92 evTree env amap (UnmatchedCase str) = Nothing

98 evTree env amap (UnmatchedCase str) = Nothing

src/Core/ProofState.hs+20

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

38 | Claim Name Raw

39 | Exact Raw

40 | Fill Raw

41+ | PrepFill Name [Name]

42+ | CompleteFill

41 | Regret

43 | Regret

42 | Solve

44 | Solve

43 | StartUnify Name

45 | StartUnify Name

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

210 return $ Bind x (Guess ty val) sc

212 return $ Bind x (Guess ty val) sc

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

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

212

214

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+

213solve :: RunTactic

231solve :: RunTactic

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

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

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

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

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

340 mktac (Claim n r) = claim n r

358 mktac (Claim n r) = claim n r

341 mktac (Exact r) = exact r

359 mktac (Exact r) = exact r

342 mktac (Fill r) = fill r

360 mktac (Fill r) = fill r

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

362+ mktac CompleteFill = complete_fill

343 mktac Regret = regret

363 mktac Regret = regret

344 mktac Solve = solve

364 mktac Solve = solve

345 mktac (StartUnify n) = start_unify n

365 mktac (StartUnify n) = start_unify n

src/Core/TT.hs+4

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

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

221 ua args t = (t, reverse args)

222

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

224+mkApp f [] = f

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

226+

223forget :: TT Name -> Raw

227forget :: TT Name -> Raw

224forget tm = fe [] tm

228forget tm = fe [] tm

225 where

229 where

src/Idris/AbsSyntax.hs+20−13

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

22

23data IState = IState { tt_ctxt :: Context,

24 idris_infixes :: [FixDecl],

25− idris_implicits :: Ctxt [Name],

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

26 idris_log :: String,

27 idris_options :: IOption

28 }

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

237getInferTerm, getInferType :: Term -> Term

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

239getInferTerm (App (App _ _) tm) = tm

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

240

241

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

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

242getInferType (App (App _ ty) _) = ty

243getInferType (App (App _ ty) _) = ty

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

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

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

248-- argument position.

249-- argument position.

249

250

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

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

251implicitise ist tm

252implicitise ist tm

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

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

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

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

254 where

255 where

255 imps env (PApp f is es)

256 imps env (PApp f is es)

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

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

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

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

258 let esn = concatMap (namesIn ist) es

259 let esn = concatMap (namesIn ist) es

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

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

260 imps env (PPi Imp n ty sc)

261 imps env (PPi Imp n ty sc)

261 = do imps env ty

262 = do imps env ty

262− (decls, ns) <- get

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

263− put (n:decls, ns)

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

264 imps (n:env) sc

265 imps (n:env) sc

265 imps env (PPi Exp n ty sc)

266 imps env (PPi Exp n ty sc)

266 = do imps env ty

267 = do imps env ty

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

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

267 imps (n:env) sc

270 imps (n:env) sc

268 imps env (PLam n ty sc)

271 imps env (PLam n ty sc)

269 = do imps env ty

272 = do imps env ty

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

297

300

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

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

299 = case lookupCtxt f (idris_implicits ist) of

302 = case lookupCtxt f (idris_implicits ist) of

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

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

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

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

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

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

303

306

304− pApp f [] [] = f

307+ pApp a f [] [] = f

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

305− pApp f is es = PApp f is es

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

310+

311+ appRest f [] = f

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

306

313

307 insertImpl [] given = []

314 insertImpl [] given = []

308 insertImpl (n:ns) given

315 insertImpl (n:ns) given

src/Idris/ElabDecls.hs+11−3

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

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

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

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

21− updateContext (addConstant n cty)

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

22

23elabData :: PData -> Idris ()

24elabData (PDatadecl n t dcons)

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

82 build False rhs

83 psolve lhs_tm

84 get_term)

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

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

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

86 return (clhs, crhs)

87 return (clhs, crhs)

87 where

88 where

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

111

112

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

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

113build pattern tm = do elab pattern tm

114build pattern tm = do elab pattern tm

114− get_term

115+ get_term

115

116

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

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

117elab pattern tm = do elab' tm

118elab pattern tm = do elab' tm

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

121 isph (_, Placeholder) = True

122 isph (_, Placeholder) = True

122 isph _ = False

123 isph _ = False

123

124

125+ toElab (_, Placeholder) = Nothing

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

127+

124 mkPat = do hs <- get_holes

128 mkPat = do hs <- get_holes

125 case hs of

129 case hs of

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

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

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

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

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

149 solve

153 solve

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

154 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

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

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

153

161

154 elabArgs [] _ = return ()

162 elabArgs [] _ = return ()

src/Idris/Parser.hs+6−3

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

56collect (d : ds) = d : collect ds

57collect [] = []

58

59+pFullExpr :: IParser PTerm

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

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

61+ i <- getState

62+ return (addImpl i x)

60

63

61pDecl :: IParser PDecl

64pDecl :: IParser PDecl

62pDecl = do d <- pDecl'

65pDecl = do d <- pDecl'

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

222implicit :: Name -> PTerm -> IParser PTerm

225implicit :: Name -> PTerm -> IParser PTerm

223implicit n ptm

226implicit n ptm

224 = do i <- getState

227 = do i <- getState

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

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

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

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

227 return tm'

230 return tm'

228

231

229addImplicits :: PTerm -> IParser PTerm

232addImplicits :: PTerm -> IParser PTerm

src/Idris/REPL.hs+1

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

8

9import Core.Evaluate

10import Core.ProofShell

11+import Core.TT

11

12

12import System.Console.Readline

13import System.Console.Readline

13import Control.Monad

14import Control.Monad