diff --git a/libs/base/Data/List.idr b/libs/base/Data/List.idr index 7a21df2..577c0bf 100644 --- a/libs/base/Data/List.idr +++ b/libs/base/Data/List.idr @@ -99,3 +99,9 @@ data NonEmpty : (xs : List a) -> Type where export Uninhabited (NonEmpty []) where uninhabited IsNonEmpty impossible + +||| Convert any Foldable structure to a list. +export +toList : Foldable t => t a -> List a +toList = foldr (::) [] + diff --git a/libs/base/Data/Maybe.idr b/libs/base/Data/Maybe.idr index db664f3..f5f4e41 100644 --- a/libs/base/Data/Maybe.idr +++ b/libs/base/Data/Maybe.idr @@ -25,3 +25,33 @@ isItJust : (v : Maybe a) -> Dec (IsJust v) isItJust (Just x) = Yes ItIsJust isItJust Nothing = No absurd +||| Convert a `Maybe a` value to an `a` value by providing a default `a` value +||| in the case that the `Maybe` value is `Nothing`. +public export +fromMaybe : (Lazy a) -> Maybe a -> a +fromMaybe def Nothing = def +fromMaybe def (Just j) = j + +||| Returns `Just` the given value if the conditional is `True` +||| and `Nothing` if the conditional is `False`. +public export +toMaybe : Bool -> Lazy a -> Maybe a +toMaybe True j = Just j +toMaybe False j = Nothing + +export +justInjective : {x : t} -> {y : t} -> (Just x = Just y) -> x = y +justInjective Refl = Refl + +||| Convert a `Maybe a` value to an `a` value, using `neutral` in the case +||| that the `Maybe` value is `Nothing`. +public export +lowerMaybe : Monoid a => Maybe a -> a +lowerMaybe Nothing = neutral +lowerMaybe (Just x) = x + +||| Returns `Nothing` when applied to `neutral`, and `Just` the value otherwise. +export +raiseToMaybe : (Monoid a, Eq a) => a -> Maybe a +raiseToMaybe x = if x == neutral then Nothing else Just x + diff --git a/libs/base/Data/Nat.idr b/libs/base/Data/Nat.idr index 816723e..aa46802 100644 --- a/libs/base/Data/Nat.idr +++ b/libs/base/Data/Nat.idr @@ -232,6 +232,25 @@ lcm _ Z = Z lcm Z _ = Z lcm a (S b) = divNat (a * (S b)) (gcd a (S b)) +-------------------------------------------------------------------------------- +-- An informative comparison view +-------------------------------------------------------------------------------- +public export +data CmpNat : Nat -> Nat -> Type where + CmpLT : (y : _) -> CmpNat x (x + S y) + CmpEQ : CmpNat x x + CmpGT : (x : _) -> CmpNat (y + S x) y + +export +total cmp : (x, y : Nat) -> CmpNat x y +cmp Z Z = CmpEQ +cmp Z (S k) = CmpLT _ +cmp (S k) Z = CmpGT _ +cmp (S x) (S y) with (cmp x y) + cmp (S x) (S (x + (S k))) | CmpLT k = CmpLT k + cmp (S x) (S x) | CmpEQ = CmpEQ + cmp (S (y + (S k))) (S y) | CmpGT k = CmpGT k + -- Proofs on + export @@ -397,3 +416,5 @@ multOneRightNeutral (S left) = let inductiveHypothesis = multOneRightNeutral left in rewrite inductiveHypothesis in Refl + + diff --git a/libs/base/Data/Vect.idr b/libs/base/Data/Vect.idr index 5b013aa..540f3f9 100644 --- a/libs/base/Data/Vect.idr +++ b/libs/base/Data/Vect.idr @@ -4,6 +4,8 @@ import Data.List import Data.Nat import public Data.Fin +import Decidable.Equality + public export data Vect : (len : Nat) -> (elem : Type) -> Type where ||| Empty vector @@ -566,5 +568,252 @@ public export elemIndices : Eq elem => elem -> Vect m elem -> List (Fin m) elemIndices = elemIndicesBy (==) +-------------------------------------------------------------------------------- +-- Filters +-------------------------------------------------------------------------------- + +||| Find all elements of a vector that satisfy some test +||| +||| ```idris example +||| filter (< 3) (fromList [1,2,3,4]) +||| ``` +filter : (elem -> Bool) -> Vect len elem -> (p ** Vect p elem) +filter p [] = ( _ ** [] ) +filter p (x::xs) = + let (_ ** tail) = filter p xs + in if p x then + (_ ** x::tail) + else + (_ ** tail) + +||| Make the elements of some vector unique by some test +||| +||| ```idris example +||| nubBy (==) (fromList [1,2,2,3,4,4]) +||| ``` +-- nubBy : (elem -> elem -> Bool) -> Vect len elem -> (p ** Vect p elem) +-- nubBy = nubBy' [] +-- where +-- nubBy' : forall len . Vect m elem -> (elem -> elem -> Bool) -> Vect len elem -> (p ** Vect p elem) +-- nubBy' acc p [] = (_ ** []) +-- nubBy' acc p (x::xs) with (elemBy p x acc) +-- nubBy' acc p (x :: xs) | True = nubBy' acc p xs +-- nubBy' acc p (x :: xs) | False with (nubBy' (x::acc) p xs) +-- nubBy' acc p (x :: xs) | False | (_ ** tail) = (_ ** x::tail) +-- +-- ||| Make the elements of some vector unique by the default Boolean equality +-- ||| +-- ||| ```idris example +-- ||| nub (fromList [1,2,2,3,4,4]) +-- ||| ``` +-- nub : Eq elem => Vect len elem -> (p ** Vect p elem) +-- nub = nubBy (==) + +||| Delete first element from list according to some test +||| +||| ```idris example +||| deleteBy (<) 3 (fromList [1,2,2,3,4,4]) +||| ``` +deleteBy : {len : _} -> -- needed for the dependent pair + (elem -> elem -> Bool) -> elem -> Vect len elem -> (p ** Vect p elem) +deleteBy _ _ [] = (_ ** []) +deleteBy eq x (y::ys) = + let (len ** zs) = deleteBy eq x ys + in if x `eq` y then (_ ** ys) else (S len ** y ::zs) + +||| Delete first element from list equal to the given one +||| +||| ```idris example +||| delete 2 (fromList [1,2,2,3,4,4]) +||| ``` +delete : {len : _} -> + Eq elem => elem -> Vect len elem -> (p ** Vect p elem) +delete = deleteBy (==) + +-------------------------------------------------------------------------------- +-- Splitting and breaking lists +-------------------------------------------------------------------------------- + +||| A tuple where the first element is a `Vect` of the `n` first elements and +||| the second element is a `Vect` of the remaining elements of the original. +||| It is equivalent to `(take n xs, drop n xs)` (`splitAtTakeDrop`), +||| but is more efficient. +||| +||| @ n the index to split at +||| @ xs the `Vect` to split in two +||| +||| ```idris example +||| splitAt 2 (fromList [1,2,3,4]) +||| ``` +splitAt : (n : Nat) -> (xs : Vect (n + m) elem) -> (Vect n elem, Vect m elem) +splitAt Z xs = ([], xs) +splitAt (S k) (x :: xs) with (splitAt k {m} xs) + splitAt (S k) (x :: xs) | (tk, dr) = (x :: tk, dr) + +||| A tuple where the first element is a `Vect` of the `n` elements passing given test +||| and the second element is a `Vect` of the remaining elements of the original. +||| +||| ```idris example +||| partition (== 2) (fromList [1,2,3,2,4]) +||| ``` +partition : (elem -> Bool) -> Vect len elem -> ((p ** Vect p elem), (q ** Vect q elem)) +partition p [] = ((_ ** []), (_ ** [])) +partition p (x::xs) = + let ((leftLen ** lefts), (rightLen ** rights)) = partition p xs in + if p x then + ((S leftLen ** x::lefts), (rightLen ** rights)) + else + ((leftLen ** lefts), (S rightLen ** x::rights)) + +-------------------------------------------------------------------------------- +-- Predicates +-------------------------------------------------------------------------------- + +||| Verify vector prefix +||| +||| ```idris example +||| isPrefixOfBy (==) (fromList [1,2]) (fromList [1,2,3,4]) +||| ``` +isPrefixOfBy : (elem -> elem -> Bool) -> Vect m elem -> Vect len elem -> Bool +isPrefixOfBy p [] right = True +isPrefixOfBy p left [] = False +isPrefixOfBy p (x::xs) (y::ys) = p x y && isPrefixOfBy p xs ys + +||| Verify vector prefix +||| +||| ```idris example +||| isPrefixOf (fromList [1,2]) (fromList [1,2,3,4]) +||| ``` +isPrefixOf : Eq elem => Vect m elem -> Vect len elem -> Bool +isPrefixOf = isPrefixOfBy (==) + +||| Verify vector suffix +||| +||| ```idris example +||| isSuffixOfBy (==) (fromList [3,4]) (fromList [1,2,3,4]) +||| ``` +isSuffixOfBy : (elem -> elem -> Bool) -> Vect m elem -> Vect len elem -> Bool +isSuffixOfBy p left right = isPrefixOfBy p (reverse left) (reverse right) + +||| Verify vector suffix +||| +||| ```idris example +||| isSuffixOf (fromList [3,4]) (fromList [1,2,3,4]) +||| ``` +isSuffixOf : Eq elem => Vect m elem -> Vect len elem -> Bool +isSuffixOf = isSuffixOfBy (==) + +-------------------------------------------------------------------------------- +-- Conversions +-------------------------------------------------------------------------------- + +||| Convert Maybe type into Vect +||| +||| ```idris example +||| maybeToVect (Just 2) +||| ``` +maybeToVect : Maybe elem -> (p ** Vect p elem) +maybeToVect Nothing = (_ ** []) +maybeToVect (Just j) = (_ ** [j]) + +||| Convert first element of Vect (if exists) into Maybe. +||| +||| ```idris example +||| vectToMaybe [2] +||| ``` +vectToMaybe : Vect len elem -> Maybe elem +vectToMaybe [] = Nothing +vectToMaybe (x::xs) = Just x + +-------------------------------------------------------------------------------- +-- Misc +-------------------------------------------------------------------------------- + +||| Filter out Nothings from Vect +||| +||| ```idris example +||| catMaybes [Just 1, Just 2, Nothing, Nothing, Just 5] +||| ``` +catMaybes : Vect n (Maybe elem) -> (p ** Vect p elem) +catMaybes [] = (_ ** []) +catMaybes (Nothing::xs) = catMaybes xs +catMaybes ((Just j)::xs) = + let (_ ** tail) = catMaybes xs + in (_ ** j::tail) + +||| Get diagonal elements +||| +||| ```idris example +||| diag [[1,2,3], [4,5,6], [7,8,9]] +||| ``` +diag : Vect len (Vect len elem) -> Vect len elem +diag [] = [] +diag ((x::xs)::xss) = x :: diag (map tail xss) + +range : {len : Nat} -> Vect len (Fin len) +range {len=Z} = [] +range {len=S _} = FZ :: map FS range + +||| Transpose a `Vect` of `Vect`s, turning rows into columns and vice versa. +||| +||| This is like zipping all the inner `Vect`s together and is equivalent to `traverse id` (`transposeTraverse`). +||| +||| As the types ensure rectangularity, this is an involution, unlike `Prelude.List.transpose`. +||| +||| ```idris example +||| transpose [[1,2], [3,4], [5,6], [7,8]] +||| ``` +transpose : {n : _} -> Vect m (Vect n elem) -> Vect n (Vect m elem) +transpose [] = replicate _ [] -- = [| [] |] +transpose (x :: xs) = zipWith (::) x (transpose xs) -- = [| x :: xs |] + +-------------------------------------------------------------------------------- +-- Applicative/Monad/Traversable +-------------------------------------------------------------------------------- + +-- implementation Applicative (Vect k) where +-- pure = replicate _ +-- fs <*> vs = zipWith apply fs vs +-- +-- ||| This monad is different from the List monad, (>>=) +-- ||| uses the diagonal. +-- implementation Monad (Vect len) where +-- m >>= f = diag (map f m) +-- +-- implementation Traversable (Vect n) where +-- traverse f [] = pure [] +-- traverse f (x :: xs) = pure (::) <*> (f x) <*> (traverse f xs) + +-------------------------------------------------------------------------------- +-- Show +-------------------------------------------------------------------------------- + +export +implementation Show elem => Show (Vect len elem) where + show = show . toList + +-- Some convenience functions for testing lengths + +-- Needs to be Maybe rather than Dec, because if 'n' is unequal to m, we +-- only know we don't know how to make a Vect n a, not that one can't exist. +export +exactLength : {m : Nat} -> -- expected at run-time + (len : Nat) -> (xs : Vect m a) -> Maybe (Vect len a) +exactLength {m} len xs with (decEq m len) + exactLength {m = m} m xs | (Yes Refl) = Just xs + exactLength {m = m} len xs | (No contra) = Nothing + +||| If the given Vect is at least the required length, return a Vect with +||| at least that length in its type, otherwise return Nothing +||| @len the required length +||| @xs the vector with the desired length +-- overLength : {m : Nat} -> -- expected at run-time +-- (len : Nat) -> (xs : Vect m a) -> Maybe (p ** Vect (plus p len) a) +-- overLength {m} n xs with (cmp m n) +-- overLength {m = m} (plus m (S y)) xs | (CmpLT y) = Nothing +-- overLength {m = m} m xs | CmpEQ +-- = Just (0 ** xs) +-- overLength {m = plus n (S x)} n xs | (CmpGT x) +-- = Just (S x ** rewrite plusCommutative (S x) n in xs) diff --git a/libs/base/Decidable/Equality.idr b/libs/base/Decidable/Equality.idr index 4c47fc1..8205864 100644 --- a/libs/base/Decidable/Equality.idr +++ b/libs/base/Decidable/Equality.idr @@ -1,5 +1,8 @@ module Decidable.Equality +import Data.Maybe +import Data.Nat + -------------------------------------------------------------------------------- -- Decidable equality -------------------------------------------------------------------------------- @@ -30,8 +33,57 @@ decEqSelfIsYes {x} with (decEq x x) --- Unit -------------------------------------------------------------------------------- +export implementation DecEq () where decEq () () = Yes Refl +-------------------------------------------------------------------------------- +-- Booleans +-------------------------------------------------------------------------------- +total trueNotFalse : True = False -> Void +trueNotFalse Refl impossible + +export +implementation DecEq Bool where + decEq True True = Yes Refl + decEq False False = Yes Refl + decEq True False = No trueNotFalse + decEq False True = No (negEqSym trueNotFalse) + +-------------------------------------------------------------------------------- +-- Nat +-------------------------------------------------------------------------------- + +total ZnotS : Z = S n -> Void +ZnotS Refl impossible + +export +implementation DecEq Nat where + decEq Z Z = Yes Refl + decEq Z (S _) = No ZnotS + decEq (S _) Z = No (negEqSym ZnotS) + decEq (S n) (S m) with (decEq n m) + decEq (S n) (S m) | Yes p = Yes $ cong S p + decEq (S n) (S m) | No p = No $ \h : (S n = S m) => p $ succInjective n m h + +-------------------------------------------------------------------------------- +-- Maybe +-------------------------------------------------------------------------------- + +total nothingNotJust : {x : t} -> (Nothing {ty = t} = Just x) -> Void +nothingNotJust Refl impossible + +export +implementation (DecEq t) => DecEq (Maybe t) where + decEq Nothing Nothing = Yes Refl + decEq (Just x') (Just y') with (decEq x' y') + decEq (Just x') (Just y') | Yes p = Yes $ cong Just p + decEq (Just x') (Just y') | No p + = No $ \h : Just x' = Just y' => p $ justInjective h + decEq Nothing (Just _) = No nothingNotJust + decEq (Just _) Nothing = No (negEqSym nothingNotJust) + -- TODO: Primitives and other prelude data types + + diff --git a/libs/prelude/Builtin.idr b/libs/prelude/Builtin.idr index e551c6d..8a4d11a 100644 --- a/libs/prelude/Builtin.idr +++ b/libs/prelude/Builtin.idr @@ -35,17 +35,10 @@ snd (x, y) = y 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 + record DPair a (p : a -> Type) where + constructor MkDPair + fst : a + snd : p fst -- The empty type diff --git a/src/Core/UnifyState.idr b/src/Core/UnifyState.idr index 4e7c829..0547dc6 100644 --- a/src/Core/UnifyState.idr +++ b/src/Core/UnifyState.idr @@ -592,7 +592,7 @@ dumpHole lvl hole ++ if inj then " (Invertible)" else "" (BySearch _ _ _, ty) => log lvl $ "Search " ++ show hole ++ " : " ++ - show !(normaliseHoles defs [] ty) + show !(toFullNames !(normaliseHoles defs [] ty)) (PMDef _ args t _ _, ty) => log 4 $ "Solved: " ++ show hole ++ " : " ++ show !(normalise defs [] ty) ++ diff --git a/src/TTImp/Elab.idr b/src/TTImp/Elab.idr index 4454c3f..8140f6b 100644 --- a/src/TTImp/Elab.idr +++ b/src/TTImp/Elab.idr @@ -89,6 +89,9 @@ elabTermSub {vars} defining mode opts nest env env' sub tm ty oldhs <- if not incase then saveHoles else pure empty + ust <- get UST + let olddelayed = delayedElab ust + put UST (record { delayedElab = [] } ust) defs <- get Ctxt e <- newRef EST (initEStateSub defining env' sub) @@ -108,8 +111,10 @@ elabTermSub {vars} defining mode opts nest env env' sub tm ty catch (retryDelayed (delayedElab ust)) (\err => do ust <- get UST - put UST (record { delayedElab = [] } ust) + put UST (record { delayedElab = olddelayed } ust) throw err) + ust <- get UST + put UST (record { delayedElab = olddelayed } ust) -- As long as we're not in a case block, finish off constraint solving when (not incase) $ -- resolve any default hints diff --git a/src/TTImp/Elab/Ambiguity.idr b/src/TTImp/Elab/Ambiguity.idr index 8b17ded..491c149 100644 --- a/src/TTImp/Elab/Ambiguity.idr +++ b/src/TTImp/Elab/Ambiguity.idr @@ -252,10 +252,10 @@ checkAlternative rig elabinfo nest env fc (UniqueDefault def) alts mexpected let solvemode = case elabMode elabinfo of InLHS c => InLHS _ => InTerm - solveConstraints solvemode Normal delayOnFailure fc rig env expected ambiguous $ (\delayed => - do defs <- get Ctxt + do solveConstraints solvemode Normal + defs <- get Ctxt alts' <- pruneByType !(getNF expected) alts if delayed -- use the default if there's still ambiguity then try @@ -278,10 +278,10 @@ checkAlternative rig elabinfo nest env fc uniq alts mexpected let solvemode = case elabMode elabinfo of InLHS c => InLHS _ => InTerm - solveConstraints solvemode Normal delayOnFailure fc rig env expected ambiguous $ (\delayed => - do defs <- get Ctxt + do solveConstraints solvemode Normal + defs <- get Ctxt alts' <- pruneByType !(getNF expected) alts exp <- getTerm expected -- If we don't know the target type on the first attempt, diff --git a/src/TTImp/Elab/Case.idr b/src/TTImp/Elab/Case.idr index 6072ed8..efd1c1a 100644 --- a/src/TTImp/Elab/Case.idr +++ b/src/TTImp/Elab/Case.idr @@ -10,6 +10,7 @@ import Core.TT import Core.Value import TTImp.Elab.Check +import TTImp.Elab.Delayed import TTImp.Elab.ImplicitBind import TTImp.TTImp @@ -418,26 +419,27 @@ checkCase : {vars : _} -> Maybe (Glued vars) -> Core (Term vars, Glued vars) checkCase rig elabinfo nest env fc scr scrty_exp alts exp - = do (scrtyv, scrtyt) <- check Rig0 elabinfo nest env scrty_exp - (Just (gType fc)) - - logTerm 10 "Expected scrutinee type" scrtyv - -- Try checking at the given multiplicity; if that doesn't work, - -- try checking at Rig1 (meaning that we're using a linear variable - -- so the scrutinee should be linear) - (scrtm_in, gscrty, caseRig) <- handle - (do c <- check RigW elabinfo nest env scr (Just (gnf env scrtyv)) - pure (fst c, snd c, RigW)) - (\err => case err of - LinearMisuse _ _ Rig1 _ - => do c <- check Rig1 elabinfo nest env scr - (Just (gnf env scrtyv)) - pure (fst c, snd c, Rig1) - e => throw e) - scrty <- getTerm gscrty - logTermNF 5 "Scrutinee type" env scrty - checkConcrete !(getNF gscrty) - caseBlock rig elabinfo fc nest env scr scrtm_in scrty caseRig alts exp + = delayElab fc rig env exp $ + do (scrtyv, scrtyt) <- check Rig0 elabinfo nest env scrty_exp + (Just (gType fc)) + + logTerm 10 "Expected scrutinee type" scrtyv + -- Try checking at the given multiplicity; if that doesn't work, + -- try checking at Rig1 (meaning that we're using a linear variable + -- so the scrutinee should be linear) + (scrtm_in, gscrty, caseRig) <- handle + (do c <- check RigW elabinfo nest env scr (Just (gnf env scrtyv)) + pure (fst c, snd c, RigW)) + (\err => case err of + LinearMisuse _ _ Rig1 _ + => do c <- check Rig1 elabinfo nest env scr + (Just (gnf env scrtyv)) + pure (fst c, snd c, Rig1) + e => throw e) + scrty <- getTerm gscrty + logTermNF 5 "Scrutinee type" env scrty + checkConcrete !(getNF gscrty) + caseBlock rig elabinfo fc nest env scr scrtm_in scrty caseRig alts exp where -- For the moment, throw an error if we haven't been able to work out -- the type of the case scrutinee, because we'll need it to build the diff --git a/src/TTImp/Elab/Check.idr b/src/TTImp/Elab/Check.idr index c28e96f..c998fa8 100644 --- a/src/TTImp/Elab/Check.idr +++ b/src/TTImp/Elab/Check.idr @@ -425,7 +425,7 @@ successful ((tm, elab) :: elabs) put MD md put Ctxt defs elabs' <- successful elabs - pure (Left (tm, err) :: elabs')) + pure (Left (tm, !(normaliseErr err)) :: elabs')) export exactlyOne : {vars : _} -> diff --git a/src/TTImp/Elab/Delayed.idr b/src/TTImp/Elab/Delayed.idr index 5e4cd19..34f522d 100644 --- a/src/TTImp/Elab/Delayed.idr +++ b/src/TTImp/Elab/Delayed.idr @@ -75,6 +75,41 @@ delayOnFailure fc rig env expected pred elab pure (dtm, expected) else throw err) +export +delayElab : {auto c : Ref Ctxt Defs} -> + {auto m : Ref MD Metadata} -> + {auto u : Ref UST UState} -> + {auto e : Ref EST (EState vars)} -> + FC -> RigCount -> Env Term vars -> + (expected : Maybe (Glued vars)) -> + Core (Term vars, Glued vars) -> + Core (Term vars, Glued vars) +delayElab {vars} fc rig env exp elab + = do est <- get EST + nm <- genName "delayed" + expected <- mkExpected exp + (ci, dtm) <- newDelayed fc Rig1 env nm !(getTerm expected) + logGlueNF 5 ("Postponing elaborator " ++ show nm ++ + " for") env expected + ust <- get UST + put UST (record { delayedElab $= + ((ci, mkClosedElab fc env + (do est <- get EST + put EST (record { allowDelay = False } est) + tm <- elab + est <- get EST + put EST (record { allowDelay = True } est) + pure tm)) :: ) } + ust) + pure (dtm, expected) + where + mkExpected : Maybe (Glued vars) -> Core (Glued vars) + mkExpected (Just ty) = pure ty + mkExpected Nothing + = do nm <- genName "delayTy" + ty <- metaVar fc Rig0 env nm (TType fc) + pure (gnf env ty) + export retryDelayed : {auto c : Ref Ctxt Defs} -> {auto u : Ref UST UState} -> diff --git a/tests/idris2/basic017/expected b/tests/idris2/basic017/expected index 8c895c0..940b9a8 100644 --- a/tests/idris2/basic017/expected +++ b/tests/idris2/basic017/expected @@ -1,6 +1,8 @@ 1/1: Building CaseInf (CaseInf.idr) CaseInf.idr:6:17--6:24:While processing right hand side of Main.test3bad at CaseInf.idr:6:1--9:1: -Can't infer type for case scrutinee +Ambiguous elaboration. Possible correct results: + Builtin.Pair (Prelude.fromInteger 1) (Prelude.fromInteger 2) + Builtin.MkPair (Prelude.fromInteger 1) (Prelude.fromInteger 2) Welcome to Idris 2 version 0.0. Enjoy yourself! Main> S (S (S Z)) Main> Bye for now! diff --git a/tests/ttimp/qtt002/expected b/tests/ttimp/qtt002/expected index 267d43d..dbf7124 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 m Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just {k:17} Main.Nat (%pi Rig1 Explicit Just ws ((Main.Vect {k:17}) a) (%pi RigW Explicit Nothing a (%pi Rig1 Explicit Just zs ((Main.Vect (Main.S {k:17})) a) (%pi RigW Explicit Nothing a (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just n Main.Nat ((Main.Vect ((Main.plus (Main.S (Main.S {k:17}))) 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:44} Main.Nat (%pi Rig1 Explicit Just zs ((Main.Vect {k:44}) a) (%pi RigW Explicit Nothing a (%pi Rig0 Explicit Just xs ((Main.Vect (Main.S {k:44})) a) (%pi Rig0 Explicit Just n Main.Nat ((Main.Vect ((Main.plus (Main.S {k:44})) 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:72} Main.Nat (%pi Rig0 Explicit Just zs ((Main.Vect {k:72}) a) (%pi RigW Explicit Nothing a (%pi Rig0 Explicit Just xs ((Main.Vect (Main.S {k:72})) a) (%pi Rig0 Explicit Just n Main.Nat (%pi Rig1 Explicit Just ts ((Main.Vect {k:72}) a) ((Main.Vect ((Main.plus (Main.S {k:72})) 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:45} Main.Nat (%pi Rig1 Explicit Just zs ((Main.Vect {k:45}) a) (%pi RigW Explicit Nothing a (%pi Rig0 Explicit Just xs ((Main.Vect (Main.S {k:45})) a) (%pi Rig0 Explicit Just n Main.Nat ((Main.Vect ((Main.plus (Main.S {k:45})) 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:74} Main.Nat (%pi Rig0 Explicit Just zs ((Main.Vect {k:74}) a) (%pi RigW Explicit Nothing a (%pi Rig0 Explicit Just xs ((Main.Vect (Main.S {k:74})) a) (%pi Rig0 Explicit Just n Main.Nat (%pi Rig1 Explicit Just ts ((Main.Vect {k:74}) a) ((Main.Vect ((Main.plus (Main.S {k:74})) m)) a))))))))))))))) Yaffle> Bye for now!