text:
{-# LANGUAGE PatternGuards #-}

module Idris.ElabTerm where

import Idris.AbsSyntax
import Idris.DSL
import Idris.Delaborate

import Core.Elaborate hiding (Tactic(..))
import Core.TT
import Core.Evaluate

import Control.Monad
import Control.Monad.State
import Data.List

import Debug.Trace

-- Data to pass to recursively called elaborators; e.g. for where blocks,
-- paramaterised declarations, etc.

data ElabInfo = EInfo { params :: [(Name, PTerm)],
                        inblock :: Ctxt [Name], -- names in the block, and their params
                        liftname :: Name -> Name,
                        namespace :: Maybe [String] }

toplevel = EInfo [] emptyContext id Nothing

type ElabD a = Elab' [PDecl] a

-- Using the elaborator, convert a term in raw syntax to a fully
-- elaborated, typechecked term.
--
-- If building a pattern match, we convert undeclared variables from
-- holes to pattern bindings.

-- Also find deferred names in the term and their types

build :: IState -> ElabInfo -> Bool -> Name -> PTerm ->
         ElabD (Term, [(Name, Type)], [PDecl])
build ist info pattern fn tm
    = do elab ist info pattern False fn tm
         ivs <- get_instances
         hs <- get_holes
         ptm <- get_term
         -- Resolve remaining type classes. Two passes - first to get the
         -- default Num instances, second to clean up the rest
         when (not pattern) $
              mapM_ (\n -> when (n `elem` hs) $
                             do focus n
                                try (resolveTC 7 fn ist)
                                    (movelast n)) ivs
         ivs <- get_instances
         hs <- get_holes
         when (not pattern) $
              mapM_ (\n -> when (n `elem` hs) $
                             do focus n
                                resolveTC 7 fn ist) ivs
         probs <- get_probs
         tm <- get_term
         ctxt <- get_context
         case probs of
            [] -> return ()
            ((_,_,_,e):es) -> lift (Error e)
         is <- getAux
         tt <- get_term
         let (tm, ds) = runState (collectDeferred tt) []
         log <- getLog
         if (log /= "") then trace log $ return (tm, ds, is)
            else return (tm, ds, is)

-- Build a term autogenerated as a typeclass method definition
-- (Separate, so we don't go overboard resolving things that we don't
-- know about yet on the LHS of a pattern def)

buildTC :: IState -> ElabInfo -> Bool -> Bool -> Name -> PTerm ->
         ElabD (Term, [(Name, Type)], [PDecl])
buildTC ist info pattern tcgen fn tm
    = do elab ist info pattern tcgen fn tm
         probs <- get_probs
         tm <- get_term
         case probs of
            [] -> return ()
            ((_,_,_,e):es) -> lift (Error e)
         is <- getAux
         tt <- get_term
         let (tm, ds) = runState (collectDeferred tt) []
         log <- getLog
         if (log /= "") then trace log $ return (tm, ds, is)
            else return (tm, ds, is)

-- Returns the set of declarations we need to add to complete the definition
-- (most likely case blocks to elaborate)

elab :: IState -> ElabInfo -> Bool -> Bool -> Name -> PTerm ->
        ElabD ()
elab ist info pattern tcgen fn tm
    = do elabE (False, False) tm -- (in argument, guarded)
         end_unify
         when pattern -- convert remaining holes to pattern vars
              (do update_term orderPats
                  tm <- get_term
                  mkPat)
  where
    isph arg = case getTm arg of
        Placeholder -> (True, priority arg)
        _ -> (False, priority arg)

    toElab ina arg = case getTm arg of
        Placeholder -> Nothing
        v -> Just (priority arg, elabE ina v)

    toElab' ina arg = case getTm arg of
        Placeholder -> Nothing
        v -> Just (elabE ina v)

    mkPat = do hs <- get_holes
               tm <- get_term
               case hs of
                  (h: hs) -> do patvar h; mkPat
                  [] -> return ()

    elabE ina t = {- do g <- goal
                 tm <- get_term
                 trace ("Elaborating " ++ show t ++ " : " ++ show g ++ "\n\tin " ++ show tm)
                    $ -}
                  do t' <- insertCoerce ina t
                     g <- goal
                     tm <- get_term
                     ps <- get_probs
                     hs <- get_holes
--                      trace ("Elaborating " ++ show t' ++ " in " ++ show g
-- --                             ++ "\n" ++ show tm
--                             ++ "\nholes " ++ show hs
--                             ++ "\nproblems " ++ show ps
--                             ++ "\n-----------\n") $
                     elab' ina t'

    local f = do e <- get_env
                 return (f `elem` map fst e)

    elab' ina PType           = do apply RType []; solve
    elab' ina (PConstant c)  = do apply (RConstant c) []; solve
    elab' ina (PQuote r)     = do fill r; solve
    elab' ina (PTrue fc)     = try (elab' ina (PRef fc unitCon))
                                   (elab' ina (PRef fc unitTy))
    elab' ina (PFalse fc)    = elab' ina (PRef fc falseTy)
    elab' ina (PResolveTC (FC "HACK" _)) -- for chasing parent classes
       = resolveTC 5 fn ist
    elab' ina (PResolveTC fc)
        | True = do c <- unique_hole (MN 0 "class")
                    instanceArg c
        | otherwise = do g <- goal
                         try (resolveTC 2 fn ist)
                          (do c <- unique_hole (MN 0 "class")
                              instanceArg c)
    elab' ina (PRefl fc t)   = elab' ina (PApp fc (PRef fc eqCon) [pimp (MN 0 "a") Placeholder,
                                                           pimp (MN 0 "x") t])
    elab' ina (PEq fc l r)   = elab' ina (PApp fc (PRef fc eqTy) [pimp (MN 0 "a") Placeholder,
                                                          pimp (MN 0 "b") Placeholder,
                                                          pexp l, pexp r])
    elab' ina@(_, a) (PPair fc l r)
        = do hnf_compute
             g <- goal
             case g of
                TType _ -> elabE (True, a) (PApp fc (PRef fc pairTy)
                                            [pexp l,pexp r])
                _ -> elabE (True, a) (PApp fc (PRef fc pairCon)
                                            [pimp (MN 0 "A") Placeholder,
                                             pimp (MN 0 "B") Placeholder,
                                             pexp l, pexp r])
    elab' ina (PDPair fc l@(PRef _ n) t r)
            = case t of
                Placeholder ->
                   do hnf_compute
                      g <- goal
                      case g of
                         TType _ -> asType
                         _ -> asValue
                _ -> asType
         where asType = elab' ina (PApp fc (PRef fc sigmaTy)
                                        [pexp t,
                                         pexp (PLam n Placeholder r)])
               asValue = elab' ina (PApp fc (PRef fc existsCon)
                                         [pimp (MN 0 "a") t,
                                          pimp (MN 0 "P") Placeholder,
                                          pexp l, pexp r])
    elab' ina (PDPair fc l t r) = elab' ina (PApp fc (PRef fc existsCon)
                                            [pimp (MN 0 "a") t,
                                             pimp (MN 0 "P") Placeholder,
                                             pexp l, pexp r])
    elab' ina (PAlternative True as)
        = do hnf_compute
             ty <- goal
             ctxt <- get_context
             let (tc, _) = unApply ty
             let as' = pruneByType tc ctxt as
