>
>
>
>
>
>
>
>
>
>
>
> module Ivor.Construction(auto,split,left,right,useCon,exists,
> isItJust) where
> import Ivor.TT
> import Debug.Trace
>
>
>
>
>
>
>
>
> auto :: Int
> -> Tactic
> 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 (n1))) >|>
> (right >+> (auto (n1)))) g ctxt
>
>
> split :: Tactic
> split = useCon 1 0
>
>
> left :: Tactic
> left = useCon 2 0
>
>
> right :: Tactic
> right = useCon 2 1
Get the goal, look at the type. Refine by the constructor of that type
check that there is the right number (num).
>
> useCon :: Int
> -> Int
> -> Tactic
> useCon num use g ctxt = do
> goal <- goalData ctxt False g
> let ty = getApp (view (goalType goal))
> case ty of
> (Name _ n) -> do cons <- getConstructors ctxt n
> splitnCon cons g ctxt
> _ -> fail "Not a type constructor"
> where splitnCon cs | length cs >= num || num == 0
> = refine (Name DataCon (cs!!use))
> splitnCon _ = \g ctxt -> fail $ "Not a " ++ show num ++ " constructor family"
>
>
>
> exists :: IsTerm a => a
> -> Tactic
> exists t = useCon 1 0 >+> fill t
>
>
> isItJust :: IsTerm a => a -> Tactic
> isItJust tm g ctxt = do
> gd <- goalData ctxt False g
> let gty = view $ goalType gd
> vtm <- evalCtxt ctxt g tm
> let (prf, ty) = (view vtm, viewType vtm)
>
> case ty of
> (App (Name _ m) a) | m == (name "Maybe")
> -> do case prf of
> (App (Name _ n) _) | n == (name "Nothing")
> -> fail "No solution found"
> (App (App (Name _ j) _) p) | j == (name "Just")
> -> fill p g ctxt
> tm -> fail $ "Evaluated to " ++ show tm
> _ -> fail $ "Type of decision procedure must be ++ " ++
> show (App (Name Unknown (name "Maybe")) gty)