cdc7238 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Make FunDefn and FunClause polymorphic over TT and Raw

cdc7238Shea Levy11 years ago

libs/prelude/Language/Reflection/Elab.idr+10−10

compare with master

unifiedsplit

@@ -70,15 +70,15 @@ record TyDecl where

72||| A single pattern-matching clause

73−data FunClause : Type where

73+data FunClause : Type -> Type where

74− MkFunClause : (lhs, rhs : Raw) -> FunClause

74+ MkFunClause : (lhs, rhs : a) -> FunClause a

75− MkImpossibleClause : (lhs : Raw) -> FunClause

75+ MkImpossibleClause : (lhs : a) -> FunClause a

77||| A reflected function definition.

78−record FunDefn where

78+record FunDefn a where

79 constructor DefineFun

80 name : TTName

81− clauses : List FunClause

81+ clauses : List (FunClause a)

84data CtorArg = CtorParameter FunArg | CtorField FunArg

@@ -115,7 +115,7 @@ data Elab : Type -> Type where

115 Prim__Guess : Elab TT

116 Prim__LookupTy : TTName -> Elab (List (TTName, NameType, TT))

117 Prim__LookupDatatype : TTName -> Elab (List Datatype)

118− Prim__LookupFunDefn : TTName -> Elab (List FunDefn)

118+ Prim__LookupFunDefn : TTName -> Elab (List (FunDefn TT))

119 Prim__LookupArgs : TTName -> Elab (List (TTName, List FunArg, Raw))

120

121 Prim__Check : List (TTName, Binder TT) -> Raw -> Elab (TT, TT)

@@ -148,7 +148,7 @@ data Elab : Type -> Type where

148 Prim__Converts : (List (TTName, Binder TT)) -> TT -> TT -> Elab ()

149

150 Prim__DeclareType : TyDecl -> Elab ()

151− Prim__DefineFunction : FunDefn -> Elab ()

151+ Prim__DefineFunction : FunDefn Raw -> Elab ()

152 Prim__AddInstance : TTName -> TTName -> Elab ()

153 Prim__IsTCName : TTName -> Elab Bool

154

@@ -233,13 +233,13 @@ namespace Tactics

233

234 ||| Find the reflected function definition of all functions whose names

235 ||| are overloadings of some name.

236− lookupFunDefn : TTName -> Elab (List FunDefn)

236+ lookupFunDefn : TTName -> Elab (List (FunDefn TT))

237 lookupFunDefn n = Prim__LookupFunDefn n

238

239 ||| Find the reflected function definition of a function, given its

240 ||| fully-qualified name. Fail if the name does not uniquely resolve

241 ||| to a function.

242− lookupFunDefnExact : TTName -> Elab FunDefn

242+ lookupFunDefnExact : TTName -> Elab (FunDefn TT)

243 lookupFunDefnExact n = case !(lookupFunDefn n) of

244 [res] => return res

245 [] => fail [TextPart "No function named", NamePart n]

@@ -465,7 +465,7 @@ namespace Tactics

465 ||| Define a function in the global context. The function must have

466 ||| already been declared, either in ordinary Idris code or using

467 ||| `declareType`.

468− defineFunction : FunDefn -> Elab ()

468+ defineFunction : FunDefn Raw -> Elab ()

469 defineFunction defun = Prim__DefineFunction defun

470

471 ||| Register a new instance for type class resolution.

libs/pruviloj/Pruviloj/Derive/DecEq.idr+1−1

@@ -183,7 +183,7 @@ deriveDecEq fn =

183 Nothing => return False

184

185 partial -- mkRhs

186− mkCase : Nat -> TTName -> (x, y : (TTName, List CtorArg, Raw)) -> Elab (Maybe FunClause)

186+ mkCase : Nat -> TTName -> (x, y : (TTName, List CtorArg, Raw)) -> Elab (Maybe (FunClause Raw))

187 mkCase k fam (cn1, args1, _) (cn2, args2, _) =

188 perhaps $ elabPatternClause