--              case as' of
--                 [a] -> elab' ina a
--                 as -> lift $ tfail $ CantResolveAlts (map showHd as)
             tryAll (zip (map (elab' ina) as') (map showHd as'))
        where showHd (PApp _ h _) = show h
              showHd x = show x
    elab' ina (PAlternative False as)
        = trySeq as
        where -- if none work, take the error from the first
              trySeq (x : xs) = let e1 = elab' ina x in
                                    try' e1 (trySeq' e1 xs) True
              trySeq' deferr [] = proofFail deferr
              trySeq' deferr (x : xs)
                  = try' (elab' ina x) (trySeq' deferr xs) True
    elab' ina (PPatvar fc n) | pattern = patvar n
    elab' (ina, guarded) (PRef fc n) | pattern && not (inparamBlock n)
        = do ctxt <- get_context
             let defined = case lookupTy n ctxt of
                               [] -> False
                               _ -> True
           -- this is to stop us resolve type classes recursively
             -- trace (show (n, guarded)) $
             if (tcname n && ina) then erun fc $ patvar n
               else if (defined && not guarded)
                       then do apply (Var n) []; solve
                       else try (do apply (Var n) []; solve)
                                (patvar n)
      where inparamBlock n = case lookupCtxtName n (inblock info) of
                                [] -> False
                                _ -> True
    elab' ina f@(PInferRef fc n) = elab' ina (PApp fc f [])
    elab' ina (PRef fc n) = erun fc $ do apply (Var n) []; solve
    elab' ina@(_, a) (PLam n Placeholder sc)
          = do -- n' <- unique_hole n
               -- let sc' = mapPT (repN n n') sc
               ptm <- get_term
               g <- goal
               checkPiGoal
               attack; intro (Just n);
               -- trace ("------ intro " ++ show n ++ " ---- \n" ++ show ptm)
               elabE (True, a) sc; solve
       where repN n n' (PRef fc x) | x == n' = PRef fc n'
             repN _ _ t = t
    elab' ina@(_, a) (PLam n ty sc)
          = do hsin <- get_holes
               ptmin <- get_term
               tyn <- unique_hole (MN 0 "lamty")
               checkPiGoal
               claim tyn RType
               attack
               ptm <- get_term
               hs <- get_holes
               -- trace ("BEFORE:\n" ++ show hsin ++ "\n" ++ show ptmin ++
               --       "\nNOW:\n" ++ show hs ++ "\n" ++ show ptm) $
               introTy (Var tyn) (Just n)
               -- end_unify
               focus tyn
               ptm <- get_term
               hs <- get_holes
               elabE (True, a) ty
               elabE (True, a) sc
               solve
    elab' ina@(_,a) (PPi _ n Placeholder sc)
          = do attack; arg n (MN 0 "ty"); elabE (True, a) sc; solve
    elab' ina@(_,a) (PPi _ n ty sc)
          = do attack; tyn <- unique_hole (MN 0 "ty")
               claim tyn RType
               n' <- case n of
                        MN _ _ -> unique_hole n
                        _ -> return n
               forall n' (Var tyn)
               focus tyn
               elabE (True, a) ty
               elabE (True, a) sc
               solve
    elab' ina@(_,a) (PLet n ty val sc)
          = do attack;
               tyn <- unique_hole (MN 0 "letty")
               claim tyn RType
               valn <- unique_hole (MN 0 "letval")
               claim valn (Var tyn)
               letbind n (Var tyn) (Var valn)
               case ty of
                   Placeholder -> return ()
                   _ -> do focus tyn
                           elabE (True, a) ty
               focus valn
               elabE (True, a) val
               elabE (True, a) sc
               ptm <- get_term
               solve
    elab' ina tm@(PApp fc (PInferRef _ f) args) = do
         rty <- goal
         ds <- get_deferred
         ctxt <- get_context
         -- make a function type a -> b -> c -> ... -> rty for the
         -- new function name
         env <- get_env
         argTys <- claimArgTys env args
         fn <- unique_hole (MN 0 "inf_fn")
         let fty = fnTy argTys rty
--             trace (show (ptm, map fst argTys)) $ focus fn
            -- build and defer the function application
         attack; deferType (mkN f) fty (map fst argTys); solve
         -- elaborate the arguments, to unify their types. They all have to
         -- be explicit.
         mapM_ elabIArg (zip argTys args)
       where claimArgTys env [] = return []
             claimArgTys env (arg : xs) | Just n <- localVar env (getTm arg)
                                  = do nty <- get_type (Var n)
                                       ans <- claimArgTys env xs
                                       return ((n, (False, forget nty)) : ans)
             claimArgTys env (_ : xs)
                                  = do an <- unique_hole (MN 0 "inf_argTy")
                                       aval <- unique_hole (MN 0 "inf_arg")
                                       claim an RType
                                       claim aval (Var an)
                                       ans <- claimArgTys env xs
                                       return ((aval, (True, (Var an))) : ans)
             fnTy [] ret  = forget ret
             fnTy ((x, (_, xt)) : xs) ret = RBind x (Pi xt) (fnTy xs ret)

             localVar env (PRef _ x)
                           = case lookup x env of
                                  Just _ -> Just x
                                  _ -> Nothing
             localVar env _ = Nothing

             elabIArg ((n, (True, ty)), def) = do focus n; elabE ina (getTm def)
             elabIArg _ = return () -- already done, just a name

             mkN n@(NS _ _) = n
             mkN n = case namespace info of
                        Just xs@(_:_) -> NS n xs
                        _ -> n

    -- if f is local, just do a simple_app
    elab' (ina, g) tm@(PApp fc (PRef _ f) args')
       = do let args = {- case lookupCtxt f (inblock info) of
                          Just ps -> (map (pexp . (PRef fc)) ps ++ args')
                          _ -> -} args'
--             newtm <- mkSpecialised ist fc f (map getTm args') tm
            env <- get_env
            if (f `elem` map fst env && length args' == 1)
               then -- simple app, as below
                    do simple_app (elabE (ina, g) (PRef fc f))
                                  (elabE (True, g) (getTm (head args')))
                       solve
               else
                 do ivs <- get_instances
                    ps <- get_probs
                    -- HACK: we shouldn't resolve type classes if we're defining an instance
                    -- function or default definition.
                    let isinf = f == inferCon || tcname f
                    -- if f is a type class, we need to know its arguments so that
                    -- we can unify with them
                    case lookupCtxt f (idris_classes ist) of
                        [] -> return ()
                        _ -> mapM_ setInjective (map getTm args')
                    ctxt <- get_context
                    let guarded = isConName f ctxt
                    ns <- apply (Var f) (map isph args)
                    ptm <- get_term
                    g <- goal
                    let (ns', eargs) = unzip $
                             sortBy (\(_,x) (_,y) ->
                                            compare (priority x) (priority y))
                                    (zip ns args)
                    elabArgs (ina || not isinf, guarded)
                           [] fc False ns' (map (\x -> (lazyarg x, getTm x)) eargs)
                    mkSpecialised ist fc f (map getTm args') tm
                    solve
                    ptm <- get_term
                    ivs' <- get_instances
                    ps' <- get_probs
            -- Attempt to resolve any type classes which have 'complete' types,
            -- i.e. no holes in them
                    when (not pattern || (ina && not tcgen && not guarded)) $
                        mapM_ (\n -> do focus n
                                        g <- goal
                                        env <- get_env
                                        hs <- get_holes
                                        if all (\n -> not (n `elem` hs)) (freeNames g)
                                        -- let insts = filter tcname $ map fst (ctxtAlist (tt_ctxt ist))
                                         then try (resolveTC 7 fn ist)
                                                  (movelast n)
                                         else movelast n)
                              (ivs' \\ ivs)
      where tcArg (n, PConstraint _ _ Placeholder _) = True
            tcArg _ = False

            tacTm (PTactics _) = True
            tacTm (PProof _) = True
            tacTm _ = False

            setInjective (PRef _ n) = setinj n
            setInjective (PApp _ (PRef _ n) _) = setinj n
            setInjective _ = return ()

    elab' ina@(_, a) (PApp fc f [arg])
          = erun fc $
             do simple_app (elabE ina f) (elabE (True, a) (getTm arg))
                solve
    elab' ina Placeholder = do (h : hs) <- get_holes
                               movelast h
    elab' ina (PMetavar n) = let n' = mkN n in
                                 do attack; defer n'; solve
        where mkN n@(NS _ _) = n
              mkN n = case namespace info of
                        Just xs@(_:_) -> NS n xs
                        _ -> n
    elab' ina (PProof ts) = do compute; mapM_ (runTac True ist) ts
    elab' ina (PTactics ts)
        | not pattern = do mapM_ (runTac False ist) ts
        | otherwise = elab' ina Placeholder
    elab' ina (PElabError e) = fail (pshow ist e)
    elab' ina (PRewrite fc r sc)
        = do attack
             tyn <- unique_hole (MN 0 "rty")
             claim tyn RType
             valn <- unique_hole (MN 0 "rval")
             claim valn (Var tyn)
             letn <- unique_hole (MN 0 "rewrite_rule")
             letbind letn (Var tyn) (Var valn)
             focus valn
             elab' ina r
             compute
             g <- goal
             rewrite (Var letn)
             g' <- goal
             when (g == g') $ lift $ tfail (NoRewriting g)
             elab' ina sc
             solve
    elab' ina@(_, a) c@(PCase fc scr opts)
        = do attack
             tyn <- unique_hole (MN 0 "scty")
             claim tyn RType
             valn <- unique_hole (MN 0 "scval")
             scvn <- unique_hole (MN 0 "scvar")
             claim valn (Var tyn)
             letbind scvn (Var tyn) (Var valn)
             focus valn
             elabE (True, a) scr
             args <- get_env
             cname <- unique_hole' True (mkCaseName fn)
             let cname' = mkN cname
             elab' ina (PMetavar cname')
             let newdef = PClauses fc [] cname'
                             (caseBlock fc cname' (reverse args) opts)
             -- fail $ "Not implemented " ++ show c ++ "\n" ++ show args
             -- elaborate case
             updateAux (newdef : )
             -- if we haven't got the type yet, hopefully we'll get it later!
             movelast tyn
             solve
        where mkCaseName (NS n ns) = NS (mkCaseName n) ns
              mkCaseName (UN x) = UN (x ++ "_case")
              mkCaseName (MN i x) = MN i (x ++ "_case")
              mkN n@(NS _ _) = n
              mkN n = case namespace info of
                        Just xs@(_:_) -> NS n xs
                        _ -> n
    elab' ina x = fail $ "Something's gone wrong. Did you miss a semi-colon somewhere?"

    caseBlock :: FC -> Name -> [(Name, Binder Term)] ->
                               [(PTerm, PTerm)] -> [PClause]
    caseBlock fc n env opts
        = let args = map mkarg (map fst (init env)) in
              map (mkClause args) opts
       where -- mkarg (MN _ _) = Placeholder
             mkarg n = PRef fc n
             -- may be shadowed names in the new pattern - so replace the
             -- old ones with an _
             mkClause args (l, r)
                   = let args' = map (shadowed (allNamesIn l)) args
                         lhs = PApp fc (PRef fc n)
                                 (map pexp args' ++ [pexp l]) in
                         PClause fc n lhs [] r []

             shadowed new (PRef _ n) | n `elem` new = Placeholder
             shadowed new t = t

    insertCoerce ina t =
        do ty <- goal
           -- Check for possible coercions to get to the goal
           -- and add them as 'alternatives'
           env <- get_env
           let ty' = normalise (tt_ctxt ist) env ty
           let cs = getCoercionsTo ist ty'
           let t' = case (t, cs) of
                         (PCoerced tm, _) -> tm
                         (_, []) -> t
                         (_, cs) -> PAlternative False [t ,
                                       PAlternative True (map (mkCoerce t) cs)]
           return t'
       where
         mkCoerce t n = let fc = FC "Coercion" 0 in -- line never appears!
                            addImpl ist (PApp fc (PRef fc n) [pexp (PCoerced t)])

    elabArgs ina failed fc retry [] _
--         | retry = let (ns, ts) = unzip (reverse failed) in
--                       elabArgs ina [] False ns ts
        | otherwise = return ()
    elabArgs ina failed fc r (n:ns) ((_, Placeholder) : args)
        = elabArgs ina failed fc r ns args
    elabArgs ina failed fc r (n:ns) ((lazy, t) : args)
        | lazy && not pattern
          = do elabArg n (PApp bi (PRef bi (UN "lazy"))
                               [pimp (UN "a") Placeholder,
                                pexp t]);
        | otherwise = elabArg n t
      where elabArg n t
                = do hs <- get_holes
                     tm <- get_term
                     failed' <- -- trace (show (n, t, hs, tm)) $
                                -- traceWhen (not (null cs)) (show ty ++ "\n" ++ showImp True t) $
                                case n `elem` hs of
                                   True ->
--                                       if r
--                                          then try (do focus n; elabE ina t; return failed)
--                                                   (return ((n,(lazy, t)):failed))
                                         do focus n; elabE ina t; return failed
                                   False -> return failed
                     elabArgs ina failed fc r ns args

-- For every alternative, look at the function at the head. Automatically resolve
-- any nested alternatives where that function is also at the head

pruneAlt :: [PTerm] -> [PTerm]
pruneAlt xs = map prune xs
  where
    prune (PApp fc1 (PRef fc2 f) as)
        = PApp fc1 (PRef fc2 f) (fmap (fmap (choose f)) as)
    prune t = t

    choose f (PAlternative a as)
        = let as' = fmap (choose f) as
              fs = filter (headIs f) as' in
              case fs of
                 [a] -> a
                 _ -> PAlternative a as'
    choose f (PApp fc f' as) = PApp fc (choose f f') (fmap (fmap (choose f)) as)
    choose f t = t

    headIs f (PApp _ (PRef _ f') _) = f == f'
    headIs f (PApp _ f' _) = headIs f f'
    headIs f _ = True -- keep if it's not an application

-- Rule out alternatives that don't return the same type as the head of the goal
-- (If there are none left as a result, do nothing)
pruneByType :: Term -> Context -> [PTerm] -> [PTerm]
pruneByType (P _ n _) c as
-- if the goal type is polymorphic, keep e
   | [] <- lookupTy n c = as
   | otherwise
       = let asV = filter (headIs True n) as
             as' = filter (headIs False n) as in
             case as' of
               [] -> case asV of
                        [] -> as
                        _ -> asV
               _ -> as'
  where
    headIs var f (PApp _ (PRef _ f') _) = typeHead var f f'
    headIs var f (PApp _ f' _) = headIs var f f'
    headIs var f (PPi _ _ _ sc) = headIs var f sc
    headIs _ _ _ = True -- keep if it's not an application

    typeHead var f f'
        = case lookupTy f' c of
                       [ty] -> let ty' = normalise c [] ty in
                                   case unApply (getRetTy ty') of
                                    (P _ ftyn _, _) -> ftyn == f
                                    (V _, _) -> var -- keep, variable
                                    _ -> False
                       _ -> False

pruneByType t _ as = as

trivial :: IState -> ElabD ()
trivial ist = try' (do elab ist toplevel False False (MN 0 "tac")
                                    (PRefl (FC "prf" 0) Placeholder)
                       return ())
                   (do env <- get_env
                       g <- goal
                       tryAll env
                       return ()) True
      where
        tryAll []     = fail "No trivial solution"
        tryAll ((x, b):xs)
           = do -- if type of x has any holes in it, move on
                hs <- get_holes
                g <- goal
                if all (\n -> not (n `elem` hs)) (freeNames (binderTy b))
                   then try' (elab ist toplevel False False
                                    (MN 0 "tac") (PRef (FC "prf" 0) x))
                             (tryAll xs) True
                   else tryAll xs

findInstances :: IState -> Term -> [Name]
findInstances ist t
    | (P _ n _, _) <- unApply t
        = case lookupCtxt n (idris_classes ist) of
            [CI _ _ _ _ ins] -> ins
            _ -> []
    | otherwise = []

resolveTC :: Int -> Name -> IState -> ElabD ()
resolveTC 0 fn ist = fail $ "Can't resolve type class"
resolveTC 1 fn ist = try' (trivial ist) (resolveTC 0 fn ist) True
resolveTC depth fn ist
      = do hnf_compute
           g <- goal
           ptm <- get_term
           hs <- get_holes
           if True -- all (\n -> not (n `elem` hs)) (freeNames g)
            then try' (trivial ist)
                (do t <- goal
                    let insts = findInstances ist t
                    let (tc, ttypes) = unApply t
                    scopeOnly <- needsDefault t tc ttypes
                    tm <- get_term
--                    traceWhen (depth > 6) ("GOAL: " ++ show t ++ "\nTERM: " ++ show tm) $
--                        (tryAll (map elabTC (map fst (ctxtAlist (tt_ctxt ist)))))
--                     if scopeOnly then fail "Can't resolve" else
                    let depth' = if scopeOnly then 2 else depth
                    blunderbuss t depth' insts) True
            else do try' (trivial ist)
                         (do g <- goal
                             fail $ "Can't resolve " ++ show g) True
--             tm <- get_term
--                     fail $ "Can't resolve yet in " ++ show tm
  where
    elabTC n | n /= fn && tcname n = (resolve n depth, show n)
             | otherwise = (fail "Can't resolve", show n)

    needsDefault t num@(P _ (NS (UN "Num") ["Builtins"]) _) [P Bound a _]
        = do focus a
             fill (RConstant IType) -- default Int
             solve
             return False
    needsDefault t f as
          | all boundVar as = return True -- fail $ "Can't resolve " ++ show t
    needsDefault t f a = return False -- trace (show t) $ return ()

    boundVar (P Bound _ _) = True
    boundVar _ = False

    blunderbuss t d [] = do -- c <- get_env
                            -- ps <- get_probs
                            lift $ tfail $ CantResolve t
    blunderbuss t d (n:ns)
        | n /= fn && tcname n = try' (resolve n d)
                                     (blunderbuss t d ns) True
        | otherwise = blunderbuss t d ns

    resolve n depth
       | depth == 0 = fail $ "Can't resolve type class"
       | otherwise
           = do t <- goal
                let (tc, ttypes) = unApply t
--                 if (all boundVar ttypes) then resolveTC (depth - 1) fn insts ist
--                   else do
                   -- if there's a hole in the goal, don't even try
                let imps = case lookupCtxtName n (idris_implicits ist) of
                                [] -> []
                                [args] -> map isImp (snd args) -- won't be overloaded!
                ps <- get_probs
                args <- apply (Var n) imps
                ps' <- get_probs
                when (length ps < length ps') $ fail "Can't apply type class"
--                 traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $
                mapM_ (\ (_,n) -> do focus n
                                     t' <- goal
                                     let (tc', ttype) = unApply t'
                                     let depth' = if t == t' then depth - 1 else depth
                                     resolveTC depth' fn ist)
                      (filter (\ (x, y) -> not x) (zip (map fst imps) args))
                -- if there's any arguments left, we've failed to resolve
                hs <- get_holes
                solve
       where isImp (PImp p _ _ _ _) = (True, p)
             isImp arg = (False, priority arg)

collectDeferred :: Term -> State [(Name, Type)] Term
collectDeferred (Bind n (GHole t) app) =
    do ds <- get
       when (not (n `elem` map fst ds)) $ put ((n, t) : ds)
       collectDeferred app
collectDeferred (Bind n b t) = do b' <- cdb b
                                  t' <- collectDeferred t
                                  return (Bind n b' t')
  where
    cdb (Let t v)   = liftM2 Let (collectDeferred t) (collectDeferred v)
    cdb (Guess t v) = liftM2 Guess (collectDeferred t) (collectDeferred v)
    cdb b           = do ty' <- collectDeferred (binderTy b)
                         return (b { binderTy = ty' })
collectDeferred (App f a) = liftM2 App (collectDeferred f) (collectDeferred a)
collectDeferred t = return t

-- Running tactics directly
-- if a tactic adds unification problems, return an error

runTac :: Bool -> IState -> PTactic -> ElabD ()
runTac autoSolve ist tac
    = do env <- get_env
         no_errors $ runT (fmap (addImplBound ist (map fst env)) tac)
  where
    runT (Intro []) = do g <- goal
                         attack; intro (bname g)
      where
        bname (Bind n _ _) = Just n
        bname _ = Nothing
    runT (Intro xs) = mapM_ (\x -> do attack; intro (Just x)) xs
    runT Intros = do g <- goal
                     attack; intro (bname g)
                     try' (runT Intros)
                          (return ()) True
      where
        bname (Bind n _ _) = Just n
        bname _ = Nothing
    runT (Exact tm) = do elab ist toplevel False False (MN 0 "tac") tm
                         when autoSolve solveAll
    runT (Refine fn [])
        = do (fn', imps) <- case lookupCtxtName fn (idris_implicits ist) of
                                    [] -> do a <- envArgs fn
                                             return (fn, a)
                                    -- FIXME: resolve ambiguities
                                    [(n, args)] -> return $ (n, map isImp args)
             ns <- apply (Var fn') (map (\x -> (x, 0)) imps)
             when autoSolve solveAll
       where isImp (PImp _ _ _ _ _) = True
             isImp _ = False
             envArgs n = do e <- get_env
                            case lookup n e of
                               Just t -> return $ map (const False)
                                                      (getArgTys (binderTy t))
                               _ -> return []
    runT (Refine fn imps) = do ns <- apply (Var fn) (map (\x -> (x,0)) imps)
                               when autoSolve solveAll
    runT (Rewrite tm) -- to elaborate tm, let bind it, then rewrite by that
              = do attack; -- (h:_) <- get_holes
                   tyn <- unique_hole (MN 0 "rty")
                   -- start_unify h
                   claim tyn RType
                   valn <- unique_hole (MN 0 "rval")
                   claim valn (Var tyn)
                   letn <- unique_hole (MN 0 "rewrite_rule")
                   letbind letn (Var tyn) (Var valn)
                   focus valn
                   elab ist toplevel False False (MN 0 "tac") tm
                   rewrite (Var letn)
                   when autoSolve solveAll
    runT (LetTac n tm)
              = do attack
                   tyn <- unique_hole (MN 0 "letty")
                   claim tyn RType
                   valn <- unique_hole (MN 0 "letval")
                   claim valn (Var tyn)
                   letn <- unique_hole n
                   letbind letn (Var tyn) (Var valn)
                   focus valn
                   elab ist toplevel False False (MN 0 "tac") tm
                   when autoSolve solveAll
    runT (LetTacTy n ty tm)
              = do attack
                   tyn <- unique_hole (MN 0 "letty")
                   claim tyn RType
                   valn <- unique_hole (MN 0 "letval")
                   claim valn (Var tyn)
                   letn <- unique_hole n
                   letbind letn (Var tyn) (Var valn)
                   focus tyn
                   elab ist toplevel False False (MN 0 "tac") ty
                   focus valn
                   elab ist toplevel False False (MN 0 "tac") tm
                   when autoSolve solveAll
    runT Compute = compute
    runT Trivial = do trivial ist; when autoSolve solveAll
    runT (Focus n) = focus n
    runT Solve = solve
    runT (Try l r) = do try' (runT l) (runT r) True
    runT (TSeq l r) = do runT l; runT r
    runT (ApplyTactic tm) = do tenv <- get_env -- store the environment
                               tgoal <- goal -- store the goal
                               attack -- let f : List (TTName, Binder TT) -> TT -> Tactic = tm in ...
                               script <- unique_hole (MN 0 "script")
                               claim script scriptTy
                               scriptvar <- unique_hole (MN 0 "scriptvar" )
                               letbind scriptvar scriptTy (Var script)
                               focus script
                               elab ist toplevel False False (MN 0 "tac") tm
                               (script', _) <- get_type_val (Var scriptvar)
                               -- now that we have the script apply
                               -- it to the reflected goal and context
                               restac <- unique_hole (MN 0 "restac")
                               claim restac tacticTy
                               focus restac
                               fill (raw_apply (forget script')
                                               [reflectEnv tenv, reflect tgoal])
                               restac' <- get_guess
                               solve
                               -- normalise the result in order to
                               -- reify it
                               ctxt <- get_context
                               env <- get_env
                               let tactic = normalise ctxt env restac'
                               runReflected tactic
        where tacticTy = Var (reflm "Tactic")
              listTy = Var (NS (UN "List") ["List", "Prelude"])
              scriptTy = (RBind (UN "__pi_arg")
                                (Pi (RApp listTy envTupleType))
                                    (RBind (UN "__pi_arg1")
                                           (Pi (Var $ reflm "TT")) tacticTy))

    runT (Reflect v) = do attack -- let x = reflect v in ...
                          tyn <- unique_hole (MN 0 "letty")
                          claim tyn RType
                          valn <- unique_hole (MN 0 "letval")
                          claim valn (Var tyn)
                          letn <- unique_hole (MN 0 "letvar")
                          letbind letn (Var tyn) (Var valn)
                          focus valn
                          elab ist toplevel False False (MN 0 "tac") v
                          (value, _) <- get_type_val (Var letn)
                          ctxt <- get_context
                          env <- get_env
                          let value' = hnf ctxt env value
                          runTac autoSolve ist (Exact $ PQuote (reflect value'))
    runT (Fill v) = do attack -- let x = fill x in ...
                       tyn <- unique_hole (MN 0 "letty")
                       claim tyn RType
                       valn <- unique_hole (MN 0 "letval")
                       claim valn (Var tyn)
                       letn <- unique_hole (MN 0 "letvar")
                       letbind letn (Var tyn) (Var valn)
                       focus valn
                       elab ist toplevel False False (MN 0 "tac") v
                       (value, _) <- get_type_val (Var letn)
                       ctxt <- get_context
                       env <- get_env
                       let value' = normalise ctxt env value
                       rawValue <- reifyRaw value'
                       runTac autoSolve ist (Exact $ PQuote rawValue)
    runT (GoalType n tac) = do g <- goal
                               case unApply g of
                                    (P _ n' _, _) ->
                                       if nsroot n' == UN n
                                          then runT tac
                                          else fail "Wrong goal type"
                                    _ -> fail "Wrong goal type"
    runT x = fail $ "Not implemented " ++ show x

    runReflected t = do t' <- reify ist t
                        runTac autoSolve ist t'

-- | Prefix a name with the "Reflection.Language" namespace
reflm :: String -> Name
reflm n = NS (UN n) ["Reflection", "Language"]

-- | Reify tactics from their reflected representation
reify :: IState -> Term -> ElabD PTactic
reify _ (P _ n _) | n == reflm "Intros" = return Intros
reify _ (P _ n _) | n == reflm "Trivial" = return Trivial
reify _ (P _ n _) | n == reflm "Solve" = return Solve
reify _ (P _ n _) | n == reflm "Compute" = return Compute
reify ist t@(App _ _)
          | (P _ f _, args) <- unApply t = reifyApp ist f args
reify _ t = fail ("Unknown tactic " ++ show t)

reifyApp :: IState -> Name -> [Term] -> ElabD PTactic
reifyApp ist t [l, r] | t == reflm "Try" = liftM2 Try (reify ist l) (reify ist r)
reifyApp _ t [x]
           | t == reflm "Refine" = do n <- reifyTTName x
                                      return $ Refine n []
reifyApp ist t [l, r] | t == reflm "Seq" = liftM2 TSeq (reify ist l) (reify ist r)
reifyApp ist t [Constant (Str n), x]
             | t == reflm "GoalType" = liftM (GoalType n) (reify ist x)
reifyApp _ t [Constant (Str n)]
           | t == reflm "Intro" = return $ Intro [UN n]
reifyApp ist t [t']
             | t == reflm "ApplyTactic" = liftM (ApplyTactic . delab ist) (reifyTT t')
reifyApp ist t [t']
             | t == reflm "Reflect" = liftM (Reflect . delab ist) (reifyTT t')
reifyApp _ t [t']
           | t == reflm "Fill" = liftM (Fill . PQuote) (reifyRaw t')
reifyApp ist t [t']
             | t == reflm "Exact" = liftM (Exact . delab ist) (reifyTT t')
reifyApp ist t [x]
             | t == reflm "Focus" = liftM Focus (reifyTTName x)
reifyApp ist t [t']
             | t == reflm "Rewrite" = liftM (Rewrite . delab ist) (reifyTT t')
reifyApp ist t [n, t']
             | t == reflm "LetTac" = do n'  <- reifyTTName n
                                        t'' <- reifyTT t'
                                        return $ LetTac n' (delab ist t')
reifyApp ist t [n, tt', t']
             | t == reflm "LetTacTy" = do n'   <- reifyTTName n
                                          tt'' <- reifyTT tt'
                                          t''  <- reifyTT t'
                                          return $ LetTacTy n' (delab ist tt'') (delab ist t'')
reifyApp _ f args = fail ("Unknown tactic " ++ show (f, args)) -- shouldn't happen

-- | Reify terms from their reflected representation
reifyTT :: Term -> ElabD Term
reifyTT t@(App _ _)
        | (P _ f _, args) <- unApply t = reifyTTApp f args
reifyTT t@(P _ n _)
        | n == reflm "Erased" = return $ Erased
reifyTT t@(P _ n _)
        | n == reflm "Impossible" = return $ Impossible
reifyTT t = fail ("Unknown reflection term: " ++ show t)

reifyTTApp :: Name -> [Term] -> ElabD Term
reifyTTApp t [nt, n, x]
           | t == reflm "P" = do nt' <- reifyTTNameType nt
                                 n'  <- reifyTTName n
                                 x'  <- reifyTT x
                                 return $ P nt' n' x'
reifyTTApp t [Constant (I i)]
           | t == reflm "V" = return $ V i
reifyTTApp t [n, b, x]
           | t == reflm "Bind" = do n' <- reifyTTName n
                                    b' <- reifyTTBinder reifyTT (reflm "TT") b
                                    x' <- reifyTT x
                                    return $ Bind n' b' x'
reifyTTApp t [f, x]
           | t == reflm "App" = do f' <- reifyTT f
                                   x' <- reifyTT x
                                   return $ App f' x'
reifyTTApp t [c]
           | t == reflm "TConst" = liftM Constant (reifyTTConst c)
reifyTTApp t [t', Constant (I i)]
           | t == reflm "Proj" = do t'' <- reifyTT t'
                                    return $ Proj t'' i
reifyTTApp t [tt]
           | t == reflm "TType" = liftM TType (reifyTTUExp tt)
reifyTTApp t args = fail ("Unknown reflection term: " ++ show (t, args))

-- | Reify raw terms from their reflected representation
reifyRaw :: Term -> ElabD Raw
reifyRaw t@(App _ _)
         | (P _ f _, args) <- unApply t = reifyRawApp f args
reifyRaw t@(P _ n _)
         | n == reflm "RType" = return $ RType
reifyRaw t = fail ("Unknown reflection raw term: " ++ show t)

reifyRawApp :: Name -> [Term] -> ElabD Raw
reifyRawApp t [n]
            | t == reflm "Var" = liftM Var (reifyTTName n)
reifyRawApp t [n, b, x]
            | t == reflm "RBind" = do n' <- reifyTTName n
                                      b' <- reifyTTBinder reifyRaw (reflm "Raw") b
                                      x' <- reifyRaw x
                                      return $ RBind n' b' x'
reifyRawApp t [f, x]
            | t == reflm "RApp" = liftM2 RApp (reifyRaw f) (reifyRaw x)
reifyRawApp t [t']
            | t == reflm "RForce" = liftM RForce (reifyRaw t')
reifyRawApp t [c]
            | t == reflm "RConstant" = liftM RConstant (reifyTTConst c)
reifyRawApp t args = fail ("Unknown reflection raw term: " ++ show (t, args))

reifyTTName :: Term -> ElabD Name
reifyTTName t@(App _ _)
            | (P _ f _, args) <- unApply t = reifyTTNameApp f args
reifyTTName t = fail ("Unknown reflection term name: " ++ show t)

reifyTTNameApp :: Name -> [Term] -> ElabD Name
reifyTTNameApp t [Constant (Str n)]
               | t == reflm "UN" = return $ UN n
reifyTTNameApp t [n, ns]
               | t == reflm "NS" = do n'  <- reifyTTName n
                                      ns' <- reifyTTNamespace ns
                                      return $ NS n' ns'
reifyTTNameApp t [Constant (I i), Constant (Str n)]
               | t == reflm "MN" = return $ MN i n
reifyTTNameApp t []
               | t == reflm "NErased" = return NErased
reifyTTNameApp t args = fail ("Unknown reflection term name: " ++ show (t, args))

reifyTTNamespace :: Term -> ElabD [String]
reifyTTNamespace t@(App _ _)
  = case unApply t of
      (P _ f _, [Constant StrType])
           | f == NS (UN "Nil") ["List", "Prelude"] -> return []
      (P _ f _, [Constant StrType, Constant (Str n), ns])
           | f == NS (UN "::")  ["List", "Prelude"] -> liftM (n:) (reifyTTNamespace ns)
      _ -> fail ("Unknown reflection namespace arg: " ++ show t)
reifyTTNamespace t = fail ("Unknown reflection namespace arg: " ++ show t)

reifyTTNameType :: Term -> ElabD NameType
reifyTTNameType t@(P _ n _) | n == reflm "Bound" = return $ Bound
reifyTTNameType t@(P _ n _) | n == reflm "Ref" = return $ Ref
reifyTTNameType t@(App _ _)
  = case unApply t of
      (P _ f _, [Constant (I tag), Constant (I num)])
           | f == reflm "DCon" -> return $ DCon tag num
           | f == reflm "TCon" -> return $ TCon tag num
      _ -> fail ("Unknown reflection name type: " ++ show t)
reifyTTNameType t = fail ("Unknown reflection name type: " ++ show t)

reifyTTBinder :: (Term -> ElabD a) -> Name -> Term -> ElabD (Binder a)
reifyTTBinder reificator binderType t@(App _ _)
  = case unApply t of
     (P _ f _, bt:args) | forget bt == Var binderType
       -> reifyTTBinderApp reificator f args
     _ -> fail ("Mismatching binder reflection: " ++ show t)
reifyTTBinder _ _ t = fail ("Unknown reflection binder: " ++ show t)

reifyTTBinderApp :: (Term -> ElabD a) -> Name -> [Term] -> ElabD (Binder a)
reifyTTBinderApp reif f [t]
                      | f == reflm "Lam" = liftM Lam (reif t)
reifyTTBinderApp reif f [t]
                      | f == reflm "Pi" = liftM Pi (reif t)
reifyTTBinderApp reif f [x, y]
                      | f == reflm "Let" = liftM2 Let (reif x) (reif y)
reifyTTBinderApp reif f [x, y]
                      | f == reflm "NLet" = liftM2 NLet (reif x) (reif y)
reifyTTBinderApp reif f [t]
                      | f == reflm "Hole" = liftM Hole (reif t)
reifyTTBinderApp reif f [t]
                      | f == reflm "GHole" = liftM GHole (reif t)
reifyTTBinderApp reif f [x, y]
                      | f == reflm "Guess" = liftM2 Guess (reif x) (reif y)
reifyTTBinderApp reif f [t]
                      | f == reflm "PVar" = liftM PVar (reif t)
reifyTTBinderApp reif f [t]
                      | f == reflm "PVTy" = liftM PVTy (reif t)
reifyTTBinderApp _ f args = fail ("Unknown reflection binder: " ++ show (f, args))

reifyTTConst :: Term -> ElabD Const
reifyTTConst (P _ n _) | n == reflm "IType"    = return $ IType
reifyTTConst (P _ n _) | n == reflm "BIType"   = return $ BIType
reifyTTConst (P _ n _) | n == reflm "FlType"   = return $ FlType
reifyTTConst (P _ n _) | n == reflm "ChType"   = return $ ChType
reifyTTConst (P _ n _) | n == reflm "StrType"  = return $ StrType
reifyTTConst (P _ n _) | n == reflm "B8Type"   = return $ B8Type
reifyTTConst (P _ n _) | n == reflm "B16Type"  = return $ B16Type
reifyTTConst (P _ n _) | n == reflm "B32Type"  = return $ B32Type
reifyTTConst (P _ n _) | n == reflm "B64Type"  = return $ B64Type
reifyTTConst (P _ n _) | n == reflm "PtrType"  = return $ PtrType
reifyTTConst (P _ n _) | n == reflm "VoidType" = return $ VoidType
reifyTTConst (P _ n _) | n == reflm "Forgot"   = return $ Forgot
reifyTTConst t@(App _ _)
             | (P _ f _, [arg]) <- unApply t   = reifyTTConstApp f arg
reifyTTConst t = fail ("Unknown reflection constant: " ++ show t)

reifyTTConstApp :: Name -> Term -> ElabD Const
reifyTTConstApp f (Constant c@(I _))
                | f == reflm "I"   = return $ c
reifyTTConstApp f (Constant c@(BI _))
                | f == reflm "BI"  = return $ c
reifyTTConstApp f (Constant c@(Fl _))
                | f == reflm "Fl"  = return $ c
reifyTTConstApp f (Constant c@(I _))
                | f == reflm "Ch"  = return $ c
reifyTTConstApp f (Constant c@(Str _))
                | f == reflm "Str" = return $ c
reifyTTConstApp f (Constant c@(B8 _))
                | f == reflm "B8"  = return $ c
reifyTTConstApp f (Constant c@(B16 _))
                | f == reflm "B16" = return $ c
reifyTTConstApp f (Constant c@(B32 _))
                | f == reflm "B32" = return $ c
reifyTTConstApp f (Constant c@(B64 _))
                | f == reflm "B64" = return $ c
reifyTTConstApp f arg = fail ("Unknown reflection constant: " ++ show (f, arg))

reifyTTUExp :: Term -> ElabD UExp
reifyTTUExp t@(App _ _)
  = case unApply t of
      (P _ f _, [Constant (I i)]) | f == reflm "UVar" -> return $ UVar i
      (P _ f _, [Constant (I i)]) | f == reflm "UVal" -> return $ UVal i
      _ -> fail ("Unknown reflection type universe expression: " ++ show t)
reifyTTUExp t = fail ("Unknown reflection type universe expression: " ++ show t)

-- | Create a reflected call to a named function/constructor
reflCall :: String -> [Raw] -> Raw
reflCall funName args
  = raw_apply (Var (reflm funName)) args

-- | Lift a term into its Language.Reflection.TT representation
reflect :: Term -> Raw
reflect (P nt n t)
  = reflCall "P" [reflectNameType nt, reflectName n, reflect t]
reflect (V n)
  = reflCall "V" [RConstant (I n)]
reflect (Bind n b x)
  = reflCall "Bind" [reflectName n, reflectBinder b, reflect x]
reflect (App f x)
  = reflCall "App" [reflect f, reflect x]
reflect (Constant c)
  = reflCall "TConst" [reflectConstant c]
reflect (Proj t i)
  = reflCall "Proj" [reflect t, RConstant (I i)]
reflect (Erased) = Var (reflm "Erased")
reflect (Impossible) = Var (reflm "Impossible")
reflect (TType exp) = reflCall "TType" [reflectUExp exp]

reflectNameType :: NameType -> Raw
reflectNameType (Bound) = Var (reflm "Bound")
reflectNameType (Ref) = Var (reflm "Ref")
reflectNameType (DCon x y)
  = reflCall "DCon" [RConstant (I x), RConstant (I y)]
reflectNameType (TCon x y)
  = reflCall "TCon" [RConstant (I x), RConstant (I y)]

reflectName :: Name -> Raw
reflectName (UN str)
  = reflCall "UN" [RConstant (Str str)]
reflectName (NS n ns)
  = reflCall "NS" [ reflectName n
                  , foldr (\ n s ->
                             raw_apply ( Var $ NS (UN "::") ["List", "Prelude"] )
                                       [ RConstant StrType, RConstant (Str n), s ])
                             ( raw_apply ( Var $ NS (UN "Nil") ["List", "Prelude"] )
                                         [ RConstant StrType ])
                             ns
                  ]
reflectName (MN i n)
  = reflCall "MN" [RConstant (I i), RConstant (Str n)]
reflectName (NErased) = Var (reflm "NErased")

reflectBinder :: Binder Term -> Raw
reflectBinder (Lam t)
   = reflCall "Lam" [Var (reflm "TT"), reflect t]
reflectBinder (Pi t)
   = reflCall "Pi" [Var (reflm "TT"), reflect t]
reflectBinder (Let x y)
   = reflCall "Let" [Var (reflm "TT"), reflect x, reflect y]
reflectBinder (NLet x y)
   = reflCall "NLet" [Var (reflm "TT"), reflect x, reflect y]
reflectBinder (Hole t)
   = reflCall "Hole" [Var (reflm "TT"), reflect t]
reflectBinder (GHole t)
   = reflCall "GHole" [Var (reflm "TT"), reflect t]
reflectBinder (Guess x y)
   = reflCall "Guess" [Var (reflm "TT"), reflect x, reflect y]
reflectBinder (PVar t)
   = reflCall "PVar" [Var (reflm "TT"), reflect t]
reflectBinder (PVTy t)
   = reflCall "PVTy" [Var (reflm "TT"), reflect t]

reflectConstant :: Const -> Raw
reflectConstant c@(I  _) = reflCall "I"  [RConstant c]
reflectConstant c@(BI _) = reflCall "BI" [RConstant c]
reflectConstant c@(Fl _) = reflCall "Fl" [RConstant c]
reflectConstant c@(Ch _) = reflCall "Ch" [RConstant c]
reflectConstant c@(Str _) = reflCall "Str" [RConstant c]
reflectConstant (IType) = Var (reflm "IType")
reflectConstant (BIType) = Var (reflm "BIType")
reflectConstant (FlType) = Var (reflm "FlType")
reflectConstant (ChType) = Var (reflm "ChType")
reflectConstant (StrType) = Var (reflm "StrType")
reflectConstant c@(B8 _) = reflCall "B8" [RConstant c]
reflectConstant c@(B16 _) = reflCall "B16" [RConstant c]
reflectConstant c@(B32 _) = reflCall "B32" [RConstant c]
reflectConstant c@(B64 _) = reflCall "B64" [RConstant c]
reflectConstant (B8Type) = Var (reflm "B8Type")
reflectConstant (B16Type) = Var (reflm "B16Type")
reflectConstant (B32Type) = Var (reflm "B32Type")
reflectConstant (B64Type) = Var (reflm "B64Type")
reflectConstant (PtrType) = Var (reflm "PtrType")
reflectConstant (VoidType) = Var (reflm "VoidType")
reflectConstant (Forgot) = Var (reflm "Forgot")

reflectUExp :: UExp -> Raw
reflectUExp (UVar i) = reflCall "UVar" [RConstant (I i)]
reflectUExp (UVal i) = reflCall "UVal" [RConstant (I i)]

-- | Reflect the environment of a proof into a List (TTName, Binder TT)
reflectEnv :: Env -> Raw
reflectEnv = foldr consToEnvList emptyEnvList
  where
    consToEnvList :: (Name, Binder Term) -> Raw -> Raw
    consToEnvList (n, b) l
      = raw_apply (Var (NS (UN "::") ["List", "Prelude"]))
                  [ envTupleType
                  , raw_apply (Var pairCon) [ (Var $ reflm "TTName")
                                            , (RApp (Var $ reflm "Binder")
                                                    (Var $ reflm "TT"))
                                            , reflectName n
                                            , reflectBinder b
                                            ]
                  , l
                  ]

    emptyEnvList :: Raw
    emptyEnvList = raw_apply (Var (NS (UN "Nil") ["List", "Prelude"]))
                             [envTupleType]

envTupleType :: Raw
envTupleType
  = raw_apply (Var pairTy) [ (Var $ reflm "TTName")
                           , (RApp (Var $ reflm "Binder") (Var $ reflm "TT"))
                           ]

solveAll = try (do solve; solveAll) (return ())

-- If the function application is specialisable, make a new
-- top level function by normalising the application
-- and elaborating the new expression.

mkSpecialised :: IState -> FC -> Name -> [PTerm] -> PTerm -> ElabD PTerm
mkSpecialised i fc n args def
    = do let tm' = def
         case lookupCtxt n (idris_statics i) of
           [] -> return tm'
           [as] -> if (not (or as)) then return tm' else
                       mkSpecDecl i n (zip args as) tm'

mkSpecDecl :: IState -> Name -> [(PTerm, Bool)] -> PTerm -> ElabD PTerm
mkSpecDecl i n pargs tm'
    = do t <- goal
         g <- get_guess
         let (f, args) = unApply g
         let sargs = zip args (map snd pargs)
         let staticArgs = map fst (filter (\ (_,x) -> x) sargs)
         let ns = group (sort (concatMap staticFnNames staticArgs))
         let ntimes = map (\xs -> (head xs, length xs - 1)) ns
         if (not (null ns)) then
           do env <- get_env
              let g' = g -- specialise ctxt env ntimes g
              return tm'
--               trace (show t ++ "\n" ++
--                      show ntimes ++ "\n" ++
--                      show (delab i g) ++ "\n" ++ show (delab i g')) $ return tm' -- TODO
           else return tm'
  where
    ctxt = tt_ctxt i
    cg = idris_callgraph i

    staticFnNames tm | (P _ f _, as) <- unApply tm
        = if not (isFnName f ctxt) then []
             else case lookupCtxt f cg of
                    [ns] -> f : f : [] --(ns \\ [f])
                    [] -> [f,f]
                    _ -> []
    staticFnNames _ = []


text:
using System;
using System.Collections.Generic;
using CleanKludge.Core.Articles;
using CleanKludge.Core.Articles.Data;
using CleanKludge.Data.File.Articles.Converters;
using Newtonsoft.Json;
using Newtonsoft.Json.Converters;

namespace CleanKludge.Data.File.Articles
{
    public class ArticleSummaryRecord : IArticleSummaryDto
    {
        [JsonProperty("identifier")]
        [JsonConverter(typeof(ArticleIdentifierConverter))]
        public ArticleIdentifier Identifier { get; set; }

        [JsonProperty("enabled")]
        public bool Enabled { get; set; }

        [JsonProperty("created")]
        [JsonConverter(typeof(IsoDateTimeConverter))]
        public DateTimeOffset Created { get; set; }

        [JsonProperty("description")]
        public string Description { get; set; }

        [JsonProperty("author")]
        public string Author { get; set; }

        [JsonProperty("tags")]
        public List<string> Tags { get; set; }

        [JsonProperty("keywords")]
        public List<string> Keywords { get; set; }

        [JsonProperty("title")]
        public string Title { get; set; }

        [JsonProperty("location")]
        [JsonConverter(typeof(StringEnumConverter))]
        public Location Location { get; set; }

        protected bool Equals(ArticleSummaryRecord other)
        {
            return Equals(Identifier, other.Identifier);
        }

        public override bool Equals(object obj)
        {
            if(ReferenceEquals(null, obj))
                return false;

            if (ReferenceEquals(this, obj))
                return true;

            return obj.GetType() == GetType() && Equals((ArticleSummaryRecord)obj);
        }

        public override int GetHashCode()
        {
            return Identifier != null ? Identifier.GetHashCode() : 0;
        }
    }
}

redpajama_set_name: RedPajamaGithub


text:
SYNONYM

#### According to
The Catalogue of Life, 3rd January 2011

#### Published in
in Bourdot & Galzin, Bull. Soc. mycol. Fr. 27(2): 236 (1911)

#### Original name
Corticium avellaneum Bres., 1911

### Remarks
null


text:
set -ex

# We don't list explicit directories here. Instead, rely on the tools' default behaviour
# (or explicit configuration in setup.cfg/pyproject.toml). This helps to keep this script
# consistent with CI.

black .
flake8
isort .
mypy


text:
package com.planet_ink.coffee_mud.Abilities.Thief;
import com.planet_ink.coffee_mud.core.interfaces.*;
import com.planet_ink.coffee_mud.core.*;
import com.planet_ink.coffee_mud.core.collections.*;
import com.planet_ink.coffee_mud.Abilities.interfaces.*;
import com.planet_ink.coffee_mud.Areas.interfaces.*;
import com.planet_ink.coffee_mud.Behaviors.interfaces.*;
import com.planet_ink.coffee_mud.CharClasses.interfaces.*;
import com.planet_ink.coffee_mud.Commands.interfaces.*;
import com.planet_ink.coffee_mud.Common.interfaces.*;
import com.planet_ink.coffee_mud.Exits.interfaces.*;
import com.planet_ink.coffee_mud.Items.interfaces.*;
import com.planet_ink.coffee_mud.Libraries.interfaces.*;
import com.planet_ink.coffee_mud.Locales.interfaces.*;
import com.planet_ink.coffee_mud.MOBS.interfaces.*;
import com.planet_ink.coffee_mud.Races.interfaces.*;

import java.util.*;

public class Thief_Ambush extends ThiefSkill
{
	@Override public String ID() { return "Thief_Ambush"; }
	private final static String localizedName = CMLib.lang().L("Ambush");
	@Override public String name() { return localizedName; }
	@Override public String displayText(){ return "";}
	@Override protected int canAffectCode(){return CAN_MOBS;}
	@Override protected int canTargetCode(){return 0;}
	@Override public int abstractQuality(){return Ability.QUALITY_OK_OTHERS;}
	private static final String[] triggerStrings =I(new String[] {"AMBUSH"});
	@Override public String[] triggerStrings(){return triggerStrings;}
	@Override public int usageType(){return USAGE_MOVEMENT|USAGE_MANA;}
	@Override public int classificationCode(){return Ability.ACODE_THIEF_SKILL|Ability.DOMAIN_STEALTHY;}

	@Override
	public boolean invoke(MOB mob, List<String> commands, Physical givenTarget, boolean auto, int asLevel)
	{
		if(mob.fetchEffect("Thief_Hide")!=null)
		{
			mob.tell(L("You are already hiding."));
			return false;
		}

		if(mob.isInCombat())
		{
			mob.tell(L("Not while in combat!"));
			return false;
		}

		if(!super.invoke(mob,commands,givenTarget,auto,asLevel))
			return false;

		final Set<MOB> H=mob.getGroupMembers(new HashSet<MOB>());
		if(!H.contains(mob))
			H.add(mob);
		int numBesidesMe=0;
		for (final Object element : H)
		{
			final MOB M=(MOB)element;
			if((M!=mob)&&(mob.location().isInhabitant(M)))
				numBesidesMe++;
		}
		if(numBesidesMe==0)
		{
			mob.tell(L("You need a group to set up an ambush!"));
			return false;
		}
		for(int i=0;i<mob.location().numInhabitants();i++)
		{
			final MOB M=mob.location().fetchInhabitant(i);
			if((M!=null)&&(M!=mob)&&(!H.contains(M))&&(CMLib.flags().canSee(M)))
			{
				mob.tell(M,null,null,L("<S-NAME> is watching you too closely."));
				return false;
			}
		}
		boolean success=proficiencyCheck(mob,0,auto);

		if(!success)
			beneficialVisualFizzle(mob,null,L("<S-NAME> attempt(s) to set up an ambush, but fail(s)."));
		else
		{
			final CMMsg msg=CMClass.getMsg(mob,null,this,auto?CMMsg.MSG_OK_ACTION:(CMMsg.MSG_DELICATE_HANDS_ACT|CMMsg.MASK_MOVE),L("<S-NAME> set(s) up an ambush, directing everyone to hiding places."));
			if(mob.location().okMessage(mob,msg))
			{
				mob.location().send(mob,msg);
				invoker=mob;
				final Ability hide=CMClass.getAbility("Thief_Hide");
				for (final Object element : H)
				{
					final MOB M=(MOB)element;
					hide.invoke(M,M,true,adjustedLevel(mob,asLevel));
				}
			}
			else
				success=false;
		}
		return success;
	}
}


text:
#pragma once

#ifndef _QI_TRACKABLE_HPP_
# define _QI_TRACKABLE_HPP_

# include <boost/thread/mutex.hpp>
# include <boost/shared_ptr.hpp>
# include <boost/thread/condition_variable.hpp>
# include <boost/function.hpp>

# include <qi/log.hpp>

namespace qi
{

  /// Common base class to templates Trackable for compile-time detection.
  class TrackableBase {};

  /**
   * \brief Object tracking by blocking destruction while shared pointers are present.
   *
   * \includename{qi/trackable.hpp}
   * Inherit from Trackable to allow a form of tracking that blocks destruction
   * while shared pointers are held. This allows using your class without a
   * shared_ptr wrapper.
   *
   * \warning when inheriting from this class, you *must* invoke the destroy()
   * method from your destructor, before any operation that puts your object in
   * an invalid state.
   *
   * \warning since destroy() blocks until all shared pointers are destroyed,
   * deadlocks may occur if used improperly.
   *
   */
  template<typename T>
  class Trackable: public TrackableBase
  {
  public:
    /// Default constructor
    Trackable(T* ptr);
    /// Default destructor
    ~Trackable();

    /**
     * \return A shared_ptr that will block destruction (call to destroy() until
     *         it is released, or an empty shared_ptr if destroy was already called.
     */
    boost::shared_ptr<T> lock();

    /**
     * \return A weak_ptr from this. While a shared_ptr exists from this weak_ptr,
     *         a call to destroy will block()
     *
     */
    boost::weak_ptr<T>   weakPtr();

    /**
     * Blocks until destroy() is called and all shared_ptr built from weak_ptr()
     * are deleted.
     */
    void wait();
  protected:
    /**
     * *Must* be called by parent class destructor, first thing.
     * Can block until lock holders terminate
     */
    void destroy();
  private:
    void _destroyed();

    boost::shared_ptr<T>      _ptr;
    boost::condition_variable _cond;
    boost::mutex              _mutex;
    bool                      _wasDestroyed;
  };

  class QI_API PointerLockException: public std::exception
  {
  public:
    virtual const char* what() const throw()
    {
      return "Pointer Lock failed";
    }
  };

#ifdef DOXYGEN
  /** Bind a set of arguments or placeholders to a function.
   *
   * Handles first function argument of kind boost::weak_ptr and qi::Trackable:
   * will try to lock and throw qi::PointerLockException in case of failure
   */
  template<typename RF, typename AF> boost::function<RF> bind(const AF& fun, ...);
#endif

  /**
   * \brief Wrap given function f with a tracking check on arg0, which must
   *        be a weak pointer or a Trackable instance.
   * \return a function that, when called:
   *   - If lock can be acquired, calls f
   *   - Else throws qi::PointerLockException
   */
  template<typename F, typename ARG0>
  boost::function<F> track(const boost::function<F>& f, const ARG0& arg0);
  /**
   * \brief Wrap given function f with a tracking check on arg0, which must
   *        be a weak pointer or a Trackable instance.
   * \return a function that, when called:
   *   - If lock can be acquired, calls f
   *   - Else calls onFail
   */
  template<typename F, typename ARG0>
  boost::function<F> trackWithFallback(boost::function<void()> onFail,
      const boost::function<F>& f, const ARG0& arg0);
}

# include <qi/detail/trackable.hxx>
#endif  // _QI_TRACKABLE_HPP_


text:
using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Threading.Tasks;
using RopeSnake.IO;

namespace RopeSnake.Mother3.Text
{
    public abstract class StringReader
    {
        protected Dictionary<short, string> charLookup;
        protected IEnumerable<ControlCode> controlCodes;

        protected StringReader(Mother3Rom rom)
        {
            controlCodes = rom.Settings.ControlCodes;
            if (controlCodes == null)
            {
                throw new Exception("The control codes collection is null");
            }
        }

        public abstract string ReadDialogString(IBinaryReader reader);

        public abstract string ReadCodedString(IBinaryReader reader);

        public abstract string ReadCodedString(IBinaryReader reader, int maxLength);

        internal virtual ControlCode ProcessChar(IBinaryReader reader, StringBuilder sb, ref int count)
        {
            short ch = reader.ReadShort();
            count++;

            ControlCode code = controlCodes.FirstOrDefault(cc => cc.Code == ch);

            if (code != null)
            {
                if (code.Code != -1)
                {
                    sb.Append('[');

                    if (code.Tag != null)
                    {
                        sb.Append(code.Tag);
                    }
                    else
                    {
                        sb.Append(((ushort)ch).ToString("X4"));
                    }

                    for (int i = 0; i < code.Arguments; i++)
                    {
                        ch = reader.ReadShort();
                        count++;

                        sb.Append(' ');
                        sb.Append(((ushort)ch).ToString("X4"));
                    }

                    sb.Append(']');
                }
            }
            else
            {
                if (charLookup.ContainsKey(ch))
                {
                    sb.Append(charLookup[ch]);
                }
                else
                {
                    sb.Append('[');
                    sb.Append(((ushort)ch).ToString("X4"));
                    sb.Append(']');
                }
            }

            return code;
        }
    }
}


text:
oegen-html-bp
=============

Frontend HTML boilerplate


text:
<?php

require_once 'phing/input/MultipleChoiceInputRequest.php';

/**
 * Encapsulates an input request that returns a boolean (yes/no).
 *
 * @author  Hans Lellelid <hans@xmpl.org>
 * @version $Id$
 * @package phing.input
 */
class YesNoInputRequest extends MultipleChoiceInputRequest
{

    /**
     * @return true if the input is one of the allowed values.
     */
    public function isInputValid()
    {

        return StringHelper::isBoolean( $this->input );
    }

    /**
     * Converts input to boolean.
     *
     * @return boolean
     */
    public function getInput()
    {

        return StringHelper::booleanValue( $this->input );
    }
}


text:
<?php
namespace Phalcon
{

    /**
     * Phalcon\Dispatcher
     *
     * This is the base class for Phalcon\Mvc\Dispatcher and Phalcon\CLI\Dispatcher.
     * This class can't be instantiated directly, you can use it to create your own dispatchers
     */
    abstract class Dispatcher implements \Phalcon\DispatcherInterface, \Phalcon\Di\InjectionAwareInterface, \Phalcon\Events\EventsAwareInterface
    {

        const EXCEPTION_NO_DI = 0;

        const EXCEPTION_CYCLIC_ROUTING = 1;

        const EXCEPTION_HANDLER_NOT_FOUND = 2;

        const EXCEPTION_INVALID_HANDLER = 3;

        const EXCEPTION_INVALID_PARAMS = 4;

        const EXCEPTION_ACTION_NOT_FOUND = 5;

        /**
         *
         * @var \Phalcon\DiInterface
         */
        protected $_dependencyInjector;

        /**
         *
         * @var \Phalcon\Events\ManagerInterface
         */
        protected $_eventsManager;

        protected $_activeHandler;

        protected $_finished = false;

        protected $_forwarded = false;

        protected $_moduleName = null;

        protected $_namespaceName = null;

        protected $_handlerName = null;

        protected $_actionName = null;

        protected $_params = null;

        protected $_returnedValue = null;

        protected $_lastHandler = null;

        protected $_defaultNamespace = null;

        protected $_defaultHandler = null;

        protected $_defaultAction = '';

        protected $_handlerSuffix = '';

        protected $_actionSuffix = 'Action';

        protected $_previousHandlerName = null;

        protected $_previousActionName = null;

        /**
         * \Phalcon\Dispatcher constructor
         */
        public function __construct()
        {
            $this->_params = array();
        }

        /**
         * Sets the dependency injector
         *
         * @param
         *            \Phalcon\DiInterface dependencyInjector
         */
        public function setDI(\Phalcon\DiInterface $dependencyInjector)
        {
            $this->_dependencyInjector = $dependencyInjector;
        }

        /**
         * Returns the internal dependency injector
         *
         * @return \Phalcon\DiInterface
         */
        public function getDI()
        {
            return $this->_dependencyInjector;
        }

        /**
         * Sets the events manager
         *
         * @param
         *            \Phalcon\Events\ManagerInterface eventsManager
         */
        public function setEventsManager(\Phalcon\Events\ManagerInterface $eventsManager)
        {
            $this->_eventsManager = $eventsManager;
        }

        /**
         * Returns the internal event manager
         *
         * @return \Phalcon\Events\ManagerInterface
         */
        public function getEventsManager()
        {
            return $this->_eventsManager;
        }

        /**
         * Sets the default action suffix
         *
         * @param
         *            string actionSuffix
         */
        public function setActionSuffix($actionSuffix)
        {
            $this->_actionSuffix = $actionSuffix;
        }

        /**
         * Sets the module where the controller is (only informative)
         *
         * @param
         *            string moduleName
         */
        public function setModuleName($moduleName)
        {
            $this->_moduleName = $moduleName;
        }

        /**
         * Gets the module where the controller class is
         *
         * @return string
         */
        public function getModuleName()
        {
            return $this->_moduleName;
        }

        /**
         * Sets the namespace where the controller class is
         *
         * @param
         *            string namespaceName
         */
        public function setNamespaceName($namespaceName)
        {
            return $this->_namespaceName = $namespaceName;
        }

        /**
         * Gets a namespace to be prepended to the current handler name
         *
         * @return string
         */
        public function getNamespaceName()
        {
            return $this->_namespaceName;
        }

        /**
         * Sets the default namespace
         *
         * @param
         *            string namespaceName
         */
        public function setDefaultNamespace($namespaceName)
        {
            $this->_defaultNamespace = $namespaceName;
        }

        /**
         * Returns the default namespace
         *
         * @return string
         */
        public function getDefaultNamespace()
        {
            return $this->_defaultNamespace;
        }

        /**
         * Sets the default action name
         *
         * @param
         *            string actionName
         */
        public function setDefaultAction($actionName)
        {
            $this->_defaultAction = $actionName;
        }

        /**
         * Sets the action name to be dispatched
         *
         * @param
         *            string actionName
         */
        public function setActionName($actionName)
        {
            $this->_actionName = $actionName;
        }

        /**
         * Gets the latest dispatched action name
         *
         * @return string
         */
        public function getActionName()
        {
            return $this->_actionName;
        }

        /**
         * Sets action params to be dispatched
         *
         * @param
         *            array params
         */
        public function setParams($params)
        {
            if (! is_array($params)) {
                $this->_throwDispatchException('Parameters must be an Array', self::EXCEPTION_INVALID_PARAMS);
                return;
            }
            $this->_params = $params;
        }

        /**
         * Gets action params
         *
         * @return array
         */
        public function getParams()
        {
            return $this->_params;
        }

        /**
         * Set a param by its name or numeric index
         *
         * @param
         *            mixed param
         * @param
         *            mixed value
         */
        public function setParam($param, $value)
        {
            $this->_params[$name] = $value;
        }

        /**
         * Gets a param by its name or numeric index
         *
         * @param
         *            mixed param
         * @param
         *            string|array filters
         * @param
         *            mixed defaultValue
         * @return mixed
         */
        public function getParam($param, $filters = null, $defaultValue = null)
        {
            $params = $this->_params;
            $paramValue = null;
            if (isset($params[$param])) {
                $paramValue = $params[$param];
                if ($filters != null) {
                    $dependencyInjector = $this->_dependencyInjector;
                    if (! is_object($dependencyInjector)) {
                        $this->_throwDispatchException('A dependency injection object is required to access the \'filter\' service', self::EXCEPTION_NO_DI);
                        return null;
                    }
                    $filter = $dependencyInjector->getShared('filter');
                    return $filter->sanitize($paramValue, $filters);
                } else {
                    return $paramValue;
                }
            }
            return $defaultValue;
        }

        /**
         * Returns the current method to be/executed in the dispatcher
         *
         * @return string
         */
        public function getActiveMethod()
        {
            return $this->_actionName . $this->_actionSuffix;
        }

        /**
         * Checks if the dispatch loop is finished or has more pendent controllers/tasks to dispatch
         *
         * @return boolean
         */
        public function isFinished()
        {
            return $this->_finished;
        }

        /**
         * Sets the latest returned value by an action manually
         *
         * @param
         *            mixed value
         */
        public function setReturnedValue($value)
        {
            $this->_returnedValue = $value;
        }

        /**
         * Returns value returned by the lastest dispatched action
         *
         * @return mixed
         */
        public function getReturnedValue()
        {
            return $this->_returnedValue;
        }

        /**
         * Dispatches a handle action taking into account the routing parameters
         *
         * @return object
         */
        public function dispatch()
        {
            $dependencyInjector = $this->_dependencyInjector;
            if (! is_object($dependencyInjector)) {
                $this->_throwDispatchException('A dependency injection container is required to access related dispatching services', self::EXCEPTION_NO_DI);
                return false;
            }

            // Calling beforeDispatchLoop
            $eventsManager = $this->_eventsManager;
            $hasEventsManager = is_object($eventsManager);
            if ($hasEventsManager) {
                if ($eventsManager->fire('dispatch:beforeDispatchLoop', $this) === false) {
                    return false;
                }
            }

            $numberDispatches = 0;
            $handlerSuffix = $this->_handlerSuffix;
            $actionSuffix = $this->_actionSuffix;

            $this->_finished = false;

            while (! $this->_finished) {
                ++ $numberDispatches;

                // Throw an exception after 256 consecutive forwards
                if ($numberDispatches == 256) {
                    $this->_throwDispatchException('Dispatcher has detected a cyclic routing causing stability problems', self::EXCEPTION_CYCLIC_ROUTING);
                    break;
                }

                $this->_finished = true;

                // If the current namespace is null we used the set in this->_defaultNamespace
                $namespaceName = $this->_namespaceName;
                if (! $namespaceName) {
                    $this->_namespaceName = $namespaceName = $this->_defaultNamespace;
                }

                // If the handler is null we use the set in this->_defaultHandler
                $handlerName = $this->_handlerName;
                if (! $handlerName) {
                    $this->_handlerName = $handlerName = $this->_defaultHandler;
                }

                // If the action is null we use the set in this->_defaultAction
                $actionName = $this->_actionName;
                if (! $actionName) {
                    $this->_actionName = $actionName = $this->_defaultAction;
                }

                // Calling beforeDispatch
                if ($hasEventsManager) {
                    if ($eventsManager->fire('dispatch:beforeDispatch', $this) === false) {
                        continue;
                    }

                    // Check if the user made a forward in the listener
                    if (! $this->_finished == false) {
                        continue;
                    }
                }

                // We don't camelize the classes if they are in namespaces
                if (strpos($handlerName, '\\') === false) {
                    $camelizedClass = \Phalcon\Text::camelize($handlerName);
                } else {
                    $camelizedClass = $handlerName;
                }

                // Create the complete controller class name prepending the namespace
                if ($namespaceName) {
                    if (\Phalcon\Text::_ends_with($namespaceName, '\\')) {
                        $handlerClass = $namespaceName . $camelizedClass . $handlerSuffix;
                    } else {
                        $handlerClass = $namespaceName . '\\' . $camelizedClass . $handlerSuffix;
                    }
                } else {
                    $handlerClass = $camelizedClass . $handlerSuffix;
                }

                // Handlers are retrieved as shared instances from the Service Container
                $hasService = $dependencyInjector->has($handlerClass);
                if (! $hasService) {
                    // DI doesn't have a service with that name, try to load it using an autoloader
                    $hasService = class_exists($handlerClass);
                }

                // If the service can be loaded we throw an exception
                if (! $hasService) {
                    $status = $this->_throwDispatchException($handlerClass . '  handler class cannot be loaded', self::EXCEPTION_HANDLER_NOT_FOUND);
                    if ($status === false) {
                        // Check if the user made a forward in the listener
                        if ($this->_finished == false) {
                            continue;
                        }
                    }
                    break;
                }

                // Handlers must be only objects
                $handler = $dependencyInjector->getShared($handlerClass);

                $wasFresh = false;
                // If the object was recently created in the DI we initialize it
                if ($dependencyInjector->wasFreshInstance() === true) {
                    $wasFresh = true;
                }

                if (! is_object($handler)) {
                    $status = $this->_throwDispatchException('Invalid handler returned from the services container', self::EXCEPTION_INVALID_HANDLER);
                    if ($status === false) {
                        if ($this->_finished === false) {
                            continue;
                        }
                    }
                    break;
                }

                $this->_activeHandler = $handler;

                // Check if the params is an array
                $params = $this->_params;
                if (! is_array($params)) {
                    // An invalid parameter variable was passed throw an exception
                    $status = $this->_throwDispatchException('Action parameters must be an Array', self::EXCEPTION_INVALID_PARAMS);
                    if ($status === false) {
                        if ($this->_finished === false) {
                            continue;
                        }
                    }
                    break;
                }

                // Check if the method exists in the handler
                $actionMethod = $actionName . $actionSuffix;
                if (! method_exists($handler, $actionMethod)) {

                    // Call beforeNotFoundAction
                    if ($hasEventsManager) {
                        if ($eventsManager->fire('dispatch:beforeNotFoundAction', $this) === false) {
                            continue;
                        }

                        if ($this->_finished === false) {
                            continue;
                        }
                    }

                    // Try to throw an exception when an action isn't defined on the object
                    $status = $this->_throwDispatchException('Action \'' . $actionName . '\' was not found on handler \'' . $handlerName . '\'', self::EXCEPTION_ACTION_NOT_FOUND);
                    if ($status === false) {
                        if ($this->_finished === false) {
                            continue;
                        }
                    }

                    break;
                }

                // Calling beforeExecuteRoute
                if ($hasEventsManager) {
                    if ($eventsManager->fire('dispatch:beforeExecuteRoute', $this) === false) {
                        continue;
                    }

                    // Check if the user made a forward in the listener
                    if ($this->_finished === false) {
                        continue;
                    }
                }

                // Calling beforeExecuteRoute as callback and event
                if (method_exists($handler, 'beforeExecuteRoute')) {
                    if ($handler->beforeExecuteRoute($this) === false) {
                        continue;
                    }

                    // Check if the user made a forward in the listener
                    if ($this->_finished === false) {
                        continue;
                    }
                }

                /**
                 * Call the 'initialize' method just once per request
                 */
                if ($wasFresh === true) {
                    if (method_exists($handler, 'initialize')) {
                        $handler->initialize();
                    }

                    /**
                     * Calling afterInitialize
                     */
                    if ($hasEventsManager) {
                        if ($eventsManager->fire('dispatch:afterInitialize', $this) === false) {
                            continue;
                        }
                        // Check if the user made a forward in the listener
                        if ($this->_finished === false) {
                            continue;
                        }
                    }
                }

                try {
                    // We update the latest value produced by the latest handler
                    $this->_returnedValue = call_user_func_array(array(
                        $handler,
                        $actionMethod
                    ), $params);
                    $this->_lastHandler = $handler;
                } catch (\Exception $e) {
                    if ($this->_handleException($e) === false) {
                        if ($this->_finished === false) {
                            continue;
                        }
                    } else {
                        throw $e;
                    }
                }

                // Calling afterExecuteRoute
                if ($hasEventsManager) {
                    if ($eventsManager->fire('dispatch:afterExecuteRoute', $this, $this->_returnedValue) === false) {
                        continue;
                    }

                    if ($this->_finished === false) {
                        continue;
                    }

                    // Call afterDispatch
                    $eventsManager->fire('dispatch:afterDispatch', $this);
                }

                // Calling afterExecuteRoute as callback and event
                if (method_exists($handler, 'afterExecuteRoute')) {
                    if ($handler->afterExecuteRoute($this, $this->_returnedValue) === false) {
                        continue;
                    }
                    if ($this->_finished === false) {
                        continue;
                    }
                }
            }

            // Call afterDispatchLoop
            if ($hasEventsManager) {
                $eventsManager->fire('dispatch:afterDispatchLoop', $this);
            }
            return $handler;
        }

        /**
         * Forwards the execution flow to another controller/action
         * Dispatchers are unique per module.
         * Forwarding between modules is not allowed
         *
         * <code>
         * $this->dispatcher->forward(array("controller" => "posts", "action" => "index"));
         * </code>
         *
         * @param
         *            array forward
         */
        public function forward($forward)
        {
            if (! is_array($forward)) {
                $this->_throwDispatchException('Forward parameter must be an Array');
                return null;
            }

            // Check if we need to forward to another namespace
            if (isset($forward['namespace'])) {
                $this->_namespaceName = $forward['namespace'];
            }

            // Check if we need to forward to another controller
            if (isset($forward['controller'])) {
                $this->_previousHandlerName = $this->_handlerName;
                $this->_handlerName = $forward['controller'];
            } elseif (isset($forward['task'])) {
                $this->_previousHandlerName = $this->_handlerName;
                $this->_handlerName = $forward['task'];
            }

            // Check if we need to forward to another action
            if (isset($forward['action'])) {
                $this->_previousActionName = $this->_actionName;
                $this->_actionName = $forward['action'];
            }

            // Check if we need to forward changing the current parameters
            if (isset($forward['params'])) {
                $this->_params = $forward['params'];
            }

            $this->_finished = false;
            $this->_forwarded = true;
        }

        /**
         * Check if the current executed action was forwarded by another one
         *
         * @return boolean
         */
        public function wasForwarded()
        {
            return $this->_forwarded;
        }

        /**
         * Throws an internal exception
         *
         * @param string $message
         * @param int $exceptionCode
         * @return boolean
         */
        protected abstract function _throwDispatchException($message, $exceptionCode = null);

        /**
         * Handles a user exception
         *
         * @param \Exception $exception
         * @return boolean
         */
        protected abstract function _handleException(\Exception $exception);
    }
}


text:
     Edit
     View

           Delete
          {{controls.carreId}}


text:
<?php
$_GET['controller'] = 'Cron';
$_GET['action'] = 'index';
require_once 'index.php';
?>


text:
#ifndef __srtkThreeDCircularProjectionGeometryXMLFileReader_h
#define __srtkThreeDCircularProjectionGeometryXMLFileReader_h

#include "srtkMacro.h"
#include "srtkThreeDCircularProjectionGeometry.h"
#include "srtkMemberFunctionFactory.h"
#include "srtkIO.h"
#include "srtkProcessObject.h"

#include <memory>

namespace rtk {
  namespace simple {

    /** \class ThreeDCircularProjectionGeometryXMLFileReader
     * \brief Reads in an RTK 3D circular geometry as XML
     */
    class SRTKIO_EXPORT ThreeDCircularProjectionGeometryXMLFileReader  :
      public ProcessObject
    {
    public:
      typedef ThreeDCircularProjectionGeometryXMLFileReader Self;

      // function pointer type
      typedef Self& (Self::*MemberFunctionType)( const ThreeDCircularProjectionGeometry& );

      ThreeDCircularProjectionGeometryXMLFileReader( void );

      /** Print ourselves to string */
      virtual std::string ToString() const;

      /** return user readable name fo the filter */
      virtual std::string GetName() const { return std::string("ThreeDCircularProjectionGeometryXMLFileReader"); }

      Self& SetFileName ( std::string fileName );
      std::string GetFileName() const;

      ThreeDCircularProjectionGeometry Execute ( );
      ThreeDCircularProjectionGeometry Execute ( const std::string &inFileName );

    private:

      std::string m_FileName;
      ThreeDCircularProjectionGeometry m_Geometry;
    };

  SRTKIO_EXPORT ThreeDCircularProjectionGeometry ReadXML ( const std::string &fileName );
  }
}

#endif


text:
A tool for parsing the Hans Wehr dictionary from fodt format to plain-old-xml

To setup:
 - Run bundle to install all dependancies
 - build the xml file by running ``` ruby parser.rb ```


text:
title: "Long hair with a slight curl"
excerpt: "PaperFaces portrait of @VanessaTSmiles drawn with Paper by 53 on an iPad."
image:
  path: &image /assets/images/paperfaces-vanessatsmiles-twitter-lg.jpg
  feature: *image
  thumb: /assets/images/paperfaces-vanessatsmiles-twitter-150.jpg
tags: [portrait, illustration, Paper by 53, time lapse]
---

PaperFaces portrait of project donator [@VanessaTSmiles](http://twitter.com/VanessaTSmiles). First illustration done with the newly updated Paper by 53 app. Really like how zoom was implemented and the explore feature.

I also recorded my iPad's screen for this portrait that shows the new zoom tool in action. <del>Just have to edit the raw capture in Adobe AfterEffects and then post to YouTube. Should be up soon…</del>

{% include boilerplate/paperfaces.md %}

<iframe width="560" height="315" src="https://www.youtube.com/embed/PWf4WUoMXwg" frameborder="0"> </iframe>


text:
namespace remoting {
namespace protocol {

class HostVideoDispatcher : public ChannelDispatcherBase, public VideoStub {
 public:
  HostVideoDispatcher();
  ~HostVideoDispatcher() override;

  // VideoStub interface.
  void ProcessVideoPacket(scoped_ptr<VideoPacket> packet,
                          const base::Closure& done) override;

 private:
  DISALLOW_COPY_AND_ASSIGN(HostVideoDispatcher);
};

}  // namespace protocol
}  // namespace remoting

#endif  // REMOTING_PROTOCOL_HOST_VIDEO_DISPATCHER_H_