67de7f7 · Idris-dev · git.iko.soy

lib/Builtins.idr+4

compare with master

unifiedsplit

@@ -38,6 +38,10 @@ abstract

38believe_me : a -> b -- compiled specially as id, use with care!

39believe_me x = prim__believe_me _ _ x

40

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+

41namespace Builtins {

45namespace Builtins {

42

46

43id : a -> a

47id : a -> a

lib/Prelude/Strings.idr+2−2

@@ -25,8 +25,8 @@ strTail' x p = prim__strTail x

25%assert_total

26strM : (x : String) -> StrM x

27strM x with (choose (not (x == "")))

28− strM x | (Left p) = believe_me $ StrCons (strHead' x p) (strTail' x p)

28+ strM x | (Left p) = really_believe_me $ StrCons (strHead' x p) (strTail' x p)

29− strM x | (Right p) = believe_me StrNil

29+ strM x | (Right p) = really_believe_me StrNil

30

31-- annoyingly, we need these assert_totals because StrCons doesn't have

32-- 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:

25

26\begin{SaveVerbatim}{constprims}

27

28−module main

28+module Main

29

30x : Int

31x = 42

@@ -47,7 +47,7 @@ undecidable for languages with

47dependent types.

48

49A 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}.

51

52

53\subsection{Types and Functions}

@@ -66,8 +66,7 @@ data List a = Nil | (::) a (List a) -- Polymorphic lists

66\useverb{natlist}

67

68\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

71the successor of another natural number (\texttt{S k}).

70the successor of another natural number (\texttt{S k}).

72Lists can either be empty (\texttt{Nil})

71Lists can either be empty (\texttt{Nil})

73or a value added to the front of another list (\texttt{x :: xs}).

72or a value added to the front of another list (\texttt{x :: xs}).

@@ -166,7 +165,7 @@ reverse xs = revAcc [] xs where

166Indentation is significant --- functions in the \texttt{where} block must be indented

165Indentation is significant --- functions in the \texttt{where} block must be indented

167further than the outer function.

166further than the outer function.

168

167

169−\textbf{Scope:}

168+\textbf{Remark (scope):}

170Any names which are visible in the outer scope are also visible in the \texttt{where}

169Any names which are visible in the outer scope are also visible in the \texttt{where}

171clause (unless they have been redefined, such as \texttt{xs} here).

170clause (unless they have been redefined, such as \texttt{xs} here).

172\emph{However}, names which appear in the type are \emph{not} automatically

171\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

68 let fty' = case uniqueBinders (map fst env) (finalise fty) of

69 ty@(Bind x (Pi s) t) -> ty

70 _ -> 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

72 case fty' of

74 case fty' of

73 Bind x (Pi s) t ->

75 Bind x (Pi s) t ->

74-- trace ("Converting " ++ show aty ++ " and " ++ show s ++

76-- trace ("Converting " ++ show aty ++ " and " ++ show s ++

src/Core/Unify.hs+1−1

@@ -183,7 +183,7 @@ unify ctxt env topx topy injtc holes =

183 unArgs vs xs ys

184

185 metavarApp tm = let (f, args) = unApply tm in

186− all metavar (f : args)

186+ all (\x -> metavar x || notFn x) (f : args)

187 metavar t = case t of

188 P _ x _ -> x `elem` holes || holeIn env x

189 _ -> False