git.iko.soy/Idris-dev
on master help sign in
make Elab a state monad for ease of EDSL programming
5ee3376Edwin Brady
src/Elaborate.hs+53−44
compare with master
unifiedsplit
@@ -14,76 +14,85 @@ import ProofState
14import Core
14import Core
15import Evaluate
15import Evaluate
16
16
17+import Control.Monad.State
18+
17-- I don't really want this here, but it's useful for the test shell
19-- I don't really want this here, but it's useful for the test shell
18data Command = Theorem Name Raw
20data Command = Theorem Name Raw
19 | Eval Raw
21 | Eval Raw
20 | Quit
22 | Quit
21 | Print Name
23 | Print Name
22− | Tac Elab
24+ | Tac (Elab ())
25+
26+type Elab a = StateT (ProofState, String) TC a
23
27
24−type Elab = ProofState -> TC (ProofState, String)
28+runElab :: Elab a -> ProofState -> TC (ProofState, String)
29+runElab e ps = execStateT e (ps, "")
25
30
26initElaborator :: Name -> Context -> Type -> ProofState
31initElaborator :: Name -> Context -> Type -> ProofState
27initElaborator = newProof
32initElaborator = newProof
28
33
34+processTactic' t = do (p, logs) <- get
35+ (p', log) <- lift $ processTactic t p
36+ put (p', logs ++ log)
37+ return ()
38+
29-- The primitives, from ProofState
39-- The primitives, from ProofState
30
40
31−attack :: Elab
41+attack :: Elab ()
32−attack = processTactic Attack
42+attack = processTactic' Attack
33
43
34−claim :: Name -> Raw -> Elab
44+claim :: Name -> Raw -> Elab ()
35−claim n t = processTactic (Claim n t)
45+claim n t = processTactic' (Claim n t)
36
46
37−fill :: Raw -> Elab
47+fill :: Raw -> Elab ()
38−fill t = processTactic (Fill t)
48+fill t = processTactic' (Fill t)
39
49
40−unify_fill :: Raw -> Elab
50+unify_fill :: Raw -> Elab ()
41−unify_fill t = processTactic (UnifyFill t)
51+unify_fill t = processTactic' (UnifyFill t)
42
52
43−solve :: Elab
53+solve :: Elab ()
44−solve = processTactic Solve
54+solve = processTactic' Solve
45
55
46−regret :: Elab
56+regret :: Elab ()
47−regret = processTactic Regret
57+regret = processTactic' Regret
48
58
49−compute :: Elab
59+compute :: Elab ()
50−compute = processTactic Compute
60+compute = processTactic' Compute
51
61
52−eval_in :: Raw -> Elab
62+eval_in :: Raw -> Elab ()
53−eval_in t = processTactic (EvalIn t)
63+eval_in t = processTactic' (EvalIn t)
54
64
55−check_in :: Raw -> Elab
65+check_in :: Raw -> Elab ()
56−check_in t = processTactic (CheckIn t)
66+check_in t = processTactic' (CheckIn t)
57
67
58−intro :: Name -> Elab
68+intro :: Name -> Elab ()
59−intro n = processTactic (Intro n)
69+intro n = processTactic' (Intro n)
60
70
61−forall :: Name -> Raw -> Elab
71+forall :: Name -> Raw -> Elab ()
62−forall n t = processTactic (Forall n t)
72+forall n t = processTactic' (Forall n t)
63
73
64−focus :: Name -> Elab
74+focus :: Name -> Elab ()
65−focus n = processTactic (Focus n)
75+focus n = processTactic' (Focus n)
66
76
67−proofstate :: Elab
77+proofstate :: Elab ()
68−proofstate = processTactic ProofState
78+proofstate = processTactic' ProofState
69
79
70−qed :: Elab
80+qed :: Elab ()
71−qed = processTactic QED
81+qed = processTactic' QED
72
82
73-- Some combinators on elaborations
83-- Some combinators on elaborations
74
84
75-- Sequencing
85-- Sequencing
76−infixr 5 ==>
86+-- infixr 5 ==>
77−
87+
78−(==>) :: Elab -> Elab -> Elab
88+-- (==>) :: Elab -> Elab -> Elab
79−(==>) t1 t2 ps = do (ps', log') <- t1 ps
89+-- (==>) t1 t2 ps = do (ps', log') <- t1 ps
80− (ps'', log'') <- t2 ps'
90+-- (ps'', log'') <- t2 ps'
81− return (ps'', log' ++ log')
91+-- return (ps'', log' ++ log')
82−
92+--
83−-- Try a tactic, if it fails, try another
93+-- -- Try a tactic, if it fails, try another
84−try :: Elab -> Elab -> Elab
94+-- try :: Elab -> Elab -> Elab
85−try t1 t2 ps = case t1 ps of
95+-- try t1 t2 ps = case t1 ps of
86− OK v -> return v
96+-- OK v -> return v
87− _ -> t2 ps
97+-- _ -> t2 ps
88−
98+--
89−
src/ProofShell.hs+1−1
@@ -39,7 +39,7 @@ processCommand (Print n) state =
39 Just tm -> (state, show tm)
39 Just tm -> (state, show tm)
40 Nothing -> (state, "No such name")
40 Nothing -> (state, "No such name")
41processCommand (Tac e) state
41processCommand (Tac e) state
42− | Just ps <- prf state = case e ps of
42+ | Just ps <- prf state = case runElab e ps of
43 OK (ps', resp) ->
43 OK (ps', resp) ->
44 if (not (done ps'))
44 if (not (done ps'))
45 then (state { prf = Just ps' }, resp)
45 then (state { prf = Just ps' }, resp)
src/ShellParser.hs+1−1
@@ -43,7 +43,7 @@ pCommand = do reserved "theorem"; n <- iName; lchar ':'; ty <- pTerm
43 <|> do reserved "quit";
43 <|> do reserved "quit";
44 return Quit
44 return Quit
45
45
46−pTactic :: Parser Elab
46+pTactic :: Parser (Elab ())
47pTactic = do reserved "attack"; return attack
47pTactic = do reserved "attack"; return attack
48 <|> do reserved "claim"; n <- iName; lchar ':'; ty <- pTerm
48 <|> do reserved "claim"; n <- iName; lchar ':'; ty <- pTerm
49 return (claim n ty)
49 return (claim n ty)