189 (do (h2 :: h1 :: _) <- reverse <$>

libs/pruviloj/Pruviloj/Derive/Eliminators.idr+3−3

@@ -134,7 +134,7 @@ instance Show ElimArg where

134 show (NormalArgument x) = "NormalArgument " ++ show x

135

136getElimClause : TyConInfo -> (elimn : TTName) -> (methCount : Nat) ->

137− (TTName, List CtorArg, Raw) -> Nat -> Elab FunClause

137+ (TTName, List CtorArg, Raw) -> Nat -> Elab (FunClause Raw)

138getElimClause info elimn methCount (cn, args, resTy) whichCon =

139 elabPatternClause

140 (do -- Establish a hole for each parameter

@@ -242,13 +242,13 @@ getElimClause info elimn methCount (cn, args, resTy) whichCon =

242 bindLam ((n, b)::rest) x = RBind n (Lam (getBinderTy b)) $ bindLam rest x

243

244getElimClauses : TyConInfo -> (elimn : TTName) ->

245− List (TTName, List CtorArg, Raw) -> Elab (List FunClause)

245+ List (TTName, List CtorArg, Raw) -> Elab (List (FunClause Raw))

246getElimClauses info elimn ctors =

247 let methodCount = length ctors

248 in traverse (\(i, con) => getElimClause info elimn methodCount con i)

249 (enumerate ctors)

250

251−instance Show FunClause where

251+instance (Show a) => Show (FunClause a) where

252 show (MkFunClause x y) = "(MkFunClause " ++ show x ++ " " ++ show y ++ ")"

253

254abstract

libs/pruviloj/Pruviloj/Internals.idr+1−1

@@ -101,7 +101,7 @@ bindPatTys ((n, b)::bs) res = RBind n (PVTy (getBinderTy b)) $ bindPatTys bs res

101||| It will be run in a context where the pattern variables are

102||| already bound, and should leave behind no holes.

103partial

104−elabPatternClause : (lhs, rhs : Elab ()) -> Elab FunClause

104+elabPatternClause : (lhs, rhs : Elab ()) -> Elab (FunClause Raw)

105elabPatternClause lhs rhs =

106 do -- Elaborate the LHS in a context where its type will be solved via unification

107 (pat, _) <- runElab `(Infer) $

src/Idris/Core/TT.hs−1

@@ -1107,7 +1107,6 @@ instantiate e = subst 0 where

1107 subst i (Bind x b sc) = Bind x (fmap (subst i) b) (subst (i+1) sc)

1108 subst i (App s f a) = App s (subst i f) (subst i a)

1109 subst i (Proj x idx) = Proj (subst i x) idx

1110− -- If ever adding a clause here, please update mkFunClause in Idris/Reflection.hs

1111 subst i t = t

1110 subst i t = t

1112

1111

1113-- | As 'instantiate', but also decrement the indices of all de Bruijn variables

1112-- | As 'instantiate', but also decrement the indices of all de Bruijn variables

src/Idris/Elab/Term.hs+2−2

@@ -1770,7 +1770,7 @@ runElabAction ist fc env tm ns = do tm' <- eval tm

1770 pullVars :: (Term, Term) -> ([Name], Term, Term)

1771 pullVars (lhs, rhs) = (fst (patvars [] lhs), snd (patvars [] lhs), snd (patvars [] rhs)) -- TODO alpha-convert rhs

1772

1773− defineFunction :: RFunDefn -> ElabD ()

1773+ defineFunction :: RFunDefn Raw -> ElabD ()

1774 defineFunction (RDefineFun n clauses) =

1775 do ctxt <- get_context

1776 ty <- maybe (fail "no type decl") return $ lookupTyExact n ctxt

@@ -1865,7 +1865,7 @@ runElabAction ist fc env tm ns = do tm' <- eval tm

1865 | n == tacN "Prim__LookupFunDefn", [name] <- args

1866 = do n' <- reifyTTName name

1867 fmap fst . checkClosed $

1868− rawList (Var (tacN "FunDefn"))

1868+ rawList (RApp (Var $ tacN "FunDefn") (Var $ reflm "TT"))

1869 (map reflectFunDefn (buildFunDefns ist n'))

1870 | n == tacN "Prim__LookupArgs", [name] <- args

1871 = do n' <- reifyTTName name

src/Idris/Reflection.hs+30−45

@@ -11,7 +11,7 @@ import Prelude hiding (mapM)

11import Data.Traversable (mapM)

12#endif

13import Control.Monad (liftM, liftM2, liftM4)

14−import Control.Monad.State.Strict (lift, State, runState, put)

14+import Control.Monad.State.Strict (lift)

15import Data.Maybe (catMaybes)

16import Data.List ((\\), findIndex)

17import qualified Data.Text as T

@@ -57,11 +57,11 @@ rFunArgToPArg (RFunArg n _ RExplicit e) = PExp 0 (rArgOpts e) n Placeholder

57rFunArgToPArg (RFunArg n _ RImplicit e) = PImp 0 False (rArgOpts e) n Placeholder

58rFunArgToPArg (RFunArg n _ RConstraint e) = PConstraint 0 (rArgOpts e) n Placeholder

60−data RFunClause = RMkFunClause Raw Raw

60+data RFunClause a = RMkFunClause a a

61− | RMkImpossibleClause Raw

61+ | RMkImpossibleClause a

62− deriving Show

62+ deriving Show

64−data RFunDefn = RDefineFun Name [RFunClause] deriving Show

64+data RFunDefn a = RDefineFun Name [RFunClause a] deriving Show

66-- | Prefix a name with the "Language.Reflection" namespace

67reflm :: String -> Name

@@ -1025,21 +1025,21 @@ reifyTyDecl (App _ (App _ (App _ (P (DCon _ _ _) n _) tyN) args) ret)

1025 return $ RDeclare tyN' args' ret'

1026reifyTyDecl tm = fail $ "Couldn't reify " ++ show tm ++ " as a type declaration."

1027

1028−reifyFunDefn :: Term -> ElabD RFunDefn

1028+reifyFunDefn :: Term -> ElabD (RFunDefn Raw)

1029−reifyFunDefn (App _ (App _ (P _ n _) fnN) clauses)

1029+reifyFunDefn (App _ (App _ (App _ (P _ n _) (P _ t _)) fnN) clauses)

1030− | n == tacN "DefineFun" =

1030+ | n == tacN "DefineFun" && t == reflm "Raw" =

1031 do fnN' <- reifyTTName fnN

1032 clauses' <- case unList clauses of

1033 Nothing -> fail $ "Couldn't reify " ++ show clauses ++ " as a clause list"

1034 Just cs -> mapM reifyC cs

1035 return $ RDefineFun fnN' clauses'

1036− where reifyC :: Term -> ElabD RFunClause

1036+ where reifyC :: Term -> ElabD (RFunClause Raw)

1037− reifyC (App _ (App _ (P (DCon _ _ _) n _) lhs) rhs)

1037+ reifyC (App _ (App _ (App _ (P (DCon _ _ _) n _) (P _ t _)) lhs) rhs)

1038− | n == tacN "MkFunClause" = liftM2 RMkFunClause

1038+ | n == tacN "MkFunClause" && t == reflm "Raw" = liftM2 RMkFunClause

1039 (reifyRaw lhs)

1040 (reifyRaw rhs)

1041− reifyC (App _ (P (DCon _ _ _) n _) lhs)

1041+ reifyC (App _ (App _ (P (DCon _ _ _) n _) (P _ t _)) lhs)

1042− | n == tacN "MkImpossibleClause" = fmap RMkImpossibleClause $ reifyRaw lhs

1042+ | n == tacN "MkImpossibleClause" && t == reflm "Raw" = fmap RMkImpossibleClause $ reifyRaw lhs

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

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

1045

@@ -1078,37 +1078,19 @@ unApplyRaw tm = ua [] tm

1078

1079-- | Build the reflected function definition(s) that correspond(s) to

1080-- a provided unqualifed name

1081−buildFunDefns :: IState -> Name -> [RFunDefn]

1081+buildFunDefns :: IState -> Name -> [RFunDefn Term]

1082buildFunDefns ist n =

1083 [ mkFunDefn name clauses

1084 | (name, (clauses, _)) <- lookupCtxtName n $ idris_patdefs ist

1085 ]

1086+

1086− where mkFunDefn name clauses = RDefineFun name (map (mkFunClause name) clauses)

1087+ where mkFunDefn name clauses = RDefineFun name (map mkFunClause clauses)

1087−

1088+

1088− mkFunClause :: Name -> ([Name], Term, Term) -> RFunClause

1089− mkFunClause _ ([], lhs, Impossible) = RMkImpossibleClause (forget lhs)

1089+ mkFunClause ([], lhs, Impossible) = RMkImpossibleClause lhs

1090− mkFunClause _ ([], lhs, rhs) = RMkFunClause (forget lhs) (forget rhs)

1090+ mkFunClause ([], lhs, rhs) = RMkFunClause lhs rhs

1091− mkFunClause name ((n : ns), lhs, rhs) = mkFunClause name (ns, lhs', rhs') where

1091+ mkFunClause ((n : ns), lhs, rhs) = mkFunClause (ns, bind lhs, bind rhs) where

1092− (lhs', ty) = case (runState (subst 0 lhs) Nothing) of

1092+ bind Impossible = Impossible

1093− (_, Nothing) -> error $ "Patvar " ++ show n ++ " not bound on the LHS of " ++ show name

1094− (tm', Just ty) -> (Bind n (PVar ty) tm', ty)

1095−

1096− rhs' = case (runState (subst 0 rhs) (Just ty)) of

1097− (tm', _) -> Bind n (PVar ty) tm'

1093+ bind tm = Bind n (PVar Erased) tm

1098−

1099− subst :: Int -> Term -> State (Maybe Term) Term

1100− subst i (P nt n' ty) | n' == n && nt == Bound = put (Just ty) >> return (V i)

1101− | otherwise = subst i ty >>= return . P nt n'

1102− subst i t@(Bind n' b sc) | n == n = return t -- The name is shadowed, so we won't find it here

1103− | otherwise = do b' <- mapM (subst i) b

1104− sc' <- subst (i + 1) sc

1105− return $ Bind n' b' sc'

1106− subst i (App s f a) = do f' <- subst i f

1107− a' <- subst i a

1108− return $ App s f' a'

1109− subst i (Proj x idx) = do x' <- subst i x

1110− return $ Proj x' idx

1111− subst i t = return t

1112

1094

1113-- | Build the reflected datatype definition(s) that correspond(s) to

1095-- | Build the reflected datatype definition(s) that correspond(s) to

1114-- a provided unqualified name

1096-- a provided unqualified name

@@ -1200,9 +1182,12 @@ reflectDatatype (RDatatype tyn tyConArgs tyConRes constrs) =

1200 reflectConArg (RIndex a) =

1182 reflectConArg (RIndex a) =

1201 RApp (Var $ tacN "TyConIndex") (reflectArg a)

1183 RApp (Var $ tacN "TyConIndex") (reflectArg a)

1202

1184

1203−reflectFunClause :: RFunClause -> Raw

1185+reflectFunClause :: RFunClause Term -> Raw

1204−reflectFunClause (RMkFunClause lhs rhs) = raw_apply (Var $ tacN "MkFunClause") [ lhs, rhs ]

1186+reflectFunClause (RMkFunClause lhs rhs) = raw_apply (Var $ tacN "MkFunClause") $ (Var $ reflm "TT") : map reflect [ lhs, rhs ]

1205−reflectFunClause (RMkImpossibleClause lhs) = RApp (Var $ tacN "MkImpossibleClause") lhs

1187+reflectFunClause (RMkImpossibleClause lhs) = raw_apply (Var $ tacN "MkImpossibleClause") $ [ Var $ reflm "TT", reflect lhs ]

1206

1188

1207−reflectFunDefn :: RFunDefn -> Raw

1189+reflectFunDefn :: RFunDefn Term -> Raw

1208−reflectFunDefn (RDefineFun name clauses) = raw_apply (Var $ tacN "DefineFun") [reflectName name, rawList (Var $ tacN "FunClause") (map reflectFunClause clauses)]

1190+reflectFunDefn (RDefineFun name clauses) = raw_apply (Var $ tacN "DefineFun") [ Var $ reflm "TT"

1191+ , reflectName name

1192+ , rawList (RApp (Var $ tacN "FunClause") (Var $ reflm "TT")) (map reflectFunClause clauses)

1193+ ]

test/meta001/Finite.idr+13−13

@@ -29,7 +29,7 @@ mkFin (S k) (S j) = do i <- mkFin k j

30mkToClause : TTName -> (size, i : Nat) ->

31 (constr : (TTName, List CtorArg, Raw)) ->

32− Elab FunClause

32+ Elab (FunClause Raw)

33mkToClause fn size i (n, [], Var ty) =

34 MkFunClause (RApp (Var fn) (Var n)) <$> mkFin size i

35mkToClause fn size i (n, _, ty) =

@@ -38,14 +38,14 @@ mkToClause fn size i (n, _, ty) =

39mkFromClause : TTName -> (size, i : Nat) ->

40 (constr : (TTName, List CtorArg, Raw)) ->

41− Elab FunClause

41+ Elab (FunClause Raw)

42mkFromClause fn size i (n, [], Var ty) =

43 return $ MkFunClause (RApp (Var fn) !(mkFin size i)) (Var n)

44mkFromClause fn size i (n, _, ty) =

45 fail [TextPart "unsupported constructor", NamePart n]

48−mkOk1Clause : TTName -> (size, i : Nat) -> (constr : (TTName, List CtorArg, Raw)) -> Elab FunClause

48+mkOk1Clause : TTName -> (size, i : Nat) -> (constr : (TTName, List CtorArg, Raw)) -> Elab (FunClause Raw)

49mkOk1Clause fn size i (n, [], Var ty) =

50 return $ MkFunClause (RApp (Var fn) (Var n))

51 [| (Var (UN "Refl")) (Var ty) (Var n) |]

@@ -53,7 +53,7 @@ mkOk1Clause fn size i (n, _, ty) =

53 fail [TextPart "unsupported constructor", NamePart n]

56−mkOk2Clause : TTName -> (size, i : Nat) -> (constr : (TTName, List CtorArg, Raw)) -> Elab FunClause

56+mkOk2Clause : TTName -> (size, i : Nat) -> (constr : (TTName, List CtorArg, Raw)) -> Elab (FunClause Raw)

57mkOk2Clause fn size i (n, [], Var ty) =

58 return $ MkFunClause (RApp (Var fn) !(mkFin size i))

59 [| (Var "Refl") `(Fin ~(quote size))

@@ -62,9 +62,9 @@ mkOk2Clause fn size i (n, _, ty) =

62 fail [TextPart "unsupported constructor", NamePart n]

65−mkToClauses : TTName -> Nat -> List (TTName, List CtorArg, Raw) -> Elab (List FunClause)

65+mkToClauses : TTName -> Nat -> List (TTName, List CtorArg, Raw) -> Elab (List (FunClause Raw))

66mkToClauses fn size xs = mkToClauses' Z xs

67− where mkToClauses' : Nat -> List (TTName, List CtorArg, Raw) -> Elab (List FunClause)

67+ where mkToClauses' : Nat -> List (TTName, List CtorArg, Raw) -> Elab (List (FunClause Raw))

68 mkToClauses' k [] = return []

69 mkToClauses' k (x :: xs) = do rest <- mkToClauses' (S k) xs

70 clause <- mkToClause fn size k x

@@ -76,7 +76,7 @@ mkToClauses fn size xs = mkToClauses' Z xs

76||| This is to satisfy the totality checker, because `impossible`

77||| clauses are still

78mkAbsurdFinClause : (fn : TTName) -> (goal : Raw -> Raw) -> (size : Nat) ->

79− Elab FunClause

79+ Elab (FunClause Raw)

80mkAbsurdFinClause fn goal size =

81 do pv <- gensym "badfin"

82 lhsArg <- lhsBody pv size

@@ -92,26 +92,26 @@ mkAbsurdFinClause fn goal size =

94mkFromClauses : TTName -> TTName -> Nat ->

95− List (TTName, List CtorArg, Raw) -> Elab (List FunClause)

95+ List (TTName, List CtorArg, Raw) -> Elab (List (FunClause Raw))

96mkFromClauses fn ty size xs = mkFromClauses' Z xs

97− where mkFromClauses' : Nat -> List (TTName, List CtorArg, Raw) -> Elab (List FunClause)

97+ where mkFromClauses' : Nat -> List (TTName, List CtorArg, Raw) -> Elab (List (FunClause Raw))

98 mkFromClauses' k [] =

99 return [!(mkAbsurdFinClause fn (const (Var ty)) size)]

100 mkFromClauses' k (x :: xs) = do rest <- mkFromClauses' (S k) xs

101 clause <- mkFromClause fn size k x

102 return $ clause :: rest

103

104−mkOk1Clauses : TTName -> Nat -> List (TTName, List CtorArg, Raw) -> Elab (List FunClause)

104+mkOk1Clauses : TTName -> Nat -> List (TTName, List CtorArg, Raw) -> Elab (List (FunClause Raw))

105mkOk1Clauses fn size xs = mkOk1Clauses' Z xs

106− where mkOk1Clauses' : Nat -> List (TTName, List CtorArg, Raw) -> Elab (List FunClause)

106+ where mkOk1Clauses' : Nat -> List (TTName, List CtorArg, Raw) -> Elab (List (FunClause Raw))

107 mkOk1Clauses' k [] = return []

108 mkOk1Clauses' k (x :: xs) = do rest <- mkOk1Clauses' (S k) xs

109 clause <- mkOk1Clause fn size k x

110 return $ clause :: rest

111

112−mkOk2Clauses : TTName -> Nat -> List (TTName, List CtorArg, Raw) -> (Raw -> Raw) -> Elab (List FunClause)

112+mkOk2Clauses : TTName -> Nat -> List (TTName, List CtorArg, Raw) -> (Raw -> Raw) -> Elab (List (FunClause Raw))

113mkOk2Clauses fn size xs resTy = mkOk2Clauses' Z xs

114− where mkOk2Clauses' : Nat -> List (TTName, List CtorArg, Raw) -> Elab (List FunClause)

114+ where mkOk2Clauses' : Nat -> List (TTName, List CtorArg, Raw) -> Elab (List (FunClause Raw))

115 mkOk2Clauses' k [] = return [!(mkAbsurdFinClause fn resTy size)]

116 mkOk2Clauses' k (x :: xs) = do rest <- mkOk2Clauses' (S k) xs

117 clause <- mkOk2Clause fn size k x