@@ -14,76 +14,85 @@ import ProofState
1414import Core
1515import Evaluate
1616
17+import Control.Monad.State
18+
1719-- I don't really want this here, but it's useful for the test shell
1820data Command = Theorem Name Raw
1921 | Eval Raw
2022 | Quit
2123 | Print Name
22− | Tac Elab
24+ | Tac (Elab ())
25+
26+type Elab a = StateT (ProofState, String) TC a
2327
24−type Elab = ProofState -> TC (ProofState, String)
28+runElab :: Elab a -> ProofState -> TC (ProofState, String)
29+runElab e ps = execStateT e (ps, "")
2530
2631initElaborator :: Name -> Context -> Type -> ProofState
2732initElaborator = newProof
2833
34+processTactic' t = do (p, logs) <- get
35+ (p', log) <- lift $ processTactic t p
36+ put (p', logs ++ log)
37+ return ()
38+
2939-- The primitives, from ProofState
3040
31−attack :: Elab
32−attack = processTactic Attack
41+attack :: Elab ()
42+attack = processTactic' Attack
3343
34−claim :: Name -> Raw -> Elab
35−claim n t = processTactic (Claim n t)
44+claim :: Name -> Raw -> Elab ()
45+claim n t = processTactic' (Claim n t)
3646
37−fill :: Raw -> Elab
38−fill t = processTactic (Fill t)
47+fill :: Raw -> Elab ()
48+fill t = processTactic' (Fill t)
3949
40−unify_fill :: Raw -> Elab
41−unify_fill t = processTactic (UnifyFill t)
50+unify_fill :: Raw -> Elab ()
51+unify_fill t = processTactic' (UnifyFill t)
4252
43−solve :: Elab
44−solve = processTactic Solve
53+solve :: Elab ()
54+solve = processTactic' Solve
4555
46−regret :: Elab
47−regret = processTactic Regret
56+regret :: Elab ()
57+regret = processTactic' Regret
4858
49−compute :: Elab
50−compute = processTactic Compute
59+compute :: Elab ()
60+compute = processTactic' Compute
5161
52−eval_in :: Raw -> Elab
53−eval_in t = processTactic (EvalIn t)
62+eval_in :: Raw -> Elab ()
63+eval_in t = processTactic' (EvalIn t)
5464
55−check_in :: Raw -> Elab
56−check_in t = processTactic (CheckIn t)
65+check_in :: Raw -> Elab ()
66+check_in t = processTactic' (CheckIn t)
5767
58−intro :: Name -> Elab
59−intro n = processTactic (Intro n)
68+intro :: Name -> Elab ()
69+intro n = processTactic' (Intro n)
6070
61−forall :: Name -> Raw -> Elab
62−forall n t = processTactic (Forall n t)
71+forall :: Name -> Raw -> Elab ()
72+forall n t = processTactic' (Forall n t)
6373
64−focus :: Name -> Elab
65−focus n = processTactic (Focus n)
74+focus :: Name -> Elab ()
75+focus n = processTactic' (Focus n)
6676
67−proofstate :: Elab
68−proofstate = processTactic ProofState
77+proofstate :: Elab ()
78+proofstate = processTactic' ProofState
6979
70−qed :: Elab
71−qed = processTactic QED
80+qed :: Elab ()
81+qed = processTactic' QED
7282
7383-- Some combinators on elaborations
7484
7585-- Sequencing
76−infixr 5 ==>
77−
78−(==>) :: Elab -> Elab -> Elab
79−(==>) t1 t2 ps = do (ps', log') <- t1 ps
80− (ps'', log'') <- t2 ps'
81− return (ps'', log' ++ log')
82−
83−-- Try a tactic, if it fails, try another
84−try :: Elab -> Elab -> Elab
85−try t1 t2 ps = case t1 ps of
86− OK v -> return v
87− _ -> t2 ps
88−
89−
86+-- infixr 5 ==>
87+
88+-- (==>) :: Elab -> Elab -> Elab
89+-- (==>) t1 t2 ps = do (ps', log') <- t1 ps
90+-- (ps'', log'') <- t2 ps'
91+-- return (ps'', log' ++ log')
92+--
93+-- -- Try a tactic, if it fails, try another
94+-- try :: Elab -> Elab -> Elab
95+-- try t1 t2 ps = case t1 ps of
96+-- OK v -> return v
97+-- _ -> t2 ps
98+--