44d62c7 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Better if unification substitutes rather than let binds

commit44d62c7ec0938aa8a7b16f002fb0198d1fc31694 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateWed 28 Sep 2011, 22:20 (15 years ago) parent89ffe9b

4 files changed+22−14

compare with master

unifiedsplit

impl-paper/overview.tex+4 src/CoreParser.hs+3−2 src/Main.hs+9−7 src/ProofState.hs+6−5

impl-paper/overview.tex+4

@@ -19,6 +19,10 @@ High level view of steps we've taken to implement this new version:

1919 and de Bruijn indices when done.

2020\end{itemize}

2121\item Unification, and incorporation into the tactic engine.

22+\begin{itemize}

23+ \item Note that this can introduce constraints on hole ordering. If we can't satisfy them,

24+ report an error.

25+\end{itemize}

2226\item An Elaborator, as an EDSL, which is a language for applying primitive tactics and

2327 constructing derived tactics.

2428\end{itemize}

src/CoreParser.hs+3−2

@@ -34,7 +34,8 @@ parseDef = parse pDef "(input)"

3434parseTerm = parse pTerm "(input)"

3535

3636pTestFile :: Parser RProgram

37−pTestFile = many1 pDef

37+pTestFile = do p <- many1 pDef ; eof

38+ return p

3839

3940iName :: Parser Name

4041iName = identifier >>= (\n -> return (UN [n]))

@@ -47,7 +48,7 @@ pDef = try (do x <- iName; lchar ':'; ty <- pTerm

4748 return (x, RFunction (RawFun ty tm)))

4849 <|> do x <- iName; lchar ':'; ty <- pTerm; lchar ';'

4950 return (x, RConst ty)

50− <|> do (x, d) <- pData

51+ <|> do (x, d) <- pData; lchar ';'

5152 return (x, RData d)

5253

5354app :: Parser (Raw -> Raw -> Raw)

src/Main.hs+9−7

@@ -7,10 +7,12 @@ import Typecheck

77import ProofShell

99main = do f <- readFile "test.mi"

10− let Right defs = parseFile f

11− print defs

12− case checkProgram [] defs of

13− OK ctxt -> do print ctxt

14− runShell (initState ctxt)

15− return ()

16− err -> print err

10+ case parseFile f of

11+ Left err -> print err

12+ Right defs -> do

13+ print defs

14+ case checkProgram [] defs of

15+ OK ctxt -> do print ctxt

16+ runShell (initState ctxt)

17+ return ()

18+ err -> print err

src/ProofState.hs+6−5

@@ -22,6 +22,7 @@ data ProofState = PS { thname :: Name,

2222 nextname :: Int, -- name supply

2323 pterm :: Term, -- current proof term

2424 ptype :: Type, -- original goal

25+ defer :: [(Name, Type)], -- names we'll need to define

2526 previous :: Maybe ProofState, -- for undo

2627 context :: Context,

2728 done :: Bool

@@ -60,8 +61,8 @@ data TacticAction = AddGoal Name -- add a new goal, solve immediately

6061-- Some utilites on proof and tactic states

6162

6263instance Show ProofState where

63− show (PS nm [] _ tm _ _ _ _) = show nm ++ ": no more goals"

64− show (PS nm (h:hs) _ tm _ i_ ctxt _)

64+ show (PS nm [] _ tm _ _ _ _ _) = show nm ++ ": no more goals"

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

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

6667 wkenv = premises g in

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

@@ -103,7 +104,8 @@ action a = do (n, ts) <- get

103104newProof :: Name -> Context -> Type -> ProofState

104105newProof n ctxt ty = let h = holeName 0

105106 ty' = vToP ty in

106− PS n [h] 1 (Bind h (Hole ty') (P Bound h ty')) ty Nothing ctxt False

107+ PS n [h] 1 (Bind h (Hole ty') (P Bound h ty')) ty []

108+ Nothing ctxt False

107109

108110type TState = (Int, [TacticAction])

109111type RunTactic = Context -> Env -> Term -> StateT TState TC Term

@@ -250,7 +252,6 @@ eval_in t ctxt env tm =

250252 showEnv env valty'))

251253 return tm

252254

253−

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

255256processTactic QED ps = case holes ps of

256257 [] -> let tm = finalise (pterm ps) in

@@ -291,7 +292,7 @@ processTactic t ps

291292 getSolved (_ : xs) = getSolved xs

292293

293294 updateSolved xs (Bind n b@(Hole _) t)

294− | Just v <- lookup n xs = Bind n (Let (binderTy b) v) (updateSolved xs t)

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

295296 updateSolved xs (Bind n b t)

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

297298 updateSolved xs (App f a) = App (updateSolved xs f) (updateSolved xs a)