3501adb · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Changed way of building pattern match terms

3501adbEdwin Brady15 years ago

miniidris.cabal+1

compare with master

unifiedsplit

@@ -26,3 +26,4 @@ Executable miniidris

26 Extensions: MultiParamTypeClasses, FunctionalDependencies,

27 FlexibleInstances

28 ghc-prof-options: -auto-all

29+ ghc-options: -rtsopts

src/Elaborate.hs+21−10

@@ -51,6 +51,10 @@ get_env :: Elab Env

51get_env = do (p, _) <- get

52 lift $ envAtFocus p

54+get_holes :: Elab [Name]

55+get_holes = do (p, _) <- get

56+ return (holes p)

57+

54-- get the current goal type

58-- get the current goal type

55goal :: Elab Type

59goal :: Elab Type

56goal = do (p, _) <- get

60goal = do (p, _) <- get

@@ -65,8 +69,9 @@ get_type tm = do ctxt <- get_context

66-- given a desired hole name, return a unique hole name

70-- given a desired hole name, return a unique hole name

67unique_hole :: Name -> Elab Name

71unique_hole :: Name -> Elab Name

68−unique_hole n = do env <- get_env

72+unique_hole n = do (p, _) <- get

73+ env <- get_env

69− return (uniq n (map fst env))

74+ return (uniq n (holes p ++ map fst env))

70 where

75 where

71 uniq n hs | n `elem` hs = uniq (next n) hs

76 uniq n hs | n `elem` hs = uniq (next n) hs

72 | otherwise = n

77 | otherwise = n

@@ -125,8 +130,8 @@ intro n = processTactic' (Intro n)

125forall :: Name -> Raw -> Elab ()

130forall :: Name -> Raw -> Elab ()

126forall n t = processTactic' (Forall n t)

131forall n t = processTactic' (Forall n t)

127

132

128−patvar :: Name -> Raw -> Elab ()

133+patvar :: Name -> Elab ()

129−patvar n t = processTactic' (PatVar n t)

134+patvar n = processTactic' (PatVar n)

130

135

131focus :: Name -> Elab ()

136focus :: Name -> Elab ()

132focus n = processTactic' (Focus n)

137focus n = processTactic' (Focus n)

@@ -148,7 +153,13 @@ prepare_apply :: Raw -> [Bool] -> Elab [Name]

148prepare_apply fn imps =

153prepare_apply fn imps =

149 do ty <- get_type fn

154 do ty <- get_type fn

150 -- let claims = getArgs ty imps

155 -- let claims = getArgs ty imps

151− doClaims ty imps []

156+ claims <- doClaims ty imps []

157+ (p, s) <- get

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

159+ let n = length (filter not imps)

160+ let (h : hs) = holes p

161+ put (p { holes = h : (reverse (take n hs) ++ drop n hs) }, s)

162+ return claims

152 where

163 where

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

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

154 do n <- unique_hole n'

165 do n <- unique_hole n'

@@ -164,7 +175,7 @@ apply :: Raw -> [Bool] -> Elab ()

164apply fn imps =

175apply fn imps =

165 do args <- prepare_apply fn imps

176 do args <- prepare_apply fn imps

166 fill (raw_apply fn (map Var args))

177 fill (raw_apply fn (map Var args))

167− when (not (null args)) end_unify

178+ end_unify

168

179

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

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

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

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

@@ -173,10 +184,10 @@ arg n tyhole = do ty <- unique_hole tyhole

173 claim ty (RSet 0)

184 claim ty (RSet 0)

174 forall n (Var ty)

185 forall n (Var ty)

175

186

176−patarg :: Name -> Name -> Elab ()

187+-- patarg :: Name -> Name -> Elab ()

177−patarg n tyhole = do ty <- unique_hole tyhole

188+-- patarg n tyhole = do ty <- unique_hole tyhole

178− claim ty (RSet 0)

189+-- claim ty (RSet 0)

179− patvar n (Var ty)

190+-- patvar n (Var ty)

180

191

181-- Some combinators on elaborations

192-- Some combinators on elaborations

182

193

src/ProofState.hs+31−24

@@ -47,21 +47,13 @@ data Tactic = Attack

47 | CheckIn Raw

48 | Intro Name

49 | Forall Name Raw

50− | PatVar Name Raw

50+ | PatVar Name

51 | Focus Name

52 | MoveLast Name

53 | ProofState

54 | Undo

55 | QED

57−data TacticAction = AddGoal Name -- add a new goal, solve immediately

58− | NextGoal Name -- add a new goal, solve it after current one

59− | FocusGoal Name -- focus on this goal next

60− | MoveGoal Name -- move this goal to the end of the hole queue

61− | Solved Name

62− | AlsoSolved [(Name, Term)] -- variables solved by unification

63− | Log String

64−

65-- Some utilites on proof and tactic states

57-- Some utilites on proof and tactic states

67instance Show ProofState where

59instance Show ProofState where

@@ -69,21 +61,22 @@ instance Show ProofState where

69 show (PS nm (h:hs) _ tm _ _ i _ ctxt _ _)

