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

git.iko.soy/Idris-dev

Changed way of building pattern match terms

commit3501adbbcc4bcf569e5042eec71cbdde6742668d authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateSun 2 Oct 2011, 23:37 (15 years ago) parentc966457

5 files changed+57−39

compare with master

unifiedsplit

miniidris.cabal+1 src/Elaborate.hs+21−10 src/ProofState.hs+31−24 src/ShellParser.hs+3−4 src/Typecheck.hs+1−1

miniidris.cabal+1

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

2626 Extensions: MultiParamTypeClasses, FunctionalDependencies,

2727 FlexibleInstances

2828 ghc-prof-options: -auto-all

29+ ghc-options: -rtsopts

src/Elaborate.hs+21−10

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

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

5252 lift $ envAtFocus p

5353

54+get_holes :: Elab [Name]

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

56+ return (holes p)

57+

5458-- get the current goal type

5559goal :: Elab Type

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

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

6569

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

6771unique_hole :: Name -> Elab Name

68−unique_hole n = do env <- get_env

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

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

73+ env <- get_env

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

7075 where

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

7277 | otherwise = n

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

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

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

127132

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

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

133+patvar :: Name -> Elab ()

134+patvar n = processTactic' (PatVar n)

130135

131136focus :: Name -> Elab ()

132137focus n = processTactic' (Focus n)

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

148153prepare_apply fn imps =

149154 do ty <- get_type fn

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

152163 where

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

154165 do n <- unique_hole n'

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

164175apply fn imps =

165176 do args <- prepare_apply fn imps

166177 fill (raw_apply fn (map Var args))

167− when (not (null args)) end_unify

178+ end_unify

168179

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

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

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

173184 claim ty (RSet 0)

174185 forall n (Var ty)

175186

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

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

178− claim ty (RSet 0)

179− patvar n (Var ty)

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

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

189+-- claim ty (RSet 0)

190+-- patvar n (Var ty)

180191

181192-- Some combinators on elaborations

182193

src/ProofState.hs+31−24

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

4747 | CheckIn Raw

4848 | Intro Name

4949 | Forall Name Raw

50− | PatVar Name Raw

50+ | PatVar Name

5151 | Focus Name

5252 | MoveLast Name

5353 | ProofState

5454 | Undo

5555 | QED

5656

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−

6557-- Some utilites on proof and tactic states

6658

6759instance Show ProofState where

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

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

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

7163 wkenv = premises g in

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

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

7366 "-------------------------------- (" ++ show nm ++

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

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

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

7669 where showPs env [] = ""

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

7871 = " " ++ show n ++ " : " ++

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

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

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

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

8174 "\n" ++ showPs env bs

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

8376 = " " ++ show n ++ " : " ++

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

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

8578 "\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) ++

8780 " =?= " ++ showEnv ps v

8881 showG ps b = showEnv ps (binderTy b)

8982

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

211204 ps <- get

212205 let (uh, uns) = unified ps

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

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

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

215208 return $ Bind x (Guess ty val) sc

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

217210

218211solve :: RunTactic

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

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

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

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

224217

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

238231 lift $ isSet ctxt env t

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

240233

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

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

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

244− lift $ isSet ctxt env tyt

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

234+patvar :: Name -> RunTactic

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

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

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

246238

247239compute :: RunTactic

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

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

276268 do ps <- get

277269 let (_, ns) = unified ps

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

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

279272 return (updateSolved ns tm)

280273 where

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

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

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

283276 updateSolved xs (Bind n b t)

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

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

295288

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

297290processTactic QED ps = case holes ps of

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

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

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

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

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

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

304297processTactic Undo ps = case previous ps of

305298 Nothing -> Error "Nothing to undo."

306299 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

307314processTactic t ps

308315 = case holes ps of

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

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

327334 mktac Compute = compute

328335 mktac (Intro n) = intro n

329336 mktac (Forall n t) = forall n t

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

337+ mktac (PatVar n) = patvar n

331338 mktac (CheckIn r) = check_in r

332339 mktac (EvalIn r) = eval_in r

333340 mktac (Focus n) = focus n

src/ShellParser.hs+3−4

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

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

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

5959 return (forall n ty)

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

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

62− return (patvar n ty)

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

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

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

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

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

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

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

src/Typecheck.hs+1−1

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

3434check ctxt env (Var n)

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

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

3838check ctxt env (RApp f a)

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

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