git.iko.soy/Idris-dev
on master help sign in
Rename record fields in reflection
1e687f3David Raymond Christiansen
libs/prelude/Language/Reflection/Elab.idr+10−8
compare with master
unifiedsplit
@@ -37,8 +37,8 @@ data Plicity =
37||| used for functions.
37||| used for functions.
38record FunArg where
38record FunArg where
39 constructor MkFunArg
39 constructor MkFunArg
40− argName : TTName
40+ name : TTName
41− argTy : Raw
41+ type : Raw
42 plicity : Plicity
42 plicity : Plicity
43 erasure : Erasure
43 erasure : Erasure
44
44
@@ -58,15 +58,17 @@ record TyDecl where
58 constructor Declare
58 constructor Declare
59
59
60 ||| The name of the function being declared.
60 ||| The name of the function being declared.
61− tyDeclName : TTName
61+ name : TTName
62
62
63 ||| Each argument is in the scope of the names of previous arguments.
63 ||| Each argument is in the scope of the names of previous arguments.
64− tyDeclArgs : List FunArg
64+ arguments : List FunArg
65
65
66 ||| The return type is in the scope of all the argument names.
66 ||| The return type is in the scope of all the argument names.
67− tyDeclReturnTy : Raw
67+ returnType : Raw
68
68
69
69
70+-- Note: FunClause is not a record because impossible clauses may be
71+-- added at some point.
70||| A single pattern-matching clause
72||| A single pattern-matching clause
71data FunClause : Type where
73data FunClause : Type where
72 MkFunClause : (lhs, rhs : Raw) -> FunClause
74 MkFunClause : (lhs, rhs : Raw) -> FunClause
@@ -74,8 +76,8 @@ data FunClause : Type where
74||| A reflected function definition.
76||| A reflected function definition.
75record FunDefn where
77record FunDefn where
76 constructor DefineFun
78 constructor DefineFun
77− funDefnName : TTName
79+ name : TTName
78− funDefnClauses : List FunClause
80+ clauses : List FunClause
79
81
80
82
81data CtorArg = CtorParameter FunArg | CtorField FunArg
83data CtorArg = CtorParameter FunArg | CtorField FunArg
@@ -85,7 +87,7 @@ record Datatype where
85 constructor MkDatatype
87 constructor MkDatatype
86
88
87 ||| The name of the type constructor
89 ||| The name of the type constructor
88− familyName : TTName
90+ name : TTName
89
91
90 ||| The arguments to the type constructor
92 ||| The arguments to the type constructor
91 tyConArgs : List TyConArg
93 tyConArgs : List TyConArg
libs/pruviloj/Pruviloj/Derive/Eliminators.idr+9−9
@@ -86,10 +86,10 @@ elabMethodTy info motiveName [] res ctorApp =
86 focus argH; fill ctorApp; solve
86 focus argH; fill ctorApp; solve
87 solve
87 solve
88elabMethodTy info motiveName (CtorParameter arg :: args) res ctorApp =
88elabMethodTy info motiveName (CtorParameter arg :: args) res ctorApp =
89− elabMethodTy info motiveName args res (RApp ctorApp (Var (argName arg)))
89+ elabMethodTy info motiveName args res (RApp ctorApp (Var (name arg)))
90elabMethodTy info motiveName (CtorField arg :: args) res ctorApp =
90elabMethodTy info motiveName (CtorField arg :: args) res ctorApp =
91− do let n = argName arg
91+ do let n = name arg
92− let t = argTy arg
92+ let t = type arg
93 attack; forall n t
93 attack; forall n t
94 mkIh info motiveName n t (result info)
94 mkIh info motiveName n t (result info)
95 elabMethodTy info motiveName args res (RApp ctorApp (Var n))
95 elabMethodTy info motiveName args res (RApp ctorApp (Var n))
@@ -153,8 +153,8 @@ getElimClause info elimn methCount (cn, args, resTy) whichCon =
153 for {b=()} args $ \arg =>
153 for {b=()} args $ \arg =>
154 case arg of
154 case arg of
155 CtorParameter _ => return ()
155 CtorParameter _ => return ()
156− CtorField arg => do claim (argName arg) (argTy arg)
156+ CtorField arg => do claim (name arg) (type arg)
157− unfocus (argName arg)
157+ unfocus (name arg)
158
158
159 -- Establish a hole for the scrutinee (infer type)
159 -- Establish a hole for the scrutinee (infer type)
160 scrutinee <- newHole "scrutinee" resTy
160 scrutinee <- newHole "scrutinee" resTy
@@ -177,8 +177,8 @@ getElimClause info elimn methCount (cn, args, resTy) whichCon =
177 focus scrutinee
177 focus scrutinee
178 apply (mkApp (Var cn) $
178 apply (mkApp (Var cn) $
179 map (\x => case x of
179 map (\x => case x of
180− CtorParameter param => Var (argName param)
180+ CtorParameter param => Var (name param)
181− CtorField arg => Var (argName arg))
181+ CtorField arg => Var (name arg))
182 args)
182 args)
183 []
183 []
184 solve)
184 solve)
@@ -195,8 +195,8 @@ getElimClause info elimn methCount (cn, args, resTy) whichCon =
195 case x of
195 case x of
196 CtorParameter _ => return List.Nil
196 CtorParameter _ => return List.Nil
197 CtorField arg =>
197 CtorField arg =>
198− do let n = argName arg
198+ do let n = name arg
199− let t = argTy arg
199+ let t = type arg
200 (argArgs, argRes) <- stealBindings t (const Nothing)
200 (argArgs, argRes) <- stealBindings t (const Nothing)
201 if headsMatch argRes (result info) --recursive
201 if headsMatch argRes (result info) --recursive
202 then return [ NormalArgument n
202 then return [ NormalArgument n
libs/pruviloj/Pruviloj/Injective.idr+4−4
@@ -43,10 +43,10 @@ getInjectivity cn = exists <|> declare
43 let res = foldr (\t1, t2 => RApp (RApp (Var `{Pair}) t1) t2)
43 let res = foldr (\t1, t2 => RApp (RApp (Var `{Pair}) t1) t2)
44 `(() : Type)
44 `(() : Type)
45 (map (\(a1, a2) =>
45 (map (\(a1, a2) =>
46− `((=) {A=~(argTy a1)}
46+ `((=) {A=~(type a1)}
47− {B=~(argTy a2)}
47+ {B=~(type a2)}
48− ~(Var (argName a1))
48+ ~(Var (name a1))
49− ~(Var (argName a2))))
49+ ~(Var (name a2))))
50 (zip impls1 impls2))
50 (zip impls1 impls2))
51
51
52 declareType $ Declare fn (impls1 ++ impls2 ++
52 declareType $ Declare fn (impls1 ++ impls2 ++
libs/pruviloj/Pruviloj/Internals.idr+6−6
@@ -9,20 +9,20 @@ import Data.Vect
9
9
10||| Get the name of a reflected type constructor argument.
10||| Get the name of a reflected type constructor argument.
11tyConArgName : TyConArg -> TTName
11tyConArgName : TyConArg -> TTName
12−tyConArgName (TyConParameter a) = argName a
12+tyConArgName (TyConParameter a) = name a
13−tyConArgName (TyConIndex a) = argName a
13+tyConArgName (TyConIndex a) = name a
14
14
15||| Modify the name of a reflected type constructor argument.
15||| Modify the name of a reflected type constructor argument.
16setTyConArgName : TyConArg -> TTName -> TyConArg
16setTyConArgName : TyConArg -> TTName -> TyConArg
17−setTyConArgName (TyConParameter a) n = TyConParameter (record {argName = n} a)
17+setTyConArgName (TyConParameter a) n = TyConParameter (record {name = n} a)
18−setTyConArgName (TyConIndex a) n = TyConIndex (record {argName = n} a)
18+setTyConArgName (TyConIndex a) n = TyConIndex (record {name = n} a)
19
19
20||| Modify the type of a reflected type constructor argument using some function.
20||| Modify the type of a reflected type constructor argument using some function.
21updateTyConArgTy : (Raw -> Raw) -> TyConArg -> TyConArg
21updateTyConArgTy : (Raw -> Raw) -> TyConArg -> TyConArg
22updateTyConArgTy f (TyConParameter a) =
22updateTyConArgTy f (TyConParameter a) =
23− TyConParameter (record {argTy = f (argTy a) } a)
23+ TyConParameter (record {type = f (type a) } a)
24updateTyConArgTy f (TyConIndex a) =
24updateTyConArgTy f (TyConIndex a) =
25− TyConIndex (record {argTy = f (argTy a) } a)
25+ TyConIndex (record {type = f (type a) } a)
26
26
27unApply : Raw -> (Raw, List Raw)
27unApply : Raw -> (Raw, List Raw)
28unApply tm = unApply' tm []
28unApply tm = unApply' tm []
libs/pruviloj/Pruviloj/Internals/TyConInfo.idr+11−11
@@ -23,13 +23,13 @@ record TyConInfo where
23getParams : TyConInfo -> List (TTName, Raw)
23getParams : TyConInfo -> List (TTName, Raw)
24getParams info = mapMaybe param (args info)
24getParams info = mapMaybe param (args info)
25 where param : TyConArg -> Maybe (TTName, Raw)
25 where param : TyConArg -> Maybe (TTName, Raw)
26− param (TyConParameter a) = Just (argName a, argTy a)
26+ param (TyConParameter a) = Just (name a, type a)
27 param _ = Nothing
27 param _ = Nothing
28
28
29getIndices : TyConInfo -> List (TTName, Raw)
29getIndices : TyConInfo -> List (TTName, Raw)
30getIndices info = mapMaybe index (args info)
30getIndices info = mapMaybe index (args info)
31 where index : TyConArg -> Maybe (TTName, Raw)
31 where index : TyConArg -> Maybe (TTName, Raw)
32− index (TyConIndex a) = Just (argName a, argTy a)
32+ index (TyConIndex a) = Just (name a, type a)
33 index _ = Nothing
33 index _ = Nothing
34
34
35||| Rename a bound variable across a telescope
35||| Rename a bound variable across a telescope
@@ -75,7 +75,7 @@ processCtorArgs info (cn, cargs, resTy) =
75 findParam : TTName -> List Raw -> List TyConArg -> Elab TTName
75 findParam : TTName -> List Raw -> List TyConArg -> Elab TTName
76 findParam paramN (Var n :: args) (TyConParameter a :: tcArgs) =
76 findParam paramN (Var n :: args) (TyConParameter a :: tcArgs) =
77 if n == paramN
77 if n == paramN
78− then return (argName a)
78+ then return (name a)
79 else findParam paramN args tcArgs
79 else findParam paramN args tcArgs
80 findParam paramN (_ :: args) (_ :: tcArgs) =
80 findParam paramN (_ :: args) (_ :: tcArgs) =
81 findParam paramN args tcArgs
81 findParam paramN args tcArgs
@@ -89,20 +89,20 @@ processCtorArgs info (cn, cargs, resTy) =
89 TyConInfo -> Elab (List CtorArg, Raw)
89 TyConInfo -> Elab (List CtorArg, Raw)
90 convert' subst [] ty info = return ([], alphaRaw subst ty)
90 convert' subst [] ty info = return ([], alphaRaw subst ty)
91 convert' subst (CtorField a :: args) ty info =
91 convert' subst (CtorField a :: args) ty info =
92− do n' <- nameFrom (argName a)
92+ do n' <- nameFrom (name a)
93 let a' = record {
93 let a' = record {
94− argName = n'
94+ name = n'
95− , argTy = alphaRaw subst (argTy a)
95+ , type = alphaRaw subst (type a)
96 } a
96 } a
97− let subst' = extend subst (argName a) n'
97+ let subst' = extend subst (name a) n'
98 (args', ty') <- convert' subst' args ty info
98 (args', ty') <- convert' subst' args ty info
99 return (CtorField a' :: args', ty')
99 return (CtorField a' :: args', ty')
100 convert' subst (CtorParameter a :: ctorArgs) ty info =
100 convert' subst (CtorParameter a :: ctorArgs) ty info =
101− do n' <- findParam (argName a) (snd (unApply ty)) (args info)
101+ do n' <- findParam (name a) (snd (unApply ty)) (args info)
102 let a' = record {
102 let a' = record {
103− argName = n'
103+ name = n'
104− , argTy = alphaRaw subst (argTy a)
104+ , type = alphaRaw subst (type a)
105 } a
105 } a
106− let subst' = extend subst (argName a) n'
106+ let subst' = extend subst (name a) n'
107 (args', ty') <- convert' subst' ctorArgs ty info
107 (args', ty') <- convert' subst' ctorArgs ty info
108 return (CtorParameter a' :: args', ty')
108 return (CtorParameter a' :: args', ty')