git.iko.soy/Idris-dev
on master help sign in
Better if unification substitutes rather than let binds
44d62c7Edwin Brady
impl-paper/overview.tex+4
compare with master
unifiedsplit
@@ -19,6 +19,10 @@ High level view of steps we've taken to implement this new version:
19 and de Bruijn indices when done.
19 and de Bruijn indices when done.
20\end{itemize}
20\end{itemize}
21\item Unification, and incorporation into the tactic engine.
21\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}
22\item An Elaborator, as an EDSL, which is a language for applying primitive tactics and
26\item An Elaborator, as an EDSL, which is a language for applying primitive tactics and
23 constructing derived tactics.
27 constructing derived tactics.
24\end{itemize}
28\end{itemize}
src/CoreParser.hs+3−2
@@ -34,7 +34,8 @@ parseDef = parse pDef "(input)"
34parseTerm = parse pTerm "(input)"
34parseTerm = parse pTerm "(input)"
35
35
36pTestFile :: Parser RProgram
36pTestFile :: Parser RProgram
37−pTestFile = many1 pDef
37+pTestFile = do p <- many1 pDef ; eof
38+ return p
38
39
39iName :: Parser Name
40iName :: Parser Name
40iName = identifier >>= (\n -> return (UN [n]))
41iName = identifier >>= (\n -> return (UN [n]))
@@ -47,7 +48,7 @@ pDef = try (do x <- iName; lchar ':'; ty <- pTerm
47 return (x, RFunction (RawFun ty tm)))
48 return (x, RFunction (RawFun ty tm)))
48 <|> do x <- iName; lchar ':'; ty <- pTerm; lchar ';'
49 <|> do x <- iName; lchar ':'; ty <- pTerm; lchar ';'
49 return (x, RConst ty)
50 return (x, RConst ty)
50− <|> do (x, d) <- pData
51+ <|> do (x, d) <- pData; lchar ';'
51 return (x, RData d)
52 return (x, RData d)
52
53
53app :: Parser (Raw -> Raw -> Raw)
54app :: Parser (Raw -> Raw -> Raw)
src/Main.hs+9−7
@@ -7,10 +7,12 @@ import Typecheck
7import ProofShell
7import ProofShell
8
8
9main = do f <- readFile "test.mi"
9main = do f <- readFile "test.mi"
10− let Right defs = parseFile f
10+ case parseFile f of
11+ Left err -> print err
12+ Right defs -> do
11− print defs
13+ print defs
12− case checkProgram [] defs of
14+ case checkProgram [] defs of
13− OK ctxt -> do print ctxt
15+ OK ctxt -> do print ctxt
14− runShell (initState ctxt)
16+ runShell (initState ctxt)
15− return ()
17+ return ()
16− err -> print err
18+ err -> print err
src/ProofState.hs+6−5
@@ -22,6 +22,7 @@ data ProofState = PS { thname :: Name,
22 nextname :: Int, -- name supply
22 nextname :: Int, -- name supply
23 pterm :: Term, -- current proof term
23 pterm :: Term, -- current proof term
24 ptype :: Type, -- original goal
24 ptype :: Type, -- original goal
25+ defer :: [(Name, Type)], -- names we'll need to define
25 previous :: Maybe ProofState, -- for undo
26 previous :: Maybe ProofState, -- for undo
26 context :: Context,
27 context :: Context,
27 done :: Bool
28 done :: Bool
@@ -60,8 +61,8 @@ data TacticAction = AddGoal Name -- add a new goal, solve immediately
60-- Some utilites on proof and tactic states
61-- Some utilites on proof and tactic states
61
62
62instance Show ProofState where
63instance Show ProofState where
63− show (PS nm [] _ tm _ _ _ _) = show nm ++ ": no more goals"
64+ show (PS nm [] _ tm _ _ _ _ _) = show nm ++ ": no more goals"
64− show (PS nm (h:hs) _ tm _ i_ ctxt _)
65+ show (PS nm (h:hs) _ tm _ i _ ctxt _)
65 = let OK g = goal (Just h) tm
66 = let OK g = goal (Just h) tm
66 wkenv = premises g in
67 wkenv = premises g in
67 showPs wkenv (reverse wkenv) ++ "\n" ++
68 showPs wkenv (reverse wkenv) ++ "\n" ++
@@ -103,7 +104,8 @@ action a = do (n, ts) <- get
103newProof :: Name -> Context -> Type -> ProofState
104newProof :: Name -> Context -> Type -> ProofState
104newProof n ctxt ty = let h = holeName 0
105newProof n ctxt ty = let h = holeName 0
105 ty' = vToP ty in
106 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
107
109
108type TState = (Int, [TacticAction])
110type TState = (Int, [TacticAction])
109type RunTactic = Context -> Env -> Term -> StateT TState TC Term
111type RunTactic = Context -> Env -> Term -> StateT TState TC Term
@@ -250,7 +252,6 @@ eval_in t ctxt env tm =
250 showEnv env valty'))
252 showEnv env valty'))
251 return tm
253 return tm
252
254
253−
254processTactic :: Tactic -> ProofState -> TC (ProofState, String)
255processTactic :: Tactic -> ProofState -> TC (ProofState, String)
255processTactic QED ps = case holes ps of
256processTactic QED ps = case holes ps of
256 [] -> let tm = finalise (pterm ps) in
257 [] -> let tm = finalise (pterm ps) in
@@ -291,7 +292,7 @@ processTactic t ps
291 getSolved (_ : xs) = getSolved xs
292 getSolved (_ : xs) = getSolved xs
292
293
293 updateSolved xs (Bind n b@(Hole _) t)
294 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))
295 updateSolved xs (Bind n b t)
296 updateSolved xs (Bind n b t)
296 | otherwise = Bind n (fmap (updateSolved xs) b) (updateSolved xs t)
297 | otherwise = Bind n (fmap (updateSolved xs) b) (updateSolved xs t)
297 updateSolved xs (App f a) = App (updateSolved xs f) (updateSolved xs a)
298 updateSolved xs (App f a) = App (updateSolved xs f) (updateSolved xs a)