git.iko.soy/Idris-dev
on master help sign in
Code simplifications in eliminator derivation
commita4dbf1f2df26ad92d0ec62f575a261e3243efe34 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateMon 19 Oct 2015, 01:05 (11 years ago) parent5f9e595
2 files changed+7−12
compare with master
unifiedsplit
libs/pruviloj/Pruviloj/Derive/Eliminators.idr+4−10 libs/pruviloj/Pruviloj/Internals.idr+3−2
libs/pruviloj/Pruviloj/Derive/Eliminators.idr+4−10
@@ -18,7 +18,7 @@ bindParams info = traverse_ (uncurry forall) (getParams info)
1818||| rewrite an application of something to their designated global
1919||| names
2020bindIndices : TyConInfo -> Elab Renamer
21−bindIndices info = bind' (getIndices info) (const Nothing)
21+bindIndices info = bind' (getIndices info) noRenames
2222 where bind' : List (TTName, Raw) -> Renamer -> Elab Renamer
2323 bind' [] ren = return ren
2424 bind' ((n, t) :: ixs) ren = do n' <- nameFrom n
@@ -54,7 +54,7 @@ headsMatch x y =
5454||| Make an induction hypothesis if one is called for
5555mkIh : TyConInfo -> (motiveName : TTName) -> (recArg : TTName) -> (argty, fam : Raw) -> Elab ()
5656mkIh info motiveName recArg argty fam =
57− case !(stealBindings argty (const Nothing)) of
57+ case !(stealBindings argty noRenames) of
5858 (argArgs, argRes) =>
5959 if headsMatch argRes fam
6060 then do ih <- gensym "ih"
@@ -96,19 +96,13 @@ elabMethodTy info motiveName (CtorField arg :: args) res ctorApp =
9696 solve
9797
9898
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−
10599||| Bind a method for a constructor
106100bindMethod : TyConInfo -> (motiveName, cn : TTName) -> List CtorArg -> Raw -> Elab ()
107101bindMethod info motiveName cn cargs cty =
108102 do n <- nameFrom cn
109103 h <- newHole "methTy" `(Type)
110104 forall n (Var h)
111− focus h; elabMethod info motiveName cn cargs cty
105+ focus h; elabMethodTy info motiveName cargs cty (Var cn)
112106
113107getElimTy : TyConInfo -> List (TTName, List CtorArg, Raw) -> Elab Raw
114108getElimTy info ctors =
@@ -197,7 +191,7 @@ getElimClause info elimn methCount (cn, args, resTy) whichCon =
197191 CtorField arg =>
198192 do let n = name arg
199193 let t = type arg
200− (argArgs, argRes) <- stealBindings t (const Nothing)
194+ (argArgs, argRes) <- stealBindings t noRenames
201195 if headsMatch argRes (result info) --recursive
202196 then return [ NormalArgument n
203197 , IHArgument n
libs/pruviloj/Pruviloj/Internals.idr+3−2
@@ -112,8 +112,9 @@ elabPatternClause lhs rhs =
112112 focus patH
113113 lhs
114114 -- Convert all remaining holes to pattern variables
115− traverse_ {b=()} (\h => focus h *> patvar h) !getHoles
116− (pvars, `(MkInfer ~rhsTy ~lhsTm)) <- extractBinders <$> (forget pat)
115+ for_ {b=()} !getHoles $ \h =>
116+ do focus h; patvar h
117+ (pvars, `(MkInfer ~rhsTy ~lhsTm)) <- extractBinders <$> forget pat
117118 | fail [TextPart "Couldn't infer type of left-hand pattern"]
118119 rhsTm <- runElab (bindPatTys pvars rhsTy) $
119120 do -- Introduce all the pattern variables from the LHS