61 show (PS nm (h:hs) _ tm _ _ i _ ctxt _ _)

70 = let OK g = goal (Just h) tm

62 = let OK g = goal (Just h) tm

71 wkenv = premises g in

63 wkenv = premises g in

64+ "Other goals: " ++ show hs ++ "\n" ++

72 showPs wkenv (reverse wkenv) ++ "\n" ++

65 showPs wkenv (reverse wkenv) ++ "\n" ++

73 "-------------------------------- (" ++ show nm ++

66 "-------------------------------- (" ++ show nm ++

74− ") -------\n" ++

67+ ") -------\n " ++

75 show h ++ " : " ++ showG wkenv (goalType g) ++ "\n"

68 show h ++ " : " ++ showG wkenv (goalType g) ++ "\n"

76 where showPs env [] = ""

69 where showPs env [] = ""

77 showPs env ((n, Let t v):bs)

70 showPs env ((n, Let t v):bs)

78 = " " ++ show n ++ " : " ++

71 = " " ++ show n ++ " : " ++

79− showEnv env (normalise ctxt env t) ++ " = " ++

72+ showEnv env ({- normalise ctxt env -} t) ++ " = " ++

80− showEnv env (normalise ctxt env v) ++

73+ showEnv env ({- normalise ctxt env -} v) ++

81 "\n" ++ showPs env bs

74 "\n" ++ showPs env bs

82 showPs env ((n, b):bs)

75 showPs env ((n, b):bs)

83 = " " ++ show n ++ " : " ++

76 = " " ++ show n ++ " : " ++

84− showEnv env (normalise ctxt env (binderTy b)) ++

77+ showEnv env ({- normalise ctxt env -} (binderTy b)) ++

85 "\n" ++ showPs env bs

78 "\n" ++ showPs env bs

86− showG ps (Guess t v) = showEnv ps (normalise ctxt ps t) ++

79+ showG ps (Guess t v) = showEnv ps ({- normalise ctxt ps -} t) ++

87 " =?= " ++ showEnv ps v

80 " =?= " ++ showEnv ps v

88 showG ps b = showEnv ps (binderTy b)

81 showG ps b = showEnv ps (binderTy b)

@@ -211,14 +204,14 @@ fill guess ctxt env (Bind x (Hole ty) sc) =

211 ps <- get

204 ps <- get

212 let (uh, uns) = unified ps

205 let (uh, uns) = unified ps

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

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

214− addLog (show (uh, uns ++ ns))

207+-- addLog (show (uh, uns ++ ns))

215 return $ Bind x (Guess ty val) sc

208 return $ Bind x (Guess ty val) sc

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

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

217

210

218solve :: RunTactic

211solve :: RunTactic

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

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

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

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

221− return $ Bind x (Let ty val) sc -- instantiate val (pToV x sc)

214+ return $ {- Bind x (Let ty val) sc -} instantiate val (pToV x sc)

222 | otherwise = fail "I see a hole in your solution."

215 | otherwise = fail "I see a hole in your solution."

223solve _ _ _ = fail "Not a guess."

216solve _ _ _ = fail "Not a guess."

224

217

@@ -238,11 +231,10 @@ forall n ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

238 lift $ isSet ctxt env t

231 lift $ isSet ctxt env t

239 return $ Bind n (Pi tyv) (Bind x (Hole t) (P Bound x t))

232 return $ Bind n (Pi tyv) (Bind x (Hole t) (P Bound x t))

240

233

241−patvar :: Name -> Raw -> RunTactic

234+patvar :: Name -> RunTactic

242−patvar n ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

235+patvar n ctxt env (Bind x (Hole t) sc) =

243− do (tyv, tyt) <- lift $ check ctxt env ty

236+ do action (\ps -> ps { holes = holes ps \\ [x] })

244− lift $ isSet ctxt env tyt

245− return $ Bind n (PVar tyv) (Bind x (Hole t) (P Bound x t))

237+ return $ Bind n (PVar t) (instantiate (P Bound n t) (pToV x sc))

246

238

247compute :: RunTactic

239compute :: RunTactic

248compute ctxt env (Bind x (Hole ty) sc) =

240compute ctxt env (Bind x (Hole ty) sc) =

@@ -276,9 +268,10 @@ solve_unified ctxt env tm =

276 do ps <- get

268 do ps <- get

277 let (_, ns) = unified ps

269 let (_, ns) = unified ps

278 action (\ps -> ps { holes = holes ps \\ map fst ns })

270 action (\ps -> ps { holes = holes ps \\ map fst ns })

271+-- action (\ps -> ps { pterm = updateSolved ns (pterm ps) })

279 return (updateSolved ns tm)

272 return (updateSolved ns tm)

280 where

273 where

281− updateSolved xs (Bind n b@(Hole _) t)

274+ updateSolved xs (Bind n (Hole ty) t)

282 | Just v <- lookup n xs = instantiate v (pToV n (updateSolved xs t))

275 | Just v <- lookup n xs = instantiate v (pToV n (updateSolved xs t))

283 updateSolved xs (Bind n b t)

