@@ -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
@@ -1596,6 +1597,30 @@ runTactical fc env tm = do tm' <- eval tm
15961597
15971598 returnUnit = fmap fst $ get_type_val (Var unitCon)
15981599
1600+ defineFunction :: RFunDefn -> ElabD ()
1601+ defineFunction (RDefineFun n clauses) =
1602+ do ctxt <- get_context
1603+ ty <- maybe (fail "no type decl") return $ lookupTyExact n ctxt
1604+ let info = CaseInfo True True False -- TODO document and figure out
1605+ clauses' <- forM clauses (\(RMkFunClause lhs rhs) ->
1606+ do lhs' <- lift $ check ctxt [] lhs
1607+ rhs' <- lift $ check ctxt [] rhs
1608+ return (fst lhs', fst rhs'))
1609+ trace (show clauses') $ return ()
1610+ set_context $
1611+ addCasedef n (const [])
1612+ info False (STerm Erased)
1613+ True False -- TODO what are these?
1614+ [] [] -- TODO argument types, inaccessible types
1615+ (map Right clauses')
1616+ (map (\(l,r) -> ([], l, r)) clauses')
1617+ (map (\(l,r) -> ([], l, r)) clauses')
1618+ (map (\(l,r) -> ([], l, r)) clauses')
1619+ (map (\(l,r) -> ([], l, r)) clauses')
1620+ ty
1621+ ctxt
1622+ return ()
1623+
15991624 -- | Do a step in the reflected elaborator monad. The input is the
16001625 -- step, the output is the (reflected) term returned.
16011626 runTacTm :: Term -> ElabD Term
@@ -1709,8 +1734,9 @@ runTactical fc env tm = do tm' <- eval tm
17091734 aux <- getAux
17101735 returnUnit
17111736 | n == tacN "prim__DefineFunction", [decl] <- args
1712− = do undefined
1713− undefined
1737+ = do defn <- reifyFunDefn decl
1738+ defineFunction defn
1739+ returnUnit
17141740 | n == tacN "prim__Debug", [ty, msg] <- args
17151741 = do let msg' = fromTTMaybe msg
17161742 case msg' of