git.iko.soy/Idris-dev
on master help sign in
Add a reducing version of believe_me (be careful!)
commit67de7f79448cd3ed88d10c6896aa13deedce7270 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 1 Feb 2013, 12:30 (14 years ago) parent8f76315
5 files changed+14−9
compare with master
unifiedsplit
lib/Builtins.idr+4 lib/Prelude/Strings.idr+2−2 papers/impl-paper/hll.tex+4−5 src/Core/Typecheck.hs+3−1 src/Core/Unify.hs+1−1
lib/Builtins.idr+4
@@ -38,6 +38,10 @@ abstract
3838believe_me : a -> b -- compiled specially as id, use with care!
3939believe_me x = prim__believe_me _ _ x
4040
41+public -- reduces at compile time, use with extreme care!
42+really_believe_me : a -> b
43+really_believe_me x = prim__believe_me _ _ x
44+
4145namespace Builtins {
4246
4347id : a -> a
lib/Prelude/Strings.idr+2−2
@@ -25,8 +25,8 @@ strTail' x p = prim__strTail x
2525%assert_total
2626strM : (x : String) -> StrM x
2727strM x with (choose (not (x == "")))
28− strM x | (Left p) = believe_me $ StrCons (strHead' x p) (strTail' x p)
29− strM x | (Right p) = believe_me StrNil
28+ strM x | (Left p) = really_believe_me $ StrCons (strHead' x p) (strTail' x p)
29+ strM x | (Right p) = really_believe_me StrNil
3030
3131-- annoyingly, we need these assert_totals because StrCons doesn't have
3232-- a recursive argument, therefore the termination checker doesn't believe
papers/impl-paper/hll.tex+4−5
@@ -25,7 +25,7 @@ list of imports and a collection of definitions and declarations, for example:
2525
2626\begin{SaveVerbatim}{constprims}
2727
28−module main
28+module Main
2929
3030x : Int
3131x = 42
@@ -47,7 +47,7 @@ undecidable for languages with
4747dependent types.
4848
4949A module declaration also opens a \remph{namespace}. The fully qualified names
50−declared in this module are \texttt{main.x} and \texttt{main.main}.
50+declared in this module are \texttt{Main.x} and \texttt{Main.main}.
5151
5252
5353\subsection{Types and Functions}
@@ -66,8 +66,7 @@ data List a = Nil | (::) a (List a) -- Polymorphic lists
6666\useverb{natlist}
6767
6868\noindent
69−The above declarations are taken from the standard library. Unary natural
70−numbers can be either zero, or
69+Unary natural numbers can be either zero, or
7170the successor of another natural number (\texttt{S k}).
7271Lists can either be empty (\texttt{Nil})
7372or a value added to the front of another list (\texttt{x :: xs}).
@@ -166,7 +165,7 @@ reverse xs = revAcc [] xs where
166165Indentation is significant --- functions in the \texttt{where} block must be indented
167166further than the outer function.
168167
169−\textbf{Scope:}
168+\textbf{Remark (scope):}
170169Any names which are visible in the outer scope are also visible in the \texttt{where}
171170clause (unless they have been redefined, such as \texttt{xs} here).
172171\emph{However}, names which appear in the type are \emph{not} automatically
src/Core/Typecheck.hs+3−1
@@ -68,7 +68,9 @@ check' holes ctxt env top = chk env top where
6868 let fty' = case uniqueBinders (map fst env) (finalise fty) of
6969 ty@(Bind x (Pi s) t) -> ty
7070 _ -> uniqueBinders (map fst env)
71− $ hnf ctxt env fty
71+ $ case hnf ctxt env fty of
72+ ty@(Bind x (Pi s) t) -> ty
73+ _ -> normalise ctxt env fty
7274 case fty' of
7375 Bind x (Pi s) t ->
7476-- trace ("Converting " ++ show aty ++ " and " ++ show s ++
src/Core/Unify.hs+1−1
@@ -183,7 +183,7 @@ unify ctxt env topx topy injtc holes =
183183 unArgs vs xs ys
184184
185185 metavarApp tm = let (f, args) = unApply tm in
186− all metavar (f : args)
186+ all (\x -> metavar x || notFn x) (f : args)
187187 metavar t = case t of
188188 P _ x _ -> x `elem` holes || holeIn env x
189189 _ -> False