git.iko.soy/Idris-dev
on master help sign in
Rename record fields in reflection

Now, there is more overloading, but we get simpler, more memorable names as a result.

commit1e687f3b5d73f68b99f78a16e7e3c5bb8f09853c authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateMon 12 Oct 2015, 20:05 (11 years ago) parent83ca4ae
5 files changed+40−38
compare with master
unifiedsplit
libs/prelude/Language/Reflection/Elab.idr+10−8 libs/pruviloj/Pruviloj/Derive/Eliminators.idr+9−9 libs/pruviloj/Pruviloj/Injective.idr+4−4 libs/pruviloj/Pruviloj/Internals.idr+6−6 libs/pruviloj/Pruviloj/Internals/TyConInfo.idr+11−11
libs/prelude/Language/Reflection/Elab.idr+10−8
@@ -37,8 +37,8 @@ data Plicity =
3737||| used for functions.
3838record FunArg where
3939 constructor MkFunArg
40− argName : TTName
41− argTy : Raw
40+ name : TTName
41+ type : Raw
4242 plicity : Plicity
4343 erasure : Erasure
4444
@@ -58,15 +58,17 @@ record TyDecl where
5858 constructor Declare
5959
6060 ||| The name of the function being declared.
61− tyDeclName : TTName
61+ name : TTName
6262
6363 ||| Each argument is in the scope of the names of previous arguments.
64− tyDeclArgs : List FunArg
64+ arguments : List FunArg
6565
6666 ||| The return type is in the scope of all the argument names.
67− tyDeclReturnTy : Raw
67+ returnType : Raw
6868
6969
70+-- Note: FunClause is not a record because impossible clauses may be
71+-- added at some point.
7072||| A single pattern-matching clause
7173data FunClause : Type where
7274 MkFunClause : (lhs, rhs : Raw) -> FunClause
@@ -74,8 +76,8 @@ data FunClause : Type where
7476||| A reflected function definition.
7577record FunDefn where
7678 constructor DefineFun
77− funDefnName : TTName
78− funDefnClauses : List FunClause
79+ name : TTName
80+ clauses : List FunClause
7981
8082
8183data CtorArg = CtorParameter FunArg | CtorField FunArg
@@ -85,7 +87,7 @@ record Datatype where
8587 constructor MkDatatype
8688
8789 ||| The name of the type constructor
88− familyName : TTName
90+ name : TTName
8991
9092 ||| The arguments to the type constructor
9193 tyConArgs : List TyConArg
libs/pruviloj/Pruviloj/Derive/Eliminators.idr+9−9
@@ -86,10 +86,10 @@ elabMethodTy info motiveName [] res ctorApp =
8686 focus argH; fill ctorApp; solve
8787 solve
8888elabMethodTy 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)))
9090elabMethodTy info motiveName (CtorField arg :: args) res ctorApp =
91− do let n = argName arg
92− let t = argTy arg
91+ do let n = name arg
92+ let t = type arg
9393 attack; forall n t
9494 mkIh info motiveName n t (result info)
9595 elabMethodTy info motiveName args res (RApp ctorApp (Var n))
@@ -153,8 +153,8 @@ getElimClause info elimn methCount (cn, args, resTy) whichCon =
153153 for {b=()} args $ \arg =>
154154 case arg of
155155 CtorParameter _ => return ()
156− CtorField arg => do claim (argName arg) (argTy arg)
157− unfocus (argName arg)
156+ CtorField arg => do claim (name arg) (type arg)
157+ unfocus (name arg)
158158
159159 -- Establish a hole for the scrutinee (infer type)
160160 scrutinee <- newHole "scrutinee" resTy
@@ -177,8 +177,8 @@ getElimClause info elimn methCount (cn, args, resTy) whichCon =
177177 focus scrutinee
178178 apply (mkApp (Var cn) $
179179 map (\x => case x of
180− CtorParameter param => Var (argName param)
181− CtorField arg => Var (argName arg))
180+ CtorParameter param => Var (name param)
181+ CtorField arg => Var (name arg))
182182 args)
183183 []
184184 solve)
@@ -195,8 +195,8 @@ getElimClause info elimn methCount (cn, args, resTy) whichCon =
195195 case x of
196196 CtorParameter _ => return List.Nil
197197 CtorField arg =>
198− do let n = argName arg
199− let t = argTy arg
198+ do let n = name arg
199+ let t = type arg
200200 (argArgs, argRes) <- stealBindings t (const Nothing)
201201 if headsMatch argRes (result info) --recursive
202202 then return [ NormalArgument n
libs/pruviloj/Pruviloj/Injective.idr+4−4
@@ -43,10 +43,10 @@ getInjectivity cn = exists <|> declare
4343 let res = foldr (\t1, t2 => RApp (RApp (Var `{Pair}) t1) t2)
4444 `(() : Type)
4545 (map (\(a1, a2) =>
46− `((=) {A=~(argTy a1)}
47− {B=~(argTy a2)}
48− ~(Var (argName a1))
49− ~(Var (argName a2))))
46+ `((=) {A=~(type a1)}
47+ {B=~(type a2)}
48+ ~(Var (name a1))
49+ ~(Var (name a2))))
5050 (zip impls1 impls2))
5151
5252 declareType $ Declare fn (impls1 ++ impls2 ++
libs/pruviloj/Pruviloj/Internals.idr+6−6
@@ -9,20 +9,20 @@ import Data.Vect
99
1010||| Get the name of a reflected type constructor argument.
1111tyConArgName : TyConArg -> TTName
12−tyConArgName (TyConParameter a) = argName a
13−tyConArgName (TyConIndex a) = argName a
12+tyConArgName (TyConParameter a) = name a
13+tyConArgName (TyConIndex a) = name a
1414
1515||| Modify the name of a reflected type constructor argument.
1616setTyConArgName : TyConArg -> TTName -> TyConArg
17−setTyConArgName (TyConParameter a) n = TyConParameter (record {argName = n} a)
18−setTyConArgName (TyConIndex a) n = TyConIndex (record {argName = n} a)
17+setTyConArgName (TyConParameter a) n = TyConParameter (record {name = n} a)
18+setTyConArgName (TyConIndex a) n = TyConIndex (record {name = n} a)
1919
2020||| Modify the type of a reflected type constructor argument using some function.
2121updateTyConArgTy : (Raw -> Raw) -> TyConArg -> TyConArg
2222updateTyConArgTy f (TyConParameter a) =
23− TyConParameter (record {argTy = f (argTy a) } a)
23+ TyConParameter (record {type = f (type a) } a)
2424updateTyConArgTy f (TyConIndex a) =
25− TyConIndex (record {argTy = f (argTy a) } a)
25+ TyConIndex (record {type = f (type a) } a)
2626
2727unApply : Raw -> (Raw, List Raw)
2828unApply tm = unApply' tm []
libs/pruviloj/Pruviloj/Internals/TyConInfo.idr+11−11
@@ -23,13 +23,13 @@ record TyConInfo where
2323getParams : TyConInfo -> List (TTName, Raw)
2424getParams info = mapMaybe param (args info)
2525 where param : TyConArg -> Maybe (TTName, Raw)
26− param (TyConParameter a) = Just (argName a, argTy a)
26+ param (TyConParameter a) = Just (name a, type a)
2727 param _ = Nothing
2828
2929getIndices : TyConInfo -> List (TTName, Raw)
3030getIndices info = mapMaybe index (args info)
3131 where index : TyConArg -> Maybe (TTName, Raw)
32− index (TyConIndex a) = Just (argName a, argTy a)
32+ index (TyConIndex a) = Just (name a, type a)
3333 index _ = Nothing
3434
3535||| Rename a bound variable across a telescope
@@ -75,7 +75,7 @@ processCtorArgs info (cn, cargs, resTy) =
7575 findParam : TTName -> List Raw -> List TyConArg -> Elab TTName
7676 findParam paramN (Var n :: args) (TyConParameter a :: tcArgs) =
7777 if n == paramN
78− then return (argName a)
78+ then return (name a)
7979 else findParam paramN args tcArgs
8080 findParam paramN (_ :: args) (_ :: tcArgs) =
8181 findParam paramN args tcArgs
@@ -89,20 +89,20 @@ processCtorArgs info (cn, cargs, resTy) =
8989 TyConInfo -> Elab (List CtorArg, Raw)
9090 convert' subst [] ty info = return ([], alphaRaw subst ty)
9191 convert' subst (CtorField a :: args) ty info =
92− do n' <- nameFrom (argName a)
92+ do n' <- nameFrom (name a)
9393 let a' = record {
94− argName = n'
95− , argTy = alphaRaw subst (argTy a)
94+ name = n'
95+ , type = alphaRaw subst (type a)
9696 } a
97− let subst' = extend subst (argName a) n'
97+ let subst' = extend subst (name a) n'
9898 (args', ty') <- convert' subst' args ty info
9999 return (CtorField a' :: args', ty')
100100 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)
102102 let a' = record {
103− argName = n'
104− , argTy = alphaRaw subst (argTy a)
103+ name = n'
104+ , type = alphaRaw subst (type a)
105105 } a
106− let subst' = extend subst (argName a) n'
106+ let subst' = extend subst (name a) n'
107107 (args', ty') <- convert' subst' ctorArgs ty info
108108 return (CtorParameter a' :: args', ty')