git.iko.soy/Idris-dev
on master help sign in
Start of defining functions in Tactical
cfd6dbcDavid Raymond Christiansen
libs/prelude/Language/Reflection/Tactical.idr+7
compare with master
unifiedsplit
@@ -16,6 +16,12 @@ data Arg : Type where
16data TyDecl : Type where
16data TyDecl : Type where
17 Declare : TTName -> List Arg -> Raw -> TyDecl
17 Declare : TTName -> List Arg -> Raw -> TyDecl
18
18
19+data FunClause : Type where
20+ MkFunClause : (lhs, rhs : Raw) -> FunClause
21+
22+data FunDefn : Type where
23+ DefineFun : TTName -> List FunClause -> FunDefn
24+
19abstract
25abstract
20data Tactical : Type -> Type where
26data Tactical : Type -> Type where
21 -- obligatory control stuff
27 -- obligatory control stuff
@@ -48,6 +54,7 @@ data Tactical : Type -> Type where
48 prim__Intro : Maybe TTName -> Tactical ()
54 prim__Intro : Maybe TTName -> Tactical ()
49
55
50 prim__DeclareType : TyDecl -> Tactical ()
56 prim__DeclareType : TyDecl -> Tactical ()
57+ prim__DefineFunction : FunDefn -> Tactical ()
51
58
52 prim__Debug : {a : Type} -> Maybe String -> Tactical a
59 prim__Debug : {a : Type} -> Maybe String -> Tactical a
53
60
src/Idris/ElabTerm.hs+19
@@ -1701,6 +1701,9 @@ runTactical fc env tm = do tm' <- eval tm
1701 new_tyDecls e }
1701 new_tyDecls e }
1702 aux <- getAux
1702 aux <- getAux
1703 returnUnit
1703 returnUnit
1704+ | n == tacN "prim__DefineFunction", [decl] <- args
1705+ = do undefined
1706+ undefined
1704 | n == tacN "prim__Debug", [ty, msg] <- args
1707 | n == tacN "prim__Debug", [ty, msg] <- args
1705 = do let msg' = fromTTMaybe msg
1708 = do let msg' = fromTTMaybe msg
1706 case msg' of
1709 case msg' of
@@ -2879,6 +2882,22 @@ reifyTyDecl (App (App (App (P (DCon _ _ _) n _) tyN) args) ret)
2879 reifyRArg aTm = fail $ "Couldn't reify " ++ show aTm ++ " as an RArg."
2882 reifyRArg aTm = fail $ "Couldn't reify " ++ show aTm ++ " as an RArg."
2880reifyTyDecl tm = fail $ "Couldn't reify " ++ show tm ++ " as a type declaration."
2883reifyTyDecl tm = fail $ "Couldn't reify " ++ show tm ++ " as a type declaration."
2881
2884
2885+reifyFunDefn :: Term -> ElabD RFunDefn
2886+reifyFunDefn (App (App (P _ n _) fnN) clauses)
2887+ | n == tacN "DefineFun" =
2888+ do fnN' <- reifyTTName fnN
2889+ clauses' <- case unList clauses of
2890+ Nothing -> fail $ "Couldn't reify " ++ show clauses ++ " as a clause list"
2891+ Just cs -> mapM reifyC cs
2892+ return $ RDefineFun fnN' clauses'
2893+ where reifyC :: Term -> ElabD RFunClause
2894+ reifyC (App (App (P (DCon _ _ _) n _) lhs) rhs)
2895+ | n == tacN "MkFunClause" = liftM2 RMkFunClause
2896+ (reifyRaw lhs)
2897+ (reifyRaw rhs)
2898+ reifyC tm = fail $ "Couldn't reify " ++ show tm ++ " as a clause."
2899+reifyFunDefn tm = fail $ "Couldn't reify " ++ show tm ++ " as a function declaration."
2900+
2882envTupleType :: Raw
2901envTupleType :: Raw
2883envTupleType
2902envTupleType
2884 = raw_apply (Var pairTy) [ (Var $ reflm "TTName")
2903 = raw_apply (Var pairTy) [ (Var $ reflm "TTName")
src/Idris/Reflection.hs+2
@@ -17,5 +17,7 @@ rArgToPArg (RExplicit n _) = PExp 0 [] n Placeholder
17rArgToPArg (RImplicit n _) = PImp 0 False [] n Placeholder
17rArgToPArg (RImplicit n _) = PImp 0 False [] n Placeholder
18rArgToPArg (RConstraint n _) = PConstraint 0 [] n Placeholder
18rArgToPArg (RConstraint n _) = PConstraint 0 [] n Placeholder
19
19
20+data RFunClause = RMkFunClause Raw Raw
20
21
22+data RFunDefn = RDefineFun Name [RFunClause]
21
23