@@ -10,6 +10,7 @@ import Idris.Error
1010import Idris.ProofSearch
1111import Idris.Output (pshow)
1212
13+import Idris.Core.CaseTree (SC, SC'(STerm))
1314import Idris.Core.Elaborate hiding (Tactic(..))
1415import Idris.Core.TT
1516import Idris.Core.Evaluate
@@ -61,6 +62,11 @@ processTacticDecls info =
6162 addIBC (IBCDef n)
6263 let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds
6364 addDeferred ds'
65+ RClausesInstrs n cs ->
66+ do logLvl 3 $ "Pattern-matching definition from tactics: " ++ show n
67+ solveDeferred n
68+ updateIState $ \i -> i { idris_patdefs = addDef n (cs, []) $ idris_patdefs i } -- TODO: missing clauses
69+ addIBC (IBCDef n)
6470
6571-- Using the elaborator, convert a term in raw syntax to a fully
6672-- elaborated, typechecked term.
@@ -1596,6 +1602,45 @@ runTactical fc env tm = do tm' <- eval tm
15961602
15971603 returnUnit = fmap fst $ get_type_val (Var unitCon)
15981604
1605+ patvars :: [Name] -> Term -> ([Name], Term)
1606+ patvars ns (Bind n (PVar t) sc) = patvars (n : ns) (instantiate (P Bound n t) sc)
1607+ patvars ns tm = (ns, tm)
1608+
1609+ pullVars :: (Term, Term) -> ([Name], Term, Term)
1610+ pullVars (lhs, rhs) = (fst (patvars [] lhs), snd (patvars [] lhs), snd (patvars [] rhs)) -- TODO alpha-convert rhs
1611+
1612+ defineFunction :: RFunDefn -> ElabD ()
1613+ defineFunction (RDefineFun n clauses) =
1614+ do ctxt <- get_context
1615+ ty <- maybe (fail "no type decl") return $ lookupTyExact n ctxt
1616+ let info = CaseInfo True True False -- TODO document and figure out
1617+ clauses' <- forM clauses (\case
1618+ RMkFunClause lhs rhs ->
1619+ do lhs' <- fmap fst . lift $ check ctxt [] lhs
1620+ rhs' <- fmap fst . lift $ check ctxt [] rhs
1621+ return $ Right (lhs', rhs')
1622+ RMkImpossibleClause lhs ->
1623+ do lhs' <- fmap fst . lift $ check ctxt [] lhs
1624+ return $ Left lhs')
1625+ let clauses'' = map (\case Right c -> pullVars c
1626+ Left lhs -> let (ns, lhs') = patvars [] lhs'
1627+ in (ns, lhs', Impossible))
1628+ clauses'
1629+ set_context $
1630+ addCasedef n (const [])
1631+ info False (STerm Erased)
1632+ True False -- TODO what are these?
1633+ [] [] -- TODO argument types, inaccessible types
1634+ clauses'
1635+ clauses''
1636+ clauses''
1637+ clauses''
1638+ clauses''
1639+ ty
1640+ ctxt
1641+ updateAux $ \e -> e { new_tyDecls = RClausesInstrs n clauses'' : new_tyDecls e}
1642+ return ()
1643+
15991644 -- | Do a step in the reflected elaborator monad. The input is the
16001645 -- step, the output is the (reflected) term returned.
16011646 runTacTm :: Term -> ElabD Term
@@ -1709,8 +1754,9 @@ runTactical fc env tm = do tm' <- eval tm
17091754 aux <- getAux
17101755 returnUnit
17111756 | n == tacN "prim__DefineFunction", [decl] <- args
1712− = do undefined
1713− undefined
1757+ = do defn <- reifyFunDefn decl
1758+ defineFunction defn
1759+ returnUnit
17141760 | n == tacN "prim__Debug", [ty, msg] <- args
17151761 = do let msg' = fromTTMaybe msg
17161762 case msg' of
@@ -2890,6 +2936,8 @@ reifyFunDefn (App (App (P _ n _) fnN) clauses)
28902936 | n == tacN "MkFunClause" = liftM2 RMkFunClause
28912937 (reifyRaw lhs)
28922938 (reifyRaw rhs)
2939+ reifyC (App (P (DCon _ _ _) n _) lhs)
2940+ | n == tacN "MkImpossibleClause" = fmap RMkImpossibleClause $ reifyRaw lhs
28932941 reifyC tm = fail $ "Couldn't reify " ++ show tm ++ " as a clause."
28942942reifyFunDefn tm = fail $ "Couldn't reify " ++ show tm ++ " as a function declaration."
28952943