git.iko.soy/Idris-dev
on master help sign in
Code simplifications in eliminator derivation
a4dbf1fDavid Raymond Christiansen
libs/pruviloj/Pruviloj/Derive/Eliminators.idr+4−10
compare with master
unifiedsplit
@@ -18,7 +18,7 @@ bindParams info = traverse_ (uncurry forall) (getParams info)
18||| rewrite an application of something to their designated global
18||| rewrite an application of something to their designated global
19||| names
19||| names
20bindIndices : TyConInfo -> Elab Renamer
20bindIndices : TyConInfo -> Elab Renamer
21−bindIndices info = bind' (getIndices info) (const Nothing)
21+bindIndices info = bind' (getIndices info) noRenames
22 where bind' : List (TTName, Raw) -> Renamer -> Elab Renamer
22 where bind' : List (TTName, Raw) -> Renamer -> Elab Renamer
23 bind' [] ren = return ren
23 bind' [] ren = return ren
24 bind' ((n, t) :: ixs) ren = do n' <- nameFrom n
24 bind' ((n, t) :: ixs) ren = do n' <- nameFrom n
@@ -54,7 +54,7 @@ headsMatch x y =
54||| Make an induction hypothesis if one is called for
54||| Make an induction hypothesis if one is called for
55mkIh : TyConInfo -> (motiveName : TTName) -> (recArg : TTName) -> (argty, fam : Raw) -> Elab ()
55mkIh : TyConInfo -> (motiveName : TTName) -> (recArg : TTName) -> (argty, fam : Raw) -> Elab ()
56mkIh info motiveName recArg argty fam =
56mkIh info motiveName recArg argty fam =
57− case !(stealBindings argty (const Nothing)) of
57+ case !(stealBindings argty noRenames) of
58 (argArgs, argRes) =>
58 (argArgs, argRes) =>
59 if headsMatch argRes fam
59 if headsMatch argRes fam
60 then do ih <- gensym "ih"
60 then do ih <- gensym "ih"
@@ -96,19 +96,13 @@ elabMethodTy info motiveName (CtorField arg :: args) res ctorApp =
96 solve
96 solve
97
97
98
98
99−
100−elabMethod : TyConInfo -> (motiveName, ctorN : TTName) -> List CtorArg -> Raw -> Elab ()
101−elabMethod info motiveName ctorN ctorArgs resTy =
102− do elabMethodTy info motiveName ctorArgs resTy (Var ctorN)
103−
104−
105||| Bind a method for a constructor
99||| Bind a method for a constructor
106bindMethod : TyConInfo -> (motiveName, cn : TTName) -> List CtorArg -> Raw -> Elab ()
100bindMethod : TyConInfo -> (motiveName, cn : TTName) -> List CtorArg -> Raw -> Elab ()
107bindMethod info motiveName cn cargs cty =
101bindMethod info motiveName cn cargs cty =
108 do n <- nameFrom cn
102 do n <- nameFrom cn
109 h <- newHole "methTy" `(Type)
103 h <- newHole "methTy" `(Type)
110 forall n (Var h)
104 forall n (Var h)
111− focus h; elabMethod info motiveName cn cargs cty
105+ focus h; elabMethodTy info motiveName cargs cty (Var cn)
112
106
113getElimTy : TyConInfo -> List (TTName, List CtorArg, Raw) -> Elab Raw
107getElimTy : TyConInfo -> List (TTName, List CtorArg, Raw) -> Elab Raw
114getElimTy info ctors =
108getElimTy info ctors =
@@ -197,7 +191,7 @@ getElimClause info elimn methCount (cn, args, resTy) whichCon =
197 CtorField arg =>
191 CtorField arg =>
198 do let n = name arg
192 do let n = name arg
199 let t = type arg
193 let t = type arg
200− (argArgs, argRes) <- stealBindings t (const Nothing)
194+ (argArgs, argRes) <- stealBindings t noRenames
201 if headsMatch argRes (result info) --recursive
195 if headsMatch argRes (result info) --recursive
202 then return [ NormalArgument n
196 then return [ NormalArgument n
203 , IHArgument n
197 , IHArgument n
libs/pruviloj/Pruviloj/Internals.idr+3−2
@@ -112,8 +112,9 @@ elabPatternClause lhs rhs =
112 focus patH
112 focus patH
113 lhs
113 lhs
114 -- Convert all remaining holes to pattern variables
114 -- Convert all remaining holes to pattern variables
115+ for_ {b=()} !getHoles $ \h =>
115− traverse_ {b=()} (\h => focus h *> patvar h) !getHoles
116+ do focus h; patvar h
116− (pvars, `(MkInfer ~rhsTy ~lhsTm)) <- extractBinders <$> (forget pat)
117+ (pvars, `(MkInfer ~rhsTy ~lhsTm)) <- extractBinders <$> forget pat
117 | fail [TextPart "Couldn't infer type of left-hand pattern"]
118 | fail [TextPart "Couldn't infer type of left-hand pattern"]
118 rhsTm <- runElab (bindPatTys pvars rhsTy) $
119 rhsTm <- runElab (bindPatTys pvars rhsTy) $
119 do -- Introduce all the pattern variables from the LHS
120 do -- Introduce all the pattern variables from the LHS