diff --git a/libs/prelude/Builtin.idr b/libs/prelude/Builtin.idr new file mode 100644 index 0000000..c5fba59 --- /dev/null +++ b/libs/prelude/Builtin.idr @@ -0,0 +1,89 @@ +module Builtin + +-- The most primitive data types; things which are used by desugaring + +-- Totality assertions + +%inline +public export +assert_total : {0 a : _} -> a -> a +assert_total x = x + +%inline +public export +assert_smaller : {0 a, b : _} -> (x : a) -> (y : b) -> b +assert_smaller x y = y + +-- Unit type and pairs + +public export +data Unit = MkUnit + +public export +data Pair : Type -> Type -> Type where + MkPair : {0 a, b : Type} -> (1 x : a) -> (1 y : b) -> Pair a b + +public export +fst : {0 a, b : Type} -> (a, b) -> a +fst (x, y) = x + +public export +snd : {0 a, b : Type} -> (a, b) -> b +snd (x, y) = y + +-- This directive tells auto implicit search what to use to look inside pairs +%pair Pair fst snd + +namespace DPair + public export + data DPair : (a : Type) -> (a -> Type) -> Type where + MkDPair : {0 a : Type} -> {0 p : a -> Type} -> + (1 x : a) -> (1 y : p x)-> DPair a p + + public export + fst : DPair a p -> a + fst (MkDPair x y) = x + + public export + snd : (x : DPair a p) -> p (fst x) + snd (MkDPair x y) = y + +-- The empty type + +public export +data Void : Type where + +-- Equality + +public export +data Equal : forall a, b . a -> b -> Type where + Refl : {0 x : a} -> Equal x x + +%name Equal prf + +%inline +public export +rewrite__impl : {0 x, y : a} -> (0 p : _) -> + (0 rule : x = y) -> (1 val : p y) -> p x +rewrite__impl p Refl prf = prf + +%rewrite Equal rewrite__impl + +%inline +public export +replace : forall x, y, p . (0 rule : x = y) -> p x -> p y +replace Refl prf = prf + +%inline +public export +sym : (0 rule : x = y) -> y = x +sym Refl = Refl + +%inline +public export +trans : forall a, b, c . (0 l : a = b) -> (0 r : b = c) -> a = c +trans Refl Refl = Refl + +public export +believe_me : a -> b +believe_me = prim__believe_me _ _ diff --git a/libs/prelude/Prelude.idr b/libs/prelude/Prelude.idr new file mode 100644 index 0000000..12ab5d8 --- /dev/null +++ b/libs/prelude/Prelude.idr @@ -0,0 +1,1156 @@ +module Prelude + +import public Builtin +import public PrimIO + +{- +The Prelude is minimal (since it is effectively part of the language +specification, this seems to be desirable - we should, nevertheless, aim to +provide a good selection of base libraries). A rule of thumb is that it should +contain the basic functions required by almost any non-trivial program. + +As such, it should contain: + +- Anything the elaborator can desugar to (e.g. pairs, unit, =, laziness) +- Basic types Bool, Nat, List, Dec, Maybe, Either +- The most important utility functions: id, the, composition, etc +- Interfaces for arithmetic and implementations for the primitives and + basic types +- Char and String manipulation +- Show, Eq, Ord, and implementations for all types in the prelude +- Interfaces and functions for basic proof (cong, Uninhabited, etc) -- +- Semigroup, Monoid +- Functor, Applicative, Monad and related functions +- Foldable +- [TODO: Enum for range syntax] +- Console IO + +Everything else should be in the base libraries, and imported as required. +In particular, proofs of Nat/List properties that almost never get used in +practice would probably be better in base libraries. + +(These guidelines will probably get revised a few times.) +-} + +-- Numerical operators +infix 6 ==, /=, <, <=, >, >= +infixl 7 <<, >> -- unused +infixl 8 +, - +infixl 9 *, / + +-- Boolean operators +infixr 4 && +infixr 5 || + +-- List and String operators +infixr 7 ::, ++ + +-- Functor/Applicative/Monad/Algebra operators +infixl 1 >>= +infixr 2 <|> +infixl 3 <*>, *>, <* +infixr 4 <$> +infixl 6 <+> + +-- Utility operators +infixr 9 . +infixr 0 $ + +infixl 9 `div`, `mod` + +----------------------- +-- UTILITY FUNCTIONS -- +----------------------- + +public export %inline +the : (0 a : Type) -> (1 x : a) -> a +the _ x = x + +public export %inline +id : (x : a) -> a +id x = x + +public export %inline +const : a -> b -> a +const x = \value => x + +public export %inline +(.) : (b -> c) -> (a -> b) -> a -> c +(.) f g = \x => f (g x) + +public export +flip : (f : a -> b -> c) -> b -> a -> c +flip f x y = f y x + +public export +apply : (a -> b) -> a -> b +apply f a = f a + +-- $ is compiled specially to shortcut any tricky unification issues, but if +-- it did have a type this is what it would be, and it might be useful to +-- use directly sometimes (e.g. in higher order functions) +public export +($) : forall a, b . ((x : a) -> b x) -> (x : a) -> b x +($) f a = f a + +------------------- +-- PROOF HELPERS -- +------------------- + +public export +cong : {0 f : t -> u} -> a = b -> f a = f b +cong Refl = Refl + +public export +interface Uninhabited t where + uninhabited : t -> Void + +%extern +public export +void : Void -> a + +export +Uninhabited Void where + uninhabited = id + +public export +absurd : Uninhabited t => (h : t) -> a +absurd h = void (uninhabited h) + +public export +Not : Type -> Type +Not x = x -> Void + +-------------- +-- BOOLEANS -- +-------------- + +public export +data Bool = True | False + +public export +not : Bool -> Bool +not True = False +not False = True + +public export +(&&) : Bool -> Lazy Bool -> Bool +(&&) True x = x +(&&) False x = False + +public export +(||) : Bool -> Lazy Bool -> Bool +(||) True x = True +(||) False x = x + +%inline +public export +intToBool : Int -> Bool +intToBool 0 = False +intToBool x = True + +------------------------ +-- EQUALITY, ORDERING -- +------------------------ + +public export +interface Eq ty where + (==) : ty -> ty -> Bool + (/=) : ty -> ty -> Bool + + x == y = not (x /= y) + x /= y = not (x == y) + +public export +Eq () where + _ == _ = True + +public export +Eq Bool where + True == True = True + False == False = True + _ == _ = False + +public export +Eq Int where + x == y = intToBool (prim__eq_Int x y) + +public export +Eq Integer where + x == y = intToBool (prim__eq_Integer x y) + +public export +Eq Double where + x == y = intToBool (prim__eq_Double x y) + +public export +Eq Char where + x == y = intToBool (prim__eq_Char x y) + +public export +Eq String where + x == y = intToBool (prim__eq_String x y) + +public export +Eq a => Eq b => Eq (a, b) where + (x1, y1) == (x2, y2) = x1 == x2 && y1 == y2 + +public export +data Ordering = LT | EQ | GT + +public export +Eq Ordering where + LT == LT = True + EQ == EQ = True + GT == GT = True + _ == _ = False + +public export +interface Eq ty => Ord ty where + compare : ty -> ty -> Ordering + + (<) : ty -> ty -> Bool + (<) x y = compare x y == LT + + (>) : ty -> ty -> Bool + (>) x y = compare x y == GT + + (<=) : ty -> ty -> Bool + (<=) x y = compare x y /= GT + + (>=) : ty -> ty -> Bool + (>=) x y = compare x y /= LT + + max : ty -> ty -> ty + max x y = if x > y then x else y + + min : ty -> ty -> ty + min x y = if (x < y) then x else y + +public export +Ord () where + compare _ _ = EQ + +public export +Ord Bool where + compare False False = EQ + compare False True = LT + compare True False = GT + compare True True = EQ + +public export +Ord Int where + compare x y = if x < y then LT else if x == y then EQ else GT + + (<) x y = intToBool (prim__lt_Int x y) + (<=) x y = intToBool (prim__lte_Int x y) + (>) x y = intToBool (prim__gt_Int x y) + (>=) x y = intToBool (prim__gte_Int x y) + +public export +Ord Integer where + compare x y = if x < y then LT else if x == y then EQ else GT + + (<) x y = intToBool (prim__lt_Integer x y) + (<=) x y = intToBool (prim__lte_Integer x y) + (>) x y = intToBool (prim__gt_Integer x y) + (>=) x y = intToBool (prim__gte_Integer x y) + +public export +Ord Double where + compare x y = if x < y then LT else if x == y then EQ else GT + + (<) x y = intToBool (prim__lt_Double x y) + (<=) x y = intToBool (prim__lte_Double x y) + (>) x y = intToBool (prim__gt_Double x y) + (>=) x y = intToBool (prim__gte_Double x y) + +public export +Ord String where + compare x y = if x < y then LT else if x == y then EQ else GT + + (<) x y = intToBool (prim__lt_String x y) + (<=) x y = intToBool (prim__lte_String x y) + (>) x y = intToBool (prim__gt_String x y) + (>=) x y = intToBool (prim__gte_String x y) + +public export +Ord Char where + compare x y = if x < y then LT else if x == y then EQ else GT + + (<) x y = intToBool (prim__lt_Char x y) + (<=) x y = intToBool (prim__lte_Char x y) + (>) x y = intToBool (prim__gt_Char x y) + (>=) x y = intToBool (prim__gte_Char x y) + +public export +Ord a => Ord b => Ord (a, b) where + compare (x1, y1) (x2, y2) + = if x1 /= x2 then compare x1 x2 + else compare y1 y2 + +------------------------ +-- NUMERIC INTERFACES -- +------------------------ + +%integerLit fromInteger + +public export +interface Num ty where + (+) : ty -> ty -> ty + (*) : ty -> ty -> ty + fromInteger : Integer -> ty + +%allow_overloads fromInteger + +public export +interface Num ty => Neg ty where + negate : ty -> ty + (-) : ty -> ty -> ty + +public export +interface Num ty => Abs ty where + abs : ty -> ty + +public export +interface Num ty => Fractional ty where + (/) : ty -> ty -> ty + recip : ty -> ty + + recip x = 1 / x + +public export +interface Num ty => Integral ty where + div : ty -> ty -> ty + mod : ty -> ty -> ty + +----- instances for primitives +-- Integer + +public export +Num Integer where + (+) = prim__add_Integer + (*) = prim__mul_Integer + fromInteger = id + +Neg Integer where + negate x = prim__sub_Integer 0 x + (-) = prim__sub_Integer + +Abs Integer where + abs x = if x < 0 then -x else x + +Integral Integer where + div x y + = case y == 0 of + False => prim__div_Integer x y + mod x y + = case y == 0 of + False => prim__mod_Integer x y + +-- This allows us to pick integer as a default at the end of elaboration if +-- all other possibilities fail. I don't plan to provide a nicer syntax for +-- this... +%defaulthint +public export +defaultInteger : Num Integer +defaultInteger = %search + +-- Int + +public export +Num Int where + (+) = prim__add_Int + (*) = prim__mul_Int + fromInteger = prim__cast_IntegerInt + +Neg Int where + negate x = prim__sub_Int 0 x + (-) = prim__sub_Int + +Abs Int where + abs x = if x < 0 then -x else x + +Integral Int where + div x y + = case y == 0 of + False => prim__div_Int x y + mod x y + = case y == 0 of + False => prim__mod_Int x y + +-- Double + +public export +Num Double where + (+) = prim__add_Double + (*) = prim__mul_Double + fromInteger = prim__cast_IntegerDouble + +Neg Double where + negate x = prim__negate_Double x + (-) = prim__sub_Double + +Abs Double where + abs x = if x < 0 then -x else x + +Fractional Double where + (/) = prim__div_Double + +------------- +-- ALGEBRA -- +------------- + +public export +interface Semigroup ty where + (<+>) : ty -> ty -> ty + +public export +interface Semigroup ty => Monoid ty where + neutral : ty + +--------------------------------- +-- FUNCTOR, APPLICATIVE, MONAD -- +--------------------------------- + +public export +interface Functor f where + map : (a -> b) -> f a -> f b + +public export +(<$>) : Functor f => (func : a -> b) -> f a -> f b +(<$>) func x = map func x + +public export +interface Functor f => Applicative f where + pure : a -> f a + (<*>) : f (a -> b) -> f a -> f b + +public export +(<*) : Applicative f => f a -> f b -> f a +a <* b = map const a <*> b + +public export +(*>) : Applicative f => f a -> f b -> f b +a *> b = map (const id) a <*> b + +%allow_overloads pure +%allow_overloads (<*) +%allow_overloads (*>) + +public export +interface Applicative f => Alternative f where + empty : f a + (<|>) : f a -> f a -> f a + +public export +interface Applicative m => Monad m where + (>>=) : m a -> (a -> m b) -> m b + join : m (m a) -> m a + + -- default implementations + (>>=) x f = join (f <$> x) + join x = x >>= id + +%allow_overloads (>>=) + +public export +guard : Alternative f => Bool -> f () +guard x = if x then pure () else empty + +public export +when : Applicative f => Bool -> Lazy (f ()) -> f () +when True f = f +when False f = pure () + +--------------------------- +-- FOLDABLE, TRAVERSABLE -- +--------------------------- + +public export +interface Foldable (t : Type -> Type) where + foldr : (func : elem -> acc -> acc) -> (init : acc) -> (input : t elem) -> acc + foldl : (func : acc -> elem -> acc) -> (init : acc) -> (input : t elem) -> acc + foldl f z t = foldr (flip (.) . flip f) id t z + +public export +concat : (Foldable t, Monoid a) => t a -> a +concat = foldr (<+>) neutral + +public export +concatMap : (Foldable t, Monoid m) => (a -> m) -> t a -> m +concatMap f = foldr ((<+>) . f) neutral + +public export +and : Foldable t => t (Lazy Bool) -> Bool +and = foldl (&&) True + +public export +or : Foldable t => t (Lazy Bool) -> Bool +or = foldl (||) False + +public export +any : Foldable t => (a -> Bool) -> t a -> Bool +any p = foldl (\x,y => x || p y) False + +public export +all : Foldable t => (a -> Bool) -> t a -> Bool +all p = foldl (\x,y => x && p y) True + +public export +sum : (Foldable t, Num a) => t a -> a +sum = foldr (+) 0 + +public export +product : (Foldable t, Num a) => t a -> a +product = foldr (*) 1 + +----------- +-- NATS --- +----------- + +public export +data Nat = Z | S Nat + +%name Nat k, j, i + +public export +integerToNat : Integer -> Nat +integerToNat x + = if intToBool (prim__eq_Integer x 0) + then Z + else S (assert_total (integerToNat (prim__sub_Integer x 1))) + +-- Define separately so we can spot the name when optimising Nats +public export +plus : Nat -> Nat -> Nat +plus Z y = y +plus (S k) y = S (plus k y) + +public export +mult : Nat -> Nat -> Nat +mult Z y = Z +mult (S k) y = plus y (mult k y) + +public export +Num Nat where + (+) = plus + (*) = mult + + fromInteger x = integerToNat x + +public export +Eq Nat where + Z == Z = True + S j == S k = j == k + _ == _ = False + +public export +Ord Nat where + compare Z Z = EQ + compare Z (S k) = LT + compare (S k) Z = GT + compare (S j) (S k) = compare j k + +public export +natToInteger : Nat -> Integer +natToInteger Z = 0 +natToInteger (S k) = 1 + natToInteger k + +----------- +-- MAYBE -- +----------- + +public export +data Maybe : (ty : Type) -> Type where + Nothing : Maybe ty + Just : (1 x : ty) -> Maybe ty + +public export +maybe : Lazy b -> Lazy (a -> b) -> Maybe a -> b +maybe n j Nothing = n +maybe n j (Just x) = j x + +public export +Eq a => Eq (Maybe a) where + Nothing == Nothing = True + Nothing == (Just _) = False + (Just _) == Nothing = False + (Just a) == (Just b) = a == b + +public export +Ord a => Ord (Maybe a) where + compare Nothing Nothing = EQ + compare Nothing (Just _) = LT + compare (Just _) Nothing = GT + compare (Just a) (Just b) = compare a b + +public export +Semigroup (Maybe a) where + Nothing <+> m = m + (Just x) <+> _ = Just x + +public export +Monoid (Maybe a) where + neutral = Nothing + +public export +Functor Maybe where + map f (Just x) = Just (f x) + map f Nothing = Nothing + +public export +Applicative Maybe where + pure = Just + + Just f <*> Just a = Just (f a) + _ <*> _ = Nothing + +public export +Alternative Maybe where + empty = Nothing + + (Just x) <|> _ = Just x + Nothing <|> v = v + +public export +Monad Maybe where + Nothing >>= k = Nothing + (Just x) >>= k = k x + +public export +Foldable Maybe where + foldr _ z Nothing = z + foldr f z (Just x) = f x z + +--------- +-- DEC -- +--------- + +public export +data Dec : Type -> Type where + Yes : (prf : prop) -> Dec prop + No : (contra : prop -> Void) -> Dec prop + +------------ +-- EITHER -- +------------ + +public export +data Either : (a : Type) -> (b : Type) -> Type where + Left : forall a, b. (1 x : a) -> Either a b + Right : forall a, b. (1 x : b) -> Either a b + +public export +either : Lazy (a -> c) -> Lazy (b -> c) -> Either a b -> c +either l r (Left x) = l x +either l r (Right x) = r x + +public export +(Eq a, Eq b) => Eq (Either a b) where + Left x == Left x' = x == x' + Right x == Right x' = x == x' + _ == _ = False + +public export +Functor (Either e) where + map f (Left x) = Left x + map f (Right x) = Right (f x) + +public export +Applicative (Either e) where + pure = Right + + (Left a) <*> _ = Left a + (Right f) <*> (Right r) = Right (f r) + (Right _) <*> (Left l) = Left l + +public export +Monad (Either e) where + (Left n) >>= _ = Left n + (Right r) >>= f = f r + +----------- +-- LISTS -- +----------- + +public export +data List a = Nil | (::) a (List a) + +%name List xs, ys, zs + +public export +Eq a => Eq (List a) where + [] == [] = True + x :: xs == y :: ys = x == y && xs == ys + _ == _ = False + +public export +Ord a => Ord (List a) where + compare [] [] = EQ + compare [] (x :: xs) = LT + compare (x :: xs) [] = GT + compare (x :: xs) (y ::ys) + = case compare x y of + EQ => compare xs ys + c => c + +namespace List + public export + (++) : List a -> List a -> List a + [] ++ ys = ys + (x :: xs) ++ ys = x :: xs ++ ys + +public export +Functor List where + map f [] = [] + map f (x :: xs) = f x :: map f xs + +public export +Semigroup (List a) where + (<+>) = (++) + +public export +Monoid (List a) where + neutral = [] + +public export +Foldable List where + foldr c n [] = n + foldr c n (x::xs) = c x (foldr c n xs) + + foldl f q [] = q + foldl f q (x::xs) = foldl f (f q x) xs + +public export +Applicative List where + pure x = [x] + fs <*> vs = concatMap (\f => map f vs) fs + +public export +Alternative List where + empty = [] + (<|>) = (++) + +public export +Monad List where + m >>= f = concatMap f m + +public export +elem : Eq a => a -> List a -> Bool +x `elem` [] = False +x `elem` (y :: ys) = if x == y then True else x `elem` ys + +------------- +-- STREAMS -- +------------- + +namespace Stream + public export + data Stream : Type -> Type where + (::) : a -> Inf (Stream a) -> Stream a + +public export +Functor Stream where + map f (x :: xs) = f x :: map f xs + +public export +head : Stream a -> a +head (x :: xs) = x + +public export +tail : Stream a -> Stream a +tail (x :: xs) = xs + +public export +take : Nat -> Stream a -> List a +take Z xs = [] +take (S k) (x :: xs) = x :: take k xs + +------------- +-- STRINGS -- +------------- + +namespace Strings + public export + (++) : (1 x : String) -> (1 y : String) -> String + x ++ y = prim__strAppend x y + +public export +length : String -> Nat +length str = fromInteger (prim__cast_IntInteger (prim__strLength str)) + +public export +reverse : String -> String +reverse = prim__strReverse + +public export +substr : Nat -> Nat -> String -> String +substr s e = prim__strSubstr (prim__cast_IntegerInt (natToInteger s)) + (prim__cast_IntegerInt (natToInteger e)) + +public export +strCons : Char -> String -> String +strCons = prim__strCons + +public export +strUncons : String -> Maybe (Char, String) +strUncons "" = Nothing +strUncons str = Just (prim__strHead str, prim__strTail str) + +export +pack : List Char -> String +pack [] = "" +pack (x :: xs) = strCons x (pack xs) + +export +fastPack : List Char -> String +fastPack xs + = unsafePerformIO (schemeCall String "string" (toFArgs xs)) + where + toFArgs : List Char -> FArgList + toFArgs [] = [] + toFArgs (x :: xs) = x :: toFArgs xs + +export +unpack : String -> List Char +unpack str = unpack' 0 (prim__cast_IntegerInt (natToInteger (length str))) str + where + unpack' : Int -> Int -> String -> List Char + unpack' pos len str + = if pos >= len + then [] + else (prim__strIndex str pos) :: unpack' (pos + 1) len str + + +public export +Semigroup String where + (<+>) = (++) + +public export +Monoid String where + neutral = "" + +---------------- +-- CHARACTERS -- +---------------- +public export +isUpper : Char -> Bool +isUpper x = x >= 'A' && x <= 'Z' + +public export +isLower : Char -> Bool +isLower x = x >= 'a' && x <= 'z' + +public export +isAlpha : Char -> Bool +isAlpha x = isUpper x || isLower x + +public export +isDigit : Char -> Bool +isDigit x = (x >= '0' && x <= '9') + +public export +isAlphaNum : Char -> Bool +isAlphaNum x = isDigit x || isAlpha x + +public export +isSpace : Char -> Bool +isSpace x + = x == ' ' || x == '\t' || x == '\r' || + x == '\n' || x == '\f' || x == '\v' || + x == '\xa0' + +public export +isNL : Char -> Bool +isNL x = x == '\r' || x == '\n' + +public export +toUpper : Char -> Char +toUpper x + = if (isLower x) + then prim__cast_IntChar (prim__cast_CharInt x - 32) + else x + +public export +toLower : Char -> Char +toLower x + = if (isUpper x) + then prim__cast_IntChar (prim__cast_CharInt x + 32) + else x + +public export +isHexDigit : Char -> Bool +isHexDigit x = elem (toUpper x) hexChars where + hexChars : List Char + hexChars + = ['0', '1', '2', '3', '4', '5', '6', '7', '8', '9', + 'A', 'B', 'C', 'D', 'E', 'F'] + +public export +isOctDigit : Char -> Bool +isOctDigit x = (x >= '0' && x <= '7') + +public export +isControl : Char -> Bool +isControl x + = (x >= '\x0000' && x <= '\x001f') + || (x >= '\x007f' && x <= '\x009f') + +---------- +-- SHOW -- +---------- + +public export +data Prec = Open | Equal | Dollar | Backtick | User Nat | PrefixMinus | App + +public export +precCon : Prec -> Integer +precCon Open = 0 +precCon Equal = 1 +precCon Dollar = 2 +precCon Backtick = 3 +precCon (User n) = 4 +precCon PrefixMinus = 5 +precCon App = 6 + +Eq Prec where + (==) (User m) (User n) = m == n + (==) x y = precCon x == precCon y + +Ord Prec where + compare (User m) (User n) = compare m n + compare x y = compare (precCon x) (precCon y) + +public export +interface Show ty where + show : (x : ty) -> String + show x = showPrec Open x + + showPrec : (d : Prec) -> (x : ty) -> String + showPrec _ x = show x + +showParens : (b : Bool) -> String -> String +showParens False s = s +showParens True s = "(" ++ s ++ ")" + +export +showCon : (d : Prec) -> (conName : String) -> (shownArgs : String) -> String +showCon d conName shownArgs = showParens (d >= App) (conName ++ shownArgs) + +export +showArg : Show a => (x : a) -> String +showArg x = " " ++ showPrec App x + +firstCharIs : (Char -> Bool) -> String -> Bool +firstCharIs p "" = False +firstCharIs p str = p (prim__strHead str) + +primNumShow : (a -> String) -> Prec -> a -> String +primNumShow f d x = let str = f x in showParens (d >= PrefixMinus && firstCharIs (== '-') str) str + +export +Show Int where + showPrec = primNumShow prim__cast_IntString + +export +Show Integer where + showPrec = primNumShow prim__cast_IntegerString + +export +Show Double where + showPrec = primNumShow prim__cast_DoubleString + +protectEsc : (Char -> Bool) -> String -> String -> String +protectEsc p f s = f ++ (if firstCharIs p s then "\\&" else "") ++ s + +showLitChar : Char -> String -> String +showLitChar '\a' = ("\\a" ++) +showLitChar '\b' = ("\\b" ++) +showLitChar '\f' = ("\\f" ++) +showLitChar '\n' = ("\\n" ++) +showLitChar '\r' = ("\\r" ++) +showLitChar '\t' = ("\\t" ++) +showLitChar '\v' = ("\\v" ++) +showLitChar '\SO' = protectEsc (== 'H') "\\SO" +showLitChar '\DEL' = ("\\DEL" ++) +showLitChar '\\' = ("\\\\" ++) +showLitChar c + = case getAt (fromInteger (prim__cast_CharInteger c)) asciiTab of + Just k => strCons '\\' . (k ++) + Nothing => if (c > '\DEL') + then strCons '\\' . protectEsc isDigit (show (prim__cast_CharInt c)) + else strCons c + where + asciiTab : List String + asciiTab + = ["NUL", "SOH", "STX", "ETX", "EOT", "ENQ", "ACK", "BEL", + "BS", "HT", "LF", "VT", "FF", "CR", "SO", "SI", + "DLE", "DC1", "DC2", "DC3", "DC4", "NAK", "SYN", "ETB", + "CAN", "EM", "SUB", "ESC", "FS", "GS", "RS", "US"] + + getAt : Nat -> List String -> Maybe String + getAt Z (x :: xs) = Just x + getAt (S k) (x :: xs) = getAt k xs + getAt _ [] = Nothing + +showLitString : List Char -> String -> String +showLitString [] = id +showLitString ('"'::cs) = ("\\\"" ++) . showLitString cs +showLitString (c ::cs) = (showLitChar c) . showLitString cs + +export +Show Char where + show '\'' = "'\\''" + show c = strCons '\'' (showLitChar c "'") + +export +Show String where + show cs = strCons '"' (showLitString (unpack cs) "\"") + +export +Show Nat where + show n = show (the Integer (natToInteger n)) + +export +Show Bool where + show True = "True" + show False = "False" + +export +Show () where + show () = "()" + +export +(Show a, Show b) => Show (a, b) where + show (x, y) = "(" ++ show x ++ ", " ++ show y ++ ")" + +export +(Show a, {y : a} -> Show (p y)) => Show (DPair a p) where + show (y ** prf) = "(" ++ show y ++ " ** " ++ show prf ++ ")" + +export +Show a => Show (List a) where + show xs = "[" ++ show' "" xs ++ "]" + where + show' : String -> List a -> String + show' acc [] = acc + show' acc [x] = acc ++ show x + show' acc (x :: xs) = show' (acc ++ show x ++ ", ") xs + +export +Show a => Show (Maybe a) where + showPrec d Nothing = "Nothing" + showPrec d (Just x) = showCon d "Just" (showArg x) + +-------- +-- IO -- +-------- + +public export +Functor IO where + map f io = io_bind io (\b => io_pure (f b)) + +public export +Applicative IO where + pure x = io_pure x + f <*> a + = io_bind f (\f' => + io_bind a (\a' => + io_pure (f' a'))) + +public export +Monad IO where + b >>= k = io_bind b k + +export +print : Show a => a -> IO () +print x = putStr $ show x + +export +printLn : Show a => a -> IO () +printLn x = putStrLn $ show x + +----------- +-- CASTS -- +----------- + +-- Casts between primitives only here. They might be lossy. + +-- To String + +public export +interface Cast from to where + cast : from -> to + +export +Cast Int String where + cast = prim__cast_IntString + +export +Cast Integer String where + cast = prim__cast_IntegerString + +export +Cast Char String where + cast = prim__cast_CharString + +export +Cast Double String where + cast = prim__cast_DoubleString + +-- To Integer + +export +Cast Int Integer where + cast = prim__cast_IntInteger + +export +Cast Char Integer where + cast = prim__cast_CharInteger + +export +Cast Double Integer where + cast = prim__cast_DoubleInteger + +export +Cast String Integer where + cast = prim__cast_StringInteger + +-- To Int + +export +Cast Integer Int where + cast = prim__cast_IntegerInt + +export +Cast Char Int where + cast = prim__cast_CharInt + +export +Cast Double Int where + cast = prim__cast_DoubleInt + +export +Cast String Int where + cast = prim__cast_StringInt + +-- To Char + +export +Cast Int Char where + cast = prim__cast_IntChar + +-- To Double + +export +Cast Int Double where + cast = prim__cast_IntDouble + +export +Cast Integer Double where + cast = prim__cast_IntegerDouble + +export +Cast String Double where + cast = prim__cast_StringDouble diff --git a/libs/prelude/PrimIO.idr b/libs/prelude/PrimIO.idr new file mode 100644 index 0000000..55f719b --- /dev/null +++ b/libs/prelude/PrimIO.idr @@ -0,0 +1,81 @@ +module PrimIO + +import Builtin + +public export +data IORes : Type -> Type where + MkIORes : (result : a) -> (1 x : %World) -> IORes a + +export +data IO : Type -> Type where + MkIO : (1 fn : (1 x : %World) -> IORes a) -> IO a + +export +io_pure : a -> IO a +io_pure x = MkIO (\w => MkIORes x w) + +export +io_bind : (1 act : IO a) -> (1 k : a -> IO b) -> IO b +io_bind (MkIO fn) + = \k => MkIO (\w => let MkIORes x' w' = fn w + MkIO res = k x' in + res w') + +%extern prim__putStr : String -> (1 x : %World) -> IORes () +%extern prim__getStr : (1 x : %World) -> IORes String + +public export +data Ptr : Type where + +public export +data ThreadID : Type where + +public export +data FArgList : Type where + Nil : FArgList + (::) : {a : Type} -> (1 arg : a) -> (1 args : FArgList) -> FArgList + +%extern prim__cCall : (ret : Type) -> String -> (1 args : FArgList) -> + (1 x : %World) -> IORes ret +%extern prim__schemeCall : (ret : Type) -> String -> (1 args : FArgList) -> + (1 x : %World) -> IORes ret + +export %inline +primIO : (1 fn : (1 x : %World) -> IORes a) -> IO a +primIO op = MkIO op + +export %inline +schemeCall : (ret : Type) -> String -> (1 args : FArgList) -> IO ret +schemeCall ret fn args = primIO (prim__schemeCall ret fn args) + +export %inline +cCall : (ret : Type) -> String -> FArgList -> IO ret +cCall ret fn args = primIO (prim__cCall ret fn args) + +export +putStr : String -> IO () +putStr str = primIO (prim__putStr str) + +export +putStrLn : String -> IO () +putStrLn str = putStr (prim__strAppend str "\n") + +export +getLine : IO String +getLine = primIO prim__getStr + +export +fork : (1 prog : IO ()) -> IO ThreadID +fork (MkIO act) = schemeCall ThreadID "blodwen-thread" [act] + +unsafeCreateWorld : (1 f : (1 x : %World) -> a) -> a +unsafeCreateWorld f = f %MkWorld + +unsafeDestroyWorld : (1 x : %World) -> a -> a +unsafeDestroyWorld %MkWorld x = x + +export +unsafePerformIO : IO a -> a +unsafePerformIO (MkIO f) + = unsafeCreateWorld (\w => case f w of + MkIORes res w' => unsafeDestroyWorld w' res) diff --git a/src/Core/AutoSearch.idr b/src/Core/AutoSearch.idr index c2d90ff..6297a7d 100644 --- a/src/Core/AutoSearch.idr +++ b/src/Core/AutoSearch.idr @@ -353,6 +353,29 @@ concreteDets {vars} fc defaults env top pos dets ((p, arg) :: args) = throw (CantSolveGoal fc [] top) concrete defs tm top = pure () +checkConcreteDets : {auto c : Ref Ctxt Defs} -> + {auto u : Ref UST UState} -> + FC -> Bool -> + Env Term vars -> (top : ClosedTerm) -> + NF vars -> + Core () +checkConcreteDets fc defaults env top (NTCon tfc tyn t a args) + = do defs <- get Ctxt + if isPairType tyn defs + then case args of + [(_, aty), (_, bty)] => + do anf <- evalClosure defs aty + bnf <- evalClosure defs bty + checkConcreteDets fc defaults env top anf + checkConcreteDets fc defaults env top bnf + _ => do sd <- getSearchData fc defaults tyn + concreteDets fc defaults env top 0 (detArgs sd) args + else + do sd <- getSearchData fc defaults tyn + concreteDets fc defaults env top 0 (detArgs sd) args +checkConcreteDets fc defaults env top _ + = pure () + -- Declared at the top searchType fc rigc defaults depth def top env (Bind nfc x (Pi c p ty) sc) = pure (Bind nfc x (Lam c p ty) @@ -371,7 +394,8 @@ searchType {vars} fc rigc defaults depth def top env target then do logNF 10 "Next target: " env nty sd <- getSearchData fc defaults tyn -- Check determining arguments are okay for 'args' - concreteDets fc defaults env top 0 (detArgs sd) args + checkConcreteDets fc defaults env top + (NTCon tfc tyn t a args) tryUnify (searchLocal fc rigc defaults depth def top env nty) (tryGroups nty (hintGroups sd)) diff --git a/src/Core/Binary.idr b/src/Core/Binary.idr index 6d8edac..38ad5f1 100644 --- a/src/Core/Binary.idr +++ b/src/Core/Binary.idr @@ -229,12 +229,36 @@ addGlobalDef modns as def addTypeHint : {auto c : Ref Ctxt Defs} -> FC -> (Name, Name, Bool) -> Core () -addTypeHint fc (tyn, hintn, d) = addHintFor fc tyn hintn d True +addTypeHint fc (tyn, hintn, d) + = do logC 10 (pure (show !(getFullName hintn) ++ " for " ++ + show !(getFullName tyn))) + addHintFor fc tyn hintn d True addAutoHint : {auto c : Ref Ctxt Defs} -> (Name, Bool) -> Core () addAutoHint (hintn, d) = addGlobalHint hintn d +export +updatePair : {auto c : Ref Ctxt Defs} -> + Maybe PairNames -> Core () +updatePair p + = do defs <- get Ctxt + put Ctxt (record { options->pairnames $= (p <+>) } defs) + +export +updateRewrite : {auto c : Ref Ctxt Defs} -> + Maybe RewriteNames -> Core () +updateRewrite r + = do defs <- get Ctxt + put Ctxt (record { options->rewritenames $= (r <+>) } defs) + +export +updatePrims : {auto c : Ref Ctxt Defs} -> + PrimNames -> Core () +updatePrims p + = do defs <- get Ctxt + put Ctxt (record { options->primnames = p } defs) + -- Add definitions from a binary file to the current context -- Returns the "extra" section of the file (user defined data), the interface -- hash and the list of additional TTCs that need importing @@ -272,8 +296,14 @@ readFromTTC loc reexp fname modNS importAs setNS (currentNS ttc) -- Set up typeHints and autoHints based on the loaded data traverse_ (addTypeHint loc) (typeHints ttc) + defs <- get Ctxt traverse_ addAutoHint (autoHints ttc) - -- TODO: Set up pair/rewrite etc names, name directives + -- Set up pair/rewrite etc names + updatePair (pairnames ttc) + updateRewrite (rewritenames ttc) + updatePrims (primnames ttc) + -- TODO: Name directives + when (not reexp) clearSavedHints resetFirstEntry diff --git a/src/Core/Context.idr b/src/Core/Context.idr index 19b970d..274a840 100644 --- a/src/Core/Context.idr +++ b/src/Core/Context.idr @@ -1025,11 +1025,14 @@ addHintFor fc tyn hintn_in direct loading let hs = case lookup tyn (typeHints defs) of Just hs => hs Nothing => [] - let defs' = record { typeHints $= insert tyn ((hintn, direct) :: hs) } - defs - when True $ -- (not loading) $ - put Ctxt (record { saveTypeHints $= ((tyn, hintn, direct) :: ) - } defs') + if loading + then put Ctxt + (record { typeHints $= insert tyn ((hintn, direct) :: hs) + } defs) + else put Ctxt + (record { typeHints $= insert tyn ((hintn, direct) :: hs), + saveTypeHints $= ((tyn, hintn, direct) :: ) + } defs) export addGlobalHint : {auto c : Ref Ctxt Defs} -> diff --git a/src/Core/LinearCheck.idr b/src/Core/LinearCheck.idr index c7b705a..db62557 100644 --- a/src/Core/LinearCheck.idr +++ b/src/Core/LinearCheck.idr @@ -289,7 +289,7 @@ mutual glueBack defs env sc', fused ++ aused) _ => do tfty <- getTerm gfty - throw (InternalError ("Linearity checking failed on " ++ show f' ++ + throw (GenericMsg fc ("Linearity checking failed on " ++ show f' ++ " (" ++ show tfty ++ " not a function type)")) lcheck rig erase env (As fc as pat) @@ -529,13 +529,15 @@ mutual | Nothing => throw (InternalError ("Linearity checking failed on " ++ show n)) if linearChecked def then pure (type def) - else case definition def of + else do case definition def of PMDef _ _ _ pats => do u <- getArgUsage (getLoc (type def)) rig (type def) pats let ty' = updateUsage u (type def) updateTy idx ty' setLinearCheck idx True + logTerm 5 ("New type of " ++ + show (fullname def)) ty' pure ty' _ => pure (type def) where @@ -565,9 +567,9 @@ mutual substMeta (Bind bfc n (Lam c e ty) sc) (a :: as) env = substMeta sc as (a :: env) substMeta rhs [] env = pure (substs env rhs) - substMeta _ _ _ = throw (InternalError ("Badly formed metavar solution " ++ show n)) - expandMeta rig erase env n idx _ _ - = throw (InternalError ("Badly formed metavar solution " ++ show n)) + substMeta rhs _ _ = throw (InternalError ("Badly formed metavar solution " ++ show n ++ " " ++ show rhs)) + expandMeta rig erase env n idx def _ + = throw (InternalError ("Badly formed metavar solution " ++ show n ++ " " ++ show def)) lcheckMeta : {auto c : Ref Ctxt Defs} -> {auto u : Ref UST UState} -> @@ -590,7 +592,7 @@ mutual = do defs <- get Ctxt empty <- clearDefs defs ty <- quote empty env nty - throw (InternalError ("Linearity checking failed on metavar + throw (GenericMsg fc ("Linearity checking failed on metavar " ++ show n ++ " (" ++ show ty ++ " not a function type)")) lcheckMeta rig erase env fc n idx [] chk nty diff --git a/src/Core/Normalise.idr b/src/Core/Normalise.idr index d351b9b..8eaaccf 100644 --- a/src/Core/Normalise.idr +++ b/src/Core/Normalise.idr @@ -105,9 +105,10 @@ parameters (defs : Defs, topopts : EvalOpts) = pure (NDelay fc r (MkClosure topopts locs env ty) (MkClosure topopts locs env tm)) eval env locs (TForce fc tm) stk - = do tm' <- eval env locs tm stk + = do tm' <- eval env locs tm [] case tm' of - NDelay fc r _ arg => evalClosure defs arg + NDelay fc r _ arg => + eval env (arg :: locs) (Local {name = UN "fvar"} fc Nothing _ First) stk _ => pure (NForce fc tm') eval env locs (PrimVal fc c) stk = pure $ NPrimVal fc c eval env locs (Erased fc) stk = pure $ NErased fc diff --git a/src/Core/Options.idr b/src/Core/Options.idr index 861176b..03dbc3d 100644 --- a/src/Core/Options.idr +++ b/src/Core/Options.idr @@ -160,7 +160,7 @@ defaultPPrint : PPrinter defaultPPrint = MkPPOpts False True False defaultSession : Session -defaultSession = MkSessionOpts True Chez 0 False +defaultSession = MkSessionOpts False Chez 0 False defaultElab : ElabDirectives defaultElab = MkElabDirectives True True diff --git a/src/Core/TT.idr b/src/Core/TT.idr index 9be214f..b9630d8 100644 --- a/src/Core/TT.idr +++ b/src/Core/TT.idr @@ -650,6 +650,10 @@ Weaken Term where weaken tm = thin {outer = []} _ tm weakenNs ns tm = insertNames {outer = []} ns tm +export +Weaken Var where + weaken (MkVar p) = MkVar (Later p) + export varExtend : IsVar x idx xs -> IsVar x idx (xs ++ ys) -- What Could Possibly Go Wrong? diff --git a/src/Core/TTC.idr b/src/Core/TTC.idr index aff63e0..efe15f4 100644 --- a/src/Core/TTC.idr +++ b/src/Core/TTC.idr @@ -259,7 +259,7 @@ mutual Just (n, Just idx) <- coreLift $ readArray r x | Just (n, Nothing) => corrupt ("Metavar name index " ++ show x) - | Nothing => corrupt ("Metavar name index " ++ show x) + | Nothing => corrupt ("Metavar name index " ++ show x ++ " (not in array)") xs <- fromBuf r b pure (Meta fc (UN "metavar") idx xs) 3 => do fc <- fromBuf r b; x <- fromBuf r b diff --git a/src/Core/Unify.idr b/src/Core/Unify.idr index df6e1e9..68f873f 100644 --- a/src/Core/Unify.idr +++ b/src/Core/Unify.idr @@ -32,6 +32,12 @@ Eq UnifyMode where public export data AddLazy = NoLazy | AddForce | AddDelay LazyReason +export +Show AddLazy where + show NoLazy = "NoLazy" + show AddForce = "AddForce" + show (AddDelay _) = "AddDelay" + public export record UnifyResult where constructor MkUnifyResult @@ -301,8 +307,8 @@ instantiate : {auto c : Ref Ctxt Defs} -> Core () instantiate {newvars} loc env mname mref mdef locs otm tm = do log 5 $ "Instantiating " ++ show tm ++ " in " ++ show newvars - let Hole _ _ = definition mdef - | def => ufail {a=()} loc (show mname ++ " already resolved as " ++ show def) +-- let Hole _ _ = definition mdef +-- | def => ufail {a=()} loc (show mname ++ " already resolved as " ++ show def) case fullname mdef of PV pv pi => throw (PatternVariableUnifies loc env (PV pv pi) otm) _ => pure () @@ -512,15 +518,16 @@ mutual {vars : _} -> UnifyMode -> FC -> Env Term vars -> (metaname : Name) -> (metaref : Int) -> - (args : List (AppInfo, Closure vars)) -> + (margs : List (AppInfo, Closure vars)) -> + (margs' : List (AppInfo, Closure vars)) -> (soln : NF vars) -> Core UnifyResult -- TODO: if either side is a pattern variable application, and we're in a term, -- (which will be a type) we can proceed because the pattern variable -- has to end up pi bound. Unify the right most variables, and continue. - unifyPatVar mode loc env mname mref args tm + unifyPatVar mode loc env mname mref margs margs' tm = postpone loc "Not in pattern fragment" env - (NApp loc (NMeta mname mref args) []) tm + (NApp loc (NMeta mname mref margs) margs') tm solveHole : {auto c : Ref Ctxt Defs} -> {auto u : Ref UST UState} -> @@ -580,10 +587,10 @@ mutual case !(patternEnv env args) of Nothing => do Just (Hole _ inv) <- lookupDefExact (Resolved mref) (gamma defs) - | _ => unifyPatVar mode loc env mname mref args tmnf + | _ => unifyPatVar mode loc env mname mref margs margs' tmnf if inv then unifyHoleApp mode loc env mname mref margs margs' tmnf - else unifyPatVar mode loc env mname mref args tmnf + else unifyPatVar mode loc env mname mref margs margs' tmnf Just (newvars ** (locs, submv)) => do tm <- quote empty env tmnf case shrinkTerm tm submv of @@ -931,7 +938,7 @@ mutual unifyD _ _ mode loc env x y = do defs <- get Ctxt if x == y - then do log 10 $ "S§kipped unification (equal already): " + then do log 10 $ "Skipped unification (equal already): " ++ show x ++ " and " ++ show y pure success else unify mode loc env !(nf defs env x) !(nf defs env y) @@ -946,11 +953,8 @@ mutual export Unify Closure where unifyD _ _ mode loc env x y - = do gam <- get Ctxt - empty <- clearDefs gam - -- 'quote' using an empty global context, because then function - -- names won't reduce until they have to - unify mode loc env !(quote empty env x) !(quote empty env y) + = do defs <- get Ctxt + unify mode loc env !(evalClosure defs x) !(evalClosure defs y) export setInvertible : {auto c : Ref Ctxt Defs} -> diff --git a/src/Idris/CommandLine.idr b/src/Idris/CommandLine.idr index 112aa98..168bc4a 100644 --- a/src/Idris/CommandLine.idr +++ b/src/Idris/CommandLine.idr @@ -47,6 +47,7 @@ data CLOpt IdeModeSocket | ||| Run as a checker for the core language TTImp Yaffle String | + Timing | BlodwenPaths @@ -95,7 +96,9 @@ options = [MkOpt ["--check", "-c"] [] [CheckOnly] MkOpt ["--help", "-h", "-?"] [] [Help] (Just "Display help text"), MkOpt ["--yaffle", "--ttimp"] ["ttimp file"] (\f => [Yaffle f]) - Nothing + Nothing, + MkOpt ["--timing"] [] [Timing] + (Just "Display timing logs") ] optUsage : OptDesc -> String diff --git a/src/Idris/Elab/Interface.idr b/src/Idris/Elab/Interface.idr index a129895..ca212d8 100644 --- a/src/Idris/Elab/Interface.idr +++ b/src/Idris/Elab/Interface.idr @@ -293,7 +293,7 @@ elabInterface {vars} fc vis env nest constraints iname params dets mcon body (FC, List FnOpt, Name, List ImpClause) -> Core (Name, List ImpClause) elabDefault tydecls (fc, opts, n, cs) - = do orig <- branch + = do -- orig <- branch let dn_in = UN ("Default implementation of " ++ show n) dn <- inCurrentNS dn_in @@ -310,7 +310,8 @@ elabInterface {vars} fc vis env nest constraints iname params dets mcon body let cs' = map (changeName dn) cs processDecl [] nest env (IDef fc dn cs') -- Reset the original context, we don't need to keep the definition - put Ctxt orig + -- Actually we do for the metadata and name map! +-- put Ctxt orig pure (n, cs) where changeNameTerm : Name -> RawImp -> RawImp diff --git a/src/Idris/ProcessIdr.idr b/src/Idris/ProcessIdr.idr index c0fb743..3307632 100644 --- a/src/Idris/ProcessIdr.idr +++ b/src/Idris/ProcessIdr.idr @@ -18,6 +18,8 @@ import Idris.REPLCommon import Idris.REPLOpts import Idris.Syntax +import Data.NameMap + import Control.Catchable processDecl : {auto c : Ref Ctxt Defs} -> @@ -204,7 +206,7 @@ processMod srcf ttcf msg mod sourcecode -- a phase before this which builds the dependency graph -- (also that we only build child dependencies if rebuilding -- changes the interface - will need to store a hash in .ttc!) - traverse readImport imps + traverse_ readImport imps -- Before we process the source, make sure the "hide_everywhere" -- names are set to private (TODO, maybe if we want this?) @@ -228,7 +230,9 @@ process : {auto c : Ref Ctxt Defs} -> process buildmsg file = do Right res <- coreLift (readFile file) | Left err => pure [FileErr file err] - case runParser res (do p <- prog file; eoi; pure p) of + parseRes <- logTime ("Parsing " ++ file) $ + pure (runParser res (do p <- prog file; eoi; pure p)) + case parseRes of Left err => pure [ParseFail (getParseErrorLoc file err) err] Right mod => -- Processing returns a list of errors across a whole module, @@ -236,16 +240,18 @@ process buildmsg file -- other possible errors catch (do initHash fn <- getTTCFileName file ".ttc" - Just errs <- processMod file fn buildmsg mod res + Just errs <- logTime ("Elaborating " ++ file) $ + processMod file fn buildmsg mod res | Nothing => pure [] -- skipped it if isNil errs then - do defs <- get Ctxt - d <- getDirs - makeBuildDirectory (pathToNS (working_dir d) file) - writeToTTC !(get Syn) fn - mfn <- getTTCFileName file ".ttm" - writeToTTM mfn - pure [] + logTime ("Writing TTC/TTM for " ++ file) $ + do defs <- get Ctxt + d <- getDirs + makeBuildDirectory (pathToNS (working_dir d) file) + writeToTTC !(get Syn) fn + mfn <- getTTCFileName file ".ttm" + writeToTTM mfn + pure [] else pure errs) (\err => pure [err]) diff --git a/src/Idris/SetOptions.idr b/src/Idris/SetOptions.idr index b1c053b..26da398 100644 --- a/src/Idris/SetOptions.idr +++ b/src/Idris/SetOptions.idr @@ -45,6 +45,8 @@ preOptions (SetCG e :: opts) preOptions (PkgPath p :: opts) = do addPkgDir p preOptions opts +preOptions (Timing :: opts) + = setLogTimings True preOptions (_ :: opts) = preOptions opts -- Options to be processed after type checking. Returns whether execution diff --git a/src/TTImp/BindImplicits.idr b/src/TTImp/BindImplicits.idr index 7993dec..91eaadc 100644 --- a/src/TTImp/BindImplicits.idr +++ b/src/TTImp/BindImplicits.idr @@ -86,6 +86,12 @@ doBind ns (IAs fc s n pat) = IAs fc s n (doBind ns pat) doBind ns (IMustUnify fc r pat) = IMustUnify fc r (doBind ns pat) +doBind ns (IDelayed fc r ty) + = IDelayed fc r (doBind ns ty) +doBind ns (IDelay fc tm) + = IDelay fc (doBind ns tm) +doBind ns (IForce fc tm) + = IForce fc (doBind ns tm) doBind ns (IAlternative fc u alts) = IAlternative fc u (map (doBind ns) alts) doBind ns tm = tm diff --git a/src/TTImp/Elab.idr b/src/TTImp/Elab.idr index 3f1f7c0..d49f119 100644 --- a/src/TTImp/Elab.idr +++ b/src/TTImp/Elab.idr @@ -31,7 +31,7 @@ doPLetRenames ns drops (Bind fc n b@(PLet _ _ _) sc) doPLetRenames ns drops (Bind fc n b sc) = case lookup n ns of Just (c, n') => - Bind fc n' (setMultiplicity b c) + Bind fc n' (setMultiplicity b (max c (multiplicity b))) (doPLetRenames ns (n' :: drops) (renameTop n' sc)) Nothing => Bind fc n b (doPLetRenames ns drops sc) doPLetRenames ns drops sc = sc @@ -107,7 +107,8 @@ elabTermSub {vars} defining mode opts nest env env' sub tm ty linearCheck (getFC tm) rigc False env chktm -- Linearity checking looks in case blocks, so no -- need to check here. - else pure chktm + else do checkNoGuards + pure chktm -- Put the current hole state back to what it was (minus anything -- which has been solved in the meantime) @@ -128,7 +129,8 @@ elabTermSub {vars} defining mode opts nest env env' sub tm ty -- On the RHS, erase everything in a 0-multiplicity position -- (This doesn't do a full linearity check, just erases by -- type) - do chkErase <- linearCheck (getFC tm) rigc True env chktm + do dumpConstraints 2 False + chkErase <- linearCheck (getFC tm) rigc True env chktm pure (chktm, chkErase, chkty) _ => pure (chktm, chktm, chkty) where diff --git a/src/TTImp/Elab/App.idr b/src/TTImp/Elab/App.idr index 4dce102..e403bb9 100644 --- a/src/TTImp/Elab/App.idr +++ b/src/TTImp/Elab/App.idr @@ -30,6 +30,10 @@ getNameType rigc env fc x do rigSafe rigb rigc let bty = binderType (getBinder lv env) addNameType fc x env bty + when (isLinear rigb) $ + do est <- get EST + put EST + (record { linearUsed $= ((MkVar lv) :: ) } est) pure (Local fc (Just rigb) _ lv, gnf env bty) Nothing => do defs <- get Ctxt @@ -194,6 +198,27 @@ mutual solveIfUndefined env metavar soln = pure False + -- Defer elaborating anything which will be easier given a known target + -- type (ambiguity, cases, etc) + needsDelay : {auto c : Ref Ctxt Defs} -> + (knownRet : Bool) -> RawImp -> + Core Bool + needsDelay False _ = pure False + needsDelay True (IVar fc n) + = do defs <- get Ctxt + case !(lookupCtxtName n (gamma defs)) of + [] => pure False + [x] => pure False + _ => pure True + needsDelay True (IApp _ f _) = needsDelay True f + needsDelay True (IImplicitApp _ f _ _) = needsDelay True f + needsDelay True (ICase _ _ _ _) = pure True + needsDelay True (ILocal _ _ _) = pure True + needsDelay True (IUpdate _ _ _) = pure True + needsDelay True (IAlternative _ _ _) = pure True + needsDelay True (ISearch _ _) = pure True + needsDelay True _ = pure False + -- Check the rest of an application given the argument type and the -- raw argument. We choose elaboration order depending on whether we know -- the return type now. If we know it, elaborate the rest of the @@ -222,7 +247,7 @@ mutual then pure True else do sc' <- sc defs (toClosure defaultOpts env (Erased fc)) concrete defs env sc' - if kr then do + if !(needsDelay kr arg) then do nm <- genMVName x empty <- clearDefs defs metaty <- quote empty env aty @@ -300,6 +325,9 @@ mutual = do let argRig = rigMult rig rigb checkRestApp rig argRig elabinfo nest env fc (explApp (Just x)) tm x aty sc arg expargs impargs kr expty + -- Function type is delayed, so force the term and continue + checkAppWith rig elabinfo nest env fc tm (NDelayed dfc r ty) expargs impargs kr expty + = checkAppWith rig elabinfo nest env fc (TForce dfc tm) ty expargs impargs kr expty -- If there's no more arguments given, and the plicities of the type and -- the expected type line up, stop checkAppWith rig elabinfo nest env fc tm ty@(NBind tfc x (Pi rigb Implicit aty) sc) diff --git a/src/TTImp/Elab/Case.idr b/src/TTImp/Elab/Case.idr index b808889..0910a46 100644 --- a/src/TTImp/Elab/Case.idr +++ b/src/TTImp/Elab/Case.idr @@ -113,10 +113,20 @@ toRig1 First (b :: bs) else b :: bs toRig1 (Later p) (b :: bs) = b :: toRig1 p bs +toRig0 : {idx : Nat} -> .(IsVar name idx vs) -> Env Term vs -> Env Term vs +toRig0 First (b :: bs) = setMultiplicity b Rig0 :: bs +toRig0 (Later p) (b :: bs) = b :: toRig0 p bs + allow : Maybe (Var vs) -> Env Term vs -> Env Term vs allow Nothing env = env allow (Just (MkVar p)) env = toRig1 p env +-- If the name is used elsewhere, update its multiplicity so it's +-- not required to be used in the case block +updateMults : List (Var vs) -> Env Term vs -> Env Term vs +updateMults [] env = env +updateMults (MkVar p :: us) env = updateMults us (toRig0 p env) + shrinkImp : SubVars outer vars -> (Name, ImplBinding vars) -> Maybe (Name, ImplBinding outer) shrinkImp sub (n, NameBinding c tm ty) @@ -256,6 +266,10 @@ caseBlock {vars} rigc elabinfo fc nest env scr scrtm scrty caseRig alts expected scrn <- genVarName "scr" casen <- genCaseName (defining est) + -- Update environment so that linear bindings which were used + -- (esp. in the scrutinee!) are set to 0 in the case type + let env = updateMults (linearUsed est) env + -- The 'pre_env' is the environment we apply any local (nested) -- names to. Here *all* the names have multiplicity 0 (we're -- going to abstract over them all again, in case the case block diff --git a/src/TTImp/Elab/Check.idr b/src/TTImp/Elab/Check.idr index 248bead..0842e0d 100644 --- a/src/TTImp/Elab/Check.idr +++ b/src/TTImp/Elab/Check.idr @@ -105,13 +105,14 @@ record EState (vars : List Name) where -- Holes standing for pattern variables, which we'll delete -- once we're done elaborating allowDelay : Bool -- Delaying elaborators is okay. We can't nest delays. + linearUsed : List (Var vars) export data EST : Type where export initEStateSub : Int -> Env Term outer -> SubVars outer vars -> EState vars -initEStateSub n env sub = MkEState n env sub [] [] [] [] [] True +initEStateSub n env sub = MkEState n env sub [] [] [] [] [] True [] export initEState : Int -> Env Term vars -> EState vars @@ -130,7 +131,8 @@ weakenedEState {e} (bindIfUnsolved est) (lhsPatVars est) (allPatVars est) - (allowDelay est)) + (allowDelay est) + (map weaken (linearUsed est))) pure eref where wknTms : (Name, ImplBinding vs) -> @@ -158,7 +160,8 @@ strengthenedEState {n} {vars} c e fc env (bindIfUnsolved est) (lhsPatVars est) (allPatVars est) - (allowDelay est)) + (allowDelay est) + (mapMaybe dropTop (linearUsed est))) where dropSub : SubVars xs (y :: ys) -> Core (SubVars xs ys) dropSub (DropCons sub) = pure sub @@ -185,6 +188,10 @@ strengthenedEState {n} {vars} c e fc env _ => throw (GenericMsg fc ("Invalid as binding " ++ show f ++ " " ++ show xnf ++ " : " ++ show ynf)) + dropTop : (Var (n :: vs)) -> Maybe (Var vs) + dropTop (MkVar First) = Nothing + dropTop (MkVar (Later p)) = Just (MkVar p) + export inScope : {auto c : Ref Ctxt Defs} -> {auto e : Ref EST (EState vars)} -> @@ -208,6 +215,7 @@ updateEnv env sub bif st (lhsPatVars st) (allPatVars st) (allowDelay st) + (linearUsed st) export addBindIfUnsolved : Name -> RigCount -> Env Term vars -> Term vars -> Term vars -> @@ -220,6 +228,7 @@ addBindIfUnsolved hn r env tm ty st (lhsPatVars st) (allPatVars st) (allowDelay st) + (linearUsed st) clearBindIfUnsolved : EState vars -> EState vars clearBindIfUnsolved st @@ -229,6 +238,7 @@ clearBindIfUnsolved st (lhsPatVars st) (allPatVars st) (allowDelay st) + (linearUsed st) -- Clear the 'toBind' list, except for the names given export @@ -473,14 +483,15 @@ processDecl : {vars : _} -> -- in doing so. -- Returns a list of constraints which need to be solved for the conversion -- to work; if this is empty, the terms are convertible. -export -convert : {vars : _} -> +convertWithLazy + : {vars : _} -> {auto c : Ref Ctxt Defs} -> {auto u : Ref UST UState} -> {auto e : Ref EST (EState vars)} -> + (withLazy : Bool) -> FC -> ElabInfo -> Env Term vars -> Glued vars -> Glued vars -> Core UnifyResult -convert fc elabinfo env x y +convertWithLazy withLazy fc elabinfo env x y = let umode : UnifyMode = case elabMode elabinfo of InLHS _ => InLHS @@ -491,10 +502,14 @@ convert fc elabinfo env x y vs <- if isFromTerm x && isFromTerm y then do xtm <- getTerm x ytm <- getTerm y - unifyWithLazy umode fc env xtm ytm + if withLazy + then unifyWithLazy umode fc env xtm ytm + else unify umode fc env xtm ytm else do xnf <- getNF x ynf <- getNF y - unifyWithLazy umode fc env xnf ynf + if withLazy + then unifyWithLazy umode fc env xnf ynf + else unify umode fc env xnf ynf when (holesSolved vs) $ solveConstraints umode Normal pure vs) @@ -514,6 +529,15 @@ convert fc elabinfo env x y !(normaliseHoles defs env xtm) !(normaliseHoles defs env ytm) err)) +export +convert : {vars : _} -> + {auto c : Ref Ctxt Defs} -> + {auto u : Ref UST UState} -> + {auto e : Ref EST (EState vars)} -> + FC -> ElabInfo -> Env Term vars -> Glued vars -> Glued vars -> + Core UnifyResult +convert = convertWithLazy False + -- Check whether the type we got for the given type matches the expected -- type. -- Returns the term and its type. @@ -529,11 +553,14 @@ checkExp : {vars : _} -> (got : Glued vars) -> (expected : Maybe (Glued vars)) -> Core (Term vars, Glued vars) checkExp rig elabinfo env fc tm got (Just exp) - = do vs <- convert fc elabinfo env got exp + = do vs <- convertWithLazy True fc elabinfo env got exp case (constraints vs) of [] => case addLazy vs of NoLazy => pure (tm, got) - AddForce => pure (TForce fc tm, exp) + AddForce => do logTerm 0 "Force" tm + logGlue 0 "Got" env got + logGlue 0 "Exp" env exp + pure (TForce fc tm, exp) AddDelay r => do ty <- getTerm got pure (TDelay fc r ty tm, exp) cs => do defs <- get Ctxt diff --git a/src/TTImp/Elab/Local.idr b/src/TTImp/Elab/Local.idr index 73338f2..b8ce54a 100644 --- a/src/TTImp/Elab/Local.idr +++ b/src/TTImp/Elab/Local.idr @@ -51,7 +51,7 @@ checkLocal {vars} rig elabinfo nest env fc nestdecls scope expty applyEnv outer inner = do n' <- resolveName (Nested outer inner) pure (inner, (Just (Resolved n'), - \fc, nt => applyToFull fc + \fc, nt => applyTo fc (Ref fc nt (Resolved n')) env)) -- Update the names in the declarations to the new 'nested' names. diff --git a/src/TTImp/TTImp.idr b/src/TTImp/TTImp.idr index 39a248d..ab2edfd 100644 --- a/src/TTImp/TTImp.idr +++ b/src/TTImp/TTImp.idr @@ -371,6 +371,9 @@ findImplicits (IMustUnify fc r pat) = findImplicits pat findImplicits (IAlternative fc u alts) = concatMap findImplicits alts +findImplicits (IDelayed fc _ ty) = findImplicits ty +findImplicits (IDelay fc tm) = findImplicits tm +findImplicits (IForce fc tm) = findImplicits tm findImplicits (IBindVar _ n) = [n] findImplicits tm = [] diff --git a/tests/idris2/basic001/expected b/tests/idris2/basic001/expected index 7d394f0..bdc009f 100644 --- a/tests/idris2/basic001/expected +++ b/tests/idris2/basic001/expected @@ -1,9 +1,9 @@ 1/1: Building Vect (Vect.idr) Welcome to Idris 2 version 0.0. Fingers crossed! Main> Main> Cons (S Z) (Cons (S (S Z)) []) : Vect (S (S Z)) Nat -Main> (interactive):1:22--1:25:When unifying Vect Z ?a and Vect (S Z) ?a +Main> (interactive):1:28--1:51:When unifying Vect (S (S Z)) Nat and Vect (S Z) Nat Mismatch between: - Z -and S ?k +and + Z Main> Bye for now! diff --git a/tests/ttimp/basic003/expected b/tests/ttimp/basic003/expected index c351295..dd8fe06 100644 --- a/tests/ttimp/basic003/expected +++ b/tests/ttimp/basic003/expected @@ -1,8 +1,8 @@ Processing as TTImp Written TTC -Yaffle> Main.foo : (%pi Rig0 Explicit Just {k:45} Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just m Main.Nat (%let Rig0 n Main.Nat (Main.S {k:45}) (%pi RigW Explicit Nothing a (%pi RigW Explicit Nothing ((Main.Vect {k:45}) a) (%pi RigW Explicit Nothing ((Main.Vect m) a) ((Main.Vect ((Main.plus {k:45}) m)) a)))))))) +Yaffle> Main.foo : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just {k:20} Main.Nat (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi RigW Explicit Nothing ((Main.Vect {k:20}) a) (%pi RigW Explicit Nothing a (%let Rig0 n Main.Nat (Main.S {k:20}) ((Main.Vect ((Main.plus {k:20}) m)) a)))))))) Yaffle> Bye for now! Processing as TTC Read TTC -Yaffle> Main.foo : (%pi Rig0 Explicit Just {k:45} Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just m Main.Nat (%let Rig0 n ? (Main.S {k:45}) (%pi RigW Explicit Nothing a (%pi RigW Explicit Nothing ((Main.Vect {k:45}) a) (%pi RigW Explicit Nothing ((Main.Vect m) a) ((Main.Vect ((Main.plus {k:45}) m)) a)))))))) +Yaffle> Main.foo : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just {k:20} Main.Nat (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi RigW Explicit Nothing ((Main.Vect {k:20}) a) (%pi RigW Explicit Nothing a (%let Rig0 n ? (Main.S {k:20}) ((Main.Vect ((Main.plus {k:20}) m)) a)))))))) Yaffle> Bye for now! diff --git a/tests/ttimp/basic006/expected b/tests/ttimp/basic006/expected index 3cea5cd..d078cfd 100644 --- a/tests/ttimp/basic006/expected +++ b/tests/ttimp/basic006/expected @@ -2,5 +2,5 @@ Processing as TTImp Written TTC Yaffle> ((Main.Just [Just a = ((Main.Vect.Vect (Main.S Main.Z)) Integer)]) ((((Main.Vect.Cons [Just k = Main.Z]) [Just a = Integer]) 1) (Main.Vect.Nil [Just a = Integer]))) Yaffle> ((Main.MkInfer [Just a = (Main.List.List Integer)]) (((Main.List.Cons [Just a = Integer]) 1) (Main.List.Nil [Just a = Integer]))) -Yaffle> (repl):1:9--1:12:Ambiguous elaboration [($resolved102 ?Main.{a:71}_[]), ($resolved78 ?Main.{a:71}_[])] +Yaffle> (repl):1:9--1:12:Ambiguous elaboration [($resolved94 ?Main.{a:52}_[]), ($resolved78 ?Main.{a:52}_[])] Yaffle> Bye for now! diff --git a/tests/ttimp/coverage001/expected b/tests/ttimp/coverage001/expected index e2394b1..0873952 100644 --- a/tests/ttimp/coverage001/expected +++ b/tests/ttimp/coverage001/expected @@ -2,9 +2,9 @@ Processing as TTImp Written TTC Yaffle> Bye for now! Processing as TTImp -Vect2.yaff:25:1--26:1:pat 0 {b:34} : Type => pat 0 {a:33} : Type => ($resolved102 {b:34}[1] {a:33}[0] $resolved77 ($resolved92 {a:33}[0]) ($resolved92 {b:34}[1])) is not a valid impossible pattern because it typechecks +Vect2.yaff:25:1--26:1:pat 0 {b:21} : Type => pat 0 {a:20} : Type => ($resolved91 {b:21}[1] {a:20}[0] $resolved75 ($resolved82 {a:20}[0]) ($resolved82 {b:21}[1])) is not a valid impossible pattern because it typechecks Yaffle> Bye for now! Processing as TTImp Vect3.yaff:25:1--26:1:Not a valid impossible pattern: - Vect3.yaff:25:9--25:11:Type mismatch: $resolved76 and ($resolved90 ?Main.{n:28}_[] ?Main.{b:26}_[]) + Vect3.yaff:25:9--25:11:Type mismatch: $resolved74 and ($resolved80 ?Main.{n:17}_[] ?Main.{b:15}_[]) Yaffle> Bye for now! diff --git a/tests/ttimp/coverage002/expected b/tests/ttimp/coverage002/expected index ee783b7..85c90bc 100644 --- a/tests/ttimp/coverage002/expected +++ b/tests/ttimp/coverage002/expected @@ -2,6 +2,6 @@ Processing as TTImp Written TTC Yaffle> Main.lookup: All cases covered Yaffle> Main.lookup': -($resolved132 {arg:0} {arg:1} (Main.FZ {m:0}) {arg:3}) -Yaffle> Main.lookup'': Calls non covering function $resolved132 +($resolved114 {arg:0} {arg:1} (Main.FZ {m:0}) {arg:3}) +Yaffle> Main.lookup'': Calls non covering function $resolved114 Yaffle> Bye for now! diff --git a/tests/ttimp/dot001/expected b/tests/ttimp/dot001/expected index 1c64727..6488034 100644 --- a/tests/ttimp/dot001/expected +++ b/tests/ttimp/dot001/expected @@ -2,14 +2,14 @@ Processing as TTImp Written TTC Yaffle> Bye for now! Processing as TTImp -Dot2.yaff:15:1--16:1:When elaborating left hand side of $resolved92: -Dot2.yaff:15:10--15:15:Can't match on ($resolved73 ?{P:n:92}_[] ?{P:m:92}_[]) (Not a constructor application or primitive) - it elaborates to ($resolved73 ?{P:n:92}_[] ?{P:n:92}_[]) +Dot2.yaff:15:1--16:1:When elaborating left hand side of $resolved79: +Dot2.yaff:15:10--15:15:Can't match on ($resolved73 ?{P:n:79}_[] ?{P:m:79}_[]) (Not a constructor application or primitive) - it elaborates to ($resolved73 ?{P:n:79}_[] ?{P:n:79}_[]) Yaffle> Bye for now! Processing as TTImp -Dot3.yaff:18:1--20:1:When elaborating left hand side of $resolved100: -Dot3.yaff:18:10--18:15:Can't match on ($resolved73 ?{P:x:100}_[] ?{P:y:100}_[]) (Not a constructor application or primitive) - it elaborates to ($resolved73 ?Main.{_:30}_[] ?Main.{_:29}_[]) +Dot3.yaff:18:1--20:1:When elaborating left hand side of $resolved82: +Dot3.yaff:18:10--18:15:Can't match on ($resolved73 ?{P:x:82}_[] ?{P:y:82}_[]) (Not a constructor application or primitive) - it elaborates to ($resolved73 ?Main.{_:8}_[] ?Main.{_:9}_[]) Yaffle> Bye for now! Processing as TTImp -Dot4.yaff:17:1--19:1:When elaborating left hand side of $resolved100: -Dot4.yaff:17:10--17:15:Can't match on ($resolved73 ?Main.{_:32}_[] ?Main.{_:31}_[]) (Not a constructor application or primitive) - it elaborates to ($resolved73 ?{P:x:100}_[] ?{P:y:100}_[]) +Dot4.yaff:17:1--19:1:When elaborating left hand side of $resolved82: +Dot4.yaff:17:10--17:15:Can't match on ($resolved73 ?Main.{_:7}_[] ?Main.{_:8}_[]) (Not a constructor application or primitive) - it elaborates to ($resolved73 ?{P:x:82}_[] ?{P:y:82}_[]) Yaffle> Bye for now! diff --git a/tests/ttimp/eta001/expected b/tests/ttimp/eta001/expected index a970f5c..392602a 100644 --- a/tests/ttimp/eta001/expected +++ b/tests/ttimp/eta001/expected @@ -1,5 +1,5 @@ Processing as TTImp Written TTC -Yaffle> ((Main.Refl [Just {b:15} = Main.Nat]) [Just x = (Main.S (Main.S (Main.S (Main.S Main.Z))))]) +Yaffle> ((Main.Refl [Just {b:7} = Main.Nat]) [Just x = (Main.S (Main.S (Main.S (Main.S Main.Z))))]) Yaffle> Main.etaGood1 : ((((Main.Eq [Just b = (%pi RigW Explicit Nothing Integer (%pi RigW Explicit Nothing Integer Main.Test))]) [Just a = (%pi RigW Explicit Nothing Integer (%pi RigW Explicit Nothing Integer Main.Test))]) Main.MkTest) (%lam RigW Explicit Just x Integer (%lam RigW Explicit Just y Integer ((Main.MkTest x) y)))) Yaffle> Bye for now! diff --git a/tests/ttimp/eta002/expected b/tests/ttimp/eta002/expected index 8327ce6..c4e7876 100644 --- a/tests/ttimp/eta002/expected +++ b/tests/ttimp/eta002/expected @@ -1,4 +1,4 @@ Processing as TTImp -Eta.yaff:16:10--17:1:When unifying: ($resolved84 ((x : Char) -> ((y : ?Main.{_:20}_[x[0]]) -> $resolved92)) ((x : Char) -> ((y : ?Main.{_:20}_[x[0]]) -> $resolved92)) ?Main.{x:26}_[] ?Main.{x:26}_[]) and ($resolved84 ((x : Char) -> ((y : ?Main.{_:20}_[x[0]]) -> $resolved92)) (({arg:16} : Integer) -> (({arg:17} : Integer) -> $resolved92)) $resolved93 \x : Char => \y : ?Main.{_:20}_[x[0]] => ($resolved93 ?Main.{_:24}_[x[1], y[0]] ?Main.{_:23}_[x[1], y[0]])) +Eta.yaff:16:10--17:1:When unifying: ($resolved76 ((x : Char) -> ((y : ?Main.{_:12}_[x[0]]) -> $resolved84)) ((x : Char) -> ((y : ?Main.{_:12}_[x[0]]) -> $resolved84)) ?Main.{x:16}_[] ?Main.{x:16}_[]) and ($resolved76 ((x : Char) -> ((y : ?Main.{_:12}_[x[0]]) -> $resolved84)) (({arg:8} : Integer) -> (({arg:9} : Integer) -> $resolved84)) $resolved85 \x : Char => \y : ?Main.{_:12}_[x[0]] => ($resolved85 ?Main.{_:13}_[x[1], y[0]] ?Main.{_:14}_[x[1], y[0]])) Eta.yaff:16:10--17:1:Type mismatch: Char and Integer Yaffle> Bye for now! diff --git a/tests/ttimp/qtt002/expected b/tests/ttimp/qtt002/expected index cc3adc4..8ffd0b9 100644 --- a/tests/ttimp/qtt002/expected +++ b/tests/ttimp/qtt002/expected @@ -1,6 +1,6 @@ Processing as TTImp Written TTC -Yaffle> Main.foo : (%pi Rig0 Explicit Just {k:36} Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just m Main.Nat (%let Rig0 n Main.Nat (Main.S (Main.S {k:36})) (%pi RigW Explicit Nothing a (%pi Rig0 Explicit Just y a (%pi Rig0 Explicit Just ws ((Main.Vect {k:36}) a) (%let Rig1 zs ((Main.Vect (Main.S {k:36})) a) ((((Main.Cons [Just k = {k:36}]) [Just a = a]) y) ws) (%pi RigW Explicit Nothing ((Main.Vect m) a) ((Main.Vect ((Main.plus n@((Main.S (Main.S {k:36})))) m)) a)))))))))) -Yaffle> Main.bar : (%pi Rig0 Explicit Just n Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just xs ((Main.Vect n) a) (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just {k:82} Main.Nat (%let Rig0 n Main.Nat (Main.S {k:82}) (%pi RigW Explicit Just x a (%pi Rig1 Explicit Just zs ((Main.Vect {k:82}) a) (%let Rig0 xs ((Main.Vect n@((Main.S {k:82}))) a) ((((Main.Cons [Just k = {k:82}]) [Just a = a]) x) zs) ((Main.Vect ((Main.plus n@((Main.S {k:82}))) m)) a)))))))))))))) -Yaffle> Main.baz : (%pi Rig0 Explicit Just n Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just xs ((Main.Vect n) a) (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just {k:129} Main.Nat (%let Rig0 n Main.Nat (Main.S {k:129}) (%pi RigW Explicit Just x a (%pi Rig0 Explicit Just zs ((Main.Vect {k:129}) a) (%let Rig0 xs ((Main.Vect n@((Main.S {k:129}))) a) ((((Main.Cons [Just k = {k:129}]) [Just a = a]) x) zs) (%let Rig1 ts ((Main.Vect {k:129}) a) zs ((Main.Vect ((Main.plus n@((Main.S {k:129}))) m)) a))))))))))))))) +Yaffle> Main.foo : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just {k:14} Main.Nat (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just ws ((Main.Vect {k:14}) a) (%pi Rig0 Explicit Just y a (%let Rig1 zs ((Main.Vect (Main.S {k:14})) a) ((((Main.Cons [Just k = {k:14}]) [Just a = a]) y) ws) (%pi RigW Explicit Nothing a (%let Rig0 n Main.Nat (Main.S (Main.S {k:14})) ((Main.Vect ((Main.plus (Main.S (Main.S {k:14}))) m)) a)))))))))) +Yaffle> Main.bar : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just n Main.Nat (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just xs ((Main.Vect n) a) (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just {k:41} Main.Nat (%pi Rig1 Explicit Just zs ((Main.Vect {k:41}) a) (%pi RigW Explicit Just x a (%let Rig0 xs ((Main.Vect (Main.S {k:41})) a) ((((Main.Cons [Just k = {k:41}]) [Just a = a]) x) zs) (%let Rig0 n Main.Nat (Main.S {k:41}) ((Main.Vect ((Main.plus (Main.S {k:41})) m)) a)))))))))))))) +Yaffle> Main.baz : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just n Main.Nat (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just xs ((Main.Vect n) a) (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just {k:69} Main.Nat (%pi Rig0 Explicit Just zs ((Main.Vect {k:69}) a) (%pi RigW Explicit Just x a (%let Rig0 xs ((Main.Vect (Main.S {k:69})) a) ((((Main.Cons [Just k = {k:69}]) [Just a = a]) x) zs) (%let Rig0 n Main.Nat (Main.S {k:69}) (%let Rig1 ts ((Main.Vect {k:69}) a) zs ((Main.Vect ((Main.plus (Main.S {k:69})) m)) a))))))))))))))) Yaffle> Bye for now! diff --git a/tests/ttimp/search001/expected b/tests/ttimp/search001/expected index 02886f5..501ebcb 100644 --- a/tests/ttimp/search001/expected +++ b/tests/ttimp/search001/expected @@ -1,6 +1,6 @@ Processing as TTImp Written TTC -Yaffle> (((((Main.There [Just {a:17} = Main.Nat]) [Just y = (Main.S Main.Z)]) [Just xs = (((Main.Cons [Just a = Main.Nat]) Main.Z) (Main.Nil [Just a = Main.Nat]))]) [Just x = Main.Z]) (((Main.Here [Just {a:10} = Main.Nat]) [Just xs = (Main.Nil [Just a = Main.Nat])]) [Just x = Main.Z])) -Yaffle> (((Main.Here [Just {a:10} = Main.Nat]) [Just xs = (((Main.Cons [Just a = Main.Nat]) Main.Z) (Main.Nil [Just a = Main.Nat]))]) [Just x = (Main.S Main.Z)]) +Yaffle> (((((Main.There [Just {impty:14} = Main.Nat]) [Just y = (Main.S Main.Z)]) [Just xs = (((Main.Cons [Just a = Main.Nat]) Main.Z) (Main.Nil [Just a = Main.Nat]))]) [Just x = Main.Z]) (((Main.Here [Just {a:8} = Main.Nat]) [Just xs = (Main.Nil [Just a = Main.Nat])]) [Just x = Main.Z])) +Yaffle> (((Main.Here [Just {a:8} = Main.Nat]) [Just xs = (((Main.Cons [Just a = Main.Nat]) Main.Z) (Main.Nil [Just a = Main.Nat]))]) [Just x = (Main.S Main.Z)]) Yaffle> ((((Main.MkPair [Just b = Integer]) [Just a = String]) "b") 94) Yaffle> Bye for now! diff --git a/tests/ttimp/search004/Functor.yaff b/tests/ttimp/search004/Functor.yaff index bded682..b36c020 100644 --- a/tests/ttimp/search004/Functor.yaff +++ b/tests/ttimp/search004/Functor.yaff @@ -67,7 +67,7 @@ namespace Vect tryMap : Nat -> Nat -> List Nat tryMap $x $y = map (plus x) (Cons y (Cons (S y) Nil)) -tryVMap : Nat -> Nat -> Vect ? Nat +tryVMap : Nat -> Nat -> Vect (S (S Z)) Nat tryVMap $x $y = map (plus x) (Cons y (Cons (S y) Nil)) diff --git a/tests/ttimp/search005/expected b/tests/ttimp/search005/expected index 49d8bd8..75d73f6 100644 --- a/tests/ttimp/search005/expected +++ b/tests/ttimp/search005/expected @@ -1,8 +1,8 @@ Processing as TTImp Written TTC -Yaffle> \0 a : Type => \0 m : Main.Nat => \ys : (Main.Vect m[0] a[1]) => ys[0] -Yaffle> \0 {k:49} : Main.Nat => \0 a : Type => \0 m : Main.Nat => \x : a[1] => \xs : (Main.Vect {k:49}[3] a[2]) => \ys : (Main.Vect m[2] a[3]) => (Main.Cons (Main.plus {k:49}[5] m[3]) a[4] x[2] (Main.append m[3] a[4] {k:49}[5] xs[1] ys[0])) -Yaffle> [((Main.app2 (Main.Nil [Just a = _])) $y) = y, ((Main.app2 ((((Main.Cons [Just k = _]) [Just a = _]) $x) $z)) $y) = ((((Main.Cons [Just k = ((Main.plus {_:242}) m)]) [Just a = a]) x) (((((Main.app2 [Just m = m]) [Just a = a]) [Just n = {_:242}]) z) y))] -Yaffle> [((Main.zip (Main.Nil [Just a = _])) $y) = (Main.Nil [Just a = ((Main.Pair a) b)]), ((Main.zip ((((Main.Cons [Just k = _]) [Just a = _]) $x) $z)) ((((Main.Cons [Just k = _]) [Just a = _]) $y) $w)) = ((((Main.Cons [Just k = {_:368}]) [Just a = ((Main.Pair a) b)]) ((((Main.MkPair [Just b = b]) [Just a = a]) x) y)) (((((Main.zip [Just b = b]) [Just a = a]) [Just n = {_:368}]) z) w))] -Yaffle> [(((Main.zipWith $f) (Main.Nil [Just a = _])) $y) = (Main.Nil [Just a = c]), (((Main.zipWith $f) ((((Main.Cons [Just k = _]) [Just a = _]) $x) $z)) ((((Main.Cons [Just k = _]) [Just a = _]) $y) $w)) = ((((Main.Cons [Just k = {_:497}]) [Just a = c]) ((f x) y)) (((((((Main.zipWith [Just n = {_:497}]) [Just c = c]) [Just b = b]) [Just a = a]) f) z) w))] +Yaffle> \0 m : Main.Nat => \0 a : Type => \ys : (Main.Vect m[1] a[0]) => ys[0] +Yaffle> \0 m : Main.Nat => \0 a : Type => \0 {k:22} : Main.Nat => \ys : (Main.Vect m[2] a[1]) => \xs : (Main.Vect {k:22}[1] a[2]) => \x : a[3] => (Main.Cons (Main.plus {k:22}[3] m[5]) a[4] x[0] (Main.append m[5] a[4] {k:22}[3] xs[1] ys[2])) +Yaffle> [((Main.app2 (Main.Nil [Just a = _])) $y) = y, ((Main.app2 ((((Main.Cons [Just k = _]) [Just a = _]) $x) $z)) $y) = ((((Main.Cons [Just k = ((Main.plus {_:191}) m)]) [Just a = a]) x) (((((Main.app2 [Just m = m]) [Just a = a]) [Just n = {_:191}]) z) y))] +Yaffle> [((Main.zip (Main.Nil [Just a = _])) $y) = (Main.Nil [Just a = ((Main.Pair a) b)]), ((Main.zip ((((Main.Cons [Just k = _]) [Just a = _]) $x) $z)) ((((Main.Cons [Just k = _]) [Just a = _]) $y) $w)) = ((((Main.Cons [Just k = {_:298}]) [Just a = ((Main.Pair a) b)]) ((((Main.MkPair [Just b = b]) [Just a = a]) x) y)) (((((Main.zip [Just b = b]) [Just a = a]) [Just n = {_:298}]) z) w))] +Yaffle> [(((Main.zipWith $f) (Main.Nil [Just a = _])) $y) = (Main.Nil [Just a = c]), (((Main.zipWith $f) ((((Main.Cons [Just k = _]) [Just a = _]) $x) $z)) ((((Main.Cons [Just k = _]) [Just a = _]) $y) $w)) = ((((Main.Cons [Just k = {_:448}]) [Just a = c]) ((f x) y)) (((((((Main.zipWith [Just n = {_:448}]) [Just c = c]) [Just b = b]) [Just a = a]) f) z) w))] Yaffle> Bye for now! diff --git a/tests/ttimp/total002/expected b/tests/ttimp/total002/expected index 46c2b55..65a7907 100644 --- a/tests/ttimp/total002/expected +++ b/tests/ttimp/total002/expected @@ -5,5 +5,5 @@ Yaffle> Main.ack is total Yaffle> Main.foo is total Yaffle> Main.foo' is total Yaffle> Main.foom is total -Yaffle> Main.pfoom is not terminating due to recursive path $resolved158 -> Main.pfoom -> Main.pfoom +Yaffle> Main.pfoom is not terminating due to recursive path $resolved95 -> Main.pfoom -> Main.pfoom Yaffle> Bye for now! diff --git a/tests/ttimp/with001/expected b/tests/ttimp/with001/expected index 954ce32..edaba20 100644 --- a/tests/ttimp/with001/expected +++ b/tests/ttimp/with001/expected @@ -3,5 +3,5 @@ Written TTC Yaffle> (Main.Odd (Main.S Main.Z)) Yaffle> (Main.Even (Main.S Main.Z)) Yaffle> (Main.Nothing [Just a = ((((Main.Eq [Just b = ((Main.Pair Main.Nat) Main.Nat)]) [Just a = ((Main.Pair Main.Nat) Main.Nat)]) ((((Main.MkPair [Just b = Main.Nat]) [Just a = Main.Nat]) Main.Z) (Main.S Main.Z))) ((((Main.MkPair [Just b = Main.Nat]) [Just a = Main.Nat]) (Main.S Main.Z)) (Main.S (Main.S Main.Z))))]) -Yaffle> ((Main.Just [Just a = ((((Main.Eq [Just b = ((Main.Pair Main.Nat) Main.Nat)]) [Just a = ((Main.Pair Main.Nat) Main.Nat)]) ((((Main.MkPair [Just b = Main.Nat]) [Just a = Main.Nat]) Main.Z) (Main.S Main.Z))) ((((Main.MkPair [Just b = Main.Nat]) [Just a = Main.Nat]) Main.Z) (Main.S Main.Z)))]) ((Main.Refl [Just {b:15} = ((Main.Pair Main.Nat) Main.Nat)]) [Just x = ((((Main.MkPair [Just b = Main.Nat]) [Just a = Main.Nat]) Main.Z) (Main.S Main.Z))])) +Yaffle> ((Main.Just [Just a = ((((Main.Eq [Just b = ((Main.Pair Main.Nat) Main.Nat)]) [Just a = ((Main.Pair Main.Nat) Main.Nat)]) ((((Main.MkPair [Just b = Main.Nat]) [Just a = Main.Nat]) Main.Z) (Main.S Main.Z))) ((((Main.MkPair [Just b = Main.Nat]) [Just a = Main.Nat]) Main.Z) (Main.S Main.Z)))]) ((Main.Refl [Just {b:7} = ((Main.Pair Main.Nat) Main.Nat)]) [Just x = ((((Main.MkPair [Just b = Main.Nat]) [Just a = Main.Nat]) Main.Z) (Main.S Main.Z))])) Yaffle> Bye for now!