276 updateSolved xs (Bind n b t)

284 | otherwise = Bind n (fmap (updateSolved xs) b) (updateSolved xs t)

277 | otherwise = Bind n (fmap (updateSolved xs) b) (updateSolved xs t)

@@ -295,7 +288,7 @@ solve_unified ctxt env tm =

295

288

296processTactic :: Tactic -> ProofState -> TC (ProofState, String)

289processTactic :: Tactic -> ProofState -> TC (ProofState, String)

297processTactic QED ps = case holes ps of

290processTactic QED ps = case holes ps of

298− [] -> do let tm = pterm ps

291+ [] -> do let tm = {- normalise (context ps) [] -} (pterm ps)

299 (tm', ty') <- recheck (context ps) [] tm

292 (tm', ty') <- recheck (context ps) [] tm

300 return (ps { done = True, pterm = tm' },

293 return (ps { done = True, pterm = tm' },

301 "Proof complete: " ++ showEnv [] tm')

294 "Proof complete: " ++ showEnv [] tm')

@@ -304,6 +297,20 @@ processTactic ProofState ps = return (ps, showEnv [] (pterm ps))

304processTactic Undo ps = case previous ps of

297processTactic Undo ps = case previous ps of

305 Nothing -> Error "Nothing to undo."

298 Nothing -> Error "Nothing to undo."

306 Just pold -> return (pold, "")

299 Just pold -> return (pold, "")

300+processTactic EndUnify ps = let (h, ns) = unified ps

301+ tm' = updateSolved ns (pterm ps) in

302+ return (ps { pterm = tm',

303+ unified = (h, []),

304+ holes = holes ps \\ map fst ns }, "")

305+ where

306+ updateSolved xs (Bind n (Hole ty) t)

307+ | Just v <- lookup n xs = instantiate v (pToV n (updateSolved xs t))

308+ updateSolved xs (Bind n b t)

309+ | otherwise = Bind n (fmap (updateSolved xs) b) (updateSolved xs t)

310+ updateSolved xs (App f a) = App (updateSolved xs f) (updateSolved xs a)

311+ updateSolved xs (P _ n _)

312+ | Just v <- lookup n xs = v

313+ updateSolved xs t = t

307processTactic t ps

314processTactic t ps

308 = case holes ps of

315 = case holes ps of

309 [] -> Error "Nothing to fill in."

316 [] -> Error "Nothing to fill in."

@@ -327,7 +334,7 @@ process t h = tactic (Just h) (mktac t)

327 mktac Compute = compute

334 mktac Compute = compute

328 mktac (Intro n) = intro n

335 mktac (Intro n) = intro n

329 mktac (Forall n t) = forall n t

336 mktac (Forall n t) = forall n t

330− mktac (PatVar n t) = patvar n t

337+ mktac (PatVar n) = patvar n

331 mktac (CheckIn r) = check_in r

338 mktac (CheckIn r) = check_in r

332 mktac (EvalIn r) = eval_in r

339 mktac (EvalIn r) = eval_in r

333 mktac (Focus n) = focus n

340 mktac (Focus n) = focus n

src/ShellParser.hs+3−4

@@ -57,10 +57,9 @@ pTactic = do reserved "attack"; return attack

57 <|> do reserved "intro"; n <- iName; return (intro n)

58 <|> do reserved "forall"; n <- iName; lchar ':'; ty <- pTerm

59 return (forall n ty)

60− <|> do reserved "arg"; n <- iName; t <- iName; return (arg n t)

60+-- <|> do reserved "arg"; n <- iName; t <- iName; return (arg n t)

61− <|> do reserved "patvar"; n <- iName; lchar ':'; ty <- pTerm

61+ <|> do reserved "patvar"; n <- iName; return (patvar n)

62− return (patvar n ty)

63− <|> do reserved "patarg"; n <- iName; t <- iName; return (patarg n t)

62+-- <|> do reserved "patarg"; n <- iName; t <- iName; return (patarg n t)

64 <|> do reserved "eval"; t <- pTerm; return (eval_in t)

63 <|> do reserved "eval"; t <- pTerm; return (eval_in t)

65 <|> do reserved "check"; t <- pTerm; return (check_in t)

64 <|> do reserved "check"; t <- pTerm; return (check_in t)

66 <|> do reserved "focus"; n <- iName; return (focus n)

65 <|> do reserved "focus"; n <- iName; return (focus n)

src/Typecheck.hs+1−1

@@ -34,7 +34,7 @@ check :: Context -> Env -> Raw -> TC (Term, Type)

34check ctxt env (Var n)

35 | Just (i, ty) <- lookupTyEnv n env = return (P Bound n ty, ty)

36 | Just (P nt n' ty) <- lookupP n ctxt = return (P nt n' ty, ty)

37− | otherwise = do fail $ "No such variable " ++ show n

37+ | otherwise = do fail $ "No such variable " ++ show n ++ " in " ++ show (map fst env)

38check ctxt env (RApp f a)

39 = do (fv, fty) <- check ctxt env f

40 (av, aty) <- check ctxt env a