mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-09-11 16:05:51 +03:00
Tweak expression search heuristic
Search locals left to right, so that they are used as arguments in the same order by default in recursive calls.
This commit is contained in:
parent
14e9872f07
commit
84faedba50
@ -357,7 +357,10 @@ searchLocal : {auto c : Ref Ctxt Defs} ->
|
||||
Maybe RecData -> Core (List (Term vars))
|
||||
searchLocal fc rig opts env ty topty defining
|
||||
= do defs <- get Ctxt
|
||||
searchLocalWith fc rig opts env (getAllEnv fc [] env)
|
||||
-- Reverse the environment so we try the patterns left to right.
|
||||
-- This heuristic is just so arguments appear the same order in
|
||||
-- recursive calls
|
||||
searchLocalWith fc rig opts env (reverse (getAllEnv fc [] env))
|
||||
ty topty defining
|
||||
|
||||
searchType : {auto c : Ref Ctxt Defs} ->
|
||||
|
@ -12,6 +12,8 @@ my_uncurry : (a -> b -> c) -> (a, b) -> c
|
||||
|
||||
append : Vect n a -> Vect m a -> Vect (n + m) a
|
||||
|
||||
lappend : (1 xs : List a) -> (1 ys : List a) -> List a
|
||||
|
||||
zipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c
|
||||
|
||||
data Env : Vect n Type -> Type where
|
||||
|
@ -4,6 +4,8 @@ Main> my_curry f x y = f (x, y)
|
||||
Main> my_uncurry f x = f (fst x) (snd x)
|
||||
Main> append [] ys = ys
|
||||
append (x :: xs) ys = x :: append xs ys
|
||||
Main> lappend [] ys = ys
|
||||
lappend (x :: xs) ys = x :: lappend xs ys
|
||||
Main> zipWith f [] ys = []
|
||||
zipWith f (x :: xs) (y :: ys) = f x y :: zipWith f xs ys
|
||||
Main> lookup Here (ECons x es) = x
|
||||
|
@ -2,7 +2,8 @@
|
||||
:gd 9 my_curry
|
||||
:gd 11 my_uncurry
|
||||
:gd 13 append
|
||||
:gd 15 zipWith
|
||||
:gd 27 lookup
|
||||
:gd 15 lappend
|
||||
:gd 17 zipWith
|
||||
:gd 29 lookup
|
||||
:t my_uncurry
|
||||
:q
|
||||
|
Loading…
Reference in New Issue
Block a user