39d643b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge branch 'elab-lookup-function-def' of https://github.com/shlevy/Idris-dev into shlevy-elab-lookup-function-def

commit39d643baa9610886fb498329e874b4093366fddb authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateWed 2 Dec 2015, 01:46 (11 years ago) parentfe2dc3d 5eaf49c

11 files changed+118−40

compare with master

unifiedsplit

idris.cabal+3 libs/prelude/Language/Reflection/Elab.idr+21−8 libs/pruviloj/Pruviloj/Derive/DecEq.idr+1−1 libs/pruviloj/Pruviloj/Derive/Eliminators.idr+3−3 libs/pruviloj/Pruviloj/Internals.idr+1−1 src/Idris/Elab/Term.hs+6−1 src/Idris/Reflection.hs+41−13 test/meta001/Finite.idr+13−13 test/meta004/expected test/meta004/meta004.idr+26 test/meta004/run+3

idris.cabal+3

@@ -571,6 +571,9 @@ Extra-source-files:

571571 test/meta002/run

572572 test/meta002/*.idr

573573 test/meta002/expected

574+ test/meta004/run

575+ test/meta004/*.idr

576+ test/meta004/expected

574577

575578 test/primitives001/run

576579 test/primitives001/*.idr

libs/prelude/Language/Reflection/Elab.idr+21−8

@@ -69,17 +69,16 @@ record TyDecl where

6969 returnType : Raw

7070

7171

72−-- Note: FunClause is not a record because impossible clauses may be

73−-- added at some point.

7472||| A single pattern-matching clause

75−data FunClause : Type where

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

73+data FunClause : Type -> Type where

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

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

7776

7877||| A reflected function definition.

79−record FunDefn where

78+record FunDefn a where

8079 constructor DefineFun

8180 name : TTName

82− clauses : List FunClause

81+ clauses : List (FunClause a)

8382

8483

8584data CtorArg = CtorParameter FunArg | CtorField FunArg

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

116115 Prim__Guess : Elab TT

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

118117 Prim__LookupDatatype : TTName -> Elab (List Datatype)

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

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

120120

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

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

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

149149

150150 Prim__DeclareType : TyDecl -> Elab ()

151− Prim__DefineFunction : FunDefn -> Elab ()

151+ Prim__DefineFunction : FunDefn Raw -> Elab ()

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

153153 Prim__IsTCName : TTName -> Elab Bool

154154

@@ -231,6 +231,19 @@ namespace Tactics

231231 [] => fail [TextPart "No datatype named", NamePart n]

232232 xs => fail [TextPart "More than one datatype named", NamePart n]

233233

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

235+ ||| are overloadings of some name.

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

243+ lookupFunDefnExact n = case !(lookupFunDefn n) of

244+ [res] => return res

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

246+ xs => fail [TextPart "More than one function named", NamePart n]

234247

235248 ||| Get the argument specification for each overloading of a name.

236249 lookupArgs : TTName -> Elab (List (TTName, List FunArg, Raw))

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

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

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

454467 ||| `declareType`.

455− defineFunction : FunDefn -> Elab ()

468+ defineFunction : FunDefn Raw -> Elab ()

456469 defineFunction defun = Prim__DefineFunction defun

457470

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

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

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

181181 Nothing => return False

182182

183183 partial -- mkRhs

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

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

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

186186 perhaps $ elabPatternClause

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

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

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

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

135135

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

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

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

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

139139 elabPatternClause

140140 (do -- Establish a hole for each parameter

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

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

243243

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

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

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

246246getElimClauses info elimn ctors =

247247 let methodCount = length ctors

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

249249 (enumerate ctors)

250250

251−instance Show FunClause where

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

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

253253

254254abstract

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

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

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

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

103103partial

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

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

105105elabPatternClause lhs rhs =

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

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

src/Idris/Elab/Term.hs+6−1

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

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

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

17841784

1785− defineFunction :: RFunDefn -> ElabD ()

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

17861786 defineFunction (RDefineFun n clauses) =

17871787 do ctxt <- get_context

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

@@ -1874,6 +1874,11 @@ runElabAction ist fc env tm ns = do tm' <- eval tm

18741874 fmap fst . checkClosed $

18751875 rawList (Var (tacN "Datatype"))

18761876 (map reflectDatatype (buildDatatypes ist n'))

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

1878+ = do n' <- reifyTTName name

1879+ fmap fst . checkClosed $

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

1881+ (map reflectFunDefn (buildFunDefns ist n'))

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

18781883 = do n' <- reifyTTName name

18791884 let listTy = Var (sNS (sUN "List") ["List", "Prelude"])

src/Idris/Reflection.hs+41−13

@@ -7,6 +7,8 @@ module Idris.Reflection where

88#if __GLASGOW_HASKELL__ < 710

99import Control.Applicative ((<$>), (<*>), pure)

10+import Prelude hiding (mapM)

11+import Data.Traversable (mapM)

1012#endif

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

1214import Control.Monad.State.Strict (lift)

@@ -19,7 +21,7 @@ import Idris.Core.Elaborate (claim, fill, focus, getNameFrom, initElaborator,

1921import Idris.Core.Evaluate (Def(TyDecl), initContext, lookupDefExact, lookupTyExact)

2022import Idris.Core.TT

2123

22−import Idris.AbsSyntaxTree (ArgOpt(..),ElabD, IState(tt_ctxt, idris_implicits,idris_datatypes),

24+import Idris.AbsSyntaxTree (ArgOpt(..),ElabD, IState(tt_ctxt, idris_implicits,idris_datatypes, idris_patdefs),

2325 PArg'(..), PArg, PTactic, PTactic'(..), PTerm(..), Fixity (..),

2426 initEState, pairCon, pairTy)

2527import Idris.Delaborate (delab)

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

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

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

5759

58−data RFunClause = RMkFunClause Raw Raw

59− | RMkImpossibleClause Raw

60− deriving Show

60+data RFunClause a = RMkFunClause a a

61+ | RMkImpossibleClause a

62+ deriving Show

6163

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

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

6365

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

6567reflm :: String -> Name

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

10231025 return $ RDeclare tyN' args' ret'

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

10251027

1026−reifyFunDefn :: Term -> ElabD RFunDefn

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

1028− | n == tacN "DefineFun" =

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

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

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

10291031 do fnN' <- reifyTTName fnN

10301032 clauses' <- case unList clauses of

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

10321034 Just cs -> mapM reifyC cs

10331035 return $ RDefineFun fnN' clauses'

1034− where reifyC :: Term -> ElabD RFunClause

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

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

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

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

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

10371039 (reifyRaw lhs)

10381040 (reifyRaw rhs)

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

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

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

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

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

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

10431045

@@ -1074,6 +1076,22 @@ unApplyRaw tm = ua [] tm

10741076 ua args (RApp f a) = ua (a:args) f

10751077 ua args t = (t, args)

10761078

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

1080+-- a provided unqualifed name

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

1082+buildFunDefns ist n =

1083+ [ mkFunDefn name clauses

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

1085+ ]

1086+

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

1088+

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

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

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

1092+ bind Impossible = Impossible

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

1094+

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

10781096-- a provided unqualified name

10791097buildDatatypes :: IState -> Name -> [RDatatype]

@@ -1163,3 +1181,13 @@ reflectDatatype (RDatatype tyn tyConArgs tyConRes constrs) =

11631181 RApp (Var $ tacN "TyConParameter") (reflectArg a)

11641182 reflectConArg (RIndex a) =

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

1184+

1185+reflectFunClause :: RFunClause Term -> Raw

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

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

1188+

1189+reflectFunDefn :: RFunDefn Term -> Raw

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

2929

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

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

32− Elab FunClause

32+ Elab (FunClause Raw)

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

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

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

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

3838

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

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

41− Elab FunClause

41+ Elab (FunClause Raw)

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

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

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

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

4646

4747

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)

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

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

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

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

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

5454

5555

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)

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

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

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

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

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

6363

6464

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

6666mkToClauses 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))

6868 mkToClauses' k [] = return []

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

7070 clause <- mkToClause fn size k x

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

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

7777||| clauses are still

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

79− Elab FunClause

79+ Elab (FunClause Raw)

8080mkAbsurdFinClause fn goal size =

8181 do pv <- gensym "badfin"

8282 lhsArg <- lhsBody pv size

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

9292

9393

9494mkFromClauses : TTName -> TTName -> Nat ->

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

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

9696mkFromClauses 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))

9898 mkFromClauses' k [] =

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

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

101101 clause <- mkFromClause fn size k x

102102 return $ clause :: rest

103103

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

105105mkOk1Clauses 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))

107107 mkOk1Clauses' k [] = return []

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

109109 clause <- mkOk1Clause fn size k x

110110 return $ clause :: rest

111111

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

113113mkOk2Clauses 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))

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

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

117117 clause <- mkOk2Clause fn size k x

test/meta004/expectednew file

No changes to the content.

test/meta004/meta004.idrnew file+26

@@ -0,0 +1,26 @@

1+import Language.Reflection.Utils

2+import Pruviloj.Core

4+forgotToNatAndRename : TTName -> TTName -> Raw -> Raw

5+forgotToNatAndRename old new (RBind name b body) = RBind name (map (forgotToNatAndRename old new) b) (forgotToNatAndRename old new body)

6+forgotToNatAndRename old new (RApp f arg) = RApp (forgotToNatAndRename old new f) (forgotToNatAndRename old new arg)

7+forgotToNatAndRename old new (RConstant Forgot) = Var `{Nat}

8+forgotToNatAndRename old new (Var n) = if n == old then Var new else Var n

9+forgotToNatAndRename old new tm = tm

10+

11+roundtrip : TTName -> TTName -> Elab ()

12+roundtrip old new = do

13+ DefineFun _ clauses <- lookupFunDefnExact old

14+ clauses' <- for clauses (\(MkFunClause lhs rhs) => do

15+ lhs' <- forgotToNatAndRename old new <$> forget lhs

16+ rhs' <- forgotToNatAndRename old new <$> forget rhs

17+ pure $ MkFunClause lhs' rhs')

18+ defineFunction (DefineFun new clauses')

19+

20+plus' : Nat -> Nat -> Nat

21+%runElab (roundtrip `{plus} `{plus'})

22+

23+total

24+p : (a : Nat) -> (b : Nat) -> plus a b = plus' a b

25+p Z right = Refl

26+p (S left) right = Refl

test/meta004/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+idris $@ -p pruviloj --nocolour --check --consolewidth 70 meta004.idr

3+rm -f *.ibc