git.iko.soy/Idris-dev
on master help sign in
Add views for recursion over Int/Integer
f2ab362Edwin Brady
libs/base/Data/Primitives/Views.idr+26
compare with master
unifiedsplit
@@ -24,6 +24,19 @@ namespace Integer
24 believe_me (DivBy {d} {div = dividend} {rem = remainder}
24 believe_me (DivBy {d} {div = dividend} {rem = remainder}
25 (believe_me (Refl {x = True})))
25 (believe_me (Refl {x = True})))
26
26
27+ ||| View for recursion over Integers
28+ data IntegerRec : Integer -> Type where
29+ IntegerZ : IntegerRec 0
30+ IntegerSucc : IntegerRec (n - 1) -> IntegerRec n
31+ IntegerPred : IntegerRec ((-n) + 1) -> IntegerRec (-n)
32+
33+ ||| Covering function for `IntegerRec`
34+ integerRec : (x : Integer) -> IntegerRec x
35+ integerRec 0 = IntegerZ
36+ integerRec x = if x > 0 then IntegerSucc (assert_total (integerRec (x - 1)))
37+ else believe_me (IntegerPred {n=-x}
38+ (assert_total (believe_me (integerRec (x + 1)))))
39+
27namespace Int
40namespace Int
28 ||| View for expressing a number as a multiplication + a remainder
41 ||| View for expressing a number as a multiplication + a remainder
29 public export
42 public export
@@ -47,3 +60,16 @@ namespace Int
47 believe_me (DivBy {d} {div = dividend} {rem = remainder}
60 believe_me (DivBy {d} {div = dividend} {rem = remainder}
48 (believe_me (Refl {x = True})))
61 (believe_me (Refl {x = True})))
49
62
63+ ||| View for recursion over Ints
64+ data IntRec : Int -> Type where
65+ IntZ : IntRec 0
66+ IntSucc : IntRec (n - 1) -> IntRec n
67+ IntPred : IntRec ((-n) + 1) -> IntRec (-n)
68+
69+ ||| Covering function for `IntRec`
70+ intRec : (x : Int) -> IntRec x
71+ intRec 0 = IntZ
72+ intRec x = if x > 0 then IntSucc (assert_total (intRec (x - 1)))
73+ else believe_me (IntPred {n=-x}
74+ (assert_total (believe_me (intRec (x + 1)))))
75+
src/Idris/Elab/Clause.hs+11−2
@@ -1041,9 +1041,18 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)
1041
1041
1042 lhs_arity = arity toplhs
1042 lhs_arity = arity toplhs
1043
1043
1044+ currentFn fname (PAlternative _ _ as)
1045+ | Just tm <- getApp as = tm
1046+ where getApp (tm@(PApp _ (PRef _ _ f) _) : as)
1047+ | f == fname = Just tm
1048+ getApp (_ : as) = getApp as
1049+ getApp [] = Nothing
1050+ currentFn _ tm = tm
1051+
1044− updateApp wtm@(PWithApp fcw tm warg) =
1052+ updateApp wtm@(PWithApp fcw tm_in warg) =
1053+ let tm = currentFn fname tm_in in
1045 case matchClause ist toplhs tm of
1054 case matchClause ist toplhs tm of
1046− Left _ -> PElabError (Msg (show fc ++ ":with application does not match top level"))
1055+ Left _ -> PElabError (Msg (show fc ++ ":with application does not match top level "))
1047 Right mvars ->
1056 Right mvars ->
1048 let ns = map (keepMvar (map fst mvars) fcw) ns_in
1057 let ns = map (keepMvar (map fst mvars) fcw) ns_in
1049 ns' = map (keepMvar (map fst mvars) fcw) ns_in'
1058 ns' = map (keepMvar (map fst mvars) fcw) ns_in'