7d2893e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Progress towards defining functions in Tactical

7d2893eDavid Raymond Christiansen12 years ago

libs/prelude/Language/Reflection/Tactical.idr+3

compare with master

unifiedsplit

@@ -138,6 +138,9 @@ rewriteWith rule = prim__Rewrite rule

138declareType : TyDecl -> Tactical ()

139declareType decl = prim__DeclareType decl

140

141+defineFunction : FunDefn -> Tactical ()

142+defineFunction defun = prim__DefineFunction defun

143+

141debug : Tactical a

144debug : Tactical a

142debug = prim__Debug Nothing

145debug = prim__Debug Nothing

143

146

src/Idris/ElabTerm.hs+28−2

@@ -10,6 +10,7 @@ import Idris.Error

10import Idris.ProofSearch

11import Idris.Output (pshow)

13+import Idris.Core.CaseTree (SC, SC'(STerm))

13import Idris.Core.Elaborate hiding (Tactic(..))

14import Idris.Core.Elaborate hiding (Tactic(..))

14import Idris.Core.TT

15import Idris.Core.TT

15import Idris.Core.Evaluate

16import Idris.Core.Evaluate

@@ -1596,6 +1597,30 @@ runTactical fc env tm = do tm' <- eval tm

1596

1597

1597 returnUnit = fmap fst $ get_type_val (Var unitCon)

1598 returnUnit = fmap fst $ get_type_val (Var unitCon)

1598

1599

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+

1599 -- | Do a step in the reflected elaborator monad. The input is the

1624 -- | Do a step in the reflected elaborator monad. The input is the

1600 -- step, the output is the (reflected) term returned.

1625 -- step, the output is the (reflected) term returned.

1601 runTacTm :: Term -> ElabD Term

1626 runTacTm :: Term -> ElabD Term

@@ -1709,8 +1734,9 @@ runTactical fc env tm = do tm' <- eval tm

1709 aux <- getAux

1734 aux <- getAux

1710 returnUnit

1735 returnUnit

1711 | n == tacN "prim__DefineFunction", [decl] <- args

1736 | n == tacN "prim__DefineFunction", [decl] <- args

1712− = do undefined

1737+ = do defn <- reifyFunDefn decl

1713− undefined

1738+ defineFunction defn

1739+ returnUnit

1714 | n == tacN "prim__Debug", [ty, msg] <- args

1740 | n == tacN "prim__Debug", [ty, msg] <- args

1715 = do let msg' = fromTTMaybe msg

1741 = do let msg' = fromTTMaybe msg

1716 case msg' of

1742 case msg' of

src/Idris/Reflection.hs+2−3

@@ -17,7 +17,6 @@ rArgToPArg (RExplicit n _) = PExp 0 [] n Placeholder

17rArgToPArg (RImplicit n _) = PImp 0 False [] n Placeholder

18rArgToPArg (RConstraint n _) = PConstraint 0 [] n Placeholder

20−data RFunClause = RMkFunClause Raw Raw

20+data RFunClause = RMkFunClause Raw Raw deriving Show

21−

22−data RFunDefn = RDefineFun Name [RFunClause]

22+data RFunDefn = RDefineFun Name [RFunClause] deriving Show