Permalink
Browse files

Better 'trivial' tactic (tries refine and fill) and began auto implem…

…entation

darcs-hash:20061107135413-974a0-0c9c7e9bf05ba2613e3128e6d348f4374cd0408e.gz
  • Loading branch information...
1 parent 775ec26 commit 0b8a640cf3c234b22ec1508ffda34100a2260a86 eb committed Nov 7, 2006
Showing with 23 additions and 10 deletions.
  1. +10 −2 Ivor/Decisions.lhs
  2. +1 −0 Ivor/Shell.lhs
  3. +2 −1 Ivor/ShellParser.lhs
  4. +3 −2 Ivor/TT.lhs
  5. +7 −5 examplett/logic.tt
View
@@ -14,6 +14,7 @@
> module Ivor.Decisions(auto,split,left,right,useCon) where
> import Ivor.TT
+> import Debug.Trace
> -- | Tries to solve a simple goal automatically by trying each of these
> -- in turn:
@@ -24,7 +25,14 @@
> -- on each constructor in turn.
> auto :: Int -- ^ Search depth
> -> Tactic
-> auto _ = fail "auto undefined"
+> auto 0 = \g ctxt -> fail "auto got bored, try a bigger search depth"
+> auto n = \g ctxt -> if (allSolved ctxt) then return ctxt else
+> trace ("Auto "++ show n) $
+> ((trivial >+> (auto n)) >|>
+> (intros1 >+> (auto n)) >|>
+> (split >+> (auto n)) >|>
+> (left >+> (auto (n-1))) >|>
+> (right >+> (auto (n-1)))) g ctxt
> -- | Split a goal into subgoals. Type of goal must be a one constructor
> -- family, with constructor @c@, then proceeds by 'refine' @c@.
@@ -57,5 +65,5 @@ check that there is the right number (num).
> _ -> fail "Not a type constructor"
> where splitnCon cs | length cs >= num || num == 0
> = refine (Name DataCon (cs!!use))
-> splitnCon _ = fail $ "Not a " ++ show num ++ " constructor family"
+> splitnCon _ = \g ctxt -> fail $ "Not a " ++ show num ++ " constructor family"
View
@@ -216,6 +216,7 @@
> runTactic _ _ Split = split
> runTactic _ _ LeftCon = left
> runTactic _ _ RightCon = right
+> runTactic _ _ AutoSolve = auto 20
> runTactic _ _ (By tm) = by tm
> runTactic _ _ (Induction tm) = induction tm
> runTactic _ _ (Cases tm) = cases tm
View
@@ -88,7 +88,7 @@
> | Normalise
> | Unfold String
> | Trivial
-> | Split | LeftCon | RightCon
+> | Split | LeftCon | RightCon | AutoSolve
> | By ViewTerm
> | Induction ViewTerm
> | Cases ViewTerm
@@ -322,6 +322,7 @@ which runs it.
> <|> do reserved "split" ; semi ; return Split
> <|> do reserved "left" ; semi ; return LeftCon
> <|> do reserved "right" ; semi ; return RightCon
+> <|> do reserved "auto" ; semi ; return AutoSolve
> <|> do reserved "by" ; tm <- pTerm ext ; semi ;
> return $ By tm
> <|> do reserved "induction" ; tm <- pTerm ext ; semi ;
View
@@ -40,7 +40,7 @@
> -- ** Basics
> intro,
> introName,
-> intros,
+> intros,intros1,
> introsNames,
> Ivor.TT.addArg,
> generalise,
@@ -1177,7 +1177,8 @@ FIXME: Choose a sensible name here
> tryall ps g ctxt
> where tryall [] g ctxt = fail "No trivial solution found"
> tryall ((x,ty):xs) g ctxt
-> = do ctxt' <- try (refine (Name Free x)) idTac idTac g ctxt
+> = do ctxt' <- ((refine (Name Free x)) >|> (fill (Name Free x))
+> >|> idTac) g ctxt
> if (numUnsolved ctxt' < numUnsolved ctxt)
> then return ctxt'
> else tryall xs g ctxt
View
@@ -21,8 +21,8 @@ intros;
induction p;
intros;
split;
-fill b;
-fill a;
+trivial;
+trivial;
Qed;
Freeze and_commutes;
@@ -31,10 +31,10 @@ intros;
induction p;
intros;
right;
-fill a;
+trivial;
intros;
left;
-fill b;
+trivial;
Qed;
Freeze or_commutes;
@@ -48,5 +48,7 @@ refine X0;
trivial;
intros;
left;
-fill b;
+trivial;
Qed;
+
+

0 comments on commit 0b8a640

Please sign in to comment.