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

git.iko.soy/Idris-dev

on master help sign in

Progress towards defining functions in Tactical

7d02904David Raymond Christiansen12 years ago

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

compare with master

unifiedsplit

@@ -18,6 +18,7 @@ data TyDecl : Type where

19data FunClause : Type where

20 MkFunClause : (lhs, rhs : Raw) -> FunClause

21+ MkImpossibleClause : (lhs : Raw) -> FunClause

22data FunDefn : Type where

23data FunDefn : Type where

23 DefineFun : TTName -> List FunClause -> FunDefn

24 DefineFun : TTName -> List FunClause -> FunDefn

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

138declareType : TyDecl -> Tactical ()

139declareType : TyDecl -> Tactical ()

139declareType decl = prim__DeclareType decl

140declareType decl = prim__DeclareType decl

140

141

142+defineFunction : FunDefn -> Tactical ()

143+defineFunction defun = prim__DefineFunction defun

144+

141debug : Tactical a

145debug : Tactical a

142debug = prim__Debug Nothing

146debug = prim__Debug Nothing

143

147

src/Idris/AbsSyntaxTree.hs+1

@@ -648,6 +648,7 @@ deriving instance NFData PDecl'

648-- | A set of instructions for things that need to happen in IState

649-- after a term elaboration when there's been reflected elaboration.

650data RDeclInstructions = RTyDeclInstrs Name FC [PArg] Type

651+ | RClausesInstrs Name [([Name], Term, Term)]

651

652

652-- | For elaborator state

653-- | For elaborator state

653data EState = EState {

654data EState = EState {

src/Idris/ElabTerm.hs+50−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

@@ -61,6 +62,11 @@ processTacticDecls info =

61 addIBC (IBCDef n)

62 addIBC (IBCDef n)

62 let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds

63 let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds

63 addDeferred ds'

64 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)

65-- Using the elaborator, convert a term in raw syntax to a fully

71-- Using the elaborator, convert a term in raw syntax to a fully

66-- elaborated, typechecked term.

72-- elaborated, typechecked term.

@@ -1596,6 +1602,45 @@ runTactical fc env tm = do tm' <- eval tm

1596

1602

1597 returnUnit = fmap fst $ get_type_val (Var unitCon)

1603 returnUnit = fmap fst $ get_type_val (Var unitCon)

1598

1604

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+

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

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

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

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

1601 runTacTm :: Term -> ElabD Term

1646 runTacTm :: Term -> ElabD Term

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

1709 aux <- getAux

1754 aux <- getAux

1710 returnUnit

1755 returnUnit

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

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

1712− = do undefined

1757+ = do defn <- reifyFunDefn decl

1713− undefined

1758+ defineFunction defn

1759+ returnUnit

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

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

1715 = do let msg' = fromTTMaybe msg

1761 = do let msg' = fromTTMaybe msg

1716 case msg' of

1762 case msg' of

@@ -2890,6 +2936,8 @@ reifyFunDefn (App (App (P _ n _) fnN) clauses)

2890 | n == tacN "MkFunClause" = liftM2 RMkFunClause

2936 | n == tacN "MkFunClause" = liftM2 RMkFunClause

2891 (reifyRaw lhs)

2937 (reifyRaw lhs)

2892 (reifyRaw rhs)

2938 (reifyRaw rhs)

2939+ reifyC (App (P (DCon _ _ _) n _) lhs)

2940+ | n == tacN "MkImpossibleClause" = fmap RMkImpossibleClause $ reifyRaw lhs

2893 reifyC tm = fail $ "Couldn't reify " ++ show tm ++ " as a clause."

2941 reifyC tm = fail $ "Couldn't reify " ++ show tm ++ " as a clause."

2894reifyFunDefn tm = fail $ "Couldn't reify " ++ show tm ++ " as a function declaration."

2942reifyFunDefn tm = fail $ "Couldn't reify " ++ show tm ++ " as a function declaration."

2895

2943

src/Idris/Reflection.hs+3−2

@@ -18,6 +18,7 @@ rArgToPArg (RImplicit n _) = PImp 0 False [] n Placeholder

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

20data RFunClause = RMkFunClause Raw Raw

21+ | RMkImpossibleClause Raw

22+ deriving Show

22−data RFunDefn = RDefineFun Name [RFunClause]

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

23−